%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM540+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 : n022.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 12:24:54 EDT 2024 % Result : Theorem 5.53s 5.65s % Output : CNFRefutation 5.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NUM540+1 : TPTP v8.2.0. Released v4.0.0. % 0.04/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n022.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sat Jun 22 21:29:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.51/0.57 start to proof:theBenchmark % 5.53/5.63 %------------------------------------------- % 5.53/5.63 % File :CSE---1.7 % 5.53/5.63 % Problem :theBenchmark % 5.53/5.63 % Transform :cnf % 5.53/5.63 % Format :tptp:raw % 5.53/5.63 % Command :java -jar mcs_scs.jar %d %s % 5.53/5.63 % 5.53/5.63 % Result :Theorem 5.010000s % 5.53/5.63 % Output :CNFRefutation 5.010000s % 5.53/5.63 %------------------------------------------- % 5.53/5.64 %------------------------------------------------------------------------------ % 5.53/5.64 % File : NUM540+1 : TPTP v8.2.0. Released v4.0.0. % 5.53/5.64 % Domain : Number Theory % 5.53/5.64 % Problem : Ramsey's Infinite Theorem 08, 00 expansion % 5.53/5.64 % Version : Especial. % 5.53/5.64 % English : % 5.53/5.64 % 5.53/5.64 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 5.53/5.64 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 5.53/5.64 % Source : [Pas08] % 5.53/5.64 % Names : ramsey_08.00 [Pas08] % 5.53/5.64 % 5.53/5.64 % Status : Theorem % 5.53/5.64 % Rating : 0.25 v8.2.0, 0.28 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.23 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.22 v7.0.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.30 v6.0.0, 0.26 v5.5.0, 0.30 v5.4.0, 0.36 v5.3.0, 0.37 v5.2.0, 0.20 v5.1.0, 0.33 v5.0.0, 0.50 v4.1.0, 0.57 v4.0.1, 0.83 v4.0.0 % 5.53/5.64 % Syntax : Number of formulae : 52 ( 3 unt; 7 def) % 5.53/5.64 % Number of atoms : 193 ( 30 equ) % 5.53/5.64 % Maximal formula atoms : 8 ( 3 avg) % 5.53/5.64 % Number of connectives : 154 ( 13 ~; 3 |; 52 &) % 5.53/5.64 % ( 13 <=>; 73 =>; 0 <=; 0 <~>) % 5.53/5.64 % Maximal formula depth : 12 ( 5 avg) % 5.53/5.64 % Maximal term depth : 4 ( 1 avg) % 5.53/5.64 % Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty) % 5.53/5.64 % Number of functors : 10 ( 10 usr; 3 con; 0-2 aty) % 5.53/5.64 % Number of variables : 89 ( 86 !; 3 ?) % 5.53/5.64 % SPC : FOF_THM_RFO_SEQ % 5.53/5.64 % 5.53/5.64 % Comments : Problem generated by the SAD system [VLP07] % 5.53/5.64 %------------------------------------------------------------------------------ % 5.53/5.64 fof(mSetSort,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( aSet0(W0) % 5.53/5.64 => $true ) ). % 5.53/5.64 % 5.53/5.64 fof(mElmSort,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( aElement0(W0) % 5.53/5.64 => $true ) ). % 5.53/5.64 % 5.53/5.64 fof(mEOfElem,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( aSet0(W0) % 5.53/5.64 => ! [W1] : % 5.53/5.64 ( aElementOf0(W1,W0) % 5.53/5.64 => aElement0(W1) ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mFinRel,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( aSet0(W0) % 5.53/5.64 => ( isFinite0(W0) % 5.53/5.64 => $true ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mDefEmp,definition, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( W0 = slcrc0 % 5.53/5.64 <=> ( aSet0(W0) % 5.53/5.64 & ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mEmpFin,axiom, % 5.53/5.64 isFinite0(slcrc0) ). % 5.53/5.64 % 5.53/5.64 fof(mCntRel,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( aSet0(W0) % 5.53/5.64 => ( isCountable0(W0) % 5.53/5.64 => $true ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mCountNFin,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( ( aSet0(W0) % 5.53/5.64 & isCountable0(W0) ) % 5.53/5.64 => ~ isFinite0(W0) ) ). % 5.53/5.64 % 5.53/5.64 fof(mCountNFin_01,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( ( aSet0(W0) % 5.53/5.64 & isCountable0(W0) ) % 5.53/5.64 => W0 != slcrc0 ) ). % 5.53/5.64 % 5.53/5.64 fof(mDefSub,definition, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( aSet0(W0) % 5.53/5.64 => ! [W1] : % 5.53/5.64 ( aSubsetOf0(W1,W0) % 5.53/5.64 <=> ( aSet0(W1) % 5.53/5.64 & ! [W2] : % 5.53/5.64 ( aElementOf0(W2,W1) % 5.53/5.64 => aElementOf0(W2,W0) ) ) ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mSubFSet,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( ( aSet0(W0) % 5.53/5.64 & isFinite0(W0) ) % 5.53/5.64 => ! [W1] : % 5.53/5.64 ( aSubsetOf0(W1,W0) % 5.53/5.64 => isFinite0(W1) ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mSubRefl,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( aSet0(W0) % 5.53/5.64 => aSubsetOf0(W0,W0) ) ). % 5.53/5.64 % 5.53/5.64 fof(mSubASymm,axiom, % 5.53/5.64 ! [W0,W1] : % 5.53/5.64 ( ( aSet0(W0) % 5.53/5.64 & aSet0(W1) ) % 5.53/5.64 => ( ( aSubsetOf0(W0,W1) % 5.53/5.64 & aSubsetOf0(W1,W0) ) % 5.53/5.64 => W0 = W1 ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mSubTrans,axiom, % 5.53/5.64 ! [W0,W1,W2] : % 5.53/5.64 ( ( aSet0(W0) % 5.53/5.64 & aSet0(W1) % 5.53/5.64 & aSet0(W2) ) % 5.53/5.64 => ( ( aSubsetOf0(W0,W1) % 5.53/5.64 & aSubsetOf0(W1,W2) ) % 5.53/5.64 => aSubsetOf0(W0,W2) ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mDefCons,definition, % 5.53/5.64 ! [W0,W1] : % 5.53/5.64 ( ( aSet0(W0) % 5.53/5.64 & aElement0(W1) ) % 5.53/5.64 => ! [W2] : % 5.53/5.64 ( W2 = sdtpldt0(W0,W1) % 5.53/5.64 <=> ( aSet0(W2) % 5.53/5.64 & ! [W3] : % 5.53/5.64 ( aElementOf0(W3,W2) % 5.53/5.64 <=> ( aElement0(W3) % 5.53/5.64 & ( aElementOf0(W3,W0) % 5.53/5.64 | W3 = W1 ) ) ) ) ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mDefDiff,definition, % 5.53/5.64 ! [W0,W1] : % 5.53/5.64 ( ( aSet0(W0) % 5.53/5.64 & aElement0(W1) ) % 5.53/5.64 => ! [W2] : % 5.53/5.64 ( W2 = sdtmndt0(W0,W1) % 5.53/5.64 <=> ( aSet0(W2) % 5.53/5.64 & ! [W3] : % 5.53/5.64 ( aElementOf0(W3,W2) % 5.53/5.64 <=> ( aElement0(W3) % 5.53/5.64 & aElementOf0(W3,W0) % 5.53/5.64 & W3 != W1 ) ) ) ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mConsDiff,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( aSet0(W0) % 5.53/5.64 => ! [W1] : % 5.53/5.64 ( aElementOf0(W1,W0) % 5.53/5.64 => sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mDiffCons,axiom, % 5.53/5.64 ! [W0,W1] : % 5.53/5.64 ( ( aElement0(W0) % 5.53/5.64 & aSet0(W1) ) % 5.53/5.64 => ( ~ aElementOf0(W0,W1) % 5.53/5.64 => sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mCConsSet,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( aElement0(W0) % 5.53/5.64 => ! [W1] : % 5.53/5.64 ( ( aSet0(W1) % 5.53/5.64 & isCountable0(W1) ) % 5.53/5.64 => isCountable0(sdtpldt0(W1,W0)) ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mCDiffSet,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( aElement0(W0) % 5.53/5.64 => ! [W1] : % 5.53/5.64 ( ( aSet0(W1) % 5.53/5.64 & isCountable0(W1) ) % 5.53/5.64 => isCountable0(sdtmndt0(W1,W0)) ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mFConsSet,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( aElement0(W0) % 5.53/5.64 => ! [W1] : % 5.53/5.64 ( ( aSet0(W1) % 5.53/5.64 & isFinite0(W1) ) % 5.53/5.64 => isFinite0(sdtpldt0(W1,W0)) ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mFDiffSet,axiom, % 5.53/5.64 ! [W0] : % 5.53/5.64 ( aElement0(W0) % 5.53/5.64 => ! [W1] : % 5.53/5.64 ( ( aSet0(W1) % 5.53/5.64 & isFinite0(W1) ) % 5.53/5.64 => isFinite0(sdtmndt0(W1,W0)) ) ) ). % 5.53/5.64 % 5.53/5.64 fof(mNATSet,axiom, % 5.53/5.64 ( aSet0(szNzAzT0) % 5.53/5.64 & isCountable0(szNzAzT0) ) ). % 5.53/5.64 % 5.53/5.64 fof(mZeroNum,axiom, % 5.53/5.64 aElementOf0(sz00,szNzAzT0) ). % 5.53/5.64 % 5.53/5.65 fof(mSuccNum,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 => ( aElementOf0(szszuzczcdt0(W0),szNzAzT0) % 5.53/5.65 & szszuzczcdt0(W0) != sz00 ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mSuccEquSucc,axiom, % 5.53/5.65 ! [W0,W1] : % 5.53/5.65 ( ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 & aElementOf0(W1,szNzAzT0) ) % 5.53/5.65 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 5.53/5.65 => W0 = W1 ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mNatExtra,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 => ( W0 = sz00 % 5.53/5.65 | ? [W1] : % 5.53/5.65 ( aElementOf0(W1,szNzAzT0) % 5.53/5.65 & W0 = szszuzczcdt0(W1) ) ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mNatNSucc,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 => W0 != szszuzczcdt0(W0) ) ). % 5.53/5.65 % 5.53/5.65 fof(mLessRel,axiom, % 5.53/5.65 ! [W0,W1] : % 5.53/5.65 ( ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 & aElementOf0(W1,szNzAzT0) ) % 5.53/5.65 => ( sdtlseqdt0(W0,W1) % 5.53/5.65 => $true ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mZeroLess,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 => sdtlseqdt0(sz00,W0) ) ). % 5.53/5.65 % 5.53/5.65 fof(mNoScLessZr,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 => ~ sdtlseqdt0(szszuzczcdt0(W0),sz00) ) ). % 5.53/5.65 % 5.53/5.65 fof(mSuccLess,axiom, % 5.53/5.65 ! [W0,W1] : % 5.53/5.65 ( ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 & aElementOf0(W1,szNzAzT0) ) % 5.53/5.65 => ( sdtlseqdt0(W0,W1) % 5.53/5.65 <=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mLessSucc,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 => sdtlseqdt0(W0,szszuzczcdt0(W0)) ) ). % 5.53/5.65 % 5.53/5.65 fof(mLessRefl,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 => sdtlseqdt0(W0,W0) ) ). % 5.53/5.65 % 5.53/5.65 fof(mLessASymm,axiom, % 5.53/5.65 ! [W0,W1] : % 5.53/5.65 ( ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 & aElementOf0(W1,szNzAzT0) ) % 5.53/5.65 => ( ( sdtlseqdt0(W0,W1) % 5.53/5.65 & sdtlseqdt0(W1,W0) ) % 5.53/5.65 => W0 = W1 ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mLessTrans,axiom, % 5.53/5.65 ! [W0,W1,W2] : % 5.53/5.65 ( ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 & aElementOf0(W1,szNzAzT0) % 5.53/5.65 & aElementOf0(W2,szNzAzT0) ) % 5.53/5.65 => ( ( sdtlseqdt0(W0,W1) % 5.53/5.65 & sdtlseqdt0(W1,W2) ) % 5.53/5.65 => sdtlseqdt0(W0,W2) ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mLessTotal,axiom, % 5.53/5.65 ! [W0,W1] : % 5.53/5.65 ( ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 & aElementOf0(W1,szNzAzT0) ) % 5.53/5.65 => ( sdtlseqdt0(W0,W1) % 5.53/5.65 | sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mIHSort,axiom, % 5.53/5.65 ! [W0,W1] : % 5.53/5.65 ( ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 & aElementOf0(W1,szNzAzT0) ) % 5.53/5.65 => ( iLess0(W0,W1) % 5.53/5.65 => $true ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mIH,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 5.53/5.65 % 5.53/5.65 fof(mCardS,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aSet0(W0) % 5.53/5.65 => aElement0(sbrdtbr0(W0)) ) ). % 5.53/5.65 % 5.53/5.65 fof(mCardNum,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aSet0(W0) % 5.53/5.65 => ( aElementOf0(sbrdtbr0(W0),szNzAzT0) % 5.53/5.65 <=> isFinite0(W0) ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mCardEmpty,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aSet0(W0) % 5.53/5.65 => ( sbrdtbr0(W0) = sz00 % 5.53/5.65 <=> W0 = slcrc0 ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mCardCons,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( ( aSet0(W0) % 5.53/5.65 & isFinite0(W0) ) % 5.53/5.65 => ! [W1] : % 5.53/5.65 ( aElement0(W1) % 5.53/5.65 => ( ~ aElementOf0(W1,W0) % 5.53/5.65 => sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mCardDiff,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aSet0(W0) % 5.53/5.65 => ! [W1] : % 5.53/5.65 ( ( isFinite0(W0) % 5.53/5.65 & aElementOf0(W1,W0) ) % 5.53/5.65 => szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mCardSub,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aSet0(W0) % 5.53/5.65 => ! [W1] : % 5.53/5.65 ( ( isFinite0(W0) % 5.53/5.65 & aSubsetOf0(W1,W0) ) % 5.53/5.65 => sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mCardSubEx,axiom, % 5.53/5.65 ! [W0,W1] : % 5.53/5.65 ( ( aSet0(W0) % 5.53/5.65 & aElementOf0(W1,szNzAzT0) ) % 5.53/5.65 => ( ( isFinite0(W0) % 5.53/5.65 & sdtlseqdt0(W1,sbrdtbr0(W0)) ) % 5.53/5.65 => ? [W2] : % 5.53/5.65 ( aSubsetOf0(W2,W0) % 5.53/5.65 & sbrdtbr0(W2) = W1 ) ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mDefMin,definition, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( ( aSubsetOf0(W0,szNzAzT0) % 5.53/5.65 & W0 != slcrc0 ) % 5.53/5.65 => ! [W1] : % 5.53/5.65 ( W1 = szmzizndt0(W0) % 5.53/5.65 <=> ( aElementOf0(W1,W0) % 5.53/5.65 & ! [W2] : % 5.53/5.65 ( aElementOf0(W2,W0) % 5.53/5.65 => sdtlseqdt0(W1,W2) ) ) ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mDefMax,definition, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( ( aSubsetOf0(W0,szNzAzT0) % 5.53/5.65 & isFinite0(W0) % 5.53/5.65 & W0 != slcrc0 ) % 5.53/5.65 => ! [W1] : % 5.53/5.65 ( W1 = szmzazxdt0(W0) % 5.53/5.65 <=> ( aElementOf0(W1,W0) % 5.53/5.65 & ! [W2] : % 5.53/5.65 ( aElementOf0(W2,W0) % 5.53/5.65 => sdtlseqdt0(W2,W1) ) ) ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mMinMin,axiom, % 5.53/5.65 ! [W0,W1] : % 5.53/5.65 ( ( aSubsetOf0(W0,szNzAzT0) % 5.53/5.65 & aSubsetOf0(W1,szNzAzT0) % 5.53/5.65 & W0 != slcrc0 % 5.53/5.65 & W1 != slcrc0 ) % 5.53/5.65 => ( ( aElementOf0(szmzizndt0(W0),W1) % 5.53/5.65 & aElementOf0(szmzizndt0(W1),W0) ) % 5.53/5.65 => szmzizndt0(W0) = szmzizndt0(W1) ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mDefSeg,definition, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 => ! [W1] : % 5.53/5.65 ( W1 = slbdtrb0(W0) % 5.53/5.65 <=> ( aSet0(W1) % 5.53/5.65 & ! [W2] : % 5.53/5.65 ( aElementOf0(W2,W1) % 5.53/5.65 <=> ( aElementOf0(W2,szNzAzT0) % 5.53/5.65 & sdtlseqdt0(szszuzczcdt0(W2),W0) ) ) ) ) ) ). % 5.53/5.65 % 5.53/5.65 fof(mSegFin,axiom, % 5.53/5.65 ! [W0] : % 5.53/5.65 ( aElementOf0(W0,szNzAzT0) % 5.53/5.65 => isFinite0(slbdtrb0(W0)) ) ). % 5.53/5.65 % 5.53/5.65 fof(m__,conjecture, % 5.53/5.65 slbdtrb0(sz00) = slcrc0 ). % 5.53/5.65 % 5.53/5.65 %------------------------------------------------------------------------------ % 5.53/5.65 %------------------------------------------- % 5.53/5.65 % Proof found % 5.53/5.65 % SZS status Theorem for theBenchmark % 5.53/5.65 % SZS output start Proof % 5.53/5.65 %ClaNum:128(EqnAxiom:42) % 5.53/5.65 %VarNum:575(SingletonVarNum:175) % 5.53/5.65 %MaxLitNum:8 % 5.53/5.65 %MaxfuncDepth:3 % 5.53/5.65 %SharedTerms:9 % 5.53/5.65 %goalClause: 47 % 5.53/5.65 %singleGoalClaCount:1 % 5.53/5.65 [43]P1(a1) % 5.53/5.65 [44]P4(a2) % 5.53/5.65 [45]P5(a1) % 5.53/5.65 [46]P2(a16,a1) % 5.53/5.65 [47]~E(f3(a16),a2) % 5.53/5.65 [48]P1(x481)+~E(x481,a2) % 5.53/5.65 [54]~P1(x541)+P6(x541,x541) % 5.53/5.65 [60]~P2(x601,a1)+P8(a16,x601) % 5.53/5.65 [66]P8(x661,x661)+~P2(x661,a1) % 5.53/5.65 [52]~P1(x521)+P3(f4(x521)) % 5.53/5.65 [56]~P2(x561,a1)+~E(f17(x561),a16) % 5.53/5.65 [57]~P2(x571,a1)+~E(f17(x571),x571) % 5.53/5.65 [59]~P2(x591,a1)+P4(f3(x591)) % 5.53/5.65 [67]~P2(x671,a1)+P2(f17(x671),a1) % 5.53/5.65 [68]~P2(x681,a1)+P8(x681,f17(x681)) % 5.53/5.65 [69]~P2(x691,a1)+P7(x691,f17(x691)) % 5.53/5.65 [76]~P2(x761,a1)+~P8(f17(x761),a16) % 5.53/5.65 [55]~P2(x552,x551)+~E(x551,a2) % 5.53/5.65 [51]~P1(x511)+~P5(x511)+~E(x511,a2) % 5.53/5.65 [53]~P4(x531)+~P5(x531)+~P1(x531) % 5.53/5.65 [49]~P1(x491)+~E(x491,a2)+E(f4(x491),a16) % 5.53/5.65 [50]~P1(x501)+E(x501,a2)+~E(f4(x501),a16) % 5.53/5.65 [58]~P1(x581)+P2(f5(x581),x581)+E(x581,a2) % 5.53/5.65 [63]~P1(x631)+~P4(x631)+P2(f4(x631),a1) % 5.53/5.65 [70]~P2(x701,a1)+E(x701,a16)+P2(f6(x701),a1) % 5.53/5.65 [71]~P1(x711)+P4(x711)+~P2(f4(x711),a1) % 5.53/5.65 [61]~P2(x611,a1)+E(x611,a16)+E(f17(f6(x611)),x611) % 5.53/5.65 [64]~P6(x641,x642)+P1(x641)+~P1(x642) % 5.53/5.65 [65]~P2(x651,x652)+P3(x651)+~P1(x652) % 5.53/5.65 [62]P1(x621)+~P2(x622,a1)+~E(x621,f3(x622)) % 5.53/5.65 [94]~P1(x941)+~P2(x942,x941)+E(f14(f15(x941,x942),x942),x941) % 5.53/5.65 [72]~P4(x722)+~P6(x721,x722)+P4(x721)+~P1(x722) % 5.53/5.65 [75]P2(x752,x751)+~E(x752,f18(x751))+~P6(x751,a1)+E(x751,a2) % 5.53/5.65 [78]~P1(x781)+~P3(x782)+~P4(x781)+P4(f14(x781,x782)) % 5.53/5.65 [79]~P1(x791)+~P3(x792)+~P4(x791)+P4(f15(x791,x792)) % 5.53/5.65 [80]~P1(x801)+~P3(x802)+~P5(x801)+P5(f14(x801,x802)) % 5.53/5.65 [81]~P1(x811)+~P3(x812)+~P5(x811)+P5(f15(x811,x812)) % 5.53/5.65 [82]E(x821,x822)+~E(f17(x821),f17(x822))+~P2(x822,a1)+~P2(x821,a1) % 5.53/5.65 [85]~P1(x852)+~P4(x852)+~P6(x851,x852)+P8(f4(x851),f4(x852)) % 5.53/5.65 [92]~P1(x921)+~P1(x922)+P6(x921,x922)+P2(f7(x922,x921),x921) % 5.53/5.65 [98]P8(x981,x982)+P8(f17(x982),x981)+~P2(x982,a1)+~P2(x981,a1) % 5.53/5.65 [105]~P8(x1051,x1052)+~P2(x1052,a1)+~P2(x1051,a1)+P8(f17(x1051),f17(x1052)) % 5.53/5.65 [107]~P1(x1071)+~P1(x1072)+P6(x1071,x1072)+~P2(f7(x1072,x1071),x1072) % 5.53/5.65 [109]P8(x1091,x1092)+~P2(x1092,a1)+~P2(x1091,a1)+~P8(f17(x1091),f17(x1092)) % 5.53/5.65 [93]P2(x932,x931)+~P1(x931)+~P3(x932)+E(f15(f14(x931,x932),x932),x931) % 5.53/5.65 [112]~P1(x1121)+~P4(x1121)+~P2(x1122,x1121)+E(f17(f4(f15(x1121,x1122))),f4(x1121)) % 5.53/5.65 [90]~P1(x902)+~P6(x903,x902)+P2(x901,x902)+~P2(x901,x903) % 5.53/5.65 [73]~P1(x732)+~P3(x733)+P1(x731)+~E(x731,f14(x732,x733)) % 5.53/5.65 [74]~P1(x742)+~P3(x743)+P1(x741)+~E(x741,f15(x742,x743)) % 5.53/5.65 [86]~P2(x861,x862)+~P2(x863,a1)+P2(x861,a1)+~E(x862,f3(x863)) % 5.53/5.65 [95]~P2(x951,x953)+~P2(x952,a1)+P8(f17(x951),x952)+~E(x953,f3(x952)) % 5.53/5.65 [83]~P1(x832)+~P1(x831)+~P6(x832,x831)+~P6(x831,x832)+E(x831,x832) % 5.53/5.65 [104]~P8(x1042,x1041)+~P8(x1041,x1042)+E(x1041,x1042)+~P2(x1042,a1)+~P2(x1041,a1) % 5.53/5.65 [77]~P4(x771)+P2(x772,x771)+~E(x772,f19(x771))+~P6(x771,a1)+E(x771,a2) % 5.53/5.65 [106]~P2(x1062,x1061)+P2(f10(x1061,x1062),x1061)+~P6(x1061,a1)+E(x1061,a2)+E(x1062,f18(x1061)) % 5.53/5.65 [113]~P1(x1131)+~P4(x1131)+~P2(x1132,a1)+~P8(x1132,f4(x1131))+P6(f11(x1131,x1132),x1131) % 5.53/5.65 [114]~P1(x1141)+P2(f13(x1142,x1141),x1141)+~P2(x1142,a1)+E(x1141,f3(x1142))+P2(f13(x1142,x1141),a1) % 5.53/5.65 [115]~P2(x1152,x1151)+~P6(x1151,a1)+~P8(x1152,f10(x1151,x1152))+E(x1151,a2)+E(x1152,f18(x1151)) % 5.53/5.65 [99]P2(x992,x991)+~P1(x991)+~P3(x992)+~P4(x991)+E(f4(f14(x991,x992)),f17(f4(x991))) % 5.53/5.65 [111]~P1(x1111)+~P4(x1111)+~P2(x1112,a1)+~P8(x1112,f4(x1111))+E(f4(f11(x1111,x1112)),x1112) % 5.53/5.65 [119]~P1(x1191)+P2(f13(x1192,x1191),x1191)+~P2(x1192,a1)+E(x1191,f3(x1192))+P8(f17(f13(x1192,x1191)),x1192) % 5.53/5.65 [91]~P2(x913,x911)+P8(x912,x913)+~E(x912,f18(x911))+~P6(x911,a1)+E(x911,a2) % 5.53/5.65 [108]P2(x1081,x1082)+~P2(x1083,a1)+~P2(x1081,a1)+~P8(f17(x1081),x1083)+~E(x1082,f3(x1083)) % 5.53/5.65 [87]~P1(x874)+~P3(x872)+~P2(x871,x873)+~E(x871,x872)+~E(x873,f15(x874,x872)) % 5.53/5.65 [88]~P1(x883)+~P3(x884)+~P2(x881,x882)+P3(x881)+~E(x882,f14(x883,x884)) % 5.53/5.65 [89]~P1(x893)+~P3(x894)+~P2(x891,x892)+P3(x891)+~E(x892,f15(x893,x894)) % 5.53/5.65 [97]~P1(x972)+~P3(x974)+~P2(x971,x973)+P2(x971,x972)+~E(x973,f15(x972,x974)) % 5.53/5.65 [110]~P4(x1101)+~P2(x1102,x1101)+P2(f12(x1101,x1102),x1101)+~P6(x1101,a1)+E(x1101,a2)+E(x1102,f19(x1101)) % 5.53/5.65 [117]~P4(x1171)+~P2(x1172,x1171)+~P6(x1171,a1)+~P8(f12(x1171,x1172),x1172)+E(x1171,a2)+E(x1172,f19(x1171)) % 5.53/5.65 [123]~P1(x1231)+~P2(x1232,a1)+~P2(f13(x1232,x1231),x1231)+E(x1231,f3(x1232))+~P2(f13(x1232,x1231),a1)+~P8(f17(f13(x1232,x1231)),x1232) % 5.53/5.65 [101]~P1(x1012)+~P1(x1011)+~P6(x1013,x1012)+~P6(x1011,x1013)+P6(x1011,x1012)+~P1(x1013) % 5.53/5.65 [118]~P8(x1181,x1183)+P8(x1181,x1182)+~P8(x1183,x1182)+~P2(x1182,a1)+~P2(x1183,a1)+~P2(x1181,a1) % 5.53/5.65 [96]~P4(x961)+~P2(x962,x961)+P8(x962,x963)+~E(x963,f19(x961))+~P6(x961,a1)+E(x961,a2) % 5.53/5.65 [120]~P1(x1201)+~P1(x1202)+~P3(x1203)+P2(f8(x1202,x1203,x1201),x1201)+~E(f8(x1202,x1203,x1201),x1203)+E(x1201,f15(x1202,x1203)) % 5.53/5.65 [121]~P1(x1211)+~P1(x1212)+~P3(x1213)+P2(f9(x1212,x1213,x1211),x1211)+E(x1211,f14(x1212,x1213))+P3(f9(x1212,x1213,x1211)) % 5.53/5.65 [122]~P1(x1221)+~P1(x1222)+~P3(x1223)+P2(f8(x1222,x1223,x1221),x1221)+E(x1221,f15(x1222,x1223))+P3(f8(x1222,x1223,x1221)) % 5.53/5.65 [124]~P1(x1241)+~P1(x1242)+~P3(x1243)+P2(f8(x1242,x1243,x1241),x1241)+P2(f8(x1242,x1243,x1241),x1242)+E(x1241,f15(x1242,x1243)) % 5.53/5.65 [84]~P1(x844)+~P3(x843)+~P3(x841)+P2(x841,x842)+~E(x841,x843)+~E(x842,f14(x844,x843)) % 5.53/5.65 [100]~P1(x1003)+~P3(x1002)+~P2(x1001,x1004)+E(x1001,x1002)+P2(x1001,x1003)+~E(x1004,f14(x1003,x1002)) % 5.53/5.65 [102]~P1(x1023)+~P3(x1024)+~P3(x1021)+~P2(x1021,x1023)+P2(x1021,x1022)+~E(x1022,f14(x1023,x1024)) % 5.53/5.65 [116]E(f18(x1162),f18(x1161))+~P6(x1161,a1)+~P6(x1162,a1)+~P2(f18(x1161),x1162)+~P2(f18(x1162),x1161)+E(x1161,a2)+E(x1162,a2) % 5.53/5.65 [125]~P1(x1251)+~P1(x1252)+~P3(x1253)+E(f9(x1252,x1253,x1251),x1253)+P2(f9(x1252,x1253,x1251),x1251)+P2(f9(x1252,x1253,x1251),x1252)+E(x1251,f14(x1252,x1253)) % 5.53/5.65 [126]~P1(x1261)+~P1(x1262)+~P3(x1263)+~E(f9(x1262,x1263,x1261),x1263)+~P2(f9(x1262,x1263,x1261),x1261)+E(x1261,f14(x1262,x1263))+~P3(f9(x1262,x1263,x1261)) % 5.53/5.65 [127]~P1(x1271)+~P1(x1272)+~P3(x1273)+~P2(f9(x1272,x1273,x1271),x1271)+~P2(f9(x1272,x1273,x1271),x1272)+E(x1271,f14(x1272,x1273))+~P3(f9(x1272,x1273,x1271)) % 5.53/5.65 [103]~P1(x1034)+~P3(x1032)+~P3(x1031)+~P2(x1031,x1034)+E(x1031,x1032)+P2(x1031,x1033)+~E(x1033,f15(x1034,x1032)) % 5.53/5.65 [128]~P1(x1281)+~P1(x1282)+~P3(x1283)+E(f8(x1282,x1283,x1281),x1283)+~P2(f8(x1282,x1283,x1281),x1281)+~P2(f8(x1282,x1283,x1281),x1282)+E(x1281,f15(x1282,x1283))+~P3(f8(x1282,x1283,x1281)) % 5.53/5.65 %EqnAxiom % 5.53/5.65 [1]E(x11,x11) % 5.53/5.65 [2]E(x22,x21)+~E(x21,x22) % 5.53/5.65 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 5.53/5.65 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 5.53/5.65 [5]~E(x51,x52)+E(f4(x51),f4(x52)) % 5.53/5.65 [6]~E(x61,x62)+E(f14(x61,x63),f14(x62,x63)) % 5.53/5.65 [7]~E(x71,x72)+E(f14(x73,x71),f14(x73,x72)) % 5.53/5.65 [8]~E(x81,x82)+E(f9(x81,x83,x84),f9(x82,x83,x84)) % 5.53/5.65 [9]~E(x91,x92)+E(f9(x93,x91,x94),f9(x93,x92,x94)) % 5.53/5.65 [10]~E(x101,x102)+E(f9(x103,x104,x101),f9(x103,x104,x102)) % 5.53/5.65 [11]~E(x111,x112)+E(f17(x111),f17(x112)) % 5.53/5.65 [12]~E(x121,x122)+E(f10(x121,x123),f10(x122,x123)) % 5.53/5.65 [13]~E(x131,x132)+E(f10(x133,x131),f10(x133,x132)) % 5.53/5.65 [14]~E(x141,x142)+E(f5(x141),f5(x142)) % 5.53/5.66 [15]~E(x151,x152)+E(f8(x151,x153,x154),f8(x152,x153,x154)) % 5.53/5.66 [16]~E(x161,x162)+E(f8(x163,x161,x164),f8(x163,x162,x164)) % 5.53/5.66 [17]~E(x171,x172)+E(f8(x173,x174,x171),f8(x173,x174,x172)) % 5.53/5.66 [18]~E(x181,x182)+E(f6(x181),f6(x182)) % 5.53/5.66 [19]~E(x191,x192)+E(f18(x191),f18(x192)) % 5.53/5.66 [20]~E(x201,x202)+E(f7(x201,x203),f7(x202,x203)) % 5.53/5.66 [21]~E(x211,x212)+E(f7(x213,x211),f7(x213,x212)) % 5.53/5.66 [22]~E(x221,x222)+E(f13(x221,x223),f13(x222,x223)) % 5.53/5.66 [23]~E(x231,x232)+E(f13(x233,x231),f13(x233,x232)) % 5.53/5.66 [24]~E(x241,x242)+E(f15(x241,x243),f15(x242,x243)) % 5.53/5.66 [25]~E(x251,x252)+E(f15(x253,x251),f15(x253,x252)) % 5.53/5.66 [26]~E(x261,x262)+E(f12(x261,x263),f12(x262,x263)) % 5.53/5.66 [27]~E(x271,x272)+E(f12(x273,x271),f12(x273,x272)) % 5.53/5.66 [28]~E(x281,x282)+E(f11(x281,x283),f11(x282,x283)) % 5.53/5.66 [29]~E(x291,x292)+E(f11(x293,x291),f11(x293,x292)) % 5.53/5.66 [30]~E(x301,x302)+E(f19(x301),f19(x302)) % 5.53/5.66 [31]~P1(x311)+P1(x312)+~E(x311,x312) % 5.53/5.66 [32]~P4(x321)+P4(x322)+~E(x321,x322) % 5.53/5.66 [33]~P5(x331)+P5(x332)+~E(x331,x332) % 5.53/5.66 [34]P2(x342,x343)+~E(x341,x342)+~P2(x341,x343) % 5.53/5.66 [35]P2(x353,x352)+~E(x351,x352)+~P2(x353,x351) % 5.53/5.66 [36]P6(x362,x363)+~E(x361,x362)+~P6(x361,x363) % 5.53/5.66 [37]P6(x373,x372)+~E(x371,x372)+~P6(x373,x371) % 5.53/5.66 [38]~P3(x381)+P3(x382)+~E(x381,x382) % 5.53/5.66 [39]P8(x392,x393)+~E(x391,x392)+~P8(x391,x393) % 5.53/5.66 [40]P8(x403,x402)+~E(x401,x402)+~P8(x403,x401) % 5.53/5.66 [41]P7(x412,x413)+~E(x411,x412)+~P7(x411,x413) % 5.53/5.66 [42]P7(x423,x422)+~E(x421,x422)+~P7(x423,x421) % 5.53/5.66 % 5.53/5.66 %------------------------------------------- % 5.53/5.66 cnf(129,plain, % 5.53/5.66 (P1(a2)), % 5.53/5.66 inference(equality_inference,[],[48])). % 5.53/5.66 cnf(132,plain, % 5.53/5.66 (~P2(x1321,a2)), % 5.53/5.66 inference(equality_inference,[],[55])). % 5.53/5.66 cnf(133,plain, % 5.53/5.66 (P1(f3(x1331))+~P2(x1331,a1)), % 5.53/5.66 inference(equality_inference,[],[62])). % 5.53/5.66 cnf(139,plain, % 5.53/5.66 (~P2(x1391,f3(x1392))+P2(x1391,a1)+~P2(x1392,a1)), % 5.53/5.66 inference(equality_inference,[],[86])). % 5.53/5.66 cnf(143,plain, % 5.53/5.66 (~P2(x1431,f3(x1432))+P8(f17(x1431),x1432)+~P2(x1432,a1)), % 5.53/5.66 inference(equality_inference,[],[95])). % 5.53/5.66 cnf(152,plain, % 5.53/5.66 (P1(f3(a16))), % 5.53/5.66 inference(scs_inference,[],[46,133])). % 5.53/5.66 cnf(159,plain, % 5.53/5.66 (~P2(x1591,a2)), % 5.53/5.66 inference(rename_variables,[],[132])). % 5.53/5.66 cnf(167,plain, % 5.53/5.66 (P8(f17(x1671),a16)+~P2(x1671,f3(a16))), % 5.53/5.66 inference(scs_inference,[],[43,132,159,129,45,46,133,66,53,35,92,105,83,143])). % 5.53/5.66 cnf(1225,plain, % 5.53/5.66 (P8(f17(f5(f3(a16))),a16)), % 5.53/5.66 inference(scs_inference,[],[47,152,167,58])). % 5.53/5.66 cnf(1226,plain, % 5.53/5.66 (~P2(f5(f3(a16)),a1)), % 5.53/5.66 inference(scs_inference,[],[1225,76])). % 5.53/5.66 cnf(1259,plain, % 5.53/5.66 ($false), % 5.53/5.66 inference(scs_inference,[],[46,47,152,1226,139,58]), % 5.53/5.66 ['proof']). % 5.53/5.66 % SZS output end Proof % 5.53/5.66 % Total time :5.010000s %------------------------------------------------------------------------------