%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG088+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n024.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 14:01:01 EDT 2024 % Result : Theorem 3.45s 3.52s % Output : CNFRefutation 3.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : RNG088+1 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Jun 18 14:51:24 EDT 2024 % 0.13/0.34 % CPUTime : % 0.20/0.58 start to proof:theBenchmark % 3.45/3.51 %------------------------------------------- % 3.45/3.51 % File :CSE---1.7 % 3.45/3.51 % Problem :theBenchmark % 3.45/3.51 % Transform :cnf % 3.45/3.51 % Format :tptp:raw % 3.45/3.51 % Command :java -jar mcs_scs.jar %d %s % 3.45/3.51 % 3.45/3.51 % Result :Theorem 2.890000s % 3.45/3.51 % Output :CNFRefutation 2.890000s % 3.45/3.51 %------------------------------------------- % 3.45/3.51 %------------------------------------------------------------------------------ % 3.45/3.51 % File : RNG088+1 : TPTP v8.2.0. Released v4.0.0. % 3.45/3.51 % Domain : Ring Theory % 3.45/3.51 % Problem : Chinese remainder theorem in a ring 03_03, 00 expansion % 3.45/3.51 % Version : Especial. % 3.45/3.51 % English : % 3.45/3.51 % 3.45/3.51 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 3.45/3.51 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 3.45/3.51 % Source : [Pas08] % 3.45/3.51 % Names : chines_03_03.00 [Pas08] % 3.45/3.51 % 3.45/3.51 % Status : Theorem % 3.45/3.51 % Rating : 0.22 v8.2.0, 0.25 v8.1.0, 0.14 v7.5.0, 0.12 v7.4.0, 0.17 v7.3.0, 0.14 v7.1.0, 0.17 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.12 v6.2.0, 0.16 v6.1.0, 0.23 v6.0.0, 0.22 v5.5.0, 0.30 v5.4.0, 0.36 v5.3.0, 0.37 v5.2.0, 0.20 v5.1.0, 0.29 v5.0.0, 0.33 v4.1.0, 0.43 v4.0.1, 0.83 v4.0.0 % 3.45/3.51 % Syntax : Number of formulae : 29 ( 3 unt; 3 def) % 3.45/3.51 % Number of atoms : 99 ( 26 equ) % 3.45/3.51 % Maximal formula atoms : 8 ( 3 avg) % 3.45/3.51 % Number of connectives : 71 ( 1 ~; 1 |; 36 &) % 3.45/3.51 % ( 5 <=>; 28 =>; 0 <=; 0 <~>) % 3.45/3.51 % Maximal formula depth : 13 ( 5 avg) % 3.45/3.51 % Maximal term depth : 3 ( 1 avg) % 3.45/3.51 % Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty) % 3.45/3.51 % Number of functors : 16 ( 16 usr; 11 con; 0-2 aty) % 3.45/3.51 % Number of variables : 47 ( 45 !; 2 ?) % 3.45/3.51 % SPC : FOF_THM_RFO_SEQ % 3.45/3.51 % 3.45/3.52 % Comments : Problem generated by the SAD system [VLP07] % 3.45/3.52 %------------------------------------------------------------------------------ % 3.45/3.52 fof(mElmSort,axiom, % 3.45/3.52 ! [W0] : % 3.45/3.52 ( aElement0(W0) % 3.45/3.52 => $true ) ). % 3.45/3.52 % 3.45/3.52 fof(mSortsC,axiom, % 3.45/3.52 aElement0(sz00) ). % 3.45/3.52 % 3.45/3.52 fof(mSortsC_01,axiom, % 3.45/3.52 aElement0(sz10) ). % 3.45/3.52 % 3.45/3.52 fof(mSortsU,axiom, % 3.45/3.52 ! [W0] : % 3.45/3.52 ( aElement0(W0) % 3.45/3.52 => aElement0(smndt0(W0)) ) ). % 3.45/3.52 % 3.45/3.52 fof(mSortsB,axiom, % 3.45/3.52 ! [W0,W1] : % 3.45/3.52 ( ( aElement0(W0) % 3.45/3.52 & aElement0(W1) ) % 3.45/3.52 => aElement0(sdtpldt0(W0,W1)) ) ). % 3.45/3.52 % 3.45/3.52 fof(mSortsB_02,axiom, % 3.45/3.52 ! [W0,W1] : % 3.45/3.52 ( ( aElement0(W0) % 3.45/3.52 & aElement0(W1) ) % 3.45/3.52 => aElement0(sdtasdt0(W0,W1)) ) ). % 3.45/3.52 % 3.45/3.52 fof(mAddComm,axiom, % 3.45/3.52 ! [W0,W1] : % 3.45/3.52 ( ( aElement0(W0) % 3.45/3.52 & aElement0(W1) ) % 3.45/3.52 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 3.45/3.52 % 3.45/3.52 fof(mAddAsso,axiom, % 3.45/3.52 ! [W0,W1,W2] : % 3.45/3.52 ( ( aElement0(W0) % 3.45/3.52 & aElement0(W1) % 3.45/3.52 & aElement0(W2) ) % 3.45/3.52 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 3.45/3.52 % 3.45/3.52 fof(mAddZero,axiom, % 3.45/3.52 ! [W0] : % 3.45/3.52 ( aElement0(W0) % 3.45/3.52 => ( sdtpldt0(W0,sz00) = W0 % 3.45/3.52 & W0 = sdtpldt0(sz00,W0) ) ) ). % 3.45/3.52 % 3.45/3.52 fof(mAddInvr,axiom, % 3.45/3.52 ! [W0] : % 3.45/3.52 ( aElement0(W0) % 3.45/3.52 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 3.45/3.52 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 3.45/3.52 % 3.45/3.52 fof(mMulComm,axiom, % 3.45/3.52 ! [W0,W1] : % 3.45/3.52 ( ( aElement0(W0) % 3.45/3.52 & aElement0(W1) ) % 3.45/3.52 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 3.45/3.52 % 3.45/3.52 fof(mMulAsso,axiom, % 3.45/3.52 ! [W0,W1,W2] : % 3.45/3.52 ( ( aElement0(W0) % 3.45/3.52 & aElement0(W1) % 3.45/3.52 & aElement0(W2) ) % 3.45/3.52 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 3.45/3.52 % 3.45/3.52 fof(mMulUnit,axiom, % 3.45/3.52 ! [W0] : % 3.45/3.52 ( aElement0(W0) % 3.45/3.52 => ( sdtasdt0(W0,sz10) = W0 % 3.45/3.52 & W0 = sdtasdt0(sz10,W0) ) ) ). % 3.45/3.52 % 3.45/3.52 fof(mAMDistr,axiom, % 3.45/3.52 ! [W0,W1,W2] : % 3.45/3.52 ( ( aElement0(W0) % 3.45/3.52 & aElement0(W1) % 3.45/3.52 & aElement0(W2) ) % 3.45/3.52 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 3.45/3.52 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 3.45/3.52 % 3.45/3.52 fof(mMulMnOne,axiom, % 3.45/3.52 ! [W0] : % 3.45/3.52 ( aElement0(W0) % 3.45/3.52 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 3.45/3.52 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 3.45/3.52 % 3.45/3.52 fof(mMulZero,axiom, % 3.45/3.52 ! [W0] : % 3.45/3.52 ( aElement0(W0) % 3.45/3.52 => ( sdtasdt0(W0,sz00) = sz00 % 3.45/3.52 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 3.45/3.52 % 3.45/3.52 fof(mCancel,axiom, % 3.45/3.52 ! [W0,W1] : % 3.45/3.52 ( ( aElement0(W0) % 3.45/3.52 & aElement0(W1) ) % 3.45/3.52 => ( sdtasdt0(W0,W1) = sz00 % 3.45/3.52 => ( W0 = sz00 % 3.45/3.52 | W1 = sz00 ) ) ) ). % 3.45/3.52 % 3.45/3.52 fof(mUnNeZr,axiom, % 3.45/3.52 sz10 != sz00 ). % 3.45/3.52 % 3.45/3.52 fof(mSetSort,axiom, % 3.45/3.52 ! [W0] : % 3.45/3.52 ( aSet0(W0) % 3.45/3.52 => $true ) ). % 3.45/3.52 % 3.45/3.52 fof(mEOfElem,axiom, % 3.45/3.52 ! [W0] : % 3.45/3.52 ( aSet0(W0) % 3.45/3.52 => ! [W1] : % 3.45/3.52 ( aElementOf0(W1,W0) % 3.45/3.52 => aElement0(W1) ) ) ). % 3.45/3.52 % 3.45/3.52 fof(mSetEq,axiom, % 3.45/3.52 ! [W0,W1] : % 3.45/3.52 ( ( aSet0(W0) % 3.45/3.52 & aSet0(W1) ) % 3.45/3.52 => ( ( ! [W2] : % 3.45/3.52 ( aElementOf0(W2,W0) % 3.45/3.52 => aElementOf0(W2,W1) ) % 3.45/3.52 & ! [W2] : % 3.45/3.52 ( aElementOf0(W2,W1) % 3.45/3.52 => aElementOf0(W2,W0) ) ) % 3.45/3.52 => W0 = W1 ) ) ). % 3.45/3.52 % 3.45/3.52 fof(mDefSSum,definition, % 3.45/3.52 ! [W0,W1] : % 3.45/3.52 ( ( aSet0(W0) % 3.45/3.52 & aSet0(W1) ) % 3.45/3.52 => ! [W2] : % 3.45/3.52 ( W2 = sdtpldt1(W0,W1) % 3.45/3.52 <=> ( aSet0(W2) % 3.45/3.52 & ! [W3] : % 3.45/3.52 ( aElementOf0(W3,W2) % 3.45/3.52 <=> ? [W4,W5] : % 3.45/3.52 ( aElementOf0(W4,W0) % 3.45/3.52 & aElementOf0(W5,W1) % 3.45/3.52 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 3.45/3.52 % 3.45/3.52 fof(mDefSInt,definition, % 3.45/3.52 ! [W0,W1] : % 3.45/3.52 ( ( aSet0(W0) % 3.45/3.52 & aSet0(W1) ) % 3.45/3.52 => ! [W2] : % 3.45/3.52 ( W2 = sdtasasdt0(W0,W1) % 3.45/3.52 <=> ( aSet0(W2) % 3.45/3.52 & ! [W3] : % 3.45/3.52 ( aElementOf0(W3,W2) % 3.45/3.52 <=> ( aElementOf0(W3,W0) % 3.45/3.52 & aElementOf0(W3,W1) ) ) ) ) ) ). % 3.45/3.52 % 3.45/3.52 fof(mDefIdeal,definition, % 3.45/3.52 ! [W0] : % 3.45/3.52 ( aIdeal0(W0) % 3.45/3.52 <=> ( aSet0(W0) % 3.45/3.52 & ! [W1] : % 3.45/3.52 ( aElementOf0(W1,W0) % 3.45/3.52 => ( ! [W2] : % 3.45/3.52 ( aElementOf0(W2,W0) % 3.45/3.52 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 3.45/3.52 & ! [W2] : % 3.45/3.52 ( aElement0(W2) % 3.45/3.52 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 3.45/3.52 % 3.45/3.52 fof(m__870,hypothesis, % 3.45/3.52 ( aIdeal0(xI) % 3.45/3.52 & aIdeal0(xJ) ) ). % 3.45/3.52 % 3.45/3.52 fof(m__901,hypothesis, % 3.45/3.52 ( aElementOf0(xx,sdtpldt1(xI,xJ)) % 3.45/3.52 & aElementOf0(xy,sdtpldt1(xI,xJ)) % 3.45/3.52 & aElement0(xz) ) ). % 3.45/3.52 % 3.45/3.52 fof(m__934,hypothesis, % 3.45/3.52 ( aElementOf0(xk,xI) % 3.45/3.52 & aElementOf0(xl,xJ) % 3.45/3.52 & xx = sdtpldt0(xk,xl) ) ). % 3.45/3.52 % 3.45/3.52 fof(m__967,hypothesis, % 3.45/3.52 ( aElementOf0(xm,xI) % 3.45/3.52 & aElementOf0(xn,xJ) % 3.45/3.52 & xy = sdtpldt0(xm,xn) ) ). % 3.45/3.52 % 3.45/3.52 fof(m__,conjecture, % 3.45/3.52 ( aElementOf0(sdtpldt0(xk,xm),xI) % 3.45/3.52 & aElementOf0(sdtpldt0(xl,xn),xJ) ) ). % 3.45/3.52 % 3.45/3.52 %------------------------------------------------------------------------------ % 3.45/3.52 %------------------------------------------- % 3.45/3.52 % Proof found % 3.45/3.52 % SZS status Theorem for theBenchmark % 3.45/3.52 % SZS output start Proof % 3.45/3.52 %ClaNum:108(EqnAxiom:44) % 3.45/3.52 %VarNum:392(SingletonVarNum:114) % 3.45/3.52 %MaxLitNum:8 % 3.45/3.52 %MaxfuncDepth:2 % 3.45/3.52 %SharedTerms:33 % 3.45/3.52 %goalClause: 89 % 3.45/3.53 [45]P1(a1) % 3.45/3.53 [46]P1(a18) % 3.45/3.53 [47]P1(a19) % 3.45/3.53 [48]P2(a20) % 3.45/3.53 [49]P2(a21) % 3.45/3.53 [52]P3(a22,a20) % 3.51/3.53 [53]P3(a23,a21) % 3.51/3.53 [54]P3(a25,a20) % 3.51/3.53 [55]P3(a26,a21) % 3.51/3.53 [58]~E(a1,a18) % 3.51/3.53 [50]E(f2(a22,a23),a24) % 3.51/3.53 [51]E(f2(a25,a26),a27) % 3.51/3.53 [56]P3(a24,f16(a20,a21)) % 3.51/3.53 [57]P3(a27,f16(a20,a21)) % 3.51/3.53 [89]~P3(f2(a22,a25),a20)+~P3(f2(a23,a26),a21) % 3.51/3.53 [59]~P2(x591)+P4(x591) % 3.51/3.53 [60]~P1(x601)+P1(f17(x601)) % 3.51/3.53 [61]~P1(x611)+E(f3(a1,x611),a1) % 3.51/3.53 [62]~P1(x621)+E(f3(x621,a1),a1) % 3.51/3.53 [63]~P1(x631)+E(f2(a1,x631),x631) % 3.51/3.53 [64]~P1(x641)+E(f3(a18,x641),x641) % 3.51/3.53 [65]~P1(x651)+E(f2(x651,a1),x651) % 3.51/3.53 [66]~P1(x661)+E(f3(x661,a18),x661) % 3.51/3.53 [67]~P1(x671)+E(f2(f17(x671),x671),a1) % 3.51/3.53 [68]~P1(x681)+E(f2(x681,f17(x681)),a1) % 3.51/3.53 [69]~P1(x691)+E(f3(x691,f17(a18)),f17(x691)) % 3.51/3.53 [70]~P1(x701)+E(f3(f17(a18),x701),f17(x701)) % 3.51/3.53 [71]~P4(x711)+P2(x711)+P3(f4(x711),x711) % 3.51/3.53 [72]~P3(x721,x722)+P1(x721)+~P4(x722) % 3.51/3.53 [74]~P1(x742)+~P1(x741)+E(f2(x741,x742),f2(x742,x741)) % 3.51/3.53 [75]~P1(x752)+~P1(x751)+E(f3(x751,x752),f3(x752,x751)) % 3.51/3.53 [79]~P1(x792)+~P1(x791)+P1(f2(x791,x792)) % 3.51/3.53 [80]~P1(x802)+~P1(x801)+P1(f3(x801,x802)) % 3.51/3.53 [78]~P4(x781)+P2(x781)+P3(f6(x781),x781)+P1(f5(x781)) % 3.51/3.53 [93]~P4(x931)+P2(x931)+P1(f5(x931))+~P3(f2(f4(x931),f6(x931)),x931) % 3.51/3.53 [96]~P4(x961)+P2(x961)+P3(f6(x961),x961)+~P3(f3(f5(x961),f4(x961)),x961) % 3.51/3.53 [98]~P4(x981)+P2(x981)+~P3(f2(f4(x981),f6(x981)),x981)+~P3(f3(f5(x981),f4(x981)),x981) % 3.51/3.53 [76]~P4(x763)+~P4(x762)+P4(x761)+~E(x761,f16(x762,x763)) % 3.51/3.53 [77]~P4(x773)+~P4(x772)+P4(x771)+~E(x771,f15(x772,x773)) % 3.51/3.53 [83]~P1(x831)+~P2(x833)+~P3(x832,x833)+P3(f3(x831,x832),x833) % 3.51/3.53 [84]~P2(x843)+~P3(x841,x843)+~P3(x842,x843)+P3(f2(x841,x842),x843) % 3.51/3.53 [87]~P1(x873)+~P1(x872)+~P1(x871)+E(f2(f2(x871,x872),x873),f2(x871,f2(x872,x873))) % 3.51/3.53 [88]~P1(x883)+~P1(x882)+~P1(x881)+E(f3(f3(x881,x882),x883),f3(x881,f3(x882,x883))) % 3.51/3.53 [94]~P1(x943)+~P1(x942)+~P1(x941)+E(f2(f3(x941,x942),f3(x941,x943)),f3(x941,f2(x942,x943))) % 3.51/3.53 [95]~P1(x952)+~P1(x953)+~P1(x951)+E(f2(f3(x951,x952),f3(x953,x952)),f3(f2(x951,x953),x952)) % 3.51/3.53 [73]~P1(x731)+~P1(x732)+E(x731,a1)+E(x732,a1)+~E(f3(x732,x731),a1) % 3.51/3.53 [85]~P4(x852)+~P4(x851)+E(x851,x852)+P3(f7(x851,x852),x851)+P3(f8(x851,x852),x852) % 3.51/3.53 [90]~P4(x902)+~P4(x901)+E(x901,x902)+P3(f7(x901,x902),x901)+~P3(f8(x901,x902),x901) % 3.51/3.53 [91]~P4(x912)+~P4(x911)+E(x911,x912)+P3(f8(x911,x912),x912)+~P3(f7(x911,x912),x912) % 3.51/3.53 [97]~P4(x972)+~P4(x971)+E(x971,x972)+~P3(f7(x971,x972),x972)+~P3(f8(x971,x972),x971) % 3.51/3.53 [81]~P4(x814)+~P4(x812)+~P3(x811,x813)+P3(x811,x812)+~E(x813,f15(x814,x812)) % 3.51/3.53 [82]~P4(x824)+~P4(x822)+~P3(x821,x823)+P3(x821,x822)+~E(x823,f15(x822,x824)) % 3.51/3.53 [105]~P4(x1052)+~P4(x1051)+~P3(x1054,x1053)+~E(x1053,f16(x1051,x1052))+P3(f10(x1051,x1052,x1053,x1054),x1051) % 3.51/3.53 [106]~P4(x1062)+~P4(x1061)+~P3(x1064,x1063)+~E(x1063,f16(x1061,x1062))+P3(f11(x1061,x1062,x1063,x1064),x1062) % 3.51/3.53 [108]~P4(x1082)+~P4(x1081)+~P3(x1084,x1083)+~E(x1083,f16(x1081,x1082))+E(f2(f10(x1081,x1082,x1083,x1084),f11(x1081,x1082,x1083,x1084)),x1084) % 3.51/3.53 [99]~P4(x991)+~P4(x993)+~P4(x992)+P3(f9(x992,x993,x991),x991)+P3(f12(x992,x993,x991),x992)+E(x991,f16(x992,x993)) % 3.51/3.53 [100]~P4(x1001)+~P4(x1003)+~P4(x1002)+P3(f9(x1002,x1003,x1001),x1001)+P3(f13(x1002,x1003,x1001),x1003)+E(x1001,f16(x1002,x1003)) % 3.51/3.53 [101]~P4(x1011)+~P4(x1013)+~P4(x1012)+P3(f14(x1012,x1013,x1011),x1011)+P3(f14(x1012,x1013,x1011),x1013)+E(x1011,f15(x1012,x1013)) % 3.51/3.53 [102]~P4(x1021)+~P4(x1023)+~P4(x1022)+P3(f14(x1022,x1023,x1021),x1021)+P3(f14(x1022,x1023,x1021),x1022)+E(x1021,f15(x1022,x1023)) % 3.51/3.53 [104]~P4(x1041)+~P4(x1043)+~P4(x1042)+P3(f9(x1042,x1043,x1041),x1041)+E(x1041,f16(x1042,x1043))+E(f2(f12(x1042,x1043,x1041),f13(x1042,x1043,x1041)),f9(x1042,x1043,x1041)) % 3.51/3.53 [86]~P4(x864)+~P4(x863)+~P3(x861,x864)+~P3(x861,x863)+P3(x861,x862)+~E(x862,f15(x863,x864)) % 3.51/3.53 [107]~P4(x1071)+~P4(x1073)+~P4(x1072)+~P3(f14(x1072,x1073,x1071),x1071)+~P3(f14(x1072,x1073,x1071),x1073)+~P3(f14(x1072,x1073,x1071),x1072)+E(x1071,f15(x1072,x1073)) % 3.51/3.53 [92]~P4(x924)+~P4(x923)+~P3(x926,x924)+~P3(x925,x923)+P3(x921,x922)+~E(x922,f16(x923,x924))+~E(f2(x925,x926),x921) % 3.51/3.53 [103]~P4(x1031)+~P4(x1033)+~P4(x1032)+~P3(x1035,x1033)+~P3(x1034,x1032)+~P3(f9(x1032,x1033,x1031),x1031)+E(x1031,f16(x1032,x1033))+~E(f2(x1034,x1035),f9(x1032,x1033,x1031)) % 3.51/3.53 %EqnAxiom % 3.51/3.53 [1]E(x11,x11) % 3.51/3.53 [2]E(x22,x21)+~E(x21,x22) % 3.51/3.53 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 3.51/3.53 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 3.51/3.53 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 3.51/3.53 [6]~E(x61,x62)+E(f16(x61,x63),f16(x62,x63)) % 3.51/3.53 [7]~E(x71,x72)+E(f16(x73,x71),f16(x73,x72)) % 3.51/3.53 [8]~E(x81,x82)+E(f14(x81,x83,x84),f14(x82,x83,x84)) % 3.51/3.53 [9]~E(x91,x92)+E(f14(x93,x91,x94),f14(x93,x92,x94)) % 3.51/3.53 [10]~E(x101,x102)+E(f14(x103,x104,x101),f14(x103,x104,x102)) % 3.51/3.53 [11]~E(x111,x112)+E(f4(x111),f4(x112)) % 3.51/3.53 [12]~E(x121,x122)+E(f17(x121),f17(x122)) % 3.51/3.53 [13]~E(x131,x132)+E(f3(x131,x133),f3(x132,x133)) % 3.51/3.53 [14]~E(x141,x142)+E(f3(x143,x141),f3(x143,x142)) % 3.51/3.53 [15]~E(x151,x152)+E(f9(x151,x153,x154),f9(x152,x153,x154)) % 3.51/3.53 [16]~E(x161,x162)+E(f9(x163,x161,x164),f9(x163,x162,x164)) % 3.51/3.53 [17]~E(x171,x172)+E(f9(x173,x174,x171),f9(x173,x174,x172)) % 3.51/3.53 [18]~E(x181,x182)+E(f11(x181,x183,x184,x185),f11(x182,x183,x184,x185)) % 3.51/3.53 [19]~E(x191,x192)+E(f11(x193,x191,x194,x195),f11(x193,x192,x194,x195)) % 3.51/3.53 [20]~E(x201,x202)+E(f11(x203,x204,x201,x205),f11(x203,x204,x202,x205)) % 3.51/3.53 [21]~E(x211,x212)+E(f11(x213,x214,x215,x211),f11(x213,x214,x215,x212)) % 3.51/3.53 [22]~E(x221,x222)+E(f10(x221,x223,x224,x225),f10(x222,x223,x224,x225)) % 3.51/3.53 [23]~E(x231,x232)+E(f10(x233,x231,x234,x235),f10(x233,x232,x234,x235)) % 3.51/3.53 [24]~E(x241,x242)+E(f10(x243,x244,x241,x245),f10(x243,x244,x242,x245)) % 3.51/3.53 [25]~E(x251,x252)+E(f10(x253,x254,x255,x251),f10(x253,x254,x255,x252)) % 3.51/3.53 [26]~E(x261,x262)+E(f7(x261,x263),f7(x262,x263)) % 3.51/3.53 [27]~E(x271,x272)+E(f7(x273,x271),f7(x273,x272)) % 3.51/3.53 [28]~E(x281,x282)+E(f6(x281),f6(x282)) % 3.51/3.53 [29]~E(x291,x292)+E(f13(x291,x293,x294),f13(x292,x293,x294)) % 3.51/3.53 [30]~E(x301,x302)+E(f13(x303,x301,x304),f13(x303,x302,x304)) % 3.51/3.53 [31]~E(x311,x312)+E(f13(x313,x314,x311),f13(x313,x314,x312)) % 3.51/3.53 [32]~E(x321,x322)+E(f5(x321),f5(x322)) % 3.51/3.53 [33]~E(x331,x332)+E(f15(x331,x333),f15(x332,x333)) % 3.51/3.53 [34]~E(x341,x342)+E(f15(x343,x341),f15(x343,x342)) % 3.51/3.53 [35]~E(x351,x352)+E(f12(x351,x353,x354),f12(x352,x353,x354)) % 3.51/3.53 [36]~E(x361,x362)+E(f12(x363,x361,x364),f12(x363,x362,x364)) % 3.51/3.53 [37]~E(x371,x372)+E(f12(x373,x374,x371),f12(x373,x374,x372)) % 3.51/3.53 [38]~E(x381,x382)+E(f8(x381,x383),f8(x382,x383)) % 3.51/3.53 [39]~E(x391,x392)+E(f8(x393,x391),f8(x393,x392)) % 3.51/3.53 [40]~P1(x401)+P1(x402)+~E(x401,x402) % 3.51/3.53 [41]P3(x412,x413)+~E(x411,x412)+~P3(x411,x413) % 3.51/3.53 [42]P3(x423,x422)+~E(x421,x422)+~P3(x423,x421) % 3.51/3.53 [43]~P4(x431)+P4(x432)+~E(x431,x432) % 3.51/3.53 [44]~P2(x441)+P2(x442)+~E(x441,x442) % 3.51/3.53 % 3.51/3.53 %------------------------------------------- % 3.51/3.53 cnf(672,plain, % 3.51/3.53 (~P3(f2(a23,a26),a21)), % 3.51/3.53 inference(scs_inference,[],[48,52,54,89,84])). % 3.51/3.53 cnf(674,plain, % 3.51/3.53 ($false), % 3.51/3.53 inference(scs_inference,[],[672,53,55,49,41,84]), % 3.51/3.53 ['proof']). % 3.51/3.53 % SZS output end Proof % 3.51/3.53 % Total time :2.890000s %------------------------------------------------------------------------------