%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : TOP034+1 : TPTP v8.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n013.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 21:15:12 EDT 2024 % Result : Theorem 58.70s 58.87s % Output : CNFRefutation 58.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : TOP034+1 : TPTP v8.2.0. Released v3.4.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n013.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Tue Jun 18 11:07:39 EDT 2024 % 0.11/0.33 % CPUTime : % 0.18/0.55 start to proof:theBenchmark % 58.70/58.83 %------------------------------------------- % 58.70/58.83 % File :CSE---1.7 % 58.70/58.83 % Problem :theBenchmark % 58.70/58.83 % Transform :cnf % 58.70/58.83 % Format :tptp:raw % 58.70/58.83 % Command :java -jar mcs_scs.jar %d %s % 58.70/58.83 % 58.70/58.83 % Result :Theorem 58.160000s % 58.70/58.83 % Output :CNFRefutation 58.160000s % 58.70/58.83 %------------------------------------------- % 58.70/58.84 %------------------------------------------------------------------------------ % 58.70/58.84 % File : TOP034+1 : TPTP v8.2.0. Released v3.4.0. % 58.70/58.84 % Domain : Topology % 58.70/58.84 % Problem : Maximal Kolmogorov Subspaces of a Topological Space T23 % 58.70/58.84 % Version : [Urb08] axioms : Especial. % 58.70/58.84 % English : % 58.70/58.84 % 58.70/58.84 % Refs : [Kar96] Karno (1996), Maximal Kolmogorov Subspaces of a Topolo % 58.70/58.84 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 58.70/58.84 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 58.70/58.84 % Source : [Urb08] % 58.70/58.84 % Names : t23_tsp_2 [Urb08] % 58.70/58.84 % 58.70/58.84 % Status : Theorem % 58.70/58.84 % Rating : 0.19 v8.1.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.17 v7.3.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.17 v6.2.0, 0.16 v6.1.0, 0.20 v6.0.0, 0.17 v5.5.0, 0.22 v5.4.0, 0.29 v5.3.0, 0.30 v5.2.0, 0.15 v5.1.0, 0.24 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.0, 0.29 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0 % 58.70/58.84 % Syntax : Number of formulae : 95 ( 14 unt; 0 def) % 58.70/58.84 % Number of atoms : 466 ( 2 equ) % 58.70/58.84 % Maximal formula atoms : 15 ( 4 avg) % 58.70/58.84 % Number of connectives : 476 ( 105 ~; 1 |; 230 &) % 58.70/58.84 % ( 4 <=>; 136 =>; 0 <=; 0 <~>) % 58.70/58.84 % Maximal formula depth : 15 ( 6 avg) % 58.70/58.84 % Maximal term depth : 3 ( 1 avg) % 58.70/58.84 % Number of predicates : 46 ( 44 usr; 1 prp; 0-3 aty) % 58.70/58.84 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 58.70/58.84 % Number of variables : 160 ( 139 !; 21 ?) % 58.70/58.84 % SPC : FOF_THM_RFO_SEQ % 58.70/58.84 % 58.70/58.84 % Comments : Normal version: includes the axioms (which may be theorems from % 58.70/58.84 % other articles) and background that are possibly necessary. % 58.70/58.84 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 58.70/58.84 % : The problem encoding is based on set theory. % 58.70/58.84 %------------------------------------------------------------------------------ % 58.70/58.84 fof(t23_tsp_2,conjecture, % 58.70/58.84 ! [A] : % 58.70/58.84 ( ( ~ v3_struct_0(A) % 58.70/58.84 & v2_pre_topc(A) % 58.70/58.84 & l1_pre_topc(A) ) % 58.70/58.84 => ! [B] : % 58.70/58.84 ( ( ~ v3_struct_0(B) % 58.70/58.84 & v2_tsp_2(B,A) % 58.70/58.84 & m2_tsp_1(B,A) ) % 58.70/58.84 => r1_borsuk_1(A,B) ) ) ). % 58.70/58.84 % 58.70/58.84 fof(antisymmetry_r2_hidden,axiom, % 58.70/58.84 ! [A,B] : % 58.70/58.84 ( r2_hidden(A,B) % 58.70/58.84 => ~ r2_hidden(B,A) ) ). % 58.70/58.84 % 58.70/58.84 fof(cc10_membered,axiom, % 58.70/58.84 ! [A] : % 58.70/58.84 ( v1_membered(A) % 58.70/58.84 => ! [B] : % 58.70/58.84 ( m1_subset_1(B,A) % 58.70/58.84 => v1_xcmplx_0(B) ) ) ). % 58.70/58.84 % 58.70/58.84 fof(cc10_tsp_1,axiom, % 58.70/58.84 ! [A] : % 58.70/58.84 ( l1_pre_topc(A) % 58.70/58.84 => ( ( ~ v3_struct_0(A) % 58.70/58.84 & v2_pre_topc(A) % 58.70/58.84 & ~ v1_tdlat_3(A) % 58.70/58.84 & v2_t_0topsp(A) ) % 58.70/58.84 => ( ~ v3_struct_0(A) % 58.70/58.84 & ~ v3_realset2(A) % 58.70/58.84 & v2_pre_topc(A) % 58.70/58.84 & ~ v1_tdlat_3(A) % 58.70/58.84 & ~ v2_tdlat_3(A) % 58.70/58.84 & ~ v3_tdlat_3(A) ) ) ) ). % 58.70/58.84 % 58.70/58.84 fof(cc10_tsp_2,axiom, % 58.70/58.84 ! [A] : % 58.70/58.84 ( ( ~ v3_struct_0(A) % 58.70/58.84 & v2_pre_topc(A) % 58.70/58.84 & l1_pre_topc(A) ) % 58.70/58.84 => ! [B] : % 58.70/58.84 ( m1_pre_topc(B,A) % 58.70/58.84 => ( ( v2_tex_2(B,A) % 58.70/58.84 & v2_tsp_2(B,A) ) % 58.70/58.84 => ( v2_pre_topc(B) % 58.70/58.84 & ~ v1_borsuk_1(B,A) ) ) ) ) ). % 58.70/58.84 % 58.70/58.84 fof(cc11_membered,axiom, % 58.70/58.84 ! [A] : % 58.70/58.84 ( v2_membered(A) % 58.70/58.84 => ! [B] : % 58.70/58.84 ( m1_subset_1(B,A) % 58.70/58.84 => ( v1_xcmplx_0(B) % 58.70/58.84 & v1_xreal_0(B) ) ) ) ). % 58.70/58.84 % 58.70/58.84 fof(cc11_tsp_1,axiom, % 58.70/58.84 ! [A] : % 58.70/58.84 ( ( ~ v3_struct_0(A) % 58.70/58.84 & v2_pre_topc(A) % 58.70/58.84 & v2_t_0topsp(A) % 58.70/58.84 & l1_pre_topc(A) ) % 58.70/58.84 => ! [B] : % 58.70/58.84 ( m1_pre_topc(B,A) % 58.70/58.84 => ( ~ v3_struct_0(B) % 58.70/58.84 => ( ~ v3_struct_0(B) % 58.70/58.84 & v2_t_0topsp(B) ) ) ) ) ). % 58.70/58.84 % 58.70/58.84 fof(cc12_membered,axiom, % 58.70/58.84 ! [A] : % 58.70/58.84 ( v3_membered(A) % 58.70/58.84 => ! [B] : % 58.70/58.84 ( m1_subset_1(B,A) % 58.70/58.84 => ( v1_xcmplx_0(B) % 58.70/58.84 & v1_xreal_0(B) % 58.70/58.84 & v1_rat_1(B) ) ) ) ). % 58.70/58.84 % 58.70/58.84 fof(cc12_tsp_1,axiom, % 58.70/58.84 ! [A] : % 58.70/58.84 ( ( ~ v3_struct_0(A) % 58.70/58.84 & v2_pre_topc(A) % 58.70/58.84 & ~ v2_t_0topsp(A) % 58.70/58.84 & l1_pre_topc(A) ) % 58.70/58.84 => ! [B] : % 58.70/58.84 ( m1_pre_topc(B,A) % 58.70/58.84 => ( ( ~ v3_struct_0(B) % 58.70/58.84 & ~ v2_tex_2(B,A) ) % 58.70/58.84 => ( ~ v3_struct_0(B) % 58.70/58.84 & ~ v3_realset2(B) % 58.70/58.84 & ~ v2_t_0topsp(B) ) ) ) ) ). % 58.70/58.84 % 58.70/58.84 fof(cc13_membered,axiom, % 58.70/58.84 ! [A] : % 58.70/58.84 ( v4_membered(A) % 58.70/58.85 => ! [B] : % 58.70/58.85 ( m1_subset_1(B,A) % 58.70/58.85 => ( v1_xcmplx_0(B) % 58.70/58.85 & v1_xreal_0(B) % 58.70/58.85 & v1_int_1(B) % 58.70/58.85 & v1_rat_1(B) ) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc13_tsp_1,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( ( ~ v3_struct_0(A) % 58.70/58.85 & v2_pre_topc(A) % 58.70/58.85 & ~ v2_t_0topsp(A) % 58.70/58.85 & l1_pre_topc(A) ) % 58.70/58.85 => ! [B] : % 58.70/58.85 ( m1_pre_topc(B,A) % 58.70/58.85 => ( ( ~ v3_struct_0(B) % 58.70/58.85 & v2_t_0topsp(B) ) % 58.70/58.85 => ( ~ v3_struct_0(B) % 58.70/58.85 & v2_tex_2(B,A) ) ) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc14_membered,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( v5_membered(A) % 58.70/58.85 => ! [B] : % 58.70/58.85 ( m1_subset_1(B,A) % 58.70/58.85 => ( v1_xcmplx_0(B) % 58.70/58.85 & v4_ordinal2(B) % 58.70/58.85 & v1_xreal_0(B) % 58.70/58.85 & v1_int_1(B) % 58.70/58.85 & v1_rat_1(B) ) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc15_membered,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( v1_xboole_0(A) % 58.70/58.85 => ( v1_membered(A) % 58.70/58.85 & v2_membered(A) % 58.70/58.85 & v3_membered(A) % 58.70/58.85 & v4_membered(A) % 58.70/58.85 & v5_membered(A) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc16_membered,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( v1_membered(A) % 58.70/58.85 => ! [B] : % 58.70/58.85 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.70/58.85 => v1_membered(B) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc17_membered,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( v2_membered(A) % 58.70/58.85 => ! [B] : % 58.70/58.85 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.70/58.85 => ( v1_membered(B) % 58.70/58.85 & v2_membered(B) ) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc18_membered,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( v3_membered(A) % 58.70/58.85 => ! [B] : % 58.70/58.85 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.70/58.85 => ( v1_membered(B) % 58.70/58.85 & v2_membered(B) % 58.70/58.85 & v3_membered(B) ) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc19_membered,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( v4_membered(A) % 58.70/58.85 => ! [B] : % 58.70/58.85 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.70/58.85 => ( v1_membered(B) % 58.70/58.85 & v2_membered(B) % 58.70/58.85 & v3_membered(B) % 58.70/58.85 & v4_membered(B) ) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc1_membered,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( v5_membered(A) % 58.70/58.85 => v4_membered(A) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc1_pre_topc,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( ( v2_pre_topc(A) % 58.70/58.85 & l1_pre_topc(A) ) % 58.70/58.85 => ! [B] : % 58.70/58.85 ( m1_pre_topc(B,A) % 58.70/58.85 => v2_pre_topc(B) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc1_relset_1,axiom, % 58.70/58.85 ! [A,B,C] : % 58.70/58.85 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 58.70/58.85 => v1_relat_1(C) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc1_tops_1,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( ( v2_pre_topc(A) % 58.70/58.85 & l1_pre_topc(A) ) % 58.70/58.85 => ! [B] : % 58.70/58.85 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.85 => ( v1_xboole_0(B) % 58.70/58.85 => ( v3_pre_topc(B,A) % 58.70/58.85 & v4_pre_topc(B,A) ) ) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc1_tsp_1,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( l1_pre_topc(A) % 58.70/58.85 => ( ( ~ v3_struct_0(A) % 58.70/58.85 & v3_realset2(A) ) % 58.70/58.85 => ( ~ v3_struct_0(A) % 58.70/58.85 & v2_t_0topsp(A) ) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc1_tsp_2,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( ( ~ v3_struct_0(A) % 58.70/58.85 & l1_pre_topc(A) ) % 58.70/58.85 => ! [B] : % 58.70/58.85 ( m1_pre_topc(B,A) % 58.70/58.85 => ( ( ~ v3_struct_0(B) % 58.70/58.85 & v2_tsp_2(B,A) ) % 58.70/58.85 => ( ~ v3_struct_0(B) % 58.70/58.85 & v2_t_0topsp(B) ) ) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc20_membered,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( v5_membered(A) % 58.70/58.85 => ! [B] : % 58.70/58.85 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.70/58.85 => ( v1_membered(B) % 58.70/58.85 & v2_membered(B) % 58.70/58.85 & v3_membered(B) % 58.70/58.85 & v4_membered(B) % 58.70/58.85 & v5_membered(B) ) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc2_membered,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( v4_membered(A) % 58.70/58.85 => v3_membered(A) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc2_tops_1,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( l1_pre_topc(A) % 58.70/58.85 => ! [B] : % 58.70/58.85 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.85 => ( v1_xboole_0(B) % 58.70/58.85 => v2_tops_1(B,A) ) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc2_tsp_1,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( l1_pre_topc(A) % 58.70/58.85 => ( ( ~ v3_struct_0(A) % 58.70/58.85 & ~ v2_t_0topsp(A) ) % 58.70/58.85 => ( ~ v3_struct_0(A) % 58.70/58.85 & ~ v3_realset2(A) ) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc2_tsp_2,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( ( ~ v3_struct_0(A) % 58.70/58.85 & l1_pre_topc(A) ) % 58.70/58.85 => ! [B] : % 58.70/58.85 ( m1_pre_topc(B,A) % 58.70/58.85 => ( ( ~ v3_struct_0(B) % 58.70/58.85 & ~ v2_t_0topsp(B) ) % 58.70/58.85 => ( ~ v3_struct_0(B) % 58.70/58.85 & ~ v2_tsp_2(B,A) ) ) ) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc3_membered,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( v3_membered(A) % 58.70/58.85 => v2_membered(A) ) ). % 58.70/58.85 % 58.70/58.85 fof(cc3_tops_1,axiom, % 58.70/58.85 ! [A] : % 58.70/58.85 ( ( v2_pre_topc(A) % 58.70/58.85 & l1_pre_topc(A) ) % 58.70/58.85 => ! [B] : % 58.70/58.86 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.86 => ( v1_xboole_0(B) % 58.70/58.86 => v3_tops_1(B,A) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc3_tsp_1,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( l1_pre_topc(A) % 58.70/58.86 => ( ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & v1_tdlat_3(A) ) % 58.70/58.86 => ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & v2_t_0topsp(A) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc3_tsp_2,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & l1_pre_topc(A) ) % 58.70/58.86 => ! [B] : % 58.70/58.86 ( m1_pre_topc(B,A) % 58.70/58.86 => ( v2_tsp_2(B,A) % 58.70/58.86 => ( v2_pre_topc(B) % 58.70/58.86 & v1_tex_3(B,A) ) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc4_membered,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( v2_membered(A) % 58.70/58.86 => v1_membered(A) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc4_tops_1,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( ( v2_pre_topc(A) % 58.70/58.86 & l1_pre_topc(A) ) % 58.70/58.86 => ! [B] : % 58.70/58.86 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.86 => ( v3_tops_1(B,A) % 58.70/58.86 => v2_tops_1(B,A) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc4_tsp_1,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( l1_pre_topc(A) % 58.70/58.86 => ( ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & ~ v2_t_0topsp(A) ) % 58.70/58.86 => ( ~ v3_struct_0(A) % 58.70/58.86 & ~ v3_realset2(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & ~ v1_tdlat_3(A) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc4_tsp_2,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & l1_pre_topc(A) ) % 58.70/58.86 => ! [B] : % 58.70/58.86 ( m1_pre_topc(B,A) % 58.70/58.86 => ( ~ v1_tex_3(B,A) % 58.70/58.86 => ( v2_pre_topc(B) % 58.70/58.86 & ~ v2_tsp_2(B,A) ) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc5_tops_1,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( ( v2_pre_topc(A) % 58.70/58.86 & l1_pre_topc(A) ) % 58.70/58.86 => ! [B] : % 58.70/58.86 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.86 => ( ( v4_pre_topc(B,A) % 58.70/58.86 & v2_tops_1(B,A) ) % 58.70/58.86 => ( v2_tops_1(B,A) % 58.70/58.86 & v3_tops_1(B,A) ) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc5_tsp_1,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( l1_pre_topc(A) % 58.70/58.86 => ( ( ~ v3_struct_0(A) % 58.70/58.86 & ~ v3_realset2(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & v2_tdlat_3(A) ) % 58.70/58.86 => ( ~ v3_struct_0(A) % 58.70/58.86 & ~ v3_realset2(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & ~ v2_t_0topsp(A) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc5_tsp_2,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & l1_pre_topc(A) ) % 58.70/58.86 => ! [B] : % 58.70/58.86 ( m1_pre_topc(B,A) % 58.70/58.86 => ( ( v1_tsep_1(B,A) % 58.70/58.86 & v2_tsp_2(B,A) ) % 58.70/58.86 => ( v2_pre_topc(B) % 58.70/58.86 & ~ v2_tex_2(B,A) ) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc6_tops_1,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( ( v2_pre_topc(A) % 58.70/58.86 & l1_pre_topc(A) ) % 58.70/58.86 => ! [B] : % 58.70/58.86 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.86 => ( ( v3_pre_topc(B,A) % 58.70/58.86 & v3_tops_1(B,A) ) % 58.70/58.86 => ( v1_xboole_0(B) % 58.70/58.86 & v3_pre_topc(B,A) % 58.70/58.86 & v4_pre_topc(B,A) % 58.70/58.86 & v1_membered(B) % 58.70/58.86 & v2_membered(B) % 58.70/58.86 & v3_membered(B) % 58.70/58.86 & v4_membered(B) % 58.70/58.86 & v5_membered(B) % 58.70/58.86 & v2_tops_1(B,A) % 58.70/58.86 & v3_tops_1(B,A) ) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc6_tsp_1,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( l1_pre_topc(A) % 58.70/58.86 => ( ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & v2_tdlat_3(A) % 58.70/58.86 & v2_t_0topsp(A) ) % 58.70/58.86 => ( ~ v3_struct_0(A) % 58.70/58.86 & v3_realset2(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & v1_tdlat_3(A) % 58.70/58.86 & v2_tdlat_3(A) % 58.70/58.86 & v3_tdlat_3(A) % 58.70/58.86 & v4_tdlat_3(A) % 58.70/58.86 & v5_tdlat_3(A) % 58.70/58.86 & v2_t_0topsp(A) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc6_tsp_2,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & l1_pre_topc(A) ) % 58.70/58.86 => ! [B] : % 58.70/58.86 ( m1_pre_topc(B,A) % 58.70/58.86 => ( ( v1_tsep_1(B,A) % 58.70/58.86 & v2_tex_2(B,A) ) % 58.70/58.86 => ( v2_pre_topc(B) % 58.70/58.86 & ~ v2_tsp_2(B,A) ) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc7_tsp_1,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( l1_pre_topc(A) % 58.70/58.86 => ( ( ~ v3_struct_0(A) % 58.70/58.86 & ~ v3_realset2(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & v2_t_0topsp(A) ) % 58.70/58.86 => ( ~ v3_struct_0(A) % 58.70/58.86 & ~ v3_realset2(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & ~ v2_tdlat_3(A) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc7_tsp_2,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & l1_pre_topc(A) ) % 58.70/58.86 => ! [B] : % 58.70/58.86 ( m1_pre_topc(B,A) % 58.70/58.86 => ( ( v2_tex_2(B,A) % 58.70/58.86 & v2_tsp_2(B,A) ) % 58.70/58.86 => ( v2_pre_topc(B) % 58.70/58.86 & ~ v1_tsep_1(B,A) ) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc8_tsp_1,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( l1_pre_topc(A) % 58.70/58.86 => ( ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & v3_tdlat_3(A) % 58.70/58.86 & v2_t_0topsp(A) ) % 58.70/58.86 => ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & v1_tdlat_3(A) % 58.70/58.86 & v3_tdlat_3(A) % 58.70/58.86 & v4_tdlat_3(A) % 58.70/58.86 & v5_tdlat_3(A) % 58.70/58.86 & v2_t_0topsp(A) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc8_tsp_2,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & l1_pre_topc(A) ) % 58.70/58.86 => ! [B] : % 58.70/58.86 ( m1_pre_topc(B,A) % 58.70/58.86 => ( ( v1_borsuk_1(B,A) % 58.70/58.86 & v2_tsp_2(B,A) ) % 58.70/58.86 => ( v2_pre_topc(B) % 58.70/58.86 & ~ v2_tex_2(B,A) ) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc9_tsp_1,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( l1_pre_topc(A) % 58.70/58.86 => ( ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & ~ v1_tdlat_3(A) % 58.70/58.86 & v3_tdlat_3(A) ) % 58.70/58.86 => ( ~ v3_struct_0(A) % 58.70/58.86 & ~ v3_realset2(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & ~ v1_tdlat_3(A) % 58.70/58.86 & ~ v2_t_0topsp(A) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(cc9_tsp_2,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & l1_pre_topc(A) ) % 58.70/58.86 => ! [B] : % 58.70/58.86 ( m1_pre_topc(B,A) % 58.70/58.86 => ( ( v2_tex_2(B,A) % 58.70/58.86 & v1_borsuk_1(B,A) ) % 58.70/58.86 => ( v2_pre_topc(B) % 58.70/58.86 & ~ v2_tsp_2(B,A) ) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(d20_borsuk_1,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( ( ~ v3_struct_0(A) % 58.70/58.86 & v2_pre_topc(A) % 58.70/58.86 & l1_pre_topc(A) ) % 58.70/58.86 => ! [B] : % 58.70/58.86 ( ( ~ v3_struct_0(B) % 58.70/58.86 & m1_pre_topc(B,A) ) % 58.70/58.86 => ( r1_borsuk_1(A,B) % 58.70/58.86 <=> ? [C] : % 58.70/58.86 ( v1_funct_1(C) % 58.70/58.86 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 58.70/58.86 & v5_pre_topc(C,A,B) % 58.70/58.86 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 58.70/58.86 & v3_borsuk_1(C,A,B) ) ) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(dt_k1_xboole_0,axiom, % 58.70/58.86 $true ). % 58.70/58.86 % 58.70/58.86 fof(dt_k1_zfmisc_1,axiom, % 58.70/58.86 $true ). % 58.70/58.86 % 58.70/58.86 fof(dt_k2_zfmisc_1,axiom, % 58.70/58.86 $true ). % 58.70/58.86 % 58.70/58.86 fof(dt_l1_pre_topc,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( l1_pre_topc(A) % 58.70/58.86 => l1_struct_0(A) ) ). % 58.70/58.86 % 58.70/58.86 fof(dt_l1_struct_0,axiom, % 58.70/58.86 $true ). % 58.70/58.86 % 58.70/58.86 fof(dt_m1_pre_topc,axiom, % 58.70/58.86 ! [A] : % 58.70/58.86 ( l1_pre_topc(A) % 58.70/58.86 => ! [B] : % 58.70/58.86 ( m1_pre_topc(B,A) % 58.70/58.86 => l1_pre_topc(B) ) ) ). % 58.70/58.86 % 58.70/58.86 fof(dt_m1_relset_1,axiom, % 58.70/58.86 $true ). % 58.70/58.86 % 58.70/58.86 fof(dt_m1_subset_1,axiom, % 58.70/58.87 $true ). % 58.70/58.87 % 58.70/58.87 fof(dt_m2_relset_1,axiom, % 58.70/58.87 ! [A,B,C] : % 58.70/58.87 ( m2_relset_1(C,A,B) % 58.70/58.87 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 58.70/58.87 % 58.70/58.87 fof(dt_m2_tsp_1,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( l1_pre_topc(A) % 58.70/58.87 => ! [B] : % 58.70/58.87 ( m2_tsp_1(B,A) % 58.70/58.87 => l1_pre_topc(B) ) ) ). % 58.70/58.87 % 58.70/58.87 fof(dt_u1_struct_0,axiom, % 58.70/58.87 $true ). % 58.70/58.87 % 58.70/58.87 fof(existence_l1_pre_topc,axiom, % 58.70/58.87 ? [A] : l1_pre_topc(A) ). % 58.70/58.87 % 58.70/58.87 fof(existence_l1_struct_0,axiom, % 58.70/58.87 ? [A] : l1_struct_0(A) ). % 58.70/58.87 % 58.70/58.87 fof(existence_m1_pre_topc,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( l1_pre_topc(A) % 58.70/58.87 => ? [B] : m1_pre_topc(B,A) ) ). % 58.70/58.87 % 58.70/58.87 fof(existence_m1_relset_1,axiom, % 58.70/58.87 ! [A,B] : % 58.70/58.87 ? [C] : m1_relset_1(C,A,B) ). % 58.70/58.87 % 58.70/58.87 fof(existence_m1_subset_1,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ? [B] : m1_subset_1(B,A) ). % 58.70/58.87 % 58.70/58.87 fof(existence_m2_relset_1,axiom, % 58.70/58.87 ! [A,B] : % 58.70/58.87 ? [C] : m2_relset_1(C,A,B) ). % 58.70/58.87 % 58.70/58.87 fof(existence_m2_tsp_1,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( l1_pre_topc(A) % 58.70/58.87 => ? [B] : m2_tsp_1(B,A) ) ). % 58.70/58.87 % 58.70/58.87 fof(fc1_struct_0,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( ( ~ v3_struct_0(A) % 58.70/58.87 & l1_struct_0(A) ) % 58.70/58.87 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 58.70/58.87 % 58.70/58.87 fof(fc1_subset_1,axiom, % 58.70/58.87 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 58.70/58.87 % 58.70/58.87 fof(fc4_subset_1,axiom, % 58.70/58.87 ! [A,B] : % 58.70/58.87 ( ( ~ v1_xboole_0(A) % 58.70/58.87 & ~ v1_xboole_0(B) ) % 58.70/58.87 => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ). % 58.70/58.87 % 58.70/58.87 fof(fc6_membered,axiom, % 58.70/58.87 ( v1_xboole_0(k1_xboole_0) % 58.70/58.87 & v1_membered(k1_xboole_0) % 58.70/58.87 & v2_membered(k1_xboole_0) % 58.70/58.87 & v3_membered(k1_xboole_0) % 58.70/58.87 & v4_membered(k1_xboole_0) % 58.70/58.87 & v5_membered(k1_xboole_0) ) ). % 58.70/58.87 % 58.70/58.87 fof(rc1_membered,axiom, % 58.70/58.87 ? [A] : % 58.70/58.87 ( ~ v1_xboole_0(A) % 58.70/58.87 & v1_membered(A) % 58.70/58.87 & v2_membered(A) % 58.70/58.87 & v3_membered(A) % 58.70/58.87 & v4_membered(A) % 58.70/58.87 & v5_membered(A) ) ). % 58.70/58.87 % 58.70/58.87 fof(rc1_subset_1,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( ~ v1_xboole_0(A) % 58.70/58.87 => ? [B] : % 58.70/58.87 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.70/58.87 & ~ v1_xboole_0(B) ) ) ). % 58.70/58.87 % 58.70/58.87 fof(rc1_tops_1,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( ( v2_pre_topc(A) % 58.70/58.87 & l1_pre_topc(A) ) % 58.70/58.87 => ? [B] : % 58.70/58.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.87 & v3_pre_topc(B,A) ) ) ). % 58.70/58.87 % 58.70/58.87 fof(rc2_subset_1,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ? [B] : % 58.70/58.87 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.70/58.87 & v1_xboole_0(B) ) ). % 58.70/58.87 % 58.70/58.87 fof(rc2_tops_1,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( ( v2_pre_topc(A) % 58.70/58.87 & l1_pre_topc(A) ) % 58.70/58.87 => ? [B] : % 58.70/58.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.87 & v3_pre_topc(B,A) % 58.70/58.87 & v4_pre_topc(B,A) ) ) ). % 58.70/58.87 % 58.70/58.87 fof(rc3_struct_0,axiom, % 58.70/58.87 ? [A] : % 58.70/58.87 ( l1_struct_0(A) % 58.70/58.87 & ~ v3_struct_0(A) ) ). % 58.70/58.87 % 58.70/58.87 fof(rc3_tops_1,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( ( ~ v3_struct_0(A) % 58.70/58.87 & v2_pre_topc(A) % 58.70/58.87 & l1_pre_topc(A) ) % 58.70/58.87 => ? [B] : % 58.70/58.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.87 & ~ v1_xboole_0(B) % 58.70/58.87 & v3_pre_topc(B,A) % 58.70/58.87 & v4_pre_topc(B,A) ) ) ). % 58.70/58.87 % 58.70/58.87 fof(rc4_tops_1,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( l1_pre_topc(A) % 58.70/58.87 => ? [B] : % 58.70/58.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.87 & v1_xboole_0(B) % 58.70/58.87 & v1_membered(B) % 58.70/58.87 & v2_membered(B) % 58.70/58.87 & v3_membered(B) % 58.70/58.87 & v4_membered(B) % 58.70/58.87 & v5_membered(B) % 58.70/58.87 & v2_tops_1(B,A) ) ) ). % 58.70/58.87 % 58.70/58.87 fof(rc5_struct_0,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( ( ~ v3_struct_0(A) % 58.70/58.87 & l1_struct_0(A) ) % 58.70/58.87 => ? [B] : % 58.70/58.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.87 & ~ v1_xboole_0(B) ) ) ). % 58.70/58.87 % 58.70/58.87 fof(rc5_tops_1,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( ( v2_pre_topc(A) % 58.70/58.87 & l1_pre_topc(A) ) % 58.70/58.87 => ? [B] : % 58.70/58.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.87 & v1_xboole_0(B) % 58.70/58.87 & v3_pre_topc(B,A) % 58.70/58.87 & v4_pre_topc(B,A) % 58.70/58.87 & v1_membered(B) % 58.70/58.87 & v2_membered(B) % 58.70/58.87 & v3_membered(B) % 58.70/58.87 & v4_membered(B) % 58.70/58.87 & v5_membered(B) % 58.70/58.87 & v2_tops_1(B,A) % 58.70/58.87 & v3_tops_1(B,A) ) ) ). % 58.70/58.87 % 58.70/58.87 fof(rc6_pre_topc,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( ( v2_pre_topc(A) % 58.70/58.87 & l1_pre_topc(A) ) % 58.70/58.87 => ? [B] : % 58.70/58.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.87 & v4_pre_topc(B,A) ) ) ). % 58.70/58.87 % 58.70/58.87 fof(rc7_pre_topc,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( ( ~ v3_struct_0(A) % 58.70/58.87 & v2_pre_topc(A) % 58.70/58.87 & l1_pre_topc(A) ) % 58.70/58.87 => ? [B] : % 58.70/58.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.70/58.87 & ~ v1_xboole_0(B) % 58.70/58.87 & v4_pre_topc(B,A) ) ) ). % 58.70/58.87 % 58.70/58.87 fof(redefinition_m2_relset_1,axiom, % 58.70/58.87 ! [A,B,C] : % 58.70/58.87 ( m2_relset_1(C,A,B) % 58.70/58.87 <=> m1_relset_1(C,A,B) ) ). % 58.70/58.87 % 58.70/58.87 fof(redefinition_m2_tsp_1,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( l1_pre_topc(A) % 58.70/58.87 => ! [B] : % 58.70/58.87 ( m2_tsp_1(B,A) % 58.70/58.87 <=> m1_pre_topc(B,A) ) ) ). % 58.70/58.87 % 58.70/58.87 fof(reflexivity_r1_tarski,axiom, % 58.70/58.87 ! [A,B] : r1_tarski(A,A) ). % 58.70/58.87 % 58.70/58.87 fof(t1_subset,axiom, % 58.70/58.87 ! [A,B] : % 58.70/58.87 ( r2_hidden(A,B) % 58.70/58.87 => m1_subset_1(A,B) ) ). % 58.70/58.87 % 58.70/58.87 fof(t22_tsp_2,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( ( ~ v3_struct_0(A) % 58.70/58.87 & v2_pre_topc(A) % 58.70/58.87 & l1_pre_topc(A) ) % 58.70/58.87 => ! [B] : % 58.70/58.87 ( ( ~ v3_struct_0(B) % 58.70/58.87 & v2_tsp_2(B,A) % 58.70/58.87 & m2_tsp_1(B,A) ) % 58.70/58.87 => ? [C] : % 58.70/58.87 ( v1_funct_1(C) % 58.70/58.87 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 58.70/58.87 & v5_pre_topc(C,A,B) % 58.70/58.87 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 58.70/58.87 & v3_borsuk_1(C,A,B) ) ) ) ). % 58.70/58.87 % 58.70/58.87 fof(t2_subset,axiom, % 58.70/58.87 ! [A,B] : % 58.70/58.87 ( m1_subset_1(A,B) % 58.70/58.87 => ( v1_xboole_0(B) % 58.70/58.87 | r2_hidden(A,B) ) ) ). % 58.70/58.87 % 58.70/58.87 fof(t3_subset,axiom, % 58.70/58.87 ! [A,B] : % 58.70/58.87 ( m1_subset_1(A,k1_zfmisc_1(B)) % 58.70/58.87 <=> r1_tarski(A,B) ) ). % 58.70/58.87 % 58.70/58.87 fof(t4_subset,axiom, % 58.70/58.87 ! [A,B,C] : % 58.70/58.87 ( ( r2_hidden(A,B) % 58.70/58.87 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 58.70/58.87 => m1_subset_1(A,C) ) ). % 58.70/58.87 % 58.70/58.87 fof(t5_subset,axiom, % 58.70/58.87 ! [A,B,C] : % 58.70/58.87 ~ ( r2_hidden(A,B) % 58.70/58.87 & m1_subset_1(B,k1_zfmisc_1(C)) % 58.70/58.87 & v1_xboole_0(C) ) ). % 58.70/58.87 % 58.70/58.87 fof(t6_boole,axiom, % 58.70/58.87 ! [A] : % 58.70/58.87 ( v1_xboole_0(A) % 58.70/58.87 => A = k1_xboole_0 ) ). % 58.70/58.87 % 58.70/58.87 fof(t7_boole,axiom, % 58.70/58.87 ! [A,B] : % 58.70/58.87 ~ ( r2_hidden(A,B) % 58.70/58.87 & v1_xboole_0(B) ) ). % 58.70/58.87 % 58.70/58.87 fof(t8_boole,axiom, % 58.70/58.87 ! [A,B] : % 58.70/58.87 ~ ( v1_xboole_0(A) % 58.70/58.87 & A != B % 58.70/58.87 & v1_xboole_0(B) ) ). % 58.70/58.87 % 58.70/58.87 %------------------------------------------------------------------------------ % 58.70/58.87 %------------------------------------------- % 58.70/58.87 % Proof found % 58.70/58.87 % SZS status Theorem for theBenchmark % 58.70/58.87 % SZS output start Proof % 58.70/58.87 %ClaNum:294(EqnAxiom:97) % 58.70/58.87 %VarNum:766(SingletonVarNum:239) % 58.70/58.87 %MaxLitNum:11 % 58.70/58.87 %MaxfuncDepth:2 % 58.70/58.87 %SharedTerms:30 % 58.70/58.87 %goalClause: 98 99 115 116 122 123 127 % 58.70/58.87 %singleGoalClaCount:7 % 58.70/58.87 [98]P1(a1) % 58.70/58.87 [99]P2(a1) % 58.70/58.87 [100]P2(a12) % 58.70/58.87 [101]P3(a19) % 58.70/58.87 [102]P3(a2) % 58.70/58.87 [103]P17(a19) % 58.70/58.87 [104]P17(a2) % 58.70/58.87 [105]P26(a19) % 58.70/58.87 [106]P26(a2) % 58.70/58.87 [107]P33(a19) % 58.70/58.87 [108]P33(a2) % 58.70/58.87 [109]P39(a19) % 58.70/58.87 [110]P39(a2) % 58.70/58.87 [111]P18(a19) % 58.70/58.87 [112]P4(a20) % 58.70/58.87 [113]P4(a4) % 58.70/58.87 [115]P27(a13,a1) % 58.70/58.87 [116]P5(a13,a1) % 58.70/58.87 [122]~P34(a1) % 58.70/58.87 [123]~P34(a13) % 58.70/58.87 [124]~P34(a4) % 58.70/58.87 [125]~P18(a2) % 58.70/58.87 [127]~P11(a1,a13) % 58.70/58.87 [117]P10(x1171,x1171) % 58.70/58.87 [114]P18(f5(x1141)) % 58.70/58.87 [118]P6(f21(x1181),x1181) % 58.70/58.87 [119]P6(f5(x1191),f25(x1191)) % 58.70/58.87 [126]~P18(f25(x1261)) % 58.70/58.87 [120]P9(f24(x1201,x1202),x1201,x1202) % 58.70/58.87 [121]P7(f22(x1211,x1212),x1211,x1212) % 58.70/58.87 [128]~P18(x1281)+E(x1281,a19) % 58.70/58.87 [129]~P17(x1291)+P3(x1291) % 58.70/58.87 [130]~P18(x1301)+P3(x1301) % 58.70/58.87 [131]~P26(x1311)+P17(x1311) % 58.70/58.87 [132]~P18(x1321)+P17(x1321) % 58.70/58.87 [133]~P33(x1331)+P26(x1331) % 58.70/58.87 [134]~P18(x1341)+P26(x1341) % 58.70/58.87 [135]~P39(x1351)+P33(x1351) % 58.70/58.87 [136]~P18(x1361)+P33(x1361) % 58.70/58.87 [137]~P18(x1371)+P39(x1371) % 58.70/58.87 [138]~P2(x1381)+P4(x1381) % 58.70/58.87 [140]~P2(x1401)+P3(f9(x1401)) % 58.70/58.87 [141]~P2(x1411)+P17(f9(x1411)) % 58.70/58.87 [142]~P2(x1421)+P26(f9(x1421)) % 58.70/58.87 [143]~P2(x1431)+P33(f9(x1431)) % 58.70/58.87 [144]~P2(x1441)+P39(f9(x1441)) % 58.70/58.87 [145]~P2(x1451)+P18(f9(x1451)) % 58.70/58.87 [146]P18(x1461)+~P18(f6(x1461)) % 58.70/58.87 [155]~P2(x1551)+P5(f3(x1551),x1551) % 58.70/58.87 [156]~P2(x1561)+P8(f23(x1561),x1561) % 58.70/58.87 [157]~P2(x1571)+P29(f9(x1571),x1571) % 58.70/58.87 [164]P18(x1641)+P6(f6(x1641),f25(x1641)) % 58.70/58.87 [232]~P2(x2321)+P6(f9(x2321),f25(f26(x2321))) % 58.70/58.87 [160]~P18(x1601)+~P12(x1602,x1601) % 58.70/58.87 [192]~P12(x1921,x1922)+P6(x1921,x1922) % 58.70/58.87 [231]~P12(x2312,x2311)+~P12(x2311,x2312) % 58.70/58.87 [213]~P10(x2131,x2132)+P6(x2131,f25(x2132)) % 58.70/58.87 [233]P10(x2331,x2332)+~P6(x2331,f25(x2332)) % 58.70/58.87 [283]~P7(x2831,x2832,x2833)+P9(x2831,x2832,x2833) % 58.70/58.87 [284]~P9(x2841,x2842,x2843)+P7(x2841,x2842,x2843) % 58.70/58.87 [279]P21(x2791)+~P6(x2791,f25(f27(x2792,x2793))) % 58.70/58.87 [289]~P9(x2891,x2892,x2893)+P6(x2891,f25(f27(x2892,x2893))) % 58.70/58.87 [149]~P1(x1491)+~P2(x1491)+P3(f14(x1491)) % 58.70/58.87 [150]~P1(x1501)+~P2(x1501)+P17(f14(x1501)) % 58.70/58.87 [151]~P1(x1511)+~P2(x1511)+P26(f14(x1511)) % 58.70/58.87 [152]~P1(x1521)+~P2(x1521)+P33(f14(x1521)) % 58.70/58.87 [153]~P1(x1531)+~P2(x1531)+P39(f14(x1531)) % 58.70/58.87 [154]~P1(x1541)+~P2(x1541)+P18(f14(x1541)) % 58.70/58.87 [158]~P4(x1581)+P34(x1581)+~P18(f26(x1581)) % 58.70/58.87 [159]~P4(x1591)+P34(x1591)+~P18(f11(x1591)) % 58.70/58.87 [182]~P1(x1821)+~P2(x1821)+P36(f7(x1821),x1821) % 58.70/58.87 [183]~P1(x1831)+~P2(x1831)+P36(f8(x1831),x1831) % 58.70/58.87 [184]~P1(x1841)+~P2(x1841)+P36(f14(x1841),x1841) % 58.70/58.87 [185]~P1(x1851)+~P2(x1851)+P41(f8(x1851),x1851) % 58.70/58.87 [186]~P1(x1861)+~P2(x1861)+P41(f14(x1861),x1861) % 58.70/58.87 [187]~P1(x1871)+~P2(x1871)+P41(f15(x1871),x1871) % 58.70/58.87 [188]~P1(x1881)+~P2(x1881)+P29(f14(x1881),x1881) % 58.70/58.87 [189]~P1(x1891)+~P2(x1891)+P37(f14(x1891),x1891) % 58.70/58.87 [234]~P4(x2341)+P34(x2341)+P6(f11(x2341),f25(f26(x2341))) % 58.70/58.87 [235]~P1(x2351)+~P2(x2351)+P6(f7(x2351),f25(f26(x2351))) % 58.70/58.87 [236]~P1(x2361)+~P2(x2361)+P6(f8(x2361),f25(f26(x2361))) % 58.70/58.87 [237]~P1(x2371)+~P2(x2371)+P6(f14(x2371),f25(f26(x2371))) % 58.70/58.87 [238]~P1(x2381)+~P2(x2381)+P6(f15(x2381),f25(f26(x2381))) % 58.70/58.87 [139]~P18(x1392)+~P18(x1391)+E(x1391,x1392) % 58.70/58.87 [165]~P5(x1651,x1652)+P2(x1651)+~P2(x1652) % 58.70/58.87 [166]~P8(x1661,x1662)+P2(x1661)+~P2(x1662) % 58.70/58.87 [167]~P6(x1671,x1672)+P24(x1671)+~P3(x1672) % 58.70/58.88 [168]~P6(x1681,x1682)+P24(x1681)+~P17(x1682) % 58.70/58.88 [169]~P6(x1691,x1692)+P24(x1691)+~P26(x1692) % 58.70/58.88 [170]~P6(x1701,x1702)+P24(x1701)+~P33(x1702) % 58.70/58.88 [171]~P6(x1711,x1712)+P24(x1711)+~P39(x1712) % 58.70/58.88 [172]~P6(x1721,x1722)+P25(x1721)+~P17(x1722) % 58.70/58.88 [173]~P6(x1731,x1732)+P25(x1731)+~P26(x1732) % 58.70/58.88 [174]~P6(x1741,x1742)+P25(x1741)+~P33(x1742) % 58.70/58.88 [175]~P6(x1751,x1752)+P25(x1751)+~P39(x1752) % 58.70/58.88 [176]~P6(x1761,x1762)+P20(x1761)+~P26(x1762) % 58.70/58.88 [177]~P6(x1771,x1772)+P20(x1771)+~P33(x1772) % 58.70/58.88 [178]~P6(x1781,x1782)+P20(x1781)+~P39(x1782) % 58.70/58.88 [179]~P6(x1791,x1792)+P13(x1791)+~P33(x1792) % 58.70/58.88 [180]~P6(x1801,x1802)+P13(x1801)+~P39(x1802) % 58.70/58.88 [181]~P6(x1811,x1812)+P40(x1811)+~P39(x1812) % 58.70/58.88 [212]~P6(x2122,x2121)+P18(x2121)+P12(x2122,x2121) % 58.70/58.88 [229]~P2(x2292)+~P8(x2291,x2292)+P5(x2291,x2292) % 58.70/58.88 [230]~P2(x2302)+~P5(x2301,x2302)+P8(x2301,x2302) % 58.70/58.88 [214]P3(x2141)+~P3(x2142)+~P6(x2141,f25(x2142)) % 58.70/58.88 [215]P3(x2151)+~P17(x2152)+~P6(x2151,f25(x2152)) % 58.70/58.88 [216]P3(x2161)+~P26(x2162)+~P6(x2161,f25(x2162)) % 58.70/58.88 [217]P3(x2171)+~P33(x2172)+~P6(x2171,f25(x2172)) % 58.70/58.88 [218]P3(x2181)+~P39(x2182)+~P6(x2181,f25(x2182)) % 58.70/58.88 [219]P17(x2191)+~P17(x2192)+~P6(x2191,f25(x2192)) % 58.70/58.88 [220]P17(x2201)+~P26(x2202)+~P6(x2201,f25(x2202)) % 58.70/58.88 [221]P17(x2211)+~P33(x2212)+~P6(x2211,f25(x2212)) % 58.70/58.88 [222]P17(x2221)+~P39(x2222)+~P6(x2221,f25(x2222)) % 58.70/58.88 [223]P26(x2231)+~P26(x2232)+~P6(x2231,f25(x2232)) % 58.70/58.88 [224]P26(x2241)+~P33(x2242)+~P6(x2241,f25(x2242)) % 58.70/58.88 [225]P26(x2251)+~P39(x2252)+~P6(x2251,f25(x2252)) % 58.70/58.88 [226]P33(x2261)+~P33(x2262)+~P6(x2261,f25(x2262)) % 58.70/58.88 [227]P33(x2271)+~P39(x2272)+~P6(x2271,f25(x2272)) % 58.70/58.88 [228]P39(x2281)+~P39(x2282)+~P6(x2281,f25(x2282)) % 58.70/58.88 [239]P18(x2391)+P18(x2392)+~P18(f27(x2392,x2391)) % 58.70/58.88 [244]~P18(x2441)+~P12(x2442,x2443)+~P6(x2443,f25(x2441)) % 58.70/58.88 [248]P6(x2481,x2482)+~P12(x2481,x2483)+~P6(x2483,f25(x2482)) % 58.70/58.88 [148]P28(x1481)+~P2(x1481)+~P35(x1481)+P34(x1481) % 58.70/58.88 [190]~P1(x1901)+~P2(x1901)+P34(x1901)+~P18(f10(x1901)) % 58.70/58.88 [191]~P1(x1911)+~P2(x1911)+P34(x1911)+~P18(f16(x1911)) % 58.70/58.88 [208]~P1(x2081)+~P2(x2081)+P34(x2081)+P36(f10(x2081),x2081) % 58.70/58.88 [209]~P1(x2091)+~P2(x2091)+P34(x2091)+P41(f10(x2091),x2091) % 58.70/58.88 [210]~P1(x2101)+~P2(x2101)+P34(x2101)+P41(f16(x2101),x2101) % 58.70/58.88 [240]~P1(x2401)+~P2(x2401)+P34(x2401)+P6(f10(x2401),f25(f26(x2401))) % 58.70/58.88 [241]~P1(x2411)+~P2(x2411)+P34(x2411)+P6(f16(x2411),f25(f26(x2411))) % 58.70/58.88 [211]~P2(x2112)+~P8(x2111,x2112)+P1(x2111)+~P1(x2112) % 58.70/58.88 [254]~P2(x2542)+~P18(x2541)+P29(x2541,x2542)+~P6(x2541,f25(f26(x2542))) % 58.70/58.88 [162]P28(x1621)+~P1(x1621)+~P2(x1621)+~P19(x1621)+P34(x1621) % 58.70/58.88 [255]~P1(x2552)+~P2(x2552)+~P18(x2551)+P36(x2551,x2552)+~P6(x2551,f25(f26(x2552))) % 58.70/58.88 [256]~P1(x2562)+~P2(x2562)+~P18(x2561)+P41(x2561,x2562)+~P6(x2561,f25(f26(x2562))) % 58.70/58.88 [257]~P1(x2572)+~P2(x2572)+~P18(x2571)+P37(x2571,x2572)+~P6(x2571,f25(f26(x2572))) % 58.70/58.88 [266]~P1(x2662)+~P2(x2662)+~P37(x2661,x2662)+P29(x2661,x2662)+~P6(x2661,f25(f26(x2662))) % 58.70/58.88 [193]P19(x1931)+~P1(x1931)+~P2(x1931)+~P28(x1931)+~P35(x1931)+P34(x1931) % 58.70/58.88 [195]P19(x1951)+~P1(x1951)+~P2(x1951)+~P28(x1951)+~P30(x1951)+P34(x1951) % 58.70/58.88 [198]P19(x1981)+~P1(x1981)+~P2(x1981)+~P28(x1981)+~P38(x1981)+P34(x1981) % 58.70/58.88 [199]P19(x1991)+~P1(x1991)+~P2(x1991)+~P35(x1991)+~P38(x1991)+P34(x1991) % 58.70/58.88 [202]P35(x2021)+~P1(x2021)+~P2(x2021)+~P28(x2021)+~P30(x2021)+P34(x2021) % 58.70/58.88 [203]P38(x2031)+~P1(x2031)+~P2(x2031)+~P28(x2031)+~P30(x2031)+P34(x2031) % 58.70/58.88 [204]P42(x2041)+~P1(x2041)+~P2(x2041)+~P28(x2041)+~P30(x2041)+P34(x2041) % 58.70/58.88 [205]P42(x2051)+~P1(x2051)+~P2(x2051)+~P28(x2051)+~P38(x2051)+P34(x2051) % 58.70/58.88 [206]P43(x2061)+~P1(x2061)+~P2(x2061)+~P28(x2061)+~P30(x2061)+P34(x2061) % 58.70/58.88 [207]P43(x2071)+~P1(x2071)+~P2(x2071)+~P28(x2071)+~P38(x2071)+P34(x2071) % 58.70/58.88 [246]P28(x2462)+~P2(x2461)+~P27(x2462,x2461)+~P8(x2462,x2461)+P34(x2461)+P34(x2462) % 58.70/58.88 [253]~P1(x2531)+~P2(x2531)+~P27(x2532,x2531)+~P8(x2532,x2531)+P34(x2531)+P22(x2532,x2531) % 58.70/58.88 [273]~P2(x2732)+~P36(x2731,x2732)+~P37(x2731,x2732)+P3(x2731)+~P1(x2732)+~P6(x2731,f25(f26(x2732))) % 58.70/58.88 [274]~P2(x2742)+~P36(x2741,x2742)+~P37(x2741,x2742)+P17(x2741)+~P1(x2742)+~P6(x2741,f25(f26(x2742))) % 58.70/58.88 [275]~P2(x2752)+~P36(x2751,x2752)+~P37(x2751,x2752)+P26(x2751)+~P1(x2752)+~P6(x2751,f25(f26(x2752))) % 58.70/58.88 [276]~P2(x2762)+~P36(x2761,x2762)+~P37(x2761,x2762)+P33(x2761)+~P1(x2762)+~P6(x2761,f25(f26(x2762))) % 58.70/58.88 [277]~P2(x2772)+~P36(x2771,x2772)+~P37(x2771,x2772)+P39(x2771)+~P1(x2772)+~P6(x2771,f25(f26(x2772))) % 58.70/58.88 [278]~P2(x2782)+~P36(x2781,x2782)+~P37(x2781,x2782)+P18(x2781)+~P1(x2782)+~P6(x2781,f25(f26(x2782))) % 58.70/58.88 [280]~P1(x2802)+~P2(x2802)+~P36(x2801,x2802)+~P37(x2801,x2802)+P41(x2801,x2802)+~P6(x2801,f25(f26(x2802))) % 58.70/58.88 [282]~P1(x2822)+~P2(x2822)+~P41(x2821,x2822)+~P29(x2821,x2822)+P37(x2821,x2822)+~P6(x2821,f25(f26(x2822))) % 58.70/58.88 [242]P28(x2422)+~P1(x2421)+~P2(x2421)+~P28(x2421)+~P8(x2422,x2421)+P34(x2421)+P34(x2422) % 58.70/58.88 [269]~P1(x2691)+~P2(x2691)+~P8(x2692,x2691)+~P31(x2692,x2691)+~P14(x2692,x2691)+P34(x2691)+~P27(x2692,x2691) % 58.70/58.88 [272]~P1(x2721)+~P2(x2721)+~P8(x2722,x2721)+~P31(x2722,x2721)+~P23(x2722,x2721)+P34(x2721)+~P27(x2722,x2721) % 58.70/58.88 [264]~P1(x2642)+~P2(x2642)+~P11(x2642,x2641)+~P8(x2641,x2642)+P34(x2641)+P34(x2642)+P15(f18(x2642,x2641)) % 58.70/58.88 [265]~P1(x2652)+~P2(x2652)+~P27(x2651,x2652)+~P5(x2651,x2652)+P34(x2651)+P34(x2652)+P15(f17(x2652,x2651)) % 58.70/58.88 [285]~P1(x2852)+~P2(x2852)+~P11(x2852,x2851)+~P8(x2851,x2852)+P34(x2851)+P34(x2852)+P44(f18(x2852,x2851),x2852,x2851) % 58.70/58.88 [286]~P1(x2862)+~P2(x2862)+~P27(x2861,x2862)+~P5(x2861,x2862)+P34(x2861)+P34(x2862)+P44(f17(x2862,x2861),x2862,x2861) % 58.70/58.88 [287]~P1(x2872)+~P2(x2872)+~P11(x2872,x2871)+~P8(x2871,x2872)+P34(x2871)+P34(x2872)+P32(f18(x2872,x2871),x2872,x2871) % 58.70/58.88 [288]~P1(x2882)+~P2(x2882)+~P27(x2881,x2882)+~P5(x2881,x2882)+P34(x2881)+P34(x2882)+P32(f17(x2882,x2881),x2882,x2881) % 58.70/58.88 [290]~P1(x2902)+~P2(x2902)+~P11(x2902,x2901)+~P8(x2901,x2902)+P34(x2901)+P34(x2902)+P16(f18(x2902,x2901),f26(x2902),f26(x2901)) % 58.70/58.88 [291]~P1(x2912)+~P2(x2912)+~P27(x2911,x2912)+~P5(x2911,x2912)+P34(x2911)+P34(x2912)+P16(f17(x2912,x2911),f26(x2912),f26(x2911)) % 58.70/58.88 [292]~P1(x2922)+~P2(x2922)+~P11(x2922,x2921)+~P8(x2921,x2922)+P34(x2921)+P34(x2922)+P9(f18(x2922,x2921),f26(x2922),f26(x2921)) % 58.70/58.88 [293]~P1(x2932)+~P2(x2932)+~P27(x2931,x2932)+~P5(x2931,x2932)+P34(x2931)+P34(x2932)+P9(f17(x2932,x2931),f26(x2932),f26(x2931)) % 58.70/58.88 [250]P28(x2501)+P31(x2502,x2501)+~P1(x2501)+~P2(x2501)+~P28(x2502)+~P8(x2502,x2501)+P34(x2501)+P34(x2502) % 58.70/58.88 [251]P28(x2511)+P31(x2512,x2511)+~P1(x2511)+~P2(x2511)+~P35(x2512)+~P8(x2512,x2511)+P34(x2511)+P34(x2512) % 58.70/58.88 [294]P11(x2942,x2941)+~P1(x2942)+~P2(x2942)+~P8(x2941,x2942)+~P44(x2943,x2942,x2941)+~P32(x2943,x2942,x2941)+P34(x2941)+P34(x2942)+~P15(x2943)+~P16(x2943,f26(x2942),f26(x2941))+~P9(x2943,f26(x2942),f26(x2941)) % 58.70/58.88 %EqnAxiom % 58.70/58.88 [1]E(x11,x11) % 58.70/58.88 [2]E(x22,x21)+~E(x21,x22) % 58.70/58.88 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.70/58.88 [4]~E(x41,x42)+E(f5(x41),f5(x42)) % 58.70/58.88 [5]~E(x51,x52)+E(f21(x51),f21(x52)) % 58.70/58.88 [6]~E(x61,x62)+E(f26(x61),f26(x62)) % 58.70/58.88 [7]~E(x71,x72)+E(f25(x71),f25(x72)) % 58.70/58.88 [8]~E(x81,x82)+E(f24(x81,x83),f24(x82,x83)) % 58.70/58.88 [9]~E(x91,x92)+E(f24(x93,x91),f24(x93,x92)) % 58.70/58.88 [10]~E(x101,x102)+E(f22(x101,x103),f22(x102,x103)) % 58.70/58.88 [11]~E(x111,x112)+E(f22(x113,x111),f22(x113,x112)) % 58.70/58.88 [12]~E(x121,x122)+E(f27(x121,x123),f27(x122,x123)) % 58.70/58.88 [13]~E(x131,x132)+E(f27(x133,x131),f27(x133,x132)) % 58.70/58.88 [14]~E(x141,x142)+E(f9(x141),f9(x142)) % 58.70/58.88 [15]~E(x151,x152)+E(f11(x151),f11(x152)) % 58.70/58.88 [16]~E(x161,x162)+E(f17(x161,x163),f17(x162,x163)) % 58.70/58.88 [17]~E(x171,x172)+E(f17(x173,x171),f17(x173,x172)) % 58.70/58.88 [18]~E(x181,x182)+E(f7(x181),f7(x182)) % 58.70/58.88 [19]~E(x191,x192)+E(f18(x191,x193),f18(x192,x193)) % 58.70/58.88 [20]~E(x201,x202)+E(f18(x203,x201),f18(x203,x202)) % 58.70/58.88 [21]~E(x211,x212)+E(f8(x211),f8(x212)) % 58.70/58.88 [22]~E(x221,x222)+E(f6(x221),f6(x222)) % 58.70/58.88 [23]~E(x231,x232)+E(f14(x231),f14(x232)) % 58.70/58.88 [24]~E(x241,x242)+E(f10(x241),f10(x242)) % 58.70/58.88 [25]~E(x251,x252)+E(f15(x251),f15(x252)) % 58.70/58.88 [26]~E(x261,x262)+E(f16(x261),f16(x262)) % 58.70/58.88 [27]~E(x271,x272)+E(f23(x271),f23(x272)) % 58.70/58.88 [28]~E(x281,x282)+E(f3(x281),f3(x282)) % 58.70/58.88 [29]~P1(x291)+P1(x292)+~E(x291,x292) % 58.70/58.88 [30]~P2(x301)+P2(x302)+~E(x301,x302) % 58.70/58.88 [31]~P18(x311)+P18(x312)+~E(x311,x312) % 58.70/58.88 [32]~P3(x321)+P3(x322)+~E(x321,x322) % 58.70/58.88 [33]P41(x332,x333)+~E(x331,x332)+~P41(x331,x333) % 58.70/58.88 [34]P41(x343,x342)+~E(x341,x342)+~P41(x343,x341) % 58.70/58.88 [35]~P17(x351)+P17(x352)+~E(x351,x352) % 58.70/58.88 [36]P37(x362,x363)+~E(x361,x362)+~P37(x361,x363) % 58.70/58.88 [37]P37(x373,x372)+~E(x371,x372)+~P37(x373,x371) % 58.70/58.88 [38]~P26(x381)+P26(x382)+~E(x381,x382) % 58.70/58.88 [39]~P34(x391)+P34(x392)+~E(x391,x392) % 58.70/58.88 [40]~P33(x401)+P33(x402)+~E(x401,x402) % 58.70/58.88 [41]P6(x412,x413)+~E(x411,x412)+~P6(x411,x413) % 58.70/58.88 [42]P6(x423,x422)+~E(x421,x422)+~P6(x423,x421) % 58.70/58.88 [43]~P39(x431)+P39(x432)+~E(x431,x432) % 58.70/58.88 [44]~P30(x441)+P30(x442)+~E(x441,x442) % 58.70/58.88 [45]P29(x452,x453)+~E(x451,x452)+~P29(x451,x453) % 58.70/58.88 [46]P29(x463,x462)+~E(x461,x462)+~P29(x463,x461) % 58.70/58.88 [47]~P4(x471)+P4(x472)+~E(x471,x472) % 58.70/58.88 [48]~P19(x481)+P19(x482)+~E(x481,x482) % 58.70/58.88 [49]P14(x492,x493)+~E(x491,x492)+~P14(x491,x493) % 58.70/58.88 [50]P14(x503,x502)+~E(x501,x502)+~P14(x503,x501) % 58.70/58.88 [51]P27(x512,x513)+~E(x511,x512)+~P27(x511,x513) % 58.70/58.88 [52]P27(x523,x522)+~E(x521,x522)+~P27(x523,x521) % 58.70/58.88 [53]P5(x532,x533)+~E(x531,x532)+~P5(x531,x533) % 58.70/58.88 [54]P5(x543,x542)+~E(x541,x542)+~P5(x543,x541) % 58.70/58.88 [55]P10(x552,x553)+~E(x551,x552)+~P10(x551,x553) % 58.70/58.88 [56]P10(x563,x562)+~E(x561,x562)+~P10(x563,x561) % 58.70/58.88 [57]~P28(x571)+P28(x572)+~E(x571,x572) % 58.70/58.88 [58]P23(x582,x583)+~E(x581,x582)+~P23(x581,x583) % 58.70/58.88 [59]P23(x593,x592)+~E(x591,x592)+~P23(x593,x591) % 58.70/58.88 [60]P9(x602,x603,x604)+~E(x601,x602)+~P9(x601,x603,x604) % 58.70/58.88 [61]P9(x613,x612,x614)+~E(x611,x612)+~P9(x613,x611,x614) % 58.70/58.88 [62]P9(x623,x624,x622)+~E(x621,x622)+~P9(x623,x624,x621) % 58.70/58.88 [63]P7(x632,x633,x634)+~E(x631,x632)+~P7(x631,x633,x634) % 58.70/58.88 [64]P7(x643,x642,x644)+~E(x641,x642)+~P7(x643,x641,x644) % 58.70/58.88 [65]P7(x653,x654,x652)+~E(x651,x652)+~P7(x653,x654,x651) % 58.70/58.88 [66]P8(x662,x663)+~E(x661,x662)+~P8(x661,x663) % 58.70/58.88 [67]P8(x673,x672)+~E(x671,x672)+~P8(x673,x671) % 58.70/58.88 [68]~P35(x681)+P35(x682)+~E(x681,x682) % 58.70/58.88 [69]~P15(x691)+P15(x692)+~E(x691,x692) % 58.70/58.88 [70]P36(x702,x703)+~E(x701,x702)+~P36(x701,x703) % 58.70/58.88 [71]P36(x713,x712)+~E(x711,x712)+~P36(x713,x711) % 58.70/58.88 [72]~P43(x721)+P43(x722)+~E(x721,x722) % 58.70/58.88 [73]P11(x732,x733)+~E(x731,x732)+~P11(x731,x733) % 58.70/58.88 [74]P11(x743,x742)+~E(x741,x742)+~P11(x743,x741) % 58.70/58.88 [75]P31(x752,x753)+~E(x751,x752)+~P31(x751,x753) % 58.70/58.88 [76]P31(x763,x762)+~E(x761,x762)+~P31(x763,x761) % 58.70/58.88 [77]~P25(x771)+P25(x772)+~E(x771,x772) % 58.70/58.88 [78]~P21(x781)+P21(x782)+~E(x781,x782) % 58.70/58.88 [79]~P38(x791)+P38(x792)+~E(x791,x792) % 58.70/58.88 [80]P12(x802,x803)+~E(x801,x802)+~P12(x801,x803) % 58.70/58.88 [81]P12(x813,x812)+~E(x811,x812)+~P12(x813,x811) % 58.70/58.88 [82]P22(x822,x823)+~E(x821,x822)+~P22(x821,x823) % 58.70/58.88 [83]P22(x833,x832)+~E(x831,x832)+~P22(x833,x831) % 58.70/58.88 [84]P16(x842,x843,x844)+~E(x841,x842)+~P16(x841,x843,x844) % 58.70/58.88 [85]P16(x853,x852,x854)+~E(x851,x852)+~P16(x853,x851,x854) % 58.70/58.88 [86]P16(x863,x864,x862)+~E(x861,x862)+~P16(x863,x864,x861) % 58.70/58.88 [87]P44(x872,x873,x874)+~E(x871,x872)+~P44(x871,x873,x874) % 58.70/58.88 [88]P44(x883,x882,x884)+~E(x881,x882)+~P44(x883,x881,x884) % 58.70/58.88 [89]P44(x893,x894,x892)+~E(x891,x892)+~P44(x893,x894,x891) % 58.70/58.88 [90]~P20(x901)+P20(x902)+~E(x901,x902) % 58.70/58.88 [91]P32(x912,x913,x914)+~E(x911,x912)+~P32(x911,x913,x914) % 58.70/58.88 [92]P32(x923,x922,x924)+~E(x921,x922)+~P32(x923,x921,x924) % 58.70/58.88 [93]P32(x933,x934,x932)+~E(x931,x932)+~P32(x933,x934,x931) % 58.70/58.88 [94]~P13(x941)+P13(x942)+~E(x941,x942) % 58.70/58.88 [95]~P24(x951)+P24(x952)+~E(x951,x952) % 58.70/58.88 [96]~P40(x961)+P40(x962)+~E(x961,x962) % 58.70/58.88 [97]~P42(x971)+P42(x972)+~E(x971,x972) % 58.70/58.88 % 58.70/58.88 %------------------------------------------- % 58.70/58.88 cnf(295,plain, % 58.70/58.88 (~P12(x2951,a19)), % 58.70/58.88 inference(scs_inference,[],[111,160])). % 58.70/58.88 cnf(297,plain, % 58.70/58.88 (P10(f21(f25(x2971)),x2971)), % 58.70/58.88 inference(scs_inference,[],[118,111,160,233])). % 58.70/58.88 cnf(298,plain, % 58.70/58.88 (P6(f21(x2981),x2981)), % 58.70/58.88 inference(rename_variables,[],[118])). % 58.70/58.88 cnf(300,plain, % 58.70/58.88 (P21(f5(f27(x3001,x3002)))), % 58.70/58.88 inference(scs_inference,[],[118,119,111,160,233,279])). % 58.70/58.88 cnf(301,plain, % 58.70/58.88 (P6(f5(x3011),f25(x3011))), % 58.70/58.88 inference(rename_variables,[],[119])). % 58.70/58.88 cnf(303,plain, % 58.70/58.88 (P12(f21(a2),a2)), % 58.70/58.88 inference(scs_inference,[],[118,298,119,111,125,160,233,279,212])). % 58.70/58.88 cnf(304,plain, % 58.70/58.88 (P6(f21(x3041),x3041)), % 58.70/58.88 inference(rename_variables,[],[118])). % 58.70/58.88 cnf(307,plain, % 58.70/58.88 (P6(f21(x3071),x3071)), % 58.70/58.88 inference(rename_variables,[],[118])). % 58.70/58.88 cnf(310,plain, % 58.70/58.88 (P6(f5(x3101),f25(x3101))), % 58.70/58.88 inference(rename_variables,[],[119])). % 58.70/58.88 cnf(313,plain, % 58.70/58.88 (P6(f21(x3131),x3131)), % 58.70/58.88 inference(rename_variables,[],[118])). % 58.70/58.88 cnf(316,plain, % 58.70/58.88 (P6(f5(x3161),f25(x3161))), % 58.70/58.88 inference(rename_variables,[],[119])). % 58.70/58.88 cnf(319,plain, % 58.70/58.88 (P6(f21(x3191),x3191)), % 58.70/58.88 inference(rename_variables,[],[118])). % 58.70/58.88 cnf(321,plain, % 58.70/58.88 (P26(f5(a19))), % 58.70/58.88 inference(scs_inference,[],[118,298,304,307,313,119,301,310,316,111,125,101,103,105,107,160,233,279,212,214,215,219,220,223,224])). % 58.70/58.88 cnf(322,plain, % 58.70/58.88 (P6(f5(x3221),f25(x3221))), % 58.70/58.88 inference(rename_variables,[],[119])). % 58.70/58.88 cnf(325,plain, % 58.70/58.88 (P6(f21(x3251),x3251)), % 58.70/58.88 inference(rename_variables,[],[118])). % 58.70/58.88 cnf(328,plain, % 58.70/58.88 (P6(f5(x3281),f25(x3281))), % 58.70/58.88 inference(rename_variables,[],[119])). % 58.70/58.88 cnf(331,plain, % 58.70/58.88 (P6(f21(x3311),x3311)), % 58.70/58.88 inference(rename_variables,[],[118])). % 58.70/58.88 cnf(333,plain, % 58.70/58.88 (~P12(x3331,f21(f25(a19)))), % 58.70/58.88 inference(scs_inference,[],[118,298,304,307,313,319,325,331,119,301,310,316,322,111,125,101,103,105,107,109,160,233,279,212,214,215,219,220,223,224,226,227,228,244])). % 58.70/58.88 cnf(336,plain, % 58.70/58.88 (~E(a2,a19)), % 58.70/58.88 inference(scs_inference,[],[118,298,304,307,313,319,325,331,119,301,310,316,322,111,125,101,103,105,107,109,160,233,279,212,214,215,219,220,223,224,226,227,228,244,81])). % 58.70/58.88 cnf(337,plain, % 58.70/58.88 (P29(f5(f26(a1)),a1)), % 58.70/58.88 inference(scs_inference,[],[99,118,298,304,307,313,319,325,331,119,301,310,316,322,328,111,125,114,101,103,105,107,109,160,233,279,212,214,215,219,220,223,224,226,227,228,244,81,254])). % 58.70/58.88 cnf(338,plain, % 58.70/58.88 (P6(f5(x3381),f25(x3381))), % 58.70/58.88 inference(rename_variables,[],[119])). % 58.70/58.88 cnf(339,plain, % 58.70/58.88 (P18(f5(x3391))), % 58.70/58.88 inference(rename_variables,[],[114])). % 58.70/58.88 cnf(342,plain, % 58.70/58.88 (P6(f5(x3421),f25(x3421))), % 58.70/58.88 inference(rename_variables,[],[119])). % 58.70/58.88 cnf(343,plain, % 58.70/58.88 (P18(f5(x3431))), % 58.70/58.88 inference(rename_variables,[],[114])). % 58.70/58.88 cnf(345,plain, % 58.70/58.88 (P41(f5(f26(a1)),a1)), % 58.70/58.88 inference(scs_inference,[],[98,99,118,298,304,307,313,319,325,331,119,301,310,316,322,328,338,342,111,125,114,339,343,101,103,105,107,109,160,233,279,212,214,215,219,220,223,224,226,227,228,244,81,254,255,256])). % 58.70/58.88 cnf(346,plain, % 58.70/58.88 (P6(f5(x3461),f25(x3461))), % 58.70/58.88 inference(rename_variables,[],[119])). % 58.70/58.88 cnf(347,plain, % 58.70/58.88 (P18(f5(x3471))), % 58.70/58.88 inference(rename_variables,[],[114])). % 58.70/58.88 cnf(349,plain, % 58.70/58.88 (P37(f5(f26(a1)),a1)), % 58.70/58.88 inference(scs_inference,[],[98,99,118,298,304,307,313,319,325,331,119,301,310,316,322,328,338,342,346,111,125,114,339,343,347,101,103,105,107,109,160,233,279,212,214,215,219,220,223,224,226,227,228,244,81,254,255,256,257])). % 58.70/58.88 cnf(383,plain, % 58.70/58.88 (P10(f5(x3831),x3831)), % 58.70/58.88 inference(scs_inference,[],[119,233])). % 58.70/58.88 cnf(385,plain, % 58.70/58.88 (~P12(x3851,f5(x3852))), % 58.70/58.88 inference(scs_inference,[],[119,114,233,160])). % 58.70/58.88 cnf(387,plain, % 58.70/58.88 (P12(f21(f25(x3871)),f25(x3871))), % 58.70/58.88 inference(scs_inference,[],[126,118,119,114,233,160,212])). % 58.70/58.88 cnf(388,plain, % 58.70/58.88 (P6(f21(x3881),x3881)), % 58.70/58.88 inference(rename_variables,[],[118])). % 58.70/58.88 cnf(398,plain, % 58.70/58.88 (P6(f21(x3981),x3982)+~E(x3981,x3982)), % 58.70/58.88 inference(scs_inference,[],[345,349,333,303,126,118,388,119,114,233,160,212,81,231,34,36,37,41,42])). % 58.70/58.88 cnf(413,plain, % 58.70/58.88 (P9(f24(x4131,x4132),x4133,x4132)+~E(x4131,x4133)), % 58.70/58.88 inference(scs_inference,[],[337,119,387,385,120,126,212,81,46,60,61])). % 58.70/58.88 cnf(414,plain, % 58.70/58.88 (P9(f24(x4141,x4142),x4141,x4143)+~E(x4142,x4143)), % 58.70/58.88 inference(scs_inference,[],[337,119,387,385,120,126,212,81,46,60,61,62])). % 58.70/58.88 cnf(426,plain, % 58.70/58.88 (P10(f5(x4261),x4262)+~E(x4261,x4262)), % 58.70/58.88 inference(scs_inference,[],[387,383,295,81,55,56])). % 58.70/58.88 cnf(428,plain, % 58.70/58.88 (P7(f22(x4281,x4282),x4283,x4282)+~E(x4281,x4283)), % 58.70/58.88 inference(scs_inference,[],[387,383,295,121,81,55,56,63,64])). % 58.70/58.88 cnf(429,plain, % 58.70/58.88 (P7(f22(x4291,x4292),x4291,x4293)+~E(x4292,x4293)), % 58.70/58.89 inference(scs_inference,[],[387,383,295,121,81,55,56,63,64,65])). % 58.70/58.89 cnf(457,plain, % 58.70/58.89 (P10(x4571,x4572)+~E(x4572,x4571)), % 58.70/58.89 inference(scs_inference,[],[303,297,117,56,80,55])). % 58.70/58.89 cnf(470,plain, % 58.70/58.89 (P10(x4701,x4702)+~E(x4701,x4702)), % 58.70/58.89 inference(scs_inference,[],[117,56])). % 58.70/58.89 cnf(639,plain, % 58.70/58.89 (P17(f5(x6391))), % 58.70/58.89 inference(scs_inference,[],[114,134,131])). % 58.70/58.89 cnf(728,plain, % 58.70/58.89 (P33(f5(x7281))), % 58.70/58.89 inference(scs_inference,[],[114,137,135])). % 58.70/58.89 cnf(868,plain, % 58.70/58.89 (E(f9(a1),a19)), % 58.70/58.89 inference(scs_inference,[],[99,128,145])). % 58.70/58.89 cnf(870,plain, % 58.70/58.89 (P6(f21(f9(a1)),a19)), % 58.70/58.89 inference(scs_inference,[],[868,398])). % 58.70/58.89 cnf(876,plain, % 58.70/58.89 (P10(a19,f9(a1))), % 58.70/58.89 inference(scs_inference,[],[868,398,413,414,426,428,429,457])). % 58.70/58.89 cnf(878,plain, % 58.70/58.89 (E(a19,f9(a1))), % 58.70/58.89 inference(scs_inference,[],[868,398,413,414,426,428,429,457,470,2])). % 58.70/58.89 cnf(879,plain, % 58.70/58.89 (P18(f9(a1))), % 58.70/58.89 inference(scs_inference,[],[111,868,398,413,414,426,428,429,457,470,2,31])). % 58.70/58.89 cnf(884,plain, % 58.70/58.89 (P39(f9(a1))), % 58.70/58.89 inference(scs_inference,[],[111,868,101,103,105,107,109,398,413,414,426,428,429,457,470,2,31,32,35,38,40,43])). % 58.70/58.89 cnf(886,plain, % 58.70/58.89 (P9(f24(f9(a1),f9(a1)),a19,a19)), % 58.70/58.89 inference(scs_inference,[],[111,868,336,101,103,105,107,109,398,413,414,426,428,429,457,470,2,31,32,35,38,40,43,3,62])). % 58.70/58.89 cnf(896,plain, % 58.70/58.89 (P9(f24(x8961,a19),x8961,f9(a1))), % 58.70/58.89 inference(scs_inference,[],[878,414])). % 58.70/58.89 cnf(898,plain, % 58.70/58.89 (P7(f22(x8981,a19),x8981,f9(a1))), % 58.70/58.89 inference(scs_inference,[],[878,414,426,429])). % 58.70/58.89 cnf(901,plain, % 58.70/58.89 (P6(f21(a19),f9(a1))), % 58.70/58.89 inference(scs_inference,[],[878,414,426,429,413,428,398])). % 58.70/58.89 cnf(1222,plain, % 58.70/58.89 (~P18(f6(a2))), % 58.70/58.89 inference(scs_inference,[],[303,146,160])). % 58.70/58.89 cnf(1229,plain, % 58.70/58.89 (~E(f6(a2),f5(x12291))), % 58.70/58.89 inference(scs_inference,[],[118,1222,385,212,231,80,81])). % 58.70/58.89 cnf(3537,plain, % 58.70/58.89 (P6(f5(f9(a1)),f25(a19))), % 58.70/58.89 inference(scs_inference,[],[868,213,426])). % 58.70/58.89 cnf(3845,plain, % 58.70/58.89 (P12(f5(f9(a1)),f25(a19))), % 58.70/58.89 inference(scs_inference,[],[3537,126,212])). % 58.70/58.89 cnf(4520,plain, % 58.70/58.89 (P39(f5(a2))), % 58.70/58.89 inference(scs_inference,[],[110,119,228])). % 58.70/58.89 cnf(4778,plain, % 58.70/58.89 (P6(f22(x47781,x47782),f25(f27(x47781,x47782)))), % 58.70/58.89 inference(scs_inference,[],[121,283,289])). % 58.70/58.89 cnf(6489,plain, % 58.70/58.89 (P6(f21(x64891),x64891)), % 58.70/58.89 inference(rename_variables,[],[118])). % 58.70/58.89 cnf(6492,plain, % 58.70/58.89 (P6(f21(x64921),x64921)), % 58.70/58.89 inference(rename_variables,[],[118])). % 58.70/58.89 cnf(6549,plain, % 58.70/58.89 (P6(f21(x65491),x65491)), % 58.70/58.89 inference(rename_variables,[],[118])). % 58.70/58.89 cnf(6552,plain, % 58.70/58.89 (P6(f21(x65521),x65521)), % 58.70/58.89 inference(rename_variables,[],[118])). % 58.70/58.89 cnf(6555,plain, % 58.70/58.89 (P6(f21(x65551),x65551)), % 58.70/58.89 inference(rename_variables,[],[118])). % 58.70/58.89 cnf(6566,plain, % 58.70/58.89 (P6(f21(x65661),x65661)), % 58.70/58.89 inference(rename_variables,[],[118])). % 58.70/58.89 cnf(6571,plain, % 58.70/58.89 (P6(f21(x65711),x65711)), % 58.70/58.89 inference(rename_variables,[],[118])). % 58.70/58.89 cnf(6619,plain, % 58.70/58.89 ($false), % 58.70/58.89 inference(scs_inference,[],[98,127,113,124,321,884,4520,300,1229,876,3845,108,1222,901,870,898,896,886,639,879,123,103,728,126,107,114,4778,116,878,115,122,99,118,6489,6492,6549,6552,6555,6566,6571,100,129,133,137,138,140,141,142,143,144,145,146,155,156,157,213,283,284,164,4,5,6,7,14,15,18,21,22,23,24,25,26,27,28,232,289,8,9,10,11,12,13,16,17,19,20,128,2,169,171,149,150,151,152,153,154,158,159,229,182,183,184,185,186,187,188,189,239,234,235,236,237,238,180,166,168,177,170,173,175,172,179,165,230,174,181,176,3,178,96,31,78,244,212,190,191,208,209,210,240,241,211,255,256,257,253,265,286,288,291,293,294]), % 58.70/58.89 ['proof']). % 58.70/58.89 % SZS output end Proof % 58.70/58.89 % Total time :58.160000s %------------------------------------------------------------------------------