%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT300+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 : n028.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:43 EDT 2024 % Result : Theorem 118.48s 118.53s % Output : CNFRefutation 118.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.10 % Problem : LAT300+1 : TPTP v8.2.0. Released v3.4.0. % 0.02/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.09/0.30 % Computer : n028.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Fri Jun 21 22:05:24 EDT 2024 % 0.09/0.30 % CPUTime : % 0.15/0.55 start to proof:theBenchmark % 118.43/118.49 %------------------------------------------- % 118.43/118.49 % File :CSE---1.7 % 118.43/118.49 % Problem :theBenchmark % 118.43/118.49 % Transform :cnf % 118.43/118.49 % Format :tptp:raw % 118.43/118.49 % Command :java -jar mcs_scs.jar %d %s % 118.43/118.49 % 118.43/118.49 % Result :Theorem 117.870000s % 118.43/118.49 % Output :CNFRefutation 117.870000s % 118.43/118.49 %------------------------------------------- % 118.43/118.51 %------------------------------------------------------------------------------ % 118.43/118.51 % File : LAT300+1 : TPTP v8.2.0. Released v3.4.0. % 118.43/118.51 % Domain : Lattice Theory % 118.43/118.51 % Problem : Ideals T24 % 118.43/118.51 % Version : [Urb08] axioms : Especial. % 118.43/118.51 % English : % 118.43/118.51 % 118.43/118.51 % Refs : [Ban96] Bancerek (1996), Ideals % 118.43/118.51 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 118.43/118.51 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 118.43/118.51 % Source : [Urb08] % 118.43/118.51 % Names : t24_filter_2 [Urb08] % 118.43/118.51 % 118.43/118.51 % Status : Theorem % 118.43/118.51 % Rating : 0.11 v8.2.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.07 v7.2.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.08 v6.3.0, 0.12 v6.2.0, 0.08 v6.1.0, 0.17 v6.0.0, 0.13 v5.5.0, 0.19 v5.4.0, 0.21 v5.3.0, 0.26 v5.2.0, 0.05 v5.1.0, 0.10 v5.0.0, 0.12 v4.1.0, 0.17 v4.0.0, 0.21 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0 % 118.43/118.51 % Syntax : Number of formulae : 44 ( 15 unt; 0 def) % 118.43/118.51 % Number of atoms : 127 ( 2 equ) % 118.43/118.51 % Maximal formula atoms : 10 ( 2 avg) % 118.43/118.51 % Number of connectives : 115 ( 32 ~; 1 |; 51 &) % 118.43/118.51 % ( 2 <=>; 29 =>; 0 <=; 0 <~>) % 118.43/118.51 % Maximal formula depth : 10 ( 4 avg) % 118.43/118.51 % Maximal term depth : 3 ( 1 avg) % 118.43/118.51 % Number of predicates : 22 ( 20 usr; 1 prp; 0-3 aty) % 118.43/118.51 % Number of functors : 3 ( 3 usr; 1 con; 0-1 aty) % 118.43/118.51 % Number of variables : 66 ( 50 !; 16 ?) % 118.43/118.51 % SPC : FOF_THM_RFO_SEQ % 118.43/118.51 % 118.43/118.51 % Comments : Normal version: includes the axioms (which may be theorems from % 118.43/118.51 % other articles) and background that are possibly necessary. % 118.43/118.51 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 118.43/118.52 % : The problem encoding is based on set theory. % 118.43/118.52 %------------------------------------------------------------------------------ % 118.43/118.52 fof(t24_filter_2,conjecture, % 118.43/118.52 ! [A] : % 118.43/118.52 ( ( ~ v3_struct_0(A) % 118.43/118.52 & v10_lattices(A) % 118.43/118.52 & l3_lattices(A) ) % 118.43/118.52 => ! [B] : % 118.43/118.52 ( m2_filter_2(B,A) % 118.43/118.52 => ? [C] : % 118.43/118.52 ( m1_subset_1(C,u1_struct_0(A)) % 118.43/118.52 & r2_hidden(C,B) ) ) ) ). % 118.43/118.52 % 118.43/118.52 fof(antisymmetry_r2_hidden,axiom, % 118.43/118.52 ! [A,B] : % 118.43/118.52 ( r2_hidden(A,B) % 118.43/118.52 => ~ r2_hidden(B,A) ) ). % 118.43/118.52 % 118.43/118.52 fof(cc1_funct_1,axiom, % 118.43/118.52 ! [A] : % 118.43/118.52 ( v1_xboole_0(A) % 118.43/118.52 => v1_funct_1(A) ) ). % 118.43/118.52 % 118.43/118.52 fof(cc1_lattices,axiom, % 118.43/118.52 ! [A] : % 118.43/118.52 ( l3_lattices(A) % 118.43/118.52 => ( ( ~ v3_struct_0(A) % 118.43/118.52 & v10_lattices(A) ) % 118.43/118.52 => ( ~ v3_struct_0(A) % 118.43/118.52 & v4_lattices(A) % 118.43/118.52 & v5_lattices(A) % 118.43/118.52 & v6_lattices(A) % 118.43/118.52 & v7_lattices(A) % 118.48/118.52 & v8_lattices(A) % 118.48/118.52 & v9_lattices(A) ) ) ) ). % 118.48/118.52 % 118.48/118.52 fof(cc2_lattices,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ( l3_lattices(A) % 118.48/118.52 => ( ( ~ v3_struct_0(A) % 118.48/118.52 & v4_lattices(A) % 118.48/118.52 & v5_lattices(A) % 118.48/118.52 & v6_lattices(A) % 118.48/118.52 & v7_lattices(A) % 118.48/118.52 & v8_lattices(A) % 118.48/118.52 & v9_lattices(A) ) % 118.48/118.52 => ( ~ v3_struct_0(A) % 118.48/118.52 & v10_lattices(A) ) ) ) ). % 118.48/118.52 % 118.48/118.52 fof(dt_k1_xboole_0,axiom, % 118.48/118.52 $true ). % 118.48/118.52 % 118.48/118.52 fof(dt_k1_zfmisc_1,axiom, % 118.48/118.52 $true ). % 118.48/118.52 % 118.48/118.52 fof(dt_l1_lattices,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ( l1_lattices(A) % 118.48/118.52 => l1_struct_0(A) ) ). % 118.48/118.52 % 118.48/118.52 fof(dt_l1_struct_0,axiom, % 118.48/118.52 $true ). % 118.48/118.52 % 118.48/118.52 fof(dt_l2_lattices,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ( l2_lattices(A) % 118.48/118.52 => l1_struct_0(A) ) ). % 118.48/118.52 % 118.48/118.52 fof(dt_l3_lattices,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ( l3_lattices(A) % 118.48/118.52 => ( l1_lattices(A) % 118.48/118.52 & l2_lattices(A) ) ) ). % 118.48/118.52 % 118.48/118.52 fof(dt_m1_struct_0,axiom, % 118.48/118.52 ! [A,B] : % 118.48/118.52 ( ( ~ v3_struct_0(A) % 118.48/118.52 & l1_struct_0(A) % 118.48/118.52 & ~ v1_xboole_0(B) % 118.48/118.52 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 118.48/118.52 => ! [C] : % 118.48/118.52 ( m1_struct_0(C,A,B) % 118.48/118.52 => m1_subset_1(C,u1_struct_0(A)) ) ) ). % 118.48/118.52 % 118.48/118.52 fof(dt_m1_subset_1,axiom, % 118.48/118.52 $true ). % 118.48/118.52 % 118.48/118.52 fof(dt_m2_filter_2,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ( ( ~ v3_struct_0(A) % 118.48/118.52 & v10_lattices(A) % 118.48/118.52 & l3_lattices(A) ) % 118.48/118.52 => ! [B] : % 118.48/118.52 ( m2_filter_2(B,A) % 118.48/118.52 => ( ~ v1_xboole_0(B) % 118.48/118.52 & m2_lattice4(B,A) ) ) ) ). % 118.48/118.52 % 118.48/118.52 fof(dt_m2_lattice4,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ( ( ~ v3_struct_0(A) % 118.48/118.52 & v10_lattices(A) % 118.48/118.52 & l3_lattices(A) ) % 118.48/118.52 => ! [B] : % 118.48/118.52 ( m2_lattice4(B,A) % 118.48/118.52 => m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ) ). % 118.48/118.52 % 118.48/118.52 fof(dt_u1_struct_0,axiom, % 118.48/118.52 $true ). % 118.48/118.52 % 118.48/118.52 fof(existence_l1_lattices,axiom, % 118.48/118.52 ? [A] : l1_lattices(A) ). % 118.48/118.52 % 118.48/118.52 fof(existence_l1_struct_0,axiom, % 118.48/118.52 ? [A] : l1_struct_0(A) ). % 118.48/118.52 % 118.48/118.52 fof(existence_l2_lattices,axiom, % 118.48/118.52 ? [A] : l2_lattices(A) ). % 118.48/118.52 % 118.48/118.52 fof(existence_l3_lattices,axiom, % 118.48/118.52 ? [A] : l3_lattices(A) ). % 118.48/118.52 % 118.48/118.52 fof(existence_m1_struct_0,axiom, % 118.48/118.52 ! [A,B] : % 118.48/118.52 ( ( ~ v3_struct_0(A) % 118.48/118.52 & l1_struct_0(A) % 118.48/118.52 & ~ v1_xboole_0(B) % 118.48/118.52 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 118.48/118.52 => ? [C] : m1_struct_0(C,A,B) ) ). % 118.48/118.52 % 118.48/118.52 fof(existence_m1_subset_1,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ? [B] : m1_subset_1(B,A) ). % 118.48/118.52 % 118.48/118.52 fof(existence_m2_filter_2,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ( ( ~ v3_struct_0(A) % 118.48/118.52 & v10_lattices(A) % 118.48/118.52 & l3_lattices(A) ) % 118.48/118.52 => ? [B] : m2_filter_2(B,A) ) ). % 118.48/118.52 % 118.48/118.52 fof(existence_m2_lattice4,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ( ( ~ v3_struct_0(A) % 118.48/118.52 & v10_lattices(A) % 118.48/118.52 & l3_lattices(A) ) % 118.48/118.52 => ? [B] : m2_lattice4(B,A) ) ). % 118.48/118.52 % 118.48/118.52 fof(fc1_struct_0,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ( ( ~ v3_struct_0(A) % 118.48/118.52 & l1_struct_0(A) ) % 118.48/118.52 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 118.48/118.52 % 118.48/118.52 fof(fc1_subset_1,axiom, % 118.48/118.52 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 118.48/118.52 % 118.48/118.52 fof(fc1_xboole_0,axiom, % 118.48/118.52 v1_xboole_0(k1_xboole_0) ). % 118.48/118.52 % 118.48/118.52 fof(rc1_lattice4,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ( ( ~ v3_struct_0(A) % 118.48/118.52 & v10_lattices(A) % 118.48/118.52 & l3_lattices(A) ) % 118.48/118.52 => ? [B] : % 118.48/118.52 ( m2_lattice4(B,A) % 118.48/118.52 & ~ v1_xboole_0(B) ) ) ). % 118.48/118.52 % 118.48/118.52 fof(rc1_subset_1,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ( ~ v1_xboole_0(A) % 118.48/118.52 => ? [B] : % 118.48/118.52 ( m1_subset_1(B,k1_zfmisc_1(A)) % 118.48/118.52 & ~ v1_xboole_0(B) ) ) ). % 118.48/118.52 % 118.48/118.52 fof(rc1_xboole_0,axiom, % 118.48/118.52 ? [A] : v1_xboole_0(A) ). % 118.48/118.52 % 118.48/118.52 fof(rc2_subset_1,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ? [B] : % 118.48/118.52 ( m1_subset_1(B,k1_zfmisc_1(A)) % 118.48/118.52 & v1_xboole_0(B) ) ). % 118.48/118.52 % 118.48/118.52 fof(rc2_xboole_0,axiom, % 118.48/118.52 ? [A] : ~ v1_xboole_0(A) ). % 118.48/118.52 % 118.48/118.52 fof(rc3_struct_0,axiom, % 118.48/118.52 ? [A] : % 118.48/118.52 ( l1_struct_0(A) % 118.48/118.52 & ~ v3_struct_0(A) ) ). % 118.48/118.52 % 118.48/118.52 fof(rc5_struct_0,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ( ( ~ v3_struct_0(A) % 118.48/118.52 & l1_struct_0(A) ) % 118.48/118.52 => ? [B] : % 118.48/118.52 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 118.48/118.52 & ~ v1_xboole_0(B) ) ) ). % 118.48/118.52 % 118.48/118.52 fof(redefinition_m1_struct_0,axiom, % 118.48/118.52 ! [A,B] : % 118.48/118.52 ( ( ~ v3_struct_0(A) % 118.48/118.52 & l1_struct_0(A) % 118.48/118.52 & ~ v1_xboole_0(B) % 118.48/118.52 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 118.48/118.52 => ! [C] : % 118.48/118.52 ( m1_struct_0(C,A,B) % 118.48/118.52 <=> m1_subset_1(C,B) ) ) ). % 118.48/118.52 % 118.48/118.52 fof(reflexivity_r1_tarski,axiom, % 118.48/118.52 ! [A,B] : r1_tarski(A,A) ). % 118.48/118.52 % 118.48/118.52 fof(t1_subset,axiom, % 118.48/118.52 ! [A,B] : % 118.48/118.52 ( r2_hidden(A,B) % 118.48/118.52 => m1_subset_1(A,B) ) ). % 118.48/118.52 % 118.48/118.52 fof(t2_subset,axiom, % 118.48/118.52 ! [A,B] : % 118.48/118.52 ( m1_subset_1(A,B) % 118.48/118.52 => ( v1_xboole_0(B) % 118.48/118.52 | r2_hidden(A,B) ) ) ). % 118.48/118.52 % 118.48/118.52 fof(t3_subset,axiom, % 118.48/118.52 ! [A,B] : % 118.48/118.52 ( m1_subset_1(A,k1_zfmisc_1(B)) % 118.48/118.52 <=> r1_tarski(A,B) ) ). % 118.48/118.52 % 118.48/118.52 fof(t4_subset,axiom, % 118.48/118.52 ! [A,B,C] : % 118.48/118.52 ( ( r2_hidden(A,B) % 118.48/118.52 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 118.48/118.52 => m1_subset_1(A,C) ) ). % 118.48/118.52 % 118.48/118.52 fof(t5_subset,axiom, % 118.48/118.52 ! [A,B,C] : % 118.48/118.52 ~ ( r2_hidden(A,B) % 118.48/118.52 & m1_subset_1(B,k1_zfmisc_1(C)) % 118.48/118.52 & v1_xboole_0(C) ) ). % 118.48/118.52 % 118.48/118.52 fof(t6_boole,axiom, % 118.48/118.52 ! [A] : % 118.48/118.52 ( v1_xboole_0(A) % 118.48/118.52 => A = k1_xboole_0 ) ). % 118.48/118.52 % 118.48/118.52 fof(t7_boole,axiom, % 118.48/118.53 ! [A,B] : % 118.48/118.53 ~ ( r2_hidden(A,B) % 118.48/118.53 & v1_xboole_0(B) ) ). % 118.48/118.53 % 118.48/118.53 fof(t8_boole,axiom, % 118.48/118.53 ! [A,B] : % 118.48/118.53 ~ ( v1_xboole_0(A) % 118.48/118.53 & A != B % 118.48/118.53 & v1_xboole_0(B) ) ). % 118.48/118.53 % 118.48/118.53 %------------------------------------------------------------------------------ % 118.48/118.53 %------------------------------------------- % 118.48/118.53 % Proof found % 118.48/118.53 % SZS status Theorem for theBenchmark % 118.48/118.53 % SZS output start Proof % 118.48/118.54 %ClaNum:98(EqnAxiom:41) % 118.48/118.54 %VarNum:187(SingletonVarNum:65) % 118.48/118.54 %MaxLitNum:9 % 118.48/118.54 %MaxfuncDepth:2 % 118.48/118.54 %SharedTerms:24 % 118.48/118.54 %goalClause: 42 43 52 56 87 % 118.48/118.54 %singleGoalClaCount:4 % 118.48/118.54 [42]P1(a1) % 118.48/118.54 [43]P2(a1) % 118.48/118.54 [44]P2(a10) % 118.48/118.54 [45]P12(a15) % 118.48/118.54 [46]P12(a2) % 118.48/118.54 [47]P3(a11) % 118.48/118.54 [48]P4(a13) % 118.48/118.54 [49]P4(a6) % 118.48/118.54 [50]P5(a14) % 118.48/118.54 [52]P6(a12,a1) % 118.48/118.54 [56]~P14(a1) % 118.48/118.54 [57]~P14(a6) % 118.48/118.54 [58]~P12(a8) % 118.48/118.54 [53]P9(x531,x531) % 118.48/118.54 [51]P12(f7(x511)) % 118.48/118.54 [54]P7(f16(x541),x541) % 118.48/118.54 [55]P7(f7(x551),f19(x551)) % 118.48/118.54 [59]~P12(f19(x591)) % 118.48/118.54 [60]~P12(x601)+E(x601,a15) % 118.48/118.54 [61]~P12(x611)+P13(x611) % 118.48/118.54 [62]~P2(x621)+P3(x621) % 118.48/118.54 [63]~P3(x631)+P4(x631) % 118.48/118.54 [64]~P5(x641)+P4(x641) % 118.48/118.54 [65]~P2(x651)+P5(x651) % 118.48/118.54 [67]P12(x671)+~P12(f3(x671)) % 118.48/118.54 [77]P12(x771)+P7(f3(x771),f19(x771)) % 118.48/118.54 [87]~P11(x871,a12)+~P7(x871,f20(a1)) % 118.48/118.54 [76]~P12(x761)+~P11(x762,x761) % 118.48/118.54 [79]~P11(x791,x792)+P7(x791,x792) % 118.48/118.54 [85]~P11(x852,x851)+~P11(x851,x852) % 118.48/118.54 [84]~P9(x841,x842)+P7(x841,f19(x842)) % 118.48/118.54 [86]P9(x861,x862)+~P7(x861,f19(x862)) % 118.48/118.54 [74]~P4(x741)+P14(x741)+~P12(f20(x741)) % 118.48/118.54 [75]~P4(x751)+P14(x751)+~P12(f9(x751)) % 118.48/118.54 [89]~P4(x891)+P14(x891)+P7(f9(x891),f19(f20(x891))) % 118.48/118.54 [66]~P12(x662)+~P12(x661)+E(x661,x662) % 118.48/118.54 [83]~P7(x832,x831)+P12(x831)+P11(x832,x831) % 118.48/118.54 [92]~P12(x921)+~P11(x922,x923)+~P7(x923,f19(x921)) % 118.48/118.54 [93]P7(x931,x932)+~P11(x931,x933)+~P7(x933,f19(x932)) % 118.48/118.54 [68]P15(x681)+~P1(x681)+~P2(x681)+P14(x681) % 118.48/118.54 [69]P16(x691)+~P1(x691)+~P2(x691)+P14(x691) % 118.48/118.54 [70]P17(x701)+~P1(x701)+~P2(x701)+P14(x701) % 118.48/118.54 [71]P18(x711)+~P1(x711)+~P2(x711)+P14(x711) % 118.48/118.54 [72]P19(x721)+~P1(x721)+~P2(x721)+P14(x721) % 118.48/118.54 [73]P20(x731)+~P1(x731)+~P2(x731)+P14(x731) % 118.48/118.54 [78]~P1(x781)+~P2(x781)+P14(x781)+~P12(f4(x781)) % 118.48/118.54 [80]~P1(x801)+~P2(x801)+P14(x801)+P6(f18(x801),x801) % 118.48/118.54 [81]~P1(x811)+~P2(x811)+P14(x811)+P10(f5(x811),x811) % 118.48/118.54 [82]~P1(x821)+~P2(x821)+P14(x821)+P10(f4(x821),x821) % 118.48/118.54 [88]~P1(x881)+~P2(x881)+~P6(x882,x881)+P14(x881)+~P12(x882) % 118.48/118.54 [90]~P1(x901)+~P2(x901)+~P6(x902,x901)+P14(x901)+P10(x902,x901) % 118.48/118.54 [94]~P1(x941)+~P2(x941)+~P10(x942,x941)+P14(x941)+P7(x942,f19(f20(x941))) % 118.48/118.54 [96]~P4(x961)+P14(x961)+P12(x962)+P8(f17(x961,x962),x961,x962)+~P7(x962,f19(f20(x961))) % 118.48/118.54 [95]~P4(x951)+~P7(x953,x952)+P14(x951)+P8(x953,x951,x952)+P12(x952)+~P7(x952,f19(f20(x951))) % 118.48/118.54 [97]~P4(x971)+~P8(x973,x971,x972)+P14(x971)+P7(x973,x972)+P12(x972)+~P7(x972,f19(f20(x971))) % 118.48/118.54 [98]~P4(x981)+~P8(x983,x981,x982)+P14(x981)+P12(x982)+P7(x983,f20(x981))+~P7(x982,f19(f20(x981))) % 118.48/118.54 [91]P1(x911)+~P2(x911)+~P15(x911)+~P16(x911)+~P17(x911)+~P18(x911)+~P19(x911)+~P20(x911)+P14(x911) % 118.48/118.54 %EqnAxiom % 118.48/118.54 [1]E(x11,x11) % 118.48/118.54 [2]E(x22,x21)+~E(x21,x22) % 118.48/118.54 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 118.48/118.54 [4]~E(x41,x42)+E(f7(x41),f7(x42)) % 118.48/118.54 [5]~E(x51,x52)+E(f16(x51),f16(x52)) % 118.48/118.54 [6]~E(x61,x62)+E(f19(x61),f19(x62)) % 118.48/118.54 [7]~E(x71,x72)+E(f20(x71),f20(x72)) % 118.48/118.54 [8]~E(x81,x82)+E(f9(x81),f9(x82)) % 118.48/118.54 [9]~E(x91,x92)+E(f3(x91),f3(x92)) % 118.48/118.54 [10]~E(x101,x102)+E(f17(x101,x103),f17(x102,x103)) % 118.48/118.54 [11]~E(x111,x112)+E(f17(x113,x111),f17(x113,x112)) % 118.48/118.54 [12]~E(x121,x122)+E(f5(x121),f5(x122)) % 118.48/118.54 [13]~E(x131,x132)+E(f18(x131),f18(x132)) % 118.48/118.54 [14]~E(x141,x142)+E(f4(x141),f4(x142)) % 118.48/118.54 [15]~P1(x151)+P1(x152)+~E(x151,x152) % 118.48/118.54 [16]~P2(x161)+P2(x162)+~E(x161,x162) % 118.48/118.54 [17]P8(x172,x173,x174)+~E(x171,x172)+~P8(x171,x173,x174) % 118.48/118.54 [18]P8(x183,x182,x184)+~E(x181,x182)+~P8(x183,x181,x184) % 118.48/118.54 [19]P8(x193,x194,x192)+~E(x191,x192)+~P8(x193,x194,x191) % 118.48/118.54 [20]~P12(x201)+P12(x202)+~E(x201,x202) % 118.48/118.54 [21]~P20(x211)+P20(x212)+~E(x211,x212) % 118.48/118.54 [22]~P3(x221)+P3(x222)+~E(x221,x222) % 118.48/118.54 [23]~P4(x231)+P4(x232)+~E(x231,x232) % 118.48/118.54 [24]P9(x242,x243)+~E(x241,x242)+~P9(x241,x243) % 118.48/118.54 [25]P9(x253,x252)+~E(x251,x252)+~P9(x253,x251) % 118.48/118.54 [26]~P5(x261)+P5(x262)+~E(x261,x262) % 118.48/118.54 [27]~P19(x271)+P19(x272)+~E(x271,x272) % 118.48/118.54 [28]P6(x282,x283)+~E(x281,x282)+~P6(x281,x283) % 118.48/118.54 [29]P6(x293,x292)+~E(x291,x292)+~P6(x293,x291) % 118.48/118.54 [30]P10(x302,x303)+~E(x301,x302)+~P10(x301,x303) % 118.48/118.54 [31]P10(x313,x312)+~E(x311,x312)+~P10(x313,x311) % 118.48/118.54 [32]P7(x322,x323)+~E(x321,x322)+~P7(x321,x323) % 118.48/118.54 [33]P7(x333,x332)+~E(x331,x332)+~P7(x333,x331) % 118.48/118.54 [34]~P14(x341)+P14(x342)+~E(x341,x342) % 118.48/118.54 [35]P11(x352,x353)+~E(x351,x352)+~P11(x351,x353) % 118.48/118.54 [36]P11(x363,x362)+~E(x361,x362)+~P11(x363,x361) % 118.48/118.54 [37]~P18(x371)+P18(x372)+~E(x371,x372) % 118.48/118.54 [38]~P17(x381)+P17(x382)+~E(x381,x382) % 118.48/118.54 [39]~P16(x391)+P16(x392)+~E(x391,x392) % 118.48/118.54 [40]~P15(x401)+P15(x402)+~E(x401,x402) % 118.48/118.54 [41]~P13(x411)+P13(x412)+~E(x411,x412) % 118.48/118.54 % 118.48/118.54 %------------------------------------------- % 118.52/118.56 cnf(99,plain, % 118.52/118.56 (~P11(f16(f20(a1)),a12)), % 118.52/118.56 inference(scs_inference,[],[54,87])). % 118.52/118.56 cnf(100,plain, % 118.52/118.56 (P7(f16(x1001),x1001)), % 118.52/118.56 inference(rename_variables,[],[54])). % 118.52/118.56 cnf(104,plain, % 118.52/118.56 (P9(f16(f19(x1041)),x1041)), % 118.52/118.56 inference(scs_inference,[],[54,100,45,87,76,86])). % 118.52/118.56 cnf(105,plain, % 118.52/118.56 (P7(f16(x1051),x1051)), % 118.52/118.56 inference(rename_variables,[],[54])). % 118.52/118.56 cnf(107,plain, % 118.52/118.56 (P11(f16(a8),a8)), % 118.52/118.56 inference(scs_inference,[],[54,100,105,45,58,87,76,86,83])). % 118.52/118.56 cnf(108,plain, % 118.52/118.56 (P7(f16(x1081),x1081)), % 118.52/118.56 inference(rename_variables,[],[54])). % 118.52/118.56 cnf(110,plain, % 118.52/118.56 (~E(a8,a15)), % 118.52/118.56 inference(scs_inference,[],[54,100,105,45,58,87,76,86,83,36])). % 118.52/118.56 cnf(111,plain, % 118.52/118.56 (~P11(x1111,f16(f19(a15)))), % 118.52/118.56 inference(scs_inference,[],[54,100,105,108,45,58,87,76,86,83,36,92])). % 118.52/118.56 cnf(112,plain, % 118.52/118.56 (P7(f16(x1121),x1121)), % 118.52/118.56 inference(rename_variables,[],[54])). % 118.52/118.56 cnf(126,plain, % 118.52/118.56 (~P6(a15,a1)), % 118.52/118.56 inference(scs_inference,[],[42,43,56,54,100,105,108,45,58,87,76,86,83,36,92,68,69,70,71,72,73,88])). % 118.52/118.56 cnf(128,plain, % 118.52/118.56 (P10(a12,a1)), % 118.52/118.56 inference(scs_inference,[],[42,43,52,56,54,100,105,108,45,58,87,76,86,83,36,92,68,69,70,71,72,73,88,90])). % 118.52/118.56 cnf(132,plain, % 118.52/118.56 (P7(x1321,x1322)+~P11(x1321,f16(f19(x1322)))), % 118.52/118.56 inference(scs_inference,[],[42,43,52,56,54,100,105,108,112,45,58,87,76,86,83,36,92,68,69,70,71,72,73,88,90,85,93])). % 118.52/118.56 cnf(133,plain, % 118.52/118.56 (P7(f16(x1331),x1331)), % 118.52/118.56 inference(rename_variables,[],[54])). % 118.52/118.56 cnf(136,plain, % 118.52/118.56 (~P12(a12)), % 118.52/118.56 inference(scs_inference,[],[42,43,52,56,54,100,105,108,112,45,58,87,76,86,83,36,92,68,69,70,71,72,73,88,90,85,93,28,66])). % 118.52/118.56 cnf(139,plain, % 118.52/118.56 (P7(x1391,x1392)+~E(f16(x1392),x1391)), % 118.52/118.56 inference(scs_inference,[],[42,43,52,56,54,100,105,108,112,133,45,58,87,76,86,83,36,92,68,69,70,71,72,73,88,90,85,93,28,66,29,32])). % 118.52/118.56 cnf(140,plain, % 118.52/118.56 (P7(f16(x1401),x1402)+~E(x1401,x1402)), % 118.52/118.56 inference(scs_inference,[],[42,43,52,56,54,100,105,108,112,133,45,58,87,76,86,83,36,92,68,69,70,71,72,73,88,90,85,93,28,66,29,32,33])). % 118.52/118.56 cnf(148,plain, % 118.52/118.56 (P9(f7(x1481),x1481)), % 118.52/118.56 inference(scs_inference,[],[55,86])). % 118.52/118.56 cnf(152,plain, % 118.52/118.56 (~P7(f16(f20(a1)),a12)), % 118.52/118.56 inference(scs_inference,[],[99,55,46,136,86,76,83])). % 118.52/118.56 cnf(155,plain, % 118.52/118.56 (P7(f16(x1551),x1551)), % 118.52/118.56 inference(rename_variables,[],[54])). % 118.52/118.56 cnf(156,plain, % 118.52/118.56 (~P11(x1561,f16(f19(a2)))), % 118.52/118.56 inference(scs_inference,[],[99,54,155,55,46,136,86,76,83,33,92])). % 118.52/118.56 cnf(157,plain, % 118.52/118.56 (P7(f16(x1571),x1571)), % 118.52/118.56 inference(rename_variables,[],[54])). % 118.52/118.56 cnf(159,plain, % 118.52/118.56 (~E(f16(a12),f16(f20(a1)))), % 118.52/118.56 inference(scs_inference,[],[99,54,155,157,55,46,136,86,76,83,33,92,32])). % 118.52/118.56 cnf(160,plain, % 118.52/118.56 (P7(f16(x1601),x1601)), % 118.52/118.56 inference(rename_variables,[],[54])). % 118.52/118.56 cnf(163,plain, % 118.52/118.56 (~P6(a2,a1)), % 118.52/118.56 inference(scs_inference,[],[42,43,99,56,107,54,155,157,111,55,46,136,86,76,83,33,92,32,36,88])). % 118.52/118.56 cnf(171,plain, % 118.52/118.56 (P9(f16(f19(x1711)),x1712)+~E(x1711,x1712)), % 118.52/118.56 inference(scs_inference,[],[42,43,99,56,107,128,54,155,157,160,104,111,55,46,136,86,76,83,33,92,32,36,88,5,31,93,24,25])). % 118.52/118.56 cnf(177,plain, % 118.52/118.56 (~P11(x1771,f7(x1772))), % 118.52/118.56 inference(scs_inference,[],[51,76])). % 118.52/118.56 cnf(179,plain, % 118.52/118.56 (P11(f16(f19(x1791)),f19(x1791))), % 118.52/118.56 inference(scs_inference,[],[54,51,59,76,83])). % 118.52/118.56 cnf(182,plain, % 118.52/118.56 (~E(a12,a2)), % 118.52/118.56 inference(scs_inference,[],[52,163,54,51,59,76,83,28])). % 118.52/118.56 cnf(185,plain, % 118.52/118.56 (~P6(f7(x1851),a1)), % 118.52/118.56 inference(scs_inference,[],[42,43,52,56,107,163,54,156,51,59,76,83,28,36,88])). % 118.52/118.56 cnf(189,plain, % 118.52/118.56 (P11(x1891,f19(x1892))+~E(f16(f19(x1892)),x1891)), % 118.52/118.56 inference(scs_inference,[],[42,43,52,56,107,163,54,156,51,59,76,83,28,36,88,85,35])). % 118.52/118.56 cnf(190,plain, % 118.52/118.56 (P9(f7(x1901),x1902)+~E(x1901,x1902)), % 118.52/118.56 inference(scs_inference,[],[42,43,52,56,107,163,54,148,156,51,59,76,83,28,36,88,85,35,25])). % 118.52/118.56 cnf(191,plain, % 118.52/118.56 (P9(x1911,x1912)+~E(f7(x1912),x1911)), % 118.52/118.56 inference(scs_inference,[],[42,43,52,56,107,163,54,148,156,51,59,76,83,28,36,88,85,35,25,24])). % 118.52/118.56 cnf(194,plain, % 118.52/118.56 (P7(f7(x1941),x1942)+~E(f19(x1941),x1942)), % 118.52/118.56 inference(scs_inference,[],[42,43,52,56,107,159,163,54,148,156,51,59,55,76,83,28,36,88,85,35,25,24,66,33])). % 118.52/118.56 cnf(195,plain, % 118.52/118.56 (P7(x1951,f19(x1952))+~E(f7(x1952),x1951)), % 118.52/118.56 inference(scs_inference,[],[42,43,52,56,107,159,163,54,148,156,51,59,55,76,83,28,36,88,85,35,25,24,66,33,32])). % 118.52/118.56 cnf(201,plain, % 118.52/118.56 (~E(a8,f7(x2011))), % 118.52/118.56 inference(scs_inference,[],[107,177,36])). % 118.52/118.56 cnf(203,plain, % 118.52/118.56 (~E(a12,f7(x2031))), % 118.52/118.56 inference(scs_inference,[],[52,107,185,177,36,28])). % 118.52/118.56 cnf(204,plain, % 118.52/118.56 (P9(x2041,x2042)+~E(x2042,x2041)), % 118.52/118.56 inference(scs_inference,[],[52,107,185,177,53,36,28,24])). % 118.52/118.56 cnf(205,plain, % 118.52/118.56 (P9(x2051,x2052)+~E(x2051,x2052)), % 118.52/118.56 inference(scs_inference,[],[52,107,185,177,53,36,28,24,25])). % 118.52/118.56 cnf(221,plain, % 118.52/118.56 (~E(f19(x2211),f7(x2212))), % 118.52/118.56 inference(scs_inference,[],[179,177,36])). % 118.52/118.56 cnf(297,plain, % 118.52/118.56 (P4(a1)), % 118.52/118.56 inference(scs_inference,[],[43,62,63])). % 118.52/118.56 cnf(347,plain, % 118.52/118.56 (~P12(f3(a8))), % 118.52/118.56 inference(scs_inference,[],[110,60,67])). % 118.52/118.56 cnf(348,plain, % 118.52/118.56 (P11(f16(f3(a8)),f3(a8))), % 118.52/118.56 inference(scs_inference,[],[54,347,83])). % 118.52/118.56 cnf(363,plain, % 118.52/118.56 (~E(f3(a8),f7(x3631))), % 118.52/118.56 inference(scs_inference,[],[348,177,36])). % 118.52/118.56 cnf(385,plain, % 118.52/118.56 (E(a15,a2)), % 118.52/118.56 inference(scs_inference,[],[46,2,60])). % 118.52/118.56 cnf(387,plain, % 118.52/118.56 (E(a2,a15)), % 118.52/118.56 inference(scs_inference,[],[385,140,2])). % 118.52/118.56 cnf(390,plain, % 118.52/118.56 (P9(a2,a15)), % 118.52/118.56 inference(scs_inference,[],[385,140,2,171,190,204])). % 118.52/118.56 cnf(401,plain, % 118.52/118.56 (P9(f16(f19(a2)),a15)), % 118.52/118.56 inference(scs_inference,[],[387,140,190,171])). % 118.52/118.56 cnf(1017,plain, % 118.52/118.56 (P7(f16(f19(a15)),f19(a2))), % 118.52/118.56 inference(scs_inference,[],[385,84,171])). % 118.52/118.56 cnf(1018,plain, % 118.52/118.56 (P7(x10181,f19(a2))+~E(f16(f19(a15)),x10181)), % 118.52/118.56 inference(scs_inference,[],[1017,32])). % 118.52/118.56 cnf(1056,plain, % 118.52/118.56 (E(f7(f16(a15)),f7(f16(a2)))), % 118.52/118.56 inference(scs_inference,[],[385,4,5])). % 118.52/118.56 cnf(1058,plain, % 118.52/118.56 (P9(f7(f16(a2)),f16(a15))), % 118.52/118.56 inference(scs_inference,[],[1056,195,191])). % 118.52/118.56 cnf(1061,plain, % 118.52/118.56 (E(f7(f16(a2)),f7(f16(a15)))), % 118.52/118.56 inference(scs_inference,[],[1056,195,191,204,205,2])). % 118.52/118.56 cnf(1067,plain, % 118.52/118.56 (P9(f7(f16(a15)),f16(a2))), % 118.52/118.56 inference(scs_inference,[],[1061,195,86])). % 118.52/118.56 cnf(1124,plain, % 118.52/118.56 (E(f19(f20(a15)),f19(f20(a2)))), % 118.52/118.56 inference(scs_inference,[],[385,6,7])). % 118.52/118.56 cnf(1126,plain, % 118.52/118.56 (P9(f7(f20(a15)),f20(a2))), % 118.52/118.56 inference(scs_inference,[],[1124,194,86])). % 118.52/118.56 cnf(1130,plain, % 118.52/118.56 (E(f19(f20(a2)),f19(f20(a15)))), % 118.52/118.56 inference(scs_inference,[],[1124,194,86,204,205,2])). % 118.52/118.56 cnf(1139,plain, % 118.52/118.56 (P9(f7(f20(a2)),f20(a15))), % 118.52/118.56 inference(scs_inference,[],[1130,194,86])). % 118.52/118.56 cnf(1142,plain, % 118.52/118.56 (P9(x11421,f20(a2))+~E(f7(f20(a15)),x11421)), % 118.52/118.56 inference(scs_inference,[],[1126,1130,194,86,41,24])). % 118.52/118.56 cnf(1151,plain, % 118.52/118.56 (P9(x11511,f20(a15))+~E(f7(f20(a2)),x11511)), % 118.52/118.56 inference(scs_inference,[],[1130,1139,21,22,24])). % 118.52/118.56 cnf(1185,plain, % 118.52/118.56 (E(f9(f3(a15)),f9(f3(a2)))), % 118.52/118.56 inference(scs_inference,[],[385,8,9])). % 118.52/118.56 cnf(1188,plain, % 118.52/118.56 (E(f9(f3(a2)),f9(f3(a15)))), % 118.52/118.56 inference(scs_inference,[],[1185,204,205,2])). % 118.52/118.56 cnf(1373,plain, % 118.52/118.56 (E(f4(a2),f4(a15))), % 118.52/118.56 inference(scs_inference,[],[385,14,2])). % 118.52/118.56 cnf(1375,plain, % 118.52/118.56 (P9(f7(f4(a2)),f4(a15))), % 118.52/118.56 inference(scs_inference,[],[1373,140,190])). % 118.52/118.56 cnf(1376,plain, % 118.52/118.56 (P9(f4(a15),f4(a2))), % 118.52/118.56 inference(scs_inference,[],[1373,140,190,204])). % 118.52/118.56 cnf(1377,plain, % 118.52/118.56 (P9(f4(a2),f4(a15))), % 118.52/118.56 inference(scs_inference,[],[1373,140,190,204,205])). % 118.52/118.56 cnf(1378,plain, % 118.52/118.56 (E(f4(a15),f4(a2))), % 118.52/118.56 inference(scs_inference,[],[1373,140,190,204,205,2])). % 118.52/118.56 cnf(1385,plain, % 118.52/118.56 (P9(f7(f4(a15)),f4(a2))), % 118.52/118.56 inference(scs_inference,[],[1378,140,190])). % 118.52/118.56 cnf(1386,plain, % 118.52/118.56 (P9(x13861,f4(a15))+~E(f7(f4(a2)),x13861)), % 118.52/118.56 inference(scs_inference,[],[1378,1375,140,190,24])). % 118.52/118.56 cnf(1402,plain, % 118.52/118.56 (P9(x14021,f4(a2))+~E(f7(f4(a15)),x14021)), % 118.52/118.56 inference(scs_inference,[],[1373,1385,39,24])). % 118.52/118.56 cnf(2290,plain, % 118.52/118.56 (P11(f7(x22901),f19(x22901))), % 118.52/118.56 inference(scs_inference,[],[55,59,83])). % 118.52/118.56 cnf(2652,plain, % 118.52/118.56 (P11(f7(f16(a15)),f19(f16(a2)))), % 118.52/118.56 inference(scs_inference,[],[2290,1061,35])). % 118.52/118.56 cnf(3465,plain, % 118.52/118.56 (P11(x34651,f19(x34652))+~E(f7(x34652),x34651)), % 118.52/118.56 inference(scs_inference,[],[2290,35])). % 118.52/118.56 cnf(3469,plain, % 118.52/118.56 (P9(x34691,f16(a2))+~E(f7(f16(a15)),x34691)), % 118.52/118.56 inference(scs_inference,[],[1067,24])). % 118.52/118.56 cnf(3473,plain, % 118.52/118.56 (P9(x34731,f16(a15))+~E(f7(f16(a2)),x34731)), % 118.52/118.56 inference(scs_inference,[],[1058,24])). % 118.52/118.56 cnf(3491,plain, % 118.52/118.56 (~P12(f3(f3(a8)))), % 118.52/118.56 inference(scs_inference,[],[347,67])). % 118.52/118.56 cnf(3493,plain, % 118.52/118.56 (P7(f4(a15),f19(f4(a2)))), % 118.52/118.56 inference(scs_inference,[],[1376,347,67,84])). % 118.52/118.56 cnf(3497,plain, % 118.52/118.56 (E(f7(a2),f7(a15))), % 118.52/118.56 inference(scs_inference,[],[1376,347,387,67,84,77,4])). % 118.52/118.56 cnf(3498,plain, % 118.52/118.56 (E(f19(a2),f19(a15))), % 118.52/118.56 inference(scs_inference,[],[1376,347,387,67,84,77,4,6])). % 118.52/118.56 cnf(3499,plain, % 118.52/118.56 (E(f20(a2),f20(a15))), % 118.52/118.56 inference(scs_inference,[],[1376,347,387,67,84,77,4,6,7])). % 118.52/118.56 cnf(3500,plain, % 118.52/118.56 (E(f9(a2),f9(a15))), % 118.52/118.56 inference(scs_inference,[],[1376,347,387,67,84,77,4,6,7,8])). % 118.52/118.56 cnf(3501,plain, % 118.52/118.56 (E(f3(a2),f3(a15))), % 118.52/118.56 inference(scs_inference,[],[1376,347,387,67,84,77,4,6,7,8,9])). % 118.52/118.56 cnf(3502,plain, % 118.52/118.56 (E(f5(a2),f5(a15))), % 118.52/118.56 inference(scs_inference,[],[1376,347,387,67,84,77,4,6,7,8,9,12])). % 118.52/118.56 cnf(3503,plain, % 118.52/118.56 (E(f18(a2),f18(a15))), % 118.52/118.56 inference(scs_inference,[],[1376,347,387,67,84,77,4,6,7,8,9,12,13])). % 118.52/118.56 cnf(3504,plain, % 118.52/118.56 (E(f4(f4(a2)),f4(f4(a15)))), % 118.52/118.56 inference(scs_inference,[],[1376,347,387,1373,67,84,77,4,6,7,8,9,12,13,14])). % 118.52/118.56 cnf(3505,plain, % 118.52/118.56 (E(f17(a2,x35051),f17(a15,x35051))), % 118.52/118.56 inference(scs_inference,[],[1376,347,387,1373,67,84,77,4,6,7,8,9,12,13,14,10])). % 118.52/118.56 cnf(3506,plain, % 118.52/118.56 (E(f17(x35061,a2),f17(x35061,a15))), % 118.52/118.56 inference(scs_inference,[],[1376,347,387,1373,67,84,77,4,6,7,8,9,12,13,14,10,11])). % 118.52/118.56 cnf(3507,plain, % 118.52/118.56 (E(f7(x35071),a15)), % 118.52/118.56 inference(scs_inference,[],[1376,347,387,1373,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60])). % 118.52/118.56 cnf(3509,plain, % 118.52/118.56 (E(f16(a2),f16(a15))), % 118.52/118.56 inference(scs_inference,[],[1376,347,387,1373,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5])). % 118.52/118.56 cnf(3519,plain, % 118.52/118.56 (~P12(f20(a6))), % 118.52/118.56 inference(scs_inference,[],[47,49,57,1376,363,347,43,387,1373,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74])). % 118.52/118.56 cnf(3521,plain, % 118.52/118.56 (~P12(f9(a6))), % 118.52/118.56 inference(scs_inference,[],[47,49,57,1376,363,347,43,387,1373,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74,75])). % 118.52/118.56 cnf(3523,plain, % 118.52/118.56 (P7(f9(a6),f19(f20(a6)))), % 118.52/118.56 inference(scs_inference,[],[47,49,57,1376,363,347,43,387,1373,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74,75,89])). % 118.52/118.56 cnf(3525,plain, % 118.52/118.56 (E(f17(a2,a2),f17(a15,a15))), % 118.52/118.56 inference(scs_inference,[],[47,49,57,1376,363,347,43,387,1373,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74,75,89,3])). % 118.52/118.56 cnf(3526,plain, % 118.52/118.56 (~P7(f19(f16(a2)),f19(a2))), % 118.52/118.56 inference(scs_inference,[],[47,49,57,2652,1376,363,347,43,387,1373,46,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74,75,89,3,92])). % 118.52/118.56 cnf(3529,plain, % 118.52/118.56 (P12(f16(f19(a15)))), % 118.52/118.56 inference(scs_inference,[],[47,49,57,2652,1376,363,347,111,1017,43,387,1373,54,46,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74,75,89,3,92,32,83])). % 118.52/118.56 cnf(3533,plain, % 118.52/118.56 (~E(a2,f3(a8))), % 118.52/118.56 inference(scs_inference,[],[47,49,57,2652,1376,363,347,111,1017,43,387,1373,54,46,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74,75,89,3,92,32,83,20])). % 118.52/118.56 cnf(3534,plain, % 118.52/118.56 (~P12(f4(a1))), % 118.52/118.56 inference(scs_inference,[],[42,47,49,57,2652,1376,363,347,111,1017,43,387,1373,54,56,46,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74,75,89,3,92,32,83,20,78])). % 118.52/118.56 cnf(3536,plain, % 118.52/118.56 (P6(f18(a1),a1)), % 118.52/118.56 inference(scs_inference,[],[42,47,49,57,2652,1376,363,347,111,1017,43,387,1373,54,56,46,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74,75,89,3,92,32,83,20,78,80])). % 118.52/118.56 cnf(3538,plain, % 118.52/118.56 (P10(f5(a1),a1)), % 118.52/118.56 inference(scs_inference,[],[42,47,49,57,2652,1376,363,347,111,1017,43,387,1373,54,56,46,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74,75,89,3,92,32,83,20,78,80,81])). % 118.52/118.56 cnf(3540,plain, % 118.52/118.56 (P10(f4(a1),a1)), % 118.52/118.56 inference(scs_inference,[],[42,47,49,57,2652,1376,363,347,111,1017,43,387,1373,54,56,46,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74,75,89,3,92,32,83,20,78,80,81,82])). % 118.52/118.56 cnf(3542,plain, % 118.52/118.56 (P7(a12,f19(f20(a1)))), % 118.52/118.56 inference(scs_inference,[],[42,47,49,57,2652,1376,363,347,111,1017,43,387,1373,128,54,56,46,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74,75,89,3,92,32,83,20,78,80,81,82,94])). % 118.52/118.56 cnf(3544,plain, % 118.52/118.56 (~P8(f16(f20(a1)),a1,a12)), % 118.52/118.56 inference(scs_inference,[],[42,47,49,57,2652,1376,363,347,136,297,111,152,1017,43,387,1373,128,54,56,46,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74,75,89,3,92,32,83,20,78,80,81,82,94,97])). % 118.52/118.56 cnf(3547,plain, % 118.52/118.56 (P9(a15,f20(a2))), % 118.52/118.56 inference(scs_inference,[],[42,47,49,57,2652,1376,363,347,136,297,111,152,1017,43,387,1373,128,54,56,46,44,51,67,84,77,4,6,7,8,9,12,13,14,10,11,60,5,61,63,62,2,65,74,75,89,3,92,32,83,20,78,80,81,82,94,97,139,1142])). % 118.52/118.56 cnf(3568,plain, % 118.52/118.56 (P9(a15,f20(a15))), % 118.52/118.56 inference(scs_inference,[],[3507,1151])). % 118.52/118.56 cnf(3569,plain, % 118.52/118.56 (E(f7(x35691),a15)), % 118.52/118.56 inference(rename_variables,[],[3507])). % 118.52/118.56 cnf(3570,plain, % 118.52/118.56 (P9(a15,f4(a15))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,1151,1386])). % 118.52/118.56 cnf(3571,plain, % 118.52/118.56 (E(f7(x35711),a15)), % 118.52/118.56 inference(rename_variables,[],[3507])). % 118.52/118.56 cnf(3572,plain, % 118.52/118.56 (P9(a15,f4(a2))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,1151,1386,1402])). % 118.52/118.56 cnf(3573,plain, % 118.52/118.56 (E(f7(x35731),a15)), % 118.52/118.56 inference(rename_variables,[],[3507])). % 118.52/118.56 cnf(3574,plain, % 118.52/118.56 (P9(a15,f16(a2))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,1151,1386,1402,3469])). % 118.52/118.56 cnf(3575,plain, % 118.52/118.56 (E(f7(x35751),a15)), % 118.52/118.56 inference(rename_variables,[],[3507])). % 118.52/118.56 cnf(3576,plain, % 118.52/118.56 (P9(a15,f16(a15))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,1151,1386,1402,3469,3473])). % 118.52/118.56 cnf(3577,plain, % 118.52/118.56 (E(f7(x35771),a15)), % 118.52/118.56 inference(rename_variables,[],[3507])). % 118.52/118.56 cnf(3580,plain, % 118.52/118.56 (E(f16(f19(a15)),a15)), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3547,3529,1151,1386,1402,3469,3473,84,60])). % 118.52/118.56 cnf(3582,plain, % 118.52/118.56 (~P12(f3(f20(a6)))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3519,3547,3529,1151,1386,1402,3469,3473,84,60,67])). % 118.52/118.56 cnf(3584,plain, % 118.52/118.56 (E(f20(f7(x35841)),f20(a15))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3547,3529,1151,1386,1402,3469,3473,84,60,67,7])). % 118.52/118.56 cnf(3585,plain, % 118.52/118.56 (E(f17(f7(x35851),x35852),f17(a15,x35852))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3547,3529,1151,1386,1402,3469,3473,84,60,67,7,10])). % 118.52/118.56 cnf(3586,plain, % 118.52/118.56 (E(f18(f7(x35861)),f18(a15))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3547,3529,1151,1386,1402,3469,3473,84,60,67,7,10,13])). % 118.52/118.56 cnf(3587,plain, % 118.52/118.56 (E(f3(f7(x35871)),f3(a15))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3547,3529,1151,1386,1402,3469,3473,84,60,67,7,10,13,9])). % 118.52/118.56 cnf(3588,plain, % 118.52/118.56 (E(f19(f7(x35881)),f19(a15))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3547,3529,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6])). % 118.52/118.56 cnf(3589,plain, % 118.52/118.56 (E(f7(f7(x35891)),f7(a15))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3547,3529,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4])). % 118.52/118.56 cnf(3590,plain, % 118.52/118.56 (E(f17(x35901,f7(x35902)),f17(x35901,a15))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3547,3529,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11])). % 118.52/118.56 cnf(3591,plain, % 118.52/118.56 (P7(f3(a8),f19(a8))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3547,3529,58,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77])). % 118.52/118.56 cnf(3593,plain, % 118.52/118.56 (E(f9(f7(x35931)),f9(a15))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3547,3529,58,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8])). % 118.52/118.56 cnf(3594,plain, % 118.52/118.56 (E(f4(f7(x35941)),f4(a15))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3547,3529,58,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14])). % 118.52/118.56 cnf(3595,plain, % 118.52/118.56 (E(f5(f7(x35951)),f5(a15))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3547,3529,58,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12])). % 118.52/118.56 cnf(3598,plain, % 118.52/118.56 (E(f16(f7(x35981)),f16(a15))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3547,3529,58,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5])). % 118.52/118.56 cnf(3602,plain, % 118.52/118.56 (~P12(f20(a1))), % 118.52/118.56 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3533,3547,3529,58,297,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74])). % 118.52/118.56 cnf(3604,plain, % 118.52/118.56 (~P12(f9(a1))), % 118.52/118.57 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3533,3547,3529,58,297,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74,75])). % 118.52/118.57 cnf(3606,plain, % 118.52/118.57 (P7(f9(a1),f19(f20(a1)))), % 118.52/118.57 inference(scs_inference,[],[3507,3569,3571,3573,3575,3577,3519,3533,3547,3529,58,297,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74,75,89])). % 118.52/118.57 cnf(3609,plain, % 118.52/118.57 (P7(f7(a15),f19(a2))), % 118.52/118.57 inference(scs_inference,[],[3497,3507,3569,3571,3573,3575,3577,3519,3533,3547,3529,58,297,55,387,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74,75,89,3,32])). % 118.52/118.57 cnf(3614,plain, % 118.52/118.57 (~E(f16(f19(a15)),f20(a6))), % 118.52/118.57 inference(scs_inference,[],[3497,3507,3569,3571,3573,3575,3577,3519,3533,3547,3529,3493,58,297,59,55,387,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74,75,89,3,32,83,20])). % 118.52/118.57 cnf(3615,plain, % 118.52/118.57 (P7(f5(a1),f19(f20(a1)))), % 118.52/118.57 inference(scs_inference,[],[42,3497,3507,3569,3571,3573,3575,3577,3519,3533,3538,3547,3529,3493,58,297,59,55,43,387,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74,75,89,3,32,83,20,94])). % 118.52/118.57 cnf(3617,plain, % 118.52/118.57 (P10(f18(a1),a1)), % 118.52/118.57 inference(scs_inference,[],[42,3497,3507,3569,3571,3573,3575,3577,3519,3533,3536,3538,3547,3529,3493,58,297,59,55,43,387,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74,75,89,3,32,83,20,94,90])). % 118.52/118.57 cnf(3619,plain, % 118.52/118.57 (~P12(f18(a1))), % 118.52/118.57 inference(scs_inference,[],[42,3497,3507,3569,3571,3573,3575,3577,3519,3533,3536,3538,3547,3529,3493,58,297,59,55,43,387,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74,75,89,3,32,83,20,94,90,88])). % 118.52/118.57 cnf(3622,plain, % 118.52/118.57 (P7(a15,f19(a2))), % 118.52/118.57 inference(scs_inference,[],[42,3497,3507,3569,3571,3573,3575,3577,3519,3533,3536,3538,3547,3529,3493,58,297,59,55,43,387,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74,75,89,3,32,83,20,94,90,88,189,1018])). % 118.52/118.57 cnf(3623,plain, % 118.52/118.57 (P7(a15,f19(a15))), % 118.52/118.57 inference(scs_inference,[],[42,3497,3507,3569,3571,3573,3575,3577,3519,3533,3536,3538,3547,3529,3493,58,297,59,55,43,387,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74,75,89,3,32,83,20,94,90,88,189,1018,79])). % 118.52/118.57 cnf(3628,plain, % 118.52/118.57 (P7(f16(f3(a8)),a8)), % 118.52/118.57 inference(scs_inference,[],[42,3497,3507,3569,3571,3573,3575,3577,3519,3533,3536,3538,3547,3529,3493,3544,58,297,59,348,55,43,387,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74,75,89,3,32,83,20,94,90,88,189,1018,79,85,17,93])). % 118.52/118.57 cnf(3631,plain, % 118.52/118.57 (~P6(f16(f19(a15)),a1)), % 118.52/118.57 inference(scs_inference,[],[42,3497,3507,3569,3571,3573,3575,3577,3519,3533,3536,3538,3547,3529,3493,3544,126,58,297,59,348,55,43,1373,387,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74,75,89,3,32,83,20,94,90,88,189,1018,79,85,17,93,36,28])). % 118.52/118.57 cnf(3632,plain, % 118.52/118.57 (P8(f17(a6,f9(a6)),a6,f9(a6))), % 118.52/118.57 inference(scs_inference,[],[42,3497,3507,3569,3571,3573,3575,3577,3519,3521,3533,3536,3538,3547,3529,3493,3523,3544,126,58,49,57,297,59,348,55,43,1373,387,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74,75,89,3,32,83,20,94,90,88,189,1018,79,85,17,93,36,28,96])). % 118.52/118.57 cnf(3634,plain, % 118.52/118.57 (P7(f17(a6,f9(a6)),f20(a6))), % 118.52/118.57 inference(scs_inference,[],[42,3497,3507,3569,3571,3573,3575,3577,3519,3521,3533,3536,3538,3547,3529,3493,3523,3544,126,58,49,57,297,59,348,55,43,1373,387,56,44,1151,1386,1402,3469,3473,84,60,67,7,10,13,9,6,4,11,77,8,14,12,61,5,62,2,74,75,89,3,32,83,20,94,90,88,189,1018,79,85,17,93,36,28,96,98])). % 118.52/118.57 cnf(3641,plain, % 118.52/118.57 (~P12(f3(f4(a1)))), % 118.52/118.57 inference(scs_inference,[],[3534,3568,84,67])). % 118.52/118.57 cnf(3643,plain, % 118.52/118.57 (P7(f3(a12),f19(a12))), % 118.52/118.57 inference(scs_inference,[],[3534,3568,136,84,67,77])). % 118.52/118.57 cnf(3645,plain, % 118.52/118.57 (E(f17(a15,x36451),f17(a2,x36451))), % 118.52/118.57 inference(scs_inference,[],[3534,3568,136,385,84,67,77,10])). % 118.52/118.57 cnf(3646,plain, % 118.52/118.57 (E(f3(a15),f3(a2))), % 118.52/118.57 inference(scs_inference,[],[3534,3568,136,385,84,67,77,10,9])). % 118.52/118.57 cnf(3647,plain, % 118.52/118.57 (E(f9(a15),f9(a2))), % 118.52/118.57 inference(scs_inference,[],[3534,3568,136,385,84,67,77,10,9,8])). % 118.52/118.57 cnf(3648,plain, % 118.52/118.57 (E(f19(a15),f19(a2))), % 118.52/118.57 inference(scs_inference,[],[3534,3568,136,385,84,67,77,10,9,8,6])). % 118.52/118.57 cnf(3649,plain, % 118.52/118.57 (E(f20(a15),f20(a2))), % 118.52/118.57 inference(scs_inference,[],[3534,3568,136,385,84,67,77,10,9,8,6,7])). % 118.52/118.57 cnf(3650,plain, % 118.52/118.57 (E(f18(a15),f18(a2))), % 118.52/118.57 inference(scs_inference,[],[3534,3568,136,385,84,67,77,10,9,8,6,7,13])). % 118.52/118.57 cnf(3651,plain, % 118.52/118.57 (E(f7(a15),f7(a2))), % 118.52/118.57 inference(scs_inference,[],[3534,3568,136,385,84,67,77,10,9,8,6,7,13,4])). % 118.52/118.57 cnf(3652,plain, % 118.52/118.57 (E(f17(x36521,a15),f17(x36521,a2))), % 118.52/118.57 inference(scs_inference,[],[3534,3568,136,385,84,67,77,10,9,8,6,7,13,4,11])). % 118.52/118.57 cnf(3653,plain, % 118.52/118.57 (E(f5(a15),f5(a2))), % 118.52/118.57 inference(scs_inference,[],[3534,3568,136,385,84,67,77,10,9,8,6,7,13,4,11,12])). % 118.52/118.57 cnf(3654,plain, % 118.52/118.57 (E(f16(a15),f16(a2))), % 118.52/118.57 inference(scs_inference,[],[3534,3568,136,385,84,67,77,10,9,8,6,7,13,4,11,12,5])). % 118.52/118.57 cnf(3658,plain, % 118.52/118.57 (E(f17(f7(x36581),a2),f17(a15,a15))), % 118.52/118.57 inference(scs_inference,[],[3506,3498,3534,3568,3585,3614,136,2290,385,84,67,77,10,9,8,6,7,13,4,11,12,5,2,36,3])). % 118.52/118.57 cnf(3661,plain, % 118.52/118.57 (~P7(f19(f16(a2)),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[3506,3498,3534,3568,3585,3614,3526,136,2290,385,84,67,77,10,9,8,6,7,13,4,11,12,5,2,36,3,33])). % 118.52/118.57 cnf(3663,plain, % 118.52/118.57 (P12(f16(f19(a2)))), % 118.52/118.57 inference(scs_inference,[],[3506,3498,3534,3568,3585,3614,3631,3526,3536,136,156,2290,54,385,84,67,77,10,9,8,6,7,13,4,11,12,5,2,36,3,33,28,83])). % 118.52/118.57 cnf(3665,plain, % 118.52/118.57 (P7(f16(x36651),x36651)), % 118.52/118.57 inference(rename_variables,[],[54])). % 118.52/118.57 cnf(3668,plain, % 118.52/118.57 (~E(f16(f19(a15)),f4(a1))), % 118.52/118.57 inference(scs_inference,[],[3506,3498,3534,3609,3568,3585,3614,3631,3526,3536,136,3529,156,2290,54,385,84,67,77,10,9,8,6,7,13,4,11,12,5,2,36,3,33,28,83,32,20])). % 118.52/118.57 cnf(3669,plain, % 118.52/118.57 (P7(f4(a1),f19(f20(a1)))), % 118.52/118.57 inference(scs_inference,[],[42,3540,3506,3498,3534,3609,3568,3585,3614,3631,3526,3536,136,3529,156,2290,43,54,385,56,84,67,77,10,9,8,6,7,13,4,11,12,5,2,36,3,33,28,83,32,20,94])). % 118.52/118.57 cnf(3671,plain, % 118.52/118.57 (P7(f17(a6,f9(a6)),f9(a6))), % 118.52/118.57 inference(scs_inference,[],[42,3540,3506,3498,3534,3609,3568,3585,3614,3632,3631,3526,3536,3521,3523,136,3529,156,2290,49,57,43,54,385,56,84,67,77,10,9,8,6,7,13,4,11,12,5,2,36,3,33,28,83,32,20,94,97])). % 118.52/118.57 cnf(3673,plain, % 118.52/118.57 (P7(f7(a2),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[42,3540,3506,3498,3534,3609,3568,3585,3614,3632,3631,3526,3536,3521,3523,136,3529,156,2290,49,57,43,54,385,56,84,67,77,10,9,8,6,7,13,4,11,12,5,2,36,3,33,28,83,32,20,94,97,79])). % 118.52/118.57 cnf(3676,plain, % 118.52/118.57 (P8(f17(a1,f4(a1)),a1,f4(a1))), % 118.52/118.57 inference(scs_inference,[],[42,3540,3505,3506,3498,3534,3609,3568,3585,3614,3632,3631,3526,3536,3521,3523,136,3529,156,2290,49,57,297,43,54,385,56,84,67,77,10,9,8,6,7,13,4,11,12,5,2,36,3,33,28,83,32,20,94,97,79,29,96])). % 118.52/118.57 cnf(3678,plain, % 118.52/118.57 (P8(f16(f9(a6)),a6,f9(a6))), % 118.52/118.57 inference(scs_inference,[],[42,3540,3505,3506,3498,3534,3609,3568,3585,3614,3632,3631,3526,3536,3521,3523,136,3529,156,2290,49,57,297,43,54,3665,385,56,84,67,77,10,9,8,6,7,13,4,11,12,5,2,36,3,33,28,83,32,20,94,97,79,29,96,95])). % 118.52/118.57 cnf(3685,plain, % 118.52/118.57 (E(f16(f19(a2)),a15)), % 118.52/118.57 inference(scs_inference,[],[3570,3663,84,60])). % 118.52/118.57 cnf(3688,plain, % 118.52/118.57 (~P12(f3(f20(a1)))), % 118.52/118.57 inference(scs_inference,[],[3570,3602,3663,84,60,189,67])). % 118.52/118.57 cnf(3693,plain, % 118.52/118.57 (~P11(f16(f20(a1)),f3(a12))), % 118.52/118.57 inference(scs_inference,[],[3570,3602,3643,3668,3663,152,84,60,189,67,61,2,93])). % 118.52/118.57 cnf(3695,plain, % 118.52/118.57 (~E(a15,f4(a1))), % 118.52/118.57 inference(scs_inference,[],[3570,3602,3643,3668,3663,3580,152,84,60,189,67,61,2,93,3])). % 118.52/118.57 cnf(3696,plain, % 118.52/118.57 (P7(f16(f17(a2,a2)),f17(a15,a15))), % 118.52/118.57 inference(scs_inference,[],[3570,3525,3602,3643,3668,3663,3580,152,54,84,60,189,67,61,2,93,3,33])). % 118.52/118.57 cnf(3701,plain, % 118.52/118.57 (~P6(f16(f19(a2)),a1)), % 118.52/118.57 inference(scs_inference,[],[3570,3525,3591,3602,3643,3668,3663,3580,126,59,152,54,84,60,189,67,61,2,93,3,33,83,28])). % 118.52/118.57 cnf(3702,plain, % 118.52/118.57 (P7(f7(a15),f19(f7(x37021)))), % 118.52/118.57 inference(scs_inference,[],[3570,3525,3591,3602,3643,3589,3668,3663,3580,126,59,152,55,54,84,60,189,67,61,2,93,3,33,83,28,32])). % 118.52/118.57 cnf(3704,plain, % 118.52/118.57 (~E(f16(f19(a2)),f20(a1))), % 118.52/118.57 inference(scs_inference,[],[3570,3525,3591,3602,3643,3589,3668,3663,3580,126,59,152,55,54,84,60,189,67,61,2,93,3,33,83,28,32,20])). % 118.52/118.57 cnf(3705,plain, % 118.52/118.57 (P7(f18(a1),f19(f20(a1)))), % 118.52/118.57 inference(scs_inference,[],[42,3570,3525,3591,3617,3602,3643,3589,3668,3663,3580,126,59,152,55,43,54,56,84,60,189,67,61,2,93,3,33,83,28,32,20,94])). % 118.52/118.57 cnf(3707,plain, % 118.52/118.57 (P7(f16(f9(a6)),f20(a6))), % 118.52/118.57 inference(scs_inference,[],[42,3570,3525,3591,3617,3602,3643,3589,3668,3678,3663,3580,126,3521,3523,59,152,49,57,55,43,54,56,84,60,189,67,61,2,93,3,33,83,28,32,20,94,98])). % 118.52/118.57 cnf(3709,plain, % 118.52/118.57 (P7(f17(a1,f4(a1)),f4(a1))), % 118.52/118.57 inference(scs_inference,[],[42,3570,3525,3591,3617,3602,3643,3589,3668,3678,3676,3663,3669,3580,126,3534,3521,3523,59,152,49,297,57,55,43,54,56,84,60,189,67,61,2,93,3,33,83,28,32,20,94,98,97])). % 118.52/118.57 cnf(3711,plain, % 118.52/118.57 (~P11(f19(a8),f3(a8))), % 118.52/118.57 inference(scs_inference,[],[42,3570,3525,3591,3617,3602,3643,3589,3668,3678,3676,3663,3669,3580,126,3534,3521,3523,59,152,49,297,57,55,43,54,56,84,60,189,67,61,2,93,3,33,83,28,32,20,94,98,97,85])). % 118.52/118.57 cnf(3719,plain, % 118.52/118.57 (~P12(f3(f9(a1)))), % 118.52/118.57 inference(scs_inference,[],[3604,67])). % 118.52/118.57 cnf(3723,plain, % 118.52/118.57 (~E(f4(a1),a15)), % 118.52/118.57 inference(scs_inference,[],[3572,3604,3695,67,84,2])). % 118.52/118.57 cnf(3724,plain, % 118.52/118.57 (E(f17(a15,a15),f17(a2,a2))), % 118.52/118.57 inference(scs_inference,[],[3572,3645,3652,3604,3695,67,84,2,3])). % 118.52/118.57 cnf(3727,plain, % 118.52/118.57 (P11(f7(f7(x37271)),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[3572,3645,3652,3604,3695,3588,2290,67,84,2,3,36])). % 118.52/118.57 cnf(3729,plain, % 118.52/118.57 (~P7(f19(a8),f3(a8))), % 118.52/118.57 inference(scs_inference,[],[3572,3645,3652,3604,3711,3695,3588,2290,347,67,84,2,3,36,83])). % 118.52/118.57 cnf(3733,plain, % 118.52/118.57 (~E(f16(f19(a2)),f9(a1))), % 118.52/118.57 inference(scs_inference,[],[3572,3623,3645,3652,3604,3711,3695,3588,3701,3661,3663,3536,2290,347,67,84,2,3,36,83,28,32,20])). % 118.52/118.57 cnf(3734,plain, % 118.52/118.57 (P8(f17(a1,f9(a1)),a1,f9(a1))), % 118.52/118.57 inference(scs_inference,[],[3572,3623,3645,3652,3604,3711,3695,3588,3606,3701,3661,3663,3536,2290,347,297,56,67,84,2,3,36,83,28,32,20,96])). % 118.52/118.57 cnf(3736,plain, % 118.52/118.57 (P7(f17(a1,f4(a1)),f20(a1))), % 118.52/118.57 inference(scs_inference,[],[3572,3623,3645,3652,3604,3711,3695,3588,3606,3701,3661,3676,3669,3663,3536,3534,2290,347,297,56,67,84,2,3,36,83,28,32,20,96,98])). % 118.52/118.57 cnf(3746,plain, % 118.52/118.57 (~P12(f3(f18(a1)))), % 118.52/118.57 inference(scs_inference,[],[3574,3619,84,67])). % 118.52/118.57 cnf(3749,plain, % 118.52/118.57 (~E(f4(a1),f16(f19(a2)))), % 118.52/118.57 inference(scs_inference,[],[3574,3619,3723,3704,3685,84,67,2,3])). % 118.52/118.57 cnf(3750,plain, % 118.52/118.57 (P11(f17(a6,f9(a6)),f20(a6))), % 118.52/118.57 inference(scs_inference,[],[3574,3619,3723,3634,3704,3685,3519,84,67,2,3,83])). % 118.52/118.57 cnf(3753,plain, % 118.52/118.57 (~E(f16(f19(a2)),f18(a1))), % 118.52/118.57 inference(scs_inference,[],[3574,3619,3723,3634,3704,3702,3651,3685,3519,3663,84,67,2,3,83,32,20])). % 118.52/118.57 cnf(3754,plain, % 118.52/118.57 (P7(f17(a1,f9(a1)),f20(a1))), % 118.52/118.57 inference(scs_inference,[],[3574,3619,3723,3634,3704,3734,3702,3651,3685,3606,3519,3604,3663,297,56,84,67,2,3,83,32,20,98])). % 118.52/118.57 cnf(3764,plain, % 118.52/118.57 (~P12(f3(a12))), % 118.52/118.57 inference(scs_inference,[],[136,67])). % 118.52/118.57 cnf(3771,plain, % 118.52/118.57 (P9(f17(a2,a2),f17(a15,a15))), % 118.52/118.57 inference(scs_inference,[],[3576,3733,3724,136,148,53,67,84,2,25,24])). % 118.52/118.57 cnf(3773,plain, % 118.52/118.57 (~P7(f20(a6),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[3576,3750,3733,3724,136,148,53,45,67,84,2,25,24,92])). % 118.52/118.57 cnf(3775,plain, % 118.52/118.57 (E(f17(a15,f7(x37751)),f17(a2,a2))), % 118.52/118.57 inference(scs_inference,[],[3576,3750,3733,3724,3590,136,148,53,45,67,84,2,25,24,92,3])). % 118.52/118.57 cnf(3779,plain, % 118.52/118.57 (~P7(f20(a6),f19(f7(x37791)))), % 118.52/118.57 inference(scs_inference,[],[3576,3750,3733,3724,3590,3588,136,148,53,156,45,67,84,2,25,24,92,3,36,33])). % 118.52/118.57 cnf(3782,plain, % 118.52/118.57 (~E(f7(a2),f20(a6))), % 118.52/118.57 inference(scs_inference,[],[3576,3673,3693,3750,3733,3724,3590,3588,136,148,53,156,45,67,84,2,25,24,92,3,36,33,83,32])). % 118.52/118.57 cnf(3783,plain, % 118.52/118.57 (~E(a15,f3(f3(a8)))), % 118.52/118.57 inference(scs_inference,[],[3576,3673,3693,3750,3733,3491,3724,3590,3588,136,148,53,156,45,67,84,2,25,24,92,3,36,33,83,32,20])). % 118.52/118.57 cnf(3784,plain, % 118.52/118.57 (~E(f7(a15),f20(a6))), % 118.52/118.57 inference(scs_inference,[],[3576,3673,3693,3750,3733,3491,3724,3590,3588,136,148,53,156,45,67,84,2,25,24,92,3,36,33,83,32,20,195])). % 118.52/118.57 cnf(3785,plain, % 118.52/118.57 (~E(f20(a1),f3(a12))), % 118.52/118.57 inference(scs_inference,[],[3576,3673,3693,3750,3733,3491,3724,3590,3588,136,148,53,156,45,67,84,2,25,24,92,3,36,33,83,32,20,195,140])). % 118.52/118.57 cnf(3789,plain, % 118.52/118.57 (P7(f17(a2,a2),f19(f17(a15,a15)))), % 118.52/118.57 inference(scs_inference,[],[3771,84])). % 118.52/118.57 cnf(3791,plain, % 118.52/118.57 (~P12(f3(f3(a12)))), % 118.52/118.57 inference(scs_inference,[],[3771,3764,84,67])). % 118.52/118.57 cnf(3795,plain, % 118.52/118.57 (P11(f7(f7(x37951)),f19(a2))), % 118.52/118.57 inference(scs_inference,[],[3771,3764,3782,3779,3648,3727,84,67,195,2,36])). % 118.52/118.57 cnf(3798,plain, % 118.52/118.57 (~E(a15,f18(a1))), % 118.52/118.57 inference(scs_inference,[],[3771,3764,3782,3707,3753,3779,3648,3727,3685,3519,84,67,195,2,36,83,3])). % 118.52/118.57 cnf(3800,plain, % 118.52/118.57 (P7(f16(x38001),x38001)), % 118.52/118.57 inference(rename_variables,[],[54])). % 118.52/118.57 cnf(3801,plain, % 118.52/118.57 (P7(f16(a15),f7(x38011))), % 118.52/118.57 inference(scs_inference,[],[3771,3764,3782,3707,3753,3779,3499,3648,3598,3727,3685,3519,54,3800,84,67,195,2,36,83,3,33,32])). % 118.52/118.57 cnf(3803,plain, % 118.52/118.57 (~E(f16(f19(a15)),f3(a12))), % 118.52/118.57 inference(scs_inference,[],[3771,3764,3782,3707,3753,3779,3499,3648,3598,3727,3685,3519,3529,54,3800,84,67,195,2,36,83,3,33,32,20])). % 118.52/118.57 cnf(3804,plain, % 118.52/118.57 (P7(f7(f7(x38041)),f19(a2))), % 118.52/118.57 inference(scs_inference,[],[3771,3764,3782,3707,3753,3779,3499,3648,3598,3727,3685,3519,3529,54,3800,84,67,195,2,36,83,3,33,32,20,79])). % 118.52/118.57 cnf(3815,plain, % 118.52/118.57 (~P12(f3(f9(a6)))), % 118.52/118.57 inference(scs_inference,[],[3521,67])). % 118.52/118.57 cnf(3817,plain, % 118.52/118.57 (P7(f4(a2),f19(f4(a15)))), % 118.52/118.57 inference(scs_inference,[],[1377,3521,67,84])). % 118.52/118.57 cnf(3820,plain, % 118.52/118.57 (E(f17(f7(x38201),a2),f17(a2,a15))), % 118.52/118.57 inference(scs_inference,[],[3785,3658,1377,3645,3521,67,84,2,3])). % 118.52/118.57 cnf(3822,plain, % 118.52/118.57 (~P7(f20(a6),f19(a2))), % 118.52/118.57 inference(scs_inference,[],[3785,3773,3658,1377,3645,3498,3521,67,84,2,3,33])). % 118.52/118.57 cnf(3823,plain, % 118.52/118.57 (~E(a15,f20(a6))), % 118.52/118.57 inference(scs_inference,[],[3622,3785,3773,3658,1377,3645,3498,3521,67,84,2,3,33,32])). % 118.52/118.57 cnf(3824,plain, % 118.52/118.57 (~E(a2,f3(f20(a6)))), % 118.52/118.57 inference(scs_inference,[],[3622,3785,3582,3773,3658,1377,3645,3498,3521,46,67,84,2,3,33,32,20])). % 118.52/118.57 cnf(3834,plain, % 118.52/118.57 (P7(a2,f19(a15))), % 118.52/118.57 inference(scs_inference,[],[390,84])). % 118.52/118.57 cnf(3836,plain, % 118.52/118.57 (~P12(f3(f19(x38361)))), % 118.52/118.57 inference(scs_inference,[],[390,59,84,67])). % 118.52/118.57 cnf(3838,plain, % 118.52/118.57 (~E(f20(a6),f7(a15))), % 118.52/118.57 inference(scs_inference,[],[3784,390,59,84,67,2])). % 118.52/118.57 cnf(3839,plain, % 118.52/118.57 (~E(a2,f18(a1))), % 118.52/118.57 inference(scs_inference,[],[3784,3798,390,59,385,84,67,2,3])). % 118.52/118.57 cnf(3843,plain, % 118.52/118.57 (~E(f16(f19(a2)),f3(a12))), % 118.52/118.57 inference(scs_inference,[],[3784,3798,3801,3501,3654,390,3764,3663,59,54,385,84,67,2,3,33,32,20])). % 118.52/118.57 cnf(3849,plain, % 118.52/118.57 (P7(f16(f19(a2)),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[401,84])). % 118.52/118.57 cnf(3852,plain, % 118.52/118.57 (E(f17(f7(x38521),a2),f17(a2,a2))), % 118.52/118.57 inference(scs_inference,[],[3823,3820,3652,401,84,2,3])). % 118.52/118.57 cnf(3854,plain, % 118.52/118.57 (~E(a2,f20(a6))), % 118.52/118.57 inference(scs_inference,[],[3823,3834,3820,3652,3773,401,84,2,3,32])). % 118.52/118.57 cnf(3855,plain, % 118.52/118.57 (~E(a15,f3(f19(x38551)))), % 118.52/118.57 inference(scs_inference,[],[3823,3834,3836,3820,3652,3773,401,45,84,2,3,32,20])). % 118.52/118.57 cnf(3861,plain, % 118.52/118.57 (P7(x38611,f19(x38611))), % 118.52/118.57 inference(scs_inference,[],[53,84])). % 118.52/118.57 cnf(3863,plain, % 118.52/118.57 (~E(f18(a1),a2)), % 118.52/118.57 inference(scs_inference,[],[3839,53,84,2])). % 118.52/118.57 cnf(3864,plain, % 118.52/118.57 (~E(f19(f19(a8)),f3(a8))), % 118.52/118.57 inference(scs_inference,[],[3839,3729,53,84,2,33])). % 118.52/118.57 cnf(3868,plain, % 118.52/118.57 (~E(f16(f19(a15)),f20(a1))), % 118.52/118.57 inference(scs_inference,[],[3838,3839,3789,3729,3505,3589,3602,53,3529,84,2,33,3,32,20])). % 118.52/118.57 cnf(3877,plain, % 118.52/118.57 (P9(f17(a2,a2),f17(f7(x38771),a2))), % 118.52/118.57 inference(scs_inference,[],[3854,3852,3503,148,53,2,25,24])). % 118.52/118.57 cnf(3879,plain, % 118.52/118.57 (~P7(f19(a2),f19(a2))), % 118.52/118.57 inference(scs_inference,[],[3854,3852,3503,3795,148,53,46,2,25,24,92])). % 118.52/118.57 cnf(3883,plain, % 118.52/118.57 (E(f20(f7(x38831)),f20(a2))), % 118.52/118.57 inference(scs_inference,[],[3854,3852,3503,3649,3584,3795,148,53,54,46,2,25,24,92,33,3])). % 118.52/118.57 cnf(3884,plain, % 118.52/118.57 (~E(f7(x38841),f20(a6))), % 118.52/118.57 inference(scs_inference,[],[3861,3854,3852,3503,3649,3584,3795,3779,148,53,54,46,2,25,24,92,33,3,32])). % 118.52/118.57 cnf(3885,plain, % 118.52/118.57 (P7(x38851,f19(x38851))), % 118.52/118.57 inference(rename_variables,[],[3861])). % 118.52/118.57 cnf(3886,plain, % 118.52/118.57 (~E(a2,f3(f4(a1)))), % 118.52/118.57 inference(scs_inference,[],[3861,3854,3641,3852,3503,3649,3584,3795,3779,148,53,54,46,2,25,24,92,33,3,32,20])). % 118.52/118.57 cnf(3888,plain, % 118.52/118.57 (~E(f7(a2),f19(a2))), % 118.52/118.57 inference(scs_inference,[],[3861,3854,3641,3852,3503,3649,3584,3795,3779,148,53,54,46,2,25,24,92,33,3,32,20,139,195])). % 118.52/118.57 cnf(3890,plain, % 118.52/118.57 (P7(x38901,f19(x38901))), % 118.52/118.57 inference(rename_variables,[],[3861])). % 118.52/118.57 cnf(3893,plain, % 118.52/118.57 (~P11(f20(a6),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[3861,3885,3854,3641,3852,3503,3649,3822,3584,3795,3779,3648,148,53,57,54,46,2,25,24,92,33,3,32,20,139,195,93,34,36])). % 118.52/118.57 cnf(3894,plain, % 118.52/118.57 (P8(f17(a6,f20(a6)),a6,f20(a6))), % 118.52/118.57 inference(scs_inference,[],[3861,3885,3890,3854,3641,3852,3503,3649,3822,3584,3795,3779,3648,3519,148,53,49,57,54,46,2,25,24,92,33,3,32,20,139,195,93,34,36,96])). % 118.52/118.57 cnf(3904,plain, % 118.52/118.57 (~P11(f20(a6),f19(f7(x39041)))), % 118.52/118.57 inference(scs_inference,[],[3884,3893,3588,2,36])). % 118.52/118.57 cnf(3905,plain, % 118.52/118.57 (~P7(f19(a2),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[3884,3879,3893,3588,3648,2,36,33])). % 118.52/118.57 cnf(3907,plain, % 118.52/118.57 (P7(f3(a2),f19(f3(a15)))), % 118.52/118.57 inference(scs_inference,[],[3884,3879,3888,3893,3646,3861,3497,3588,3648,2,36,33,3,32])). % 118.52/118.57 cnf(3908,plain, % 118.52/118.57 (P7(x39081,f19(x39081))), % 118.52/118.57 inference(rename_variables,[],[3861])). % 118.52/118.57 cnf(3909,plain, % 118.52/118.57 (~E(f16(f19(a2)),a8)), % 118.52/118.57 inference(scs_inference,[],[3884,3879,3888,3893,3646,3861,3497,3588,3648,58,3663,2,36,33,3,32,20])). % 118.52/118.57 cnf(3910,plain, % 118.52/118.57 (P7(f17(a6,f20(a6)),f20(a6))), % 118.52/118.57 inference(scs_inference,[],[3884,3879,3888,3893,3894,3646,3861,3908,3497,3588,3648,58,3519,3663,49,57,2,36,33,3,32,20,98])). % 118.52/118.57 cnf(3925,plain, % 118.52/118.57 (~P7(f19(a15),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[3905,3849,3803,3509,3650,3586,3648,59,54,2,83,33,3,32])). % 118.52/118.57 cnf(3926,plain, % 118.52/118.57 (~E(a15,f3(f20(a1)))), % 118.52/118.57 inference(scs_inference,[],[3905,3849,3803,3688,3509,3650,3586,3648,59,54,45,2,83,33,3,32,20])). % 118.52/118.57 cnf(3927,plain, % 118.52/118.57 (P7(f17(a1,f9(a1)),f9(a1))), % 118.52/118.57 inference(scs_inference,[],[3905,3849,3803,3688,3509,3650,3586,3734,3606,3648,3604,59,297,54,56,45,2,83,33,3,32,20,97])). % 118.52/118.57 cnf(3930,plain, % 118.52/118.57 (~E(f7(a15),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[3905,3849,3803,3688,3509,3650,3586,3734,3606,3648,3604,59,297,54,56,45,2,83,33,3,32,20,97,139,195])). % 118.52/118.57 cnf(3937,plain, % 118.52/118.57 (~P7(f19(a15),f19(a2))), % 118.52/118.57 inference(scs_inference,[],[3925,3843,3498,2,33])). % 118.52/118.57 cnf(3939,plain, % 118.52/118.57 (P7(f9(a2),f19(f9(a15)))), % 118.52/118.57 inference(scs_inference,[],[3925,3930,3843,3647,3651,3861,3498,2,33,3,32])). % 118.52/118.57 cnf(3947,plain, % 118.52/118.57 (P11(a15,f19(x39471))), % 118.52/118.57 inference(scs_inference,[],[3507,3465])). % 118.52/118.57 cnf(3948,plain, % 118.52/118.57 (P7(a15,f19(x39481))), % 118.52/118.57 inference(scs_inference,[],[3507,3465,79])). % 118.52/118.57 cnf(3951,plain, % 118.52/118.57 (E(f3(f7(x39511)),f3(a2))), % 118.52/118.57 inference(scs_inference,[],[3864,3587,3646,3507,3465,79,2,3])). % 118.52/118.57 cnf(3954,plain, % 118.52/118.57 (~P7(f19(f7(x39541)),f19(a2))), % 118.52/118.57 inference(scs_inference,[],[3937,3864,3653,3587,3646,3507,3588,54,3465,79,2,3,33,32])). % 118.52/118.57 cnf(3955,plain, % 118.52/118.57 (~E(a15,f3(f9(a1)))), % 118.52/118.57 inference(scs_inference,[],[3937,3864,3719,3653,3587,3646,3507,3588,54,45,3465,79,2,3,33,32,20])). % 118.52/118.57 cnf(3961,plain, % 118.52/118.57 (~E(f18(a1),a15)), % 118.52/118.57 inference(scs_inference,[],[3863,3868,385,2,3])). % 118.52/118.57 cnf(3962,plain, % 118.52/118.57 (~P7(f19(f7(x39621)),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[3863,3954,3868,3648,385,2,3,33])). % 118.52/118.57 cnf(3963,plain, % 118.52/118.57 (P7(f20(a15),f19(f20(a2)))), % 118.52/118.57 inference(scs_inference,[],[3863,3954,3868,3499,3861,3648,385,2,3,33,32])). % 118.52/118.57 cnf(3965,plain, % 118.52/118.57 (~E(f16(f19(a2)),a12)), % 118.52/118.57 inference(scs_inference,[],[3863,3954,3868,3499,3861,3648,136,3663,385,2,3,33,32,20])). % 118.52/118.57 cnf(3972,plain, % 118.52/118.57 (~P7(f19(x39721),f19(a2))), % 118.52/118.57 inference(scs_inference,[],[3749,3947,46,2,92])). % 118.52/118.57 cnf(3976,plain, % 118.52/118.57 (P9(f9(a15),f9(f7(x39761)))), % 118.52/118.57 inference(scs_inference,[],[3749,3947,3593,3500,148,53,46,2,92,25,24])). % 118.52/118.57 cnf(3978,plain, % 118.52/118.57 (E(f9(f7(x39781)),f9(a2))), % 118.52/118.57 inference(scs_inference,[],[3749,3947,3593,3500,3647,148,53,46,2,92,25,24,3])). % 118.52/118.57 cnf(3983,plain, % 118.52/118.57 (~E(a2,f3(f18(a1)))), % 118.52/118.57 inference(scs_inference,[],[3948,3962,3746,3749,3947,3593,3500,3647,148,53,54,46,2,92,25,24,3,33,32,20])). % 118.52/118.57 cnf(3984,plain, % 118.52/118.57 (~E(f16(f19(a2)),f19(x39841))), % 118.52/118.57 inference(scs_inference,[],[3948,3962,3746,3749,3947,3593,3500,3647,148,53,54,46,2,92,25,24,3,33,32,20,139])). % 118.52/118.57 cnf(3985,plain, % 118.52/118.57 (~E(f7(a2),f19(x39851))), % 118.52/118.57 inference(scs_inference,[],[3948,3962,3746,3749,3947,3593,3500,3647,148,53,54,46,2,92,25,24,3,33,32,20,139,195])). % 118.52/118.57 cnf(3991,plain, % 118.52/118.57 (P11(f17(a1,f9(a1)),f9(a1))), % 118.52/118.57 inference(scs_inference,[],[3927,3855,3604,2,83])). % 118.52/118.57 cnf(3994,plain, % 118.52/118.57 (~P7(f19(x39941),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[3972,3985,3927,3855,3497,3604,3648,2,83,3,33])). % 118.52/118.57 cnf(3995,plain, % 118.52/118.57 (P7(f5(a15),f19(f5(a2)))), % 118.52/118.57 inference(scs_inference,[],[3972,3985,3927,3855,3502,3497,3861,3604,3648,2,83,3,33,32])). % 118.52/118.57 cnf(3998,plain, % 118.52/118.57 (~P11(f9(a1),f17(a1,f9(a1)))), % 118.52/118.57 inference(scs_inference,[],[3972,3985,3927,3855,3502,3497,58,3861,3604,3648,3529,2,83,3,33,32,20,85])). % 118.52/118.57 cnf(4007,plain, % 118.52/118.57 (~E(f9(a1),f16(f19(a15)))), % 118.52/118.57 inference(scs_inference,[],[3991,3783,111,2,36])). % 118.52/118.57 cnf(4009,plain, % 118.52/118.57 (E(f4(f7(x40091)),f4(a2))), % 118.52/118.57 inference(scs_inference,[],[3991,3783,3594,111,1378,2,36,3])). % 118.52/118.57 cnf(4010,plain, % 118.52/118.57 (P7(f16(f17(x40101,a2)),f17(x40101,a15))), % 118.52/118.57 inference(scs_inference,[],[3991,3783,3594,3506,111,1378,54,2,36,3,33])). % 118.52/118.57 cnf(4012,plain, % 118.52/118.57 (~E(a15,f3(f3(a12)))), % 118.52/118.57 inference(scs_inference,[],[3991,3791,3783,3594,3506,111,1378,54,45,2,36,3,33,20])). % 118.52/118.57 cnf(4015,plain, % 118.52/118.57 (P7(f18(a2),f19(f18(a15)))), % 118.52/118.57 inference(scs_inference,[],[3991,3791,3783,3594,3650,3506,3589,111,3861,1378,54,56,45,2,36,3,33,20,3465,34,32])). % 118.52/118.57 cnf(4022,plain, % 118.52/118.57 (~E(f16(f19(a15)),f9(a1))), % 118.52/118.57 inference(scs_inference,[],[4007,2])). % 118.52/118.57 cnf(4023,plain, % 118.52/118.57 (~E(a15,f19(x40231))), % 118.52/118.57 inference(scs_inference,[],[3984,4007,3685,2,3])). % 118.52/118.57 cnf(4037,plain, % 118.52/118.57 (E(f5(f7(x40371)),f5(a2))), % 118.52/118.57 inference(scs_inference,[],[3696,3824,3595,3652,3653,2,33,3])). % 118.52/118.57 cnf(4038,plain, % 118.52/118.57 (~E(a15,f3(f9(a6)))), % 118.52/118.57 inference(scs_inference,[],[3696,3815,3824,3595,3652,3653,45,2,33,3,20])). % 118.52/118.57 cnf(4047,plain, % 118.52/118.57 (~E(f16(f19(a15)),a12)), % 118.52/118.57 inference(scs_inference,[],[4023,3910,3886,136,3519,3529,385,2,83,3,20])). % 118.52/118.57 cnf(4050,plain, % 118.52/118.57 (~P11(x40501,f5(f7(x40502)))+P11(x40501,f5(a2))), % 118.52/118.57 inference(scs_inference,[],[4023,3910,4037,3886,136,3519,3529,385,2,83,3,20,85,36])). % 118.52/118.57 cnf(4063,plain, % 118.52/118.57 (E(f17(f7(x40631),f7(x40632)),f17(a15,a15))), % 118.52/118.57 inference(scs_inference,[],[3976,3926,4009,3978,3590,3585,53,2,25,24,3])). % 118.52/118.57 cnf(4066,plain, % 118.52/118.57 (~E(a2,f3(f19(x40661)))), % 118.52/118.57 inference(scs_inference,[],[3976,3926,4009,3978,3836,3590,3585,53,46,2,25,24,3,20])). % 118.52/118.57 cnf(4067,plain, % 118.52/118.57 (P11(f7(a15),f19(a2))), % 118.52/118.57 inference(scs_inference,[],[3976,3926,4009,3978,3836,3590,3585,3497,53,46,2,25,24,3,20,3465])). % 118.52/118.57 cnf(4068,plain, % 118.52/118.57 (P7(f9(a15),f19(f9(a2)))), % 118.52/118.57 inference(scs_inference,[],[3976,3926,4009,3978,3836,3590,3585,3497,53,46,2,25,24,3,20,3465,84])). % 118.52/118.57 cnf(4079,plain, % 118.52/118.57 (~E(a15,f9(a1))), % 118.52/118.57 inference(scs_inference,[],[4067,4022,3736,4066,3580,3602,51,2,92,83,3])). % 118.52/118.57 cnf(4080,plain, % 118.52/118.57 (~P7(f19(a15),f19(f7(x40801)))), % 118.52/118.57 inference(scs_inference,[],[4067,4022,3736,4066,3580,3602,3648,51,2,92,83,3,32])). % 118.52/118.57 cnf(4081,plain, % 118.52/118.57 (~E(f16(f19(a2)),f9(a6))), % 118.52/118.57 inference(scs_inference,[],[4067,4022,3736,4066,3580,3602,3648,3521,3663,51,2,92,83,3,32,20])). % 118.52/118.57 cnf(4093,plain, % 118.52/118.57 (P7(f17(x40931,a2),f19(f17(x40931,a15)))), % 118.52/118.57 inference(scs_inference,[],[4079,4063,4080,3645,3652,3861,195,2,3,32])). % 118.52/118.57 cnf(4107,plain, % 118.52/118.57 (~E(a15,f9(a6))), % 118.52/118.57 inference(scs_inference,[],[4081,3615,3685,59,2,83,3])). % 118.52/118.57 cnf(4119,plain, % 118.52/118.57 (~E(f9(a6),a15)), % 118.52/118.57 inference(scs_inference,[],[4107,2])). % 118.52/118.57 cnf(4121,plain, % 118.52/118.57 (E(f16(f7(x41211)),f16(a2))), % 118.52/118.57 inference(scs_inference,[],[4107,3994,3654,3598,3588,2,33,3])). % 118.52/118.57 cnf(4122,plain, % 118.52/118.57 (P7(f17(a15,a15),f19(f17(a2,a15)))), % 118.52/118.57 inference(scs_inference,[],[4107,4093,3994,3654,3525,3598,3588,2,33,3,32])). % 118.52/118.57 cnf(4133,plain, % 118.52/118.57 (~E(f9(a6),f16(f19(a15)))), % 118.52/118.57 inference(scs_inference,[],[4119,3817,3955,3580,59,2,83,3])). % 118.52/118.57 cnf(4134,plain, % 118.52/118.57 (~P11(f19(f4(a15)),f4(a2))), % 118.52/118.57 inference(scs_inference,[],[4119,3817,3955,3580,59,2,83,3,85])). % 118.52/118.57 cnf(4146,plain, % 118.52/118.57 (E(f17(a15,f7(x41461)),f17(a15,a2))), % 118.52/118.57 inference(scs_inference,[],[4121,4134,3965,3775,3501,3505,148,53,1378,2,24,25,36,3])). % 118.52/118.57 cnf(4152,plain, % 118.52/118.57 (P11(f16(f3(a8)),a8)), % 118.52/118.57 inference(scs_inference,[],[3628,4133,58,2,83])). % 118.52/118.57 cnf(4154,plain, % 118.52/118.57 (~E(f18(a1),f7(x41541))), % 118.52/118.57 inference(scs_inference,[],[3961,3628,4133,3507,58,2,83,3])). % 118.52/118.57 cnf(4162,plain, % 118.52/118.57 (~P7(a8,f19(a15))), % 118.52/118.57 inference(scs_inference,[],[4154,4152,45,2,92])). % 118.52/118.57 cnf(4164,plain, % 118.52/118.57 (~P7(a8,f19(a2))), % 118.52/118.57 inference(scs_inference,[],[4154,4152,3498,45,2,92,33])). % 118.52/118.57 cnf(4165,plain, % 118.52/118.57 (E(f17(f7(x41651),f7(x41652)),f17(a15,a2))), % 118.52/118.57 inference(scs_inference,[],[4154,4146,4152,3585,3498,45,2,92,33,3])). % 118.52/118.57 cnf(4174,plain, % 118.52/118.57 (~E(f3(f18(a1)),a2)), % 118.52/118.57 inference(scs_inference,[],[4164,3983,195,2])). % 118.52/118.57 cnf(4178,plain, % 118.52/118.57 (~P7(a8,f19(f7(x41781)))), % 118.52/118.57 inference(scs_inference,[],[4162,4164,4068,3983,3588,59,195,2,83,33])). % 118.52/118.57 cnf(4181,plain, % 118.52/118.57 (~E(a15,a8)), % 118.52/118.57 inference(scs_inference,[],[4162,4164,4068,3909,3983,3789,3506,3685,3588,59,195,2,83,33,32,3])). % 118.52/118.57 cnf(4182,plain, % 118.52/118.57 (~P11(f19(f9(a2)),f9(a15))), % 118.52/118.57 inference(scs_inference,[],[4162,4164,4068,3909,3983,3789,3506,3685,3588,59,195,2,83,33,32,3,85])). % 118.52/118.57 cnf(4184,plain, % 118.52/118.57 (~P11(x41841,f17(f7(x41842),f7(x41843)))+P11(x41841,f17(a15,a2))), % 118.52/118.57 inference(scs_inference,[],[4162,4164,4165,4068,3909,3983,3789,3506,3685,3588,59,195,2,83,33,32,3,85,36])). % 118.52/118.57 cnf(4195,plain, % 118.52/118.57 (~E(f19(a8),f19(f7(x41951)))), % 118.52/118.57 inference(scs_inference,[],[4178,4012,3861,2,33])). % 118.52/118.57 cnf(4197,plain, % 118.52/118.57 (E(f17(f7(x41971),f7(x41972)),f17(a2,a2))), % 118.52/118.57 inference(scs_inference,[],[4178,4012,4165,3645,3861,2,33,3])). % 118.52/118.57 cnf(4199,plain, % 118.52/118.57 (~E(a15,f3(f4(a1)))), % 118.52/118.57 inference(scs_inference,[],[4178,4012,3641,4165,3645,3861,45,2,33,3,20])). % 118.52/118.57 cnf(4204,plain, % 118.52/118.57 (~E(f19(f7(x42041)),f19(a8))), % 118.52/118.57 inference(scs_inference,[],[4195,2])). % 118.52/118.57 cnf(4208,plain, % 118.52/118.57 (P7(f16(f17(a15,a2)),f17(a2,a2))), % 118.52/118.57 inference(scs_inference,[],[4010,3705,4195,3724,59,2,83,33])). % 118.52/118.57 cnf(4211,plain, % 118.52/118.57 (~P11(f19(f20(a1)),f18(a1))), % 118.52/118.57 inference(scs_inference,[],[4181,4010,3705,4195,3724,59,385,2,83,33,3,85])). % 118.52/118.57 cnf(4226,plain, % 118.52/118.57 (P7(f17(a15,a2),f19(f17(a2,a15)))), % 118.52/118.57 inference(scs_inference,[],[4197,4211,4122,3877,4038,4182,3820,3500,3619,3652,53,2,25,24,83,36,32])). % 118.52/118.57 cnf(4228,plain, % 118.52/118.57 (E(f17(a2,f7(x42281)),f17(a15,a15))), % 118.52/118.57 inference(scs_inference,[],[4197,4211,4122,3877,4038,4182,3820,3590,3505,3500,3619,3652,53,2,25,24,83,36,32,3])). % 118.52/118.57 cnf(4239,plain, % 118.52/118.57 (~E(f19(a15),f19(a8))), % 118.52/118.57 inference(scs_inference,[],[4204,3542,4047,3588,59,2,83,3])). % 118.52/118.57 cnf(4241,plain, % 118.52/118.57 (~P11(f19(f20(a1)),a12)), % 118.52/118.57 inference(scs_inference,[],[4204,3542,4047,3588,59,2,83,3,85])). % 118.52/118.57 cnf(4246,plain, % 118.52/118.57 (~E(f19(a8),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[4239,2])). % 118.52/118.57 cnf(4251,plain, % 118.52/118.57 (~E(f16(a12),f19(f20(a1)))), % 118.52/118.57 inference(scs_inference,[],[4239,4208,4241,3506,136,54,2,83,33,32])). % 118.52/118.57 cnf(4253,plain, % 118.52/118.57 (E(f17(a2,f7(x42531)),f17(a15,a2))), % 118.52/118.57 inference(scs_inference,[],[4239,4208,4241,4146,3506,3505,136,54,2,83,33,32,3])). % 118.52/118.57 cnf(4255,plain, % 118.52/118.57 (~P11(f19(f20(a1)),f3(a12))), % 118.52/118.57 inference(scs_inference,[],[4239,4208,4241,3643,4146,3506,3505,136,54,2,83,33,32,3,93])). % 118.52/118.57 cnf(4257,plain, % 118.52/118.57 (~P11(x42571,f17(f7(x42572),f7(x42573)))+P11(x42571,f17(a2,a2))), % 118.52/118.57 inference(scs_inference,[],[4239,4208,4241,3643,4197,4146,3506,3505,136,54,2,83,33,32,3,93,36])). % 118.52/118.57 cnf(4273,plain, % 118.52/118.57 (~E(f19(a8),f19(a2))), % 118.52/118.57 inference(scs_inference,[],[4246,4226,4251,3948,3498,59,385,2,83,32,3])). % 118.52/118.57 cnf(4274,plain, % 118.52/118.57 (~P11(f19(f17(a2,a15)),f17(a15,a2))), % 118.52/118.57 inference(scs_inference,[],[4246,4226,4251,3948,3498,59,385,2,83,32,3,85])). % 118.52/118.57 cnf(4283,plain, % 118.52/118.57 (~P11(f19(f17(a2,a15)),f17(a15,a15))), % 118.52/118.57 inference(scs_inference,[],[4273,4274,4255,3764,3652,2,83,36])). % 118.52/118.57 cnf(4285,plain, % 118.52/118.57 (E(f17(a2,f7(x42851)),f17(a2,a2))), % 118.52/118.57 inference(scs_inference,[],[4273,4274,4255,4253,3764,3645,3652,2,83,36,3])). % 118.52/118.57 cnf(4287,plain, % 118.52/118.57 (~E(a2,f3(f20(a1)))), % 118.52/118.57 inference(scs_inference,[],[4273,4274,4255,3688,4253,3764,3645,3652,46,2,83,36,3,20])). % 118.52/118.57 cnf(4299,plain, % 118.52/118.57 (P9(f17(a2,a2),f17(a2,f7(x42991)))), % 118.52/118.57 inference(scs_inference,[],[4285,4199,53,2,24])). % 118.52/118.57 cnf(4304,plain, % 118.52/118.57 (E(f17(f7(x43041),a15),f17(a2,a2))), % 118.52/118.57 inference(scs_inference,[],[4283,4285,4199,3852,3502,3525,3652,148,53,2,24,25,36,3])). % 118.52/118.57 cnf(4315,plain, % 118.52/118.57 (~P11(f19(f3(a15)),f3(a2))), % 118.52/118.57 inference(scs_inference,[],[3907,4174,4287,59,385,2,83,3,85])). % 118.52/118.57 cnf(4330,plain, % 118.52/118.57 (~P11(f19(f20(a2)),f20(a15))), % 118.52/118.57 inference(scs_inference,[],[3963,221,59,2,83,85])). % 118.52/118.57 cnf(4338,plain, % 118.52/118.57 (~E(a2,f3(f9(a1)))), % 118.52/118.57 inference(scs_inference,[],[4330,201,3719,3499,46,2,36,20])). % 118.52/118.57 cnf(4360,plain, % 118.52/118.57 (P7(f17(a2,a2),f19(f17(a15,a2)))), % 118.52/118.57 inference(scs_inference,[],[3995,4299,4338,4304,4253,53,59,2,24,25,83,84])). % 118.52/118.57 cnf(4369,plain, % 118.52/118.57 (P7(f17(a15,a15),f19(f17(a15,a2)))), % 118.52/118.57 inference(scs_inference,[],[4360,203,4315,3646,3525,2,36,32])). % 118.52/118.57 cnf(4377,plain, % 118.52/118.57 (~P11(f19(f17(a15,a2)),f17(a15,a15))), % 118.52/118.57 inference(scs_inference,[],[4369,182,59,2,83,85])). % 118.52/118.57 cnf(4399,plain, % 118.52/118.57 (~E(f7(x43991),f3(f18(a1)))), % 118.52/118.57 inference(scs_inference,[],[4015,3746,59,159,51,2,83,20])). % 118.52/118.57 cnf(4400,plain, % 118.52/118.57 (~E(a2,f4(a1))), % 118.52/118.57 inference(scs_inference,[],[4015,3695,3746,59,159,385,51,2,83,20,3])). % 118.52/118.57 cnf(4401,plain, % 118.52/118.57 (~P11(f19(f18(a15)),f18(a2))), % 118.52/118.57 inference(scs_inference,[],[4015,3695,3746,59,159,385,51,2,83,20,3,85])). % 118.52/118.57 cnf(4408,plain, % 118.52/118.57 (~P11(f19(f18(a15)),f18(a15))), % 118.52/118.57 inference(scs_inference,[],[4400,4401,3650,2,36])). % 118.52/118.57 cnf(4414,plain, % 118.52/118.57 (P9(f3(a2),f3(f7(x44141)))), % 118.52/118.57 inference(scs_inference,[],[4399,3951,53,2,24])). % 118.52/118.57 cnf(4451,plain, % 118.52/118.57 (~P11(f19(f9(a15)),f9(a2))), % 118.52/118.57 inference(scs_inference,[],[3939,3791,59,46,83,20,85])). % 118.52/118.57 cnf(4454,plain, % 118.52/118.57 (~P11(f9(a1),x44541)+~E(x44541,f17(a1,f9(a1)))), % 118.52/118.57 inference(scs_inference,[],[3939,3998,3791,59,46,83,20,85,2,36])). % 118.52/118.57 cnf(4461,plain, % 118.52/118.57 (~E(a15,f20(a1))), % 118.52/118.57 inference(scs_inference,[],[4408,4451,3704,3647,3685,36,83,3])). % 118.52/118.57 cnf(4469,plain, % 118.52/118.57 (P11(f17(a6,f9(a6)),f9(a6))), % 118.52/118.57 inference(scs_inference,[],[4414,3671,3649,3587,3521,53,24,25,83])). % 118.52/118.57 cnf(4472,plain, % 118.52/118.57 (P7(f20(a2),f19(f20(a15)))), % 118.52/118.57 inference(scs_inference,[],[4461,4414,3671,3649,3587,3521,53,385,24,25,83,3,84])). % 118.52/118.57 cnf(4474,plain, % 118.52/118.57 (~P11(f9(a6),f17(a6,f9(a6)))), % 118.52/118.57 inference(scs_inference,[],[4461,4414,3671,3649,3587,3521,53,385,24,25,83,3,84,85])). % 118.52/118.57 cnf(4481,plain, % 118.52/118.57 (~P7(f9(a6),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[4469,45,92])). % 118.52/118.57 cnf(4485,plain, % 118.52/118.57 (~E(f7(a15),f9(a6))), % 118.52/118.57 inference(scs_inference,[],[4469,4377,3843,3525,3685,45,92,36,3,195])). % 118.52/118.57 cnf(4498,plain, % 118.52/118.57 (E(f17(a15,f7(x44981)),f17(a2,a15))), % 118.52/118.57 inference(scs_inference,[],[4481,4485,4472,3775,3506,3588,59,2,33,83,3])). % 118.52/118.57 cnf(4503,plain, % 118.52/118.57 (~P11(f9(a6),x45031)+~E(x45031,f17(a6,f9(a6)))), % 118.52/118.57 inference(scs_inference,[],[4481,4485,4474,4472,3775,3506,3588,59,2,33,83,3,85,195,36])). % 118.52/118.57 cnf(4516,plain, % 118.52/118.57 (P11(f17(a1,f9(a1)),f20(a1))), % 118.52/118.57 inference(scs_inference,[],[3754,3602,83])). % 118.52/118.57 cnf(4519,plain, % 118.52/118.57 (E(f17(f7(x45191),a15),f17(a15,a2))), % 118.52/118.57 inference(scs_inference,[],[3754,3815,4304,3505,3602,46,83,20,3])). % 118.52/118.57 cnf(4549,plain, % 118.52/118.57 (P11(f17(a1,f4(a1)),f4(a1))), % 118.52/118.57 inference(scs_inference,[],[4516,3709,3534,45,92,83])). % 118.52/118.57 cnf(4557,plain, % 118.52/118.57 (~P11(x45571,f17(a15,f7(x45572)))+P11(x45571,f17(a2,a15))), % 118.52/118.57 inference(scs_inference,[],[3804,4516,3709,4498,3534,3498,45,92,83,33,32,195,85,2,36])). % 118.52/118.57 cnf(4589,plain, % 118.52/118.57 (~P11(x45891,f17(f7(x45892),a2))+P11(x45891,f17(a2,a15))), % 118.52/118.57 inference(scs_inference,[],[4122,3820,59,83,36])). % 118.52/118.57 cnf(4603,plain, % 118.52/118.57 (P9(f20(a15),f20(f7(x46031)))), % 118.52/118.57 inference(scs_inference,[],[3584,53,24])). % 118.52/118.57 cnf(4652,plain, % 118.52/118.57 (~P11(f19(f17(x46521,a15)),f17(x46521,a2))), % 118.52/118.57 inference(scs_inference,[],[4603,4093,4519,3883,53,59,24,25,83,85])). % 118.52/118.57 cnf(4701,plain, % 118.52/118.57 (P9(f5(a2),f5(f7(x47011)))), % 118.52/118.57 inference(scs_inference,[],[4037,53,24])). % 118.52/118.57 cnf(4712,plain, % 118.52/118.57 (P11(f9(a1),f19(f20(a1)))), % 118.52/118.57 inference(scs_inference,[],[3606,59,83])). % 118.52/118.57 cnf(4725,plain, % 118.52/118.57 (P11(f9(a6),f19(f20(a6)))), % 118.52/118.57 inference(scs_inference,[],[3523,59,83])). % 118.52/118.57 cnf(4728,plain, % 118.52/118.57 (~P11(f19(f20(a6)),f9(a6))), % 118.52/118.57 inference(scs_inference,[],[3523,59,83,85])). % 118.52/118.57 cnf(4735,plain, % 118.52/118.57 (~P7(f19(f20(a6)),f9(a6))), % 118.52/118.57 inference(scs_inference,[],[4728,3521,83])). % 118.52/118.57 cnf(4741,plain, % 118.52/118.57 (P9(f17(a15,a15),f17(f7(x47411),a2))), % 118.52/118.57 inference(scs_inference,[],[3658,53,24])). % 118.52/118.57 cnf(4750,plain, % 118.52/118.57 (P7(f5(a2),f19(f5(a15)))), % 118.52/118.57 inference(scs_inference,[],[4735,4701,3658,3595,3523,1017,3521,49,53,57,59,24,25,83,97,84])). % 118.52/118.57 cnf(4782,plain, % 118.52/118.57 (P7(f17(a15,a15),f19(f17(a2,a2)))), % 118.52/118.57 inference(scs_inference,[],[4750,4741,4253,3852,53,59,24,25,83,84])). % 118.52/118.57 cnf(4784,plain, % 118.52/118.57 (~P11(f19(f5(a15)),f5(a2))), % 118.52/118.57 inference(scs_inference,[],[4750,4741,4253,3852,53,59,24,25,83,84,85])). % 118.52/118.57 cnf(4793,plain, % 118.52/118.57 (P7(f17(a2,a15),f19(f17(a2,a2)))), % 118.52/118.57 inference(scs_inference,[],[4784,4782,3653,3645,36,32])). % 118.52/118.57 cnf(4802,plain, % 118.52/118.57 (~P11(f19(f17(a2,a2)),f17(a2,a15))), % 118.52/118.57 inference(scs_inference,[],[4793,59,83,85])). % 118.52/118.57 cnf(4860,plain, % 118.52/118.57 (P11(x48601,f19(x48601))), % 118.52/118.57 inference(scs_inference,[],[3861,59,83])). % 118.52/118.57 cnf(4877,plain, % 118.52/118.57 (~P11(f19(x48771),x48771)), % 118.52/118.57 inference(scs_inference,[],[4860,85])). % 118.52/118.57 cnf(5027,plain, % 118.52/118.57 (P7(f17(a1,f18(a1)),f18(a1))), % 118.52/118.57 inference(scs_inference,[],[56,4474,3705,3619,297,96,98,83,97])). % 118.52/118.57 cnf(5033,plain, % 118.52/118.57 (P11(f17(a1,f18(a1)),f18(a1))), % 118.52/118.57 inference(scs_inference,[],[5027,3619,83])). % 118.52/118.57 cnf(5042,plain, % 118.52/118.57 (~P7(f18(a1),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[5033,45,92])). % 118.52/118.57 cnf(5181,plain, % 118.52/118.57 (~P7(f9(a1),f19(a15))), % 118.52/118.57 inference(scs_inference,[],[45,3991,92])). % 118.52/118.57 cnf(5187,plain, % 118.52/118.57 (~P7(f9(a1),f19(a2))), % 118.52/118.57 inference(scs_inference,[],[5181,3498,195,33])). % 118.52/118.57 cnf(5194,plain, % 118.52/118.57 (~P7(f9(a1),f19(f7(x51941)))), % 118.52/118.57 inference(scs_inference,[],[5187,5181,3588,195,33])). % 118.52/118.57 cnf(5525,plain, % 118.52/118.57 (P9(f17(a15,x55251),f17(f7(x55252),x55251))), % 118.52/118.57 inference(scs_inference,[],[53,3585,24])). % 118.52/118.57 cnf(5533,plain, % 118.52/118.57 (P9(f17(a2,f7(x55331)),f17(a15,a15))), % 118.52/118.57 inference(scs_inference,[],[53,4228,25])). % 118.52/118.57 cnf(5551,plain, % 118.52/118.57 (P9(x55511,x55511)), % 118.52/118.57 inference(rename_variables,[],[53])). % 118.52/118.57 cnf(5552,plain, % 118.52/118.57 (P9(f17(f7(x55521),f7(x55522)),f17(a2,a2))), % 118.52/118.57 inference(scs_inference,[],[53,5551,4197,3580,24,25])). % 118.52/118.57 cnf(5586,plain, % 118.52/118.57 (P9(f17(f7(x55861),a15),f17(a2,a2))), % 118.52/118.57 inference(scs_inference,[],[5552,3590,3505,25,24])). % 118.52/118.57 cnf(5615,plain, % 118.52/118.57 (P9(f17(a2,f7(x56151)),f17(a2,a2))), % 118.52/118.57 inference(scs_inference,[],[5533,3724,25])). % 118.52/118.57 cnf(5641,plain, % 118.52/118.57 (P9(f17(a15,f7(x56411)),f17(a2,a2))), % 118.52/118.57 inference(scs_inference,[],[5615,3505,24])). % 118.52/118.57 cnf(5691,plain, % 118.52/118.57 (P9(f17(a15,f7(x56911)),f17(a15,a15))), % 118.52/118.57 inference(scs_inference,[],[5641,3525,25])). % 118.52/118.57 cnf(5739,plain, % 118.52/118.57 (~P11(f19(f17(x57391,a15)),f17(x57391,a2))), % 118.52/118.57 inference(rename_variables,[],[4652])). % 118.52/118.57 cnf(5757,plain, % 118.52/118.57 (E(f7(f4(f4(a2))),f7(f4(f4(a15))))), % 118.52/118.57 inference(scs_inference,[],[5691,3504,5194,4725,4712,3746,4652,5739,4784,4454,4503,4257,132,67,4184,4050,84,8,10,77,9,14,2,7,4])). % 118.52/118.57 cnf(5764,plain, % 118.52/118.57 (E(f19(f4(f4(a2))),f19(f4(f4(a15))))), % 118.52/118.57 inference(scs_inference,[],[5691,3504,5194,4725,4712,3746,4652,5739,4784,4454,4503,4257,132,67,4184,4050,84,8,10,77,9,14,2,7,4,12,3465,13,79,11,6])). % 118.52/118.57 cnf(5766,plain, % 118.52/118.57 (E(f16(f4(f4(a2))),f16(f4(f4(a15))))), % 118.52/118.57 inference(scs_inference,[],[5691,3504,5194,4725,4712,3746,4652,5739,4784,4454,4503,4257,132,67,4184,4050,84,8,10,77,9,14,2,7,4,12,3465,13,79,11,6,139,5])). % 118.52/118.57 cnf(5904,plain, % 118.52/118.57 (~P11(f19(x59041),x59041)), % 118.52/118.57 inference(rename_variables,[],[4877])). % 118.52/118.57 cnf(5906,plain, % 118.52/118.57 (~P11(f19(x59061),x59061)), % 118.52/118.57 inference(rename_variables,[],[4877])). % 118.52/118.57 cnf(5925,plain, % 118.52/118.57 (P7(f16(x59251),x59251)), % 118.52/118.57 inference(rename_variables,[],[54])). % 118.52/118.57 cnf(5931,plain, % 118.52/118.57 (P11(f16(a12),a12)), % 118.52/118.57 inference(scs_inference,[],[51,54,5925,1188,3588,3504,3861,3498,3645,3506,136,4802,3606,4860,4877,5904,5906,5194,5586,4549,3736,3904,5757,5764,5766,5525,139,79,2,189,171,86,205,4589,4557,194,204,84,191,87,190,140,36,24,25,35,92,33,3,83])). % 118.52/118.57 cnf(5934,plain, % 118.52/118.57 (P7(f16(a12),f20(a1))), % 118.52/118.57 inference(scs_inference,[],[51,54,5925,1188,3588,3504,3861,3498,3645,3506,136,4802,3606,4860,4877,5904,5906,3542,5194,5586,4549,3736,3904,5757,5764,5766,5525,139,79,2,189,171,86,205,4589,4557,194,204,84,191,87,190,140,36,24,25,35,92,33,3,83,93])). % 118.52/118.57 cnf(6031,plain, % 118.52/118.57 ($false), % 118.52/118.57 inference(scs_inference,[],[3588,3506,4519,3542,5187,5042,5764,5934,5931,79,2,171,205,86,204,84,87]), % 118.52/118.57 ['proof']). % 118.52/118.57 % SZS output end Proof % 118.52/118.57 % Total time :117.870000s %------------------------------------------------------------------------------