%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU424+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:01 EDT 2024 % Result : Theorem 0.55s 0.63s % Output : CNFRefutation 0.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SEU424+1 : TPTP v8.2.0. Released v3.4.0. % 0.04/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n018.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Fri Jun 21 18:06:09 EDT 2024 % 0.13/0.33 % CPUTime : % 0.52/0.58 start to proof:theBenchmark % 0.55/0.62 %------------------------------------------- % 0.55/0.62 % File :CSE---1.7 % 0.55/0.62 % Problem :theBenchmark % 0.55/0.62 % Transform :cnf % 0.55/0.62 % Format :tptp:raw % 0.55/0.62 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.62 % 0.55/0.62 % Result :Theorem 0.000000s % 0.55/0.62 % Output :CNFRefutation 0.000000s % 0.55/0.62 %------------------------------------------- % 0.55/0.62 %------------------------------------------------------------------------------ % 0.55/0.62 % File : SEU424+1 : TPTP v8.2.0. Released v3.4.0. % 0.55/0.62 % Domain : Set Theory % 0.55/0.62 % Problem : First and Second Order Cutting of Binary Relations T18 % 0.55/0.62 % Version : [Urb08] axioms : Especial. % 0.55/0.62 % English : % 0.55/0.62 % 0.55/0.62 % Refs : [Ret05] Retel (2005), Properties of First and Second Order Cut % 0.55/0.62 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 0.55/0.62 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 0.55/0.62 % Source : [Urb08] % 0.55/0.62 % Names : t18_relset_2 [Urb08] % 0.55/0.62 % 0.55/0.62 % Status : Theorem % 0.55/0.62 % Rating : 0.11 v8.1.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.1.0, 0.13 v5.5.0, 0.11 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.10 v5.1.0, 0.14 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.55/0.62 % Syntax : Number of formulae : 43 ( 14 unt; 0 def) % 0.55/0.62 % Number of atoms : 91 ( 6 equ) % 0.55/0.62 % Maximal formula atoms : 7 ( 2 avg) % 0.55/0.62 % Number of connectives : 64 ( 16 ~; 1 |; 22 &) % 0.55/0.62 % ( 4 <=>; 21 =>; 0 <=; 0 <~>) % 0.55/0.62 % Maximal formula depth : 11 ( 4 avg) % 0.55/0.62 % Maximal term depth : 3 ( 1 avg) % 0.55/0.62 % Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty) % 0.55/0.62 % Number of functors : 8 ( 8 usr; 1 con; 0-4 aty) % 0.55/0.62 % Number of variables : 85 ( 76 !; 9 ?) % 0.55/0.62 % SPC : FOF_THM_RFO_SEQ % 0.55/0.62 % 0.55/0.62 % Comments : Normal version: includes the axioms (which may be theorems from % 0.55/0.62 % other articles) and background that are possibly necessary. % 0.55/0.62 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 0.55/0.62 % : The problem encoding is based on set theory. % 0.55/0.62 %------------------------------------------------------------------------------ % 0.55/0.62 fof(t18_relset_2,conjecture, % 0.55/0.62 ! [A] : % 0.55/0.62 ( ~ v1_xboole_0(A) % 0.55/0.62 => ! [B,C] : % 0.55/0.62 ( m1_subset_1(C,k1_zfmisc_1(A)) % 0.55/0.62 => ! [D] : % 0.55/0.62 ( m2_relset_1(D,A,B) % 0.55/0.62 => m1_subset_1(a_4_0_relset_2(A,B,C,D),k1_zfmisc_1(k1_zfmisc_1(B))) ) ) ) ). % 0.55/0.62 % 0.55/0.62 fof(antisymmetry_r2_hidden,axiom, % 0.55/0.62 ! [A,B] : % 0.55/0.62 ( r2_hidden(A,B) % 0.55/0.62 => ~ r2_hidden(B,A) ) ). % 0.55/0.62 % 0.55/0.62 fof(cc1_relat_1,axiom, % 0.55/0.62 ! [A] : % 0.55/0.62 ( v1_xboole_0(A) % 0.55/0.62 => v1_relat_1(A) ) ). % 0.55/0.62 % 0.55/0.62 fof(cc1_relset_1,axiom, % 0.55/0.62 ! [A,B,C] : % 0.55/0.62 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 0.55/0.62 => v1_relat_1(C) ) ). % 0.55/0.62 % 0.55/0.62 fof(d1_relset_2,axiom, % 0.55/0.62 ! [A,B,C] : % 0.55/0.62 ( m2_relset_1(C,A,B) % 0.55/0.62 => ! [D] : % 0.55/0.62 ( m1_subset_1(D,A) % 0.55/0.62 => k2_relset_2(A,B,C,D) = k10_relset_1(A,B,C,k1_tarski(D)) ) ) ). % 0.55/0.62 % 0.55/0.62 fof(dt_k10_relset_1,axiom, % 0.55/0.62 ! [A,B,C,D] : % 0.55/0.62 ( m1_relset_1(C,A,B) % 0.55/0.62 => m1_subset_1(k10_relset_1(A,B,C,D),k1_zfmisc_1(B)) ) ). % 0.55/0.62 % 0.55/0.62 fof(dt_k1_tarski,axiom, % 0.55/0.62 $true ). % 0.55/0.62 % 0.55/0.62 fof(dt_k1_xboole_0,axiom, % 0.55/0.62 $true ). % 0.55/0.62 % 0.55/0.62 fof(dt_k1_zfmisc_1,axiom, % 0.55/0.62 $true ). % 0.55/0.62 % 0.55/0.62 fof(dt_k2_relset_2,axiom, % 0.55/0.62 ! [A,B,C,D] : % 0.55/0.62 ( ( m1_relset_1(C,A,B) % 0.55/0.62 & m1_subset_1(D,A) ) % 0.55/0.62 => m1_subset_1(k2_relset_2(A,B,C,D),k1_zfmisc_1(B)) ) ). % 0.55/0.62 % 0.55/0.62 fof(dt_k2_zfmisc_1,axiom, % 0.55/0.62 $true ). % 0.55/0.62 % 0.55/0.62 fof(dt_k9_relat_1,axiom, % 0.55/0.62 $true ). % 0.55/0.62 % 0.55/0.62 fof(dt_m1_relset_1,axiom, % 0.55/0.62 $true ). % 0.55/0.62 % 0.55/0.62 fof(dt_m1_subset_1,axiom, % 0.55/0.62 $true ). % 0.55/0.62 % 0.55/0.62 fof(dt_m2_relset_1,axiom, % 0.55/0.62 ! [A,B,C] : % 0.55/0.62 ( m2_relset_1(C,A,B) % 0.55/0.62 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 0.55/0.62 % 0.55/0.62 fof(existence_m1_relset_1,axiom, % 0.55/0.62 ! [A,B] : % 0.55/0.62 ? [C] : m1_relset_1(C,A,B) ). % 0.55/0.62 % 0.55/0.62 fof(existence_m1_subset_1,axiom, % 0.55/0.62 ! [A] : % 0.55/0.62 ? [B] : m1_subset_1(B,A) ). % 0.55/0.62 % 0.55/0.62 fof(existence_m2_relset_1,axiom, % 0.55/0.62 ! [A,B] : % 0.55/0.62 ? [C] : m2_relset_1(C,A,B) ). % 0.55/0.62 % 0.55/0.62 fof(fc12_relat_1,axiom, % 0.55/0.62 ( v1_xboole_0(k1_xboole_0) % 0.55/0.62 & v1_relat_1(k1_xboole_0) % 0.55/0.62 & v3_relat_1(k1_xboole_0) ) ). % 0.55/0.62 % 0.55/0.62 fof(fc1_subset_1,axiom, % 0.55/0.62 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 0.55/0.62 % 0.55/0.62 fof(fc1_sysrel,axiom, % 0.55/0.62 ! [A,B] : v1_relat_1(k2_zfmisc_1(A,B)) ). % 0.55/0.62 % 0.55/0.62 fof(fc2_subset_1,axiom, % 0.55/0.62 ! [A] : ~ v1_xboole_0(k1_tarski(A)) ). % 0.55/0.62 % 0.55/0.62 fof(fc4_relat_1,axiom, % 0.55/0.62 ( v1_xboole_0(k1_xboole_0) % 0.55/0.62 & v1_relat_1(k1_xboole_0) ) ). % 0.55/0.62 % 0.55/0.63 fof(fc4_subset_1,axiom, % 0.55/0.63 ! [A,B] : % 0.55/0.63 ( ( ~ v1_xboole_0(A) % 0.55/0.63 & ~ v1_xboole_0(B) ) % 0.55/0.63 => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ). % 0.55/0.63 % 0.55/0.63 fof(fraenkel_a_4_0_relset_2,axiom, % 0.55/0.63 ! [A,B,C,D,E] : % 0.55/0.63 ( ( ~ v1_xboole_0(B) % 0.55/0.63 & m1_subset_1(D,k1_zfmisc_1(B)) % 0.55/0.63 & m2_relset_1(E,B,C) ) % 0.55/0.63 => ( r2_hidden(A,a_4_0_relset_2(B,C,D,E)) % 0.55/0.63 <=> ? [F] : % 0.55/0.63 ( m1_subset_1(F,B) % 0.55/0.63 & A = k2_relset_2(B,C,E,F) % 0.55/0.63 & r2_hidden(F,D) ) ) ) ). % 0.55/0.63 % 0.55/0.63 fof(rc1_relat_1,axiom, % 0.55/0.63 ? [A] : % 0.55/0.63 ( v1_xboole_0(A) % 0.55/0.63 & v1_relat_1(A) ) ). % 0.55/0.63 % 0.55/0.63 fof(rc1_subset_1,axiom, % 0.55/0.63 ! [A] : % 0.55/0.63 ( ~ v1_xboole_0(A) % 0.55/0.63 => ? [B] : % 0.55/0.63 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.55/0.63 & ~ v1_xboole_0(B) ) ) ). % 0.55/0.63 % 0.55/0.63 fof(rc2_relat_1,axiom, % 0.55/0.63 ? [A] : % 0.55/0.63 ( ~ v1_xboole_0(A) % 0.55/0.63 & v1_relat_1(A) ) ). % 0.55/0.63 % 0.55/0.63 fof(rc2_subset_1,axiom, % 0.55/0.63 ! [A] : % 0.55/0.63 ? [B] : % 0.55/0.63 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.55/0.63 & v1_xboole_0(B) ) ). % 0.55/0.63 % 0.55/0.63 fof(rc3_relat_1,axiom, % 0.55/0.63 ? [A] : % 0.55/0.63 ( v1_relat_1(A) % 0.55/0.63 & v3_relat_1(A) ) ). % 0.55/0.63 % 0.55/0.63 fof(redefinition_k10_relset_1,axiom, % 0.55/0.63 ! [A,B,C,D] : % 0.55/0.63 ( m1_relset_1(C,A,B) % 0.55/0.63 => k10_relset_1(A,B,C,D) = k9_relat_1(C,D) ) ). % 0.55/0.63 % 0.55/0.63 fof(redefinition_m2_relset_1,axiom, % 0.55/0.63 ! [A,B,C] : % 0.55/0.63 ( m2_relset_1(C,A,B) % 0.55/0.63 <=> m1_relset_1(C,A,B) ) ). % 0.55/0.63 % 0.55/0.63 fof(reflexivity_r1_tarski,axiom, % 0.55/0.63 ! [A,B] : r1_tarski(A,A) ). % 0.55/0.63 % 0.55/0.63 fof(s8_domain_1__e1_22__relset_2,axiom, % 0.55/0.63 ! [A,B,C,D] : % 0.55/0.63 ( ( ~ v1_xboole_0(A) % 0.55/0.63 & m1_subset_1(C,k1_zfmisc_1(A)) % 0.55/0.63 & m2_relset_1(D,A,B) ) % 0.55/0.63 => m1_subset_1(a_4_0_relset_2(A,B,C,D),k1_zfmisc_1(k1_zfmisc_1(B))) ) ). % 0.55/0.63 % 0.55/0.63 fof(t1_subset,axiom, % 0.55/0.63 ! [A,B] : % 0.55/0.63 ( r2_hidden(A,B) % 0.55/0.63 => m1_subset_1(A,B) ) ). % 0.55/0.63 % 0.55/0.63 fof(t2_subset,axiom, % 0.55/0.63 ! [A,B] : % 0.55/0.63 ( m1_subset_1(A,B) % 0.55/0.63 => ( v1_xboole_0(B) % 0.55/0.63 | r2_hidden(A,B) ) ) ). % 0.55/0.63 % 0.55/0.63 fof(t2_tarski,axiom, % 0.55/0.63 ! [A,B] : % 0.55/0.63 ( ! [C] : % 0.55/0.63 ( r2_hidden(C,A) % 0.55/0.63 <=> r2_hidden(C,B) ) % 0.55/0.63 => A = B ) ). % 0.55/0.63 % 0.55/0.63 fof(t3_subset,axiom, % 0.55/0.63 ! [A,B] : % 0.55/0.63 ( m1_subset_1(A,k1_zfmisc_1(B)) % 0.55/0.63 <=> r1_tarski(A,B) ) ). % 0.55/0.63 % 0.55/0.63 fof(t4_subset,axiom, % 0.55/0.63 ! [A,B,C] : % 0.55/0.63 ( ( r2_hidden(A,B) % 0.55/0.63 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 0.55/0.63 => m1_subset_1(A,C) ) ). % 0.55/0.63 % 0.55/0.63 fof(t5_subset,axiom, % 0.55/0.63 ! [A,B,C] : % 0.55/0.63 ~ ( r2_hidden(A,B) % 0.55/0.63 & m1_subset_1(B,k1_zfmisc_1(C)) % 0.55/0.63 & v1_xboole_0(C) ) ). % 0.55/0.63 % 0.55/0.63 fof(t6_boole,axiom, % 0.55/0.63 ! [A] : % 0.55/0.63 ( v1_xboole_0(A) % 0.55/0.63 => A = k1_xboole_0 ) ). % 0.55/0.63 % 0.55/0.63 fof(t7_boole,axiom, % 0.55/0.63 ! [A,B] : % 0.55/0.63 ~ ( r2_hidden(A,B) % 0.55/0.63 & v1_xboole_0(B) ) ). % 0.55/0.63 % 0.55/0.63 fof(t8_boole,axiom, % 0.55/0.63 ! [A,B] : % 0.55/0.63 ~ ( v1_xboole_0(A) % 0.55/0.63 & A != B % 0.55/0.63 & v1_xboole_0(B) ) ). % 0.55/0.63 % 0.55/0.63 %------------------------------------------------------------------------------ % 0.55/0.63 %------------------------------------------- % 0.55/0.63 % Proof found % 0.55/0.63 % SZS status Theorem for theBenchmark % 0.55/0.63 % SZS output start Proof % 0.55/0.63 %ClaNum:103(EqnAxiom:50) % 0.55/0.63 %VarNum:234(SingletonVarNum:95) % 0.55/0.63 %MaxLitNum:7 % 0.55/0.63 %MaxfuncDepth:2 % 0.55/0.63 %SharedTerms:25 % 0.55/0.63 %goalClause: 63 67 70 74 % 0.55/0.63 %singleGoalClaCount:4 % 0.55/0.63 [52]P1(a1) % 0.55/0.63 [53]P1(a2) % 0.55/0.63 [55]P2(a1) % 0.55/0.63 [56]P2(a2) % 0.55/0.63 [57]P2(a3) % 0.55/0.63 [58]P2(a6) % 0.55/0.63 [59]P8(a1) % 0.55/0.63 [60]P8(a6) % 0.55/0.63 [67]P6(a13,a9,a11) % 0.55/0.63 [70]~P1(a9) % 0.55/0.63 [71]~P1(a3) % 0.55/0.63 [63]P4(a8,f19(a9)) % 0.55/0.63 [74]~P4(f4(a9,a11,a8,a13),f19(f19(a11))) % 0.55/0.63 [62]P3(x621,x621) % 0.55/0.63 [61]P1(f7(x611)) % 0.55/0.63 [64]P4(f12(x641),x641) % 0.55/0.63 [65]P4(f7(x651),f19(x651)) % 0.55/0.63 [72]~P1(f19(x721)) % 0.55/0.63 [73]~P1(f17(x731)) % 0.55/0.63 [66]P2(f20(x661,x662)) % 0.55/0.63 [68]P6(f15(x681,x682),x681,x682) % 0.55/0.63 [69]P5(f14(x691,x692),x691,x692) % 0.55/0.63 [75]~P1(x751)+E(x751,a1) % 0.55/0.63 [76]~P1(x761)+P2(x761) % 0.55/0.63 [78]P1(x781)+~P1(f5(x781)) % 0.55/0.63 [80]P1(x801)+P4(f5(x801),f19(x801)) % 0.55/0.63 [79]~P1(x791)+~P7(x792,x791) % 0.55/0.63 [81]~P7(x811,x812)+P4(x811,x812) % 0.55/0.63 [84]~P7(x842,x841)+~P7(x841,x842) % 0.55/0.63 [83]~P3(x831,x832)+P4(x831,f19(x832)) % 0.55/0.63 [85]P3(x851,x852)+~P4(x851,f19(x852)) % 0.55/0.63 [92]~P5(x921,x922,x923)+P6(x921,x922,x923) % 0.55/0.63 [93]~P6(x931,x932,x933)+P5(x931,x932,x933) % 0.55/0.63 [90]P2(x901)+~P4(x901,f19(f20(x902,x903))) % 0.55/0.63 [94]~P6(x941,x942,x943)+P4(x941,f19(f20(x942,x943))) % 0.55/0.63 [95]~P5(x953,x951,x952)+E(f18(x951,x952,x953,x954),f22(x953,x954)) % 0.55/0.63 [96]~P5(x963,x961,x962)+P4(f18(x961,x962,x963,x964),f19(x962)) % 0.55/0.63 [77]~P1(x772)+~P1(x771)+E(x771,x772) % 0.55/0.63 [82]~P4(x822,x821)+P1(x821)+P7(x822,x821) % 0.55/0.63 [86]P1(x861)+P1(x862)+~P1(f20(x862,x861)) % 0.55/0.63 [89]E(x891,x892)+P7(f10(x891,x892),x892)+P7(f10(x891,x892),x891) % 0.55/0.63 [91]E(x911,x912)+~P7(f10(x911,x912),x912)+~P7(f10(x911,x912),x911) % 0.55/0.63 [87]~P1(x871)+~P7(x872,x873)+~P4(x873,f19(x871)) % 0.55/0.63 [88]P4(x881,x882)+~P7(x881,x883)+~P4(x883,f19(x882)) % 0.55/0.63 [98]~P4(x984,x981)+~P5(x983,x981,x982)+P4(f21(x981,x982,x983,x984),f19(x982)) % 0.55/0.63 [97]~P4(x974,x971)+~P6(x973,x971,x972)+E(f21(x971,x972,x973,x974),f18(x971,x972,x973,f17(x974))) % 0.55/0.63 [99]~P6(x994,x991,x992)+P1(x991)+~P4(x993,f19(x991))+P4(f4(x991,x992,x993,x994),f19(f19(x992))) % 0.55/0.63 [101]~P6(x1015,x1011,x1013)+P1(x1011)+~P4(x1014,f19(x1011))+~P7(x1012,f4(x1011,x1013,x1014,x1015))+P4(f16(x1012,x1011,x1013,x1014,x1015),x1011) % 0.55/0.63 [102]~P6(x1025,x1021,x1023)+P1(x1021)+~P4(x1024,f19(x1021))+~P7(x1022,f4(x1021,x1023,x1024,x1025))+P7(f16(x1022,x1021,x1023,x1024,x1025),x1024) % 0.55/0.63 [103]P1(x1031)+~P6(x1033,x1031,x1032)+~P4(x1035,f19(x1031))+~P7(x1034,f4(x1031,x1032,x1035,x1033))+E(f21(x1031,x1032,x1033,f16(x1034,x1031,x1032,x1035,x1033)),x1034) % 0.55/0.63 [100]~P4(x1006,x1001)+~P7(x1006,x1004)+~P6(x1005,x1001,x1003)+P1(x1001)+~P4(x1004,f19(x1001))+P7(x1002,f4(x1001,x1003,x1004,x1005))+~E(x1002,f21(x1001,x1003,x1005,x1006)) % 0.55/0.63 %EqnAxiom % 0.55/0.63 [1]E(x11,x11) % 0.55/0.63 [2]E(x22,x21)+~E(x21,x22) % 0.55/0.63 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.55/0.63 [4]~E(x41,x42)+E(f7(x41),f7(x42)) % 0.55/0.63 [5]~E(x51,x52)+E(f19(x51),f19(x52)) % 0.55/0.63 [6]~E(x61,x62)+E(f12(x61),f12(x62)) % 0.55/0.63 [7]~E(x71,x72)+E(f4(x71,x73,x74,x75),f4(x72,x73,x74,x75)) % 0.55/0.63 [8]~E(x81,x82)+E(f4(x83,x81,x84,x85),f4(x83,x82,x84,x85)) % 0.55/0.63 [9]~E(x91,x92)+E(f4(x93,x94,x91,x95),f4(x93,x94,x92,x95)) % 0.55/0.63 [10]~E(x101,x102)+E(f4(x103,x104,x105,x101),f4(x103,x104,x105,x102)) % 0.55/0.63 [11]~E(x111,x112)+E(f21(x111,x113,x114,x115),f21(x112,x113,x114,x115)) % 0.55/0.63 [12]~E(x121,x122)+E(f21(x123,x121,x124,x125),f21(x123,x122,x124,x125)) % 0.55/0.63 [13]~E(x131,x132)+E(f21(x133,x134,x131,x135),f21(x133,x134,x132,x135)) % 0.55/0.63 [14]~E(x141,x142)+E(f21(x143,x144,x145,x141),f21(x143,x144,x145,x142)) % 0.55/0.63 [15]~E(x151,x152)+E(f20(x151,x153),f20(x152,x153)) % 0.55/0.63 [16]~E(x161,x162)+E(f20(x163,x161),f20(x163,x162)) % 0.55/0.63 [17]~E(x171,x172)+E(f15(x171,x173),f15(x172,x173)) % 0.55/0.63 [18]~E(x181,x182)+E(f15(x183,x181),f15(x183,x182)) % 0.55/0.63 [19]~E(x191,x192)+E(f14(x191,x193),f14(x192,x193)) % 0.55/0.63 [20]~E(x201,x202)+E(f14(x203,x201),f14(x203,x202)) % 0.55/0.63 [21]~E(x211,x212)+E(f16(x211,x213,x214,x215,x216),f16(x212,x213,x214,x215,x216)) % 0.55/0.63 [22]~E(x221,x222)+E(f16(x223,x221,x224,x225,x226),f16(x223,x222,x224,x225,x226)) % 0.55/0.63 [23]~E(x231,x232)+E(f16(x233,x234,x231,x235,x236),f16(x233,x234,x232,x235,x236)) % 0.55/0.63 [24]~E(x241,x242)+E(f16(x243,x244,x245,x241,x246),f16(x243,x244,x245,x242,x246)) % 0.55/0.63 [25]~E(x251,x252)+E(f16(x253,x254,x255,x256,x251),f16(x253,x254,x255,x256,x252)) % 0.55/0.63 [26]~E(x261,x262)+E(f17(x261),f17(x262)) % 0.55/0.63 [27]~E(x271,x272)+E(f18(x271,x273,x274,x275),f18(x272,x273,x274,x275)) % 0.55/0.63 [28]~E(x281,x282)+E(f18(x283,x281,x284,x285),f18(x283,x282,x284,x285)) % 0.55/0.63 [29]~E(x291,x292)+E(f18(x293,x294,x291,x295),f18(x293,x294,x292,x295)) % 0.55/0.63 [30]~E(x301,x302)+E(f18(x303,x304,x305,x301),f18(x303,x304,x305,x302)) % 0.55/0.63 [31]~E(x311,x312)+E(f22(x311,x313),f22(x312,x313)) % 0.55/0.63 [32]~E(x321,x322)+E(f22(x323,x321),f22(x323,x322)) % 0.55/0.63 [33]~E(x331,x332)+E(f10(x331,x333),f10(x332,x333)) % 0.55/0.63 [34]~E(x341,x342)+E(f10(x343,x341),f10(x343,x342)) % 0.55/0.63 [35]~E(x351,x352)+E(f5(x351),f5(x352)) % 0.55/0.63 [36]~P1(x361)+P1(x362)+~E(x361,x362) % 0.55/0.63 [37]P7(x372,x373)+~E(x371,x372)+~P7(x371,x373) % 0.55/0.63 [38]P7(x383,x382)+~E(x381,x382)+~P7(x383,x381) % 0.55/0.63 [39]P4(x392,x393)+~E(x391,x392)+~P4(x391,x393) % 0.55/0.63 [40]P4(x403,x402)+~E(x401,x402)+~P4(x403,x401) % 0.55/0.63 [41]~P2(x411)+P2(x412)+~E(x411,x412) % 0.55/0.63 [42]P5(x422,x423,x424)+~E(x421,x422)+~P5(x421,x423,x424) % 0.55/0.63 [43]P5(x433,x432,x434)+~E(x431,x432)+~P5(x433,x431,x434) % 0.55/0.63 [44]P5(x443,x444,x442)+~E(x441,x442)+~P5(x443,x444,x441) % 0.55/0.63 [45]P6(x452,x453,x454)+~E(x451,x452)+~P6(x451,x453,x454) % 0.55/0.63 [46]P6(x463,x462,x464)+~E(x461,x462)+~P6(x463,x461,x464) % 0.63/0.63 [47]P6(x473,x474,x472)+~E(x471,x472)+~P6(x473,x474,x471) % 0.63/0.63 [48]P3(x482,x483)+~E(x481,x482)+~P3(x481,x483) % 0.63/0.63 [49]P3(x493,x492)+~E(x491,x492)+~P3(x493,x491) % 0.63/0.63 [50]~P8(x501)+P8(x502)+~E(x501,x502) % 0.63/0.63 % 0.63/0.63 %------------------------------------------- % 0.63/0.63 cnf(105,plain, % 0.63/0.63 ($false), % 0.63/0.63 inference(scs_inference,[],[67,70,63,74,99]), % 0.63/0.63 ['proof']). % 0.63/0.63 % SZS output end Proof % 0.63/0.63 % Total time :0.000000s %------------------------------------------------------------------------------