%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP620+1 : TPTP v8.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n020.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:03 EDT 2024 % Result : Theorem 61.99s 62.06s % Output : CNFRefutation 62.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : GRP620+1 : TPTP v8.2.0. Released v3.4.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n020.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Thu Jun 20 09:03:24 EDT 2024 % 0.13/0.33 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 61.99/62.03 %------------------------------------------- % 61.99/62.03 % File :CSE---1.7 % 61.99/62.03 % Problem :theBenchmark % 61.99/62.03 % Transform :cnf % 61.99/62.03 % Format :tptp:raw % 61.99/62.03 % Command :java -jar mcs_scs.jar %d %s % 61.99/62.03 % 61.99/62.03 % Result :Theorem 61.410000s % 61.99/62.03 % Output :CNFRefutation 61.410000s % 61.99/62.03 %------------------------------------------- % 61.99/62.04 %------------------------------------------------------------------------------ % 61.99/62.04 % File : GRP620+1 : TPTP v8.2.0. Released v3.4.0. % 61.99/62.04 % Domain : Group Theory % 61.99/62.04 % Problem : On the Group of Inner Automorphisms T07 % 61.99/62.04 % Version : [Urb08] axioms : Especial. % 61.99/62.04 % English : % 61.99/62.04 % 61.99/62.04 % Refs : [Kor96] Kornilowicz (1996), On the Group of Inner Automorphism % 61.99/62.04 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 61.99/62.04 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 61.99/62.04 % Source : [Urb08] % 61.99/62.04 % Names : t7_autgroup [Urb08] % 61.99/62.04 % 61.99/62.04 % Status : Theorem % 61.99/62.05 % Rating : 0.36 v8.2.0, 0.31 v7.5.0, 0.34 v7.4.0, 0.27 v7.3.0, 0.34 v7.2.0, 0.31 v7.1.0, 0.26 v7.0.0, 0.20 v6.4.0, 0.27 v6.3.0, 0.25 v6.2.0, 0.32 v6.1.0, 0.37 v6.0.0, 0.30 v5.5.0, 0.44 v5.4.0, 0.46 v5.3.0, 0.56 v5.2.0, 0.40 v5.1.0, 0.43 v5.0.0, 0.46 v4.1.0, 0.52 v4.0.0, 0.58 v3.7.0, 0.55 v3.5.0, 0.53 v3.4.0 % 61.99/62.05 % Syntax : Number of formulae : 69 ( 17 unt; 0 def) % 61.99/62.05 % Number of atoms : 286 ( 8 equ) % 61.99/62.05 % Maximal formula atoms : 19 ( 4 avg) % 61.99/62.05 % Number of connectives : 257 ( 40 ~; 1 |; 148 &) % 61.99/62.05 % ( 8 <=>; 60 =>; 0 <=; 0 <~>) % 61.99/62.05 % Maximal formula depth : 12 ( 5 avg) % 61.99/62.05 % Maximal term depth : 3 ( 1 avg) % 61.99/62.05 % Number of predicates : 27 ( 25 usr; 1 prp; 0-4 aty) % 61.99/62.05 % Number of functors : 8 ( 8 usr; 1 con; 0-2 aty) % 61.99/62.05 % Number of variables : 128 ( 106 !; 22 ?) % 61.99/62.05 % SPC : FOF_THM_RFO_SEQ % 61.99/62.05 % 61.99/62.05 % Comments : Normal version: includes the axioms (which may be theorems from % 61.99/62.05 % other articles) and background that are possibly necessary. % 61.99/62.05 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 61.99/62.05 % : The problem encoding is based on set theory. % 61.99/62.05 %------------------------------------------------------------------------------ % 61.99/62.05 fof(t7_autgroup,conjecture, % 61.99/62.05 ! [A] : % 61.99/62.05 ( ( ~ v3_struct_0(A) % 61.99/62.05 & v1_group_1(A) % 61.99/62.05 & v3_group_1(A) % 61.99/62.05 & v4_group_1(A) % 61.99/62.05 & l1_group_1(A) ) % 61.99/62.05 => ! [B] : % 61.99/62.05 ( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A)) % 61.99/62.05 => m2_fraenkel(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A),k1_autgroup(A)) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(abstractness_v1_group_1,axiom, % 61.99/62.05 ! [A] : % 61.99/62.05 ( l1_group_1(A) % 61.99/62.05 => ( v1_group_1(A) % 61.99/62.05 => A = g1_group_1(u1_struct_0(A),u1_group_1(A)) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(antisymmetry_r2_hidden,axiom, % 61.99/62.05 ! [A,B] : % 61.99/62.05 ( r2_hidden(A,B) % 61.99/62.05 => ~ r2_hidden(B,A) ) ). % 61.99/62.05 % 61.99/62.05 fof(cc1_fraenkel,axiom, % 61.99/62.05 ! [A] : % 61.99/62.05 ( v1_fraenkel(A) % 61.99/62.05 => ! [B] : % 61.99/62.05 ( m1_subset_1(B,A) % 61.99/62.05 => ( v1_relat_1(B) % 61.99/62.05 & v1_funct_1(B) ) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(cc1_funct_1,axiom, % 61.99/62.05 ! [A] : % 61.99/62.05 ( v1_xboole_0(A) % 61.99/62.05 => v1_funct_1(A) ) ). % 61.99/62.05 % 61.99/62.05 fof(cc1_funct_2,axiom, % 61.99/62.05 ! [A,B,C] : % 61.99/62.05 ( m1_relset_1(C,A,B) % 61.99/62.05 => ( ( v1_funct_1(C) % 61.99/62.05 & v1_partfun1(C,A,B) ) % 61.99/62.05 => ( v1_funct_1(C) % 61.99/62.05 & v1_funct_2(C,A,B) ) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(cc1_group_1,axiom, % 61.99/62.05 ! [A] : % 61.99/62.05 ( l1_group_1(A) % 61.99/62.05 => ( ( ~ v3_struct_0(A) % 61.99/62.05 & v3_group_1(A) ) % 61.99/62.05 => ( ~ v3_struct_0(A) % 61.99/62.05 & v2_group_1(A) ) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(cc1_relset_1,axiom, % 61.99/62.05 ! [A,B,C] : % 61.99/62.05 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 61.99/62.05 => v1_relat_1(C) ) ). % 61.99/62.05 % 61.99/62.05 fof(cc2_funct_1,axiom, % 61.99/62.05 ! [A] : % 61.99/62.05 ( ( v1_relat_1(A) % 61.99/62.05 & v1_xboole_0(A) % 61.99/62.05 & v1_funct_1(A) ) % 61.99/62.05 => ( v1_relat_1(A) % 61.99/62.05 & v1_funct_1(A) % 61.99/62.05 & v2_funct_1(A) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(cc5_funct_2,axiom, % 61.99/62.05 ! [A,B] : % 61.99/62.05 ( ~ v1_xboole_0(B) % 61.99/62.05 => ! [C] : % 61.99/62.05 ( m1_relset_1(C,A,B) % 61.99/62.05 => ( ( v1_funct_1(C) % 61.99/62.05 & v1_funct_2(C,A,B) ) % 61.99/62.05 => ( v1_funct_1(C) % 61.99/62.05 & v1_partfun1(C,A,B) % 61.99/62.05 & v1_funct_2(C,A,B) ) ) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(cc6_funct_2,axiom, % 61.99/62.05 ! [A,B] : % 61.99/62.05 ( ( ~ v1_xboole_0(A) % 61.99/62.05 & ~ v1_xboole_0(B) ) % 61.99/62.05 => ! [C] : % 61.99/62.05 ( m1_relset_1(C,A,B) % 61.99/62.05 => ( ( v1_funct_1(C) % 61.99/62.05 & v1_funct_2(C,A,B) ) % 61.99/62.05 => ( v1_funct_1(C) % 61.99/62.05 & ~ v1_xboole_0(C) % 61.99/62.05 & v1_partfun1(C,A,B) % 61.99/62.05 & v1_funct_2(C,A,B) ) ) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(d12_group_6,axiom, % 61.99/62.05 ! [A] : % 61.99/62.05 ( ( ~ v3_struct_0(A) % 61.99/62.05 & v3_group_1(A) % 61.99/62.05 & v4_group_1(A) % 61.99/62.05 & l1_group_1(A) ) % 61.99/62.05 => ! [B] : % 61.99/62.05 ( ( ~ v3_struct_0(B) % 61.99/62.05 & v3_group_1(B) % 61.99/62.05 & v4_group_1(B) % 61.99/62.05 & l1_group_1(B) ) % 61.99/62.05 => ! [C] : % 61.99/62.05 ( ( v1_funct_1(C) % 61.99/62.05 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 61.99/62.05 & v1_group_6(C,A,B) % 61.99/62.05 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) % 61.99/62.05 => ( v2_group_6(C,A,B) % 61.99/62.05 <=> v2_funct_1(C) ) ) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(d14_group_6,axiom, % 61.99/62.05 ! [A] : % 61.99/62.05 ( ( ~ v3_struct_0(A) % 61.99/62.05 & v3_group_1(A) % 61.99/62.05 & v4_group_1(A) % 61.99/62.05 & l1_group_1(A) ) % 61.99/62.05 => ! [B] : % 61.99/62.05 ( ( ~ v3_struct_0(B) % 61.99/62.05 & v3_group_1(B) % 61.99/62.05 & v4_group_1(B) % 61.99/62.05 & l1_group_1(B) ) % 61.99/62.05 => ! [C] : % 61.99/62.05 ( ( v1_funct_1(C) % 61.99/62.05 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 61.99/62.05 & v1_group_6(C,A,B) % 61.99/62.05 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) % 61.99/62.05 => ( v4_group_6(C,A,B) % 61.99/62.05 <=> ( v3_group_6(C,A,B) % 61.99/62.05 & v2_group_6(C,A,B) ) ) ) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(d1_autgroup,axiom, % 61.99/62.05 ! [A] : % 61.99/62.05 ( ( ~ v3_struct_0(A) % 61.99/62.05 & v1_group_1(A) % 61.99/62.05 & v3_group_1(A) % 61.99/62.05 & v4_group_1(A) % 61.99/62.05 & l1_group_1(A) ) % 61.99/62.05 => ! [B] : % 61.99/62.05 ( m1_fraenkel(B,u1_struct_0(A),u1_struct_0(A)) % 61.99/62.05 => ( B = k1_autgroup(A) % 61.99/62.05 <=> ( ! [C] : % 61.99/62.05 ( m2_fraenkel(C,u1_struct_0(A),u1_struct_0(A),B) % 61.99/62.05 => ( v1_funct_1(C) % 61.99/62.05 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)) % 61.99/62.05 & v1_group_6(C,A,A) % 61.99/62.05 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)) ) ) % 61.99/62.05 & ! [C] : % 61.99/62.05 ( ( v1_funct_1(C) % 61.99/62.05 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)) % 61.99/62.05 & v1_group_6(C,A,A) % 61.99/62.05 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)) ) % 61.99/62.05 => ( r2_hidden(C,B) % 61.99/62.05 <=> ( v2_funct_1(C) % 61.99/62.05 & v3_group_6(C,A,A) ) ) ) ) ) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(dt_g1_group_1,axiom, % 61.99/62.05 ! [A,B] : % 61.99/62.05 ( ( v1_funct_1(B) % 61.99/62.05 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 61.99/62.05 & m1_relset_1(B,k2_zfmisc_1(A,A),A) ) % 61.99/62.05 => ( v1_group_1(g1_group_1(A,B)) % 61.99/62.05 & l1_group_1(g1_group_1(A,B)) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(dt_k1_autgroup,axiom, % 61.99/62.05 ! [A] : % 61.99/62.05 ( ( ~ v3_struct_0(A) % 61.99/62.05 & v1_group_1(A) % 61.99/62.05 & v3_group_1(A) % 61.99/62.05 & v4_group_1(A) % 61.99/62.05 & l1_group_1(A) ) % 61.99/62.05 => m1_fraenkel(k1_autgroup(A),u1_struct_0(A),u1_struct_0(A)) ) ). % 61.99/62.05 % 61.99/62.05 fof(dt_k1_xboole_0,axiom, % 61.99/62.05 $true ). % 61.99/62.05 % 61.99/62.05 fof(dt_k1_zfmisc_1,axiom, % 61.99/62.05 $true ). % 61.99/62.05 % 61.99/62.05 fof(dt_k2_funct_1,axiom, % 61.99/62.05 ! [A] : % 61.99/62.05 ( ( v1_relat_1(A) % 61.99/62.05 & v1_funct_1(A) ) % 61.99/62.05 => ( v1_relat_1(k2_funct_1(A)) % 61.99/62.05 & v1_funct_1(k2_funct_1(A)) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(dt_k2_zfmisc_1,axiom, % 61.99/62.05 $true ). % 61.99/62.05 % 61.99/62.05 fof(dt_l1_group_1,axiom, % 61.99/62.05 ! [A] : % 61.99/62.05 ( l1_group_1(A) % 61.99/62.05 => l1_struct_0(A) ) ). % 61.99/62.05 % 61.99/62.05 fof(dt_l1_struct_0,axiom, % 61.99/62.05 $true ). % 61.99/62.05 % 61.99/62.05 fof(dt_m1_fraenkel,axiom, % 61.99/62.05 ! [A,B,C] : % 61.99/62.05 ( m1_fraenkel(C,A,B) % 61.99/62.05 => ( ~ v1_xboole_0(C) % 61.99/62.05 & v1_fraenkel(C) ) ) ). % 61.99/62.05 % 61.99/62.05 fof(dt_m1_relset_1,axiom, % 61.99/62.05 $true ). % 61.99/62.05 % 61.99/62.05 fof(dt_m1_subset_1,axiom, % 61.99/62.05 $true ). % 61.99/62.05 % 61.99/62.05 fof(dt_m2_fraenkel,axiom, % 61.99/62.05 ! [A,B,C] : % 61.99/62.05 ( ( ~ v1_xboole_0(B) % 61.99/62.05 & m1_fraenkel(C,A,B) ) % 61.99/62.06 => ! [D] : % 61.99/62.06 ( m2_fraenkel(D,A,B,C) % 61.99/62.06 => ( v1_funct_1(D) % 61.99/62.06 & v1_funct_2(D,A,B) % 61.99/62.06 & m2_relset_1(D,A,B) ) ) ) ). % 61.99/62.06 % 61.99/62.06 fof(dt_m2_relset_1,axiom, % 61.99/62.06 ! [A,B,C] : % 61.99/62.06 ( m2_relset_1(C,A,B) % 61.99/62.06 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 61.99/62.06 % 61.99/62.06 fof(dt_u1_group_1,axiom, % 61.99/62.06 ! [A] : % 61.99/62.06 ( l1_group_1(A) % 61.99/62.06 => ( v1_funct_1(u1_group_1(A)) % 61.99/62.06 & v1_funct_2(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 61.99/62.06 & m2_relset_1(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 61.99/62.06 % 61.99/62.06 fof(dt_u1_struct_0,axiom, % 61.99/62.06 $true ). % 61.99/62.06 % 61.99/62.06 fof(existence_l1_group_1,axiom, % 61.99/62.06 ? [A] : l1_group_1(A) ). % 61.99/62.06 % 61.99/62.06 fof(existence_l1_struct_0,axiom, % 61.99/62.06 ? [A] : l1_struct_0(A) ). % 61.99/62.06 % 61.99/62.06 fof(existence_m1_fraenkel,axiom, % 61.99/62.06 ! [A,B] : % 61.99/62.06 ? [C] : m1_fraenkel(C,A,B) ). % 61.99/62.06 % 61.99/62.06 fof(existence_m1_relset_1,axiom, % 61.99/62.06 ! [A,B] : % 61.99/62.06 ? [C] : m1_relset_1(C,A,B) ). % 61.99/62.06 % 61.99/62.06 fof(existence_m1_subset_1,axiom, % 61.99/62.06 ! [A] : % 61.99/62.06 ? [B] : m1_subset_1(B,A) ). % 61.99/62.06 % 61.99/62.06 fof(existence_m2_fraenkel,axiom, % 61.99/62.06 ! [A,B,C] : % 61.99/62.06 ( ( ~ v1_xboole_0(B) % 61.99/62.06 & m1_fraenkel(C,A,B) ) % 61.99/62.06 => ? [D] : m2_fraenkel(D,A,B,C) ) ). % 61.99/62.06 % 61.99/62.06 fof(existence_m2_relset_1,axiom, % 61.99/62.06 ! [A,B] : % 61.99/62.06 ? [C] : m2_relset_1(C,A,B) ). % 61.99/62.06 % 61.99/62.06 fof(fc1_group_1,axiom, % 61.99/62.06 ! [A,B] : % 61.99/62.06 ( ( ~ v1_xboole_0(A) % 61.99/62.06 & v1_funct_1(B) % 61.99/62.06 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 61.99/62.06 & m1_relset_1(B,k2_zfmisc_1(A,A),A) ) % 61.99/62.06 => ( ~ v3_struct_0(g1_group_1(A,B)) % 61.99/62.06 & v1_group_1(g1_group_1(A,B)) ) ) ). % 61.99/62.06 % 61.99/62.06 fof(fc1_struct_0,axiom, % 61.99/62.06 ! [A] : % 61.99/62.06 ( ( ~ v3_struct_0(A) % 61.99/62.06 & l1_struct_0(A) ) % 61.99/62.06 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 61.99/62.06 % 61.99/62.06 fof(fc1_xboole_0,axiom, % 61.99/62.06 v1_xboole_0(k1_xboole_0) ). % 61.99/62.06 % 61.99/62.06 fof(free_g1_group_1,axiom, % 61.99/62.06 ! [A,B] : % 61.99/62.06 ( ( v1_funct_1(B) % 61.99/62.06 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 61.99/62.06 & m1_relset_1(B,k2_zfmisc_1(A,A),A) ) % 61.99/62.06 => ! [C,D] : % 61.99/62.06 ( g1_group_1(A,B) = g1_group_1(C,D) % 61.99/62.06 => ( A = C % 61.99/62.06 & B = D ) ) ) ). % 61.99/62.06 % 61.99/62.06 fof(rc1_fraenkel,axiom, % 61.99/62.06 ? [A] : % 61.99/62.06 ( ~ v1_xboole_0(A) % 61.99/62.06 & v1_fraenkel(A) ) ). % 61.99/62.06 % 61.99/62.06 fof(rc1_funct_1,axiom, % 61.99/62.06 ? [A] : % 61.99/62.06 ( v1_relat_1(A) % 61.99/62.06 & v1_funct_1(A) ) ). % 61.99/62.06 % 61.99/62.06 fof(rc1_funct_2,axiom, % 61.99/62.06 ! [A,B] : % 61.99/62.06 ? [C] : % 61.99/62.06 ( m1_relset_1(C,A,B) % 61.99/62.06 & v1_relat_1(C) % 61.99/62.06 & v1_funct_1(C) % 61.99/62.06 & v1_funct_2(C,A,B) ) ). % 61.99/62.06 % 61.99/62.06 fof(rc1_group_1,axiom, % 61.99/62.06 ? [A] : % 61.99/62.06 ( l1_group_1(A) % 61.99/62.06 & v1_group_1(A) ) ). % 61.99/62.06 % 61.99/62.06 fof(rc1_partfun1,axiom, % 61.99/62.06 ? [A] : % 61.99/62.06 ( v1_relat_1(A) % 61.99/62.06 & v1_funct_1(A) % 61.99/62.06 & v2_funct_1(A) % 61.99/62.06 & v1_xboole_0(A) ) ). % 61.99/62.06 % 61.99/62.06 fof(rc1_xboole_0,axiom, % 61.99/62.06 ? [A] : v1_xboole_0(A) ). % 61.99/62.06 % 61.99/62.06 fof(rc2_funct_1,axiom, % 61.99/62.06 ? [A] : % 61.99/62.06 ( v1_relat_1(A) % 61.99/62.06 & v1_xboole_0(A) % 61.99/62.06 & v1_funct_1(A) ) ). % 61.99/62.06 % 61.99/62.06 fof(rc2_group_1,axiom, % 61.99/62.06 ? [A] : % 61.99/62.06 ( l1_group_1(A) % 61.99/62.06 & ~ v3_struct_0(A) % 61.99/62.06 & v1_group_1(A) ) ). % 61.99/62.06 % 61.99/62.06 fof(rc2_group_6,axiom, % 61.99/62.06 ! [A,B] : % 61.99/62.06 ( ( ~ v3_struct_0(A) % 61.99/62.06 & v3_group_1(A) % 61.99/62.06 & v4_group_1(A) % 61.99/62.06 & l1_group_1(A) % 61.99/62.06 & ~ v3_struct_0(B) % 61.99/62.06 & v3_group_1(B) % 61.99/62.06 & v4_group_1(B) % 61.99/62.06 & l1_group_1(B) ) % 61.99/62.06 => ? [C] : % 61.99/62.06 ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 61.99/62.06 & ~ v1_xboole_0(C) % 61.99/62.06 & v1_relat_1(C) % 61.99/62.06 & v1_funct_1(C) % 61.99/62.06 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 61.99/62.06 & v1_partfun1(C,u1_struct_0(A),u1_struct_0(B)) % 61.99/62.06 & v1_group_6(C,A,B) ) ) ). % 61.99/62.06 % 61.99/62.06 fof(rc2_partfun1,axiom, % 61.99/62.06 ! [A,B] : % 61.99/62.06 ? [C] : % 61.99/62.06 ( m1_relset_1(C,A,B) % 61.99/62.06 & v1_relat_1(C) % 61.99/62.06 & v1_funct_1(C) ) ). % 61.99/62.06 % 61.99/62.06 fof(rc2_xboole_0,axiom, % 61.99/62.06 ? [A] : ~ v1_xboole_0(A) ). % 61.99/62.06 % 61.99/62.06 fof(rc3_funct_1,axiom, % 61.99/62.06 ? [A] : % 61.99/62.06 ( v1_relat_1(A) % 61.99/62.06 & v1_funct_1(A) % 61.99/62.06 & v2_funct_1(A) ) ). % 61.99/62.06 % 61.99/62.06 fof(rc3_group_1,axiom, % 61.99/62.06 ? [A] : % 61.99/62.06 ( l1_group_1(A) % 61.99/62.06 & ~ v3_struct_0(A) % 61.99/62.06 & v1_group_1(A) % 61.99/62.06 & v2_group_1(A) % 61.99/62.06 & v3_group_1(A) % 61.99/62.06 & v4_group_1(A) ) ). % 61.99/62.06 % 61.99/62.06 fof(rc3_struct_0,axiom, % 61.99/62.06 ? [A] : % 61.99/62.06 ( l1_struct_0(A) % 61.99/62.06 & ~ v3_struct_0(A) ) ). % 61.99/62.06 % 61.99/62.06 fof(rc5_struct_0,axiom, % 61.99/62.06 ! [A] : % 61.99/62.06 ( ( ~ v3_struct_0(A) % 61.99/62.06 & l1_struct_0(A) ) % 61.99/62.06 => ? [B] : % 61.99/62.06 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 61.99/62.06 & ~ v1_xboole_0(B) ) ) ). % 61.99/62.06 % 61.99/62.06 fof(redefinition_m2_fraenkel,axiom, % 61.99/62.06 ! [A,B,C] : % 61.99/62.06 ( ( ~ v1_xboole_0(B) % 61.99/62.06 & m1_fraenkel(C,A,B) ) % 61.99/62.06 => ! [D] : % 61.99/62.06 ( m2_fraenkel(D,A,B,C) % 61.99/62.06 <=> m1_subset_1(D,C) ) ) ). % 61.99/62.06 % 61.99/62.06 fof(redefinition_m2_relset_1,axiom, % 61.99/62.06 ! [A,B,C] : % 61.99/62.06 ( m2_relset_1(C,A,B) % 61.99/62.06 <=> m1_relset_1(C,A,B) ) ). % 61.99/62.06 % 61.99/62.06 fof(reflexivity_r1_tarski,axiom, % 61.99/62.06 ! [A,B] : r1_tarski(A,A) ). % 61.99/62.06 % 61.99/62.06 fof(t1_subset,axiom, % 61.99/62.06 ! [A,B] : % 61.99/62.06 ( r2_hidden(A,B) % 61.99/62.06 => m1_subset_1(A,B) ) ). % 61.99/62.06 % 61.99/62.06 fof(t2_subset,axiom, % 61.99/62.06 ! [A,B] : % 61.99/62.06 ( m1_subset_1(A,B) % 61.99/62.06 => ( v1_xboole_0(B) % 61.99/62.06 | r2_hidden(A,B) ) ) ). % 61.99/62.06 % 61.99/62.06 fof(t3_subset,axiom, % 61.99/62.06 ! [A,B] : % 61.99/62.06 ( m1_subset_1(A,k1_zfmisc_1(B)) % 61.99/62.06 <=> r1_tarski(A,B) ) ). % 61.99/62.06 % 61.99/62.06 fof(t4_subset,axiom, % 61.99/62.06 ! [A,B,C] : % 61.99/62.06 ( ( r2_hidden(A,B) % 61.99/62.06 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 61.99/62.06 => m1_subset_1(A,C) ) ). % 61.99/62.06 % 61.99/62.06 fof(t5_autgroup,axiom, % 61.99/62.06 ! [A] : % 61.99/62.06 ( ( ~ v3_struct_0(A) % 61.99/62.06 & v1_group_1(A) % 61.99/62.06 & v3_group_1(A) % 61.99/62.06 & v4_group_1(A) % 61.99/62.06 & l1_group_1(A) ) % 61.99/62.06 => ! [B] : % 61.99/62.06 ( ( v1_funct_1(B) % 61.99/62.06 & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)) % 61.99/62.06 & v1_group_6(B,A,A) % 61.99/62.06 & m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)) ) % 61.99/62.06 => ( r2_hidden(B,k1_autgroup(A)) % 61.99/62.06 <=> v4_group_6(B,A,A) ) ) ) ). % 61.99/62.06 % 61.99/62.06 fof(t5_subset,axiom, % 61.99/62.06 ! [A,B,C] : % 61.99/62.06 ~ ( r2_hidden(A,B) % 61.99/62.06 & m1_subset_1(B,k1_zfmisc_1(C)) % 61.99/62.06 & v1_xboole_0(C) ) ). % 61.99/62.06 % 61.99/62.06 fof(t6_autgroup,axiom, % 61.99/62.06 ! [A] : % 61.99/62.06 ( ( ~ v3_struct_0(A) % 61.99/62.06 & v1_group_1(A) % 61.99/62.06 & v3_group_1(A) % 61.99/62.06 & v4_group_1(A) % 61.99/62.06 & l1_group_1(A) ) % 61.99/62.06 => ! [B] : % 61.99/62.06 ( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A)) % 61.99/62.06 => ( v1_funct_1(k2_funct_1(B)) % 61.99/62.06 & v1_funct_2(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A)) % 61.99/62.06 & v1_group_6(k2_funct_1(B),A,A) % 61.99/62.06 & m2_relset_1(k2_funct_1(B),u1_struct_0(A),u1_struct_0(A)) ) ) ) ). % 61.99/62.06 % 61.99/62.06 fof(t6_boole,axiom, % 61.99/62.06 ! [A] : % 61.99/62.06 ( v1_xboole_0(A) % 61.99/62.06 => A = k1_xboole_0 ) ). % 61.99/62.06 % 61.99/62.06 fof(t73_group_6,axiom, % 61.99/62.06 ! [A] : % 61.99/62.06 ( ( ~ v3_struct_0(A) % 61.99/62.06 & v3_group_1(A) % 61.99/62.06 & v4_group_1(A) % 61.99/62.06 & l1_group_1(A) ) % 61.99/62.06 => ! [B] : % 61.99/62.06 ( ( ~ v3_struct_0(B) % 61.99/62.06 & v3_group_1(B) % 61.99/62.06 & v4_group_1(B) % 61.99/62.06 & l1_group_1(B) ) % 61.99/62.06 => ! [C] : % 61.99/62.06 ( ( v1_funct_1(C) % 61.99/62.06 & v1_funct_2(C,u1_struct_0(B),u1_struct_0(A)) % 61.99/62.06 & v1_group_6(C,B,A) % 61.99/62.06 & m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) ) % 61.99/62.06 => ! [D] : % 61.99/62.06 ( ( v1_funct_1(D) % 61.99/62.06 & v1_funct_2(D,u1_struct_0(A),u1_struct_0(B)) % 61.99/62.06 & v1_group_6(D,A,B) % 61.99/62.06 & m2_relset_1(D,u1_struct_0(A),u1_struct_0(B)) ) % 61.99/62.06 => ( ( v4_group_6(C,B,A) % 61.99/62.06 & D = k2_funct_1(C) ) % 61.99/62.06 => v4_group_6(D,A,B) ) ) ) ) ) ). % 61.99/62.06 % 61.99/62.06 fof(t7_boole,axiom, % 61.99/62.06 ! [A,B] : % 61.99/62.06 ~ ( r2_hidden(A,B) % 61.99/62.06 & v1_xboole_0(B) ) ). % 61.99/62.06 % 61.99/62.06 fof(t8_boole,axiom, % 61.99/62.06 ! [A,B] : % 61.99/62.06 ~ ( v1_xboole_0(A) % 61.99/62.06 & A != B % 61.99/62.06 & v1_xboole_0(B) ) ). % 61.99/62.06 % 61.99/62.06 %------------------------------------------------------------------------------ % 61.99/62.06 %------------------------------------------- % 61.99/62.06 % Proof found % 61.99/62.06 % SZS status Theorem for theBenchmark % 61.99/62.06 % SZS output start Proof % 61.99/62.06 %ClaNum:221(EqnAxiom:82) % 61.99/62.06 %VarNum:1126(SingletonVarNum:219) % 61.99/62.06 %MaxLitNum:19 % 61.99/62.06 %MaxfuncDepth:2 % 61.99/62.06 %SharedTerms:58 % 61.99/62.06 %goalClause: 83 87 89 91 126 127 133 % 61.99/62.06 %singleGoalClaCount:7 % 61.99/62.06 [83]P1(a1) % 61.99/62.06 [84]P1(a2) % 61.99/62.06 [85]P1(a8) % 61.99/62.06 [86]P1(a12) % 61.99/62.06 [87]P14(a1) % 61.99/62.06 [88]P14(a12) % 61.99/62.06 [89]P22(a1) % 61.99/62.06 [90]P22(a12) % 61.99/62.06 [91]P2(a1) % 61.99/62.06 [92]P2(a17) % 61.99/62.06 [93]P2(a2) % 61.99/62.06 [94]P2(a8) % 61.99/62.06 [95]P2(a12) % 61.99/62.06 [96]P3(a3) % 61.99/62.06 [97]P15(a6) % 61.99/62.06 [98]P15(a9) % 61.99/62.06 [99]P15(a10) % 61.99/62.06 [100]P15(a13) % 61.99/62.06 [101]P12(a6) % 61.99/62.06 [102]P12(a9) % 61.99/62.06 [103]P12(a10) % 61.99/62.06 [104]P12(a13) % 61.99/62.06 [105]P18(a23) % 61.99/62.06 [106]P18(a9) % 61.99/62.06 [107]P18(a11) % 61.99/62.06 [108]P18(a10) % 61.99/62.06 [109]P19(a12) % 61.99/62.06 [110]P20(a9) % 61.99/62.06 [111]P20(a13) % 61.99/62.06 [112]P4(a24) % 61.99/62.06 [113]P4(a18) % 61.99/62.06 [127]~P23(a1) % 61.99/62.06 [128]~P23(a8) % 61.99/62.06 [129]~P23(a12) % 61.99/62.06 [130]~P23(a18) % 61.99/62.06 [131]~P18(a3) % 61.99/62.06 [132]~P18(a16) % 61.99/62.06 [126]P10(a19,f30(a1),f30(a1),f28(a1)) % 61.99/62.06 [133]~P10(f31(a19),f30(a1),f30(a1),f28(a1)) % 61.99/62.06 [114]P5(x1141,x1141) % 61.99/62.06 [115]P6(f25(x1151),x1151) % 61.99/62.06 [116]P15(f7(x1161,x1162)) % 61.99/62.06 [117]P15(f14(x1171,x1172)) % 61.99/62.07 [118]P12(f7(x1181,x1182)) % 61.99/62.07 [119]P12(f14(x1191,x1192)) % 61.99/62.07 [120]P7(f26(x1201,x1202),x1201,x1202) % 61.99/62.07 [121]P7(f7(x1211,x1212),x1211,x1212) % 61.99/62.07 [122]P7(f14(x1221,x1222),x1221,x1222) % 61.99/62.07 [123]P13(f7(x1231,x1232),x1231,x1232) % 61.99/62.07 [124]P9(f4(x1241,x1242),x1241,x1242) % 61.99/62.07 [125]P8(f27(x1251,x1252),x1251,x1252) % 61.99/62.07 [134]~P18(x1341)+E(x1341,a23) % 61.99/62.07 [135]~P18(x1351)+P12(x1351) % 61.99/62.07 [136]~P2(x1361)+P4(x1361) % 61.99/62.07 [138]~P2(x1381)+P12(f33(x1381)) % 61.99/62.07 [164]~P2(x1641)+P13(f33(x1641),f34(f30(x1641),f30(x1641)),f30(x1641)) % 61.99/62.07 [165]~P2(x1651)+P9(f33(x1651),f34(f30(x1651),f30(x1651)),f30(x1651)) % 61.99/62.07 [145]~P18(x1451)+~P11(x1452,x1451) % 61.99/62.07 [148]~P11(x1481,x1482)+P6(x1481,x1482) % 61.99/62.07 [152]~P11(x1522,x1521)+~P11(x1521,x1522) % 61.99/62.07 [151]~P5(x1511,x1512)+P6(x1511,f32(x1512)) % 61.99/62.07 [153]P5(x1531,x1532)+~P6(x1531,f32(x1532)) % 61.99/62.07 [159]P3(x1591)+~P8(x1591,x1592,x1593) % 61.99/62.07 [160]~P18(x1601)+~P8(x1601,x1602,x1603) % 61.99/62.07 [167]~P9(x1671,x1672,x1673)+P7(x1671,x1672,x1673) % 61.99/62.07 [168]~P7(x1681,x1682,x1683)+P9(x1681,x1682,x1683) % 61.99/62.07 [163]P15(x1631)+~P6(x1631,f32(f34(x1632,x1633))) % 61.99/62.07 [172]~P9(x1721,x1722,x1723)+P6(x1721,f32(f34(x1722,x1723))) % 61.99/62.07 [140]~P15(x1401)+~P12(x1401)+P15(f31(x1401)) % 61.99/62.07 [141]~P15(x1411)+~P12(x1411)+P12(f31(x1411)) % 61.99/62.07 [143]~P4(x1431)+P23(x1431)+~P18(f30(x1431)) % 61.99/62.07 [144]~P4(x1441)+P23(x1441)+~P18(f20(x1441)) % 61.99/62.07 [150]~P1(x1501)+~P2(x1501)+E(f29(f30(x1501),f33(x1501)),x1501) % 61.99/62.07 [154]~P4(x1541)+P23(x1541)+P6(f20(x1541),f32(f30(x1541))) % 61.99/62.07 [137]~P18(x1372)+~P18(x1371)+E(x1371,x1372) % 61.99/62.07 [146]~P6(x1461,x1462)+P15(x1461)+~P3(x1462) % 61.99/62.07 [147]~P6(x1471,x1472)+P12(x1471)+~P3(x1472) % 61.99/62.07 [149]~P6(x1492,x1491)+P18(x1491)+P11(x1492,x1491) % 61.99/62.07 [155]~P18(x1551)+~P11(x1552,x1553)+~P6(x1553,f32(x1551)) % 61.99/62.07 [156]P6(x1561,x1562)+~P11(x1561,x1563)+~P6(x1563,f32(x1562)) % 61.99/62.07 [187]~P8(x1873,x1872,x1871)+P18(x1871)+P10(f5(x1872,x1871,x1873),x1872,x1871,x1873) % 61.99/62.07 [139]P19(x1391)+~P14(x1391)+~P2(x1391)+P23(x1391) % 61.99/62.07 [142]~P15(x1421)+~P12(x1421)+~P18(x1421)+P20(x1421) % 61.99/62.07 [177]~P12(x1772)+~P7(x1772,f34(x1771,x1771),x1771)+~P13(x1772,f34(x1771,x1771),x1771)+P1(f29(x1771,x1772)) % 61.99/62.07 [178]~P12(x1782)+~P7(x1782,f34(x1781,x1781),x1781)+~P13(x1782,f34(x1781,x1781),x1781)+P2(f29(x1781,x1782)) % 61.99/62.07 [174]~P12(x1741)+~P7(x1741,x1742,x1743)+~P17(x1741,x1742,x1743)+P13(x1741,x1742,x1743) % 61.99/62.07 [183]~P6(x1832,x1834)+~P8(x1834,x1833,x1831)+P18(x1831)+P10(x1832,x1833,x1831,x1834) % 61.99/62.07 [192]~P10(x1921,x1924,x1922,x1923)+P12(x1921)+~P8(x1923,x1924,x1922)+P18(x1922) % 61.99/62.07 [193]~P10(x1932,x1934,x1931,x1933)+P18(x1931)+~P8(x1933,x1934,x1931)+P6(x1932,x1933) % 61.99/62.07 [204]~P10(x2042,x2043,x2041,x2044)+P18(x2041)+P13(x2042,x2043,x2041)+~P8(x2044,x2043,x2041) % 61.99/62.07 [205]~P10(x2052,x2053,x2051,x2054)+P18(x2051)+P9(x2052,x2053,x2051)+~P8(x2054,x2053,x2051) % 61.99/62.07 [182]P18(x1821)+~P12(x1822)+~P7(x1822,f34(x1821,x1821),x1821)+~P13(x1822,f34(x1821,x1821),x1821)+~P23(f29(x1821,x1822)) % 61.99/62.07 [175]~P12(x1752)+~P7(x1752,x1753,x1751)+~P13(x1752,x1753,x1751)+P18(x1751)+P17(x1752,x1753,x1751) % 61.99/62.07 [180]~P12(x1801)+E(x1801,x1802)+~P7(x1801,f34(x1803,x1803),x1803)+~P13(x1801,f34(x1803,x1803),x1803)+~E(f29(x1803,x1801),f29(x1804,x1802)) % 61.99/62.07 [181]~P12(x1813)+E(x1811,x1812)+~P7(x1813,f34(x1811,x1811),x1811)+~P13(x1813,f34(x1811,x1811),x1811)+~E(f29(x1811,x1813),f29(x1812,x1814)) % 61.99/62.07 [162]~P1(x1621)+~P14(x1621)+~P22(x1621)+~P2(x1621)+P23(x1621)+P8(f28(x1621),f30(x1621),f30(x1621)) % 61.99/62.07 [173]~P18(x1733)+~P7(x1733,x1732,x1731)+~P13(x1733,x1732,x1731)+P18(x1731)+P18(x1732)+~P12(x1733) % 61.99/62.07 [190]~P1(x1901)+~P14(x1901)+~P22(x1901)+~P2(x1901)+P23(x1901)+~P10(x1902,f30(x1901),f30(x1901),f28(x1901))+P12(f31(x1902)) % 61.99/62.07 [198]~P1(x1981)+~P14(x1981)+~P22(x1981)+~P2(x1981)+P23(x1981)+~P10(x1982,f30(x1981),f30(x1981),f28(x1981))+P16(f31(x1982),x1981,x1981) % 61.99/62.07 [201]~P1(x2011)+~P14(x2011)+~P22(x2011)+~P2(x2011)+P23(x2011)+~P10(x2012,f30(x2011),f30(x2011),f28(x2011))+P13(f31(x2012),f30(x2011),f30(x2011)) % 61.99/62.07 [202]~P1(x2021)+~P14(x2021)+~P22(x2021)+~P2(x2021)+P23(x2021)+~P10(x2022,f30(x2021),f30(x2021),f28(x2021))+P9(f31(x2022),f30(x2021),f30(x2021)) % 61.99/62.07 [157]~P14(x1571)+~P14(x1572)+~P22(x1571)+~P22(x1572)+~P2(x1571)+~P2(x1572)+P23(x1571)+P23(x1572)+P15(f15(x1572,x1571)) % 61.99/62.07 [158]~P14(x1581)+~P14(x1582)+~P22(x1581)+~P22(x1582)+~P2(x1581)+~P2(x1582)+P23(x1581)+P23(x1582)+P12(f15(x1582,x1581)) % 61.99/62.07 [161]~P14(x1611)+~P14(x1612)+~P22(x1611)+~P22(x1612)+~P2(x1611)+~P2(x1612)+P23(x1611)+P23(x1612)+~P18(f15(x1612,x1611)) % 61.99/62.07 [166]~P14(x1661)+~P14(x1662)+~P22(x1661)+~P22(x1662)+~P2(x1661)+~P2(x1662)+P23(x1661)+P23(x1662)+P16(f15(x1662,x1661),x1662,x1661) % 61.99/62.07 [169]~P14(x1691)+~P14(x1692)+~P22(x1691)+~P22(x1692)+~P2(x1691)+~P2(x1692)+P23(x1691)+P23(x1692)+P7(f15(x1692,x1691),f30(x1692),f30(x1691)) % 61.99/62.07 [170]~P14(x1701)+~P14(x1702)+~P22(x1701)+~P22(x1702)+~P2(x1701)+~P2(x1702)+P23(x1701)+P23(x1702)+P17(f15(x1702,x1701),f30(x1702),f30(x1701)) % 61.99/62.07 [171]~P14(x1711)+~P14(x1712)+~P22(x1711)+~P22(x1712)+~P2(x1711)+~P2(x1712)+P23(x1711)+P23(x1712)+P13(f15(x1712,x1711),f30(x1712),f30(x1711)) % 61.99/62.07 [189]P23(x1892)+~P1(x1892)+~P14(x1892)+~P22(x1892)+~P2(x1892)+P10(f22(x1892,x1891),f30(x1892),f30(x1892),x1891)+~P8(x1891,f30(x1892),f30(x1892))+E(x1891,f28(x1892))+P12(f21(x1892,x1891)) % 61.99/62.07 [197]P23(x1972)+~P1(x1972)+~P14(x1972)+~P22(x1972)+~P2(x1972)+P10(f22(x1972,x1971),f30(x1972),f30(x1972),x1971)+P16(f21(x1972,x1971),x1972,x1972)+~P8(x1971,f30(x1972),f30(x1972))+E(x1971,f28(x1972)) % 61.99/62.07 [199]P23(x1992)+~P1(x1992)+~P14(x1992)+~P22(x1992)+~P2(x1992)+P10(f22(x1992,x1991),f30(x1992),f30(x1992),x1991)+P13(f21(x1992,x1991),f30(x1992),f30(x1992))+~P8(x1991,f30(x1992),f30(x1992))+E(x1991,f28(x1992)) % 61.99/62.07 [200]P23(x2002)+~P1(x2002)+~P14(x2002)+~P22(x2002)+~P2(x2002)+P10(f22(x2002,x2001),f30(x2002),f30(x2002),x2001)+P9(f21(x2002,x2001),f30(x2002),f30(x2002))+~P8(x2001,f30(x2002),f30(x2002))+E(x2001,f28(x2002)) % 61.99/62.07 [208]~P1(x2081)+~P14(x2081)+~P22(x2081)+~P2(x2081)+P23(x2081)+P12(x2082)+~P10(x2082,f30(x2081),f30(x2081),x2083)+~P8(x2083,f30(x2081),f30(x2081))+~E(x2083,f28(x2081)) % 61.99/62.07 [210]~P1(x2101)+~P14(x2101)+~P22(x2101)+~P2(x2101)+P16(x2102,x2101,x2101)+P23(x2101)+~P10(x2102,f30(x2101),f30(x2101),x2103)+~P8(x2103,f30(x2101),f30(x2101))+~E(x2103,f28(x2101)) % 61.99/62.07 [211]~P1(x2111)+~P14(x2111)+~P22(x2111)+~P2(x2111)+P23(x2111)+~P10(x2112,f30(x2111),f30(x2111),x2113)+~P8(x2113,f30(x2111),f30(x2111))+P13(x2112,f30(x2111),f30(x2111))+~E(x2113,f28(x2111)) % 61.99/62.07 [212]~P1(x2121)+~P14(x2121)+~P22(x2121)+~P2(x2121)+P23(x2121)+~P10(x2122,f30(x2121),f30(x2121),x2123)+~P8(x2123,f30(x2121),f30(x2121))+P9(x2122,f30(x2121),f30(x2121))+~E(x2123,f28(x2121)) % 61.99/62.07 [196]P23(x1962)+~P1(x1962)+~P14(x1962)+~P22(x1962)+~P2(x1962)+P10(f22(x1962,x1961),f30(x1962),f30(x1962),x1961)+~P8(x1961,f30(x1962),f30(x1962))+P11(f21(x1962,x1961),x1961)+E(x1961,f28(x1962))+P20(f21(x1962,x1961)) % 61.99/62.07 [206]P23(x2062)+~P1(x2062)+~P14(x2062)+~P22(x2062)+~P2(x2062)+P10(f22(x2062,x2061),f30(x2062),f30(x2062),x2061)+P24(f21(x2062,x2061),x2062,x2062)+~P8(x2061,f30(x2062),f30(x2062))+P11(f21(x2062,x2061),x2061)+E(x2061,f28(x2062)) % 61.99/62.07 [185]~P1(x1851)+~P14(x1851)+~P22(x1851)+~P2(x1851)+~P12(x1852)+~P16(x1852,x1851,x1851)+P25(x1852,x1851,x1851)+P23(x1851)+~P13(x1852,f30(x1851),f30(x1851))+~P9(x1852,f30(x1851),f30(x1851))+~P11(x1852,f28(x1851)) % 61.99/62.07 [186]~P1(x1861)+~P14(x1861)+~P22(x1861)+~P2(x1861)+~P12(x1862)+~P16(x1862,x1861,x1861)+~P25(x1862,x1861,x1861)+P23(x1861)+~P13(x1862,f30(x1861),f30(x1861))+~P9(x1862,f30(x1861),f30(x1861))+P11(x1862,f28(x1861)) % 61.99/62.07 [214]P23(x2142)+~P1(x2142)+~P14(x2142)+~P22(x2142)+~P2(x2142)+P10(f22(x2142,x2141),f30(x2142),f30(x2142),x2141)+~P24(f21(x2142,x2141),x2142,x2142)+~P8(x2141,f30(x2142),f30(x2142))+~P11(f21(x2142,x2141),x2141)+E(x2141,f28(x2142))+~P20(f21(x2142,x2141)) % 61.99/62.07 [213]P23(x2132)+~P1(x2132)+~P14(x2132)+~P22(x2132)+~P2(x2132)+~P16(f22(x2132,x2131),x2132,x2132)+~P8(x2131,f30(x2132),f30(x2132))+~P13(f22(x2132,x2131),f30(x2132),f30(x2132))+~P9(f22(x2132,x2131),f30(x2132),f30(x2132))+E(x2131,f28(x2132))+P12(f21(x2132,x2131))+~P12(f22(x2132,x2131)) % 61.99/62.07 [216]P23(x2162)+~P1(x2162)+~P14(x2162)+~P22(x2162)+~P2(x2162)+P16(f21(x2162,x2161),x2162,x2162)+~P16(f22(x2162,x2161),x2162,x2162)+~P8(x2161,f30(x2162),f30(x2162))+~P13(f22(x2162,x2161),f30(x2162),f30(x2162))+~P9(f22(x2162,x2161),f30(x2162),f30(x2162))+E(x2161,f28(x2162))+~P12(f22(x2162,x2161)) % 61.99/62.07 [217]P23(x2172)+~P1(x2172)+~P14(x2172)+~P22(x2172)+~P2(x2172)+P13(f21(x2172,x2171),f30(x2172),f30(x2172))+~P16(f22(x2172,x2171),x2172,x2172)+~P8(x2171,f30(x2172),f30(x2172))+~P13(f22(x2172,x2171),f30(x2172),f30(x2172))+~P9(f22(x2172,x2171),f30(x2172),f30(x2172))+E(x2171,f28(x2172))+~P12(f22(x2172,x2171)) % 61.99/62.07 [218]P23(x2182)+~P1(x2182)+~P14(x2182)+~P22(x2182)+~P2(x2182)+P9(f21(x2182,x2181),f30(x2182),f30(x2182))+~P16(f22(x2182,x2181),x2182,x2182)+~P8(x2181,f30(x2182),f30(x2182))+~P13(f22(x2182,x2181),f30(x2182),f30(x2182))+~P9(f22(x2182,x2181),f30(x2182),f30(x2182))+E(x2181,f28(x2182))+~P12(f22(x2182,x2181)) % 61.99/62.07 [215]P23(x2152)+~P1(x2152)+~P14(x2152)+~P22(x2152)+~P2(x2152)+~P16(f22(x2152,x2151),x2152,x2152)+~P8(x2151,f30(x2152),f30(x2152))+~P13(f22(x2152,x2151),f30(x2152),f30(x2152))+~P9(f22(x2152,x2151),f30(x2152),f30(x2152))+P11(f21(x2152,x2151),x2151)+E(x2151,f28(x2152))+P20(f21(x2152,x2151))+~P12(f22(x2152,x2151)) % 61.99/62.07 [219]P23(x2192)+~P1(x2192)+~P14(x2192)+~P22(x2192)+~P2(x2192)+P24(f21(x2192,x2191),x2192,x2192)+~P16(f22(x2192,x2191),x2192,x2192)+~P8(x2191,f30(x2192),f30(x2192))+~P13(f22(x2192,x2191),f30(x2192),f30(x2192))+~P9(f22(x2192,x2191),f30(x2192),f30(x2192))+P11(f21(x2192,x2191),x2191)+E(x2191,f28(x2192))+~P12(f22(x2192,x2191)) % 61.99/62.07 [191]~P1(x1911)+~P14(x1911)+~P22(x1911)+~P2(x1911)+~P12(x1912)+~P11(x1912,x1913)+~P16(x1912,x1911,x1911)+P23(x1911)+P20(x1912)+~P13(x1912,f30(x1911),f30(x1911))+~P9(x1912,f30(x1911),f30(x1911))+~P8(x1913,f30(x1911),f30(x1911))+~E(x1913,f28(x1911)) % 61.99/62.07 [203]~P1(x2031)+~P14(x2031)+~P22(x2031)+~P2(x2031)+~P12(x2032)+~P11(x2032,x2033)+~P16(x2032,x2031,x2031)+P24(x2032,x2031,x2031)+P23(x2031)+~P13(x2032,f30(x2031),f30(x2031))+~P9(x2032,f30(x2031),f30(x2031))+~P8(x2033,f30(x2031),f30(x2031))+~E(x2033,f28(x2031)) % 61.99/62.07 [221]P23(x2212)+~P1(x2212)+~P14(x2212)+~P22(x2212)+~P2(x2212)+~P16(f22(x2212,x2211),x2212,x2212)+~P24(f21(x2212,x2211),x2212,x2212)+~P8(x2211,f30(x2212),f30(x2212))+~P13(f22(x2212,x2211),f30(x2212),f30(x2212))+~P9(f22(x2212,x2211),f30(x2212),f30(x2212))+~P11(f21(x2212,x2211),x2211)+E(x2211,f28(x2212))+~P12(f22(x2212,x2211))+~P20(f21(x2212,x2211)) % 61.99/62.07 [184]~P14(x1841)+~P14(x1842)+~P22(x1841)+~P22(x1842)+~P2(x1841)+~P2(x1842)+~P12(x1843)+~P20(x1843)+~P16(x1843,x1842,x1841)+P23(x1841)+P21(x1843,x1842,x1841)+P23(x1842)+~P13(x1843,f30(x1842),f30(x1841))+~P9(x1843,f30(x1842),f30(x1841)) % 61.99/62.07 [188]~P14(x1881)+~P14(x1882)+~P22(x1881)+~P22(x1882)+~P2(x1881)+~P2(x1882)+~P12(x1883)+~P16(x1883,x1882,x1881)+~P21(x1883,x1882,x1881)+P23(x1881)+P23(x1882)+P20(x1883)+~P13(x1883,f30(x1882),f30(x1881))+~P9(x1883,f30(x1882),f30(x1881)) % 61.99/62.07 [194]~P14(x1941)+~P14(x1942)+~P22(x1941)+~P22(x1942)+~P2(x1941)+~P2(x1942)+~P12(x1943)+~P16(x1943,x1942,x1941)+~P25(x1943,x1942,x1941)+P23(x1941)+P21(x1943,x1942,x1941)+P23(x1942)+~P13(x1943,f30(x1942),f30(x1941))+~P9(x1943,f30(x1942),f30(x1941)) % 61.99/62.07 [195]~P14(x1951)+~P14(x1952)+~P22(x1951)+~P22(x1952)+~P2(x1951)+~P2(x1952)+~P12(x1953)+~P16(x1953,x1952,x1951)+~P25(x1953,x1952,x1951)+P23(x1951)+P24(x1953,x1952,x1951)+P23(x1952)+~P13(x1953,f30(x1952),f30(x1951))+~P9(x1953,f30(x1952),f30(x1951)) % 61.99/62.07 [207]~P1(x2071)+~P14(x2071)+~P22(x2071)+~P2(x2071)+~P12(x2072)+~P20(x2072)+~P16(x2072,x2071,x2071)+~P24(x2072,x2071,x2071)+P23(x2071)+P11(x2072,x2073)+~P13(x2072,f30(x2071),f30(x2071))+~P9(x2072,f30(x2071),f30(x2071))+~P8(x2073,f30(x2071),f30(x2071))+~E(x2073,f28(x2071)) % 61.99/62.07 [209]~P14(x2091)+~P14(x2092)+~P22(x2091)+~P22(x2092)+~P2(x2091)+~P2(x2092)+~P12(x2093)+~P16(x2093,x2092,x2091)+~P21(x2093,x2092,x2091)+~P24(x2093,x2092,x2091)+P23(x2091)+P25(x2093,x2092,x2091)+P23(x2092)+~P13(x2093,f30(x2092),f30(x2091))+~P9(x2093,f30(x2092),f30(x2091)) % 61.99/62.07 [220]~P25(x2204,x2201,x2202)+~P14(x2201)+~P14(x2202)+~P22(x2201)+~P22(x2202)+~P2(x2201)+~P2(x2202)+~P12(x2203)+~P12(x2204)+~P16(x2203,x2202,x2201)+~P16(x2204,x2201,x2202)+P23(x2201)+P25(x2203,x2202,x2201)+P23(x2202)+~P13(x2203,f30(x2202),f30(x2201))+~P13(x2204,f30(x2201),f30(x2202))+~P9(x2203,f30(x2202),f30(x2201))+~P9(x2204,f30(x2201),f30(x2202))+~E(x2203,f31(x2204)) % 61.99/62.07 %EqnAxiom % 61.99/62.07 [1]E(x11,x11) % 61.99/62.07 [2]E(x22,x21)+~E(x21,x22) % 61.99/62.07 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 61.99/62.07 [4]~E(x41,x42)+E(f25(x41),f25(x42)) % 61.99/62.07 [5]~E(x51,x52)+E(f7(x51,x53),f7(x52,x53)) % 61.99/62.07 [6]~E(x61,x62)+E(f7(x63,x61),f7(x63,x62)) % 61.99/62.07 [7]~E(x71,x72)+E(f14(x71,x73),f14(x72,x73)) % 61.99/62.07 [8]~E(x81,x82)+E(f14(x83,x81),f14(x83,x82)) % 61.99/62.07 [9]~E(x91,x92)+E(f30(x91),f30(x92)) % 61.99/62.07 [10]~E(x101,x102)+E(f22(x101,x103),f22(x102,x103)) % 61.99/62.07 [11]~E(x111,x112)+E(f22(x113,x111),f22(x113,x112)) % 61.99/62.07 [12]~E(x121,x122)+E(f26(x121,x123),f26(x122,x123)) % 61.99/62.07 [13]~E(x131,x132)+E(f26(x133,x131),f26(x133,x132)) % 61.99/62.07 [14]~E(x141,x142)+E(f21(x141,x143),f21(x142,x143)) % 61.99/62.07 [15]~E(x151,x152)+E(f21(x153,x151),f21(x153,x152)) % 61.99/62.07 [16]~E(x161,x162)+E(f28(x161),f28(x162)) % 61.99/62.07 [17]~E(x171,x172)+E(f5(x171,x173,x174),f5(x172,x173,x174)) % 61.99/62.07 [18]~E(x181,x182)+E(f5(x183,x181,x184),f5(x183,x182,x184)) % 61.99/62.07 [19]~E(x191,x192)+E(f5(x193,x194,x191),f5(x193,x194,x192)) % 61.99/62.07 [20]~E(x201,x202)+E(f4(x201,x203),f4(x202,x203)) % 61.99/62.07 [21]~E(x211,x212)+E(f4(x213,x211),f4(x213,x212)) % 61.99/62.07 [22]~E(x221,x222)+E(f27(x221,x223),f27(x222,x223)) % 61.99/62.07 [23]~E(x231,x232)+E(f27(x233,x231),f27(x233,x232)) % 61.99/62.07 [24]~E(x241,x242)+E(f34(x241,x243),f34(x242,x243)) % 61.99/62.07 [25]~E(x251,x252)+E(f34(x253,x251),f34(x253,x252)) % 61.99/62.07 [26]~E(x261,x262)+E(f29(x261,x263),f29(x262,x263)) % 61.99/62.07 [27]~E(x271,x272)+E(f29(x273,x271),f29(x273,x272)) % 61.99/62.07 [28]~E(x281,x282)+E(f15(x281,x283),f15(x282,x283)) % 61.99/62.07 [29]~E(x291,x292)+E(f15(x293,x291),f15(x293,x292)) % 61.99/62.07 [30]~E(x301,x302)+E(f31(x301),f31(x302)) % 61.99/62.07 [31]~E(x311,x312)+E(f32(x311),f32(x312)) % 61.99/62.07 [32]~E(x321,x322)+E(f20(x321),f20(x322)) % 61.99/62.07 [33]~E(x331,x332)+E(f33(x331),f33(x332)) % 61.99/62.07 [34]~P1(x341)+P1(x342)+~E(x341,x342) % 61.99/62.07 [35]P9(x352,x353,x354)+~E(x351,x352)+~P9(x351,x353,x354) % 61.99/62.07 [36]P9(x363,x362,x364)+~E(x361,x362)+~P9(x363,x361,x364) % 61.99/62.07 [37]P9(x373,x374,x372)+~E(x371,x372)+~P9(x373,x374,x371) % 61.99/62.07 [38]P13(x382,x383,x384)+~E(x381,x382)+~P13(x381,x383,x384) % 61.99/62.07 [39]P13(x393,x392,x394)+~E(x391,x392)+~P13(x393,x391,x394) % 61.99/62.07 [40]P13(x403,x404,x402)+~E(x401,x402)+~P13(x403,x404,x401) % 61.99/62.07 [41]P8(x412,x413,x414)+~E(x411,x412)+~P8(x411,x413,x414) % 61.99/62.07 [42]P8(x423,x422,x424)+~E(x421,x422)+~P8(x423,x421,x424) % 61.99/62.07 [43]P8(x433,x434,x432)+~E(x431,x432)+~P8(x433,x434,x431) % 61.99/62.07 [44]~P14(x441)+P14(x442)+~E(x441,x442) % 61.99/62.07 [45]~P22(x451)+P22(x452)+~E(x451,x452) % 61.99/62.07 [46]~P2(x461)+P2(x462)+~E(x461,x462) % 61.99/62.07 [47]~P18(x471)+P18(x472)+~E(x471,x472) % 61.99/62.07 [48]P10(x482,x483,x484,x485)+~E(x481,x482)+~P10(x481,x483,x484,x485) % 61.99/62.07 [49]P10(x493,x492,x494,x495)+~E(x491,x492)+~P10(x493,x491,x494,x495) % 61.99/62.07 [50]P10(x503,x504,x502,x505)+~E(x501,x502)+~P10(x503,x504,x501,x505) % 61.99/62.07 [51]P10(x513,x514,x515,x512)+~E(x511,x512)+~P10(x513,x514,x515,x511) % 61.99/62.07 [52]P16(x522,x523,x524)+~E(x521,x522)+~P16(x521,x523,x524) % 61.99/62.07 [53]P16(x533,x532,x534)+~E(x531,x532)+~P16(x533,x531,x534) % 61.99/62.07 [54]P16(x543,x544,x542)+~E(x541,x542)+~P16(x543,x544,x541) % 61.99/62.07 [55]~P23(x551)+P23(x552)+~E(x551,x552) % 61.99/62.07 [56]~P20(x561)+P20(x562)+~E(x561,x562) % 61.99/62.07 [57]P24(x572,x573,x574)+~E(x571,x572)+~P24(x571,x573,x574) % 61.99/62.07 [58]P24(x583,x582,x584)+~E(x581,x582)+~P24(x583,x581,x584) % 61.99/62.07 [59]P24(x593,x594,x592)+~E(x591,x592)+~P24(x593,x594,x591) % 61.99/62.07 [60]~P3(x601)+P3(x602)+~E(x601,x602) % 61.99/62.07 [61]~P15(x611)+P15(x612)+~E(x611,x612) % 61.99/62.07 [62]P21(x622,x623,x624)+~E(x621,x622)+~P21(x621,x623,x624) % 61.99/62.07 [63]P21(x633,x632,x634)+~E(x631,x632)+~P21(x633,x631,x634) % 61.99/62.07 [64]P21(x643,x644,x642)+~E(x641,x642)+~P21(x643,x644,x641) % 61.99/62.07 [65]P6(x652,x653)+~E(x651,x652)+~P6(x651,x653) % 61.99/62.07 [66]P6(x663,x662)+~E(x661,x662)+~P6(x663,x661) % 61.99/62.07 [67]~P12(x671)+P12(x672)+~E(x671,x672) % 61.99/62.07 [68]P25(x682,x683,x684)+~E(x681,x682)+~P25(x681,x683,x684) % 61.99/62.07 [69]P25(x693,x692,x694)+~E(x691,x692)+~P25(x693,x691,x694) % 61.99/62.07 [70]P25(x703,x704,x702)+~E(x701,x702)+~P25(x703,x704,x701) % 61.99/62.07 [71]P17(x712,x713,x714)+~E(x711,x712)+~P17(x711,x713,x714) % 61.99/62.07 [72]P17(x723,x722,x724)+~E(x721,x722)+~P17(x723,x721,x724) % 61.99/62.07 [73]P17(x733,x734,x732)+~E(x731,x732)+~P17(x733,x734,x731) % 61.99/62.07 [74]P11(x742,x743)+~E(x741,x742)+~P11(x741,x743) % 61.99/62.07 [75]P11(x753,x752)+~E(x751,x752)+~P11(x753,x751) % 61.99/62.07 [76]P7(x762,x763,x764)+~E(x761,x762)+~P7(x761,x763,x764) % 61.99/62.07 [77]P7(x773,x772,x774)+~E(x771,x772)+~P7(x773,x771,x774) % 61.99/62.07 [78]P7(x783,x784,x782)+~E(x781,x782)+~P7(x783,x784,x781) % 61.99/62.07 [79]~P4(x791)+P4(x792)+~E(x791,x792) % 61.99/62.07 [80]~P19(x801)+P19(x802)+~E(x801,x802) % 61.99/62.07 [81]P5(x812,x813)+~E(x811,x812)+~P5(x811,x813) % 61.99/62.07 [82]P5(x823,x822)+~E(x821,x822)+~P5(x823,x821) % 61.99/62.07 % 61.99/62.07 %------------------------------------------- % 61.99/62.07 cnf(227,plain, % 61.99/62.07 (~P14(x2271)+~P22(x2271)+~P2(x2271)+P23(x2271)+~P1(x2271)+P12(x2272)+~P10(x2272,f30(x2271),f30(x2271),f28(x2271))+~P8(f28(x2271),f30(x2271),f30(x2271))), % 61.99/62.07 inference(equality_inference,[],[208])). % 61.99/62.07 cnf(228,plain, % 61.99/62.07 (~P14(x2281)+~P22(x2281)+~P2(x2281)+P23(x2281)+P16(x2282,x2281,x2281)+~P1(x2281)+~P10(x2282,f30(x2281),f30(x2281),f28(x2281))+~P8(f28(x2281),f30(x2281),f30(x2281))), % 61.99/62.07 inference(equality_inference,[],[210])). % 61.99/62.07 cnf(229,plain, % 61.99/62.07 (~P14(x2291)+~P22(x2291)+~P2(x2291)+P23(x2291)+~P1(x2291)+~P10(x2292,f30(x2291),f30(x2291),f28(x2291))+~P8(f28(x2291),f30(x2291),f30(x2291))+P13(x2292,f30(x2291),f30(x2291))), % 61.99/62.07 inference(equality_inference,[],[211])). % 61.99/62.07 cnf(230,plain, % 61.99/62.07 (~P14(x2301)+~P22(x2301)+~P2(x2301)+P23(x2301)+~P1(x2301)+~P10(x2302,f30(x2301),f30(x2301),f28(x2301))+~P8(f28(x2301),f30(x2301),f30(x2301))+P9(x2302,f30(x2301),f30(x2301))), % 61.99/62.07 inference(equality_inference,[],[212])). % 61.99/62.07 cnf(231,plain, % 61.99/62.07 (~P14(x2311)+~P14(x2312)+~P22(x2311)+~P22(x2312)+~P2(x2311)+~P2(x2312)+~P12(x2313)+~P16(f31(x2313),x2312,x2311)+~P16(x2313,x2311,x2312)+P23(x2311)+P25(f31(x2313),x2312,x2311)+P23(x2312)+~P25(x2313,x2311,x2312)+~P12(f31(x2313))+~P13(f31(x2313),f30(x2312),f30(x2311))+~P13(x2313,f30(x2311),f30(x2312))+~P9(f31(x2313),f30(x2312),f30(x2311))+~P9(x2313,f30(x2311),f30(x2312))), % 61.99/62.07 inference(equality_inference,[],[220])). % 61.99/62.07 cnf(232,plain, % 61.99/62.07 (~P11(x2321,a23)), % 61.99/62.07 inference(scs_inference,[],[105,145])). % 61.99/62.07 cnf(235,plain, % 61.99/62.07 (P6(f25(x2351),x2351)), % 61.99/62.07 inference(rename_variables,[],[115])). % 61.99/62.07 cnf(237,plain, % 61.99/62.07 (~P8(a23,x2371,x2372)), % 61.99/62.07 inference(scs_inference,[],[115,105,145,153,160])). % 61.99/62.07 cnf(241,plain, % 61.99/62.07 (P8(f27(x2411,x2412),x2411,x2412)), % 61.99/62.07 inference(rename_variables,[],[125])). % 61.99/62.07 cnf(242,plain, % 61.99/62.07 (~P18(f27(x2421,x2422))), % 61.99/62.07 inference(scs_inference,[],[133,126,125,115,105,145,153,160,48,41,137])). % 61.99/62.07 cnf(244,plain, % 61.99/62.07 (P11(f25(a3),a3)), % 61.99/62.07 inference(scs_inference,[],[133,126,125,115,235,105,131,145,153,160,48,41,137,149])). % 61.99/62.07 cnf(245,plain, % 61.99/62.07 (P6(f25(x2451),x2451)), % 61.99/62.07 inference(rename_variables,[],[115])). % 61.99/62.07 cnf(247,plain, % 61.99/62.07 (~P11(x2471,f25(f32(a23)))), % 61.99/62.07 inference(scs_inference,[],[133,126,125,115,235,245,105,131,145,153,160,48,41,137,149,155])). % 61.99/62.07 cnf(248,plain, % 61.99/62.07 (P6(f25(x2481),x2481)), % 61.99/62.07 inference(rename_variables,[],[115])). % 61.99/62.07 cnf(252,plain, % 61.99/62.07 (P10(f25(f27(x2521,a3)),x2521,a3,f27(x2521,a3))), % 61.99/62.07 inference(scs_inference,[],[133,126,87,91,127,125,241,115,235,245,248,105,131,145,153,160,48,41,137,149,155,139,183])). % 61.99/62.07 cnf(254,plain, % 61.99/62.07 (P8(f27(x2541,x2542),x2541,x2542)), % 61.99/62.07 inference(rename_variables,[],[125])). % 61.99/62.07 cnf(256,plain, % 61.99/62.07 (P13(f25(f27(x2561,a3)),x2561,a3)), % 61.99/62.07 inference(scs_inference,[],[133,126,87,91,127,125,241,254,115,235,245,248,105,131,145,153,160,48,41,137,149,155,139,183,204])). % 61.99/62.07 cnf(257,plain, % 61.99/62.07 (P8(f27(x2571,x2572),x2571,x2572)), % 61.99/62.07 inference(rename_variables,[],[125])). % 61.99/62.07 cnf(259,plain, % 61.99/62.07 (P9(f25(f27(x2591,a3)),x2591,a3)), % 61.99/62.07 inference(scs_inference,[],[133,126,87,91,127,125,241,254,257,115,235,245,248,105,131,145,153,160,48,41,137,149,155,139,183,204,205])). % 61.99/62.07 cnf(262,plain, % 61.99/62.07 (P20(a10)), % 61.99/62.07 inference(scs_inference,[],[133,126,87,91,127,125,241,254,257,115,235,245,248,99,103,105,108,131,145,153,160,48,41,137,149,155,139,183,204,205,142])). % 61.99/62.07 cnf(264,plain, % 61.99/62.07 (P17(f7(x2641,a3),x2641,a3)), % 61.99/62.07 inference(scs_inference,[],[133,126,87,91,127,121,123,125,241,254,257,115,235,245,248,99,103,105,108,131,118,145,153,160,48,41,137,149,155,139,183,204,205,142,175])). % 61.99/62.07 cnf(265,plain, % 61.99/62.07 (P13(f7(x2651,x2652),x2651,x2652)), % 61.99/62.07 inference(rename_variables,[],[123])). % 61.99/62.07 cnf(266,plain, % 61.99/62.07 (P12(f7(x2661,x2662))), % 61.99/62.07 inference(rename_variables,[],[118])). % 61.99/62.07 cnf(267,plain, % 61.99/62.07 (P7(f7(x2671,x2672),x2671,x2672)), % 61.99/62.07 inference(rename_variables,[],[121])). % 61.99/62.07 cnf(269,plain, % 61.99/62.07 (~P18(f7(a3,a3))), % 61.99/62.07 inference(scs_inference,[],[133,126,87,91,127,121,267,123,265,125,241,254,257,115,235,245,248,99,103,105,108,131,118,266,145,153,160,48,41,137,149,155,139,183,204,205,142,175,173])). % 61.99/62.07 cnf(277,plain, % 61.99/62.07 (~E(a3,a23)), % 61.99/62.07 inference(scs_inference,[],[133,126,87,91,127,121,267,123,265,125,241,254,257,115,235,245,248,99,103,105,108,131,118,266,145,153,160,48,41,137,149,155,139,183,204,205,142,175,173,152,49,75])). % 61.99/62.07 cnf(281,plain, % 61.99/62.07 (P9(f4(x2811,x2812),x2813,x2812)+~E(x2811,x2813)), % 61.99/62.07 inference(scs_inference,[],[133,126,87,91,127,121,267,123,265,124,125,241,254,257,115,235,245,248,99,103,105,108,131,118,266,145,153,160,48,41,137,149,155,139,183,204,205,142,175,173,152,49,75,50,51,35,36])). % 61.99/62.07 cnf(282,plain, % 61.99/62.07 (P9(f4(x2821,x2822),x2821,x2823)+~E(x2822,x2823)), % 61.99/62.07 inference(scs_inference,[],[133,126,87,91,127,121,267,123,265,124,125,241,254,257,115,235,245,248,99,103,105,108,131,118,266,145,153,160,48,41,137,149,155,139,183,204,205,142,175,173,152,49,75,50,51,35,36,37])). % 61.99/62.07 cnf(289,plain, % 61.99/62.07 (~P8(a9,x2891,x2892)), % 61.99/62.07 inference(scs_inference,[],[106,160])). % 61.99/62.07 cnf(291,plain, % 61.99/62.07 (~P11(x2911,a9)), % 61.99/62.07 inference(scs_inference,[],[106,160,145])). % 61.99/62.07 cnf(293,plain, % 61.99/62.07 (P11(f25(f27(x2931,x2932)),f27(x2931,x2932))), % 61.99/62.07 inference(scs_inference,[],[242,106,115,160,145,149])). % 61.99/62.07 cnf(294,plain, % 61.99/62.07 (P6(f25(x2941),x2941)), % 61.99/62.07 inference(rename_variables,[],[115])). % 61.99/62.07 cnf(296,plain, % 61.99/62.07 (~P11(x2961,f25(f32(a9)))), % 61.99/62.07 inference(scs_inference,[],[242,106,115,294,160,145,149,155])). % 61.99/62.07 cnf(297,plain, % 61.99/62.07 (P6(f25(x2971),x2971)), % 61.99/62.07 inference(rename_variables,[],[115])). % 61.99/62.07 cnf(301,plain, % 61.99/62.07 (P10(f25(f27(x3011,a16)),x3011,a16,f27(x3011,a16))), % 61.99/62.07 inference(scs_inference,[],[242,247,244,106,132,125,115,294,297,160,145,149,155,75,183])). % 61.99/62.07 cnf(302,plain, % 61.99/62.07 (P6(f25(x3021),x3021)), % 61.99/62.07 inference(rename_variables,[],[115])). % 61.99/62.07 cnf(303,plain, % 61.99/62.07 (P8(f27(x3031,x3032),x3031,x3032)), % 61.99/62.07 inference(rename_variables,[],[125])). % 61.99/62.07 cnf(305,plain, % 61.99/62.07 (P9(f25(f27(x3051,a16)),x3051,a16)), % 61.99/62.07 inference(scs_inference,[],[242,247,244,106,132,125,303,115,294,297,160,145,149,155,75,183,205])). % 61.99/62.07 cnf(306,plain, % 61.99/62.07 (P8(f27(x3061,x3062),x3061,x3062)), % 61.99/62.07 inference(rename_variables,[],[125])). % 61.99/62.07 cnf(308,plain, % 61.99/62.07 (P13(f25(f27(x3081,a16)),x3081,a16)), % 61.99/62.07 inference(scs_inference,[],[242,247,244,106,132,125,303,306,115,294,297,160,145,149,155,75,183,205,204])). % 61.99/62.07 cnf(309,plain, % 61.99/62.07 (P8(f27(x3091,x3092),x3091,x3092)), % 61.99/62.07 inference(rename_variables,[],[125])). % 61.99/62.07 cnf(311,plain, % 61.99/62.07 (~P11(f27(x3111,x3112),f25(f27(x3111,x3112)))), % 61.99/62.07 inference(scs_inference,[],[242,247,244,106,132,125,303,306,115,294,297,160,145,149,155,75,183,205,204,152])). % 61.99/62.07 cnf(314,plain, % 61.99/62.07 (P13(f25(f27(x3141,a3)),x3142,a3)+~E(x3141,x3142)), % 61.99/62.07 inference(scs_inference,[],[256,242,247,244,106,132,125,303,306,115,294,297,160,145,149,155,75,183,205,204,152,38,39])). % 61.99/62.07 cnf(316,plain, % 61.99/62.07 (P8(f27(x3161,x3162),x3163,x3162)+~E(x3161,x3163)), % 61.99/62.07 inference(scs_inference,[],[256,242,247,244,106,132,125,303,306,309,115,294,297,160,145,149,155,75,183,205,204,152,38,39,40,42])). % 61.99/62.07 cnf(317,plain, % 61.99/62.07 (P8(f27(x3171,x3172),x3171,x3173)+~E(x3172,x3173)), % 61.99/62.07 inference(scs_inference,[],[256,242,247,244,106,132,125,303,306,309,115,294,297,160,145,149,155,75,183,205,204,152,38,39,40,42,43])). % 61.99/62.07 cnf(318,plain, % 61.99/62.07 (P6(x3181,x3182)+~E(f25(x3182),x3181)), % 61.99/62.07 inference(scs_inference,[],[256,242,247,244,106,132,125,303,306,309,115,294,297,302,160,145,149,155,75,183,205,204,152,38,39,40,42,43,65])). % 61.99/62.07 cnf(327,plain, % 61.99/62.07 (~P11(x3271,a11)), % 61.99/62.07 inference(scs_inference,[],[107,160,145])). % 61.99/62.07 cnf(329,plain, % 61.99/62.07 (P11(f25(a16),a16)), % 61.99/62.07 inference(scs_inference,[],[132,107,115,160,145,149])). % 61.99/62.07 cnf(330,plain, % 61.99/62.07 (P6(f25(x3301),x3301)), % 61.99/62.07 inference(rename_variables,[],[115])). % 61.99/62.07 cnf(332,plain, % 61.99/62.07 (~P11(x3321,f25(f32(a11)))), % 61.99/62.07 inference(scs_inference,[],[132,107,115,330,160,145,149,155])). % 61.99/62.07 cnf(333,plain, % 61.99/62.07 (P6(f25(x3331),x3331)), % 61.99/62.07 inference(rename_variables,[],[115])). % 61.99/62.07 cnf(339,plain, % 61.99/62.07 (P6(f25(x3391),x3392)+~E(x3391,x3392)), % 61.99/62.07 inference(scs_inference,[],[132,293,296,107,115,330,333,160,145,149,155,75,152,66])). % 61.99/62.07 cnf(350,plain, % 61.99/62.07 (~P11(x3501,a10)), % 61.99/62.07 inference(scs_inference,[],[108,160,145])). % 61.99/62.07 cnf(352,plain, % 61.99/62.07 (P11(f25(f7(a3,a3)),f7(a3,a3))), % 61.99/62.07 inference(scs_inference,[],[269,108,115,160,145,149])). % 61.99/62.07 cnf(353,plain, % 61.99/62.07 (P6(f25(x3531),x3531)), % 61.99/62.07 inference(rename_variables,[],[115])). % 61.99/62.07 cnf(355,plain, % 61.99/62.07 (~P11(x3551,f25(f32(a10)))), % 61.99/62.07 inference(scs_inference,[],[269,108,115,353,160,145,149,155])). % 61.99/62.07 cnf(362,plain, % 61.99/62.07 (P7(f14(x3621,x3622),x3623,x3622)+~E(x3621,x3623)), % 61.99/62.07 inference(scs_inference,[],[332,122,269,329,108,115,353,160,145,149,155,75,152,77])). % 61.99/62.07 cnf(363,plain, % 61.99/62.07 (P7(f14(x3631,x3632),x3631,x3633)+~E(x3632,x3633)), % 61.99/62.07 inference(scs_inference,[],[332,122,269,329,108,115,353,160,145,149,155,75,152,77,78])). % 61.99/62.07 cnf(364,plain, % 61.99/62.07 (P5(x3641,x3642)+~E(x3642,x3641)), % 61.99/62.07 inference(scs_inference,[],[114,332,122,269,329,108,115,353,160,145,149,155,75,152,77,78,81])). % 61.99/62.07 cnf(365,plain, % 61.99/62.07 (P5(x3651,x3652)+~E(x3651,x3652)), % 61.99/62.07 inference(scs_inference,[],[114,332,122,269,329,108,115,353,160,145,149,155,75,152,77,78,81,82])). % 61.99/62.07 cnf(380,plain, % 61.99/62.07 (~P9(a9,a3,a16)+~E(f25(f27(a3,a16)),a9)), % 61.99/62.07 inference(scs_inference,[],[308,131,132,102,352,355,106,75,38,173,167])). % 61.99/62.07 cnf(389,plain, % 61.99/62.07 (P7(f26(x3891,x3892),x3893,x3892)+~E(x3891,x3893)), % 61.99/62.07 inference(scs_inference,[],[264,352,232,120,75,73,77])). % 61.99/62.07 cnf(392,plain, % 61.99/62.07 (P9(f25(f27(x3921,a3)),x3922,a3)+~E(x3921,x3922)), % 61.99/62.07 inference(scs_inference,[],[259,264,352,232,120,75,73,77,37,74,36])). % 61.99/62.08 cnf(403,plain, % 61.99/62.08 (~E(f25(f27(a3,a16)),a9)), % 61.99/62.08 inference(scs_inference,[],[305,244,291,75,35,380])). % 61.99/62.08 cnf(415,plain, % 61.99/62.08 (P7(f7(x4151,x4152),x4151,x4153)+~E(x4152,x4153)), % 61.99/62.08 inference(scs_inference,[],[403,106,329,311,327,121,137,149,75,78])). % 61.99/62.08 cnf(416,plain, % 61.99/62.08 (P13(f25(f27(x4161,a16)),x4162,a16)+~E(x4161,x4162)), % 61.99/62.08 inference(scs_inference,[],[308,403,106,329,311,327,121,137,149,75,78,39])). % 61.99/62.08 cnf(417,plain, % 61.99/62.08 (P17(f7(x4171,a3),x4172,a3)+~E(x4171,x4172)), % 61.99/62.08 inference(scs_inference,[],[308,403,106,264,329,311,327,121,137,149,75,78,39,72])). % 61.99/62.08 cnf(418,plain, % 61.99/62.08 (P10(f25(f27(x4181,a3)),x4182,a3,f27(x4181,a3))+~E(x4181,x4182)), % 61.99/62.08 inference(scs_inference,[],[252,308,403,106,264,329,311,327,121,137,149,75,78,39,72,49])). % 61.99/62.08 cnf(429,plain, % 61.99/62.08 (P10(f25(f27(x4291,a16)),x4291,a16,x4292)+~E(f27(x4291,a16),x4292)), % 61.99/62.08 inference(scs_inference,[],[301,293,350,75,51])). % 61.99/62.08 cnf(430,plain, % 61.99/62.08 (P17(x4301,x4302,a3)+~E(f7(x4302,a3),x4301)), % 61.99/62.08 inference(scs_inference,[],[301,264,293,350,75,51,71])). % 61.99/62.08 cnf(443,plain, % 61.99/62.08 (P9(f25(f27(x4431,a16)),x4432,a16)+~E(x4431,x4432)), % 61.99/62.08 inference(scs_inference,[],[305,329,247,75,36])). % 61.99/62.08 cnf(445,plain, % 61.99/62.08 (P13(f7(x4451,x4452),x4453,x4452)+~E(x4451,x4453)), % 61.99/62.08 inference(scs_inference,[],[305,123,329,247,75,36,38,39])). % 61.99/62.08 cnf(446,plain, % 61.99/62.08 (P7(f7(x4461,x4462),x4463,x4462)+~E(x4461,x4463)), % 61.99/62.08 inference(scs_inference,[],[305,123,329,247,121,75,36,38,39,77])). % 61.99/62.08 cnf(447,plain, % 61.99/62.08 (P10(f25(f27(x4471,a16)),x4472,a16,f27(x4471,a16))+~E(x4471,x4472)), % 61.99/62.08 inference(scs_inference,[],[301,305,123,329,247,121,75,36,38,39,77,49])). % 61.99/62.08 cnf(460,plain, % 61.99/62.08 (P7(f26(x4601,x4602),x4601,x4603)+~E(x4602,x4603)), % 61.99/62.08 inference(scs_inference,[],[308,305,301,244,120,296,75,40,37,50,78])). % 61.99/62.08 cnf(471,plain, % 61.99/62.08 (P10(f25(f27(x4711,a3)),x4711,a3,x4712)+~E(f27(x4711,a3),x4712)), % 61.99/62.08 inference(scs_inference,[],[252,352,332,75,51])). % 61.99/62.08 cnf(476,plain, % 61.99/62.08 (P13(f7(x4761,x4762),x4761,x4763)+~E(x4762,x4763)), % 61.99/62.08 inference(scs_inference,[],[123,329,355,75,40])). % 61.99/62.08 cnf(556,plain, % 61.99/62.08 (~P8(f28(a1),f30(a1),f30(a1))+P12(a19)), % 61.99/62.08 inference(scs_inference,[],[83,126,87,89,91,127,227])). % 61.99/62.08 cnf(584,plain, % 61.99/62.08 (~P18(f30(a1))), % 61.99/62.08 inference(scs_inference,[],[91,127,136,143])). % 61.99/62.08 cnf(585,plain, % 61.99/62.08 (P11(f25(f30(a1)),f30(a1))), % 61.99/62.08 inference(scs_inference,[],[584,115,149])). % 61.99/62.08 cnf(590,plain, % 61.99/62.08 (P17(f7(x5901,f30(a1)),x5901,f30(a1))), % 61.99/62.08 inference(scs_inference,[],[584,123,121,115,118,232,149,75,175])). % 61.99/62.08 cnf(591,plain, % 61.99/62.08 (P13(f7(x5911,x5912),x5911,x5912)), % 61.99/62.08 inference(rename_variables,[],[123])). % 61.99/62.08 cnf(592,plain, % 61.99/62.08 (P12(f7(x5921,x5922))), % 61.99/62.08 inference(rename_variables,[],[118])). % 61.99/62.08 cnf(593,plain, % 61.99/62.08 (P7(f7(x5931,x5932),x5931,x5932)), % 61.99/62.08 inference(rename_variables,[],[121])). % 61.99/62.08 cnf(595,plain, % 61.99/62.08 (~P18(f7(f30(a1),f30(a1)))), % 61.99/62.08 inference(scs_inference,[],[584,123,591,121,593,115,118,592,232,149,75,175,173])). % 61.99/62.08 cnf(602,plain, % 61.99/62.08 (P17(f7(x6021,f30(a1)),x6022,f30(a1))+~E(x6021,x6022)), % 61.99/62.08 inference(scs_inference,[],[584,123,591,121,593,115,118,592,232,149,75,175,173,152,72])). % 61.99/62.08 cnf(603,plain, % 61.99/62.08 (P17(x6031,x6032,f30(a1))+~E(f7(x6032,f30(a1)),x6031)), % 61.99/62.08 inference(scs_inference,[],[584,123,591,121,593,115,118,592,232,149,75,175,173,152,72,71])). % 61.99/62.08 cnf(614,plain, % 61.99/62.08 (~P6(f31(a19),f28(a1))+~P8(f28(a1),f30(a1),f30(a1))), % 61.99/62.08 inference(scs_inference,[],[133,584,352,291,75,183])). % 61.99/62.08 cnf(616,plain, % 61.99/62.08 (~P11(f31(a19),f28(a1))+~P8(f28(a1),f30(a1),f30(a1))), % 61.99/62.08 inference(scs_inference,[],[133,584,352,291,75,183,148])). % 61.99/62.08 cnf(655,plain, % 61.99/62.08 (~P10(x6551,f30(a12),f30(a12),f28(a12))+~P8(f28(a12),f30(a12),f30(a12))+P16(x6551,a12,a12)), % 61.99/62.08 inference(scs_inference,[],[256,584,86,95,131,244,88,355,90,129,75,228])). % 61.99/62.08 cnf(733,plain, % 61.99/62.08 (P10(f5(x7331,a3,f27(x7331,a3)),x7331,a3,f27(x7331,a3))), % 61.99/62.08 inference(scs_inference,[],[277,125,134,187])). % 61.99/62.08 cnf(734,plain, % 61.99/62.08 (P10(f5(x7341,a3,f27(x7341,a3)),x7341,a3,x7342)+~E(f27(x7341,a3),x7342)), % 61.99/62.08 inference(scs_inference,[],[733,51])). % 61.99/62.08 cnf(735,plain, % 61.99/62.08 (P10(f5(x7351,a3,f27(x7351,a3)),x7352,a3,f27(x7351,a3))+~E(x7351,x7352)), % 61.99/62.08 inference(scs_inference,[],[733,51,49])). % 61.99/62.08 cnf(737,plain, % 61.99/62.08 (P10(x7371,x7372,a3,f27(x7372,a3))+~E(f5(x7372,a3,f27(x7372,a3)),x7371)), % 61.99/62.08 inference(scs_inference,[],[733,51,49,50,48])). % 61.99/62.08 cnf(940,plain, % 61.99/62.08 (~E(x9401,x9402)+P6(x9402,f32(x9401))), % 61.99/62.08 inference(scs_inference,[],[151,364])). % 61.99/62.08 cnf(941,plain, % 61.99/62.08 (P6(x9411,f32(x9411))), % 61.99/62.08 inference(equality_inference,[],[940])). % 61.99/62.08 cnf(978,plain, % 61.99/62.08 (E(f25(a10),f25(a23))), % 61.99/62.08 inference(scs_inference,[],[108,4,134])). % 61.99/62.08 cnf(979,plain, % 61.99/62.08 (P9(f4(f25(a10),x9791),f25(a23),x9791)), % 61.99/62.08 inference(scs_inference,[],[978,281])). % 61.99/62.08 cnf(980,plain, % 61.99/62.08 (P9(f4(x9801,f25(a10)),x9801,f25(a23))), % 61.99/62.08 inference(scs_inference,[],[978,281,282])). % 61.99/62.08 cnf(981,plain, % 61.99/62.08 (P8(f27(f25(a10),x9811),f25(a23),x9811)), % 61.99/62.08 inference(scs_inference,[],[978,281,282,316])). % 61.99/62.08 cnf(982,plain, % 61.99/62.08 (P8(f27(x9821,f25(a10)),x9821,f25(a23))), % 61.99/62.08 inference(scs_inference,[],[978,281,282,316,317])). % 61.99/62.08 cnf(984,plain, % 61.99/62.08 (P6(f25(f25(a10)),f25(a23))), % 61.99/62.08 inference(scs_inference,[],[978,281,282,316,317,318,339])). % 61.99/62.08 cnf(985,plain, % 61.99/62.08 (P7(f14(f25(a10),x9851),f25(a23),x9851)), % 61.99/62.08 inference(scs_inference,[],[978,281,282,316,317,318,339,362])). % 61.99/62.08 cnf(986,plain, % 61.99/62.08 (P7(f14(x9861,f25(a10)),x9861,f25(a23))), % 61.99/62.08 inference(scs_inference,[],[978,281,282,316,317,318,339,362,363])). % 61.99/62.08 cnf(989,plain, % 61.99/62.08 (P7(f26(f25(a10),x9891),f25(a23),x9891)), % 61.99/62.08 inference(scs_inference,[],[978,281,282,316,317,318,339,362,363,364,365,389])). % 61.99/62.08 cnf(990,plain, % 61.99/62.08 (P7(f7(x9901,f25(a10)),x9901,f25(a23))), % 61.99/62.08 inference(scs_inference,[],[978,281,282,316,317,318,339,362,363,364,365,389,415])). % 61.99/62.08 cnf(991,plain, % 61.99/62.08 (P13(f7(f25(a10),x9911),f25(a23),x9911)), % 61.99/62.08 inference(scs_inference,[],[978,281,282,316,317,318,339,362,363,364,365,389,415,445])). % 61.99/62.08 cnf(992,plain, % 61.99/62.08 (P7(f7(f25(a10),x9921),f25(a23),x9921)), % 61.99/62.08 inference(scs_inference,[],[978,281,282,316,317,318,339,362,363,364,365,389,415,445,446])). % 61.99/62.08 cnf(993,plain, % 61.99/62.08 (P7(f26(x9931,f25(a10)),x9931,f25(a23))), % 61.99/62.08 inference(scs_inference,[],[978,281,282,316,317,318,339,362,363,364,365,389,415,445,446,460])). % 61.99/62.08 cnf(994,plain, % 61.99/62.08 (P13(f7(x9941,f25(a10)),x9941,f25(a23))), % 61.99/62.08 inference(scs_inference,[],[978,281,282,316,317,318,339,362,363,364,365,389,415,445,446,460,476])). % 61.99/62.08 cnf(995,plain, % 61.99/62.08 (E(f25(a23),f25(a10))), % 61.99/62.08 inference(scs_inference,[],[978,281,282,316,317,318,339,362,363,364,365,389,415,445,446,460,476,2])). % 61.99/62.08 cnf(998,plain, % 61.99/62.08 (P8(f27(f25(a10),f25(a10)),f25(a23),f25(a23))), % 61.99/62.08 inference(scs_inference,[],[978,281,282,316,317,318,339,362,363,364,365,389,415,445,446,460,476,2,39,36,43])). % 61.99/62.08 cnf(1012,plain, % 61.99/62.08 (P7(f7(x10121,f25(a23)),x10121,f25(a10))), % 61.99/62.08 inference(scs_inference,[],[995,318,415])). % 61.99/62.08 cnf(1013,plain, % 61.99/62.08 (P9(f4(x10131,f25(a23)),x10131,f25(a10))), % 61.99/62.08 inference(scs_inference,[],[995,318,415,282])). % 61.99/62.08 cnf(1014,plain, % 61.99/62.08 (P7(f26(f25(a23),x10141),f25(a10),x10141)), % 61.99/62.08 inference(scs_inference,[],[995,318,415,282,389])). % 61.99/62.08 cnf(1015,plain, % 61.99/62.08 (P13(f7(f25(a23),x10151),f25(a10),x10151)), % 61.99/62.08 inference(scs_inference,[],[995,318,415,282,389,445])). % 61.99/62.08 cnf(1016,plain, % 61.99/62.08 (P7(f14(x10161,f25(a23)),x10161,f25(a10))), % 61.99/62.08 inference(scs_inference,[],[995,318,415,282,389,445,363])). % 61.99/62.08 cnf(1017,plain, % 61.99/62.08 (P7(f14(f25(a23),x10171),f25(a10),x10171)), % 61.99/62.08 inference(scs_inference,[],[995,318,415,282,389,445,363,362])). % 61.99/62.08 cnf(1018,plain, % 61.99/62.08 (P8(f27(f25(a23),x10181),f25(a10),x10181)), % 61.99/62.08 inference(scs_inference,[],[995,318,415,282,389,445,363,362,316])). % 61.99/62.08 cnf(1019,plain, % 61.99/62.08 (P7(f26(x10191,f25(a23)),x10191,f25(a10))), % 61.99/62.08 inference(scs_inference,[],[995,318,415,282,389,445,363,362,316,460])). % 61.99/62.08 cnf(1020,plain, % 61.99/62.08 (P7(f7(f25(a23),x10201),f25(a10),x10201)), % 61.99/62.08 inference(scs_inference,[],[995,318,415,282,389,445,363,362,316,460,446])). % 61.99/62.08 cnf(1021,plain, % 61.99/62.08 (P9(f4(f25(a23),x10211),f25(a10),x10211)), % 61.99/62.08 inference(scs_inference,[],[995,318,415,282,389,445,363,362,316,460,446,281])). % 61.99/62.08 cnf(1022,plain, % 61.99/62.08 (P8(f27(x10221,f25(a23)),x10221,f25(a10))), % 61.99/62.08 inference(scs_inference,[],[995,318,415,282,389,445,363,362,316,460,446,281,317])). % 61.99/62.08 cnf(1023,plain, % 61.99/62.08 (P13(f7(x10231,f25(a23)),x10231,f25(a10))), % 61.99/62.08 inference(scs_inference,[],[995,318,415,282,389,445,363,362,316,460,446,281,317,476])). % 61.99/62.08 cnf(1024,plain, % 61.99/62.08 (P6(f25(f25(a23)),f25(a10))), % 61.99/62.08 inference(scs_inference,[],[995,318,415,282,389,445,363,362,316,460,446,281,317,476,339])). % 61.99/62.08 cnf(1031,plain, % 61.99/62.08 (P8(f27(f25(a10),f25(a23)),f25(a23),f25(a10))), % 61.99/62.08 inference(scs_inference,[],[979,980,981,991,995,318,415,282,389,445,363,362,316,460,446,281,317,476,339,37,40,36,43])). % 61.99/62.08 cnf(1033,plain, % 61.99/62.08 (P8(f27(f25(a23),f25(a10)),f25(a10),f25(a23))), % 61.99/62.08 inference(scs_inference,[],[979,980,981,982,991,995,318,415,282,389,445,363,362,316,460,446,281,317,476,339,37,40,36,43,42])). % 61.99/62.08 cnf(1037,plain, % 61.99/62.08 (P17(f7(f25(a23),f30(a1)),f25(a10),f30(a1))), % 61.99/62.08 inference(scs_inference,[],[979,980,981,982,991,994,995,590,318,415,282,389,445,363,362,316,460,446,281,317,476,339,37,40,36,43,42,39,72])). % 61.99/62.08 cnf(1043,plain, % 61.99/62.08 (P6(f25(a10),f32(f25(a23)))), % 61.99/62.08 inference(scs_inference,[],[979,980,981,982,985,986,991,994,995,590,941,318,415,282,389,445,363,362,316,460,446,281,317,476,339,37,40,36,43,42,39,72,77,78,65])). % 61.99/62.08 cnf(1051,plain, % 61.99/62.08 (P17(f7(f25(a10),a3),f25(a23),a3)), % 61.99/62.08 inference(scs_inference,[],[978,264,72])). % 61.99/62.08 cnf(1088,plain, % 61.99/62.08 (~E(a16,a9)), % 61.99/62.08 inference(scs_inference,[],[329,291,75])). % 61.99/62.08 cnf(1111,plain, % 61.99/62.08 (P13(x11111,f25(a10),x11112)+~E(f7(f25(a23),x11112),x11111)), % 61.99/62.08 inference(scs_inference,[],[1015,329,350,75,38])). % 61.99/62.08 cnf(1123,plain, % 61.99/62.08 (P13(x11231,f25(a23),x11232)+~E(f7(f25(a10),x11232),x11231)), % 61.99/62.08 inference(scs_inference,[],[991,1043,1037,1051,585,247,75,73,71,156,38])). % 61.99/62.08 cnf(1178,plain, % 61.99/62.08 (P13(x11781,x11782,f25(a10))+~E(f7(x11782,f25(a23)),x11781)), % 61.99/62.08 inference(scs_inference,[],[1023,38])). % 61.99/62.08 cnf(1198,plain, % 61.99/62.08 (P9(x11981,x11982,f25(a10))+~E(f4(x11982,f25(a23)),x11981)), % 61.99/62.08 inference(scs_inference,[],[1013,35])). % 61.99/62.08 cnf(1199,plain, % 61.99/62.08 (P13(x11991,x11992,f25(a23))+~E(f7(x11992,f25(a10)),x11991)), % 61.99/62.08 inference(scs_inference,[],[1013,994,35,38])). % 61.99/62.08 cnf(1201,plain, % 61.99/62.08 (P7(x12011,f25(a23),x12012)+~E(f26(f25(a10),x12012),x12011)), % 61.99/62.08 inference(scs_inference,[],[989,1013,994,984,35,38,65,76])). % 61.99/62.08 cnf(1211,plain, % 61.99/62.08 (P9(x12111,f25(a10),x12112)+~E(f4(f25(a23),x12112),x12111)), % 61.99/62.08 inference(scs_inference,[],[1021,35])). % 61.99/62.08 cnf(1213,plain, % 61.99/62.08 (P7(x12131,x12132,f25(a23))+~E(f26(x12132,f25(a10)),x12131)), % 61.99/62.08 inference(scs_inference,[],[993,1021,1024,35,65,76])). % 61.99/62.08 cnf(1224,plain, % 61.99/62.08 (P9(x12241,f25(a23),x12242)+~E(f4(f25(a10),x12242),x12241)), % 61.99/62.08 inference(scs_inference,[],[979,35])). % 61.99/62.08 cnf(1225,plain, % 61.99/62.08 (P7(x12251,x12252,f25(a10))+~E(f14(x12252,f25(a23)),x12251)), % 61.99/62.08 inference(scs_inference,[],[1016,979,35,76])). % 61.99/62.08 cnf(1238,plain, % 61.99/62.08 (P9(x12381,x12382,f25(a23))+~E(f4(x12382,f25(a10)),x12381)), % 61.99/62.08 inference(scs_inference,[],[980,35])). % 61.99/62.08 cnf(1239,plain, % 61.99/62.08 (P7(x12391,f25(a10),x12392)+~E(f14(f25(a23),x12392),x12391)), % 61.99/62.08 inference(scs_inference,[],[1017,980,35,76])). % 61.99/62.08 cnf(1270,plain, % 61.99/62.08 (P7(x12701,f25(a23),x12702)+~E(f14(f25(a10),x12702),x12701)), % 61.99/62.08 inference(scs_inference,[],[985,76])). % 61.99/62.08 cnf(1285,plain, % 61.99/62.08 (P7(x12851,x12852,f25(a23))+~E(f14(x12852,f25(a10)),x12851)), % 61.99/62.08 inference(scs_inference,[],[986,76])). % 61.99/62.08 cnf(1301,plain, % 61.99/62.08 (P7(x13011,x13012,f25(a23))+~E(f7(x13012,f25(a10)),x13011)), % 61.99/62.08 inference(scs_inference,[],[990,76])). % 61.99/62.08 cnf(1317,plain, % 61.99/62.08 (P7(x13171,f25(a23),x13172)+~E(f7(f25(a10),x13172),x13171)), % 61.99/62.08 inference(scs_inference,[],[992,76])). % 61.99/62.08 cnf(1329,plain, % 61.99/62.08 (P7(x13291,x13292,f25(a10))+~E(f7(x13292,f25(a23)),x13291)), % 61.99/62.08 inference(scs_inference,[],[1012,76])). % 61.99/62.08 cnf(1341,plain, % 61.99/62.08 (P7(x13411,f25(a10),x13412)+~E(f26(f25(a23),x13412),x13411)), % 61.99/62.08 inference(scs_inference,[],[1014,76])). % 61.99/62.08 cnf(1353,plain, % 61.99/62.08 (P7(x13531,f25(a10),x13532)+~E(f7(f25(a23),x13532),x13531)), % 61.99/62.08 inference(scs_inference,[],[1020,76])). % 61.99/62.08 cnf(1372,plain, % 61.99/62.08 (P7(x13721,x13722,f25(a10))+~E(f26(x13722,f25(a23)),x13721)), % 61.99/62.08 inference(scs_inference,[],[1019,76])). % 61.99/62.08 cnf(4245,plain, % 61.99/62.08 (P12(a19)), % 61.99/62.08 inference(scs_inference,[],[87,89,91,127,83,556,162])). % 61.99/62.08 cnf(5565,plain, % 61.99/62.08 (P7(f14(f25(a23),f25(a23)),f25(a10),f25(a10))), % 61.99/62.08 inference(scs_inference,[],[995,1017,78])). % 61.99/62.08 cnf(5569,plain, % 61.99/62.08 (P9(f4(f25(a23),f25(a23)),f25(a10),f25(a10))), % 61.99/62.08 inference(scs_inference,[],[995,1015,1021,1017,78,40,37])). % 61.99/62.08 cnf(5573,plain, % 61.99/62.08 (P8(f27(f25(a23),f25(a23)),f25(a10),f25(a10))), % 61.99/62.08 inference(scs_inference,[],[995,1015,1021,1017,1012,1018,78,40,37,77,43])). % 61.99/62.08 cnf(6550,plain, % 61.99/62.08 (P12(a23)), % 61.99/62.08 inference(scs_inference,[],[105,135])). % 61.99/62.08 cnf(6564,plain, % 61.99/62.08 (E(a11,a23)), % 61.99/62.08 inference(scs_inference,[],[92,5565,124,107,105,135,136,138,168,172,164,165,134])). % 61.99/62.08 cnf(6568,plain, % 61.99/62.08 (E(f25(a11),f25(a23))), % 61.99/62.08 inference(scs_inference,[],[92,5573,5565,124,107,105,135,136,138,168,172,164,165,134,159,4])). % 61.99/62.08 cnf(6569,plain, % 61.99/62.08 (~E(a9,a16)), % 61.99/62.08 inference(scs_inference,[],[92,5573,1088,5565,124,107,105,135,136,138,168,172,164,165,134,159,4,2])). % 61.99/62.08 cnf(6572,plain, % 61.99/62.08 (P12(f25(a3))), % 61.99/62.08 inference(scs_inference,[],[92,5573,1088,5565,5569,96,124,107,105,115,135,136,138,168,172,164,165,134,159,4,2,167,147])). % 61.99/62.08 cnf(6573,plain, % 61.99/62.08 (P6(f25(x65731),x65731)), % 61.99/62.08 inference(rename_variables,[],[115])). % 61.99/62.08 cnf(6577,plain, % 61.99/62.08 (P12(f31(a13))), % 61.99/62.08 inference(scs_inference,[],[92,98,100,5573,1088,104,5565,5569,102,96,124,107,105,115,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141])). % 61.99/62.08 cnf(6579,plain, % 61.99/62.08 (~P18(f20(a18))), % 61.99/62.08 inference(scs_inference,[],[92,98,100,113,130,5573,1088,104,5565,5569,102,96,124,107,105,115,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144])). % 61.99/62.08 cnf(6586,plain, % 61.99/62.08 (~P18(f30(a18))), % 61.99/62.08 inference(scs_inference,[],[84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,124,107,105,115,995,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143])). % 61.99/62.08 cnf(6588,plain, % 61.99/62.08 (P15(f25(a3))), % 61.99/62.08 inference(scs_inference,[],[84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,124,107,105,115,6573,995,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146])). % 61.99/62.08 cnf(6589,plain, % 61.99/62.08 (P6(f25(x65891),x65891)), % 61.99/62.08 inference(rename_variables,[],[115])). % 61.99/62.08 cnf(6591,plain, % 61.99/62.08 (~E(a11,f7(f30(a1),f30(a1)))), % 61.99/62.08 inference(scs_inference,[],[84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,107,105,115,6573,995,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47])). % 61.99/62.08 cnf(6592,plain, % 61.99/62.08 (P18(f25(f32(a23)))), % 61.99/62.08 inference(scs_inference,[],[84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,247,107,105,115,6573,6589,995,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149])). % 61.99/62.08 cnf(6596,plain, % 61.99/62.08 (~P6(f30(a1),f32(a11))), % 61.99/62.08 inference(scs_inference,[],[84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,247,107,105,115,6573,6589,995,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155])). % 61.99/62.08 cnf(6598,plain, % 61.99/62.08 (P6(f5(x65981,a3,f27(x65981,a3)),f27(x65981,a3))), % 61.99/62.08 inference(scs_inference,[],[84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193])). % 61.99/62.08 cnf(6601,plain, % 61.99/62.08 (P8(f28(a1),f30(a1),f30(a1))), % 61.99/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162])). % 61.99/62.08 cnf(6603,plain, % 61.99/62.08 (P12(f31(a19))), % 61.99/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190])). % 61.99/62.08 cnf(6605,plain, % 61.99/62.08 (P16(f31(a19),a1,a1)), % 61.99/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198])). % 61.99/62.08 cnf(6607,plain, % 61.99/62.08 (P13(f31(a19),f30(a1),f30(a1))), % 61.99/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201])). % 61.99/62.08 cnf(6609,plain, % 61.99/62.08 (P9(f31(a19),f30(a1),f30(a1))), % 61.99/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202])). % 61.99/62.08 cnf(6611,plain, % 61.99/62.08 (P13(a19,f30(a1),f30(a1))), % 61.99/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229])). % 61.99/62.08 cnf(6613,plain, % 61.99/62.08 (P16(a19,a1,a1)), % 61.99/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228])). % 61.99/62.08 cnf(6615,plain, % 61.99/62.08 (P9(a19,f30(a1),f30(a1))), % 61.99/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230])). % 61.99/62.08 cnf(6617,plain, % 61.99/62.08 (P15(f15(a1,a1))), % 61.99/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157])). % 61.99/62.08 cnf(6619,plain, % 61.99/62.08 (P12(f15(a1,a1))), % 61.99/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158])). % 61.99/62.08 cnf(6621,plain, % 61.99/62.08 (~P18(f15(a1,a1))), % 61.99/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161])). % 61.99/62.08 cnf(6625,plain, % 61.99/62.08 (P7(f15(a1,a1),f30(a1),f30(a1))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169])). % 62.16/62.08 cnf(6631,plain, % 62.16/62.08 (P6(a23,f32(a11))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940])). % 62.16/62.08 cnf(6633,plain, % 62.16/62.08 (E(f30(a11),f30(a23))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9])). % 62.16/62.08 cnf(6640,plain, % 62.16/62.08 (E(f7(a11,x66401),f7(a23,x66401))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5])). % 62.16/62.08 cnf(6641,plain, % 62.16/62.08 (E(f7(x66411,a11),f7(x66411,a23))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6])). % 62.16/62.08 cnf(6642,plain, % 62.16/62.08 (E(f14(a11,x66421),f14(a23,x66421))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7])). % 62.16/62.08 cnf(6643,plain, % 62.16/62.08 (E(f14(x66431,a11),f14(x66431,a23))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8])). % 62.16/62.08 cnf(6646,plain, % 62.16/62.08 (E(f26(a11,x66461),f26(a23,x66461))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12])). % 62.16/62.08 cnf(6647,plain, % 62.16/62.08 (E(f26(x66471,a11),f26(x66471,a23))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13])). % 62.16/62.08 cnf(6650,plain, % 62.16/62.08 (E(f4(a11,x66501),f4(a23,x66501))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20])). % 62.16/62.08 cnf(6651,plain, % 62.16/62.08 (E(f4(x66511,a11),f4(x66511,a23))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21])). % 62.16/62.08 cnf(6652,plain, % 62.16/62.08 (E(f27(a11,x66521),f27(a23,x66521))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21,22])). % 62.16/62.08 cnf(6653,plain, % 62.16/62.08 (E(f27(x66531,a11),f27(x66531,a23))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21,22,23])). % 62.16/62.08 cnf(6664,plain, % 62.16/62.08 (E(f5(a11,x66641,x66642),f5(a23,x66641,x66642))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21,22,23,24,25,26,27,28,29,314,392,416,443,17])). % 62.16/62.08 cnf(6670,plain, % 62.16/62.08 (P9(f4(a23,f25(a23)),a11,f25(a10))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21,22,23,24,25,26,27,28,29,314,392,416,443,17,18,19,602,603,1111,1198])). % 62.16/62.08 cnf(6671,plain, % 62.16/62.08 (P7(f26(f25(a10),a23),f25(a23),a11)), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21,22,23,24,25,26,27,28,29,314,392,416,443,17,18,19,602,603,1111,1198,1201])). % 62.16/62.08 cnf(6672,plain, % 62.16/62.08 (P9(f4(f25(a23),a23),f25(a10),a11)), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21,22,23,24,25,26,27,28,29,314,392,416,443,17,18,19,602,603,1111,1198,1201,1211])). % 62.16/62.08 cnf(6673,plain, % 62.16/62.08 (P7(f26(a23,f25(a10)),a11,f25(a23))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21,22,23,24,25,26,27,28,29,314,392,416,443,17,18,19,602,603,1111,1198,1201,1211,1213])). % 62.16/62.08 cnf(6674,plain, % 62.16/62.08 (P7(f14(a23,f25(a23)),a11,f25(a10))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21,22,23,24,25,26,27,28,29,314,392,416,443,17,18,19,602,603,1111,1198,1201,1211,1213,1225])). % 62.16/62.08 cnf(6676,plain, % 62.16/62.08 (P7(f7(f25(a23),a23),f25(a10),a11)), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21,22,23,24,25,26,27,28,29,314,392,416,443,17,18,19,602,603,1111,1198,1201,1211,1213,1225,1239,1353])). % 62.16/62.08 cnf(6680,plain, % 62.16/62.08 (~P6(f31(a19),f28(a1))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21,22,23,24,25,26,27,28,29,314,392,416,443,17,18,19,602,603,1111,1198,1201,1211,1213,1225,1239,1353,418,429,447,614])). % 62.16/62.08 cnf(6681,plain, % 62.16/62.08 (~P11(f31(a19),f28(a1))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21,22,23,24,25,26,27,28,29,314,392,416,443,17,18,19,602,603,1111,1198,1201,1211,1213,1225,1239,1353,418,429,447,614,616])). % 62.16/62.08 cnf(6683,plain, % 62.16/62.08 (P10(f5(a23,a3,f27(a11,a3)),a11,a3,f27(a11,a3))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21,22,23,24,25,26,27,28,29,314,392,416,443,17,18,19,602,603,1111,1198,1201,1211,1213,1225,1239,1353,418,429,447,614,616,735,737])). % 62.16/62.08 cnf(6684,plain, % 62.16/62.08 (~P18(f28(a1))), % 62.16/62.08 inference(scs_inference,[],[83,84,92,93,98,100,113,130,5573,1088,104,5565,5569,102,96,595,124,585,733,247,107,105,125,115,6573,6589,89,87,127,91,126,995,131,135,136,138,168,172,164,165,134,159,4,2,167,147,140,141,144,3,154,150,143,146,47,149,155,193,162,190,198,201,202,229,228,230,157,158,161,166,169,170,171,940,9,16,30,31,32,33,417,5,6,7,8,10,11,12,13,14,15,20,21,22,23,24,25,26,27,28,29,314,392,416,443,17,18,19,602,603,1111,1198,1201,1211,1213,1225,1239,1353,418,429,447,614,616,735,737,160])). % 62.16/62.08 cnf(6742,plain, % 62.16/62.08 (E(f7(a11,x67421),f7(a23,x67421))), % 62.16/62.08 inference(rename_variables,[],[6640])). % 62.16/62.08 cnf(6743,plain, % 62.16/62.08 (P13(f7(f25(a10),a23),f25(a23),a11)), % 62.16/62.08 inference(scs_inference,[],[6640,6641,430,1123])). % 62.16/62.08 cnf(6744,plain, % 62.16/62.08 (E(f7(x67441,a11),f7(x67441,a23))), % 62.16/62.08 inference(rename_variables,[],[6641])). % 62.16/62.08 cnf(6746,plain, % 62.16/62.08 (E(f7(a11,x67461),f7(a23,x67461))), % 62.16/62.08 inference(rename_variables,[],[6640])). % 62.16/62.08 cnf(6748,plain, % 62.16/62.08 (E(f7(a11,x67481),f7(a23,x67481))), % 62.16/62.08 inference(rename_variables,[],[6640])). % 62.16/62.08 cnf(6749,plain, % 62.16/62.08 (P9(f4(f25(a10),a23),f25(a23),a11)), % 62.16/62.08 inference(scs_inference,[],[6640,6742,6746,6641,6651,430,1123,1178,1199,1224])). % 62.16/62.08 cnf(6751,plain, % 62.16/62.08 (P9(f4(a23,f25(a10)),a11,f25(a23))), % 62.16/62.08 inference(scs_inference,[],[6640,6742,6746,6641,6650,6651,430,1123,1178,1199,1224,1238])). % 62.16/62.08 cnf(6753,plain, % 62.16/62.08 (P7(f14(f25(a10),a23),f25(a23),a11)), % 62.16/62.08 inference(scs_inference,[],[6640,6742,6746,6641,6643,6650,6651,430,1123,1178,1199,1224,1238,1270])). % 62.16/62.08 cnf(6758,plain, % 62.16/62.08 (E(f7(a11,x67581),f7(a23,x67581))), % 62.16/62.08 inference(rename_variables,[],[6640])). % 62.16/62.08 cnf(6768,plain, % 62.16/62.08 (E(f27(a11,x67681),f27(a23,x67681))), % 62.16/62.08 inference(rename_variables,[],[6652])). % 62.16/62.08 cnf(6770,plain, % 62.16/62.08 (E(f27(a11,x67701),f27(a23,x67701))), % 62.16/62.08 inference(rename_variables,[],[6652])). % 62.16/62.08 cnf(6771,plain, % 62.16/62.08 (P6(f5(a23,x67711,x67712),f32(f5(a11,x67711,x67712)))), % 62.16/62.08 inference(scs_inference,[],[6664,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940])). % 62.16/62.08 cnf(6779,plain, % 62.16/62.08 (E(f25(f32(a23)),a23)), % 62.16/62.08 inference(scs_inference,[],[94,6664,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6625,6592,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134])). % 62.16/62.08 cnf(6789,plain, % 62.16/62.08 (P3(f28(a1))), % 62.16/62.08 inference(scs_inference,[],[94,6664,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6625,6601,6592,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159])). % 62.16/62.08 cnf(6793,plain, % 62.16/62.08 (~E(f25(f28(a1)),f31(a19))), % 62.16/62.08 inference(scs_inference,[],[94,6615,6680,6664,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6625,6601,6592,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159,167,318])). % 62.16/62.08 cnf(6795,plain, % 62.16/62.08 (P10(f5(f30(a1),f30(a1),f28(a1)),f30(a1),f30(a1),f28(a1))), % 62.16/62.08 inference(scs_inference,[],[94,6615,6680,6664,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6625,6601,6592,6591,584,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159,167,318,2,187])). % 62.16/62.08 cnf(6803,plain, % 62.16/62.08 (~P18(f20(a8))), % 62.16/62.08 inference(scs_inference,[],[94,128,6615,6680,6664,6619,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6625,6572,6588,6601,6617,6592,6591,584,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159,167,318,2,187,140,141,154,144])). % 62.16/62.08 cnf(6805,plain, % 62.16/62.08 (E(f29(f30(a1),f33(a1)),a1)), % 62.16/62.08 inference(scs_inference,[],[83,94,128,6615,6680,6664,6619,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6625,6572,6588,6601,6617,6592,6591,91,584,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159,167,318,2,187,140,141,154,144,150])). % 62.16/62.08 cnf(6807,plain, % 62.16/62.08 (~P18(f30(a8))), % 62.16/62.08 inference(scs_inference,[],[83,94,128,6615,6680,6664,6619,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6625,6572,6588,6601,6617,6592,6591,91,584,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159,167,318,2,187,140,141,154,144,150,143])). % 62.16/62.08 cnf(6811,plain, % 62.16/62.08 (P6(x68111,f32(x68111))), % 62.16/62.08 inference(rename_variables,[],[941])). % 62.16/62.08 cnf(6813,plain, % 62.16/62.08 (P8(f27(a23,f25(a23)),a11,f25(a10))), % 62.16/62.08 inference(scs_inference,[],[83,94,128,6564,6615,6680,6664,6619,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6770,6625,6572,6588,6596,6601,6617,6592,6591,1022,941,91,584,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159,167,318,2,187,140,141,154,144,150,143,3,156,41])). % 62.16/62.08 cnf(6814,plain, % 62.16/62.08 (E(f27(a11,x68141),f27(a23,x68141))), % 62.16/62.08 inference(rename_variables,[],[6652])). % 62.16/62.08 cnf(6816,plain, % 62.16/62.08 (~P11(f27(a11,x68161),f25(f27(a23,x68161)))), % 62.16/62.08 inference(scs_inference,[],[83,94,128,6564,6615,6680,6664,6619,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6770,6814,6625,6572,6588,6596,6601,6617,6592,6591,1022,311,941,91,584,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159,167,318,2,187,140,141,154,144,150,143,3,156,41,74])). % 62.16/62.08 cnf(6818,plain, % 62.16/62.08 (~E(f30(a1),a9)), % 62.16/62.08 inference(scs_inference,[],[83,94,128,6564,6615,6680,6664,6619,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6770,6814,6625,6572,6588,6596,6601,6617,6592,6591,1022,311,291,941,585,91,584,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159,167,318,2,187,140,141,154,144,150,143,3,156,41,74,75])). % 62.16/62.08 cnf(6820,plain, % 62.16/62.08 (~E(f25(f32(a23)),f15(a1,a1))), % 62.16/62.08 inference(scs_inference,[],[83,94,128,6564,6615,6680,6621,6664,6619,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6770,6814,6625,6572,6588,6596,6601,6617,6592,6591,1022,311,291,941,585,91,584,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159,167,318,2,187,140,141,154,144,150,143,3,156,41,74,75,47])). % 62.16/62.08 cnf(6829,plain, % 62.16/62.08 (P8(f27(x68291,x68292),x68291,x68292)), % 62.16/62.08 inference(rename_variables,[],[125])). % 62.16/62.08 cnf(6832,plain, % 62.16/62.08 (P8(f27(x68321,x68322),x68321,x68322)), % 62.16/62.08 inference(rename_variables,[],[125])). % 62.16/62.08 cnf(6839,plain, % 62.16/62.08 (P8(f28(a12),f30(a12),f30(a12))), % 62.16/62.08 inference(scs_inference,[],[83,94,128,6564,6611,6615,6680,6621,6664,6631,6619,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6770,6814,6625,6572,6588,6596,6601,6617,6683,6598,6592,6591,1022,311,291,941,6811,585,242,125,6829,6832,91,86,90,95,129,88,131,584,4245,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159,167,318,2,187,140,141,154,144,150,143,3,156,41,74,75,47,149,65,66,192,205,204,175,162])). % 62.16/62.08 cnf(6841,plain, % 62.16/62.08 (~P18(a19)), % 62.16/62.08 inference(scs_inference,[],[83,94,128,6564,6611,6615,6680,6621,6664,6631,6619,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6770,6814,6625,6572,6588,6596,6601,6617,6683,6598,6592,6591,1022,311,291,941,6811,585,242,125,6829,6832,91,86,90,95,129,88,131,584,4245,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159,167,318,2,187,140,141,154,144,150,143,3,156,41,74,75,47,149,65,66,192,205,204,175,162,173])). % 62.16/62.08 cnf(6843,plain, % 62.16/62.08 (~P18(f28(a12))), % 62.16/62.08 inference(scs_inference,[],[83,94,128,6564,6611,6615,6680,6621,6664,6631,6619,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6770,6814,6625,6572,6588,6596,6601,6617,6683,6598,6592,6591,1022,311,291,941,6811,585,242,125,6829,6832,91,86,90,95,129,88,131,584,4245,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159,167,318,2,187,140,141,154,144,150,143,3,156,41,74,75,47,149,65,66,192,205,204,175,162,173,160])). % 62.16/62.08 cnf(6845,plain, % 62.16/62.08 (~P11(f27(x68451,a3),f5(x68451,a3,f27(x68451,a3)))), % 62.16/62.08 inference(scs_inference,[],[83,94,128,6564,6611,6615,6680,6621,6664,6631,6619,6640,6742,6746,6748,6758,6641,6744,6642,6643,6646,6647,6650,6651,6652,6768,6770,6814,6625,6572,6588,6596,6601,6617,6683,6598,6592,6591,1022,311,291,941,6811,585,242,125,6829,6832,91,86,90,95,129,88,131,584,4245,430,1123,1178,1199,1224,1238,1270,1285,1301,1317,1329,1341,1372,471,734,940,168,165,135,134,164,138,602,417,136,159,167,318,2,187,140,141,154,144,150,143,3,156,41,74,75,47,149,65,66,192,205,204,175,162,173,160,152])). % 62.16/62.08 cnf(6877,plain, % 62.16/62.08 (~P10(x68771,f30(a12),f30(a12),f28(a12))+P16(x68771,a12,a12)), % 62.16/62.08 inference(scs_inference,[],[6839,655])). % 62.16/62.08 cnf(6886,plain, % 62.16/62.08 (E(a10,a23)), % 62.16/62.08 inference(scs_inference,[],[6676,6568,93,108,940,165,168,136,134])). % 62.16/62.08 cnf(6888,plain, % 62.16/62.08 (E(f27(x68881,a10),f27(x68881,a23))), % 62.16/62.08 inference(scs_inference,[],[6676,6568,93,108,940,165,168,136,134,23])). % 62.16/62.08 cnf(6889,plain, % 62.16/62.08 (E(f26(x68891,a10),f26(x68891,a23))), % 62.16/62.08 inference(scs_inference,[],[6676,6568,93,108,940,165,168,136,134,23,13])). % 62.16/62.08 cnf(6890,plain, % 62.16/62.08 (E(f20(a10),f20(a23))), % 62.16/62.08 inference(scs_inference,[],[6676,6568,93,108,940,165,168,136,134,23,13,32])). % 62.16/62.08 cnf(6893,plain, % 62.16/62.08 (E(f4(a10,x68931),f4(a23,x68931))), % 62.16/62.08 inference(scs_inference,[],[6676,6568,93,108,940,165,168,136,134,23,13,32,164,20])). % 62.16/62.08 cnf(6895,plain, % 62.16/62.08 (E(f14(a10,x68951),f14(a23,x68951))), % 62.16/62.08 inference(scs_inference,[],[6676,6568,93,108,940,165,168,136,134,23,13,32,164,20,25,7])). % 62.16/62.08 cnf(6896,plain, % 62.16/62.08 (P3(f28(a12))), % 62.16/62.08 inference(scs_inference,[],[6839,6676,6568,93,108,940,165,168,136,134,23,13,32,164,20,25,7,159])). % 62.16/62.08 cnf(6905,plain, % 62.16/62.08 (P10(f5(x69051,a19,f27(x69051,a19)),x69051,a19,f27(x69051,a19))), % 62.16/62.08 inference(scs_inference,[],[6841,6609,6839,6818,6676,6568,93,108,125,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187])). % 62.16/62.08 cnf(6909,plain, % 62.16/62.08 (P6(f25(x69091),x69091)), % 62.16/62.08 inference(rename_variables,[],[115])). % 62.16/62.08 cnf(6915,plain, % 62.16/62.08 (E(f29(f30(a8),f33(a8)),a8)), % 62.16/62.08 inference(scs_inference,[],[85,6841,6609,6789,6839,6818,6676,6568,93,97,6619,6617,101,94,108,125,115,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150])). % 62.16/62.08 cnf(6917,plain, % 62.16/62.08 (~E(a23,f15(a1,a1))), % 62.16/62.08 inference(scs_inference,[],[85,6841,6609,6789,6839,6818,6676,6820,6779,6568,93,97,6619,6617,101,94,108,125,115,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3])). % 62.16/62.08 cnf(6919,plain, % 62.16/62.08 (P6(f25(x69191),x69191)), % 62.16/62.08 inference(rename_variables,[],[115])). % 62.16/62.08 cnf(6921,plain, % 62.16/62.08 (~E(f5(f30(a1),f30(a1),f28(a1)),f31(a19))), % 62.16/62.08 inference(scs_inference,[],[85,6841,6609,6789,6839,6818,6676,6795,6820,6779,6568,93,97,6619,6617,101,94,108,125,115,6909,133,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48])). % 62.16/62.08 cnf(6922,plain, % 62.16/62.08 (~E(f28(a12),a9)), % 62.16/62.08 inference(scs_inference,[],[85,6841,6609,6789,6839,6818,6676,6795,6820,6779,289,6568,93,97,6619,6617,101,94,108,125,115,6909,133,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41])). % 62.16/62.08 cnf(6926,plain, % 62.16/62.08 (E(f27(x69261,a11),f27(x69261,a23))), % 62.16/62.08 inference(rename_variables,[],[6653])). % 62.16/62.08 cnf(6928,plain, % 62.16/62.08 (~E(f25(f32(a23)),a19)), % 62.16/62.08 inference(scs_inference,[],[85,262,6841,6609,6789,6839,6818,6676,6795,6820,6779,289,6568,6653,93,97,6619,6617,101,6592,94,108,293,125,115,6909,133,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47])). % 62.16/62.08 cnf(6932,plain, % 62.16/62.08 (P15(a23)), % 62.16/62.08 inference(scs_inference,[],[85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6653,6926,93,97,99,6619,6617,101,6592,94,108,293,125,115,6909,133,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61])). % 62.16/62.08 cnf(6933,plain, % 62.16/62.08 (P18(f25(f32(a9)))), % 62.16/62.08 inference(scs_inference,[],[85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6653,6926,93,97,99,6619,6617,101,6592,94,296,108,293,125,115,6909,6919,133,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61,149])). % 62.16/62.08 cnf(6935,plain, % 62.16/62.08 (P6(f25(x69351),x69351)), % 62.16/62.08 inference(rename_variables,[],[115])). % 62.16/62.08 cnf(6954,plain, % 62.16/62.08 (P10(f5(a10,a3,f27(a10,a3)),a23,a3,f27(a10,a3))), % 62.16/62.08 inference(scs_inference,[],[83,85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6633,6653,6926,93,97,99,6619,6617,101,6601,6592,1020,94,1015,296,941,108,293,125,115,6909,6919,6935,89,87,127,91,133,118,584,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61,149,65,66,192,175,228,230,229,735])). % 62.16/62.08 cnf(6957,plain, % 62.16/62.08 (E(f14(x69571,a10),f14(x69571,a23))), % 62.16/62.08 inference(scs_inference,[],[83,85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6633,6653,6926,93,97,99,6619,6617,101,6601,6592,1020,94,1015,296,941,108,293,125,115,6909,6919,6935,89,87,127,91,133,118,584,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61,149,65,66,192,175,228,230,229,735,1341,14,8])). % 62.16/62.08 cnf(6961,plain, % 62.16/62.08 (E(f7(a10,x69611),f7(a23,x69611))), % 62.16/62.08 inference(scs_inference,[],[83,85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6633,6653,6926,93,97,99,6619,6617,101,6601,6592,1020,94,1015,296,941,108,293,125,115,6909,6919,6935,89,87,127,91,133,118,584,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61,149,65,66,192,175,228,230,229,735,1341,14,8,28,416,9,5])). % 62.16/62.08 cnf(6963,plain, % 62.16/62.08 (E(f4(x69631,a10),f4(x69631,a23))), % 62.16/62.08 inference(scs_inference,[],[83,85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6633,6653,6926,93,97,99,6619,6617,101,6601,6592,1020,94,1015,296,941,108,293,125,115,6909,6919,6935,89,87,127,91,133,118,584,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61,149,65,66,192,175,228,230,229,735,1341,14,8,28,416,9,5,19,21])). % 62.16/62.08 cnf(6965,plain, % 62.16/62.08 (P9(f4(a23,f25(a23)),a10,f25(a10))), % 62.16/62.08 inference(scs_inference,[],[83,85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6633,6653,6926,93,97,99,6619,6617,101,6601,6592,1020,94,1015,296,941,108,293,125,115,6909,6919,6935,89,87,127,91,133,118,584,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61,149,65,66,192,175,228,230,229,735,1341,14,8,28,416,9,5,19,21,10,1198])). % 62.16/62.08 cnf(6969,plain, % 62.16/62.08 (E(f7(x69691,a10),f7(x69691,a23))), % 62.16/62.08 inference(scs_inference,[],[83,85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6633,6653,6926,93,97,99,6619,6617,101,6601,6592,1020,94,1015,296,941,108,293,125,115,6909,6919,6935,89,87,127,91,133,118,584,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61,149,65,66,192,175,228,230,229,735,1341,14,8,28,416,9,5,19,21,10,1198,1199,1270,30,6])). % 62.16/62.08 cnf(6971,plain, % 62.16/62.08 (P9(f4(f25(a10),a23),f25(a23),a10)), % 62.16/62.08 inference(scs_inference,[],[83,85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6633,6653,6926,93,97,99,6619,6617,101,6601,6592,1020,94,1015,296,941,108,293,125,115,6909,6919,6935,89,87,127,91,133,118,584,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61,149,65,66,192,175,228,230,229,735,1341,14,8,28,416,9,5,19,21,10,1198,1199,1270,30,6,15,1224])). % 62.16/62.08 cnf(6972,plain, % 62.16/62.08 (E(f27(a10,x69721),f27(a23,x69721))), % 62.16/62.08 inference(scs_inference,[],[83,85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6633,6653,6926,93,97,99,6619,6617,101,6601,6592,1020,94,1015,296,941,108,293,125,115,6909,6919,6935,89,87,127,91,133,118,584,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61,149,65,66,192,175,228,230,229,735,1341,14,8,28,416,9,5,19,21,10,1198,1199,1270,30,6,15,1224,22])). % 62.16/62.08 cnf(6986,plain, % 62.16/62.08 (P7(f7(f25(a23),a23),f25(a10),a10)), % 62.16/62.08 inference(scs_inference,[],[83,85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6633,6653,6926,93,97,99,6619,6617,101,6601,6592,1020,94,1015,296,941,108,293,125,115,6909,6919,6935,89,87,127,91,133,118,584,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61,149,65,66,192,175,228,230,229,735,1341,14,8,28,416,9,5,19,21,10,1198,1199,1270,30,6,15,1224,22,1285,1301,26,11,31,418,27,392,29,16,314,18,33,1353])). % 62.16/62.08 cnf(6988,plain, % 62.16/62.08 (E(f5(a10,x69881,x69882),f5(a23,x69881,x69882))), % 62.16/62.08 inference(scs_inference,[],[83,85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6633,6653,6926,93,97,99,6619,6617,101,6601,6592,1020,94,1015,296,941,108,293,125,115,6909,6919,6935,89,87,127,91,133,118,584,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61,149,65,66,192,175,228,230,229,735,1341,14,8,28,416,9,5,19,21,10,1198,1199,1270,30,6,15,1224,22,1285,1301,26,11,31,418,27,392,29,16,314,18,33,1353,24,17])). % 62.16/62.08 cnf(6992,plain, % 62.16/62.08 (E(f26(a10,x69921),f26(a23,x69921))), % 62.16/62.08 inference(scs_inference,[],[83,85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6633,6653,6926,93,97,99,6619,6617,101,6601,6592,1020,94,1015,296,941,108,293,125,115,6909,6919,6935,89,87,127,91,133,118,584,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61,149,65,66,192,175,228,230,229,735,1341,14,8,28,416,9,5,19,21,10,1198,1199,1270,30,6,15,1224,22,1285,1301,26,11,31,418,27,392,29,16,314,18,33,1353,24,17,148,447,12])). % 62.16/62.08 cnf(6995,plain, % 62.16/62.08 (~P11(f27(x69951,a23),f25(f27(x69951,a11)))), % 62.16/62.08 inference(scs_inference,[],[83,85,262,6841,6609,6789,6839,6818,6676,6795,6820,6816,6779,289,6568,6633,6653,6926,93,97,99,6619,6617,101,6601,6592,1020,94,1015,296,941,108,293,125,115,6909,6919,6935,89,87,127,91,133,118,584,940,165,168,136,134,23,13,32,164,20,25,7,159,138,602,417,167,2,187,147,141,140,150,3,146,48,41,56,75,47,74,61,149,65,66,192,175,228,230,229,735,1341,14,8,28,416,9,5,19,21,10,1198,1199,1270,30,6,15,1224,22,1285,1301,26,11,31,418,27,392,29,16,314,18,33,1353,24,17,148,447,12,443,1111,152])). % 62.16/62.08 cnf(7028,plain, % 62.16/62.08 (E(f7(x70281,a10),f7(x70281,a23))), % 62.16/62.08 inference(rename_variables,[],[6969])). % 62.16/62.08 cnf(7032,plain, % 62.16/62.08 (E(f27(a10,x70321),f27(a23,x70321))), % 62.16/62.08 inference(rename_variables,[],[6972])). % 62.16/62.08 cnf(7034,plain, % 62.16/62.08 (E(f26(a10,x70341),f26(a23,x70341))), % 62.16/62.08 inference(rename_variables,[],[6992])). % 62.16/62.08 cnf(7036,plain, % 62.16/62.08 (E(f27(a10,x70361),f27(a23,x70361))), % 62.16/62.08 inference(rename_variables,[],[6972])). % 62.16/62.08 cnf(7038,plain, % 62.16/62.08 (E(f7(a10,x70381),f7(a23,x70381))), % 62.16/62.08 inference(rename_variables,[],[6961])). % 62.16/62.08 cnf(7040,plain, % 62.16/62.08 (E(f7(a10,x70401),f7(a23,x70401))), % 62.16/62.08 inference(rename_variables,[],[6961])). % 62.16/62.08 cnf(7043,plain, % 62.16/62.08 (P9(f4(a23,f25(a10)),a10,f25(a23))), % 62.16/62.08 inference(scs_inference,[],[6893,6957,6961,7038,6963,6969,6972,7032,6992,1317,1211,471,1213,734,430,603,1239,1238])). % 62.16/62.08 cnf(7050,plain, % 62.16/62.08 (E(f7(a10,x70501),f7(a23,x70501))), % 62.16/62.08 inference(rename_variables,[],[6961])). % 62.16/62.08 cnf(7071,plain, % 62.16/62.08 (E(f25(f32(a9)),a23)), % 62.16/62.08 inference(scs_inference,[],[6886,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6671,6813,6933,91,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134])). % 62.16/62.08 cnf(7075,plain, % 62.16/62.08 (P10(f5(a23,a3,f27(a10,a3)),a10,a3,f27(a10,a3))), % 62.16/62.08 inference(scs_inference,[],[6886,6988,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6671,6813,6933,91,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737])). % 62.16/62.08 cnf(7076,plain, % 62.16/62.08 (E(f5(a10,x70761,x70762),f5(a23,x70761,x70762))), % 62.16/62.08 inference(rename_variables,[],[6988])). % 62.16/62.08 cnf(7083,plain, % 62.16/62.08 (~E(f15(a1,a1),a23)), % 62.16/62.08 inference(scs_inference,[],[6886,6988,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6917,6672,6671,6813,6933,91,95,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737,138,602,417,167,2])). % 62.16/62.08 cnf(7084,plain, % 62.16/62.08 (~P18(f20(a1))), % 62.16/62.08 inference(scs_inference,[],[6886,6988,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6917,6672,6671,6813,6933,127,91,95,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737,138,602,417,167,2,144])). % 62.16/62.08 cnf(7089,plain, % 62.16/62.08 (P6(f25(x70891),x70891)), % 62.16/62.08 inference(rename_variables,[],[115])). % 62.16/62.08 cnf(7091,plain, % 62.16/62.08 (P12(f31(a23))), % 62.16/62.08 inference(scs_inference,[],[6550,6886,6932,6988,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6896,6917,6672,6671,6813,6933,115,127,91,95,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737,138,602,417,167,2,144,154,147,141])). % 62.16/62.08 cnf(7095,plain, % 62.16/62.08 (P15(f31(a23))), % 62.16/62.08 inference(scs_inference,[],[6550,6886,6932,6988,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6896,6917,6672,6671,6813,6933,115,86,127,91,95,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737,138,602,417,167,2,144,154,147,141,150,140])). % 62.16/62.08 cnf(7100,plain, % 62.16/62.08 (~E(a23,a19)), % 62.16/62.08 inference(scs_inference,[],[6550,6886,6932,6988,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6896,6917,6672,6671,6813,6933,6928,6779,115,7089,86,127,91,95,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737,138,602,417,167,2,144,154,147,141,150,140,146,3])). % 62.16/62.08 cnf(7102,plain, % 62.16/62.08 (E(f5(a10,x71021,x71022),f5(a23,x71021,x71022))), % 62.16/62.08 inference(rename_variables,[],[6988])). % 62.16/62.08 cnf(7103,plain, % 62.16/62.08 (P10(f5(x71031,a19,f27(x71031,a19)),x71031,a19,f27(x71031,a19))), % 62.16/62.08 inference(rename_variables,[],[6905])). % 62.16/62.08 cnf(7104,plain, % 62.16/62.08 (P8(f27(f25(a23),a23),f25(a10),a10)), % 62.16/62.08 inference(scs_inference,[],[6550,6886,6932,6988,7076,6888,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6896,6917,6672,6671,6905,6813,6933,6928,6779,1018,115,7089,86,127,91,95,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737,138,602,417,167,2,144,154,147,141,150,140,146,3,48,41])). % 62.16/62.08 cnf(7105,plain, % 62.16/62.08 (E(f27(x71051,a10),f27(x71051,a23))), % 62.16/62.08 inference(rename_variables,[],[6888])). % 62.16/62.08 cnf(7107,plain, % 62.16/62.08 (~E(f25(f32(a9)),f20(a18))), % 62.16/62.08 inference(scs_inference,[],[6550,6886,6932,6988,7076,6888,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6579,6896,6917,6672,6671,6905,6813,6933,6928,6779,1018,115,7089,86,127,91,95,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737,138,602,417,167,2,144,154,147,141,150,140,146,3,48,41,47])). % 62.16/62.08 cnf(7108,plain, % 62.16/62.08 (~P11(f27(a23,a3),f5(a10,a3,f27(a23,a3)))), % 62.16/62.08 inference(scs_inference,[],[6550,6886,6932,6988,7076,7102,6888,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6579,6896,6917,6672,6671,6905,6813,6845,6933,6928,6779,1018,115,7089,86,127,91,95,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737,138,602,417,167,2,144,154,147,141,150,140,146,3,48,41,47,75])). % 62.16/62.08 cnf(7112,plain, % 62.16/62.08 (~P11(f27(x71121,a10),f25(f27(x71121,a11)))), % 62.16/62.08 inference(scs_inference,[],[6550,6886,6932,6988,7076,7102,6888,7105,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6579,6896,6917,6672,6671,6905,6813,6995,6845,6933,6915,6928,6779,128,1018,115,7089,86,127,91,95,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737,138,602,417,167,2,144,154,147,141,150,140,146,3,48,41,47,75,55,74])). % 62.16/62.08 cnf(7116,plain, % 62.16/62.08 (P12(f5(x71161,a19,f27(x71161,a19)))), % 62.16/62.08 inference(scs_inference,[],[6550,6886,6932,6988,7076,7102,6888,7105,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6579,6896,6917,6672,6671,6905,7103,6813,6995,6845,6933,6915,6928,6779,6596,128,6841,941,1018,125,115,7089,86,127,91,95,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737,138,602,417,167,2,144,154,147,141,150,140,146,3,48,41,47,75,55,74,66,192])). % 62.16/62.08 cnf(7124,plain, % 62.16/62.08 (P15(f15(a12,a1))), % 62.16/62.08 inference(scs_inference,[],[6550,6886,6932,6988,7076,7102,6888,7105,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6579,6896,6917,6672,6671,6905,7103,6813,6995,6845,6933,6915,6928,6779,6596,128,6841,941,1018,125,115,7089,89,86,87,127,91,90,95,129,88,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737,138,602,417,167,2,144,154,147,141,150,140,146,3,48,41,47,75,55,74,66,192,161,166,157])). % 62.16/62.08 cnf(7128,plain, % 62.16/62.08 (P12(f15(a12,a1))), % 62.16/62.08 inference(scs_inference,[],[6550,6886,6932,6988,7076,7102,6888,7105,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6579,6896,6917,6672,6671,6905,7103,6813,6995,6845,6933,6915,6928,6779,6596,128,6841,941,1018,125,115,7089,89,86,87,127,91,90,95,129,88,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737,138,602,417,167,2,144,154,147,141,150,140,146,3,48,41,47,75,55,74,66,192,161,166,157,170,158])). % 62.16/62.08 cnf(7132,plain, % 62.16/62.08 (P7(f15(a12,a1),f30(a12),f30(a1))), % 62.16/62.08 inference(scs_inference,[],[6550,6886,6932,6988,7076,7102,6888,7105,6889,6893,6895,6957,6961,7038,7040,7050,6963,6969,7028,6972,7032,7036,6992,7034,6579,6896,6917,6672,6671,6905,7103,6813,6995,6845,6933,6915,6928,6779,6596,128,6841,941,1018,125,115,7089,89,86,87,127,91,90,95,129,88,1317,1211,471,1213,734,430,603,1239,1238,940,135,1178,1329,1225,1123,1201,1372,165,429,136,159,168,134,164,737,138,602,417,167,2,144,154,147,141,150,140,146,3,48,41,47,75,55,74,66,192,161,166,157,170,158,171,169])). % 62.16/62.08 cnf(7148,plain, % 62.16/62.08 (E(a9,a23)), % 62.16/62.08 inference(scs_inference,[],[6890,106,95,940,165,134])). % 62.16/62.08 cnf(7151,plain, % 62.16/62.08 (E(f27(x71511,a9),f27(x71511,a23))), % 62.16/62.08 inference(scs_inference,[],[6890,106,95,940,165,134,26,23])). % 62.16/62.08 cnf(7155,plain, % 62.16/62.08 (E(f32(a9),f32(a23))), % 62.16/62.08 inference(scs_inference,[],[6890,106,95,940,165,134,26,23,24,136,31])). % 62.16/62.08 cnf(7158,plain, % 62.16/62.08 (E(f33(a9),f33(a23))), % 62.16/62.08 inference(scs_inference,[],[7104,6890,106,95,940,165,134,26,23,24,136,31,159,33])). % 62.16/62.08 cnf(7164,plain, % 62.16/62.08 (E(f26(a9,x71641),f26(a23,x71641))), % 62.16/62.08 inference(scs_inference,[],[7132,7104,6890,106,95,940,165,134,26,23,24,136,31,159,33,164,25,168,12])). % 62.16/62.08 cnf(7169,plain, % 62.16/62.08 (~E(a19,a23)), % 62.16/62.08 inference(scs_inference,[],[7100,7132,6670,7104,6890,106,95,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2])). % 62.16/62.08 cnf(7172,plain, % 62.16/62.08 (~P18(f30(a12))), % 62.16/62.08 inference(scs_inference,[],[7100,7132,6670,7104,6890,106,129,95,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143])). % 62.16/62.08 cnf(7180,plain, % 62.16/62.08 (~E(a23,f20(a18))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6670,7107,7104,7071,6890,106,129,95,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3])). % 62.16/62.08 cnf(7182,plain, % 62.16/62.08 (P11(f25(f27(x71821,a10)),f27(x71821,a23))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7107,7104,7071,6890,6888,6933,106,293,129,95,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75])). % 62.16/62.08 cnf(7183,plain, % 62.16/62.08 (E(f27(x71831,a10),f27(x71831,a23))), % 62.16/62.08 inference(rename_variables,[],[6888])). % 62.16/62.08 cnf(7190,plain, % 62.16/62.08 (P6(f25(x71901),x71901)), % 62.16/62.08 inference(rename_variables,[],[115])). % 62.16/62.08 cnf(7205,plain, % 62.16/62.08 (P15(f15(a12,a12))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157])). % 62.16/62.08 cnf(7213,plain, % 62.16/62.08 (P7(f15(a12,a12),f30(a12),f30(a12))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169])). % 62.16/62.08 cnf(7215,plain, % 62.16/62.08 (P12(f15(a12,a12))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158])). % 62.16/62.08 cnf(7218,plain, % 62.16/62.08 (E(f14(x72181,a9),f14(x72181,a23))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8])). % 62.16/62.08 cnf(7222,plain, % 62.16/62.08 (E(f5(x72221,x72222,a9),f5(x72221,x72222,a23))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19])). % 62.16/62.08 cnf(7223,plain, % 62.16/62.08 (E(f7(a9,x72231),f7(a23,x72231))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5])). % 62.16/62.08 cnf(7229,plain, % 62.16/62.08 (E(f4(x72291,a9),f4(x72291,a23))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21])). % 62.16/62.08 cnf(7230,plain, % 62.16/62.08 (E(f5(x72301,a9,x72302),f5(x72301,a23,x72302))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18])). % 62.16/62.08 cnf(7233,plain, % 62.16/62.08 (E(f30(a9),f30(a23))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9])). % 62.16/62.08 cnf(7234,plain, % 62.16/62.08 (E(f25(a9),f25(a23))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4])). % 62.16/62.08 cnf(7236,plain, % 62.16/62.08 (E(f4(a9,x72361),f4(a23,x72361))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4,1329,20])). % 62.16/62.08 cnf(7237,plain, % 62.16/62.08 (E(f14(a9,x72371),f14(a23,x72371))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4,1329,20,7])). % 62.16/62.08 cnf(7240,plain, % 62.16/62.08 (E(f5(a9,x72401,x72402),f5(a23,x72401,x72402))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4,1329,20,7,1238,416,17])). % 62.16/62.08 cnf(7241,plain, % 62.16/62.08 (P10(f25(f27(a9,a3)),a23,a3,f27(a9,a3))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4,1329,20,7,1238,416,17,418])). % 62.16/62.08 cnf(7247,plain, % 62.16/62.08 (E(f26(x72471,a9),f26(x72471,a23))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4,1329,20,7,1238,416,17,418,1225,27,29,443,314,13])). % 62.16/62.08 cnf(7248,plain, % 62.16/62.08 (E(f31(a9),f31(a23))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4,1329,20,7,1238,416,17,418,1225,27,29,443,314,13,30])). % 62.16/62.08 cnf(7251,plain, % 62.16/62.08 (E(f7(x72511,a9),f7(x72511,a23))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4,1329,20,7,1238,416,17,418,1225,27,29,443,314,13,30,1201,16,6])). % 62.16/62.08 cnf(7254,plain, % 62.16/62.08 (E(f27(a9,x72541),f27(a23,x72541))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4,1329,20,7,1238,416,17,418,1225,27,29,443,314,13,30,1201,16,6,11,10,22])). % 62.16/62.08 cnf(7259,plain, % 62.16/62.08 (P10(f5(a23,a3,f27(a9,a3)),a9,a3,f27(a9,a3))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4,1329,20,7,1238,416,17,418,1225,27,29,443,314,13,30,1201,16,6,11,10,22,447,32,1353,1111,737])). % 62.16/62.08 cnf(7260,plain, % 62.16/62.08 (P10(f25(f27(a9,a16)),a9,a16,f27(a23,a16))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4,1329,20,7,1238,416,17,418,1225,27,29,443,314,13,30,1201,16,6,11,10,22,447,32,1353,1111,737,429])). % 62.16/62.08 cnf(7263,plain, % 62.16/62.08 (P10(f5(f30(a12),f30(a12),f28(a12)),f30(a12),f30(a12),f28(a12))), % 62.16/62.08 inference(scs_inference,[],[7100,7128,7124,7132,6586,6670,7075,7107,7104,7071,6890,6888,7183,6816,237,6933,6839,106,293,125,115,7190,86,90,88,129,95,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4,1329,20,7,1238,416,17,418,1225,27,29,443,314,13,30,1201,16,6,11,10,22,447,32,1353,1111,737,429,152,187])). % 62.16/62.08 cnf(7268,plain, % 62.16/62.08 (~P25(f31(a19),a1,a1)), % 62.16/62.08 inference(scs_inference,[],[83,7100,7128,7124,7132,6586,6670,6954,7075,7107,7104,7071,6890,6988,6681,6888,7183,6816,237,6605,6609,6607,6603,6933,6839,106,293,125,115,7190,86,89,87,127,91,90,88,129,95,133,131,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4,1329,20,7,1238,416,17,418,1225,27,29,443,314,13,30,1201,16,6,11,10,22,447,32,1353,1111,737,429,152,187,49,48,186])). % 62.16/62.08 cnf(7270,plain, % 62.16/62.08 (~P25(a19,a1,a1)), % 62.16/62.08 inference(scs_inference,[],[83,7100,7128,7124,7132,6586,6670,6954,7075,7107,7104,7071,6890,6613,6988,6681,6888,7183,6816,237,6615,6605,6611,6609,6607,6603,6933,6839,106,293,125,115,7190,86,89,87,127,91,90,88,129,95,133,131,4245,940,165,134,26,23,24,136,31,159,33,164,25,168,12,417,602,167,2,154,143,144,140,141,3,47,75,41,74,66,183,192,228,229,230,166,157,161,170,171,169,158,735,8,15,148,19,5,28,14,392,1178,1213,21,18,1224,1270,9,4,1329,20,7,1238,416,17,418,1225,27,29,443,314,13,30,1201,16,6,11,10,22,447,32,1353,1111,737,429,152,187,49,48,186,231])). % 62.16/62.08 cnf(7287,plain, % 62.16/62.08 (E(f7(x72871,a9),f7(x72871,a23))), % 62.16/62.08 inference(rename_variables,[],[7251])). % 62.16/62.08 cnf(7289,plain, % 62.16/62.08 (E(f7(a9,x72891),f7(a23,x72891))), % 62.16/62.08 inference(rename_variables,[],[7223])). % 62.16/62.08 cnf(7291,plain, % 62.16/62.08 (E(f27(a9,x72911),f27(a23,x72911))), % 62.16/62.08 inference(rename_variables,[],[7254])). % 62.16/62.08 cnf(7295,plain, % 62.16/62.08 (E(f7(a9,x72951),f7(a23,x72951))), % 62.16/62.08 inference(rename_variables,[],[7223])). % 62.16/62.08 cnf(7297,plain, % 62.16/62.08 (E(f7(a9,x72971),f7(a23,x72971))), % 62.16/62.08 inference(rename_variables,[],[7223])). % 62.16/62.08 cnf(7301,plain, % 62.16/62.08 (E(f27(a9,x73011),f27(a23,x73011))), % 62.16/62.08 inference(rename_variables,[],[7254])). % 62.16/62.08 cnf(7328,plain, % 62.16/62.08 (~P11(f27(a23,a3),f5(a9,a3,f27(a23,a3)))), % 62.16/62.08 inference(scs_inference,[],[7270,6569,7148,7215,7205,7213,7240,7164,7218,7223,7289,7295,7297,7229,7236,7237,7247,7251,7287,7254,7291,6684,6922,7263,6749,7260,998,6845,6805,6933,6877,1341,940,1198,1317,1199,734,1285,603,1301,430,471,1239,1211,1123,1372,159,168,602,417,167,2,69,70,49,141,140,3,47,75])). % 62.16/62.08 cnf(7338,plain, % 62.16/62.08 (~P11(a19,f28(a1))), % 62.16/62.08 inference(scs_inference,[],[83,7270,6569,7148,7215,7205,7213,7240,7151,7164,7218,7223,7289,7295,7297,7229,7236,7237,7247,7251,7287,7254,7291,7301,6684,7172,6922,7263,6749,7260,7108,998,6845,6805,6613,6615,6611,6933,6839,1018,89,87,127,91,4245,6877,1341,940,1198,1317,1199,734,1285,603,1301,430,471,1239,1211,1123,1372,159,168,602,417,167,2,69,70,49,141,140,3,47,75,41,74,192,185])). % 62.16/62.08 cnf(7356,plain, % 62.16/62.08 (~P25(f31(a19),a1,f29(f30(a1),f33(a1)))), % 62.16/62.08 inference(scs_inference,[],[7268,7180,6751,6673,7155,1031,6805,940,159,168,167,417,602,2,69,70])). % 62.16/62.08 cnf(7368,plain, % 62.16/62.08 (P5(x73681,x73681)), % 62.16/62.08 inference(rename_variables,[],[114])). % 62.16/62.08 cnf(7371,plain, % 62.16/62.08 (~P6(f27(x73711,a23),f32(a10))), % 62.16/62.08 inference(scs_inference,[],[7268,7091,7095,7180,6751,6673,7155,7182,1031,985,979,6805,1015,114,7368,108,940,159,168,167,417,602,2,69,70,140,141,37,78,40,82,81,155])). % 62.16/62.08 cnf(7379,plain, % 62.16/62.09 (E(f25(a9),f25(a10))), % 62.16/62.09 inference(scs_inference,[],[7268,7091,7095,7180,6751,6673,7155,7158,7234,7182,1031,993,985,979,980,6805,590,1015,114,7368,108,995,940,159,168,167,417,602,2,69,70,140,141,37,78,40,82,81,155,36,77,72,3])). % 62.16/62.09 cnf(7380,plain, % 62.16/62.09 (~P6(f27(x73801,a9),f32(a10))), % 62.16/62.09 inference(scs_inference,[],[7268,7091,7095,7180,6751,6673,7155,7158,7234,7182,1031,7151,993,985,979,980,6805,590,1015,114,7368,108,995,940,159,168,167,417,602,2,69,70,140,141,37,78,40,82,81,155,36,77,72,3,65])). % 62.16/62.09 cnf(7382,plain, % 62.16/62.09 (P11(f25(f27(x73821,a9)),f27(x73821,a23))), % 62.16/62.09 inference(scs_inference,[],[7268,6803,7091,7095,7180,6751,6673,7155,7158,7234,7182,1031,7151,993,985,979,980,6805,590,6592,1015,114,7368,108,293,995,940,159,168,167,417,602,2,69,70,140,141,37,78,40,82,81,155,36,77,72,3,65,47,75])). % 62.16/62.09 cnf(7416,plain, % 62.16/62.09 (~P11(f27(x74161,a23),f32(a10))), % 62.16/62.09 inference(scs_inference,[],[7371,7380,7379,6971,6793,6674,1033,941,940,159,168,318,167,602,417,2,156])). % 62.16/62.09 cnf(7417,plain, % 62.16/62.09 (P6(x74171,f32(x74171))), % 62.16/62.09 inference(rename_variables,[],[941])). % 62.16/62.09 cnf(7419,plain, % 62.16/62.09 (P10(f25(f27(a9,a3)),a23,a3,f27(a23,a3))), % 62.16/62.09 inference(scs_inference,[],[7371,7380,7379,6971,6793,6674,7241,1033,7254,941,940,159,168,318,167,602,417,2,156,51])). % 62.16/62.09 cnf(7420,plain, % 62.16/62.09 (E(f27(a9,x74201),f27(a23,x74201))), % 62.16/62.09 inference(rename_variables,[],[7254])). % 62.16/62.09 cnf(7431,plain, % 62.16/62.09 (P8(f27(a23,f25(a10)),a9,f25(a23))), % 62.16/62.09 inference(scs_inference,[],[7169,7371,7380,6807,7379,6971,6793,6674,6743,7241,7233,1033,6572,6588,116,7254,7420,982,7071,6933,941,7417,995,118,940,159,168,318,167,602,417,2,156,51,140,141,39,3,65,47,41])). % 62.16/62.09 cnf(7432,plain, % 62.16/62.09 (E(f27(a9,x74321),f27(a23,x74321))), % 62.16/62.09 inference(rename_variables,[],[7254])). % 62.16/62.09 cnf(7441,plain, % 62.16/62.09 (P8(f27(x74411,x74412),x74411,x74412)), % 62.16/62.09 inference(rename_variables,[],[125])). % 62.16/62.09 cnf(7444,plain, % 62.16/62.09 (P8(f27(x74441,x74442),x74441,x74442)), % 62.16/62.09 inference(rename_variables,[],[125])). % 62.16/62.09 cnf(7453,plain, % 62.16/62.09 (P11(f5(f30(a1),f30(a1),f28(a1)),f28(a1))+~E(x74531,f29(f30(a1),f33(a1)))), % 62.16/62.09 inference(scs_inference,[],[7169,7371,7380,6807,7379,6971,6793,6674,6743,7241,7259,7328,7356,7233,1033,6572,6588,6684,116,7254,7420,7432,6789,982,7071,6795,6933,6805,6601,941,7417,125,7441,7444,115,995,131,118,584,940,159,168,318,167,602,417,2,156,51,140,141,39,3,65,47,41,74,66,193,205,204,192,70,69,146,149])). % 62.16/62.09 cnf(7467,plain, % 62.16/62.09 (P11(f5(f30(a1),f30(a1),f28(a1)),f28(a1))), % 62.16/62.09 inference(equality_inference,[],[7453])). % 62.16/62.09 cnf(7486,plain, % 62.16/62.09 (P15(f31(a13))), % 62.16/62.09 inference(scs_inference,[],[6753,7043,6921,7431,7248,100,103,104,99,940,159,168,167,417,602,2,141,140])). % 62.16/62.09 cnf(7488,plain, % 62.16/62.09 (~P6(a19,f28(a1))), % 62.16/62.09 inference(scs_inference,[],[7338,6753,7043,6921,7431,7248,100,103,104,6684,99,940,159,168,167,417,602,2,141,140,149])). % 62.16/62.09 cnf(7490,plain, % 62.16/62.09 (E(f5(x74901,a9,a9),f5(x74901,a23,a23))), % 62.16/62.09 inference(scs_inference,[],[7338,6753,7043,6921,7431,7248,7222,7230,100,103,104,6684,99,940,159,168,167,417,602,2,141,140,149,3])). % 62.16/62.09 cnf(7493,plain, % 62.16/62.09 (~E(f28(a1),a11)), % 62.16/62.09 inference(scs_inference,[],[7338,6753,7043,6921,7467,7431,7248,7222,7230,100,103,104,6684,99,327,940,159,168,167,417,602,2,141,140,149,3,75])). % 62.16/62.09 cnf(7495,plain, % 62.16/62.09 (~P6(f27(x74951,a11),f32(a10))), % 62.16/62.09 inference(scs_inference,[],[7338,6753,7043,6921,7467,7431,7248,7222,7230,100,7371,6653,103,104,6684,99,327,940,159,168,167,417,602,2,141,140,149,3,75,65])). % 62.16/62.09 cnf(7502,plain, % 62.16/62.09 (P6(f25(f27(a9,a3)),f27(a23,a3))), % 62.16/62.09 inference(scs_inference,[],[7338,7416,6843,6753,7043,6921,7467,7419,7431,7248,7222,7230,100,7371,7380,6653,103,104,6684,99,327,6592,941,125,131,940,159,168,167,417,602,2,141,140,149,3,75,65,47,74,66,193])). % 62.16/62.09 cnf(7544,plain, % 62.16/62.09 (E(f27(a10,x75441),f27(a23,x75441))), % 62.16/62.09 inference(rename_variables,[],[6972])). % 62.16/62.09 cnf(7548,plain, % 62.16/62.09 (E(f5(x75481,a9,a9),f5(x75481,a23,a23))), % 62.16/62.09 inference(rename_variables,[],[7490])). % 62.16/62.09 cnf(7556,plain, % 62.16/62.09 ($false), % 62.16/62.09 inference(scs_inference,[],[7490,7548,7495,6577,7084,7486,7083,7488,7493,6986,6965,7502,6771,7112,7116,7382,7240,6972,7544,1022,6779,6933,6601,242,115,126,584,940,159,168,318,167,602,417,2,67,140,141,149,75,3,65,47,74,66,193]), % 62.16/62.09 ['proof']). % 62.16/62.09 % SZS output end Proof % 62.16/62.09 % Total time :61.410000s %------------------------------------------------------------------------------