%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : TOP025+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 : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 21:15:07 EDT 2024 % Result : Theorem 148.66s 148.87s % Output : CNFRefutation 148.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.14 % Problem : TOP025+1 : TPTP v8.2.0. Released v3.4.0. % 0.11/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n027.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 : Tue Jun 18 11:00:09 EDT 2024 % 0.13/0.36 % CPUTime : % 0.50/0.59 start to proof:theBenchmark % 148.66/148.84 %------------------------------------------- % 148.66/148.84 % File :CSE---1.7 % 148.66/148.84 % Problem :theBenchmark % 148.66/148.84 % Transform :cnf % 148.66/148.84 % Format :tptp:raw % 148.66/148.84 % Command :java -jar mcs_scs.jar %d %s % 148.66/148.84 % 148.66/148.84 % Result :Theorem 148.030000s % 148.66/148.84 % Output :CNFRefutation 148.030000s % 148.66/148.84 %------------------------------------------- % 148.66/148.86 %------------------------------------------------------------------------------ % 148.66/148.86 % File : TOP025+1 : TPTP v8.2.0. Released v3.4.0. % 148.66/148.86 % Domain : Topology % 148.66/148.86 % Problem : Maximal Kolmogorov Subspaces of a Topological Space T03 % 148.66/148.86 % Version : [Urb08] axioms : Especial. % 148.66/148.86 % English : % 148.66/148.86 % 148.66/148.86 % Refs : [Kar96] Karno (1996), Maximal Kolmogorov Subspaces of a Topolo % 148.66/148.86 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 148.66/148.86 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 148.66/148.86 % Source : [Urb08] % 148.66/148.86 % Names : t3_tsp_2 [Urb08] % 148.66/148.86 % 148.66/148.86 % Status : Theorem % 148.66/148.86 % Rating : 0.22 v8.2.0, 0.19 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.13 v7.3.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.2.0, 0.20 v6.0.0, 0.09 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.33 v5.2.0, 0.20 v5.1.0, 0.29 v5.0.0, 0.17 v4.1.0, 0.22 v4.0.1, 0.26 v4.0.0, 0.29 v3.7.0, 0.15 v3.5.0, 0.16 v3.4.0 % 148.66/148.86 % Syntax : Number of formulae : 61 ( 10 unt; 0 def) % 148.66/148.86 % Number of atoms : 248 ( 6 equ) % 148.66/148.86 % Maximal formula atoms : 15 ( 4 avg) % 148.66/148.86 % Number of connectives : 212 ( 25 ~; 2 |; 111 &) % 148.66/148.86 % ( 3 <=>; 71 =>; 0 <=; 0 <~>) % 148.66/148.86 % Maximal formula depth : 15 ( 5 avg) % 148.66/148.86 % Maximal term depth : 3 ( 1 avg) % 148.66/148.86 % Number of predicates : 27 ( 25 usr; 1 prp; 0-2 aty) % 148.66/148.86 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 148.66/148.86 % Number of variables : 99 ( 84 !; 15 ?) % 148.66/148.86 % SPC : FOF_THM_RFO_SEQ % 148.66/148.86 % 148.66/148.86 % Comments : Normal version: includes the axioms (which may be theorems from % 148.66/148.86 % other articles) and background that are possibly necessary. % 148.66/148.86 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 148.66/148.86 % : The problem encoding is based on set theory. % 148.66/148.86 %------------------------------------------------------------------------------ % 148.66/148.86 fof(t3_tsp_2,conjecture, % 148.66/148.86 ! [A] : % 148.66/148.86 ( ( ~ v3_struct_0(A) % 148.66/148.86 & v2_pre_topc(A) % 148.66/148.86 & l1_pre_topc(A) ) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.86 => ~ ( ( v3_pre_topc(B,A) % 148.66/148.86 | v4_pre_topc(B,A) ) % 148.66/148.86 & v1_tsp_2(B,A) % 148.66/148.86 & v1_tex_2(B,k1_zfmisc_1(u1_struct_0(A))) ) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(antisymmetry_r2_hidden,axiom, % 148.66/148.86 ! [A,B] : % 148.66/148.86 ( r2_hidden(A,B) % 148.66/148.86 => ~ r2_hidden(B,A) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc10_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v1_membered(A) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,A) % 148.66/148.86 => v1_xcmplx_0(B) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc11_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v2_membered(A) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,A) % 148.66/148.86 => ( v1_xcmplx_0(B) % 148.66/148.86 & v1_xreal_0(B) ) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc12_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v3_membered(A) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,A) % 148.66/148.86 => ( v1_xcmplx_0(B) % 148.66/148.86 & v1_xreal_0(B) % 148.66/148.86 & v1_rat_1(B) ) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc13_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v4_membered(A) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,A) % 148.66/148.86 => ( v1_xcmplx_0(B) % 148.66/148.86 & v1_xreal_0(B) % 148.66/148.86 & v1_int_1(B) % 148.66/148.86 & v1_rat_1(B) ) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc14_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v5_membered(A) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,A) % 148.66/148.86 => ( v1_xcmplx_0(B) % 148.66/148.86 & v4_ordinal2(B) % 148.66/148.86 & v1_xreal_0(B) % 148.66/148.86 & v1_int_1(B) % 148.66/148.86 & v1_rat_1(B) ) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc15_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v1_xboole_0(A) % 148.66/148.86 => ( v1_membered(A) % 148.66/148.86 & v2_membered(A) % 148.66/148.86 & v3_membered(A) % 148.66/148.86 & v4_membered(A) % 148.66/148.86 & v5_membered(A) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc16_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v1_membered(A) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,k1_zfmisc_1(A)) % 148.66/148.86 => v1_membered(B) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc17_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v2_membered(A) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,k1_zfmisc_1(A)) % 148.66/148.86 => ( v1_membered(B) % 148.66/148.86 & v2_membered(B) ) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc18_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v3_membered(A) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,k1_zfmisc_1(A)) % 148.66/148.86 => ( v1_membered(B) % 148.66/148.86 & v2_membered(B) % 148.66/148.86 & v3_membered(B) ) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc19_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v4_membered(A) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,k1_zfmisc_1(A)) % 148.66/148.86 => ( v1_membered(B) % 148.66/148.86 & v2_membered(B) % 148.66/148.86 & v3_membered(B) % 148.66/148.86 & v4_membered(B) ) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc1_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v5_membered(A) % 148.66/148.86 => v4_membered(A) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc1_tops_1,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( ( v2_pre_topc(A) % 148.66/148.86 & l1_pre_topc(A) ) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.86 => ( v1_xboole_0(B) % 148.66/148.86 => ( v3_pre_topc(B,A) % 148.66/148.86 & v4_pre_topc(B,A) ) ) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc20_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v5_membered(A) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,k1_zfmisc_1(A)) % 148.66/148.86 => ( v1_membered(B) % 148.66/148.86 & v2_membered(B) % 148.66/148.86 & v3_membered(B) % 148.66/148.86 & v4_membered(B) % 148.66/148.86 & v5_membered(B) ) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc2_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v4_membered(A) % 148.66/148.86 => v3_membered(A) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc2_tops_1,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( l1_pre_topc(A) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.86 => ( v1_xboole_0(B) % 148.66/148.86 => v2_tops_1(B,A) ) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc3_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v3_membered(A) % 148.66/148.86 => v2_membered(A) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc3_tops_1,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( ( v2_pre_topc(A) % 148.66/148.86 & l1_pre_topc(A) ) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.86 => ( v1_xboole_0(B) % 148.66/148.86 => v3_tops_1(B,A) ) ) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc4_membered,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( v2_membered(A) % 148.66/148.86 => v1_membered(A) ) ). % 148.66/148.86 % 148.66/148.86 fof(cc4_tops_1,axiom, % 148.66/148.86 ! [A] : % 148.66/148.86 ( ( v2_pre_topc(A) % 148.66/148.86 & l1_pre_topc(A) ) % 148.66/148.86 => ! [B] : % 148.66/148.86 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.86 => ( v3_tops_1(B,A) % 148.66/148.86 => v2_tops_1(B,A) ) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(cc5_tops_1,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ( v2_pre_topc(A) % 148.66/148.87 & l1_pre_topc(A) ) % 148.66/148.87 => ! [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.87 => ( ( v4_pre_topc(B,A) % 148.66/148.87 & v2_tops_1(B,A) ) % 148.66/148.87 => ( v2_tops_1(B,A) % 148.66/148.87 & v3_tops_1(B,A) ) ) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(cc6_tops_1,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ( v2_pre_topc(A) % 148.66/148.87 & l1_pre_topc(A) ) % 148.66/148.87 => ! [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.87 => ( ( v3_pre_topc(B,A) % 148.66/148.87 & v3_tops_1(B,A) ) % 148.66/148.87 => ( v1_xboole_0(B) % 148.66/148.87 & v3_pre_topc(B,A) % 148.66/148.87 & v4_pre_topc(B,A) % 148.66/148.87 & v1_membered(B) % 148.66/148.87 & v2_membered(B) % 148.66/148.87 & v3_membered(B) % 148.66/148.87 & v4_membered(B) % 148.66/148.87 & v5_membered(B) % 148.66/148.87 & v2_tops_1(B,A) % 148.66/148.87 & v3_tops_1(B,A) ) ) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(d5_tsp_2,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ( ~ v3_struct_0(A) % 148.66/148.87 & v2_pre_topc(A) % 148.66/148.87 & l1_pre_topc(A) ) % 148.66/148.87 => ! [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.87 => ( v1_tsp_2(B,A) % 148.66/148.87 <=> ( v1_tsp_1(B,A) % 148.66/148.87 & k3_tex_4(A,B) = u1_struct_0(A) ) ) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(dt_k1_xboole_0,axiom, % 148.66/148.87 $true ). % 148.66/148.87 % 148.66/148.87 fof(dt_k1_zfmisc_1,axiom, % 148.66/148.87 $true ). % 148.66/148.87 % 148.66/148.87 fof(dt_k3_tex_4,axiom, % 148.66/148.87 ! [A,B] : % 148.66/148.87 ( ( ~ v3_struct_0(A) % 148.66/148.87 & l1_pre_topc(A) % 148.66/148.87 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 148.66/148.87 => m1_subset_1(k3_tex_4(A,B),k1_zfmisc_1(u1_struct_0(A))) ) ). % 148.66/148.87 % 148.66/148.87 fof(dt_l1_pre_topc,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( l1_pre_topc(A) % 148.66/148.87 => l1_struct_0(A) ) ). % 148.66/148.87 % 148.66/148.87 fof(dt_l1_struct_0,axiom, % 148.66/148.87 $true ). % 148.66/148.87 % 148.66/148.87 fof(dt_m1_subset_1,axiom, % 148.66/148.87 $true ). % 148.66/148.87 % 148.66/148.87 fof(dt_u1_struct_0,axiom, % 148.66/148.87 $true ). % 148.66/148.87 % 148.66/148.87 fof(existence_l1_pre_topc,axiom, % 148.66/148.87 ? [A] : l1_pre_topc(A) ). % 148.66/148.87 % 148.66/148.87 fof(existence_l1_struct_0,axiom, % 148.66/148.87 ? [A] : l1_struct_0(A) ). % 148.66/148.87 % 148.66/148.87 fof(existence_m1_subset_1,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ? [B] : m1_subset_1(B,A) ). % 148.66/148.87 % 148.66/148.87 fof(fc1_struct_0,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ( ~ v3_struct_0(A) % 148.66/148.87 & l1_struct_0(A) ) % 148.66/148.87 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 148.66/148.87 % 148.66/148.87 fof(fc1_subset_1,axiom, % 148.66/148.87 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 148.66/148.87 % 148.66/148.87 fof(fc6_membered,axiom, % 148.66/148.87 ( v1_xboole_0(k1_xboole_0) % 148.66/148.87 & v1_membered(k1_xboole_0) % 148.66/148.87 & v2_membered(k1_xboole_0) % 148.66/148.87 & v3_membered(k1_xboole_0) % 148.66/148.87 & v4_membered(k1_xboole_0) % 148.66/148.87 & v5_membered(k1_xboole_0) ) ). % 148.66/148.87 % 148.66/148.87 fof(rc1_membered,axiom, % 148.66/148.87 ? [A] : % 148.66/148.87 ( ~ v1_xboole_0(A) % 148.66/148.87 & v1_membered(A) % 148.66/148.87 & v2_membered(A) % 148.66/148.87 & v3_membered(A) % 148.66/148.87 & v4_membered(A) % 148.66/148.87 & v5_membered(A) ) ). % 148.66/148.87 % 148.66/148.87 fof(rc1_subset_1,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ~ v1_xboole_0(A) % 148.66/148.87 => ? [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(A)) % 148.66/148.87 & ~ v1_xboole_0(B) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(rc1_tops_1,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ( v2_pre_topc(A) % 148.66/148.87 & l1_pre_topc(A) ) % 148.66/148.87 => ? [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.87 & v3_pre_topc(B,A) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(rc2_subset_1,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ? [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(A)) % 148.66/148.87 & v1_xboole_0(B) ) ). % 148.66/148.87 % 148.66/148.87 fof(rc2_tops_1,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ( v2_pre_topc(A) % 148.66/148.87 & l1_pre_topc(A) ) % 148.66/148.87 => ? [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.87 & v3_pre_topc(B,A) % 148.66/148.87 & v4_pre_topc(B,A) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(rc3_struct_0,axiom, % 148.66/148.87 ? [A] : % 148.66/148.87 ( l1_struct_0(A) % 148.66/148.87 & ~ v3_struct_0(A) ) ). % 148.66/148.87 % 148.66/148.87 fof(rc3_tops_1,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ( ~ v3_struct_0(A) % 148.66/148.87 & v2_pre_topc(A) % 148.66/148.87 & l1_pre_topc(A) ) % 148.66/148.87 => ? [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.87 & ~ v1_xboole_0(B) % 148.66/148.87 & v3_pre_topc(B,A) % 148.66/148.87 & v4_pre_topc(B,A) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(rc4_tops_1,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( l1_pre_topc(A) % 148.66/148.87 => ? [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.87 & v1_xboole_0(B) % 148.66/148.87 & v1_membered(B) % 148.66/148.87 & v2_membered(B) % 148.66/148.87 & v3_membered(B) % 148.66/148.87 & v4_membered(B) % 148.66/148.87 & v5_membered(B) % 148.66/148.87 & v2_tops_1(B,A) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(rc5_struct_0,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ( ~ v3_struct_0(A) % 148.66/148.87 & l1_struct_0(A) ) % 148.66/148.87 => ? [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.87 & ~ v1_xboole_0(B) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(rc5_tops_1,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ( v2_pre_topc(A) % 148.66/148.87 & l1_pre_topc(A) ) % 148.66/148.87 => ? [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.87 & v1_xboole_0(B) % 148.66/148.87 & v3_pre_topc(B,A) % 148.66/148.87 & v4_pre_topc(B,A) % 148.66/148.87 & v1_membered(B) % 148.66/148.87 & v2_membered(B) % 148.66/148.87 & v3_membered(B) % 148.66/148.87 & v4_membered(B) % 148.66/148.87 & v5_membered(B) % 148.66/148.87 & v2_tops_1(B,A) % 148.66/148.87 & v3_tops_1(B,A) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(rc6_pre_topc,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ( v2_pre_topc(A) % 148.66/148.87 & l1_pre_topc(A) ) % 148.66/148.87 => ? [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.87 & v4_pre_topc(B,A) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(rc7_pre_topc,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ( ~ v3_struct_0(A) % 148.66/148.87 & v2_pre_topc(A) % 148.66/148.87 & l1_pre_topc(A) ) % 148.66/148.87 => ? [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.87 & ~ v1_xboole_0(B) % 148.66/148.87 & v4_pre_topc(B,A) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(reflexivity_r1_tarski,axiom, % 148.66/148.87 ! [A,B] : r1_tarski(A,A) ). % 148.66/148.87 % 148.66/148.87 fof(t1_subset,axiom, % 148.66/148.87 ! [A,B] : % 148.66/148.87 ( r2_hidden(A,B) % 148.66/148.87 => m1_subset_1(A,B) ) ). % 148.66/148.87 % 148.66/148.87 fof(t2_subset,axiom, % 148.66/148.87 ! [A,B] : % 148.66/148.87 ( m1_subset_1(A,B) % 148.66/148.87 => ( v1_xboole_0(B) % 148.66/148.87 | r2_hidden(A,B) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(t3_subset,axiom, % 148.66/148.87 ! [A,B] : % 148.66/148.87 ( m1_subset_1(A,k1_zfmisc_1(B)) % 148.66/148.87 <=> r1_tarski(A,B) ) ). % 148.66/148.87 % 148.66/148.87 fof(t4_subset,axiom, % 148.66/148.87 ! [A,B,C] : % 148.66/148.87 ( ( r2_hidden(A,B) % 148.66/148.87 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 148.66/148.87 => m1_subset_1(A,C) ) ). % 148.66/148.87 % 148.66/148.87 fof(t58_tex_4,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ( ~ v3_struct_0(A) % 148.66/148.87 & v2_pre_topc(A) % 148.66/148.87 & l1_pre_topc(A) ) % 148.66/148.87 => ! [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.87 => ( v3_pre_topc(B,A) % 148.66/148.87 => k3_tex_4(A,B) = B ) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(t5_subset,axiom, % 148.66/148.87 ! [A,B,C] : % 148.66/148.87 ~ ( r2_hidden(A,B) % 148.66/148.87 & m1_subset_1(B,k1_zfmisc_1(C)) % 148.66/148.87 & v1_xboole_0(C) ) ). % 148.66/148.87 % 148.66/148.87 fof(t5_tex_2,axiom, % 148.66/148.87 ! [A,B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(A)) % 148.66/148.87 => ( v1_tex_2(B,k1_zfmisc_1(A)) % 148.66/148.87 <=> B != A ) ) ). % 148.66/148.87 % 148.66/148.87 fof(t62_tex_4,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( ( ~ v3_struct_0(A) % 148.66/148.87 & v2_pre_topc(A) % 148.66/148.87 & l1_pre_topc(A) ) % 148.66/148.87 => ! [B] : % 148.66/148.87 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 148.66/148.87 => ( v4_pre_topc(B,A) % 148.66/148.87 => k3_tex_4(A,B) = B ) ) ) ). % 148.66/148.87 % 148.66/148.87 fof(t6_boole,axiom, % 148.66/148.87 ! [A] : % 148.66/148.87 ( v1_xboole_0(A) % 148.66/148.87 => A = k1_xboole_0 ) ). % 148.66/148.87 % 148.66/148.87 fof(t7_boole,axiom, % 148.66/148.87 ! [A,B] : % 148.66/148.87 ~ ( r2_hidden(A,B) % 148.66/148.87 & v1_xboole_0(B) ) ). % 148.66/148.87 % 148.66/148.87 fof(t8_boole,axiom, % 148.66/148.87 ! [A,B] : % 148.66/148.87 ~ ( v1_xboole_0(A) % 148.66/148.87 & A != B % 148.66/148.87 & v1_xboole_0(B) ) ). % 148.66/148.87 % 148.66/148.87 %------------------------------------------------------------------------------ % 148.66/148.87 %------------------------------------------- % 148.66/148.87 % Proof found % 148.66/148.87 % SZS status Theorem for theBenchmark % 148.66/148.87 % SZS output start Proof % 148.66/148.87 %ClaNum:191(EqnAxiom:53) % 148.66/148.87 %VarNum:500(SingletonVarNum:176) % 148.66/148.87 %MaxLitNum:7 % 148.66/148.87 %MaxfuncDepth:2 % 148.66/148.87 %SharedTerms:33 % 148.66/148.87 %goalClause: 54 55 71 74 75 77 100 % 148.66/148.87 %singleGoalClaCount:6 % 148.66/148.87 [54]P1(a1) % 148.66/148.87 [55]P2(a1) % 148.66/148.87 [56]P2(a10) % 148.66/148.87 [57]P3(a12) % 148.66/148.87 [58]P3(a13) % 148.66/148.87 [59]P9(a12) % 148.66/148.87 [60]P9(a13) % 148.66/148.87 [61]P17(a12) % 148.66/148.87 [62]P17(a13) % 148.66/148.87 [63]P19(a12) % 148.66/148.87 [64]P19(a13) % 148.66/148.87 [65]P23(a12) % 148.66/148.87 [66]P23(a13) % 148.66/148.87 [67]P10(a12) % 148.66/148.87 [68]P4(a14) % 148.66/148.87 [69]P4(a2) % 148.66/148.87 [71]P11(a11,a1) % 148.66/148.87 [77]~P20(a1) % 148.66/148.87 [78]~P20(a2) % 148.66/148.87 [79]~P10(a13) % 148.66/148.87 [74]P6(a11,f20(f19(a1))) % 148.66/148.87 [75]P12(a11,f20(f19(a1))) % 148.66/148.87 [72]P5(x721,x721) % 148.66/148.87 [70]P10(f16(x701)) % 148.66/148.87 [73]P6(f15(x731),x731) % 148.66/148.87 [76]P6(f16(x761),f20(x761)) % 148.66/148.87 [80]~P10(f20(x801)) % 148.66/148.87 [100]P21(a11,a1)+P24(a11,a1) % 148.66/148.87 [81]~P10(x811)+E(x811,a12) % 148.66/148.87 [82]~P9(x821)+P3(x821) % 148.66/148.87 [83]~P10(x831)+P3(x831) % 148.66/148.87 [84]~P17(x841)+P9(x841) % 148.66/148.87 [85]~P10(x851)+P9(x851) % 148.66/148.87 [86]~P19(x861)+P17(x861) % 148.66/148.87 [87]~P10(x871)+P17(x871) % 148.66/148.87 [88]~P23(x881)+P19(x881) % 148.66/148.87 [89]~P10(x891)+P19(x891) % 148.66/148.87 [90]~P10(x901)+P23(x901) % 148.66/148.87 [91]~P2(x911)+P4(x911) % 148.66/148.87 [93]~P2(x931)+P3(f4(x931)) % 148.66/148.87 [94]~P2(x941)+P9(f4(x941)) % 148.66/148.87 [95]~P2(x951)+P17(f4(x951)) % 148.66/148.87 [96]~P2(x961)+P19(f4(x961)) % 148.66/148.87 [97]~P2(x971)+P23(f4(x971)) % 148.66/148.87 [98]~P2(x981)+P10(f4(x981)) % 148.66/148.87 [99]P10(x991)+~P10(f17(x991)) % 148.66/148.87 [107]~P2(x1071)+P18(f4(x1071),x1071) % 148.66/148.87 [111]P10(x1111)+P6(f17(x1111),f20(x1111)) % 148.66/148.87 [159]~P2(x1591)+P6(f4(x1591),f20(f19(x1591))) % 148.66/148.87 [110]~P10(x1101)+~P7(x1102,x1101) % 148.66/148.87 [137]~P7(x1371,x1372)+P6(x1371,x1372) % 148.66/148.87 [158]~P7(x1582,x1581)+~P7(x1581,x1582) % 148.66/148.87 [142]~P5(x1421,x1422)+P6(x1421,f20(x1422)) % 148.66/148.87 [160]P5(x1601,x1602)+~P6(x1601,f20(x1602)) % 148.66/148.87 [101]~P1(x1011)+~P2(x1011)+P3(f6(x1011)) % 148.66/148.87 [102]~P1(x1021)+~P2(x1021)+P9(f6(x1021)) % 148.66/148.87 [103]~P1(x1031)+~P2(x1031)+P17(f6(x1031)) % 148.66/148.87 [104]~P1(x1041)+~P2(x1041)+P19(f6(x1041)) % 148.66/148.87 [105]~P1(x1051)+~P2(x1051)+P23(f6(x1051)) % 148.66/148.87 [106]~P1(x1061)+~P2(x1061)+P10(f6(x1061)) % 148.66/148.87 [108]~P4(x1081)+P20(x1081)+~P10(f19(x1081)) % 148.66/148.88 [109]~P4(x1091)+P20(x1091)+~P10(f7(x1091)) % 148.66/148.88 [127]~P1(x1271)+~P2(x1271)+P21(f18(x1271),x1271) % 148.66/148.88 [128]~P1(x1281)+~P2(x1281)+P21(f3(x1281),x1281) % 148.66/148.88 [129]~P1(x1291)+~P2(x1291)+P21(f6(x1291),x1291) % 148.66/148.88 [130]~P1(x1301)+~P2(x1301)+P24(f3(x1301),x1301) % 148.66/148.88 [131]~P1(x1311)+~P2(x1311)+P24(f6(x1311),x1311) % 148.66/148.88 [132]~P1(x1321)+~P2(x1321)+P24(f8(x1321),x1321) % 148.66/148.88 [133]~P1(x1331)+~P2(x1331)+P18(f6(x1331),x1331) % 148.66/148.88 [134]~P1(x1341)+~P2(x1341)+P22(f6(x1341),x1341) % 148.66/148.88 [161]~P4(x1611)+P20(x1611)+P6(f7(x1611),f20(f19(x1611))) % 148.66/148.88 [162]~P1(x1621)+~P2(x1621)+P6(f18(x1621),f20(f19(x1621))) % 148.66/148.88 [163]~P1(x1631)+~P2(x1631)+P6(f3(x1631),f20(f19(x1631))) % 148.66/148.88 [164]~P1(x1641)+~P2(x1641)+P6(f6(x1641),f20(f19(x1641))) % 148.66/148.88 [165]~P1(x1651)+~P2(x1651)+P6(f8(x1651),f20(f19(x1651))) % 148.66/148.88 [92]~P10(x922)+~P10(x921)+E(x921,x922) % 148.66/148.88 [112]~P6(x1121,x1122)+P15(x1121)+~P3(x1122) % 148.66/148.88 [113]~P6(x1131,x1132)+P15(x1131)+~P9(x1132) % 148.66/148.88 [114]~P6(x1141,x1142)+P15(x1141)+~P17(x1142) % 148.66/148.88 [115]~P6(x1151,x1152)+P15(x1151)+~P19(x1152) % 148.66/148.88 [116]~P6(x1161,x1162)+P15(x1161)+~P23(x1162) % 148.66/148.88 [117]~P6(x1171,x1172)+P16(x1171)+~P9(x1172) % 148.66/148.88 [118]~P6(x1181,x1182)+P16(x1181)+~P17(x1182) % 148.66/148.88 [119]~P6(x1191,x1192)+P16(x1191)+~P19(x1192) % 148.66/148.88 [120]~P6(x1201,x1202)+P16(x1201)+~P23(x1202) % 148.66/148.88 [121]~P6(x1211,x1212)+P13(x1211)+~P17(x1212) % 148.66/148.88 [122]~P6(x1221,x1222)+P13(x1221)+~P19(x1222) % 148.66/148.88 [123]~P6(x1231,x1232)+P13(x1231)+~P23(x1232) % 148.66/148.88 [124]~P6(x1241,x1242)+P8(x1241)+~P19(x1242) % 148.66/148.88 [125]~P6(x1251,x1252)+P8(x1251)+~P23(x1252) % 148.66/148.88 [126]~P6(x1261,x1262)+P25(x1261)+~P23(x1262) % 148.66/148.88 [141]~P6(x1412,x1411)+P10(x1411)+P7(x1412,x1411) % 148.66/148.88 [143]P3(x1431)+~P3(x1432)+~P6(x1431,f20(x1432)) % 148.66/148.88 [144]P3(x1441)+~P9(x1442)+~P6(x1441,f20(x1442)) % 148.66/148.88 [145]P3(x1451)+~P17(x1452)+~P6(x1451,f20(x1452)) % 148.66/148.88 [146]P3(x1461)+~P19(x1462)+~P6(x1461,f20(x1462)) % 148.66/148.88 [147]P3(x1471)+~P23(x1472)+~P6(x1471,f20(x1472)) % 148.66/148.88 [148]P9(x1481)+~P9(x1482)+~P6(x1481,f20(x1482)) % 148.66/148.88 [149]P9(x1491)+~P17(x1492)+~P6(x1491,f20(x1492)) % 148.66/148.88 [150]P9(x1501)+~P19(x1502)+~P6(x1501,f20(x1502)) % 148.66/148.88 [151]P9(x1511)+~P23(x1512)+~P6(x1511,f20(x1512)) % 148.66/148.88 [152]P17(x1521)+~P17(x1522)+~P6(x1521,f20(x1522)) % 148.66/148.88 [153]P17(x1531)+~P19(x1532)+~P6(x1531,f20(x1532)) % 148.66/148.88 [154]P17(x1541)+~P23(x1542)+~P6(x1541,f20(x1542)) % 148.66/148.88 [155]P19(x1551)+~P19(x1552)+~P6(x1551,f20(x1552)) % 148.66/148.88 [156]P19(x1561)+~P23(x1562)+~P6(x1561,f20(x1562)) % 148.66/148.88 [157]P23(x1571)+~P23(x1572)+~P6(x1571,f20(x1572)) % 148.66/148.88 [166]E(x1661,x1662)+P12(x1661,f20(x1662))+~P6(x1661,f20(x1662)) % 148.66/148.88 [170]~E(x1701,x1702)+~P6(x1701,f20(x1702))+~P12(x1701,f20(x1702)) % 148.66/148.88 [169]~P10(x1691)+~P7(x1692,x1693)+~P6(x1693,f20(x1691)) % 148.66/148.88 [171]P6(x1711,x1712)+~P7(x1711,x1713)+~P6(x1713,f20(x1712)) % 148.66/148.88 [135]~P1(x1351)+~P2(x1351)+P20(x1351)+~P10(f5(x1351)) % 148.66/148.88 [136]~P1(x1361)+~P2(x1361)+P20(x1361)+~P10(f9(x1361)) % 148.66/148.88 [138]~P1(x1381)+~P2(x1381)+P20(x1381)+P21(f5(x1381),x1381) % 148.66/148.88 [139]~P1(x1391)+~P2(x1391)+P20(x1391)+P24(f5(x1391),x1391) % 148.66/148.88 [140]~P1(x1401)+~P2(x1401)+P20(x1401)+P24(f9(x1401),x1401) % 148.66/148.88 [167]~P1(x1671)+~P2(x1671)+P20(x1671)+P6(f5(x1671),f20(f19(x1671))) % 148.66/148.88 [168]~P1(x1681)+~P2(x1681)+P20(x1681)+P6(f9(x1681),f20(f19(x1681))) % 148.66/148.88 [172]~P2(x1722)+~P10(x1721)+P18(x1721,x1722)+~P6(x1721,f20(f19(x1722))) % 148.66/148.88 [187]~P2(x1871)+P20(x1871)+~P6(x1872,f20(f19(x1871)))+P6(f21(x1871,x1872),f20(f19(x1871))) % 148.66/148.88 [173]~P1(x1732)+~P2(x1732)+~P10(x1731)+P21(x1731,x1732)+~P6(x1731,f20(f19(x1732))) % 148.66/148.88 [174]~P1(x1742)+~P2(x1742)+~P10(x1741)+P24(x1741,x1742)+~P6(x1741,f20(f19(x1742))) % 148.66/148.88 [175]~P1(x1752)+~P2(x1752)+~P10(x1751)+P22(x1751,x1752)+~P6(x1751,f20(f19(x1752))) % 148.66/148.88 [176]~P1(x1762)+~P2(x1762)+~P22(x1761,x1762)+P18(x1761,x1762)+~P6(x1761,f20(f19(x1762))) % 148.66/148.88 [177]~P1(x1771)+~P2(x1771)+~P11(x1772,x1771)+P20(x1771)+P14(x1772,x1771)+~P6(x1772,f20(f19(x1771))) % 148.66/148.88 [178]P20(x1781)+~P1(x1781)+~P2(x1781)+~P21(x1782,x1781)+E(f21(x1781,x1782),x1782)+~P6(x1782,f20(f19(x1781))) % 148.66/148.88 [179]P20(x1791)+~P1(x1791)+~P2(x1791)+~P24(x1792,x1791)+E(f21(x1791,x1792),x1792)+~P6(x1792,f20(f19(x1791))) % 148.66/148.88 [180]P20(x1801)+~P1(x1801)+~P2(x1801)+~P11(x1802,x1801)+E(f21(x1801,x1802),f19(x1801))+~P6(x1802,f20(f19(x1801))) % 148.66/148.88 [181]~P2(x1812)+~P21(x1811,x1812)+~P22(x1811,x1812)+P3(x1811)+~P1(x1812)+~P6(x1811,f20(f19(x1812))) % 148.66/148.88 [182]~P2(x1822)+~P21(x1821,x1822)+~P22(x1821,x1822)+P9(x1821)+~P1(x1822)+~P6(x1821,f20(f19(x1822))) % 148.66/148.88 [183]~P2(x1832)+~P21(x1831,x1832)+~P22(x1831,x1832)+P17(x1831)+~P1(x1832)+~P6(x1831,f20(f19(x1832))) % 148.66/148.88 [184]~P2(x1842)+~P21(x1841,x1842)+~P22(x1841,x1842)+P19(x1841)+~P1(x1842)+~P6(x1841,f20(f19(x1842))) % 148.66/148.88 [185]~P2(x1852)+~P21(x1851,x1852)+~P22(x1851,x1852)+P23(x1851)+~P1(x1852)+~P6(x1851,f20(f19(x1852))) % 148.66/148.88 [186]~P2(x1862)+~P21(x1861,x1862)+~P22(x1861,x1862)+P10(x1861)+~P1(x1862)+~P6(x1861,f20(f19(x1862))) % 148.66/148.88 [188]~P1(x1882)+~P2(x1882)+~P21(x1881,x1882)+~P22(x1881,x1882)+P24(x1881,x1882)+~P6(x1881,f20(f19(x1882))) % 148.66/148.88 [190]~P1(x1902)+~P2(x1902)+~P24(x1901,x1902)+~P18(x1901,x1902)+P22(x1901,x1902)+~P6(x1901,f20(f19(x1902))) % 148.66/148.88 [191]~P1(x1911)+~P2(x1911)+~P14(x1912,x1911)+P20(x1911)+P11(x1912,x1911)+~E(f21(x1911,x1912),f19(x1911))+~P6(x1912,f20(f19(x1911))) % 148.66/148.88 %EqnAxiom % 148.66/148.88 [1]E(x11,x11) % 148.66/148.88 [2]E(x22,x21)+~E(x21,x22) % 148.66/148.88 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 148.66/148.88 [4]~E(x41,x42)+E(f16(x41),f16(x42)) % 148.66/148.88 [5]~E(x51,x52)+E(f15(x51),f15(x52)) % 148.66/148.88 [6]~E(x61,x62)+E(f19(x61),f19(x62)) % 148.66/148.88 [7]~E(x71,x72)+E(f20(x71),f20(x72)) % 148.66/148.88 [8]~E(x81,x82)+E(f21(x81,x83),f21(x82,x83)) % 148.66/148.88 [9]~E(x91,x92)+E(f21(x93,x91),f21(x93,x92)) % 148.66/148.88 [10]~E(x101,x102)+E(f4(x101),f4(x102)) % 148.66/148.88 [11]~E(x111,x112)+E(f7(x111),f7(x112)) % 148.66/148.88 [12]~E(x121,x122)+E(f18(x121),f18(x122)) % 148.66/148.88 [13]~E(x131,x132)+E(f9(x131),f9(x132)) % 148.66/148.88 [14]~E(x141,x142)+E(f6(x141),f6(x142)) % 148.66/148.88 [15]~E(x151,x152)+E(f3(x151),f3(x152)) % 148.66/148.88 [16]~E(x161,x162)+E(f8(x161),f8(x162)) % 148.66/148.88 [17]~E(x171,x172)+E(f5(x171),f5(x172)) % 148.66/148.88 [18]~E(x181,x182)+E(f17(x181),f17(x182)) % 148.66/148.88 [19]~P1(x191)+P1(x192)+~E(x191,x192) % 148.66/148.88 [20]~P2(x201)+P2(x202)+~E(x201,x202) % 148.66/148.88 [21]P21(x212,x213)+~E(x211,x212)+~P21(x211,x213) % 148.66/148.88 [22]P21(x223,x222)+~E(x221,x222)+~P21(x223,x221) % 148.66/148.88 [23]~P3(x231)+P3(x232)+~E(x231,x232) % 148.66/148.88 [24]P12(x242,x243)+~E(x241,x242)+~P12(x241,x243) % 148.66/148.88 [25]P12(x253,x252)+~E(x251,x252)+~P12(x253,x251) % 148.66/148.88 [26]~P9(x261)+P9(x262)+~E(x261,x262) % 148.66/148.88 [27]P6(x272,x273)+~E(x271,x272)+~P6(x271,x273) % 148.66/148.88 [28]P6(x283,x282)+~E(x281,x282)+~P6(x283,x281) % 148.66/148.88 [29]~P17(x291)+P17(x292)+~E(x291,x292) % 148.66/148.88 [30]~P20(x301)+P20(x302)+~E(x301,x302) % 148.66/148.88 [31]~P19(x311)+P19(x312)+~E(x311,x312) % 148.66/148.88 [32]~P25(x321)+P25(x322)+~E(x321,x322) % 148.66/148.88 [33]~P23(x331)+P23(x332)+~E(x331,x332) % 148.66/148.88 [34]~P16(x341)+P16(x342)+~E(x341,x342) % 148.66/148.88 [35]~P10(x351)+P10(x352)+~E(x351,x352) % 148.66/148.88 [36]~P4(x361)+P4(x362)+~E(x361,x362) % 148.66/148.88 [37]P11(x372,x373)+~E(x371,x372)+~P11(x371,x373) % 148.66/148.88 [38]P11(x383,x382)+~E(x381,x382)+~P11(x383,x381) % 148.66/148.88 [39]P18(x392,x393)+~E(x391,x392)+~P18(x391,x393) % 148.66/148.88 [40]P18(x403,x402)+~E(x401,x402)+~P18(x403,x401) % 148.66/148.88 [41]P22(x412,x413)+~E(x411,x412)+~P22(x411,x413) % 148.66/148.88 [42]P22(x423,x422)+~E(x421,x422)+~P22(x423,x421) % 148.66/148.88 [43]P5(x432,x433)+~E(x431,x432)+~P5(x431,x433) % 148.66/148.88 [44]P5(x443,x442)+~E(x441,x442)+~P5(x443,x441) % 148.66/148.88 [45]P24(x452,x453)+~E(x451,x452)+~P24(x451,x453) % 148.66/148.88 [46]P24(x463,x462)+~E(x461,x462)+~P24(x463,x461) % 148.66/148.88 [47]~P8(x471)+P8(x472)+~E(x471,x472) % 148.66/148.88 [48]P7(x482,x483)+~E(x481,x482)+~P7(x481,x483) % 148.66/148.88 [49]P7(x493,x492)+~E(x491,x492)+~P7(x493,x491) % 148.66/148.88 [50]~P13(x501)+P13(x502)+~E(x501,x502) % 148.66/148.88 [51]~P15(x511)+P15(x512)+~E(x511,x512) % 148.66/148.88 [52]P14(x522,x523)+~E(x521,x522)+~P14(x521,x523) % 148.66/148.88 [53]P14(x533,x532)+~E(x531,x532)+~P14(x533,x531) % 148.66/148.88 % 148.66/148.88 %------------------------------------------- % 148.66/148.90 cnf(192,plain, % 148.66/148.90 (~P6(x1921,f20(x1921))+~P12(x1921,f20(x1921))), % 148.66/148.90 inference(equality_inference,[],[170])). % 148.66/148.90 cnf(193,plain, % 148.66/148.90 (P5(a11,f19(a1))), % 148.66/148.90 inference(scs_inference,[],[74,160])). % 148.66/148.90 cnf(195,plain, % 148.66/148.90 (~P7(x1951,a12)), % 148.66/148.90 inference(scs_inference,[],[74,67,160,110])). % 148.66/148.90 cnf(197,plain, % 148.66/148.90 (P7(f15(a13),a13)), % 148.66/148.90 inference(scs_inference,[],[74,73,67,79,160,110,141])). % 148.66/148.90 cnf(198,plain, % 148.66/148.90 (P6(f15(x1981),x1981)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(201,plain, % 148.66/148.90 (P6(f15(x2011),x2011)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(203,plain, % 148.66/148.90 (P3(f16(a12))), % 148.66/148.90 inference(scs_inference,[],[74,73,198,76,67,57,59,79,160,110,141,143,144])). % 148.66/148.90 cnf(204,plain, % 148.66/148.90 (P6(f16(x2041),f20(x2041))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(207,plain, % 148.66/148.90 (P6(f15(x2071),x2071)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(209,plain, % 148.66/148.90 (P9(f16(a12))), % 148.66/148.90 inference(scs_inference,[],[74,73,198,201,76,204,67,57,59,61,79,160,110,141,143,144,148,149])). % 148.66/148.90 cnf(210,plain, % 148.66/148.90 (P6(f16(x2101),f20(x2101))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(213,plain, % 148.66/148.90 (P6(f15(x2131),x2131)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(216,plain, % 148.66/148.90 (P6(f16(x2161),f20(x2161))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(219,plain, % 148.66/148.90 (P6(f15(x2191),x2191)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(222,plain, % 148.66/148.90 (P6(f16(x2221),f20(x2221))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(225,plain, % 148.66/148.90 (P6(f15(x2251),x2251)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(227,plain, % 148.66/148.90 (~P7(x2271,f15(f20(a12)))), % 148.66/148.90 inference(scs_inference,[],[74,73,198,201,207,213,219,225,76,204,210,216,67,57,59,61,63,65,79,160,110,141,143,144,148,149,152,153,155,156,157,169])). % 148.66/148.90 cnf(228,plain, % 148.66/148.90 (P6(f15(x2281),x2281)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(230,plain, % 148.66/148.90 (~E(a11,f19(a1))), % 148.66/148.90 inference(scs_inference,[],[74,75,73,198,201,207,213,219,225,76,204,210,216,67,57,59,61,63,65,79,160,110,141,143,144,148,149,152,153,155,156,157,169,170])). % 148.66/148.90 cnf(232,plain, % 148.66/148.90 (~E(a13,a12)), % 148.66/148.90 inference(scs_inference,[],[74,75,73,198,201,207,213,219,225,76,204,210,216,67,57,59,61,63,65,79,160,110,141,143,144,148,149,152,153,155,156,157,169,170,49])). % 148.66/148.90 cnf(233,plain, % 148.66/148.90 (P18(f16(f19(a1)),a1)), % 148.66/148.90 inference(scs_inference,[],[55,74,75,73,198,201,207,213,219,225,76,204,210,216,222,67,70,57,59,61,63,65,79,160,110,141,143,144,148,149,152,153,155,156,157,169,170,49,172])). % 148.66/148.90 cnf(234,plain, % 148.66/148.90 (P6(f16(x2341),f20(x2341))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(235,plain, % 148.66/148.90 (P10(f16(x2351))), % 148.66/148.90 inference(rename_variables,[],[70])). % 148.66/148.90 cnf(237,plain, % 148.66/148.90 (P21(f16(f19(a1)),a1)), % 148.66/148.90 inference(scs_inference,[],[54,55,74,75,73,198,201,207,213,219,225,76,204,210,216,222,234,67,70,235,57,59,61,63,65,79,160,110,141,143,144,148,149,152,153,155,156,157,169,170,49,172,173])). % 148.66/148.90 cnf(238,plain, % 148.66/148.90 (P6(f16(x2381),f20(x2381))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(239,plain, % 148.66/148.90 (P10(f16(x2391))), % 148.66/148.90 inference(rename_variables,[],[70])). % 148.66/148.90 cnf(241,plain, % 148.66/148.90 (P24(f16(f19(a1)),a1)), % 148.66/148.90 inference(scs_inference,[],[54,55,74,75,73,198,201,207,213,219,225,76,204,210,216,222,234,238,67,70,235,239,57,59,61,63,65,79,160,110,141,143,144,148,149,152,153,155,156,157,169,170,49,172,173,174])). % 148.66/148.90 cnf(242,plain, % 148.66/148.90 (P6(f16(x2421),f20(x2421))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(243,plain, % 148.66/148.90 (P10(f16(x2431))), % 148.66/148.90 inference(rename_variables,[],[70])). % 148.66/148.90 cnf(245,plain, % 148.66/148.90 (P22(f16(f19(a1)),a1)), % 148.66/148.90 inference(scs_inference,[],[54,55,74,75,73,198,201,207,213,219,225,76,204,210,216,222,234,238,242,67,70,235,239,243,57,59,61,63,65,79,160,110,141,143,144,148,149,152,153,155,156,157,169,170,49,172,173,174,175])). % 148.66/148.90 cnf(246,plain, % 148.66/148.90 (P6(f16(x2461),f20(x2461))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(251,plain, % 148.66/148.90 (E(f21(a1,a11),f19(a1))), % 148.66/148.90 inference(scs_inference,[],[54,55,71,77,74,75,73,198,201,207,213,219,225,76,204,210,216,222,234,238,242,67,70,235,239,243,57,59,61,63,65,79,160,110,141,143,144,148,149,152,153,155,156,157,169,170,49,172,173,174,175,177,180])). % 148.66/148.90 cnf(254,plain, % 148.66/148.90 (P6(f16(x2541),f20(x2541))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(257,plain, % 148.66/148.90 (P6(f16(x2571),f20(x2571))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(260,plain, % 148.66/148.90 (P6(f16(x2601),f20(x2601))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(263,plain, % 148.66/148.90 (P6(f16(x2631),f20(x2631))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(270,plain, % 148.66/148.90 (E(f19(a1),f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[54,55,71,77,74,75,73,198,201,207,213,219,225,76,204,210,216,222,234,238,242,246,254,257,260,263,67,70,235,239,243,57,59,61,63,65,79,160,110,141,143,144,148,149,152,153,155,156,157,169,170,49,172,173,174,175,177,180,181,182,183,184,185,158,2])). % 148.66/148.90 cnf(273,plain, % 148.66/148.90 (P6(f15(f21(a1,a11)),f19(a1))), % 148.66/148.90 inference(scs_inference,[],[54,55,71,77,74,75,73,198,201,207,213,219,225,228,76,204,210,216,222,234,238,242,246,254,257,260,263,67,70,235,239,243,57,59,61,63,65,79,160,110,141,143,144,148,149,152,153,155,156,157,169,170,49,172,173,174,175,177,180,181,182,183,184,185,158,2,145,28])). % 148.66/148.90 cnf(275,plain, % 148.66/148.90 (~E(a11,f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[54,55,71,77,74,75,73,198,201,207,213,219,225,228,76,204,210,216,222,234,238,242,246,254,257,260,263,67,70,235,239,243,57,59,61,63,65,79,160,110,141,143,144,148,149,152,153,155,156,157,169,170,49,172,173,174,175,177,180,181,182,183,184,185,158,2,145,28,3])). % 148.66/148.90 cnf(276,plain, % 148.66/148.90 (P5(f19(a1),f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[54,55,71,77,74,75,73,198,201,207,213,219,225,228,76,204,210,216,222,234,238,242,246,254,257,260,263,67,70,235,239,243,72,57,59,61,63,65,79,160,110,141,143,144,148,149,152,153,155,156,157,169,170,49,172,173,174,175,177,180,181,182,183,184,185,158,2,145,28,3,43])). % 148.66/148.90 cnf(290,plain, % 148.66/148.90 (P5(f15(f20(x2901)),x2901)), % 148.66/148.90 inference(scs_inference,[],[73,160])). % 148.66/148.90 cnf(295,plain, % 148.66/148.90 (P7(a11,f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[74,73,70,80,160,110,141])). % 148.66/148.90 cnf(300,plain, % 148.66/148.90 (P5(a11,f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[74,227,193,197,73,70,270,80,160,110,141,49,44])). % 148.66/148.90 cnf(301,plain, % 148.66/148.90 (~P7(f20(f19(a1)),a11)), % 148.66/148.90 inference(scs_inference,[],[74,227,193,197,73,70,270,80,160,110,141,49,44,158])). % 148.66/148.90 cnf(303,plain, % 148.66/148.90 (P6(x3031,f19(a1))+~P7(x3031,a11)), % 148.66/148.90 inference(scs_inference,[],[74,227,193,197,73,70,270,80,160,110,141,49,44,158,171])). % 148.66/148.90 cnf(309,plain, % 148.66/148.90 (P5(f16(x3091),x3091)), % 148.66/148.90 inference(scs_inference,[],[76,160])). % 148.66/148.90 cnf(314,plain, % 148.66/148.90 (P12(a11,x3141)+~E(f20(f19(a1)),x3141)), % 148.66/148.90 inference(scs_inference,[],[75,251,295,227,76,160,49,44,25])). % 148.66/148.90 cnf(316,plain, % 148.66/148.90 (P11(x3161,a1)+~E(a11,x3161)), % 148.66/148.90 inference(scs_inference,[],[71,75,251,295,227,76,160,49,44,25,30,37])). % 148.66/148.90 cnf(318,plain, % 148.66/148.90 (P24(x3181,a1)+~E(f16(f19(a1)),x3181)), % 148.66/148.90 inference(scs_inference,[],[71,75,251,241,295,227,76,160,49,44,25,30,37,38,45])). % 148.66/148.90 cnf(325,plain, % 148.66/148.90 (~P3(f21(a1,a11))+P3(f19(a1))), % 148.66/148.90 inference(scs_inference,[],[251,23])). % 148.66/148.90 cnf(330,plain, % 148.66/148.90 (~P17(f21(a1,a11))+P3(f19(a1))), % 148.66/148.90 inference(scs_inference,[],[251,23,82,83,84])). % 148.66/148.90 cnf(332,plain, % 148.66/148.90 (~P19(f21(a1,a11))+P3(f19(a1))), % 148.66/148.90 inference(scs_inference,[],[251,23,82,83,84,86])). % 148.66/148.90 cnf(334,plain, % 148.66/148.90 (~P23(f21(a1,a11))+P3(f19(a1))), % 148.66/148.90 inference(scs_inference,[],[251,23,82,83,84,86,88])). % 148.66/148.90 cnf(337,plain, % 148.66/148.90 (P18(x3371,a1)+~E(f16(f19(a1)),x3371)), % 148.66/148.90 inference(scs_inference,[],[233,39])). % 148.66/148.90 cnf(339,plain, % 148.66/148.90 (P22(x3391,a1)+~E(f16(f19(a1)),x3391)), % 148.66/148.90 inference(scs_inference,[],[233,245,39,40,41])). % 148.66/148.90 cnf(381,plain, % 148.66/148.90 (~P10(f21(a1,a11))+P10(f19(a1))), % 148.66/148.90 inference(scs_inference,[],[74,251,148,155,143,20,35])). % 148.66/148.90 cnf(382,plain, % 148.66/148.90 (P21(x3821,a1)+~E(f16(f19(a1)),x3821)), % 148.66/148.90 inference(scs_inference,[],[74,251,237,148,155,143,20,35,21])). % 148.66/148.90 cnf(389,plain, % 148.66/148.90 (P7(f15(f21(a1,a11)),f19(a1))+~E(a11,a13)), % 148.66/148.90 inference(scs_inference,[],[74,197,273,27,169,171,141])). % 148.66/148.90 cnf(433,plain, % 148.66/148.90 (P6(f16(x4331),f20(x4331))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(438,plain, % 148.66/148.90 (P5(x4381,x4382)+~E(f16(x4382),x4381)), % 148.66/148.90 inference(scs_inference,[],[309,209,76,433,148,144,43])). % 148.66/148.90 cnf(439,plain, % 148.66/148.90 (P5(x4391,f19(a1))+~E(f16(f21(a1,a11)),x4391)), % 148.66/148.90 inference(scs_inference,[],[251,309,209,76,433,148,144,43,44])). % 148.66/148.90 cnf(454,plain, % 148.66/148.90 (~P9(f21(a1,a11))+P9(f19(a1))), % 148.66/148.90 inference(scs_inference,[],[74,251,273,237,76,73,169,171,27,170,22,26])). % 148.66/148.90 cnf(531,plain, % 148.66/148.90 (P7(f15(f21(a1,a11)),f19(a1))+P3(f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[273,270,23,325,330,332,334,82,83,84,86,88,141])). % 148.66/148.90 cnf(534,plain, % 148.66/148.90 (P6(x5341,f20(x5342))+~E(f16(x5342),x5341)), % 148.66/148.90 inference(scs_inference,[],[76,27])). % 148.66/148.90 cnf(550,plain, % 148.66/148.90 (P7(f15(f21(a1,a11)),f19(a1))+P9(f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[273,270,26,85,454,84,86,88,141])). % 148.66/148.90 cnf(565,plain, % 148.66/148.90 (P6(x5651,x5652)+~E(f15(x5652),x5651)), % 148.66/148.90 inference(scs_inference,[],[197,290,73,270,43,48,19,27])). % 148.66/148.90 cnf(579,plain, % 148.66/148.90 (E(f4(a1),a12)), % 148.66/148.90 inference(scs_inference,[],[55,81,98])). % 148.66/148.90 cnf(580,plain, % 148.66/148.90 (E(a12,f4(a1))), % 148.66/148.90 inference(scs_inference,[],[579,2])). % 148.66/148.90 cnf(581,plain, % 148.66/148.90 (~E(a13,f4(a1))), % 148.66/148.90 inference(scs_inference,[],[579,232,2,3])). % 148.66/148.90 cnf(583,plain, % 148.66/148.90 (P23(f4(a1))), % 148.66/148.90 inference(scs_inference,[],[579,232,57,65,2,3,23,33])). % 148.66/148.90 cnf(585,plain, % 148.66/148.90 (P10(f4(a1))), % 148.66/148.90 inference(scs_inference,[],[67,579,232,57,59,65,2,3,23,33,26,35])). % 148.66/148.90 cnf(586,plain, % 148.66/148.90 (P19(f4(a1))), % 148.66/148.90 inference(scs_inference,[],[67,579,232,57,59,63,65,2,3,23,33,26,35,31])). % 148.66/148.90 cnf(587,plain, % 148.66/148.90 (P17(f4(a1))), % 148.66/148.90 inference(scs_inference,[],[67,579,232,57,59,61,63,65,2,3,23,33,26,35,31,29])). % 148.66/148.90 cnf(647,plain, % 148.66/148.90 (P10(f21(a1,a11))+~P10(f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[270,35,381])). % 148.66/148.90 cnf(648,plain, % 148.66/148.90 (P7(f15(f21(a1,a11)),f19(a1))+P10(f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[273,270,35,381,141])). % 148.66/148.90 cnf(681,plain, % 148.66/148.90 (E(f19(a1),a11)+~P10(a11)), % 148.66/148.90 inference(scs_inference,[],[54,74,77,55,270,275,173,178,2,3])). % 148.66/148.90 cnf(693,plain, % 148.66/148.90 (E(f19(a1),a11)+~P24(a11,a1)), % 148.66/148.90 inference(scs_inference,[],[54,74,77,55,270,275,179,2,3])). % 148.66/148.90 cnf(2667,plain, % 148.66/148.90 (P18(x26671,a10)+~E(f16(f19(a10)),x26671)), % 148.66/148.90 inference(scs_inference,[],[56,76,70,172,40,39])). % 148.66/148.90 cnf(3112,plain, % 148.66/148.90 (P6(f21(a1,a11),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[295,77,55,137,187])). % 148.66/148.90 cnf(3115,plain, % 148.66/148.90 (P6(f19(a1),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[251,3112,170,27])). % 148.66/148.90 cnf(3149,plain, % 148.66/148.90 (~E(f20(f19(a1)),f20(a12))+P10(f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[3115,67,61,63,28,169,150,155,152,389,531,550,648])). % 148.66/148.90 cnf(3503,plain, % 148.66/148.90 (P3(f15(f20(a13)))), % 148.66/148.90 inference(scs_inference,[],[58,73,143])). % 148.66/148.90 cnf(3710,plain, % 148.66/148.90 (~P10(a11)), % 148.66/148.90 inference(scs_inference,[],[230,681,2])). % 148.66/148.90 cnf(3712,plain, % 148.66/148.90 (~P6(f20(f19(a1)),a11)), % 148.66/148.90 inference(scs_inference,[],[3710,301,141])). % 148.66/148.90 cnf(3714,plain, % 148.66/148.90 (~E(f15(a11),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[3710,73,301,141,27])). % 148.66/148.90 cnf(4431,plain, % 148.66/148.90 (P17(f16(a13))), % 148.66/148.90 inference(scs_inference,[],[62,76,152])). % 148.66/148.90 cnf(4962,plain, % 148.66/148.90 (P19(f15(f20(a13)))), % 148.66/148.90 inference(scs_inference,[],[64,73,155])). % 148.66/148.90 cnf(4966,plain, % 148.66/148.90 (P19(f16(a13))), % 148.66/148.90 inference(scs_inference,[],[64,76,155])). % 148.66/148.90 cnf(5016,plain, % 148.66/148.90 (P6(f16(f21(a1,a11)),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[309,251,142,44])). % 148.66/148.90 cnf(5018,plain, % 148.66/148.90 (P10(f16(x50181))), % 148.66/148.90 inference(rename_variables,[],[70])). % 148.66/148.90 cnf(5021,plain, % 148.66/148.90 (P10(f16(x50211))), % 148.66/148.90 inference(rename_variables,[],[70])). % 148.66/148.90 cnf(5023,plain, % 148.66/148.90 (P21(f16(f21(a1,a11)),a1)), % 148.66/148.90 inference(scs_inference,[],[54,55,70,5018,5021,5016,172,174,173])). % 148.66/148.90 cnf(5069,plain, % 148.66/148.90 (P6(x50691,f20(f19(a1)))+~E(f16(f21(a1,a11)),x50691)), % 148.66/148.90 inference(scs_inference,[],[5023,5016,22,27])). % 148.66/148.90 cnf(5157,plain, % 148.66/148.90 (P23(f16(a12))), % 148.66/148.90 inference(scs_inference,[],[65,76,157])). % 148.66/148.90 cnf(5281,plain, % 148.66/148.90 (P23(f16(a13))), % 148.66/148.90 inference(scs_inference,[],[66,76,157])). % 148.66/148.90 cnf(5780,plain, % 148.66/148.90 (P21(a11,a1)+E(f19(a1),a11)), % 148.66/148.90 inference(scs_inference,[],[693,100])). % 148.66/148.90 cnf(6004,plain, % 148.66/148.90 (P7(f15(f20(x60041)),f20(x60041))), % 148.66/148.90 inference(scs_inference,[],[73,80,141])). % 148.66/148.90 cnf(6009,plain, % 148.66/148.90 (~E(f20(x60091),f15(f20(a12)))), % 148.66/148.90 inference(scs_inference,[],[73,227,80,141,158,49])). % 148.66/148.90 cnf(6011,plain, % 148.66/148.90 (P7(x60111,f20(x60112))+~E(f15(f20(x60112)),x60111)), % 148.66/148.90 inference(scs_inference,[],[73,227,80,141,158,49,48])). % 148.66/148.90 cnf(6283,plain, % 148.66/148.90 (E(f19(a1),a11)+E(f21(a1,a11),a11)), % 148.66/148.90 inference(scs_inference,[],[74,54,55,77,5780,178])). % 148.66/148.90 cnf(6465,plain, % 148.66/148.90 (E(f16(f19(a1)),f16(f21(a1,a11)))), % 148.66/148.90 inference(scs_inference,[],[251,4,2])). % 148.66/148.90 cnf(6466,plain, % 148.66/148.90 (E(f16(f21(a1,a11)),f16(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[6465,2])). % 148.66/148.90 cnf(6468,plain, % 148.66/148.90 (P5(f16(f19(a1)),f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[6465,2,534,438])). % 148.66/148.90 cnf(6557,plain, % 148.66/148.90 (E(f15(f19(f21(a1,a11))),f15(f19(f19(a1))))), % 148.66/148.90 inference(scs_inference,[],[251,5,6])). % 148.66/148.90 cnf(6622,plain, % 148.66/148.90 (P7(f16(x66221),f20(x66221))), % 148.66/148.90 inference(scs_inference,[],[76,80,141])). % 148.66/148.90 cnf(6625,plain, % 148.66/148.90 (P7(f16(f21(a1,a11)),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[76,6465,80,141,48])). % 148.66/148.90 cnf(7686,plain, % 148.66/148.90 (P7(x76861,f20(x76862))+~E(f16(x76862),x76861)), % 148.66/148.90 inference(scs_inference,[],[6622,48])). % 148.66/148.90 cnf(7692,plain, % 148.66/148.90 (P6(f16(x76921),f20(x76921))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(7695,plain, % 148.66/148.90 (P6(f16(x76951),f20(x76951))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(7698,plain, % 148.66/148.90 (P6(f16(x76981),f20(x76981))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(7701,plain, % 148.66/148.90 (P6(f16(x77011),f20(x77011))), % 148.66/148.90 inference(rename_variables,[],[76])). % 148.66/148.90 cnf(7706,plain, % 148.66/148.90 (P5(x77061,f21(a1,a11))+~E(f16(f19(a1)),x77061)), % 148.66/148.90 inference(scs_inference,[],[4966,5281,76,7692,7695,7698,7701,6468,155,150,154,146,157,43])). % 148.66/148.90 cnf(7727,plain, % 148.66/148.90 (P9(f4(a10))), % 148.66/148.90 inference(scs_inference,[],[56,93,94])). % 148.66/148.90 cnf(7731,plain, % 148.66/148.90 (P19(f4(a10))), % 148.66/148.90 inference(scs_inference,[],[56,93,94,95,96])). % 148.66/148.90 cnf(7733,plain, % 148.66/148.90 (P23(f4(a10))), % 148.66/148.90 inference(scs_inference,[],[56,93,94,95,96,97])). % 148.66/148.90 cnf(7735,plain, % 148.66/148.90 (P10(f4(a10))), % 148.66/148.90 inference(scs_inference,[],[56,93,94,95,96,97,98])). % 148.66/148.90 cnf(7737,plain, % 148.66/148.90 (~P10(f17(a13))), % 148.66/148.90 inference(scs_inference,[],[79,56,93,94,95,96,97,98,99])). % 148.66/148.90 cnf(7741,plain, % 148.66/148.90 (P6(f19(a1),f20(f21(a1,a11)))), % 148.66/148.90 inference(scs_inference,[],[276,79,56,93,94,95,96,97,98,99,107,142])). % 148.66/148.90 cnf(7743,plain, % 148.66/148.90 (P6(f17(a13),f20(a13))), % 148.66/148.90 inference(scs_inference,[],[276,79,56,93,94,95,96,97,98,99,107,142,111])). % 148.66/148.90 cnf(7746,plain, % 148.66/148.90 (E(f15(a12),f15(f4(a1)))), % 148.66/148.90 inference(scs_inference,[],[276,79,580,56,93,94,95,96,97,98,99,107,142,111,4,5])). % 148.66/148.90 cnf(7748,plain, % 148.66/148.90 (E(f20(a12),f20(f4(a1)))), % 148.66/148.90 inference(scs_inference,[],[276,79,580,56,93,94,95,96,97,98,99,107,142,111,4,5,6,7])). % 148.66/148.90 cnf(7758,plain, % 148.66/148.90 (P6(f4(a10),f20(f19(a10)))), % 148.66/148.90 inference(scs_inference,[],[276,79,580,56,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159])). % 148.66/148.90 cnf(7760,plain, % 148.66/148.90 (E(f21(a12,x77601),f21(f4(a1),x77601))), % 148.66/148.90 inference(scs_inference,[],[276,79,580,56,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8])). % 148.66/148.90 cnf(7761,plain, % 148.66/148.90 (E(f21(x77611,a12),f21(x77611,f4(a1)))), % 148.66/148.90 inference(scs_inference,[],[276,79,580,56,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9])). % 148.66/148.90 cnf(7762,plain, % 148.66/148.90 (E(f16(x77621),a12)), % 148.66/148.90 inference(scs_inference,[],[276,79,580,70,56,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81])). % 148.66/148.90 cnf(7764,plain, % 148.66/148.90 (P23(f16(x77641))), % 148.66/148.90 inference(scs_inference,[],[276,79,580,70,56,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90])). % 148.66/148.90 cnf(7766,plain, % 148.66/148.90 (P9(f16(x77661))), % 148.66/148.90 inference(scs_inference,[],[276,79,580,70,56,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85])). % 148.66/148.90 cnf(7770,plain, % 148.66/148.90 (P19(f16(x77701))), % 148.66/148.90 inference(scs_inference,[],[276,79,580,70,56,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89])). % 148.66/148.90 cnf(7777,plain, % 148.66/148.90 (P3(f6(a1))), % 148.66/148.90 inference(scs_inference,[],[54,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101])). % 148.66/148.90 cnf(7783,plain, % 148.66/148.90 (P19(f6(a1))), % 148.66/148.90 inference(scs_inference,[],[54,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104])). % 148.66/148.90 cnf(7785,plain, % 148.66/148.90 (P23(f6(a1))), % 148.66/148.90 inference(scs_inference,[],[54,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105])). % 148.66/148.90 cnf(7787,plain, % 148.66/148.90 (P10(f6(a1))), % 148.66/148.90 inference(scs_inference,[],[54,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106])). % 148.66/148.90 cnf(7789,plain, % 148.66/148.90 (~P10(f19(a2))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108])). % 148.66/148.90 cnf(7791,plain, % 148.66/148.90 (~P10(f7(a2))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109])). % 148.66/148.90 cnf(7793,plain, % 148.66/148.90 (P21(f18(a1),a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127])). % 148.66/148.90 cnf(7795,plain, % 148.66/148.90 (P21(f3(a1),a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128])). % 148.66/148.90 cnf(7799,plain, % 148.66/148.90 (P24(f3(a1),a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130])). % 148.66/148.90 cnf(7801,plain, % 148.66/148.90 (P24(f6(a1),a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131])). % 148.66/148.90 cnf(7803,plain, % 148.66/148.90 (P24(f8(a1),a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132])). % 148.66/148.90 cnf(7805,plain, % 148.66/148.90 (P18(f6(a1),a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133])). % 148.66/148.90 cnf(7809,plain, % 148.66/148.90 (P6(f7(a2),f20(f19(a2)))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161])). % 148.66/148.90 cnf(7811,plain, % 148.66/148.90 (P6(f18(a1),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162])). % 148.66/148.90 cnf(7813,plain, % 148.66/148.90 (P6(f3(a1),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163])). % 148.66/148.90 cnf(7815,plain, % 148.66/148.90 (P6(f6(a1),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164])). % 148.66/148.90 cnf(7817,plain, % 148.66/148.90 (P6(f8(a1),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,3714,276,79,580,70,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165])). % 148.66/148.90 cnf(7820,plain, % 148.66/148.90 (P6(f15(x78201),x78201)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7823,plain, % 148.66/148.90 (P6(f15(x78231),x78231)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7826,plain, % 148.66/148.90 (P6(f15(x78261),x78261)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7829,plain, % 148.66/148.90 (P6(f15(x78291),x78291)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7832,plain, % 148.66/148.90 (P6(f15(x78321),x78321)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7835,plain, % 148.66/148.90 (P6(f15(x78351),x78351)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7838,plain, % 148.66/148.90 (P6(f15(x78381),x78381)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7841,plain, % 148.66/148.90 (P6(f15(x78411),x78411)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7844,plain, % 148.66/148.90 (P5(x78441,x78441)), % 148.66/148.90 inference(rename_variables,[],[72])). % 148.66/148.90 cnf(7846,plain, % 148.66/148.90 (P6(f15(x78461),x78461)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7850,plain, % 148.66/148.90 (~E(f4(a1),a13)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,6466,580,70,73,7820,7823,7826,7829,7832,7835,7838,7841,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35])). % 148.66/148.90 cnf(7851,plain, % 148.66/148.90 (P10(f15(f20(a12)))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,227,6466,580,70,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141])). % 148.66/148.90 cnf(7853,plain, % 148.66/148.90 (P6(f15(x78531),x78531)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7855,plain, % 148.66/148.90 (~E(a12,a13)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,227,6466,580,579,70,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3])). % 148.66/148.90 cnf(7856,plain, % 148.66/148.90 (~P10(f5(a1))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135])). % 148.66/148.90 cnf(7858,plain, % 148.66/148.90 (~P10(f9(a1))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136])). % 148.66/148.90 cnf(7860,plain, % 148.66/148.90 (P21(f5(a1),a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138])). % 148.66/148.90 cnf(7862,plain, % 148.66/148.90 (P24(f5(a1),a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139])). % 148.66/148.90 cnf(7864,plain, % 148.66/148.90 (P24(f9(a1),a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140])). % 148.66/148.90 cnf(7866,plain, % 148.66/148.90 (P6(f5(a1),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140,167])). % 148.66/148.90 cnf(7868,plain, % 148.66/148.90 (P6(f9(a1),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140,167,168])). % 148.66/148.90 cnf(7870,plain, % 148.66/148.90 (~P22(f5(a1),a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140,167,168,186])). % 148.66/148.90 cnf(7873,plain, % 148.66/148.90 (P18(a12,a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140,167,168,186,318,337])). % 148.66/148.90 cnf(7874,plain, % 148.66/148.90 (P22(a12,a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140,167,168,186,318,337,339])). % 148.66/148.90 cnf(7875,plain, % 148.66/148.90 (P21(a12,a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,585,276,79,72,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140,167,168,186,318,337,339,382])). % 148.66/148.90 cnf(7880,plain, % 148.66/148.90 (P6(f15(x78801),x78801)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7884,plain, % 148.66/148.90 (P6(f15(x78841),x78841)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7887,plain, % 148.66/148.90 (P6(f15(x78871),x78871)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7889,plain, % 148.66/148.90 (P6(f16(f4(a1)),f20(a12))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,581,585,276,79,72,60,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,7853,7880,7884,76,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140,167,168,186,318,337,339,382,534,166,118,45,113,115,27])). % 148.66/148.90 cnf(7891,plain, % 148.66/148.90 (P6(f15(a12),f4(a1))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,581,585,276,79,72,60,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,7853,7880,7884,7887,76,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140,167,168,186,318,337,339,382,534,166,118,45,113,115,27,28])). % 148.66/148.90 cnf(7892,plain, % 148.66/148.90 (P6(f15(x78921),x78921)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7893,plain, % 148.66/148.90 (P21(f4(a1),a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,581,585,276,79,72,60,64,227,6466,580,579,70,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,7853,7880,7884,7887,76,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140,167,168,186,318,337,339,382,534,166,118,45,113,115,27,28,21])). % 148.66/148.90 cnf(7895,plain, % 148.66/148.90 (P6(f15(x78951),x78951)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7903,plain, % 148.66/148.90 (~P12(f19(a1),f20(f21(a1,a11)))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,581,585,276,6622,79,72,60,64,5157,227,6466,580,579,70,270,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,7853,7880,7884,7887,7892,7895,76,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140,167,168,186,318,337,339,382,534,166,118,45,113,115,27,28,21,123,39,49,124,170])). % 148.66/148.90 cnf(7905,plain, % 148.66/148.90 (P22(f4(a1),a1)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,581,585,276,6622,79,72,60,64,5157,227,6466,580,579,70,270,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,7853,7880,7884,7887,7892,7895,76,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140,167,168,186,318,337,339,382,534,166,118,45,113,115,27,28,21,123,39,49,124,170,41])). % 148.66/148.90 cnf(7906,plain, % 148.66/148.90 (P5(f4(a1),a12)), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,581,585,276,6622,79,72,7844,60,64,5157,227,6466,580,579,70,270,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,7853,7880,7884,7887,7892,7895,76,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140,167,168,186,318,337,339,382,534,166,118,45,113,115,27,28,21,123,39,49,124,170,41,43])). % 148.66/148.90 cnf(7908,plain, % 148.66/148.90 (P6(f16(a12),f20(f4(a1)))), % 148.66/148.90 inference(scs_inference,[],[54,69,78,203,583,587,4431,3714,6625,581,585,276,6622,79,72,7844,60,64,5157,227,6466,580,579,70,270,77,73,7820,7823,7826,7829,7832,7835,7838,7841,7846,7853,7880,7884,7887,7892,7895,76,56,55,93,94,95,96,97,98,99,107,142,111,4,5,6,7,10,11,12,13,14,15,16,17,18,159,8,9,81,90,85,87,89,82,91,2,101,102,103,104,105,106,108,109,127,128,129,130,131,132,133,134,161,162,163,164,165,126,121,112,120,119,122,116,114,44,125,169,35,141,3,135,136,138,139,140,167,168,186,318,337,339,382,534,166,118,45,113,115,27,28,21,123,39,49,124,170,41,43,137])). % 148.66/148.90 cnf(7913,plain, % 148.66/148.90 (E(f16(x79131),a12)), % 148.66/148.90 inference(rename_variables,[],[7762])). % 148.66/148.90 cnf(7915,plain, % 148.66/148.90 (E(f16(x79151),a12)), % 148.66/148.90 inference(rename_variables,[],[7762])). % 148.66/148.90 cnf(7917,plain, % 148.66/148.90 (E(f16(x79171),a12)), % 148.66/148.90 inference(rename_variables,[],[7762])). % 148.66/148.90 cnf(7918,plain, % 148.66/148.90 (E(f4(a10),a12)), % 148.66/148.90 inference(scs_inference,[],[7735,7762,7913,7915,2667,439,5069,81])). % 148.66/148.90 cnf(7920,plain, % 148.66/148.90 (P6(f17(a11),f20(a11))), % 148.66/148.90 inference(scs_inference,[],[7735,7762,7913,7915,3710,2667,439,5069,81,111])). % 148.66/148.90 cnf(7922,plain, % 148.66/148.90 (P6(f4(a1),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[7735,7762,7913,7915,3710,55,2667,439,5069,81,111,159])). % 148.66/148.90 cnf(7924,plain, % 148.66/148.90 (P6(f4(a1),f20(a12))), % 148.66/148.90 inference(scs_inference,[],[7735,7762,7913,7915,7906,3710,55,2667,439,5069,81,111,159,142])). % 148.66/148.90 cnf(7926,plain, % 148.66/148.90 (~P10(f17(f17(a13)))), % 148.66/148.90 inference(scs_inference,[],[7735,7737,7762,7913,7915,7906,3710,55,2667,439,5069,81,111,159,142,99])). % 148.66/148.90 cnf(7928,plain, % 148.66/148.90 (E(f20(f16(x79281)),f20(a12))), % 148.66/148.90 inference(scs_inference,[],[7735,7737,7762,7913,7915,7917,7906,3710,55,2667,439,5069,81,111,159,142,99,7])). % 148.66/148.90 cnf(7933,plain, % 148.66/148.90 (E(f21(x79331,f16(x79332)),f21(x79331,a12))), % 148.66/148.90 inference(scs_inference,[],[7735,7737,7762,7913,7915,7917,7906,3710,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9])). % 148.66/148.90 cnf(7934,plain, % 148.66/148.90 (E(f6(f16(x79341)),f6(a12))), % 148.66/148.90 inference(scs_inference,[],[7735,7737,7762,7913,7915,7917,7906,3710,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14])). % 148.66/148.90 cnf(7936,plain, % 148.66/148.90 (E(f15(f16(x79361)),f15(a12))), % 148.66/148.90 inference(scs_inference,[],[7735,7737,7762,7913,7915,7917,7906,3710,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5])). % 148.66/148.90 cnf(7938,plain, % 148.66/148.90 (E(f16(f16(x79381)),f16(a12))), % 148.66/148.90 inference(scs_inference,[],[7735,7737,7762,7913,7915,7917,7906,3710,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4])). % 148.66/148.90 cnf(7946,plain, % 148.66/148.90 (P6(f7(a1),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[7735,7737,7762,7913,7915,7917,7906,6009,3710,77,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161])). % 148.66/148.90 cnf(7950,plain, % 148.66/148.90 (~P10(f19(a1))), % 148.66/148.90 inference(scs_inference,[],[7735,7737,7762,7913,7915,7917,7891,7906,6009,583,3710,77,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161,126,108])). % 148.66/148.90 cnf(7952,plain, % 148.66/148.90 (~P10(f7(a1))), % 148.66/148.90 inference(scs_inference,[],[7735,7737,7762,7913,7915,7917,7891,7906,6009,583,3710,77,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161,126,108,109])). % 148.66/148.90 cnf(7959,plain, % 148.66/148.90 (P6(f15(x79591),x79591)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7962,plain, % 148.66/148.90 (P6(f15(x79621),x79621)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7965,plain, % 148.66/148.90 (P6(f15(x79651),x79651)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7968,plain, % 148.66/148.90 (P6(f15(x79681),x79681)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7971,plain, % 148.66/148.90 (P6(f15(x79711),x79711)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(7973,plain, % 148.66/148.90 (~P6(f20(x79731),f20(f4(a10)))), % 148.66/148.90 inference(scs_inference,[],[7764,7766,7770,7727,7735,7737,7762,7913,7915,7917,7777,7891,7906,586,6009,587,6004,583,3710,77,73,7959,7962,7965,7968,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161,126,108,109,119,121,120,122,113,117,112,169])). % 148.66/148.90 cnf(7983,plain, % 148.66/148.90 (~E(f4(a10),f17(a13))), % 148.66/148.90 inference(scs_inference,[],[7764,7766,7770,7727,7735,7737,7743,7762,7913,7915,7917,7777,7891,7906,7903,586,6009,587,6004,58,583,3710,77,73,7959,7962,7965,7968,7971,251,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161,126,108,109,119,121,120,122,113,117,112,169,125,124,143,24,35])). % 148.66/148.90 cnf(7984,plain, % 148.66/148.90 (P7(f17(a13),f20(a13))), % 148.66/148.90 inference(scs_inference,[],[7764,7766,7770,7727,7735,7737,7743,7762,7913,7915,7917,7777,7891,7906,7903,586,6009,587,6004,58,80,583,3710,77,73,7959,7962,7965,7968,7971,251,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161,126,108,109,119,121,120,122,113,117,112,169,125,124,143,24,35,141])). % 148.66/148.90 cnf(7989,plain, % 148.66/148.90 (~E(a12,f5(a1))), % 148.66/148.90 inference(scs_inference,[],[7874,7764,7766,7770,7727,7735,7737,7743,7762,7913,7915,7917,7777,7891,7870,7906,7903,586,6009,587,6004,58,66,80,583,3710,77,73,7959,7962,7965,7968,7971,251,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161,126,108,109,119,121,120,122,113,117,112,169,125,124,143,24,35,141,156,41])). % 148.66/148.90 cnf(7990,plain, % 148.66/148.90 (E(f16(x79901),f4(a1))), % 148.66/148.90 inference(scs_inference,[],[7874,7764,7766,7770,7727,7735,7737,7743,7762,7913,7915,7917,7777,7891,7870,7906,7903,586,6009,587,6004,58,66,80,583,580,3710,77,73,7959,7962,7965,7968,7971,251,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161,126,108,109,119,121,120,122,113,117,112,169,125,124,143,24,35,141,156,41,3])). % 148.66/148.90 cnf(7991,plain, % 148.66/148.90 (P6(f21(a1,a12),f20(f19(a1)))), % 148.66/148.90 inference(scs_inference,[],[7874,7764,7766,7770,7727,7735,7737,7743,7762,7913,7915,7917,7777,7891,7870,7906,7903,586,6009,587,6004,58,66,80,583,580,3710,77,73,7959,7962,7965,7968,7971,251,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161,126,108,109,119,121,120,122,113,117,112,169,125,124,143,24,35,141,156,41,3,187])). % 148.66/148.90 cnf(7993,plain, % 148.66/148.90 (E(f21(a1,a12),a12)), % 148.66/148.90 inference(scs_inference,[],[54,7874,7875,7764,7766,7770,7727,7735,7737,7743,7762,7913,7915,7917,7777,7891,7870,7906,7903,586,6009,587,6004,58,66,80,583,580,3710,77,73,7959,7962,7965,7968,7971,251,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161,126,108,109,119,121,120,122,113,117,112,169,125,124,143,24,35,141,156,41,3,187,178])). % 148.66/148.90 cnf(7996,plain, % 148.66/148.90 (P17(f17(a13))), % 148.66/148.90 inference(scs_inference,[],[54,7874,7875,7764,7766,7770,7727,7735,7737,7743,7762,7913,7915,7917,7777,7891,7870,7906,7903,586,6009,587,6004,58,66,80,583,580,3710,77,73,7959,7962,7965,7968,7971,251,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161,126,108,109,119,121,120,122,113,117,112,169,125,124,143,24,35,141,156,41,3,187,178,534,86])). % 148.66/148.90 cnf(7998,plain, % 148.66/148.90 (~P7(f20(a13),f17(a13))), % 148.66/148.90 inference(scs_inference,[],[54,7874,7875,7764,7766,7770,7727,7735,7737,7743,7762,7913,7915,7917,7777,7891,7870,7906,7903,586,6009,587,6004,58,66,80,583,580,3710,77,73,7959,7962,7965,7968,7971,251,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161,126,108,109,119,121,120,122,113,117,112,169,125,124,143,24,35,141,156,41,3,187,178,534,86,158])). % 148.66/148.90 cnf(8004,plain, % 148.66/148.90 (P23(f17(a13))), % 148.66/148.90 inference(scs_inference,[],[54,7874,7875,7764,7766,7770,7727,7735,7737,7743,7762,7913,7915,7917,7777,7891,7870,7906,7903,586,6009,587,6004,58,66,60,80,583,580,3710,77,73,7959,7962,7965,7968,7971,251,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161,126,108,109,119,121,120,122,113,117,112,169,125,124,143,24,35,141,156,41,3,187,178,534,86,158,166,148,157])). % 148.66/148.90 cnf(8006,plain, % 148.66/148.90 (~P18(f5(a1),a1)), % 148.66/148.90 inference(scs_inference,[],[54,7874,7875,7764,7766,7770,7727,7735,7737,7743,7762,7913,7915,7917,7777,7891,7862,7870,7906,7903,7866,586,6009,587,6004,58,66,60,80,583,580,3710,77,73,7959,7962,7965,7968,7971,251,55,2667,439,5069,81,111,159,142,99,7,18,15,6,11,9,14,12,5,13,4,16,8,10,17,91,2,161,126,108,109,119,121,120,122,113,117,112,169,125,124,143,24,35,141,156,41,3,187,178,534,86,158,166,148,157,190])). % 148.66/148.90 cnf(8011,plain, % 148.66/148.90 (~P10(f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[7950,381])). % 148.66/148.90 cnf(8015,plain, % 148.66/148.90 (~P10(f17(f19(a2)))), % 148.66/148.90 inference(scs_inference,[],[7789,300,142,99])). % 148.66/148.90 cnf(8017,plain, % 148.66/148.90 (E(f6(a1),a12)), % 148.66/148.90 inference(scs_inference,[],[7789,7787,300,142,99,81])). % 148.66/148.90 cnf(8020,plain, % 148.66/148.90 (E(f16(x80201),f4(a1))), % 148.66/148.90 inference(rename_variables,[],[7990])). % 148.66/148.90 cnf(8021,plain, % 148.66/148.90 (P5(f4(a1),f19(a1))), % 148.66/148.90 inference(scs_inference,[],[7990,8020,7789,7787,300,142,99,81,2667,439])). % 148.66/148.90 cnf(8024,plain, % 148.66/148.90 (E(f20(f21(a1,a12)),f20(a12))), % 148.66/148.90 inference(scs_inference,[],[7993,7990,8020,7789,7787,300,142,99,81,2667,439,18,7])). % 148.66/148.90 cnf(8025,plain, % 148.66/148.90 (E(f21(x80251,f21(a1,a12)),f21(x80251,a12))), % 148.66/148.90 inference(scs_inference,[],[7993,7990,8020,7789,7787,300,142,99,81,2667,439,18,7,9])). % 148.66/148.90 cnf(8033,plain, % 148.66/148.90 (E(f16(f21(a1,a12)),f16(a12))), % 148.66/148.90 inference(scs_inference,[],[7993,7990,8020,7789,7787,300,142,99,81,2667,439,18,7,9,11,6,12,15,16,17,5,4])). % 148.66/148.90 cnf(8040,plain, % 148.66/148.90 (P6(f15(x80401),x80401)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8043,plain, % 148.66/148.90 (P6(f15(x80431),x80431)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8045,plain, % 148.66/148.90 (P12(a11,f20(f21(a1,a11)))), % 148.66/148.90 inference(scs_inference,[],[7993,7990,8020,7783,7789,7983,8004,7787,300,275,73,8040,142,99,81,2667,439,18,7,9,11,6,12,15,16,17,5,4,14,13,8,10,2,126,119,166])). % 148.66/148.90 cnf(8048,plain, % 148.66/148.90 (P6(f15(x80481),x80481)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8051,plain, % 148.66/148.90 (P6(f15(x80511),x80511)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8054,plain, % 148.66/148.90 (P6(f15(x80541),x80541)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8057,plain, % 148.66/148.90 (P6(f15(x80571),x80571)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8061,plain, % 148.66/148.90 (~P6(f20(a13),f20(f6(a1)))), % 148.66/148.90 inference(scs_inference,[],[7993,7990,8020,7731,7783,7789,7920,7983,7984,7996,8004,7787,300,3712,275,73,8040,8043,8048,8051,8054,142,99,81,2667,439,18,7,9,11,6,12,15,16,17,5,4,14,13,8,10,2,126,119,166,121,116,118,122,171,169])). % 148.66/148.90 cnf(8064,plain, % 148.66/148.90 (P6(f15(x80641),x80641)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8069,plain, % 148.66/148.90 (~P7(x80691,f21(a1,a12))), % 148.66/148.90 inference(scs_inference,[],[7993,7990,8020,7731,7783,7789,7920,7983,7984,7996,8004,195,7787,300,3712,275,73,8040,8043,8048,8051,8054,8057,8064,142,99,81,2667,439,18,7,9,11,6,12,15,16,17,5,4,14,13,8,10,2,126,119,166,121,116,118,122,171,169,124,125,49])). % 148.66/148.90 cnf(8070,plain, % 148.66/148.90 (~P6(f20(a13),f17(a13))), % 148.66/148.90 inference(scs_inference,[],[7993,7990,8020,7731,7783,7789,7920,7983,7984,7996,7998,8004,195,7787,300,7737,3712,275,73,8040,8043,8048,8051,8054,8057,8064,142,99,81,2667,439,18,7,9,11,6,12,15,16,17,5,4,14,13,8,10,2,126,119,166,121,116,118,122,171,169,124,125,49,141])). % 148.66/148.90 cnf(8072,plain, % 148.66/148.90 (~E(f6(a1),f19(a2))), % 148.66/148.90 inference(scs_inference,[],[7993,7990,8020,7731,7783,7789,7920,7983,7984,7996,7998,8004,195,7787,300,7737,3712,275,73,8040,8043,8048,8051,8054,8057,8064,142,99,81,2667,439,18,7,9,11,6,12,15,16,17,5,4,14,13,8,10,2,126,119,166,121,116,118,122,171,169,124,125,49,141,35])). % 148.66/148.90 cnf(8073,plain, % 148.66/148.90 (~E(a12,f17(a13))), % 148.66/148.90 inference(scs_inference,[],[7993,7990,8020,7731,7783,7789,7920,7983,7984,7996,7998,8004,7918,195,7787,300,7737,3712,275,73,8040,8043,8048,8051,8054,8057,8064,142,99,81,2667,439,18,7,9,11,6,12,15,16,17,5,4,14,13,8,10,2,126,119,166,121,116,118,122,171,169,124,125,49,141,35,3])). % 148.66/148.90 cnf(8076,plain, % 148.66/148.90 (~E(f15(f17(a13)),f20(a13))), % 148.66/148.90 inference(scs_inference,[],[54,7993,7793,7990,8020,7731,7783,7789,7920,7983,7984,7996,7998,8004,7918,7811,195,7787,300,7737,3712,275,77,73,8040,8043,8048,8051,8054,8057,8064,55,142,99,81,2667,439,18,7,9,11,6,12,15,16,17,5,4,14,13,8,10,2,126,119,166,121,116,118,122,171,169,124,125,49,141,35,3,178,565])). % 148.66/148.90 cnf(8086,plain, % 148.66/148.90 (~P10(f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[8011,647])). % 148.66/148.90 cnf(8087,plain, % 148.66/148.90 (P7(f15(f21(a1,a11)),f19(a1))), % 148.66/148.90 inference(scs_inference,[],[8011,648])). % 148.66/148.90 cnf(8088,plain, % 148.66/148.90 (~E(f20(f19(a1)),f20(a12))), % 148.66/148.90 inference(scs_inference,[],[8011,3149])). % 148.66/148.90 cnf(8090,plain, % 148.66/148.90 (P6(x80901,f20(x80901))), % 148.66/148.90 inference(scs_inference,[],[72,142])). % 148.66/148.90 cnf(8092,plain, % 148.66/148.90 (~P10(f17(f21(a1,a11)))), % 148.66/148.90 inference(scs_inference,[],[8011,72,142,99])). % 148.66/148.90 cnf(8094,plain, % 148.66/148.90 (E(f15(f20(a12)),a12)), % 148.66/148.90 inference(scs_inference,[],[8011,7851,72,142,99,81])). % 148.66/148.90 cnf(8097,plain, % 148.66/148.90 (E(f20(f6(a1)),f20(a12))), % 148.66/148.90 inference(scs_inference,[],[8011,8017,7851,72,142,99,81,18,7])). % 148.66/148.90 cnf(8099,plain, % 148.66/148.90 (E(f21(x80991,f6(a1)),f21(x80991,a12))), % 148.66/148.90 inference(scs_inference,[],[8011,8017,7851,72,142,99,81,18,7,11,9])). % 148.66/148.90 cnf(8104,plain, % 148.66/148.90 (E(f16(f6(a1)),f16(a12))), % 148.66/148.90 inference(scs_inference,[],[8011,8017,7851,72,142,99,81,18,7,11,9,6,17,16,15,4])). % 148.66/148.90 cnf(8106,plain, % 148.66/148.90 (E(f6(f6(a1)),f6(a12))), % 148.66/148.90 inference(scs_inference,[],[8011,8017,7851,72,142,99,81,18,7,11,9,6,17,16,15,4,12,14])). % 148.66/148.90 cnf(8109,plain, % 148.66/148.90 (E(f21(f6(a1),x81091),f21(a12,x81091))), % 148.66/148.90 inference(scs_inference,[],[8011,8017,7851,72,142,99,81,18,7,11,9,6,17,16,15,4,12,14,10,5,8])). % 148.66/148.90 cnf(8115,plain, % 148.66/148.90 (~E(f20(f20(a13)),f17(a13))), % 148.66/148.90 inference(scs_inference,[],[8011,7989,8070,8017,7733,7851,72,73,142,99,81,18,7,11,9,6,17,16,15,4,12,14,10,5,8,13,2,126,28])). % 148.66/148.90 cnf(8116,plain, % 148.66/148.90 (~P7(x81161,f6(a1))), % 148.66/148.90 inference(scs_inference,[],[8011,7989,8070,8017,7733,7851,195,72,73,142,99,81,18,7,11,9,6,17,16,15,4,12,14,10,5,8,13,2,126,28,49])). % 148.66/148.90 cnf(8117,plain, % 148.66/148.90 (P7(f4(a1),f20(a12))), % 148.66/148.90 inference(scs_inference,[],[8011,7989,7924,8070,8017,7733,7851,195,72,80,73,142,99,81,18,7,11,9,6,17,16,15,4,12,14,10,5,8,13,2,126,28,49,141])). % 148.66/148.90 cnf(8120,plain, % 148.66/148.90 (~E(f15(f20(a12)),f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[8011,7989,7924,8070,8017,7733,7851,195,72,80,73,142,99,81,18,7,11,9,6,17,16,15,4,12,14,10,5,8,13,2,126,28,49,141,35])). % 148.66/148.90 cnf(8121,plain, % 148.66/148.90 (~E(a12,f19(a2))), % 148.66/148.90 inference(scs_inference,[],[8011,7989,7924,8070,8072,8017,7733,7851,195,72,80,73,142,99,81,18,7,11,9,6,17,16,15,4,12,14,10,5,8,13,2,126,28,49,141,35,3])). % 148.66/148.90 cnf(8122,plain, % 148.66/148.90 (E(f21(a1,f3(a1)),f3(a1))), % 148.66/148.90 inference(scs_inference,[],[54,8011,7799,7989,7924,8070,8072,8017,7813,7733,7851,195,72,80,77,73,55,142,99,81,18,7,11,9,6,17,16,15,4,12,14,10,5,8,13,2,126,28,49,141,35,3,179])). % 148.66/148.90 cnf(8124,plain, % 148.66/148.90 (P7(a12,f20(a12))), % 148.66/148.90 inference(scs_inference,[],[54,8011,7799,7989,7924,8070,8072,8017,7813,7733,7851,195,72,80,77,73,55,142,99,81,18,7,11,9,6,17,16,15,4,12,14,10,5,8,13,2,126,28,49,141,35,3,179,6011])). % 148.66/148.90 cnf(8132,plain, % 148.66/148.90 (~P10(f17(f7(a2)))), % 148.66/148.90 inference(scs_inference,[],[7791,99])). % 148.66/148.90 cnf(8134,plain, % 148.66/148.90 (E(f20(f4(a10)),f20(a12))), % 148.66/148.90 inference(scs_inference,[],[7791,7918,99,7])). % 148.66/148.90 cnf(8137,plain, % 148.66/148.90 (E(f21(x81371,f4(a10)),f21(x81371,a12))), % 148.66/148.90 inference(scs_inference,[],[7791,7918,99,7,11,18,9])). % 148.66/148.90 cnf(8145,plain, % 148.66/148.90 (E(f16(f4(a10)),f16(a12))), % 148.66/148.90 inference(scs_inference,[],[7791,8087,7918,99,7,11,18,9,16,17,6,158,12,14,4])). % 148.66/148.90 cnf(8148,plain, % 148.66/148.90 (E(f21(f4(a10),x81481),f21(a12,x81481))), % 148.66/148.90 inference(scs_inference,[],[7791,8087,7918,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8])). % 148.66/148.90 cnf(8153,plain, % 148.66/148.90 (P6(f15(x81531),x81531)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8157,plain, % 148.66/148.90 (P6(f15(x81571),x81571)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8159,plain, % 148.66/148.90 (~E(f6(a1),f20(a13))), % 148.66/148.90 inference(scs_inference,[],[8090,7791,8073,8087,8061,7785,7918,73,8153,251,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8,10,13,2,126,48,123,27])). % 148.66/148.90 cnf(8160,plain, % 148.66/148.90 (P6(x81601,f20(x81601))), % 148.66/148.90 inference(rename_variables,[],[8090])). % 148.66/148.90 cnf(8162,plain, % 148.66/148.90 (P6(f15(x81621),x81621)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8164,plain, % 148.66/148.90 (P6(f6(a1),f20(a12))), % 148.66/148.90 inference(scs_inference,[],[8090,8160,7791,8073,8087,8097,8061,7785,7918,73,8153,8157,251,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8,10,13,2,126,48,123,27,125,28])). % 148.66/148.90 cnf(8165,plain, % 148.66/148.90 (P6(x81651,f20(x81651))), % 148.66/148.90 inference(rename_variables,[],[8090])). % 148.66/148.90 cnf(8166,plain, % 148.66/148.90 (P10(f21(a1,a12))), % 148.66/148.90 inference(scs_inference,[],[8090,8160,8069,7791,8073,8087,8097,8061,7785,7918,73,8153,8157,8162,251,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8,10,13,2,126,48,123,27,125,28,141])). % 148.66/148.90 cnf(8167,plain, % 148.66/148.90 (~P7(x81671,f21(a1,a12))), % 148.66/148.90 inference(rename_variables,[],[8069])). % 148.66/148.90 cnf(8170,plain, % 148.66/148.90 (~P7(x81701,f21(a1,f6(a1)))), % 148.66/148.90 inference(scs_inference,[],[8090,8160,8069,8167,7791,8073,8087,8099,8097,8061,7785,7918,73,8153,8157,8162,251,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8,10,13,2,126,48,123,27,125,28,141,49])). % 148.66/148.90 cnf(8172,plain, % 148.66/148.90 (~E(f4(a1),f21(a1,a11))), % 148.66/148.90 inference(scs_inference,[],[8090,8160,8086,8069,8167,7791,8073,8087,8099,8097,8061,7785,7918,585,73,8153,8157,8162,251,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8,10,13,2,126,48,123,27,125,28,141,49,35])). % 148.66/148.90 cnf(8173,plain, % 148.66/148.90 (~E(f4(a1),f17(a13))), % 148.66/148.90 inference(scs_inference,[],[8090,8160,8086,8069,8167,7791,8073,8087,8099,8097,8061,7785,7918,585,580,73,8153,8157,8162,251,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8,10,13,2,126,48,123,27,125,28,141,49,35,3])). % 148.66/148.90 cnf(8178,plain, % 148.66/148.90 (P23(f21(a1,a12))), % 148.66/148.90 inference(scs_inference,[],[54,8090,8160,8086,7803,7860,8069,8167,7791,8073,8087,8099,8097,7817,8061,7785,7866,7918,585,580,77,73,8153,8157,8162,251,55,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8,10,13,2,126,48,123,27,125,28,141,49,35,3,178,179,90])). % 148.66/148.90 cnf(8180,plain, % 148.66/148.90 (P19(f21(a1,a12))), % 148.66/148.90 inference(scs_inference,[],[54,8090,8160,8086,7803,7860,8069,8167,7791,8073,8087,8099,8097,7817,8061,7785,7866,7918,585,580,77,73,8153,8157,8162,251,55,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8,10,13,2,126,48,123,27,125,28,141,49,35,3,178,179,90,89])). % 148.66/148.90 cnf(8182,plain, % 148.66/148.90 (P17(f21(a1,a12))), % 148.66/148.90 inference(scs_inference,[],[54,8090,8160,8086,7803,7860,8069,8167,7791,8073,8087,8099,8097,7817,8061,7785,7866,7918,585,580,77,73,8153,8157,8162,251,55,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8,10,13,2,126,48,123,27,125,28,141,49,35,3,178,179,90,89,87])). % 148.66/148.90 cnf(8184,plain, % 148.66/148.90 (P9(f21(a1,a12))), % 148.66/148.90 inference(scs_inference,[],[54,8090,8160,8086,7803,7860,8069,8167,7791,8073,8087,8099,8097,7817,8061,7785,7866,7918,585,580,77,73,8153,8157,8162,251,55,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8,10,13,2,126,48,123,27,125,28,141,49,35,3,178,179,90,89,87,85])). % 148.66/148.90 cnf(8186,plain, % 148.66/148.90 (P3(f21(a1,a12))), % 148.66/148.90 inference(scs_inference,[],[54,8090,8160,8086,7803,7860,8069,8167,7791,8073,8087,8099,8097,7817,8061,7785,7866,7918,585,580,77,73,8153,8157,8162,251,55,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8,10,13,2,126,48,123,27,125,28,141,49,35,3,178,179,90,89,87,85,83])). % 148.66/148.90 cnf(8190,plain, % 148.66/148.90 (~P18(f21(a1,f5(a1)),a1)), % 148.66/148.90 inference(scs_inference,[],[54,8090,8160,8165,8086,7803,7860,8069,8167,7791,8073,8087,8099,8097,7817,8061,8006,7785,7866,7918,585,580,77,73,8153,8157,8162,251,55,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8,10,13,2,126,48,123,27,125,28,141,49,35,3,178,179,90,89,87,85,83,119,39])). % 148.66/148.90 cnf(8191,plain, % 148.66/148.90 (~P22(f21(a1,f5(a1)),a1)), % 148.66/148.90 inference(scs_inference,[],[54,8090,8160,8165,8086,7803,7860,8069,8167,7791,8073,8087,8099,8097,7817,8061,8006,7785,7866,7918,585,7870,580,77,73,8153,8157,8162,251,55,99,7,11,18,9,16,17,6,158,12,14,4,15,5,8,10,13,2,126,48,123,27,125,28,141,49,35,3,178,179,90,89,87,85,83,119,39,41])). % 148.66/148.90 cnf(8195,plain, % 148.66/148.90 (~P10(f17(f5(a1)))), % 148.66/148.90 inference(scs_inference,[],[7856,99])). % 148.66/148.90 cnf(8197,plain, % 148.66/148.90 (E(f20(f4(a1)),f20(a12))), % 148.66/148.90 inference(scs_inference,[],[7856,579,99,7])). % 148.66/148.90 cnf(8198,plain, % 148.66/148.90 (E(f21(x81981,f4(a1)),f21(x81981,a12))), % 148.66/148.90 inference(scs_inference,[],[7856,579,99,7,9])). % 148.66/148.90 cnf(8200,plain, % 148.66/148.90 (E(f5(f4(a1)),f5(a12))), % 148.66/148.90 inference(scs_inference,[],[7856,579,99,7,9,16,17])). % 148.66/148.90 cnf(8204,plain, % 148.66/148.90 (E(f18(f4(a1)),f18(a12))), % 148.66/148.90 inference(scs_inference,[],[7856,579,99,7,9,16,17,11,6,18,12])). % 148.66/148.90 cnf(8207,plain, % 148.66/148.90 (E(f6(f4(a1)),f6(a12))), % 148.66/148.90 inference(scs_inference,[],[7856,579,99,7,9,16,17,11,6,18,12,5,15,14])). % 148.66/148.90 cnf(8208,plain, % 148.66/148.90 (E(f16(f4(a1)),f16(a12))), % 148.66/148.90 inference(scs_inference,[],[7856,579,99,7,9,16,17,11,6,18,12,5,15,14,4])). % 148.66/148.90 cnf(8211,plain, % 148.66/148.90 (E(f21(f4(a1),x82111),f21(a12,x82111))), % 148.66/148.90 inference(scs_inference,[],[7856,579,99,7,9,16,17,11,6,18,12,5,15,14,4,10,13,8])). % 148.66/148.90 cnf(8212,plain, % 148.66/148.90 (~E(f21(a1,a11),f4(a1))), % 148.66/148.90 inference(scs_inference,[],[8172,7856,579,99,7,9,16,17,11,6,18,12,5,15,14,4,10,13,8,2])). % 148.66/148.90 cnf(8214,plain, % 148.66/148.90 (P6(f15(x82141),x82141)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8217,plain, % 148.66/148.90 (P6(f15(x82171),x82171)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8220,plain, % 148.66/148.90 (P6(f15(x82201),x82201)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8223,plain, % 148.66/148.90 (P6(f15(x82231),x82231)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8226,plain, % 148.66/148.90 (E(f21(x82261,a12),f21(x82261,f4(a1)))), % 148.66/148.90 inference(rename_variables,[],[7761])). % 148.66/148.90 cnf(8228,plain, % 148.66/148.90 (E(f21(x82281,a12),f21(x82281,f4(a1)))), % 148.66/148.90 inference(rename_variables,[],[7761])). % 148.66/148.90 cnf(8229,plain, % 148.66/148.90 (~P6(f20(a12),f20(f21(a1,a12)))), % 148.66/148.90 inference(scs_inference,[],[8166,8178,8180,8182,8172,7856,8124,7761,8226,579,73,8214,8217,8220,99,7,9,16,17,11,6,18,12,5,15,14,4,10,13,8,2,118,126,115,121,33,31,169])). % 148.66/148.90 cnf(8235,plain, % 148.66/148.90 (E(f21(x82351,a12),f21(x82351,f4(a1)))), % 148.66/148.90 inference(rename_variables,[],[7761])). % 148.66/148.90 cnf(8237,plain, % 148.66/148.90 (E(f21(x82371,a12),f21(x82371,f4(a1)))), % 148.66/148.90 inference(rename_variables,[],[7761])). % 148.66/148.90 cnf(8240,plain, % 148.66/148.90 (P6(a12,f20(f4(a1)))), % 148.66/148.90 inference(scs_inference,[],[8166,8178,8180,8182,8184,8186,8172,7856,8124,7761,8226,8228,8235,8237,8090,579,73,8214,8217,8220,8223,99,7,9,16,17,11,6,18,12,5,15,14,4,10,13,8,2,118,126,115,121,33,31,169,124,23,26,29,27])). % 148.66/148.90 cnf(8242,plain, % 148.66/148.90 (P7(f6(a1),f20(a12))), % 148.66/148.90 inference(scs_inference,[],[8166,8178,8180,8182,8184,8186,8172,7856,8164,8124,7761,8226,8228,8235,8237,8090,80,579,73,8214,8217,8220,8223,99,7,9,16,17,11,6,18,12,5,15,14,4,10,13,8,2,118,126,115,121,33,31,169,124,23,26,29,27,141])). % 148.66/148.90 cnf(8245,plain, % 148.66/148.90 (~E(f21(a1,a12),f5(a1))), % 148.66/148.90 inference(scs_inference,[],[8166,8178,8180,8182,8184,8186,8172,7856,8164,8124,7761,8226,8228,8235,8237,8090,80,579,73,8214,8217,8220,8223,99,7,9,16,17,11,6,18,12,5,15,14,4,10,13,8,2,118,126,115,121,33,31,169,124,23,26,29,27,141,35])). % 148.66/148.90 cnf(8246,plain, % 148.66/148.90 (~P7(x82461,f21(a1,f4(a10)))), % 148.66/148.90 inference(scs_inference,[],[8166,8178,8180,8182,8184,8186,8172,7856,8164,8137,8124,7761,8226,8228,8235,8237,8090,8069,80,579,73,8214,8217,8220,8223,99,7,9,16,17,11,6,18,12,5,15,14,4,10,13,8,2,118,126,115,121,33,31,169,124,23,26,29,27,141,35,49])). % 148.66/148.90 cnf(8247,plain, % 148.66/148.90 (E(f21(x82471,f4(a10)),f21(x82471,a12))), % 148.66/148.90 inference(rename_variables,[],[8137])). % 148.66/148.90 cnf(8249,plain, % 148.66/148.90 (E(f21(f6(a1),f4(a10)),f21(a12,a12))), % 148.66/148.90 inference(scs_inference,[],[8166,8178,8180,8182,8184,8186,8172,7856,8164,8109,8137,8247,8191,8124,7761,8226,8228,8235,8237,7905,8090,8069,80,579,73,8214,8217,8220,8223,99,7,9,16,17,11,6,18,12,5,15,14,4,10,13,8,2,118,126,115,121,33,31,169,124,23,26,29,27,141,35,49,41,3])). % 148.66/148.90 cnf(8252,plain, % 148.66/148.90 (P18(f21(a1,a12),a1)), % 148.66/148.90 inference(scs_inference,[],[8166,8178,8180,8182,8184,8186,8172,7856,8164,8109,8137,8247,7991,8191,8124,7761,8226,8228,8235,8237,7905,8090,8069,80,579,73,8214,8217,8220,8223,55,99,7,9,16,17,11,6,18,12,5,15,14,4,10,13,8,2,118,126,115,121,33,31,169,124,23,26,29,27,141,35,49,41,3,172])). % 148.66/148.90 cnf(8254,plain, % 148.66/148.90 (P21(f21(a1,a12),a1)), % 148.66/148.90 inference(scs_inference,[],[54,8166,8178,8180,8182,8184,8186,8172,7856,8164,8109,8137,8247,7991,8191,8124,7761,8226,8228,8235,8237,7905,8090,8069,80,579,73,8214,8217,8220,8223,55,99,7,9,16,17,11,6,18,12,5,15,14,4,10,13,8,2,118,126,115,121,33,31,169,124,23,26,29,27,141,35,49,41,3,172,173])). % 148.66/148.90 cnf(8256,plain, % 148.66/148.90 (P22(f21(a1,a12),a1)), % 148.66/148.90 inference(scs_inference,[],[54,8166,8178,8180,8182,8184,8186,8172,7856,8164,8109,8137,8247,7991,8191,8124,7761,8226,8228,8235,8237,7905,8090,8069,80,579,73,8214,8217,8220,8223,55,99,7,9,16,17,11,6,18,12,5,15,14,4,10,13,8,2,118,126,115,121,33,31,169,124,23,26,29,27,141,35,49,41,3,172,173,175])). % 148.66/148.90 cnf(8258,plain, % 148.66/148.90 (P24(f21(a1,a12),a1)), % 148.66/148.90 inference(scs_inference,[],[54,8166,8178,8180,8182,8184,8186,8172,7856,8164,8109,8137,8247,7991,8191,8124,7761,8226,8228,8235,8237,7905,8090,8069,80,579,73,8214,8217,8220,8223,55,99,7,9,16,17,11,6,18,12,5,15,14,4,10,13,8,2,118,126,115,121,33,31,169,124,23,26,29,27,141,35,49,41,3,172,173,175,174])). % 148.66/148.90 cnf(8262,plain, % 148.66/148.90 (~E(f16(f21(a1,a12)),f20(a12))), % 148.66/148.90 inference(scs_inference,[],[54,7864,8166,8178,8180,8182,8184,8186,8172,7856,8164,8109,8137,8247,7868,7991,8191,8124,7761,8226,8228,8235,8237,7905,8090,8069,80,579,77,73,8214,8217,8220,8223,55,99,7,9,16,17,11,6,18,12,5,15,14,4,10,13,8,2,118,126,115,121,33,31,169,124,23,26,29,27,141,35,49,41,3,172,173,175,174,179,534])). % 148.66/148.90 cnf(8270,plain, % 148.66/148.90 (~P10(f17(f9(a1)))), % 148.66/148.90 inference(scs_inference,[],[7858,99])). % 148.66/148.90 cnf(8272,plain, % 148.66/148.90 (~E(f5(a1),f21(a1,a12))), % 148.66/148.90 inference(scs_inference,[],[8245,7858,99,2])). % 148.66/148.90 cnf(8273,plain, % 148.66/148.90 (P24(f21(a1,f4(a1)),a1)), % 148.66/148.90 inference(scs_inference,[],[8258,8245,7858,7761,99,2,45])). % 148.66/148.90 cnf(8274,plain, % 148.66/148.90 (E(f21(x82741,a12),f21(x82741,f4(a1)))), % 148.66/148.90 inference(rename_variables,[],[7761])). % 148.66/148.90 cnf(8276,plain, % 148.66/148.90 (P6(f15(x82761),x82761)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8280,plain, % 148.66/148.90 (E(f21(x82801,a12),f21(x82801,f4(a1)))), % 148.66/148.90 inference(rename_variables,[],[7761])). % 148.66/148.90 cnf(8281,plain, % 148.66/148.90 (~P6(f20(a12),f20(f6(a1)))), % 148.66/148.90 inference(scs_inference,[],[8254,8258,8245,7858,8242,8021,7761,8274,7764,7787,270,73,99,2,45,126,44,21,169])). % 148.66/148.90 cnf(8284,plain, % 148.66/148.90 (P6(f15(x82841),x82841)), % 148.66/148.90 inference(rename_variables,[],[73])). % 148.66/148.90 cnf(8287,plain, % 148.66/148.90 (P5(f21(x82871,a12),f21(x82871,f4(a1)))), % 148.66/148.90 inference(scs_inference,[],[7873,8254,8258,8245,7858,8242,8198,8190,8021,8094,7761,8274,7764,7787,72,270,73,8276,99,2,45,126,44,21,169,170,39,43])). % 148.66/148.90 cnf(8289,plain, % 148.66/148.90 (P10(f21(a1,f6(a1)))), % 148.66/148.90 inference(scs_inference,[],[7873,8254,8258,8245,7858,8242,8198,8170,8190,8021,8094,7761,8274,7764,7787,72,270,73,8276,8284,99,2,45,126,44,21,169,170,39,43,141])). % 148.66/148.90 cnf(8294,plain, % 148.66/148.90 (~E(f20(a12),f6(a1))), % 148.66/148.90 inference(scs_inference,[],[7873,8116,8254,8258,8245,7858,8242,8198,8170,8190,8021,8094,7761,8274,7764,7851,7787,72,270,73,8276,8284,99,2,45,126,44,21,169,170,39,43,141,35,49])). % 148.66/148.90 cnf(8299,plain, % 148.66/148.90 (P6(f4(a1),f20(f21(a1,a11)))), % 148.66/148.90 inference(scs_inference,[],[7873,8116,8212,8254,8256,8258,8245,7858,8242,8198,8170,8190,8021,8094,7761,8274,8280,7764,7851,7787,72,270,73,8276,8284,251,99,2,45,126,44,21,169,170,39,43,141,35,49,41,3,142])). % 148.66/148.91 cnf(8332,plain, % 148.66/148.91 (E(f21(a1,f6(a1)),a12)), % 148.66/148.91 inference(scs_inference,[],[8289,90,89,83,85,87,81])). % 148.66/148.91 cnf(8334,plain, % 148.66/148.91 (~P10(f17(f19(a1)))), % 148.66/148.91 inference(scs_inference,[],[7950,8289,90,89,83,85,87,81,99])). % 148.66/148.91 cnf(8336,plain, % 148.66/148.91 (~E(f20(a13),f6(a1))), % 148.66/148.91 inference(scs_inference,[],[8159,7950,8289,90,89,83,85,87,81,99,2])). % 148.66/148.91 cnf(8341,plain, % 148.66/148.91 (P7(f16(f4(a1)),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8159,8252,7950,7889,8289,8299,8172,7761,80,90,89,83,85,87,81,99,2,166,39,141])). % 148.66/148.91 cnf(8344,plain, % 148.66/148.91 (~E(f21(a1,f6(a1)),f19(a1))), % 148.66/148.91 inference(scs_inference,[],[8159,8252,7950,7889,8289,8299,8172,7761,80,90,89,83,85,87,81,99,2,166,39,141,35])). % 148.66/148.91 cnf(8347,plain, % 148.66/148.91 (E(f21(f4(a1),f21(a1,a12)),f21(a12,a12))), % 148.66/148.91 inference(scs_inference,[],[8159,8252,7950,7889,8289,8299,8211,8134,8025,8172,7761,6622,80,90,89,83,85,87,81,99,2,166,39,141,35,49,3])). % 148.66/148.91 cnf(8361,plain, % 148.66/148.91 (~P10(f17(f7(a1)))), % 148.66/148.91 inference(scs_inference,[],[7952,99])). % 148.66/148.91 cnf(8363,plain, % 148.66/148.91 (~E(f17(a13),f4(a1))), % 148.66/148.91 inference(scs_inference,[],[7952,8173,99,2])). % 148.66/148.91 cnf(8365,plain, % 148.66/148.91 (P6(x83651,f20(x83651))), % 148.66/148.91 inference(rename_variables,[],[8090])). % 148.66/148.91 cnf(8367,plain, % 148.66/148.91 (P6(f21(a1,a12),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[7952,8173,8229,8024,8090,8365,99,2,171,28])). % 148.66/148.91 cnf(8368,plain, % 148.66/148.91 (P6(x83681,f20(x83681))), % 148.66/148.91 inference(rename_variables,[],[8090])). % 148.66/148.91 cnf(8369,plain, % 148.66/148.91 (P6(a12,f20(f21(a1,a12)))), % 148.66/148.91 inference(scs_inference,[],[7952,8173,8229,8024,8090,8365,8368,7993,99,2,171,28,27])). % 148.66/148.91 cnf(8371,plain, % 148.66/148.91 (P10(f21(a1,f4(a10)))), % 148.66/148.91 inference(scs_inference,[],[7952,8173,8246,8229,8024,8090,8365,8368,7993,73,99,2,171,28,27,141])). % 148.66/148.91 cnf(8372,plain, % 148.66/148.91 (~P7(x83721,f21(a1,f4(a10)))), % 148.66/148.91 inference(rename_variables,[],[8246])). % 148.66/148.91 cnf(8378,plain, % 148.66/148.91 (~E(f5(a1),f21(a1,f16(x83781)))), % 148.66/148.91 inference(scs_inference,[],[8272,7952,8173,8341,8246,8372,8229,8024,7933,8090,8365,8368,7851,7993,73,99,2,171,28,27,141,35,49,3])). % 148.66/148.91 cnf(8395,plain, % 148.66/148.91 (E(f21(a1,f4(a10)),a12)), % 148.66/148.91 inference(scs_inference,[],[8371,85,89,83,87,90,81])). % 148.66/148.91 cnf(8397,plain, % 148.66/148.91 (~P10(f17(f20(x83971)))), % 148.66/148.91 inference(scs_inference,[],[8371,80,85,89,83,87,90,81,99])). % 148.66/148.91 cnf(8399,plain, % 148.66/148.91 (~E(f6(a1),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8294,8371,80,85,89,83,87,90,81,99,2])). % 148.66/148.91 cnf(8400,plain, % 148.66/148.91 (P7(f21(a1,a12),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8367,8294,8371,80,85,89,83,87,90,81,99,2,141])). % 148.66/148.91 cnf(8403,plain, % 148.66/148.91 (~E(f21(a1,f4(a10)),f21(a1,a11))), % 148.66/148.91 inference(scs_inference,[],[8367,8294,8371,8086,80,85,89,83,87,90,81,99,2,141,35])). % 148.66/148.91 cnf(8404,plain, % 148.66/148.91 (~P7(x84041,f21(a1,f4(a1)))), % 148.66/148.91 inference(scs_inference,[],[8367,8294,8371,8086,8198,8069,80,85,89,83,87,90,81,99,2,141,35,49])). % 148.66/148.91 cnf(8406,plain, % 148.66/148.91 (~E(a12,f19(a1))), % 148.66/148.91 inference(scs_inference,[],[8367,8294,8344,8332,8371,8086,8198,8069,80,85,89,83,87,90,81,99,2,141,35,49,3])). % 148.66/148.91 cnf(8423,plain, % 148.66/148.91 (~P10(f17(a11))), % 148.66/148.91 inference(scs_inference,[],[3710,99])). % 148.66/148.91 cnf(8426,plain, % 148.66/148.91 (~P6(f20(a12),f20(f4(a1)))), % 148.66/148.91 inference(scs_inference,[],[8400,8406,585,3710,99,2,169])). % 148.66/148.91 cnf(8428,plain, % 148.66/148.91 (P6(f16(x84281),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8400,8406,7928,8090,585,3710,99,2,169,28])). % 148.66/148.91 cnf(8430,plain, % 148.66/148.91 (P6(f21(a1,f4(a1)),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8400,8406,7928,8367,8090,7761,585,3710,99,2,169,28,27])). % 148.66/148.91 cnf(8452,plain, % 148.66/148.91 (~P10(f17(f17(a11)))), % 148.66/148.91 inference(scs_inference,[],[8423,7762,7706,142,99])). % 148.66/148.91 cnf(8455,plain, % 148.66/148.91 (~P6(f19(a1),f20(f6(a1)))), % 148.66/148.91 inference(scs_inference,[],[8423,8121,8087,7762,7787,7706,142,99,2,169])). % 148.66/148.91 cnf(8457,plain, % 148.66/148.91 (~P6(f20(a12),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8423,8121,8426,7748,8087,7762,7787,7706,142,99,2,169,28])). % 148.66/148.91 cnf(8458,plain, % 148.66/148.91 (~P6(f21(a1,a11),f20(f6(a1)))), % 148.66/148.91 inference(scs_inference,[],[8423,8121,8426,7748,8087,7762,7787,251,7706,142,99,2,169,28,27])). % 148.66/148.91 cnf(8459,plain, % 148.66/148.91 (P7(f16(x84591),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8428,8423,8121,8426,7748,8087,7762,7787,80,251,7706,142,99,2,169,28,27,141])). % 148.66/148.91 cnf(8462,plain, % 148.66/148.91 (~E(f6(a1),f17(a11))), % 148.66/148.91 inference(scs_inference,[],[8428,8423,8121,8426,7748,8087,7762,7787,80,251,7706,142,99,2,169,28,27,141,35])). % 148.66/148.91 cnf(8463,plain, % 148.66/148.91 (~P7(x84631,f21(a1,f21(a1,a12)))), % 148.66/148.91 inference(scs_inference,[],[8428,8423,8121,8426,8025,7748,8087,7762,8069,7787,80,251,7706,142,99,2,169,28,27,141,35,49])). % 148.66/148.91 cnf(8465,plain, % 148.66/148.91 (~E(a12,f21(a1,a11))), % 148.66/148.91 inference(scs_inference,[],[8428,8423,8121,8403,8395,8426,8025,7748,8087,7762,8069,7787,80,251,7706,142,99,2,169,28,27,141,35,49,3])). % 148.66/148.91 cnf(8475,plain, % 148.66/148.91 (P6(f16(a12),f20(f6(a1)))), % 148.66/148.91 inference(scs_inference,[],[8104,7686,137])). % 148.66/148.91 cnf(8477,plain, % 148.66/148.91 (~E(f16(a12),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8457,8104,7686,137,534])). % 148.66/148.91 cnf(8480,plain, % 148.66/148.91 (P6(f15(x84801),x84801)), % 148.66/148.91 inference(rename_variables,[],[73])). % 148.66/148.91 cnf(8485,plain, % 148.66/148.91 (~P6(f20(a12),f20(f16(x84851)))), % 148.66/148.91 inference(scs_inference,[],[8457,8459,8465,8287,8104,7760,66,70,73,7686,137,534,2,126,44,169])). % 148.66/148.91 cnf(8487,plain, % 148.66/148.91 (~P12(f16(a12),f20(f4(a1)))), % 148.66/148.91 inference(scs_inference,[],[8457,8459,8465,8287,8104,7760,7908,7990,66,70,73,7686,137,534,2,126,44,169,170])). % 148.66/148.91 cnf(8488,plain, % 148.66/148.91 (E(f16(x84881),f4(a1))), % 148.66/148.91 inference(rename_variables,[],[7990])). % 148.66/148.91 cnf(8490,plain, % 148.66/148.91 (P5(f21(a12,a12),f21(f4(a1),f21(a1,a12)))), % 148.66/148.91 inference(scs_inference,[],[8457,8459,8465,8287,8347,8104,7760,7908,7990,66,72,70,73,7686,137,534,2,126,44,169,170,43])). % 148.66/148.91 cnf(8493,plain, % 148.66/148.91 (P6(f15(x84931),x84931)), % 148.66/148.91 inference(rename_variables,[],[73])). % 148.66/148.91 cnf(8494,plain, % 148.66/148.91 (~P6(f20(f4(a1)),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8457,8459,8465,8287,8347,8104,7760,7908,8197,7990,8488,66,72,70,73,8480,7686,137,534,2,126,44,169,170,43,28,27])). % 148.66/148.91 cnf(8495,plain, % 148.66/148.91 (P10(f21(a1,f4(a1)))), % 148.66/148.91 inference(scs_inference,[],[8457,8459,8465,8404,8287,8347,8104,7760,7908,8197,7990,8488,66,72,70,73,8480,8493,7686,137,534,2,126,44,169,170,43,28,27,141])). % 148.66/148.91 cnf(8502,plain, % 148.66/148.91 (~E(f17(a13),f16(x85021))), % 148.66/148.91 inference(scs_inference,[],[8457,8459,8465,8363,8397,8404,8463,8287,8347,8104,7760,7908,8197,7990,8488,7735,66,72,70,73,8480,8493,7686,137,534,2,126,44,169,170,43,28,27,141,35,49,3])). % 148.66/148.91 cnf(8503,plain, % 148.66/148.91 (E(f21(a1,f6(a1)),f6(a1))), % 148.66/148.91 inference(scs_inference,[],[54,8457,8459,8465,8363,8397,8404,8463,8287,7801,8347,8104,7760,7908,7815,8197,7990,8488,7735,66,72,70,77,73,8480,8493,55,7686,137,534,2,126,44,169,170,43,28,27,141,35,49,3,179])). % 148.66/148.91 cnf(8511,plain, % 148.66/148.91 (E(f21(a1,f4(a1)),a12)), % 148.66/148.91 inference(scs_inference,[],[8495,81])). % 148.66/148.91 cnf(8514,plain, % 148.66/148.91 (~E(f16(x85141),f17(a13))), % 148.66/148.91 inference(scs_inference,[],[8502,8494,8495,81,534,2])). % 148.66/148.91 cnf(8515,plain, % 148.66/148.91 (~P12(f16(a12),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8502,8494,8495,8487,7748,81,534,2,25])). % 148.66/148.91 cnf(8516,plain, % 148.66/148.91 (P7(f21(a1,f4(a1)),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8502,8494,8430,8495,8487,7748,80,81,534,2,25,141])). % 148.66/148.91 cnf(8519,plain, % 148.66/148.91 (~E(f16(a12),f20(a13))), % 148.66/148.91 inference(scs_inference,[],[8502,8494,8430,8495,8475,8487,8061,7748,80,81,534,2,25,141,27])). % 148.66/148.91 cnf(8520,plain, % 148.66/148.91 (~E(f21(a1,f4(a1)),f7(a2))), % 148.66/148.91 inference(scs_inference,[],[8502,8494,8430,8495,8475,8487,7791,8061,7748,80,81,534,2,25,141,27,35])). % 148.66/148.91 cnf(8521,plain, % 148.66/148.91 (~P7(x85211,f21(a1,f16(x85212)))), % 148.66/148.91 inference(scs_inference,[],[8502,8494,8430,8495,8475,8487,7791,7933,8061,7748,8069,80,81,534,2,25,141,27,35,49])). % 148.66/148.91 cnf(8523,plain, % 148.66/148.91 (~E(f6(a1),f19(a1))), % 148.66/148.91 inference(scs_inference,[],[8502,8494,8430,8503,8495,8475,8487,8344,7791,7933,8061,7748,8069,80,81,534,2,25,141,27,35,49,3])). % 148.66/148.91 cnf(8531,plain, % 148.66/148.91 (~E(f16(f6(a1)),f21(a1,a11))), % 148.66/148.91 inference(scs_inference,[],[8458,534])). % 148.66/148.91 cnf(8532,plain, % 148.66/148.91 (~E(f19(a1),f6(a1))), % 148.66/148.91 inference(scs_inference,[],[8523,8458,534,2])). % 148.66/148.91 cnf(8533,plain, % 148.66/148.91 (~P7(f21(a1,a11),f20(f6(a1)))), % 148.66/148.91 inference(scs_inference,[],[8523,8458,8090,534,2,171])). % 148.66/148.91 cnf(8536,plain, % 148.66/148.91 (~P12(f16(a12),f20(f6(a1)))), % 148.66/148.91 inference(scs_inference,[],[8515,8523,8458,8097,8090,534,2,171,25])). % 148.66/148.91 cnf(8538,plain, % 148.66/148.91 (P10(f21(a1,f16(x85381)))), % 148.66/148.91 inference(scs_inference,[],[8515,8523,8458,8521,8145,8097,8090,73,534,2,171,25,24,141])). % 148.66/148.91 cnf(8539,plain, % 148.66/148.91 (~P7(x85391,f21(a1,f16(x85392)))), % 148.66/148.91 inference(rename_variables,[],[8521])). % 148.66/148.91 cnf(8542,plain, % 148.66/148.91 (P6(f4(a1),f20(f6(a1)))), % 148.66/148.91 inference(scs_inference,[],[8515,8523,8458,8521,8145,8475,8097,7990,8090,73,534,2,171,25,24,141,27])). % 148.66/148.91 cnf(8550,plain, % 148.66/148.91 (E(f16(a12),f6(a1))), % 148.66/148.91 inference(scs_inference,[],[8515,8523,8336,8516,7758,8458,8521,8539,7926,8145,8475,8503,8097,7990,8090,585,73,534,2,171,25,24,141,27,35,49,3,113,166])). % 148.66/148.91 cnf(8565,plain, % 148.66/148.91 (E(f21(a1,f16(x85651)),a12)), % 148.66/148.91 inference(scs_inference,[],[8538,87,90,89,83,85,81])). % 148.66/148.91 cnf(8568,plain, % 148.66/148.91 (~E(f17(a11),f6(a1))), % 148.66/148.91 inference(scs_inference,[],[8462,8485,8538,87,90,89,83,85,81,534,2])). % 148.66/148.91 cnf(8570,plain, % 148.66/148.91 (~P12(f16(a12),f20(f4(a10)))), % 148.66/148.91 inference(scs_inference,[],[8462,8533,8485,8538,8134,8515,270,87,90,89,83,85,81,534,2,48,25])). % 148.66/148.91 cnf(8575,plain, % 148.66/148.91 (~P6(f20(f4(a10)),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8462,7809,8533,8485,8538,8033,8134,8515,8457,80,270,87,90,89,83,85,81,534,2,48,25,24,141,27])). % 148.66/148.91 cnf(8576,plain, % 148.66/148.91 (~E(f21(a1,f16(x85761)),f21(a1,a11))), % 148.66/148.91 inference(scs_inference,[],[8462,7809,8533,8485,8538,8033,8134,8515,8011,8457,80,270,87,90,89,83,85,81,534,2,48,25,24,141,27,35])). % 148.66/148.91 cnf(8578,plain, % 148.66/148.91 (~E(f6(a1),f17(a13))), % 148.66/148.91 inference(scs_inference,[],[8514,8462,8550,7809,8533,8485,8538,8033,8117,8134,8515,8011,8457,7748,80,270,87,90,89,83,85,81,534,2,48,25,24,141,27,35,49,3])). % 148.66/148.91 cnf(8580,plain, % 148.66/148.91 (~P7(f20(f19(a2)),f7(a2))), % 148.66/148.91 inference(scs_inference,[],[8514,8462,8550,7809,8533,8485,8538,8033,8117,8134,8515,8011,8457,7748,80,270,87,90,89,83,85,81,534,2,48,25,24,141,27,35,49,3,158])). % 148.66/148.91 cnf(8587,plain, % 148.66/148.91 (~E(f16(a12),f20(f4(a10)))), % 148.66/148.91 inference(scs_inference,[],[8575,534])). % 148.66/148.91 cnf(8588,plain, % 148.66/148.91 (~E(f20(a12),f16(a12))), % 148.66/148.91 inference(scs_inference,[],[8477,8575,534,2])). % 148.66/148.91 cnf(8593,plain, % 148.66/148.91 (~E(a12,f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8399,8477,8575,8580,8015,7758,7791,7735,7918,8017,534,2,141,27,35,3])). % 148.66/148.91 cnf(8595,plain, % 148.66/148.91 (P6(f16(a12),f20(f16(x85951)))), % 148.66/148.91 inference(scs_inference,[],[8399,8477,8575,8580,8015,7938,7758,7791,7735,7918,8017,534,2,141,27,35,3,7686,137])). % 148.66/148.91 cnf(8604,plain, % 148.66/148.91 (~E(f20(a13),f16(a12))), % 148.66/148.91 inference(scs_inference,[],[8519,2])). % 148.66/148.91 cnf(8605,plain, % 148.66/148.91 (P7(f7(a1),f20(f19(a1)))), % 148.66/148.91 inference(scs_inference,[],[8519,7946,80,2,141])). % 148.66/148.91 cnf(8609,plain, % 148.66/148.91 (~E(f21(a1,f4(a1)),f21(a1,a11))), % 148.66/148.91 inference(scs_inference,[],[8519,7946,7924,8575,8086,8495,80,2,141,27,35])). % 148.66/148.91 cnf(8610,plain, % 148.66/148.91 (E(f21(f4(a10),f4(a10)),f21(a12,a12))), % 148.66/148.91 inference(scs_inference,[],[8519,7946,8148,7924,8575,8137,8086,8495,80,2,141,27,35,3])). % 148.66/148.91 cnf(8613,plain, % 148.66/148.91 (E(f21(a1,f4(a1)),f4(a1))), % 148.66/148.91 inference(scs_inference,[],[54,8519,7946,8148,7893,7924,8575,8137,7922,8086,8495,80,77,55,2,141,27,35,3,178])). % 148.66/148.91 cnf(8615,plain, % 148.66/148.91 (~P7(f20(f19(a1)),f7(a1))), % 148.66/148.91 inference(scs_inference,[],[54,8519,7946,8148,7893,7924,8575,8137,7922,8086,8495,80,77,55,2,141,27,35,3,178,158])). % 148.66/148.91 cnf(8618,plain, % 148.66/148.91 (P6(f15(f16(a12)),f6(a1))), % 148.66/148.91 inference(scs_inference,[],[54,8519,7946,8565,8148,7893,7924,8575,8550,8137,7922,8086,8495,80,77,73,55,2,141,27,35,3,178,158,40,28])). % 148.66/148.91 cnf(8622,plain, % 148.66/148.91 (~E(f17(a13),f6(a1))), % 148.66/148.91 inference(scs_inference,[],[8578,2])). % 148.66/148.91 cnf(8623,plain, % 148.66/148.91 (P5(f21(a1,a12),f4(a1))), % 148.66/148.91 inference(scs_inference,[],[8578,8613,8287,2,44])). % 148.66/148.91 cnf(8627,plain, % 148.66/148.91 (~P6(f20(f19(a1)),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8578,8613,8605,8287,8511,8430,67,2,44,170,169])). % 148.66/148.91 cnf(8629,plain, % 148.66/148.91 (P5(f21(a12,a12),f21(f4(a10),f4(a10)))), % 148.66/148.91 inference(scs_inference,[],[8578,8610,8613,8605,8287,8511,8430,72,67,2,44,170,169,43])). % 148.66/148.91 cnf(8631,plain, % 148.66/148.91 (~P12(f21(a1,a12),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8578,8610,8613,8605,8287,8511,8430,7761,72,67,2,44,170,169,43,24])). % 148.66/148.91 cnf(8635,plain, % 148.66/148.91 (P6(f15(a12),f6(a1))), % 148.66/148.91 inference(scs_inference,[],[8578,8610,8613,8615,8618,8605,7936,8287,8511,8430,7952,7761,72,67,2,44,170,169,43,24,141,27])). % 148.66/148.91 cnf(8638,plain, % 148.66/148.91 (~E(f21(a1,a11),f6(a1))), % 148.66/148.91 inference(scs_inference,[],[8532,8578,8610,8613,8615,8618,8132,8605,7936,8287,8511,8430,7952,7761,585,72,67,270,2,44,170,169,43,24,141,27,35,3])). % 148.66/148.91 cnf(8639,plain, % 148.66/148.91 (P6(f21(a1,a12),f20(f4(a1)))), % 148.66/148.91 inference(scs_inference,[],[8532,8578,8610,8613,8615,8618,8132,8605,7936,8287,8511,8430,7952,7761,585,72,67,270,2,44,170,169,43,24,141,27,35,3,142])). % 148.66/148.91 cnf(8647,plain, % 148.66/148.91 (~E(f6(a1),f21(a1,a11))), % 148.66/148.91 inference(scs_inference,[],[8638,2])). % 148.66/148.91 cnf(8648,plain, % 148.66/148.91 (~P12(f21(a1,a12),f20(f16(x86481)))), % 148.66/148.91 inference(scs_inference,[],[8631,8638,7928,2,25])). % 148.66/148.91 cnf(8655,plain, % 148.66/148.91 (~E(f21(a1,f4(a1)),f19(a2))), % 148.66/148.91 inference(scs_inference,[],[8631,8638,8627,8639,8164,7928,8099,7789,8495,80,2,25,24,141,27,35])). % 148.66/148.91 cnf(8668,plain, % 148.66/148.91 (~P12(f21(a1,a12),f20(f4(a1)))), % 148.66/148.91 inference(scs_inference,[],[8593,8281,8631,8197,8090,2,171,25])). % 148.66/148.91 cnf(8669,plain, % 148.66/148.91 (P10(f21(a1,f21(a1,a12)))), % 148.66/148.91 inference(scs_inference,[],[8593,8281,8463,8631,8197,8090,73,2,171,25,141])). % 148.66/148.91 cnf(8676,plain, % 148.66/148.91 (~E(f17(a11),f16(a12))), % 148.66/148.91 inference(scs_inference,[],[8568,8593,8195,8635,8281,8463,7746,8631,8197,8550,195,8090,8166,7918,73,2,171,25,141,27,49,35,3])). % 148.66/148.91 cnf(8678,plain, % 148.66/148.91 (P6(f16(a12),f20(f4(a10)))), % 148.66/148.91 inference(scs_inference,[],[8568,8593,8195,8635,8281,8463,8145,7746,8631,8197,8550,195,8090,8166,7918,73,2,171,25,141,27,49,35,3,7686,137])). % 148.66/148.91 cnf(8693,plain, % 148.66/148.91 (E(f21(a1,f21(a1,a12)),a12)), % 148.66/148.91 inference(scs_inference,[],[8669,83,87,89,90,85,81])). % 148.66/148.91 cnf(8695,plain, % 148.66/148.91 (~E(f16(a12),f17(a11))), % 148.66/148.91 inference(scs_inference,[],[8676,8669,83,87,89,90,85,81,2])). % 148.66/148.91 cnf(8696,plain, % 148.66/148.91 (E(f16(a12),f4(a10))), % 148.66/148.91 inference(scs_inference,[],[8676,8669,8570,8678,83,87,89,90,85,81,2,166])). % 148.66/148.91 cnf(8703,plain, % 148.66/148.91 (~E(f21(a1,a12),f21(a1,a11))), % 148.66/148.91 inference(scs_inference,[],[8676,8669,8240,8570,8678,8403,8627,7924,8137,7856,80,83,87,89,90,85,81,2,166,141,27,35,3])). % 148.66/148.91 cnf(8709,plain, % 148.66/148.91 (~E(f21(a1,a11),f21(a1,a12))), % 148.66/148.91 inference(scs_inference,[],[8703,2])). % 148.66/148.91 cnf(8716,plain, % 148.66/148.91 (P7(f4(a1),f20(f6(a1)))), % 148.66/148.91 inference(scs_inference,[],[8703,8588,8270,8542,8678,8208,8550,8515,7748,7787,80,2,24,27,35,3,126,141])). % 148.66/148.91 cnf(8722,plain, % 148.66/148.91 (P6(f15(f16(a12)),f4(a10))), % 148.66/148.91 inference(scs_inference,[],[8609,8696,73,2,28])). % 148.66/148.91 cnf(8725,plain, % 148.66/148.91 (~E(f21(a1,f4(a1)),f9(a1))), % 148.66/148.91 inference(scs_inference,[],[8609,8696,8164,8575,7858,8495,73,2,28,27,35])). % 148.66/148.91 cnf(8726,plain, % 148.66/148.91 (~E(f4(a10),f17(a11))), % 148.66/148.91 inference(scs_inference,[],[8695,8609,8696,8164,8575,7858,8495,73,2,28,27,35,3])). % 148.66/148.91 cnf(8731,plain, % 148.66/148.91 (P5(f21(a12,a12),f21(a12,f4(a10)))), % 148.66/148.91 inference(scs_inference,[],[8726,8629,8148,2,44])). % 148.66/148.91 cnf(8733,plain, % 148.66/148.91 (~P6(f20(f6(a1)),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8726,8629,8716,8148,67,2,44,169])). % 148.66/148.91 cnf(8735,plain, % 148.66/148.91 (~P12(f16(x87351),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8726,8629,8716,8148,8428,7762,67,2,44,169,170])). % 148.66/148.91 cnf(8741,plain, % 148.66/148.91 (P6(f15(a12),f4(a10))), % 148.66/148.91 inference(scs_inference,[],[8726,8722,8629,8693,8716,8148,7936,8428,8097,8631,7762,72,67,2,44,169,170,43,25,27])). % 148.66/148.91 cnf(8744,plain, % 148.66/148.91 (~E(f19(a1),f21(a1,a12))), % 148.66/148.91 inference(scs_inference,[],[8709,8726,8722,8629,8334,8693,8716,8148,7936,8428,8097,8631,7762,7735,72,67,251,2,44,169,170,43,25,27,35,3])). % 148.66/148.91 cnf(8746,plain, % 148.66/148.91 (P6(f16(a12),f20(f21(a1,a12)))), % 148.66/148.91 inference(scs_inference,[],[8709,8726,8722,8629,8334,8693,8716,8148,8033,7936,8428,8097,8631,7762,7735,72,67,251,2,44,169,170,43,25,27,35,3,7686,137])). % 148.66/148.91 cnf(8752,plain, % 148.66/148.91 (~E(f21(a1,a12),f19(a1))), % 148.66/148.91 inference(scs_inference,[],[8744,2])). % 148.66/148.91 cnf(8755,plain, % 148.66/148.91 (~P12(f16(x87551),f20(f21(a1,a12)))), % 148.66/148.91 inference(scs_inference,[],[8735,8744,8024,7991,2,166,25])). % 148.66/148.91 cnf(8758,plain, % 148.66/148.91 (~E(f4(a1),f7(a2))), % 148.66/148.91 inference(scs_inference,[],[8735,8744,8520,8733,8613,8024,7950,7924,7991,7851,2,166,25,27,35,3])). % 148.66/148.91 cnf(8763,plain, % 148.66/148.91 (~E(f7(a2),f4(a1))), % 148.66/148.91 inference(scs_inference,[],[8758,2])). % 148.66/148.91 cnf(8767,plain, % 148.66/148.91 (E(f16(a12),f21(a1,a12))), % 148.66/148.91 inference(scs_inference,[],[8758,8755,7973,8746,8090,2,171,166])). % 148.66/148.91 cnf(8770,plain, % 148.66/148.91 (~P12(f16(x87701),f20(f16(x87702)))), % 148.66/148.91 inference(scs_inference,[],[8758,8755,7973,8735,8746,7928,8090,2,171,166,25])). % 148.66/148.91 cnf(8771,plain, % 148.66/148.91 (P7(f15(f21(a1,a11)),f21(a1,a11))), % 148.66/148.91 inference(scs_inference,[],[8758,8755,7973,8735,8746,7928,8087,8090,270,2,171,166,25,49])). % 148.66/148.91 cnf(8774,plain, % 148.66/148.91 (~E(f21(a1,f4(a1)),f19(a1))), % 148.66/148.91 inference(scs_inference,[],[8752,8758,8755,8361,8741,7973,8735,8746,7928,7746,8087,7761,8090,585,270,2,171,166,25,49,27,35,3])). % 148.66/148.91 cnf(8785,plain, % 148.66/148.91 (~E(f21(a1,f4(a1)),f17(a11))), % 148.66/148.91 inference(scs_inference,[],[8262,8771,8733,8521,8423,8164,8495,2,49,27,35])). % 148.66/148.91 cnf(8795,plain, % 148.66/148.91 (P6(f21(a1,a12),f20(f16(x87951)))), % 148.66/148.91 inference(scs_inference,[],[8076,8369,8595,8767,80,2,141,27])). % 148.66/148.91 cnf(8798,plain, % 148.66/148.91 (~P11(f4(a1),a1)), % 148.66/148.91 inference(scs_inference,[],[54,8604,8076,8774,8452,8369,8595,8767,8104,7922,8166,80,77,55,2,141,27,35,3,180])). % 148.66/148.91 cnf(8800,plain, % 148.66/148.91 (~E(a11,f4(a1))), % 148.66/148.91 inference(scs_inference,[],[54,8604,8076,8774,8452,8369,8595,8767,8104,7922,8166,80,77,55,2,141,27,35,3,180,316])). % 148.66/148.91 cnf(8801,plain, % 148.66/148.91 (P7(f4(a10),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[54,8604,8076,8774,8452,8369,8595,8767,8104,7922,8696,8166,80,77,55,2,141,27,35,3,180,316,7686])). % 148.66/148.91 cnf(8803,plain, % 148.66/148.91 (~P11(f21(a1,f4(a1)),a1)), % 148.66/148.91 inference(scs_inference,[],[54,8604,8076,8774,8452,8369,8595,8767,8104,8613,7922,8696,8166,80,77,55,2,141,27,35,3,180,316,7686,38,37])). % 148.66/148.91 cnf(8804,plain, % 148.66/148.91 (P6(f4(a10),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[54,8604,8076,8774,8452,8369,8595,8767,8104,8613,7922,8696,8090,8166,80,77,55,2,141,27,35,3,180,316,7686,38,37,171])). % 148.66/148.91 cnf(8813,plain, % 148.66/148.91 (E(f21(a1,a12),f16(x88131))), % 148.66/148.91 inference(scs_inference,[],[8800,8795,8648,8803,316,2,166])). % 148.66/148.91 cnf(8816,plain, % 148.66/148.91 (~P11(f16(x88161),a1)), % 148.66/148.91 inference(scs_inference,[],[8798,8800,8795,8648,8803,7990,316,2,166,37])). % 148.66/148.91 cnf(8817,plain, % 148.66/148.91 (~P7(f20(f4(a1)),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8798,8800,8795,8648,8803,8494,7990,8090,316,2,166,37,171])). % 148.66/148.91 cnf(8820,plain, % 148.66/148.91 (P18(f16(x88201),a1)), % 148.66/148.91 inference(scs_inference,[],[8798,8800,8795,8648,8803,8252,8494,7990,8090,316,2,166,37,171,39])). % 148.66/148.91 cnf(8821,plain, % 148.66/148.91 (P22(f16(x88211),a1)), % 148.66/148.91 inference(scs_inference,[],[8798,8800,8795,8648,8803,8252,8494,8256,7990,8090,316,2,166,37,171,39,41])). % 148.66/148.91 cnf(8822,plain, % 148.66/148.91 (P6(f15(f16(a12)),f21(a1,a12))), % 148.66/148.91 inference(scs_inference,[],[8798,8800,8795,8648,8803,8252,8494,8256,8767,7990,8090,73,316,2,166,37,171,39,41,28])). % 148.66/148.91 cnf(8828,plain, % 148.66/148.91 (P6(f4(a10),f20(f4(a1)))), % 148.66/148.91 inference(scs_inference,[],[8804,8798,8801,8800,8795,8648,8587,8803,8252,8494,8256,8767,8733,7737,7851,7990,7748,8090,73,316,2,166,37,171,39,41,28,49,27,35,3,137])). % 148.66/148.91 cnf(8835,plain, % 148.66/148.91 (~E(a11,f16(x88351))), % 148.66/148.91 inference(scs_inference,[],[8816,316])). % 148.66/148.91 cnf(8837,plain, % 148.66/148.91 (P24(f16(x88371),a1)), % 148.66/148.91 inference(scs_inference,[],[8813,8816,8531,8258,316,2,45])). % 148.66/148.91 cnf(8838,plain, % 148.66/148.91 (~P7(f20(a12),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8813,8816,8531,8817,8258,7748,316,2,45,48])). % 148.66/148.91 cnf(8839,plain, % 148.66/148.91 (P21(f16(x88391),a1)), % 148.66/148.91 inference(scs_inference,[],[8813,8816,8531,8817,8258,8254,7748,316,2,45,48,21])). % 148.66/148.91 cnf(8842,plain, % 148.66/148.91 (~P11(f21(a1,a12),a1)), % 148.66/148.91 inference(scs_inference,[],[8813,8816,8531,8817,8490,8258,8211,8254,7748,316,2,45,48,21,44,37])). % 148.66/148.91 cnf(8844,plain, % 148.66/148.91 (~P12(f4(a10),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8813,8816,8531,8817,8490,8258,8211,8254,8804,7748,7918,316,2,45,48,21,44,37,170])). % 148.66/148.91 cnf(8846,plain, % 148.66/148.91 (~E(f16(x88461),f21(a1,f5(a1)))), % 148.66/148.91 inference(scs_inference,[],[8813,8816,8820,8531,8817,8490,8258,8211,8254,8804,8190,7748,7918,316,2,45,48,21,44,37,170,39])). % 148.66/148.91 cnf(8848,plain, % 148.66/148.91 (~P12(f21(a1,a12),f20(f21(a1,a12)))), % 148.66/148.91 inference(scs_inference,[],[8813,8816,8820,8531,8817,8490,8623,8755,8258,8211,8254,8804,8190,7748,7918,316,2,45,48,21,44,37,170,39,43,24])). % 148.66/148.91 cnf(8851,plain, % 148.66/148.91 (P6(f16(x88511),f20(f16(x88512)))), % 148.66/148.91 inference(scs_inference,[],[8813,8816,8820,8531,8817,8490,8623,8795,8755,8258,8211,8254,8804,8190,8197,7748,7918,316,2,45,48,21,44,37,170,39,43,24,49,27])). % 148.66/148.91 cnf(8854,plain, % 148.66/148.91 (P6(f16(x88541),f20(f4(a1)))), % 148.66/148.91 inference(scs_inference,[],[8813,8622,8816,8820,8531,8817,8490,8623,8092,8795,8755,8258,8211,8254,8804,8503,8190,8197,7748,7787,7918,316,2,45,48,21,44,37,170,39,43,24,49,27,35,3,142])). % 148.66/148.91 cnf(8862,plain, % 148.66/148.91 (~E(a11,f21(a1,a12))), % 148.66/148.91 inference(scs_inference,[],[8842,316])). % 148.66/148.91 cnf(8863,plain, % 148.66/148.91 (~E(f16(x88631),a11)), % 148.66/148.91 inference(scs_inference,[],[8835,8842,316,2])). % 148.66/148.91 cnf(8865,plain, % 148.66/148.91 (P12(f16(a11),f20(a11))), % 148.66/148.91 inference(scs_inference,[],[8835,8838,8842,8097,76,316,2,48,166])). % 148.66/148.91 cnf(8868,plain, % 148.66/148.91 (~P11(f21(a1,f6(a1)),a1)), % 148.66/148.91 inference(scs_inference,[],[8835,8838,8842,8099,8097,76,316,2,48,166,37])). % 148.66/148.91 cnf(8870,plain, % 148.66/148.91 (P18(f4(a10),a1)), % 148.66/148.91 inference(scs_inference,[],[8835,8838,8842,8820,8099,8097,8696,76,316,2,48,166,37,39])). % 148.66/148.91 cnf(8877,plain, % 148.66/148.91 (~E(f21(a1,f4(a1)),f5(a1))), % 148.66/148.91 inference(scs_inference,[],[8835,8838,8842,8844,8820,8099,8627,8367,8097,7928,7856,8696,8495,7990,76,316,2,48,166,37,39,25,24,49,27,35])). % 148.66/148.91 cnf(8878,plain, % 148.66/148.91 (~E(f21(a1,a12),f19(a2))), % 148.66/148.91 inference(scs_inference,[],[8835,8838,8842,8844,8655,8820,8198,8099,8627,8367,8097,7928,7856,8696,8495,7990,76,316,2,48,166,37,39,25,24,49,27,35,3])). % 148.66/148.91 cnf(8885,plain, % 148.66/148.91 (~P7(f20(f4(a10)),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8878,8868,8838,8134,316,2,48])). % 148.66/148.91 cnf(8886,plain, % 148.66/148.91 (E(f16(x88861),f16(x88862))), % 148.66/148.91 inference(scs_inference,[],[8878,8770,8851,8868,8838,8134,316,2,48,166])). % 148.66/148.91 cnf(8889,plain, % 148.66/148.91 (~P11(f21(a1,f16(x88891)),a1)), % 148.66/148.91 inference(scs_inference,[],[8878,8770,8851,8868,8842,8838,7933,8134,316,2,48,166,37])). % 148.66/148.91 cnf(8890,plain, % 148.66/148.91 (E(f21(x88901,f16(x88902)),f21(x88901,a12))), % 148.66/148.91 inference(rename_variables,[],[7933])). % 148.66/148.91 cnf(8899,plain, % 148.66/148.91 (~E(f16(x88991),f19(a2))), % 148.66/148.91 inference(scs_inference,[],[8878,8865,8870,8822,8770,8851,8868,8397,8842,8838,7933,8890,7936,8134,8190,8631,8813,585,316,2,48,166,37,39,25,24,27,35,3])). % 148.66/148.91 cnf(8900,plain, % 148.66/148.91 (P7(a12,f20(x89001))), % 148.66/148.91 inference(scs_inference,[],[8878,8865,8870,8822,8770,8851,8868,8397,8842,8838,7933,8890,7936,8134,8190,8631,8813,7762,585,316,2,48,166,37,39,25,24,27,35,3,7686])). % 148.66/148.91 cnf(8902,plain, % 148.66/148.91 (P6(a12,f20(x89021))), % 148.66/148.91 inference(scs_inference,[],[8878,8865,8870,8822,8770,8851,8868,8200,8397,8842,8838,7933,8890,7936,8134,8190,8631,8813,7762,585,8090,316,2,48,166,37,39,25,24,27,35,3,7686,40,171])). % 148.66/148.91 cnf(8907,plain, % 148.66/148.91 (P6(f16(x89071),f20(f19(a1)))), % 148.66/148.91 inference(scs_inference,[],[8886,5069])). % 148.66/148.91 cnf(8908,plain, % 148.66/148.91 (E(f16(x89081),f16(x89082))), % 148.66/148.91 inference(rename_variables,[],[8886])). % 148.66/148.91 cnf(8910,plain, % 148.66/148.91 (E(f16(x89101),f16(x89102))), % 148.66/148.91 inference(rename_variables,[],[8886])). % 148.66/148.91 cnf(8911,plain, % 148.66/148.91 (P18(f16(x89111),a10)), % 148.66/148.91 inference(scs_inference,[],[8886,8908,8910,5069,439,2667])). % 148.66/148.91 cnf(8912,plain, % 148.66/148.91 (E(f16(x89121),f16(x89122))), % 148.66/148.91 inference(rename_variables,[],[8886])). % 148.66/148.91 cnf(8914,plain, % 148.66/148.91 (~E(f19(a2),f16(x89141))), % 148.66/148.91 inference(scs_inference,[],[8886,8908,8910,8899,8889,5069,439,2667,316,2])). % 148.66/148.91 cnf(8915,plain, % 148.66/148.91 (~P6(f20(x89151),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[8886,8908,8910,8899,8900,8889,67,5069,439,2667,316,2,169])). % 148.66/148.91 cnf(8918,plain, % 148.66/148.91 (P6(a12,f20(x89181))), % 148.66/148.91 inference(rename_variables,[],[8902])). % 148.66/148.91 cnf(8920,plain, % 148.66/148.91 (~P11(f21(a1,f21(a1,a12)),a1)), % 148.66/148.91 inference(scs_inference,[],[7855,8886,8908,8910,8899,8900,8902,8889,8025,8842,67,5069,439,2667,316,2,169,166,37])). % 148.66/148.91 cnf(8922,plain, % 148.66/148.91 (~P6(f20(x89221),f20(f21(a1,a12)))), % 148.66/148.91 inference(scs_inference,[],[7855,8886,8908,8910,8899,8900,8902,8889,8025,8842,8024,67,5069,439,2667,316,2,169,166,37,28])). % 148.66/148.91 cnf(8923,plain, % 148.66/148.91 (~P12(f16(x89231),f20(f6(a1)))), % 148.66/148.91 inference(scs_inference,[],[7855,8886,8908,8910,8912,8899,8900,8902,8536,8889,8025,8842,8024,67,5069,439,2667,316,2,169,166,37,28,24])). % 148.66/148.91 cnf(8924,plain, % 148.66/148.91 (E(f16(x89241),f16(x89242))), % 148.66/148.91 inference(rename_variables,[],[8886])). % 148.66/148.91 cnf(8927,plain, % 148.66/148.91 (~E(a12,f20(a13))), % 148.66/148.91 inference(scs_inference,[],[7855,8886,8908,8910,8912,8899,8900,8902,8918,8536,8889,8246,8025,8061,8842,8024,67,5069,439,2667,316,2,169,166,37,28,24,49,27])). % 148.66/148.91 cnf(8930,plain, % 148.66/148.91 (~E(a12,f9(a1))), % 148.66/148.91 inference(scs_inference,[],[7855,8886,8908,8910,8912,8899,8900,8902,8918,8725,8536,8889,8246,8511,8025,8061,8842,8024,7789,7851,67,5069,439,2667,316,2,169,166,37,28,24,49,27,35,3])). % 148.66/148.91 cnf(8933,plain, % 148.66/148.91 (P6(f16(x89331),f20(f21(a1,a11)))), % 148.66/148.91 inference(scs_inference,[],[7855,8886,8908,8910,8912,8924,8899,8900,8902,8918,8725,8536,8889,8246,8511,8025,8061,8842,8024,7789,7851,67,5069,439,2667,316,2,169,166,37,28,24,49,27,35,3,7706,142])). % 148.66/148.91 cnf(8935,plain, % 148.66/148.91 (~E(f16(a12),f20(x89351))), % 148.66/148.91 inference(scs_inference,[],[7855,8886,8908,8910,8912,8924,8899,8900,8902,8918,8725,8536,8889,8246,8511,8025,8061,8842,8024,7789,7851,67,5069,439,2667,316,2,169,166,37,28,24,49,27,35,3,7706,142,534])). % 148.66/148.91 cnf(8942,plain, % 148.66/148.91 (~E(f16(f21(a1,a12)),f20(x89421))), % 148.66/148.91 inference(scs_inference,[],[8922,8920,316,534])). % 148.66/148.91 cnf(8947,plain, % 148.66/148.91 (~P11(f21(a1,f4(a10)),a1)), % 148.66/148.91 inference(scs_inference,[],[8935,8927,8922,8920,8902,8137,8842,316,534,2,166,37])). % 148.66/148.91 cnf(8949,plain, % 148.66/148.91 (P18(f21(a1,a12),a10)), % 148.66/148.91 inference(scs_inference,[],[8935,8911,8927,8922,8920,8902,8137,8842,8767,316,534,2,166,37,39])). % 148.66/148.91 cnf(8953,plain, % 148.66/148.91 (P6(f15(f16(x89531)),f16(x89532))), % 148.66/148.91 inference(scs_inference,[],[8935,8911,8927,8922,8923,8920,8886,8865,8902,8137,8842,8767,73,316,534,2,166,37,39,25,28])). % 148.66/148.91 cnf(8958,plain, % 148.66/148.91 (~P12(f16(x89581),f20(f4(a10)))), % 148.66/148.91 inference(scs_inference,[],[8935,8911,8927,8933,8922,8923,8920,8886,8865,8902,8570,8137,8842,8767,80,73,316,534,2,166,37,39,25,28,141,24])). % 148.66/148.91 cnf(8968,plain, % 148.66/148.91 (~E(f21(a1,a12),a11)), % 148.66/148.91 inference(scs_inference,[],[8862,8947,316,2])). % 148.66/148.91 cnf(8974,plain, % 148.66/148.91 (~P11(a12,a1)), % 148.66/148.91 inference(scs_inference,[],[8862,8930,8947,8821,8798,8902,8696,580,316,2,166,41,37])). % 148.66/148.91 cnf(8978,plain, % 148.66/148.91 (~E(f21(a1,f21(a1,a12)),f21(a1,a11))), % 148.66/148.91 inference(scs_inference,[],[8862,8930,8958,8947,8915,8821,8798,8902,8011,8197,8696,8813,8669,580,316,2,166,41,37,28,24,35])). % 148.66/148.91 cnf(8979,plain, % 148.66/148.91 (~E(f4(a1),f17(a11))), % 148.66/148.91 inference(scs_inference,[],[8862,8930,8785,8958,8947,8915,8821,8798,8902,8613,8011,8197,8696,8813,8669,580,316,2,166,41,37,28,24,35,3])). % 148.66/148.91 cnf(8982,plain, % 148.66/148.91 (E(f21(a1,f16(x89821)),f16(x89821))), % 148.66/148.91 inference(scs_inference,[],[54,8862,8930,8785,8907,8958,8947,8915,8837,8821,8798,4962,8902,8613,8011,8197,8696,8813,8669,580,77,55,316,2,166,41,37,28,24,35,3,534,31,179])). % 148.66/148.91 cnf(8990,plain, % 148.66/148.91 (~E(a11,a12)), % 148.66/148.91 inference(scs_inference,[],[8974,316])). % 148.66/148.91 cnf(8991,plain, % 148.66/148.91 (~E(f17(a11),f4(a1))), % 148.66/148.91 inference(scs_inference,[],[8974,8979,316,2])). % 148.66/148.91 cnf(8998,plain, % 148.66/148.91 (E(f21(a1,a12),f4(a1))), % 148.66/148.91 inference(scs_inference,[],[8974,8979,8668,8839,8837,8639,8287,8511,8696,316,2,45,21,44,166])). % 148.66/148.91 cnf(9003,plain, % 148.66/148.91 (P5(f16(x90031),f21(a1,f16(x90031)))), % 148.66/148.91 inference(scs_inference,[],[8974,8979,8982,8668,8854,8839,8837,8639,8287,8511,8696,72,7990,316,2,45,21,44,166,170,43])). % 148.66/148.91 cnf(9006,plain, % 148.66/148.91 (~E(f4(a1),f20(a13))), % 148.66/148.91 inference(scs_inference,[],[8974,8979,8982,8668,8854,8839,8837,8915,8639,8542,8287,8511,8061,7928,8696,72,7990,316,2,45,21,44,166,170,43,28,27])). % 148.66/148.91 cnf(9010,plain, % 148.66/148.91 (P7(f16(x90101),f20(x90102))), % 148.66/148.91 inference(scs_inference,[],[8974,8914,8979,8982,8668,8854,8839,8015,8837,8915,8639,8542,8287,8886,8511,8061,7928,8696,72,7990,8166,316,2,45,21,44,166,170,43,28,27,35,3,7686])). % 148.66/148.91 cnf(9011,plain, % 148.66/148.91 (~E(f16(f16(x90111)),f20(x90112))), % 148.66/148.91 inference(scs_inference,[],[8974,8914,8979,8982,8668,8854,8839,8015,8837,8915,8639,8542,8287,8886,8511,8061,7928,8696,72,7990,8166,316,2,45,21,44,166,170,43,28,27,35,3,7686,534])). % 148.66/148.91 cnf(9019,plain, % 148.66/148.91 (P6(f16(x90191),f20(x90192))), % 148.66/148.91 inference(scs_inference,[],[9010,137])). % 148.66/148.91 cnf(9021,plain, % 148.66/148.91 (~E(a12,a11)), % 148.66/148.91 inference(scs_inference,[],[8990,9010,137,2])). % 148.66/148.91 cnf(9025,plain, % 148.66/148.91 (P6(f4(a1),f20(f16(x90251)))), % 148.66/148.91 inference(scs_inference,[],[8990,9010,8998,7989,8795,8902,137,2,166,27])). % 148.66/148.91 cnf(9026,plain, % 148.66/148.91 (~E(f21(a1,f16(x90261)),f7(a2))), % 148.66/148.91 inference(scs_inference,[],[8990,9010,8998,7989,8795,8902,7791,8538,137,2,166,27,35])). % 148.66/148.91 cnf(9027,plain, % 148.66/148.91 (~E(f16(x90271),f21(a1,a11))), % 148.66/148.91 inference(scs_inference,[],[8990,9010,8998,8576,7989,8795,8902,8982,7791,8538,137,2,166,27,35,3])). % 148.66/148.91 cnf(9036,plain, % 148.66/148.91 (~E(f21(a1,a11),f16(x90361))), % 148.66/148.91 inference(scs_inference,[],[9027,2])). % 148.66/148.91 cnf(9039,plain, % 148.66/148.91 (P6(f16(x90391),f20(x90392))), % 148.66/148.91 inference(rename_variables,[],[9019])). % 148.66/148.91 cnf(9041,plain, % 148.66/148.91 (~E(f16(x90411),f20(a13))), % 148.66/148.91 inference(scs_inference,[],[9019,9039,9027,8885,8801,8061,2,48,166,27])). % 148.66/148.91 cnf(9044,plain, % 148.66/148.91 (~E(f7(a2),f21(a1,a12))), % 148.66/148.91 inference(scs_inference,[],[9019,9039,9027,8763,8885,8998,8132,8801,8061,7787,2,48,166,27,35,3])). % 148.66/148.91 cnf(9054,plain, % 148.66/148.91 (P6(f15(f16(x90541)),f6(a1))), % 148.66/148.91 inference(scs_inference,[],[9021,9041,8953,8902,8550,2,166,28])). % 148.66/148.91 cnf(9055,plain, % 148.66/148.91 (P6(f15(f16(x90551)),f16(x90552))), % 148.66/148.91 inference(rename_variables,[],[8953])). % 148.66/148.91 cnf(9056,plain, % 148.66/148.91 (P6(f15(a12),f16(x90561))), % 148.66/148.91 inference(scs_inference,[],[9021,9041,8953,9055,7936,8902,8550,2,166,28,27])). % 148.66/148.91 cnf(9058,plain, % 148.66/148.91 (~E(f21(a1,f4(a1)),f7(a1))), % 148.66/148.91 inference(scs_inference,[],[9021,9041,8953,9055,7936,7952,8902,8550,8495,2,166,28,27,35])). % 148.66/148.91 cnf(9059,plain, % 148.66/148.91 (~E(a12,f7(a2))), % 148.66/148.91 inference(scs_inference,[],[9021,9041,8953,9055,9026,8565,7936,7952,8902,8550,8495,2,166,28,27,35,3])). % 148.66/148.91 cnf(9066,plain, % 148.66/148.91 (~E(f21(a1,a12),f7(a2))), % 148.66/148.91 inference(scs_inference,[],[9044,2])). % 148.66/148.91 cnf(9077,plain, % 148.66/148.91 (~E(f19(a1),f16(x90771))), % 148.66/148.91 inference(scs_inference,[],[9036,9044,8863,9025,9019,8911,8195,8844,8134,8550,7735,80,251,2,166,39,25,141,35,3])). % 148.66/148.91 cnf(9078,plain, % 148.66/148.91 (P7(f4(a1),f20(x90781))), % 148.66/148.91 inference(scs_inference,[],[9036,9044,8863,9025,9019,8911,8195,8844,8134,8550,7735,7990,80,251,2,166,39,25,141,35,3,7686])). % 148.66/148.91 cnf(9079,plain, % 148.66/148.91 (P6(f4(a1),f20(x90791))), % 148.66/148.91 inference(scs_inference,[],[9036,9044,8863,9025,9019,8911,8195,8844,8134,8550,7735,7990,8090,80,251,2,166,39,25,141,35,3,7686,171])). % 148.66/148.91 cnf(9085,plain, % 148.66/148.91 (~E(f16(x90851),f19(a1))), % 148.66/148.91 inference(scs_inference,[],[9077,2])). % 148.66/148.91 cnf(9086,plain, % 148.66/148.91 (~P6(f20(x90861),f20(f6(a1)))), % 148.66/148.91 inference(scs_inference,[],[9077,9078,7787,2,169])). % 148.66/148.91 cnf(9091,plain, % 148.66/148.91 (~E(f21(a1,f4(a10)),f9(a1))), % 148.66/148.91 inference(scs_inference,[],[7850,9077,9078,9079,7858,8371,7787,2,169,166,35])). % 148.66/148.91 cnf(9092,plain, % 148.66/148.91 (~E(f4(a1),f5(a1))), % 148.66/148.91 inference(scs_inference,[],[7850,9077,9078,9079,8877,7858,8613,8371,7787,2,169,166,35,3])). % 148.66/148.91 cnf(9097,plain, % 148.66/148.91 (~E(f20(a13),f4(a1))), % 148.66/148.91 inference(scs_inference,[],[9006,2])). % 148.66/148.91 cnf(9100,plain, % 148.66/148.91 (~P12(f6(a1),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[9006,8731,7760,8164,8017,2,44,170])). % 148.66/148.91 cnf(9107,plain, % 148.66/148.91 (~P11(f15(f20(a12)),a1)), % 148.66/148.91 inference(scs_inference,[],[9006,9085,8731,8204,7760,8094,9019,8974,8164,72,8017,2,44,170,166,43,37])). % 148.66/148.91 cnf(9109,plain, % 148.66/148.91 (~E(f17(a11),f21(a1,a12))), % 148.66/148.91 inference(scs_inference,[],[9006,9085,8991,8731,8204,8270,7760,8094,9019,8998,8974,8164,72,585,8017,2,44,170,166,43,37,35,3])). % 148.66/148.91 cnf(9115,plain, % 148.66/148.91 (~E(f21(a1,a12),f17(a11))), % 148.66/148.91 inference(scs_inference,[],[9109,2])). % 148.66/148.91 cnf(9119,plain, % 148.66/148.91 (~P12(f6(a1),f20(f21(a1,a12)))), % 148.66/148.91 inference(scs_inference,[],[9109,9092,9100,9079,8024,2,166,25])). % 148.66/148.91 cnf(9120,plain, % 148.66/148.91 (~E(f21(a1,f6(a1)),f21(a1,a11))), % 148.66/148.91 inference(scs_inference,[],[9109,9092,9100,9079,8086,8024,8289,2,166,25,35])). % 148.66/148.91 cnf(9121,plain, % 148.66/148.91 (~E(f21(a1,a12),f7(a1))), % 148.66/148.91 inference(scs_inference,[],[9109,9092,9100,9058,9079,8198,8086,8024,8289,2,166,25,35,3])). % 148.66/148.91 cnf(9124,plain, % 148.66/148.91 (P6(f15(f4(a1)),f16(x91241))), % 148.66/148.91 inference(scs_inference,[],[9056,9109,9092,9100,9058,9107,9079,8198,8086,8024,7746,8289,2,166,25,35,3,38,27])). % 148.66/148.91 cnf(9129,plain, % 148.66/148.91 (~E(f7(a1),f21(a1,a12))), % 148.66/148.91 inference(scs_inference,[],[9121,2])). % 148.66/148.91 cnf(9130,plain, % 148.66/148.91 (P12(a12,f20(f7(a2)))), % 148.66/148.91 inference(scs_inference,[],[9121,9059,8902,2,166])). % 148.66/148.91 cnf(9135,plain, % 148.66/148.91 (~E(f4(a1),f7(a1))), % 148.66/148.91 inference(scs_inference,[],[9121,9059,8334,9100,8998,8902,8197,67,2,166,25,35,3])). % 148.66/148.91 cnf(9141,plain, % 148.66/148.91 (~E(f7(a1),f4(a1))), % 148.66/148.91 inference(scs_inference,[],[9135,2])). % 148.66/148.91 cnf(9149,plain, % 148.66/148.91 (~E(f21(a1,a12),f9(a1))), % 148.66/148.91 inference(scs_inference,[],[9135,9124,9091,9130,9079,8423,8137,7851,7762,580,2,166,28,24,35,3])). % 148.66/148.91 cnf(9156,plain, % 148.66/148.91 (~E(f9(a1),f21(a1,a12))), % 148.66/148.91 inference(scs_inference,[],[9149,2])). % 148.66/148.91 cnf(9169,plain, % 148.66/148.91 (~P7(f20(f21(a1,a11)),f21(a1,a11))), % 148.66/148.91 inference(scs_inference,[],[8949,9129,9149,8828,7741,8361,8099,7761,8166,80,251,2,39,141,35,3,158,115,49])). % 148.66/148.91 cnf(9180,plain, % 148.66/148.91 (~P6(f20(f21(a1,a11)),f19(a1))), % 148.66/148.91 inference(scs_inference,[],[9011,9169,8846,8025,7950,8011,8631,8767,8669,270,2,35,3,24,141,28])). % 148.66/148.91 cnf(9181,plain, % 148.66/148.91 (~P7(f20(f21(a1,a11)),a11)), % 148.66/148.91 inference(scs_inference,[],[9011,9169,8846,8025,7950,8011,8631,8767,8669,270,2,35,3,24,141,28,303])). % 148.66/148.91 cnf(9194,plain, % 148.66/148.91 (~P12(f4(a1),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[9120,9079,579,2,170])). % 148.66/148.91 cnf(9206,plain, % 148.66/148.91 (~P12(a12,f20(a12))), % 148.66/148.91 inference(scs_inference,[],[9156,9120,9003,8207,8452,9100,8565,9079,8974,7933,8097,72,7735,7918,579,580,2,170,44,37,35,43,25,3,24])). % 148.66/148.91 cnf(9207,plain, % 148.66/148.91 (P7(f17(a11),f20(a11))), % 148.66/148.91 inference(scs_inference,[],[9156,9120,9003,8207,7920,8452,9100,8565,9079,8974,7933,8097,72,7735,7918,80,579,580,2,170,44,37,35,43,25,3,24,141])). % 148.66/148.91 cnf(9211,plain, % 148.66/148.91 (~P7(f20(a11),f17(a11))), % 148.66/148.91 inference(scs_inference,[],[9156,9120,9003,9054,8207,7920,8452,9100,8565,9079,8974,7933,8097,72,7735,7918,8017,80,579,580,2,170,44,37,35,43,25,3,24,141,28,158])). % 148.66/148.91 cnf(9213,plain, % 148.66/148.91 (~E(a11,f4(a10))), % 148.66/148.91 inference(scs_inference,[],[9156,9120,9003,9054,8207,7920,8452,9100,8565,9079,8974,7933,8097,72,7735,7918,8017,80,579,580,2,170,44,37,35,43,25,3,24,141,28,158,316])). % 148.66/148.91 cnf(9219,plain, % 148.66/148.91 (~E(f21(a1,f16(x92191)),f17(a13))), % 148.66/148.91 inference(scs_inference,[],[9213,7737,8538,2,35])). % 148.66/148.91 cnf(9220,plain, % 148.66/148.91 (P6(f21(a1,a12),f20(x92201))), % 148.66/148.91 inference(scs_inference,[],[9213,9019,7737,8767,8538,2,35,27])). % 148.66/148.91 cnf(9224,plain, % 148.66/148.91 (~P12(f4(a1),f20(f4(a10)))), % 148.66/148.91 inference(scs_inference,[],[9194,9207,9213,8170,9019,7737,8134,8767,8538,2,35,27,49,25])). % 148.66/148.91 cnf(9227,plain, % 148.66/148.91 (~E(f16(x92271),f20(x92272))), % 148.66/148.91 inference(scs_inference,[],[9066,9194,9207,9213,8942,8170,9019,7737,8134,8886,8767,8538,2,35,27,49,25,166,3])). % 148.66/148.91 cnf(9232,plain, % 148.66/148.91 (~E(f20(f20(a11)),f17(a11))), % 148.66/148.91 inference(scs_inference,[],[9066,9194,9207,9211,9206,9213,8942,8395,8170,9019,7737,8423,8134,8886,8767,8538,8090,2,35,27,49,25,166,3,24,141,28])). % 148.66/148.91 cnf(9237,plain, % 148.66/148.91 (~E(a11,f6(a1))), % 148.66/148.91 inference(scs_inference,[],[55,9066,9194,9207,9211,9206,9213,8942,8395,8344,8170,9019,7815,7737,8423,8134,8886,8767,8538,8090,77,54,2,35,27,49,25,166,3,24,141,28,180,565,316])). % 148.66/148.91 cnf(9244,plain, % 148.66/148.91 (~P7(f20(f21(a1,a12)),f20(a12))), % 148.66/148.91 inference(scs_inference,[],[9227,8092,8838,8024,67,2,35,48])). % 148.66/148.91 cnf(9245,plain, % 148.66/148.91 (~P12(f4(a1),f20(f21(a1,a12)))), % 148.66/148.91 inference(scs_inference,[],[9227,9194,8092,8838,8024,67,2,35,48,25])). % 148.66/148.91 cnf(9247,plain, % 148.66/148.91 (~E(f16(x92471),f20(x92472))), % 148.66/148.91 inference(rename_variables,[],[9227])). % 148.66/148.91 cnf(9250,plain, % 148.66/148.91 (~E(f6(a1),f20(x92501))), % 148.66/148.91 inference(scs_inference,[],[9227,9247,9194,8092,8838,9019,8024,8550,67,2,35,48,25,166,3])). % 148.66/148.91 cnf(9252,plain, % 148.66/148.91 (~P12(a12,f20(f4(a10)))), % 148.66/148.91 inference(scs_inference,[],[9227,9247,9224,9194,8092,8838,9019,8024,8550,67,580,2,35,48,25,166,3,24])). % 148.66/148.91 cnf(9253,plain, % 148.66/148.91 (P7(f21(a1,a12),f20(x92531))), % 148.66/148.91 inference(scs_inference,[],[9220,9227,9247,9224,9194,8092,8838,9019,8024,8550,67,80,580,2,35,48,25,166,3,24,141])). % 148.66/148.91 cnf(9260,plain, % 148.66/148.91 (~E(f6(a1),a11)), % 148.66/148.91 inference(scs_inference,[],[9237,2])). % 148.66/148.91 cnf(9261,plain, % 148.66/148.91 (~E(f21(a1,f4(a1)),a13)), % 148.66/148.91 inference(scs_inference,[],[9237,79,8495,2,35])). % 148.66/148.91 cnf(9265,plain, % 148.66/148.91 (~E(f21(a1,a12),f17(a13))), % 148.66/148.91 inference(scs_inference,[],[9237,9115,9219,9220,7933,79,8495,2,35,166,3])). % 148.66/148.91 cnf(9272,plain, % 148.66/148.91 (~E(f21(a1,a12),f17(f20(x92721)))), % 148.66/148.91 inference(scs_inference,[],[9250,8397,8166,2,35])). % 148.66/148.91 cnf(9276,plain, % 148.66/148.91 (~E(a12,f20(x92761))), % 148.66/148.91 inference(scs_inference,[],[9250,9265,9220,8397,8166,8017,2,35,166,3])). % 148.66/148.91 cnf(9294,plain, % 148.66/148.91 (~E(f21(a1,a12),a13)), % 148.66/148.91 inference(scs_inference,[],[8968,9276,9261,9180,7811,9220,8198,7789,8371,2,35,171,166,3])). % 148.66/148.91 cnf(9296,plain, % 148.66/148.91 (~P6(f20(f21(a1,a11)),a11)), % 148.66/148.91 inference(scs_inference,[],[8968,9276,9181,9261,9180,7811,9220,8198,7789,8371,3710,2,35,171,166,3,141])). % 148.66/148.91 cnf(9305,plain, % 148.66/148.91 (~E(a13,f21(a1,a12))), % 148.66/148.91 inference(scs_inference,[],[9294,2])). % 148.66/148.91 cnf(9309,plain, % 148.66/148.91 (P12(f21(a1,a12),f20(a13))), % 148.66/148.91 inference(scs_inference,[],[9294,8249,7926,9220,72,7787,2,35,43,166])). % 148.66/148.91 cnf(9312,plain, % 148.66/148.91 (~E(f20(a13),f21(a1,a12))), % 148.66/148.91 inference(scs_inference,[],[9097,9294,8249,7926,9220,8998,72,7787,2,35,43,166,3])). % 148.66/148.91 cnf(9323,plain, % 148.66/148.91 (P6(f6(a1),f20(x93231))), % 148.66/148.91 inference(scs_inference,[],[9312,7791,9019,8550,8289,2,35,27])). % 148.66/148.91 cnf(9324,plain, % 148.66/148.91 (P6(f16(x93241),f20(x93242))), % 148.66/148.91 inference(rename_variables,[],[9019])). % 148.66/148.91 cnf(9325,plain, % 148.66/148.91 (P12(f16(x93251),f20(f17(a13)))), % 148.66/148.91 inference(scs_inference,[],[9312,8514,7791,9019,9324,8550,8289,2,35,27,166])). % 148.66/148.91 cnf(9328,plain, % 148.66/148.91 (~E(f16(x93281),f17(f20(x93282)))), % 148.66/148.91 inference(scs_inference,[],[9312,9272,8514,7791,9019,9324,8550,8813,8289,2,35,27,166,3])). % 148.66/148.91 cnf(9329,plain, % 148.66/148.91 (~P12(f6(a1),f20(f4(a10)))), % 148.66/148.91 inference(scs_inference,[],[9312,9272,9252,8514,7791,9019,9324,8550,8813,8289,8017,2,35,27,166,3,24])). % 148.66/148.91 cnf(9344,plain, % 148.66/148.91 (~P12(a12,f20(f4(a1)))), % 148.66/148.91 inference(scs_inference,[],[8647,9323,9305,8088,8848,9309,9244,9253,8015,58,8099,8902,585,580,2,35,48,25,166,3,23,170])). % 148.66/148.91 cnf(9353,plain, % 148.66/148.91 (P12(f6(a1),f20(a11))), % 148.66/148.91 inference(scs_inference,[],[9260,8115,9323,7856,7851,2,35,166])). % 148.66/148.91 cnf(9384,plain, % 148.66/148.91 (~P12(f4(a10),f20(f4(a1)))), % 148.66/148.91 inference(scs_inference,[],[8978,9328,9344,8550,7918,2,3,24])). % 148.66/148.91 cnf(9387,plain, % 148.66/148.91 (~E(f21(a1,f21(a1,a12)),f9(a1))), % 148.66/148.91 inference(scs_inference,[],[8978,9328,9344,9296,7920,7858,8550,8669,7918,2,3,24,171,35])). % 148.66/148.91 cnf(9424,plain, % 148.66/148.91 (E(f4(a10),f4(a1))), % 148.66/148.91 inference(scs_inference,[],[8120,9384,8828,2,166])). % 148.66/148.91 cnf(9426,plain, % 148.66/148.91 (~E(f4(a10),f19(a2))), % 148.66/148.91 inference(scs_inference,[],[8120,9384,8899,8828,8696,2,166,3])). % 148.66/148.91 cnf(9429,plain, % 148.66/148.91 (P6(f21(a1,f4(a1)),f20(x94291))), % 148.66/148.91 inference(scs_inference,[],[8120,9384,8899,9344,8828,9220,7761,8696,579,2,166,3,24,27])). % 148.66/148.91 cnf(9432,plain, % 148.66/148.91 (P7(f6(a1),f20(x94321))), % 148.66/148.91 inference(scs_inference,[],[8120,9384,8899,9344,9323,8828,7950,9220,7761,8696,8538,80,579,2,166,3,24,27,35,141])). % 148.66/148.91 cnf(9444,plain, % 148.66/148.91 (~E(f7(a1),f4(a10))), % 148.66/148.91 inference(scs_inference,[],[9141,9424,9426,8578,9323,2,166,3])). % 148.66/148.91 cnf(9450,plain, % 148.66/148.91 (~E(f20(a11),f20(f21(a1,a12)))), % 148.66/148.91 inference(scs_inference,[],[9432,9141,9424,9426,9119,9353,9245,8578,8270,8463,9323,8838,7928,8166,2,166,3,24,35,49,48,25])). % 148.66/148.91 cnf(9454,plain, % 148.66/148.91 (~E(f4(a10),f7(a1))), % 148.66/148.91 inference(scs_inference,[],[9444,2])). % 148.66/148.91 cnf(9458,plain, % 148.66/148.91 (~E(f4(a10),f19(a1))), % 148.66/148.91 inference(scs_inference,[],[9444,9429,9085,8696,80,2,141,3])). % 148.66/148.91 cnf(9466,plain, % 148.66/148.91 (~E(f19(a1),f4(a10))), % 148.66/148.91 inference(scs_inference,[],[9458,2])). % 148.66/148.91 cnf(9481,plain, % 148.66/148.91 (P7(f18(a1),f20(f19(a1)))), % 148.66/148.91 inference(scs_inference,[],[9232,8695,7811,9019,80,2,166,141])). % 148.66/148.91 cnf(9484,plain, % 148.66/148.91 (~E(f16(x94841),f17(a11))), % 148.66/148.91 inference(scs_inference,[],[9232,8695,7811,9019,8886,80,2,166,141,3])). % 148.66/148.91 cnf(9497,plain, % 148.66/148.91 (~E(f21(a1,a11),f4(a10))), % 148.66/148.91 inference(scs_inference,[],[9484,9466,9019,270,2,166,3])). % 148.66/148.91 cnf(9509,plain, % 148.66/148.91 (~E(a12,f7(a1))), % 148.66/148.91 inference(scs_inference,[],[9497,9454,7866,7918,80,2,141,3])). % 148.66/148.91 cnf(9510,plain, % 148.66/148.91 (P6(f4(a10),f20(x95101))), % 148.66/148.91 inference(scs_inference,[],[9497,9454,7866,9019,8696,7918,80,2,141,3,27])). % 148.66/148.91 cnf(9521,plain, % 148.66/148.91 (~E(f7(a1),a12)), % 148.66/148.91 inference(scs_inference,[],[9509,2])). % 148.66/148.91 cnf(9606,plain, % 148.66/148.91 (P7(x96061,f20(x96061))), % 148.66/148.91 inference(scs_inference,[],[9387,9149,9220,8090,80,2,166,141])). % 148.66/148.91 cnf(9619,plain, % 148.66/148.91 (~P7(f20(x96191),x96191)), % 148.66/148.91 inference(scs_inference,[],[9606,158])). % 148.66/148.91 cnf(9993,plain, % 148.66/148.91 (~E(f21(a1,f6(a1)),a13)), % 148.66/148.91 inference(scs_inference,[],[9450,9521,8565,79,8289,2,3,35])). % 148.66/148.91 cnf(9997,plain, % 148.66/148.91 (~E(f21(a1,f16(x99971)),f5(a1))), % 148.66/148.91 inference(scs_inference,[],[8378,2])). % 148.66/148.91 cnf(9998,plain, % 148.66/148.91 (~E(f6(a1),a13)), % 148.66/148.91 inference(scs_inference,[],[8378,9993,8503,2,3])). % 148.66/148.91 cnf(10003,plain, % 148.66/148.91 (~E(f4(a1),f9(a1))), % 148.66/148.91 inference(scs_inference,[],[9998,8930,580,2,3])). % 148.66/148.91 cnf(10004,plain, % 148.66/148.91 (P12(f6(a1),f20(a13))), % 148.66/148.91 inference(scs_inference,[],[9998,8930,9323,580,2,3,166])). % 148.66/148.91 cnf(10018,plain, % 148.66/148.91 (~E(f20(a13),f20(f4(a10)))), % 148.66/148.91 inference(scs_inference,[],[10003,10004,9997,9329,7934,8982,9079,72,2,3,166,43,25])). % 148.66/148.91 cnf(10072,plain, % 148.66/148.91 (~P12(x100721,f20(x100721))), % 148.66/148.91 inference(scs_inference,[],[7918,8090,8902,8696,8455,9619,10018,142,7,160,2,438,6011,192])). % 148.66/148.91 cnf(10121,plain, % 148.66/148.91 (~P7(f20(x101211),f20(f21(a1,a12)))), % 148.66/148.91 inference(scs_inference,[],[8017,9019,8550,8915,8922,8533,6557,142,565,160,2,438,6011,137])). % 148.66/148.91 cnf(10126,plain, % 148.66/148.91 (~P7(f20(x101261),x101261)), % 148.66/148.91 inference(rename_variables,[],[9619])). % 148.66/148.91 cnf(10128,plain, % 148.66/148.91 (P6(f15(x101281),x101281)), % 148.66/148.91 inference(rename_variables,[],[73])). % 148.66/148.91 cnf(10130,plain, % 148.66/148.91 (P6(f15(x101301),x101301)), % 148.66/148.91 inference(rename_variables,[],[73])). % 148.66/148.91 cnf(10133,plain, % 148.66/148.91 (P6(f15(x101331),x101331)), % 148.66/148.91 inference(rename_variables,[],[73])). % 148.66/148.91 cnf(10136,plain, % 148.66/148.91 (P6(f15(x101361),x101361)), % 148.66/148.91 inference(rename_variables,[],[73])). % 148.66/148.91 cnf(10139,plain, % 148.66/148.91 (P6(f15(x101391),x101391)), % 148.66/148.91 inference(rename_variables,[],[73])). % 148.66/148.91 cnf(10145,plain, % 148.66/148.91 (P6(f15(x101451),x101451)), % 148.66/148.91 inference(rename_variables,[],[73])). % 148.66/148.91 cnf(10167,plain, % 148.66/148.91 (E(f21(a1,a11),a11)), % 148.66/148.91 inference(scs_inference,[],[54,251,73,10128,10130,10133,10136,10139,10145,77,3710,8017,70,8696,9019,55,9323,8550,7761,295,9429,8190,3503,8455,7996,8755,8915,8629,9521,9619,10126,290,9329,9325,8953,8922,8533,6557,10072,8273,7805,142,565,160,2,438,6011,137,314,48,27,143,152,171,145,166,169,3,141,25,44,28,39,149,43,179,7,6283])). % 148.66/148.91 cnf(10189,plain, % 148.66/148.91 (~P7(f20(x101891),x101891)), % 148.66/148.91 inference(rename_variables,[],[9619])). % 148.66/148.91 cnf(10195,plain, % 148.66/148.91 (~P6(f20(f20(x101951)),f20(x101951))), % 148.66/148.91 inference(scs_inference,[],[80,7993,9019,9510,7762,7990,9521,9619,10189,8922,9606,8923,10121,9086,142,160,2,438,6011,137,48,166,3,141])). % 148.66/148.91 cnf(10345,plain, % 148.66/148.91 (P5(f3(a1),f19(a1))), % 148.66/148.91 inference(scs_inference,[],[7813,7973,142,160])). % 148.66/148.91 cnf(10349,plain, % 148.66/148.91 (~P7(f20(x103491),x103491)), % 148.66/148.91 inference(rename_variables,[],[9619])). % 148.66/148.91 cnf(10352,plain, % 148.66/148.91 (~E(f20(f20(x103521)),x103521)), % 148.66/148.91 inference(scs_inference,[],[9619,10349,7813,8137,7809,10195,9606,7973,9481,142,160,2,48,27,49])). % 148.66/148.91 cnf(10924,plain, % 148.66/148.91 ($false), % 148.66/148.91 inference(scs_inference,[],[270,10352,8106,10072,8122,7795,10345,10167,8045,2,3,25,43,44,21,7]), % 148.66/148.91 ['proof']). % 148.66/148.91 % SZS output end Proof % 148.66/148.91 % Total time :148.030000s %------------------------------------------------------------------------------