%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU177+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 : n022.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 15:01:34 EDT 2024 % Result : Theorem 0.53s 0.83s % Output : CNFRefutation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SEU177+2 : TPTP v8.2.0. Released v3.3.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.31 % Computer : n022.cluster.edu % 0.12/0.31 % Model : x86_64 x86_64 % 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.31 % Memory : 8042.1875MB % 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.31 % CPULimit : 300 % 0.12/0.31 % WCLimit : 300 % 0.12/0.31 % DateTime : Fri Jun 21 18:13:39 EDT 2024 % 0.12/0.31 % CPUTime : % 0.52/0.55 start to proof:theBenchmark % 0.53/0.80 %------------------------------------------- % 0.53/0.80 % File :CSE---1.7 % 0.53/0.80 % Problem :theBenchmark % 0.53/0.80 % Transform :cnf % 0.53/0.80 % Format :tptp:raw % 0.53/0.80 % Command :java -jar mcs_scs.jar %d %s % 0.53/0.80 % 0.53/0.80 % Result :Theorem 0.150000s % 0.53/0.80 % Output :CNFRefutation 0.150000s % 0.53/0.80 %------------------------------------------- % 0.53/0.81 %------------------------------------------------------------------------------ % 0.53/0.81 % File : SEU177+2 : TPTP v8.2.0. Released v3.3.0. % 0.53/0.81 % Domain : Set theory % 0.53/0.81 % Problem : MPTP chainy problem t20_relat_1 % 0.53/0.81 % Version : [Urb07] axioms : Especial. % 0.53/0.81 % English : % 0.53/0.81 % 0.53/0.81 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.53/0.81 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.53/0.81 % Source : [Urb07] % 0.53/0.81 % Names : chainy-t20_relat_1 [Urb07] % 0.53/0.81 % 0.53/0.81 % Status : Theorem % 0.53/0.81 % Rating : 0.25 v8.2.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.17 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.21 v6.2.0, 0.32 v6.1.0, 0.30 v6.0.0, 0.39 v5.5.0, 0.30 v5.4.0, 0.29 v5.3.0, 0.30 v5.2.0, 0.10 v5.0.0, 0.21 v4.1.0, 0.22 v4.0.1, 0.26 v4.0.0, 0.29 v3.7.0, 0.25 v3.5.0, 0.26 v3.4.0, 0.32 v3.3.0 % 0.53/0.81 % Syntax : Number of formulae : 142 ( 47 unt; 0 def) % 0.53/0.81 % Number of atoms : 330 ( 83 equ) % 0.53/0.81 % Maximal formula atoms : 11 ( 2 avg) % 0.53/0.81 % Number of connectives : 242 ( 54 ~; 6 |; 59 &) % 0.53/0.81 % ( 46 <=>; 77 =>; 0 <=; 0 <~>) % 0.53/0.81 % Maximal formula depth : 14 ( 5 avg) % 0.53/0.81 % Maximal term depth : 3 ( 1 avg) % 0.53/0.81 % Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty) % 0.53/0.81 % Number of functors : 19 ( 19 usr; 1 con; 0-3 aty) % 0.53/0.81 % Number of variables : 306 ( 291 !; 15 ?) % 0.53/0.81 % SPC : FOF_THM_RFO_SEQ % 0.53/0.81 % 0.53/0.81 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.53/0.81 % library, www.mizar.org % 0.53/0.81 %------------------------------------------------------------------------------ % 0.53/0.81 fof(antisymmetry_r2_hidden,axiom, % 0.53/0.81 ! [A,B] : % 0.53/0.81 ( in(A,B) % 0.53/0.81 => ~ in(B,A) ) ). % 0.53/0.81 % 0.53/0.81 fof(antisymmetry_r2_xboole_0,axiom, % 0.53/0.81 ! [A,B] : % 0.53/0.81 ( proper_subset(A,B) % 0.53/0.81 => ~ proper_subset(B,A) ) ). % 0.53/0.81 % 0.53/0.81 fof(commutativity_k2_tarski,axiom, % 0.53/0.81 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 0.53/0.81 % 0.53/0.81 fof(commutativity_k2_xboole_0,axiom, % 0.53/0.81 ! [A,B] : set_union2(A,B) = set_union2(B,A) ). % 0.53/0.81 % 0.53/0.81 fof(commutativity_k3_xboole_0,axiom, % 0.53/0.81 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 0.53/0.81 % 0.53/0.81 fof(d10_xboole_0,axiom, % 0.53/0.81 ! [A,B] : % 0.53/0.81 ( A = B % 0.53/0.81 <=> ( subset(A,B) % 0.53/0.81 & subset(B,A) ) ) ). % 0.53/0.81 % 0.53/0.81 fof(d1_setfam_1,axiom, % 0.53/0.81 ! [A,B] : % 0.53/0.81 ( ( A != empty_set % 0.53/0.81 => ( B = set_meet(A) % 0.53/0.81 <=> ! [C] : % 0.53/0.81 ( in(C,B) % 0.53/0.81 <=> ! [D] : % 0.53/0.81 ( in(D,A) % 0.53/0.81 => in(C,D) ) ) ) ) % 0.53/0.81 & ( A = empty_set % 0.53/0.81 => ( B = set_meet(A) % 0.53/0.81 <=> B = empty_set ) ) ) ). % 0.53/0.81 % 0.53/0.81 fof(d1_tarski,axiom, % 0.53/0.81 ! [A,B] : % 0.53/0.81 ( B = singleton(A) % 0.53/0.81 <=> ! [C] : % 0.53/0.81 ( in(C,B) % 0.53/0.81 <=> C = A ) ) ). % 0.53/0.81 % 0.53/0.81 fof(d1_xboole_0,axiom, % 0.53/0.81 ! [A] : % 0.53/0.81 ( A = empty_set % 0.53/0.81 <=> ! [B] : ~ in(B,A) ) ). % 0.53/0.81 % 0.53/0.81 fof(d1_zfmisc_1,axiom, % 0.53/0.81 ! [A,B] : % 0.53/0.81 ( B = powerset(A) % 0.53/0.81 <=> ! [C] : % 0.53/0.81 ( in(C,B) % 0.53/0.81 <=> subset(C,A) ) ) ). % 0.53/0.81 % 0.53/0.81 fof(d2_subset_1,axiom, % 0.53/0.81 ! [A,B] : % 0.53/0.81 ( ( ~ empty(A) % 0.53/0.81 => ( element(B,A) % 0.53/0.81 <=> in(B,A) ) ) % 0.53/0.81 & ( empty(A) % 0.53/0.81 => ( element(B,A) % 0.53/0.81 <=> empty(B) ) ) ) ). % 0.53/0.81 % 0.53/0.81 fof(d2_tarski,axiom, % 0.53/0.81 ! [A,B,C] : % 0.53/0.81 ( C = unordered_pair(A,B) % 0.53/0.81 <=> ! [D] : % 0.53/0.81 ( in(D,C) % 0.53/0.81 <=> ( D = A % 0.53/0.81 | D = B ) ) ) ). % 0.53/0.81 % 0.53/0.81 fof(d2_xboole_0,axiom, % 0.53/0.81 ! [A,B,C] : % 0.53/0.81 ( C = set_union2(A,B) % 0.53/0.81 <=> ! [D] : % 0.53/0.81 ( in(D,C) % 0.53/0.81 <=> ( in(D,A) % 0.53/0.81 | in(D,B) ) ) ) ). % 0.53/0.81 % 0.53/0.81 fof(d2_zfmisc_1,axiom, % 0.53/0.81 ! [A,B,C] : % 0.53/0.81 ( C = cartesian_product2(A,B) % 0.53/0.81 <=> ! [D] : % 0.53/0.81 ( in(D,C) % 0.53/0.81 <=> ? [E,F] : % 0.53/0.81 ( in(E,A) % 0.53/0.81 & in(F,B) % 0.53/0.81 & D = ordered_pair(E,F) ) ) ) ). % 0.53/0.81 % 0.53/0.81 fof(d3_tarski,axiom, % 0.53/0.81 ! [A,B] : % 0.53/0.81 ( subset(A,B) % 0.53/0.81 <=> ! [C] : % 0.53/0.81 ( in(C,A) % 0.53/0.81 => in(C,B) ) ) ). % 0.53/0.81 % 0.53/0.81 fof(d3_xboole_0,axiom, % 0.53/0.81 ! [A,B,C] : % 0.53/0.81 ( C = set_intersection2(A,B) % 0.53/0.81 <=> ! [D] : % 0.53/0.81 ( in(D,C) % 0.53/0.81 <=> ( in(D,A) % 0.53/0.81 & in(D,B) ) ) ) ). % 0.53/0.81 % 0.53/0.81 fof(d4_relat_1,axiom, % 0.53/0.81 ! [A] : % 0.53/0.81 ( relation(A) % 0.53/0.81 => ! [B] : % 0.53/0.81 ( B = relation_dom(A) % 0.53/0.81 <=> ! [C] : % 0.53/0.81 ( in(C,B) % 0.53/0.81 <=> ? [D] : in(ordered_pair(C,D),A) ) ) ) ). % 0.53/0.81 % 0.53/0.81 fof(d4_subset_1,axiom, % 0.53/0.81 ! [A] : cast_to_subset(A) = A ). % 0.53/0.81 % 0.53/0.81 fof(d4_tarski,axiom, % 0.53/0.81 ! [A,B] : % 0.53/0.81 ( B = union(A) % 0.53/0.81 <=> ! [C] : % 0.53/0.82 ( in(C,B) % 0.53/0.82 <=> ? [D] : % 0.53/0.82 ( in(C,D) % 0.53/0.82 & in(D,A) ) ) ) ). % 0.53/0.82 % 0.53/0.82 fof(d4_xboole_0,axiom, % 0.53/0.82 ! [A,B,C] : % 0.53/0.82 ( C = set_difference(A,B) % 0.53/0.82 <=> ! [D] : % 0.53/0.82 ( in(D,C) % 0.53/0.82 <=> ( in(D,A) % 0.53/0.82 & ~ in(D,B) ) ) ) ). % 0.53/0.82 % 0.53/0.82 fof(d5_relat_1,axiom, % 0.53/0.82 ! [A] : % 0.53/0.82 ( relation(A) % 0.53/0.82 => ! [B] : % 0.53/0.82 ( B = relation_rng(A) % 0.53/0.82 <=> ! [C] : % 0.53/0.82 ( in(C,B) % 0.53/0.82 <=> ? [D] : in(ordered_pair(D,C),A) ) ) ) ). % 0.53/0.82 % 0.53/0.82 fof(d5_subset_1,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( element(B,powerset(A)) % 0.53/0.82 => subset_complement(A,B) = set_difference(A,B) ) ). % 0.53/0.82 % 0.53/0.82 fof(d5_tarski,axiom, % 0.53/0.82 ! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) ). % 0.53/0.82 % 0.53/0.82 fof(d7_xboole_0,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( disjoint(A,B) % 0.53/0.82 <=> set_intersection2(A,B) = empty_set ) ). % 0.53/0.82 % 0.53/0.82 fof(d8_setfam_1,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( element(B,powerset(powerset(A))) % 0.53/0.82 => ! [C] : % 0.53/0.82 ( element(C,powerset(powerset(A))) % 0.53/0.82 => ( C = complements_of_subsets(A,B) % 0.53/0.82 <=> ! [D] : % 0.53/0.82 ( element(D,powerset(A)) % 0.53/0.82 => ( in(D,C) % 0.53/0.82 <=> in(subset_complement(A,D),B) ) ) ) ) ) ). % 0.53/0.82 % 0.53/0.82 fof(d8_xboole_0,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( proper_subset(A,B) % 0.53/0.82 <=> ( subset(A,B) % 0.53/0.82 & A != B ) ) ). % 0.53/0.82 % 0.53/0.82 fof(dt_k1_relat_1,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(dt_k1_setfam_1,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(dt_k1_tarski,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(dt_k1_xboole_0,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(dt_k1_zfmisc_1,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(dt_k2_relat_1,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(dt_k2_subset_1,axiom, % 0.53/0.82 ! [A] : element(cast_to_subset(A),powerset(A)) ). % 0.53/0.82 % 0.53/0.82 fof(dt_k2_tarski,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(dt_k2_xboole_0,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(dt_k2_zfmisc_1,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(dt_k3_subset_1,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( element(B,powerset(A)) % 0.53/0.82 => element(subset_complement(A,B),powerset(A)) ) ). % 0.53/0.82 % 0.53/0.82 fof(dt_k3_tarski,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(dt_k3_xboole_0,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(dt_k4_tarski,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(dt_k4_xboole_0,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(dt_k5_setfam_1,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( element(B,powerset(powerset(A))) % 0.53/0.82 => element(union_of_subsets(A,B),powerset(A)) ) ). % 0.53/0.82 % 0.53/0.82 fof(dt_k6_setfam_1,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( element(B,powerset(powerset(A))) % 0.53/0.82 => element(meet_of_subsets(A,B),powerset(A)) ) ). % 0.53/0.82 % 0.53/0.82 fof(dt_k6_subset_1,axiom, % 0.53/0.82 ! [A,B,C] : % 0.53/0.82 ( ( element(B,powerset(A)) % 0.53/0.82 & element(C,powerset(A)) ) % 0.53/0.82 => element(subset_difference(A,B,C),powerset(A)) ) ). % 0.53/0.82 % 0.53/0.82 fof(dt_k7_setfam_1,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( element(B,powerset(powerset(A))) % 0.53/0.82 => element(complements_of_subsets(A,B),powerset(powerset(A))) ) ). % 0.53/0.82 % 0.53/0.82 fof(dt_m1_subset_1,axiom, % 0.53/0.82 $true ). % 0.53/0.82 % 0.53/0.82 fof(existence_m1_subset_1,axiom, % 0.53/0.82 ! [A] : % 0.53/0.82 ? [B] : element(B,A) ). % 0.53/0.82 % 0.53/0.82 fof(fc1_subset_1,axiom, % 0.53/0.82 ! [A] : ~ empty(powerset(A)) ). % 0.53/0.82 % 0.53/0.82 fof(fc1_xboole_0,axiom, % 0.53/0.82 empty(empty_set) ). % 0.53/0.82 % 0.53/0.82 fof(fc1_zfmisc_1,axiom, % 0.53/0.82 ! [A,B] : ~ empty(ordered_pair(A,B)) ). % 0.53/0.82 % 0.53/0.82 fof(fc2_subset_1,axiom, % 0.53/0.82 ! [A] : ~ empty(singleton(A)) ). % 0.53/0.82 % 0.53/0.82 fof(fc2_xboole_0,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( ~ empty(A) % 0.53/0.82 => ~ empty(set_union2(A,B)) ) ). % 0.53/0.82 % 0.53/0.82 fof(fc3_subset_1,axiom, % 0.53/0.82 ! [A,B] : ~ empty(unordered_pair(A,B)) ). % 0.53/0.82 % 0.53/0.82 fof(fc3_xboole_0,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( ~ empty(A) % 0.53/0.82 => ~ empty(set_union2(B,A)) ) ). % 0.53/0.82 % 0.53/0.82 fof(idempotence_k2_xboole_0,axiom, % 0.53/0.82 ! [A,B] : set_union2(A,A) = A ). % 0.53/0.82 % 0.53/0.82 fof(idempotence_k3_xboole_0,axiom, % 0.53/0.82 ! [A,B] : set_intersection2(A,A) = A ). % 0.53/0.82 % 0.53/0.82 fof(involutiveness_k3_subset_1,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( element(B,powerset(A)) % 0.53/0.82 => subset_complement(A,subset_complement(A,B)) = B ) ). % 0.53/0.82 % 0.53/0.82 fof(involutiveness_k7_setfam_1,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( element(B,powerset(powerset(A))) % 0.53/0.82 => complements_of_subsets(A,complements_of_subsets(A,B)) = B ) ). % 0.53/0.82 % 0.53/0.82 fof(irreflexivity_r2_xboole_0,axiom, % 0.53/0.82 ! [A,B] : ~ proper_subset(A,A) ). % 0.53/0.82 % 0.53/0.82 fof(l1_zfmisc_1,lemma, % 0.53/0.82 ! [A] : singleton(A) != empty_set ). % 0.53/0.82 % 0.53/0.82 fof(l23_zfmisc_1,lemma, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( in(A,B) % 0.53/0.82 => set_union2(singleton(A),B) = B ) ). % 0.53/0.82 % 0.53/0.82 fof(l25_zfmisc_1,lemma, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ~ ( disjoint(singleton(A),B) % 0.53/0.82 & in(A,B) ) ). % 0.53/0.82 % 0.53/0.82 fof(l28_zfmisc_1,lemma, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( ~ in(A,B) % 0.53/0.82 => disjoint(singleton(A),B) ) ). % 0.53/0.82 % 0.53/0.82 fof(l2_zfmisc_1,lemma, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( subset(singleton(A),B) % 0.53/0.82 <=> in(A,B) ) ). % 0.53/0.82 % 0.53/0.82 fof(l32_xboole_1,lemma, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( set_difference(A,B) = empty_set % 0.53/0.82 <=> subset(A,B) ) ). % 0.53/0.82 % 0.53/0.82 fof(l3_subset_1,lemma, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( element(B,powerset(A)) % 0.53/0.82 => ! [C] : % 0.53/0.82 ( in(C,B) % 0.53/0.82 => in(C,A) ) ) ). % 0.53/0.82 % 0.53/0.82 fof(l3_zfmisc_1,lemma, % 0.53/0.82 ! [A,B,C] : % 0.53/0.82 ( subset(A,B) % 0.53/0.82 => ( in(C,A) % 0.53/0.82 | subset(A,set_difference(B,singleton(C))) ) ) ). % 0.53/0.82 % 0.53/0.82 fof(l4_zfmisc_1,lemma, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( subset(A,singleton(B)) % 0.53/0.82 <=> ( A = empty_set % 0.53/0.82 | A = singleton(B) ) ) ). % 0.53/0.82 % 0.53/0.82 fof(l50_zfmisc_1,lemma, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( in(A,B) % 0.53/0.82 => subset(A,union(B)) ) ). % 0.53/0.82 % 0.53/0.82 fof(l55_zfmisc_1,lemma, % 0.53/0.82 ! [A,B,C,D] : % 0.53/0.82 ( in(ordered_pair(A,B),cartesian_product2(C,D)) % 0.53/0.82 <=> ( in(A,C) % 0.53/0.82 & in(B,D) ) ) ). % 0.53/0.82 % 0.53/0.82 fof(l71_subset_1,lemma, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( ! [C] : % 0.53/0.82 ( in(C,A) % 0.53/0.82 => in(C,B) ) % 0.53/0.82 => element(A,powerset(B)) ) ). % 0.53/0.82 % 0.53/0.82 fof(rc1_relat_1,axiom, % 0.53/0.82 ? [A] : % 0.53/0.82 ( empty(A) % 0.53/0.82 & relation(A) ) ). % 0.53/0.82 % 0.53/0.82 fof(rc1_subset_1,axiom, % 0.53/0.82 ! [A] : % 0.53/0.82 ( ~ empty(A) % 0.53/0.82 => ? [B] : % 0.53/0.82 ( element(B,powerset(A)) % 0.53/0.82 & ~ empty(B) ) ) ). % 0.53/0.82 % 0.53/0.82 fof(rc1_xboole_0,axiom, % 0.53/0.82 ? [A] : empty(A) ). % 0.53/0.82 % 0.53/0.82 fof(rc2_subset_1,axiom, % 0.53/0.82 ! [A] : % 0.53/0.82 ? [B] : % 0.53/0.82 ( element(B,powerset(A)) % 0.53/0.82 & empty(B) ) ). % 0.53/0.82 % 0.53/0.82 fof(rc2_xboole_0,axiom, % 0.53/0.82 ? [A] : ~ empty(A) ). % 0.53/0.82 % 0.53/0.82 fof(redefinition_k5_setfam_1,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( element(B,powerset(powerset(A))) % 0.53/0.82 => union_of_subsets(A,B) = union(B) ) ). % 0.53/0.82 % 0.53/0.82 fof(redefinition_k6_setfam_1,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( element(B,powerset(powerset(A))) % 0.53/0.82 => meet_of_subsets(A,B) = set_meet(B) ) ). % 0.53/0.82 % 0.53/0.82 fof(redefinition_k6_subset_1,axiom, % 0.53/0.82 ! [A,B,C] : % 0.53/0.82 ( ( element(B,powerset(A)) % 0.53/0.82 & element(C,powerset(A)) ) % 0.53/0.82 => subset_difference(A,B,C) = set_difference(B,C) ) ). % 0.53/0.82 % 0.53/0.82 fof(reflexivity_r1_tarski,axiom, % 0.53/0.82 ! [A,B] : subset(A,A) ). % 0.53/0.82 % 0.53/0.82 fof(symmetry_r1_xboole_0,axiom, % 0.53/0.82 ! [A,B] : % 0.53/0.82 ( disjoint(A,B) % 0.53/0.82 => disjoint(B,A) ) ). % 0.53/0.82 % 0.53/0.82 fof(t106_zfmisc_1,lemma, % 0.53/0.82 ! [A,B,C,D] : % 0.53/0.82 ( in(ordered_pair(A,B),cartesian_product2(C,D)) % 0.53/0.82 <=> ( in(A,C) % 0.53/0.82 & in(B,D) ) ) ). % 0.53/0.82 % 0.53/0.82 fof(t10_zfmisc_1,lemma, % 0.53/0.82 ! [A,B,C,D] : % 0.53/0.82 ~ ( unordered_pair(A,B) = unordered_pair(C,D) % 0.53/0.82 & A != C % 0.53/0.82 & A != D ) ). % 0.53/0.82 % 0.53/0.82 fof(t118_zfmisc_1,lemma, % 0.53/0.82 ! [A,B,C] : % 0.53/0.82 ( subset(A,B) % 0.53/0.82 => ( subset(cartesian_product2(A,C),cartesian_product2(B,C)) % 0.53/0.82 & subset(cartesian_product2(C,A),cartesian_product2(C,B)) ) ) ). % 0.53/0.82 % 0.53/0.82 fof(t119_zfmisc_1,lemma, % 0.53/0.82 ! [A,B,C,D] : % 0.53/0.82 ( ( subset(A,B) % 0.53/0.83 & subset(C,D) ) % 0.53/0.83 => subset(cartesian_product2(A,C),cartesian_product2(B,D)) ) ). % 0.53/0.83 % 0.53/0.83 fof(t12_xboole_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( subset(A,B) % 0.53/0.83 => set_union2(A,B) = B ) ). % 0.53/0.83 % 0.53/0.83 fof(t136_zfmisc_1,lemma, % 0.53/0.83 ! [A] : % 0.53/0.83 ? [B] : % 0.53/0.83 ( in(A,B) % 0.53/0.83 & ! [C,D] : % 0.53/0.83 ( ( in(C,B) % 0.53/0.83 & subset(D,C) ) % 0.53/0.83 => in(D,B) ) % 0.53/0.83 & ! [C] : % 0.53/0.83 ( in(C,B) % 0.53/0.83 => in(powerset(C),B) ) % 0.53/0.83 & ! [C] : % 0.53/0.83 ~ ( subset(C,B) % 0.53/0.83 & ~ are_equipotent(C,B) % 0.53/0.83 & ~ in(C,B) ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t17_xboole_1,lemma, % 0.53/0.83 ! [A,B] : subset(set_intersection2(A,B),A) ). % 0.53/0.83 % 0.53/0.83 fof(t19_xboole_1,lemma, % 0.53/0.83 ! [A,B,C] : % 0.53/0.83 ( ( subset(A,B) % 0.53/0.83 & subset(A,C) ) % 0.53/0.83 => subset(A,set_intersection2(B,C)) ) ). % 0.53/0.83 % 0.53/0.83 fof(t1_boole,axiom, % 0.53/0.83 ! [A] : set_union2(A,empty_set) = A ). % 0.53/0.83 % 0.53/0.83 fof(t1_subset,axiom, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( in(A,B) % 0.53/0.83 => element(A,B) ) ). % 0.53/0.83 % 0.53/0.83 fof(t1_xboole_1,lemma, % 0.53/0.83 ! [A,B,C] : % 0.53/0.83 ( ( subset(A,B) % 0.53/0.83 & subset(B,C) ) % 0.53/0.83 => subset(A,C) ) ). % 0.53/0.83 % 0.53/0.83 fof(t1_zfmisc_1,lemma, % 0.53/0.83 powerset(empty_set) = singleton(empty_set) ). % 0.53/0.83 % 0.53/0.83 fof(t20_relat_1,conjecture, % 0.53/0.83 ! [A,B,C] : % 0.53/0.83 ( relation(C) % 0.53/0.83 => ( in(ordered_pair(A,B),C) % 0.53/0.83 => ( in(A,relation_dom(C)) % 0.53/0.83 & in(B,relation_rng(C)) ) ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t26_xboole_1,lemma, % 0.53/0.83 ! [A,B,C] : % 0.53/0.83 ( subset(A,B) % 0.53/0.83 => subset(set_intersection2(A,C),set_intersection2(B,C)) ) ). % 0.53/0.83 % 0.53/0.83 fof(t28_xboole_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( subset(A,B) % 0.53/0.83 => set_intersection2(A,B) = A ) ). % 0.53/0.83 % 0.53/0.83 fof(t2_boole,axiom, % 0.53/0.83 ! [A] : set_intersection2(A,empty_set) = empty_set ). % 0.53/0.83 % 0.53/0.83 fof(t2_subset,axiom, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( element(A,B) % 0.53/0.83 => ( empty(B) % 0.53/0.83 | in(A,B) ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t2_tarski,axiom, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( ! [C] : % 0.53/0.83 ( in(C,A) % 0.53/0.83 <=> in(C,B) ) % 0.53/0.83 => A = B ) ). % 0.53/0.83 % 0.53/0.83 fof(t2_xboole_1,lemma, % 0.53/0.83 ! [A] : subset(empty_set,A) ). % 0.53/0.83 % 0.53/0.83 fof(t33_xboole_1,lemma, % 0.53/0.83 ! [A,B,C] : % 0.53/0.83 ( subset(A,B) % 0.53/0.83 => subset(set_difference(A,C),set_difference(B,C)) ) ). % 0.53/0.83 % 0.53/0.83 fof(t33_zfmisc_1,lemma, % 0.53/0.83 ! [A,B,C,D] : % 0.53/0.83 ( ordered_pair(A,B) = ordered_pair(C,D) % 0.53/0.83 => ( A = C % 0.53/0.83 & B = D ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t36_xboole_1,lemma, % 0.53/0.83 ! [A,B] : subset(set_difference(A,B),A) ). % 0.53/0.83 % 0.53/0.83 fof(t37_xboole_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( set_difference(A,B) = empty_set % 0.53/0.83 <=> subset(A,B) ) ). % 0.53/0.83 % 0.53/0.83 fof(t37_zfmisc_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( subset(singleton(A),B) % 0.53/0.83 <=> in(A,B) ) ). % 0.53/0.83 % 0.53/0.83 fof(t38_zfmisc_1,lemma, % 0.53/0.83 ! [A,B,C] : % 0.53/0.83 ( subset(unordered_pair(A,B),C) % 0.53/0.83 <=> ( in(A,C) % 0.53/0.83 & in(B,C) ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t39_xboole_1,lemma, % 0.53/0.83 ! [A,B] : set_union2(A,set_difference(B,A)) = set_union2(A,B) ). % 0.53/0.83 % 0.53/0.83 fof(t39_zfmisc_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( subset(A,singleton(B)) % 0.53/0.83 <=> ( A = empty_set % 0.53/0.83 | A = singleton(B) ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t3_boole,axiom, % 0.53/0.83 ! [A] : set_difference(A,empty_set) = A ). % 0.53/0.83 % 0.53/0.83 fof(t3_subset,axiom, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( element(A,powerset(B)) % 0.53/0.83 <=> subset(A,B) ) ). % 0.53/0.83 % 0.53/0.83 fof(t3_xboole_0,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( ~ ( ~ disjoint(A,B) % 0.53/0.83 & ! [C] : % 0.53/0.83 ~ ( in(C,A) % 0.53/0.83 & in(C,B) ) ) % 0.53/0.83 & ~ ( ? [C] : % 0.53/0.83 ( in(C,A) % 0.53/0.83 & in(C,B) ) % 0.53/0.83 & disjoint(A,B) ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t3_xboole_1,lemma, % 0.53/0.83 ! [A] : % 0.53/0.83 ( subset(A,empty_set) % 0.53/0.83 => A = empty_set ) ). % 0.53/0.83 % 0.53/0.83 fof(t40_xboole_1,lemma, % 0.53/0.83 ! [A,B] : set_difference(set_union2(A,B),B) = set_difference(A,B) ). % 0.53/0.83 % 0.53/0.83 fof(t43_subset_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( element(B,powerset(A)) % 0.53/0.83 => ! [C] : % 0.53/0.83 ( element(C,powerset(A)) % 0.53/0.83 => ( disjoint(B,C) % 0.53/0.83 <=> subset(B,subset_complement(A,C)) ) ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t45_xboole_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( subset(A,B) % 0.53/0.83 => B = set_union2(A,set_difference(B,A)) ) ). % 0.53/0.83 % 0.53/0.83 fof(t46_setfam_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( element(B,powerset(powerset(A))) % 0.53/0.83 => ~ ( B != empty_set % 0.53/0.83 & complements_of_subsets(A,B) = empty_set ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t46_zfmisc_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( in(A,B) % 0.53/0.83 => set_union2(singleton(A),B) = B ) ). % 0.53/0.83 % 0.53/0.83 fof(t47_setfam_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( element(B,powerset(powerset(A))) % 0.53/0.83 => ( B != empty_set % 0.53/0.83 => subset_difference(A,cast_to_subset(A),union_of_subsets(A,B)) = meet_of_subsets(A,complements_of_subsets(A,B)) ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t48_setfam_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( element(B,powerset(powerset(A))) % 0.53/0.83 => ( B != empty_set % 0.53/0.83 => union_of_subsets(A,complements_of_subsets(A,B)) = subset_difference(A,cast_to_subset(A),meet_of_subsets(A,B)) ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t48_xboole_1,lemma, % 0.53/0.83 ! [A,B] : set_difference(A,set_difference(A,B)) = set_intersection2(A,B) ). % 0.53/0.83 % 0.53/0.83 fof(t4_boole,axiom, % 0.53/0.83 ! [A] : set_difference(empty_set,A) = empty_set ). % 0.53/0.83 % 0.53/0.83 fof(t4_subset,axiom, % 0.53/0.83 ! [A,B,C] : % 0.53/0.83 ( ( in(A,B) % 0.53/0.83 & element(B,powerset(C)) ) % 0.53/0.83 => element(A,C) ) ). % 0.53/0.83 % 0.53/0.83 fof(t4_xboole_0,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( ~ ( ~ disjoint(A,B) % 0.53/0.83 & ! [C] : ~ in(C,set_intersection2(A,B)) ) % 0.53/0.83 & ~ ( ? [C] : in(C,set_intersection2(A,B)) % 0.53/0.83 & disjoint(A,B) ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t50_subset_1,lemma, % 0.53/0.83 ! [A] : % 0.53/0.83 ( A != empty_set % 0.53/0.83 => ! [B] : % 0.53/0.83 ( element(B,powerset(A)) % 0.53/0.83 => ! [C] : % 0.53/0.83 ( element(C,A) % 0.53/0.83 => ( ~ in(C,B) % 0.53/0.83 => in(C,subset_complement(A,B)) ) ) ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t54_subset_1,lemma, % 0.53/0.83 ! [A,B,C] : % 0.53/0.83 ( element(C,powerset(A)) % 0.53/0.83 => ~ ( in(B,subset_complement(A,C)) % 0.53/0.83 & in(B,C) ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t5_subset,axiom, % 0.53/0.83 ! [A,B,C] : % 0.53/0.83 ~ ( in(A,B) % 0.53/0.83 & element(B,powerset(C)) % 0.53/0.83 & empty(C) ) ). % 0.53/0.83 % 0.53/0.83 fof(t60_xboole_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ~ ( subset(A,B) % 0.53/0.83 & proper_subset(B,A) ) ). % 0.53/0.83 % 0.53/0.83 fof(t63_xboole_1,lemma, % 0.53/0.83 ! [A,B,C] : % 0.53/0.83 ( ( subset(A,B) % 0.53/0.83 & disjoint(B,C) ) % 0.53/0.83 => disjoint(A,C) ) ). % 0.53/0.83 % 0.53/0.83 fof(t65_zfmisc_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( set_difference(A,singleton(B)) = A % 0.53/0.83 <=> ~ in(B,A) ) ). % 0.53/0.83 % 0.53/0.83 fof(t69_enumset1,lemma, % 0.53/0.83 ! [A] : unordered_pair(A,A) = singleton(A) ). % 0.53/0.83 % 0.53/0.83 fof(t6_boole,axiom, % 0.53/0.83 ! [A] : % 0.53/0.83 ( empty(A) % 0.53/0.83 => A = empty_set ) ). % 0.53/0.83 % 0.53/0.83 fof(t6_zfmisc_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( subset(singleton(A),singleton(B)) % 0.53/0.83 => A = B ) ). % 0.53/0.83 % 0.53/0.83 fof(t7_boole,axiom, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ~ ( in(A,B) % 0.53/0.83 & empty(B) ) ). % 0.53/0.83 % 0.53/0.83 fof(t7_xboole_1,lemma, % 0.53/0.83 ! [A,B] : subset(A,set_union2(A,B)) ). % 0.53/0.83 % 0.53/0.83 fof(t83_xboole_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( disjoint(A,B) % 0.53/0.83 <=> set_difference(A,B) = A ) ). % 0.53/0.83 % 0.53/0.83 fof(t8_boole,axiom, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ~ ( empty(A) % 0.53/0.83 & A != B % 0.53/0.83 & empty(B) ) ). % 0.53/0.83 % 0.53/0.83 fof(t8_xboole_1,lemma, % 0.53/0.83 ! [A,B,C] : % 0.53/0.83 ( ( subset(A,B) % 0.53/0.83 & subset(C,B) ) % 0.53/0.83 => subset(set_union2(A,C),B) ) ). % 0.53/0.83 % 0.53/0.83 fof(t8_zfmisc_1,lemma, % 0.53/0.83 ! [A,B,C] : % 0.53/0.83 ( singleton(A) = unordered_pair(B,C) % 0.53/0.83 => A = B ) ). % 0.53/0.83 % 0.53/0.83 fof(t92_zfmisc_1,lemma, % 0.53/0.83 ! [A,B] : % 0.53/0.83 ( in(A,B) % 0.53/0.83 => subset(A,union(B)) ) ). % 0.53/0.83 % 0.53/0.83 fof(t99_zfmisc_1,lemma, % 0.53/0.83 ! [A] : union(powerset(A)) = A ). % 0.53/0.83 % 0.53/0.83 fof(t9_tarski,axiom, % 0.53/0.83 ! [A] : % 0.53/0.83 ? [B] : % 0.53/0.83 ( in(A,B) % 0.53/0.83 & ! [C,D] : % 0.53/0.83 ( ( in(C,B) % 0.53/0.83 & subset(D,C) ) % 0.53/0.83 => in(D,B) ) % 0.53/0.83 & ! [C] : % 0.53/0.83 ~ ( in(C,B) % 0.53/0.83 & ! [D] : % 0.53/0.83 ~ ( in(D,B) % 0.53/0.83 & ! [E] : % 0.53/0.83 ( subset(E,C) % 0.53/0.83 => in(E,D) ) ) ) % 0.53/0.83 & ! [C] : % 0.53/0.83 ~ ( subset(C,B) % 0.53/0.83 & ~ are_equipotent(C,B) % 0.53/0.83 & ~ in(C,B) ) ) ). % 0.53/0.83 % 0.53/0.83 fof(t9_zfmisc_1,lemma, % 0.53/0.83 ! [A,B,C] : % 0.53/0.83 ( singleton(A) = unordered_pair(B,C) % 0.53/0.83 => B = C ) ). % 0.53/0.83 % 0.53/0.83 %------------------------------------------------------------------------------ % 0.53/0.83 %------------------------------------------- % 0.53/0.83 % Proof found % 0.53/0.83 % SZS status Theorem for theBenchmark % 0.53/0.83 % SZS output start Proof % 0.53/0.83 %ClaNum:350(EqnAxiom:123) % 0.53/0.83 %VarNum:1364(SingletonVarNum:490) % 0.53/0.83 %MaxLitNum:6 % 0.53/0.83 %MaxfuncDepth:3 % 0.53/0.83 %SharedTerms:24 % 0.53/0.83 %goalClause: 128 153 209 % 0.53/0.83 %singleGoalClaCount:2 % 0.53/0.83 [124]P1(a1) % 0.53/0.83 [125]P1(a4) % 0.53/0.83 [126]P1(a25) % 0.53/0.83 [127]P5(a4) % 0.53/0.83 [128]P5(a28) % 0.53/0.83 [154]~P1(a31) % 0.53/0.83 [135]E(f56(a1,a1),f34(a1)) % 0.53/0.83 [153]P6(f56(f56(a32,a33),f56(a32,a32)),a28) % 0.53/0.83 [132]P8(a1,x1321) % 0.53/0.83 [136]P8(x1361,x1361) % 0.53/0.83 [157]~P7(x1571,x1571) % 0.53/0.83 [129]P1(f29(x1291)) % 0.53/0.83 [131]E(f49(a1,x1311),a1) % 0.53/0.83 [133]E(f52(x1331,a1),x1331) % 0.53/0.83 [134]E(f49(x1341,a1),x1341) % 0.53/0.83 [137]E(f52(x1371,x1371),x1371) % 0.53/0.83 [138]P6(x1381,f30(x1381)) % 0.53/0.83 [139]P6(x1391,f35(x1391)) % 0.53/0.83 [140]P2(x1401,f34(x1401)) % 0.53/0.83 [141]P2(f5(x1411),x1411) % 0.53/0.83 [142]P2(f29(x1421),f34(x1421)) % 0.53/0.83 [155]~P1(f34(x1551)) % 0.53/0.83 [156]~E(f56(x1561,x1561),a1) % 0.53/0.83 [130]E(f48(f34(x1301)),x1301) % 0.53/0.83 [145]E(f49(x1451,f49(x1451,a1)),a1) % 0.53/0.83 [148]E(f49(x1481,f49(x1481,x1481)),x1481) % 0.53/0.83 [143]E(f56(x1431,x1432),f56(x1432,x1431)) % 0.53/0.83 [144]E(f52(x1441,x1442),f52(x1442,x1441)) % 0.53/0.83 [146]P8(x1461,f52(x1461,x1462)) % 0.53/0.83 [147]P8(f49(x1471,x1472),x1471) % 0.53/0.83 [158]~P1(f56(x1581,x1582)) % 0.53/0.83 [149]E(f52(x1491,f49(x1492,x1491)),f52(x1491,x1492)) % 0.53/0.83 [150]E(f49(f52(x1501,x1502),x1502),f49(x1501,x1502)) % 0.53/0.83 [151]E(f49(x1511,f49(x1511,x1512)),f49(x1512,f49(x1512,x1511))) % 0.53/0.83 [209]~P6(a32,f50(a28))+~P6(a33,f51(a28)) % 0.53/0.83 [161]~P1(x1611)+E(x1611,a1) % 0.53/0.83 [168]~P8(x1681,a1)+E(x1681,a1) % 0.53/0.83 [167]P1(x1671)+~P1(f26(x1671)) % 0.53/0.83 [169]P6(f40(x1691),x1691)+E(x1691,a1) % 0.53/0.83 [174]P1(x1741)+P2(f26(x1741),f34(x1741)) % 0.53/0.83 [166]~E(x1661,x1662)+P8(x1661,x1662) % 0.53/0.83 [170]~P6(x1702,x1701)+~E(x1701,a1) % 0.53/0.83 [171]~P7(x1711,x1712)+~E(x1711,x1712) % 0.53/0.83 [173]~P1(x1731)+~P6(x1732,x1731) % 0.53/0.83 [180]~P7(x1801,x1802)+P8(x1801,x1802) % 0.53/0.83 [181]~P6(x1811,x1812)+P2(x1811,x1812) % 0.53/0.83 [182]~P3(x1822,x1821)+P3(x1821,x1822) % 0.53/0.83 [198]~P6(x1982,x1981)+~P6(x1981,x1982) % 0.53/0.83 [199]~P7(x1992,x1991)+~P7(x1991,x1992) % 0.53/0.83 [200]~P8(x2002,x2001)+~P7(x2001,x2002) % 0.53/0.83 [177]~P8(x1771,x1772)+E(f49(x1771,x1772),a1) % 0.53/0.83 [179]P8(x1791,x1792)+~E(f49(x1791,x1792),a1) % 0.53/0.83 [183]~P8(x1831,x1832)+E(f52(x1831,x1832),x1832) % 0.53/0.83 [184]~P3(x1841,x1842)+E(f49(x1841,x1842),x1841) % 0.53/0.83 [185]P3(x1851,x1852)+~E(f49(x1851,x1852),x1851) % 0.53/0.83 [194]~E(x1941,a1)+P8(x1941,f56(x1942,x1942)) % 0.53/0.83 [196]~P6(x1961,x1962)+P8(x1961,f48(x1962)) % 0.53/0.83 [197]~P8(x1971,x1972)+P2(x1971,f34(x1972)) % 0.53/0.83 [205]P8(x2051,x2052)+~P2(x2051,f34(x2052)) % 0.53/0.83 [211]P1(x2111)+~P1(f52(x2112,x2111)) % 0.53/0.83 [212]P1(x2121)+~P1(f52(x2121,x2122)) % 0.53/0.83 [213]P6(x2131,x2132)+P3(f56(x2131,x2131),x2132) % 0.53/0.83 [214]P8(x2141,x2142)+P6(f6(x2141,x2142),x2141) % 0.53/0.83 [215]P3(x2151,x2152)+P6(f36(x2151,x2152),x2152) % 0.53/0.83 [216]P3(x2161,x2162)+P6(f36(x2161,x2162),x2161) % 0.53/0.83 [218]P6(f34(x2181),f30(x2182))+~P6(x2181,f30(x2182)) % 0.53/0.83 [222]~P2(x2222,f34(x2221))+E(f54(x2221,x2222),f49(x2221,x2222)) % 0.53/0.83 [223]P6(f24(x2231,x2232),x2231)+P2(x2231,f34(x2232)) % 0.53/0.83 [230]~P6(x2301,x2302)+P8(f56(x2301,x2301),x2302) % 0.53/0.83 [259]P8(x2591,x2592)+~P6(f6(x2591,x2592),x2592) % 0.53/0.83 [260]~P6(x2602,f35(x2601))+P6(f42(x2601,x2602),f35(x2601)) % 0.53/0.83 [261]~P2(x2612,f34(x2611))+P2(f54(x2611,x2612),f34(x2611)) % 0.53/0.83 [265]~P6(f24(x2651,x2652),x2652)+P2(x2651,f34(x2652)) % 0.53/0.83 [270]~P6(x2701,x2702)+~P3(f56(x2701,x2701),x2702) % 0.53/0.83 [282]E(x2821,x2822)+~P8(f56(x2821,x2821),f56(x2822,x2822)) % 0.53/0.83 [217]P6(x2172,x2171)+E(f49(x2171,f56(x2172,x2172)),x2171) % 0.53/0.83 [228]~P3(x2281,x2282)+E(f49(x2281,f49(x2281,x2282)),a1) % 0.53/0.83 [231]~P8(x2311,x2312)+E(f52(x2311,f49(x2312,x2311)),x2312) % 0.53/0.83 [232]~P8(x2321,x2322)+E(f49(x2321,f49(x2321,x2322)),x2321) % 0.53/0.83 [234]~P6(x2341,x2342)+E(f52(f56(x2341,x2341),x2342),x2342) % 0.53/0.83 [242]E(f57(x2421,x2422),f48(x2422))+~P2(x2422,f34(f34(x2421))) % 0.53/0.83 [243]E(f43(x2431,x2432),f53(x2432))+~P2(x2432,f34(f34(x2431))) % 0.53/0.83 [246]~P2(x2462,f34(x2461))+E(f54(x2461,f54(x2461,x2462)),x2462) % 0.53/0.83 [254]P3(x2541,x2542)+~E(f49(x2541,f49(x2541,x2542)),a1) % 0.53/0.83 [271]~P6(x2712,x2711)+~E(f49(x2711,f56(x2712,x2712)),x2711) % 0.53/0.83 [275]~P2(x2752,f34(f34(x2751)))+E(f2(x2751,f2(x2751,x2752)),x2752) % 0.53/0.83 [277]P2(f57(x2771,x2772),f34(x2771))+~P2(x2772,f34(f34(x2771))) % 0.53/0.83 [278]P2(f43(x2781,x2782),f34(x2781))+~P2(x2782,f34(f34(x2781))) % 0.53/0.83 [283]~P2(x2832,f34(f34(x2831)))+P2(f2(x2831,x2832),f34(f34(x2831))) % 0.53/0.83 [295]P3(x2951,x2952)+P6(f39(x2951,x2952),f49(x2951,f49(x2951,x2952))) % 0.53/0.83 [203]E(x2031,x2032)+~E(f56(x2033,x2033),f56(x2031,x2032)) % 0.53/0.83 [204]E(x2041,x2042)+~E(f56(x2041,x2041),f56(x2042,x2043)) % 0.53/0.83 [255]P6(x2551,x2552)+~P8(f56(x2553,x2551),x2552) % 0.53/0.83 [256]P6(x2561,x2562)+~P8(f56(x2561,x2563),x2562) % 0.53/0.83 [272]~P8(x2721,x2723)+P8(f3(x2721,x2722),f3(x2723,x2722)) % 0.53/0.83 [273]~P8(x2732,x2733)+P8(f3(x2731,x2732),f3(x2731,x2733)) % 0.53/0.83 [274]~P8(x2741,x2743)+P8(f49(x2741,x2742),f49(x2743,x2742)) % 0.53/0.83 [303]~P3(x3031,x3032)+~P6(x3033,f49(x3031,f49(x3031,x3032))) % 0.53/0.83 [309]~P8(x3091,x3093)+P8(f49(x3091,f49(x3091,x3092)),f49(x3093,f49(x3093,x3092))) % 0.53/0.83 [310]E(x3101,x3102)+~E(f56(f56(x3103,x3101),f56(x3103,x3103)),f56(f56(x3104,x3102),f56(x3104,x3104))) % 0.53/0.83 [311]E(x3111,x3112)+~E(f56(f56(x3111,x3113),f56(x3111,x3111)),f56(f56(x3112,x3114),f56(x3112,x3112))) % 0.53/0.83 [325]P6(x3251,x3252)+~P6(f56(f56(x3253,x3251),f56(x3253,x3253)),f3(x3254,x3252)) % 0.53/0.83 [327]P6(x3271,x3272)+~P6(f56(f56(x3271,x3273),f56(x3271,x3271)),f3(x3272,x3274)) % 0.53/0.83 [164]~P1(x1642)+~P1(x1641)+E(x1641,x1642) % 0.53/0.83 [172]~P1(x1722)+~P1(x1721)+P2(x1721,x1722) % 0.53/0.83 [175]~P2(x1751,x1752)+P1(x1751)+~P1(x1752) % 0.53/0.83 [186]P7(x1861,x1862)+~P8(x1861,x1862)+E(x1861,x1862) % 0.53/0.83 [188]~P2(x1882,x1881)+P1(x1881)+P6(x1882,x1881) % 0.53/0.83 [206]~P8(x2062,x2061)+~P8(x2061,x2062)+E(x2061,x2062) % 0.53/0.83 [162]~E(x1622,a1)+~E(x1621,a1)+E(x1621,f53(x1622)) % 0.53/0.83 [163]~E(x1631,f53(x1632))+E(x1631,a1)+~E(x1632,a1) % 0.53/0.83 [245]E(f41(x2452,x2451),x2452)+P6(f41(x2452,x2451),x2451)+E(x2451,f56(x2452,x2452)) % 0.53/0.83 [247]P6(x2471,f30(x2472))+P4(x2471,f30(x2472))+~P8(x2471,f30(x2472)) % 0.53/0.83 [248]P6(x2481,f35(x2482))+P4(x2481,f35(x2482))+~P8(x2481,f35(x2482)) % 0.53/0.83 [263]E(x2631,f56(x2632,x2632))+~P8(x2631,f56(x2632,x2632))+E(x2631,a1) % 0.53/0.83 [264]E(x2641,x2642)+P6(f37(x2641,x2642),x2642)+P6(f37(x2641,x2642),x2641) % 0.53/0.83 [268]P6(f44(x2682,x2681),x2681)+P8(f44(x2682,x2681),x2682)+E(x2681,f34(x2682)) % 0.53/0.83 [269]P6(f11(x2692,x2691),x2691)+P6(f18(x2692,x2691),x2692)+E(x2691,f48(x2692)) % 0.53/0.83 [281]~E(f41(x2812,x2811),x2812)+~P6(f41(x2812,x2811),x2811)+E(x2811,f56(x2812,x2812)) % 0.53/0.83 [288]P6(f11(x2882,x2881),x2881)+P6(f11(x2882,x2881),f18(x2882,x2881))+E(x2881,f48(x2882)) % 0.53/0.83 [292]E(x2921,x2922)+~P6(f37(x2921,x2922),x2922)+~P6(f37(x2921,x2922),x2921) % 0.53/0.83 [294]~P6(f44(x2942,x2941),x2941)+~P8(f44(x2942,x2941),x2942)+E(x2941,f34(x2942)) % 0.53/0.83 [253]E(x2531,a1)+~P2(x2531,f34(f34(x2532)))+~E(f2(x2532,x2531),a1) % 0.53/0.83 [304]E(x3041,a1)+~P2(x3041,f34(f34(x3042)))+E(f55(x3042,x3042,f43(x3042,x3041)),f57(x3042,f2(x3042,x3041))) % 0.53/0.83 [305]E(x3051,a1)+~P2(x3051,f34(f34(x3052)))+E(f55(x3052,x3052,f57(x3052,x3051)),f43(x3052,f2(x3052,x3051))) % 0.53/0.83 [219]~P8(x2193,x2192)+P6(x2191,x2192)+~P6(x2191,x2193) % 0.53/0.83 [220]~P8(x2201,x2203)+P8(x2201,x2202)+~P8(x2203,x2202) % 0.53/0.83 [221]~P3(x2213,x2212)+P3(x2211,x2212)+~P8(x2211,x2213) % 0.53/0.83 [237]~P3(x2373,x2372)+~P6(x2371,x2372)+~P6(x2371,x2373) % 0.53/0.83 [201]~P8(x2011,x2013)+P6(x2011,x2012)+~E(x2012,f34(x2013)) % 0.53/0.83 [202]~P6(x2021,x2023)+P8(x2021,x2022)+~E(x2023,f34(x2022)) % 0.53/0.83 [208]~P6(x2081,x2083)+E(x2081,x2082)+~E(x2083,f56(x2082,x2082)) % 0.53/0.83 [227]~P1(x2271)+~P6(x2272,x2273)+~P2(x2273,f34(x2271)) % 0.53/0.83 [240]P6(x2401,x2402)+~P6(x2401,x2403)+~P2(x2403,f34(x2402)) % 0.53/0.83 [241]P2(x2411,x2412)+~P6(x2411,x2413)+~P2(x2413,f34(x2412)) % 0.53/0.83 [249]~P8(x2491,x2493)+P6(x2491,f30(x2492))+~P6(x2493,f30(x2492)) % 0.53/0.83 [250]~P8(x2501,x2503)+P6(x2501,f35(x2502))+~P6(x2503,f35(x2502)) % 0.53/0.83 [266]~P6(x2662,x2663)+~P6(x2661,x2663)+P8(f56(x2661,x2662),x2663) % 0.53/0.83 [267]~P8(x2672,x2673)+~P8(x2671,x2673)+P8(f52(x2671,x2672),x2673) % 0.53/0.83 [276]~P8(x2761,x2763)+~P6(x2763,f35(x2762))+P6(x2761,f42(x2762,x2763)) % 0.53/0.83 [289]~P6(x2891,x2892)+~P6(x2891,f54(x2893,x2892))+~P2(x2892,f34(x2893)) % 0.53/0.83 [296]~P2(x2963,f34(x2961))+~P2(x2962,f34(x2961))+E(f55(x2961,x2962,x2963),f49(x2962,x2963)) % 0.53/0.83 [300]~P6(x3001,x3003)+~E(x3003,f48(x3002))+P6(x3001,f13(x3002,x3003,x3001)) % 0.53/0.83 [301]~P6(x3013,x3012)+~E(x3012,f48(x3011))+P6(f13(x3011,x3012,x3013),x3011) % 0.53/0.83 [308]~P2(x3083,f34(x3081))+~P2(x3082,f34(x3081))+P2(f55(x3081,x3082,x3083),f34(x3081)) % 0.53/0.83 [321]P6(f7(x3212,x3213,x3211),x3211)+P6(f9(x3212,x3213,x3211),x3212)+E(x3211,f3(x3212,x3213)) % 0.53/0.83 [322]P6(f7(x3222,x3223,x3221),x3221)+P6(f10(x3222,x3223,x3221),x3223)+E(x3221,f3(x3222,x3223)) % 0.53/0.83 [323]P6(f20(x3232,x3233,x3231),x3231)+P6(f20(x3232,x3233,x3231),x3232)+E(x3231,f49(x3232,x3233)) % 0.53/0.83 [330]~E(f45(x3302,x3303,x3301),x3303)+~P6(f45(x3302,x3303,x3301),x3301)+E(x3301,f56(x3302,x3303)) % 0.53/0.83 [331]~E(f45(x3312,x3313,x3311),x3312)+~P6(f45(x3312,x3313,x3311),x3311)+E(x3311,f56(x3312,x3313)) % 0.53/0.83 [332]P6(f20(x3322,x3323,x3321),x3321)+~P6(f20(x3322,x3323,x3321),x3323)+E(x3321,f49(x3322,x3323)) % 0.53/0.83 [334]~P6(f46(x3342,x3343,x3341),x3341)+~P6(f46(x3342,x3343,x3341),x3343)+E(x3341,f52(x3342,x3343)) % 0.53/0.83 [335]~P6(f46(x3352,x3353,x3351),x3351)+~P6(f46(x3352,x3353,x3351),x3352)+E(x3351,f52(x3352,x3353)) % 0.53/0.83 [293]~P8(x2932,x2933)+P6(x2931,x2932)+P8(x2932,f49(x2933,f56(x2931,x2931))) % 0.53/0.83 [297]~P8(x2971,x2973)+~P8(x2971,x2972)+P8(x2971,f49(x2972,f49(x2972,x2973))) % 0.53/0.83 [328]P6(f14(x3282,x3283,x3281),x3281)+P6(f14(x3282,x3283,x3281),x3283)+E(x3281,f49(x3282,f49(x3282,x3283))) % 0.53/0.83 [329]P6(f14(x3292,x3293,x3291),x3291)+P6(f14(x3292,x3293,x3291),x3292)+E(x3291,f49(x3292,f49(x3292,x3293))) % 0.53/0.83 [348]P6(f7(x3482,x3483,x3481),x3481)+E(x3481,f3(x3482,x3483))+E(f56(f56(f9(x3482,x3483,x3481),f10(x3482,x3483,x3481)),f56(f9(x3482,x3483,x3481),f9(x3482,x3483,x3481))),f7(x3482,x3483,x3481)) % 0.53/0.83 [190]P6(x1901,x1902)+~E(x1901,x1903)+~E(x1902,f56(x1904,x1903)) % 0.53/0.83 [191]P6(x1911,x1912)+~E(x1911,x1913)+~E(x1912,f56(x1913,x1914)) % 0.53/0.83 [207]E(x2071,x2072)+E(x2071,x2073)+~E(f56(x2071,x2074),f56(x2073,x2072)) % 0.53/0.83 [224]~P6(x2241,x2244)+P6(x2241,x2242)+~E(x2242,f52(x2243,x2244)) % 0.53/0.83 [225]~P6(x2251,x2253)+P6(x2251,x2252)+~E(x2252,f52(x2253,x2254)) % 0.53/0.83 [226]~P6(x2261,x2263)+P6(x2261,x2262)+~E(x2263,f49(x2262,x2264)) % 0.53/0.83 [239]~P6(x2394,x2393)+~P6(x2394,x2391)+~E(x2391,f49(x2392,x2393)) % 0.53/0.83 [287]~P8(x2872,x2874)+~P8(x2871,x2873)+P8(f3(x2871,x2872),f3(x2873,x2874)) % 0.53/0.83 [340]~P6(x3404,x3403)+~E(x3403,f3(x3401,x3402))+P6(f47(x3401,x3402,x3403,x3404),x3401) % 0.53/0.83 [341]~P6(x3414,x3413)+~E(x3413,f3(x3411,x3412))+P6(f8(x3411,x3412,x3413,x3414),x3412) % 0.53/0.83 [279]~P6(x2791,x2793)+P6(x2791,x2792)+~E(x2793,f49(x2794,f49(x2794,x2792))) % 0.53/0.83 [314]~P6(x3142,x3144)+~P6(x3141,x3143)+P6(f56(f56(x3141,x3142),f56(x3141,x3141)),f3(x3143,x3144)) % 0.53/0.83 [350]~P6(x3504,x3503)+~E(x3503,f3(x3501,x3502))+E(f56(f56(f47(x3501,x3502,x3503,x3504),f8(x3501,x3502,x3503,x3504)),f56(f47(x3501,x3502,x3503,x3504),f47(x3501,x3502,x3503,x3504))),x3504) % 0.53/0.83 [285]P6(f38(x2851,x2852),x2851)+~P6(f27(x2851,x2852),x2852)+E(x2851,a1)+E(x2852,f53(x2851)) % 0.53/0.83 [306]~P6(f27(x3061,x3062),x3062)+~P6(f27(x3061,x3062),f38(x3061,x3062))+E(x3061,a1)+E(x3062,f53(x3061)) % 0.53/0.83 [343]~P5(x3432)+P6(f16(x3432,x3431),x3431)+E(x3431,f50(x3432))+P6(f56(f56(f16(x3432,x3431),f17(x3432,x3431)),f56(f16(x3432,x3431),f16(x3432,x3431))),x3432) % 0.53/0.83 [344]~P5(x3442)+P6(f21(x3442,x3441),x3441)+E(x3441,f51(x3442))+P6(f56(f56(f23(x3442,x3441),f21(x3442,x3441)),f56(f23(x3442,x3441),f23(x3442,x3441))),x3442) % 0.53/0.84 [291]~P3(x2911,x2913)+~P2(x2913,f34(x2912))+~P2(x2911,f34(x2912))+P8(x2911,f54(x2912,x2913)) % 0.53/0.84 [298]P3(x2981,x2982)+~P8(x2981,f54(x2983,x2982))+~P2(x2982,f34(x2983))+~P2(x2981,f34(x2983)) % 0.53/0.84 [299]P6(x2992,x2993)+P6(f12(x2991,x2993,x2992),x2991)+~E(x2993,f53(x2991))+E(x2991,a1) % 0.53/0.84 [302]~P6(x3023,x3022)+~P6(f11(x3022,x3021),x3023)+~P6(f11(x3022,x3021),x3021)+E(x3021,f48(x3022)) % 0.53/0.84 [312]P6(x3122,x3123)+~E(x3123,f53(x3121))+~P6(x3122,f12(x3121,x3123,x3122))+E(x3121,a1) % 0.53/0.84 [318]E(f45(x3182,x3183,x3181),x3183)+E(f45(x3182,x3183,x3181),x3182)+P6(f45(x3182,x3183,x3181),x3181)+E(x3181,f56(x3182,x3183)) % 0.53/0.84 [333]P6(f46(x3332,x3333,x3331),x3331)+P6(f46(x3332,x3333,x3331),x3333)+P6(f46(x3332,x3333,x3331),x3332)+E(x3331,f52(x3332,x3333)) % 0.53/0.84 [339]P6(f20(x3392,x3393,x3391),x3393)+~P6(f20(x3392,x3393,x3391),x3391)+~P6(f20(x3392,x3393,x3391),x3392)+E(x3391,f49(x3392,x3393)) % 0.53/0.84 [317]P2(f19(x3172,x3173,x3171),f34(x3172))+E(x3171,f2(x3172,x3173))+~P2(x3171,f34(f34(x3172)))+~P2(x3173,f34(f34(x3172))) % 0.53/0.84 [337]~P5(x3372)+~P6(f21(x3372,x3371),x3371)+E(x3371,f51(x3372))+~P6(f56(f56(x3373,f21(x3372,x3371)),f56(x3373,x3373)),x3372) % 0.53/0.84 [342]~P5(x3422)+~P6(x3421,x3423)+~E(x3423,f50(x3422))+P6(f56(f56(x3421,f15(x3422,x3423,x3421)),f56(x3421,x3421)),x3422) % 0.53/0.84 [345]~P6(f14(x3452,x3453,x3451),x3451)+~P6(f14(x3452,x3453,x3451),x3453)+~P6(f14(x3452,x3453,x3451),x3452)+E(x3451,f49(x3452,f49(x3452,x3453))) % 0.53/0.84 [347]~P5(x3472)+~P6(f16(x3472,x3471),x3471)+E(x3471,f50(x3472))+~P6(f56(f56(f16(x3472,x3471),x3473),f56(f16(x3472,x3471),f16(x3472,x3471))),x3472) % 0.53/0.84 [349]~P5(x3491)+~P6(x3493,x3492)+~E(x3492,f51(x3491))+P6(f56(f56(f22(x3491,x3492,x3493),x3493),f56(f22(x3491,x3492,x3493),f22(x3491,x3492,x3493))),x3491) % 0.53/0.84 [210]~P6(x2101,x2104)+E(x2101,x2102)+E(x2101,x2103)+~E(x2104,f56(x2103,x2102)) % 0.53/0.84 [238]~P6(x2381,x2384)+P6(x2381,x2382)+~P6(x2384,x2383)+~E(x2382,f48(x2383)) % 0.53/0.84 [251]~P6(x2511,x2514)+P6(x2511,x2512)+P6(x2511,x2513)+~E(x2512,f49(x2514,x2513)) % 0.53/0.84 [252]~P6(x2521,x2524)+P6(x2521,x2522)+P6(x2521,x2523)+~E(x2524,f52(x2523,x2522)) % 0.53/0.84 [290]~P6(x2901,x2904)+~P6(x2901,x2903)+P6(x2901,x2902)+~E(x2902,f49(x2903,f49(x2903,x2904))) % 0.53/0.84 [319]~P5(x3193)+P6(x3191,x3192)+~E(x3192,f51(x3193))+~P6(f56(f56(x3194,x3191),f56(x3194,x3194)),x3193) % 0.53/0.84 [320]~P5(x3203)+P6(x3201,x3202)+~E(x3202,f50(x3203))+~P6(f56(f56(x3201,x3204),f56(x3201,x3201)),x3203) % 0.53/0.84 [284]~P6(x2843,x2841)+P6(f27(x2841,x2842),x2842)+E(x2841,a1)+E(x2842,f53(x2841))+P6(f27(x2841,x2842),x2843) % 0.53/0.84 [286]~P2(x2862,x2861)+P6(x2862,x2863)+P6(x2862,f54(x2861,x2863))+~P2(x2863,f34(x2861))+E(x2861,a1) % 0.53/0.84 [338]P6(f19(x3382,x3383,x3381),x3381)+E(x3381,f2(x3382,x3383))+P6(f54(x3382,f19(x3382,x3383,x3381)),x3383)+~P2(x3381,f34(f34(x3382)))+~P2(x3383,f34(f34(x3382))) % 0.53/0.84 [346]~P6(f19(x3462,x3463,x3461),x3461)+E(x3461,f2(x3462,x3463))+~P2(x3461,f34(f34(x3462)))+~P2(x3463,f34(f34(x3462)))+~P6(f54(x3462,f19(x3462,x3463,x3461)),x3463) % 0.53/0.84 [244]~P6(x2443,x2441)+~P6(x2442,x2444)+P6(x2442,x2443)+E(x2441,a1)+~E(x2444,f53(x2441)) % 0.53/0.84 [336]~P6(x3365,x3363)+~P6(x3364,x3362)+~P6(f7(x3362,x3363,x3361),x3361)+E(x3361,f3(x3362,x3363))+~E(f7(x3362,x3363,x3361),f56(f56(x3364,x3365),f56(x3364,x3364))) % 0.53/0.84 [307]~P6(x3076,x3074)+~P6(x3075,x3073)+P6(x3071,x3072)+~E(x3072,f3(x3073,x3074))+~E(x3071,f56(f56(x3075,x3076),f56(x3075,x3075))) % 0.53/0.84 [315]~P6(x3152,x3154)+~P2(x3152,f34(x3151))+P6(f54(x3151,x3152),x3153)+~E(x3154,f2(x3151,x3153))+~P2(x3153,f34(f34(x3151)))+~P2(x3154,f34(f34(x3151))) % 0.53/0.84 [316]P6(x3161,x3162)+~P2(x3161,f34(x3163))+~P6(f54(x3163,x3161),x3164)+~E(x3162,f2(x3163,x3164))+~P2(x3162,f34(f34(x3163)))+~P2(x3164,f34(f34(x3163))) % 0.53/0.84 %EqnAxiom % 0.53/0.84 [1]E(x11,x11) % 0.53/0.84 [2]E(x22,x21)+~E(x21,x22) % 0.53/0.84 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.53/0.84 [4]~E(x41,x42)+E(f29(x41),f29(x42)) % 0.53/0.84 [5]~E(x51,x52)+E(f34(x51),f34(x52)) % 0.53/0.84 [6]~E(x61,x62)+E(f48(x61),f48(x62)) % 0.53/0.84 [7]~E(x71,x72)+E(f49(x71,x73),f49(x72,x73)) % 0.53/0.84 [8]~E(x81,x82)+E(f49(x83,x81),f49(x83,x82)) % 0.53/0.84 [9]~E(x91,x92)+E(f52(x91,x93),f52(x92,x93)) % 0.53/0.84 [10]~E(x101,x102)+E(f52(x103,x101),f52(x103,x102)) % 0.53/0.84 [11]~E(x111,x112)+E(f56(x111,x113),f56(x112,x113)) % 0.53/0.84 [12]~E(x121,x122)+E(f56(x123,x121),f56(x123,x122)) % 0.53/0.84 [13]~E(x131,x132)+E(f54(x131,x133),f54(x132,x133)) % 0.53/0.84 [14]~E(x141,x142)+E(f54(x143,x141),f54(x143,x142)) % 0.53/0.84 [15]~E(x151,x152)+E(f50(x151),f50(x152)) % 0.53/0.84 [16]~E(x161,x162)+E(f2(x161,x163),f2(x162,x163)) % 0.53/0.84 [17]~E(x171,x172)+E(f2(x173,x171),f2(x173,x172)) % 0.53/0.84 [18]~E(x181,x182)+E(f30(x181),f30(x182)) % 0.53/0.84 [19]~E(x191,x192)+E(f35(x191),f35(x192)) % 0.53/0.84 [20]~E(x201,x202)+E(f43(x201,x203),f43(x202,x203)) % 0.53/0.84 [21]~E(x211,x212)+E(f43(x213,x211),f43(x213,x212)) % 0.53/0.84 [22]~E(x221,x222)+E(f5(x221),f5(x222)) % 0.53/0.84 [23]~E(x231,x232)+E(f3(x231,x233),f3(x232,x233)) % 0.53/0.84 [24]~E(x241,x242)+E(f3(x243,x241),f3(x243,x242)) % 0.53/0.84 [25]~E(x251,x252)+E(f47(x251,x253,x254,x255),f47(x252,x253,x254,x255)) % 0.53/0.84 [26]~E(x261,x262)+E(f47(x263,x261,x264,x265),f47(x263,x262,x264,x265)) % 0.53/0.84 [27]~E(x271,x272)+E(f47(x273,x274,x271,x275),f47(x273,x274,x272,x275)) % 0.53/0.84 [28]~E(x281,x282)+E(f47(x283,x284,x285,x281),f47(x283,x284,x285,x282)) % 0.53/0.84 [29]~E(x291,x292)+E(f16(x291,x293),f16(x292,x293)) % 0.53/0.84 [30]~E(x301,x302)+E(f16(x303,x301),f16(x303,x302)) % 0.53/0.84 [31]~E(x311,x312)+E(f53(x311),f53(x312)) % 0.53/0.84 [32]~E(x321,x322)+E(f17(x321,x323),f17(x322,x323)) % 0.53/0.84 [33]~E(x331,x332)+E(f17(x333,x331),f17(x333,x332)) % 0.53/0.84 [34]~E(x341,x342)+E(f27(x341,x343),f27(x342,x343)) % 0.53/0.84 [35]~E(x351,x352)+E(f27(x353,x351),f27(x353,x352)) % 0.53/0.84 [36]~E(x361,x362)+E(f21(x361,x363),f21(x362,x363)) % 0.53/0.84 [37]~E(x371,x372)+E(f21(x373,x371),f21(x373,x372)) % 0.53/0.84 [38]~E(x381,x382)+E(f41(x381,x383),f41(x382,x383)) % 0.53/0.84 [39]~E(x391,x392)+E(f41(x393,x391),f41(x393,x392)) % 0.53/0.84 [40]~E(x401,x402)+E(f57(x401,x403),f57(x402,x403)) % 0.53/0.84 [41]~E(x411,x412)+E(f57(x413,x411),f57(x413,x412)) % 0.53/0.84 [42]~E(x421,x422)+E(f51(x421),f51(x422)) % 0.53/0.84 [43]~E(x431,x432)+E(f7(x431,x433,x434),f7(x432,x433,x434)) % 0.53/0.84 [44]~E(x441,x442)+E(f7(x443,x441,x444),f7(x443,x442,x444)) % 0.53/0.84 [45]~E(x451,x452)+E(f7(x453,x454,x451),f7(x453,x454,x452)) % 0.53/0.84 [46]~E(x461,x462)+E(f11(x461,x463),f11(x462,x463)) % 0.53/0.84 [47]~E(x471,x472)+E(f11(x473,x471),f11(x473,x472)) % 0.53/0.84 [48]~E(x481,x482)+E(f19(x481,x483,x484),f19(x482,x483,x484)) % 0.53/0.84 [49]~E(x491,x492)+E(f19(x493,x491,x494),f19(x493,x492,x494)) % 0.53/0.84 [50]~E(x501,x502)+E(f19(x503,x504,x501),f19(x503,x504,x502)) % 0.53/0.84 [51]~E(x511,x512)+E(f14(x511,x513,x514),f14(x512,x513,x514)) % 0.53/0.84 [52]~E(x521,x522)+E(f14(x523,x521,x524),f14(x523,x522,x524)) % 0.53/0.84 [53]~E(x531,x532)+E(f14(x533,x534,x531),f14(x533,x534,x532)) % 0.53/0.84 [54]~E(x541,x542)+E(f12(x541,x543,x544),f12(x542,x543,x544)) % 0.53/0.84 [55]~E(x551,x552)+E(f12(x553,x551,x554),f12(x553,x552,x554)) % 0.53/0.84 [56]~E(x561,x562)+E(f12(x563,x564,x561),f12(x563,x564,x562)) % 0.53/0.84 [57]~E(x571,x572)+E(f20(x571,x573,x574),f20(x572,x573,x574)) % 0.53/0.84 [58]~E(x581,x582)+E(f20(x583,x581,x584),f20(x583,x582,x584)) % 0.53/0.84 [59]~E(x591,x592)+E(f20(x593,x594,x591),f20(x593,x594,x592)) % 0.53/0.84 [60]~E(x601,x602)+E(f44(x601,x603),f44(x602,x603)) % 0.53/0.84 [61]~E(x611,x612)+E(f44(x613,x611),f44(x613,x612)) % 0.53/0.84 [62]~E(x621,x622)+E(f23(x621,x623),f23(x622,x623)) % 0.53/0.84 [63]~E(x631,x632)+E(f23(x633,x631),f23(x633,x632)) % 0.53/0.84 [64]~E(x641,x642)+E(f37(x641,x643),f37(x642,x643)) % 0.53/0.84 [65]~E(x651,x652)+E(f37(x653,x651),f37(x653,x652)) % 0.53/0.84 [66]~E(x661,x662)+E(f46(x661,x663,x664),f46(x662,x663,x664)) % 0.53/0.84 [67]~E(x671,x672)+E(f46(x673,x671,x674),f46(x673,x672,x674)) % 0.53/0.84 [68]~E(x681,x682)+E(f46(x683,x684,x681),f46(x683,x684,x682)) % 0.53/0.84 [69]~E(x691,x692)+E(f39(x691,x693),f39(x692,x693)) % 0.53/0.84 [70]~E(x701,x702)+E(f39(x703,x701),f39(x703,x702)) % 0.53/0.84 [71]~E(x711,x712)+E(f45(x711,x713,x714),f45(x712,x713,x714)) % 0.53/0.84 [72]~E(x721,x722)+E(f45(x723,x721,x724),f45(x723,x722,x724)) % 0.53/0.84 [73]~E(x731,x732)+E(f45(x733,x734,x731),f45(x733,x734,x732)) % 0.53/0.84 [74]~E(x741,x742)+E(f36(x741,x743),f36(x742,x743)) % 0.53/0.84 [75]~E(x751,x752)+E(f36(x753,x751),f36(x753,x752)) % 0.53/0.84 [76]~E(x761,x762)+E(f10(x761,x763,x764),f10(x762,x763,x764)) % 0.53/0.84 [77]~E(x771,x772)+E(f10(x773,x771,x774),f10(x773,x772,x774)) % 0.53/0.84 [78]~E(x781,x782)+E(f10(x783,x784,x781),f10(x783,x784,x782)) % 0.53/0.84 [79]~E(x791,x792)+E(f9(x791,x793,x794),f9(x792,x793,x794)) % 0.53/0.84 [80]~E(x801,x802)+E(f9(x803,x801,x804),f9(x803,x802,x804)) % 0.53/0.84 [81]~E(x811,x812)+E(f9(x813,x814,x811),f9(x813,x814,x812)) % 0.53/0.84 [82]~E(x821,x822)+E(f13(x821,x823,x824),f13(x822,x823,x824)) % 0.53/0.84 [83]~E(x831,x832)+E(f13(x833,x831,x834),f13(x833,x832,x834)) % 0.53/0.84 [84]~E(x841,x842)+E(f13(x843,x844,x841),f13(x843,x844,x842)) % 0.53/0.84 [85]~E(x851,x852)+E(f6(x851,x853),f6(x852,x853)) % 0.53/0.84 [86]~E(x861,x862)+E(f6(x863,x861),f6(x863,x862)) % 0.53/0.84 [87]~E(x871,x872)+E(f22(x871,x873,x874),f22(x872,x873,x874)) % 0.53/0.84 [88]~E(x881,x882)+E(f22(x883,x881,x884),f22(x883,x882,x884)) % 0.53/0.84 [89]~E(x891,x892)+E(f22(x893,x894,x891),f22(x893,x894,x892)) % 0.53/0.84 [90]~E(x901,x902)+E(f18(x901,x903),f18(x902,x903)) % 0.53/0.84 [91]~E(x911,x912)+E(f18(x913,x911),f18(x913,x912)) % 0.53/0.84 [92]~E(x921,x922)+E(f38(x921,x923),f38(x922,x923)) % 0.53/0.84 [93]~E(x931,x932)+E(f38(x933,x931),f38(x933,x932)) % 0.53/0.84 [94]~E(x941,x942)+E(f55(x941,x943,x944),f55(x942,x943,x944)) % 0.53/0.84 [95]~E(x951,x952)+E(f55(x953,x951,x954),f55(x953,x952,x954)) % 0.53/0.84 [96]~E(x961,x962)+E(f55(x963,x964,x961),f55(x963,x964,x962)) % 0.53/0.84 [97]~E(x971,x972)+E(f8(x971,x973,x974,x975),f8(x972,x973,x974,x975)) % 0.53/0.84 [98]~E(x981,x982)+E(f8(x983,x981,x984,x985),f8(x983,x982,x984,x985)) % 0.53/0.84 [99]~E(x991,x992)+E(f8(x993,x994,x991,x995),f8(x993,x994,x992,x995)) % 0.53/0.84 [100]~E(x1001,x1002)+E(f8(x1003,x1004,x1005,x1001),f8(x1003,x1004,x1005,x1002)) % 0.53/0.84 [101]~E(x1011,x1012)+E(f24(x1011,x1013),f24(x1012,x1013)) % 0.53/0.84 [102]~E(x1021,x1022)+E(f24(x1023,x1021),f24(x1023,x1022)) % 0.53/0.84 [103]~E(x1031,x1032)+E(f15(x1031,x1033,x1034),f15(x1032,x1033,x1034)) % 0.53/0.84 [104]~E(x1041,x1042)+E(f15(x1043,x1041,x1044),f15(x1043,x1042,x1044)) % 0.53/0.84 [105]~E(x1051,x1052)+E(f15(x1053,x1054,x1051),f15(x1053,x1054,x1052)) % 0.53/0.84 [106]~E(x1061,x1062)+E(f42(x1061,x1063),f42(x1062,x1063)) % 0.53/0.84 [107]~E(x1071,x1072)+E(f42(x1073,x1071),f42(x1073,x1072)) % 0.53/0.84 [108]~E(x1081,x1082)+E(f26(x1081),f26(x1082)) % 0.53/0.84 [109]~E(x1091,x1092)+E(f40(x1091),f40(x1092)) % 0.53/0.84 [110]~P1(x1101)+P1(x1102)+~E(x1101,x1102) % 0.53/0.84 [111]P6(x1112,x1113)+~E(x1111,x1112)+~P6(x1111,x1113) % 0.53/0.84 [112]P6(x1123,x1122)+~E(x1121,x1122)+~P6(x1123,x1121) % 0.53/0.84 [113]P2(x1132,x1133)+~E(x1131,x1132)+~P2(x1131,x1133) % 0.53/0.84 [114]P2(x1143,x1142)+~E(x1141,x1142)+~P2(x1143,x1141) % 0.53/0.84 [115]~P5(x1151)+P5(x1152)+~E(x1151,x1152) % 0.53/0.84 [116]P8(x1162,x1163)+~E(x1161,x1162)+~P8(x1161,x1163) % 0.53/0.84 [117]P8(x1173,x1172)+~E(x1171,x1172)+~P8(x1173,x1171) % 0.53/0.84 [118]P3(x1182,x1183)+~E(x1181,x1182)+~P3(x1181,x1183) % 0.53/0.84 [119]P3(x1193,x1192)+~E(x1191,x1192)+~P3(x1193,x1191) % 0.53/0.84 [120]P7(x1202,x1203)+~E(x1201,x1202)+~P7(x1201,x1203) % 0.53/0.84 [121]P7(x1213,x1212)+~E(x1211,x1212)+~P7(x1213,x1211) % 0.53/0.84 [122]P4(x1222,x1223)+~E(x1221,x1222)+~P4(x1221,x1223) % 0.53/0.84 [123]P4(x1233,x1232)+~E(x1231,x1232)+~P4(x1233,x1231) % 0.53/0.84 % 0.53/0.84 %------------------------------------------- % 0.53/0.84 cnf(352,plain, % 0.53/0.84 (~P6(x3521,a1)), % 0.53/0.84 inference(equality_inference,[],[170])). % 0.53/0.84 cnf(360,plain, % 0.53/0.84 (~P6(x3601,f56(x3602,x3602))+E(x3601,x3602)), % 0.53/0.84 inference(equality_inference,[],[208])). % 0.53/0.84 cnf(362,plain, % 0.53/0.84 (~P6(x3621,x3622)+P6(x3621,f52(x3623,x3622))), % 0.53/0.84 inference(equality_inference,[],[224])). % 0.53/0.84 cnf(363,plain, % 0.53/0.84 (~P6(x3631,x3632)+P6(x3631,f52(x3632,x3633))), % 0.53/0.84 inference(equality_inference,[],[225])). % 0.53/0.84 cnf(364,plain, % 0.53/0.84 (~P6(x3641,f49(x3642,x3643))+P6(x3641,x3642)), % 0.53/0.84 inference(equality_inference,[],[226])). % 0.53/0.84 cnf(365,plain, % 0.53/0.84 (~P6(x3651,x3652)+P6(x3651,f48(x3653))+~P6(x3652,x3653)), % 0.53/0.84 inference(equality_inference,[],[238])). % 0.53/0.84 cnf(366,plain, % 0.53/0.84 (~P6(x3661,x3662)+~P6(x3661,f49(x3663,x3662))), % 0.53/0.84 inference(equality_inference,[],[239])). % 0.53/0.84 cnf(367,plain, % 0.53/0.84 (P6(x3671,x3672)+~P6(x3672,x3673)+~P6(x3671,f53(x3673))+E(x3673,a1)), % 0.53/0.84 inference(equality_inference,[],[244])). % 0.53/0.84 cnf(368,plain, % 0.53/0.84 (~P6(x3681,x3682)+P6(x3681,f49(x3682,x3683))+P6(x3681,x3683)), % 0.53/0.84 inference(equality_inference,[],[251])). % 0.53/0.84 cnf(369,plain, % 0.53/0.84 (~P6(x3691,f52(x3692,x3693))+P6(x3691,x3693)+P6(x3691,x3692)), % 0.53/0.84 inference(equality_inference,[],[252])). % 0.53/0.84 cnf(370,plain, % 0.53/0.84 (~P6(x3701,f49(x3702,f49(x3702,x3703)))+P6(x3701,x3703)), % 0.53/0.84 inference(equality_inference,[],[279])). % 0.53/0.84 cnf(374,plain, % 0.53/0.84 (~P6(x3741,f48(x3742))+P6(f13(x3742,f48(x3742),x3741),x3742)), % 0.53/0.84 inference(equality_inference,[],[301])). % 0.53/0.84 cnf(380,plain, % 0.53/0.84 (~P5(x3801)+P6(x3802,f51(x3801))+~P6(f56(f56(x3803,x3802),f56(x3803,x3803)),x3801)), % 0.53/0.84 inference(equality_inference,[],[319])). % 0.53/0.84 cnf(381,plain, % 0.53/0.84 (~P5(x3811)+P6(x3812,f50(x3811))+~P6(f56(f56(x3812,x3813),f56(x3812,x3812)),x3811)), % 0.53/0.84 inference(equality_inference,[],[320])). % 0.53/0.84 cnf(382,plain, % 0.53/0.84 (~P6(x3821,f3(x3822,x3823))+P6(f47(x3822,x3823,f3(x3822,x3823),x3821),x3822)), % 0.53/0.84 inference(equality_inference,[],[340])). % 0.53/0.84 cnf(383,plain, % 0.53/0.84 (~P6(x3831,f3(x3832,x3833))+P6(f8(x3832,x3833,f3(x3832,x3833),x3831),x3833)), % 0.53/0.84 inference(equality_inference,[],[341])). % 0.53/0.84 cnf(388,plain, % 0.53/0.84 (E(f52(x3881,x3881),x3881)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(395,plain, % 0.53/0.84 (P8(x3951,x3951)), % 0.53/0.84 inference(rename_variables,[],[136])). % 0.53/0.84 cnf(398,plain, % 0.53/0.84 (P8(x3981,x3981)), % 0.53/0.84 inference(rename_variables,[],[136])). % 0.53/0.84 cnf(413,plain, % 0.53/0.84 (~P6(x4131,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(416,plain, % 0.53/0.84 (~P6(x4161,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(419,plain, % 0.53/0.84 (~P6(x4191,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(435,plain, % 0.53/0.84 (P2(f5(x4351),x4351)), % 0.53/0.84 inference(rename_variables,[],[141])). % 0.53/0.84 cnf(442,plain, % 0.53/0.84 (~P6(x4421,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(445,plain, % 0.53/0.84 (P2(x4451,f34(x4451))), % 0.53/0.84 inference(rename_variables,[],[140])). % 0.53/0.84 cnf(448,plain, % 0.53/0.84 (P2(x4481,f34(x4481))), % 0.53/0.84 inference(rename_variables,[],[140])). % 0.53/0.84 cnf(451,plain, % 0.53/0.84 (P2(x4511,f34(x4511))), % 0.53/0.84 inference(rename_variables,[],[140])). % 0.53/0.84 cnf(454,plain, % 0.53/0.84 (P2(x4541,f34(x4541))), % 0.53/0.84 inference(rename_variables,[],[140])). % 0.53/0.84 cnf(457,plain, % 0.53/0.84 (P2(f5(x4571),x4571)), % 0.53/0.84 inference(rename_variables,[],[141])). % 0.53/0.84 cnf(460,plain, % 0.53/0.84 (E(f52(x4601,x4601),x4601)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(463,plain, % 0.53/0.84 (E(f52(x4631,x4631),x4631)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(466,plain, % 0.53/0.84 (E(f52(x4661,x4661),x4661)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(469,plain, % 0.53/0.84 (E(f52(x4691,a1),x4691)), % 0.53/0.84 inference(rename_variables,[],[133])). % 0.53/0.84 cnf(472,plain, % 0.53/0.84 (E(f52(x4721,a1),x4721)), % 0.53/0.84 inference(rename_variables,[],[133])). % 0.53/0.84 cnf(475,plain, % 0.53/0.84 (P8(x4751,f52(x4751,x4752))), % 0.53/0.84 inference(rename_variables,[],[146])). % 0.53/0.84 cnf(478,plain, % 0.53/0.84 (E(f52(x4781,x4781),x4781)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(481,plain, % 0.53/0.84 (E(f52(x4811,x4811),x4811)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(484,plain, % 0.53/0.84 (E(f52(x4841,x4841),x4841)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(487,plain, % 0.53/0.84 (P2(f5(x4871),x4871)), % 0.53/0.84 inference(rename_variables,[],[141])). % 0.53/0.84 cnf(490,plain, % 0.53/0.84 (E(f52(x4901,x4901),x4901)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(496,plain, % 0.53/0.84 (P2(x4961,f34(x4961))), % 0.53/0.84 inference(rename_variables,[],[140])). % 0.53/0.84 cnf(499,plain, % 0.53/0.84 (E(f52(x4991,x4991),x4991)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(502,plain, % 0.53/0.84 (P2(x5021,f34(x5021))), % 0.53/0.84 inference(rename_variables,[],[140])). % 0.53/0.84 cnf(505,plain, % 0.53/0.84 (~P6(x5051,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(506,plain, % 0.53/0.84 (E(f52(x5061,x5061),x5061)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(509,plain, % 0.53/0.84 (~P6(x5091,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(510,plain, % 0.53/0.84 (E(f52(x5101,x5101),x5101)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(513,plain, % 0.53/0.84 (~P6(x5131,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(514,plain, % 0.53/0.84 (E(f52(x5141,x5141),x5141)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(519,plain, % 0.53/0.84 (~P6(x5191,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(530,plain, % 0.53/0.84 (~P6(x5301,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(532,plain, % 0.53/0.84 (E(f52(x5321,x5321),x5321)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(534,plain, % 0.53/0.84 (E(f52(x5341,x5341),x5341)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(544,plain, % 0.53/0.84 (E(f52(x5441,x5441),x5441)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(557,plain, % 0.53/0.84 (~P6(x5571,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(560,plain, % 0.53/0.84 (~P6(x5601,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(563,plain, % 0.53/0.84 (~P6(x5631,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(566,plain, % 0.53/0.84 (~P6(x5661,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(569,plain, % 0.53/0.84 (~P6(x5691,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(575,plain, % 0.53/0.84 (E(f52(x5751,a1),x5751)), % 0.53/0.84 inference(rename_variables,[],[133])). % 0.53/0.84 cnf(580,plain, % 0.53/0.84 (~P6(x5801,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(583,plain, % 0.53/0.84 (E(f52(x5831,x5831),x5831)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(586,plain, % 0.53/0.84 (E(f52(x5861,x5861),x5861)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(589,plain, % 0.53/0.84 (E(f52(x5891,x5891),x5891)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(592,plain, % 0.53/0.84 (E(f52(x5921,x5921),x5921)), % 0.53/0.84 inference(rename_variables,[],[137])). % 0.53/0.84 cnf(595,plain, % 0.53/0.84 (~E(f56(x5951,x5951),a1)), % 0.53/0.84 inference(rename_variables,[],[156])). % 0.53/0.84 cnf(598,plain, % 0.53/0.84 (~P6(x5981,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(601,plain, % 0.53/0.84 (~P6(x6011,a1)), % 0.53/0.84 inference(rename_variables,[],[352])). % 0.53/0.84 cnf(604,plain, % 0.53/0.84 (~E(f56(x6041,x6041),a1)), % 0.53/0.84 inference(rename_variables,[],[156])). % 0.53/0.84 cnf(612,plain, % 0.53/0.84 ($false), % 0.53/0.84 inference(scs_inference,[],[128,153,352,413,416,419,442,505,509,513,519,530,557,560,563,566,569,580,598,601,136,395,398,132,137,388,460,463,466,478,481,484,490,499,506,510,514,532,534,544,583,586,589,592,138,140,445,448,451,454,496,502,141,435,457,487,142,143,146,475,147,133,469,472,575,134,124,125,154,156,595,604,145,170,173,198,255,256,360,362,363,364,366,370,374,382,383,171,185,2,168,169,179,180,205,214,215,216,242,243,277,278,188,190,191,201,202,208,219,224,225,226,227,239,240,241,279,289,301,340,341,365,368,369,380,381,111,112,3,110,113,114,116,117,163,164,175,186,206,245,264,269,321,322,210,238,251,252,290,319,320,367,318,333,244,284,209]), % 0.53/0.84 ['proof']). % 0.53/0.84 % SZS output end Proof % 0.53/0.84 % Total time :0.150000s %------------------------------------------------------------------------------