%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU444+1 : TPTP v8.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/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:03:15 EDT 2024 % Result : Theorem 57.66s 57.69s % Output : CNFRefutation 57.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SEU444+1 : TPTP v8.2.0. Released v3.4.0. % 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n027.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 17:37:38 EDT 2024 % 0.12/0.33 % CPUTime : % 0.47/0.55 start to proof:theBenchmark % 57.64/57.67 %------------------------------------------- % 57.64/57.67 % File :CSE---1.7 % 57.64/57.67 % Problem :theBenchmark % 57.64/57.67 % Transform :cnf % 57.64/57.67 % Format :tptp:raw % 57.64/57.67 % Command :java -jar mcs_scs.jar %d %s % 57.64/57.67 % 57.64/57.67 % Result :Theorem 57.080000s % 57.64/57.67 % Output :CNFRefutation 57.080000s % 57.64/57.67 %------------------------------------------- % 57.64/57.68 %------------------------------------------------------------------------------ % 57.64/57.68 % File : SEU444+1 : TPTP v8.2.0. Released v3.4.0. % 57.64/57.68 % Domain : Set Theory % 57.64/57.68 % Problem : First and Second Order Cutting of Binary Relations T56 % 57.64/57.68 % Version : [Urb08] axioms : Especial. % 57.64/57.68 % English : % 57.64/57.68 % 57.64/57.68 % Refs : [Ret05] Retel (2005), Properties of First and Second Order Cut % 57.64/57.68 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 57.64/57.68 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 57.64/57.68 % Source : [Urb08] % 57.64/57.68 % Names : t56_relset_2 [Urb08] % 57.64/57.68 % 57.64/57.68 % Status : Theorem % 57.64/57.68 % Rating : 0.17 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.07 v7.3.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.27 v6.0.0, 0.17 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.30 v5.2.0, 0.10 v5.1.0, 0.19 v5.0.0, 0.29 v4.1.0, 0.35 v4.0.0, 0.38 v3.7.0, 0.25 v3.5.0, 0.26 v3.4.0 % 57.64/57.68 % Syntax : Number of formulae : 45 ( 14 unt; 0 def) % 57.64/57.68 % Number of atoms : 86 ( 10 equ) % 57.64/57.68 % Maximal formula atoms : 3 ( 1 avg) % 57.64/57.68 % Number of connectives : 53 ( 12 ~; 1 |; 18 &) % 57.64/57.68 % ( 2 <=>; 20 =>; 0 <=; 0 <~>) % 57.64/57.68 % Maximal formula depth : 7 ( 4 avg) % 57.64/57.68 % Maximal term depth : 3 ( 1 avg) % 57.64/57.68 % Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty) % 57.64/57.68 % Number of functors : 9 ( 9 usr; 1 con; 0-4 aty) % 57.64/57.68 % Number of variables : 77 ( 69 !; 8 ?) % 57.64/57.68 % SPC : FOF_THM_RFO_SEQ % 57.64/57.68 % 57.64/57.68 % Comments : Normal version: includes the axioms (which may be theorems from % 57.64/57.68 % other articles) and background that are possibly necessary. % 57.64/57.68 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 57.64/57.68 % : The problem encoding is based on set theory. % 57.64/57.68 %------------------------------------------------------------------------------ % 57.64/57.68 fof(t56_relset_2,conjecture, % 57.64/57.68 ! [A,B,C] : % 57.64/57.68 ( m2_relset_1(C,B,A) % 57.64/57.68 => ( k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A) % 57.64/57.68 & k10_relset_1(A,B,k6_relset_1(B,A,C),k10_relset_1(B,A,C,B)) = k10_relset_1(A,B,k6_relset_1(B,A,C),k2_funct_5(C)) ) ) ). % 57.64/57.68 % 57.64/57.68 fof(rc3_relat_1,axiom, % 57.64/57.68 ? [A] : % 57.64/57.68 ( v1_relat_1(A) % 57.64/57.68 & v3_relat_1(A) ) ). % 57.64/57.68 % 57.64/57.68 fof(antisymmetry_r2_hidden,axiom, % 57.64/57.68 ! [A,B] : % 57.64/57.68 ( r2_hidden(A,B) % 57.64/57.68 => ~ r2_hidden(B,A) ) ). % 57.64/57.68 % 57.64/57.68 fof(dt_k1_xboole_0,axiom, % 57.64/57.68 $true ). % 57.64/57.68 % 57.64/57.68 fof(fc12_relat_1,axiom, % 57.64/57.68 ( v1_xboole_0(k1_xboole_0) % 57.64/57.68 & v1_relat_1(k1_xboole_0) % 57.64/57.68 & v3_relat_1(k1_xboole_0) ) ). % 57.64/57.68 % 57.64/57.68 fof(fc4_relat_1,axiom, % 57.64/57.68 ( v1_xboole_0(k1_xboole_0) % 57.64/57.68 & v1_relat_1(k1_xboole_0) ) ). % 57.64/57.68 % 57.64/57.68 fof(t1_subset,axiom, % 57.64/57.68 ! [A,B] : % 57.66/57.68 ( r2_hidden(A,B) % 57.66/57.68 => m1_subset_1(A,B) ) ). % 57.66/57.68 % 57.66/57.68 fof(t4_subset,axiom, % 57.66/57.68 ! [A,B,C] : % 57.66/57.68 ( ( r2_hidden(A,B) % 57.66/57.68 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 57.66/57.68 => m1_subset_1(A,C) ) ). % 57.66/57.68 % 57.66/57.68 fof(t5_subset,axiom, % 57.66/57.68 ! [A,B,C] : % 57.66/57.68 ~ ( r2_hidden(A,B) % 57.66/57.68 & m1_subset_1(B,k1_zfmisc_1(C)) % 57.66/57.68 & v1_xboole_0(C) ) ). % 57.66/57.68 % 57.66/57.68 fof(reflexivity_r1_tarski,axiom, % 57.66/57.68 ! [A,B] : r1_tarski(A,A) ). % 57.66/57.68 % 57.66/57.68 fof(cc1_relat_1,axiom, % 57.66/57.68 ! [A] : % 57.66/57.68 ( v1_xboole_0(A) % 57.66/57.68 => v1_relat_1(A) ) ). % 57.66/57.68 % 57.66/57.68 fof(fc11_relat_1,axiom, % 57.66/57.68 ! [A] : % 57.66/57.68 ( v1_xboole_0(A) % 57.66/57.68 => ( v1_xboole_0(k4_relat_1(A)) % 57.66/57.68 & v1_relat_1(k4_relat_1(A)) ) ) ). % 57.66/57.68 % 57.66/57.68 fof(fc4_subset_1,axiom, % 57.66/57.68 ! [A,B] : % 57.66/57.68 ( ( ~ v1_xboole_0(A) % 57.66/57.68 & ~ v1_xboole_0(B) ) % 57.66/57.68 => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ). % 57.66/57.68 % 57.66/57.68 fof(rc1_relat_1,axiom, % 57.66/57.68 ? [A] : % 57.66/57.68 ( v1_xboole_0(A) % 57.66/57.68 & v1_relat_1(A) ) ). % 57.66/57.68 % 57.66/57.68 fof(rc1_subset_1,axiom, % 57.66/57.68 ! [A] : % 57.66/57.68 ( ~ v1_xboole_0(A) % 57.66/57.68 => ? [B] : % 57.66/57.68 ( m1_subset_1(B,k1_zfmisc_1(A)) % 57.66/57.68 & ~ v1_xboole_0(B) ) ) ). % 57.66/57.68 % 57.66/57.68 fof(rc2_relat_1,axiom, % 57.66/57.68 ? [A] : % 57.66/57.69 ( ~ v1_xboole_0(A) % 57.66/57.69 & v1_relat_1(A) ) ). % 57.66/57.69 % 57.66/57.69 fof(rc2_subset_1,axiom, % 57.66/57.69 ! [A] : % 57.66/57.69 ? [B] : % 57.66/57.69 ( m1_subset_1(B,k1_zfmisc_1(A)) % 57.66/57.69 & v1_xboole_0(B) ) ). % 57.66/57.69 % 57.66/57.69 fof(t2_subset,axiom, % 57.66/57.69 ! [A,B] : % 57.66/57.69 ( m1_subset_1(A,B) % 57.66/57.69 => ( v1_xboole_0(B) % 57.66/57.69 | r2_hidden(A,B) ) ) ). % 57.66/57.69 % 57.66/57.69 fof(t6_boole,axiom, % 57.66/57.69 ! [A] : % 57.66/57.69 ( v1_xboole_0(A) % 57.66/57.69 => A = k1_xboole_0 ) ). % 57.66/57.69 % 57.66/57.69 fof(t7_boole,axiom, % 57.66/57.69 ! [A,B] : % 57.66/57.69 ~ ( r2_hidden(A,B) % 57.66/57.69 & v1_xboole_0(B) ) ). % 57.66/57.69 % 57.66/57.69 fof(t8_boole,axiom, % 57.66/57.69 ! [A,B] : % 57.66/57.69 ~ ( v1_xboole_0(A) % 57.66/57.69 & A != B % 57.66/57.69 & v1_xboole_0(B) ) ). % 57.66/57.69 % 57.66/57.69 fof(involutiveness_k4_relat_1,axiom, % 57.66/57.69 ! [A] : % 57.66/57.69 ( v1_relat_1(A) % 57.66/57.69 => k4_relat_1(k4_relat_1(A)) = A ) ). % 57.66/57.69 % 57.66/57.69 fof(existence_m1_relset_1,axiom, % 57.66/57.69 ! [A,B] : % 57.66/57.69 ? [C] : m1_relset_1(C,A,B) ). % 57.66/57.69 % 57.66/57.69 fof(existence_m1_subset_1,axiom, % 57.66/57.69 ! [A] : % 57.66/57.69 ? [B] : m1_subset_1(B,A) ). % 57.66/57.69 % 57.66/57.69 fof(dt_k1_zfmisc_1,axiom, % 57.66/57.69 $true ). % 57.66/57.69 % 57.66/57.69 fof(dt_k2_zfmisc_1,axiom, % 57.66/57.69 $true ). % 57.66/57.69 % 57.66/57.69 fof(dt_k4_relat_1,axiom, % 57.66/57.69 ! [A] : % 57.66/57.69 ( v1_relat_1(A) % 57.66/57.69 => v1_relat_1(k4_relat_1(A)) ) ). % 57.66/57.69 % 57.66/57.69 fof(dt_k9_relat_1,axiom, % 57.66/57.69 $true ). % 57.66/57.69 % 57.66/57.69 fof(dt_m1_relset_1,axiom, % 57.66/57.69 $true ). % 57.66/57.69 % 57.66/57.69 fof(dt_m1_subset_1,axiom, % 57.66/57.69 $true ). % 57.66/57.69 % 57.66/57.69 fof(cc1_relset_1,axiom, % 57.66/57.69 ! [A,B,C] : % 57.66/57.69 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 57.66/57.69 => v1_relat_1(C) ) ). % 57.66/57.69 % 57.66/57.69 fof(fc1_subset_1,axiom, % 57.66/57.69 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 57.66/57.69 % 57.66/57.69 fof(fc1_sysrel,axiom, % 57.66/57.69 ! [A,B] : v1_relat_1(k2_zfmisc_1(A,B)) ). % 57.66/57.69 % 57.66/57.69 fof(t3_subset,axiom, % 57.66/57.69 ! [A,B] : % 57.66/57.69 ( m1_subset_1(A,k1_zfmisc_1(B)) % 57.66/57.69 <=> r1_tarski(A,B) ) ). % 57.66/57.69 % 57.66/57.69 fof(involutiveness_k6_relset_1,axiom, % 57.66/57.69 ! [A,B,C] : % 57.66/57.69 ( m1_relset_1(C,A,B) % 57.66/57.69 => k6_relset_1(A,B,k6_relset_1(A,B,C)) = C ) ). % 57.66/57.69 % 57.66/57.69 fof(existence_m2_relset_1,axiom, % 57.66/57.69 ! [A,B] : % 57.66/57.69 ? [C] : m2_relset_1(C,A,B) ). % 57.66/57.69 % 57.66/57.69 fof(redefinition_k10_relset_1,axiom, % 57.66/57.69 ! [A,B,C,D] : % 57.66/57.69 ( m1_relset_1(C,A,B) % 57.66/57.69 => k10_relset_1(A,B,C,D) = k9_relat_1(C,D) ) ). % 57.66/57.69 % 57.66/57.69 fof(redefinition_k6_relset_1,axiom, % 57.66/57.69 ! [A,B,C] : % 57.66/57.69 ( m1_relset_1(C,A,B) % 57.66/57.69 => k6_relset_1(A,B,C) = k4_relat_1(C) ) ). % 57.66/57.69 % 57.66/57.69 fof(redefinition_m2_relset_1,axiom, % 57.66/57.69 ! [A,B,C] : % 57.66/57.69 ( m2_relset_1(C,A,B) % 57.66/57.69 <=> m1_relset_1(C,A,B) ) ). % 57.66/57.69 % 57.66/57.69 fof(dt_k10_relset_1,axiom, % 57.66/57.69 ! [A,B,C,D] : % 57.66/57.69 ( m1_relset_1(C,A,B) % 57.66/57.69 => m1_subset_1(k10_relset_1(A,B,C,D),k1_zfmisc_1(B)) ) ). % 57.66/57.69 % 57.66/57.69 fof(dt_k1_funct_5,axiom, % 57.66/57.69 $true ). % 57.66/57.69 % 57.66/57.69 fof(dt_k2_funct_5,axiom, % 57.66/57.69 $true ). % 57.66/57.69 % 57.66/57.69 fof(dt_k6_relset_1,axiom, % 57.66/57.69 ! [A,B,C] : % 57.66/57.69 ( m1_relset_1(C,A,B) % 57.66/57.69 => m2_relset_1(k6_relset_1(A,B,C),B,A) ) ). % 57.66/57.69 % 57.66/57.69 fof(dt_m2_relset_1,axiom, % 57.66/57.69 ! [A,B,C] : % 57.66/57.69 ( m2_relset_1(C,A,B) % 57.66/57.69 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 57.66/57.69 % 57.66/57.69 fof(t51_relset_2,axiom, % 57.66/57.69 ! [A,B,C] : % 57.66/57.69 ( m2_relset_1(C,B,A) % 57.66/57.69 => ( k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A) % 57.66/57.69 & k2_funct_5(C) = k10_relset_1(B,A,C,B) ) ) ). % 57.66/57.69 % 57.66/57.69 %------------------------------------------------------------------------------ % 57.66/57.69 %------------------------------------------- % 57.66/57.69 % Proof found % 57.66/57.69 % SZS status Theorem for theBenchmark % 57.66/57.69 % SZS output start Proof % 57.66/57.69 %ClaNum:90(EqnAxiom:40) % 57.66/57.69 %VarNum:160(SingletonVarNum:76) % 57.66/57.69 %MaxLitNum:3 % 57.66/57.69 %MaxfuncDepth:2 % 57.66/57.69 %SharedTerms:26 % 57.66/57.69 %goalClause: 56 90 % 57.66/57.69 %singleGoalClaCount:1 % 57.66/57.69 [42]P1(a1) % 57.66/57.69 [43]P1(a2) % 57.66/57.69 [44]P1(a8) % 57.66/57.69 [45]P1(a9) % 57.66/57.69 [46]P7(a1) % 57.66/57.69 [47]P7(a2) % 57.66/57.69 [49]P8(a1) % 57.66/57.69 [50]P8(a8) % 57.66/57.69 [56]P5(a4,a5,a6) % 57.66/57.69 [59]~P8(a9) % 57.66/57.69 [52]P2(x521,x521) % 57.66/57.69 [51]P8(f11(x511)) % 57.66/57.69 [53]P3(f3(x531),x531) % 57.66/57.69 [54]P3(f11(x541),f15(x541)) % 57.66/57.69 [60]~P8(f15(x601)) % 57.66/57.69 [55]P1(f16(x551,x552)) % 57.66/57.69 [57]P5(f7(x571,x572),x571,x572) % 57.66/57.69 [58]P4(f12(x581,x582),x581,x582) % 57.66/57.69 [90]~E(f13(a6,a5,f19(a5,a6,a4),f13(a5,a6,a4,a5)),f13(a6,a5,f19(a5,a6,a4),f17(a4)))+~E(f13(a6,a5,f19(a5,a6,a4),a6),f14(a4)) % 57.66/57.69 [61]~P8(x611)+E(x611,a1) % 57.66/57.69 [62]~P8(x621)+P1(x621) % 57.66/57.69 [64]~P1(x641)+P1(f18(x641)) % 57.66/57.69 [65]~P8(x651)+P1(f18(x651)) % 57.66/57.69 [66]~P8(x661)+P8(f18(x661)) % 57.66/57.69 [68]P8(x681)+~P8(f10(x681)) % 57.66/57.69 [70]P8(x701)+P3(f10(x701),f15(x701)) % 57.66/57.69 [67]~P1(x671)+E(f18(f18(x671)),x671) % 57.66/57.69 [69]~P8(x691)+~P6(x692,x691) % 57.66/57.69 [71]~P6(x711,x712)+P3(x711,x712) % 57.66/57.69 [74]~P6(x742,x741)+~P6(x741,x742) % 57.66/57.69 [73]~P2(x731,x732)+P3(x731,f15(x732)) % 57.66/57.69 [75]P2(x751,x752)+~P3(x751,f15(x752)) % 57.66/57.69 [80]~P4(x801,x802,x803)+P5(x801,x802,x803) % 57.66/57.69 [81]~P5(x811,x812,x813)+P4(x811,x812,x813) % 57.66/57.69 [82]~P4(x823,x821,x822)+E(f19(x821,x822,x823),f18(x823)) % 57.66/57.69 [84]~P4(x843,x841,x842)+P5(f19(x841,x842,x843),x842,x841) % 57.66/57.69 [86]~P5(x863,x861,x862)+E(f13(x861,x862,x863,x861),f17(x863)) % 57.66/57.69 [79]P1(x791)+~P3(x791,f15(f16(x792,x793))) % 57.66/57.69 [83]~P5(x831,x832,x833)+P3(x831,f15(f16(x832,x833))) % 57.66/57.69 [85]~P4(x853,x851,x852)+E(f19(x851,x852,f19(x851,x852,x853)),x853) % 57.66/57.69 [88]~P5(x883,x882,x881)+E(f13(x881,x882,f19(x882,x881,x883),x881),f14(x883)) % 57.66/57.69 [87]~P4(x873,x871,x872)+E(f13(x871,x872,x873,x874),f20(x873,x874)) % 57.66/57.69 [89]~P4(x893,x891,x892)+P3(f13(x891,x892,x893,x894),f15(x892)) % 57.66/57.69 [63]~P8(x632)+~P8(x631)+E(x631,x632) % 57.66/57.69 [72]~P3(x722,x721)+P8(x721)+P6(x722,x721) % 57.66/57.69 [76]P8(x761)+P8(x762)+~P8(f16(x762,x761)) % 57.66/57.69 [77]~P8(x771)+~P6(x772,x773)+~P3(x773,f15(x771)) % 57.66/57.69 [78]P3(x781,x782)+~P6(x781,x783)+~P3(x783,f15(x782)) % 57.66/57.69 %EqnAxiom % 57.66/57.69 [1]E(x11,x11) % 57.66/57.69 [2]E(x22,x21)+~E(x21,x22) % 57.66/57.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 57.66/57.69 [4]~E(x41,x42)+E(f11(x41),f11(x42)) % 57.66/57.69 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 57.66/57.69 [6]~E(x61,x62)+E(f13(x61,x63,x64,x65),f13(x62,x63,x64,x65)) % 57.66/57.69 [7]~E(x71,x72)+E(f13(x73,x71,x74,x75),f13(x73,x72,x74,x75)) % 57.66/57.69 [8]~E(x81,x82)+E(f13(x83,x84,x81,x85),f13(x83,x84,x82,x85)) % 57.66/57.69 [9]~E(x91,x92)+E(f13(x93,x94,x95,x91),f13(x93,x94,x95,x92)) % 57.66/57.69 [10]~E(x101,x102)+E(f15(x101),f15(x102)) % 57.66/57.69 [11]~E(x111,x112)+E(f16(x111,x113),f16(x112,x113)) % 57.66/57.69 [12]~E(x121,x122)+E(f16(x123,x121),f16(x123,x122)) % 57.66/57.69 [13]~E(x131,x132)+E(f7(x131,x133),f7(x132,x133)) % 57.66/57.69 [14]~E(x141,x142)+E(f7(x143,x141),f7(x143,x142)) % 57.66/57.69 [15]~E(x151,x152)+E(f12(x151,x153),f12(x152,x153)) % 57.66/57.69 [16]~E(x161,x162)+E(f12(x163,x161),f12(x163,x162)) % 57.66/57.69 [17]~E(x171,x172)+E(f19(x171,x173,x174),f19(x172,x173,x174)) % 57.66/57.69 [18]~E(x181,x182)+E(f19(x183,x181,x184),f19(x183,x182,x184)) % 57.66/57.69 [19]~E(x191,x192)+E(f19(x193,x194,x191),f19(x193,x194,x192)) % 57.66/57.69 [20]~E(x201,x202)+E(f18(x201),f18(x202)) % 57.66/57.69 [21]~E(x211,x212)+E(f20(x211,x213),f20(x212,x213)) % 57.66/57.69 [22]~E(x221,x222)+E(f20(x223,x221),f20(x223,x222)) % 57.66/57.69 [23]~E(x231,x232)+E(f17(x231),f17(x232)) % 57.66/57.69 [24]~E(x241,x242)+E(f14(x241),f14(x242)) % 57.66/57.69 [25]~E(x251,x252)+E(f10(x251),f10(x252)) % 57.66/57.69 [26]~P1(x261)+P1(x262)+~E(x261,x262) % 57.66/57.69 [27]P4(x272,x273,x274)+~E(x271,x272)+~P4(x271,x273,x274) % 57.66/57.69 [28]P4(x283,x282,x284)+~E(x281,x282)+~P4(x283,x281,x284) % 57.66/57.69 [29]P4(x293,x294,x292)+~E(x291,x292)+~P4(x293,x294,x291) % 57.66/57.69 [30]P3(x302,x303)+~E(x301,x302)+~P3(x301,x303) % 57.66/57.69 [31]P3(x313,x312)+~E(x311,x312)+~P3(x313,x311) % 57.66/57.69 [32]P5(x322,x323,x324)+~E(x321,x322)+~P5(x321,x323,x324) % 57.66/57.69 [33]P5(x333,x332,x334)+~E(x331,x332)+~P5(x333,x331,x334) % 57.66/57.69 [34]P5(x343,x344,x342)+~E(x341,x342)+~P5(x343,x344,x341) % 57.66/57.69 [35]P2(x352,x353)+~E(x351,x352)+~P2(x351,x353) % 57.66/57.69 [36]P2(x363,x362)+~E(x361,x362)+~P2(x363,x361) % 57.66/57.69 [37]~P7(x371)+P7(x372)+~E(x371,x372) % 57.66/57.69 [38]P6(x382,x383)+~E(x381,x382)+~P6(x381,x383) % 57.66/57.69 [39]P6(x393,x392)+~E(x391,x392)+~P6(x393,x391) % 57.66/57.69 [40]~P8(x401)+P8(x402)+~E(x401,x402) % 57.66/57.69 % 57.66/57.69 %------------------------------------------- % 57.66/57.69 cnf(2842,plain, % 57.66/57.69 (~E(f13(a6,a5,f19(a5,a6,a4),f17(a4)),f13(a6,a5,f19(a5,a6,a4),f13(a5,a6,a4,a5)))+~E(f13(a6,a5,f19(a5,a6,a4),a6),f14(a4))), % 57.66/57.69 inference(scs_inference,[],[90,2])). % 57.66/57.69 cnf(2843,plain, % 57.66/57.69 (~E(f17(a4),f13(a5,a6,a4,a5))+~E(f13(a6,a5,f19(a5,a6,a4),a6),f14(a4))), % 57.66/57.69 inference(scs_inference,[],[2842,9])). % 57.66/57.69 cnf(2844,plain, % 57.66/57.69 (~E(f13(a5,a6,a4,a5),f17(a4))+~E(f13(a6,a5,f19(a5,a6,a4),a6),f14(a4))), % 57.66/57.69 inference(scs_inference,[],[2843,2])). % 57.66/57.69 cnf(2845,plain, % 57.66/57.69 (~E(f13(a6,a5,f19(a5,a6,a4),a6),f14(a4))), % 57.66/57.69 inference(scs_inference,[],[56,2844,86])). % 57.66/57.69 cnf(2846,plain, % 57.66/57.69 ($false), % 57.66/57.69 inference(scs_inference,[],[56,2845,88]), % 57.66/57.69 ['proof']). % 57.66/57.70 % SZS output end Proof % 57.66/57.70 % Total time :57.080000s %------------------------------------------------------------------------------