%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU217+2 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n019.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:49 EDT 2024 % Result : Theorem 0.56s 0.91s % Output : CNFRefutation 0.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.15 % Problem : SEU217+2 : TPTP v8.2.0. Released v3.3.0. % 0.08/0.15 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.14/0.37 % Computer : n019.cluster.edu % 0.14/0.37 % Model : x86_64 x86_64 % 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.37 % Memory : 8042.1875MB % 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.37 % CPULimit : 300 % 0.14/0.37 % WCLimit : 300 % 0.14/0.37 % DateTime : Fri Jun 21 11:37:54 EDT 2024 % 0.14/0.37 % CPUTime : % 0.52/0.60 start to proof:theBenchmark % 0.56/0.87 %------------------------------------------- % 0.56/0.87 % File :CSE---1.7 % 0.56/0.87 % Problem :theBenchmark % 0.56/0.87 % Transform :cnf % 0.56/0.87 % Format :tptp:raw % 0.56/0.87 % Command :java -jar mcs_scs.jar %d %s % 0.56/0.87 % 0.56/0.87 % Result :Theorem 0.080000s % 0.56/0.87 % Output :CNFRefutation 0.080000s % 0.56/0.87 %------------------------------------------- % 0.56/0.88 %------------------------------------------------------------------------------ % 0.56/0.88 % File : SEU217+2 : TPTP v8.2.0. Released v3.3.0. % 0.56/0.88 % Domain : Set theory % 0.56/0.88 % Problem : MPTP chainy problem t35_funct_1 % 0.56/0.88 % Version : [Urb07] axioms : Especial. % 0.56/0.88 % English : % 0.56/0.88 % 0.56/0.88 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.56/0.88 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.56/0.88 % Source : [Urb07] % 0.56/0.88 % Names : chainy-t35_funct_1 [Urb07] % 0.56/0.88 % 0.56/0.88 % Status : Theorem % 0.56/0.88 % Rating : 0.22 v8.2.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.17 v7.1.0, 0.13 v6.4.0, 0.15 v6.3.0, 0.21 v6.2.0, 0.28 v6.1.0, 0.40 v6.0.0, 0.39 v5.5.0, 0.41 v5.4.0, 0.43 v5.3.0, 0.48 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.33 v4.1.0, 0.35 v4.0.1, 0.39 v4.0.0, 0.42 v3.7.0, 0.40 v3.5.0, 0.42 v3.3.0 % 0.56/0.88 % Syntax : Number of formulae : 222 ( 52 unt; 0 def) % 0.56/0.88 % Number of atoms : 592 ( 128 equ) % 0.56/0.88 % Maximal formula atoms : 11 ( 2 avg) % 0.56/0.88 % Number of connectives : 438 ( 68 ~; 7 |; 116 &) % 0.56/0.88 % ( 75 <=>; 172 =>; 0 <=; 0 <~>) % 0.56/0.88 % Maximal formula depth : 14 ( 5 avg) % 0.56/0.88 % Maximal term depth : 4 ( 1 avg) % 0.56/0.88 % Number of predicates : 12 ( 10 usr; 1 prp; 0-2 aty) % 0.56/0.88 % Number of functors : 28 ( 28 usr; 1 con; 0-3 aty) % 0.56/0.88 % Number of variables : 476 ( 453 !; 23 ?) % 0.56/0.88 % SPC : FOF_THM_RFO_SEQ % 0.56/0.88 % 0.56/0.88 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.56/0.88 % library, www.mizar.org % 0.56/0.88 %------------------------------------------------------------------------------ % 0.56/0.88 fof(antisymmetry_r2_hidden,axiom, % 0.56/0.88 ! [A,B] : % 0.56/0.88 ( in(A,B) % 0.56/0.88 => ~ in(B,A) ) ). % 0.56/0.88 % 0.56/0.88 fof(antisymmetry_r2_xboole_0,axiom, % 0.56/0.88 ! [A,B] : % 0.56/0.88 ( proper_subset(A,B) % 0.56/0.88 => ~ proper_subset(B,A) ) ). % 0.56/0.88 % 0.56/0.88 fof(cc1_funct_1,axiom, % 0.56/0.88 ! [A] : % 0.56/0.88 ( empty(A) % 0.56/0.88 => function(A) ) ). % 0.56/0.88 % 0.56/0.88 fof(cc1_relat_1,axiom, % 0.56/0.88 ! [A] : % 0.56/0.88 ( empty(A) % 0.56/0.88 => relation(A) ) ). % 0.56/0.88 % 0.56/0.88 fof(commutativity_k2_tarski,axiom, % 0.56/0.88 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 0.56/0.88 % 0.56/0.88 fof(commutativity_k2_xboole_0,axiom, % 0.56/0.88 ! [A,B] : set_union2(A,B) = set_union2(B,A) ). % 0.56/0.88 % 0.56/0.88 fof(commutativity_k3_xboole_0,axiom, % 0.56/0.88 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 0.56/0.88 % 0.56/0.88 fof(d10_relat_1,axiom, % 0.56/0.88 ! [A,B] : % 0.56/0.88 ( relation(B) % 0.56/0.88 => ( B = identity_relation(A) % 0.56/0.88 <=> ! [C,D] : % 0.56/0.88 ( in(ordered_pair(C,D),B) % 0.56/0.88 <=> ( in(C,A) % 0.56/0.88 & C = D ) ) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d10_xboole_0,axiom, % 0.56/0.88 ! [A,B] : % 0.56/0.88 ( A = B % 0.56/0.88 <=> ( subset(A,B) % 0.56/0.88 & subset(B,A) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d11_relat_1,axiom, % 0.56/0.88 ! [A] : % 0.56/0.88 ( relation(A) % 0.56/0.88 => ! [B,C] : % 0.56/0.88 ( relation(C) % 0.56/0.88 => ( C = relation_dom_restriction(A,B) % 0.56/0.88 <=> ! [D,E] : % 0.56/0.88 ( in(ordered_pair(D,E),C) % 0.56/0.88 <=> ( in(D,B) % 0.56/0.88 & in(ordered_pair(D,E),A) ) ) ) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d12_relat_1,axiom, % 0.56/0.88 ! [A,B] : % 0.56/0.88 ( relation(B) % 0.56/0.88 => ! [C] : % 0.56/0.88 ( relation(C) % 0.56/0.88 => ( C = relation_rng_restriction(A,B) % 0.56/0.88 <=> ! [D,E] : % 0.56/0.88 ( in(ordered_pair(D,E),C) % 0.56/0.88 <=> ( in(E,A) % 0.56/0.88 & in(ordered_pair(D,E),B) ) ) ) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d13_relat_1,axiom, % 0.56/0.88 ! [A] : % 0.56/0.88 ( relation(A) % 0.56/0.88 => ! [B,C] : % 0.56/0.88 ( C = relation_image(A,B) % 0.56/0.88 <=> ! [D] : % 0.56/0.88 ( in(D,C) % 0.56/0.88 <=> ? [E] : % 0.56/0.88 ( in(ordered_pair(E,D),A) % 0.56/0.88 & in(E,B) ) ) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d14_relat_1,axiom, % 0.56/0.88 ! [A] : % 0.56/0.88 ( relation(A) % 0.56/0.88 => ! [B,C] : % 0.56/0.88 ( C = relation_inverse_image(A,B) % 0.56/0.88 <=> ! [D] : % 0.56/0.88 ( in(D,C) % 0.56/0.88 <=> ? [E] : % 0.56/0.88 ( in(ordered_pair(D,E),A) % 0.56/0.88 & in(E,B) ) ) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d1_relat_1,axiom, % 0.56/0.88 ! [A] : % 0.56/0.88 ( relation(A) % 0.56/0.88 <=> ! [B] : % 0.56/0.88 ~ ( in(B,A) % 0.56/0.88 & ! [C,D] : B != ordered_pair(C,D) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d1_setfam_1,axiom, % 0.56/0.88 ! [A,B] : % 0.56/0.88 ( ( A != empty_set % 0.56/0.88 => ( B = set_meet(A) % 0.56/0.88 <=> ! [C] : % 0.56/0.88 ( in(C,B) % 0.56/0.88 <=> ! [D] : % 0.56/0.88 ( in(D,A) % 0.56/0.88 => in(C,D) ) ) ) ) % 0.56/0.88 & ( A = empty_set % 0.56/0.88 => ( B = set_meet(A) % 0.56/0.88 <=> B = empty_set ) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d1_tarski,axiom, % 0.56/0.88 ! [A,B] : % 0.56/0.88 ( B = singleton(A) % 0.56/0.88 <=> ! [C] : % 0.56/0.88 ( in(C,B) % 0.56/0.88 <=> C = A ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d1_xboole_0,axiom, % 0.56/0.88 ! [A] : % 0.56/0.88 ( A = empty_set % 0.56/0.88 <=> ! [B] : ~ in(B,A) ) ). % 0.56/0.88 % 0.56/0.88 fof(d1_zfmisc_1,axiom, % 0.56/0.88 ! [A,B] : % 0.56/0.88 ( B = powerset(A) % 0.56/0.88 <=> ! [C] : % 0.56/0.88 ( in(C,B) % 0.56/0.88 <=> subset(C,A) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d2_relat_1,axiom, % 0.56/0.88 ! [A] : % 0.56/0.88 ( relation(A) % 0.56/0.88 => ! [B] : % 0.56/0.88 ( relation(B) % 0.56/0.88 => ( A = B % 0.56/0.88 <=> ! [C,D] : % 0.56/0.88 ( in(ordered_pair(C,D),A) % 0.56/0.88 <=> in(ordered_pair(C,D),B) ) ) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d2_subset_1,axiom, % 0.56/0.88 ! [A,B] : % 0.56/0.88 ( ( ~ empty(A) % 0.56/0.88 => ( element(B,A) % 0.56/0.88 <=> in(B,A) ) ) % 0.56/0.88 & ( empty(A) % 0.56/0.88 => ( element(B,A) % 0.56/0.88 <=> empty(B) ) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d2_tarski,axiom, % 0.56/0.88 ! [A,B,C] : % 0.56/0.88 ( C = unordered_pair(A,B) % 0.56/0.88 <=> ! [D] : % 0.56/0.88 ( in(D,C) % 0.56/0.88 <=> ( D = A % 0.56/0.88 | D = B ) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d2_xboole_0,axiom, % 0.56/0.88 ! [A,B,C] : % 0.56/0.88 ( C = set_union2(A,B) % 0.56/0.88 <=> ! [D] : % 0.56/0.88 ( in(D,C) % 0.56/0.88 <=> ( in(D,A) % 0.56/0.88 | in(D,B) ) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d2_zfmisc_1,axiom, % 0.56/0.88 ! [A,B,C] : % 0.56/0.88 ( C = cartesian_product2(A,B) % 0.56/0.88 <=> ! [D] : % 0.56/0.88 ( in(D,C) % 0.56/0.88 <=> ? [E,F] : % 0.56/0.88 ( in(E,A) % 0.56/0.88 & in(F,B) % 0.56/0.88 & D = ordered_pair(E,F) ) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d3_relat_1,axiom, % 0.56/0.88 ! [A] : % 0.56/0.88 ( relation(A) % 0.56/0.88 => ! [B] : % 0.56/0.88 ( relation(B) % 0.56/0.88 => ( subset(A,B) % 0.56/0.88 <=> ! [C,D] : % 0.56/0.88 ( in(ordered_pair(C,D),A) % 0.56/0.88 => in(ordered_pair(C,D),B) ) ) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d3_tarski,axiom, % 0.56/0.88 ! [A,B] : % 0.56/0.88 ( subset(A,B) % 0.56/0.88 <=> ! [C] : % 0.56/0.88 ( in(C,A) % 0.56/0.88 => in(C,B) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d3_xboole_0,axiom, % 0.56/0.88 ! [A,B,C] : % 0.56/0.88 ( C = set_intersection2(A,B) % 0.56/0.88 <=> ! [D] : % 0.56/0.88 ( in(D,C) % 0.56/0.88 <=> ( in(D,A) % 0.56/0.88 & in(D,B) ) ) ) ). % 0.56/0.88 % 0.56/0.88 fof(d4_funct_1,axiom, % 0.56/0.88 ! [A] : % 0.56/0.88 ( ( relation(A) % 0.56/0.88 & function(A) ) % 0.56/0.88 => ! [B,C] : % 0.56/0.88 ( ( in(B,relation_dom(A)) % 0.56/0.88 => ( C = apply(A,B) % 0.56/0.88 <=> in(ordered_pair(B,C),A) ) ) % 0.56/0.88 & ( ~ in(B,relation_dom(A)) % 0.56/0.88 => ( C = apply(A,B) % 0.56/0.88 <=> C = empty_set ) ) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(d4_relat_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ( relation(A) % 0.56/0.89 => ! [B] : % 0.56/0.89 ( B = relation_dom(A) % 0.56/0.89 <=> ! [C] : % 0.56/0.89 ( in(C,B) % 0.56/0.89 <=> ? [D] : in(ordered_pair(C,D),A) ) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(d4_subset_1,axiom, % 0.56/0.89 ! [A] : cast_to_subset(A) = A ). % 0.56/0.89 % 0.56/0.89 fof(d4_tarski,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( B = union(A) % 0.56/0.89 <=> ! [C] : % 0.56/0.89 ( in(C,B) % 0.56/0.89 <=> ? [D] : % 0.56/0.89 ( in(C,D) % 0.56/0.89 & in(D,A) ) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(d4_xboole_0,axiom, % 0.56/0.89 ! [A,B,C] : % 0.56/0.89 ( C = set_difference(A,B) % 0.56/0.89 <=> ! [D] : % 0.56/0.89 ( in(D,C) % 0.56/0.89 <=> ( in(D,A) % 0.56/0.89 & ~ in(D,B) ) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(d5_relat_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ( relation(A) % 0.56/0.89 => ! [B] : % 0.56/0.89 ( B = relation_rng(A) % 0.56/0.89 <=> ! [C] : % 0.56/0.89 ( in(C,B) % 0.56/0.89 <=> ? [D] : in(ordered_pair(D,C),A) ) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(d5_subset_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( element(B,powerset(A)) % 0.56/0.89 => subset_complement(A,B) = set_difference(A,B) ) ). % 0.56/0.89 % 0.56/0.89 fof(d5_tarski,axiom, % 0.56/0.89 ! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) ). % 0.56/0.89 % 0.56/0.89 fof(d6_relat_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ( relation(A) % 0.56/0.89 => relation_field(A) = set_union2(relation_dom(A),relation_rng(A)) ) ). % 0.56/0.89 % 0.56/0.89 fof(d7_relat_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ( relation(A) % 0.56/0.89 => ! [B] : % 0.56/0.89 ( relation(B) % 0.56/0.89 => ( B = relation_inverse(A) % 0.56/0.89 <=> ! [C,D] : % 0.56/0.89 ( in(ordered_pair(C,D),B) % 0.56/0.89 <=> in(ordered_pair(D,C),A) ) ) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(d7_xboole_0,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( disjoint(A,B) % 0.56/0.89 <=> set_intersection2(A,B) = empty_set ) ). % 0.56/0.89 % 0.56/0.89 fof(d8_relat_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ( relation(A) % 0.56/0.89 => ! [B] : % 0.56/0.89 ( relation(B) % 0.56/0.89 => ! [C] : % 0.56/0.89 ( relation(C) % 0.56/0.89 => ( C = relation_composition(A,B) % 0.56/0.89 <=> ! [D,E] : % 0.56/0.89 ( in(ordered_pair(D,E),C) % 0.56/0.89 <=> ? [F] : % 0.56/0.89 ( in(ordered_pair(D,F),A) % 0.56/0.89 & in(ordered_pair(F,E),B) ) ) ) ) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(d8_setfam_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( element(B,powerset(powerset(A))) % 0.56/0.89 => ! [C] : % 0.56/0.89 ( element(C,powerset(powerset(A))) % 0.56/0.89 => ( C = complements_of_subsets(A,B) % 0.56/0.89 <=> ! [D] : % 0.56/0.89 ( element(D,powerset(A)) % 0.56/0.89 => ( in(D,C) % 0.56/0.89 <=> in(subset_complement(A,D),B) ) ) ) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(d8_xboole_0,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( proper_subset(A,B) % 0.56/0.89 <=> ( subset(A,B) % 0.56/0.89 & A != B ) ) ). % 0.56/0.89 % 0.56/0.89 fof(dt_k10_relat_1,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k1_funct_1,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k1_relat_1,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k1_setfam_1,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k1_tarski,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k1_xboole_0,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k1_zfmisc_1,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k2_relat_1,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k2_subset_1,axiom, % 0.56/0.89 ! [A] : element(cast_to_subset(A),powerset(A)) ). % 0.56/0.89 % 0.56/0.89 fof(dt_k2_tarski,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k2_xboole_0,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k2_zfmisc_1,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k3_relat_1,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k3_subset_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( element(B,powerset(A)) % 0.56/0.89 => element(subset_complement(A,B),powerset(A)) ) ). % 0.56/0.89 % 0.56/0.89 fof(dt_k3_tarski,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k3_xboole_0,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k4_relat_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ( relation(A) % 0.56/0.89 => relation(relation_inverse(A)) ) ). % 0.56/0.89 % 0.56/0.89 fof(dt_k4_tarski,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k4_xboole_0,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_k5_relat_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( ( relation(A) % 0.56/0.89 & relation(B) ) % 0.56/0.89 => relation(relation_composition(A,B)) ) ). % 0.56/0.89 % 0.56/0.89 fof(dt_k5_setfam_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( element(B,powerset(powerset(A))) % 0.56/0.89 => element(union_of_subsets(A,B),powerset(A)) ) ). % 0.56/0.89 % 0.56/0.89 fof(dt_k6_relat_1,axiom, % 0.56/0.89 ! [A] : relation(identity_relation(A)) ). % 0.56/0.89 % 0.56/0.89 fof(dt_k6_setfam_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( element(B,powerset(powerset(A))) % 0.56/0.89 => element(meet_of_subsets(A,B),powerset(A)) ) ). % 0.56/0.89 % 0.56/0.89 fof(dt_k6_subset_1,axiom, % 0.56/0.89 ! [A,B,C] : % 0.56/0.89 ( ( element(B,powerset(A)) % 0.56/0.89 & element(C,powerset(A)) ) % 0.56/0.89 => element(subset_difference(A,B,C),powerset(A)) ) ). % 0.56/0.89 % 0.56/0.89 fof(dt_k7_relat_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( relation(A) % 0.56/0.89 => relation(relation_dom_restriction(A,B)) ) ). % 0.56/0.89 % 0.56/0.89 fof(dt_k7_setfam_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( element(B,powerset(powerset(A))) % 0.56/0.89 => element(complements_of_subsets(A,B),powerset(powerset(A))) ) ). % 0.56/0.89 % 0.56/0.89 fof(dt_k8_relat_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( relation(B) % 0.56/0.89 => relation(relation_rng_restriction(A,B)) ) ). % 0.56/0.89 % 0.56/0.89 fof(dt_k9_relat_1,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(dt_m1_subset_1,axiom, % 0.56/0.89 $true ). % 0.56/0.89 % 0.56/0.89 fof(existence_m1_subset_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ? [B] : element(B,A) ). % 0.56/0.89 % 0.56/0.89 fof(fc10_relat_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( ( empty(A) % 0.56/0.89 & relation(B) ) % 0.56/0.89 => ( empty(relation_composition(B,A)) % 0.56/0.89 & relation(relation_composition(B,A)) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc12_relat_1,axiom, % 0.56/0.89 ( empty(empty_set) % 0.56/0.89 & relation(empty_set) % 0.56/0.89 & relation_empty_yielding(empty_set) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc1_funct_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( ( relation(A) % 0.56/0.89 & function(A) % 0.56/0.89 & relation(B) % 0.56/0.89 & function(B) ) % 0.56/0.89 => ( relation(relation_composition(A,B)) % 0.56/0.89 & function(relation_composition(A,B)) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc1_relat_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( ( relation(A) % 0.56/0.89 & relation(B) ) % 0.56/0.89 => relation(set_intersection2(A,B)) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc1_subset_1,axiom, % 0.56/0.89 ! [A] : ~ empty(powerset(A)) ). % 0.56/0.89 % 0.56/0.89 fof(fc1_xboole_0,axiom, % 0.56/0.89 empty(empty_set) ). % 0.56/0.89 % 0.56/0.89 fof(fc1_zfmisc_1,axiom, % 0.56/0.89 ! [A,B] : ~ empty(ordered_pair(A,B)) ). % 0.56/0.89 % 0.56/0.89 fof(fc2_funct_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ( relation(identity_relation(A)) % 0.56/0.89 & function(identity_relation(A)) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc2_relat_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( ( relation(A) % 0.56/0.89 & relation(B) ) % 0.56/0.89 => relation(set_union2(A,B)) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc2_subset_1,axiom, % 0.56/0.89 ! [A] : ~ empty(singleton(A)) ). % 0.56/0.89 % 0.56/0.89 fof(fc2_xboole_0,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( ~ empty(A) % 0.56/0.89 => ~ empty(set_union2(A,B)) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc3_subset_1,axiom, % 0.56/0.89 ! [A,B] : ~ empty(unordered_pair(A,B)) ). % 0.56/0.89 % 0.56/0.89 fof(fc3_xboole_0,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( ~ empty(A) % 0.56/0.89 => ~ empty(set_union2(B,A)) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc4_relat_1,axiom, % 0.56/0.89 ( empty(empty_set) % 0.56/0.89 & relation(empty_set) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc4_subset_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( ( ~ empty(A) % 0.56/0.89 & ~ empty(B) ) % 0.56/0.89 => ~ empty(cartesian_product2(A,B)) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc5_relat_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ( ( ~ empty(A) % 0.56/0.89 & relation(A) ) % 0.56/0.89 => ~ empty(relation_dom(A)) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc6_relat_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ( ( ~ empty(A) % 0.56/0.89 & relation(A) ) % 0.56/0.89 => ~ empty(relation_rng(A)) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc7_relat_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ( empty(A) % 0.56/0.89 => ( empty(relation_dom(A)) % 0.56/0.89 & relation(relation_dom(A)) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc8_relat_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ( empty(A) % 0.56/0.89 => ( empty(relation_rng(A)) % 0.56/0.89 & relation(relation_rng(A)) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(fc9_relat_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( ( empty(A) % 0.56/0.89 & relation(B) ) % 0.56/0.89 => ( empty(relation_composition(A,B)) % 0.56/0.89 & relation(relation_composition(A,B)) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(idempotence_k2_xboole_0,axiom, % 0.56/0.89 ! [A,B] : set_union2(A,A) = A ). % 0.56/0.89 % 0.56/0.89 fof(idempotence_k3_xboole_0,axiom, % 0.56/0.89 ! [A,B] : set_intersection2(A,A) = A ). % 0.56/0.89 % 0.56/0.89 fof(involutiveness_k3_subset_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( element(B,powerset(A)) % 0.56/0.89 => subset_complement(A,subset_complement(A,B)) = B ) ). % 0.56/0.89 % 0.56/0.89 fof(involutiveness_k4_relat_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ( relation(A) % 0.56/0.89 => relation_inverse(relation_inverse(A)) = A ) ). % 0.56/0.89 % 0.56/0.89 fof(involutiveness_k7_setfam_1,axiom, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( element(B,powerset(powerset(A))) % 0.56/0.89 => complements_of_subsets(A,complements_of_subsets(A,B)) = B ) ). % 0.56/0.89 % 0.56/0.89 fof(irreflexivity_r2_xboole_0,axiom, % 0.56/0.89 ! [A,B] : ~ proper_subset(A,A) ). % 0.56/0.89 % 0.56/0.89 fof(l1_zfmisc_1,lemma, % 0.56/0.89 ! [A] : singleton(A) != empty_set ). % 0.56/0.89 % 0.56/0.89 fof(l23_zfmisc_1,lemma, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( in(A,B) % 0.56/0.89 => set_union2(singleton(A),B) = B ) ). % 0.56/0.89 % 0.56/0.89 fof(l25_zfmisc_1,lemma, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ~ ( disjoint(singleton(A),B) % 0.56/0.89 & in(A,B) ) ). % 0.56/0.89 % 0.56/0.89 fof(l28_zfmisc_1,lemma, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( ~ in(A,B) % 0.56/0.89 => disjoint(singleton(A),B) ) ). % 0.56/0.89 % 0.56/0.89 fof(l2_zfmisc_1,lemma, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( subset(singleton(A),B) % 0.56/0.89 <=> in(A,B) ) ). % 0.56/0.89 % 0.56/0.89 fof(l32_xboole_1,lemma, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( set_difference(A,B) = empty_set % 0.56/0.89 <=> subset(A,B) ) ). % 0.56/0.89 % 0.56/0.89 fof(l3_subset_1,lemma, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( element(B,powerset(A)) % 0.56/0.89 => ! [C] : % 0.56/0.89 ( in(C,B) % 0.56/0.89 => in(C,A) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(l3_zfmisc_1,lemma, % 0.56/0.89 ! [A,B,C] : % 0.56/0.89 ( subset(A,B) % 0.56/0.89 => ( in(C,A) % 0.56/0.89 | subset(A,set_difference(B,singleton(C))) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(l4_zfmisc_1,lemma, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( subset(A,singleton(B)) % 0.56/0.89 <=> ( A = empty_set % 0.56/0.89 | A = singleton(B) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(l50_zfmisc_1,lemma, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( in(A,B) % 0.56/0.89 => subset(A,union(B)) ) ). % 0.56/0.89 % 0.56/0.89 fof(l55_zfmisc_1,lemma, % 0.56/0.89 ! [A,B,C,D] : % 0.56/0.89 ( in(ordered_pair(A,B),cartesian_product2(C,D)) % 0.56/0.89 <=> ( in(A,C) % 0.56/0.89 & in(B,D) ) ) ). % 0.56/0.89 % 0.56/0.89 fof(l71_subset_1,lemma, % 0.56/0.89 ! [A,B] : % 0.56/0.89 ( ! [C] : % 0.56/0.89 ( in(C,A) % 0.56/0.89 => in(C,B) ) % 0.56/0.89 => element(A,powerset(B)) ) ). % 0.56/0.89 % 0.56/0.89 fof(rc1_funct_1,axiom, % 0.56/0.89 ? [A] : % 0.56/0.89 ( relation(A) % 0.56/0.89 & function(A) ) ). % 0.56/0.89 % 0.56/0.89 fof(rc1_relat_1,axiom, % 0.56/0.89 ? [A] : % 0.56/0.89 ( empty(A) % 0.56/0.89 & relation(A) ) ). % 0.56/0.89 % 0.56/0.89 fof(rc1_subset_1,axiom, % 0.56/0.89 ! [A] : % 0.56/0.89 ( ~ empty(A) % 0.56/0.89 => ? [B] : % 0.56/0.89 ( element(B,powerset(A)) % 0.56/0.89 & ~ empty(B) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(rc1_xboole_0,axiom, % 0.56/0.90 ? [A] : empty(A) ). % 0.56/0.90 % 0.56/0.90 fof(rc2_relat_1,axiom, % 0.56/0.90 ? [A] : % 0.56/0.90 ( ~ empty(A) % 0.56/0.90 & relation(A) ) ). % 0.56/0.90 % 0.56/0.90 fof(rc2_subset_1,axiom, % 0.56/0.90 ! [A] : % 0.56/0.90 ? [B] : % 0.56/0.90 ( element(B,powerset(A)) % 0.56/0.90 & empty(B) ) ). % 0.56/0.90 % 0.56/0.90 fof(rc2_xboole_0,axiom, % 0.56/0.90 ? [A] : ~ empty(A) ). % 0.56/0.90 % 0.56/0.90 fof(rc3_relat_1,axiom, % 0.56/0.90 ? [A] : % 0.56/0.90 ( relation(A) % 0.56/0.90 & relation_empty_yielding(A) ) ). % 0.56/0.90 % 0.56/0.90 fof(redefinition_k5_setfam_1,axiom, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( element(B,powerset(powerset(A))) % 0.56/0.90 => union_of_subsets(A,B) = union(B) ) ). % 0.56/0.90 % 0.56/0.90 fof(redefinition_k6_setfam_1,axiom, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( element(B,powerset(powerset(A))) % 0.56/0.90 => meet_of_subsets(A,B) = set_meet(B) ) ). % 0.56/0.90 % 0.56/0.90 fof(redefinition_k6_subset_1,axiom, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( ( element(B,powerset(A)) % 0.56/0.90 & element(C,powerset(A)) ) % 0.56/0.90 => subset_difference(A,B,C) = set_difference(B,C) ) ). % 0.56/0.90 % 0.56/0.90 fof(reflexivity_r1_tarski,axiom, % 0.56/0.90 ! [A,B] : subset(A,A) ). % 0.56/0.90 % 0.56/0.90 fof(symmetry_r1_xboole_0,axiom, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( disjoint(A,B) % 0.56/0.90 => disjoint(B,A) ) ). % 0.56/0.90 % 0.56/0.90 fof(t106_zfmisc_1,lemma, % 0.56/0.90 ! [A,B,C,D] : % 0.56/0.90 ( in(ordered_pair(A,B),cartesian_product2(C,D)) % 0.56/0.90 <=> ( in(A,C) % 0.56/0.90 & in(B,D) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t10_zfmisc_1,lemma, % 0.56/0.90 ! [A,B,C,D] : % 0.56/0.90 ~ ( unordered_pair(A,B) = unordered_pair(C,D) % 0.56/0.90 & A != C % 0.56/0.90 & A != D ) ). % 0.56/0.90 % 0.56/0.90 fof(t115_relat_1,lemma, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( relation(C) % 0.56/0.90 => ( in(A,relation_rng(relation_rng_restriction(B,C))) % 0.56/0.90 <=> ( in(A,B) % 0.56/0.90 & in(A,relation_rng(C)) ) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t116_relat_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( relation(B) % 0.56/0.90 => subset(relation_rng(relation_rng_restriction(A,B)),A) ) ). % 0.56/0.90 % 0.56/0.90 fof(t117_relat_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( relation(B) % 0.56/0.90 => subset(relation_rng_restriction(A,B),B) ) ). % 0.56/0.90 % 0.56/0.90 fof(t118_relat_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( relation(B) % 0.56/0.90 => subset(relation_rng(relation_rng_restriction(A,B)),relation_rng(B)) ) ). % 0.56/0.90 % 0.56/0.90 fof(t118_zfmisc_1,lemma, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( subset(A,B) % 0.56/0.90 => ( subset(cartesian_product2(A,C),cartesian_product2(B,C)) % 0.56/0.90 & subset(cartesian_product2(C,A),cartesian_product2(C,B)) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t119_relat_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( relation(B) % 0.56/0.90 => relation_rng(relation_rng_restriction(A,B)) = set_intersection2(relation_rng(B),A) ) ). % 0.56/0.90 % 0.56/0.90 fof(t119_zfmisc_1,lemma, % 0.56/0.90 ! [A,B,C,D] : % 0.56/0.90 ( ( subset(A,B) % 0.56/0.90 & subset(C,D) ) % 0.56/0.90 => subset(cartesian_product2(A,C),cartesian_product2(B,D)) ) ). % 0.56/0.90 % 0.56/0.90 fof(t12_xboole_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( subset(A,B) % 0.56/0.90 => set_union2(A,B) = B ) ). % 0.56/0.90 % 0.56/0.90 fof(t136_zfmisc_1,lemma, % 0.56/0.90 ! [A] : % 0.56/0.90 ? [B] : % 0.56/0.90 ( in(A,B) % 0.56/0.90 & ! [C,D] : % 0.56/0.90 ( ( in(C,B) % 0.56/0.90 & subset(D,C) ) % 0.56/0.90 => in(D,B) ) % 0.56/0.90 & ! [C] : % 0.56/0.90 ( in(C,B) % 0.56/0.90 => in(powerset(C),B) ) % 0.56/0.90 & ! [C] : % 0.56/0.90 ~ ( subset(C,B) % 0.56/0.90 & ~ are_equipotent(C,B) % 0.56/0.90 & ~ in(C,B) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t140_relat_1,lemma, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( relation(C) % 0.56/0.90 => relation_dom_restriction(relation_rng_restriction(A,C),B) = relation_rng_restriction(A,relation_dom_restriction(C,B)) ) ). % 0.56/0.90 % 0.56/0.90 fof(t143_relat_1,lemma, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( relation(C) % 0.56/0.90 => ( in(A,relation_image(C,B)) % 0.56/0.90 <=> ? [D] : % 0.56/0.90 ( in(D,relation_dom(C)) % 0.56/0.90 & in(ordered_pair(D,A),C) % 0.56/0.90 & in(D,B) ) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t144_relat_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( relation(B) % 0.56/0.90 => subset(relation_image(B,A),relation_rng(B)) ) ). % 0.56/0.90 % 0.56/0.90 fof(t145_relat_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( relation(B) % 0.56/0.90 => relation_image(B,A) = relation_image(B,set_intersection2(relation_dom(B),A)) ) ). % 0.56/0.90 % 0.56/0.90 fof(t146_relat_1,lemma, % 0.56/0.90 ! [A] : % 0.56/0.90 ( relation(A) % 0.56/0.90 => relation_image(A,relation_dom(A)) = relation_rng(A) ) ). % 0.56/0.90 % 0.56/0.90 fof(t160_relat_1,lemma, % 0.56/0.90 ! [A] : % 0.56/0.90 ( relation(A) % 0.56/0.90 => ! [B] : % 0.56/0.90 ( relation(B) % 0.56/0.90 => relation_rng(relation_composition(A,B)) = relation_image(B,relation_rng(A)) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t166_relat_1,lemma, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( relation(C) % 0.56/0.90 => ( in(A,relation_inverse_image(C,B)) % 0.56/0.90 <=> ? [D] : % 0.56/0.90 ( in(D,relation_rng(C)) % 0.56/0.90 & in(ordered_pair(A,D),C) % 0.56/0.90 & in(D,B) ) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t167_relat_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( relation(B) % 0.56/0.90 => subset(relation_inverse_image(B,A),relation_dom(B)) ) ). % 0.56/0.90 % 0.56/0.90 fof(t174_relat_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( relation(B) % 0.56/0.90 => ~ ( A != empty_set % 0.56/0.90 & subset(A,relation_rng(B)) % 0.56/0.90 & relation_inverse_image(B,A) = empty_set ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t178_relat_1,lemma, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( relation(C) % 0.56/0.90 => ( subset(A,B) % 0.56/0.90 => subset(relation_inverse_image(C,A),relation_inverse_image(C,B)) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t17_xboole_1,lemma, % 0.56/0.90 ! [A,B] : subset(set_intersection2(A,B),A) ). % 0.56/0.90 % 0.56/0.90 fof(t19_xboole_1,lemma, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( ( subset(A,B) % 0.56/0.90 & subset(A,C) ) % 0.56/0.90 => subset(A,set_intersection2(B,C)) ) ). % 0.56/0.90 % 0.56/0.90 fof(t1_boole,axiom, % 0.56/0.90 ! [A] : set_union2(A,empty_set) = A ). % 0.56/0.90 % 0.56/0.90 fof(t1_subset,axiom, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( in(A,B) % 0.56/0.90 => element(A,B) ) ). % 0.56/0.90 % 0.56/0.90 fof(t1_xboole_1,lemma, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( ( subset(A,B) % 0.56/0.90 & subset(B,C) ) % 0.56/0.90 => subset(A,C) ) ). % 0.56/0.90 % 0.56/0.90 fof(t1_zfmisc_1,lemma, % 0.56/0.90 powerset(empty_set) = singleton(empty_set) ). % 0.56/0.90 % 0.56/0.90 fof(t20_relat_1,lemma, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( relation(C) % 0.56/0.90 => ( in(ordered_pair(A,B),C) % 0.56/0.90 => ( in(A,relation_dom(C)) % 0.56/0.90 & in(B,relation_rng(C)) ) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t21_funct_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( ( relation(B) % 0.56/0.90 & function(B) ) % 0.56/0.90 => ! [C] : % 0.56/0.90 ( ( relation(C) % 0.56/0.90 & function(C) ) % 0.56/0.90 => ( in(A,relation_dom(relation_composition(C,B))) % 0.56/0.90 <=> ( in(A,relation_dom(C)) % 0.56/0.90 & in(apply(C,A),relation_dom(B)) ) ) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t21_relat_1,lemma, % 0.56/0.90 ! [A] : % 0.56/0.90 ( relation(A) % 0.56/0.90 => subset(A,cartesian_product2(relation_dom(A),relation_rng(A))) ) ). % 0.56/0.90 % 0.56/0.90 fof(t22_funct_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( ( relation(B) % 0.56/0.90 & function(B) ) % 0.56/0.90 => ! [C] : % 0.56/0.90 ( ( relation(C) % 0.56/0.90 & function(C) ) % 0.56/0.90 => ( in(A,relation_dom(relation_composition(C,B))) % 0.56/0.90 => apply(relation_composition(C,B),A) = apply(B,apply(C,A)) ) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t23_funct_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( ( relation(B) % 0.56/0.90 & function(B) ) % 0.56/0.90 => ! [C] : % 0.56/0.90 ( ( relation(C) % 0.56/0.90 & function(C) ) % 0.56/0.90 => ( in(A,relation_dom(B)) % 0.56/0.90 => apply(relation_composition(B,C),A) = apply(C,apply(B,A)) ) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t25_relat_1,lemma, % 0.56/0.90 ! [A] : % 0.56/0.90 ( relation(A) % 0.56/0.90 => ! [B] : % 0.56/0.90 ( relation(B) % 0.56/0.90 => ( subset(A,B) % 0.56/0.90 => ( subset(relation_dom(A),relation_dom(B)) % 0.56/0.90 & subset(relation_rng(A),relation_rng(B)) ) ) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t26_xboole_1,lemma, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( subset(A,B) % 0.56/0.90 => subset(set_intersection2(A,C),set_intersection2(B,C)) ) ). % 0.56/0.90 % 0.56/0.90 fof(t28_xboole_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( subset(A,B) % 0.56/0.90 => set_intersection2(A,B) = A ) ). % 0.56/0.90 % 0.56/0.90 fof(t2_boole,axiom, % 0.56/0.90 ! [A] : set_intersection2(A,empty_set) = empty_set ). % 0.56/0.90 % 0.56/0.90 fof(t2_subset,axiom, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( element(A,B) % 0.56/0.90 => ( empty(B) % 0.56/0.90 | in(A,B) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t2_tarski,axiom, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( ! [C] : % 0.56/0.90 ( in(C,A) % 0.56/0.90 <=> in(C,B) ) % 0.56/0.90 => A = B ) ). % 0.56/0.90 % 0.56/0.90 fof(t2_xboole_1,lemma, % 0.56/0.90 ! [A] : subset(empty_set,A) ). % 0.56/0.90 % 0.56/0.90 fof(t30_relat_1,lemma, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( relation(C) % 0.56/0.90 => ( in(ordered_pair(A,B),C) % 0.56/0.90 => ( in(A,relation_field(C)) % 0.56/0.90 & in(B,relation_field(C)) ) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t33_xboole_1,lemma, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( subset(A,B) % 0.56/0.90 => subset(set_difference(A,C),set_difference(B,C)) ) ). % 0.56/0.90 % 0.56/0.90 fof(t33_zfmisc_1,lemma, % 0.56/0.90 ! [A,B,C,D] : % 0.56/0.90 ( ordered_pair(A,B) = ordered_pair(C,D) % 0.56/0.90 => ( A = C % 0.56/0.90 & B = D ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t34_funct_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( ( relation(B) % 0.56/0.90 & function(B) ) % 0.56/0.90 => ( B = identity_relation(A) % 0.56/0.90 <=> ( relation_dom(B) = A % 0.56/0.90 & ! [C] : % 0.56/0.90 ( in(C,A) % 0.56/0.90 => apply(B,C) = C ) ) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t35_funct_1,conjecture, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( in(B,A) % 0.56/0.90 => apply(identity_relation(A),B) = B ) ). % 0.56/0.90 % 0.56/0.90 fof(t36_xboole_1,lemma, % 0.56/0.90 ! [A,B] : subset(set_difference(A,B),A) ). % 0.56/0.90 % 0.56/0.90 fof(t37_relat_1,lemma, % 0.56/0.90 ! [A] : % 0.56/0.90 ( relation(A) % 0.56/0.90 => ( relation_rng(A) = relation_dom(relation_inverse(A)) % 0.56/0.90 & relation_dom(A) = relation_rng(relation_inverse(A)) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t37_xboole_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( set_difference(A,B) = empty_set % 0.56/0.90 <=> subset(A,B) ) ). % 0.56/0.90 % 0.56/0.90 fof(t37_zfmisc_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( subset(singleton(A),B) % 0.56/0.90 <=> in(A,B) ) ). % 0.56/0.90 % 0.56/0.90 fof(t38_zfmisc_1,lemma, % 0.56/0.90 ! [A,B,C] : % 0.56/0.90 ( subset(unordered_pair(A,B),C) % 0.56/0.90 <=> ( in(A,C) % 0.56/0.90 & in(B,C) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t39_xboole_1,lemma, % 0.56/0.90 ! [A,B] : set_union2(A,set_difference(B,A)) = set_union2(A,B) ). % 0.56/0.90 % 0.56/0.90 fof(t39_zfmisc_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( subset(A,singleton(B)) % 0.56/0.90 <=> ( A = empty_set % 0.56/0.90 | A = singleton(B) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t3_boole,axiom, % 0.56/0.90 ! [A] : set_difference(A,empty_set) = A ). % 0.56/0.90 % 0.56/0.90 fof(t3_subset,axiom, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( element(A,powerset(B)) % 0.56/0.90 <=> subset(A,B) ) ). % 0.56/0.90 % 0.56/0.90 fof(t3_xboole_0,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( ~ ( ~ disjoint(A,B) % 0.56/0.90 & ! [C] : % 0.56/0.90 ~ ( in(C,A) % 0.56/0.90 & in(C,B) ) ) % 0.56/0.90 & ~ ( ? [C] : % 0.56/0.90 ( in(C,A) % 0.56/0.90 & in(C,B) ) % 0.56/0.90 & disjoint(A,B) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t3_xboole_1,lemma, % 0.56/0.90 ! [A] : % 0.56/0.90 ( subset(A,empty_set) % 0.56/0.90 => A = empty_set ) ). % 0.56/0.90 % 0.56/0.90 fof(t40_xboole_1,lemma, % 0.56/0.90 ! [A,B] : set_difference(set_union2(A,B),B) = set_difference(A,B) ). % 0.56/0.90 % 0.56/0.90 fof(t43_subset_1,lemma, % 0.56/0.90 ! [A,B] : % 0.56/0.90 ( element(B,powerset(A)) % 0.56/0.90 => ! [C] : % 0.56/0.90 ( element(C,powerset(A)) % 0.56/0.90 => ( disjoint(B,C) % 0.56/0.90 <=> subset(B,subset_complement(A,C)) ) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t44_relat_1,lemma, % 0.56/0.90 ! [A] : % 0.56/0.90 ( relation(A) % 0.56/0.90 => ! [B] : % 0.56/0.90 ( relation(B) % 0.56/0.90 => subset(relation_dom(relation_composition(A,B)),relation_dom(A)) ) ) ). % 0.56/0.90 % 0.56/0.90 fof(t45_relat_1,lemma, % 0.56/0.90 ! [A] : % 0.56/0.90 ( relation(A) % 0.56/0.90 => ! [B] : % 0.56/0.90 ( relation(B) % 0.56/0.90 => subset(relation_rng(relation_composition(A,B)),relation_rng(B)) ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t45_xboole_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( subset(A,B) % 0.56/0.91 => B = set_union2(A,set_difference(B,A)) ) ). % 0.56/0.91 % 0.56/0.91 fof(t46_relat_1,lemma, % 0.56/0.91 ! [A] : % 0.56/0.91 ( relation(A) % 0.56/0.91 => ! [B] : % 0.56/0.91 ( relation(B) % 0.56/0.91 => ( subset(relation_rng(A),relation_dom(B)) % 0.56/0.91 => relation_dom(relation_composition(A,B)) = relation_dom(A) ) ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t46_setfam_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( element(B,powerset(powerset(A))) % 0.56/0.91 => ~ ( B != empty_set % 0.56/0.91 & complements_of_subsets(A,B) = empty_set ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t46_zfmisc_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( in(A,B) % 0.56/0.91 => set_union2(singleton(A),B) = B ) ). % 0.56/0.91 % 0.56/0.91 fof(t47_relat_1,lemma, % 0.56/0.91 ! [A] : % 0.56/0.91 ( relation(A) % 0.56/0.91 => ! [B] : % 0.56/0.91 ( relation(B) % 0.56/0.91 => ( subset(relation_dom(A),relation_rng(B)) % 0.56/0.91 => relation_rng(relation_composition(B,A)) = relation_rng(A) ) ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t47_setfam_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( element(B,powerset(powerset(A))) % 0.56/0.91 => ( B != empty_set % 0.56/0.91 => subset_difference(A,cast_to_subset(A),union_of_subsets(A,B)) = meet_of_subsets(A,complements_of_subsets(A,B)) ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t48_setfam_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( element(B,powerset(powerset(A))) % 0.56/0.91 => ( B != empty_set % 0.56/0.91 => union_of_subsets(A,complements_of_subsets(A,B)) = subset_difference(A,cast_to_subset(A),meet_of_subsets(A,B)) ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t48_xboole_1,lemma, % 0.56/0.91 ! [A,B] : set_difference(A,set_difference(A,B)) = set_intersection2(A,B) ). % 0.56/0.91 % 0.56/0.91 fof(t4_boole,axiom, % 0.56/0.91 ! [A] : set_difference(empty_set,A) = empty_set ). % 0.56/0.91 % 0.56/0.91 fof(t4_subset,axiom, % 0.56/0.91 ! [A,B,C] : % 0.56/0.91 ( ( in(A,B) % 0.56/0.91 & element(B,powerset(C)) ) % 0.56/0.91 => element(A,C) ) ). % 0.56/0.91 % 0.56/0.91 fof(t4_xboole_0,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( ~ ( ~ disjoint(A,B) % 0.56/0.91 & ! [C] : ~ in(C,set_intersection2(A,B)) ) % 0.56/0.91 & ~ ( ? [C] : in(C,set_intersection2(A,B)) % 0.56/0.91 & disjoint(A,B) ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t50_subset_1,lemma, % 0.56/0.91 ! [A] : % 0.56/0.91 ( A != empty_set % 0.56/0.91 => ! [B] : % 0.56/0.91 ( element(B,powerset(A)) % 0.56/0.91 => ! [C] : % 0.56/0.91 ( element(C,A) % 0.56/0.91 => ( ~ in(C,B) % 0.56/0.91 => in(C,subset_complement(A,B)) ) ) ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t54_subset_1,lemma, % 0.56/0.91 ! [A,B,C] : % 0.56/0.91 ( element(C,powerset(A)) % 0.56/0.91 => ~ ( in(B,subset_complement(A,C)) % 0.56/0.91 & in(B,C) ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t56_relat_1,lemma, % 0.56/0.91 ! [A] : % 0.56/0.91 ( relation(A) % 0.56/0.91 => ( ! [B,C] : ~ in(ordered_pair(B,C),A) % 0.56/0.91 => A = empty_set ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t5_subset,axiom, % 0.56/0.91 ! [A,B,C] : % 0.56/0.91 ~ ( in(A,B) % 0.56/0.91 & element(B,powerset(C)) % 0.56/0.91 & empty(C) ) ). % 0.56/0.91 % 0.56/0.91 fof(t60_relat_1,lemma, % 0.56/0.91 ( relation_dom(empty_set) = empty_set % 0.56/0.91 & relation_rng(empty_set) = empty_set ) ). % 0.56/0.91 % 0.56/0.91 fof(t60_xboole_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ~ ( subset(A,B) % 0.56/0.91 & proper_subset(B,A) ) ). % 0.56/0.91 % 0.56/0.91 fof(t63_xboole_1,lemma, % 0.56/0.91 ! [A,B,C] : % 0.56/0.91 ( ( subset(A,B) % 0.56/0.91 & disjoint(B,C) ) % 0.56/0.91 => disjoint(A,C) ) ). % 0.56/0.91 % 0.56/0.91 fof(t64_relat_1,lemma, % 0.56/0.91 ! [A] : % 0.56/0.91 ( relation(A) % 0.56/0.91 => ( ( relation_dom(A) = empty_set % 0.56/0.91 | relation_rng(A) = empty_set ) % 0.56/0.91 => A = empty_set ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t65_relat_1,lemma, % 0.56/0.91 ! [A] : % 0.56/0.91 ( relation(A) % 0.56/0.91 => ( relation_dom(A) = empty_set % 0.56/0.91 <=> relation_rng(A) = empty_set ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t65_zfmisc_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( set_difference(A,singleton(B)) = A % 0.56/0.91 <=> ~ in(B,A) ) ). % 0.56/0.91 % 0.56/0.91 fof(t69_enumset1,lemma, % 0.56/0.91 ! [A] : unordered_pair(A,A) = singleton(A) ). % 0.56/0.91 % 0.56/0.91 fof(t6_boole,axiom, % 0.56/0.91 ! [A] : % 0.56/0.91 ( empty(A) % 0.56/0.91 => A = empty_set ) ). % 0.56/0.91 % 0.56/0.91 fof(t6_zfmisc_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( subset(singleton(A),singleton(B)) % 0.56/0.91 => A = B ) ). % 0.56/0.91 % 0.56/0.91 fof(t71_relat_1,lemma, % 0.56/0.91 ! [A] : % 0.56/0.91 ( relation_dom(identity_relation(A)) = A % 0.56/0.91 & relation_rng(identity_relation(A)) = A ) ). % 0.56/0.91 % 0.56/0.91 fof(t74_relat_1,lemma, % 0.56/0.91 ! [A,B,C,D] : % 0.56/0.91 ( relation(D) % 0.56/0.91 => ( in(ordered_pair(A,B),relation_composition(identity_relation(C),D)) % 0.56/0.91 <=> ( in(A,C) % 0.56/0.91 & in(ordered_pair(A,B),D) ) ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t7_boole,axiom, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ~ ( in(A,B) % 0.56/0.91 & empty(B) ) ). % 0.56/0.91 % 0.56/0.91 fof(t7_xboole_1,lemma, % 0.56/0.91 ! [A,B] : subset(A,set_union2(A,B)) ). % 0.56/0.91 % 0.56/0.91 fof(t83_xboole_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( disjoint(A,B) % 0.56/0.91 <=> set_difference(A,B) = A ) ). % 0.56/0.91 % 0.56/0.91 fof(t86_relat_1,lemma, % 0.56/0.91 ! [A,B,C] : % 0.56/0.91 ( relation(C) % 0.56/0.91 => ( in(A,relation_dom(relation_dom_restriction(C,B))) % 0.56/0.91 <=> ( in(A,B) % 0.56/0.91 & in(A,relation_dom(C)) ) ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t88_relat_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( relation(B) % 0.56/0.91 => subset(relation_dom_restriction(B,A),B) ) ). % 0.56/0.91 % 0.56/0.91 fof(t8_boole,axiom, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ~ ( empty(A) % 0.56/0.91 & A != B % 0.56/0.91 & empty(B) ) ). % 0.56/0.91 % 0.56/0.91 fof(t8_funct_1,lemma, % 0.56/0.91 ! [A,B,C] : % 0.56/0.91 ( ( relation(C) % 0.56/0.91 & function(C) ) % 0.56/0.91 => ( in(ordered_pair(A,B),C) % 0.56/0.91 <=> ( in(A,relation_dom(C)) % 0.56/0.91 & B = apply(C,A) ) ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t8_xboole_1,lemma, % 0.56/0.91 ! [A,B,C] : % 0.56/0.91 ( ( subset(A,B) % 0.56/0.91 & subset(C,B) ) % 0.56/0.91 => subset(set_union2(A,C),B) ) ). % 0.56/0.91 % 0.56/0.91 fof(t8_zfmisc_1,lemma, % 0.56/0.91 ! [A,B,C] : % 0.56/0.91 ( singleton(A) = unordered_pair(B,C) % 0.56/0.91 => A = B ) ). % 0.56/0.91 % 0.56/0.91 fof(t90_relat_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( relation(B) % 0.56/0.91 => relation_dom(relation_dom_restriction(B,A)) = set_intersection2(relation_dom(B),A) ) ). % 0.56/0.91 % 0.56/0.91 fof(t92_zfmisc_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( in(A,B) % 0.56/0.91 => subset(A,union(B)) ) ). % 0.56/0.91 % 0.56/0.91 fof(t94_relat_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( relation(B) % 0.56/0.91 => relation_dom_restriction(B,A) = relation_composition(identity_relation(A),B) ) ). % 0.56/0.91 % 0.56/0.91 fof(t99_relat_1,lemma, % 0.56/0.91 ! [A,B] : % 0.56/0.91 ( relation(B) % 0.56/0.91 => subset(relation_rng(relation_dom_restriction(B,A)),relation_rng(B)) ) ). % 0.56/0.91 % 0.56/0.91 fof(t99_zfmisc_1,lemma, % 0.56/0.91 ! [A] : union(powerset(A)) = A ). % 0.56/0.91 % 0.56/0.91 fof(t9_tarski,axiom, % 0.56/0.91 ! [A] : % 0.56/0.91 ? [B] : % 0.56/0.91 ( in(A,B) % 0.56/0.91 & ! [C,D] : % 0.56/0.91 ( ( in(C,B) % 0.56/0.91 & subset(D,C) ) % 0.56/0.91 => in(D,B) ) % 0.56/0.91 & ! [C] : % 0.56/0.91 ~ ( in(C,B) % 0.56/0.91 & ! [D] : % 0.56/0.91 ~ ( in(D,B) % 0.56/0.91 & ! [E] : % 0.56/0.91 ( subset(E,C) % 0.56/0.91 => in(E,D) ) ) ) % 0.56/0.91 & ! [C] : % 0.56/0.91 ~ ( subset(C,B) % 0.56/0.91 & ~ are_equipotent(C,B) % 0.56/0.91 & ~ in(C,B) ) ) ). % 0.56/0.91 % 0.56/0.91 fof(t9_zfmisc_1,lemma, % 0.56/0.91 ! [A,B,C] : % 0.56/0.91 ( singleton(A) = unordered_pair(B,C) % 0.56/0.91 => B = C ) ). % 0.56/0.91 % 0.56/0.91 %------------------------------------------------------------------------------ % 0.56/0.91 %------------------------------------------- % 0.56/0.91 % Proof found % 0.56/0.91 % SZS status Theorem for theBenchmark % 0.56/0.91 % SZS output start Proof % 0.56/0.91 %ClaNum:599(EqnAxiom:217) % 0.56/0.91 %VarNum:2774(SingletonVarNum:848) % 0.56/0.91 %MaxLitNum:7 % 0.56/0.91 %MaxfuncDepth:4 % 0.56/0.91 %SharedTerms:33 % 0.56/0.91 %goalClause: 241 269 % 0.56/0.91 %singleGoalClaCount:2 % 0.56/0.91 [222]P1(a1) % 0.56/0.91 [223]P1(a6) % 0.56/0.91 [224]P1(a56) % 0.56/0.91 [225]P5(a7) % 0.56/0.91 [227]P6(a1) % 0.56/0.91 [228]P6(a7) % 0.56/0.91 [229]P6(a6) % 0.56/0.91 [230]P6(a58) % 0.56/0.91 [231]P6(a59) % 0.56/0.91 [232]P9(a1) % 0.56/0.91 [233]P9(a59) % 0.56/0.91 [241]P7(a64,a65) % 0.56/0.91 [264]~P1(a58) % 0.56/0.91 [265]~P1(a61) % 0.56/0.91 [218]E(f5(a1),a1) % 0.56/0.91 [219]E(f84(a1),a1) % 0.56/0.91 [246]E(f97(a1,a1),f81(a1)) % 0.56/0.91 [269]~E(f2(f63(a65),a64),a64) % 0.56/0.91 [243]P10(a1,x2431) % 0.56/0.91 [247]P10(x2471,x2471) % 0.56/0.91 [268]~P8(x2681,x2681) % 0.56/0.91 [234]P1(f60(x2341)) % 0.56/0.91 [235]P5(f63(x2351)) % 0.56/0.91 [237]P6(f63(x2371)) % 0.56/0.91 [242]E(f91(a1,x2421),a1) % 0.56/0.91 [244]E(f93(x2441,a1),x2441) % 0.56/0.91 [245]E(f91(x2451,a1),x2451) % 0.56/0.91 [248]E(f93(x2481,x2481),x2481) % 0.56/0.91 [249]P7(x2491,f66(x2491)) % 0.56/0.91 [250]P7(x2501,f71(x2501)) % 0.56/0.91 [251]P2(x2511,f81(x2511)) % 0.56/0.91 [252]P2(f8(x2521),x2521) % 0.56/0.91 [253]P2(f60(x2531),f81(x2531)) % 0.56/0.91 [266]~P1(f81(x2661)) % 0.56/0.91 [267]~E(f97(x2671,x2671),a1) % 0.56/0.91 [238]E(f5(f63(x2381)),x2381) % 0.56/0.91 [239]E(f90(f81(x2391)),x2391) % 0.56/0.91 [240]E(f84(f63(x2401)),x2401) % 0.56/0.91 [256]E(f91(x2561,f91(x2561,a1)),a1) % 0.56/0.91 [259]E(f91(x2591,f91(x2591,x2591)),x2591) % 0.56/0.91 [254]E(f97(x2541,x2542),f97(x2542,x2541)) % 0.56/0.91 [255]E(f93(x2551,x2552),f93(x2552,x2551)) % 0.56/0.91 [257]P10(x2571,f93(x2571,x2572)) % 0.56/0.91 [258]P10(f91(x2581,x2582),x2581) % 0.56/0.91 [270]~P1(f97(x2701,x2702)) % 0.56/0.91 [260]E(f93(x2601,f91(x2602,x2601)),f93(x2601,x2602)) % 0.56/0.91 [261]E(f91(f93(x2611,x2612),x2612),f91(x2611,x2612)) % 0.56/0.91 [262]E(f91(x2621,f91(x2621,x2622)),f91(x2622,f91(x2622,x2621))) % 0.56/0.91 [273]~P1(x2731)+E(x2731,a1) % 0.56/0.91 [275]~P1(x2751)+P5(x2751) % 0.56/0.91 [276]~P1(x2761)+P6(x2761) % 0.56/0.91 [294]~P10(x2941,a1)+E(x2941,a1) % 0.56/0.91 [281]~P1(x2811)+P1(f5(x2811)) % 0.56/0.91 [282]~P1(x2821)+P1(f84(x2821)) % 0.56/0.91 [283]~P1(x2831)+P6(f5(x2831)) % 0.56/0.91 [284]~P1(x2841)+P6(f84(x2841)) % 0.56/0.91 [285]~P6(x2851)+P6(f85(x2851)) % 0.56/0.91 [291]P1(x2911)+~P1(f57(x2911)) % 0.56/0.91 [295]P7(f9(x2951),x2951)+E(x2951,a1) % 0.56/0.91 [296]P6(x2961)+P7(f10(x2961),x2961) % 0.56/0.91 [304]P1(x3041)+P2(f57(x3041),f81(x3041)) % 0.56/0.91 [288]~P6(x2881)+E(f85(f85(x2881)),x2881) % 0.56/0.91 [292]~P6(x2921)+E(f84(f85(x2921)),f5(x2921)) % 0.56/0.91 [293]~P6(x2931)+E(f5(f85(x2931)),f84(x2931)) % 0.56/0.91 [305]~P6(x3051)+E(f86(x3051,f5(x3051)),f84(x3051)) % 0.56/0.91 [316]~P6(x3161)+E(f93(f5(x3161),f84(x3161)),f88(x3161)) % 0.56/0.91 [401]~P6(x4011)+P10(x4011,f3(f5(x4011),f84(x4011))) % 0.56/0.91 [287]~E(x2871,x2872)+P10(x2871,x2872) % 0.56/0.91 [297]~P7(x2972,x2971)+~E(x2971,a1) % 0.56/0.91 [298]~P8(x2981,x2982)+~E(x2981,x2982) % 0.56/0.91 [303]~P1(x3031)+~P7(x3032,x3031) % 0.56/0.91 [311]~P8(x3111,x3112)+P10(x3111,x3112) % 0.56/0.91 [312]~P7(x3121,x3122)+P2(x3121,x3122) % 0.56/0.91 [313]~P3(x3132,x3131)+P3(x3131,x3132) % 0.56/0.91 [339]~P7(x3392,x3391)+~P7(x3391,x3392) % 0.56/0.91 [340]~P8(x3402,x3401)+~P8(x3401,x3402) % 0.56/0.91 [341]~P10(x3412,x3411)+~P8(x3411,x3412) % 0.56/0.91 [308]~P10(x3081,x3082)+E(f91(x3081,x3082),a1) % 0.56/0.91 [310]P10(x3101,x3102)+~E(f91(x3101,x3102),a1) % 0.56/0.91 [314]~P6(x3141)+P6(f87(x3141,x3142)) % 0.56/0.91 [315]~P6(x3152)+P6(f92(x3151,x3152)) % 0.56/0.91 [317]~P10(x3171,x3172)+E(f93(x3171,x3172),x3172) % 0.56/0.91 [318]~P3(x3181,x3182)+E(f91(x3181,x3182),x3181) % 0.56/0.91 [319]P3(x3191,x3192)+~E(f91(x3191,x3192),x3191) % 0.56/0.91 [329]~E(x3291,a1)+P10(x3291,f97(x3292,x3292)) % 0.56/0.91 [331]~P7(x3311,x3312)+P10(x3311,f90(x3312)) % 0.56/0.91 [332]~P10(x3321,x3322)+P2(x3321,f81(x3322)) % 0.56/0.91 [346]P10(x3461,x3462)+~P2(x3461,f81(x3462)) % 0.56/0.91 [347]~P6(x3471)+P10(f87(x3471,x3472),x3471) % 0.56/0.91 [348]~P6(x3482)+P10(f92(x3481,x3482),x3482) % 0.56/0.91 [353]P1(x3531)+~P1(f93(x3532,x3531)) % 0.56/0.91 [354]P1(x3541)+~P1(f93(x3541,x3542)) % 0.56/0.91 [356]~P6(x3561)+P10(f86(x3561,x3562),f84(x3561)) % 0.56/0.91 [357]~P6(x3571)+P10(f89(x3571,x3572),f5(x3571)) % 0.56/0.91 [358]P7(x3581,x3582)+P3(f97(x3581,x3581),x3582) % 0.56/0.91 [359]P10(x3591,x3592)+P7(f21(x3591,x3592),x3591) % 0.56/0.91 [360]P3(x3601,x3602)+P7(f72(x3601,x3602),x3602) % 0.56/0.91 [361]P3(x3611,x3612)+P7(f72(x3611,x3612),x3611) % 0.56/0.91 [364]P7(f81(x3641),f66(x3642))+~P7(x3641,f66(x3642)) % 0.56/0.91 [371]~P2(x3712,f81(x3711))+E(f95(x3711,x3712),f91(x3711,x3712)) % 0.56/0.91 [373]P7(f55(x3731,x3732),x3731)+P2(x3731,f81(x3732)) % 0.56/0.91 [380]~P7(x3801,x3802)+P10(f97(x3801,x3801),x3802) % 0.56/0.91 [415]P10(x4151,x4152)+~P7(f21(x4151,x4152),x4152) % 0.56/0.91 [416]~P7(x4162,f71(x4161))+P7(f77(x4161,x4162),f71(x4161)) % 0.56/0.91 [417]~P2(x4172,f81(x4171))+P2(f95(x4171,x4172),f81(x4171)) % 0.56/0.91 [422]~P7(f55(x4221,x4222),x4222)+P2(x4221,f81(x4222)) % 0.56/0.91 [429]~P7(x4291,x4292)+~P3(f97(x4291,x4291),x4292) % 0.56/0.91 [450]E(x4501,x4502)+~P10(f97(x4501,x4501),f97(x4502,x4502)) % 0.56/0.91 [321]~P6(x3212)+E(f83(f63(x3211),x3212),f87(x3212,x3211)) % 0.56/0.91 [362]P7(x3622,x3621)+E(f91(x3621,f97(x3622,x3622)),x3621) % 0.56/0.91 [378]~P3(x3781,x3782)+E(f91(x3781,f91(x3781,x3782)),a1) % 0.56/0.91 [384]~P10(x3841,x3842)+E(f93(x3841,f91(x3842,x3841)),x3842) % 0.56/0.91 [385]~P10(x3851,x3852)+E(f91(x3851,f91(x3851,x3852)),x3851) % 0.56/0.91 [387]~P7(x3871,x3872)+E(f93(f97(x3871,x3871),x3872),x3872) % 0.56/0.91 [397]E(f98(x3971,x3972),f90(x3972))+~P2(x3972,f81(f81(x3971))) % 0.56/0.91 [398]E(f82(x3981,x3982),f94(x3982))+~P2(x3982,f81(f81(x3981))) % 0.56/0.91 [402]~P2(x4022,f81(x4021))+E(f95(x4021,f95(x4021,x4022)),x4022) % 0.56/0.91 [410]P3(x4101,x4102)+~E(f91(x4101,f91(x4101,x4102)),a1) % 0.56/0.91 [418]~P6(x4182)+P10(f84(f92(x4181,x4182)),x4181) % 0.56/0.91 [423]~P6(x4231)+P10(f84(f87(x4231,x4232)),f84(x4231)) % 0.56/0.91 [424]~P6(x4242)+P10(f84(f92(x4241,x4242)),f84(x4242)) % 0.56/0.91 [431]~P7(x4312,x4311)+~E(f91(x4311,f97(x4312,x4312)),x4311) % 0.56/0.91 [437]~P2(x4372,f81(f81(x4371)))+E(f4(x4371,f4(x4371,x4372)),x4372) % 0.56/0.91 [445]P2(f98(x4451,x4452),f81(x4451))+~P2(x4452,f81(f81(x4451))) % 0.56/0.91 [446]P2(f82(x4461,x4462),f81(x4461))+~P2(x4462,f81(f81(x4461))) % 0.56/0.91 [451]~P2(x4512,f81(f81(x4511)))+P2(f4(x4511,x4512),f81(f81(x4511))) % 0.56/0.91 [465]P3(x4651,x4652)+P7(f73(x4651,x4652),f91(x4651,f91(x4651,x4652))) % 0.56/0.91 [441]~P6(x4411)+E(f91(f5(x4411),f91(f5(x4411),x4412)),f5(f87(x4411,x4412))) % 0.56/0.91 [442]~P6(x4421)+E(f91(f84(x4421),f91(f84(x4421),x4422)),f84(f92(x4422,x4421))) % 0.56/0.91 [477]~P6(x4771)+E(f86(x4771,f91(f5(x4771),f91(f5(x4771),x4772))),f86(x4771,x4772)) % 0.56/0.91 [344]E(x3441,x3442)+~E(f97(x3443,x3443),f97(x3441,x3442)) % 0.56/0.91 [345]E(x3451,x3452)+~E(f97(x3451,x3451),f97(x3452,x3453)) % 0.56/0.91 [411]P7(x4111,x4112)+~P10(f97(x4113,x4111),x4112) % 0.56/0.91 [412]P7(x4121,x4122)+~P10(f97(x4121,x4123),x4122) % 0.56/0.91 [432]~P10(x4321,x4323)+P10(f3(x4321,x4322),f3(x4323,x4322)) % 0.56/0.91 [433]~P10(x4332,x4333)+P10(f3(x4331,x4332),f3(x4331,x4333)) % 0.56/0.91 [434]~P10(x4341,x4343)+P10(f91(x4341,x4342),f91(x4343,x4342)) % 0.56/0.91 [430]~P6(x4302)+E(f92(x4301,f87(x4302,x4303)),f87(f92(x4301,x4302),x4303)) % 0.56/0.91 [458]P6(x4581)+~E(f10(x4581),f97(f97(x4582,x4583),f97(x4582,x4582))) % 0.56/0.91 [482]~P3(x4821,x4822)+~P7(x4823,f91(x4821,f91(x4821,x4822))) % 0.56/0.91 [492]~P10(x4921,x4923)+P10(f91(x4921,f91(x4921,x4922)),f91(x4923,f91(x4923,x4922))) % 0.56/0.91 [496]E(x4961,x4962)+~E(f97(f97(x4963,x4961),f97(x4963,x4963)),f97(f97(x4964,x4962),f97(x4964,x4964))) % 0.56/0.91 [497]E(x4971,x4972)+~E(f97(f97(x4971,x4973),f97(x4971,x4971)),f97(f97(x4972,x4974),f97(x4972,x4972))) % 0.56/0.91 [527]P7(x5271,x5272)+~P7(f97(f97(x5273,x5271),f97(x5273,x5273)),f3(x5274,x5272)) % 0.56/0.91 [529]P7(x5291,x5292)+~P7(f97(f97(x5291,x5293),f97(x5291,x5291)),f3(x5292,x5294)) % 0.56/0.91 [278]~P6(x2781)+E(x2781,a1)+~E(f5(x2781),a1) % 0.56/0.91 [279]~P6(x2791)+E(x2791,a1)+~E(f84(x2791),a1) % 0.56/0.91 [289]~P6(x2891)+~E(f84(x2891),a1)+E(f5(x2891),a1) % 0.56/0.91 [290]~P6(x2901)+~E(f5(x2901),a1)+E(f84(x2901),a1) % 0.56/0.91 [300]~P6(x3001)+P1(x3001)+~P1(f5(x3001)) % 0.56/0.91 [301]~P6(x3011)+P1(x3011)+~P1(f84(x3011)) % 0.56/0.91 [509]~P6(x5091)+E(x5091,a1)+P7(f97(f97(f75(x5091),f76(x5091)),f97(f75(x5091),f75(x5091))),x5091) % 0.56/0.91 [280]~P1(x2802)+~P1(x2801)+E(x2801,x2802) % 0.56/0.91 [302]~P1(x3022)+~P1(x3021)+P2(x3021,x3022) % 0.56/0.91 [306]~P2(x3061,x3062)+P1(x3061)+~P1(x3062) % 0.56/0.91 [320]P8(x3201,x3202)+~P10(x3201,x3202)+E(x3201,x3202) % 0.56/0.91 [323]~P2(x3232,x3231)+P1(x3231)+P7(x3232,x3231) % 0.56/0.91 [349]~P10(x3492,x3491)+~P10(x3491,x3492)+E(x3491,x3492) % 0.56/0.91 [274]~E(x2742,a1)+~E(x2741,a1)+E(x2741,f94(x2742)) % 0.56/0.91 [277]~E(x2771,f94(x2772))+E(x2771,a1)+~E(x2772,a1) % 0.56/0.91 [333]~P1(x3332)+~P6(x3331)+P1(f83(x3331,x3332)) % 0.56/0.91 [334]~P1(x3341)+~P6(x3342)+P1(f83(x3341,x3342)) % 0.56/0.91 [335]~P6(x3352)+~P6(x3351)+P6(f93(x3351,x3352)) % 0.56/0.91 [336]~P1(x3362)+~P6(x3361)+P6(f83(x3361,x3362)) % 0.56/0.91 [337]~P1(x3371)+~P6(x3372)+P6(f83(x3371,x3372)) % 0.56/0.91 [338]~P6(x3382)+~P6(x3381)+P6(f83(x3381,x3382)) % 0.56/0.91 [363]P1(x3631)+P1(x3632)+~P1(f3(x3632,x3631)) % 0.56/0.91 [400]E(f16(x4002,x4001),x4002)+P7(f16(x4002,x4001),x4001)+E(x4001,f97(x4002,x4002)) % 0.56/0.91 [403]P7(x4031,f66(x4032))+P4(x4031,f66(x4032))+~P10(x4031,f66(x4032)) % 0.56/0.91 [404]P7(x4041,f71(x4042))+P4(x4041,f71(x4042))+~P10(x4041,f71(x4042)) % 0.56/0.91 [420]E(x4201,f97(x4202,x4202))+~P10(x4201,f97(x4202,x4202))+E(x4201,a1) % 0.56/0.91 [421]E(x4211,x4212)+P7(f68(x4211,x4212),x4212)+P7(f68(x4211,x4212),x4211) % 0.56/0.91 [427]P7(f22(x4272,x4271),x4271)+P10(f22(x4272,x4271),x4272)+E(x4271,f81(x4272)) % 0.56/0.91 [428]P7(f35(x4282,x4281),x4281)+P7(f41(x4282,x4281),x4282)+E(x4281,f90(x4282)) % 0.56/0.91 [449]~E(f16(x4492,x4491),x4492)+~P7(f16(x4492,x4491),x4491)+E(x4491,f97(x4492,x4492)) % 0.56/0.91 [456]P7(f35(x4562,x4561),x4561)+P7(f35(x4562,x4561),f41(x4562,x4561))+E(x4561,f90(x4562)) % 0.56/0.91 [462]E(x4621,x4622)+~P7(f68(x4621,x4622),x4622)+~P7(f68(x4621,x4622),x4621) % 0.56/0.91 [464]~P7(f22(x4642,x4641),x4641)+~P10(f22(x4642,x4641),x4642)+E(x4641,f81(x4642)) % 0.56/0.91 [390]~P6(x3902)+~P6(x3901)+E(f84(f83(x3901,x3902)),f86(x3902,f84(x3901))) % 0.56/0.91 [409]E(x4091,a1)+~P2(x4091,f81(f81(x4092)))+~E(f4(x4092,x4091),a1) % 0.56/0.91 [438]~P6(x4382)+~P6(x4381)+P10(f5(f83(x4381,x4382)),f5(x4381)) % 0.56/0.91 [439]~P6(x4392)+~P6(x4391)+P10(f84(f83(x4391,x4392)),f84(x4392)) % 0.56/0.91 [444]~P6(x4442)+~P6(x4441)+P6(f91(x4441,f91(x4441,x4442))) % 0.56/0.91 [483]E(x4831,a1)+~P2(x4831,f81(f81(x4832)))+E(f96(x4832,x4832,f82(x4832,x4831)),f98(x4832,f4(x4832,x4831))) % 0.56/0.91 [484]E(x4841,a1)+~P2(x4841,f81(f81(x4842)))+E(f96(x4842,x4842,f98(x4842,x4841)),f82(x4842,f4(x4842,x4841))) % 0.56/0.91 [537]~P6(x5371)+~P7(x5372,x5371)+E(f97(f97(f14(x5371,x5372),f15(x5371,x5372)),f97(f14(x5371,x5372),f14(x5371,x5372))),x5372) % 0.56/0.91 [367]~P10(x3673,x3672)+P7(x3671,x3672)+~P7(x3671,x3673) % 0.56/0.91 [368]~P10(x3681,x3683)+P10(x3681,x3682)+~P10(x3683,x3682) % 0.56/0.91 [369]~P3(x3693,x3692)+P3(x3691,x3692)+~P10(x3691,x3693) % 0.56/0.91 [391]~P3(x3913,x3912)+~P7(x3911,x3912)+~P7(x3911,x3913) % 0.56/0.91 [342]~P10(x3421,x3423)+P7(x3421,x3422)+~E(x3422,f81(x3423)) % 0.56/0.91 [343]~P7(x3431,x3433)+P10(x3431,x3432)+~E(x3433,f81(x3432)) % 0.56/0.91 [351]~P7(x3511,x3513)+E(x3511,x3512)+~E(x3513,f97(x3512,x3512)) % 0.56/0.91 [377]~P1(x3771)+~P7(x3772,x3773)+~P2(x3773,f81(x3771)) % 0.56/0.91 [395]P7(x3951,x3952)+~P7(x3951,x3953)+~P2(x3953,f81(x3952)) % 0.56/0.91 [396]P2(x3961,x3962)+~P7(x3961,x3963)+~P2(x3963,f81(x3962)) % 0.56/0.91 [405]~P10(x4051,x4053)+P7(x4051,f66(x4052))+~P7(x4053,f66(x4052)) % 0.56/0.91 [406]~P10(x4061,x4063)+P7(x4061,f71(x4062))+~P7(x4063,f71(x4062)) % 0.56/0.91 [425]~P7(x4252,x4253)+~P7(x4251,x4253)+P10(f97(x4251,x4252),x4253) % 0.56/0.91 [426]~P10(x4262,x4263)+~P10(x4261,x4263)+P10(f93(x4261,x4262),x4263) % 0.56/0.91 [440]~P10(x4401,x4403)+~P7(x4403,f71(x4402))+P7(x4401,f77(x4402,x4403)) % 0.56/0.91 [443]~P6(x4431)+~P10(x4432,x4433)+P10(f89(x4431,x4432),f89(x4431,x4433)) % 0.56/0.91 [459]~P7(x4591,x4592)+~P7(x4591,f95(x4593,x4592))+~P2(x4592,f81(x4593)) % 0.56/0.91 [466]~P2(x4663,f81(x4661))+~P2(x4662,f81(x4661))+E(f96(x4661,x4662,x4663),f91(x4662,x4663)) % 0.56/0.91 [478]~P7(x4781,x4783)+~E(x4783,f90(x4782))+P7(x4781,f36(x4782,x4783,x4781)) % 0.56/0.91 [479]~P7(x4793,x4792)+~E(x4792,f90(x4791))+P7(f36(x4791,x4792,x4793),x4791) % 0.56/0.91 [489]~P6(x4893)+~P7(x4891,f86(x4893,x4892))+P7(f69(x4891,x4892,x4893),x4892) % 0.56/0.91 [490]~P6(x4903)+~P7(x4901,f89(x4903,x4902))+P7(f70(x4901,x4902,x4903),x4902) % 0.56/0.91 [491]~P2(x4913,f81(x4911))+~P2(x4912,f81(x4911))+P2(f96(x4911,x4912,x4913),f81(x4911)) % 0.56/0.91 [493]~P6(x4933)+~P7(x4931,f86(x4933,x4932))+P7(f69(x4931,x4932,x4933),f5(x4933)) % 0.56/0.91 [494]~P6(x4943)+~P7(x4941,f89(x4943,x4942))+P7(f70(x4941,x4942,x4943),f84(x4943)) % 0.56/0.91 [518]P7(f26(x5182,x5183,x5181),x5181)+P7(f30(x5182,x5183,x5181),x5182)+E(x5181,f3(x5182,x5183)) % 0.56/0.91 [519]P7(f26(x5192,x5193,x5191),x5191)+P7(f31(x5192,x5193,x5191),x5193)+E(x5191,f3(x5192,x5193)) % 0.56/0.91 [520]P7(f44(x5202,x5203,x5201),x5201)+P7(f44(x5202,x5203,x5201),x5202)+E(x5201,f91(x5202,x5203)) % 0.56/0.91 [533]~E(f23(x5332,x5333,x5331),x5333)+~P7(f23(x5332,x5333,x5331),x5331)+E(x5331,f97(x5332,x5333)) % 0.56/0.91 [534]~E(f23(x5342,x5343,x5341),x5342)+~P7(f23(x5342,x5343,x5341),x5341)+E(x5341,f97(x5342,x5343)) % 0.56/0.91 [539]P7(f44(x5392,x5393,x5391),x5391)+~P7(f44(x5392,x5393,x5391),x5393)+E(x5391,f91(x5392,x5393)) % 0.56/0.91 [545]~P7(f27(x5452,x5453,x5451),x5451)+~P7(f27(x5452,x5453,x5451),x5453)+E(x5451,f93(x5452,x5453)) % 0.56/0.91 [546]~P7(f27(x5462,x5463,x5461),x5461)+~P7(f27(x5462,x5463,x5461),x5462)+E(x5461,f93(x5462,x5463)) % 0.56/0.91 [463]~P10(x4632,x4633)+P7(x4631,x4632)+P10(x4632,f91(x4633,f97(x4631,x4631))) % 0.56/0.91 [469]P7(x4691,x4692)+~P6(x4693)+~P7(x4691,f5(f87(x4693,x4692))) % 0.56/0.91 [470]P7(x4701,x4702)+~P6(x4703)+~P7(x4701,f84(f92(x4702,x4703))) % 0.56/0.91 [471]~P10(x4711,x4713)+~P10(x4711,x4712)+P10(x4711,f91(x4712,f91(x4712,x4713))) % 0.56/0.91 [473]~P6(x4732)+P7(x4731,f5(x4732))+~P7(x4731,f5(f87(x4732,x4733))) % 0.56/0.91 [474]~P6(x4742)+P7(x4741,f84(x4742))+~P7(x4741,f84(f92(x4743,x4742))) % 0.56/0.91 [510]~P6(x5102)+P7(x5101,f5(x5102))+~P7(f97(f97(x5101,x5103),f97(x5101,x5101)),x5102) % 0.56/0.91 [511]~P6(x5112)+P7(x5111,f84(x5112))+~P7(f97(f97(x5113,x5111),f97(x5113,x5113)),x5112) % 0.56/0.91 [512]~P6(x5122)+P7(x5121,f88(x5122))+~P7(f97(f97(x5123,x5121),f97(x5123,x5123)),x5122) % 0.56/0.91 [513]~P6(x5132)+P7(x5131,f88(x5132))+~P7(f97(f97(x5131,x5133),f97(x5131,x5131)),x5132) % 0.56/0.91 [530]P7(f37(x5302,x5303,x5301),x5301)+P7(f37(x5302,x5303,x5301),x5303)+E(x5301,f91(x5302,f91(x5302,x5303))) % 0.56/0.91 [531]P7(f37(x5312,x5313,x5311),x5311)+P7(f37(x5312,x5313,x5311),x5312)+E(x5311,f91(x5312,f91(x5312,x5313))) % 0.56/0.91 [569]~P6(x5693)+~P7(x5691,f89(x5693,x5692))+P7(f97(f97(x5691,f70(x5691,x5692,x5693)),f97(x5691,x5691)),x5693) % 0.56/0.91 [575]P7(f26(x5752,x5753,x5751),x5751)+E(x5751,f3(x5752,x5753))+E(f97(f97(f30(x5752,x5753,x5751),f31(x5752,x5753,x5751)),f97(f30(x5752,x5753,x5751),f30(x5752,x5753,x5751))),f26(x5752,x5753,x5751)) % 0.56/0.91 [580]~P6(x5803)+~P7(x5801,f86(x5803,x5802))+P7(f97(f97(f69(x5801,x5802,x5803),x5801),f97(f69(x5801,x5802,x5803),f69(x5801,x5802,x5803))),x5803) % 0.56/0.91 [325]P7(x3251,x3252)+~E(x3251,x3253)+~E(x3252,f97(x3254,x3253)) % 0.56/0.91 [326]P7(x3261,x3262)+~E(x3261,x3263)+~E(x3262,f97(x3263,x3264)) % 0.56/0.91 [350]E(x3501,x3502)+E(x3501,x3503)+~E(f97(x3501,x3504),f97(x3503,x3502)) % 0.56/0.91 [374]~P7(x3741,x3744)+P7(x3741,x3742)+~E(x3742,f93(x3743,x3744)) % 0.56/0.91 [375]~P7(x3751,x3753)+P7(x3751,x3752)+~E(x3752,f93(x3753,x3754)) % 0.56/0.91 [376]~P7(x3761,x3763)+P7(x3761,x3762)+~E(x3763,f91(x3762,x3764)) % 0.56/0.91 [394]~P7(x3944,x3943)+~P7(x3944,x3941)+~E(x3941,f91(x3942,x3943)) % 0.56/0.91 [455]~P10(x4552,x4554)+~P10(x4551,x4553)+P10(f3(x4551,x4552),f3(x4553,x4554)) % 0.56/0.91 [558]~P7(x5584,x5583)+~E(x5583,f3(x5581,x5582))+P7(f28(x5581,x5582,x5583,x5584),x5581) % 0.56/0.91 [559]~P7(x5594,x5593)+~E(x5593,f3(x5591,x5592))+P7(f29(x5591,x5592,x5593,x5594),x5592) % 0.56/0.91 [447]~P7(x4471,x4473)+P7(x4471,x4472)+~E(x4473,f91(x4474,f91(x4474,x4472))) % 0.56/0.91 [502]~P7(x5022,x5024)+~P7(x5021,x5023)+P7(f97(f97(x5021,x5022),f97(x5021,x5021)),f3(x5023,x5024)) % 0.56/0.91 [538]P7(x5381,x5382)+~P6(x5383)+~P7(f97(f97(x5381,x5384),f97(x5381,x5381)),f83(f63(x5382),x5383)) % 0.56/0.91 [552]~P6(x5523)+P7(f97(f97(x5521,x5522),f97(x5521,x5521)),x5523)+~P7(f97(f97(x5521,x5522),f97(x5521,x5521)),f83(f63(x5524),x5523)) % 0.56/0.91 [593]~P7(x5934,x5933)+~E(x5933,f3(x5931,x5932))+E(f97(f97(f28(x5931,x5932,x5933,x5934),f29(x5931,x5932,x5933,x5934)),f97(f28(x5931,x5932,x5933,x5934),f28(x5931,x5932,x5933,x5934))),x5934) % 0.56/0.91 [299]~P5(x2991)+~P6(x2991)+~E(x2991,f63(x2992))+E(f5(x2991),x2992) % 0.56/0.91 [381]~P6(x3812)+~P10(x3811,f84(x3812))+E(x3811,a1)+~E(f89(x3812,x3811),a1) % 0.56/0.91 [382]~P6(x3822)+~P6(x3821)+~P10(x3821,x3822)+P10(f5(x3821),f5(x3822)) % 0.56/0.91 [383]~P6(x3832)+~P6(x3831)+~P10(x3831,x3832)+P10(f84(x3831),f84(x3832)) % 0.56/0.91 [453]P7(f19(x4531,x4532),x4531)+~P7(f17(x4531,x4532),x4532)+E(x4531,a1)+E(x4532,f94(x4531)) % 0.56/0.91 [485]~P7(f17(x4851,x4852),x4852)+~P7(f17(x4851,x4852),f19(x4851,x4852))+E(x4851,a1)+E(x4852,f94(x4851)) % 0.56/0.91 [435]~P6(x4352)+~P6(x4351)+~P10(f84(x4351),f5(x4352))+E(f5(f83(x4351,x4352)),f5(x4351)) % 0.56/0.91 [436]~P6(x4361)+~P6(x4362)+~P10(f5(x4362),f84(x4361))+E(f84(f83(x4361,x4362)),f84(x4362)) % 0.56/0.91 [562]~P6(x5622)+~P6(x5621)+P10(x5621,x5622)+P7(f97(f97(f33(x5621,x5622),f34(x5621,x5622)),f97(f33(x5621,x5622),f33(x5621,x5622))),x5621) % 0.56/0.91 [563]~P6(x5631)+E(f20(x5632,x5631),f32(x5632,x5631))+E(x5631,f63(x5632))+P7(f97(f97(f20(x5632,x5631),f32(x5632,x5631)),f97(f20(x5632,x5631),f20(x5632,x5631))),x5631) % 0.56/0.91 [565]~P6(x5651)+P7(f20(x5652,x5651),x5652)+E(x5651,f63(x5652))+P7(f97(f97(f20(x5652,x5651),f32(x5652,x5651)),f97(f20(x5652,x5651),f20(x5652,x5651))),x5651) % 0.56/0.91 [566]~P6(x5662)+P7(f39(x5662,x5661),x5661)+E(x5661,f5(x5662))+P7(f97(f97(f39(x5662,x5661),f40(x5662,x5661)),f97(f39(x5662,x5661),f39(x5662,x5661))),x5662) % 0.56/0.91 [567]~P6(x5672)+P7(f45(x5672,x5671),x5671)+E(x5671,f84(x5672))+P7(f97(f97(f47(x5672,x5671),f45(x5672,x5671)),f97(f47(x5672,x5671),f47(x5672,x5671))),x5672) % 0.56/0.91 [573]~P6(x5732)+~P6(x5731)+P10(x5731,x5732)+~P7(f97(f97(f33(x5731,x5732),f34(x5731,x5732)),f97(f33(x5731,x5732),f33(x5731,x5732))),x5732) % 0.56/0.91 [461]~P3(x4611,x4613)+~P2(x4613,f81(x4612))+~P2(x4611,f81(x4612))+P10(x4611,f95(x4612,x4613)) % 0.56/0.91 [475]P3(x4751,x4752)+~P10(x4751,f95(x4753,x4752))+~P2(x4752,f81(x4753))+~P2(x4751,f81(x4753)) % 0.56/0.91 [476]P7(x4762,x4763)+P7(f18(x4761,x4763,x4762),x4761)+~E(x4763,f94(x4761))+E(x4761,a1) % 0.56/0.91 [480]~P7(x4803,x4802)+~P7(f35(x4802,x4801),x4803)+~P7(f35(x4802,x4801),x4801)+E(x4801,f90(x4802)) % 0.56/0.91 [500]P7(x5002,x5003)+~E(x5003,f94(x5001))+~P7(x5002,f18(x5001,x5003,x5002))+E(x5001,a1) % 0.56/0.91 [508]E(f23(x5082,x5083,x5081),x5083)+E(f23(x5082,x5083,x5081),x5082)+P7(f23(x5082,x5083,x5081),x5081)+E(x5081,f97(x5082,x5083)) % 0.56/0.91 [522]~P6(x5222)+P7(f78(x5222,x5223,x5221),x5221)+P7(f80(x5222,x5223,x5221),x5223)+E(x5221,f86(x5222,x5223)) % 0.56/0.91 [523]~P6(x5232)+P7(f11(x5232,x5233,x5231),x5231)+P7(f13(x5232,x5233,x5231),x5233)+E(x5231,f89(x5232,x5233)) % 0.56/0.91 [542]P7(f27(x5422,x5423,x5421),x5421)+P7(f27(x5422,x5423,x5421),x5423)+P7(f27(x5422,x5423,x5421),x5422)+E(x5421,f93(x5422,x5423)) % 0.56/0.91 [557]P7(f44(x5572,x5573,x5571),x5573)+~P7(f44(x5572,x5573,x5571),x5571)+~P7(f44(x5572,x5573,x5571),x5572)+E(x5571,f91(x5572,x5573)) % 0.56/0.91 [467]~P6(x4672)+~P7(x4671,x4673)+~P7(x4671,f5(x4672))+P7(x4671,f5(f87(x4672,x4673))) % 0.56/0.91 [468]~P6(x4683)+~P7(x4681,x4682)+~P7(x4681,f84(x4683))+P7(x4681,f84(f92(x4682,x4683))) % 0.56/0.91 [507]P2(f43(x5072,x5073,x5071),f81(x5072))+E(x5071,f4(x5072,x5073))+~P2(x5071,f81(f81(x5072)))+~P2(x5073,f81(f81(x5072))) % 0.56/0.91 [514]~P5(x5142)+~P6(x5142)+E(x5141,f2(x5142,x5143))+~P7(f97(f97(x5143,x5141),f97(x5143,x5143)),x5142) % 0.56/0.91 [555]~P6(x5552)+~P7(f45(x5552,x5551),x5551)+E(x5551,f84(x5552))+~P7(f97(f97(x5553,f45(x5552,x5551)),f97(x5553,x5553)),x5552) % 0.56/0.91 [564]~P6(x5642)+~P7(x5641,x5643)+~E(x5643,f5(x5642))+P7(f97(f97(x5641,f38(x5642,x5643,x5641)),f97(x5641,x5641)),x5642) % 0.56/0.91 [568]~P7(f37(x5682,x5683,x5681),x5681)+~P7(f37(x5682,x5683,x5681),x5683)+~P7(f37(x5682,x5683,x5681),x5682)+E(x5681,f91(x5682,f91(x5682,x5683))) % 0.56/0.91 [572]~P6(x5722)+~P7(f39(x5722,x5721),x5721)+E(x5721,f5(x5722))+~P7(f97(f97(f39(x5722,x5721),x5723),f97(f39(x5722,x5721),f39(x5722,x5721))),x5722) % 0.56/0.91 [579]~P6(x5791)+~P7(x5793,x5792)+~E(x5792,f84(x5791))+P7(f97(f97(f46(x5791,x5792,x5793),x5793),f97(f46(x5791,x5792,x5793),f46(x5791,x5792,x5793))),x5791) % 0.56/0.91 [583]~P6(x5832)+P7(f78(x5832,x5833,x5831),x5831)+E(x5831,f86(x5832,x5833))+P7(f97(f97(f80(x5832,x5833,x5831),f78(x5832,x5833,x5831)),f97(f80(x5832,x5833,x5831),f80(x5832,x5833,x5831))),x5832) % 0.56/0.91 [584]~P6(x5842)+P7(f11(x5842,x5843,x5841),x5841)+E(x5841,f89(x5842,x5843))+P7(f97(f97(f11(x5842,x5843,x5841),f13(x5842,x5843,x5841)),f97(f11(x5842,x5843,x5841),f11(x5842,x5843,x5841))),x5842) % 0.56/0.91 [352]~P7(x3521,x3524)+E(x3521,x3522)+E(x3521,x3523)+~E(x3524,f97(x3523,x3522)) % 0.56/0.91 [392]~P7(x3921,x3924)+P7(x3921,x3922)+~P7(x3924,x3923)+~E(x3922,f90(x3923)) % 0.56/0.91 [407]~P7(x4071,x4074)+P7(x4071,x4072)+P7(x4071,x4073)+~E(x4072,f91(x4074,x4073)) % 0.56/0.91 [408]~P7(x4081,x4084)+P7(x4081,x4082)+P7(x4081,x4083)+~E(x4084,f93(x4083,x4082)) % 0.56/0.91 [560]~P6(x5601)+~P7(x5604,x5603)+~E(x5603,f86(x5601,x5602))+P7(f79(x5601,x5602,x5603,x5604),x5602) % 0.56/0.91 [561]~P6(x5611)+~P7(x5614,x5613)+~E(x5613,f89(x5611,x5612))+P7(f12(x5611,x5612,x5613,x5614),x5612) % 0.56/0.91 [460]~P7(x4601,x4604)+~P7(x4601,x4603)+P7(x4601,x4602)+~E(x4602,f91(x4603,f91(x4603,x4604))) % 0.56/0.91 [506]~P6(x5063)+E(x5061,x5062)+~E(x5063,f63(x5064))+~P7(f97(f97(x5061,x5062),f97(x5061,x5061)),x5063) % 0.56/0.91 [515]~P6(x5153)+P7(x5151,x5152)+~E(x5152,f84(x5153))+~P7(f97(f97(x5154,x5151),f97(x5154,x5154)),x5153) % 0.56/0.91 [516]~P6(x5163)+P7(x5161,x5162)+~E(x5162,f5(x5163))+~P7(f97(f97(x5161,x5164),f97(x5161,x5161)),x5163) % 0.56/0.91 [517]~P6(x5173)+P7(x5171,x5172)+~E(x5173,f63(x5172))+~P7(f97(f97(x5171,x5174),f97(x5171,x5171)),x5173) % 0.56/0.91 [553]~P6(x5534)+~P7(x5531,x5533)+~P7(f97(f97(x5531,x5532),f97(x5531,x5531)),x5534)+P7(f97(f97(x5531,x5532),f97(x5531,x5531)),f83(f63(x5533),x5534)) % 0.56/0.91 [587]~P6(x5872)+~P7(x5871,x5874)+~E(x5874,f89(x5872,x5873))+P7(f97(f97(x5871,f12(x5872,x5873,x5874,x5871)),f97(x5871,x5871)),x5872) % 0.56/0.91 [597]~P6(x5971)+~P7(x5974,x5973)+~E(x5973,f86(x5971,x5972))+P7(f97(f97(f79(x5971,x5972,x5973,x5974),x5974),f97(f79(x5971,x5972,x5973,x5974),f79(x5971,x5972,x5973,x5974))),x5971) % 0.56/0.91 [365]~P5(x3652)+~P5(x3651)+~P6(x3652)+~P6(x3651)+P5(f83(x3651,x3652)) % 0.56/0.91 [393]~P5(x3931)+~P6(x3931)+P7(f67(x3932,x3931),x3932)+~E(f5(x3931),x3932)+E(x3931,f63(x3932)) % 0.56/0.91 [457]~P5(x4571)+~P6(x4571)+~E(f5(x4571),x4572)+E(x4571,f63(x4572))+~E(f2(x4571,f67(x4572,x4571)),f67(x4572,x4571)) % 0.56/0.91 [574]~P6(x5741)+~E(f20(x5742,x5741),f32(x5742,x5741))+~P7(f20(x5742,x5741),x5742)+E(x5741,f63(x5742))+~P7(f97(f97(f20(x5742,x5741),f32(x5742,x5741)),f97(f20(x5742,x5741),f20(x5742,x5741))),x5741) % 0.56/0.91 [577]~P6(x5772)+~P6(x5771)+E(x5771,x5772)+P7(f97(f97(f24(x5771,x5772),f25(x5771,x5772)),f97(f24(x5771,x5772),f24(x5771,x5772))),x5772)+P7(f97(f97(f24(x5771,x5772),f25(x5771,x5772)),f97(f24(x5771,x5772),f24(x5771,x5772))),x5771) % 0.56/0.91 [578]~P6(x5781)+~P6(x5782)+E(x5781,f85(x5782))+P7(f97(f97(f48(x5782,x5781),f49(x5782,x5781)),f97(f48(x5782,x5781),f48(x5782,x5781))),x5781)+P7(f97(f97(f49(x5782,x5781),f48(x5782,x5781)),f97(f49(x5782,x5781),f49(x5782,x5781))),x5782) % 0.56/0.91 [581]~P6(x5812)+~P6(x5811)+E(x5811,x5812)+~P7(f97(f97(f24(x5811,x5812),f25(x5811,x5812)),f97(f24(x5811,x5812),f24(x5811,x5812))),x5812)+~P7(f97(f97(f24(x5811,x5812),f25(x5811,x5812)),f97(f24(x5811,x5812),f24(x5811,x5812))),x5811) % 0.56/0.91 [582]~P6(x5821)+~P6(x5822)+E(x5821,f85(x5822))+~P7(f97(f97(f48(x5822,x5821),f49(x5822,x5821)),f97(f48(x5822,x5821),f48(x5822,x5821))),x5821)+~P7(f97(f97(f49(x5822,x5821),f48(x5822,x5821)),f97(f49(x5822,x5821),f49(x5822,x5821))),x5822) % 0.56/0.91 [355]~P5(x3552)+~P6(x3552)+P7(x3553,f5(x3552))+~E(x3551,a1)+E(x3551,f2(x3552,x3553)) % 0.56/0.91 [370]~P5(x3703)+~P6(x3703)+~E(x3701,f2(x3703,x3702))+E(x3701,a1)+P7(x3702,f5(x3703)) % 0.56/0.91 [372]~P5(x3721)+~P6(x3721)+~P7(x3722,x3723)+E(f2(x3721,x3722),x3722)+~E(x3721,f63(x3723)) % 0.56/0.91 [452]~P7(x4523,x4521)+P7(f17(x4521,x4522),x4522)+E(x4521,a1)+E(x4522,f94(x4521))+P7(f17(x4521,x4522),x4523) % 0.56/0.91 [454]~P2(x4542,x4541)+P7(x4542,x4543)+P7(x4542,f95(x4541,x4543))+~P2(x4543,f81(x4541))+E(x4541,a1) % 0.56/0.91 [499]~P5(x4993)+~P6(x4993)+~E(x4992,f2(x4993,x4991))+~P7(x4991,f5(x4993))+P7(f97(f97(x4991,x4992),f97(x4991,x4991)),x4993) % 0.56/0.91 [556]P7(f43(x5562,x5563,x5561),x5561)+E(x5561,f4(x5562,x5563))+P7(f95(x5562,f43(x5562,x5563,x5561)),x5563)+~P2(x5561,f81(f81(x5562)))+~P2(x5563,f81(f81(x5562))) % 0.56/0.91 [571]~P7(f43(x5712,x5713,x5711),x5711)+E(x5711,f4(x5712,x5713))+~P2(x5711,f81(f81(x5712)))+~P2(x5713,f81(f81(x5712)))+~P7(f95(x5712,f43(x5712,x5713,x5711)),x5713) % 0.56/0.91 [585]~P6(x5851)+~P6(x5852)+P7(f42(x5852,x5853,x5851),x5853)+E(x5851,f87(x5852,x5853))+P7(f97(f97(f42(x5852,x5853,x5851),f50(x5852,x5853,x5851)),f97(f42(x5852,x5853,x5851),f42(x5852,x5853,x5851))),x5851) % 0.56/0.91 [586]~P6(x5861)+~P6(x5863)+P7(f74(x5862,x5863,x5861),x5862)+E(x5861,f92(x5862,x5863))+P7(f97(f97(f62(x5862,x5863,x5861),f74(x5862,x5863,x5861)),f97(f62(x5862,x5863,x5861),f62(x5862,x5863,x5861))),x5861) % 0.56/0.91 [589]~P6(x5891)+~P6(x5892)+E(x5891,f87(x5892,x5893))+P7(f97(f97(f42(x5892,x5893,x5891),f50(x5892,x5893,x5891)),f97(f42(x5892,x5893,x5891),f42(x5892,x5893,x5891))),x5891)+P7(f97(f97(f42(x5892,x5893,x5891),f50(x5892,x5893,x5891)),f97(f42(x5892,x5893,x5891),f42(x5892,x5893,x5891))),x5892) % 0.56/0.91 [590]~P6(x5901)+~P6(x5903)+E(x5901,f92(x5902,x5903))+P7(f97(f97(f62(x5902,x5903,x5901),f74(x5902,x5903,x5901)),f97(f62(x5902,x5903,x5901),f62(x5902,x5903,x5901))),x5901)+P7(f97(f97(f62(x5902,x5903,x5901),f74(x5902,x5903,x5901)),f97(f62(x5902,x5903,x5901),f62(x5902,x5903,x5901))),x5903) % 0.56/0.91 [399]~P7(x3993,x3991)+~P7(x3992,x3994)+P7(x3992,x3993)+E(x3991,a1)+~E(x3994,f94(x3991)) % 0.56/0.91 [486]~E(x4861,x4862)+~P6(x4863)+~P7(x4861,x4864)+~E(x4863,f63(x4864))+P7(f97(f97(x4861,x4862),f97(x4861,x4861)),x4863) % 0.56/0.91 [540]~P6(x5402)+~P7(x5404,x5403)+~P7(x5404,f5(x5402))+P7(x5401,f86(x5402,x5403))+~P7(f97(f97(x5404,x5401),f97(x5404,x5404)),x5402) % 0.56/0.91 [541]~P6(x5412)+~P7(x5414,x5413)+~P7(x5414,f84(x5412))+P7(x5411,f89(x5412,x5413))+~P7(f97(f97(x5411,x5414),f97(x5411,x5411)),x5412) % 0.56/0.91 [543]~P6(x5433)+~P6(x5434)+~E(x5433,f85(x5434))+~P7(f97(f97(x5432,x5431),f97(x5432,x5432)),x5434)+P7(f97(f97(x5431,x5432),f97(x5431,x5431)),x5433) % 0.56/0.91 [544]~P6(x5443)+~P6(x5444)+~E(x5444,f85(x5443))+~P7(f97(f97(x5442,x5441),f97(x5442,x5442)),x5444)+P7(f97(f97(x5441,x5442),f97(x5441,x5441)),x5443) % 0.56/0.91 [576]~P6(x5762)+~P7(x5764,x5763)+~P7(f78(x5762,x5763,x5761),x5761)+E(x5761,f86(x5762,x5763))+~P7(f97(f97(x5764,f78(x5762,x5763,x5761)),f97(x5764,x5764)),x5762) % 0.56/0.91 [588]~P6(x5882)+~P7(x5884,x5883)+~P7(f11(x5882,x5883,x5881),x5881)+E(x5881,f89(x5882,x5883))+~P7(f97(f97(f11(x5882,x5883,x5881),x5884),f97(f11(x5882,x5883,x5881),f11(x5882,x5883,x5881))),x5882) % 0.56/0.91 [524]~P6(x5244)+~P6(x5243)+P7(x5241,x5242)+~E(x5243,f87(x5244,x5242))+~P7(f97(f97(x5241,x5245),f97(x5241,x5241)),x5243) % 0.56/0.91 [525]~P6(x5254)+~P6(x5253)+P7(x5251,x5252)+~E(x5253,f92(x5252,x5254))+~P7(f97(f97(x5255,x5251),f97(x5255,x5255)),x5253) % 0.56/0.91 [535]~P6(x5353)+P7(x5351,x5352)+~P7(x5355,x5354)+~E(x5352,f86(x5353,x5354))+~P7(f97(f97(x5355,x5351),f97(x5355,x5355)),x5353) % 0.56/0.91 [536]~P6(x5363)+P7(x5361,x5362)+~P7(x5365,x5364)+~E(x5362,f89(x5363,x5364))+~P7(f97(f97(x5361,x5365),f97(x5361,x5361)),x5363) % 0.56/0.91 [548]~P6(x5484)+~P6(x5483)+~E(x5484,f87(x5483,x5485))+~P7(f97(f97(x5481,x5482),f97(x5481,x5481)),x5484)+P7(f97(f97(x5481,x5482),f97(x5481,x5481)),x5483) % 0.56/0.91 [549]~P6(x5494)+~P6(x5493)+~E(x5494,f92(x5495,x5493))+~P7(f97(f97(x5491,x5492),f97(x5491,x5491)),x5494)+P7(f97(f97(x5491,x5492),f97(x5491,x5491)),x5493) % 0.56/0.91 [554]~P7(x5545,x5543)+~P7(x5544,x5542)+~P7(f26(x5542,x5543,x5541),x5541)+E(x5541,f3(x5542,x5543))+~E(f26(x5542,x5543,x5541),f97(f97(x5544,x5545),f97(x5544,x5544))) % 0.56/0.91 [488]~P7(x4886,x4884)+~P7(x4885,x4883)+P7(x4881,x4882)+~E(x4882,f3(x4883,x4884))+~E(x4881,f97(f97(x4885,x4886),f97(x4885,x4885))) % 0.56/0.91 [472]~P5(x4722)+~P5(x4721)+~P6(x4722)+~P6(x4721)+~P7(x4723,f5(x4721))+E(f2(f83(x4721,x4722),x4723),f2(x4722,f2(x4721,x4723))) % 0.56/0.91 [481]~P5(x4812)+~P6(x4813)+~P6(x4812)+~P5(x4813)+P7(x4811,f5(x4812))+~P7(x4811,f5(f83(x4812,x4813))) % 0.56/0.91 [487]~P5(x4873)+~P5(x4871)+~P6(x4873)+~P6(x4871)+P7(f2(x4871,x4872),f5(x4873))+~P7(x4872,f5(f83(x4871,x4873))) % 0.56/0.91 [504]~P5(x5041)+~P5(x5042)+~P6(x5041)+~P6(x5042)+E(f2(f83(x5041,x5042),x5043),f2(x5042,f2(x5041,x5043)))+~P7(x5043,f5(f83(x5041,x5042))) % 0.56/0.91 [591]~P6(x5911)+~P6(x5913)+~P6(x5912)+E(x5911,f83(x5912,x5913))+P7(f97(f97(f51(x5912,x5913,x5911),f53(x5912,x5913,x5911)),f97(f51(x5912,x5913,x5911),f51(x5912,x5913,x5911))),x5911)+P7(f97(f97(f51(x5912,x5913,x5911),f54(x5912,x5913,x5911)),f97(f51(x5912,x5913,x5911),f51(x5912,x5913,x5911))),x5912) % 0.56/0.91 [592]~P6(x5921)+~P6(x5923)+~P6(x5922)+E(x5921,f83(x5922,x5923))+P7(f97(f97(f51(x5922,x5923,x5921),f53(x5922,x5923,x5921)),f97(f51(x5922,x5923,x5921),f51(x5922,x5923,x5921))),x5921)+P7(f97(f97(f54(x5922,x5923,x5921),f53(x5922,x5923,x5921)),f97(f54(x5922,x5923,x5921),f54(x5922,x5923,x5921))),x5923) % 0.56/0.91 [594]~P6(x5941)+~P6(x5942)+~P7(f42(x5942,x5943,x5941),x5943)+E(x5941,f87(x5942,x5943))+~P7(f97(f97(f42(x5942,x5943,x5941),f50(x5942,x5943,x5941)),f97(f42(x5942,x5943,x5941),f42(x5942,x5943,x5941))),x5941)+~P7(f97(f97(f42(x5942,x5943,x5941),f50(x5942,x5943,x5941)),f97(f42(x5942,x5943,x5941),f42(x5942,x5943,x5941))),x5942) % 0.56/0.91 [595]~P6(x5951)+~P6(x5953)+~P7(f74(x5952,x5953,x5951),x5952)+E(x5951,f92(x5952,x5953))+~P7(f97(f97(f62(x5952,x5953,x5951),f74(x5952,x5953,x5951)),f97(f62(x5952,x5953,x5951),f62(x5952,x5953,x5951))),x5951)+~P7(f97(f97(f62(x5952,x5953,x5951),f74(x5952,x5953,x5951)),f97(f62(x5952,x5953,x5951),f62(x5952,x5953,x5951))),x5953) % 0.56/0.91 [503]~P7(x5032,x5034)+~P2(x5032,f81(x5031))+P7(f95(x5031,x5032),x5033)+~E(x5034,f4(x5031,x5033))+~P2(x5033,f81(f81(x5031)))+~P2(x5034,f81(f81(x5031))) % 0.56/0.91 [505]P7(x5051,x5052)+~P2(x5051,f81(x5053))+~P7(f95(x5053,x5051),x5054)+~E(x5052,f4(x5053,x5054))+~P2(x5052,f81(f81(x5053)))+~P2(x5054,f81(f81(x5053))) % 0.56/0.91 [550]~P6(x5503)+~P6(x5505)+~P7(x5502,x5504)+~E(x5503,f92(x5504,x5505))+~P7(f97(f97(x5501,x5502),f97(x5501,x5501)),x5505)+P7(f97(f97(x5501,x5502),f97(x5501,x5501)),x5503) % 0.92/0.91 [551]~P6(x5513)+~P6(x5514)+~P7(x5511,x5515)+~E(x5513,f87(x5514,x5515))+~P7(f97(f97(x5511,x5512),f97(x5511,x5511)),x5514)+P7(f97(f97(x5511,x5512),f97(x5511,x5511)),x5513) % 0.92/0.91 [598]~P6(x5984)+~P6(x5983)+~P6(x5982)+~E(x5984,f83(x5982,x5983))+~P7(f97(f97(x5981,x5985),f97(x5981,x5981)),x5984)+P7(f97(f97(x5981,f52(x5982,x5983,x5984,x5981,x5985)),f97(x5981,x5981)),x5982) % 0.92/0.91 [599]~P6(x5993)+~P6(x5992)+~P6(x5991)+~E(x5993,f83(x5991,x5992))+~P7(f97(f97(x5994,x5995),f97(x5994,x5994)),x5993)+P7(f97(f97(f52(x5991,x5992,x5993,x5994,x5995),x5995),f97(f52(x5991,x5992,x5993,x5994,x5995),f52(x5991,x5992,x5993,x5994,x5995))),x5992) % 0.92/0.91 [495]~P5(x4953)+~P5(x4952)+~P6(x4953)+~P6(x4952)+~P7(x4951,f5(x4952))+~P7(f2(x4952,x4951),f5(x4953))+P7(x4951,f5(f83(x4952,x4953))) % 0.92/0.91 [596]~P6(x5961)+~P6(x5963)+~P6(x5962)+E(x5961,f83(x5962,x5963))+~P7(f97(f97(x5964,f53(x5962,x5963,x5961)),f97(x5964,x5964)),x5963)+~P7(f97(f97(f51(x5962,x5963,x5961),x5964),f97(f51(x5962,x5963,x5961),f51(x5962,x5963,x5961))),x5962)+~P7(f97(f97(f51(x5962,x5963,x5961),f53(x5962,x5963,x5961)),f97(f51(x5962,x5963,x5961),f51(x5962,x5963,x5961))),x5961) % 0.92/0.91 [570]~P6(x5703)+~P6(x5705)+~P6(x5704)+~E(x5703,f83(x5704,x5705))+~P7(f97(f97(x5701,x5706),f97(x5701,x5701)),x5704)+P7(f97(f97(x5701,x5702),f97(x5701,x5701)),x5703)+~P7(f97(f97(x5706,x5702),f97(x5706,x5706)),x5705) % 0.92/0.91 %EqnAxiom % 0.92/0.91 [1]E(x11,x11) % 0.92/0.91 [2]E(x22,x21)+~E(x21,x22) % 0.92/0.91 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.92/0.91 [4]~E(x41,x42)+E(f5(x41),f5(x42)) % 0.92/0.91 [5]~E(x51,x52)+E(f84(x51),f84(x52)) % 0.92/0.91 [6]~E(x61,x62)+E(f60(x61),f60(x62)) % 0.92/0.91 [7]~E(x71,x72)+E(f63(x71),f63(x72)) % 0.92/0.91 [8]~E(x81,x82)+E(f51(x81,x83,x84),f51(x82,x83,x84)) % 0.92/0.91 [9]~E(x91,x92)+E(f51(x93,x91,x94),f51(x93,x92,x94)) % 0.92/0.91 [10]~E(x101,x102)+E(f51(x103,x104,x101),f51(x103,x104,x102)) % 0.92/0.91 [11]~E(x111,x112)+E(f97(x111,x113),f97(x112,x113)) % 0.92/0.91 [12]~E(x121,x122)+E(f97(x123,x121),f97(x123,x122)) % 0.92/0.91 [13]~E(x131,x132)+E(f54(x131,x133,x134),f54(x132,x133,x134)) % 0.92/0.91 [14]~E(x141,x142)+E(f54(x143,x141,x144),f54(x143,x142,x144)) % 0.92/0.91 [15]~E(x151,x152)+E(f54(x153,x154,x151),f54(x153,x154,x152)) % 0.92/0.91 [16]~E(x161,x162)+E(f42(x161,x163,x164),f42(x162,x163,x164)) % 0.92/0.91 [17]~E(x171,x172)+E(f42(x173,x171,x174),f42(x173,x172,x174)) % 0.92/0.91 [18]~E(x181,x182)+E(f42(x183,x184,x181),f42(x183,x184,x182)) % 0.92/0.91 [19]~E(x191,x192)+E(f81(x191),f81(x192)) % 0.92/0.91 [20]~E(x201,x202)+E(f90(x201),f90(x202)) % 0.92/0.91 [21]~E(x211,x212)+E(f44(x211,x213,x214),f44(x212,x213,x214)) % 0.92/0.91 [22]~E(x221,x222)+E(f44(x223,x221,x224),f44(x223,x222,x224)) % 0.92/0.91 [23]~E(x231,x232)+E(f44(x233,x234,x231),f44(x233,x234,x232)) % 0.92/0.91 [24]~E(x241,x242)+E(f62(x241,x243,x244),f62(x242,x243,x244)) % 0.92/0.91 [25]~E(x251,x252)+E(f62(x253,x251,x254),f62(x253,x252,x254)) % 0.92/0.91 [26]~E(x261,x262)+E(f62(x263,x264,x261),f62(x263,x264,x262)) % 0.92/0.91 [27]~E(x271,x272)+E(f91(x271,x273),f91(x272,x273)) % 0.92/0.91 [28]~E(x281,x282)+E(f91(x283,x281),f91(x283,x282)) % 0.92/0.91 [29]~E(x291,x292)+E(f93(x291,x293),f93(x292,x293)) % 0.92/0.91 [30]~E(x301,x302)+E(f93(x303,x301),f93(x303,x302)) % 0.92/0.91 [31]~E(x311,x312)+E(f79(x311,x313,x314,x315),f79(x312,x313,x314,x315)) % 0.92/0.91 [32]~E(x321,x322)+E(f79(x323,x321,x324,x325),f79(x323,x322,x324,x325)) % 0.92/0.91 [33]~E(x331,x332)+E(f79(x333,x334,x331,x335),f79(x333,x334,x332,x335)) % 0.92/0.91 [34]~E(x341,x342)+E(f79(x343,x344,x345,x341),f79(x343,x344,x345,x342)) % 0.92/0.91 [35]~E(x351,x352)+E(f14(x351,x353),f14(x352,x353)) % 0.92/0.91 [36]~E(x361,x362)+E(f14(x363,x361),f14(x363,x362)) % 0.92/0.91 [37]~E(x371,x372)+E(f27(x371,x373,x374),f27(x372,x373,x374)) % 0.92/0.91 [38]~E(x381,x382)+E(f27(x383,x381,x384),f27(x383,x382,x384)) % 0.92/0.91 [39]~E(x391,x392)+E(f27(x393,x394,x391),f27(x393,x394,x392)) % 0.92/0.91 [40]~E(x401,x402)+E(f69(x401,x403,x404),f69(x402,x403,x404)) % 0.92/0.91 [41]~E(x411,x412)+E(f69(x413,x411,x414),f69(x413,x412,x414)) % 0.92/0.91 [42]~E(x421,x422)+E(f69(x423,x424,x421),f69(x423,x424,x422)) % 0.92/0.91 [43]~E(x431,x432)+E(f66(x431),f66(x432)) % 0.92/0.91 [44]~E(x441,x442)+E(f71(x441),f71(x442)) % 0.92/0.91 [45]~E(x451,x452)+E(f23(x451,x453,x454),f23(x452,x453,x454)) % 0.92/0.91 [46]~E(x461,x462)+E(f23(x463,x461,x464),f23(x463,x462,x464)) % 0.92/0.91 [47]~E(x471,x472)+E(f23(x473,x474,x471),f23(x473,x474,x472)) % 0.92/0.91 [48]~E(x481,x482)+E(f8(x481),f8(x482)) % 0.92/0.91 [49]~E(x491,x492)+E(f50(x491,x493,x494),f50(x492,x493,x494)) % 0.92/0.91 [50]~E(x501,x502)+E(f50(x503,x501,x504),f50(x503,x502,x504)) % 0.92/0.91 [51]~E(x511,x512)+E(f50(x513,x514,x511),f50(x513,x514,x512)) % 0.92/0.91 [52]~E(x521,x522)+E(f86(x521,x523),f86(x522,x523)) % 0.92/0.91 [53]~E(x531,x532)+E(f86(x533,x531),f86(x533,x532)) % 0.92/0.91 [54]~E(x541,x542)+E(f17(x541,x543),f17(x542,x543)) % 0.92/0.91 [55]~E(x551,x552)+E(f17(x553,x551),f17(x553,x552)) % 0.92/0.91 [56]~E(x561,x562)+E(f87(x561,x563),f87(x562,x563)) % 0.92/0.91 [57]~E(x571,x572)+E(f87(x573,x571),f87(x573,x572)) % 0.92/0.91 [58]~E(x581,x582)+E(f53(x581,x583,x584),f53(x582,x583,x584)) % 0.92/0.91 [59]~E(x591,x592)+E(f53(x593,x591,x594),f53(x593,x592,x594)) % 0.92/0.91 [60]~E(x601,x602)+E(f53(x603,x604,x601),f53(x603,x604,x602)) % 0.92/0.91 [61]~E(x611,x612)+E(f78(x611,x613,x614),f78(x612,x613,x614)) % 0.92/0.91 [62]~E(x621,x622)+E(f78(x623,x621,x624),f78(x623,x622,x624)) % 0.92/0.91 [63]~E(x631,x632)+E(f78(x633,x634,x631),f78(x633,x634,x632)) % 0.92/0.91 [64]~E(x641,x642)+E(f3(x641,x643),f3(x642,x643)) % 0.92/0.91 [65]~E(x651,x652)+E(f3(x653,x651),f3(x653,x652)) % 0.92/0.91 [66]~E(x661,x662)+E(f43(x661,x663,x664),f43(x662,x663,x664)) % 0.92/0.91 [67]~E(x671,x672)+E(f43(x673,x671,x674),f43(x673,x672,x674)) % 0.92/0.91 [68]~E(x681,x682)+E(f43(x683,x684,x681),f43(x683,x684,x682)) % 0.92/0.91 [69]~E(x691,x692)+E(f70(x691,x693,x694),f70(x692,x693,x694)) % 0.92/0.91 [70]~E(x701,x702)+E(f70(x703,x701,x704),f70(x703,x702,x704)) % 0.92/0.91 [71]~E(x711,x712)+E(f70(x713,x714,x711),f70(x713,x714,x712)) % 0.92/0.91 [72]~E(x721,x722)+E(f4(x721,x723),f4(x722,x723)) % 0.92/0.91 [73]~E(x731,x732)+E(f4(x733,x731),f4(x733,x732)) % 0.92/0.91 [74]~E(x741,x742)+E(f32(x741,x743),f32(x742,x743)) % 0.92/0.91 [75]~E(x751,x752)+E(f32(x753,x751),f32(x753,x752)) % 0.92/0.91 [76]~E(x761,x762)+E(f20(x761,x763),f20(x762,x763)) % 0.92/0.91 [77]~E(x771,x772)+E(f20(x773,x771),f20(x773,x772)) % 0.92/0.91 [78]~E(x781,x782)+E(f26(x781,x783,x784),f26(x782,x783,x784)) % 0.92/0.91 [79]~E(x791,x792)+E(f26(x793,x791,x794),f26(x793,x792,x794)) % 0.92/0.91 [80]~E(x801,x802)+E(f26(x803,x804,x801),f26(x803,x804,x802)) % 0.92/0.91 [81]~E(x811,x812)+E(f31(x811,x813,x814),f31(x812,x813,x814)) % 0.92/0.91 [82]~E(x821,x822)+E(f31(x823,x821,x824),f31(x823,x822,x824)) % 0.92/0.91 [83]~E(x831,x832)+E(f31(x833,x834,x831),f31(x833,x834,x832)) % 0.92/0.91 [84]~E(x841,x842)+E(f39(x841,x843),f39(x842,x843)) % 0.92/0.91 [85]~E(x851,x852)+E(f39(x853,x851),f39(x853,x852)) % 0.92/0.91 [86]~E(x861,x862)+E(f95(x861,x863),f95(x862,x863)) % 0.92/0.91 [87]~E(x871,x872)+E(f95(x873,x871),f95(x873,x872)) % 0.92/0.91 [88]~E(x881,x882)+E(f83(x881,x883),f83(x882,x883)) % 0.92/0.91 [89]~E(x891,x892)+E(f83(x893,x891),f83(x893,x892)) % 0.92/0.91 [90]~E(x901,x902)+E(f11(x901,x903,x904),f11(x902,x903,x904)) % 0.92/0.91 [91]~E(x911,x912)+E(f11(x913,x911,x914),f11(x913,x912,x914)) % 0.92/0.91 [92]~E(x921,x922)+E(f11(x923,x924,x921),f11(x923,x924,x922)) % 0.92/0.91 [93]~E(x931,x932)+E(f29(x931,x933,x934,x935),f29(x932,x933,x934,x935)) % 0.92/0.91 [94]~E(x941,x942)+E(f29(x943,x941,x944,x945),f29(x943,x942,x944,x945)) % 0.92/0.91 [95]~E(x951,x952)+E(f29(x953,x954,x951,x955),f29(x953,x954,x952,x955)) % 0.92/0.91 [96]~E(x961,x962)+E(f29(x963,x964,x965,x961),f29(x963,x964,x965,x962)) % 0.92/0.91 [97]~E(x971,x972)+E(f30(x971,x973,x974),f30(x972,x973,x974)) % 0.92/0.91 [98]~E(x981,x982)+E(f30(x983,x981,x984),f30(x983,x982,x984)) % 0.92/0.91 [99]~E(x991,x992)+E(f30(x993,x994,x991),f30(x993,x994,x992)) % 0.92/0.91 [100]~E(x1001,x1002)+E(f28(x1001,x1003,x1004,x1005),f28(x1002,x1003,x1004,x1005)) % 0.92/0.91 [101]~E(x1011,x1012)+E(f28(x1013,x1011,x1014,x1015),f28(x1013,x1012,x1014,x1015)) % 0.92/0.91 [102]~E(x1021,x1022)+E(f28(x1023,x1024,x1021,x1025),f28(x1023,x1024,x1022,x1025)) % 0.92/0.91 [103]~E(x1031,x1032)+E(f28(x1033,x1034,x1035,x1031),f28(x1033,x1034,x1035,x1032)) % 0.92/0.91 [104]~E(x1041,x1042)+E(f77(x1041,x1043),f77(x1042,x1043)) % 0.92/0.91 [105]~E(x1051,x1052)+E(f77(x1053,x1051),f77(x1053,x1052)) % 0.92/0.91 [106]~E(x1061,x1062)+E(f68(x1061,x1063),f68(x1062,x1063)) % 0.92/0.91 [107]~E(x1071,x1072)+E(f68(x1073,x1071),f68(x1073,x1072)) % 0.92/0.91 [108]~E(x1081,x1082)+E(f45(x1081,x1083),f45(x1082,x1083)) % 0.92/0.91 [109]~E(x1091,x1092)+E(f45(x1093,x1091),f45(x1093,x1092)) % 0.92/0.91 [110]~E(x1101,x1102)+E(f85(x1101),f85(x1102)) % 0.92/0.91 [111]~E(x1111,x1112)+E(f22(x1111,x1113),f22(x1112,x1113)) % 0.92/0.91 [112]~E(x1121,x1122)+E(f22(x1123,x1121),f22(x1123,x1122)) % 0.92/0.91 [113]~E(x1131,x1132)+E(f49(x1131,x1133),f49(x1132,x1133)) % 0.92/0.91 [114]~E(x1141,x1142)+E(f49(x1143,x1141),f49(x1143,x1142)) % 0.92/0.91 [115]~E(x1151,x1152)+E(f2(x1151,x1153),f2(x1152,x1153)) % 0.92/0.91 [116]~E(x1161,x1162)+E(f2(x1163,x1161),f2(x1163,x1162)) % 0.92/0.91 [117]~E(x1171,x1172)+E(f33(x1171,x1173),f33(x1172,x1173)) % 0.92/0.91 [118]~E(x1181,x1182)+E(f33(x1183,x1181),f33(x1183,x1182)) % 0.92/0.91 [119]~E(x1191,x1192)+E(f48(x1191,x1193),f48(x1192,x1193)) % 0.92/0.91 [120]~E(x1201,x1202)+E(f48(x1203,x1201),f48(x1203,x1202)) % 0.92/0.91 [121]~E(x1211,x1212)+E(f89(x1211,x1213),f89(x1212,x1213)) % 0.92/0.91 [122]~E(x1221,x1222)+E(f89(x1223,x1221),f89(x1223,x1222)) % 0.92/0.91 [123]~E(x1231,x1232)+E(f10(x1231),f10(x1232)) % 0.92/0.91 [124]~E(x1241,x1242)+E(f12(x1241,x1243,x1244,x1245),f12(x1242,x1243,x1244,x1245)) % 0.92/0.91 [125]~E(x1251,x1252)+E(f12(x1253,x1251,x1254,x1255),f12(x1253,x1252,x1254,x1255)) % 0.92/0.91 [126]~E(x1261,x1262)+E(f12(x1263,x1264,x1261,x1265),f12(x1263,x1264,x1262,x1265)) % 0.92/0.91 [127]~E(x1271,x1272)+E(f12(x1273,x1274,x1275,x1271),f12(x1273,x1274,x1275,x1272)) % 0.92/0.91 [128]~E(x1281,x1282)+E(f94(x1281),f94(x1282)) % 0.92/0.91 [129]~E(x1291,x1292)+E(f96(x1291,x1293,x1294),f96(x1292,x1293,x1294)) % 0.92/0.91 [130]~E(x1301,x1302)+E(f96(x1303,x1301,x1304),f96(x1303,x1302,x1304)) % 0.92/0.91 [131]~E(x1311,x1312)+E(f96(x1313,x1314,x1311),f96(x1313,x1314,x1312)) % 0.92/0.91 [132]~E(x1321,x1322)+E(f74(x1321,x1323,x1324),f74(x1322,x1323,x1324)) % 0.92/0.91 [133]~E(x1331,x1332)+E(f74(x1333,x1331,x1334),f74(x1333,x1332,x1334)) % 0.92/0.91 [134]~E(x1341,x1342)+E(f74(x1343,x1344,x1341),f74(x1343,x1344,x1342)) % 0.92/0.91 [135]~E(x1351,x1352)+E(f24(x1351,x1353),f24(x1352,x1353)) % 0.92/0.91 [136]~E(x1361,x1362)+E(f24(x1363,x1361),f24(x1363,x1362)) % 0.92/0.91 [137]~E(x1371,x1372)+E(f75(x1371),f75(x1372)) % 0.92/0.91 [138]~E(x1381,x1382)+E(f92(x1381,x1383),f92(x1382,x1383)) % 0.92/0.91 [139]~E(x1391,x1392)+E(f92(x1393,x1391),f92(x1393,x1392)) % 0.92/0.91 [140]~E(x1401,x1402)+E(f52(x1401,x1403,x1404,x1405,x1406),f52(x1402,x1403,x1404,x1405,x1406)) % 0.92/0.91 [141]~E(x1411,x1412)+E(f52(x1413,x1411,x1414,x1415,x1416),f52(x1413,x1412,x1414,x1415,x1416)) % 0.92/0.91 [142]~E(x1421,x1422)+E(f52(x1423,x1424,x1421,x1425,x1426),f52(x1423,x1424,x1422,x1425,x1426)) % 0.92/0.91 [143]~E(x1431,x1432)+E(f52(x1433,x1434,x1435,x1431,x1436),f52(x1433,x1434,x1435,x1432,x1436)) % 0.92/0.91 [144]~E(x1441,x1442)+E(f52(x1443,x1444,x1445,x1446,x1441),f52(x1443,x1444,x1445,x1446,x1442)) % 0.92/0.91 [145]~E(x1451,x1452)+E(f37(x1451,x1453,x1454),f37(x1452,x1453,x1454)) % 0.92/0.91 [146]~E(x1461,x1462)+E(f37(x1463,x1461,x1464),f37(x1463,x1462,x1464)) % 0.92/0.91 [147]~E(x1471,x1472)+E(f37(x1473,x1474,x1471),f37(x1473,x1474,x1472)) % 0.92/0.91 [148]~E(x1481,x1482)+E(f16(x1481,x1483),f16(x1482,x1483)) % 0.92/0.91 [149]~E(x1491,x1492)+E(f16(x1493,x1491),f16(x1493,x1492)) % 0.92/0.91 [150]~E(x1501,x1502)+E(f88(x1501),f88(x1502)) % 0.92/0.91 [151]~E(x1511,x1512)+E(f36(x1511,x1513,x1514),f36(x1512,x1513,x1514)) % 0.92/0.91 [152]~E(x1521,x1522)+E(f36(x1523,x1521,x1524),f36(x1523,x1522,x1524)) % 0.92/0.91 [153]~E(x1531,x1532)+E(f36(x1533,x1534,x1531),f36(x1533,x1534,x1532)) % 0.92/0.91 [154]~E(x1541,x1542)+E(f98(x1541,x1543),f98(x1542,x1543)) % 0.92/0.91 [155]~E(x1551,x1552)+E(f98(x1553,x1551),f98(x1553,x1552)) % 0.92/0.91 [156]~E(x1561,x1562)+E(f35(x1561,x1563),f35(x1562,x1563)) % 0.92/0.91 [157]~E(x1571,x1572)+E(f35(x1573,x1571),f35(x1573,x1572)) % 0.92/0.91 [158]~E(x1581,x1582)+E(f41(x1581,x1583),f41(x1582,x1583)) % 0.92/0.91 [159]~E(x1591,x1592)+E(f41(x1593,x1591),f41(x1593,x1592)) % 0.92/0.91 [160]~E(x1601,x1602)+E(f82(x1601,x1603),f82(x1602,x1603)) % 0.92/0.91 [161]~E(x1611,x1612)+E(f82(x1613,x1611),f82(x1613,x1612)) % 0.92/0.91 [162]~E(x1621,x1622)+E(f57(x1621),f57(x1622)) % 0.92/0.91 [163]~E(x1631,x1632)+E(f67(x1631,x1633),f67(x1632,x1633)) % 0.92/0.91 [164]~E(x1641,x1642)+E(f67(x1643,x1641),f67(x1643,x1642)) % 0.92/0.91 [165]~E(x1651,x1652)+E(f15(x1651,x1653),f15(x1652,x1653)) % 0.92/0.91 [166]~E(x1661,x1662)+E(f15(x1663,x1661),f15(x1663,x1662)) % 0.92/0.91 [167]~E(x1671,x1672)+E(f18(x1671,x1673,x1674),f18(x1672,x1673,x1674)) % 0.92/0.91 [168]~E(x1681,x1682)+E(f18(x1683,x1681,x1684),f18(x1683,x1682,x1684)) % 0.92/0.91 [169]~E(x1691,x1692)+E(f18(x1693,x1694,x1691),f18(x1693,x1694,x1692)) % 0.92/0.91 [170]~E(x1701,x1702)+E(f21(x1701,x1703),f21(x1702,x1703)) % 0.92/0.91 [171]~E(x1711,x1712)+E(f21(x1713,x1711),f21(x1713,x1712)) % 0.92/0.91 [172]~E(x1721,x1722)+E(f38(x1721,x1723,x1724),f38(x1722,x1723,x1724)) % 0.92/0.91 [173]~E(x1731,x1732)+E(f38(x1733,x1731,x1734),f38(x1733,x1732,x1734)) % 0.92/0.91 [174]~E(x1741,x1742)+E(f38(x1743,x1744,x1741),f38(x1743,x1744,x1742)) % 0.92/0.91 [175]~E(x1751,x1752)+E(f19(x1751,x1753),f19(x1752,x1753)) % 0.92/0.91 [176]~E(x1761,x1762)+E(f19(x1763,x1761),f19(x1763,x1762)) % 0.92/0.91 [177]~E(x1771,x1772)+E(f9(x1771),f9(x1772)) % 0.92/0.91 [178]~E(x1781,x1782)+E(f34(x1781,x1783),f34(x1782,x1783)) % 0.92/0.91 [179]~E(x1791,x1792)+E(f34(x1793,x1791),f34(x1793,x1792)) % 0.92/0.91 [180]~E(x1801,x1802)+E(f72(x1801,x1803),f72(x1802,x1803)) % 0.92/0.91 [181]~E(x1811,x1812)+E(f72(x1813,x1811),f72(x1813,x1812)) % 0.92/0.91 [182]~E(x1821,x1822)+E(f25(x1821,x1823),f25(x1822,x1823)) % 0.92/0.91 [183]~E(x1831,x1832)+E(f25(x1833,x1831),f25(x1833,x1832)) % 0.92/0.91 [184]~E(x1841,x1842)+E(f73(x1841,x1843),f73(x1842,x1843)) % 0.92/0.91 [185]~E(x1851,x1852)+E(f73(x1853,x1851),f73(x1853,x1852)) % 0.92/0.91 [186]~E(x1861,x1862)+E(f80(x1861,x1863,x1864),f80(x1862,x1863,x1864)) % 0.92/0.91 [187]~E(x1871,x1872)+E(f80(x1873,x1871,x1874),f80(x1873,x1872,x1874)) % 0.92/0.91 [188]~E(x1881,x1882)+E(f80(x1883,x1884,x1881),f80(x1883,x1884,x1882)) % 0.92/0.91 [189]~E(x1891,x1892)+E(f46(x1891,x1893,x1894),f46(x1892,x1893,x1894)) % 0.92/0.91 [190]~E(x1901,x1902)+E(f46(x1903,x1901,x1904),f46(x1903,x1902,x1904)) % 0.92/0.91 [191]~E(x1911,x1912)+E(f46(x1913,x1914,x1911),f46(x1913,x1914,x1912)) % 0.92/0.91 [192]~E(x1921,x1922)+E(f47(x1921,x1923),f47(x1922,x1923)) % 0.92/0.91 [193]~E(x1931,x1932)+E(f47(x1933,x1931),f47(x1933,x1932)) % 0.92/0.91 [194]~E(x1941,x1942)+E(f76(x1941),f76(x1942)) % 0.92/0.91 [195]~E(x1951,x1952)+E(f55(x1951,x1953),f55(x1952,x1953)) % 0.92/0.91 [196]~E(x1961,x1962)+E(f55(x1963,x1961),f55(x1963,x1962)) % 0.92/0.91 [197]~E(x1971,x1972)+E(f40(x1971,x1973),f40(x1972,x1973)) % 0.92/0.91 [198]~E(x1981,x1982)+E(f40(x1983,x1981),f40(x1983,x1982)) % 0.92/0.91 [199]~E(x1991,x1992)+E(f13(x1991,x1993,x1994),f13(x1992,x1993,x1994)) % 0.92/0.91 [200]~E(x2001,x2002)+E(f13(x2003,x2001,x2004),f13(x2003,x2002,x2004)) % 0.92/0.91 [201]~E(x2011,x2012)+E(f13(x2013,x2014,x2011),f13(x2013,x2014,x2012)) % 0.92/0.91 [202]~P1(x2021)+P1(x2022)+~E(x2021,x2022) % 0.92/0.91 [203]P7(x2032,x2033)+~E(x2031,x2032)+~P7(x2031,x2033) % 0.92/0.91 [204]P7(x2043,x2042)+~E(x2041,x2042)+~P7(x2043,x2041) % 0.92/0.91 [205]~P6(x2051)+P6(x2052)+~E(x2051,x2052) % 0.92/0.91 [206]P10(x2062,x2063)+~E(x2061,x2062)+~P10(x2061,x2063) % 0.92/0.91 [207]P10(x2073,x2072)+~E(x2071,x2072)+~P10(x2073,x2071) % 0.92/0.91 [208]P2(x2082,x2083)+~E(x2081,x2082)+~P2(x2081,x2083) % 0.92/0.91 [209]P2(x2093,x2092)+~E(x2091,x2092)+~P2(x2093,x2091) % 0.92/0.91 [210]~P5(x2101)+P5(x2102)+~E(x2101,x2102) % 0.92/0.91 [211]P8(x2112,x2113)+~E(x2111,x2112)+~P8(x2111,x2113) % 0.92/0.91 [212]P8(x2123,x2122)+~E(x2121,x2122)+~P8(x2123,x2121) % 0.92/0.91 [213]P3(x2132,x2133)+~E(x2131,x2132)+~P3(x2131,x2133) % 0.92/0.91 [214]P3(x2143,x2142)+~E(x2141,x2142)+~P3(x2143,x2141) % 0.92/0.91 [215]P4(x2152,x2153)+~E(x2151,x2152)+~P4(x2151,x2153) % 0.92/0.91 [216]P4(x2163,x2162)+~E(x2161,x2162)+~P4(x2163,x2161) % 0.92/0.91 [217]~P9(x2171)+P9(x2172)+~E(x2171,x2172) % 0.92/0.91 % 0.92/0.91 %------------------------------------------- % 0.92/0.91 cnf(614,plain, % 0.92/0.91 (~P6(f63(x6141))+~P5(f63(x6141))+~P7(x6142,x6141)+E(f2(f63(x6141),x6142),x6142)), % 0.92/0.91 inference(equality_inference,[],[372])). % 0.92/0.91 cnf(661,plain, % 0.92/0.91 ($false), % 0.92/0.91 inference(scs_inference,[],[237,235,241,269,614]), % 0.92/0.91 ['proof']). % 0.92/0.91 % SZS output end Proof % 0.92/0.91 % Total time :0.080000s %------------------------------------------------------------------------------