%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP653+1 : TPTP v8.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 06:40:19 EDT 2024 % Result : Theorem 63.63s 63.79s % Output : CNFRefutation 63.79s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : GRP653+1 : TPTP v8.2.0. Released v3.4.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n019.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Jun 20 13:09:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.53/0.57 start to proof:theBenchmark % 63.63/63.76 %------------------------------------------- % 63.63/63.76 % File :CSE---1.7 % 63.63/63.76 % Problem :theBenchmark % 63.63/63.76 % Transform :cnf % 63.63/63.76 % Format :tptp:raw % 63.63/63.76 % Command :java -jar mcs_scs.jar %d %s % 63.63/63.76 % 63.63/63.76 % Result :Theorem 63.040000s % 63.63/63.76 % Output :CNFRefutation 63.040000s % 63.63/63.76 %------------------------------------------- % 63.63/63.77 %------------------------------------------------------------------------------ % 63.63/63.77 % File : GRP653+1 : TPTP v8.2.0. Released v3.4.0. % 63.63/63.77 % Domain : Group Theory % 63.63/63.77 % Problem : On the Lattice of Subgroups of a Group T38 % 63.63/63.77 % Version : [Urb08] axioms : Especial. % 63.63/63.77 % English : % 63.63/63.77 % 63.63/63.78 % Refs : [Gan96] Ganczarski (1996), On the Lattice of Subgroups of a Gr % 63.63/63.78 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 63.63/63.78 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 63.63/63.78 % Source : [Urb08] % 63.63/63.78 % Names : t38_latsubgr [Urb08] % 63.63/63.78 % 63.63/63.78 % Status : Theorem % 63.63/63.78 % Rating : 0.25 v8.2.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.20 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.22 v7.0.0, 0.20 v6.4.0, 0.23 v6.3.0, 0.33 v6.2.0, 0.32 v6.1.0, 0.33 v6.0.0, 0.22 v5.5.0, 0.30 v5.4.0, 0.32 v5.3.0, 0.44 v5.2.0, 0.35 v5.1.0, 0.38 v4.1.0, 0.39 v4.0.0, 0.42 v3.7.0, 0.45 v3.5.0, 0.47 v3.4.0 % 63.63/63.78 % Syntax : Number of formulae : 66 ( 20 unt; 0 def) % 63.63/63.78 % Number of atoms : 277 ( 7 equ) % 63.63/63.78 % Maximal formula atoms : 16 ( 4 avg) % 63.63/63.78 % Number of connectives : 258 ( 47 ~; 1 |; 151 &) % 63.63/63.78 % ( 3 <=>; 56 =>; 0 <=; 0 <~>) % 63.63/63.78 % Maximal formula depth : 15 ( 5 avg) % 63.63/63.78 % Maximal term depth : 3 ( 1 avg) % 63.63/63.78 % Number of predicates : 36 ( 34 usr; 1 prp; 0-3 aty) % 63.63/63.78 % Number of functors : 9 ( 9 usr; 1 con; 0-3 aty) % 63.63/63.78 % Number of variables : 123 ( 103 !; 20 ?) % 63.63/63.78 % SPC : FOF_THM_RFO_SEQ % 63.63/63.78 % 63.63/63.78 % Comments : Normal version: includes the axioms (which may be theorems from % 63.63/63.78 % other articles) and background that are possibly necessary. % 63.63/63.78 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 63.63/63.78 % : The problem encoding is based on set theory. % 63.63/63.78 %------------------------------------------------------------------------------ % 63.63/63.78 fof(t38_latsubgr,conjecture, % 63.63/63.78 ! [A] : % 63.63/63.78 ( ( ~ v3_struct_0(A) % 63.63/63.78 & v3_group_1(A) % 63.63/63.78 & v4_group_1(A) % 63.63/63.78 & l1_group_1(A) ) % 63.63/63.78 => ! [B] : % 63.63/63.78 ( ( ~ v3_struct_0(B) % 63.63/63.78 & v3_group_1(B) % 63.63/63.78 & v4_group_1(B) % 63.63/63.78 & l1_group_1(B) ) % 63.63/63.78 => ! [C] : % 63.63/63.78 ( ( v1_funct_1(C) % 63.63/63.78 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 63.63/63.78 & v1_group_6(C,A,B) % 63.63/63.78 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) % 63.63/63.78 => ( v2_funct_1(C) % 63.63/63.78 => m1_lattice4(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B)) ) ) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(abstractness_v3_lattices,axiom, % 63.63/63.78 ! [A] : % 63.63/63.78 ( l3_lattices(A) % 63.63/63.78 => ( v3_lattices(A) % 63.63/63.78 => A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(antisymmetry_r2_hidden,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ( r2_hidden(A,B) % 63.63/63.78 => ~ r2_hidden(B,A) ) ). % 63.63/63.78 % 63.63/63.78 fof(cc1_funct_2,axiom, % 63.63/63.78 ! [A,B,C] : % 63.63/63.78 ( m1_relset_1(C,A,B) % 63.63/63.78 => ( ( v1_funct_1(C) % 63.63/63.78 & v1_partfun1(C,A,B) ) % 63.63/63.78 => ( v1_funct_1(C) % 63.63/63.78 & v1_funct_2(C,A,B) ) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(cc1_relset_1,axiom, % 63.63/63.78 ! [A,B,C] : % 63.63/63.78 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 63.63/63.78 => v1_relat_1(C) ) ). % 63.63/63.78 % 63.63/63.78 fof(cc5_funct_2,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ( ~ v1_xboole_0(B) % 63.63/63.78 => ! [C] : % 63.63/63.78 ( m1_relset_1(C,A,B) % 63.63/63.78 => ( ( v1_funct_1(C) % 63.63/63.78 & v1_funct_2(C,A,B) ) % 63.63/63.78 => ( v1_funct_1(C) % 63.63/63.78 & v1_partfun1(C,A,B) % 63.63/63.78 & v1_funct_2(C,A,B) ) ) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(cc6_funct_2,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ( ( ~ v1_xboole_0(A) % 63.63/63.78 & ~ v1_xboole_0(B) ) % 63.63/63.78 => ! [C] : % 63.63/63.78 ( m1_relset_1(C,A,B) % 63.63/63.78 => ( ( v1_funct_1(C) % 63.63/63.78 & v1_funct_2(C,A,B) ) % 63.63/63.78 => ( v1_funct_1(C) % 63.63/63.78 & ~ v1_xboole_0(C) % 63.63/63.78 & v1_partfun1(C,A,B) % 63.63/63.78 & v1_funct_2(C,A,B) ) ) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(dt_g3_lattices,axiom, % 63.63/63.78 ! [A,B,C] : % 63.63/63.78 ( ( v1_funct_1(B) % 63.63/63.78 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 63.63/63.78 & m1_relset_1(B,k2_zfmisc_1(A,A),A) % 63.63/63.78 & v1_funct_1(C) % 63.63/63.78 & v1_funct_2(C,k2_zfmisc_1(A,A),A) % 63.63/63.78 & m1_relset_1(C,k2_zfmisc_1(A,A),A) ) % 63.63/63.78 => ( v3_lattices(g3_lattices(A,B,C)) % 63.63/63.78 & l3_lattices(g3_lattices(A,B,C)) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(dt_k11_group_4,axiom, % 63.63/63.78 ! [A] : % 63.63/63.78 ( ( ~ v3_struct_0(A) % 63.63/63.78 & v3_group_1(A) % 63.63/63.78 & v4_group_1(A) % 63.63/63.78 & l1_group_1(A) ) % 63.63/63.78 => ( ~ v3_struct_0(k11_group_4(A)) % 63.63/63.78 & v3_lattices(k11_group_4(A)) % 63.63/63.78 & v10_lattices(k11_group_4(A)) % 63.63/63.78 & l3_lattices(k11_group_4(A)) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(dt_k1_xboole_0,axiom, % 63.63/63.78 $true ). % 63.63/63.78 % 63.63/63.78 fof(dt_k1_zfmisc_1,axiom, % 63.63/63.78 $true ). % 63.63/63.78 % 63.63/63.78 fof(dt_k2_zfmisc_1,axiom, % 63.63/63.78 $true ). % 63.63/63.78 % 63.63/63.78 fof(dt_k3_latsubgr,axiom, % 63.63/63.78 ! [A,B,C] : % 63.63/63.78 ( ( ~ v3_struct_0(A) % 63.63/63.78 & v3_group_1(A) % 63.63/63.78 & v4_group_1(A) % 63.63/63.78 & l1_group_1(A) % 63.63/63.78 & ~ v3_struct_0(B) % 63.63/63.78 & v3_group_1(B) % 63.63/63.78 & v4_group_1(B) % 63.63/63.78 & l1_group_1(B) % 63.63/63.78 & v1_funct_1(C) % 63.63/63.78 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 63.63/63.78 & m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) % 63.63/63.78 => ( v1_funct_1(k3_latsubgr(A,B,C)) % 63.63/63.78 & v1_funct_2(k3_latsubgr(A,B,C),u1_struct_0(k11_group_4(A)),u1_struct_0(k11_group_4(B))) % 63.63/63.78 & m2_relset_1(k3_latsubgr(A,B,C),u1_struct_0(k11_group_4(A)),u1_struct_0(k11_group_4(B))) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(dt_l1_group_1,axiom, % 63.63/63.78 ! [A] : % 63.63/63.78 ( l1_group_1(A) % 63.63/63.78 => l1_struct_0(A) ) ). % 63.63/63.78 % 63.63/63.78 fof(dt_l1_lattices,axiom, % 63.63/63.78 ! [A] : % 63.63/63.78 ( l1_lattices(A) % 63.63/63.78 => l1_struct_0(A) ) ). % 63.63/63.78 % 63.63/63.78 fof(dt_l1_struct_0,axiom, % 63.63/63.78 $true ). % 63.63/63.78 % 63.63/63.78 fof(dt_l2_lattices,axiom, % 63.63/63.78 ! [A] : % 63.63/63.78 ( l2_lattices(A) % 63.63/63.78 => l1_struct_0(A) ) ). % 63.63/63.78 % 63.63/63.78 fof(dt_l3_lattices,axiom, % 63.63/63.78 ! [A] : % 63.63/63.78 ( l3_lattices(A) % 63.63/63.78 => ( l1_lattices(A) % 63.63/63.78 & l2_lattices(A) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(dt_m1_lattice4,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ( ( ~ v3_struct_0(A) % 63.63/63.78 & v10_lattices(A) % 63.63/63.78 & l3_lattices(A) % 63.63/63.78 & ~ v3_struct_0(B) % 63.63/63.78 & v10_lattices(B) % 63.63/63.78 & l3_lattices(B) ) % 63.63/63.78 => ! [C] : % 63.63/63.78 ( m1_lattice4(C,A,B) % 63.63/63.78 => ( v1_funct_1(C) % 63.63/63.78 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 63.63/63.78 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(dt_m1_relset_1,axiom, % 63.63/63.78 $true ). % 63.63/63.78 % 63.63/63.78 fof(dt_m1_subset_1,axiom, % 63.63/63.78 $true ). % 63.63/63.78 % 63.63/63.78 fof(dt_m2_relset_1,axiom, % 63.63/63.78 ! [A,B,C] : % 63.63/63.78 ( m2_relset_1(C,A,B) % 63.63/63.78 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 63.63/63.78 % 63.63/63.78 fof(dt_m3_vectsp_8,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ( ( ~ v3_struct_0(A) % 63.63/63.78 & v10_lattices(A) % 63.63/63.78 & l3_lattices(A) % 63.63/63.78 & ~ v3_struct_0(B) % 63.63/63.78 & v10_lattices(B) % 63.63/63.78 & l3_lattices(B) ) % 63.63/63.78 => ! [C] : % 63.63/63.78 ( m3_vectsp_8(C,A,B) % 63.63/63.78 => ( v1_funct_1(C) % 63.63/63.78 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 63.63/63.78 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(dt_m4_vectsp_8,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ( ( ~ v3_struct_0(A) % 63.63/63.78 & v10_lattices(A) % 63.63/63.78 & l3_lattices(A) % 63.63/63.78 & ~ v3_struct_0(B) % 63.63/63.78 & v10_lattices(B) % 63.63/63.78 & l3_lattices(B) ) % 63.63/63.78 => ! [C] : % 63.63/63.78 ( m4_vectsp_8(C,A,B) % 63.63/63.78 => ( v1_funct_1(C) % 63.63/63.78 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 63.63/63.78 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(dt_u1_lattices,axiom, % 63.63/63.78 ! [A] : % 63.63/63.78 ( l1_lattices(A) % 63.63/63.78 => ( v1_funct_1(u1_lattices(A)) % 63.63/63.78 & v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 63.63/63.78 & m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(dt_u1_struct_0,axiom, % 63.63/63.78 $true ). % 63.63/63.78 % 63.63/63.78 fof(dt_u2_lattices,axiom, % 63.63/63.78 ! [A] : % 63.63/63.78 ( l2_lattices(A) % 63.63/63.78 => ( v1_funct_1(u2_lattices(A)) % 63.63/63.78 & v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 63.63/63.78 & m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(existence_l1_group_1,axiom, % 63.63/63.78 ? [A] : l1_group_1(A) ). % 63.63/63.78 % 63.63/63.78 fof(existence_l1_lattices,axiom, % 63.63/63.78 ? [A] : l1_lattices(A) ). % 63.63/63.78 % 63.63/63.78 fof(existence_l1_struct_0,axiom, % 63.63/63.78 ? [A] : l1_struct_0(A) ). % 63.63/63.78 % 63.63/63.78 fof(existence_l2_lattices,axiom, % 63.63/63.78 ? [A] : l2_lattices(A) ). % 63.63/63.78 % 63.63/63.78 fof(existence_l3_lattices,axiom, % 63.63/63.78 ? [A] : l3_lattices(A) ). % 63.63/63.78 % 63.63/63.78 fof(existence_m1_lattice4,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ( ( ~ v3_struct_0(A) % 63.63/63.78 & v10_lattices(A) % 63.63/63.78 & l3_lattices(A) % 63.63/63.78 & ~ v3_struct_0(B) % 63.63/63.78 & v10_lattices(B) % 63.63/63.78 & l3_lattices(B) ) % 63.63/63.78 => ? [C] : m1_lattice4(C,A,B) ) ). % 63.63/63.78 % 63.63/63.78 fof(existence_m1_relset_1,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ? [C] : m1_relset_1(C,A,B) ). % 63.63/63.78 % 63.63/63.78 fof(existence_m1_subset_1,axiom, % 63.63/63.78 ! [A] : % 63.63/63.78 ? [B] : m1_subset_1(B,A) ). % 63.63/63.78 % 63.63/63.78 fof(existence_m2_relset_1,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ? [C] : m2_relset_1(C,A,B) ). % 63.63/63.78 % 63.63/63.78 fof(existence_m3_vectsp_8,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ( ( ~ v3_struct_0(A) % 63.63/63.78 & v10_lattices(A) % 63.63/63.78 & l3_lattices(A) % 63.63/63.78 & ~ v3_struct_0(B) % 63.63/63.78 & v10_lattices(B) % 63.63/63.78 & l3_lattices(B) ) % 63.63/63.78 => ? [C] : m3_vectsp_8(C,A,B) ) ). % 63.63/63.78 % 63.63/63.78 fof(existence_m4_vectsp_8,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ( ( ~ v3_struct_0(A) % 63.63/63.78 & v10_lattices(A) % 63.63/63.78 & l3_lattices(A) % 63.63/63.78 & ~ v3_struct_0(B) % 63.63/63.78 & v10_lattices(B) % 63.63/63.78 & l3_lattices(B) ) % 63.63/63.78 => ? [C] : m4_vectsp_8(C,A,B) ) ). % 63.63/63.78 % 63.63/63.78 fof(fc1_group_4,axiom, % 63.63/63.78 ! [A] : % 63.63/63.78 ( ( ~ v3_struct_0(A) % 63.63/63.78 & v3_group_1(A) % 63.63/63.78 & v4_group_1(A) % 63.63/63.78 & l1_group_1(A) ) % 63.63/63.78 => ( ~ v3_struct_0(k11_group_4(A)) % 63.63/63.78 & v3_lattices(k11_group_4(A)) % 63.63/63.78 & v4_lattices(k11_group_4(A)) % 63.63/63.78 & v5_lattices(k11_group_4(A)) % 63.63/63.78 & v6_lattices(k11_group_4(A)) % 63.63/63.78 & v7_lattices(k11_group_4(A)) % 63.63/63.78 & v8_lattices(k11_group_4(A)) % 63.63/63.78 & v9_lattices(k11_group_4(A)) % 63.63/63.78 & v10_lattices(k11_group_4(A)) % 63.63/63.78 & v13_lattices(k11_group_4(A)) % 63.63/63.78 & v14_lattices(k11_group_4(A)) % 63.63/63.78 & v15_lattices(k11_group_4(A)) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(fc1_struct_0,axiom, % 63.63/63.78 ! [A] : % 63.63/63.78 ( ( ~ v3_struct_0(A) % 63.63/63.78 & l1_struct_0(A) ) % 63.63/63.78 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 63.63/63.78 % 63.63/63.78 fof(fc1_subset_1,axiom, % 63.63/63.78 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 63.63/63.78 % 63.63/63.78 fof(fc1_xboole_0,axiom, % 63.63/63.78 v1_xboole_0(k1_xboole_0) ). % 63.63/63.78 % 63.63/63.78 fof(fc4_subset_1,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ( ( ~ v1_xboole_0(A) % 63.63/63.78 & ~ v1_xboole_0(B) ) % 63.63/63.78 => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ). % 63.63/63.78 % 63.63/63.78 fof(free_g3_lattices,axiom, % 63.63/63.78 ! [A,B,C] : % 63.63/63.78 ( ( v1_funct_1(B) % 63.63/63.78 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 63.63/63.78 & m1_relset_1(B,k2_zfmisc_1(A,A),A) % 63.63/63.78 & v1_funct_1(C) % 63.63/63.78 & v1_funct_2(C,k2_zfmisc_1(A,A),A) % 63.63/63.78 & m1_relset_1(C,k2_zfmisc_1(A,A),A) ) % 63.63/63.78 => ! [D,E,F] : % 63.63/63.78 ( g3_lattices(A,B,C) = g3_lattices(D,E,F) % 63.63/63.78 => ( A = D % 63.63/63.78 & B = E % 63.63/63.78 & C = F ) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(rc1_funct_2,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ? [C] : % 63.63/63.78 ( m1_relset_1(C,A,B) % 63.63/63.78 & v1_relat_1(C) % 63.63/63.78 & v1_funct_1(C) % 63.63/63.78 & v1_funct_2(C,A,B) ) ). % 63.63/63.78 % 63.63/63.78 fof(rc1_partfun1,axiom, % 63.63/63.78 ? [A] : % 63.63/63.78 ( v1_relat_1(A) % 63.63/63.78 & v1_funct_1(A) % 63.63/63.78 & v2_funct_1(A) % 63.63/63.78 & v1_xboole_0(A) ) ). % 63.63/63.78 % 63.63/63.78 fof(rc1_subset_1,axiom, % 63.63/63.78 ! [A] : % 63.63/63.78 ( ~ v1_xboole_0(A) % 63.63/63.78 => ? [B] : % 63.63/63.78 ( m1_subset_1(B,k1_zfmisc_1(A)) % 63.63/63.78 & ~ v1_xboole_0(B) ) ) ). % 63.63/63.78 % 63.63/63.78 fof(rc1_xboole_0,axiom, % 63.63/63.78 ? [A] : v1_xboole_0(A) ). % 63.63/63.78 % 63.63/63.78 fof(rc2_partfun1,axiom, % 63.63/63.78 ! [A,B] : % 63.63/63.78 ? [C] : % 63.63/63.78 ( m1_relset_1(C,A,B) % 63.63/63.78 & v1_relat_1(C) % 63.63/63.78 & v1_funct_1(C) ) ). % 63.63/63.78 % 63.63/63.78 fof(rc2_subset_1,axiom, % 63.63/63.78 ! [A] : % 63.63/63.78 ? [B] : % 63.63/63.78 ( m1_subset_1(B,k1_zfmisc_1(A)) % 63.63/63.78 & v1_xboole_0(B) ) ). % 63.63/63.78 % 63.63/63.78 fof(rc2_xboole_0,axiom, % 63.63/63.78 ? [A] : ~ v1_xboole_0(A) ). % 63.63/63.78 % 63.63/63.78 fof(rc3_struct_0,axiom, % 63.63/63.78 ? [A] : % 63.63/63.78 ( l1_struct_0(A) % 63.63/63.78 & ~ v3_struct_0(A) ) ). % 63.63/63.78 % 63.63/63.79 fof(rc5_struct_0,axiom, % 63.63/63.79 ! [A] : % 63.63/63.79 ( ( ~ v3_struct_0(A) % 63.63/63.79 & l1_struct_0(A) ) % 63.63/63.79 => ? [B] : % 63.63/63.79 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 63.63/63.79 & ~ v1_xboole_0(B) ) ) ). % 63.63/63.79 % 63.63/63.79 fof(redefinition_m2_relset_1,axiom, % 63.63/63.79 ! [A,B,C] : % 63.63/63.79 ( m2_relset_1(C,A,B) % 63.63/63.79 <=> m1_relset_1(C,A,B) ) ). % 63.63/63.79 % 63.63/63.79 fof(reflexivity_r1_tarski,axiom, % 63.63/63.79 ! [A,B] : r1_tarski(A,A) ). % 63.63/63.79 % 63.63/63.79 fof(t11_vectsp_8,axiom, % 63.63/63.79 ! [A] : % 63.63/63.79 ( ( ~ v3_struct_0(A) % 63.63/63.79 & v10_lattices(A) % 63.63/63.79 & l3_lattices(A) ) % 63.63/63.79 => ! [B] : % 63.63/63.79 ( ( ~ v3_struct_0(B) % 63.63/63.79 & v10_lattices(B) % 63.63/63.79 & l3_lattices(B) ) % 63.63/63.79 => ! [C] : % 63.63/63.79 ( ( v1_funct_1(C) % 63.63/63.79 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 63.63/63.79 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) % 63.63/63.79 => ( m1_lattice4(C,A,B) % 63.63/63.79 <=> ( m4_vectsp_8(C,A,B) % 63.63/63.79 & m3_vectsp_8(C,A,B) ) ) ) ) ) ). % 63.63/63.79 % 63.63/63.79 fof(t1_subset,axiom, % 63.63/63.79 ! [A,B] : % 63.63/63.79 ( r2_hidden(A,B) % 63.63/63.79 => m1_subset_1(A,B) ) ). % 63.63/63.79 % 63.63/63.79 fof(t2_subset,axiom, % 63.63/63.79 ! [A,B] : % 63.63/63.79 ( m1_subset_1(A,B) % 63.63/63.79 => ( v1_xboole_0(B) % 63.63/63.79 | r2_hidden(A,B) ) ) ). % 63.63/63.79 % 63.63/63.79 fof(t36_latsubgr,axiom, % 63.63/63.79 ! [A] : % 63.63/63.79 ( ( ~ v3_struct_0(A) % 63.63/63.79 & v3_group_1(A) % 63.63/63.79 & v4_group_1(A) % 63.63/63.79 & l1_group_1(A) ) % 63.63/63.79 => ! [B] : % 63.63/63.79 ( ( ~ v3_struct_0(B) % 63.63/63.79 & v3_group_1(B) % 63.63/63.79 & v4_group_1(B) % 63.63/63.79 & l1_group_1(B) ) % 63.63/63.79 => ! [C] : % 63.63/63.79 ( ( v1_funct_1(C) % 63.63/63.79 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 63.63/63.79 & v1_group_6(C,A,B) % 63.63/63.79 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) % 63.63/63.79 => ( v2_funct_1(C) % 63.63/63.79 => m3_vectsp_8(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B)) ) ) ) ) ). % 63.63/63.79 % 63.63/63.79 fof(t37_latsubgr,axiom, % 63.63/63.79 ! [A] : % 63.63/63.79 ( ( ~ v3_struct_0(A) % 63.63/63.79 & v3_group_1(A) % 63.63/63.79 & v4_group_1(A) % 63.63/63.79 & l1_group_1(A) ) % 63.63/63.79 => ! [B] : % 63.63/63.79 ( ( ~ v3_struct_0(B) % 63.63/63.79 & v3_group_1(B) % 63.63/63.79 & v4_group_1(B) % 63.63/63.79 & l1_group_1(B) ) % 63.63/63.79 => ! [C] : % 63.63/63.79 ( ( v1_funct_1(C) % 63.63/63.79 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 63.63/63.79 & v1_group_6(C,A,B) % 63.63/63.79 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) % 63.63/63.79 => m4_vectsp_8(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B)) ) ) ) ). % 63.63/63.79 % 63.63/63.79 fof(t3_subset,axiom, % 63.63/63.79 ! [A,B] : % 63.63/63.79 ( m1_subset_1(A,k1_zfmisc_1(B)) % 63.63/63.79 <=> r1_tarski(A,B) ) ). % 63.63/63.79 % 63.63/63.79 fof(t4_subset,axiom, % 63.63/63.79 ! [A,B,C] : % 63.63/63.79 ( ( r2_hidden(A,B) % 63.63/63.79 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 63.63/63.79 => m1_subset_1(A,C) ) ). % 63.63/63.79 % 63.63/63.79 fof(t5_subset,axiom, % 63.63/63.79 ! [A,B,C] : % 63.63/63.79 ~ ( r2_hidden(A,B) % 63.63/63.79 & m1_subset_1(B,k1_zfmisc_1(C)) % 63.63/63.79 & v1_xboole_0(C) ) ). % 63.63/63.79 % 63.63/63.79 fof(t6_boole,axiom, % 63.63/63.79 ! [A] : % 63.63/63.79 ( v1_xboole_0(A) % 63.63/63.79 => A = k1_xboole_0 ) ). % 63.63/63.79 % 63.63/63.79 fof(t7_boole,axiom, % 63.63/63.79 ! [A,B] : % 63.63/63.79 ~ ( r2_hidden(A,B) % 63.63/63.79 & v1_xboole_0(B) ) ). % 63.63/63.79 % 63.63/63.79 fof(t8_boole,axiom, % 63.63/63.79 ! [A,B] : % 63.63/63.79 ~ ( v1_xboole_0(A) % 63.63/63.79 & A != B % 63.63/63.79 & v1_xboole_0(B) ) ). % 63.63/63.79 % 63.63/63.79 %------------------------------------------------------------------------------ % 63.63/63.79 %------------------------------------------- % 63.63/63.79 % Proof found % 63.63/63.79 % SZS status Theorem for theBenchmark % 63.63/63.79 % SZS output start Proof % 63.63/63.79 %ClaNum:206(EqnAxiom:87) % 63.63/63.79 %VarNum:671(SingletonVarNum:178) % 63.63/63.79 %MaxLitNum:14 % 63.63/63.79 %MaxfuncDepth:2 % 63.63/63.79 %SharedTerms:46 % 63.63/63.79 %goalClause: 88 89 90 91 92 93 95 97 116 117 118 124 125 129 % 63.63/63.79 %singleGoalClaCount:14 % 63.63/63.79 [88]P1(a1) % 63.63/63.79 [89]P1(a12) % 63.63/63.79 [90]P26(a1) % 63.63/63.79 [91]P26(a12) % 63.63/63.79 [92]P2(a1) % 63.63/63.79 [93]P2(a12) % 63.63/63.79 [94]P2(a17) % 63.63/63.79 [95]P3(a18) % 63.63/63.79 [96]P3(a2) % 63.63/63.79 [97]P20(a18) % 63.63/63.79 [98]P20(a2) % 63.63/63.79 [99]P4(a19) % 63.63/63.79 [100]P21(a2) % 63.63/63.79 [101]P25(a23) % 63.63/63.79 [102]P25(a2) % 63.63/63.79 [103]P25(a9) % 63.63/63.79 [104]P5(a20) % 63.63/63.79 [105]P5(a13) % 63.63/63.79 [106]P6(a21) % 63.63/63.79 [107]P7(a22) % 63.63/63.79 [116]P22(a18,a1,a12) % 63.63/63.79 [124]~P27(a1) % 63.63/63.79 [125]~P27(a12) % 63.63/63.79 [126]~P27(a13) % 63.63/63.79 [127]~P25(a15) % 63.63/63.79 [117]P23(a18,f28(a1),f28(a12)) % 63.63/63.79 [118]P12(a18,f28(a1),f28(a12)) % 63.63/63.79 [129]~P11(f29(a1,a12,a18),f24(a1),f24(a12)) % 63.63/63.79 [109]P8(x1091,x1091) % 63.63/63.79 [108]P25(f14(x1081)) % 63.63/63.79 [110]P9(f3(x1101),x1101) % 63.63/63.79 [111]P9(f14(x1111),f27(x1111)) % 63.63/63.79 [128]~P25(f27(x1281)) % 63.63/63.79 [112]P3(f5(x1121,x1122)) % 63.63/63.79 [113]P3(f11(x1131,x1132)) % 63.63/63.79 [114]P21(f5(x1141,x1142)) % 63.63/63.79 [115]P21(f11(x1151,x1152)) % 63.63/63.79 [119]P23(f5(x1191,x1192),x1191,x1192) % 63.63/63.79 [120]P12(f6(x1201,x1202),x1201,x1202) % 63.63/63.79 [121]P10(f4(x1211,x1212),x1211,x1212) % 63.63/63.79 [122]P10(f5(x1221,x1222),x1221,x1222) % 63.63/63.79 [123]P10(f11(x1231,x1232),x1231,x1232) % 63.63/63.79 [130]~P25(x1301)+E(x1301,a23) % 63.63/63.79 [131]~P2(x1311)+P5(x1311) % 63.63/63.79 [132]~P6(x1321)+P5(x1321) % 63.63/63.79 [133]~P7(x1331)+P5(x1331) % 63.63/63.79 [134]~P4(x1341)+P6(x1341) % 63.63/63.79 [135]~P4(x1351)+P7(x1351) % 63.63/63.79 [137]~P7(x1371)+P3(f32(x1371)) % 63.63/63.79 [138]~P6(x1381)+P3(f31(x1381)) % 63.63/63.79 [139]P25(x1391)+~P25(f10(x1391)) % 63.63/63.79 [143]P25(x1431)+P9(f10(x1431),f27(x1431)) % 63.63/63.79 [174]~P7(x1741)+P23(f32(x1741),f30(f28(x1741),f28(x1741)),f28(x1741)) % 63.63/63.79 [175]~P6(x1751)+P23(f31(x1751),f30(f28(x1751),f28(x1751)),f28(x1751)) % 63.63/63.79 [176]~P7(x1761)+P12(f32(x1761),f30(f28(x1761),f28(x1761)),f28(x1761)) % 63.63/63.79 [177]~P6(x1771)+P12(f31(x1771),f30(f28(x1771),f28(x1771)),f28(x1771)) % 63.63/63.79 [142]~P25(x1421)+~P15(x1422,x1421) % 63.63/63.79 [158]~P15(x1581,x1582)+P9(x1581,x1582) % 63.63/63.79 [163]~P15(x1632,x1631)+~P15(x1631,x1632) % 63.63/63.79 [162]~P8(x1621,x1622)+P9(x1621,f27(x1622)) % 63.63/63.79 [164]P8(x1641,x1642)+~P9(x1641,f27(x1642)) % 63.63/63.79 [181]~P10(x1811,x1812,x1813)+P12(x1811,x1812,x1813) % 63.63/63.79 [182]~P12(x1821,x1822,x1823)+P10(x1821,x1822,x1823) % 63.63/63.79 [170]P21(x1701)+~P9(x1701,f27(f30(x1702,x1703))) % 63.63/63.79 [183]~P12(x1831,x1832,x1833)+P9(x1831,f27(f30(x1832,x1833))) % 63.63/63.79 [140]~P5(x1401)+P27(x1401)+~P25(f28(x1401)) % 63.63/63.79 [141]~P5(x1411)+P27(x1411)+~P25(f16(x1411)) % 63.63/63.79 [165]~P5(x1651)+P27(x1651)+P9(f16(x1651),f27(f28(x1651))) % 63.63/63.79 [169]~P4(x1691)+~P28(x1691)+E(f25(f28(x1691),f32(x1691),f31(x1691)),x1691) % 63.63/63.79 [136]~P25(x1362)+~P25(x1361)+E(x1361,x1362) % 63.63/63.79 [159]~P9(x1592,x1591)+P25(x1591)+P15(x1592,x1591) % 63.63/63.79 [166]P25(x1661)+P25(x1662)+~P25(f30(x1662,x1661)) % 63.63/63.79 [167]~P25(x1671)+~P15(x1672,x1673)+~P9(x1673,f27(x1671)) % 63.63/63.79 [168]P9(x1681,x1682)+~P15(x1681,x1683)+~P9(x1683,f27(x1682)) % 63.63/63.79 [191]~P3(x1911)+~P10(x1911,x1912,x1913)+~P24(x1911,x1912,x1913)+P23(x1911,x1912,x1913) % 63.63/63.79 [144]~P1(x1441)+~P26(x1441)+~P2(x1441)+P27(x1441)+P4(f24(x1441)) % 63.63/63.79 [146]~P1(x1461)+~P26(x1461)+~P2(x1461)+P27(x1461)+P28(f24(x1461)) % 63.63/63.79 [148]~P1(x1481)+~P26(x1481)+~P2(x1481)+P27(x1481)+P16(f24(x1481)) % 63.63/63.79 [149]~P1(x1491)+~P26(x1491)+~P2(x1491)+P27(x1491)+P29(f24(x1491)) % 63.63/63.79 [150]~P1(x1501)+~P26(x1501)+~P2(x1501)+P27(x1501)+P30(f24(x1501)) % 63.63/63.79 [151]~P1(x1511)+~P26(x1511)+~P2(x1511)+P27(x1511)+P31(f24(x1511)) % 63.63/63.79 [152]~P1(x1521)+~P26(x1521)+~P2(x1521)+P27(x1521)+P32(f24(x1521)) % 63.63/63.79 [153]~P1(x1531)+~P26(x1531)+~P2(x1531)+P27(x1531)+P33(f24(x1531)) % 63.63/63.79 [154]~P1(x1541)+~P26(x1541)+~P2(x1541)+P27(x1541)+P34(f24(x1541)) % 63.63/63.79 [155]~P1(x1551)+~P26(x1551)+~P2(x1551)+P27(x1551)+P17(f24(x1551)) % 63.63/63.79 [156]~P1(x1561)+~P26(x1561)+~P2(x1561)+P27(x1561)+P18(f24(x1561)) % 63.63/63.79 [157]~P1(x1571)+~P26(x1571)+~P2(x1571)+P27(x1571)+P19(f24(x1571)) % 63.63/63.79 [161]~P1(x1611)+~P26(x1611)+~P2(x1611)+P27(x1611)+~P27(f24(x1611)) % 63.63/63.79 [192]~P3(x1922)+~P23(x1922,x1923,x1921)+~P10(x1922,x1923,x1921)+P25(x1921)+P24(x1922,x1923,x1921) % 63.63/63.79 [190]~P25(x1903)+~P23(x1903,x1902,x1901)+~P10(x1903,x1902,x1901)+P25(x1901)+P25(x1902)+~P3(x1903) % 63.63/63.79 [171]~P4(x1711)+~P4(x1712)+~P16(x1711)+~P16(x1712)+P27(x1711)+P27(x1712)+P11(f26(x1712,x1711),x1712,x1711) % 63.63/63.79 [172]~P4(x1721)+~P4(x1722)+~P16(x1721)+~P16(x1722)+P27(x1721)+P27(x1722)+P13(f7(x1722,x1721),x1722,x1721) % 63.63/63.79 [173]~P4(x1731)+~P4(x1732)+~P16(x1731)+~P16(x1732)+P27(x1731)+P27(x1732)+P14(f8(x1732,x1731),x1732,x1731) % 63.63/63.79 [202]~P3(x2023)+~P3(x2022)+~P23(x2023,f30(x2021,x2021),x2021)+~P23(x2022,f30(x2021,x2021),x2021)+~P10(x2023,f30(x2021,x2021),x2021)+~P10(x2022,f30(x2021,x2021),x2021)+P4(f25(x2021,x2022,x2023)) % 63.63/63.79 [203]~P3(x2033)+~P3(x2032)+~P23(x2033,f30(x2031,x2031),x2031)+~P23(x2032,f30(x2031,x2031),x2031)+~P10(x2033,f30(x2031,x2031),x2031)+~P10(x2032,f30(x2031,x2031),x2031)+P28(f25(x2031,x2032,x2033)) % 63.63/63.79 [178]~P4(x1781)+~P4(x1782)+~P16(x1781)+~P16(x1782)+~P11(x1783,x1782,x1781)+P27(x1781)+P27(x1782)+P3(x1783) % 63.63/63.79 [179]~P4(x1791)+~P4(x1792)+~P16(x1791)+~P16(x1792)+~P13(x1793,x1792,x1791)+P27(x1791)+P27(x1792)+P3(x1793) % 63.63/63.79 [180]~P4(x1801)+~P4(x1802)+~P16(x1801)+~P16(x1802)+~P14(x1803,x1802,x1801)+P27(x1801)+P27(x1802)+P3(x1803) % 63.63/63.79 [184]~P4(x1841)+~P4(x1842)+~P16(x1841)+~P16(x1842)+~P11(x1843,x1842,x1841)+P27(x1841)+P27(x1842)+P23(x1843,f28(x1842),f28(x1841)) % 63.63/63.79 [185]~P4(x1851)+~P4(x1852)+~P16(x1851)+~P16(x1852)+~P13(x1853,x1852,x1851)+P27(x1851)+P27(x1852)+P23(x1853,f28(x1852),f28(x1851)) % 63.63/63.79 [186]~P4(x1861)+~P4(x1862)+~P16(x1861)+~P16(x1862)+~P14(x1863,x1862,x1861)+P27(x1861)+P27(x1862)+P23(x1863,f28(x1862),f28(x1861)) % 63.63/63.79 [187]~P4(x1871)+~P4(x1872)+~P16(x1871)+~P16(x1872)+~P11(x1873,x1872,x1871)+P27(x1871)+P27(x1872)+P12(x1873,f28(x1872),f28(x1871)) % 63.63/63.79 [188]~P4(x1881)+~P4(x1882)+~P16(x1881)+~P16(x1882)+~P13(x1883,x1882,x1881)+P27(x1881)+P27(x1882)+P12(x1883,f28(x1882),f28(x1881)) % 63.63/63.79 [189]~P4(x1891)+~P4(x1892)+~P16(x1891)+~P16(x1892)+~P14(x1893,x1892,x1891)+P27(x1891)+P27(x1892)+P12(x1893,f28(x1892),f28(x1891)) % 63.63/63.79 [204]~P3(x2044)+~P3(x2041)+E(x2041,x2042)+~P23(x2044,f30(x2043,x2043),x2043)+~P23(x2041,f30(x2043,x2043),x2043)+~P10(x2044,f30(x2043,x2043),x2043)+~P10(x2041,f30(x2043,x2043),x2043)+~E(f25(x2043,x2044,x2041),f25(x2045,x2046,x2042)) % 63.63/63.79 [205]~P3(x2054)+~P3(x2051)+E(x2051,x2052)+~P23(x2054,f30(x2053,x2053),x2053)+~P23(x2051,f30(x2053,x2053),x2053)+~P10(x2054,f30(x2053,x2053),x2053)+~P10(x2051,f30(x2053,x2053),x2053)+~E(f25(x2053,x2051,x2054),f25(x2055,x2052,x2056)) % 63.63/63.79 [206]~P3(x2064)+~P3(x2063)+E(x2061,x2062)+~P23(x2064,f30(x2061,x2061),x2061)+~P23(x2063,f30(x2061,x2061),x2061)+~P10(x2064,f30(x2061,x2061),x2061)+~P10(x2063,f30(x2061,x2061),x2061)+~E(f25(x2061,x2063,x2064),f25(x2062,x2065,x2066)) % 63.63/63.79 [195]~P3(x1953)+~P4(x1951)+~P4(x1952)+~P16(x1951)+~P16(x1952)+~P11(x1953,x1952,x1951)+P27(x1951)+P13(x1953,x1952,x1951)+P27(x1952)+~P23(x1953,f28(x1952),f28(x1951))+~P12(x1953,f28(x1952),f28(x1951)) % 63.63/63.79 [196]~P3(x1963)+~P4(x1961)+~P4(x1962)+~P16(x1961)+~P16(x1962)+~P11(x1963,x1962,x1961)+P27(x1961)+P14(x1963,x1962,x1961)+P27(x1962)+~P23(x1963,f28(x1962),f28(x1961))+~P12(x1963,f28(x1962),f28(x1961)) % 63.63/63.79 [194]~P1(x1941)+~P1(x1942)+~P26(x1941)+~P26(x1942)+~P2(x1941)+~P2(x1942)+~P3(x1943)+P27(x1941)+P27(x1942)+~P23(x1943,f28(x1942),f28(x1941))+~P10(x1943,f28(x1942),f28(x1941))+P3(f29(x1942,x1941,x1943)) % 63.63/63.79 [199]~P3(x1993)+~P4(x1991)+~P4(x1992)+~P16(x1991)+~P16(x1992)+~P13(x1993,x1992,x1991)+~P14(x1993,x1992,x1991)+P27(x1991)+P11(x1993,x1992,x1991)+P27(x1992)+~P23(x1993,f28(x1992),f28(x1991))+~P12(x1993,f28(x1992),f28(x1991)) % 63.63/63.79 [197]~P1(x1971)+~P1(x1972)+~P26(x1971)+~P26(x1972)+~P2(x1971)+~P2(x1972)+~P3(x1973)+P27(x1971)+P27(x1972)+~P23(x1973,f28(x1972),f28(x1971))+~P10(x1973,f28(x1972),f28(x1971))+P23(f29(x1972,x1971,x1973),f28(f24(x1972)),f28(f24(x1971))) % 63.63/63.79 [198]~P1(x1981)+~P1(x1982)+~P26(x1981)+~P26(x1982)+~P2(x1981)+~P2(x1982)+~P3(x1983)+P27(x1981)+P27(x1982)+~P23(x1983,f28(x1982),f28(x1981))+~P10(x1983,f28(x1982),f28(x1981))+P12(f29(x1982,x1981,x1983),f28(f24(x1982)),f28(f24(x1981))) % 63.63/63.80 [200]~P1(x2001)+~P1(x2002)+~P26(x2001)+~P26(x2002)+~P2(x2001)+~P2(x2002)+~P3(x2003)+~P22(x2003,x2002,x2001)+P27(x2001)+P27(x2002)+~P23(x2003,f28(x2002),f28(x2001))+~P12(x2003,f28(x2002),f28(x2001))+P14(f29(x2002,x2001,x2003),f24(x2002),f24(x2001)) % 63.63/63.80 [201]~P1(x2011)+~P1(x2012)+~P26(x2011)+~P26(x2012)+~P2(x2011)+~P2(x2012)+~P3(x2013)+~P20(x2013)+~P22(x2013,x2012,x2011)+P27(x2011)+P27(x2012)+~P23(x2013,f28(x2012),f28(x2011))+~P12(x2013,f28(x2012),f28(x2011))+P13(f29(x2012,x2011,x2013),f24(x2012),f24(x2011)) % 63.63/63.80 %EqnAxiom % 63.63/63.80 [1]E(x11,x11) % 63.63/63.80 [2]E(x22,x21)+~E(x21,x22) % 63.63/63.80 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 63.63/63.80 [4]~E(x41,x42)+E(f14(x41),f14(x42)) % 63.63/63.80 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 63.63/63.80 [6]~E(x61,x62)+E(f30(x61,x63),f30(x62,x63)) % 63.63/63.80 [7]~E(x71,x72)+E(f30(x73,x71),f30(x73,x72)) % 63.63/63.80 [8]~E(x81,x82)+E(f27(x81),f27(x82)) % 63.63/63.80 [9]~E(x91,x92)+E(f5(x91,x93),f5(x92,x93)) % 63.63/63.80 [10]~E(x101,x102)+E(f5(x103,x101),f5(x103,x102)) % 63.63/63.80 [11]~E(x111,x112)+E(f11(x111,x113),f11(x112,x113)) % 63.63/63.80 [12]~E(x121,x122)+E(f11(x123,x121),f11(x123,x122)) % 63.63/63.80 [13]~E(x131,x132)+E(f28(x131),f28(x132)) % 63.63/63.80 [14]~E(x141,x142)+E(f24(x141),f24(x142)) % 63.63/63.80 [15]~E(x151,x152)+E(f29(x151,x153,x154),f29(x152,x153,x154)) % 63.63/63.80 [16]~E(x161,x162)+E(f29(x163,x161,x164),f29(x163,x162,x164)) % 63.63/63.80 [17]~E(x171,x172)+E(f29(x173,x174,x171),f29(x173,x174,x172)) % 63.63/63.80 [18]~E(x181,x182)+E(f25(x181,x183,x184),f25(x182,x183,x184)) % 63.63/63.80 [19]~E(x191,x192)+E(f25(x193,x191,x194),f25(x193,x192,x194)) % 63.63/63.80 [20]~E(x201,x202)+E(f25(x203,x204,x201),f25(x203,x204,x202)) % 63.63/63.80 [21]~E(x211,x212)+E(f31(x211),f31(x212)) % 63.63/63.80 [22]~E(x221,x222)+E(f32(x221),f32(x222)) % 63.63/63.80 [23]~E(x231,x232)+E(f10(x231),f10(x232)) % 63.63/63.80 [24]~E(x241,x242)+E(f6(x241,x243),f6(x242,x243)) % 63.63/63.80 [25]~E(x251,x252)+E(f6(x253,x251),f6(x253,x252)) % 63.63/63.80 [26]~E(x261,x262)+E(f4(x261,x263),f4(x262,x263)) % 63.63/63.80 [27]~E(x271,x272)+E(f4(x273,x271),f4(x273,x272)) % 63.63/63.80 [28]~E(x281,x282)+E(f16(x281),f16(x282)) % 63.63/63.80 [29]~E(x291,x292)+E(f8(x291,x293),f8(x292,x293)) % 63.63/63.80 [30]~E(x301,x302)+E(f8(x303,x301),f8(x303,x302)) % 63.63/63.80 [31]~E(x311,x312)+E(f26(x311,x313),f26(x312,x313)) % 63.63/63.80 [32]~E(x321,x322)+E(f26(x323,x321),f26(x323,x322)) % 63.63/63.80 [33]~E(x331,x332)+E(f7(x331,x333),f7(x332,x333)) % 63.63/63.80 [34]~E(x341,x342)+E(f7(x343,x341),f7(x343,x342)) % 63.63/63.80 [35]~P1(x351)+P1(x352)+~E(x351,x352) % 63.63/63.80 [36]P10(x362,x363,x364)+~E(x361,x362)+~P10(x361,x363,x364) % 63.63/63.80 [37]P10(x373,x372,x374)+~E(x371,x372)+~P10(x373,x371,x374) % 63.63/63.80 [38]P10(x383,x384,x382)+~E(x381,x382)+~P10(x383,x384,x381) % 63.63/63.80 [39]~P26(x391)+P26(x392)+~E(x391,x392) % 63.63/63.80 [40]P22(x402,x403,x404)+~E(x401,x402)+~P22(x401,x403,x404) % 63.63/63.80 [41]P22(x413,x412,x414)+~E(x411,x412)+~P22(x413,x411,x414) % 63.63/63.80 [42]P22(x423,x424,x422)+~E(x421,x422)+~P22(x423,x424,x421) % 63.63/63.80 [43]~P2(x431)+P2(x432)+~E(x431,x432) % 63.63/63.80 [44]~P3(x441)+P3(x442)+~E(x441,x442) % 63.63/63.80 [45]P12(x452,x453,x454)+~E(x451,x452)+~P12(x451,x453,x454) % 63.63/63.80 [46]P12(x463,x462,x464)+~E(x461,x462)+~P12(x463,x461,x464) % 63.63/63.80 [47]P12(x473,x474,x472)+~E(x471,x472)+~P12(x473,x474,x471) % 63.63/63.80 [48]P23(x482,x483,x484)+~E(x481,x482)+~P23(x481,x483,x484) % 63.63/63.80 [49]P23(x493,x492,x494)+~E(x491,x492)+~P23(x493,x491,x494) % 63.63/63.80 [50]P23(x503,x504,x502)+~E(x501,x502)+~P23(x503,x504,x501) % 63.63/63.80 [51]P11(x512,x513,x514)+~E(x511,x512)+~P11(x511,x513,x514) % 63.63/63.80 [52]P11(x523,x522,x524)+~E(x521,x522)+~P11(x523,x521,x524) % 63.63/63.80 [53]P11(x533,x534,x532)+~E(x531,x532)+~P11(x533,x534,x531) % 63.63/63.80 [54]~P20(x541)+P20(x542)+~E(x541,x542) % 63.63/63.80 [55]~P27(x551)+P27(x552)+~E(x551,x552) % 63.63/63.80 [56]~P4(x561)+P4(x562)+~E(x561,x562) % 63.63/63.80 [57]~P21(x571)+P21(x572)+~E(x571,x572) % 63.63/63.80 [58]~P25(x581)+P25(x582)+~E(x581,x582) % 63.63/63.80 [59]P15(x592,x593)+~E(x591,x592)+~P15(x591,x593) % 63.63/63.80 [60]P15(x603,x602)+~E(x601,x602)+~P15(x603,x601) % 63.63/63.80 [61]P9(x612,x613)+~E(x611,x612)+~P9(x611,x613) % 63.63/63.80 [62]P9(x623,x622)+~E(x621,x622)+~P9(x623,x621) % 63.63/63.80 [63]~P5(x631)+P5(x632)+~E(x631,x632) % 63.63/63.80 [64]~P7(x641)+P7(x642)+~E(x641,x642) % 63.63/63.80 [65]~P6(x651)+P6(x652)+~E(x651,x652) % 63.63/63.80 [66]~P16(x661)+P16(x662)+~E(x661,x662) % 63.63/63.80 [67]~P28(x671)+P28(x672)+~E(x671,x672) % 63.63/63.80 [68]P8(x682,x683)+~E(x681,x682)+~P8(x681,x683) % 63.63/63.80 [69]P8(x693,x692)+~E(x691,x692)+~P8(x693,x691) % 63.63/63.80 [70]~P32(x701)+P32(x702)+~E(x701,x702) % 63.63/63.80 [71]~P34(x711)+P34(x712)+~E(x711,x712) % 63.63/63.80 [72]P24(x722,x723,x724)+~E(x721,x722)+~P24(x721,x723,x724) % 63.63/63.80 [73]P24(x733,x732,x734)+~E(x731,x732)+~P24(x733,x731,x734) % 63.63/63.80 [74]P24(x743,x744,x742)+~E(x741,x742)+~P24(x743,x744,x741) % 63.63/63.80 [75]P13(x752,x753,x754)+~E(x751,x752)+~P13(x751,x753,x754) % 63.63/63.80 [76]P13(x763,x762,x764)+~E(x761,x762)+~P13(x763,x761,x764) % 63.63/63.80 [77]P13(x773,x774,x772)+~E(x771,x772)+~P13(x773,x774,x771) % 63.63/63.80 [78]~P31(x781)+P31(x782)+~E(x781,x782) % 63.63/63.80 [79]P14(x792,x793,x794)+~E(x791,x792)+~P14(x791,x793,x794) % 63.63/63.80 [80]P14(x803,x802,x804)+~E(x801,x802)+~P14(x803,x801,x804) % 63.63/63.80 [81]P14(x813,x814,x812)+~E(x811,x812)+~P14(x813,x814,x811) % 63.63/63.80 [82]~P18(x821)+P18(x822)+~E(x821,x822) % 63.63/63.80 [83]~P30(x831)+P30(x832)+~E(x831,x832) % 63.63/63.80 [84]~P19(x841)+P19(x842)+~E(x841,x842) % 63.63/63.80 [85]~P17(x851)+P17(x852)+~E(x851,x852) % 63.63/63.80 [86]~P29(x861)+P29(x862)+~E(x861,x862) % 63.63/63.80 [87]~P33(x871)+P33(x872)+~E(x871,x872) % 63.63/63.80 % 63.63/63.80 %------------------------------------------- % 63.79/63.82 cnf(210,plain, % 63.79/63.82 (~P15(x2101,a23)), % 63.79/63.82 inference(scs_inference,[],[101,142])). % 63.79/63.82 cnf(212,plain, % 63.79/63.82 (P8(f3(f27(x2121)),x2121)), % 63.79/63.82 inference(scs_inference,[],[101,110,142,164])). % 63.79/63.82 cnf(213,plain, % 63.79/63.82 (P9(f3(x2131),x2131)), % 63.79/63.82 inference(rename_variables,[],[110])). % 63.79/63.82 cnf(216,plain, % 63.79/63.82 (P9(f3(x2161),x2161)), % 63.79/63.82 inference(rename_variables,[],[110])). % 63.79/63.82 cnf(218,plain, % 63.79/63.82 (P15(f3(a15),a15)), % 63.79/63.82 inference(scs_inference,[],[101,127,110,213,216,142,164,170,159])). % 63.79/63.82 cnf(219,plain, % 63.79/63.82 (P9(f3(x2191),x2191)), % 63.79/63.82 inference(rename_variables,[],[110])). % 63.79/63.82 cnf(221,plain, % 63.79/63.82 (~P15(x2211,f3(f27(a23)))), % 63.79/63.82 inference(scs_inference,[],[101,127,110,213,216,219,142,164,170,159,167])). % 63.79/63.82 cnf(224,plain, % 63.79/63.82 (~E(a15,a23)), % 63.79/63.82 inference(scs_inference,[],[101,127,110,213,216,219,142,164,170,159,167,60])). % 63.79/63.82 cnf(225,plain, % 63.79/63.82 (P24(f5(x2251,a15),x2251,a15)), % 63.79/63.82 inference(scs_inference,[],[119,122,101,127,112,110,213,216,219,142,164,170,159,167,60,192])). % 63.79/63.82 cnf(226,plain, % 63.79/63.82 (P10(f5(x2261,x2262),x2261,x2262)), % 63.79/63.82 inference(rename_variables,[],[122])). % 63.79/63.82 cnf(227,plain, % 63.79/63.82 (P3(f5(x2271,x2272))), % 63.79/63.82 inference(rename_variables,[],[112])). % 63.79/63.82 cnf(228,plain, % 63.79/63.82 (P23(f5(x2281,x2282),x2281,x2282)), % 63.79/63.82 inference(rename_variables,[],[119])). % 63.79/63.82 cnf(230,plain, % 63.79/63.82 (~P25(f5(a15,a15))), % 63.79/63.82 inference(scs_inference,[],[119,228,122,226,101,127,112,227,110,213,216,219,142,164,170,159,167,60,192,190])). % 63.79/63.82 cnf(235,plain, % 63.79/63.82 (P14(f29(a1,a12,a18),f24(a1),f24(a12))), % 63.79/63.82 inference(scs_inference,[],[88,89,90,91,92,93,95,116,124,125,117,118,119,228,122,226,101,127,112,227,110,213,216,219,142,164,170,159,167,60,192,190,200])). % 63.79/63.82 cnf(237,plain, % 63.79/63.82 (P13(f29(a1,a12,a18),f24(a1),f24(a12))), % 63.79/63.82 inference(scs_inference,[],[88,89,90,91,92,93,95,97,116,124,125,117,118,119,228,122,226,101,127,112,227,110,213,216,219,142,164,170,159,167,60,192,190,200,201])). % 63.79/63.82 cnf(253,plain, % 63.79/63.82 (~P15(x2531,a2)), % 63.79/63.82 inference(scs_inference,[],[102,142])). % 63.79/63.82 cnf(255,plain, % 63.79/63.82 (P21(f14(f30(x2551,x2552)))), % 63.79/63.82 inference(scs_inference,[],[102,111,142,170])). % 63.79/63.82 cnf(256,plain, % 63.79/63.82 (P9(f14(x2561),f27(x2561))), % 63.79/63.82 inference(rename_variables,[],[111])). % 63.79/63.82 cnf(258,plain, % 63.79/63.82 (P8(f14(x2581),x2581)), % 63.79/63.82 inference(scs_inference,[],[102,111,256,142,170,164])). % 63.79/63.82 cnf(260,plain, % 63.79/63.82 (P15(f3(f5(a15,a15)),f5(a15,a15))), % 63.79/63.82 inference(scs_inference,[],[230,102,111,256,110,142,170,164,159])). % 63.79/63.82 cnf(268,plain, % 63.79/63.82 (P24(f5(x2681,f5(a15,a15)),x2681,f5(a15,a15))), % 63.79/63.82 inference(scs_inference,[],[230,221,218,102,119,122,112,111,256,110,142,170,164,159,167,60,192])). % 63.79/63.82 cnf(269,plain, % 63.79/63.82 (P10(f5(x2691,x2692),x2691,x2692)), % 63.79/63.82 inference(rename_variables,[],[122])). % 63.79/63.82 cnf(270,plain, % 63.79/63.82 (P3(f5(x2701,x2702))), % 63.79/63.82 inference(rename_variables,[],[112])). % 63.79/63.82 cnf(271,plain, % 63.79/63.82 (P23(f5(x2711,x2712),x2711,x2712)), % 63.79/63.82 inference(rename_variables,[],[119])). % 63.79/63.82 cnf(273,plain, % 63.79/63.82 (~P25(f5(f5(a15,a15),f5(a15,a15)))), % 63.79/63.82 inference(scs_inference,[],[230,221,218,102,119,271,122,269,112,270,111,256,110,142,170,164,159,167,60,192,190])). % 63.79/63.82 cnf(284,plain, % 63.79/63.82 (P10(f4(x2841,x2842),x2843,x2842)+~E(x2841,x2843)), % 63.79/63.82 inference(scs_inference,[],[117,230,221,121,218,102,119,271,122,269,112,270,111,256,110,142,170,164,159,167,60,192,190,163,48,49,50,36,37])). % 63.79/63.82 cnf(285,plain, % 63.79/63.82 (P10(f4(x2851,x2852),x2851,x2853)+~E(x2852,x2853)), % 63.79/63.82 inference(scs_inference,[],[117,230,221,121,218,102,119,271,122,269,112,270,111,256,110,142,170,164,159,167,60,192,190,163,48,49,50,36,37,38])). % 63.79/63.82 cnf(292,plain, % 63.79/63.82 (~P15(x2921,a9)), % 63.79/63.82 inference(scs_inference,[],[103,142])). % 63.79/63.82 cnf(294,plain, % 63.79/63.82 (P15(f14(x2941),f27(x2941))), % 63.79/63.82 inference(scs_inference,[],[103,128,111,142,159])). % 63.79/63.82 cnf(297,plain, % 63.79/63.82 (~P15(x2971,f14(a9))), % 63.79/63.82 inference(scs_inference,[],[103,128,111,142,159,167])). % 63.79/63.82 cnf(306,plain, % 63.79/63.82 (~P15(x3061,f14(x3062))), % 63.79/63.82 inference(scs_inference,[],[108,142])). % 63.79/63.82 cnf(308,plain, % 63.79/63.82 (P15(f3(f27(x3081)),f27(x3081))), % 63.79/63.82 inference(scs_inference,[],[108,128,110,142,159])). % 63.79/63.82 cnf(309,plain, % 63.79/63.82 (P9(f3(x3091),x3091)), % 63.79/63.82 inference(rename_variables,[],[110])). % 63.79/63.82 cnf(311,plain, % 63.79/63.82 (~P15(x3111,f3(f27(f14(x3112))))), % 63.79/63.82 inference(scs_inference,[],[108,128,110,309,142,159,167])). % 63.79/63.82 cnf(318,plain, % 63.79/63.82 (P24(f5(x3181,a15),x3182,a15)+~E(x3181,x3182)), % 63.79/63.82 inference(scs_inference,[],[225,218,297,108,128,110,309,142,159,167,60,163,73])). % 63.79/63.82 cnf(334,plain, % 63.79/63.82 (P9(x3341,x3342)+~P15(x3341,f3(f27(x3342)))), % 63.79/63.82 inference(scs_inference,[],[235,260,306,110,60,80,81,168])). % 63.79/63.82 cnf(337,plain, % 63.79/63.82 (P23(f5(x3371,x3372),x3371,x3373)+~E(x3372,x3373)), % 63.79/63.82 inference(scs_inference,[],[235,260,306,119,110,60,80,81,168,50])). % 63.79/63.82 cnf(339,plain, % 63.79/63.82 (P8(x3391,x3392)+~E(f14(x3392),x3391)), % 63.79/63.82 inference(scs_inference,[],[235,260,306,123,119,110,258,60,80,81,168,50,36,68])). % 63.79/63.82 cnf(347,plain, % 63.79/63.83 (P8(f3(f27(x3471)),x3472)+~E(x3471,x3472)), % 63.79/63.83 inference(scs_inference,[],[218,311,212,60,69])). % 63.79/63.83 cnf(350,plain, % 63.79/63.83 (P9(x3501,f27(x3502))+~E(f14(x3502),x3501)), % 63.79/63.83 inference(scs_inference,[],[218,311,119,111,212,60,69,48,62,61])). % 63.79/63.83 cnf(352,plain, % 63.79/63.83 (P12(f6(x3521,x3522),x3523,x3522)+~E(x3521,x3523)), % 63.79/63.83 inference(scs_inference,[],[268,218,311,120,119,111,212,60,69,48,62,61,74,46])). % 63.79/63.83 cnf(361,plain, % 63.79/63.83 (P23(f5(x3611,x3612),x3613,x3612)+~E(x3611,x3613)), % 63.79/63.83 inference(scs_inference,[],[260,210,119,60,49])). % 63.79/63.83 cnf(362,plain, % 63.79/63.83 (P24(x3621,x3622,a15)+~E(f5(x3622,a15),x3621)), % 63.79/63.83 inference(scs_inference,[],[225,260,210,119,60,49,72])). % 63.79/63.83 cnf(364,plain, % 63.79/63.83 (P10(f5(x3641,x3642),x3641,x3643)+~E(x3642,x3643)), % 63.79/63.83 inference(scs_inference,[],[225,260,122,210,120,119,60,49,72,45,38])). % 63.79/63.83 cnf(365,plain, % 63.79/63.83 (P24(f5(x3651,f5(a15,a15)),x3652,f5(a15,a15))+~E(x3651,x3652)), % 63.79/63.83 inference(scs_inference,[],[225,268,260,122,210,120,119,60,49,72,45,38,73])). % 63.79/63.83 cnf(366,plain, % 63.79/63.83 (P10(f5(x3661,x3662),x3663,x3662)+~E(x3661,x3663)), % 63.79/63.83 inference(scs_inference,[],[225,268,260,122,210,120,119,60,49,72,45,38,73,37])). % 63.79/63.83 cnf(375,plain, % 63.79/63.83 (P12(f6(x3751,x3752),x3751,x3753)+~E(x3752,x3753)), % 63.79/63.83 inference(scs_inference,[],[218,253,120,60,47])). % 63.79/63.83 cnf(378,plain, % 63.79/63.83 (P9(f3(x3781),x3782)+~E(x3781,x3782)), % 63.79/63.83 inference(scs_inference,[],[218,253,120,110,212,60,47,59,68,62])). % 63.79/63.83 cnf(380,plain, % 63.79/63.83 (P12(f6(x3801,x3802),x3803,x3804)+~E(x3802,x3804)+~E(x3801,x3803)), % 63.79/63.83 inference(scs_inference,[],[218,122,253,120,110,212,60,47,46])). % 63.79/63.83 cnf(388,plain, % 63.79/63.83 (P24(x3881,x3882,f5(a15,a15))+~E(f5(x3882,f5(a15,a15)),x3881)), % 63.79/63.83 inference(scs_inference,[],[268,260,292,60,72])). % 63.79/63.83 cnf(393,plain, % 63.79/63.83 (P8(x3931,x3932)+~E(x3932,x3931)), % 63.79/63.83 inference(scs_inference,[],[218,306,109,60,68])). % 63.79/63.83 cnf(394,plain, % 63.79/63.83 (P15(x3941,f27(x3942))+~E(f14(x3942),x3941)), % 63.79/63.83 inference(scs_inference,[],[218,294,306,109,60,68,59])). % 63.79/63.83 cnf(395,plain, % 63.79/63.83 (P10(f11(x3951,x3952),x3951,x3953)+~E(x3952,x3953)), % 63.79/63.83 inference(scs_inference,[],[218,294,306,123,109,60,68,59,38])). % 63.79/63.83 cnf(396,plain, % 63.79/63.83 (P9(x3961,x3962)+~E(f3(x3962),x3961)), % 63.79/63.83 inference(scs_inference,[],[218,294,306,123,110,109,60,68,59,38,61])). % 63.79/63.83 cnf(404,plain, % 63.79/63.83 (P10(f11(x4041,x4042),x4043,x4042)+~E(x4041,x4043)), % 63.79/63.83 inference(scs_inference,[],[260,123,311,60,37])). % 63.79/63.83 cnf(411,plain, % 63.79/63.83 (P8(f14(x4111),x4112)+~E(x4111,x4112)), % 63.79/63.83 inference(scs_inference,[],[260,221,258,60,69])). % 63.79/63.83 cnf(420,plain, % 63.79/63.83 (P8(x4201,x4202)+~E(x4201,x4202)), % 63.79/63.83 inference(scs_inference,[],[294,210,109,60,69])). % 63.79/63.83 cnf(456,plain, % 63.79/63.83 (~P25(f28(a12))), % 63.79/63.83 inference(scs_inference,[],[93,125,131,140])). % 63.79/63.83 cnf(866,plain, % 63.79/63.83 (~P25(f10(a15))), % 63.79/63.83 inference(scs_inference,[],[224,130,139])). % 63.79/63.83 cnf(1192,plain, % 63.79/63.83 (~E(x11921,x11922)+P9(f3(f27(x11921)),f27(x11922))), % 63.79/63.83 inference(scs_inference,[],[162,347])). % 63.79/63.83 cnf(1421,plain, % 63.79/63.83 (~E(x14211,x14212)+E(f27(f14(x14211)),f27(f14(x14212)))), % 63.79/63.83 inference(scs_inference,[],[8,4])). % 63.79/63.83 cnf(1575,plain, % 63.79/63.83 (~E(x15751,x15752)+E(f24(f3(x15751)),f24(f3(x15752)))), % 63.79/63.83 inference(scs_inference,[],[14,5])). % 63.79/63.83 cnf(1729,plain, % 63.79/63.83 (~E(x17291,x17292)+E(f32(f27(x17291)),f32(f27(x17292)))), % 63.79/63.83 inference(scs_inference,[],[22,8])). % 63.79/63.83 cnf(1883,plain, % 63.79/63.83 (~E(x18831,x18832)+E(f16(f28(x18831)),f16(f28(x18832)))), % 63.79/63.83 inference(scs_inference,[],[28,13])). % 63.79/63.83 cnf(1960,plain, % 63.79/63.83 (P9(f4(x19601,x19602),f27(f30(x19601,x19602)))), % 63.79/63.83 inference(scs_inference,[],[121,181,183])). % 63.79/63.83 cnf(1968,plain, % 63.79/63.83 (~P15(f27(f30(x19681,x19682)),f4(x19681,x19682))), % 63.79/63.83 inference(scs_inference,[],[1960,128,164,170,159,163])). % 63.79/63.83 cnf(2591,plain, % 63.79/63.83 (~E(x25911,x25912)+E(f30(x25913,f30(x25911,x25914)),f30(x25913,f30(x25912,x25914)))), % 63.79/63.83 inference(scs_inference,[],[7,6])). % 63.79/63.83 cnf(2745,plain, % 63.79/63.83 (~E(x27451,x27452)+E(f5(x27453,f30(x27454,x27451)),f5(x27453,f30(x27454,x27452)))), % 63.79/63.83 inference(scs_inference,[],[10,7])). % 63.79/63.83 cnf(2899,plain, % 63.79/63.83 (~E(x28991,x28992)+E(f11(x28993,f5(x28991,x28994)),f11(x28993,f5(x28992,x28994)))), % 63.79/63.83 inference(scs_inference,[],[12,9])). % 63.79/63.83 cnf(3053,plain, % 63.79/63.83 (~E(x30531,x30532)+E(f6(x30533,f5(x30534,x30531)),f6(x30533,f5(x30534,x30532)))), % 63.79/63.83 inference(scs_inference,[],[25,10])). % 63.79/63.83 cnf(3207,plain, % 63.79/63.83 (~E(x32071,x32072)+E(f4(x32073,f11(x32071,x32074)),f4(x32073,f11(x32072,x32074)))), % 63.79/63.83 inference(scs_inference,[],[27,11])). % 63.79/63.83 cnf(3361,plain, % 63.79/63.83 (~E(x33611,x33612)+E(f8(x33613,f11(x33614,x33611)),f8(x33613,f11(x33614,x33612)))), % 63.79/63.83 inference(scs_inference,[],[30,12])). % 63.79/63.83 cnf(3515,plain, % 63.79/63.83 (~E(x35151,x35152)+E(f26(x35153,f24(x35151)),f26(x35153,f24(x35152)))), % 63.79/63.83 inference(scs_inference,[],[32,14])). % 63.79/63.83 cnf(3669,plain, % 63.79/63.83 (~E(x36691,x36692)+E(f7(x36693,f31(x36691)),f7(x36693,f31(x36692)))), % 63.79/63.83 inference(scs_inference,[],[34,21])). % 63.79/63.83 cnf(4051,plain, % 63.79/63.83 (~E(x40511,x40512)+E(f29(x40513,f29(x40511,x40514,x40515),x40516),f29(x40513,f29(x40512,x40514,x40515),x40516))), % 63.79/63.83 inference(scs_inference,[],[16,15])). % 63.79/63.83 cnf(4205,plain, % 63.79/63.83 (~E(x42051,x42052)+E(f25(f29(x42053,x42051,x42054),x42055,x42056),f25(f29(x42053,x42052,x42054),x42055,x42056))), % 63.79/63.83 inference(scs_inference,[],[18,16])). % 63.79/63.83 cnf(4359,plain, % 63.79/63.83 (~E(x43591,x43592)+E(f25(x43593,x43594,f29(x43595,x43596,x43591)),f25(x43593,x43594,f29(x43595,x43596,x43592)))), % 63.79/63.83 inference(scs_inference,[],[20,17])). % 63.79/63.83 cnf(8587,plain, % 63.79/63.83 (~P11(x85871,x85872,f24(a12))+~E(x85871,f29(a1,a12,a18))+~E(x85872,f24(a1))), % 63.79/63.83 inference(scs_inference,[],[129,51,52])). % 63.79/63.83 cnf(10797,plain, % 63.79/63.83 (~P25(f16(a12))), % 63.79/63.83 inference(scs_inference,[],[93,125,131,141])). % 63.79/63.83 cnf(10798,plain, % 63.79/63.83 (P15(f3(f16(a12)),f16(a12))), % 63.79/63.83 inference(scs_inference,[],[10797,110,159])). % 63.79/63.83 cnf(10902,plain, % 63.79/63.83 (~P25(f28(a1))), % 63.79/63.83 inference(scs_inference,[],[92,124,131,140])). % 63.79/63.83 cnf(11084,plain, % 63.79/63.83 (P9(f16(a1),f27(f28(a1)))), % 63.79/63.83 inference(scs_inference,[],[92,124,131,165])). % 63.79/63.83 cnf(11383,plain, % 63.79/63.83 (~P15(f27(f28(a1)),f16(a1))), % 63.79/63.83 inference(scs_inference,[],[11084,128,159,163])). % 63.79/63.83 cnf(11476,plain, % 63.79/63.83 (P9(f16(a12),f27(f28(a12)))), % 63.79/63.83 inference(scs_inference,[],[93,125,131,165])). % 63.79/63.83 cnf(11479,plain, % 63.79/63.83 (P9(f3(f16(a12)),f28(a12))), % 63.79/63.83 inference(scs_inference,[],[11476,10798,164,168])). % 63.79/63.83 cnf(12530,plain, % 63.79/63.83 (P15(f3(f16(a12)),f28(a12))), % 63.79/63.83 inference(scs_inference,[],[456,11479,159])). % 63.79/63.83 cnf(12555,plain, % 63.79/63.83 (~P25(f16(a1))), % 63.79/63.83 inference(scs_inference,[],[92,124,131,141])). % 63.79/63.83 cnf(12556,plain, % 63.79/63.83 (P15(f3(f16(a1)),f16(a1))), % 63.79/63.83 inference(scs_inference,[],[12555,110,159])). % 63.79/63.83 cnf(12560,plain, % 63.79/63.83 (P9(f3(f16(a1)),f28(a1))), % 63.79/63.83 inference(scs_inference,[],[11084,12555,110,11383,159,59,168])). % 63.79/63.83 cnf(12626,plain, % 63.79/63.83 (~E(f16(a1),f14(x126261))), % 63.79/63.83 inference(scs_inference,[],[12556,306,60])). % 63.79/63.83 cnf(13133,plain, % 63.79/63.83 (P15(f3(f16(a1)),f28(a1))), % 63.79/63.83 inference(scs_inference,[],[10902,12560,159])). % 63.79/63.83 cnf(13146,plain, % 63.79/63.83 (~P15(f27(f28(a12)),f16(a12))), % 63.79/63.83 inference(scs_inference,[],[11476,128,159,163])). % 63.79/63.83 cnf(14722,plain, % 63.79/63.83 (P6(f24(a12))), % 63.79/63.83 inference(scs_inference,[],[91,93,125,89,134,144])). % 63.79/63.83 cnf(14875,plain, % 63.79/63.83 (P6(f24(a1))), % 63.79/63.83 inference(scs_inference,[],[90,92,124,88,134,144])). % 63.79/63.83 cnf(15255,plain, % 63.79/63.83 (P7(f24(a1))), % 63.79/63.83 inference(scs_inference,[],[90,92,124,88,135,144])). % 63.79/63.83 cnf(15637,plain, % 63.79/63.83 (P7(f24(a12))), % 63.79/63.83 inference(scs_inference,[],[91,93,125,89,135,144])). % 63.79/63.83 cnf(15713,plain, % 63.79/63.83 (P7(f25(x157131,f5(f30(x157131,x157131),x157131),f5(f30(x157131,x157131),x157131)))), % 63.79/63.83 inference(scs_inference,[],[119,122,112,135,202])). % 63.79/63.83 cnf(15864,plain, % 63.79/63.83 (E(a23,f14(x158641))), % 63.79/63.83 inference(scs_inference,[],[108,130,2])). % 63.79/63.83 cnf(15865,plain, % 63.79/63.83 (P23(f5(x158651,a23),x158651,f14(x158652))), % 63.79/63.83 inference(scs_inference,[],[15864,337])). % 63.79/63.83 cnf(15866,plain, % 63.79/63.83 (P12(f6(a23,x158661),f14(x158662),x158661)), % 63.79/63.83 inference(scs_inference,[],[15864,337,352])). % 63.79/63.83 cnf(15867,plain, % 63.79/63.83 (P23(f5(a23,x158671),f14(x158672),x158671)), % 63.79/63.83 inference(scs_inference,[],[15864,337,352,361])). % 63.79/63.83 cnf(15868,plain, % 63.79/63.83 (P12(f6(x158681,a23),x158681,f14(x158682))), % 63.79/63.83 inference(scs_inference,[],[15864,337,352,361,375])). % 63.79/63.83 cnf(15869,plain, % 63.79/63.83 (P10(f4(a23,x158691),f14(x158692),x158691)), % 63.79/63.83 inference(scs_inference,[],[15864,337,352,361,375,284])). % 63.79/63.83 cnf(15870,plain, % 63.79/63.83 (P10(f4(x158701,a23),x158701,f14(x158702))), % 63.79/63.83 inference(scs_inference,[],[15864,337,352,361,375,284,285])). % 63.79/63.83 cnf(15872,plain, % 63.79/63.83 (P10(f5(x158721,a23),x158721,f14(x158722))), % 63.79/63.83 inference(scs_inference,[],[15864,337,352,361,375,284,285,347,364])). % 63.79/63.83 cnf(15873,plain, % 63.79/63.83 (P10(f5(a23,x158731),f14(x158732),x158731)), % 63.79/63.83 inference(scs_inference,[],[15864,337,352,361,375,284,285,347,364,366])). % 63.79/63.83 cnf(15876,plain, % 63.79/63.83 (P10(f11(x158761,a23),x158761,f14(x158762))), % 63.79/63.83 inference(scs_inference,[],[15864,337,352,361,375,284,285,347,364,366,378,393,395])). % 63.79/63.83 cnf(15877,plain, % 63.79/63.83 (P10(f11(a23,x158771),f14(x158772),x158771)), % 63.79/63.83 inference(scs_inference,[],[15864,337,352,361,375,284,285,347,364,366,378,393,395,404])). % 63.79/63.83 cnf(15879,plain, % 63.79/63.83 (P8(a23,f14(x158791))), % 63.79/63.83 inference(scs_inference,[],[15864,337,352,361,375,284,285,347,364,366,378,393,395,404,411,420])). % 63.79/63.83 cnf(15880,plain, % 63.79/63.83 (E(f14(x158801),a23)), % 63.79/63.83 inference(scs_inference,[],[15864,337,352,361,375,284,285,347,364,366,378,393,395,404,411,420,2])). % 63.79/63.83 cnf(15882,plain, % 63.79/63.83 (P21(a23)), % 63.79/63.83 inference(scs_inference,[],[15864,255,337,352,361,375,284,285,347,364,366,378,393,395,404,411,420,2,380,57])). % 63.79/63.83 cnf(15884,plain, % 63.79/63.83 (E(a23,f14(x158841))), % 63.79/63.83 inference(rename_variables,[],[15864])). % 63.79/63.83 cnf(15888,plain, % 63.79/63.83 (P15(a23,f27(f30(x158881,x158882)))), % 63.79/63.83 inference(scs_inference,[],[294,15864,15884,258,255,337,352,361,375,284,285,347,364,366,378,393,395,404,411,420,2,380,57,37,46,68,59])). % 63.79/63.83 cnf(15890,plain, % 63.79/63.83 (P9(a23,f27(f30(x158901,x158902)))), % 63.79/63.83 inference(scs_inference,[],[294,15864,15884,111,258,255,337,352,361,375,284,285,347,364,366,378,393,395,404,411,420,2,380,57,37,46,68,59,61])). % 63.79/63.83 cnf(15905,plain, % 63.79/63.83 (P8(a23,x159051)), % 63.79/63.83 inference(scs_inference,[],[15880,339])). % 63.79/63.83 cnf(15906,plain, % 63.79/63.83 (P9(a23,f27(x159061))), % 63.79/63.83 inference(scs_inference,[],[15880,339,350])). % 63.79/63.83 cnf(15907,plain, % 63.79/63.83 (P15(a23,f27(x159071))), % 63.79/63.83 inference(scs_inference,[],[15880,339,350,394])). % 63.79/63.83 cnf(15908,plain, % 63.79/63.83 (P23(f5(f14(x159081),x159082),a23,x159082)), % 63.79/63.83 inference(scs_inference,[],[15880,339,350,394,361])). % 63.79/63.83 cnf(15909,plain, % 63.79/63.83 (P10(f5(x159091,f14(x159092)),x159091,a23)), % 63.79/63.83 inference(scs_inference,[],[15880,339,350,394,361,364])). % 63.79/63.83 cnf(15910,plain, % 63.79/63.83 (P12(f6(x159101,f14(x159102)),x159101,a23)), % 63.79/63.83 inference(scs_inference,[],[15880,339,350,394,361,364,375])). % 63.79/63.83 cnf(15911,plain, % 63.79/63.83 (P10(f4(f14(x159111),x159112),a23,x159112)), % 63.79/63.83 inference(scs_inference,[],[15880,339,350,394,361,364,375,284])). % 63.79/63.83 cnf(15912,plain, % 63.79/63.83 (P23(f5(x159121,f14(x159122)),x159121,a23)), % 63.79/63.83 inference(scs_inference,[],[15880,339,350,394,361,364,375,284,337])). % 63.79/63.83 cnf(15913,plain, % 63.79/63.83 (P8(f3(f27(f14(x159131))),a23)), % 63.79/63.83 inference(scs_inference,[],[15880,339,350,394,361,364,375,284,337,347])). % 63.79/63.83 cnf(15914,plain, % 63.79/63.83 (P10(f11(f14(x159141),x159142),a23,x159142)), % 63.79/63.83 inference(scs_inference,[],[15880,339,350,394,361,364,375,284,337,347,404])). % 63.79/63.83 cnf(15916,plain, % 63.79/63.83 (P10(f4(x159161,f14(x159162)),x159161,a23)), % 63.79/63.83 inference(scs_inference,[],[15880,339,350,394,361,364,375,284,337,347,404,378,285])). % 63.79/63.83 cnf(15917,plain, % 63.79/63.83 (P10(f5(f14(x159171),x159172),a23,x159172)), % 63.79/63.83 inference(scs_inference,[],[15880,339,350,394,361,364,375,284,337,347,404,378,285,366])). % 63.79/63.83 cnf(15918,plain, % 63.79/63.83 (P12(f6(f14(x159181),x159182),a23,x159182)), % 63.79/63.83 inference(scs_inference,[],[15880,339,350,394,361,364,375,284,337,347,404,378,285,366,352])). % 63.79/63.83 cnf(15919,plain, % 63.79/63.83 (P10(f11(x159191,f14(x159192)),x159191,a23)), % 63.79/63.83 inference(scs_inference,[],[15880,339,350,394,361,364,375,284,337,347,404,378,285,366,352,395])). % 63.79/63.83 cnf(15925,plain, % 63.79/63.83 (P10(f4(f14(x159251),a23),a23,f14(x159252))), % 63.79/63.83 inference(scs_inference,[],[15868,15870,15879,15880,15882,15864,339,350,394,361,364,375,284,337,347,404,378,285,366,352,395,57,380,46,68,37])). % 63.79/63.83 cnf(15929,plain, % 63.79/63.83 (P24(f5(f14(x159291),a15),a23,a15)), % 63.79/63.83 inference(scs_inference,[],[225,15868,15870,15879,15880,15888,15890,15882,15864,339,350,394,361,364,375,284,337,347,404,378,285,366,352,395,57,380,46,68,37,59,61,73])). % 63.79/63.83 cnf(15932,plain, % 63.79/63.83 (P23(f5(a23,x159321),f14(x159322),x159321)), % 63.79/63.83 inference(rename_variables,[],[15867])). % 63.79/63.83 cnf(15941,plain, % 63.79/63.83 (P24(f5(a23,f5(a15,a15)),f14(x159411),f5(a15,a15))), % 63.79/63.83 inference(scs_inference,[],[225,230,15865,15866,15867,15932,15868,15869,15870,15873,15879,15880,15888,15890,15882,15864,112,339,350,394,361,364,375,284,337,347,404,378,285,366,352,395,57,380,46,68,37,59,61,73,50,62,49,38,69,47,192])). % 63.79/63.83 cnf(15954,plain, % 63.79/63.83 (P12(f6(f14(x159541),x159542),f14(x159543),x159542)), % 63.79/63.83 inference(scs_inference,[],[15918,15864,46])). % 63.79/63.83 cnf(15957,plain, % 63.79/63.83 (P15(f14(x159571),f27(x159572))), % 63.79/63.83 inference(scs_inference,[],[15918,15864,15872,15907,46,37,59])). % 63.79/63.83 cnf(15961,plain, % 63.79/63.83 (P23(f5(x159611,f14(x159612)),x159611,f14(x159613))), % 63.79/63.83 inference(scs_inference,[],[15912,15918,15864,15872,15905,15906,15907,15929,46,37,59,68,61,73,50])). % 63.79/63.83 cnf(15962,plain, % 63.79/63.83 (P23(f5(f14(x159621),x159622),f14(x159623),x159622)), % 63.79/63.83 inference(scs_inference,[],[15908,15912,15918,15864,15872,15905,15906,15907,15929,46,37,59,68,61,73,50,49])). % 63.79/63.83 cnf(15965,plain, % 63.79/63.83 (P12(f6(x159651,f14(x159652)),x159651,f14(x159653))), % 63.79/63.83 inference(scs_inference,[],[15908,15910,15912,15918,15864,15872,15877,15905,15906,15907,15929,46,37,59,68,61,73,50,49,38,47])). % 63.79/63.83 cnf(15966,plain, % 63.79/63.83 (P24(f5(f14(x159661),f5(a15,a15)),a23,f5(a15,a15))), % 63.79/63.83 inference(scs_inference,[],[230,15908,15910,15912,15918,15864,15872,15877,15917,15905,15906,15907,15929,112,46,37,59,68,61,73,50,49,38,47,192])). % 63.79/63.83 cnf(15977,plain, % 63.79/63.83 (P12(f6(f14(x159771),f14(x159772)),a23,f14(x159773))), % 63.79/63.83 inference(scs_inference,[],[15965,15880,46])). % 63.79/63.83 cnf(15981,plain, % 63.79/63.83 (P23(f5(f14(x159811),f14(x159812)),f14(x159813),a23)), % 63.79/63.83 inference(scs_inference,[],[15962,15965,15880,15876,46,37,50])). % 63.79/63.83 cnf(15983,plain, % 63.79/63.83 (P24(f5(f14(x159831),f5(a15,a15)),f14(x159832),f5(a15,a15))), % 63.79/63.83 inference(scs_inference,[],[15962,15965,15966,15880,15864,15876,46,37,50,73])). % 63.79/63.83 cnf(15986,plain, % 63.79/63.83 (P10(f5(x159861,f14(x159862)),x159861,f14(x159863))), % 63.79/63.83 inference(scs_inference,[],[15961,15962,15965,15966,15880,15864,15876,15909,46,37,50,73,49,38])). % 63.79/63.83 cnf(15995,plain, % 63.79/63.83 (P12(f6(f14(x159951),f14(x159952)),f14(x159953),f14(x159954))), % 63.79/63.83 inference(scs_inference,[],[15977,15864,46])). % 63.79/63.83 cnf(15999,plain, % 63.79/63.83 (P10(f5(f14(x159991),x159992),f14(x159993),x159992)), % 63.79/63.83 inference(scs_inference,[],[15977,15981,15880,15864,15917,46,50,49,37])). % 63.79/63.83 cnf(16002,plain, % 63.79/63.83 (P12(f6(f14(x160021),f14(x160022)),a23,a23)), % 63.79/63.83 inference(scs_inference,[],[15977,15981,15880,15864,15873,15917,46,50,49,37,38,47])). % 63.79/63.83 cnf(16036,plain, % 63.79/63.83 (P10(f4(f14(x160361),x160362),f14(x160363),x160362)), % 63.79/63.83 inference(scs_inference,[],[15864,15911,37])). % 63.79/63.83 cnf(16042,plain, % 63.79/63.83 (P10(f11(f14(x160421),x160422),f14(x160423),x160422)), % 63.79/63.83 inference(scs_inference,[],[15864,15914,37])). % 63.79/63.84 cnf(16043,plain, % 63.79/63.84 (P10(f4(f14(x160431),f14(x160432)),f14(x160433),a23)), % 63.79/63.84 inference(scs_inference,[],[15880,15864,16036,15914,37,38])). % 63.79/63.84 cnf(16054,plain, % 63.79/63.84 (P10(f11(f14(x160541),f14(x160542)),f14(x160543),a23)), % 63.79/63.84 inference(scs_inference,[],[15880,16042,15919,37,38])). % 63.79/63.84 cnf(16065,plain, % 63.79/63.84 (P10(f4(f14(x160651),f14(x160652)),f14(x160653),f14(x160654))), % 63.79/63.84 inference(scs_inference,[],[15864,16043,15925,37,38])). % 63.79/63.84 cnf(16076,plain, % 63.79/63.84 (P10(f11(f14(x160761),f14(x160762)),f14(x160763),f14(x160764))), % 63.79/63.84 inference(scs_inference,[],[15880,15864,16065,16054,37,38])). % 63.79/63.84 cnf(16085,plain, % 63.79/63.84 (P10(f4(x160851,f14(x160852)),x160851,f14(x160853))), % 63.79/63.84 inference(scs_inference,[],[15880,15864,16076,15916,37,38])). % 63.79/63.84 cnf(16088,plain, % 63.79/63.84 (P10(x160881,a23,x160882)+~E(f5(f14(x160883),x160882),x160881)), % 63.79/63.84 inference(scs_inference,[],[15941,15995,15880,15864,15917,16076,15916,37,38,72,45,36])). % 63.79/63.84 cnf(16106,plain, % 63.79/63.84 (P10(f5(f14(x161061),a23),a23,f14(x161062))), % 63.79/63.84 inference(scs_inference,[],[15880,15872,37])). % 63.79/63.84 cnf(16119,plain, % 63.79/63.84 (P10(f11(a23,f14(x161191)),f14(x161192),a23)), % 63.79/63.84 inference(scs_inference,[],[15880,15864,16106,15877,37,38])). % 63.79/63.84 cnf(16121,plain, % 63.79/63.84 (P10(x161211,f14(x161212),x161213)+~E(f5(f14(x161214),x161213),x161211)), % 63.79/63.84 inference(scs_inference,[],[15880,15864,15999,16106,15877,37,38,36])). % 63.79/63.84 cnf(16134,plain, % 63.79/63.84 (P10(x161341,x161342,f14(x161343))+~E(f4(x161342,f14(x161344)),x161341)), % 63.79/63.84 inference(scs_inference,[],[15864,16085,16119,38,36])). % 63.79/63.84 cnf(16147,plain, % 63.79/63.84 (P10(f11(x161471,f14(x161472)),x161471,f14(x161473))), % 63.79/63.84 inference(scs_inference,[],[15864,15919,38])). % 63.79/63.84 cnf(16183,plain, % 63.79/63.84 (P23(x161831,x161832,f14(x161833))+~E(f5(x161832,f14(x161834)),x161831)), % 63.79/63.84 inference(scs_inference,[],[15961,48])). % 63.79/63.84 cnf(16184,plain, % 63.79/63.84 (P23(x161841,x161842,a23)+~E(f5(x161842,f14(x161843)),x161841)), % 63.79/63.84 inference(scs_inference,[],[15961,15880,48,50])). % 63.79/63.84 cnf(16188,plain, % 63.79/63.84 (P23(x161881,f14(x161882),x161883)+~E(f5(f14(x161884),x161883),x161881)), % 63.79/63.84 inference(scs_inference,[],[15962,48])). % 63.79/63.84 cnf(16189,plain, % 63.79/63.84 (P23(x161891,a23,x161892)+~E(f5(f14(x161893),x161892),x161891)), % 63.79/63.84 inference(scs_inference,[],[15962,15880,48,49])). % 63.79/63.84 cnf(16212,plain, % 63.79/63.84 (P10(x162121,f14(x162122),x162123)+~E(f11(f14(x162124),x162123),x162121)), % 63.79/63.84 inference(scs_inference,[],[15867,15983,16042,48,74,36])). % 63.79/63.84 cnf(16222,plain, % 63.79/63.84 (P12(x162221,f14(x162222),x162223)+~E(f6(f14(x162224),x162223),x162221)), % 63.79/63.84 inference(scs_inference,[],[15954,45])). % 63.79/63.84 cnf(16223,plain, % 63.79/63.84 (P12(x162231,a23,x162232)+~E(f6(f14(x162233),x162232),x162231)), % 63.79/63.84 inference(scs_inference,[],[15954,15880,45,46])). % 63.79/63.84 cnf(16234,plain, % 63.79/63.84 (P12(x162341,x162342,f14(x162343))+~E(f6(x162342,f14(x162344)),x162341)), % 63.79/63.84 inference(scs_inference,[],[15965,45])). % 63.79/63.84 cnf(16235,plain, % 63.79/63.84 (P12(x162351,x162352,a23)+~E(f6(x162352,f14(x162353)),x162351)), % 63.79/63.84 inference(scs_inference,[],[15965,15880,45,47])). % 63.79/63.84 cnf(16270,plain, % 63.79/63.84 (P10(x162701,a23,x162702)+~E(f11(f14(x162703),x162702),x162701)), % 63.79/63.84 inference(scs_inference,[],[15914,36])). % 63.79/63.84 cnf(16326,plain, % 63.79/63.84 (P10(x163261,x163262,f14(x163263))+~E(f5(x163262,f14(x163264)),x163261)), % 63.79/63.84 inference(scs_inference,[],[15986,36])). % 63.79/63.84 cnf(16327,plain, % 63.79/63.84 (P10(x163271,x163272,a23)+~E(f5(x163272,f14(x163273)),x163271)), % 63.79/63.84 inference(scs_inference,[],[15880,15986,36,38])). % 63.79/63.84 cnf(16331,plain, % 63.79/63.84 (P10(x163311,f14(x163312),x163313)+~E(f4(f14(x163314),x163313),x163311)), % 63.79/63.84 inference(scs_inference,[],[16036,36])). % 63.79/63.84 cnf(16373,plain, % 63.79/63.84 (P10(x163731,x163732,a23)+~E(f4(x163732,f14(x163733)),x163731)), % 63.79/63.84 inference(scs_inference,[],[15916,36])). % 63.79/63.84 cnf(16385,plain, % 63.79/63.84 (P10(x163851,a23,x163852)+~E(f4(f14(x163853),x163852),x163851)), % 63.79/63.84 inference(scs_inference,[],[15911,36])). % 63.79/63.84 cnf(16391,plain, % 63.79/63.84 (P10(x163911,x163912,a23)+~E(f11(x163912,f14(x163913)),x163911)), % 63.79/63.84 inference(scs_inference,[],[15919,36])). % 63.79/63.84 cnf(16392,plain, % 63.79/63.84 (P10(x163921,x163922,f14(x163923))+~E(f11(x163922,f14(x163924)),x163921)), % 63.79/63.84 inference(scs_inference,[],[15864,15919,36,38])). % 63.79/63.84 cnf(17111,plain, % 63.79/63.84 (P9(f3(f27(f14(x171111))),f27(a23))), % 63.79/63.84 inference(scs_inference,[],[14722,15255,273,15913,137,138,139,162])). % 63.79/63.84 cnf(17121,plain, % 63.79/63.84 (E(f27(a23),f27(f14(x171211)))), % 63.79/63.84 inference(scs_inference,[],[14722,15255,273,16147,16002,12555,15913,15864,137,138,139,162,181,182,143,4,5,8])). % 63.79/63.84 cnf(17135,plain, % 63.79/63.84 (E(f5(a23,x171351),f5(f14(x171352),x171351))), % 63.79/63.84 inference(scs_inference,[],[14722,15255,273,16147,16002,12555,15913,15864,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9])). % 63.79/63.84 cnf(17141,plain, % 63.79/63.84 (E(f4(a23,x171411),f4(f14(x171412),x171411))), % 63.79/63.84 inference(scs_inference,[],[14722,15255,273,16147,16002,12555,15913,15864,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26])). % 63.79/63.84 cnf(17161,plain, % 63.79/63.84 (P23(f32(a22),f30(f28(a22),f28(a22)),f28(a22))), % 63.79/63.84 inference(scs_inference,[],[14722,15255,273,16147,16002,12555,15913,107,15864,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174])). % 63.79/63.84 cnf(17163,plain, % 63.79/63.84 (P23(f31(a21),f30(f28(a21),f28(a21)),f28(a21))), % 63.79/63.84 inference(scs_inference,[],[14722,15255,273,16147,16002,12555,15913,106,107,15864,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175])). % 63.79/63.84 cnf(17165,plain, % 63.79/63.84 (P12(f32(a22),f30(f28(a22),f28(a22)),f28(a22))), % 63.79/63.84 inference(scs_inference,[],[14722,15255,273,16147,16002,12555,15913,106,107,15864,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176])). % 63.79/63.84 cnf(17167,plain, % 63.79/63.84 (P12(f31(a21),f30(f28(a21),f28(a21)),f28(a21))), % 63.79/63.84 inference(scs_inference,[],[14722,15255,273,16147,16002,12555,15913,106,107,15864,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177])). % 63.79/63.84 cnf(17179,plain, % 63.79/63.84 (E(a9,a23)), % 63.79/63.84 inference(scs_inference,[],[14722,15255,273,16147,16002,12555,15913,106,107,103,15864,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130])). % 63.79/63.84 cnf(17183,plain, % 63.79/63.84 (P5(f24(a12))), % 63.79/63.84 inference(scs_inference,[],[94,14722,15255,273,16147,16002,12555,15913,106,107,103,15864,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132])). % 63.79/63.84 cnf(17185,plain, % 63.79/63.84 (P5(f24(a1))), % 63.79/63.84 inference(scs_inference,[],[94,14722,15255,273,16147,16002,12555,15913,106,107,103,15864,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133])). % 63.79/63.84 cnf(17188,plain, % 63.79/63.84 (~P25(f28(a13))), % 63.79/63.84 inference(scs_inference,[],[94,105,126,14722,15255,273,12626,16147,16002,12555,15913,106,107,103,15864,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140])). % 63.79/63.84 cnf(17190,plain, % 63.79/63.84 (~P25(f16(a13))), % 63.79/63.84 inference(scs_inference,[],[94,105,126,14722,15255,273,12626,16147,16002,12555,15913,106,107,103,15864,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141])). % 63.79/63.84 cnf(17194,plain, % 63.79/63.84 (P9(f16(a13),f27(f28(a13)))), % 63.79/63.84 inference(scs_inference,[],[94,105,126,14722,15255,273,12626,16147,16002,12555,15913,106,107,103,15864,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141,166,165])). % 63.79/63.84 cnf(17196,plain, % 63.79/63.84 (~E(f14(x171961),f5(f5(a15,a15),f5(a15,a15)))), % 63.79/63.84 inference(scs_inference,[],[94,105,126,14722,15255,273,12626,16147,16002,12555,15913,106,107,108,103,15864,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141,166,165,58])). % 63.79/63.84 cnf(17201,plain, % 63.79/63.84 (~P9(f27(f28(a12)),f16(a12))), % 63.79/63.84 inference(scs_inference,[],[94,105,126,14722,15255,273,12626,15957,16147,16002,12555,10797,13146,15913,106,107,108,103,15864,15880,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141,166,165,58,3,380,167,159])). % 63.79/63.84 cnf(17205,plain, % 63.79/63.84 (~P9(f27(x172051),f27(a23))), % 63.79/63.84 inference(scs_inference,[],[94,105,126,14722,15255,273,15713,12626,15957,16147,16002,12555,10797,13146,15913,106,107,108,103,15864,15880,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141,166,165,58,3,380,167,159,64,62])). % 63.79/63.84 cnf(17208,plain, % 63.79/63.84 (P4(f24(a1))), % 63.79/63.84 inference(scs_inference,[],[88,94,105,126,14722,15255,273,15713,12626,15957,16147,16002,12555,10797,13146,15913,106,107,308,108,103,124,92,15864,90,15880,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141,166,165,58,3,380,167,159,64,62,60,144])). % 63.79/63.84 cnf(17212,plain, % 63.79/63.84 (P16(f24(a1))), % 63.79/63.84 inference(scs_inference,[],[88,94,105,126,14722,15255,273,15713,12626,15957,16147,16002,12555,10797,13146,15913,106,107,308,108,103,124,92,15864,90,15880,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141,166,165,58,3,380,167,159,64,62,60,144,146,148])). % 63.79/63.84 cnf(17232,plain, % 63.79/63.84 (~P27(f24(a1))), % 63.79/63.84 inference(scs_inference,[],[88,94,105,126,14722,15255,273,15713,12626,15957,16147,16002,12555,10797,13146,15913,106,107,308,108,103,124,92,15864,90,15880,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141,166,165,58,3,380,167,159,64,62,60,144,146,148,149,150,151,152,153,154,155,156,157,161])). % 63.79/63.84 cnf(17234,plain, % 63.79/63.84 (P11(f26(f24(a1),f24(a1)),f24(a1),f24(a1))), % 63.79/63.84 inference(scs_inference,[],[88,94,105,126,14722,15255,273,15713,12626,15957,16147,16002,12555,10797,13146,15913,106,107,308,108,103,124,92,15864,90,15880,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141,166,165,58,3,380,167,159,64,62,60,144,146,148,149,150,151,152,153,154,155,156,157,161,171])). % 63.79/63.84 cnf(17236,plain, % 63.79/63.84 (P13(f7(f24(a1),f24(a1)),f24(a1),f24(a1))), % 63.79/63.84 inference(scs_inference,[],[88,94,105,126,14722,15255,273,15713,12626,15957,16147,16002,12555,10797,13146,15913,106,107,308,108,103,124,92,15864,90,15880,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141,166,165,58,3,380,167,159,64,62,60,144,146,148,149,150,151,152,153,154,155,156,157,161,171,172])). % 63.79/63.84 cnf(17238,plain, % 63.79/63.84 (P14(f8(f24(a1),f24(a1)),f24(a1),f24(a1))), % 63.79/63.84 inference(scs_inference,[],[88,94,105,126,14722,15255,273,15713,12626,15957,16147,16002,12555,10797,13146,15913,106,107,308,108,103,124,92,15864,90,15880,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141,166,165,58,3,380,167,159,64,62,60,144,146,148,149,150,151,152,153,154,155,156,157,161,171,172,173])). % 63.79/63.84 cnf(17241,plain, % 63.79/63.84 (P23(f5(x172411,f14(x172412)),x172411,a23)), % 63.79/63.84 inference(rename_variables,[],[15912])). % 63.79/63.84 cnf(17242,plain, % 63.79/63.84 (P10(f5(x172421,f14(x172422)),x172421,a23)), % 63.79/63.84 inference(rename_variables,[],[15909])). % 63.79/63.84 cnf(17243,plain, % 63.79/63.84 (P3(f5(x172431,x172432))), % 63.79/63.84 inference(rename_variables,[],[112])). % 63.79/63.84 cnf(17248,plain, % 63.79/63.84 (P3(f5(x172481,x172482))), % 63.79/63.84 inference(rename_variables,[],[112])). % 63.79/63.84 cnf(17250,plain, % 63.79/63.84 (P23(f26(f24(a1),f24(a1)),f28(f24(a1)),f28(f24(a1)))), % 63.79/63.84 inference(scs_inference,[],[88,94,105,126,14722,15255,273,15713,12626,15957,16147,16002,12555,10797,13146,15913,15912,17241,15909,17242,106,107,308,108,103,124,92,15864,90,112,17243,15880,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141,166,165,58,3,380,167,159,64,62,60,144,146,148,149,150,151,152,153,154,155,156,157,161,171,172,173,202,203,184])). % 63.79/63.84 cnf(17256,plain, % 63.79/63.84 (P12(f26(f24(a1),f24(a1)),f28(f24(a1)),f28(f24(a1)))), % 63.79/63.84 inference(scs_inference,[],[88,94,105,126,14722,15255,273,15713,12626,15957,16147,16002,12555,10797,13146,15913,15912,17241,15909,17242,106,107,308,108,103,124,92,15864,90,112,17243,15880,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141,166,165,58,3,380,167,159,64,62,60,144,146,148,149,150,151,152,153,154,155,156,157,161,171,172,173,202,203,184,185,186,187])). % 63.79/63.84 cnf(17277,plain, % 63.79/63.84 (P10(f5(f14(x172771),f30(x172772,f14(x172773))),f14(x172774),f30(x172772,a23))), % 63.79/63.84 inference(scs_inference,[],[88,94,105,126,14722,15255,273,15713,12626,15957,16147,16002,12555,10797,13146,15913,15912,17241,15909,17242,106,107,308,108,103,122,124,92,15864,90,112,17243,17248,119,15880,137,138,139,162,181,182,143,4,5,8,13,14,21,22,23,28,183,318,1192,6,7,9,10,11,12,24,25,26,27,29,30,31,32,33,34,1421,1575,1729,1883,15,16,17,18,19,20,3515,3669,174,175,176,177,2591,2745,2899,3053,3207,3361,365,4051,4205,4359,130,131,132,133,2,140,141,166,165,58,3,380,167,159,64,62,60,144,146,148,149,150,151,152,153,154,155,156,157,161,171,172,173,202,203,184,185,186,187,188,189,194,134,396,334,16088,16189,16223,16270,16385,16121])). % 63.79/63.84 cnf(17321,plain, % 63.79/63.84 (P10(f32(a22),f30(f28(a22),f28(a22)),f28(a22))), % 63.79/63.84 inference(scs_inference,[],[17205,17165,17277,334,181,182])). % 63.79/63.84 cnf(17323,plain, % 63.79/63.84 (E(a2,a23)), % 63.79/63.84 inference(scs_inference,[],[17205,17165,17277,102,334,181,182,130])). % 63.79/63.84 cnf(17325,plain, % 63.79/63.84 (~P25(f10(f28(a13)))), % 63.79/63.84 inference(scs_inference,[],[17205,17188,17165,17277,102,334,181,182,130,139])). % 63.79/63.84 cnf(17327,plain, % 63.79/63.84 (P9(x173271,f27(x173271))), % 63.79/63.84 inference(scs_inference,[],[17205,17188,17165,17277,109,102,334,181,182,130,139,162])). % 63.79/63.84 cnf(17334,plain, % 63.79/63.84 (E(f27(a9),f27(a23))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,17188,17165,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8])). % 63.79/63.84 cnf(17339,plain, % 63.79/63.84 (E(f29(x173391,a9,x173392),f29(x173391,a23,x173392))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17188,17165,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16])). % 63.79/63.84 cnf(17343,plain, % 63.79/63.84 (P10(f5(f14(x173431),f30(x173432,a23)),f14(x173433),f30(x173432,a9))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17188,17165,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121])). % 63.79/63.84 cnf(17353,plain, % 63.79/63.84 (E(f6(x173531,f5(x173532,a9)),f6(x173531,f5(x173532,a23)))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17188,17165,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053])). % 63.79/63.84 cnf(17366,plain, % 63.79/63.84 (E(f5(x173661,a9),f5(x173661,a23))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17188,17165,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10])). % 63.79/63.84 cnf(17371,plain, % 63.79/63.84 (P10(f11(f14(x173711),f5(a23,x173712)),f14(x173713),f5(a9,x173712))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17188,17165,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212])). % 63.79/63.84 cnf(17372,plain, % 63.79/63.84 (E(f4(x173721,a9),f4(x173721,a23))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17188,17165,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27])). % 63.79/63.84 cnf(17380,plain, % 63.79/63.84 (E(f5(a9,x173801),f5(a23,x173801))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17188,17165,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9])). % 63.79/63.84 cnf(17390,plain, % 63.79/63.84 (P12(f6(f14(x173901),a23),a23,a9)), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17188,17165,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223])). % 63.79/63.84 cnf(17393,plain, % 63.79/63.84 (E(f11(x173931,a9),f11(x173931,a23))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17188,17165,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12])). % 63.79/63.84 cnf(17396,plain, % 63.79/63.84 (E(f4(a9,x173961),f4(a23,x173961))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17188,17165,17196,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26])). % 63.79/63.84 cnf(17398,plain, % 63.79/63.84 (P10(f4(f14(x173981),f11(a23,x173982)),f14(x173983),f11(a9,x173982))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17188,17165,17196,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331])). % 63.79/63.84 cnf(17400,plain, % 63.79/63.84 (~P25(f30(f28(a13),f28(a13)))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17188,17165,17196,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166])). % 63.79/63.84 cnf(17402,plain, % 63.79/63.84 (~P25(f16(f24(a1)))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17185,17188,17232,17165,17196,17277,15910,109,102,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141])). % 63.79/63.84 cnf(17404,plain, % 63.79/63.84 (E(a9,f14(x174041))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17185,17188,17232,17165,17196,17277,15910,109,102,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3])). % 63.79/63.84 cnf(17407,plain, % 63.79/63.84 (~E(a23,f28(a13))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17185,17188,17232,17165,17196,17277,15910,109,101,102,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3,140,58])). % 63.79/63.84 cnf(17408,plain, % 63.79/63.84 (~P9(f28(a12),f27(a23))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17185,17188,17232,17165,17196,17277,12530,15910,109,101,102,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3,140,58,167])). % 63.79/63.84 cnf(17410,plain, % 63.79/63.84 (P15(f16(a13),f27(f28(a13)))), % 63.79/63.84 inference(scs_inference,[],[17179,17205,14875,15637,17185,17188,17232,17165,17196,17194,17277,12530,15910,109,128,101,102,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3,140,58,167,159])). % 63.79/63.84 cnf(17417,plain, % 63.79/63.84 (~P15(f27(f30(f14(x174171),x174172)),f4(a23,x174172))), % 63.79/63.84 inference(scs_inference,[],[98,17179,17205,14875,15637,17185,17188,17232,17165,17196,17141,17194,17277,17111,12530,1968,15910,109,128,101,102,110,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3,140,58,167,159,54,62,61,60])). % 63.79/63.84 cnf(17426,plain, % 63.79/63.84 (P16(f24(a12))), % 63.79/63.84 inference(scs_inference,[],[98,17179,17205,14875,15637,17185,17188,17232,17165,17196,17141,17194,17277,17111,12530,1968,15910,109,128,101,102,110,89,125,93,91,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3,140,58,167,159,54,62,61,60,154,150,151,148])). % 63.79/63.84 cnf(17436,plain, % 63.79/63.84 (P4(f24(a12))), % 63.79/63.84 inference(scs_inference,[],[98,17179,17205,14875,15637,17185,17188,17232,17165,17196,17141,17194,17277,17111,12530,1968,15910,109,128,101,102,110,89,125,93,91,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3,140,58,167,159,54,62,61,60,154,150,151,148,149,155,153,152,144])). % 63.79/63.84 cnf(17442,plain, % 63.79/63.84 (~P27(f24(a12))), % 63.79/63.84 inference(scs_inference,[],[98,17179,17205,14875,15637,17185,17188,17232,17165,17196,17141,17194,17277,17111,12530,1968,15910,109,128,101,102,110,89,125,93,91,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3,140,58,167,159,54,62,61,60,154,150,151,148,149,155,153,152,144,146,156,161])). % 63.79/63.84 cnf(17446,plain, % 63.79/63.84 (P13(f7(f24(a12),f24(a1)),f24(a12),f24(a1))), % 63.79/63.84 inference(scs_inference,[],[98,17179,17205,14875,15637,17185,17188,17208,17212,17232,17165,17196,17141,17194,17277,17111,12530,1968,15910,109,128,101,102,110,89,125,93,91,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3,140,58,167,159,54,62,61,60,154,150,151,148,149,155,153,152,144,146,156,161,157,172])). % 63.79/63.84 cnf(17448,plain, % 63.79/63.84 (P11(f26(f24(a12),f24(a1)),f24(a12),f24(a1))), % 63.79/63.84 inference(scs_inference,[],[98,17179,17205,14875,15637,17185,17188,17208,17212,17232,17165,17196,17141,17194,17277,17111,12530,1968,15910,109,128,101,102,110,89,125,93,91,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3,140,58,167,159,54,62,61,60,154,150,151,148,149,155,153,152,144,146,156,161,157,172,171])). % 63.79/63.84 cnf(17450,plain, % 63.79/63.84 (P14(f8(f24(a12),f24(a1)),f24(a12),f24(a1))), % 63.79/63.84 inference(scs_inference,[],[98,17179,17205,14875,15637,17185,17188,17208,17212,17232,17165,17196,17141,17194,17277,17111,12530,1968,15910,109,128,101,102,110,89,125,93,91,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3,140,58,167,159,54,62,61,60,154,150,151,148,149,155,153,152,144,146,156,161,157,172,171,173])). % 63.79/63.84 cnf(17479,plain, % 63.79/63.84 (P24(f5(a23,a15),a9,a15)), % 63.79/63.84 inference(scs_inference,[],[98,17179,17205,14875,15637,17185,17188,17208,17212,17232,17165,17234,17236,17238,17196,17141,17194,17277,17111,17256,17250,12530,1968,15910,109,128,101,102,110,122,89,125,93,91,112,119,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3,140,58,167,159,54,62,61,60,154,150,151,148,149,155,153,152,144,146,156,161,157,172,171,173,186,178,185,180,188,184,187,189,179,196,195,194,362])). % 63.79/63.84 cnf(17480,plain, % 63.79/63.84 (P12(f6(a23,f14(x174801)),a9,a23)), % 63.79/63.84 inference(scs_inference,[],[98,17179,17205,14875,15637,17185,17188,17208,17212,17232,17165,17234,17236,17238,17196,17141,17194,17277,17111,17256,17250,12530,1968,15910,109,128,101,102,110,122,89,125,93,91,112,119,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3,140,58,167,159,54,62,61,60,154,150,151,148,149,155,153,152,144,146,156,161,157,172,171,173,186,178,185,180,188,184,187,189,179,196,195,194,362,16235])). % 63.79/63.84 cnf(17486,plain, % 63.79/63.84 (~P15(f27(f28(a13)),f16(a13))), % 63.79/63.84 inference(scs_inference,[],[98,17179,17205,14875,15637,17185,17188,17208,17212,17232,17165,17234,17236,17238,17196,17141,17194,17277,17111,17256,17250,12530,1968,15910,109,128,101,102,110,122,89,125,93,91,112,119,15864,334,181,182,130,139,162,138,183,3207,8,2745,1729,137,16,11,25,19,16121,21,31,1192,143,3515,29,13,3053,18,365,16188,2591,15,16088,2899,16222,30,4205,34,16385,10,1883,318,24,28,16212,27,1421,4359,32,396,20,33,1575,9,3669,5,22,7,6,16189,4051,17,23,16223,4,16270,12,3361,2,26,14,16331,350,166,141,3,140,58,167,159,54,62,61,60,154,150,151,148,149,155,153,152,144,146,156,161,157,172,171,173,186,178,185,180,188,184,187,189,179,196,195,194,362,16235,16373,16391,16134,16234,16392,163])). % 63.79/63.84 cnf(17508,plain, % 63.79/63.84 (E(f5(a9,x175081),f5(a23,x175081))), % 63.79/63.84 inference(rename_variables,[],[17380])). % 63.79/63.84 cnf(17510,plain, % 63.79/63.84 (E(f5(a9,x175101),f5(a23,x175101))), % 63.79/63.84 inference(rename_variables,[],[17380])). % 63.79/63.84 cnf(17512,plain, % 63.79/63.84 (E(f5(a9,x175121),f5(a23,x175121))), % 63.79/63.84 inference(rename_variables,[],[17380])). % 63.79/63.84 cnf(17514,plain, % 63.79/63.84 (E(f5(a9,x175141),f5(a23,x175141))), % 63.79/63.84 inference(rename_variables,[],[17380])). % 63.79/63.84 cnf(17519,plain, % 63.79/63.84 (P10(f31(a21),f30(f28(a21),f28(a21)),f28(a21))), % 63.79/63.84 inference(scs_inference,[],[17380,17508,17510,17512,17514,17190,17167,16184,16327,16183,16326,388,139,182])). % 63.79/63.84 cnf(17527,plain, % 63.79/63.84 (E(f27(a2),f27(a23))), % 63.79/63.84 inference(scs_inference,[],[17323,17380,17508,17510,17512,17514,17190,17408,17167,17343,107,16184,16327,16183,16326,388,139,182,181,334,137,8])). % 63.79/63.84 cnf(17528,plain, % 63.79/63.84 (P3(f31(a21))), % 63.79/63.84 inference(scs_inference,[],[17323,17380,17508,17510,17512,17514,17190,17408,17167,17343,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138])). % 63.79/63.84 cnf(17536,plain, % 63.79/63.84 (E(f25(a2,x175361,x175362),f25(a23,x175361,x175362))), % 63.79/63.84 inference(scs_inference,[],[17323,17380,17508,17510,17512,17514,17190,17408,17167,17343,17390,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18])). % 63.79/63.85 cnf(17537,plain, % 63.79/63.85 (P9(f3(f27(a2)),f27(a23))), % 63.79/63.85 inference(scs_inference,[],[17323,17380,17508,17510,17512,17514,17190,17408,17167,17343,17390,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192])). % 63.79/63.85 cnf(17540,plain, % 63.79/63.85 (E(f5(x175401,a9),f5(x175401,a23))), % 63.79/63.85 inference(rename_variables,[],[17366])). % 63.79/63.85 cnf(17542,plain, % 63.79/63.85 (E(f4(x175421,a9),f4(x175421,a23))), % 63.79/63.85 inference(rename_variables,[],[17372])). % 63.79/63.85 cnf(17543,plain, % 63.79/63.85 (E(f25(x175431,a2,x175432),f25(x175431,a23,x175432))), % 63.79/63.85 inference(scs_inference,[],[17323,17366,17372,17380,17508,17510,17512,17514,17190,17408,17167,17343,17390,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19])). % 63.79/63.85 cnf(17547,plain, % 63.79/63.85 (E(f6(x175471,a2),f6(x175471,a23))), % 63.79/63.85 inference(scs_inference,[],[17323,17366,17372,17380,17508,17510,17512,17514,17190,17408,17167,17343,17390,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25])). % 63.79/63.85 cnf(17549,plain, % 63.79/63.85 (E(f5(x175491,a9),f5(x175491,a23))), % 63.79/63.85 inference(rename_variables,[],[17366])). % 63.79/63.85 cnf(17551,plain, % 63.79/63.85 (E(f11(x175511,a9),f11(x175511,a23))), % 63.79/63.85 inference(rename_variables,[],[17393])). % 63.79/63.85 cnf(17552,plain, % 63.79/63.85 (E(f29(a2,x175521,x175522),f29(a23,x175521,x175522))), % 63.79/63.85 inference(scs_inference,[],[17323,17366,17540,17372,17380,17508,17510,17512,17514,17393,17190,17408,17167,17343,17390,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15])). % 63.79/63.85 cnf(17556,plain, % 63.79/63.85 (E(f5(a2,x175561),f5(a23,x175561))), % 63.79/63.85 inference(scs_inference,[],[17323,17366,17540,17372,17380,17508,17510,17512,17514,17393,17190,17408,17167,17343,17390,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9])). % 63.79/63.85 cnf(17558,plain, % 63.79/63.85 (E(f29(x175581,a2,x175582),f29(x175581,a23,x175582))), % 63.79/63.85 inference(scs_inference,[],[17323,17366,17540,17372,17380,17508,17510,17512,17514,17393,17190,17408,17167,17343,17390,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16])). % 63.79/63.85 cnf(17565,plain, % 63.79/63.85 (E(f5(x175651,a9),f5(x175651,a23))), % 63.79/63.85 inference(rename_variables,[],[17366])). % 63.79/63.85 cnf(17571,plain, % 63.79/63.85 (P12(f6(f14(x175711),f5(x175712,a23)),f14(x175713),f5(x175712,a9))), % 63.79/63.85 inference(scs_inference,[],[17323,17366,17540,17549,17372,17380,17508,17510,17512,17514,17393,17190,17408,17167,17343,17390,17353,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222])). % 63.79/63.85 cnf(17572,plain, % 63.79/63.85 (E(f6(x175721,f5(x175722,a9)),f6(x175721,f5(x175722,a23)))), % 63.79/63.85 inference(rename_variables,[],[17353])). % 63.79/63.85 cnf(17574,plain, % 63.79/63.85 (E(f11(x175741,a2),f11(x175741,a23))), % 63.79/63.85 inference(scs_inference,[],[17323,17366,17540,17549,17372,17380,17508,17510,17512,17514,17393,17190,17408,17167,17343,17390,17353,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12])). % 63.79/63.85 cnf(17576,plain, % 63.79/63.85 (E(f5(x175761,a2),f5(x175761,a23))), % 63.79/63.85 inference(scs_inference,[],[17323,17366,17540,17549,17372,17380,17508,17510,17512,17514,17393,17190,17408,17167,17343,17390,17353,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10])). % 63.79/63.85 cnf(17581,plain, % 63.79/63.85 (E(f4(a2,x175811),f4(a23,x175811))), % 63.79/63.85 inference(scs_inference,[],[17323,17366,17540,17549,17372,17380,17508,17510,17512,17514,17393,17190,17408,17167,17343,17390,17353,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10,3669,20,23,6,26])). % 63.79/63.85 cnf(17586,plain, % 63.79/63.85 (E(f4(x175861,a2),f4(x175861,a23))), % 63.79/63.85 inference(scs_inference,[],[17323,17366,17540,17549,17372,17380,17508,17510,17512,17514,17393,17190,17408,17167,17343,17390,17353,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10,3669,20,23,6,26,34,4,4051,13,27])). % 63.79/63.85 cnf(17589,plain, % 63.79/63.85 (~E(f28(a13),a23)), % 63.79/63.85 inference(scs_inference,[],[17323,17366,17540,17549,17372,17380,17508,17510,17512,17514,17393,17190,17408,17407,17167,17343,17390,17353,106,107,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10,3669,20,23,6,26,34,4,4051,13,27,365,14,2])). % 63.79/63.85 cnf(17610,plain, % 63.79/63.85 (~E(f14(x176101),f28(a13))), % 63.79/63.85 inference(scs_inference,[],[17323,17366,17540,17549,17565,17372,17542,17380,17508,17510,17512,17514,17393,17551,17183,17190,17408,17442,17407,17167,17343,17390,17353,17572,106,107,15864,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10,3669,20,23,6,26,34,4,4051,13,27,365,14,2,396,4359,24,33,17,16223,16189,16331,16270,7,3361,350,166,141,3])). % 63.79/63.85 cnf(17613,plain, % 63.79/63.85 (~E(a9,f16(a13))), % 63.79/63.85 inference(scs_inference,[],[17323,17366,17540,17549,17565,17372,17542,17380,17508,17510,17512,17514,17393,17551,17183,17190,17408,17442,17407,17167,17343,17390,17353,17572,106,107,103,15864,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10,3669,20,23,6,26,34,4,4051,13,27,365,14,2,396,4359,24,33,17,16223,16189,16331,16270,7,3361,350,166,141,3,140,58])). % 63.79/63.85 cnf(17615,plain, % 63.79/63.85 (P9(x176151,f27(x176151))), % 63.79/63.85 inference(rename_variables,[],[17327])). % 63.79/63.85 cnf(17619,plain, % 63.79/63.85 (~P9(f27(f28(a13)),f27(a9))), % 63.79/63.85 inference(scs_inference,[],[17323,17327,17366,17540,17549,17565,17372,17542,17380,17508,17510,17512,17514,17393,17551,17183,17190,17408,17442,17407,17167,17343,17410,17390,17353,17572,15957,106,107,103,15864,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10,3669,20,23,6,26,34,4,4051,13,27,365,14,2,396,4359,24,33,17,16223,16189,16331,16270,7,3361,350,166,141,3,140,58,168,59,167])). % 63.79/63.85 cnf(17621,plain, % 63.79/63.85 (~P9(f27(f28(a13)),f16(a13))), % 63.79/63.85 inference(scs_inference,[],[17323,17327,17366,17540,17549,17565,17372,17542,17380,17508,17510,17512,17514,17393,17551,17183,17190,17408,17442,17407,17167,17343,17486,17410,17390,17353,17572,15957,106,107,103,15864,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10,3669,20,23,6,26,34,4,4051,13,27,365,14,2,396,4359,24,33,17,16223,16189,16331,16270,7,3361,350,166,141,3,140,58,168,59,167,159])). % 63.79/63.85 cnf(17623,plain, % 63.79/63.85 (~P9(f28(a12),f27(a9))), % 63.79/63.85 inference(scs_inference,[],[17323,17327,17366,17540,17549,17565,17372,17542,17380,17508,17510,17512,17514,17393,17551,17183,17190,17334,17408,17442,17407,17167,17343,17486,17410,17390,17353,17572,15957,106,107,103,15864,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10,3669,20,23,6,26,34,4,4051,13,27,365,14,2,396,4359,24,33,17,16223,16189,16331,16270,7,3361,350,166,141,3,140,58,168,59,167,159,62])). % 63.79/63.85 cnf(17624,plain, % 63.79/63.85 (P9(f29(x176241,a23,x176242),f27(f29(x176241,a9,x176242)))), % 63.79/63.85 inference(scs_inference,[],[17323,17327,17615,17339,17366,17540,17549,17565,17372,17542,17380,17508,17510,17512,17514,17393,17551,17183,17190,17334,17408,17442,17407,17167,17343,17486,17410,17390,17353,17572,15957,106,107,103,15864,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10,3669,20,23,6,26,34,4,4051,13,27,365,14,2,396,4359,24,33,17,16223,16189,16331,16270,7,3361,350,166,141,3,140,58,168,59,167,159,62,61])). % 63.79/63.85 cnf(17653,plain, % 63.79/63.85 (P12(f6(a23,f14(x176531)),a2,a23)), % 63.79/63.85 inference(scs_inference,[],[17323,17327,17615,17339,17366,17540,17549,17565,17372,17542,17380,17508,17510,17512,17514,17393,17551,17183,17190,17334,17408,17426,17436,17442,17407,17167,17343,17486,17410,17390,17353,17572,15957,308,106,107,103,122,112,119,15864,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10,3669,20,23,6,26,34,4,4051,13,27,365,14,2,396,4359,24,33,17,16223,16189,16331,16270,7,3361,350,166,141,3,140,58,168,59,167,159,62,61,60,190,173,171,172,186,187,189,185,184,188,16234,362,16235])). % 63.79/63.85 cnf(17667,plain, % 63.79/63.85 (P3(f29(a1,a12,a18))), % 63.79/63.85 inference(scs_inference,[],[17323,17327,17615,17339,17479,17366,17540,17549,17565,17372,17542,17380,17508,17510,17512,17514,17393,17551,17183,17190,17334,17408,17426,17436,17442,17407,17167,17161,17343,17321,17486,17410,17390,17353,17572,17135,15957,308,106,107,103,17212,17232,17208,235,122,112,119,15864,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10,3669,20,23,6,26,34,4,4051,13,27,365,14,2,396,4359,24,33,17,16223,16189,16331,16270,7,3361,350,166,141,3,140,58,168,59,167,159,62,61,60,190,173,171,172,186,187,189,185,184,188,16234,362,16235,16391,16392,16373,16134,8587,72,202,203,178,180])). % 63.79/63.85 cnf(17669,plain, % 63.79/63.85 (P7(f25(f28(a22),f32(a22),f32(a22)))), % 63.79/63.85 inference(scs_inference,[],[17323,17327,17615,17339,17479,17366,17540,17549,17565,17372,17542,17380,17508,17510,17512,17514,17393,17551,17183,17190,17334,17408,17426,17436,17442,17407,17167,17161,17343,17321,17486,17410,17390,17353,17572,17135,15957,308,106,107,103,17212,17232,17208,235,122,112,119,15864,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10,3669,20,23,6,26,34,4,4051,13,27,365,14,2,396,4359,24,33,17,16223,16189,16331,16270,7,3361,350,166,141,3,140,58,168,59,167,159,62,61,60,190,173,171,172,186,187,189,185,184,188,16234,362,16235,16391,16392,16373,16134,8587,72,202,203,178,180,135])). % 63.79/63.85 cnf(17671,plain, % 63.79/63.85 (P6(f25(f28(a22),f32(a22),f32(a22)))), % 63.79/63.85 inference(scs_inference,[],[17323,17327,17615,17339,17479,17366,17540,17549,17565,17372,17542,17380,17508,17510,17512,17514,17393,17551,17183,17190,17334,17408,17426,17436,17442,17407,17167,17161,17343,17321,17486,17410,17390,17353,17572,17135,15957,308,106,107,103,17212,17232,17208,235,122,112,119,15864,16184,16327,16183,16326,388,139,182,181,334,137,8,138,2745,183,29,143,18,1192,16088,16385,19,2591,32,318,25,16121,16212,15,3207,22,3515,9,1421,16,30,3053,21,1883,28,16188,2899,31,11,4205,1575,16222,1729,12,5,10,3669,20,23,6,26,34,4,4051,13,27,365,14,2,396,4359,24,33,17,16223,16189,16331,16270,7,3361,350,166,141,3,140,58,168,59,167,159,62,61,60,190,173,171,172,186,187,189,185,184,188,16234,362,16235,16391,16392,16373,16134,8587,72,202,203,178,180,135,134])). % 63.79/63.85 cnf(17680,plain, % 63.79/63.85 (E(f5(a2,x176801),f5(a23,x176801))), % 63.79/63.85 inference(rename_variables,[],[17556])). % 63.79/63.85 cnf(17682,plain, % 63.79/63.85 (E(f5(a2,x176821),f5(a23,x176821))), % 63.79/63.85 inference(rename_variables,[],[17556])). % 63.79/63.85 cnf(17686,plain, % 63.79/63.85 (E(f5(a2,x176861),f5(a23,x176861))), % 63.79/63.85 inference(rename_variables,[],[17556])). % 63.79/63.85 cnf(17694,plain, % 63.79/63.85 (E(f5(a2,x176941),f5(a23,x176941))), % 63.79/63.85 inference(rename_variables,[],[17556])). % 63.79/63.85 cnf(17699,plain, % 63.79/63.85 (E(f27(f25(a2,x176991,x176992)),f27(f25(a23,x176991,x176992)))), % 63.79/63.85 inference(scs_inference,[],[17536,17556,17680,17682,17686,17694,17623,17371,17571,17671,17669,17325,139,16327,388,334,16184,138,181,137,16326,182,16183,8])). % 63.79/63.85 cnf(17710,plain, % 63.79/63.85 (E(f5(x177101,a2),f5(x177101,a23))), % 63.79/63.85 inference(rename_variables,[],[17576])). % 63.79/63.85 cnf(17712,plain, % 63.79/63.85 (E(f11(f25(a2,x177121,x177122),x177123),f11(f25(a23,x177121,x177122),x177123))), % 63.79/63.85 inference(scs_inference,[],[17536,17556,17680,17682,17686,17694,17576,17623,17371,17571,17671,17669,17325,17480,17404,866,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11])). % 63.79/63.85 cnf(17714,plain, % 63.79/63.85 (E(f11(x177141,a2),f11(x177141,a23))), % 63.79/63.85 inference(rename_variables,[],[17574])). % 63.79/63.85 cnf(17717,plain, % 63.79/63.85 (E(f5(x177171,a2),f5(x177171,a23))), % 63.79/63.85 inference(rename_variables,[],[17576])). % 63.79/63.85 cnf(17721,plain, % 63.79/63.85 (E(f6(x177211,f25(a2,x177212,x177213)),f6(x177211,f25(a23,x177212,x177213)))), % 63.79/63.85 inference(scs_inference,[],[17536,17556,17680,17682,17686,17694,17574,17576,17710,17623,17371,17571,17671,17669,17325,17480,17404,866,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11,16212,19,16121,23,28,29,25])). % 63.79/63.85 cnf(17722,plain, % 63.79/63.85 (E(f4(x177221,f25(a2,x177222,x177223)),f4(x177221,f25(a23,x177222,x177223)))), % 63.79/63.85 inference(scs_inference,[],[17536,17556,17680,17682,17686,17694,17574,17576,17710,17623,17371,17571,17671,17669,17325,17480,17404,866,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11,16212,19,16121,23,28,29,25,27])). % 63.79/63.85 cnf(17724,plain, % 63.79/63.85 (E(f4(x177241,a2),f4(x177241,a23))), % 63.79/63.85 inference(rename_variables,[],[17586])). % 63.79/63.85 cnf(17732,plain, % 63.79/63.85 (E(f5(x177321,a2),f5(x177321,a23))), % 63.79/63.85 inference(rename_variables,[],[17576])). % 63.79/63.85 cnf(17735,plain, % 63.79/63.85 (E(f5(x177351,f25(a2,x177352,x177353)),f5(x177351,f25(a23,x177352,x177353)))), % 63.79/63.85 inference(scs_inference,[],[17536,17556,17680,17682,17686,17694,17574,17576,17710,17717,17586,17623,17371,17571,17671,17669,17325,17480,17404,866,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11,16212,19,16121,23,28,29,25,27,16385,31,5,13,15,16,30,16088,396,17,10])). % 63.79/63.85 cnf(17737,plain, % 63.79/63.85 (E(f11(x177371,f25(a2,x177372,x177373)),f11(x177371,f25(a23,x177372,x177373)))), % 63.79/63.85 inference(scs_inference,[],[17536,17556,17680,17682,17686,17694,17574,17576,17710,17717,17586,17623,17371,17571,17671,17669,17325,17480,17404,866,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11,16212,19,16121,23,28,29,25,27,16385,31,5,13,15,16,30,16088,396,17,10,6,12])). % 63.79/63.85 cnf(17739,plain, % 63.79/63.85 (E(f5(f25(a2,x177391,x177392),x177393),f5(f25(a23,x177391,x177392),x177393))), % 63.79/63.85 inference(scs_inference,[],[17536,17556,17680,17682,17686,17694,17574,17576,17710,17717,17586,17623,17371,17571,17671,17669,17325,17480,17404,866,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11,16212,19,16121,23,28,29,25,27,16385,31,5,13,15,16,30,16088,396,17,10,6,12,20,9])). % 63.79/63.85 cnf(17747,plain, % 63.79/63.85 (E(f6(x177471,a2),f6(x177471,a23))), % 63.79/63.85 inference(rename_variables,[],[17547])). % 63.79/63.85 cnf(17748,plain, % 63.79/63.85 (E(f4(f25(a2,x177481,x177482),x177483),f4(f25(a23,x177481,x177482),x177483))), % 63.79/63.85 inference(scs_inference,[],[17536,17547,17556,17680,17682,17686,17694,17574,17576,17710,17717,17732,17586,17724,17623,17371,17571,17671,17669,17325,17480,17404,866,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11,16212,19,16121,23,28,29,25,27,16385,31,5,13,15,16,30,16088,396,17,10,6,12,20,9,21,16189,34,16331,16222,26])). % 63.79/63.85 cnf(17750,plain, % 63.79/63.85 (E(f6(f25(a2,x177501,x177502),x177503),f6(f25(a23,x177501,x177502),x177503))), % 63.79/63.85 inference(scs_inference,[],[17536,17547,17556,17680,17682,17686,17694,17574,17576,17710,17717,17732,17586,17724,17623,17371,17571,17671,17669,17325,17480,17404,866,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11,16212,19,16121,23,28,29,25,27,16385,31,5,13,15,16,30,16088,396,17,10,6,12,20,9,21,16189,34,16331,16222,26,7,24])). % 63.79/63.85 cnf(17758,plain, % 63.79/63.85 (P12(f6(f14(x177581),a23),a23,a2)), % 63.79/63.85 inference(scs_inference,[],[17536,17547,17747,17556,17680,17682,17686,17694,17574,17714,17576,17710,17717,17732,17586,17724,17610,17623,17371,17571,17671,17669,17325,17480,17404,866,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11,16212,19,16121,23,28,29,25,27,16385,31,5,13,15,16,30,16088,396,17,10,6,12,20,9,21,16189,34,16331,16222,26,7,24,4,14,2,33,365,16270,16223])). % 63.79/63.85 cnf(17763,plain, % 63.79/63.85 (E(f25(a2,a2,x177631),f25(a23,a23,x177631))), % 63.79/63.85 inference(scs_inference,[],[17536,17543,17547,17747,17556,17680,17682,17686,17694,17574,17714,17576,17710,17717,17732,17586,17724,17610,17623,17371,17571,17619,17671,17669,17325,17480,17404,866,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11,16212,19,16121,23,28,29,25,27,16385,31,5,13,15,16,30,16088,396,17,10,6,12,20,9,21,16189,34,16331,16222,26,7,24,4,14,2,33,365,16270,16223,350,166,3])). % 63.79/63.85 cnf(17764,plain, % 63.79/63.85 (E(f25(a2,x177641,x177642),f25(a23,x177641,x177642))), % 63.79/63.85 inference(rename_variables,[],[17536])). % 63.79/63.85 cnf(17769,plain, % 63.79/63.85 (P15(f3(f27(a2)),f27(a23))), % 63.79/63.85 inference(scs_inference,[],[17536,17543,17547,17747,17556,17680,17682,17686,17694,17574,17714,17576,17710,17717,17732,17586,17724,17610,17623,17371,17571,17537,17619,17671,17669,17325,17480,17404,866,12530,128,108,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11,16212,19,16121,23,28,29,25,27,16385,31,5,13,15,16,30,16088,396,17,10,6,12,20,9,21,16189,34,16331,16222,26,7,24,4,14,2,33,365,16270,16223,350,166,3,58,167,159])). % 63.79/63.85 cnf(17788,plain, % 63.79/63.85 (P7(f25(f28(a21),f31(a21),f31(a21)))), % 63.79/63.85 inference(scs_inference,[],[17536,17764,17543,17547,17747,17556,17680,17682,17686,17694,17574,17714,17576,17710,17717,17732,17581,17586,17724,17610,17528,17623,17163,17371,17571,17519,17537,17619,17446,17448,17450,17671,17669,17325,17480,17417,17404,17327,866,12530,128,17426,17436,108,17442,17212,110,17232,17208,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11,16212,19,16121,23,28,29,25,27,16385,31,5,13,15,16,30,16088,396,17,10,6,12,20,9,21,16189,34,16331,16222,26,7,24,4,14,2,33,365,16270,16223,350,166,3,58,167,159,62,61,60,203,202,178,179,180,135])). % 63.79/63.85 cnf(17792,plain, % 63.79/63.85 (P12(f6(f25(a23,a2,x177921),f14(x177922)),f25(a2,a2,x177921),f14(x177923))), % 63.79/63.85 inference(scs_inference,[],[17536,17764,17543,17547,17747,17556,17680,17682,17686,17694,17574,17714,17576,17710,17717,17732,17581,17586,17724,17610,17528,17623,17163,17371,17571,17519,17537,17619,17446,17448,17450,17671,17669,17325,17480,17417,17404,17327,866,12530,128,17426,17436,108,17442,17212,110,17232,17208,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11,16212,19,16121,23,28,29,25,27,16385,31,5,13,15,16,30,16088,396,17,10,6,12,20,9,21,16189,34,16331,16222,26,7,24,4,14,2,33,365,16270,16223,350,166,3,58,167,159,62,61,60,203,202,178,179,180,135,362,16235,16234])). % 63.79/63.85 cnf(17793,plain, % 63.79/63.85 (P6(f25(f28(a21),f31(a21),f31(a21)))), % 63.79/63.85 inference(scs_inference,[],[17536,17764,17543,17547,17747,17556,17680,17682,17686,17694,17574,17714,17576,17710,17717,17732,17581,17586,17724,17610,17528,17623,17163,17371,17571,17519,17537,17619,17446,17448,17450,17671,17669,17325,17480,17417,17404,17327,866,12530,128,17426,17436,108,17442,17212,110,17232,17208,139,16327,388,334,16184,138,181,137,16326,182,16183,8,183,143,1192,18,318,22,16188,32,11,16212,19,16121,23,28,29,25,27,16385,31,5,13,15,16,30,16088,396,17,10,6,12,20,9,21,16189,34,16331,16222,26,7,24,4,14,2,33,365,16270,16223,350,166,3,58,167,159,62,61,60,203,202,178,179,180,135,362,16235,16234,134])). % 63.79/63.85 cnf(17810,plain, % 63.79/63.85 (E(f5(f25(a2,x178101,x178102),x178103),f5(f25(a23,x178101,x178102),x178103))), % 63.79/63.85 inference(rename_variables,[],[17739])). % 63.79/63.85 cnf(17814,plain, % 63.79/63.85 (E(f5(f25(a2,x178141,x178142),x178143),f5(f25(a23,x178141,x178142),x178143))), % 63.79/63.85 inference(rename_variables,[],[17739])). % 63.79/63.85 cnf(17818,plain, % 63.79/63.85 (E(f5(f25(a2,x178181,x178182),x178183),f5(f25(a23,x178181,x178182),x178183))), % 63.79/63.85 inference(rename_variables,[],[17739])). % 63.79/63.85 cnf(17826,plain, % 63.79/63.85 (P10(f5(f25(a23,x178261,x178262),f14(x178263)),f25(a2,x178261,x178262),f14(x178264))), % 63.79/63.85 inference(scs_inference,[],[17763,17398,17792,17793,17788,17400,17653,17739,17810,17814,17818,10797,139,138,16327,182,16183,137,16184,8,181,143,183,16326])). % 63.79/63.85 cnf(17827,plain, % 63.79/63.85 (E(f5(f25(a2,x178271,x178272),x178273),f5(f25(a23,x178271,x178272),x178273))), % 63.79/63.85 inference(rename_variables,[],[17739])). % 63.79/63.85 cnf(17829,plain, % 63.79/63.85 (E(f5(f25(a2,x178291,x178292),x178293),f5(f25(a23,x178291,x178292),x178293))), % 63.79/63.85 inference(rename_variables,[],[17739])). % 63.79/63.85 cnf(17831,plain, % 63.79/63.85 (E(f6(f25(a2,x178311,x178312),x178313),f6(f25(a23,x178311,x178312),x178313))), % 63.79/63.85 inference(rename_variables,[],[17750])). % 63.79/63.85 cnf(17832,plain, % 63.79/63.85 (P12(f6(f25(a23,x178321,x178322),f14(x178323)),f25(a2,x178321,x178322),f14(x178324))), % 63.79/63.85 inference(scs_inference,[],[17763,17398,17792,17793,17788,17400,17653,17739,17810,17814,17818,17827,17750,17831,10797,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234])). % 63.79/63.85 cnf(17837,plain, % 63.79/63.85 (E(f4(f25(a2,x178371,x178372),x178373),f4(f25(a23,x178371,x178372),x178373))), % 63.79/63.85 inference(rename_variables,[],[17748])). % 63.79/63.85 cnf(17839,plain, % 63.79/63.85 (E(f11(f25(a2,x178391,x178392),x178393),f11(f25(a23,x178391,x178392),x178393))), % 63.79/63.85 inference(rename_variables,[],[17712])). % 63.79/63.85 cnf(17843,plain, % 63.79/63.85 (E(f25(f25(a2,a2,x178431),x178432,x178433),f25(f25(a23,a23,x178431),x178432,x178433))), % 63.79/63.85 inference(scs_inference,[],[17763,17398,17792,17793,17788,17400,17653,17712,17839,17739,17810,17814,17818,17827,17829,17748,17750,17831,10797,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18])). % 63.79/63.85 cnf(17847,plain, % 63.79/63.85 (E(f5(x178471,f25(a2,x178472,x178473)),f5(x178471,f25(a23,x178472,x178473)))), % 63.79/63.85 inference(rename_variables,[],[17735])). % 63.79/63.85 cnf(17849,plain, % 63.79/63.85 (E(f4(x178491,f25(a2,x178492,x178493)),f4(x178491,f25(a23,x178492,x178493)))), % 63.79/63.85 inference(rename_variables,[],[17722])). % 63.79/63.85 cnf(17851,plain, % 63.79/63.85 (E(f25(x178511,f25(a2,a2,x178512),x178513),f25(x178511,f25(a23,a23,x178512),x178513))), % 63.79/63.85 inference(scs_inference,[],[17763,17398,17792,17793,17788,17400,17653,17712,17839,17722,17735,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,10797,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19])). % 63.79/63.85 cnf(17852,plain, % 63.79/63.85 (E(f11(f25(a2,a2,x178521),x178522),f11(f25(a23,a23,x178521),x178522))), % 63.79/63.85 inference(scs_inference,[],[17763,17398,17792,17793,17788,17400,17653,17712,17839,17722,17735,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,10797,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19,11])). % 63.79/63.85 cnf(17855,plain, % 63.79/63.85 (E(f5(x178551,f25(a2,a2,x178552)),f5(x178551,f25(a23,a23,x178552)))), % 63.79/63.85 inference(scs_inference,[],[17763,17398,17792,17793,17788,17400,17653,17712,17839,17722,17735,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,10797,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19,11,28,29,10])). % 63.79/63.85 cnf(17857,plain, % 63.79/63.85 (E(f11(x178571,f25(a2,x178572,x178573)),f11(x178571,f25(a23,x178572,x178573)))), % 63.79/63.85 inference(rename_variables,[],[17737])). % 63.79/63.85 cnf(17861,plain, % 63.79/63.85 (E(f4(x178611,f25(a2,a2,x178612)),f4(x178611,f25(a23,a23,x178612)))), % 63.79/63.85 inference(scs_inference,[],[17763,17398,17792,17793,17788,17400,17653,17712,17839,17722,17735,17737,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,10797,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19,11,28,29,10,16212,23,32,20,27])). % 63.79/63.85 cnf(17865,plain, % 63.79/63.85 (E(f5(x178651,f25(a2,x178652,x178653)),f5(x178651,f25(a23,x178652,x178653)))), % 63.79/63.85 inference(rename_variables,[],[17735])). % 63.79/63.85 cnf(17866,plain, % 63.79/63.85 (E(f11(x178661,f25(a2,a2,x178662)),f11(x178661,f25(a23,a23,x178662)))), % 63.79/63.85 inference(scs_inference,[],[17763,17398,17792,17793,17788,17400,17653,17712,17839,17722,17735,17847,17737,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,10797,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19,11,28,29,10,16212,23,32,20,27,13,17,16188,12])). % 63.79/63.85 cnf(17867,plain, % 63.79/63.85 (E(f6(x178671,f25(a2,a2,x178672)),f6(x178671,f25(a23,a23,x178672)))), % 63.79/63.85 inference(scs_inference,[],[17763,17398,17792,17793,17788,17400,17653,17712,17839,17722,17735,17847,17737,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,10797,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19,11,28,29,10,16212,23,32,20,27,13,17,16188,12,25])). % 63.79/63.85 cnf(17871,plain, % 63.79/63.85 (E(f6(x178711,f25(a2,x178712,x178713)),f6(x178711,f25(a23,x178712,x178713)))), % 63.79/63.85 inference(rename_variables,[],[17721])). % 63.79/63.85 cnf(17873,plain, % 63.79/63.85 (E(f5(f25(a2,a2,x178731),x178732),f5(f25(a23,a23,x178731),x178732))), % 63.79/63.85 inference(scs_inference,[],[17763,17398,17792,17793,17788,17400,17653,17712,17839,17721,17722,17735,17847,17737,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,10797,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19,11,28,29,10,16212,23,32,20,27,13,17,16188,12,25,4,15,16222,7,9])). % 63.79/63.85 cnf(17881,plain, % 63.79/63.85 (E(f5(x178811,f25(a2,x178812,x178813)),f5(x178811,f25(a23,x178812,x178813)))), % 63.79/63.85 inference(rename_variables,[],[17735])). % 63.79/63.85 cnf(17884,plain, % 63.79/63.85 (E(f4(f25(a2,a2,x178841),x178842),f4(f25(a23,a23,x178841),x178842))), % 63.79/63.85 inference(scs_inference,[],[17763,17398,17792,17621,17793,17788,17400,17653,17712,17839,17721,17722,17849,17735,17847,17865,17737,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,10797,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19,11,28,29,10,16212,23,32,20,27,13,17,16188,12,25,4,15,16222,7,9,396,21,16,30,31,5,16088,16331,26])). % 63.79/63.85 cnf(17891,plain, % 63.79/63.85 (E(f6(f25(a2,a2,x178911),x178912),f6(f25(a23,a23,x178911),x178912))), % 63.79/63.85 inference(scs_inference,[],[17763,17398,17792,17621,17793,17788,17400,17653,17712,17839,17721,17722,17849,17735,17847,17865,17881,17737,17857,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,10797,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19,11,28,29,10,16212,23,32,20,27,13,17,16188,12,25,4,15,16222,7,9,396,21,16,30,31,5,16088,16331,26,6,34,16270,16189,24])). % 63.79/63.85 cnf(17900,plain, % 63.79/63.85 (~E(f28(a13),a2)), % 63.79/63.85 inference(scs_inference,[],[17763,17589,17613,17398,17792,17621,17793,17788,17400,17653,17712,17839,17721,17871,17722,17849,17735,17847,17865,17881,17737,17857,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,12555,10797,17323,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19,11,28,29,10,16212,23,32,20,27,13,17,16188,12,25,4,15,16222,7,9,396,21,16,30,31,5,16088,16331,26,6,34,16270,16189,24,16223,14,33,2,365,166,3])). % 63.79/63.85 cnf(17902,plain, % 63.79/63.85 (~P9(f27(a23),f27(a2))), % 63.79/63.85 inference(scs_inference,[],[17763,17589,17613,17398,17792,17621,17769,17793,17788,17400,17653,17712,17839,17721,17871,17722,17849,17735,17847,17865,17881,17737,17857,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,12555,10797,102,17323,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19,11,28,29,10,16212,23,32,20,27,13,17,16188,12,25,4,15,16222,7,9,396,21,16,30,31,5,16088,16331,26,6,34,16270,16189,24,16223,14,33,2,365,166,3,58,167])). % 63.79/63.85 cnf(17907,plain, % 63.79/63.85 (P9(x179071,f27(x179071))), % 63.79/63.85 inference(rename_variables,[],[17327])). % 63.79/63.85 cnf(17908,plain, % 63.79/63.85 (P9(f25(a23,a23,x179081),f27(f25(a2,a2,x179081)))), % 63.79/63.85 inference(scs_inference,[],[17763,17589,17613,17398,17792,17201,17621,17769,17793,17788,17400,17653,17712,17839,17721,17871,17722,17849,17735,17847,17865,17881,17737,17857,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,17327,17907,11383,12555,10797,102,17323,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19,11,28,29,10,16212,23,32,20,27,13,17,16188,12,25,4,15,16222,7,9,396,21,16,30,31,5,16088,16331,26,6,34,16270,16189,24,16223,14,33,2,365,166,3,58,167,159,62,61])). % 63.79/63.85 cnf(17911,plain, % 63.79/63.85 (P23(f29(a1,a12,a18),f28(f24(a1)),f28(f24(a12)))), % 63.79/63.85 inference(scs_inference,[],[17763,17589,17613,17398,17792,17201,17621,17769,17793,17788,17400,17653,17712,17839,17721,17871,17722,17849,17735,17847,17865,17881,17737,17857,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,17121,17327,17907,11383,12555,10797,102,17426,17436,17442,17212,17232,17208,235,17323,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19,11,28,29,10,16212,23,32,20,27,13,17,16188,12,25,4,15,16222,7,9,396,21,16,30,31,5,16088,16331,26,6,34,16270,16189,24,16223,14,33,2,365,166,3,58,167,159,62,61,60,186])). % 63.79/63.85 cnf(17913,plain, % 63.79/63.85 (P12(f29(a1,a12,a18),f28(f24(a1)),f28(f24(a12)))), % 63.79/63.85 inference(scs_inference,[],[17763,17589,17613,17398,17792,17201,17621,17769,17793,17788,17400,17653,17712,17839,17721,17871,17722,17849,17735,17847,17865,17881,17737,17857,17739,17810,17814,17818,17827,17829,17748,17837,17750,17831,17121,17327,17907,11383,12555,10797,102,17426,17436,17442,17212,17232,17208,237,235,17323,139,138,16327,182,16183,137,16184,8,181,143,183,16326,388,16235,16234,362,16373,16391,16392,318,18,16134,16121,16385,22,19,11,28,29,10,16212,23,32,20,27,13,17,16188,12,25,4,15,16222,7,9,396,21,16,30,31,5,16088,16331,26,6,34,16270,16189,24,16223,14,33,2,365,166,3,58,167,159,62,61,60,186,188])). % 63.79/63.85 cnf(17932,plain, % 63.79/63.85 (E(f5(f25(a2,a2,x179321),x179322),f5(f25(a23,a23,x179321),x179322))), % 63.79/63.85 inference(rename_variables,[],[17873])). % 63.79/63.85 cnf(17938,plain, % 63.79/63.85 (E(f5(f25(a2,a2,x179381),x179382),f5(f25(a23,a23,x179381),x179382))), % 63.79/63.85 inference(rename_variables,[],[17873])). % 63.79/63.85 cnf(17943,plain, % 63.79/63.85 (E(f5(f25(a2,a2,x179431),x179432),f5(f25(a23,a23,x179431),x179432))), % 63.79/63.85 inference(rename_variables,[],[17873])). % 63.79/63.85 cnf(17945,plain, % 63.79/63.85 (E(f5(f25(a2,a2,x179451),x179452),f5(f25(a23,a23,x179451),x179452))), % 63.79/63.85 inference(rename_variables,[],[17873])). % 63.79/63.85 cnf(17947,plain, % 63.79/63.85 (E(f5(f25(a2,a2,x179471),x179472),f5(f25(a23,a23,x179471),x179472))), % 63.79/63.85 inference(rename_variables,[],[17873])). % 63.79/63.85 cnf(17949,plain, % 63.79/63.85 (E(f6(f25(a2,a2,x179491),x179492),f6(f25(a23,a23,x179491),x179492))), % 63.79/63.85 inference(rename_variables,[],[17891])). % 63.79/63.85 cnf(17956,plain, % 63.79/63.85 (E(f11(f25(a2,a2,x179561),x179562),f11(f25(a23,a23,x179561),x179562))), % 63.79/63.85 inference(rename_variables,[],[17852])). % 63.79/63.85 cnf(17958,plain, % 63.79/63.85 (E(f4(f25(a2,a2,x179581),x179582),f4(f25(a23,a23,x179581),x179582))), % 63.79/63.85 inference(rename_variables,[],[17884])). % 63.79/63.85 cnf(17962,plain, % 63.79/63.85 (E(f5(x179621,f25(a2,a2,x179622)),f5(x179621,f25(a23,a23,x179622)))), % 63.79/63.85 inference(rename_variables,[],[17855])). % 63.79/63.85 cnf(17964,plain, % 63.79/63.85 (E(f4(x179641,f25(a2,a2,x179642)),f4(x179641,f25(a23,a23,x179642)))), % 63.79/63.85 inference(rename_variables,[],[17861])). % 63.79/63.85 cnf(17974,plain, % 63.79/63.85 (E(f5(x179741,f25(a2,a2,x179742)),f5(x179741,f25(a23,a23,x179742)))), % 63.79/63.85 inference(rename_variables,[],[17855])). % 63.79/63.85 cnf(17976,plain, % 63.79/63.85 (E(f6(x179761,f25(a2,a2,x179762)),f6(x179761,f25(a23,a23,x179762)))), % 63.79/63.85 inference(rename_variables,[],[17867])). % 63.79/63.85 cnf(17989,plain, % 63.79/63.85 (E(f11(x179891,f25(a2,a2,x179892)),f11(x179891,f25(a23,a23,x179892)))), % 63.79/63.85 inference(rename_variables,[],[17866])). % 63.79/63.85 cnf(17992,plain, % 63.79/63.85 (E(f5(x179921,f25(a2,a2,x179922)),f5(x179921,f25(a23,a23,x179922)))), % 63.79/63.85 inference(rename_variables,[],[17855])). % 63.79/63.85 cnf(18032,plain, % 63.79/63.85 ($false), % 63.79/63.85 inference(scs_inference,[],[17667,17902,17900,17826,17832,17624,17402,17908,17758,17843,17851,17911,17913,17852,17956,17855,17962,17974,17992,17861,17964,17866,17989,17867,17976,17873,17932,17938,17943,17945,17947,17884,17958,17891,17949,17699,17552,17558,17396,17527,17417,13133,129,10797,10902,128,101,17436,17426,17442,17212,237,17232,17208,235,139,182,16327,181,183,16183,8,143,16184,388,362,16235,16326,16234,18,16392,16134,16373,16121,16385,318,11,16391,10,29,32,17,16188,16222,23,25,13,9,22,19,30,27,28,5,7,16212,396,16088,21,6,12,26,20,15,24,16189,16,31,34,33,16223,4,16331,14,16270,2,365,166,3,167,58,159,62,61,60,199]), % 63.79/63.85 ['proof']). % 63.79/63.86 % SZS output end Proof % 63.79/63.86 % Total time :63.040000s %------------------------------------------------------------------------------