%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT356+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 : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 10:19:06 EDT 2024 % Result : Theorem 129.18s 129.23s % Output : CNFRefutation 129.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : LAT356+1 : TPTP v8.2.0. Released v3.4.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.14/0.34 % Computer : n024.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Sat Jun 22 00:17:24 EDT 2024 % 0.14/0.34 % CPUTime : % 0.46/0.60 start to proof:theBenchmark % 129.14/129.18 %------------------------------------------- % 129.14/129.18 % File :CSE---1.7 % 129.14/129.18 % Problem :theBenchmark % 129.14/129.18 % Transform :cnf % 129.14/129.18 % Format :tptp:raw % 129.14/129.18 % Command :java -jar mcs_scs.jar %d %s % 129.14/129.18 % 129.14/129.18 % Result :Theorem 128.360000s % 129.14/129.18 % Output :CNFRefutation 128.360000s % 129.14/129.18 %------------------------------------------- % 129.18/129.20 %------------------------------------------------------------------------------ % 129.18/129.20 % File : LAT356+1 : TPTP v8.2.0. Released v3.4.0. % 129.18/129.20 % Domain : Lattice Theory % 129.18/129.20 % Problem : Duality Based on Galois Connection - Part I T07 % 129.18/129.20 % Version : [Urb08] axioms : Especial. % 129.18/129.20 % English : % 129.18/129.20 % 129.18/129.20 % Refs : [Ban01] Bancerek (2001), Duality Based on the Galois Connectio % 129.18/129.20 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 129.18/129.20 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 129.18/129.20 % Source : [Urb08] % 129.18/129.20 % Names : t7_waybel34 [Urb08] % 129.18/129.20 % 129.18/129.20 % Status : Theorem % 129.18/129.20 % Rating : 0.33 v8.2.0, 0.31 v8.1.0, 0.25 v7.5.0, 0.31 v7.4.0, 0.27 v7.3.0, 0.31 v7.2.0, 0.28 v7.1.0, 0.35 v7.0.0, 0.33 v6.4.0, 0.38 v6.3.0, 0.29 v6.2.0, 0.28 v6.1.0, 0.40 v6.0.0, 0.35 v5.5.0, 0.44 v5.4.0, 0.43 v5.3.0, 0.52 v5.2.0, 0.35 v5.1.0, 0.38 v5.0.0, 0.42 v4.1.0, 0.48 v4.0.0, 0.50 v3.5.0, 0.53 v3.4.0 % 129.18/129.20 % Syntax : Number of formulae : 130 ( 19 unt; 0 def) % 129.18/129.20 % Number of atoms : 865 ( 9 equ) % 129.18/129.20 % Maximal formula atoms : 28 ( 6 avg) % 129.18/129.20 % Number of connectives : 828 ( 93 ~; 1 |; 582 &) % 129.18/129.20 % ( 4 <=>; 148 =>; 0 <=; 0 <~>) % 129.18/129.20 % Maximal formula depth : 22 ( 7 avg) % 129.18/129.20 % Maximal term depth : 3 ( 1 avg) % 129.18/129.20 % Number of predicates : 55 ( 53 usr; 1 prp; 0-3 aty) % 129.18/129.20 % Number of functors : 11 ( 11 usr; 1 con; 0-4 aty) % 129.18/129.20 % Number of variables : 218 ( 192 !; 26 ?) % 129.18/129.20 % SPC : FOF_THM_RFO_SEQ % 129.18/129.20 % 129.18/129.20 % Comments : Normal version: includes the axioms (which may be theorems from % 129.18/129.20 % other articles) and background that are possibly necessary. % 129.18/129.20 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 129.18/129.20 % : The problem encoding is based on set theory. % 129.18/129.20 %------------------------------------------------------------------------------ % 129.18/129.20 fof(t7_waybel34,conjecture, % 129.18/129.20 ! [A] : % 129.18/129.20 ( ( v2_orders_2(A) % 129.18/129.20 & v3_orders_2(A) % 129.18/129.20 & v4_orders_2(A) % 129.18/129.20 & v1_lattice3(A) % 129.18/129.20 & v2_lattice3(A) % 129.18/129.20 & v3_lattice3(A) % 129.18/129.20 & l1_orders_2(A) ) % 129.18/129.20 => ( k1_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A) % 129.18/129.20 & k2_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(antisymmetry_r2_hidden,axiom, % 129.18/129.20 ! [A,B] : % 129.18/129.20 ( r2_hidden(A,B) % 129.18/129.20 => ~ r2_hidden(B,A) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc10_membered,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( v1_membered(A) % 129.18/129.20 => ! [B] : % 129.18/129.20 ( m1_subset_1(B,A) % 129.18/129.20 => v1_xcmplx_0(B) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc10_waybel_0,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( l1_orders_2(A) % 129.18/129.20 => ( ( ~ v3_struct_0(A) % 129.18/129.20 & v2_orders_2(A) % 129.18/129.20 & v3_lattice3(A) ) % 129.18/129.20 => ( ~ v3_struct_0(A) % 129.18/129.20 & v2_orders_2(A) % 129.18/129.20 & v24_waybel_0(A) % 129.18/129.20 & v25_waybel_0(A) ) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc11_membered,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( v2_membered(A) % 129.18/129.20 => ! [B] : % 129.18/129.20 ( m1_subset_1(B,A) % 129.18/129.20 => ( v1_xcmplx_0(B) % 129.18/129.20 & v1_xreal_0(B) ) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc11_waybel_0,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( l1_orders_2(A) % 129.18/129.20 => ( ( ~ v3_struct_0(A) % 129.18/129.20 & v2_orders_2(A) % 129.18/129.20 & v25_waybel_0(A) ) % 129.18/129.20 => ( ~ v3_struct_0(A) % 129.18/129.20 & v2_orders_2(A) % 129.18/129.20 & v1_yellow_0(A) ) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc12_membered,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( v3_membered(A) % 129.18/129.20 => ! [B] : % 129.18/129.20 ( m1_subset_1(B,A) % 129.18/129.20 => ( v1_xcmplx_0(B) % 129.18/129.20 & v1_xreal_0(B) % 129.18/129.20 & v1_rat_1(B) ) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc12_waybel_0,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( l1_orders_2(A) % 129.18/129.20 => ( ( ~ v3_struct_0(A) % 129.18/129.20 & v2_orders_2(A) % 129.18/129.20 & v3_orders_2(A) % 129.18/129.20 & v4_orders_2(A) % 129.18/129.20 & v1_lattice3(A) % 129.18/129.20 & v1_yellow_0(A) % 129.18/129.20 & v24_waybel_0(A) ) % 129.18/129.20 => ( ~ v3_struct_0(A) % 129.18/129.20 & v2_orders_2(A) % 129.18/129.20 & v3_orders_2(A) % 129.18/129.20 & v4_orders_2(A) % 129.18/129.20 & v1_lattice3(A) % 129.18/129.20 & v2_lattice3(A) % 129.18/129.20 & v3_lattice3(A) % 129.18/129.20 & v1_yellow_0(A) % 129.18/129.20 & v2_yellow_0(A) % 129.18/129.20 & v3_yellow_0(A) ) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc13_membered,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( v4_membered(A) % 129.18/129.20 => ! [B] : % 129.18/129.20 ( m1_subset_1(B,A) % 129.18/129.20 => ( v1_xcmplx_0(B) % 129.18/129.20 & v1_xreal_0(B) % 129.18/129.20 & v1_int_1(B) % 129.18/129.20 & v1_rat_1(B) ) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc13_waybel_0,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( l1_orders_2(A) % 129.18/129.20 => ( ( ~ v3_struct_0(A) % 129.18/129.20 & v2_orders_2(A) % 129.18/129.20 & v4_orders_2(A) % 129.18/129.20 & v25_waybel_0(A) ) % 129.18/129.20 => ( ~ v3_struct_0(A) % 129.18/129.20 & v2_orders_2(A) % 129.18/129.20 & v4_orders_2(A) % 129.18/129.20 & v2_lattice3(A) ) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc14_membered,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( v5_membered(A) % 129.18/129.20 => ! [B] : % 129.18/129.20 ( m1_subset_1(B,A) % 129.18/129.20 => ( v1_xcmplx_0(B) % 129.18/129.20 & v4_ordinal2(B) % 129.18/129.20 & v1_xreal_0(B) % 129.18/129.20 & v1_int_1(B) % 129.18/129.20 & v1_rat_1(B) ) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc14_waybel_0,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( l1_orders_2(A) % 129.18/129.20 => ( ( ~ v3_struct_0(A) % 129.18/129.20 & v2_orders_2(A) % 129.18/129.20 & v4_orders_2(A) % 129.18/129.20 & v2_yellow_0(A) % 129.18/129.20 & v25_waybel_0(A) ) % 129.18/129.20 => ( ~ v3_struct_0(A) % 129.18/129.20 & v2_orders_2(A) % 129.18/129.20 & v4_orders_2(A) % 129.18/129.20 & v1_lattice3(A) % 129.18/129.20 & v2_yellow_0(A) ) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc15_membered,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( v1_xboole_0(A) % 129.18/129.20 => ( v1_membered(A) % 129.18/129.20 & v2_membered(A) % 129.18/129.20 & v3_membered(A) % 129.18/129.20 & v4_membered(A) % 129.18/129.20 & v5_membered(A) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc16_membered,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( v1_membered(A) % 129.18/129.20 => ! [B] : % 129.18/129.20 ( m1_subset_1(B,k1_zfmisc_1(A)) % 129.18/129.20 => v1_membered(B) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc17_membered,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( v2_membered(A) % 129.18/129.20 => ! [B] : % 129.18/129.20 ( m1_subset_1(B,k1_zfmisc_1(A)) % 129.18/129.20 => ( v1_membered(B) % 129.18/129.20 & v2_membered(B) ) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc18_membered,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( v3_membered(A) % 129.18/129.20 => ! [B] : % 129.18/129.20 ( m1_subset_1(B,k1_zfmisc_1(A)) % 129.18/129.20 => ( v1_membered(B) % 129.18/129.20 & v2_membered(B) % 129.18/129.20 & v3_membered(B) ) ) ) ). % 129.18/129.20 % 129.18/129.20 fof(cc19_membered,axiom, % 129.18/129.20 ! [A] : % 129.18/129.20 ( v4_membered(A) % 129.18/129.20 => ! [B] : % 129.18/129.20 ( m1_subset_1(B,k1_zfmisc_1(A)) % 129.18/129.20 => ( v1_membered(B) % 129.18/129.20 & v2_membered(B) % 129.18/129.20 & v3_membered(B) % 129.18/129.20 & v4_membered(B) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc1_finset_1,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( v1_xboole_0(A) % 129.18/129.21 => v1_finset_1(A) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc1_funct_1,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( v1_xboole_0(A) % 129.18/129.21 => v1_funct_1(A) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc1_lattice3,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( l1_orders_2(A) % 129.18/129.21 => ( v1_lattice3(A) % 129.18/129.21 => ~ v3_struct_0(A) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc1_membered,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( v5_membered(A) % 129.18/129.21 => v4_membered(A) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc1_relset_1,axiom, % 129.18/129.21 ! [A,B,C] : % 129.18/129.21 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 129.18/129.21 => v1_relat_1(C) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc1_setfam_1,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( ( ~ v1_xboole_0(A) % 129.18/129.21 & v1_setfam_1(A) ) % 129.18/129.21 => ! [B] : % 129.18/129.21 ( m1_subset_1(B,A) % 129.18/129.21 => ~ v1_xboole_0(B) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc1_waybel10,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( ( ~ v3_struct_0(A) % 129.18/129.21 & l1_orders_2(A) ) % 129.18/129.21 => ! [B] : % 129.18/129.21 ( m1_relset_1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.21 => ( ( v1_funct_1(B) % 129.18/129.21 & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.21 & v6_waybel_1(B,A) ) % 129.18/129.21 => ( v1_funct_1(B) % 129.18/129.21 & ~ v1_xboole_0(B) % 129.18/129.21 & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.21 & v1_partfun1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.21 & v11_quantal1(B) % 129.18/129.21 & v5_orders_3(B,A,A) ) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc1_waybel17,axiom, % 129.18/129.21 ! [A,B] : % 129.18/129.21 ( ( ~ v3_struct_0(A) % 129.18/129.21 & v2_orders_2(A) % 129.18/129.21 & v4_orders_2(A) % 129.18/129.21 & l1_orders_2(A) % 129.18/129.21 & ~ v3_struct_0(B) % 129.18/129.21 & v2_orders_2(B) % 129.18/129.21 & v4_orders_2(B) % 129.18/129.21 & l1_orders_2(B) ) % 129.18/129.21 => ! [C] : % 129.18/129.21 ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 => ( ( v1_funct_1(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v22_waybel_0(C,A,B) ) % 129.18/129.21 => ( ~ v1_xboole_0(C) % 129.18/129.21 & v1_funct_1(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v5_orders_3(C,A,B) % 129.18/129.21 & v1_partfun1(C,u1_struct_0(A),u1_struct_0(B)) ) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc1_waybel21,axiom, % 129.18/129.21 ! [A,B] : % 129.18/129.21 ( ( v2_orders_2(A) % 129.18/129.21 & v3_orders_2(A) % 129.18/129.21 & v4_orders_2(A) % 129.18/129.21 & v2_lattice3(A) % 129.18/129.21 & l1_orders_2(A) % 129.18/129.21 & v2_orders_2(B) % 129.18/129.21 & v3_orders_2(B) % 129.18/129.21 & v4_orders_2(B) % 129.18/129.21 & v2_lattice3(B) % 129.18/129.21 & l1_orders_2(B) ) % 129.18/129.21 => ! [C] : % 129.18/129.21 ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 => ( ( v1_funct_1(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v19_waybel_0(C,A,B) ) % 129.18/129.21 => ( v1_funct_1(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v5_orders_3(C,A,B) ) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc1_waybel_1,axiom, % 129.18/129.21 ! [A,B] : % 129.18/129.21 ( ( ~ v3_struct_0(A) % 129.18/129.21 & v2_orders_2(A) % 129.18/129.21 & v3_orders_2(A) % 129.18/129.21 & v4_orders_2(A) % 129.18/129.21 & l1_orders_2(A) % 129.18/129.21 & ~ v3_struct_0(B) % 129.18/129.21 & v2_orders_2(B) % 129.18/129.21 & v3_orders_2(B) % 129.18/129.21 & v4_orders_2(B) % 129.18/129.21 & l1_orders_2(B) ) % 129.18/129.21 => ! [C] : % 129.18/129.21 ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 => ( ( v1_funct_1(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v4_waybel_1(C,A,B) ) % 129.18/129.21 => ( v1_funct_1(C) % 129.18/129.21 & ~ v1_xboole_0(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v1_partfun1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v17_waybel_0(C,A,B) % 129.18/129.21 & v19_waybel_0(C,A,B) % 129.18/129.21 & v21_waybel_0(C,A,B) ) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc1_yellow_0,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( l1_orders_2(A) % 129.18/129.21 => ( ( ~ v3_struct_0(A) % 129.18/129.21 & v3_lattice3(A) ) % 129.18/129.21 => ( ~ v3_struct_0(A) % 129.18/129.21 & v1_lattice3(A) % 129.18/129.21 & v2_lattice3(A) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc1_yellow_2,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( l1_orders_2(A) % 129.18/129.21 => ( ( ~ v3_struct_0(A) % 129.18/129.21 & v2_orders_2(A) % 129.18/129.21 & v3_orders_2(A) % 129.18/129.21 & v4_orders_2(A) % 129.18/129.21 & v2_yellow_0(A) % 129.18/129.21 & v24_waybel_0(A) % 129.18/129.21 & v25_waybel_0(A) ) % 129.18/129.21 => ( ~ v3_struct_0(A) % 129.18/129.21 & v2_orders_2(A) % 129.18/129.21 & v3_orders_2(A) % 129.18/129.21 & v4_orders_2(A) % 129.18/129.21 & v1_yellow_0(A) % 129.18/129.21 & v2_yellow_0(A) % 129.18/129.21 & v3_yellow_0(A) % 129.18/129.21 & v24_waybel_0(A) % 129.18/129.21 & v25_waybel_0(A) % 129.18/129.21 & v1_lattice3(A) % 129.18/129.21 & v2_lattice3(A) % 129.18/129.21 & v3_lattice3(A) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc20_membered,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( v5_membered(A) % 129.18/129.21 => ! [B] : % 129.18/129.21 ( m1_subset_1(B,k1_zfmisc_1(A)) % 129.18/129.21 => ( v1_membered(B) % 129.18/129.21 & v2_membered(B) % 129.18/129.21 & v3_membered(B) % 129.18/129.21 & v4_membered(B) % 129.18/129.21 & v5_membered(B) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc2_finset_1,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( v1_finset_1(A) % 129.18/129.21 => ! [B] : % 129.18/129.21 ( m1_subset_1(B,k1_zfmisc_1(A)) % 129.18/129.21 => v1_finset_1(B) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc2_funct_1,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( ( v1_relat_1(A) % 129.18/129.21 & v1_xboole_0(A) % 129.18/129.21 & v1_funct_1(A) ) % 129.18/129.21 => ( v1_relat_1(A) % 129.18/129.21 & v1_funct_1(A) % 129.18/129.21 & v2_funct_1(A) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc2_lattice3,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( l1_orders_2(A) % 129.18/129.21 => ( v2_lattice3(A) % 129.18/129.21 => ~ v3_struct_0(A) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc2_membered,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( v4_membered(A) % 129.18/129.21 => v3_membered(A) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc2_waybel_1,axiom, % 129.18/129.21 ! [A,B] : % 129.18/129.21 ( ( ~ v3_struct_0(A) % 129.18/129.21 & v2_orders_2(A) % 129.18/129.21 & v3_orders_2(A) % 129.18/129.21 & v4_orders_2(A) % 129.18/129.21 & l1_orders_2(A) % 129.18/129.21 & ~ v3_struct_0(B) % 129.18/129.21 & v2_orders_2(B) % 129.18/129.21 & v3_orders_2(B) % 129.18/129.21 & v4_orders_2(B) % 129.18/129.21 & l1_orders_2(B) ) % 129.18/129.21 => ! [C] : % 129.18/129.21 ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 => ( ( v1_funct_1(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v5_waybel_1(C,B,A) ) % 129.18/129.21 => ( v1_funct_1(C) % 129.18/129.21 & ~ v1_xboole_0(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v1_partfun1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v18_waybel_0(C,A,B) % 129.18/129.21 & v20_waybel_0(C,A,B) % 129.18/129.21 & v22_waybel_0(C,A,B) ) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc3_membered,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( v3_membered(A) % 129.18/129.21 => v2_membered(A) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc3_waybel_1,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( ( ~ v3_struct_0(A) % 129.18/129.21 & l1_orders_2(A) ) % 129.18/129.21 => ! [B] : % 129.18/129.21 ( m1_relset_1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.21 => ( ( v1_funct_1(B) % 129.18/129.21 & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.21 & v7_waybel_1(B,A) ) % 129.18/129.21 => ( v1_funct_1(B) % 129.18/129.21 & ~ v1_xboole_0(B) % 129.18/129.21 & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.21 & v1_partfun1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.21 & v6_waybel_1(B,A) ) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc3_yellow_0,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( l1_orders_2(A) % 129.18/129.21 => ( ( ~ v3_struct_0(A) % 129.18/129.21 & v3_lattice3(A) ) % 129.18/129.21 => ( ~ v3_struct_0(A) % 129.18/129.21 & v3_yellow_0(A) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc4_membered,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( v2_membered(A) % 129.18/129.21 => v1_membered(A) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc4_waybel_1,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( ( ~ v3_struct_0(A) % 129.18/129.21 & l1_orders_2(A) ) % 129.18/129.21 => ! [B] : % 129.18/129.21 ( m1_relset_1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.21 => ( ( v1_funct_1(B) % 129.18/129.21 & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.21 & v8_waybel_1(B,A) ) % 129.18/129.21 => ( v1_funct_1(B) % 129.18/129.21 & ~ v1_xboole_0(B) % 129.18/129.21 & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.21 & v1_partfun1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.21 & v6_waybel_1(B,A) ) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc4_yellow_0,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( l1_orders_2(A) % 129.18/129.21 => ( v3_yellow_0(A) % 129.18/129.21 => ( v1_yellow_0(A) % 129.18/129.21 & v2_yellow_0(A) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc5_yellow_0,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( l1_orders_2(A) % 129.18/129.21 => ( ( v1_yellow_0(A) % 129.18/129.21 & v2_yellow_0(A) ) % 129.18/129.21 => v3_yellow_0(A) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc6_waybel_0,axiom, % 129.18/129.21 ! [A,B] : % 129.18/129.21 ( ( ~ v3_struct_0(A) % 129.18/129.21 & l1_orders_2(A) % 129.18/129.21 & ~ v3_struct_0(B) % 129.18/129.21 & l1_orders_2(B) ) % 129.18/129.21 => ! [C] : % 129.18/129.21 ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 => ( ( v1_funct_1(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v17_waybel_0(C,A,B) ) % 129.18/129.21 => ( v1_funct_1(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v19_waybel_0(C,A,B) % 129.18/129.21 & v21_waybel_0(C,A,B) ) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc7_waybel_0,axiom, % 129.18/129.21 ! [A,B] : % 129.18/129.21 ( ( ~ v3_struct_0(A) % 129.18/129.21 & l1_orders_2(A) % 129.18/129.21 & ~ v3_struct_0(B) % 129.18/129.21 & l1_orders_2(B) ) % 129.18/129.21 => ! [C] : % 129.18/129.21 ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 => ( ( v1_funct_1(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v18_waybel_0(C,A,B) ) % 129.18/129.21 => ( v1_funct_1(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v20_waybel_0(C,A,B) % 129.18/129.21 & v22_waybel_0(C,A,B) ) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc8_waybel_0,axiom, % 129.18/129.21 ! [A,B] : % 129.18/129.21 ( ( ~ v3_struct_0(A) % 129.18/129.21 & l1_orders_2(A) % 129.18/129.21 & ~ v3_struct_0(B) % 129.18/129.21 & l1_orders_2(B) ) % 129.18/129.21 => ! [C] : % 129.18/129.21 ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 => ( ( v1_funct_1(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v23_waybel_0(C,A,B) ) % 129.18/129.21 => ( v1_funct_1(C) % 129.18/129.21 & v2_funct_1(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & v5_orders_3(C,A,B) ) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(cc9_waybel_0,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( l1_orders_2(A) % 129.18/129.21 => ( ( v2_orders_2(A) % 129.18/129.21 & v1_lattice3(A) % 129.18/129.21 & v24_waybel_0(A) ) % 129.18/129.21 => ( ~ v3_struct_0(A) % 129.18/129.21 & v2_orders_2(A) % 129.18/129.21 & v1_lattice3(A) % 129.18/129.21 & v2_yellow_0(A) ) ) ) ). % 129.18/129.21 % 129.18/129.21 fof(commutativity_k2_tarski,axiom, % 129.18/129.21 ! [A,B] : k2_tarski(A,B) = k2_tarski(B,A) ). % 129.18/129.21 % 129.18/129.21 fof(d1_waybel34,axiom, % 129.18/129.21 ! [A] : % 129.18/129.21 ( ( v2_orders_2(A) % 129.18/129.21 & v3_orders_2(A) % 129.18/129.21 & v4_orders_2(A) % 129.18/129.21 & v1_lattice3(A) % 129.18/129.21 & v2_lattice3(A) % 129.18/129.21 & l1_orders_2(A) ) % 129.18/129.21 => ! [B] : % 129.18/129.21 ( ( v2_orders_2(B) % 129.18/129.21 & v3_orders_2(B) % 129.18/129.21 & v4_orders_2(B) % 129.18/129.21 & v1_lattice3(B) % 129.18/129.21 & v2_lattice3(B) % 129.18/129.21 & l1_orders_2(B) ) % 129.18/129.21 => ! [C] : % 129.18/129.21 ( ( v1_funct_1(C) % 129.18/129.21 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.21 & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) % 129.18/129.21 => ( ( v3_lattice3(A) % 129.18/129.21 & v3_lattice3(B) % 129.18/129.21 & v17_waybel_0(C,A,B) ) % 129.18/129.22 => ! [D] : % 129.18/129.22 ( ( v1_funct_1(D) % 129.18/129.22 & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) % 129.18/129.22 & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) % 129.18/129.22 => ( D = k1_waybel34(A,B,C) % 129.18/129.22 <=> v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) ) ) ) ) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(d2_waybel34,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( ( v2_orders_2(A) % 129.18/129.22 & v3_orders_2(A) % 129.18/129.22 & v4_orders_2(A) % 129.18/129.22 & v1_lattice3(A) % 129.18/129.22 & v2_lattice3(A) % 129.18/129.22 & l1_orders_2(A) ) % 129.18/129.22 => ! [B] : % 129.18/129.22 ( ( v2_orders_2(B) % 129.18/129.22 & v3_orders_2(B) % 129.18/129.22 & v4_orders_2(B) % 129.18/129.22 & v1_lattice3(B) % 129.18/129.22 & v2_lattice3(B) % 129.18/129.22 & l1_orders_2(B) ) % 129.18/129.22 => ! [C] : % 129.18/129.22 ( ( v1_funct_1(C) % 129.18/129.22 & v1_funct_2(C,u1_struct_0(B),u1_struct_0(A)) % 129.18/129.22 & m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) ) % 129.18/129.22 => ( ( v3_lattice3(A) % 129.18/129.22 & v3_lattice3(B) % 129.18/129.22 & v18_waybel_0(C,B,A) ) % 129.18/129.22 => ! [D] : % 129.18/129.22 ( ( v1_funct_1(D) % 129.18/129.22 & v1_funct_2(D,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.22 & m2_relset_1(D,u1_struct_0(A),u1_struct_0(B)) ) % 129.18/129.22 => ( D = k2_waybel34(A,B,C) % 129.18/129.22 <=> v3_waybel_1(k1_waybel_1(A,B,D,C),A,B) ) ) ) ) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(d5_tarski,axiom, % 129.18/129.22 ! [A,B] : k4_tarski(A,B) = k2_tarski(k2_tarski(A,B),k1_tarski(A)) ). % 129.18/129.22 % 129.18/129.22 fof(dt_k1_tarski,axiom, % 129.18/129.22 $true ). % 129.18/129.22 % 129.18/129.22 fof(dt_k1_waybel34,axiom, % 129.18/129.22 ! [A,B,C] : % 129.18/129.22 ( ( v2_orders_2(A) % 129.18/129.22 & v3_orders_2(A) % 129.18/129.22 & v4_orders_2(A) % 129.18/129.22 & v1_lattice3(A) % 129.18/129.22 & v2_lattice3(A) % 129.18/129.22 & l1_orders_2(A) % 129.18/129.22 & v2_orders_2(B) % 129.18/129.22 & v3_orders_2(B) % 129.18/129.22 & v4_orders_2(B) % 129.18/129.22 & v1_lattice3(B) % 129.18/129.22 & v2_lattice3(B) % 129.18/129.22 & l1_orders_2(B) % 129.18/129.22 & v1_funct_1(C) % 129.18/129.22 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.22 & m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) % 129.18/129.22 => ( v1_funct_1(k1_waybel34(A,B,C)) % 129.18/129.22 & v1_funct_2(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A)) % 129.18/129.22 & m2_relset_1(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(dt_k1_waybel_1,axiom, % 129.18/129.22 ! [A,B,C,D] : % 129.18/129.22 ( ( l1_orders_2(A) % 129.18/129.22 & l1_orders_2(B) % 129.18/129.22 & v1_funct_1(C) % 129.18/129.22 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.22 & m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.22 & v1_funct_1(D) % 129.18/129.22 & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) % 129.18/129.22 & m1_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) % 129.18/129.22 => m1_waybel_1(k1_waybel_1(A,B,C,D),A,B) ) ). % 129.18/129.22 % 129.18/129.22 fof(dt_k1_xboole_0,axiom, % 129.18/129.22 $true ). % 129.18/129.22 % 129.18/129.22 fof(dt_k1_zfmisc_1,axiom, % 129.18/129.22 $true ). % 129.18/129.22 % 129.18/129.22 fof(dt_k2_tarski,axiom, % 129.18/129.22 $true ). % 129.18/129.22 % 129.18/129.22 fof(dt_k2_waybel34,axiom, % 129.18/129.22 ! [A,B,C] : % 129.18/129.22 ( ( v2_orders_2(A) % 129.18/129.22 & v3_orders_2(A) % 129.18/129.22 & v4_orders_2(A) % 129.18/129.22 & v1_lattice3(A) % 129.18/129.22 & v2_lattice3(A) % 129.18/129.22 & l1_orders_2(A) % 129.18/129.22 & v2_orders_2(B) % 129.18/129.22 & v3_orders_2(B) % 129.18/129.22 & v4_orders_2(B) % 129.18/129.22 & v1_lattice3(B) % 129.18/129.22 & v2_lattice3(B) % 129.18/129.22 & l1_orders_2(B) % 129.18/129.22 & v1_funct_1(C) % 129.18/129.22 & v1_funct_2(C,u1_struct_0(B),u1_struct_0(A)) % 129.18/129.22 & m1_relset_1(C,u1_struct_0(B),u1_struct_0(A)) ) % 129.18/129.22 => ( v1_funct_1(k2_waybel34(A,B,C)) % 129.18/129.22 & v1_funct_2(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B)) % 129.18/129.22 & m2_relset_1(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(dt_k2_zfmisc_1,axiom, % 129.18/129.22 $true ). % 129.18/129.22 % 129.18/129.22 fof(dt_k4_tarski,axiom, % 129.18/129.22 $true ). % 129.18/129.22 % 129.18/129.22 fof(dt_k7_grcat_1,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( l1_struct_0(A) % 129.18/129.22 => ( v1_funct_1(k7_grcat_1(A)) % 129.18/129.22 & v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & m2_relset_1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(dt_l1_orders_2,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( l1_orders_2(A) % 129.18/129.22 => l1_struct_0(A) ) ). % 129.18/129.22 % 129.18/129.22 fof(dt_l1_struct_0,axiom, % 129.18/129.22 $true ). % 129.18/129.22 % 129.18/129.22 fof(dt_m1_relset_1,axiom, % 129.18/129.22 $true ). % 129.18/129.22 % 129.18/129.22 fof(dt_m1_subset_1,axiom, % 129.18/129.22 $true ). % 129.18/129.22 % 129.18/129.22 fof(dt_m1_waybel_1,axiom, % 129.18/129.22 $true ). % 129.18/129.22 % 129.18/129.22 fof(dt_m2_relset_1,axiom, % 129.18/129.22 ! [A,B,C] : % 129.18/129.22 ( m2_relset_1(C,A,B) % 129.18/129.22 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 129.18/129.22 % 129.18/129.22 fof(dt_u1_struct_0,axiom, % 129.18/129.22 $true ). % 129.18/129.22 % 129.18/129.22 fof(existence_l1_orders_2,axiom, % 129.18/129.22 ? [A] : l1_orders_2(A) ). % 129.18/129.22 % 129.18/129.22 fof(existence_l1_struct_0,axiom, % 129.18/129.22 ? [A] : l1_struct_0(A) ). % 129.18/129.22 % 129.18/129.22 fof(existence_m1_relset_1,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ? [C] : m1_relset_1(C,A,B) ). % 129.18/129.22 % 129.18/129.22 fof(existence_m1_subset_1,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ? [B] : m1_subset_1(B,A) ). % 129.18/129.22 % 129.18/129.22 fof(existence_m1_waybel_1,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ( ( l1_orders_2(A) % 129.18/129.22 & l1_orders_2(B) ) % 129.18/129.22 => ? [C] : m1_waybel_1(C,A,B) ) ). % 129.18/129.22 % 129.18/129.22 fof(existence_m2_relset_1,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ? [C] : m2_relset_1(C,A,B) ). % 129.18/129.22 % 129.18/129.22 fof(fc10_membered,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( v1_int_1(A) % 129.18/129.22 => ( v1_membered(k1_tarski(A)) % 129.18/129.22 & v2_membered(k1_tarski(A)) % 129.18/129.22 & v3_membered(k1_tarski(A)) % 129.18/129.22 & v4_membered(k1_tarski(A)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc11_membered,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( v4_ordinal2(A) % 129.18/129.22 => ( v1_membered(k1_tarski(A)) % 129.18/129.22 & v2_membered(k1_tarski(A)) % 129.18/129.22 & v3_membered(k1_tarski(A)) % 129.18/129.22 & v4_membered(k1_tarski(A)) % 129.18/129.22 & v5_membered(k1_tarski(A)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc12_membered,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ( ( v1_xcmplx_0(A) % 129.18/129.22 & v1_xcmplx_0(B) ) % 129.18/129.22 => v1_membered(k2_tarski(A,B)) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc13_membered,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ( ( v1_xreal_0(A) % 129.18/129.22 & v1_xreal_0(B) ) % 129.18/129.22 => ( v1_membered(k2_tarski(A,B)) % 129.18/129.22 & v2_membered(k2_tarski(A,B)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc14_finset_1,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ( ( v1_finset_1(A) % 129.18/129.22 & v1_finset_1(B) ) % 129.18/129.22 => v1_finset_1(k2_zfmisc_1(A,B)) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc14_membered,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ( ( v1_rat_1(A) % 129.18/129.22 & v1_rat_1(B) ) % 129.18/129.22 => ( v1_membered(k2_tarski(A,B)) % 129.18/129.22 & v2_membered(k2_tarski(A,B)) % 129.18/129.22 & v3_membered(k2_tarski(A,B)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc15_membered,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ( ( v1_int_1(A) % 129.18/129.22 & v1_int_1(B) ) % 129.18/129.22 => ( v1_membered(k2_tarski(A,B)) % 129.18/129.22 & v2_membered(k2_tarski(A,B)) % 129.18/129.22 & v3_membered(k2_tarski(A,B)) % 129.18/129.22 & v4_membered(k2_tarski(A,B)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc16_membered,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ( ( v4_ordinal2(A) % 129.18/129.22 & v4_ordinal2(B) ) % 129.18/129.22 => ( v1_membered(k2_tarski(A,B)) % 129.18/129.22 & v2_membered(k2_tarski(A,B)) % 129.18/129.22 & v3_membered(k2_tarski(A,B)) % 129.18/129.22 & v4_membered(k2_tarski(A,B)) % 129.18/129.22 & v5_membered(k2_tarski(A,B)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc1_finset_1,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( ~ v1_xboole_0(k1_tarski(A)) % 129.18/129.22 & v1_finset_1(k1_tarski(A)) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc1_struct_0,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( ( ~ v3_struct_0(A) % 129.18/129.22 & l1_struct_0(A) ) % 129.18/129.22 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc1_waybel34,axiom, % 129.18/129.22 ! [A,B,C] : % 129.18/129.22 ( ( v2_orders_2(A) % 129.18/129.22 & v3_orders_2(A) % 129.18/129.22 & v4_orders_2(A) % 129.18/129.22 & v1_lattice3(A) % 129.18/129.22 & v2_lattice3(A) % 129.18/129.22 & v3_lattice3(A) % 129.18/129.22 & l1_orders_2(A) % 129.18/129.22 & v2_orders_2(B) % 129.18/129.22 & v3_orders_2(B) % 129.18/129.22 & v4_orders_2(B) % 129.18/129.22 & v1_lattice3(B) % 129.18/129.22 & v2_lattice3(B) % 129.18/129.22 & v3_lattice3(B) % 129.18/129.22 & l1_orders_2(B) % 129.18/129.22 & v1_funct_1(C) % 129.18/129.22 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.22 & v17_waybel_0(C,A,B) % 129.18/129.22 & m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) % 129.18/129.22 => ( v1_relat_1(k1_waybel34(A,B,C)) % 129.18/129.22 & v1_funct_1(k1_waybel34(A,B,C)) % 129.18/129.22 & ~ v1_xboole_0(k1_waybel34(A,B,C)) % 129.18/129.22 & v1_funct_2(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A)) % 129.18/129.22 & v1_partfun1(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A)) % 129.18/129.22 & v18_waybel_0(k1_waybel34(A,B,C),B,A) % 129.18/129.22 & v20_waybel_0(k1_waybel34(A,B,C),B,A) % 129.18/129.22 & v22_waybel_0(k1_waybel34(A,B,C),B,A) % 129.18/129.22 & v5_waybel_1(k1_waybel34(A,B,C),A,B) % 129.18/129.22 & v5_orders_3(k1_waybel34(A,B,C),B,A) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc2_finset_1,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ( ~ v1_xboole_0(k2_tarski(A,B)) % 129.18/129.22 & v1_finset_1(k2_tarski(A,B)) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc2_setfam_1,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( ~ v1_xboole_0(A) % 129.18/129.22 => ( ~ v1_xboole_0(k1_tarski(A)) % 129.18/129.22 & v1_setfam_1(k1_tarski(A)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc2_waybel34,axiom, % 129.18/129.22 ! [A,B,C] : % 129.18/129.22 ( ( v2_orders_2(A) % 129.18/129.22 & v3_orders_2(A) % 129.18/129.22 & v4_orders_2(A) % 129.18/129.22 & v1_lattice3(A) % 129.18/129.22 & v2_lattice3(A) % 129.18/129.22 & v3_lattice3(A) % 129.18/129.22 & l1_orders_2(A) % 129.18/129.22 & v2_orders_2(B) % 129.18/129.22 & v3_orders_2(B) % 129.18/129.22 & v4_orders_2(B) % 129.18/129.22 & v1_lattice3(B) % 129.18/129.22 & v2_lattice3(B) % 129.18/129.22 & v3_lattice3(B) % 129.18/129.22 & l1_orders_2(B) % 129.18/129.22 & v1_funct_1(C) % 129.18/129.22 & v1_funct_2(C,u1_struct_0(B),u1_struct_0(A)) % 129.18/129.22 & v18_waybel_0(C,B,A) % 129.18/129.22 & m1_relset_1(C,u1_struct_0(B),u1_struct_0(A)) ) % 129.18/129.22 => ( v1_relat_1(k2_waybel34(A,B,C)) % 129.18/129.22 & v1_funct_1(k2_waybel34(A,B,C)) % 129.18/129.22 & ~ v1_xboole_0(k2_waybel34(A,B,C)) % 129.18/129.22 & v1_funct_2(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B)) % 129.18/129.22 & v1_partfun1(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B)) % 129.18/129.22 & v17_waybel_0(k2_waybel34(A,B,C),A,B) % 129.18/129.22 & v19_waybel_0(k2_waybel34(A,B,C),A,B) % 129.18/129.22 & v21_waybel_0(k2_waybel34(A,B,C),A,B) % 129.18/129.22 & v4_waybel_1(k2_waybel34(A,B,C),A,B) % 129.18/129.22 & v5_orders_3(k2_waybel34(A,B,C),A,B) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc2_waybel_1,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( l1_orders_2(A) % 129.18/129.22 => ( v1_relat_1(k7_grcat_1(A)) % 129.18/129.22 & v1_funct_1(k7_grcat_1(A)) % 129.18/129.22 & v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v23_waybel_0(k7_grcat_1(A),A,A) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc3_setfam_1,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ( ( ~ v1_xboole_0(A) % 129.18/129.22 & ~ v1_xboole_0(B) ) % 129.18/129.22 => ( ~ v1_xboole_0(k2_tarski(A,B)) % 129.18/129.22 & v1_setfam_1(k2_tarski(A,B)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc3_waybel10,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( l1_struct_0(A) % 129.18/129.22 => ( v1_relat_1(k7_grcat_1(A)) % 129.18/129.22 & v1_funct_1(k7_grcat_1(A)) % 129.18/129.22 & v2_funct_1(k7_grcat_1(A)) % 129.18/129.22 & v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc3_waybel_1,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( ( ~ v3_struct_0(A) % 129.18/129.22 & l1_orders_2(A) ) % 129.18/129.22 => ( v1_relat_1(k7_grcat_1(A)) % 129.18/129.22 & v1_funct_1(k7_grcat_1(A)) % 129.18/129.22 & v2_funct_1(k7_grcat_1(A)) % 129.18/129.22 & ~ v1_xboole_0(k7_grcat_1(A)) % 129.18/129.22 & v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v1_partfun1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v5_orders_3(k7_grcat_1(A),A,A) % 129.18/129.22 & v23_waybel_0(k7_grcat_1(A),A,A) % 129.18/129.22 & v6_waybel_1(k7_grcat_1(A),A) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc4_waybel10,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( ( ~ v3_struct_0(A) % 129.18/129.22 & v2_orders_2(A) % 129.18/129.22 & l1_orders_2(A) ) % 129.18/129.22 => ( v1_relat_1(k7_grcat_1(A)) % 129.18/129.22 & v1_funct_1(k7_grcat_1(A)) % 129.18/129.22 & v2_funct_1(k7_grcat_1(A)) % 129.18/129.22 & ~ v1_xboole_0(k7_grcat_1(A)) % 129.18/129.22 & v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v1_partfun1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v11_quantal1(k7_grcat_1(A)) % 129.18/129.22 & v5_orders_3(k7_grcat_1(A),A,A) % 129.18/129.22 & v17_waybel_0(k7_grcat_1(A),A,A) % 129.18/129.22 & v18_waybel_0(k7_grcat_1(A),A,A) % 129.18/129.22 & v19_waybel_0(k7_grcat_1(A),A,A) % 129.18/129.22 & v20_waybel_0(k7_grcat_1(A),A,A) % 129.18/129.22 & v21_waybel_0(k7_grcat_1(A),A,A) % 129.18/129.22 & v22_waybel_0(k7_grcat_1(A),A,A) % 129.18/129.22 & v23_waybel_0(k7_grcat_1(A),A,A) % 129.18/129.22 & v6_waybel_1(k7_grcat_1(A),A) % 129.18/129.22 & v7_waybel_1(k7_grcat_1(A),A) % 129.18/129.22 & v8_waybel_1(k7_grcat_1(A),A) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc4_waybel_1,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( ( ~ v3_struct_0(A) % 129.18/129.22 & v2_orders_2(A) % 129.18/129.22 & l1_orders_2(A) ) % 129.18/129.22 => ( v1_relat_1(k7_grcat_1(A)) % 129.18/129.22 & v1_funct_1(k7_grcat_1(A)) % 129.18/129.22 & v2_funct_1(k7_grcat_1(A)) % 129.18/129.22 & ~ v1_xboole_0(k7_grcat_1(A)) % 129.18/129.22 & v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v1_partfun1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v5_orders_3(k7_grcat_1(A),A,A) % 129.18/129.22 & v23_waybel_0(k7_grcat_1(A),A,A) % 129.18/129.22 & v6_waybel_1(k7_grcat_1(A),A) % 129.18/129.22 & v7_waybel_1(k7_grcat_1(A),A) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc5_waybel_1,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( ( ~ v3_struct_0(A) % 129.18/129.22 & v2_orders_2(A) % 129.18/129.22 & l1_orders_2(A) ) % 129.18/129.22 => ( v1_relat_1(k7_grcat_1(A)) % 129.18/129.22 & v1_funct_1(k7_grcat_1(A)) % 129.18/129.22 & v2_funct_1(k7_grcat_1(A)) % 129.18/129.22 & ~ v1_xboole_0(k7_grcat_1(A)) % 129.18/129.22 & v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v1_partfun1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v5_orders_3(k7_grcat_1(A),A,A) % 129.18/129.22 & v23_waybel_0(k7_grcat_1(A),A,A) % 129.18/129.22 & v6_waybel_1(k7_grcat_1(A),A) % 129.18/129.22 & v7_waybel_1(k7_grcat_1(A),A) % 129.18/129.22 & v8_waybel_1(k7_grcat_1(A),A) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc6_membered,axiom, % 129.18/129.22 ( v1_xboole_0(k1_xboole_0) % 129.18/129.22 & v1_membered(k1_xboole_0) % 129.18/129.22 & v2_membered(k1_xboole_0) % 129.18/129.22 & v3_membered(k1_xboole_0) % 129.18/129.22 & v4_membered(k1_xboole_0) % 129.18/129.22 & v5_membered(k1_xboole_0) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc7_membered,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( v1_xcmplx_0(A) % 129.18/129.22 => v1_membered(k1_tarski(A)) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc8_membered,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( v1_xreal_0(A) % 129.18/129.22 => ( v1_membered(k1_tarski(A)) % 129.18/129.22 & v2_membered(k1_tarski(A)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(fc9_membered,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( v1_rat_1(A) % 129.18/129.22 => ( v1_membered(k1_tarski(A)) % 129.18/129.22 & v2_membered(k1_tarski(A)) % 129.18/129.22 & v3_membered(k1_tarski(A)) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(rc1_finset_1,axiom, % 129.18/129.22 ? [A] : % 129.18/129.22 ( ~ v1_xboole_0(A) % 129.18/129.22 & v1_finset_1(A) ) ). % 129.18/129.22 % 129.18/129.22 fof(rc1_funct_1,axiom, % 129.18/129.22 ? [A] : % 129.18/129.22 ( v1_relat_1(A) % 129.18/129.22 & v1_funct_1(A) ) ). % 129.18/129.22 % 129.18/129.22 fof(rc1_lattice5,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ( ( v2_orders_2(A) % 129.18/129.22 & v3_orders_2(A) % 129.18/129.22 & v4_orders_2(A) % 129.18/129.22 & v1_lattice3(A) % 129.18/129.22 & v2_lattice3(A) % 129.18/129.22 & l1_orders_2(A) % 129.18/129.22 & v2_orders_2(B) % 129.18/129.22 & v3_orders_2(B) % 129.18/129.22 & v4_orders_2(B) % 129.18/129.22 & v1_lattice3(B) % 129.18/129.22 & v2_lattice3(B) % 129.18/129.22 & l1_orders_2(B) ) % 129.18/129.22 => ? [C] : % 129.18/129.22 ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.22 & v1_relat_1(C) % 129.18/129.22 & v1_funct_1(C) % 129.18/129.22 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.22 & v19_waybel_0(C,A,B) % 129.18/129.22 & v20_waybel_0(C,A,B) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(rc1_membered,axiom, % 129.18/129.22 ? [A] : % 129.18/129.22 ( ~ v1_xboole_0(A) % 129.18/129.22 & v1_membered(A) % 129.18/129.22 & v2_membered(A) % 129.18/129.22 & v3_membered(A) % 129.18/129.22 & v4_membered(A) % 129.18/129.22 & v5_membered(A) ) ). % 129.18/129.22 % 129.18/129.22 fof(rc1_setfam_1,axiom, % 129.18/129.22 ? [A] : % 129.18/129.22 ( ~ v1_xboole_0(A) % 129.18/129.22 & v1_setfam_1(A) ) ). % 129.18/129.22 % 129.18/129.22 fof(rc1_waybel10,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ( ( l1_orders_2(A) % 129.18/129.22 & ~ v3_struct_0(B) % 129.18/129.22 & v2_orders_2(B) % 129.18/129.22 & l1_orders_2(B) ) % 129.18/129.22 => ? [C] : % 129.18/129.22 ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.22 & v1_relat_1(C) % 129.18/129.22 & v1_funct_1(C) % 129.18/129.22 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.22 & v1_partfun1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.22 & v5_orders_3(C,A,B) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(rc1_waybel34,axiom, % 129.18/129.22 ! [A,B] : % 129.18/129.22 ( ( v2_orders_2(A) % 129.18/129.22 & v3_orders_2(A) % 129.18/129.22 & v4_orders_2(A) % 129.18/129.22 & v1_lattice3(A) % 129.18/129.22 & v2_lattice3(A) % 129.18/129.22 & v3_lattice3(A) % 129.18/129.22 & l1_orders_2(A) % 129.18/129.22 & v2_orders_2(B) % 129.18/129.22 & v3_orders_2(B) % 129.18/129.22 & v4_orders_2(B) % 129.18/129.22 & v1_lattice3(B) % 129.18/129.22 & v2_lattice3(B) % 129.18/129.22 & v3_lattice3(B) % 129.18/129.22 & l1_orders_2(B) ) % 129.18/129.22 => ? [C] : % 129.18/129.22 ( m1_waybel_1(C,A,B) % 129.18/129.22 & v3_waybel_1(C,A,B) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(rc1_waybel_1,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( ( ~ v3_struct_0(A) % 129.18/129.22 & l1_orders_2(A) ) % 129.18/129.22 => ? [B] : % 129.18/129.22 ( m1_relset_1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v1_relat_1(B) % 129.18/129.22 & v1_funct_1(B) % 129.18/129.22 & ~ v1_xboole_0(B) % 129.18/129.22 & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v1_partfun1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v6_waybel_1(B,A) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(rc2_funct_1,axiom, % 129.18/129.22 ? [A] : % 129.18/129.22 ( v1_relat_1(A) % 129.18/129.22 & v1_xboole_0(A) % 129.18/129.22 & v1_funct_1(A) ) ). % 129.18/129.22 % 129.18/129.22 fof(rc2_waybel10,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( ( ~ v3_struct_0(A) % 129.18/129.22 & v2_orders_2(A) % 129.18/129.22 & l1_orders_2(A) ) % 129.18/129.22 => ? [B] : % 129.18/129.22 ( m1_relset_1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v1_relat_1(B) % 129.18/129.22 & v1_funct_1(B) % 129.18/129.22 & v2_funct_1(B) % 129.18/129.22 & ~ v1_xboole_0(B) % 129.18/129.22 & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v1_partfun1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v11_quantal1(B) % 129.18/129.22 & v5_orders_3(B,A,A) % 129.18/129.22 & v17_waybel_0(B,A,A) % 129.18/129.22 & v18_waybel_0(B,A,A) % 129.18/129.22 & v19_waybel_0(B,A,A) % 129.18/129.22 & v20_waybel_0(B,A,A) % 129.18/129.22 & v21_waybel_0(B,A,A) % 129.18/129.22 & v22_waybel_0(B,A,A) % 129.18/129.22 & v6_waybel_1(B,A) % 129.18/129.22 & v7_waybel_1(B,A) % 129.18/129.22 & v8_waybel_1(B,A) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(rc2_waybel_1,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( ( ~ v3_struct_0(A) % 129.18/129.22 & v2_orders_2(A) % 129.18/129.22 & l1_orders_2(A) ) % 129.18/129.22 => ? [B] : % 129.18/129.22 ( m1_relset_1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v1_relat_1(B) % 129.18/129.22 & v1_funct_1(B) % 129.18/129.22 & ~ v1_xboole_0(B) % 129.18/129.22 & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v1_partfun1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.22 & v6_waybel_1(B,A) % 129.18/129.22 & v7_waybel_1(B,A) ) ) ). % 129.18/129.22 % 129.18/129.22 fof(rc2_yellow_0,axiom, % 129.18/129.22 ? [A] : % 129.18/129.22 ( l1_orders_2(A) % 129.18/129.22 & ~ v3_struct_0(A) % 129.18/129.22 & v2_orders_2(A) % 129.18/129.22 & v3_orders_2(A) % 129.18/129.22 & v4_orders_2(A) % 129.18/129.22 & v1_lattice3(A) % 129.18/129.22 & v2_lattice3(A) % 129.18/129.22 & v3_lattice3(A) % 129.18/129.22 & v1_yellow_0(A) % 129.18/129.22 & v2_yellow_0(A) % 129.18/129.22 & v3_yellow_0(A) ) ). % 129.18/129.22 % 129.18/129.22 fof(rc3_finset_1,axiom, % 129.18/129.22 ! [A] : % 129.18/129.22 ( ~ v1_xboole_0(A) % 129.18/129.22 => ? [B] : % 129.18/129.22 ( m1_subset_1(B,k1_zfmisc_1(A)) % 129.18/129.23 & ~ v1_xboole_0(B) % 129.18/129.23 & v1_finset_1(B) ) ) ). % 129.18/129.23 % 129.18/129.23 fof(rc3_funct_1,axiom, % 129.18/129.23 ? [A] : % 129.18/129.23 ( v1_relat_1(A) % 129.18/129.23 & v1_funct_1(A) % 129.18/129.23 & v2_funct_1(A) ) ). % 129.18/129.23 % 129.18/129.23 fof(rc3_struct_0,axiom, % 129.18/129.23 ? [A] : % 129.18/129.23 ( l1_struct_0(A) % 129.18/129.23 & ~ v3_struct_0(A) ) ). % 129.18/129.23 % 129.18/129.23 fof(rc3_waybel_1,axiom, % 129.18/129.23 ! [A] : % 129.18/129.23 ( ( ~ v3_struct_0(A) % 129.18/129.23 & v2_orders_2(A) % 129.18/129.23 & l1_orders_2(A) ) % 129.18/129.23 => ? [B] : % 129.18/129.23 ( m1_relset_1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.23 & v1_relat_1(B) % 129.18/129.23 & v1_funct_1(B) % 129.18/129.23 & ~ v1_xboole_0(B) % 129.18/129.23 & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.23 & v1_partfun1(B,u1_struct_0(A),u1_struct_0(A)) % 129.18/129.23 & v6_waybel_1(B,A) % 129.18/129.23 & v8_waybel_1(B,A) ) ) ). % 129.18/129.23 % 129.18/129.23 fof(rc3_yellow_9,axiom, % 129.18/129.23 ! [A,B] : % 129.18/129.23 ( ( ~ v3_struct_0(A) % 129.18/129.23 & l1_orders_2(A) % 129.18/129.23 & ~ v3_struct_0(B) % 129.18/129.23 & v2_orders_2(B) % 129.18/129.23 & v4_orders_2(B) % 129.18/129.23 & v2_yellow_0(B) % 129.18/129.23 & l1_orders_2(B) ) % 129.18/129.23 => ? [C] : % 129.18/129.23 ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.23 & v1_relat_1(C) % 129.18/129.23 & v1_funct_1(C) % 129.18/129.23 & ~ v1_xboole_0(C) % 129.18/129.23 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.23 & v17_waybel_0(C,A,B) % 129.18/129.23 & v19_waybel_0(C,A,B) % 129.18/129.23 & v21_waybel_0(C,A,B) % 129.18/129.23 & v1_partfun1(C,u1_struct_0(A),u1_struct_0(B)) ) ) ). % 129.18/129.23 % 129.18/129.23 fof(rc4_finset_1,axiom, % 129.18/129.23 ! [A] : % 129.18/129.23 ( ~ v1_xboole_0(A) % 129.18/129.23 => ? [B] : % 129.18/129.23 ( m1_subset_1(B,k1_zfmisc_1(A)) % 129.18/129.23 & ~ v1_xboole_0(B) % 129.18/129.23 & v1_finset_1(B) ) ) ). % 129.18/129.23 % 129.18/129.23 fof(rc4_yellow_9,axiom, % 129.18/129.23 ! [A,B] : % 129.18/129.23 ( ( ~ v3_struct_0(A) % 129.18/129.23 & l1_orders_2(A) % 129.18/129.23 & ~ v3_struct_0(B) % 129.18/129.23 & v2_orders_2(B) % 129.18/129.23 & v4_orders_2(B) % 129.18/129.23 & v1_yellow_0(B) % 129.18/129.23 & l1_orders_2(B) ) % 129.18/129.23 => ? [C] : % 129.18/129.23 ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.23 & v1_relat_1(C) % 129.18/129.23 & v1_funct_1(C) % 129.18/129.23 & ~ v1_xboole_0(C) % 129.18/129.23 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.23 & v18_waybel_0(C,A,B) % 129.18/129.23 & v20_waybel_0(C,A,B) % 129.18/129.23 & v22_waybel_0(C,A,B) % 129.18/129.23 & v1_partfun1(C,u1_struct_0(A),u1_struct_0(B)) ) ) ). % 129.18/129.23 % 129.18/129.23 fof(rc5_struct_0,axiom, % 129.18/129.23 ! [A] : % 129.18/129.23 ( ( ~ v3_struct_0(A) % 129.18/129.23 & l1_struct_0(A) ) % 129.18/129.23 => ? [B] : % 129.18/129.23 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 129.18/129.23 & ~ v1_xboole_0(B) ) ) ). % 129.18/129.23 % 129.18/129.23 fof(redefinition_k1_waybel_1,axiom, % 129.18/129.23 ! [A,B,C,D] : % 129.18/129.23 ( ( l1_orders_2(A) % 129.18/129.23 & l1_orders_2(B) % 129.18/129.23 & v1_funct_1(C) % 129.18/129.23 & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.23 & m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) % 129.18/129.23 & v1_funct_1(D) % 129.18/129.23 & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) % 129.18/129.23 & m1_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) % 129.18/129.23 => k1_waybel_1(A,B,C,D) = k4_tarski(C,D) ) ). % 129.18/129.23 % 129.18/129.23 fof(redefinition_m2_relset_1,axiom, % 129.18/129.23 ! [A,B,C] : % 129.18/129.23 ( m2_relset_1(C,A,B) % 129.18/129.23 <=> m1_relset_1(C,A,B) ) ). % 129.18/129.23 % 129.18/129.23 fof(reflexivity_r1_tarski,axiom, % 129.18/129.23 ! [A,B] : r1_tarski(A,A) ). % 129.18/129.23 % 129.18/129.23 fof(t1_subset,axiom, % 129.18/129.23 ! [A,B] : % 129.18/129.23 ( r2_hidden(A,B) % 129.18/129.23 => m1_subset_1(A,B) ) ). % 129.18/129.23 % 129.18/129.23 fof(t2_subset,axiom, % 129.18/129.23 ! [A,B] : % 129.18/129.23 ( m1_subset_1(A,B) % 129.18/129.23 => ( v1_xboole_0(B) % 129.18/129.23 | r2_hidden(A,B) ) ) ). % 129.18/129.23 % 129.18/129.23 fof(t3_subset,axiom, % 129.18/129.23 ! [A,B] : % 129.18/129.23 ( m1_subset_1(A,k1_zfmisc_1(B)) % 129.18/129.23 <=> r1_tarski(A,B) ) ). % 129.18/129.23 % 129.18/129.23 fof(t4_subset,axiom, % 129.18/129.23 ! [A,B,C] : % 129.18/129.23 ( ( r2_hidden(A,B) % 129.18/129.23 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 129.18/129.23 => m1_subset_1(A,C) ) ). % 129.18/129.23 % 129.18/129.23 fof(t5_subset,axiom, % 129.18/129.23 ! [A,B,C] : % 129.18/129.23 ~ ( r2_hidden(A,B) % 129.18/129.23 & m1_subset_1(B,k1_zfmisc_1(C)) % 129.18/129.23 & v1_xboole_0(C) ) ). % 129.18/129.23 % 129.18/129.23 fof(t6_boole,axiom, % 129.18/129.23 ! [A] : % 129.18/129.23 ( v1_xboole_0(A) % 129.18/129.23 => A = k1_xboole_0 ) ). % 129.18/129.23 % 129.18/129.23 fof(t6_waybel34,axiom, % 129.18/129.23 ! [A] : % 129.18/129.23 ( ( ~ v3_struct_0(A) % 129.18/129.23 & l1_orders_2(A) ) % 129.18/129.23 => v3_waybel_1(k1_waybel_1(A,A,k7_grcat_1(A),k7_grcat_1(A)),A,A) ) ). % 129.18/129.23 % 129.18/129.23 fof(t7_boole,axiom, % 129.18/129.23 ! [A,B] : % 129.18/129.23 ~ ( r2_hidden(A,B) % 129.18/129.23 & v1_xboole_0(B) ) ). % 129.18/129.23 % 129.18/129.23 fof(t8_boole,axiom, % 129.18/129.23 ! [A,B] : % 129.18/129.23 ~ ( v1_xboole_0(A) % 129.18/129.23 & A != B % 129.18/129.23 & v1_xboole_0(B) ) ). % 129.18/129.23 % 129.18/129.23 %------------------------------------------------------------------------------ % 129.18/129.23 %------------------------------------------- % 129.18/129.23 % Proof found % 129.18/129.23 % SZS status Theorem for theBenchmark % 129.18/129.23 % SZS output start Proof % 129.18/129.23 %ClaNum:515(EqnAxiom:136) % 129.18/129.23 %VarNum:2488(SingletonVarNum:503) % 129.18/129.23 %MaxLitNum:23 % 129.18/129.23 %MaxfuncDepth:2 % 129.18/129.23 %SharedTerms:63 % 129.18/129.23 %goalClause: 137 139 141 143 145 147 149 450 % 129.18/129.23 %singleGoalClaCount:7 % 129.18/129.23 [137]P1(a1) % 129.18/129.23 [138]P1(a2) % 129.18/129.23 [139]P37(a1) % 129.18/129.23 [140]P37(a2) % 129.18/129.23 [141]P41(a1) % 129.18/129.23 [142]P41(a2) % 129.18/129.23 [143]P2(a1) % 129.18/129.23 [144]P2(a2) % 129.18/129.23 [145]P19(a1) % 129.18/129.23 [146]P19(a2) % 129.18/129.23 [147]P38(a1) % 129.18/129.23 [148]P38(a2) % 129.18/129.23 [149]P3(a1) % 129.18/129.23 [150]P3(a12) % 129.18/129.23 [151]P3(a2) % 129.18/129.23 [152]P20(a21) % 129.18/129.23 [153]P20(a3) % 129.18/129.23 [154]P36(a21) % 129.18/129.23 [155]P36(a3) % 129.18/129.23 [156]P21(a2) % 129.18/129.23 [157]P40(a21) % 129.18/129.23 [158]P40(a3) % 129.18/129.23 [159]P39(a2) % 129.18/129.23 [160]P42(a2) % 129.18/129.23 [161]P45(a21) % 129.18/129.23 [162]P45(a3) % 129.18/129.23 [163]P46(a21) % 129.18/129.23 [164]P46(a3) % 129.18/129.23 [165]P22(a21) % 129.18/129.23 [166]P22(a5) % 129.18/129.23 [167]P4(a22) % 129.18/129.23 [168]P16(a28) % 129.18/129.23 [169]P16(a5) % 129.18/129.23 [170]P16(a13) % 129.18/129.23 [171]P23(a28) % 129.18/129.23 [172]P23(a5) % 129.18/129.23 [173]P23(a13) % 129.18/129.23 [174]P26(a6) % 129.18/129.23 [175]P29(a13) % 129.18/129.23 [176]P5(a23) % 129.18/129.23 [177]P5(a15) % 129.18/129.23 [185]~P43(a2) % 129.18/129.23 [186]~P43(a15) % 129.18/129.23 [187]~P22(a22) % 129.18/129.23 [188]~P22(a3) % 129.18/129.23 [189]~P22(a6) % 129.18/129.23 [179]P6(x1791,x1791) % 129.18/129.23 [178]P4(f29(x1781)) % 129.18/129.23 [180]P7(f24(x1801),x1801) % 129.18/129.23 [190]~P22(f29(x1901)) % 129.18/129.23 [181]E(f32(x1811,x1812),f32(x1812,x1811)) % 129.18/129.23 [182]P4(f32(x1821,x1822)) % 129.18/129.23 [183]P8(f25(x1831,x1832),x1831,x1832) % 129.18/129.23 [184]P9(f26(x1841,x1842),x1841,x1842) % 129.18/129.23 [191]~P22(f32(x1911,x1912)) % 129.18/129.23 [450]~E(f30(a1,a1,f34(a1)),f34(a1))+~E(f36(a1,a1,f34(a1)),f34(a1)) % 129.18/129.23 [192]~P22(x1921)+E(x1921,a21) % 129.18/129.23 [193]~P36(x1931)+P20(x1931) % 129.18/129.23 [194]~P22(x1941)+P20(x1941) % 129.18/129.23 [195]~P40(x1951)+P36(x1951) % 129.18/129.23 [196]~P22(x1961)+P36(x1961) % 129.18/129.23 [197]~P45(x1971)+P40(x1971) % 129.18/129.23 [198]~P22(x1981)+P40(x1981) % 129.18/129.23 [199]~P46(x1991)+P45(x1991) % 129.18/129.23 [200]~P22(x2001)+P45(x2001) % 129.18/129.23 [201]~P22(x2011)+P46(x2011) % 129.18/129.23 [202]~P22(x2021)+P4(x2021) % 129.18/129.23 [203]~P22(x2031)+P16(x2031) % 129.18/129.23 [204]~P3(x2041)+P5(x2041) % 129.18/129.23 [205]P22(x2051)+P4(f14(x2051)) % 129.18/129.23 [206]P22(x2061)+P4(f16(x2061)) % 129.18/129.23 [207]P22(x2071)+P26(f29(x2071)) % 129.18/129.23 [209]~P27(x2091)+P20(f29(x2091)) % 129.18/129.23 [210]~P28(x2101)+P20(f29(x2101)) % 129.18/129.23 [211]~P24(x2111)+P20(f29(x2111)) % 129.18/129.23 [212]~P17(x2121)+P20(f29(x2121)) % 129.18/129.23 [213]~P47(x2131)+P20(f29(x2131)) % 129.18/129.23 [214]~P28(x2141)+P36(f29(x2141)) % 129.18/129.23 [215]~P24(x2151)+P36(f29(x2151)) % 129.18/129.23 [216]~P17(x2161)+P36(f29(x2161)) % 129.18/129.23 [217]~P47(x2171)+P36(f29(x2171)) % 129.18/129.23 [218]~P24(x2181)+P40(f29(x2181)) % 129.18/129.23 [219]~P17(x2191)+P40(f29(x2191)) % 129.18/129.23 [220]~P47(x2201)+P40(f29(x2201)) % 129.18/129.23 [221]~P17(x2211)+P45(f29(x2211)) % 129.18/129.23 [222]~P47(x2221)+P45(f29(x2221)) % 129.18/129.23 [223]~P47(x2231)+P46(f29(x2231)) % 129.18/129.23 [224]~P3(x2241)+P16(f34(x2241)) % 129.18/129.23 [226]~P5(x2261)+P16(f34(x2261)) % 129.18/129.23 [227]~P3(x2271)+P23(f34(x2271)) % 129.18/129.23 [228]~P5(x2281)+P23(f34(x2281)) % 129.18/129.23 [229]~P5(x2291)+P29(f34(x2291)) % 129.18/129.23 [233]P22(x2331)+~P22(f14(x2331)) % 129.18/129.23 [234]P22(x2341)+~P22(f16(x2341)) % 129.18/129.23 [273]P22(x2731)+P7(f14(x2731),f33(x2731)) % 129.18/129.23 [274]P22(x2741)+P7(f16(x2741),f33(x2741)) % 129.18/129.23 [370]~P3(x3701)+P31(f34(x3701),x3701,x3701) % 129.18/129.23 [397]~P3(x3971)+P18(f34(x3971),f37(x3971),f37(x3971)) % 129.18/129.23 [399]~P5(x3991)+P18(f34(x3991),f37(x3991),f37(x3991)) % 129.18/129.23 [400]~P5(x4001)+P9(f34(x4001),f37(x4001),f37(x4001)) % 129.18/129.23 [269]~P22(x2691)+~P12(x2692,x2691) % 129.18/129.23 [300]~P12(x3001,x3002)+P7(x3001,x3002) % 129.18/129.23 [354]~P12(x3542,x3541)+~P12(x3541,x3542) % 129.18/129.23 [320]~P6(x3201,x3202)+P7(x3201,f33(x3202)) % 129.18/129.23 [355]P6(x3551,x3552)+~P7(x3551,f33(x3552)) % 129.18/129.23 [443]~P9(x4431,x4432,x4433)+P8(x4431,x4432,x4433) % 129.18/129.23 [444]~P8(x4441,x4442,x4443)+P9(x4441,x4442,x4443) % 129.18/129.23 [427]P23(x4271)+~P7(x4271,f33(f35(x4272,x4273))) % 129.18/129.23 [445]~P9(x4451,x4452,x4453)+P7(x4451,f33(f35(x4452,x4453))) % 129.18/129.23 [230]~P3(x2301)+~P42(x2301)+P21(x2301) % 129.18/129.23 [231]~P3(x2311)+~P42(x2311)+P39(x2311) % 129.18/129.23 [235]~P3(x2351)+~P43(x2351)+~P2(x2351) % 129.18/129.23 [236]~P3(x2361)+~P43(x2361)+~P19(x2361) % 129.18/129.23 [238]~P3(x2381)+P43(x2381)+P16(f7(x2381)) % 129.18/129.23 [240]~P3(x2401)+P43(x2401)+P23(f7(x2401)) % 129.18/129.23 [241]~P3(x2411)+P43(x2411)+P29(f34(x2411)) % 129.18/129.23 [247]~P3(x2471)+P43(x2471)+~P22(f34(x2471)) % 129.18/129.23 [248]~P3(x2481)+P43(x2481)+~P22(f7(x2481)) % 129.18/129.23 [249]~P5(x2491)+P43(x2491)+~P22(f37(x2491)) % 129.18/129.23 [250]~P5(x2501)+P43(x2501)+~P22(f19(x2501)) % 129.18/129.23 [275]~P3(x2751)+P43(x2751)+P49(f34(x2751),x2751) % 129.18/129.23 [276]~P3(x2761)+P43(x2761)+P49(f7(x2761),x2761) % 129.18/129.23 [372]~P3(x3721)+P43(x3721)+P50(f34(x3721),x3721,x3721) % 129.18/129.23 [401]~P3(x4011)+P43(x4011)+P8(f7(x4011),f37(x4011),f37(x4011)) % 129.18/129.23 [403]~P3(x4031)+P43(x4031)+P18(f7(x4031),f37(x4031),f37(x4031)) % 129.18/129.23 [404]~P3(x4041)+P43(x4041)+P25(f34(x4041),f37(x4041),f37(x4041)) % 129.18/129.23 [405]~P3(x4051)+P43(x4051)+P25(f7(x4051),f37(x4051),f37(x4051)) % 129.18/129.23 [356]~P5(x3561)+P43(x3561)+P7(f19(x3561),f33(f37(x3561))) % 129.18/129.23 [509]~P3(x5091)+P43(x5091)+P44(f31(x5091,x5091,f34(x5091),f34(x5091)),x5091,x5091) % 129.18/129.23 [208]~P22(x2082)+~P22(x2081)+E(x2081,x2082) % 129.18/129.23 [278]~P7(x2781,x2782)+P27(x2781)+~P20(x2782) % 129.18/129.23 [279]~P7(x2791,x2792)+P27(x2791)+~P36(x2792) % 129.18/129.23 [280]~P7(x2801,x2802)+P27(x2801)+~P40(x2802) % 129.18/129.23 [281]~P7(x2811,x2812)+P27(x2811)+~P45(x2812) % 129.18/129.23 [282]~P7(x2821,x2822)+P27(x2821)+~P46(x2822) % 129.18/129.23 [283]~P7(x2831,x2832)+P28(x2831)+~P36(x2832) % 129.18/129.23 [284]~P7(x2841,x2842)+P28(x2841)+~P40(x2842) % 129.18/129.23 [285]~P7(x2851,x2852)+P28(x2851)+~P45(x2852) % 129.18/129.23 [286]~P7(x2861,x2862)+P28(x2861)+~P46(x2862) % 129.18/129.23 [287]~P7(x2871,x2872)+P24(x2871)+~P40(x2872) % 129.18/129.23 [288]~P7(x2881,x2882)+P24(x2881)+~P45(x2882) % 129.18/129.23 [289]~P7(x2891,x2892)+P24(x2891)+~P46(x2892) % 129.18/129.23 [290]~P7(x2901,x2902)+P17(x2901)+~P45(x2902) % 129.18/129.23 [291]~P7(x2911,x2912)+P17(x2911)+~P46(x2912) % 129.18/129.23 [292]~P7(x2921,x2922)+P47(x2921)+~P46(x2922) % 129.18/129.23 [319]~P7(x3192,x3191)+P22(x3191)+P12(x3192,x3191) % 129.18/129.23 [317]P22(x3171)+P22(x3172)+P26(f32(x3172,x3171)) % 129.18/129.23 [321]P20(x3211)+~P20(x3212)+~P7(x3211,f33(x3212)) % 129.18/129.23 [322]P20(x3221)+~P36(x3222)+~P7(x3221,f33(x3222)) % 129.18/129.23 [323]P20(x3231)+~P40(x3232)+~P7(x3231,f33(x3232)) % 129.18/129.23 [324]P20(x3241)+~P45(x3242)+~P7(x3241,f33(x3242)) % 129.18/129.23 [325]P20(x3251)+~P46(x3252)+~P7(x3251,f33(x3252)) % 129.18/129.23 [326]P36(x3261)+~P36(x3262)+~P7(x3261,f33(x3262)) % 129.18/129.23 [327]P36(x3271)+~P40(x3272)+~P7(x3271,f33(x3272)) % 129.18/129.23 [328]P36(x3281)+~P45(x3282)+~P7(x3281,f33(x3282)) % 129.18/129.23 [329]P36(x3291)+~P46(x3292)+~P7(x3291,f33(x3292)) % 129.18/129.23 [330]P40(x3301)+~P40(x3302)+~P7(x3301,f33(x3302)) % 129.18/129.23 [331]P40(x3311)+~P45(x3312)+~P7(x3311,f33(x3312)) % 129.18/129.23 [332]P40(x3321)+~P46(x3322)+~P7(x3321,f33(x3322)) % 129.18/129.23 [333]P45(x3331)+~P45(x3332)+~P7(x3331,f33(x3332)) % 129.18/129.23 [334]P45(x3341)+~P46(x3342)+~P7(x3341,f33(x3342)) % 129.18/129.23 [335]P46(x3351)+~P46(x3352)+~P7(x3351,f33(x3352)) % 129.18/129.23 [336]P4(x3361)+~P4(x3362)+~P7(x3361,f33(x3362)) % 129.18/129.23 [337]~P27(x3372)+~P27(x3371)+P20(f32(x3371,x3372)) % 129.18/129.23 [338]~P28(x3382)+~P28(x3381)+P20(f32(x3381,x3382)) % 129.18/129.23 [339]~P24(x3392)+~P24(x3391)+P20(f32(x3391,x3392)) % 129.18/129.23 [340]~P17(x3402)+~P17(x3401)+P20(f32(x3401,x3402)) % 129.18/129.23 [341]~P47(x3412)+~P47(x3411)+P20(f32(x3411,x3412)) % 129.18/129.23 [342]~P28(x3422)+~P28(x3421)+P36(f32(x3421,x3422)) % 129.18/129.23 [343]~P24(x3432)+~P24(x3431)+P36(f32(x3431,x3432)) % 129.18/129.23 [344]~P17(x3442)+~P17(x3441)+P36(f32(x3441,x3442)) % 129.18/129.23 [345]~P47(x3452)+~P47(x3451)+P36(f32(x3451,x3452)) % 129.18/129.23 [346]~P24(x3462)+~P24(x3461)+P40(f32(x3461,x3462)) % 129.18/129.23 [347]~P17(x3472)+~P17(x3471)+P40(f32(x3471,x3472)) % 129.18/129.23 [348]~P47(x3482)+~P47(x3481)+P40(f32(x3481,x3482)) % 129.18/129.23 [349]~P17(x3492)+~P17(x3491)+P45(f32(x3491,x3492)) % 129.18/129.23 [350]~P47(x3502)+~P47(x3501)+P45(f32(x3501,x3502)) % 129.18/129.23 [351]~P47(x3512)+~P47(x3511)+P46(f32(x3511,x3512)) % 129.18/129.23 [352]~P4(x3522)+~P4(x3521)+P4(f35(x3521,x3522)) % 129.18/129.23 [423]~P3(x4232)+~P3(x4231)+P10(f27(x4231,x4232),x4231,x4232) % 129.18/129.23 [369]~P22(x3691)+~P12(x3692,x3693)+~P7(x3693,f33(x3691)) % 129.18/129.23 [371]P7(x3711,x3712)+~P12(x3711,x3713)+~P7(x3713,f33(x3712)) % 129.18/129.23 [242]P43(x2421)+~P38(x2421)+~P3(x2421)+P2(x2421) % 129.18/129.23 [243]P43(x2431)+~P38(x2431)+~P3(x2431)+P19(x2431) % 129.18/129.23 [244]P42(x2441)+~P38(x2441)+~P3(x2441)+P43(x2441) % 129.18/129.23 [245]~P3(x2451)+~P21(x2451)+~P39(x2451)+P42(x2451) % 129.18/129.23 [246]~P22(x2461)+~P16(x2461)+~P23(x2461)+P29(x2461) % 129.18/129.23 [254]~P1(x2541)+~P3(x2541)+P43(x2541)+P16(f10(x2541)) % 129.18/129.23 [255]~P1(x2551)+~P3(x2551)+P43(x2551)+P16(f11(x2551)) % 129.18/129.23 [256]~P1(x2561)+~P3(x2561)+P43(x2561)+P16(f17(x2561)) % 129.18/129.23 [260]~P1(x2601)+~P3(x2601)+P43(x2601)+P23(f10(x2601)) % 129.18/129.23 [261]~P1(x2611)+~P3(x2611)+P43(x2611)+P23(f11(x2611)) % 129.18/129.23 [262]~P1(x2621)+~P3(x2621)+P43(x2621)+P23(f17(x2621)) % 129.18/129.23 [263]~P1(x2631)+~P3(x2631)+P43(x2631)+P11(f34(x2631)) % 129.18/129.23 [264]~P1(x2641)+~P3(x2641)+P43(x2641)+P11(f10(x2641)) % 129.18/129.23 [268]~P1(x2681)+~P3(x2681)+P43(x2681)+P29(f10(x2681)) % 129.18/129.23 [296]~P1(x2961)+~P3(x2961)+P43(x2961)+~P22(f10(x2961)) % 129.18/129.23 [297]~P1(x2971)+~P3(x2971)+P43(x2971)+~P22(f11(x2971)) % 129.18/129.23 [298]~P1(x2981)+~P3(x2981)+P43(x2981)+~P22(f17(x2981)) % 129.18/129.23 [305]~P1(x3051)+~P3(x3051)+P43(x3051)+P49(f10(x3051),x3051) % 129.18/129.23 [306]~P1(x3061)+~P3(x3061)+P43(x3061)+P49(f11(x3061),x3061) % 129.18/129.23 [307]~P1(x3071)+~P3(x3071)+P43(x3071)+P49(f17(x3071),x3071) % 129.18/129.23 [310]~P1(x3101)+~P3(x3101)+P43(x3101)+P52(f34(x3101),x3101) % 129.18/129.23 [311]~P1(x3111)+~P3(x3111)+P43(x3111)+P52(f10(x3111),x3111) % 129.18/129.23 [312]~P1(x3121)+~P3(x3121)+P43(x3121)+P52(f11(x3121),x3121) % 129.18/129.23 [314]~P1(x3141)+~P3(x3141)+P43(x3141)+P53(f34(x3141),x3141) % 129.18/129.23 [315]~P1(x3151)+~P3(x3151)+P43(x3151)+P53(f10(x3151),x3151) % 129.18/129.23 [316]~P1(x3161)+~P3(x3161)+P43(x3161)+P53(f17(x3161),x3161) % 129.18/129.23 [381]~P1(x3811)+~P3(x3811)+P43(x3811)+P50(f10(x3811),x3811,x3811) % 129.18/129.23 [382]~P1(x3821)+~P3(x3821)+P43(x3821)+P32(f34(x3821),x3821,x3821) % 129.18/129.23 [383]~P1(x3831)+~P3(x3831)+P43(x3831)+P32(f10(x3831),x3831,x3831) % 129.18/129.23 [384]~P1(x3841)+~P3(x3841)+P43(x3841)+P13(f34(x3841),x3841,x3841) % 129.18/129.23 [385]~P1(x3851)+~P3(x3851)+P43(x3851)+P13(f10(x3851),x3851,x3851) % 129.18/129.23 [386]~P1(x3861)+~P3(x3861)+P43(x3861)+P14(f34(x3861),x3861,x3861) % 129.18/129.23 [387]~P1(x3871)+~P3(x3871)+P43(x3871)+P14(f10(x3871),x3871,x3871) % 129.18/129.23 [388]~P1(x3881)+~P3(x3881)+P43(x3881)+P33(f34(x3881),x3881,x3881) % 129.18/129.23 [389]~P1(x3891)+~P3(x3891)+P43(x3891)+P33(f10(x3891),x3891,x3891) % 129.18/129.23 [390]~P1(x3901)+~P3(x3901)+P43(x3901)+P15(f34(x3901),x3901,x3901) % 129.18/129.23 [391]~P1(x3911)+~P3(x3911)+P43(x3911)+P15(f10(x3911),x3911,x3911) % 129.18/129.23 [392]~P1(x3921)+~P3(x3921)+P43(x3921)+P34(f34(x3921),x3921,x3921) % 129.18/129.23 [393]~P1(x3931)+~P3(x3931)+P43(x3931)+P34(f10(x3931),x3931,x3931) % 129.18/129.23 [406]~P1(x4061)+~P3(x4061)+P43(x4061)+P8(f10(x4061),f37(x4061),f37(x4061)) % 129.18/129.23 [407]~P1(x4071)+~P3(x4071)+P43(x4071)+P8(f11(x4071),f37(x4071),f37(x4071)) % 129.18/129.23 [408]~P1(x4081)+~P3(x4081)+P43(x4081)+P8(f17(x4081),f37(x4081),f37(x4081)) % 129.18/129.23 [412]~P1(x4121)+~P3(x4121)+P43(x4121)+P18(f10(x4121),f37(x4121),f37(x4121)) % 129.18/129.23 [413]~P1(x4131)+~P3(x4131)+P43(x4131)+P18(f11(x4131),f37(x4131),f37(x4131)) % 129.18/129.23 [414]~P1(x4141)+~P3(x4141)+P43(x4141)+P18(f17(x4141),f37(x4141),f37(x4141)) % 129.18/129.23 [418]~P1(x4181)+~P3(x4181)+P43(x4181)+P25(f10(x4181),f37(x4181),f37(x4181)) % 129.18/129.23 [419]~P1(x4191)+~P3(x4191)+P43(x4191)+P25(f11(x4191),f37(x4191),f37(x4191)) % 129.18/129.23 [420]~P1(x4201)+~P3(x4201)+P43(x4201)+P25(f17(x4201),f37(x4201),f37(x4201)) % 129.18/129.23 [318]~P26(x3181)+~P7(x3182,x3181)+P22(x3181)+~P22(x3182) % 129.18/129.23 [270]P30(x2701)+~P1(x2701)+~P38(x2701)+~P3(x2701)+P43(x2701) % 129.18/129.23 [271]P35(x2711)+~P1(x2711)+~P38(x2711)+~P3(x2711)+P43(x2711) % 129.18/129.23 [272]P21(x2721)+~P1(x2721)+~P3(x2721)+~P35(x2721)+P43(x2721) % 129.18/129.23 [277]~P1(x2771)+~P2(x2771)+~P3(x2771)+~P30(x2771)+P39(x2771) % 129.18/129.23 [357]~P1(x3571)+~P3(x3571)+~P3(x3572)+P43(x3571)+P16(f8(x3572,x3571)) % 129.18/129.23 [358]~P1(x3581)+~P3(x3581)+~P3(x3582)+P43(x3581)+P23(f8(x3582,x3581)) % 129.18/129.23 [424]~P1(x4241)+~P3(x4241)+~P3(x4242)+P43(x4241)+P50(f8(x4242,x4241),x4242,x4241) % 129.18/129.23 [428]~P1(x4281)+~P3(x4281)+~P3(x4282)+P43(x4281)+P8(f8(x4282,x4281),f37(x4282),f37(x4281)) % 129.18/129.23 [429]~P1(x4291)+~P3(x4291)+~P3(x4292)+P43(x4291)+P18(f8(x4292,x4291),f37(x4292),f37(x4291)) % 129.18/129.23 [430]~P1(x4301)+~P3(x4301)+~P3(x4302)+P43(x4301)+P25(f8(x4302,x4301),f37(x4302),f37(x4301)) % 129.18/129.23 [301]P43(x3011)+~P1(x3011)+~P41(x3011)+~P3(x3011)+~P35(x3011)+P19(x3011) % 129.18/129.23 [353]P43(x3531)+~P1(x3531)+~P41(x3531)+~P3(x3531)+~P35(x3531)+~P39(x3531)+P2(x3531) % 129.18/129.23 [453]~P3(x4531)+~P16(x4532)+~P49(x4532,x4531)+P43(x4531)+P11(x4532)+~P8(x4532,f37(x4531),f37(x4531))+~P18(x4532,f37(x4531),f37(x4531)) % 129.18/129.23 [454]~P3(x4541)+~P16(x4542)+~P49(x4542,x4541)+P43(x4541)+~P22(x4542)+~P8(x4542,f37(x4541),f37(x4541))+~P18(x4542,f37(x4541),f37(x4541)) % 129.18/129.23 [455]~P3(x4551)+~P16(x4552)+~P52(x4552,x4551)+P43(x4551)+~P22(x4552)+~P8(x4552,f37(x4551),f37(x4551))+~P18(x4552,f37(x4551),f37(x4551)) % 129.18/129.23 [456]~P3(x4561)+~P16(x4562)+~P53(x4562,x4561)+P43(x4561)+~P22(x4562)+~P8(x4562,f37(x4561),f37(x4561))+~P18(x4562,f37(x4561),f37(x4561)) % 129.18/129.23 [457]~P3(x4571)+~P16(x4572)+~P52(x4572,x4571)+P43(x4571)+P49(x4572,x4571)+~P8(x4572,f37(x4571),f37(x4571))+~P18(x4572,f37(x4571),f37(x4571)) % 129.18/129.23 [458]~P3(x4581)+~P16(x4582)+~P53(x4582,x4581)+P43(x4581)+P49(x4582,x4581)+~P8(x4582,f37(x4581),f37(x4581))+~P18(x4582,f37(x4581),f37(x4581)) % 129.18/129.23 [459]~P3(x4591)+~P16(x4592)+~P49(x4592,x4591)+P50(x4592,x4591,x4591)+P43(x4591)+~P8(x4592,f37(x4591),f37(x4591))+~P18(x4592,f37(x4591),f37(x4591)) % 129.18/129.23 [460]~P3(x4601)+~P16(x4602)+~P49(x4602,x4601)+P43(x4601)+~P8(x4602,f37(x4601),f37(x4601))+~P18(x4602,f37(x4601),f37(x4601))+P25(x4602,f37(x4601),f37(x4601)) % 129.18/129.23 [461]~P3(x4611)+~P16(x4612)+~P52(x4612,x4611)+P43(x4611)+~P8(x4612,f37(x4611),f37(x4611))+~P18(x4612,f37(x4611),f37(x4611))+P25(x4612,f37(x4611),f37(x4611)) % 129.18/129.23 [462]~P3(x4621)+~P16(x4622)+~P53(x4622,x4621)+P43(x4621)+~P8(x4622,f37(x4621),f37(x4621))+~P18(x4622,f37(x4621),f37(x4621))+P25(x4622,f37(x4621),f37(x4621)) % 129.18/129.23 [374]~P1(x3741)+~P41(x3741)+~P3(x3741)+~P3(x3742)+~P39(x3741)+P43(x3741)+P43(x3742)+P16(f18(x3742,x3741)) % 129.18/129.23 [375]~P1(x3751)+~P41(x3751)+~P3(x3751)+~P3(x3752)+~P21(x3751)+P43(x3751)+P43(x3752)+P16(f20(x3752,x3751)) % 129.18/129.23 [376]~P1(x3761)+~P41(x3761)+~P3(x3761)+~P3(x3762)+~P39(x3761)+P43(x3761)+P43(x3762)+P23(f18(x3762,x3761)) % 129.18/129.23 [377]~P1(x3771)+~P41(x3771)+~P3(x3771)+~P3(x3772)+~P21(x3771)+P43(x3771)+P43(x3772)+P23(f20(x3772,x3771)) % 129.18/129.23 [421]~P1(x4211)+~P41(x4211)+~P3(x4211)+~P3(x4212)+~P21(x4211)+P43(x4211)+P43(x4212)+~P22(f20(x4212,x4211)) % 129.18/129.23 [422]~P1(x4221)+~P41(x4221)+~P3(x4221)+~P3(x4222)+~P39(x4221)+P43(x4221)+P43(x4222)+~P22(f18(x4222,x4221)) % 129.18/129.23 [431]~P1(x4311)+~P41(x4311)+~P3(x4311)+~P3(x4312)+~P21(x4311)+P43(x4311)+P43(x4312)+P32(f20(x4312,x4311),x4312,x4311) % 129.18/129.23 [432]~P1(x4321)+~P41(x4321)+~P3(x4321)+~P3(x4322)+~P39(x4321)+P43(x4321)+P43(x4322)+P13(f18(x4322,x4321),x4322,x4321) % 129.18/129.23 [433]~P1(x4331)+~P41(x4331)+~P3(x4331)+~P3(x4332)+~P39(x4331)+P43(x4331)+P43(x4332)+P14(f18(x4332,x4331),x4332,x4331) % 129.18/129.23 [434]~P1(x4341)+~P41(x4341)+~P3(x4341)+~P3(x4342)+~P39(x4341)+P43(x4341)+P43(x4342)+P33(f18(x4342,x4341),x4342,x4341) % 129.18/129.23 [435]~P1(x4351)+~P41(x4351)+~P3(x4351)+~P3(x4352)+~P21(x4351)+P43(x4351)+P43(x4352)+P15(f20(x4352,x4351),x4352,x4351) % 129.18/129.23 [436]~P1(x4361)+~P41(x4361)+~P3(x4361)+~P3(x4362)+~P21(x4361)+P43(x4361)+P43(x4362)+P34(f20(x4362,x4361),x4362,x4361) % 129.18/129.23 [437]~P1(x4371)+~P41(x4371)+~P3(x4371)+~P3(x4372)+~P39(x4371)+P43(x4371)+P43(x4372)+P8(f18(x4372,x4371),f37(x4372),f37(x4371)) % 129.18/129.23 [438]~P1(x4381)+~P41(x4381)+~P3(x4381)+~P3(x4382)+~P21(x4381)+P43(x4381)+P43(x4382)+P8(f20(x4382,x4381),f37(x4382),f37(x4381)) % 129.18/129.23 [439]~P1(x4391)+~P41(x4391)+~P3(x4391)+~P3(x4392)+~P39(x4391)+P43(x4391)+P43(x4392)+P18(f18(x4392,x4391),f37(x4392),f37(x4391)) % 129.18/129.23 [440]~P1(x4401)+~P41(x4401)+~P3(x4401)+~P3(x4402)+~P21(x4401)+P43(x4401)+P43(x4402)+P18(f20(x4402,x4401),f37(x4402),f37(x4401)) % 129.18/129.23 [441]~P1(x4411)+~P41(x4411)+~P3(x4411)+~P3(x4412)+~P39(x4411)+P43(x4411)+P43(x4412)+P25(f18(x4412,x4411),f37(x4412),f37(x4411)) % 129.18/129.23 [442]~P1(x4421)+~P41(x4421)+~P3(x4421)+~P3(x4422)+~P21(x4421)+P43(x4421)+P43(x4422)+P25(f20(x4422,x4421),f37(x4422),f37(x4421)) % 129.18/129.23 [361]P43(x3611)+~P1(x3611)+~P37(x3611)+~P41(x3611)+~P2(x3611)+~P3(x3611)+~P30(x3611)+~P21(x3611)+P19(x3611) % 129.18/129.23 [363]P43(x3631)+~P1(x3631)+~P37(x3631)+~P41(x3631)+~P2(x3631)+~P3(x3631)+~P30(x3631)+~P21(x3631)+P38(x3631) % 129.18/129.23 [364]P43(x3641)+~P1(x3641)+~P37(x3641)+~P41(x3641)+~P3(x3641)+~P30(x3641)+~P35(x3641)+~P39(x3641)+P38(x3641) % 129.18/129.23 [367]P42(x3671)+~P1(x3671)+~P37(x3671)+~P41(x3671)+~P2(x3671)+~P3(x3671)+~P30(x3671)+~P21(x3671)+P43(x3671) % 129.18/129.23 [368]P42(x3681)+~P1(x3681)+~P37(x3681)+~P41(x3681)+~P3(x3681)+~P30(x3681)+~P35(x3681)+~P39(x3681)+P43(x3681) % 129.18/129.23 [463]~P3(x4631)+~P3(x4632)+~P16(x4633)+~P31(x4633,x4632,x4631)+P43(x4631)+P43(x4632)+P29(x4633)+~P8(x4633,f37(x4632),f37(x4631))+~P18(x4633,f37(x4632),f37(x4631)) % 129.18/129.23 [467]~P3(x4671)+~P3(x4672)+~P16(x4673)+~P31(x4673,x4672,x4671)+P43(x4671)+P50(x4673,x4672,x4671)+P43(x4672)+~P8(x4673,f37(x4672),f37(x4671))+~P18(x4673,f37(x4672),f37(x4671)) % 129.18/129.23 [468]~P3(x4681)+~P3(x4682)+~P16(x4683)+~P15(x4683,x4682,x4681)+P43(x4681)+P32(x4683,x4682,x4681)+P43(x4682)+~P8(x4683,f37(x4682),f37(x4681))+~P18(x4683,f37(x4682),f37(x4681)) % 129.18/129.23 [469]~P3(x4691)+~P3(x4692)+~P16(x4693)+~P14(x4693,x4692,x4691)+P43(x4691)+P13(x4693,x4692,x4691)+P43(x4692)+~P8(x4693,f37(x4692),f37(x4691))+~P18(x4693,f37(x4692),f37(x4691)) % 129.18/129.23 [470]~P3(x4701)+~P3(x4702)+~P16(x4703)+~P14(x4703,x4702,x4701)+P43(x4701)+P33(x4703,x4702,x4701)+P43(x4702)+~P8(x4703,f37(x4702),f37(x4701))+~P18(x4703,f37(x4702),f37(x4701)) % 129.18/129.23 [471]~P3(x4711)+~P3(x4712)+~P16(x4713)+~P15(x4713,x4712,x4711)+P43(x4711)+P34(x4713,x4712,x4711)+P43(x4712)+~P8(x4713,f37(x4712),f37(x4711))+~P18(x4713,f37(x4712),f37(x4711)) % 129.18/129.23 [511]~P3(x5112)+~P3(x5111)+~P16(x5114)+~P16(x5113)+~P8(x5114,f37(x5112),f37(x5111))+~P8(x5113,f37(x5111),f37(x5112))+~P18(x5114,f37(x5112),f37(x5111))+~P18(x5113,f37(x5111),f37(x5112))+P10(f31(x5111,x5112,x5113,x5114),x5111,x5112) % 129.18/129.23 [510]~P3(x5102)+~P3(x5101)+~P16(x5104)+~P16(x5103)+~P8(x5104,f37(x5102),f37(x5101))+~P8(x5103,f37(x5101),f37(x5102))+~P18(x5104,f37(x5102),f37(x5101))+~P18(x5103,f37(x5101),f37(x5102))+E(f31(x5101,x5102,x5103,x5104),f32(f32(x5103,x5104),f29(x5103))) % 129.18/129.23 [425]~P1(x4252)+~P1(x4251)+~P37(x4252)+~P37(x4251)+~P41(x4252)+~P41(x4251)+~P2(x4252)+~P2(x4251)+~P19(x4252)+~P19(x4251)+~P3(x4252)+~P3(x4251)+P16(f4(x4251,x4252)) % 129.18/129.23 [426]~P1(x4262)+~P1(x4261)+~P37(x4262)+~P37(x4261)+~P41(x4262)+~P41(x4261)+~P2(x4262)+~P2(x4261)+~P19(x4262)+~P19(x4261)+~P3(x4262)+~P3(x4261)+P23(f4(x4261,x4262)) % 129.18/129.23 [446]~P1(x4462)+~P1(x4461)+~P37(x4462)+~P37(x4461)+~P41(x4462)+~P41(x4461)+~P2(x4462)+~P2(x4461)+~P19(x4462)+~P19(x4461)+~P3(x4462)+~P3(x4461)+P13(f4(x4461,x4462),x4461,x4462) % 129.18/129.23 [447]~P1(x4472)+~P1(x4471)+~P37(x4472)+~P37(x4471)+~P41(x4472)+~P41(x4471)+~P2(x4472)+~P2(x4471)+~P19(x4472)+~P19(x4471)+~P3(x4472)+~P3(x4471)+P34(f4(x4471,x4472),x4471,x4472) % 129.18/129.23 [448]~P1(x4482)+~P1(x4481)+~P37(x4482)+~P37(x4481)+~P41(x4482)+~P41(x4481)+~P2(x4482)+~P2(x4481)+~P19(x4482)+~P19(x4481)+~P3(x4482)+~P3(x4481)+P8(f4(x4481,x4482),f37(x4481),f37(x4482)) % 129.18/129.23 [449]~P1(x4492)+~P1(x4491)+~P37(x4492)+~P37(x4491)+~P41(x4492)+~P41(x4491)+~P2(x4492)+~P2(x4491)+~P19(x4492)+~P19(x4491)+~P3(x4492)+~P3(x4491)+P18(f4(x4491,x4492),f37(x4491),f37(x4492)) % 129.18/129.23 [464]~P1(x4641)+~P1(x4642)+~P41(x4641)+~P41(x4642)+~P3(x4641)+~P3(x4642)+~P16(x4643)+~P32(x4643,x4642,x4641)+P43(x4641)+P43(x4642)+~P22(x4643)+~P8(x4643,f37(x4642),f37(x4641))+~P18(x4643,f37(x4642),f37(x4641)) % 129.18/129.23 [472]~P1(x4721)+~P1(x4722)+~P41(x4721)+~P41(x4722)+~P3(x4721)+~P3(x4722)+~P16(x4723)+~P32(x4723,x4722,x4721)+P43(x4721)+P50(x4723,x4722,x4721)+P43(x4722)+~P8(x4723,f37(x4722),f37(x4721))+~P18(x4723,f37(x4722),f37(x4721)) % 129.18/129.23 [475]~P1(x4751)+~P1(x4752)+~P41(x4751)+~P41(x4752)+~P3(x4751)+~P3(x4752)+~P16(x4753)+~P32(x4753,x4752,x4751)+P43(x4751)+P43(x4752)+~P8(x4753,f37(x4752),f37(x4751))+~P18(x4753,f37(x4752),f37(x4751))+P25(x4753,f37(x4752),f37(x4751)) % 129.18/129.23 [451]~P1(x4512)+~P1(x4511)+~P37(x4512)+~P37(x4511)+~P41(x4512)+~P41(x4511)+~P2(x4512)+~P2(x4511)+~P19(x4512)+~P19(x4511)+~P38(x4512)+~P38(x4511)+~P3(x4512)+~P3(x4511)+P44(f9(x4511,x4512),x4511,x4512) % 129.18/129.23 [452]~P1(x4522)+~P1(x4521)+~P37(x4522)+~P37(x4521)+~P41(x4522)+~P41(x4521)+~P2(x4522)+~P2(x4521)+~P19(x4522)+~P19(x4521)+~P38(x4522)+~P38(x4521)+~P3(x4522)+~P3(x4521)+P10(f9(x4521,x4522),x4521,x4522) % 129.18/129.23 [465]~P1(x4651)+~P1(x4652)+~P37(x4651)+~P37(x4652)+~P41(x4651)+~P41(x4652)+~P3(x4651)+~P3(x4652)+~P16(x4653)+~P48(x4653,x4652,x4651)+P43(x4651)+P43(x4652)+~P22(x4653)+~P8(x4653,f37(x4652),f37(x4651))+~P18(x4653,f37(x4652),f37(x4651)) % 129.18/129.23 [466]~P1(x4661)+~P1(x4662)+~P37(x4661)+~P37(x4662)+~P41(x4661)+~P41(x4662)+~P3(x4661)+~P3(x4662)+~P16(x4663)+~P51(x4663,x4661,x4662)+P43(x4661)+P43(x4662)+~P22(x4663)+~P8(x4663,f37(x4662),f37(x4661))+~P18(x4663,f37(x4662),f37(x4661)) % 129.18/129.23 [476]~P1(x4761)+~P1(x4762)+~P37(x4761)+~P37(x4762)+~P41(x4761)+~P41(x4762)+~P3(x4761)+~P3(x4762)+~P16(x4763)+~P51(x4763,x4761,x4762)+P43(x4761)+P32(x4763,x4762,x4761)+P43(x4762)+~P8(x4763,f37(x4762),f37(x4761))+~P18(x4763,f37(x4762),f37(x4761)) % 129.18/129.23 [477]~P1(x4771)+~P1(x4772)+~P37(x4771)+~P37(x4772)+~P41(x4771)+~P41(x4772)+~P3(x4771)+~P3(x4772)+~P16(x4773)+~P48(x4773,x4772,x4771)+P43(x4771)+P13(x4773,x4772,x4771)+P43(x4772)+~P8(x4773,f37(x4772),f37(x4771))+~P18(x4773,f37(x4772),f37(x4771)) % 129.18/129.23 [478]~P1(x4781)+~P1(x4782)+~P37(x4781)+~P37(x4782)+~P41(x4781)+~P41(x4782)+~P3(x4781)+~P3(x4782)+~P16(x4783)+~P48(x4783,x4782,x4781)+P43(x4781)+P14(x4783,x4782,x4781)+P43(x4782)+~P8(x4783,f37(x4782),f37(x4781))+~P18(x4783,f37(x4782),f37(x4781)) % 129.18/129.23 [479]~P1(x4791)+~P1(x4792)+~P37(x4791)+~P37(x4792)+~P41(x4791)+~P41(x4792)+~P3(x4791)+~P3(x4792)+~P16(x4793)+~P48(x4793,x4792,x4791)+P43(x4791)+P33(x4793,x4792,x4791)+P43(x4792)+~P8(x4793,f37(x4792),f37(x4791))+~P18(x4793,f37(x4792),f37(x4791)) % 129.18/129.23 [480]~P1(x4801)+~P1(x4802)+~P37(x4801)+~P37(x4802)+~P41(x4801)+~P41(x4802)+~P3(x4801)+~P3(x4802)+~P16(x4803)+~P51(x4803,x4801,x4802)+P43(x4801)+P15(x4803,x4802,x4801)+P43(x4802)+~P8(x4803,f37(x4802),f37(x4801))+~P18(x4803,f37(x4802),f37(x4801)) % 129.18/129.23 [481]~P1(x4811)+~P1(x4812)+~P37(x4811)+~P37(x4812)+~P41(x4811)+~P41(x4812)+~P3(x4811)+~P3(x4812)+~P16(x4813)+~P51(x4813,x4811,x4812)+P43(x4811)+P34(x4813,x4812,x4811)+P43(x4812)+~P8(x4813,f37(x4812),f37(x4811))+~P18(x4813,f37(x4812),f37(x4811)) % 129.18/129.23 [482]~P1(x4823)+~P1(x4822)+~P37(x4823)+~P37(x4822)+~P41(x4823)+~P41(x4822)+~P19(x4823)+~P19(x4822)+~P3(x4823)+~P3(x4822)+~P16(x4821)+~P13(x4821,x4822,x4823)+P50(x4821,x4822,x4823)+~P8(x4821,f37(x4822),f37(x4823))+~P18(x4821,f37(x4822),f37(x4823)) % 129.18/129.23 [483]~P1(x4831)+~P1(x4832)+~P37(x4831)+~P37(x4832)+~P41(x4831)+~P41(x4832)+~P3(x4831)+~P3(x4832)+~P16(x4833)+~P48(x4833,x4832,x4831)+P43(x4831)+P43(x4832)+~P8(x4833,f37(x4832),f37(x4831))+~P18(x4833,f37(x4832),f37(x4831))+P25(x4833,f37(x4832),f37(x4831)) % 129.18/129.23 [484]~P1(x4841)+~P1(x4842)+~P37(x4841)+~P37(x4842)+~P41(x4841)+~P41(x4842)+~P3(x4841)+~P3(x4842)+~P16(x4843)+~P51(x4843,x4841,x4842)+P43(x4841)+P43(x4842)+~P8(x4843,f37(x4842),f37(x4841))+~P18(x4843,f37(x4842),f37(x4841))+P25(x4843,f37(x4842),f37(x4841)) % 129.18/129.23 [473]~P1(x4732)+~P1(x4731)+~P37(x4732)+~P37(x4731)+~P41(x4732)+~P41(x4731)+~P2(x4732)+~P2(x4731)+~P19(x4732)+~P19(x4731)+~P3(x4732)+~P3(x4731)+~P16(x4733)+~P8(x4733,f37(x4731),f37(x4732))+~P18(x4733,f37(x4731),f37(x4732))+P16(f30(x4731,x4732,x4733)) % 129.18/129.23 [474]~P1(x4742)+~P1(x4741)+~P37(x4742)+~P37(x4741)+~P41(x4742)+~P41(x4741)+~P2(x4742)+~P2(x4741)+~P19(x4742)+~P19(x4741)+~P3(x4742)+~P3(x4741)+~P16(x4743)+~P8(x4743,f37(x4742),f37(x4741))+~P18(x4743,f37(x4742),f37(x4741))+P16(f36(x4741,x4742,x4743)) % 129.18/129.23 [485]~P1(x4852)+~P1(x4851)+~P37(x4852)+~P37(x4851)+~P41(x4852)+~P41(x4851)+~P2(x4852)+~P2(x4851)+~P19(x4852)+~P19(x4851)+~P3(x4852)+~P3(x4851)+~P16(x4853)+~P8(x4853,f37(x4851),f37(x4852))+~P18(x4853,f37(x4851),f37(x4852))+P18(f30(x4851,x4852,x4853),f37(x4852),f37(x4851)) % 129.18/129.23 [486]~P1(x4862)+~P1(x4861)+~P37(x4862)+~P37(x4861)+~P41(x4862)+~P41(x4861)+~P2(x4862)+~P2(x4861)+~P19(x4862)+~P19(x4861)+~P3(x4862)+~P3(x4861)+~P16(x4863)+~P8(x4863,f37(x4862),f37(x4861))+~P18(x4863,f37(x4862),f37(x4861))+P18(f36(x4861,x4862,x4863),f37(x4861),f37(x4862)) % 129.18/129.23 [487]~P1(x4872)+~P1(x4871)+~P37(x4872)+~P37(x4871)+~P41(x4872)+~P41(x4871)+~P2(x4872)+~P2(x4871)+~P19(x4872)+~P19(x4871)+~P3(x4872)+~P3(x4871)+~P16(x4873)+~P8(x4873,f37(x4871),f37(x4872))+~P18(x4873,f37(x4871),f37(x4872))+P9(f30(x4871,x4872,x4873),f37(x4872),f37(x4871)) % 129.18/129.23 [488]~P1(x4882)+~P1(x4881)+~P37(x4882)+~P37(x4881)+~P41(x4882)+~P41(x4881)+~P2(x4882)+~P2(x4881)+~P19(x4882)+~P19(x4881)+~P3(x4882)+~P3(x4881)+~P16(x4883)+~P8(x4883,f37(x4882),f37(x4881))+~P18(x4883,f37(x4882),f37(x4881))+P9(f36(x4881,x4882,x4883),f37(x4881),f37(x4882)) % 129.18/129.23 [491]~P1(x4912)+~P14(x4913,x4911,x4912)+~P16(x4913)+~P3(x4911)+~P3(x4912)+~P38(x4911)+~P38(x4912)+~P19(x4911)+~P19(x4912)+~P2(x4911)+~P2(x4912)+~P41(x4911)+~P41(x4912)+~P37(x4911)+~P37(x4912)+~P1(x4911)+~P8(x4913,f37(x4911),f37(x4912))+~P18(x4913,f37(x4911),f37(x4912))+P23(f30(x4911,x4912,x4913)) % 129.18/129.23 [492]~P1(x4922)+~P15(x4923,x4922,x4921)+~P16(x4923)+~P3(x4921)+~P3(x4922)+~P38(x4921)+~P38(x4922)+~P19(x4921)+~P19(x4922)+~P2(x4921)+~P2(x4922)+~P41(x4921)+~P41(x4922)+~P37(x4921)+~P37(x4922)+~P1(x4921)+~P8(x4923,f37(x4922),f37(x4921))+~P18(x4923,f37(x4922),f37(x4921))+P23(f36(x4921,x4922,x4923)) % 129.18/129.23 [493]~P1(x4932)+~P14(x4933,x4931,x4932)+~P16(x4933)+~P3(x4931)+~P3(x4932)+~P38(x4931)+~P38(x4932)+~P19(x4931)+~P19(x4932)+~P2(x4931)+~P2(x4932)+~P41(x4931)+~P41(x4932)+~P37(x4931)+~P37(x4932)+~P1(x4931)+~P8(x4933,f37(x4931),f37(x4932))+~P18(x4933,f37(x4931),f37(x4932))+P50(f30(x4931,x4932,x4933),x4932,x4931) % 129.18/129.23 [494]~P1(x4942)+~P15(x4943,x4942,x4941)+~P16(x4943)+~P3(x4941)+~P3(x4942)+~P38(x4941)+~P38(x4942)+~P19(x4941)+~P19(x4942)+~P2(x4941)+~P2(x4942)+~P41(x4941)+~P41(x4942)+~P37(x4941)+~P37(x4942)+~P1(x4941)+~P8(x4943,f37(x4942),f37(x4941))+~P18(x4943,f37(x4942),f37(x4941))+P50(f36(x4941,x4942,x4943),x4941,x4942) % 129.18/129.23 [495]~P1(x4952)+~P14(x4953,x4951,x4952)+~P16(x4953)+~P3(x4951)+~P3(x4952)+~P38(x4951)+~P38(x4952)+~P19(x4951)+~P19(x4952)+~P2(x4951)+~P2(x4952)+~P41(x4951)+~P41(x4952)+~P37(x4951)+~P37(x4952)+~P1(x4951)+~P8(x4953,f37(x4951),f37(x4952))+~P18(x4953,f37(x4951),f37(x4952))+P32(f30(x4951,x4952,x4953),x4952,x4951) % 129.18/129.23 [496]~P1(x4962)+~P15(x4963,x4962,x4961)+~P16(x4963)+~P3(x4961)+~P3(x4962)+~P38(x4961)+~P38(x4962)+~P19(x4961)+~P19(x4962)+~P2(x4961)+~P2(x4962)+~P41(x4961)+~P41(x4962)+~P37(x4961)+~P37(x4962)+~P1(x4961)+~P8(x4963,f37(x4962),f37(x4961))+~P18(x4963,f37(x4962),f37(x4961))+P13(f36(x4961,x4962,x4963),x4961,x4962) % 129.18/129.23 [497]~P1(x4972)+~P15(x4973,x4972,x4971)+~P16(x4973)+~P3(x4971)+~P3(x4972)+~P38(x4971)+~P38(x4972)+~P19(x4971)+~P19(x4972)+~P2(x4971)+~P2(x4972)+~P41(x4971)+~P41(x4972)+~P37(x4971)+~P37(x4972)+~P1(x4971)+~P8(x4973,f37(x4972),f37(x4971))+~P18(x4973,f37(x4972),f37(x4971))+P48(f36(x4971,x4972,x4973),x4971,x4972) % 129.18/129.23 [498]~P1(x4982)+~P15(x4983,x4982,x4981)+~P16(x4983)+~P3(x4981)+~P3(x4982)+~P38(x4981)+~P38(x4982)+~P19(x4981)+~P19(x4982)+~P2(x4981)+~P2(x4982)+~P41(x4981)+~P41(x4982)+~P37(x4981)+~P37(x4982)+~P1(x4981)+~P8(x4983,f37(x4982),f37(x4981))+~P18(x4983,f37(x4982),f37(x4981))+P14(f36(x4981,x4982,x4983),x4981,x4982) % 129.18/129.23 [499]~P1(x4992)+~P15(x4993,x4992,x4991)+~P16(x4993)+~P3(x4991)+~P3(x4992)+~P38(x4991)+~P38(x4992)+~P19(x4991)+~P19(x4992)+~P2(x4991)+~P2(x4992)+~P41(x4991)+~P41(x4992)+~P37(x4991)+~P37(x4992)+~P1(x4991)+~P8(x4993,f37(x4992),f37(x4991))+~P18(x4993,f37(x4992),f37(x4991))+P33(f36(x4991,x4992,x4993),x4991,x4992) % 129.18/129.23 [500]~P1(x5002)+~P14(x5003,x5001,x5002)+~P16(x5003)+~P3(x5001)+~P3(x5002)+~P38(x5001)+~P38(x5002)+~P19(x5001)+~P19(x5002)+~P2(x5001)+~P2(x5002)+~P41(x5001)+~P41(x5002)+~P37(x5001)+~P37(x5002)+~P1(x5001)+~P8(x5003,f37(x5001),f37(x5002))+~P18(x5003,f37(x5001),f37(x5002))+P51(f30(x5001,x5002,x5003),x5001,x5002) % 129.18/129.23 [501]~P1(x5012)+~P14(x5013,x5011,x5012)+~P16(x5013)+~P3(x5011)+~P3(x5012)+~P38(x5011)+~P38(x5012)+~P19(x5011)+~P19(x5012)+~P2(x5011)+~P2(x5012)+~P41(x5011)+~P41(x5012)+~P37(x5011)+~P37(x5012)+~P1(x5011)+~P8(x5013,f37(x5011),f37(x5012))+~P18(x5013,f37(x5011),f37(x5012))+P15(f30(x5011,x5012,x5013),x5012,x5011) % 129.18/129.23 [502]~P1(x5022)+~P14(x5023,x5021,x5022)+~P16(x5023)+~P3(x5021)+~P3(x5022)+~P38(x5021)+~P38(x5022)+~P19(x5021)+~P19(x5022)+~P2(x5021)+~P2(x5022)+~P41(x5021)+~P41(x5022)+~P37(x5021)+~P37(x5022)+~P1(x5021)+~P8(x5023,f37(x5021),f37(x5022))+~P18(x5023,f37(x5021),f37(x5022))+P34(f30(x5021,x5022,x5023),x5022,x5021) % 129.18/129.23 [505]~P1(x5052)+~P14(x5053,x5051,x5052)+~P16(x5053)+~P3(x5051)+~P3(x5052)+~P38(x5051)+~P38(x5052)+~P19(x5051)+~P19(x5052)+~P2(x5051)+~P2(x5052)+~P41(x5051)+~P41(x5052)+~P37(x5051)+~P37(x5052)+~P1(x5051)+~P8(x5053,f37(x5051),f37(x5052))+~P18(x5053,f37(x5051),f37(x5052))+P25(f30(x5051,x5052,x5053),f37(x5052),f37(x5051)) % 129.18/129.23 [506]~P1(x5062)+~P15(x5063,x5062,x5061)+~P16(x5063)+~P3(x5061)+~P3(x5062)+~P38(x5061)+~P38(x5062)+~P19(x5061)+~P19(x5062)+~P2(x5061)+~P2(x5062)+~P41(x5061)+~P41(x5062)+~P37(x5061)+~P37(x5062)+~P1(x5061)+~P8(x5063,f37(x5062),f37(x5061))+~P18(x5063,f37(x5062),f37(x5061))+P25(f36(x5061,x5062,x5063),f37(x5061),f37(x5062)) % 129.18/129.23 [507]~P37(x5071)+~P37(x5072)+~P41(x5071)+~P41(x5072)+~P2(x5071)+~P2(x5072)+~P19(x5071)+~P19(x5072)+~P38(x5071)+~P38(x5072)+~P3(x5071)+~P3(x5072)+~P14(x5073,x5072,x5071)+~P1(x5071)+~P1(x5072)+~P16(x5073)+~P8(x5073,f37(x5072),f37(x5071))+~P18(x5073,f37(x5072),f37(x5071))+~P22(f30(x5072,x5071,x5073)) % 129.18/129.23 [508]~P37(x5081)+~P37(x5082)+~P41(x5081)+~P41(x5082)+~P2(x5081)+~P2(x5082)+~P19(x5081)+~P19(x5082)+~P38(x5081)+~P38(x5082)+~P3(x5081)+~P3(x5082)+~P15(x5083,x5081,x5082)+~P1(x5081)+~P1(x5082)+~P16(x5083)+~P8(x5083,f37(x5081),f37(x5082))+~P18(x5083,f37(x5081),f37(x5082))+~P22(f36(x5082,x5081,x5083)) % 129.18/129.23 [512]~P2(x5121)+~P14(x5123,x5121,x5122)+~P16(x5124)+~P16(x5123)+~P3(x5121)+~P3(x5122)+~P38(x5121)+~P38(x5122)+~P19(x5121)+~P19(x5122)+~P2(x5122)+~P41(x5121)+~P41(x5122)+~P37(x5121)+~P37(x5122)+~P1(x5121)+~P1(x5122)+~P18(x5124,f37(x5122),f37(x5121))+~P9(x5124,f37(x5122),f37(x5121))+~P9(x5123,f37(x5121),f37(x5122))+~P18(x5123,f37(x5121),f37(x5122))+P44(f31(x5121,x5122,x5123,x5124),x5121,x5122)+~E(x5124,f30(x5121,x5122,x5123)) % 129.18/129.23 [513]~P2(x5131)+~P15(x5134,x5132,x5131)+~P16(x5133)+~P16(x5134)+~P3(x5131)+~P3(x5132)+~P38(x5131)+~P38(x5132)+~P19(x5131)+~P19(x5132)+~P2(x5132)+~P41(x5131)+~P41(x5132)+~P37(x5131)+~P37(x5132)+~P1(x5131)+~P1(x5132)+~P18(x5133,f37(x5131),f37(x5132))+~P9(x5133,f37(x5131),f37(x5132))+~P9(x5134,f37(x5132),f37(x5131))+~P18(x5134,f37(x5132),f37(x5131))+P44(f31(x5131,x5132,x5133,x5134),x5131,x5132)+~E(x5133,f36(x5131,x5132,x5134)) % 129.18/129.23 [514]~P1(x5143)+~P14(x5144,x5142,x5143)+~P16(x5144)+~P16(x5141)+~P3(x5142)+~P3(x5143)+~P38(x5142)+~P38(x5143)+~P19(x5142)+~P19(x5143)+~P2(x5142)+~P2(x5143)+~P41(x5142)+~P41(x5143)+~P37(x5142)+~P37(x5143)+~P1(x5142)+~P18(x5141,f37(x5143),f37(x5142))+~P18(x5144,f37(x5142),f37(x5143))+~P9(x5141,f37(x5143),f37(x5142))+~P9(x5144,f37(x5142),f37(x5143))+~P44(f31(x5142,x5143,x5144,x5141),x5142,x5143)+E(x5141,f30(x5142,x5143,x5144)) % 129.18/129.23 [515]~P1(x5153)+~P15(x5154,x5153,x5152)+~P16(x5151)+~P16(x5154)+~P3(x5152)+~P3(x5153)+~P38(x5152)+~P38(x5153)+~P19(x5152)+~P19(x5153)+~P2(x5152)+~P2(x5153)+~P41(x5152)+~P41(x5153)+~P37(x5152)+~P37(x5153)+~P1(x5152)+~P18(x5154,f37(x5153),f37(x5152))+~P18(x5151,f37(x5152),f37(x5153))+~P9(x5154,f37(x5153),f37(x5152))+~P9(x5151,f37(x5152),f37(x5153))+~P44(f31(x5152,x5153,x5151,x5154),x5152,x5153)+E(x5151,f36(x5152,x5153,x5154)) % 129.18/129.23 %EqnAxiom % 129.18/129.23 [1]E(x11,x11) % 129.18/129.23 [2]E(x22,x21)+~E(x21,x22) % 129.18/129.23 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 129.18/129.23 [4]~E(x41,x42)+E(f29(x41),f29(x42)) % 129.18/129.23 [5]~E(x51,x52)+E(f24(x51),f24(x52)) % 129.18/129.23 [6]~E(x61,x62)+E(f32(x61,x63),f32(x62,x63)) % 129.18/129.23 [7]~E(x71,x72)+E(f32(x73,x71),f32(x73,x72)) % 129.18/129.23 [8]~E(x81,x82)+E(f30(x81,x83,x84),f30(x82,x83,x84)) % 129.18/129.23 [9]~E(x91,x92)+E(f30(x93,x91,x94),f30(x93,x92,x94)) % 129.18/129.23 [10]~E(x101,x102)+E(f30(x103,x104,x101),f30(x103,x104,x102)) % 129.18/129.23 [11]~E(x111,x112)+E(f37(x111),f37(x112)) % 129.18/129.23 [12]~E(x121,x122)+E(f25(x121,x123),f25(x122,x123)) % 129.18/129.23 [13]~E(x131,x132)+E(f25(x133,x131),f25(x133,x132)) % 129.18/129.23 [14]~E(x141,x142)+E(f26(x141,x143),f26(x142,x143)) % 129.18/129.23 [15]~E(x151,x152)+E(f26(x153,x151),f26(x153,x152)) % 129.18/129.23 [16]~E(x161,x162)+E(f31(x161,x163,x164,x165),f31(x162,x163,x164,x165)) % 129.18/129.23 [17]~E(x171,x172)+E(f31(x173,x171,x174,x175),f31(x173,x172,x174,x175)) % 129.18/129.23 [18]~E(x181,x182)+E(f31(x183,x184,x181,x185),f31(x183,x184,x182,x185)) % 129.18/129.23 [19]~E(x191,x192)+E(f31(x193,x194,x195,x191),f31(x193,x194,x195,x192)) % 129.18/129.23 [20]~E(x201,x202)+E(f10(x201),f10(x202)) % 129.18/129.23 [21]~E(x211,x212)+E(f14(x211),f14(x212)) % 129.18/129.23 [22]~E(x221,x222)+E(f16(x221),f16(x222)) % 129.18/129.23 [23]~E(x231,x232)+E(f11(x231),f11(x232)) % 129.18/129.23 [24]~E(x241,x242)+E(f17(x241),f17(x242)) % 129.18/129.23 [25]~E(x251,x252)+E(f34(x251),f34(x252)) % 129.18/129.23 [26]~E(x261,x262)+E(f18(x261,x263),f18(x262,x263)) % 129.18/129.23 [27]~E(x271,x272)+E(f18(x273,x271),f18(x273,x272)) % 129.18/129.23 [28]~E(x281,x282)+E(f36(x281,x283,x284),f36(x282,x283,x284)) % 129.18/129.23 [29]~E(x291,x292)+E(f36(x293,x291,x294),f36(x293,x292,x294)) % 129.18/129.23 [30]~E(x301,x302)+E(f36(x303,x304,x301),f36(x303,x304,x302)) % 129.18/129.23 [31]~E(x311,x312)+E(f33(x311),f33(x312)) % 129.18/129.23 [32]~E(x321,x322)+E(f20(x321,x323),f20(x322,x323)) % 129.18/129.23 [33]~E(x331,x332)+E(f20(x333,x331),f20(x333,x332)) % 129.18/129.23 [34]~E(x341,x342)+E(f8(x341,x343),f8(x342,x343)) % 129.18/129.23 [35]~E(x351,x352)+E(f8(x353,x351),f8(x353,x352)) % 129.18/129.23 [36]~E(x361,x362)+E(f9(x361,x363),f9(x362,x363)) % 129.18/129.23 [37]~E(x371,x372)+E(f9(x373,x371),f9(x373,x372)) % 129.18/129.23 [38]~E(x381,x382)+E(f19(x381),f19(x382)) % 129.18/129.23 [39]~E(x391,x392)+E(f7(x391),f7(x392)) % 129.18/129.23 [40]~E(x401,x402)+E(f4(x401,x403),f4(x402,x403)) % 129.18/129.23 [41]~E(x411,x412)+E(f4(x413,x411),f4(x413,x412)) % 129.18/129.23 [42]~E(x421,x422)+E(f35(x421,x423),f35(x422,x423)) % 129.18/129.23 [43]~E(x431,x432)+E(f35(x433,x431),f35(x433,x432)) % 129.18/129.23 [44]~E(x441,x442)+E(f27(x441,x443),f27(x442,x443)) % 129.18/129.23 [45]~E(x451,x452)+E(f27(x453,x451),f27(x453,x452)) % 129.18/129.23 [46]~P1(x461)+P1(x462)+~E(x461,x462) % 129.18/129.23 [47]P44(x472,x473,x474)+~E(x471,x472)+~P44(x471,x473,x474) % 129.18/129.23 [48]P44(x483,x482,x484)+~E(x481,x482)+~P44(x483,x481,x484) % 129.18/129.23 [49]P44(x493,x494,x492)+~E(x491,x492)+~P44(x493,x494,x491) % 129.18/129.23 [50]~P37(x501)+P37(x502)+~E(x501,x502) % 129.18/129.23 [51]P8(x512,x513,x514)+~E(x511,x512)+~P8(x511,x513,x514) % 129.18/129.23 [52]P8(x523,x522,x524)+~E(x521,x522)+~P8(x523,x521,x524) % 129.18/129.23 [53]P8(x533,x534,x532)+~E(x531,x532)+~P8(x533,x534,x531) % 129.18/129.23 [54]~P41(x541)+P41(x542)+~E(x541,x542) % 129.18/129.23 [55]~P19(x551)+P19(x552)+~E(x551,x552) % 129.18/129.23 [56]~P2(x561)+P2(x562)+~E(x561,x562) % 129.18/129.23 [57]~P3(x571)+P3(x572)+~E(x571,x572) % 129.18/129.23 [58]P18(x582,x583,x584)+~E(x581,x582)+~P18(x581,x583,x584) % 129.18/129.23 [59]P18(x593,x592,x594)+~E(x591,x592)+~P18(x593,x591,x594) % 129.18/129.23 [60]P18(x603,x604,x602)+~E(x601,x602)+~P18(x603,x604,x601) % 129.18/129.23 [61]~P43(x611)+P43(x612)+~E(x611,x612) % 129.18/129.23 [62]~P38(x621)+P38(x622)+~E(x621,x622) % 129.18/129.23 [63]P13(x632,x633,x634)+~E(x631,x632)+~P13(x631,x633,x634) % 129.18/129.23 [64]P13(x643,x642,x644)+~E(x641,x642)+~P13(x643,x641,x644) % 129.18/129.23 [65]P13(x653,x654,x652)+~E(x651,x652)+~P13(x653,x654,x651) % 129.18/129.23 [66]~P16(x661)+P16(x662)+~E(x661,x662) % 129.18/129.23 [67]P34(x672,x673,x674)+~E(x671,x672)+~P34(x671,x673,x674) % 129.18/129.23 [68]P34(x683,x682,x684)+~E(x681,x682)+~P34(x683,x681,x684) % 129.18/129.23 [69]P34(x693,x694,x692)+~E(x691,x692)+~P34(x693,x694,x691) % 129.18/129.23 [70]P31(x702,x703,x704)+~E(x701,x702)+~P31(x701,x703,x704) % 129.18/129.23 [71]P31(x713,x712,x714)+~E(x711,x712)+~P31(x713,x711,x714) % 129.18/129.23 [72]P31(x723,x724,x722)+~E(x721,x722)+~P31(x723,x724,x721) % 129.18/129.23 [73]~P20(x731)+P20(x732)+~E(x731,x732) % 129.18/129.23 [74]P12(x742,x743)+~E(x741,x742)+~P12(x741,x743) % 129.18/129.23 [75]P12(x753,x752)+~E(x751,x752)+~P12(x753,x751) % 129.18/129.23 [76]~P36(x761)+P36(x762)+~E(x761,x762) % 129.18/129.23 [77]~P40(x771)+P40(x772)+~E(x771,x772) % 129.18/129.23 [78]~P21(x781)+P21(x782)+~E(x781,x782) % 129.18/129.23 [79]~P17(x791)+P17(x792)+~E(x791,x792) % 129.18/129.23 [80]~P45(x801)+P45(x802)+~E(x801,x802) % 129.18/129.23 [81]~P39(x811)+P39(x812)+~E(x811,x812) % 129.18/129.23 [82]~P42(x821)+P42(x822)+~E(x821,x822) % 129.18/129.23 [83]~P47(x831)+P47(x832)+~E(x831,x832) % 129.18/129.23 [84]P7(x842,x843)+~E(x841,x842)+~P7(x841,x843) % 129.18/129.23 [85]P7(x853,x852)+~E(x851,x852)+~P7(x853,x851) % 129.18/129.23 [86]~P46(x861)+P46(x862)+~E(x861,x862) % 129.18/129.23 [87]P15(x872,x873,x874)+~E(x871,x872)+~P15(x871,x873,x874) % 129.18/129.23 [88]P15(x883,x882,x884)+~E(x881,x882)+~P15(x883,x881,x884) % 129.18/129.23 [89]P15(x893,x894,x892)+~E(x891,x892)+~P15(x893,x894,x891) % 129.18/129.23 [90]~P22(x901)+P22(x902)+~E(x901,x902) % 129.18/129.23 [91]~P24(x911)+P24(x912)+~E(x911,x912) % 129.18/129.23 [92]~P4(x921)+P4(x922)+~E(x921,x922) % 129.18/129.23 [93]~P5(x931)+P5(x932)+~E(x931,x932) % 129.18/129.23 [94]P25(x942,x943,x944)+~E(x941,x942)+~P25(x941,x943,x944) % 129.18/129.23 [95]P25(x953,x952,x954)+~E(x951,x952)+~P25(x953,x951,x954) % 129.18/129.23 [96]P25(x963,x964,x962)+~E(x961,x962)+~P25(x963,x964,x961) % 129.18/129.23 [97]P50(x972,x973,x974)+~E(x971,x972)+~P50(x971,x973,x974) % 129.18/129.23 [98]P50(x983,x982,x984)+~E(x981,x982)+~P50(x983,x981,x984) % 129.18/129.23 [99]P50(x993,x994,x992)+~E(x991,x992)+~P50(x993,x994,x991) % 129.18/129.23 [100]~P23(x1001)+P23(x1002)+~E(x1001,x1002) % 129.18/129.23 [101]~P30(x1011)+P30(x1012)+~E(x1011,x1012) % 129.18/129.23 [102]P53(x1022,x1023)+~E(x1021,x1022)+~P53(x1021,x1023) % 129.18/129.23 [103]P53(x1033,x1032)+~E(x1031,x1032)+~P53(x1033,x1031) % 129.18/129.23 [104]~P26(x1041)+P26(x1042)+~E(x1041,x1042) % 129.18/129.23 [105]~P29(x1051)+P29(x1052)+~E(x1051,x1052) % 129.18/129.23 [106]P10(x1062,x1063,x1064)+~E(x1061,x1062)+~P10(x1061,x1063,x1064) % 129.18/129.23 [107]P10(x1073,x1072,x1074)+~E(x1071,x1072)+~P10(x1073,x1071,x1074) % 129.18/129.23 [108]P10(x1083,x1084,x1082)+~E(x1081,x1082)+~P10(x1083,x1084,x1081) % 129.18/129.23 [109]P33(x1092,x1093,x1094)+~E(x1091,x1092)+~P33(x1091,x1093,x1094) % 129.18/129.23 [110]P33(x1103,x1102,x1104)+~E(x1101,x1102)+~P33(x1103,x1101,x1104) % 129.18/129.23 [111]P33(x1113,x1114,x1112)+~E(x1111,x1112)+~P33(x1113,x1114,x1111) % 129.18/129.23 [112]P49(x1122,x1123)+~E(x1121,x1122)+~P49(x1121,x1123) % 129.18/129.23 [113]P49(x1133,x1132)+~E(x1131,x1132)+~P49(x1133,x1131) % 129.18/129.23 [114]P6(x1142,x1143)+~E(x1141,x1142)+~P6(x1141,x1143) % 129.18/129.23 [115]P6(x1153,x1152)+~E(x1151,x1152)+~P6(x1153,x1151) % 129.18/129.23 [116]~P35(x1161)+P35(x1162)+~E(x1161,x1162) % 129.18/129.23 [117]P9(x1172,x1173,x1174)+~E(x1171,x1172)+~P9(x1171,x1173,x1174) % 129.18/129.23 [118]P9(x1183,x1182,x1184)+~E(x1181,x1182)+~P9(x1183,x1181,x1184) % 129.18/129.23 [119]P9(x1193,x1194,x1192)+~E(x1191,x1192)+~P9(x1193,x1194,x1191) % 129.18/129.23 [120]P48(x1202,x1203,x1204)+~E(x1201,x1202)+~P48(x1201,x1203,x1204) % 129.18/129.23 [121]P48(x1213,x1212,x1214)+~E(x1211,x1212)+~P48(x1213,x1211,x1214) % 129.18/129.23 [122]P48(x1223,x1224,x1222)+~E(x1221,x1222)+~P48(x1223,x1224,x1221) % 129.18/129.23 [123]P32(x1232,x1233,x1234)+~E(x1231,x1232)+~P32(x1231,x1233,x1234) % 129.18/129.23 [124]P32(x1243,x1242,x1244)+~E(x1241,x1242)+~P32(x1243,x1241,x1244) % 129.18/129.23 [125]P32(x1253,x1254,x1252)+~E(x1251,x1252)+~P32(x1253,x1254,x1251) % 129.18/129.23 [126]P14(x1262,x1263,x1264)+~E(x1261,x1262)+~P14(x1261,x1263,x1264) % 129.18/129.23 [127]P14(x1273,x1272,x1274)+~E(x1271,x1272)+~P14(x1273,x1271,x1274) % 129.18/129.23 [128]P14(x1283,x1284,x1282)+~E(x1281,x1282)+~P14(x1283,x1284,x1281) % 129.18/129.23 [129]P51(x1292,x1293,x1294)+~E(x1291,x1292)+~P51(x1291,x1293,x1294) % 129.18/129.23 [130]P51(x1303,x1302,x1304)+~E(x1301,x1302)+~P51(x1303,x1301,x1304) % 129.18/129.23 [131]P51(x1313,x1314,x1312)+~E(x1311,x1312)+~P51(x1313,x1314,x1311) % 129.18/129.23 [132]~P28(x1321)+P28(x1322)+~E(x1321,x1322) % 129.18/129.23 [133]~P11(x1331)+P11(x1332)+~E(x1331,x1332) % 129.18/129.23 [134]~P27(x1341)+P27(x1342)+~E(x1341,x1342) % 129.18/129.23 [135]P52(x1352,x1353)+~E(x1351,x1352)+~P52(x1351,x1353) % 129.18/129.23 [136]P52(x1363,x1362)+~E(x1361,x1362)+~P52(x1363,x1361) % 129.18/129.23 % 129.18/129.23 %------------------------------------------- % 129.18/129.23 cnf(518,plain, % 129.18/129.23 (~P12(x5181,a21)), % 129.18/129.23 inference(scs_inference,[],[165,269])). % 129.18/129.23 cnf(521,plain, % 129.18/129.23 (P7(f24(x5211),x5211)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(523,plain, % 129.18/129.23 (P12(f24(a22),a22)), % 129.18/129.23 inference(scs_inference,[],[165,180,521,187,269,355,319])). % 129.18/129.23 cnf(524,plain, % 129.18/129.23 (P7(f24(x5241),x5241)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(526,plain, % 129.18/129.23 (P8(f25(f32(x5261,x5262),x5263),f32(x5262,x5261),x5263)), % 129.18/129.23 inference(scs_inference,[],[183,165,180,521,181,187,269,355,319,52])). % 129.18/129.23 cnf(527,plain, % 129.18/129.23 (P8(f25(x5271,x5272),x5271,x5272)), % 129.18/129.23 inference(rename_variables,[],[183])). % 129.18/129.23 cnf(528,plain, % 129.18/129.23 (P8(f25(x5281,f32(x5282,x5283)),x5281,f32(x5283,x5282))), % 129.18/129.23 inference(scs_inference,[],[183,527,165,180,521,181,187,269,355,319,52,53])). % 129.18/129.23 cnf(530,plain, % 129.18/129.23 (~E(a22,a21)), % 129.18/129.23 inference(scs_inference,[],[183,527,165,180,521,181,187,269,355,319,52,53,75])). % 129.18/129.23 cnf(531,plain, % 129.18/129.23 (P7(f24(f32(x5311,x5312)),f32(x5312,x5311))), % 129.18/129.23 inference(scs_inference,[],[183,527,165,180,521,524,181,187,269,355,319,52,53,75,85])). % 129.18/129.23 cnf(532,plain, % 129.18/129.23 (P7(f24(x5321),x5321)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(533,plain, % 129.18/129.23 (P6(f32(x5331,x5332),f32(x5332,x5331))), % 129.18/129.23 inference(scs_inference,[],[183,527,165,179,180,521,524,181,187,269,355,319,52,53,75,85,114])). % 129.18/129.23 cnf(535,plain, % 129.18/129.23 (P9(f26(f32(x5351,x5352),x5353),f32(x5352,x5351),x5353)), % 129.18/129.23 inference(scs_inference,[],[183,527,184,165,179,180,521,524,181,187,269,355,319,52,53,75,85,114,118])). % 129.18/129.23 cnf(536,plain, % 129.18/129.23 (P9(f26(x5361,x5362),x5361,x5362)), % 129.18/129.23 inference(rename_variables,[],[184])). % 129.18/129.23 cnf(540,plain, % 129.18/129.23 (P7(f24(x5401),x5401)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(543,plain, % 129.18/129.23 (P7(f24(x5431),x5431)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(546,plain, % 129.18/129.23 (P7(f24(x5461),x5461)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(549,plain, % 129.18/129.23 (P7(f24(x5491),x5491)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(552,plain, % 129.18/129.23 (P7(f24(x5521),x5521)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(555,plain, % 129.18/129.23 (P7(f24(x5551),x5551)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(557,plain, % 129.18/129.23 (~P12(x5571,f24(f33(a21)))), % 129.18/129.23 inference(scs_inference,[],[183,527,184,536,165,179,180,521,524,532,540,543,546,549,552,555,181,152,154,157,161,163,167,187,269,355,319,52,53,75,85,114,118,119,321,326,330,333,335,336,369])). % 129.18/129.23 cnf(558,plain, % 129.18/129.23 (P7(f24(x5581),x5581)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(562,plain, % 129.18/129.23 (~P7(a21,a6)), % 129.18/129.23 inference(scs_inference,[],[183,527,184,536,165,166,169,179,180,521,524,532,540,543,546,549,552,555,181,152,154,157,161,163,167,172,174,187,189,269,355,319,52,53,75,85,114,118,119,321,326,330,333,335,336,369,246,318])). % 129.18/129.23 cnf(574,plain, % 129.18/129.23 (P7(f24(x5741),x5741)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(578,plain, % 129.18/129.23 (~P22(f24(a6))), % 129.18/129.23 inference(scs_inference,[],[138,183,527,184,536,148,151,165,166,169,185,179,180,521,524,532,540,543,546,549,552,555,558,574,181,152,154,157,161,163,167,172,174,187,189,269,355,319,52,53,75,85,114,118,119,321,326,330,333,335,336,369,246,318,270,271,300,354,46,84,371,192])). % 129.18/129.23 cnf(585,plain, % 129.18/129.23 (~P12(x5851,a5)), % 129.18/129.23 inference(scs_inference,[],[166,269])). % 129.18/129.23 cnf(587,plain, % 129.18/129.23 (~P12(x5871,f24(f33(a5)))), % 129.18/129.23 inference(scs_inference,[],[166,180,269,369])). % 129.18/129.23 cnf(588,plain, % 129.18/129.23 (P7(f24(x5881),x5881)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(595,plain, % 129.18/129.23 (P9(f26(f32(x5951,x5952),f32(x5953,x5954)),f32(x5952,x5951),f32(x5954,x5953))), % 129.18/129.23 inference(scs_inference,[],[535,523,166,181,557,578,180,588,269,369,319,75,119])). % 129.18/129.23 cnf(597,plain, % 129.18/129.23 (P8(f25(f32(x5971,x5972),f32(x5973,x5974)),f32(x5972,x5971),f32(x5974,x5973))), % 129.18/129.23 inference(scs_inference,[],[526,535,523,166,181,557,578,180,588,269,369,319,75,119,53])). % 129.18/129.23 cnf(613,plain, % 129.18/129.23 (P12(f24(a3),a3)), % 129.18/129.23 inference(scs_inference,[],[188,180,319])). % 129.18/129.23 cnf(630,plain, % 129.18/129.23 (P12(f24(f29(x6301)),f29(x6301))), % 129.18/129.23 inference(scs_inference,[],[190,180,319])). % 129.18/129.23 cnf(635,plain, % 129.18/129.23 (~P12(f29(x6351),f24(f29(x6351)))), % 129.18/129.23 inference(scs_inference,[],[613,518,190,180,319,75,354])). % 129.18/129.23 cnf(643,plain, % 129.18/129.23 (P12(f24(f32(x6431,x6432)),f32(x6432,x6431))), % 129.18/129.23 inference(scs_inference,[],[531,191,319])). % 129.18/129.23 cnf(648,plain, % 129.18/129.23 (~P12(f32(x6481,x6482),f24(f32(x6482,x6481)))), % 129.18/129.23 inference(scs_inference,[],[531,630,585,191,319,75,354])). % 129.18/129.23 cnf(678,plain, % 129.18/129.23 (P7(x6781,f32(x6782,x6783))+~E(f24(f32(x6783,x6782)),x6781)), % 129.18/129.23 inference(scs_inference,[],[531,643,518,75,84])). % 129.18/129.23 cnf(734,plain, % 129.18/129.23 (~E(a22,a5)), % 129.18/129.23 inference(scs_inference,[],[523,585,75])). % 129.18/129.23 cnf(736,plain, % 129.18/129.23 (~P26(f32(x7361,x7362))+P26(f32(x7362,x7361))), % 129.18/129.23 inference(scs_inference,[],[523,181,585,75,104])). % 129.18/129.23 cnf(759,plain, % 129.18/129.23 (P43(a1)+P42(a1)), % 129.18/129.23 inference(scs_inference,[],[147,149,595,597,643,523,181,587,75,51,74,82,117,244])). % 129.18/129.23 cnf(791,plain, % 129.18/129.23 (~P26(f29(x7911))+~P7(a5,f29(x7911))), % 129.18/129.23 inference(scs_inference,[],[166,190,318])). % 129.18/129.23 cnf(800,plain, % 129.18/129.23 (~P26(f29(x8001))+~P7(a21,f29(x8001))), % 129.18/129.23 inference(scs_inference,[],[165,190,318])). % 129.18/129.23 cnf(806,plain, % 129.18/129.23 (~P26(f32(x8061,x8062))+~P7(a21,f32(x8061,x8062))), % 129.18/129.23 inference(scs_inference,[],[165,191,318])). % 129.18/129.23 cnf(808,plain, % 129.18/129.23 (~P26(f32(x8081,x8082))+~P7(a21,f32(x8082,x8081))), % 129.18/129.23 inference(scs_inference,[],[165,191,318,736])). % 129.18/129.23 cnf(811,plain, % 129.18/129.23 (~P26(f32(x8111,x8112))+~P7(a5,f32(x8111,x8112))), % 129.18/129.23 inference(scs_inference,[],[166,191,318])). % 129.18/129.23 cnf(813,plain, % 129.18/129.23 (~P26(f32(x8131,x8132))+~P7(a5,f32(x8132,x8131))), % 129.18/129.23 inference(scs_inference,[],[166,191,318,736])). % 129.18/129.23 cnf(922,plain, % 129.18/129.23 (P28(f24(a21))), % 129.18/129.23 inference(scs_inference,[],[165,180,198,284])). % 129.18/129.23 cnf(968,plain, % 129.18/129.23 (P40(a5)), % 129.18/129.23 inference(scs_inference,[],[166,200,197])). % 129.18/129.23 cnf(1014,plain, % 129.18/129.23 (P24(f24(a21))), % 129.18/129.23 inference(scs_inference,[],[165,180,201,289])). % 129.18/129.23 cnf(1161,plain, % 129.18/129.23 (P16(f34(a1))), % 129.18/129.23 inference(scs_inference,[],[149,204,226])). % 129.18/129.23 cnf(1177,plain, % 129.18/129.23 (P42(a1)), % 129.18/129.23 inference(scs_inference,[],[143,149,759,235])). % 129.18/129.23 cnf(1178,plain, % 129.18/129.23 (P21(a1)), % 129.18/129.23 inference(scs_inference,[],[149,1177,230])). % 129.18/129.23 cnf(1292,plain, % 129.18/129.23 (P4(f14(a22))), % 129.18/129.23 inference(scs_inference,[],[530,205,192])). % 129.18/129.23 cnf(3269,plain, % 129.18/129.23 (P7(f32(x32691,x32692),f33(f32(x32691,x32692)))), % 129.18/129.23 inference(scs_inference,[],[533,181,320,114])). % 129.18/129.23 cnf(8271,plain, % 129.18/129.23 (P18(f34(a1),f37(a1),f37(a1))), % 129.18/129.23 inference(scs_inference,[],[149,399,204])). % 129.18/129.23 cnf(8332,plain, % 129.18/129.23 (P9(f34(a1),f37(a1),f37(a1))), % 129.18/129.23 inference(scs_inference,[],[149,400,204])). % 129.18/129.23 cnf(8450,plain, % 129.18/129.23 (~P26(f32(x84501,x84502))+~P12(a21,f32(x84502,x84501))), % 129.18/129.23 inference(scs_inference,[],[808,300])). % 129.18/129.23 cnf(8562,plain, % 129.18/129.23 (~E(f24(f32(x85621,x85622)),a5)+~P26(f32(x85621,x85622))), % 129.18/129.23 inference(scs_inference,[],[813,678])). % 129.18/129.23 cnf(10887,plain, % 129.18/129.23 (P46(a5)), % 129.18/129.23 inference(scs_inference,[],[166,196,200,201])). % 129.18/129.23 cnf(10889,plain, % 129.18/129.23 (P4(a5)), % 129.18/129.23 inference(scs_inference,[],[166,196,200,201,202])). % 129.18/129.23 cnf(10891,plain, % 129.18/129.23 (P5(a12)), % 129.18/129.23 inference(scs_inference,[],[166,150,196,200,201,202,204])). % 129.18/129.23 cnf(10909,plain, % 129.18/129.23 (~P22(f14(a22))), % 129.18/129.23 inference(scs_inference,[],[176,1014,187,188,166,150,196,200,201,202,204,205,206,218,224,226,227,228,229,233])). % 129.18/129.23 cnf(10913,plain, % 129.18/129.23 (P7(x109131,f33(x109131))), % 129.18/129.23 inference(scs_inference,[],[176,179,1014,187,188,166,150,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320])). % 129.18/129.23 cnf(10974,plain, % 129.18/129.23 (E(a5,a21)), % 129.18/129.23 inference(scs_inference,[],[176,734,526,179,535,1014,187,188,184,166,150,181,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192])). % 129.18/129.23 cnf(10976,plain, % 129.18/129.23 (P26(f29(a22))), % 129.18/129.23 inference(scs_inference,[],[176,734,526,179,535,1014,187,188,184,166,150,181,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207])). % 129.18/129.23 cnf(10980,plain, % 129.18/129.23 (P7(f24(x109801),x109801)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(10983,plain, % 129.18/129.23 (P7(f24(x109831),x109831)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(10986,plain, % 129.18/129.23 (P7(f24(x109861),x109861)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(10989,plain, % 129.18/129.23 (P7(f24(x109891),x109891)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(10992,plain, % 129.18/129.23 (P7(f24(x109921),x109921)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(10995,plain, % 129.18/129.23 (P7(f24(x109951),x109951)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(11042,plain, % 129.18/129.23 (~P43(a1)), % 129.18/129.23 inference(scs_inference,[],[176,177,1292,734,158,164,922,526,179,535,162,1014,187,188,184,143,166,180,10980,10983,10986,10989,10992,150,181,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235])). % 129.18/129.23 cnf(11051,plain, % 129.18/129.23 (P17(f24(a21))), % 129.18/129.23 inference(scs_inference,[],[176,177,1292,734,158,164,922,526,179,535,162,1014,187,188,184,161,143,523,166,180,10980,10983,10986,10989,10992,10995,150,181,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290])). % 129.18/129.23 cnf(11052,plain, % 129.18/129.23 (P7(f24(x110521),x110521)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(11061,plain, % 129.18/129.23 (P22(f24(f33(a21)))), % 129.18/129.23 inference(scs_inference,[],[176,177,1292,648,734,158,164,922,526,179,535,162,1014,562,187,188,184,161,557,143,523,166,180,10980,10983,10986,10989,10992,10995,11052,150,181,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319])). % 129.18/129.23 cnf(11063,plain, % 129.18/129.23 (P7(f24(x110631),x110631)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(11069,plain, % 129.18/129.23 (P16(f11(a2))), % 129.18/129.23 inference(scs_inference,[],[176,177,1292,648,734,158,164,922,533,526,179,535,138,162,1014,562,187,188,184,161,557,143,523,166,180,10980,10983,10986,10989,10992,10995,11052,150,181,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255])). % 129.18/129.23 cnf(11093,plain, % 129.18/129.23 (P49(f11(a2),a2)), % 129.18/129.23 inference(scs_inference,[],[176,177,1292,648,734,158,164,922,533,526,179,535,138,162,1014,562,187,188,184,161,557,143,523,166,180,10980,10983,10986,10989,10992,10995,11052,150,181,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306])). % 129.18/129.23 cnf(11137,plain, % 129.18/129.23 (P8(f11(a2),f37(a2),f37(a2))), % 129.18/129.23 inference(scs_inference,[],[176,177,1292,648,734,158,164,922,533,526,179,535,138,162,1014,562,187,188,184,161,557,143,523,166,180,10980,10983,10986,10989,10992,10995,11052,150,181,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306,307,310,311,312,314,315,316,381,382,383,384,385,386,387,388,389,390,391,392,393,406,407])). % 129.18/129.23 cnf(11143,plain, % 129.18/129.23 (P18(f11(a2),f37(a2),f37(a2))), % 129.18/129.23 inference(scs_inference,[],[176,177,1292,648,734,158,164,922,533,526,179,535,138,162,1014,562,187,188,184,161,557,143,523,166,180,10980,10983,10986,10989,10992,10995,11052,150,181,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306,307,310,311,312,314,315,316,381,382,383,384,385,386,387,388,389,390,391,392,393,406,407,408,412,413])). % 129.18/129.23 cnf(11173,plain, % 129.18/129.23 (P16(f4(a1,a1))), % 129.18/129.23 inference(scs_inference,[],[137,139,176,177,1292,648,734,158,164,922,533,526,145,179,535,138,162,1014,562,187,188,184,161,557,143,523,174,189,166,180,10980,10983,10986,10989,10992,10995,11052,150,181,141,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306,307,310,311,312,314,315,316,381,382,383,384,385,386,387,388,389,390,391,392,393,406,407,408,412,413,414,418,419,420,318,357,358,424,428,429,430,453,459,511,425])). % 129.18/129.23 cnf(11181,plain, % 129.18/129.23 (P8(f4(a1,a1),f37(a1),f37(a1))), % 129.18/129.23 inference(scs_inference,[],[137,139,176,177,1292,648,734,158,164,922,533,526,145,179,535,138,162,1014,562,187,188,184,161,557,143,523,174,189,166,180,10980,10983,10986,10989,10992,10995,11052,150,181,141,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306,307,310,311,312,314,315,316,381,382,383,384,385,386,387,388,389,390,391,392,393,406,407,408,412,413,414,418,419,420,318,357,358,424,428,429,430,453,459,511,425,426,446,447,448])). % 129.18/129.23 cnf(11183,plain, % 129.18/129.23 (P18(f4(a1,a1),f37(a1),f37(a1))), % 129.18/129.23 inference(scs_inference,[],[137,139,176,177,1292,648,734,158,164,922,533,526,145,179,535,138,162,1014,562,187,188,184,161,557,143,523,174,189,166,180,10980,10983,10986,10989,10992,10995,11052,150,181,141,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306,307,310,311,312,314,315,316,381,382,383,384,385,386,387,388,389,390,391,392,393,406,407,408,412,413,414,418,419,420,318,357,358,424,428,429,430,453,459,511,425,426,446,447,448,449])). % 129.18/129.23 cnf(11245,plain, % 129.18/129.23 (~P7(a5,f29(a22))), % 129.18/129.23 inference(scs_inference,[],[137,139,140,142,146,176,177,1292,648,734,144,158,164,922,533,526,145,179,148,535,138,162,1014,562,187,188,184,161,557,143,523,174,189,147,166,180,10980,10983,10986,10989,10992,10995,11052,150,181,141,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306,307,310,311,312,314,315,316,381,382,383,384,385,386,387,388,389,390,391,392,393,406,407,408,412,413,414,418,419,420,318,357,358,424,428,429,430,453,459,511,425,426,446,447,448,449,451,452,482,473,474,485,486,487,488,491,492,507,508,493,494,495,496,497,498,499,500,501,502,505,506,203,209,219,221,223,791])). % 129.18/129.23 cnf(11249,plain, % 129.18/129.23 (E(f29(a5),f29(a21))), % 129.18/129.23 inference(scs_inference,[],[137,139,140,142,146,176,177,1292,648,734,144,158,164,922,533,526,145,179,148,535,138,162,1014,562,187,188,184,161,557,143,523,174,189,147,166,180,10980,10983,10986,10989,10992,10995,11052,150,181,141,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306,307,310,311,312,314,315,316,381,382,383,384,385,386,387,388,389,390,391,392,393,406,407,408,412,413,414,418,419,420,318,357,358,424,428,429,430,453,459,511,425,426,446,447,448,449,451,452,482,473,474,485,486,487,488,491,492,507,508,493,494,495,496,497,498,499,500,501,502,505,506,203,209,219,221,223,791,800,4])). % 129.18/129.23 cnf(11252,plain, % 129.18/129.23 (~P7(a5,f32(a22,a22))), % 129.18/129.23 inference(scs_inference,[],[137,139,140,142,146,176,177,1292,648,734,144,158,164,922,533,526,145,179,148,535,138,162,1014,562,187,188,184,161,557,143,523,174,189,147,166,180,10980,10983,10986,10989,10992,10995,11052,150,181,141,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306,307,310,311,312,314,315,316,381,382,383,384,385,386,387,388,389,390,391,392,393,406,407,408,412,413,414,418,419,420,318,357,358,424,428,429,430,453,459,511,425,426,446,447,448,449,451,452,482,473,474,485,486,487,488,491,492,507,508,493,494,495,496,497,498,499,500,501,502,505,506,203,209,219,221,223,791,800,4,806,811])). % 129.18/129.23 cnf(11256,plain, % 129.18/129.23 (~E(f24(f32(a22,a22)),a21)), % 129.18/129.23 inference(scs_inference,[],[137,139,140,142,146,176,177,1292,648,734,144,158,164,922,533,526,145,179,148,535,138,162,1014,562,187,188,184,161,557,143,523,174,189,147,166,180,10980,10983,10986,10989,10992,10995,11052,150,181,141,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306,307,310,311,312,314,315,316,381,382,383,384,385,386,387,388,389,390,391,392,393,406,407,408,412,413,414,418,419,420,318,357,358,424,428,429,430,453,459,511,425,426,446,447,448,449,451,452,482,473,474,485,486,487,488,491,492,507,508,493,494,495,496,497,498,499,500,501,502,505,506,203,209,219,221,223,791,800,4,806,811,8450,678])). % 129.18/129.23 cnf(11263,plain, % 129.18/129.23 (P24(f24(a5))), % 129.18/129.23 inference(scs_inference,[],[137,139,140,142,146,176,177,1292,648,734,144,158,164,922,533,526,145,968,179,148,535,138,162,1014,562,187,188,184,161,557,143,523,174,189,3269,147,166,180,10980,10983,10986,10989,10992,10995,11052,11063,150,181,141,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306,307,310,311,312,314,315,316,381,382,383,384,385,386,387,388,389,390,391,392,393,406,407,408,412,413,414,418,419,420,318,357,358,424,428,429,430,453,459,511,425,426,446,447,448,449,451,452,482,473,474,485,486,487,488,491,492,507,508,493,494,495,496,497,498,499,500,501,502,505,506,203,209,219,221,223,791,800,4,806,811,8450,678,8562,214,278,287])). % 129.18/129.23 cnf(11264,plain, % 129.18/129.23 (P7(f24(x112641),x112641)), % 129.18/129.23 inference(rename_variables,[],[180])). % 129.18/129.23 cnf(11266,plain, % 129.18/129.23 (P9(f26(a5,x112661),a21,x112661)), % 129.18/129.23 inference(scs_inference,[],[137,139,140,142,146,176,177,1292,648,734,144,158,164,922,533,526,145,968,179,148,535,138,162,1014,562,187,188,184,161,557,143,523,174,189,3269,147,166,180,10980,10983,10986,10989,10992,10995,11052,11063,150,181,141,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306,307,310,311,312,314,315,316,381,382,383,384,385,386,387,388,389,390,391,392,393,406,407,408,412,413,414,418,419,420,318,357,358,424,428,429,430,453,459,511,425,426,446,447,448,449,451,452,482,473,474,485,486,487,488,491,492,507,508,493,494,495,496,497,498,499,500,501,502,505,506,203,209,219,221,223,791,800,4,806,811,8450,678,8562,214,278,287,118])). % 129.18/129.23 cnf(11268,plain, % 129.18/129.23 (P28(f24(a5))), % 129.18/129.23 inference(scs_inference,[],[137,139,140,142,146,176,177,1292,648,734,144,158,164,922,533,526,145,968,179,148,535,138,162,1014,562,187,188,184,161,557,143,523,174,189,3269,147,166,180,10980,10983,10986,10989,10992,10995,11052,11063,11264,150,181,141,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306,307,310,311,312,314,315,316,381,382,383,384,385,386,387,388,389,390,391,392,393,406,407,408,412,413,414,418,419,420,318,357,358,424,428,429,430,453,459,511,425,426,446,447,448,449,451,452,482,473,474,485,486,487,488,491,492,507,508,493,494,495,496,497,498,499,500,501,502,505,506,203,209,219,221,223,791,800,4,806,811,8450,678,8562,214,278,287,118,284])). % 129.18/129.23 cnf(11281,plain, % 129.18/129.23 (~E(a5,a3)), % 129.18/129.23 inference(scs_inference,[],[137,139,140,142,146,176,177,1292,648,734,144,158,164,922,533,526,145,968,179,148,535,138,162,1014,562,187,188,184,528,161,557,143,523,174,189,3269,147,166,180,10980,10983,10986,10989,10992,10995,11052,11063,11264,150,181,141,186,185,151,149,196,200,201,202,204,205,206,218,224,226,227,228,229,233,234,320,370,443,444,273,274,11,20,21,22,23,24,25,31,38,39,397,399,400,445,6,7,12,13,14,15,26,27,32,33,34,35,36,37,40,41,42,43,44,45,8,9,10,28,29,30,16,17,18,19,2,192,207,5,280,281,286,288,291,292,238,240,241,247,248,249,250,275,276,342,343,346,347,352,3,372,423,356,401,403,404,405,509,235,337,92,350,369,290,74,351,317,85,319,114,254,255,256,260,261,262,263,264,268,296,297,298,305,306,307,310,311,312,314,315,316,381,382,383,384,385,386,387,388,389,390,391,392,393,406,407,408,412,413,414,418,419,420,318,357,358,424,428,429,430,453,459,511,425,426,446,447,448,449,451,452,482,473,474,485,486,487,488,491,492,507,508,493,494,495,496,497,498,499,500,501,502,505,506,203,209,219,221,223,791,800,4,806,811,8450,678,8562,214,278,287,118,284,339,53,52,119,349,90])). % 129.18/129.23 cnf(11419,plain, % 129.18/129.23 (P7(f24(x114191),x114191)), % 129.18/129.24 inference(rename_variables,[],[180])). % 129.18/129.24 cnf(11427,plain, % 129.18/129.24 (P7(f24(x114271),x114271)), % 129.18/129.24 inference(rename_variables,[],[180])). % 129.18/129.24 cnf(11452,plain, % 129.18/129.24 (P7(f24(x114521),x114521)), % 129.18/129.24 inference(rename_variables,[],[180])). % 129.18/129.24 cnf(11471,plain, % 129.18/129.24 (P7(f24(x114711),x114711)), % 129.18/129.24 inference(rename_variables,[],[180])). % 129.18/129.24 cnf(11646,plain, % 129.18/129.24 (E(f34(a1),f30(a1,a1,f34(a1)))), % 129.18/129.24 inference(scs_inference,[],[137,159,10887,10889,10891,10974,11042,11281,10913,11252,11093,11183,11181,11266,10909,10976,11051,11069,11137,11143,11173,11249,11263,11268,11245,11256,11061,1178,635,177,8271,8332,587,190,613,188,139,145,143,147,148,140,146,142,144,180,11419,11427,11452,11471,138,150,141,185,1161,151,149,211,221,400,227,370,234,205,228,224,229,192,397,443,207,204,214,10,31,40,274,226,37,25,18,444,20,6,15,218,202,233,41,19,44,16,791,7,206,23,399,8,45,14,273,445,9,30,32,33,36,29,42,43,28,35,11,38,24,27,34,26,13,39,12,2,17,22,21,5,240,346,238,423,84,405,403,249,291,247,401,275,509,250,276,356,352,372,404,343,292,248,3,349,90,371,83,317,74,351,85,75,305,381,406,386,297,254,384,418,387,256,310,263,412,311,382,268,307,419,312,408,413,260,392,315,390,261,385,383,389,306,264,314,391,420,393,414,388,316,255,262,296,298,407,318,357,358,428,424,429,430,459,453,374,375,376,377,421,422,431,432,433,434,435,436,437,438,439,440,441,442,511,425,447,446,448,426,449,451,452,474,473,492,491,507,508,514])). % 129.18/129.24 cnf(11648,plain, % 129.18/129.24 (E(f34(a1),f36(a1,a1,f34(a1)))), % 129.18/129.24 inference(scs_inference,[],[137,159,10887,10889,10891,10974,11042,11281,10913,11252,11093,11183,11181,11266,10909,10976,11051,11069,11137,11143,11173,11249,11263,11268,11245,11256,11061,1178,635,177,8271,8332,587,190,613,188,139,145,143,147,148,140,146,142,144,180,11419,11427,11452,11471,138,150,141,185,1161,151,149,211,221,400,227,370,234,205,228,224,229,192,397,443,207,204,214,10,31,40,274,226,37,25,18,444,20,6,15,218,202,233,41,19,44,16,791,7,206,23,399,8,45,14,273,445,9,30,32,33,36,29,42,43,28,35,11,38,24,27,34,26,13,39,12,2,17,22,21,5,240,346,238,423,84,405,403,249,291,247,401,275,509,250,276,356,352,372,404,343,292,248,3,349,90,371,83,317,74,351,85,75,305,381,406,386,297,254,384,418,387,256,310,263,412,311,382,268,307,419,312,408,413,260,392,315,390,261,385,383,389,306,264,314,391,420,393,414,388,316,255,262,296,298,407,318,357,358,428,424,429,430,459,453,374,375,376,377,421,422,431,432,433,434,435,436,437,438,439,440,441,442,511,425,447,446,448,426,449,451,452,474,473,492,491,507,508,514,515])). % 129.18/129.24 cnf(14526,plain, % 129.18/129.24 (E(f36(a1,a1,f34(a1)),f34(a1))), % 129.18/129.24 inference(scs_inference,[],[11648,2])). % 129.18/129.24 cnf(14628,plain, % 129.18/129.24 (~E(f30(a1,a1,f34(a1)),f34(a1))), % 129.18/129.24 inference(scs_inference,[],[14526,450])). % 129.18/129.24 cnf(14725,plain, % 129.18/129.24 ($false), % 129.18/129.24 inference(scs_inference,[],[11646,14628,2]), % 129.18/129.24 ['proof']). % 129.18/129.25 % SZS output end Proof % 129.18/129.25 % Total time :128.360000s %------------------------------------------------------------------------------