%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ALG220+1 : TPTP v8.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n013.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 03:41:04 EDT 2024 % Result : Theorem 78.05s 78.40s % Output : CNFRefutation 78.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : ALG220+1 : TPTP v8.2.0. Released v3.4.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.14/0.34 % Computer : n013.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Jun 19 16:58:24 EDT 2024 % 0.14/0.34 % CPUTime : % 0.56/0.59 start to proof:theBenchmark % 78.00/78.37 %------------------------------------------- % 78.00/78.37 % File :CSE---1.7 % 78.00/78.37 % Problem :theBenchmark % 78.00/78.37 % Transform :cnf % 78.00/78.37 % Format :tptp:raw % 78.00/78.37 % Command :java -jar mcs_scs.jar %d %s % 78.00/78.37 % 78.00/78.37 % Result :Theorem 77.360000s % 78.00/78.37 % Output :CNFRefutation 77.360000s % 78.00/78.37 %------------------------------------------- % 78.00/78.38 %------------------------------------------------------------------------------ % 78.00/78.38 % File : ALG220+1 : TPTP v8.2.0. Released v3.4.0. % 78.00/78.38 % Domain : General Algebra % 78.00/78.38 % Problem : Linear Independence in Right Module over Domain T16 % 78.00/78.38 % Version : [Urb08] axioms : Especial. % 78.00/78.38 % English : % 78.00/78.38 % 78.00/78.38 % Refs : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 78.00/78.38 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 78.00/78.38 % Source : [Urb08] % 78.00/78.38 % Names : t16_rmod_5 [Urb08] % 78.00/78.38 % 78.00/78.38 % Status : Theorem % 78.00/78.38 % Rating : 0.28 v8.2.0, 0.25 v8.1.0, 0.31 v7.4.0, 0.20 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.22 v7.0.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.37 v6.0.0, 0.30 v5.5.0, 0.41 v5.4.0, 0.43 v5.3.0, 0.48 v5.2.0, 0.30 v5.1.0, 0.33 v5.0.0, 0.42 v4.1.0, 0.43 v4.0.1, 0.39 v4.0.0, 0.42 v3.7.0, 0.40 v3.5.0, 0.42 v3.4.0 % 78.00/78.38 % Syntax : Number of formulae : 69 ( 22 unt; 0 def) % 78.00/78.38 % Number of atoms : 365 ( 12 equ) % 78.00/78.38 % Maximal formula atoms : 29 ( 5 avg) % 78.00/78.38 % Number of connectives : 345 ( 49 ~; 1 |; 237 &) % 78.00/78.38 % ( 2 <=>; 56 =>; 0 <=; 0 <~>) % 78.00/78.38 % Maximal formula depth : 25 ( 6 avg) % 78.00/78.38 % Maximal term depth : 3 ( 1 avg) % 78.00/78.38 % Number of predicates : 35 ( 33 usr; 1 prp; 0-3 aty) % 78.00/78.39 % Number of functors : 9 ( 9 usr; 1 con; 0-5 aty) % 78.00/78.39 % Number of variables : 128 ( 104 !; 24 ?) % 78.00/78.39 % SPC : FOF_THM_RFO_SEQ % 78.00/78.39 % 78.00/78.39 % Comments : Normal version: includes the axioms (which may be theorems from % 78.00/78.39 % other articles) and background that are possibly necessary. % 78.00/78.39 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 78.00/78.39 % : The problem encoding is based on set theory. % 78.00/78.39 %------------------------------------------------------------------------------ % 78.00/78.39 fof(t16_rmod_5,conjecture, % 78.00/78.39 ! [A] : % 78.00/78.39 ( ( ~ v3_struct_0(A) % 78.00/78.39 & v3_rlvect_1(A) % 78.00/78.39 & v4_rlvect_1(A) % 78.00/78.39 & v5_rlvect_1(A) % 78.00/78.39 & v6_rlvect_1(A) % 78.00/78.39 & v4_group_1(A) % 78.00/78.39 & v7_group_1(A) % 78.00/78.39 & v6_vectsp_1(A) % 78.00/78.39 & v7_vectsp_1(A) % 78.00/78.39 & v8_vectsp_1(A) % 78.00/78.39 & ~ v10_vectsp_1(A) % 78.00/78.39 & v2_vectsp_2(A) % 78.00/78.39 & l3_vectsp_1(A) ) % 78.00/78.39 => ! [B] : % 78.00/78.39 ( ( ~ v3_struct_0(B) % 78.00/78.39 & v3_rlvect_1(B) % 78.00/78.39 & v4_rlvect_1(B) % 78.00/78.39 & v5_rlvect_1(B) % 78.00/78.39 & v6_rlvect_1(B) % 78.00/78.39 & v3_vectsp_2(B,A) % 78.00/78.39 & v5_vectsp_2(B,A) % 78.00/78.39 & l1_vectsp_2(B,A) ) % 78.00/78.39 => ! [C] : % 78.00/78.39 ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) % 78.00/78.39 => ! [D] : % 78.00/78.39 ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) % 78.00/78.39 => ( ( k1_rmod_5(A,B,C) = B % 78.00/78.39 & r1_tarski(C,D) ) % 78.00/78.39 => k1_rmod_5(A,B,D) = B ) ) ) ) ) ). % 78.00/78.39 % 78.00/78.39 fof(abstractness_v3_vectsp_2,axiom, % 78.00/78.39 ! [A,B] : % 78.00/78.39 ( ( l1_struct_0(A) % 78.00/78.39 & l1_vectsp_2(B,A) ) % 78.00/78.39 => ( v3_vectsp_2(B,A) % 78.00/78.39 => B = g1_vectsp_2(A,u1_struct_0(B),u1_rlvect_1(B),u2_struct_0(B),u1_vectsp_2(A,B)) ) ) ). % 78.00/78.39 % 78.00/78.39 fof(antisymmetry_r2_hidden,axiom, % 78.00/78.39 ! [A,B] : % 78.00/78.39 ( r2_hidden(A,B) % 78.00/78.39 => ~ r2_hidden(B,A) ) ). % 78.00/78.39 % 78.00/78.39 fof(cc1_relset_1,axiom, % 78.00/78.39 ! [A,B,C] : % 78.00/78.39 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 78.00/78.39 => v1_relat_1(C) ) ). % 78.00/78.39 % 78.00/78.39 fof(cc2_vectsp_2,axiom, % 78.00/78.39 ! [A] : % 78.00/78.39 ( l1_vectsp_1(A) % 78.00/78.39 => ( ( ~ v3_struct_0(A) % 78.00/78.39 & v7_group_1(A) % 78.00/78.39 & v8_vectsp_1(A) ) % 78.00/78.39 => ( ~ v3_struct_0(A) % 78.00/78.39 & v2_group_1(A) % 78.00/78.39 & v6_vectsp_1(A) % 78.00/78.39 & v8_vectsp_1(A) ) ) ) ). % 78.00/78.39 % 78.00/78.39 fof(cc3_vectsp_2,axiom, % 78.00/78.39 ! [A] : % 78.00/78.39 ( l1_vectsp_1(A) % 78.00/78.39 => ( ( ~ v3_struct_0(A) % 78.00/78.39 & v7_group_1(A) % 78.00/78.39 & v6_vectsp_1(A) ) % 78.00/78.39 => ( ~ v3_struct_0(A) % 78.00/78.39 & v2_group_1(A) % 78.00/78.39 & v6_vectsp_1(A) % 78.00/78.39 & v8_vectsp_1(A) ) ) ) ). % 78.00/78.39 % 78.00/78.39 fof(dt_g1_vectsp_2,axiom, % 78.00/78.39 ! [A,B,C,D,E] : % 78.00/78.39 ( ( l1_struct_0(A) % 78.00/78.39 & v1_funct_1(C) % 78.00/78.39 & v1_funct_2(C,k2_zfmisc_1(B,B),B) % 78.00/78.39 & m1_relset_1(C,k2_zfmisc_1(B,B),B) % 78.00/78.39 & m1_subset_1(D,B) % 78.00/78.39 & v1_funct_1(E) % 78.00/78.39 & v1_funct_2(E,k2_zfmisc_1(B,u1_struct_0(A)),B) % 78.00/78.39 & m1_relset_1(E,k2_zfmisc_1(B,u1_struct_0(A)),B) ) % 78.00/78.39 => ( v3_vectsp_2(g1_vectsp_2(A,B,C,D,E),A) % 78.00/78.39 & l1_vectsp_2(g1_vectsp_2(A,B,C,D,E),A) ) ) ). % 78.00/78.39 % 78.00/78.39 fof(dt_k1_rmod_5,axiom, % 78.00/78.39 ! [A,B,C] : % 78.00/78.39 ( ( ~ v3_struct_0(A) % 78.00/78.39 & v3_rlvect_1(A) % 78.00/78.39 & v4_rlvect_1(A) % 78.00/78.39 & v5_rlvect_1(A) % 78.00/78.39 & v6_rlvect_1(A) % 78.00/78.39 & v4_group_1(A) % 78.00/78.39 & v7_group_1(A) % 78.00/78.39 & v6_vectsp_1(A) % 78.00/78.39 & v7_vectsp_1(A) % 78.00/78.39 & v8_vectsp_1(A) % 78.00/78.39 & ~ v10_vectsp_1(A) % 78.00/78.39 & v2_vectsp_2(A) % 78.00/78.39 & l3_vectsp_1(A) % 78.00/78.39 & ~ v3_struct_0(B) % 78.00/78.39 & v3_rlvect_1(B) % 78.00/78.39 & v4_rlvect_1(B) % 78.00/78.39 & v5_rlvect_1(B) % 78.00/78.39 & v6_rlvect_1(B) % 78.00/78.39 & v5_vectsp_2(B,A) % 78.00/78.39 & l1_vectsp_2(B,A) % 78.00/78.39 & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) ) % 78.00/78.39 => ( v3_vectsp_2(k1_rmod_5(A,B,C),A) % 78.00/78.39 & m1_rmod_2(k1_rmod_5(A,B,C),A,B) ) ) ). % 78.00/78.39 % 78.00/78.39 fof(dt_k1_xboole_0,axiom, % 78.00/78.39 $true ). % 78.00/78.39 % 78.00/78.39 fof(dt_k1_zfmisc_1,axiom, % 78.00/78.39 $true ). % 78.00/78.39 % 78.00/78.39 fof(dt_k2_zfmisc_1,axiom, % 78.00/78.39 $true ). % 78.00/78.39 % 78.00/78.39 fof(dt_l1_group_1,axiom, % 78.00/78.39 ! [A] : % 78.00/78.39 ( l1_group_1(A) % 78.00/78.39 => l1_struct_0(A) ) ). % 78.00/78.39 % 78.00/78.39 fof(dt_l1_rlvect_1,axiom, % 78.00/78.39 ! [A] : % 78.00/78.39 ( l1_rlvect_1(A) % 78.00/78.39 => l2_struct_0(A) ) ). % 78.00/78.39 % 78.00/78.39 fof(dt_l1_struct_0,axiom, % 78.00/78.39 $true ). % 78.00/78.39 % 78.00/78.39 fof(dt_l1_vectsp_1,axiom, % 78.00/78.39 ! [A] : % 78.00/78.39 ( l1_vectsp_1(A) % 78.00/78.39 => l1_group_1(A) ) ). % 78.00/78.39 % 78.00/78.39 fof(dt_l1_vectsp_2,axiom, % 78.00/78.39 ! [A] : % 78.00/78.39 ( l1_struct_0(A) % 78.00/78.39 => ! [B] : % 78.00/78.39 ( l1_vectsp_2(B,A) % 78.00/78.39 => l1_rlvect_1(B) ) ) ). % 78.00/78.39 % 78.00/78.39 fof(dt_l2_struct_0,axiom, % 78.00/78.39 ! [A] : % 78.00/78.39 ( l2_struct_0(A) % 78.00/78.39 => l1_struct_0(A) ) ). % 78.00/78.39 % 78.00/78.39 fof(dt_l2_vectsp_1,axiom, % 78.00/78.39 ! [A] : % 78.00/78.39 ( l2_vectsp_1(A) % 78.00/78.39 => ( l1_vectsp_1(A) % 78.00/78.39 & l2_struct_0(A) ) ) ). % 78.00/78.39 % 78.00/78.39 fof(dt_l3_vectsp_1,axiom, % 78.00/78.39 ! [A] : % 78.00/78.39 ( l3_vectsp_1(A) % 78.00/78.39 => ( l1_rlvect_1(A) % 78.00/78.39 & l2_vectsp_1(A) ) ) ). % 78.00/78.39 % 78.00/78.39 fof(dt_m1_relset_1,axiom, % 78.00/78.39 $true ). % 78.00/78.39 % 78.00/78.39 fof(dt_m1_rmod_2,axiom, % 78.00/78.39 ! [A,B] : % 78.00/78.39 ( ( ~ v3_struct_0(A) % 78.00/78.39 & v3_rlvect_1(A) % 78.00/78.39 & v4_rlvect_1(A) % 78.00/78.39 & v5_rlvect_1(A) % 78.00/78.39 & v6_rlvect_1(A) % 78.00/78.39 & v4_group_1(A) % 78.00/78.39 & v6_vectsp_1(A) % 78.00/78.39 & v7_vectsp_1(A) % 78.00/78.39 & v8_vectsp_1(A) % 78.00/78.39 & l3_vectsp_1(A) % 78.00/78.39 & ~ v3_struct_0(B) % 78.00/78.39 & v3_rlvect_1(B) % 78.00/78.39 & v4_rlvect_1(B) % 78.00/78.39 & v5_rlvect_1(B) % 78.00/78.39 & v6_rlvect_1(B) % 78.00/78.39 & v5_vectsp_2(B,A) % 78.00/78.39 & l1_vectsp_2(B,A) ) % 78.00/78.39 => ! [C] : % 78.00/78.39 ( m1_rmod_2(C,A,B) % 78.00/78.39 => ( ~ v3_struct_0(C) % 78.00/78.39 & v3_rlvect_1(C) % 78.00/78.39 & v4_rlvect_1(C) % 78.00/78.39 & v5_rlvect_1(C) % 78.00/78.39 & v6_rlvect_1(C) % 78.00/78.39 & v5_vectsp_2(C,A) % 78.00/78.39 & l1_vectsp_2(C,A) ) ) ) ). % 78.00/78.39 % 78.00/78.39 fof(dt_m1_subset_1,axiom, % 78.05/78.39 $true ). % 78.05/78.39 % 78.05/78.39 fof(dt_m2_relset_1,axiom, % 78.05/78.39 ! [A,B,C] : % 78.05/78.39 ( m2_relset_1(C,A,B) % 78.05/78.39 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 78.05/78.39 % 78.05/78.39 fof(dt_u1_rlvect_1,axiom, % 78.05/78.39 ! [A] : % 78.05/78.39 ( l1_rlvect_1(A) % 78.05/78.39 => ( v1_funct_1(u1_rlvect_1(A)) % 78.05/78.39 & v1_funct_2(u1_rlvect_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 78.05/78.39 & m2_relset_1(u1_rlvect_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 78.05/78.39 % 78.05/78.39 fof(dt_u1_struct_0,axiom, % 78.05/78.39 $true ). % 78.05/78.39 % 78.05/78.39 fof(dt_u1_vectsp_2,axiom, % 78.05/78.39 ! [A,B] : % 78.05/78.39 ( ( l1_struct_0(A) % 78.05/78.39 & l1_vectsp_2(B,A) ) % 78.05/78.39 => ( v1_funct_1(u1_vectsp_2(A,B)) % 78.05/78.39 & v1_funct_2(u1_vectsp_2(A,B),k2_zfmisc_1(u1_struct_0(B),u1_struct_0(A)),u1_struct_0(B)) % 78.05/78.39 & m2_relset_1(u1_vectsp_2(A,B),k2_zfmisc_1(u1_struct_0(B),u1_struct_0(A)),u1_struct_0(B)) ) ) ). % 78.05/78.39 % 78.05/78.39 fof(dt_u2_struct_0,axiom, % 78.05/78.39 ! [A] : % 78.05/78.39 ( l2_struct_0(A) % 78.05/78.39 => m1_subset_1(u2_struct_0(A),u1_struct_0(A)) ) ). % 78.05/78.40 % 78.05/78.40 fof(existence_l1_group_1,axiom, % 78.05/78.40 ? [A] : l1_group_1(A) ). % 78.05/78.40 % 78.05/78.40 fof(existence_l1_rlvect_1,axiom, % 78.05/78.40 ? [A] : l1_rlvect_1(A) ). % 78.05/78.40 % 78.05/78.40 fof(existence_l1_struct_0,axiom, % 78.05/78.40 ? [A] : l1_struct_0(A) ). % 78.05/78.40 % 78.05/78.40 fof(existence_l1_vectsp_1,axiom, % 78.05/78.40 ? [A] : l1_vectsp_1(A) ). % 78.05/78.40 % 78.05/78.40 fof(existence_l1_vectsp_2,axiom, % 78.05/78.40 ! [A] : % 78.05/78.40 ( l1_struct_0(A) % 78.05/78.40 => ? [B] : l1_vectsp_2(B,A) ) ). % 78.05/78.40 % 78.05/78.40 fof(existence_l2_struct_0,axiom, % 78.05/78.40 ? [A] : l2_struct_0(A) ). % 78.05/78.40 % 78.05/78.40 fof(existence_l2_vectsp_1,axiom, % 78.05/78.40 ? [A] : l2_vectsp_1(A) ). % 78.05/78.40 % 78.05/78.40 fof(existence_l3_vectsp_1,axiom, % 78.05/78.40 ? [A] : l3_vectsp_1(A) ). % 78.05/78.40 % 78.05/78.40 fof(existence_m1_relset_1,axiom, % 78.05/78.40 ! [A,B] : % 78.05/78.40 ? [C] : m1_relset_1(C,A,B) ). % 78.05/78.40 % 78.05/78.40 fof(existence_m1_rmod_2,axiom, % 78.05/78.40 ! [A,B] : % 78.05/78.40 ( ( ~ v3_struct_0(A) % 78.05/78.40 & v3_rlvect_1(A) % 78.05/78.40 & v4_rlvect_1(A) % 78.05/78.40 & v5_rlvect_1(A) % 78.05/78.40 & v6_rlvect_1(A) % 78.05/78.40 & v4_group_1(A) % 78.05/78.40 & v6_vectsp_1(A) % 78.05/78.40 & v7_vectsp_1(A) % 78.05/78.40 & v8_vectsp_1(A) % 78.05/78.40 & l3_vectsp_1(A) % 78.05/78.40 & ~ v3_struct_0(B) % 78.05/78.40 & v3_rlvect_1(B) % 78.05/78.40 & v4_rlvect_1(B) % 78.05/78.40 & v5_rlvect_1(B) % 78.05/78.40 & v6_rlvect_1(B) % 78.05/78.40 & v5_vectsp_2(B,A) % 78.05/78.40 & l1_vectsp_2(B,A) ) % 78.05/78.40 => ? [C] : m1_rmod_2(C,A,B) ) ). % 78.05/78.40 % 78.05/78.40 fof(existence_m1_subset_1,axiom, % 78.05/78.40 ! [A] : % 78.05/78.40 ? [B] : m1_subset_1(B,A) ). % 78.05/78.40 % 78.05/78.40 fof(existence_m2_relset_1,axiom, % 78.05/78.40 ! [A,B] : % 78.05/78.40 ? [C] : m2_relset_1(C,A,B) ). % 78.05/78.40 % 78.05/78.40 fof(fc1_struct_0,axiom, % 78.05/78.40 ! [A] : % 78.05/78.40 ( ( ~ v3_struct_0(A) % 78.05/78.40 & l1_struct_0(A) ) % 78.05/78.40 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 78.05/78.40 % 78.05/78.40 fof(fc1_subset_1,axiom, % 78.05/78.40 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 78.05/78.40 % 78.05/78.40 fof(fc1_vectsp_2,axiom, % 78.05/78.40 ! [A,B,C,D,E] : % 78.05/78.40 ( ( l1_struct_0(A) % 78.05/78.40 & ~ v1_xboole_0(B) % 78.05/78.40 & v1_funct_1(C) % 78.05/78.40 & v1_funct_2(C,k2_zfmisc_1(B,B),B) % 78.05/78.40 & m1_relset_1(C,k2_zfmisc_1(B,B),B) % 78.05/78.40 & m1_subset_1(D,B) % 78.05/78.40 & v1_funct_1(E) % 78.05/78.40 & v1_funct_2(E,k2_zfmisc_1(B,u1_struct_0(A)),B) % 78.05/78.40 & m1_relset_1(E,k2_zfmisc_1(B,u1_struct_0(A)),B) ) % 78.05/78.40 => ( ~ v3_struct_0(g1_vectsp_2(A,B,C,D,E)) % 78.05/78.40 & v3_vectsp_2(g1_vectsp_2(A,B,C,D,E),A) ) ) ). % 78.05/78.40 % 78.05/78.40 fof(fc1_xboole_0,axiom, % 78.05/78.40 v1_xboole_0(k1_xboole_0) ). % 78.05/78.40 % 78.05/78.40 fof(fc4_subset_1,axiom, % 78.05/78.40 ! [A,B] : % 78.05/78.40 ( ( ~ v1_xboole_0(A) % 78.05/78.40 & ~ v1_xboole_0(B) ) % 78.05/78.40 => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ). % 78.05/78.40 % 78.05/78.40 fof(free_g1_vectsp_2,axiom, % 78.05/78.40 ! [A,B,C,D,E] : % 78.05/78.40 ( ( l1_struct_0(A) % 78.05/78.40 & v1_funct_1(C) % 78.05/78.40 & v1_funct_2(C,k2_zfmisc_1(B,B),B) % 78.05/78.40 & m1_relset_1(C,k2_zfmisc_1(B,B),B) % 78.05/78.40 & m1_subset_1(D,B) % 78.05/78.40 & v1_funct_1(E) % 78.05/78.40 & v1_funct_2(E,k2_zfmisc_1(B,u1_struct_0(A)),B) % 78.05/78.40 & m1_relset_1(E,k2_zfmisc_1(B,u1_struct_0(A)),B) ) % 78.05/78.40 => ! [F,G,H,I,J] : % 78.05/78.40 ( g1_vectsp_2(A,B,C,D,E) = g1_vectsp_2(F,G,H,I,J) % 78.05/78.40 => ( A = F % 78.05/78.40 & B = G % 78.05/78.40 & C = H % 78.05/78.40 & D = I % 78.05/78.40 & E = J ) ) ) ). % 78.05/78.40 % 78.05/78.40 fof(rc13_vectsp_2,axiom, % 78.05/78.40 ! [A] : % 78.05/78.40 ( ( ~ v3_struct_0(A) % 78.05/78.40 & v3_rlvect_1(A) % 78.05/78.40 & v4_rlvect_1(A) % 78.05/78.40 & v5_rlvect_1(A) % 78.05/78.40 & v6_rlvect_1(A) % 78.05/78.40 & v4_group_1(A) % 78.05/78.40 & v6_vectsp_1(A) % 78.05/78.40 & v7_vectsp_1(A) % 78.05/78.40 & v8_vectsp_1(A) % 78.05/78.40 & l3_vectsp_1(A) ) % 78.05/78.40 => ? [B] : % 78.05/78.40 ( l1_vectsp_2(B,A) % 78.05/78.40 & ~ v3_struct_0(B) % 78.05/78.40 & v3_rlvect_1(B) % 78.05/78.40 & v4_rlvect_1(B) % 78.05/78.40 & v5_rlvect_1(B) % 78.05/78.40 & v6_rlvect_1(B) % 78.05/78.40 & v3_vectsp_2(B,A) ) ) ). % 78.05/78.40 % 78.05/78.40 fof(rc16_vectsp_2,axiom, % 78.05/78.40 ! [A] : % 78.05/78.40 ( ( ~ v3_struct_0(A) % 78.05/78.40 & v3_rlvect_1(A) % 78.05/78.40 & v4_rlvect_1(A) % 78.05/78.40 & v5_rlvect_1(A) % 78.05/78.40 & v6_rlvect_1(A) % 78.05/78.40 & v4_group_1(A) % 78.05/78.40 & v6_vectsp_1(A) % 78.05/78.40 & v7_vectsp_1(A) % 78.05/78.40 & v8_vectsp_1(A) % 78.05/78.40 & l3_vectsp_1(A) ) % 78.05/78.40 => ? [B] : % 78.05/78.40 ( l1_vectsp_2(B,A) % 78.05/78.40 & ~ v3_struct_0(B) % 78.05/78.40 & v3_rlvect_1(B) % 78.05/78.40 & v4_rlvect_1(B) % 78.05/78.40 & v5_rlvect_1(B) % 78.05/78.40 & v6_rlvect_1(B) % 78.05/78.40 & v3_vectsp_2(B,A) % 78.05/78.40 & v5_vectsp_2(B,A) ) ) ). % 78.05/78.40 % 78.05/78.40 fof(rc1_rmod_2,axiom, % 78.05/78.40 ! [A,B] : % 78.05/78.40 ( ( ~ v3_struct_0(A) % 78.05/78.40 & v3_rlvect_1(A) % 78.05/78.40 & v4_rlvect_1(A) % 78.05/78.40 & v5_rlvect_1(A) % 78.05/78.40 & v6_rlvect_1(A) % 78.05/78.40 & v4_group_1(A) % 78.05/78.40 & v6_vectsp_1(A) % 78.05/78.40 & v7_vectsp_1(A) % 78.05/78.40 & v8_vectsp_1(A) % 78.05/78.40 & l3_vectsp_1(A) % 78.05/78.40 & ~ v3_struct_0(B) % 78.05/78.40 & v3_rlvect_1(B) % 78.05/78.40 & v4_rlvect_1(B) % 78.05/78.40 & v5_rlvect_1(B) % 78.05/78.40 & v6_rlvect_1(B) % 78.05/78.40 & v5_vectsp_2(B,A) % 78.05/78.40 & l1_vectsp_2(B,A) ) % 78.05/78.40 => ? [C] : % 78.05/78.40 ( m1_rmod_2(C,A,B) % 78.05/78.40 & ~ v3_struct_0(C) % 78.05/78.40 & v3_rlvect_1(C) % 78.05/78.40 & v4_rlvect_1(C) % 78.05/78.40 & v5_rlvect_1(C) % 78.05/78.40 & v6_rlvect_1(C) % 78.05/78.40 & v3_vectsp_2(C,A) % 78.05/78.40 & v5_vectsp_2(C,A) ) ) ). % 78.05/78.40 % 78.05/78.40 fof(rc1_subset_1,axiom, % 78.05/78.40 ! [A] : % 78.05/78.40 ( ~ v1_xboole_0(A) % 78.05/78.40 => ? [B] : % 78.05/78.40 ( m1_subset_1(B,k1_zfmisc_1(A)) % 78.05/78.40 & ~ v1_xboole_0(B) ) ) ). % 78.05/78.40 % 78.05/78.40 fof(rc1_xboole_0,axiom, % 78.05/78.40 ? [A] : v1_xboole_0(A) ). % 78.05/78.40 % 78.05/78.40 fof(rc2_subset_1,axiom, % 78.05/78.40 ! [A] : % 78.05/78.40 ? [B] : % 78.05/78.40 ( m1_subset_1(B,k1_zfmisc_1(A)) % 78.05/78.40 & v1_xboole_0(B) ) ). % 78.05/78.40 % 78.05/78.40 fof(rc2_xboole_0,axiom, % 78.05/78.40 ? [A] : ~ v1_xboole_0(A) ). % 78.05/78.40 % 78.05/78.40 fof(rc3_struct_0,axiom, % 78.05/78.40 ? [A] : % 78.05/78.40 ( l1_struct_0(A) % 78.05/78.40 & ~ v3_struct_0(A) ) ). % 78.05/78.40 % 78.05/78.40 fof(rc4_struct_0,axiom, % 78.05/78.40 ? [A] : % 78.05/78.40 ( l2_struct_0(A) % 78.05/78.40 & ~ v3_struct_0(A) ) ). % 78.05/78.40 % 78.05/78.40 fof(rc5_struct_0,axiom, % 78.05/78.40 ! [A] : % 78.05/78.40 ( ( ~ v3_struct_0(A) % 78.05/78.40 & l1_struct_0(A) ) % 78.05/78.40 => ? [B] : % 78.05/78.40 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 78.05/78.40 & ~ v1_xboole_0(B) ) ) ). % 78.05/78.40 % 78.05/78.40 fof(rc8_vectsp_2,axiom, % 78.05/78.40 ! [A] : % 78.05/78.40 ( l1_struct_0(A) % 78.05/78.40 => ? [B] : % 78.05/78.40 ( l1_vectsp_2(B,A) % 78.05/78.40 & v3_vectsp_2(B,A) ) ) ). % 78.05/78.40 % 78.05/78.40 fof(rc9_vectsp_2,axiom, % 78.05/78.40 ! [A] : % 78.05/78.40 ( l1_struct_0(A) % 78.05/78.40 => ? [B] : % 78.05/78.40 ( l1_vectsp_2(B,A) % 78.05/78.40 & ~ v3_struct_0(B) ) ) ). % 78.05/78.40 % 78.05/78.40 fof(redefinition_m2_relset_1,axiom, % 78.05/78.40 ! [A,B,C] : % 78.05/78.40 ( m2_relset_1(C,A,B) % 78.05/78.40 <=> m1_relset_1(C,A,B) ) ). % 78.05/78.40 % 78.05/78.40 fof(reflexivity_r1_tarski,axiom, % 78.05/78.40 ! [A,B] : r1_tarski(A,A) ). % 78.05/78.40 % 78.05/78.40 fof(t15_rmod_5,axiom, % 78.05/78.40 ! [A] : % 78.05/78.40 ( ( ~ v3_struct_0(A) % 78.05/78.40 & v3_rlvect_1(A) % 78.05/78.40 & v4_rlvect_1(A) % 78.05/78.40 & v5_rlvect_1(A) % 78.05/78.40 & v6_rlvect_1(A) % 78.05/78.40 & v4_group_1(A) % 78.05/78.40 & v7_group_1(A) % 78.05/78.40 & v6_vectsp_1(A) % 78.05/78.40 & v7_vectsp_1(A) % 78.05/78.40 & v8_vectsp_1(A) % 78.05/78.40 & ~ v10_vectsp_1(A) % 78.05/78.40 & v2_vectsp_2(A) % 78.05/78.40 & l3_vectsp_1(A) ) % 78.05/78.40 => ! [B] : % 78.05/78.40 ( ( ~ v3_struct_0(B) % 78.05/78.40 & v3_rlvect_1(B) % 78.05/78.40 & v4_rlvect_1(B) % 78.05/78.40 & v5_rlvect_1(B) % 78.05/78.40 & v6_rlvect_1(B) % 78.05/78.40 & v5_vectsp_2(B,A) % 78.05/78.40 & l1_vectsp_2(B,A) ) % 78.05/78.40 => ! [C] : % 78.05/78.40 ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) % 78.05/78.40 => ! [D] : % 78.05/78.40 ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) % 78.05/78.40 => ( r1_tarski(C,D) % 78.05/78.40 => m1_rmod_2(k1_rmod_5(A,B,C),A,k1_rmod_5(A,B,D)) ) ) ) ) ) ). % 78.05/78.40 % 78.05/78.40 fof(t1_subset,axiom, % 78.05/78.40 ! [A,B] : % 78.05/78.40 ( r2_hidden(A,B) % 78.05/78.40 => m1_subset_1(A,B) ) ). % 78.05/78.40 % 78.05/78.40 fof(t2_subset,axiom, % 78.05/78.40 ! [A,B] : % 78.05/78.40 ( m1_subset_1(A,B) % 78.05/78.40 => ( v1_xboole_0(B) % 78.05/78.40 | r2_hidden(A,B) ) ) ). % 78.05/78.40 % 78.05/78.40 fof(t33_rmod_2,axiom, % 78.05/78.40 ! [A] : % 78.05/78.40 ( ( ~ v3_struct_0(A) % 78.05/78.40 & v3_rlvect_1(A) % 78.05/78.40 & v4_rlvect_1(A) % 78.05/78.40 & v5_rlvect_1(A) % 78.05/78.40 & v6_rlvect_1(A) % 78.05/78.40 & v4_group_1(A) % 78.05/78.40 & v6_vectsp_1(A) % 78.05/78.40 & v7_vectsp_1(A) % 78.05/78.40 & v8_vectsp_1(A) % 78.05/78.40 & l3_vectsp_1(A) ) % 78.05/78.40 => ! [B] : % 78.05/78.40 ( ( ~ v3_struct_0(B) % 78.05/78.40 & v3_rlvect_1(B) % 78.05/78.40 & v4_rlvect_1(B) % 78.05/78.40 & v5_rlvect_1(B) % 78.05/78.40 & v6_rlvect_1(B) % 78.05/78.40 & v3_vectsp_2(B,A) % 78.05/78.40 & v5_vectsp_2(B,A) % 78.05/78.40 & l1_vectsp_2(B,A) ) % 78.05/78.40 => ! [C] : % 78.05/78.40 ( ( ~ v3_struct_0(C) % 78.05/78.40 & v3_rlvect_1(C) % 78.05/78.40 & v4_rlvect_1(C) % 78.05/78.40 & v5_rlvect_1(C) % 78.05/78.40 & v6_rlvect_1(C) % 78.05/78.40 & v3_vectsp_2(C,A) % 78.05/78.40 & v5_vectsp_2(C,A) % 78.05/78.40 & l1_vectsp_2(C,A) ) % 78.05/78.40 => ( ( m1_rmod_2(C,A,B) % 78.05/78.40 & m1_rmod_2(B,A,C) ) % 78.05/78.40 => C = B ) ) ) ) ). % 78.05/78.40 % 78.05/78.40 fof(t3_subset,axiom, % 78.05/78.40 ! [A,B] : % 78.05/78.40 ( m1_subset_1(A,k1_zfmisc_1(B)) % 78.05/78.40 <=> r1_tarski(A,B) ) ). % 78.05/78.40 % 78.05/78.40 fof(t4_subset,axiom, % 78.05/78.40 ! [A,B,C] : % 78.05/78.40 ( ( r2_hidden(A,B) % 78.05/78.40 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 78.05/78.40 => m1_subset_1(A,C) ) ). % 78.05/78.40 % 78.05/78.40 fof(t5_subset,axiom, % 78.05/78.40 ! [A,B,C] : % 78.05/78.40 ~ ( r2_hidden(A,B) % 78.05/78.40 & m1_subset_1(B,k1_zfmisc_1(C)) % 78.05/78.40 & v1_xboole_0(C) ) ). % 78.05/78.40 % 78.05/78.40 fof(t6_boole,axiom, % 78.05/78.40 ! [A] : % 78.05/78.40 ( v1_xboole_0(A) % 78.05/78.40 => A = k1_xboole_0 ) ). % 78.05/78.40 % 78.05/78.40 fof(t7_boole,axiom, % 78.05/78.40 ! [A,B] : % 78.05/78.40 ~ ( r2_hidden(A,B) % 78.05/78.40 & v1_xboole_0(B) ) ). % 78.05/78.40 % 78.05/78.40 fof(t8_boole,axiom, % 78.05/78.40 ! [A,B] : % 78.05/78.40 ~ ( v1_xboole_0(A) % 78.05/78.40 & A != B % 78.05/78.40 & v1_xboole_0(B) ) ). % 78.05/78.40 % 78.05/78.40 %------------------------------------------------------------------------------ % 78.05/78.40 %------------------------------------------- % 78.05/78.40 % Proof found % 78.05/78.40 % SZS status Theorem for theBenchmark % 78.05/78.40 % SZS output start Proof % 78.05/78.40 %ClaNum:220(EqnAxiom:83) % 78.05/78.40 %VarNum:1106(SingletonVarNum:212) % 78.05/78.40 %MaxLitNum:29 % 78.05/78.40 %MaxfuncDepth:2 % 78.05/78.40 %SharedTerms:60 % 78.05/78.40 %goalClause: 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 111 112 113 114 117 118 120 123 124 127 130 % 78.05/78.40 %singleGoalClaCount:26 % 78.05/78.40 [84]P1(a1) % 78.05/78.41 [85]P1(a12) % 78.05/78.41 [86]P23(a1) % 78.05/78.41 [87]P23(a12) % 78.05/78.41 [88]P27(a1) % 78.05/78.41 [89]P27(a12) % 78.05/78.41 [90]P28(a1) % 78.05/78.41 [91]P28(a12) % 78.05/78.41 [92]P24(a1) % 78.05/78.41 [93]P30(a1) % 78.05/78.41 [94]P31(a1) % 78.05/78.41 [95]P32(a1) % 78.05/78.41 [96]P33(a1) % 78.05/78.41 [97]P2(a1) % 78.05/78.41 [98]P3(a1) % 78.05/78.41 [99]P3(a2) % 78.05/78.41 [100]P4(a22) % 78.05/78.41 [101]P4(a13) % 78.05/78.41 [102]P7(a27) % 78.05/78.41 [103]P5(a23) % 78.05/78.41 [104]P6(a26) % 78.05/78.41 [105]P8(a3) % 78.05/78.41 [106]P8(a18) % 78.05/78.41 [107]P10(a4) % 78.05/78.41 [108]P11(a28) % 78.05/78.41 [109]P11(a14) % 78.05/78.41 [111]P25(a12,a1) % 78.05/78.41 [112]P29(a12,a1) % 78.05/78.41 [113]P9(a12,a1) % 78.05/78.41 [114]P12(a24,a25) % 78.05/78.41 [123]~P26(a1) % 78.05/78.41 [124]~P26(a12) % 78.05/78.41 [125]~P26(a13) % 78.05/78.41 [126]~P26(a18) % 78.05/78.41 [127]~P17(a1) % 78.05/78.41 [128]~P11(a17) % 78.05/78.41 [120]E(f29(a1,a12,a24),a12) % 78.05/78.41 [130]~E(f29(a1,a12,a25),a12) % 78.05/78.41 [117]P13(a24,f33(f32(a12))) % 78.05/78.41 [118]P13(a25,f33(f32(a12))) % 78.05/78.41 [115]P12(x1151,x1151) % 78.05/78.41 [110]P11(f16(x1101)) % 78.05/78.41 [116]P13(f5(x1161),x1161) % 78.05/78.41 [119]P13(f16(x1191),f33(x1191)) % 78.05/78.41 [129]~P11(f33(x1291)) % 78.05/78.41 [121]P14(f6(x1211,x1212),x1211,x1212) % 78.05/78.41 [122]P16(f8(x1221,x1222),x1221,x1222) % 78.05/78.41 [131]~P11(x1311)+E(x1311,a28) % 78.05/78.41 [132]~P5(x1321)+P4(x1321) % 78.05/78.41 [133]~P8(x1331)+P4(x1331) % 78.05/78.41 [134]~P10(x1341)+P7(x1341) % 78.05/78.41 [135]~P7(x1351)+P5(x1351) % 78.05/78.41 [136]~P3(x1361)+P6(x1361) % 78.05/78.41 [137]~P6(x1371)+P8(x1371) % 78.05/78.41 [138]~P10(x1381)+P8(x1381) % 78.05/78.41 [139]~P3(x1391)+P10(x1391) % 78.05/78.41 [141]~P6(x1411)+P19(f34(x1411)) % 78.05/78.41 [142]P11(x1421)+~P11(f15(x1421)) % 78.05/78.41 [143]~P4(x1431)+~P26(f19(x1431)) % 78.05/78.41 [144]~P4(x1441)+P25(f20(x1441),x1441) % 78.05/78.41 [145]~P4(x1451)+P9(f30(x1451),x1451) % 78.05/78.41 [146]~P4(x1461)+P9(f20(x1461),x1461) % 78.05/78.41 [147]~P4(x1471)+P9(f19(x1471),x1471) % 78.05/78.41 [155]P11(x1551)+P13(f15(x1551),f33(x1551)) % 78.05/78.41 [156]~P8(x1561)+P13(f36(x1561),f32(x1561)) % 78.05/78.41 [184]~P6(x1841)+P21(f34(x1841),f35(f32(x1841),f32(x1841)),f32(x1841)) % 78.05/78.41 [185]~P6(x1851)+P16(f34(x1851),f35(f32(x1851),f32(x1851)),f32(x1851)) % 78.05/78.41 [150]~P11(x1501)+~P18(x1502,x1501) % 78.05/78.41 [158]~P18(x1581,x1582)+P13(x1581,x1582) % 78.05/78.41 [161]~P18(x1612,x1611)+~P18(x1611,x1612) % 78.05/78.41 [160]~P12(x1601,x1602)+P13(x1601,f33(x1602)) % 78.05/78.41 [162]P12(x1621,x1622)+~P13(x1621,f33(x1622)) % 78.05/78.41 [186]~P16(x1861,x1862,x1863)+P14(x1861,x1862,x1863) % 78.05/78.41 [187]~P14(x1871,x1872,x1873)+P16(x1871,x1872,x1873) % 78.05/78.41 [183]P20(x1831)+~P13(x1831,f33(f35(x1832,x1833))) % 78.05/78.41 [188]~P16(x1881,x1882,x1883)+P13(x1881,f33(f35(x1882,x1883))) % 78.05/78.41 [148]~P4(x1481)+P26(x1481)+~P11(f32(x1481)) % 78.05/78.41 [149]~P4(x1491)+P26(x1491)+~P11(f21(x1491)) % 78.05/78.41 [163]~P4(x1631)+P26(x1631)+P13(f21(x1631),f33(f32(x1631))) % 78.05/78.41 [140]~P11(x1402)+~P11(x1401)+E(x1401,x1402) % 78.05/78.41 [157]~P9(x1571,x1572)+P6(x1571)+~P4(x1572) % 78.05/78.41 [159]~P13(x1592,x1591)+P11(x1591)+P18(x1592,x1591) % 78.05/78.41 [164]P11(x1641)+P11(x1642)+~P11(f35(x1642,x1641)) % 78.05/78.41 [165]~P4(x1651)+~P9(x1652,x1651)+P19(f37(x1651,x1652)) % 78.05/78.41 [189]~P4(x1891)+~P9(x1892,x1891)+P21(f37(x1891,x1892),f35(f32(x1892),f32(x1891)),f32(x1892)) % 78.05/78.41 [190]~P4(x1901)+~P9(x1902,x1901)+P16(f37(x1901,x1902),f35(f32(x1902),f32(x1901)),f32(x1902)) % 78.05/78.41 [166]~P11(x1661)+~P18(x1662,x1663)+~P13(x1663,f33(x1661)) % 78.05/78.41 [167]P13(x1671,x1672)+~P18(x1671,x1673)+~P13(x1673,f33(x1672)) % 78.05/78.41 [211]~P4(x2111)+~P25(x2112,x2111)+~P9(x2112,x2111)+E(f31(x2111,f32(x2112),f34(x2112),f36(x2112),f37(x2111,x2112)),x2112) % 78.05/78.41 [151]P31(x1511)+~P30(x1511)+~P33(x1511)+~P7(x1511)+P26(x1511) % 78.05/78.41 [152]P33(x1521)+~P30(x1521)+~P31(x1521)+~P7(x1521)+P26(x1521) % 78.05/78.41 [153]P22(x1531)+~P30(x1531)+~P31(x1531)+~P7(x1531)+P26(x1531) % 78.05/78.41 [154]P22(x1541)+~P30(x1541)+~P33(x1541)+~P7(x1541)+P26(x1541) % 78.05/78.41 [212]~P4(x2121)+~P19(x2125)+~P19(x2123)+~P13(x2124,x2122)+~P21(x2123,f35(x2122,x2122),x2122)+~P14(x2123,f35(x2122,x2122),x2122)+P25(f31(x2121,x2122,x2123,x2124,x2125),x2121)+~P21(x2125,f35(x2122,f32(x2121)),x2122)+~P14(x2125,f35(x2122,f32(x2121)),x2122) % 78.05/78.41 [213]~P4(x2131)+~P19(x2135)+~P19(x2133)+~P13(x2134,x2132)+~P21(x2133,f35(x2132,x2132),x2132)+~P14(x2133,f35(x2132,x2132),x2132)+P9(f31(x2131,x2132,x2133,x2134,x2135),x2131)+~P21(x2135,f35(x2132,f32(x2131)),x2132)+~P14(x2135,f35(x2132,f32(x2131)),x2132) % 78.05/78.41 [220]P11(x2201)+~P4(x2202)+~P13(x2205,x2201)+~P19(x2203)+~P19(x2204)+~P21(x2204,f35(x2201,x2201),x2201)+~P14(x2204,f35(x2201,x2201),x2201)+~P21(x2203,f35(x2201,f32(x2202)),x2201)+~P14(x2203,f35(x2201,f32(x2202)),x2201)+~P26(f31(x2202,x2201,x2204,x2205,x2203)) % 78.05/78.41 [215]~P4(x2153)+~P19(x2155)+~P19(x2151)+~P13(x2156,x2154)+E(x2151,x2152)+~P21(x2155,f35(x2154,x2154),x2154)+~P14(x2155,f35(x2154,x2154),x2154)+~E(f31(x2153,x2154,x2155,x2156,x2151),f31(x2157,x2158,x2159,x21510,x2152))+~P21(x2151,f35(x2154,f32(x2153)),x2154)+~P14(x2151,f35(x2154,f32(x2153)),x2154) % 78.05/78.41 [216]~P4(x2163)+~P19(x2166)+~P19(x2165)+~P13(x2161,x2164)+E(x2161,x2162)+~P21(x2165,f35(x2164,x2164),x2164)+~P14(x2165,f35(x2164,x2164),x2164)+~E(f31(x2163,x2164,x2165,x2161,x2166),f31(x2167,x2168,x2169,x2162,x21610))+~P21(x2166,f35(x2164,f32(x2163)),x2164)+~P14(x2166,f35(x2164,f32(x2163)),x2164) % 78.05/78.41 [217]~P4(x2173)+~P19(x2176)+~P19(x2171)+~P13(x2175,x2174)+E(x2171,x2172)+~P21(x2171,f35(x2174,x2174),x2174)+~P14(x2171,f35(x2174,x2174),x2174)+~E(f31(x2173,x2174,x2171,x2175,x2176),f31(x2177,x2178,x2172,x2179,x21710))+~P21(x2176,f35(x2174,f32(x2173)),x2174)+~P14(x2176,f35(x2174,f32(x2173)),x2174) % 78.05/78.41 [218]~P4(x2183)+~P19(x2186)+~P19(x2184)+~P13(x2185,x2181)+E(x2181,x2182)+~P21(x2184,f35(x2181,x2181),x2181)+~P14(x2184,f35(x2181,x2181),x2181)+~E(f31(x2183,x2181,x2184,x2185,x2186),f31(x2187,x2182,x2188,x2189,x21810))+~P21(x2186,f35(x2181,f32(x2183)),x2181)+~P14(x2186,f35(x2181,f32(x2183)),x2181) % 78.05/78.41 [219]~P4(x2191)+~P19(x2196)+~P19(x2194)+~P13(x2195,x2193)+E(x2191,x2192)+~P21(x2194,f35(x2193,x2193),x2193)+~P14(x2194,f35(x2193,x2193),x2193)+~E(f31(x2191,x2193,x2194,x2195,x2196),f31(x2192,x2197,x2198,x2199,x21910))+~P21(x2196,f35(x2193,f32(x2191)),x2193)+~P14(x2196,f35(x2193,f32(x2191)),x2193) % 78.05/78.41 [168]~P1(x1681)+~P23(x1681)+~P27(x1681)+~P28(x1681)+~P24(x1681)+~P31(x1681)+~P32(x1681)+~P33(x1681)+~P3(x1681)+P26(x1681)+P1(f9(x1681)) % 78.05/78.41 [169]~P1(x1691)+~P23(x1691)+~P27(x1691)+~P28(x1691)+~P24(x1691)+~P31(x1691)+~P32(x1691)+~P33(x1691)+~P3(x1691)+P26(x1691)+P1(f10(x1691)) % 78.05/78.41 [170]~P1(x1701)+~P23(x1701)+~P27(x1701)+~P28(x1701)+~P24(x1701)+~P31(x1701)+~P32(x1701)+~P33(x1701)+~P3(x1701)+P26(x1701)+P23(f9(x1701)) % 78.05/78.41 [171]~P1(x1711)+~P23(x1711)+~P27(x1711)+~P28(x1711)+~P24(x1711)+~P31(x1711)+~P32(x1711)+~P33(x1711)+~P3(x1711)+P26(x1711)+P23(f10(x1711)) % 78.05/78.41 [172]~P1(x1721)+~P23(x1721)+~P27(x1721)+~P28(x1721)+~P24(x1721)+~P31(x1721)+~P32(x1721)+~P33(x1721)+~P3(x1721)+P26(x1721)+P27(f9(x1721)) % 78.05/78.41 [173]~P1(x1731)+~P23(x1731)+~P27(x1731)+~P28(x1731)+~P24(x1731)+~P31(x1731)+~P32(x1731)+~P33(x1731)+~P3(x1731)+P26(x1731)+P27(f10(x1731)) % 78.05/78.41 [174]~P1(x1741)+~P23(x1741)+~P27(x1741)+~P28(x1741)+~P24(x1741)+~P31(x1741)+~P32(x1741)+~P33(x1741)+~P3(x1741)+P26(x1741)+P28(f9(x1741)) % 78.05/78.41 [175]~P1(x1751)+~P23(x1751)+~P27(x1751)+~P28(x1751)+~P24(x1751)+~P31(x1751)+~P32(x1751)+~P33(x1751)+~P3(x1751)+P26(x1751)+P28(f10(x1751)) % 78.05/78.41 [176]~P1(x1761)+~P23(x1761)+~P27(x1761)+~P28(x1761)+~P24(x1761)+~P31(x1761)+~P32(x1761)+~P33(x1761)+~P3(x1761)+P26(x1761)+~P26(f9(x1761)) % 78.05/78.41 [177]~P1(x1771)+~P23(x1771)+~P27(x1771)+~P28(x1771)+~P24(x1771)+~P31(x1771)+~P32(x1771)+~P33(x1771)+~P3(x1771)+P26(x1771)+~P26(f10(x1771)) % 78.05/78.41 [178]~P1(x1781)+~P23(x1781)+~P27(x1781)+~P28(x1781)+~P24(x1781)+~P31(x1781)+~P32(x1781)+~P33(x1781)+~P3(x1781)+P26(x1781)+P25(f9(x1781),x1781) % 78.05/78.41 [179]~P1(x1791)+~P23(x1791)+~P27(x1791)+~P28(x1791)+~P24(x1791)+~P31(x1791)+~P32(x1791)+~P33(x1791)+~P3(x1791)+P26(x1791)+P25(f10(x1791),x1791) % 78.05/78.41 [180]~P1(x1801)+~P23(x1801)+~P27(x1801)+~P28(x1801)+~P24(x1801)+~P31(x1801)+~P32(x1801)+~P33(x1801)+~P3(x1801)+P26(x1801)+P29(f10(x1801),x1801) % 78.05/78.41 [181]~P1(x1811)+~P23(x1811)+~P27(x1811)+~P28(x1811)+~P24(x1811)+~P31(x1811)+~P32(x1811)+~P33(x1811)+~P3(x1811)+P26(x1811)+P9(f9(x1811),x1811) % 78.05/78.41 [182]~P1(x1821)+~P23(x1821)+~P27(x1821)+~P28(x1821)+~P24(x1821)+~P31(x1821)+~P32(x1821)+~P33(x1821)+~P3(x1821)+P26(x1821)+P9(f10(x1821),x1821) % 78.05/78.41 [191]~P28(x1911)+~P9(x1911,x1912)+~P29(x1911,x1912)+~P3(x1912)+~P33(x1912)+~P32(x1912)+~P31(x1912)+~P24(x1912)+~P28(x1912)+~P27(x1912)+~P27(x1911)+~P23(x1912)+~P23(x1911)+~P1(x1912)+~P1(x1911)+P26(x1911)+P26(x1912)+P1(f11(x1912,x1911)) % 78.05/78.41 [192]~P28(x1921)+~P9(x1921,x1922)+~P29(x1921,x1922)+~P3(x1922)+~P33(x1922)+~P32(x1922)+~P31(x1922)+~P24(x1922)+~P28(x1922)+~P27(x1922)+~P27(x1921)+~P23(x1922)+~P23(x1921)+~P1(x1922)+~P1(x1921)+P26(x1921)+P26(x1922)+P23(f11(x1922,x1921)) % 78.05/78.41 [193]~P28(x1931)+~P9(x1931,x1932)+~P29(x1931,x1932)+~P3(x1932)+~P33(x1932)+~P32(x1932)+~P31(x1932)+~P24(x1932)+~P28(x1932)+~P27(x1932)+~P27(x1931)+~P23(x1932)+~P23(x1931)+~P1(x1932)+~P1(x1931)+P26(x1931)+P26(x1932)+P27(f11(x1932,x1931)) % 78.05/78.41 [194]~P28(x1941)+~P9(x1941,x1942)+~P29(x1941,x1942)+~P3(x1942)+~P33(x1942)+~P32(x1942)+~P31(x1942)+~P24(x1942)+~P28(x1942)+~P27(x1942)+~P27(x1941)+~P23(x1942)+~P23(x1941)+~P1(x1942)+~P1(x1941)+P26(x1941)+P26(x1942)+P28(f11(x1942,x1941)) % 78.05/78.41 [195]~P28(x1951)+~P9(x1951,x1952)+~P29(x1951,x1952)+~P3(x1952)+~P33(x1952)+~P32(x1952)+~P31(x1952)+~P24(x1952)+~P28(x1952)+~P27(x1952)+~P27(x1951)+~P23(x1952)+~P23(x1951)+~P1(x1952)+~P1(x1951)+P26(x1951)+P26(x1952)+P25(f11(x1952,x1951),x1952) % 78.05/78.41 [196]~P28(x1961)+~P9(x1961,x1962)+~P29(x1961,x1962)+~P3(x1962)+~P33(x1962)+~P32(x1962)+~P31(x1962)+~P24(x1962)+~P28(x1962)+~P27(x1962)+~P27(x1961)+~P23(x1962)+~P23(x1961)+~P1(x1962)+~P1(x1961)+P26(x1961)+P26(x1962)+P29(f11(x1962,x1961),x1962) % 78.05/78.41 [197]~P28(x1971)+~P9(x1971,x1972)+~P29(x1971,x1972)+~P3(x1972)+~P33(x1972)+~P32(x1972)+~P31(x1972)+~P24(x1972)+~P28(x1972)+~P27(x1972)+~P27(x1971)+~P23(x1972)+~P23(x1971)+~P1(x1972)+~P1(x1971)+P26(x1971)+P26(x1972)+~P26(f11(x1972,x1971)) % 78.05/78.41 [198]~P28(x1981)+~P9(x1981,x1982)+~P29(x1981,x1982)+~P3(x1982)+~P33(x1982)+~P32(x1982)+~P31(x1982)+~P24(x1982)+~P28(x1982)+~P27(x1982)+~P27(x1981)+~P23(x1982)+~P23(x1981)+~P1(x1982)+~P1(x1981)+P26(x1981)+P26(x1982)+P15(f7(x1982,x1981),x1982,x1981) % 78.05/78.41 [199]~P28(x1991)+~P9(x1991,x1992)+~P29(x1991,x1992)+~P3(x1992)+~P33(x1992)+~P32(x1992)+~P31(x1992)+~P24(x1992)+~P28(x1992)+~P27(x1992)+~P27(x1991)+~P23(x1992)+~P23(x1991)+~P1(x1992)+~P1(x1991)+P26(x1991)+P26(x1992)+P15(f11(x1992,x1991),x1992,x1991) % 78.05/78.41 [200]~P28(x2001)+~P15(x2003,x2002,x2001)+~P9(x2001,x2002)+~P29(x2001,x2002)+~P3(x2002)+~P33(x2002)+~P32(x2002)+~P31(x2002)+~P24(x2002)+~P28(x2002)+~P27(x2002)+~P27(x2001)+~P23(x2002)+~P23(x2001)+~P1(x2002)+~P1(x2001)+P26(x2001)+P26(x2002)+P1(x2003) % 78.05/78.41 [201]~P28(x2011)+~P15(x2013,x2012,x2011)+~P9(x2011,x2012)+~P29(x2011,x2012)+~P3(x2012)+~P33(x2012)+~P32(x2012)+~P31(x2012)+~P24(x2012)+~P28(x2012)+~P27(x2012)+~P27(x2011)+~P23(x2012)+~P23(x2011)+~P1(x2012)+~P1(x2011)+P26(x2011)+P26(x2012)+P23(x2013) % 78.05/78.41 [202]~P28(x2021)+~P15(x2023,x2022,x2021)+~P9(x2021,x2022)+~P29(x2021,x2022)+~P3(x2022)+~P33(x2022)+~P32(x2022)+~P31(x2022)+~P24(x2022)+~P28(x2022)+~P27(x2022)+~P27(x2021)+~P23(x2022)+~P23(x2021)+~P1(x2022)+~P1(x2021)+P26(x2021)+P26(x2022)+P27(x2023) % 78.05/78.41 [203]~P28(x2031)+~P15(x2033,x2032,x2031)+~P9(x2031,x2032)+~P29(x2031,x2032)+~P3(x2032)+~P33(x2032)+~P32(x2032)+~P31(x2032)+~P24(x2032)+~P28(x2032)+~P27(x2032)+~P27(x2031)+~P23(x2032)+~P23(x2031)+~P1(x2032)+~P1(x2031)+P26(x2031)+P26(x2032)+P28(x2033) % 78.05/78.41 [204]~P28(x2041)+~P15(x2043,x2042,x2041)+~P9(x2041,x2042)+~P29(x2041,x2042)+~P3(x2042)+~P33(x2042)+~P32(x2042)+~P31(x2042)+~P24(x2042)+~P28(x2042)+~P27(x2042)+~P27(x2041)+~P23(x2042)+~P23(x2041)+~P1(x2042)+~P1(x2041)+P26(x2041)+P26(x2042)+~P26(x2043) % 78.05/78.41 [205]~P28(x2051)+~P15(x2053,x2052,x2051)+~P9(x2051,x2052)+~P29(x2051,x2052)+~P3(x2052)+~P33(x2052)+~P32(x2052)+~P31(x2052)+~P24(x2052)+~P28(x2052)+~P27(x2052)+~P27(x2051)+~P23(x2052)+~P23(x2051)+~P1(x2052)+~P1(x2051)+P26(x2051)+P29(x2053,x2052)+P26(x2052) % 78.05/78.41 [206]~P28(x2061)+~P15(x2063,x2062,x2061)+~P9(x2061,x2062)+~P29(x2061,x2062)+~P3(x2062)+~P33(x2062)+~P32(x2062)+~P31(x2062)+~P24(x2062)+~P28(x2062)+~P27(x2062)+~P27(x2061)+~P23(x2062)+~P23(x2061)+~P1(x2062)+~P1(x2061)+P26(x2061)+P9(x2063,x2062)+P26(x2062) % 78.05/78.41 [207]~P28(x2071)+~P29(x2071,x2072)+~P3(x2072)+~P2(x2072)+~P33(x2072)+~P32(x2072)+~P31(x2072)+~P30(x2072)+~P24(x2072)+~P28(x2072)+~P27(x2072)+~P27(x2071)+~P23(x2072)+~P23(x2071)+~P1(x2072)+~P1(x2071)+~P9(x2071,x2072)+P17(x2072)+P26(x2071)+P26(x2072)+P25(f29(x2072,x2071,x2073),x2072)+~P13(x2073,f33(f32(x2071))) % 78.05/78.41 [208]~P28(x2081)+~P29(x2081,x2082)+~P3(x2082)+~P2(x2082)+~P33(x2082)+~P32(x2082)+~P31(x2082)+~P30(x2082)+~P24(x2082)+~P28(x2082)+~P27(x2082)+~P27(x2081)+~P23(x2082)+~P23(x2081)+~P1(x2082)+~P1(x2081)+~P9(x2081,x2082)+P17(x2082)+P26(x2081)+P26(x2082)+P15(f29(x2082,x2081,x2083),x2082,x2081)+~P13(x2083,f33(f32(x2081))) % 78.05/78.41 [210]~P28(x2101)+~P9(x2101,x2102)+~P29(x2101,x2102)+~P3(x2102)+~P2(x2102)+~P33(x2102)+~P32(x2102)+~P31(x2102)+~P30(x2102)+~P24(x2102)+~P28(x2102)+~P27(x2102)+~P27(x2101)+~P23(x2102)+~P23(x2101)+~P1(x2102)+~P1(x2101)+~P12(x2103,x2104)+P17(x2102)+P26(x2101)+P26(x2102)+P15(f29(x2102,x2101,x2103),x2102,f29(x2102,x2101,x2104))+~P13(x2104,f33(f32(x2101)))+~P13(x2103,f33(f32(x2101))) % 78.05/78.41 [209]~P28(x2091)+~P15(x2091,x2093,x2092)+~P15(x2092,x2093,x2091)+~P9(x2091,x2093)+~P9(x2092,x2093)+~P29(x2091,x2093)+~P29(x2092,x2093)+~P25(x2091,x2093)+~P25(x2092,x2093)+~P3(x2093)+~P33(x2093)+~P32(x2093)+~P31(x2093)+~P24(x2093)+~P28(x2093)+~P28(x2092)+~P27(x2093)+~P27(x2091)+~P27(x2092)+~P23(x2093)+~P23(x2091)+~P23(x2092)+~P1(x2093)+~P1(x2091)+~P1(x2092)+P26(x2091)+P26(x2092)+E(x2091,x2092)+P26(x2093) % 78.05/78.41 %EqnAxiom % 78.05/78.41 [1]E(x11,x11) % 78.05/78.41 [2]E(x22,x21)+~E(x21,x22) % 78.05/78.41 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 78.05/78.41 [4]~E(x41,x42)+E(f16(x41),f16(x42)) % 78.05/78.41 [5]~E(x51,x52)+E(f5(x51),f5(x52)) % 78.05/78.41 [6]~E(x61,x62)+E(f32(x61),f32(x62)) % 78.05/78.41 [7]~E(x71,x72)+E(f33(x71),f33(x72)) % 78.05/78.41 [8]~E(x81,x82)+E(f35(x81,x83),f35(x82,x83)) % 78.05/78.41 [9]~E(x91,x92)+E(f35(x93,x91),f35(x93,x92)) % 78.05/78.41 [10]~E(x101,x102)+E(f31(x101,x103,x104,x105,x106),f31(x102,x103,x104,x105,x106)) % 78.05/78.41 [11]~E(x111,x112)+E(f31(x113,x111,x114,x115,x116),f31(x113,x112,x114,x115,x116)) % 78.05/78.41 [12]~E(x121,x122)+E(f31(x123,x124,x121,x125,x126),f31(x123,x124,x122,x125,x126)) % 78.05/78.41 [13]~E(x131,x132)+E(f31(x133,x134,x135,x131,x136),f31(x133,x134,x135,x132,x136)) % 78.05/78.41 [14]~E(x141,x142)+E(f31(x143,x144,x145,x146,x141),f31(x143,x144,x145,x146,x142)) % 78.05/78.41 [15]~E(x151,x152)+E(f37(x151,x153),f37(x152,x153)) % 78.05/78.41 [16]~E(x161,x162)+E(f37(x163,x161),f37(x163,x162)) % 78.05/78.41 [17]~E(x171,x172)+E(f11(x171,x173),f11(x172,x173)) % 78.05/78.41 [18]~E(x181,x182)+E(f11(x183,x181),f11(x183,x182)) % 78.05/78.41 [19]~E(x191,x192)+E(f29(x191,x193,x194),f29(x192,x193,x194)) % 78.05/78.41 [20]~E(x201,x202)+E(f29(x203,x201,x204),f29(x203,x202,x204)) % 78.05/78.41 [21]~E(x211,x212)+E(f29(x213,x214,x211),f29(x213,x214,x212)) % 78.05/78.41 [22]~E(x221,x222)+E(f6(x221,x223),f6(x222,x223)) % 78.05/78.41 [23]~E(x231,x232)+E(f6(x233,x231),f6(x233,x232)) % 78.05/78.41 [24]~E(x241,x242)+E(f8(x241,x243),f8(x242,x243)) % 78.05/78.41 [25]~E(x251,x252)+E(f8(x253,x251),f8(x253,x252)) % 78.05/78.41 [26]~E(x261,x262)+E(f10(x261),f10(x262)) % 78.05/78.41 [27]~E(x271,x272)+E(f9(x271),f9(x272)) % 78.05/78.41 [28]~E(x281,x282)+E(f34(x281),f34(x282)) % 78.05/78.41 [29]~E(x291,x292)+E(f15(x291),f15(x292)) % 78.05/78.41 [30]~E(x301,x302)+E(f19(x301),f19(x302)) % 78.05/78.41 [31]~E(x311,x312)+E(f20(x311),f20(x312)) % 78.05/78.41 [32]~E(x321,x322)+E(f30(x321),f30(x322)) % 78.05/78.41 [33]~E(x331,x332)+E(f7(x331,x333),f7(x332,x333)) % 78.05/78.41 [34]~E(x341,x342)+E(f7(x343,x341),f7(x343,x342)) % 78.05/78.41 [35]~E(x351,x352)+E(f36(x351),f36(x352)) % 78.05/78.41 [36]~E(x361,x362)+E(f21(x361),f21(x362)) % 78.05/78.41 [37]~P1(x371)+P1(x372)+~E(x371,x372) % 78.05/78.41 [38]P14(x382,x383,x384)+~E(x381,x382)+~P14(x381,x383,x384) % 78.05/78.41 [39]P14(x393,x392,x394)+~E(x391,x392)+~P14(x393,x391,x394) % 78.05/78.41 [40]P14(x403,x404,x402)+~E(x401,x402)+~P14(x403,x404,x401) % 78.05/78.41 [41]~P23(x411)+P23(x412)+~E(x411,x412) % 78.05/78.41 [42]P13(x422,x423)+~E(x421,x422)+~P13(x421,x423) % 78.05/78.41 [43]P13(x433,x432)+~E(x431,x432)+~P13(x433,x431) % 78.05/78.41 [44]~P27(x441)+P27(x442)+~E(x441,x442) % 78.05/78.41 [45]~P33(x451)+P33(x452)+~E(x451,x452) % 78.05/78.41 [46]~P28(x461)+P28(x462)+~E(x461,x462) % 78.05/78.41 [47]~P26(x471)+P26(x472)+~E(x471,x472) % 78.05/78.41 [48]~P24(x481)+P24(x482)+~E(x481,x482) % 78.05/78.41 [49]~P30(x491)+P30(x492)+~E(x491,x492) % 78.05/78.41 [50]~P31(x501)+P31(x502)+~E(x501,x502) % 78.05/78.41 [51]~P32(x511)+P32(x512)+~E(x511,x512) % 78.05/78.41 [52]~P3(x521)+P3(x522)+~E(x521,x522) % 78.05/78.41 [53]~P2(x531)+P2(x532)+~E(x531,x532) % 78.05/78.41 [54]P21(x542,x543,x544)+~E(x541,x542)+~P21(x541,x543,x544) % 78.05/78.41 [55]P21(x553,x552,x554)+~E(x551,x552)+~P21(x553,x551,x554) % 78.05/78.41 [56]P21(x563,x564,x562)+~E(x561,x562)+~P21(x563,x564,x561) % 78.05/78.41 [57]~P19(x571)+P19(x572)+~E(x571,x572) % 78.05/78.41 [58]~P4(x581)+P4(x582)+~E(x581,x582) % 78.05/78.41 [59]P29(x592,x593)+~E(x591,x592)+~P29(x591,x593) % 78.05/78.41 [60]P29(x603,x602)+~E(x601,x602)+~P29(x603,x601) % 78.05/78.41 [61]~P7(x611)+P7(x612)+~E(x611,x612) % 78.05/78.41 [62]~P5(x621)+P5(x622)+~E(x621,x622) % 78.05/78.41 [63]~P6(x631)+P6(x632)+~E(x631,x632) % 78.05/78.41 [64]~P8(x641)+P8(x642)+~E(x641,x642) % 78.05/78.41 [65]P18(x652,x653)+~E(x651,x652)+~P18(x651,x653) % 78.05/78.41 [66]P18(x663,x662)+~E(x661,x662)+~P18(x663,x661) % 78.05/78.41 [67]~P10(x671)+P10(x672)+~E(x671,x672) % 78.05/78.41 [68]~P11(x681)+P11(x682)+~E(x681,x682) % 78.05/78.41 [69]P16(x692,x693,x694)+~E(x691,x692)+~P16(x691,x693,x694) % 78.05/78.41 [70]P16(x703,x702,x704)+~E(x701,x702)+~P16(x703,x701,x704) % 78.05/78.41 [71]P16(x713,x714,x712)+~E(x711,x712)+~P16(x713,x714,x711) % 78.05/78.41 [72]P12(x722,x723)+~E(x721,x722)+~P12(x721,x723) % 78.05/78.41 [73]P12(x733,x732)+~E(x731,x732)+~P12(x733,x731) % 78.05/78.41 [74]P25(x742,x743)+~E(x741,x742)+~P25(x741,x743) % 78.05/78.41 [75]P25(x753,x752)+~E(x751,x752)+~P25(x753,x751) % 78.05/78.41 [76]P9(x762,x763)+~E(x761,x762)+~P9(x761,x763) % 78.05/78.41 [77]P9(x773,x772)+~E(x771,x772)+~P9(x773,x771) % 78.05/78.41 [78]P15(x782,x783,x784)+~E(x781,x782)+~P15(x781,x783,x784) % 78.05/78.41 [79]P15(x793,x792,x794)+~E(x791,x792)+~P15(x793,x791,x794) % 78.05/78.41 [80]P15(x803,x804,x802)+~E(x801,x802)+~P15(x803,x804,x801) % 78.05/78.41 [81]~P17(x811)+P17(x812)+~E(x811,x812) % 78.05/78.41 [82]~P22(x821)+P22(x822)+~E(x821,x822) % 78.05/78.41 [83]~P20(x831)+P20(x832)+~E(x831,x832) % 78.05/78.41 % 78.05/78.41 %------------------------------------------- % 78.05/78.41 cnf(228,plain, % 78.05/78.41 (E(a12,f29(a1,a12,a24))), % 78.05/78.41 inference(scs_inference,[],[120,117,162,2])). % 78.05/78.41 cnf(231,plain, % 78.05/78.41 (P20(f16(f35(x2311,x2312)))), % 78.05/78.41 inference(scs_inference,[],[120,117,119,108,162,2,150,183])). % 78.05/78.41 cnf(234,plain, % 78.05/78.41 (P18(f5(a17),a17)), % 78.05/78.41 inference(scs_inference,[],[120,117,116,119,108,128,162,2,150,183,159])). % 78.05/78.41 cnf(235,plain, % 78.05/78.41 (P13(f5(x2351),x2351)), % 78.05/78.41 inference(rename_variables,[],[116])). % 78.05/78.41 cnf(237,plain, % 78.05/78.41 (~P18(x2371,f5(f33(a28)))), % 78.05/78.41 inference(scs_inference,[],[120,117,116,235,119,108,128,162,2,150,183,159,166])). % 78.05/78.41 cnf(238,plain, % 78.05/78.41 (P13(f5(x2381),x2381)), % 78.05/78.41 inference(rename_variables,[],[116])). % 78.05/78.41 cnf(240,plain, % 78.05/78.41 (~E(f29(a1,a12,a25),f29(a1,a12,a24))), % 78.05/78.41 inference(scs_inference,[],[120,130,117,116,235,119,108,128,162,2,150,183,159,166,3])). % 78.05/78.41 cnf(241,plain, % 78.05/78.41 (P1(f29(a1,a12,a24))), % 78.05/78.41 inference(scs_inference,[],[85,120,130,117,116,235,119,108,128,162,2,150,183,159,166,3,37])). % 78.05/78.41 cnf(242,plain, % 78.05/78.41 (P14(f6(f29(a1,a12,a24),x2421),a12,x2421)), % 78.05/78.41 inference(scs_inference,[],[85,120,130,117,121,116,235,119,108,128,162,2,150,183,159,166,3,37,39])). % 78.05/78.41 cnf(243,plain, % 78.05/78.41 (P14(f6(x2431,x2432),x2431,x2432)), % 78.05/78.41 inference(rename_variables,[],[121])). % 78.05/78.41 cnf(244,plain, % 78.05/78.41 (P14(f6(x2441,f29(a1,a12,a24)),x2441,a12)), % 78.05/78.41 inference(scs_inference,[],[85,120,130,117,121,243,116,235,119,108,128,162,2,150,183,159,166,3,37,39,40])). % 78.05/78.41 cnf(246,plain, % 78.05/78.41 (P23(f29(a1,a12,a24))), % 78.05/78.41 inference(scs_inference,[],[85,87,120,130,117,121,243,116,235,119,108,128,162,2,150,183,159,166,3,37,39,40,41])). % 78.05/78.41 cnf(249,plain, % 78.05/78.41 (P27(f29(a1,a12,a24))), % 78.05/78.41 inference(scs_inference,[],[85,87,89,120,130,117,121,243,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44])). % 78.05/78.41 cnf(250,plain, % 78.05/78.41 (P28(f29(a1,a12,a24))), % 78.05/78.41 inference(scs_inference,[],[85,87,89,91,120,130,117,121,243,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44,46])). % 78.05/78.41 cnf(251,plain, % 78.05/78.41 (~P26(f29(a1,a12,a24))), % 78.05/78.41 inference(scs_inference,[],[85,87,89,91,124,120,130,117,121,243,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44,46,47])). % 78.05/78.41 cnf(252,plain, % 78.05/78.41 (P29(f29(a1,a12,a24),a1)), % 78.05/78.41 inference(scs_inference,[],[85,87,89,91,112,124,120,130,117,121,243,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44,46,47,59])). % 78.05/78.41 cnf(254,plain, % 78.05/78.41 (P16(f8(f29(a1,a12,a24),x2541),a12,x2541)), % 78.05/78.41 inference(scs_inference,[],[85,87,89,91,112,124,120,130,117,121,243,122,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44,46,47,59,66,70])). % 78.05/78.41 cnf(255,plain, % 78.05/78.41 (P16(f8(x2551,x2552),x2551,x2552)), % 78.05/78.41 inference(rename_variables,[],[122])). % 78.05/78.41 cnf(256,plain, % 78.05/78.41 (P12(a12,f29(a1,a12,a24))), % 78.05/78.41 inference(scs_inference,[],[85,87,89,91,112,124,120,130,117,115,121,243,122,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44,46,47,59,66,70,72])). % 78.05/78.41 cnf(257,plain, % 78.05/78.41 (P12(x2571,x2571)), % 78.05/78.41 inference(rename_variables,[],[115])). % 78.05/78.41 cnf(258,plain, % 78.05/78.41 (P12(f29(a1,a12,a24),a12)), % 78.05/78.41 inference(scs_inference,[],[85,87,89,91,112,124,120,130,117,115,257,121,243,122,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44,46,47,59,66,70,72,73])). % 78.05/78.41 cnf(259,plain, % 78.05/78.41 (P12(x2591,x2591)), % 78.05/78.41 inference(rename_variables,[],[115])). % 78.05/78.41 cnf(260,plain, % 78.05/78.41 (P25(f29(a1,a12,a24),a1)), % 78.05/78.41 inference(scs_inference,[],[85,87,89,91,111,112,124,120,130,117,115,257,121,243,122,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44,46,47,59,66,70,72,73,74])). % 78.05/78.41 cnf(261,plain, % 78.05/78.41 (P9(f29(a1,a12,a24),a1)), % 78.05/78.41 inference(scs_inference,[],[85,87,89,91,111,112,113,124,120,130,117,115,257,121,243,122,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44,46,47,59,66,70,72,73,74,76])). % 78.05/78.41 cnf(262,plain, % 78.05/78.41 (P16(f8(x2621,f29(a1,a12,a24)),x2621,a12)), % 78.05/78.41 inference(scs_inference,[],[85,87,89,91,111,112,113,124,120,130,117,115,257,121,243,122,255,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44,46,47,59,66,70,72,73,74,76,71])). % 78.05/78.41 cnf(264,plain, % 78.05/78.41 (P25(f29(a1,a12,a25),a1)), % 78.05/78.41 inference(scs_inference,[],[84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,111,112,113,123,124,127,120,130,117,118,115,257,121,243,122,255,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44,46,47,59,66,70,72,73,74,76,71,207])). % 78.05/78.41 cnf(268,plain, % 78.05/78.41 (P15(f29(a1,a12,a24),a1,f29(a1,a12,a24))), % 78.05/78.41 inference(scs_inference,[],[84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,111,112,113,123,124,127,120,130,117,118,115,257,259,121,243,122,255,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44,46,47,59,66,70,72,73,74,76,71,207,208,210])). % 78.05/78.41 cnf(272,plain, % 78.05/78.41 (~P18(a17,f5(a17))), % 78.05/78.41 inference(scs_inference,[],[84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,111,112,113,123,124,127,120,130,117,118,115,257,259,121,243,122,255,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44,46,47,59,66,70,72,73,74,76,71,207,208,210,21,161])). % 78.05/78.41 cnf(274,plain, % 78.05/78.41 (P13(x2741,f32(a12))+~P18(x2741,a24)), % 78.05/78.41 inference(scs_inference,[],[84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,111,112,113,123,124,127,120,130,117,118,115,257,259,121,243,122,255,116,235,238,119,108,128,162,2,150,183,159,166,3,37,39,40,41,43,44,46,47,59,66,70,72,73,74,76,71,207,208,210,21,161,167])). % 78.05/78.41 cnf(280,plain, % 78.05/78.41 (~P18(x2801,a14)), % 78.05/78.41 inference(scs_inference,[],[109,150])). % 78.05/78.41 cnf(284,plain, % 78.05/78.41 (P18(a25,f33(f32(a12)))), % 78.05/78.41 inference(scs_inference,[],[118,109,129,150,162,159])). % 78.05/78.41 cnf(288,plain, % 78.05/78.41 (~P18(x2881,f5(f33(a14)))), % 78.05/78.41 inference(scs_inference,[],[118,120,268,109,129,116,150,162,159,78,166])). % 78.05/78.41 cnf(291,plain, % 78.05/78.41 (P16(f8(f29(a1,a12,a24),f29(a1,a12,a24)),a12,a12)), % 78.05/78.41 inference(scs_inference,[],[118,120,268,254,109,129,116,150,162,159,78,166,71])). % 78.05/78.41 cnf(293,plain, % 78.05/78.41 (P14(f6(f29(a1,a12,a24),f29(a1,a12,a24)),a12,a12)), % 78.05/78.41 inference(scs_inference,[],[118,120,268,244,254,109,129,116,150,162,159,78,166,71,39])). % 78.05/78.41 cnf(297,plain, % 78.05/78.41 (P15(f29(a1,a12,a25),a1,a12)), % 78.05/78.41 inference(scs_inference,[],[84,113,118,86,88,90,92,93,94,95,96,97,98,123,127,85,87,89,91,112,124,120,268,237,244,254,234,109,129,116,150,162,159,78,166,71,39,66,208])). % 78.05/78.41 cnf(299,plain, % 78.05/78.41 (P15(f29(a1,a12,a25),a1,f29(a1,a12,a25))), % 78.05/78.41 inference(scs_inference,[],[84,113,118,86,88,90,92,93,94,95,96,97,98,123,127,85,87,89,91,112,124,120,268,237,244,254,234,109,129,115,116,150,162,159,78,166,71,39,66,208,210])). % 78.05/78.41 cnf(316,plain, % 78.05/78.41 (P18(a24,f33(f32(a12)))), % 78.05/78.41 inference(scs_inference,[],[117,119,110,129,162,150,159])). % 78.05/78.41 cnf(319,plain, % 78.05/78.41 (P12(f16(f29(a1,a12,a24)),a12)), % 78.05/78.41 inference(scs_inference,[],[120,117,119,110,129,162,150,159,73])). % 78.05/78.41 cnf(320,plain, % 78.05/78.41 (P15(f29(a1,a12,a25),a1,f29(a1,a12,a24))), % 78.05/78.41 inference(scs_inference,[],[120,117,228,297,119,110,129,162,150,159,73,80])). % 78.05/78.41 cnf(321,plain, % 78.05/78.41 (~E(f33(f32(a12)),f5(f33(a14)))), % 78.05/78.41 inference(scs_inference,[],[120,117,228,288,284,297,119,110,129,162,150,159,73,80,66])). % 78.05/78.41 cnf(329,plain, % 78.05/78.41 (P12(f5(f33(x3291)),x3291)), % 78.05/78.41 inference(scs_inference,[],[116,162])). % 78.05/78.41 cnf(364,plain, % 78.05/78.41 (P16(x3641,a12,x3642)+~E(f8(f29(a1,a12,a24),x3642),x3641)), % 78.05/78.41 inference(scs_inference,[],[120,117,228,254,316,45,57,166,63,65,69])). % 78.05/78.41 cnf(441,plain, % 78.05/78.41 (P8(a1)), % 78.05/78.41 inference(scs_inference,[],[98,136,137])). % 78.05/78.41 cnf(446,plain, % 78.05/78.41 (P15(x4461,a1,a12)+~E(f29(a1,a12,a25),x4461)), % 78.05/78.41 inference(scs_inference,[],[120,297,116,81,167,78])). % 78.05/78.41 cnf(463,plain, % 78.05/78.41 (P12(a24,x4631)+~E(a25,x4631)), % 78.05/78.41 inference(scs_inference,[],[120,114,299,79,48,73])). % 78.05/78.41 cnf(466,plain, % 78.05/78.41 (P14(x4661,a12,x4662)+~E(f6(f29(a1,a12,a24),x4662),x4661)), % 78.05/78.41 inference(scs_inference,[],[120,118,114,242,299,79,48,73,43,72,38])). % 78.05/78.41 cnf(507,plain, % 78.05/78.41 (P16(x5071,x5072,a12)+~E(f8(x5072,f29(a1,a12,a24)),x5071)), % 78.05/78.41 inference(scs_inference,[],[262,69])). % 78.05/78.41 cnf(531,plain, % 78.05/78.41 (P12(x5311,a12)+~E(f16(f29(a1,a12,a24)),x5311)), % 78.05/78.41 inference(scs_inference,[],[319,72])). % 78.05/78.41 cnf(538,plain, % 78.05/78.41 (P14(x5381,x5382,a12)+~E(f6(x5382,f29(a1,a12,a24)),x5381)), % 78.05/78.41 inference(scs_inference,[],[244,38])). % 78.05/78.41 cnf(547,plain, % 78.05/78.41 (P13(x5471,f33(x5472))+~E(f16(x5472),x5471)), % 78.05/78.41 inference(scs_inference,[],[119,42])). % 78.05/78.41 cnf(556,plain, % 78.05/78.41 (P13(x5561,x5562)+~E(f5(x5562),x5561)), % 78.05/78.41 inference(scs_inference,[],[329,116,121,122,72,38,69,42])). % 78.05/78.41 cnf(629,plain, % 78.05/78.41 (P1(f29(a1,a12,a25))), % 78.05/78.41 inference(scs_inference,[],[85,113,112,87,89,91,124,84,86,92,95,96,94,123,88,90,98,297,200])). % 78.05/78.41 cnf(631,plain, % 78.05/78.41 (P23(f29(a1,a12,a25))), % 78.05/78.41 inference(scs_inference,[],[85,113,112,87,89,91,124,84,86,92,95,96,94,123,88,90,98,297,200,201])). % 78.05/78.41 cnf(633,plain, % 78.05/78.41 (P27(f29(a1,a12,a25))), % 78.05/78.41 inference(scs_inference,[],[85,113,112,87,89,91,124,84,86,92,95,96,94,123,88,90,98,297,200,201,202])). % 78.05/78.41 cnf(635,plain, % 78.05/78.41 (P28(f29(a1,a12,a25))), % 78.05/78.41 inference(scs_inference,[],[85,113,112,87,89,91,124,84,86,92,95,96,94,123,88,90,98,297,200,201,202,203])). % 78.05/78.41 cnf(637,plain, % 78.05/78.41 (~P26(f29(a1,a12,a25))), % 78.05/78.41 inference(scs_inference,[],[85,113,112,87,89,91,124,84,86,92,95,96,94,123,88,90,98,297,200,201,202,203,204])). % 78.05/78.41 cnf(639,plain, % 78.05/78.41 (P29(f29(a1,a12,a25),a1)), % 78.05/78.41 inference(scs_inference,[],[85,113,112,87,89,91,124,84,86,92,95,96,94,123,88,90,98,297,200,201,202,203,204,205])). % 78.05/78.41 cnf(641,plain, % 78.05/78.41 (P9(f29(a1,a12,a25),a1)), % 78.05/78.41 inference(scs_inference,[],[85,113,112,87,89,91,124,84,86,92,95,96,94,123,88,90,98,297,200,201,202,203,204,205,206])). % 78.05/78.41 cnf(989,plain, % 78.05/78.41 (P13(a24,f33(x9891))+~E(a25,x9891)), % 78.05/78.41 inference(scs_inference,[],[160,463])). % 78.05/78.41 cnf(990,plain, % 78.05/78.41 (P13(a24,f33(a25))), % 78.05/78.41 inference(equality_inference,[],[989])). % 78.05/78.41 cnf(1083,plain, % 78.05/78.41 (P13(x10831,x10832)+~E(f32(a12),x10832)+~P18(x10831,a24)), % 78.05/78.41 inference(scs_inference,[],[274,43])). % 78.05/78.41 cnf(2285,plain, % 78.05/78.41 (P14(f8(f29(a1,a12,a24),x22851),f29(a1,a12,a24),x22851)), % 78.05/78.41 inference(scs_inference,[],[254,228,186,39])). % 78.05/78.41 cnf(2286,plain, % 78.05/78.41 (P14(f8(f29(a1,a12,a24),x22861),a12,x22861)), % 78.05/78.41 inference(scs_inference,[],[120,2285,39])). % 78.05/78.41 cnf(2287,plain, % 78.05/78.41 (P14(f8(f29(a1,a12,a24),f29(a1,a12,a24)),f29(a1,a12,a24),a12)), % 78.05/78.41 inference(scs_inference,[],[120,2285,39,40])). % 78.05/78.41 cnf(2292,plain, % 78.05/78.41 (P14(x22921,f29(a1,a12,a24),a12)+~E(f8(f29(a1,a12,a24),f29(a1,a12,a24)),x22921)), % 78.05/78.41 inference(scs_inference,[],[120,2287,39,38])). % 78.05/78.41 cnf(2294,plain, % 78.05/78.41 (P14(x22941,a12,x22942)+~E(f8(f29(a1,a12,a24),x22942),x22941)), % 78.05/78.41 inference(scs_inference,[],[2286,38])). % 78.05/78.41 cnf(2313,plain, % 78.05/78.41 (P13(f6(f29(a1,a12,a24),x23131),f33(f35(a12,x23131)))), % 78.05/78.41 inference(scs_inference,[],[242,187,188])). % 78.05/78.41 cnf(2318,plain, % 78.05/78.41 (P12(x23181,f35(a12,x23182))+~E(f6(f29(a1,a12,a24),x23182),x23181)), % 78.05/78.41 inference(scs_inference,[],[2313,183,162,72])). % 78.05/78.41 cnf(2334,plain, % 78.05/78.41 (P13(x23341,f33(f35(a12,x23342)))+~E(f6(f29(a1,a12,a24),x23342),x23341)), % 78.05/78.41 inference(scs_inference,[],[2313,42])). % 78.05/78.41 cnf(2335,plain, % 78.05/78.41 (P20(x23351)+~E(f6(f29(a1,a12,a24),x23352),x23351)), % 78.05/78.41 inference(scs_inference,[],[2313,42,183])). % 78.05/78.41 cnf(2693,plain, % 78.05/78.41 (E(f7(x26931,a14),f7(x26931,a28))), % 78.05/78.41 inference(scs_inference,[],[109,34,131])). % 78.05/78.41 cnf(2694,plain, % 78.05/78.41 (E(f7(x26941,a28),f7(x26941,a14))), % 78.05/78.41 inference(scs_inference,[],[2693,2])). % 78.05/78.41 cnf(3005,plain, % 78.05/78.41 (~P11(f15(a17))), % 78.05/78.41 inference(scs_inference,[],[104,128,141,142])). % 78.05/78.41 cnf(3007,plain, % 78.05/78.41 (~P26(f19(a22))), % 78.05/78.41 inference(scs_inference,[],[100,104,128,141,142,143])). % 78.05/78.41 cnf(3013,plain, % 78.05/78.41 (P9(f20(a22),a22)), % 78.05/78.41 inference(scs_inference,[],[100,104,128,141,142,143,144,145,146])). % 78.05/78.41 cnf(3015,plain, % 78.05/78.41 (P9(f19(a22),a22)), % 78.05/78.41 inference(scs_inference,[],[100,104,128,141,142,143,144,145,146,147])). % 78.05/78.41 cnf(3017,plain, % 78.05/78.41 (P13(a12,f33(f29(a1,a12,a24)))), % 78.05/78.41 inference(scs_inference,[],[256,100,104,128,141,142,143,144,145,146,147,160])). % 78.05/78.41 cnf(3019,plain, % 78.05/78.41 (P14(f8(x30191,f29(a1,a12,a24)),x30191,a12)), % 78.05/78.41 inference(scs_inference,[],[256,100,104,262,128,141,142,143,144,145,146,147,160,186])). % 78.05/78.41 cnf(3058,plain, % 78.05/78.41 (P16(f34(a26),f35(f32(a26),f32(a26)),f32(a26))), % 78.05/78.41 inference(scs_inference,[],[441,256,291,100,104,293,262,128,129,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185])). % 78.05/78.41 cnf(3061,plain, % 78.05/78.41 (P14(f6(f29(a1,a12,a24),f7(x30611,a14)),a12,f7(x30611,a28))), % 78.05/78.41 inference(scs_inference,[],[441,256,291,100,104,293,262,128,129,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466])). % 78.05/78.41 cnf(3062,plain, % 78.05/78.41 (P16(f8(f7(x30621,a14),f29(a1,a12,a24)),f7(x30621,a28),a12)), % 78.05/78.41 inference(scs_inference,[],[441,256,291,100,104,293,262,128,129,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507])). % 78.05/78.41 cnf(3063,plain, % 78.05/78.41 (P14(f6(f7(x30631,a14),f29(a1,a12,a24)),f7(x30631,a28),a12)), % 78.05/78.41 inference(scs_inference,[],[441,256,291,100,104,293,262,128,129,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538])). % 78.05/78.41 cnf(3071,plain, % 78.05/78.41 (E(f16(x30711),a28)), % 78.05/78.41 inference(scs_inference,[],[441,256,291,100,104,293,262,110,128,129,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131])). % 78.05/78.41 cnf(3073,plain, % 78.05/78.41 (P6(a2)), % 78.05/78.41 inference(scs_inference,[],[99,441,256,291,100,104,293,262,110,128,129,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136])). % 78.05/78.41 cnf(3075,plain, % 78.05/78.41 (P8(a4)), % 78.05/78.41 inference(scs_inference,[],[99,107,441,256,291,100,104,293,262,110,128,129,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138])). % 78.05/78.41 cnf(3077,plain, % 78.05/78.41 (P4(a23)), % 78.05/78.41 inference(scs_inference,[],[99,107,441,256,291,100,104,293,262,110,128,129,103,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132])). % 78.05/78.41 cnf(3079,plain, % 78.05/78.41 (P8(a26)), % 78.05/78.41 inference(scs_inference,[],[99,107,441,256,291,100,104,293,262,110,128,129,103,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137])). % 78.05/78.41 cnf(3082,plain, % 78.05/78.41 (P4(a1)), % 78.05/78.41 inference(scs_inference,[],[99,107,441,256,291,100,104,293,262,110,128,129,103,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133])). % 78.05/78.41 cnf(3084,plain, % 78.05/78.41 (P5(a27)), % 78.05/78.41 inference(scs_inference,[],[99,102,107,441,256,291,100,104,293,262,110,128,129,103,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135])). % 78.05/78.41 cnf(3086,plain, % 78.05/78.41 (P10(a2)), % 78.05/78.41 inference(scs_inference,[],[99,102,107,441,256,291,100,104,293,262,110,128,129,103,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139])). % 78.05/78.41 cnf(3088,plain, % 78.05/78.41 (P7(a4)), % 78.05/78.41 inference(scs_inference,[],[99,102,107,441,256,291,100,104,293,262,110,128,129,103,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134])). % 78.05/78.41 cnf(3091,plain, % 78.05/78.41 (~P11(f32(a13))), % 78.05/78.41 inference(scs_inference,[],[99,102,107,125,441,321,256,291,100,101,104,293,262,110,128,129,103,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148])). % 78.05/78.41 cnf(3093,plain, % 78.05/78.41 (~P11(f21(a13))), % 78.05/78.41 inference(scs_inference,[],[99,102,107,125,441,321,256,291,100,101,104,293,262,110,128,129,103,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149])). % 78.05/78.41 cnf(3095,plain, % 78.05/78.41 (~P11(f35(a17,a17))), % 78.05/78.41 inference(scs_inference,[],[99,102,107,125,441,321,256,291,100,101,104,293,262,110,128,129,103,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164])). % 78.05/78.41 cnf(3099,plain, % 78.05/78.41 (P13(f21(a13),f33(f32(a13)))), % 78.05/78.41 inference(scs_inference,[],[99,102,107,125,441,321,256,291,100,101,104,293,262,110,128,129,103,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163])). % 78.05/78.41 cnf(3102,plain, % 78.05/78.41 (P18(a24,f33(a25))), % 78.05/78.41 inference(scs_inference,[],[99,102,107,125,441,231,321,256,291,100,101,104,293,262,110,128,129,103,990,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159])). % 78.05/78.41 cnf(3105,plain, % 78.05/78.41 (~E(f16(f35(x31051,x31052)),a17)), % 78.05/78.41 inference(scs_inference,[],[99,102,107,125,441,231,321,256,291,100,101,104,293,262,110,128,129,103,990,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68])). % 78.05/78.41 cnf(3106,plain, % 78.05/78.41 (P11(f16(x31061))), % 78.05/78.41 inference(rename_variables,[],[110])). % 78.05/78.41 cnf(3107,plain, % 78.05/78.41 (P6(f30(a22))), % 78.05/78.41 inference(scs_inference,[],[99,102,107,125,441,231,321,256,291,100,101,104,293,262,110,128,129,103,990,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157])). % 78.05/78.41 cnf(3110,plain, % 78.05/78.41 (~P13(a17,f33(f16(x31101)))), % 78.05/78.41 inference(scs_inference,[],[99,102,107,125,441,231,321,256,291,100,101,104,293,262,110,3106,128,129,103,990,234,2694,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166])). % 78.05/78.41 cnf(3112,plain, % 78.05/78.41 (E(f31(a1,f32(a12),f34(a12),f36(a12),f37(a1,a12)),a12)), % 78.05/78.41 inference(scs_inference,[],[99,102,107,125,441,231,321,256,291,100,101,104,293,262,110,3106,128,129,103,990,234,2694,111,113,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166,211])). % 78.05/78.41 cnf(3132,plain, % 78.05/78.41 (~P26(f10(a1))), % 78.05/78.41 inference(scs_inference,[],[84,99,102,107,125,441,231,321,256,291,100,101,104,293,262,110,3106,128,129,103,990,234,2694,111,88,90,113,86,92,95,98,96,94,123,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166,211,168,169,170,171,172,173,174,175,176,177])). % 78.05/78.41 cnf(3140,plain, % 78.05/78.41 (P9(f9(a1),a1)), % 78.05/78.41 inference(scs_inference,[],[84,99,102,107,125,441,231,321,256,291,100,101,104,293,262,110,3106,128,129,103,990,234,2694,111,88,90,113,86,92,95,98,96,94,123,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166,211,168,169,170,171,172,173,174,175,176,177,178,179,180,181])). % 78.05/78.42 cnf(3142,plain, % 78.05/78.42 (P9(f10(a1),a1)), % 78.05/78.42 inference(scs_inference,[],[84,99,102,107,125,441,231,321,256,291,100,101,104,293,262,110,3106,128,129,103,990,234,2694,111,88,90,113,86,92,95,98,96,94,123,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166,211,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182])). % 78.05/78.42 cnf(3144,plain, % 78.05/78.42 (P1(f11(a1,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[84,99,102,107,125,441,231,321,256,291,100,101,104,293,262,251,110,3106,128,129,103,252,261,250,990,241,246,234,249,2694,111,88,90,113,86,92,95,98,96,94,123,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166,211,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,191])). % 78.05/78.42 cnf(3146,plain, % 78.05/78.42 (P23(f11(a1,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[84,99,102,107,125,441,231,321,256,291,100,101,104,293,262,251,110,3106,128,129,103,252,261,250,990,241,246,234,249,2694,111,88,90,113,86,92,95,98,96,94,123,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166,211,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,191,192])). % 78.05/78.42 cnf(3148,plain, % 78.05/78.42 (P27(f11(a1,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[84,99,102,107,125,441,231,321,256,291,100,101,104,293,262,251,110,3106,128,129,103,252,261,250,990,241,246,234,249,2694,111,88,90,113,86,92,95,98,96,94,123,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166,211,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,191,192,193])). % 78.05/78.42 cnf(3150,plain, % 78.05/78.42 (P28(f11(a1,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[84,99,102,107,125,441,231,321,256,291,100,101,104,293,262,251,110,3106,128,129,103,252,261,250,990,241,246,234,249,2694,111,88,90,113,86,92,95,98,96,94,123,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166,211,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,191,192,193,194])). % 78.05/78.42 cnf(3152,plain, % 78.05/78.42 (~P26(f11(a1,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[84,99,102,107,125,441,231,321,256,291,100,101,104,293,262,251,110,3106,128,129,103,252,261,250,990,241,246,234,249,2694,111,88,90,113,86,92,95,98,96,94,123,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166,211,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,191,192,193,194,197])). % 78.05/78.42 cnf(3154,plain, % 78.05/78.42 (P25(f11(a1,f29(a1,a12,a24)),a1)), % 78.05/78.42 inference(scs_inference,[],[84,99,102,107,125,441,231,321,256,291,100,101,104,293,262,251,110,3106,128,129,103,252,261,250,990,241,246,234,249,2694,111,88,90,113,86,92,95,98,96,94,123,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166,211,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,191,192,193,194,197,195])). % 78.05/78.42 cnf(3156,plain, % 78.05/78.42 (P29(f11(a1,f29(a1,a12,a24)),a1)), % 78.05/78.42 inference(scs_inference,[],[84,99,102,107,125,441,231,321,256,291,100,101,104,293,262,251,110,3106,128,129,103,252,261,250,990,241,246,234,249,2694,111,88,90,113,86,92,95,98,96,94,123,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166,211,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,191,192,193,194,197,195,196])). % 78.05/78.42 cnf(3158,plain, % 78.05/78.42 (P15(f7(a1,f29(a1,a12,a24)),a1,f29(a1,a12,a24))), % 78.05/78.42 inference(scs_inference,[],[84,99,102,107,125,441,231,321,256,291,100,101,104,293,262,251,110,3106,128,129,103,252,261,250,990,241,246,234,249,2694,111,88,90,113,86,92,95,98,96,94,123,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166,211,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,191,192,193,194,197,195,196,198])). % 78.05/78.42 cnf(3160,plain, % 78.05/78.42 (P15(f11(a1,f29(a1,a12,a24)),a1,f29(a1,a12,a24))), % 78.05/78.42 inference(scs_inference,[],[84,99,102,107,125,441,231,321,256,291,100,101,104,293,262,251,110,3106,128,129,103,252,261,250,990,241,246,234,249,2694,111,88,90,113,86,92,95,98,96,94,123,141,142,143,144,145,146,147,160,186,187,155,156,4,5,6,7,26,27,28,29,30,31,32,35,36,188,8,9,15,16,17,18,22,23,24,25,33,34,19,20,184,185,364,466,507,538,2294,10,11,12,13,14,2318,131,136,138,132,137,21,133,135,139,134,2,148,149,164,165,163,83,159,68,157,3,166,211,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,191,192,193,194,197,195,196,198,199])). % 78.05/78.42 cnf(3193,plain, % 78.05/78.42 (P12(a28,a12)), % 78.05/78.42 inference(scs_inference,[],[3071,531])). % 78.05/78.42 cnf(3194,plain, % 78.05/78.42 (E(f16(x31941),a28)), % 78.05/78.42 inference(rename_variables,[],[3071])). % 78.05/78.42 cnf(3195,plain, % 78.05/78.42 (P16(f34(a2),f35(f32(a2),f32(a2)),f32(a2))), % 78.05/78.42 inference(scs_inference,[],[3073,3071,531,185])). % 78.05/78.42 cnf(3199,plain, % 78.05/78.42 (P9(f20(a23),a23)), % 78.05/78.42 inference(scs_inference,[],[3073,3077,3071,3058,531,185,186,146])). % 78.05/78.42 cnf(3203,plain, % 78.05/78.42 (~P26(f19(a1))), % 78.05/78.42 inference(scs_inference,[],[3073,3077,3082,3071,3058,3061,531,185,186,146,187,143])). % 78.05/78.42 cnf(3207,plain, % 78.05/78.42 (E(a14,a28)), % 78.05/78.42 inference(scs_inference,[],[3073,3077,3082,3071,3058,3061,109,531,185,186,146,187,143,144,131])). % 78.05/78.42 cnf(3209,plain, % 78.05/78.42 (P13(f8(x32091,x32092),f33(f35(x32091,x32092)))), % 78.05/78.42 inference(scs_inference,[],[3073,3077,3082,3071,3058,3061,109,122,531,185,186,146,187,143,144,131,188])). % 78.05/78.42 cnf(3211,plain, % 78.05/78.42 (P19(f34(a2))), % 78.05/78.42 inference(scs_inference,[],[3073,3077,3082,3071,3058,3061,109,122,531,185,186,146,187,143,144,131,188,141])). % 78.05/78.42 cnf(3213,plain, % 78.05/78.42 (P6(a1)), % 78.05/78.42 inference(scs_inference,[],[3073,3077,3082,3071,3058,3061,109,122,98,531,185,186,146,187,143,144,131,188,141,136])). % 78.05/78.42 cnf(3221,plain, % 78.05/78.42 (P9(f19(a1),a1)), % 78.05/78.42 inference(scs_inference,[],[3073,3077,3082,3071,3194,3058,3061,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147])). % 78.05/78.42 cnf(3225,plain, % 78.05/78.42 (P21(f34(a2),f35(f32(a2),f32(a2)),f32(a2))), % 78.05/78.42 inference(scs_inference,[],[3073,3077,3082,3071,3194,3058,3061,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184])). % 78.05/78.42 cnf(3229,plain, % 78.05/78.42 (P13(f29(a1,a12,a24),f33(a12))), % 78.05/78.42 inference(scs_inference,[],[3073,3077,3082,3071,3194,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160])). % 78.05/78.42 cnf(3231,plain, % 78.05/78.42 (E(f33(f16(x32311)),f33(a28))), % 78.05/78.42 inference(scs_inference,[],[3073,3077,3082,3071,3194,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7])). % 78.05/78.42 cnf(3232,plain, % 78.05/78.42 (E(f31(x32321,x32322,x32323,f16(x32324),x32325),f31(x32321,x32322,x32323,a28,x32325))), % 78.05/78.42 inference(scs_inference,[],[3073,3077,3082,3071,3194,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13])). % 78.05/78.42 cnf(3233,plain, % 78.05/78.42 (~P11(f15(f15(a17)))), % 78.05/78.42 inference(scs_inference,[],[3073,3077,3082,3005,3071,3194,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142])). % 78.05/78.42 cnf(3235,plain, % 78.05/78.42 (E(f31(x32351,x32352,x32353,x32354,f16(x32355)),f31(x32351,x32352,x32353,x32354,a28))), % 78.05/78.42 inference(scs_inference,[],[3073,3077,3082,3005,3071,3194,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14])). % 78.05/78.42 cnf(3236,plain, % 78.05/78.42 (P4(a4)), % 78.05/78.42 inference(scs_inference,[],[3073,3075,3077,3082,3005,3071,3194,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133])). % 78.05/78.42 cnf(3242,plain, % 78.05/78.42 (P8(a2)), % 78.05/78.42 inference(scs_inference,[],[3073,3075,3077,3082,3086,3005,3071,3194,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138])). % 78.05/78.42 cnf(3244,plain, % 78.05/78.42 (P9(f30(a1),a1)), % 78.05/78.42 inference(scs_inference,[],[3073,3075,3077,3082,3086,3005,3071,3194,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145])). % 78.05/78.42 cnf(3246,plain, % 78.05/78.42 (E(f35(x32461,f16(x32462)),f35(x32461,a28))), % 78.05/78.42 inference(scs_inference,[],[3073,3075,3077,3082,3086,3005,3071,3194,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9])). % 78.05/78.42 cnf(3247,plain, % 78.05/78.42 (P14(f6(f29(a1,a12,a24),a28),a12,f16(x32471))), % 78.05/78.42 inference(scs_inference,[],[3073,3075,3077,3082,3086,3005,3071,3194,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466])). % 78.05/78.42 cnf(3252,plain, % 78.05/78.42 (P4(a27)), % 78.05/78.42 inference(scs_inference,[],[3073,3075,3077,3082,3084,3086,3005,3071,3194,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132])). % 78.05/78.42 cnf(3260,plain, % 78.05/78.42 (P14(f6(a28,f29(a1,a12,a24)),f16(x32601),a12)), % 78.05/78.42 inference(scs_inference,[],[3073,3075,3077,3082,3084,3086,3005,3071,3194,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538])). % 78.05/78.42 cnf(3266,plain, % 78.05/78.42 (P8(f30(a22))), % 78.05/78.42 inference(scs_inference,[],[3073,3075,3077,3082,3084,3086,3005,3071,3194,3107,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137])). % 78.05/78.42 cnf(3269,plain, % 78.05/78.42 (P16(f8(a28,f29(a1,a12,a24)),f16(x32691),a12)), % 78.05/78.42 inference(scs_inference,[],[3073,3075,3077,3082,3084,3086,3005,3071,3194,3107,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507])). % 78.05/78.42 cnf(3275,plain, % 78.05/78.42 (P7(a2)), % 78.05/78.42 inference(scs_inference,[],[3073,3075,3077,3082,3084,3086,3088,3005,3071,3194,3107,3058,3061,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507,35,5,16,135,134])). % 78.05/78.42 cnf(3278,plain, % 78.05/78.42 (P10(a1)), % 78.05/78.42 inference(scs_inference,[],[3073,3075,3077,3082,3084,3086,3088,3005,3071,3194,3107,3058,3061,3105,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507,35,5,16,135,134,2,139])). % 78.05/78.42 cnf(3280,plain, % 78.05/78.42 (~P11(f35(f15(a17),f15(a17)))), % 78.05/78.42 inference(scs_inference,[],[3073,3075,3077,3082,3084,3086,3088,3005,3071,3194,3107,3058,3061,3105,258,109,122,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507,35,5,16,135,134,2,139,164])). % 78.05/78.42 cnf(3283,plain, % 78.05/78.42 (~E(f33(a25),a14)), % 78.05/78.42 inference(scs_inference,[],[280,3073,3075,3077,3082,3084,3086,3088,3005,3071,3194,3107,3102,3058,3061,3105,3112,258,109,122,124,98,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507,35,5,16,135,134,2,139,164,47,66])). % 78.05/78.42 cnf(3285,plain, % 78.05/78.42 (~P11(f21(a1))), % 78.05/78.42 inference(scs_inference,[],[280,3073,3075,3077,3082,3084,3086,3088,3005,3071,3194,3107,3102,3058,3061,3105,3112,258,109,122,124,98,123,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507,35,5,16,135,134,2,139,164,47,66,149])). % 78.05/78.42 cnf(3289,plain, % 78.05/78.42 (~P11(f32(a1))), % 78.05/78.42 inference(scs_inference,[],[280,3073,3075,3077,3082,3084,3086,3088,3005,3071,3194,3107,3013,3102,3058,3061,3105,3112,258,109,122,100,124,98,123,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507,35,5,16,135,134,2,139,164,47,66,149,165,148])). % 78.05/78.42 cnf(3291,plain, % 78.05/78.42 (P13(f21(a1),f33(f32(a1)))), % 78.05/78.42 inference(scs_inference,[],[280,3073,3075,3077,3082,3084,3086,3088,3005,3071,3194,3107,3013,3102,3058,3061,3105,3112,258,109,122,100,124,98,123,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507,35,5,16,135,134,2,139,164,47,66,149,165,148,163])). % 78.05/78.42 cnf(3293,plain, % 78.05/78.42 (P11(f5(f33(a14)))), % 78.05/78.42 inference(scs_inference,[],[280,3073,3075,3077,3082,3084,3086,3088,3005,3071,3194,3107,3013,3102,3058,3061,3105,3112,258,109,122,288,100,116,124,98,123,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507,35,5,16,135,134,2,139,164,47,66,149,165,148,163,159])). % 78.05/78.42 cnf(3297,plain, % 78.05/78.42 (~E(a28,f15(a17))), % 78.05/78.42 inference(scs_inference,[],[280,3073,3075,3077,3082,3084,3086,3088,3005,3071,3194,3107,3013,3102,3058,3061,3105,3112,258,108,109,122,288,100,116,124,98,123,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507,35,5,16,135,134,2,139,164,47,66,149,165,148,163,159,68])). % 78.05/78.42 cnf(3298,plain, % 78.05/78.42 (P6(f20(a22))), % 78.05/78.42 inference(scs_inference,[],[280,3073,3075,3077,3082,3084,3086,3088,3005,3071,3194,3107,3013,3102,3058,3061,3105,3112,258,108,109,122,288,100,116,124,98,123,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507,35,5,16,135,134,2,139,164,47,66,149,165,148,163,159,68,157])). % 78.05/78.42 cnf(3302,plain, % 78.05/78.42 (~P13(f33(a25),f33(a28))), % 78.05/78.42 inference(scs_inference,[],[280,3073,3075,3077,3082,3084,3086,3088,3005,3071,3194,3107,3013,3102,3058,3061,3105,3112,258,108,109,122,288,100,116,124,98,123,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507,35,5,16,135,134,2,139,164,47,66,149,165,148,163,159,68,157,3,166])). % 78.05/78.42 cnf(3304,plain, % 78.05/78.42 (~E(f5(f33(a28)),f33(a25))), % 78.05/78.42 inference(scs_inference,[],[280,3073,3075,3077,3082,3084,3086,3088,3005,3071,3194,3107,3013,3102,3058,3061,3105,3112,258,108,109,122,288,100,116,124,98,123,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507,35,5,16,135,134,2,139,164,47,66,149,165,148,163,159,68,157,3,166,556])). % 78.05/78.42 cnf(3305,plain, % 78.05/78.42 (~E(f16(a28),f33(a25))), % 78.05/78.42 inference(scs_inference,[],[280,3073,3075,3077,3082,3084,3086,3088,3005,3071,3194,3107,3013,3102,3058,3061,3105,3112,258,108,109,122,288,100,116,124,98,123,531,185,186,146,187,143,144,131,188,141,136,23,24,33,36,19,31,147,28,27,184,20,32,160,7,13,142,14,133,15,156,25,138,145,9,466,29,22,34,30,132,18,12,17,11,10,2294,538,8,26,6,364,4,137,21,507,35,5,16,135,134,2,139,164,47,66,149,165,148,163,159,68,157,3,166,556,547])). % 78.05/78.42 cnf(3311,plain, % 78.05/78.42 (P14(f34(a2),f35(f32(a2),f32(a2)),f32(a2))), % 78.05/78.42 inference(scs_inference,[],[3195,186])). % 78.05/78.42 cnf(3315,plain, % 78.05/78.42 (P9(f20(a4),a4)), % 78.05/78.42 inference(scs_inference,[],[3236,3195,186,143,146])). % 78.05/78.42 cnf(3319,plain, % 78.05/78.42 (P9(f19(a4),a4)), % 78.05/78.42 inference(scs_inference,[],[3236,3298,3195,186,143,146,141,147])). % 78.05/78.42 cnf(3321,plain, % 78.05/78.42 (P16(f34(a1),f35(f32(a1),f32(a1)),f32(a1))), % 78.05/78.42 inference(scs_inference,[],[3213,3236,3298,3195,186,143,146,141,147,185])). % 78.05/78.42 cnf(3325,plain, % 78.05/78.42 (P9(f30(a4),a4)), % 78.05/78.42 inference(scs_inference,[],[3213,3236,3298,3195,186,143,146,141,147,185,144,145])). % 78.05/78.42 cnf(3327,plain, % 78.05/78.42 (E(f5(f33(a14)),a28)), % 78.05/78.42 inference(scs_inference,[],[3213,3236,3298,3195,3293,186,143,146,141,147,185,144,145,131])). % 78.05/78.42 cnf(3331,plain, % 78.05/78.42 (P4(a26)), % 78.05/78.42 inference(scs_inference,[],[3079,3213,3236,3298,3195,3247,3293,186,143,146,141,147,185,144,145,131,187,133])). % 78.05/78.42 cnf(3333,plain, % 78.05/78.42 (E(f34(a14),f34(a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3207,3213,3236,3298,3195,3247,3293,186,143,146,141,147,185,144,145,131,187,133,28])). % 78.05/78.42 cnf(3334,plain, % 78.05/78.42 (E(f29(x33341,a14,x33342),f29(x33341,a28,x33342))), % 78.05/78.42 inference(scs_inference,[],[3079,3207,3213,3236,3298,3195,3247,3293,186,143,146,141,147,185,144,145,131,187,133,28,20])). % 78.05/78.42 cnf(3337,plain, % 78.05/78.42 (E(f33(a14),f33(a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3207,3213,3236,3298,3195,3247,3293,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7])). % 78.05/78.42 cnf(3338,plain, % 78.05/78.42 (E(f29(a14,x33381,x33382),f29(a28,x33381,x33382))), % 78.05/78.42 inference(scs_inference,[],[3079,3207,3213,3236,3298,3195,3247,3293,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19])). % 78.05/78.42 cnf(3340,plain, % 78.05/78.42 (~P11(f15(f32(a13)))), % 78.05/78.42 inference(scs_inference,[],[3079,3207,3213,3236,3091,3298,3195,3247,3293,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142])). % 78.05/78.42 cnf(3343,plain, % 78.05/78.42 (P13(f36(a2),f32(a2))), % 78.05/78.42 inference(scs_inference,[],[3079,3207,3213,3236,3242,3091,3298,3195,3247,3293,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156])). % 78.05/78.42 cnf(3345,plain, % 78.05/78.42 (E(f15(a14),f15(a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3207,3213,3236,3242,3091,3298,3195,3247,3293,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29])). % 78.05/78.42 cnf(3346,plain, % 78.05/78.42 (P13(a28,f33(a12))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3091,3298,3195,3247,3293,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160])). % 78.05/78.42 cnf(3348,plain, % 78.05/78.42 (E(f9(a14),f9(a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3091,3298,3195,3247,3293,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27])). % 78.05/78.42 cnf(3349,plain, % 78.05/78.42 (E(f31(x33491,x33492,x33493,a14,x33494),f31(x33491,x33492,x33493,a28,x33494))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3091,3298,3195,3247,3293,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13])). % 78.05/78.42 cnf(3350,plain, % 78.05/78.42 (E(f7(x33501,a12),f7(x33501,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34])). % 78.05/78.42 cnf(3354,plain, % 78.05/78.42 (E(f31(x33541,x33542,x33543,x33544,a14),f31(x33541,x33542,x33543,x33544,a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14])). % 78.05/78.42 cnf(3355,plain, % 78.05/78.42 (E(f19(a14),f19(a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30])). % 78.05/78.42 cnf(3356,plain, % 78.05/78.42 (P8(f20(a22))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137])). % 78.05/78.42 cnf(3358,plain, % 78.05/78.42 (P4(a2)), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132])). % 78.05/78.42 cnf(3360,plain, % 78.05/78.42 (E(f20(a14),f20(a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31])). % 78.05/78.42 cnf(3361,plain, % 78.05/78.42 (E(f6(x33611,a14),f6(x33611,a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23])). % 78.05/78.42 cnf(3362,plain, % 78.05/78.42 (E(f8(a14,x33621),f8(a28,x33621))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24])). % 78.05/78.42 cnf(3363,plain, % 78.05/78.42 (E(f21(a14),f21(a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36])). % 78.05/78.42 cnf(3364,plain, % 78.05/78.42 (E(f8(x33641,a14),f8(x33641,a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25])). % 78.05/78.42 cnf(3366,plain, % 78.05/78.42 (E(f32(a14),f32(a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6])). % 78.05/78.42 cnf(3371,plain, % 78.05/78.42 (E(f6(a14,x33711),f6(a28,x33711))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22])). % 78.05/78.42 cnf(3373,plain, % 78.05/78.42 (P14(f6(a28,f29(a1,a12,a24)),a14,a12)), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538])). % 78.05/78.42 cnf(3376,plain, % 78.05/78.42 (E(f31(a14,x33761,x33762,x33763,x33764),f31(a28,x33761,x33762,x33763,x33764))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10])). % 78.05/78.42 cnf(3377,plain, % 78.05/78.42 (E(f10(a14),f10(a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26])). % 78.05/78.42 cnf(3378,plain, % 78.05/78.42 (E(f31(x33781,x33782,a14,x33783,x33784),f31(x33781,x33782,a28,x33783,x33784))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12])). % 78.05/78.42 cnf(3379,plain, % 78.05/78.42 (P16(f8(a28,f29(a1,a12,a24)),a14,a12)), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507])). % 78.05/78.42 cnf(3380,plain, % 78.05/78.42 (E(f31(x33801,a14,x33802,x33803,x33804),f31(x33801,a28,x33802,x33803,x33804))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507,11])). % 78.05/78.42 cnf(3381,plain, % 78.05/78.42 (E(f16(a14),f16(a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507,11,4])). % 78.05/78.42 cnf(3382,plain, % 78.05/78.42 (E(f36(a14),f36(a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507,11,4,35])). % 78.05/78.42 cnf(3383,plain, % 78.05/78.42 (E(f5(a14),f5(a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507,11,4,35,5])). % 78.05/78.42 cnf(3384,plain, % 78.05/78.42 (P7(a1)), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3278,3091,3298,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507,11,4,35,5,134])). % 78.05/78.42 cnf(3386,plain, % 78.05/78.42 (~E(f33(a25),f16(a28))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3278,3091,3298,3305,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507,11,4,35,5,134,2])). % 78.05/78.42 cnf(3387,plain, % 78.05/78.42 (~P11(f35(f32(a13),f32(a13)))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3278,3091,3298,3305,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507,11,4,35,5,134,2,164])). % 78.05/78.42 cnf(3389,plain, % 78.05/78.42 (~P13(f33(a25),f33(f16(x33891)))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3278,3091,3298,3302,3305,3231,3195,3247,3293,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507,11,4,35,5,134,2,164,43])). % 78.05/78.42 cnf(3392,plain, % 78.05/78.42 (P18(f29(a1,a12,a24),f33(a12))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3278,3140,3229,3091,3298,3302,3305,3231,3195,3247,3293,129,3082,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507,11,4,35,5,134,2,164,43,165,159])). % 78.05/78.42 cnf(3395,plain, % 78.05/78.42 (P6(f20(a4))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3278,3140,3229,3091,3298,3302,3305,3231,3195,3247,3293,129,3082,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507,11,4,35,5,134,2,164,43,165,159,157])). % 78.05/78.42 cnf(3397,plain, % 78.05/78.42 (~E(f5(f33(a14)),f32(a13))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3278,3140,3229,3091,3298,3302,3305,3231,3195,3247,3293,129,3082,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507,11,4,35,5,134,2,164,43,165,159,157,68])). % 78.05/78.42 cnf(3403,plain, % 78.05/78.42 (P14(f6(f29(a1,a12,a24),a28),a12,a14)), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3278,3140,3229,3091,3298,3302,3305,3232,3235,3231,3195,3247,3293,129,3082,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507,11,4,35,5,134,2,164,43,165,159,157,68,3,2318,547,466])). % 78.05/78.42 cnf(3404,plain, % 78.05/78.42 (~P18(f33(a12),f29(a1,a12,a24))), % 78.05/78.42 inference(scs_inference,[],[3079,3193,3207,3213,3236,3242,3275,3278,3140,3229,3091,3298,3302,3305,3232,3235,3231,3195,3247,3293,129,3082,228,186,143,146,141,147,185,144,145,131,187,133,28,20,184,7,19,32,142,9,156,29,160,27,13,34,135,18,14,30,137,132,31,23,24,36,25,33,6,16,21,364,17,22,15,538,2294,8,10,26,12,507,11,4,35,5,134,2,164,43,165,159,157,68,3,2318,547,466,161])). % 78.05/78.42 cnf(3413,plain, % 78.05/78.42 (P9(f20(a27),a27)), % 78.05/78.42 inference(scs_inference,[],[3252,146])). % 78.05/78.42 cnf(3419,plain, % 78.05/78.42 (P4(f30(a22))), % 78.05/78.42 inference(scs_inference,[],[3252,3266,3395,3269,146,186,141,133])). % 78.05/78.42 cnf(3421,plain, % 78.05/78.42 (~P26(f19(a27))), % 78.05/78.42 inference(scs_inference,[],[3252,3266,3395,3269,146,186,141,133,143])). % 78.05/78.42 cnf(3429,plain, % 78.05/78.42 (P9(f30(a27),a27)), % 78.05/78.42 inference(scs_inference,[],[3252,3093,3266,3395,3260,3269,146,186,141,133,143,187,144,142,145])). % 78.05/78.42 cnf(3431,plain, % 78.05/78.42 (P9(f19(a27),a27)), % 78.05/78.42 inference(scs_inference,[],[3252,3093,3266,3395,3260,3269,146,186,141,133,143,187,144,142,145,147])). % 78.05/78.42 cnf(3433,plain, % 78.05/78.42 (P13(f16(f29(a1,a12,a24)),f33(a12))), % 78.05/78.42 inference(scs_inference,[],[3252,3093,3266,3395,3260,3269,319,146,186,141,133,143,187,144,142,145,147,160])). % 78.05/78.42 cnf(3435,plain, % 78.05/78.42 (E(f29(a12,x34351,x34352),f29(f29(a1,a12,a24),x34351,x34352))), % 78.05/78.42 inference(scs_inference,[],[3252,3093,3266,3395,3260,3269,319,228,146,186,141,133,143,187,144,142,145,147,160,19])). % 78.05/78.42 cnf(3441,plain, % 78.05/78.42 (E(f7(x34411,f29(a1,a12,a24)),f7(x34411,a12))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34])). % 78.05/78.42 cnf(3443,plain, % 78.05/78.42 (E(f8(a12,x34431),f8(f29(a1,a12,a24),x34431))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24])). % 78.05/78.42 cnf(3448,plain, % 78.05/78.42 (E(f29(x34481,a12,x34482),f29(x34481,f29(a1,a12,a24),x34482))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20])). % 78.05/78.42 cnf(3449,plain, % 78.05/78.42 (E(f33(a12),f33(f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7])). % 78.05/78.42 cnf(3451,plain, % 78.05/78.42 (E(f37(x34511,a12),f37(x34511,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16])). % 78.05/78.42 cnf(3453,plain, % 78.05/78.42 (E(f31(x34531,x34532,x34533,x34534,a12),f31(x34531,x34532,x34533,x34534,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14])). % 78.05/78.42 cnf(3454,plain, % 78.05/78.42 (P8(f20(a4))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137])). % 78.05/78.42 cnf(3456,plain, % 78.05/78.42 (E(f29(x34561,x34562,a12),f29(x34561,x34562,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21])). % 78.05/78.42 cnf(3458,plain, % 78.05/78.42 (E(f8(x34581,a12),f8(x34581,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21,17,25])). % 78.05/78.42 cnf(3459,plain, % 78.05/78.42 (E(f6(x34591,a12),f6(x34591,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21,17,25,23])). % 78.05/78.42 cnf(3460,plain, % 78.05/78.42 (E(f11(x34601,a12),f11(x34601,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21,17,25,23,18])). % 78.05/78.42 cnf(3462,plain, % 78.05/78.42 (E(f31(x34621,x34622,x34623,a12,x34624),f31(x34621,x34622,x34623,f29(a1,a12,a24),x34624))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21,17,25,23,18,31,13])). % 78.05/78.42 cnf(3464,plain, % 78.05/78.42 (E(f37(a12,x34641),f37(f29(a1,a12,a24),x34641))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21,17,25,23,18,31,13,6,15])). % 78.05/78.42 cnf(3468,plain, % 78.05/78.42 (E(f6(a12,x34681),f6(f29(a1,a12,a24),x34681))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21,17,25,23,18,31,13,6,15,11,446,5,22])). % 78.05/78.42 cnf(3475,plain, % 78.05/78.42 (~E(a14,f33(a25))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3093,3266,3395,3283,3260,3269,105,319,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21,17,25,23,18,31,13,6,15,11,446,5,22,10,8,26,35,12,4,2])). % 78.05/78.42 cnf(3482,plain, % 78.05/78.42 (P13(f5(f31(x34821,x34822,x34823,a14,x34824)),f31(x34821,x34822,x34823,a28,x34824))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3349,3093,3266,3395,3283,3260,3269,105,319,629,631,633,635,116,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21,17,25,23,18,31,13,6,15,11,446,5,22,10,8,26,35,12,4,2,41,44,37,164,46,43])). % 78.05/78.42 cnf(3483,plain, % 78.05/78.42 (P13(f5(x34831),x34831)), % 78.05/78.42 inference(rename_variables,[],[116])). % 78.05/78.42 cnf(3486,plain, % 78.05/78.42 (P11(f5(f33(a28)))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3349,3093,3266,3395,3283,3260,3269,105,319,629,631,633,635,237,116,3483,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21,17,25,23,18,31,13,6,15,11,446,5,22,10,8,26,35,12,4,2,41,44,37,164,46,43,165,159])). % 78.05/78.42 cnf(3490,plain, % 78.05/78.42 (~P18(f33(a12),a12)), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3349,3404,3093,3266,3395,3283,3260,3269,105,319,629,631,633,635,237,116,3483,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21,17,25,23,18,31,13,6,15,11,446,5,22,10,8,26,35,12,4,2,41,44,37,164,46,43,165,159,66])). % 78.05/78.42 cnf(3491,plain, % 78.05/78.42 (P6(f10(a1))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3142,3349,3404,3093,3266,3395,3283,3260,3269,105,319,629,631,633,635,237,3082,116,3483,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21,17,25,23,18,31,13,6,15,11,446,5,22,10,8,26,35,12,4,2,41,44,37,164,46,43,165,159,66,157])). % 78.05/78.42 cnf(3493,plain, % 78.05/78.42 (~E(f5(f33(a14)),f21(a13))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3142,3349,3404,3093,3266,3395,3283,3260,3269,105,319,629,631,633,635,3293,237,3082,116,3483,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21,17,25,23,18,31,13,6,15,11,446,5,22,10,8,26,35,12,4,2,41,44,37,164,46,43,165,159,66,157,68])). % 78.05/78.42 cnf(3494,plain, % 78.05/78.42 (~E(f33(a25),f16(a14))), % 78.05/78.42 inference(scs_inference,[],[3252,3384,3142,3349,3404,3093,3266,3381,3386,3395,3283,3260,3269,105,319,629,631,633,635,3293,237,3082,116,3483,228,120,146,186,141,133,143,187,144,142,145,147,160,19,156,9,135,34,27,24,36,33,28,30,20,7,32,16,29,14,137,21,17,25,23,18,31,13,6,15,11,446,5,22,10,8,26,35,12,4,2,41,44,37,164,46,43,165,159,66,157,68,3])). % 78.05/78.42 cnf(3512,plain, % 78.05/78.42 (E(f5(f33(a28)),a28)), % 78.05/78.42 inference(scs_inference,[],[3486,131])). % 78.05/78.42 cnf(3516,plain, % 78.05/78.42 (P4(f20(a22))), % 78.05/78.42 inference(scs_inference,[],[3356,3321,3486,131,186,133])). % 78.05/78.42 cnf(3520,plain, % 78.05/78.42 (P9(f19(a2),a2)), % 78.05/78.42 inference(scs_inference,[],[3358,3356,3321,3486,131,186,133,146,147])). % 78.05/78.42 cnf(3526,plain, % 78.05/78.42 (P13(x35261,f33(x35261))), % 78.05/78.42 inference(scs_inference,[],[3358,3356,3491,3321,3063,3486,115,131,186,133,146,147,141,187,160])). % 78.05/78.42 cnf(3528,plain, % 78.05/78.42 (~P26(f19(a2))), % 78.05/78.42 inference(scs_inference,[],[3358,3356,3491,3321,3063,3486,115,131,186,133,146,147,141,187,160,143])). % 78.05/78.42 cnf(3530,plain, % 78.05/78.42 (P9(f30(a2),a2)), % 78.05/78.42 inference(scs_inference,[],[3358,3356,3491,3321,3063,3486,115,131,186,133,146,147,141,187,160,143,145])). % 78.05/78.42 cnf(3539,plain, % 78.05/78.42 (E(f29(f29(a1,a12,a24),x35391,x35392),f29(a12,x35391,x35392))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19])). % 78.05/78.42 cnf(3540,plain, % 78.05/78.42 (E(f34(f29(a1,a12,a24)),f34(a12))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28])). % 78.05/78.42 cnf(3541,plain, % 78.05/78.42 (E(f21(f29(a1,a12,a24)),f21(a12))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36])). % 78.05/78.42 cnf(3543,plain, % 78.05/78.42 (E(f35(x35431,f29(a1,a12,a24)),f35(x35431,a12))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9])). % 78.05/78.42 cnf(3545,plain, % 78.05/78.42 (E(f29(x35451,f29(a1,a12,a24),x35452),f29(x35451,a12,x35452))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20])). % 78.05/78.42 cnf(3546,plain, % 78.05/78.42 (P8(f10(a1))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137])). % 78.05/78.42 cnf(3548,plain, % 78.05/78.42 (E(f33(f29(a1,a12,a24)),f33(a12))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7])). % 78.05/78.42 cnf(3551,plain, % 78.05/78.42 (E(f11(x35511,f29(a1,a12,a24)),f11(x35511,a12))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18])). % 78.05/78.42 cnf(3552,plain, % 78.05/78.42 (E(f31(x35521,x35522,x35523,f29(a1,a12,a24),x35524),f31(x35521,x35522,x35523,a12,x35524))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13])). % 78.05/78.42 cnf(3554,plain, % 78.05/78.42 (E(f8(x35541,f29(a1,a12,a24)),f8(x35541,a12))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13,30,25])). % 78.05/78.42 cnf(3556,plain, % 78.05/78.42 (E(f8(f29(a1,a12,a24),x35561),f8(a12,x35561))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13,30,25,23,24])). % 78.05/78.42 cnf(3557,plain, % 78.05/78.42 (E(f37(x35571,f29(a1,a12,a24)),f37(x35571,a12))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13,30,25,23,24,16])). % 78.05/78.42 cnf(3559,plain, % 78.05/78.42 (E(f29(x35591,x35592,f29(a1,a12,a24)),f29(x35591,x35592,a12))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13,30,25,23,24,16,29,21])). % 78.05/78.42 cnf(3563,plain, % 78.05/78.42 (E(f37(f29(a1,a12,a24),x35631),f37(a12,x35631))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13,30,25,23,24,16,29,21,22,31,8,15])). % 78.05/78.42 cnf(3566,plain, % 78.05/78.42 (E(f31(x35661,x35662,f29(a1,a12,a24),x35663,x35664),f31(x35661,x35662,a12,x35663,x35664))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13,30,25,23,24,16,29,21,22,31,8,15,6,5,12])). % 78.05/78.42 cnf(3569,plain, % 78.05/78.42 (E(f31(x35691,f29(a1,a12,a24),x35692,x35693,x35694),f31(x35691,a12,x35692,x35693,x35694))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13,30,25,23,24,16,29,21,22,31,8,15,6,5,12,4,35,11])). % 78.05/78.42 cnf(3571,plain, % 78.05/78.42 (E(f31(f29(a1,a12,a24),x35711,x35712,x35713,x35714),f31(a12,x35711,x35712,x35713,x35714))), % 78.05/78.42 inference(scs_inference,[],[3358,3095,3356,3491,3321,3063,3486,106,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13,30,25,23,24,16,29,21,22,31,8,15,6,5,12,4,35,11,26,10])). % 78.05/78.42 cnf(3579,plain, % 78.05/78.42 (P6(f20(a2))), % 78.05/78.42 inference(scs_inference,[],[3358,3490,3095,3356,3491,3494,3321,3063,3486,106,3110,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13,30,25,23,24,16,29,21,22,31,8,15,6,5,12,4,35,11,26,10,2,65,164,165,43,157])). % 78.05/78.42 cnf(3582,plain, % 78.05/78.42 (P18(a28,f33(a12))), % 78.05/78.42 inference(scs_inference,[],[3358,3346,3490,3095,3356,3491,3494,3321,3063,3449,3486,3392,106,3110,129,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13,30,25,23,24,16,29,21,22,31,8,15,6,5,12,4,35,11,26,10,2,65,164,165,43,157,66,159])). % 78.05/78.42 cnf(3597,plain, % 78.05/78.42 (P14(f6(f29(a1,a12,a24),a12),a12,f29(a1,a12,a24))), % 78.05/78.42 inference(scs_inference,[],[3358,3346,3490,3095,3211,3343,3356,3491,3494,3225,3321,3311,3063,3453,3462,3449,3486,3392,106,3110,129,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13,30,25,23,24,16,29,21,22,31,8,15,6,5,12,4,35,11,26,10,2,65,164,165,43,157,66,159,68,3,212,213,2334,2292,2335,466])). % 78.05/78.42 cnf(3598,plain, % 78.05/78.42 (P12(f6(a12,x35981),f35(a12,x35981))), % 78.05/78.42 inference(scs_inference,[],[3358,3346,3490,3095,3211,3343,3356,3491,3494,3225,3321,3311,3063,3453,3462,3449,3486,3392,106,3110,129,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13,30,25,23,24,16,29,21,22,31,8,15,6,5,12,4,35,11,26,10,2,65,164,165,43,157,66,159,68,3,212,213,2334,2292,2335,466,2318])). % 78.05/78.42 cnf(3602,plain, % 78.05/78.42 (P14(f6(a12,f29(a1,a12,a24)),f29(a1,a12,a24),a12)), % 78.05/78.42 inference(scs_inference,[],[3358,3346,3490,3095,3211,3343,3356,3491,3494,3225,3321,3311,3063,3453,3462,3449,3486,3392,106,3110,129,115,120,131,186,133,146,147,141,187,160,143,145,142,144,156,33,19,28,36,32,9,27,20,137,7,14,17,18,13,30,25,23,24,16,29,21,22,31,8,15,6,5,12,4,35,11,26,10,2,65,164,165,43,157,66,159,68,3,212,213,2334,2292,2335,466,2318,507,364,2294,538])). % 78.05/78.42 cnf(3617,plain, % 78.05/78.42 (P4(f20(a4))), % 78.05/78.42 inference(scs_inference,[],[3419,3454,3062,146,186,145,133])). % 78.05/78.42 cnf(3627,plain, % 78.05/78.42 (P16(f6(f29(a1,a12,a24),a12),a12,f29(a1,a12,a24))), % 78.05/78.42 inference(scs_inference,[],[3285,3419,3454,3579,3597,3062,146,186,145,133,147,141,142,143,187])). % 78.05/78.42 cnf(3631,plain, % 78.05/78.42 (P8(f20(a2))), % 78.05/78.42 inference(scs_inference,[],[3285,3419,3454,3579,3597,3062,146,186,145,133,147,141,142,143,187,144,137])). % 78.05/78.42 cnf(3633,plain, % 78.05/78.42 (P14(f8(a12,x36331),a12,x36331)), % 78.05/78.42 inference(scs_inference,[],[3285,3419,3454,3579,3556,3597,3062,146,186,145,133,147,141,142,143,187,144,137,2294])). % 78.05/78.42 cnf(3636,plain, % 78.05/78.42 (P13(x36361,f33(x36361))), % 78.05/78.42 inference(rename_variables,[],[3526])). % 78.05/78.42 cnf(3642,plain, % 78.05/78.42 (~E(f16(x36421),f33(a25))), % 78.05/78.42 inference(scs_inference,[],[3526,3636,3285,3419,3454,3579,3015,3297,3556,3597,3062,3389,100,146,186,145,133,147,141,142,143,187,144,137,2294,2,167,164,165,42])). % 78.05/78.42 cnf(3644,plain, % 78.05/78.42 (P13(f5(f31(x36441,x36442,x36443,a14,a14)),f31(x36441,x36442,x36443,a28,a28))), % 78.05/78.42 inference(scs_inference,[],[3526,3636,3285,3419,3454,3579,3015,3297,3482,3556,3597,3062,3354,3389,100,146,186,145,133,147,141,142,143,187,144,137,2294,2,167,164,165,42,43])). % 78.05/78.42 cnf(3647,plain, % 78.05/78.42 (P6(f19(a22))), % 78.05/78.42 inference(scs_inference,[],[3526,3636,3285,3419,3454,3579,3015,3297,3482,3556,3597,3062,3354,3389,100,146,186,145,133,147,141,142,143,187,144,137,2294,2,167,164,165,42,43,157])). % 78.05/78.42 cnf(3649,plain, % 78.05/78.42 (~E(f33(a12),a14)), % 78.05/78.42 inference(scs_inference,[],[3526,3636,3285,3419,3454,3579,3015,3297,3582,3482,3556,3597,3062,3354,3389,280,100,146,186,145,133,147,141,142,143,187,144,137,2294,2,167,164,165,42,43,157,66])). % 78.05/78.42 cnf(3652,plain, % 78.05/78.42 (~E(a28,f33(a25))), % 78.05/78.42 inference(scs_inference,[],[3526,3636,3285,3419,3454,3579,3015,3297,3475,3582,3482,3556,3597,3062,3354,3389,280,3486,100,3207,146,186,145,133,147,141,142,143,187,144,137,2294,2,167,164,165,42,43,157,66,68,3])). % 78.05/78.42 cnf(3681,plain, % 78.05/78.42 (P4(f10(a1))), % 78.05/78.42 inference(scs_inference,[],[3516,3546,3379,186,146,133])). % 78.05/78.42 cnf(3697,plain, % 78.05/78.42 (P8(f19(a22))), % 78.05/78.42 inference(scs_inference,[],[3516,3546,3647,3602,3379,3289,186,146,133,145,144,141,187,143,147,142,137])). % 78.05/78.42 cnf(3704,plain, % 78.05/78.42 (P16(f37(a1,a12),f35(f32(a12),f32(a1)),f32(a12))), % 78.05/78.42 inference(scs_inference,[],[3642,3516,3546,3647,3602,3379,3289,3132,3082,113,186,146,133,145,144,141,187,143,147,142,137,2,189,149,190])). % 78.05/78.42 cnf(3710,plain, % 78.05/78.42 (P14(f8(a12,x37101),a12,x37101)), % 78.05/78.42 inference(rename_variables,[],[3633])). % 78.05/78.42 cnf(3717,plain, % 78.05/78.42 (P14(f8(a12,a12),a12,f29(a1,a12,a24))), % 78.05/78.42 inference(scs_inference,[],[3642,3633,3710,3516,3546,3647,3602,3627,3379,3598,3540,3543,3459,3333,3554,3289,115,3132,3082,113,186,146,133,145,144,141,187,143,147,142,137,2,189,149,190,73,40,69,72,148,38])). % 78.05/78.42 cnf(3722,plain, % 78.05/78.42 (~P11(f35(f32(a1),f32(a1)))), % 78.05/78.42 inference(scs_inference,[],[3642,3633,3710,3516,3546,3647,3199,3602,3627,3379,3598,3540,3543,3459,3333,3554,3289,3077,115,3132,3082,113,186,146,133,145,144,141,187,143,147,142,137,2,189,149,190,73,40,69,72,148,38,165,164])). % 78.05/78.42 cnf(3725,plain, % 78.05/78.42 (P13(x37251,f33(x37251))), % 78.05/78.42 inference(rename_variables,[],[3526])). % 78.05/78.42 cnf(3726,plain, % 78.05/78.42 (P6(f20(f20(a22)))), % 78.05/78.42 inference(scs_inference,[],[3642,3633,3710,3516,3546,3647,3199,3602,3627,3379,3598,3540,3543,3459,3333,3554,3526,3289,3077,115,3132,3082,113,186,146,133,145,144,141,187,143,147,142,137,2,189,149,190,73,40,69,72,148,38,165,164,42,157])). % 78.05/78.42 cnf(3728,plain, % 78.05/78.42 (~P13(f33(a25),f33(a14))), % 78.05/78.42 inference(scs_inference,[],[3642,3633,3710,3516,3546,3647,3199,3602,3627,3379,3598,3540,3543,3459,3333,3337,3554,3526,3289,3302,3077,115,3132,3082,113,186,146,133,145,144,141,187,143,147,142,137,2,189,149,190,73,40,69,72,148,38,165,164,42,157,43])). % 78.05/78.42 cnf(3729,plain, % 78.05/78.42 (P16(f8(x37291,f34(a14)),x37291,f34(a28))), % 78.05/78.42 inference(scs_inference,[],[3642,3633,3710,3516,3546,3647,3199,3602,3627,3379,3598,3540,3543,3459,3333,3337,3554,3526,3289,3302,3077,122,115,3132,3082,113,186,146,133,145,144,141,187,143,147,142,137,2,189,149,190,73,40,69,72,148,38,165,164,42,157,43,71])). % 78.05/78.42 cnf(3731,plain, % 78.05/78.42 (P18(a28,f33(f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[3642,3633,3710,3516,3546,3647,3199,3602,3627,3379,3598,3540,3543,3459,3333,3337,3554,3526,3289,3449,3582,3302,3077,122,115,3132,3082,113,186,146,133,145,144,141,187,143,147,142,137,2,189,149,190,73,40,69,72,148,38,165,164,42,157,43,71,66])). % 78.05/78.42 cnf(3737,plain, % 78.05/78.42 (E(f31(x37371,x37372,f29(a1,a12,a24),f29(a1,a12,a24),x37373),f31(x37371,x37372,a12,a12,x37373))), % 78.05/78.42 inference(scs_inference,[],[3642,3633,3710,3516,3546,3647,3199,3602,3627,3379,3233,3019,3598,3540,3552,3566,3543,3459,3333,3337,3554,3526,3289,3449,3582,3302,3077,262,110,122,115,3132,3082,113,186,146,133,145,144,141,187,143,147,142,137,2,189,149,190,73,40,69,72,148,38,165,164,42,157,43,71,66,70,39,68,3])). % 78.05/78.42 cnf(3741,plain, % 78.05/78.42 (P13(x37411,f33(x37411))), % 78.05/78.42 inference(rename_variables,[],[3526])). % 78.05/78.42 cnf(3743,plain, % 78.05/78.42 (P25(f29(a1,a12,f32(a12)),a1)), % 78.05/78.42 inference(scs_inference,[],[84,3642,3633,3710,3516,3546,3647,3199,3602,3627,3379,3233,3019,3598,3540,3552,3566,3543,3459,3333,3337,3554,3526,3725,3741,3289,3449,3582,3302,3077,262,110,122,115,3132,3082,85,87,89,91,124,112,113,88,90,97,127,93,86,92,95,96,98,94,123,186,146,133,145,144,141,187,143,147,142,137,2,189,149,190,73,40,69,72,148,38,165,164,42,157,43,71,66,70,39,68,3,208,207])). % 78.05/78.42 cnf(3748,plain, % 78.05/78.42 (~E(f5(f33(a14)),f33(a25))), % 78.05/78.42 inference(scs_inference,[],[84,3642,3633,3710,3516,3546,3647,3199,3602,3627,3379,3233,3019,3598,3540,3552,3566,3543,3459,3333,3337,3554,3526,3725,3741,3289,3449,3582,3302,3077,262,110,122,115,3132,3082,85,87,89,91,124,112,113,88,90,97,127,93,86,92,95,96,98,94,123,186,146,133,145,144,141,187,143,147,142,137,2,189,149,190,73,40,69,72,148,38,165,164,42,157,43,71,66,70,39,68,3,208,207,158,556])). % 78.05/78.42 cnf(3766,plain, % 78.05/78.42 (P4(f20(a2))), % 78.05/78.42 inference(scs_inference,[],[3617,3631,3704,186,146,145,144,143,147,133])). % 78.05/78.42 cnf(3770,plain, % 78.05/78.42 (~P11(f15(f33(x37701)))), % 78.05/78.42 inference(scs_inference,[],[3617,3631,3704,3107,129,186,146,145,144,143,147,133,141,142])). % 78.05/78.42 cnf(3774,plain, % 78.05/78.42 (P8(f20(f20(a22)))), % 78.05/78.42 inference(scs_inference,[],[3617,3631,3717,3704,3726,3107,129,186,146,145,144,143,147,133,141,142,187,137])). % 78.05/78.42 cnf(3776,plain, % 78.05/78.42 (~E(a14,f33(a12))), % 78.05/78.42 inference(scs_inference,[],[3617,3631,3717,3649,3704,3726,3107,129,186,146,145,144,143,147,133,141,142,187,137,2])). % 78.05/78.42 cnf(3777,plain, % 78.05/78.42 (~P26(f11(a1,a12))), % 78.05/78.42 inference(scs_inference,[],[3617,3631,3717,3649,3704,3152,3726,3460,3107,129,186,146,145,144,143,147,133,141,142,187,137,2,47])). % 78.05/78.42 cnf(3779,plain, % 78.05/78.42 (P15(f7(a1,a12),a1,f29(a1,a12,a24))), % 78.05/78.42 inference(scs_inference,[],[3617,3631,3717,3649,3704,3158,3152,3726,3441,3460,3107,129,186,146,145,144,143,147,133,141,142,187,137,2,47,78])). % 78.05/78.42 cnf(3783,plain, % 78.05/78.42 (~P11(f35(f33(x37831),f33(x37831)))), % 78.05/78.42 inference(scs_inference,[],[3617,3631,3717,3315,3649,3704,3158,3152,3726,3441,3460,3107,3236,129,186,146,145,144,143,147,133,141,142,187,137,2,47,78,165,164])). % 78.05/78.42 cnf(3785,plain, % 78.05/78.42 (P6(f19(a1))), % 78.05/78.42 inference(scs_inference,[],[3617,3631,3717,3221,3315,3649,3704,3158,3152,3726,3441,3460,3107,3236,129,3082,186,146,145,144,143,147,133,141,142,187,137,2,47,78,165,164,157])). % 78.05/78.42 cnf(3787,plain, % 78.05/78.42 (~E(f16(x37871),a17)), % 78.05/78.42 inference(scs_inference,[],[3617,3631,3717,3221,3315,3649,3704,3158,3152,3726,3441,3460,3107,3526,3110,3236,129,3082,186,146,145,144,143,147,133,141,142,187,137,2,47,78,165,164,157,42])). % 78.05/78.42 cnf(3800,plain, % 78.05/78.42 (P14(f8(x38001,f34(a14)),x38001,f34(a28))), % 78.05/78.42 inference(scs_inference,[],[3729,186])). % 78.05/78.42 cnf(3814,plain, % 78.05/78.42 (P4(f19(a22))), % 78.05/78.42 inference(scs_inference,[],[3697,3766,3785,3729,186,144,146,143,141,145,147,133])). % 78.05/78.42 cnf(3816,plain, % 78.05/78.42 (P8(f19(a1))), % 78.05/78.42 inference(scs_inference,[],[3697,3766,3785,3729,186,144,146,143,141,145,147,133,137])). % 78.05/78.42 cnf(3824,plain, % 78.05/78.42 (E(f11(x38241,f29(a1,a12,a24)),f11(x38241,a12))), % 78.05/78.42 inference(rename_variables,[],[3551])). % 78.05/78.42 cnf(3833,plain, % 78.05/78.42 (P6(f20(f20(a2)))), % 78.05/78.42 inference(scs_inference,[],[3652,3007,3697,3766,3779,3785,3319,3729,3403,3156,3154,3551,3824,3448,3236,186,144,146,143,141,145,147,133,137,187,2,149,59,74,148,165,80,157])). % 78.05/78.42 cnf(3835,plain, % 78.05/78.42 (~P13(f33(f29(a1,a12,a24)),f33(a28))), % 78.05/78.42 inference(scs_inference,[],[3652,3007,3697,3766,3779,3785,3319,3729,3403,3156,3154,3551,3824,3731,3448,108,3236,186,144,146,143,141,145,147,133,137,187,2,149,59,74,148,165,80,157,166])). % 78.05/78.42 cnf(3838,plain, % 78.05/78.42 (P13(x38381,f33(x38381))), % 78.05/78.42 inference(rename_variables,[],[3526])). % 78.05/78.42 cnf(3839,plain, % 78.05/78.42 (~E(f33(f33(a25)),f33(a14))), % 78.05/78.42 inference(scs_inference,[],[3652,3007,3697,3766,3779,3785,3319,3729,3403,3156,3154,3728,3551,3824,3731,3345,3448,3526,3838,108,3236,186,144,146,143,141,145,147,133,137,187,2,149,59,74,148,165,80,157,166,42,43])). % 78.05/78.42 cnf(3849,plain, % 78.05/78.42 (P15(f7(a1,f29(a1,a12,a25)),a1,f29(a1,a12,a25))), % 78.05/78.42 inference(scs_inference,[],[84,3652,3007,3697,3766,3779,3785,3319,3729,3783,3403,3156,3154,3737,3728,3569,3551,3824,3731,3345,3448,637,3526,3838,629,631,633,635,108,3236,639,641,88,90,86,95,92,98,96,94,123,186,144,146,143,141,145,147,133,137,187,2,149,59,74,148,165,80,157,166,42,43,68,3,191,199,198])). % 78.05/78.42 cnf(3863,plain, % 78.05/78.42 (P29(f7(a1,a12),a1)), % 78.05/78.42 inference(scs_inference,[],[84,3652,3007,3697,3766,3779,3785,3319,3729,3783,3403,3156,3154,3737,3728,3569,3551,3824,3731,3345,3448,637,3526,3838,629,631,633,635,108,3236,639,641,251,252,261,250,241,246,249,88,90,86,95,92,98,96,94,123,186,144,146,143,141,145,147,133,137,187,2,149,59,74,148,165,80,157,166,42,43,68,3,191,199,198,192,194,195,193,197,196,205])). % 78.05/78.42 cnf(3865,plain, % 78.05/78.42 (P9(f7(a1,a12),a1)), % 78.05/78.42 inference(scs_inference,[],[84,3652,3007,3697,3766,3779,3785,3319,3729,3783,3403,3156,3154,3737,3728,3569,3551,3824,3731,3345,3448,637,3526,3838,629,631,633,635,108,3236,639,641,251,252,261,250,241,246,249,88,90,86,95,92,98,96,94,123,186,144,146,143,141,145,147,133,137,187,2,149,59,74,148,165,80,157,166,42,43,68,3,191,199,198,192,194,195,193,197,196,205,206])). % 78.05/78.42 cnf(3867,plain, % 78.05/78.42 (P27(f7(a1,a12))), % 78.05/78.42 inference(scs_inference,[],[84,3652,3007,3697,3766,3779,3785,3319,3729,3783,3403,3156,3154,3737,3728,3569,3551,3824,3731,3345,3448,637,3526,3838,629,631,633,635,108,3236,639,641,251,252,261,250,241,246,249,88,90,86,95,92,98,96,94,123,186,144,146,143,141,145,147,133,137,187,2,149,59,74,148,165,80,157,166,42,43,68,3,191,199,198,192,194,195,193,197,196,205,206,202])). % 78.05/78.42 cnf(3869,plain, % 78.05/78.42 (P23(f7(a1,a12))), % 78.05/78.42 inference(scs_inference,[],[84,3652,3007,3697,3766,3779,3785,3319,3729,3783,3403,3156,3154,3737,3728,3569,3551,3824,3731,3345,3448,637,3526,3838,629,631,633,635,108,3236,639,641,251,252,261,250,241,246,249,88,90,86,95,92,98,96,94,123,186,144,146,143,141,145,147,133,137,187,2,149,59,74,148,165,80,157,166,42,43,68,3,191,199,198,192,194,195,193,197,196,205,206,202,201])). % 78.05/78.42 cnf(3871,plain, % 78.05/78.42 (P1(f7(a1,a12))), % 78.05/78.42 inference(scs_inference,[],[84,3652,3007,3697,3766,3779,3785,3319,3729,3783,3403,3156,3154,3737,3728,3569,3551,3824,3731,3345,3448,637,3526,3838,629,631,633,635,108,3236,639,641,251,252,261,250,241,246,249,88,90,86,95,92,98,96,94,123,186,144,146,143,141,145,147,133,137,187,2,149,59,74,148,165,80,157,166,42,43,68,3,191,199,198,192,194,195,193,197,196,205,206,202,201,200])). % 78.05/78.42 cnf(3873,plain, % 78.05/78.42 (P28(f7(a1,a12))), % 78.05/78.42 inference(scs_inference,[],[84,3652,3007,3697,3766,3779,3785,3319,3729,3783,3403,3156,3154,3737,3728,3569,3551,3824,3731,3345,3448,637,3526,3838,629,631,633,635,108,3236,639,641,251,252,261,250,241,246,249,88,90,86,95,92,98,96,94,123,186,144,146,143,141,145,147,133,137,187,2,149,59,74,148,165,80,157,166,42,43,68,3,191,199,198,192,194,195,193,197,196,205,206,202,201,200,203])). % 78.05/78.42 cnf(3878,plain, % 78.05/78.42 (~P26(f7(a1,a12))), % 78.05/78.42 inference(scs_inference,[],[84,3652,3007,3697,3766,3779,3785,3319,3729,3783,3403,3156,3154,3737,3728,3569,3551,3824,3731,3345,3448,637,3526,3838,629,631,633,635,108,3236,639,641,251,252,261,250,241,246,249,88,90,86,95,92,98,96,94,123,186,144,146,143,141,145,147,133,137,187,2,149,59,74,148,165,80,157,166,42,43,68,3,191,199,198,192,194,195,193,197,196,205,206,202,201,200,203,547,1083,204])). % 78.05/78.42 cnf(3888,plain, % 78.05/78.42 (P14(f8(x38881,x38882),x38881,x38882)), % 78.05/78.42 inference(scs_inference,[],[3814,122,144,146,143,186])). % 78.05/78.42 cnf(3890,plain, % 78.05/78.42 (P4(f19(a1))), % 78.05/78.42 inference(scs_inference,[],[3814,3816,122,144,146,143,186,133])). % 78.05/78.42 cnf(3896,plain, % 78.05/78.42 (P8(f20(f20(a2)))), % 78.05/78.42 inference(scs_inference,[],[3814,3816,3833,122,144,146,143,186,133,145,147,137])). % 78.05/78.42 cnf(3902,plain, % 78.05/78.42 (E(f7(x39021,a12),f7(x39021,f29(a1,a12,a24)))), % 78.05/78.42 inference(rename_variables,[],[3350])). % 78.05/78.42 cnf(3906,plain, % 78.05/78.42 (E(f7(x39061,a12),f7(x39061,f29(a1,a12,a24)))), % 78.05/78.42 inference(rename_variables,[],[3350])). % 78.05/78.42 cnf(3908,plain, % 78.05/78.42 (E(f7(x39081,a12),f7(x39081,f29(a1,a12,a24)))), % 78.05/78.42 inference(rename_variables,[],[3350])). % 78.05/78.42 cnf(3915,plain, % 78.05/78.42 (P6(f30(a1))), % 78.05/78.42 inference(scs_inference,[],[3203,3787,3814,3816,3867,3869,3871,3873,3244,3373,3833,3350,3902,3906,3908,122,3082,144,146,143,186,133,145,147,137,187,2,44,149,41,37,46,165,148,157])). % 78.05/78.42 cnf(3917,plain, % 78.05/78.42 (~P13(f33(a12),f33(a28))), % 78.05/78.42 inference(scs_inference,[],[3203,3787,3814,3816,3867,3869,3871,3873,3244,3835,3373,3833,3350,3902,3906,3908,3449,122,3082,144,146,143,186,133,145,147,137,187,2,44,149,41,37,46,165,148,157,42])). % 78.05/78.42 cnf(3920,plain, % 78.05/78.42 (~E(f5(f33(a14)),f35(a17,a17))), % 78.05/78.42 inference(scs_inference,[],[3203,3787,3814,3816,3867,3869,3871,3873,3244,3835,3373,3833,3348,3350,3902,3906,3908,3449,3095,3293,122,3082,116,144,146,143,186,133,145,147,137,187,2,44,149,41,37,46,165,148,157,42,43,68])). % 78.05/78.42 cnf(3921,plain, % 78.05/78.42 (~E(a28,f33(a12))), % 78.05/78.42 inference(scs_inference,[],[3203,3787,3814,3816,3867,3869,3871,3873,3244,3776,3835,3373,3833,3348,3350,3902,3906,3908,3449,3095,3293,122,3082,116,3207,144,146,143,186,133,145,147,137,187,2,44,149,41,37,46,165,148,157,42,43,68,3])). % 78.05/78.42 cnf(3932,plain, % 78.05/78.42 (P15(f11(a1,f7(a1,a12)),a1,f7(a1,a12))), % 78.05/78.42 inference(scs_inference,[],[84,3203,3787,3814,3816,3867,3869,3871,3873,3878,3244,3776,3863,3865,3835,3373,3833,3348,3350,3902,3906,3908,3449,3095,3293,122,3082,116,3207,88,90,86,95,92,98,96,94,123,144,146,143,186,133,145,147,137,187,2,44,149,41,37,46,165,148,157,42,43,68,3,191,194,198,195,197,199])). % 78.05/78.42 cnf(3940,plain, % 78.05/78.42 (P9(f11(a1,f29(a1,a12,a24)),a1)), % 78.05/78.42 inference(scs_inference,[],[84,3203,3787,3814,3816,3867,3869,3871,3873,3878,3244,3776,3863,3865,3835,3160,3373,3833,3348,3350,3902,3906,3908,3449,3095,3293,122,3082,251,252,261,250,241,246,249,116,3207,88,90,86,95,92,98,96,94,123,144,146,143,186,133,145,147,137,187,2,44,149,41,37,46,165,148,157,42,43,68,3,191,194,198,195,197,199,192,193,196,206])). % 78.05/78.42 cnf(3954,plain, % 78.05/78.42 (~E(f5(f33(a28)),f33(a12))), % 78.05/78.42 inference(scs_inference,[],[84,3203,3787,3814,3816,3867,3869,3871,3873,3878,3244,3776,3863,3865,3835,3160,3849,3373,3833,3348,3350,3902,3906,3908,3449,3095,3293,122,637,3082,629,631,633,635,639,641,251,252,261,250,241,246,249,116,3207,88,90,86,95,92,98,96,94,123,144,146,143,186,133,145,147,137,187,2,44,149,41,37,46,165,148,157,42,43,68,3,191,194,198,195,197,199,192,193,196,206,204,200,202,205,201,203,556])). % 78.05/78.42 cnf(3955,plain, % 78.05/78.42 (~E(f16(a28),f33(a12))), % 78.05/78.42 inference(scs_inference,[],[84,3203,3787,3814,3816,3867,3869,3871,3873,3878,3244,3776,3863,3865,3835,3160,3849,3373,3833,3348,3350,3902,3906,3908,3449,3095,3293,122,637,3082,629,631,633,635,639,641,251,252,261,250,241,246,249,116,3207,88,90,86,95,92,98,96,94,123,144,146,143,186,133,145,147,137,187,2,44,149,41,37,46,165,148,157,42,43,68,3,191,194,198,195,197,199,192,193,196,206,204,200,202,205,201,203,556,547])). % 78.05/78.42 cnf(3973,plain, % 78.05/78.42 (P8(f30(a1))), % 78.05/78.42 inference(scs_inference,[],[3890,3915,3774,146,144,143,147,133,145,137])). % 78.05/78.42 cnf(3977,plain, % 78.05/78.42 (~E(f33(a12),f16(a28))), % 78.05/78.42 inference(scs_inference,[],[3890,3915,3955,3774,244,146,144,143,147,133,145,137,187,2])). % 78.05/78.42 cnf(3983,plain, % 78.05/78.42 (P6(f20(f19(a1)))), % 78.05/78.42 inference(scs_inference,[],[3890,3915,3955,3325,3433,3774,244,3236,129,146,144,143,147,133,145,137,187,2,165,159,157])). % 78.05/78.42 cnf(3987,plain, % 78.05/78.42 (~P13(f33(a12),f33(a14))), % 78.05/78.42 inference(scs_inference,[],[3890,3915,3917,3955,3325,3433,3774,3355,3337,244,3526,3236,129,146,144,143,147,133,145,137,187,2,165,159,157,42,43])). % 78.05/78.42 cnf(3989,plain, % 78.05/78.42 (E(f29(f29(a1,a12,a24),x39891,f29(a1,a12,a24)),f29(a12,x39891,a12))), % 78.05/78.42 inference(scs_inference,[],[3890,3915,3917,3955,3325,3433,3770,3774,3539,3559,3355,3337,244,3526,109,3236,129,146,144,143,147,133,145,137,187,2,165,159,157,42,43,68,3])). % 78.05/78.42 cnf(3992,plain, % 78.05/78.42 (~E(f5(f33(a14)),f33(a12))), % 78.05/78.42 inference(scs_inference,[],[3890,3915,3917,3955,3325,3433,3770,3774,3539,3559,3355,3337,244,3526,109,3236,129,146,144,143,147,133,145,137,187,2,165,159,157,42,43,68,3,556])). % 78.05/78.42 cnf(3993,plain, % 78.05/78.42 (~E(f16(a14),f33(a12))), % 78.05/78.42 inference(scs_inference,[],[3890,3915,3917,3955,3325,3433,3770,3774,3539,3559,3355,3337,244,3526,109,3236,129,146,144,143,147,133,145,137,187,2,165,159,157,42,43,68,3,556,547])). % 78.05/78.42 cnf(4024,plain, % 78.05/78.42 (P4(f30(a1))), % 78.05/78.42 inference(scs_inference,[],[3973,3681,144,146,143,133])). % 78.05/78.42 cnf(4026,plain, % 78.05/78.42 (P8(f20(f19(a1)))), % 78.05/78.42 inference(scs_inference,[],[3973,3983,3681,144,146,143,133,137])). % 78.05/78.42 cnf(4032,plain, % 78.05/78.42 (P16(f6(x40321,x40322),x40321,x40322)), % 78.05/78.42 inference(scs_inference,[],[3973,3983,3681,121,144,146,143,133,137,147,145,187])). % 78.05/78.42 cnf(4034,plain, % 78.05/78.42 (~E(f33(a12),f16(a14))), % 78.05/78.42 inference(scs_inference,[],[3973,3993,3983,3681,121,144,146,143,133,137,147,145,187,2])). % 78.05/78.42 cnf(4039,plain, % 78.05/78.42 (P9(f11(a1,a12),a1)), % 78.05/78.42 inference(scs_inference,[],[3973,3987,3993,3983,3940,3681,3548,3551,121,3526,144,146,143,133,137,147,145,187,2,167,65,76])). % 78.05/78.42 cnf(4044,plain, % 78.05/78.42 (P6(f20(a27))), % 78.05/78.42 inference(scs_inference,[],[3973,3987,3993,3413,3983,3940,3681,3548,3551,121,3526,3252,129,144,146,143,133,137,147,145,187,2,167,65,76,159,157])). % 78.05/78.42 cnf(4052,plain, % 78.05/78.42 (P13(f6(x40521,x40522),f33(f35(x40521,x40522)))), % 78.05/78.42 inference(scs_inference,[],[84,3973,3977,3987,3993,3413,3932,3983,3940,3681,3548,3360,3551,3091,3449,121,3486,3526,3252,3863,3865,3878,129,3867,3869,3871,3873,116,88,90,86,95,92,98,96,94,123,144,146,143,133,137,147,145,187,2,167,65,76,159,157,43,68,3,206,188])). % 78.05/78.42 cnf(4069,plain, % 78.05/78.42 (P8(f20(a27))), % 78.05/78.42 inference(scs_inference,[],[4024,4044,3896,146,143,144,133,137])). % 78.05/78.42 cnf(4077,plain, % 78.05/78.42 (~E(f33(a12),a28)), % 78.05/78.42 inference(scs_inference,[],[4024,4044,3921,3896,242,146,143,144,133,137,147,145,187,2])). % 78.05/78.42 cnf(4081,plain, % 78.05/78.42 (P14(f8(x40811,f21(a14)),x40811,f21(a28))), % 78.05/78.42 inference(scs_inference,[],[3888,4024,4044,3921,3896,3363,3246,3598,242,146,143,144,133,137,147,145,187,2,73,40])). % 78.05/78.42 cnf(4082,plain, % 78.05/78.42 (P14(f8(x40821,x40822),x40821,x40822)), % 78.05/78.42 inference(rename_variables,[],[3888])). % 78.05/78.42 cnf(4083,plain, % 78.05/78.42 (P12(f29(a12,x40831,a12),f29(f29(a1,a12,a24),x40831,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[3888,4024,4044,3921,3989,3896,3363,3246,3598,115,242,146,143,144,133,137,147,145,187,2,73,40,72])). % 78.05/78.42 cnf(4086,plain, % 78.05/78.42 (E(f8(a14,x40861),f8(a28,x40861))), % 78.05/78.42 inference(rename_variables,[],[3362])). % 78.05/78.42 cnf(4088,plain, % 78.05/78.42 (P14(f8(a28,x40881),a14,x40881)), % 78.05/78.42 inference(scs_inference,[],[3888,4082,4024,4044,3921,3989,3896,3363,3246,3362,4086,3729,3598,115,242,146,143,144,133,137,147,145,187,2,73,40,72,69,38])). % 78.05/78.42 cnf(4090,plain, % 78.05/78.42 (P14(f8(x40901,x40902),x40901,x40902)), % 78.05/78.42 inference(rename_variables,[],[3888])). % 78.05/78.42 cnf(4093,plain, % 78.05/78.42 (P18(f8(x40931,x40932),f33(f35(x40931,x40932)))), % 78.05/78.42 inference(scs_inference,[],[3888,4082,4024,4044,3429,3921,3989,3209,3896,3363,3246,3362,4086,3729,3598,3252,115,129,242,146,143,144,133,137,147,145,187,2,73,40,72,69,38,165,159])). % 78.05/78.42 cnf(4096,plain, % 78.05/78.42 (P16(f6(f21(a14),x40961),f21(a28),x40961)), % 78.05/78.42 inference(scs_inference,[],[3888,4082,4032,4024,4044,3429,3921,3989,3209,3896,3363,3246,3362,4086,3729,3598,3252,115,129,242,146,143,144,133,137,147,145,187,2,73,40,72,69,38,165,159,70])). % 78.05/78.42 cnf(4097,plain, % 78.05/78.42 (P16(f6(x40971,x40972),x40971,x40972)), % 78.05/78.42 inference(rename_variables,[],[4032])). % 78.05/78.42 cnf(4098,plain, % 78.05/78.42 (P16(f6(x40981,f21(a14)),x40981,f21(a28))), % 78.05/78.42 inference(scs_inference,[],[3888,4082,4032,4097,4024,4044,3429,3921,3989,3209,3896,3363,3246,3362,4086,3729,3598,3252,115,129,242,146,143,144,133,137,147,145,187,2,73,40,72,69,38,165,159,70,71])). % 78.05/78.42 cnf(4100,plain, % 78.05/78.42 (P14(f8(f21(a14),x41001),f21(a28),x41001)), % 78.05/78.42 inference(scs_inference,[],[3888,4082,4090,4032,4097,4024,4044,3429,3921,3989,3209,3896,3363,3246,3362,4086,3729,3598,3252,115,129,242,146,143,144,133,137,147,145,187,2,73,40,72,69,38,165,159,70,71,39])). % 78.05/78.42 cnf(4102,plain, % 78.05/78.42 (P6(f20(f30(a1)))), % 78.05/78.42 inference(scs_inference,[],[3888,4082,4090,4032,4097,4024,4044,3429,3921,3989,3209,3896,3363,3246,3362,4086,3729,3598,3252,115,129,242,146,143,144,133,137,147,145,187,2,73,40,72,69,38,165,159,70,71,39,157])). % 78.05/78.42 cnf(4105,plain, % 78.05/78.42 (P13(x41051,f33(x41051))), % 78.05/78.42 inference(rename_variables,[],[3526])). % 78.05/78.42 cnf(4106,plain, % 78.05/78.42 (~E(f33(f33(a12)),f33(a14))), % 78.05/78.42 inference(scs_inference,[],[3888,4082,4090,4032,4097,4024,4044,3429,3921,3989,3209,3896,3363,3246,3362,4086,3987,3729,3598,3526,4105,3252,115,129,242,146,143,144,133,137,147,145,187,2,73,40,72,69,38,165,159,70,71,39,157,42,43])). % 78.05/78.42 cnf(4109,plain, % 78.05/78.42 (E(f37(f29(a1,a12,a24),f29(a1,a12,a24)),f37(a12,a12))), % 78.05/78.42 inference(scs_inference,[],[3888,4082,4090,4032,4097,4024,4044,3429,3921,3989,3209,3722,3896,3557,3563,3363,3246,3362,4086,3987,3729,3598,110,3526,4105,3252,115,129,242,146,143,144,133,137,147,145,187,2,73,40,72,69,38,165,159,70,71,39,157,42,43,68,3])). % 78.05/78.42 cnf(4114,plain, % 78.05/78.42 (~P18(f33(f35(x41141,x41142)),f8(x41141,x41142))), % 78.05/78.42 inference(scs_inference,[],[3888,4082,4090,4032,4097,4024,4044,3429,3921,3989,3209,3722,3896,3557,3563,3363,3246,3362,4086,3987,3729,3598,110,3526,4105,3252,115,129,242,146,143,144,133,137,147,145,187,2,73,40,72,69,38,165,159,70,71,39,157,42,43,68,3,186,161])). % 78.05/78.42 cnf(4122,plain, % 78.05/78.42 (P14(f6(f21(a14),x41221),f21(a28),x41221)), % 78.05/78.42 inference(scs_inference,[],[4096,186])). % 78.05/78.42 cnf(4124,plain, % 78.05/78.42 (P9(f20(a26),a26)), % 78.05/78.42 inference(scs_inference,[],[4096,3331,186,146])). % 78.05/78.42 cnf(4130,plain, % 78.05/78.42 (P4(f20(a27))), % 78.05/78.42 inference(scs_inference,[],[4069,4096,3331,186,146,143,144,133])). % 78.05/78.42 cnf(4132,plain, % 78.05/78.42 (P8(f20(f30(a1)))), % 78.05/78.42 inference(scs_inference,[],[4069,4096,4102,3331,186,146,143,144,133,137])). % 78.05/78.42 cnf(4134,plain, % 78.05/78.42 (P9(f30(a26),a26)), % 78.05/78.42 inference(scs_inference,[],[4069,4096,4102,3331,186,146,143,144,133,137,145])). % 78.05/78.42 cnf(4136,plain, % 78.05/78.42 (P9(f19(a26),a26)), % 78.05/78.42 inference(scs_inference,[],[4069,4096,4102,3331,186,146,143,144,133,137,145,147])). % 78.05/78.42 cnf(4141,plain, % 78.05/78.42 (P15(f11(a1,a12),a1,f29(a1,a12,a24))), % 78.05/78.42 inference(scs_inference,[],[4088,4069,3304,4096,4102,3160,3551,3331,186,146,143,144,133,137,145,147,187,2,78])). % 78.05/78.42 cnf(4147,plain, % 78.05/78.42 (~P18(f33(f35(x41471,a28)),f8(x41471,a14))), % 78.05/78.42 inference(scs_inference,[],[4088,4069,4039,4114,3304,4096,4102,3364,3160,3441,3551,3331,3878,3082,186,146,143,144,133,137,145,147,187,2,78,47,165,66])). % 78.05/78.42 cnf(4150,plain, % 78.05/78.42 (P6(f11(a1,a12))), % 78.05/78.42 inference(scs_inference,[],[4088,4069,4039,4114,3304,4096,4102,3364,3160,3441,3551,3331,3878,3082,186,146,143,144,133,137,145,147,187,2,78,47,165,66,157])). % 78.05/78.42 cnf(4162,plain, % 78.05/78.42 (~P15(f29(a1,a12,a24),a1,f29(a1,a12,a25))), % 78.05/78.42 inference(scs_inference,[],[84,4088,4034,4069,4039,4114,3304,4096,4102,3366,3364,3160,3441,240,3551,320,3331,3285,260,3293,3449,3878,3082,637,629,631,633,251,635,252,261,250,241,246,639,641,249,116,264,124,88,90,86,95,92,98,96,94,123,186,146,143,144,133,137,145,147,187,2,78,47,165,66,157,43,68,3,188,141,163,209])). % 78.05/78.42 cnf(4171,plain, % 78.05/78.42 (P14(f6(x41711,f21(a14)),x41711,f21(a28))), % 78.05/78.42 inference(scs_inference,[],[4130,4098,143,186])). % 78.05/78.42 cnf(4182,plain, % 78.05/78.42 (P8(f11(a1,a12))), % 78.05/78.42 inference(scs_inference,[],[4150,4130,3748,4098,4026,143,186,146,2,133,144,145,137])). % 78.05/78.42 cnf(4186,plain, % 78.05/78.42 (P16(f8(x41861,f21(a14)),x41861,f21(a28))), % 78.05/78.42 inference(scs_inference,[],[4150,4130,3748,4081,4098,4026,143,186,146,2,133,144,145,137,147,187])). % 78.05/78.42 cnf(4191,plain, % 78.05/78.42 (E(f11(x41911,a12),f11(x41911,f29(a1,a12,a24)))), % 78.05/78.42 inference(rename_variables,[],[3460])). % 78.05/78.42 cnf(4195,plain, % 78.05/78.42 (~P13(f33(f35(x41951,x41952)),f33(a14))), % 78.05/78.42 inference(scs_inference,[],[4150,4130,4124,3748,4081,4098,3280,4026,4093,3460,4191,109,3331,143,186,146,2,133,144,145,137,147,187,165,64,68,63,166])). % 78.05/78.42 cnf(4201,plain, % 78.05/78.42 (E(f29(a12,x42011,a12),f29(f29(a1,a12,a24),x42011,f29(a1,a12,a24)))), % 78.05/78.42 inference(scs_inference,[],[4150,4130,4124,3748,4081,4098,3743,3280,4026,4093,3435,3456,3460,4191,3350,3448,109,3331,3863,143,186,146,2,133,144,145,137,147,187,165,64,68,63,166,59,74,3])). % 78.05/78.42 cnf(4205,plain, % 78.05/78.42 (E(f29(x42051,f29(a1,a12,a24),x42052),f29(x42051,a12,x42052))), % 78.05/78.42 inference(rename_variables,[],[3545])). % 78.05/78.42 cnf(4207,plain, % 78.05/78.42 (E(f29(x42071,f29(a1,a12,a24),x42072),f29(x42071,a12,x42072))), % 78.05/78.42 inference(rename_variables,[],[3545])). % 78.05/78.42 cnf(4208,plain, % 78.05/78.42 (P6(f20(f20(a27)))), % 78.05/78.42 inference(scs_inference,[],[4162,4150,4130,4124,3748,4081,4098,3743,3280,4026,4093,3435,3456,3545,4205,3460,4191,3350,3448,109,3331,3863,143,186,146,2,133,144,145,137,147,187,165,64,68,63,166,59,74,3,80,78,157])). % 78.05/78.42 cnf(4211,plain, % 78.05/78.42 (~P13(f33(a12),f33(f16(x42111)))), % 78.05/78.42 inference(scs_inference,[],[4162,4150,4130,4124,3748,4081,4098,3743,3280,4026,4093,3435,3456,3917,3545,4205,3460,4191,3350,3231,3448,3490,3112,109,3331,3863,143,186,146,2,133,144,145,137,147,187,165,64,68,63,166,59,74,3,80,78,157,66,43])). % 78.05/78.42 cnf(4219,plain, % 78.05/78.42 (~P15(a12,a1,f29(a1,a12,a25))), % 78.05/78.42 inference(scs_inference,[],[84,272,4162,4150,4130,4124,3748,4081,4098,3743,3280,4026,4093,3435,3456,3917,3545,4205,4207,3460,4191,3350,3231,3448,3490,3112,109,3526,3331,3863,637,629,631,633,251,635,639,641,130,264,297,111,87,89,91,85,124,112,113,88,90,86,92,95,98,96,94,123,143,186,146,2,133,144,145,137,147,187,165,64,68,63,166,59,74,3,80,78,157,66,43,547,159,42,47,209])). % 78.05/78.42 cnf(4224,plain, % 78.05/78.42 (~P26(f19(a13))), % 78.05/78.42 inference(scs_inference,[],[101,143])). % 78.05/78.42 cnf(4226,plain, % 78.05/78.42 (P9(f20(a13),a13)), % 78.05/78.42 inference(scs_inference,[],[101,143,146])). % 78.05/78.42 cnf(4230,plain, % 78.05/78.42 (P4(f11(a1,a12))), % 78.05/78.42 inference(scs_inference,[],[4182,101,143,146,144,133])). % 78.05/78.42 cnf(4234,plain, % 78.05/78.42 (P9(f30(a13),a13)), % 78.05/78.42 inference(scs_inference,[],[4182,3954,4211,101,143,146,144,133,2,547,145])). % 78.05/78.42 cnf(4236,plain, % 78.05/78.42 (P8(f20(f20(a27)))), % 78.05/78.42 inference(scs_inference,[],[4182,3954,4208,4211,101,143,146,144,133,2,547,145,137])). % 78.05/78.42 cnf(4238,plain, % 78.05/78.42 (P9(f19(a13),a13)), % 78.05/78.42 inference(scs_inference,[],[4182,3954,4208,4211,101,143,146,144,133,2,547,145,137,147])). % 78.05/78.42 cnf(4240,plain, % 78.05/78.42 (P16(f8(f21(a14),x42401),f21(a28),x42401)), % 78.05/78.42 inference(scs_inference,[],[4182,3954,4100,4208,4211,101,143,146,144,133,2,547,145,137,147,187])). % 78.05/78.42 cnf(4250,plain, % 78.05/78.42 (E(f11(x42501,f29(a1,a12,a24)),f11(x42501,a12))), % 78.05/78.42 inference(rename_variables,[],[3551])). % 78.05/78.42 cnf(4252,plain, % 78.05/78.42 (E(f11(x42521,f29(a1,a12,a24)),f11(x42521,a12))), % 78.05/78.42 inference(rename_variables,[],[3551])). % 78.05/78.42 cnf(4254,plain, % 78.05/78.42 (~P11(f21(f11(a1,a12)))), % 78.05/78.42 inference(scs_inference,[],[4182,3431,3954,4100,4052,3148,3146,4208,4211,3777,3460,3551,4250,3093,3486,101,3252,129,143,146,144,133,2,547,145,137,147,187,165,58,159,41,44,68,149])). % 78.05/78.42 cnf(4259,plain, % 78.05/78.42 (E(f11(x42591,f29(a1,a12,a24)),f11(x42591,a12))), % 78.05/78.42 inference(rename_variables,[],[3551])). % 78.05/78.42 cnf(4263,plain, % 78.05/78.42 (~P11(f32(f11(a1,a12)))), % 78.05/78.42 inference(scs_inference,[],[4182,3431,4077,3954,4100,4052,3150,3148,3146,3144,4208,4211,3777,3377,3460,3551,4250,4252,4259,3093,3486,3449,101,3526,3252,129,143,146,144,133,2,547,145,137,147,187,165,58,159,41,44,68,149,42,37,46,3,148])). % 78.05/78.42 cnf(4267,plain, % 78.05/78.42 (P6(f19(a27))), % 78.05/78.42 inference(scs_inference,[],[4219,4182,3431,4077,3954,4100,4052,3150,3148,3146,3144,4208,4211,3777,3377,3545,3460,3551,4250,4252,4259,3093,3486,3449,101,3526,3252,129,143,146,144,133,2,547,145,137,147,187,165,58,159,41,44,68,149,42,37,46,3,148,80,157])). % 78.05/78.42 cnf(4275,plain, % 78.05/78.42 (~P18(f33(f35(x42751,x42752)),f6(x42751,x42752))), % 78.05/78.42 inference(scs_inference,[],[4219,4182,3431,4077,3954,4147,4100,4052,3150,3148,3146,3144,4208,4211,3777,3377,3362,3545,3460,3551,4250,4252,4259,3112,3093,3486,3449,101,3526,3252,129,116,143,146,144,133,2,547,145,137,147,187,165,58,159,41,44,68,149,42,37,46,3,148,80,157,78,66,43,161])). % 78.05/78.42 cnf(4294,plain, % 78.05/78.42 (P8(f19(a27))), % 78.05/78.42 inference(scs_inference,[],[4230,4267,3992,4132,143,146,144,133,2,145,137])). % 78.05/78.42 cnf(4304,plain, % 78.05/78.42 (P15(f11(a1,a12),a1,a12)), % 78.05/78.42 inference(scs_inference,[],[4230,4141,4267,4134,3992,4254,4132,4201,3334,110,3331,120,143,146,144,133,2,145,137,147,165,68,3,80])). % 78.05/78.42 cnf(4305,plain, % 78.05/78.42 (P6(f20(f11(a1,a12)))), % 78.05/78.42 inference(scs_inference,[],[4230,4141,4267,4134,3992,4254,4132,4201,3334,110,3331,120,143,146,144,133,2,145,137,147,165,68,3,80,157])). % 78.05/78.42 cnf(4350,plain, % 78.05/78.42 (P9(f20(a1),a1)), % 78.05/78.42 inference(scs_inference,[],[3082,146])). % 78.05/78.42 cnf(4354,plain, % 78.05/78.42 (P4(f19(a27))), % 78.05/78.42 inference(scs_inference,[],[4294,3082,146,144,133])). % 78.05/78.42 cnf(4357,plain, % 78.05/78.42 (P9(f30(f19(a27)),f19(a27))), % 78.05/78.42 inference(scs_inference,[],[4294,3493,3082,146,144,133,2,145])). % 78.05/78.42 cnf(4359,plain, % 78.05/78.42 (P8(f20(f11(a1,a12)))), % 78.05/78.42 inference(scs_inference,[],[4294,3493,4305,3082,146,144,133,2,145,137])). % 78.05/78.42 cnf(4369,plain, % 78.05/78.42 (P13(x43691,f33(x43691))), % 78.05/78.42 inference(rename_variables,[],[3526])). % 78.05/78.42 cnf(4378,plain, % 78.05/78.42 (~E(a28,f21(a13))), % 78.05/78.42 inference(scs_inference,[],[3421,4294,3520,3493,3017,4305,4195,3382,3327,3350,3289,3293,3358,3526,4369,3865,129,3082,146,144,133,2,145,137,147,165,159,167,76,149,68,42,3])). % 78.05/78.42 cnf(4381,plain, % 78.05/78.42 (P6(f19(a2))), % 78.05/78.42 inference(scs_inference,[],[3421,4294,3520,3493,3017,4305,4195,3382,3327,3350,3289,3293,3358,3526,4369,3865,129,3082,146,144,133,2,145,137,147,165,159,167,76,149,68,42,3,148,157])). % 78.05/78.42 cnf(4383,plain, % 78.05/78.42 (~P18(f33(f35(a28,x43831)),f6(a14,x43831))), % 78.05/78.42 inference(scs_inference,[],[3421,4294,3520,4275,3493,3017,4305,4195,3382,3327,3371,3350,3289,3293,3358,3526,4369,3865,129,3082,146,144,133,2,145,137,147,165,159,167,76,149,68,42,3,148,157,66])). % 78.05/78.42 cnf(4404,plain, % 78.05/78.42 (~E(f21(a13),a28)), % 78.05/78.42 inference(scs_inference,[],[4354,4378,4359,146,144,133,2])). % 78.05/78.42 cnf(4405,plain, % 78.05/78.42 (P8(f19(a2))), % 78.05/78.42 inference(scs_inference,[],[4354,4381,4378,4359,146,144,133,2,137])). % 78.05/78.42 cnf(4412,plain, % 78.05/78.42 (P16(f8(f21(a14),f5(a14)),f21(a28),f5(a28))), % 78.05/78.42 inference(scs_inference,[],[4136,4354,4381,4378,4359,4263,4240,4186,3383,108,3331,146,144,133,2,137,165,70,68,71])). % 78.05/78.42 cnf(4418,plain, % 78.05/78.42 (P14(f6(f21(a14),f5(a14)),f21(a28),f5(a28))), % 78.05/78.42 inference(scs_inference,[],[4136,4354,4381,4378,4359,4263,4083,3800,4122,4240,4186,3383,3539,108,3331,146,144,133,2,137,165,70,68,71,39,73,40])). % 78.05/78.42 cnf(4425,plain, % 78.05/78.42 (P14(f6(f29(a1,a12,a24),f21(a14)),a12,f21(a28))), % 78.05/78.42 inference(scs_inference,[],[4136,4354,4381,4378,4359,4263,4083,3800,4122,4171,4240,4186,4109,3443,3458,3468,3383,3539,108,115,3331,146,144,133,2,137,165,70,68,71,39,73,40,72,3,38])). % 78.05/78.42 cnf(4428,plain, % 78.05/78.42 (P6(f30(f19(a27)))), % 78.05/78.42 inference(scs_inference,[],[4136,4354,4381,4378,4357,4359,4263,4083,3800,4122,4171,4240,4186,4109,3443,3458,3468,3383,3539,108,115,3331,146,144,133,2,137,165,70,68,71,39,73,40,72,3,38,157])). % 78.05/78.42 cnf(4448,plain, % 78.05/78.42 (P4(f19(a2))), % 78.05/78.42 inference(scs_inference,[],[4405,4412,186,133])). % 78.05/78.42 cnf(4451,plain, % 78.05/78.42 (P9(f30(f19(a2)),f19(a2))), % 78.05/78.42 inference(scs_inference,[],[4405,3839,4412,186,133,2,145])). % 78.05/78.42 cnf(4453,plain, % 78.05/78.42 (P8(f30(f19(a27)))), % 78.05/78.42 inference(scs_inference,[],[4405,3839,4412,4428,186,133,2,145,137])). % 78.05/78.42 cnf(4461,plain, % 78.05/78.42 (P18(f21(a13),f33(f32(a13)))), % 78.05/78.42 inference(scs_inference,[],[3530,4405,3839,4412,4418,3099,4428,3358,129,186,133,2,145,137,147,187,165,159])). % 78.05/78.42 cnf(4467,plain, % 78.05/78.42 (P13(f31(a28,x44671,x44672,x44673,x44674),f33(f31(a14,x44671,x44672,x44673,x44674)))), % 78.05/78.42 inference(scs_inference,[],[3530,3528,4405,3839,4412,4418,3099,4428,3376,3289,3486,3526,3358,129,186,133,2,145,137,147,187,165,159,149,68,42])). % 78.05/78.42 cnf(4472,plain, % 78.05/78.42 (P6(f30(a2))), % 78.05/78.42 inference(scs_inference,[],[3530,3528,4405,4404,3839,4412,4418,3099,4428,3376,3512,3289,3486,3526,3358,129,186,133,2,145,137,147,187,165,159,149,68,42,148,3,157])). % 78.05/78.42 cnf(4477,plain, % 78.05/78.42 (P13(f5(f31(a14,x44771,x44772,a14,a14)),f31(a28,x44771,x44772,a28,a28))), % 78.05/78.42 inference(scs_inference,[],[3530,3528,4405,4404,3839,3644,4383,4412,4418,3099,4428,3376,3361,3512,3289,3486,3526,3358,129,186,133,2,145,137,147,187,165,159,149,68,42,148,3,157,66,43])). % 78.05/78.42 cnf(4480,plain, % 78.05/78.42 (~P18(f33(f32(a13)),f21(a13))), % 78.05/78.42 inference(scs_inference,[],[3530,3528,4405,4404,3839,3644,4383,4412,4418,3099,4428,3376,3361,3512,3289,3486,3526,3358,129,186,133,2,145,137,147,187,165,159,149,68,42,148,3,157,66,43,161])). % 78.05/78.42 cnf(4497,plain, % 78.05/78.42 (P8(f30(a2))), % 78.05/78.42 inference(scs_inference,[],[4472,4106,4236,133,2,137])). % 78.05/78.42 cnf(4505,plain, % 78.05/78.42 (~P13(f33(f32(a13)),f33(a28))), % 78.05/78.42 inference(scs_inference,[],[4234,4472,4106,4480,4425,4236,4461,3093,108,101,133,2,137,187,165,159,166])). % 78.05/78.42 cnf(4515,plain, % 78.05/78.42 (P6(f30(f19(a2)))), % 78.05/78.42 inference(scs_inference,[],[4234,4448,4472,4106,4451,4480,4425,3340,4236,4461,3451,3464,3448,3093,110,108,101,3526,252,133,2,137,187,165,159,166,68,42,59,3,157])). % 78.05/78.42 cnf(4519,plain, % 78.05/78.42 (~P13(f33(f32(a13)),f33(a14))), % 78.05/78.43 inference(scs_inference,[],[4234,4448,4472,4106,4451,4480,4425,3340,4236,4461,3451,3464,3337,3448,280,3093,110,108,101,3526,252,133,2,137,187,165,159,166,68,42,59,3,157,66,43])). % 78.05/78.43 cnf(4522,plain, % 78.05/78.43 (P15(f7(a1,a12),a1,a12)), % 78.05/78.43 inference(scs_inference,[],[85,4234,4448,4472,4106,4451,4480,4425,3340,4236,4461,3541,3451,3464,3337,3448,280,3093,110,108,101,3526,252,87,89,91,124,112,113,88,90,86,84,92,95,98,96,94,123,133,2,137,187,165,159,166,68,42,59,3,157,66,43,547,69,198])). % 78.05/78.43 cnf(4529,plain, % 78.05/78.43 (P4(f30(a2))), % 78.05/78.43 inference(scs_inference,[],[4497,133])). % 78.05/78.43 cnf(4533,plain, % 78.05/78.43 (P9(f30(f30(a2)),f30(a2))), % 78.05/78.43 inference(scs_inference,[],[4497,3920,4519,133,547,2,145])). % 78.05/78.43 cnf(4545,plain, % 78.05/78.43 (E(f29(x45451,a12,x45452),f29(x45451,f29(a1,a12,a24),x45452))), % 78.05/78.43 inference(rename_variables,[],[3448])). % 78.05/78.43 cnf(4547,plain, % 78.05/78.43 (E(f29(x45471,a12,x45472),f29(x45471,f29(a1,a12,a24),x45472))), % 78.05/78.43 inference(rename_variables,[],[3448])). % 78.05/78.43 cnf(4550,plain, % 78.05/78.43 (E(f29(x45501,a12,x45502),f29(x45501,f29(a1,a12,a24),x45502))), % 78.05/78.43 inference(rename_variables,[],[3448])). % 78.05/78.43 cnf(4551,plain, % 78.05/78.43 (P13(f31(a28,x45511,a28,x45512,x45513),f33(f31(a14,x45511,a14,x45512,x45513)))), % 78.05/78.43 inference(scs_inference,[],[4238,4497,3920,4519,3291,4467,4515,3378,3448,4545,4547,3005,3293,101,129,241,246,249,133,547,2,145,137,147,165,159,44,41,68,37,42])). % 78.05/78.43 cnf(4552,plain, % 78.05/78.43 (E(f31(x45521,x45522,a14,x45523,x45524),f31(x45521,x45522,a28,x45523,x45524))), % 78.05/78.43 inference(rename_variables,[],[3378])). % 78.05/78.43 cnf(4556,plain, % 78.05/78.43 (~E(a28,f35(a17,a17))), % 78.05/78.43 inference(scs_inference,[],[4238,4497,3920,4519,3291,4467,4515,3378,3327,3448,4545,4547,4550,3005,3293,101,129,250,241,246,249,133,547,2,145,137,147,165,159,44,41,68,37,42,46,3])). % 78.05/78.43 cnf(4559,plain, % 78.05/78.43 (P6(f19(a13))), % 78.05/78.43 inference(scs_inference,[],[4238,4304,4497,3920,4519,3291,4467,4515,3378,3327,3460,3448,4545,4547,4550,3005,3293,101,129,250,241,246,249,133,547,2,145,137,147,165,159,44,41,68,37,42,46,3,78,157])). % 78.05/78.43 cnf(4567,plain, % 78.05/78.43 (~P18(f33(f32(a1)),f21(a1))), % 78.05/78.43 inference(scs_inference,[],[4238,4304,4497,3920,4477,4519,3291,4467,4515,3378,4552,4275,3327,3361,3460,3448,4545,4547,4550,3005,3293,101,129,250,241,246,249,133,547,2,145,137,147,165,159,44,41,68,37,42,46,3,78,157,66,43,161])). % 78.05/78.43 cnf(4582,plain, % 78.05/78.43 (~E(f35(a17,a17),a28)), % 78.05/78.43 inference(scs_inference,[],[4556,4453,133,2])). % 78.05/78.43 cnf(4583,plain, % 78.05/78.43 (P8(f19(a13))), % 78.05/78.43 inference(scs_inference,[],[4556,4559,4453,133,2,137])). % 78.05/78.43 cnf(4595,plain, % 78.05/78.43 (P6(f30(f30(a2)))), % 78.05/78.43 inference(scs_inference,[],[4226,4529,4556,4559,4533,4567,3387,4453,3571,3380,4519,3285,109,3526,101,133,2,137,165,159,68,42,3,157])). % 78.05/78.43 cnf(4625,plain, % 78.05/78.43 (P13(x46251,f33(x46251))), % 78.05/78.43 inference(rename_variables,[],[3526])). % 78.05/78.43 cnf(4644,plain, % 78.05/78.43 ($false), % 78.05/78.43 inference(scs_inference,[],[85,4350,4522,4224,4582,4583,3397,4551,4595,4505,3338,4114,3071,4162,3362,3350,3448,128,3486,3526,4625,129,3082,114,261,117,118,87,89,91,124,112,113,88,90,127,97,93,86,84,92,95,98,96,94,123,133,145,2,137,147,165,159,167,76,149,68,42,148,3,78,157,66,210]), % 78.05/78.43 ['proof']). % 78.05/78.43 % SZS output end Proof % 78.05/78.43 % Total time :77.360000s %------------------------------------------------------------------------------