%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM561+2 : 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 : n029.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:25:03 EDT 2024 % Result : Theorem 0.53s 0.68s % Output : CNFRefutation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NUM561+2 : 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.32 % Computer : n029.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Sun Jun 23 00:39:24 EDT 2024 % 0.12/0.32 % CPUTime : % 0.49/0.56 start to proof:theBenchmark % 0.53/0.66 %------------------------------------------- % 0.53/0.66 % File :CSE---1.7 % 0.53/0.66 % Problem :theBenchmark % 0.53/0.66 % Transform :cnf % 0.53/0.66 % Format :tptp:raw % 0.53/0.66 % Command :java -jar mcs_scs.jar %d %s % 0.53/0.66 % 0.53/0.66 % Result :Theorem 0.020000s % 0.53/0.66 % Output :CNFRefutation 0.020000s % 0.53/0.66 %------------------------------------------- % 0.53/0.67 %------------------------------------------------------------------------------ % 0.53/0.67 % File : NUM561+2 : TPTP v8.2.0. Released v4.0.0. % 0.53/0.67 % Domain : Number Theory % 0.53/0.67 % Problem : Ramsey's Infinite Theorem 14, 01 expansion % 0.53/0.67 % Version : Especial. % 0.53/0.67 % English : % 0.53/0.67 % 0.53/0.67 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 0.53/0.67 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 0.53/0.67 % Source : [Pas08] % 0.53/0.67 % Names : ramsey_14.01 [Pas08] % 0.53/0.67 % 0.53/0.67 % Status : Theorem % 0.53/0.67 % Rating : 0.11 v8.2.0, 0.08 v8.1.0, 0.03 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.1.0, 0.13 v6.0.0, 0.09 v5.5.0, 0.11 v5.4.0, 0.14 v5.3.0, 0.19 v5.2.0, 0.15 v5.1.0, 0.24 v5.0.0, 0.29 v4.1.0, 0.35 v4.0.1, 0.70 v4.0.0 % 0.53/0.67 % Syntax : Number of formulae : 71 ( 5 unt; 10 def) % 0.53/0.67 % Number of atoms : 271 ( 43 equ) % 0.53/0.67 % Maximal formula atoms : 8 ( 3 avg) % 0.53/0.67 % Number of connectives : 218 ( 18 ~; 5 |; 77 &) % 0.53/0.67 % ( 21 <=>; 97 =>; 0 <=; 0 <~>) % 0.53/0.67 % Maximal formula depth : 12 ( 5 avg) % 0.53/0.67 % Maximal term depth : 4 ( 1 avg) % 0.53/0.67 % Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty) % 0.53/0.67 % Number of functors : 17 ( 17 usr; 5 con; 0-2 aty) % 0.53/0.67 % Number of variables : 129 ( 122 !; 7 ?) % 0.53/0.67 % SPC : FOF_THM_RFO_SEQ % 0.53/0.67 % 0.53/0.67 % Comments : Problem generated by the SAD system [VLP07] % 0.53/0.67 %------------------------------------------------------------------------------ % 0.53/0.67 fof(mSetSort,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aSet0(W0) % 0.53/0.67 => $true ) ). % 0.53/0.67 % 0.53/0.67 fof(mElmSort,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aElement0(W0) % 0.53/0.67 => $true ) ). % 0.53/0.67 % 0.53/0.67 fof(mEOfElem,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aSet0(W0) % 0.53/0.67 => ! [W1] : % 0.53/0.67 ( aElementOf0(W1,W0) % 0.53/0.67 => aElement0(W1) ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mFinRel,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aSet0(W0) % 0.53/0.67 => ( isFinite0(W0) % 0.53/0.67 => $true ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mDefEmp,definition, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( W0 = slcrc0 % 0.53/0.67 <=> ( aSet0(W0) % 0.53/0.67 & ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mEmpFin,axiom, % 0.53/0.67 isFinite0(slcrc0) ). % 0.53/0.67 % 0.53/0.67 fof(mCntRel,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aSet0(W0) % 0.53/0.67 => ( isCountable0(W0) % 0.53/0.67 => $true ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mCountNFin,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( ( aSet0(W0) % 0.53/0.67 & isCountable0(W0) ) % 0.53/0.67 => ~ isFinite0(W0) ) ). % 0.53/0.67 % 0.53/0.67 fof(mCountNFin_01,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( ( aSet0(W0) % 0.53/0.67 & isCountable0(W0) ) % 0.53/0.67 => W0 != slcrc0 ) ). % 0.53/0.67 % 0.53/0.67 fof(mDefSub,definition, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aSet0(W0) % 0.53/0.67 => ! [W1] : % 0.53/0.67 ( aSubsetOf0(W1,W0) % 0.53/0.67 <=> ( aSet0(W1) % 0.53/0.67 & ! [W2] : % 0.53/0.67 ( aElementOf0(W2,W1) % 0.53/0.67 => aElementOf0(W2,W0) ) ) ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mSubFSet,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( ( aSet0(W0) % 0.53/0.67 & isFinite0(W0) ) % 0.53/0.67 => ! [W1] : % 0.53/0.67 ( aSubsetOf0(W1,W0) % 0.53/0.67 => isFinite0(W1) ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mSubRefl,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aSet0(W0) % 0.53/0.67 => aSubsetOf0(W0,W0) ) ). % 0.53/0.67 % 0.53/0.67 fof(mSubASymm,axiom, % 0.53/0.67 ! [W0,W1] : % 0.53/0.67 ( ( aSet0(W0) % 0.53/0.67 & aSet0(W1) ) % 0.53/0.67 => ( ( aSubsetOf0(W0,W1) % 0.53/0.67 & aSubsetOf0(W1,W0) ) % 0.53/0.67 => W0 = W1 ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mSubTrans,axiom, % 0.53/0.67 ! [W0,W1,W2] : % 0.53/0.67 ( ( aSet0(W0) % 0.53/0.67 & aSet0(W1) % 0.53/0.67 & aSet0(W2) ) % 0.53/0.67 => ( ( aSubsetOf0(W0,W1) % 0.53/0.67 & aSubsetOf0(W1,W2) ) % 0.53/0.67 => aSubsetOf0(W0,W2) ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mDefCons,definition, % 0.53/0.67 ! [W0,W1] : % 0.53/0.67 ( ( aSet0(W0) % 0.53/0.67 & aElement0(W1) ) % 0.53/0.67 => ! [W2] : % 0.53/0.67 ( W2 = sdtpldt0(W0,W1) % 0.53/0.67 <=> ( aSet0(W2) % 0.53/0.67 & ! [W3] : % 0.53/0.67 ( aElementOf0(W3,W2) % 0.53/0.67 <=> ( aElement0(W3) % 0.53/0.67 & ( aElementOf0(W3,W0) % 0.53/0.67 | W3 = W1 ) ) ) ) ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mDefDiff,definition, % 0.53/0.67 ! [W0,W1] : % 0.53/0.67 ( ( aSet0(W0) % 0.53/0.67 & aElement0(W1) ) % 0.53/0.67 => ! [W2] : % 0.53/0.67 ( W2 = sdtmndt0(W0,W1) % 0.53/0.67 <=> ( aSet0(W2) % 0.53/0.67 & ! [W3] : % 0.53/0.67 ( aElementOf0(W3,W2) % 0.53/0.67 <=> ( aElement0(W3) % 0.53/0.67 & aElementOf0(W3,W0) % 0.53/0.67 & W3 != W1 ) ) ) ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mConsDiff,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aSet0(W0) % 0.53/0.67 => ! [W1] : % 0.53/0.67 ( aElementOf0(W1,W0) % 0.53/0.67 => sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mDiffCons,axiom, % 0.53/0.67 ! [W0,W1] : % 0.53/0.67 ( ( aElement0(W0) % 0.53/0.67 & aSet0(W1) ) % 0.53/0.67 => ( ~ aElementOf0(W0,W1) % 0.53/0.67 => sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mCConsSet,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aElement0(W0) % 0.53/0.67 => ! [W1] : % 0.53/0.67 ( ( aSet0(W1) % 0.53/0.67 & isCountable0(W1) ) % 0.53/0.67 => isCountable0(sdtpldt0(W1,W0)) ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mCDiffSet,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aElement0(W0) % 0.53/0.67 => ! [W1] : % 0.53/0.67 ( ( aSet0(W1) % 0.53/0.67 & isCountable0(W1) ) % 0.53/0.67 => isCountable0(sdtmndt0(W1,W0)) ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mFConsSet,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aElement0(W0) % 0.53/0.67 => ! [W1] : % 0.53/0.67 ( ( aSet0(W1) % 0.53/0.67 & isFinite0(W1) ) % 0.53/0.67 => isFinite0(sdtpldt0(W1,W0)) ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mFDiffSet,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aElement0(W0) % 0.53/0.67 => ! [W1] : % 0.53/0.67 ( ( aSet0(W1) % 0.53/0.67 & isFinite0(W1) ) % 0.53/0.67 => isFinite0(sdtmndt0(W1,W0)) ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mNATSet,axiom, % 0.53/0.67 ( aSet0(szNzAzT0) % 0.53/0.67 & isCountable0(szNzAzT0) ) ). % 0.53/0.67 % 0.53/0.67 fof(mZeroNum,axiom, % 0.53/0.67 aElementOf0(sz00,szNzAzT0) ). % 0.53/0.67 % 0.53/0.67 fof(mSuccNum,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aElementOf0(W0,szNzAzT0) % 0.53/0.67 => ( aElementOf0(szszuzczcdt0(W0),szNzAzT0) % 0.53/0.67 & szszuzczcdt0(W0) != sz00 ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mSuccEquSucc,axiom, % 0.53/0.67 ! [W0,W1] : % 0.53/0.67 ( ( aElementOf0(W0,szNzAzT0) % 0.53/0.67 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.67 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 0.53/0.67 => W0 = W1 ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mNatExtra,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aElementOf0(W0,szNzAzT0) % 0.53/0.67 => ( W0 = sz00 % 0.53/0.67 | ? [W1] : % 0.53/0.67 ( aElementOf0(W1,szNzAzT0) % 0.53/0.67 & W0 = szszuzczcdt0(W1) ) ) ) ). % 0.53/0.67 % 0.53/0.67 fof(mNatNSucc,axiom, % 0.53/0.67 ! [W0] : % 0.53/0.67 ( aElementOf0(W0,szNzAzT0) % 0.53/0.67 => W0 != szszuzczcdt0(W0) ) ). % 0.53/0.67 % 0.53/0.67 fof(mLessRel,axiom, % 0.53/0.67 ! [W0,W1] : % 0.53/0.67 ( ( aElementOf0(W0,szNzAzT0) % 0.53/0.67 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.67 => ( sdtlseqdt0(W0,W1) % 0.53/0.67 => $true ) ) ). % 0.53/0.67 % 0.53/0.68 fof(mZeroLess,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 => sdtlseqdt0(sz00,W0) ) ). % 0.53/0.68 % 0.53/0.68 fof(mNoScLessZr,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 => ~ sdtlseqdt0(szszuzczcdt0(W0),sz00) ) ). % 0.53/0.68 % 0.53/0.68 fof(mSuccLess,axiom, % 0.53/0.68 ! [W0,W1] : % 0.53/0.68 ( ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.68 => ( sdtlseqdt0(W0,W1) % 0.53/0.68 <=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mLessSucc,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 => sdtlseqdt0(W0,szszuzczcdt0(W0)) ) ). % 0.53/0.68 % 0.53/0.68 fof(mLessRefl,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 => sdtlseqdt0(W0,W0) ) ). % 0.53/0.68 % 0.53/0.68 fof(mLessASymm,axiom, % 0.53/0.68 ! [W0,W1] : % 0.53/0.68 ( ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.68 => ( ( sdtlseqdt0(W0,W1) % 0.53/0.68 & sdtlseqdt0(W1,W0) ) % 0.53/0.68 => W0 = W1 ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mLessTrans,axiom, % 0.53/0.68 ! [W0,W1,W2] : % 0.53/0.68 ( ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 & aElementOf0(W1,szNzAzT0) % 0.53/0.68 & aElementOf0(W2,szNzAzT0) ) % 0.53/0.68 => ( ( sdtlseqdt0(W0,W1) % 0.53/0.68 & sdtlseqdt0(W1,W2) ) % 0.53/0.68 => sdtlseqdt0(W0,W2) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mLessTotal,axiom, % 0.53/0.68 ! [W0,W1] : % 0.53/0.68 ( ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.68 => ( sdtlseqdt0(W0,W1) % 0.53/0.68 | sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mIHSort,axiom, % 0.53/0.68 ! [W0,W1] : % 0.53/0.68 ( ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.68 => ( iLess0(W0,W1) % 0.53/0.68 => $true ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mIH,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 0.53/0.68 % 0.53/0.68 fof(mCardS,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aSet0(W0) % 0.53/0.68 => aElement0(sbrdtbr0(W0)) ) ). % 0.53/0.68 % 0.53/0.68 fof(mCardNum,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aSet0(W0) % 0.53/0.68 => ( aElementOf0(sbrdtbr0(W0),szNzAzT0) % 0.53/0.68 <=> isFinite0(W0) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mCardEmpty,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aSet0(W0) % 0.53/0.68 => ( sbrdtbr0(W0) = sz00 % 0.53/0.68 <=> W0 = slcrc0 ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mCardCons,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( ( aSet0(W0) % 0.53/0.68 & isFinite0(W0) ) % 0.53/0.68 => ! [W1] : % 0.53/0.68 ( aElement0(W1) % 0.53/0.68 => ( ~ aElementOf0(W1,W0) % 0.53/0.68 => sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mCardDiff,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aSet0(W0) % 0.53/0.68 => ! [W1] : % 0.53/0.68 ( ( isFinite0(W0) % 0.53/0.68 & aElementOf0(W1,W0) ) % 0.53/0.68 => szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mCardSub,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aSet0(W0) % 0.53/0.68 => ! [W1] : % 0.53/0.68 ( ( isFinite0(W0) % 0.53/0.68 & aSubsetOf0(W1,W0) ) % 0.53/0.68 => sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mCardSubEx,axiom, % 0.53/0.68 ! [W0,W1] : % 0.53/0.68 ( ( aSet0(W0) % 0.53/0.68 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.68 => ( ( isFinite0(W0) % 0.53/0.68 & sdtlseqdt0(W1,sbrdtbr0(W0)) ) % 0.53/0.68 => ? [W2] : % 0.53/0.68 ( aSubsetOf0(W2,W0) % 0.53/0.68 & sbrdtbr0(W2) = W1 ) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mDefMin,definition, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( ( aSubsetOf0(W0,szNzAzT0) % 0.53/0.68 & W0 != slcrc0 ) % 0.53/0.68 => ! [W1] : % 0.53/0.68 ( W1 = szmzizndt0(W0) % 0.53/0.68 <=> ( aElementOf0(W1,W0) % 0.53/0.68 & ! [W2] : % 0.53/0.68 ( aElementOf0(W2,W0) % 0.53/0.68 => sdtlseqdt0(W1,W2) ) ) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mDefMax,definition, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( ( aSubsetOf0(W0,szNzAzT0) % 0.53/0.68 & isFinite0(W0) % 0.53/0.68 & W0 != slcrc0 ) % 0.53/0.68 => ! [W1] : % 0.53/0.68 ( W1 = szmzazxdt0(W0) % 0.53/0.68 <=> ( aElementOf0(W1,W0) % 0.53/0.68 & ! [W2] : % 0.53/0.68 ( aElementOf0(W2,W0) % 0.53/0.68 => sdtlseqdt0(W2,W1) ) ) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mMinMin,axiom, % 0.53/0.68 ! [W0,W1] : % 0.53/0.68 ( ( aSubsetOf0(W0,szNzAzT0) % 0.53/0.68 & aSubsetOf0(W1,szNzAzT0) % 0.53/0.68 & W0 != slcrc0 % 0.53/0.68 & W1 != slcrc0 ) % 0.53/0.68 => ( ( aElementOf0(szmzizndt0(W0),W1) % 0.53/0.68 & aElementOf0(szmzizndt0(W1),W0) ) % 0.53/0.68 => szmzizndt0(W0) = szmzizndt0(W1) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mDefSeg,definition, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 => ! [W1] : % 0.53/0.68 ( W1 = slbdtrb0(W0) % 0.53/0.68 <=> ( aSet0(W1) % 0.53/0.68 & ! [W2] : % 0.53/0.68 ( aElementOf0(W2,W1) % 0.53/0.68 <=> ( aElementOf0(W2,szNzAzT0) % 0.53/0.68 & sdtlseqdt0(szszuzczcdt0(W2),W0) ) ) ) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mSegFin,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 => isFinite0(slbdtrb0(W0)) ) ). % 0.53/0.68 % 0.53/0.68 fof(mSegZero,axiom, % 0.53/0.68 slbdtrb0(sz00) = slcrc0 ). % 0.53/0.68 % 0.53/0.68 fof(mSegSucc,axiom, % 0.53/0.68 ! [W0,W1] : % 0.53/0.68 ( ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.68 => ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1))) % 0.53/0.68 <=> ( aElementOf0(W0,slbdtrb0(W1)) % 0.53/0.68 | W0 = W1 ) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mSegLess,axiom, % 0.53/0.68 ! [W0,W1] : % 0.53/0.68 ( ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.68 => ( sdtlseqdt0(W0,W1) % 0.53/0.68 <=> aSubsetOf0(slbdtrb0(W0),slbdtrb0(W1)) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mFinSubSeg,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( ( aSubsetOf0(W0,szNzAzT0) % 0.53/0.68 & isFinite0(W0) ) % 0.53/0.68 => ? [W1] : % 0.53/0.68 ( aElementOf0(W1,szNzAzT0) % 0.53/0.68 & aSubsetOf0(W0,slbdtrb0(W1)) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mCardSeg,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 => sbrdtbr0(slbdtrb0(W0)) = W0 ) ). % 0.53/0.68 % 0.53/0.68 fof(mDefSel,definition, % 0.53/0.68 ! [W0,W1] : % 0.53/0.68 ( ( aSet0(W0) % 0.53/0.68 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.68 => ! [W2] : % 0.53/0.68 ( W2 = slbdtsldtrb0(W0,W1) % 0.53/0.68 <=> ( aSet0(W2) % 0.53/0.68 & ! [W3] : % 0.53/0.68 ( aElementOf0(W3,W2) % 0.53/0.68 <=> ( aSubsetOf0(W3,W0) % 0.53/0.68 & sbrdtbr0(W3) = W1 ) ) ) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mSelFSet,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( ( aSet0(W0) % 0.53/0.68 & isFinite0(W0) ) % 0.53/0.68 => ! [W1] : % 0.53/0.68 ( aElementOf0(W1,szNzAzT0) % 0.53/0.68 => isFinite0(slbdtsldtrb0(W0,W1)) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mSelNSet,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( ( aSet0(W0) % 0.53/0.68 & ~ isFinite0(W0) ) % 0.53/0.68 => ! [W1] : % 0.53/0.68 ( aElementOf0(W1,szNzAzT0) % 0.53/0.68 => slbdtsldtrb0(W0,W1) != slcrc0 ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mSelCSet,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( ( aSet0(W0) % 0.53/0.68 & isCountable0(W0) ) % 0.53/0.68 => ! [W1] : % 0.53/0.68 ( ( aElementOf0(W1,szNzAzT0) % 0.53/0.68 & W1 != sz00 ) % 0.53/0.68 => isCountable0(slbdtsldtrb0(W0,W1)) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mSelSub,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aElementOf0(W0,szNzAzT0) % 0.53/0.68 => ! [W1,W2] : % 0.53/0.68 ( ( aSet0(W1) % 0.53/0.68 & aSet0(W2) % 0.53/0.68 & W0 != sz00 ) % 0.53/0.68 => ( ( aSubsetOf0(slbdtsldtrb0(W1,W0),slbdtsldtrb0(W2,W0)) % 0.53/0.68 & slbdtsldtrb0(W1,W0) != slcrc0 ) % 0.53/0.68 => aSubsetOf0(W1,W2) ) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mSelExtra,axiom, % 0.53/0.68 ! [W0,W1] : % 0.53/0.68 ( ( aSet0(W0) % 0.53/0.68 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.68 => ! [W2] : % 0.53/0.68 ( ( aSubsetOf0(W2,slbdtsldtrb0(W0,W1)) % 0.53/0.68 & isFinite0(W2) ) % 0.53/0.68 => ? [W3] : % 0.53/0.68 ( aSubsetOf0(W3,W0) % 0.53/0.68 & isFinite0(W3) % 0.53/0.68 & aSubsetOf0(W2,slbdtsldtrb0(W3,W1)) ) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mFunSort,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aFunction0(W0) % 0.53/0.68 => $true ) ). % 0.53/0.68 % 0.53/0.68 fof(mDomSet,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aFunction0(W0) % 0.53/0.68 => aSet0(szDzozmdt0(W0)) ) ). % 0.53/0.68 % 0.53/0.68 fof(mImgElm,axiom, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aFunction0(W0) % 0.53/0.68 => ! [W1] : % 0.53/0.68 ( aElementOf0(W1,szDzozmdt0(W0)) % 0.53/0.68 => aElement0(sdtlpdtrp0(W0,W1)) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mDefPtt,definition, % 0.53/0.68 ! [W0,W1] : % 0.53/0.68 ( ( aFunction0(W0) % 0.53/0.68 & aElement0(W1) ) % 0.53/0.68 => ! [W2] : % 0.53/0.68 ( W2 = sdtlbdtrb0(W0,W1) % 0.53/0.68 <=> ( aSet0(W2) % 0.53/0.68 & ! [W3] : % 0.53/0.68 ( aElementOf0(W3,W2) % 0.53/0.68 <=> ( aElementOf0(W3,szDzozmdt0(W0)) % 0.53/0.68 & sdtlpdtrp0(W0,W3) = W1 ) ) ) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(mPttSet,axiom, % 0.53/0.68 ! [W0,W1] : % 0.53/0.68 ( ( aFunction0(W0) % 0.53/0.68 & aElement0(W1) ) % 0.53/0.68 => aSubsetOf0(sdtlbdtrb0(W0,W1),szDzozmdt0(W0)) ) ). % 0.53/0.68 % 0.53/0.68 fof(mDefSImg,definition, % 0.53/0.68 ! [W0] : % 0.53/0.68 ( aFunction0(W0) % 0.53/0.68 => ! [W1] : % 0.53/0.68 ( aSubsetOf0(W1,szDzozmdt0(W0)) % 0.53/0.68 => ! [W2] : % 0.53/0.68 ( W2 = sdtlcdtrc0(W0,W1) % 0.53/0.68 <=> ( aSet0(W2) % 0.53/0.68 & ! [W3] : % 0.53/0.68 ( aElementOf0(W3,W2) % 0.53/0.68 <=> ? [W4] : % 0.53/0.68 ( aElementOf0(W4,W1) % 0.53/0.68 & sdtlpdtrp0(W0,W4) = W3 ) ) ) ) ) ) ). % 0.53/0.68 % 0.53/0.68 fof(m__2911,hypothesis, % 0.53/0.68 aFunction0(xF) ). % 0.53/0.68 % 0.53/0.68 fof(m__2911_02,hypothesis, % 0.53/0.68 aElementOf0(xx,szDzozmdt0(xF)) ). % 0.53/0.68 % 0.53/0.68 fof(m__,conjecture, % 0.53/0.68 ( ? [W0] : % 0.53/0.68 ( aElementOf0(W0,szDzozmdt0(xF)) % 0.53/0.68 & sdtlpdtrp0(xF,W0) = sdtlpdtrp0(xF,xx) ) % 0.53/0.68 | aElementOf0(sdtlpdtrp0(xF,xx),sdtlcdtrc0(xF,szDzozmdt0(xF))) ) ). % 0.53/0.68 % 0.53/0.68 %------------------------------------------------------------------------------ % 0.53/0.68 %------------------------------------------- % 0.53/0.68 % Proof found % 0.53/0.68 % SZS status Theorem for theBenchmark % 0.53/0.68 % SZS output start Proof % 0.53/0.68 %ClaNum:201(EqnAxiom:72) % 0.53/0.68 %VarNum:953(SingletonVarNum:286) % 0.53/0.68 %MaxLitNum:8 % 0.53/0.68 %MaxfuncDepth:3 % 0.53/0.68 %SharedTerms:17 % 0.53/0.68 %goalClause: 80 128 % 0.53/0.68 %singleGoalClaCount:1 % 0.53/0.68 [74]P1(a27) % 0.53/0.68 [75]P5(a25) % 0.53/0.68 [76]P6(a27) % 0.53/0.68 [77]P2(a29) % 0.53/0.68 [78]P3(a1,a27) % 0.53/0.68 [73]E(f2(a1),a25) % 0.53/0.68 [79]P3(a33,f28(a29)) % 0.53/0.68 [80]~P3(f3(a29,a33),f4(a29,f28(a29))) % 0.53/0.68 [81]P1(x811)+~E(x811,a25) % 0.53/0.68 [88]~P1(x881)+P7(x881,x881) % 0.53/0.68 [95]~P3(x951,a27)+P9(a1,x951) % 0.53/0.68 [101]P9(x1011,x1011)+~P3(x1011,a27) % 0.53/0.68 [85]~P2(x851)+P1(f28(x851)) % 0.53/0.68 [86]~P1(x861)+P4(f5(x861)) % 0.53/0.68 [90]~P3(x901,a27)+~E(f30(x901),a1) % 0.53/0.68 [91]~P3(x911,a27)+~E(f30(x911),x911) % 0.53/0.68 [93]~P3(x931,a27)+P5(f2(x931)) % 0.53/0.68 [102]~P3(x1021,a27)+P3(f30(x1021),a27) % 0.53/0.68 [103]~P3(x1031,a27)+P9(x1031,f30(x1031)) % 0.53/0.68 [104]~P3(x1041,a27)+P8(x1041,f30(x1041)) % 0.53/0.68 [113]~P3(x1131,a27)+~P9(f30(x1131),a1) % 0.53/0.68 [128]~P3(x1281,f28(a29))+~E(f3(a29,x1281),f3(a29,a33)) % 0.53/0.68 [94]~P3(x941,a27)+E(f5(f2(x941)),x941) % 0.53/0.68 [89]~P3(x892,x891)+~E(x891,a25) % 0.53/0.68 [84]~P1(x841)+~P6(x841)+~E(x841,a25) % 0.53/0.68 [87]~P5(x871)+~P6(x871)+~P1(x871) % 0.53/0.68 [82]~P1(x821)+~E(x821,a25)+E(f5(x821),a1) % 0.53/0.68 [83]~P1(x831)+E(x831,a25)+~E(f5(x831),a1) % 0.53/0.68 [92]~P1(x921)+P3(f6(x921),x921)+E(x921,a25) % 0.53/0.68 [98]~P1(x981)+~P5(x981)+P3(f5(x981),a27) % 0.53/0.68 [105]~P3(x1051,a27)+E(x1051,a1)+P3(f14(x1051),a27) % 0.53/0.68 [106]~P1(x1061)+P5(x1061)+~P3(f5(x1061),a27) % 0.53/0.68 [112]~P5(x1121)+~P7(x1121,a27)+P3(f7(x1121),a27) % 0.53/0.68 [96]~P3(x961,a27)+E(x961,a1)+E(f30(f14(x961)),x961) % 0.53/0.68 [122]~P5(x1221)+~P7(x1221,a27)+P7(x1221,f2(f7(x1221))) % 0.53/0.68 [99]~P7(x991,x992)+P1(x991)+~P1(x992) % 0.53/0.68 [100]~P3(x1001,x1002)+P4(x1001)+~P1(x1002) % 0.53/0.68 [97]P1(x971)+~P3(x972,a27)+~E(x971,f2(x972)) % 0.53/0.68 [123]~P4(x1232)+~P2(x1231)+P7(f22(x1231,x1232),f28(x1231)) % 0.53/0.68 [138]~P2(x1381)+~P3(x1382,f28(x1381))+P4(f3(x1381,x1382)) % 0.53/0.68 [140]~P1(x1401)+~P3(x1402,x1401)+E(f23(f24(x1401,x1402),x1402),x1401) % 0.53/0.68 [107]~P5(x1072)+~P7(x1071,x1072)+P5(x1071)+~P1(x1072) % 0.53/0.68 [111]P3(x1112,x1111)+~E(x1112,f31(x1111))+~P7(x1111,a27)+E(x1111,a25) % 0.53/0.68 [115]~P1(x1151)+~P4(x1152)+~P5(x1151)+P5(f23(x1151,x1152)) % 0.53/0.68 [116]~P1(x1161)+~P4(x1162)+~P5(x1161)+P5(f24(x1161,x1162)) % 0.53/0.68 [117]~P1(x1171)+~P4(x1172)+~P6(x1171)+P6(f23(x1171,x1172)) % 0.53/0.68 [118]~P1(x1181)+~P4(x1182)+~P6(x1181)+P6(f24(x1181,x1182)) % 0.53/0.68 [119]~P1(x1191)+P5(x1191)+~P3(x1192,a27)+~E(f26(x1191,x1192),a25) % 0.53/0.68 [121]E(x1211,x1212)+~E(f30(x1211),f30(x1212))+~P3(x1212,a27)+~P3(x1211,a27) % 0.53/0.68 [126]~P1(x1262)+~P5(x1262)+~P7(x1261,x1262)+P9(f5(x1261),f5(x1262)) % 0.53/0.68 [130]~P1(x1301)+~P5(x1301)+~P3(x1302,a27)+P5(f26(x1301,x1302)) % 0.53/0.68 [137]~P1(x1371)+~P1(x1372)+P7(x1371,x1372)+P3(f15(x1372,x1371),x1371) % 0.53/0.68 [144]P9(x1441,x1442)+P9(f30(x1442),x1441)+~P3(x1442,a27)+~P3(x1441,a27) % 0.53/0.68 [156]~P9(x1561,x1562)+~P3(x1562,a27)+~P3(x1561,a27)+P7(f2(x1561),f2(x1562)) % 0.53/0.68 [157]~P9(x1571,x1572)+~P3(x1572,a27)+~P3(x1571,a27)+P9(f30(x1571),f30(x1572)) % 0.53/0.68 [159]~P1(x1591)+~P1(x1592)+P7(x1591,x1592)+~P3(f15(x1592,x1591),x1592) % 0.53/0.68 [161]P9(x1611,x1612)+~P3(x1612,a27)+~P3(x1611,a27)+~P7(f2(x1611),f2(x1612)) % 0.53/0.68 [162]P9(x1621,x1622)+~P3(x1622,a27)+~P3(x1621,a27)+~P9(f30(x1621),f30(x1622)) % 0.53/0.68 [139]P3(x1392,x1391)+~P1(x1391)+~P4(x1392)+E(f24(f23(x1391,x1392),x1392),x1391) % 0.53/0.68 [147]~E(x1471,x1472)+~P3(x1472,a27)+~P3(x1471,a27)+P3(x1471,f2(f30(x1472))) % 0.53/0.68 [167]~P3(x1672,a27)+~P3(x1671,a27)+~P3(x1671,f2(x1672))+P3(x1671,f2(f30(x1672))) % 0.53/0.68 [166]~P1(x1661)+~P5(x1661)+~P3(x1662,x1661)+E(f30(f5(f24(x1661,x1662))),f5(x1661)) % 0.53/0.68 [134]~P1(x1342)+~P7(x1343,x1342)+P3(x1341,x1342)+~P3(x1341,x1343) % 0.53/0.68 [108]~P1(x1082)+~P4(x1083)+P1(x1081)+~E(x1081,f23(x1082,x1083)) % 0.53/0.68 [109]~P1(x1092)+~P4(x1093)+P1(x1091)+~E(x1091,f24(x1092,x1093)) % 0.53/0.68 [110]~P4(x1103)+~P2(x1102)+P1(x1101)+~E(x1101,f22(x1102,x1103)) % 0.53/0.68 [120]~P1(x1202)+P1(x1201)+~P3(x1203,a27)+~E(x1201,f26(x1202,x1203)) % 0.53/0.68 [127]~P3(x1271,x1272)+~P3(x1273,a27)+P3(x1271,a27)+~E(x1272,f2(x1273)) % 0.53/0.68 [136]~P2(x1362)+P1(x1361)+~P7(x1363,f28(x1362))+~E(x1361,f4(x1362,x1363)) % 0.53/0.68 [141]~P3(x1411,x1413)+~P3(x1412,a27)+P9(f30(x1411),x1412)+~E(x1413,f2(x1412)) % 0.53/0.68 [124]~P1(x1242)+~P1(x1241)+~P7(x1242,x1241)+~P7(x1241,x1242)+E(x1241,x1242) % 0.53/0.68 [154]~P9(x1542,x1541)+~P9(x1541,x1542)+E(x1541,x1542)+~P3(x1542,a27)+~P3(x1541,a27) % 0.53/0.68 [114]~P5(x1141)+P3(x1142,x1141)+~E(x1142,f32(x1141))+~P7(x1141,a27)+E(x1141,a25) % 0.53/0.68 [133]~P1(x1332)+~P6(x1332)+~P3(x1331,a27)+E(x1331,a1)+P6(f26(x1332,x1331)) % 0.53/0.68 [158]~P3(x1582,x1581)+P3(f18(x1581,x1582),x1581)+~P7(x1581,a27)+E(x1581,a25)+E(x1582,f31(x1581)) % 0.53/0.68 [168]~P1(x1681)+~P5(x1681)+~P3(x1682,a27)+~P9(x1682,f5(x1681))+P7(f19(x1681,x1682),x1681) % 0.53/0.68 [170]~P1(x1701)+P3(f21(x1702,x1701),x1701)+~P3(x1702,a27)+E(x1701,f2(x1702))+P3(f21(x1702,x1701),a27) % 0.53/0.68 [171]~P3(x1712,x1711)+~P7(x1711,a27)+~P9(x1712,f18(x1711,x1712))+E(x1711,a25)+E(x1712,f31(x1711)) % 0.53/0.68 [146]P3(x1462,x1461)+~P1(x1461)+~P4(x1462)+~P5(x1461)+E(f5(f23(x1461,x1462)),f30(f5(x1461))) % 0.53/0.68 [165]~P1(x1651)+~P5(x1651)+~P3(x1652,a27)+~P9(x1652,f5(x1651))+E(f5(f19(x1651,x1652)),x1652) % 0.53/0.68 [172]E(x1721,x1722)+P3(x1721,f2(x1722))+~P3(x1722,a27)+~P3(x1721,a27)+~P3(x1721,f2(f30(x1722))) % 0.53/0.68 [177]~P1(x1771)+P3(f21(x1772,x1771),x1771)+~P3(x1772,a27)+E(x1771,f2(x1772))+P9(f30(f21(x1772,x1771)),x1772) % 0.53/0.68 [135]~P3(x1353,x1351)+P9(x1352,x1353)+~E(x1352,f31(x1351))+~P7(x1351,a27)+E(x1351,a25) % 0.53/0.68 [160]P3(x1601,x1602)+~P3(x1603,a27)+~P3(x1601,a27)+~P9(f30(x1601),x1603)+~E(x1602,f2(x1603)) % 0.53/0.69 [179]~P1(x1791)+~P5(x1793)+~P3(x1792,a27)+~P7(x1793,f26(x1791,x1792))+P5(f8(x1791,x1792,x1793)) % 0.53/0.69 [180]~P1(x1801)+~P5(x1803)+~P3(x1802,a27)+~P7(x1803,f26(x1801,x1802))+P7(f8(x1801,x1802,x1803),x1801) % 0.53/0.69 [192]~P1(x1922)+~P5(x1921)+~P3(x1923,a27)+~P7(x1921,f26(x1922,x1923))+P7(x1921,f26(f8(x1922,x1923,x1921),x1923)) % 0.53/0.69 [129]~P1(x1294)+~P4(x1292)+~P3(x1291,x1293)+~E(x1291,x1292)+~E(x1293,f24(x1294,x1292)) % 0.53/0.69 [131]~P1(x1313)+~P4(x1314)+~P3(x1311,x1312)+P4(x1311)+~E(x1312,f23(x1313,x1314)) % 0.53/0.69 [132]~P1(x1323)+~P4(x1324)+~P3(x1321,x1322)+P4(x1321)+~E(x1322,f24(x1323,x1324)) % 0.53/0.69 [143]~P1(x1432)+~P4(x1434)+~P3(x1431,x1433)+P3(x1431,x1432)+~E(x1433,f24(x1432,x1434)) % 0.53/0.69 [145]~P4(x1453)+~P2(x1451)+~P3(x1452,x1454)+E(f3(x1451,x1452),x1453)+~E(x1454,f22(x1451,x1453)) % 0.53/0.69 [149]~P1(x1494)+~P3(x1491,x1493)+~P3(x1492,a27)+E(f5(x1491),x1492)+~E(x1493,f26(x1494,x1492)) % 0.53/0.69 [151]~P4(x1514)+~P2(x1512)+~P3(x1511,x1513)+P3(x1511,f28(x1512))+~E(x1513,f22(x1512,x1514)) % 0.53/0.69 [155]~P1(x1552)+~P3(x1551,x1553)+P7(x1551,x1552)+~P3(x1554,a27)+~E(x1553,f26(x1552,x1554)) % 0.53/0.69 [197]~P2(x1971)+~P3(x1974,x1973)+~E(x1973,f4(x1971,x1972))+~P7(x1972,f28(x1971))+P3(f12(x1971,x1972,x1973,x1974),x1972) % 0.53/0.69 [198]~P2(x1981)+~P3(x1984,x1983)+~E(x1983,f4(x1981,x1982))+~P7(x1982,f28(x1981))+E(f3(x1981,f12(x1981,x1982,x1983,x1984)),x1984) % 0.53/0.69 [164]~P5(x1641)+~P3(x1642,x1641)+P3(f20(x1641,x1642),x1641)+~P7(x1641,a27)+E(x1641,a25)+E(x1642,f32(x1641)) % 0.53/0.69 [174]~P5(x1741)+~P3(x1742,x1741)+~P7(x1741,a27)+~P9(f20(x1741,x1742),x1742)+E(x1741,a25)+E(x1742,f32(x1741)) % 0.53/0.69 [184]~P1(x1841)+~P3(x1842,a27)+~P3(f21(x1842,x1841),x1841)+E(x1841,f2(x1842))+~P3(f21(x1842,x1841),a27)+~P9(f30(f21(x1842,x1841)),x1842) % 0.53/0.69 [150]~P1(x1502)+~P1(x1501)+~P7(x1503,x1502)+~P7(x1501,x1503)+P7(x1501,x1502)+~P1(x1503) % 0.53/0.69 [175]~P9(x1751,x1753)+P9(x1751,x1752)+~P9(x1753,x1752)+~P3(x1752,a27)+~P3(x1753,a27)+~P3(x1751,a27) % 0.53/0.69 [142]~P5(x1421)+~P3(x1422,x1421)+P9(x1422,x1423)+~E(x1423,f32(x1421))+~P7(x1421,a27)+E(x1421,a25) % 0.53/0.69 [181]~P1(x1811)+~P1(x1812)+~P4(x1813)+P3(f16(x1812,x1813,x1811),x1811)+~E(f16(x1812,x1813,x1811),x1813)+E(x1811,f24(x1812,x1813)) % 0.53/0.69 [182]~P1(x1821)+~P1(x1822)+~P4(x1823)+P3(f17(x1822,x1823,x1821),x1821)+E(x1821,f23(x1822,x1823))+P4(f17(x1822,x1823,x1821)) % 0.53/0.69 [183]~P1(x1831)+~P1(x1832)+~P4(x1833)+P3(f16(x1832,x1833,x1831),x1831)+E(x1831,f24(x1832,x1833))+P4(f16(x1832,x1833,x1831)) % 0.53/0.69 [185]~P1(x1851)+~P1(x1852)+~P4(x1853)+P3(f16(x1852,x1853,x1851),x1851)+P3(f16(x1852,x1853,x1851),x1852)+E(x1851,f24(x1852,x1853)) % 0.53/0.69 [188]~P1(x1881)+~P4(x1883)+~P2(x1882)+P3(f10(x1882,x1883,x1881),x1881)+P3(f10(x1882,x1883,x1881),f28(x1882))+E(x1881,f22(x1882,x1883)) % 0.53/0.69 [189]~P1(x1891)+~P1(x1892)+P3(f9(x1892,x1893,x1891),x1891)+P7(f9(x1892,x1893,x1891),x1892)+~P3(x1893,a27)+E(x1891,f26(x1892,x1893)) % 0.53/0.69 [190]~P1(x1901)+~P2(x1902)+P3(f11(x1902,x1903,x1901),x1901)+P3(f13(x1902,x1903,x1901),x1903)+~P7(x1903,f28(x1902))+E(x1901,f4(x1902,x1903)) % 0.53/0.69 [186]~P1(x1861)+~P4(x1863)+~P2(x1862)+P3(f10(x1862,x1863,x1861),x1861)+E(x1861,f22(x1862,x1863))+E(f3(x1862,f10(x1862,x1863,x1861)),x1863) % 0.53/0.69 [187]~P1(x1871)+~P1(x1872)+P3(f9(x1872,x1873,x1871),x1871)+~P3(x1873,a27)+E(x1871,f26(x1872,x1873))+E(f5(f9(x1872,x1873,x1871)),x1873) % 0.53/0.69 [193]~P1(x1931)+~P2(x1932)+P3(f11(x1932,x1933,x1931),x1931)+~P7(x1933,f28(x1932))+E(x1931,f4(x1932,x1933))+E(f3(x1932,f13(x1932,x1933,x1931)),f11(x1932,x1933,x1931)) % 0.53/0.69 [125]~P1(x1254)+~P4(x1253)+~P4(x1251)+P3(x1251,x1252)+~E(x1251,x1253)+~E(x1252,f23(x1254,x1253)) % 0.53/0.69 [148]~P1(x1483)+~P4(x1482)+~P3(x1481,x1484)+E(x1481,x1482)+P3(x1481,x1483)+~E(x1484,f23(x1483,x1482)) % 0.53/0.69 [152]~P1(x1523)+~P4(x1524)+~P4(x1521)+~P3(x1521,x1523)+P3(x1521,x1522)+~E(x1522,f23(x1523,x1524)) % 0.53/0.69 [163]~P1(x1634)+~P7(x1631,x1634)+P3(x1631,x1632)+~P3(x1633,a27)+~E(x1632,f26(x1634,x1633))+~E(f5(x1631),x1633) % 0.53/0.69 [169]~P4(x1694)+~P2(x1693)+P3(x1691,x1692)+~E(f3(x1693,x1691),x1694)+~P3(x1691,f28(x1693))+~E(x1692,f22(x1693,x1694)) % 0.53/0.69 [176]~P2(x1763)+~P3(x1765,x1764)+P3(x1761,x1762)+~P7(x1764,f28(x1763))+~E(x1762,f4(x1763,x1764))+~E(f3(x1763,x1765),x1761) % 0.53/0.69 [173]E(f31(x1732),f31(x1731))+~P7(x1731,a27)+~P7(x1732,a27)+~P3(f31(x1731),x1732)+~P3(f31(x1732),x1731)+E(x1731,a25)+E(x1732,a25) % 0.53/0.69 [178]~P1(x1783)+~P1(x1782)+P7(x1782,x1783)+~P3(x1781,a27)+~P7(f26(x1782,x1781),f26(x1783,x1781))+E(x1781,a1)+E(f26(x1782,x1781),a25) % 0.53/0.69 [191]~P1(x1911)+~P1(x1912)+~P4(x1913)+E(f17(x1912,x1913,x1911),x1913)+P3(f17(x1912,x1913,x1911),x1911)+P3(f17(x1912,x1913,x1911),x1912)+E(x1911,f23(x1912,x1913)) % 0.53/0.69 [195]~P1(x1951)+~P1(x1952)+~P4(x1953)+~E(f17(x1952,x1953,x1951),x1953)+~P3(f17(x1952,x1953,x1951),x1951)+E(x1951,f23(x1952,x1953))+~P4(f17(x1952,x1953,x1951)) % 0.53/0.69 [196]~P1(x1961)+~P1(x1962)+~P4(x1963)+~P3(f17(x1962,x1963,x1961),x1961)+~P3(f17(x1962,x1963,x1961),x1962)+E(x1961,f23(x1962,x1963))+~P4(f17(x1962,x1963,x1961)) % 0.53/0.69 [199]~P1(x1991)+~P1(x1992)+~P3(x1993,a27)+~P3(f9(x1992,x1993,x1991),x1991)+~P7(f9(x1992,x1993,x1991),x1992)+E(x1991,f26(x1992,x1993))+~E(f5(f9(x1992,x1993,x1991)),x1993) % 0.53/0.69 [200]~P1(x2001)+~P4(x2003)+~P2(x2002)+~P3(f10(x2002,x2003,x2001),x2001)+~P3(f10(x2002,x2003,x2001),f28(x2002))+E(x2001,f22(x2002,x2003))+~E(f3(x2002,f10(x2002,x2003,x2001)),x2003) % 0.53/0.69 [153]~P1(x1534)+~P4(x1532)+~P4(x1531)+~P3(x1531,x1534)+E(x1531,x1532)+P3(x1531,x1533)+~E(x1533,f24(x1534,x1532)) % 0.53/0.69 [194]~P1(x1941)+~P2(x1942)+~P3(x1944,x1943)+~P7(x1943,f28(x1942))+~P3(f11(x1942,x1943,x1941),x1941)+~E(f3(x1942,x1944),f11(x1942,x1943,x1941))+E(x1941,f4(x1942,x1943)) % 0.53/0.69 [201]~P1(x2011)+~P1(x2012)+~P4(x2013)+E(f16(x2012,x2013,x2011),x2013)+~P3(f16(x2012,x2013,x2011),x2011)+~P3(f16(x2012,x2013,x2011),x2012)+E(x2011,f24(x2012,x2013))+~P4(f16(x2012,x2013,x2011)) % 0.53/0.69 %EqnAxiom % 0.53/0.69 [1]E(x11,x11) % 0.53/0.69 [2]E(x22,x21)+~E(x21,x22) % 0.53/0.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.53/0.69 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.53/0.69 [5]~E(x51,x52)+E(f28(x51),f28(x52)) % 0.53/0.69 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63)) % 0.53/0.69 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72)) % 0.53/0.69 [8]~E(x81,x82)+E(f12(x81,x83,x84,x85),f12(x82,x83,x84,x85)) % 0.53/0.69 [9]~E(x91,x92)+E(f12(x93,x91,x94,x95),f12(x93,x92,x94,x95)) % 0.53/0.69 [10]~E(x101,x102)+E(f12(x103,x104,x101,x105),f12(x103,x104,x102,x105)) % 0.53/0.69 [11]~E(x111,x112)+E(f12(x113,x114,x115,x111),f12(x113,x114,x115,x112)) % 0.53/0.69 [12]~E(x121,x122)+E(f4(x121,x123),f4(x122,x123)) % 0.53/0.69 [13]~E(x131,x132)+E(f4(x133,x131),f4(x133,x132)) % 0.53/0.69 [14]~E(x141,x142)+E(f5(x141),f5(x142)) % 0.53/0.69 [15]~E(x151,x152)+E(f9(x151,x153,x154),f9(x152,x153,x154)) % 0.53/0.69 [16]~E(x161,x162)+E(f9(x163,x161,x164),f9(x163,x162,x164)) % 0.53/0.69 [17]~E(x171,x172)+E(f9(x173,x174,x171),f9(x173,x174,x172)) % 0.53/0.69 [18]~E(x181,x182)+E(f17(x181,x183,x184),f17(x182,x183,x184)) % 0.53/0.69 [19]~E(x191,x192)+E(f17(x193,x191,x194),f17(x193,x192,x194)) % 0.53/0.69 [20]~E(x201,x202)+E(f17(x203,x204,x201),f17(x203,x204,x202)) % 0.53/0.69 [21]~E(x211,x212)+E(f26(x211,x213),f26(x212,x213)) % 0.53/0.69 [22]~E(x221,x222)+E(f26(x223,x221),f26(x223,x222)) % 0.53/0.69 [23]~E(x231,x232)+E(f30(x231),f30(x232)) % 0.53/0.69 [24]~E(x241,x242)+E(f31(x241),f31(x242)) % 0.53/0.69 [25]~E(x251,x252)+E(f6(x251),f6(x252)) % 0.53/0.69 [26]~E(x261,x262)+E(f16(x261,x263,x264),f16(x262,x263,x264)) % 0.53/0.69 [27]~E(x271,x272)+E(f16(x273,x271,x274),f16(x273,x272,x274)) % 0.53/0.69 [28]~E(x281,x282)+E(f16(x283,x284,x281),f16(x283,x284,x282)) % 0.53/0.69 [29]~E(x291,x292)+E(f24(x291,x293),f24(x292,x293)) % 0.53/0.69 [30]~E(x301,x302)+E(f24(x303,x301),f24(x303,x302)) % 0.53/0.69 [31]~E(x311,x312)+E(f11(x311,x313,x314),f11(x312,x313,x314)) % 0.53/0.69 [32]~E(x321,x322)+E(f11(x323,x321,x324),f11(x323,x322,x324)) % 0.53/0.69 [33]~E(x331,x332)+E(f11(x333,x334,x331),f11(x333,x334,x332)) % 0.53/0.69 [34]~E(x341,x342)+E(f14(x341),f14(x342)) % 0.53/0.69 [35]~E(x351,x352)+E(f10(x351,x353,x354),f10(x352,x353,x354)) % 0.53/0.69 [36]~E(x361,x362)+E(f10(x363,x361,x364),f10(x363,x362,x364)) % 0.53/0.69 [37]~E(x371,x372)+E(f10(x373,x374,x371),f10(x373,x374,x372)) % 0.53/0.69 [38]~E(x381,x382)+E(f21(x381,x383),f21(x382,x383)) % 0.53/0.69 [39]~E(x391,x392)+E(f21(x393,x391),f21(x393,x392)) % 0.53/0.69 [40]~E(x401,x402)+E(f13(x401,x403,x404),f13(x402,x403,x404)) % 0.53/0.69 [41]~E(x411,x412)+E(f13(x413,x411,x414),f13(x413,x412,x414)) % 0.53/0.69 [42]~E(x421,x422)+E(f13(x423,x424,x421),f13(x423,x424,x422)) % 0.53/0.69 [43]~E(x431,x432)+E(f19(x431,x433),f19(x432,x433)) % 0.53/0.69 [44]~E(x441,x442)+E(f19(x443,x441),f19(x443,x442)) % 0.53/0.69 [45]~E(x451,x452)+E(f18(x451,x453),f18(x452,x453)) % 0.53/0.69 [46]~E(x461,x462)+E(f18(x463,x461),f18(x463,x462)) % 0.53/0.69 [47]~E(x471,x472)+E(f20(x471,x473),f20(x472,x473)) % 0.53/0.69 [48]~E(x481,x482)+E(f20(x483,x481),f20(x483,x482)) % 0.53/0.69 [49]~E(x491,x492)+E(f22(x491,x493),f22(x492,x493)) % 0.53/0.69 [50]~E(x501,x502)+E(f22(x503,x501),f22(x503,x502)) % 0.53/0.69 [51]~E(x511,x512)+E(f23(x511,x513),f23(x512,x513)) % 0.53/0.69 [52]~E(x521,x522)+E(f23(x523,x521),f23(x523,x522)) % 0.53/0.69 [53]~E(x531,x532)+E(f32(x531),f32(x532)) % 0.53/0.69 [54]~E(x541,x542)+E(f8(x541,x543,x544),f8(x542,x543,x544)) % 0.53/0.69 [55]~E(x551,x552)+E(f8(x553,x551,x554),f8(x553,x552,x554)) % 0.53/0.69 [56]~E(x561,x562)+E(f8(x563,x564,x561),f8(x563,x564,x562)) % 0.53/0.69 [57]~E(x571,x572)+E(f15(x571,x573),f15(x572,x573)) % 0.53/0.69 [58]~E(x581,x582)+E(f15(x583,x581),f15(x583,x582)) % 0.53/0.69 [59]~E(x591,x592)+E(f7(x591),f7(x592)) % 0.53/0.69 [60]~P1(x601)+P1(x602)+~E(x601,x602) % 0.53/0.69 [61]~P5(x611)+P5(x612)+~E(x611,x612) % 0.53/0.69 [62]~P6(x621)+P6(x622)+~E(x621,x622) % 0.53/0.69 [63]~P2(x631)+P2(x632)+~E(x631,x632) % 0.53/0.69 [64]P3(x642,x643)+~E(x641,x642)+~P3(x641,x643) % 0.53/0.69 [65]P3(x653,x652)+~E(x651,x652)+~P3(x653,x651) % 0.53/0.69 [66]~P4(x661)+P4(x662)+~E(x661,x662) % 0.53/0.69 [67]P9(x672,x673)+~E(x671,x672)+~P9(x671,x673) % 0.53/0.69 [68]P9(x683,x682)+~E(x681,x682)+~P9(x683,x681) % 0.53/0.69 [69]P7(x692,x693)+~E(x691,x692)+~P7(x691,x693) % 0.53/0.69 [70]P7(x703,x702)+~E(x701,x702)+~P7(x703,x701) % 0.53/0.69 [71]P8(x712,x713)+~E(x711,x712)+~P8(x711,x713) % 0.53/0.69 [72]P8(x723,x722)+~E(x721,x722)+~P8(x723,x721) % 0.53/0.69 % 0.53/0.69 %------------------------------------------- % 0.53/0.69 cnf(215,plain, % 0.53/0.69 (~P3(a33,f28(a29))), % 0.53/0.69 inference(equality_inference,[],[128])). % 0.53/0.69 cnf(234,plain, % 0.53/0.69 ($false), % 0.53/0.69 inference(scs_inference,[],[215,79]), % 0.53/0.69 ['proof']). % 0.53/0.69 % SZS output end Proof % 0.53/0.69 % Total time :0.020000s %------------------------------------------------------------------------------