%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : TOP027+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 : 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 21:15:08 EDT 2024 % Result : Theorem 0.73s 0.76s % Output : CNFRefutation 0.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.10 % Problem : TOP027+1 : TPTP v8.2.0. Released v3.4.0. % 0.02/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.30 % Computer : n019.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Tue Jun 18 11:17:08 EDT 2024 % 0.09/0.30 % CPUTime : % 0.15/0.56 start to proof:theBenchmark % 0.51/0.73 %------------------------------------------- % 0.51/0.73 % File :CSE---1.7 % 0.51/0.73 % Problem :theBenchmark % 0.51/0.73 % Transform :cnf % 0.51/0.73 % Format :tptp:raw % 0.51/0.73 % Command :java -jar mcs_scs.jar %d %s % 0.51/0.73 % 0.51/0.73 % Result :Theorem 0.110000s % 0.51/0.73 % Output :CNFRefutation 0.110000s % 0.51/0.73 %------------------------------------------- % 0.51/0.74 %------------------------------------------------------------------------------ % 0.51/0.74 % File : TOP027+1 : TPTP v8.2.0. Released v3.4.0. % 0.51/0.74 % Domain : Topology % 0.51/0.74 % Problem : Maximal Kolmogorov Subspaces of a Topological Space T08 % 0.51/0.74 % Version : [Urb08] axioms : Especial. % 0.51/0.74 % English : % 0.51/0.74 % 0.51/0.74 % Refs : [Kar96] Karno (1996), Maximal Kolmogorov Subspaces of a Topolo % 0.51/0.74 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 0.51/0.74 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 0.51/0.74 % Source : [Urb08] % 0.51/0.74 % Names : t8_tsp_2 [Urb08] % 0.51/0.74 % 0.51/0.74 % Status : Theorem % 0.51/0.74 % Rating : 0.25 v8.2.0, 0.22 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.07 v7.3.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.08 v6.2.0, 0.24 v6.1.0, 0.23 v6.0.0, 0.22 v5.5.0, 0.19 v5.4.0, 0.29 v5.3.0, 0.33 v5.2.0, 0.05 v5.1.0, 0.14 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.1, 0.30 v4.0.0, 0.33 v3.7.0, 0.25 v3.5.0, 0.26 v3.4.0 % 0.51/0.74 % Syntax : Number of formulae : 79 ( 14 unt; 0 def) % 0.51/0.74 % Number of atoms : 306 ( 10 equ) % 0.51/0.74 % Maximal formula atoms : 15 ( 3 avg) % 0.51/0.74 % Number of connectives : 248 ( 21 ~; 1 |; 139 &) % 0.51/0.74 % ( 1 <=>; 86 =>; 0 <=; 0 <~>) % 0.51/0.74 % Maximal formula depth : 15 ( 5 avg) % 0.51/0.74 % Maximal term depth : 4 ( 1 avg) % 0.51/0.74 % Number of predicates : 25 ( 23 usr; 1 prp; 0-2 aty) % 0.51/0.74 % Number of functors : 7 ( 7 usr; 1 con; 0-3 aty) % 0.51/0.74 % Number of variables : 138 ( 123 !; 15 ?) % 0.51/0.74 % SPC : FOF_THM_RFO_SEQ % 0.51/0.74 % 0.51/0.74 % Comments : Normal version: includes the axioms (which may be theorems from % 0.51/0.74 % other articles) and background that are possibly necessary. % 0.51/0.74 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 0.51/0.74 % : The problem encoding is based on set theory. % 0.51/0.74 %------------------------------------------------------------------------------ % 0.51/0.74 fof(t8_tsp_2,conjecture, % 0.51/0.74 ! [A] : % 0.51/0.74 ( ( ~ v3_struct_0(A) % 0.51/0.74 & v2_pre_topc(A) % 0.51/0.74 & l1_pre_topc(A) ) % 0.51/0.74 => ! [B] : % 0.51/0.74 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.74 => ( v1_tsp_2(B,A) % 0.51/0.74 => ! [C] : % 0.51/0.74 ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.74 => k1_tops_1(A,C) = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,k1_tops_1(A,C))) ) ) ) ) ). % 0.51/0.74 % 0.51/0.74 fof(antisymmetry_r2_hidden,axiom, % 0.51/0.74 ! [A,B] : % 0.51/0.74 ( r2_hidden(A,B) % 0.51/0.74 => ~ r2_hidden(B,A) ) ). % 0.51/0.74 % 0.51/0.74 fof(dt_k1_xboole_0,axiom, % 0.51/0.74 $true ). % 0.51/0.74 % 0.51/0.74 fof(cc10_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v1_membered(A) % 0.51/0.74 => ! [B] : % 0.51/0.74 ( m1_subset_1(B,A) % 0.51/0.74 => v1_xcmplx_0(B) ) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc11_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v2_membered(A) % 0.51/0.74 => ! [B] : % 0.51/0.74 ( m1_subset_1(B,A) % 0.51/0.74 => ( v1_xcmplx_0(B) % 0.51/0.74 & v1_xreal_0(B) ) ) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc12_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v3_membered(A) % 0.51/0.74 => ! [B] : % 0.51/0.74 ( m1_subset_1(B,A) % 0.51/0.74 => ( v1_xcmplx_0(B) % 0.51/0.74 & v1_xreal_0(B) % 0.51/0.74 & v1_rat_1(B) ) ) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc13_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v4_membered(A) % 0.51/0.74 => ! [B] : % 0.51/0.74 ( m1_subset_1(B,A) % 0.51/0.74 => ( v1_xcmplx_0(B) % 0.51/0.74 & v1_xreal_0(B) % 0.51/0.74 & v1_int_1(B) % 0.51/0.74 & v1_rat_1(B) ) ) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc14_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v5_membered(A) % 0.51/0.74 => ! [B] : % 0.51/0.74 ( m1_subset_1(B,A) % 0.51/0.74 => ( v1_xcmplx_0(B) % 0.51/0.74 & v4_ordinal2(B) % 0.51/0.74 & v1_xreal_0(B) % 0.51/0.74 & v1_int_1(B) % 0.51/0.74 & v1_rat_1(B) ) ) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc16_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v1_membered(A) % 0.51/0.74 => ! [B] : % 0.51/0.74 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.51/0.74 => v1_membered(B) ) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc17_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v2_membered(A) % 0.51/0.74 => ! [B] : % 0.51/0.74 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.51/0.74 => ( v1_membered(B) % 0.51/0.74 & v2_membered(B) ) ) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc18_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v3_membered(A) % 0.51/0.74 => ! [B] : % 0.51/0.74 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.51/0.74 => ( v1_membered(B) % 0.51/0.74 & v2_membered(B) % 0.51/0.74 & v3_membered(B) ) ) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc19_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v4_membered(A) % 0.51/0.74 => ! [B] : % 0.51/0.74 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.51/0.74 => ( v1_membered(B) % 0.51/0.74 & v2_membered(B) % 0.51/0.74 & v3_membered(B) % 0.51/0.74 & v4_membered(B) ) ) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc1_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v5_membered(A) % 0.51/0.74 => v4_membered(A) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc20_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v5_membered(A) % 0.51/0.74 => ! [B] : % 0.51/0.74 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.51/0.74 => ( v1_membered(B) % 0.51/0.74 & v2_membered(B) % 0.51/0.74 & v3_membered(B) % 0.51/0.74 & v4_membered(B) % 0.51/0.74 & v5_membered(B) ) ) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc2_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v4_membered(A) % 0.51/0.74 => v3_membered(A) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc3_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v3_membered(A) % 0.51/0.74 => v2_membered(A) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc4_membered,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( v2_membered(A) % 0.51/0.74 => v1_membered(A) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc4_tops_1,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( ( v2_pre_topc(A) % 0.51/0.74 & l1_pre_topc(A) ) % 0.51/0.74 => ! [B] : % 0.51/0.74 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.74 => ( v3_tops_1(B,A) % 0.51/0.74 => v2_tops_1(B,A) ) ) ) ). % 0.51/0.74 % 0.51/0.74 fof(cc5_tops_1,axiom, % 0.51/0.74 ! [A] : % 0.51/0.74 ( ( v2_pre_topc(A) % 0.51/0.75 & l1_pre_topc(A) ) % 0.51/0.75 => ! [B] : % 0.51/0.75 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.75 => ( ( v4_pre_topc(B,A) % 0.51/0.75 & v2_tops_1(B,A) ) % 0.51/0.75 => ( v2_tops_1(B,A) % 0.51/0.75 & v3_tops_1(B,A) ) ) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(cc6_tops_1,axiom, % 0.51/0.75 ! [A] : % 0.51/0.75 ( ( v2_pre_topc(A) % 0.51/0.75 & l1_pre_topc(A) ) % 0.51/0.75 => ! [B] : % 0.51/0.75 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.75 => ( ( v3_pre_topc(B,A) % 0.51/0.75 & v3_tops_1(B,A) ) % 0.51/0.75 => ( v1_xboole_0(B) % 0.51/0.75 & v3_pre_topc(B,A) % 0.51/0.75 & v4_pre_topc(B,A) % 0.51/0.75 & v1_membered(B) % 0.51/0.75 & v2_membered(B) % 0.51/0.75 & v3_membered(B) % 0.51/0.75 & v4_membered(B) % 0.51/0.75 & v5_membered(B) % 0.51/0.75 & v2_tops_1(B,A) % 0.51/0.75 & v3_tops_1(B,A) ) ) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(fc10_tops_1,axiom, % 0.51/0.75 ! [A,B] : % 0.51/0.75 ( ( l1_pre_topc(A) % 0.51/0.75 & v2_tops_1(B,A) % 0.51/0.75 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 0.51/0.75 => ( v1_xboole_0(k1_tops_1(A,B)) % 0.51/0.75 & v1_membered(k1_tops_1(A,B)) % 0.51/0.75 & v2_membered(k1_tops_1(A,B)) % 0.51/0.75 & v3_membered(k1_tops_1(A,B)) % 0.51/0.75 & v4_membered(k1_tops_1(A,B)) % 0.51/0.75 & v5_membered(k1_tops_1(A,B)) % 0.51/0.75 & v2_tops_1(k1_tops_1(A,B),A) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(fc27_membered,axiom, % 0.51/0.75 ! [A,B] : % 0.51/0.75 ( v1_membered(A) % 0.51/0.75 => v1_membered(k3_xboole_0(A,B)) ) ). % 0.51/0.75 % 0.51/0.75 fof(fc28_membered,axiom, % 0.51/0.75 ! [A,B] : % 0.51/0.75 ( v1_membered(A) % 0.51/0.75 => v1_membered(k3_xboole_0(B,A)) ) ). % 0.51/0.75 % 0.51/0.75 fof(fc29_membered,axiom, % 0.51/0.75 ! [A,B] : % 0.51/0.75 ( v2_membered(A) % 0.51/0.75 => ( v1_membered(k3_xboole_0(A,B)) % 0.51/0.75 & v2_membered(k3_xboole_0(A,B)) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(fc30_membered,axiom, % 0.51/0.75 ! [A,B] : % 0.51/0.75 ( v2_membered(A) % 0.51/0.75 => ( v1_membered(k3_xboole_0(B,A)) % 0.51/0.75 & v2_membered(k3_xboole_0(B,A)) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(fc31_membered,axiom, % 0.51/0.75 ! [A,B] : % 0.51/0.75 ( v3_membered(A) % 0.51/0.75 => ( v1_membered(k3_xboole_0(A,B)) % 0.51/0.75 & v2_membered(k3_xboole_0(A,B)) % 0.51/0.75 & v3_membered(k3_xboole_0(A,B)) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(fc32_membered,axiom, % 0.51/0.75 ! [A,B] : % 0.51/0.75 ( v3_membered(A) % 0.51/0.75 => ( v1_membered(k3_xboole_0(B,A)) % 0.51/0.75 & v2_membered(k3_xboole_0(B,A)) % 0.51/0.75 & v3_membered(k3_xboole_0(B,A)) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(fc33_membered,axiom, % 0.51/0.75 ! [A,B] : % 0.51/0.75 ( v4_membered(A) % 0.51/0.75 => ( v1_membered(k3_xboole_0(A,B)) % 0.51/0.75 & v2_membered(k3_xboole_0(A,B)) % 0.51/0.75 & v3_membered(k3_xboole_0(A,B)) % 0.51/0.75 & v4_membered(k3_xboole_0(A,B)) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(fc34_membered,axiom, % 0.51/0.75 ! [A,B] : % 0.51/0.75 ( v4_membered(A) % 0.51/0.75 => ( v1_membered(k3_xboole_0(B,A)) % 0.51/0.75 & v2_membered(k3_xboole_0(B,A)) % 0.51/0.75 & v3_membered(k3_xboole_0(B,A)) % 0.51/0.75 & v4_membered(k3_xboole_0(B,A)) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(fc35_membered,axiom, % 0.51/0.75 ! [A,B] : % 0.51/0.75 ( v5_membered(A) % 0.51/0.75 => ( v1_membered(k3_xboole_0(A,B)) % 0.51/0.75 & v2_membered(k3_xboole_0(A,B)) % 0.51/0.75 & v3_membered(k3_xboole_0(A,B)) % 0.51/0.75 & v4_membered(k3_xboole_0(A,B)) % 0.51/0.75 & v5_membered(k3_xboole_0(A,B)) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(fc36_membered,axiom, % 0.51/0.75 ! [A,B] : % 0.51/0.75 ( v5_membered(A) % 0.51/0.75 => ( v1_membered(k3_xboole_0(B,A)) % 0.51/0.75 & v2_membered(k3_xboole_0(B,A)) % 0.51/0.75 & v3_membered(k3_xboole_0(B,A)) % 0.51/0.75 & v4_membered(k3_xboole_0(B,A)) % 0.51/0.75 & v5_membered(k3_xboole_0(B,A)) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(fc6_membered,axiom, % 0.51/0.75 ( v1_xboole_0(k1_xboole_0) % 0.51/0.75 & v1_membered(k1_xboole_0) % 0.51/0.75 & v2_membered(k1_xboole_0) % 0.51/0.75 & v3_membered(k1_xboole_0) % 0.51/0.75 & v4_membered(k1_xboole_0) % 0.51/0.75 & v5_membered(k1_xboole_0) ) ). % 0.51/0.75 % 0.51/0.75 fof(rc1_membered,axiom, % 0.51/0.75 ? [A] : % 0.51/0.75 ( ~ v1_xboole_0(A) % 0.51/0.75 & v1_membered(A) % 0.51/0.75 & v2_membered(A) % 0.51/0.75 & v3_membered(A) % 0.51/0.75 & v4_membered(A) % 0.51/0.75 & v5_membered(A) ) ). % 0.51/0.75 % 0.51/0.75 fof(rc2_tops_1,axiom, % 0.51/0.75 ! [A] : % 0.51/0.75 ( ( v2_pre_topc(A) % 0.51/0.75 & l1_pre_topc(A) ) % 0.51/0.75 => ? [B] : % 0.51/0.75 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.75 & v3_pre_topc(B,A) % 0.51/0.75 & v4_pre_topc(B,A) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(rc3_tops_1,axiom, % 0.51/0.75 ! [A] : % 0.51/0.75 ( ( ~ v3_struct_0(A) % 0.51/0.75 & v2_pre_topc(A) % 0.51/0.75 & l1_pre_topc(A) ) % 0.51/0.75 => ? [B] : % 0.51/0.75 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.75 & ~ v1_xboole_0(B) % 0.51/0.75 & v3_pre_topc(B,A) % 0.51/0.75 & v4_pre_topc(B,A) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(rc4_tops_1,axiom, % 0.51/0.75 ! [A] : % 0.51/0.75 ( l1_pre_topc(A) % 0.51/0.75 => ? [B] : % 0.51/0.75 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.75 & v1_xboole_0(B) % 0.51/0.75 & v1_membered(B) % 0.51/0.75 & v2_membered(B) % 0.51/0.75 & v3_membered(B) % 0.51/0.75 & v4_membered(B) % 0.51/0.75 & v5_membered(B) % 0.51/0.75 & v2_tops_1(B,A) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(rc5_tops_1,axiom, % 0.51/0.75 ! [A] : % 0.51/0.75 ( ( v2_pre_topc(A) % 0.51/0.75 & l1_pre_topc(A) ) % 0.51/0.75 => ? [B] : % 0.51/0.75 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.75 & v1_xboole_0(B) % 0.51/0.75 & v3_pre_topc(B,A) % 0.51/0.75 & v4_pre_topc(B,A) % 0.51/0.75 & v1_membered(B) % 0.51/0.75 & v2_membered(B) % 0.51/0.75 & v3_membered(B) % 0.51/0.75 & v4_membered(B) % 0.51/0.75 & v5_membered(B) % 0.51/0.75 & v2_tops_1(B,A) % 0.51/0.75 & v3_tops_1(B,A) ) ) ). % 0.51/0.75 % 0.51/0.75 fof(rc6_pre_topc,axiom, % 0.51/0.75 ! [A] : % 0.51/0.76 ( ( v2_pre_topc(A) % 0.51/0.76 & l1_pre_topc(A) ) % 0.51/0.76 => ? [B] : % 0.51/0.76 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.76 & v4_pre_topc(B,A) ) ) ). % 0.51/0.76 % 0.51/0.76 fof(rc7_pre_topc,axiom, % 0.51/0.76 ! [A] : % 0.51/0.76 ( ( ~ v3_struct_0(A) % 0.51/0.76 & v2_pre_topc(A) % 0.51/0.76 & l1_pre_topc(A) ) % 0.51/0.76 => ? [B] : % 0.51/0.76 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.76 & ~ v1_xboole_0(B) % 0.51/0.76 & v4_pre_topc(B,A) ) ) ). % 0.51/0.76 % 0.51/0.76 fof(t1_subset,axiom, % 0.51/0.76 ! [A,B] : % 0.51/0.76 ( r2_hidden(A,B) % 0.51/0.76 => m1_subset_1(A,B) ) ). % 0.51/0.76 % 0.51/0.76 fof(t2_boole,axiom, % 0.51/0.76 ! [A] : k3_xboole_0(A,k1_xboole_0) = k1_xboole_0 ). % 0.51/0.76 % 0.51/0.76 fof(t4_subset,axiom, % 0.51/0.76 ! [A,B,C] : % 0.51/0.76 ( ( r2_hidden(A,B) % 0.51/0.76 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 0.51/0.76 => m1_subset_1(A,C) ) ). % 0.51/0.76 % 0.51/0.76 fof(t5_subset,axiom, % 0.51/0.76 ! [A,B,C] : % 0.51/0.76 ~ ( r2_hidden(A,B) % 0.51/0.76 & m1_subset_1(B,k1_zfmisc_1(C)) % 0.51/0.76 & v1_xboole_0(C) ) ). % 0.51/0.76 % 0.51/0.76 fof(commutativity_k3_xboole_0,axiom, % 0.51/0.76 ! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A) ). % 0.51/0.76 % 0.51/0.76 fof(idempotence_k3_xboole_0,axiom, % 0.51/0.76 ! [A,B] : k3_xboole_0(A,A) = A ). % 0.51/0.76 % 0.51/0.76 fof(reflexivity_r1_tarski,axiom, % 0.51/0.76 ! [A,B] : r1_tarski(A,A) ). % 0.51/0.76 % 0.51/0.76 fof(existence_l1_struct_0,axiom, % 0.51/0.76 ? [A] : l1_struct_0(A) ). % 0.51/0.76 % 0.51/0.76 fof(dt_k3_xboole_0,axiom, % 0.51/0.76 $true ). % 0.51/0.76 % 0.51/0.76 fof(dt_l1_struct_0,axiom, % 0.51/0.76 $true ). % 0.51/0.76 % 0.51/0.76 fof(cc15_membered,axiom, % 0.51/0.76 ! [A] : % 0.51/0.76 ( v1_xboole_0(A) % 0.51/0.76 => ( v1_membered(A) % 0.51/0.76 & v2_membered(A) % 0.51/0.76 & v3_membered(A) % 0.51/0.76 & v4_membered(A) % 0.51/0.76 & v5_membered(A) ) ) ). % 0.51/0.76 % 0.51/0.76 fof(cc1_tops_1,axiom, % 0.51/0.76 ! [A] : % 0.51/0.76 ( ( v2_pre_topc(A) % 0.51/0.76 & l1_pre_topc(A) ) % 0.51/0.76 => ! [B] : % 0.51/0.76 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.76 => ( v1_xboole_0(B) % 0.51/0.76 => ( v3_pre_topc(B,A) % 0.51/0.76 & v4_pre_topc(B,A) ) ) ) ) ). % 0.51/0.76 % 0.51/0.76 fof(cc2_tops_1,axiom, % 0.51/0.76 ! [A] : % 0.51/0.76 ( l1_pre_topc(A) % 0.51/0.76 => ! [B] : % 0.51/0.76 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.76 => ( v1_xboole_0(B) % 0.51/0.76 => v2_tops_1(B,A) ) ) ) ). % 0.51/0.76 % 0.51/0.76 fof(cc3_tops_1,axiom, % 0.51/0.76 ! [A] : % 0.51/0.76 ( ( v2_pre_topc(A) % 0.51/0.76 & l1_pre_topc(A) ) % 0.51/0.76 => ! [B] : % 0.51/0.76 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.51/0.76 => ( v1_xboole_0(B) % 0.51/0.76 => v3_tops_1(B,A) ) ) ) ). % 0.51/0.76 % 0.51/0.76 fof(fc1_struct_0,axiom, % 0.51/0.76 ! [A] : % 0.51/0.76 ( ( ~ v3_struct_0(A) % 0.51/0.76 & l1_struct_0(A) ) % 0.51/0.76 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 0.51/0.76 % 0.51/0.76 fof(rc1_subset_1,axiom, % 0.73/0.76 ! [A] : % 0.73/0.76 ( ~ v1_xboole_0(A) % 0.73/0.76 => ? [B] : % 0.73/0.76 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.73/0.76 & ~ v1_xboole_0(B) ) ) ). % 0.73/0.76 % 0.73/0.76 fof(rc2_subset_1,axiom, % 0.73/0.76 ! [A] : % 0.73/0.76 ? [B] : % 0.73/0.76 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.73/0.76 & v1_xboole_0(B) ) ). % 0.73/0.76 % 0.73/0.76 fof(rc3_struct_0,axiom, % 0.73/0.76 ? [A] : % 0.73/0.76 ( l1_struct_0(A) % 0.73/0.76 & ~ v3_struct_0(A) ) ). % 0.73/0.76 % 0.73/0.76 fof(rc5_struct_0,axiom, % 0.73/0.76 ! [A] : % 0.73/0.76 ( ( ~ v3_struct_0(A) % 0.73/0.76 & l1_struct_0(A) ) % 0.73/0.76 => ? [B] : % 0.73/0.76 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.73/0.76 & ~ v1_xboole_0(B) ) ) ). % 0.73/0.76 % 0.73/0.76 fof(t2_subset,axiom, % 0.73/0.76 ! [A,B] : % 0.73/0.76 ( m1_subset_1(A,B) % 0.73/0.76 => ( v1_xboole_0(B) % 0.73/0.76 | r2_hidden(A,B) ) ) ). % 0.73/0.76 % 0.73/0.76 fof(t6_boole,axiom, % 0.73/0.76 ! [A] : % 0.73/0.76 ( v1_xboole_0(A) % 0.73/0.76 => A = k1_xboole_0 ) ). % 0.73/0.76 % 0.73/0.76 fof(t7_boole,axiom, % 0.73/0.76 ! [A,B] : % 0.73/0.76 ~ ( r2_hidden(A,B) % 0.73/0.76 & v1_xboole_0(B) ) ). % 0.73/0.76 % 0.73/0.76 fof(t8_boole,axiom, % 0.73/0.76 ! [A,B] : % 0.73/0.76 ~ ( v1_xboole_0(A) % 0.73/0.76 & A != B % 0.73/0.76 & v1_xboole_0(B) ) ). % 0.73/0.76 % 0.73/0.76 fof(commutativity_k5_subset_1,axiom, % 0.73/0.76 ! [A,B,C] : % 0.73/0.76 ( ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.73/0.76 & m1_subset_1(C,k1_zfmisc_1(A)) ) % 0.73/0.76 => k5_subset_1(A,B,C) = k5_subset_1(A,C,B) ) ). % 0.73/0.76 % 0.73/0.76 fof(idempotence_k5_subset_1,axiom, % 0.73/0.76 ! [A,B,C] : % 0.73/0.76 ( ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.73/0.76 & m1_subset_1(C,k1_zfmisc_1(A)) ) % 0.73/0.76 => k5_subset_1(A,B,B) = B ) ). % 0.73/0.76 % 0.73/0.76 fof(existence_l1_pre_topc,axiom, % 0.73/0.76 ? [A] : l1_pre_topc(A) ). % 0.73/0.76 % 0.73/0.76 fof(existence_m1_subset_1,axiom, % 0.73/0.76 ! [A] : % 0.73/0.76 ? [B] : m1_subset_1(B,A) ). % 0.73/0.76 % 0.73/0.76 fof(redefinition_k5_subset_1,axiom, % 0.73/0.76 ! [A,B,C] : % 0.73/0.76 ( ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.73/0.76 & m1_subset_1(C,k1_zfmisc_1(A)) ) % 0.73/0.76 => k5_subset_1(A,B,C) = k3_xboole_0(B,C) ) ). % 0.73/0.76 % 0.73/0.76 fof(dt_k1_tops_1,axiom, % 0.73/0.76 ! [A,B] : % 0.73/0.76 ( ( l1_pre_topc(A) % 0.73/0.76 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 0.73/0.76 => m1_subset_1(k1_tops_1(A,B),k1_zfmisc_1(u1_struct_0(A))) ) ). % 0.73/0.76 % 0.73/0.76 fof(dt_k1_zfmisc_1,axiom, % 0.73/0.76 $true ). % 0.73/0.76 % 0.73/0.76 fof(dt_k3_tex_4,axiom, % 0.73/0.76 ! [A,B] : % 0.73/0.76 ( ( ~ v3_struct_0(A) % 0.73/0.76 & l1_pre_topc(A) % 0.73/0.76 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 0.73/0.76 => m1_subset_1(k3_tex_4(A,B),k1_zfmisc_1(u1_struct_0(A))) ) ). % 0.73/0.76 % 0.73/0.76 fof(dt_k5_subset_1,axiom, % 0.73/0.76 ! [A,B,C] : % 0.73/0.76 ( ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.73/0.76 & m1_subset_1(C,k1_zfmisc_1(A)) ) % 0.73/0.76 => m1_subset_1(k5_subset_1(A,B,C),k1_zfmisc_1(A)) ) ). % 0.73/0.76 % 0.73/0.76 fof(dt_l1_pre_topc,axiom, % 0.73/0.76 ! [A] : % 0.73/0.76 ( l1_pre_topc(A) % 0.73/0.76 => l1_struct_0(A) ) ). % 0.73/0.76 % 0.73/0.76 fof(dt_m1_subset_1,axiom, % 0.73/0.76 $true ). % 0.73/0.76 % 0.73/0.76 fof(dt_u1_struct_0,axiom, % 0.73/0.76 $true ). % 0.73/0.76 % 0.73/0.76 fof(fc1_subset_1,axiom, % 0.73/0.76 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 0.73/0.76 % 0.73/0.76 fof(fc6_tops_1,axiom, % 0.73/0.76 ! [A,B] : % 0.73/0.76 ( ( v2_pre_topc(A) % 0.73/0.76 & l1_pre_topc(A) % 0.73/0.76 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 0.73/0.76 => v3_pre_topc(k1_tops_1(A,B),A) ) ). % 0.73/0.76 % 0.73/0.76 fof(rc1_tops_1,axiom, % 0.73/0.76 ! [A] : % 0.73/0.76 ( ( v2_pre_topc(A) % 0.73/0.76 & l1_pre_topc(A) ) % 0.73/0.76 => ? [B] : % 0.73/0.76 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.73/0.76 & v3_pre_topc(B,A) ) ) ). % 0.73/0.76 % 0.73/0.76 fof(t3_subset,axiom, % 0.73/0.76 ! [A,B] : % 0.73/0.76 ( m1_subset_1(A,k1_zfmisc_1(B)) % 0.73/0.76 <=> r1_tarski(A,B) ) ). % 0.73/0.76 % 0.73/0.76 fof(t6_tsp_2,axiom, % 0.73/0.76 ! [A] : % 0.73/0.76 ( ( ~ v3_struct_0(A) % 0.73/0.76 & v2_pre_topc(A) % 0.73/0.76 & l1_pre_topc(A) ) % 0.73/0.76 => ! [B] : % 0.73/0.76 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.73/0.76 => ( v1_tsp_2(B,A) % 0.73/0.76 => ! [C] : % 0.73/0.76 ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) % 0.73/0.76 => ( v3_pre_topc(C,A) % 0.73/0.76 => C = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,C)) ) ) ) ) ) ). % 0.73/0.76 % 0.73/0.76 %------------------------------------------------------------------------------ % 0.73/0.76 %------------------------------------------- % 0.73/0.76 % Proof found % 0.73/0.76 % SZS status Theorem for theBenchmark % 0.73/0.76 % SZS output start Proof % 0.73/0.76 %ClaNum:234(EqnAxiom:56) % 0.73/0.76 %VarNum:649(SingletonVarNum:259) % 0.73/0.76 %MaxLitNum:8 % 0.73/0.76 %MaxfuncDepth:3 % 0.73/0.76 %SharedTerms:36 % 0.73/0.76 %goalClause: 57 58 74 79 80 83 87 % 0.73/0.76 %singleGoalClaCount:7 % 0.73/0.76 [57]P1(a1) % 0.73/0.76 [58]P2(a1) % 0.73/0.76 [59]P2(a2) % 0.73/0.76 [60]P3(a11) % 0.73/0.76 [61]P3(a12) % 0.73/0.76 [62]P9(a11) % 0.73/0.76 [63]P9(a12) % 0.73/0.76 [64]P15(a11) % 0.73/0.76 [65]P15(a12) % 0.73/0.76 [66]P17(a11) % 0.73/0.76 [67]P17(a12) % 0.73/0.76 [68]P21(a11) % 0.73/0.76 [69]P21(a12) % 0.73/0.76 [70]P10(a11) % 0.73/0.76 [71]P4(a3) % 0.73/0.76 [72]P4(a5) % 0.73/0.76 [74]P11(a13,a1) % 0.73/0.76 [83]~P18(a1) % 0.73/0.76 [84]~P18(a5) % 0.73/0.76 [85]~P10(a12) % 0.73/0.76 [79]P6(a13,f22(f24(a1))) % 0.73/0.76 [80]P6(a14,f22(f24(a1))) % 0.73/0.76 [87]~E(f23(a1,f25(f24(a1),a13,f15(a1,a14))),f15(a1,a14)) % 0.73/0.76 [76]P5(x761,x761) % 0.73/0.76 [73]P10(f6(x731)) % 0.73/0.76 [75]E(f21(x751,a11),a11) % 0.73/0.76 [77]E(f21(x771,x771),x771) % 0.73/0.76 [78]P6(f9(x781),x781) % 0.73/0.76 [81]P6(f6(x811),f22(x811)) % 0.73/0.76 [86]~P10(f22(x861)) % 0.73/0.76 [82]E(f21(x821,x822),f21(x822,x821)) % 0.73/0.76 [88]~P10(x881)+E(x881,a11) % 0.73/0.76 [89]~P9(x891)+P3(x891) % 0.73/0.76 [90]~P10(x901)+P3(x901) % 0.73/0.76 [91]~P15(x911)+P9(x911) % 0.73/0.76 [92]~P10(x921)+P9(x921) % 0.73/0.76 [93]~P17(x931)+P15(x931) % 0.73/0.76 [94]~P10(x941)+P15(x941) % 0.73/0.77 [95]~P21(x951)+P17(x951) % 0.73/0.77 [96]~P10(x961)+P17(x961) % 0.73/0.77 [97]~P10(x971)+P21(x971) % 0.73/0.77 [98]~P2(x981)+P4(x981) % 0.73/0.77 [100]~P2(x1001)+P3(f16(x1001)) % 0.73/0.77 [101]~P2(x1011)+P9(f16(x1011)) % 0.73/0.77 [102]~P2(x1021)+P15(f16(x1021)) % 0.73/0.77 [103]~P2(x1031)+P17(f16(x1031)) % 0.73/0.77 [104]~P2(x1041)+P21(f16(x1041)) % 0.73/0.77 [105]~P2(x1051)+P10(f16(x1051)) % 0.73/0.77 [106]P10(x1061)+~P10(f7(x1061)) % 0.73/0.77 [113]~P2(x1131)+P16(f16(x1131),x1131) % 0.73/0.77 [117]P10(x1171)+P6(f7(x1171),f22(x1171)) % 0.73/0.77 [195]~P2(x1951)+P6(f16(x1951),f22(f24(x1951))) % 0.73/0.77 [116]~P10(x1161)+~P7(x1162,x1161) % 0.73/0.77 [143]~P7(x1431,x1432)+P6(x1431,x1432) % 0.73/0.77 [194]~P7(x1942,x1941)+~P7(x1941,x1942) % 0.73/0.77 [144]~P3(x1442)+P3(f21(x1441,x1442)) % 0.73/0.77 [145]~P3(x1451)+P3(f21(x1451,x1452)) % 0.73/0.77 [146]~P9(x1462)+P3(f21(x1461,x1462)) % 0.73/0.77 [147]~P9(x1471)+P3(f21(x1471,x1472)) % 0.73/0.77 [148]~P15(x1482)+P3(f21(x1481,x1482)) % 0.73/0.77 [149]~P15(x1491)+P3(f21(x1491,x1492)) % 0.73/0.77 [150]~P17(x1502)+P3(f21(x1501,x1502)) % 0.73/0.77 [151]~P17(x1511)+P3(f21(x1511,x1512)) % 0.73/0.77 [152]~P21(x1522)+P3(f21(x1521,x1522)) % 0.73/0.77 [153]~P21(x1531)+P3(f21(x1531,x1532)) % 0.73/0.77 [154]~P9(x1542)+P9(f21(x1541,x1542)) % 0.73/0.77 [155]~P9(x1551)+P9(f21(x1551,x1552)) % 0.73/0.77 [156]~P15(x1562)+P9(f21(x1561,x1562)) % 0.73/0.77 [157]~P15(x1571)+P9(f21(x1571,x1572)) % 0.73/0.77 [158]~P17(x1582)+P9(f21(x1581,x1582)) % 0.73/0.77 [159]~P17(x1591)+P9(f21(x1591,x1592)) % 0.73/0.77 [160]~P21(x1602)+P9(f21(x1601,x1602)) % 0.73/0.77 [161]~P21(x1611)+P9(f21(x1611,x1612)) % 0.73/0.77 [162]~P15(x1622)+P15(f21(x1621,x1622)) % 0.73/0.77 [163]~P15(x1631)+P15(f21(x1631,x1632)) % 0.73/0.77 [164]~P17(x1642)+P15(f21(x1641,x1642)) % 0.73/0.77 [165]~P17(x1651)+P15(f21(x1651,x1652)) % 0.73/0.77 [166]~P21(x1662)+P15(f21(x1661,x1662)) % 0.73/0.77 [167]~P21(x1671)+P15(f21(x1671,x1672)) % 0.73/0.77 [168]~P17(x1682)+P17(f21(x1681,x1682)) % 0.73/0.77 [169]~P17(x1691)+P17(f21(x1691,x1692)) % 0.73/0.77 [170]~P21(x1702)+P17(f21(x1701,x1702)) % 0.73/0.77 [171]~P21(x1711)+P17(f21(x1711,x1712)) % 0.73/0.77 [172]~P21(x1722)+P21(f21(x1721,x1722)) % 0.73/0.77 [173]~P21(x1731)+P21(f21(x1731,x1732)) % 0.73/0.77 [178]~P5(x1781,x1782)+P6(x1781,f22(x1782)) % 0.73/0.77 [196]P5(x1961,x1962)+~P6(x1961,f22(x1962)) % 0.73/0.77 [107]~P1(x1071)+~P2(x1071)+P3(f19(x1071)) % 0.73/0.77 [108]~P1(x1081)+~P2(x1081)+P9(f19(x1081)) % 0.73/0.77 [109]~P1(x1091)+~P2(x1091)+P15(f19(x1091)) % 0.73/0.77 [110]~P1(x1101)+~P2(x1101)+P17(f19(x1101)) % 0.73/0.77 [111]~P1(x1111)+~P2(x1111)+P21(f19(x1111)) % 0.73/0.77 [112]~P1(x1121)+~P2(x1121)+P10(f19(x1121)) % 0.73/0.77 [114]~P4(x1141)+P18(x1141)+~P10(f24(x1141)) % 0.73/0.77 [115]~P4(x1151)+P18(x1151)+~P10(f8(x1151)) % 0.73/0.77 [133]~P1(x1331)+~P2(x1331)+P20(f19(x1331),x1331) % 0.73/0.77 [134]~P1(x1341)+~P2(x1341)+P16(f19(x1341),x1341) % 0.73/0.77 [135]~P1(x1351)+~P2(x1351)+P23(f17(x1351),x1351) % 0.73/0.77 [136]~P1(x1361)+~P2(x1361)+P23(f19(x1361),x1361) % 0.73/0.77 [137]~P1(x1371)+~P2(x1371)+P23(f20(x1371),x1371) % 0.73/0.77 [138]~P1(x1381)+~P2(x1381)+P19(f17(x1381),x1381) % 0.73/0.77 [139]~P1(x1391)+~P2(x1391)+P19(f19(x1391),x1391) % 0.73/0.77 [140]~P1(x1401)+~P2(x1401)+P19(f10(x1401),x1401) % 0.73/0.77 [197]~P4(x1971)+P18(x1971)+P6(f8(x1971),f22(f24(x1971))) % 0.73/0.77 [198]~P1(x1981)+~P2(x1981)+P6(f17(x1981),f22(f24(x1981))) % 0.73/0.77 [199]~P1(x1991)+~P2(x1991)+P6(f19(x1991),f22(f24(x1991))) % 0.73/0.77 [200]~P1(x2001)+~P2(x2001)+P6(f20(x2001),f22(f24(x2001))) % 0.73/0.77 [201]~P1(x2011)+~P2(x2011)+P6(f10(x2011),f22(f24(x2011))) % 0.73/0.77 [99]~P10(x992)+~P10(x991)+E(x991,x992) % 0.73/0.77 [118]~P6(x1181,x1182)+P13(x1181)+~P3(x1182) % 0.73/0.77 [119]~P6(x1191,x1192)+P13(x1191)+~P9(x1192) % 0.73/0.77 [120]~P6(x1201,x1202)+P13(x1201)+~P15(x1202) % 0.73/0.77 [121]~P6(x1211,x1212)+P13(x1211)+~P17(x1212) % 0.73/0.77 [122]~P6(x1221,x1222)+P13(x1221)+~P21(x1222) % 0.73/0.77 [123]~P6(x1231,x1232)+P14(x1231)+~P9(x1232) % 0.73/0.77 [124]~P6(x1241,x1242)+P14(x1241)+~P15(x1242) % 0.73/0.77 [125]~P6(x1251,x1252)+P14(x1251)+~P17(x1252) % 0.73/0.77 [126]~P6(x1261,x1262)+P14(x1261)+~P21(x1262) % 0.73/0.77 [127]~P6(x1271,x1272)+P12(x1271)+~P15(x1272) % 0.73/0.77 [128]~P6(x1281,x1282)+P12(x1281)+~P17(x1282) % 0.73/0.77 [129]~P6(x1291,x1292)+P12(x1291)+~P21(x1292) % 0.73/0.77 [130]~P6(x1301,x1302)+P8(x1301)+~P17(x1302) % 0.73/0.77 [131]~P6(x1311,x1312)+P8(x1311)+~P21(x1312) % 0.73/0.77 [132]~P6(x1321,x1322)+P22(x1321)+~P21(x1322) % 0.73/0.77 [177]~P6(x1772,x1771)+P10(x1771)+P7(x1772,x1771) % 0.73/0.77 [179]P3(x1791)+~P3(x1792)+~P6(x1791,f22(x1792)) % 0.73/0.77 [180]P3(x1801)+~P9(x1802)+~P6(x1801,f22(x1802)) % 0.73/0.77 [181]P3(x1811)+~P15(x1812)+~P6(x1811,f22(x1812)) % 0.73/0.77 [182]P3(x1821)+~P17(x1822)+~P6(x1821,f22(x1822)) % 0.73/0.77 [183]P3(x1831)+~P21(x1832)+~P6(x1831,f22(x1832)) % 0.73/0.77 [184]P9(x1841)+~P9(x1842)+~P6(x1841,f22(x1842)) % 0.73/0.77 [185]P9(x1851)+~P15(x1852)+~P6(x1851,f22(x1852)) % 0.73/0.77 [186]P9(x1861)+~P17(x1862)+~P6(x1861,f22(x1862)) % 0.73/0.77 [187]P9(x1871)+~P21(x1872)+~P6(x1871,f22(x1872)) % 0.73/0.77 [188]P15(x1881)+~P15(x1882)+~P6(x1881,f22(x1882)) % 0.73/0.77 [189]P15(x1891)+~P17(x1892)+~P6(x1891,f22(x1892)) % 0.73/0.77 [190]P15(x1901)+~P21(x1902)+~P6(x1901,f22(x1902)) % 0.73/0.77 [191]P17(x1911)+~P17(x1912)+~P6(x1911,f22(x1912)) % 0.73/0.77 [192]P17(x1921)+~P21(x1922)+~P6(x1921,f22(x1922)) % 0.73/0.77 [193]P21(x1931)+~P21(x1932)+~P6(x1931,f22(x1932)) % 0.73/0.77 [224]~P2(x2241)+~P6(x2242,f22(f24(x2241)))+P6(f15(x2241,x2242),f22(f24(x2241))) % 0.73/0.77 [204]~P10(x2041)+~P7(x2042,x2043)+~P6(x2043,f22(x2041)) % 0.73/0.77 [205]P6(x2051,x2052)+~P7(x2051,x2053)+~P6(x2053,f22(x2052)) % 0.73/0.77 [225]~P6(x2252,f22(x2251))+E(f25(x2251,x2252,x2252),x2252)+~P6(x2253,f22(x2251)) % 0.73/0.77 [231]~P6(x2313,f22(x2311))+~P6(x2312,f22(x2311))+E(f25(x2311,x2312,x2313),f21(x2312,x2313)) % 0.73/0.77 [232]~P6(x2323,f22(x2321))+~P6(x2322,f22(x2321))+E(f25(x2321,x2322,x2323),f25(x2321,x2323,x2322)) % 0.73/0.77 [233]~P6(x2333,f22(x2331))+~P6(x2332,f22(x2331))+P6(f25(x2331,x2332,x2333),f22(x2331)) % 0.73/0.77 [141]~P1(x1411)+~P2(x1411)+P18(x1411)+~P10(f18(x1411)) % 0.73/0.77 [142]~P1(x1421)+~P2(x1421)+P18(x1421)+~P10(f4(x1421)) % 0.73/0.77 [174]~P1(x1741)+~P2(x1741)+P18(x1741)+P23(f18(x1741),x1741) % 0.73/0.77 [175]~P1(x1751)+~P2(x1751)+P18(x1751)+P23(f4(x1751),x1751) % 0.73/0.77 [176]~P1(x1761)+~P2(x1761)+P18(x1761)+P19(f18(x1761),x1761) % 0.73/0.77 [202]~P1(x2021)+~P2(x2021)+P18(x2021)+P6(f18(x2021),f22(f24(x2021))) % 0.73/0.77 [203]~P1(x2031)+~P2(x2031)+P18(x2031)+P6(f4(x2031),f22(f24(x2031))) % 0.73/0.77 [206]~P2(x2062)+~P10(x2061)+P16(x2061,x2062)+~P6(x2061,f22(f24(x2062))) % 0.73/0.77 [211]~P1(x2111)+~P2(x2111)+P19(f15(x2111,x2112),x2111)+~P6(x2112,f22(f24(x2111))) % 0.73/0.77 [212]~P2(x2121)+~P16(x2122,x2121)+~P6(x2122,f22(f24(x2121)))+P3(f15(x2121,x2122)) % 0.73/0.77 [213]~P2(x2131)+~P16(x2132,x2131)+~P6(x2132,f22(f24(x2131)))+P9(f15(x2131,x2132)) % 0.73/0.77 [214]~P2(x2141)+~P16(x2142,x2141)+~P6(x2142,f22(f24(x2141)))+P15(f15(x2141,x2142)) % 0.73/0.77 [215]~P2(x2151)+~P16(x2152,x2151)+~P6(x2152,f22(f24(x2151)))+P17(f15(x2151,x2152)) % 0.73/0.77 [216]~P2(x2161)+~P16(x2162,x2161)+~P6(x2162,f22(f24(x2161)))+P21(f15(x2161,x2162)) % 0.73/0.77 [217]~P2(x2171)+~P16(x2172,x2171)+~P6(x2172,f22(f24(x2171)))+P10(f15(x2171,x2172)) % 0.73/0.77 [226]~P2(x2261)+~P16(x2262,x2261)+P16(f15(x2261,x2262),x2261)+~P6(x2262,f22(f24(x2261))) % 0.73/0.77 [227]~P2(x2271)+P18(x2271)+~P6(x2272,f22(f24(x2271)))+P6(f23(x2271,x2272),f22(f24(x2271))) % 0.73/0.77 [207]~P1(x2072)+~P2(x2072)+~P10(x2071)+P20(x2071,x2072)+~P6(x2071,f22(f24(x2072))) % 0.73/0.77 [208]~P1(x2082)+~P2(x2082)+~P10(x2081)+P23(x2081,x2082)+~P6(x2081,f22(f24(x2082))) % 0.73/0.77 [209]~P1(x2092)+~P2(x2092)+~P10(x2091)+P19(x2091,x2092)+~P6(x2091,f22(f24(x2092))) % 0.73/0.77 [210]~P1(x2102)+~P2(x2102)+~P20(x2101,x2102)+P16(x2101,x2102)+~P6(x2101,f22(f24(x2102))) % 0.73/0.77 [218]~P2(x2182)+~P20(x2181,x2182)+~P19(x2181,x2182)+P3(x2181)+~P1(x2182)+~P6(x2181,f22(f24(x2182))) % 0.73/0.77 [219]~P2(x2192)+~P20(x2191,x2192)+~P19(x2191,x2192)+P9(x2191)+~P1(x2192)+~P6(x2191,f22(f24(x2192))) % 0.73/0.77 [220]~P2(x2202)+~P20(x2201,x2202)+~P19(x2201,x2202)+P15(x2201)+~P1(x2202)+~P6(x2201,f22(f24(x2202))) % 0.73/0.77 [221]~P2(x2212)+~P20(x2211,x2212)+~P19(x2211,x2212)+P17(x2211)+~P1(x2212)+~P6(x2211,f22(f24(x2212))) % 0.73/0.77 [222]~P2(x2222)+~P20(x2221,x2222)+~P19(x2221,x2222)+P21(x2221)+~P1(x2222)+~P6(x2221,f22(f24(x2222))) % 0.73/0.77 [223]~P2(x2232)+~P20(x2231,x2232)+~P19(x2231,x2232)+P10(x2231)+~P1(x2232)+~P6(x2231,f22(f24(x2232))) % 0.73/0.77 [228]~P1(x2282)+~P2(x2282)+~P16(x2281,x2282)+~P23(x2281,x2282)+P20(x2281,x2282)+~P6(x2281,f22(f24(x2282))) % 0.73/0.77 [230]~P1(x2302)+~P2(x2302)+~P20(x2301,x2302)+~P19(x2301,x2302)+P23(x2301,x2302)+~P6(x2301,f22(f24(x2302))) % 0.73/0.77 [234]P18(x2341)+~P1(x2341)+~P2(x2341)+~P11(x2342,x2341)+~P19(x2343,x2341)+~P6(x2343,f22(f24(x2341)))+~P6(x2342,f22(f24(x2341)))+E(f23(x2341,f25(f24(x2341),x2342,x2343)),x2343) % 0.73/0.77 %EqnAxiom % 0.73/0.77 [1]E(x11,x11) % 0.73/0.77 [2]E(x22,x21)+~E(x21,x22) % 0.73/0.77 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.73/0.77 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 0.73/0.77 [5]~E(x51,x52)+E(f21(x51,x53),f21(x52,x53)) % 0.73/0.77 [6]~E(x61,x62)+E(f21(x63,x61),f21(x63,x62)) % 0.73/0.77 [7]~E(x71,x72)+E(f24(x71),f24(x72)) % 0.73/0.77 [8]~E(x81,x82)+E(f9(x81),f9(x82)) % 0.73/0.77 [9]~E(x91,x92)+E(f25(x91,x93,x94),f25(x92,x93,x94)) % 0.73/0.77 [10]~E(x101,x102)+E(f25(x103,x101,x104),f25(x103,x102,x104)) % 0.73/0.77 [11]~E(x111,x112)+E(f25(x113,x114,x111),f25(x113,x114,x112)) % 0.73/0.77 [12]~E(x121,x122)+E(f22(x121),f22(x122)) % 0.73/0.77 [13]~E(x131,x132)+E(f15(x131,x133),f15(x132,x133)) % 0.73/0.77 [14]~E(x141,x142)+E(f15(x143,x141),f15(x143,x142)) % 0.73/0.77 [15]~E(x151,x152)+E(f23(x151,x153),f23(x152,x153)) % 0.73/0.77 [16]~E(x161,x162)+E(f23(x163,x161),f23(x163,x162)) % 0.73/0.77 [17]~E(x171,x172)+E(f4(x171),f4(x172)) % 0.73/0.77 [18]~E(x181,x182)+E(f18(x181),f18(x182)) % 0.73/0.77 [19]~E(x191,x192)+E(f19(x191),f19(x192)) % 0.73/0.77 [20]~E(x201,x202)+E(f10(x201),f10(x202)) % 0.73/0.77 [21]~E(x211,x212)+E(f20(x211),f20(x212)) % 0.73/0.77 [22]~E(x221,x222)+E(f17(x221),f17(x222)) % 0.73/0.77 [23]~E(x231,x232)+E(f8(x231),f8(x232)) % 0.73/0.77 [24]~E(x241,x242)+E(f16(x241),f16(x242)) % 0.73/0.77 [25]~E(x251,x252)+E(f7(x251),f7(x252)) % 0.73/0.77 [26]~P1(x261)+P1(x262)+~E(x261,x262) % 0.73/0.77 [27]~P2(x271)+P2(x272)+~E(x271,x272) % 0.73/0.77 [28]P6(x282,x283)+~E(x281,x282)+~P6(x281,x283) % 0.73/0.77 [29]P6(x293,x292)+~E(x291,x292)+~P6(x293,x291) % 0.73/0.77 [30]~P3(x301)+P3(x302)+~E(x301,x302) % 0.73/0.77 [31]~P15(x311)+P15(x312)+~E(x311,x312) % 0.73/0.77 [32]~P9(x321)+P9(x322)+~E(x321,x322) % 0.73/0.77 [33]~P17(x331)+P17(x332)+~E(x331,x332) % 0.73/0.77 [34]~P21(x341)+P21(x342)+~E(x341,x342) % 0.73/0.77 [35]P5(x352,x353)+~E(x351,x352)+~P5(x351,x353) % 0.73/0.77 [36]P5(x363,x362)+~E(x361,x362)+~P5(x363,x361) % 0.73/0.77 [37]~P18(x371)+P18(x372)+~E(x371,x372) % 0.73/0.77 [38]P20(x382,x383)+~E(x381,x382)+~P20(x381,x383) % 0.73/0.77 [39]P20(x393,x392)+~E(x391,x392)+~P20(x393,x391) % 0.73/0.77 [40]~P8(x401)+P8(x402)+~E(x401,x402) % 0.73/0.77 [41]P19(x412,x413)+~E(x411,x412)+~P19(x411,x413) % 0.73/0.77 [42]P19(x423,x422)+~E(x421,x422)+~P19(x423,x421) % 0.73/0.77 [43]~P10(x431)+P10(x432)+~E(x431,x432) % 0.73/0.77 [44]~P4(x441)+P4(x442)+~E(x441,x442) % 0.73/0.77 [45]P16(x452,x453)+~E(x451,x452)+~P16(x451,x453) % 0.73/0.77 [46]P16(x463,x462)+~E(x461,x462)+~P16(x463,x461) % 0.73/0.77 [47]P7(x472,x473)+~E(x471,x472)+~P7(x471,x473) % 0.73/0.77 [48]P7(x483,x482)+~E(x481,x482)+~P7(x483,x481) % 0.73/0.77 [49]P11(x492,x493)+~E(x491,x492)+~P11(x491,x493) % 0.73/0.77 [50]P11(x503,x502)+~E(x501,x502)+~P11(x503,x501) % 0.73/0.77 [51]~P12(x511)+P12(x512)+~E(x511,x512) % 0.73/0.77 [52]~P13(x521)+P13(x522)+~E(x521,x522) % 0.73/0.77 [53]P23(x532,x533)+~E(x531,x532)+~P23(x531,x533) % 0.73/0.77 [54]P23(x543,x542)+~E(x541,x542)+~P23(x543,x541) % 0.73/0.77 [55]~P14(x551)+P14(x552)+~E(x551,x552) % 0.73/0.77 [56]~P22(x561)+P22(x562)+~E(x561,x562) % 0.73/0.77 % 0.73/0.77 %------------------------------------------- % 0.73/0.77 cnf(235,plain, % 0.73/0.77 (P5(a13,f24(a1))), % 0.73/0.77 inference(scs_inference,[],[79,196])). % 0.73/0.77 cnf(237,plain, % 0.73/0.77 (E(x2371,f21(x2371,x2371))), % 0.73/0.77 inference(scs_inference,[],[79,77,196,2])). % 0.73/0.77 cnf(240,plain, % 0.73/0.77 (P7(f9(a12),a12)), % 0.73/0.77 inference(scs_inference,[],[79,78,77,70,85,196,2,116,177])). % 0.73/0.77 cnf(241,plain, % 0.73/0.77 (P6(f9(x2411),x2411)), % 0.73/0.77 inference(rename_variables,[],[78])). % 0.73/0.77 cnf(243,plain, % 0.73/0.77 (P3(f9(f22(a11)))), % 0.73/0.77 inference(scs_inference,[],[79,78,241,77,60,70,85,196,2,116,177,179])). % 0.73/0.77 cnf(244,plain, % 0.73/0.77 (P6(f9(x2441),x2441)), % 0.73/0.77 inference(rename_variables,[],[78])). % 0.73/0.77 cnf(247,plain, % 0.73/0.77 (P6(f6(x2471),f22(x2471))), % 0.73/0.77 inference(rename_variables,[],[81])). % 0.73/0.77 cnf(250,plain, % 0.73/0.77 (P6(f9(x2501),x2501)), % 0.73/0.77 inference(rename_variables,[],[78])). % 0.73/0.77 cnf(253,plain, % 0.73/0.77 (P6(f6(x2531),f22(x2531))), % 0.73/0.77 inference(rename_variables,[],[81])). % 0.73/0.77 cnf(256,plain, % 0.73/0.77 (P6(f9(x2561),x2561)), % 0.73/0.77 inference(rename_variables,[],[78])). % 0.73/0.77 cnf(259,plain, % 0.73/0.77 (P6(f6(x2591),f22(x2591))), % 0.73/0.77 inference(rename_variables,[],[81])). % 0.73/0.77 cnf(262,plain, % 0.73/0.77 (P6(f9(x2621),x2621)), % 0.73/0.77 inference(rename_variables,[],[78])). % 0.73/0.77 cnf(265,plain, % 0.73/0.77 (P6(f6(x2651),f22(x2651))), % 0.73/0.77 inference(rename_variables,[],[81])). % 0.73/0.77 cnf(268,plain, % 0.73/0.77 (P6(f9(x2681),x2681)), % 0.73/0.77 inference(rename_variables,[],[78])). % 0.73/0.77 cnf(270,plain, % 0.73/0.77 (~P7(x2701,f9(f22(a11)))), % 0.73/0.77 inference(scs_inference,[],[79,78,241,244,250,256,262,268,81,247,253,259,77,60,62,64,66,68,70,85,196,2,116,177,179,180,184,185,188,189,191,192,193,204])). % 0.73/0.77 cnf(271,plain, % 0.73/0.77 (P6(f9(x2711),x2711)), % 0.73/0.77 inference(rename_variables,[],[78])). % 0.73/0.77 cnf(274,plain, % 0.73/0.77 (E(f21(x2741,x2741),x2741)), % 0.73/0.77 inference(rename_variables,[],[77])). % 0.73/0.77 cnf(275,plain, % 0.73/0.77 (P6(f9(f21(x2751,x2751)),x2751)), % 0.73/0.77 inference(scs_inference,[],[79,87,78,241,244,250,256,262,268,271,81,247,253,259,77,274,60,62,64,66,68,70,85,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29])). % 0.73/0.77 cnf(278,plain, % 0.73/0.77 (E(f21(x2781,x2781),x2781)), % 0.73/0.77 inference(rename_variables,[],[77])). % 0.73/0.77 cnf(279,plain, % 0.73/0.77 (~P10(f21(a12,a12))), % 0.73/0.77 inference(scs_inference,[],[83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,77,274,278,60,62,64,66,68,70,85,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43])). % 0.73/0.77 cnf(280,plain, % 0.73/0.77 (E(f21(x2801,x2801),x2801)), % 0.73/0.77 inference(rename_variables,[],[77])). % 0.73/0.77 cnf(282,plain, % 0.73/0.77 (P5(x2821,x2821)), % 0.73/0.77 inference(rename_variables,[],[76])). % 0.73/0.77 cnf(285,plain, % 0.73/0.77 (~E(a12,a11)), % 0.73/0.77 inference(scs_inference,[],[83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,76,282,77,274,278,280,60,62,64,66,68,70,85,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48])). % 0.73/0.77 cnf(286,plain, % 0.73/0.77 (P16(f6(f24(a1)),a1)), % 0.73/0.77 inference(scs_inference,[],[58,83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,265,76,282,77,274,278,280,60,62,64,66,68,70,85,73,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48,206])). % 0.73/0.77 cnf(287,plain, % 0.73/0.77 (P6(f6(x2871),f22(x2871))), % 0.73/0.77 inference(rename_variables,[],[81])). % 0.73/0.77 cnf(288,plain, % 0.73/0.77 (P10(f6(x2881))), % 0.73/0.77 inference(rename_variables,[],[73])). % 0.73/0.77 cnf(293,plain, % 0.73/0.77 (P6(f6(x2931),f22(x2931))), % 0.73/0.77 inference(rename_variables,[],[81])). % 0.73/0.77 cnf(296,plain, % 0.73/0.77 (P6(f6(x2961),f22(x2961))), % 0.73/0.77 inference(rename_variables,[],[81])). % 0.73/0.77 cnf(299,plain, % 0.73/0.77 (P6(f6(x2991),f22(x2991))), % 0.73/0.77 inference(rename_variables,[],[81])). % 0.73/0.77 cnf(302,plain, % 0.73/0.77 (P6(f6(x3021),f22(x3021))), % 0.73/0.77 inference(rename_variables,[],[81])). % 0.73/0.77 cnf(305,plain, % 0.73/0.77 (P6(f6(x3051),f22(x3051))), % 0.73/0.77 inference(rename_variables,[],[81])). % 0.73/0.77 cnf(307,plain, % 0.73/0.77 (P10(f15(a1,f6(f24(a1))))), % 0.73/0.77 inference(scs_inference,[],[57,58,83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,265,287,293,296,299,302,305,76,282,77,274,278,280,60,62,64,66,68,70,85,73,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48,206,211,212,213,214,215,216,217])). % 0.73/0.77 cnf(308,plain, % 0.73/0.77 (P6(f6(x3081),f22(x3081))), % 0.73/0.77 inference(rename_variables,[],[81])). % 0.73/0.77 cnf(311,plain, % 0.73/0.77 (P6(f6(x3111),f22(x3111))), % 0.73/0.77 inference(rename_variables,[],[81])). % 0.73/0.77 cnf(313,plain, % 0.73/0.77 (P20(f6(f24(a1)),a1)), % 0.73/0.77 inference(scs_inference,[],[57,58,83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,265,287,293,296,299,302,305,308,311,76,282,77,274,278,280,60,62,64,66,68,70,85,73,288,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48,206,211,212,213,214,215,216,217,226,207])). % 0.73/0.77 cnf(314,plain, % 0.73/0.77 (P6(f6(x3141),f22(x3141))), % 0.73/0.77 inference(rename_variables,[],[81])). % 0.73/0.77 cnf(315,plain, % 0.73/0.77 (P10(f6(x3151))), % 0.73/0.77 inference(rename_variables,[],[73])). % 0.73/0.77 cnf(317,plain, % 0.73/0.77 (P23(f6(f24(a1)),a1)), % 0.73/0.77 inference(scs_inference,[],[57,58,83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,265,287,293,296,299,302,305,308,311,314,76,282,77,274,278,280,60,62,64,66,68,70,85,73,288,315,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48,206,211,212,213,214,215,216,217,226,207,208])). % 0.73/0.77 cnf(318,plain, % 0.73/0.78 (P6(f6(x3181),f22(x3181))), % 0.73/0.78 inference(rename_variables,[],[81])). % 0.73/0.78 cnf(319,plain, % 0.73/0.78 (P10(f6(x3191))), % 0.73/0.78 inference(rename_variables,[],[73])). % 0.73/0.78 cnf(321,plain, % 0.73/0.78 (P19(f6(f24(a1)),a1)), % 0.73/0.78 inference(scs_inference,[],[57,58,83,79,87,78,241,244,250,256,262,268,271,81,247,253,259,265,287,293,296,299,302,305,308,311,314,318,76,282,77,274,278,280,60,62,64,66,68,70,85,73,288,315,319,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,37,43,35,36,48,206,211,212,213,214,215,216,217,226,207,208,209])). % 0.73/0.78 cnf(360,plain, % 0.73/0.78 (E(x3601,f21(x3601,x3601))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(362,plain, % 0.73/0.78 (E(x3621,f21(x3621,x3621))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(363,plain, % 0.73/0.78 (P6(f21(a14,a14),f22(f24(a1)))), % 0.73/0.78 inference(scs_inference,[],[57,80,58,237,360,362,307,75,196,116,2,26,27,28])). % 0.73/0.78 cnf(364,plain, % 0.73/0.78 (E(x3641,f21(x3641,x3641))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(366,plain, % 0.73/0.78 (E(x3661,f21(x3661,x3661))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(368,plain, % 0.73/0.78 (E(x3681,f21(x3681,x3681))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(370,plain, % 0.73/0.78 (E(x3701,f21(x3701,x3701))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(376,plain, % 0.73/0.78 (E(x3761,f21(x3761,x3761))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(378,plain, % 0.73/0.78 (E(x3781,f21(x3781,x3781))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(380,plain, % 0.73/0.78 (E(x3801,f21(x3801,x3801))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(382,plain, % 0.73/0.78 (E(x3821,f21(x3821,x3821))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(384,plain, % 0.73/0.78 (E(x3841,f21(x3841,x3841))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(386,plain, % 0.73/0.78 (E(x3861,f21(x3861,x3861))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(388,plain, % 0.73/0.78 (E(x3881,f21(x3881,x3881))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(390,plain, % 0.73/0.78 (E(x3901,f21(x3901,x3901))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(392,plain, % 0.73/0.78 (E(x3921,f21(x3921,x3921))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(394,plain, % 0.73/0.78 (E(x3941,f21(x3941,x3941))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(395,plain, % 0.73/0.78 (P7(f9(f21(f21(a12,a12),f21(a12,a12))),f21(a12,a12))), % 0.73/0.78 inference(scs_inference,[],[57,74,80,58,237,360,362,364,366,368,370,376,378,380,382,384,386,388,390,392,275,307,286,313,317,243,321,240,279,71,75,62,64,66,68,196,116,2,26,27,28,49,50,30,31,32,33,34,38,39,41,42,45,46,53,54,44,47,177])). % 0.73/0.78 cnf(402,plain, % 0.73/0.78 (E(x4021,f21(x4021,x4021))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(404,plain, % 0.73/0.78 (E(x4041,f21(x4041,x4041))), % 0.73/0.78 inference(rename_variables,[],[237])). % 0.73/0.78 cnf(414,plain, % 0.73/0.78 (~P6(f15(a1,a14),f22(f24(a1)))), % 0.73/0.78 inference(scs_inference,[],[57,74,80,83,87,79,58,237,360,362,364,366,368,370,376,378,380,382,384,386,388,390,392,394,402,404,275,307,270,286,313,317,243,321,235,240,279,81,71,285,75,77,62,64,66,68,196,116,2,26,27,28,49,50,30,31,32,33,34,38,39,41,42,45,46,53,54,44,47,177,179,29,36,3,43,35,48,211,234])). % 0.73/0.78 cnf(438,plain, % 0.73/0.78 ($false), % 0.73/0.78 inference(scs_inference,[],[80,58,414,395,363,275,73,85,194,196,116,177,224]), % 0.73/0.78 ['proof']). % 0.73/0.78 % SZS output end Proof % 0.73/0.78 % Total time :0.110000s %------------------------------------------------------------------------------