%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT292+1 : TPTP v8.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n022.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:39 EDT 2024 % Result : Theorem 60.01s 60.07s % Output : CNFRefutation 60.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : LAT292+1 : TPTP v8.2.0. Released v3.4.0. % 0.08/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n022.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 300 % 0.13/0.36 % DateTime : Fri Jun 21 22:31:24 EDT 2024 % 0.13/0.36 % CPUTime : % 0.42/0.61 start to proof:theBenchmark % 59.97/60.04 %------------------------------------------- % 59.97/60.04 % File :CSE---1.7 % 59.97/60.04 % Problem :theBenchmark % 59.97/60.04 % Transform :cnf % 59.97/60.04 % Format :tptp:raw % 59.97/60.04 % Command :java -jar mcs_scs.jar %d %s % 59.97/60.04 % 59.97/60.04 % Result :Theorem 59.330000s % 59.97/60.04 % Output :CNFRefutation 59.330000s % 59.97/60.04 %------------------------------------------- % 60.01/60.05 %------------------------------------------------------------------------------ % 60.01/60.05 % File : LAT292+1 : TPTP v8.2.0. Released v3.4.0. % 60.01/60.05 % Domain : Lattice Theory % 60.01/60.05 % Problem : Representation Theorem for Boolean Algebras T44 % 60.01/60.05 % Version : [Urb08] axioms : Especial. % 60.01/60.05 % English : % 60.01/60.05 % 60.01/60.05 % Refs : [Wal93] Walijewski (1993), Representation Theorem for Boolean % 60.01/60.05 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 60.01/60.05 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 60.01/60.05 % Source : [Urb08] % 60.01/60.05 % Names : t44_lopclset [Urb08] % 60.01/60.05 % 60.01/60.05 % Status : Theorem % 60.01/60.05 % Rating : 0.28 v8.2.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.17 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.22 v7.0.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.40 v6.0.0, 0.26 v5.5.0, 0.33 v5.4.0, 0.32 v5.3.0, 0.37 v5.2.0, 0.30 v5.1.0, 0.33 v5.0.0, 0.42 v4.1.0, 0.39 v4.0.1, 0.30 v4.0.0, 0.33 v3.7.0, 0.30 v3.5.0, 0.32 v3.4.0 % 60.01/60.05 % Syntax : Number of formulae : 112 ( 16 unt; 0 def) % 60.01/60.05 % Number of atoms : 512 ( 16 equ) % 60.01/60.05 % Maximal formula atoms : 17 ( 4 avg) % 60.01/60.05 % Number of connectives : 477 ( 77 ~; 1 |; 293 &) % 60.01/60.05 % ( 4 <=>; 102 =>; 0 <=; 0 <~>) % 60.01/60.05 % Maximal formula depth : 19 ( 6 avg) % 60.01/60.05 % Maximal term depth : 4 ( 1 avg) % 60.01/60.05 % Number of predicates : 53 ( 51 usr; 1 prp; 0-3 aty) % 60.01/60.05 % Number of functors : 16 ( 16 usr; 1 con; 0-3 aty) % 60.01/60.05 % Number of variables : 173 ( 143 !; 30 ?) % 60.01/60.05 % SPC : FOF_THM_RFO_SEQ % 60.01/60.05 % 60.01/60.05 % Comments : Normal version: includes the axioms (which may be theorems from % 60.01/60.05 % other articles) and background that are possibly necessary. % 60.01/60.05 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 60.01/60.05 % : The problem encoding is based on set theory. % 60.01/60.05 %------------------------------------------------------------------------------ % 60.01/60.05 fof(t44_lopclset,conjecture, % 60.01/60.05 ! [A] : % 60.01/60.05 ( ( ~ v3_struct_0(A) % 60.01/60.05 & v10_lattices(A) % 60.01/60.05 & v17_lattices(A) % 60.01/60.05 & ~ v3_realset2(A) % 60.01/60.05 & l3_lattices(A) ) % 60.01/60.05 => ? [B] : % 60.01/60.05 ( ~ v3_struct_0(B) % 60.01/60.05 & v2_pre_topc(B) % 60.01/60.05 & l1_pre_topc(B) % 60.01/60.05 & r1_filter_1(A,k6_lopclset(B)) ) ) ). % 60.01/60.05 % 60.01/60.05 fof(abstractness_v1_pre_topc,axiom, % 60.01/60.05 ! [A] : % 60.01/60.05 ( l1_pre_topc(A) % 60.01/60.05 => ( v1_pre_topc(A) % 60.01/60.05 => A = g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)) ) ) ). % 60.01/60.05 % 60.01/60.05 fof(abstractness_v3_lattices,axiom, % 60.01/60.05 ! [A] : % 60.01/60.05 ( l3_lattices(A) % 60.01/60.05 => ( v3_lattices(A) % 60.01/60.05 => A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ) ). % 60.01/60.05 % 60.01/60.05 fof(antisymmetry_r2_hidden,axiom, % 60.01/60.05 ! [A,B] : % 60.01/60.05 ( r2_hidden(A,B) % 60.01/60.05 => ~ r2_hidden(B,A) ) ). % 60.01/60.05 % 60.01/60.05 fof(cc10_membered,axiom, % 60.01/60.05 ! [A] : % 60.01/60.05 ( v1_membered(A) % 60.01/60.05 => ! [B] : % 60.01/60.05 ( m1_subset_1(B,A) % 60.01/60.05 => v1_xcmplx_0(B) ) ) ). % 60.01/60.05 % 60.01/60.05 fof(cc11_membered,axiom, % 60.01/60.05 ! [A] : % 60.01/60.05 ( v2_membered(A) % 60.01/60.05 => ! [B] : % 60.01/60.05 ( m1_subset_1(B,A) % 60.01/60.05 => ( v1_xcmplx_0(B) % 60.01/60.05 & v1_xreal_0(B) ) ) ) ). % 60.01/60.05 % 60.01/60.05 fof(cc12_membered,axiom, % 60.01/60.05 ! [A] : % 60.01/60.05 ( v3_membered(A) % 60.01/60.05 => ! [B] : % 60.01/60.05 ( m1_subset_1(B,A) % 60.01/60.05 => ( v1_xcmplx_0(B) % 60.01/60.05 & v1_xreal_0(B) % 60.01/60.05 & v1_rat_1(B) ) ) ) ). % 60.01/60.05 % 60.01/60.05 fof(cc13_membered,axiom, % 60.01/60.05 ! [A] : % 60.01/60.05 ( v4_membered(A) % 60.01/60.05 => ! [B] : % 60.01/60.05 ( m1_subset_1(B,A) % 60.01/60.05 => ( v1_xcmplx_0(B) % 60.01/60.05 & v1_xreal_0(B) % 60.01/60.05 & v1_int_1(B) % 60.01/60.05 & v1_rat_1(B) ) ) ) ). % 60.01/60.05 % 60.01/60.05 fof(cc14_membered,axiom, % 60.01/60.05 ! [A] : % 60.01/60.05 ( v5_membered(A) % 60.01/60.05 => ! [B] : % 60.01/60.05 ( m1_subset_1(B,A) % 60.01/60.05 => ( v1_xcmplx_0(B) % 60.01/60.05 & v4_ordinal2(B) % 60.01/60.05 & v1_xreal_0(B) % 60.01/60.05 & v1_int_1(B) % 60.01/60.05 & v1_rat_1(B) ) ) ) ). % 60.01/60.05 % 60.01/60.05 fof(cc15_membered,axiom, % 60.01/60.05 ! [A] : % 60.01/60.05 ( v1_xboole_0(A) % 60.01/60.05 => ( v1_membered(A) % 60.01/60.05 & v2_membered(A) % 60.01/60.05 & v3_membered(A) % 60.01/60.05 & v4_membered(A) % 60.01/60.05 & v5_membered(A) ) ) ). % 60.01/60.05 % 60.01/60.05 fof(cc16_membered,axiom, % 60.01/60.05 ! [A] : % 60.01/60.05 ( v1_membered(A) % 60.01/60.05 => ! [B] : % 60.01/60.05 ( m1_subset_1(B,k1_zfmisc_1(A)) % 60.01/60.05 => v1_membered(B) ) ) ). % 60.01/60.05 % 60.01/60.05 fof(cc17_membered,axiom, % 60.01/60.05 ! [A] : % 60.01/60.05 ( v2_membered(A) % 60.01/60.05 => ! [B] : % 60.01/60.05 ( m1_subset_1(B,k1_zfmisc_1(A)) % 60.01/60.05 => ( v1_membered(B) % 60.01/60.05 & v2_membered(B) ) ) ) ). % 60.01/60.05 % 60.01/60.05 fof(cc18_membered,axiom, % 60.01/60.05 ! [A] : % 60.01/60.05 ( v3_membered(A) % 60.01/60.05 => ! [B] : % 60.01/60.05 ( m1_subset_1(B,k1_zfmisc_1(A)) % 60.01/60.05 => ( v1_membered(B) % 60.01/60.05 & v2_membered(B) % 60.01/60.05 & v3_membered(B) ) ) ) ). % 60.01/60.05 % 60.01/60.05 fof(cc19_membered,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( v4_membered(A) % 60.01/60.06 => ! [B] : % 60.01/60.06 ( m1_subset_1(B,k1_zfmisc_1(A)) % 60.01/60.06 => ( v1_membered(B) % 60.01/60.06 & v2_membered(B) % 60.01/60.06 & v3_membered(B) % 60.01/60.06 & v4_membered(B) ) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc1_finset_1,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( v1_xboole_0(A) % 60.01/60.06 => v1_finset_1(A) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc1_finsub_1,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( v4_finsub_1(A) % 60.01/60.06 => ( v1_finsub_1(A) % 60.01/60.06 & v3_finsub_1(A) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc1_funct_2,axiom, % 60.01/60.06 ! [A,B,C] : % 60.01/60.06 ( m1_relset_1(C,A,B) % 60.01/60.06 => ( ( v1_funct_1(C) % 60.01/60.06 & v1_partfun1(C,A,B) ) % 60.01/60.06 => ( v1_funct_1(C) % 60.01/60.06 & v1_funct_2(C,A,B) ) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc1_lattices,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( l3_lattices(A) % 60.01/60.06 => ( ( ~ v3_struct_0(A) % 60.01/60.06 & v10_lattices(A) ) % 60.01/60.06 => ( ~ v3_struct_0(A) % 60.01/60.06 & v4_lattices(A) % 60.01/60.06 & v5_lattices(A) % 60.01/60.06 & v6_lattices(A) % 60.01/60.06 & v7_lattices(A) % 60.01/60.06 & v8_lattices(A) % 60.01/60.06 & v9_lattices(A) ) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc1_membered,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( v5_membered(A) % 60.01/60.06 => v4_membered(A) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc1_relset_1,axiom, % 60.01/60.06 ! [A,B,C] : % 60.01/60.06 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 60.01/60.06 => v1_relat_1(C) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc20_membered,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( v5_membered(A) % 60.01/60.06 => ! [B] : % 60.01/60.06 ( m1_subset_1(B,k1_zfmisc_1(A)) % 60.01/60.06 => ( v1_membered(B) % 60.01/60.06 & v2_membered(B) % 60.01/60.06 & v3_membered(B) % 60.01/60.06 & v4_membered(B) % 60.01/60.06 & v5_membered(B) ) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc2_finset_1,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( v1_finset_1(A) % 60.01/60.06 => ! [B] : % 60.01/60.06 ( m1_subset_1(B,k1_zfmisc_1(A)) % 60.01/60.06 => v1_finset_1(B) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc2_finsub_1,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( ( v1_finsub_1(A) % 60.01/60.06 & v3_finsub_1(A) ) % 60.01/60.06 => v4_finsub_1(A) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc2_lattices,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( l3_lattices(A) % 60.01/60.06 => ( ( ~ v3_struct_0(A) % 60.01/60.06 & v4_lattices(A) % 60.01/60.06 & v5_lattices(A) % 60.01/60.06 & v6_lattices(A) % 60.01/60.06 & v7_lattices(A) % 60.01/60.06 & v8_lattices(A) % 60.01/60.06 & v9_lattices(A) ) % 60.01/60.06 => ( ~ v3_struct_0(A) % 60.01/60.06 & v10_lattices(A) ) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc2_membered,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( v4_membered(A) % 60.01/60.06 => v3_membered(A) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc3_lattices,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( l3_lattices(A) % 60.01/60.06 => ( ( ~ v3_struct_0(A) % 60.01/60.06 & v13_lattices(A) % 60.01/60.06 & v14_lattices(A) ) % 60.01/60.06 => ( ~ v3_struct_0(A) % 60.01/60.06 & v15_lattices(A) ) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc3_membered,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( v3_membered(A) % 60.01/60.06 => v2_membered(A) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc4_lattices,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( l3_lattices(A) % 60.01/60.06 => ( ( ~ v3_struct_0(A) % 60.01/60.06 & v15_lattices(A) ) % 60.01/60.06 => ( ~ v3_struct_0(A) % 60.01/60.06 & v13_lattices(A) % 60.01/60.06 & v14_lattices(A) ) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc4_membered,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( v2_membered(A) % 60.01/60.06 => v1_membered(A) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc5_funct_2,axiom, % 60.01/60.06 ! [A,B] : % 60.01/60.06 ( ~ v1_xboole_0(B) % 60.01/60.06 => ! [C] : % 60.01/60.06 ( m1_relset_1(C,A,B) % 60.01/60.06 => ( ( v1_funct_1(C) % 60.01/60.06 & v1_funct_2(C,A,B) ) % 60.01/60.06 => ( v1_funct_1(C) % 60.01/60.06 & v1_partfun1(C,A,B) % 60.01/60.06 & v1_funct_2(C,A,B) ) ) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc5_lattices,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( l3_lattices(A) % 60.01/60.06 => ( ( ~ v3_struct_0(A) % 60.01/60.06 & v17_lattices(A) ) % 60.01/60.06 => ( ~ v3_struct_0(A) % 60.01/60.06 & v11_lattices(A) % 60.01/60.06 & v13_lattices(A) % 60.01/60.06 & v14_lattices(A) % 60.01/60.06 & v15_lattices(A) % 60.01/60.06 & v16_lattices(A) ) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc6_funct_2,axiom, % 60.01/60.06 ! [A,B] : % 60.01/60.06 ( ( ~ v1_xboole_0(A) % 60.01/60.06 & ~ v1_xboole_0(B) ) % 60.01/60.06 => ! [C] : % 60.01/60.06 ( m1_relset_1(C,A,B) % 60.01/60.06 => ( ( v1_funct_1(C) % 60.01/60.06 & v1_funct_2(C,A,B) ) % 60.01/60.06 => ( v1_funct_1(C) % 60.01/60.06 & ~ v1_xboole_0(C) % 60.01/60.06 & v1_partfun1(C,A,B) % 60.01/60.06 & v1_funct_2(C,A,B) ) ) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc6_lattices,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( l3_lattices(A) % 60.01/60.06 => ( ( ~ v3_struct_0(A) % 60.01/60.06 & v11_lattices(A) % 60.01/60.06 & v15_lattices(A) % 60.01/60.06 & v16_lattices(A) ) % 60.01/60.06 => ( ~ v3_struct_0(A) % 60.01/60.06 & v17_lattices(A) ) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(cc7_lattices,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( l3_lattices(A) % 60.01/60.06 => ( ( ~ v3_struct_0(A) % 60.01/60.06 & v10_lattices(A) % 60.01/60.06 & v11_lattices(A) ) % 60.01/60.06 => ( ~ v3_struct_0(A) % 60.01/60.06 & v4_lattices(A) % 60.01/60.06 & v5_lattices(A) % 60.01/60.06 & v6_lattices(A) % 60.01/60.06 & v7_lattices(A) % 60.01/60.06 & v8_lattices(A) % 60.01/60.06 & v9_lattices(A) % 60.01/60.06 & v10_lattices(A) % 60.01/60.06 & v12_lattices(A) ) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(d1_lopclset,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( ( ~ v3_struct_0(A) % 60.01/60.06 & l1_pre_topc(A) ) % 60.01/60.06 => k1_lopclset(A) = a_1_0_lopclset(A) ) ). % 60.01/60.06 % 60.01/60.06 fof(d4_lopclset,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( ( ~ v3_struct_0(A) % 60.01/60.06 & v2_pre_topc(A) % 60.01/60.06 & l1_pre_topc(A) ) % 60.01/60.06 => k6_lopclset(A) = g3_lattices(k1_lopclset(A),k4_lopclset(A),k5_lopclset(A)) ) ). % 60.01/60.06 % 60.01/60.06 fof(d9_lopclset,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( ( ~ v3_struct_0(A) % 60.01/60.06 & v10_lattices(A) % 60.01/60.06 & v17_lattices(A) % 60.01/60.06 & ~ v3_realset2(A) % 60.01/60.06 & l3_lattices(A) ) % 60.01/60.06 => k12_lopclset(A) = k6_lopclset(k11_lopclset(A)) ) ). % 60.01/60.06 % 60.01/60.06 fof(dt_g1_pre_topc,axiom, % 60.01/60.06 ! [A,B] : % 60.01/60.06 ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) % 60.01/60.06 => ( v1_pre_topc(g1_pre_topc(A,B)) % 60.01/60.06 & l1_pre_topc(g1_pre_topc(A,B)) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(dt_g3_lattices,axiom, % 60.01/60.06 ! [A,B,C] : % 60.01/60.06 ( ( v1_funct_1(B) % 60.01/60.06 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 60.01/60.06 & m1_relset_1(B,k2_zfmisc_1(A,A),A) % 60.01/60.06 & v1_funct_1(C) % 60.01/60.06 & v1_funct_2(C,k2_zfmisc_1(A,A),A) % 60.01/60.06 & m1_relset_1(C,k2_zfmisc_1(A,A),A) ) % 60.01/60.06 => ( v3_lattices(g3_lattices(A,B,C)) % 60.01/60.06 & l3_lattices(g3_lattices(A,B,C)) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(dt_k11_lopclset,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( ( ~ v3_struct_0(A) % 60.01/60.06 & v10_lattices(A) % 60.01/60.06 & v17_lattices(A) % 60.01/60.06 & ~ v3_realset2(A) % 60.01/60.06 & l3_lattices(A) ) % 60.01/60.06 => ( v1_pre_topc(k11_lopclset(A)) % 60.01/60.06 & v2_pre_topc(k11_lopclset(A)) % 60.01/60.06 & l1_pre_topc(k11_lopclset(A)) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(dt_k12_lopclset,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( ( ~ v3_struct_0(A) % 60.01/60.06 & v10_lattices(A) % 60.01/60.06 & v17_lattices(A) % 60.01/60.06 & ~ v3_realset2(A) % 60.01/60.06 & l3_lattices(A) ) % 60.01/60.06 => ( ~ v3_struct_0(k12_lopclset(A)) % 60.01/60.06 & v10_lattices(k12_lopclset(A)) % 60.01/60.06 & l3_lattices(k12_lopclset(A)) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(dt_k1_lopclset,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( ( ~ v3_struct_0(A) % 60.01/60.06 & l1_pre_topc(A) ) % 60.01/60.06 => m1_subset_1(k1_lopclset(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) ) ). % 60.01/60.06 % 60.01/60.06 fof(dt_k1_xboole_0,axiom, % 60.01/60.06 $true ). % 60.01/60.06 % 60.01/60.06 fof(dt_k1_zfmisc_1,axiom, % 60.01/60.06 $true ). % 60.01/60.06 % 60.01/60.06 fof(dt_k2_zfmisc_1,axiom, % 60.01/60.06 $true ). % 60.01/60.06 % 60.01/60.06 fof(dt_k4_lopclset,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( ( ~ v3_struct_0(A) % 60.01/60.06 & v2_pre_topc(A) % 60.01/60.06 & l1_pre_topc(A) ) % 60.01/60.06 => ( v1_funct_1(k4_lopclset(A)) % 60.01/60.06 & v1_funct_2(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A)) % 60.01/60.06 & m2_relset_1(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A)) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(dt_k5_lopclset,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( ( ~ v3_struct_0(A) % 60.01/60.06 & v2_pre_topc(A) % 60.01/60.06 & l1_pre_topc(A) ) % 60.01/60.06 => ( v1_funct_1(k5_lopclset(A)) % 60.01/60.06 & v1_funct_2(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A)) % 60.01/60.06 & m2_relset_1(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A)) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(dt_k6_lopclset,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( ( ~ v3_struct_0(A) % 60.01/60.06 & v2_pre_topc(A) % 60.01/60.06 & l1_pre_topc(A) ) % 60.01/60.06 => ( ~ v3_struct_0(k6_lopclset(A)) % 60.01/60.06 & v10_lattices(k6_lopclset(A)) % 60.01/60.06 & l3_lattices(k6_lopclset(A)) ) ) ). % 60.01/60.06 % 60.01/60.06 fof(dt_l1_lattices,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( l1_lattices(A) % 60.01/60.06 => l1_struct_0(A) ) ). % 60.01/60.06 % 60.01/60.06 fof(dt_l1_pre_topc,axiom, % 60.01/60.06 ! [A] : % 60.01/60.06 ( l1_pre_topc(A) % 60.01/60.06 => l1_struct_0(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(dt_l1_struct_0,axiom, % 60.01/60.07 $true ). % 60.01/60.07 % 60.01/60.07 fof(dt_l2_lattices,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( l2_lattices(A) % 60.01/60.07 => l1_struct_0(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(dt_l3_lattices,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( l3_lattices(A) % 60.01/60.07 => ( l1_lattices(A) % 60.01/60.07 & l2_lattices(A) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(dt_m1_relset_1,axiom, % 60.01/60.07 $true ). % 60.01/60.07 % 60.01/60.07 fof(dt_m1_subset_1,axiom, % 60.01/60.07 $true ). % 60.01/60.07 % 60.01/60.07 fof(dt_m2_relset_1,axiom, % 60.01/60.07 ! [A,B,C] : % 60.01/60.07 ( m2_relset_1(C,A,B) % 60.01/60.07 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 60.01/60.07 % 60.01/60.07 fof(dt_u1_lattices,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( l1_lattices(A) % 60.01/60.07 => ( v1_funct_1(u1_lattices(A)) % 60.01/60.07 & v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 60.01/60.07 & m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(dt_u1_pre_topc,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( l1_pre_topc(A) % 60.01/60.07 => m1_subset_1(u1_pre_topc(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) ) ). % 60.01/60.07 % 60.01/60.07 fof(dt_u1_struct_0,axiom, % 60.01/60.07 $true ). % 60.01/60.07 % 60.01/60.07 fof(dt_u2_lattices,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( l2_lattices(A) % 60.01/60.07 => ( v1_funct_1(u2_lattices(A)) % 60.01/60.07 & v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 60.01/60.07 & m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(existence_l1_lattices,axiom, % 60.01/60.07 ? [A] : l1_lattices(A) ). % 60.01/60.07 % 60.01/60.07 fof(existence_l1_pre_topc,axiom, % 60.01/60.07 ? [A] : l1_pre_topc(A) ). % 60.01/60.07 % 60.01/60.07 fof(existence_l1_struct_0,axiom, % 60.01/60.07 ? [A] : l1_struct_0(A) ). % 60.01/60.07 % 60.01/60.07 fof(existence_l2_lattices,axiom, % 60.01/60.07 ? [A] : l2_lattices(A) ). % 60.01/60.07 % 60.01/60.07 fof(existence_l3_lattices,axiom, % 60.01/60.07 ? [A] : l3_lattices(A) ). % 60.01/60.07 % 60.01/60.07 fof(existence_m1_relset_1,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ? [C] : m1_relset_1(C,A,B) ). % 60.01/60.07 % 60.01/60.07 fof(existence_m1_subset_1,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ? [B] : m1_subset_1(B,A) ). % 60.01/60.07 % 60.01/60.07 fof(existence_m2_relset_1,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ? [C] : m2_relset_1(C,A,B) ). % 60.01/60.07 % 60.01/60.07 fof(fc14_finset_1,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ( ( v1_finset_1(A) % 60.01/60.07 & v1_finset_1(B) ) % 60.01/60.07 => v1_finset_1(k2_zfmisc_1(A,B)) ) ). % 60.01/60.07 % 60.01/60.07 fof(fc1_finsub_1,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( ~ v1_xboole_0(k1_zfmisc_1(A)) % 60.01/60.07 & v1_finsub_1(k1_zfmisc_1(A)) % 60.01/60.07 & v3_finsub_1(k1_zfmisc_1(A)) % 60.01/60.07 & v4_finsub_1(k1_zfmisc_1(A)) ) ). % 60.01/60.07 % 60.01/60.07 fof(fc1_lopclset,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( ( ~ v3_struct_0(A) % 60.01/60.07 & v2_pre_topc(A) % 60.01/60.07 & l1_pre_topc(A) ) % 60.01/60.07 => ~ v1_xboole_0(k1_lopclset(A)) ) ). % 60.01/60.07 % 60.01/60.07 fof(fc1_struct_0,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( ( ~ v3_struct_0(A) % 60.01/60.07 & l1_struct_0(A) ) % 60.01/60.07 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 60.01/60.07 % 60.01/60.07 fof(fc3_lattices,axiom, % 60.01/60.07 ! [A,B,C] : % 60.01/60.07 ( ( ~ v1_xboole_0(A) % 60.01/60.07 & v1_funct_1(B) % 60.01/60.07 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 60.01/60.07 & m1_relset_1(B,k2_zfmisc_1(A,A),A) % 60.01/60.07 & v1_funct_1(C) % 60.01/60.07 & v1_funct_2(C,k2_zfmisc_1(A,A),A) % 60.01/60.07 & m1_relset_1(C,k2_zfmisc_1(A,A),A) ) % 60.01/60.07 => ( ~ v3_struct_0(g3_lattices(A,B,C)) % 60.01/60.07 & v3_lattices(g3_lattices(A,B,C)) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(fc4_lopclset,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( ( ~ v3_struct_0(A) % 60.01/60.07 & v10_lattices(A) % 60.01/60.07 & v17_lattices(A) % 60.01/60.07 & ~ v3_realset2(A) % 60.01/60.07 & l3_lattices(A) ) % 60.01/60.07 => ( ~ v3_struct_0(k11_lopclset(A)) % 60.01/60.07 & v1_pre_topc(k11_lopclset(A)) % 60.01/60.07 & v2_pre_topc(k11_lopclset(A)) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(fc6_membered,axiom, % 60.01/60.07 ( v1_xboole_0(k1_xboole_0) % 60.01/60.07 & v1_membered(k1_xboole_0) % 60.01/60.07 & v2_membered(k1_xboole_0) % 60.01/60.07 & v3_membered(k1_xboole_0) % 60.01/60.07 & v4_membered(k1_xboole_0) % 60.01/60.07 & v5_membered(k1_xboole_0) ) ). % 60.01/60.07 % 60.01/60.07 fof(fraenkel_a_1_0_lopclset,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ( ( ~ v3_struct_0(B) % 60.01/60.07 & l1_pre_topc(B) ) % 60.01/60.07 => ( r2_hidden(A,a_1_0_lopclset(B)) % 60.01/60.07 <=> ? [C] : % 60.01/60.07 ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) % 60.01/60.07 & A = C % 60.01/60.07 & v3_pre_topc(C,B) % 60.01/60.07 & v4_pre_topc(C,B) ) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(free_g1_pre_topc,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) % 60.01/60.07 => ! [C,D] : % 60.01/60.07 ( g1_pre_topc(A,B) = g1_pre_topc(C,D) % 60.01/60.07 => ( A = C % 60.01/60.07 & B = D ) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(free_g3_lattices,axiom, % 60.01/60.07 ! [A,B,C] : % 60.01/60.07 ( ( v1_funct_1(B) % 60.01/60.07 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 60.01/60.07 & m1_relset_1(B,k2_zfmisc_1(A,A),A) % 60.01/60.07 & v1_funct_1(C) % 60.01/60.07 & v1_funct_2(C,k2_zfmisc_1(A,A),A) % 60.01/60.07 & m1_relset_1(C,k2_zfmisc_1(A,A),A) ) % 60.01/60.07 => ! [D,E,F] : % 60.01/60.07 ( g3_lattices(A,B,C) = g3_lattices(D,E,F) % 60.01/60.07 => ( A = D % 60.01/60.07 & B = E % 60.01/60.07 & C = F ) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc10_lattices,axiom, % 60.01/60.07 ? [A] : % 60.01/60.07 ( l3_lattices(A) % 60.01/60.07 & ~ v3_struct_0(A) % 60.01/60.07 & v3_lattices(A) % 60.01/60.07 & v4_lattices(A) % 60.01/60.07 & v5_lattices(A) % 60.01/60.07 & v6_lattices(A) % 60.01/60.07 & v7_lattices(A) % 60.01/60.07 & v8_lattices(A) % 60.01/60.07 & v9_lattices(A) % 60.01/60.07 & v10_lattices(A) % 60.01/60.07 & v11_lattices(A) % 60.01/60.07 & v12_lattices(A) % 60.01/60.07 & v13_lattices(A) % 60.01/60.07 & v14_lattices(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc11_lattices,axiom, % 60.01/60.07 ? [A] : % 60.01/60.07 ( l3_lattices(A) % 60.01/60.07 & ~ v3_struct_0(A) % 60.01/60.07 & v3_lattices(A) % 60.01/60.07 & v4_lattices(A) % 60.01/60.07 & v5_lattices(A) % 60.01/60.07 & v6_lattices(A) % 60.01/60.07 & v7_lattices(A) % 60.01/60.07 & v8_lattices(A) % 60.01/60.07 & v9_lattices(A) % 60.01/60.07 & v10_lattices(A) % 60.01/60.07 & v13_lattices(A) % 60.01/60.07 & v14_lattices(A) % 60.01/60.07 & v15_lattices(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc12_lattices,axiom, % 60.01/60.07 ? [A] : % 60.01/60.07 ( l3_lattices(A) % 60.01/60.07 & ~ v3_struct_0(A) % 60.01/60.07 & v3_lattices(A) % 60.01/60.07 & v4_lattices(A) % 60.01/60.07 & v5_lattices(A) % 60.01/60.07 & v6_lattices(A) % 60.01/60.07 & v7_lattices(A) % 60.01/60.07 & v8_lattices(A) % 60.01/60.07 & v9_lattices(A) % 60.01/60.07 & v10_lattices(A) % 60.01/60.07 & v13_lattices(A) % 60.01/60.07 & v14_lattices(A) % 60.01/60.07 & v15_lattices(A) % 60.01/60.07 & v16_lattices(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc13_lattices,axiom, % 60.01/60.07 ? [A] : % 60.01/60.07 ( l3_lattices(A) % 60.01/60.07 & ~ v3_struct_0(A) % 60.01/60.07 & v3_lattices(A) % 60.01/60.07 & v4_lattices(A) % 60.01/60.07 & v5_lattices(A) % 60.01/60.07 & v6_lattices(A) % 60.01/60.07 & v7_lattices(A) % 60.01/60.07 & v8_lattices(A) % 60.01/60.07 & v9_lattices(A) % 60.01/60.07 & v10_lattices(A) % 60.01/60.07 & v11_lattices(A) % 60.01/60.07 & v13_lattices(A) % 60.01/60.07 & v14_lattices(A) % 60.01/60.07 & v15_lattices(A) % 60.01/60.07 & v16_lattices(A) % 60.01/60.07 & v17_lattices(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc1_finset_1,axiom, % 60.01/60.07 ? [A] : % 60.01/60.07 ( ~ v1_xboole_0(A) % 60.01/60.07 & v1_finset_1(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc1_funct_2,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ? [C] : % 60.01/60.07 ( m1_relset_1(C,A,B) % 60.01/60.07 & v1_relat_1(C) % 60.01/60.07 & v1_funct_1(C) % 60.01/60.07 & v1_funct_2(C,A,B) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc1_lopclset,axiom, % 60.01/60.07 ? [A] : % 60.01/60.07 ( l3_lattices(A) % 60.01/60.07 & ~ v3_struct_0(A) % 60.01/60.07 & v4_lattices(A) % 60.01/60.07 & v5_lattices(A) % 60.01/60.07 & v6_lattices(A) % 60.01/60.07 & v7_lattices(A) % 60.01/60.07 & v8_lattices(A) % 60.01/60.07 & v9_lattices(A) % 60.01/60.07 & v10_lattices(A) % 60.01/60.07 & v11_lattices(A) % 60.01/60.07 & v12_lattices(A) % 60.01/60.07 & v13_lattices(A) % 60.01/60.07 & v14_lattices(A) % 60.01/60.07 & v15_lattices(A) % 60.01/60.07 & v16_lattices(A) % 60.01/60.07 & v17_lattices(A) % 60.01/60.07 & ~ v3_realset2(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc1_membered,axiom, % 60.01/60.07 ? [A] : % 60.01/60.07 ( ~ v1_xboole_0(A) % 60.01/60.07 & v1_membered(A) % 60.01/60.07 & v2_membered(A) % 60.01/60.07 & v3_membered(A) % 60.01/60.07 & v4_membered(A) % 60.01/60.07 & v5_membered(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc1_pre_topc,axiom, % 60.01/60.07 ? [A] : % 60.01/60.07 ( l1_pre_topc(A) % 60.01/60.07 & v1_pre_topc(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc2_partfun1,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ? [C] : % 60.01/60.07 ( m1_relset_1(C,A,B) % 60.01/60.07 & v1_relat_1(C) % 60.01/60.07 & v1_funct_1(C) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc2_pre_topc,axiom, % 60.01/60.07 ? [A] : % 60.01/60.07 ( l1_pre_topc(A) % 60.01/60.07 & ~ v3_struct_0(A) % 60.01/60.07 & v1_pre_topc(A) % 60.01/60.07 & v2_pre_topc(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc3_finset_1,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( ~ v1_xboole_0(A) % 60.01/60.07 => ? [B] : % 60.01/60.07 ( m1_subset_1(B,k1_zfmisc_1(A)) % 60.01/60.07 & ~ v1_xboole_0(B) % 60.01/60.07 & v1_finset_1(B) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc3_lattices,axiom, % 60.01/60.07 ? [A] : % 60.01/60.07 ( l3_lattices(A) % 60.01/60.07 & v3_lattices(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc3_struct_0,axiom, % 60.01/60.07 ? [A] : % 60.01/60.07 ( l1_struct_0(A) % 60.01/60.07 & ~ v3_struct_0(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc4_finset_1,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( ~ v1_xboole_0(A) % 60.01/60.07 => ? [B] : % 60.01/60.07 ( m1_subset_1(B,k1_zfmisc_1(A)) % 60.01/60.07 & ~ v1_xboole_0(B) % 60.01/60.07 & v1_finset_1(B) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc5_struct_0,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( ( ~ v3_struct_0(A) % 60.01/60.07 & l1_struct_0(A) ) % 60.01/60.07 => ? [B] : % 60.01/60.07 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 60.01/60.07 & ~ v1_xboole_0(B) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc6_lattices,axiom, % 60.01/60.07 ? [A] : % 60.01/60.07 ( l3_lattices(A) % 60.01/60.07 & ~ v3_struct_0(A) % 60.01/60.07 & v3_lattices(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc6_pre_topc,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( ( v2_pre_topc(A) % 60.01/60.07 & l1_pre_topc(A) ) % 60.01/60.07 => ? [B] : % 60.01/60.07 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 60.01/60.07 & v4_pre_topc(B,A) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc7_pre_topc,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( ( ~ v3_struct_0(A) % 60.01/60.07 & v2_pre_topc(A) % 60.01/60.07 & l1_pre_topc(A) ) % 60.01/60.07 => ? [B] : % 60.01/60.07 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 60.01/60.07 & ~ v1_xboole_0(B) % 60.01/60.07 & v4_pre_topc(B,A) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(rc9_lattices,axiom, % 60.01/60.07 ? [A] : % 60.01/60.07 ( l3_lattices(A) % 60.01/60.07 & ~ v3_struct_0(A) % 60.01/60.07 & v3_lattices(A) % 60.01/60.07 & v4_lattices(A) % 60.01/60.07 & v5_lattices(A) % 60.01/60.07 & v6_lattices(A) % 60.01/60.07 & v7_lattices(A) % 60.01/60.07 & v8_lattices(A) % 60.01/60.07 & v9_lattices(A) % 60.01/60.07 & v10_lattices(A) ) ). % 60.01/60.07 % 60.01/60.07 fof(redefinition_m2_relset_1,axiom, % 60.01/60.07 ! [A,B,C] : % 60.01/60.07 ( m2_relset_1(C,A,B) % 60.01/60.07 <=> m1_relset_1(C,A,B) ) ). % 60.01/60.07 % 60.01/60.07 fof(reflexivity_r1_filter_1,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ( ( ~ v3_struct_0(A) % 60.01/60.07 & v10_lattices(A) % 60.01/60.07 & l3_lattices(A) % 60.01/60.07 & ~ v3_struct_0(B) % 60.01/60.07 & v10_lattices(B) % 60.01/60.07 & l3_lattices(B) ) % 60.01/60.07 => r1_filter_1(A,A) ) ). % 60.01/60.07 % 60.01/60.07 fof(reflexivity_r1_tarski,axiom, % 60.01/60.07 ! [A,B] : r1_tarski(A,A) ). % 60.01/60.07 % 60.01/60.07 fof(symmetry_r1_filter_1,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ( ( ~ v3_struct_0(A) % 60.01/60.07 & v10_lattices(A) % 60.01/60.07 & l3_lattices(A) % 60.01/60.07 & ~ v3_struct_0(B) % 60.01/60.07 & v10_lattices(B) % 60.01/60.07 & l3_lattices(B) ) % 60.01/60.07 => ( r1_filter_1(A,B) % 60.01/60.07 => r1_filter_1(B,A) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(t1_subset,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ( r2_hidden(A,B) % 60.01/60.07 => m1_subset_1(A,B) ) ). % 60.01/60.07 % 60.01/60.07 fof(t2_subset,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ( m1_subset_1(A,B) % 60.01/60.07 => ( v1_xboole_0(B) % 60.01/60.07 | r2_hidden(A,B) ) ) ). % 60.01/60.07 % 60.01/60.07 fof(t2_tarski,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ( ! [C] : % 60.01/60.07 ( r2_hidden(C,A) % 60.01/60.07 <=> r2_hidden(C,B) ) % 60.01/60.07 => A = B ) ). % 60.01/60.07 % 60.01/60.07 fof(t3_subset,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ( m1_subset_1(A,k1_zfmisc_1(B)) % 60.01/60.07 <=> r1_tarski(A,B) ) ). % 60.01/60.07 % 60.01/60.07 fof(t43_lopclset,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( ( ~ v3_struct_0(A) % 60.01/60.07 & v10_lattices(A) % 60.01/60.07 & v17_lattices(A) % 60.01/60.07 & ~ v3_realset2(A) % 60.01/60.07 & l3_lattices(A) ) % 60.01/60.07 => r1_filter_1(A,k12_lopclset(A)) ) ). % 60.01/60.07 % 60.01/60.07 fof(t4_subset,axiom, % 60.01/60.07 ! [A,B,C] : % 60.01/60.07 ( ( r2_hidden(A,B) % 60.01/60.07 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 60.01/60.07 => m1_subset_1(A,C) ) ). % 60.01/60.07 % 60.01/60.07 fof(t5_subset,axiom, % 60.01/60.07 ! [A,B,C] : % 60.01/60.07 ~ ( r2_hidden(A,B) % 60.01/60.07 & m1_subset_1(B,k1_zfmisc_1(C)) % 60.01/60.07 & v1_xboole_0(C) ) ). % 60.01/60.07 % 60.01/60.07 fof(t6_boole,axiom, % 60.01/60.07 ! [A] : % 60.01/60.07 ( v1_xboole_0(A) % 60.01/60.07 => A = k1_xboole_0 ) ). % 60.01/60.07 % 60.01/60.07 fof(t7_boole,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ~ ( r2_hidden(A,B) % 60.01/60.07 & v1_xboole_0(B) ) ). % 60.01/60.07 % 60.01/60.07 fof(t8_boole,axiom, % 60.01/60.07 ! [A,B] : % 60.01/60.07 ~ ( v1_xboole_0(A) % 60.01/60.07 & A != B % 60.01/60.07 & v1_xboole_0(B) ) ). % 60.01/60.07 % 60.01/60.07 %------------------------------------------------------------------------------ % 60.01/60.07 %------------------------------------------- % 60.01/60.07 % Proof found % 60.01/60.07 % SZS status Theorem for theBenchmark % 60.01/60.07 % SZS output start Proof % 60.01/60.07 %ClaNum:400(EqnAxiom:105) % 60.01/60.07 %VarNum:823(SingletonVarNum:269) % 60.01/60.07 %MaxLitNum:9 % 60.01/60.07 %MaxfuncDepth:3 % 60.01/60.07 %SharedTerms:141 % 60.01/60.07 %goalClause: 106 113 116 227 237 353 % 60.01/60.07 %singleGoalClaCount:5 % 60.01/60.07 [106]P1(a1) % 60.01/60.07 [107]P1(a2) % 60.01/60.07 [108]P1(a5) % 60.01/60.07 [109]P1(a6) % 60.01/60.07 [110]P1(a7) % 60.01/60.07 [111]P1(a8) % 60.01/60.07 [112]P1(a13) % 60.01/60.07 [113]P13(a1) % 60.01/60.07 [114]P13(a7) % 60.01/60.07 [115]P13(a8) % 60.01/60.07 [116]P2(a1) % 60.01/60.07 [117]P2(a25) % 60.01/60.07 [118]P2(a2) % 60.01/60.07 [119]P2(a5) % 60.01/60.07 [120]P2(a6) % 60.01/60.07 [121]P2(a7) % 60.01/60.07 [122]P2(a8) % 60.01/60.07 [123]P2(a14) % 60.01/60.07 [124]P2(a18) % 60.01/60.07 [125]P2(a13) % 60.01/60.07 [126]P20(a15) % 60.01/60.07 [127]P3(a26) % 60.01/60.07 [128]P3(a11) % 60.01/60.07 [129]P3(a15) % 60.01/60.07 [130]P21(a11) % 60.01/60.07 [131]P21(a15) % 60.01/60.07 [132]P35(a2) % 60.01/60.07 [133]P35(a5) % 60.01/60.07 [134]P35(a6) % 60.01/60.07 [135]P35(a7) % 60.01/60.07 [136]P35(a14) % 60.01/60.07 [137]P35(a18) % 60.01/60.07 [138]P35(a13) % 60.01/60.07 [139]P22(a30) % 60.01/60.07 [140]P22(a12) % 60.01/60.07 [141]P29(a30) % 60.01/60.07 [142]P29(a12) % 60.01/60.07 [143]P37(a30) % 60.01/60.07 [144]P37(a12) % 60.01/60.08 [145]P38(a30) % 60.01/60.08 [146]P38(a12) % 60.01/60.08 [147]P44(a30) % 60.01/60.08 [148]P44(a12) % 60.01/60.08 [149]P30(a30) % 60.01/60.08 [150]P23(a9) % 60.01/60.08 [151]P39(a2) % 60.01/60.08 [152]P39(a5) % 60.01/60.08 [153]P39(a6) % 60.01/60.08 [154]P39(a7) % 60.01/60.08 [155]P39(a8) % 60.01/60.08 [156]P39(a13) % 60.01/60.08 [157]P45(a2) % 60.01/60.08 [158]P45(a5) % 60.01/60.08 [159]P45(a6) % 60.01/60.08 [160]P45(a7) % 60.01/60.08 [161]P45(a8) % 60.01/60.08 [162]P45(a13) % 60.01/60.08 [163]P48(a2) % 60.01/60.08 [164]P48(a5) % 60.01/60.08 [165]P48(a6) % 60.01/60.08 [166]P48(a7) % 60.01/60.08 [167]P48(a8) % 60.01/60.08 [168]P48(a13) % 60.01/60.08 [169]P49(a2) % 60.01/60.08 [170]P49(a5) % 60.01/60.08 [171]P49(a6) % 60.01/60.08 [172]P49(a7) % 60.01/60.08 [173]P49(a8) % 60.01/60.08 [174]P49(a13) % 60.01/60.08 [175]P50(a2) % 60.01/60.08 [176]P50(a5) % 60.01/60.08 [177]P50(a6) % 60.01/60.08 [178]P50(a7) % 60.01/60.08 [179]P50(a8) % 60.01/60.08 [180]P50(a13) % 60.01/60.08 [181]P51(a2) % 60.01/60.08 [182]P51(a5) % 60.01/60.08 [183]P51(a6) % 60.01/60.08 [184]P51(a7) % 60.01/60.08 [185]P51(a8) % 60.01/60.08 [186]P51(a13) % 60.01/60.08 [187]P14(a2) % 60.01/60.08 [188]P14(a5) % 60.01/60.08 [189]P14(a6) % 60.01/60.08 [190]P14(a7) % 60.01/60.08 [191]P14(a8) % 60.01/60.08 [192]P17(a2) % 60.01/60.08 [193]P17(a5) % 60.01/60.08 [194]P17(a6) % 60.01/60.08 [195]P17(a7) % 60.01/60.08 [196]P17(a8) % 60.01/60.08 [197]P18(a5) % 60.01/60.08 [198]P18(a6) % 60.01/60.08 [199]P18(a7) % 60.01/60.08 [200]P18(a8) % 60.01/60.08 [201]P15(a2) % 60.01/60.08 [202]P15(a7) % 60.01/60.08 [203]P15(a8) % 60.01/60.08 [204]P19(a6) % 60.01/60.08 [205]P19(a7) % 60.01/60.08 [206]P19(a8) % 60.01/60.08 [207]P16(a2) % 60.01/60.08 [208]P16(a8) % 60.01/60.08 [209]P4(a22) % 60.01/60.08 [210]P5(a28) % 60.01/60.08 [211]P5(a19) % 60.01/60.08 [212]P6(a29) % 60.01/60.08 [227]~P41(a1) % 60.01/60.08 [228]~P41(a2) % 60.01/60.08 [229]~P41(a5) % 60.01/60.08 [230]~P41(a6) % 60.01/60.08 [231]~P41(a7) % 60.01/60.08 [232]~P41(a8) % 60.01/60.08 [233]~P41(a15) % 60.01/60.08 [234]~P41(a19) % 60.01/60.08 [235]~P41(a18) % 60.01/60.08 [236]~P41(a13) % 60.01/60.08 [237]~P42(a1) % 60.01/60.08 [238]~P42(a8) % 60.01/60.08 [239]~P30(a9) % 60.01/60.08 [240]~P30(a12) % 60.01/60.08 [216]P7(x2161,x2161) % 60.01/60.08 [213]P40(f39(x2131)) % 60.01/60.08 [214]P24(f39(x2141)) % 60.01/60.08 [215]P36(f39(x2151)) % 60.01/60.08 [217]P8(f31(x2171),x2171) % 60.01/60.08 [241]~P30(f39(x2411)) % 60.01/60.08 [218]P25(f10(x2181,x2182)) % 60.01/60.08 [219]P25(f16(x2191,x2192)) % 60.01/60.08 [220]P31(f10(x2201,x2202)) % 60.01/60.08 [221]P31(f16(x2211,x2212)) % 60.01/60.08 [222]P9(f32(x2221,x2222),x2221,x2222) % 60.01/60.08 [223]P9(f10(x2231,x2232),x2231,x2232) % 60.01/60.08 [224]P9(f16(x2241,x2242),x2241,x2242) % 60.01/60.08 [225]P26(f10(x2251,x2252),x2251,x2252) % 60.01/60.08 [226]P10(f33(x2261,x2262),x2261,x2262) % 60.01/60.08 [242]~P30(x2421)+E(x2421,a30) % 60.01/60.08 [243]~P29(x2431)+P22(x2431) % 60.01/60.08 [244]~P30(x2441)+P22(x2441) % 60.01/60.08 [245]~P37(x2451)+P29(x2451) % 60.01/60.08 [246]~P30(x2461)+P29(x2461) % 60.01/60.08 [247]~P38(x2471)+P37(x2471) % 60.01/60.08 [248]~P30(x2481)+P37(x2481) % 60.01/60.08 [249]~P44(x2491)+P38(x2491) % 60.01/60.08 [250]~P30(x2501)+P38(x2501) % 60.01/60.08 [251]~P30(x2511)+P44(x2511) % 60.01/60.08 [252]~P30(x2521)+P23(x2521) % 60.01/60.08 [253]~P40(x2531)+P24(x2531) % 60.01/60.08 [254]~P40(x2541)+P36(x2541) % 60.01/60.08 [255]~P2(x2551)+P4(x2551) % 60.01/60.08 [256]~P3(x2561)+P5(x2561) % 60.01/60.08 [257]~P4(x2571)+P5(x2571) % 60.01/60.08 [258]~P6(x2581)+P5(x2581) % 60.01/60.08 [259]~P2(x2591)+P6(x2591) % 60.01/60.08 [260]P30(x2601)+P23(f17(x2601)) % 60.01/60.08 [261]P30(x2611)+P23(f20(x2611)) % 60.01/60.08 [263]~P6(x2631)+P25(f40(x2631)) % 60.01/60.08 [264]~P4(x2641)+P25(f41(x2641)) % 60.01/60.08 [267]P30(x2671)+~P30(f17(x2671)) % 60.01/60.08 [268]P30(x2681)+~P30(f20(x2681)) % 60.01/60.08 [297]P30(x2971)+P8(f17(x2971),f39(x2971)) % 60.01/60.08 [298]P30(x2981)+P8(f20(x2981),f39(x2981)) % 60.01/60.08 [377]~P6(x3771)+P26(f40(x3771),f44(f46(x3771),f46(x3771)),f46(x3771)) % 60.01/60.08 [378]~P4(x3781)+P26(f41(x3781),f44(f46(x3781),f46(x3781)),f46(x3781)) % 60.01/60.08 [379]~P6(x3791)+P10(f40(x3791),f44(f46(x3791),f46(x3791)),f46(x3791)) % 60.01/60.08 [380]~P4(x3801)+P10(f41(x3801),f44(f46(x3801),f46(x3801)),f46(x3801)) % 60.01/60.08 [363]~P3(x3631)+P8(f47(x3631),f39(f39(f46(x3631)))) % 60.01/60.08 [288]~P30(x2881)+~P12(x2882,x2881) % 60.01/60.08 [318]~P12(x3181,x3182)+P8(x3181,x3182) % 60.01/60.08 [349]~P12(x3492,x3491)+~P12(x3491,x3492) % 60.01/60.08 [330]~P7(x3301,x3302)+P8(x3301,f39(x3302)) % 60.01/60.08 [350]P7(x3501,x3502)+~P8(x3501,f39(x3502)) % 60.01/60.08 [366]~P8(x3662,f39(f39(x3661)))+P3(f37(x3661,x3662)) % 60.01/60.08 [367]~P8(x3672,f39(f39(x3671)))+P21(f37(x3671,x3672)) % 60.01/60.08 [387]~P10(x3871,x3872,x3873)+P9(x3871,x3872,x3873) % 60.01/60.08 [388]~P9(x3881,x3882,x3883)+P10(x3881,x3882,x3883) % 60.01/60.08 [376]P31(x3761)+~P8(x3761,f39(f44(x3762,x3763))) % 60.01/60.08 [389]~P10(x3891,x3892,x3893)+P8(x3891,f39(f44(x3892,x3893))) % 60.01/60.08 [265]~P24(x2651)+~P36(x2651)+P40(x2651) % 60.01/60.08 [266]P41(x2661)+~P3(x2661)+E(f34(x2661),f3(x2661)) % 60.01/60.08 [282]~P5(x2821)+P41(x2821)+~P30(f46(x2821)) % 60.01/60.08 [283]~P5(x2831)+P41(x2831)+~P30(f21(x2831)) % 60.01/60.08 [314]~P20(x3141)+~P3(x3141)+P47(f23(x3141),x3141) % 60.01/60.08 [329]~P3(x3291)+~P21(x3291)+E(f37(f46(x3291),f47(x3291)),x3291) % 60.01/60.08 [354]~P5(x3541)+P41(x3541)+P8(f21(x3541),f39(f46(x3541))) % 60.01/60.08 [357]~P20(x3571)+~P3(x3571)+P8(f23(x3571),f39(f46(x3571))) % 60.01/60.08 [371]~P2(x3711)+~P35(x3711)+E(f38(f46(x3711),f40(x3711),f41(x3711)),x3711) % 60.01/60.08 [364]~P3(x3641)+P41(x3641)+P8(f34(x3641),f39(f39(f46(x3641)))) % 60.01/60.08 [262]~P30(x2622)+~P30(x2621)+E(x2621,x2622) % 60.01/60.08 [299]~P8(x2991,x2992)+P33(x2991)+~P22(x2992) % 60.01/60.08 [300]~P8(x3001,x3002)+P33(x3001)+~P29(x3002) % 60.01/60.08 [301]~P8(x3011,x3012)+P33(x3011)+~P37(x3012) % 60.01/60.08 [302]~P8(x3021,x3022)+P33(x3021)+~P38(x3022) % 60.01/60.08 [303]~P8(x3031,x3032)+P33(x3031)+~P44(x3032) % 60.01/60.08 [304]~P8(x3041,x3042)+P34(x3041)+~P29(x3042) % 60.01/60.08 [305]~P8(x3051,x3052)+P34(x3051)+~P37(x3052) % 60.01/60.08 [306]~P8(x3061,x3062)+P34(x3061)+~P38(x3062) % 60.01/60.08 [307]~P8(x3071,x3072)+P34(x3071)+~P44(x3072) % 60.01/60.08 [308]~P8(x3081,x3082)+P32(x3081)+~P37(x3082) % 60.01/60.08 [309]~P8(x3091,x3092)+P32(x3091)+~P38(x3092) % 60.01/60.08 [310]~P8(x3101,x3102)+P32(x3101)+~P44(x3102) % 60.01/60.08 [311]~P8(x3111,x3112)+P27(x3111)+~P38(x3112) % 60.01/60.08 [312]~P8(x3121,x3122)+P27(x3121)+~P44(x3122) % 60.01/60.08 [313]~P8(x3131,x3132)+P46(x3131)+~P44(x3132) % 60.01/60.08 [328]~P8(x3282,x3281)+P30(x3281)+P12(x3282,x3281) % 60.01/60.08 [331]P22(x3311)+~P22(x3312)+~P8(x3311,f39(x3312)) % 60.01/60.08 [332]P22(x3321)+~P29(x3322)+~P8(x3321,f39(x3322)) % 60.01/60.08 [333]P22(x3331)+~P37(x3332)+~P8(x3331,f39(x3332)) % 60.01/60.08 [334]P22(x3341)+~P38(x3342)+~P8(x3341,f39(x3342)) % 60.01/60.08 [335]P22(x3351)+~P44(x3352)+~P8(x3351,f39(x3352)) % 60.01/60.08 [336]P29(x3361)+~P29(x3362)+~P8(x3361,f39(x3362)) % 60.01/60.08 [337]P29(x3371)+~P37(x3372)+~P8(x3371,f39(x3372)) % 60.01/60.08 [338]P29(x3381)+~P38(x3382)+~P8(x3381,f39(x3382)) % 60.01/60.08 [339]P29(x3391)+~P44(x3392)+~P8(x3391,f39(x3392)) % 60.01/60.08 [340]P37(x3401)+~P37(x3402)+~P8(x3401,f39(x3402)) % 60.01/60.08 [341]P37(x3411)+~P38(x3412)+~P8(x3411,f39(x3412)) % 60.01/60.08 [342]P37(x3421)+~P44(x3422)+~P8(x3421,f39(x3422)) % 60.01/60.08 [343]P38(x3431)+~P38(x3432)+~P8(x3431,f39(x3432)) % 60.01/60.08 [344]P38(x3441)+~P44(x3442)+~P8(x3441,f39(x3442)) % 60.01/60.08 [345]P44(x3451)+~P44(x3452)+~P8(x3451,f39(x3452)) % 60.01/60.08 [346]P23(x3461)+~P23(x3462)+~P8(x3461,f39(x3462)) % 60.01/60.08 [347]~P23(x3472)+~P23(x3471)+P23(f44(x3471,x3472)) % 60.01/60.08 [368]E(x3681,x3682)+P12(f27(x3681,x3682),x3682)+P12(f27(x3681,x3682),x3681) % 60.01/60.08 [381]E(x3811,x3812)+~P12(f27(x3811,x3812),x3812)+~P12(f27(x3811,x3812),x3811) % 60.01/60.08 [361]~P30(x3611)+~P12(x3612,x3613)+~P8(x3613,f39(x3611)) % 60.01/60.08 [362]P8(x3621,x3622)+~P12(x3621,x3623)+~P8(x3623,f39(x3622)) % 60.01/60.08 [373]E(x3731,x3732)+~E(f37(x3733,x3731),f37(x3734,x3732))+~P8(x3731,f39(f39(x3733))) % 60.01/60.08 [374]E(x3741,x3742)+~E(f37(x3741,x3743),f37(x3742,x3744))+~P8(x3743,f39(f39(x3741))) % 60.01/60.08 [269]P39(x2691)+~P1(x2691)+~P2(x2691)+P41(x2691) % 60.01/60.08 [270]P45(x2701)+~P1(x2701)+~P2(x2701)+P41(x2701) % 60.01/60.08 [271]P48(x2711)+~P1(x2711)+~P2(x2711)+P41(x2711) % 60.01/60.08 [272]P49(x2721)+~P1(x2721)+~P2(x2721)+P41(x2721) % 60.01/60.08 [273]P50(x2731)+~P1(x2731)+~P2(x2731)+P41(x2731) % 60.01/60.08 [274]P51(x2741)+~P1(x2741)+~P2(x2741)+P41(x2741) % 60.01/60.08 [275]P14(x2751)+~P13(x2751)+~P2(x2751)+P41(x2751) % 60.01/60.08 [276]P14(x2761)+~P2(x2761)+~P18(x2761)+P41(x2761) % 60.01/60.08 [277]P17(x2771)+~P13(x2771)+~P2(x2771)+P41(x2771) % 60.01/60.08 [278]P17(x2781)+~P2(x2781)+~P18(x2781)+P41(x2781) % 60.01/60.08 [279]P18(x2791)+~P13(x2791)+~P2(x2791)+P41(x2791) % 60.01/60.08 [280]P15(x2801)+~P13(x2801)+~P2(x2801)+P41(x2801) % 60.01/60.08 [281]P19(x2811)+~P13(x2811)+~P2(x2811)+P41(x2811) % 60.01/60.08 [284]~P20(x2841)+~P3(x2841)+P41(x2841)+P1(f42(x2841)) % 60.01/60.08 [285]~P20(x2851)+~P3(x2851)+P41(x2851)+P2(f42(x2851)) % 60.01/60.08 [286]~P20(x2861)+~P3(x2861)+P41(x2861)+P25(f43(x2861)) % 60.01/60.08 [287]~P20(x2871)+~P3(x2871)+P41(x2871)+P25(f45(x2871)) % 60.01/60.08 [315]~P20(x3151)+~P3(x3151)+P41(x3151)+~P41(f42(x3151)) % 60.01/60.08 [316]~P20(x3161)+~P3(x3161)+P41(x3161)+~P30(f34(x3161)) % 60.01/60.08 [317]~P20(x3171)+~P3(x3171)+P41(x3171)+~P30(f24(x3171)) % 60.01/60.08 [320]~P20(x3201)+~P3(x3201)+P41(x3201)+P47(f24(x3201),x3201) % 60.01/60.08 [353]~P20(x3531)+~P3(x3531)+P41(x3531)+~P11(a1,f42(x3531)) % 60.01/60.08 [358]~P20(x3581)+~P3(x3581)+P41(x3581)+P8(f24(x3581),f39(f46(x3581))) % 60.01/60.08 [372]P41(x3721)+~P20(x3721)+~P3(x3721)+E(f38(f34(x3721),f43(x3721),f45(x3721)),f42(x3721)) % 60.01/60.08 [383]~P20(x3831)+~P3(x3831)+P41(x3831)+P26(f43(x3831),f44(f34(x3831),f34(x3831)),f34(x3831)) % 60.01/60.08 [384]~P20(x3841)+~P3(x3841)+P41(x3841)+P26(f45(x3841),f44(f34(x3841),f34(x3841)),f34(x3841)) % 60.01/60.08 [385]~P20(x3851)+~P3(x3851)+P41(x3851)+P10(f43(x3851),f44(f34(x3851),f34(x3851)),f34(x3851)) % 60.01/60.08 [386]~P20(x3861)+~P3(x3861)+P41(x3861)+P10(f45(x3861),f44(f34(x3861),f34(x3861)),f34(x3861)) % 60.01/60.08 [359]P41(x3592)+~P3(x3592)+~P12(x3591,f3(x3592))+E(f4(x3591,x3592),x3591) % 60.01/60.08 [369]~P3(x3691)+P41(x3691)+~P12(x3692,f3(x3691))+P43(f4(x3692,x3691),x3691) % 60.01/60.08 [370]~P3(x3701)+P41(x3701)+~P12(x3702,f3(x3701))+P47(f4(x3702,x3701),x3701) % 60.01/60.08 [375]~P3(x3751)+P41(x3751)+~P12(x3752,f3(x3751))+P8(f4(x3752,x3751),f39(f46(x3751))) % 60.01/60.08 [391]~P25(x3911)+~P9(x3911,x3912,x3913)+~P28(x3911,x3912,x3913)+P26(x3911,x3912,x3913) % 60.01/60.08 [295]P18(x2951)+~P2(x2951)+~P14(x2951)+~P17(x2951)+P41(x2951) % 60.01/60.08 [296]P16(x2961)+~P1(x2961)+~P2(x2961)+~P15(x2961)+P41(x2961) % 60.01/60.08 [392]~P25(x3922)+~P9(x3922,x3923,x3921)+~P26(x3922,x3923,x3921)+P30(x3921)+P28(x3922,x3923,x3921) % 60.01/60.08 [319]P13(x3191)+~P2(x3191)+~P18(x3191)+~P15(x3191)+~P19(x3191)+P41(x3191) % 60.01/60.08 [321]P42(x3211)+~P1(x3211)+~P13(x3211)+~P2(x3211)+P41(x3211)+P1(f35(x3211)) % 60.01/60.08 [322]P42(x3221)+~P1(x3221)+~P13(x3221)+~P2(x3221)+P41(x3221)+P2(f35(x3221)) % 60.01/60.08 [324]P42(x3241)+~P1(x3241)+~P13(x3241)+~P2(x3241)+P41(x3241)+P20(f36(x3241)) % 60.01/60.08 [325]P42(x3251)+~P1(x3251)+~P13(x3251)+~P2(x3251)+P41(x3251)+P3(f36(x3251)) % 60.01/60.08 [327]P42(x3271)+~P1(x3271)+~P13(x3271)+~P2(x3271)+P41(x3271)+P21(f36(x3271)) % 60.01/60.08 [351]P42(x3511)+~P1(x3511)+~P13(x3511)+~P2(x3511)+P41(x3511)+~P41(f35(x3511)) % 60.01/60.08 [352]P42(x3521)+~P1(x3521)+~P13(x3521)+~P2(x3521)+P41(x3521)+~P41(f36(x3521)) % 60.01/60.08 [355]P42(x3551)+~P1(x3551)+~P13(x3551)+~P2(x3551)+P41(x3551)+P11(x3551,f35(x3551)) % 60.01/60.08 [348]P41(x3481)+P42(x3481)+~P1(x3481)+~P13(x3481)+~P2(x3481)+E(f35(x3481),f42(f36(x3481))) % 60.01/60.08 [390]~P25(x3903)+~P9(x3903,x3902,x3901)+~P26(x3903,x3902,x3901)+P30(x3901)+P30(x3902)+~P30(x3903) % 60.01/60.08 [356]P11(x3562,x3562)+~P1(x3561)+~P1(x3562)+~P2(x3561)+~P2(x3562)+P41(x3561)+P41(x3562) % 60.01/60.08 [394]~P25(x3943)+~P25(x3942)+~P9(x3943,f44(x3941,x3941),x3941)+~P9(x3942,f44(x3941,x3941),x3941)+~P26(x3943,f44(x3941,x3941),x3941)+~P26(x3942,f44(x3941,x3941),x3941)+P2(f38(x3941,x3942,x3943)) % 60.01/60.08 [395]~P25(x3953)+~P25(x3952)+~P9(x3953,f44(x3951,x3951),x3951)+~P9(x3952,f44(x3951,x3951),x3951)+~P26(x3953,f44(x3951,x3951),x3951)+~P26(x3952,f44(x3951,x3951),x3951)+P35(f38(x3951,x3952,x3953)) % 60.01/60.08 [382]~P3(x3821)+~P43(x3823,x3821)+~P47(x3823,x3821)+P41(x3821)+~E(x3823,x3822)+P12(x3822,f3(x3821))+~P8(x3823,f39(f46(x3821))) % 60.01/60.08 [365]P11(x3651,x3652)+~P1(x3651)+~P1(x3652)+~P2(x3651)+~P2(x3652)+~P11(x3652,x3651)+P41(x3651)+P41(x3652) % 60.01/60.08 [400]P30(x4001)+~P25(x4002)+~P25(x4003)+~P9(x4002,f44(x4001,x4001),x4001)+~P9(x4003,f44(x4001,x4001),x4001)+~P26(x4002,f44(x4001,x4001),x4001)+~P26(x4003,f44(x4001,x4001),x4001)+~P41(f38(x4001,x4003,x4002)) % 60.01/60.08 [397]~P25(x3974)+~P25(x3971)+E(x3971,x3972)+~P9(x3974,f44(x3973,x3973),x3973)+~P9(x3971,f44(x3973,x3973),x3973)+~P26(x3974,f44(x3973,x3973),x3973)+~P26(x3971,f44(x3973,x3973),x3973)+~E(f38(x3973,x3974,x3971),f38(x3975,x3976,x3972)) % 60.01/60.08 [398]~P25(x3984)+~P25(x3981)+E(x3981,x3982)+~P9(x3984,f44(x3983,x3983),x3983)+~P9(x3981,f44(x3983,x3983),x3983)+~P26(x3984,f44(x3983,x3983),x3983)+~P26(x3981,f44(x3983,x3983),x3983)+~E(f38(x3983,x3981,x3984),f38(x3985,x3982,x3986)) % 60.01/60.08 [399]~P25(x3994)+~P25(x3993)+E(x3991,x3992)+~P9(x3994,f44(x3991,x3991),x3991)+~P9(x3993,f44(x3991,x3991),x3991)+~P26(x3994,f44(x3991,x3991),x3991)+~P26(x3993,f44(x3991,x3991),x3991)+~E(f38(x3991,x3993,x3994),f38(x3992,x3995,x3996)) % 60.01/60.08 [360]P1(x3601)+~P2(x3601)+~P39(x3601)+~P45(x3601)+~P48(x3601)+~P49(x3601)+~P50(x3601)+~P51(x3601)+P41(x3601) % 60.01/60.08 %EqnAxiom % 60.01/60.08 [1]E(x11,x11) % 60.01/60.08 [2]E(x22,x21)+~E(x21,x22) % 60.01/60.08 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 60.01/60.08 [4]~E(x41,x42)+E(f39(x41),f39(x42)) % 60.01/60.08 [5]~E(x51,x52)+E(f44(x51,x53),f44(x52,x53)) % 60.01/60.08 [6]~E(x61,x62)+E(f44(x63,x61),f44(x63,x62)) % 60.01/60.08 [7]~E(x71,x72)+E(f45(x71),f45(x72)) % 60.01/60.08 [8]~E(x81,x82)+E(f31(x81),f31(x82)) % 60.01/60.08 [9]~E(x91,x92)+E(f10(x91,x93),f10(x92,x93)) % 60.01/60.08 [10]~E(x101,x102)+E(f10(x103,x101),f10(x103,x102)) % 60.01/60.08 [11]~E(x111,x112)+E(f16(x111,x113),f16(x112,x113)) % 60.01/60.08 [12]~E(x121,x122)+E(f16(x123,x121),f16(x123,x122)) % 60.01/60.08 [13]~E(x131,x132)+E(f34(x131),f34(x132)) % 60.01/60.08 [14]~E(x141,x142)+E(f41(x141),f41(x142)) % 60.01/60.08 [15]~E(x151,x152)+E(f32(x151,x153),f32(x152,x153)) % 60.01/60.08 [16]~E(x161,x162)+E(f32(x163,x161),f32(x163,x162)) % 60.01/60.08 [17]~E(x171,x172)+E(f46(x171),f46(x172)) % 60.01/60.08 [18]~E(x181,x182)+E(f3(x181),f3(x182)) % 60.01/60.08 [19]~E(x191,x192)+E(f38(x191,x193,x194),f38(x192,x193,x194)) % 60.01/60.08 [20]~E(x201,x202)+E(f38(x203,x201,x204),f38(x203,x202,x204)) % 60.01/60.08 [21]~E(x211,x212)+E(f38(x213,x214,x211),f38(x213,x214,x212)) % 60.01/60.08 [22]~E(x221,x222)+E(f33(x221,x223),f33(x222,x223)) % 60.01/60.08 [23]~E(x231,x232)+E(f33(x233,x231),f33(x233,x232)) % 60.01/60.08 [24]~E(x241,x242)+E(f4(x241,x243),f4(x242,x243)) % 60.01/60.08 [25]~E(x251,x252)+E(f4(x253,x251),f4(x253,x252)) % 60.01/60.08 [26]~E(x261,x262)+E(f17(x261),f17(x262)) % 60.01/60.08 [27]~E(x271,x272)+E(f20(x271),f20(x272)) % 60.01/60.08 [28]~E(x281,x282)+E(f40(x281),f40(x282)) % 60.01/60.08 [29]~E(x291,x292)+E(f43(x291),f43(x292)) % 60.01/60.08 [30]~E(x301,x302)+E(f35(x301),f35(x302)) % 60.01/60.08 [31]~E(x311,x312)+E(f42(x311),f42(x312)) % 60.01/60.08 [32]~E(x321,x322)+E(f37(x321,x323),f37(x322,x323)) % 60.01/60.08 [33]~E(x331,x332)+E(f37(x333,x331),f37(x333,x332)) % 60.01/60.08 [34]~E(x341,x342)+E(f47(x341),f47(x342)) % 60.01/60.08 [35]~E(x351,x352)+E(f36(x351),f36(x352)) % 60.01/60.08 [36]~E(x361,x362)+E(f21(x361),f21(x362)) % 60.01/60.08 [37]~E(x371,x372)+E(f27(x371,x373),f27(x372,x373)) % 60.01/60.08 [38]~E(x381,x382)+E(f27(x383,x381),f27(x383,x382)) % 60.01/60.08 [39]~E(x391,x392)+E(f23(x391),f23(x392)) % 60.01/60.08 [40]~E(x401,x402)+E(f24(x401),f24(x402)) % 60.01/60.08 [41]~P1(x411)+P1(x412)+~E(x411,x412) % 60.01/60.08 [42]P26(x422,x423,x424)+~E(x421,x422)+~P26(x421,x423,x424) % 60.01/60.08 [43]P26(x433,x432,x434)+~E(x431,x432)+~P26(x433,x431,x434) % 60.01/60.08 [44]P26(x443,x444,x442)+~E(x441,x442)+~P26(x443,x444,x441) % 60.01/60.08 [45]P9(x452,x453,x454)+~E(x451,x452)+~P9(x451,x453,x454) % 60.01/60.08 [46]P9(x463,x462,x464)+~E(x461,x462)+~P9(x463,x461,x464) % 60.01/60.08 [47]P9(x473,x474,x472)+~E(x471,x472)+~P9(x473,x474,x471) % 60.01/60.08 [48]P28(x482,x483,x484)+~E(x481,x482)+~P28(x481,x483,x484) % 60.01/60.08 [49]P28(x493,x492,x494)+~E(x491,x492)+~P28(x493,x491,x494) % 60.01/60.08 [50]P28(x503,x504,x502)+~E(x501,x502)+~P28(x503,x504,x501) % 60.01/60.08 [51]~P25(x511)+P25(x512)+~E(x511,x512) % 60.01/60.08 [52]~P41(x521)+P41(x522)+~E(x521,x522) % 60.01/60.08 [53]~P3(x531)+P3(x532)+~E(x531,x532) % 60.01/60.08 [54]~P13(x541)+P13(x542)+~E(x541,x542) % 60.01/60.08 [55]~P23(x551)+P23(x552)+~E(x551,x552) % 60.01/60.08 [56]~P38(x561)+P38(x562)+~E(x561,x562) % 60.01/60.08 [57]~P2(x571)+P2(x572)+~E(x571,x572) % 60.01/60.08 [58]~P22(x581)+P22(x582)+~E(x581,x582) % 60.01/60.08 [59]P8(x592,x593)+~E(x591,x592)+~P8(x591,x593) % 60.01/60.08 [60]P8(x603,x602)+~E(x601,x602)+~P8(x603,x601) % 60.01/60.08 [61]~P37(x611)+P37(x612)+~E(x611,x612) % 60.01/60.08 [62]P12(x622,x623)+~E(x621,x622)+~P12(x621,x623) % 60.01/60.08 [63]P12(x633,x632)+~E(x631,x632)+~P12(x633,x631) % 60.01/60.08 [64]~P19(x641)+P19(x642)+~E(x641,x642) % 60.01/60.08 [65]~P29(x651)+P29(x652)+~E(x651,x652) % 60.01/60.08 [66]~P44(x661)+P44(x662)+~E(x661,x662) % 60.01/60.08 [67]~P15(x671)+P15(x672)+~E(x671,x672) % 60.01/60.08 [68]P10(x682,x683,x684)+~E(x681,x682)+~P10(x681,x683,x684) % 60.01/60.08 [69]P10(x693,x692,x694)+~E(x691,x692)+~P10(x693,x691,x694) % 60.01/60.08 [70]P10(x703,x704,x702)+~E(x701,x702)+~P10(x703,x704,x701) % 60.01/60.08 [71]~P20(x711)+P20(x712)+~E(x711,x712) % 60.01/60.08 [72]P11(x722,x723)+~E(x721,x722)+~P11(x721,x723) % 60.01/60.08 [73]P11(x733,x732)+~E(x731,x732)+~P11(x733,x731) % 60.01/60.08 [74]~P42(x741)+P42(x742)+~E(x741,x742) % 60.01/60.08 [75]~P30(x751)+P30(x752)+~E(x751,x752) % 60.01/60.08 [76]~P21(x761)+P21(x762)+~E(x761,x762) % 60.01/60.08 [77]~P6(x771)+P6(x772)+~E(x771,x772) % 60.01/60.08 [78]~P35(x781)+P35(x782)+~E(x781,x782) % 60.01/60.08 [79]P7(x792,x793)+~E(x791,x792)+~P7(x791,x793) % 60.01/60.08 [80]P7(x803,x802)+~E(x801,x802)+~P7(x803,x801) % 60.01/60.08 [81]~P5(x811)+P5(x812)+~E(x811,x812) % 60.01/60.08 [82]~P4(x821)+P4(x822)+~E(x821,x822) % 60.01/60.08 [83]~P24(x831)+P24(x832)+~E(x831,x832) % 60.01/60.08 [84]~P33(x841)+P33(x842)+~E(x841,x842) % 60.01/60.08 [85]~P45(x851)+P45(x852)+~E(x851,x852) % 60.01/60.08 [86]~P32(x861)+P32(x862)+~E(x861,x862) % 60.01/60.08 [87]~P14(x871)+P14(x872)+~E(x871,x872) % 60.01/60.08 [88]~P51(x881)+P51(x882)+~E(x881,x882) % 60.01/60.08 [89]~P49(x891)+P49(x892)+~E(x891,x892) % 60.01/60.08 [90]~P34(x901)+P34(x902)+~E(x901,x902) % 60.01/60.08 [91]~P39(x911)+P39(x912)+~E(x911,x912) % 60.01/60.08 [92]~P18(x921)+P18(x922)+~E(x921,x922) % 60.01/60.08 [93]~P17(x931)+P17(x932)+~E(x931,x932) % 60.01/60.08 [94]~P31(x941)+P31(x942)+~E(x941,x942) % 60.01/60.08 [95]~P46(x951)+P46(x952)+~E(x951,x952) % 60.01/60.08 [96]~P16(x961)+P16(x962)+~E(x961,x962) % 60.01/60.08 [97]P43(x972,x973)+~E(x971,x972)+~P43(x971,x973) % 60.01/60.08 [98]P43(x983,x982)+~E(x981,x982)+~P43(x983,x981) % 60.01/60.08 [99]~P50(x991)+P50(x992)+~E(x991,x992) % 60.01/60.08 [100]~P27(x1001)+P27(x1002)+~E(x1001,x1002) % 60.01/60.08 [101]~P48(x1011)+P48(x1012)+~E(x1011,x1012) % 60.01/60.08 [102]P47(x1022,x1023)+~E(x1021,x1022)+~P47(x1021,x1023) % 60.01/60.08 [103]P47(x1033,x1032)+~E(x1031,x1032)+~P47(x1033,x1031) % 60.01/60.08 [104]~P40(x1041)+P40(x1042)+~E(x1041,x1042) % 60.01/60.08 [105]~P36(x1051)+P36(x1052)+~E(x1051,x1052) % 60.01/60.08 % 60.01/60.08 %------------------------------------------- % 60.01/60.08 cnf(407,plain, % 60.01/60.08 (~P12(x4071,a30)), % 60.01/60.08 inference(scs_inference,[],[149,288])). % 60.01/60.08 cnf(409,plain, % 60.01/60.08 (P7(f31(f39(x4091)),x4091)), % 60.01/60.08 inference(scs_inference,[],[217,149,288,350])). % 60.01/60.08 cnf(410,plain, % 60.01/60.08 (P8(f31(x4101),x4101)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(413,plain, % 60.01/60.08 (P8(f31(x4131),x4131)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(415,plain, % 60.01/60.08 (P12(f31(a9),a9)), % 60.01/60.08 inference(scs_inference,[],[217,410,413,149,239,288,350,376,328])). % 60.01/60.08 cnf(416,plain, % 60.01/60.08 (P8(f31(x4161),x4161)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(419,plain, % 60.01/60.08 (P8(f31(x4191),x4191)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(422,plain, % 60.01/60.08 (P8(f31(x4221),x4221)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(425,plain, % 60.01/60.08 (P8(f31(x4251),x4251)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(428,plain, % 60.01/60.08 (P8(f31(x4281),x4281)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(431,plain, % 60.01/60.08 (P8(f31(x4311),x4311)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(433,plain, % 60.01/60.08 (P23(f31(f39(a9)))), % 60.01/60.08 inference(scs_inference,[],[217,410,413,416,419,422,425,428,431,139,141,143,145,147,149,150,239,288,350,376,328,331,336,340,343,345,346])). % 60.01/60.08 cnf(434,plain, % 60.01/60.08 (P8(f31(x4341),x4341)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(436,plain, % 60.01/60.08 (~P12(x4361,f31(f39(a30)))), % 60.01/60.08 inference(scs_inference,[],[217,410,413,416,419,422,425,428,431,434,139,141,143,145,147,149,150,239,288,350,376,328,331,336,340,343,345,346,361])). % 60.01/60.08 cnf(437,plain, % 60.01/60.08 (P8(f31(x4371),x4371)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(439,plain, % 60.01/60.08 (E(a30,f31(f39(a30)))), % 60.01/60.08 inference(scs_inference,[],[217,410,413,416,419,422,425,428,431,434,139,141,143,145,147,149,150,239,288,350,376,328,331,336,340,343,345,346,361,368])). % 60.01/60.08 cnf(467,plain, % 60.01/60.08 (P28(f10(x4671,a9),x4671,a9)), % 60.01/60.08 inference(scs_inference,[],[106,113,116,227,228,118,223,225,217,410,413,416,419,422,425,428,431,434,139,141,143,145,147,149,150,187,192,239,218,288,350,376,328,331,336,340,343,345,346,361,368,269,270,271,272,273,274,275,277,279,280,281,295,296,392])). % 60.01/60.08 cnf(468,plain, % 60.01/60.08 (P26(f10(x4681,x4682),x4681,x4682)), % 60.01/60.08 inference(rename_variables,[],[225])). % 60.01/60.08 cnf(469,plain, % 60.01/60.08 (P25(f10(x4691,x4692))), % 60.01/60.08 inference(rename_variables,[],[218])). % 60.01/60.08 cnf(470,plain, % 60.01/60.08 (P9(f10(x4701,x4702),x4701,x4702)), % 60.01/60.08 inference(rename_variables,[],[223])). % 60.01/60.08 cnf(472,plain, % 60.01/60.08 (~P30(f10(a9,a9))), % 60.01/60.08 inference(scs_inference,[],[106,113,116,227,228,118,223,470,225,468,217,410,413,416,419,422,425,428,431,434,139,141,143,145,147,149,150,187,192,239,218,469,288,350,376,328,331,336,340,343,345,346,361,368,269,270,271,272,273,274,275,277,279,280,281,295,296,392,390])). % 60.01/60.08 cnf(473,plain, % 60.01/60.08 (P26(f10(x4731,x4732),x4731,x4732)), % 60.01/60.08 inference(rename_variables,[],[225])). % 60.01/60.08 cnf(477,plain, % 60.01/60.08 (P11(a1,a1)), % 60.01/60.08 inference(scs_inference,[],[106,113,116,227,228,118,223,470,225,468,217,410,413,416,419,422,425,428,431,434,139,141,143,145,147,149,150,187,192,239,218,469,288,350,376,328,331,336,340,343,345,346,361,368,269,270,271,272,273,274,275,277,279,280,281,295,296,392,390,356])). % 60.01/60.08 cnf(479,plain, % 60.01/60.08 (E(f31(f39(a30)),a30)), % 60.01/60.08 inference(scs_inference,[],[106,113,116,227,228,118,223,470,225,468,217,410,413,416,419,422,425,428,431,434,139,141,143,145,147,149,150,187,192,239,218,469,288,350,376,328,331,336,340,343,345,346,361,368,269,270,271,272,273,274,275,277,279,280,281,295,296,392,390,356,2])). % 60.01/60.08 cnf(483,plain, % 60.01/60.08 (P26(f10(a30,x4831),f31(f39(a30)),x4831)), % 60.01/60.08 inference(scs_inference,[],[106,113,116,227,228,118,223,470,225,468,473,217,410,413,416,419,422,425,428,431,434,139,141,143,145,147,149,150,187,192,239,218,469,288,350,376,328,331,336,340,343,345,346,361,368,269,270,271,272,273,274,275,277,279,280,281,295,296,392,390,356,2,349,41,43])). % 60.01/60.08 cnf(484,plain, % 60.01/60.08 (P26(f10(x4841,x4842),x4841,x4842)), % 60.01/60.08 inference(rename_variables,[],[225])). % 60.01/60.08 cnf(485,plain, % 60.01/60.08 (P26(f10(x4851,a30),x4851,f31(f39(a30)))), % 60.01/60.08 inference(scs_inference,[],[106,113,116,227,228,118,223,470,225,468,473,484,217,410,413,416,419,422,425,428,431,434,139,141,143,145,147,149,150,187,192,239,218,469,288,350,376,328,331,336,340,343,345,346,361,368,269,270,271,272,273,274,275,277,279,280,281,295,296,392,390,356,2,349,41,43,44])). % 60.01/60.08 cnf(487,plain, % 60.01/60.08 (P9(f32(a30,x4871),f31(f39(a30)),x4871)), % 60.01/60.08 inference(scs_inference,[],[106,113,116,227,228,118,222,223,470,225,468,473,484,217,410,413,416,419,422,425,428,431,434,139,141,143,145,147,149,150,187,192,239,218,469,288,350,376,328,331,336,340,343,345,346,361,368,269,270,271,272,273,274,275,277,279,280,281,295,296,392,390,356,2,349,41,43,44,46])). % 60.01/60.08 cnf(488,plain, % 60.01/60.08 (P9(f32(x4881,x4882),x4881,x4882)), % 60.01/60.08 inference(rename_variables,[],[222])). % 60.01/60.08 cnf(489,plain, % 60.01/60.08 (P9(f32(x4891,a30),x4891,f31(f39(a30)))), % 60.01/60.08 inference(scs_inference,[],[106,113,116,227,228,118,222,488,223,470,225,468,473,484,217,410,413,416,419,422,425,428,431,434,139,141,143,145,147,149,150,187,192,239,218,469,288,350,376,328,331,336,340,343,345,346,361,368,269,270,271,272,273,274,275,277,279,280,281,295,296,392,390,356,2,349,41,43,44,46,47])). % 60.01/60.08 cnf(491,plain, % 60.01/60.08 (P28(f10(a30,a9),f31(f39(a30)),a9)), % 60.01/60.08 inference(scs_inference,[],[106,113,116,227,228,118,222,488,223,470,225,468,473,484,217,410,413,416,419,422,425,428,431,434,139,141,143,145,147,149,150,187,192,239,218,469,288,350,376,328,331,336,340,343,345,346,361,368,269,270,271,272,273,274,275,277,279,280,281,295,296,392,390,356,2,349,41,43,44,46,47,49])). % 60.01/60.08 cnf(492,plain, % 60.01/60.08 (P8(a30,f39(a30))), % 60.01/60.08 inference(scs_inference,[],[106,113,116,227,228,118,222,488,223,470,225,468,473,484,217,410,413,416,419,422,425,428,431,434,437,139,141,143,145,147,149,150,187,192,239,218,469,288,350,376,328,331,336,340,343,345,346,361,368,269,270,271,272,273,274,275,277,279,280,281,295,296,392,390,356,2,349,41,43,44,46,47,49,59])). % 60.01/60.08 cnf(493,plain, % 60.01/60.08 (P8(f31(x4931),x4931)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(496,plain, % 60.01/60.08 (P10(f33(a30,x4961),f31(f39(a30)),x4961)), % 60.01/60.08 inference(scs_inference,[],[106,113,116,227,228,118,222,488,223,470,225,468,473,484,226,217,410,413,416,419,422,425,428,431,434,437,493,139,141,143,145,147,149,150,187,192,239,218,469,288,350,376,328,331,336,340,343,345,346,361,368,269,270,271,272,273,274,275,277,279,280,281,295,296,392,390,356,2,349,41,43,44,46,47,49,59,60,69])). % 60.01/60.08 cnf(497,plain, % 60.01/60.08 (P10(f33(x4971,x4972),x4971,x4972)), % 60.01/60.08 inference(rename_variables,[],[226])). % 60.01/60.08 cnf(498,plain, % 60.01/60.08 (P10(f33(x4981,a30),x4981,f31(f39(a30)))), % 60.01/60.08 inference(scs_inference,[],[106,113,116,227,228,118,222,488,223,470,225,468,473,484,226,497,217,410,413,416,419,422,425,428,431,434,437,493,139,141,143,145,147,149,150,187,192,239,218,469,288,350,376,328,331,336,340,343,345,346,361,368,269,270,271,272,273,274,275,277,279,280,281,295,296,392,390,356,2,349,41,43,44,46,47,49,59,60,69,70])). % 60.01/60.08 cnf(500,plain, % 60.01/60.08 (P30(f31(f39(a30)))), % 60.01/60.08 inference(scs_inference,[],[106,113,116,227,228,118,222,488,223,470,225,468,473,484,226,497,217,410,413,416,419,422,425,428,431,434,437,493,139,141,143,145,147,149,150,187,192,239,218,469,288,350,376,328,331,336,340,343,345,346,361,368,269,270,271,272,273,274,275,277,279,280,281,295,296,392,390,356,2,349,41,43,44,46,47,49,59,60,69,70,75])). % 60.01/60.08 cnf(510,plain, % 60.01/60.08 (P12(f31(f10(a9,a9)),f10(a9,a9))), % 60.01/60.08 inference(scs_inference,[],[436,472,415,217,63,328])). % 60.01/60.08 cnf(511,plain, % 60.01/60.08 (P8(f31(x5111),x5111)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(515,plain, % 60.01/60.08 (P10(f33(a30,f31(f39(a30))),f31(f39(a30)),a30)), % 60.01/60.08 inference(scs_inference,[],[496,479,436,467,472,415,217,63,328,49,70])). % 60.01/60.08 cnf(517,plain, % 60.01/60.08 (P9(f32(a30,f31(f39(a30))),f31(f39(a30)),a30)), % 60.01/60.08 inference(scs_inference,[],[487,496,479,436,467,472,415,217,63,328,49,70,47])). % 60.01/60.08 cnf(519,plain, % 60.01/60.08 (P8(f31(f31(f39(a30))),a30)), % 60.01/60.08 inference(scs_inference,[],[487,496,479,436,467,472,415,217,511,63,328,49,70,47,60])). % 60.01/60.08 cnf(521,plain, % 60.01/60.08 (P26(f10(a30,f31(f39(a30))),f31(f39(a30)),a30)), % 60.01/60.08 inference(scs_inference,[],[483,487,496,479,436,467,472,415,217,511,63,328,49,70,47,60,44])). % 60.01/60.08 cnf(523,plain, % 60.01/60.08 (P26(f10(f31(f39(a30)),a30),a30,f31(f39(a30)))), % 60.01/60.08 inference(scs_inference,[],[483,485,487,496,479,436,467,472,415,217,511,63,328,49,70,47,60,44,43])). % 60.01/60.08 cnf(525,plain, % 60.01/60.08 (P10(f33(f31(f39(a30)),a30),a30,f31(f39(a30)))), % 60.01/60.08 inference(scs_inference,[],[483,485,487,496,498,479,436,467,472,415,217,511,63,328,49,70,47,60,44,43,69])). % 60.01/60.08 cnf(527,plain, % 60.01/60.08 (P9(f32(f31(f39(a30)),a30),a30,f31(f39(a30)))), % 60.01/60.08 inference(scs_inference,[],[483,485,487,489,496,498,479,436,467,472,415,217,511,63,328,49,70,47,60,44,43,69,46])). % 60.01/60.08 cnf(529,plain, % 60.01/60.08 (P28(f10(x5291,f10(a9,a9)),x5291,f10(a9,a9))), % 60.01/60.08 inference(scs_inference,[],[483,485,487,489,496,498,479,436,467,472,415,223,225,217,511,218,63,328,49,70,47,60,44,43,69,46,392])). % 60.01/60.08 cnf(530,plain, % 60.01/60.08 (P26(f10(x5301,x5302),x5301,x5302)), % 60.01/60.08 inference(rename_variables,[],[225])). % 60.01/60.08 cnf(531,plain, % 60.01/60.08 (P25(f10(x5311,x5312))), % 60.01/60.08 inference(rename_variables,[],[218])). % 60.01/60.08 cnf(532,plain, % 60.01/60.08 (P9(f10(x5321,x5322),x5321,x5322)), % 60.01/60.08 inference(rename_variables,[],[223])). % 60.01/60.08 cnf(536,plain, % 60.01/60.08 (~P30(f10(f10(a9,a9),f10(a9,a9)))), % 60.01/60.08 inference(scs_inference,[],[231,121,483,485,487,489,496,498,479,110,202,436,467,472,415,223,532,225,530,217,511,218,531,63,328,49,70,47,60,44,43,69,46,392,296,390])). % 60.01/60.08 cnf(541,plain, % 60.01/60.08 (P11(a2,a2)), % 60.01/60.08 inference(scs_inference,[],[106,116,227,231,228,121,118,483,485,487,489,496,498,479,107,110,202,436,467,472,415,223,532,225,530,217,511,218,531,63,328,49,70,47,60,44,43,69,46,392,296,390,356])). % 60.01/60.08 cnf(547,plain, % 60.01/60.08 (P11(a1,x5471)+~E(a1,x5471)), % 60.01/60.08 inference(scs_inference,[],[106,116,227,477,231,228,121,118,483,485,487,489,496,498,479,107,110,202,436,467,472,439,415,223,532,225,530,217,511,218,531,63,328,49,70,47,60,44,43,69,46,392,296,390,356,349,72,3,73])). % 60.01/60.08 cnf(556,plain, % 60.01/60.08 (P12(f31(f10(f10(a9,a9),f10(a9,a9))),f10(f10(a9,a9),f10(a9,a9)))), % 60.01/60.08 inference(scs_inference,[],[536,217,328])). % 60.01/60.08 cnf(559,plain, % 60.01/60.08 (P28(f10(f31(f39(a30)),f10(a9,a9)),a30,f10(a9,a9))), % 60.01/60.08 inference(scs_inference,[],[479,529,536,217,328,49])). % 60.01/60.08 cnf(570,plain, % 60.01/60.08 (P26(f10(x5701,x5702),x5701,x5702)), % 60.01/60.08 inference(rename_variables,[],[225])). % 60.01/60.08 cnf(571,plain, % 60.01/60.08 (P25(f10(x5711,x5712))), % 60.01/60.08 inference(rename_variables,[],[218])). % 60.01/60.08 cnf(572,plain, % 60.01/60.08 (P9(f10(x5721,x5722),x5721,x5722)), % 60.01/60.08 inference(rename_variables,[],[223])). % 60.01/60.08 cnf(574,plain, % 60.01/60.08 (~P30(f10(f10(f10(a9,a9),f10(a9,a9)),f10(f10(a9,a9),f10(a9,a9))))), % 60.01/60.08 inference(scs_inference,[],[479,515,517,521,523,525,527,407,529,536,510,223,572,225,570,217,218,571,328,49,63,44,46,69,43,47,70,392,390])). % 60.01/60.08 cnf(579,plain, % 60.01/60.08 (P11(a5,a5)), % 60.01/60.08 inference(scs_inference,[],[106,116,227,229,119,479,108,515,517,521,523,525,527,407,529,536,510,223,572,225,570,217,218,571,328,49,63,44,46,69,43,47,70,392,390,356])). % 60.01/60.08 cnf(586,plain, % 60.01/60.08 (~P23(f31(f39(a30)))+P23(a30)), % 60.01/60.08 inference(scs_inference,[],[106,116,227,229,119,479,108,515,517,521,523,525,527,491,407,529,536,510,223,572,225,570,217,218,571,328,49,63,44,46,69,43,47,70,392,390,356,349,48,50,51,55])). % 60.01/60.08 cnf(594,plain, % 60.01/60.08 (P12(f31(a12),a12)), % 60.01/60.08 inference(scs_inference,[],[436,556,240,217,63,328])). % 60.01/60.08 cnf(597,plain, % 60.01/60.08 (P10(f33(f31(f39(a30)),x5971),a30,x5971)), % 60.01/60.08 inference(scs_inference,[],[479,436,556,240,226,217,63,328,69])). % 60.01/60.08 cnf(598,plain, % 60.01/60.08 (P10(f33(x5981,x5982),x5981,x5982)), % 60.01/60.08 inference(rename_variables,[],[226])). % 60.01/60.08 cnf(599,plain, % 60.01/60.08 (P26(f10(f31(f39(a30)),x5991),a30,x5991)), % 60.01/60.08 inference(scs_inference,[],[479,436,556,240,226,225,217,63,328,69,43])). % 60.01/60.08 cnf(600,plain, % 60.01/60.08 (P26(f10(x6001,x6002),x6001,x6002)), % 60.01/60.08 inference(rename_variables,[],[225])). % 60.01/60.08 cnf(601,plain, % 60.01/60.08 (P10(f33(x6011,f31(f39(a30))),x6011,a30)), % 60.01/60.08 inference(scs_inference,[],[479,436,556,240,226,598,225,217,63,328,69,43,70])). % 60.01/60.08 cnf(603,plain, % 60.01/60.08 (P9(f16(x6031,f31(f39(a30))),x6031,a30)), % 60.01/60.08 inference(scs_inference,[],[479,436,556,224,240,226,598,225,217,63,328,69,43,70,47])). % 60.01/60.08 cnf(604,plain, % 60.01/60.08 (P9(f16(x6041,x6042),x6041,x6042)), % 60.01/60.08 inference(rename_variables,[],[224])). % 60.01/60.08 cnf(605,plain, % 60.01/60.08 (P26(f10(x6051,f31(f39(a30))),x6051,a30)), % 60.01/60.08 inference(scs_inference,[],[479,436,556,224,240,226,598,225,600,217,63,328,69,43,70,47,44])). % 60.01/60.08 cnf(607,plain, % 60.01/60.08 (P9(f16(f31(f39(a30)),x6071),a30,x6071)), % 60.01/60.08 inference(scs_inference,[],[479,436,556,224,604,240,226,598,225,600,217,63,328,69,43,70,47,44,46])). % 60.01/60.08 cnf(609,plain, % 60.01/60.08 (P11(a8,a8)), % 60.01/60.08 inference(scs_inference,[],[106,116,227,232,479,122,111,436,556,224,604,240,226,598,225,600,217,63,328,69,43,70,47,44,46,356])). % 60.01/60.08 cnf(620,plain, % 60.01/60.08 (P12(a30,f39(a30))), % 60.01/60.08 inference(scs_inference,[],[492,241,328])). % 60.01/60.08 cnf(623,plain, % 60.01/60.08 (P10(f33(f31(f39(a30)),f31(f39(a30))),a30,a30)), % 60.01/60.08 inference(scs_inference,[],[492,479,601,241,328,69])). % 60.01/60.08 cnf(627,plain, % 60.01/60.08 (P9(f16(f31(f39(a30)),f31(f39(a30))),a30,a30)), % 60.01/60.08 inference(scs_inference,[],[492,479,601,607,407,594,241,328,69,63,47])). % 60.01/60.08 cnf(631,plain, % 60.01/60.08 (P9(f32(f31(f39(a30)),x6311),a30,x6311)), % 60.01/60.08 inference(scs_inference,[],[492,479,599,601,607,407,594,241,222,328,69,63,47,44,46])). % 60.01/60.08 cnf(633,plain, % 60.01/60.08 (P11(a7,a7)), % 60.01/60.08 inference(scs_inference,[],[106,116,227,231,492,479,110,121,599,601,607,407,594,241,222,328,69,63,47,44,46,356])). % 60.01/60.08 cnf(636,plain, % 60.01/60.08 (P12(f31(f39(a30)),f39(a30))), % 60.01/60.08 inference(scs_inference,[],[106,116,227,231,492,479,110,121,599,601,607,439,407,594,241,222,328,69,63,47,44,46,356,82,62])). % 60.01/60.08 cnf(642,plain, % 60.01/60.08 (P9(f10(f31(f39(a30)),x6421),a30,x6421)), % 60.01/60.08 inference(scs_inference,[],[479,636,436,223,63,46])). % 60.01/60.08 cnf(644,plain, % 60.01/60.08 (P9(f32(f31(f39(a30)),f31(f39(a30))),a30,a30)), % 60.01/60.08 inference(scs_inference,[],[479,631,636,436,223,63,46,47])). % 60.01/60.08 cnf(654,plain, % 60.01/60.08 (~E(f39(a30),a30)), % 60.01/60.08 inference(scs_inference,[],[636,407,63])). % 60.01/60.08 cnf(657,plain, % 60.01/60.08 (P9(f10(f31(f39(a30)),x6571),a30,x6571)), % 60.01/60.08 inference(rename_variables,[],[642])). % 60.01/60.08 cnf(658,plain, % 60.01/60.08 (P28(f10(f31(f39(a30)),a12),a30,a12)), % 60.01/60.08 inference(scs_inference,[],[479,599,636,642,657,407,240,218,63,47,392])). % 60.01/60.08 cnf(660,plain, % 60.01/60.08 (P25(f10(x6601,x6602))), % 60.01/60.08 inference(rename_variables,[],[218])). % 60.01/60.08 cnf(663,plain, % 60.01/60.08 (~P30(f10(a12,a12))), % 60.01/60.08 inference(scs_inference,[],[479,599,636,642,657,407,225,240,218,660,223,63,47,392,390])). % 60.01/60.08 cnf(683,plain, % 60.01/60.08 (P8(f31(x6831),x6831)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(686,plain, % 60.01/60.08 (P8(f31(x6861),x6861)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(688,plain, % 60.01/60.08 (P37(f31(f39(a12)))), % 60.01/60.08 inference(scs_inference,[],[217,683,686,148,335,339,342])). % 60.01/60.08 cnf(689,plain, % 60.01/60.08 (P8(f31(x6891),x6891)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(691,plain, % 60.01/60.08 (P38(f31(f39(a12)))), % 60.01/60.08 inference(scs_inference,[],[217,683,686,689,148,335,339,342,344])). % 60.01/60.08 cnf(692,plain, % 60.01/60.08 (P8(f31(x6921),x6921)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(694,plain, % 60.01/60.08 (P44(f31(f39(a12)))), % 60.01/60.08 inference(scs_inference,[],[217,683,686,689,692,148,335,339,342,344,345])). % 60.01/60.08 cnf(695,plain, % 60.01/60.08 (P8(f31(x6951),x6951)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(697,plain, % 60.01/60.08 (P28(f10(f31(f39(a30)),a12),f31(f39(a30)),a12)), % 60.01/60.08 inference(scs_inference,[],[439,217,683,686,689,692,658,148,335,339,342,344,345,49])). % 60.01/60.08 cnf(698,plain, % 60.01/60.08 (P12(f31(f10(a12,a12)),f10(a12,a12))), % 60.01/60.08 inference(scs_inference,[],[439,217,683,686,689,692,695,663,658,148,335,339,342,344,345,49,328])). % 60.01/60.08 cnf(701,plain, % 60.01/60.08 (P9(f32(x7011,f31(f39(a30))),x7011,a30)), % 60.01/60.08 inference(scs_inference,[],[479,439,217,683,686,689,692,695,222,663,658,148,335,339,342,344,345,49,328,47])). % 60.01/60.08 cnf(705,plain, % 60.01/60.08 (P28(f10(f31(f39(a30)),f39(x7051)),a30,f39(x7051))), % 60.01/60.08 inference(scs_inference,[],[479,599,642,439,217,683,686,689,692,695,594,436,241,222,663,658,148,218,335,339,342,344,345,49,328,47,63,392])). % 60.01/60.08 cnf(707,plain, % 60.01/60.08 (P25(f10(x7071,x7072))), % 60.01/60.08 inference(rename_variables,[],[218])). % 60.01/60.08 cnf(710,plain, % 60.01/60.08 (~P30(f10(f39(x7101),f39(x7101)))), % 60.01/60.08 inference(scs_inference,[],[479,599,642,439,217,683,686,689,692,695,594,436,225,241,222,663,658,148,218,707,223,335,339,342,344,345,49,328,47,63,392,390])). % 60.01/60.08 cnf(728,plain, % 60.01/60.08 (P28(f10(f31(f39(a30)),f39(x7281)),f31(f39(a30)),f39(x7281))), % 60.01/60.08 inference(scs_inference,[],[439,217,710,705,328,49])). % 60.01/60.08 cnf(729,plain, % 60.01/60.08 (P9(f10(x7291,f31(f39(a30))),x7291,a30)), % 60.01/60.08 inference(scs_inference,[],[479,439,217,710,705,223,328,49,47])). % 60.01/60.08 cnf(737,plain, % 60.01/60.08 (P23(f31(f39(a30)))+~P23(a30)), % 60.01/60.08 inference(scs_inference,[],[492,479,439,217,407,556,710,705,223,328,49,47,63,349,346,55])). % 60.01/60.08 cnf(775,plain, % 60.01/60.08 (P9(x7751,x7752,a30)+~E(f16(x7752,f31(f39(a30))),x7751)), % 60.01/60.08 inference(scs_inference,[],[603,45])). % 60.01/60.08 cnf(831,plain, % 60.01/60.08 (P8(x8311,x8312)+~P12(x8311,f31(f39(x8312)))), % 60.01/60.08 inference(scs_inference,[],[217,362])). % 60.01/60.08 cnf(884,plain, % 60.01/60.08 (P26(x8841,a30,x8842)+~E(f10(f31(f39(a30)),x8842),x8841)), % 60.01/60.08 inference(scs_inference,[],[479,559,599,439,594,96,62,50,90,82,42])). % 60.01/60.08 cnf(904,plain, % 60.01/60.08 (P9(x9041,a30,x9042)+~E(f32(f31(f39(a30)),x9042),x9041)), % 60.01/60.08 inference(scs_inference,[],[541,631,73,45])). % 60.01/60.08 cnf(906,plain, % 60.01/60.08 (P10(x9061,a30,x9062)+~E(f33(f31(f39(a30)),x9062),x9061)), % 60.01/60.08 inference(scs_inference,[],[541,597,631,439,73,45,85,68])). % 60.01/60.08 cnf(921,plain, % 60.01/60.08 (P10(x9211,x9212,a30)+~E(f33(x9212,f31(f39(a30))),x9211)), % 60.01/60.08 inference(scs_inference,[],[579,601,697,728,519,521,42,72,48,59,50,68])). % 60.01/60.08 cnf(933,plain, % 60.01/60.08 (P28(x9331,x9332,a9)+~E(f10(x9332,a9),x9331)), % 60.01/60.08 inference(scs_inference,[],[609,467,73,48])). % 60.01/60.08 cnf(934,plain, % 60.01/60.08 (P9(x9341,a30,x9342)+~E(f16(f31(f39(a30)),x9342),x9341)), % 60.01/60.08 inference(scs_inference,[],[609,607,467,73,48,45])). % 60.01/60.08 cnf(943,plain, % 60.01/60.08 (P9(x9431,x9432,a30)+~E(f32(x9432,f31(f39(a30))),x9431)), % 60.01/60.08 inference(scs_inference,[],[701,45])). % 60.01/60.08 cnf(950,plain, % 60.01/60.08 (P28(f10(f31(f39(a30)),f39(x9501)),f31(f39(a30)),x9502)+~E(f39(x9501),x9502)), % 60.01/60.08 inference(scs_inference,[],[633,728,72,50])). % 60.01/60.08 cnf(954,plain, % 60.01/60.08 (P28(x9541,x9542,f10(a9,a9))+~E(f10(x9542,f10(a9,a9)),x9541)), % 60.01/60.08 inference(scs_inference,[],[633,728,515,529,698,72,50,68,62,73,48])). % 60.01/60.08 cnf(962,plain, % 60.01/60.08 (P9(x9621,a30,x9622)+~E(f10(f31(f39(a30)),x9622),x9621)), % 60.01/60.08 inference(scs_inference,[],[642,525,68,45])). % 60.01/60.08 cnf(996,plain, % 60.01/60.08 (P28(f10(f31(f39(a30)),f39(x9961)),a30,x9962)+~E(f39(x9961),x9962)), % 60.01/60.08 inference(scs_inference,[],[705,50])). % 60.01/60.08 cnf(1236,plain, % 60.01/60.08 (P23(a30)), % 60.01/60.08 inference(scs_inference,[],[500,252,586])). % 60.01/60.08 cnf(1237,plain, % 60.01/60.08 (P23(f31(f39(a30)))), % 60.01/60.08 inference(scs_inference,[],[1236,737])). % 60.01/60.08 cnf(1757,plain, % 60.01/60.08 (~P30(f20(f39(a30)))), % 60.01/60.08 inference(scs_inference,[],[636,268,288])). % 60.01/60.08 cnf(4518,plain, % 60.01/60.08 (P6(a8)), % 60.01/60.08 inference(scs_inference,[],[127,209,212,122,256,257,258,259])). % 60.01/60.08 cnf(4524,plain, % 60.01/60.08 (P25(f40(a29))), % 60.01/60.08 inference(scs_inference,[],[127,209,212,1757,122,256,257,258,259,260,261,263])). % 60.01/60.08 cnf(4526,plain, % 60.01/60.08 (P25(f41(a22))), % 60.01/60.08 inference(scs_inference,[],[127,209,212,1757,122,256,257,258,259,260,261,263,264])). % 60.01/60.08 cnf(4532,plain, % 60.01/60.08 (P8(x45321,f39(x45321))), % 60.01/60.08 inference(scs_inference,[],[127,209,212,1757,216,122,256,257,258,259,260,261,263,264,267,268,330])). % 60.01/60.08 cnf(4542,plain, % 60.01/60.08 (E(f39(a30),f39(f31(f39(a30))))), % 60.01/60.08 inference(scs_inference,[],[127,209,212,627,623,1757,216,122,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4])). % 60.01/60.08 cnf(4560,plain, % 60.01/60.08 (P8(f31(x45601),x45601)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(4563,plain, % 60.01/60.08 (P8(f31(x45631),x45631)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(4579,plain, % 60.01/60.08 (E(f37(a30,x45791),f37(f31(f39(a30)),x45791))), % 60.01/60.08 inference(scs_inference,[],[127,209,212,627,623,1757,216,122,217,4560,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32])). % 60.01/60.08 cnf(4581,plain, % 60.01/60.08 (E(f27(a30,x45811),f27(f31(f39(a30)),x45811))), % 60.01/60.08 inference(scs_inference,[],[127,209,212,627,623,1757,216,122,217,4560,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37])). % 60.01/60.08 cnf(4583,plain, % 60.01/60.08 (P8(f47(a26),f39(f39(f46(a26))))), % 60.01/60.08 inference(scs_inference,[],[127,209,212,627,623,1757,216,122,217,4560,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363])). % 60.01/60.08 cnf(4585,plain, % 60.01/60.08 (E(f38(a30,x45851,x45852),f38(f31(f39(a30)),x45851,x45852))), % 60.01/60.08 inference(scs_inference,[],[127,209,212,627,623,1757,216,122,217,4560,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19])). % 60.01/60.08 cnf(4586,plain, % 60.01/60.08 (E(f38(x45861,a30,x45862),f38(x45861,f31(f39(a30)),x45862))), % 60.01/60.08 inference(scs_inference,[],[127,209,212,627,623,1757,216,122,217,4560,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20])). % 60.01/60.08 cnf(4588,plain, % 60.01/60.08 (P26(f40(a29),f44(f46(a29),f46(a29)),f46(a29))), % 60.01/60.08 inference(scs_inference,[],[127,209,212,627,623,1757,216,122,217,4560,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377])). % 60.01/60.08 cnf(4590,plain, % 60.01/60.08 (P26(f41(a22),f44(f46(a22),f46(a22)),f46(a22))), % 60.01/60.08 inference(scs_inference,[],[127,209,212,627,623,1757,216,122,217,4560,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378])). % 60.01/60.08 cnf(4592,plain, % 60.01/60.08 (P10(f40(a29),f44(f46(a29),f46(a29)),f46(a29))), % 60.01/60.08 inference(scs_inference,[],[127,209,212,627,623,1757,216,122,217,4560,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379])). % 60.01/60.08 cnf(4594,plain, % 60.01/60.08 (P10(f41(a22),f44(f46(a22),f46(a22)),f46(a22))), % 60.01/60.08 inference(scs_inference,[],[127,209,212,627,623,1757,216,122,217,4560,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380])). % 60.01/60.08 cnf(4598,plain, % 60.01/60.08 (P4(a8)), % 60.01/60.08 inference(scs_inference,[],[127,209,212,627,623,1757,216,122,217,4560,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255])). % 60.01/60.08 cnf(4605,plain, % 60.01/60.08 (P8(f31(x46051),x46051)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(4608,plain, % 60.01/60.08 (P8(f31(x46081),x46081)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(4613,plain, % 60.01/60.08 (P8(f31(x46131),x46131)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(4616,plain, % 60.01/60.08 (P8(f31(x46161),x46161)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(4621,plain, % 60.01/60.08 (P8(f31(x46211),x46211)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(4624,plain, % 60.01/60.08 (P8(f31(x46241),x46241)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(4629,plain, % 60.01/60.08 (P8(f31(x46291),x46291)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(4631,plain, % 60.01/60.08 (~P30(f46(a19))), % 60.01/60.08 inference(scs_inference,[],[127,142,144,146,209,211,212,234,654,688,691,627,623,694,1757,216,122,519,139,141,143,145,217,4560,4563,4605,4608,4613,4616,4621,4624,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282])). % 60.01/60.08 cnf(4633,plain, % 60.01/60.08 (~P30(f21(a19))), % 60.01/60.08 inference(scs_inference,[],[127,142,144,146,209,211,212,234,654,688,691,627,623,694,1757,216,122,519,139,141,143,145,217,4560,4563,4605,4608,4613,4616,4621,4624,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283])). % 60.01/60.08 cnf(4637,plain, % 60.01/60.08 (P23(f44(a30,a30))), % 60.01/60.08 inference(scs_inference,[],[126,127,129,142,144,146,209,211,212,234,1236,654,688,691,627,623,694,1757,216,122,519,139,141,143,145,217,4560,4563,4605,4608,4613,4616,4621,4624,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347])). % 60.01/60.08 cnf(4639,plain, % 60.01/60.08 (E(f34(a15),f3(a15))), % 60.01/60.08 inference(scs_inference,[],[126,127,129,142,144,146,209,211,212,233,234,1236,654,688,691,627,623,694,1757,216,122,519,139,141,143,145,217,4560,4563,4605,4608,4613,4616,4621,4624,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266])). % 60.01/60.08 cnf(4641,plain, % 60.01/60.08 (P8(f21(a19),f39(f46(a19)))), % 60.01/60.08 inference(scs_inference,[],[126,127,129,142,144,146,209,211,212,233,234,1236,654,688,691,627,623,694,1757,216,122,519,139,141,143,145,217,4560,4563,4605,4608,4613,4616,4621,4624,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354])). % 60.01/60.08 cnf(4643,plain, % 60.01/60.08 (P8(f23(a15),f39(f46(a15)))), % 60.01/60.08 inference(scs_inference,[],[126,127,129,142,144,146,209,211,212,233,234,1236,654,688,691,627,623,694,1757,216,122,519,139,141,143,145,217,4560,4563,4605,4608,4613,4616,4621,4624,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357])). % 60.01/60.08 cnf(4647,plain, % 60.01/60.08 (P8(f34(a15),f39(f39(f46(a15))))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,142,144,146,209,211,212,233,234,1236,654,688,691,627,623,694,1757,216,122,519,139,141,143,145,217,4560,4563,4605,4608,4613,4616,4621,4624,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364])). % 60.01/60.08 cnf(4653,plain, % 60.01/60.08 (~P8(f39(a30),f39(a30))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,217,4560,4563,4605,4608,4613,4616,4621,4624,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361])). % 60.01/60.08 cnf(4656,plain, % 60.01/60.08 (P12(f27(a30,f39(a30)),f39(a30))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368])). % 60.01/60.08 cnf(4661,plain, % 60.01/60.08 (P8(f31(x46611),x46611)), % 60.01/60.08 inference(rename_variables,[],[217])). % 60.01/60.08 cnf(4663,plain, % 60.01/60.08 (~E(f31(f39(a30)),f39(a30))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59])). % 60.01/60.08 cnf(4666,plain, % 60.01/60.08 (~E(f39(f39(a30)),f39(a30))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60])). % 60.01/60.08 cnf(4667,plain, % 60.01/60.08 (P1(f42(a15))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284])). % 60.01/60.08 cnf(4669,plain, % 60.01/60.08 (P2(f42(a15))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285])). % 60.01/60.08 cnf(4671,plain, % 60.01/60.08 (P25(f43(a15))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286])). % 60.01/60.08 cnf(4673,plain, % 60.01/60.08 (P25(f45(a15))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287])). % 60.01/60.08 cnf(4675,plain, % 60.01/60.08 (~P41(f42(a15))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315])). % 60.01/60.08 cnf(4677,plain, % 60.01/60.08 (~P30(f34(a15))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316])). % 60.01/60.08 cnf(4679,plain, % 60.01/60.08 (~P30(f24(a15))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317])). % 60.01/60.08 cnf(4683,plain, % 60.01/60.08 (~P11(a1,f42(a15))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353])). % 60.01/60.08 cnf(4685,plain, % 60.01/60.08 (P8(f24(a15),f39(f46(a15)))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358])). % 60.01/60.08 cnf(4687,plain, % 60.01/60.08 (E(f38(f34(a15),f43(a15),f45(a15)),f42(a15))), % 60.01/60.08 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372])). % 60.01/60.08 cnf(4689,plain, % 60.01/60.08 (P26(f43(a15),f44(f34(a15),f34(a15)),f34(a15))), % 60.01/60.09 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383])). % 60.01/60.09 cnf(4691,plain, % 60.01/60.09 (P26(f45(a15),f44(f34(a15),f34(a15)),f34(a15))), % 60.01/60.09 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384])). % 60.01/60.09 cnf(4693,plain, % 60.01/60.09 (P10(f43(a15),f44(f34(a15),f34(a15)),f34(a15))), % 60.01/60.09 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384,385])). % 60.01/60.09 cnf(4695,plain, % 60.01/60.09 (P10(f45(a15),f44(f34(a15),f34(a15)),f34(a15))), % 60.01/60.09 inference(scs_inference,[],[126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,147,149,407,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384,385,386])). % 60.01/60.09 cnf(4709,plain, % 60.01/60.09 (P1(f35(a1))), % 60.01/60.09 inference(scs_inference,[],[106,237,126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,113,147,149,407,227,116,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384,385,386,274,269,271,270,273,272,321])). % 60.01/60.09 cnf(4711,plain, % 60.01/60.09 (P2(f35(a1))), % 60.01/60.09 inference(scs_inference,[],[106,237,126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,113,147,149,407,227,116,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384,385,386,274,269,271,270,273,272,321,322])). % 60.01/60.09 cnf(4713,plain, % 60.01/60.09 (P20(f36(a1))), % 60.01/60.09 inference(scs_inference,[],[106,237,126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,113,147,149,407,227,116,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384,385,386,274,269,271,270,273,272,321,322,324])). % 60.01/60.09 cnf(4715,plain, % 60.01/60.09 (P3(f36(a1))), % 60.01/60.09 inference(scs_inference,[],[106,237,126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,113,147,149,407,227,116,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384,385,386,274,269,271,270,273,272,321,322,324,325])). % 60.01/60.09 cnf(4717,plain, % 60.01/60.09 (P21(f36(a1))), % 60.01/60.09 inference(scs_inference,[],[106,237,126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,113,147,149,407,227,116,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384,385,386,274,269,271,270,273,272,321,322,324,325,327])). % 60.01/60.09 cnf(4719,plain, % 60.01/60.09 (~P41(f35(a1))), % 60.01/60.09 inference(scs_inference,[],[106,237,126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,113,147,149,407,227,116,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384,385,386,274,269,271,270,273,272,321,322,324,325,327,351])). % 60.01/60.09 cnf(4721,plain, % 60.01/60.09 (~P41(f36(a1))), % 60.01/60.09 inference(scs_inference,[],[106,237,126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,113,147,149,407,227,116,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384,385,386,274,269,271,270,273,272,321,322,324,325,327,351,352])). % 60.01/60.09 cnf(4723,plain, % 60.01/60.09 (P11(a1,f35(a1))), % 60.01/60.09 inference(scs_inference,[],[106,237,126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,113,147,149,407,227,116,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384,385,386,274,269,271,270,273,272,321,322,324,325,327,351,352,355])). % 60.01/60.09 cnf(4725,plain, % 60.01/60.09 (E(f35(a1),f42(f36(a1)))), % 60.01/60.09 inference(scs_inference,[],[106,237,126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,113,147,149,407,227,116,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384,385,386,274,269,271,270,273,272,321,322,324,325,327,351,352,355,348])). % 60.01/60.09 cnf(4729,plain, % 60.01/60.09 (P8(f27(a30,f39(a30)),f39(a30))), % 60.01/60.09 inference(scs_inference,[],[106,237,126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,113,147,149,407,227,116,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384,385,386,274,269,271,270,273,272,321,322,324,325,327,351,352,355,348,356,318])). % 60.01/60.09 cnf(4731,plain, % 60.01/60.09 (~E(a1,f42(a15))), % 60.01/60.09 inference(scs_inference,[],[106,237,126,127,128,129,130,132,142,144,146,209,211,212,233,234,1236,654,688,691,574,620,627,623,694,1757,216,122,519,139,141,143,145,118,113,147,149,407,227,116,217,4560,4563,4605,4608,4613,4616,4621,4624,4629,4661,439,256,257,258,259,260,261,263,264,267,268,330,387,388,297,298,4,7,13,14,17,18,26,27,28,29,30,31,34,35,36,39,40,366,367,389,5,6,9,10,11,12,15,16,22,23,24,25,32,33,37,38,363,19,20,21,377,378,379,380,996,950,255,8,2,299,300,301,304,305,306,308,309,310,311,312,282,283,314,347,266,354,357,329,364,371,313,361,75,368,3,362,59,55,60,284,285,286,287,315,316,317,320,353,358,372,383,384,385,386,274,269,271,270,273,272,321,322,324,325,327,351,352,355,348,356,318,547])). % 60.01/60.09 cnf(4797,plain, % 60.01/60.09 (P5(f36(a1))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4631,4715,644,257,267,388,263,256])). % 60.01/60.09 cnf(4799,plain, % 60.01/60.09 (P9(f45(a15),f44(f34(a15),f34(a15)),f34(a15))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4631,4715,4695,644,257,267,388,263,256,387])). % 60.01/60.09 cnf(4805,plain, % 60.01/60.09 (P23(f20(f46(a19)))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4631,4715,4695,644,257,267,388,263,256,387,297,268,261])). % 60.01/60.09 cnf(4807,plain, % 60.01/60.09 (P3(f37(x48071,f39(x48071)))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4532,4631,4715,4695,644,257,267,388,263,256,387,297,268,261,366])). % 60.01/60.09 cnf(4808,plain, % 60.01/60.09 (P8(x48081,f39(x48081))), % 60.01/60.09 inference(rename_variables,[],[4532])). % 60.01/60.09 cnf(4812,plain, % 60.01/60.09 (P8(f47(a11),f39(f39(f46(a11))))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4532,4631,4715,4695,644,128,257,267,388,263,256,387,297,268,261,366,389,363])). % 60.01/60.09 cnf(4814,plain, % 60.01/60.09 (P6(f42(a15))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4532,4631,4669,4715,4695,644,128,257,267,388,263,256,387,297,268,261,366,389,363,259])). % 60.01/60.09 cnf(4828,plain, % 60.01/60.09 (P5(f42(a15))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4532,4631,4639,4669,4715,4695,644,128,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258])). % 60.01/60.09 cnf(4832,plain, % 60.01/60.09 (P23(f17(f46(a19)))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4532,4631,4639,4669,4715,4695,644,128,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260])). % 60.01/60.09 cnf(4835,plain, % 60.01/60.09 (E(f38(f34(a15),x48351,x48352),f38(f3(a15),x48351,x48352))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4532,4631,4639,4669,4715,4695,644,128,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19])). % 60.01/60.09 cnf(4837,plain, % 60.01/60.09 (P8(x48371,f39(x48371))), % 60.01/60.09 inference(rename_variables,[],[4532])). % 60.01/60.09 cnf(4839,plain, % 60.01/60.09 (E(f38(x48391,f34(a15),x48392),f38(x48391,f3(a15),x48392))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4532,4808,4631,4639,4669,4715,4695,644,128,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20])). % 60.01/60.09 cnf(4842,plain, % 60.01/60.09 (P10(f40(a8),f44(f46(a8),f46(a8)),f46(a8))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4532,4808,4631,4639,4669,4715,4695,644,128,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379])). % 60.01/60.09 cnf(4844,plain, % 60.01/60.09 (P10(f41(a8),f44(f46(a8),f46(a8)),f46(a8))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4532,4808,4631,4639,4669,4715,4695,644,128,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380])). % 60.01/60.09 cnf(4856,plain, % 60.01/60.09 (E(f10(f34(a15),x48561),f10(f3(a15),x48561))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4532,4808,4631,4639,4669,4715,4695,644,128,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9])). % 60.01/60.09 cnf(4860,plain, % 60.01/60.09 (P4(f42(a15))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4532,4808,4631,4639,4669,4715,4695,644,128,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255])). % 60.01/60.09 cnf(4877,plain, % 60.01/60.09 (~P30(f46(a8))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4532,4808,4631,4639,4669,4715,4721,4731,4695,644,128,232,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282])). % 60.01/60.09 cnf(4881,plain, % 60.01/60.09 (~P30(f21(a8))), % 60.01/60.09 inference(scs_inference,[],[4518,4598,4532,4808,4631,4639,4669,4715,4717,4721,4731,4695,644,128,232,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283])). % 60.01/60.09 cnf(4888,plain, % 60.01/60.09 (P8(f31(x48881),x48881)), % 60.01/60.09 inference(rename_variables,[],[217])). % 60.01/60.09 cnf(4894,plain, % 60.01/60.09 (P23(f44(f44(a30,a30),f44(a30,a30)))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4637,4631,4639,4669,4713,4715,4717,4721,4731,4695,644,128,232,119,146,217,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347])). % 60.01/60.09 cnf(4897,plain, % 60.01/60.09 (P8(f31(x48971),x48971)), % 60.01/60.09 inference(rename_variables,[],[217])). % 60.01/60.09 cnf(4899,plain, % 60.01/60.09 (~P8(f39(a30),f39(f31(f39(a30))))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4637,4631,4639,4669,4713,4715,4717,4721,4731,4695,4656,644,128,232,119,146,148,500,217,4888,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361])). % 60.01/60.09 cnf(4901,plain, % 60.01/60.09 (~P11(a1,f38(f34(a15),f43(a15),f45(a15)))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4637,4631,4639,4669,4713,4715,4717,4721,4683,4731,4695,4687,4656,644,128,232,119,146,148,500,217,4888,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73])). % 60.01/60.09 cnf(4902,plain, % 60.01/60.09 (P12(f27(f31(f39(a30)),f39(a30)),f39(a30))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4637,4631,4639,4669,4713,4715,4717,4721,4683,4731,4695,4663,4687,4656,644,128,232,119,146,148,500,436,217,4888,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368])). % 60.01/60.09 cnf(4905,plain, % 60.01/60.09 (~E(f31(f39(a30)),f46(a19))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4637,4631,4639,4669,4713,4715,4717,4721,4683,4731,4695,4663,4687,4656,644,128,232,119,146,148,500,436,217,4888,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75])). % 60.01/60.09 cnf(4907,plain, % 60.01/60.09 (E(f37(a30,x49071),f37(f31(f39(a30)),x49071))), % 60.01/60.09 inference(rename_variables,[],[4579])). % 60.01/60.09 cnf(4914,plain, % 60.01/60.09 (P2(f42(f36(a1)))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4637,4631,4639,4669,4709,4711,4713,4715,4717,4721,4683,4731,4695,4663,4687,4656,4725,4585,4586,4579,4907,644,128,232,119,146,148,500,436,217,4888,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57])). % 60.01/60.09 cnf(4915,plain, % 60.01/60.09 (P8(f27(f31(f39(a30)),f39(a30)),f39(a30))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4837,4637,4631,4639,4669,4709,4711,4713,4715,4717,4721,4683,4731,4695,4663,4687,4656,4725,4585,4586,4579,4907,644,128,232,119,146,148,500,436,217,4888,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362])). % 60.01/60.09 cnf(4916,plain, % 60.01/60.09 (P8(x49161,f39(x49161))), % 60.01/60.09 inference(rename_variables,[],[4532])). % 60.01/60.09 cnf(4919,plain, % 60.01/60.09 (P8(x49191,f39(x49191))), % 60.01/60.09 inference(rename_variables,[],[4532])). % 60.01/60.09 cnf(4934,plain, % 60.01/60.09 (P51(f35(a1))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4656,4725,4585,4586,4579,4907,644,128,232,119,146,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274])). % 60.01/60.09 cnf(4936,plain, % 60.01/60.09 (~P11(a1,f42(f36(a1)))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4656,4725,4585,4586,4579,4907,644,128,232,119,146,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353])). % 60.01/60.09 cnf(4940,plain, % 60.01/60.09 (P48(f35(a1))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4656,4725,4585,4586,4579,4907,644,128,232,119,146,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271])). % 60.01/60.09 cnf(4942,plain, % 60.01/60.09 (P45(f35(a1))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4656,4725,4585,4586,4579,4907,644,128,232,119,146,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270])). % 60.01/60.09 cnf(4944,plain, % 60.01/60.09 (P50(f35(a1))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4656,4725,4585,4586,4579,4907,644,128,232,119,146,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273])). % 60.01/60.09 cnf(4946,plain, % 60.01/60.09 (P49(f35(a1))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4656,4725,4585,4586,4579,4907,644,128,232,119,146,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272])). % 60.01/60.09 cnf(4948,plain, % 60.01/60.09 (P39(f35(a1))), % 60.01/60.09 inference(scs_inference,[],[133,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4656,4725,4585,4586,4579,4907,644,128,232,119,146,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269])). % 60.01/60.09 cnf(4952,plain, % 60.01/60.09 (P3(f36(a8))), % 60.01/60.09 inference(scs_inference,[],[133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4673,4677,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325])). % 60.01/60.09 cnf(4954,plain, % 60.01/60.09 (P21(f36(a8))), % 60.01/60.09 inference(scs_inference,[],[133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4673,4677,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327])). % 60.01/60.09 cnf(4956,plain, % 60.01/60.09 (~P41(f35(a8))), % 60.01/60.09 inference(scs_inference,[],[133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4673,4677,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351])). % 60.01/60.09 cnf(4958,plain, % 60.01/60.09 (P1(f35(a8))), % 60.01/60.09 inference(scs_inference,[],[133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4673,4677,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321])). % 60.01/60.09 cnf(4960,plain, % 60.01/60.09 (P20(f36(a8))), % 60.01/60.09 inference(scs_inference,[],[133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4673,4677,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324])). % 60.01/60.09 cnf(4962,plain, % 60.01/60.09 (~P41(f36(a8))), % 60.01/60.09 inference(scs_inference,[],[133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4673,4677,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352])). % 60.01/60.09 cnf(4964,plain, % 60.01/60.09 (P11(a8,f35(a8))), % 60.01/60.09 inference(scs_inference,[],[133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4673,4677,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355])). % 60.01/60.09 cnf(4966,plain, % 60.01/60.09 (E(f35(a8),f42(f36(a8)))), % 60.01/60.09 inference(scs_inference,[],[133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4673,4677,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348])). % 60.01/60.09 cnf(4968,plain, % 60.01/60.09 (P2(f35(a8))), % 60.01/60.09 inference(scs_inference,[],[133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4673,4677,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322])). % 60.01/60.09 cnf(4970,plain, % 60.01/60.09 (P2(f38(f34(a15),f45(a15),f45(a15)))), % 60.01/60.09 inference(scs_inference,[],[133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4673,4677,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394])). % 60.01/60.09 cnf(4972,plain, % 60.01/60.09 (P35(f38(f34(a15),f45(a15),f45(a15)))), % 60.01/60.09 inference(scs_inference,[],[133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4669,4673,4677,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394,395])). % 60.01/60.09 cnf(4976,plain, % 60.01/60.09 (~P41(f38(f34(a15),f45(a15),f45(a15)))), % 60.01/60.09 inference(scs_inference,[],[133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4667,4669,4673,4675,4677,4709,4711,4713,4715,4717,4719,4721,4683,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394,395,356,400])). % 60.01/60.09 cnf(4978,plain, % 60.01/60.09 (P11(f35(a1),a1)), % 60.01/60.09 inference(scs_inference,[],[106,133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4667,4669,4673,4675,4677,4709,4711,4713,4715,4717,4719,4721,4683,4723,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,227,116,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394,395,356,400,365])). % 60.01/60.09 cnf(4981,plain, % 60.01/60.09 (P9(f16(f3(a15),f31(f39(a30))),f34(a15),a30)), % 60.01/60.09 inference(scs_inference,[],[106,133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4667,4669,4673,4675,4677,4709,4711,4713,4715,4717,4719,4721,4683,4723,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,227,116,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394,395,356,400,365,933,775])). % 60.01/60.09 cnf(4982,plain, % 60.01/60.09 (P26(f10(f31(f39(a30)),f3(a15)),a30,f34(a15))), % 60.01/60.09 inference(scs_inference,[],[106,133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4667,4669,4673,4675,4677,4709,4711,4713,4715,4717,4719,4721,4683,4723,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,227,116,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394,395,356,400,365,933,775,884])). % 60.01/60.09 cnf(4983,plain, % 60.01/60.09 (P9(f32(f31(f39(a30)),f3(a15)),a30,f34(a15))), % 60.01/60.09 inference(scs_inference,[],[106,133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4667,4669,4673,4675,4677,4709,4711,4713,4715,4717,4719,4721,4683,4723,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,227,116,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394,395,356,400,365,933,775,884,904])). % 60.01/60.09 cnf(4986,plain, % 60.01/60.09 (P9(f16(f31(f39(a30)),f3(a15)),a30,f34(a15))), % 60.01/60.09 inference(scs_inference,[],[106,133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4667,4669,4673,4675,4677,4709,4711,4713,4715,4717,4719,4721,4683,4723,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,227,116,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394,395,356,400,365,933,775,884,904,906,921,934])). % 60.01/60.09 cnf(4987,plain, % 60.01/60.09 (P9(f32(f3(a15),f31(f39(a30))),f34(a15),a30)), % 60.01/60.09 inference(scs_inference,[],[106,133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4667,4669,4673,4675,4677,4709,4711,4713,4715,4717,4719,4721,4683,4723,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,227,116,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394,395,356,400,365,933,775,884,904,906,921,934,943])). % 60.01/60.09 cnf(4988,plain, % 60.01/60.09 (P9(f10(f31(f39(a30)),f3(a15)),a30,f34(a15))), % 60.01/60.09 inference(scs_inference,[],[106,133,238,4518,4598,4532,4808,4837,4916,4637,4631,4639,4667,4669,4673,4675,4677,4709,4711,4713,4715,4717,4719,4721,4683,4723,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,122,148,500,436,217,4888,4897,227,116,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394,395,356,400,365,933,775,884,904,906,921,934,943,962])). % 60.01/60.09 cnf(4998,plain, % 60.01/60.09 (P9(f10(f3(a15),a9),f34(a15),a9)), % 60.01/60.09 inference(scs_inference,[],[106,133,238,4518,4598,4532,4808,4837,4916,4919,4637,4631,4639,4667,4669,4673,4675,4677,4709,4711,4713,4715,4717,4719,4721,4683,4723,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,226,122,148,500,223,436,217,4888,4897,227,116,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394,395,356,400,365,933,775,884,904,906,921,934,943,962,547,349,306,72,50,68,45])). % 60.01/60.09 cnf(5000,plain, % 60.01/60.09 (P26(f10(f3(a15),a9),f34(a15),a9)), % 60.01/60.09 inference(scs_inference,[],[106,133,238,4518,4598,4532,4808,4837,4916,4919,4637,4631,4639,4667,4669,4673,4675,4677,4709,4711,4713,4715,4717,4719,4721,4683,4723,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,226,122,148,500,225,223,436,217,4888,4897,227,116,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394,395,356,400,365,933,775,884,904,906,921,934,943,962,547,349,306,72,50,68,45,42])). % 60.01/60.09 cnf(5002,plain, % 60.01/60.09 (P2(f42(f36(a8)))), % 60.01/60.09 inference(scs_inference,[],[106,133,238,4518,4598,4532,4808,4837,4916,4919,4637,4631,4639,4667,4669,4673,4675,4677,4709,4711,4713,4715,4717,4719,4721,4683,4723,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,226,122,148,500,225,223,436,217,4888,4897,227,116,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394,395,356,400,365,933,775,884,904,906,921,934,943,962,547,349,306,72,50,68,45,42,285])). % 60.01/60.09 cnf(5004,plain, % 60.01/60.09 (P1(f42(f36(a8)))), % 60.01/60.09 inference(scs_inference,[],[106,133,238,4518,4598,4532,4808,4837,4916,4919,4637,4631,4639,4667,4669,4673,4675,4677,4709,4711,4713,4715,4717,4719,4721,4683,4723,4731,4695,4663,4687,4691,4656,4725,4585,4586,4579,4907,115,644,128,232,111,119,146,226,122,148,500,225,223,436,217,4888,4897,227,116,257,267,388,263,256,387,297,268,261,366,389,363,259,14,11,32,34,28,39,264,18,5,16,25,258,37,6,260,26,19,367,20,298,379,380,15,33,4,377,21,36,378,31,9,7,13,10,255,27,23,29,17,30,22,38,12,24,35,40,2,8,266,282,329,283,357,371,311,314,354,347,313,361,73,368,75,76,3,53,41,57,362,59,60,315,286,317,287,316,320,274,353,358,271,270,273,272,269,392,325,327,351,321,324,352,355,348,322,394,395,356,400,365,933,775,884,904,906,921,934,943,962,547,349,306,72,50,68,45,42,285,284])). % 60.01/60.09 cnf(5016,plain, % 60.01/60.09 (P6(f35(a8))), % 60.01/60.09 inference(scs_inference,[],[4633,4968,4856,954,267,297,261,259])). % 60.01/60.09 cnf(5020,plain, % 60.01/60.09 (P9(f43(a15),f44(f34(a15),f34(a15)),f34(a15))), % 60.01/60.09 inference(scs_inference,[],[4633,4814,4968,4693,4856,954,267,297,261,259,263,387])). % 60.01/60.09 cnf(5022,plain, % 60.01/60.09 (P8(f47(a15),f39(f39(f46(a15))))), % 60.01/60.09 inference(scs_inference,[],[4633,4814,4968,4693,4856,129,954,267,297,261,259,263,387,363])). % 60.01/60.09 cnf(5030,plain, % 60.01/60.09 (P5(f36(a8))), % 60.01/60.09 inference(scs_inference,[],[4633,4814,4952,4968,4693,4998,4856,4647,129,954,267,297,261,259,263,387,363,388,260,367,256])). % 60.01/60.09 cnf(5032,plain, % 60.01/60.09 (P3(f37(f46(a15),f34(a15)))), % 60.01/60.09 inference(scs_inference,[],[4633,4814,4952,4968,4693,4998,4856,4647,129,954,267,297,261,259,263,387,363,388,260,367,256,366])). % 60.01/60.09 cnf(5037,plain, % 60.01/60.09 (P4(f35(a8))), % 60.01/60.09 inference(scs_inference,[],[4633,4814,4952,4968,4693,4998,4966,4856,4647,129,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255])). % 60.01/60.09 cnf(5052,plain, % 60.01/60.09 (E(f38(x50521,x50522,f35(a8)),f38(x50521,x50522,f42(f36(a8))))), % 60.01/60.09 inference(scs_inference,[],[4633,4814,4860,4952,4968,4693,4998,4966,4856,4647,129,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21])). % 60.01/60.09 cnf(5057,plain, % 60.01/60.09 (E(f40(f35(a8)),f40(f42(f36(a8))))), % 60.01/60.09 inference(scs_inference,[],[4633,4814,4860,4952,4968,4693,4998,4966,4856,4647,129,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28])). % 60.01/60.09 cnf(5076,plain, % 60.01/60.09 (E(f10(f35(a8),x50761),f10(f42(f36(a8)),x50761))), % 60.01/60.09 inference(scs_inference,[],[4633,4814,4860,4952,4968,4693,4998,4966,4936,4856,4647,129,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9])). % 60.01/60.09 cnf(5089,plain, % 60.01/60.09 (P29(f27(f31(f39(a30)),f39(a30)))), % 60.01/60.09 inference(scs_inference,[],[4633,4814,4860,4952,4968,4729,4693,4666,4998,4966,4936,4856,4647,4581,143,145,129,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65])). % 60.01/60.09 cnf(5093,plain, % 60.01/60.09 (P8(f31(x50931),x50931)), % 60.01/60.09 inference(rename_variables,[],[217])). % 60.01/60.09 cnf(5100,plain, % 60.01/60.09 (E(f37(f46(a15),f47(a15)),a15)), % 60.01/60.09 inference(scs_inference,[],[131,4633,4814,4860,4942,4952,4956,4968,4729,4693,4666,4998,4966,4936,4856,4647,4581,4725,143,145,129,217,5093,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329])). % 60.01/60.09 cnf(5110,plain, % 60.01/60.09 (E(f38(f46(a6),f40(a6),f41(a6)),a6)), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4942,4952,4956,4960,4962,4968,4729,4693,4666,4998,4966,4936,4856,4647,4581,4725,120,143,145,129,217,5093,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371])). % 60.01/60.09 cnf(5114,plain, % 60.01/60.09 (P37(f27(a30,f39(a30)))), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4942,4952,4956,4960,4962,4968,4729,4693,4666,4998,4966,4936,4856,4647,4581,4725,120,143,145,129,217,5093,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371,314,340])). % 60.01/60.09 cnf(5118,plain, % 60.01/60.09 (P38(f27(a30,f39(a30)))), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4942,4952,4956,4960,4962,4968,4729,4693,4666,4998,4894,4966,4936,4856,4647,4581,4725,120,143,145,129,217,5093,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371,314,340,347,343])). % 60.01/60.09 cnf(5120,plain, % 60.01/60.09 (P5(f42(f36(a8)))), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4942,4952,4956,4960,4962,4968,4729,4693,4666,4998,4894,4966,4936,4856,4647,4581,4725,120,143,145,129,217,5093,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371,314,340,347,343,81])). % 60.01/60.09 cnf(5121,plain, % 60.01/60.09 (P12(f27(f31(f39(a30)),f46(a19)),f46(a19))), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4942,4952,4956,4960,4962,4968,4729,4693,4666,4905,4998,4894,4966,4936,4856,4647,4581,4725,120,143,145,436,129,217,5093,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371,314,340,347,343,81,368])). % 60.01/60.09 cnf(5125,plain, % 60.01/60.09 (~E(a30,f21(a19))), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4942,4944,4952,4956,4960,4962,4968,4729,4693,4666,4905,4998,4894,4966,4936,4856,4647,4581,4725,120,143,145,149,436,129,217,5093,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371,314,340,347,343,81,368,99,75])). % 60.01/60.09 cnf(5128,plain, % 60.01/60.09 (P11(a8,f42(f36(a8)))), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4942,4944,4946,4952,4956,4960,4962,4968,4964,4729,4693,4666,4905,4998,4894,4966,4936,4856,4647,4581,4725,120,143,145,149,436,129,217,5093,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371,314,340,347,343,81,368,99,75,89,77,73])). % 60.01/60.09 cnf(5135,plain, % 60.01/60.09 (~P12(f39(a30),f39(f31(f39(a30))))), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4934,4940,4942,4944,4946,4948,4952,4956,4960,4962,4968,4964,4729,4693,4666,4905,4998,4894,4972,4966,4936,4835,4856,4647,4899,4581,4532,4725,120,143,145,149,436,129,217,5093,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371,314,340,347,343,81,368,99,75,89,77,73,91,88,101,78,82,362])). % 60.01/60.09 cnf(5138,plain, % 60.01/60.09 (~E(a30,f46(a19))), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4934,4940,4942,4944,4946,4948,4952,4956,4960,4962,4968,4964,4729,4693,4666,4905,4998,4894,4972,4966,4936,4835,4856,4647,4899,4581,4532,4725,120,143,145,149,436,129,217,5093,479,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371,314,340,347,343,81,368,99,75,89,77,73,91,88,101,78,82,362,3])). % 60.01/60.09 cnf(5142,plain, % 60.01/60.09 (~P41(f42(f36(a8)))), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4934,4940,4942,4944,4946,4948,4952,4956,4960,4962,4968,4964,4729,4693,4666,4905,4998,4894,4972,4966,4936,4835,4856,4647,4899,4653,4581,4532,4725,120,143,145,149,436,129,217,5093,479,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371,314,340,347,343,81,368,99,75,89,77,73,91,88,101,78,82,362,3,59,286,315])). % 60.01/60.09 cnf(5146,plain, % 60.01/60.09 (~P11(a1,f42(f36(a8)))), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4934,4940,4942,4944,4946,4948,4952,4956,4960,4962,4968,4964,4729,4693,4666,4905,4998,4894,4972,4966,4936,4835,4856,4647,4899,4653,4581,4532,4725,120,143,145,149,436,129,217,5093,479,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371,314,340,347,343,81,368,99,75,89,77,73,91,88,101,78,82,362,3,59,286,315,316,353])). % 60.01/60.09 cnf(5157,plain, % 60.01/60.09 (P25(f10(x51571,x51572))), % 60.01/60.09 inference(rename_variables,[],[218])). % 60.01/60.09 cnf(5159,plain, % 60.01/60.09 (~P30(f10(f3(a15),a9))), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4934,4940,4942,4944,4946,4948,4952,4956,4960,4962,4968,4964,4729,4693,4666,4905,5000,4998,4894,4972,4966,4936,4988,4982,4835,4856,4647,4899,4653,4581,4532,4677,4725,120,143,145,239,149,436,129,217,5093,479,218,5157,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371,314,340,347,343,81,368,99,75,89,77,73,91,88,101,78,82,362,3,59,286,315,316,353,287,317,320,358,392,390])). % 60.01/60.09 cnf(5162,plain, % 60.01/60.09 (P11(f35(a8),f35(a8))), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4934,4940,4942,4944,4946,4948,4952,4956,4958,4960,4962,4968,4964,4729,4693,4666,4905,5000,4998,4894,4972,4966,4936,4988,4982,4835,4856,4647,4899,4653,4581,4532,4677,4725,120,143,145,239,149,436,129,217,5093,479,218,5157,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371,314,340,347,343,81,368,99,75,89,77,73,91,88,101,78,82,362,3,59,286,315,316,353,287,317,320,358,392,390,356])). % 60.01/60.09 cnf(5171,plain, % 60.01/60.09 (~P12(f46(a19),f27(f31(f39(a30)),f46(a19)))), % 60.01/60.09 inference(scs_inference,[],[131,134,4633,4814,4860,4934,4940,4942,4944,4946,4948,4952,4956,4958,4960,4962,4968,4964,4729,4693,4666,4905,5000,4998,4894,4972,4966,4936,4988,4982,4835,4856,4647,4899,4653,4581,4532,4677,4725,120,143,145,239,149,436,111,122,232,129,217,5093,479,218,5157,954,267,297,261,259,263,387,363,388,260,367,256,366,268,39,255,298,18,25,264,258,389,5,14,32,21,15,33,34,31,28,19,6,10,16,547,23,11,37,4,30,27,22,26,7,17,38,20,36,9,29,13,35,12,40,24,8,2,333,338,65,85,299,282,304,329,357,266,354,283,371,314,340,347,343,81,368,99,75,89,77,73,91,88,101,78,82,362,3,59,286,315,316,353,287,317,320,358,392,390,356,365,243,318,933,349])). % 60.01/60.09 cnf(5213,plain, % 60.01/60.09 (P9(f40(a29),f44(f46(a29),f46(a29)),f46(a29))), % 60.01/60.09 inference(scs_inference,[],[4679,4592,4983,5076,267,954,388,387])). % 60.01/60.09 cnf(5227,plain, % 60.01/60.09 (P6(f42(f36(a1)))), % 60.01/60.09 inference(scs_inference,[],[4679,5016,4592,4807,4914,4983,4583,5076,267,954,388,387,366,261,263,256,297,260,259])). % 60.01/60.09 cnf(5235,plain, % 60.01/60.09 (P4(f42(f36(a1)))), % 60.01/60.09 inference(scs_inference,[],[4679,5016,4592,4807,4914,4983,4583,5076,267,954,388,387,366,261,263,256,297,260,259,268,258,389,255])). % 60.01/60.09 cnf(5254,plain, % 60.01/60.09 (E(f42(f37(f46(a15),f47(a15))),f42(a15))), % 60.01/60.09 inference(scs_inference,[],[4679,5016,5037,4592,4807,4914,5100,5146,4983,4583,5076,267,954,388,387,366,261,263,256,297,260,259,268,258,389,255,367,25,298,14,264,33,28,18,39,547,5,15,4,23,31])). % 60.01/60.09 cnf(5266,plain, % 60.01/60.09 (E(f10(f37(f46(a15),f47(a15)),x52661),f10(a15,x52661))), % 60.01/60.09 inference(scs_inference,[],[4679,5016,5037,4592,4807,4914,5100,5146,4983,4583,5076,267,954,388,387,366,261,263,256,297,260,259,268,258,389,255,367,25,298,14,264,33,28,18,39,547,5,15,4,23,31,32,6,22,21,16,20,27,38,11,37,10,9])). % 60.01/60.09 cnf(5277,plain, % 60.01/60.09 (E(f24(f37(f46(a15),f47(a15))),f24(a15))), % 60.01/60.09 inference(scs_inference,[],[4679,5016,5037,4592,4807,4914,5100,5146,4983,4583,5076,267,954,388,387,366,261,263,256,297,260,259,268,258,389,255,367,25,298,14,264,33,28,18,39,547,5,15,4,23,31,32,6,22,21,16,20,27,38,11,37,10,9,34,36,19,30,7,26,35,13,12,17,40])). % 60.01/60.09 cnf(5281,plain, % 60.01/60.09 (~E(f21(a19),a30)), % 60.01/60.09 inference(scs_inference,[],[4679,5016,5037,5125,4592,4807,4914,5100,5146,4983,4583,5076,267,954,388,387,366,261,263,256,297,260,259,268,258,389,255,367,25,298,14,264,33,28,18,39,547,5,15,4,23,31,32,6,22,21,16,20,27,38,11,37,10,9,34,36,19,30,7,26,35,13,12,17,40,29,24,8,2])). % 60.01/60.09 cnf(5282,plain, % 60.01/60.09 (P37(f27(f31(f39(a30)),f39(a30)))), % 60.01/60.09 inference(scs_inference,[],[4679,5016,5037,5125,4592,4807,5114,4914,5100,5146,4983,4583,5076,4581,267,954,388,387,366,261,263,256,297,260,259,268,258,389,255,367,25,298,14,264,33,28,18,39,547,5,15,4,23,31,32,6,22,21,16,20,27,38,11,37,10,9,34,36,19,30,7,26,35,13,12,17,40,29,24,8,2,61])). % 60.01/60.09 cnf(5285,plain, % 60.01/60.09 (P8(f31(x52851),x52851)), % 60.01/60.09 inference(rename_variables,[],[217])). % 60.01/60.09 cnf(5288,plain, % 60.01/60.09 (P8(f31(x52881),x52881)), % 60.01/60.09 inference(rename_variables,[],[217])). % 60.01/60.09 cnf(5306,plain, % 60.01/60.09 (P11(f42(f36(a8)),f35(a8))), % 60.01/60.09 inference(scs_inference,[],[135,4679,4797,4954,5016,5037,5162,5125,4592,4807,5118,5114,433,4914,5100,5146,4983,5089,4583,5135,5076,4542,4581,121,4721,4952,217,5285,5288,4966,267,954,388,387,366,261,263,256,297,260,259,268,258,389,255,367,25,298,14,264,33,28,18,39,547,5,15,4,23,31,32,6,22,21,16,20,27,38,11,37,10,9,34,36,19,30,7,26,35,13,12,17,40,29,24,8,2,61,309,300,329,282,283,354,311,371,347,63,72])). % 60.01/60.09 cnf(5307,plain, % 60.01/60.09 (~P8(f46(a19),f39(f31(f39(a30))))), % 60.01/60.09 inference(scs_inference,[],[135,4679,4797,4954,5016,5037,5162,5125,4592,4807,5118,5114,433,4914,5100,5146,4983,5121,5089,4583,5135,5076,4542,4581,121,4721,500,4952,217,5285,5288,4966,267,954,388,387,366,261,263,256,297,260,259,268,258,389,255,367,25,298,14,264,33,28,18,39,547,5,15,4,23,31,32,6,22,21,16,20,27,38,11,37,10,9,34,36,19,30,7,26,35,13,12,17,40,29,24,8,2,61,309,300,329,282,283,354,311,371,347,63,72,361])). % 60.01/60.09 cnf(5310,plain, % 60.01/60.09 (P12(f27(a30,f21(a19)),f21(a19))), % 60.01/60.09 inference(scs_inference,[],[135,4679,4797,4954,5016,5037,5162,5125,4592,4807,5118,5114,433,4914,5100,5146,4983,5121,5089,4583,5135,5076,5057,4542,4581,121,4721,500,407,4952,217,5285,5288,4966,267,954,388,387,366,261,263,256,297,260,259,268,258,389,255,367,25,298,14,264,33,28,18,39,547,5,15,4,23,31,32,6,22,21,16,20,27,38,11,37,10,9,34,36,19,30,7,26,35,13,12,17,40,29,24,8,2,61,309,300,329,282,283,354,311,371,347,63,72,361,51,368])). % 60.01/60.09 cnf(5314,plain, % 60.01/60.09 (~E(f31(f39(a30)),f24(a15))), % 60.01/60.09 inference(scs_inference,[],[135,4679,4797,4954,5016,5037,5162,5125,4592,4807,5118,5114,433,4914,5100,5146,4983,5121,5089,4583,5135,5076,5057,4902,4542,4581,121,4721,500,407,4952,217,5285,5288,4966,267,954,388,387,366,261,263,256,297,260,259,268,258,389,255,367,25,298,14,264,33,28,18,39,547,5,15,4,23,31,32,6,22,21,16,20,27,38,11,37,10,9,34,36,19,30,7,26,35,13,12,17,40,29,24,8,2,61,309,300,329,282,283,354,311,371,347,63,72,361,51,368,62,75])). % 60.01/60.09 cnf(5323,plain, % 60.01/60.09 (~P8(f46(a19),f39(a30))), % 60.01/60.09 inference(scs_inference,[],[135,4679,4797,4954,5016,5037,5162,5125,4592,4807,5118,5114,4641,433,4914,4901,5100,5146,4983,5121,5089,4583,5135,5052,5076,5057,4902,4839,4542,4723,4581,4532,121,4721,500,407,4952,217,5285,5288,4966,267,954,388,387,366,261,263,256,297,260,259,268,258,389,255,367,25,298,14,264,33,28,18,39,547,5,15,4,23,31,32,6,22,21,16,20,27,38,11,37,10,9,34,36,19,30,7,26,35,13,12,17,40,29,24,8,2,61,309,300,329,282,283,354,311,371,347,63,72,361,51,368,62,75,73,362,3,59,60])). % 60.01/60.09 cnf(5361,plain, % 60.01/60.09 (P9(f41(a22),f44(f46(a22),f46(a22)),f46(a22))), % 60.01/60.09 inference(scs_inference,[],[4877,4594,5227,5266,267,297,954,263,387])). % 60.01/60.09 cnf(5371,plain, % 60.01/60.09 (P3(f37(f46(a11),f47(a11)))), % 60.01/60.09 inference(scs_inference,[],[4877,4594,5227,4986,5266,4812,267,297,954,263,387,261,388,268,260,366])). % 60.01/60.09 cnf(5379,plain, % 60.01/60.09 (P6(f38(f34(a15),f45(a15),f45(a15)))), % 60.01/60.09 inference(scs_inference,[],[4877,4594,5032,4970,5227,4986,5266,4812,267,297,954,263,387,261,388,268,260,366,256,389,367,259])). % 60.01/60.09 cnf(5381,plain, % 60.01/60.09 (P4(f38(f34(a15),f45(a15),f45(a15)))), % 60.01/60.09 inference(scs_inference,[],[4877,4594,5032,4970,5227,4986,5266,4812,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255])). % 60.01/60.09 cnf(5394,plain, % 60.01/60.09 (E(f38(x53941,f38(f46(a6),f40(a6),f41(a6)),x53942),f38(x53941,a6,x53942))), % 60.01/60.09 inference(scs_inference,[],[4877,4594,5032,4970,5227,5235,5110,4986,5266,4812,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255,298,14,33,264,25,28,39,4,32,20])). % 60.01/60.09 cnf(5404,plain, % 60.01/60.09 (E(f10(f38(f46(a6),f40(a6),f41(a6)),x54041),f10(a6,x54041))), % 60.01/60.09 inference(scs_inference,[],[4877,4594,5032,4970,5227,5235,5110,4986,5266,4812,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255,298,14,33,264,25,28,39,4,32,20,18,15,27,31,37,22,16,5,34,9])). % 60.01/60.09 cnf(5406,plain, % 60.01/60.09 (E(f38(x54061,x54062,f38(f46(a6),f40(a6),f41(a6))),f38(x54061,x54062,a6))), % 60.01/60.09 inference(scs_inference,[],[4877,4594,5032,4970,5227,5235,5110,4986,5266,4812,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255,298,14,33,264,25,28,39,4,32,20,18,15,27,31,37,22,16,5,34,9,38,21])). % 60.01/60.09 cnf(5424,plain, % 60.01/60.09 (~E(f46(a19),a30)), % 60.01/60.09 inference(scs_inference,[],[4877,5138,4594,5032,4970,5227,5235,5110,4986,5266,4812,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255,298,14,33,264,25,28,39,4,32,20,18,15,27,31,37,22,16,5,34,9,38,21,23,26,11,7,6,13,19,35,10,36,40,29,17,30,12,24,8,2])). % 60.01/60.09 cnf(5426,plain, % 60.01/60.09 (P8(f31(x54261),x54261)), % 60.01/60.09 inference(rename_variables,[],[217])). % 60.01/60.09 cnf(5429,plain, % 60.01/60.09 (P8(f31(x54291),x54291)), % 60.01/60.09 inference(rename_variables,[],[217])). % 60.01/60.09 cnf(5437,plain, % 60.01/60.09 (E(f38(f46(a14),f40(a14),f41(a14)),a14)), % 60.01/60.09 inference(scs_inference,[],[136,4828,4877,5138,4594,5032,4970,5120,5142,5227,5235,5110,4986,5282,5266,4812,4675,217,5426,123,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255,298,14,33,264,25,28,39,4,32,20,18,15,27,31,37,22,16,5,34,9,38,21,23,26,11,7,6,13,19,35,10,36,40,29,17,30,12,24,8,2,305,308,283,354,282,371])). % 60.01/60.09 cnf(5441,plain, % 60.01/60.09 (~P8(f21(a19),f39(a30))), % 60.01/60.09 inference(scs_inference,[],[136,4828,4877,5138,4594,5310,5032,1237,4970,5120,5142,5227,5235,5110,4986,5282,5266,4812,4675,149,217,5426,123,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255,298,14,33,264,25,28,39,4,32,20,18,15,27,31,37,22,16,5,34,9,38,21,23,26,11,7,6,13,19,35,10,36,40,29,17,30,12,24,8,2,305,308,283,354,282,371,347,361])). % 60.01/60.09 cnf(5443,plain, % 60.01/60.09 (~E(a8,a1)), % 60.01/60.09 inference(scs_inference,[],[136,4828,4877,5138,4594,5310,5032,1237,4970,5120,5142,5227,5235,5110,5128,4986,5282,5266,4812,4675,5146,149,217,5426,123,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255,298,14,33,264,25,28,39,4,32,20,18,15,27,31,37,22,16,5,34,9,38,21,23,26,11,7,6,13,19,35,10,36,40,29,17,30,12,24,8,2,305,308,283,354,282,371,347,361,72])). % 60.01/60.09 cnf(5446,plain, % 60.01/60.09 (P12(f27(f31(f39(a30)),f24(a15)),f24(a15))), % 60.01/60.09 inference(scs_inference,[],[136,4828,4877,5138,4594,5314,5310,5032,1237,4970,5120,5142,5227,5235,5110,5128,4986,5282,5171,5266,4812,4675,5146,4581,149,436,217,5426,123,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255,298,14,33,264,25,28,39,4,32,20,18,15,27,31,37,22,16,5,34,9,38,21,23,26,11,7,6,13,19,35,10,36,40,29,17,30,12,24,8,2,305,308,283,354,282,371,347,361,72,63,368])). % 60.01/60.09 cnf(5453,plain, % 60.01/60.09 (~E(a30,f46(a8))), % 60.01/60.09 inference(scs_inference,[],[136,4828,4877,5323,5138,4594,5314,5310,5032,1237,4970,5120,5142,5227,5235,5110,5128,4986,5282,5171,5266,5254,4812,4675,5146,4581,4532,149,436,217,5426,123,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255,298,14,33,264,25,28,39,4,32,20,18,15,27,31,37,22,16,5,34,9,38,21,23,26,11,7,6,13,19,35,10,36,40,29,17,30,12,24,8,2,305,308,283,354,282,371,347,361,72,63,368,362,52,75])). % 60.01/60.09 cnf(5461,plain, % 60.01/60.09 (P2(f38(f46(a29),f40(a29),f40(a29)))), % 60.01/60.09 inference(scs_inference,[],[136,4524,4828,4877,5323,5138,5281,4594,4588,5213,5314,5310,5032,1237,4970,5120,5142,5227,5235,5110,5128,4915,4986,5282,5171,5266,5254,4812,4675,5146,4683,4581,4532,149,436,217,5426,5429,479,123,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255,298,14,33,264,25,28,39,4,32,20,18,15,27,31,37,22,16,5,34,9,38,21,23,26,11,7,6,13,19,35,10,36,40,29,17,30,12,24,8,2,305,308,283,354,282,371,347,361,72,63,368,362,52,75,73,3,59,60,395,394])). % 60.01/60.09 cnf(5465,plain, % 60.01/60.09 (~P11(f42(f36(a8)),a1)), % 60.01/60.09 inference(scs_inference,[],[106,136,4524,4828,4877,5323,5138,5281,4594,4588,5213,4799,5314,5310,5032,1237,4970,5002,5004,5120,5142,5227,5235,5110,5128,4915,4986,5282,5171,5266,5254,4812,4675,5146,4683,4581,4532,4691,4673,4671,4677,5020,4689,149,436,217,5426,5429,227,116,479,123,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255,298,14,33,264,25,28,39,4,32,20,18,15,27,31,37,22,16,5,34,9,38,21,23,26,11,7,6,13,19,35,10,36,40,29,17,30,12,24,8,2,305,308,283,354,282,371,347,361,72,63,368,362,52,75,73,3,59,60,395,394,400,365])). % 60.01/60.09 cnf(5467,plain, % 60.01/60.09 (P5(f38(f34(a15),f45(a15),f45(a15)))), % 60.01/60.09 inference(scs_inference,[],[106,136,4524,4828,4877,5323,5138,5281,4594,4588,5213,4799,5314,5310,5032,1237,4970,5002,5004,5120,5142,5227,5235,5110,5128,4915,4986,5282,5171,5266,5254,4812,4675,5146,4683,4581,4532,4691,4673,4671,4677,5020,4689,149,436,217,5426,5429,227,116,479,123,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255,298,14,33,264,25,28,39,4,32,20,18,15,27,31,37,22,16,5,34,9,38,21,23,26,11,7,6,13,19,35,10,36,40,29,17,30,12,24,8,2,305,308,283,354,282,371,347,361,72,63,368,362,52,75,73,3,59,60,395,394,400,365,257])). % 60.01/60.09 cnf(5475,plain, % 60.01/60.09 (~P12(f24(a15),f27(f31(f39(a30)),f24(a15)))), % 60.01/60.09 inference(scs_inference,[],[106,136,4524,4828,4877,5323,5138,5281,4594,4588,5213,4799,5314,5310,5032,1237,4970,5002,5004,5120,5142,5227,5235,5110,5128,4915,4986,5282,5171,5266,5254,4812,4675,5146,4683,4581,4532,4691,4673,4671,4677,5020,4689,149,436,217,5426,5429,227,116,479,123,267,297,954,263,387,261,388,268,260,366,256,389,367,259,255,298,14,33,264,25,28,39,4,32,20,18,15,27,31,37,22,16,5,34,9,38,21,23,26,11,7,6,13,19,35,10,36,40,29,17,30,12,24,8,2,305,308,283,354,282,371,347,361,72,63,368,362,52,75,73,3,59,60,395,394,400,365,257,831,318,933,547,349])). % 60.01/60.09 cnf(5512,plain, % 60.01/60.09 (P3(f37(f46(a15),f47(a15)))), % 60.01/60.09 inference(scs_inference,[],[4881,4844,5379,5371,5404,4981,5022,267,263,297,260,387,268,954,256,261,388,366])). % 60.01/60.09 cnf(5518,plain, % 60.01/60.09 (P6(f38(f46(a29),f40(a29),f40(a29)))), % 60.01/60.09 inference(scs_inference,[],[4881,4844,5379,5371,5461,5404,4981,5022,267,263,297,260,387,268,954,256,261,388,366,389,367,259])). % 60.01/60.09 cnf(5520,plain, % 60.01/60.09 (P4(f38(f46(a29),f40(a29),f40(a29)))), % 60.01/60.09 inference(scs_inference,[],[4881,4844,5379,5371,5461,5404,4981,5022,267,263,297,260,387,268,954,256,261,388,366,389,367,259,255])). % 60.01/60.09 cnf(5548,plain, % 60.01/60.09 (E(f10(f38(f46(a14),f40(a14),f41(a14)),x55481),f10(a14,x55481))), % 60.01/60.09 inference(scs_inference,[],[4881,4844,5379,5381,5371,5461,5437,5404,4981,5022,267,263,297,260,387,268,954,256,261,388,366,389,367,259,255,14,298,25,33,28,264,32,4,31,15,22,37,20,18,39,38,21,34,16,26,27,23,5,11,9])). % 60.01/60.09 cnf(5566,plain, % 60.01/60.09 (E(f38(f46(a18),f40(a18),f41(a18)),a18)), % 60.01/60.09 inference(scs_inference,[],[5443,137,4881,5030,4844,5379,5381,5371,5461,5437,5404,4981,5022,4962,124,267,263,297,260,387,268,954,256,261,388,366,389,367,259,255,14,298,25,33,28,264,32,4,31,15,22,37,20,18,39,38,21,34,16,26,27,23,5,11,9,6,7,17,35,36,10,19,13,40,24,29,12,30,8,2,354,371])). % 60.01/60.09 cnf(5568,plain, % 60.01/60.09 (P44(f27(f31(f39(a30)),f39(a30)))), % 60.01/60.09 inference(scs_inference,[],[5443,137,4881,5030,4844,5379,5381,5371,5461,5437,5404,4981,5022,4915,147,4962,124,267,263,297,260,387,268,954,256,261,388,366,389,367,259,255,14,298,25,33,28,264,32,4,31,15,22,37,20,18,39,38,21,34,16,26,27,23,5,11,9,6,7,17,35,36,10,19,13,40,24,29,12,30,8,2,354,371,345])). % 60.01/60.09 cnf(5573,plain, % 60.01/60.09 (E(f27(a30,x55731),f27(f31(f39(a30)),x55731))), % 60.01/60.09 inference(rename_variables,[],[4581])). % 60.01/60.09 cnf(5586,plain, % 60.01/60.09 (~P11(f35(a8),a1)), % 60.01/60.09 inference(scs_inference,[],[5443,137,4881,5030,5424,4844,5379,5381,5371,5461,4805,5437,5465,5446,5404,4981,5022,4915,5118,4581,147,4962,500,407,217,4966,124,267,263,297,260,387,268,954,256,261,388,366,389,367,259,255,14,298,25,33,28,264,32,4,31,15,22,37,20,18,39,38,21,34,16,26,27,23,5,11,9,6,7,17,35,36,10,19,13,40,24,29,12,30,8,2,354,371,345,282,56,311,283,347,361,368,72])). % 60.01/60.09 cnf(5587,plain, % 60.01/60.09 (~P12(f24(a15),f27(a30,f24(a15)))), % 60.01/60.09 inference(scs_inference,[],[5443,137,4881,5030,5424,4844,5379,5381,5371,5461,4805,5437,5465,5446,5475,5404,4981,5022,4915,5118,4581,5573,147,4962,500,407,217,4966,124,267,263,297,260,387,268,954,256,261,388,366,389,367,259,255,14,298,25,33,28,264,32,4,31,15,22,37,20,18,39,38,21,34,16,26,27,23,5,11,9,6,7,17,35,36,10,19,13,40,24,29,12,30,8,2,354,371,345,282,56,311,283,347,361,368,72,63])). % 60.01/60.09 cnf(5591,plain, % 60.01/60.09 (~E(f31(f39(a30)),f21(a8))), % 60.01/60.09 inference(scs_inference,[],[5443,137,4881,5030,5424,4844,4685,5379,5381,5371,5461,4805,5437,5465,5446,5475,5404,4981,5022,4915,5118,4581,5573,147,4962,500,407,217,4966,124,267,263,297,260,387,268,954,256,261,388,366,389,367,259,255,14,298,25,33,28,264,32,4,31,15,22,37,20,18,39,38,21,34,16,26,27,23,5,11,9,6,7,17,35,36,10,19,13,40,24,29,12,30,8,2,354,371,345,282,56,311,283,347,361,368,72,63,362,75])). % 60.01/60.09 cnf(5596,plain, % 60.01/60.09 (~E(f39(f46(a19)),f39(a30))), % 60.01/60.09 inference(scs_inference,[],[5443,137,4881,5030,5441,5424,4844,5306,4685,5379,5381,5371,5461,4805,5437,5465,5446,5475,5394,5406,5404,4981,5022,4641,4915,5118,4581,5573,147,4962,500,407,217,4966,124,267,263,297,260,387,268,954,256,261,388,366,389,367,259,255,14,298,25,33,28,264,32,4,31,15,22,37,20,18,39,38,21,34,16,26,27,23,5,11,9,6,7,17,35,36,10,19,13,40,24,29,12,30,8,2,354,371,345,282,56,311,283,347,361,368,72,63,362,75,73,3,60])). % 60.01/60.09 cnf(5601,plain, % 60.01/60.09 (P2(f38(f46(a22),f41(a22),f41(a22)))), % 60.01/60.09 inference(scs_inference,[],[5443,137,4526,4881,5030,5441,5424,4844,4590,5361,5306,4685,5379,5381,5371,5461,4805,5437,5465,5446,5475,5394,5406,5404,4981,5022,4641,4915,5118,4581,5573,4532,147,4962,500,407,217,4966,124,267,263,297,260,387,268,954,256,261,388,366,389,367,259,255,14,298,25,33,28,264,32,4,31,15,22,37,20,18,39,38,21,34,16,26,27,23,5,11,9,6,7,17,35,36,10,19,13,40,24,29,12,30,8,2,354,371,345,282,56,311,283,347,361,368,72,63,362,75,73,3,60,59,395,394])). % 60.01/60.09 cnf(5717,plain, % 60.01/60.09 (P8(x57171,f39(x57171))), % 60.01/60.09 inference(rename_variables,[],[4532])). % 60.01/60.09 cnf(5738,plain, % 60.01/60.09 ($false), % 60.01/60.09 inference(scs_inference,[],[138,4978,5453,5586,4842,5591,5596,4643,5467,5512,5159,5518,5520,5601,4832,5587,5566,5568,5548,4987,5307,5277,4976,1236,663,409,729,4723,4936,5446,224,605,4915,216,529,601,496,483,4532,5717,241,4725,436,149,217,125,267,263,260,297,387,261,256,268,388,389,954,264,298,255,259,28,25,4,33,31,14,18,37,38,15,22,39,27,32,23,20,21,11,16,5,34,9,26,933,19,36,10,24,35,7,30,6,17,13,8,40,29,12,2,47,328,46,70,79,313,371,43,282,283,80,346,373,69,347,361,44,49,368,62,72,362,75,73]), % 60.01/60.09 ['proof']). % 60.01/60.09 % SZS output end Proof % 60.01/60.09 % Total time :59.330000s %------------------------------------------------------------------------------