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