%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM560+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 : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 12:25:03 EDT 2024 % Result : Theorem 0.53s 0.64s % Output : CNFRefutation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM560+2 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n018.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 : Sat Jun 22 20:14:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 0.52/0.62 %------------------------------------------- % 0.52/0.62 % File :CSE---1.7 % 0.52/0.62 % Problem :theBenchmark % 0.52/0.62 % Transform :cnf % 0.52/0.62 % Format :tptp:raw % 0.52/0.62 % Command :java -jar mcs_scs.jar %d %s % 0.52/0.62 % 0.52/0.62 % Result :Theorem 0.010000s % 0.52/0.62 % Output :CNFRefutation 0.010000s % 0.52/0.62 %------------------------------------------- % 0.52/0.63 %------------------------------------------------------------------------------ % 0.52/0.63 % File : NUM560+2 : TPTP v8.2.0. Released v4.0.0. % 0.52/0.63 % Domain : Number Theory % 0.52/0.63 % Problem : Ramsey's Infinite Theorem 13, 01 expansion % 0.52/0.63 % Version : Especial. % 0.52/0.63 % English : % 0.52/0.63 % 0.52/0.63 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 0.52/0.63 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 0.52/0.63 % Source : [Pas08] % 0.52/0.63 % Names : ramsey_13.01 [Pas08] % 0.52/0.63 % 0.52/0.63 % Status : Theorem % 0.52/0.63 % Rating : 0.11 v8.1.0, 0.06 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.08 v6.1.0, 0.10 v6.0.0, 0.09 v5.5.0, 0.11 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.15 v5.1.0, 0.24 v5.0.0, 0.29 v4.1.0, 0.39 v4.0.1, 0.70 v4.0.0 % 0.52/0.63 % Syntax : Number of formulae : 68 ( 3 unt; 9 def) % 0.52/0.63 % Number of atoms : 265 ( 41 equ) % 0.52/0.63 % Maximal formula atoms : 8 ( 3 avg) % 0.52/0.63 % Number of connectives : 215 ( 18 ~; 5 |; 76 &) % 0.52/0.63 % ( 20 <=>; 96 =>; 0 <=; 0 <~>) % 0.52/0.63 % Maximal formula depth : 12 ( 5 avg) % 0.52/0.63 % Maximal term depth : 4 ( 1 avg) % 0.52/0.63 % Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty) % 0.52/0.63 % Number of functors : 16 ( 16 usr; 5 con; 0-2 aty) % 0.52/0.63 % Number of variables : 123 ( 118 !; 5 ?) % 0.52/0.63 % SPC : FOF_THM_RFO_SEQ % 0.52/0.63 % 0.52/0.63 % Comments : Problem generated by the SAD system [VLP07] % 0.52/0.63 %------------------------------------------------------------------------------ % 0.52/0.63 fof(mSetSort,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aSet0(W0) % 0.52/0.63 => $true ) ). % 0.52/0.63 % 0.52/0.63 fof(mElmSort,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aElement0(W0) % 0.52/0.63 => $true ) ). % 0.52/0.63 % 0.52/0.63 fof(mEOfElem,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aSet0(W0) % 0.52/0.63 => ! [W1] : % 0.52/0.63 ( aElementOf0(W1,W0) % 0.52/0.63 => aElement0(W1) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mFinRel,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aSet0(W0) % 0.52/0.63 => ( isFinite0(W0) % 0.52/0.63 => $true ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mDefEmp,definition, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( W0 = slcrc0 % 0.52/0.63 <=> ( aSet0(W0) % 0.52/0.63 & ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mEmpFin,axiom, % 0.52/0.63 isFinite0(slcrc0) ). % 0.52/0.63 % 0.52/0.63 fof(mCntRel,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aSet0(W0) % 0.52/0.63 => ( isCountable0(W0) % 0.52/0.63 => $true ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mCountNFin,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( ( aSet0(W0) % 0.52/0.63 & isCountable0(W0) ) % 0.52/0.63 => ~ isFinite0(W0) ) ). % 0.52/0.63 % 0.52/0.63 fof(mCountNFin_01,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( ( aSet0(W0) % 0.52/0.63 & isCountable0(W0) ) % 0.52/0.63 => W0 != slcrc0 ) ). % 0.52/0.63 % 0.52/0.63 fof(mDefSub,definition, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aSet0(W0) % 0.52/0.63 => ! [W1] : % 0.52/0.63 ( aSubsetOf0(W1,W0) % 0.52/0.63 <=> ( aSet0(W1) % 0.52/0.63 & ! [W2] : % 0.52/0.63 ( aElementOf0(W2,W1) % 0.52/0.63 => aElementOf0(W2,W0) ) ) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mSubFSet,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( ( aSet0(W0) % 0.52/0.63 & isFinite0(W0) ) % 0.52/0.63 => ! [W1] : % 0.52/0.63 ( aSubsetOf0(W1,W0) % 0.52/0.63 => isFinite0(W1) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mSubRefl,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aSet0(W0) % 0.52/0.63 => aSubsetOf0(W0,W0) ) ). % 0.52/0.63 % 0.52/0.63 fof(mSubASymm,axiom, % 0.52/0.63 ! [W0,W1] : % 0.52/0.63 ( ( aSet0(W0) % 0.52/0.63 & aSet0(W1) ) % 0.52/0.63 => ( ( aSubsetOf0(W0,W1) % 0.52/0.63 & aSubsetOf0(W1,W0) ) % 0.52/0.63 => W0 = W1 ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mSubTrans,axiom, % 0.52/0.63 ! [W0,W1,W2] : % 0.52/0.63 ( ( aSet0(W0) % 0.52/0.63 & aSet0(W1) % 0.52/0.63 & aSet0(W2) ) % 0.52/0.63 => ( ( aSubsetOf0(W0,W1) % 0.52/0.63 & aSubsetOf0(W1,W2) ) % 0.52/0.63 => aSubsetOf0(W0,W2) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mDefCons,definition, % 0.52/0.63 ! [W0,W1] : % 0.52/0.63 ( ( aSet0(W0) % 0.52/0.63 & aElement0(W1) ) % 0.52/0.63 => ! [W2] : % 0.52/0.63 ( W2 = sdtpldt0(W0,W1) % 0.52/0.63 <=> ( aSet0(W2) % 0.52/0.63 & ! [W3] : % 0.52/0.63 ( aElementOf0(W3,W2) % 0.52/0.63 <=> ( aElement0(W3) % 0.52/0.63 & ( aElementOf0(W3,W0) % 0.52/0.63 | W3 = W1 ) ) ) ) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mDefDiff,definition, % 0.52/0.63 ! [W0,W1] : % 0.52/0.63 ( ( aSet0(W0) % 0.52/0.63 & aElement0(W1) ) % 0.52/0.63 => ! [W2] : % 0.52/0.63 ( W2 = sdtmndt0(W0,W1) % 0.52/0.63 <=> ( aSet0(W2) % 0.52/0.63 & ! [W3] : % 0.52/0.63 ( aElementOf0(W3,W2) % 0.52/0.63 <=> ( aElement0(W3) % 0.52/0.63 & aElementOf0(W3,W0) % 0.52/0.63 & W3 != W1 ) ) ) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mConsDiff,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aSet0(W0) % 0.52/0.63 => ! [W1] : % 0.52/0.63 ( aElementOf0(W1,W0) % 0.52/0.63 => sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mDiffCons,axiom, % 0.52/0.63 ! [W0,W1] : % 0.52/0.63 ( ( aElement0(W0) % 0.52/0.63 & aSet0(W1) ) % 0.52/0.63 => ( ~ aElementOf0(W0,W1) % 0.52/0.63 => sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mCConsSet,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aElement0(W0) % 0.52/0.63 => ! [W1] : % 0.52/0.63 ( ( aSet0(W1) % 0.52/0.63 & isCountable0(W1) ) % 0.52/0.63 => isCountable0(sdtpldt0(W1,W0)) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mCDiffSet,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aElement0(W0) % 0.52/0.63 => ! [W1] : % 0.52/0.63 ( ( aSet0(W1) % 0.52/0.63 & isCountable0(W1) ) % 0.52/0.63 => isCountable0(sdtmndt0(W1,W0)) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mFConsSet,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aElement0(W0) % 0.52/0.63 => ! [W1] : % 0.52/0.63 ( ( aSet0(W1) % 0.52/0.63 & isFinite0(W1) ) % 0.52/0.63 => isFinite0(sdtpldt0(W1,W0)) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mFDiffSet,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aElement0(W0) % 0.52/0.63 => ! [W1] : % 0.52/0.63 ( ( aSet0(W1) % 0.52/0.63 & isFinite0(W1) ) % 0.52/0.63 => isFinite0(sdtmndt0(W1,W0)) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mNATSet,axiom, % 0.52/0.63 ( aSet0(szNzAzT0) % 0.52/0.63 & isCountable0(szNzAzT0) ) ). % 0.52/0.63 % 0.52/0.63 fof(mZeroNum,axiom, % 0.52/0.63 aElementOf0(sz00,szNzAzT0) ). % 0.52/0.63 % 0.52/0.63 fof(mSuccNum,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 => ( aElementOf0(szszuzczcdt0(W0),szNzAzT0) % 0.52/0.63 & szszuzczcdt0(W0) != sz00 ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mSuccEquSucc,axiom, % 0.52/0.63 ! [W0,W1] : % 0.52/0.63 ( ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 & aElementOf0(W1,szNzAzT0) ) % 0.52/0.63 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 0.52/0.63 => W0 = W1 ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mNatExtra,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 => ( W0 = sz00 % 0.52/0.63 | ? [W1] : % 0.52/0.63 ( aElementOf0(W1,szNzAzT0) % 0.52/0.63 & W0 = szszuzczcdt0(W1) ) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mNatNSucc,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 => W0 != szszuzczcdt0(W0) ) ). % 0.52/0.63 % 0.52/0.63 fof(mLessRel,axiom, % 0.52/0.63 ! [W0,W1] : % 0.52/0.63 ( ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 & aElementOf0(W1,szNzAzT0) ) % 0.52/0.63 => ( sdtlseqdt0(W0,W1) % 0.52/0.63 => $true ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mZeroLess,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 => sdtlseqdt0(sz00,W0) ) ). % 0.52/0.63 % 0.52/0.63 fof(mNoScLessZr,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 => ~ sdtlseqdt0(szszuzczcdt0(W0),sz00) ) ). % 0.52/0.63 % 0.52/0.63 fof(mSuccLess,axiom, % 0.52/0.63 ! [W0,W1] : % 0.52/0.63 ( ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 & aElementOf0(W1,szNzAzT0) ) % 0.52/0.63 => ( sdtlseqdt0(W0,W1) % 0.52/0.63 <=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mLessSucc,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 => sdtlseqdt0(W0,szszuzczcdt0(W0)) ) ). % 0.52/0.63 % 0.52/0.63 fof(mLessRefl,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 => sdtlseqdt0(W0,W0) ) ). % 0.52/0.63 % 0.52/0.63 fof(mLessASymm,axiom, % 0.52/0.63 ! [W0,W1] : % 0.52/0.63 ( ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 & aElementOf0(W1,szNzAzT0) ) % 0.52/0.63 => ( ( sdtlseqdt0(W0,W1) % 0.52/0.63 & sdtlseqdt0(W1,W0) ) % 0.52/0.63 => W0 = W1 ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mLessTrans,axiom, % 0.52/0.63 ! [W0,W1,W2] : % 0.52/0.63 ( ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 & aElementOf0(W1,szNzAzT0) % 0.52/0.63 & aElementOf0(W2,szNzAzT0) ) % 0.52/0.63 => ( ( sdtlseqdt0(W0,W1) % 0.52/0.63 & sdtlseqdt0(W1,W2) ) % 0.52/0.63 => sdtlseqdt0(W0,W2) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mLessTotal,axiom, % 0.52/0.63 ! [W0,W1] : % 0.52/0.63 ( ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 & aElementOf0(W1,szNzAzT0) ) % 0.52/0.63 => ( sdtlseqdt0(W0,W1) % 0.52/0.63 | sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mIHSort,axiom, % 0.52/0.63 ! [W0,W1] : % 0.52/0.63 ( ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 & aElementOf0(W1,szNzAzT0) ) % 0.52/0.63 => ( iLess0(W0,W1) % 0.52/0.63 => $true ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mIH,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aElementOf0(W0,szNzAzT0) % 0.52/0.63 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 0.52/0.63 % 0.52/0.63 fof(mCardS,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aSet0(W0) % 0.52/0.63 => aElement0(sbrdtbr0(W0)) ) ). % 0.52/0.63 % 0.52/0.63 fof(mCardNum,axiom, % 0.52/0.63 ! [W0] : % 0.52/0.63 ( aSet0(W0) % 0.52/0.63 => ( aElementOf0(sbrdtbr0(W0),szNzAzT0) % 0.52/0.63 <=> isFinite0(W0) ) ) ). % 0.52/0.63 % 0.52/0.63 fof(mCardEmpty,axiom, % 0.52/0.63 ! [W0] : % 0.53/0.63 ( aSet0(W0) % 0.53/0.63 => ( sbrdtbr0(W0) = sz00 % 0.53/0.63 <=> W0 = slcrc0 ) ) ). % 0.53/0.63 % 0.53/0.63 fof(mCardCons,axiom, % 0.53/0.63 ! [W0] : % 0.53/0.63 ( ( aSet0(W0) % 0.53/0.63 & isFinite0(W0) ) % 0.53/0.63 => ! [W1] : % 0.53/0.63 ( aElement0(W1) % 0.53/0.63 => ( ~ aElementOf0(W1,W0) % 0.53/0.63 => sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ) ). % 0.53/0.63 % 0.53/0.63 fof(mCardDiff,axiom, % 0.53/0.63 ! [W0] : % 0.53/0.63 ( aSet0(W0) % 0.53/0.63 => ! [W1] : % 0.53/0.63 ( ( isFinite0(W0) % 0.53/0.63 & aElementOf0(W1,W0) ) % 0.53/0.63 => szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ) ). % 0.53/0.63 % 0.53/0.63 fof(mCardSub,axiom, % 0.53/0.63 ! [W0] : % 0.53/0.63 ( aSet0(W0) % 0.53/0.63 => ! [W1] : % 0.53/0.64 ( ( isFinite0(W0) % 0.53/0.64 & aSubsetOf0(W1,W0) ) % 0.53/0.64 => sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mCardSubEx,axiom, % 0.53/0.64 ! [W0,W1] : % 0.53/0.64 ( ( aSet0(W0) % 0.53/0.64 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.64 => ( ( isFinite0(W0) % 0.53/0.64 & sdtlseqdt0(W1,sbrdtbr0(W0)) ) % 0.53/0.64 => ? [W2] : % 0.53/0.64 ( aSubsetOf0(W2,W0) % 0.53/0.64 & sbrdtbr0(W2) = W1 ) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mDefMin,definition, % 0.53/0.64 ! [W0] : % 0.53/0.64 ( ( aSubsetOf0(W0,szNzAzT0) % 0.53/0.64 & W0 != slcrc0 ) % 0.53/0.64 => ! [W1] : % 0.53/0.64 ( W1 = szmzizndt0(W0) % 0.53/0.64 <=> ( aElementOf0(W1,W0) % 0.53/0.64 & ! [W2] : % 0.53/0.64 ( aElementOf0(W2,W0) % 0.53/0.64 => sdtlseqdt0(W1,W2) ) ) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mDefMax,definition, % 0.53/0.64 ! [W0] : % 0.53/0.64 ( ( aSubsetOf0(W0,szNzAzT0) % 0.53/0.64 & isFinite0(W0) % 0.53/0.64 & W0 != slcrc0 ) % 0.53/0.64 => ! [W1] : % 0.53/0.64 ( W1 = szmzazxdt0(W0) % 0.53/0.64 <=> ( aElementOf0(W1,W0) % 0.53/0.64 & ! [W2] : % 0.53/0.64 ( aElementOf0(W2,W0) % 0.53/0.64 => sdtlseqdt0(W2,W1) ) ) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mMinMin,axiom, % 0.53/0.64 ! [W0,W1] : % 0.53/0.64 ( ( aSubsetOf0(W0,szNzAzT0) % 0.53/0.64 & aSubsetOf0(W1,szNzAzT0) % 0.53/0.64 & W0 != slcrc0 % 0.53/0.64 & W1 != slcrc0 ) % 0.53/0.64 => ( ( aElementOf0(szmzizndt0(W0),W1) % 0.53/0.64 & aElementOf0(szmzizndt0(W1),W0) ) % 0.53/0.64 => szmzizndt0(W0) = szmzizndt0(W1) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mDefSeg,definition, % 0.53/0.64 ! [W0] : % 0.53/0.64 ( aElementOf0(W0,szNzAzT0) % 0.53/0.64 => ! [W1] : % 0.53/0.64 ( W1 = slbdtrb0(W0) % 0.53/0.64 <=> ( aSet0(W1) % 0.53/0.64 & ! [W2] : % 0.53/0.64 ( aElementOf0(W2,W1) % 0.53/0.64 <=> ( aElementOf0(W2,szNzAzT0) % 0.53/0.64 & sdtlseqdt0(szszuzczcdt0(W2),W0) ) ) ) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mSegFin,axiom, % 0.53/0.64 ! [W0] : % 0.53/0.64 ( aElementOf0(W0,szNzAzT0) % 0.53/0.64 => isFinite0(slbdtrb0(W0)) ) ). % 0.53/0.64 % 0.53/0.64 fof(mSegZero,axiom, % 0.53/0.64 slbdtrb0(sz00) = slcrc0 ). % 0.53/0.64 % 0.53/0.64 fof(mSegSucc,axiom, % 0.53/0.64 ! [W0,W1] : % 0.53/0.64 ( ( aElementOf0(W0,szNzAzT0) % 0.53/0.64 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.64 => ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1))) % 0.53/0.64 <=> ( aElementOf0(W0,slbdtrb0(W1)) % 0.53/0.64 | W0 = W1 ) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mSegLess,axiom, % 0.53/0.64 ! [W0,W1] : % 0.53/0.64 ( ( aElementOf0(W0,szNzAzT0) % 0.53/0.64 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.64 => ( sdtlseqdt0(W0,W1) % 0.53/0.64 <=> aSubsetOf0(slbdtrb0(W0),slbdtrb0(W1)) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mFinSubSeg,axiom, % 0.53/0.64 ! [W0] : % 0.53/0.64 ( ( aSubsetOf0(W0,szNzAzT0) % 0.53/0.64 & isFinite0(W0) ) % 0.53/0.64 => ? [W1] : % 0.53/0.64 ( aElementOf0(W1,szNzAzT0) % 0.53/0.64 & aSubsetOf0(W0,slbdtrb0(W1)) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mCardSeg,axiom, % 0.53/0.64 ! [W0] : % 0.53/0.64 ( aElementOf0(W0,szNzAzT0) % 0.53/0.64 => sbrdtbr0(slbdtrb0(W0)) = W0 ) ). % 0.53/0.64 % 0.53/0.64 fof(mDefSel,definition, % 0.53/0.64 ! [W0,W1] : % 0.53/0.64 ( ( aSet0(W0) % 0.53/0.64 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.64 => ! [W2] : % 0.53/0.64 ( W2 = slbdtsldtrb0(W0,W1) % 0.53/0.64 <=> ( aSet0(W2) % 0.53/0.64 & ! [W3] : % 0.53/0.64 ( aElementOf0(W3,W2) % 0.53/0.64 <=> ( aSubsetOf0(W3,W0) % 0.53/0.64 & sbrdtbr0(W3) = W1 ) ) ) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mSelFSet,axiom, % 0.53/0.64 ! [W0] : % 0.53/0.64 ( ( aSet0(W0) % 0.53/0.64 & isFinite0(W0) ) % 0.53/0.64 => ! [W1] : % 0.53/0.64 ( aElementOf0(W1,szNzAzT0) % 0.53/0.64 => isFinite0(slbdtsldtrb0(W0,W1)) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mSelNSet,axiom, % 0.53/0.64 ! [W0] : % 0.53/0.64 ( ( aSet0(W0) % 0.53/0.64 & ~ isFinite0(W0) ) % 0.53/0.64 => ! [W1] : % 0.53/0.64 ( aElementOf0(W1,szNzAzT0) % 0.53/0.64 => slbdtsldtrb0(W0,W1) != slcrc0 ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mSelCSet,axiom, % 0.53/0.64 ! [W0] : % 0.53/0.64 ( ( aSet0(W0) % 0.53/0.64 & isCountable0(W0) ) % 0.53/0.64 => ! [W1] : % 0.53/0.64 ( ( aElementOf0(W1,szNzAzT0) % 0.53/0.64 & W1 != sz00 ) % 0.53/0.64 => isCountable0(slbdtsldtrb0(W0,W1)) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mSelSub,axiom, % 0.53/0.64 ! [W0] : % 0.53/0.64 ( aElementOf0(W0,szNzAzT0) % 0.53/0.64 => ! [W1,W2] : % 0.53/0.64 ( ( aSet0(W1) % 0.53/0.64 & aSet0(W2) % 0.53/0.64 & W0 != sz00 ) % 0.53/0.64 => ( ( aSubsetOf0(slbdtsldtrb0(W1,W0),slbdtsldtrb0(W2,W0)) % 0.53/0.64 & slbdtsldtrb0(W1,W0) != slcrc0 ) % 0.53/0.64 => aSubsetOf0(W1,W2) ) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mSelExtra,axiom, % 0.53/0.64 ! [W0,W1] : % 0.53/0.64 ( ( aSet0(W0) % 0.53/0.64 & aElementOf0(W1,szNzAzT0) ) % 0.53/0.64 => ! [W2] : % 0.53/0.64 ( ( aSubsetOf0(W2,slbdtsldtrb0(W0,W1)) % 0.53/0.64 & isFinite0(W2) ) % 0.53/0.64 => ? [W3] : % 0.53/0.64 ( aSubsetOf0(W3,W0) % 0.53/0.64 & isFinite0(W3) % 0.53/0.64 & aSubsetOf0(W2,slbdtsldtrb0(W3,W1)) ) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mFunSort,axiom, % 0.53/0.64 ! [W0] : % 0.53/0.64 ( aFunction0(W0) % 0.53/0.64 => $true ) ). % 0.53/0.64 % 0.53/0.64 fof(mDomSet,axiom, % 0.53/0.64 ! [W0] : % 0.53/0.64 ( aFunction0(W0) % 0.53/0.64 => aSet0(szDzozmdt0(W0)) ) ). % 0.53/0.64 % 0.53/0.64 fof(mImgElm,axiom, % 0.53/0.64 ! [W0] : % 0.53/0.64 ( aFunction0(W0) % 0.53/0.64 => ! [W1] : % 0.53/0.64 ( aElementOf0(W1,szDzozmdt0(W0)) % 0.53/0.64 => aElement0(sdtlpdtrp0(W0,W1)) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(mDefPtt,definition, % 0.53/0.64 ! [W0,W1] : % 0.53/0.64 ( ( aFunction0(W0) % 0.53/0.64 & aElement0(W1) ) % 0.53/0.64 => ! [W2] : % 0.53/0.64 ( W2 = sdtlbdtrb0(W0,W1) % 0.53/0.64 <=> ( aSet0(W2) % 0.53/0.64 & ! [W3] : % 0.53/0.64 ( aElementOf0(W3,W2) % 0.53/0.64 <=> ( aElementOf0(W3,szDzozmdt0(W0)) % 0.53/0.64 & sdtlpdtrp0(W0,W3) = W1 ) ) ) ) ) ). % 0.53/0.64 % 0.53/0.64 fof(m__2693,hypothesis, % 0.53/0.64 ( aFunction0(xF) % 0.53/0.64 & aElement0(xy) ) ). % 0.53/0.64 % 0.53/0.64 fof(m__,conjecture, % 0.53/0.64 ( ( aSet0(sdtlbdtrb0(xF,xy)) % 0.53/0.64 & ! [W0] : % 0.53/0.64 ( aElementOf0(W0,sdtlbdtrb0(xF,xy)) % 0.53/0.64 <=> ( aElementOf0(W0,szDzozmdt0(xF)) % 0.53/0.64 & sdtlpdtrp0(xF,W0) = xy ) ) ) % 0.53/0.64 => ( ! [W0] : % 0.53/0.64 ( aElementOf0(W0,sdtlbdtrb0(xF,xy)) % 0.53/0.64 => aElementOf0(W0,szDzozmdt0(xF)) ) % 0.53/0.64 | aSubsetOf0(sdtlbdtrb0(xF,xy),szDzozmdt0(xF)) ) ) ). % 0.53/0.64 % 0.53/0.64 %------------------------------------------------------------------------------ % 0.53/0.64 %------------------------------------------- % 0.53/0.64 % Proof found % 0.53/0.64 % SZS status Theorem for theBenchmark % 0.53/0.64 % SZS output start Proof % 0.53/0.64 %ClaNum:186(EqnAxiom:60) % 0.53/0.64 %VarNum:855(SingletonVarNum:260) % 0.53/0.64 %MaxLitNum:8 % 0.53/0.64 %MaxfuncDepth:3 % 0.53/0.64 %SharedTerms:20 % 0.53/0.64 %goalClause: 68 69 70 71 123 130 142 % 0.53/0.64 %singleGoalClaCount:4 % 0.53/0.64 [62]P1(a24) % 0.53/0.64 [63]P2(a26) % 0.53/0.64 [64]P5(a22) % 0.53/0.64 [65]P6(a24) % 0.53/0.64 [66]P3(a27) % 0.53/0.64 [67]P4(a1,a24) % 0.53/0.64 [61]E(f2(a1),a22) % 0.53/0.64 [68]P1(f3(a27,a26)) % 0.53/0.64 [69]P4(a4,f3(a27,a26)) % 0.53/0.64 [70]~P4(a4,f25(a27)) % 0.53/0.64 [71]~P7(f3(a27,a26),f25(a27)) % 0.53/0.64 [72]P1(x721)+~E(x721,a22) % 0.53/0.64 [79]~P1(x791)+P7(x791,x791) % 0.53/0.64 [86]~P4(x861,a24)+P9(a1,x861) % 0.53/0.64 [92]P9(x921,x921)+~P4(x921,a24) % 0.53/0.64 [76]~P3(x761)+P1(f25(x761)) % 0.53/0.64 [77]~P1(x771)+P2(f9(x771)) % 0.53/0.64 [81]~P4(x811,a24)+~E(f28(x811),a1) % 0.53/0.64 [82]~P4(x821,a24)+~E(f28(x821),x821) % 0.53/0.64 [84]~P4(x841,a24)+P5(f2(x841)) % 0.53/0.64 [93]~P4(x931,a24)+P4(f28(x931),a24) % 0.53/0.64 [94]~P4(x941,a24)+P9(x941,f28(x941)) % 0.53/0.64 [95]~P4(x951,a24)+P8(x951,f28(x951)) % 0.53/0.64 [104]~P4(x1041,a24)+~P9(f28(x1041),a1) % 0.53/0.64 [123]~P4(x1231,f3(a27,a26))+E(f21(a27,x1231),a26) % 0.53/0.64 [130]~P4(x1301,f3(a27,a26))+P4(x1301,f25(a27)) % 0.53/0.64 [85]~P4(x851,a24)+E(f9(f2(x851)),x851) % 0.53/0.64 [80]~P4(x802,x801)+~E(x801,a22) % 0.53/0.64 [75]~P1(x751)+~P6(x751)+~E(x751,a22) % 0.53/0.64 [78]~P5(x781)+~P6(x781)+~P1(x781) % 0.53/0.64 [73]~P1(x731)+~E(x731,a22)+E(f9(x731),a1) % 0.53/0.64 [74]~P1(x741)+E(x741,a22)+~E(f9(x741),a1) % 0.53/0.64 [83]~P1(x831)+P4(f10(x831),x831)+E(x831,a22) % 0.53/0.64 [89]~P1(x891)+~P5(x891)+P4(f9(x891),a24) % 0.53/0.64 [96]~P4(x961,a24)+E(x961,a1)+P4(f11(x961),a24) % 0.53/0.64 [97]~P1(x971)+P5(x971)+~P4(f9(x971),a24) % 0.53/0.64 [103]~P5(x1031)+~P7(x1031,a24)+P4(f5(x1031),a24) % 0.53/0.64 [142]P4(x1421,f3(a27,a26))+~P4(x1421,f25(a27))+~E(f21(a27,x1421),a26) % 0.53/0.64 [87]~P4(x871,a24)+E(x871,a1)+E(f28(f11(x871)),x871) % 0.53/0.64 [113]~P5(x1131)+~P7(x1131,a24)+P7(x1131,f2(f5(x1131))) % 0.53/0.64 [90]~P7(x901,x902)+P1(x901)+~P1(x902) % 0.53/0.64 [91]~P4(x911,x912)+P2(x911)+~P1(x912) % 0.53/0.64 [88]P1(x881)+~P4(x882,a24)+~E(x881,f2(x882)) % 0.53/0.64 [127]~P3(x1271)+~P4(x1272,f25(x1271))+P2(f21(x1271,x1272)) % 0.53/0.64 [129]~P1(x1291)+~P4(x1292,x1291)+E(f19(f20(x1291,x1292),x1292),x1291) % 0.53/0.64 [98]~P5(x982)+~P7(x981,x982)+P5(x981)+~P1(x982) % 0.53/0.64 [102]P4(x1022,x1021)+~E(x1022,f29(x1021))+~P7(x1021,a24)+E(x1021,a22) % 0.53/0.64 [106]~P1(x1061)+~P2(x1062)+~P5(x1061)+P5(f19(x1061,x1062)) % 0.53/0.64 [107]~P1(x1071)+~P2(x1072)+~P5(x1071)+P5(f20(x1071,x1072)) % 0.53/0.64 [108]~P1(x1081)+~P2(x1082)+~P6(x1081)+P6(f19(x1081,x1082)) % 0.53/0.64 [109]~P1(x1091)+~P2(x1092)+~P6(x1091)+P6(f20(x1091,x1092)) % 0.53/0.64 [110]~P1(x1101)+P5(x1101)+~P4(x1102,a24)+~E(f23(x1101,x1102),a22) % 0.53/0.64 [112]E(x1121,x1122)+~E(f28(x1121),f28(x1122))+~P4(x1122,a24)+~P4(x1121,a24) % 0.53/0.64 [116]~P1(x1162)+~P5(x1162)+~P7(x1161,x1162)+P9(f9(x1161),f9(x1162)) % 0.53/0.64 [119]~P1(x1191)+~P5(x1191)+~P4(x1192,a24)+P5(f23(x1191,x1192)) % 0.53/0.64 [126]~P1(x1261)+~P1(x1262)+P7(x1261,x1262)+P4(f12(x1262,x1261),x1261) % 0.53/0.64 [134]P9(x1341,x1342)+P9(f28(x1342),x1341)+~P4(x1342,a24)+~P4(x1341,a24) % 0.53/0.64 [147]~P9(x1471,x1472)+~P4(x1472,a24)+~P4(x1471,a24)+P7(f2(x1471),f2(x1472)) % 0.53/0.64 [148]~P9(x1481,x1482)+~P4(x1482,a24)+~P4(x1481,a24)+P9(f28(x1481),f28(x1482)) % 0.53/0.64 [150]~P1(x1501)+~P1(x1502)+P7(x1501,x1502)+~P4(f12(x1502,x1501),x1502) % 0.53/0.64 [152]P9(x1521,x1522)+~P4(x1522,a24)+~P4(x1521,a24)+~P7(f2(x1521),f2(x1522)) % 0.53/0.64 [153]P9(x1531,x1532)+~P4(x1532,a24)+~P4(x1531,a24)+~P9(f28(x1531),f28(x1532)) % 0.53/0.64 [128]P4(x1282,x1281)+~P1(x1281)+~P2(x1282)+E(f20(f19(x1281,x1282),x1282),x1281) % 0.53/0.64 [137]~E(x1371,x1372)+~P4(x1372,a24)+~P4(x1371,a24)+P4(x1371,f2(f28(x1372))) % 0.53/0.64 [158]~P4(x1582,a24)+~P4(x1581,a24)+~P4(x1581,f2(x1582))+P4(x1581,f2(f28(x1582))) % 0.53/0.64 [157]~P1(x1571)+~P5(x1571)+~P4(x1572,x1571)+E(f28(f9(f20(x1571,x1572))),f9(x1571)) % 0.53/0.64 [124]~P1(x1242)+~P7(x1243,x1242)+P4(x1241,x1242)+~P4(x1241,x1243) % 0.53/0.64 [99]~P1(x992)+~P2(x993)+P1(x991)+~E(x991,f19(x992,x993)) % 0.53/0.64 [100]~P1(x1002)+~P2(x1003)+P1(x1001)+~E(x1001,f20(x1002,x1003)) % 0.53/0.64 [101]~P2(x1013)+~P3(x1012)+P1(x1011)+~E(x1011,f3(x1012,x1013)) % 0.53/0.64 [111]~P1(x1112)+P1(x1111)+~P4(x1113,a24)+~E(x1111,f23(x1112,x1113)) % 0.53/0.64 [117]~P4(x1171,x1172)+~P4(x1173,a24)+P4(x1171,a24)+~E(x1172,f2(x1173)) % 0.53/0.64 [131]~P4(x1311,x1313)+~P4(x1312,a24)+P9(f28(x1311),x1312)+~E(x1313,f2(x1312)) % 0.53/0.64 [114]~P1(x1142)+~P1(x1141)+~P7(x1142,x1141)+~P7(x1141,x1142)+E(x1141,x1142) % 0.53/0.64 [145]~P9(x1452,x1451)+~P9(x1451,x1452)+E(x1451,x1452)+~P4(x1452,a24)+~P4(x1451,a24) % 0.53/0.64 [105]~P5(x1051)+P4(x1052,x1051)+~E(x1052,f30(x1051))+~P7(x1051,a24)+E(x1051,a22) % 0.53/0.64 [122]~P1(x1222)+~P6(x1222)+~P4(x1221,a24)+E(x1221,a1)+P6(f23(x1222,x1221)) % 0.53/0.64 [149]~P4(x1492,x1491)+P4(f15(x1491,x1492),x1491)+~P7(x1491,a24)+E(x1491,a22)+E(x1492,f29(x1491)) % 0.53/0.64 [159]~P1(x1591)+~P5(x1591)+~P4(x1592,a24)+~P9(x1592,f9(x1591))+P7(f16(x1591,x1592),x1591) % 0.53/0.64 [161]~P1(x1611)+P4(f18(x1612,x1611),x1611)+~P4(x1612,a24)+E(x1611,f2(x1612))+P4(f18(x1612,x1611),a24) % 0.53/0.64 [162]~P4(x1622,x1621)+~P7(x1621,a24)+~P9(x1622,f15(x1621,x1622))+E(x1621,a22)+E(x1622,f29(x1621)) % 0.53/0.64 [136]P4(x1362,x1361)+~P1(x1361)+~P2(x1362)+~P5(x1361)+E(f9(f19(x1361,x1362)),f28(f9(x1361))) % 0.53/0.64 [156]~P1(x1561)+~P5(x1561)+~P4(x1562,a24)+~P9(x1562,f9(x1561))+E(f9(f16(x1561,x1562)),x1562) % 0.53/0.64 [163]E(x1631,x1632)+P4(x1631,f2(x1632))+~P4(x1632,a24)+~P4(x1631,a24)+~P4(x1631,f2(f28(x1632))) % 0.53/0.64 [167]~P1(x1671)+P4(f18(x1672,x1671),x1671)+~P4(x1672,a24)+E(x1671,f2(x1672))+P9(f28(f18(x1672,x1671)),x1672) % 0.53/0.64 [125]~P4(x1253,x1251)+P9(x1252,x1253)+~E(x1252,f29(x1251))+~P7(x1251,a24)+E(x1251,a22) % 0.53/0.64 [151]P4(x1511,x1512)+~P4(x1513,a24)+~P4(x1511,a24)+~P9(f28(x1511),x1513)+~E(x1512,f2(x1513)) % 0.53/0.64 [169]~P1(x1691)+~P5(x1693)+~P4(x1692,a24)+~P7(x1693,f23(x1691,x1692))+P5(f6(x1691,x1692,x1693)) % 0.53/0.64 [170]~P1(x1701)+~P5(x1703)+~P4(x1702,a24)+~P7(x1703,f23(x1701,x1702))+P7(f6(x1701,x1702,x1703),x1701) % 0.53/0.64 [181]~P1(x1812)+~P5(x1811)+~P4(x1813,a24)+~P7(x1811,f23(x1812,x1813))+P7(x1811,f23(f6(x1812,x1813,x1811),x1813)) % 0.53/0.64 [118]~P1(x1184)+~P2(x1182)+~P4(x1181,x1183)+~E(x1181,x1182)+~E(x1183,f20(x1184,x1182)) % 0.53/0.64 [120]~P1(x1203)+~P2(x1204)+~P4(x1201,x1202)+P2(x1201)+~E(x1202,f19(x1203,x1204)) % 0.53/0.64 [121]~P1(x1213)+~P2(x1214)+~P4(x1211,x1212)+P2(x1211)+~E(x1212,f20(x1213,x1214)) % 0.53/0.64 [133]~P1(x1332)+~P2(x1334)+~P4(x1331,x1333)+P4(x1331,x1332)+~E(x1333,f20(x1332,x1334)) % 0.53/0.64 [135]~P2(x1353)+~P3(x1351)+~P4(x1352,x1354)+E(f21(x1351,x1352),x1353)+~E(x1354,f3(x1351,x1353)) % 0.53/0.64 [139]~P1(x1394)+~P4(x1391,x1393)+~P4(x1392,a24)+E(f9(x1391),x1392)+~E(x1393,f23(x1394,x1392)) % 0.53/0.64 [141]~P2(x1414)+~P3(x1412)+~P4(x1411,x1413)+P4(x1411,f25(x1412))+~E(x1413,f3(x1412,x1414)) % 0.53/0.64 [146]~P1(x1462)+~P4(x1461,x1463)+P7(x1461,x1462)+~P4(x1464,a24)+~E(x1463,f23(x1462,x1464)) % 0.53/0.64 [155]~P5(x1551)+~P4(x1552,x1551)+P4(f17(x1551,x1552),x1551)+~P7(x1551,a24)+E(x1551,a22)+E(x1552,f30(x1551)) % 0.53/0.64 [165]~P5(x1651)+~P4(x1652,x1651)+~P7(x1651,a24)+~P9(f17(x1651,x1652),x1652)+E(x1651,a22)+E(x1652,f30(x1651)) % 0.53/0.64 [174]~P1(x1741)+~P4(x1742,a24)+~P4(f18(x1742,x1741),x1741)+E(x1741,f2(x1742))+~P4(f18(x1742,x1741),a24)+~P9(f28(f18(x1742,x1741)),x1742) % 0.53/0.64 [140]~P1(x1402)+~P1(x1401)+~P7(x1403,x1402)+~P7(x1401,x1403)+P7(x1401,x1402)+~P1(x1403) % 0.53/0.64 [166]~P9(x1661,x1663)+P9(x1661,x1662)+~P9(x1663,x1662)+~P4(x1662,a24)+~P4(x1663,a24)+~P4(x1661,a24) % 0.53/0.64 [132]~P5(x1321)+~P4(x1322,x1321)+P9(x1322,x1323)+~E(x1323,f30(x1321))+~P7(x1321,a24)+E(x1321,a22) % 0.53/0.64 [171]~P1(x1711)+~P1(x1712)+~P2(x1713)+P4(f13(x1712,x1713,x1711),x1711)+~E(f13(x1712,x1713,x1711),x1713)+E(x1711,f20(x1712,x1713)) % 0.53/0.64 [172]~P1(x1721)+~P1(x1722)+~P2(x1723)+P4(f14(x1722,x1723,x1721),x1721)+E(x1721,f19(x1722,x1723))+P2(f14(x1722,x1723,x1721)) % 0.53/0.64 [173]~P1(x1731)+~P1(x1732)+~P2(x1733)+P4(f13(x1732,x1733,x1731),x1731)+E(x1731,f20(x1732,x1733))+P2(f13(x1732,x1733,x1731)) % 0.53/0.64 [175]~P1(x1751)+~P1(x1752)+~P2(x1753)+P4(f13(x1752,x1753,x1751),x1751)+P4(f13(x1752,x1753,x1751),x1752)+E(x1751,f20(x1752,x1753)) % 0.53/0.64 [178]~P1(x1781)+~P2(x1783)+~P3(x1782)+P4(f8(x1782,x1783,x1781),x1781)+P4(f8(x1782,x1783,x1781),f25(x1782))+E(x1781,f3(x1782,x1783)) % 0.53/0.64 [179]~P1(x1791)+~P1(x1792)+P4(f7(x1792,x1793,x1791),x1791)+P7(f7(x1792,x1793,x1791),x1792)+~P4(x1793,a24)+E(x1791,f23(x1792,x1793)) % 0.53/0.64 [176]~P1(x1761)+~P2(x1763)+~P3(x1762)+P4(f8(x1762,x1763,x1761),x1761)+E(x1761,f3(x1762,x1763))+E(f21(x1762,f8(x1762,x1763,x1761)),x1763) % 0.53/0.64 [177]~P1(x1771)+~P1(x1772)+P4(f7(x1772,x1773,x1771),x1771)+~P4(x1773,a24)+E(x1771,f23(x1772,x1773))+E(f9(f7(x1772,x1773,x1771)),x1773) % 0.53/0.64 [115]~P1(x1154)+~P2(x1153)+~P2(x1151)+P4(x1151,x1152)+~E(x1151,x1153)+~E(x1152,f19(x1154,x1153)) % 0.53/0.64 [138]~P1(x1383)+~P2(x1382)+~P4(x1381,x1384)+E(x1381,x1382)+P4(x1381,x1383)+~E(x1384,f19(x1383,x1382)) % 0.53/0.64 [143]~P1(x1433)+~P2(x1434)+~P2(x1431)+~P4(x1431,x1433)+P4(x1431,x1432)+~E(x1432,f19(x1433,x1434)) % 0.53/0.64 [154]~P1(x1544)+~P7(x1541,x1544)+P4(x1541,x1542)+~P4(x1543,a24)+~E(x1542,f23(x1544,x1543))+~E(f9(x1541),x1543) % 0.53/0.64 [160]~P2(x1604)+~P3(x1603)+P4(x1601,x1602)+~E(f21(x1603,x1601),x1604)+~P4(x1601,f25(x1603))+~E(x1602,f3(x1603,x1604)) % 0.53/0.64 [164]E(f29(x1642),f29(x1641))+~P7(x1641,a24)+~P7(x1642,a24)+~P4(f29(x1641),x1642)+~P4(f29(x1642),x1641)+E(x1641,a22)+E(x1642,a22) % 0.53/0.64 [168]~P1(x1683)+~P1(x1682)+P7(x1682,x1683)+~P4(x1681,a24)+~P7(f23(x1682,x1681),f23(x1683,x1681))+E(x1681,a1)+E(f23(x1682,x1681),a22) % 0.53/0.64 [180]~P1(x1801)+~P1(x1802)+~P2(x1803)+E(f14(x1802,x1803,x1801),x1803)+P4(f14(x1802,x1803,x1801),x1801)+P4(f14(x1802,x1803,x1801),x1802)+E(x1801,f19(x1802,x1803)) % 0.53/0.64 [182]~P1(x1821)+~P1(x1822)+~P2(x1823)+~E(f14(x1822,x1823,x1821),x1823)+~P4(f14(x1822,x1823,x1821),x1821)+E(x1821,f19(x1822,x1823))+~P2(f14(x1822,x1823,x1821)) % 0.53/0.64 [183]~P1(x1831)+~P1(x1832)+~P2(x1833)+~P4(f14(x1832,x1833,x1831),x1831)+~P4(f14(x1832,x1833,x1831),x1832)+E(x1831,f19(x1832,x1833))+~P2(f14(x1832,x1833,x1831)) % 0.53/0.64 [184]~P1(x1841)+~P1(x1842)+~P4(x1843,a24)+~P4(f7(x1842,x1843,x1841),x1841)+~P7(f7(x1842,x1843,x1841),x1842)+E(x1841,f23(x1842,x1843))+~E(f9(f7(x1842,x1843,x1841)),x1843) % 0.53/0.64 [185]~P1(x1851)+~P2(x1853)+~P3(x1852)+~P4(f8(x1852,x1853,x1851),x1851)+~P4(f8(x1852,x1853,x1851),f25(x1852))+E(x1851,f3(x1852,x1853))+~E(f21(x1852,f8(x1852,x1853,x1851)),x1853) % 0.53/0.64 [144]~P1(x1444)+~P2(x1442)+~P2(x1441)+~P4(x1441,x1444)+E(x1441,x1442)+P4(x1441,x1443)+~E(x1443,f20(x1444,x1442)) % 0.53/0.64 [186]~P1(x1861)+~P1(x1862)+~P2(x1863)+E(f13(x1862,x1863,x1861),x1863)+~P4(f13(x1862,x1863,x1861),x1861)+~P4(f13(x1862,x1863,x1861),x1862)+E(x1861,f20(x1862,x1863))+~P2(f13(x1862,x1863,x1861)) % 0.53/0.64 %EqnAxiom % 0.53/0.64 [1]E(x11,x11) % 0.53/0.64 [2]E(x22,x21)+~E(x21,x22) % 0.53/0.64 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.53/0.64 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.53/0.64 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53)) % 0.53/0.64 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62)) % 0.53/0.64 [7]~E(x71,x72)+E(f19(x71,x73),f19(x72,x73)) % 0.53/0.64 [8]~E(x81,x82)+E(f19(x83,x81),f19(x83,x82)) % 0.53/0.64 [9]~E(x91,x92)+E(f25(x91),f25(x92)) % 0.53/0.64 [10]~E(x101,x102)+E(f14(x101,x103,x104),f14(x102,x103,x104)) % 0.53/0.64 [11]~E(x111,x112)+E(f14(x113,x111,x114),f14(x113,x112,x114)) % 0.53/0.64 [12]~E(x121,x122)+E(f14(x123,x124,x121),f14(x123,x124,x122)) % 0.53/0.64 [13]~E(x131,x132)+E(f8(x131,x133,x134),f8(x132,x133,x134)) % 0.53/0.64 [14]~E(x141,x142)+E(f8(x143,x141,x144),f8(x143,x142,x144)) % 0.53/0.64 [15]~E(x151,x152)+E(f8(x153,x154,x151),f8(x153,x154,x152)) % 0.53/0.64 [16]~E(x161,x162)+E(f9(x161),f9(x162)) % 0.53/0.64 [17]~E(x171,x172)+E(f23(x171,x173),f23(x172,x173)) % 0.53/0.64 [18]~E(x181,x182)+E(f23(x183,x181),f23(x183,x182)) % 0.53/0.64 [19]~E(x191,x192)+E(f13(x191,x193,x194),f13(x192,x193,x194)) % 0.53/0.64 [20]~E(x201,x202)+E(f13(x203,x201,x204),f13(x203,x202,x204)) % 0.53/0.64 [21]~E(x211,x212)+E(f13(x213,x214,x211),f13(x213,x214,x212)) % 0.53/0.64 [22]~E(x221,x222)+E(f28(x221),f28(x222)) % 0.53/0.64 [23]~E(x231,x232)+E(f12(x231,x233),f12(x232,x233)) % 0.53/0.64 [24]~E(x241,x242)+E(f12(x243,x241),f12(x243,x242)) % 0.53/0.64 [25]~E(x251,x252)+E(f15(x251,x253),f15(x252,x253)) % 0.53/0.64 [26]~E(x261,x262)+E(f15(x263,x261),f15(x263,x262)) % 0.53/0.64 [27]~E(x271,x272)+E(f10(x271),f10(x272)) % 0.53/0.64 [28]~E(x281,x282)+E(f17(x281,x283),f17(x282,x283)) % 0.53/0.64 [29]~E(x291,x292)+E(f17(x293,x291),f17(x293,x292)) % 0.53/0.64 [30]~E(x301,x302)+E(f30(x301),f30(x302)) % 0.53/0.64 [31]~E(x311,x312)+E(f18(x311,x313),f18(x312,x313)) % 0.53/0.64 [32]~E(x321,x322)+E(f18(x323,x321),f18(x323,x322)) % 0.53/0.64 [33]~E(x331,x332)+E(f11(x331),f11(x332)) % 0.53/0.64 [34]~E(x341,x342)+E(f29(x341),f29(x342)) % 0.53/0.64 [35]~E(x351,x352)+E(f16(x351,x353),f16(x352,x353)) % 0.53/0.64 [36]~E(x361,x362)+E(f16(x363,x361),f16(x363,x362)) % 0.53/0.64 [37]~E(x371,x372)+E(f20(x371,x373),f20(x372,x373)) % 0.53/0.64 [38]~E(x381,x382)+E(f20(x383,x381),f20(x383,x382)) % 0.53/0.64 [39]~E(x391,x392)+E(f21(x391,x393),f21(x392,x393)) % 0.53/0.64 [40]~E(x401,x402)+E(f21(x403,x401),f21(x403,x402)) % 0.53/0.64 [41]~E(x411,x412)+E(f6(x411,x413,x414),f6(x412,x413,x414)) % 0.53/0.64 [42]~E(x421,x422)+E(f6(x423,x421,x424),f6(x423,x422,x424)) % 0.53/0.64 [43]~E(x431,x432)+E(f6(x433,x434,x431),f6(x433,x434,x432)) % 0.53/0.64 [44]~E(x441,x442)+E(f5(x441),f5(x442)) % 0.53/0.64 [45]~E(x451,x452)+E(f7(x451,x453,x454),f7(x452,x453,x454)) % 0.53/0.64 [46]~E(x461,x462)+E(f7(x463,x461,x464),f7(x463,x462,x464)) % 0.53/0.64 [47]~E(x471,x472)+E(f7(x473,x474,x471),f7(x473,x474,x472)) % 0.53/0.64 [48]~P1(x481)+P1(x482)+~E(x481,x482) % 0.53/0.64 [49]~P2(x491)+P2(x492)+~E(x491,x492) % 0.53/0.64 [50]~P5(x501)+P5(x502)+~E(x501,x502) % 0.53/0.64 [51]~P6(x511)+P6(x512)+~E(x511,x512) % 0.53/0.64 [52]~P3(x521)+P3(x522)+~E(x521,x522) % 0.53/0.64 [53]P4(x532,x533)+~E(x531,x532)+~P4(x531,x533) % 0.53/0.64 [54]P4(x543,x542)+~E(x541,x542)+~P4(x543,x541) % 0.53/0.64 [55]P7(x552,x553)+~E(x551,x552)+~P7(x551,x553) % 0.53/0.64 [56]P7(x563,x562)+~E(x561,x562)+~P7(x563,x561) % 0.53/0.64 [57]P9(x572,x573)+~E(x571,x572)+~P9(x571,x573) % 0.53/0.64 [58]P9(x583,x582)+~E(x581,x582)+~P9(x583,x581) % 0.53/0.64 [59]P8(x592,x593)+~E(x591,x592)+~P8(x591,x593) % 0.53/0.64 [60]P8(x603,x602)+~E(x601,x602)+~P8(x603,x601) % 0.53/0.64 % 0.53/0.64 %------------------------------------------- % 0.53/0.64 cnf(215,plain, % 0.53/0.64 ($false), % 0.53/0.64 inference(scs_inference,[],[69,70,130]), % 0.53/0.64 ['proof']). % 0.53/0.64 % SZS output end Proof % 0.53/0.64 % Total time :0.010000s %------------------------------------------------------------------------------