%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU435+1 : TPTP v8.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n018.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:03:10 EDT 2024 % Result : Theorem 0.45s 0.55s % Output : CNFRefutation 0.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : SEU435+1 : TPTP v8.2.0. Released v3.4.0. % 0.00/0.08 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.27 % Computer : n018.cluster.edu % 0.07/0.27 % Model : x86_64 x86_64 % 0.07/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.27 % Memory : 8042.1875MB % 0.07/0.27 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.27 % CPULimit : 300 % 0.07/0.27 % WCLimit : 300 % 0.07/0.27 % DateTime : Fri Jun 21 15:22:38 EDT 2024 % 0.07/0.27 % CPUTime : % 0.12/0.49 start to proof:theBenchmark % 0.12/0.53 %------------------------------------------- % 0.12/0.53 % File :CSE---1.7 % 0.12/0.53 % Problem :theBenchmark % 0.12/0.53 % Transform :cnf % 0.12/0.53 % Format :tptp:raw % 0.12/0.53 % Command :java -jar mcs_scs.jar %d %s % 0.12/0.53 % 0.12/0.53 % Result :Theorem 0.000000s % 0.12/0.53 % Output :CNFRefutation 0.000000s % 0.12/0.53 %------------------------------------------- % 0.45/0.53 %------------------------------------------------------------------------------ % 0.45/0.53 % File : SEU435+1 : TPTP v8.2.0. Released v3.4.0. % 0.45/0.53 % Domain : Set Theory % 0.45/0.53 % Problem : First and Second Order Cutting of Binary Relations T36 % 0.45/0.53 % Version : [Urb08] axioms : Especial. % 0.45/0.54 % English : % 0.45/0.54 % 0.45/0.54 % Refs : [Ret05] Retel (2005), Properties of First and Second Order Cut % 0.45/0.54 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 0.45/0.54 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 0.45/0.54 % Source : [Urb08] % 0.45/0.54 % Names : t36_relset_2 [Urb08] % 0.45/0.54 % 0.45/0.54 % Status : Theorem % 0.45/0.54 % Rating : 0.08 v8.1.0, 0.06 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.1.0, 0.17 v6.0.0, 0.13 v5.5.0, 0.15 v5.4.0, 0.21 v5.3.0, 0.26 v5.2.0, 0.15 v5.1.0, 0.19 v5.0.0, 0.17 v4.1.0, 0.22 v4.0.1, 0.26 v4.0.0, 0.29 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0 % 0.45/0.54 % Syntax : Number of formulae : 51 ( 15 unt; 0 def) % 0.45/0.54 % Number of atoms : 108 ( 8 equ) % 0.45/0.54 % Maximal formula atoms : 6 ( 2 avg) % 0.45/0.54 % Number of connectives : 69 ( 12 ~; 1 |; 26 &) % 0.45/0.54 % ( 4 <=>; 26 =>; 0 <=; 0 <~>) % 0.45/0.54 % Maximal formula depth : 13 ( 4 avg) % 0.45/0.54 % Maximal term depth : 4 ( 1 avg) % 0.45/0.54 % Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty) % 0.45/0.54 % Number of functors : 12 ( 12 usr; 1 con; 0-6 aty) % 0.45/0.54 % Number of variables : 112 ( 101 !; 11 ?) % 0.45/0.54 % SPC : FOF_THM_RFO_SEQ % 0.45/0.54 % 0.45/0.54 % Comments : Normal version: includes the axioms (which may be theorems from % 0.45/0.54 % other articles) and background that are possibly necessary. % 0.45/0.54 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 0.45/0.54 % : The problem encoding is based on set theory. % 0.45/0.54 %------------------------------------------------------------------------------ % 0.45/0.54 fof(t36_relset_2,conjecture, % 0.45/0.54 ! [A,B,C] : % 0.45/0.54 ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(A,B)))) % 0.45/0.54 => ! [D,E,F] : % 0.45/0.54 ( m1_subset_1(F,k1_zfmisc_1(D)) % 0.45/0.54 => m1_subset_1(a_6_0_relset_2(A,B,C,D,E,F),k1_zfmisc_1(k1_zfmisc_1(E))) ) ) ). % 0.45/0.54 % 0.45/0.54 fof(antisymmetry_r2_hidden,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ( r2_hidden(A,B) % 0.45/0.54 => ~ r2_hidden(B,A) ) ). % 0.45/0.54 % 0.45/0.54 fof(cc1_relat_1,axiom, % 0.45/0.54 ! [A] : % 0.45/0.54 ( v1_xboole_0(A) % 0.45/0.54 => v1_relat_1(A) ) ). % 0.45/0.54 % 0.45/0.54 fof(cc1_relset_1,axiom, % 0.45/0.54 ! [A,B,C] : % 0.45/0.54 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 0.45/0.54 => v1_relat_1(C) ) ). % 0.45/0.54 % 0.45/0.54 fof(d4_relset_2,axiom, % 0.45/0.54 ! [A,B,C] : % 0.45/0.54 ( m1_subset_1(C,k1_zfmisc_1(A)) % 0.45/0.54 => ! [D] : % 0.45/0.54 ( m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 0.45/0.54 => k7_relset_2(A,B,C,D) = k8_setfam_1(B,k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,D),k3_pua2mss1(C))) ) ) ). % 0.45/0.54 % 0.45/0.54 fof(dt_k1_xboole_0,axiom, % 0.45/0.54 $true ). % 0.45/0.54 % 0.45/0.54 fof(dt_k1_zfmisc_1,axiom, % 0.45/0.54 $true ). % 0.45/0.54 % 0.45/0.54 fof(dt_k2_zfmisc_1,axiom, % 0.45/0.54 $true ). % 0.45/0.54 % 0.45/0.54 fof(dt_k3_pua2mss1,axiom, % 0.45/0.54 ! [A] : m1_eqrel_1(k3_pua2mss1(A),A) ). % 0.45/0.54 % 0.45/0.54 fof(dt_k4_relset_2,axiom, % 0.45/0.54 ! [A,B,C,D] : % 0.45/0.54 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,k1_zfmisc_1(B)))) % 0.45/0.54 => m1_subset_1(k4_relset_2(A,B,C,D),k1_zfmisc_1(k1_zfmisc_1(B))) ) ). % 0.45/0.54 % 0.45/0.54 fof(dt_k5_relset_2,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ( v1_relat_1(B) % 0.45/0.54 => ( v1_relat_1(k5_relset_2(A,B)) % 0.45/0.54 & v1_funct_1(k5_relset_2(A,B)) ) ) ). % 0.45/0.54 % 0.45/0.54 fof(dt_k6_relset_2,axiom, % 0.45/0.54 ! [A,B,C] : % 0.45/0.54 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(B,A))) % 0.45/0.54 => ( v1_funct_1(k6_relset_2(A,B,C)) % 0.45/0.54 & v1_funct_2(k6_relset_2(A,B,C),k1_zfmisc_1(B),k1_zfmisc_1(A)) % 0.45/0.54 & m2_relset_1(k6_relset_2(A,B,C),k1_zfmisc_1(B),k1_zfmisc_1(A)) ) ) ). % 0.45/0.54 % 0.45/0.54 fof(dt_k7_relset_2,axiom, % 0.45/0.54 $true ). % 0.45/0.54 % 0.45/0.54 fof(dt_k8_relset_2,axiom, % 0.45/0.54 ! [A,B,C,D] : % 0.45/0.54 ( ( m1_subset_1(C,k1_zfmisc_1(A)) % 0.45/0.54 & m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) % 0.45/0.54 => m1_subset_1(k8_relset_2(A,B,C,D),k1_zfmisc_1(B)) ) ). % 0.45/0.54 % 0.45/0.54 fof(dt_k8_setfam_1,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) % 0.45/0.54 => m1_subset_1(k8_setfam_1(A,B),k1_zfmisc_1(A)) ) ). % 0.45/0.54 % 0.45/0.54 fof(dt_k9_relat_1,axiom, % 0.45/0.54 $true ). % 0.45/0.54 % 0.45/0.54 fof(dt_m1_eqrel_1,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ( m1_eqrel_1(B,A) % 0.45/0.54 => m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) ) ). % 0.45/0.54 % 0.45/0.54 fof(dt_m1_relset_1,axiom, % 0.45/0.54 $true ). % 0.45/0.54 % 0.45/0.54 fof(dt_m1_subset_1,axiom, % 0.45/0.54 $true ). % 0.45/0.54 % 0.45/0.54 fof(dt_m2_relset_1,axiom, % 0.45/0.54 ! [A,B,C] : % 0.45/0.54 ( m2_relset_1(C,A,B) % 0.45/0.54 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 0.45/0.54 % 0.45/0.54 fof(existence_m1_eqrel_1,axiom, % 0.45/0.54 ! [A] : % 0.45/0.54 ? [B] : m1_eqrel_1(B,A) ). % 0.45/0.54 % 0.45/0.54 fof(existence_m1_relset_1,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ? [C] : m1_relset_1(C,A,B) ). % 0.45/0.54 % 0.45/0.54 fof(existence_m1_subset_1,axiom, % 0.45/0.54 ! [A] : % 0.45/0.54 ? [B] : m1_subset_1(B,A) ). % 0.45/0.54 % 0.45/0.54 fof(existence_m2_relset_1,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ? [C] : m2_relset_1(C,A,B) ). % 0.45/0.54 % 0.45/0.54 fof(fc12_relat_1,axiom, % 0.45/0.54 ( v1_xboole_0(k1_xboole_0) % 0.45/0.54 & v1_relat_1(k1_xboole_0) % 0.45/0.54 & v3_relat_1(k1_xboole_0) ) ). % 0.45/0.54 % 0.45/0.54 fof(fc1_subset_1,axiom, % 0.45/0.54 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 0.45/0.54 % 0.45/0.54 fof(fc1_sysrel,axiom, % 0.45/0.54 ! [A,B] : v1_relat_1(k2_zfmisc_1(A,B)) ). % 0.45/0.54 % 0.45/0.54 fof(fc4_relat_1,axiom, % 0.45/0.54 ( v1_xboole_0(k1_xboole_0) % 0.45/0.54 & v1_relat_1(k1_xboole_0) ) ). % 0.45/0.54 % 0.45/0.54 fof(fc4_subset_1,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ( ( ~ v1_xboole_0(A) % 0.45/0.54 & ~ v1_xboole_0(B) ) % 0.45/0.54 => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ). % 0.45/0.54 % 0.45/0.54 fof(fraenkel_a_6_0_relset_2,axiom, % 0.45/0.54 ! [A,B,C,D,E,F,G] : % 0.45/0.54 ( ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(B,C)))) % 0.45/0.54 & m1_subset_1(G,k1_zfmisc_1(E)) ) % 0.45/0.54 => ( r2_hidden(A,a_6_0_relset_2(B,C,D,E,F,G)) % 0.45/0.54 <=> ? [H] : % 0.45/0.54 ( m1_subset_1(H,k1_zfmisc_1(k2_zfmisc_1(E,F))) % 0.45/0.54 & A = k8_relset_2(E,F,G,H) % 0.45/0.54 & r2_hidden(H,D) ) ) ) ). % 0.45/0.54 % 0.45/0.54 fof(rc1_relat_1,axiom, % 0.45/0.54 ? [A] : % 0.45/0.54 ( v1_xboole_0(A) % 0.45/0.54 & v1_relat_1(A) ) ). % 0.45/0.54 % 0.45/0.54 fof(rc1_subset_1,axiom, % 0.45/0.54 ! [A] : % 0.45/0.54 ( ~ v1_xboole_0(A) % 0.45/0.54 => ? [B] : % 0.45/0.54 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.45/0.54 & ~ v1_xboole_0(B) ) ) ). % 0.45/0.54 % 0.45/0.54 fof(rc2_partfun1,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ? [C] : % 0.45/0.54 ( m1_relset_1(C,A,B) % 0.45/0.54 & v1_relat_1(C) % 0.45/0.54 & v1_funct_1(C) ) ). % 0.45/0.54 % 0.45/0.54 fof(rc2_relat_1,axiom, % 0.45/0.54 ? [A] : % 0.45/0.54 ( ~ v1_xboole_0(A) % 0.45/0.54 & v1_relat_1(A) ) ). % 0.45/0.54 % 0.45/0.54 fof(rc2_subset_1,axiom, % 0.45/0.54 ! [A] : % 0.45/0.54 ? [B] : % 0.45/0.54 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.45/0.54 & v1_xboole_0(B) ) ). % 0.45/0.54 % 0.45/0.54 fof(rc3_relat_1,axiom, % 0.45/0.54 ? [A] : % 0.45/0.54 ( v1_relat_1(A) % 0.45/0.54 & v3_relat_1(A) ) ). % 0.45/0.54 % 0.45/0.54 fof(redefinition_k4_relset_2,axiom, % 0.45/0.54 ! [A,B,C,D] : % 0.45/0.54 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,k1_zfmisc_1(B)))) % 0.45/0.54 => k4_relset_2(A,B,C,D) = k9_relat_1(C,D) ) ). % 0.45/0.54 % 0.45/0.54 fof(redefinition_k6_relset_2,axiom, % 0.45/0.54 ! [A,B,C] : % 0.45/0.54 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(B,A))) % 0.45/0.54 => k6_relset_2(A,B,C) = k5_relset_2(B,C) ) ). % 0.45/0.54 % 0.45/0.54 fof(redefinition_k8_relset_2,axiom, % 0.45/0.54 ! [A,B,C,D] : % 0.45/0.54 ( ( m1_subset_1(C,k1_zfmisc_1(A)) % 0.45/0.54 & m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) % 0.45/0.54 => k8_relset_2(A,B,C,D) = k7_relset_2(A,B,C,D) ) ). % 0.45/0.54 % 0.45/0.54 fof(redefinition_m2_relset_1,axiom, % 0.45/0.54 ! [A,B,C] : % 0.45/0.54 ( m2_relset_1(C,A,B) % 0.45/0.54 <=> m1_relset_1(C,A,B) ) ). % 0.45/0.54 % 0.45/0.54 fof(reflexivity_r1_tarski,axiom, % 0.45/0.54 ! [A,B] : r1_tarski(A,A) ). % 0.45/0.54 % 0.45/0.54 fof(s8_domain_1__e1_46__relset_2,axiom, % 0.45/0.54 ! [A,B,C,D,E,F] : % 0.45/0.54 ( ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(A,B)))) % 0.45/0.54 & m1_subset_1(F,k1_zfmisc_1(D)) ) % 0.45/0.54 => m1_subset_1(a_6_0_relset_2(A,B,C,D,E,F),k1_zfmisc_1(k1_zfmisc_1(E))) ) ). % 0.45/0.54 % 0.45/0.54 fof(t1_subset,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ( r2_hidden(A,B) % 0.45/0.54 => m1_subset_1(A,B) ) ). % 0.45/0.54 % 0.45/0.54 fof(t2_subset,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ( m1_subset_1(A,B) % 0.45/0.54 => ( v1_xboole_0(B) % 0.45/0.54 | r2_hidden(A,B) ) ) ). % 0.45/0.54 % 0.45/0.54 fof(t2_tarski,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ( ! [C] : % 0.45/0.54 ( r2_hidden(C,A) % 0.45/0.54 <=> r2_hidden(C,B) ) % 0.45/0.54 => A = B ) ). % 0.45/0.54 % 0.45/0.54 fof(t3_subset,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ( m1_subset_1(A,k1_zfmisc_1(B)) % 0.45/0.54 <=> r1_tarski(A,B) ) ). % 0.45/0.54 % 0.45/0.54 fof(t4_subset,axiom, % 0.45/0.54 ! [A,B,C] : % 0.45/0.54 ( ( r2_hidden(A,B) % 0.45/0.54 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 0.45/0.54 => m1_subset_1(A,C) ) ). % 0.45/0.54 % 0.45/0.54 fof(t5_subset,axiom, % 0.45/0.54 ! [A,B,C] : % 0.45/0.54 ~ ( r2_hidden(A,B) % 0.45/0.54 & m1_subset_1(B,k1_zfmisc_1(C)) % 0.45/0.54 & v1_xboole_0(C) ) ). % 0.45/0.54 % 0.45/0.54 fof(t6_boole,axiom, % 0.45/0.54 ! [A] : % 0.45/0.54 ( v1_xboole_0(A) % 0.45/0.54 => A = k1_xboole_0 ) ). % 0.45/0.54 % 0.45/0.54 fof(t7_boole,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ~ ( r2_hidden(A,B) % 0.45/0.54 & v1_xboole_0(B) ) ). % 0.45/0.54 % 0.45/0.54 fof(t8_boole,axiom, % 0.45/0.54 ! [A,B] : % 0.45/0.54 ~ ( v1_xboole_0(A) % 0.45/0.54 & A != B % 0.45/0.54 & v1_xboole_0(B) ) ). % 0.45/0.54 % 0.45/0.54 %------------------------------------------------------------------------------ % 0.45/0.54 %------------------------------------------- % 0.45/0.55 % Proof found % 0.45/0.55 % SZS status Theorem for theBenchmark % 0.45/0.55 % SZS output start Proof % 0.45/0.55 %ClaNum:139(EqnAxiom:74) % 0.45/0.55 %VarNum:319(SingletonVarNum:136) % 0.45/0.55 %MaxLitNum:6 % 0.45/0.55 %MaxfuncDepth:3 % 0.45/0.55 %SharedTerms:29 % 0.45/0.55 %goalClause: 87 98 101 % 0.45/0.55 %singleGoalClaCount:3 % 0.45/0.55 [76]P1(a1) % 0.45/0.55 [77]P1(a2) % 0.45/0.55 [79]P2(a1) % 0.45/0.55 [80]P2(a2) % 0.45/0.55 [81]P2(a6) % 0.45/0.55 [82]P2(a9) % 0.45/0.55 [83]P11(a1) % 0.45/0.55 [84]P11(a9) % 0.45/0.55 [99]~P1(a6) % 0.45/0.55 [87]P4(a11,f21(a12)) % 0.45/0.55 [101]~P4(f4(a14,a16,a13,a12,a17,a11),f21(f21(a17))) % 0.45/0.55 [98]P4(a13,f21(f21(f23(a14,a16)))) % 0.45/0.55 [86]P3(x861,x861) % 0.45/0.55 [85]P1(f10(x851)) % 0.45/0.55 [88]P4(f18(x881),x881) % 0.45/0.55 [89]P5(f22(x891),x891) % 0.45/0.55 [90]P5(f19(x901),x901) % 0.45/0.55 [91]P4(f10(x911),f21(x911)) % 0.45/0.55 [100]~P1(f21(x1001)) % 0.45/0.55 [92]P2(f23(x921,x922)) % 0.45/0.55 [93]P2(f7(x931,x932)) % 0.45/0.55 [94]P8(f7(x941,x942)) % 0.45/0.55 [95]P7(f3(x951,x952),x951,x952) % 0.45/0.55 [96]P6(f20(x961,x962),x961,x962) % 0.45/0.55 [97]P6(f7(x971,x972),x971,x972) % 0.45/0.55 [102]~P1(x1021)+E(x1021,a1) % 0.45/0.55 [103]~P1(x1031)+P2(x1031) % 0.45/0.55 [105]P1(x1051)+~P1(f8(x1051)) % 0.45/0.55 [107]P1(x1071)+P4(f8(x1071),f21(x1071)) % 0.45/0.55 [106]~P1(x1061)+~P9(x1062,x1061) % 0.45/0.55 [108]~P9(x1081,x1082)+P4(x1081,x1082) % 0.45/0.55 [113]~P9(x1132,x1131)+~P9(x1131,x1132) % 0.45/0.55 [109]~P2(x1092)+P2(f24(x1091,x1092)) % 0.45/0.55 [110]~P2(x1102)+P8(f24(x1101,x1102)) % 0.45/0.55 [112]~P3(x1121,x1122)+P4(x1121,f21(x1122)) % 0.45/0.55 [114]P3(x1141,x1142)+~P4(x1141,f21(x1142)) % 0.45/0.55 [115]~P5(x1151,x1152)+P4(x1151,f21(f21(x1152))) % 0.45/0.55 [120]P4(f26(x1201,x1202),f21(x1201))+~P4(x1202,f21(f21(x1201))) % 0.45/0.55 [123]~P6(x1231,x1232,x1233)+P7(x1231,x1232,x1233) % 0.45/0.55 [124]~P7(x1241,x1242,x1243)+P6(x1241,x1242,x1243) % 0.45/0.55 [121]P2(x1211)+~P4(x1211,f21(f23(x1212,x1213))) % 0.45/0.55 [125]~P7(x1251,x1252,x1253)+P4(x1251,f21(f23(x1252,x1253))) % 0.45/0.55 [126]E(f27(x1261,x1262,x1263),f24(x1262,x1263))+~P4(x1263,f21(f23(x1262,x1261))) % 0.45/0.55 [127]~P4(x1273,f21(f23(x1272,x1271)))+P8(f27(x1271,x1272,x1273)) % 0.45/0.55 [128]P10(f27(x1281,x1282,x1283),f21(x1282),f21(x1281))+~P4(x1283,f21(f23(x1282,x1281))) % 0.45/0.55 [129]P7(f27(x1291,x1292,x1293),f21(x1292),f21(x1291))+~P4(x1293,f21(f23(x1292,x1291))) % 0.45/0.55 [130]E(f25(x1301,x1302,x1303,x1304),f30(x1303,x1304))+~P4(x1303,f21(f23(x1301,f21(x1302)))) % 0.45/0.55 [133]P4(f25(x1331,x1332,x1333,x1334),f21(f21(x1332)))+~P4(x1333,f21(f23(x1331,f21(x1332)))) % 0.45/0.55 [104]~P1(x1042)+~P1(x1041)+E(x1041,x1042) % 0.45/0.55 [111]~P4(x1112,x1111)+P1(x1111)+P9(x1112,x1111) % 0.45/0.55 [116]P1(x1161)+P1(x1162)+~P1(f23(x1162,x1161)) % 0.45/0.55 [119]E(x1191,x1192)+P9(f15(x1191,x1192),x1192)+P9(f15(x1191,x1192),x1191) % 0.45/0.55 [122]E(x1221,x1222)+~P9(f15(x1221,x1222),x1222)+~P9(f15(x1221,x1222),x1221) % 0.45/0.55 [117]~P1(x1171)+~P9(x1172,x1173)+~P4(x1173,f21(x1171)) % 0.45/0.55 [118]P4(x1181,x1182)+~P9(x1181,x1183)+~P4(x1183,f21(x1182)) % 0.45/0.55 [131]~P4(x1313,f21(x1311))+E(f28(x1311,x1312,x1313,x1314),f29(x1311,x1312,x1313,x1314))+~P4(x1314,f21(f23(x1311,x1312))) % 0.45/0.55 [132]~P4(x1323,f21(x1321))+P4(f29(x1321,x1322,x1323,x1324),f21(x1322))+~P4(x1324,f21(f23(x1321,x1322))) % 0.45/0.55 [134]~P4(x1344,f21(x1342))+~P4(x1343,f21(f23(x1342,x1341)))+E(f26(x1341,f25(f21(x1342),x1341,f27(x1341,x1342,x1343),f22(x1344))),f28(x1342,x1341,x1344,x1343)) % 0.45/0.55 [135]~P4(x1356,f21(x1354))+P4(f4(x1351,x1352,x1353,x1354,x1355,x1356),f21(f21(x1355)))+~P4(x1353,f21(f21(f23(x1351,x1352)))) % 0.45/0.55 [137]~P4(x1377,f21(x1375))+~P9(x1371,f4(x1372,x1373,x1374,x1375,x1376,x1377))+P9(f5(x1371,x1372,x1373,x1374,x1375,x1376,x1377),x1374)+~P4(x1374,f21(f21(f23(x1372,x1373)))) % 0.45/0.55 [138]~P4(x1387,f21(x1385))+~P9(x1381,f4(x1382,x1383,x1384,x1385,x1386,x1387))+P4(f5(x1381,x1382,x1383,x1384,x1385,x1386,x1387),f21(f23(x1385,x1386)))+~P4(x1384,f21(f21(f23(x1382,x1383)))) % 0.45/0.55 [139]~P4(x1393,f21(x1391))+~P9(x1394,f4(x1395,x1396,x1397,x1391,x1392,x1393))+E(f29(x1391,x1392,x1393,f5(x1394,x1395,x1396,x1397,x1391,x1392,x1393)),x1394)+~P4(x1397,f21(f21(f23(x1395,x1396)))) % 0.45/0.55 [136]~P9(x1368,x1364)+~P4(x1367,f21(x1365))+P9(x1361,f4(x1362,x1363,x1364,x1365,x1366,x1367))+~E(x1361,f29(x1365,x1366,x1367,x1368))+~P4(x1368,f21(f23(x1365,x1366)))+~P4(x1364,f21(f21(f23(x1362,x1363)))) % 0.45/0.55 %EqnAxiom % 0.45/0.55 [1]E(x11,x11) % 0.45/0.55 [2]E(x22,x21)+~E(x21,x22) % 0.45/0.55 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.45/0.55 [4]~E(x41,x42)+E(f10(x41),f10(x42)) % 0.45/0.55 [5]~E(x51,x52)+E(f21(x51),f21(x52)) % 0.45/0.55 [6]~E(x61,x62)+E(f18(x61),f18(x62)) % 0.45/0.55 [7]~E(x71,x72)+E(f22(x71),f22(x72)) % 0.45/0.55 [8]~E(x81,x82)+E(f19(x81),f19(x82)) % 0.45/0.55 [9]~E(x91,x92)+E(f4(x91,x93,x94,x95,x96,x97),f4(x92,x93,x94,x95,x96,x97)) % 0.45/0.55 [10]~E(x101,x102)+E(f4(x103,x101,x104,x105,x106,x107),f4(x103,x102,x104,x105,x106,x107)) % 0.45/0.55 [11]~E(x111,x112)+E(f4(x113,x114,x111,x115,x116,x117),f4(x113,x114,x112,x115,x116,x117)) % 0.45/0.55 [12]~E(x121,x122)+E(f4(x123,x124,x125,x121,x126,x127),f4(x123,x124,x125,x122,x126,x127)) % 0.45/0.55 [13]~E(x131,x132)+E(f4(x133,x134,x135,x136,x131,x137),f4(x133,x134,x135,x136,x132,x137)) % 0.45/0.55 [14]~E(x141,x142)+E(f4(x143,x144,x145,x146,x147,x141),f4(x143,x144,x145,x146,x147,x142)) % 0.45/0.55 [15]~E(x151,x152)+E(f23(x151,x153),f23(x152,x153)) % 0.45/0.55 [16]~E(x161,x162)+E(f23(x163,x161),f23(x163,x162)) % 0.45/0.55 [17]~E(x171,x172)+E(f29(x171,x173,x174,x175),f29(x172,x173,x174,x175)) % 0.45/0.55 [18]~E(x181,x182)+E(f29(x183,x181,x184,x185),f29(x183,x182,x184,x185)) % 0.45/0.55 [19]~E(x191,x192)+E(f29(x193,x194,x191,x195),f29(x193,x194,x192,x195)) % 0.45/0.55 [20]~E(x201,x202)+E(f29(x203,x204,x205,x201),f29(x203,x204,x205,x202)) % 0.45/0.55 [21]~E(x211,x212)+E(f7(x211,x213),f7(x212,x213)) % 0.45/0.55 [22]~E(x221,x222)+E(f7(x223,x221),f7(x223,x222)) % 0.45/0.55 [23]~E(x231,x232)+E(f25(x231,x233,x234,x235),f25(x232,x233,x234,x235)) % 0.45/0.55 [24]~E(x241,x242)+E(f25(x243,x241,x244,x245),f25(x243,x242,x244,x245)) % 0.45/0.55 [25]~E(x251,x252)+E(f25(x253,x254,x251,x255),f25(x253,x254,x252,x255)) % 0.45/0.55 [26]~E(x261,x262)+E(f25(x263,x264,x265,x261),f25(x263,x264,x265,x262)) % 0.45/0.55 [27]~E(x271,x272)+E(f3(x271,x273),f3(x272,x273)) % 0.45/0.55 [28]~E(x281,x282)+E(f3(x283,x281),f3(x283,x282)) % 0.45/0.55 [29]~E(x291,x292)+E(f20(x291,x293),f20(x292,x293)) % 0.45/0.55 [30]~E(x301,x302)+E(f20(x303,x301),f20(x303,x302)) % 0.45/0.55 [31]~E(x311,x312)+E(f27(x311,x313,x314),f27(x312,x313,x314)) % 0.45/0.55 [32]~E(x321,x322)+E(f27(x323,x321,x324),f27(x323,x322,x324)) % 0.45/0.55 [33]~E(x331,x332)+E(f27(x333,x334,x331),f27(x333,x334,x332)) % 0.45/0.55 [34]~E(x341,x342)+E(f30(x341,x343),f30(x342,x343)) % 0.45/0.55 [35]~E(x351,x352)+E(f30(x353,x351),f30(x353,x352)) % 0.45/0.55 [36]~E(x361,x362)+E(f15(x361,x363),f15(x362,x363)) % 0.45/0.55 [37]~E(x371,x372)+E(f15(x373,x371),f15(x373,x372)) % 0.45/0.55 [38]~E(x381,x382)+E(f5(x381,x383,x384,x385,x386,x387,x388),f5(x382,x383,x384,x385,x386,x387,x388)) % 0.45/0.55 [39]~E(x391,x392)+E(f5(x393,x391,x394,x395,x396,x397,x398),f5(x393,x392,x394,x395,x396,x397,x398)) % 0.45/0.55 [40]~E(x401,x402)+E(f5(x403,x404,x401,x405,x406,x407,x408),f5(x403,x404,x402,x405,x406,x407,x408)) % 0.45/0.55 [41]~E(x411,x412)+E(f5(x413,x414,x415,x411,x416,x417,x418),f5(x413,x414,x415,x412,x416,x417,x418)) % 0.45/0.55 [42]~E(x421,x422)+E(f5(x423,x424,x425,x426,x421,x427,x428),f5(x423,x424,x425,x426,x422,x427,x428)) % 0.45/0.55 [43]~E(x431,x432)+E(f5(x433,x434,x435,x436,x437,x431,x438),f5(x433,x434,x435,x436,x437,x432,x438)) % 0.45/0.55 [44]~E(x441,x442)+E(f5(x443,x444,x445,x446,x447,x448,x441),f5(x443,x444,x445,x446,x447,x448,x442)) % 0.45/0.55 [45]~E(x451,x452)+E(f26(x451,x453),f26(x452,x453)) % 0.45/0.55 [46]~E(x461,x462)+E(f26(x463,x461),f26(x463,x462)) % 0.45/0.55 [47]~E(x471,x472)+E(f24(x471,x473),f24(x472,x473)) % 0.45/0.55 [48]~E(x481,x482)+E(f24(x483,x481),f24(x483,x482)) % 0.45/0.55 [49]~E(x491,x492)+E(f28(x491,x493,x494,x495),f28(x492,x493,x494,x495)) % 0.45/0.55 [50]~E(x501,x502)+E(f28(x503,x501,x504,x505),f28(x503,x502,x504,x505)) % 0.45/0.55 [51]~E(x511,x512)+E(f28(x513,x514,x511,x515),f28(x513,x514,x512,x515)) % 0.45/0.55 [52]~E(x521,x522)+E(f28(x523,x524,x525,x521),f28(x523,x524,x525,x522)) % 0.45/0.55 [53]~E(x531,x532)+E(f8(x531),f8(x532)) % 0.45/0.55 [54]~P1(x541)+P1(x542)+~E(x541,x542) % 0.45/0.55 [55]P9(x552,x553)+~E(x551,x552)+~P9(x551,x553) % 0.45/0.55 [56]P9(x563,x562)+~E(x561,x562)+~P9(x563,x561) % 0.45/0.55 [57]P4(x572,x573)+~E(x571,x572)+~P4(x571,x573) % 0.45/0.55 [58]P4(x583,x582)+~E(x581,x582)+~P4(x583,x581) % 0.45/0.55 [59]~P2(x591)+P2(x592)+~E(x591,x592) % 0.45/0.55 [60]~P8(x601)+P8(x602)+~E(x601,x602) % 0.45/0.55 [61]P3(x612,x613)+~E(x611,x612)+~P3(x611,x613) % 0.45/0.55 [62]P3(x623,x622)+~E(x621,x622)+~P3(x623,x621) % 0.45/0.55 [63]P6(x632,x633,x634)+~E(x631,x632)+~P6(x631,x633,x634) % 0.45/0.55 [64]P6(x643,x642,x644)+~E(x641,x642)+~P6(x643,x641,x644) % 0.45/0.55 [65]P6(x653,x654,x652)+~E(x651,x652)+~P6(x653,x654,x651) % 0.45/0.55 [66]P5(x662,x663)+~E(x661,x662)+~P5(x661,x663) % 0.45/0.55 [67]P5(x673,x672)+~E(x671,x672)+~P5(x673,x671) % 0.45/0.55 [68]~P11(x681)+P11(x682)+~E(x681,x682) % 0.45/0.55 [69]P10(x692,x693,x694)+~E(x691,x692)+~P10(x691,x693,x694) % 0.45/0.55 [70]P10(x703,x702,x704)+~E(x701,x702)+~P10(x703,x701,x704) % 0.45/0.55 [71]P10(x713,x714,x712)+~E(x711,x712)+~P10(x713,x714,x711) % 0.45/0.55 [72]P7(x722,x723,x724)+~E(x721,x722)+~P7(x721,x723,x724) % 0.45/0.55 [73]P7(x733,x732,x734)+~E(x731,x732)+~P7(x733,x731,x734) % 0.45/0.55 [74]P7(x743,x744,x742)+~E(x741,x742)+~P7(x743,x744,x741) % 0.45/0.55 % 0.45/0.55 %------------------------------------------- % 0.45/0.55 cnf(141,plain, % 0.45/0.55 ($false), % 0.45/0.55 inference(scs_inference,[],[87,101,98,135]), % 0.45/0.55 ['proof']). % 0.45/0.55 % SZS output end Proof % 0.45/0.55 % Total time :0.000000s %------------------------------------------------------------------------------