%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : TOP026+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 : n012.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.57s 0.82s % Output : CNFRefutation 0.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.13 % Problem : TOP026+1 : TPTP v8.2.0. Released v3.4.0. % 0.05/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n012.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Jun 18 11:26:23 EDT 2024 % 0.12/0.34 % CPUTime : % 0.48/0.61 start to proof:theBenchmark % 0.57/0.80 %------------------------------------------- % 0.57/0.80 % File :CSE---1.7 % 0.57/0.80 % Problem :theBenchmark % 0.57/0.80 % Transform :cnf % 0.57/0.80 % Format :tptp:raw % 0.57/0.80 % Command :java -jar mcs_scs.jar %d %s % 0.57/0.80 % 0.57/0.80 % Result :Theorem 0.110000s % 0.57/0.80 % Output :CNFRefutation 0.110000s % 0.57/0.80 %------------------------------------------- % 0.57/0.80 %------------------------------------------------------------------------------ % 0.57/0.80 % File : TOP026+1 : TPTP v8.2.0. Released v3.4.0. % 0.57/0.80 % Domain : Topology % 0.57/0.80 % Problem : Maximal Kolmogorov Subspaces of a Topological Space T07 % 0.57/0.80 % Version : [Urb08] axioms : Especial. % 0.57/0.80 % English : % 0.57/0.80 % 0.57/0.80 % Refs : [Kar96] Karno (1996), Maximal Kolmogorov Subspaces of a Topolo % 0.57/0.80 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 0.57/0.80 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 0.57/0.80 % Source : [Urb08] % 0.57/0.80 % Names : t7_tsp_2 [Urb08] % 0.57/0.80 % 0.57/0.80 % Status : Theorem % 0.57/0.80 % Rating : 0.28 v8.2.0, 0.25 v8.1.0, 0.17 v7.5.0, 0.22 v7.4.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.20 v6.0.0, 0.22 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.30 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.57/0.80 % Syntax : Number of formulae : 78 ( 14 unt; 0 def) % 0.57/0.80 % Number of atoms : 296 ( 10 equ) % 0.57/0.80 % Maximal formula atoms : 15 ( 3 avg) % 0.57/0.80 % Number of connectives : 239 ( 21 ~; 1 |; 131 &) % 0.57/0.80 % ( 1 <=>; 85 =>; 0 <=; 0 <~>) % 0.57/0.80 % Maximal formula depth : 15 ( 5 avg) % 0.57/0.80 % Maximal term depth : 4 ( 1 avg) % 0.57/0.80 % Number of predicates : 25 ( 23 usr; 1 prp; 0-2 aty) % 0.57/0.80 % Number of functors : 7 ( 7 usr; 1 con; 0-3 aty) % 0.57/0.80 % Number of variables : 136 ( 121 !; 15 ?) % 0.57/0.80 % SPC : FOF_THM_RFO_SEQ % 0.57/0.80 % 0.57/0.80 % Comments : Normal version: includes the axioms (which may be theorems from % 0.57/0.80 % other articles) and background that are possibly necessary. % 0.57/0.80 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 0.57/0.80 % : The problem encoding is based on set theory. % 0.57/0.80 %------------------------------------------------------------------------------ % 0.57/0.80 fof(t7_tsp_2,conjecture, % 0.57/0.80 ! [A] : % 0.57/0.80 ( ( ~ v3_struct_0(A) % 0.57/0.80 & v2_pre_topc(A) % 0.57/0.80 & l1_pre_topc(A) ) % 0.57/0.80 => ! [B] : % 0.57/0.80 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.80 => ( v1_tsp_2(B,A) % 0.57/0.80 => ! [C] : % 0.57/0.80 ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.80 => k6_pre_topc(A,C) = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,k6_pre_topc(A,C))) ) ) ) ) ). % 0.57/0.80 % 0.57/0.80 fof(antisymmetry_r2_hidden,axiom, % 0.57/0.80 ! [A,B] : % 0.57/0.80 ( r2_hidden(A,B) % 0.57/0.80 => ~ r2_hidden(B,A) ) ). % 0.57/0.80 % 0.57/0.80 fof(dt_k1_xboole_0,axiom, % 0.57/0.80 $true ). % 0.57/0.80 % 0.57/0.80 fof(cc10_membered,axiom, % 0.57/0.80 ! [A] : % 0.57/0.80 ( v1_membered(A) % 0.57/0.80 => ! [B] : % 0.57/0.80 ( m1_subset_1(B,A) % 0.57/0.80 => v1_xcmplx_0(B) ) ) ). % 0.57/0.80 % 0.57/0.80 fof(cc11_membered,axiom, % 0.57/0.80 ! [A] : % 0.57/0.80 ( v2_membered(A) % 0.57/0.80 => ! [B] : % 0.57/0.80 ( m1_subset_1(B,A) % 0.57/0.80 => ( v1_xcmplx_0(B) % 0.57/0.80 & v1_xreal_0(B) ) ) ) ). % 0.57/0.80 % 0.57/0.80 fof(cc12_membered,axiom, % 0.57/0.80 ! [A] : % 0.57/0.80 ( v3_membered(A) % 0.57/0.80 => ! [B] : % 0.57/0.80 ( m1_subset_1(B,A) % 0.57/0.80 => ( v1_xcmplx_0(B) % 0.57/0.80 & v1_xreal_0(B) % 0.57/0.80 & v1_rat_1(B) ) ) ) ). % 0.57/0.80 % 0.57/0.80 fof(cc13_membered,axiom, % 0.57/0.80 ! [A] : % 0.57/0.80 ( v4_membered(A) % 0.57/0.80 => ! [B] : % 0.57/0.80 ( m1_subset_1(B,A) % 0.57/0.80 => ( v1_xcmplx_0(B) % 0.57/0.80 & v1_xreal_0(B) % 0.57/0.80 & v1_int_1(B) % 0.57/0.81 & v1_rat_1(B) ) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc14_membered,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( v5_membered(A) % 0.57/0.81 => ! [B] : % 0.57/0.81 ( m1_subset_1(B,A) % 0.57/0.81 => ( v1_xcmplx_0(B) % 0.57/0.81 & v4_ordinal2(B) % 0.57/0.81 & v1_xreal_0(B) % 0.57/0.81 & v1_int_1(B) % 0.57/0.81 & v1_rat_1(B) ) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc16_membered,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( v1_membered(A) % 0.57/0.81 => ! [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.57/0.81 => v1_membered(B) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc17_membered,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( v2_membered(A) % 0.57/0.81 => ! [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.57/0.81 => ( v1_membered(B) % 0.57/0.81 & v2_membered(B) ) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc18_membered,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( v3_membered(A) % 0.57/0.81 => ! [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.57/0.81 => ( v1_membered(B) % 0.57/0.81 & v2_membered(B) % 0.57/0.81 & v3_membered(B) ) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc19_membered,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( v4_membered(A) % 0.57/0.81 => ! [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.57/0.81 => ( v1_membered(B) % 0.57/0.81 & v2_membered(B) % 0.57/0.81 & v3_membered(B) % 0.57/0.81 & v4_membered(B) ) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc1_membered,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( v5_membered(A) % 0.57/0.81 => v4_membered(A) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc20_membered,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( v5_membered(A) % 0.57/0.81 => ! [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.57/0.81 => ( v1_membered(B) % 0.57/0.81 & v2_membered(B) % 0.57/0.81 & v3_membered(B) % 0.57/0.81 & v4_membered(B) % 0.57/0.81 & v5_membered(B) ) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc2_membered,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( v4_membered(A) % 0.57/0.81 => v3_membered(A) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc3_membered,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( v3_membered(A) % 0.57/0.81 => v2_membered(A) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc4_membered,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( v2_membered(A) % 0.57/0.81 => v1_membered(A) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc4_tops_1,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( ( v2_pre_topc(A) % 0.57/0.81 & l1_pre_topc(A) ) % 0.57/0.81 => ! [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.81 => ( v3_tops_1(B,A) % 0.57/0.81 => v2_tops_1(B,A) ) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc5_tops_1,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( ( v2_pre_topc(A) % 0.57/0.81 & l1_pre_topc(A) ) % 0.57/0.81 => ! [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.81 => ( ( v4_pre_topc(B,A) % 0.57/0.81 & v2_tops_1(B,A) ) % 0.57/0.81 => ( v2_tops_1(B,A) % 0.57/0.81 & v3_tops_1(B,A) ) ) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc6_tops_1,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( ( v2_pre_topc(A) % 0.57/0.81 & l1_pre_topc(A) ) % 0.57/0.81 => ! [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.81 => ( ( v3_pre_topc(B,A) % 0.57/0.81 & v3_tops_1(B,A) ) % 0.57/0.81 => ( v1_xboole_0(B) % 0.57/0.81 & v3_pre_topc(B,A) % 0.57/0.81 & v4_pre_topc(B,A) % 0.57/0.81 & v1_membered(B) % 0.57/0.81 & v2_membered(B) % 0.57/0.81 & v3_membered(B) % 0.57/0.81 & v4_membered(B) % 0.57/0.81 & v5_membered(B) % 0.57/0.81 & v2_tops_1(B,A) % 0.57/0.81 & v3_tops_1(B,A) ) ) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(fc27_membered,axiom, % 0.57/0.81 ! [A,B] : % 0.57/0.81 ( v1_membered(A) % 0.57/0.81 => v1_membered(k3_xboole_0(A,B)) ) ). % 0.57/0.81 % 0.57/0.81 fof(fc28_membered,axiom, % 0.57/0.81 ! [A,B] : % 0.57/0.81 ( v1_membered(A) % 0.57/0.81 => v1_membered(k3_xboole_0(B,A)) ) ). % 0.57/0.81 % 0.57/0.81 fof(fc29_membered,axiom, % 0.57/0.81 ! [A,B] : % 0.57/0.81 ( v2_membered(A) % 0.57/0.81 => ( v1_membered(k3_xboole_0(A,B)) % 0.57/0.81 & v2_membered(k3_xboole_0(A,B)) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(fc30_membered,axiom, % 0.57/0.81 ! [A,B] : % 0.57/0.81 ( v2_membered(A) % 0.57/0.81 => ( v1_membered(k3_xboole_0(B,A)) % 0.57/0.81 & v2_membered(k3_xboole_0(B,A)) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(fc31_membered,axiom, % 0.57/0.81 ! [A,B] : % 0.57/0.81 ( v3_membered(A) % 0.57/0.81 => ( v1_membered(k3_xboole_0(A,B)) % 0.57/0.81 & v2_membered(k3_xboole_0(A,B)) % 0.57/0.81 & v3_membered(k3_xboole_0(A,B)) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(fc32_membered,axiom, % 0.57/0.81 ! [A,B] : % 0.57/0.81 ( v3_membered(A) % 0.57/0.81 => ( v1_membered(k3_xboole_0(B,A)) % 0.57/0.81 & v2_membered(k3_xboole_0(B,A)) % 0.57/0.81 & v3_membered(k3_xboole_0(B,A)) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(fc33_membered,axiom, % 0.57/0.81 ! [A,B] : % 0.57/0.81 ( v4_membered(A) % 0.57/0.81 => ( v1_membered(k3_xboole_0(A,B)) % 0.57/0.81 & v2_membered(k3_xboole_0(A,B)) % 0.57/0.81 & v3_membered(k3_xboole_0(A,B)) % 0.57/0.81 & v4_membered(k3_xboole_0(A,B)) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(fc34_membered,axiom, % 0.57/0.81 ! [A,B] : % 0.57/0.81 ( v4_membered(A) % 0.57/0.81 => ( v1_membered(k3_xboole_0(B,A)) % 0.57/0.81 & v2_membered(k3_xboole_0(B,A)) % 0.57/0.81 & v3_membered(k3_xboole_0(B,A)) % 0.57/0.81 & v4_membered(k3_xboole_0(B,A)) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(fc35_membered,axiom, % 0.57/0.81 ! [A,B] : % 0.57/0.81 ( v5_membered(A) % 0.57/0.81 => ( v1_membered(k3_xboole_0(A,B)) % 0.57/0.81 & v2_membered(k3_xboole_0(A,B)) % 0.57/0.81 & v3_membered(k3_xboole_0(A,B)) % 0.57/0.81 & v4_membered(k3_xboole_0(A,B)) % 0.57/0.81 & v5_membered(k3_xboole_0(A,B)) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(fc36_membered,axiom, % 0.57/0.81 ! [A,B] : % 0.57/0.81 ( v5_membered(A) % 0.57/0.81 => ( v1_membered(k3_xboole_0(B,A)) % 0.57/0.81 & v2_membered(k3_xboole_0(B,A)) % 0.57/0.81 & v3_membered(k3_xboole_0(B,A)) % 0.57/0.81 & v4_membered(k3_xboole_0(B,A)) % 0.57/0.81 & v5_membered(k3_xboole_0(B,A)) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(fc6_membered,axiom, % 0.57/0.81 ( v1_xboole_0(k1_xboole_0) % 0.57/0.81 & v1_membered(k1_xboole_0) % 0.57/0.81 & v2_membered(k1_xboole_0) % 0.57/0.81 & v3_membered(k1_xboole_0) % 0.57/0.81 & v4_membered(k1_xboole_0) % 0.57/0.81 & v5_membered(k1_xboole_0) ) ). % 0.57/0.81 % 0.57/0.81 fof(rc1_membered,axiom, % 0.57/0.81 ? [A] : % 0.57/0.81 ( ~ v1_xboole_0(A) % 0.57/0.81 & v1_membered(A) % 0.57/0.81 & v2_membered(A) % 0.57/0.81 & v3_membered(A) % 0.57/0.81 & v4_membered(A) % 0.57/0.81 & v5_membered(A) ) ). % 0.57/0.81 % 0.57/0.81 fof(rc1_tops_1,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( ( v2_pre_topc(A) % 0.57/0.81 & l1_pre_topc(A) ) % 0.57/0.81 => ? [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.81 & v3_pre_topc(B,A) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(rc2_tops_1,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( ( v2_pre_topc(A) % 0.57/0.81 & l1_pre_topc(A) ) % 0.57/0.81 => ? [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.81 & v3_pre_topc(B,A) % 0.57/0.81 & v4_pre_topc(B,A) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(rc3_tops_1,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( ( ~ v3_struct_0(A) % 0.57/0.81 & v2_pre_topc(A) % 0.57/0.81 & l1_pre_topc(A) ) % 0.57/0.81 => ? [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.81 & ~ v1_xboole_0(B) % 0.57/0.81 & v3_pre_topc(B,A) % 0.57/0.81 & v4_pre_topc(B,A) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(rc4_tops_1,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( l1_pre_topc(A) % 0.57/0.81 => ? [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.81 & v1_xboole_0(B) % 0.57/0.81 & v1_membered(B) % 0.57/0.81 & v2_membered(B) % 0.57/0.81 & v3_membered(B) % 0.57/0.81 & v4_membered(B) % 0.57/0.81 & v5_membered(B) % 0.57/0.81 & v2_tops_1(B,A) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(rc5_tops_1,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( ( v2_pre_topc(A) % 0.57/0.81 & l1_pre_topc(A) ) % 0.57/0.81 => ? [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.81 & v1_xboole_0(B) % 0.57/0.81 & v3_pre_topc(B,A) % 0.57/0.81 & v4_pre_topc(B,A) % 0.57/0.81 & v1_membered(B) % 0.57/0.81 & v2_membered(B) % 0.57/0.81 & v3_membered(B) % 0.57/0.81 & v4_membered(B) % 0.57/0.81 & v5_membered(B) % 0.57/0.81 & v2_tops_1(B,A) % 0.57/0.81 & v3_tops_1(B,A) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(t1_subset,axiom, % 0.57/0.81 ! [A,B] : % 0.57/0.81 ( r2_hidden(A,B) % 0.57/0.81 => m1_subset_1(A,B) ) ). % 0.57/0.81 % 0.57/0.81 fof(t2_boole,axiom, % 0.57/0.81 ! [A] : k3_xboole_0(A,k1_xboole_0) = k1_xboole_0 ). % 0.57/0.81 % 0.57/0.81 fof(t4_subset,axiom, % 0.57/0.81 ! [A,B,C] : % 0.57/0.81 ( ( r2_hidden(A,B) % 0.57/0.81 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 0.57/0.81 => m1_subset_1(A,C) ) ). % 0.57/0.81 % 0.57/0.81 fof(t5_subset,axiom, % 0.57/0.81 ! [A,B,C] : % 0.57/0.81 ~ ( r2_hidden(A,B) % 0.57/0.81 & m1_subset_1(B,k1_zfmisc_1(C)) % 0.57/0.81 & v1_xboole_0(C) ) ). % 0.57/0.81 % 0.57/0.81 fof(commutativity_k3_xboole_0,axiom, % 0.57/0.81 ! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A) ). % 0.57/0.81 % 0.57/0.81 fof(idempotence_k3_xboole_0,axiom, % 0.57/0.81 ! [A,B] : k3_xboole_0(A,A) = A ). % 0.57/0.81 % 0.57/0.81 fof(reflexivity_r1_tarski,axiom, % 0.57/0.81 ! [A,B] : r1_tarski(A,A) ). % 0.57/0.81 % 0.57/0.81 fof(existence_l1_struct_0,axiom, % 0.57/0.81 ? [A] : l1_struct_0(A) ). % 0.57/0.81 % 0.57/0.81 fof(dt_k3_xboole_0,axiom, % 0.57/0.81 $true ). % 0.57/0.81 % 0.57/0.81 fof(dt_l1_struct_0,axiom, % 0.57/0.81 $true ). % 0.57/0.81 % 0.57/0.81 fof(cc15_membered,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( v1_xboole_0(A) % 0.57/0.81 => ( v1_membered(A) % 0.57/0.81 & v2_membered(A) % 0.57/0.81 & v3_membered(A) % 0.57/0.81 & v4_membered(A) % 0.57/0.81 & v5_membered(A) ) ) ). % 0.57/0.81 % 0.57/0.81 fof(cc1_tops_1,axiom, % 0.57/0.81 ! [A] : % 0.57/0.81 ( ( v2_pre_topc(A) % 0.57/0.81 & l1_pre_topc(A) ) % 0.57/0.81 => ! [B] : % 0.57/0.81 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.81 => ( v1_xboole_0(B) % 0.57/0.82 => ( v3_pre_topc(B,A) % 0.57/0.82 & v4_pre_topc(B,A) ) ) ) ) ). % 0.57/0.82 % 0.57/0.82 fof(cc2_tops_1,axiom, % 0.57/0.82 ! [A] : % 0.57/0.82 ( l1_pre_topc(A) % 0.57/0.82 => ! [B] : % 0.57/0.82 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.82 => ( v1_xboole_0(B) % 0.57/0.82 => v2_tops_1(B,A) ) ) ) ). % 0.57/0.82 % 0.57/0.82 fof(cc3_tops_1,axiom, % 0.57/0.82 ! [A] : % 0.57/0.82 ( ( v2_pre_topc(A) % 0.57/0.82 & l1_pre_topc(A) ) % 0.57/0.82 => ! [B] : % 0.57/0.82 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.82 => ( v1_xboole_0(B) % 0.57/0.82 => v3_tops_1(B,A) ) ) ) ). % 0.57/0.82 % 0.57/0.82 fof(fc1_struct_0,axiom, % 0.57/0.82 ! [A] : % 0.57/0.82 ( ( ~ v3_struct_0(A) % 0.57/0.82 & l1_struct_0(A) ) % 0.57/0.82 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 0.57/0.82 % 0.57/0.82 fof(rc1_subset_1,axiom, % 0.57/0.82 ! [A] : % 0.57/0.82 ( ~ v1_xboole_0(A) % 0.57/0.82 => ? [B] : % 0.57/0.82 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.57/0.82 & ~ v1_xboole_0(B) ) ) ). % 0.57/0.82 % 0.57/0.82 fof(rc2_subset_1,axiom, % 0.57/0.82 ! [A] : % 0.57/0.82 ? [B] : % 0.57/0.82 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.57/0.82 & v1_xboole_0(B) ) ). % 0.57/0.82 % 0.57/0.82 fof(rc3_struct_0,axiom, % 0.57/0.82 ? [A] : % 0.57/0.82 ( l1_struct_0(A) % 0.57/0.82 & ~ v3_struct_0(A) ) ). % 0.57/0.82 % 0.57/0.82 fof(rc5_struct_0,axiom, % 0.57/0.82 ! [A] : % 0.57/0.82 ( ( ~ v3_struct_0(A) % 0.57/0.82 & l1_struct_0(A) ) % 0.57/0.82 => ? [B] : % 0.57/0.82 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.82 & ~ v1_xboole_0(B) ) ) ). % 0.57/0.82 % 0.57/0.82 fof(rc7_pre_topc,axiom, % 0.57/0.82 ! [A] : % 0.57/0.82 ( ( ~ v3_struct_0(A) % 0.57/0.82 & v2_pre_topc(A) % 0.57/0.82 & l1_pre_topc(A) ) % 0.57/0.82 => ? [B] : % 0.57/0.82 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.82 & ~ v1_xboole_0(B) % 0.57/0.82 & v4_pre_topc(B,A) ) ) ). % 0.57/0.82 % 0.57/0.82 fof(t2_subset,axiom, % 0.57/0.82 ! [A,B] : % 0.57/0.82 ( m1_subset_1(A,B) % 0.57/0.82 => ( v1_xboole_0(B) % 0.57/0.82 | r2_hidden(A,B) ) ) ). % 0.57/0.82 % 0.57/0.82 fof(t6_boole,axiom, % 0.57/0.82 ! [A] : % 0.57/0.82 ( v1_xboole_0(A) % 0.57/0.82 => A = k1_xboole_0 ) ). % 0.57/0.82 % 0.57/0.82 fof(t7_boole,axiom, % 0.57/0.82 ! [A,B] : % 0.57/0.82 ~ ( r2_hidden(A,B) % 0.57/0.82 & v1_xboole_0(B) ) ). % 0.57/0.82 % 0.57/0.82 fof(t8_boole,axiom, % 0.57/0.82 ! [A,B] : % 0.57/0.82 ~ ( v1_xboole_0(A) % 0.57/0.82 & A != B % 0.57/0.82 & v1_xboole_0(B) ) ). % 0.57/0.82 % 0.57/0.82 fof(commutativity_k5_subset_1,axiom, % 0.57/0.82 ! [A,B,C] : % 0.57/0.82 ( ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.57/0.82 & m1_subset_1(C,k1_zfmisc_1(A)) ) % 0.57/0.82 => k5_subset_1(A,B,C) = k5_subset_1(A,C,B) ) ). % 0.57/0.82 % 0.57/0.82 fof(idempotence_k5_subset_1,axiom, % 0.57/0.82 ! [A,B,C] : % 0.57/0.82 ( ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.57/0.82 & m1_subset_1(C,k1_zfmisc_1(A)) ) % 0.57/0.82 => k5_subset_1(A,B,B) = B ) ). % 0.57/0.82 % 0.57/0.82 fof(existence_l1_pre_topc,axiom, % 0.57/0.82 ? [A] : l1_pre_topc(A) ). % 0.57/0.82 % 0.57/0.82 fof(existence_m1_subset_1,axiom, % 0.57/0.82 ! [A] : % 0.57/0.82 ? [B] : m1_subset_1(B,A) ). % 0.57/0.82 % 0.57/0.82 fof(redefinition_k5_subset_1,axiom, % 0.57/0.82 ! [A,B,C] : % 0.57/0.82 ( ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.57/0.82 & m1_subset_1(C,k1_zfmisc_1(A)) ) % 0.57/0.82 => k5_subset_1(A,B,C) = k3_xboole_0(B,C) ) ). % 0.57/0.82 % 0.57/0.82 fof(dt_k1_zfmisc_1,axiom, % 0.57/0.82 $true ). % 0.57/0.82 % 0.57/0.82 fof(dt_k3_tex_4,axiom, % 0.57/0.82 ! [A,B] : % 0.57/0.82 ( ( ~ v3_struct_0(A) % 0.57/0.82 & l1_pre_topc(A) % 0.57/0.82 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 0.57/0.82 => m1_subset_1(k3_tex_4(A,B),k1_zfmisc_1(u1_struct_0(A))) ) ). % 0.57/0.82 % 0.57/0.82 fof(dt_k5_subset_1,axiom, % 0.57/0.82 ! [A,B,C] : % 0.57/0.82 ( ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.57/0.82 & m1_subset_1(C,k1_zfmisc_1(A)) ) % 0.57/0.82 => m1_subset_1(k5_subset_1(A,B,C),k1_zfmisc_1(A)) ) ). % 0.57/0.82 % 0.57/0.82 fof(dt_k6_pre_topc,axiom, % 0.57/0.82 ! [A,B] : % 0.57/0.82 ( ( l1_pre_topc(A) % 0.57/0.82 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 0.57/0.82 => m1_subset_1(k6_pre_topc(A,B),k1_zfmisc_1(u1_struct_0(A))) ) ). % 0.57/0.82 % 0.57/0.82 fof(dt_l1_pre_topc,axiom, % 0.57/0.82 ! [A] : % 0.57/0.82 ( l1_pre_topc(A) % 0.57/0.82 => l1_struct_0(A) ) ). % 0.57/0.82 % 0.57/0.82 fof(dt_m1_subset_1,axiom, % 0.57/0.82 $true ). % 0.57/0.82 % 0.57/0.82 fof(dt_u1_struct_0,axiom, % 0.57/0.82 $true ). % 0.57/0.82 % 0.57/0.82 fof(fc1_subset_1,axiom, % 0.57/0.82 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 0.57/0.82 % 0.57/0.82 fof(fc2_tops_1,axiom, % 0.57/0.82 ! [A,B] : % 0.57/0.82 ( ( v2_pre_topc(A) % 0.57/0.82 & l1_pre_topc(A) % 0.57/0.82 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 0.57/0.82 => v4_pre_topc(k6_pre_topc(A,B),A) ) ). % 0.57/0.82 % 0.57/0.82 fof(rc6_pre_topc,axiom, % 0.57/0.82 ! [A] : % 0.57/0.82 ( ( v2_pre_topc(A) % 0.57/0.82 & l1_pre_topc(A) ) % 0.57/0.82 => ? [B] : % 0.57/0.82 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.82 & v4_pre_topc(B,A) ) ) ). % 0.57/0.82 % 0.57/0.82 fof(t3_subset,axiom, % 0.57/0.82 ! [A,B] : % 0.57/0.82 ( m1_subset_1(A,k1_zfmisc_1(B)) % 0.57/0.82 <=> r1_tarski(A,B) ) ). % 0.57/0.82 % 0.57/0.82 fof(t5_tsp_2,axiom, % 0.57/0.82 ! [A] : % 0.57/0.82 ( ( ~ v3_struct_0(A) % 0.57/0.82 & v2_pre_topc(A) % 0.57/0.82 & l1_pre_topc(A) ) % 0.57/0.82 => ! [B] : % 0.57/0.82 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.82 => ( v1_tsp_2(B,A) % 0.57/0.82 => ! [C] : % 0.57/0.82 ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.82 => ( v4_pre_topc(C,A) % 0.57/0.82 => C = k3_tex_4(A,k5_subset_1(u1_struct_0(A),B,C)) ) ) ) ) ) ). % 0.57/0.82 % 0.57/0.82 %------------------------------------------------------------------------------ % 0.57/0.82 %------------------------------------------- % 0.57/0.82 % Proof found % 0.57/0.82 % SZS status Theorem for theBenchmark % 0.57/0.82 % SZS output start Proof % 0.57/0.82 %ClaNum:227(EqnAxiom:56) % 0.57/0.82 %VarNum:599(SingletonVarNum:245) % 0.57/0.82 %MaxLitNum:8 % 0.57/0.82 %MaxfuncDepth:3 % 0.57/0.82 %SharedTerms:36 % 0.57/0.82 %goalClause: 57 58 74 79 80 83 87 % 0.57/0.82 %singleGoalClaCount:7 % 0.57/0.82 [57]P1(a1) % 0.57/0.82 [58]P2(a1) % 0.57/0.82 [59]P2(a2) % 0.57/0.82 [60]P3(a11) % 0.57/0.82 [61]P3(a12) % 0.57/0.82 [62]P9(a11) % 0.57/0.82 [63]P9(a12) % 0.57/0.82 [64]P15(a11) % 0.57/0.82 [65]P15(a12) % 0.57/0.82 [66]P17(a11) % 0.57/0.82 [67]P17(a12) % 0.57/0.82 [68]P21(a11) % 0.57/0.82 [69]P21(a12) % 0.57/0.82 [70]P10(a11) % 0.57/0.82 [71]P4(a3) % 0.57/0.82 [72]P4(a4) % 0.57/0.82 [74]P11(a13,a1) % 0.57/0.82 [83]~P18(a1) % 0.57/0.82 [84]~P18(a4) % 0.57/0.82 [85]~P10(a12) % 0.57/0.82 [79]P6(a13,f21(f23(a1))) % 0.57/0.82 [80]P6(a14,f21(f23(a1))) % 0.57/0.82 [87]~E(f22(a1,f25(f23(a1),a13,f24(a1,a14))),f24(a1,a14)) % 0.57/0.82 [76]P5(x761,x761) % 0.57/0.82 [73]P10(f5(x731)) % 0.57/0.82 [75]E(f20(x751,a11),a11) % 0.57/0.82 [77]E(f20(x771,x771),x771) % 0.57/0.82 [78]P6(f9(x781),x781) % 0.57/0.82 [81]P6(f5(x811),f21(x811)) % 0.57/0.82 [86]~P10(f21(x861)) % 0.57/0.82 [82]E(f20(x821,x822),f20(x822,x821)) % 0.57/0.82 [88]~P10(x881)+E(x881,a11) % 0.57/0.82 [89]~P9(x891)+P3(x891) % 0.57/0.82 [90]~P10(x901)+P3(x901) % 0.57/0.82 [91]~P15(x911)+P9(x911) % 0.57/0.82 [92]~P10(x921)+P9(x921) % 0.57/0.82 [93]~P17(x931)+P15(x931) % 0.57/0.82 [94]~P10(x941)+P15(x941) % 0.57/0.82 [95]~P21(x951)+P17(x951) % 0.57/0.82 [96]~P10(x961)+P17(x961) % 0.57/0.82 [97]~P10(x971)+P21(x971) % 0.57/0.82 [98]~P2(x981)+P4(x981) % 0.57/0.82 [100]~P2(x1001)+P3(f15(x1001)) % 0.57/0.82 [101]~P2(x1011)+P9(f15(x1011)) % 0.57/0.82 [102]~P2(x1021)+P15(f15(x1021)) % 0.57/0.82 [103]~P2(x1031)+P17(f15(x1031)) % 0.57/0.82 [104]~P2(x1041)+P21(f15(x1041)) % 0.57/0.82 [105]~P2(x1051)+P10(f15(x1051)) % 0.57/0.82 [106]P10(x1061)+~P10(f6(x1061)) % 0.57/0.82 [113]~P2(x1131)+P16(f15(x1131),x1131) % 0.57/0.82 [117]P10(x1171)+P6(f6(x1171),f21(x1171)) % 0.57/0.82 [195]~P2(x1951)+P6(f15(x1951),f21(f23(x1951))) % 0.57/0.82 [116]~P10(x1161)+~P7(x1162,x1161) % 0.57/0.82 [143]~P7(x1431,x1432)+P6(x1431,x1432) % 0.57/0.82 [194]~P7(x1942,x1941)+~P7(x1941,x1942) % 0.57/0.82 [144]~P3(x1442)+P3(f20(x1441,x1442)) % 0.57/0.82 [145]~P3(x1451)+P3(f20(x1451,x1452)) % 0.57/0.82 [146]~P9(x1462)+P3(f20(x1461,x1462)) % 0.57/0.82 [147]~P9(x1471)+P3(f20(x1471,x1472)) % 0.57/0.82 [148]~P15(x1482)+P3(f20(x1481,x1482)) % 0.57/0.82 [149]~P15(x1491)+P3(f20(x1491,x1492)) % 0.57/0.82 [150]~P17(x1502)+P3(f20(x1501,x1502)) % 0.57/0.82 [151]~P17(x1511)+P3(f20(x1511,x1512)) % 0.57/0.82 [152]~P21(x1522)+P3(f20(x1521,x1522)) % 0.57/0.82 [153]~P21(x1531)+P3(f20(x1531,x1532)) % 0.57/0.82 [154]~P9(x1542)+P9(f20(x1541,x1542)) % 0.57/0.82 [155]~P9(x1551)+P9(f20(x1551,x1552)) % 0.57/0.82 [156]~P15(x1562)+P9(f20(x1561,x1562)) % 0.57/0.82 [157]~P15(x1571)+P9(f20(x1571,x1572)) % 0.57/0.82 [158]~P17(x1582)+P9(f20(x1581,x1582)) % 0.57/0.82 [159]~P17(x1591)+P9(f20(x1591,x1592)) % 0.57/0.82 [160]~P21(x1602)+P9(f20(x1601,x1602)) % 0.57/0.82 [161]~P21(x1611)+P9(f20(x1611,x1612)) % 0.57/0.82 [162]~P15(x1622)+P15(f20(x1621,x1622)) % 0.57/0.82 [163]~P15(x1631)+P15(f20(x1631,x1632)) % 0.57/0.82 [164]~P17(x1642)+P15(f20(x1641,x1642)) % 0.57/0.82 [165]~P17(x1651)+P15(f20(x1651,x1652)) % 0.57/0.82 [166]~P21(x1662)+P15(f20(x1661,x1662)) % 0.57/0.82 [167]~P21(x1671)+P15(f20(x1671,x1672)) % 0.57/0.82 [168]~P17(x1682)+P17(f20(x1681,x1682)) % 0.57/0.82 [169]~P17(x1691)+P17(f20(x1691,x1692)) % 0.57/0.82 [170]~P21(x1702)+P17(f20(x1701,x1702)) % 0.57/0.82 [171]~P21(x1711)+P17(f20(x1711,x1712)) % 0.57/0.82 [172]~P21(x1722)+P21(f20(x1721,x1722)) % 0.57/0.82 [173]~P21(x1731)+P21(f20(x1731,x1732)) % 0.57/0.82 [178]~P5(x1781,x1782)+P6(x1781,f21(x1782)) % 0.57/0.82 [196]P5(x1961,x1962)+~P6(x1961,f21(x1962)) % 0.57/0.82 [107]~P1(x1071)+~P2(x1071)+P3(f19(x1071)) % 0.57/0.82 [108]~P1(x1081)+~P2(x1081)+P9(f19(x1081)) % 0.57/0.82 [109]~P1(x1091)+~P2(x1091)+P15(f19(x1091)) % 0.57/0.82 [110]~P1(x1101)+~P2(x1101)+P17(f19(x1101)) % 0.57/0.82 [111]~P1(x1111)+~P2(x1111)+P21(f19(x1111)) % 0.57/0.82 [112]~P1(x1121)+~P2(x1121)+P10(f19(x1121)) % 0.57/0.82 [114]~P4(x1141)+P18(x1141)+~P10(f23(x1141)) % 0.57/0.82 [115]~P4(x1151)+P18(x1151)+~P10(f7(x1151)) % 0.57/0.82 [133]~P1(x1331)+~P2(x1331)+P20(f19(x1331),x1331) % 0.57/0.82 [134]~P1(x1341)+~P2(x1341)+P16(f19(x1341),x1341) % 0.57/0.82 [135]~P1(x1351)+~P2(x1351)+P23(f16(x1351),x1351) % 0.57/0.82 [136]~P1(x1361)+~P2(x1361)+P23(f19(x1361),x1361) % 0.57/0.82 [137]~P1(x1371)+~P2(x1371)+P23(f10(x1371),x1371) % 0.57/0.82 [138]~P1(x1381)+~P2(x1381)+P19(f17(x1381),x1381) % 0.57/0.82 [139]~P1(x1391)+~P2(x1391)+P19(f16(x1391),x1391) % 0.57/0.82 [140]~P1(x1401)+~P2(x1401)+P19(f19(x1401),x1401) % 0.57/0.82 [197]~P4(x1971)+P18(x1971)+P6(f7(x1971),f21(f23(x1971))) % 0.57/0.82 [198]~P1(x1981)+~P2(x1981)+P6(f17(x1981),f21(f23(x1981))) % 0.57/0.82 [199]~P1(x1991)+~P2(x1991)+P6(f16(x1991),f21(f23(x1991))) % 0.57/0.82 [200]~P1(x2001)+~P2(x2001)+P6(f19(x2001),f21(f23(x2001))) % 0.57/0.82 [201]~P1(x2011)+~P2(x2011)+P6(f10(x2011),f21(f23(x2011))) % 0.57/0.82 [99]~P10(x992)+~P10(x991)+E(x991,x992) % 0.57/0.82 [118]~P6(x1181,x1182)+P13(x1181)+~P3(x1182) % 0.57/0.82 [119]~P6(x1191,x1192)+P13(x1191)+~P9(x1192) % 0.57/0.82 [120]~P6(x1201,x1202)+P13(x1201)+~P15(x1202) % 0.57/0.82 [121]~P6(x1211,x1212)+P13(x1211)+~P17(x1212) % 0.57/0.82 [122]~P6(x1221,x1222)+P13(x1221)+~P21(x1222) % 0.57/0.82 [123]~P6(x1231,x1232)+P14(x1231)+~P9(x1232) % 0.57/0.82 [124]~P6(x1241,x1242)+P14(x1241)+~P15(x1242) % 0.57/0.82 [125]~P6(x1251,x1252)+P14(x1251)+~P17(x1252) % 0.57/0.82 [126]~P6(x1261,x1262)+P14(x1261)+~P21(x1262) % 0.57/0.82 [127]~P6(x1271,x1272)+P12(x1271)+~P15(x1272) % 0.57/0.82 [128]~P6(x1281,x1282)+P12(x1281)+~P17(x1282) % 0.57/0.82 [129]~P6(x1291,x1292)+P12(x1291)+~P21(x1292) % 0.57/0.82 [130]~P6(x1301,x1302)+P8(x1301)+~P17(x1302) % 0.57/0.82 [131]~P6(x1311,x1312)+P8(x1311)+~P21(x1312) % 0.57/0.82 [132]~P6(x1321,x1322)+P22(x1321)+~P21(x1322) % 0.57/0.82 [177]~P6(x1772,x1771)+P10(x1771)+P7(x1772,x1771) % 0.57/0.82 [179]P3(x1791)+~P3(x1792)+~P6(x1791,f21(x1792)) % 0.57/0.82 [180]P3(x1801)+~P9(x1802)+~P6(x1801,f21(x1802)) % 0.57/0.82 [181]P3(x1811)+~P15(x1812)+~P6(x1811,f21(x1812)) % 0.57/0.82 [182]P3(x1821)+~P17(x1822)+~P6(x1821,f21(x1822)) % 0.57/0.82 [183]P3(x1831)+~P21(x1832)+~P6(x1831,f21(x1832)) % 0.57/0.82 [184]P9(x1841)+~P9(x1842)+~P6(x1841,f21(x1842)) % 0.57/0.82 [185]P9(x1851)+~P15(x1852)+~P6(x1851,f21(x1852)) % 0.57/0.82 [186]P9(x1861)+~P17(x1862)+~P6(x1861,f21(x1862)) % 0.57/0.82 [187]P9(x1871)+~P21(x1872)+~P6(x1871,f21(x1872)) % 0.57/0.82 [188]P15(x1881)+~P15(x1882)+~P6(x1881,f21(x1882)) % 0.57/0.82 [189]P15(x1891)+~P17(x1892)+~P6(x1891,f21(x1892)) % 0.57/0.82 [190]P15(x1901)+~P21(x1902)+~P6(x1901,f21(x1902)) % 0.57/0.82 [191]P17(x1911)+~P17(x1912)+~P6(x1911,f21(x1912)) % 0.57/0.82 [192]P17(x1921)+~P21(x1922)+~P6(x1921,f21(x1922)) % 0.57/0.82 [193]P21(x1931)+~P21(x1932)+~P6(x1931,f21(x1932)) % 0.57/0.82 [218]~P2(x2181)+~P6(x2182,f21(f23(x2181)))+P6(f24(x2181,x2182),f21(f23(x2181))) % 0.57/0.82 [204]~P10(x2041)+~P7(x2042,x2043)+~P6(x2043,f21(x2041)) % 0.57/0.82 [205]P6(x2051,x2052)+~P7(x2051,x2053)+~P6(x2053,f21(x2052)) % 0.57/0.82 [219]~P6(x2192,f21(x2191))+E(f25(x2191,x2192,x2192),x2192)+~P6(x2193,f21(x2191)) % 0.57/0.82 [224]~P6(x2243,f21(x2241))+~P6(x2242,f21(x2241))+E(f25(x2241,x2242,x2243),f20(x2242,x2243)) % 0.57/0.82 [225]~P6(x2253,f21(x2251))+~P6(x2252,f21(x2251))+E(f25(x2251,x2252,x2253),f25(x2251,x2253,x2252)) % 0.57/0.82 [226]~P6(x2263,f21(x2261))+~P6(x2262,f21(x2261))+P6(f25(x2261,x2262,x2263),f21(x2261)) % 0.57/0.82 [141]~P1(x1411)+~P2(x1411)+P18(x1411)+~P10(f18(x1411)) % 0.57/0.82 [142]~P1(x1421)+~P2(x1421)+P18(x1421)+~P10(f8(x1421)) % 0.57/0.82 [174]~P1(x1741)+~P2(x1741)+P18(x1741)+P23(f18(x1741),x1741) % 0.57/0.82 [175]~P1(x1751)+~P2(x1751)+P18(x1751)+P23(f8(x1751),x1751) % 0.57/0.82 [176]~P1(x1761)+~P2(x1761)+P18(x1761)+P19(f18(x1761),x1761) % 0.57/0.82 [202]~P1(x2021)+~P2(x2021)+P18(x2021)+P6(f18(x2021),f21(f23(x2021))) % 0.57/0.82 [203]~P1(x2031)+~P2(x2031)+P18(x2031)+P6(f8(x2031),f21(f23(x2031))) % 0.57/0.82 [206]~P2(x2062)+~P10(x2061)+P16(x2061,x2062)+~P6(x2061,f21(f23(x2062))) % 0.57/0.82 [211]~P1(x2111)+~P2(x2111)+P23(f24(x2111,x2112),x2111)+~P6(x2112,f21(f23(x2111))) % 0.57/0.82 [220]~P2(x2201)+P18(x2201)+~P6(x2202,f21(f23(x2201)))+P6(f22(x2201,x2202),f21(f23(x2201))) % 0.57/0.82 [207]~P1(x2072)+~P2(x2072)+~P10(x2071)+P20(x2071,x2072)+~P6(x2071,f21(f23(x2072))) % 0.57/0.82 [208]~P1(x2082)+~P2(x2082)+~P10(x2081)+P23(x2081,x2082)+~P6(x2081,f21(f23(x2082))) % 0.57/0.82 [209]~P1(x2092)+~P2(x2092)+~P10(x2091)+P19(x2091,x2092)+~P6(x2091,f21(f23(x2092))) % 0.57/0.82 [210]~P1(x2102)+~P2(x2102)+~P20(x2101,x2102)+P16(x2101,x2102)+~P6(x2101,f21(f23(x2102))) % 0.57/0.82 [212]~P2(x2122)+~P20(x2121,x2122)+~P19(x2121,x2122)+P3(x2121)+~P1(x2122)+~P6(x2121,f21(f23(x2122))) % 0.57/0.82 [213]~P2(x2132)+~P20(x2131,x2132)+~P19(x2131,x2132)+P9(x2131)+~P1(x2132)+~P6(x2131,f21(f23(x2132))) % 0.57/0.82 [214]~P2(x2142)+~P20(x2141,x2142)+~P19(x2141,x2142)+P15(x2141)+~P1(x2142)+~P6(x2141,f21(f23(x2142))) % 0.57/0.82 [215]~P2(x2152)+~P20(x2151,x2152)+~P19(x2151,x2152)+P17(x2151)+~P1(x2152)+~P6(x2151,f21(f23(x2152))) % 0.57/0.82 [216]~P2(x2162)+~P20(x2161,x2162)+~P19(x2161,x2162)+P21(x2161)+~P1(x2162)+~P6(x2161,f21(f23(x2162))) % 0.57/0.82 [217]~P2(x2172)+~P20(x2171,x2172)+~P19(x2171,x2172)+P10(x2171)+~P1(x2172)+~P6(x2171,f21(f23(x2172))) % 0.57/0.82 [221]~P1(x2212)+~P2(x2212)+~P16(x2211,x2212)+~P23(x2211,x2212)+P20(x2211,x2212)+~P6(x2211,f21(f23(x2212))) % 0.57/0.82 [223]~P1(x2232)+~P2(x2232)+~P20(x2231,x2232)+~P19(x2231,x2232)+P23(x2231,x2232)+~P6(x2231,f21(f23(x2232))) % 0.57/0.82 [227]P18(x2271)+~P1(x2271)+~P2(x2271)+~P11(x2272,x2271)+~P23(x2273,x2271)+~P6(x2273,f21(f23(x2271)))+~P6(x2272,f21(f23(x2271)))+E(f22(x2271,f25(f23(x2271),x2272,x2273)),x2273) % 0.57/0.82 %EqnAxiom % 0.57/0.82 [1]E(x11,x11) % 0.57/0.82 [2]E(x22,x21)+~E(x21,x22) % 0.57/0.82 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.57/0.82 [4]~E(x41,x42)+E(f5(x41),f5(x42)) % 0.57/0.82 [5]~E(x51,x52)+E(f20(x51,x53),f20(x52,x53)) % 0.57/0.82 [6]~E(x61,x62)+E(f20(x63,x61),f20(x63,x62)) % 0.57/0.82 [7]~E(x71,x72)+E(f23(x71),f23(x72)) % 0.57/0.82 [8]~E(x81,x82)+E(f9(x81),f9(x82)) % 0.57/0.82 [9]~E(x91,x92)+E(f21(x91),f21(x92)) % 0.57/0.82 [10]~E(x101,x102)+E(f8(x101),f8(x102)) % 0.57/0.82 [11]~E(x111,x112)+E(f24(x111,x113),f24(x112,x113)) % 0.57/0.82 [12]~E(x121,x122)+E(f24(x123,x121),f24(x123,x122)) % 0.57/0.82 [13]~E(x131,x132)+E(f18(x131),f18(x132)) % 0.57/0.82 [14]~E(x141,x142)+E(f10(x141),f10(x142)) % 0.57/0.82 [15]~E(x151,x152)+E(f19(x151),f19(x152)) % 0.57/0.82 [16]~E(x161,x162)+E(f16(x161),f16(x162)) % 0.57/0.82 [17]~E(x171,x172)+E(f17(x171),f17(x172)) % 0.57/0.82 [18]~E(x181,x182)+E(f7(x181),f7(x182)) % 0.57/0.82 [19]~E(x191,x192)+E(f15(x191),f15(x192)) % 0.57/0.82 [20]~E(x201,x202)+E(f25(x201,x203,x204),f25(x202,x203,x204)) % 0.57/0.82 [21]~E(x211,x212)+E(f25(x213,x211,x214),f25(x213,x212,x214)) % 0.57/0.82 [22]~E(x221,x222)+E(f25(x223,x224,x221),f25(x223,x224,x222)) % 0.57/0.82 [23]~E(x231,x232)+E(f22(x231,x233),f22(x232,x233)) % 0.57/0.82 [24]~E(x241,x242)+E(f22(x243,x241),f22(x243,x242)) % 0.57/0.82 [25]~E(x251,x252)+E(f6(x251),f6(x252)) % 0.57/0.82 [26]~P1(x261)+P1(x262)+~E(x261,x262) % 0.57/0.82 [27]~P2(x271)+P2(x272)+~E(x271,x272) % 0.57/0.82 [28]P6(x282,x283)+~E(x281,x282)+~P6(x281,x283) % 0.57/0.82 [29]P6(x293,x292)+~E(x291,x292)+~P6(x293,x291) % 0.57/0.82 [30]~P3(x301)+P3(x302)+~E(x301,x302) % 0.57/0.82 [31]~P21(x311)+P21(x312)+~E(x311,x312) % 0.57/0.82 [32]~P9(x321)+P9(x322)+~E(x321,x322) % 0.57/0.82 [33]~P15(x331)+P15(x332)+~E(x331,x332) % 0.57/0.82 [34]~P17(x341)+P17(x342)+~E(x341,x342) % 0.57/0.82 [35]~P10(x351)+P10(x352)+~E(x351,x352) % 0.57/0.82 [36]P19(x362,x363)+~E(x361,x362)+~P19(x361,x363) % 0.57/0.82 [37]P19(x373,x372)+~E(x371,x372)+~P19(x373,x371) % 0.57/0.82 [38]P23(x382,x383)+~E(x381,x382)+~P23(x381,x383) % 0.57/0.82 [39]P23(x393,x392)+~E(x391,x392)+~P23(x393,x391) % 0.57/0.82 [40]~P18(x401)+P18(x402)+~E(x401,x402) % 0.57/0.82 [41]P20(x412,x413)+~E(x411,x412)+~P20(x411,x413) % 0.57/0.82 [42]P20(x423,x422)+~E(x421,x422)+~P20(x423,x421) % 0.57/0.82 [43]~P12(x431)+P12(x432)+~E(x431,x432) % 0.57/0.82 [44]~P4(x441)+P4(x442)+~E(x441,x442) % 0.57/0.82 [45]P7(x452,x453)+~E(x451,x452)+~P7(x451,x453) % 0.57/0.82 [46]P7(x463,x462)+~E(x461,x462)+~P7(x463,x461) % 0.57/0.82 [47]~P14(x471)+P14(x472)+~E(x471,x472) % 0.57/0.82 [48]P11(x482,x483)+~E(x481,x482)+~P11(x481,x483) % 0.57/0.82 [49]P11(x493,x492)+~E(x491,x492)+~P11(x493,x491) % 0.57/0.82 [50]P5(x502,x503)+~E(x501,x502)+~P5(x501,x503) % 0.57/0.82 [51]P5(x513,x512)+~E(x511,x512)+~P5(x513,x511) % 0.57/0.82 [52]P16(x522,x523)+~E(x521,x522)+~P16(x521,x523) % 0.57/0.82 [53]P16(x533,x532)+~E(x531,x532)+~P16(x533,x531) % 0.57/0.82 [54]~P13(x541)+P13(x542)+~E(x541,x542) % 0.57/0.82 [55]~P8(x551)+P8(x552)+~E(x551,x552) % 0.57/0.82 [56]~P22(x561)+P22(x562)+~E(x561,x562) % 0.57/0.82 % 0.57/0.82 %------------------------------------------- % 0.57/0.82 cnf(228,plain, % 0.57/0.82 (P5(a13,f23(a1))), % 0.57/0.82 inference(scs_inference,[],[79,196])). % 0.57/0.82 cnf(230,plain, % 0.57/0.82 (E(x2301,f20(x2301,x2301))), % 0.57/0.82 inference(scs_inference,[],[79,77,196,2])). % 0.57/0.82 cnf(233,plain, % 0.57/0.82 (P7(f9(a12),a12)), % 0.57/0.82 inference(scs_inference,[],[79,78,77,70,85,196,2,116,177])). % 0.57/0.82 cnf(234,plain, % 0.57/0.82 (P6(f9(x2341),x2341)), % 0.57/0.82 inference(rename_variables,[],[78])). % 0.57/0.82 cnf(236,plain, % 0.57/0.82 (P3(f9(f21(a11)))), % 0.57/0.82 inference(scs_inference,[],[79,78,234,77,60,70,85,196,2,116,177,179])). % 0.57/0.82 cnf(237,plain, % 0.57/0.82 (P6(f9(x2371),x2371)), % 0.57/0.82 inference(rename_variables,[],[78])). % 0.57/0.82 cnf(240,plain, % 0.57/0.82 (P6(f5(x2401),f21(x2401))), % 0.57/0.82 inference(rename_variables,[],[81])). % 0.57/0.82 cnf(242,plain, % 0.57/0.82 (P9(f9(f21(a11)))), % 0.57/0.82 inference(scs_inference,[],[79,78,234,237,81,77,60,62,70,85,196,2,116,177,179,180,184])). % 0.57/0.82 cnf(243,plain, % 0.57/0.82 (P6(f9(x2431),x2431)), % 0.57/0.82 inference(rename_variables,[],[78])). % 0.57/0.82 cnf(246,plain, % 0.57/0.82 (P6(f5(x2461),f21(x2461))), % 0.57/0.82 inference(rename_variables,[],[81])). % 0.57/0.82 cnf(248,plain, % 0.57/0.82 (P15(f9(f21(a11)))), % 0.57/0.82 inference(scs_inference,[],[79,78,234,237,243,81,240,77,60,62,64,70,85,196,2,116,177,179,180,184,185,188])). % 0.57/0.82 cnf(249,plain, % 0.57/0.82 (P6(f9(x2491),x2491)), % 0.57/0.82 inference(rename_variables,[],[78])). % 0.57/0.82 cnf(252,plain, % 0.57/0.82 (P6(f5(x2521),f21(x2521))), % 0.57/0.82 inference(rename_variables,[],[81])). % 0.57/0.82 cnf(254,plain, % 0.57/0.82 (P17(f9(f21(a11)))), % 0.57/0.82 inference(scs_inference,[],[79,78,234,237,243,249,81,240,246,77,60,62,64,66,70,85,196,2,116,177,179,180,184,185,188,189,191])). % 0.57/0.82 cnf(255,plain, % 0.57/0.82 (P6(f9(x2551),x2551)), % 0.57/0.82 inference(rename_variables,[],[78])). % 0.57/0.82 cnf(258,plain, % 0.57/0.82 (P6(f5(x2581),f21(x2581))), % 0.57/0.82 inference(rename_variables,[],[81])). % 0.57/0.82 cnf(260,plain, % 0.57/0.82 (P21(f9(f21(a11)))), % 0.57/0.82 inference(scs_inference,[],[79,78,234,237,243,249,255,81,240,246,252,77,60,62,64,66,68,70,85,196,2,116,177,179,180,184,185,188,189,191,192,193])). % 0.57/0.82 cnf(261,plain, % 0.57/0.82 (P6(f9(x2611),x2611)), % 0.57/0.82 inference(rename_variables,[],[78])). % 0.57/0.82 cnf(263,plain, % 0.57/0.82 (~P7(x2631,f9(f21(a11)))), % 0.57/0.82 inference(scs_inference,[],[79,78,234,237,243,249,255,261,81,240,246,252,77,60,62,64,66,68,70,85,196,2,116,177,179,180,184,185,188,189,191,192,193,204])). % 0.57/0.82 cnf(264,plain, % 0.57/0.82 (P6(f9(x2641),x2641)), % 0.57/0.82 inference(rename_variables,[],[78])). % 0.57/0.82 cnf(267,plain, % 0.57/0.82 (E(f20(x2671,x2671),x2671)), % 0.57/0.82 inference(rename_variables,[],[77])). % 0.57/0.82 cnf(268,plain, % 0.57/0.82 (P6(f9(f20(x2681,x2681)),x2681)), % 0.57/0.82 inference(scs_inference,[],[79,87,78,234,237,243,249,255,261,264,81,240,246,252,77,267,60,62,64,66,68,70,85,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29])). % 0.57/0.82 cnf(271,plain, % 0.57/0.82 (E(f20(x2711,x2711),x2711)), % 0.57/0.82 inference(rename_variables,[],[77])). % 0.57/0.82 cnf(272,plain, % 0.57/0.82 (~P10(f20(a12,a12))), % 0.57/0.82 inference(scs_inference,[],[83,79,87,78,234,237,243,249,255,261,264,81,240,246,252,77,267,271,60,62,64,66,68,70,85,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,40,35])). % 0.57/0.82 cnf(273,plain, % 0.57/0.82 (E(f20(x2731,x2731),x2731)), % 0.57/0.82 inference(rename_variables,[],[77])). % 0.57/0.82 cnf(274,plain, % 0.57/0.82 (~E(a12,a11)), % 0.57/0.82 inference(scs_inference,[],[83,79,87,78,234,237,243,249,255,261,264,81,240,246,252,77,267,271,60,62,64,66,68,70,85,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,40,35,46])). % 0.57/0.82 cnf(276,plain, % 0.57/0.82 (P5(x2761,x2761)), % 0.57/0.82 inference(rename_variables,[],[76])). % 0.57/0.82 cnf(279,plain, % 0.57/0.82 (P16(f5(f23(a1)),a1)), % 0.57/0.82 inference(scs_inference,[],[58,83,79,87,78,234,237,243,249,255,261,264,81,240,246,252,258,76,276,77,267,271,273,60,62,64,66,68,70,85,73,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,40,35,46,50,51,206])). % 0.57/0.82 cnf(280,plain, % 0.57/0.82 (P6(f5(x2801),f21(x2801))), % 0.57/0.82 inference(rename_variables,[],[81])). % 0.57/0.82 cnf(281,plain, % 0.57/0.82 (P10(f5(x2811))), % 0.57/0.82 inference(rename_variables,[],[73])). % 0.57/0.82 cnf(285,plain, % 0.57/0.82 (P20(f5(f23(a1)),a1)), % 0.57/0.82 inference(scs_inference,[],[57,58,83,79,87,78,234,237,243,249,255,261,264,81,240,246,252,258,280,76,276,77,267,271,273,60,62,64,66,68,70,85,73,281,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,40,35,46,50,51,206,211,207])). % 0.57/0.82 cnf(286,plain, % 0.57/0.82 (P6(f5(x2861),f21(x2861))), % 0.57/0.82 inference(rename_variables,[],[81])). % 0.57/0.82 cnf(287,plain, % 0.57/0.82 (P10(f5(x2871))), % 0.57/0.82 inference(rename_variables,[],[73])). % 0.57/0.82 cnf(289,plain, % 0.57/0.82 (P23(f5(f23(a1)),a1)), % 0.57/0.82 inference(scs_inference,[],[57,58,83,79,87,78,234,237,243,249,255,261,264,81,240,246,252,258,280,286,76,276,77,267,271,273,60,62,64,66,68,70,85,73,281,287,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,40,35,46,50,51,206,211,207,208])). % 0.57/0.82 cnf(290,plain, % 0.57/0.82 (P6(f5(x2901),f21(x2901))), % 0.57/0.82 inference(rename_variables,[],[81])). % 0.57/0.82 cnf(291,plain, % 0.57/0.82 (P10(f5(x2911))), % 0.57/0.82 inference(rename_variables,[],[73])). % 0.57/0.82 cnf(293,plain, % 0.57/0.82 (P19(f5(f23(a1)),a1)), % 0.57/0.82 inference(scs_inference,[],[57,58,83,79,87,78,234,237,243,249,255,261,264,81,240,246,252,258,280,286,290,76,276,77,267,271,273,60,62,64,66,68,70,85,73,281,287,291,196,2,116,177,179,180,184,185,188,189,191,192,193,204,3,29,40,35,46,50,51,206,211,207,208,209])). % 0.57/0.82 cnf(332,plain, % 0.57/0.82 (E(x3321,f20(x3321,x3321))), % 0.57/0.82 inference(rename_variables,[],[230])). % 0.57/0.82 cnf(334,plain, % 0.57/0.82 (E(x3341,f20(x3341,x3341))), % 0.57/0.82 inference(rename_variables,[],[230])). % 0.57/0.82 cnf(335,plain, % 0.57/0.82 (P6(f20(a14,a14),f21(f23(a1)))), % 0.57/0.82 inference(scs_inference,[],[57,80,58,230,332,334,75,73,116,2,196,26,27,28])). % 0.57/0.82 cnf(336,plain, % 0.57/0.82 (E(x3361,f20(x3361,x3361))), % 0.57/0.82 inference(rename_variables,[],[230])). % 0.57/0.82 cnf(338,plain, % 0.57/0.82 (E(x3381,f20(x3381,x3381))), % 0.57/0.82 inference(rename_variables,[],[230])). % 0.57/0.82 cnf(340,plain, % 0.57/0.82 (E(x3401,f20(x3401,x3401))), % 0.57/0.82 inference(rename_variables,[],[230])). % 0.57/0.82 cnf(342,plain, % 0.57/0.82 (E(x3421,f20(x3421,x3421))), % 0.57/0.82 inference(rename_variables,[],[230])). % 0.57/0.82 cnf(344,plain, % 0.57/0.82 (E(x3441,f20(x3441,x3441))), % 0.57/0.82 inference(rename_variables,[],[230])). % 0.57/0.82 cnf(346,plain, % 0.57/0.82 (E(x3461,f20(x3461,x3461))), % 0.57/0.82 inference(rename_variables,[],[230])). % 0.57/0.82 cnf(348,plain, % 0.57/0.82 (E(x3481,f20(x3481,x3481))), % 0.57/0.82 inference(rename_variables,[],[230])). % 0.57/0.82 cnf(350,plain, % 0.57/0.82 (E(x3501,f20(x3501,x3501))), % 0.57/0.82 inference(rename_variables,[],[230])). % 0.57/0.82 cnf(352,plain, % 0.57/0.82 (E(x3521,f20(x3521,x3521))), % 0.57/0.82 inference(rename_variables,[],[230])). % 0.57/0.82 cnf(354,plain, % 0.57/0.83 (E(x3541,f20(x3541,x3541))), % 0.57/0.83 inference(rename_variables,[],[230])). % 0.57/0.83 cnf(356,plain, % 0.57/0.83 (E(x3561,f20(x3561,x3561))), % 0.57/0.83 inference(rename_variables,[],[230])). % 0.57/0.83 cnf(358,plain, % 0.57/0.83 (E(x3581,f20(x3581,x3581))), % 0.57/0.83 inference(rename_variables,[],[230])). % 0.57/0.83 cnf(360,plain, % 0.57/0.83 (E(x3601,f20(x3601,x3601))), % 0.57/0.83 inference(rename_variables,[],[230])). % 0.57/0.83 cnf(362,plain, % 0.57/0.83 (E(x3621,f20(x3621,x3621))), % 0.57/0.83 inference(rename_variables,[],[230])). % 0.57/0.83 cnf(364,plain, % 0.57/0.83 (E(x3641,f20(x3641,x3641))), % 0.57/0.83 inference(rename_variables,[],[230])). % 0.57/0.83 cnf(366,plain, % 0.57/0.83 (E(x3661,f20(x3661,x3661))), % 0.57/0.83 inference(rename_variables,[],[230])). % 0.57/0.83 cnf(368,plain, % 0.57/0.83 (E(x3681,f20(x3681,x3681))), % 0.57/0.83 inference(rename_variables,[],[230])). % 0.57/0.83 cnf(370,plain, % 0.57/0.83 (E(x3701,f20(x3701,x3701))), % 0.57/0.83 inference(rename_variables,[],[230])). % 0.57/0.83 cnf(372,plain, % 0.57/0.83 (P6(f5(x3721),f21(x3721))), % 0.57/0.83 inference(rename_variables,[],[81])). % 0.57/0.83 cnf(375,plain, % 0.57/0.83 (P6(f5(x3751),f21(x3751))), % 0.57/0.83 inference(rename_variables,[],[81])). % 0.57/0.83 cnf(378,plain, % 0.57/0.83 (P6(f5(x3781),f21(x3781))), % 0.57/0.83 inference(rename_variables,[],[81])). % 0.57/0.83 cnf(383,plain, % 0.57/0.83 (P7(f9(f20(f20(a12,a12),f20(a12,a12))),f20(a12,a12))), % 0.57/0.83 inference(scs_inference,[],[57,74,80,58,230,332,334,336,338,340,342,344,346,348,350,352,354,356,358,360,362,364,366,368,268,279,285,289,236,242,248,254,260,293,233,272,78,81,372,375,71,75,73,116,2,196,26,27,28,48,49,30,31,32,33,34,36,37,38,39,41,42,52,53,44,45,190,183,191,204,177])). % 0.57/0.83 cnf(387,plain, % 0.57/0.83 (P6(f5(x3871),f21(x3871))), % 0.57/0.83 inference(rename_variables,[],[81])). % 0.57/0.83 cnf(391,plain, % 0.57/0.83 (E(x3911,f20(x3911,x3911))), % 0.57/0.83 inference(rename_variables,[],[230])). % 0.57/0.83 cnf(396,plain, % 0.57/0.83 (E(x3961,f20(x3961,x3961))), % 0.57/0.83 inference(rename_variables,[],[230])). % 0.57/0.83 cnf(399,plain, % 0.57/0.83 (P10(f20(f5(x3991),f5(x3991)))), % 0.57/0.83 inference(scs_inference,[],[57,74,80,58,230,332,334,336,338,340,342,344,346,348,350,352,354,356,358,360,362,364,366,368,370,391,396,268,263,279,285,289,236,242,248,254,260,293,228,233,272,78,81,372,375,378,387,71,274,75,73,116,2,196,26,27,28,48,49,30,31,32,33,34,36,37,38,39,41,42,52,53,44,45,190,183,191,204,177,184,3,50,193,29,46,35])). % 0.57/0.83 cnf(400,plain, % 0.57/0.83 (E(x4001,f20(x4001,x4001))), % 0.57/0.83 inference(rename_variables,[],[230])). % 0.57/0.83 cnf(405,plain, % 0.57/0.83 (~P6(f24(a1,a14),f21(f23(a1)))), % 0.57/0.83 inference(scs_inference,[],[57,74,80,83,87,79,58,230,332,334,336,338,340,342,344,346,348,350,352,354,356,358,360,362,364,366,368,370,391,396,400,268,263,279,285,289,236,242,248,254,260,293,228,233,272,78,81,372,375,378,387,71,274,75,73,116,2,196,26,27,28,48,49,30,31,32,33,34,36,37,38,39,41,42,52,53,44,45,190,183,191,204,177,184,3,50,193,29,46,35,51,211,227])). % 0.57/0.83 cnf(426,plain, % 0.57/0.83 ($false), % 0.57/0.83 inference(scs_inference,[],[80,58,405,383,335,399,194,196,116,218]), % 0.57/0.83 ['proof']). % 0.57/0.83 % SZS output end Proof % 0.57/0.83 % Total time :0.110000s %------------------------------------------------------------------------------