%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT288+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 : n029.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 10:18:38 EDT 2024 % Result : Theorem 58.80s 58.85s % Output : CNFRefutation 58.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : LAT288+1 : TPTP v8.2.0. Released v3.4.0. % 0.00/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 19:49:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 58.73/58.82 %------------------------------------------- % 58.73/58.82 % File :CSE---1.7 % 58.73/58.82 % Problem :theBenchmark % 58.73/58.82 % Transform :cnf % 58.73/58.82 % Format :tptp:raw % 58.73/58.82 % Command :java -jar mcs_scs.jar %d %s % 58.73/58.82 % 58.73/58.82 % Result :Theorem 58.220000s % 58.73/58.82 % Output :CNFRefutation 58.220000s % 58.73/58.82 %------------------------------------------- % 58.80/58.83 %------------------------------------------------------------------------------ % 58.80/58.83 % File : LAT288+1 : TPTP v8.2.0. Released v3.4.0. % 58.80/58.83 % Domain : Lattice Theory % 58.80/58.83 % Problem : Representation Theorem for Boolean Algebras T19 % 58.80/58.83 % Version : [Urb08] axioms : Especial. % 58.80/58.83 % English : % 58.80/58.83 % 58.80/58.83 % Refs : [Wal93] Walijewski (1993), Representation Theorem for Boolean % 58.80/58.83 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 58.80/58.83 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 58.80/58.83 % Source : [Urb08] % 58.80/58.83 % Names : t19_lopclset [Urb08] % 58.80/58.83 % 58.80/58.83 % Status : Theorem % 58.80/58.83 % Rating : 0.44 v8.2.0, 0.42 v8.1.0, 0.39 v7.5.0, 0.41 v7.4.0, 0.33 v7.3.0, 0.34 v7.2.0, 0.31 v7.1.0, 0.26 v7.0.0, 0.37 v6.4.0, 0.38 v6.3.0, 0.33 v6.2.0, 0.40 v6.1.0, 0.53 v6.0.0, 0.52 v5.5.0, 0.56 v5.4.0, 0.61 v5.3.0, 0.63 v5.2.0, 0.50 v5.1.0, 0.52 v5.0.0, 0.54 v4.1.0, 0.52 v4.0.1, 0.57 v4.0.0, 0.58 v3.7.0, 0.55 v3.5.0, 0.63 v3.4.0 % 58.80/58.83 % Syntax : Number of formulae : 69 ( 11 unt; 0 def) % 58.80/58.83 % Number of atoms : 289 ( 6 equ) % 58.80/58.83 % Maximal formula atoms : 17 ( 4 avg) % 58.80/58.83 % Number of connectives : 269 ( 49 ~; 1 |; 146 &) % 58.80/58.83 % ( 5 <=>; 68 =>; 0 <=; 0 <~>) % 58.80/58.83 % Maximal formula depth : 19 ( 6 avg) % 58.80/58.83 % Maximal term depth : 4 ( 1 avg) % 58.80/58.83 % Number of predicates : 42 ( 40 usr; 1 prp; 0-2 aty) % 58.80/58.83 % Number of functors : 6 ( 6 usr; 1 con; 0-2 aty) % 58.80/58.83 % Number of variables : 101 ( 86 !; 15 ?) % 58.80/58.83 % SPC : FOF_THM_RFO_SEQ % 58.80/58.83 % 58.80/58.83 % Comments : Normal version: includes the axioms (which may be theorems from % 58.80/58.83 % other articles) and background that are possibly necessary. % 58.80/58.83 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 58.80/58.83 % : The problem encoding is based on set theory. % 58.80/58.83 %------------------------------------------------------------------------------ % 58.80/58.83 fof(t19_lopclset,conjecture, % 58.80/58.83 ! [A] : % 58.80/58.83 ( ( ~ v3_struct_0(A) % 58.80/58.83 & v10_lattices(A) % 58.80/58.83 & v17_lattices(A) % 58.80/58.83 & ~ v3_realset2(A) % 58.80/58.83 & l3_lattices(A) ) % 58.80/58.83 => ! [B] : % 58.80/58.83 ( m1_subset_1(B,u1_struct_0(A)) % 58.80/58.83 => r1_tarski(a_2_0_lopclset(A,B),k7_lopclset(A)) ) ) ). % 58.80/58.83 % 58.80/58.83 fof(antisymmetry_r2_hidden,axiom, % 58.80/58.83 ! [A,B] : % 58.80/58.83 ( r2_hidden(A,B) % 58.80/58.83 => ~ r2_hidden(B,A) ) ). % 58.80/58.83 % 58.80/58.83 fof(cc10_membered,axiom, % 58.80/58.83 ! [A] : % 58.80/58.83 ( v1_membered(A) % 58.80/58.83 => ! [B] : % 58.80/58.83 ( m1_subset_1(B,A) % 58.80/58.83 => v1_xcmplx_0(B) ) ) ). % 58.80/58.83 % 58.80/58.83 fof(cc11_membered,axiom, % 58.80/58.83 ! [A] : % 58.80/58.83 ( v2_membered(A) % 58.80/58.83 => ! [B] : % 58.80/58.83 ( m1_subset_1(B,A) % 58.80/58.83 => ( v1_xcmplx_0(B) % 58.80/58.83 & v1_xreal_0(B) ) ) ) ). % 58.80/58.83 % 58.80/58.83 fof(cc12_membered,axiom, % 58.80/58.83 ! [A] : % 58.80/58.83 ( v3_membered(A) % 58.80/58.83 => ! [B] : % 58.80/58.83 ( m1_subset_1(B,A) % 58.80/58.83 => ( v1_xcmplx_0(B) % 58.80/58.83 & v1_xreal_0(B) % 58.80/58.84 & v1_rat_1(B) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc13_membered,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v4_membered(A) % 58.80/58.84 => ! [B] : % 58.80/58.84 ( m1_subset_1(B,A) % 58.80/58.84 => ( v1_xcmplx_0(B) % 58.80/58.84 & v1_xreal_0(B) % 58.80/58.84 & v1_int_1(B) % 58.80/58.84 & v1_rat_1(B) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc14_membered,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v5_membered(A) % 58.80/58.84 => ! [B] : % 58.80/58.84 ( m1_subset_1(B,A) % 58.80/58.84 => ( v1_xcmplx_0(B) % 58.80/58.84 & v4_ordinal2(B) % 58.80/58.84 & v1_xreal_0(B) % 58.80/58.84 & v1_int_1(B) % 58.80/58.84 & v1_rat_1(B) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc15_membered,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v1_xboole_0(A) % 58.80/58.84 => ( v1_membered(A) % 58.80/58.84 & v2_membered(A) % 58.80/58.84 & v3_membered(A) % 58.80/58.84 & v4_membered(A) % 58.80/58.84 & v5_membered(A) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc16_membered,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v1_membered(A) % 58.80/58.84 => ! [B] : % 58.80/58.84 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.80/58.84 => v1_membered(B) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc17_membered,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v2_membered(A) % 58.80/58.84 => ! [B] : % 58.80/58.84 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.80/58.84 => ( v1_membered(B) % 58.80/58.84 & v2_membered(B) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc18_membered,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v3_membered(A) % 58.80/58.84 => ! [B] : % 58.80/58.84 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.80/58.84 => ( v1_membered(B) % 58.80/58.84 & v2_membered(B) % 58.80/58.84 & v3_membered(B) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc19_membered,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v4_membered(A) % 58.80/58.84 => ! [B] : % 58.80/58.84 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.80/58.84 => ( v1_membered(B) % 58.80/58.84 & v2_membered(B) % 58.80/58.84 & v3_membered(B) % 58.80/58.84 & v4_membered(B) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc1_finset_1,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v1_xboole_0(A) % 58.80/58.84 => v1_finset_1(A) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc1_finsub_1,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v4_finsub_1(A) % 58.80/58.84 => ( v1_finsub_1(A) % 58.80/58.84 & v3_finsub_1(A) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc1_lattices,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( l3_lattices(A) % 58.80/58.84 => ( ( ~ v3_struct_0(A) % 58.80/58.84 & v10_lattices(A) ) % 58.80/58.84 => ( ~ v3_struct_0(A) % 58.80/58.84 & v4_lattices(A) % 58.80/58.84 & v5_lattices(A) % 58.80/58.84 & v6_lattices(A) % 58.80/58.84 & v7_lattices(A) % 58.80/58.84 & v8_lattices(A) % 58.80/58.84 & v9_lattices(A) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc1_membered,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v5_membered(A) % 58.80/58.84 => v4_membered(A) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc20_membered,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v5_membered(A) % 58.80/58.84 => ! [B] : % 58.80/58.84 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.80/58.84 => ( v1_membered(B) % 58.80/58.84 & v2_membered(B) % 58.80/58.84 & v3_membered(B) % 58.80/58.84 & v4_membered(B) % 58.80/58.84 & v5_membered(B) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc2_finset_1,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v1_finset_1(A) % 58.80/58.84 => ! [B] : % 58.80/58.84 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.80/58.84 => v1_finset_1(B) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc2_finsub_1,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( ( v1_finsub_1(A) % 58.80/58.84 & v3_finsub_1(A) ) % 58.80/58.84 => v4_finsub_1(A) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc2_lattices,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( l3_lattices(A) % 58.80/58.84 => ( ( ~ v3_struct_0(A) % 58.80/58.84 & v4_lattices(A) % 58.80/58.84 & v5_lattices(A) % 58.80/58.84 & v6_lattices(A) % 58.80/58.84 & v7_lattices(A) % 58.80/58.84 & v8_lattices(A) % 58.80/58.84 & v9_lattices(A) ) % 58.80/58.84 => ( ~ v3_struct_0(A) % 58.80/58.84 & v10_lattices(A) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc2_membered,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v4_membered(A) % 58.80/58.84 => v3_membered(A) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc3_lattices,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( l3_lattices(A) % 58.80/58.84 => ( ( ~ v3_struct_0(A) % 58.80/58.84 & v13_lattices(A) % 58.80/58.84 & v14_lattices(A) ) % 58.80/58.84 => ( ~ v3_struct_0(A) % 58.80/58.84 & v15_lattices(A) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc3_membered,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v3_membered(A) % 58.80/58.84 => v2_membered(A) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc4_lattices,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( l3_lattices(A) % 58.80/58.84 => ( ( ~ v3_struct_0(A) % 58.80/58.84 & v15_lattices(A) ) % 58.80/58.84 => ( ~ v3_struct_0(A) % 58.80/58.84 & v13_lattices(A) % 58.80/58.84 & v14_lattices(A) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc4_membered,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( v2_membered(A) % 58.80/58.84 => v1_membered(A) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc5_lattices,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( l3_lattices(A) % 58.80/58.84 => ( ( ~ v3_struct_0(A) % 58.80/58.84 & v17_lattices(A) ) % 58.80/58.84 => ( ~ v3_struct_0(A) % 58.80/58.84 & v11_lattices(A) % 58.80/58.84 & v13_lattices(A) % 58.80/58.84 & v14_lattices(A) % 58.80/58.84 & v15_lattices(A) % 58.80/58.84 & v16_lattices(A) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc6_lattices,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( l3_lattices(A) % 58.80/58.84 => ( ( ~ v3_struct_0(A) % 58.80/58.84 & v11_lattices(A) % 58.80/58.84 & v15_lattices(A) % 58.80/58.84 & v16_lattices(A) ) % 58.80/58.84 => ( ~ v3_struct_0(A) % 58.80/58.84 & v17_lattices(A) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(cc7_lattices,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( l3_lattices(A) % 58.80/58.84 => ( ( ~ v3_struct_0(A) % 58.80/58.84 & v10_lattices(A) % 58.80/58.84 & v11_lattices(A) ) % 58.80/58.84 => ( ~ v3_struct_0(A) % 58.80/58.84 & v4_lattices(A) % 58.80/58.84 & v5_lattices(A) % 58.80/58.84 & v6_lattices(A) % 58.80/58.84 & v7_lattices(A) % 58.80/58.84 & v8_lattices(A) % 58.80/58.84 & v9_lattices(A) % 58.80/58.84 & v10_lattices(A) % 58.80/58.84 & v12_lattices(A) ) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(d3_tarski,axiom, % 58.80/58.84 ! [A,B] : % 58.80/58.84 ( r1_tarski(A,B) % 58.80/58.84 <=> ! [C] : % 58.80/58.84 ( r2_hidden(C,A) % 58.80/58.84 => r2_hidden(C,B) ) ) ). % 58.80/58.84 % 58.80/58.84 fof(d5_lopclset,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( ( ~ v3_struct_0(A) % 58.80/58.84 & v10_lattices(A) % 58.80/58.84 & v17_lattices(A) % 58.80/58.84 & ~ v3_realset2(A) % 58.80/58.84 & l3_lattices(A) ) % 58.80/58.84 => k7_lopclset(A) = a_1_1_lopclset(A) ) ). % 58.80/58.84 % 58.80/58.84 fof(dt_k1_xboole_0,axiom, % 58.80/58.84 $true ). % 58.80/58.84 % 58.80/58.84 fof(dt_k1_zfmisc_1,axiom, % 58.80/58.84 $true ). % 58.80/58.84 % 58.80/58.84 fof(dt_k7_lopclset,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( ( ~ v3_struct_0(A) % 58.80/58.84 & v10_lattices(A) % 58.80/58.84 & v17_lattices(A) % 58.80/58.84 & ~ v3_realset2(A) % 58.80/58.84 & l3_lattices(A) ) % 58.80/58.84 => m1_subset_1(k7_lopclset(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) ) ). % 58.80/58.84 % 58.80/58.84 fof(dt_l1_lattices,axiom, % 58.80/58.84 ! [A] : % 58.80/58.84 ( l1_lattices(A) % 58.80/58.84 => l1_struct_0(A) ) ). % 58.80/58.84 % 58.80/58.84 fof(dt_l1_struct_0,axiom, % 58.80/58.84 $true ). % 58.80/58.84 % 58.80/58.84 fof(dt_l2_lattices,axiom, % 58.80/58.84 ! [A] : % 58.80/58.85 ( l2_lattices(A) % 58.80/58.85 => l1_struct_0(A) ) ). % 58.80/58.85 % 58.80/58.85 fof(dt_l3_lattices,axiom, % 58.80/58.85 ! [A] : % 58.80/58.85 ( l3_lattices(A) % 58.80/58.85 => ( l1_lattices(A) % 58.80/58.85 & l2_lattices(A) ) ) ). % 58.80/58.85 % 58.80/58.85 fof(dt_m1_filter_0,axiom, % 58.80/58.85 ! [A] : % 58.80/58.85 ( ( ~ v3_struct_0(A) % 58.80/58.85 & v10_lattices(A) % 58.80/58.85 & l3_lattices(A) ) % 58.80/58.85 => ! [B] : % 58.80/58.85 ( m1_filter_0(B,A) % 58.80/58.85 => ( ~ v1_xboole_0(B) % 58.80/58.85 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ) ) ). % 58.80/58.85 % 58.80/58.85 fof(dt_m1_subset_1,axiom, % 58.80/58.85 $true ). % 58.80/58.85 % 58.80/58.85 fof(dt_u1_struct_0,axiom, % 58.80/58.85 $true ). % 58.80/58.85 % 58.80/58.85 fof(existence_l1_lattices,axiom, % 58.80/58.85 ? [A] : l1_lattices(A) ). % 58.80/58.85 % 58.80/58.85 fof(existence_l1_struct_0,axiom, % 58.80/58.85 ? [A] : l1_struct_0(A) ). % 58.80/58.85 % 58.80/58.85 fof(existence_l2_lattices,axiom, % 58.80/58.85 ? [A] : l2_lattices(A) ). % 58.80/58.85 % 58.80/58.85 fof(existence_l3_lattices,axiom, % 58.80/58.85 ? [A] : l3_lattices(A) ). % 58.80/58.85 % 58.80/58.85 fof(existence_m1_filter_0,axiom, % 58.80/58.85 ! [A] : % 58.80/58.85 ( ( ~ v3_struct_0(A) % 58.80/58.85 & v10_lattices(A) % 58.80/58.85 & l3_lattices(A) ) % 58.80/58.85 => ? [B] : m1_filter_0(B,A) ) ). % 58.80/58.85 % 58.80/58.85 fof(existence_m1_subset_1,axiom, % 58.80/58.85 ! [A] : % 58.80/58.85 ? [B] : m1_subset_1(B,A) ). % 58.80/58.85 % 58.80/58.85 fof(fc1_finsub_1,axiom, % 58.80/58.85 ! [A] : % 58.80/58.85 ( ~ v1_xboole_0(k1_zfmisc_1(A)) % 58.80/58.85 & v1_finsub_1(k1_zfmisc_1(A)) % 58.80/58.85 & v3_finsub_1(k1_zfmisc_1(A)) % 58.80/58.85 & v4_finsub_1(k1_zfmisc_1(A)) ) ). % 58.80/58.85 % 58.80/58.85 fof(fc1_struct_0,axiom, % 58.80/58.85 ! [A] : % 58.80/58.85 ( ( ~ v3_struct_0(A) % 58.80/58.85 & l1_struct_0(A) ) % 58.80/58.85 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 58.80/58.85 % 58.80/58.85 fof(fc2_lopclset,axiom, % 58.80/58.85 ! [A] : % 58.80/58.85 ( ( ~ v3_struct_0(A) % 58.80/58.85 & v10_lattices(A) % 58.80/58.85 & v17_lattices(A) % 58.80/58.85 & ~ v3_realset2(A) % 58.80/58.85 & l3_lattices(A) ) % 58.80/58.85 => ~ v1_xboole_0(k7_lopclset(A)) ) ). % 58.80/58.85 % 58.80/58.85 fof(fc6_membered,axiom, % 58.80/58.85 ( v1_xboole_0(k1_xboole_0) % 58.80/58.85 & v1_membered(k1_xboole_0) % 58.80/58.85 & v2_membered(k1_xboole_0) % 58.80/58.85 & v3_membered(k1_xboole_0) % 58.80/58.85 & v4_membered(k1_xboole_0) % 58.80/58.85 & v5_membered(k1_xboole_0) ) ). % 58.80/58.85 % 58.80/58.85 fof(fraenkel_a_1_1_lopclset,axiom, % 58.80/58.85 ! [A,B] : % 58.80/58.85 ( ( ~ v3_struct_0(B) % 58.80/58.85 & v10_lattices(B) % 58.80/58.85 & v17_lattices(B) % 58.80/58.85 & ~ v3_realset2(B) % 58.80/58.85 & l3_lattices(B) ) % 58.80/58.85 => ( r2_hidden(A,a_1_1_lopclset(B)) % 58.80/58.85 <=> ? [C] : % 58.80/58.85 ( m1_filter_0(C,B) % 58.80/58.85 & A = C % 58.80/58.85 & v1_filter_0(C,B) ) ) ) ). % 58.80/58.85 % 58.80/58.85 fof(fraenkel_a_2_0_lopclset,axiom, % 58.80/58.85 ! [A,B,C] : % 58.80/58.85 ( ( ~ v3_struct_0(B) % 58.80/58.85 & v10_lattices(B) % 58.80/58.85 & v17_lattices(B) % 58.80/58.85 & ~ v3_realset2(B) % 58.80/58.85 & l3_lattices(B) % 58.80/58.85 & m1_subset_1(C,u1_struct_0(B)) ) % 58.80/58.85 => ( r2_hidden(A,a_2_0_lopclset(B,C)) % 58.80/58.85 <=> ? [D] : % 58.80/58.85 ( m1_filter_0(D,B) % 58.80/58.85 & A = D % 58.80/58.85 & v1_filter_0(D,B) % 58.80/58.85 & r2_hidden(C,D) ) ) ) ). % 58.80/58.85 % 58.80/58.85 fof(rc1_finset_1,axiom, % 58.80/58.85 ? [A] : % 58.80/58.85 ( ~ v1_xboole_0(A) % 58.80/58.85 & v1_finset_1(A) ) ). % 58.80/58.85 % 58.80/58.85 fof(rc1_lopclset,axiom, % 58.80/58.85 ? [A] : % 58.80/58.85 ( l3_lattices(A) % 58.80/58.85 & ~ v3_struct_0(A) % 58.80/58.85 & v4_lattices(A) % 58.80/58.85 & v5_lattices(A) % 58.80/58.85 & v6_lattices(A) % 58.80/58.85 & v7_lattices(A) % 58.80/58.85 & v8_lattices(A) % 58.80/58.85 & v9_lattices(A) % 58.80/58.85 & v10_lattices(A) % 58.80/58.85 & v11_lattices(A) % 58.80/58.85 & v12_lattices(A) % 58.80/58.85 & v13_lattices(A) % 58.80/58.85 & v14_lattices(A) % 58.80/58.85 & v15_lattices(A) % 58.80/58.85 & v16_lattices(A) % 58.80/58.85 & v17_lattices(A) % 58.80/58.85 & ~ v3_realset2(A) ) ). % 58.80/58.85 % 58.80/58.85 fof(rc1_membered,axiom, % 58.80/58.85 ? [A] : % 58.80/58.85 ( ~ v1_xboole_0(A) % 58.80/58.85 & v1_membered(A) % 58.80/58.85 & v2_membered(A) % 58.80/58.85 & v3_membered(A) % 58.80/58.85 & v4_membered(A) % 58.80/58.85 & v5_membered(A) ) ). % 58.80/58.85 % 58.80/58.85 fof(rc3_finset_1,axiom, % 58.80/58.85 ! [A] : % 58.80/58.85 ( ~ v1_xboole_0(A) % 58.80/58.85 => ? [B] : % 58.80/58.85 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.80/58.85 & ~ v1_xboole_0(B) % 58.80/58.85 & v1_finset_1(B) ) ) ). % 58.80/58.85 % 58.80/58.85 fof(rc3_struct_0,axiom, % 58.80/58.85 ? [A] : % 58.80/58.85 ( l1_struct_0(A) % 58.80/58.85 & ~ v3_struct_0(A) ) ). % 58.80/58.85 % 58.80/58.85 fof(rc4_finset_1,axiom, % 58.80/58.85 ! [A] : % 58.80/58.85 ( ~ v1_xboole_0(A) % 58.80/58.85 => ? [B] : % 58.80/58.85 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.80/58.85 & ~ v1_xboole_0(B) % 58.80/58.85 & v1_finset_1(B) ) ) ). % 58.80/58.85 % 58.80/58.85 fof(rc5_struct_0,axiom, % 58.80/58.85 ! [A] : % 58.80/58.85 ( ( ~ v3_struct_0(A) % 58.80/58.85 & l1_struct_0(A) ) % 58.80/58.85 => ? [B] : % 58.80/58.85 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.80/58.85 & ~ v1_xboole_0(B) ) ) ). % 58.80/58.85 % 58.80/58.85 fof(reflexivity_r1_tarski,axiom, % 58.80/58.85 ! [A,B] : r1_tarski(A,A) ). % 58.80/58.85 % 58.80/58.85 fof(t1_subset,axiom, % 58.80/58.85 ! [A,B] : % 58.80/58.85 ( r2_hidden(A,B) % 58.80/58.85 => m1_subset_1(A,B) ) ). % 58.80/58.85 % 58.80/58.85 fof(t2_subset,axiom, % 58.80/58.85 ! [A,B] : % 58.80/58.85 ( m1_subset_1(A,B) % 58.80/58.85 => ( v1_xboole_0(B) % 58.80/58.85 | r2_hidden(A,B) ) ) ). % 58.80/58.85 % 58.80/58.85 fof(t2_tarski,axiom, % 58.80/58.85 ! [A,B] : % 58.80/58.85 ( ! [C] : % 58.80/58.85 ( r2_hidden(C,A) % 58.80/58.85 <=> r2_hidden(C,B) ) % 58.80/58.85 => A = B ) ). % 58.80/58.85 % 58.80/58.85 fof(t3_subset,axiom, % 58.80/58.85 ! [A,B] : % 58.80/58.85 ( m1_subset_1(A,k1_zfmisc_1(B)) % 58.80/58.85 <=> r1_tarski(A,B) ) ). % 58.80/58.85 % 58.80/58.85 fof(t4_subset,axiom, % 58.80/58.85 ! [A,B,C] : % 58.80/58.85 ( ( r2_hidden(A,B) % 58.80/58.85 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 58.80/58.85 => m1_subset_1(A,C) ) ). % 58.80/58.85 % 58.80/58.85 fof(t5_subset,axiom, % 58.80/58.85 ! [A,B,C] : % 58.80/58.85 ~ ( r2_hidden(A,B) % 58.80/58.85 & m1_subset_1(B,k1_zfmisc_1(C)) % 58.80/58.85 & v1_xboole_0(C) ) ). % 58.80/58.85 % 58.80/58.85 fof(t6_boole,axiom, % 58.80/58.85 ! [A] : % 58.80/58.85 ( v1_xboole_0(A) % 58.80/58.85 => A = k1_xboole_0 ) ). % 58.80/58.85 % 58.80/58.85 fof(t7_boole,axiom, % 58.80/58.85 ! [A,B] : % 58.80/58.85 ~ ( r2_hidden(A,B) % 58.80/58.85 & v1_xboole_0(B) ) ). % 58.80/58.85 % 58.80/58.85 fof(t8_boole,axiom, % 58.80/58.85 ! [A,B] : % 58.80/58.85 ~ ( v1_xboole_0(A) % 58.80/58.85 & A != B % 58.80/58.85 & v1_xboole_0(B) ) ). % 58.80/58.85 % 58.80/58.85 %------------------------------------------------------------------------------ % 58.80/58.85 %------------------------------------------- % 58.80/58.85 % Proof found % 58.80/58.85 % SZS status Theorem for theBenchmark % 58.80/58.85 % SZS output start Proof % 58.80/58.85 %ClaNum:228(EqnAxiom:68) % 58.80/58.85 %VarNum:496(SingletonVarNum:176) % 58.80/58.85 %MaxLitNum:11 % 58.80/58.85 %MaxfuncDepth:3 % 58.80/58.85 %SharedTerms:58 % 58.80/58.85 %goalClause: 69 71 73 108 110 113 118 % 58.80/58.85 %singleGoalClaCount:7 % 58.80/58.85 [69]P1(a1) % 58.80/58.85 [70]P1(a2) % 58.80/58.85 [71]P10(a1) % 58.80/58.85 [72]P10(a2) % 58.80/58.85 [73]P2(a1) % 58.80/58.85 [74]P2(a14) % 58.80/58.85 [75]P2(a2) % 58.80/58.85 [76]P17(a20) % 58.80/58.85 [77]P17(a8) % 58.80/58.85 [78]P22(a20) % 58.80/58.85 [79]P22(a8) % 58.80/58.85 [80]P27(a20) % 58.80/58.85 [81]P27(a8) % 58.80/58.85 [82]P29(a20) % 58.80/58.85 [83]P29(a8) % 58.80/58.85 [84]P34(a20) % 58.80/58.85 [85]P34(a8) % 58.80/58.85 [86]P23(a20) % 58.80/58.85 [87]P18(a3) % 58.80/58.85 [88]P30(a2) % 58.80/58.85 [89]P35(a2) % 58.80/58.85 [90]P37(a2) % 58.80/58.85 [91]P38(a2) % 58.80/58.85 [92]P39(a2) % 58.80/58.85 [93]P40(a2) % 58.80/58.85 [94]P11(a2) % 58.80/58.85 [95]P14(a2) % 58.80/58.85 [96]P15(a2) % 58.80/58.85 [97]P12(a2) % 58.80/58.85 [98]P16(a2) % 58.80/58.85 [99]P13(a2) % 58.80/58.85 [100]P3(a15) % 58.80/58.85 [101]P4(a18) % 58.80/58.85 [102]P4(a9) % 58.80/58.85 [103]P5(a19) % 58.80/58.85 [110]~P32(a1) % 58.80/58.85 [111]~P32(a2) % 58.80/58.85 [112]~P32(a9) % 58.80/58.85 [113]~P33(a1) % 58.80/58.85 [114]~P33(a2) % 58.80/58.85 [115]~P23(a3) % 58.80/58.85 [116]~P23(a8) % 58.80/58.85 [108]P7(a16,f24(a1)) % 58.80/58.85 [118]~P6(f4(a1,a16),f25(a1)) % 58.80/58.85 [107]P6(x1071,x1071) % 58.80/58.85 [104]P31(f23(x1041)) % 58.80/58.85 [105]P20(f23(x1051)) % 58.80/58.85 [106]P28(f23(x1061)) % 58.80/58.85 [109]P7(f21(x1091),x1091) % 58.80/58.85 [117]~P23(f23(x1171)) % 58.80/58.85 [119]~P23(x1191)+E(x1191,a20) % 58.80/58.85 [120]~P22(x1201)+P17(x1201) % 58.80/58.85 [121]~P23(x1211)+P17(x1211) % 58.80/58.85 [122]~P27(x1221)+P22(x1221) % 58.80/58.85 [123]~P23(x1231)+P22(x1231) % 58.80/58.85 [124]~P29(x1241)+P27(x1241) % 58.80/58.85 [125]~P23(x1251)+P27(x1251) % 58.80/58.85 [126]~P34(x1261)+P29(x1261) % 58.80/58.85 [127]~P23(x1271)+P29(x1271) % 58.80/58.85 [128]~P23(x1281)+P34(x1281) % 58.80/58.85 [129]~P23(x1291)+P18(x1291) % 58.80/58.85 [130]~P31(x1301)+P20(x1301) % 58.80/58.85 [131]~P31(x1311)+P28(x1311) % 58.80/58.85 [132]~P2(x1321)+P3(x1321) % 58.80/58.85 [133]~P3(x1331)+P4(x1331) % 58.80/58.85 [134]~P5(x1341)+P4(x1341) % 58.80/58.85 [135]~P2(x1351)+P5(x1351) % 58.80/58.85 [136]P23(x1361)+P18(f10(x1361)) % 58.80/58.85 [137]P23(x1371)+P18(f11(x1371)) % 58.80/58.85 [140]P23(x1401)+~P23(f10(x1401)) % 58.80/58.85 [141]P23(x1411)+~P23(f11(x1411)) % 58.80/58.85 [166]P23(x1661)+P7(f10(x1661),f23(x1661)) % 58.80/58.85 [167]P23(x1671)+P7(f11(x1671),f23(x1671)) % 58.80/58.85 [157]~P23(x1571)+~P9(x1572,x1571) % 58.80/58.85 [183]~P9(x1831,x1832)+P7(x1831,x1832) % 58.80/58.85 [205]~P9(x2052,x2051)+~P9(x2051,x2052) % 58.80/58.85 [188]~P6(x1881,x1882)+P7(x1881,f23(x1882)) % 58.80/58.85 [206]P6(x2061,x2062)+~P7(x2061,f23(x2062)) % 58.80/58.85 [210]P6(x2101,x2102)+P9(f17(x2101,x2102),x2101) % 58.80/58.85 [216]P6(x2161,x2162)+~P9(f17(x2161,x2162),x2162) % 58.80/58.85 [139]~P20(x1391)+~P28(x1391)+P31(x1391) % 58.80/58.85 [155]~P4(x1551)+P32(x1551)+~P23(f24(x1551)) % 58.80/58.85 [156]~P4(x1561)+P32(x1561)+~P23(f12(x1561)) % 58.80/58.85 [209]~P4(x2091)+P32(x2091)+P7(f12(x2091),f23(f24(x2091))) % 58.80/58.85 [138]~P23(x1382)+~P23(x1381)+E(x1381,x1382) % 58.80/58.85 [168]~P7(x1681,x1682)+P25(x1681)+~P17(x1682) % 58.80/58.85 [169]~P7(x1691,x1692)+P25(x1691)+~P22(x1692) % 58.80/58.85 [170]~P7(x1701,x1702)+P25(x1701)+~P27(x1702) % 58.80/58.85 [171]~P7(x1711,x1712)+P25(x1711)+~P29(x1712) % 58.80/58.85 [172]~P7(x1721,x1722)+P25(x1721)+~P34(x1722) % 58.80/58.85 [173]~P7(x1731,x1732)+P26(x1731)+~P22(x1732) % 58.80/58.85 [174]~P7(x1741,x1742)+P26(x1741)+~P27(x1742) % 58.80/58.85 [175]~P7(x1751,x1752)+P26(x1751)+~P29(x1752) % 58.80/58.85 [176]~P7(x1761,x1762)+P26(x1761)+~P34(x1762) % 58.80/58.85 [177]~P7(x1771,x1772)+P24(x1771)+~P27(x1772) % 58.80/58.85 [178]~P7(x1781,x1782)+P24(x1781)+~P29(x1782) % 58.80/58.85 [179]~P7(x1791,x1792)+P24(x1791)+~P34(x1792) % 58.80/58.85 [180]~P7(x1801,x1802)+P21(x1801)+~P29(x1802) % 58.80/58.85 [181]~P7(x1811,x1812)+P21(x1811)+~P34(x1812) % 58.80/58.85 [182]~P7(x1821,x1822)+P36(x1821)+~P34(x1822) % 58.80/58.85 [187]~P7(x1872,x1871)+P23(x1871)+P9(x1872,x1871) % 58.80/58.85 [189]P17(x1891)+~P17(x1892)+~P7(x1891,f23(x1892)) % 58.80/58.85 [190]P17(x1901)+~P22(x1902)+~P7(x1901,f23(x1902)) % 58.80/58.85 [191]P17(x1911)+~P27(x1912)+~P7(x1911,f23(x1912)) % 58.80/58.85 [192]P17(x1921)+~P29(x1922)+~P7(x1921,f23(x1922)) % 58.80/58.85 [193]P17(x1931)+~P34(x1932)+~P7(x1931,f23(x1932)) % 58.80/58.85 [194]P22(x1941)+~P22(x1942)+~P7(x1941,f23(x1942)) % 58.80/58.85 [195]P22(x1951)+~P27(x1952)+~P7(x1951,f23(x1952)) % 58.80/58.85 [196]P22(x1961)+~P29(x1962)+~P7(x1961,f23(x1962)) % 58.80/58.85 [197]P22(x1971)+~P34(x1972)+~P7(x1971,f23(x1972)) % 58.80/58.85 [198]P27(x1981)+~P27(x1982)+~P7(x1981,f23(x1982)) % 58.80/58.85 [199]P27(x1991)+~P29(x1992)+~P7(x1991,f23(x1992)) % 58.80/58.85 [200]P27(x2001)+~P34(x2002)+~P7(x2001,f23(x2002)) % 58.80/58.85 [201]P29(x2011)+~P29(x2012)+~P7(x2011,f23(x2012)) % 58.80/58.85 [202]P29(x2021)+~P34(x2022)+~P7(x2021,f23(x2022)) % 58.80/58.85 [203]P34(x2031)+~P34(x2032)+~P7(x2031,f23(x2032)) % 58.80/58.85 [204]P18(x2041)+~P18(x2042)+~P7(x2041,f23(x2042)) % 58.80/58.85 [218]E(x2181,x2182)+P9(f13(x2181,x2182),x2182)+P9(f13(x2181,x2182),x2181) % 58.80/58.85 [223]E(x2231,x2232)+~P9(f13(x2231,x2232),x2232)+~P9(f13(x2231,x2232),x2231) % 58.80/58.85 [212]~P9(x2121,x2123)+P9(x2121,x2122)+~P6(x2123,x2122) % 58.80/58.85 [213]~P23(x2131)+~P9(x2132,x2133)+~P7(x2133,f23(x2131)) % 58.80/58.85 [214]P7(x2141,x2142)+~P9(x2141,x2143)+~P7(x2143,f23(x2142)) % 58.80/58.85 [142]P30(x1421)+~P1(x1421)+~P2(x1421)+P32(x1421) % 58.80/58.85 [143]P35(x1431)+~P1(x1431)+~P2(x1431)+P32(x1431) % 58.80/58.85 [144]P37(x1441)+~P1(x1441)+~P2(x1441)+P32(x1441) % 58.80/58.85 [145]P38(x1451)+~P1(x1451)+~P2(x1451)+P32(x1451) % 58.80/58.85 [146]P39(x1461)+~P1(x1461)+~P2(x1461)+P32(x1461) % 58.80/58.85 [147]P40(x1471)+~P1(x1471)+~P2(x1471)+P32(x1471) % 58.80/58.85 [148]P11(x1481)+~P10(x1481)+~P2(x1481)+P32(x1481) % 58.80/58.85 [149]P11(x1491)+~P2(x1491)+~P15(x1491)+P32(x1491) % 58.80/58.85 [150]P14(x1501)+~P10(x1501)+~P2(x1501)+P32(x1501) % 58.80/58.85 [151]P14(x1511)+~P2(x1511)+~P15(x1511)+P32(x1511) % 58.80/58.85 [152]P15(x1521)+~P10(x1521)+~P2(x1521)+P32(x1521) % 58.80/58.85 [153]P12(x1531)+~P10(x1531)+~P2(x1531)+P32(x1531) % 58.80/58.85 [154]P16(x1541)+~P10(x1541)+~P2(x1541)+P32(x1541) % 58.80/58.85 [186]~P1(x1861)+~P2(x1861)+P32(x1861)+P8(f22(x1861),x1861) % 58.80/58.85 [164]P15(x1641)+~P2(x1641)+~P11(x1641)+~P14(x1641)+P32(x1641) % 58.80/58.85 [165]P13(x1651)+~P1(x1651)+~P2(x1651)+~P12(x1651)+P32(x1651) % 58.80/58.85 [208]~P1(x2081)+~P2(x2081)+~P8(x2082,x2081)+P32(x2081)+~P23(x2082) % 58.80/58.85 [215]~P1(x2151)+~P2(x2151)+~P8(x2152,x2151)+P32(x2151)+P7(x2152,f23(f24(x2151))) % 58.80/58.85 [184]P10(x1841)+~P2(x1841)+~P15(x1841)+~P12(x1841)+~P16(x1841)+P32(x1841) % 58.80/58.85 [185]P32(x1851)+P33(x1851)+~P1(x1851)+~P10(x1851)+~P2(x1851)+E(f25(x1851),f5(x1851)) % 58.80/58.85 [207]P33(x2071)+~P1(x2071)+~P10(x2071)+~P2(x2071)+P32(x2071)+~P23(f25(x2071)) % 58.80/58.85 [219]P33(x2191)+~P1(x2191)+~P10(x2191)+~P2(x2191)+P32(x2191)+P7(f25(x2191),f23(f23(f24(x2191)))) % 58.80/58.85 [217]P32(x2172)+P33(x2172)+~P1(x2172)+~P10(x2172)+~P2(x2172)+~P9(x2171,f5(x2172))+E(f6(x2171,x2172),x2171) % 58.80/58.85 [221]P33(x2211)+~P1(x2211)+~P10(x2211)+~P2(x2211)+P32(x2211)+~P9(x2212,f5(x2211))+P8(f6(x2212,x2211),x2211) % 58.80/58.85 [222]P33(x2221)+~P1(x2221)+~P10(x2221)+~P2(x2221)+P32(x2221)+~P9(x2222,f5(x2221))+P19(f6(x2222,x2221),x2221) % 58.80/58.85 [225]P32(x2252)+P33(x2252)+~P1(x2252)+~P10(x2252)+~P2(x2252)+~P7(x2253,f24(x2252))+~P9(x2251,f4(x2252,x2253))+E(f7(x2251,x2252,x2253),x2251) % 58.80/58.85 [226]P33(x2261)+~P1(x2261)+~P10(x2261)+~P2(x2261)+P32(x2261)+~P7(x2262,f24(x2261))+~P9(x2263,f4(x2261,x2262))+P9(x2262,f7(x2263,x2261,x2262)) % 58.80/58.85 [227]P33(x2271)+~P1(x2271)+~P10(x2271)+~P2(x2271)+P32(x2271)+~P7(x2273,f24(x2271))+~P9(x2272,f4(x2271,x2273))+P8(f7(x2272,x2271,x2273),x2271) % 58.80/58.85 [228]P33(x2281)+~P1(x2281)+~P10(x2281)+~P2(x2281)+P32(x2281)+~P7(x2283,f24(x2281))+~P9(x2282,f4(x2281,x2283))+P19(f7(x2282,x2281,x2283),x2281) % 58.80/58.85 [211]P1(x2111)+~P2(x2111)+~P30(x2111)+~P35(x2111)+~P37(x2111)+~P38(x2111)+~P39(x2111)+~P40(x2111)+P32(x2111) % 58.80/58.85 [220]P33(x2201)+~P1(x2201)+~P10(x2201)+~P2(x2201)+~P8(x2203,x2201)+~P19(x2203,x2201)+P32(x2201)+~E(x2203,x2202)+P9(x2202,f5(x2201)) % 58.80/58.85 [224]P33(x2241)+~P1(x2241)+~P10(x2241)+~P2(x2241)+~P9(x2243,x2244)+~P8(x2244,x2241)+~P19(x2244,x2241)+P32(x2241)+~E(x2244,x2242)+~P7(x2243,f24(x2241))+P9(x2242,f4(x2241,x2243)) % 58.80/58.85 %EqnAxiom % 58.80/58.85 [1]E(x11,x11) % 58.80/58.85 [2]E(x22,x21)+~E(x21,x22) % 58.80/58.85 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.80/58.85 [4]~E(x41,x42)+E(f23(x41),f23(x42)) % 58.80/58.85 [5]~E(x51,x52)+E(f4(x51,x53),f4(x52,x53)) % 58.80/58.85 [6]~E(x61,x62)+E(f4(x63,x61),f4(x63,x62)) % 58.80/58.85 [7]~E(x71,x72)+E(f24(x71),f24(x72)) % 58.80/58.85 [8]~E(x81,x82)+E(f17(x81,x83),f17(x82,x83)) % 58.80/58.85 [9]~E(x91,x92)+E(f17(x93,x91),f17(x93,x92)) % 58.80/58.85 [10]~E(x101,x102)+E(f21(x101),f21(x102)) % 58.80/58.85 [11]~E(x111,x112)+E(f7(x111,x113,x114),f7(x112,x113,x114)) % 58.80/58.85 [12]~E(x121,x122)+E(f7(x123,x121,x124),f7(x123,x122,x124)) % 58.80/58.85 [13]~E(x131,x132)+E(f7(x133,x134,x131),f7(x133,x134,x132)) % 58.80/58.85 [14]~E(x141,x142)+E(f5(x141),f5(x142)) % 58.80/58.85 [15]~E(x151,x152)+E(f25(x151),f25(x152)) % 58.80/58.85 [16]~E(x161,x162)+E(f10(x161),f10(x162)) % 58.80/58.85 [17]~E(x171,x172)+E(f11(x171),f11(x172)) % 58.80/58.85 [18]~E(x181,x182)+E(f13(x181,x183),f13(x182,x183)) % 58.80/58.85 [19]~E(x191,x192)+E(f13(x193,x191),f13(x193,x192)) % 58.80/58.85 [20]~E(x201,x202)+E(f6(x201,x203),f6(x202,x203)) % 58.80/58.85 [21]~E(x211,x212)+E(f6(x213,x211),f6(x213,x212)) % 58.80/58.85 [22]~E(x221,x222)+E(f12(x221),f12(x222)) % 58.80/58.85 [23]~E(x231,x232)+E(f22(x231),f22(x232)) % 58.80/58.85 [24]~P1(x241)+P1(x242)+~E(x241,x242) % 58.80/58.85 [25]P9(x252,x253)+~E(x251,x252)+~P9(x251,x253) % 58.80/58.85 [26]P9(x263,x262)+~E(x261,x262)+~P9(x263,x261) % 58.80/58.86 [27]~P10(x271)+P10(x272)+~E(x271,x272) % 58.80/58.86 [28]~P33(x281)+P33(x282)+~E(x281,x282) % 58.80/58.86 [29]~P2(x291)+P2(x292)+~E(x291,x292) % 58.80/58.86 [30]P19(x302,x303)+~E(x301,x302)+~P19(x301,x303) % 58.80/58.86 [31]P19(x313,x312)+~E(x311,x312)+~P19(x313,x311) % 58.80/58.86 [32]P7(x322,x323)+~E(x321,x322)+~P7(x321,x323) % 58.80/58.86 [33]P7(x333,x332)+~E(x331,x332)+~P7(x333,x331) % 58.80/58.86 [34]~P17(x341)+P17(x342)+~E(x341,x342) % 58.80/58.86 [35]~P18(x351)+P18(x352)+~E(x351,x352) % 58.80/58.86 [36]~P22(x361)+P22(x362)+~E(x361,x362) % 58.80/58.86 [37]~P36(x371)+P36(x372)+~E(x371,x372) % 58.80/58.86 [38]~P27(x381)+P27(x382)+~E(x381,x382) % 58.80/58.86 [39]~P24(x391)+P24(x392)+~E(x391,x392) % 58.80/58.86 [40]~P29(x401)+P29(x402)+~E(x401,x402) % 58.80/58.86 [41]~P26(x411)+P26(x412)+~E(x411,x412) % 58.80/58.86 [42]~P34(x421)+P34(x422)+~E(x421,x422) % 58.80/58.86 [43]~P23(x431)+P23(x432)+~E(x431,x432) % 58.80/58.86 [44]~P32(x441)+P32(x442)+~E(x441,x442) % 58.80/58.86 [45]~P30(x451)+P30(x452)+~E(x451,x452) % 58.80/58.86 [46]~P35(x461)+P35(x462)+~E(x461,x462) % 58.80/58.86 [47]~P37(x471)+P37(x472)+~E(x471,x472) % 58.80/58.86 [48]~P11(x481)+P11(x482)+~E(x481,x482) % 58.80/58.86 [49]~P38(x491)+P38(x492)+~E(x491,x492) % 58.80/58.86 [50]~P39(x501)+P39(x502)+~E(x501,x502) % 58.80/58.86 [51]~P40(x511)+P40(x512)+~E(x511,x512) % 58.80/58.86 [52]~P15(x521)+P15(x522)+~E(x521,x522) % 58.80/58.86 [53]~P14(x531)+P14(x532)+~E(x531,x532) % 58.80/58.86 [54]P8(x542,x543)+~E(x541,x542)+~P8(x541,x543) % 58.80/58.86 [55]P8(x553,x552)+~E(x551,x552)+~P8(x553,x551) % 58.80/58.86 [56]~P12(x561)+P12(x562)+~E(x561,x562) % 58.80/58.86 [57]~P16(x571)+P16(x572)+~E(x571,x572) % 58.80/58.86 [58]~P13(x581)+P13(x582)+~E(x581,x582) % 58.80/58.86 [59]~P3(x591)+P3(x592)+~E(x591,x592) % 58.80/58.86 [60]~P4(x601)+P4(x602)+~E(x601,x602) % 58.80/58.86 [61]~P25(x611)+P25(x612)+~E(x611,x612) % 58.80/58.86 [62]~P5(x621)+P5(x622)+~E(x621,x622) % 58.80/58.86 [63]~P31(x631)+P31(x632)+~E(x631,x632) % 58.80/58.86 [64]~P20(x641)+P20(x642)+~E(x641,x642) % 58.80/58.86 [65]~P28(x651)+P28(x652)+~E(x651,x652) % 58.80/58.86 [66]P6(x662,x663)+~E(x661,x662)+~P6(x661,x663) % 58.80/58.86 [67]P6(x673,x672)+~E(x671,x672)+~P6(x673,x671) % 58.80/58.86 [68]~P21(x681)+P21(x682)+~E(x681,x682) % 58.80/58.86 % 58.80/58.86 %------------------------------------------- % 58.80/58.86 cnf(229,plain, % 58.80/58.86 (~P1(x2291)+~P10(x2291)+~P2(x2291)+~P19(x2292,x2291)+P32(x2291)+P33(x2291)+~P8(x2292,x2291)+P9(x2292,f5(x2291))), % 58.80/58.86 inference(equality_inference,[],[220])). % 58.80/58.86 cnf(230,plain, % 58.80/58.86 (~P1(x2301)+~P10(x2301)+~P2(x2301)+~P8(x2302,x2301)+~P19(x2302,x2301)+P32(x2301)+P33(x2301)+~P9(x2303,x2302)+~P7(x2303,f24(x2301))+P9(x2302,f4(x2301,x2303))), % 58.80/58.86 inference(equality_inference,[],[224])). % 58.80/58.86 cnf(231,plain, % 58.80/58.86 (P6(f21(f23(x2311)),x2311)), % 58.80/58.86 inference(scs_inference,[],[109,206])). % 58.80/58.86 cnf(232,plain, % 58.80/58.86 (P7(f21(x2321),x2321)), % 58.80/58.86 inference(rename_variables,[],[109])). % 58.80/58.86 cnf(234,plain, % 58.80/58.86 (~P9(x2341,a20)), % 58.80/58.86 inference(scs_inference,[],[86,109,206,157])). % 58.80/58.86 cnf(236,plain, % 58.80/58.86 (P9(f21(a3),a3)), % 58.80/58.86 inference(scs_inference,[],[86,109,232,115,206,157,187])). % 58.80/58.86 cnf(237,plain, % 58.80/58.86 (P7(f21(x2371),x2371)), % 58.80/58.86 inference(rename_variables,[],[109])). % 58.80/58.86 cnf(239,plain, % 58.80/58.86 (~E(f25(a1),f4(a1,a16))), % 58.80/58.86 inference(scs_inference,[],[118,86,107,109,232,115,206,157,187,66])). % 58.80/58.86 cnf(240,plain, % 58.80/58.86 (P6(x2401,x2401)), % 58.80/58.86 inference(rename_variables,[],[107])). % 58.80/58.86 cnf(244,plain, % 58.80/58.86 (P7(f21(x2441),x2441)), % 58.80/58.86 inference(rename_variables,[],[109])). % 58.80/58.86 cnf(247,plain, % 58.80/58.86 (P7(f21(x2471),x2471)), % 58.80/58.86 inference(rename_variables,[],[109])). % 58.80/58.86 cnf(250,plain, % 58.80/58.86 (P7(f21(x2501),x2501)), % 58.80/58.86 inference(rename_variables,[],[109])). % 58.80/58.86 cnf(253,plain, % 58.80/58.86 (P7(f21(x2531),x2531)), % 58.80/58.86 inference(rename_variables,[],[109])). % 58.80/58.86 cnf(256,plain, % 58.80/58.86 (P7(f21(x2561),x2561)), % 58.80/58.86 inference(rename_variables,[],[109])). % 58.80/58.86 cnf(259,plain, % 58.80/58.86 (P7(f21(x2591),x2591)), % 58.80/58.86 inference(rename_variables,[],[109])). % 58.80/58.86 cnf(261,plain, % 58.80/58.86 (~P9(x2611,f21(f23(a20)))), % 58.80/58.86 inference(scs_inference,[],[118,86,107,240,109,232,237,244,247,250,253,256,259,76,78,80,82,84,87,115,206,157,187,66,67,189,194,198,201,203,204,213])). % 58.80/58.86 cnf(289,plain, % 58.80/58.86 (~P8(a20,a1)), % 58.80/58.86 inference(scs_inference,[],[69,71,73,110,118,86,107,240,109,232,237,244,247,250,253,256,259,76,78,80,82,84,87,115,206,157,187,66,67,189,194,198,201,203,204,213,26,142,143,144,145,146,147,148,150,152,153,154,165,208])). % 58.80/58.86 cnf(291,plain, % 58.80/58.86 (P6(f21(f23(a20)),x2911)), % 58.80/58.86 inference(scs_inference,[],[69,71,73,110,118,86,107,240,109,232,237,244,247,250,253,256,259,76,78,80,82,84,87,115,206,157,187,66,67,189,194,198,201,203,204,213,26,142,143,144,145,146,147,148,150,152,153,154,165,208,210])). % 58.80/58.86 cnf(293,plain, % 58.80/58.86 (~P9(a3,f21(a3))), % 58.80/58.86 inference(scs_inference,[],[69,71,73,110,118,86,107,240,109,232,237,244,247,250,253,256,259,76,78,80,82,84,87,115,206,157,187,66,67,189,194,198,201,203,204,213,26,142,143,144,145,146,147,148,150,152,153,154,165,208,210,205])). % 58.80/58.86 cnf(309,plain, % 58.80/58.86 (P6(a20,x3091)), % 58.80/58.86 inference(scs_inference,[],[234,210])). % 58.80/58.86 cnf(310,plain, % 58.80/58.86 (~P9(x3101,a20)), % 58.80/58.86 inference(rename_variables,[],[234])). % 58.80/58.86 cnf(312,plain, % 58.80/58.86 (E(f21(f23(a20)),a20)), % 58.80/58.86 inference(scs_inference,[],[261,234,310,210,218])). % 58.80/58.86 cnf(314,plain, % 58.80/58.86 (~P9(x3141,f21(f23(a20)))), % 58.80/58.86 inference(rename_variables,[],[261])). % 58.80/58.86 cnf(316,plain, % 58.80/58.86 (P7(a20,f23(a20))), % 58.80/58.86 inference(scs_inference,[],[261,234,310,109,210,218,32])). % 58.80/58.86 cnf(317,plain, % 58.80/58.86 (P7(f21(x3171),x3171)), % 58.80/58.86 inference(rename_variables,[],[109])). % 58.80/58.86 cnf(319,plain, % 58.80/58.86 (P7(f21(x3191),x3191)), % 58.80/58.86 inference(rename_variables,[],[109])). % 58.80/58.86 cnf(320,plain, % 58.80/58.86 (P9(f21(a8),a8)), % 58.80/58.86 inference(scs_inference,[],[261,234,310,116,109,317,319,210,218,32,33,187])). % 58.80/58.86 cnf(327,plain, % 58.80/58.86 (~P8(a20,a2)), % 58.80/58.86 inference(scs_inference,[],[118,231,236,75,261,314,70,111,86,234,310,116,109,317,319,210,218,32,33,187,66,26,208])). % 58.80/58.86 cnf(329,plain, % 58.80/58.86 (E(a20,f21(f23(a20)))), % 58.80/58.86 inference(scs_inference,[],[118,231,236,75,261,314,70,111,86,234,310,116,109,317,319,210,218,32,33,187,66,26,208,2])). % 58.80/58.86 cnf(333,plain, % 58.80/58.86 (P23(f21(f23(a20)))), % 58.80/58.86 inference(scs_inference,[],[118,231,236,75,261,314,70,111,86,234,310,116,109,317,319,210,218,32,33,187,66,26,208,2,205,24,43])). % 58.80/58.86 cnf(339,plain, % 58.80/58.86 (P9(a20,f23(a20))), % 58.80/58.86 inference(scs_inference,[],[316,117,187])). % 58.80/58.86 cnf(350,plain, % 58.80/58.86 (~P23(f4(a1,a16))), % 58.80/58.86 inference(scs_inference,[],[118,291,316,320,333,329,261,117,109,187,25,33,66,26,35,138])). % 58.80/58.86 cnf(353,plain, % 58.80/58.86 (P9(f21(f4(a1,a16)),f4(a1,a16))), % 58.80/58.86 inference(scs_inference,[],[350,109,187])). % 58.80/58.86 cnf(360,plain, % 58.80/58.86 (~P9(f4(a1,a16),f21(f4(a1,a16)))), % 58.80/58.86 inference(scs_inference,[],[118,309,339,261,350,109,187,66,26,205])). % 58.80/58.86 cnf(383,plain, % 58.80/58.86 (~P18(f21(f23(a20)))+P18(a20)), % 58.80/58.86 inference(scs_inference,[],[312,35])). % 58.80/58.86 cnf(454,plain, % 58.80/58.86 (P6(x4541,a8)+~E(f21(a8),f17(x4541,a8))), % 58.80/58.86 inference(scs_inference,[],[320,25,216])). % 58.80/58.86 cnf(645,plain, % 58.80/58.86 (P4(a1)), % 58.80/58.86 inference(scs_inference,[],[73,132,133])). % 58.80/58.86 cnf(708,plain, % 58.80/58.86 (~P23(f11(a8))), % 58.80/58.86 inference(scs_inference,[],[320,141,157])). % 58.80/58.86 cnf(715,plain, % 58.80/58.86 (~E(f11(a8),f21(f23(a20)))), % 58.80/58.86 inference(scs_inference,[],[261,708,109,187,205,25,26])). % 58.80/58.86 cnf(1265,plain, % 58.80/58.86 (P18(a20)), % 58.80/58.86 inference(scs_inference,[],[333,383,129])). % 58.80/58.86 cnf(2342,plain, % 58.80/58.86 (P7(f11(f10(f11(a8))),f23(f10(f11(a8))))), % 58.80/58.86 inference(scs_inference,[],[708,167,140])). % 58.80/58.86 cnf(2358,plain, % 58.80/58.86 (P7(f21(f23(a20)),f23(x23581))), % 58.80/58.86 inference(scs_inference,[],[261,188,210])). % 58.80/58.86 cnf(2359,plain, % 58.80/58.86 (P7(a20,f23(x23591))), % 58.80/58.86 inference(scs_inference,[],[312,2358,32])). % 58.80/58.86 cnf(2367,plain, % 58.80/58.86 (P9(f21(f23(a20)),f23(x23671))), % 58.80/58.86 inference(scs_inference,[],[2359,329,117,187,25])). % 58.80/58.86 cnf(2369,plain, % 58.80/58.86 (~E(f23(x23691),f21(f23(a20)))), % 58.80/58.86 inference(scs_inference,[],[2359,329,261,117,187,25,33,26])). % 58.80/58.86 cnf(3027,plain, % 58.80/58.86 (~E(f17(x30271,a8),f21(a8))+P6(x30271,a8)), % 58.80/58.86 inference(scs_inference,[],[454,2])). % 58.80/58.86 cnf(3186,plain, % 58.80/58.86 (~E(x31861,f21(a8))+~E(f17(x31862,a8),x31861)+P6(x31862,a8)), % 58.80/58.86 inference(scs_inference,[],[3027,3])). % 58.80/58.86 cnf(4331,plain, % 58.80/58.86 (P4(a2)), % 58.80/58.86 inference(scs_inference,[],[75,132,133])). % 58.80/58.86 cnf(4334,plain, % 58.80/58.86 (~E(f11(a8),a20)), % 58.80/58.86 inference(scs_inference,[],[329,75,715,2369,132,133,2,3])). % 58.80/58.86 cnf(4355,plain, % 58.80/58.86 (~E(a20,f11(a8))), % 58.80/58.86 inference(scs_inference,[],[4334,2])). % 58.80/58.86 cnf(4369,plain, % 58.80/58.86 (~P9(f4(a1,a16),x43691)+~E(x43691,f21(f4(a1,a16)))), % 58.80/58.86 inference(scs_inference,[],[360,26])). % 58.80/58.86 cnf(4438,plain, % 58.80/58.86 (~E(x44381,f4(a1,a16))+~E(f25(a1),x44381)), % 58.80/58.86 inference(scs_inference,[],[239,3])). % 58.80/58.86 cnf(4954,plain, % 58.80/58.86 (~E(f5(a1),f4(a1,a16))), % 58.80/58.86 inference(scs_inference,[],[113,69,71,73,110,4438,185])). % 58.80/58.86 cnf(4955,plain, % 58.80/58.86 (~E(f4(a1,a16),f5(a1))), % 58.80/58.86 inference(scs_inference,[],[4954,2])). % 58.80/58.86 cnf(4960,plain, % 58.80/58.86 (~E(x49601,f5(a1))+~E(f4(a1,a16),x49601)), % 58.80/58.86 inference(scs_inference,[],[4955,3])). % 58.80/58.86 cnf(5040,plain, % 58.80/58.86 (~E(a16,x50401)+~E(f4(a1,x50401),f5(a1))), % 58.80/58.86 inference(scs_inference,[],[4960,6])). % 58.80/58.86 cnf(5089,plain, % 58.80/58.86 (~E(f5(a1),f4(a1,x50891))+~E(a16,x50891)), % 58.80/58.86 inference(scs_inference,[],[5040,2])). % 58.80/58.86 cnf(5122,plain, % 58.80/58.86 (~E(x51221,f4(a1,x51222))+~E(f5(a1),x51221)+~E(a16,x51222)), % 58.80/58.86 inference(scs_inference,[],[5089,3])). % 58.80/58.86 cnf(5547,plain, % 58.80/58.86 (~P23(f10(a8))), % 58.80/58.86 inference(scs_inference,[],[116,136,137,140])). % 58.80/58.86 cnf(5549,plain, % 58.80/58.86 (~P23(f11(a3))), % 58.80/58.86 inference(scs_inference,[],[116,115,136,137,140,141])). % 58.80/58.86 cnf(5551,plain, % 58.80/58.86 (P7(x55511,f23(x55511))), % 58.80/58.86 inference(scs_inference,[],[116,107,115,136,137,140,141,188])). % 58.80/58.86 cnf(5553,plain, % 58.80/58.86 (P7(f10(a8),f23(a8))), % 58.80/58.86 inference(scs_inference,[],[116,107,115,136,137,140,141,188,166])). % 58.80/58.86 cnf(5571,plain, % 58.80/58.86 (E(f6(x55711,f21(f23(a20))),f6(x55711,a20))), % 58.80/58.86 inference(scs_inference,[],[116,107,115,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21])). % 58.80/58.86 cnf(5575,plain, % 58.80/58.86 (P9(f17(f4(a1,a16),f25(a1)),f4(a1,a16))), % 58.80/58.86 inference(scs_inference,[],[116,107,115,118,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210])). % 58.80/58.86 cnf(5577,plain, % 58.80/58.86 (~P9(f17(f4(a1,a16),f25(a1)),f25(a1))), % 58.80/58.86 inference(scs_inference,[],[116,107,115,118,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216])). % 58.80/58.86 cnf(5587,plain, % 58.80/58.86 (~P23(f24(a9))), % 58.80/58.86 inference(scs_inference,[],[102,112,116,107,115,75,118,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155])). % 58.80/58.86 cnf(5594,plain, % 58.80/58.86 (P9(f13(a20,f11(a8)),f11(a8))), % 58.80/58.86 inference(scs_inference,[],[289,102,112,4355,116,107,115,75,234,118,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155,156,54,209,218])). % 58.80/58.86 cnf(5595,plain, % 58.80/58.86 (~P9(x55951,a20)), % 58.80/58.86 inference(rename_variables,[],[234])). % 58.80/58.86 cnf(5597,plain, % 58.80/58.86 (~P6(f23(x55971),a20)), % 58.80/58.86 inference(scs_inference,[],[289,102,112,4355,2367,116,107,115,75,234,5595,118,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155,156,54,209,218,212])). % 58.80/58.86 cnf(5600,plain, % 58.80/58.86 (~P7(f23(x56001),f23(f21(f23(a20))))), % 58.80/58.86 inference(scs_inference,[],[289,102,112,4355,2367,116,107,115,75,234,5595,333,118,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155,156,54,209,218,212,213])). % 58.80/58.86 cnf(5602,plain, % 58.80/58.86 (~P6(f23(x56021),f21(f23(a20)))), % 58.80/58.86 inference(scs_inference,[],[289,102,112,4355,2367,116,107,115,75,234,5595,333,118,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155,156,54,209,218,212,213,67])). % 58.80/58.86 cnf(5611,plain, % 58.80/58.86 (~P23(f25(a1))), % 58.80/58.86 inference(scs_inference,[],[69,289,102,112,4355,2367,111,116,107,70,115,75,234,5595,333,118,113,71,110,73,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155,156,54,209,218,212,213,67,33,3,186,215,208,207])). % 58.80/58.86 cnf(5615,plain, % 58.80/58.86 (E(f25(a2),f5(a2))), % 58.80/58.86 inference(scs_inference,[],[69,289,102,112,114,72,4355,2367,111,116,107,70,115,75,234,5595,333,118,113,71,110,73,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155,156,54,209,218,212,213,67,33,3,186,215,208,207,219,185])). % 58.80/58.86 cnf(5617,plain, % 58.80/58.86 (E(f7(f21(f4(a1,a16)),a1,a16),f21(f4(a1,a16)))), % 58.80/58.86 inference(scs_inference,[],[69,289,102,112,114,72,4355,2367,111,116,107,70,115,75,234,5595,353,333,108,118,113,71,110,73,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155,156,54,209,218,212,213,67,33,3,186,215,208,207,219,185,225])). % 58.80/58.86 cnf(5621,plain, % 58.80/58.86 (P8(f7(f21(f4(a1,a16)),a1,a16),a1)), % 58.80/58.86 inference(scs_inference,[],[69,289,102,112,114,72,4355,2367,111,116,107,70,115,75,234,5595,353,333,108,118,113,71,110,73,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155,156,54,209,218,212,213,67,33,3,186,215,208,207,219,185,225,226,227])). % 58.80/58.86 cnf(5623,plain, % 58.80/58.86 (P19(f7(f21(f4(a1,a16)),a1,a16),a1)), % 58.80/58.86 inference(scs_inference,[],[69,289,102,112,114,72,4355,2367,111,116,107,70,115,75,234,5595,353,333,108,118,113,71,110,73,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155,156,54,209,218,212,213,67,33,3,186,215,208,207,219,185,225,226,227,228])). % 58.80/58.86 cnf(5625,plain, % 58.80/58.86 (P9(f21(f4(a1,a16)),f5(a1))), % 58.80/58.86 inference(scs_inference,[],[69,289,102,112,114,72,4355,2367,111,116,107,70,115,75,234,5595,353,333,108,118,113,71,110,73,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155,156,54,209,218,212,213,67,33,3,186,215,208,207,219,185,225,226,227,228,220])). % 58.80/58.86 cnf(5629,plain, % 58.80/58.86 (E(f6(f25(a2),x56291),f6(f5(a2),x56291))), % 58.80/58.86 inference(scs_inference,[],[69,289,102,112,114,72,4355,2367,111,116,107,70,115,75,234,5595,353,333,108,118,113,71,110,73,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155,156,54,209,218,212,213,67,33,3,186,215,208,207,219,185,225,226,227,228,220,230,20])). % 58.80/58.86 cnf(5633,plain, % 58.80/58.86 (~P9(f4(a1,a16),f23(f25(a1)))), % 58.80/58.86 inference(scs_inference,[],[69,289,102,112,114,72,4355,2367,111,116,107,70,115,75,234,5595,353,333,108,118,113,71,110,73,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155,156,54,209,218,212,213,67,33,3,186,215,208,207,219,185,225,226,227,228,220,230,20,4369,157,183])). % 58.80/58.86 cnf(5641,plain, % 58.80/58.86 (~E(f21(f23(a20)),f10(a8))), % 58.80/58.86 inference(scs_inference,[],[69,289,102,112,114,2342,72,4355,2367,111,116,107,70,115,117,75,234,5595,353,333,108,118,113,71,110,73,312,136,137,140,141,188,166,167,4,7,14,15,16,17,22,23,5,6,8,9,18,19,21,11,12,13,210,216,10,135,2,206,205,155,156,54,209,218,212,213,67,33,3,186,215,208,207,219,185,225,226,227,228,220,230,20,4369,157,183,171,30,187,43])). % 58.80/58.86 cnf(5673,plain, % 58.80/58.86 (P7(f10(f10(a8)),f23(f10(a8)))), % 58.80/58.86 inference(scs_inference,[],[5547,136,140,166])). % 58.80/58.86 cnf(5679,plain, % 58.80/58.86 (E(f7(x56791,f25(a2),x56792),f7(x56791,f5(a2),x56792))), % 58.80/58.86 inference(scs_inference,[],[5547,5615,136,140,166,14,141,8,12])). % 58.80/58.86 cnf(5689,plain, % 58.80/58.86 (E(f23(f25(a2)),f23(f5(a2)))), % 58.80/58.86 inference(scs_inference,[],[5547,5615,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4])). % 58.80/58.86 cnf(5691,plain, % 58.80/58.86 (E(f4(x56911,f25(a2)),f4(x56911,f5(a2)))), % 58.80/58.86 inference(scs_inference,[],[5547,5615,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6])). % 58.80/58.86 cnf(5695,plain, % 58.80/58.86 (P9(f17(f23(x56951),a20),f23(x56951))), % 58.80/58.86 inference(scs_inference,[],[5547,5597,5615,5600,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210])). % 58.80/58.86 cnf(5699,plain, % 58.80/58.86 (E(f7(f25(a2),x56991,x56992),f7(f5(a2),x56991,x56992))), % 58.80/58.86 inference(scs_inference,[],[5547,5597,5615,5600,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11])). % 58.80/58.86 cnf(5700,plain, % 58.80/58.86 (~P23(f5(a1))), % 58.80/58.86 inference(scs_inference,[],[5547,5597,5615,5625,5600,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157])). % 58.80/58.86 cnf(5708,plain, % 58.80/58.86 (E(f5(a2),f25(a2))), % 58.80/58.86 inference(scs_inference,[],[5547,5597,5615,5625,5600,73,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2])). % 58.80/58.86 cnf(5709,plain, % 58.80/58.86 (~P7(f23(x57091),f23(a20))), % 58.80/58.86 inference(scs_inference,[],[5547,5597,5615,5625,5600,73,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2,206])). % 58.80/58.86 cnf(5720,plain, % 58.80/58.86 (~P7(f17(f4(a1,a16),f25(a1)),f25(a1))), % 58.80/58.86 inference(scs_inference,[],[645,5547,5597,5611,5615,5577,5625,5600,5621,5617,110,73,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2,206,205,156,155,54,209,187])). % 58.80/58.86 cnf(5725,plain, % 58.80/58.86 (~P7(f4(a1,a16),f23(f21(f23(a20))))), % 58.80/58.86 inference(scs_inference,[],[645,5547,5597,5611,5615,5575,5577,5625,5641,5600,5621,5617,333,261,110,73,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2,206,205,156,155,54,209,187,218,213])). % 58.80/58.86 cnf(5728,plain, % 58.80/58.86 (P6(f21(f23(x57281)),x57281)), % 58.80/58.86 inference(rename_variables,[],[231])). % 58.80/58.86 cnf(5731,plain, % 58.80/58.86 (P7(f21(x57311),x57311)), % 58.80/58.86 inference(rename_variables,[],[109])). % 58.80/58.86 cnf(5732,plain, % 58.80/58.86 (~E(a20,f10(a8))), % 58.80/58.86 inference(scs_inference,[],[645,5547,5597,5611,5615,5575,5577,5625,5641,5600,5621,5617,293,231,333,261,110,73,109,86,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2,206,205,156,155,54,209,187,218,213,212,32,43])). % 58.80/58.86 cnf(5745,plain, % 58.80/58.86 (P8(f22(a1),a1)), % 58.80/58.86 inference(scs_inference,[],[69,645,5551,5547,5597,5611,5615,5575,5577,5625,5641,5629,5571,5600,5621,5617,293,231,5728,234,333,261,110,73,109,5731,86,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2,206,205,156,155,54,209,187,218,213,212,32,43,214,67,33,26,3,186])). % 58.80/58.86 cnf(5753,plain, % 58.80/58.86 (E(f25(a1),f5(a1))), % 58.80/58.86 inference(scs_inference,[],[69,645,5551,5547,5597,5611,5615,5575,5577,5625,5641,5629,5571,5600,5621,5617,114,72,293,231,5728,234,111,70,333,75,261,113,71,110,73,109,5731,86,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2,206,205,156,155,54,209,187,218,213,212,32,43,214,67,33,26,3,186,215,207,219,185])). % 58.80/58.86 cnf(5755,plain, % 58.80/58.86 (P19(f6(f21(f4(a1,a16)),a1),a1)), % 58.80/58.86 inference(scs_inference,[],[69,645,5551,5547,5597,5611,5615,5575,5577,5625,5641,5629,5571,5600,5621,5617,114,72,293,231,5728,234,111,70,333,75,261,113,71,110,73,109,5731,86,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2,206,205,156,155,54,209,187,218,213,212,32,43,214,67,33,26,3,186,215,207,219,185,222])). % 58.80/58.86 cnf(5757,plain, % 58.80/58.86 (P8(f6(f21(f4(a1,a16)),a1),a1)), % 58.80/58.86 inference(scs_inference,[],[69,645,5551,5547,5597,5611,5615,5575,5577,5625,5641,5629,5571,5600,5621,5617,114,72,293,231,5728,234,111,70,333,75,261,113,71,110,73,109,5731,86,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2,206,205,156,155,54,209,187,218,213,212,32,43,214,67,33,26,3,186,215,207,219,185,222,221])). % 58.80/58.86 cnf(5761,plain, % 58.80/58.86 (P8(f7(f17(f4(a1,a16),f25(a1)),a1,a16),a1)), % 58.80/58.86 inference(scs_inference,[],[69,645,5551,5547,5597,5611,5615,5575,5577,5625,5641,5629,5571,5600,5621,5617,114,72,293,231,5728,234,111,70,333,75,261,108,113,71,110,73,109,5731,86,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2,206,205,156,155,54,209,187,218,213,212,32,43,214,67,33,26,3,186,215,207,219,185,222,221,217,227])). % 58.80/58.86 cnf(5763,plain, % 58.80/58.86 (E(f7(f17(f4(a1,a16),f25(a1)),a1,a16),f17(f4(a1,a16),f25(a1)))), % 58.80/58.86 inference(scs_inference,[],[69,645,5551,5547,5597,5611,5615,5575,5577,5625,5641,5629,5571,5600,5621,5617,114,72,293,231,5728,234,111,70,333,75,261,108,113,71,110,73,109,5731,86,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2,206,205,156,155,54,209,187,218,213,212,32,43,214,67,33,26,3,186,215,207,219,185,222,221,217,227,225])). % 58.80/58.86 cnf(5765,plain, % 58.80/58.86 (P19(f7(f17(f4(a1,a16),f25(a1)),a1,a16),a1)), % 58.80/58.86 inference(scs_inference,[],[69,645,5551,5547,5597,5611,5615,5575,5577,5625,5641,5629,5571,5600,5621,5617,114,72,293,231,5728,234,111,70,333,75,261,108,113,71,110,73,109,5731,86,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2,206,205,156,155,54,209,187,218,213,212,32,43,214,67,33,26,3,186,215,207,219,185,222,221,217,227,225,228])). % 58.80/58.86 cnf(5769,plain, % 58.80/58.86 (P9(a16,f7(f17(f4(a1,a16),f25(a1)),a1,a16))), % 58.80/58.86 inference(scs_inference,[],[69,645,5551,5547,5597,5611,5615,5575,5577,5625,5641,5629,5571,5600,5623,5621,5617,114,72,293,231,5728,234,111,70,333,75,261,108,113,71,110,73,109,5731,86,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2,206,205,156,155,54,209,187,218,213,212,32,43,214,67,33,26,3,186,215,207,219,185,222,221,217,227,225,228,229,226])). % 58.80/58.86 cnf(5779,plain, % 58.80/58.86 (P6(f5(a2),f25(a2))), % 58.80/58.86 inference(scs_inference,[],[69,645,5551,5547,5597,5611,5615,5575,5577,5625,5641,5629,5571,5600,5623,5621,5617,114,72,293,231,5728,107,234,111,70,333,75,261,108,113,71,110,73,109,5731,86,136,140,166,14,141,8,12,19,9,167,17,22,137,23,4,7,6,183,21,210,15,18,11,157,5,13,16,135,10,2,206,205,156,155,54,209,187,218,213,212,32,43,214,67,33,26,3,186,215,207,219,185,222,221,217,227,225,228,229,226,230,188,4369,20,3186,66])). % 58.80/58.86 cnf(5827,plain, % 58.80/58.86 (E(f5(a1),f25(a1))), % 58.80/58.86 inference(scs_inference,[],[5549,5708,5753,5779,5725,5769,5602,74,136,166,167,141,188,140,183,137,157,8,14,19,9,210,21,15,23,4,13,17,12,6,20,7,18,22,11,16,5,135,10,2])). % 58.80/58.86 cnf(5840,plain, % 58.80/58.86 (P9(f10(a8),f23(a8))), % 58.80/58.86 inference(scs_inference,[],[4331,5549,5553,5708,5753,5779,5695,5725,5769,5602,117,81,79,111,74,136,166,167,141,188,140,183,137,157,8,14,19,9,210,21,15,23,4,13,17,12,6,20,7,18,22,11,16,5,135,10,2,205,155,156,198,190,194,187])). % 58.80/58.86 cnf(5849,plain, % 58.80/58.86 (~P9(x58491,a20)), % 58.80/58.86 inference(rename_variables,[],[234])). % 58.80/58.86 cnf(5851,plain, % 58.80/58.86 (~P6(f11(a8),a20)), % 58.80/58.86 inference(scs_inference,[],[327,4331,5549,5553,5708,5753,5779,5732,5695,5594,5673,5725,5769,5602,117,81,79,234,5849,111,312,74,136,166,167,141,188,140,183,137,157,8,14,19,9,210,21,15,23,4,13,17,12,6,20,7,18,22,11,16,5,135,10,2,205,155,156,198,190,194,187,54,195,209,218,212])). % 58.80/58.86 cnf(5855,plain, % 58.80/58.86 (P7(x58551,f23(x58551))), % 58.80/58.86 inference(rename_variables,[],[5551])). % 58.80/58.86 cnf(5856,plain, % 58.80/58.86 (P7(f17(f23(x58561),a20),f23(x58561))), % 58.80/58.86 inference(scs_inference,[],[327,4331,5549,5553,5708,5753,5779,5732,5695,5594,5673,5725,5769,5602,5551,5855,117,81,79,234,5849,111,312,74,136,166,167,141,188,140,183,137,157,8,14,19,9,210,21,15,23,4,13,17,12,6,20,7,18,22,11,16,5,135,10,2,205,155,156,198,190,194,187,54,195,209,218,212,32,214])). % 58.80/58.86 cnf(5859,plain, % 58.80/58.86 (~E(f21(f23(a20)),f11(a3))), % 58.80/58.86 inference(scs_inference,[],[327,4331,5549,5553,5708,5753,5779,5732,5695,5594,5673,5725,5769,5602,5551,5855,117,81,79,234,5849,111,333,312,74,136,166,167,141,188,140,183,137,157,8,14,19,9,210,21,15,23,4,13,17,12,6,20,7,18,22,11,16,5,135,10,2,205,155,156,198,190,194,187,54,195,209,218,212,32,214,43])). % 58.80/58.86 cnf(5860,plain, % 58.80/58.86 (~P6(f4(a1,a16),f5(a1))), % 58.80/58.86 inference(scs_inference,[],[327,4331,5549,5553,5708,5753,5779,5732,5695,5594,5673,5725,5769,5602,5551,5855,117,81,79,234,5849,111,333,118,312,74,136,166,167,141,188,140,183,137,157,8,14,19,9,210,21,15,23,4,13,17,12,6,20,7,18,22,11,16,5,135,10,2,205,155,156,198,190,194,187,54,195,209,218,212,32,214,43,67])). % 58.80/58.86 cnf(5862,plain, % 58.80/58.86 (P9(f17(f23(x58621),a20),f23(x58621))), % 58.80/58.86 inference(rename_variables,[],[5695])). % 58.80/58.86 cnf(5864,plain, % 58.80/58.86 (E(f7(f25(a2),f25(a2),x58641),f7(f5(a2),f5(a2),x58641))), % 58.80/58.86 inference(scs_inference,[],[327,4331,5549,5553,5708,5753,5779,5732,5695,5720,5594,5679,5699,5673,5689,5725,5769,5602,5551,5855,117,81,79,234,5849,111,333,118,312,74,136,166,167,141,188,140,183,137,157,8,14,19,9,210,21,15,23,4,13,17,12,6,20,7,18,22,11,16,5,135,10,2,205,155,156,198,190,194,187,54,195,209,218,212,32,214,43,67,26,33,3])). % 58.80/58.86 cnf(5873,plain, % 58.80/58.86 (P9(f17(f4(a1,a16),f25(a1)),f5(a1))), % 58.80/58.86 inference(scs_inference,[],[69,327,4331,5549,5553,5708,5753,5779,5732,5745,5695,5862,5720,5594,5633,5679,5699,5673,5689,5725,5755,5757,5769,5765,5761,5763,5602,5551,5855,117,81,79,234,5849,111,333,118,113,71,312,110,73,74,136,166,167,141,188,140,183,137,157,8,14,19,9,210,21,15,23,4,13,17,12,6,20,7,18,22,11,16,5,135,10,2,205,155,156,198,190,194,187,54,195,209,218,212,32,214,43,67,26,33,3,25,215,229,220])). % 58.80/58.86 cnf(5875,plain, % 58.80/58.86 (~P9(f17(f4(a1,a16),f5(a1)),f5(a1))), % 58.80/58.86 inference(scs_inference,[],[69,327,4331,5549,5553,5708,5753,5779,5732,5745,5695,5862,5720,5594,5633,5679,5699,5673,5689,5725,5755,5757,5769,5765,5761,5763,5602,5551,5855,117,81,79,234,5849,111,333,118,113,71,312,110,73,74,136,166,167,141,188,140,183,137,157,8,14,19,9,210,21,15,23,4,13,17,12,6,20,7,18,22,11,16,5,135,10,2,205,155,156,198,190,194,187,54,195,209,218,212,32,214,43,67,26,33,3,25,215,229,220,216])). % 58.80/58.86 cnf(5877,plain, % 58.80/58.86 (~P7(f11(a8),f23(a20))), % 58.80/58.86 inference(scs_inference,[],[69,327,4331,5549,5553,5708,5753,5779,5732,5745,5695,5862,5720,5594,5633,5679,5699,5673,5689,5725,5755,5757,5769,5765,5761,5763,5602,5551,5855,117,81,79,234,5849,111,333,118,113,71,312,110,73,74,136,166,167,141,188,140,183,137,157,8,14,19,9,210,21,15,23,4,13,17,12,6,20,7,18,22,11,16,5,135,10,2,205,155,156,198,190,194,187,54,195,209,218,212,32,214,43,67,26,33,3,25,215,229,220,216,206])). % 58.80/58.86 cnf(5881,plain, % 58.80/58.86 (P34(f10(a8))), % 58.80/58.86 inference(scs_inference,[],[69,327,4331,5549,5553,5708,5753,5779,5732,5745,5695,5862,5720,5594,5633,5679,5699,5691,5673,5689,5725,5755,5757,5769,5765,5761,5763,5602,5551,5855,117,81,85,79,234,5849,111,333,118,113,71,312,110,73,74,136,166,167,141,188,140,183,137,157,8,14,19,9,210,21,15,23,4,13,17,12,6,20,7,18,22,11,16,5,135,10,2,205,155,156,198,190,194,187,54,195,209,218,212,32,214,43,67,26,33,3,25,215,229,220,216,206,5122,203])). % 58.80/58.86 cnf(5887,plain, % 58.80/58.86 (P29(f10(a8))), % 58.80/58.86 inference(scs_inference,[],[69,327,4331,5549,5553,5708,5753,5779,5732,5745,5695,5862,5720,5594,5633,5679,5699,5691,5673,5689,5725,5755,5757,5769,5765,5761,5763,5602,5551,5855,117,81,85,79,234,5849,111,333,118,113,71,312,110,73,74,136,166,167,141,188,140,183,137,157,8,14,19,9,210,21,15,23,4,13,17,12,6,20,7,18,22,11,16,5,135,10,2,205,155,156,198,190,194,187,54,195,209,218,212,32,214,43,67,26,33,3,25,215,229,220,216,206,5122,203,193,213,126])). % 58.80/58.86 cnf(5933,plain, % 58.80/58.86 (P7(f21(x59331),x59331)), % 58.80/58.86 inference(rename_variables,[],[109])). % 58.80/58.86 cnf(5939,plain, % 58.80/58.86 (P7(f17(f23(x59391),a20),f23(x59391))), % 58.80/58.86 inference(rename_variables,[],[5856])). % 58.80/58.86 cnf(5942,plain, % 58.80/58.86 (P7(f17(f23(x59421),a20),f23(x59421))), % 58.80/58.86 inference(rename_variables,[],[5856])). % 58.80/58.86 cnf(5953,plain, % 58.80/58.86 (P7(f17(f23(x59531),a20),f23(x59531))), % 58.80/58.86 inference(rename_variables,[],[5856])). % 58.80/58.86 cnf(5956,plain, % 58.80/58.86 (P7(f17(f23(x59561),a20),f23(x59561))), % 58.80/58.86 inference(rename_variables,[],[5856])). % 58.80/58.86 cnf(5962,plain, % 58.80/58.86 ($false), % 58.80/58.86 inference(scs_inference,[],[1265,5709,5860,5587,5700,5827,5840,5877,5881,5887,5851,5856,5939,5942,5953,5956,5873,5875,5859,5864,5761,5763,5577,333,261,312,109,5933,136,167,140,166,141,137,8,183,210,4,9,13,12,14,21,23,7,22,19,15,17,6,20,5,11,18,16,205,2,206,10,172,179,200,192,187,218,212,54,214,204,67,32,43,26]), % 58.80/58.86 ['proof']). % 58.80/58.86 % SZS output end Proof % 58.80/58.86 % Total time :58.220000s %------------------------------------------------------------------------------