%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT346+1 : TPTP v8.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n022.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:19:02 EDT 2024 % Result : Theorem 59.60s 59.61s % Output : CNFRefutation 59.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : LAT346+1 : TPTP v8.2.0. Released v3.4.0. % 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n022.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Sat Jun 22 00:22:53 EDT 2024 % 0.13/0.33 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 59.54/59.58 %------------------------------------------- % 59.54/59.58 % File :CSE---1.7 % 59.54/59.58 % Problem :theBenchmark % 59.54/59.58 % Transform :cnf % 59.54/59.58 % Format :tptp:raw % 59.54/59.58 % Command :java -jar mcs_scs.jar %d %s % 59.54/59.58 % 59.54/59.58 % Result :Theorem 58.930000s % 59.54/59.58 % Output :CNFRefutation 58.930000s % 59.54/59.58 %------------------------------------------- % 59.54/59.59 %------------------------------------------------------------------------------ % 59.54/59.59 % File : LAT346+1 : TPTP v8.2.0. Released v3.4.0. % 59.54/59.59 % Domain : Lattice Theory % 59.54/59.59 % Problem : Dual Concept Lattices T22 % 59.54/59.59 % Version : [Urb08] axioms : Especial. % 59.54/59.59 % English : % 59.54/59.59 % 59.54/59.59 % Refs : [Sch01] Schwarzweller (2001), A Characterization of Concept La % 59.54/59.59 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 59.54/59.59 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 59.54/59.59 % Source : [Urb08] % 59.54/59.59 % Names : t22_conlat_2 [Urb08] % 59.54/59.59 % 59.54/59.59 % Status : Theorem % 59.54/59.59 % Rating : 0.31 v8.2.0, 0.33 v8.1.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.30 v7.3.0, 0.31 v7.2.0, 0.28 v7.1.0, 0.35 v7.0.0, 0.27 v6.4.0, 0.35 v6.3.0, 0.38 v6.2.0, 0.32 v6.1.0, 0.37 v6.0.0, 0.30 v5.5.0, 0.48 v5.4.0, 0.46 v5.3.0, 0.56 v5.2.0, 0.45 v5.1.0, 0.48 v5.0.0, 0.50 v4.1.0, 0.57 v4.0.1, 0.52 v4.0.0, 0.58 v3.7.0, 0.55 v3.5.0, 0.58 v3.4.0 % 59.54/59.59 % Syntax : Number of formulae : 102 ( 24 unt; 0 def) % 59.54/59.59 % Number of atoms : 412 ( 16 equ) % 59.54/59.59 % Maximal formula atoms : 15 ( 4 avg) % 59.54/59.59 % Number of connectives : 387 ( 77 ~; 1 |; 227 &) % 59.54/59.59 % ( 3 <=>; 79 =>; 0 <=; 0 <~>) % 59.54/59.59 % Maximal formula depth : 15 ( 5 avg) % 59.54/59.59 % Maximal term depth : 4 ( 1 avg) % 59.54/59.59 % Number of predicates : 38 ( 36 usr; 1 prp; 0-3 aty) % 59.54/59.59 % Number of functors : 17 ( 17 usr; 1 con; 0-3 aty) % 59.54/59.59 % Number of variables : 159 ( 132 !; 27 ?) % 59.54/59.59 % SPC : FOF_THM_RFO_SEQ % 59.54/59.59 % 59.54/59.59 % Comments : Normal version: includes the axioms (which may be theorems from % 59.54/59.59 % other articles) and background that are possibly necessary. % 59.54/59.59 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 59.54/59.59 % : The problem encoding is based on set theory. % 59.54/59.59 %------------------------------------------------------------------------------ % 59.54/59.59 fof(t22_conlat_2,conjecture, % 59.54/59.59 ! [A] : % 59.54/59.59 ( ( ~ v3_conlat_1(A) % 59.54/59.59 & l2_conlat_1(A) ) % 59.54/59.59 => r1_filter_1(k11_conlat_1(k7_conlat_2(A)),k1_lattice2(k11_conlat_1(A))) ) ). % 59.54/59.59 % 59.54/59.59 fof(abstractness_v3_lattices,axiom, % 59.54/59.59 ! [A] : % 59.54/59.59 ( l3_lattices(A) % 59.54/59.59 => ( v3_lattices(A) % 59.54/59.59 => A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ) ). % 59.54/59.59 % 59.54/59.59 fof(abstractness_v4_conlat_1,axiom, % 59.54/59.59 ! [A] : % 59.54/59.59 ( l2_conlat_1(A) % 59.54/59.59 => ( v4_conlat_1(A) % 59.54/59.59 => A = g2_conlat_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A)) ) ) ). % 59.54/59.59 % 59.54/59.59 fof(antisymmetry_r2_hidden,axiom, % 59.54/59.59 ! [A,B] : % 59.54/59.59 ( r2_hidden(A,B) % 59.54/59.59 => ~ r2_hidden(B,A) ) ). % 59.54/59.59 % 59.54/59.59 fof(cc1_funct_2,axiom, % 59.54/59.59 ! [A,B,C] : % 59.54/59.59 ( m1_relset_1(C,A,B) % 59.54/59.59 => ( ( v1_funct_1(C) % 59.54/59.59 & v1_partfun1(C,A,B) ) % 59.54/59.59 => ( v1_funct_1(C) % 59.54/59.59 & v1_funct_2(C,A,B) ) ) ) ). % 59.54/59.59 % 59.54/59.59 fof(cc1_lattices,axiom, % 59.54/59.59 ! [A] : % 59.54/59.59 ( l3_lattices(A) % 59.54/59.59 => ( ( ~ v3_struct_0(A) % 59.54/59.59 & v10_lattices(A) ) % 59.54/59.59 => ( ~ v3_struct_0(A) % 59.54/59.59 & v4_lattices(A) % 59.54/59.59 & v5_lattices(A) % 59.54/59.59 & v6_lattices(A) % 59.54/59.59 & v7_lattices(A) % 59.54/59.59 & v8_lattices(A) % 59.54/59.59 & v9_lattices(A) ) ) ) ). % 59.54/59.59 % 59.54/59.59 fof(cc1_relset_1,axiom, % 59.54/59.59 ! [A,B,C] : % 59.54/59.59 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 59.54/59.59 => v1_relat_1(C) ) ). % 59.54/59.59 % 59.54/59.59 fof(cc2_lattices,axiom, % 59.54/59.59 ! [A] : % 59.54/59.59 ( l3_lattices(A) % 59.54/59.59 => ( ( ~ v3_struct_0(A) % 59.54/59.59 & v4_lattices(A) % 59.54/59.59 & v5_lattices(A) % 59.54/59.59 & v6_lattices(A) % 59.54/59.59 & v7_lattices(A) % 59.54/59.59 & v8_lattices(A) % 59.54/59.59 & v9_lattices(A) ) % 59.54/59.59 => ( ~ v3_struct_0(A) % 59.54/59.59 & v10_lattices(A) ) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(cc3_lattices,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( l3_lattices(A) % 59.54/59.60 => ( ( ~ v3_struct_0(A) % 59.54/59.60 & v13_lattices(A) % 59.54/59.60 & v14_lattices(A) ) % 59.54/59.60 => ( ~ v3_struct_0(A) % 59.54/59.60 & v15_lattices(A) ) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(cc4_lattices,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( l3_lattices(A) % 59.54/59.60 => ( ( ~ v3_struct_0(A) % 59.54/59.60 & v15_lattices(A) ) % 59.54/59.60 => ( ~ v3_struct_0(A) % 59.54/59.60 & v13_lattices(A) % 59.54/59.60 & v14_lattices(A) ) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(cc5_funct_2,axiom, % 59.54/59.60 ! [A,B] : % 59.54/59.60 ( ~ v1_xboole_0(B) % 59.54/59.60 => ! [C] : % 59.54/59.60 ( m1_relset_1(C,A,B) % 59.54/59.60 => ( ( v1_funct_1(C) % 59.54/59.60 & v1_funct_2(C,A,B) ) % 59.54/59.60 => ( v1_funct_1(C) % 59.54/59.60 & v1_partfun1(C,A,B) % 59.54/59.60 & v1_funct_2(C,A,B) ) ) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(cc6_funct_2,axiom, % 59.54/59.60 ! [A,B] : % 59.54/59.60 ( ( ~ v1_xboole_0(A) % 59.54/59.60 & ~ v1_xboole_0(B) ) % 59.54/59.60 => ! [C] : % 59.54/59.60 ( m1_relset_1(C,A,B) % 59.54/59.60 => ( ( v1_funct_1(C) % 59.54/59.60 & v1_funct_2(C,A,B) ) % 59.54/59.60 => ( v1_funct_1(C) % 59.54/59.60 & ~ v1_xboole_0(C) % 59.54/59.60 & v1_partfun1(C,A,B) % 59.54/59.60 & v1_funct_2(C,A,B) ) ) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(d5_lattice4,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( ( ~ v3_struct_0(A) % 59.54/59.60 & v10_lattices(A) % 59.54/59.60 & l3_lattices(A) ) % 59.54/59.60 => ! [B] : % 59.54/59.60 ( ( ~ v3_struct_0(B) % 59.54/59.60 & v10_lattices(B) % 59.54/59.60 & l3_lattices(B) ) % 59.54/59.60 => ( r1_filter_1(A,B) % 59.54/59.60 <=> ? [C] : % 59.54/59.60 ( m1_lattice4(C,A,B) % 59.54/59.60 & v3_lattice4(C,A,B) ) ) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(d7_conlat_2,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( ( ~ v3_conlat_1(A) % 59.54/59.60 & l2_conlat_1(A) ) % 59.54/59.60 => k7_conlat_2(A) = g2_conlat_1(u2_conlat_1(A),u1_conlat_1(A),k6_relset_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A))) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_g2_conlat_1,axiom, % 59.54/59.60 ! [A,B,C] : % 59.54/59.60 ( m1_relset_1(C,A,B) % 59.54/59.60 => ( v4_conlat_1(g2_conlat_1(A,B,C)) % 59.54/59.60 & l2_conlat_1(g2_conlat_1(A,B,C)) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_g3_lattices,axiom, % 59.54/59.60 ! [A,B,C] : % 59.54/59.60 ( ( v1_funct_1(B) % 59.54/59.60 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 59.54/59.60 & m1_relset_1(B,k2_zfmisc_1(A,A),A) % 59.54/59.60 & v1_funct_1(C) % 59.54/59.60 & v1_funct_2(C,k2_zfmisc_1(A,A),A) % 59.54/59.60 & m1_relset_1(C,k2_zfmisc_1(A,A),A) ) % 59.54/59.60 => ( v3_lattices(g3_lattices(A,B,C)) % 59.54/59.60 & l3_lattices(g3_lattices(A,B,C)) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_k10_conlat_2,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( ( ~ v3_conlat_1(A) % 59.54/59.60 & l2_conlat_1(A) ) % 59.54/59.60 => m1_lattice4(k10_conlat_2(A),k1_lattice2(k11_conlat_1(A)),k11_conlat_1(k7_conlat_2(A))) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_k11_conlat_1,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( ( ~ v3_conlat_1(A) % 59.54/59.60 & l2_conlat_1(A) ) % 59.54/59.60 => ( ~ v3_struct_0(k11_conlat_1(A)) % 59.54/59.60 & v3_lattices(k11_conlat_1(A)) % 59.54/59.60 & l3_lattices(k11_conlat_1(A)) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_k1_lattice2,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( l3_lattices(A) % 59.54/59.60 => ( v3_lattices(k1_lattice2(A)) % 59.54/59.60 & l3_lattices(k1_lattice2(A)) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_k1_xboole_0,axiom, % 59.54/59.60 $true ). % 59.54/59.60 % 59.54/59.60 fof(dt_k1_zfmisc_1,axiom, % 59.54/59.60 $true ). % 59.54/59.60 % 59.54/59.60 fof(dt_k2_zfmisc_1,axiom, % 59.54/59.60 $true ). % 59.54/59.60 % 59.54/59.60 fof(dt_k4_relat_1,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( v1_relat_1(A) % 59.54/59.60 => v1_relat_1(k4_relat_1(A)) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_k6_relset_1,axiom, % 59.54/59.60 ! [A,B,C] : % 59.54/59.60 ( m1_relset_1(C,A,B) % 59.54/59.60 => m2_relset_1(k6_relset_1(A,B,C),B,A) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_k7_conlat_2,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( ( ~ v3_conlat_1(A) % 59.54/59.60 & l2_conlat_1(A) ) % 59.54/59.60 => ( ~ v3_conlat_1(k7_conlat_2(A)) % 59.54/59.60 & v4_conlat_1(k7_conlat_2(A)) % 59.54/59.60 & l2_conlat_1(k7_conlat_2(A)) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_l1_conlat_1,axiom, % 59.54/59.60 $true ). % 59.54/59.60 % 59.54/59.60 fof(dt_l1_lattices,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( l1_lattices(A) % 59.54/59.60 => l1_struct_0(A) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_l1_struct_0,axiom, % 59.54/59.60 $true ). % 59.54/59.60 % 59.54/59.60 fof(dt_l2_conlat_1,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( l2_conlat_1(A) % 59.54/59.60 => l1_conlat_1(A) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_l2_lattices,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( l2_lattices(A) % 59.54/59.60 => l1_struct_0(A) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_l3_lattices,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( l3_lattices(A) % 59.54/59.60 => ( l1_lattices(A) % 59.54/59.60 & l2_lattices(A) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_m1_lattice4,axiom, % 59.54/59.60 ! [A,B] : % 59.54/59.60 ( ( ~ v3_struct_0(A) % 59.54/59.60 & v10_lattices(A) % 59.54/59.60 & l3_lattices(A) % 59.54/59.60 & ~ v3_struct_0(B) % 59.54/59.60 & v10_lattices(B) % 59.54/59.60 & l3_lattices(B) ) % 59.54/59.60 => ! [C] : % 59.54/59.60 ( m1_lattice4(C,A,B) % 59.54/59.60 => ( v1_funct_1(C) % 59.54/59.60 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 59.54/59.60 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_m1_relset_1,axiom, % 59.54/59.60 $true ). % 59.54/59.60 % 59.54/59.60 fof(dt_m1_subset_1,axiom, % 59.54/59.60 $true ). % 59.54/59.60 % 59.54/59.60 fof(dt_m2_relset_1,axiom, % 59.54/59.60 ! [A,B,C] : % 59.54/59.60 ( m2_relset_1(C,A,B) % 59.54/59.60 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_u1_conlat_1,axiom, % 59.54/59.60 $true ). % 59.54/59.60 % 59.54/59.60 fof(dt_u1_lattices,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( l1_lattices(A) % 59.54/59.60 => ( v1_funct_1(u1_lattices(A)) % 59.54/59.60 & v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 59.54/59.60 & m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_u1_struct_0,axiom, % 59.54/59.60 $true ). % 59.54/59.60 % 59.54/59.60 fof(dt_u2_conlat_1,axiom, % 59.54/59.60 $true ). % 59.54/59.60 % 59.54/59.60 fof(dt_u2_lattices,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( l2_lattices(A) % 59.54/59.60 => ( v1_funct_1(u2_lattices(A)) % 59.54/59.60 & v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 59.54/59.60 & m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 59.54/59.60 % 59.54/59.60 fof(dt_u3_conlat_1,axiom, % 59.54/59.60 ! [A] : % 59.54/59.60 ( l2_conlat_1(A) % 59.54/59.60 => m2_relset_1(u3_conlat_1(A),u1_conlat_1(A),u2_conlat_1(A)) ) ). % 59.54/59.60 % 59.54/59.60 fof(existence_l1_conlat_1,axiom, % 59.54/59.60 ? [A] : l1_conlat_1(A) ). % 59.54/59.60 % 59.54/59.60 fof(existence_l1_lattices,axiom, % 59.54/59.60 ? [A] : l1_lattices(A) ). % 59.54/59.60 % 59.54/59.60 fof(existence_l1_struct_0,axiom, % 59.54/59.60 ? [A] : l1_struct_0(A) ). % 59.54/59.60 % 59.54/59.60 fof(existence_l2_conlat_1,axiom, % 59.54/59.60 ? [A] : l2_conlat_1(A) ). % 59.54/59.60 % 59.54/59.60 fof(existence_l2_lattices,axiom, % 59.54/59.60 ? [A] : l2_lattices(A) ). % 59.54/59.60 % 59.54/59.60 fof(existence_l3_lattices,axiom, % 59.54/59.60 ? [A] : l3_lattices(A) ). % 59.54/59.60 % 59.54/59.60 fof(existence_m1_lattice4,axiom, % 59.54/59.60 ! [A,B] : % 59.54/59.60 ( ( ~ v3_struct_0(A) % 59.54/59.60 & v10_lattices(A) % 59.54/59.60 & l3_lattices(A) % 59.54/59.60 & ~ v3_struct_0(B) % 59.54/59.60 & v10_lattices(B) % 59.54/59.60 & l3_lattices(B) ) % 59.54/59.60 => ? [C] : m1_lattice4(C,A,B) ) ). % 59.54/59.60 % 59.54/59.60 fof(existence_m1_relset_1,axiom, % 59.54/59.60 ! [A,B] : % 59.60/59.60 ? [C] : m1_relset_1(C,A,B) ). % 59.60/59.60 % 59.60/59.60 fof(existence_m1_subset_1,axiom, % 59.60/59.60 ! [A] : % 59.60/59.60 ? [B] : m1_subset_1(B,A) ). % 59.60/59.60 % 59.60/59.60 fof(existence_m2_relset_1,axiom, % 59.60/59.60 ! [A,B] : % 59.60/59.60 ? [C] : m2_relset_1(C,A,B) ). % 59.60/59.60 % 59.60/59.60 fof(fc1_conlat_1,axiom, % 59.60/59.60 ! [A] : % 59.60/59.60 ( ( ~ v3_conlat_1(A) % 59.60/59.60 & l1_conlat_1(A) ) % 59.60/59.60 => ~ v1_xboole_0(u2_conlat_1(A)) ) ). % 59.60/59.60 % 59.60/59.60 fof(fc1_conlat_2,axiom, % 59.60/59.60 ! [A] : % 59.60/59.60 ( ( ~ v3_conlat_1(A) % 59.60/59.60 & l2_conlat_1(A) ) % 59.60/59.61 => ( ~ v3_struct_0(k11_conlat_1(A)) % 59.60/59.61 & v3_lattices(k11_conlat_1(A)) % 59.60/59.61 & v4_lattices(k11_conlat_1(A)) % 59.60/59.61 & v5_lattices(k11_conlat_1(A)) % 59.60/59.61 & v6_lattices(k11_conlat_1(A)) % 59.60/59.61 & v7_lattices(k11_conlat_1(A)) % 59.60/59.61 & v8_lattices(k11_conlat_1(A)) % 59.60/59.61 & v9_lattices(k11_conlat_1(A)) % 59.60/59.61 & v10_lattices(k11_conlat_1(A)) % 59.60/59.61 & v13_lattices(k11_conlat_1(A)) % 59.60/59.61 & v14_lattices(k11_conlat_1(A)) % 59.60/59.61 & v15_lattices(k11_conlat_1(A)) % 59.60/59.61 & v4_lattice3(k11_conlat_1(A)) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(fc1_lattice2,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_struct_0(A) % 59.60/59.61 & l3_lattices(A) ) % 59.60/59.61 => ( ~ v3_struct_0(k1_lattice2(A)) % 59.60/59.61 & v3_lattices(k1_lattice2(A)) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(fc1_struct_0,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_struct_0(A) % 59.60/59.61 & l1_struct_0(A) ) % 59.60/59.61 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 59.60/59.61 % 59.60/59.61 fof(fc1_subset_1,axiom, % 59.60/59.61 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 59.60/59.61 % 59.60/59.61 fof(fc1_xboole_0,axiom, % 59.60/59.61 v1_xboole_0(k1_xboole_0) ). % 59.60/59.61 % 59.60/59.61 fof(fc2_conlat_1,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_conlat_1(A) % 59.60/59.61 & l1_conlat_1(A) ) % 59.60/59.61 => ~ v1_xboole_0(u1_conlat_1(A)) ) ). % 59.60/59.61 % 59.60/59.61 fof(fc2_conlat_2,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_struct_0(A) % 59.60/59.61 & v10_lattices(A) % 59.60/59.61 & v4_lattice3(A) % 59.60/59.61 & l3_lattices(A) ) % 59.60/59.61 => ( ~ v3_struct_0(k1_lattice2(A)) % 59.60/59.61 & v3_lattices(k1_lattice2(A)) % 59.60/59.61 & v4_lattices(k1_lattice2(A)) % 59.60/59.61 & v5_lattices(k1_lattice2(A)) % 59.60/59.61 & v6_lattices(k1_lattice2(A)) % 59.60/59.61 & v7_lattices(k1_lattice2(A)) % 59.60/59.61 & v8_lattices(k1_lattice2(A)) % 59.60/59.61 & v9_lattices(k1_lattice2(A)) % 59.60/59.61 & v10_lattices(k1_lattice2(A)) % 59.60/59.61 & v4_lattice3(k1_lattice2(A)) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(fc2_lattice2,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_struct_0(A) % 59.60/59.61 & v4_lattices(A) % 59.60/59.61 & l2_lattices(A) ) % 59.60/59.61 => ( v1_relat_1(u2_lattices(A)) % 59.60/59.61 & v1_funct_1(u2_lattices(A)) % 59.60/59.61 & v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 59.60/59.61 & v1_binop_1(u2_lattices(A),u1_struct_0(A)) % 59.60/59.61 & v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(fc3_lattice2,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_struct_0(A) % 59.60/59.61 & v5_lattices(A) % 59.60/59.61 & l2_lattices(A) ) % 59.60/59.61 => ( v1_relat_1(u2_lattices(A)) % 59.60/59.61 & v1_funct_1(u2_lattices(A)) % 59.60/59.61 & v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 59.60/59.61 & v2_binop_1(u2_lattices(A),u1_struct_0(A)) % 59.60/59.61 & v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(fc3_lattices,axiom, % 59.60/59.61 ! [A,B,C] : % 59.60/59.61 ( ( ~ v1_xboole_0(A) % 59.60/59.61 & v1_funct_1(B) % 59.60/59.61 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 59.60/59.61 & m1_relset_1(B,k2_zfmisc_1(A,A),A) % 59.60/59.61 & v1_funct_1(C) % 59.60/59.61 & v1_funct_2(C,k2_zfmisc_1(A,A),A) % 59.60/59.61 & m1_relset_1(C,k2_zfmisc_1(A,A),A) ) % 59.60/59.61 => ( ~ v3_struct_0(g3_lattices(A,B,C)) % 59.60/59.61 & v3_lattices(g3_lattices(A,B,C)) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(fc4_conlat_1,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_conlat_1(A) % 59.60/59.61 & l2_conlat_1(A) ) % 59.60/59.61 => ( ~ v3_struct_0(k11_conlat_1(A)) % 59.60/59.61 & v3_lattices(k11_conlat_1(A)) % 59.60/59.61 & v4_lattices(k11_conlat_1(A)) % 59.60/59.61 & v5_lattices(k11_conlat_1(A)) % 59.60/59.61 & v6_lattices(k11_conlat_1(A)) % 59.60/59.61 & v7_lattices(k11_conlat_1(A)) % 59.60/59.61 & v8_lattices(k11_conlat_1(A)) % 59.60/59.61 & v9_lattices(k11_conlat_1(A)) % 59.60/59.61 & v10_lattices(k11_conlat_1(A)) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(fc4_lattice2,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_struct_0(A) % 59.60/59.61 & v6_lattices(A) % 59.60/59.61 & l1_lattices(A) ) % 59.60/59.61 => ( v1_relat_1(u1_lattices(A)) % 59.60/59.61 & v1_funct_1(u1_lattices(A)) % 59.60/59.61 & v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 59.60/59.61 & v1_binop_1(u1_lattices(A),u1_struct_0(A)) % 59.60/59.61 & v1_partfun1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(fc4_subset_1,axiom, % 59.60/59.61 ! [A,B] : % 59.60/59.61 ( ( ~ v1_xboole_0(A) % 59.60/59.61 & ~ v1_xboole_0(B) ) % 59.60/59.61 => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ). % 59.60/59.61 % 59.60/59.61 fof(fc5_conlat_1,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_conlat_1(A) % 59.60/59.61 & l2_conlat_1(A) ) % 59.60/59.61 => ( ~ v3_struct_0(k11_conlat_1(A)) % 59.60/59.61 & v3_lattices(k11_conlat_1(A)) % 59.60/59.61 & v4_lattices(k11_conlat_1(A)) % 59.60/59.61 & v5_lattices(k11_conlat_1(A)) % 59.60/59.61 & v6_lattices(k11_conlat_1(A)) % 59.60/59.61 & v7_lattices(k11_conlat_1(A)) % 59.60/59.61 & v8_lattices(k11_conlat_1(A)) % 59.60/59.61 & v9_lattices(k11_conlat_1(A)) % 59.60/59.61 & v10_lattices(k11_conlat_1(A)) % 59.60/59.61 & v4_lattice3(k11_conlat_1(A)) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(fc5_lattice2,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_struct_0(A) % 59.60/59.61 & v7_lattices(A) % 59.60/59.61 & l1_lattices(A) ) % 59.60/59.61 => ( v1_relat_1(u1_lattices(A)) % 59.60/59.61 & v1_funct_1(u1_lattices(A)) % 59.60/59.61 & v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 59.60/59.61 & v2_binop_1(u1_lattices(A),u1_struct_0(A)) % 59.60/59.61 & v1_partfun1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(fc6_lattice2,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_struct_0(A) % 59.60/59.61 & v10_lattices(A) % 59.60/59.61 & l3_lattices(A) ) % 59.60/59.61 => ( ~ v3_struct_0(k1_lattice2(A)) % 59.60/59.61 & v3_lattices(k1_lattice2(A)) % 59.60/59.61 & v4_lattices(k1_lattice2(A)) % 59.60/59.61 & v5_lattices(k1_lattice2(A)) % 59.60/59.61 & v6_lattices(k1_lattice2(A)) % 59.60/59.61 & v7_lattices(k1_lattice2(A)) % 59.60/59.61 & v8_lattices(k1_lattice2(A)) % 59.60/59.61 & v9_lattices(k1_lattice2(A)) % 59.60/59.61 & v10_lattices(k1_lattice2(A)) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(free_g2_conlat_1,axiom, % 59.60/59.61 ! [A,B,C] : % 59.60/59.61 ( m1_relset_1(C,A,B) % 59.60/59.61 => ! [D,E,F] : % 59.60/59.61 ( g2_conlat_1(A,B,C) = g2_conlat_1(D,E,F) % 59.60/59.61 => ( A = D % 59.60/59.61 & B = E % 59.60/59.61 & C = F ) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(free_g3_lattices,axiom, % 59.60/59.61 ! [A,B,C] : % 59.60/59.61 ( ( v1_funct_1(B) % 59.60/59.61 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 59.60/59.61 & m1_relset_1(B,k2_zfmisc_1(A,A),A) % 59.60/59.61 & v1_funct_1(C) % 59.60/59.61 & v1_funct_2(C,k2_zfmisc_1(A,A),A) % 59.60/59.61 & m1_relset_1(C,k2_zfmisc_1(A,A),A) ) % 59.60/59.61 => ! [D,E,F] : % 59.60/59.61 ( g3_lattices(A,B,C) = g3_lattices(D,E,F) % 59.60/59.61 => ( A = D % 59.60/59.61 & B = E % 59.60/59.61 & C = F ) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(involutiveness_k4_relat_1,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( v1_relat_1(A) % 59.60/59.61 => k4_relat_1(k4_relat_1(A)) = A ) ). % 59.60/59.61 % 59.60/59.61 fof(involutiveness_k6_relset_1,axiom, % 59.60/59.61 ! [A,B,C] : % 59.60/59.61 ( m1_relset_1(C,A,B) % 59.60/59.61 => k6_relset_1(A,B,k6_relset_1(A,B,C)) = C ) ). % 59.60/59.61 % 59.60/59.61 fof(rc11_lattices,axiom, % 59.60/59.61 ? [A] : % 59.60/59.61 ( l3_lattices(A) % 59.60/59.61 & ~ v3_struct_0(A) % 59.60/59.61 & v3_lattices(A) % 59.60/59.61 & v4_lattices(A) % 59.60/59.61 & v5_lattices(A) % 59.60/59.61 & v6_lattices(A) % 59.60/59.61 & v7_lattices(A) % 59.60/59.61 & v8_lattices(A) % 59.60/59.61 & v9_lattices(A) % 59.60/59.61 & v10_lattices(A) % 59.60/59.61 & v13_lattices(A) % 59.60/59.61 & v14_lattices(A) % 59.60/59.61 & v15_lattices(A) ) ). % 59.60/59.61 % 59.60/59.61 fof(rc1_funct_2,axiom, % 59.60/59.61 ! [A,B] : % 59.60/59.61 ? [C] : % 59.60/59.61 ( m1_relset_1(C,A,B) % 59.60/59.61 & v1_relat_1(C) % 59.60/59.61 & v1_funct_1(C) % 59.60/59.61 & v1_funct_2(C,A,B) ) ). % 59.60/59.61 % 59.60/59.61 fof(rc1_subset_1,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ~ v1_xboole_0(A) % 59.60/59.61 => ? [B] : % 59.60/59.61 ( m1_subset_1(B,k1_zfmisc_1(A)) % 59.60/59.61 & ~ v1_xboole_0(B) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(rc1_xboole_0,axiom, % 59.60/59.61 ? [A] : v1_xboole_0(A) ). % 59.60/59.61 % 59.60/59.61 fof(rc2_partfun1,axiom, % 59.60/59.61 ! [A,B] : % 59.60/59.61 ? [C] : % 59.60/59.61 ( m1_relset_1(C,A,B) % 59.60/59.61 & v1_relat_1(C) % 59.60/59.61 & v1_funct_1(C) ) ). % 59.60/59.61 % 59.60/59.61 fof(rc2_subset_1,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ? [B] : % 59.60/59.61 ( m1_subset_1(B,k1_zfmisc_1(A)) % 59.60/59.61 & v1_xboole_0(B) ) ). % 59.60/59.61 % 59.60/59.61 fof(rc2_xboole_0,axiom, % 59.60/59.61 ? [A] : ~ v1_xboole_0(A) ). % 59.60/59.61 % 59.60/59.61 fof(rc3_lattices,axiom, % 59.60/59.61 ? [A] : % 59.60/59.61 ( l3_lattices(A) % 59.60/59.61 & v3_lattices(A) ) ). % 59.60/59.61 % 59.60/59.61 fof(rc3_struct_0,axiom, % 59.60/59.61 ? [A] : % 59.60/59.61 ( l1_struct_0(A) % 59.60/59.61 & ~ v3_struct_0(A) ) ). % 59.60/59.61 % 59.60/59.61 fof(rc5_conlat_1,axiom, % 59.60/59.61 ? [A] : % 59.60/59.61 ( l2_conlat_1(A) % 59.60/59.61 & v4_conlat_1(A) ) ). % 59.60/59.61 % 59.60/59.61 fof(rc5_struct_0,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_struct_0(A) % 59.60/59.61 & l1_struct_0(A) ) % 59.60/59.61 => ? [B] : % 59.60/59.61 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.60/59.61 & ~ v1_xboole_0(B) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(rc6_lattices,axiom, % 59.60/59.61 ? [A] : % 59.60/59.61 ( l3_lattices(A) % 59.60/59.61 & ~ v3_struct_0(A) % 59.60/59.61 & v3_lattices(A) ) ). % 59.60/59.61 % 59.60/59.61 fof(rc7_conlat_1,axiom, % 59.60/59.61 ? [A] : % 59.60/59.61 ( l2_conlat_1(A) % 59.60/59.61 & ~ v3_conlat_1(A) % 59.60/59.61 & v4_conlat_1(A) ) ). % 59.60/59.61 % 59.60/59.61 fof(rc8_conlat_1,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_conlat_1(A) % 59.60/59.61 & l1_conlat_1(A) ) % 59.60/59.61 => ? [B] : % 59.60/59.61 ( m1_subset_1(B,k1_zfmisc_1(u1_conlat_1(A))) % 59.60/59.61 & ~ v1_xboole_0(B) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(rc9_conlat_1,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_conlat_1(A) % 59.60/59.61 & l1_conlat_1(A) ) % 59.60/59.61 => ? [B] : % 59.60/59.61 ( m1_subset_1(B,k1_zfmisc_1(u2_conlat_1(A))) % 59.60/59.61 & ~ v1_xboole_0(B) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(rc9_lattices,axiom, % 59.60/59.61 ? [A] : % 59.60/59.61 ( l3_lattices(A) % 59.60/59.61 & ~ v3_struct_0(A) % 59.60/59.61 & v3_lattices(A) % 59.60/59.61 & v4_lattices(A) % 59.60/59.61 & v5_lattices(A) % 59.60/59.61 & v6_lattices(A) % 59.60/59.61 & v7_lattices(A) % 59.60/59.61 & v8_lattices(A) % 59.60/59.61 & v9_lattices(A) % 59.60/59.61 & v10_lattices(A) ) ). % 59.60/59.61 % 59.60/59.61 fof(redefinition_k6_relset_1,axiom, % 59.60/59.61 ! [A,B,C] : % 59.60/59.61 ( m1_relset_1(C,A,B) % 59.60/59.61 => k6_relset_1(A,B,C) = k4_relat_1(C) ) ). % 59.60/59.61 % 59.60/59.61 fof(redefinition_m2_relset_1,axiom, % 59.60/59.61 ! [A,B,C] : % 59.60/59.61 ( m2_relset_1(C,A,B) % 59.60/59.61 <=> m1_relset_1(C,A,B) ) ). % 59.60/59.61 % 59.60/59.61 fof(reflexivity_r1_filter_1,axiom, % 59.60/59.61 ! [A,B] : % 59.60/59.61 ( ( ~ v3_struct_0(A) % 59.60/59.61 & v10_lattices(A) % 59.60/59.61 & l3_lattices(A) % 59.60/59.61 & ~ v3_struct_0(B) % 59.60/59.61 & v10_lattices(B) % 59.60/59.61 & l3_lattices(B) ) % 59.60/59.61 => r1_filter_1(A,A) ) ). % 59.60/59.61 % 59.60/59.61 fof(reflexivity_r1_tarski,axiom, % 59.60/59.61 ! [A,B] : r1_tarski(A,A) ). % 59.60/59.61 % 59.60/59.61 fof(symmetry_r1_filter_1,axiom, % 59.60/59.61 ! [A,B] : % 59.60/59.61 ( ( ~ v3_struct_0(A) % 59.60/59.61 & v10_lattices(A) % 59.60/59.61 & l3_lattices(A) % 59.60/59.61 & ~ v3_struct_0(B) % 59.60/59.61 & v10_lattices(B) % 59.60/59.61 & l3_lattices(B) ) % 59.60/59.61 => ( r1_filter_1(A,B) % 59.60/59.61 => r1_filter_1(B,A) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(t1_subset,axiom, % 59.60/59.61 ! [A,B] : % 59.60/59.61 ( r2_hidden(A,B) % 59.60/59.61 => m1_subset_1(A,B) ) ). % 59.60/59.61 % 59.60/59.61 fof(t21_conlat_2,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( ( ~ v3_conlat_1(A) % 59.60/59.61 & l2_conlat_1(A) ) % 59.60/59.61 => v3_lattice4(k10_conlat_2(A),k1_lattice2(k11_conlat_1(A)),k11_conlat_1(k7_conlat_2(A))) ) ). % 59.60/59.61 % 59.60/59.61 fof(t2_subset,axiom, % 59.60/59.61 ! [A,B] : % 59.60/59.61 ( m1_subset_1(A,B) % 59.60/59.61 => ( v1_xboole_0(B) % 59.60/59.61 | r2_hidden(A,B) ) ) ). % 59.60/59.61 % 59.60/59.61 fof(t3_subset,axiom, % 59.60/59.61 ! [A,B] : % 59.60/59.61 ( m1_subset_1(A,k1_zfmisc_1(B)) % 59.60/59.61 <=> r1_tarski(A,B) ) ). % 59.60/59.61 % 59.60/59.61 fof(t4_subset,axiom, % 59.60/59.61 ! [A,B,C] : % 59.60/59.61 ( ( r2_hidden(A,B) % 59.60/59.61 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 59.60/59.61 => m1_subset_1(A,C) ) ). % 59.60/59.61 % 59.60/59.61 fof(t5_subset,axiom, % 59.60/59.61 ! [A,B,C] : % 59.60/59.61 ~ ( r2_hidden(A,B) % 59.60/59.61 & m1_subset_1(B,k1_zfmisc_1(C)) % 59.60/59.61 & v1_xboole_0(C) ) ). % 59.60/59.61 % 59.60/59.61 fof(t6_boole,axiom, % 59.60/59.61 ! [A] : % 59.60/59.61 ( v1_xboole_0(A) % 59.60/59.61 => A = k1_xboole_0 ) ). % 59.60/59.61 % 59.60/59.61 fof(t7_boole,axiom, % 59.60/59.61 ! [A,B] : % 59.60/59.61 ~ ( r2_hidden(A,B) % 59.60/59.61 & v1_xboole_0(B) ) ). % 59.60/59.61 % 59.60/59.61 fof(t8_boole,axiom, % 59.60/59.61 ! [A,B] : % 59.60/59.61 ~ ( v1_xboole_0(A) % 59.60/59.61 & A != B % 59.60/59.61 & v1_xboole_0(B) ) ). % 59.60/59.61 % 59.60/59.61 %------------------------------------------------------------------------------ % 59.60/59.61 %------------------------------------------- % 59.60/59.61 % Proof found % 59.60/59.61 % SZS status Theorem for theBenchmark % 59.60/59.61 % SZS output start Proof % 59.60/59.61 %ClaNum:323(EqnAxiom:98) % 59.60/59.61 %VarNum:754(SingletonVarNum:229) % 59.60/59.61 %MaxLitNum:9 % 59.60/59.61 %MaxfuncDepth:3 % 59.60/59.61 %SharedTerms:68 % 59.60/59.61 %goalClause: 99 151 159 % 59.60/59.61 %singleGoalClaCount:3 % 59.60/59.61 [99]P1(a1) % 59.60/59.61 [100]P1(a12) % 59.60/59.61 [101]P1(a13) % 59.60/59.61 [102]P1(a16) % 59.60/59.61 [103]P5(a26) % 59.60/59.61 [104]P5(a2) % 59.60/59.61 [105]P5(a14) % 59.60/59.61 [106]P5(a17) % 59.60/59.61 [107]P5(a19) % 59.60/59.61 [108]P7(a2) % 59.60/59.61 [109]P7(a14) % 59.60/59.61 [110]P7(a17) % 59.60/59.61 [111]P7(a19) % 59.60/59.61 [112]P28(a13) % 59.60/59.61 [113]P28(a16) % 59.60/59.61 [114]P8(a2) % 59.60/59.61 [115]P8(a19) % 59.60/59.61 [116]P30(a2) % 59.60/59.61 [117]P30(a19) % 59.60/59.61 [118]P32(a2) % 59.60/59.61 [119]P32(a19) % 59.60/59.61 [120]P33(a2) % 59.60/59.61 [121]P33(a19) % 59.60/59.61 [122]P34(a2) % 59.60/59.61 [123]P34(a19) % 59.60/59.61 [124]P35(a2) % 59.60/59.61 [125]P35(a19) % 59.60/59.61 [126]P36(a2) % 59.60/59.61 [127]P36(a19) % 59.60/59.61 [128]P16(a2) % 59.60/59.61 [129]P17(a2) % 59.60/59.61 [130]P18(a2) % 59.60/59.62 [131]P19(a28) % 59.60/59.62 [132]P19(a6) % 59.60/59.62 [133]P2(a22) % 59.60/59.62 [134]P4(a25) % 59.60/59.62 [135]P4(a15) % 59.60/59.62 [136]P3(a23) % 59.60/59.62 [137]P6(a27) % 59.60/59.62 [151]~P25(a1) % 59.60/59.62 [152]~P25(a16) % 59.60/59.62 [153]~P29(a2) % 59.60/59.62 [154]~P29(a15) % 59.60/59.62 [155]~P29(a17) % 59.60/59.62 [156]~P29(a19) % 59.60/59.62 [157]~P19(a11) % 59.60/59.62 [159]~P14(f29(f36(a1)),f34(f29(a1))) % 59.60/59.62 [139]P9(x1391,x1391) % 59.60/59.62 [138]P19(f9(x1381)) % 59.60/59.62 [140]P10(f3(x1401),x1401) % 59.60/59.62 [141]P10(f9(x1411),f35(x1411)) % 59.60/59.62 [158]~P19(f35(x1581)) % 59.60/59.62 [142]P20(f7(x1421,x1422)) % 59.60/59.62 [143]P20(f10(x1431,x1432)) % 59.60/59.62 [144]P22(f7(x1441,x1442)) % 59.60/59.62 [145]P22(f10(x1451,x1452)) % 59.60/59.62 [146]P11(f4(x1461,x1462),x1461,x1462) % 59.60/59.62 [147]P11(f7(x1471,x1472),x1471,x1472) % 59.60/59.62 [148]P11(f10(x1481,x1482),x1481,x1482) % 59.60/59.62 [149]P23(f7(x1491,x1492),x1491,x1492) % 59.60/59.62 [150]P13(f5(x1501,x1502),x1501,x1502) % 59.60/59.62 [160]~P19(x1601)+E(x1601,a28) % 59.60/59.62 [161]~P5(x1611)+P2(x1611) % 59.60/59.62 [162]~P2(x1621)+P4(x1621) % 59.60/59.62 [163]~P6(x1631)+P4(x1631) % 59.60/59.62 [164]~P1(x1641)+P3(x1641) % 59.60/59.62 [165]~P5(x1651)+P6(x1651) % 59.60/59.62 [167]~P5(x1671)+P5(f34(x1671)) % 59.60/59.62 [168]~P5(x1681)+P7(f34(x1681)) % 59.60/59.62 [169]~P6(x1691)+P20(f40(x1691)) % 59.60/59.62 [170]~P2(x1701)+P20(f41(x1701)) % 59.60/59.62 [171]~P22(x1711)+P22(f37(x1711)) % 59.60/59.62 [173]P19(x1731)+~P19(f8(x1731)) % 59.60/59.62 [246]P19(x2461)+P10(f8(x2461),f35(x2461)) % 59.60/59.62 [276]~P1(x2761)+P13(f45(x2761),f42(x2761),f43(x2761)) % 59.60/59.62 [172]~P22(x1721)+E(f37(f37(x1721)),x1721) % 59.60/59.62 [283]~P6(x2831)+P23(f40(x2831),f38(f44(x2831),f44(x2831)),f44(x2831)) % 59.60/59.62 [284]~P2(x2841)+P23(f41(x2841),f38(f44(x2841),f44(x2841)),f44(x2841)) % 59.60/59.62 [285]~P6(x2851)+P13(f40(x2851),f38(f44(x2851),f44(x2851)),f44(x2851)) % 59.60/59.62 [286]~P2(x2861)+P13(f41(x2861),f38(f44(x2861),f44(x2861)),f44(x2861)) % 59.60/59.62 [244]~P19(x2441)+~P15(x2442,x2441) % 59.60/59.62 [257]~P15(x2571,x2572)+P10(x2571,x2572) % 59.60/59.62 [261]~P15(x2612,x2611)+~P15(x2611,x2612) % 59.60/59.62 [260]~P9(x2601,x2602)+P10(x2601,f35(x2602)) % 59.60/59.62 [266]P9(x2661,x2662)+~P10(x2661,f35(x2662)) % 59.60/59.62 [296]~P13(x2961,x2962,x2963)+P11(x2961,x2962,x2963) % 59.60/59.62 [297]~P11(x2971,x2972,x2973)+P13(x2971,x2972,x2973) % 59.60/59.62 [300]~P11(x3003,x3001,x3002)+E(f39(x3001,x3002,x3003),f37(x3003)) % 59.60/59.62 [305]~P11(x3053,x3051,x3052)+P1(f31(x3051,x3052,x3053)) % 59.60/59.62 [306]~P11(x3063,x3061,x3062)+P28(f31(x3061,x3062,x3063)) % 59.60/59.62 [312]~P11(x3123,x3121,x3122)+P13(f39(x3121,x3122,x3123),x3122,x3121) % 59.60/59.62 [281]P22(x2811)+~P10(x2811,f35(f38(x2812,x2813))) % 59.60/59.62 [301]~P13(x3011,x3012,x3013)+P10(x3011,f35(f38(x3012,x3013))) % 59.60/59.62 [313]~P11(x3133,x3131,x3132)+E(f39(x3131,x3132,f39(x3131,x3132,x3133)),x3133) % 59.60/59.62 [174]~P1(x1741)+P25(x1741)+P1(f36(x1741)) % 59.60/59.62 [175]~P1(x1751)+P25(x1751)+P5(f29(x1751)) % 59.60/59.62 [179]~P1(x1791)+P25(x1791)+P7(f29(x1791)) % 59.60/59.62 [180]~P1(x1801)+P25(x1801)+P28(f36(x1801)) % 59.60/59.62 [183]~P1(x1831)+P25(x1831)+P8(f29(x1831)) % 59.60/59.62 [186]~P1(x1861)+P25(x1861)+P30(f29(x1861)) % 59.60/59.62 [189]~P1(x1891)+P25(x1891)+P32(f29(x1891)) % 59.60/59.62 [192]~P1(x1921)+P25(x1921)+P33(f29(x1921)) % 59.60/59.62 [195]~P1(x1951)+P25(x1951)+P34(f29(x1951)) % 59.60/59.62 [198]~P1(x1981)+P25(x1981)+P35(f29(x1981)) % 59.60/59.62 [201]~P1(x2011)+P25(x2011)+P36(f29(x2011)) % 59.60/59.62 [202]~P1(x2021)+P25(x2021)+P16(f29(x2021)) % 59.60/59.62 [203]~P1(x2031)+P25(x2031)+P17(f29(x2031)) % 59.60/59.62 [204]~P1(x2041)+P25(x2041)+P18(f29(x2041)) % 59.60/59.62 [206]~P1(x2061)+P25(x2061)+P31(f29(x2061)) % 59.60/59.62 [216]~P1(x2161)+P25(x2161)+~P25(f36(x2161)) % 59.60/59.62 [220]~P1(x2201)+P25(x2201)+~P29(f29(x2201)) % 59.60/59.62 [221]~P3(x2211)+P25(x2211)+~P19(f42(x2211)) % 59.60/59.62 [222]~P3(x2221)+P25(x2221)+~P19(f43(x2221)) % 59.60/59.62 [223]~P3(x2231)+P25(x2231)+~P19(f20(x2231)) % 59.60/59.62 [224]~P3(x2241)+P25(x2241)+~P19(f21(x2241)) % 59.60/59.62 [225]~P5(x2251)+P29(x2251)+~P29(f34(x2251)) % 59.60/59.62 [226]~P4(x2261)+P29(x2261)+~P19(f44(x2261)) % 59.60/59.62 [227]~P4(x2271)+P29(x2271)+~P19(f18(x2271)) % 59.60/59.62 [267]~P3(x2671)+P25(x2671)+P10(f20(x2671),f35(f42(x2671))) % 59.60/59.62 [268]~P3(x2681)+P25(x2681)+P10(f21(x2681),f35(f43(x2681))) % 59.60/59.62 [269]~P4(x2691)+P29(x2691)+P10(f18(x2691),f35(f44(x2691))) % 59.60/59.62 [277]~P5(x2771)+~P7(x2771)+E(f30(f44(x2771),f40(x2771),f41(x2771)),x2771) % 59.60/59.62 [278]~P1(x2781)+~P28(x2781)+E(f31(f42(x2781),f43(x2781),f45(x2781)),x2781) % 59.60/59.62 [279]~P1(x2791)+P25(x2791)+P12(f33(x2791),f34(f29(x2791)),f29(f36(x2791))) % 59.60/59.62 [280]~P1(x2801)+P25(x2801)+P27(f33(x2801),f34(f29(x2801)),f29(f36(x2801))) % 59.60/59.62 [308]P25(x3081)+~P1(x3081)+E(f31(f43(x3081),f42(x3081),f39(f42(x3081),f43(x3081),f45(x3081))),f36(x3081)) % 59.60/59.62 [166]~P19(x1662)+~P19(x1661)+E(x1661,x1662) % 59.60/59.62 [258]~P10(x2582,x2581)+P19(x2581)+P15(x2582,x2581) % 59.60/59.62 [271]P19(x2711)+P19(x2712)+~P19(f38(x2712,x2711)) % 59.60/59.62 [273]~P19(x2731)+~P15(x2732,x2733)+~P10(x2733,f35(x2731)) % 59.60/59.62 [274]P10(x2741,x2742)+~P15(x2741,x2743)+~P10(x2743,f35(x2742)) % 59.60/59.62 [314]~P11(x3141,x3143,x3144)+E(x3141,x3142)+~E(f31(x3143,x3144,x3141),f31(x3145,x3146,x3142)) % 59.60/59.62 [315]~P11(x3154,x3153,x3151)+E(x3151,x3152)+~E(f31(x3153,x3151,x3154),f31(x3155,x3152,x3156)) % 59.60/59.62 [316]~P11(x3164,x3161,x3163)+E(x3161,x3162)+~E(f31(x3161,x3163,x3164),f31(x3162,x3165,x3166)) % 59.60/59.62 [208]P30(x2081)+~P5(x2081)+~P8(x2081)+P29(x2081) % 59.60/59.62 [209]P32(x2091)+~P5(x2091)+~P8(x2091)+P29(x2091) % 59.60/59.62 [210]P33(x2101)+~P5(x2101)+~P8(x2101)+P29(x2101) % 59.60/59.62 [211]P34(x2111)+~P5(x2111)+~P8(x2111)+P29(x2111) % 59.60/59.62 [212]P35(x2121)+~P5(x2121)+~P8(x2121)+P29(x2121) % 59.60/59.62 [213]P36(x2131)+~P5(x2131)+~P8(x2131)+P29(x2131) % 59.60/59.62 [214]P16(x2141)+~P5(x2141)+~P18(x2141)+P29(x2141) % 59.60/59.62 [215]P17(x2151)+~P5(x2151)+~P18(x2151)+P29(x2151) % 59.60/59.62 [233]~P5(x2331)+~P8(x2331)+P29(x2331)+P8(f34(x2331)) % 59.60/59.62 [234]~P5(x2341)+~P8(x2341)+P29(x2341)+P30(f34(x2341)) % 59.60/59.62 [235]~P5(x2351)+~P8(x2351)+P29(x2351)+P32(f34(x2351)) % 59.60/59.62 [236]~P5(x2361)+~P8(x2361)+P29(x2361)+P33(f34(x2361)) % 59.60/59.62 [237]~P5(x2371)+~P8(x2371)+P29(x2371)+P34(f34(x2371)) % 59.60/59.62 [238]~P5(x2381)+~P8(x2381)+P29(x2381)+P35(f34(x2381)) % 59.60/59.62 [239]~P5(x2391)+~P8(x2391)+P29(x2391)+P36(f34(x2391)) % 59.60/59.62 [240]~P30(x2401)+~P6(x2401)+P29(x2401)+P22(f40(x2401)) % 59.60/59.62 [241]~P32(x2411)+~P6(x2411)+P29(x2411)+P22(f40(x2411)) % 59.60/59.62 [242]~P33(x2421)+~P2(x2421)+P29(x2421)+P22(f41(x2421)) % 59.60/59.62 [243]~P34(x2431)+~P2(x2431)+P29(x2431)+P22(f41(x2431)) % 59.60/59.62 [262]~P30(x2621)+~P6(x2621)+P29(x2621)+P21(f40(x2621),f44(x2621)) % 59.60/59.62 [263]~P33(x2631)+~P2(x2631)+P29(x2631)+P21(f41(x2631),f44(x2631)) % 59.60/59.62 [264]~P32(x2641)+~P6(x2641)+P29(x2641)+P26(f40(x2641),f44(x2641)) % 59.60/59.62 [265]~P34(x2651)+~P2(x2651)+P29(x2651)+P26(f41(x2651),f44(x2651)) % 59.60/59.62 [288]~P30(x2881)+~P6(x2881)+P29(x2881)+P24(f40(x2881),f38(f44(x2881),f44(x2881)),f44(x2881)) % 59.60/59.62 [289]~P32(x2891)+~P6(x2891)+P29(x2891)+P24(f40(x2891),f38(f44(x2891),f44(x2891)),f44(x2891)) % 59.60/59.62 [290]~P33(x2901)+~P2(x2901)+P29(x2901)+P24(f41(x2901),f38(f44(x2901),f44(x2901)),f44(x2901)) % 59.60/59.62 [291]~P34(x2911)+~P2(x2911)+P29(x2911)+P24(f41(x2911),f38(f44(x2911),f44(x2911)),f44(x2911)) % 59.60/59.62 [309]~P20(x3091)+~P11(x3091,x3092,x3093)+~P24(x3091,x3092,x3093)+P23(x3091,x3092,x3093) % 59.60/59.62 [245]P18(x2451)+~P5(x2451)+~P16(x2451)+~P17(x2451)+P29(x2451) % 59.60/59.62 [256]~P5(x2561)+~P8(x2561)+~P31(x2561)+P29(x2561)+P31(f34(x2561)) % 59.60/59.62 [310]~P20(x3102)+~P11(x3102,x3103,x3101)+~P23(x3102,x3103,x3101)+P19(x3101)+P24(x3102,x3103,x3101) % 59.60/59.62 [304]~P19(x3043)+~P11(x3043,x3042,x3041)+~P23(x3043,x3042,x3041)+P19(x3041)+P19(x3042)+~P20(x3043) % 59.60/59.62 [270]P14(x2702,x2702)+~P5(x2701)+~P5(x2702)+~P8(x2701)+~P8(x2702)+P29(x2701)+P29(x2702) % 59.60/59.62 [282]~P5(x2821)+~P5(x2822)+~P8(x2821)+~P8(x2822)+P29(x2821)+P29(x2822)+P12(f32(x2822,x2821),x2822,x2821) % 59.60/59.62 [317]~P20(x3173)+~P20(x3172)+~P11(x3173,f38(x3171,x3171),x3171)+~P11(x3172,f38(x3171,x3171),x3171)+~P23(x3173,f38(x3171,x3171),x3171)+~P23(x3172,f38(x3171,x3171),x3171)+P5(f30(x3171,x3172,x3173)) % 59.60/59.62 [318]~P20(x3183)+~P20(x3182)+~P11(x3183,f38(x3181,x3181),x3181)+~P11(x3182,f38(x3181,x3181),x3181)+~P23(x3183,f38(x3181,x3181),x3181)+~P23(x3182,f38(x3181,x3181),x3181)+P7(f30(x3181,x3182,x3183)) % 59.60/59.62 [275]P14(x2751,x2752)+~P5(x2751)+~P5(x2752)+~P8(x2751)+~P8(x2752)+~P14(x2752,x2751)+P29(x2751)+P29(x2752) % 59.60/59.62 [298]~P5(x2981)+~P5(x2982)+~P8(x2981)+~P8(x2982)+~P14(x2982,x2981)+P29(x2981)+P29(x2982)+P12(f24(x2982,x2981),x2982,x2981) % 59.60/59.62 [299]~P5(x2991)+~P5(x2992)+~P8(x2991)+~P8(x2992)+~P14(x2992,x2991)+P29(x2991)+P29(x2992)+P27(f24(x2992,x2991),x2992,x2991) % 59.60/59.62 [287]~P5(x2872)+~P5(x2873)+~P8(x2872)+~P8(x2873)+~P12(x2871,x2873,x2872)+P20(x2871)+P29(x2872)+P29(x2873) % 59.60/59.62 [302]~P5(x3021)+~P5(x3022)+~P8(x3021)+~P8(x3022)+~P12(x3023,x3022,x3021)+P29(x3021)+P29(x3022)+P23(x3023,f44(x3022),f44(x3021)) % 59.60/59.62 [303]~P5(x3031)+~P5(x3032)+~P8(x3031)+~P8(x3032)+~P12(x3033,x3032,x3031)+P29(x3031)+P29(x3032)+P13(x3033,f44(x3032),f44(x3031)) % 59.60/59.62 [323]P19(x3231)+~P20(x3232)+~P20(x3233)+~P11(x3232,f38(x3231,x3231),x3231)+~P11(x3233,f38(x3231,x3231),x3231)+~P23(x3232,f38(x3231,x3231),x3231)+~P23(x3233,f38(x3231,x3231),x3231)+~P29(f30(x3231,x3233,x3232)) % 59.60/59.62 [320]~P20(x3204)+~P20(x3201)+E(x3201,x3202)+~P11(x3204,f38(x3203,x3203),x3203)+~P11(x3201,f38(x3203,x3203),x3203)+~P23(x3204,f38(x3203,x3203),x3203)+~P23(x3201,f38(x3203,x3203),x3203)+~E(f30(x3203,x3204,x3201),f30(x3205,x3206,x3202)) % 59.60/59.62 [321]~P20(x3214)+~P20(x3211)+E(x3211,x3212)+~P11(x3214,f38(x3213,x3213),x3213)+~P11(x3211,f38(x3213,x3213),x3213)+~P23(x3214,f38(x3213,x3213),x3213)+~P23(x3211,f38(x3213,x3213),x3213)+~E(f30(x3213,x3211,x3214),f30(x3215,x3212,x3216)) % 59.60/59.62 [322]~P20(x3224)+~P20(x3223)+E(x3221,x3222)+~P11(x3224,f38(x3221,x3221),x3221)+~P11(x3223,f38(x3221,x3221),x3221)+~P23(x3224,f38(x3221,x3221),x3221)+~P23(x3223,f38(x3221,x3221),x3221)+~E(f30(x3221,x3223,x3224),f30(x3222,x3225,x3226)) % 59.60/59.62 [272]P8(x2721)+~P5(x2721)+~P30(x2721)+~P32(x2721)+~P33(x2721)+~P34(x2721)+~P35(x2721)+~P36(x2721)+P29(x2721) % 59.60/59.62 [307]P14(x3072,x3071)+~P5(x3071)+~P5(x3072)+~P8(x3071)+~P8(x3072)+~P27(x3073,x3072,x3071)+P29(x3071)+~P12(x3073,x3072,x3071)+P29(x3072) % 59.60/59.62 %EqnAxiom % 59.60/59.62 [1]E(x11,x11) % 59.60/59.62 [2]E(x22,x21)+~E(x21,x22) % 59.60/59.62 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.60/59.62 [4]~E(x41,x42)+E(f9(x41),f9(x42)) % 59.60/59.62 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 59.60/59.62 [6]~E(x61,x62)+E(f38(x61,x63),f38(x62,x63)) % 59.60/59.62 [7]~E(x71,x72)+E(f38(x73,x71),f38(x73,x72)) % 59.60/59.62 [8]~E(x81,x82)+E(f35(x81),f35(x82)) % 59.60/59.62 [9]~E(x91,x92)+E(f7(x91,x93),f7(x92,x93)) % 59.60/59.62 [10]~E(x101,x102)+E(f7(x103,x101),f7(x103,x102)) % 59.60/59.62 [11]~E(x111,x112)+E(f10(x111,x113),f10(x112,x113)) % 59.60/59.62 [12]~E(x121,x122)+E(f10(x123,x121),f10(x123,x122)) % 59.60/59.62 [13]~E(x131,x132)+E(f43(x131),f43(x132)) % 59.60/59.62 [14]~E(x141,x142)+E(f44(x141),f44(x142)) % 59.60/59.62 [15]~E(x151,x152)+E(f4(x151,x153),f4(x152,x153)) % 59.60/59.62 [16]~E(x161,x162)+E(f4(x163,x161),f4(x163,x162)) % 59.60/59.62 [17]~E(x171,x172)+E(f31(x171,x173,x174),f31(x172,x173,x174)) % 59.60/59.62 [18]~E(x181,x182)+E(f31(x183,x181,x184),f31(x183,x182,x184)) % 59.60/59.62 [19]~E(x191,x192)+E(f31(x193,x194,x191),f31(x193,x194,x192)) % 59.60/59.62 [20]~E(x201,x202)+E(f39(x201,x203,x204),f39(x202,x203,x204)) % 59.60/59.62 [21]~E(x211,x212)+E(f39(x213,x211,x214),f39(x213,x212,x214)) % 59.60/59.62 [22]~E(x221,x222)+E(f39(x223,x224,x221),f39(x223,x224,x222)) % 59.60/59.62 [23]~E(x231,x232)+E(f30(x231,x233,x234),f30(x232,x233,x234)) % 59.60/59.62 [24]~E(x241,x242)+E(f30(x243,x241,x244),f30(x243,x242,x244)) % 59.60/59.62 [25]~E(x251,x252)+E(f30(x253,x254,x251),f30(x253,x254,x252)) % 59.60/59.62 [26]~E(x261,x262)+E(f5(x261,x263),f5(x262,x263)) % 59.60/59.62 [27]~E(x271,x272)+E(f5(x273,x271),f5(x273,x272)) % 59.60/59.62 [28]~E(x281,x282)+E(f41(x281),f41(x282)) % 59.60/59.62 [29]~E(x291,x292)+E(f36(x291),f36(x292)) % 59.60/59.62 [30]~E(x301,x302)+E(f29(x301),f29(x302)) % 59.60/59.62 [31]~E(x311,x312)+E(f45(x311),f45(x312)) % 59.60/59.62 [32]~E(x321,x322)+E(f34(x321),f34(x322)) % 59.60/59.62 [33]~E(x331,x332)+E(f33(x331),f33(x332)) % 59.60/59.62 [34]~E(x341,x342)+E(f40(x341),f40(x342)) % 59.60/59.62 [35]~E(x351,x352)+E(f42(x351),f42(x352)) % 59.60/59.62 [36]~E(x361,x362)+E(f24(x361,x363),f24(x362,x363)) % 59.60/59.62 [37]~E(x371,x372)+E(f24(x373,x371),f24(x373,x372)) % 59.60/59.62 [38]~E(x381,x382)+E(f37(x381),f37(x382)) % 59.60/59.62 [39]~E(x391,x392)+E(f21(x391),f21(x392)) % 59.60/59.62 [40]~E(x401,x402)+E(f32(x401,x403),f32(x402,x403)) % 59.60/59.62 [41]~E(x411,x412)+E(f32(x413,x411),f32(x413,x412)) % 59.60/59.62 [42]~E(x421,x422)+E(f8(x421),f8(x422)) % 59.60/59.62 [43]~E(x431,x432)+E(f20(x431),f20(x432)) % 59.60/59.62 [44]~E(x441,x442)+E(f18(x441),f18(x442)) % 59.60/59.62 [45]~P1(x451)+P1(x452)+~E(x451,x452) % 59.60/59.62 [46]P23(x462,x463,x464)+~E(x461,x462)+~P23(x461,x463,x464) % 59.60/59.62 [47]P23(x473,x472,x474)+~E(x471,x472)+~P23(x473,x471,x474) % 59.60/59.62 [48]P23(x483,x484,x482)+~E(x481,x482)+~P23(x483,x484,x481) % 59.60/59.62 [49]P11(x492,x493,x494)+~E(x491,x492)+~P11(x491,x493,x494) % 59.60/59.62 [50]P11(x503,x502,x504)+~E(x501,x502)+~P11(x503,x501,x504) % 59.60/59.62 [51]P11(x513,x514,x512)+~E(x511,x512)+~P11(x513,x514,x511) % 59.60/59.62 [52]~P8(x521)+P8(x522)+~E(x521,x522) % 59.60/59.62 [53]~P5(x531)+P5(x532)+~E(x531,x532) % 59.60/59.62 [54]~P32(x541)+P32(x542)+~E(x541,x542) % 59.60/59.62 [55]P24(x552,x553,x554)+~E(x551,x552)+~P24(x551,x553,x554) % 59.60/59.62 [56]P24(x563,x562,x564)+~E(x561,x562)+~P24(x563,x561,x564) % 59.60/59.62 [57]P24(x573,x574,x572)+~E(x571,x572)+~P24(x573,x574,x571) % 59.60/59.62 [58]~P29(x581)+P29(x582)+~E(x581,x582) % 59.60/59.62 [59]~P6(x591)+P6(x592)+~E(x591,x592) % 59.60/59.62 [60]~P7(x601)+P7(x602)+~E(x601,x602) % 59.60/59.62 [61]~P22(x611)+P22(x612)+~E(x611,x612) % 59.60/59.62 [62]~P33(x621)+P33(x622)+~E(x621,x622) % 59.60/59.62 [63]~P2(x631)+P2(x632)+~E(x631,x632) % 59.60/59.62 [64]~P28(x641)+P28(x642)+~E(x641,x642) % 59.60/59.62 [65]~P19(x651)+P19(x652)+~E(x651,x652) % 59.60/59.62 [66]~P3(x661)+P3(x662)+~E(x661,x662) % 59.60/59.62 [67]P10(x672,x673)+~E(x671,x672)+~P10(x671,x673) % 59.60/59.62 [68]P10(x683,x682)+~E(x681,x682)+~P10(x683,x681) % 59.60/59.62 [69]~P30(x691)+P30(x692)+~E(x691,x692) % 59.60/59.62 [70]P15(x702,x703)+~E(x701,x702)+~P15(x701,x703) % 59.60/59.62 [71]P15(x713,x712)+~E(x711,x712)+~P15(x713,x711) % 59.60/59.62 [72]P12(x722,x723,x724)+~E(x721,x722)+~P12(x721,x723,x724) % 59.60/59.62 [73]P12(x733,x732,x734)+~E(x731,x732)+~P12(x733,x731,x734) % 59.60/59.62 [74]P12(x743,x744,x742)+~E(x741,x742)+~P12(x743,x744,x741) % 59.60/59.62 [75]~P25(x751)+P25(x752)+~E(x751,x752) % 59.60/59.62 [76]~P34(x761)+P34(x762)+~E(x761,x762) % 59.60/59.62 [77]~P4(x771)+P4(x772)+~E(x771,x772) % 59.60/59.62 [78]~P18(x781)+P18(x782)+~E(x781,x782) % 59.60/59.62 [79]~P35(x791)+P35(x792)+~E(x791,x792) % 59.60/59.62 [80]P14(x802,x803)+~E(x801,x802)+~P14(x801,x803) % 59.60/59.62 [81]P14(x813,x812)+~E(x811,x812)+~P14(x813,x811) % 59.60/59.62 [82]~P20(x821)+P20(x822)+~E(x821,x822) % 59.60/59.62 [83]~P36(x831)+P36(x832)+~E(x831,x832) % 59.60/59.62 [84]P26(x842,x843)+~E(x841,x842)+~P26(x841,x843) % 59.60/59.62 [85]P26(x853,x852)+~E(x851,x852)+~P26(x853,x851) % 59.60/59.62 [86]~P16(x861)+P16(x862)+~E(x861,x862) % 59.60/59.62 [87]~P17(x871)+P17(x872)+~E(x871,x872) % 59.60/59.62 [88]P13(x882,x883,x884)+~E(x881,x882)+~P13(x881,x883,x884) % 59.60/59.62 [89]P13(x893,x892,x894)+~E(x891,x892)+~P13(x893,x891,x894) % 59.60/59.62 [90]P13(x903,x904,x902)+~E(x901,x902)+~P13(x903,x904,x901) % 59.60/59.62 [91]P9(x912,x913)+~E(x911,x912)+~P9(x911,x913) % 59.60/59.62 [92]P9(x923,x922)+~E(x921,x922)+~P9(x923,x921) % 59.60/59.62 [93]~P31(x931)+P31(x932)+~E(x931,x932) % 59.60/59.62 [94]P21(x942,x943)+~E(x941,x942)+~P21(x941,x943) % 59.60/59.62 [95]P21(x953,x952)+~E(x951,x952)+~P21(x953,x951) % 59.60/59.62 [96]P27(x962,x963,x964)+~E(x961,x962)+~P27(x961,x963,x964) % 59.60/59.62 [97]P27(x973,x972,x974)+~E(x971,x972)+~P27(x973,x971,x974) % 59.60/59.62 [98]P27(x983,x984,x982)+~E(x981,x982)+~P27(x983,x984,x981) % 59.60/59.62 % 59.60/59.62 %------------------------------------------- % 59.60/59.62 cnf(330,plain, % 59.60/59.62 (~P15(x3301,a28)), % 59.60/59.62 inference(scs_inference,[],[131,244])). % 59.60/59.62 cnf(333,plain, % 59.60/59.62 (P10(f3(x3331),x3331)), % 59.60/59.62 inference(rename_variables,[],[140])). % 59.60/59.62 cnf(336,plain, % 59.60/59.62 (P10(f3(x3361),x3361)), % 59.60/59.62 inference(rename_variables,[],[140])). % 59.60/59.62 cnf(338,plain, % 59.60/59.62 (P15(f3(a11),a11)), % 59.60/59.62 inference(scs_inference,[],[140,333,336,131,157,244,266,281,258])). % 59.60/59.62 cnf(339,plain, % 59.60/59.62 (P10(f3(x3391),x3391)), % 59.60/59.62 inference(rename_variables,[],[140])). % 59.60/59.62 cnf(341,plain, % 59.60/59.62 (~P15(x3411,f3(f35(a28)))), % 59.60/59.62 inference(scs_inference,[],[140,333,336,339,131,157,244,266,281,258,273])). % 59.60/59.62 cnf(344,plain, % 59.60/59.62 (P24(f7(x3441,a11),x3441,a11)), % 59.60/59.62 inference(scs_inference,[],[147,149,140,333,336,339,131,157,142,244,266,281,258,273,310])). % 59.60/59.62 cnf(345,plain, % 59.60/59.62 (P23(f7(x3451,x3452),x3451,x3452)), % 59.60/59.62 inference(rename_variables,[],[149])). % 59.60/59.62 cnf(346,plain, % 59.60/59.62 (P20(f7(x3461,x3462))), % 59.60/59.62 inference(rename_variables,[],[142])). % 59.60/59.62 cnf(347,plain, % 59.60/59.62 (P11(f7(x3471,x3472),x3471,x3472)), % 59.60/59.62 inference(rename_variables,[],[147])). % 59.60/59.62 cnf(349,plain, % 59.60/59.62 (~P19(f7(a11,a11))), % 59.60/59.62 inference(scs_inference,[],[147,347,149,345,140,333,336,339,131,157,142,346,244,266,281,258,273,310,304])). % 59.60/59.62 cnf(363,plain, % 59.60/59.62 (P9(f9(x3631),x3631)), % 59.60/59.62 inference(scs_inference,[],[141,266])). % 59.60/59.62 cnf(365,plain, % 59.60/59.62 (~P15(x3651,a6)), % 59.60/59.62 inference(scs_inference,[],[141,132,266,244])). % 59.60/59.62 cnf(368,plain, % 59.60/59.62 (P10(f9(x3681),f35(x3681))), % 59.60/59.62 inference(rename_variables,[],[141])). % 59.60/59.62 cnf(370,plain, % 59.60/59.62 (~P15(x3701,f9(a6))), % 59.60/59.62 inference(scs_inference,[],[141,368,132,266,244,281,273])). % 59.60/59.62 cnf(373,plain, % 59.60/59.62 (P15(f3(f7(a11,a11)),f7(a11,a11))), % 59.60/59.62 inference(scs_inference,[],[141,368,349,132,140,266,244,281,273,258])). % 59.60/59.62 cnf(378,plain, % 59.60/59.62 (P24(f7(x3781,f7(a11,a11)),x3781,f7(a11,a11))), % 59.60/59.62 inference(scs_inference,[],[341,141,368,349,338,132,147,149,140,142,266,244,281,273,258,71,310])). % 59.60/59.62 cnf(379,plain, % 59.60/59.62 (P23(f7(x3791,x3792),x3791,x3792)), % 59.60/59.62 inference(rename_variables,[],[149])). % 59.60/59.62 cnf(380,plain, % 59.60/59.62 (P20(f7(x3801,x3802))), % 59.60/59.62 inference(rename_variables,[],[142])). % 59.60/59.62 cnf(381,plain, % 59.60/59.62 (P11(f7(x3811,x3812),x3811,x3812)), % 59.60/59.62 inference(rename_variables,[],[147])). % 59.60/59.62 cnf(383,plain, % 59.60/59.62 (~P19(f7(f7(a11,a11),f7(a11,a11)))), % 59.60/59.62 inference(scs_inference,[],[341,141,368,349,338,132,147,381,149,379,140,142,380,266,244,281,273,258,71,310,304])). % 59.60/59.62 cnf(388,plain, % 59.60/59.62 (P14(a19,a19)), % 59.60/59.62 inference(scs_inference,[],[107,341,141,368,349,338,115,132,156,147,381,149,379,140,142,380,266,244,281,273,258,71,310,304,270])). % 59.60/59.62 cnf(390,plain, % 59.60/59.62 (~P15(f7(a11,a11),f3(f7(a11,a11)))), % 59.60/59.62 inference(scs_inference,[],[107,341,141,368,349,338,115,132,156,147,381,149,379,140,142,380,266,244,281,273,258,71,310,304,270,261])). % 59.60/59.62 cnf(393,plain, % 59.60/59.62 (P24(x3931,x3932,a11)+~E(f7(x3932,a11),x3931)), % 59.60/59.62 inference(scs_inference,[],[107,341,148,344,141,368,349,338,115,132,156,147,381,149,379,140,142,380,266,244,281,273,258,71,310,304,270,261,51,55])). % 59.60/59.62 cnf(394,plain, % 59.60/59.62 (P24(f7(x3941,a11),x3942,a11)+~E(x3941,x3942)), % 59.60/59.62 inference(scs_inference,[],[107,341,148,344,141,368,349,338,115,132,156,147,381,149,379,140,142,380,266,244,281,273,258,71,310,304,270,261,51,55,56])). % 59.60/59.62 cnf(404,plain, % 59.60/59.62 (~P15(x4041,f9(x4042))), % 59.60/59.62 inference(scs_inference,[],[138,244])). % 59.60/59.62 cnf(406,plain, % 59.60/59.62 (P15(f3(f7(f7(a11,a11),f7(a11,a11))),f7(f7(a11,a11),f7(a11,a11)))), % 59.60/59.62 inference(scs_inference,[],[383,138,140,244,258])). % 59.60/59.62 cnf(407,plain, % 59.60/59.62 (P10(f3(x4071),x4071)), % 59.60/59.62 inference(rename_variables,[],[140])). % 59.60/59.62 cnf(409,plain, % 59.60/59.62 (~P15(x4091,f3(f35(f9(x4092))))), % 59.60/59.62 inference(scs_inference,[],[383,138,140,407,244,258,273])). % 59.60/59.62 cnf(414,plain, % 59.60/59.62 (P24(f7(x4141,f7(f7(a11,a11),f7(a11,a11))),x4141,f7(f7(a11,a11),f7(a11,a11)))), % 59.60/59.62 inference(scs_inference,[],[370,383,373,138,147,149,140,407,142,244,258,273,71,310])). % 59.60/59.62 cnf(415,plain, % 59.60/59.62 (P23(f7(x4151,x4152),x4151,x4152)), % 59.60/59.62 inference(rename_variables,[],[149])). % 59.60/59.62 cnf(416,plain, % 59.60/59.62 (P20(f7(x4161,x4162))), % 59.60/59.62 inference(rename_variables,[],[142])). % 59.60/59.62 cnf(417,plain, % 59.60/59.62 (P11(f7(x4171,x4172),x4171,x4172)), % 59.60/59.62 inference(rename_variables,[],[147])). % 59.60/59.62 cnf(419,plain, % 59.60/59.62 (~P19(f7(f7(f7(a11,a11),f7(a11,a11)),f7(f7(a11,a11),f7(a11,a11))))), % 59.60/59.62 inference(scs_inference,[],[370,383,373,138,147,417,149,415,140,407,142,416,244,258,273,71,310,304])). % 59.60/59.62 cnf(430,plain, % 59.60/59.62 (P9(x4301,x4302)+~E(x4302,x4301)), % 59.60/59.62 inference(scs_inference,[],[139,370,383,150,373,138,147,417,149,415,140,407,142,416,244,258,273,71,310,304,261,70,88,89,90,91])). % 59.60/59.62 cnf(438,plain, % 59.60/59.62 (P15(f9(x4381),f35(x4381))), % 59.60/59.62 inference(scs_inference,[],[141,158,258])). % 59.60/59.62 cnf(450,plain, % 59.60/59.62 (~P15(x4501,f3(f35(a6)))), % 59.60/59.62 inference(scs_inference,[],[132,140,273])). % 59.60/59.62 cnf(469,plain, % 59.60/59.62 (P24(f7(x4691,f35(x4692)),x4691,f35(x4692))), % 59.60/59.62 inference(scs_inference,[],[373,158,450,147,142,149,71,310])). % 59.60/59.62 cnf(470,plain, % 59.60/59.62 (P23(f7(x4701,x4702),x4701,x4702)), % 59.60/59.62 inference(rename_variables,[],[149])). % 59.60/59.62 cnf(471,plain, % 59.60/59.62 (P20(f7(x4711,x4712))), % 59.60/59.62 inference(rename_variables,[],[142])). % 59.60/59.62 cnf(472,plain, % 59.60/59.62 (P11(f7(x4721,x4722),x4721,x4722)), % 59.60/59.62 inference(rename_variables,[],[147])). % 59.60/59.62 cnf(475,plain, % 59.60/59.62 (P23(f7(x4751,x4752),x4751,x4752)), % 59.60/59.62 inference(rename_variables,[],[149])). % 59.60/59.62 cnf(480,plain, % 59.60/59.62 (P15(f3(f7(f35(x4801),f35(x4801))),f7(f35(x4801),f35(x4801)))), % 59.60/59.62 inference(scs_inference,[],[373,158,450,146,147,472,142,471,149,470,140,71,310,304,51,258])). % 59.60/59.62 cnf(486,plain, % 59.60/59.62 (P24(f7(x4861,f7(a11,a11)),x4862,f7(a11,a11))+~E(x4861,x4862)), % 59.60/59.62 inference(scs_inference,[],[378,373,158,450,146,147,472,142,471,149,470,475,140,71,310,304,51,258,261,46,56])). % 59.60/59.62 cnf(488,plain, % 59.60/59.62 (P24(x4881,x4882,f7(a11,a11))+~E(f7(x4882,f7(a11,a11)),x4881)), % 59.60/59.62 inference(scs_inference,[],[378,373,158,363,450,146,147,472,142,471,149,470,475,140,71,310,304,51,258,261,46,56,92,55])). % 59.60/59.62 cnf(496,plain, % 59.60/59.62 (~E(a11,a28)), % 59.60/59.62 inference(scs_inference,[],[338,330,71])). % 59.60/59.62 cnf(498,plain, % 59.60/59.62 (P10(x4981,x4982)+~E(f3(x4982),x4981)), % 59.60/59.62 inference(scs_inference,[],[338,140,330,71,67])). % 59.60/59.62 cnf(511,plain, % 59.60/59.62 (P24(f7(x5111,f7(f7(a11,a11),f7(a11,a11))),x5112,f7(f7(a11,a11),f7(a11,a11)))+~E(x5111,x5112)), % 59.60/59.62 inference(scs_inference,[],[388,414,406,149,148,365,71,57,48,50,70,81,56])). % 59.60/59.62 cnf(522,plain, % 59.60/59.62 (P24(x5221,x5222,f7(f7(a11,a11),f7(a11,a11)))+~E(f7(x5222,f7(f7(a11,a11),f7(a11,a11))),x5221)), % 59.60/59.62 inference(scs_inference,[],[414,373,148,404,147,71,49,51,55])). % 59.60/59.62 cnf(542,plain, % 59.60/59.62 (P24(x5421,x5422,f35(x5423))+~E(f7(x5422,f35(x5423)),x5421)), % 59.60/59.62 inference(scs_inference,[],[373,469,341,71,56,55])). % 59.60/59.62 cnf(551,plain, % 59.60/59.62 (~E(f7(a11,a11),a28)), % 59.60/59.62 inference(scs_inference,[],[373,330,71])). % 59.60/59.62 cnf(565,plain, % 59.60/59.62 (~E(a11,f9(x5651))), % 59.60/59.62 inference(scs_inference,[],[338,404,71])). % 59.60/59.62 cnf(578,plain, % 59.60/59.62 (P4(a2)), % 59.60/59.62 inference(scs_inference,[],[104,161,162])). % 59.60/59.62 cnf(597,plain, % 59.60/59.62 (~E(a11,a6)), % 59.60/59.62 inference(scs_inference,[],[338,365,71])). % 59.60/59.62 cnf(628,plain, % 59.60/59.62 (~E(f7(f35(x6281),f35(x6281)),f9(x6282))), % 59.60/59.62 inference(scs_inference,[],[480,404,71])). % 59.60/59.62 cnf(650,plain, % 59.60/59.62 (~E(f7(f35(x6501),f35(x6501)),a6)), % 59.60/59.62 inference(scs_inference,[],[480,365,71])). % 59.60/59.62 cnf(668,plain, % 59.60/59.62 (~P19(f42(a1))), % 59.60/59.62 inference(scs_inference,[],[99,151,164,221])). % 59.60/59.62 cnf(675,plain, % 59.60/59.62 (P23(f7(x6751,x6752),x6751,x6752)), % 59.60/59.62 inference(rename_variables,[],[149])). % 59.60/59.62 cnf(676,plain, % 59.60/59.62 (P20(f7(x6761,x6762))), % 59.60/59.62 inference(rename_variables,[],[142])). % 59.60/59.62 cnf(677,plain, % 59.60/59.62 (P11(f7(x6771,x6772),x6771,x6772)), % 59.60/59.62 inference(rename_variables,[],[147])). % 59.60/59.62 cnf(679,plain, % 59.60/59.62 (~P19(f7(f42(a1),f42(a1)))), % 59.60/59.62 inference(scs_inference,[],[668,140,149,675,147,677,142,676,404,258,71,310,304])). % 59.60/59.62 cnf(687,plain, % 59.60/59.62 (P24(f7(x6871,f42(a1)),x6872,f42(a1))+~E(x6871,x6872)), % 59.60/59.62 inference(scs_inference,[],[668,140,149,675,147,677,142,676,404,258,71,310,304,261,57,56])). % 59.60/59.62 cnf(689,plain, % 59.60/59.62 (P24(x6891,x6892,f42(a1))+~E(f7(x6892,f42(a1)),x6891)), % 59.60/59.62 inference(scs_inference,[],[668,140,149,675,147,677,142,676,404,258,71,310,304,261,57,56,70,55])). % 59.60/59.62 cnf(696,plain, % 59.60/59.62 (P15(f3(f7(f42(a1),f42(a1))),f7(f42(a1),f42(a1)))), % 59.60/59.62 inference(scs_inference,[],[140,679,258])). % 59.60/59.62 cnf(723,plain, % 59.60/59.62 (~E(f7(f42(a1),f42(a1)),f9(x7231))), % 59.60/59.62 inference(scs_inference,[],[696,404,71])). % 59.60/59.62 cnf(743,plain, % 59.60/59.62 (~E(f7(f42(a1),f42(a1)),a6)), % 59.60/59.62 inference(scs_inference,[],[696,365,71])). % 59.60/59.62 cnf(926,plain, % 59.60/59.62 (~P19(f8(a11))), % 59.60/59.62 inference(scs_inference,[],[496,160,173])). % 59.60/59.62 cnf(927,plain, % 59.60/59.62 (P15(f3(f8(a11)),f8(a11))), % 59.60/59.62 inference(scs_inference,[],[140,926,258])). % 59.60/59.62 cnf(950,plain, % 59.60/59.62 (~E(f8(a11),a28)), % 59.60/59.62 inference(scs_inference,[],[927,330,71])). % 59.60/59.62 cnf(967,plain, % 59.60/59.62 (P5(f34(f29(a1)))), % 59.60/59.62 inference(scs_inference,[],[151,99,167,175])). % 59.60/59.62 cnf(1073,plain, % 59.60/59.62 (~P15(f35(x10731),f3(f35(x10731)))), % 59.60/59.62 inference(scs_inference,[],[140,158,258,261])). % 59.60/59.62 cnf(1075,plain, % 59.60/59.62 (P15(x10751,f35(x10752))+~E(f3(f35(x10752)),x10751)), % 59.60/59.62 inference(scs_inference,[],[140,158,258,261,70])). % 59.60/59.62 cnf(1441,plain, % 59.60/59.62 (P10(f8(a11),f35(a11))), % 59.60/59.62 inference(scs_inference,[],[496,246,160])). % 59.60/59.62 cnf(1476,plain, % 59.60/59.62 (~E(x14761,x14762)+P10(x14762,f35(x14761))), % 59.60/59.62 inference(scs_inference,[],[260,430])). % 59.60/59.62 cnf(1477,plain, % 59.60/59.62 (P10(x14771,f35(x14771))), % 59.60/59.62 inference(equality_inference,[],[1476])). % 59.60/59.62 cnf(1478,plain, % 59.60/59.62 (P22(f38(x14781,x14782))), % 59.60/59.62 inference(scs_inference,[],[1477,281])). % 59.60/59.62 cnf(1479,plain, % 59.60/59.62 (P10(x14791,f35(x14791))), % 59.60/59.62 inference(rename_variables,[],[1477])). % 59.60/59.62 cnf(1481,plain, % 59.60/59.62 (P10(x14811,x14812)+~E(f35(x14811),x14812)), % 59.60/59.62 inference(scs_inference,[],[1477,1479,281,68])). % 59.60/59.62 cnf(1502,plain, % 59.60/59.62 (E(f9(f39(x15021,x15022,f10(x15021,x15022))),f9(f37(f10(x15021,x15022))))), % 59.60/59.62 inference(scs_inference,[],[148,4,300])). % 59.60/59.62 cnf(1534,plain, % 59.60/59.62 (E(f35(f39(x15341,x15342,f10(x15341,x15342))),f35(f37(f10(x15341,x15342))))), % 59.60/59.62 inference(scs_inference,[],[148,8,300])). % 59.60/59.62 cnf(1595,plain, % 59.60/59.62 (P15(f8(a11),f35(a11))), % 59.60/59.62 inference(scs_inference,[],[1441,158,258])). % 59.60/59.62 cnf(1598,plain, % 59.60/59.62 (~P15(f35(a11),f8(a11))), % 59.60/59.62 inference(scs_inference,[],[1441,158,258,261])). % 59.60/59.62 cnf(1604,plain, % 59.60/59.62 (~P10(f35(a11),f8(a11))), % 59.60/59.62 inference(scs_inference,[],[926,1598,258])). % 59.60/59.62 cnf(1819,plain, % 59.60/59.62 (P1(f31(x18191,x18192,f5(x18191,x18192)))), % 59.60/59.62 inference(scs_inference,[],[150,296,305])). % 59.60/59.62 cnf(1835,plain, % 59.60/59.62 (P10(f10(x18351,x18352),f35(f38(x18351,x18352)))), % 59.60/59.62 inference(scs_inference,[],[148,297,301])). % 59.60/59.62 cnf(1841,plain, % 59.60/59.62 (~P15(f35(f38(x18411,x18412)),f10(x18411,x18412))), % 59.60/59.62 inference(scs_inference,[],[1835,158,266,258,261])). % 59.60/59.62 cnf(1845,plain, % 59.60/59.62 (P15(x18451,f35(f38(x18452,x18453)))+~E(f10(x18452,x18453),x18451)), % 59.60/59.62 inference(scs_inference,[],[1835,158,266,258,261,273,70])). % 59.60/59.62 cnf(1912,plain, % 59.60/59.62 (P28(f31(x19121,x19122,f5(x19121,x19122)))), % 59.60/59.62 inference(scs_inference,[],[150,306,296])). % 59.60/59.62 cnf(2040,plain, % 59.60/59.62 (E(f7(f39(x20401,x20402,f10(x20401,x20402)),x20403),f7(f37(f10(x20401,x20402)),x20403))), % 59.60/59.62 inference(scs_inference,[],[148,9,300])). % 59.60/59.62 cnf(2104,plain, % 59.60/59.62 (E(f4(f39(x21041,x21042,f10(x21041,x21042)),x21043),f4(f37(f10(x21041,x21042)),x21043))), % 59.60/59.62 inference(scs_inference,[],[148,15,300])). % 59.60/59.62 cnf(4007,plain, % 59.60/59.62 (~E(x40071,x40072)+P28(f31(x40072,x40073,f5(x40071,x40073)))), % 59.60/59.62 inference(scs_inference,[],[1912,64,17])). % 59.60/59.62 cnf(4024,plain, % 59.60/59.62 (~E(f31(x40241,a28,f10(x40241,a28)),f31(x40242,f42(a1),x40243))), % 59.60/59.62 inference(scs_inference,[],[131,668,148,65,315])). % 59.60/59.62 cnf(4235,plain, % 59.60/59.62 (~P15(f35(f38(x42351,x42352)),x42353)+~E(x42353,f10(x42351,x42352))), % 59.60/59.62 inference(scs_inference,[],[1841,71])). % 59.60/59.62 cnf(4288,plain, % 59.60/59.62 (~P15(f35(x42881),x42882)+~E(x42882,f3(f35(x42881)))), % 59.60/59.62 inference(scs_inference,[],[1073,71])). % 59.60/59.62 cnf(4372,plain, % 59.60/59.62 (P19(f3(f35(a28)))), % 59.60/59.62 inference(scs_inference,[],[140,341,258])). % 59.60/59.62 cnf(4377,plain, % 59.60/59.62 (P19(f3(f35(a6)))), % 59.60/59.62 inference(scs_inference,[],[140,450,258])). % 59.60/59.62 cnf(4382,plain, % 59.60/59.62 (P19(f3(f35(f9(x43821))))), % 59.60/59.62 inference(scs_inference,[],[140,409,258])). % 59.60/59.62 cnf(4483,plain, % 59.60/59.62 (~E(f31(x44831,f42(a1),x44832),f31(x44833,a28,f10(x44833,a28)))), % 59.60/59.62 inference(scs_inference,[],[4024,2])). % 59.60/59.62 cnf(4568,plain, % 59.60/59.62 (~E(a28,a11)), % 59.60/59.62 inference(scs_inference,[],[496,2])). % 59.60/59.62 cnf(4571,plain, % 59.60/59.62 (~E(a28,f7(a11,a11))), % 59.60/59.62 inference(scs_inference,[],[551,2])). % 59.60/59.62 cnf(4587,plain, % 59.60/59.62 (~E(a28,f8(a11))), % 59.60/59.62 inference(scs_inference,[],[950,2])). % 59.60/59.62 cnf(4602,plain, % 59.60/59.62 (~E(f9(x46021),a11)), % 59.60/59.62 inference(scs_inference,[],[565,2])). % 59.60/59.62 cnf(4605,plain, % 59.60/59.62 (~E(a6,a11)), % 59.60/59.62 inference(scs_inference,[],[597,2])). % 59.60/59.62 cnf(5100,plain, % 59.60/59.62 (P2(a19)), % 59.60/59.62 inference(scs_inference,[],[107,161])). % 59.60/59.62 cnf(5104,plain, % 59.60/59.62 (P6(a19)), % 59.60/59.62 inference(scs_inference,[],[99,107,161,164,165])). % 59.60/59.62 cnf(5106,plain, % 59.60/59.62 (P5(f34(a19))), % 59.60/59.62 inference(scs_inference,[],[99,107,161,164,165,167])). % 59.60/59.62 cnf(5119,plain, % 59.60/59.62 (P11(f5(x51191,x51192),x51191,x51192)), % 59.60/59.62 inference(scs_inference,[],[99,1478,1502,137,679,133,107,150,161,164,165,167,168,169,170,171,173,430,296])). % 59.60/59.62 cnf(5121,plain, % 59.60/59.62 (P13(f4(x51211,x51212),x51211,x51212)), % 59.60/59.62 inference(scs_inference,[],[99,1478,1502,137,679,133,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297])). % 59.60/59.62 cnf(5131,plain, % 59.60/59.62 (P13(f45(a1),f42(a1),f43(a1))), % 59.60/59.62 inference(scs_inference,[],[99,1478,1502,137,679,133,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276])). % 59.60/59.62 cnf(5133,plain, % 59.60/59.62 (P10(f5(x51331,x51332),f35(f38(x51331,x51332)))), % 59.60/59.62 inference(scs_inference,[],[99,1478,1502,137,679,133,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301])). % 59.60/59.62 cnf(5138,plain, % 59.60/59.62 (E(f7(f39(x51381,x51382,f10(x51381,x51382)),x51383),f7(f37(f10(x51381,x51382)),x51383))), % 59.60/59.62 inference(rename_variables,[],[2040])). % 59.60/59.62 cnf(5143,plain, % 59.60/59.62 (E(f7(f39(x51431,x51432,f10(x51431,x51432)),x51433),f7(f37(f10(x51431,x51432)),x51433))), % 59.60/59.62 inference(rename_variables,[],[2040])). % 59.60/59.62 cnf(5156,plain, % 59.60/59.62 (E(f7(f39(x51561,x51562,f10(x51561,x51562)),x51563),f7(f37(f10(x51561,x51562)),x51563))), % 59.60/59.62 inference(rename_variables,[],[2040])). % 59.60/59.62 cnf(5167,plain, % 59.60/59.62 (E(f7(f39(x51671,x51672,f10(x51671,x51672)),x51673),f7(f37(f10(x51671,x51672)),x51673))), % 59.60/59.62 inference(rename_variables,[],[2040])). % 59.60/59.62 cnf(5169,plain, % 59.60/59.62 (E(f3(f35(a28)),a28)), % 59.60/59.62 inference(scs_inference,[],[99,1478,1502,2040,5138,5143,5156,4372,137,679,133,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160])). % 59.60/59.62 cnf(5175,plain, % 59.60/59.62 (P1(f36(a16))), % 59.60/59.62 inference(scs_inference,[],[99,102,152,1478,419,1502,2040,5138,5143,5156,4372,137,679,133,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174])). % 59.60/59.62 cnf(5177,plain, % 59.60/59.62 (P5(f29(a16))), % 59.60/59.62 inference(scs_inference,[],[99,102,152,1478,419,1502,2040,5138,5143,5156,4372,137,679,133,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175])). % 59.60/59.62 cnf(5181,plain, % 59.60/59.62 (P28(f36(a16))), % 59.60/59.62 inference(scs_inference,[],[99,102,152,1478,419,1502,2040,5138,5143,5156,4372,137,679,133,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180])). % 59.60/59.62 cnf(5183,plain, % 59.60/59.62 (P8(f29(a16))), % 59.60/59.62 inference(scs_inference,[],[99,102,152,1478,419,1502,2040,5138,5143,5156,4372,137,679,133,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183])). % 59.60/59.62 cnf(5201,plain, % 59.60/59.62 (P18(f29(a16))), % 59.60/59.62 inference(scs_inference,[],[99,102,152,1478,419,1502,2040,5138,5143,5156,4372,137,679,133,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204])). % 59.60/59.62 cnf(5207,plain, % 59.60/59.62 (~P29(f29(a16))), % 59.60/59.62 inference(scs_inference,[],[99,102,152,1478,419,1502,2040,5138,5143,5156,4372,137,679,133,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220])). % 59.60/59.62 cnf(5209,plain, % 59.60/59.62 (~P19(f43(a1))), % 59.60/59.62 inference(scs_inference,[],[99,102,152,1478,419,1502,2040,5138,5143,5156,4372,137,679,151,133,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222])). % 59.60/59.62 cnf(5211,plain, % 59.60/59.62 (~P19(f20(a1))), % 59.60/59.62 inference(scs_inference,[],[99,102,152,1478,419,1502,2040,5138,5143,5156,4372,137,679,151,133,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223])). % 59.60/59.62 cnf(5213,plain, % 59.60/59.62 (~P19(f21(a1))), % 59.60/59.62 inference(scs_inference,[],[99,102,152,1478,419,1502,2040,5138,5143,5156,4372,137,679,151,133,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224])). % 59.60/59.62 cnf(5215,plain, % 59.60/59.62 (~P29(f34(a19))), % 59.60/59.62 inference(scs_inference,[],[99,102,152,1478,419,1502,2040,5138,5143,5156,4372,137,679,151,133,156,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225])). % 59.60/59.62 cnf(5224,plain, % 59.60/59.62 (P10(f20(a1),f35(f42(a1)))), % 59.60/59.62 inference(scs_inference,[],[99,102,152,1478,419,1502,2040,5138,5143,5156,4372,154,137,679,135,151,133,156,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267])). % 59.60/59.62 cnf(5230,plain, % 59.60/59.62 (E(f30(f44(a19),f40(a19),f41(a19)),a19)), % 59.60/59.62 inference(scs_inference,[],[99,102,111,152,1478,419,1502,2040,5138,5143,5156,4372,154,137,679,135,151,133,156,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277])). % 59.60/59.62 cnf(5232,plain, % 59.60/59.62 (E(f31(f42(a13),f43(a13),f45(a13)),a13)), % 59.60/59.62 inference(scs_inference,[],[99,101,102,111,112,152,1478,419,1502,2040,5138,5143,5156,4372,154,137,679,135,151,133,156,107,146,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278])). % 59.60/59.62 cnf(5239,plain, % 59.60/59.62 (P11(f7(x52391,x52392),x52391,x52392)), % 59.60/59.62 inference(rename_variables,[],[147])). % 59.60/59.62 cnf(5242,plain, % 59.60/59.62 (P11(f4(x52421,x52422),x52421,x52422)), % 59.60/59.62 inference(rename_variables,[],[146])). % 59.60/59.62 cnf(5245,plain, % 59.60/59.62 (P11(f4(x52451,x52452),x52451,x52452)), % 59.60/59.62 inference(rename_variables,[],[146])). % 59.60/59.62 cnf(5247,plain, % 59.60/59.62 (E(f31(f43(a1),f42(a1),f39(f42(a1),f43(a1),f45(a1))),f36(a1))), % 59.60/59.62 inference(scs_inference,[],[99,4568,101,102,111,112,152,1478,419,1502,2040,5138,5143,5156,4372,154,137,679,723,135,151,133,156,107,146,5242,147,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278,279,280,314,315,316,308])). % 59.60/59.62 cnf(5252,plain, % 59.60/59.62 (P10(x52521,f35(x52521))), % 59.60/59.62 inference(rename_variables,[],[1477])). % 59.60/59.62 cnf(5254,plain, % 59.60/59.62 (P10(x52541,f35(x52541))), % 59.60/59.62 inference(rename_variables,[],[1477])). % 59.60/59.62 cnf(5258,plain, % 59.60/59.62 (P15(x52581,f35(x52581))), % 59.60/59.62 inference(scs_inference,[],[99,4568,101,102,111,112,152,1478,419,1502,1534,2040,5138,5143,5156,4372,154,137,679,723,1595,135,151,133,156,107,1477,5252,5254,146,5242,438,158,147,150,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278,279,280,314,315,316,308,273,68,274,71,258])). % 59.60/59.62 cnf(5261,plain, % 59.60/59.62 (P8(f34(a19))), % 59.60/59.62 inference(scs_inference,[],[99,4568,101,102,111,112,152,1478,419,1502,1534,2040,5138,5143,5156,4372,154,137,679,723,1595,135,151,133,156,107,1477,5252,5254,146,5242,438,158,147,150,115,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278,279,280,314,315,316,308,273,68,274,71,258,233])). % 59.60/59.62 cnf(5263,plain, % 59.60/59.62 (P30(f34(a19))), % 59.60/59.62 inference(scs_inference,[],[99,4568,101,102,111,112,152,1478,419,1502,1534,2040,5138,5143,5156,4372,154,137,679,723,1595,135,151,133,156,107,1477,5252,5254,146,5242,438,158,147,150,115,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278,279,280,314,315,316,308,273,68,274,71,258,233,234])). % 59.60/59.62 cnf(5265,plain, % 59.60/59.62 (P32(f34(a19))), % 59.60/59.62 inference(scs_inference,[],[99,4568,101,102,111,112,152,1478,419,1502,1534,2040,5138,5143,5156,4372,154,137,679,723,1595,135,151,133,156,107,1477,5252,5254,146,5242,438,158,147,150,115,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278,279,280,314,315,316,308,273,68,274,71,258,233,234,235])). % 59.60/59.62 cnf(5267,plain, % 59.60/59.62 (P33(f34(a19))), % 59.60/59.62 inference(scs_inference,[],[99,4568,101,102,111,112,152,1478,419,1502,1534,2040,5138,5143,5156,4372,154,137,679,723,1595,135,151,133,156,107,1477,5252,5254,146,5242,438,158,147,150,115,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278,279,280,314,315,316,308,273,68,274,71,258,233,234,235,236])). % 59.60/59.62 cnf(5269,plain, % 59.60/59.62 (P34(f34(a19))), % 59.60/59.62 inference(scs_inference,[],[99,4568,101,102,111,112,152,1478,419,1502,1534,2040,5138,5143,5156,4372,154,137,679,723,1595,135,151,133,156,107,1477,5252,5254,146,5242,438,158,147,150,115,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278,279,280,314,315,316,308,273,68,274,71,258,233,234,235,236,237])). % 59.60/59.62 cnf(5275,plain, % 59.60/59.62 (P22(f40(a19))), % 59.60/59.62 inference(scs_inference,[],[99,4568,101,102,111,112,117,152,1478,419,1502,1534,2040,5138,5143,5156,4372,154,137,679,723,1595,135,151,133,156,107,1477,5252,5254,146,5242,438,158,147,150,115,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278,279,280,314,315,316,308,273,68,274,71,258,233,234,235,236,237,238,239,240])). % 59.60/59.62 cnf(5277,plain, % 59.60/59.62 (P22(f41(a19))), % 59.60/59.62 inference(scs_inference,[],[99,4568,101,102,111,112,117,121,152,1478,419,1502,1534,2040,5138,5143,5156,4372,154,137,679,723,1595,135,151,133,156,107,1477,5252,5254,146,5242,438,158,147,150,115,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278,279,280,314,315,316,308,273,68,274,71,258,233,234,235,236,237,238,239,240,242])). % 59.60/59.62 cnf(5303,plain, % 59.60/59.62 (P13(f32(a19,a19),f44(a19),f44(a19))), % 59.60/59.62 inference(scs_inference,[],[99,4568,101,102,111,112,117,119,121,123,152,1478,419,1502,1534,2040,5138,5143,5156,4372,154,137,679,723,1595,135,151,133,388,156,107,1477,5252,5254,146,5242,438,158,147,150,115,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278,279,280,314,315,316,308,273,68,274,71,258,233,234,235,236,237,238,239,240,242,262,263,264,265,288,290,256,282,270,298,299,302,303])). % 59.60/59.62 cnf(5346,plain, % 59.60/59.62 (~P15(f35(f35(f38(x53461,x53462))),f35(f38(x53461,x53462)))), % 59.60/59.62 inference(scs_inference,[],[99,4568,101,102,111,112,117,119,121,123,152,1478,419,1502,1534,2040,5138,5143,5156,4372,154,137,679,723,1595,135,151,133,388,156,107,1477,5252,5254,146,5242,438,158,147,150,115,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278,279,280,314,315,316,308,273,68,274,71,258,233,234,235,236,237,238,239,240,242,262,263,264,265,288,290,256,282,270,298,299,302,303,1476,4,5,8,13,14,28,29,30,31,32,33,34,35,38,39,42,43,44,4007,4288,6,7,9,10,11,12,15,16,26,27,36,37,40,41,4235,522,257,498,261])). % 59.60/59.62 cnf(5351,plain, % 59.60/59.62 (P13(f5(x53511,x53512),x53511,x53512)), % 59.60/59.62 inference(rename_variables,[],[150])). % 59.60/59.62 cnf(5357,plain, % 59.60/59.62 (P23(f7(x53571,x53572),x53571,x53572)), % 59.60/59.62 inference(rename_variables,[],[149])). % 59.60/59.62 cnf(5359,plain, % 59.60/59.62 (P23(f7(x53591,x53592),x53591,x53592)), % 59.60/59.62 inference(rename_variables,[],[149])). % 59.60/59.62 cnf(5360,plain, % 59.60/59.62 (P11(f7(f37(f10(x53601,x53602)),x53603),f39(x53601,x53602,f10(x53601,x53602)),x53603)), % 59.60/59.62 inference(scs_inference,[],[99,4568,101,102,111,112,117,119,121,123,152,1478,419,1502,1534,2040,5138,5143,5156,5167,4372,154,137,679,723,1595,135,151,133,388,363,156,107,1477,5252,5254,146,5242,5245,438,158,147,5239,150,115,149,5357,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278,279,280,314,315,316,308,273,68,274,71,258,233,234,235,236,237,238,239,240,242,262,263,264,265,288,290,256,282,270,298,299,302,303,1476,4,5,8,13,14,28,29,30,31,32,33,34,35,38,39,42,43,44,4007,4288,6,7,9,10,11,12,15,16,26,27,36,37,40,41,4235,522,257,498,261,52,58,89,91,50,48,47,49])). % 59.60/59.62 cnf(5361,plain, % 59.60/59.62 (E(f7(f39(x53611,x53612,f10(x53611,x53612)),x53613),f7(f37(f10(x53611,x53612)),x53613))), % 59.60/59.62 inference(rename_variables,[],[2040])). % 59.60/59.62 cnf(5367,plain, % 59.60/59.62 (P23(f7(f37(f10(x53671,x53672)),x53673),f39(x53671,x53672,f10(x53671,x53672)),x53673)), % 59.60/59.62 inference(scs_inference,[],[99,4568,101,102,111,112,117,119,121,123,152,1478,419,1502,1534,2040,5138,5143,5156,5167,5361,2104,4372,154,137,679,723,1595,135,151,133,388,363,156,107,1477,5252,5254,146,5242,5245,438,158,147,5239,150,5351,115,149,5357,5359,161,164,165,167,168,169,170,171,173,430,296,297,172,246,305,306,276,301,312,393,394,300,542,17,19,20,21,22,23,24,25,313,687,689,283,284,285,286,486,488,511,160,2,1075,18,65,174,175,179,180,183,186,189,192,195,198,201,202,203,204,206,216,220,222,223,224,225,226,227,271,3,267,268,269,277,278,279,280,314,315,316,308,273,68,274,71,258,233,234,235,236,237,238,239,240,242,262,263,264,265,288,290,256,282,270,298,299,302,303,1476,4,5,8,13,14,28,29,30,31,32,33,34,35,38,39,42,43,44,4007,4288,6,7,9,10,11,12,15,16,26,27,36,37,40,41,4235,522,257,498,261,52,58,89,91,50,48,47,49,88,90,46])). % 59.60/59.62 cnf(5407,plain, % 59.60/59.62 (P2(f34(a19))), % 59.60/59.62 inference(scs_inference,[],[5106,161])). % 59.60/59.62 cnf(5437,plain, % 59.60/59.62 (P5(f34(f34(a19)))), % 59.60/59.62 inference(scs_inference,[],[100,5100,5104,5119,5106,5209,5275,5169,147,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167])). % 59.60/59.62 cnf(5439,plain, % 59.60/59.62 (P10(f4(x54391,x54392),f35(f38(x54391,x54392)))), % 59.60/59.62 inference(scs_inference,[],[100,5100,5104,5119,5121,5106,5209,5275,5169,147,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301])). % 59.60/59.62 cnf(5456,plain, % 59.60/59.62 (E(f3(f35(a6)),a28)), % 59.60/59.62 inference(scs_inference,[],[100,5100,5104,5119,5121,5106,5209,5275,5169,5230,4377,147,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160])). % 59.60/59.62 cnf(5458,plain, % 59.60/59.62 (P11(f45(a1),f42(a1),f43(a1))), % 59.60/59.62 inference(scs_inference,[],[100,5100,5104,5119,5121,5131,5106,5209,5275,5169,5230,4377,147,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296])). % 59.60/59.62 cnf(5461,plain, % 59.60/59.62 (E(f35(f3(f35(a28))),f35(a28))), % 59.60/59.62 inference(scs_inference,[],[100,5100,5104,5119,5121,5131,5106,5209,5275,5169,5230,4377,147,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8])). % 59.60/59.62 cnf(5474,plain, % 59.60/59.62 (P13(f45(a12),f42(a12),f43(a12))), % 59.60/59.62 inference(scs_inference,[],[100,5100,5104,5119,5121,5131,5106,5209,5275,5169,5230,4377,147,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276])). % 59.60/59.62 cnf(5476,plain, % 59.60/59.62 (P6(f34(a19))), % 59.60/59.62 inference(scs_inference,[],[100,5100,5104,5119,5121,5131,5106,5209,5275,5169,5230,4377,147,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165])). % 59.60/59.62 cnf(5490,plain, % 59.60/59.62 (E(f7(f3(f35(a28)),x54901),f7(a28,x54901))), % 59.60/59.62 inference(scs_inference,[],[100,5100,5104,5119,5121,5131,5106,5209,5275,5169,5230,5360,4377,147,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9])). % 59.60/59.62 cnf(5508,plain, % 59.60/59.62 (P15(a28,f35(a6))), % 59.60/59.62 inference(scs_inference,[],[100,5100,5104,5119,5121,5131,5106,5209,5275,5169,5230,5360,5346,4377,147,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075])). % 59.60/59.62 cnf(5510,plain, % 59.60/59.62 (~P15(f35(x55101),x55101)), % 59.60/59.62 inference(scs_inference,[],[100,5100,5104,5258,5119,5121,5131,5106,5209,5275,5169,5230,5360,5346,4377,147,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261])). % 59.60/59.63 cnf(5512,plain, % 59.60/59.63 (~P25(f36(a1))), % 59.60/59.63 inference(scs_inference,[],[99,100,5100,5104,5258,5119,5121,5131,5106,5209,5275,5169,5230,5360,5346,4377,151,147,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216])). % 59.60/59.63 cnf(5516,plain, % 59.60/59.63 (P8(f29(a1))), % 59.60/59.63 inference(scs_inference,[],[99,100,5100,5104,5258,5119,5121,5131,5106,5177,5207,5209,5275,5169,5230,5360,5346,4377,151,147,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183])). % 59.60/59.63 cnf(5518,plain, % 59.60/59.63 (P7(f29(a1))), % 59.60/59.63 inference(scs_inference,[],[99,100,5100,5104,5258,5119,5121,5131,5106,5177,5207,5209,5275,5169,5230,5360,5346,4377,151,147,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179])). % 59.60/59.63 cnf(5524,plain, % 59.60/59.63 (E(f30(f44(a2),f40(a2),f41(a2)),a2)), % 59.60/59.63 inference(scs_inference,[],[99,100,108,5100,5104,5258,5119,5121,5131,5106,5177,5207,5209,5275,5169,5230,5360,5346,4377,104,151,147,102,152,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277])). % 59.60/59.63 cnf(5533,plain, % 59.60/59.63 (P32(f29(a1))), % 59.60/59.63 inference(scs_inference,[],[99,100,108,5100,5104,5258,5119,5121,5131,5106,5177,5207,5209,5275,5169,5230,5360,5346,4377,743,578,153,104,151,147,102,152,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189])). % 59.60/59.63 cnf(5538,plain, % 59.60/59.63 (P11(f5(x55381,x55382),x55381,x55382)), % 59.60/59.63 inference(rename_variables,[],[5119])). % 59.60/59.63 cnf(5540,plain, % 59.60/59.63 (P30(f29(a1))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5121,5131,5106,5177,5207,5209,5275,5169,5230,5360,5346,4377,743,578,153,104,151,147,102,152,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186])). % 59.60/59.63 cnf(5544,plain, % 59.60/59.63 (P34(f29(a1))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5121,5131,5106,5177,5207,5209,5275,5169,5230,5360,5346,4377,743,578,153,104,151,147,102,152,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186,206,195])). % 59.60/59.63 cnf(5546,plain, % 59.60/59.63 (P1(f36(a1))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5121,5131,5106,5177,5207,5209,5275,5169,5230,5360,5346,4377,743,578,153,104,151,147,102,152,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186,206,195,174])). % 59.60/59.63 cnf(5552,plain, % 59.60/59.63 (P12(f33(a1),f34(f29(a1)),f29(f36(a1)))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5121,5131,5106,5177,5207,5209,5275,5169,5230,5360,5346,4377,743,578,153,104,151,147,102,152,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186,206,195,174,198,201,279])). % 59.60/59.63 cnf(5563,plain, % 59.60/59.63 (P28(f36(a1))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5538,5121,5131,5106,5175,5177,5181,5207,5209,5275,5169,5230,5247,5360,5346,4377,4483,743,578,153,104,151,147,102,152,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186,206,195,174,198,201,279,3,278,204,315,180])). % 59.60/59.63 cnf(5565,plain, % 59.60/59.63 (P27(f33(a1),f34(f29(a1)),f29(f36(a1)))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5538,5121,5131,5106,5175,5177,5181,5207,5209,5275,5169,5230,5247,5360,5346,4377,4483,743,578,153,104,151,147,102,152,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186,206,195,174,198,201,279,3,278,204,315,180,280])). % 59.60/59.63 cnf(5569,plain, % 59.60/59.63 (P33(f29(a1))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5538,5121,5131,5106,5175,5177,5181,5207,5209,5275,5169,5230,5247,5360,5346,4377,4483,743,578,153,104,151,147,102,152,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186,206,195,174,198,201,279,3,278,204,315,180,280,203,192])). % 59.60/59.63 cnf(5571,plain, % 59.60/59.63 (~P29(f29(a1))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5538,5121,5131,5106,5175,5177,5181,5207,5209,5275,5169,5230,5247,5360,5346,4377,4483,743,578,153,104,151,147,102,152,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186,206,195,174,198,201,279,3,278,204,315,180,280,203,192,220])). % 59.60/59.63 cnf(5573,plain, % 59.60/59.63 (P5(f29(a1))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5538,5121,5131,5106,5175,5177,5181,5207,5209,5275,5169,5230,5247,5360,5346,4377,4483,743,578,153,104,151,147,102,152,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186,206,195,174,198,201,279,3,278,204,315,180,280,203,192,220,175])). % 59.60/59.63 cnf(5577,plain, % 59.60/59.63 (~E(f3(f35(a6)),f43(a1))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5538,5121,5131,5106,5175,5177,5181,5207,5209,5275,5169,5230,5247,5360,5346,4377,4483,743,578,153,104,151,147,102,152,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186,206,195,174,198,201,279,3,278,204,315,180,280,203,192,220,175,226,65])). % 59.60/59.63 cnf(5580,plain, % 59.60/59.63 (~P10(f35(x55801),f35(f3(f35(a6))))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5538,5121,5131,5106,5175,5177,5181,5207,5209,5275,5169,5230,5247,5360,5346,4377,4483,743,578,153,104,151,147,102,152,140,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186,206,195,174,198,201,279,3,278,204,315,180,280,203,192,220,175,226,65,68,273])). % 59.60/59.63 cnf(5586,plain, % 59.60/59.63 (P15(f5(x55861,x55862),f35(f38(x55861,x55862)))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5538,5121,5131,5106,5175,5177,5181,5207,5209,5275,5133,5169,5230,5247,5360,5346,4377,4483,743,578,153,104,1477,151,158,147,102,152,140,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186,206,195,174,198,201,279,3,278,204,315,180,280,203,192,220,175,226,65,68,273,274,71,258])). % 59.60/59.63 cnf(5615,plain, % 59.60/59.63 (P31(f34(f29(a1)))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5538,5121,5131,5106,5175,5177,5181,5183,5207,5209,5215,5263,5265,5267,5269,5275,5133,5169,5230,5247,5360,5346,4377,4483,743,578,153,104,1477,151,158,147,102,152,140,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186,206,195,174,198,201,279,3,278,204,315,180,280,203,192,220,175,226,65,68,273,274,71,258,241,243,233,264,234,238,235,237,239,262,265,236,263,256])). % 59.60/59.63 cnf(5624,plain, % 59.60/59.63 (P14(f34(a19),f34(a19))), % 59.60/59.63 inference(scs_inference,[],[99,4605,100,108,5100,5104,5258,5119,5538,5121,5131,5106,5175,5177,5181,5183,5207,5209,5215,5261,5263,5265,5267,5269,5275,5133,5169,5230,5247,5360,5367,5346,4377,4483,743,578,153,104,1477,142,151,158,147,102,152,140,161,246,313,164,312,1476,172,305,171,169,170,31,168,39,300,283,167,301,33,486,284,173,32,5,4,6,24,687,42,17,23,160,296,26,8,38,285,37,16,14,394,22,11,25,306,276,165,19,35,286,36,511,297,10,44,43,430,9,12,41,2,34,542,7,21,1845,29,27,28,40,13,15,30,20,498,1075,18,261,216,225,183,179,308,271,277,269,202,314,189,227,316,186,206,195,174,198,201,279,3,278,204,315,180,280,203,192,220,175,226,65,68,273,274,71,258,241,243,233,264,234,238,235,237,239,262,265,236,263,256,310,282,270])). % 59.60/59.63 cnf(5649,plain, % 59.60/59.63 (P2(f29(a1))), % 59.60/59.63 inference(scs_inference,[],[5573,161])). % 59.60/59.63 cnf(5654,plain, % 59.60/59.63 (E(f7(f3(f35(a28)),x56541),f7(a28,x56541))), % 59.60/59.63 inference(rename_variables,[],[5490])). % 59.60/59.63 cnf(5662,plain, % 59.60/59.63 (E(f7(f3(f35(a28)),x56621),f7(a28,x56621))), % 59.60/59.63 inference(rename_variables,[],[5490])). % 59.60/59.63 cnf(5666,plain, % 59.60/59.63 (E(f7(f3(f35(a28)),x56661),f7(a28,x56661))), % 59.60/59.63 inference(rename_variables,[],[5490])). % 59.60/59.63 cnf(5678,plain, % 59.60/59.63 (P11(f32(a19,a19),f44(a19),f44(a19))), % 59.60/59.63 inference(scs_inference,[],[5303,5211,5277,5458,5546,5573,5232,5490,5654,5662,5666,5580,4382,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296])). % 59.60/59.63 cnf(5687,plain, % 59.60/59.63 (P13(f7(x56871,x56872),x56871,x56872)), % 59.60/59.63 inference(scs_inference,[],[5303,5211,5277,5458,5476,5546,5573,5232,5490,5654,5662,5666,5580,4382,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297])). % 59.60/59.63 cnf(5696,plain, % 59.60/59.63 (P6(f29(a1))), % 59.60/59.63 inference(scs_inference,[],[5303,5211,5277,5407,5458,5476,5546,5573,5232,5490,5654,5662,5666,5580,4382,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165])). % 59.60/59.63 cnf(5698,plain, % 59.60/59.63 (E(f3(f31(f42(a13),f43(a13),f45(a13))),f3(a13))), % 59.60/59.63 inference(scs_inference,[],[5303,5211,5277,5407,5458,5476,5546,5573,5232,5490,5654,5662,5666,5580,4382,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5])). % 59.60/59.63 cnf(5712,plain, % 59.60/59.63 (E(f30(f31(f42(a13),f43(a13),f45(a13)),x57121,x57122),f30(a13,x57121,x57122))), % 59.60/59.63 inference(scs_inference,[],[5303,5211,5277,5407,5458,5476,5546,5573,5437,5232,5490,5654,5662,5666,5580,4382,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23])). % 59.60/59.63 cnf(5719,plain, % 59.60/59.63 (E(f7(f31(f42(a13),f43(a13),f45(a13)),x57191),f7(a13,x57191))), % 59.60/59.63 inference(scs_inference,[],[5303,5211,5277,5407,5458,5476,5546,5573,5437,5232,5490,5654,5662,5666,5580,4382,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9])). % 59.60/59.63 cnf(5725,plain, % 59.60/59.63 (E(f30(x57251,x57252,f31(f42(a13),f43(a13),f45(a13))),f30(x57251,x57252,a13))), % 59.60/59.63 inference(scs_inference,[],[5303,5211,5277,5407,5458,5476,5546,5573,5437,5232,5490,5654,5662,5666,5580,4382,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25])). % 59.60/59.63 cnf(5730,plain, % 59.60/59.63 (E(a13,f31(f42(a13),f43(a13),f45(a13)))), % 59.60/59.63 inference(scs_inference,[],[5303,5211,5277,5407,5458,5476,5546,5573,5437,5232,5490,5654,5662,5666,5580,4382,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2])). % 59.60/59.63 cnf(5761,plain, % 59.60/59.63 (~P25(f36(f36(a1)))), % 59.60/59.63 inference(scs_inference,[],[5303,5211,5277,5407,5458,5476,5512,5546,5573,5586,5437,5232,5490,5654,5662,5666,5580,4382,112,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216])). % 59.60/59.63 cnf(5763,plain, % 59.60/59.63 (P8(f29(f36(a1)))), % 59.60/59.63 inference(scs_inference,[],[5303,5211,5277,5407,5458,5476,5512,5546,5573,5586,5437,5232,5490,5654,5662,5666,5580,4382,112,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216,183])). % 59.60/59.63 cnf(5768,plain, % 59.60/59.63 (P11(f7(x57681,x57682),x57681,x57682)), % 59.60/59.63 inference(rename_variables,[],[147])). % 59.60/59.63 cnf(5772,plain, % 59.60/59.63 (P32(f29(f36(a1)))), % 59.60/59.63 inference(scs_inference,[],[5303,5211,5277,5407,5458,5476,5512,5546,5573,5586,5437,5232,5490,5654,5662,5666,5580,4382,112,628,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216,183,224,314,271,189])). % 59.60/59.63 cnf(5776,plain, % 59.60/59.63 (P31(f29(f36(a1)))), % 59.60/59.63 inference(scs_inference,[],[5303,5211,5277,5407,5458,5476,5512,5546,5573,5586,5437,5232,5490,5654,5662,5666,5580,4382,112,628,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216,183,224,314,271,189,222,206])). % 59.60/59.63 cnf(5780,plain, % 59.60/59.63 (~P29(f34(f29(a1)))), % 59.60/59.63 inference(scs_inference,[],[5303,5211,5277,5407,5458,5476,5512,5546,5571,5573,5586,5437,5232,5490,5654,5662,5666,5580,4382,112,628,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216,183,224,314,271,189,222,206,267,225])). % 59.60/59.63 cnf(5783,plain, % 59.60/59.63 (P11(f5(x57831,x57832),x57831,x57832)), % 59.60/59.63 inference(rename_variables,[],[5119])). % 59.60/59.63 cnf(5793,plain, % 59.60/59.63 (~P29(f29(f36(a1)))), % 59.60/59.63 inference(scs_inference,[],[4571,5303,5211,5277,5407,5458,5476,5512,5546,5571,5573,5586,5437,5232,5490,5654,5662,5666,5580,4382,112,628,5119,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216,183,224,314,271,189,222,206,267,225,315,186,268,203,195,220])). % 59.60/59.63 cnf(5808,plain, % 59.60/59.63 (P33(f29(f36(a1)))), % 59.60/59.63 inference(scs_inference,[],[4571,5303,5211,5277,5407,5458,5476,5512,5518,5546,5571,5573,5586,5437,5232,5490,5654,5662,5666,5580,4382,112,628,5119,5783,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216,183,224,314,271,189,222,206,267,225,315,186,268,203,195,220,202,198,180,277,316,201,192])). % 59.60/59.63 cnf(5811,plain, % 59.60/59.63 (P1(f36(f36(a1)))), % 59.60/59.63 inference(scs_inference,[],[4571,5303,5211,5277,5407,5458,5476,5512,5518,5546,5571,5573,5577,5586,5437,5232,5456,5490,5654,5662,5666,5580,4382,112,628,5119,5783,147,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216,183,224,314,271,189,222,206,267,225,315,186,268,203,195,220,202,198,180,277,316,201,192,3,174])). % 59.60/59.63 cnf(5815,plain, % 59.60/59.63 (P5(f29(f36(a1)))), % 59.60/59.63 inference(scs_inference,[],[113,4571,5303,5211,5277,5407,5458,5476,5512,5518,5546,5571,5573,5577,5586,5437,5232,5456,5490,5654,5662,5666,5580,4382,112,628,5119,5783,147,102,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216,183,224,314,271,189,222,206,267,225,315,186,268,203,195,220,202,198,180,277,316,201,192,3,174,278,175])). % 59.60/59.63 cnf(5827,plain, % 59.60/59.63 (P15(f3(f20(a1)),f20(a1))), % 59.60/59.63 inference(scs_inference,[],[113,4571,5510,5303,5211,5277,5407,5458,5476,5512,5518,5546,5571,5573,5577,5586,5437,5232,5456,5490,5654,5662,5666,5580,4382,112,628,1604,5258,5119,5783,1477,147,102,140,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216,183,224,314,271,189,222,206,267,225,315,186,268,203,195,220,202,198,180,277,316,201,192,3,174,278,175,204,65,70,274,68,258])). % 59.60/59.63 cnf(5852,plain, % 59.60/59.63 (P8(f34(f29(a1)))), % 59.60/59.63 inference(scs_inference,[],[113,4571,5510,5303,5211,5277,5407,5458,5476,5512,5516,5518,5533,5540,5544,5546,5569,5571,5573,5577,5586,5437,5232,5456,5490,5654,5662,5666,5461,5580,4382,112,628,1604,5258,5119,5783,1477,438,147,102,140,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216,183,224,314,271,189,222,206,267,225,315,186,268,203,195,220,202,198,180,277,316,201,192,3,174,278,175,204,65,70,274,68,258,71,264,238,242,234,262,239,240,237,265,235,233])). % 59.60/59.63 cnf(5862,plain, % 59.60/59.63 (P20(f7(x58621,x58622))), % 59.60/59.63 inference(rename_variables,[],[142])). % 59.60/59.63 cnf(5866,plain, % 59.60/59.63 (P11(f7(x58661,x58662),x58661,x58662)), % 59.60/59.63 inference(rename_variables,[],[147])). % 59.60/59.63 cnf(5867,plain, % 59.60/59.63 (P20(f7(x58671,x58672))), % 59.60/59.63 inference(rename_variables,[],[142])). % 59.60/59.63 cnf(5868,plain, % 59.60/59.63 (P23(f7(x58681,x58682),x58681,x58682)), % 59.60/59.63 inference(rename_variables,[],[149])). % 59.60/59.63 cnf(5870,plain, % 59.60/59.63 (P5(f30(x58701,f7(f38(x58701,x58701),x58701),f7(f38(x58701,x58701),x58701)))), % 59.60/59.63 inference(scs_inference,[],[113,4571,5510,5303,5211,5277,5407,5458,5476,5512,5516,5518,5533,5540,5544,5546,5569,5571,5573,5577,5586,5437,5615,5232,5456,5490,5654,5662,5666,5461,5580,4382,112,5367,628,1604,5360,5258,5119,5783,1477,142,5862,5867,438,147,5768,5866,102,140,149,5868,967,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216,183,224,314,271,189,222,206,267,225,315,186,268,203,195,220,202,198,180,277,316,201,192,3,174,278,175,204,65,70,274,68,258,71,264,238,242,234,262,239,240,237,265,235,233,236,263,256,310,304,317])). % 59.60/59.63 cnf(5871,plain, % 59.60/59.63 (P20(f7(x58711,x58712))), % 59.60/59.63 inference(rename_variables,[],[142])). % 59.60/59.63 cnf(5872,plain, % 59.60/59.63 (P23(f7(x58721,x58722),x58721,x58722)), % 59.60/59.63 inference(rename_variables,[],[149])). % 59.60/59.63 cnf(5873,plain, % 59.60/59.63 (P11(f7(x58731,x58732),x58731,x58732)), % 59.60/59.63 inference(rename_variables,[],[147])). % 59.60/59.63 cnf(5876,plain, % 59.60/59.63 (P20(f7(x58761,x58762))), % 59.60/59.63 inference(rename_variables,[],[142])). % 59.60/59.63 cnf(5877,plain, % 59.60/59.63 (P23(f7(x58771,x58772),x58771,x58772)), % 59.60/59.63 inference(rename_variables,[],[149])). % 59.60/59.63 cnf(5878,plain, % 59.60/59.63 (P11(f7(x58781,x58782),x58781,x58782)), % 59.60/59.63 inference(rename_variables,[],[147])). % 59.60/59.63 cnf(5901,plain, % 59.60/59.63 (P14(f34(f29(a1)),f29(f36(a1)))), % 59.60/59.63 inference(scs_inference,[],[113,4571,5510,5624,5303,5211,5277,5407,5458,5476,5512,5516,5518,5533,5540,5544,5546,5569,5571,5573,5577,5586,5437,5615,5232,5456,5552,5565,5490,5654,5662,5666,5461,5580,4382,112,5367,5261,628,1604,5360,5258,5119,5783,5106,1477,142,5862,5867,5871,5876,5215,438,147,5768,5866,5873,5878,102,140,149,5868,5872,5877,967,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216,183,224,314,271,189,222,206,267,225,315,186,268,203,195,220,202,198,180,277,316,201,192,3,174,278,175,204,65,70,274,68,258,71,264,238,242,234,262,239,240,237,265,235,233,236,263,256,310,304,317,318,282,270,299,303,298,322,287,302,307])). % 59.60/59.63 cnf(5907,plain, % 59.60/59.63 (~P10(f35(a6),f35(f3(f35(a28))))), % 59.60/59.63 inference(scs_inference,[],[113,4571,5510,5624,5303,5201,5211,5277,5407,5458,5476,5512,5516,5518,5533,5540,5544,5546,5569,5571,5573,5508,5577,5586,5437,5615,5232,5456,5552,5565,5490,5654,5662,5666,5461,5580,4382,112,5367,5261,628,1604,5360,5258,5119,5783,4372,5106,1477,142,5862,5867,5871,5876,5215,438,147,5768,5866,5873,5878,102,140,149,5868,5872,5877,967,161,246,522,1476,312,172,689,164,393,488,168,1481,305,160,300,296,169,313,171,39,297,301,173,170,33,165,5,276,486,16,17,42,11,26,167,36,35,687,23,14,4,306,511,34,9,394,8,29,44,38,25,13,32,21,43,2,31,430,40,22,24,498,20,28,6,10,19,37,7,12,41,542,15,30,27,1075,18,261,64,221,223,179,216,183,224,314,271,189,222,206,267,225,315,186,268,203,195,220,202,198,180,277,316,201,192,3,174,278,175,204,65,70,274,68,258,71,264,238,242,234,262,239,240,237,265,235,233,236,263,256,310,304,317,318,282,270,299,303,298,322,287,302,307,257,4007,78,273])). % 59.60/59.63 cnf(5945,plain, % 59.60/59.63 (E(f7(f31(f42(a13),f43(a13),f45(a13)),x59451),f7(a13,x59451))), % 59.60/59.63 inference(rename_variables,[],[5719])). % 59.60/59.63 cnf(5949,plain, % 59.60/59.63 (E(f7(f31(f42(a13),f43(a13),f45(a13)),x59491),f7(a13,x59491))), % 59.60/59.63 inference(rename_variables,[],[5719])). % 59.60/59.63 cnf(5954,plain, % 59.60/59.63 (E(f7(f31(f42(a13),f43(a13),f45(a13)),x59541),f7(a13,x59541))), % 59.60/59.63 inference(rename_variables,[],[5719])). % 59.60/59.63 cnf(6030,plain, % 59.60/59.63 (P11(f7(x60301,x60302),x60301,x60302)), % 59.60/59.63 inference(rename_variables,[],[147])). % 59.60/59.63 cnf(6126,plain, % 59.60/59.63 ($false), % 59.60/59.63 inference(scs_inference,[],[109,116,124,128,4587,5687,5678,4602,5213,5474,5563,5649,5696,144,5827,1819,5439,5224,5761,5763,5772,5776,5780,5793,5808,5811,5815,5852,5730,5524,5901,5712,5725,5719,5945,5949,5954,5698,5907,5870,122,126,129,101,108,120,5510,650,159,4382,5360,390,5119,132,578,104,153,130,142,158,114,147,6030,5546,140,149,148,105,967,161,246,160,305,164,172,300,312,1476,171,170,297,168,313,276,689,301,488,296,4007,393,39,169,522,173,42,167,486,16,33,11,23,26,17,1481,165,511,14,25,306,44,4,498,32,36,19,13,430,5,6,8,394,35,24,34,41,43,12,10,687,2,38,31,7,9,29,28,21,22,40,20,30,27,542,37,15,18,261,60,62,69,76,79,83,86,87,179,314,78,183,189,206,315,202,277,52,225,216,271,186,203,192,316,174,53,195,175,204,198,220,201,180,278,3,65,77,274,70,258,68,71,242,234,241,237,235,238,239,233,236,256,304,282,270,275]), % 59.60/59.63 ['proof']). % 59.60/59.63 % SZS output end Proof % 59.60/59.63 % Total time :58.930000s %------------------------------------------------------------------------------