%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU149+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 : n027.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:20 EDT 2024 % Result : Theorem 0.73s 0.82s % Output : CNFRefutation 0.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SEU149+2 : TPTP v8.2.0. Released v3.3.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.34 % Computer : n027.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Jun 21 12:50:39 EDT 2024 % 0.14/0.34 % CPUTime : % 0.21/0.58 start to proof:theBenchmark % 0.73/0.80 %------------------------------------------- % 0.73/0.80 % File :CSE---1.7 % 0.73/0.80 % Problem :theBenchmark % 0.73/0.80 % Transform :cnf % 0.73/0.80 % Format :tptp:raw % 0.73/0.80 % Command :java -jar mcs_scs.jar %d %s % 0.73/0.80 % 0.73/0.80 % Result :Theorem 0.170000s % 0.73/0.80 % Output :CNFRefutation 0.170000s % 0.73/0.80 %------------------------------------------- % 0.73/0.81 %------------------------------------------------------------------------------ % 0.73/0.81 % File : SEU149+2 : TPTP v8.2.0. Released v3.3.0. % 0.73/0.81 % Domain : Set theory % 0.73/0.81 % Problem : MPTP chainy problem t8_zfmisc_1 % 0.73/0.81 % Version : [Urb07] axioms : Especial. % 0.73/0.81 % English : % 0.73/0.81 % 0.73/0.81 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.73/0.81 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.73/0.81 % Source : [Urb07] % 0.73/0.81 % Names : chainy-t8_zfmisc_1 [Urb07] % 0.73/0.81 % 0.73/0.81 % Status : Theorem % 0.73/0.81 % Rating : 0.19 v7.5.0, 0.22 v7.4.0, 0.17 v7.3.0, 0.14 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.08 v6.3.0, 0.17 v6.2.0, 0.32 v6.1.0, 0.33 v6.0.0, 0.35 v5.5.0, 0.26 v5.4.0, 0.29 v5.3.0, 0.30 v5.2.0, 0.05 v5.0.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.26 v3.4.0, 0.21 v3.3.0 % 0.73/0.81 % Syntax : Number of formulae : 72 ( 31 unt; 0 def) % 0.73/0.81 % Number of atoms : 140 ( 43 equ) % 0.73/0.81 % Maximal formula atoms : 6 ( 1 avg) % 0.73/0.81 % Number of connectives : 92 ( 24 ~; 4 |; 20 &) % 0.73/0.81 % ( 23 <=>; 21 =>; 0 <=; 0 <~>) % 0.73/0.81 % Maximal formula depth : 9 ( 4 avg) % 0.73/0.81 % Maximal term depth : 3 ( 1 avg) % 0.73/0.81 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 0.73/0.81 % Number of functors : 7 ( 7 usr; 1 con; 0-2 aty) % 0.73/0.81 % Number of variables : 139 ( 135 !; 4 ?) % 0.73/0.81 % SPC : FOF_THM_RFO_SEQ % 0.73/0.81 % 0.73/0.81 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.73/0.81 % library, www.mizar.org % 0.73/0.81 %------------------------------------------------------------------------------ % 0.73/0.81 fof(antisymmetry_r2_hidden,axiom, % 0.73/0.81 ! [A,B] : % 0.73/0.81 ( in(A,B) % 0.73/0.81 => ~ in(B,A) ) ). % 0.73/0.81 % 0.73/0.81 fof(antisymmetry_r2_xboole_0,axiom, % 0.73/0.81 ! [A,B] : % 0.73/0.81 ( proper_subset(A,B) % 0.73/0.81 => ~ proper_subset(B,A) ) ). % 0.73/0.81 % 0.73/0.81 fof(commutativity_k2_tarski,axiom, % 0.73/0.81 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 0.73/0.81 % 0.73/0.81 fof(commutativity_k2_xboole_0,axiom, % 0.73/0.81 ! [A,B] : set_union2(A,B) = set_union2(B,A) ). % 0.73/0.81 % 0.73/0.81 fof(commutativity_k3_xboole_0,axiom, % 0.73/0.81 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 0.73/0.81 % 0.73/0.81 fof(d10_xboole_0,axiom, % 0.73/0.81 ! [A,B] : % 0.73/0.81 ( A = B % 0.73/0.81 <=> ( subset(A,B) % 0.73/0.81 & subset(B,A) ) ) ). % 0.73/0.81 % 0.73/0.81 fof(d1_tarski,axiom, % 0.73/0.81 ! [A,B] : % 0.73/0.81 ( B = singleton(A) % 0.73/0.81 <=> ! [C] : % 0.73/0.81 ( in(C,B) % 0.73/0.81 <=> C = A ) ) ). % 0.73/0.81 % 0.73/0.81 fof(d1_xboole_0,axiom, % 0.73/0.81 ! [A] : % 0.73/0.81 ( A = empty_set % 0.73/0.81 <=> ! [B] : ~ in(B,A) ) ). % 0.73/0.81 % 0.73/0.81 fof(d1_zfmisc_1,axiom, % 0.73/0.81 ! [A,B] : % 0.73/0.81 ( B = powerset(A) % 0.73/0.81 <=> ! [C] : % 0.73/0.81 ( in(C,B) % 0.73/0.81 <=> subset(C,A) ) ) ). % 0.73/0.81 % 0.73/0.81 fof(d2_tarski,axiom, % 0.73/0.81 ! [A,B,C] : % 0.73/0.81 ( C = unordered_pair(A,B) % 0.73/0.81 <=> ! [D] : % 0.73/0.81 ( in(D,C) % 0.73/0.81 <=> ( D = A % 0.73/0.81 | D = B ) ) ) ). % 0.73/0.81 % 0.73/0.81 fof(d2_xboole_0,axiom, % 0.73/0.81 ! [A,B,C] : % 0.73/0.81 ( C = set_union2(A,B) % 0.73/0.81 <=> ! [D] : % 0.73/0.81 ( in(D,C) % 0.73/0.81 <=> ( in(D,A) % 0.73/0.81 | in(D,B) ) ) ) ). % 0.73/0.81 % 0.73/0.81 fof(d3_tarski,axiom, % 0.73/0.81 ! [A,B] : % 0.73/0.81 ( subset(A,B) % 0.73/0.81 <=> ! [C] : % 0.73/0.81 ( in(C,A) % 0.73/0.81 => in(C,B) ) ) ). % 0.73/0.81 % 0.73/0.81 fof(d3_xboole_0,axiom, % 0.73/0.81 ! [A,B,C] : % 0.73/0.81 ( C = set_intersection2(A,B) % 0.73/0.81 <=> ! [D] : % 0.73/0.81 ( in(D,C) % 0.73/0.81 <=> ( in(D,A) % 0.73/0.81 & in(D,B) ) ) ) ). % 0.73/0.81 % 0.73/0.81 fof(d4_xboole_0,axiom, % 0.73/0.81 ! [A,B,C] : % 0.73/0.81 ( C = set_difference(A,B) % 0.73/0.81 <=> ! [D] : % 0.73/0.81 ( in(D,C) % 0.73/0.81 <=> ( in(D,A) % 0.73/0.81 & ~ in(D,B) ) ) ) ). % 0.73/0.81 % 0.73/0.81 fof(d7_xboole_0,axiom, % 0.73/0.81 ! [A,B] : % 0.73/0.81 ( disjoint(A,B) % 0.73/0.81 <=> set_intersection2(A,B) = empty_set ) ). % 0.73/0.81 % 0.73/0.81 fof(d8_xboole_0,axiom, % 0.73/0.81 ! [A,B] : % 0.73/0.81 ( proper_subset(A,B) % 0.73/0.81 <=> ( subset(A,B) % 0.73/0.81 & A != B ) ) ). % 0.73/0.81 % 0.73/0.81 fof(dt_k1_tarski,axiom, % 0.73/0.81 $true ). % 0.73/0.81 % 0.73/0.81 fof(dt_k1_xboole_0,axiom, % 0.73/0.81 $true ). % 0.73/0.81 % 0.73/0.81 fof(dt_k1_zfmisc_1,axiom, % 0.73/0.81 $true ). % 0.73/0.81 % 0.73/0.81 fof(dt_k2_tarski,axiom, % 0.73/0.81 $true ). % 0.73/0.81 % 0.73/0.81 fof(dt_k2_xboole_0,axiom, % 0.73/0.81 $true ). % 0.73/0.81 % 0.73/0.81 fof(dt_k3_xboole_0,axiom, % 0.73/0.81 $true ). % 0.73/0.81 % 0.73/0.81 fof(dt_k4_xboole_0,axiom, % 0.73/0.81 $true ). % 0.73/0.81 % 0.73/0.81 fof(fc1_xboole_0,axiom, % 0.73/0.81 empty(empty_set) ). % 0.73/0.82 % 0.73/0.82 fof(fc2_xboole_0,axiom, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( ~ empty(A) % 0.73/0.82 => ~ empty(set_union2(A,B)) ) ). % 0.73/0.82 % 0.73/0.82 fof(fc3_xboole_0,axiom, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( ~ empty(A) % 0.73/0.82 => ~ empty(set_union2(B,A)) ) ). % 0.73/0.82 % 0.73/0.82 fof(idempotence_k2_xboole_0,axiom, % 0.73/0.82 ! [A,B] : set_union2(A,A) = A ). % 0.73/0.82 % 0.73/0.82 fof(idempotence_k3_xboole_0,axiom, % 0.73/0.82 ! [A,B] : set_intersection2(A,A) = A ). % 0.73/0.82 % 0.73/0.82 fof(irreflexivity_r2_xboole_0,axiom, % 0.73/0.82 ! [A,B] : ~ proper_subset(A,A) ). % 0.73/0.82 % 0.73/0.82 fof(l1_zfmisc_1,lemma, % 0.73/0.82 ! [A] : singleton(A) != empty_set ). % 0.73/0.82 % 0.73/0.82 fof(l2_zfmisc_1,lemma, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( subset(singleton(A),B) % 0.73/0.82 <=> in(A,B) ) ). % 0.73/0.82 % 0.73/0.82 fof(l32_xboole_1,lemma, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( set_difference(A,B) = empty_set % 0.73/0.82 <=> subset(A,B) ) ). % 0.73/0.82 % 0.73/0.82 fof(l3_zfmisc_1,lemma, % 0.73/0.82 ! [A,B,C] : % 0.73/0.82 ( subset(A,B) % 0.73/0.82 => ( in(C,A) % 0.73/0.82 | subset(A,set_difference(B,singleton(C))) ) ) ). % 0.73/0.82 % 0.73/0.82 fof(l4_zfmisc_1,lemma, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( subset(A,singleton(B)) % 0.73/0.82 <=> ( A = empty_set % 0.73/0.82 | A = singleton(B) ) ) ). % 0.73/0.82 % 0.73/0.82 fof(rc1_xboole_0,axiom, % 0.73/0.82 ? [A] : empty(A) ). % 0.73/0.82 % 0.73/0.82 fof(rc2_xboole_0,axiom, % 0.73/0.82 ? [A] : ~ empty(A) ). % 0.73/0.82 % 0.73/0.82 fof(reflexivity_r1_tarski,axiom, % 0.73/0.82 ! [A,B] : subset(A,A) ). % 0.73/0.82 % 0.73/0.82 fof(symmetry_r1_xboole_0,axiom, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( disjoint(A,B) % 0.73/0.82 => disjoint(B,A) ) ). % 0.73/0.82 % 0.73/0.82 fof(t12_xboole_1,lemma, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( subset(A,B) % 0.73/0.82 => set_union2(A,B) = B ) ). % 0.73/0.82 % 0.73/0.82 fof(t17_xboole_1,lemma, % 0.73/0.82 ! [A,B] : subset(set_intersection2(A,B),A) ). % 0.73/0.82 % 0.73/0.82 fof(t19_xboole_1,lemma, % 0.73/0.82 ! [A,B,C] : % 0.73/0.82 ( ( subset(A,B) % 0.73/0.82 & subset(A,C) ) % 0.73/0.82 => subset(A,set_intersection2(B,C)) ) ). % 0.73/0.82 % 0.73/0.82 fof(t1_boole,axiom, % 0.73/0.82 ! [A] : set_union2(A,empty_set) = A ). % 0.73/0.82 % 0.73/0.82 fof(t1_xboole_1,lemma, % 0.73/0.82 ! [A,B,C] : % 0.73/0.82 ( ( subset(A,B) % 0.73/0.82 & subset(B,C) ) % 0.73/0.82 => subset(A,C) ) ). % 0.73/0.82 % 0.73/0.82 fof(t1_zfmisc_1,lemma, % 0.73/0.82 powerset(empty_set) = singleton(empty_set) ). % 0.73/0.82 % 0.73/0.82 fof(t26_xboole_1,lemma, % 0.73/0.82 ! [A,B,C] : % 0.73/0.82 ( subset(A,B) % 0.73/0.82 => subset(set_intersection2(A,C),set_intersection2(B,C)) ) ). % 0.73/0.82 % 0.73/0.82 fof(t28_xboole_1,lemma, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( subset(A,B) % 0.73/0.82 => set_intersection2(A,B) = A ) ). % 0.73/0.82 % 0.73/0.82 fof(t2_boole,axiom, % 0.73/0.82 ! [A] : set_intersection2(A,empty_set) = empty_set ). % 0.73/0.82 % 0.73/0.82 fof(t2_tarski,axiom, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( ! [C] : % 0.73/0.82 ( in(C,A) % 0.73/0.82 <=> in(C,B) ) % 0.73/0.82 => A = B ) ). % 0.73/0.82 % 0.73/0.82 fof(t2_xboole_1,lemma, % 0.73/0.82 ! [A] : subset(empty_set,A) ). % 0.73/0.82 % 0.73/0.82 fof(t33_xboole_1,lemma, % 0.73/0.82 ! [A,B,C] : % 0.73/0.82 ( subset(A,B) % 0.73/0.82 => subset(set_difference(A,C),set_difference(B,C)) ) ). % 0.73/0.82 % 0.73/0.82 fof(t36_xboole_1,lemma, % 0.73/0.82 ! [A,B] : subset(set_difference(A,B),A) ). % 0.73/0.82 % 0.73/0.82 fof(t37_xboole_1,lemma, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( set_difference(A,B) = empty_set % 0.73/0.82 <=> subset(A,B) ) ). % 0.73/0.82 % 0.73/0.82 fof(t39_xboole_1,lemma, % 0.73/0.82 ! [A,B] : set_union2(A,set_difference(B,A)) = set_union2(A,B) ). % 0.73/0.82 % 0.73/0.82 fof(t3_boole,axiom, % 0.73/0.82 ! [A] : set_difference(A,empty_set) = A ). % 0.73/0.82 % 0.73/0.82 fof(t3_xboole_0,lemma, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( ~ ( ~ disjoint(A,B) % 0.73/0.82 & ! [C] : % 0.73/0.82 ~ ( in(C,A) % 0.73/0.82 & in(C,B) ) ) % 0.73/0.82 & ~ ( ? [C] : % 0.73/0.82 ( in(C,A) % 0.73/0.82 & in(C,B) ) % 0.73/0.82 & disjoint(A,B) ) ) ). % 0.73/0.82 % 0.73/0.82 fof(t3_xboole_1,lemma, % 0.73/0.82 ! [A] : % 0.73/0.82 ( subset(A,empty_set) % 0.73/0.82 => A = empty_set ) ). % 0.73/0.82 % 0.73/0.82 fof(t40_xboole_1,lemma, % 0.73/0.82 ! [A,B] : set_difference(set_union2(A,B),B) = set_difference(A,B) ). % 0.73/0.82 % 0.73/0.82 fof(t45_xboole_1,lemma, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( subset(A,B) % 0.73/0.82 => B = set_union2(A,set_difference(B,A)) ) ). % 0.73/0.82 % 0.73/0.82 fof(t48_xboole_1,lemma, % 0.73/0.82 ! [A,B] : set_difference(A,set_difference(A,B)) = set_intersection2(A,B) ). % 0.73/0.82 % 0.73/0.82 fof(t4_boole,axiom, % 0.73/0.82 ! [A] : set_difference(empty_set,A) = empty_set ). % 0.73/0.82 % 0.73/0.82 fof(t4_xboole_0,lemma, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( ~ ( ~ disjoint(A,B) % 0.73/0.82 & ! [C] : ~ in(C,set_intersection2(A,B)) ) % 0.73/0.82 & ~ ( ? [C] : in(C,set_intersection2(A,B)) % 0.73/0.82 & disjoint(A,B) ) ) ). % 0.73/0.82 % 0.73/0.82 fof(t60_xboole_1,lemma, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ~ ( subset(A,B) % 0.73/0.82 & proper_subset(B,A) ) ). % 0.73/0.82 % 0.73/0.82 fof(t63_xboole_1,lemma, % 0.73/0.82 ! [A,B,C] : % 0.73/0.82 ( ( subset(A,B) % 0.73/0.82 & disjoint(B,C) ) % 0.73/0.82 => disjoint(A,C) ) ). % 0.73/0.82 % 0.73/0.82 fof(t69_enumset1,lemma, % 0.73/0.82 ! [A] : unordered_pair(A,A) = singleton(A) ). % 0.73/0.82 % 0.73/0.82 fof(t6_boole,axiom, % 0.73/0.82 ! [A] : % 0.73/0.82 ( empty(A) % 0.73/0.82 => A = empty_set ) ). % 0.73/0.82 % 0.73/0.82 fof(t6_zfmisc_1,lemma, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( subset(singleton(A),singleton(B)) % 0.73/0.82 => A = B ) ). % 0.73/0.82 % 0.73/0.82 fof(t7_boole,axiom, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ~ ( in(A,B) % 0.73/0.82 & empty(B) ) ). % 0.73/0.82 % 0.73/0.82 fof(t7_xboole_1,lemma, % 0.73/0.82 ! [A,B] : subset(A,set_union2(A,B)) ). % 0.73/0.82 % 0.73/0.82 fof(t83_xboole_1,lemma, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ( disjoint(A,B) % 0.73/0.82 <=> set_difference(A,B) = A ) ). % 0.73/0.82 % 0.73/0.82 fof(t8_boole,axiom, % 0.73/0.82 ! [A,B] : % 0.73/0.82 ~ ( empty(A) % 0.73/0.82 & A != B % 0.73/0.82 & empty(B) ) ). % 0.73/0.82 % 0.73/0.82 fof(t8_xboole_1,lemma, % 0.73/0.82 ! [A,B,C] : % 0.73/0.82 ( ( subset(A,B) % 0.73/0.82 & subset(C,B) ) % 0.73/0.82 => subset(set_union2(A,C),B) ) ). % 0.73/0.82 % 0.73/0.82 fof(t8_zfmisc_1,conjecture, % 0.73/0.82 ! [A,B,C] : % 0.73/0.82 ( singleton(A) = unordered_pair(B,C) % 0.73/0.82 => A = B ) ). % 0.73/0.82 % 0.73/0.82 %------------------------------------------------------------------------------ % 0.73/0.82 %------------------------------------------- % 0.73/0.82 % Proof found % 0.73/0.82 % SZS status Theorem for theBenchmark % 0.73/0.82 % SZS output start Proof % 0.73/0.82 %ClaNum:152(EqnAxiom:44) % 0.73/0.82 %VarNum:587(SingletonVarNum:224) % 0.73/0.82 %MaxLitNum:4 % 0.73/0.82 %MaxfuncDepth:2 % 0.73/0.82 %SharedTerms:16 % 0.73/0.82 %goalClause: 54 65 % 0.73/0.82 %singleGoalClaCount:2 % 0.73/0.82 [45]P1(a1) % 0.73/0.82 [46]P1(a2) % 0.73/0.82 [65]~E(a3,a8) % 0.73/0.82 [66]~P1(a4) % 0.73/0.82 [51]E(f21(a1,a1),f19(a1)) % 0.73/0.82 [54]E(f21(a3,a3),f21(a8,a9)) % 0.73/0.82 [48]P3(a1,x481) % 0.73/0.82 [52]P3(x521,x521) % 0.73/0.82 [68]~P4(x681,x681) % 0.73/0.82 [47]E(f18(a1,x471),a1) % 0.73/0.82 [49]E(f20(x491,a1),x491) % 0.73/0.82 [50]E(f18(x501,a1),x501) % 0.73/0.82 [53]E(f20(x531,x531),x531) % 0.73/0.82 [67]~E(f21(x671,x671),a1) % 0.73/0.82 [57]E(f18(x571,f18(x571,a1)),a1) % 0.73/0.82 [60]E(f18(x601,f18(x601,x601)),x601) % 0.73/0.82 [55]E(f21(x551,x552),f21(x552,x551)) % 0.73/0.82 [56]E(f20(x561,x562),f20(x562,x561)) % 0.73/0.82 [58]P3(x581,f20(x581,x582)) % 0.73/0.82 [59]P3(f18(x591,x592),x591) % 0.73/0.82 [61]E(f20(x611,f18(x612,x611)),f20(x611,x612)) % 0.73/0.82 [62]E(f18(f20(x621,x622),x622),f18(x621,x622)) % 0.73/0.82 [63]E(f18(x631,f18(x631,x632)),f18(x632,f18(x632,x631))) % 0.73/0.82 [69]~P1(x691)+E(x691,a1) % 0.73/0.82 [73]~P3(x731,a1)+E(x731,a1) % 0.73/0.82 [74]P5(f10(x741),x741)+E(x741,a1) % 0.73/0.82 [72]~E(x721,x722)+P3(x721,x722) % 0.73/0.82 [75]~P5(x752,x751)+~E(x751,a1) % 0.73/0.82 [76]~P4(x761,x762)+~E(x761,x762) % 0.73/0.82 [77]~P1(x771)+~P5(x772,x771) % 0.73/0.82 [82]~P4(x821,x822)+P3(x821,x822) % 0.73/0.82 [83]~P2(x832,x831)+P2(x831,x832) % 0.73/0.82 [92]~P5(x922,x921)+~P5(x921,x922) % 0.73/0.82 [93]~P4(x932,x931)+~P4(x931,x932) % 0.73/0.82 [94]~P3(x942,x941)+~P4(x941,x942) % 0.73/0.82 [79]~P3(x791,x792)+E(f18(x791,x792),a1) % 0.73/0.82 [81]P3(x811,x812)+~E(f18(x811,x812),a1) % 0.73/0.82 [84]~P3(x841,x842)+E(f20(x841,x842),x842) % 0.73/0.82 [85]~P2(x851,x852)+E(f18(x851,x852),x851) % 0.73/0.82 [86]P2(x861,x862)+~E(f18(x861,x862),x861) % 0.73/0.82 [91]~E(x911,a1)+P3(x911,f21(x912,x912)) % 0.73/0.82 [100]P1(x1001)+~P1(f20(x1002,x1001)) % 0.73/0.82 [101]P1(x1011)+~P1(f20(x1011,x1012)) % 0.73/0.82 [102]P3(x1021,x1022)+P5(f12(x1021,x1022),x1021) % 0.73/0.82 [103]P2(x1031,x1032)+P5(f5(x1031,x1032),x1032) % 0.73/0.82 [104]P2(x1041,x1042)+P5(f5(x1041,x1042),x1041) % 0.73/0.82 [112]~P5(x1121,x1122)+P3(f21(x1121,x1121),x1122) % 0.73/0.83 [122]P5(x1221,x1222)+~P3(f21(x1221,x1221),x1222) % 0.73/0.83 [123]P3(x1231,x1232)+~P5(f12(x1231,x1232),x1232) % 0.73/0.83 [132]E(x1321,x1322)+~P3(f21(x1321,x1321),f21(x1322,x1322)) % 0.73/0.83 [111]~P2(x1111,x1112)+E(f18(x1111,f18(x1111,x1112)),a1) % 0.73/0.83 [113]~P3(x1131,x1132)+E(f20(x1131,f18(x1132,x1131)),x1132) % 0.73/0.83 [114]~P3(x1141,x1142)+E(f18(x1141,f18(x1141,x1142)),x1141) % 0.73/0.83 [121]P2(x1211,x1212)+~E(f18(x1211,f18(x1211,x1212)),a1) % 0.73/0.83 [137]P2(x1371,x1372)+P5(f7(x1371,x1372),f18(x1371,f18(x1371,x1372))) % 0.73/0.83 [128]~P3(x1281,x1283)+P3(f18(x1281,x1282),f18(x1283,x1282)) % 0.73/0.83 [139]~P2(x1391,x1392)+~P5(x1393,f18(x1391,f18(x1391,x1392))) % 0.73/0.83 [140]~P3(x1401,x1403)+P3(f18(x1401,f18(x1401,x1402)),f18(x1403,f18(x1403,x1402))) % 0.73/0.83 [70]~P1(x702)+~P1(x701)+E(x701,x702) % 0.73/0.83 [87]P4(x871,x872)+~P3(x871,x872)+E(x871,x872) % 0.73/0.83 [97]~P3(x972,x971)+~P3(x971,x972)+E(x971,x972) % 0.73/0.83 [118]E(f11(x1182,x1181),x1182)+P5(f11(x1182,x1181),x1181)+E(x1181,f21(x1182,x1182)) % 0.73/0.83 [124]E(x1241,f21(x1242,x1242))+~P3(x1241,f21(x1242,x1242))+E(x1241,a1) % 0.73/0.83 [125]E(x1251,x1252)+P5(f6(x1251,x1252),x1252)+P5(f6(x1251,x1252),x1251) % 0.73/0.83 [127]P5(f13(x1272,x1271),x1271)+P3(f13(x1272,x1271),x1272)+E(x1271,f19(x1272)) % 0.73/0.83 [131]~E(f11(x1312,x1311),x1312)+~P5(f11(x1312,x1311),x1311)+E(x1311,f21(x1312,x1312)) % 0.73/0.83 [134]E(x1341,x1342)+~P5(f6(x1341,x1342),x1342)+~P5(f6(x1341,x1342),x1341) % 0.73/0.83 [136]~P5(f13(x1362,x1361),x1361)+~P3(f13(x1362,x1361),x1362)+E(x1361,f19(x1362)) % 0.73/0.83 [105]~P3(x1053,x1052)+P5(x1051,x1052)+~P5(x1051,x1053) % 0.73/0.83 [106]~P3(x1061,x1063)+P3(x1061,x1062)+~P3(x1063,x1062) % 0.73/0.83 [107]~P2(x1073,x1072)+P2(x1071,x1072)+~P3(x1071,x1073) % 0.73/0.83 [116]~P2(x1163,x1162)+~P5(x1161,x1162)+~P5(x1161,x1163) % 0.73/0.83 [95]~P3(x951,x953)+P5(x951,x952)+~E(x952,f19(x953)) % 0.73/0.83 [96]~P5(x961,x963)+P3(x961,x962)+~E(x963,f19(x962)) % 0.73/0.83 [98]~P5(x981,x983)+E(x981,x982)+~E(x983,f21(x982,x982)) % 0.73/0.83 [126]~P3(x1262,x1263)+~P3(x1261,x1263)+P3(f20(x1261,x1262),x1263) % 0.73/0.83 [142]P5(f16(x1422,x1423,x1421),x1421)+P5(f16(x1422,x1423,x1421),x1422)+E(x1421,f18(x1422,x1423)) % 0.73/0.83 [145]~E(f14(x1452,x1453,x1451),x1453)+~P5(f14(x1452,x1453,x1451),x1451)+E(x1451,f21(x1452,x1453)) % 0.73/0.83 [146]~E(f14(x1462,x1463,x1461),x1462)+~P5(f14(x1462,x1463,x1461),x1461)+E(x1461,f21(x1462,x1463)) % 0.73/0.83 [147]P5(f16(x1472,x1473,x1471),x1471)+~P5(f16(x1472,x1473,x1471),x1473)+E(x1471,f18(x1472,x1473)) % 0.73/0.83 [149]~P5(f15(x1492,x1493,x1491),x1491)+~P5(f15(x1492,x1493,x1491),x1493)+E(x1491,f20(x1492,x1493)) % 0.73/0.83 [150]~P5(f15(x1502,x1503,x1501),x1501)+~P5(f15(x1502,x1503,x1501),x1502)+E(x1501,f20(x1502,x1503)) % 0.73/0.83 [135]~P3(x1352,x1353)+P5(x1351,x1352)+P3(x1352,f18(x1353,f21(x1351,x1351))) % 0.73/0.83 [138]~P3(x1381,x1383)+~P3(x1381,x1382)+P3(x1381,f18(x1382,f18(x1382,x1383))) % 0.73/0.83 [143]P5(f17(x1432,x1433,x1431),x1431)+P5(f17(x1432,x1433,x1431),x1433)+E(x1431,f18(x1432,f18(x1432,x1433))) % 0.73/0.83 [144]P5(f17(x1442,x1443,x1441),x1441)+P5(f17(x1442,x1443,x1441),x1442)+E(x1441,f18(x1442,f18(x1442,x1443))) % 0.73/0.83 [88]P5(x881,x882)+~E(x881,x883)+~E(x882,f21(x884,x883)) % 0.73/0.83 [89]P5(x891,x892)+~E(x891,x893)+~E(x892,f21(x893,x894)) % 0.73/0.83 [108]~P5(x1081,x1084)+P5(x1081,x1082)+~E(x1082,f20(x1083,x1084)) % 0.73/0.83 [109]~P5(x1091,x1093)+P5(x1091,x1092)+~E(x1092,f20(x1093,x1094)) % 0.73/0.83 [110]~P5(x1101,x1103)+P5(x1101,x1102)+~E(x1103,f18(x1102,x1104)) % 0.73/0.83 [117]~P5(x1174,x1173)+~P5(x1174,x1171)+~E(x1171,f18(x1172,x1173)) % 0.73/0.83 [129]~P5(x1291,x1293)+P5(x1291,x1292)+~E(x1293,f18(x1294,f18(x1294,x1292))) % 0.73/0.83 [141]E(f14(x1412,x1413,x1411),x1413)+E(f14(x1412,x1413,x1411),x1412)+P5(f14(x1412,x1413,x1411),x1411)+E(x1411,f21(x1412,x1413)) % 0.73/0.83 [148]P5(f15(x1482,x1483,x1481),x1481)+P5(f15(x1482,x1483,x1481),x1483)+P5(f15(x1482,x1483,x1481),x1482)+E(x1481,f20(x1482,x1483)) % 0.73/0.83 [151]P5(f16(x1512,x1513,x1511),x1513)+~P5(f16(x1512,x1513,x1511),x1511)+~P5(f16(x1512,x1513,x1511),x1512)+E(x1511,f18(x1512,x1513)) % 0.73/0.83 [152]~P5(f17(x1522,x1523,x1521),x1521)+~P5(f17(x1522,x1523,x1521),x1523)+~P5(f17(x1522,x1523,x1521),x1522)+E(x1521,f18(x1522,f18(x1522,x1523))) % 0.73/0.83 [99]~P5(x991,x994)+E(x991,x992)+E(x991,x993)+~E(x994,f21(x993,x992)) % 0.73/0.83 [119]~P5(x1191,x1194)+P5(x1191,x1192)+P5(x1191,x1193)+~E(x1192,f18(x1194,x1193)) % 0.73/0.83 [120]~P5(x1201,x1204)+P5(x1201,x1202)+P5(x1201,x1203)+~E(x1204,f20(x1203,x1202)) % 0.73/0.83 [133]~P5(x1331,x1334)+~P5(x1331,x1333)+P5(x1331,x1332)+~E(x1332,f18(x1333,f18(x1333,x1334))) % 0.73/0.83 %EqnAxiom % 0.73/0.83 [1]E(x11,x11) % 0.73/0.83 [2]E(x22,x21)+~E(x21,x22) % 0.73/0.83 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.73/0.83 [4]~E(x41,x42)+E(f18(x41,x43),f18(x42,x43)) % 0.73/0.83 [5]~E(x51,x52)+E(f18(x53,x51),f18(x53,x52)) % 0.73/0.83 [6]~E(x61,x62)+E(f20(x61,x63),f20(x62,x63)) % 0.73/0.83 [7]~E(x71,x72)+E(f20(x73,x71),f20(x73,x72)) % 0.73/0.83 [8]~E(x81,x82)+E(f17(x81,x83,x84),f17(x82,x83,x84)) % 0.73/0.83 [9]~E(x91,x92)+E(f17(x93,x91,x94),f17(x93,x92,x94)) % 0.73/0.83 [10]~E(x101,x102)+E(f17(x103,x104,x101),f17(x103,x104,x102)) % 0.73/0.83 [11]~E(x111,x112)+E(f21(x111,x113),f21(x112,x113)) % 0.73/0.83 [12]~E(x121,x122)+E(f21(x123,x121),f21(x123,x122)) % 0.73/0.83 [13]~E(x131,x132)+E(f19(x131),f19(x132)) % 0.73/0.83 [14]~E(x141,x142)+E(f6(x141,x143),f6(x142,x143)) % 0.73/0.83 [15]~E(x151,x152)+E(f6(x153,x151),f6(x153,x152)) % 0.73/0.83 [16]~E(x161,x162)+E(f14(x161,x163,x164),f14(x162,x163,x164)) % 0.73/0.83 [17]~E(x171,x172)+E(f14(x173,x171,x174),f14(x173,x172,x174)) % 0.73/0.83 [18]~E(x181,x182)+E(f14(x183,x184,x181),f14(x183,x184,x182)) % 0.73/0.83 [19]~E(x191,x192)+E(f16(x191,x193,x194),f16(x192,x193,x194)) % 0.73/0.83 [20]~E(x201,x202)+E(f16(x203,x201,x204),f16(x203,x202,x204)) % 0.73/0.83 [21]~E(x211,x212)+E(f16(x213,x214,x211),f16(x213,x214,x212)) % 0.73/0.83 [22]~E(x221,x222)+E(f13(x221,x223),f13(x222,x223)) % 0.73/0.83 [23]~E(x231,x232)+E(f13(x233,x231),f13(x233,x232)) % 0.73/0.83 [24]~E(x241,x242)+E(f15(x241,x243,x244),f15(x242,x243,x244)) % 0.73/0.83 [25]~E(x251,x252)+E(f15(x253,x251,x254),f15(x253,x252,x254)) % 0.73/0.83 [26]~E(x261,x262)+E(f15(x263,x264,x261),f15(x263,x264,x262)) % 0.73/0.83 [27]~E(x271,x272)+E(f5(x271,x273),f5(x272,x273)) % 0.73/0.83 [28]~E(x281,x282)+E(f5(x283,x281),f5(x283,x282)) % 0.73/0.83 [29]~E(x291,x292)+E(f11(x291,x293),f11(x292,x293)) % 0.73/0.83 [30]~E(x301,x302)+E(f11(x303,x301),f11(x303,x302)) % 0.73/0.83 [31]~E(x311,x312)+E(f7(x311,x313),f7(x312,x313)) % 0.73/0.83 [32]~E(x321,x322)+E(f7(x323,x321),f7(x323,x322)) % 0.73/0.83 [33]~E(x331,x332)+E(f12(x331,x333),f12(x332,x333)) % 0.73/0.83 [34]~E(x341,x342)+E(f12(x343,x341),f12(x343,x342)) % 0.73/0.83 [35]~E(x351,x352)+E(f10(x351),f10(x352)) % 0.73/0.83 [36]~P1(x361)+P1(x362)+~E(x361,x362) % 0.73/0.83 [37]P5(x372,x373)+~E(x371,x372)+~P5(x371,x373) % 0.73/0.83 [38]P5(x383,x382)+~E(x381,x382)+~P5(x383,x381) % 0.73/0.83 [39]P3(x392,x393)+~E(x391,x392)+~P3(x391,x393) % 0.73/0.83 [40]P3(x403,x402)+~E(x401,x402)+~P3(x403,x401) % 0.73/0.83 [41]P2(x412,x413)+~E(x411,x412)+~P2(x411,x413) % 0.73/0.83 [42]P2(x423,x422)+~E(x421,x422)+~P2(x423,x421) % 0.73/0.83 [43]P4(x432,x433)+~E(x431,x432)+~P4(x431,x433) % 0.73/0.83 [44]P4(x443,x442)+~E(x441,x442)+~P4(x443,x441) % 0.73/0.83 % 0.73/0.83 %------------------------------------------- % 0.73/0.83 cnf(154,plain, % 0.73/0.83 (~P5(x1541,a1)), % 0.73/0.83 inference(equality_inference,[],[75])). % 0.73/0.83 cnf(158,plain, % 0.73/0.83 (~P5(x1581,f19(x1582))+P3(x1581,x1582)), % 0.73/0.83 inference(equality_inference,[],[96])). % 0.73/0.83 cnf(159,plain, % 0.73/0.83 (~P5(x1591,f21(x1592,x1592))+E(x1591,x1592)), % 0.73/0.83 inference(equality_inference,[],[98])). % 0.73/0.83 cnf(160,plain, % 0.73/0.83 (~P5(x1601,f21(x1602,x1603))+E(x1601,x1603)+E(x1601,x1602)), % 0.73/0.83 inference(equality_inference,[],[99])). % 0.73/0.83 cnf(161,plain, % 0.73/0.83 (~P5(x1611,x1612)+P5(x1611,f20(x1613,x1612))), % 0.73/0.83 inference(equality_inference,[],[108])). % 0.73/0.83 cnf(162,plain, % 0.73/0.83 (~P5(x1621,x1622)+P5(x1621,f20(x1622,x1623))), % 0.73/0.83 inference(equality_inference,[],[109])). % 0.73/0.83 cnf(163,plain, % 0.73/0.83 (~P5(x1631,f18(x1632,x1633))+P5(x1631,x1632)), % 0.73/0.83 inference(equality_inference,[],[110])). % 0.73/0.83 cnf(164,plain, % 0.73/0.83 (~P5(x1641,x1642)+~P5(x1641,f18(x1643,x1642))), % 0.73/0.83 inference(equality_inference,[],[117])). % 0.73/0.83 cnf(165,plain, % 0.73/0.83 (~P5(x1651,x1652)+P5(x1651,f18(x1652,x1653))+P5(x1651,x1653)), % 0.73/0.83 inference(equality_inference,[],[119])). % 0.73/0.83 cnf(166,plain, % 0.73/0.83 (~P5(x1661,f20(x1662,x1663))+P5(x1661,x1663)+P5(x1661,x1662)), % 0.73/0.83 inference(equality_inference,[],[120])). % 0.73/0.83 cnf(167,plain, % 0.73/0.83 (~P5(x1671,f18(x1672,f18(x1672,x1673)))+P5(x1671,x1673)), % 0.73/0.83 inference(equality_inference,[],[129])). % 0.73/0.83 cnf(173,plain, % 0.73/0.83 (E(f21(a8,a9),f21(a3,a3))), % 0.73/0.83 inference(scs_inference,[],[54,65,76,159,2])). % 0.73/0.83 cnf(174,plain, % 0.73/0.83 (~P1(f21(x1741,x1741))), % 0.73/0.83 inference(scs_inference,[],[54,65,67,76,159,2,69])). % 0.73/0.83 cnf(176,plain, % 0.73/0.83 (~P3(f21(x1761,x1761),a1)), % 0.73/0.83 inference(scs_inference,[],[54,65,67,76,159,2,69,73])). % 0.73/0.83 cnf(178,plain, % 0.73/0.83 (P5(f10(f21(x1781,x1781)),f21(x1781,x1781))), % 0.73/0.83 inference(scs_inference,[],[54,65,67,76,159,2,69,73,74])). % 0.73/0.83 cnf(180,plain, % 0.73/0.83 (~P5(x1801,f20(a1,a1))), % 0.73/0.83 inference(scs_inference,[],[54,65,53,67,76,159,2,69,73,74,75])). % 0.73/0.83 cnf(181,plain, % 0.73/0.83 (E(f20(x1811,x1811),x1811)), % 0.73/0.83 inference(rename_variables,[],[53])). % 0.73/0.83 cnf(185,plain, % 0.73/0.83 (P3(x1851,f18(x1851,a1))), % 0.73/0.83 inference(scs_inference,[],[54,65,53,46,67,57,76,159,2,69,73,74,75,77,81])). % 0.73/0.83 cnf(195,plain, % 0.73/0.83 (P2(x1951,a2)), % 0.73/0.83 inference(scs_inference,[],[54,65,53,50,46,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103])). % 0.73/0.83 cnf(198,plain, % 0.73/0.83 (~P5(x1981,a1)), % 0.73/0.83 inference(rename_variables,[],[154])). % 0.73/0.83 cnf(200,plain, % 0.73/0.83 (P5(x2001,f21(x2001,x2001))), % 0.73/0.83 inference(scs_inference,[],[54,65,52,154,53,50,46,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122])). % 0.73/0.83 cnf(201,plain, % 0.73/0.83 (P3(x2011,x2011)), % 0.73/0.83 inference(rename_variables,[],[52])). % 0.73/0.83 cnf(209,plain, % 0.73/0.83 (~P5(x2091,f18(a1,x2092))), % 0.73/0.83 inference(scs_inference,[],[54,65,52,154,198,53,50,46,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163])). % 0.73/0.83 cnf(213,plain, % 0.73/0.83 (~P5(x2131,f18(x2132,f18(x2132,a1)))), % 0.73/0.83 inference(scs_inference,[],[54,65,52,154,198,53,50,46,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163,164,167])). % 0.73/0.83 cnf(215,plain, % 0.73/0.83 (P5(f20(a9,a9),f21(a3,a3))), % 0.73/0.83 inference(scs_inference,[],[54,65,52,154,198,53,181,50,46,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163,164,167,88])). % 0.73/0.83 cnf(216,plain, % 0.73/0.83 (E(f20(x2161,x2161),x2161)), % 0.73/0.83 inference(rename_variables,[],[53])). % 0.73/0.83 cnf(219,plain, % 0.73/0.83 (E(f20(x2191,x2191),x2191)), % 0.73/0.83 inference(rename_variables,[],[53])). % 0.73/0.83 cnf(221,plain, % 0.73/0.83 (~P5(f21(x2211,x2211),f21(a1,a1))), % 0.73/0.83 inference(scs_inference,[],[54,65,52,154,198,53,181,216,50,46,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163,164,167,88,89,160])). % 0.73/0.83 cnf(223,plain, % 0.73/0.83 (E(f20(f21(a3,a3),f21(a3,a3)),f21(a8,a9))), % 0.73/0.83 inference(scs_inference,[],[54,65,52,154,198,53,181,216,219,50,46,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163,164,167,88,89,160,3])). % 0.73/0.83 cnf(224,plain, % 0.73/0.83 (E(f20(x2241,x2241),x2241)), % 0.73/0.83 inference(rename_variables,[],[53])). % 0.73/0.83 cnf(226,plain, % 0.73/0.83 (E(f20(x2261,x2261),x2261)), % 0.73/0.83 inference(rename_variables,[],[53])). % 0.73/0.83 cnf(227,plain, % 0.73/0.83 (~E(f10(f21(a8,a8)),a3)), % 0.73/0.83 inference(scs_inference,[],[54,65,52,154,198,53,181,216,219,224,50,46,66,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163,164,167,88,89,160,3,36,37])). % 0.73/0.83 cnf(228,plain, % 0.73/0.83 (~E(f20(x2281,f21(a8,a8)),a1)), % 0.73/0.83 inference(scs_inference,[],[54,65,52,154,198,53,181,216,219,224,50,46,66,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163,164,167,88,89,160,3,36,37,38])). % 0.73/0.83 cnf(229,plain, % 0.73/0.83 (~P5(x2291,a1)), % 0.73/0.83 inference(rename_variables,[],[154])). % 0.73/0.83 cnf(230,plain, % 0.73/0.83 (~E(a1,f21(a8,a8))), % 0.73/0.83 inference(scs_inference,[],[54,65,52,201,154,198,53,181,216,219,224,50,46,66,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163,164,167,88,89,160,3,36,37,38,39])). % 0.73/0.83 cnf(231,plain, % 0.73/0.83 (P3(x2311,x2311)), % 0.73/0.83 inference(rename_variables,[],[52])). % 0.73/0.83 cnf(232,plain, % 0.73/0.83 (~E(f20(f21(a8,a8),x2321),a1)), % 0.73/0.83 inference(scs_inference,[],[54,65,52,201,154,198,53,181,216,219,224,58,50,46,66,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163,164,167,88,89,160,3,36,37,38,39,40])). % 0.73/0.83 cnf(233,plain, % 0.73/0.83 (P3(x2331,f20(x2331,x2332))), % 0.73/0.83 inference(rename_variables,[],[58])). % 0.73/0.83 cnf(240,plain, % 0.73/0.83 (E(f20(x2401,x2401),x2401)), % 0.73/0.83 inference(rename_variables,[],[53])). % 0.73/0.83 cnf(243,plain, % 0.73/0.83 (E(f20(x2431,a1),x2431)), % 0.73/0.83 inference(rename_variables,[],[49])). % 0.73/0.83 cnf(246,plain, % 0.73/0.83 (P3(x2461,f20(x2461,x2462))), % 0.73/0.83 inference(rename_variables,[],[58])). % 0.73/0.83 cnf(248,plain, % 0.73/0.83 (E(f10(f21(a8,a8)),a8)), % 0.73/0.83 inference(scs_inference,[],[54,65,52,201,231,48,154,198,53,181,216,219,224,226,240,58,233,49,50,45,46,66,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163,164,167,88,89,160,3,36,37,38,39,40,70,87,95,96,97,98])). % 0.73/0.83 cnf(249,plain, % 0.73/0.83 (E(f20(x2491,x2491),x2491)), % 0.73/0.83 inference(rename_variables,[],[53])). % 0.73/0.83 cnf(254,plain, % 0.73/0.83 (~P5(x2541,f20(f18(a1,x2542),f18(a1,x2542)))), % 0.73/0.83 inference(scs_inference,[],[54,65,52,201,231,48,154,198,229,53,181,216,219,224,226,240,249,58,233,246,49,50,45,46,66,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163,164,167,88,89,160,3,36,37,38,39,40,70,87,95,96,97,98,105,110])). % 0.73/0.83 cnf(255,plain, % 0.73/0.83 (E(f20(x2551,x2551),x2551)), % 0.73/0.83 inference(rename_variables,[],[53])). % 0.73/0.83 cnf(258,plain, % 0.73/0.83 (~P5(x2581,a1)), % 0.73/0.83 inference(rename_variables,[],[154])). % 0.73/0.83 cnf(264,plain, % 0.73/0.83 (~P5(x2641,a1)), % 0.73/0.83 inference(rename_variables,[],[154])). % 0.73/0.83 cnf(268,plain, % 0.73/0.83 (E(a3,a9)), % 0.73/0.83 inference(scs_inference,[],[54,65,52,201,231,48,154,198,229,258,53,181,216,219,224,226,240,249,58,233,246,49,243,50,45,46,66,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163,164,167,88,89,160,3,36,37,38,39,40,70,87,95,96,97,98,105,110,118,129,165,166,99])). % 0.73/0.83 cnf(270,plain, % 0.73/0.83 (P5(x2701,f19(x2701))), % 0.73/0.83 inference(scs_inference,[],[54,65,52,201,231,48,154,198,229,258,53,181,216,219,224,226,240,249,255,58,233,246,49,243,50,45,46,66,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163,164,167,88,89,160,3,36,37,38,39,40,70,87,95,96,97,98,105,110,118,129,165,166,99,120])). % 0.73/0.83 cnf(276,plain, % 0.73/0.83 (P2(f20(a1,a1),x2761)), % 0.73/0.83 inference(scs_inference,[],[54,65,52,201,231,48,154,198,229,258,264,53,181,216,219,224,226,240,249,255,58,233,246,49,243,50,45,46,66,67,57,76,159,2,69,73,74,75,77,81,82,86,92,102,103,104,122,158,161,162,163,164,167,88,89,160,3,36,37,38,39,40,70,87,95,96,97,98,105,110,118,129,165,166,99,120,141,41])). % 0.73/0.83 cnf(301,plain, % 0.73/0.83 (P3(f18(x3011,f18(x3011,a1)),x3012)), % 0.73/0.83 inference(scs_inference,[],[221,230,268,215,232,213,60,159,73,158,167,76,162,163,86,161,164,102])). % 0.73/0.83 cnf(302,plain, % 0.73/0.83 (~P5(x3021,f18(x3022,f18(x3022,a1)))), % 0.73/0.83 inference(rename_variables,[],[213])). % 0.73/0.83 cnf(305,plain, % 0.73/0.83 (~P5(x3051,f18(x3052,f18(x3052,a1)))), % 0.73/0.83 inference(rename_variables,[],[213])). % 0.73/0.83 cnf(308,plain, % 0.73/0.83 (P3(x3081,f18(x3081,a1))), % 0.73/0.83 inference(rename_variables,[],[185])). % 0.73/0.83 cnf(318,plain, % 0.73/0.83 (~P5(x3181,f18(x3182,f18(x3182,a1)))), % 0.73/0.83 inference(rename_variables,[],[213])). % 0.73/0.83 cnf(321,plain, % 0.73/0.83 (P3(x3211,f18(x3211,a1))), % 0.73/0.83 inference(rename_variables,[],[185])). % 0.73/0.83 cnf(325,plain, % 0.73/0.83 (~P5(x3251,f18(x3252,f18(x3252,a1)))), % 0.73/0.83 inference(rename_variables,[],[213])). % 0.73/0.83 cnf(328,plain, % 0.73/0.83 (E(f20(x3281,a1),x3281)), % 0.73/0.83 inference(rename_variables,[],[49])). % 0.73/0.83 cnf(338,plain, % 0.73/0.83 (P5(f10(f21(a8,a8)),f21(a3,a3))), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,215,232,59,213,302,305,318,254,185,308,248,60,61,49,328,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89])). % 0.73/0.83 cnf(340,plain, % 0.73/0.83 (E(x3401,f18(x3401,a1))), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,215,232,59,213,302,305,318,254,185,308,321,248,60,61,49,328,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97])). % 0.73/0.83 cnf(341,plain, % 0.73/0.83 (P3(x3411,f18(x3411,a1))), % 0.73/0.83 inference(rename_variables,[],[185])). % 0.73/0.83 cnf(342,plain, % 0.73/0.83 (P3(f18(x3421,x3422),x3421)), % 0.73/0.83 inference(rename_variables,[],[59])). % 0.73/0.83 cnf(345,plain, % 0.73/0.83 (P3(f18(x3451,x3452),x3451)), % 0.73/0.83 inference(rename_variables,[],[59])). % 0.73/0.83 cnf(352,plain, % 0.73/0.83 (P5(f20(a9,a9),f18(f21(a3,a3),a1))), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,215,232,59,342,62,213,302,305,318,254,185,308,321,341,248,51,60,61,49,328,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105])). % 0.73/0.83 cnf(355,plain, % 0.73/0.83 (~P1(f21(a8,a9))), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,59,342,62,174,213,302,305,318,254,185,308,321,341,248,51,60,61,49,328,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36])). % 0.73/0.83 cnf(358,plain, % 0.73/0.83 (P5(f10(f21(x3581,x3581)),f21(x3581,x3581))), % 0.73/0.83 inference(rename_variables,[],[178])). % 0.73/0.83 cnf(360,plain, % 0.73/0.83 (~E(f18(a1,x3601),f21(x3602,x3602))), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,59,342,345,62,178,174,213,302,305,318,254,185,308,321,341,176,248,51,60,61,49,328,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36,96,39])). % 0.73/0.83 cnf(361,plain, % 0.73/0.83 (P3(f18(x3611,x3612),x3611)), % 0.73/0.83 inference(rename_variables,[],[59])). % 0.73/0.83 cnf(362,plain, % 0.73/0.83 (~P5(f20(f21(a8,a8),x3621),f21(a1,a1))), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,59,342,345,62,178,174,213,302,305,318,254,185,308,321,341,176,248,51,60,61,49,328,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36,96,39,160])). % 0.73/0.83 cnf(369,plain, % 0.73/0.83 (P2(x3691,f18(a2,a1))), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,227,59,342,345,62,178,200,174,213,302,305,318,254,185,308,321,341,195,176,248,51,60,61,49,328,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36,96,39,160,165,98,42])). % 0.73/0.83 cnf(370,plain, % 0.73/0.83 (E(f18(a3,f18(a3,a3)),a9)), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,227,59,342,345,62,178,200,174,213,302,305,318,254,185,308,321,341,195,176,248,51,60,61,49,328,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36,96,39,160,165,98,42,3])). % 0.73/0.83 cnf(372,plain, % 0.73/0.83 (~E(f10(f21(a1,a1)),f21(x3721,x3721))), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,227,59,342,345,62,178,358,200,174,213,302,305,318,254,185,308,321,341,195,176,248,51,60,61,49,328,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36,96,39,160,165,98,42,3,37])). % 0.73/0.83 cnf(374,plain, % 0.73/0.83 (~E(f21(a3,a3),f18(x3741,f18(x3741,a1)))), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,227,59,342,345,62,178,358,200,174,213,302,305,318,325,254,185,308,321,341,195,176,248,51,60,61,49,328,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36,96,39,160,165,98,42,3,37,38])). % 0.73/0.83 cnf(375,plain, % 0.73/0.83 (~P5(x3751,f18(x3752,f18(x3752,a1)))), % 0.73/0.83 inference(rename_variables,[],[213])). % 0.73/0.83 cnf(377,plain, % 0.73/0.83 (P3(f18(f21(a3,a3),x3771),f21(a8,a9))), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,227,59,342,345,361,62,178,358,200,174,213,302,305,318,325,254,185,308,321,341,195,176,248,51,60,61,49,328,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36,96,39,160,165,98,42,3,37,38,41,40])). % 0.73/0.83 cnf(385,plain, % 0.73/0.83 (E(f20(a9,a9),a3)), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,227,63,59,342,345,361,62,178,358,200,174,213,302,305,318,325,254,185,308,321,341,195,55,176,248,51,60,61,49,328,50,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36,96,39,160,165,98,42,3,37,38,41,40,133,120,99])). % 0.73/0.83 cnf(388,plain, % 0.73/0.83 (E(f14(x3881,x3881,f18(a1,f18(a1,a1))),x3881)), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,227,63,59,342,345,361,62,178,358,200,174,213,302,305,318,325,375,254,185,308,321,341,195,55,176,248,51,60,61,49,328,50,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36,96,39,160,165,98,42,3,37,38,41,40,133,120,99,141])). % 0.73/0.83 cnf(389,plain, % 0.73/0.83 (~P5(x3891,f18(x3892,f18(x3892,a1)))), % 0.73/0.83 inference(rename_variables,[],[213])). % 0.73/0.83 cnf(391,plain, % 0.73/0.83 (~P2(f21(a3,a3),f21(a3,a3))), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,227,63,59,342,345,361,62,178,358,200,174,213,302,305,318,325,375,254,185,308,321,341,195,55,176,248,51,60,61,49,328,50,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36,96,39,160,165,98,42,3,37,38,41,40,133,120,99,141,139])). % 0.73/0.83 cnf(400,plain, % 0.73/0.83 (E(f11(a1,f18(a1,f18(a1,a1))),a1)), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,227,63,59,342,345,361,62,178,358,200,174,213,302,305,318,325,375,389,254,185,308,321,341,195,55,176,248,51,60,61,154,49,328,50,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36,96,39,160,165,98,42,3,37,38,41,40,133,120,99,141,139,75,143,147,118])). % 0.73/0.83 cnf(407,plain, % 0.73/0.83 (~P3(f21(a1,a1),f18(a1,f18(a1,a1)))), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,227,63,59,342,345,361,62,178,358,200,174,213,302,305,318,325,375,389,254,185,308,321,341,195,55,176,248,51,60,61,154,49,328,50,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36,96,39,160,165,98,42,3,37,38,41,40,133,120,99,141,139,75,143,147,118,87,93,94])). % 0.73/0.83 cnf(409,plain, % 0.73/0.83 (~E(f21(a1,a1),f18(a1,f18(a1,a1)))), % 0.73/0.83 inference(scs_inference,[],[54,221,230,268,223,173,215,232,227,63,59,342,345,361,62,68,178,358,200,174,213,302,305,318,325,375,389,254,185,308,321,341,195,55,176,248,51,60,61,154,49,328,50,159,73,158,167,76,162,163,86,161,164,102,103,122,82,2,69,92,104,106,125,117,108,109,166,89,97,95,88,110,105,36,96,39,160,165,98,42,3,37,38,41,40,133,120,99,141,139,75,143,147,118,87,93,94,44])). % 0.73/0.83 cnf(428,plain, % 0.73/0.83 (~P5(x4281,f18(a1,x4282))), % 0.73/0.83 inference(rename_variables,[],[209])). % 0.73/0.83 cnf(439,plain, % 0.73/0.83 (P3(x4391,f20(x4391,x4392))), % 0.73/0.83 inference(rename_variables,[],[58])). % 0.73/0.83 cnf(446,plain, % 0.73/0.83 (~P5(x4461,f18(a1,x4462))), % 0.73/0.83 inference(rename_variables,[],[209])). % 0.73/0.83 cnf(449,plain, % 0.73/0.83 (~P5(x4491,f18(a1,x4492))), % 0.73/0.83 inference(rename_variables,[],[209])). % 0.73/0.83 cnf(454,plain, % 0.73/0.83 (~P5(x4541,f18(a1,x4542))), % 0.73/0.83 inference(rename_variables,[],[209])). % 0.73/0.83 cnf(462,plain, % 0.73/0.83 (P3(x4621,f20(x4621,x4622))), % 0.73/0.83 inference(rename_variables,[],[58])). % 0.73/0.83 cnf(466,plain, % 0.73/0.83 (~P5(x4661,f18(a1,x4662))), % 0.73/0.83 inference(rename_variables,[],[209])). % 0.73/0.83 cnf(472,plain, % 0.73/0.83 (P3(f18(x4721,f18(x4721,a1)),x4722)), % 0.73/0.83 inference(rename_variables,[],[301])). % 0.73/0.83 cnf(473,plain, % 0.73/0.83 (~E(f18(a1,x4731),f21(x4732,x4732))), % 0.73/0.83 inference(rename_variables,[],[360])). % 0.73/0.83 cnf(477,plain, % 0.73/0.83 (~E(f18(a1,x4771),f21(x4772,x4772))), % 0.73/0.83 inference(rename_variables,[],[360])). % 0.73/0.83 cnf(480,plain, % 0.73/0.83 (E(f14(x4801,x4801,f18(a1,f18(a1,a1))),x4801)), % 0.73/0.83 inference(rename_variables,[],[388])). % 0.73/0.83 cnf(484,plain, % 0.73/0.83 (~P5(x4841,f18(a1,x4842))), % 0.73/0.83 inference(rename_variables,[],[209])). % 0.73/0.83 cnf(498,plain, % 0.73/0.83 (P3(x4981,f20(x4981,x4982))), % 0.73/0.83 inference(rename_variables,[],[58])). % 0.73/0.83 cnf(503,plain, % 0.73/0.83 (~P5(x5031,f18(a1,x5032))), % 0.73/0.83 inference(rename_variables,[],[209])). % 0.73/0.83 cnf(518,plain, % 0.73/0.83 ($false), % 0.73/0.83 inference(scs_inference,[],[54,65,228,276,372,362,338,360,473,477,369,374,377,355,385,370,223,227,221,270,58,439,462,498,63,209,428,446,449,454,466,484,503,409,407,352,388,480,301,472,340,180,391,400,68,55,154,73,159,76,158,161,162,102,167,92,164,163,122,82,75,104,103,2,142,144,166,106,125,105,87,97,89,118,44,98,160,88,110,39,165,38,3,41,36,37,42,40,119,99]), % 0.73/0.83 ['proof']). % 0.73/0.83 % SZS output end Proof % 0.73/0.83 % Total time :0.170000s %------------------------------------------------------------------------------