%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM555+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 12:25:00 EDT 2024 % Result : Theorem 0.48s 0.65s % Output : CNFRefutation 0.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : NUM555+1 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.31 % Computer : n024.cluster.edu % 0.11/0.31 % Model : x86_64 x86_64 % 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.31 % Memory : 8042.1875MB % 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.31 % CPULimit : 300 % 0.11/0.31 % WCLimit : 300 % 0.11/0.31 % DateTime : Sat Jun 22 21:56:39 EDT 2024 % 0.16/0.31 % CPUTime : % 0.16/0.55 start to proof:theBenchmark % 0.48/0.63 %------------------------------------------- % 0.48/0.63 % File :CSE---1.7 % 0.48/0.63 % Problem :theBenchmark % 0.48/0.63 % Transform :cnf % 0.48/0.63 % Format :tptp:raw % 0.48/0.63 % Command :java -jar mcs_scs.jar %d %s % 0.48/0.63 % 0.48/0.63 % Result :Theorem 0.010000s % 0.48/0.63 % Output :CNFRefutation 0.010000s % 0.48/0.63 %------------------------------------------- % 0.48/0.63 %------------------------------------------------------------------------------ % 0.48/0.63 % File : NUM555+1 : TPTP v8.2.0. Released v4.0.0. % 0.48/0.64 % Domain : Number Theory % 0.48/0.64 % Problem : Ramsey's Infinite Theorem 12_05_02_01, 00 expansion % 0.48/0.64 % Version : Especial. % 0.48/0.64 % English : % 0.48/0.64 % 0.48/0.64 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 0.48/0.64 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 0.48/0.64 % Source : [Pas08] % 0.48/0.64 % Names : ramsey_12_05_02_01.00 [Pas08] % 0.48/0.64 % 0.48/0.64 % Status : Theorem % 0.48/0.64 % Rating : 0.22 v8.2.0, 0.25 v8.1.0, 0.22 v7.4.0, 0.17 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.17 v6.2.0, 0.28 v6.1.0, 0.33 v6.0.0, 0.22 v5.5.0, 0.26 v5.4.0, 0.29 v5.3.0, 0.37 v5.2.0, 0.20 v5.1.0, 0.29 v5.0.0, 0.38 v4.1.0, 0.48 v4.0.1, 0.70 v4.0.0 % 0.48/0.64 % Syntax : Number of formulae : 71 ( 10 unt; 8 def) % 0.48/0.64 % Number of atoms : 245 ( 40 equ) % 0.48/0.64 % Maximal formula atoms : 8 ( 3 avg) % 0.48/0.64 % Number of connectives : 195 ( 21 ~; 4 |; 69 &) % 0.48/0.64 % ( 17 <=>; 84 =>; 0 <=; 0 <~>) % 0.48/0.64 % Maximal formula depth : 12 ( 5 avg) % 0.48/0.64 % Maximal term depth : 4 ( 1 avg) % 0.48/0.64 % Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty) % 0.48/0.64 % Number of functors : 18 ( 18 usr; 10 con; 0-2 aty) % 0.48/0.64 % Number of variables : 106 ( 102 !; 4 ?) % 0.48/0.64 % SPC : FOF_THM_RFO_SEQ % 0.48/0.64 % 0.48/0.64 % Comments : Problem generated by the SAD system [VLP07] % 0.48/0.64 %------------------------------------------------------------------------------ % 0.48/0.64 fof(mSetSort,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aSet0(W0) % 0.48/0.64 => $true ) ). % 0.48/0.64 % 0.48/0.64 fof(mElmSort,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aElement0(W0) % 0.48/0.64 => $true ) ). % 0.48/0.64 % 0.48/0.64 fof(mEOfElem,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aSet0(W0) % 0.48/0.64 => ! [W1] : % 0.48/0.64 ( aElementOf0(W1,W0) % 0.48/0.64 => aElement0(W1) ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mFinRel,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aSet0(W0) % 0.48/0.64 => ( isFinite0(W0) % 0.48/0.64 => $true ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mDefEmp,definition, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( W0 = slcrc0 % 0.48/0.64 <=> ( aSet0(W0) % 0.48/0.64 & ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mEmpFin,axiom, % 0.48/0.64 isFinite0(slcrc0) ). % 0.48/0.64 % 0.48/0.64 fof(mCntRel,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aSet0(W0) % 0.48/0.64 => ( isCountable0(W0) % 0.48/0.64 => $true ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mCountNFin,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( ( aSet0(W0) % 0.48/0.64 & isCountable0(W0) ) % 0.48/0.64 => ~ isFinite0(W0) ) ). % 0.48/0.64 % 0.48/0.64 fof(mCountNFin_01,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( ( aSet0(W0) % 0.48/0.64 & isCountable0(W0) ) % 0.48/0.64 => W0 != slcrc0 ) ). % 0.48/0.64 % 0.48/0.64 fof(mDefSub,definition, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aSet0(W0) % 0.48/0.64 => ! [W1] : % 0.48/0.64 ( aSubsetOf0(W1,W0) % 0.48/0.64 <=> ( aSet0(W1) % 0.48/0.64 & ! [W2] : % 0.48/0.64 ( aElementOf0(W2,W1) % 0.48/0.64 => aElementOf0(W2,W0) ) ) ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mSubFSet,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( ( aSet0(W0) % 0.48/0.64 & isFinite0(W0) ) % 0.48/0.64 => ! [W1] : % 0.48/0.64 ( aSubsetOf0(W1,W0) % 0.48/0.64 => isFinite0(W1) ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mSubRefl,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aSet0(W0) % 0.48/0.64 => aSubsetOf0(W0,W0) ) ). % 0.48/0.64 % 0.48/0.64 fof(mSubASymm,axiom, % 0.48/0.64 ! [W0,W1] : % 0.48/0.64 ( ( aSet0(W0) % 0.48/0.64 & aSet0(W1) ) % 0.48/0.64 => ( ( aSubsetOf0(W0,W1) % 0.48/0.64 & aSubsetOf0(W1,W0) ) % 0.48/0.64 => W0 = W1 ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mSubTrans,axiom, % 0.48/0.64 ! [W0,W1,W2] : % 0.48/0.64 ( ( aSet0(W0) % 0.48/0.64 & aSet0(W1) % 0.48/0.64 & aSet0(W2) ) % 0.48/0.64 => ( ( aSubsetOf0(W0,W1) % 0.48/0.64 & aSubsetOf0(W1,W2) ) % 0.48/0.64 => aSubsetOf0(W0,W2) ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mDefCons,definition, % 0.48/0.64 ! [W0,W1] : % 0.48/0.64 ( ( aSet0(W0) % 0.48/0.64 & aElement0(W1) ) % 0.48/0.64 => ! [W2] : % 0.48/0.64 ( W2 = sdtpldt0(W0,W1) % 0.48/0.64 <=> ( aSet0(W2) % 0.48/0.64 & ! [W3] : % 0.48/0.64 ( aElementOf0(W3,W2) % 0.48/0.64 <=> ( aElement0(W3) % 0.48/0.64 & ( aElementOf0(W3,W0) % 0.48/0.64 | W3 = W1 ) ) ) ) ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mDefDiff,definition, % 0.48/0.64 ! [W0,W1] : % 0.48/0.64 ( ( aSet0(W0) % 0.48/0.64 & aElement0(W1) ) % 0.48/0.64 => ! [W2] : % 0.48/0.64 ( W2 = sdtmndt0(W0,W1) % 0.48/0.64 <=> ( aSet0(W2) % 0.48/0.64 & ! [W3] : % 0.48/0.64 ( aElementOf0(W3,W2) % 0.48/0.64 <=> ( aElement0(W3) % 0.48/0.64 & aElementOf0(W3,W0) % 0.48/0.64 & W3 != W1 ) ) ) ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mConsDiff,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aSet0(W0) % 0.48/0.64 => ! [W1] : % 0.48/0.64 ( aElementOf0(W1,W0) % 0.48/0.64 => sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mDiffCons,axiom, % 0.48/0.64 ! [W0,W1] : % 0.48/0.64 ( ( aElement0(W0) % 0.48/0.64 & aSet0(W1) ) % 0.48/0.64 => ( ~ aElementOf0(W0,W1) % 0.48/0.64 => sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mCConsSet,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aElement0(W0) % 0.48/0.64 => ! [W1] : % 0.48/0.64 ( ( aSet0(W1) % 0.48/0.64 & isCountable0(W1) ) % 0.48/0.64 => isCountable0(sdtpldt0(W1,W0)) ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mCDiffSet,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aElement0(W0) % 0.48/0.64 => ! [W1] : % 0.48/0.64 ( ( aSet0(W1) % 0.48/0.64 & isCountable0(W1) ) % 0.48/0.64 => isCountable0(sdtmndt0(W1,W0)) ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mFConsSet,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aElement0(W0) % 0.48/0.64 => ! [W1] : % 0.48/0.64 ( ( aSet0(W1) % 0.48/0.64 & isFinite0(W1) ) % 0.48/0.64 => isFinite0(sdtpldt0(W1,W0)) ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mFDiffSet,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aElement0(W0) % 0.48/0.64 => ! [W1] : % 0.48/0.64 ( ( aSet0(W1) % 0.48/0.64 & isFinite0(W1) ) % 0.48/0.64 => isFinite0(sdtmndt0(W1,W0)) ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mNATSet,axiom, % 0.48/0.64 ( aSet0(szNzAzT0) % 0.48/0.64 & isCountable0(szNzAzT0) ) ). % 0.48/0.64 % 0.48/0.64 fof(mZeroNum,axiom, % 0.48/0.64 aElementOf0(sz00,szNzAzT0) ). % 0.48/0.64 % 0.48/0.64 fof(mSuccNum,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aElementOf0(W0,szNzAzT0) % 0.48/0.64 => ( aElementOf0(szszuzczcdt0(W0),szNzAzT0) % 0.48/0.64 & szszuzczcdt0(W0) != sz00 ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mSuccEquSucc,axiom, % 0.48/0.64 ! [W0,W1] : % 0.48/0.64 ( ( aElementOf0(W0,szNzAzT0) % 0.48/0.64 & aElementOf0(W1,szNzAzT0) ) % 0.48/0.64 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 0.48/0.64 => W0 = W1 ) ) ). % 0.48/0.64 % 0.48/0.64 fof(mNatExtra,axiom, % 0.48/0.64 ! [W0] : % 0.48/0.64 ( aElementOf0(W0,szNzAzT0) % 0.48/0.64 => ( W0 = sz00 % 0.48/0.64 | ? [W1] : % 0.48/0.64 ( aElementOf0(W1,szNzAzT0) % 0.48/0.64 & W0 = szszuzczcdt0(W1) ) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mNatNSucc,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 => W0 != szszuzczcdt0(W0) ) ). % 0.48/0.65 % 0.48/0.65 fof(mLessRel,axiom, % 0.48/0.65 ! [W0,W1] : % 0.48/0.65 ( ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 & aElementOf0(W1,szNzAzT0) ) % 0.48/0.65 => ( sdtlseqdt0(W0,W1) % 0.48/0.65 => $true ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mZeroLess,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 => sdtlseqdt0(sz00,W0) ) ). % 0.48/0.65 % 0.48/0.65 fof(mNoScLessZr,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 => ~ sdtlseqdt0(szszuzczcdt0(W0),sz00) ) ). % 0.48/0.65 % 0.48/0.65 fof(mSuccLess,axiom, % 0.48/0.65 ! [W0,W1] : % 0.48/0.65 ( ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 & aElementOf0(W1,szNzAzT0) ) % 0.48/0.65 => ( sdtlseqdt0(W0,W1) % 0.48/0.65 <=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mLessSucc,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 => sdtlseqdt0(W0,szszuzczcdt0(W0)) ) ). % 0.48/0.65 % 0.48/0.65 fof(mLessRefl,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 => sdtlseqdt0(W0,W0) ) ). % 0.48/0.65 % 0.48/0.65 fof(mLessASymm,axiom, % 0.48/0.65 ! [W0,W1] : % 0.48/0.65 ( ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 & aElementOf0(W1,szNzAzT0) ) % 0.48/0.65 => ( ( sdtlseqdt0(W0,W1) % 0.48/0.65 & sdtlseqdt0(W1,W0) ) % 0.48/0.65 => W0 = W1 ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mLessTrans,axiom, % 0.48/0.65 ! [W0,W1,W2] : % 0.48/0.65 ( ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 & aElementOf0(W1,szNzAzT0) % 0.48/0.65 & aElementOf0(W2,szNzAzT0) ) % 0.48/0.65 => ( ( sdtlseqdt0(W0,W1) % 0.48/0.65 & sdtlseqdt0(W1,W2) ) % 0.48/0.65 => sdtlseqdt0(W0,W2) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mLessTotal,axiom, % 0.48/0.65 ! [W0,W1] : % 0.48/0.65 ( ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 & aElementOf0(W1,szNzAzT0) ) % 0.48/0.65 => ( sdtlseqdt0(W0,W1) % 0.48/0.65 | sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mIHSort,axiom, % 0.48/0.65 ! [W0,W1] : % 0.48/0.65 ( ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 & aElementOf0(W1,szNzAzT0) ) % 0.48/0.65 => ( iLess0(W0,W1) % 0.48/0.65 => $true ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mIH,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 0.48/0.65 % 0.48/0.65 fof(mCardS,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aSet0(W0) % 0.48/0.65 => aElement0(sbrdtbr0(W0)) ) ). % 0.48/0.65 % 0.48/0.65 fof(mCardNum,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aSet0(W0) % 0.48/0.65 => ( aElementOf0(sbrdtbr0(W0),szNzAzT0) % 0.48/0.65 <=> isFinite0(W0) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mCardEmpty,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aSet0(W0) % 0.48/0.65 => ( sbrdtbr0(W0) = sz00 % 0.48/0.65 <=> W0 = slcrc0 ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mCardCons,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( ( aSet0(W0) % 0.48/0.65 & isFinite0(W0) ) % 0.48/0.65 => ! [W1] : % 0.48/0.65 ( aElement0(W1) % 0.48/0.65 => ( ~ aElementOf0(W1,W0) % 0.48/0.65 => sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mCardDiff,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aSet0(W0) % 0.48/0.65 => ! [W1] : % 0.48/0.65 ( ( isFinite0(W0) % 0.48/0.65 & aElementOf0(W1,W0) ) % 0.48/0.65 => szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mCardSub,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aSet0(W0) % 0.48/0.65 => ! [W1] : % 0.48/0.65 ( ( isFinite0(W0) % 0.48/0.65 & aSubsetOf0(W1,W0) ) % 0.48/0.65 => sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mCardSubEx,axiom, % 0.48/0.65 ! [W0,W1] : % 0.48/0.65 ( ( aSet0(W0) % 0.48/0.65 & aElementOf0(W1,szNzAzT0) ) % 0.48/0.65 => ( ( isFinite0(W0) % 0.48/0.65 & sdtlseqdt0(W1,sbrdtbr0(W0)) ) % 0.48/0.65 => ? [W2] : % 0.48/0.65 ( aSubsetOf0(W2,W0) % 0.48/0.65 & sbrdtbr0(W2) = W1 ) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mDefMin,definition, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( ( aSubsetOf0(W0,szNzAzT0) % 0.48/0.65 & W0 != slcrc0 ) % 0.48/0.65 => ! [W1] : % 0.48/0.65 ( W1 = szmzizndt0(W0) % 0.48/0.65 <=> ( aElementOf0(W1,W0) % 0.48/0.65 & ! [W2] : % 0.48/0.65 ( aElementOf0(W2,W0) % 0.48/0.65 => sdtlseqdt0(W1,W2) ) ) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mDefMax,definition, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( ( aSubsetOf0(W0,szNzAzT0) % 0.48/0.65 & isFinite0(W0) % 0.48/0.65 & W0 != slcrc0 ) % 0.48/0.65 => ! [W1] : % 0.48/0.65 ( W1 = szmzazxdt0(W0) % 0.48/0.65 <=> ( aElementOf0(W1,W0) % 0.48/0.65 & ! [W2] : % 0.48/0.65 ( aElementOf0(W2,W0) % 0.48/0.65 => sdtlseqdt0(W2,W1) ) ) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mMinMin,axiom, % 0.48/0.65 ! [W0,W1] : % 0.48/0.65 ( ( aSubsetOf0(W0,szNzAzT0) % 0.48/0.65 & aSubsetOf0(W1,szNzAzT0) % 0.48/0.65 & W0 != slcrc0 % 0.48/0.65 & W1 != slcrc0 ) % 0.48/0.65 => ( ( aElementOf0(szmzizndt0(W0),W1) % 0.48/0.65 & aElementOf0(szmzizndt0(W1),W0) ) % 0.48/0.65 => szmzizndt0(W0) = szmzizndt0(W1) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mDefSeg,definition, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 => ! [W1] : % 0.48/0.65 ( W1 = slbdtrb0(W0) % 0.48/0.65 <=> ( aSet0(W1) % 0.48/0.65 & ! [W2] : % 0.48/0.65 ( aElementOf0(W2,W1) % 0.48/0.65 <=> ( aElementOf0(W2,szNzAzT0) % 0.48/0.65 & sdtlseqdt0(szszuzczcdt0(W2),W0) ) ) ) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mSegFin,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 => isFinite0(slbdtrb0(W0)) ) ). % 0.48/0.65 % 0.48/0.65 fof(mSegZero,axiom, % 0.48/0.65 slbdtrb0(sz00) = slcrc0 ). % 0.48/0.65 % 0.48/0.65 fof(mSegSucc,axiom, % 0.48/0.65 ! [W0,W1] : % 0.48/0.65 ( ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 & aElementOf0(W1,szNzAzT0) ) % 0.48/0.65 => ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1))) % 0.48/0.65 <=> ( aElementOf0(W0,slbdtrb0(W1)) % 0.48/0.65 | W0 = W1 ) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mSegLess,axiom, % 0.48/0.65 ! [W0,W1] : % 0.48/0.65 ( ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 & aElementOf0(W1,szNzAzT0) ) % 0.48/0.65 => ( sdtlseqdt0(W0,W1) % 0.48/0.65 <=> aSubsetOf0(slbdtrb0(W0),slbdtrb0(W1)) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mFinSubSeg,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( ( aSubsetOf0(W0,szNzAzT0) % 0.48/0.65 & isFinite0(W0) ) % 0.48/0.65 => ? [W1] : % 0.48/0.65 ( aElementOf0(W1,szNzAzT0) % 0.48/0.65 & aSubsetOf0(W0,slbdtrb0(W1)) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mCardSeg,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( aElementOf0(W0,szNzAzT0) % 0.48/0.65 => sbrdtbr0(slbdtrb0(W0)) = W0 ) ). % 0.48/0.65 % 0.48/0.65 fof(mDefSel,definition, % 0.48/0.65 ! [W0,W1] : % 0.48/0.65 ( ( aSet0(W0) % 0.48/0.65 & aElementOf0(W1,szNzAzT0) ) % 0.48/0.65 => ! [W2] : % 0.48/0.65 ( W2 = slbdtsldtrb0(W0,W1) % 0.48/0.65 <=> ( aSet0(W2) % 0.48/0.65 & ! [W3] : % 0.48/0.65 ( aElementOf0(W3,W2) % 0.48/0.65 <=> ( aSubsetOf0(W3,W0) % 0.48/0.65 & sbrdtbr0(W3) = W1 ) ) ) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mSelFSet,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( ( aSet0(W0) % 0.48/0.65 & isFinite0(W0) ) % 0.48/0.65 => ! [W1] : % 0.48/0.65 ( aElementOf0(W1,szNzAzT0) % 0.48/0.65 => isFinite0(slbdtsldtrb0(W0,W1)) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mSelNSet,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( ( aSet0(W0) % 0.48/0.65 & ~ isFinite0(W0) ) % 0.48/0.65 => ! [W1] : % 0.48/0.65 ( aElementOf0(W1,szNzAzT0) % 0.48/0.65 => slbdtsldtrb0(W0,W1) != slcrc0 ) ) ). % 0.48/0.65 % 0.48/0.65 fof(mSelCSet,axiom, % 0.48/0.65 ! [W0] : % 0.48/0.65 ( ( aSet0(W0) % 0.48/0.65 & isCountable0(W0) ) % 0.48/0.65 => ! [W1] : % 0.48/0.65 ( ( aElementOf0(W1,szNzAzT0) % 0.48/0.65 & W1 != sz00 ) % 0.48/0.65 => isCountable0(slbdtsldtrb0(W0,W1)) ) ) ). % 0.48/0.65 % 0.48/0.65 fof(m__2202,hypothesis, % 0.48/0.65 aElementOf0(xk,szNzAzT0) ). % 0.48/0.65 % 0.48/0.65 fof(m__2202_02,hypothesis, % 0.48/0.65 ( aSet0(xS) % 0.48/0.65 & aSet0(xT) % 0.48/0.65 & xk != sz00 ) ). % 0.48/0.65 % 0.48/0.65 fof(m__2227,hypothesis, % 0.48/0.65 ( aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk)) % 0.48/0.65 & slbdtsldtrb0(xS,xk) != slcrc0 ) ). % 0.48/0.65 % 0.48/0.65 fof(m__2256,hypothesis, % 0.48/0.65 aElementOf0(xx,xS) ). % 0.48/0.65 % 0.48/0.65 fof(m__2270,hypothesis, % 0.48/0.65 aElementOf0(xQ,slbdtsldtrb0(xS,xk)) ). % 0.48/0.65 % 0.48/0.65 fof(m__2291,hypothesis, % 0.48/0.65 ( aSet0(xQ) % 0.48/0.65 & isFinite0(xQ) % 0.48/0.65 & sbrdtbr0(xQ) = xk ) ). % 0.48/0.65 % 0.48/0.65 fof(m__2304,hypothesis, % 0.48/0.65 ( aElement0(xy) % 0.48/0.65 & aElementOf0(xy,xQ) ) ). % 0.48/0.65 % 0.48/0.65 fof(m__2323,hypothesis, % 0.48/0.65 ~ aElementOf0(xx,xQ) ). % 0.48/0.65 % 0.48/0.65 fof(m__2338,hypothesis, % 0.48/0.65 ~ aElementOf0(xx,xQ) ). % 0.48/0.65 % 0.48/0.65 fof(m__2357,hypothesis, % 0.48/0.65 xP = sdtpldt0(sdtmndt0(xQ,xy),xx) ). % 0.48/0.65 % 0.48/0.65 fof(m__,conjecture, % 0.48/0.65 ~ aElementOf0(xx,sdtmndt0(xQ,xy)) ). % 0.48/0.65 % 0.48/0.65 %------------------------------------------------------------------------------ % 0.48/0.65 %------------------------------------------- % 0.48/0.65 % Proof found % 0.48/0.65 % SZS status Theorem for theBenchmark % 0.48/0.65 % SZS output start Proof % 0.48/0.65 %ClaNum:169(EqnAxiom:48) % 0.48/0.65 %VarNum:714(SingletonVarNum:218) % 0.48/0.65 %MaxLitNum:8 % 0.48/0.65 %MaxfuncDepth:3 % 0.48/0.65 %SharedTerms:37 % 0.48/0.65 %goalClause: 64 % 0.48/0.65 %singleGoalClaCount:1 % 0.48/0.65 [51]P1(a20) % 0.48/0.65 [52]P1(a26) % 0.48/0.65 [53]P1(a27) % 0.48/0.65 [54]P1(a1) % 0.48/0.65 [55]P2(a28) % 0.48/0.65 [56]P4(a18) % 0.48/0.65 [57]P4(a1) % 0.48/0.65 [58]P5(a20) % 0.48/0.65 [59]P3(a14,a20) % 0.48/0.65 [60]P3(a25,a20) % 0.48/0.65 [61]P3(a29,a26) % 0.48/0.65 [62]P3(a28,a1) % 0.48/0.65 [67]~E(a14,a25) % 0.48/0.65 [70]~P3(a29,a1) % 0.48/0.65 [49]E(f2(a1),a25) % 0.48/0.65 [50]E(f15(a14),a18) % 0.48/0.65 [64]P3(a29,f16(a1,a28)) % 0.48/0.65 [65]P3(a1,f19(a26,a25)) % 0.48/0.65 [66]P6(f19(a26,a25),f19(a27,a25)) % 0.48/0.65 [68]~E(f19(a26,a25),a18) % 0.48/0.65 [63]E(f17(f16(a1,a28),a29),a21) % 0.48/0.65 [71]P1(x711)+~E(x711,a18) % 0.48/0.65 [77]~P1(x771)+P6(x771,x771) % 0.48/0.65 [84]~P3(x841,a20)+P8(a14,x841) % 0.48/0.65 [90]P8(x901,x901)+~P3(x901,a20) % 0.48/0.65 [75]~P1(x751)+P2(f2(x751)) % 0.48/0.65 [79]~P3(x791,a20)+~E(f22(x791),a14) % 0.48/0.65 [80]~P3(x801,a20)+~E(f22(x801),x801) % 0.48/0.65 [82]~P3(x821,a20)+P4(f15(x821)) % 0.48/0.65 [91]~P3(x911,a20)+P3(f22(x911),a20) % 0.48/0.65 [92]~P3(x921,a20)+P8(x921,f22(x921)) % 0.48/0.65 [93]~P3(x931,a20)+P7(x931,f22(x931)) % 0.48/0.65 [101]~P3(x1011,a20)+~P8(f22(x1011),a14) % 0.48/0.65 [83]~P3(x831,a20)+E(f2(f15(x831)),x831) % 0.48/0.65 [78]~P3(x782,x781)+~E(x781,a18) % 0.48/0.65 [74]~P1(x741)+~P5(x741)+~E(x741,a18) % 0.48/0.65 [76]~P4(x761)+~P5(x761)+~P1(x761) % 0.48/0.65 [72]~P1(x721)+~E(x721,a18)+E(f2(x721),a14) % 0.48/0.65 [73]~P1(x731)+E(x731,a18)+~E(f2(x731),a14) % 0.48/0.65 [81]~P1(x811)+P3(f3(x811),x811)+E(x811,a18) % 0.48/0.65 [87]~P1(x871)+~P4(x871)+P3(f2(x871),a20) % 0.48/0.65 [94]~P3(x941,a20)+E(x941,a14)+P3(f6(x941),a20) % 0.48/0.65 [95]~P1(x951)+P4(x951)+~P3(f2(x951),a20) % 0.48/0.65 [100]~P4(x1001)+~P6(x1001,a20)+P3(f4(x1001),a20) % 0.48/0.65 [85]~P3(x851,a20)+E(x851,a14)+E(f22(f6(x851)),x851) % 0.48/0.65 [110]~P4(x1101)+~P6(x1101,a20)+P6(x1101,f15(f4(x1101))) % 0.48/0.65 [88]~P6(x881,x882)+P1(x881)+~P1(x882) % 0.48/0.65 [89]~P3(x891,x892)+P2(x891)+~P1(x892) % 0.48/0.65 [86]P1(x861)+~P3(x862,a20)+~E(x861,f15(x862)) % 0.48/0.65 [124]~P1(x1241)+~P3(x1242,x1241)+E(f17(f16(x1241,x1242),x1242),x1241) % 0.48/0.65 [96]~P4(x962)+~P6(x961,x962)+P4(x961)+~P1(x962) % 0.48/0.65 [99]P3(x992,x991)+~E(x992,f23(x991))+~P6(x991,a20)+E(x991,a18) % 0.48/0.65 [103]~P1(x1031)+~P2(x1032)+~P4(x1031)+P4(f17(x1031,x1032)) % 0.48/0.65 [104]~P1(x1041)+~P2(x1042)+~P4(x1041)+P4(f16(x1041,x1042)) % 0.48/0.65 [105]~P1(x1051)+~P2(x1052)+~P5(x1051)+P5(f17(x1051,x1052)) % 0.48/0.65 [106]~P1(x1061)+~P2(x1062)+~P5(x1061)+P5(f16(x1061,x1062)) % 0.48/0.65 [107]~P1(x1071)+P4(x1071)+~P3(x1072,a20)+~E(f19(x1071,x1072),a18) % 0.48/0.65 [109]E(x1091,x1092)+~E(f22(x1091),f22(x1092))+~P3(x1092,a20)+~P3(x1091,a20) % 0.48/0.65 [113]~P1(x1132)+~P4(x1132)+~P6(x1131,x1132)+P8(f2(x1131),f2(x1132)) % 0.48/0.65 [116]~P1(x1161)+~P4(x1161)+~P3(x1162,a20)+P4(f19(x1161,x1162)) % 0.48/0.65 [122]~P1(x1221)+~P1(x1222)+P6(x1221,x1222)+P3(f7(x1222,x1221),x1221) % 0.48/0.65 [128]P8(x1281,x1282)+P8(f22(x1282),x1281)+~P3(x1282,a20)+~P3(x1281,a20) % 0.48/0.65 [138]~P8(x1381,x1382)+~P3(x1382,a20)+~P3(x1381,a20)+P6(f15(x1381),f15(x1382)) % 0.48/0.65 [139]~P8(x1391,x1392)+~P3(x1392,a20)+~P3(x1391,a20)+P8(f22(x1391),f22(x1392)) % 0.48/0.65 [141]~P1(x1411)+~P1(x1412)+P6(x1411,x1412)+~P3(f7(x1412,x1411),x1412) % 0.48/0.65 [143]P8(x1431,x1432)+~P3(x1432,a20)+~P3(x1431,a20)+~P6(f15(x1431),f15(x1432)) % 0.48/0.65 [144]P8(x1441,x1442)+~P3(x1442,a20)+~P3(x1441,a20)+~P8(f22(x1441),f22(x1442)) % 0.48/0.65 [123]P3(x1232,x1231)+~P1(x1231)+~P2(x1232)+E(f16(f17(x1231,x1232),x1232),x1231) % 0.48/0.65 [130]~E(x1301,x1302)+~P3(x1302,a20)+~P3(x1301,a20)+P3(x1301,f15(f22(x1302))) % 0.48/0.65 [149]~P3(x1492,a20)+~P3(x1491,a20)+~P3(x1491,f15(x1492))+P3(x1491,f15(f22(x1492))) % 0.48/0.65 [148]~P1(x1481)+~P4(x1481)+~P3(x1482,x1481)+E(f22(f2(f16(x1481,x1482))),f2(x1481)) % 0.48/0.65 [120]~P1(x1202)+~P6(x1203,x1202)+P3(x1201,x1202)+~P3(x1201,x1203) % 0.48/0.65 [97]~P1(x972)+~P2(x973)+P1(x971)+~E(x971,f17(x972,x973)) % 0.48/0.65 [98]~P1(x982)+~P2(x983)+P1(x981)+~E(x981,f16(x982,x983)) % 0.48/0.65 [108]~P1(x1082)+P1(x1081)+~P3(x1083,a20)+~E(x1081,f19(x1082,x1083)) % 0.48/0.65 [114]~P3(x1141,x1142)+~P3(x1143,a20)+P3(x1141,a20)+~E(x1142,f15(x1143)) % 0.48/0.65 [125]~P3(x1251,x1253)+~P3(x1252,a20)+P8(f22(x1251),x1252)+~E(x1253,f15(x1252)) % 0.48/0.65 [111]~P1(x1112)+~P1(x1111)+~P6(x1112,x1111)+~P6(x1111,x1112)+E(x1111,x1112) % 0.48/0.65 [136]~P8(x1362,x1361)+~P8(x1361,x1362)+E(x1361,x1362)+~P3(x1362,a20)+~P3(x1361,a20) % 0.48/0.65 [102]~P4(x1021)+P3(x1022,x1021)+~E(x1022,f24(x1021))+~P6(x1021,a20)+E(x1021,a18) % 0.48/0.65 [119]~P1(x1192)+~P5(x1192)+~P3(x1191,a20)+E(x1191,a14)+P5(f19(x1192,x1191)) % 0.48/0.65 [140]~P3(x1402,x1401)+P3(f10(x1401,x1402),x1401)+~P6(x1401,a20)+E(x1401,a18)+E(x1402,f23(x1401)) % 0.48/0.65 [150]~P1(x1501)+~P4(x1501)+~P3(x1502,a20)+~P8(x1502,f2(x1501))+P6(f11(x1501,x1502),x1501) % 0.48/0.65 [151]~P1(x1511)+P3(f13(x1512,x1511),x1511)+~P3(x1512,a20)+E(x1511,f15(x1512))+P3(f13(x1512,x1511),a20) % 0.48/0.65 [152]~P3(x1522,x1521)+~P6(x1521,a20)+~P8(x1522,f10(x1521,x1522))+E(x1521,a18)+E(x1522,f23(x1521)) % 0.48/0.65 [129]P3(x1292,x1291)+~P1(x1291)+~P2(x1292)+~P4(x1291)+E(f2(f17(x1291,x1292)),f22(f2(x1291))) % 0.48/0.65 [147]~P1(x1471)+~P4(x1471)+~P3(x1472,a20)+~P8(x1472,f2(x1471))+E(f2(f11(x1471,x1472)),x1472) % 0.48/0.65 [153]E(x1531,x1532)+P3(x1531,f15(x1532))+~P3(x1532,a20)+~P3(x1531,a20)+~P3(x1531,f15(f22(x1532))) % 0.48/0.65 [157]~P1(x1571)+P3(f13(x1572,x1571),x1571)+~P3(x1572,a20)+E(x1571,f15(x1572))+P8(f22(f13(x1572,x1571)),x1572) % 0.48/0.65 [121]~P3(x1213,x1211)+P8(x1212,x1213)+~E(x1212,f23(x1211))+~P6(x1211,a20)+E(x1211,a18) % 0.48/0.65 [142]P3(x1421,x1422)+~P3(x1423,a20)+~P3(x1421,a20)+~P8(f22(x1421),x1423)+~E(x1422,f15(x1423)) % 0.48/0.65 [115]~P1(x1154)+~P2(x1152)+~P3(x1151,x1153)+~E(x1151,x1152)+~E(x1153,f16(x1154,x1152)) % 0.48/0.65 [117]~P1(x1173)+~P2(x1174)+~P3(x1171,x1172)+P2(x1171)+~E(x1172,f17(x1173,x1174)) % 0.48/0.65 [118]~P1(x1183)+~P2(x1184)+~P3(x1181,x1182)+P2(x1181)+~E(x1182,f16(x1183,x1184)) % 0.48/0.65 [127]~P1(x1272)+~P2(x1274)+~P3(x1271,x1273)+P3(x1271,x1272)+~E(x1273,f16(x1272,x1274)) % 0.48/0.65 [132]~P1(x1324)+~P3(x1321,x1323)+~P3(x1322,a20)+E(f2(x1321),x1322)+~E(x1323,f19(x1324,x1322)) % 0.48/0.65 [137]~P1(x1372)+~P3(x1371,x1373)+P6(x1371,x1372)+~P3(x1374,a20)+~E(x1373,f19(x1372,x1374)) % 0.48/0.65 [146]~P4(x1461)+~P3(x1462,x1461)+P3(f12(x1461,x1462),x1461)+~P6(x1461,a20)+E(x1461,a18)+E(x1462,f24(x1461)) % 0.48/0.65 [155]~P4(x1551)+~P3(x1552,x1551)+~P6(x1551,a20)+~P8(f12(x1551,x1552),x1552)+E(x1551,a18)+E(x1552,f24(x1551)) % 0.48/0.65 [161]~P1(x1611)+~P3(x1612,a20)+~P3(f13(x1612,x1611),x1611)+E(x1611,f15(x1612))+~P3(f13(x1612,x1611),a20)+~P8(f22(f13(x1612,x1611)),x1612) % 0.48/0.65 [133]~P1(x1332)+~P1(x1331)+~P6(x1333,x1332)+~P6(x1331,x1333)+P6(x1331,x1332)+~P1(x1333) % 0.48/0.65 [156]~P8(x1561,x1563)+P8(x1561,x1562)+~P8(x1563,x1562)+~P3(x1562,a20)+~P3(x1563,a20)+~P3(x1561,a20) % 0.48/0.65 [126]~P4(x1261)+~P3(x1262,x1261)+P8(x1262,x1263)+~E(x1263,f24(x1261))+~P6(x1261,a20)+E(x1261,a18) % 0.48/0.65 [158]~P1(x1581)+~P1(x1582)+~P2(x1583)+P3(f8(x1582,x1583,x1581),x1581)+~E(f8(x1582,x1583,x1581),x1583)+E(x1581,f16(x1582,x1583)) % 0.48/0.65 [159]~P1(x1591)+~P1(x1592)+~P2(x1593)+P3(f9(x1592,x1593,x1591),x1591)+E(x1591,f17(x1592,x1593))+P2(f9(x1592,x1593,x1591)) % 0.48/0.65 [160]~P1(x1601)+~P1(x1602)+~P2(x1603)+P3(f8(x1602,x1603,x1601),x1601)+E(x1601,f16(x1602,x1603))+P2(f8(x1602,x1603,x1601)) % 0.48/0.65 [162]~P1(x1621)+~P1(x1622)+~P2(x1623)+P3(f8(x1622,x1623,x1621),x1621)+P3(f8(x1622,x1623,x1621),x1622)+E(x1621,f16(x1622,x1623)) % 0.48/0.65 [164]~P1(x1641)+~P1(x1642)+P3(f5(x1642,x1643,x1641),x1641)+P6(f5(x1642,x1643,x1641),x1642)+~P3(x1643,a20)+E(x1641,f19(x1642,x1643)) % 0.48/0.65 [163]~P1(x1631)+~P1(x1632)+P3(f5(x1632,x1633,x1631),x1631)+~P3(x1633,a20)+E(x1631,f19(x1632,x1633))+E(f2(f5(x1632,x1633,x1631)),x1633) % 0.48/0.65 [112]~P1(x1124)+~P2(x1123)+~P2(x1121)+P3(x1121,x1122)+~E(x1121,x1123)+~E(x1122,f17(x1124,x1123)) % 0.48/0.65 [131]~P1(x1313)+~P2(x1312)+~P3(x1311,x1314)+E(x1311,x1312)+P3(x1311,x1313)+~E(x1314,f17(x1313,x1312)) % 0.48/0.65 [134]~P1(x1343)+~P2(x1344)+~P2(x1341)+~P3(x1341,x1343)+P3(x1341,x1342)+~E(x1342,f17(x1343,x1344)) % 0.48/0.65 [145]~P1(x1454)+~P6(x1451,x1454)+P3(x1451,x1452)+~P3(x1453,a20)+~E(x1452,f19(x1454,x1453))+~E(f2(x1451),x1453) % 0.48/0.65 [154]E(f23(x1542),f23(x1541))+~P6(x1541,a20)+~P6(x1542,a20)+~P3(f23(x1541),x1542)+~P3(f23(x1542),x1541)+E(x1541,a18)+E(x1542,a18) % 0.48/0.65 [165]~P1(x1651)+~P1(x1652)+~P2(x1653)+E(f9(x1652,x1653,x1651),x1653)+P3(f9(x1652,x1653,x1651),x1651)+P3(f9(x1652,x1653,x1651),x1652)+E(x1651,f17(x1652,x1653)) % 0.48/0.65 [166]~P1(x1661)+~P1(x1662)+~P2(x1663)+~E(f9(x1662,x1663,x1661),x1663)+~P3(f9(x1662,x1663,x1661),x1661)+E(x1661,f17(x1662,x1663))+~P2(f9(x1662,x1663,x1661)) % 0.48/0.65 [167]~P1(x1671)+~P1(x1672)+~P2(x1673)+~P3(f9(x1672,x1673,x1671),x1671)+~P3(f9(x1672,x1673,x1671),x1672)+E(x1671,f17(x1672,x1673))+~P2(f9(x1672,x1673,x1671)) % 0.48/0.65 [168]~P1(x1681)+~P1(x1682)+~P3(x1683,a20)+~P3(f5(x1682,x1683,x1681),x1681)+~P6(f5(x1682,x1683,x1681),x1682)+E(x1681,f19(x1682,x1683))+~E(f2(f5(x1682,x1683,x1681)),x1683) % 0.48/0.65 [135]~P1(x1354)+~P2(x1352)+~P2(x1351)+~P3(x1351,x1354)+E(x1351,x1352)+P3(x1351,x1353)+~E(x1353,f16(x1354,x1352)) % 0.48/0.65 [169]~P1(x1691)+~P1(x1692)+~P2(x1693)+E(f8(x1692,x1693,x1691),x1693)+~P3(f8(x1692,x1693,x1691),x1691)+~P3(f8(x1692,x1693,x1691),x1692)+E(x1691,f16(x1692,x1693))+~P2(f8(x1692,x1693,x1691)) % 0.48/0.65 %EqnAxiom % 0.48/0.65 [1]E(x11,x11) % 0.48/0.65 [2]E(x22,x21)+~E(x21,x22) % 0.48/0.65 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.48/0.65 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.48/0.65 [5]~E(x51,x52)+E(f15(x51),f15(x52)) % 0.48/0.65 [6]~E(x61,x62)+E(f16(x61,x63),f16(x62,x63)) % 0.48/0.65 [7]~E(x71,x72)+E(f16(x73,x71),f16(x73,x72)) % 0.48/0.65 [8]~E(x81,x82)+E(f17(x81,x83),f17(x82,x83)) % 0.48/0.65 [9]~E(x91,x92)+E(f17(x93,x91),f17(x93,x92)) % 0.48/0.65 [10]~E(x101,x102)+E(f8(x101,x103,x104),f8(x102,x103,x104)) % 0.48/0.65 [11]~E(x111,x112)+E(f8(x113,x111,x114),f8(x113,x112,x114)) % 0.48/0.65 [12]~E(x121,x122)+E(f8(x123,x124,x121),f8(x123,x124,x122)) % 0.48/0.65 [13]~E(x131,x132)+E(f19(x131,x133),f19(x132,x133)) % 0.48/0.65 [14]~E(x141,x142)+E(f19(x143,x141),f19(x143,x142)) % 0.48/0.65 [15]~E(x151,x152)+E(f12(x151,x153),f12(x152,x153)) % 0.48/0.65 [16]~E(x161,x162)+E(f12(x163,x161),f12(x163,x162)) % 0.48/0.65 [17]~E(x171,x172)+E(f24(x171),f24(x172)) % 0.48/0.65 [18]~E(x181,x182)+E(f9(x181,x183,x184),f9(x182,x183,x184)) % 0.48/0.65 [19]~E(x191,x192)+E(f9(x193,x191,x194),f9(x193,x192,x194)) % 0.48/0.65 [20]~E(x201,x202)+E(f9(x203,x204,x201),f9(x203,x204,x202)) % 0.48/0.65 [21]~E(x211,x212)+E(f23(x211),f23(x212)) % 0.48/0.65 [22]~E(x221,x222)+E(f22(x221),f22(x222)) % 0.48/0.65 [23]~E(x231,x232)+E(f7(x231,x233),f7(x232,x233)) % 0.48/0.65 [24]~E(x241,x242)+E(f7(x243,x241),f7(x243,x242)) % 0.48/0.65 [25]~E(x251,x252)+E(f13(x251,x253),f13(x252,x253)) % 0.48/0.65 [26]~E(x261,x262)+E(f13(x263,x261),f13(x263,x262)) % 0.48/0.65 [27]~E(x271,x272)+E(f4(x271),f4(x272)) % 0.48/0.65 [28]~E(x281,x282)+E(f3(x281),f3(x282)) % 0.48/0.65 [29]~E(x291,x292)+E(f5(x291,x293,x294),f5(x292,x293,x294)) % 0.48/0.65 [30]~E(x301,x302)+E(f5(x303,x301,x304),f5(x303,x302,x304)) % 0.48/0.65 [31]~E(x311,x312)+E(f5(x313,x314,x311),f5(x313,x314,x312)) % 0.48/0.65 [32]~E(x321,x322)+E(f11(x321,x323),f11(x322,x323)) % 0.48/0.65 [33]~E(x331,x332)+E(f11(x333,x331),f11(x333,x332)) % 0.48/0.65 [34]~E(x341,x342)+E(f6(x341),f6(x342)) % 0.48/0.65 [35]~E(x351,x352)+E(f10(x351,x353),f10(x352,x353)) % 0.48/0.65 [36]~E(x361,x362)+E(f10(x363,x361),f10(x363,x362)) % 0.48/0.65 [37]~P1(x371)+P1(x372)+~E(x371,x372) % 0.48/0.65 [38]P3(x382,x383)+~E(x381,x382)+~P3(x381,x383) % 0.48/0.65 [39]P3(x393,x392)+~E(x391,x392)+~P3(x393,x391) % 0.48/0.65 [40]P6(x402,x403)+~E(x401,x402)+~P6(x401,x403) % 0.48/0.65 [41]P6(x413,x412)+~E(x411,x412)+~P6(x413,x411) % 0.48/0.65 [42]~P2(x421)+P2(x422)+~E(x421,x422) % 0.48/0.65 [43]~P4(x431)+P4(x432)+~E(x431,x432) % 0.48/0.65 [44]P8(x442,x443)+~E(x441,x442)+~P8(x441,x443) % 0.48/0.65 [45]P8(x453,x452)+~E(x451,x452)+~P8(x453,x451) % 0.48/0.65 [46]~P5(x461)+P5(x462)+~E(x461,x462) % 0.48/0.65 [47]P7(x472,x473)+~E(x471,x472)+~P7(x471,x473) % 0.48/0.65 [48]P7(x483,x482)+~E(x481,x482)+~P7(x483,x481) % 0.48/0.65 % 0.48/0.65 %------------------------------------------- % 0.48/0.65 cnf(173,plain, % 0.48/0.65 (~P3(x1731,a18)), % 0.48/0.65 inference(equality_inference,[],[78])). % 0.48/0.65 cnf(174,plain, % 0.48/0.65 (P1(f15(x1741))+~P3(x1741,a20)), % 0.48/0.65 inference(equality_inference,[],[86])). % 0.48/0.65 cnf(179,plain, % 0.48/0.65 (~P1(x1791)+P1(f19(x1791,x1792))+~P3(x1792,a20)), % 0.48/0.65 inference(equality_inference,[],[108])). % 0.48/0.65 cnf(183,plain, % 0.48/0.65 (P2(x1831)+~P1(x1832)+~P2(x1833)+~P3(x1831,f16(x1832,x1833))), % 0.48/0.65 inference(equality_inference,[],[118])). % 0.48/0.65 cnf(187,plain, % 0.48/0.65 (P3(x1871,x1872)+~P1(x1872)+~P2(x1873)+~P3(x1871,f16(x1872,x1873))), % 0.48/0.65 inference(equality_inference,[],[127])). % 0.48/0.65 cnf(188,plain, % 0.48/0.65 (~P3(x1881,a20)+~P3(x1881,a20)+P3(x1881,f15(f22(x1881)))), % 0.48/0.65 inference(equality_inference,[],[130])). % 0.48/0.65 cnf(221,plain, % 0.48/0.65 ($false), % 0.48/0.65 inference(scs_inference,[],[64,173,59,60,62,50,51,54,55,56,58,70,68,78,2,71,90,174,38,39,188,3,74,76,179,43,183,187]), % 0.48/0.65 ['proof']). % 0.48/0.65 % SZS output end Proof % 0.48/0.65 % Total time :0.010000s %------------------------------------------------------------------------------