%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT313+1 : TPTP v8.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 10:18:48 EDT 2024 % Result : Theorem 72.34s 72.46s % Output : CNFRefutation 72.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : LAT313+1 : TPTP v8.2.0. Released v3.4.0. % 0.12/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Jun 21 20:04:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.56/0.60 start to proof:theBenchmark % 72.34/72.43 %------------------------------------------- % 72.34/72.43 % File :CSE---1.7 % 72.34/72.43 % Problem :theBenchmark % 72.34/72.43 % Transform :cnf % 72.34/72.43 % Format :tptp:raw % 72.34/72.43 % Command :java -jar mcs_scs.jar %d %s % 72.34/72.43 % 72.34/72.43 % Result :Theorem 71.740000s % 72.34/72.43 % Output :CNFRefutation 71.740000s % 72.34/72.43 %------------------------------------------- % 72.34/72.44 %------------------------------------------------------------------------------ % 72.34/72.44 % File : LAT313+1 : TPTP v8.2.0. Released v3.4.0. % 72.34/72.44 % Domain : Lattice Theory % 72.34/72.44 % Problem : Ideals T43 % 72.34/72.44 % Version : [Urb08] axioms : Especial. % 72.34/72.44 % English : % 72.34/72.44 % 72.34/72.44 % Refs : [Ban96] Bancerek (1996), Ideals % 72.34/72.44 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 72.34/72.44 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 72.34/72.44 % Source : [Urb08] % 72.34/72.44 % Names : t43_filter_2 [Urb08] % 72.34/72.44 % 72.34/72.44 % Status : Theorem % 72.34/72.45 % Rating : 0.22 v8.2.0, 0.19 v8.1.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.13 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.25 v6.2.0, 0.32 v6.1.0, 0.43 v6.0.0, 0.30 v5.5.0, 0.37 v5.4.0, 0.43 v5.3.0, 0.52 v5.2.0, 0.35 v5.1.0, 0.38 v5.0.0, 0.42 v4.1.0, 0.48 v4.0.1, 0.43 v4.0.0, 0.46 v3.7.0, 0.30 v3.5.0, 0.32 v3.4.0 % 72.34/72.45 % Syntax : Number of formulae : 50 ( 15 unt; 0 def) % 72.34/72.45 % Number of atoms : 157 ( 6 equ) % 72.34/72.45 % Maximal formula atoms : 10 ( 3 avg) % 72.34/72.45 % Number of connectives : 144 ( 37 ~; 1 |; 65 &) % 72.34/72.45 % ( 2 <=>; 39 =>; 0 <=; 0 <~>) % 72.34/72.45 % Maximal formula depth : 10 ( 4 avg) % 72.34/72.45 % Maximal term depth : 3 ( 1 avg) % 72.34/72.45 % Number of predicates : 23 ( 21 usr; 1 prp; 0-3 aty) % 72.34/72.45 % Number of functors : 6 ( 6 usr; 1 con; 0-2 aty) % 72.34/72.45 % Number of variables : 74 ( 60 !; 14 ?) % 72.34/72.45 % SPC : FOF_THM_RFO_SEQ % 72.34/72.45 % 72.34/72.45 % Comments : Normal version: includes the axioms (which may be theorems from % 72.34/72.45 % other articles) and background that are possibly necessary. % 72.34/72.45 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 72.34/72.45 % : The problem encoding is based on set theory. % 72.34/72.45 %------------------------------------------------------------------------------ % 72.34/72.45 fof(t43_filter_2,conjecture, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & v10_lattices(A) % 72.34/72.45 & l3_lattices(A) ) % 72.34/72.45 => ! [B] : % 72.34/72.45 ( m2_filter_2(B,A) % 72.34/72.45 => ( ( v14_lattices(A) % 72.34/72.45 & r2_hidden(k6_lattices(A),B) ) % 72.34/72.45 => ( r1_filter_2(u1_struct_0(A),B,k17_filter_2(A)) % 72.34/72.45 & B = u1_struct_0(A) ) ) ) ) ). % 72.34/72.45 % 72.34/72.45 fof(antisymmetry_r2_hidden,axiom, % 72.34/72.45 ! [A,B] : % 72.34/72.45 ( r2_hidden(A,B) % 72.34/72.45 => ~ r2_hidden(B,A) ) ). % 72.34/72.45 % 72.34/72.45 fof(cc1_funct_1,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( v1_xboole_0(A) % 72.34/72.45 => v1_funct_1(A) ) ). % 72.34/72.45 % 72.34/72.45 fof(cc1_lattices,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( l3_lattices(A) % 72.34/72.45 => ( ( ~ v3_struct_0(A) % 72.34/72.45 & v10_lattices(A) ) % 72.34/72.45 => ( ~ v3_struct_0(A) % 72.34/72.45 & v4_lattices(A) % 72.34/72.45 & v5_lattices(A) % 72.34/72.45 & v6_lattices(A) % 72.34/72.45 & v7_lattices(A) % 72.34/72.45 & v8_lattices(A) % 72.34/72.45 & v9_lattices(A) ) ) ) ). % 72.34/72.45 % 72.34/72.45 fof(cc2_lattices,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( l3_lattices(A) % 72.34/72.45 => ( ( ~ v3_struct_0(A) % 72.34/72.45 & v4_lattices(A) % 72.34/72.45 & v5_lattices(A) % 72.34/72.45 & v6_lattices(A) % 72.34/72.45 & v7_lattices(A) % 72.34/72.45 & v8_lattices(A) % 72.34/72.45 & v9_lattices(A) ) % 72.34/72.45 => ( ~ v3_struct_0(A) % 72.34/72.45 & v10_lattices(A) ) ) ) ). % 72.34/72.45 % 72.34/72.45 fof(d8_filter_2,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & v10_lattices(A) % 72.34/72.45 & l3_lattices(A) ) % 72.34/72.45 => k17_filter_2(A) = u1_struct_0(A) ) ). % 72.34/72.45 % 72.34/72.45 fof(dt_k17_filter_2,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & v10_lattices(A) % 72.34/72.45 & l3_lattices(A) ) % 72.34/72.45 => m2_filter_2(k17_filter_2(A),A) ) ). % 72.34/72.45 % 72.34/72.45 fof(dt_k19_filter_2,axiom, % 72.34/72.45 ! [A,B] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & v10_lattices(A) % 72.34/72.45 & l3_lattices(A) % 72.34/72.45 & ~ v1_xboole_0(B) % 72.34/72.45 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 72.34/72.45 => m2_filter_2(k19_filter_2(A,B),A) ) ). % 72.34/72.45 % 72.34/72.45 fof(dt_k1_xboole_0,axiom, % 72.34/72.45 $true ). % 72.34/72.45 % 72.34/72.45 fof(dt_k1_zfmisc_1,axiom, % 72.34/72.45 $true ). % 72.34/72.45 % 72.34/72.45 fof(dt_k6_lattices,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & l2_lattices(A) ) % 72.34/72.45 => m1_subset_1(k6_lattices(A),u1_struct_0(A)) ) ). % 72.34/72.45 % 72.34/72.45 fof(dt_l1_lattices,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( l1_lattices(A) % 72.34/72.45 => l1_struct_0(A) ) ). % 72.34/72.45 % 72.34/72.45 fof(dt_l1_struct_0,axiom, % 72.34/72.45 $true ). % 72.34/72.45 % 72.34/72.45 fof(dt_l2_lattices,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( l2_lattices(A) % 72.34/72.45 => l1_struct_0(A) ) ). % 72.34/72.45 % 72.34/72.45 fof(dt_l3_lattices,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( l3_lattices(A) % 72.34/72.45 => ( l1_lattices(A) % 72.34/72.45 & l2_lattices(A) ) ) ). % 72.34/72.45 % 72.34/72.45 fof(dt_m1_subset_1,axiom, % 72.34/72.45 $true ). % 72.34/72.45 % 72.34/72.45 fof(dt_m2_filter_2,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & v10_lattices(A) % 72.34/72.45 & l3_lattices(A) ) % 72.34/72.45 => ! [B] : % 72.34/72.45 ( m2_filter_2(B,A) % 72.34/72.45 => ( ~ v1_xboole_0(B) % 72.34/72.45 & m2_lattice4(B,A) ) ) ) ). % 72.34/72.45 % 72.34/72.45 fof(dt_m2_lattice4,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & v10_lattices(A) % 72.34/72.45 & l3_lattices(A) ) % 72.34/72.45 => ! [B] : % 72.34/72.45 ( m2_lattice4(B,A) % 72.34/72.45 => m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ) ). % 72.34/72.45 % 72.34/72.45 fof(dt_u1_struct_0,axiom, % 72.34/72.45 $true ). % 72.34/72.45 % 72.34/72.45 fof(existence_l1_lattices,axiom, % 72.34/72.45 ? [A] : l1_lattices(A) ). % 72.34/72.45 % 72.34/72.45 fof(existence_l1_struct_0,axiom, % 72.34/72.45 ? [A] : l1_struct_0(A) ). % 72.34/72.45 % 72.34/72.45 fof(existence_l2_lattices,axiom, % 72.34/72.45 ? [A] : l2_lattices(A) ). % 72.34/72.45 % 72.34/72.45 fof(existence_l3_lattices,axiom, % 72.34/72.45 ? [A] : l3_lattices(A) ). % 72.34/72.45 % 72.34/72.45 fof(existence_m1_subset_1,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ? [B] : m1_subset_1(B,A) ). % 72.34/72.45 % 72.34/72.45 fof(existence_m2_filter_2,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & v10_lattices(A) % 72.34/72.45 & l3_lattices(A) ) % 72.34/72.45 => ? [B] : m2_filter_2(B,A) ) ). % 72.34/72.45 % 72.34/72.45 fof(existence_m2_lattice4,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & v10_lattices(A) % 72.34/72.45 & l3_lattices(A) ) % 72.34/72.45 => ? [B] : m2_lattice4(B,A) ) ). % 72.34/72.45 % 72.34/72.45 fof(fc1_struct_0,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & l1_struct_0(A) ) % 72.34/72.45 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 72.34/72.45 % 72.34/72.45 fof(fc1_subset_1,axiom, % 72.34/72.45 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 72.34/72.45 % 72.34/72.45 fof(fc1_xboole_0,axiom, % 72.34/72.45 v1_xboole_0(k1_xboole_0) ). % 72.34/72.45 % 72.34/72.45 fof(rc1_lattice4,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & v10_lattices(A) % 72.34/72.45 & l3_lattices(A) ) % 72.34/72.45 => ? [B] : % 72.34/72.45 ( m2_lattice4(B,A) % 72.34/72.45 & ~ v1_xboole_0(B) ) ) ). % 72.34/72.45 % 72.34/72.45 fof(rc1_subset_1,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ~ v1_xboole_0(A) % 72.34/72.45 => ? [B] : % 72.34/72.45 ( m1_subset_1(B,k1_zfmisc_1(A)) % 72.34/72.45 & ~ v1_xboole_0(B) ) ) ). % 72.34/72.45 % 72.34/72.45 fof(rc1_xboole_0,axiom, % 72.34/72.45 ? [A] : v1_xboole_0(A) ). % 72.34/72.45 % 72.34/72.45 fof(rc2_subset_1,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ? [B] : % 72.34/72.45 ( m1_subset_1(B,k1_zfmisc_1(A)) % 72.34/72.45 & v1_xboole_0(B) ) ). % 72.34/72.45 % 72.34/72.45 fof(rc2_xboole_0,axiom, % 72.34/72.45 ? [A] : ~ v1_xboole_0(A) ). % 72.34/72.45 % 72.34/72.45 fof(rc3_struct_0,axiom, % 72.34/72.45 ? [A] : % 72.34/72.45 ( l1_struct_0(A) % 72.34/72.45 & ~ v3_struct_0(A) ) ). % 72.34/72.45 % 72.34/72.45 fof(rc5_struct_0,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & l1_struct_0(A) ) % 72.34/72.45 => ? [B] : % 72.34/72.45 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 72.34/72.45 & ~ v1_xboole_0(B) ) ) ). % 72.34/72.45 % 72.34/72.45 fof(redefinition_r1_filter_2,axiom, % 72.34/72.45 ! [A,B,C] : % 72.34/72.45 ( ( ~ v1_xboole_0(A) % 72.34/72.45 & m1_subset_1(B,k1_zfmisc_1(A)) % 72.34/72.45 & m1_subset_1(C,k1_zfmisc_1(A)) ) % 72.34/72.45 => ( r1_filter_2(A,B,C) % 72.34/72.45 <=> B = C ) ) ). % 72.34/72.45 % 72.34/72.45 fof(reflexivity_r1_filter_2,axiom, % 72.34/72.45 ! [A,B,C] : % 72.34/72.45 ( ( ~ v1_xboole_0(A) % 72.34/72.45 & m1_subset_1(B,k1_zfmisc_1(A)) % 72.34/72.45 & m1_subset_1(C,k1_zfmisc_1(A)) ) % 72.34/72.45 => r1_filter_2(A,B,B) ) ). % 72.34/72.45 % 72.34/72.45 fof(reflexivity_r1_tarski,axiom, % 72.34/72.45 ! [A,B] : r1_tarski(A,A) ). % 72.34/72.45 % 72.34/72.45 fof(symmetry_r1_filter_2,axiom, % 72.34/72.45 ! [A,B,C] : % 72.34/72.45 ( ( ~ v1_xboole_0(A) % 72.34/72.45 & m1_subset_1(B,k1_zfmisc_1(A)) % 72.34/72.45 & m1_subset_1(C,k1_zfmisc_1(A)) ) % 72.34/72.45 => ( r1_filter_2(A,B,C) % 72.34/72.45 => r1_filter_2(A,C,B) ) ) ). % 72.34/72.45 % 72.34/72.45 fof(t1_subset,axiom, % 72.34/72.45 ! [A,B] : % 72.34/72.45 ( r2_hidden(A,B) % 72.34/72.45 => m1_subset_1(A,B) ) ). % 72.34/72.45 % 72.34/72.45 fof(t2_subset,axiom, % 72.34/72.45 ! [A,B] : % 72.34/72.45 ( m1_subset_1(A,B) % 72.34/72.45 => ( v1_xboole_0(B) % 72.34/72.45 | r2_hidden(A,B) ) ) ). % 72.34/72.45 % 72.34/72.45 fof(t38_filter_2,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & v10_lattices(A) % 72.34/72.45 & l3_lattices(A) ) % 72.34/72.45 => ! [B] : % 72.34/72.45 ( m2_filter_2(B,A) % 72.34/72.45 => r1_filter_2(u1_struct_0(A),k19_filter_2(A,B),B) ) ) ). % 72.34/72.45 % 72.34/72.45 fof(t3_subset,axiom, % 72.34/72.45 ! [A,B] : % 72.34/72.45 ( m1_subset_1(A,k1_zfmisc_1(B)) % 72.34/72.45 <=> r1_tarski(A,B) ) ). % 72.34/72.45 % 72.34/72.45 fof(t42_filter_2,axiom, % 72.34/72.45 ! [A] : % 72.34/72.45 ( ( ~ v3_struct_0(A) % 72.34/72.45 & v10_lattices(A) % 72.34/72.45 & l3_lattices(A) ) % 72.34/72.45 => ! [B] : % 72.34/72.45 ( ( ~ v1_xboole_0(B) % 72.34/72.45 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 72.34/72.45 => ( ( v14_lattices(A) % 72.34/72.45 & r2_hidden(k6_lattices(A),B) ) % 72.34/72.46 => ( r1_filter_2(u1_struct_0(A),k19_filter_2(A,B),k17_filter_2(A)) % 72.34/72.46 & k19_filter_2(A,B) = u1_struct_0(A) ) ) ) ) ). % 72.34/72.46 % 72.34/72.46 fof(t4_subset,axiom, % 72.34/72.46 ! [A,B,C] : % 72.34/72.46 ( ( r2_hidden(A,B) % 72.34/72.46 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 72.34/72.46 => m1_subset_1(A,C) ) ). % 72.34/72.46 % 72.34/72.46 fof(t5_subset,axiom, % 72.34/72.46 ! [A,B,C] : % 72.34/72.46 ~ ( r2_hidden(A,B) % 72.34/72.46 & m1_subset_1(B,k1_zfmisc_1(C)) % 72.34/72.46 & v1_xboole_0(C) ) ). % 72.34/72.46 % 72.34/72.46 fof(t6_boole,axiom, % 72.34/72.46 ! [A] : % 72.34/72.46 ( v1_xboole_0(A) % 72.34/72.46 => A = k1_xboole_0 ) ). % 72.34/72.46 % 72.34/72.46 fof(t7_boole,axiom, % 72.34/72.46 ! [A,B] : % 72.34/72.46 ~ ( r2_hidden(A,B) % 72.34/72.46 & v1_xboole_0(B) ) ). % 72.34/72.46 % 72.34/72.46 fof(t8_boole,axiom, % 72.34/72.46 ! [A,B] : % 72.34/72.46 ~ ( v1_xboole_0(A) % 72.34/72.46 & A != B % 72.34/72.46 & v1_xboole_0(B) ) ). % 72.34/72.46 % 72.34/72.46 %------------------------------------------------------------------------------ % 72.34/72.46 %------------------------------------------- % 72.34/72.46 % Proof found % 72.34/72.46 % SZS status Theorem for theBenchmark % 72.34/72.46 % SZS output start Proof % 72.34/72.46 %ClaNum:110(EqnAxiom:44) % 72.34/72.46 %VarNum:242(SingletonVarNum:76) % 72.34/72.46 %MaxLitNum:9 % 72.34/72.46 %MaxfuncDepth:2 % 72.34/72.46 %SharedTerms:30 % 72.34/72.46 %goalClause: 45 46 48 56 58 61 102 % 72.34/72.46 %singleGoalClaCount:6 % 72.34/72.46 [45]P1(a1) % 72.34/72.46 [46]P2(a1) % 72.34/72.46 [47]P2(a9) % 72.34/72.46 [48]P12(a1) % 72.34/72.46 [49]P13(a14) % 72.34/72.46 [50]P13(a2) % 72.34/72.46 [51]P3(a10) % 72.34/72.46 [52]P4(a11) % 72.34/72.46 [53]P5(a13) % 72.34/72.46 [54]P5(a5) % 72.34/72.46 [56]P6(a12,a1) % 72.34/72.46 [61]~P15(a1) % 72.34/72.46 [62]~P15(a5) % 72.34/72.46 [63]~P13(a7) % 72.34/72.46 [58]P11(f20(a1),a12) % 72.34/72.46 [57]P8(x571,x571) % 72.34/72.46 [55]P13(f6(x551)) % 72.34/72.46 [59]P7(f15(x591),x591) % 72.34/72.46 [60]P7(f6(x601),f21(x601)) % 72.34/72.46 [64]~P13(f21(x641)) % 72.34/72.46 [102]~P10(f22(a1),a12,f16(a1))+~E(f22(a1),a12) % 72.34/72.46 [65]~P13(x651)+E(x651,a14) % 72.34/72.46 [66]~P13(x661)+P14(x661) % 72.34/72.46 [67]~P2(x671)+P3(x671) % 72.34/72.46 [68]~P2(x681)+P4(x681) % 72.34/72.46 [69]~P3(x691)+P5(x691) % 72.34/72.46 [70]~P4(x701)+P5(x701) % 72.34/72.46 [72]P13(x721)+~P13(f3(x721)) % 72.34/72.46 [83]P13(x831)+P7(f3(x831),f21(x831)) % 72.34/72.46 [82]~P13(x821)+~P11(x822,x821) % 72.34/72.46 [85]~P11(x851,x852)+P7(x851,x852) % 72.34/72.46 [93]~P11(x932,x931)+~P11(x931,x932) % 72.34/72.46 [92]~P8(x921,x922)+P7(x921,f21(x922)) % 72.34/72.46 [94]P8(x941,x942)+~P7(x941,f21(x942)) % 72.34/72.46 [80]~P5(x801)+P15(x801)+~P13(f22(x801)) % 72.34/72.46 [81]~P5(x811)+P15(x811)+~P13(f8(x811)) % 72.34/72.46 [86]~P3(x861)+P15(x861)+P7(f20(x861),f22(x861)) % 72.34/72.46 [96]~P5(x961)+P15(x961)+P7(f8(x961),f21(f22(x961))) % 72.34/72.46 [71]~P13(x712)+~P13(x711)+E(x711,x712) % 72.34/72.46 [91]~P7(x912,x911)+P13(x911)+P11(x912,x911) % 72.34/72.46 [99]~P13(x991)+~P11(x992,x993)+~P7(x993,f21(x991)) % 72.34/72.46 [100]P7(x1001,x1002)+~P11(x1001,x1003)+~P7(x1003,f21(x1002)) % 72.34/72.46 [73]P16(x731)+~P1(x731)+~P2(x731)+P15(x731) % 72.34/72.46 [74]P17(x741)+~P1(x741)+~P2(x741)+P15(x741) % 72.34/72.46 [75]P18(x751)+~P1(x751)+~P2(x751)+P15(x751) % 72.34/72.46 [76]P19(x761)+~P1(x761)+~P2(x761)+P15(x761) % 72.34/72.46 [77]P20(x771)+~P1(x771)+~P2(x771)+P15(x771) % 72.34/72.46 [78]P21(x781)+~P1(x781)+~P2(x781)+P15(x781) % 72.34/72.46 [79]P15(x791)+~P1(x791)+~P2(x791)+E(f16(x791),f22(x791)) % 72.34/72.46 [84]~P1(x841)+~P2(x841)+P15(x841)+~P13(f4(x841)) % 72.34/72.46 [87]~P1(x871)+~P2(x871)+P15(x871)+P6(f16(x871),x871) % 72.34/72.46 [88]~P1(x881)+~P2(x881)+P15(x881)+P6(f17(x881),x881) % 72.34/72.46 [89]~P1(x891)+~P2(x891)+P15(x891)+P9(f18(x891),x891) % 72.34/72.46 [90]~P1(x901)+~P2(x901)+P15(x901)+P9(f4(x901),x901) % 72.34/72.46 [104]P10(x1041,x1042,x1042)+P13(x1041)+~P7(x1042,f21(x1041))+~P7(x1043,f21(x1041)) % 72.34/72.46 [95]~P1(x951)+~P2(x951)+~P6(x952,x951)+P15(x951)+~P13(x952) % 72.34/72.46 [97]~P1(x971)+~P2(x971)+~P6(x972,x971)+P15(x971)+P9(x972,x971) % 72.34/72.46 [106]~P1(x1061)+~P2(x1061)+~P6(x1062,x1061)+P15(x1061)+P10(f22(x1061),f19(x1061,x1062),x1062) % 72.34/72.46 [101]~P1(x1011)+~P2(x1011)+~P9(x1012,x1011)+P15(x1011)+P7(x1012,f21(f22(x1011))) % 72.34/72.46 [105]~E(x1052,x1053)+P13(x1051)+P10(x1051,x1052,x1053)+~P7(x1053,f21(x1051))+~P7(x1052,f21(x1051)) % 72.34/72.46 [108]~P10(x1083,x1081,x1082)+E(x1081,x1082)+P13(x1083)+~P7(x1082,f21(x1083))+~P7(x1081,f21(x1083)) % 72.34/72.46 [110]~P10(x1101,x1103,x1102)+P13(x1101)+P10(x1101,x1102,x1103)+~P7(x1102,f21(x1101))+~P7(x1103,f21(x1101)) % 72.34/72.46 [103]~P1(x1031)+~P2(x1031)+P15(x1031)+P13(x1032)+P6(f19(x1031,x1032),x1031)+~P7(x1032,f21(f22(x1031))) % 72.34/72.46 [107]P15(x1071)+P13(x1072)+~P1(x1071)+~P2(x1071)+~P12(x1071)+~P11(f20(x1071),x1072)+E(f19(x1071,x1072),f22(x1071))+~P7(x1072,f21(f22(x1071))) % 72.34/72.46 [109]~P1(x1091)+~P2(x1091)+~P12(x1091)+P15(x1091)+P13(x1092)+P10(f22(x1091),f19(x1091,x1092),f16(x1091))+~P11(f20(x1091),x1092)+~P7(x1092,f21(f22(x1091))) % 72.34/72.46 [98]P1(x981)+~P2(x981)+~P16(x981)+~P17(x981)+~P18(x981)+~P19(x981)+~P20(x981)+~P21(x981)+P15(x981) % 72.34/72.46 %EqnAxiom % 72.34/72.46 [1]E(x11,x11) % 72.34/72.46 [2]E(x22,x21)+~E(x21,x22) % 72.34/72.46 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 72.34/72.46 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 72.34/72.46 [5]~E(x51,x52)+E(f20(x51),f20(x52)) % 72.34/72.46 [6]~E(x61,x62)+E(f15(x61),f15(x62)) % 72.34/72.46 [7]~E(x71,x72)+E(f21(x71),f21(x72)) % 72.34/72.46 [8]~E(x81,x82)+E(f22(x81),f22(x82)) % 72.34/72.46 [9]~E(x91,x92)+E(f16(x91),f16(x92)) % 72.34/72.46 [10]~E(x101,x102)+E(f3(x101),f3(x102)) % 72.34/72.46 [11]~E(x111,x112)+E(f8(x111),f8(x112)) % 72.34/72.46 [12]~E(x121,x122)+E(f19(x121,x123),f19(x122,x123)) % 72.34/72.46 [13]~E(x131,x132)+E(f19(x133,x131),f19(x133,x132)) % 72.34/72.46 [14]~E(x141,x142)+E(f4(x141),f4(x142)) % 72.34/72.46 [15]~E(x151,x152)+E(f18(x151),f18(x152)) % 72.34/72.46 [16]~E(x161,x162)+E(f17(x161),f17(x162)) % 72.34/72.46 [17]~P1(x171)+P1(x172)+~E(x171,x172) % 72.34/72.46 [18]~P2(x181)+P2(x182)+~E(x181,x182) % 72.34/72.46 [19]~P12(x191)+P12(x192)+~E(x191,x192) % 72.34/72.46 [20]P10(x202,x203,x204)+~E(x201,x202)+~P10(x201,x203,x204) % 72.34/72.46 [21]P10(x213,x212,x214)+~E(x211,x212)+~P10(x213,x211,x214) % 72.34/72.46 [22]P10(x223,x224,x222)+~E(x221,x222)+~P10(x223,x224,x221) % 72.34/72.46 [23]~P13(x231)+P13(x232)+~E(x231,x232) % 72.34/72.46 [24]P7(x242,x243)+~E(x241,x242)+~P7(x241,x243) % 72.34/72.46 [25]P7(x253,x252)+~E(x251,x252)+~P7(x253,x251) % 72.34/72.46 [26]~P3(x261)+P3(x262)+~E(x261,x262) % 72.34/72.46 [27]~P4(x271)+P4(x272)+~E(x271,x272) % 72.34/72.46 [28]~P5(x281)+P5(x282)+~E(x281,x282) % 72.34/72.46 [29]P11(x292,x293)+~E(x291,x292)+~P11(x291,x293) % 72.34/72.46 [30]P11(x303,x302)+~E(x301,x302)+~P11(x303,x301) % 72.34/72.46 [31]~P15(x311)+P15(x312)+~E(x311,x312) % 72.34/72.46 [32]P6(x322,x323)+~E(x321,x322)+~P6(x321,x323) % 72.34/72.46 [33]P6(x333,x332)+~E(x331,x332)+~P6(x333,x331) % 72.34/72.46 [34]P8(x342,x343)+~E(x341,x342)+~P8(x341,x343) % 72.34/72.46 [35]P8(x353,x352)+~E(x351,x352)+~P8(x353,x351) % 72.34/72.46 [36]P9(x362,x363)+~E(x361,x362)+~P9(x361,x363) % 72.34/72.46 [37]P9(x373,x372)+~E(x371,x372)+~P9(x373,x371) % 72.34/72.46 [38]~P16(x381)+P16(x382)+~E(x381,x382) % 72.34/72.46 [39]~P21(x391)+P21(x392)+~E(x391,x392) % 72.34/72.46 [40]~P18(x401)+P18(x402)+~E(x401,x402) % 72.34/72.46 [41]~P20(x411)+P20(x412)+~E(x411,x412) % 72.34/72.46 [42]~P19(x421)+P19(x422)+~E(x421,x422) % 72.34/72.46 [43]~P17(x431)+P17(x432)+~E(x431,x432) % 72.34/72.46 [44]~P14(x441)+P14(x442)+~E(x441,x442) % 72.34/72.46 % 72.34/72.46 %------------------------------------------- % 72.47/72.49 cnf(112,plain, % 72.47/72.49 (~P11(x1121,a14)), % 72.47/72.49 inference(scs_inference,[],[49,82])). % 72.47/72.49 cnf(116,plain, % 72.47/72.49 (P8(f15(f21(x1161)),x1161)), % 72.47/72.49 inference(scs_inference,[],[58,59,49,82,93,94])). % 72.47/72.49 cnf(117,plain, % 72.47/72.49 (P7(f15(x1171),x1171)), % 72.47/72.49 inference(rename_variables,[],[59])). % 72.47/72.49 cnf(119,plain, % 72.47/72.49 (~P11(x1191,f15(f21(a14)))), % 72.47/72.49 inference(scs_inference,[],[58,59,117,49,82,93,94,99])). % 72.47/72.49 cnf(120,plain, % 72.47/72.49 (P7(f15(x1201),x1201)), % 72.47/72.49 inference(rename_variables,[],[59])). % 72.47/72.49 cnf(122,plain, % 72.47/72.49 (~E(a12,a14)), % 72.47/72.49 inference(scs_inference,[],[58,59,117,49,82,93,94,99,30])). % 72.47/72.49 cnf(123,plain, % 72.47/72.49 (P11(f15(a7),a7)), % 72.47/72.49 inference(scs_inference,[],[58,59,117,120,49,63,82,93,94,99,30,91])). % 72.47/72.49 cnf(124,plain, % 72.47/72.49 (P7(f15(x1241),x1241)), % 72.47/72.49 inference(rename_variables,[],[59])). % 72.47/72.49 cnf(142,plain, % 72.47/72.49 (~P6(a14,a1)), % 72.47/72.49 inference(scs_inference,[],[45,46,61,58,59,117,120,124,49,63,82,93,94,99,30,91,73,74,75,76,77,78,104,95])). % 72.47/72.49 cnf(144,plain, % 72.47/72.49 (P9(a12,a1)), % 72.47/72.49 inference(scs_inference,[],[45,46,56,61,58,59,117,120,124,49,63,82,93,94,99,30,91,73,74,75,76,77,78,104,95,97])). % 72.47/72.49 cnf(146,plain, % 72.47/72.49 (~P13(a12)), % 72.47/72.49 inference(scs_inference,[],[45,46,56,61,58,59,117,120,124,49,63,82,93,94,99,30,91,73,74,75,76,77,78,104,95,97,65])). % 72.47/72.49 cnf(161,plain, % 72.47/72.49 (~P11(a7,f15(a7))), % 72.47/72.49 inference(scs_inference,[],[123,93])). % 72.47/72.49 cnf(163,plain, % 72.47/72.49 (P8(f6(x1631),x1631)), % 72.47/72.49 inference(scs_inference,[],[60,123,93,94])). % 72.47/72.49 cnf(165,plain, % 72.47/72.49 (~P11(x1651,a2)), % 72.47/72.49 inference(scs_inference,[],[60,123,50,93,94,82])). % 72.47/72.49 cnf(167,plain, % 72.47/72.49 (P11(f15(a12),a12)), % 72.47/72.49 inference(scs_inference,[],[60,123,50,146,59,93,94,82,91])). % 72.47/72.49 cnf(170,plain, % 72.47/72.49 (~P11(x1701,f6(a2))), % 72.47/72.49 inference(scs_inference,[],[60,123,50,146,59,93,94,82,91,99])). % 72.47/72.49 cnf(171,plain, % 72.47/72.49 (P7(f6(x1711),f21(x1711))), % 72.47/72.49 inference(rename_variables,[],[60])). % 72.47/72.49 cnf(175,plain, % 72.47/72.49 (P10(a12,f6(a12),f6(a12))), % 72.47/72.49 inference(scs_inference,[],[58,119,60,171,123,50,146,59,93,94,82,91,99,30,104])). % 72.47/72.49 cnf(177,plain, % 72.47/72.49 (P7(f6(x1771),f21(x1771))), % 72.47/72.49 inference(rename_variables,[],[60])). % 72.47/72.49 cnf(179,plain, % 72.47/72.49 (~P6(a2,a1)), % 72.47/72.49 inference(scs_inference,[],[45,46,58,61,119,60,171,123,50,146,59,93,94,82,91,99,30,104,95])). % 72.47/72.49 cnf(181,plain, % 72.47/72.49 (P7(x1811,f21(x1812))+~E(f6(x1812),x1811)), % 72.47/72.49 inference(scs_inference,[],[45,46,58,61,119,60,171,177,123,50,146,59,93,94,82,91,99,30,104,95,24])). % 72.47/72.49 cnf(194,plain, % 72.47/72.49 (~P11(x1941,f6(x1942))), % 72.47/72.49 inference(scs_inference,[],[55,82])). % 72.47/72.49 cnf(199,plain, % 72.47/72.49 (P11(f15(f21(x1991)),f21(x1991))), % 72.47/72.49 inference(scs_inference,[],[56,179,167,55,64,59,82,93,32,91])). % 72.47/72.49 cnf(200,plain, % 72.47/72.49 (P7(f15(x2001),x2001)), % 72.47/72.49 inference(rename_variables,[],[59])). % 72.47/72.49 cnf(204,plain, % 72.47/72.49 (P10(f21(x2041),f6(f21(x2041)),f6(f21(x2041)))), % 72.47/72.49 inference(scs_inference,[],[56,58,170,179,167,55,64,59,200,60,82,93,32,91,30,104])). % 72.47/72.49 cnf(206,plain, % 72.47/72.49 (P7(f15(x2061),x2061)), % 72.47/72.49 inference(rename_variables,[],[59])). % 72.47/72.49 cnf(208,plain, % 72.47/72.49 (~P6(f6(x2081),a1)), % 72.47/72.49 inference(scs_inference,[],[45,56,46,58,61,170,179,167,55,64,59,200,60,82,93,32,91,30,104,95])). % 72.47/72.49 cnf(213,plain, % 72.47/72.49 (P8(f15(x2131),f6(x2132))+~E(x2131,f21(f6(x2132)))), % 72.47/72.49 inference(scs_inference,[],[45,56,46,58,61,170,179,167,55,64,59,200,206,60,82,93,32,91,30,104,95,25,99,94])). % 72.47/72.49 cnf(221,plain, % 72.47/72.49 (~E(a12,f6(x2211))), % 72.47/72.49 inference(scs_inference,[],[56,208,199,93,32])). % 72.47/72.49 cnf(224,plain, % 72.47/72.49 (P10(a7,f6(a7),f6(a7))), % 72.47/72.49 inference(scs_inference,[],[56,194,208,199,63,59,60,93,32,30,104])). % 72.47/72.49 cnf(229,plain, % 72.47/72.49 (P11(x2291,f21(x2292))+~E(f15(f21(x2292)),x2291)), % 72.47/72.49 inference(scs_inference,[],[56,194,208,199,204,63,59,60,93,32,30,104,21,29])). % 72.47/72.49 cnf(231,plain, % 72.47/72.49 (P8(f6(x2311),x2312)+~E(x2311,x2312)), % 72.47/72.49 inference(scs_inference,[],[56,194,208,163,199,204,63,59,60,93,32,30,104,21,29,20,35])). % 72.47/72.49 cnf(243,plain, % 72.47/72.49 (P10(a12,f6(a12),x2431)+~E(f6(a12),x2431)), % 72.47/72.49 inference(scs_inference,[],[112,116,175,123,30,34,22])). % 72.47/72.49 cnf(245,plain, % 72.47/72.49 (P10(a12,x2451,f6(a12))+~E(f6(a12),x2451)), % 72.47/72.49 inference(scs_inference,[],[112,116,175,123,60,30,34,22,25,21])). % 72.47/72.49 cnf(246,plain, % 72.47/72.49 (P7(x2461,x2462)+~E(f15(x2462),x2461)), % 72.47/72.49 inference(scs_inference,[],[112,116,175,123,59,60,30,34,22,25,21,24])). % 72.47/72.49 cnf(254,plain, % 72.47/72.49 (~E(a7,a2)), % 72.47/72.49 inference(scs_inference,[],[165,123,30])). % 72.47/72.49 cnf(261,plain, % 72.47/72.49 (P11(f6(x2611),f21(x2611))), % 72.47/72.49 inference(scs_inference,[],[60,64,91])). % 72.47/72.49 cnf(266,plain, % 72.47/72.49 (P10(a7,x2661,f6(a7))+~E(f6(a7),x2661)), % 72.47/72.49 inference(scs_inference,[],[194,60,64,123,224,91,30,21])). % 72.47/72.49 cnf(270,plain, % 72.47/72.49 (P8(x2701,x2702)+~E(x2702,x2701)), % 72.47/72.49 inference(scs_inference,[],[194,60,64,123,224,116,57,91,30,21,35,29,20,34])). % 72.47/72.49 cnf(271,plain, % 72.47/72.49 (P10(a7,f6(a7),x2711)+~E(f6(a7),x2711)), % 72.47/72.49 inference(scs_inference,[],[194,60,64,123,224,116,57,91,30,21,35,29,20,34,22])). % 72.47/72.49 cnf(280,plain, % 72.47/72.49 (P11(x2801,f21(x2802))+~E(f6(x2802),x2801)), % 72.47/72.49 inference(scs_inference,[],[119,199,261,30,29])). % 72.47/72.49 cnf(285,plain, % 72.47/72.49 (~P11(x2851,f15(f21(a2)))), % 72.47/72.49 inference(scs_inference,[],[59,50,99])). % 72.47/72.49 cnf(290,plain, % 72.47/72.49 (P8(x2901,x2902)+~E(f6(x2902),x2901)), % 72.47/72.49 inference(scs_inference,[],[112,59,199,50,163,99,30,34])). % 72.47/72.49 cnf(291,plain, % 72.47/72.49 (P8(x2911,x2912)+~E(x2911,x2912)), % 72.47/72.49 inference(scs_inference,[],[112,59,199,50,163,57,99,30,34,35])). % 72.47/72.49 cnf(353,plain, % 72.47/72.49 (~E(a1,x3531)+P4(x3531)), % 72.47/72.49 inference(scs_inference,[],[46,68,27])). % 72.47/72.49 cnf(354,plain, % 72.47/72.49 (P4(a1)), % 72.47/72.49 inference(equality_inference,[],[353])). % 72.47/72.49 cnf(370,plain, % 72.47/72.49 (~P13(f22(a1))), % 72.47/72.49 inference(scs_inference,[],[354,61,70,80])). % 72.47/72.49 cnf(371,plain, % 72.47/72.49 (P11(f15(f22(a1)),f22(a1))), % 72.47/72.49 inference(scs_inference,[],[370,59,91])). % 72.47/72.49 cnf(382,plain, % 72.47/72.49 (P10(f22(a1),x3821,f6(f22(a1)))+~E(f6(f22(a1)),x3821)), % 72.47/72.49 inference(scs_inference,[],[370,194,60,59,91,30,104,93,21])). % 72.47/72.49 cnf(385,plain, % 72.47/72.49 (P10(f22(a1),f6(f22(a1)),x3851)+~E(f6(f22(a1)),x3851)), % 72.47/72.49 inference(scs_inference,[],[370,194,60,59,91,30,104,93,21,20,29,22])). % 72.47/72.49 cnf(400,plain, % 72.47/72.49 (~E(f22(a1),a14)), % 72.47/72.49 inference(scs_inference,[],[112,371,30])). % 72.47/72.49 cnf(404,plain, % 72.47/72.49 (~E(f22(a1),a2)), % 72.47/72.49 inference(scs_inference,[],[165,371,30])). % 72.47/72.49 cnf(418,plain, % 72.47/72.49 (~P13(f3(a12))), % 72.47/72.49 inference(scs_inference,[],[122,72,65])). % 72.47/72.49 cnf(419,plain, % 72.47/72.49 (P11(f15(f3(a12)),f3(a12))), % 72.47/72.49 inference(scs_inference,[],[59,418,91])). % 72.47/72.49 cnf(422,plain, % 72.47/72.49 (~E(f3(a12),f6(x4221))), % 72.47/72.49 inference(scs_inference,[],[194,59,418,91,30])). % 72.47/72.49 cnf(430,plain, % 72.47/72.49 (~E(f22(a1),f15(f21(a14)))), % 72.47/72.49 inference(scs_inference,[],[119,371,30])). % 72.47/72.49 cnf(434,plain, % 72.47/72.49 (~E(f22(a1),f15(f21(a2)))), % 72.47/72.49 inference(scs_inference,[],[285,371,30])). % 72.47/72.49 cnf(438,plain, % 72.47/72.49 (~E(f3(a12),a14)), % 72.47/72.49 inference(scs_inference,[],[112,419,30])). % 72.47/72.49 cnf(472,plain, % 72.47/72.49 (P7(f3(a12),f21(a12))), % 72.47/72.49 inference(scs_inference,[],[58,83,82])). % 72.47/72.49 cnf(473,plain, % 72.47/72.49 (P8(f3(a12),a12)), % 72.47/72.49 inference(scs_inference,[],[472,94])). % 72.47/72.49 cnf(475,plain, % 72.47/72.49 (P7(f15(f3(a12)),a12)), % 72.47/72.49 inference(scs_inference,[],[419,472,94,100])). % 72.47/72.49 cnf(477,plain, % 72.47/72.49 (P10(a12,f3(a12),f3(a12))), % 72.47/72.49 inference(scs_inference,[],[419,146,472,94,100,104])). % 72.47/72.49 cnf(483,plain, % 72.47/72.49 (P11(f15(f3(a12)),a12)), % 72.47/72.49 inference(scs_inference,[],[475,146,91])). % 72.47/72.49 cnf(490,plain, % 72.47/72.49 (P8(x4901,a12)+~E(f3(a12),x4901)), % 72.47/72.49 inference(scs_inference,[],[475,146,477,473,91,93,24,25,21,34])). % 72.47/72.49 cnf(529,plain, % 72.47/72.49 (~E(x5291,x5292)+P7(f6(x5291),f21(x5292))), % 72.47/72.49 inference(scs_inference,[],[92,231])). % 72.47/72.49 cnf(546,plain, % 72.47/72.49 (E(f6(f6(x5461)),f6(a14))), % 72.47/72.49 inference(scs_inference,[],[55,4,65])). % 72.47/72.49 cnf(547,plain, % 72.47/72.49 (P11(f6(a14),f21(f6(x5471)))), % 72.47/72.49 inference(scs_inference,[],[546,280])). % 72.47/72.49 cnf(548,plain, % 72.47/72.49 (P7(f6(a14),f21(f6(x5481)))), % 72.47/72.49 inference(scs_inference,[],[546,280,181])). % 72.47/72.49 cnf(550,plain, % 72.47/72.49 (P8(f6(a14),f6(x5501))), % 72.47/72.49 inference(scs_inference,[],[546,280,181,270,290])). % 72.47/72.49 cnf(551,plain, % 72.47/72.49 (P8(f6(f6(x5511)),f6(a14))), % 72.47/72.49 inference(scs_inference,[],[546,280,181,270,290,291])). % 72.47/72.49 cnf(552,plain, % 72.47/72.49 (E(f6(a14),f6(f6(x5521)))), % 72.47/72.49 inference(scs_inference,[],[546,280,181,270,290,291,2])). % 72.47/72.49 cnf(561,plain, % 72.47/72.49 (P11(f6(f6(x5611)),f21(a14))), % 72.47/72.49 inference(scs_inference,[],[552,181,290,280])). % 72.47/72.49 cnf(565,plain, % 72.47/72.49 (P7(f6(f6(x5651)),f21(f6(x5652)))), % 72.47/72.49 inference(scs_inference,[],[547,552,550,551,548,181,290,280,35,34,29,24])). % 72.47/72.49 cnf(592,plain, % 72.47/72.49 (P8(f6(f6(x5921)),x5922)+~E(f21(f6(x5923)),f21(x5922))), % 72.47/72.49 inference(scs_inference,[],[565,25,94])). % 72.47/72.49 cnf(1957,plain, % 72.47/72.49 (~P10(x19571,a12,f16(a1))+~E(x19571,f22(a1))+~E(f22(a1),a12)), % 72.47/72.49 inference(scs_inference,[],[102,20])). % 72.47/72.49 cnf(2838,plain, % 72.47/72.49 (~P10(f16(a1),a12,f16(a1))+~E(f22(a1),a12)), % 72.47/72.49 inference(scs_inference,[],[45,46,61,1957,79])). % 72.47/72.49 cnf(2874,plain, % 72.47/72.49 (~P10(x28741,a12,f16(a1))+~E(x28741,f16(a1))+~E(f22(a1),a12)), % 72.47/72.49 inference(scs_inference,[],[2838,20])). % 72.47/72.49 cnf(3795,plain, % 72.47/72.49 (P7(f20(a1),f22(a1))), % 72.47/72.49 inference(scs_inference,[],[46,61,67,86])). % 72.47/72.49 cnf(3796,plain, % 72.47/72.49 (P11(f20(a1),f22(a1))), % 72.47/72.49 inference(scs_inference,[],[370,3795,91])). % 72.47/72.49 cnf(3802,plain, % 72.47/72.49 (~E(f22(a1),f15(a7))+~E(f20(a1),a7)), % 72.47/72.49 inference(scs_inference,[],[370,161,3795,91,93,24,29,30])). % 72.47/72.49 cnf(3836,plain, % 72.47/72.49 (~E(a7,f20(a1))+~E(f22(a1),f15(a7))), % 72.47/72.49 inference(scs_inference,[],[3802,2])). % 72.47/72.49 cnf(3903,plain, % 72.47/72.49 (~E(f15(a7),f22(a1))+~E(a7,f20(a1))), % 72.47/72.49 inference(scs_inference,[],[3836,2])). % 72.47/72.49 cnf(3973,plain, % 72.47/72.49 (~E(x39731,f22(a1))+~E(f15(a7),x39731)+~E(a7,f20(a1))), % 72.47/72.49 inference(scs_inference,[],[3903,3])). % 72.47/72.49 cnf(5132,plain, % 72.47/72.49 (~P13(f8(a1))), % 72.47/72.49 inference(scs_inference,[],[354,61,70,81])). % 72.47/72.49 cnf(5133,plain, % 72.47/72.49 (P11(f15(f8(a1)),f8(a1))), % 72.47/72.49 inference(scs_inference,[],[5132,59,91])). % 72.47/72.49 cnf(5136,plain, % 72.47/72.49 (~P11(f8(a1),f15(f8(a1)))), % 72.47/72.49 inference(scs_inference,[],[5132,59,91,93])). % 72.47/72.49 cnf(5138,plain, % 72.47/72.49 (~E(f8(a1),f15(f21(a14)))), % 72.47/72.49 inference(scs_inference,[],[119,5132,59,91,93,30])). % 72.47/72.49 cnf(5202,plain, % 72.47/72.49 (~E(f8(a1),f6(x52021))), % 72.47/72.49 inference(scs_inference,[],[194,5133,30])). % 72.47/72.49 cnf(5319,plain, % 72.47/72.49 (P7(f8(a1),f21(f22(a1)))), % 72.47/72.49 inference(scs_inference,[],[354,61,70,96])). % 72.47/72.49 cnf(5325,plain, % 72.47/72.49 (P7(f15(f8(a1)),f22(a1))), % 72.47/72.49 inference(scs_inference,[],[5319,5133,64,94,91,100])). % 72.47/72.49 cnf(5328,plain, % 72.47/72.49 (P10(f22(a1),f8(a1),f8(a1))), % 72.47/72.49 inference(scs_inference,[],[370,5136,5319,5133,64,94,91,100,30,104])). % 72.47/72.49 cnf(5330,plain, % 72.47/72.49 (~P10(f22(a1),f8(a1),f6(f22(a1)))), % 72.47/72.49 inference(scs_inference,[],[370,5136,5202,5319,60,5133,64,94,91,100,30,104,108])). % 72.47/72.49 cnf(5334,plain, % 72.47/72.49 (P6(f19(a1,f8(a1)),a1)), % 72.47/72.49 inference(scs_inference,[],[46,45,61,370,5136,5202,5319,5132,60,5133,64,94,91,100,30,104,108,103])). % 72.47/72.49 cnf(5337,plain, % 72.47/72.49 (~P11(f21(f22(a1)),f8(a1))), % 72.47/72.49 inference(scs_inference,[],[46,45,61,370,5136,5202,5319,5132,60,5133,64,94,91,100,30,104,108,103,382,93])). % 72.47/72.49 cnf(5341,plain, % 72.47/72.49 (~E(f19(a1,f8(a1)),a2)), % 72.47/72.49 inference(scs_inference,[],[46,45,61,370,5136,5202,5319,5132,179,60,5133,64,94,91,100,30,104,108,103,382,93,29,24,32])). % 72.47/72.49 cnf(5357,plain, % 72.47/72.49 (~P13(f19(a1,f8(a1)))), % 72.47/72.49 inference(scs_inference,[],[5341,50,71])). % 72.47/72.49 cnf(5368,plain, % 72.47/72.49 (P10(x53681,f8(a1),f8(a1))+~E(f22(a1),x53681)), % 72.47/72.49 inference(scs_inference,[],[5325,5334,142,5328,32,24,20])). % 72.47/72.49 cnf(5369,plain, % 72.47/72.49 (P7(f8(a1),x53691)+~E(f21(f22(a1)),x53691)), % 72.47/72.49 inference(scs_inference,[],[5319,5325,5334,142,5328,32,24,20,25])). % 72.47/72.49 cnf(5382,plain, % 72.47/72.49 (P8(f15(f8(a1)),f22(a1))+~E(f22(a1),f21(f22(a1)))), % 72.47/72.49 inference(scs_inference,[],[370,5319,5325,25,104,94])). % 72.47/72.49 cnf(5451,plain, % 72.47/72.49 (P11(f15(f8(a1)),f22(a1))), % 72.47/72.49 inference(scs_inference,[],[5325,370,91])). % 72.47/72.49 cnf(5814,plain, % 72.47/72.49 (~E(f21(f22(a1)),f22(a1))+P8(f15(f8(a1)),f22(a1))), % 72.47/72.49 inference(scs_inference,[],[5382,2])). % 72.47/72.49 cnf(5878,plain, % 72.47/72.49 (~E(x58781,f22(a1))+~E(f21(f22(a1)),x58781)+P8(f15(f8(a1)),f22(a1))), % 72.47/72.49 inference(scs_inference,[],[5814,3])). % 72.47/72.49 cnf(6083,plain, % 72.47/72.49 (P11(f3(a12),f21(a12))), % 72.47/72.49 inference(scs_inference,[],[472,64,91])). % 72.47/72.49 cnf(6089,plain, % 72.47/72.49 (~P11(f21(a12),f3(a12))), % 72.47/72.49 inference(scs_inference,[],[6083,93])). % 72.47/72.49 cnf(6155,plain, % 72.47/72.49 (~E(f6(x61551),f22(a1))), % 72.47/72.49 inference(scs_inference,[],[430,370,47,55,67,2,23])). % 72.47/72.49 cnf(6160,plain, % 72.47/72.49 (~E(a14,f22(a1))), % 72.47/72.49 inference(scs_inference,[],[434,370,49,2,23])). % 72.47/72.49 cnf(6168,plain, % 72.47/72.49 (~E(a2,f22(a1))), % 72.47/72.49 inference(scs_inference,[],[58,5138,370,50,85,2,23])). % 72.47/72.49 cnf(6210,plain, % 72.47/72.49 (~E(x62101,f21(a14))+~E(f8(a1),f15(x62101))), % 72.47/72.49 inference(scs_inference,[],[5138,438,5357,49,2,23,3,6])). % 72.47/72.49 cnf(6233,plain, % 72.47/72.49 (~E(x62331,a14)+~E(f22(a1),x62331)), % 72.47/72.49 inference(scs_inference,[],[400,254,2,3])). % 72.47/72.49 cnf(6263,plain, % 72.47/72.49 (~E(x62631,a2)+~E(f22(a1),x62631)), % 72.47/72.49 inference(scs_inference,[],[404,3])). % 72.47/72.49 cnf(6360,plain, % 72.47/72.49 (~E(x63601,f22(a1))+~E(a14,x63601)), % 72.47/72.49 inference(scs_inference,[],[6160,3])). % 72.47/72.49 cnf(6373,plain, % 72.47/72.49 (~E(x63731,f22(a1))+~E(a2,x63731)), % 72.47/72.49 inference(scs_inference,[],[6168,3])). % 72.47/72.49 cnf(6667,plain, % 72.47/72.49 (P7(x66671,f21(x66671))), % 72.47/72.49 inference(scs_inference,[],[418,57,50,47,66,68,72,92])). % 72.47/72.49 cnf(6671,plain, % 72.47/72.49 (E(a2,a14)), % 72.47/72.49 inference(scs_inference,[],[418,57,50,47,66,68,72,92,83,65])). % 72.47/72.49 cnf(6673,plain, % 72.47/72.49 (E(f19(a2,x66731),f19(a14,x66731))), % 72.47/72.49 inference(scs_inference,[],[418,57,50,47,66,68,72,92,83,65,12])). % 72.47/72.49 cnf(6674,plain, % 72.47/72.49 (E(f19(x66741,a2),f19(x66741,a14))), % 72.47/72.49 inference(scs_inference,[],[418,57,50,47,66,68,72,92,83,65,12,13])). % 72.47/72.49 cnf(6675,plain, % 72.47/72.49 (E(a14,a2)), % 72.47/72.49 inference(scs_inference,[],[418,57,50,47,66,68,72,92,83,65,12,13,2])). % 72.47/72.49 cnf(6677,plain, % 72.47/72.49 (E(f21(a2),f21(a14))), % 72.47/72.49 inference(scs_inference,[],[418,57,50,47,66,68,72,92,83,65,12,13,2,231,7])). % 72.47/72.49 cnf(6678,plain, % 72.47/72.49 (E(f15(a2),f15(a14))), % 72.47/72.49 inference(scs_inference,[],[418,57,50,47,66,68,72,92,83,65,12,13,2,231,7,6])). % 72.47/72.49 cnf(6679,plain, % 72.47/72.49 (~P13(f22(a5))), % 72.47/72.49 inference(scs_inference,[],[62,418,54,57,50,47,66,68,72,92,83,65,12,13,2,231,7,6,80])). % 72.47/72.49 cnf(6681,plain, % 72.47/72.49 (~P13(f8(a5))), % 72.47/72.49 inference(scs_inference,[],[62,418,54,57,50,47,66,68,72,92,83,65,12,13,2,231,7,6,80,81])). % 72.47/72.49 cnf(6683,plain, % 72.47/72.49 (P7(f8(a5),f21(f22(a5)))), % 72.47/72.49 inference(scs_inference,[],[62,418,54,57,50,47,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96])). % 72.47/72.49 cnf(6686,plain, % 72.47/72.49 (~P7(f22(a1),f21(a14))), % 72.47/72.49 inference(scs_inference,[],[62,5451,418,54,57,546,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99])). % 72.47/72.49 cnf(6688,plain, % 72.47/72.49 (P11(f6(a2),f21(a14))), % 72.47/72.49 inference(scs_inference,[],[62,5451,418,261,54,57,546,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30])). % 72.47/72.49 cnf(6690,plain, % 72.47/72.49 (~P7(f22(a1),f21(a2))), % 72.47/72.49 inference(scs_inference,[],[62,5451,418,261,54,57,546,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25])). % 72.47/72.49 cnf(6691,plain, % 72.47/72.49 (~P7(f21(a12),f3(a12))), % 72.47/72.49 inference(scs_inference,[],[62,5451,6089,418,261,54,57,546,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91])). % 72.47/72.49 cnf(6695,plain, % 72.47/72.49 (~P13(f4(a1))), % 72.47/72.49 inference(scs_inference,[],[45,62,5451,6089,418,261,54,204,57,546,46,61,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84])). % 72.47/72.49 cnf(6697,plain, % 72.47/72.49 (P6(f16(a1),a1)), % 72.47/72.49 inference(scs_inference,[],[45,62,5451,6089,418,261,54,204,57,546,46,61,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87])). % 72.47/72.49 cnf(6699,plain, % 72.47/72.49 (P6(f17(a1),a1)), % 72.47/72.49 inference(scs_inference,[],[45,62,5451,6089,418,261,54,204,57,546,46,61,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88])). % 72.47/72.49 cnf(6701,plain, % 72.47/72.49 (P9(f18(a1),a1)), % 72.47/72.49 inference(scs_inference,[],[45,62,5451,6089,418,261,54,204,57,546,46,61,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89])). % 72.47/72.49 cnf(6703,plain, % 72.47/72.49 (P9(f4(a1),a1)), % 72.47/72.49 inference(scs_inference,[],[45,62,5451,6089,418,261,54,204,57,546,46,61,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90])). % 72.47/72.49 cnf(6706,plain, % 72.47/72.49 (P7(f6(x67061),f21(x67061))), % 72.47/72.49 inference(rename_variables,[],[60])). % 72.47/72.49 cnf(6708,plain, % 72.47/72.49 (E(f16(a1),f22(a1))), % 72.47/72.49 inference(scs_inference,[],[45,62,5451,6089,418,261,54,204,57,546,46,61,60,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79])). % 72.47/72.49 cnf(6710,plain, % 72.47/72.49 (P7(a12,f21(f22(a1)))), % 72.47/72.49 inference(scs_inference,[],[45,62,5451,6089,418,261,54,204,57,546,144,46,61,60,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101])). % 72.47/72.49 cnf(6714,plain, % 72.47/72.49 (P7(f6(x67141),f21(x67141))), % 72.47/72.49 inference(rename_variables,[],[60])). % 72.47/72.49 cnf(6718,plain, % 72.47/72.49 (~P10(f3(a12),f6(f3(a12)),f3(a12))), % 72.47/72.49 inference(scs_inference,[],[45,62,5451,6089,418,422,261,54,5334,204,57,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110])). % 72.47/72.49 cnf(6721,plain, % 72.47/72.49 (E(f19(a1,a12),f22(a1))), % 72.47/72.49 inference(scs_inference,[],[45,62,5451,6089,418,422,261,54,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107])). % 72.47/72.49 cnf(6723,plain, % 72.47/72.49 (P10(f22(a1),f19(a1,a12),f16(a1))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,54,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109])). % 72.47/72.50 cnf(6725,plain, % 72.47/72.50 (P7(f6(a2),f21(a14))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,54,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529])). % 72.47/72.50 cnf(6729,plain, % 72.47/72.50 (E(f6(a2),f6(a14))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,54,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4])). % 72.47/72.50 cnf(6730,plain, % 72.47/72.50 (E(f22(a2),f22(a14))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,54,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8])). % 72.47/72.50 cnf(6731,plain, % 72.47/72.50 (E(f16(a2),f16(a14))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,54,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9])). % 72.47/72.50 cnf(6732,plain, % 72.47/72.50 (E(f3(a2),f3(a14))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,54,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9,10])). % 72.47/72.50 cnf(6733,plain, % 72.47/72.50 (E(f8(a2),f8(a14))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,54,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9,10,11])). % 72.47/72.50 cnf(6734,plain, % 72.47/72.50 (E(f4(a2),f4(a14))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,54,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9,10,11,14])). % 72.47/72.50 cnf(6735,plain, % 72.47/72.50 (E(f18(a2),f18(a14))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,54,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9,10,11,14,15])). % 72.47/72.50 cnf(6736,plain, % 72.47/72.50 (E(f17(a2),f17(a14))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,54,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9,10,11,14,15,16])). % 72.47/72.50 cnf(6740,plain, % 72.47/72.50 (E(f20(a2),f20(a14))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,54,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9,10,11,14,15,16,6210,85,5])). % 72.47/72.50 cnf(6743,plain, % 72.47/72.50 (P7(f15(f3(a12)),f22(a1))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,483,54,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9,10,11,14,15,16,6210,85,5,86,100])). % 72.47/72.50 cnf(6745,plain, % 72.47/72.50 (P8(f6(a14),a2)), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,483,54,163,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9,10,11,14,15,16,6210,85,5,86,100,34])). % 72.47/72.50 cnf(6746,plain, % 72.47/72.50 (P8(f6(x67461),x67461)), % 72.47/72.50 inference(rename_variables,[],[163])). % 72.47/72.50 cnf(6747,plain, % 72.47/72.50 (P10(f22(a1),f19(a1,a12),f22(a1))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,483,54,163,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9,10,11,14,15,16,6210,85,5,86,100,34,22])). % 72.47/72.50 cnf(6748,plain, % 72.47/72.50 (P7(f15(a14),a2)), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,483,54,163,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,59,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9,10,11,14,15,16,6210,85,5,86,100,34,22,24])). % 72.47/72.50 cnf(6750,plain, % 72.47/72.50 (P6(f22(a1),a1)), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,483,54,163,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,59,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9,10,11,14,15,16,6210,85,5,86,100,34,22,24,32])). % 72.47/72.50 cnf(6751,plain, % 72.47/72.50 (P10(f22(a1),f22(a1),f16(a1))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,483,54,163,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,59,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9,10,11,14,15,16,6210,85,5,86,100,34,22,24,32,21])). % 72.47/72.50 cnf(6752,plain, % 72.47/72.50 (P8(f6(f19(a2,x67521)),f19(a14,x67521))), % 72.47/72.50 inference(scs_inference,[],[45,62,5451,6089,418,422,261,483,54,163,6746,5334,204,57,48,146,58,546,144,46,61,60,6706,6714,49,50,59,47,552,66,68,72,92,83,65,12,13,2,231,7,6,80,81,96,3,99,30,25,91,20,84,87,88,89,90,104,79,101,108,97,110,107,109,529,6360,6373,4,8,9,10,11,14,15,16,6210,85,5,86,100,34,22,24,32,21,35])). % 72.47/72.50 cnf(6760,plain, % 72.47/72.50 (P7(f6(a14),f21(a2))), % 72.47/72.50 inference(scs_inference,[],[6745,92])). % 72.47/72.50 cnf(6764,plain, % 72.47/72.50 (E(f16(a14),f16(a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6745,55,92,66,9])). % 72.47/72.50 cnf(6765,plain, % 72.47/72.50 (P7(f3(a7),f21(a7))), % 72.47/72.50 inference(scs_inference,[],[6675,6745,63,55,92,66,9,83])). % 72.47/72.50 cnf(6767,plain, % 72.47/72.50 (E(f3(a14),f3(a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6745,63,55,92,66,9,83,10])). % 72.47/72.50 cnf(6768,plain, % 72.47/72.50 (E(f22(a14),f22(a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6745,63,55,92,66,9,83,10,8])). % 72.47/72.50 cnf(6769,plain, % 72.47/72.50 (~P11(f22(a1),f21(a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6690,6745,63,55,92,66,9,83,10,8,85])). % 72.47/72.50 cnf(6775,plain, % 72.47/72.50 (E(f17(a14),f17(a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6681,6690,6745,63,55,92,66,9,83,10,8,85,6373,72,6360,16])). % 72.47/72.50 cnf(6776,plain, % 72.47/72.50 (E(f4(a14),f4(a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6681,6690,6745,63,55,92,66,9,83,10,8,85,6373,72,6360,16,14])). % 72.47/72.50 cnf(6777,plain, % 72.47/72.50 (E(f8(a14),f8(a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6681,6690,6745,63,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11])). % 72.47/72.50 cnf(6778,plain, % 72.47/72.50 (E(f18(a14),f18(a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6681,6690,6745,63,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15])). % 72.47/72.50 cnf(6779,plain, % 72.47/72.50 (E(f6(a14),f6(a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6681,6690,6745,63,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4])). % 72.47/72.50 cnf(6780,plain, % 72.47/72.50 (E(f6(x67801),a14)), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6681,6690,6745,63,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65])). % 72.47/72.50 cnf(6782,plain, % 72.47/72.50 (E(f20(a14),f20(a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6681,6690,6745,63,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5])). % 72.47/72.50 cnf(6784,plain, % 72.47/72.50 (E(f21(a14),f21(a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6681,6690,6745,63,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7])). % 72.47/72.50 cnf(6785,plain, % 72.47/72.50 (E(f22(a1),f19(a1,a12))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6681,6690,6745,63,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2])). % 72.47/72.50 cnf(6786,plain, % 72.47/72.50 (E(f19(x67861,a14),f19(x67861,a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6681,6690,6745,63,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13])). % 72.47/72.50 cnf(6787,plain, % 72.47/72.50 (E(f19(a14,x67871),f19(a2,x67871))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6681,6690,6745,63,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12])). % 72.47/72.50 cnf(6788,plain, % 72.47/72.50 (E(f15(a14),f15(a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6681,6690,6745,63,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6])). % 72.47/72.50 cnf(6789,plain, % 72.47/72.50 (~P13(f19(a1,a12))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6681,6690,6745,63,370,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23])). % 72.47/72.50 cnf(6792,plain, % 72.47/72.50 (E(f19(a2,a2),f19(a14,a14))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6673,6674,6681,6688,6690,6745,63,370,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3])). % 72.47/72.50 cnf(6795,plain, % 72.47/72.50 (~P11(f21(a14),f21(f6(x67951)))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6673,6674,6681,6688,6690,6745,6667,63,370,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100])). % 72.47/72.50 cnf(6796,plain, % 72.47/72.50 (P7(x67961,f21(x67961))), % 72.47/72.50 inference(rename_variables,[],[6667])). % 72.47/72.50 cnf(6798,plain, % 72.47/72.50 (P11(f20(a1),f19(a1,a12))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6673,6674,6681,6688,6690,6745,3796,6667,63,370,55,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30])). % 72.47/72.50 cnf(6799,plain, % 72.47/72.50 (P13(f15(f21(a2)))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6673,6674,6681,6688,6690,6745,3796,6667,285,63,370,55,59,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91])). % 72.47/72.50 cnf(6801,plain, % 72.47/72.50 (P7(f15(x68011),x68011)), % 72.47/72.50 inference(rename_variables,[],[59])). % 72.47/72.50 cnf(6803,plain, % 72.47/72.50 (~P7(f19(a1,a12),f21(a14))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6673,6674,6681,6686,6688,6690,6745,3796,6667,285,63,370,55,59,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91,24])). % 72.47/72.50 cnf(6804,plain, % 72.47/72.50 (~P10(f19(a1,a12),f8(a1),f6(f22(a1)))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6673,6674,6681,6686,6688,6690,6745,3796,6667,285,63,5330,370,55,59,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91,24,20])). % 72.47/72.50 cnf(6805,plain, % 72.47/72.50 (P7(f15(f19(a1,a12)),f22(a1))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6673,6674,6681,6686,6688,6690,6745,3796,6667,285,63,5330,370,55,59,6801,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91,24,20,25])). % 72.47/72.50 cnf(6807,plain, % 72.47/72.50 (P11(f6(a14),f21(a2))), % 72.47/72.50 inference(scs_inference,[],[6675,6721,6673,6674,6681,6686,6688,6690,6729,6745,3796,6667,261,285,63,5330,370,55,59,6801,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91,24,20,25,29])). % 72.47/72.50 cnf(6813,plain, % 72.47/72.50 (P10(f22(a1),f19(a1,f16(a1)),f16(a1))), % 72.47/72.50 inference(scs_inference,[],[45,6675,6721,6673,6674,6681,6686,6688,6690,6729,6697,6745,3796,6667,6796,261,285,63,5330,370,46,61,55,59,6801,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91,24,20,25,29,104,106])). % 72.47/72.50 cnf(6815,plain, % 72.47/72.50 (P7(f18(a1),f21(f22(a1)))), % 72.47/72.50 inference(scs_inference,[],[45,6675,6721,6673,6674,6681,6686,6688,6690,6729,6697,6701,6745,3796,6667,6796,261,285,63,5330,370,46,61,55,59,6801,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91,24,20,25,29,104,106,101])). % 72.47/72.50 cnf(6817,plain, % 72.47/72.50 (~P13(f16(a1))), % 72.47/72.50 inference(scs_inference,[],[45,6675,6721,6673,6674,6681,6686,6688,6690,6729,6697,6701,6745,3796,6667,6796,261,285,63,5330,370,46,61,55,59,6801,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91,24,20,25,29,104,106,101,95])). % 72.47/72.50 cnf(6824,plain, % 72.47/72.50 (P10(a12,f6(a12),a14)), % 72.47/72.50 inference(scs_inference,[],[45,6675,6721,6673,6674,6681,6686,6688,6690,6729,6697,6701,6745,3796,6667,6796,261,285,63,5330,370,5319,46,61,60,55,59,6801,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91,24,20,25,29,104,106,101,95,110,6233,6263,243])). % 72.47/72.50 cnf(6825,plain, % 72.47/72.50 (P10(a12,a14,f6(a12))), % 72.47/72.50 inference(scs_inference,[],[45,6675,6721,6673,6674,6681,6686,6688,6690,6729,6697,6701,6745,3796,6667,6796,261,285,63,5330,370,5319,46,61,60,55,59,6801,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91,24,20,25,29,104,106,101,95,110,6233,6263,243,245])). % 72.47/72.50 cnf(6826,plain, % 72.47/72.50 (P10(f19(a1,a12),f8(a1),f8(a1))), % 72.47/72.50 inference(scs_inference,[],[45,6675,6721,6673,6674,6681,6686,6688,6690,6729,6697,6701,6745,3796,6667,6796,261,285,63,5330,370,5319,46,61,60,55,59,6801,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91,24,20,25,29,104,106,101,95,110,6233,6263,243,245,5368])). % 72.47/72.50 cnf(6828,plain, % 72.47/72.50 (~E(f6(a14),f19(a1,a12))), % 72.51/72.50 inference(scs_inference,[],[45,6675,6721,6673,6674,6681,6686,6688,6690,6729,6697,6701,6745,3796,6667,6796,261,285,63,5330,370,5319,46,61,60,55,59,6801,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91,24,20,25,29,104,106,101,95,110,6233,6263,243,245,5368,246,181])). % 72.51/72.50 cnf(6831,plain, % 72.51/72.50 (~P10(f19(a1,a12),a12,f16(a1))+~E(f22(a1),a12)), % 72.51/72.50 inference(scs_inference,[],[45,6675,6721,6673,6674,6681,6686,6688,6690,6729,6697,6701,6745,3796,6667,6796,261,285,63,5330,370,5319,46,61,60,55,59,6801,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91,24,20,25,29,104,106,101,95,110,6233,6263,243,245,5368,246,181,93,1957])). % 72.51/72.50 cnf(6833,plain, % 72.51/72.50 (P9(f16(a1),a1)), % 72.51/72.50 inference(scs_inference,[],[45,6675,6721,6673,6674,6681,6686,6688,6690,6729,6697,6701,6745,3796,6667,6796,261,285,63,5330,370,5319,46,61,60,55,59,6801,92,66,9,83,10,8,85,6373,72,6360,16,14,11,15,4,65,5,231,7,2,13,12,6,23,99,3,100,30,91,24,20,25,29,104,106,101,95,110,6233,6263,243,245,5368,246,181,93,1957,97])). % 72.51/72.50 cnf(6837,plain, % 72.51/72.50 (P10(a7,a14,f6(a7))), % 72.51/72.50 inference(scs_inference,[],[6780,266])). % 72.51/72.50 cnf(6838,plain, % 72.51/72.50 (E(f6(x68381),a14)), % 72.51/72.50 inference(rename_variables,[],[6780])). % 72.51/72.50 cnf(6840,plain, % 72.51/72.50 (E(f6(x68401),a14)), % 72.51/72.50 inference(rename_variables,[],[6780])). % 72.51/72.50 cnf(6842,plain, % 72.51/72.50 (E(f6(x68421),a14)), % 72.51/72.50 inference(rename_variables,[],[6780])). % 72.51/72.50 cnf(6846,plain, % 72.51/72.50 (E(f6(x68461),a14)), % 72.51/72.50 inference(rename_variables,[],[6780])). % 72.51/72.50 cnf(6851,plain, % 72.51/72.50 (E(f16(f6(x68511)),f16(a14))), % 72.51/72.50 inference(scs_inference,[],[6789,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9])). % 72.51/72.50 cnf(6852,plain, % 72.51/72.50 (E(f3(f6(x68521)),f3(a14))), % 72.51/72.50 inference(scs_inference,[],[6789,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10])). % 72.51/72.50 cnf(6853,plain, % 72.51/72.50 (E(f22(f6(x68531)),f22(a14))), % 72.51/72.50 inference(scs_inference,[],[6789,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10,8])). % 72.51/72.50 cnf(6854,plain, % 72.51/72.50 (E(f17(f6(x68541)),f17(a14))), % 72.51/72.50 inference(scs_inference,[],[6789,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10,8,16])). % 72.51/72.50 cnf(6855,plain, % 72.51/72.50 (E(f15(f21(a2)),a14)), % 72.51/72.50 inference(scs_inference,[],[6789,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10,8,16,65])). % 72.51/72.50 cnf(6857,plain, % 72.51/72.50 (E(f8(f6(x68571)),f8(a14))), % 72.51/72.50 inference(scs_inference,[],[6789,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10,8,16,65,11])). % 72.51/72.50 cnf(6858,plain, % 72.51/72.50 (E(f4(f6(x68581)),f4(a14))), % 72.51/72.50 inference(scs_inference,[],[6789,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10,8,16,65,11,14])). % 72.51/72.50 cnf(6859,plain, % 72.51/72.50 (E(f18(f6(x68591)),f18(a14))), % 72.51/72.50 inference(scs_inference,[],[6789,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15])). % 72.51/72.50 cnf(6860,plain, % 72.51/72.50 (E(f20(f6(x68601)),f20(a14))), % 72.51/72.50 inference(scs_inference,[],[6789,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5])). % 72.51/72.50 cnf(6861,plain, % 72.51/72.50 (P8(f6(f22(a1)),f19(a1,a12))), % 72.51/72.50 inference(scs_inference,[],[6789,6785,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231])). % 72.51/72.50 cnf(6862,plain, % 72.51/72.50 (E(f21(f6(x68621)),f21(a14))), % 72.51/72.50 inference(scs_inference,[],[6789,6785,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7])). % 72.51/72.50 cnf(6863,plain, % 72.51/72.50 (E(f19(x68631,f6(x68632)),f19(x68631,a14))), % 72.51/72.50 inference(scs_inference,[],[6789,6785,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13])). % 72.51/72.50 cnf(6864,plain, % 72.51/72.50 (E(f19(f6(x68641),x68642),f19(a14,x68642))), % 72.51/72.50 inference(scs_inference,[],[6789,6785,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12])). % 72.51/72.50 cnf(6865,plain, % 72.51/72.50 (E(f22(a1),f16(a1))), % 72.51/72.50 inference(scs_inference,[],[6789,6785,6708,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2])). % 72.51/72.50 cnf(6866,plain, % 72.51/72.50 (E(f15(f6(x68661)),f15(a14))), % 72.51/72.50 inference(scs_inference,[],[6789,6785,6708,6803,6780,6838,6840,6842,6846,6799,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2,6])). % 72.51/72.50 cnf(6867,plain, % 72.51/72.50 (~P7(f19(a1,a12),f21(a2))), % 72.51/72.50 inference(scs_inference,[],[6789,6785,6708,6798,6803,6780,6838,6840,6842,6846,6799,50,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2,6,99])). % 72.51/72.50 cnf(6869,plain, % 72.51/72.50 (P7(f20(a1),f19(a1,a12))), % 72.51/72.50 inference(scs_inference,[],[6789,6785,6708,6798,6803,6780,6838,6840,6842,6846,6799,6667,50,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2,6,99,100])). % 72.51/72.50 cnf(6870,plain, % 72.51/72.50 (P7(x68701,f21(x68701))), % 72.51/72.50 inference(rename_variables,[],[6667])). % 72.51/72.50 cnf(6872,plain, % 72.51/72.50 (E(f16(a1),f19(a1,a12))), % 72.51/72.50 inference(scs_inference,[],[6789,6785,6708,6798,6803,6780,6838,6840,6842,6846,6799,6667,50,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2,6,99,100,3])). % 72.51/72.50 cnf(6873,plain, % 72.51/72.50 (P11(f6(f6(x68731)),f21(a2))), % 72.51/72.50 inference(scs_inference,[],[6789,6785,6708,6798,6803,6780,6838,6840,6842,6846,6784,6799,561,6667,50,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2,6,99,100,3,30])). % 72.51/72.50 cnf(6874,plain, % 72.51/72.50 (P13(f15(f21(a14)))), % 72.51/72.50 inference(scs_inference,[],[6789,6785,6708,6798,6803,6780,6838,6840,6842,6846,6784,6799,561,6667,119,50,59,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2,6,99,100,3,30,91])). % 72.51/72.50 cnf(6880,plain, % 72.51/72.50 (~P7(f16(a1),f21(a14))), % 72.51/72.50 inference(scs_inference,[],[6789,6785,6708,6691,6798,6803,6780,6838,6840,6842,6846,6784,6799,561,6686,6667,6870,119,50,59,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2,6,99,100,3,30,91,25,24])). % 72.51/72.50 cnf(6881,plain, % 72.51/72.50 (P10(f19(a1,a12),f19(a1,a12),f16(a1))), % 72.51/72.50 inference(scs_inference,[],[6789,6723,6785,6708,6691,6798,6803,6780,6838,6840,6842,6846,6784,6799,561,6686,6667,6870,119,50,59,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2,6,99,100,3,30,91,25,24,20])). % 72.51/72.50 cnf(6885,plain, % 72.51/72.50 (P7(f4(a1),f21(f22(a1)))), % 72.51/72.50 inference(scs_inference,[],[45,6789,6723,6785,6708,6699,6703,6691,6769,6798,6803,6780,6838,6840,6842,6846,6784,6799,561,6686,6667,6870,119,46,61,50,59,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2,6,99,100,3,30,91,25,24,20,29,106,101])). % 72.51/72.50 cnf(6887,plain, % 72.51/72.50 (~P13(f17(a1))), % 72.51/72.50 inference(scs_inference,[],[45,6789,6723,6785,6708,6699,6703,6691,6769,6798,6803,6780,6838,6840,6842,6846,6784,6799,561,6686,6667,6870,119,46,61,50,59,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2,6,99,100,3,30,91,25,24,20,29,106,101,95])). % 72.51/72.50 cnf(6889,plain, % 72.51/72.50 (P9(f17(a1),a1)), % 72.51/72.50 inference(scs_inference,[],[45,6789,6723,6785,6708,6699,6703,6691,6769,6798,6803,6780,6838,6840,6842,6846,6784,6799,561,6686,6667,6870,119,46,61,50,59,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2,6,99,100,3,30,91,25,24,20,29,106,101,95,97])). % 72.51/72.50 cnf(6891,plain, % 72.51/72.50 (~E(f16(a1),a2)), % 72.51/72.50 inference(scs_inference,[],[45,6789,6723,6785,6708,6699,6703,6691,6769,6798,6803,6780,6838,6840,6842,6846,6784,6799,561,6686,6667,6870,119,46,61,50,59,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2,6,99,100,3,30,91,25,24,20,29,106,101,95,97,6263])). % 72.51/72.50 cnf(6893,plain, % 72.51/72.50 (P11(a14,f21(a2))), % 72.51/72.50 inference(scs_inference,[],[45,6789,6723,6785,6708,6699,6703,6691,6769,6798,6803,6780,6838,6840,6842,6846,6784,6799,561,6686,6667,6870,119,46,61,50,59,266,271,385,66,382,72,85,9,10,8,16,65,11,14,15,5,231,7,13,12,2,6,99,100,3,30,91,25,24,20,29,106,101,95,97,6263,6233,229])). % 72.51/72.50 cnf(6910,plain, % 72.51/72.50 (E(f15(f21(a14)),a14)), % 72.51/72.50 inference(scs_inference,[],[6867,6695,6874,66,72,85,65])). % 72.51/72.50 cnf(6913,plain, % 72.51/72.50 (E(f19(a1,a12),f16(a1))), % 72.51/72.50 inference(scs_inference,[],[6678,6867,6872,6695,6874,66,72,85,65,231,2])). % 72.51/72.50 cnf(6919,plain, % 72.51/72.50 (P11(f15(f4(a1)),f4(a1))), % 72.51/72.50 inference(scs_inference,[],[6678,6867,6872,6695,6880,6874,6855,6667,142,59,66,72,85,65,231,2,181,32,100,91])). % 72.51/72.50 cnf(6920,plain, % 72.51/72.50 (P7(f15(x69201),x69201)), % 72.51/72.50 inference(rename_variables,[],[59])). % 72.51/72.50 cnf(6922,plain, % 72.51/72.50 (E(f19(a14,a14),f19(a2,a2))), % 72.51/72.50 inference(scs_inference,[],[6678,6786,6787,6867,6872,6695,6880,6874,6855,6667,142,59,66,72,85,65,231,2,181,32,100,91,3])). % 72.51/72.50 cnf(6926,plain, % 72.51/72.50 (P7(f15(f6(a14)),f6(a2))), % 72.51/72.50 inference(scs_inference,[],[6779,6678,6786,6787,6867,6872,6695,6865,6880,6874,6855,5451,6667,142,59,6920,66,72,85,65,231,2,181,32,100,91,3,30,25])). % 72.51/72.50 cnf(6929,plain, % 72.51/72.50 (P10(f16(a1),f19(a1,a12),f22(a1))), % 72.51/72.50 inference(scs_inference,[],[6779,6678,6786,6787,6867,6872,6747,6695,6865,6880,6874,6855,5451,6667,142,59,6920,66,72,85,65,231,2,181,32,100,91,3,30,25,24,20])). % 72.51/72.50 cnf(6930,plain, % 72.51/72.50 (P11(a2,f21(a2))), % 72.51/72.50 inference(scs_inference,[],[6779,6678,6786,6787,6867,6872,6747,6695,6865,6880,6893,6874,6855,5451,6667,142,6675,59,6920,66,72,85,65,231,2,181,32,100,91,3,30,25,24,20,29])). % 72.51/72.50 cnf(6931,plain, % 72.51/72.50 (P10(f22(a1),f19(a1,f22(a1)),f22(a1))), % 72.51/72.50 inference(scs_inference,[],[45,6779,6678,6786,6787,6867,6872,6747,6695,6865,6880,6750,6893,6874,6855,5451,6667,142,6675,46,61,59,6920,66,72,85,65,231,2,181,32,100,91,3,30,25,24,20,29,106])). % 72.51/72.50 cnf(6933,plain, % 72.51/72.50 (P7(f17(a1),f21(f22(a1)))), % 72.51/72.50 inference(scs_inference,[],[45,6779,6678,6786,6787,6867,6872,6747,6695,6865,6880,6750,6889,6893,6874,6855,5451,6667,142,6675,46,61,59,6920,66,72,85,65,231,2,181,32,100,91,3,30,25,24,20,29,106,101])). % 72.51/72.50 cnf(6935,plain, % 72.51/72.50 (P6(f19(a1,f4(a1)),a1)), % 72.51/72.50 inference(scs_inference,[],[45,6779,6678,6786,6787,6867,6872,6747,6695,6865,6880,6750,6889,6893,6874,6885,6855,5451,6667,142,6675,46,61,59,6920,66,72,85,65,231,2,181,32,100,91,3,30,25,24,20,29,106,101,103])). % 72.51/72.50 cnf(6937,plain, % 72.51/72.50 (P11(a14,f21(a14))), % 72.51/72.50 inference(scs_inference,[],[45,6779,6678,6786,6787,6867,6872,6747,6695,6865,6880,6750,6889,6893,6874,6885,6855,5451,6667,142,6675,46,61,59,6920,66,72,85,65,231,2,181,32,100,91,3,30,25,24,20,29,106,101,103,229])). % 72.51/72.50 cnf(6949,plain, % 72.51/72.50 (E(f19(x69491,a14),f19(x69491,f6(x69492)))), % 72.51/72.50 inference(scs_inference,[],[6730,6817,6863,72,231,2])). % 72.51/72.50 cnf(6950,plain, % 72.51/72.50 (P11(f15(f16(a1)),f16(a1))), % 72.51/72.50 inference(scs_inference,[],[6730,6817,6863,59,72,231,2,91])). % 72.51/72.50 cnf(6954,plain, % 72.51/72.50 (P7(x69541,f21(x69541))), % 72.51/72.50 inference(rename_variables,[],[6667])). % 72.51/72.50 cnf(6956,plain, % 72.51/72.50 (~P6(f15(f21(a14)),a1)), % 72.51/72.50 inference(scs_inference,[],[6730,6817,6863,6873,6910,6667,142,59,72,231,2,91,100,32])). % 72.51/72.50 cnf(6957,plain, % 72.51/72.50 (E(f15(f6(x69571)),f15(a2))), % 72.51/72.50 inference(scs_inference,[],[6730,6788,6817,6863,6866,6873,6910,6667,142,59,72,231,2,91,100,32,3])). % 72.51/72.50 cnf(6958,plain, % 72.51/72.50 (~P7(f19(a1,a12),f21(f6(x69581)))), % 72.51/72.50 inference(scs_inference,[],[6730,6788,6817,6863,6866,6873,6910,6862,6803,6667,142,59,72,231,2,91,100,32,3,25])). % 72.51/72.50 cnf(6959,plain, % 72.51/72.50 (P11(a2,f21(a14))), % 72.51/72.50 inference(scs_inference,[],[6730,6788,6817,6930,6863,6866,6873,6910,6862,6677,6803,6667,142,59,72,231,2,91,100,32,3,25,30])). % 72.51/72.50 cnf(6962,plain, % 72.51/72.50 (P10(f16(a1),f19(a1,a12),f16(a1))), % 72.51/72.50 inference(scs_inference,[],[6730,6788,6881,6913,6817,6930,6863,6866,6873,6910,6862,6677,6803,6667,6954,142,59,72,231,2,91,100,32,3,25,30,24,20])). % 72.51/72.50 cnf(6963,plain, % 72.51/72.50 (~P11(f21(a2),f21(f6(x69631)))), % 72.51/72.50 inference(scs_inference,[],[6730,6788,6881,6913,6817,6930,6863,6866,6873,6910,6795,6862,6677,6803,6667,6954,142,59,72,231,2,91,100,32,3,25,30,24,20,29])). % 72.51/72.50 cnf(6966,plain, % 72.51/72.50 (~P11(f16(a1),f15(f16(a1)))), % 72.51/72.50 inference(scs_inference,[],[6730,6788,6881,6913,6817,6930,6863,6866,6873,6910,6795,6862,6677,6803,6667,6954,142,59,72,231,2,91,100,32,3,25,30,24,20,29,85,93])). % 72.51/72.50 cnf(6976,plain, % 72.51/72.50 (E(f19(a14,x69761),f19(f6(x69762),x69761))), % 72.51/72.50 inference(scs_inference,[],[6731,6887,6864,72,231,2])). % 72.51/72.50 cnf(6980,plain, % 72.51/72.50 (E(f19(f6(x69801),a14),f19(a2,a2))), % 72.51/72.50 inference(scs_inference,[],[6731,6922,6887,6864,6963,64,72,231,2,91,3])). % 72.51/72.50 cnf(6983,plain, % 72.51/72.50 (P11(f20(a1),f16(a1))), % 72.51/72.50 inference(scs_inference,[],[6731,6922,6887,6864,6958,6963,6913,6872,6798,64,72,231,2,91,3,24,30])). % 72.51/72.50 cnf(6986,plain, % 72.51/72.50 (P10(f16(a1),f22(a1),f16(a1))), % 72.51/72.50 inference(scs_inference,[],[6731,6922,6751,6887,6864,6958,6963,6913,6872,6798,6865,64,59,72,231,2,91,3,24,30,25,20])). % 72.51/72.50 cnf(6987,plain, % 72.51/72.50 (P11(f6(a2),f21(f6(x69871)))), % 72.51/72.50 inference(scs_inference,[],[6731,6922,6751,6887,6864,6958,6963,6779,6913,547,6872,6798,6865,64,59,72,231,2,91,3,24,30,25,20,29])). % 72.51/72.50 cnf(6988,plain, % 72.51/72.50 (P7(f16(a1),f21(f22(a1)))), % 72.51/72.50 inference(scs_inference,[],[45,6731,6922,6751,6887,6864,6958,6963,6779,6833,6913,547,6872,6798,6865,64,46,61,59,72,231,2,91,3,24,30,25,20,29,101])). % 72.51/72.50 cnf(6990,plain, % 72.51/72.50 (P6(f19(a1,f17(a1)),a1)), % 72.51/72.50 inference(scs_inference,[],[45,6731,6922,6751,6887,6864,6958,6963,6933,6779,6833,6913,547,6872,6798,6865,64,46,61,59,72,231,2,91,3,24,30,25,20,29,101,103])). % 72.51/72.50 cnf(6994,plain, % 72.51/72.50 (~P11(f16(a1),f20(a1))), % 72.51/72.50 inference(scs_inference,[],[45,6731,6922,6751,6887,6864,6958,6963,6933,6779,6833,6913,547,6872,6798,6865,64,46,61,59,72,231,2,91,3,24,30,25,20,29,101,103,85,93])). % 72.51/72.50 cnf(6998,plain, % 72.51/72.50 (P10(f22(a1),f16(a1),f22(a1))), % 72.51/72.50 inference(scs_inference,[],[45,6731,6922,6751,6887,6864,6958,6963,6933,6779,6833,6913,547,6872,6798,6865,6667,64,6721,370,46,61,59,72,231,2,91,3,24,30,25,20,29,101,103,85,93,181,3973,110])). % 72.51/72.50 cnf(7006,plain, % 72.51/72.50 (E(f19(a2,a2),f19(f6(x70061),a14))), % 72.51/72.50 inference(scs_inference,[],[6732,6980,6679,72,231,2])). % 72.51/72.50 cnf(7007,plain, % 72.51/72.50 (P10(a12,a14,a14)), % 72.51/72.50 inference(scs_inference,[],[6825,6732,6980,6679,6780,72,231,2,22])). % 72.51/72.50 cnf(7008,plain, % 72.51/72.50 (E(f6(x70081),a14)), % 72.51/72.50 inference(rename_variables,[],[6780])). % 72.51/72.50 cnf(7013,plain, % 72.51/72.50 (P10(f16(a1),f16(a1),f22(a1))), % 72.51/72.50 inference(scs_inference,[],[6825,6732,6733,6929,6980,6679,6780,6913,163,57,72,231,2,22,34,35,21])). % 72.51/72.50 cnf(7016,plain, % 72.51/72.50 (E(f16(f6(x70161)),f16(a2))), % 72.51/72.50 inference(scs_inference,[],[6825,6732,6733,6764,6929,6980,6851,6679,6780,6913,163,57,5337,5132,72,231,2,22,34,35,21,91,3])). % 72.51/72.50 cnf(7018,plain, % 72.51/72.50 (P7(x70181,f21(x70181))), % 72.51/72.50 inference(rename_variables,[],[6667])). % 72.51/72.50 cnf(7019,plain, % 72.51/72.50 (P11(f15(f16(a1)),f19(a1,a12))), % 72.51/72.50 inference(scs_inference,[],[6825,6732,6733,6764,6929,6980,6851,6950,6679,6780,6913,6872,163,57,6667,5337,5132,72,231,2,22,34,35,21,91,3,24,30])). % 72.51/72.50 cnf(7021,plain, % 72.51/72.50 (P10(f19(a1,a12),f19(a1,a12),f22(a1))), % 72.51/72.50 inference(scs_inference,[],[6825,6732,6733,6764,6929,6980,6851,6950,6679,6862,6780,6913,6686,6872,163,57,6667,5337,5132,72,231,2,22,34,35,21,91,3,24,30,25,20])). % 72.51/72.50 cnf(7022,plain, % 72.51/72.50 (P11(a14,f21(f6(x70221)))), % 72.51/72.50 inference(scs_inference,[],[6825,6732,6733,6764,6929,6980,6851,6987,6950,6679,6862,6780,7008,6913,6686,6872,163,57,6667,5337,5132,72,231,2,22,34,35,21,91,3,24,30,25,20,29])). % 72.51/72.50 cnf(7024,plain, % 72.51/72.50 (E(f19(a1,f16(a1)),f22(a1))), % 72.51/72.50 inference(scs_inference,[],[45,6825,6732,6733,6764,6929,6983,6980,6851,6987,6988,6950,6679,6862,6780,7008,6817,6913,6686,6872,163,57,6667,5337,5132,48,46,61,72,231,2,22,34,35,21,91,3,24,30,25,20,29,107])). % 72.51/72.50 cnf(7030,plain, % 72.51/72.50 (~P11(f19(a1,a12),f15(f16(a1)))), % 72.51/72.50 inference(scs_inference,[],[45,6825,6732,6733,6764,6929,6983,6980,6851,6987,6988,6950,6679,6862,6780,7008,6817,6913,6686,6872,163,57,6667,5337,5132,48,46,61,72,231,2,22,34,35,21,91,3,24,30,25,20,29,107,6360,6373,85,93])). % 72.51/72.50 cnf(7038,plain, % 72.51/72.50 (~P10(f19(a1,f16(a1)),a12,f16(a1))+~E(f22(a1),a12)), % 72.51/72.50 inference(scs_inference,[],[45,6825,6732,6733,6764,6929,6983,6980,6851,6987,6988,6950,6679,6862,6780,7008,3796,6817,6913,6686,6872,163,57,6667,7018,5337,5132,48,370,46,61,72,231,2,22,34,35,21,91,3,24,30,25,20,29,107,6360,6373,85,93,3973,103,109,1957])). % 72.51/72.50 cnf(7045,plain, % 72.51/72.50 (P11(f15(f22(a5)),f22(a5))), % 72.51/72.50 inference(scs_inference,[],[6734,6852,7024,6679,64,370,59,72,231,2,23,91])). % 72.51/72.50 cnf(7046,plain, % 72.51/72.50 (P7(f15(x70461),x70461)), % 72.51/72.50 inference(rename_variables,[],[59])). % 72.51/72.50 cnf(7048,plain, % 72.51/72.50 (E(f19(a2,a2),f19(a14,f6(x70481)))), % 72.51/72.50 inference(scs_inference,[],[6734,6792,6852,7024,6949,6679,64,370,59,72,231,2,23,91,3])). % 72.51/72.50 cnf(7050,plain, % 72.51/72.50 (~P7(f19(a1,f16(a1)),f21(a2))), % 72.51/72.50 inference(scs_inference,[],[6734,6792,6852,7024,6949,6690,6679,64,370,59,72,231,2,23,91,3,24])). % 72.51/72.50 cnf(7051,plain, % 72.51/72.50 (P11(f15(f8(a1)),f19(a1,a12))), % 72.51/72.50 inference(scs_inference,[],[6734,6792,6852,7024,6949,6690,6679,5451,6785,64,370,59,72,231,2,23,91,3,24,30])). % 72.51/72.50 cnf(7054,plain, % 72.51/72.50 (P10(f19(a1,a12),f16(a1),f22(a1))), % 72.51/72.50 inference(scs_inference,[],[6734,6792,6998,6852,7024,6949,6690,6679,5451,6785,64,370,59,7046,72,231,2,23,91,3,24,30,25,20])). % 72.51/72.50 cnf(7055,plain, % 72.51/72.50 (P11(a2,f21(f6(x70551)))), % 72.51/72.50 inference(scs_inference,[],[6734,6792,6998,6852,7024,6949,7022,6690,6679,5451,6785,64,6675,370,59,7046,72,231,2,23,91,3,24,30,25,20,29])). % 72.51/72.50 cnf(7072,plain, % 72.51/72.50 (~P7(f21(a14),f21(a14))), % 72.51/72.50 inference(scs_inference,[],[6735,6937,7051,6853,5132,49,72,93,231,2,99])). % 72.51/72.50 cnf(7074,plain, % 72.51/72.50 (P9(f19(a1,a12),a1)), % 72.51/72.50 inference(scs_inference,[],[6735,6937,7051,6853,6833,6872,5132,49,72,93,231,2,99,36])). % 72.51/72.50 cnf(7075,plain, % 72.51/72.50 (~P11(f21(a14),f21(a14))), % 72.51/72.50 inference(scs_inference,[],[6735,6937,7051,6853,6833,6872,6667,5132,49,72,93,231,2,99,36,100])). % 72.51/72.50 cnf(7076,plain, % 72.51/72.50 (P7(x70761,f21(x70761))), % 72.51/72.50 inference(rename_variables,[],[6667])). % 72.51/72.50 cnf(7078,plain, % 72.51/72.50 (P6(f19(a1,a12),a1)), % 72.51/72.50 inference(scs_inference,[],[6735,6937,7051,6853,6833,6697,6872,6667,5132,49,72,93,231,2,99,36,100,32])). % 72.51/72.50 cnf(7079,plain, % 72.51/72.50 (P11(f15(f8(a5)),f8(a5))), % 72.51/72.50 inference(scs_inference,[],[6735,6937,7051,6853,6681,6833,6697,6872,6667,5132,49,59,72,93,231,2,99,36,100,32,91])). % 72.51/72.50 cnf(7082,plain, % 72.51/72.50 (E(f4(f6(x70821)),f4(a2))), % 72.51/72.50 inference(scs_inference,[],[6735,6776,6937,7051,6853,6858,6681,6833,6697,6872,6667,5132,49,59,72,93,231,2,99,36,100,32,91,3])). % 72.51/72.50 cnf(7084,plain, % 72.51/72.50 (P7(x70841,f21(x70841))), % 72.51/72.50 inference(rename_variables,[],[6667])). % 72.51/72.50 cnf(7087,plain, % 72.51/72.50 (P10(f19(a1,a12),f22(a1),f16(a1))), % 72.51/72.50 inference(scs_inference,[],[6735,6776,6937,6986,7051,6853,6858,7045,6681,6833,6697,6872,112,6667,7076,5132,49,59,72,93,231,2,99,36,100,32,91,3,24,30,20])). % 72.51/72.50 cnf(7089,plain, % 72.51/72.50 (P10(f19(a1,a12),f19(a1,a12),f19(a1,a12))), % 72.51/72.50 inference(scs_inference,[],[6735,6776,6937,6986,7051,6853,6858,7050,7045,6789,6681,6833,6784,6697,6872,112,6667,7076,7084,5132,49,59,72,93,231,2,99,36,100,32,91,3,24,30,20,25,104])). % 72.51/72.50 cnf(7105,plain, % 72.51/72.50 (~P13(f3(a7))), % 72.51/72.50 inference(scs_inference,[],[63,72])). % 72.51/72.50 cnf(7111,plain, % 72.51/72.50 (P7(f15(f8(a5)),f22(a5))), % 72.51/72.50 inference(scs_inference,[],[6736,6854,7079,6683,63,72,93,231,2,100])). % 72.51/72.50 cnf(7114,plain, % 72.51/72.50 (E(f17(f6(x71141)),f17(a2))), % 72.51/72.50 inference(scs_inference,[],[6736,6775,7078,6854,7079,6683,6956,63,72,93,231,2,100,32,3])). % 72.51/72.50 cnf(7116,plain, % 72.51/72.50 (P11(f15(f16(a1)),f22(a1))), % 72.51/72.50 inference(scs_inference,[],[6736,6775,7078,7072,6854,7079,6683,6956,7019,6677,63,6721,72,93,231,2,100,32,3,24,30])). % 72.51/72.50 cnf(7120,plain, % 72.51/72.50 (P10(f16(a1),f19(a1,f16(a1)),f16(a1))), % 72.51/72.50 inference(scs_inference,[],[6736,6775,7075,7078,7072,6813,6854,7079,6683,6956,7019,6677,6865,63,6721,59,72,93,231,2,100,32,3,24,30,29,25,20])). % 72.51/72.50 cnf(7123,plain, % 72.51/72.50 (P7(f19(a1,a12),f21(f22(a1)))), % 72.51/72.50 inference(scs_inference,[],[45,6736,6775,7075,7078,7072,7074,6813,6854,7079,6683,6956,7019,6677,6865,63,6721,46,61,59,72,93,231,2,100,32,3,24,30,29,25,20,106,101])). % 72.51/72.50 cnf(7127,plain, % 72.51/72.50 (P10(f22(a1),f16(a1),f19(a1,a12))), % 72.51/72.50 inference(scs_inference,[],[45,6736,6775,7075,7078,7072,7074,6813,6854,7079,6683,6956,6935,7019,6723,6988,6677,6865,63,6721,370,46,61,59,72,93,231,2,100,32,3,24,30,29,25,20,106,101,97,110])). % 72.51/72.50 cnf(7137,plain, % 72.51/72.50 (E(f8(a14),f8(f6(x71371)))), % 72.51/72.50 inference(scs_inference,[],[6740,7105,6857,7116,72,93,231,2])). % 72.51/72.50 cnf(7140,plain, % 72.51/72.50 (E(f18(f6(x71401)),f18(a2))), % 72.51/72.50 inference(scs_inference,[],[6740,6778,7105,6857,6859,7116,6667,72,93,231,2,24,3])). % 72.51/72.50 cnf(7147,plain, % 72.51/72.50 (~P10(f22(a1),a12,f6(f22(a1)))), % 72.51/72.50 inference(scs_inference,[],[6740,6778,7089,7105,6857,6859,7116,6710,6919,221,6913,165,6667,370,60,59,72,93,231,2,24,3,20,30,33,25,108])). % 72.51/72.50 cnf(7158,plain, % 72.51/72.50 (E(f20(f6(x71581)),f20(a2))), % 72.51/72.50 inference(scs_inference,[],[6782,6860,7072,6862,370,72,231,2,24,3])). % 72.51/72.50 cnf(7160,plain, % 72.51/72.50 (~P10(f22(a1),f6(f22(a1)),a12)), % 72.51/72.50 inference(scs_inference,[],[6782,7127,6860,7147,6710,7072,6862,6865,370,60,72,231,2,24,3,20,110])). % 72.51/72.50 cnf(7165,plain, % 72.51/72.50 (~P10(f22(a1),a12,x71651)+~E(x71651,f6(f22(a1)))), % 72.51/72.50 inference(scs_inference,[],[6782,7127,6860,7147,6710,7072,6862,6865,370,60,72,231,2,24,3,20,110,85,22])). % 72.51/72.50 cnf(7173,plain, % 72.51/72.50 (E(f15(a2),f15(f6(x71731)))), % 72.51/72.50 inference(scs_inference,[],[6767,6957,231,2])). % 72.51/72.50 cnf(7176,plain, % 72.51/72.50 (P10(a7,a14,a14)), % 72.51/72.50 inference(scs_inference,[],[6837,6767,6777,6957,6780,57,231,2,34,22])). % 72.51/72.50 cnf(7178,plain, % 72.51/72.50 (P8(f6(f19(a2,a14)),f19(a2,a2))), % 72.51/72.50 inference(scs_inference,[],[6837,6767,6777,6752,6957,6922,6780,57,231,2,34,22,35])). % 72.51/72.50 cnf(7181,plain, % 72.51/72.50 (P7(a2,f21(a14))), % 72.51/72.50 inference(scs_inference,[],[6837,6767,6777,7087,6752,6957,6959,6922,6780,6865,57,6667,231,2,34,22,35,21,100])). % 72.51/72.50 cnf(7182,plain, % 72.51/72.50 (P7(x71821,f21(x71821))), % 72.51/72.50 inference(rename_variables,[],[6667])). % 72.51/72.50 cnf(7186,plain, % 72.51/72.50 (E(f3(f6(x71861)),f3(a2))), % 72.51/72.50 inference(scs_inference,[],[6837,6767,6777,7087,6752,6957,6959,6922,6852,6780,6865,57,6667,7182,231,2,34,22,35,21,100,24,3])). % 72.51/72.50 cnf(7194,plain, % 72.51/72.50 (E(f19(a14,a2),f19(f6(x71941),a14))), % 72.51/72.50 inference(scs_inference,[],[6768,7016,6976,6674,231,2,3])). % 72.51/72.50 cnf(7208,plain, % 72.51/72.50 (E(f4(a2),f4(f6(x72081)))), % 72.51/72.50 inference(scs_inference,[],[7082,6775,231,2])). % 72.51/72.50 cnf(7215,plain, % 72.51/72.50 (E(f19(a2,a14),f19(f6(x72151),a14))), % 72.51/72.50 inference(scs_inference,[],[7082,7006,6807,6775,6786,6784,6667,50,231,2,99,100,24,3])). % 72.51/72.50 cnf(7217,plain, % 72.51/72.50 (P10(f22(a1),f18(a1),f18(a1))), % 72.51/72.50 inference(scs_inference,[],[7082,7006,6815,6807,6775,6786,6784,6667,370,50,231,2,99,100,24,3,104])). % 72.51/72.50 cnf(7219,plain, % 72.51/72.50 (~P11(f21(a14),f21(a2))), % 72.51/72.50 inference(scs_inference,[],[7082,7006,6815,6807,6775,6786,6784,6667,370,50,231,2,99,100,24,3,104,85])). % 72.51/72.50 cnf(7222,plain, % 72.51/72.50 (P11(f15(f3(a7)),f3(a7))), % 72.51/72.50 inference(scs_inference,[],[7082,7006,6815,6807,6775,6786,7105,6784,6667,370,50,59,231,2,99,100,24,3,104,85,31,91])). % 72.51/72.50 cnf(7233,plain, % 72.51/72.50 (P7(f15(f3(a7)),a7)), % 72.51/72.50 inference(scs_inference,[],[7114,7222,6778,6765,93,231,2,100])). % 72.51/72.50 cnf(7238,plain, % 72.51/72.50 (E(f19(a2,a2),f19(a2,f6(x72381)))), % 72.51/72.50 inference(scs_inference,[],[7219,7114,7222,7048,6778,6776,6765,6787,6862,6667,93,231,2,100,29,24,3])). % 72.51/72.50 cnf(7252,plain, % 72.51/72.50 (P11(f15(f8(a5)),f22(a5))), % 72.51/72.50 inference(scs_inference,[],[7140,7111,6764,6679,231,2,91])). % 72.51/72.50 cnf(7254,plain, % 72.51/72.50 (~E(f22(a5),f6(x72541))), % 72.51/72.50 inference(scs_inference,[],[7140,7111,6764,7045,6679,194,231,2,91,30])). % 72.51/72.50 cnf(7258,plain, % 72.51/72.50 (E(f8(a2),f8(f6(x72581)))), % 72.51/72.50 inference(scs_inference,[],[7140,7111,7137,6733,6764,7045,6679,194,59,231,2,91,30,25,3])). % 72.51/72.50 cnf(7271,plain, % 72.51/72.50 (E(f15(a14),f15(f6(x72711)))), % 72.51/72.50 inference(scs_inference,[],[7158,7173,6788,231,2,3])). % 72.51/72.50 cnf(7279,plain, % 72.51/72.50 (P8(f3(a2),f3(f6(x72791)))), % 72.51/72.50 inference(scs_inference,[],[7186,6792,57,231,2,34])). % 72.51/72.50 cnf(7283,plain, % 72.51/72.50 (P10(f16(a1),f22(a1),f22(a1))), % 72.51/72.50 inference(scs_inference,[],[7013,7178,7186,6792,6673,57,6708,231,2,34,35,21])). % 72.51/72.50 cnf(7284,plain, % 72.51/72.50 (P10(f19(a1,a12),f18(a1),f18(a1))), % 72.51/72.50 inference(scs_inference,[],[7013,7217,7178,7186,6792,6673,6785,57,6708,231,2,34,35,21,20])). % 72.51/72.50 cnf(7286,plain, % 72.51/72.50 (~P10(a12,f3(a12),f6(a12))), % 72.51/72.50 inference(scs_inference,[],[7013,7217,7178,7186,7208,6792,6673,6776,422,6785,57,6708,472,146,60,231,2,34,35,21,20,3,108])). % 72.51/72.50 cnf(7288,plain, % 72.51/72.50 (P7(f6(x72881),f21(x72881))), % 72.51/72.50 inference(rename_variables,[],[60])). % 72.51/72.50 cnf(7291,plain, % 72.51/72.50 (~P10(a12,f6(a12),f3(a12))), % 72.51/72.50 inference(scs_inference,[],[7013,7217,7178,7186,7208,6792,6673,6776,422,6785,57,6708,472,146,60,7288,231,2,34,35,21,20,3,108,31,110])). % 72.51/72.50 cnf(7298,plain, % 72.51/72.50 (E(f19(a2,f6(x72981)),f19(a2,a2))), % 72.51/72.50 inference(scs_inference,[],[7238,6777,231,2])). % 72.51/72.50 cnf(7299,plain, % 72.51/72.50 (P10(f19(a1,a12),f16(a1),f19(a1,a12))), % 72.51/72.50 inference(scs_inference,[],[7054,7238,6777,6785,231,2,22])). % 72.51/72.50 cnf(7300,plain, % 72.51/72.50 (E(f15(f21(a2)),a2)), % 72.51/72.50 inference(scs_inference,[],[7054,7238,6855,6777,6785,6675,231,2,22,3])). % 72.51/72.50 cnf(7301,plain, % 72.51/72.50 (~P10(f3(a12),x73011,f3(a12))+~E(x73011,f6(f3(a12)))), % 72.51/72.50 inference(scs_inference,[],[7054,7238,6718,6855,6777,6785,6675,231,2,22,3,21])). % 72.51/72.50 cnf(7302,plain, % 72.51/72.50 (~P10(f22(a5),f22(a5),f6(f22(a5)))), % 72.51/72.50 inference(scs_inference,[],[7054,7254,7238,6718,6855,6777,6679,6785,6667,6675,60,231,2,22,3,21,108])). % 72.51/72.50 cnf(7311,plain, % 72.51/72.50 (E(f19(f6(x73111),a14),f19(a2,a14))), % 72.51/72.50 inference(scs_inference,[],[7215,6922,231,2])). % 72.51/72.50 cnf(7312,plain, % 72.51/72.50 (~P7(f22(a5),f21(a14))), % 72.51/72.50 inference(scs_inference,[],[7215,7252,6922,49,231,2,99])). % 72.51/72.50 cnf(7314,plain, % 72.51/72.50 (P10(a12,a2,a14)), % 72.51/72.50 inference(scs_inference,[],[7007,7215,7252,6922,6675,49,231,2,99,21])). % 72.51/72.50 cnf(7315,plain, % 72.51/72.50 (P7(a2,f21(f6(x73151)))), % 72.51/72.50 inference(scs_inference,[],[7007,7215,7252,7055,6922,6667,6675,49,231,2,99,21,100])). % 72.51/72.50 cnf(7318,plain, % 72.51/72.50 (~P7(f22(a5),f21(f6(x73181)))), % 72.51/72.50 inference(scs_inference,[],[7007,7215,7252,7055,6922,6862,6667,6675,49,231,2,99,21,100,25])). % 72.51/72.50 cnf(7319,plain, % 72.51/72.50 (P7(f15(f6(x73191)),a2)), % 72.51/72.50 inference(scs_inference,[],[7007,6748,7215,7271,7252,7055,6922,6862,6667,6675,49,231,2,99,21,100,25,24])). % 72.51/72.50 cnf(7332,plain, % 72.51/72.50 (E(f8(f6(x73321)),f8(a2))), % 72.51/72.50 inference(scs_inference,[],[7258,7318,6674,85,181,231,2])). % 72.51/72.50 cnf(7333,plain, % 72.51/72.50 (P7(f15(f6(x73331)),a14)), % 72.51/72.50 inference(scs_inference,[],[7258,7318,7319,6671,6674,85,181,231,2,25])). % 72.51/72.50 cnf(7335,plain, % 72.51/72.50 (E(f19(a14,a2),f19(a2,a14))), % 72.51/72.50 inference(scs_inference,[],[6725,7312,7311,7258,7318,7194,7319,6671,6674,85,181,231,2,25,24,3])). % 72.51/72.50 cnf(7341,plain, % 72.51/72.50 (P6(f19(a1,f19(a1,a12)),a1)), % 72.51/72.50 inference(scs_inference,[],[45,6725,7312,7311,7258,7318,7194,7319,6671,6683,6990,7123,6674,6789,6679,46,61,85,181,231,2,25,24,3,104,97,103])). % 72.51/72.50 cnf(7344,plain, % 72.51/72.50 (P11(f15(f17(a1)),f17(a1))), % 72.51/72.50 inference(scs_inference,[],[45,6725,7312,7311,7258,7318,7194,7319,6671,6683,6990,7123,6674,6789,6887,6679,46,61,59,85,181,231,2,25,24,3,104,97,103,31,91])). % 72.51/72.50 cnf(7358,plain, % 72.51/72.50 (E(f19(a2,a14),f19(a14,a2))), % 72.51/72.50 inference(scs_inference,[],[7335,7344,93,231,2])). % 72.51/72.50 cnf(7361,plain, % 72.51/72.50 (~P7(f22(a5),f21(a2))), % 72.51/72.50 inference(scs_inference,[],[7335,7344,7312,6677,165,93,231,2,30,25])). % 72.51/72.50 cnf(7364,plain, % 72.51/72.50 (E(f22(f6(x73641)),f22(a2))), % 72.51/72.50 inference(scs_inference,[],[7335,7344,6768,6853,7312,6677,165,6667,93,231,2,30,25,24,3])). % 72.51/72.50 cnf(7380,plain, % 72.51/72.50 (P10(a7,a14,a2)), % 72.51/72.50 inference(scs_inference,[],[7176,7364,6786,6675,231,2,22])). % 72.51/72.50 cnf(7385,plain, % 72.51/72.50 (E(f19(a2,a14),f19(f6(x73851),a2))), % 72.51/72.50 inference(scs_inference,[],[7176,7358,7364,7315,6976,6786,7318,6675,59,231,2,22,25,24,3])). % 72.51/72.50 cnf(7392,plain, % 72.51/72.50 (E(f19(f6(x73921),a2),f19(a2,a14))), % 72.51/72.50 inference(scs_inference,[],[7385,6787,231,2])). % 72.51/72.50 cnf(7400,plain, % 72.51/72.50 (E(f19(f6(x74001),f6(x74002)),f19(a2,a2))), % 72.51/72.50 inference(scs_inference,[],[7284,7332,7385,7279,6678,6863,6980,6787,6852,6913,57,6667,231,2,34,35,20,24,3])). % 72.51/72.50 cnf(7405,plain, % 72.51/72.50 (~P13(f19(a1,f19(a1,a12)))), % 72.51/72.50 inference(scs_inference,[],[45,7284,7332,7385,7279,6678,6863,6980,7341,6787,6852,6913,57,6667,46,61,231,2,34,35,20,24,3,92,31,95])). % 72.51/72.50 cnf(7411,plain, % 72.51/72.50 (E(f15(f21(a14)),a2)), % 72.51/72.50 inference(scs_inference,[],[7400,6910,6776,6675,231,2,3])). % 72.51/72.50 cnf(7418,plain, % 72.51/72.50 (E(a2,f15(f21(a14)))), % 72.51/72.50 inference(scs_inference,[],[7411,6784,231,2])). % 72.51/72.50 cnf(7419,plain, % 72.51/72.50 (P7(a14,f21(a2))), % 72.51/72.50 inference(scs_inference,[],[7411,6893,6784,6667,231,2,100])). % 72.51/72.50 cnf(7422,plain, % 72.51/72.50 (P11(f15(f21(a14)),f21(a2))), % 72.51/72.50 inference(scs_inference,[],[7411,6893,6930,6784,6667,231,2,100,29])). % 72.51/72.50 cnf(7425,plain, % 72.51/72.50 (P10(f19(a1,a12),f22(a1),f22(a1))), % 72.51/72.50 inference(scs_inference,[],[7283,7411,6893,6930,6735,6784,6872,6667,59,231,2,100,29,25,20])). % 72.51/72.50 cnf(7428,plain, % 72.51/72.50 (P10(a12,a2,a2)), % 72.51/72.50 inference(scs_inference,[],[7314,6891,7283,7392,7411,6893,6930,7300,6735,6784,6872,6667,6675,59,231,2,100,29,25,20,3,33,22])). % 72.51/72.50 cnf(7432,plain, % 72.51/72.50 (P11(f15(f3(a7)),a7)), % 72.51/72.50 inference(scs_inference,[],[7233,7418,6851,63,231,2,91])). % 72.51/72.50 cnf(7444,plain, % 72.51/72.50 (E(f19(a14,f6(x74441)),f19(a2,a2))), % 72.51/72.50 inference(scs_inference,[],[7048,6677,231,2])). % 72.51/72.50 cnf(7453,plain, % 72.51/72.50 (~P7(a7,f21(f6(x74531)))), % 72.51/72.50 inference(scs_inference,[],[7428,7432,7048,7418,6919,112,6862,6677,6667,49,231,2,99,100,21,30,25])). % 72.51/72.50 cnf(7454,plain, % 72.51/72.50 (E(f19(f6(x74541),a14),f19(a14,a2))), % 72.51/72.50 inference(scs_inference,[],[7428,7432,7311,7048,7418,6919,7358,112,6862,6677,6667,49,231,2,99,100,21,30,25,3])). % 72.51/72.50 cnf(7455,plain, % 72.51/72.50 (P10(f22(a1),f4(a1),f4(a1))), % 72.51/72.50 inference(scs_inference,[],[7428,7432,7311,6885,7048,7418,6919,7358,112,6862,6677,6667,370,49,231,2,99,100,21,30,25,3,104])). % 72.51/72.50 cnf(7479,plain, % 72.51/72.50 (E(a2,f15(f21(a2)))), % 72.51/72.50 inference(scs_inference,[],[7300,6865,231,2])). % 72.51/72.50 cnf(7483,plain, % 72.51/72.50 (P11(f15(f19(a1,a12)),f22(a1))), % 72.51/72.50 inference(scs_inference,[],[6805,7422,7300,6865,6667,370,231,2,100,91])). % 72.51/72.50 cnf(7487,plain, % 72.51/72.50 (E(f19(f6(x74871),f6(x74872)),f19(a14,a2))), % 72.51/72.50 inference(scs_inference,[],[7454,6805,7422,6730,6863,7300,6865,6667,370,59,231,2,100,91,25,3])). % 72.51/72.50 cnf(7501,plain, % 72.51/72.50 (P8(f19(a14,a2),f19(f6(x75011),f6(x75012)))), % 72.51/72.50 inference(scs_inference,[],[7487,7479,57,231,2,34])). % 72.51/72.50 cnf(7505,plain, % 72.51/72.50 (P11(f15(f19(a1,a12)),f19(a1,a12))), % 72.51/72.50 inference(scs_inference,[],[7487,7483,7479,6745,6959,6785,57,231,2,34,35,29,30])). % 72.51/72.50 cnf(7508,plain, % 72.51/72.50 (P7(x75081,f21(x75081))), % 72.51/72.50 inference(rename_variables,[],[6667])). % 72.51/72.50 cnf(7509,plain, % 72.51/72.50 (E(f19(a14,f6(x75091)),f19(a14,a2))), % 72.51/72.51 inference(scs_inference,[],[7181,7487,7444,7483,7479,7453,6745,6959,6673,6785,57,6667,231,2,34,35,29,30,24,25,3])). % 72.51/72.51 cnf(7511,plain, % 72.51/72.51 (E(f19(a1,f22(a1)),f22(a1))), % 72.51/72.51 inference(scs_inference,[],[45,7181,7487,7444,7483,7479,7453,6745,6959,6673,3796,6785,57,48,6667,7508,370,46,61,231,2,34,35,29,30,24,25,3,107])). % 72.51/72.51 cnf(7516,plain, % 72.51/72.51 (~P11(f19(a1,a12),f15(f19(a1,a12)))), % 72.51/72.51 inference(scs_inference,[],[45,7181,7487,7444,7483,7479,7453,6745,6959,6673,3796,6785,57,48,6667,7508,370,46,61,231,2,34,35,29,30,24,25,3,107,6360,6373,93])). % 72.51/72.51 cnf(7519,plain, % 72.51/72.51 (~P10(f19(a1,f22(a1)),a12,f16(a1))+~E(f22(a1),a12)), % 72.51/72.51 inference(scs_inference,[],[45,7181,7487,7444,7483,7479,7453,6745,6959,6673,3796,6785,57,48,6667,7508,370,46,61,231,2,34,35,29,30,24,25,3,107,6360,6373,93,3973,1957])). % 72.51/72.51 cnf(7523,plain, % 72.51/72.51 (~P13(f19(a1,f22(a1)))), % 72.51/72.51 inference(scs_inference,[],[7509,7511,6913,370,231,2,23])). % 72.51/72.51 cnf(7524,plain, % 72.51/72.51 (P11(f15(f19(a1,a12)),f16(a1))), % 72.51/72.51 inference(scs_inference,[],[7505,7509,7511,6913,370,231,2,23,30])). % 72.51/72.51 cnf(7525,plain, % 72.51/72.51 (~P7(f19(a1,f22(a1)),f21(a2))), % 72.51/72.51 inference(scs_inference,[],[7505,7509,7511,6690,6913,370,231,2,23,30,24])). % 72.51/72.51 cnf(7528,plain, % 72.51/72.51 (E(f19(a1,f22(a1)),f19(a1,a12))), % 72.51/72.51 inference(scs_inference,[],[7505,7509,7511,6678,6690,6913,6785,370,59,231,2,23,30,24,25,3])). % 72.51/72.51 cnf(7536,plain, % 72.51/72.51 (P10(f19(a1,a12),f4(a1),f4(a1))), % 72.51/72.51 inference(scs_inference,[],[6994,7455,7505,7509,7511,6678,6690,6913,6785,370,59,231,2,23,30,24,25,3,85,93,181,91,20])). % 72.51/72.51 cnf(7552,plain, % 72.51/72.51 (E(f19(a1,a12),f19(a1,f22(a1)))), % 72.51/72.51 inference(scs_inference,[],[7528,6872,231,2])). % 72.51/72.51 cnf(7555,plain, % 72.51/72.51 (P11(f15(f3(a12)),f22(a1))), % 72.51/72.51 inference(scs_inference,[],[7528,6743,7074,7078,6872,370,231,2,36,32,91])). % 72.51/72.51 cnf(7558,plain, % 72.51/72.51 (P10(f16(a1),f19(a1,f22(a1)),f22(a1))), % 72.51/72.51 inference(scs_inference,[],[7380,6931,7528,6743,7074,7078,7418,6865,6872,370,231,2,36,32,91,22,20])). % 72.51/72.51 cnf(7559,plain, % 72.51/72.51 (P7(f15(a14),f6(a2))), % 72.51/72.51 inference(scs_inference,[],[7380,6931,7528,6743,6926,6866,7074,7078,7418,6865,6872,370,231,2,36,32,91,22,20,24])). % 72.51/72.51 cnf(7562,plain, % 72.51/72.51 (E(f19(a2,f6(x75621)),f19(a14,a14))), % 72.51/72.51 inference(scs_inference,[],[7380,6931,7528,7525,6743,6926,7298,6866,7074,7078,6792,7418,6784,6865,6872,370,231,2,36,32,91,22,20,24,25,3])). % 72.51/72.51 cnf(7574,plain, % 72.51/72.51 (P11(f15(f3(a12)),f16(a1))), % 72.51/72.51 inference(scs_inference,[],[7562,7555,6865,6708,231,2,30])). % 72.51/72.51 cnf(7576,plain, % 72.51/72.51 (P7(f20(a1),f19(a1,f22(a1)))), % 72.51/72.51 inference(scs_inference,[],[7299,6869,7562,7555,7552,6865,6708,231,2,30,20,25])). % 72.51/72.51 cnf(7577,plain, % 72.51/72.51 (E(f19(a14,a2),f19(a2,f6(x75771)))), % 72.51/72.51 inference(scs_inference,[],[7299,6869,7562,7555,7552,6949,7335,6865,6708,231,2,30,20,25,3])). % 72.51/72.51 cnf(7579,plain, % 72.51/72.51 (~P10(f22(a5),f6(f22(a5)),f22(a5))), % 72.51/72.51 inference(scs_inference,[],[7299,6869,7562,7555,7552,7302,6949,7335,6679,6865,6708,6667,60,231,2,30,20,25,3,110])). % 72.51/72.51 cnf(7587,plain, % 72.51/72.51 (E(f19(a1,f19(a1,a12)),f22(a1))), % 72.51/72.51 inference(scs_inference,[],[45,7299,6869,7562,7555,6966,7552,7302,6949,7335,7123,6789,6798,6679,6865,6708,48,6667,46,61,60,231,2,30,20,25,3,110,93,91,107])). % 72.51/72.51 cnf(7598,plain, % 72.51/72.51 (E(f22(a1),f19(a1,f19(a1,a12)))), % 72.51/72.51 inference(scs_inference,[],[7587,6373,6360,2])). % 72.51/72.51 cnf(7600,plain, % 72.51/72.51 (P7(x76001,f21(x76001))), % 72.51/72.51 inference(rename_variables,[],[6667])). % 72.51/72.51 cnf(7604,plain, % 72.51/72.51 (P11(f15(f3(a12)),f19(a1,a12))), % 72.51/72.51 inference(scs_inference,[],[7587,7574,7523,7576,7116,6872,6667,6373,6360,2,100,91,30])). % 72.51/72.51 cnf(7605,plain, % 72.51/72.51 (~P7(f19(a1,f19(a1,a12)),f21(a14))), % 72.51/72.51 inference(scs_inference,[],[7587,7574,7523,7576,7116,6686,6872,6667,6373,6360,2,100,91,30,24])). % 72.51/72.51 cnf(7606,plain, % 72.51/72.51 (P10(f19(a1,f22(a1)),f19(a1,a12),f22(a1))), % 72.51/72.51 inference(scs_inference,[],[7021,7587,7574,7523,7576,7116,7552,6686,6872,6667,6373,6360,2,100,91,30,24,20])). % 72.51/72.51 cnf(7607,plain, % 72.51/72.51 (E(f19(a14,f6(x76071)),f19(a2,a14))), % 72.51/72.51 inference(scs_inference,[],[7021,7587,7574,7523,7576,7444,7116,7552,6674,6686,6872,6667,6373,6360,2,100,91,30,24,20,3])). % 72.51/72.51 cnf(7616,plain, % 72.51/72.51 (~P11(f19(a1,f19(a1,a12)),f21(a14))), % 72.51/72.51 inference(scs_inference,[],[7021,7587,7574,7579,7523,7576,7444,7116,7552,6674,6686,6679,6872,6667,7600,60,6373,6360,2,100,91,30,24,20,3,105,6263,6233,5368,85])). % 72.51/72.51 cnf(7627,plain, % 72.51/72.51 (P7(f15(a2),a14)), % 72.51/72.51 inference(scs_inference,[],[7604,7607,7333,6957,93,2,24])). % 72.51/72.51 cnf(7630,plain, % 72.51/72.51 (E(f19(f6(x76301),f6(x76302)),f19(a2,a14))), % 72.51/72.51 inference(scs_inference,[],[7425,7604,7607,7333,6957,6864,7552,93,2,24,20,3])). % 72.51/72.51 cnf(7632,plain, % 72.51/72.51 (P10(f22(a1),f17(a1),f17(a1))), % 72.51/72.51 inference(scs_inference,[],[7425,7604,7607,7333,6933,6957,6864,7552,370,93,2,24,20,3,104])). % 72.51/72.51 cnf(7645,plain, % 72.51/72.51 (E(f19(f6(x76451),f6(x76452)),f19(a14,a14))), % 72.51/72.51 inference(scs_inference,[],[7632,7630,7606,7501,7598,7400,6792,57,6785,2,34,35,22,20,3])). % 72.51/72.51 cnf(7646,plain, % 72.51/72.51 (P10(f3(a12),f3(a12),f3(a12))), % 72.51/72.51 inference(scs_inference,[],[7632,7630,7606,7501,7598,7400,6792,418,57,6785,6667,2,34,35,22,20,3,104])). % 72.51/72.51 cnf(7667,plain, % 72.51/72.51 (E(f19(a14,a14),f19(f6(x76671),f6(x76672)))), % 72.51/72.51 inference(scs_inference,[],[7645,2])). % 72.51/72.51 cnf(7669,plain, % 72.51/72.51 (E(f6(x76691),a2)), % 72.51/72.51 inference(scs_inference,[],[7536,7645,7552,6780,6675,2,20,3])). % 72.51/72.51 cnf(7670,plain, % 72.51/72.51 (P10(a7,a2,f6(a7))), % 72.51/72.51 inference(scs_inference,[],[7536,7645,7552,6780,6675,2,20,3,266])). % 72.51/72.51 cnf(7673,plain, % 72.51/72.51 (E(f21(f6(a7)),f21(a2))), % 72.51/72.51 inference(scs_inference,[],[7536,7645,7552,6780,6675,2,20,3,266,271,4,7])). % 72.51/72.51 cnf(7685,plain, % 72.51/72.51 (P10(a12,f6(a12),a2)), % 72.51/72.51 inference(scs_inference,[],[7669,7673,592,243])). % 72.51/72.51 cnf(7686,plain, % 72.51/72.51 (E(f6(x76861),a2)), % 72.51/72.51 inference(rename_variables,[],[7669])). % 72.51/72.51 cnf(7687,plain, % 72.51/72.51 (P10(a12,a2,f6(a12))), % 72.51/72.51 inference(scs_inference,[],[7669,7686,7673,592,243,245])). % 72.51/72.51 cnf(7688,plain, % 72.51/72.51 (E(f6(x76881),a2)), % 72.51/72.51 inference(rename_variables,[],[7669])). % 72.51/72.51 cnf(7690,plain, % 72.51/72.51 (E(f6(x76901),a2)), % 72.51/72.51 inference(rename_variables,[],[7669])). % 72.51/72.51 cnf(7692,plain, % 72.51/72.51 (E(f6(x76921),a2)), % 72.51/72.51 inference(rename_variables,[],[7669])). % 72.51/72.51 cnf(7696,plain, % 72.51/72.51 (E(f19(x76961,f6(x76962)),f19(x76961,a2))), % 72.51/72.51 inference(scs_inference,[],[7669,7686,7688,7690,7692,7673,592,243,245,385,382,4,7,12,13])). % 72.51/72.51 cnf(7697,plain, % 72.51/72.51 (E(a2,f6(x76971))), % 72.51/72.51 inference(scs_inference,[],[7669,7686,7688,7690,7692,7673,592,243,245,385,382,4,7,12,13,2])). % 72.51/72.51 cnf(7699,plain, % 72.51/72.51 (~P10(f19(a1,a12),f8(a1),a2)), % 72.51/72.51 inference(scs_inference,[],[7669,7686,7688,7690,7692,7670,7673,6804,7479,592,243,245,385,382,4,7,12,13,2,21,22])). % 72.51/72.51 cnf(7700,plain, % 72.51/72.51 (P11(a2,f21(f22(a1)))), % 72.51/72.51 inference(scs_inference,[],[7669,7686,7688,7690,7692,7670,7673,6804,261,7479,592,243,245,385,382,4,7,12,13,2,21,22,29])). % 72.51/72.51 cnf(7705,plain, % 72.51/72.51 (P7(f15(a14),f6(a14))), % 72.51/72.51 inference(scs_inference,[],[7559,7669,7686,7688,7690,7692,7670,7673,6804,6729,7344,261,7479,194,592,243,245,385,382,4,7,12,13,2,21,22,29,30,25])). % 72.51/72.51 cnf(7708,plain, % 72.51/72.51 (~P10(f22(a1),a12,a2)), % 72.51/72.51 inference(scs_inference,[],[7559,7669,7686,7688,7690,7692,7670,7673,6826,6804,6155,6729,7344,7024,261,7479,7552,194,592,243,245,385,382,4,7,12,13,2,21,22,29,30,25,20,3,7165])). % 72.51/72.51 cnf(7714,plain, % 72.51/72.51 (~P10(f3(a12),a2,f3(a12))), % 72.51/72.51 inference(scs_inference,[],[7697,7301])). % 72.51/72.51 cnf(7715,plain, % 72.51/72.51 (E(a2,f6(x77151))), % 72.51/72.51 inference(rename_variables,[],[7697])). % 72.51/72.51 cnf(7719,plain, % 72.51/72.51 (E(f21(a2),f21(f6(x77191)))), % 72.51/72.51 inference(scs_inference,[],[7697,7715,7301,529,4,7])). % 72.51/72.51 cnf(7720,plain, % 72.51/72.51 (E(f19(a2,x77201),f19(f6(x77202),x77201))), % 72.51/72.51 inference(scs_inference,[],[7697,7715,7301,529,4,7,12])). % 72.51/72.51 cnf(7721,plain, % 72.51/72.51 (E(f19(x77211,a2),f19(x77211,f6(x77212)))), % 72.51/72.51 inference(scs_inference,[],[7697,7715,7301,529,4,7,12,13])). % 72.51/72.51 cnf(7724,plain, % 72.51/72.51 (~P7(f21(f22(a1)),f21(a14))), % 72.51/72.51 inference(scs_inference,[],[7697,7715,7577,7700,49,7301,529,4,7,12,13,231,2,99])). % 72.51/72.51 cnf(7730,plain, % 72.51/72.51 (E(a2,f6(x77301))), % 72.51/72.51 inference(rename_variables,[],[7697])). % 72.51/72.51 cnf(7732,plain, % 72.51/72.51 (E(a2,f6(x77321))), % 72.51/72.51 inference(rename_variables,[],[7697])). % 72.51/72.51 cnf(7733,plain, % 72.51/72.51 (P11(f6(x77331),f21(f22(a1)))), % 72.51/72.51 inference(scs_inference,[],[7697,7715,7730,7732,7577,7700,7160,7286,6667,49,7301,529,4,7,12,13,231,2,99,100,21,22,29])). % 72.51/72.51 cnf(7736,plain, % 72.51/72.51 (P10(f19(a1,a12),f19(a1,f16(a1)),f16(a1))), % 72.51/72.51 inference(scs_inference,[],[7697,7715,7730,7732,7120,7577,7700,7160,7286,7453,6872,6667,49,7301,529,4,7,12,13,231,2,99,100,21,22,29,25,20])). % 72.51/72.51 cnf(7737,plain, % 72.51/72.51 (E(f6(x77371),f6(x77372))), % 72.51/72.51 inference(scs_inference,[],[7697,7715,7730,7732,7120,7577,7700,7160,7286,7669,7453,6872,6667,49,7301,529,4,7,12,13,231,2,99,100,21,22,29,25,20,3])). % 72.51/72.51 cnf(7750,plain, % 72.51/72.51 (E(f6(x77501),f6(x77502))), % 72.51/72.51 inference(rename_variables,[],[7737])). % 72.51/72.51 cnf(7752,plain, % 72.51/72.51 (E(f6(x77521),f6(x77522))), % 72.51/72.51 inference(rename_variables,[],[7737])). % 72.51/72.51 cnf(7754,plain, % 72.51/72.51 (E(f6(x77541),f6(x77542))), % 72.51/72.51 inference(rename_variables,[],[7737])). % 72.51/72.51 cnf(7756,plain, % 72.51/72.51 (E(f6(x77561),f6(x77562))), % 72.51/72.51 inference(rename_variables,[],[7737])). % 72.51/72.51 cnf(7758,plain, % 72.51/72.51 (E(f6(x77581),f6(x77582))), % 72.51/72.51 inference(rename_variables,[],[7737])). % 72.51/72.51 cnf(7760,plain, % 72.51/72.51 (E(f6(x77601),f6(x77602))), % 72.51/72.51 inference(rename_variables,[],[7737])). % 72.51/72.51 cnf(7761,plain, % 72.51/72.51 (E(a14,f15(f21(a2)))), % 72.51/72.51 inference(scs_inference,[],[7737,7750,7752,7754,7756,7758,7719,6855,213,266,243,271,385,245,382,2])). % 72.51/72.51 cnf(7762,plain, % 72.51/72.51 (P7(f6(x77621),f21(f22(a1)))), % 72.51/72.51 inference(scs_inference,[],[7737,7750,7752,7754,7756,7758,7733,7719,6855,6667,213,266,243,271,385,245,382,2,100])). % 72.51/72.51 cnf(7766,plain, % 72.51/72.51 (E(f6(x77661),f6(x77662))), % 72.51/72.51 inference(rename_variables,[],[7737])). % 72.51/72.51 cnf(7768,plain, % 72.51/72.51 (P11(f6(x77681),f21(f6(x77682)))), % 72.51/72.51 inference(scs_inference,[],[7737,7750,7752,7754,7756,7758,7760,7699,7733,7719,7291,7697,7055,7411,6855,6667,213,266,243,271,385,245,382,2,100,21,22,29])). % 72.51/72.51 cnf(7771,plain, % 72.51/72.51 (P7(f6(x77711),f21(a2))), % 72.51/72.51 inference(scs_inference,[],[6760,7737,7750,7752,7754,7756,7758,7760,7766,7699,7733,7719,7291,7697,7252,7055,7411,6855,285,6667,213,266,243,271,385,245,382,2,100,21,22,29,30,24])). % 72.51/72.51 cnf(7772,plain, % 72.51/72.51 (E(f6(x77721),f6(x77722))), % 72.51/72.51 inference(rename_variables,[],[7737])). % 72.51/72.51 cnf(7773,plain, % 72.51/72.51 (~P10(f19(a1,f16(a1)),a12,a2)), % 72.51/72.51 inference(scs_inference,[],[6760,7737,7750,7752,7754,7756,7758,7760,7766,7699,7708,7733,7719,7291,7697,7252,7055,7411,6855,7024,285,6667,213,266,243,271,385,245,382,2,100,21,22,29,30,24,20])). % 72.51/72.51 cnf(7774,plain, % 72.51/72.51 (P7(f15(a14),f6(x77741))), % 72.51/72.51 inference(scs_inference,[],[6760,7737,7750,7752,7754,7756,7758,7760,7766,7772,7699,7705,7708,7733,7719,7291,7697,7252,7055,7411,6855,7024,285,6667,213,266,243,271,385,245,382,2,100,21,22,29,30,24,20,25])). % 72.51/72.51 cnf(7776,plain, % 72.51/72.51 (E(f19(a14,a14),f19(f6(x77761),a2))), % 72.51/72.51 inference(scs_inference,[],[6760,7737,7750,7752,7754,7756,7758,7760,7766,7772,7699,7705,7708,7696,7667,7733,7719,7291,7697,7252,7055,7411,6855,7024,285,6667,213,266,243,271,385,245,382,2,100,21,22,29,30,24,20,25,3])). % 72.51/72.51 cnf(7786,plain, % 72.51/72.51 (~P10(f3(a12),f6(x77861),f3(a12))), % 72.51/72.51 inference(scs_inference,[],[7714,7776,7669,2,21])). % 72.51/72.51 cnf(7790,plain, % 72.51/72.51 (P11(f6(x77901),f21(a14))), % 72.51/72.51 inference(scs_inference,[],[6824,7714,7768,7776,7761,7737,6807,7669,6862,2,21,22,29,30])). % 72.51/72.51 cnf(7795,plain, % 72.51/72.51 (P10(f22(a1),f19(a1,a12),a12)), % 72.51/72.51 inference(scs_inference,[],[45,6824,7771,7714,7558,7768,7776,7761,7361,7737,7719,6807,7669,6784,6862,6872,56,46,61,2,21,22,29,30,24,20,3,106])). % 72.51/72.51 cnf(7797,plain, % 72.51/72.51 (E(f19(a1,a12),a12)), % 72.51/72.51 inference(scs_inference,[],[45,6824,7771,7714,7558,7768,7776,7761,7361,7737,7719,6807,6710,7669,7123,6784,6862,6872,56,370,46,61,2,21,22,29,30,24,20,3,106,108])). % 72.51/72.51 cnf(7804,plain, % 72.51/72.51 (E(f3(f19(a1,a12)),f3(a12))), % 72.51/72.51 inference(scs_inference,[],[45,6824,7771,7714,7558,7768,7776,7761,7361,7737,7719,6807,6710,7669,7123,6784,6862,6872,56,370,46,61,2,21,22,29,30,24,20,3,106,108,213,529,8,10])). % 72.51/72.51 cnf(7811,plain, % 72.51/72.51 (E(f15(f19(a1,a12)),f15(a12))), % 72.51/72.51 inference(scs_inference,[],[45,6824,7771,7714,7558,7768,7776,7761,7361,7737,7719,6807,6710,7669,7123,6784,6862,6872,56,370,46,61,2,21,22,29,30,24,20,3,106,108,213,529,8,10,9,11,14,5,16,15,6])). % 72.51/72.51 cnf(7812,plain, % 72.51/72.51 (E(f19(f19(a1,a12),x78121),f19(a12,x78121))), % 72.51/72.51 inference(scs_inference,[],[45,6824,7771,7714,7558,7768,7776,7761,7361,7737,7719,6807,6710,7669,7123,6784,6862,6872,56,370,46,61,2,21,22,29,30,24,20,3,106,108,213,529,8,10,9,11,14,5,16,15,6,12])). % 72.51/72.51 cnf(7813,plain, % 72.51/72.51 (E(f21(f19(a1,a12)),f21(a12))), % 72.51/72.51 inference(scs_inference,[],[45,6824,7771,7714,7558,7768,7776,7761,7361,7737,7719,6807,6710,7669,7123,6784,6862,6872,56,370,46,61,2,21,22,29,30,24,20,3,106,108,213,529,8,10,9,11,14,5,16,15,6,12,7])). % 72.51/72.51 cnf(7814,plain, % 72.51/72.51 (E(f19(x78141,f19(a1,a12)),f19(x78141,a12))), % 72.51/72.51 inference(scs_inference,[],[45,6824,7771,7714,7558,7768,7776,7761,7361,7737,7719,6807,6710,7669,7123,6784,6862,6872,56,370,46,61,2,21,22,29,30,24,20,3,106,108,213,529,8,10,9,11,14,5,16,15,6,12,7,13])). % 72.51/72.51 cnf(7827,plain, % 72.51/72.51 (E(a12,f19(a1,a12))), % 72.51/72.51 inference(scs_inference,[],[7797,2])). % 72.51/72.51 cnf(7830,plain, % 72.51/72.51 (P8(f6(f22(a1)),a12)), % 72.51/72.51 inference(scs_inference,[],[7797,6861,57,2,34,35])). % 72.51/72.51 cnf(7832,plain, % 72.51/72.51 (P7(x78321,f21(x78321))), % 72.51/72.51 inference(rename_variables,[],[6667])). % 72.51/72.51 cnf(7835,plain, % 72.51/72.51 (~P10(f3(a12),f6(x78351),f3(f19(a1,a12)))), % 72.51/72.51 inference(scs_inference,[],[7790,7786,7797,6861,7804,7773,57,6667,2,34,35,100,21,22])). % 72.51/72.51 cnf(7836,plain, % 72.51/72.51 (P11(f15(a12),f16(a1))), % 72.51/72.51 inference(scs_inference,[],[7790,7786,7797,6861,7811,7804,7773,7524,57,6667,2,34,35,100,21,22,29])). % 72.51/72.51 cnf(7838,plain, % 72.51/72.51 (P7(f15(a12),f22(a1))), % 72.51/72.51 inference(scs_inference,[],[7790,7786,7797,6861,7811,7804,7773,7524,6805,7505,57,6667,2,34,35,100,21,22,29,30,24])). % 72.51/72.51 cnf(7842,plain, % 72.51/72.51 (E(f19(a1,f19(a1,a12)),a12)), % 72.51/72.51 inference(scs_inference,[],[7790,7786,7797,6861,7814,7736,7811,7813,7804,7773,7524,6805,7505,57,6667,7832,2,34,35,100,21,22,29,30,24,20,25,3])). % 72.51/72.51 cnf(7846,plain, % 72.51/72.51 (~P10(f22(a1),f6(a14),f19(a1,a12))), % 72.51/72.51 inference(scs_inference,[],[6828,7790,7786,7797,6861,7814,7736,7811,7813,7804,7762,7773,7524,6805,7505,7123,57,6667,7832,370,2,34,35,100,21,22,29,30,24,20,25,3,104,108])). % 72.51/72.51 cnf(7849,plain, % 72.51/72.51 (P10(f22(a1),a12,f19(a1,a12))), % 72.51/72.51 inference(scs_inference,[],[6828,7795,7790,7786,7797,6861,7814,7736,7811,7813,7804,7762,7773,7524,6805,7505,6710,7123,57,6667,7832,370,2,34,35,100,21,22,29,30,24,20,25,3,104,108,110])). % 72.51/72.51 cnf(7851,plain, % 72.51/72.51 (~P10(f22(a1),a12,f6(x78511))), % 72.51/72.51 inference(scs_inference,[],[6828,7795,7790,7786,7797,6861,7814,7736,7811,7813,7804,7762,7773,7524,6805,7505,7737,6710,7123,57,6667,7832,370,2,34,35,100,21,22,29,30,24,20,25,3,104,108,110,7165])). % 72.51/72.51 cnf(7855,plain, % 72.51/72.51 (P7(f6(a12),f21(f19(a1,a12)))), % 72.51/72.51 inference(scs_inference,[],[6828,7795,7790,7786,7797,6861,7814,7736,7811,7813,7804,7762,7773,7524,6805,7505,7737,6710,7123,57,6667,7832,370,2,34,35,100,21,22,29,30,24,20,25,3,104,108,110,7165,92,529])). % 72.51/72.51 cnf(7858,plain, % 72.51/72.51 (E(f3(a12),f3(f19(a1,a12)))), % 72.51/72.51 inference(scs_inference,[],[6828,7795,7790,7786,7797,6861,7814,7736,7811,7813,7804,7762,7773,7524,6805,7505,7737,6710,7123,57,6667,7832,370,2,34,35,100,21,22,29,30,24,20,25,3,104,108,110,7165,92,529,8,10])). % 72.51/72.51 cnf(7865,plain, % 72.51/72.51 (E(f15(a12),f15(f19(a1,a12)))), % 72.51/72.51 inference(scs_inference,[],[6828,7795,7790,7786,7797,6861,7814,7736,7811,7813,7804,7762,7773,7524,6805,7505,7737,6710,7123,57,6667,7832,370,2,34,35,100,21,22,29,30,24,20,25,3,104,108,110,7165,92,529,8,10,9,11,14,5,15,16,6])). % 72.51/72.51 cnf(7867,plain, % 72.51/72.51 (E(f19(a12,x78671),f19(f19(a1,a12),x78671))), % 72.51/72.51 inference(scs_inference,[],[6828,7795,7790,7786,7797,6861,7814,7736,7811,7813,7804,7762,7773,7524,6805,7505,7737,6710,7123,57,6667,7832,370,2,34,35,100,21,22,29,30,24,20,25,3,104,108,110,7165,92,529,8,10,9,11,14,5,15,16,6,7,12])). % 72.51/72.51 cnf(7868,plain, % 72.51/72.51 (E(f19(x78681,a12),f19(x78681,f19(a1,a12)))), % 72.51/72.51 inference(scs_inference,[],[6828,7795,7790,7786,7797,6861,7814,7736,7811,7813,7804,7762,7773,7524,6805,7505,7737,6710,7123,57,6667,7832,370,2,34,35,100,21,22,29,30,24,20,25,3,104,108,110,7165,92,529,8,10,9,11,14,5,15,16,6,7,12,13])). % 72.51/72.51 cnf(7874,plain, % 72.51/72.51 (P8(f3(f19(a1,a12)),a12)), % 72.51/72.51 inference(scs_inference,[],[6828,7795,7790,7786,7797,6861,7814,7736,7811,7813,7804,7030,7762,7773,7524,6805,7505,7737,6710,7123,57,6667,7832,370,2,34,35,100,21,22,29,30,24,20,25,3,104,108,110,7165,92,529,8,10,9,11,14,5,15,16,6,7,12,13,93,231,91,490])). % 72.51/72.51 cnf(7887,plain, % 72.51/72.51 (E(a12,f19(a1,f19(a1,a12)))), % 72.51/72.51 inference(scs_inference,[],[7849,7842,7874,92,7165,2])). % 72.51/72.51 cnf(7890,plain, % 72.51/72.51 (~P10(f22(a1),a2,f19(a1,a12))), % 72.51/72.51 inference(scs_inference,[],[7846,7838,7849,7842,7874,7697,370,92,7165,2,91,21])). % 72.51/72.51 cnf(7894,plain, % 72.51/72.51 (~P11(f19(a1,a12),f15(a12))), % 72.51/72.51 inference(scs_inference,[],[7846,7827,7838,7849,7516,7865,7858,7842,7874,6083,7697,370,92,7165,2,91,21,22,29,30])). % 72.51/72.51 cnf(7898,plain, % 72.51/72.51 (E(f19(f19(a1,a12),f19(a1,a12)),f19(a12,a12))), % 72.51/72.51 inference(scs_inference,[],[7685,7846,7827,7838,7849,7419,7812,7516,7865,7858,7842,7874,7724,7814,7361,6083,7697,6677,370,92,7165,2,91,21,22,29,30,24,20,25,3])). % 72.51/72.51 cnf(7901,plain, % 72.51/72.51 (P10(f19(a1,a12),f6(a12),f6(a12))), % 72.51/72.51 inference(scs_inference,[],[7685,7846,7827,7838,7849,7419,7812,7516,7865,7855,7858,7842,7874,7724,7814,7361,6083,7697,6789,6677,370,92,7165,2,91,21,22,29,30,24,20,25,3,104])). % 72.51/72.51 cnf(7903,plain, % 72.51/72.51 (~P10(f22(a1),f6(x79031),a12)), % 72.51/72.51 inference(scs_inference,[],[7685,7846,7827,7838,7849,7851,7419,7812,7516,7865,7855,7858,7842,7874,7724,7814,7361,6083,7762,7697,6710,6789,6677,370,92,7165,2,91,21,22,29,30,24,20,25,3,104,110])). % 72.51/72.51 cnf(7921,plain, % 72.51/72.51 (E(f19(x79211,a12),f19(x79211,f19(a1,a12)))), % 72.51/72.51 inference(rename_variables,[],[7868])). % 72.51/72.51 cnf(7925,plain, % 72.51/72.51 (P11(f15(a12),f19(a1,a12))), % 72.51/72.51 inference(scs_inference,[],[6962,7836,7890,7898,7868,7887,7830,7616,7814,6872,92,2,21,22,29,30])). % 72.51/72.51 cnf(7926,plain, % 72.51/72.51 (~P7(a12,f21(a14))), % 72.51/72.51 inference(scs_inference,[],[6962,7836,7890,7898,7868,7887,7830,7616,7605,7814,6872,92,2,21,22,29,30,24])). % 72.51/72.51 cnf(7928,plain, % 72.51/72.51 (E(f19(x79281,a12),f19(x79281,f19(a1,a12)))), % 72.51/72.51 inference(rename_variables,[],[7868])). % 72.51/72.51 cnf(7929,plain, % 72.51/72.51 (P7(f20(a1),f19(a1,f19(a1,a12)))), % 72.51/72.51 inference(scs_inference,[],[6962,7836,7901,7890,7898,7868,7921,7928,7887,7830,7616,7605,6869,7814,6872,92,2,21,22,29,30,24,20,25])). % 72.51/72.51 cnf(7930,plain, % 72.51/72.51 (E(f19(x79301,a12),f19(x79301,f19(a1,a12)))), % 72.51/72.51 inference(rename_variables,[],[7868])). % 72.51/72.51 cnf(7931,plain, % 72.51/72.51 (E(f19(a2,a12),f19(f6(x79311),f19(a1,a12)))), % 72.51/72.51 inference(scs_inference,[],[6962,7836,7901,7890,7898,7868,7921,7928,7930,7720,7887,7830,7616,7605,6869,7814,6872,92,2,21,22,29,30,24,20,25,3])). % 72.51/72.51 cnf(7955,plain, % 72.51/72.51 (P11(f20(a1),f19(a1,f19(a1,a12)))), % 72.51/72.51 inference(scs_inference,[],[7405,7929,7931,2,91])). % 72.51/72.51 cnf(7959,plain, % 72.51/72.51 (~P10(f22(a1),f6(x79591),f19(a1,f19(a1,a12)))), % 72.51/72.51 inference(scs_inference,[],[7903,7405,7835,7929,7931,7842,7697,2,91,21,22])). % 72.51/72.51 cnf(7961,plain, % 72.51/72.51 (P11(f15(a12),f19(a1,f19(a1,a12)))), % 72.51/72.51 inference(scs_inference,[],[7925,7903,7405,7835,7929,7931,7868,7842,6671,7700,7697,2,91,21,22,29,30])). % 72.51/72.51 cnf(7966,plain, % 72.51/72.51 (E(f19(a12,a2),f19(f19(a1,a12),f6(x79661)))), % 72.51/72.51 inference(scs_inference,[],[7687,7925,7903,7926,7867,7721,7405,7835,7929,7931,7868,7842,7813,6671,7887,7700,6691,7697,6862,2,91,21,22,29,30,24,20,25,3])). % 72.51/72.51 cnf(7997,plain, % 72.51/72.51 (E(f22(a1),a12)), % 72.51/72.51 inference(scs_inference,[],[7894,7774,7627,7959,7955,7961,7966,7646,7851,7271,7858,7761,7598,7528,7842,7252,165,6667,50,93,2,99,100,21,22,29,30,24,20,25,3])). % 72.51/72.51 cnf(8025,plain, % 72.51/72.51 (~P10(f19(a1,a12),a12,f16(a1))), % 72.51/72.51 inference(scs_inference,[],[7894,7774,7627,7959,7955,7961,7966,7646,7851,7271,7858,7761,7598,7528,7842,7252,6988,6710,7587,165,6865,6667,370,50,93,2,99,100,21,22,29,30,24,20,25,3,7038,7519,5368,8,10,9,14,11,5,15,16,7,85,6,12,13,181,2874,5878,1957,105,5369,6831])). % 72.51/72.51 cnf(8036,plain, % 72.51/72.51 ($false), % 72.51/72.51 inference(scs_inference,[],[8025,7997,7087,2,21]), % 72.51/72.51 ['proof']). % 72.51/72.51 % SZS output end Proof % 72.51/72.51 % Total time :71.740000s %------------------------------------------------------------------------------