%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT310+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 : n017.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:47 EDT 2024 % Result : Theorem 61.13s 61.36s % Output : CNFRefutation 61.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.12 % Problem : LAT310+1 : TPTP v8.2.0. Released v3.4.0. % 0.09/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n017.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 20:45:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.58 start to proof:theBenchmark % 61.13/61.34 %------------------------------------------- % 61.13/61.34 % File :CSE---1.7 % 61.13/61.34 % Problem :theBenchmark % 61.13/61.34 % Transform :cnf % 61.13/61.34 % Format :tptp:raw % 61.13/61.34 % Command :java -jar mcs_scs.jar %d %s % 61.13/61.34 % 61.13/61.34 % Result :Theorem 60.570000s % 61.13/61.34 % Output :CNFRefutation 60.570000s % 61.13/61.34 %------------------------------------------- % 61.13/61.35 %------------------------------------------------------------------------------ % 61.13/61.35 % File : LAT310+1 : TPTP v8.2.0. Released v3.4.0. % 61.13/61.35 % Domain : Lattice Theory % 61.13/61.35 % Problem : Ideals T39 % 61.13/61.35 % Version : [Urb08] axioms : Especial. % 61.13/61.35 % English : % 61.13/61.35 % 61.13/61.35 % Refs : [Ban96] Bancerek (1996), Ideals % 61.13/61.35 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 61.13/61.35 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 61.13/61.35 % Source : [Urb08] % 61.13/61.35 % Names : t39_filter_2 [Urb08] % 61.13/61.35 % 61.13/61.35 % Status : Theorem % 61.13/61.35 % Rating : 0.33 v8.2.0, 0.31 v8.1.0, 0.28 v7.5.0, 0.34 v7.4.0, 0.23 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.30 v7.0.0, 0.23 v6.4.0, 0.31 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.37 v6.0.0, 0.26 v5.5.0, 0.44 v5.4.0, 0.46 v5.3.0, 0.56 v5.2.0, 0.35 v5.1.0, 0.33 v5.0.0, 0.38 v4.1.0, 0.43 v4.0.0, 0.46 v3.7.0, 0.45 v3.5.0, 0.47 v3.4.0 % 61.13/61.35 % Syntax : Number of formulae : 44 ( 15 unt; 0 def) % 61.13/61.35 % Number of atoms : 136 ( 3 equ) % 61.13/61.35 % Maximal formula atoms : 12 ( 3 avg) % 61.13/61.35 % Number of connectives : 125 ( 33 ~; 1 |; 54 &) % 61.13/61.35 % ( 2 <=>; 35 =>; 0 <=; 0 <~>) % 61.13/61.35 % Maximal formula depth : 12 ( 5 avg) % 61.13/61.35 % Maximal term depth : 3 ( 1 avg) % 61.13/61.35 % Number of predicates : 21 ( 19 usr; 1 prp; 0-2 aty) % 61.13/61.35 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 61.13/61.35 % Number of variables : 67 ( 53 !; 14 ?) % 61.13/61.35 % SPC : FOF_THM_RFO_SEQ % 61.13/61.35 % 61.13/61.35 % Comments : Normal version: includes the axioms (which may be theorems from % 61.13/61.35 % other articles) and background that are possibly necessary. % 61.13/61.35 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 61.13/61.35 % : The problem encoding is based on set theory. % 61.13/61.35 %------------------------------------------------------------------------------ % 61.13/61.35 fof(t39_filter_2,conjecture, % 61.13/61.35 ! [A] : % 61.13/61.35 ( ( ~ v3_struct_0(A) % 61.13/61.35 & v10_lattices(A) % 61.13/61.35 & l3_lattices(A) ) % 61.13/61.35 => ! [B] : % 61.13/61.35 ( ( ~ v1_xboole_0(B) % 61.13/61.35 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 61.13/61.35 => ! [C] : % 61.13/61.35 ( ( ~ v1_xboole_0(C) % 61.13/61.35 & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) ) % 61.13/61.35 => ! [D] : % 61.13/61.35 ( ( ~ v1_xboole_0(D) % 61.13/61.36 & m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) ) % 61.13/61.36 => ( ( r1_tarski(C,D) % 61.13/61.36 => r1_tarski(k19_filter_2(A,C),k19_filter_2(A,D)) ) % 61.13/61.36 & r1_tarski(k19_filter_2(A,k19_filter_2(A,B)),k19_filter_2(A,B)) ) ) ) ) ) ). % 61.13/61.36 % 61.13/61.36 fof(antisymmetry_r2_hidden,axiom, % 61.13/61.36 ! [A,B] : % 61.13/61.36 ( r2_hidden(A,B) % 61.13/61.36 => ~ r2_hidden(B,A) ) ). % 61.13/61.36 % 61.13/61.36 fof(cc1_funct_1,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( v1_xboole_0(A) % 61.13/61.36 => v1_funct_1(A) ) ). % 61.13/61.36 % 61.13/61.36 fof(cc1_lattices,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( l3_lattices(A) % 61.13/61.36 => ( ( ~ v3_struct_0(A) % 61.13/61.36 & v10_lattices(A) ) % 61.13/61.36 => ( ~ v3_struct_0(A) % 61.13/61.36 & v4_lattices(A) % 61.13/61.36 & v5_lattices(A) % 61.13/61.36 & v6_lattices(A) % 61.13/61.36 & v7_lattices(A) % 61.13/61.36 & v8_lattices(A) % 61.13/61.36 & v9_lattices(A) ) ) ) ). % 61.13/61.36 % 61.13/61.36 fof(cc2_lattices,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( l3_lattices(A) % 61.13/61.36 => ( ( ~ v3_struct_0(A) % 61.13/61.36 & v4_lattices(A) % 61.13/61.36 & v5_lattices(A) % 61.13/61.36 & v6_lattices(A) % 61.13/61.36 & v7_lattices(A) % 61.13/61.36 & v8_lattices(A) % 61.13/61.36 & v9_lattices(A) ) % 61.13/61.36 => ( ~ v3_struct_0(A) % 61.13/61.36 & v10_lattices(A) ) ) ) ). % 61.13/61.36 % 61.13/61.36 fof(d11_filter_2,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( ( ~ v3_struct_0(A) % 61.13/61.36 & v10_lattices(A) % 61.13/61.36 & l3_lattices(A) ) % 61.13/61.36 => ! [B] : % 61.13/61.36 ( ( ~ v1_xboole_0(B) % 61.13/61.36 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 61.13/61.36 => ! [C] : % 61.13/61.36 ( m2_filter_2(C,A) % 61.13/61.36 => ( C = k19_filter_2(A,B) % 61.13/61.36 <=> ( r1_tarski(B,C) % 61.13/61.36 & ! [D] : % 61.13/61.36 ( m2_filter_2(D,A) % 61.13/61.36 => ( r1_tarski(B,D) % 61.13/61.36 => r1_tarski(C,D) ) ) ) ) ) ) ) ). % 61.13/61.36 % 61.13/61.36 fof(dt_k19_filter_2,axiom, % 61.13/61.36 ! [A,B] : % 61.13/61.36 ( ( ~ v3_struct_0(A) % 61.13/61.36 & v10_lattices(A) % 61.13/61.36 & l3_lattices(A) % 61.13/61.36 & ~ v1_xboole_0(B) % 61.13/61.36 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 61.13/61.36 => m2_filter_2(k19_filter_2(A,B),A) ) ). % 61.13/61.36 % 61.13/61.36 fof(dt_k1_xboole_0,axiom, % 61.13/61.36 $true ). % 61.13/61.36 % 61.13/61.36 fof(dt_k1_zfmisc_1,axiom, % 61.13/61.36 $true ). % 61.13/61.36 % 61.13/61.36 fof(dt_l1_lattices,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( l1_lattices(A) % 61.13/61.36 => l1_struct_0(A) ) ). % 61.13/61.36 % 61.13/61.36 fof(dt_l1_struct_0,axiom, % 61.13/61.36 $true ). % 61.13/61.36 % 61.13/61.36 fof(dt_l2_lattices,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( l2_lattices(A) % 61.13/61.36 => l1_struct_0(A) ) ). % 61.13/61.36 % 61.13/61.36 fof(dt_l3_lattices,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( l3_lattices(A) % 61.13/61.36 => ( l1_lattices(A) % 61.13/61.36 & l2_lattices(A) ) ) ). % 61.13/61.36 % 61.13/61.36 fof(dt_m1_subset_1,axiom, % 61.13/61.36 $true ). % 61.13/61.36 % 61.13/61.36 fof(dt_m2_filter_2,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( ( ~ v3_struct_0(A) % 61.13/61.36 & v10_lattices(A) % 61.13/61.36 & l3_lattices(A) ) % 61.13/61.36 => ! [B] : % 61.13/61.36 ( m2_filter_2(B,A) % 61.13/61.36 => ( ~ v1_xboole_0(B) % 61.13/61.36 & m2_lattice4(B,A) ) ) ) ). % 61.13/61.36 % 61.13/61.36 fof(dt_m2_lattice4,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( ( ~ v3_struct_0(A) % 61.13/61.36 & v10_lattices(A) % 61.13/61.36 & l3_lattices(A) ) % 61.13/61.36 => ! [B] : % 61.13/61.36 ( m2_lattice4(B,A) % 61.13/61.36 => m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ) ). % 61.13/61.36 % 61.13/61.36 fof(dt_u1_struct_0,axiom, % 61.13/61.36 $true ). % 61.13/61.36 % 61.13/61.36 fof(existence_l1_lattices,axiom, % 61.13/61.36 ? [A] : l1_lattices(A) ). % 61.13/61.36 % 61.13/61.36 fof(existence_l1_struct_0,axiom, % 61.13/61.36 ? [A] : l1_struct_0(A) ). % 61.13/61.36 % 61.13/61.36 fof(existence_l2_lattices,axiom, % 61.13/61.36 ? [A] : l2_lattices(A) ). % 61.13/61.36 % 61.13/61.36 fof(existence_l3_lattices,axiom, % 61.13/61.36 ? [A] : l3_lattices(A) ). % 61.13/61.36 % 61.13/61.36 fof(existence_m1_subset_1,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ? [B] : m1_subset_1(B,A) ). % 61.13/61.36 % 61.13/61.36 fof(existence_m2_filter_2,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( ( ~ v3_struct_0(A) % 61.13/61.36 & v10_lattices(A) % 61.13/61.36 & l3_lattices(A) ) % 61.13/61.36 => ? [B] : m2_filter_2(B,A) ) ). % 61.13/61.36 % 61.13/61.36 fof(existence_m2_lattice4,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( ( ~ v3_struct_0(A) % 61.13/61.36 & v10_lattices(A) % 61.13/61.36 & l3_lattices(A) ) % 61.13/61.36 => ? [B] : m2_lattice4(B,A) ) ). % 61.13/61.36 % 61.13/61.36 fof(fc1_struct_0,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( ( ~ v3_struct_0(A) % 61.13/61.36 & l1_struct_0(A) ) % 61.13/61.36 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 61.13/61.36 % 61.13/61.36 fof(fc1_subset_1,axiom, % 61.13/61.36 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 61.13/61.36 % 61.13/61.36 fof(fc1_xboole_0,axiom, % 61.13/61.36 v1_xboole_0(k1_xboole_0) ). % 61.13/61.36 % 61.13/61.36 fof(rc1_lattice4,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( ( ~ v3_struct_0(A) % 61.13/61.36 & v10_lattices(A) % 61.13/61.36 & l3_lattices(A) ) % 61.13/61.36 => ? [B] : % 61.13/61.36 ( m2_lattice4(B,A) % 61.13/61.36 & ~ v1_xboole_0(B) ) ) ). % 61.13/61.36 % 61.13/61.36 fof(rc1_subset_1,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( ~ v1_xboole_0(A) % 61.13/61.36 => ? [B] : % 61.13/61.36 ( m1_subset_1(B,k1_zfmisc_1(A)) % 61.13/61.36 & ~ v1_xboole_0(B) ) ) ). % 61.13/61.36 % 61.13/61.36 fof(rc1_xboole_0,axiom, % 61.13/61.36 ? [A] : v1_xboole_0(A) ). % 61.13/61.36 % 61.13/61.36 fof(rc2_subset_1,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ? [B] : % 61.13/61.36 ( m1_subset_1(B,k1_zfmisc_1(A)) % 61.13/61.36 & v1_xboole_0(B) ) ). % 61.13/61.36 % 61.13/61.36 fof(rc2_xboole_0,axiom, % 61.13/61.36 ? [A] : ~ v1_xboole_0(A) ). % 61.13/61.36 % 61.13/61.36 fof(rc3_struct_0,axiom, % 61.13/61.36 ? [A] : % 61.13/61.36 ( l1_struct_0(A) % 61.13/61.36 & ~ v3_struct_0(A) ) ). % 61.13/61.36 % 61.13/61.36 fof(rc5_struct_0,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( ( ~ v3_struct_0(A) % 61.13/61.36 & l1_struct_0(A) ) % 61.13/61.36 => ? [B] : % 61.13/61.36 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 61.13/61.36 & ~ v1_xboole_0(B) ) ) ). % 61.13/61.36 % 61.13/61.36 fof(reflexivity_r1_tarski,axiom, % 61.13/61.36 ! [A,B] : r1_tarski(A,A) ). % 61.13/61.36 % 61.13/61.36 fof(t1_subset,axiom, % 61.13/61.36 ! [A,B] : % 61.13/61.36 ( r2_hidden(A,B) % 61.13/61.36 => m1_subset_1(A,B) ) ). % 61.13/61.36 % 61.13/61.36 fof(t1_xboole_1,axiom, % 61.13/61.36 ! [A,B,C] : % 61.13/61.36 ( ( r1_tarski(A,B) % 61.13/61.36 & r1_tarski(B,C) ) % 61.13/61.36 => r1_tarski(A,C) ) ). % 61.13/61.36 % 61.13/61.36 fof(t2_subset,axiom, % 61.13/61.36 ! [A,B] : % 61.13/61.36 ( m1_subset_1(A,B) % 61.13/61.36 => ( v1_xboole_0(B) % 61.13/61.36 | r2_hidden(A,B) ) ) ). % 61.13/61.36 % 61.13/61.36 fof(t3_subset,axiom, % 61.13/61.36 ! [A,B] : % 61.13/61.36 ( m1_subset_1(A,k1_zfmisc_1(B)) % 61.13/61.36 <=> r1_tarski(A,B) ) ). % 61.13/61.36 % 61.13/61.36 fof(t4_subset,axiom, % 61.13/61.36 ! [A,B,C] : % 61.13/61.36 ( ( r2_hidden(A,B) % 61.13/61.36 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 61.13/61.36 => m1_subset_1(A,C) ) ). % 61.13/61.36 % 61.13/61.36 fof(t5_subset,axiom, % 61.13/61.36 ! [A,B,C] : % 61.13/61.36 ~ ( r2_hidden(A,B) % 61.13/61.36 & m1_subset_1(B,k1_zfmisc_1(C)) % 61.13/61.36 & v1_xboole_0(C) ) ). % 61.13/61.36 % 61.13/61.36 fof(t6_boole,axiom, % 61.13/61.36 ! [A] : % 61.13/61.36 ( v1_xboole_0(A) % 61.13/61.36 => A = k1_xboole_0 ) ). % 61.13/61.36 % 61.13/61.36 fof(t7_boole,axiom, % 61.13/61.36 ! [A,B] : % 61.13/61.36 ~ ( r2_hidden(A,B) % 61.13/61.36 & v1_xboole_0(B) ) ). % 61.13/61.36 % 61.13/61.36 fof(t8_boole,axiom, % 61.13/61.36 ! [A,B] : % 61.13/61.36 ~ ( v1_xboole_0(A) % 61.13/61.36 & A != B % 61.13/61.36 & v1_xboole_0(B) ) ). % 61.13/61.36 % 61.13/61.36 %------------------------------------------------------------------------------ % 61.13/61.36 %------------------------------------------- % 61.13/61.36 % Proof found % 61.13/61.36 % SZS status Theorem for theBenchmark % 61.13/61.36 % SZS output start Proof % 61.13/61.36 %ClaNum:107(EqnAxiom:41) % 61.13/61.36 %VarNum:242(SingletonVarNum:74) % 61.13/61.36 %MaxLitNum:10 % 61.13/61.36 %MaxfuncDepth:2 % 61.13/61.36 %SharedTerms:39 % 61.13/61.36 %goalClause: 42 43 54 55 56 58 60 61 62 102 104 % 61.13/61.36 %singleGoalClaCount:9 % 61.13/61.36 [42]P1(a1) % 61.13/61.36 [43]P2(a1) % 61.13/61.36 [44]P2(a12) % 61.13/61.36 [45]P11(a20) % 61.13/61.36 [46]P11(a2) % 61.13/61.36 [47]P3(a13) % 61.13/61.36 [48]P4(a18) % 61.13/61.36 [49]P4(a8) % 61.13/61.36 [50]P5(a19) % 61.13/61.36 [58]~P13(a1) % 61.13/61.36 [59]~P13(a8) % 61.13/61.36 [60]~P11(a14) % 61.13/61.36 [61]~P11(a15) % 61.13/61.36 [62]~P11(a16) % 61.13/61.36 [63]~P11(a10) % 61.13/61.36 [54]P7(a14,f23(f22(a1))) % 61.13/61.36 [55]P7(a15,f23(f22(a1))) % 61.13/61.36 [56]P7(a16,f23(f22(a1))) % 61.13/61.36 [52]P6(x521,x521) % 61.13/61.36 [51]P11(f9(x511)) % 61.13/61.36 [53]P7(f3(x531),x531) % 61.13/61.36 [57]P7(f9(x571),f23(x571)) % 61.13/61.36 [64]~P11(f23(x641)) % 61.13/61.36 [102]P6(a15,a16)+~P6(f21(a1,f21(a1,a14)),f21(a1,a14)) % 61.13/61.36 [104]~P6(f21(a1,a15),f21(a1,a16))+~P6(f21(a1,f21(a1,a14)),f21(a1,a14)) % 61.13/61.36 [65]~P11(x651)+E(x651,a20) % 61.13/61.36 [66]~P11(x661)+P12(x661) % 61.13/61.37 [67]~P2(x671)+P3(x671) % 61.13/61.37 [68]~P3(x681)+P4(x681) % 61.13/61.37 [69]~P5(x691)+P4(x691) % 61.13/61.37 [70]~P2(x701)+P5(x701) % 61.13/61.37 [72]P11(x721)+~P11(f4(x721)) % 61.13/61.37 [82]P11(x821)+P7(f4(x821),f23(x821)) % 61.13/61.37 [81]~P11(x811)+~P10(x812,x811) % 61.13/61.37 [84]~P10(x841,x842)+P7(x841,x842) % 61.13/61.37 [90]~P10(x902,x901)+~P10(x901,x902) % 61.13/61.37 [89]~P6(x891,x892)+P7(x891,f23(x892)) % 61.13/61.37 [91]P6(x911,x912)+~P7(x911,f23(x912)) % 61.13/61.37 [79]~P4(x791)+P13(x791)+~P11(f22(x791)) % 61.13/61.37 [80]~P4(x801)+P13(x801)+~P11(f11(x801)) % 61.13/61.37 [93]~P4(x931)+P13(x931)+P7(f11(x931),f23(f22(x931))) % 61.13/61.37 [71]~P11(x712)+~P11(x711)+E(x711,x712) % 61.13/61.37 [88]~P7(x882,x881)+P11(x881)+P10(x882,x881) % 61.13/61.37 [96]~P6(x961,x963)+P6(x961,x962)+~P6(x963,x962) % 61.13/61.37 [97]~P11(x971)+~P10(x972,x973)+~P7(x973,f23(x971)) % 61.13/61.37 [98]P7(x981,x982)+~P10(x981,x983)+~P7(x983,f23(x982)) % 61.13/61.37 [73]P14(x731)+~P1(x731)+~P2(x731)+P13(x731) % 61.13/61.37 [74]P15(x741)+~P1(x741)+~P2(x741)+P13(x741) % 61.13/61.37 [75]P16(x751)+~P1(x751)+~P2(x751)+P13(x751) % 61.13/61.37 [76]P17(x761)+~P1(x761)+~P2(x761)+P13(x761) % 61.13/61.37 [77]P18(x771)+~P1(x771)+~P2(x771)+P13(x771) % 61.13/61.37 [78]P19(x781)+~P1(x781)+~P2(x781)+P13(x781) % 61.13/61.37 [83]~P1(x831)+~P2(x831)+P13(x831)+~P11(f5(x831)) % 61.13/61.37 [85]~P1(x851)+~P2(x851)+P13(x851)+P8(f6(x851),x851) % 61.13/61.37 [86]~P1(x861)+~P2(x861)+P13(x861)+P9(f7(x861),x861) % 61.13/61.37 [87]~P1(x871)+~P2(x871)+P13(x871)+P9(f5(x871),x871) % 61.13/61.37 [92]~P1(x921)+~P2(x921)+~P8(x922,x921)+P13(x921)+~P11(x922) % 61.13/61.37 [94]~P1(x941)+~P2(x941)+~P8(x942,x941)+P13(x941)+P9(x942,x941) % 61.13/61.37 [99]~P1(x991)+~P2(x991)+~P9(x992,x991)+P13(x991)+P7(x992,f23(f22(x991))) % 61.13/61.37 [100]~P1(x1001)+~P2(x1001)+P13(x1001)+P11(x1002)+P8(f21(x1001,x1002),x1001)+~P7(x1002,f23(f22(x1001))) % 61.13/61.37 [101]~P1(x1011)+~P2(x1011)+~P8(x1013,x1011)+P13(x1011)+P6(x1012,x1013)+P11(x1012)+~E(x1013,f21(x1011,x1012))+~P7(x1012,f23(f22(x1011))) % 61.13/61.37 [95]P1(x951)+~P2(x951)+~P14(x951)+~P15(x951)+~P16(x951)+~P17(x951)+~P18(x951)+~P19(x951)+P13(x951) % 61.13/61.37 [105]P13(x1052)+P11(x1053)+~P1(x1052)+~P2(x1052)+~P6(x1053,x1051)+~P8(x1051,x1052)+P6(x1053,f17(x1052,x1053,x1051))+E(x1051,f21(x1052,x1053))+~P7(x1053,f23(f22(x1052))) % 61.13/61.37 [106]P13(x1062)+P11(x1063)+~P1(x1062)+~P2(x1062)+~P6(x1063,x1061)+~P8(x1061,x1062)+P8(f17(x1062,x1063,x1061),x1062)+E(x1061,f21(x1062,x1063))+~P7(x1063,f23(f22(x1062))) % 61.13/61.37 [107]P13(x1072)+P11(x1073)+~P1(x1072)+~P2(x1072)+~P6(x1073,x1071)+~P8(x1071,x1072)+~P6(x1071,f17(x1072,x1073,x1071))+E(x1071,f21(x1072,x1073))+~P7(x1073,f23(f22(x1072))) % 61.13/61.37 [103]~P1(x1031)+~P2(x1031)+~P6(x1032,x1034)+~P8(x1033,x1031)+~P8(x1034,x1031)+P13(x1031)+P11(x1032)+P6(x1033,x1034)+~E(x1033,f21(x1031,x1032))+~P7(x1032,f23(f22(x1031))) % 61.13/61.37 %EqnAxiom % 61.13/61.37 [1]E(x11,x11) % 61.13/61.37 [2]E(x22,x21)+~E(x21,x22) % 61.13/61.37 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 61.13/61.37 [4]~E(x41,x42)+E(f9(x41),f9(x42)) % 61.13/61.37 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 61.13/61.37 [6]~E(x61,x62)+E(f22(x61),f22(x62)) % 61.13/61.37 [7]~E(x71,x72)+E(f23(x71),f23(x72)) % 61.13/61.37 [8]~E(x81,x82)+E(f21(x81,x83),f21(x82,x83)) % 61.13/61.37 [9]~E(x91,x92)+E(f21(x93,x91),f21(x93,x92)) % 61.13/61.37 [10]~E(x101,x102)+E(f17(x101,x103,x104),f17(x102,x103,x104)) % 61.13/61.37 [11]~E(x111,x112)+E(f17(x113,x111,x114),f17(x113,x112,x114)) % 61.23/61.37 [12]~E(x121,x122)+E(f17(x123,x124,x121),f17(x123,x124,x122)) % 61.23/61.37 [13]~E(x131,x132)+E(f5(x131),f5(x132)) % 61.23/61.37 [14]~E(x141,x142)+E(f11(x141),f11(x142)) % 61.23/61.37 [15]~E(x151,x152)+E(f4(x151),f4(x152)) % 61.23/61.37 [16]~E(x161,x162)+E(f6(x161),f6(x162)) % 61.23/61.37 [17]~E(x171,x172)+E(f7(x171),f7(x172)) % 61.23/61.37 [18]~P1(x181)+P1(x182)+~E(x181,x182) % 61.23/61.37 [19]~P2(x191)+P2(x192)+~E(x191,x192) % 61.23/61.37 [20]P6(x202,x203)+~E(x201,x202)+~P6(x201,x203) % 61.23/61.37 [21]P6(x213,x212)+~E(x211,x212)+~P6(x213,x211) % 61.23/61.37 [22]~P11(x221)+P11(x222)+~E(x221,x222) % 61.23/61.37 [23]P10(x232,x233)+~E(x231,x232)+~P10(x231,x233) % 61.23/61.37 [24]P10(x243,x242)+~E(x241,x242)+~P10(x243,x241) % 61.23/61.37 [25]~P3(x251)+P3(x252)+~E(x251,x252) % 61.23/61.37 [26]~P4(x261)+P4(x262)+~E(x261,x262) % 61.23/61.37 [27]P7(x272,x273)+~E(x271,x272)+~P7(x271,x273) % 61.23/61.37 [28]P7(x283,x282)+~E(x281,x282)+~P7(x283,x281) % 61.23/61.37 [29]~P5(x291)+P5(x292)+~E(x291,x292) % 61.23/61.37 [30]P9(x302,x303)+~E(x301,x302)+~P9(x301,x303) % 61.23/61.37 [31]P9(x313,x312)+~E(x311,x312)+~P9(x313,x311) % 61.23/61.37 [32]~P13(x321)+P13(x322)+~E(x321,x322) % 61.23/61.37 [33]P8(x332,x333)+~E(x331,x332)+~P8(x331,x333) % 61.23/61.37 [34]P8(x343,x342)+~E(x341,x342)+~P8(x343,x341) % 61.23/61.37 [35]~P18(x351)+P18(x352)+~E(x351,x352) % 61.23/61.37 [36]~P14(x361)+P14(x362)+~E(x361,x362) % 61.23/61.37 [37]~P19(x371)+P19(x372)+~E(x371,x372) % 61.23/61.37 [38]~P15(x381)+P15(x382)+~E(x381,x382) % 61.23/61.37 [39]~P17(x391)+P17(x392)+~E(x391,x392) % 61.23/61.37 [40]~P12(x401)+P12(x402)+~E(x401,x402) % 61.23/61.37 [41]~P16(x411)+P16(x412)+~E(x411,x412) % 61.23/61.37 % 61.23/61.37 %------------------------------------------- % 61.24/61.38 cnf(108,plain, % 61.24/61.38 (~P2(x1081)+P13(x1081)+P11(x1082)+~P1(x1081)+~P8(f21(x1081,x1082),x1081)+P6(x1082,f21(x1081,x1082))+~P7(x1082,f23(f22(x1081)))), % 61.24/61.38 inference(equality_inference,[],[101])). % 61.24/61.38 cnf(109,plain, % 61.24/61.38 (~P2(x1091)+~P8(x1092,x1091)+P13(x1091)+P11(x1093)+P6(f21(x1091,x1093),x1092)+~P1(x1091)+~P6(x1093,x1092)+~P8(f21(x1091,x1093),x1091)+~P7(x1093,f23(f22(x1091)))), % 61.24/61.38 inference(equality_inference,[],[103])). % 61.24/61.38 cnf(110,plain, % 61.24/61.38 (P6(a14,f22(a1))), % 61.24/61.38 inference(scs_inference,[],[54,91])). % 61.24/61.38 cnf(112,plain, % 61.24/61.38 (~P10(x1121,a20)), % 61.24/61.38 inference(scs_inference,[],[54,45,91,81])). % 61.24/61.38 cnf(114,plain, % 61.24/61.38 (P10(f3(a14),a14)), % 61.24/61.38 inference(scs_inference,[],[60,54,53,45,91,81,88])). % 61.24/61.38 cnf(117,plain, % 61.24/61.38 (~P11(f22(a1))), % 61.24/61.38 inference(scs_inference,[],[60,54,53,45,91,81,88,97])). % 61.24/61.38 cnf(119,plain, % 61.24/61.38 (P7(f3(a14),f22(a1))), % 61.24/61.38 inference(scs_inference,[],[60,54,53,45,91,81,88,97,98])). % 61.24/61.38 cnf(121,plain, % 61.24/61.38 (~E(a14,a20)), % 61.24/61.38 inference(scs_inference,[],[60,54,53,45,91,81,88,97,98,24])). % 61.24/61.38 cnf(134,plain, % 61.24/61.38 (~P8(a20,a1)), % 61.24/61.38 inference(scs_inference,[],[42,43,58,60,54,53,45,91,81,88,97,98,24,73,74,75,76,77,78,92])). % 61.24/61.38 cnf(136,plain, % 61.24/61.38 (P8(f21(a1,a14),a1)), % 61.24/61.38 inference(scs_inference,[],[42,43,58,60,54,53,45,91,81,88,97,98,24,73,74,75,76,77,78,92,100])). % 61.24/61.38 cnf(138,plain, % 61.24/61.38 (P6(a14,f21(a1,a14))), % 61.24/61.38 inference(scs_inference,[],[42,43,58,60,54,53,45,91,81,88,97,98,24,73,74,75,76,77,78,92,100,108])). % 61.24/61.38 cnf(140,plain, % 61.24/61.38 (~P10(a14,f3(a14))), % 61.24/61.38 inference(scs_inference,[],[42,43,58,60,54,53,45,91,81,88,97,98,24,73,74,75,76,77,78,92,100,108,90])). % 61.24/61.38 cnf(142,plain, % 61.24/61.38 (P6(x1421,x1422)+~E(x1422,x1421)), % 61.24/61.38 inference(scs_inference,[],[42,43,58,60,54,52,53,45,91,81,88,97,98,24,73,74,75,76,77,78,92,100,108,90,20])). % 61.24/61.38 cnf(143,plain, % 61.24/61.38 (~E(f21(a1,a14),a20)), % 61.24/61.38 inference(scs_inference,[],[42,43,58,60,54,52,53,45,91,81,88,97,98,24,73,74,75,76,77,78,92,100,108,90,20,33])). % 61.24/61.38 cnf(144,plain, % 61.24/61.38 (P9(f21(a1,a14),a1)), % 61.24/61.38 inference(scs_inference,[],[42,43,58,60,54,52,53,45,91,81,88,97,98,24,73,74,75,76,77,78,92,100,108,90,20,33,94])). % 61.24/61.38 cnf(153,plain, % 61.24/61.38 (~P11(f21(a1,a14))), % 61.24/61.38 inference(scs_inference,[],[143,65])). % 61.24/61.38 cnf(157,plain, % 61.24/61.38 (P6(a15,f22(a1))), % 61.24/61.38 inference(scs_inference,[],[55,143,46,65,81,91])). % 61.24/61.38 cnf(159,plain, % 61.24/61.38 (~P10(x1591,f9(a2))), % 61.24/61.38 inference(scs_inference,[],[55,57,143,46,65,81,91,97])). % 61.24/61.38 cnf(162,plain, % 61.24/61.38 (P10(f3(a15),a15)), % 61.24/61.38 inference(scs_inference,[],[61,55,57,143,46,53,65,81,91,97,88])). % 61.24/61.38 cnf(165,plain, % 61.24/61.38 (~P8(a2,a1)), % 61.24/61.38 inference(scs_inference,[],[42,43,61,55,58,57,143,46,53,65,81,91,97,88,92])). % 61.24/61.38 cnf(167,plain, % 61.24/61.38 (P8(f21(a1,a15),a1)), % 61.24/61.38 inference(scs_inference,[],[42,43,61,55,58,57,143,46,53,65,81,91,97,88,92,100])). % 61.24/61.38 cnf(172,plain, % 61.24/61.38 (P7(f3(a15),f22(a1))), % 61.24/61.38 inference(scs_inference,[],[42,43,61,55,58,144,57,143,46,53,65,81,91,97,88,92,100,90,30,98])). % 61.24/61.38 cnf(177,plain, % 61.24/61.38 (~P11(f21(a1,a15))), % 61.24/61.38 inference(scs_inference,[],[42,43,61,55,58,144,134,112,57,143,46,53,45,65,81,91,97,88,92,100,90,30,98,24,33,71])). % 61.24/61.38 cnf(190,plain, % 61.24/61.38 (~P10(x1901,f9(x1902))), % 61.24/61.38 inference(scs_inference,[],[51,81])). % 61.24/61.38 cnf(192,plain, % 61.24/61.38 (P6(a16,f22(a1))), % 61.24/61.38 inference(scs_inference,[],[56,51,81,91])). % 61.24/61.38 cnf(200,plain, % 61.24/61.38 (~P8(f9(x2001),a1)), % 61.24/61.38 inference(scs_inference,[],[42,43,58,62,56,136,114,159,165,51,53,81,91,88,33,24,92])). % 61.24/61.38 cnf(202,plain, % 61.24/61.38 (P8(f21(a1,a16),a1)), % 61.24/61.38 inference(scs_inference,[],[42,43,58,62,56,136,114,159,165,51,53,81,91,88,33,24,92,100])). % 61.24/61.38 cnf(204,plain, % 61.24/61.38 (~P10(a16,f3(a16))), % 61.24/61.38 inference(scs_inference,[],[42,43,58,62,56,136,114,159,165,51,53,81,91,88,33,24,92,100,90])). % 61.24/61.38 cnf(206,plain, % 61.24/61.38 (P7(f3(a16),f22(a1))), % 61.24/61.38 inference(scs_inference,[],[42,43,58,62,56,136,114,159,165,51,53,81,91,88,33,24,92,100,90,98])). % 61.24/61.38 cnf(212,plain, % 61.24/61.38 (P6(f9(x2121),x2121)), % 61.24/61.38 inference(scs_inference,[],[57,91])). % 61.24/61.38 cnf(214,plain, % 61.24/61.38 (~P10(x2141,f3(f23(a20)))), % 61.24/61.38 inference(scs_inference,[],[57,53,45,91,97])). % 61.24/61.38 cnf(215,plain, % 61.24/61.38 (P7(f3(x2151),x2151)), % 61.24/61.38 inference(rename_variables,[],[53])). % 61.24/61.38 cnf(217,plain, % 61.24/61.38 (P10(f3(a14),f22(a1))), % 61.24/61.38 inference(scs_inference,[],[119,117,57,53,45,91,97,88])). % 61.24/61.38 cnf(224,plain, % 61.24/61.38 (P7(x2241,x2242)+~P10(x2241,f3(f23(x2242)))), % 61.24/61.38 inference(scs_inference,[],[114,136,119,117,200,57,190,53,215,45,91,97,88,33,24,90,98])). % 61.24/61.38 cnf(237,plain, % 61.24/61.38 (P6(f3(f23(x2371)),x2371)), % 61.24/61.38 inference(scs_inference,[],[53,91])). % 61.24/61.38 cnf(238,plain, % 61.24/61.38 (P7(f3(x2381),x2381)), % 61.24/61.38 inference(rename_variables,[],[53])). % 61.24/61.38 cnf(240,plain, % 61.24/61.38 (P6(f9(a16),f22(a1))), % 61.24/61.38 inference(scs_inference,[],[212,192,53,91,96])). % 61.24/61.38 cnf(243,plain, % 61.24/61.38 (~P10(x2431,f3(f23(a2)))), % 61.24/61.38 inference(scs_inference,[],[212,192,46,53,238,91,96,97])). % 61.24/61.38 cnf(251,plain, % 61.24/61.38 (~P11(f21(a1,a16))), % 61.24/61.38 inference(scs_inference,[],[114,212,172,214,202,192,134,117,46,53,238,91,96,97,88,24,33,65])). % 61.24/61.38 cnf(264,plain, % 61.24/61.38 (P10(f3(a16),f22(a1))), % 61.24/61.38 inference(scs_inference,[],[237,206,157,117,96,88])). % 61.24/61.38 cnf(278,plain, % 61.24/61.38 (P6(f9(f9(a16)),f22(a1))), % 61.24/61.38 inference(scs_inference,[],[240,212,96])). % 61.24/61.38 cnf(281,plain, % 61.24/61.38 (P10(f3(f21(a1,a14)),f21(a1,a14))), % 61.24/61.38 inference(scs_inference,[],[240,212,53,153,96,88])). % 61.24/61.38 cnf(318,plain, % 61.24/61.38 (P6(f9(a14),f21(a1,a14))), % 61.24/61.38 inference(scs_inference,[],[212,138,96])). % 61.24/61.38 cnf(321,plain, % 61.24/61.38 (P10(f3(f21(a1,a15)),f21(a1,a15))), % 61.24/61.38 inference(scs_inference,[],[212,138,53,177,96,88])). % 61.24/61.38 cnf(340,plain, % 61.24/61.38 (P6(f3(f23(a16)),f22(a1))), % 61.24/61.38 inference(scs_inference,[],[192,237,96])). % 61.24/61.38 cnf(343,plain, % 61.24/61.38 (P10(f3(a10),a10)), % 61.24/61.38 inference(scs_inference,[],[192,237,53,63,96,88])). % 61.24/61.38 cnf(344,plain, % 61.24/61.38 (P7(f3(x3441),x3441)), % 61.24/61.38 inference(rename_variables,[],[53])). % 61.24/61.38 cnf(350,plain, % 61.24/61.38 (P7(f3(x3501),x3502)+~E(x3501,x3502)), % 61.24/61.38 inference(scs_inference,[],[321,192,237,243,53,344,63,96,88,24,90,28])). % 61.24/61.38 cnf(359,plain, % 61.24/61.38 (P6(f9(f9(a14)),f21(a1,a14))), % 61.24/61.38 inference(scs_inference,[],[318,212,96])). % 61.24/61.38 cnf(362,plain, % 61.24/61.38 (P10(a15,f23(f22(a1)))), % 61.24/61.38 inference(scs_inference,[],[55,318,212,64,96,88])). % 61.24/61.38 cnf(368,plain, % 61.24/61.38 (~P10(f23(f22(a1)),a15)), % 61.24/61.38 inference(scs_inference,[],[55,202,217,318,165,212,214,64,96,88,33,24,90])). % 61.24/61.38 cnf(371,plain, % 61.24/61.38 (~E(f3(a15),f23(f22(a1)))), % 61.24/61.38 inference(scs_inference,[],[55,202,217,340,162,318,165,212,214,64,96,88,33,24,90,20,23])). % 61.24/61.38 cnf(384,plain, % 61.24/61.38 (~P7(f23(f22(a1)),a15)), % 61.24/61.38 inference(scs_inference,[],[61,237,138,368,96,88])). % 61.24/61.38 cnf(397,plain, % 61.24/61.38 (P6(f9(a15),f22(a1))), % 61.24/61.38 inference(scs_inference,[],[157,212,96])). % 61.24/61.38 cnf(437,plain, % 61.24/61.38 (P7(x4371,f23(x4372))+~E(f9(x4372),x4371)), % 61.24/61.38 inference(scs_inference,[],[264,362,192,243,57,24,21,23,20,27])). % 61.24/61.38 cnf(469,plain, % 61.24/61.38 (P6(x4691,f22(a1))+~E(f9(f9(a16)),x4691)), % 61.24/61.38 inference(scs_inference,[],[321,278,359,214,24,21,20])). % 61.24/61.38 cnf(488,plain, % 61.24/61.38 (P6(f3(f23(x4881)),x4882)+~E(x4881,x4882)), % 61.24/61.38 inference(scs_inference,[],[362,237,214,24,21])). % 61.24/61.38 cnf(497,plain, % 61.24/61.38 (P6(f9(x4971),x4971)), % 61.24/61.38 inference(rename_variables,[],[212])). % 61.24/61.38 cnf(501,plain, % 61.24/61.38 (P6(f9(x5011),x5012)+~E(x5011,x5012)), % 61.24/61.38 inference(scs_inference,[],[110,343,212,497,243,96,24,21])). % 61.24/61.38 cnf(502,plain, % 61.24/61.38 (P6(x5021,x5022)+~E(f9(x5022),x5021)), % 61.24/61.38 inference(scs_inference,[],[110,343,212,497,243,96,24,21,20])). % 61.24/61.38 cnf(508,plain, % 61.24/61.38 (P6(f9(f9(a15)),f22(a1))), % 61.24/61.38 inference(scs_inference,[],[397,212,96])). % 61.24/61.38 cnf(519,plain, % 61.24/61.38 (P6(x5191,f22(a1))+~E(f9(f9(a15)),x5191)), % 61.24/61.38 inference(scs_inference,[],[508,21,20])). % 61.24/61.38 cnf(525,plain, % 61.24/61.38 (P6(x5251,x5252)+~E(x5251,x5252)), % 61.24/61.38 inference(scs_inference,[],[52,21])). % 61.24/61.38 cnf(539,plain, % 61.24/61.38 (P10(a14,f23(f22(a1)))), % 61.24/61.38 inference(scs_inference,[],[54,64,88])). % 61.24/61.38 cnf(542,plain, % 61.24/61.38 (~P10(f23(f22(a1)),a14)), % 61.24/61.38 inference(scs_inference,[],[54,64,88,90])). % 61.24/61.38 cnf(547,plain, % 61.24/61.38 (~P7(f23(f22(a1)),a14)), % 61.24/61.38 inference(scs_inference,[],[60,542,88])). % 61.24/61.38 cnf(557,plain, % 61.24/61.38 (P4(a1)), % 61.24/61.38 inference(scs_inference,[],[43,67,68])). % 61.24/61.38 cnf(607,plain, % 61.24/61.38 (~P11(f4(a14))), % 61.24/61.38 inference(scs_inference,[],[121,72,65])). % 61.24/61.38 cnf(608,plain, % 61.24/61.38 (P10(f3(f4(a14)),f4(a14))), % 61.24/61.38 inference(scs_inference,[],[607,53,88])). % 61.24/61.38 cnf(636,plain, % 61.24/61.38 (E(a20,a2)), % 61.24/61.38 inference(scs_inference,[],[46,2,65])). % 61.24/61.38 cnf(637,plain, % 61.24/61.38 (P6(a2,a20)), % 61.24/61.38 inference(scs_inference,[],[636,142])). % 61.24/61.38 cnf(639,plain, % 61.24/61.38 (P6(f3(f23(a20)),a2)), % 61.24/61.38 inference(scs_inference,[],[636,142,350,488])). % 61.24/61.38 cnf(640,plain, % 61.24/61.38 (P6(f9(a20),a2)), % 61.24/61.38 inference(scs_inference,[],[636,142,350,488,501])). % 61.24/61.38 cnf(642,plain, % 61.24/61.38 (E(a2,a20)), % 61.24/61.38 inference(scs_inference,[],[636,142,350,488,501,525,2])). % 61.24/61.38 cnf(643,plain, % 61.24/61.38 (P6(f3(f23(a2)),a20)), % 61.24/61.38 inference(scs_inference,[],[237,636,142,350,488,501,525,2,96])). % 61.24/61.38 cnf(1086,plain, % 61.24/61.38 (P10(a16,f23(f22(a1)))), % 61.24/61.38 inference(scs_inference,[],[56,64,88])). % 61.24/61.38 cnf(1089,plain, % 61.24/61.38 (~P10(f23(f22(a1)),a16)), % 61.24/61.38 inference(scs_inference,[],[56,64,88,90])). % 61.24/61.38 cnf(1094,plain, % 61.24/61.38 (~P7(f23(f22(a1)),a16)), % 61.24/61.38 inference(scs_inference,[],[62,1089,88])). % 61.24/61.38 cnf(1384,plain, % 61.24/61.38 (P6(a16,f21(a1,a16))), % 61.24/61.38 inference(scs_inference,[],[1086,58,42,202,43,62,84,108])). % 61.24/61.38 cnf(1385,plain, % 61.24/61.38 (P6(f3(f23(a16)),f21(a1,a16))), % 61.24/61.38 inference(scs_inference,[],[237,1384,96])). % 61.24/61.38 cnf(1388,plain, % 61.24/61.38 (P6(x13881,f21(a1,a16))+~E(a16,x13881)), % 61.24/61.38 inference(scs_inference,[],[237,1384,96,20])). % 61.24/61.38 cnf(1396,plain, % 61.24/61.38 (P6(f9(f9(a20)),a2)), % 61.24/61.38 inference(scs_inference,[],[212,640,96])). % 61.24/61.38 cnf(1400,plain, % 61.24/61.38 (P6(x14001,f21(a1,a16))+~E(f3(f23(a16)),x14001)), % 61.24/61.38 inference(scs_inference,[],[212,640,1385,642,96,21,20])). % 61.24/61.38 cnf(1457,plain, % 61.24/61.38 (P7(a2,f23(a20))), % 61.24/61.38 inference(scs_inference,[],[636,89,142])). % 61.24/61.38 cnf(1458,plain, % 61.24/61.38 (P7(a20,f23(a20))), % 61.24/61.38 inference(scs_inference,[],[1457,642,27])). % 61.24/61.38 cnf(1459,plain, % 61.24/61.38 (P7(a2,x14591)+~E(f23(a20),x14591)), % 61.24/61.38 inference(scs_inference,[],[1457,642,27,28])). % 61.24/61.38 cnf(1465,plain, % 61.24/61.38 (P7(a20,x14651)+~E(f23(a20),x14651)), % 61.24/61.38 inference(scs_inference,[],[1458,28])). % 61.24/61.38 cnf(1501,plain, % 61.24/61.38 (P6(f9(a16),f21(a1,a16))), % 61.24/61.38 inference(scs_inference,[],[212,1384,96])). % 61.24/61.38 cnf(1505,plain, % 61.24/61.38 (P6(x15051,f21(a1,a16))+~E(f9(a16),x15051)), % 61.24/61.38 inference(scs_inference,[],[212,1384,96,21,20])). % 61.24/61.38 cnf(1513,plain, % 61.24/61.38 (P6(a15,f21(a1,a15))), % 61.24/61.38 inference(scs_inference,[],[61,55,42,43,58,167,108])). % 61.24/61.38 cnf(1525,plain, % 61.24/61.38 (P6(f9(f9(a16)),f21(a1,a16))), % 61.24/61.38 inference(scs_inference,[],[212,1501,96])). % 61.24/61.38 cnf(1534,plain, % 61.24/61.38 (P6(x15341,f21(a1,a16))+~E(f9(f9(a16)),x15341)), % 61.24/61.38 inference(scs_inference,[],[1525,20])). % 61.24/61.38 cnf(1554,plain, % 61.24/61.38 (E(f9(a2),f9(a20))), % 61.24/61.38 inference(scs_inference,[],[636,4,2])). % 61.24/61.38 cnf(1556,plain, % 61.24/61.38 (E(f9(a20),f9(a2))), % 61.24/61.38 inference(scs_inference,[],[1554,437,2])). % 61.24/61.38 cnf(1557,plain, % 61.24/61.38 (P6(f9(a2),f9(a20))), % 61.24/61.38 inference(scs_inference,[],[1554,437,2,525])). % 61.24/61.38 cnf(1558,plain, % 61.24/61.38 (P6(f9(a20),f9(a2))), % 61.24/61.38 inference(scs_inference,[],[1554,437,2,525,142])). % 61.24/61.38 cnf(1560,plain, % 61.24/61.38 (P6(f9(f9(a2)),f9(a20))), % 61.24/61.38 inference(scs_inference,[],[1554,437,2,525,142,350,501])). % 61.24/61.38 cnf(1562,plain, % 61.24/61.38 (P7(x15621,f9(a20))+~E(f3(f9(a2)),x15621)), % 61.24/61.38 inference(scs_inference,[],[1554,437,2,525,142,350,501,18,27])). % 61.24/61.38 cnf(1568,plain, % 61.24/61.38 (P7(f9(a2),f23(a20))), % 61.24/61.38 inference(scs_inference,[],[1556,437])). % 61.24/61.38 cnf(1569,plain, % 61.24/61.38 (P6(f9(f9(a20)),f9(a2))), % 61.24/61.38 inference(scs_inference,[],[1556,437,501])). % 61.24/61.38 cnf(1576,plain, % 61.24/61.38 (P7(x15761,f9(a2))+~E(f3(f9(a20)),x15761)), % 61.24/61.38 inference(scs_inference,[],[1554,1556,437,501,350,19,32,39,25,41,27])). % 61.24/61.38 cnf(1578,plain, % 61.24/61.38 (P6(f9(a15),f21(a1,a15))), % 61.24/61.38 inference(scs_inference,[],[212,1513,96])). % 61.24/61.38 cnf(1599,plain, % 61.24/61.38 (P6(x15991,f9(a20))+~E(f9(f9(a2)),x15991)), % 61.24/61.38 inference(scs_inference,[],[212,1560,1578,1554,96,36,20])). % 61.24/61.38 cnf(1606,plain, % 61.24/61.38 (P6(x16061,f9(a2))+~E(f9(f9(a20)),x16061)), % 61.24/61.38 inference(scs_inference,[],[1569,1556,36,20])). % 61.24/61.38 cnf(2566,plain, % 61.24/61.38 (E(f6(f17(x25661,a20,x25662)),f6(f17(x25661,a2,x25662)))), % 61.24/61.38 inference(scs_inference,[],[636,16,11])). % 61.24/61.38 cnf(2567,plain, % 61.24/61.38 (E(f6(f17(x25671,a2,x25672)),f6(f17(x25671,a20,x25672)))), % 61.24/61.38 inference(scs_inference,[],[2566,2])). % 61.24/61.38 cnf(2960,plain, % 61.24/61.38 (E(f9(x29601),a20)), % 61.24/61.38 inference(scs_inference,[],[47,1094,1557,607,1556,642,51,44,72,89,82,224,4,5,6,7,13,14,15,16,17,8,10,11,12,70,68,65])). % 61.24/61.38 cnf(2966,plain, % 61.24/61.38 (~P11(f22(a8))), % 61.24/61.38 inference(scs_inference,[],[47,49,59,371,1094,1557,607,1556,642,51,43,44,72,89,82,224,4,5,6,7,13,14,15,16,17,8,10,11,12,70,68,65,67,2,9,79])). % 61.24/61.38 cnf(2968,plain, % 61.24/61.38 (~P11(f11(a8))), % 61.24/61.38 inference(scs_inference,[],[47,49,59,371,1094,1557,607,1556,642,51,43,44,72,89,82,224,4,5,6,7,13,14,15,16,17,8,10,11,12,70,68,65,67,2,9,79,80])). % 61.24/61.38 cnf(2974,plain, % 61.24/61.38 (~E(f9(x29741),f4(a14))), % 61.24/61.38 inference(scs_inference,[],[47,49,59,140,371,1094,1557,607,539,1556,642,51,43,44,72,89,82,224,4,5,6,7,13,14,15,16,17,8,10,11,12,70,68,65,67,2,9,79,80,93,3,24,22])). % 61.24/61.38 cnf(2977,plain, % 61.24/61.38 (P11(f3(f23(a20)))), % 61.24/61.38 inference(scs_inference,[],[47,49,59,140,371,1094,1557,607,539,214,53,1556,642,51,43,44,72,89,82,224,4,5,6,7,13,14,15,16,17,8,10,11,12,70,68,65,67,2,9,79,80,93,3,24,22,97,88])). % 61.24/61.38 cnf(2981,plain, % 61.24/61.38 (~P11(f5(a1))), % 61.24/61.38 inference(scs_inference,[],[42,47,49,59,140,371,1094,1557,607,539,214,53,1556,642,51,58,43,44,72,89,82,224,4,5,6,7,13,14,15,16,17,8,10,11,12,70,68,65,67,2,9,79,80,93,3,24,22,97,88,83])). % 61.24/61.38 cnf(2983,plain, % 61.24/61.38 (P8(f6(a1),a1)), % 61.24/61.38 inference(scs_inference,[],[42,47,49,59,140,371,1094,1557,607,539,214,53,1556,642,51,58,43,44,72,89,82,224,4,5,6,7,13,14,15,16,17,8,10,11,12,70,68,65,67,2,9,79,80,93,3,24,22,97,88,83,85])). % 61.24/61.38 cnf(2985,plain, % 61.24/61.38 (P9(f7(a1),a1)), % 61.24/61.38 inference(scs_inference,[],[42,47,49,59,140,371,1094,1557,607,539,214,53,1556,642,51,58,43,44,72,89,82,224,4,5,6,7,13,14,15,16,17,8,10,11,12,70,68,65,67,2,9,79,80,93,3,24,22,97,88,83,85,86])). % 61.24/61.38 cnf(2987,plain, % 61.24/61.38 (P9(f5(a1),a1)), % 61.24/61.38 inference(scs_inference,[],[42,47,49,59,140,371,1094,1557,607,539,214,53,1556,642,51,58,43,44,72,89,82,224,4,5,6,7,13,14,15,16,17,8,10,11,12,70,68,65,67,2,9,79,80,93,3,24,22,97,88,83,85,86,87])). % 61.24/61.38 cnf(2989,plain, % 61.24/61.38 (P7(f21(a1,a14),f23(f22(a1)))), % 61.24/61.38 inference(scs_inference,[],[42,47,49,59,140,371,1094,1557,607,539,214,53,1556,642,144,51,58,43,44,72,89,82,224,4,5,6,7,13,14,15,16,17,8,10,11,12,70,68,65,67,2,9,79,80,93,3,24,22,97,88,83,85,86,87,99])). % 61.24/61.38 cnf(2991,plain, % 61.24/61.38 (P9(f21(a1,a15),a1)), % 61.24/61.38 inference(scs_inference,[],[42,47,49,59,140,371,1094,1557,607,539,167,214,53,1556,642,144,51,58,43,44,72,89,82,224,4,5,6,7,13,14,15,16,17,8,10,11,12,70,68,65,67,2,9,79,80,93,3,24,22,97,88,83,85,86,87,99,94])). % 61.24/61.38 cnf(2993,plain, % 61.24/61.38 (P6(a20,f22(a1))), % 61.24/61.38 inference(scs_inference,[],[42,47,49,59,140,371,1094,1557,607,539,167,214,53,1556,642,144,51,58,43,44,72,89,82,224,4,5,6,7,13,14,15,16,17,8,10,11,12,70,68,65,67,2,9,79,80,93,3,24,22,97,88,83,85,86,87,99,94,469])). % 61.24/61.38 cnf(2999,plain, % 61.24/61.38 (P7(f3(f21(a1,a14)),f22(a1))), % 61.24/61.38 inference(scs_inference,[],[42,47,49,59,140,371,1094,1557,607,539,167,281,214,2567,53,1556,642,144,51,58,43,44,72,89,82,224,4,5,6,7,13,14,15,16,17,8,10,11,12,70,68,65,67,2,9,79,80,93,3,24,22,97,88,83,85,86,87,99,94,469,69,66,31,98])). % 61.24/61.38 cnf(3014,plain, % 61.24/61.38 (P6(a20,f9(a20))), % 61.24/61.38 inference(scs_inference,[],[2960,1599])). % 61.24/61.38 cnf(3015,plain, % 61.24/61.38 (E(f9(x30151),a20)), % 61.24/61.38 inference(rename_variables,[],[2960])). % 61.24/61.38 cnf(3016,plain, % 61.24/61.38 (P6(a20,f9(a2))), % 61.24/61.38 inference(scs_inference,[],[2960,3015,1599,1606])). % 61.24/61.38 cnf(3017,plain, % 61.24/61.38 (E(f9(x30171),a20)), % 61.24/61.38 inference(rename_variables,[],[2960])). % 61.24/61.38 cnf(3020,plain, % 61.24/61.38 (P7(f4(a10),f23(a10))), % 61.24/61.38 inference(scs_inference,[],[2960,3015,2966,63,1599,1606,72,82])). % 61.24/61.38 cnf(3026,plain, % 61.24/61.38 (E(f23(f9(x30261)),f23(a20))), % 61.24/61.38 inference(scs_inference,[],[2960,3015,3017,2966,2993,63,1599,1606,72,82,89,8,6,7])). % 61.24/61.38 cnf(3029,plain, % 61.24/61.38 (E(f3(f9(x30291)),f3(a20))), % 61.24/61.38 inference(scs_inference,[],[2960,3015,3017,2966,2993,63,1599,1606,72,82,89,8,6,7,17,15,5])). % 61.24/61.38 cnf(3032,plain, % 61.24/61.38 (E(f17(f9(x30321),x30322,x30323),f17(a20,x30322,x30323))), % 61.24/61.38 inference(scs_inference,[],[2960,3015,3017,2966,2993,63,1599,1606,72,82,89,8,6,7,17,15,5,13,14,10])). % 61.24/61.38 cnf(3035,plain, % 61.24/61.38 (E(f17(x30351,x30352,f9(x30353)),f17(x30351,x30352,a20))), % 61.24/61.38 inference(scs_inference,[],[2960,3015,3017,2966,2993,63,1599,1606,72,82,89,8,6,7,17,15,5,13,14,10,16,4,12])). % 61.24/61.38 cnf(3037,plain, % 61.24/61.38 (E(f3(f23(a20)),a20)), % 61.24/61.38 inference(scs_inference,[],[2960,3015,3017,2966,2993,2977,63,1599,1606,72,82,89,8,6,7,17,15,5,13,14,10,16,4,12,11,65])). % 61.24/61.38 cnf(3045,plain, % 61.24/61.38 (~E(a20,f4(a14))), % 61.24/61.38 inference(scs_inference,[],[557,2974,2960,3015,3017,2966,2993,2977,63,58,44,1599,1606,72,82,89,8,6,7,17,15,5,13,14,10,16,4,12,11,65,67,9,2,93,3])). % 61.24/61.38 cnf(3047,plain, % 61.24/61.38 (~P11(f11(a1))), % 61.24/61.38 inference(scs_inference,[],[557,2974,2960,3015,3017,2966,2993,2977,63,58,44,1599,1606,72,82,89,8,6,7,17,15,5,13,14,10,16,4,12,11,65,67,9,2,93,3,80])). % 61.24/61.38 cnf(3049,plain, % 61.24/61.38 (~E(f3(f23(a20)),f22(a8))), % 61.24/61.38 inference(scs_inference,[],[557,2974,2960,3015,3017,2966,2993,2977,63,58,44,1599,1606,72,82,89,8,6,7,17,15,5,13,14,10,16,4,12,11,65,67,9,2,93,3,80,22])). % 61.24/61.38 cnf(3050,plain, % 61.24/61.38 (P6(a2,f22(a1))), % 61.24/61.38 inference(scs_inference,[],[557,2974,2960,3015,3017,2966,2993,2977,637,63,58,44,1599,1606,72,82,89,8,6,7,17,15,5,13,14,10,16,4,12,11,65,67,9,2,93,3,80,22,96])). % 61.24/61.38 cnf(3054,plain, % 61.24/61.38 (P7(f21(a1,a15),f23(f22(a1)))), % 61.24/61.38 inference(scs_inference,[],[42,557,2974,2960,3015,3017,2966,2991,2993,2999,2977,637,63,117,58,43,44,1599,1606,72,82,89,8,6,7,17,15,5,13,14,10,16,4,12,11,65,67,9,2,93,3,80,22,96,88,99])). % 61.24/61.38 cnf(3056,plain, % 61.24/61.38 (~P11(f6(a1))), % 61.24/61.38 inference(scs_inference,[],[42,557,2974,2960,3015,3017,2966,2991,2983,2993,2999,2977,637,63,117,58,43,44,1599,1606,72,82,89,8,6,7,17,15,5,13,14,10,16,4,12,11,65,67,9,2,93,3,80,22,96,88,99,92])). % 61.24/61.38 cnf(3058,plain, % 61.24/61.38 (P6(f9(a20),f22(a1))), % 61.24/61.38 inference(scs_inference,[],[42,557,2974,2960,3015,3017,2966,2991,2983,2993,2999,2977,637,63,117,58,43,44,1599,1606,72,82,89,8,6,7,17,15,5,13,14,10,16,4,12,11,65,67,9,2,93,3,80,22,96,88,99,92,519])). % 61.24/61.38 cnf(3069,plain, % 61.24/61.38 (E(f3(f9(x30691)),f3(a20))), % 61.24/61.38 inference(rename_variables,[],[3029])). % 61.24/61.38 cnf(3072,plain, % 61.24/61.38 (P7(f4(a15),f23(a15))), % 61.24/61.38 inference(scs_inference,[],[3029,3069,61,1562,1576,82])). % 61.24/61.38 cnf(3078,plain, % 61.24/61.38 (E(f22(a2),f22(a20))), % 61.24/61.38 inference(scs_inference,[],[2968,3058,3029,3069,61,642,1562,1576,82,72,89,6])). % 61.24/61.38 cnf(3079,plain, % 61.24/61.38 (E(f21(a2,x30791),f21(a20,x30791))), % 61.24/61.38 inference(scs_inference,[],[2968,3058,3029,3069,61,642,1562,1576,82,72,89,6,8])). % 61.24/61.38 cnf(3080,plain, % 61.24/61.38 (E(f17(a2,x30801,x30802),f17(a20,x30801,x30802))), % 61.24/61.38 inference(scs_inference,[],[2968,3058,3029,3069,61,642,1562,1576,82,72,89,6,8,10])). % 61.24/61.38 cnf(3081,plain, % 61.24/61.38 (E(f23(a2),f23(a20))), % 61.24/61.38 inference(scs_inference,[],[2968,3058,3029,3069,61,642,1562,1576,82,72,89,6,8,10,7])). % 61.24/61.38 cnf(3085,plain, % 61.24/61.38 (E(f4(a2),f4(a20))), % 61.24/61.38 inference(scs_inference,[],[2968,3058,3029,3069,61,642,636,1562,1576,82,72,89,6,8,10,7,17,14,5,15])). % 61.24/61.38 cnf(3086,plain, % 61.24/61.38 (E(f17(x30861,a2,x30862),f17(x30861,a20,x30862))), % 61.24/61.38 inference(scs_inference,[],[2968,3058,3029,3069,61,642,636,1562,1576,82,72,89,6,8,10,7,17,14,5,15,11])). % 61.24/61.38 cnf(3087,plain, % 61.24/61.38 (E(f5(a2),f5(a20))), % 61.24/61.38 inference(scs_inference,[],[2968,3058,3029,3069,61,642,636,1562,1576,82,72,89,6,8,10,7,17,14,5,15,11,13])). % 61.24/61.38 cnf(3089,plain, % 61.24/61.38 (E(f17(x30891,x30892,a2),f17(x30891,x30892,a20))), % 61.24/61.38 inference(scs_inference,[],[2968,3058,3029,3069,61,642,636,1562,1576,82,72,89,6,8,10,7,17,14,5,15,11,13,16,12])). % 61.24/61.38 cnf(3090,plain, % 61.24/61.38 (E(f21(x30901,a2),f21(x30901,a20))), % 61.24/61.38 inference(scs_inference,[],[2968,3058,3029,3069,61,642,636,1562,1576,82,72,89,6,8,10,7,17,14,5,15,11,13,16,12,9])). % 61.24/61.38 cnf(3096,plain, % 61.24/61.38 (~E(f3(f23(a20)),f11(a8))), % 61.24/61.38 inference(scs_inference,[],[204,2968,3058,3045,3032,3035,3029,3069,2977,1086,61,642,636,1562,1576,82,72,89,6,8,10,7,17,14,5,15,11,13,16,12,9,2,24,3,22])). % 61.24/61.38 cnf(3098,plain, % 61.24/61.38 (P11(f3(f23(a2)))), % 61.24/61.38 inference(scs_inference,[],[204,2968,3058,3045,3032,3035,3029,3069,3037,2977,1086,134,61,243,53,642,636,1562,1576,82,72,89,6,8,10,7,17,14,5,15,11,13,16,12,9,2,24,3,22,33,88])). % 61.24/61.38 cnf(3104,plain, % 61.24/61.38 (P9(f6(a1),a1)), % 61.24/61.38 inference(scs_inference,[],[42,204,2985,2968,3058,3045,3032,3035,3029,3069,3037,2983,2977,1086,134,61,243,53,642,58,43,636,1562,1576,82,72,89,6,8,10,7,17,14,5,15,11,13,16,12,9,2,24,3,22,33,88,99,94])). % 61.24/61.38 cnf(3113,plain, % 61.24/61.38 (P7(f4(a16),f23(a16))), % 61.24/61.38 inference(scs_inference,[],[2981,62,72,82])). % 61.24/61.38 cnf(3117,plain, % 61.24/61.38 (E(f21(a20,x31171),f21(a2,x31171))), % 61.24/61.38 inference(scs_inference,[],[3014,2981,62,636,72,82,89,8])). % 61.24/61.38 cnf(3118,plain, % 61.24/61.38 (E(f22(a20),f22(a2))), % 61.24/61.38 inference(scs_inference,[],[3014,2981,62,636,72,82,89,8,6])). % 61.24/61.38 cnf(3119,plain, % 61.24/61.38 (E(f17(a20,x31191,x31192),f17(a2,x31191,x31192))), % 61.24/61.38 inference(scs_inference,[],[3014,2981,62,636,72,82,89,8,6,10])). % 61.24/61.38 cnf(3120,plain, % 61.24/61.38 (E(f23(a20),f23(a2))), % 61.24/61.38 inference(scs_inference,[],[3014,2981,62,636,72,82,89,8,6,10,7])). % 61.24/61.38 cnf(3121,plain, % 61.24/61.38 (E(f17(x31211,a20,x31212),f17(x31211,a2,x31212))), % 61.24/61.38 inference(scs_inference,[],[3014,2981,62,636,72,82,89,8,6,10,7,11])). % 61.24/61.38 cnf(3123,plain, % 61.24/61.38 (E(f4(a20),f4(a2))), % 61.24/61.38 inference(scs_inference,[],[3014,2981,62,636,72,82,89,8,6,10,7,11,14,15])). % 61.24/61.38 cnf(3131,plain, % 61.24/61.38 (E(f17(x31311,x31312,a20),f17(x31311,x31312,a2))), % 61.24/61.38 inference(scs_inference,[],[3014,2981,3098,62,636,72,82,89,8,6,10,7,11,14,15,17,13,16,66,65,12])). % 61.24/61.38 cnf(3132,plain, % 61.24/61.38 (E(f21(x31321,a20),f21(x31321,a2))), % 61.24/61.38 inference(scs_inference,[],[3014,2981,3098,62,636,72,82,89,8,6,10,7,11,14,15,17,13,16,66,65,12,9])). % 61.24/61.38 cnf(3136,plain, % 61.24/61.38 (~E(a20,f22(a8))), % 61.24/61.38 inference(scs_inference,[],[3014,2981,3072,3049,3098,3037,384,62,636,72,82,89,8,6,10,7,11,14,15,17,13,16,66,65,12,9,2,98,3])). % 61.24/61.38 cnf(3137,plain, % 61.24/61.38 (~E(f3(f23(a2)),f5(a1))), % 61.24/61.38 inference(scs_inference,[],[3014,2981,3072,3049,3098,3037,384,62,636,72,82,89,8,6,10,7,11,14,15,17,13,16,66,65,12,9,2,98,3,22])). % 61.24/61.38 cnf(3139,plain, % 61.24/61.38 (P10(f4(a10),f23(a10))), % 61.24/61.38 inference(scs_inference,[],[3014,3020,2981,3072,3049,3098,3037,384,64,134,62,636,72,82,89,8,6,10,7,11,14,15,17,13,16,66,65,12,9,2,98,3,22,33,88])). % 61.24/61.38 cnf(3144,plain, % 61.24/61.38 (P8(f21(a1,f5(a1)),a1)), % 61.24/61.38 inference(scs_inference,[],[42,2987,3014,3020,2981,3072,3049,3098,3037,384,64,134,62,58,43,636,72,82,89,8,6,10,7,11,14,15,17,13,16,66,65,12,9,2,98,3,22,33,88,99,100])). % 61.24/61.38 cnf(3148,plain, % 61.24/61.38 (P7(a2,f23(a2))), % 61.24/61.38 inference(scs_inference,[],[42,2987,3014,3020,2981,3072,3049,3098,3037,384,64,134,62,58,43,636,72,82,89,8,6,10,7,11,14,15,17,13,16,66,65,12,9,2,98,3,22,33,88,99,100,108,1459])). % 61.24/61.38 cnf(3149,plain, % 61.24/61.38 (P7(a20,f23(a2))), % 61.24/61.38 inference(scs_inference,[],[42,2987,3014,3020,2981,3072,3049,3098,3037,384,64,134,62,58,43,636,72,82,89,8,6,10,7,11,14,15,17,13,16,66,65,12,9,2,98,3,22,33,88,99,100,108,1459,1465])). % 61.24/61.38 cnf(3158,plain, % 61.24/61.38 (P7(f4(a14),f23(a14))), % 61.24/61.38 inference(scs_inference,[],[3047,60,72,82])). % 61.24/61.38 cnf(3165,plain, % 61.24/61.38 (E(f17(a2,a2,x31651),f17(a20,a20,x31651))), % 61.24/61.38 inference(scs_inference,[],[3016,3080,3086,3047,3136,608,60,72,82,89,2,98,3])). % 61.24/61.38 cnf(3171,plain, % 61.24/61.38 (~P11(f21(a1,f5(a1)))), % 61.24/61.38 inference(scs_inference,[],[42,3016,3080,3086,3104,3047,3136,3144,3098,608,60,58,43,72,82,89,2,98,3,22,99,92])). % 61.24/61.38 cnf(3191,plain, % 61.24/61.38 (~P10(f23(f22(a1)),f4(a16))), % 61.24/61.38 inference(scs_inference,[],[3056,3050,3096,3113,1094,72,89,2,98])). % 61.24/61.38 cnf(3193,plain, % 61.24/61.38 (P7(f3(f17(a2,a2,x31931)),f17(a20,a20,x31931))), % 61.24/61.38 inference(scs_inference,[],[3165,3056,3050,3096,3113,1094,53,72,89,2,98,28])). % 61.24/61.38 cnf(3210,plain, % 61.24/61.38 (P6(f22(a20),f22(a2))), % 61.24/61.38 inference(scs_inference,[],[3137,3078,1558,153,52,72,89,2,20])). % 61.24/61.38 cnf(3211,plain, % 61.24/61.38 (P6(x32111,x32111)), % 61.24/61.38 inference(rename_variables,[],[52])). % 61.24/61.38 cnf(3212,plain, % 61.24/61.38 (P6(f22(a2),f22(a20))), % 61.24/61.38 inference(scs_inference,[],[3137,3078,1558,153,52,3211,72,89,2,20,21])). % 61.24/61.38 cnf(3216,plain, % 61.24/61.38 (~P7(f23(a10),f23(a20))), % 61.24/61.38 inference(scs_inference,[],[3137,3054,3078,3139,1558,153,52,3211,321,45,72,89,2,20,21,98,97])). % 61.24/61.38 cnf(3218,plain, % 61.24/61.38 (~P7(f23(a10),f23(a2))), % 61.24/61.38 inference(scs_inference,[],[3137,3054,3078,3081,3139,1558,153,52,3211,321,45,72,89,2,20,21,98,97,28])). % 61.24/61.38 cnf(3219,plain, % 61.24/61.38 (E(f17(a20,x32191,a2),f17(a2,x32191,a20))), % 61.24/61.38 inference(scs_inference,[],[3137,3054,3078,3081,3089,3119,3139,1558,153,52,3211,321,45,72,89,2,20,21,98,97,28,3])). % 61.24/61.38 cnf(3222,plain, % 61.24/61.38 (~E(f9(a2),f23(a10))), % 61.24/61.38 inference(scs_inference,[],[3137,3054,3078,3081,3089,3119,3139,1558,153,1568,52,3211,321,45,72,89,2,20,21,98,97,28,3,27])). % 61.24/61.38 cnf(3224,plain, % 61.24/61.38 (P8(f21(a1,f21(a1,a14)),a1)), % 61.24/61.38 inference(scs_inference,[],[42,3137,3171,2989,3054,3078,3081,3089,3119,3139,1558,153,1568,52,3211,321,45,58,43,72,89,2,20,21,98,97,28,3,27,22,100])). % 61.24/61.38 cnf(3226,plain, % 61.24/61.38 (~E(f9(a20),f23(a10))), % 61.24/61.38 inference(scs_inference,[],[42,3137,3171,2989,3054,3078,3081,3089,3119,3139,1558,153,1568,52,3211,321,45,58,43,72,89,2,20,21,98,97,28,3,27,22,100,437])). % 61.24/61.38 cnf(3234,plain, % 61.24/61.38 (~P11(f4(f21(a1,a16)))), % 61.24/61.38 inference(scs_inference,[],[251,72])). % 61.24/61.38 cnf(3239,plain, % 61.24/61.38 (P6(f9(a2),f22(a1))), % 61.24/61.38 inference(scs_inference,[],[3210,3222,3058,1557,251,72,89,2,96])). % 61.24/61.38 cnf(3244,plain, % 61.24/61.38 (E(f17(a20,x32441,a2),f17(a2,x32441,a20))), % 61.24/61.38 inference(rename_variables,[],[3219])). % 61.24/61.38 cnf(3253,plain, % 61.24/61.38 (P6(f21(a1,f21(a1,a14)),f21(a1,a14))), % 61.24/61.38 inference(scs_inference,[],[42,3158,3219,3244,3210,3222,3193,3224,3118,3058,1557,2960,547,251,2989,3098,607,153,52,136,58,43,72,89,2,96,98,28,27,3,88,22,24,109])). % 61.24/61.38 cnf(3261,plain, % 61.24/61.38 (P6(a15,a16)), % 61.24/61.38 inference(scs_inference,[],[3253,102])). % 61.24/61.38 cnf(3262,plain, % 61.24/61.38 (~P6(f21(a1,a15),f21(a1,a16))), % 61.24/61.38 inference(scs_inference,[],[3253,104])). % 61.24/61.38 cnf(3271,plain, % 61.24/61.38 (P10(a2,f23(a2))), % 61.24/61.38 inference(scs_inference,[],[3148,3226,3212,3121,3131,177,64,72,89,2,3,88])). % 61.24/61.38 cnf(3275,plain, % 61.24/61.38 (~E(a2,f23(a10))), % 61.24/61.38 inference(scs_inference,[],[3148,3226,3212,3216,3218,3121,3131,3026,177,64,72,89,2,3,88,28,27])). % 61.24/61.38 cnf(3287,plain, % 61.24/61.38 (~E(a16,f21(a1,a15))), % 61.24/61.38 inference(scs_inference,[],[3262,1388])). % 61.24/61.38 cnf(3288,plain, % 61.24/61.38 (~E(f9(a16),f21(a1,a15))), % 61.24/61.38 inference(scs_inference,[],[3262,1388,1505])). % 61.24/61.38 cnf(3289,plain, % 61.24/61.38 (~E(f3(f23(a16)),f21(a1,a15))), % 61.24/61.38 inference(scs_inference,[],[3262,1388,1505,1400])). % 61.24/61.38 cnf(3296,plain, % 61.24/61.38 (~P11(f4(a10))), % 61.24/61.38 inference(scs_inference,[],[3262,63,1388,1505,1400,1534,502,142,525,91,72])). % 61.24/61.38 cnf(3298,plain, % 61.24/61.38 (P7(a15,f23(a16))), % 61.24/61.38 inference(scs_inference,[],[3261,3262,63,1388,1505,1400,1534,502,142,525,91,72,89])). % 61.24/61.38 cnf(3325,plain, % 61.24/61.38 (P10(a2,f23(a20))), % 61.24/61.38 inference(scs_inference,[],[3287,3239,3296,3271,3081,72,89,2,24])). % 61.24/61.38 cnf(3326,plain, % 61.24/61.38 (P7(f3(a15),a16)), % 61.24/61.38 inference(scs_inference,[],[3287,3239,3296,3298,3271,3081,162,72,89,2,24,98])). % 61.24/61.38 cnf(3328,plain, % 61.24/61.38 (P10(a20,f23(a2))), % 61.24/61.38 inference(scs_inference,[],[3287,3149,3239,3296,3298,3271,3081,162,64,72,89,2,24,98,88])). % 61.24/61.38 cnf(3344,plain, % 61.24/61.38 (P7(f3(f23(a20)),f23(a2))), % 61.24/61.38 inference(scs_inference,[],[639,117,72,89])). % 61.24/61.38 cnf(3349,plain, % 61.24/61.38 (~E(a20,f21(a1,a15))), % 61.24/61.38 inference(scs_inference,[],[3288,3275,3325,639,2960,117,243,72,89,2,24,3])). % 61.24/61.38 cnf(3365,plain, % 61.24/61.38 (P6(f4(a20),f4(a2))), % 61.24/61.38 inference(scs_inference,[],[3289,3085,643,52,64,72,89,2,20])). % 61.24/61.38 cnf(3366,plain, % 61.24/61.38 (P6(x33661,x33661)), % 61.24/61.38 inference(rename_variables,[],[52])). % 61.24/61.38 cnf(3367,plain, % 61.24/61.38 (P6(f4(a2),f4(a20))), % 61.24/61.38 inference(scs_inference,[],[3289,3085,643,52,3366,64,72,89,2,20,21])). % 61.24/61.38 cnf(3369,plain, % 61.24/61.38 (~P7(f23(a2),f23(a2))), % 61.24/61.38 inference(scs_inference,[],[3289,3328,3085,643,52,3366,64,46,72,89,2,20,21,97])). % 61.24/61.38 cnf(3371,plain, % 61.24/61.38 (P10(a20,f23(a20))), % 61.24/61.38 inference(scs_inference,[],[3289,3328,3085,643,3081,52,3366,64,46,72,89,2,20,21,97,24])). % 61.24/61.38 cnf(3372,plain, % 61.24/61.38 (E(f21(a2,a2),f21(a20,a20))), % 61.24/61.38 inference(scs_inference,[],[3289,3328,3085,3079,3090,643,3081,52,3366,64,46,72,89,2,20,21,97,24,3])). % 61.24/61.38 cnf(3375,plain, % 61.24/61.38 (~P7(f23(a2),f23(a20))), % 61.24/61.38 inference(scs_inference,[],[3289,3328,3085,3079,3090,3120,643,3081,52,3366,64,46,72,89,2,20,21,97,24,3,28])). % 61.24/61.38 cnf(3378,plain, % 61.24/61.38 (~E(f9(a2),f23(a2))), % 61.24/61.38 inference(scs_inference,[],[3289,3344,3234,3328,3085,3079,3090,3120,3218,643,3081,52,3366,64,46,72,89,2,20,21,97,24,3,28,22,27,437])). % 61.24/61.38 cnf(3386,plain, % 61.24/61.38 (~P11(f4(a16))), % 61.24/61.38 inference(scs_inference,[],[3375,62,437,72])). % 61.24/61.38 cnf(3406,plain, % 61.24/61.38 (~P6(a15,f21(a1,a16))), % 61.24/61.38 inference(scs_inference,[],[42,3349,3365,3372,3375,3378,3371,3191,3123,3239,3224,1569,2966,3098,167,202,62,61,3262,214,55,53,58,636,43,437,72,89,2,96,24,88,3,28,22,27,92,94,109])). % 61.24/61.38 cnf(3410,plain, % 61.24/61.38 (~E(a16,a15)), % 61.24/61.38 inference(scs_inference,[],[42,3349,3365,3372,3375,3378,3371,3191,3123,3239,3224,1569,2966,3098,167,202,62,61,3262,214,55,53,58,636,43,437,72,89,2,96,24,88,3,28,22,27,92,94,109,1534,502,1388])). % 61.24/61.38 cnf(3413,plain, % 61.24/61.38 (~P7(a15,f23(f21(a1,a16)))), % 61.24/61.38 inference(scs_inference,[],[42,3349,3365,3372,3375,3378,3371,3191,3123,3239,3224,1569,2966,3098,167,202,62,61,3262,214,55,53,58,636,43,437,72,89,2,96,24,88,3,28,22,27,92,94,109,1534,502,1388,1505,1400,91])). % 61.24/61.38 cnf(3438,plain, % 61.24/61.38 (~E(f9(a2),f23(a20))), % 61.24/61.38 inference(scs_inference,[],[3410,3367,3369,3386,3326,3413,3087,3117,3132,3298,3120,2977,52,62,72,89,2,21,88,3,28,22,27,90,437])). % 61.24/61.38 cnf(3495,plain, % 61.24/61.38 ($false), % 61.24/61.38 inference(scs_inference,[],[3438,3406,1396,3261,1384,89,2,96]), % 61.24/61.38 ['proof']). % 61.24/61.38 % SZS output end Proof % 61.24/61.38 % Total time :60.570000s %------------------------------------------------------------------------------