%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU230+2 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n021.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 15:01:56 EDT 2024 % Result : Theorem 1.59s 1.69s % Output : CNFRefutation 1.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU230+2 : TPTP v8.2.0. Released v3.3.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 17:49:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.51/0.63 start to proof:theBenchmark % 1.59/1.66 %------------------------------------------- % 1.59/1.66 % File :CSE---1.7 % 1.59/1.66 % Problem :theBenchmark % 1.59/1.66 % Transform :cnf % 1.59/1.66 % Format :tptp:raw % 1.59/1.66 % Command :java -jar mcs_scs.jar %d %s % 1.59/1.66 % 1.59/1.66 % Result :Theorem 0.730000s % 1.59/1.66 % Output :CNFRefutation 0.730000s % 1.59/1.66 %------------------------------------------- % 1.59/1.66 %------------------------------------------------------------------------------ % 1.59/1.66 % File : SEU230+2 : TPTP v8.2.0. Released v3.3.0. % 1.59/1.66 % Domain : Set theory % 1.59/1.66 % Problem : MPTP chainy problem t10_ordinal1 % 1.59/1.66 % Version : [Urb07] axioms : Especial. % 1.59/1.66 % English : % 1.59/1.66 % 1.59/1.66 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 1.59/1.66 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 1.59/1.66 % Source : [Urb07] % 1.59/1.66 % Names : chainy-t10_ordinal1 [Urb07] % 1.59/1.66 % 1.59/1.66 % Status : Theorem % 1.59/1.66 % Rating : 0.25 v8.2.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.17 v7.3.0, 0.14 v7.1.0, 0.09 v7.0.0, 0.20 v6.4.0, 0.19 v6.3.0, 0.12 v6.2.0, 0.24 v6.1.0, 0.37 v6.0.0, 0.43 v5.5.0, 0.41 v5.4.0, 0.39 v5.3.0, 0.44 v5.2.0, 0.25 v5.1.0, 0.29 v5.0.0, 0.38 v4.1.0, 0.39 v4.0.0, 0.42 v3.7.0, 0.35 v3.5.0, 0.37 v3.3.0 % 1.59/1.66 % Syntax : Number of formulae : 255 ( 57 unt; 0 def) % 1.59/1.66 % Number of atoms : 735 ( 157 equ) % 1.59/1.66 % Maximal formula atoms : 15 ( 2 avg) % 1.59/1.66 % Number of connectives : 557 ( 77 ~; 7 |; 177 &) % 1.59/1.66 % ( 87 <=>; 209 =>; 0 <=; 0 <~>) % 1.59/1.66 % Maximal formula depth : 14 ( 5 avg) % 1.59/1.66 % Maximal term depth : 4 ( 1 avg) % 1.59/1.66 % Number of predicates : 13 ( 11 usr; 1 prp; 0-2 aty) % 1.59/1.66 % Number of functors : 31 ( 31 usr; 1 con; 0-3 aty) % 1.59/1.66 % Number of variables : 546 ( 518 !; 28 ?) % 1.59/1.66 % SPC : FOF_THM_RFO_SEQ % 1.59/1.66 % 1.59/1.66 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 1.59/1.66 % library, www.mizar.org % 1.59/1.66 %------------------------------------------------------------------------------ % 1.59/1.66 fof(antisymmetry_r2_hidden,axiom, % 1.59/1.66 ! [A,B] : % 1.59/1.66 ( in(A,B) % 1.59/1.66 => ~ in(B,A) ) ). % 1.59/1.66 % 1.59/1.66 fof(antisymmetry_r2_xboole_0,axiom, % 1.59/1.66 ! [A,B] : % 1.59/1.66 ( proper_subset(A,B) % 1.59/1.66 => ~ proper_subset(B,A) ) ). % 1.59/1.66 % 1.59/1.66 fof(cc1_funct_1,axiom, % 1.59/1.66 ! [A] : % 1.59/1.66 ( empty(A) % 1.59/1.66 => function(A) ) ). % 1.59/1.66 % 1.59/1.66 fof(cc1_relat_1,axiom, % 1.59/1.66 ! [A] : % 1.59/1.66 ( empty(A) % 1.59/1.66 => relation(A) ) ). % 1.59/1.66 % 1.59/1.66 fof(cc2_funct_1,axiom, % 1.59/1.66 ! [A] : % 1.59/1.66 ( ( relation(A) % 1.59/1.66 & empty(A) % 1.59/1.66 & function(A) ) % 1.59/1.66 => ( relation(A) % 1.59/1.66 & function(A) % 1.59/1.66 & one_to_one(A) ) ) ). % 1.59/1.66 % 1.59/1.66 fof(commutativity_k2_tarski,axiom, % 1.59/1.66 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 1.59/1.66 % 1.59/1.66 fof(commutativity_k2_xboole_0,axiom, % 1.59/1.66 ! [A,B] : set_union2(A,B) = set_union2(B,A) ). % 1.59/1.66 % 1.59/1.66 fof(commutativity_k3_xboole_0,axiom, % 1.59/1.66 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 1.59/1.66 % 1.59/1.66 fof(d10_relat_1,axiom, % 1.59/1.66 ! [A,B] : % 1.59/1.66 ( relation(B) % 1.59/1.66 => ( B = identity_relation(A) % 1.59/1.66 <=> ! [C,D] : % 1.59/1.66 ( in(ordered_pair(C,D),B) % 1.59/1.66 <=> ( in(C,A) % 1.59/1.66 & C = D ) ) ) ) ). % 1.59/1.66 % 1.59/1.66 fof(d10_xboole_0,axiom, % 1.59/1.66 ! [A,B] : % 1.59/1.66 ( A = B % 1.59/1.66 <=> ( subset(A,B) % 1.59/1.66 & subset(B,A) ) ) ). % 1.59/1.66 % 1.59/1.66 fof(d11_relat_1,axiom, % 1.59/1.66 ! [A] : % 1.59/1.66 ( relation(A) % 1.59/1.66 => ! [B,C] : % 1.59/1.66 ( relation(C) % 1.59/1.66 => ( C = relation_dom_restriction(A,B) % 1.59/1.66 <=> ! [D,E] : % 1.59/1.66 ( in(ordered_pair(D,E),C) % 1.59/1.66 <=> ( in(D,B) % 1.59/1.66 & in(ordered_pair(D,E),A) ) ) ) ) ) ). % 1.59/1.66 % 1.59/1.66 fof(d12_funct_1,axiom, % 1.59/1.66 ! [A] : % 1.59/1.66 ( ( relation(A) % 1.59/1.66 & function(A) ) % 1.59/1.66 => ! [B,C] : % 1.59/1.66 ( C = relation_image(A,B) % 1.59/1.66 <=> ! [D] : % 1.59/1.66 ( in(D,C) % 1.59/1.66 <=> ? [E] : % 1.59/1.66 ( in(E,relation_dom(A)) % 1.59/1.66 & in(E,B) % 1.59/1.66 & D = apply(A,E) ) ) ) ) ). % 1.59/1.66 % 1.59/1.67 fof(d12_relat_1,axiom, % 1.59/1.67 ! [A,B] : % 1.59/1.67 ( relation(B) % 1.59/1.67 => ! [C] : % 1.59/1.67 ( relation(C) % 1.59/1.67 => ( C = relation_rng_restriction(A,B) % 1.59/1.67 <=> ! [D,E] : % 1.59/1.67 ( in(ordered_pair(D,E),C) % 1.59/1.67 <=> ( in(E,A) % 1.59/1.67 & in(ordered_pair(D,E),B) ) ) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d13_funct_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( ( relation(A) % 1.59/1.67 & function(A) ) % 1.59/1.67 => ! [B,C] : % 1.59/1.67 ( C = relation_inverse_image(A,B) % 1.59/1.67 <=> ! [D] : % 1.59/1.67 ( in(D,C) % 1.59/1.67 <=> ( in(D,relation_dom(A)) % 1.59/1.67 & in(apply(A,D),B) ) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d13_relat_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( relation(A) % 1.59/1.67 => ! [B,C] : % 1.59/1.67 ( C = relation_image(A,B) % 1.59/1.67 <=> ! [D] : % 1.59/1.67 ( in(D,C) % 1.59/1.67 <=> ? [E] : % 1.59/1.67 ( in(ordered_pair(E,D),A) % 1.59/1.67 & in(E,B) ) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d14_relat_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( relation(A) % 1.59/1.67 => ! [B,C] : % 1.59/1.67 ( C = relation_inverse_image(A,B) % 1.59/1.67 <=> ! [D] : % 1.59/1.67 ( in(D,C) % 1.59/1.67 <=> ? [E] : % 1.59/1.67 ( in(ordered_pair(D,E),A) % 1.59/1.67 & in(E,B) ) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d1_enumset1,axiom, % 1.59/1.67 ! [A,B,C,D] : % 1.59/1.67 ( D = unordered_triple(A,B,C) % 1.59/1.67 <=> ! [E] : % 1.59/1.67 ( in(E,D) % 1.59/1.67 <=> ~ ( E != A % 1.59/1.67 & E != B % 1.59/1.67 & E != C ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d1_ordinal1,axiom, % 1.59/1.67 ! [A] : succ(A) = set_union2(A,singleton(A)) ). % 1.59/1.67 % 1.59/1.67 fof(d1_relat_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( relation(A) % 1.59/1.67 <=> ! [B] : % 1.59/1.67 ~ ( in(B,A) % 1.59/1.67 & ! [C,D] : B != ordered_pair(C,D) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d1_setfam_1,axiom, % 1.59/1.67 ! [A,B] : % 1.59/1.67 ( ( A != empty_set % 1.59/1.67 => ( B = set_meet(A) % 1.59/1.67 <=> ! [C] : % 1.59/1.67 ( in(C,B) % 1.59/1.67 <=> ! [D] : % 1.59/1.67 ( in(D,A) % 1.59/1.67 => in(C,D) ) ) ) ) % 1.59/1.67 & ( A = empty_set % 1.59/1.67 => ( B = set_meet(A) % 1.59/1.67 <=> B = empty_set ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d1_tarski,axiom, % 1.59/1.67 ! [A,B] : % 1.59/1.67 ( B = singleton(A) % 1.59/1.67 <=> ! [C] : % 1.59/1.67 ( in(C,B) % 1.59/1.67 <=> C = A ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d1_xboole_0,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( A = empty_set % 1.59/1.67 <=> ! [B] : ~ in(B,A) ) ). % 1.59/1.67 % 1.59/1.67 fof(d1_zfmisc_1,axiom, % 1.59/1.67 ! [A,B] : % 1.59/1.67 ( B = powerset(A) % 1.59/1.67 <=> ! [C] : % 1.59/1.67 ( in(C,B) % 1.59/1.67 <=> subset(C,A) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d2_relat_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( relation(A) % 1.59/1.67 => ! [B] : % 1.59/1.67 ( relation(B) % 1.59/1.67 => ( A = B % 1.59/1.67 <=> ! [C,D] : % 1.59/1.67 ( in(ordered_pair(C,D),A) % 1.59/1.67 <=> in(ordered_pair(C,D),B) ) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d2_subset_1,axiom, % 1.59/1.67 ! [A,B] : % 1.59/1.67 ( ( ~ empty(A) % 1.59/1.67 => ( element(B,A) % 1.59/1.67 <=> in(B,A) ) ) % 1.59/1.67 & ( empty(A) % 1.59/1.67 => ( element(B,A) % 1.59/1.67 <=> empty(B) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d2_tarski,axiom, % 1.59/1.67 ! [A,B,C] : % 1.59/1.67 ( C = unordered_pair(A,B) % 1.59/1.67 <=> ! [D] : % 1.59/1.67 ( in(D,C) % 1.59/1.67 <=> ( D = A % 1.59/1.67 | D = B ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d2_xboole_0,axiom, % 1.59/1.67 ! [A,B,C] : % 1.59/1.67 ( C = set_union2(A,B) % 1.59/1.67 <=> ! [D] : % 1.59/1.67 ( in(D,C) % 1.59/1.67 <=> ( in(D,A) % 1.59/1.67 | in(D,B) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d2_zfmisc_1,axiom, % 1.59/1.67 ! [A,B,C] : % 1.59/1.67 ( C = cartesian_product2(A,B) % 1.59/1.67 <=> ! [D] : % 1.59/1.67 ( in(D,C) % 1.59/1.67 <=> ? [E,F] : % 1.59/1.67 ( in(E,A) % 1.59/1.67 & in(F,B) % 1.59/1.67 & D = ordered_pair(E,F) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d3_relat_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( relation(A) % 1.59/1.67 => ! [B] : % 1.59/1.67 ( relation(B) % 1.59/1.67 => ( subset(A,B) % 1.59/1.67 <=> ! [C,D] : % 1.59/1.67 ( in(ordered_pair(C,D),A) % 1.59/1.67 => in(ordered_pair(C,D),B) ) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d3_tarski,axiom, % 1.59/1.67 ! [A,B] : % 1.59/1.67 ( subset(A,B) % 1.59/1.67 <=> ! [C] : % 1.59/1.67 ( in(C,A) % 1.59/1.67 => in(C,B) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d3_xboole_0,axiom, % 1.59/1.67 ! [A,B,C] : % 1.59/1.67 ( C = set_intersection2(A,B) % 1.59/1.67 <=> ! [D] : % 1.59/1.67 ( in(D,C) % 1.59/1.67 <=> ( in(D,A) % 1.59/1.67 & in(D,B) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d4_funct_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( ( relation(A) % 1.59/1.67 & function(A) ) % 1.59/1.67 => ! [B,C] : % 1.59/1.67 ( ( in(B,relation_dom(A)) % 1.59/1.67 => ( C = apply(A,B) % 1.59/1.67 <=> in(ordered_pair(B,C),A) ) ) % 1.59/1.67 & ( ~ in(B,relation_dom(A)) % 1.59/1.67 => ( C = apply(A,B) % 1.59/1.67 <=> C = empty_set ) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d4_relat_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( relation(A) % 1.59/1.67 => ! [B] : % 1.59/1.67 ( B = relation_dom(A) % 1.59/1.67 <=> ! [C] : % 1.59/1.67 ( in(C,B) % 1.59/1.67 <=> ? [D] : in(ordered_pair(C,D),A) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d4_subset_1,axiom, % 1.59/1.67 ! [A] : cast_to_subset(A) = A ). % 1.59/1.67 % 1.59/1.67 fof(d4_tarski,axiom, % 1.59/1.67 ! [A,B] : % 1.59/1.67 ( B = union(A) % 1.59/1.67 <=> ! [C] : % 1.59/1.67 ( in(C,B) % 1.59/1.67 <=> ? [D] : % 1.59/1.67 ( in(C,D) % 1.59/1.67 & in(D,A) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d4_xboole_0,axiom, % 1.59/1.67 ! [A,B,C] : % 1.59/1.67 ( C = set_difference(A,B) % 1.59/1.67 <=> ! [D] : % 1.59/1.67 ( in(D,C) % 1.59/1.67 <=> ( in(D,A) % 1.59/1.67 & ~ in(D,B) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d5_funct_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( ( relation(A) % 1.59/1.67 & function(A) ) % 1.59/1.67 => ! [B] : % 1.59/1.67 ( B = relation_rng(A) % 1.59/1.67 <=> ! [C] : % 1.59/1.67 ( in(C,B) % 1.59/1.67 <=> ? [D] : % 1.59/1.67 ( in(D,relation_dom(A)) % 1.59/1.67 & C = apply(A,D) ) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d5_relat_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( relation(A) % 1.59/1.67 => ! [B] : % 1.59/1.67 ( B = relation_rng(A) % 1.59/1.67 <=> ! [C] : % 1.59/1.67 ( in(C,B) % 1.59/1.67 <=> ? [D] : in(ordered_pair(D,C),A) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d5_subset_1,axiom, % 1.59/1.67 ! [A,B] : % 1.59/1.67 ( element(B,powerset(A)) % 1.59/1.67 => subset_complement(A,B) = set_difference(A,B) ) ). % 1.59/1.67 % 1.59/1.67 fof(d5_tarski,axiom, % 1.59/1.67 ! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) ). % 1.59/1.67 % 1.59/1.67 fof(d6_relat_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( relation(A) % 1.59/1.67 => relation_field(A) = set_union2(relation_dom(A),relation_rng(A)) ) ). % 1.59/1.67 % 1.59/1.67 fof(d7_relat_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( relation(A) % 1.59/1.67 => ! [B] : % 1.59/1.67 ( relation(B) % 1.59/1.67 => ( B = relation_inverse(A) % 1.59/1.67 <=> ! [C,D] : % 1.59/1.67 ( in(ordered_pair(C,D),B) % 1.59/1.67 <=> in(ordered_pair(D,C),A) ) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d7_xboole_0,axiom, % 1.59/1.67 ! [A,B] : % 1.59/1.67 ( disjoint(A,B) % 1.59/1.67 <=> set_intersection2(A,B) = empty_set ) ). % 1.59/1.67 % 1.59/1.67 fof(d8_funct_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( ( relation(A) % 1.59/1.67 & function(A) ) % 1.59/1.67 => ( one_to_one(A) % 1.59/1.67 <=> ! [B,C] : % 1.59/1.67 ( ( in(B,relation_dom(A)) % 1.59/1.67 & in(C,relation_dom(A)) % 1.59/1.67 & apply(A,B) = apply(A,C) ) % 1.59/1.67 => B = C ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d8_relat_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( relation(A) % 1.59/1.67 => ! [B] : % 1.59/1.67 ( relation(B) % 1.59/1.67 => ! [C] : % 1.59/1.67 ( relation(C) % 1.59/1.67 => ( C = relation_composition(A,B) % 1.59/1.67 <=> ! [D,E] : % 1.59/1.67 ( in(ordered_pair(D,E),C) % 1.59/1.67 <=> ? [F] : % 1.59/1.67 ( in(ordered_pair(D,F),A) % 1.59/1.67 & in(ordered_pair(F,E),B) ) ) ) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d8_setfam_1,axiom, % 1.59/1.67 ! [A,B] : % 1.59/1.67 ( element(B,powerset(powerset(A))) % 1.59/1.67 => ! [C] : % 1.59/1.67 ( element(C,powerset(powerset(A))) % 1.59/1.67 => ( C = complements_of_subsets(A,B) % 1.59/1.67 <=> ! [D] : % 1.59/1.67 ( element(D,powerset(A)) % 1.59/1.67 => ( in(D,C) % 1.59/1.67 <=> in(subset_complement(A,D),B) ) ) ) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d8_xboole_0,axiom, % 1.59/1.67 ! [A,B] : % 1.59/1.67 ( proper_subset(A,B) % 1.59/1.67 <=> ( subset(A,B) % 1.59/1.67 & A != B ) ) ). % 1.59/1.67 % 1.59/1.67 fof(d9_funct_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( ( relation(A) % 1.59/1.67 & function(A) ) % 1.59/1.67 => ( one_to_one(A) % 1.59/1.67 => function_inverse(A) = relation_inverse(A) ) ) ). % 1.59/1.67 % 1.59/1.67 fof(dt_k10_relat_1,axiom, % 1.59/1.67 $true ). % 1.59/1.67 % 1.59/1.67 fof(dt_k1_enumset1,axiom, % 1.59/1.67 $true ). % 1.59/1.67 % 1.59/1.67 fof(dt_k1_funct_1,axiom, % 1.59/1.67 $true ). % 1.59/1.67 % 1.59/1.67 fof(dt_k1_ordinal1,axiom, % 1.59/1.67 $true ). % 1.59/1.67 % 1.59/1.67 fof(dt_k1_relat_1,axiom, % 1.59/1.67 $true ). % 1.59/1.67 % 1.59/1.67 fof(dt_k1_setfam_1,axiom, % 1.59/1.67 $true ). % 1.59/1.67 % 1.59/1.67 fof(dt_k1_tarski,axiom, % 1.59/1.67 $true ). % 1.59/1.67 % 1.59/1.67 fof(dt_k1_xboole_0,axiom, % 1.59/1.67 $true ). % 1.59/1.67 % 1.59/1.67 fof(dt_k1_zfmisc_1,axiom, % 1.59/1.67 $true ). % 1.59/1.67 % 1.59/1.67 fof(dt_k2_funct_1,axiom, % 1.59/1.67 ! [A] : % 1.59/1.67 ( ( relation(A) % 1.59/1.67 & function(A) ) % 1.59/1.67 => ( relation(function_inverse(A)) % 1.59/1.68 & function(function_inverse(A)) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(dt_k2_relat_1,axiom, % 1.59/1.68 $true ). % 1.59/1.68 % 1.59/1.68 fof(dt_k2_subset_1,axiom, % 1.59/1.68 ! [A] : element(cast_to_subset(A),powerset(A)) ). % 1.59/1.68 % 1.59/1.68 fof(dt_k2_tarski,axiom, % 1.59/1.68 $true ). % 1.59/1.68 % 1.59/1.68 fof(dt_k2_xboole_0,axiom, % 1.59/1.68 $true ). % 1.59/1.68 % 1.59/1.68 fof(dt_k2_zfmisc_1,axiom, % 1.59/1.68 $true ). % 1.59/1.68 % 1.59/1.68 fof(dt_k3_relat_1,axiom, % 1.59/1.68 $true ). % 1.59/1.68 % 1.59/1.68 fof(dt_k3_subset_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( element(B,powerset(A)) % 1.59/1.68 => element(subset_complement(A,B),powerset(A)) ) ). % 1.59/1.68 % 1.59/1.68 fof(dt_k3_tarski,axiom, % 1.59/1.68 $true ). % 1.59/1.68 % 1.59/1.68 fof(dt_k3_xboole_0,axiom, % 1.59/1.68 $true ). % 1.59/1.68 % 1.59/1.68 fof(dt_k4_relat_1,axiom, % 1.59/1.68 ! [A] : % 1.59/1.68 ( relation(A) % 1.59/1.68 => relation(relation_inverse(A)) ) ). % 1.59/1.68 % 1.59/1.68 fof(dt_k4_tarski,axiom, % 1.59/1.68 $true ). % 1.59/1.68 % 1.59/1.68 fof(dt_k4_xboole_0,axiom, % 1.59/1.68 $true ). % 1.59/1.68 % 1.59/1.68 fof(dt_k5_relat_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ( relation(A) % 1.59/1.68 & relation(B) ) % 1.59/1.68 => relation(relation_composition(A,B)) ) ). % 1.59/1.68 % 1.59/1.68 fof(dt_k5_setfam_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( element(B,powerset(powerset(A))) % 1.59/1.68 => element(union_of_subsets(A,B),powerset(A)) ) ). % 1.59/1.68 % 1.59/1.68 fof(dt_k6_relat_1,axiom, % 1.59/1.68 ! [A] : relation(identity_relation(A)) ). % 1.59/1.68 % 1.59/1.68 fof(dt_k6_setfam_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( element(B,powerset(powerset(A))) % 1.59/1.68 => element(meet_of_subsets(A,B),powerset(A)) ) ). % 1.59/1.68 % 1.59/1.68 fof(dt_k6_subset_1,axiom, % 1.59/1.68 ! [A,B,C] : % 1.59/1.68 ( ( element(B,powerset(A)) % 1.59/1.68 & element(C,powerset(A)) ) % 1.59/1.68 => element(subset_difference(A,B,C),powerset(A)) ) ). % 1.59/1.68 % 1.59/1.68 fof(dt_k7_relat_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( relation(A) % 1.59/1.68 => relation(relation_dom_restriction(A,B)) ) ). % 1.59/1.68 % 1.59/1.68 fof(dt_k7_setfam_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( element(B,powerset(powerset(A))) % 1.59/1.68 => element(complements_of_subsets(A,B),powerset(powerset(A))) ) ). % 1.59/1.68 % 1.59/1.68 fof(dt_k8_relat_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( relation(B) % 1.59/1.68 => relation(relation_rng_restriction(A,B)) ) ). % 1.59/1.68 % 1.59/1.68 fof(dt_k9_relat_1,axiom, % 1.59/1.68 $true ). % 1.59/1.68 % 1.59/1.68 fof(dt_m1_subset_1,axiom, % 1.59/1.68 $true ). % 1.59/1.68 % 1.59/1.68 fof(existence_m1_subset_1,axiom, % 1.59/1.68 ! [A] : % 1.59/1.68 ? [B] : element(B,A) ). % 1.59/1.68 % 1.59/1.68 fof(fc10_relat_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ( empty(A) % 1.59/1.68 & relation(B) ) % 1.59/1.68 => ( empty(relation_composition(B,A)) % 1.59/1.68 & relation(relation_composition(B,A)) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc11_relat_1,axiom, % 1.59/1.68 ! [A] : % 1.59/1.68 ( empty(A) % 1.59/1.68 => ( empty(relation_inverse(A)) % 1.59/1.68 & relation(relation_inverse(A)) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc12_relat_1,axiom, % 1.59/1.68 ( empty(empty_set) % 1.59/1.68 & relation(empty_set) % 1.59/1.68 & relation_empty_yielding(empty_set) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc13_relat_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ( relation(A) % 1.59/1.68 & relation_empty_yielding(A) ) % 1.59/1.68 => ( relation(relation_dom_restriction(A,B)) % 1.59/1.68 & relation_empty_yielding(relation_dom_restriction(A,B)) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc1_funct_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ( relation(A) % 1.59/1.68 & function(A) % 1.59/1.68 & relation(B) % 1.59/1.68 & function(B) ) % 1.59/1.68 => ( relation(relation_composition(A,B)) % 1.59/1.68 & function(relation_composition(A,B)) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc1_ordinal1,axiom, % 1.59/1.68 ! [A] : ~ empty(succ(A)) ). % 1.59/1.68 % 1.59/1.68 fof(fc1_relat_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ( relation(A) % 1.59/1.68 & relation(B) ) % 1.59/1.68 => relation(set_intersection2(A,B)) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc1_subset_1,axiom, % 1.59/1.68 ! [A] : ~ empty(powerset(A)) ). % 1.59/1.68 % 1.59/1.68 fof(fc1_xboole_0,axiom, % 1.59/1.68 empty(empty_set) ). % 1.59/1.68 % 1.59/1.68 fof(fc1_zfmisc_1,axiom, % 1.59/1.68 ! [A,B] : ~ empty(ordered_pair(A,B)) ). % 1.59/1.68 % 1.59/1.68 fof(fc2_funct_1,axiom, % 1.59/1.68 ! [A] : % 1.59/1.68 ( relation(identity_relation(A)) % 1.59/1.68 & function(identity_relation(A)) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc2_relat_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ( relation(A) % 1.59/1.68 & relation(B) ) % 1.59/1.68 => relation(set_union2(A,B)) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc2_subset_1,axiom, % 1.59/1.68 ! [A] : ~ empty(singleton(A)) ). % 1.59/1.68 % 1.59/1.68 fof(fc2_xboole_0,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ~ empty(A) % 1.59/1.68 => ~ empty(set_union2(A,B)) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc3_funct_1,axiom, % 1.59/1.68 ! [A] : % 1.59/1.68 ( ( relation(A) % 1.59/1.68 & function(A) % 1.59/1.68 & one_to_one(A) ) % 1.59/1.68 => ( relation(relation_inverse(A)) % 1.59/1.68 & function(relation_inverse(A)) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc3_subset_1,axiom, % 1.59/1.68 ! [A,B] : ~ empty(unordered_pair(A,B)) ). % 1.59/1.68 % 1.59/1.68 fof(fc3_xboole_0,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ~ empty(A) % 1.59/1.68 => ~ empty(set_union2(B,A)) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc4_funct_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ( relation(A) % 1.59/1.68 & function(A) ) % 1.59/1.68 => ( relation(relation_dom_restriction(A,B)) % 1.59/1.68 & function(relation_dom_restriction(A,B)) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc4_relat_1,axiom, % 1.59/1.68 ( empty(empty_set) % 1.59/1.68 & relation(empty_set) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc4_subset_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ( ~ empty(A) % 1.59/1.68 & ~ empty(B) ) % 1.59/1.68 => ~ empty(cartesian_product2(A,B)) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc5_relat_1,axiom, % 1.59/1.68 ! [A] : % 1.59/1.68 ( ( ~ empty(A) % 1.59/1.68 & relation(A) ) % 1.59/1.68 => ~ empty(relation_dom(A)) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc6_relat_1,axiom, % 1.59/1.68 ! [A] : % 1.59/1.68 ( ( ~ empty(A) % 1.59/1.68 & relation(A) ) % 1.59/1.68 => ~ empty(relation_rng(A)) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc7_relat_1,axiom, % 1.59/1.68 ! [A] : % 1.59/1.68 ( empty(A) % 1.59/1.68 => ( empty(relation_dom(A)) % 1.59/1.68 & relation(relation_dom(A)) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc8_relat_1,axiom, % 1.59/1.68 ! [A] : % 1.59/1.68 ( empty(A) % 1.59/1.68 => ( empty(relation_rng(A)) % 1.59/1.68 & relation(relation_rng(A)) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(fc9_relat_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ( empty(A) % 1.59/1.68 & relation(B) ) % 1.59/1.68 => ( empty(relation_composition(A,B)) % 1.59/1.68 & relation(relation_composition(A,B)) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(idempotence_k2_xboole_0,axiom, % 1.59/1.68 ! [A,B] : set_union2(A,A) = A ). % 1.59/1.68 % 1.59/1.68 fof(idempotence_k3_xboole_0,axiom, % 1.59/1.68 ! [A,B] : set_intersection2(A,A) = A ). % 1.59/1.68 % 1.59/1.68 fof(involutiveness_k3_subset_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( element(B,powerset(A)) % 1.59/1.68 => subset_complement(A,subset_complement(A,B)) = B ) ). % 1.59/1.68 % 1.59/1.68 fof(involutiveness_k4_relat_1,axiom, % 1.59/1.68 ! [A] : % 1.59/1.68 ( relation(A) % 1.59/1.68 => relation_inverse(relation_inverse(A)) = A ) ). % 1.59/1.68 % 1.59/1.68 fof(involutiveness_k7_setfam_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( element(B,powerset(powerset(A))) % 1.59/1.68 => complements_of_subsets(A,complements_of_subsets(A,B)) = B ) ). % 1.59/1.68 % 1.59/1.68 fof(irreflexivity_r2_xboole_0,axiom, % 1.59/1.68 ! [A,B] : ~ proper_subset(A,A) ). % 1.59/1.68 % 1.59/1.68 fof(l1_zfmisc_1,lemma, % 1.59/1.68 ! [A] : singleton(A) != empty_set ). % 1.59/1.68 % 1.59/1.68 fof(l23_zfmisc_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( in(A,B) % 1.59/1.68 => set_union2(singleton(A),B) = B ) ). % 1.59/1.68 % 1.59/1.68 fof(l25_zfmisc_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ~ ( disjoint(singleton(A),B) % 1.59/1.68 & in(A,B) ) ). % 1.59/1.68 % 1.59/1.68 fof(l28_zfmisc_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ~ in(A,B) % 1.59/1.68 => disjoint(singleton(A),B) ) ). % 1.59/1.68 % 1.59/1.68 fof(l2_zfmisc_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( subset(singleton(A),B) % 1.59/1.68 <=> in(A,B) ) ). % 1.59/1.68 % 1.59/1.68 fof(l32_xboole_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( set_difference(A,B) = empty_set % 1.59/1.68 <=> subset(A,B) ) ). % 1.59/1.68 % 1.59/1.68 fof(l3_subset_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( element(B,powerset(A)) % 1.59/1.68 => ! [C] : % 1.59/1.68 ( in(C,B) % 1.59/1.68 => in(C,A) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(l3_zfmisc_1,lemma, % 1.59/1.68 ! [A,B,C] : % 1.59/1.68 ( subset(A,B) % 1.59/1.68 => ( in(C,A) % 1.59/1.68 | subset(A,set_difference(B,singleton(C))) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(l4_zfmisc_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( subset(A,singleton(B)) % 1.59/1.68 <=> ( A = empty_set % 1.59/1.68 | A = singleton(B) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(l50_zfmisc_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( in(A,B) % 1.59/1.68 => subset(A,union(B)) ) ). % 1.59/1.68 % 1.59/1.68 fof(l55_zfmisc_1,lemma, % 1.59/1.68 ! [A,B,C,D] : % 1.59/1.68 ( in(ordered_pair(A,B),cartesian_product2(C,D)) % 1.59/1.68 <=> ( in(A,C) % 1.59/1.68 & in(B,D) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(l71_subset_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ! [C] : % 1.59/1.68 ( in(C,A) % 1.59/1.68 => in(C,B) ) % 1.59/1.68 => element(A,powerset(B)) ) ). % 1.59/1.68 % 1.59/1.68 fof(l82_funct_1,lemma, % 1.59/1.68 ! [A,B,C] : % 1.59/1.68 ( ( relation(C) % 1.59/1.68 & function(C) ) % 1.59/1.68 => ( in(B,relation_dom(relation_dom_restriction(C,A))) % 1.59/1.68 <=> ( in(B,relation_dom(C)) % 1.59/1.68 & in(B,A) ) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(rc1_funct_1,axiom, % 1.59/1.68 ? [A] : % 1.59/1.68 ( relation(A) % 1.59/1.68 & function(A) ) ). % 1.59/1.68 % 1.59/1.68 fof(rc1_relat_1,axiom, % 1.59/1.68 ? [A] : % 1.59/1.68 ( empty(A) % 1.59/1.68 & relation(A) ) ). % 1.59/1.68 % 1.59/1.68 fof(rc1_subset_1,axiom, % 1.59/1.68 ! [A] : % 1.59/1.68 ( ~ empty(A) % 1.59/1.68 => ? [B] : % 1.59/1.68 ( element(B,powerset(A)) % 1.59/1.68 & ~ empty(B) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(rc1_xboole_0,axiom, % 1.59/1.68 ? [A] : empty(A) ). % 1.59/1.68 % 1.59/1.68 fof(rc2_funct_1,axiom, % 1.59/1.68 ? [A] : % 1.59/1.68 ( relation(A) % 1.59/1.68 & empty(A) % 1.59/1.68 & function(A) ) ). % 1.59/1.68 % 1.59/1.68 fof(rc2_relat_1,axiom, % 1.59/1.68 ? [A] : % 1.59/1.68 ( ~ empty(A) % 1.59/1.68 & relation(A) ) ). % 1.59/1.68 % 1.59/1.68 fof(rc2_subset_1,axiom, % 1.59/1.68 ! [A] : % 1.59/1.68 ? [B] : % 1.59/1.68 ( element(B,powerset(A)) % 1.59/1.68 & empty(B) ) ). % 1.59/1.68 % 1.59/1.68 fof(rc2_xboole_0,axiom, % 1.59/1.68 ? [A] : ~ empty(A) ). % 1.59/1.68 % 1.59/1.68 fof(rc3_funct_1,axiom, % 1.59/1.68 ? [A] : % 1.59/1.68 ( relation(A) % 1.59/1.68 & function(A) % 1.59/1.68 & one_to_one(A) ) ). % 1.59/1.68 % 1.59/1.68 fof(rc3_relat_1,axiom, % 1.59/1.68 ? [A] : % 1.59/1.68 ( relation(A) % 1.59/1.68 & relation_empty_yielding(A) ) ). % 1.59/1.68 % 1.59/1.68 fof(rc4_funct_1,axiom, % 1.59/1.68 ? [A] : % 1.59/1.68 ( relation(A) % 1.59/1.68 & relation_empty_yielding(A) % 1.59/1.68 & function(A) ) ). % 1.59/1.68 % 1.59/1.68 fof(redefinition_k5_setfam_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( element(B,powerset(powerset(A))) % 1.59/1.68 => union_of_subsets(A,B) = union(B) ) ). % 1.59/1.68 % 1.59/1.68 fof(redefinition_k6_setfam_1,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( element(B,powerset(powerset(A))) % 1.59/1.68 => meet_of_subsets(A,B) = set_meet(B) ) ). % 1.59/1.68 % 1.59/1.68 fof(redefinition_k6_subset_1,axiom, % 1.59/1.68 ! [A,B,C] : % 1.59/1.68 ( ( element(B,powerset(A)) % 1.59/1.68 & element(C,powerset(A)) ) % 1.59/1.68 => subset_difference(A,B,C) = set_difference(B,C) ) ). % 1.59/1.68 % 1.59/1.68 fof(reflexivity_r1_tarski,axiom, % 1.59/1.68 ! [A,B] : subset(A,A) ). % 1.59/1.68 % 1.59/1.68 fof(symmetry_r1_xboole_0,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( disjoint(A,B) % 1.59/1.68 => disjoint(B,A) ) ). % 1.59/1.68 % 1.59/1.68 fof(t106_zfmisc_1,lemma, % 1.59/1.68 ! [A,B,C,D] : % 1.59/1.68 ( in(ordered_pair(A,B),cartesian_product2(C,D)) % 1.59/1.68 <=> ( in(A,C) % 1.59/1.68 & in(B,D) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(t10_ordinal1,conjecture, % 1.59/1.68 ! [A] : in(A,succ(A)) ). % 1.59/1.68 % 1.59/1.68 fof(t10_zfmisc_1,lemma, % 1.59/1.68 ! [A,B,C,D] : % 1.59/1.68 ~ ( unordered_pair(A,B) = unordered_pair(C,D) % 1.59/1.68 & A != C % 1.59/1.68 & A != D ) ). % 1.59/1.68 % 1.59/1.68 fof(t115_relat_1,lemma, % 1.59/1.68 ! [A,B,C] : % 1.59/1.68 ( relation(C) % 1.59/1.68 => ( in(A,relation_rng(relation_rng_restriction(B,C))) % 1.59/1.68 <=> ( in(A,B) % 1.59/1.68 & in(A,relation_rng(C)) ) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(t116_relat_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( relation(B) % 1.59/1.68 => subset(relation_rng(relation_rng_restriction(A,B)),A) ) ). % 1.59/1.68 % 1.59/1.68 fof(t117_relat_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( relation(B) % 1.59/1.68 => subset(relation_rng_restriction(A,B),B) ) ). % 1.59/1.68 % 1.59/1.68 fof(t118_relat_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( relation(B) % 1.59/1.68 => subset(relation_rng(relation_rng_restriction(A,B)),relation_rng(B)) ) ). % 1.59/1.68 % 1.59/1.68 fof(t118_zfmisc_1,lemma, % 1.59/1.68 ! [A,B,C] : % 1.59/1.68 ( subset(A,B) % 1.59/1.68 => ( subset(cartesian_product2(A,C),cartesian_product2(B,C)) % 1.59/1.68 & subset(cartesian_product2(C,A),cartesian_product2(C,B)) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(t119_relat_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( relation(B) % 1.59/1.68 => relation_rng(relation_rng_restriction(A,B)) = set_intersection2(relation_rng(B),A) ) ). % 1.59/1.68 % 1.59/1.68 fof(t119_zfmisc_1,lemma, % 1.59/1.68 ! [A,B,C,D] : % 1.59/1.68 ( ( subset(A,B) % 1.59/1.68 & subset(C,D) ) % 1.59/1.68 => subset(cartesian_product2(A,C),cartesian_product2(B,D)) ) ). % 1.59/1.68 % 1.59/1.68 fof(t12_xboole_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( subset(A,B) % 1.59/1.68 => set_union2(A,B) = B ) ). % 1.59/1.68 % 1.59/1.68 fof(t136_zfmisc_1,lemma, % 1.59/1.68 ! [A] : % 1.59/1.68 ? [B] : % 1.59/1.68 ( in(A,B) % 1.59/1.68 & ! [C,D] : % 1.59/1.68 ( ( in(C,B) % 1.59/1.68 & subset(D,C) ) % 1.59/1.68 => in(D,B) ) % 1.59/1.68 & ! [C] : % 1.59/1.68 ( in(C,B) % 1.59/1.68 => in(powerset(C),B) ) % 1.59/1.68 & ! [C] : % 1.59/1.68 ~ ( subset(C,B) % 1.59/1.68 & ~ are_equipotent(C,B) % 1.59/1.68 & ~ in(C,B) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(t140_relat_1,lemma, % 1.59/1.68 ! [A,B,C] : % 1.59/1.68 ( relation(C) % 1.59/1.68 => relation_dom_restriction(relation_rng_restriction(A,C),B) = relation_rng_restriction(A,relation_dom_restriction(C,B)) ) ). % 1.59/1.68 % 1.59/1.68 fof(t143_relat_1,lemma, % 1.59/1.68 ! [A,B,C] : % 1.59/1.68 ( relation(C) % 1.59/1.68 => ( in(A,relation_image(C,B)) % 1.59/1.68 <=> ? [D] : % 1.59/1.68 ( in(D,relation_dom(C)) % 1.59/1.68 & in(ordered_pair(D,A),C) % 1.59/1.68 & in(D,B) ) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(t144_relat_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( relation(B) % 1.59/1.68 => subset(relation_image(B,A),relation_rng(B)) ) ). % 1.59/1.68 % 1.59/1.68 fof(t145_funct_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ( relation(B) % 1.59/1.68 & function(B) ) % 1.59/1.68 => subset(relation_image(B,relation_inverse_image(B,A)),A) ) ). % 1.59/1.68 % 1.59/1.68 fof(t145_relat_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( relation(B) % 1.59/1.68 => relation_image(B,A) = relation_image(B,set_intersection2(relation_dom(B),A)) ) ). % 1.59/1.68 % 1.59/1.68 fof(t146_funct_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( relation(B) % 1.59/1.68 => ( subset(A,relation_dom(B)) % 1.59/1.68 => subset(A,relation_inverse_image(B,relation_image(B,A))) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(t146_relat_1,lemma, % 1.59/1.68 ! [A] : % 1.59/1.68 ( relation(A) % 1.59/1.68 => relation_image(A,relation_dom(A)) = relation_rng(A) ) ). % 1.59/1.68 % 1.59/1.68 fof(t147_funct_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ( relation(B) % 1.59/1.68 & function(B) ) % 1.59/1.68 => ( subset(A,relation_rng(B)) % 1.59/1.68 => relation_image(B,relation_inverse_image(B,A)) = A ) ) ). % 1.59/1.68 % 1.59/1.68 fof(t160_relat_1,lemma, % 1.59/1.68 ! [A] : % 1.59/1.68 ( relation(A) % 1.59/1.68 => ! [B] : % 1.59/1.68 ( relation(B) % 1.59/1.68 => relation_rng(relation_composition(A,B)) = relation_image(B,relation_rng(A)) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(t166_relat_1,lemma, % 1.59/1.68 ! [A,B,C] : % 1.59/1.68 ( relation(C) % 1.59/1.68 => ( in(A,relation_inverse_image(C,B)) % 1.59/1.68 <=> ? [D] : % 1.59/1.68 ( in(D,relation_rng(C)) % 1.59/1.68 & in(ordered_pair(A,D),C) % 1.59/1.68 & in(D,B) ) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(t167_relat_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( relation(B) % 1.59/1.68 => subset(relation_inverse_image(B,A),relation_dom(B)) ) ). % 1.59/1.68 % 1.59/1.68 fof(t174_relat_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( relation(B) % 1.59/1.68 => ~ ( A != empty_set % 1.59/1.68 & subset(A,relation_rng(B)) % 1.59/1.68 & relation_inverse_image(B,A) = empty_set ) ) ). % 1.59/1.68 % 1.59/1.68 fof(t178_relat_1,lemma, % 1.59/1.68 ! [A,B,C] : % 1.59/1.68 ( relation(C) % 1.59/1.68 => ( subset(A,B) % 1.59/1.68 => subset(relation_inverse_image(C,A),relation_inverse_image(C,B)) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(t17_xboole_1,lemma, % 1.59/1.68 ! [A,B] : subset(set_intersection2(A,B),A) ). % 1.59/1.68 % 1.59/1.68 fof(t19_xboole_1,lemma, % 1.59/1.68 ! [A,B,C] : % 1.59/1.68 ( ( subset(A,B) % 1.59/1.68 & subset(A,C) ) % 1.59/1.68 => subset(A,set_intersection2(B,C)) ) ). % 1.59/1.68 % 1.59/1.68 fof(t1_boole,axiom, % 1.59/1.68 ! [A] : set_union2(A,empty_set) = A ). % 1.59/1.68 % 1.59/1.68 fof(t1_subset,axiom, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( in(A,B) % 1.59/1.68 => element(A,B) ) ). % 1.59/1.68 % 1.59/1.68 fof(t1_xboole_1,lemma, % 1.59/1.68 ! [A,B,C] : % 1.59/1.68 ( ( subset(A,B) % 1.59/1.68 & subset(B,C) ) % 1.59/1.68 => subset(A,C) ) ). % 1.59/1.68 % 1.59/1.68 fof(t1_zfmisc_1,lemma, % 1.59/1.68 powerset(empty_set) = singleton(empty_set) ). % 1.59/1.68 % 1.59/1.68 fof(t20_relat_1,lemma, % 1.59/1.68 ! [A,B,C] : % 1.59/1.68 ( relation(C) % 1.59/1.68 => ( in(ordered_pair(A,B),C) % 1.59/1.68 => ( in(A,relation_dom(C)) % 1.59/1.68 & in(B,relation_rng(C)) ) ) ) ). % 1.59/1.68 % 1.59/1.68 fof(t21_funct_1,lemma, % 1.59/1.68 ! [A,B] : % 1.59/1.68 ( ( relation(B) % 1.59/1.68 & function(B) ) % 1.59/1.68 => ! [C] : % 1.59/1.68 ( ( relation(C) % 1.59/1.69 & function(C) ) % 1.59/1.69 => ( in(A,relation_dom(relation_composition(C,B))) % 1.59/1.69 <=> ( in(A,relation_dom(C)) % 1.59/1.69 & in(apply(C,A),relation_dom(B)) ) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t21_relat_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( relation(A) % 1.59/1.69 => subset(A,cartesian_product2(relation_dom(A),relation_rng(A))) ) ). % 1.59/1.69 % 1.59/1.69 fof(t22_funct_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( ( relation(B) % 1.59/1.69 & function(B) ) % 1.59/1.69 => ! [C] : % 1.59/1.69 ( ( relation(C) % 1.59/1.69 & function(C) ) % 1.59/1.69 => ( in(A,relation_dom(relation_composition(C,B))) % 1.59/1.69 => apply(relation_composition(C,B),A) = apply(B,apply(C,A)) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t23_funct_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( ( relation(B) % 1.59/1.69 & function(B) ) % 1.59/1.69 => ! [C] : % 1.59/1.69 ( ( relation(C) % 1.59/1.69 & function(C) ) % 1.59/1.69 => ( in(A,relation_dom(B)) % 1.59/1.69 => apply(relation_composition(B,C),A) = apply(C,apply(B,A)) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t25_relat_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( relation(A) % 1.59/1.69 => ! [B] : % 1.59/1.69 ( relation(B) % 1.59/1.69 => ( subset(A,B) % 1.59/1.69 => ( subset(relation_dom(A),relation_dom(B)) % 1.59/1.69 & subset(relation_rng(A),relation_rng(B)) ) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t26_xboole_1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( subset(A,B) % 1.59/1.69 => subset(set_intersection2(A,C),set_intersection2(B,C)) ) ). % 1.59/1.69 % 1.59/1.69 fof(t28_xboole_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( subset(A,B) % 1.59/1.69 => set_intersection2(A,B) = A ) ). % 1.59/1.69 % 1.59/1.69 fof(t2_boole,axiom, % 1.59/1.69 ! [A] : set_intersection2(A,empty_set) = empty_set ). % 1.59/1.69 % 1.59/1.69 fof(t2_subset,axiom, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( element(A,B) % 1.59/1.69 => ( empty(B) % 1.59/1.69 | in(A,B) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t2_tarski,axiom, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( ! [C] : % 1.59/1.69 ( in(C,A) % 1.59/1.69 <=> in(C,B) ) % 1.59/1.69 => A = B ) ). % 1.59/1.69 % 1.59/1.69 fof(t2_xboole_1,lemma, % 1.59/1.69 ! [A] : subset(empty_set,A) ). % 1.59/1.69 % 1.59/1.69 fof(t30_relat_1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( relation(C) % 1.59/1.69 => ( in(ordered_pair(A,B),C) % 1.59/1.69 => ( in(A,relation_field(C)) % 1.59/1.69 & in(B,relation_field(C)) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t33_xboole_1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( subset(A,B) % 1.59/1.69 => subset(set_difference(A,C),set_difference(B,C)) ) ). % 1.59/1.69 % 1.59/1.69 fof(t33_zfmisc_1,lemma, % 1.59/1.69 ! [A,B,C,D] : % 1.59/1.69 ( ordered_pair(A,B) = ordered_pair(C,D) % 1.59/1.69 => ( A = C % 1.59/1.69 & B = D ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t34_funct_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( ( relation(B) % 1.59/1.69 & function(B) ) % 1.59/1.69 => ( B = identity_relation(A) % 1.59/1.69 <=> ( relation_dom(B) = A % 1.59/1.69 & ! [C] : % 1.59/1.69 ( in(C,A) % 1.59/1.69 => apply(B,C) = C ) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t35_funct_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( in(B,A) % 1.59/1.69 => apply(identity_relation(A),B) = B ) ). % 1.59/1.69 % 1.59/1.69 fof(t36_xboole_1,lemma, % 1.59/1.69 ! [A,B] : subset(set_difference(A,B),A) ). % 1.59/1.69 % 1.59/1.69 fof(t37_relat_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( relation(A) % 1.59/1.69 => ( relation_rng(A) = relation_dom(relation_inverse(A)) % 1.59/1.69 & relation_dom(A) = relation_rng(relation_inverse(A)) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t37_xboole_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( set_difference(A,B) = empty_set % 1.59/1.69 <=> subset(A,B) ) ). % 1.59/1.69 % 1.59/1.69 fof(t37_zfmisc_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( subset(singleton(A),B) % 1.59/1.69 <=> in(A,B) ) ). % 1.59/1.69 % 1.59/1.69 fof(t38_zfmisc_1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( subset(unordered_pair(A,B),C) % 1.59/1.69 <=> ( in(A,C) % 1.59/1.69 & in(B,C) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t39_xboole_1,lemma, % 1.59/1.69 ! [A,B] : set_union2(A,set_difference(B,A)) = set_union2(A,B) ). % 1.59/1.69 % 1.59/1.69 fof(t39_zfmisc_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( subset(A,singleton(B)) % 1.59/1.69 <=> ( A = empty_set % 1.59/1.69 | A = singleton(B) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t3_boole,axiom, % 1.59/1.69 ! [A] : set_difference(A,empty_set) = A ). % 1.59/1.69 % 1.59/1.69 fof(t3_ordinal1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ~ ( in(A,B) % 1.59/1.69 & in(B,C) % 1.59/1.69 & in(C,A) ) ). % 1.59/1.69 % 1.59/1.69 fof(t3_subset,axiom, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( element(A,powerset(B)) % 1.59/1.69 <=> subset(A,B) ) ). % 1.59/1.69 % 1.59/1.69 fof(t3_xboole_0,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( ~ ( ~ disjoint(A,B) % 1.59/1.69 & ! [C] : % 1.59/1.69 ~ ( in(C,A) % 1.59/1.69 & in(C,B) ) ) % 1.59/1.69 & ~ ( ? [C] : % 1.59/1.69 ( in(C,A) % 1.59/1.69 & in(C,B) ) % 1.59/1.69 & disjoint(A,B) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t3_xboole_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( subset(A,empty_set) % 1.59/1.69 => A = empty_set ) ). % 1.59/1.69 % 1.59/1.69 fof(t40_xboole_1,lemma, % 1.59/1.69 ! [A,B] : set_difference(set_union2(A,B),B) = set_difference(A,B) ). % 1.59/1.69 % 1.59/1.69 fof(t43_subset_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( element(B,powerset(A)) % 1.59/1.69 => ! [C] : % 1.59/1.69 ( element(C,powerset(A)) % 1.59/1.69 => ( disjoint(B,C) % 1.59/1.69 <=> subset(B,subset_complement(A,C)) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t44_relat_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( relation(A) % 1.59/1.69 => ! [B] : % 1.59/1.69 ( relation(B) % 1.59/1.69 => subset(relation_dom(relation_composition(A,B)),relation_dom(A)) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t45_relat_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( relation(A) % 1.59/1.69 => ! [B] : % 1.59/1.69 ( relation(B) % 1.59/1.69 => subset(relation_rng(relation_composition(A,B)),relation_rng(B)) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t45_xboole_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( subset(A,B) % 1.59/1.69 => B = set_union2(A,set_difference(B,A)) ) ). % 1.59/1.69 % 1.59/1.69 fof(t46_relat_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( relation(A) % 1.59/1.69 => ! [B] : % 1.59/1.69 ( relation(B) % 1.59/1.69 => ( subset(relation_rng(A),relation_dom(B)) % 1.59/1.69 => relation_dom(relation_composition(A,B)) = relation_dom(A) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t46_setfam_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( element(B,powerset(powerset(A))) % 1.59/1.69 => ~ ( B != empty_set % 1.59/1.69 & complements_of_subsets(A,B) = empty_set ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t46_zfmisc_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( in(A,B) % 1.59/1.69 => set_union2(singleton(A),B) = B ) ). % 1.59/1.69 % 1.59/1.69 fof(t47_relat_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( relation(A) % 1.59/1.69 => ! [B] : % 1.59/1.69 ( relation(B) % 1.59/1.69 => ( subset(relation_dom(A),relation_rng(B)) % 1.59/1.69 => relation_rng(relation_composition(B,A)) = relation_rng(A) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t47_setfam_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( element(B,powerset(powerset(A))) % 1.59/1.69 => ( B != empty_set % 1.59/1.69 => subset_difference(A,cast_to_subset(A),union_of_subsets(A,B)) = meet_of_subsets(A,complements_of_subsets(A,B)) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t48_setfam_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( element(B,powerset(powerset(A))) % 1.59/1.69 => ( B != empty_set % 1.59/1.69 => union_of_subsets(A,complements_of_subsets(A,B)) = subset_difference(A,cast_to_subset(A),meet_of_subsets(A,B)) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t48_xboole_1,lemma, % 1.59/1.69 ! [A,B] : set_difference(A,set_difference(A,B)) = set_intersection2(A,B) ). % 1.59/1.69 % 1.59/1.69 fof(t4_boole,axiom, % 1.59/1.69 ! [A] : set_difference(empty_set,A) = empty_set ). % 1.59/1.69 % 1.59/1.69 fof(t4_subset,axiom, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( ( in(A,B) % 1.59/1.69 & element(B,powerset(C)) ) % 1.59/1.69 => element(A,C) ) ). % 1.59/1.69 % 1.59/1.69 fof(t4_xboole_0,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( ~ ( ~ disjoint(A,B) % 1.59/1.69 & ! [C] : ~ in(C,set_intersection2(A,B)) ) % 1.59/1.69 & ~ ( ? [C] : in(C,set_intersection2(A,B)) % 1.59/1.69 & disjoint(A,B) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t50_subset_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( A != empty_set % 1.59/1.69 => ! [B] : % 1.59/1.69 ( element(B,powerset(A)) % 1.59/1.69 => ! [C] : % 1.59/1.69 ( element(C,A) % 1.59/1.69 => ( ~ in(C,B) % 1.59/1.69 => in(C,subset_complement(A,B)) ) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t54_funct_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( ( relation(A) % 1.59/1.69 & function(A) ) % 1.59/1.69 => ( one_to_one(A) % 1.59/1.69 => ! [B] : % 1.59/1.69 ( ( relation(B) % 1.59/1.69 & function(B) ) % 1.59/1.69 => ( B = function_inverse(A) % 1.59/1.69 <=> ( relation_dom(B) = relation_rng(A) % 1.59/1.69 & ! [C,D] : % 1.59/1.69 ( ( ( in(C,relation_rng(A)) % 1.59/1.69 & D = apply(B,C) ) % 1.59/1.69 => ( in(D,relation_dom(A)) % 1.59/1.69 & C = apply(A,D) ) ) % 1.59/1.69 & ( ( in(D,relation_dom(A)) % 1.59/1.69 & C = apply(A,D) ) % 1.59/1.69 => ( in(C,relation_rng(A)) % 1.59/1.69 & D = apply(B,C) ) ) ) ) ) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t54_subset_1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( element(C,powerset(A)) % 1.59/1.69 => ~ ( in(B,subset_complement(A,C)) % 1.59/1.69 & in(B,C) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t55_funct_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( ( relation(A) % 1.59/1.69 & function(A) ) % 1.59/1.69 => ( one_to_one(A) % 1.59/1.69 => ( relation_rng(A) = relation_dom(function_inverse(A)) % 1.59/1.69 & relation_dom(A) = relation_rng(function_inverse(A)) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t56_relat_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( relation(A) % 1.59/1.69 => ( ! [B,C] : ~ in(ordered_pair(B,C),A) % 1.59/1.69 => A = empty_set ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t57_funct_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( ( relation(B) % 1.59/1.69 & function(B) ) % 1.59/1.69 => ( ( one_to_one(B) % 1.59/1.69 & in(A,relation_rng(B)) ) % 1.59/1.69 => ( A = apply(B,apply(function_inverse(B),A)) % 1.59/1.69 & A = apply(relation_composition(function_inverse(B),B),A) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t5_subset,axiom, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ~ ( in(A,B) % 1.59/1.69 & element(B,powerset(C)) % 1.59/1.69 & empty(C) ) ). % 1.59/1.69 % 1.59/1.69 fof(t60_relat_1,lemma, % 1.59/1.69 ( relation_dom(empty_set) = empty_set % 1.59/1.69 & relation_rng(empty_set) = empty_set ) ). % 1.59/1.69 % 1.59/1.69 fof(t60_xboole_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ~ ( subset(A,B) % 1.59/1.69 & proper_subset(B,A) ) ). % 1.59/1.69 % 1.59/1.69 fof(t62_funct_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( ( relation(A) % 1.59/1.69 & function(A) ) % 1.59/1.69 => ( one_to_one(A) % 1.59/1.69 => one_to_one(function_inverse(A)) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t63_xboole_1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( ( subset(A,B) % 1.59/1.69 & disjoint(B,C) ) % 1.59/1.69 => disjoint(A,C) ) ). % 1.59/1.69 % 1.59/1.69 fof(t64_relat_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( relation(A) % 1.59/1.69 => ( ( relation_dom(A) = empty_set % 1.59/1.69 | relation_rng(A) = empty_set ) % 1.59/1.69 => A = empty_set ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t65_relat_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( relation(A) % 1.59/1.69 => ( relation_dom(A) = empty_set % 1.59/1.69 <=> relation_rng(A) = empty_set ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t65_zfmisc_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( set_difference(A,singleton(B)) = A % 1.59/1.69 <=> ~ in(B,A) ) ). % 1.59/1.69 % 1.59/1.69 fof(t68_funct_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( ( relation(B) % 1.59/1.69 & function(B) ) % 1.59/1.69 => ! [C] : % 1.59/1.69 ( ( relation(C) % 1.59/1.69 & function(C) ) % 1.59/1.69 => ( B = relation_dom_restriction(C,A) % 1.59/1.69 <=> ( relation_dom(B) = set_intersection2(relation_dom(C),A) % 1.59/1.69 & ! [D] : % 1.59/1.69 ( in(D,relation_dom(B)) % 1.59/1.69 => apply(B,D) = apply(C,D) ) ) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t69_enumset1,lemma, % 1.59/1.69 ! [A] : unordered_pair(A,A) = singleton(A) ). % 1.59/1.69 % 1.59/1.69 fof(t6_boole,axiom, % 1.59/1.69 ! [A] : % 1.59/1.69 ( empty(A) % 1.59/1.69 => A = empty_set ) ). % 1.59/1.69 % 1.59/1.69 fof(t6_zfmisc_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( subset(singleton(A),singleton(B)) % 1.59/1.69 => A = B ) ). % 1.59/1.69 % 1.59/1.69 fof(t70_funct_1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( ( relation(C) % 1.59/1.69 & function(C) ) % 1.59/1.69 => ( in(B,relation_dom(relation_dom_restriction(C,A))) % 1.59/1.69 => apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t71_relat_1,lemma, % 1.59/1.69 ! [A] : % 1.59/1.69 ( relation_dom(identity_relation(A)) = A % 1.59/1.69 & relation_rng(identity_relation(A)) = A ) ). % 1.59/1.69 % 1.59/1.69 fof(t72_funct_1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( ( relation(C) % 1.59/1.69 & function(C) ) % 1.59/1.69 => ( in(B,A) % 1.59/1.69 => apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t74_relat_1,lemma, % 1.59/1.69 ! [A,B,C,D] : % 1.59/1.69 ( relation(D) % 1.59/1.69 => ( in(ordered_pair(A,B),relation_composition(identity_relation(C),D)) % 1.59/1.69 <=> ( in(A,C) % 1.59/1.69 & in(ordered_pair(A,B),D) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t7_boole,axiom, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ~ ( in(A,B) % 1.59/1.69 & empty(B) ) ). % 1.59/1.69 % 1.59/1.69 fof(t7_tarski,axiom, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ~ ( in(A,B) % 1.59/1.69 & ! [C] : % 1.59/1.69 ~ ( in(C,B) % 1.59/1.69 & ! [D] : % 1.59/1.69 ~ ( in(D,B) % 1.59/1.69 & in(D,C) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t7_xboole_1,lemma, % 1.59/1.69 ! [A,B] : subset(A,set_union2(A,B)) ). % 1.59/1.69 % 1.59/1.69 fof(t83_xboole_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( disjoint(A,B) % 1.59/1.69 <=> set_difference(A,B) = A ) ). % 1.59/1.69 % 1.59/1.69 fof(t86_relat_1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( relation(C) % 1.59/1.69 => ( in(A,relation_dom(relation_dom_restriction(C,B))) % 1.59/1.69 <=> ( in(A,B) % 1.59/1.69 & in(A,relation_dom(C)) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t88_relat_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( relation(B) % 1.59/1.69 => subset(relation_dom_restriction(B,A),B) ) ). % 1.59/1.69 % 1.59/1.69 fof(t8_boole,axiom, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ~ ( empty(A) % 1.59/1.69 & A != B % 1.59/1.69 & empty(B) ) ). % 1.59/1.69 % 1.59/1.69 fof(t8_funct_1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( ( relation(C) % 1.59/1.69 & function(C) ) % 1.59/1.69 => ( in(ordered_pair(A,B),C) % 1.59/1.69 <=> ( in(A,relation_dom(C)) % 1.59/1.69 & B = apply(C,A) ) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t8_xboole_1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( ( subset(A,B) % 1.59/1.69 & subset(C,B) ) % 1.59/1.69 => subset(set_union2(A,C),B) ) ). % 1.59/1.69 % 1.59/1.69 fof(t8_zfmisc_1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( singleton(A) = unordered_pair(B,C) % 1.59/1.69 => A = B ) ). % 1.59/1.69 % 1.59/1.69 fof(t90_relat_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( relation(B) % 1.59/1.69 => relation_dom(relation_dom_restriction(B,A)) = set_intersection2(relation_dom(B),A) ) ). % 1.59/1.69 % 1.59/1.69 fof(t92_zfmisc_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( in(A,B) % 1.59/1.69 => subset(A,union(B)) ) ). % 1.59/1.69 % 1.59/1.69 fof(t94_relat_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( relation(B) % 1.59/1.69 => relation_dom_restriction(B,A) = relation_composition(identity_relation(A),B) ) ). % 1.59/1.69 % 1.59/1.69 fof(t99_relat_1,lemma, % 1.59/1.69 ! [A,B] : % 1.59/1.69 ( relation(B) % 1.59/1.69 => subset(relation_rng(relation_dom_restriction(B,A)),relation_rng(B)) ) ). % 1.59/1.69 % 1.59/1.69 fof(t99_zfmisc_1,lemma, % 1.59/1.69 ! [A] : union(powerset(A)) = A ). % 1.59/1.69 % 1.59/1.69 fof(t9_tarski,axiom, % 1.59/1.69 ! [A] : % 1.59/1.69 ? [B] : % 1.59/1.69 ( in(A,B) % 1.59/1.69 & ! [C,D] : % 1.59/1.69 ( ( in(C,B) % 1.59/1.69 & subset(D,C) ) % 1.59/1.69 => in(D,B) ) % 1.59/1.69 & ! [C] : % 1.59/1.69 ~ ( in(C,B) % 1.59/1.69 & ! [D] : % 1.59/1.69 ~ ( in(D,B) % 1.59/1.69 & ! [E] : % 1.59/1.69 ( subset(E,C) % 1.59/1.69 => in(E,D) ) ) ) % 1.59/1.69 & ! [C] : % 1.59/1.69 ~ ( subset(C,B) % 1.59/1.69 & ~ are_equipotent(C,B) % 1.59/1.69 & ~ in(C,B) ) ) ). % 1.59/1.69 % 1.59/1.69 fof(t9_zfmisc_1,lemma, % 1.59/1.69 ! [A,B,C] : % 1.59/1.69 ( singleton(A) = unordered_pair(B,C) % 1.59/1.69 => B = C ) ). % 1.59/1.69 % 1.59/1.69 %------------------------------------------------------------------------------ % 1.59/1.69 %------------------------------------------- % 1.59/1.69 % Proof found % 1.59/1.69 % SZS status Theorem for theBenchmark % 1.59/1.69 % SZS output start Proof % 1.59/1.69 %ClaNum:732(EqnAxiom:261) % 1.59/1.69 %VarNum:3596(SingletonVarNum:1049) % 1.59/1.69 %MaxLitNum:11 % 1.59/1.69 %MaxfuncDepth:4 % 1.59/1.69 %SharedTerms:43 % 1.59/1.69 %goalClause: 323 % 1.59/1.69 %singleGoalClaCount:1 % 1.59/1.69 [266]P1(a1) % 1.59/1.69 [267]P1(a6) % 1.59/1.69 [268]P1(a67) % 1.59/1.69 [269]P1(a69) % 1.59/1.69 [270]P5(a7) % 1.59/1.69 [271]P5(a69) % 1.59/1.69 [272]P5(a70) % 1.59/1.69 [273]P5(a75) % 1.59/1.69 [275]P6(a1) % 1.59/1.69 [276]P6(a7) % 1.59/1.69 [277]P6(a6) % 1.59/1.69 [278]P6(a69) % 1.59/1.69 [279]P6(a71) % 1.59/1.69 [280]P6(a70) % 1.59/1.69 [281]P6(a76) % 1.59/1.69 [282]P6(a75) % 1.59/1.69 [283]P7(a70) % 1.59/1.69 [284]P10(a1) % 1.59/1.69 [285]P10(a76) % 1.59/1.69 [286]P10(a75) % 1.59/1.69 [316]~P1(a71) % 1.59/1.69 [317]~P1(a74) % 1.59/1.69 [262]E(f5(a1),a1) % 1.59/1.69 [263]E(f103(a1),a1) % 1.59/1.69 [298]E(f116(a1,a1),f100(a1)) % 1.59/1.69 [323]~P8(a79,f112(a79,f116(a79,a79))) % 1.59/1.69 [295]P11(a1,x2951) % 1.59/1.69 [299]P11(x2991,x2991) % 1.59/1.69 [320]~P9(x3201,x3201) % 1.59/1.69 [287]P1(f72(x2871)) % 1.59/1.69 [288]P5(f77(x2881)) % 1.59/1.69 [290]P6(f77(x2901)) % 1.59/1.69 [294]E(f110(a1,x2941),a1) % 1.59/1.69 [296]E(f112(x2961,a1),x2961) % 1.59/1.69 [297]E(f110(x2971,a1),x2971) % 1.59/1.69 [300]E(f112(x3001,x3001),x3001) % 1.59/1.69 [301]P8(x3011,f78(x3011)) % 1.59/1.69 [302]P8(x3021,f80(x3021)) % 1.59/1.69 [303]P2(x3031,f100(x3031)) % 1.59/1.69 [304]P2(f8(x3041),x3041) % 1.59/1.69 [305]P2(f72(x3051),f100(x3051)) % 1.59/1.69 [318]~P1(f100(x3181)) % 1.59/1.69 [319]~E(f116(x3191,x3191),a1) % 1.59/1.69 [291]E(f5(f77(x2911)),x2911) % 1.59/1.69 [292]E(f109(f100(x2921)),x2921) % 1.59/1.69 [293]E(f103(f77(x2931)),x2931) % 1.59/1.69 [308]E(f110(x3081,f110(x3081,a1)),a1) % 1.59/1.69 [311]E(f110(x3111,f110(x3111,x3111)),x3111) % 1.59/1.69 [324]~P1(f112(x3241,f116(x3241,x3241))) % 1.59/1.69 [306]E(f116(x3061,x3062),f116(x3062,x3061)) % 1.59/1.69 [307]E(f112(x3071,x3072),f112(x3072,x3071)) % 1.59/1.69 [309]P11(x3091,f112(x3091,x3092)) % 1.59/1.69 [310]P11(f110(x3101,x3102),x3101) % 1.59/1.69 [321]~P1(f116(x3211,x3212)) % 1.59/1.69 [312]E(f112(x3121,f110(x3122,x3121)),f112(x3121,x3122)) % 1.59/1.69 [313]E(f110(f112(x3131,x3132),x3132),f110(x3131,x3132)) % 1.59/1.69 [314]E(f110(x3141,f110(x3141,x3142)),f110(x3142,f110(x3142,x3141))) % 1.59/1.69 [326]~P1(x3261)+E(x3261,a1) % 1.59/1.69 [328]~P1(x3281)+P5(x3281) % 1.59/1.69 [329]~P1(x3291)+P6(x3291) % 1.59/1.69 [349]~P11(x3491,a1)+E(x3491,a1) % 1.59/1.69 [334]~P1(x3341)+P1(f5(x3341)) % 1.59/1.69 [335]~P1(x3351)+P1(f103(x3351)) % 1.59/1.69 [336]~P1(x3361)+P1(f104(x3361)) % 1.59/1.69 [337]~P1(x3371)+P6(f5(x3371)) % 1.59/1.69 [338]~P1(x3381)+P6(f103(x3381)) % 1.59/1.69 [339]~P1(x3391)+P6(f104(x3391)) % 1.59/1.69 [340]~P6(x3401)+P6(f104(x3401)) % 1.59/1.69 [346]P1(x3461)+~P1(f68(x3461)) % 1.59/1.69 [350]P8(f9(x3501),x3501)+E(x3501,a1) % 1.59/1.69 [353]P6(x3531)+P8(f10(x3531),x3531) % 1.59/1.69 [363]P1(x3631)+P2(f68(x3631),f100(x3631)) % 1.59/1.69 [343]~P6(x3431)+E(f104(f104(x3431)),x3431) % 1.59/1.69 [347]~P6(x3471)+E(f103(f104(x3471)),f5(x3471)) % 1.59/1.69 [348]~P6(x3481)+E(f5(f104(x3481)),f103(x3481)) % 1.59/1.69 [364]~P6(x3641)+E(f105(x3641,f5(x3641)),f103(x3641)) % 1.59/1.69 [381]~P6(x3811)+E(f112(f5(x3811),f103(x3811)),f107(x3811)) % 1.59/1.69 [477]~P6(x4771)+P11(x4771,f3(f5(x4771),f103(x4771))) % 1.59/1.69 [342]~E(x3421,x3422)+P11(x3421,x3422) % 1.59/1.69 [354]~P8(x3542,x3541)+~E(x3541,a1) % 1.59/1.69 [356]~P9(x3561,x3562)+~E(x3561,x3562) % 1.59/1.69 [362]~P1(x3621)+~P8(x3622,x3621) % 1.59/1.69 [376]~P9(x3761,x3762)+P11(x3761,x3762) % 1.59/1.69 [377]~P8(x3771,x3772)+P2(x3771,x3772) % 1.59/1.69 [378]~P3(x3782,x3781)+P3(x3781,x3782) % 1.59/1.69 [409]~P8(x4092,x4091)+~P8(x4091,x4092) % 1.59/1.69 [410]~P9(x4102,x4101)+~P9(x4101,x4102) % 1.59/1.69 [411]~P11(x4112,x4111)+~P9(x4111,x4112) % 1.59/1.69 [373]~P11(x3731,x3732)+E(f110(x3731,x3732),a1) % 1.59/1.69 [375]P11(x3751,x3752)+~E(f110(x3751,x3752),a1) % 1.59/1.69 [379]~P6(x3791)+P6(f106(x3791,x3792)) % 1.59/1.69 [380]~P6(x3802)+P6(f111(x3801,x3802)) % 1.59/1.69 [382]~P11(x3821,x3822)+E(f112(x3821,x3822),x3822) % 1.59/1.69 [383]~P3(x3831,x3832)+E(f110(x3831,x3832),x3831) % 1.59/1.69 [384]P3(x3841,x3842)+~E(f110(x3841,x3842),x3841) % 1.59/1.69 [394]~E(x3941,a1)+P11(x3941,f116(x3942,x3942)) % 1.59/1.69 [396]~P8(x3961,x3962)+P11(x3961,f109(x3962)) % 1.59/1.69 [397]~P11(x3971,x3972)+P2(x3971,f100(x3972)) % 1.59/1.69 [418]P11(x4181,x4182)+~P2(x4181,f100(x4182)) % 1.59/1.69 [419]~P6(x4191)+P11(f106(x4191,x4192),x4191) % 1.59/1.69 [420]~P6(x4202)+P11(f111(x4201,x4202),x4202) % 1.59/1.69 [425]P1(x4251)+~P1(f112(x4252,x4251)) % 1.59/1.69 [426]P1(x4261)+~P1(f112(x4261,x4262)) % 1.59/1.69 [429]~P6(x4291)+P11(f105(x4291,x4292),f103(x4291)) % 1.59/1.69 [430]~P6(x4301)+P11(f108(x4301,x4302),f5(x4301)) % 1.59/1.69 [431]P8(x4311,x4312)+P3(f116(x4311,x4311),x4312) % 1.59/1.69 [432]P11(x4321,x4322)+P8(f27(x4321,x4322),x4321) % 1.59/1.69 [433]P3(x4331,x4332)+P8(f81(x4331,x4332),x4332) % 1.59/1.69 [434]P3(x4341,x4342)+P8(f81(x4341,x4342),x4341) % 1.59/1.69 [437]P8(f100(x4371),f78(x4372))+~P8(x4371,f78(x4372)) % 1.59/1.69 [445]~P2(x4452,f100(x4451))+E(f114(x4451,x4452),f110(x4451,x4452)) % 1.59/1.69 [447]P8(f66(x4471,x4472),x4471)+P2(x4471,f100(x4472)) % 1.59/1.69 [453]~P8(x4531,x4532)+P8(f87(x4531,x4532),x4532) % 1.59/1.69 [455]~P8(x4551,x4552)+P11(f116(x4551,x4551),x4552) % 1.59/1.69 [491]P11(x4911,x4912)+~P8(f27(x4911,x4912),x4912) % 1.59/1.69 [492]~P8(x4922,f80(x4921))+P8(f98(x4921,x4922),f80(x4921)) % 1.59/1.69 [493]~P2(x4932,f100(x4931))+P2(f114(x4931,x4932),f100(x4931)) % 1.59/1.69 [499]~P8(f66(x4991,x4992),x4992)+P2(x4991,f100(x4992)) % 1.59/1.69 [506]~P8(x5061,x5062)+~P3(f116(x5061,x5061),x5062) % 1.59/1.69 [534]E(x5341,x5342)+~P11(f116(x5341,x5341),f116(x5342,x5342)) % 1.59/1.69 [386]~P6(x3862)+E(f102(f77(x3861),x3862),f106(x3862,x3861)) % 1.59/1.69 [398]~P8(x3982,x3981)+E(f2(f77(x3981),x3982),x3982) % 1.59/1.69 [435]P8(x4352,x4351)+E(f110(x4351,f116(x4352,x4352)),x4351) % 1.59/1.69 [452]~P3(x4521,x4522)+E(f110(x4521,f110(x4521,x4522)),a1) % 1.59/1.69 [459]~P11(x4591,x4592)+E(f112(x4591,f110(x4592,x4591)),x4592) % 1.59/1.69 [460]~P11(x4601,x4602)+E(f110(x4601,f110(x4601,x4602)),x4601) % 1.59/1.69 [462]~P8(x4621,x4622)+E(f112(f116(x4621,x4621),x4622),x4622) % 1.59/1.69 [473]E(f117(x4731,x4732),f109(x4732))+~P2(x4732,f100(f100(x4731))) % 1.59/1.69 [474]E(f101(x4741,x4742),f113(x4742))+~P2(x4742,f100(f100(x4741))) % 1.59/1.69 [478]~P2(x4782,f100(x4781))+E(f114(x4781,f114(x4781,x4782)),x4782) % 1.59/1.69 [486]P3(x4861,x4862)+~E(f110(x4861,f110(x4861,x4862)),a1) % 1.59/1.69 [494]~P6(x4942)+P11(f103(f111(x4941,x4942)),x4941) % 1.59/1.69 [500]~P6(x5001)+P11(f103(f106(x5001,x5002)),f103(x5001)) % 1.59/1.69 [501]~P6(x5012)+P11(f103(f111(x5011,x5012)),f103(x5012)) % 1.59/1.69 [508]~P8(x5082,x5081)+~E(f110(x5081,f116(x5082,x5082)),x5081) % 1.59/1.69 [516]~P2(x5162,f100(f100(x5161)))+E(f4(x5161,f4(x5161,x5162)),x5162) % 1.59/1.69 [525]P2(f117(x5251,x5252),f100(x5251))+~P2(x5252,f100(f100(x5251))) % 1.59/1.69 [526]P2(f101(x5261,x5262),f100(x5261))+~P2(x5262,f100(f100(x5261))) % 1.59/1.69 [540]~P2(x5402,f100(f100(x5401)))+P2(f4(x5401,x5402),f100(f100(x5401))) % 1.59/1.69 [564]P3(x5641,x5642)+P8(f88(x5641,x5642),f110(x5641,f110(x5641,x5642))) % 1.59/1.69 [521]~P6(x5211)+E(f110(f5(x5211),f110(f5(x5211),x5212)),f5(f106(x5211,x5212))) % 1.59/1.69 [522]~P6(x5221)+E(f110(f103(x5221),f110(f103(x5221),x5222)),f103(f111(x5222,x5221))) % 1.59/1.69 [582]~P6(x5821)+E(f105(x5821,f110(f5(x5821),f110(f5(x5821),x5822))),f105(x5821,x5822)) % 1.59/1.69 [416]E(x4161,x4162)+~E(f116(x4163,x4163),f116(x4161,x4162)) % 1.59/1.69 [417]E(x4171,x4172)+~E(f116(x4171,x4171),f116(x4172,x4173)) % 1.59/1.69 [487]P8(x4871,x4872)+~P11(f116(x4873,x4871),x4872) % 1.59/1.69 [488]P8(x4881,x4882)+~P11(f116(x4881,x4883),x4882) % 1.59/1.69 [510]~P11(x5101,x5103)+P11(f3(x5101,x5102),f3(x5103,x5102)) % 1.59/1.69 [511]~P11(x5112,x5113)+P11(f3(x5111,x5112),f3(x5111,x5113)) % 1.59/1.69 [512]~P11(x5121,x5123)+P11(f110(x5121,x5122),f110(x5123,x5122)) % 1.59/1.69 [507]~P6(x5072)+E(f111(x5071,f106(x5072,x5073)),f106(f111(x5071,x5072),x5073)) % 1.59/1.69 [549]P6(x5491)+~E(f10(x5491),f116(f116(x5492,x5493),f116(x5492,x5492))) % 1.59/1.69 [592]~P3(x5921,x5922)+~P8(x5923,f110(x5921,f110(x5921,x5922))) % 1.59/1.69 [604]~P11(x6041,x6043)+P11(f110(x6041,f110(x6041,x6042)),f110(x6043,f110(x6043,x6042))) % 1.59/1.69 [608]E(x6081,x6082)+~E(f116(f116(x6083,x6081),f116(x6083,x6083)),f116(f116(x6084,x6082),f116(x6084,x6084))) % 1.59/1.69 [609]E(x6091,x6092)+~E(f116(f116(x6091,x6093),f116(x6091,x6091)),f116(f116(x6092,x6094),f116(x6092,x6092))) % 1.59/1.69 [647]P8(x6471,x6472)+~P8(f116(f116(x6473,x6471),f116(x6473,x6473)),f3(x6474,x6472)) % 1.59/1.69 [649]P8(x6491,x6492)+~P8(f116(f116(x6491,x6493),f116(x6491,x6491)),f3(x6492,x6494)) % 1.59/1.69 [331]~P6(x3311)+E(x3311,a1)+~E(f5(x3311),a1) % 1.59/1.69 [332]~P6(x3321)+E(x3321,a1)+~E(f103(x3321),a1) % 1.59/1.69 [344]~P6(x3441)+~E(f103(x3441),a1)+E(f5(x3441),a1) % 1.59/1.69 [345]~P6(x3451)+~E(f5(x3451),a1)+E(f103(x3451),a1) % 1.59/1.69 [351]~P5(x3511)+~P6(x3511)+P5(f97(x3511)) % 1.59/1.69 [352]~P5(x3521)+~P6(x3521)+P6(f97(x3521)) % 1.59/1.69 [358]~P6(x3581)+P1(x3581)+~P1(f5(x3581)) % 1.59/1.69 [359]~P6(x3591)+P1(x3591)+~P1(f103(x3591)) % 1.59/1.69 [621]~P6(x6211)+E(x6211,a1)+P8(f116(f116(f93(x6211),f94(x6211)),f116(f93(x6211),f93(x6211))),x6211) % 1.59/1.69 [333]~P1(x3332)+~P1(x3331)+E(x3331,x3332) % 1.59/1.69 [360]~P1(x3602)+~P1(x3601)+P2(x3601,x3602) % 1.59/1.69 [369]~P2(x3691,x3692)+P1(x3691)+~P1(x3692) % 1.59/1.69 [385]P9(x3851,x3852)+~P11(x3851,x3852)+E(x3851,x3852) % 1.59/1.69 [388]~P2(x3882,x3881)+P1(x3881)+P8(x3882,x3881) % 1.59/1.69 [421]~P11(x4212,x4211)+~P11(x4211,x4212)+E(x4211,x4212) % 1.59/1.69 [327]~E(x3272,a1)+~E(x3271,a1)+E(x3271,f113(x3272)) % 1.59/1.69 [330]~E(x3301,f113(x3302))+E(x3301,a1)+~E(x3302,a1) % 1.59/1.69 [399]~P1(x3992)+~P6(x3991)+P1(f102(x3991,x3992)) % 1.59/1.69 [400]~P1(x4001)+~P6(x4002)+P1(f102(x4001,x4002)) % 1.59/1.69 [401]~P5(x4011)+~P6(x4011)+P5(f106(x4011,x4012)) % 1.59/1.69 [402]~P6(x4022)+~P6(x4021)+P6(f112(x4021,x4022)) % 1.59/1.69 [405]~P1(x4052)+~P6(x4051)+P6(f102(x4051,x4052)) % 1.59/1.69 [406]~P1(x4061)+~P6(x4062)+P6(f102(x4061,x4062)) % 1.59/1.69 [407]~P6(x4072)+~P6(x4071)+P6(f102(x4071,x4072)) % 1.59/1.69 [408]~P6(x4081)+~P10(x4081)+P10(f106(x4081,x4082)) % 1.59/1.69 [436]P1(x4361)+P1(x4362)+~P1(f3(x4362,x4361)) % 1.59/1.69 [476]E(f22(x4762,x4761),x4762)+P8(f22(x4762,x4761),x4761)+E(x4761,f116(x4762,x4762)) % 1.59/1.69 [479]P8(x4791,f78(x4792))+P4(x4791,f78(x4792))+~P11(x4791,f78(x4792)) % 1.59/1.69 [480]P8(x4801,f80(x4802))+P4(x4801,f80(x4802))+~P11(x4801,f80(x4802)) % 1.59/1.69 [496]E(x4961,f116(x4962,x4962))+~P11(x4961,f116(x4962,x4962))+E(x4961,a1) % 1.59/1.69 [498]E(x4981,x4982)+P8(f83(x4981,x4982),x4982)+P8(f83(x4981,x4982),x4981) % 1.59/1.69 [504]P8(f28(x5042,x5041),x5041)+P11(f28(x5042,x5041),x5042)+E(x5041,f100(x5042)) % 1.59/1.69 [505]P8(f41(x5052,x5051),x5051)+P8(f48(x5052,x5051),x5052)+E(x5051,f109(x5052)) % 1.59/1.69 [530]~E(f22(x5302,x5301),x5302)+~P8(f22(x5302,x5301),x5301)+E(x5301,f116(x5302,x5302)) % 1.59/1.69 [545]P8(f41(x5452,x5451),x5451)+P8(f41(x5452,x5451),f48(x5452,x5451))+E(x5451,f109(x5452)) % 1.59/1.69 [559]E(x5591,x5592)+~P8(f83(x5591,x5592),x5592)+~P8(f83(x5591,x5592),x5591) % 1.59/1.69 [563]~P8(f28(x5632,x5631),x5631)+~P11(f28(x5632,x5631),x5632)+E(x5631,f100(x5632)) % 1.59/1.69 [465]~P6(x4652)+~P6(x4651)+E(f103(f102(x4651,x4652)),f105(x4652,f103(x4651))) % 1.59/1.69 [485]E(x4851,a1)+~P2(x4851,f100(f100(x4852)))+~E(f4(x4852,x4851),a1) % 1.59/1.69 [517]~P6(x5172)+~P6(x5171)+P11(f5(f102(x5171,x5172)),f5(x5171)) % 1.59/1.69 [518]~P6(x5182)+~P6(x5181)+P11(f103(f102(x5181,x5182)),f103(x5182)) % 1.59/1.69 [524]~P6(x5242)+~P6(x5241)+P6(f110(x5241,f110(x5241,x5242))) % 1.59/1.69 [535]~P5(x5351)+~P6(x5351)+P11(f105(x5351,f108(x5351,x5352)),x5352) % 1.59/1.69 [561]~P6(x5612)+~P11(x5611,f5(x5612))+P11(x5611,f108(x5612,f105(x5612,x5611))) % 1.59/1.69 [594]E(x5941,a1)+~P2(x5941,f100(f100(x5942)))+E(f115(x5942,x5942,f101(x5942,x5941)),f117(x5942,f4(x5942,x5941))) % 1.59/1.69 [595]E(x5951,a1)+~P2(x5951,f100(f100(x5952)))+E(f115(x5952,x5952,f117(x5952,x5951)),f101(x5952,f4(x5952,x5951))) % 1.59/1.69 [657]~P6(x6571)+~P8(x6572,x6571)+E(f116(f116(f18(x6571,x6572),f20(x6571,x6572)),f116(f18(x6571,x6572),f18(x6571,x6572))),x6572) % 1.59/1.69 [441]~P11(x4413,x4412)+P8(x4411,x4412)+~P8(x4411,x4413) % 1.59/1.69 [442]~P11(x4421,x4423)+P11(x4421,x4422)+~P11(x4423,x4422) % 1.59/1.69 [443]~P3(x4433,x4432)+P3(x4431,x4432)+~P11(x4431,x4433) % 1.59/1.69 [466]~P8(x4662,x4663)+~P8(x4661,x4662)+~P8(x4663,x4661) % 1.59/1.69 [467]~P3(x4673,x4672)+~P8(x4671,x4672)+~P8(x4671,x4673) % 1.59/1.69 [412]~P11(x4121,x4123)+P8(x4121,x4122)+~E(x4122,f100(x4123)) % 1.59/1.69 [413]~P8(x4131,x4133)+P11(x4131,x4132)+~E(x4133,f100(x4132)) % 1.59/1.69 [423]~P8(x4231,x4233)+E(x4231,x4232)+~E(x4233,f116(x4232,x4232)) % 1.59/1.69 [451]~P1(x4511)+~P8(x4512,x4513)+~P2(x4513,f100(x4511)) % 1.59/1.69 [471]P8(x4711,x4712)+~P8(x4711,x4713)+~P2(x4713,f100(x4712)) % 1.59/1.69 [472]P2(x4721,x4722)+~P8(x4721,x4723)+~P2(x4723,f100(x4722)) % 1.59/1.69 [481]~P11(x4811,x4813)+P8(x4811,f78(x4812))+~P8(x4813,f78(x4812)) % 1.59/1.69 [482]~P11(x4821,x4823)+P8(x4821,f80(x4822))+~P8(x4823,f80(x4822)) % 1.59/1.69 [502]~P8(x5022,x5023)+~P8(x5021,x5023)+P11(f116(x5021,x5022),x5023) % 1.59/1.69 [503]~P11(x5032,x5033)+~P11(x5031,x5033)+P11(f112(x5031,x5032),x5033) % 1.59/1.69 [520]~P11(x5201,x5203)+~P8(x5203,f80(x5202))+P8(x5201,f98(x5202,x5203)) % 1.59/1.69 [523]~P6(x5231)+~P11(x5232,x5233)+P11(f108(x5231,x5232),f108(x5231,x5233)) % 1.59/1.69 [539]~P8(x5391,x5392)+~P8(x5393,x5392)+~P8(x5393,f87(x5391,x5392)) % 1.59/1.69 [554]~P8(x5541,x5542)+~P8(x5541,f114(x5543,x5542))+~P2(x5542,f100(x5543)) % 1.59/1.69 [566]~P2(x5663,f100(x5661))+~P2(x5662,f100(x5661))+E(f115(x5661,x5662,x5663),f110(x5662,x5663)) % 1.59/1.69 [583]~P8(x5831,x5833)+~E(x5833,f109(x5832))+P8(x5831,f42(x5832,x5833,x5831)) % 1.59/1.69 [584]~P8(x5843,x5842)+~E(x5842,f109(x5841))+P8(f42(x5841,x5842,x5843),x5841) % 1.59/1.69 [601]~P6(x6013)+~P8(x6011,f105(x6013,x6012))+P8(f84(x6011,x6012,x6013),x6012) % 1.59/1.69 [602]~P6(x6023)+~P8(x6021,f108(x6023,x6022))+P8(f85(x6021,x6022,x6023),x6022) % 1.59/1.69 [603]~P2(x6033,f100(x6031))+~P2(x6032,f100(x6031))+P2(f115(x6031,x6032,x6033),f100(x6031)) % 1.59/1.69 [605]~P6(x6053)+~P8(x6051,f105(x6053,x6052))+P8(f84(x6051,x6052,x6053),f5(x6053)) % 1.59/1.69 [606]~P6(x6063)+~P8(x6061,f108(x6063,x6062))+P8(f85(x6061,x6062,x6063),f103(x6063)) % 1.59/1.69 [630]P8(f32(x6302,x6303,x6301),x6301)+P8(f37(x6302,x6303,x6301),x6302)+E(x6301,f3(x6302,x6303)) % 1.59/1.69 [631]P8(f32(x6312,x6313,x6311),x6311)+P8(f38(x6312,x6313,x6311),x6313)+E(x6311,f3(x6312,x6313)) % 1.59/1.69 [632]P8(f51(x6322,x6323,x6321),x6321)+P8(f51(x6322,x6323,x6321),x6322)+E(x6321,f110(x6322,x6323)) % 1.59/1.69 [653]~E(f29(x6532,x6533,x6531),x6533)+~P8(f29(x6532,x6533,x6531),x6531)+E(x6531,f116(x6532,x6533)) % 1.59/1.69 [654]~E(f29(x6542,x6543,x6541),x6542)+~P8(f29(x6542,x6543,x6541),x6541)+E(x6541,f116(x6542,x6543)) % 1.59/1.69 [660]P8(f51(x6602,x6603,x6601),x6601)+~P8(f51(x6602,x6603,x6601),x6603)+E(x6601,f110(x6602,x6603)) % 1.59/1.69 [668]~P8(f33(x6682,x6683,x6681),x6681)+~P8(f33(x6682,x6683,x6681),x6683)+E(x6681,f112(x6682,x6683)) % 1.59/1.69 [669]~P8(f33(x6692,x6693,x6691),x6691)+~P8(f33(x6692,x6693,x6691),x6692)+E(x6691,f112(x6692,x6693)) % 1.59/1.69 [560]~P11(x5602,x5603)+P8(x5601,x5602)+P11(x5602,f110(x5603,f116(x5601,x5601))) % 1.59/1.69 [569]P8(x5691,x5692)+~P6(x5693)+~P8(x5691,f5(f106(x5693,x5692))) % 1.59/1.69 [570]P8(x5701,x5702)+~P6(x5703)+~P8(x5701,f103(f111(x5702,x5703))) % 1.59/1.69 [571]~P11(x5711,x5713)+~P11(x5711,x5712)+P11(x5711,f110(x5712,f110(x5712,x5713))) % 1.59/1.69 [573]~P6(x5732)+P8(x5731,f5(x5732))+~P8(x5731,f5(f106(x5732,x5733))) % 1.59/1.69 [574]~P6(x5742)+P8(x5741,f103(x5742))+~P8(x5741,f103(f111(x5743,x5742))) % 1.59/1.69 [622]~P6(x6222)+P8(x6221,f5(x6222))+~P8(f116(f116(x6221,x6223),f116(x6221,x6221)),x6222) % 1.59/1.69 [623]~P6(x6232)+P8(x6231,f103(x6232))+~P8(f116(f116(x6233,x6231),f116(x6233,x6233)),x6232) % 1.59/1.69 [624]~P6(x6242)+P8(x6241,f107(x6242))+~P8(f116(f116(x6243,x6241),f116(x6243,x6243)),x6242) % 1.59/1.69 [625]~P6(x6252)+P8(x6251,f107(x6252))+~P8(f116(f116(x6251,x6253),f116(x6251,x6251)),x6252) % 1.59/1.69 [650]P8(f43(x6502,x6503,x6501),x6501)+P8(f43(x6502,x6503,x6501),x6503)+E(x6501,f110(x6502,f110(x6502,x6503))) % 1.59/1.69 [651]P8(f43(x6512,x6513,x6511),x6511)+P8(f43(x6512,x6513,x6511),x6512)+E(x6511,f110(x6512,f110(x6512,x6513))) % 1.59/1.69 [697]~P6(x6973)+~P8(x6971,f108(x6973,x6972))+P8(f116(f116(x6971,f85(x6971,x6972,x6973)),f116(x6971,x6971)),x6973) % 1.59/1.69 [704]P8(f32(x7042,x7043,x7041),x7041)+E(x7041,f3(x7042,x7043))+E(f116(f116(f37(x7042,x7043,x7041),f38(x7042,x7043,x7041)),f116(f37(x7042,x7043,x7041),f37(x7042,x7043,x7041))),f32(x7042,x7043,x7041)) % 1.59/1.69 [713]~P6(x7133)+~P8(x7131,f105(x7133,x7132))+P8(f116(f116(f84(x7131,x7132,x7133),x7131),f116(f84(x7131,x7132,x7133),f84(x7131,x7132,x7133))),x7133) % 1.59/1.69 [390]P8(x3901,x3902)+~E(x3901,x3903)+~E(x3902,f116(x3904,x3903)) % 1.59/1.69 [391]P8(x3911,x3912)+~E(x3911,x3913)+~E(x3912,f116(x3913,x3914)) % 1.59/1.69 [422]E(x4221,x4222)+E(x4221,x4223)+~E(f116(x4221,x4224),f116(x4223,x4222)) % 1.59/1.69 [448]~P8(x4481,x4484)+P8(x4481,x4482)+~E(x4482,f112(x4483,x4484)) % 1.59/1.69 [449]~P8(x4491,x4493)+P8(x4491,x4492)+~E(x4492,f112(x4493,x4494)) % 1.59/1.69 [450]~P8(x4501,x4503)+P8(x4501,x4502)+~E(x4503,f110(x4502,x4504)) % 1.59/1.69 [470]~P8(x4704,x4703)+~P8(x4704,x4701)+~E(x4701,f110(x4702,x4703)) % 1.59/1.69 [544]~P11(x5442,x5444)+~P11(x5441,x5443)+P11(f3(x5441,x5442),f3(x5443,x5444)) % 1.59/1.69 [683]~P8(x6834,x6833)+~E(x6833,f3(x6831,x6832))+P8(f35(x6831,x6832,x6833,x6834),x6831) % 1.59/1.69 [684]~P8(x6844,x6843)+~E(x6843,f3(x6841,x6842))+P8(f36(x6841,x6842,x6843,x6844),x6842) % 1.59/1.69 [708]~E(f19(x7082,x7083,x7084,x7081),x7084)+~P8(f19(x7082,x7083,x7084,x7081),x7081)+E(x7081,f118(x7082,x7083,x7084)) % 1.59/1.69 [709]~E(f19(x7092,x7093,x7094,x7091),x7093)+~P8(f19(x7092,x7093,x7094,x7091),x7091)+E(x7091,f118(x7092,x7093,x7094)) % 1.59/1.69 [710]~E(f19(x7102,x7103,x7104,x7101),x7102)+~P8(f19(x7102,x7103,x7104,x7101),x7101)+E(x7101,f118(x7102,x7103,x7104)) % 1.59/1.69 [528]~P8(x5281,x5283)+P8(x5281,x5282)+~E(x5283,f110(x5284,f110(x5284,x5282))) % 1.59/1.69 [614]~P8(x6142,x6144)+~P8(x6141,x6143)+P8(f116(f116(x6141,x6142),f116(x6141,x6141)),f3(x6143,x6144)) % 1.59/1.69 [658]P8(x6581,x6582)+~P6(x6583)+~P8(f116(f116(x6581,x6584),f116(x6581,x6581)),f102(f77(x6582),x6583)) % 1.59/1.69 [676]~P6(x6763)+P8(f116(f116(x6761,x6762),f116(x6761,x6761)),x6763)+~P8(f116(f116(x6761,x6762),f116(x6761,x6761)),f102(f77(x6764),x6763)) % 1.59/1.69 [726]~P8(x7264,x7263)+~E(x7263,f3(x7261,x7262))+E(f116(f116(f35(x7261,x7262,x7263,x7264),f36(x7261,x7262,x7263,x7264)),f116(f35(x7261,x7262,x7263,x7264),f35(x7261,x7262,x7263,x7264))),x7264) % 1.59/1.69 [531]P8(x5311,x5312)+~E(x5311,x5313)+~E(x5312,f118(x5314,x5315,x5313)) % 1.59/1.69 [532]P8(x5321,x5322)+~E(x5321,x5323)+~E(x5322,f118(x5324,x5323,x5325)) % 1.59/1.69 [533]P8(x5331,x5332)+~E(x5331,x5333)+~E(x5332,f118(x5333,x5334,x5335)) % 1.59/1.69 [355]~P1(x3551)+~P5(x3551)+~P6(x3551)+P7(x3551) % 1.59/1.69 [361]~P5(x3611)+~P6(x3611)+~P7(x3611)+E(f97(x3611),f104(x3611)) % 1.59/1.69 [365]~P5(x3651)+~P6(x3651)+P7(x3651)+~E(f26(x3651),f59(x3651)) % 1.59/1.69 [366]~P5(x3661)+~P6(x3661)+~P7(x3661)+P5(f104(x3661)) % 1.59/1.69 [368]~P5(x3681)+~P6(x3681)+~P7(x3681)+P7(f97(x3681)) % 1.59/1.69 [414]~P5(x4141)+~P6(x4141)+P7(x4141)+P8(f26(x4141),f5(x4141)) % 1.59/1.69 [415]~P5(x4151)+~P6(x4151)+P7(x4151)+P8(f59(x4151),f5(x4151)) % 1.59/1.69 [370]~P5(x3701)+~P6(x3701)+~P7(x3701)+E(f103(f97(x3701)),f5(x3701)) % 1.59/1.69 [371]~P5(x3711)+~P6(x3711)+~P7(x3711)+E(f5(f97(x3711)),f103(x3711)) % 1.59/1.69 [440]P7(x4401)+~P5(x4401)+~P6(x4401)+E(f2(x4401,f26(x4401)),f2(x4401,f59(x4401))) % 1.59/1.69 [357]~P5(x3571)+~P6(x3571)+~E(x3571,f77(x3572))+E(f5(x3571),x3572) % 1.59/1.69 [456]~P6(x4562)+~P11(x4561,f103(x4562))+E(x4561,a1)+~E(f108(x4562,x4561),a1) % 1.59/1.69 [457]~P6(x4572)+~P6(x4571)+~P11(x4571,x4572)+P11(f5(x4571),f5(x4572)) % 1.59/1.69 [458]~P6(x4582)+~P6(x4581)+~P11(x4581,x4582)+P11(f103(x4581),f103(x4582)) % 1.59/1.69 [542]P8(f25(x5421,x5422),x5421)+~P8(f23(x5421,x5422),x5422)+E(x5421,a1)+E(x5422,f113(x5421)) % 1.59/1.69 [596]~P8(f23(x5961,x5962),x5962)+~P8(f23(x5961,x5962),f25(x5961,x5962))+E(x5961,a1)+E(x5962,f113(x5961)) % 1.59/1.69 [509]~P5(x5091)+~P6(x5091)+~P11(x5092,f103(x5091))+E(f105(x5091,f108(x5091,x5092)),x5092) % 1.59/1.69 [513]~P6(x5132)+~P6(x5131)+~P11(f103(x5131),f5(x5132))+E(f5(f102(x5131,x5132)),f5(x5131)) % 1.59/1.69 [514]~P6(x5141)+~P6(x5142)+~P11(f5(x5142),f103(x5141))+E(f103(f102(x5141,x5142)),f103(x5142)) % 1.59/1.69 [690]~P6(x6902)+~P6(x6901)+P11(x6901,x6902)+P8(f116(f116(f39(x6901,x6902),f40(x6901,x6902)),f116(f39(x6901,x6902),f39(x6901,x6902))),x6901) % 1.59/1.69 [691]~P6(x6911)+E(f21(x6912,x6911),f34(x6912,x6911))+E(x6911,f77(x6912))+P8(f116(f116(f21(x6912,x6911),f34(x6912,x6911)),f116(f21(x6912,x6911),f21(x6912,x6911))),x6911) % 1.59/1.69 [693]~P6(x6931)+P8(f21(x6932,x6931),x6932)+E(x6931,f77(x6932))+P8(f116(f116(f21(x6932,x6931),f34(x6932,x6931)),f116(f21(x6932,x6931),f21(x6932,x6931))),x6931) % 1.59/1.69 [694]~P6(x6942)+P8(f46(x6942,x6941),x6941)+E(x6941,f5(x6942))+P8(f116(f116(f46(x6942,x6941),f47(x6942,x6941)),f116(f46(x6942,x6941),f46(x6942,x6941))),x6942) % 1.59/1.69 [695]~P6(x6952)+P8(f53(x6952,x6951),x6951)+E(x6951,f103(x6952))+P8(f116(f116(f56(x6952,x6951),f53(x6952,x6951)),f116(f56(x6952,x6951),f56(x6952,x6951))),x6952) % 1.59/1.69 [702]~P6(x7022)+~P6(x7021)+P11(x7021,x7022)+~P8(f116(f116(f39(x7021,x7022),f40(x7021,x7022)),f116(f39(x7021,x7022),f39(x7021,x7022))),x7022) % 1.59/1.69 [558]~P3(x5581,x5583)+~P2(x5583,f100(x5582))+~P2(x5581,f100(x5582))+P11(x5581,f114(x5582,x5583)) % 1.59/1.69 [577]P3(x5771,x5772)+~P11(x5771,f114(x5773,x5772))+~P2(x5772,f100(x5773))+~P2(x5771,f100(x5773)) % 1.59/1.69 [578]P8(x5782,x5783)+P8(f24(x5781,x5783,x5782),x5781)+~E(x5783,f113(x5781))+E(x5781,a1) % 1.59/1.69 [585]~P8(x5853,x5852)+~P8(f41(x5852,x5851),x5853)+~P8(f41(x5852,x5851),x5851)+E(x5851,f109(x5852)) % 1.59/1.69 [612]P8(x6122,x6123)+~E(x6123,f113(x6121))+~P8(x6122,f24(x6121,x6123,x6122))+E(x6121,a1) % 1.59/1.69 [620]E(f29(x6202,x6203,x6201),x6203)+E(f29(x6202,x6203,x6201),x6202)+P8(f29(x6202,x6203,x6201),x6201)+E(x6201,f116(x6202,x6203)) % 1.59/1.69 [636]~P6(x6362)+P8(f11(x6362,x6363,x6361),x6361)+P8(f14(x6362,x6363,x6361),x6363)+E(x6361,f105(x6362,x6363)) % 1.59/1.69 [637]~P6(x6372)+P8(f15(x6372,x6373,x6371),x6371)+P8(f17(x6372,x6373,x6371),x6373)+E(x6371,f108(x6372,x6373)) % 1.59/1.69 [664]P8(f33(x6642,x6643,x6641),x6641)+P8(f33(x6642,x6643,x6641),x6643)+P8(f33(x6642,x6643,x6641),x6642)+E(x6641,f112(x6642,x6643)) % 1.59/1.69 [681]P8(f51(x6812,x6813,x6811),x6813)+~P8(f51(x6812,x6813,x6811),x6811)+~P8(f51(x6812,x6813,x6811),x6812)+E(x6811,f110(x6812,x6813)) % 1.59/1.69 [515]~P5(x5151)+~P6(x5151)+~P8(x5153,x5152)+E(f2(f106(x5151,x5152),x5153),f2(x5151,x5153)) % 1.59/1.69 [567]~P6(x5672)+~P8(x5671,x5673)+~P8(x5671,f5(x5672))+P8(x5671,f5(f106(x5672,x5673))) % 1.59/1.69 [568]~P6(x5683)+~P8(x5681,x5682)+~P8(x5681,f103(x5683))+P8(x5681,f103(f111(x5682,x5683))) % 1.59/1.69 [597]~P5(x5971)+~P6(x5971)+E(f2(f106(x5971,x5972),x5973),f2(x5971,x5973))+~P8(x5973,f5(f106(x5971,x5972))) % 1.59/1.69 [619]P2(f60(x6192,x6193,x6191),f100(x6192))+E(x6191,f4(x6192,x6193))+~P2(x6191,f100(f100(x6192)))+~P2(x6193,f100(f100(x6192))) % 1.59/1.69 [626]~P5(x6262)+~P6(x6262)+E(x6261,f2(x6262,x6263))+~P8(f116(f116(x6263,x6261),f116(x6263,x6263)),x6262) % 1.59/1.69 [679]~P6(x6792)+~P8(f53(x6792,x6791),x6791)+E(x6791,f103(x6792))+~P8(f116(f116(x6793,f53(x6792,x6791)),f116(x6793,x6793)),x6792) % 1.59/1.69 [692]~P6(x6922)+~P8(x6921,x6923)+~E(x6923,f5(x6922))+P8(f116(f116(x6921,f44(x6922,x6923,x6921)),f116(x6921,x6921)),x6922) % 1.59/1.69 [696]~P8(f43(x6962,x6963,x6961),x6961)+~P8(f43(x6962,x6963,x6961),x6963)+~P8(f43(x6962,x6963,x6961),x6962)+E(x6961,f110(x6962,f110(x6962,x6963))) % 1.59/1.69 [700]~P6(x7002)+~P8(f46(x7002,x7001),x7001)+E(x7001,f5(x7002))+~P8(f116(f116(f46(x7002,x7001),x7003),f116(f46(x7002,x7001),f46(x7002,x7001))),x7002) % 1.59/1.69 [712]~P6(x7121)+~P8(x7123,x7122)+~E(x7122,f103(x7121))+P8(f116(f116(f54(x7121,x7122,x7123),x7123),f116(f54(x7121,x7122,x7123),f54(x7121,x7122,x7123))),x7121) % 1.59/1.69 [716]~P6(x7162)+P8(f11(x7162,x7163,x7161),x7161)+E(x7161,f105(x7162,x7163))+P8(f116(f116(f14(x7162,x7163,x7161),f11(x7162,x7163,x7161)),f116(f14(x7162,x7163,x7161),f14(x7162,x7163,x7161))),x7162) % 1.59/1.69 [717]~P6(x7172)+P8(f15(x7172,x7173,x7171),x7171)+E(x7171,f108(x7172,x7173))+P8(f116(f116(f15(x7172,x7173,x7171),f17(x7172,x7173,x7171)),f116(f15(x7172,x7173,x7171),f15(x7172,x7173,x7171))),x7172) % 1.59/1.69 [424]~P8(x4241,x4244)+E(x4241,x4242)+E(x4241,x4243)+~E(x4244,f116(x4243,x4242)) % 1.59/1.69 [468]~P8(x4681,x4684)+P8(x4681,x4682)+~P8(x4684,x4683)+~E(x4682,f109(x4683)) % 1.59/1.69 [483]~P8(x4831,x4834)+P8(x4831,x4832)+P8(x4831,x4833)+~E(x4832,f110(x4834,x4833)) % 1.59/1.69 [484]~P8(x4841,x4844)+P8(x4841,x4842)+P8(x4841,x4843)+~E(x4844,f112(x4843,x4842)) % 1.59/1.69 [685]~P6(x6851)+~P8(x6854,x6853)+~E(x6853,f105(x6851,x6852))+P8(f13(x6851,x6852,x6853,x6854),x6852) % 1.59/1.69 [686]~P6(x6861)+~P8(x6864,x6863)+~E(x6863,f108(x6861,x6862))+P8(f16(x6861,x6862,x6863,x6864),x6862) % 1.59/1.69 [557]~P8(x5571,x5574)+~P8(x5571,x5573)+P8(x5571,x5572)+~E(x5572,f110(x5573,f110(x5573,x5574))) % 1.59/1.69 [618]~P6(x6183)+E(x6181,x6182)+~E(x6183,f77(x6184))+~P8(f116(f116(x6181,x6182),f116(x6181,x6181)),x6183) % 1.59/1.69 [627]~P6(x6273)+P8(x6271,x6272)+~E(x6272,f103(x6273))+~P8(f116(f116(x6274,x6271),f116(x6274,x6274)),x6273) % 1.59/1.69 [628]~P6(x6283)+P8(x6281,x6282)+~E(x6282,f5(x6283))+~P8(f116(f116(x6281,x6284),f116(x6281,x6281)),x6283) % 1.59/1.69 [629]~P6(x6293)+P8(x6291,x6292)+~E(x6293,f77(x6292))+~P8(f116(f116(x6291,x6294),f116(x6291,x6291)),x6293) % 1.59/1.69 [677]~P6(x6774)+~P8(x6771,x6773)+~P8(f116(f116(x6771,x6772),f116(x6771,x6771)),x6774)+P8(f116(f116(x6771,x6772),f116(x6771,x6771)),f102(f77(x6773),x6774)) % 1.59/1.69 [720]~P6(x7202)+~P8(x7201,x7204)+~E(x7204,f108(x7202,x7203))+P8(f116(f116(x7201,f16(x7202,x7203,x7204,x7201)),f116(x7201,x7201)),x7202) % 1.59/1.69 [730]~P6(x7301)+~P8(x7304,x7303)+~E(x7303,f105(x7301,x7302))+P8(f116(f116(f13(x7301,x7302,x7303,x7304),x7304),f116(f13(x7301,x7302,x7303,x7304),f13(x7301,x7302,x7303,x7304))),x7301) % 1.59/1.69 [438]~P5(x4382)+~P5(x4381)+~P6(x4382)+~P6(x4381)+P5(f102(x4381,x4382)) % 1.59/1.69 [469]~P5(x4691)+~P6(x4691)+P8(f82(x4692,x4691),x4692)+~E(f5(x4691),x4692)+E(x4691,f77(x4692)) % 1.59/1.69 [536]~P5(x5362)+~P6(x5362)+P8(f49(x5362,x5361),x5361)+P8(f52(x5362,x5361),f5(x5362))+E(x5361,f103(x5362)) % 1.59/1.69 [546]~P5(x5461)+~P6(x5461)+~E(f5(x5461),x5462)+E(x5461,f77(x5462))+~E(f2(x5461,f82(x5462,x5461)),f82(x5462,x5461)) % 1.59/1.69 [548]~P5(x5482)+~P6(x5482)+P8(f49(x5482,x5481),x5481)+E(x5481,f103(x5482))+E(f2(x5482,f52(x5482,x5481)),f49(x5482,x5481)) % 1.59/1.69 [537]~P5(x5371)+~P6(x5371)+~P7(x5371)+~P8(x5372,f103(x5371))+E(f2(x5371,f2(f97(x5371),x5372)),x5372) % 1.59/1.69 [538]~P5(x5381)+~P6(x5381)+~P7(x5381)+~P8(x5382,f103(x5381))+E(f2(f102(f97(x5381),x5381),x5382),x5382) % 1.59/1.69 [703]~P6(x7031)+~E(f21(x7032,x7031),f34(x7032,x7031))+~P8(f21(x7032,x7031),x7032)+E(x7031,f77(x7032))+~P8(f116(f116(f21(x7032,x7031),f34(x7032,x7031)),f116(f21(x7032,x7031),f21(x7032,x7031))),x7031) % 1.59/1.69 [706]~P6(x7062)+~P6(x7061)+E(x7061,x7062)+P8(f116(f116(f30(x7061,x7062),f31(x7061,x7062)),f116(f30(x7061,x7062),f30(x7061,x7062))),x7062)+P8(f116(f116(f30(x7061,x7062),f31(x7061,x7062)),f116(f30(x7061,x7062),f30(x7061,x7062))),x7061) % 1.59/1.69 [707]~P6(x7071)+~P6(x7072)+E(x7071,f104(x7072))+P8(f116(f116(f57(x7072,x7071),f58(x7072,x7071)),f116(f57(x7072,x7071),f57(x7072,x7071))),x7071)+P8(f116(f116(f58(x7072,x7071),f57(x7072,x7071)),f116(f58(x7072,x7071),f58(x7072,x7071))),x7072) % 1.59/1.69 [714]~P6(x7142)+~P6(x7141)+E(x7141,x7142)+~P8(f116(f116(f30(x7141,x7142),f31(x7141,x7142)),f116(f30(x7141,x7142),f30(x7141,x7142))),x7142)+~P8(f116(f116(f30(x7141,x7142),f31(x7141,x7142)),f116(f30(x7141,x7142),f30(x7141,x7142))),x7141) % 1.59/1.69 [715]~P6(x7151)+~P6(x7152)+E(x7151,f104(x7152))+~P8(f116(f116(f57(x7152,x7151),f58(x7152,x7151)),f116(f57(x7152,x7151),f57(x7152,x7151))),x7151)+~P8(f116(f116(f58(x7152,x7151),f57(x7152,x7151)),f116(f58(x7152,x7151),f58(x7152,x7151))),x7152) % 1.59/1.69 [427]~P5(x4272)+~P6(x4272)+P8(x4273,f5(x4272))+~E(x4271,a1)+E(x4271,f2(x4272,x4273)) % 1.59/1.69 [444]~P5(x4443)+~P6(x4443)+~E(x4441,f2(x4443,x4442))+E(x4441,a1)+P8(x4442,f5(x4443)) % 1.59/1.69 [446]~P5(x4461)+~P6(x4461)+~P8(x4462,x4463)+E(f2(x4461,x4462),x4462)+~E(x4461,f77(x4463)) % 1.59/1.69 [541]~P8(x5413,x5411)+P8(f23(x5411,x5412),x5412)+E(x5411,a1)+E(x5412,f113(x5411))+P8(f23(x5411,x5412),x5413) % 1.59/1.69 [543]~P2(x5432,x5431)+P8(x5432,x5433)+P8(x5432,f114(x5431,x5433))+~P2(x5433,f100(x5431))+E(x5431,a1) % 1.59/1.69 [593]~P5(x5931)+~P6(x5931)+~P8(x5933,x5932)+~E(x5932,f103(x5931))+P8(f50(x5931,x5932,x5933),f5(x5931)) % 1.59/1.69 [641]~P5(x6412)+~P6(x6412)+P8(f73(x6412,x6413,x6411),x6411)+P8(f86(x6412,x6413,x6411),x6413)+E(x6411,f105(x6412,x6413)) % 1.59/1.69 [642]~P5(x6422)+~P6(x6422)+P8(f73(x6422,x6423,x6421),x6421)+P8(f86(x6422,x6423,x6421),f5(x6422))+E(x6421,f105(x6422,x6423)) % 1.59/1.69 [643]~P5(x6432)+~P6(x6432)+P8(f12(x6432,x6433,x6431),x6431)+P8(f12(x6432,x6433,x6431),f5(x6432))+E(x6431,f108(x6432,x6433)) % 1.59/1.69 [591]~P5(x5911)+~P6(x5911)+~P8(x5913,x5912)+~E(x5912,f103(x5911))+E(f2(x5911,f50(x5911,x5912,x5913)),x5913) % 1.59/1.69 [611]~P5(x6113)+~P6(x6113)+~E(x6112,f2(x6113,x6111))+~P8(x6111,f5(x6113))+P8(f116(f116(x6111,x6112),f116(x6111,x6111)),x6113) % 1.59/1.69 [659]~P5(x6592)+~P6(x6592)+P8(f73(x6592,x6593,x6591),x6591)+E(x6591,f105(x6592,x6593))+E(f2(x6592,f86(x6592,x6593,x6591)),f73(x6592,x6593,x6591)) % 1.59/1.69 [670]~P5(x6702)+~P6(x6702)+P8(f12(x6702,x6703,x6701),x6701)+E(x6701,f108(x6702,x6703))+P8(f2(x6702,f12(x6702,x6703,x6701)),x6703) % 1.59/1.69 [680]P8(f60(x6802,x6803,x6801),x6801)+E(x6801,f4(x6802,x6803))+P8(f114(x6802,f60(x6802,x6803,x6801)),x6803)+~P2(x6801,f100(f100(x6802)))+~P2(x6803,f100(f100(x6802))) % 1.59/1.69 [699]~P8(f60(x6992,x6993,x6991),x6991)+E(x6991,f4(x6992,x6993))+~P2(x6991,f100(f100(x6992)))+~P2(x6993,f100(f100(x6992)))+~P8(f114(x6992,f60(x6992,x6993,x6991)),x6993) % 1.59/1.69 [718]~P6(x7181)+~P6(x7182)+P8(f45(x7182,x7183,x7181),x7183)+E(x7181,f106(x7182,x7183))+P8(f116(f116(f45(x7182,x7183,x7181),f55(x7182,x7183,x7181)),f116(f45(x7182,x7183,x7181),f45(x7182,x7183,x7181))),x7181) % 1.59/1.69 [719]~P6(x7191)+~P6(x7193)+P8(f99(x7192,x7193,x7191),x7192)+E(x7191,f111(x7192,x7193))+P8(f116(f116(f96(x7192,x7193,x7191),f99(x7192,x7193,x7191)),f116(f96(x7192,x7193,x7191),f96(x7192,x7193,x7191))),x7191) % 1.59/1.69 [722]~P6(x7221)+~P6(x7222)+E(x7221,f106(x7222,x7223))+P8(f116(f116(f45(x7222,x7223,x7221),f55(x7222,x7223,x7221)),f116(f45(x7222,x7223,x7221),f45(x7222,x7223,x7221))),x7221)+P8(f116(f116(f45(x7222,x7223,x7221),f55(x7222,x7223,x7221)),f116(f45(x7222,x7223,x7221),f45(x7222,x7223,x7221))),x7222) % 1.59/1.69 [723]~P6(x7231)+~P6(x7233)+E(x7231,f111(x7232,x7233))+P8(f116(f116(f96(x7232,x7233,x7231),f99(x7232,x7233,x7231)),f116(f96(x7232,x7233,x7231),f96(x7232,x7233,x7231))),x7231)+P8(f116(f116(f96(x7232,x7233,x7231),f99(x7232,x7233,x7231)),f116(f96(x7232,x7233,x7231),f96(x7232,x7233,x7231))),x7233) % 1.59/1.69 [475]~P8(x4753,x4751)+~P8(x4752,x4754)+P8(x4752,x4753)+E(x4751,a1)+~E(x4754,f113(x4751)) % 1.59/1.69 [497]~P5(x4972)+~P6(x4972)+~P8(x4971,x4973)+P8(x4971,f5(x4972))+~E(x4973,f108(x4972,x4974)) % 1.59/1.69 [527]~P5(x5271)+~P6(x5271)+~P8(x5272,x5274)+P8(f2(x5271,x5272),x5273)+~E(x5274,f108(x5271,x5273)) % 1.59/1.69 [687]~P5(x6871)+~P6(x6871)+~P8(x6874,x6873)+~E(x6873,f105(x6871,x6872))+P8(f61(x6871,x6872,x6873,x6874),x6872) % 1.59/1.69 [689]~P5(x6891)+~P6(x6891)+~P8(x6894,x6893)+~E(x6893,f105(x6891,x6892))+P8(f61(x6891,x6892,x6893,x6894),f5(x6891)) % 1.59/1.69 [711]E(f19(x7112,x7113,x7114,x7111),x7114)+E(f19(x7112,x7113,x7114,x7111),x7113)+E(f19(x7112,x7113,x7114,x7111),x7112)+P8(f19(x7112,x7113,x7114,x7111),x7111)+E(x7111,f118(x7112,x7113,x7114)) % 1.59/1.69 [598]~E(x5981,x5982)+~P6(x5983)+~P8(x5981,x5984)+~E(x5983,f77(x5984))+P8(f116(f116(x5981,x5982),f116(x5981,x5981)),x5983) % 1.59/1.69 [661]~P6(x6612)+~P8(x6614,x6613)+~P8(x6614,f5(x6612))+P8(x6611,f105(x6612,x6613))+~P8(f116(f116(x6614,x6611),f116(x6614,x6614)),x6612) % 1.59/1.69 [662]~P6(x6622)+~P8(x6624,x6623)+~P8(x6624,f103(x6622))+P8(x6621,f108(x6622,x6623))+~P8(f116(f116(x6621,x6624),f116(x6621,x6621)),x6622) % 1.59/1.69 [666]~P6(x6663)+~P6(x6664)+~E(x6663,f104(x6664))+~P8(f116(f116(x6662,x6661),f116(x6662,x6662)),x6664)+P8(f116(f116(x6661,x6662),f116(x6661,x6661)),x6663) % 1.59/1.69 [667]~P6(x6673)+~P6(x6674)+~E(x6674,f104(x6673))+~P8(f116(f116(x6672,x6671),f116(x6672,x6672)),x6674)+P8(f116(f116(x6671,x6672),f116(x6671,x6671)),x6673) % 1.59/1.69 [688]~P5(x6881)+~P6(x6881)+~P8(x6884,x6883)+~E(x6883,f105(x6881,x6882))+E(f2(x6881,f61(x6881,x6882,x6883,x6884)),x6884) % 1.59/1.69 [705]~P6(x7052)+~P8(x7054,x7053)+~P8(f11(x7052,x7053,x7051),x7051)+E(x7051,f105(x7052,x7053))+~P8(f116(f116(x7054,f11(x7052,x7053,x7051)),f116(x7054,x7054)),x7052) % 1.59/1.69 [721]~P6(x7212)+~P8(x7214,x7213)+~P8(f15(x7212,x7213,x7211),x7211)+E(x7211,f108(x7212,x7213))+~P8(f116(f116(f15(x7212,x7213,x7211),x7214),f116(f15(x7212,x7213,x7211),f15(x7212,x7213,x7211))),x7212) % 1.59/1.69 [553]~P8(x5531,x5535)+E(x5531,x5532)+E(x5531,x5533)+E(x5531,x5534)+~E(x5535,f118(x5534,x5533,x5532)) % 1.59/1.69 [644]~P6(x6444)+~P6(x6443)+P8(x6441,x6442)+~E(x6443,f106(x6444,x6442))+~P8(f116(f116(x6441,x6445),f116(x6441,x6441)),x6443) % 1.59/1.69 [645]~P6(x6454)+~P6(x6453)+P8(x6451,x6452)+~E(x6453,f111(x6452,x6454))+~P8(f116(f116(x6455,x6451),f116(x6455,x6455)),x6453) % 1.59/1.69 [655]~P6(x6553)+P8(x6551,x6552)+~P8(x6555,x6554)+~E(x6552,f105(x6553,x6554))+~P8(f116(f116(x6555,x6551),f116(x6555,x6555)),x6553) % 1.59/1.69 [656]~P6(x6563)+P8(x6561,x6562)+~P8(x6565,x6564)+~E(x6562,f108(x6563,x6564))+~P8(f116(f116(x6561,x6565),f116(x6561,x6561)),x6563) % 1.59/1.69 [672]~P6(x6724)+~P6(x6723)+~E(x6724,f106(x6723,x6725))+~P8(f116(f116(x6721,x6722),f116(x6721,x6721)),x6724)+P8(f116(f116(x6721,x6722),f116(x6721,x6721)),x6723) % 1.59/1.69 [673]~P6(x6734)+~P6(x6733)+~E(x6734,f111(x6735,x6733))+~P8(f116(f116(x6731,x6732),f116(x6731,x6731)),x6734)+P8(f116(f116(x6731,x6732),f116(x6731,x6731)),x6733) % 1.59/1.69 [678]~P8(x6785,x6783)+~P8(x6784,x6782)+~P8(f32(x6782,x6783,x6781),x6781)+E(x6781,f3(x6782,x6783))+~E(f32(x6782,x6783,x6781),f116(f116(x6784,x6785),f116(x6784,x6784))) % 1.59/1.69 [600]~P8(x6006,x6004)+~P8(x6005,x6003)+P8(x6001,x6002)+~E(x6002,f3(x6003,x6004))+~E(x6001,f116(f116(x6005,x6006),f116(x6005,x6005))) % 1.59/1.69 [588]~P5(x5882)+~P6(x5882)+~P8(x5883,f5(x5882))+~P8(f49(x5882,x5881),x5881)+~E(f49(x5882,x5881),f2(x5882,x5883))+E(x5881,f103(x5882)) % 1.59/1.69 [572]~P5(x5722)+~P5(x5721)+~P6(x5722)+~P6(x5721)+~P8(x5723,f5(x5721))+E(f2(f102(x5721,x5722),x5723),f2(x5722,f2(x5721,x5723))) % 1.59/1.69 [590]~P5(x5902)+~P6(x5903)+~P6(x5902)+~P5(x5903)+P8(x5901,f5(x5902))+~P8(x5901,f5(f102(x5902,x5903))) % 1.59/1.69 [599]~P5(x5993)+~P5(x5991)+~P6(x5993)+~P6(x5991)+P8(f2(x5991,x5992),f5(x5993))+~P8(x5992,f5(f102(x5991,x5993))) % 1.59/1.69 [616]~P5(x6161)+~P5(x6162)+~P6(x6161)+~P6(x6162)+E(f2(f102(x6161,x6162),x6163),f2(x6162,f2(x6161,x6163)))+~P8(x6163,f5(f102(x6161,x6162))) % 1.59/1.69 [701]~P5(x7012)+~P6(x7012)+~P8(f12(x7012,x7013,x7011),x7011)+~P8(f12(x7012,x7013,x7011),f5(x7012))+E(x7011,f108(x7012,x7013))+~P8(f2(x7012,f12(x7012,x7013,x7011)),x7013) % 1.59/1.69 [550]~P5(x5502)+~P5(x5501)+~P6(x5502)+~P6(x5501)+~E(x5501,f106(x5502,x5503))+E(f5(x5501),f110(f5(x5502),f110(f5(x5502),x5503))) % 1.59/1.69 [724]~P6(x7241)+~P6(x7243)+~P6(x7242)+E(x7241,f102(x7242,x7243))+P8(f116(f116(f62(x7242,x7243,x7241),f64(x7242,x7243,x7241)),f116(f62(x7242,x7243,x7241),f62(x7242,x7243,x7241))),x7241)+P8(f116(f116(f62(x7242,x7243,x7241),f65(x7242,x7243,x7241)),f116(f62(x7242,x7243,x7241),f62(x7242,x7243,x7241))),x7242) % 1.59/1.69 [725]~P6(x7251)+~P6(x7253)+~P6(x7252)+E(x7251,f102(x7252,x7253))+P8(f116(f116(f62(x7252,x7253,x7251),f64(x7252,x7253,x7251)),f116(f62(x7252,x7253,x7251),f62(x7252,x7253,x7251))),x7251)+P8(f116(f116(f65(x7252,x7253,x7251),f64(x7252,x7253,x7251)),f116(f65(x7252,x7253,x7251),f65(x7252,x7253,x7251))),x7253) % 1.59/1.69 [727]~P6(x7271)+~P6(x7272)+~P8(f45(x7272,x7273,x7271),x7273)+E(x7271,f106(x7272,x7273))+~P8(f116(f116(f45(x7272,x7273,x7271),f55(x7272,x7273,x7271)),f116(f45(x7272,x7273,x7271),f45(x7272,x7273,x7271))),x7271)+~P8(f116(f116(f45(x7272,x7273,x7271),f55(x7272,x7273,x7271)),f116(f45(x7272,x7273,x7271),f45(x7272,x7273,x7271))),x7272) % 1.59/1.69 [728]~P6(x7281)+~P6(x7283)+~P8(f99(x7282,x7283,x7281),x7282)+E(x7281,f111(x7282,x7283))+~P8(f116(f116(f96(x7282,x7283,x7281),f99(x7282,x7283,x7281)),f116(f96(x7282,x7283,x7281),f96(x7282,x7283,x7281))),x7281)+~P8(f116(f116(f96(x7282,x7283,x7281),f99(x7282,x7283,x7281)),f116(f96(x7282,x7283,x7281),f96(x7282,x7283,x7281))),x7283) % 1.59/1.69 [519]~P5(x5193)+~P6(x5193)+P8(x5191,x5192)+~P8(x5194,f5(x5193))+~E(x5191,f2(x5193,x5194))+~E(x5192,f103(x5193)) % 1.59/1.69 [580]~P5(x5803)+~P6(x5803)+P8(x5801,x5802)+~P8(x5801,f5(x5803))+~P8(f2(x5803,x5801),x5804)+~E(x5802,f108(x5803,x5804)) % 1.59/1.69 [615]~P8(x6152,x6154)+~P2(x6152,f100(x6151))+P8(f114(x6151,x6152),x6153)+~E(x6154,f4(x6151,x6153))+~P2(x6153,f100(f100(x6151)))+~P2(x6154,f100(f100(x6151))) % 1.59/1.69 [617]P8(x6171,x6172)+~P2(x6171,f100(x6173))+~P8(f114(x6173,x6171),x6174)+~E(x6172,f4(x6173,x6174))+~P2(x6172,f100(f100(x6173)))+~P2(x6174,f100(f100(x6173))) % 1.59/1.69 [674]~P6(x6743)+~P6(x6745)+~P8(x6742,x6744)+~E(x6743,f111(x6744,x6745))+~P8(f116(f116(x6741,x6742),f116(x6741,x6741)),x6745)+P8(f116(f116(x6741,x6742),f116(x6741,x6741)),x6743) % 1.59/1.69 [675]~P6(x6753)+~P6(x6754)+~P8(x6751,x6755)+~E(x6753,f106(x6754,x6755))+~P8(f116(f116(x6751,x6752),f116(x6751,x6751)),x6754)+P8(f116(f116(x6751,x6752),f116(x6751,x6751)),x6753) % 1.59/1.69 [731]~P6(x7314)+~P6(x7313)+~P6(x7312)+~E(x7314,f102(x7312,x7313))+~P8(f116(f116(x7311,x7315),f116(x7311,x7311)),x7314)+P8(f116(f116(x7311,f63(x7312,x7313,x7314,x7311,x7315)),f116(x7311,x7311)),x7312) % 1.59/1.69 [732]~P6(x7323)+~P6(x7322)+~P6(x7321)+~E(x7323,f102(x7321,x7322))+~P8(f116(f116(x7324,x7325),f116(x7324,x7324)),x7323)+P8(f116(f116(f63(x7321,x7322,x7323,x7324,x7325),x7325),f116(f63(x7321,x7322,x7323,x7324,x7325),f63(x7321,x7322,x7323,x7324,x7325))),x7322) % 1.59/1.69 [428]~P5(x4281)+~P5(x4282)+~P6(x4281)+~P6(x4282)+~P7(x4281)+~E(x4282,f97(x4281))+E(f103(x4281),f5(x4282)) % 1.59/1.69 [565]~P5(x5653)+~P6(x5653)+~P7(x5653)+E(x5651,x5652)+~P8(x5652,f5(x5653))+~P8(x5651,f5(x5653))+~E(f2(x5653,x5651),f2(x5653,x5652)) % 1.59/1.69 [607]~P5(x6073)+~P5(x6072)+~P6(x6073)+~P6(x6072)+~P8(x6071,f5(x6072))+~P8(f2(x6072,x6071),f5(x6073))+P8(x6071,f5(f102(x6072,x6073))) % 1.59/1.69 [640]~P5(x6402)+~P5(x6401)+~P6(x6402)+~P6(x6401)+P8(f95(x6403,x6401,x6402),f5(x6401))+E(x6401,f106(x6402,x6403))+~E(f5(x6401),f110(f5(x6402),f110(f5(x6402),x6403))) % 1.59/1.69 [682]~P5(x6822)+~P5(x6821)+~P6(x6822)+~P6(x6821)+E(x6821,f106(x6822,x6823))+~E(f2(x6821,f95(x6823,x6821,x6822)),f2(x6822,f95(x6823,x6821,x6822)))+~E(f5(x6821),f110(f5(x6822),f110(f5(x6822),x6823))) % 1.59/1.69 [547]~P5(x5473)+~P5(x5471)+~P6(x5473)+~P6(x5471)+~P8(x5472,f5(x5471))+E(f2(x5471,x5472),f2(x5473,x5472))+~E(x5471,f106(x5473,x5474)) % 1.59/1.69 [665]~P5(x6652)+~P6(x6652)+~P8(x6654,x6653)+~P8(x6654,f5(x6652))+~P8(f73(x6652,x6653,x6651),x6651)+~E(f73(x6652,x6653,x6651),f2(x6652,x6654))+E(x6651,f105(x6652,x6653)) % 1.59/1.69 [729]~P6(x7291)+~P6(x7293)+~P6(x7292)+E(x7291,f102(x7292,x7293))+~P8(f116(f116(x7294,f64(x7292,x7293,x7291)),f116(x7294,x7294)),x7293)+~P8(f116(f116(f62(x7292,x7293,x7291),x7294),f116(f62(x7292,x7293,x7291),f62(x7292,x7293,x7291))),x7292)+~P8(f116(f116(f62(x7292,x7293,x7291),f64(x7292,x7293,x7291)),f116(f62(x7292,x7293,x7291),f62(x7292,x7293,x7291))),x7291) % 1.59/1.69 [562]~P5(x5623)+~P6(x5623)+~P8(x5625,x5624)+P8(x5621,x5622)+~P8(x5625,f5(x5623))+~E(x5622,f105(x5623,x5624))+~E(x5621,f2(x5623,x5625)) % 1.59/1.69 [698]~P6(x6983)+~P6(x6985)+~P6(x6984)+~E(x6983,f102(x6984,x6985))+~P8(f116(f116(x6981,x6986),f116(x6981,x6981)),x6984)+P8(f116(f116(x6981,x6982),f116(x6981,x6981)),x6983)+~P8(f116(f116(x6986,x6982),f116(x6986,x6986)),x6985) % 1.59/1.69 [579]~P5(x5791)+~P5(x5792)+~P6(x5791)+~P6(x5792)+~P7(x5792)+P8(f89(x5792,x5791),f103(x5792))+P8(f90(x5792,x5791),f5(x5792))+~E(f103(x5792),f5(x5791))+E(x5791,f97(x5792)) % 1.59/1.69 [586]~P5(x5861)+~P5(x5862)+~P6(x5861)+~P6(x5862)+~P7(x5862)+P8(f90(x5862,x5861),f5(x5862))+~E(f103(x5862),f5(x5861))+E(x5861,f97(x5862))+E(f2(x5861,f89(x5862,x5861)),f91(x5862,x5861)) % 1.59/1.69 [587]~P5(x5871)+~P5(x5872)+~P6(x5871)+~P6(x5872)+~P7(x5872)+P8(f89(x5872,x5871),f103(x5872))+~E(f103(x5872),f5(x5871))+E(x5871,f97(x5872))+E(f2(x5872,f90(x5872,x5871)),f92(x5872,x5871)) % 1.59/1.69 [589]~P5(x5891)+~P5(x5892)+~P6(x5891)+~P6(x5892)+~P7(x5892)+~E(f103(x5892),f5(x5891))+E(x5891,f97(x5892))+E(f2(x5891,f89(x5892,x5891)),f91(x5892,x5891))+E(f2(x5892,f90(x5892,x5891)),f92(x5892,x5891)) % 1.59/1.69 [551]~P5(x5514)+~P5(x5512)+~P6(x5514)+~P6(x5512)+~P7(x5512)+~E(x5513,f2(x5514,x5511))+~P8(x5511,f103(x5512))+E(x5511,f2(x5512,x5513))+~E(x5514,f97(x5512)) % 1.59/1.69 [552]~P5(x5524)+~P5(x5522)+~P6(x5524)+~P6(x5522)+~P7(x5524)+~E(x5523,f2(x5524,x5521))+~P8(x5521,f5(x5524))+E(x5521,f2(x5522,x5523))+~E(x5522,f97(x5524)) % 1.59/1.69 [555]~P5(x5553)+~P5(x5552)+~P6(x5553)+~P6(x5552)+~P7(x5552)+~P8(x5554,f103(x5552))+P8(x5551,f5(x5552))+~E(x5551,f2(x5553,x5554))+~E(x5553,f97(x5552)) % 1.59/1.69 [556]~P5(x5563)+~P5(x5562)+~P6(x5563)+~P6(x5562)+~P7(x5562)+~P8(x5564,f5(x5562))+P8(x5561,f103(x5562))+~E(x5561,f2(x5562,x5564))+~E(x5563,f97(x5562)) % 1.59/1.69 [633]~P5(x6331)+~P5(x6332)+~P6(x6331)+~P6(x6332)+~P7(x6332)+P8(f89(x6332,x6331),f103(x6332))+~E(f103(x6332),f5(x6331))+~P8(f92(x6332,x6331),f103(x6332))+E(x6331,f97(x6332))+~E(f2(x6331,f92(x6332,x6331)),f90(x6332,x6331)) % 1.59/1.69 [634]~P5(x6341)+~P5(x6342)+~P6(x6341)+~P6(x6342)+~P7(x6342)+P8(f90(x6342,x6341),f5(x6342))+~E(f103(x6342),f5(x6341))+~P8(f91(x6342,x6341),f5(x6342))+E(x6341,f97(x6342))+~E(f2(x6342,f91(x6342,x6341)),f89(x6342,x6341)) % 1.59/1.69 [638]~P5(x6381)+~P5(x6382)+~P6(x6381)+~P6(x6382)+~P7(x6382)+~E(f103(x6382),f5(x6381))+~P8(f92(x6382,x6381),f103(x6382))+E(x6381,f97(x6382))+E(f2(x6381,f89(x6382,x6381)),f91(x6382,x6381))+~E(f2(x6381,f92(x6382,x6381)),f90(x6382,x6381)) % 1.59/1.69 [639]~P5(x6391)+~P5(x6392)+~P6(x6391)+~P6(x6392)+~P7(x6392)+~E(f103(x6392),f5(x6391))+~P8(f91(x6392,x6391),f5(x6392))+E(x6391,f97(x6392))+E(f2(x6392,f90(x6392,x6391)),f92(x6392,x6391))+~E(f2(x6392,f91(x6392,x6391)),f89(x6392,x6391)) % 1.59/1.69 [663]~P5(x6631)+~P5(x6632)+~P6(x6631)+~P6(x6632)+~P7(x6632)+~E(f103(x6632),f5(x6631))+~P8(f91(x6632,x6631),f5(x6632))+~P8(f92(x6632,x6631),f103(x6632))+E(x6631,f97(x6632))+~E(f2(x6632,f91(x6632,x6631)),f89(x6632,x6631))+~E(f2(x6631,f92(x6632,x6631)),f90(x6632,x6631)) % 1.59/1.69 %EqnAxiom % 1.59/1.69 [1]E(x11,x11) % 1.59/1.69 [2]E(x22,x21)+~E(x21,x22) % 1.59/1.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.59/1.69 [4]~E(x41,x42)+E(f5(x41),f5(x42)) % 1.59/1.69 [5]~E(x51,x52)+E(f103(x51),f103(x52)) % 1.59/1.69 [6]~E(x61,x62)+E(f72(x61),f72(x62)) % 1.59/1.69 [7]~E(x71,x72)+E(f77(x71),f77(x72)) % 1.59/1.69 [8]~E(x81,x82)+E(f14(x81,x83,x84),f14(x82,x83,x84)) % 1.59/1.69 [9]~E(x91,x92)+E(f14(x93,x91,x94),f14(x93,x92,x94)) % 1.59/1.69 [10]~E(x101,x102)+E(f14(x103,x104,x101),f14(x103,x104,x102)) % 1.59/1.69 [11]~E(x111,x112)+E(f116(x111,x113),f116(x112,x113)) % 1.59/1.69 [12]~E(x121,x122)+E(f116(x123,x121),f116(x123,x122)) % 1.59/1.69 [13]~E(x131,x132)+E(f11(x131,x133,x134),f11(x132,x133,x134)) % 1.59/1.69 [14]~E(x141,x142)+E(f11(x143,x141,x144),f11(x143,x142,x144)) % 1.59/1.69 [15]~E(x151,x152)+E(f11(x153,x154,x151),f11(x153,x154,x152)) % 1.59/1.69 [16]~E(x161,x162)+E(f30(x161,x163),f30(x162,x163)) % 1.59/1.69 [17]~E(x171,x172)+E(f30(x173,x171),f30(x173,x172)) % 1.59/1.69 [18]~E(x181,x182)+E(f100(x181),f100(x182)) % 1.59/1.69 [19]~E(x191,x192)+E(f109(x191),f109(x192)) % 1.59/1.69 [20]~E(x201,x202)+E(f57(x201,x203),f57(x202,x203)) % 1.59/1.69 [21]~E(x211,x212)+E(f57(x213,x211),f57(x213,x212)) % 1.59/1.69 [22]~E(x221,x222)+E(f62(x221,x223,x224),f62(x222,x223,x224)) % 1.59/1.69 [23]~E(x231,x232)+E(f62(x233,x231,x234),f62(x233,x232,x234)) % 1.59/1.69 [24]~E(x241,x242)+E(f62(x243,x244,x241),f62(x243,x244,x242)) % 1.59/1.69 [25]~E(x251,x252)+E(f110(x251,x253),f110(x252,x253)) % 1.59/1.69 [26]~E(x261,x262)+E(f110(x263,x261),f110(x263,x262)) % 1.59/1.69 [27]~E(x271,x272)+E(f112(x271,x273),f112(x272,x273)) % 1.59/1.69 [28]~E(x281,x282)+E(f112(x283,x281),f112(x283,x282)) % 1.59/1.69 [29]~E(x291,x292)+E(f38(x291,x293,x294),f38(x292,x293,x294)) % 1.59/1.69 [30]~E(x301,x302)+E(f38(x303,x301,x304),f38(x303,x302,x304)) % 1.59/1.69 [31]~E(x311,x312)+E(f38(x313,x314,x311),f38(x313,x314,x312)) % 1.59/1.69 [32]~E(x321,x322)+E(f18(x321,x323),f18(x322,x323)) % 1.59/1.69 [33]~E(x331,x332)+E(f18(x333,x331),f18(x333,x332)) % 1.59/1.69 [34]~E(x341,x342)+E(f73(x341,x343,x344),f73(x342,x343,x344)) % 1.59/1.69 [35]~E(x351,x352)+E(f73(x353,x351,x354),f73(x353,x352,x354)) % 1.59/1.69 [36]~E(x361,x362)+E(f73(x363,x364,x361),f73(x363,x364,x362)) % 1.59/1.69 [37]~E(x371,x372)+E(f33(x371,x373,x374),f33(x372,x373,x374)) % 1.59/1.69 [38]~E(x381,x382)+E(f33(x383,x381,x384),f33(x383,x382,x384)) % 1.59/1.69 [39]~E(x391,x392)+E(f33(x393,x394,x391),f33(x393,x394,x392)) % 1.59/1.69 [40]~E(x401,x402)+E(f78(x401),f78(x402)) % 1.59/1.69 [41]~E(x411,x412)+E(f80(x411),f80(x412)) % 1.59/1.69 [42]~E(x421,x422)+E(f2(x421,x423),f2(x422,x423)) % 1.59/1.69 [43]~E(x431,x432)+E(f2(x433,x431),f2(x433,x432)) % 1.59/1.69 [44]~E(x441,x442)+E(f8(x441),f8(x442)) % 1.59/1.69 [45]~E(x451,x452)+E(f104(x451),f104(x452)) % 1.59/1.69 [46]~E(x461,x462)+E(f43(x461,x463,x464),f43(x462,x463,x464)) % 1.59/1.69 [47]~E(x471,x472)+E(f43(x473,x471,x474),f43(x473,x472,x474)) % 1.59/1.69 [48]~E(x481,x482)+E(f43(x483,x484,x481),f43(x483,x484,x482)) % 1.59/1.69 [49]~E(x491,x492)+E(f31(x491,x493),f31(x492,x493)) % 1.59/1.69 [50]~E(x501,x502)+E(f31(x503,x501),f31(x503,x502)) % 1.59/1.69 [51]~E(x511,x512)+E(f105(x511,x513),f105(x512,x513)) % 1.59/1.69 [52]~E(x521,x522)+E(f105(x523,x521),f105(x523,x522)) % 1.59/1.69 [53]~E(x531,x532)+E(f61(x531,x533,x534,x535),f61(x532,x533,x534,x535)) % 1.59/1.69 [54]~E(x541,x542)+E(f61(x543,x541,x544,x545),f61(x543,x542,x544,x545)) % 1.59/1.69 [55]~E(x551,x552)+E(f61(x553,x554,x551,x555),f61(x553,x554,x552,x555)) % 1.59/1.69 [56]~E(x561,x562)+E(f61(x563,x564,x565,x561),f61(x563,x564,x565,x562)) % 1.59/1.69 [57]~E(x571,x572)+E(f4(x571,x573),f4(x572,x573)) % 1.59/1.69 [58]~E(x581,x582)+E(f4(x583,x581),f4(x583,x582)) % 1.59/1.69 [59]~E(x591,x592)+E(f32(x591,x593,x594),f32(x592,x593,x594)) % 1.59/1.69 [60]~E(x601,x602)+E(f32(x603,x601,x604),f32(x603,x602,x604)) % 1.59/1.69 [61]~E(x611,x612)+E(f32(x613,x614,x611),f32(x613,x614,x612)) % 1.59/1.69 [62]~E(x621,x622)+E(f3(x621,x623),f3(x622,x623)) % 1.59/1.69 [63]~E(x631,x632)+E(f3(x633,x631),f3(x633,x632)) % 1.59/1.69 [64]~E(x641,x642)+E(f114(x641,x643),f114(x642,x643)) % 1.59/1.69 [65]~E(x651,x652)+E(f114(x653,x651),f114(x653,x652)) % 1.59/1.69 [66]~E(x661,x662)+E(f37(x661,x663,x664),f37(x662,x663,x664)) % 1.59/1.69 [67]~E(x671,x672)+E(f37(x673,x671,x674),f37(x673,x672,x674)) % 1.59/1.69 [68]~E(x681,x682)+E(f37(x683,x684,x681),f37(x683,x684,x682)) % 1.59/1.69 [69]~E(x691,x692)+E(f106(x691,x693),f106(x692,x693)) % 1.59/1.69 [70]~E(x701,x702)+E(f106(x703,x701),f106(x703,x702)) % 1.59/1.69 [71]~E(x711,x712)+E(f21(x711,x713),f21(x712,x713)) % 1.59/1.69 [72]~E(x721,x722)+E(f21(x723,x721),f21(x723,x722)) % 1.59/1.69 [73]~E(x731,x732)+E(f89(x731,x733),f89(x732,x733)) % 1.59/1.69 [74]~E(x741,x742)+E(f89(x743,x741),f89(x743,x742)) % 1.59/1.69 [75]~E(x751,x752)+E(f102(x751,x753),f102(x752,x753)) % 1.59/1.69 [76]~E(x761,x762)+E(f102(x763,x761),f102(x763,x762)) % 1.59/1.69 [77]~E(x771,x772)+E(f51(x771,x773,x774),f51(x772,x773,x774)) % 1.59/1.69 [78]~E(x781,x782)+E(f51(x783,x781,x784),f51(x783,x782,x784)) % 1.59/1.69 [79]~E(x791,x792)+E(f51(x793,x794,x791),f51(x793,x794,x792)) % 1.59/1.69 [80]~E(x801,x802)+E(f117(x801,x803),f117(x802,x803)) % 1.59/1.69 [81]~E(x811,x812)+E(f117(x813,x811),f117(x813,x812)) % 1.59/1.69 [82]~E(x821,x822)+E(f64(x821,x823,x824),f64(x822,x823,x824)) % 1.59/1.69 [83]~E(x831,x832)+E(f64(x833,x831,x834),f64(x833,x832,x834)) % 1.59/1.69 [84]~E(x841,x842)+E(f64(x843,x844,x841),f64(x843,x844,x842)) % 1.59/1.69 [85]~E(x851,x852)+E(f56(x851,x853),f56(x852,x853)) % 1.59/1.69 [86]~E(x861,x862)+E(f56(x863,x861),f56(x863,x862)) % 1.59/1.69 [87]~E(x871,x872)+E(f58(x871,x873),f58(x872,x873)) % 1.59/1.69 [88]~E(x881,x882)+E(f58(x883,x881),f58(x883,x882)) % 1.59/1.69 [89]~E(x891,x892)+E(f45(x891,x893,x894),f45(x892,x893,x894)) % 1.59/1.69 [90]~E(x901,x902)+E(f45(x903,x901,x904),f45(x903,x902,x904)) % 1.59/1.69 [91]~E(x911,x912)+E(f45(x913,x914,x911),f45(x913,x914,x912)) % 1.59/1.69 [92]~E(x921,x922)+E(f35(x921,x923,x924,x925),f35(x922,x923,x924,x925)) % 1.59/1.69 [93]~E(x931,x932)+E(f35(x933,x931,x934,x935),f35(x933,x932,x934,x935)) % 1.59/1.69 [94]~E(x941,x942)+E(f35(x943,x944,x941,x945),f35(x943,x944,x942,x945)) % 1.59/1.69 [95]~E(x951,x952)+E(f35(x953,x954,x955,x951),f35(x953,x954,x955,x952)) % 1.59/1.69 [96]~E(x961,x962)+E(f108(x961,x963),f108(x962,x963)) % 1.59/1.69 [97]~E(x971,x972)+E(f108(x973,x971),f108(x973,x972)) % 1.59/1.69 [98]~E(x981,x982)+E(f12(x981,x983,x984),f12(x982,x983,x984)) % 1.59/1.69 [99]~E(x991,x992)+E(f12(x993,x991,x994),f12(x993,x992,x994)) % 1.59/1.69 [100]~E(x1001,x1002)+E(f12(x1003,x1004,x1001),f12(x1003,x1004,x1002)) % 1.59/1.69 [101]~E(x1011,x1012)+E(f95(x1011,x1013,x1014),f95(x1012,x1013,x1014)) % 1.59/1.69 [102]~E(x1021,x1022)+E(f95(x1023,x1021,x1024),f95(x1023,x1022,x1024)) % 1.59/1.69 [103]~E(x1031,x1032)+E(f95(x1033,x1034,x1031),f95(x1033,x1034,x1032)) % 1.59/1.69 [104]~E(x1041,x1042)+E(f55(x1041,x1043,x1044),f55(x1042,x1043,x1044)) % 1.59/1.69 [105]~E(x1051,x1052)+E(f55(x1053,x1051,x1054),f55(x1053,x1052,x1054)) % 1.59/1.69 [106]~E(x1061,x1062)+E(f55(x1063,x1064,x1061),f55(x1063,x1064,x1062)) % 1.59/1.69 [107]~E(x1071,x1072)+E(f29(x1071,x1073,x1074),f29(x1072,x1073,x1074)) % 1.59/1.69 [108]~E(x1081,x1082)+E(f29(x1083,x1081,x1084),f29(x1083,x1082,x1084)) % 1.59/1.69 [109]~E(x1091,x1092)+E(f29(x1093,x1094,x1091),f29(x1093,x1094,x1092)) % 1.59/1.69 [110]~E(x1101,x1102)+E(f15(x1101,x1103,x1104),f15(x1102,x1103,x1104)) % 1.59/1.69 [111]~E(x1111,x1112)+E(f15(x1113,x1111,x1114),f15(x1113,x1112,x1114)) % 1.59/1.70 [112]~E(x1121,x1122)+E(f15(x1123,x1124,x1121),f15(x1123,x1124,x1122)) % 1.59/1.70 [113]~E(x1131,x1132)+E(f41(x1131,x1133),f41(x1132,x1133)) % 1.59/1.70 [114]~E(x1141,x1142)+E(f41(x1143,x1141),f41(x1143,x1142)) % 1.59/1.70 [115]~E(x1151,x1152)+E(f93(x1151),f93(x1152)) % 1.59/1.70 [116]~E(x1161,x1162)+E(f97(x1161),f97(x1162)) % 1.59/1.70 [117]~E(x1171,x1172)+E(f42(x1171,x1173,x1174),f42(x1172,x1173,x1174)) % 1.59/1.70 [118]~E(x1181,x1182)+E(f42(x1183,x1181,x1184),f42(x1183,x1182,x1184)) % 1.59/1.70 [119]~E(x1191,x1192)+E(f42(x1193,x1194,x1191),f42(x1193,x1194,x1192)) % 1.59/1.70 [120]~E(x1201,x1202)+E(f65(x1201,x1203,x1204),f65(x1202,x1203,x1204)) % 1.59/1.70 [121]~E(x1211,x1212)+E(f65(x1213,x1211,x1214),f65(x1213,x1212,x1214)) % 1.59/1.70 [122]~E(x1221,x1222)+E(f65(x1223,x1224,x1221),f65(x1223,x1224,x1222)) % 1.59/1.70 [123]~E(x1231,x1232)+E(f84(x1231,x1233,x1234),f84(x1232,x1233,x1234)) % 1.59/1.70 [124]~E(x1241,x1242)+E(f84(x1243,x1241,x1244),f84(x1243,x1242,x1244)) % 1.59/1.70 [125]~E(x1251,x1252)+E(f84(x1253,x1254,x1251),f84(x1253,x1254,x1252)) % 1.59/1.70 [126]~E(x1261,x1262)+E(f23(x1261,x1263),f23(x1262,x1263)) % 1.59/1.70 [127]~E(x1271,x1272)+E(f23(x1273,x1271),f23(x1273,x1272)) % 1.59/1.70 [128]~E(x1281,x1282)+E(f98(x1281,x1283),f98(x1282,x1283)) % 1.59/1.70 [129]~E(x1291,x1292)+E(f98(x1293,x1291),f98(x1293,x1292)) % 1.59/1.70 [130]~E(x1301,x1302)+E(f113(x1301),f113(x1302)) % 1.59/1.70 [131]~E(x1311,x1312)+E(f90(x1311,x1313),f90(x1312,x1313)) % 1.59/1.70 [132]~E(x1321,x1322)+E(f90(x1323,x1321),f90(x1323,x1322)) % 1.59/1.70 [133]~E(x1331,x1332)+E(f54(x1331,x1333,x1334),f54(x1332,x1333,x1334)) % 1.59/1.70 [134]~E(x1341,x1342)+E(f54(x1343,x1341,x1344),f54(x1343,x1342,x1344)) % 1.59/1.70 [135]~E(x1351,x1352)+E(f54(x1353,x1354,x1351),f54(x1353,x1354,x1352)) % 1.59/1.70 [136]~E(x1361,x1362)+E(f48(x1361,x1363),f48(x1362,x1363)) % 1.59/1.70 [137]~E(x1371,x1372)+E(f48(x1373,x1371),f48(x1373,x1372)) % 1.59/1.70 [138]~E(x1381,x1382)+E(f28(x1381,x1383),f28(x1382,x1383)) % 1.59/1.70 [139]~E(x1391,x1392)+E(f28(x1393,x1391),f28(x1393,x1392)) % 1.59/1.70 [140]~E(x1401,x1402)+E(f88(x1401,x1403),f88(x1402,x1403)) % 1.59/1.70 [141]~E(x1411,x1412)+E(f88(x1413,x1411),f88(x1413,x1412)) % 1.59/1.70 [142]~E(x1421,x1422)+E(f44(x1421,x1423,x1424),f44(x1422,x1423,x1424)) % 1.59/1.70 [143]~E(x1431,x1432)+E(f44(x1433,x1431,x1434),f44(x1433,x1432,x1434)) % 1.59/1.70 [144]~E(x1441,x1442)+E(f44(x1443,x1444,x1441),f44(x1443,x1444,x1442)) % 1.59/1.70 [145]~E(x1451,x1452)+E(f49(x1451,x1453),f49(x1452,x1453)) % 1.59/1.70 [146]~E(x1461,x1462)+E(f49(x1463,x1461),f49(x1463,x1462)) % 1.59/1.70 [147]~E(x1471,x1472)+E(f19(x1471,x1473,x1474,x1475),f19(x1472,x1473,x1474,x1475)) % 1.59/1.70 [148]~E(x1481,x1482)+E(f19(x1483,x1481,x1484,x1485),f19(x1483,x1482,x1484,x1485)) % 1.59/1.70 [149]~E(x1491,x1492)+E(f19(x1493,x1494,x1491,x1495),f19(x1493,x1494,x1492,x1495)) % 1.59/1.70 [150]~E(x1501,x1502)+E(f19(x1503,x1504,x1505,x1501),f19(x1503,x1504,x1505,x1502)) % 1.59/1.70 [151]~E(x1511,x1512)+E(f22(x1511,x1513),f22(x1512,x1513)) % 1.59/1.70 [152]~E(x1521,x1522)+E(f22(x1523,x1521),f22(x1523,x1522)) % 1.59/1.70 [153]~E(x1531,x1532)+E(f82(x1531,x1533),f82(x1532,x1533)) % 1.59/1.70 [154]~E(x1541,x1542)+E(f82(x1543,x1541),f82(x1543,x1542)) % 1.59/1.70 [155]~E(x1551,x1552)+E(f85(x1551,x1553,x1554),f85(x1552,x1553,x1554)) % 1.59/1.70 [156]~E(x1561,x1562)+E(f85(x1563,x1561,x1564),f85(x1563,x1562,x1564)) % 1.59/1.70 [157]~E(x1571,x1572)+E(f85(x1573,x1574,x1571),f85(x1573,x1574,x1572)) % 1.59/1.70 [158]~E(x1581,x1582)+E(f111(x1581,x1583),f111(x1582,x1583)) % 1.59/1.70 [159]~E(x1591,x1592)+E(f111(x1593,x1591),f111(x1593,x1592)) % 1.59/1.70 [160]~E(x1601,x1602)+E(f17(x1601,x1603,x1604),f17(x1602,x1603,x1604)) % 1.59/1.70 [161]~E(x1611,x1612)+E(f17(x1613,x1611,x1614),f17(x1613,x1612,x1614)) % 1.59/1.70 [162]~E(x1621,x1622)+E(f17(x1623,x1624,x1621),f17(x1623,x1624,x1622)) % 1.59/1.70 [163]~E(x1631,x1632)+E(f96(x1631,x1633,x1634),f96(x1632,x1633,x1634)) % 1.59/1.70 [164]~E(x1641,x1642)+E(f96(x1643,x1641,x1644),f96(x1643,x1642,x1644)) % 1.59/1.70 [165]~E(x1651,x1652)+E(f96(x1653,x1654,x1651),f96(x1653,x1654,x1652)) % 1.59/1.70 [166]~E(x1661,x1662)+E(f13(x1661,x1663,x1664,x1665),f13(x1662,x1663,x1664,x1665)) % 1.59/1.70 [167]~E(x1671,x1672)+E(f13(x1673,x1671,x1674,x1675),f13(x1673,x1672,x1674,x1675)) % 1.59/1.70 [168]~E(x1681,x1682)+E(f13(x1683,x1684,x1681,x1685),f13(x1683,x1684,x1682,x1685)) % 1.59/1.70 [169]~E(x1691,x1692)+E(f13(x1693,x1694,x1695,x1691),f13(x1693,x1694,x1695,x1692)) % 1.59/1.70 [170]~E(x1701,x1702)+E(f86(x1701,x1703,x1704),f86(x1702,x1703,x1704)) % 1.59/1.70 [171]~E(x1711,x1712)+E(f86(x1713,x1711,x1714),f86(x1713,x1712,x1714)) % 1.59/1.70 [172]~E(x1721,x1722)+E(f86(x1723,x1724,x1721),f86(x1723,x1724,x1722)) % 1.59/1.70 [173]~E(x1731,x1732)+E(f68(x1731),f68(x1732)) % 1.59/1.70 [174]~E(x1741,x1742)+E(f99(x1741,x1743,x1744),f99(x1742,x1743,x1744)) % 1.59/1.70 [175]~E(x1751,x1752)+E(f99(x1753,x1751,x1754),f99(x1753,x1752,x1754)) % 1.59/1.70 [176]~E(x1761,x1762)+E(f99(x1763,x1764,x1761),f99(x1763,x1764,x1762)) % 1.59/1.70 [177]~E(x1771,x1772)+E(f101(x1771,x1773),f101(x1772,x1773)) % 1.59/1.70 [178]~E(x1781,x1782)+E(f101(x1783,x1781),f101(x1783,x1782)) % 1.59/1.70 [179]~E(x1791,x1792)+E(f63(x1791,x1793,x1794,x1795,x1796),f63(x1792,x1793,x1794,x1795,x1796)) % 1.59/1.70 [180]~E(x1801,x1802)+E(f63(x1803,x1801,x1804,x1805,x1806),f63(x1803,x1802,x1804,x1805,x1806)) % 1.59/1.70 [181]~E(x1811,x1812)+E(f63(x1813,x1814,x1811,x1815,x1816),f63(x1813,x1814,x1812,x1815,x1816)) % 1.59/1.70 [182]~E(x1821,x1822)+E(f63(x1823,x1824,x1825,x1821,x1826),f63(x1823,x1824,x1825,x1822,x1826)) % 1.59/1.70 [183]~E(x1831,x1832)+E(f63(x1833,x1834,x1835,x1836,x1831),f63(x1833,x1834,x1835,x1836,x1832)) % 1.59/1.70 [184]~E(x1841,x1842)+E(f50(x1841,x1843,x1844),f50(x1842,x1843,x1844)) % 1.59/1.70 [185]~E(x1851,x1852)+E(f50(x1853,x1851,x1854),f50(x1853,x1852,x1854)) % 1.59/1.70 [186]~E(x1861,x1862)+E(f50(x1863,x1864,x1861),f50(x1863,x1864,x1862)) % 1.59/1.70 [187]~E(x1871,x1872)+E(f46(x1871,x1873),f46(x1872,x1873)) % 1.59/1.70 [188]~E(x1881,x1882)+E(f46(x1883,x1881),f46(x1883,x1882)) % 1.59/1.70 [189]~E(x1891,x1892)+E(f60(x1891,x1893,x1894),f60(x1892,x1893,x1894)) % 1.59/1.70 [190]~E(x1901,x1902)+E(f60(x1903,x1901,x1904),f60(x1903,x1902,x1904)) % 1.59/1.70 [191]~E(x1911,x1912)+E(f60(x1913,x1914,x1911),f60(x1913,x1914,x1912)) % 1.59/1.70 [192]~E(x1921,x1922)+E(f9(x1921),f9(x1922)) % 1.59/1.70 [193]~E(x1931,x1932)+E(f25(x1931,x1933),f25(x1932,x1933)) % 1.59/1.70 [194]~E(x1941,x1942)+E(f25(x1943,x1941),f25(x1943,x1942)) % 1.59/1.70 [195]~E(x1951,x1952)+E(f92(x1951,x1953),f92(x1952,x1953)) % 1.59/1.70 [196]~E(x1961,x1962)+E(f92(x1963,x1961),f92(x1963,x1962)) % 1.59/1.70 [197]~E(x1971,x1972)+E(f10(x1971),f10(x1972)) % 1.59/1.70 [198]~E(x1981,x1982)+E(f118(x1981,x1983,x1984),f118(x1982,x1983,x1984)) % 1.59/1.70 [199]~E(x1991,x1992)+E(f118(x1993,x1991,x1994),f118(x1993,x1992,x1994)) % 1.59/1.70 [200]~E(x2001,x2002)+E(f118(x2003,x2004,x2001),f118(x2003,x2004,x2002)) % 1.59/1.70 [201]~E(x2011,x2012)+E(f115(x2011,x2013,x2014),f115(x2012,x2013,x2014)) % 1.59/1.70 [202]~E(x2021,x2022)+E(f115(x2023,x2021,x2024),f115(x2023,x2022,x2024)) % 1.59/1.70 [203]~E(x2031,x2032)+E(f115(x2033,x2034,x2031),f115(x2033,x2034,x2032)) % 1.59/1.70 [204]~E(x2041,x2042)+E(f107(x2041),f107(x2042)) % 1.59/1.70 [205]~E(x2051,x2052)+E(f39(x2051,x2053),f39(x2052,x2053)) % 1.59/1.70 [206]~E(x2061,x2062)+E(f39(x2063,x2061),f39(x2063,x2062)) % 1.59/1.70 [207]~E(x2071,x2072)+E(f53(x2071,x2073),f53(x2072,x2073)) % 1.59/1.70 [208]~E(x2081,x2082)+E(f53(x2083,x2081),f53(x2083,x2082)) % 1.59/1.70 [209]~E(x2091,x2092)+E(f47(x2091,x2093),f47(x2092,x2093)) % 1.59/1.70 [210]~E(x2101,x2102)+E(f47(x2103,x2101),f47(x2103,x2102)) % 1.59/1.70 [211]~E(x2111,x2112)+E(f81(x2111,x2113),f81(x2112,x2113)) % 1.59/1.70 [212]~E(x2121,x2122)+E(f81(x2123,x2121),f81(x2123,x2122)) % 1.59/1.70 [213]~E(x2131,x2132)+E(f59(x2131),f59(x2132)) % 1.59/1.70 [214]~E(x2141,x2142)+E(f34(x2141,x2143),f34(x2142,x2143)) % 1.59/1.70 [215]~E(x2151,x2152)+E(f34(x2153,x2151),f34(x2153,x2152)) % 1.59/1.70 [216]~E(x2161,x2162)+E(f40(x2161,x2163),f40(x2162,x2163)) % 1.59/1.70 [217]~E(x2171,x2172)+E(f40(x2173,x2171),f40(x2173,x2172)) % 1.59/1.70 [218]~E(x2181,x2182)+E(f66(x2181,x2183),f66(x2182,x2183)) % 1.59/1.70 [219]~E(x2191,x2192)+E(f66(x2193,x2191),f66(x2193,x2192)) % 1.59/1.70 [220]~E(x2201,x2202)+E(f26(x2201),f26(x2202)) % 1.59/1.70 [221]~E(x2211,x2212)+E(f91(x2211,x2213),f91(x2212,x2213)) % 1.59/1.70 [222]~E(x2221,x2222)+E(f91(x2223,x2221),f91(x2223,x2222)) % 1.59/1.70 [223]~E(x2231,x2232)+E(f24(x2231,x2233,x2234),f24(x2232,x2233,x2234)) % 1.59/1.70 [224]~E(x2241,x2242)+E(f24(x2243,x2241,x2244),f24(x2243,x2242,x2244)) % 1.59/1.70 [225]~E(x2251,x2252)+E(f24(x2253,x2254,x2251),f24(x2253,x2254,x2252)) % 1.59/1.70 [226]~E(x2261,x2262)+E(f83(x2261,x2263),f83(x2262,x2263)) % 1.59/1.70 [227]~E(x2271,x2272)+E(f83(x2273,x2271),f83(x2273,x2272)) % 1.59/1.70 [228]~E(x2281,x2282)+E(f36(x2281,x2283,x2284,x2285),f36(x2282,x2283,x2284,x2285)) % 1.59/1.70 [229]~E(x2291,x2292)+E(f36(x2293,x2291,x2294,x2295),f36(x2293,x2292,x2294,x2295)) % 1.59/1.70 [230]~E(x2301,x2302)+E(f36(x2303,x2304,x2301,x2305),f36(x2303,x2304,x2302,x2305)) % 1.59/1.70 [231]~E(x2311,x2312)+E(f36(x2313,x2314,x2315,x2311),f36(x2313,x2314,x2315,x2312)) % 1.59/1.70 [232]~E(x2321,x2322)+E(f94(x2321),f94(x2322)) % 1.59/1.70 [233]~E(x2331,x2332)+E(f16(x2331,x2333,x2334,x2335),f16(x2332,x2333,x2334,x2335)) % 1.59/1.70 [234]~E(x2341,x2342)+E(f16(x2343,x2341,x2344,x2345),f16(x2343,x2342,x2344,x2345)) % 1.59/1.70 [235]~E(x2351,x2352)+E(f16(x2353,x2354,x2351,x2355),f16(x2353,x2354,x2352,x2355)) % 1.59/1.70 [236]~E(x2361,x2362)+E(f16(x2363,x2364,x2365,x2361),f16(x2363,x2364,x2365,x2362)) % 1.59/1.70 [237]~E(x2371,x2372)+E(f87(x2371,x2373),f87(x2372,x2373)) % 1.59/1.70 [238]~E(x2381,x2382)+E(f87(x2383,x2381),f87(x2383,x2382)) % 1.59/1.70 [239]~E(x2391,x2392)+E(f27(x2391,x2393),f27(x2392,x2393)) % 1.59/1.70 [240]~E(x2401,x2402)+E(f27(x2403,x2401),f27(x2403,x2402)) % 1.59/1.70 [241]~E(x2411,x2412)+E(f52(x2411,x2413),f52(x2412,x2413)) % 1.59/1.70 [242]~E(x2421,x2422)+E(f52(x2423,x2421),f52(x2423,x2422)) % 1.59/1.70 [243]~E(x2431,x2432)+E(f20(x2431,x2433),f20(x2432,x2433)) % 1.59/1.70 [244]~E(x2441,x2442)+E(f20(x2443,x2441),f20(x2443,x2442)) % 1.59/1.70 [245]~P1(x2451)+P1(x2452)+~E(x2451,x2452) % 1.59/1.70 [246]P8(x2462,x2463)+~E(x2461,x2462)+~P8(x2461,x2463) % 1.59/1.70 [247]P8(x2473,x2472)+~E(x2471,x2472)+~P8(x2473,x2471) % 1.59/1.70 [248]~P6(x2481)+P6(x2482)+~E(x2481,x2482) % 1.59/1.70 [249]~P5(x2491)+P5(x2492)+~E(x2491,x2492) % 1.59/1.70 [250]P2(x2502,x2503)+~E(x2501,x2502)+~P2(x2501,x2503) % 1.59/1.70 [251]P2(x2513,x2512)+~E(x2511,x2512)+~P2(x2513,x2511) % 1.59/1.70 [252]~P7(x2521)+P7(x2522)+~E(x2521,x2522) % 1.59/1.70 [253]P3(x2532,x2533)+~E(x2531,x2532)+~P3(x2531,x2533) % 1.59/1.70 [254]P3(x2543,x2542)+~E(x2541,x2542)+~P3(x2543,x2541) % 1.59/1.70 [255]P11(x2552,x2553)+~E(x2551,x2552)+~P11(x2551,x2553) % 1.59/1.70 [256]P11(x2563,x2562)+~E(x2561,x2562)+~P11(x2563,x2561) % 1.59/1.70 [257]P9(x2572,x2573)+~E(x2571,x2572)+~P9(x2571,x2573) % 1.59/1.70 [258]P9(x2583,x2582)+~E(x2581,x2582)+~P9(x2583,x2581) % 1.59/1.70 [259]~P10(x2591)+P10(x2592)+~E(x2591,x2592) % 1.59/1.70 [260]P4(x2602,x2603)+~E(x2601,x2602)+~P4(x2601,x2603) % 1.59/1.70 [261]P4(x2613,x2612)+~E(x2611,x2612)+~P4(x2613,x2611) % 1.59/1.70 % 1.59/1.70 %------------------------------------------- % 1.59/1.70 cnf(734,plain, % 1.59/1.70 (~P8(x7341,a1)), % 1.59/1.70 inference(equality_inference,[],[354])). % 1.59/1.70 cnf(738,plain, % 1.59/1.70 (~P11(x7381,x7382)+P8(x7381,f100(x7382))), % 1.59/1.70 inference(equality_inference,[],[412])). % 1.59/1.70 cnf(743,plain, % 1.59/1.70 (~P8(x7431,f116(x7432,x7432))+E(x7431,x7432)), % 1.59/1.70 inference(equality_inference,[],[423])). % 1.59/1.70 cnf(749,plain, % 1.59/1.70 (~P8(x7491,x7492)+P8(x7491,f112(x7493,x7492))), % 1.59/1.70 inference(equality_inference,[],[448])). % 1.59/1.70 cnf(750,plain, % 1.59/1.70 (~P8(x7501,x7502)+P8(x7501,f112(x7502,x7503))), % 1.59/1.70 inference(equality_inference,[],[449])). % 1.59/1.70 cnf(751,plain, % 1.59/1.70 (~P8(x7511,f110(x7512,x7513))+P8(x7511,x7512)), % 1.59/1.70 inference(equality_inference,[],[450])). % 1.59/1.70 cnf(752,plain, % 1.59/1.70 (~P8(x7521,x7522)+P8(x7521,f109(x7523))+~P8(x7522,x7523)), % 1.59/1.70 inference(equality_inference,[],[468])). % 1.59/1.70 cnf(754,plain, % 1.59/1.70 (~P8(x7541,x7542)+~P8(x7541,f110(x7543,x7542))), % 1.59/1.70 inference(equality_inference,[],[470])). % 1.59/1.70 cnf(756,plain, % 1.59/1.70 (~P8(x7561,x7562)+P8(x7561,f110(x7562,x7563))+P8(x7561,x7563)), % 1.59/1.70 inference(equality_inference,[],[483])). % 1.59/1.70 cnf(757,plain, % 1.59/1.70 (~P8(x7571,f112(x7572,x7573))+P8(x7571,x7573)+P8(x7571,x7572)), % 1.59/1.70 inference(equality_inference,[],[484])). % 1.59/1.70 cnf(760,plain, % 1.59/1.70 (~P8(x7601,f110(x7602,f110(x7602,x7603)))+P8(x7601,x7603)), % 1.59/1.70 inference(equality_inference,[],[528])). % 1.59/1.70 cnf(769,plain, % 1.59/1.70 (~P8(x7691,f109(x7692))+P8(f42(x7692,f109(x7692),x7691),x7692)), % 1.59/1.70 inference(equality_inference,[],[584])). % 1.59/1.70 cnf(792,plain, % 1.59/1.70 (~P8(x7921,f3(x7922,x7923))+P8(f35(x7922,x7923,f3(x7922,x7923),x7921),x7922)), % 1.59/1.70 inference(equality_inference,[],[683])). % 1.59/1.70 cnf(793,plain, % 1.59/1.70 (~P8(x7931,f3(x7932,x7933))+P8(f36(x7932,x7933,f3(x7932,x7933),x7931),x7933)), % 1.59/1.70 inference(equality_inference,[],[684])). % 1.59/1.70 cnf(808,plain, % 1.59/1.70 (E(f112(x8081,x8081),x8081)), % 1.59/1.70 inference(rename_variables,[],[300])). % 1.59/1.70 cnf(810,plain, % 1.59/1.70 (P8(x8101,f116(x8102,x8101))), % 1.59/1.70 inference(scs_inference,[],[299,300,354,487])). % 1.59/1.70 cnf(811,plain, % 1.59/1.70 (P11(x8111,x8111)), % 1.59/1.70 inference(rename_variables,[],[299])). % 1.59/1.70 cnf(814,plain, % 1.59/1.70 (P11(x8141,x8141)), % 1.59/1.70 inference(rename_variables,[],[299])). % 1.59/1.70 cnf(832,plain, % 1.59/1.70 (~P8(f78(x8321),x8321)), % 1.59/1.70 inference(scs_inference,[],[323,299,811,300,808,301,297,267,308,354,487,488,749,750,751,760,356,362,375,384,409])). % 1.59/1.70 cnf(839,plain, % 1.59/1.70 (~P8(x8391,a1)), % 1.59/1.70 inference(rename_variables,[],[734])). % 1.59/1.70 cnf(842,plain, % 1.59/1.70 (~P8(x8421,a1)), % 1.59/1.70 inference(rename_variables,[],[734])). % 1.59/1.70 cnf(845,plain, % 1.59/1.70 (~P8(x8451,a1)), % 1.59/1.70 inference(rename_variables,[],[734])). % 1.59/1.70 cnf(857,plain, % 1.59/1.70 (P2(f8(x8571),x8571)), % 1.59/1.70 inference(rename_variables,[],[304])). % 1.59/1.70 cnf(867,plain, % 1.59/1.70 (P2(x8671,f100(x8671))), % 1.59/1.70 inference(rename_variables,[],[303])). % 1.59/1.70 cnf(870,plain, % 1.59/1.70 (P2(x8701,f100(x8701))), % 1.59/1.70 inference(rename_variables,[],[303])). % 1.59/1.70 cnf(873,plain, % 1.59/1.70 (P2(x8731,f100(x8731))), % 1.59/1.70 inference(rename_variables,[],[303])). % 1.59/1.70 cnf(881,plain, % 1.59/1.70 (E(f112(x8811,x8811),x8811)), % 1.59/1.70 inference(rename_variables,[],[300])). % 1.59/1.70 cnf(884,plain, % 1.59/1.70 (E(f112(x8841,x8841),x8841)), % 1.59/1.70 inference(rename_variables,[],[300])). % 1.59/1.70 cnf(887,plain, % 1.59/1.70 (E(f112(x8871,x8871),x8871)), % 1.59/1.70 inference(rename_variables,[],[300])). % 1.59/1.70 cnf(893,plain, % 1.59/1.70 (E(f112(x8931,x8931),x8931)), % 1.59/1.70 inference(rename_variables,[],[300])). % 1.59/1.70 cnf(894,plain, % 1.59/1.70 (P8(x8941,f78(x8941))), % 1.59/1.70 inference(rename_variables,[],[301])). % 1.59/1.70 cnf(897,plain, % 1.59/1.70 (E(f112(x8971,x8971),x8971)), % 1.59/1.70 inference(rename_variables,[],[300])). % 1.59/1.70 cnf(900,plain, % 1.59/1.70 (E(f112(x9001,a1),x9001)), % 1.59/1.70 inference(rename_variables,[],[296])). % 1.59/1.70 cnf(903,plain, % 1.59/1.70 (P2(f8(x9031),x9031)), % 1.59/1.70 inference(rename_variables,[],[304])). % 1.59/1.70 cnf(906,plain, % 1.59/1.70 (E(f112(x9061,x9061),x9061)), % 1.59/1.70 inference(rename_variables,[],[300])). % 1.59/1.70 cnf(909,plain, % 1.59/1.70 (E(f112(x9091,x9091),x9091)), % 1.59/1.70 inference(rename_variables,[],[300])). % 1.59/1.70 cnf(912,plain, % 1.59/1.70 (E(f112(x9121,x9121),x9121)), % 1.59/1.70 inference(rename_variables,[],[300])). % 1.59/1.70 cnf(915,plain, % 1.59/1.70 (P8(x9151,f78(x9151))), % 1.59/1.70 inference(rename_variables,[],[301])). % 1.59/1.70 cnf(918,plain, % 1.59/1.70 (P8(x9181,f78(x9181))), % 1.59/1.70 inference(rename_variables,[],[301])). % 1.59/1.70 cnf(923,plain, % 1.59/1.70 (P8(x9231,f78(x9231))), % 1.59/1.70 inference(rename_variables,[],[301])). % 1.59/1.70 cnf(925,plain, % 1.59/1.70 (P8(x9251,f78(x9251))), % 1.59/1.70 inference(rename_variables,[],[301])). % 1.59/1.70 cnf(927,plain, % 1.59/1.70 (E(f112(x9271,x9271),x9271)), % 1.59/1.70 inference(rename_variables,[],[300])). % 1.59/1.70 cnf(930,plain, % 1.59/1.70 (E(f112(x9301,a1),x9301)), % 1.59/1.70 inference(rename_variables,[],[296])). % 1.59/1.70 cnf(936,plain, % 1.59/1.70 (P2(f8(x9361),x9361)), % 1.59/1.70 inference(rename_variables,[],[304])). % 1.59/1.70 cnf(939,plain, % 1.59/1.70 (P8(x9391,f78(x9391))), % 1.59/1.70 inference(rename_variables,[],[301])). % 1.59/1.70 cnf(947,plain, % 1.59/1.70 (~P11(f78(f80(f78(x9471))),x9471)), % 1.59/1.70 inference(scs_inference,[],[323,734,839,842,845,299,811,814,300,808,881,884,887,893,897,906,909,912,927,301,894,915,918,923,925,939,302,303,867,870,873,304,857,903,936,306,309,296,900,930,297,266,267,316,319,308,354,487,488,749,750,751,760,356,362,375,384,409,743,754,769,792,793,2,349,350,353,376,418,432,433,434,473,474,525,526,388,390,391,412,441,448,449,450,471,531,532,533,752,756,757,246,247,330,413,423,451,466,470,472,481])). % 1.59/1.70 cnf(1191,plain, % 1.59/1.70 (~P11(f78(f80(f78(x11911))),x11911)), % 1.59/1.70 inference(rename_variables,[],[947])). % 1.59/1.70 cnf(1198,plain, % 1.59/1.70 ($false), % 1.59/1.70 inference(scs_inference,[],[323,810,832,947,1191,738,394,396,326,749]), % 1.59/1.70 ['proof']). % 1.59/1.70 % SZS output end Proof % 1.59/1.70 % Total time :0.730000s %------------------------------------------------------------------------------