%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM634+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 : n027.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:33 EDT 2024 % Result : Theorem 0.57s 0.73s % Output : CNFRefutation 0.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : NUM634+1 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n027.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Jun 23 01:21:09 EDT 2024 % 0.12/0.35 % CPUTime : % 0.56/0.59 start to proof:theBenchmark % 0.56/0.70 %------------------------------------------- % 0.56/0.70 % File :CSE---1.7 % 0.56/0.70 % Problem :theBenchmark % 0.56/0.70 % Transform :cnf % 0.56/0.70 % Format :tptp:raw % 0.56/0.70 % Command :java -jar mcs_scs.jar %d %s % 0.56/0.70 % 0.56/0.70 % Result :Theorem 0.020000s % 0.56/0.70 % Output :CNFRefutation 0.020000s % 0.56/0.70 %------------------------------------------- % 0.56/0.71 %------------------------------------------------------------------------------ % 0.56/0.71 % File : NUM634+1 : TPTP v8.2.0. Released v4.0.0. % 0.56/0.71 % Domain : Number Theory % 0.56/0.71 % Problem : Ramsey's Infinite Theorem 15_03, 00 expansion % 0.56/0.71 % Version : Especial. % 0.56/0.71 % English : % 0.56/0.71 % 0.56/0.71 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 0.56/0.71 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 0.56/0.71 % Source : [Pas08] % 0.56/0.71 % Names : ramsey_15_03.00 [Pas08] % 0.56/0.71 % 0.56/0.71 % Status : ContradictoryAxioms % 0.56/0.71 % Rating : 0.11 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.07 v6.0.0, 0.09 v5.5.0, 0.07 v5.4.0, 0.11 v5.2.0, 0.10 v5.1.0, 0.19 v5.0.0, 0.25 v4.1.0, 0.30 v4.0.1, 0.65 v4.0.0 % 0.56/0.71 % Syntax : Number of formulae : 80 ( 6 unt; 11 def) % 0.56/0.71 % Number of atoms : 316 ( 53 equ) % 0.56/0.71 % Maximal formula atoms : 12 ( 3 avg) % 0.56/0.71 % Number of connectives : 259 ( 23 ~; 4 |; 96 &) % 0.56/0.71 % ( 22 <=>; 114 =>; 0 <=; 0 <~>) % 0.56/0.71 % Maximal formula depth : 15 ( 5 avg) % 0.56/0.71 % Maximal term depth : 4 ( 1 avg) % 0.56/0.71 % Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty) % 0.56/0.71 % Number of functors : 21 ( 21 usr; 7 con; 0-2 aty) % 0.56/0.71 % Number of variables : 148 ( 138 !; 10 ?) % 0.56/0.71 % SPC : FOF_CAX_RFO_SEQ % 0.56/0.71 % 0.56/0.71 % Comments : Problem generated by the SAD system [VLP07] % 0.56/0.71 %------------------------------------------------------------------------------ % 0.56/0.71 fof(mSetSort,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aSet0(W0) % 0.56/0.71 => $true ) ). % 0.56/0.71 % 0.56/0.71 fof(mElmSort,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aElement0(W0) % 0.56/0.71 => $true ) ). % 0.56/0.71 % 0.56/0.71 fof(mEOfElem,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aSet0(W0) % 0.56/0.71 => ! [W1] : % 0.56/0.71 ( aElementOf0(W1,W0) % 0.56/0.71 => aElement0(W1) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mFinRel,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aSet0(W0) % 0.56/0.71 => ( isFinite0(W0) % 0.56/0.71 => $true ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mDefEmp,definition, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( W0 = slcrc0 % 0.56/0.71 <=> ( aSet0(W0) % 0.56/0.71 & ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mEmpFin,axiom, % 0.56/0.71 isFinite0(slcrc0) ). % 0.56/0.71 % 0.56/0.71 fof(mCntRel,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( aSet0(W0) % 0.56/0.71 => ( isCountable0(W0) % 0.56/0.71 => $true ) ) ). % 0.56/0.71 % 0.56/0.71 fof(mCountNFin,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( ( aSet0(W0) % 0.56/0.71 & isCountable0(W0) ) % 0.56/0.71 => ~ isFinite0(W0) ) ). % 0.56/0.71 % 0.56/0.71 fof(mCountNFin_01,axiom, % 0.56/0.71 ! [W0] : % 0.56/0.71 ( ( aSet0(W0) % 0.57/0.71 & isCountable0(W0) ) % 0.57/0.71 => W0 != slcrc0 ) ). % 0.57/0.71 % 0.57/0.71 fof(mDefSub,definition, % 0.57/0.71 ! [W0] : % 0.57/0.71 ( aSet0(W0) % 0.57/0.71 => ! [W1] : % 0.57/0.71 ( aSubsetOf0(W1,W0) % 0.57/0.71 <=> ( aSet0(W1) % 0.57/0.71 & ! [W2] : % 0.57/0.71 ( aElementOf0(W2,W1) % 0.57/0.71 => aElementOf0(W2,W0) ) ) ) ) ). % 0.57/0.71 % 0.57/0.71 fof(mSubFSet,axiom, % 0.57/0.71 ! [W0] : % 0.57/0.71 ( ( aSet0(W0) % 0.57/0.71 & isFinite0(W0) ) % 0.57/0.71 => ! [W1] : % 0.57/0.71 ( aSubsetOf0(W1,W0) % 0.57/0.71 => isFinite0(W1) ) ) ). % 0.57/0.71 % 0.57/0.71 fof(mSubRefl,axiom, % 0.57/0.71 ! [W0] : % 0.57/0.71 ( aSet0(W0) % 0.57/0.71 => aSubsetOf0(W0,W0) ) ). % 0.57/0.71 % 0.57/0.71 fof(mSubASymm,axiom, % 0.57/0.71 ! [W0,W1] : % 0.57/0.71 ( ( aSet0(W0) % 0.57/0.71 & aSet0(W1) ) % 0.57/0.71 => ( ( aSubsetOf0(W0,W1) % 0.57/0.71 & aSubsetOf0(W1,W0) ) % 0.57/0.71 => W0 = W1 ) ) ). % 0.57/0.71 % 0.57/0.71 fof(mSubTrans,axiom, % 0.57/0.71 ! [W0,W1,W2] : % 0.57/0.71 ( ( aSet0(W0) % 0.57/0.71 & aSet0(W1) % 0.57/0.71 & aSet0(W2) ) % 0.57/0.71 => ( ( aSubsetOf0(W0,W1) % 0.57/0.71 & aSubsetOf0(W1,W2) ) % 0.57/0.71 => aSubsetOf0(W0,W2) ) ) ). % 0.57/0.71 % 0.57/0.71 fof(mDefCons,definition, % 0.57/0.71 ! [W0,W1] : % 0.57/0.71 ( ( aSet0(W0) % 0.57/0.71 & aElement0(W1) ) % 0.57/0.71 => ! [W2] : % 0.57/0.71 ( W2 = sdtpldt0(W0,W1) % 0.57/0.71 <=> ( aSet0(W2) % 0.57/0.71 & ! [W3] : % 0.57/0.71 ( aElementOf0(W3,W2) % 0.57/0.71 <=> ( aElement0(W3) % 0.57/0.71 & ( aElementOf0(W3,W0) % 0.57/0.71 | W3 = W1 ) ) ) ) ) ) ). % 0.57/0.71 % 0.57/0.71 fof(mDefDiff,definition, % 0.57/0.71 ! [W0,W1] : % 0.57/0.71 ( ( aSet0(W0) % 0.57/0.71 & aElement0(W1) ) % 0.57/0.71 => ! [W2] : % 0.57/0.71 ( W2 = sdtmndt0(W0,W1) % 0.57/0.71 <=> ( aSet0(W2) % 0.57/0.71 & ! [W3] : % 0.57/0.71 ( aElementOf0(W3,W2) % 0.57/0.71 <=> ( aElement0(W3) % 0.57/0.71 & aElementOf0(W3,W0) % 0.57/0.71 & W3 != W1 ) ) ) ) ) ). % 0.57/0.71 % 0.57/0.71 fof(mConsDiff,axiom, % 0.57/0.71 ! [W0] : % 0.57/0.71 ( aSet0(W0) % 0.57/0.71 => ! [W1] : % 0.57/0.71 ( aElementOf0(W1,W0) % 0.57/0.71 => sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ) ). % 0.57/0.71 % 0.57/0.71 fof(mDiffCons,axiom, % 0.57/0.71 ! [W0,W1] : % 0.57/0.71 ( ( aElement0(W0) % 0.57/0.71 & aSet0(W1) ) % 0.57/0.71 => ( ~ aElementOf0(W0,W1) % 0.57/0.71 => sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ) ). % 0.57/0.71 % 0.57/0.71 fof(mCConsSet,axiom, % 0.57/0.71 ! [W0] : % 0.57/0.71 ( aElement0(W0) % 0.57/0.71 => ! [W1] : % 0.57/0.71 ( ( aSet0(W1) % 0.57/0.71 & isCountable0(W1) ) % 0.57/0.71 => isCountable0(sdtpldt0(W1,W0)) ) ) ). % 0.57/0.71 % 0.57/0.71 fof(mCDiffSet,axiom, % 0.57/0.71 ! [W0] : % 0.57/0.71 ( aElement0(W0) % 0.57/0.71 => ! [W1] : % 0.57/0.71 ( ( aSet0(W1) % 0.57/0.71 & isCountable0(W1) ) % 0.57/0.71 => isCountable0(sdtmndt0(W1,W0)) ) ) ). % 0.57/0.71 % 0.57/0.71 fof(mFConsSet,axiom, % 0.57/0.71 ! [W0] : % 0.57/0.71 ( aElement0(W0) % 0.57/0.71 => ! [W1] : % 0.57/0.71 ( ( aSet0(W1) % 0.57/0.71 & isFinite0(W1) ) % 0.57/0.71 => isFinite0(sdtpldt0(W1,W0)) ) ) ). % 0.57/0.71 % 0.57/0.71 fof(mFDiffSet,axiom, % 0.57/0.71 ! [W0] : % 0.57/0.71 ( aElement0(W0) % 0.57/0.71 => ! [W1] : % 0.57/0.71 ( ( aSet0(W1) % 0.57/0.71 & isFinite0(W1) ) % 0.57/0.71 => isFinite0(sdtmndt0(W1,W0)) ) ) ). % 0.57/0.71 % 0.57/0.71 fof(mNATSet,axiom, % 0.57/0.71 ( aSet0(szNzAzT0) % 0.57/0.71 & isCountable0(szNzAzT0) ) ). % 0.57/0.71 % 0.57/0.71 fof(mZeroNum,axiom, % 0.57/0.71 aElementOf0(sz00,szNzAzT0) ). % 0.57/0.71 % 0.57/0.71 fof(mSuccNum,axiom, % 0.57/0.71 ! [W0] : % 0.57/0.71 ( aElementOf0(W0,szNzAzT0) % 0.57/0.71 => ( aElementOf0(szszuzczcdt0(W0),szNzAzT0) % 0.57/0.71 & szszuzczcdt0(W0) != sz00 ) ) ). % 0.57/0.71 % 0.57/0.71 fof(mSuccEquSucc,axiom, % 0.57/0.71 ! [W0,W1] : % 0.57/0.71 ( ( aElementOf0(W0,szNzAzT0) % 0.57/0.71 & aElementOf0(W1,szNzAzT0) ) % 0.57/0.71 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 0.57/0.72 => W0 = W1 ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mNatExtra,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 => ( W0 = sz00 % 0.57/0.72 | ? [W1] : % 0.57/0.72 ( aElementOf0(W1,szNzAzT0) % 0.57/0.72 & W0 = szszuzczcdt0(W1) ) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mNatNSucc,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 => W0 != szszuzczcdt0(W0) ) ). % 0.57/0.72 % 0.57/0.72 fof(mLessRel,axiom, % 0.57/0.72 ! [W0,W1] : % 0.57/0.72 ( ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 & aElementOf0(W1,szNzAzT0) ) % 0.57/0.72 => ( sdtlseqdt0(W0,W1) % 0.57/0.72 => $true ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mZeroLess,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 => sdtlseqdt0(sz00,W0) ) ). % 0.57/0.72 % 0.57/0.72 fof(mNoScLessZr,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 => ~ sdtlseqdt0(szszuzczcdt0(W0),sz00) ) ). % 0.57/0.72 % 0.57/0.72 fof(mSuccLess,axiom, % 0.57/0.72 ! [W0,W1] : % 0.57/0.72 ( ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 & aElementOf0(W1,szNzAzT0) ) % 0.57/0.72 => ( sdtlseqdt0(W0,W1) % 0.57/0.72 <=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mLessSucc,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 => sdtlseqdt0(W0,szszuzczcdt0(W0)) ) ). % 0.57/0.72 % 0.57/0.72 fof(mLessRefl,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 => sdtlseqdt0(W0,W0) ) ). % 0.57/0.72 % 0.57/0.72 fof(mLessASymm,axiom, % 0.57/0.72 ! [W0,W1] : % 0.57/0.72 ( ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 & aElementOf0(W1,szNzAzT0) ) % 0.57/0.72 => ( ( sdtlseqdt0(W0,W1) % 0.57/0.72 & sdtlseqdt0(W1,W0) ) % 0.57/0.72 => W0 = W1 ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mLessTrans,axiom, % 0.57/0.72 ! [W0,W1,W2] : % 0.57/0.72 ( ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 & aElementOf0(W1,szNzAzT0) % 0.57/0.72 & aElementOf0(W2,szNzAzT0) ) % 0.57/0.72 => ( ( sdtlseqdt0(W0,W1) % 0.57/0.72 & sdtlseqdt0(W1,W2) ) % 0.57/0.72 => sdtlseqdt0(W0,W2) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mLessTotal,axiom, % 0.57/0.72 ! [W0,W1] : % 0.57/0.72 ( ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 & aElementOf0(W1,szNzAzT0) ) % 0.57/0.72 => ( sdtlseqdt0(W0,W1) % 0.57/0.72 | sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mIHSort,axiom, % 0.57/0.72 ! [W0,W1] : % 0.57/0.72 ( ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 & aElementOf0(W1,szNzAzT0) ) % 0.57/0.72 => ( iLess0(W0,W1) % 0.57/0.72 => $true ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mIH,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 0.57/0.72 % 0.57/0.72 fof(mCardS,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aSet0(W0) % 0.57/0.72 => aElement0(sbrdtbr0(W0)) ) ). % 0.57/0.72 % 0.57/0.72 fof(mCardNum,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aSet0(W0) % 0.57/0.72 => ( aElementOf0(sbrdtbr0(W0),szNzAzT0) % 0.57/0.72 <=> isFinite0(W0) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mCardEmpty,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aSet0(W0) % 0.57/0.72 => ( sbrdtbr0(W0) = sz00 % 0.57/0.72 <=> W0 = slcrc0 ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mCardCons,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( ( aSet0(W0) % 0.57/0.72 & isFinite0(W0) ) % 0.57/0.72 => ! [W1] : % 0.57/0.72 ( aElement0(W1) % 0.57/0.72 => ( ~ aElementOf0(W1,W0) % 0.57/0.72 => sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mCardDiff,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aSet0(W0) % 0.57/0.72 => ! [W1] : % 0.57/0.72 ( ( isFinite0(W0) % 0.57/0.72 & aElementOf0(W1,W0) ) % 0.57/0.72 => szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mCardSub,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aSet0(W0) % 0.57/0.72 => ! [W1] : % 0.57/0.72 ( ( isFinite0(W0) % 0.57/0.72 & aSubsetOf0(W1,W0) ) % 0.57/0.72 => sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mCardSubEx,axiom, % 0.57/0.72 ! [W0,W1] : % 0.57/0.72 ( ( aSet0(W0) % 0.57/0.72 & aElementOf0(W1,szNzAzT0) ) % 0.57/0.72 => ( ( isFinite0(W0) % 0.57/0.72 & sdtlseqdt0(W1,sbrdtbr0(W0)) ) % 0.57/0.72 => ? [W2] : % 0.57/0.72 ( aSubsetOf0(W2,W0) % 0.57/0.72 & sbrdtbr0(W2) = W1 ) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mDefMin,definition, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( ( aSubsetOf0(W0,szNzAzT0) % 0.57/0.72 & W0 != slcrc0 ) % 0.57/0.72 => ! [W1] : % 0.57/0.72 ( W1 = szmzizndt0(W0) % 0.57/0.72 <=> ( aElementOf0(W1,W0) % 0.57/0.72 & ! [W2] : % 0.57/0.72 ( aElementOf0(W2,W0) % 0.57/0.72 => sdtlseqdt0(W1,W2) ) ) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mDefMax,definition, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( ( aSubsetOf0(W0,szNzAzT0) % 0.57/0.72 & isFinite0(W0) % 0.57/0.72 & W0 != slcrc0 ) % 0.57/0.72 => ! [W1] : % 0.57/0.72 ( W1 = szmzazxdt0(W0) % 0.57/0.72 <=> ( aElementOf0(W1,W0) % 0.57/0.72 & ! [W2] : % 0.57/0.72 ( aElementOf0(W2,W0) % 0.57/0.72 => sdtlseqdt0(W2,W1) ) ) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mMinMin,axiom, % 0.57/0.72 ! [W0,W1] : % 0.57/0.72 ( ( aSubsetOf0(W0,szNzAzT0) % 0.57/0.72 & aSubsetOf0(W1,szNzAzT0) % 0.57/0.72 & W0 != slcrc0 % 0.57/0.72 & W1 != slcrc0 ) % 0.57/0.72 => ( ( aElementOf0(szmzizndt0(W0),W1) % 0.57/0.72 & aElementOf0(szmzizndt0(W1),W0) ) % 0.57/0.72 => szmzizndt0(W0) = szmzizndt0(W1) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mDefSeg,definition, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 => ! [W1] : % 0.57/0.72 ( W1 = slbdtrb0(W0) % 0.57/0.72 <=> ( aSet0(W1) % 0.57/0.72 & ! [W2] : % 0.57/0.72 ( aElementOf0(W2,W1) % 0.57/0.72 <=> ( aElementOf0(W2,szNzAzT0) % 0.57/0.72 & sdtlseqdt0(szszuzczcdt0(W2),W0) ) ) ) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mSegFin,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 => isFinite0(slbdtrb0(W0)) ) ). % 0.57/0.72 % 0.57/0.72 fof(mSegZero,axiom, % 0.57/0.72 slbdtrb0(sz00) = slcrc0 ). % 0.57/0.72 % 0.57/0.72 fof(mSegSucc,axiom, % 0.57/0.72 ! [W0,W1] : % 0.57/0.72 ( ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 & aElementOf0(W1,szNzAzT0) ) % 0.57/0.72 => ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1))) % 0.57/0.72 <=> ( aElementOf0(W0,slbdtrb0(W1)) % 0.57/0.72 | W0 = W1 ) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mSegLess,axiom, % 0.57/0.72 ! [W0,W1] : % 0.57/0.72 ( ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 & aElementOf0(W1,szNzAzT0) ) % 0.57/0.72 => ( sdtlseqdt0(W0,W1) % 0.57/0.72 <=> aSubsetOf0(slbdtrb0(W0),slbdtrb0(W1)) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mFinSubSeg,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( ( aSubsetOf0(W0,szNzAzT0) % 0.57/0.72 & isFinite0(W0) ) % 0.57/0.72 => ? [W1] : % 0.57/0.72 ( aElementOf0(W1,szNzAzT0) % 0.57/0.72 & aSubsetOf0(W0,slbdtrb0(W1)) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mCardSeg,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 => sbrdtbr0(slbdtrb0(W0)) = W0 ) ). % 0.57/0.72 % 0.57/0.72 fof(mDefSel,definition, % 0.57/0.72 ! [W0,W1] : % 0.57/0.72 ( ( aSet0(W0) % 0.57/0.72 & aElementOf0(W1,szNzAzT0) ) % 0.57/0.72 => ! [W2] : % 0.57/0.72 ( W2 = slbdtsldtrb0(W0,W1) % 0.57/0.72 <=> ( aSet0(W2) % 0.57/0.72 & ! [W3] : % 0.57/0.72 ( aElementOf0(W3,W2) % 0.57/0.72 <=> ( aSubsetOf0(W3,W0) % 0.57/0.72 & sbrdtbr0(W3) = W1 ) ) ) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mSelFSet,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( ( aSet0(W0) % 0.57/0.72 & isFinite0(W0) ) % 0.57/0.72 => ! [W1] : % 0.57/0.72 ( aElementOf0(W1,szNzAzT0) % 0.57/0.72 => isFinite0(slbdtsldtrb0(W0,W1)) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mSelNSet,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( ( aSet0(W0) % 0.57/0.72 & ~ isFinite0(W0) ) % 0.57/0.72 => ! [W1] : % 0.57/0.72 ( aElementOf0(W1,szNzAzT0) % 0.57/0.72 => slbdtsldtrb0(W0,W1) != slcrc0 ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mSelCSet,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( ( aSet0(W0) % 0.57/0.72 & isCountable0(W0) ) % 0.57/0.72 => ! [W1] : % 0.57/0.72 ( ( aElementOf0(W1,szNzAzT0) % 0.57/0.72 & W1 != sz00 ) % 0.57/0.72 => isCountable0(slbdtsldtrb0(W0,W1)) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mSelSub,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aElementOf0(W0,szNzAzT0) % 0.57/0.72 => ! [W1,W2] : % 0.57/0.72 ( ( aSet0(W1) % 0.57/0.72 & aSet0(W2) % 0.57/0.72 & W0 != sz00 ) % 0.57/0.72 => ( ( aSubsetOf0(slbdtsldtrb0(W1,W0),slbdtsldtrb0(W2,W0)) % 0.57/0.72 & slbdtsldtrb0(W1,W0) != slcrc0 ) % 0.57/0.72 => aSubsetOf0(W1,W2) ) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mSelExtra,axiom, % 0.57/0.72 ! [W0,W1] : % 0.57/0.72 ( ( aSet0(W0) % 0.57/0.72 & aElementOf0(W1,szNzAzT0) ) % 0.57/0.72 => ! [W2] : % 0.57/0.72 ( ( aSubsetOf0(W2,slbdtsldtrb0(W0,W1)) % 0.57/0.72 & isFinite0(W2) ) % 0.57/0.72 => ? [W3] : % 0.57/0.72 ( aSubsetOf0(W3,W0) % 0.57/0.72 & isFinite0(W3) % 0.57/0.72 & aSubsetOf0(W2,slbdtsldtrb0(W3,W1)) ) ) ) ). % 0.57/0.72 % 0.57/0.72 fof(mFunSort,axiom, % 0.57/0.72 ! [W0] : % 0.57/0.72 ( aFunction0(W0) % 0.57/0.72 => $true ) ). % 0.57/0.72 % 0.57/0.72 fof(mDomSet,axiom, % 0.57/0.73 ! [W0] : % 0.57/0.73 ( aFunction0(W0) % 0.57/0.73 => aSet0(szDzozmdt0(W0)) ) ). % 0.57/0.73 % 0.57/0.73 fof(mImgElm,axiom, % 0.57/0.73 ! [W0] : % 0.57/0.73 ( aFunction0(W0) % 0.57/0.73 => ! [W1] : % 0.57/0.73 ( aElementOf0(W1,szDzozmdt0(W0)) % 0.57/0.73 => aElement0(sdtlpdtrp0(W0,W1)) ) ) ). % 0.57/0.73 % 0.57/0.73 fof(mDefPtt,definition, % 0.57/0.73 ! [W0,W1] : % 0.57/0.73 ( ( aFunction0(W0) % 0.57/0.73 & aElement0(W1) ) % 0.57/0.73 => ! [W2] : % 0.57/0.73 ( W2 = sdtlbdtrb0(W0,W1) % 0.57/0.73 <=> ( aSet0(W2) % 0.57/0.73 & ! [W3] : % 0.57/0.73 ( aElementOf0(W3,W2) % 0.57/0.73 <=> ( aElementOf0(W3,szDzozmdt0(W0)) % 0.57/0.73 & sdtlpdtrp0(W0,W3) = W1 ) ) ) ) ) ). % 0.57/0.73 % 0.57/0.73 fof(mPttSet,axiom, % 0.57/0.73 ! [W0,W1] : % 0.57/0.73 ( ( aFunction0(W0) % 0.57/0.73 & aElement0(W1) ) % 0.57/0.73 => aSubsetOf0(sdtlbdtrb0(W0,W1),szDzozmdt0(W0)) ) ). % 0.57/0.73 % 0.57/0.73 fof(mDefSImg,definition, % 0.57/0.73 ! [W0] : % 0.57/0.73 ( aFunction0(W0) % 0.57/0.73 => ! [W1] : % 0.57/0.73 ( aSubsetOf0(W1,szDzozmdt0(W0)) % 0.57/0.73 => ! [W2] : % 0.57/0.73 ( W2 = sdtlcdtrc0(W0,W1) % 0.57/0.73 <=> ( aSet0(W2) % 0.57/0.73 & ! [W3] : % 0.57/0.73 ( aElementOf0(W3,W2) % 0.57/0.73 <=> ? [W4] : % 0.57/0.73 ( aElementOf0(W4,W1) % 0.57/0.73 & sdtlpdtrp0(W0,W4) = W3 ) ) ) ) ) ) ). % 0.57/0.73 % 0.57/0.73 fof(mImgRng,axiom, % 0.57/0.73 ! [W0] : % 0.57/0.73 ( aFunction0(W0) % 0.57/0.73 => ! [W1] : % 0.57/0.73 ( aElementOf0(W1,szDzozmdt0(W0)) % 0.57/0.73 => aElementOf0(sdtlpdtrp0(W0,W1),sdtlcdtrc0(W0,szDzozmdt0(W0))) ) ) ). % 0.57/0.73 % 0.57/0.73 fof(mDefRst,definition, % 0.57/0.73 ! [W0] : % 0.57/0.73 ( aFunction0(W0) % 0.57/0.73 => ! [W1] : % 0.57/0.73 ( aSubsetOf0(W1,szDzozmdt0(W0)) % 0.57/0.73 => ! [W2] : % 0.57/0.73 ( W2 = sdtexdt0(W0,W1) % 0.57/0.73 <=> ( aFunction0(W2) % 0.57/0.73 & szDzozmdt0(W2) = W1 % 0.57/0.73 & ! [W3] : % 0.57/0.73 ( aElementOf0(W3,W1) % 0.57/0.73 => sdtlpdtrp0(W2,W3) = sdtlpdtrp0(W0,W3) ) ) ) ) ) ). % 0.57/0.73 % 0.57/0.73 fof(mImgCount,axiom, % 0.57/0.73 ! [W0] : % 0.57/0.73 ( aFunction0(W0) % 0.57/0.73 => ! [W1] : % 0.57/0.73 ( ( aSubsetOf0(W1,szDzozmdt0(W0)) % 0.57/0.73 & isCountable0(W1) ) % 0.57/0.73 => ( ! [W2,W3] : % 0.57/0.73 ( ( aElementOf0(W2,szDzozmdt0(W0)) % 0.57/0.73 & aElementOf0(W3,szDzozmdt0(W0)) % 0.57/0.73 & W2 != W3 ) % 0.57/0.73 => sdtlpdtrp0(W0,W2) != sdtlpdtrp0(W0,W3) ) % 0.57/0.73 => isCountable0(sdtlcdtrc0(W0,W1)) ) ) ) ). % 0.57/0.73 % 0.57/0.73 fof(mDirichlet,axiom, % 0.57/0.73 ! [W0] : % 0.57/0.73 ( aFunction0(W0) % 0.57/0.73 => ( ( isCountable0(szDzozmdt0(W0)) % 0.57/0.73 & isFinite0(sdtlcdtrc0(W0,szDzozmdt0(W0))) ) % 0.57/0.73 => ( aElement0(szDzizrdt0(W0)) % 0.57/0.73 & isCountable0(sdtlbdtrb0(W0,szDzizrdt0(W0))) ) ) ) ). % 0.57/0.73 % 0.57/0.73 fof(m__3291,hypothesis, % 0.57/0.73 ( aSet0(xT) % 0.57/0.73 & isFinite0(xT) ) ). % 0.57/0.73 % 0.57/0.73 fof(m__3418,hypothesis, % 0.57/0.73 aElementOf0(xK,szNzAzT0) ). % 0.57/0.73 % 0.57/0.73 fof(m__3435,hypothesis, % 0.57/0.73 ( aSubsetOf0(xS,szNzAzT0) % 0.57/0.73 & isCountable0(xS) ) ). % 0.57/0.73 % 0.57/0.73 fof(m__3453,hypothesis, % 0.57/0.73 ( aFunction0(xc) % 0.57/0.73 & szDzozmdt0(xc) = slbdtsldtrb0(xS,xK) % 0.57/0.73 & aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ). % 0.57/0.73 % 0.57/0.73 fof(m__3398,hypothesis, % 0.57/0.73 ! [W0] : % 0.57/0.73 ( aElementOf0(W0,szNzAzT0) % 0.57/0.73 => ! [W1] : % 0.57/0.73 ( ( aSubsetOf0(W1,szNzAzT0) % 0.57/0.73 & isCountable0(W1) ) % 0.57/0.73 => ! [W2] : % 0.57/0.73 ( ( aFunction0(W2) % 0.57/0.73 & szDzozmdt0(W2) = slbdtsldtrb0(W1,W0) % 0.57/0.73 & aSubsetOf0(sdtlcdtrc0(W2,szDzozmdt0(W2)),xT) ) % 0.57/0.73 => ( iLess0(W0,xK) % 0.57/0.73 => ? [W3] : % 0.57/0.73 ( aElementOf0(W3,xT) % 0.57/0.73 & ? [W4] : % 0.57/0.73 ( aSubsetOf0(W4,W1) % 0.57/0.73 & isCountable0(W4) % 0.57/0.73 & ! [W5] : % 0.57/0.73 ( aElementOf0(W5,slbdtsldtrb0(W4,W0)) % 0.57/0.73 => sdtlpdtrp0(W2,W5) = W3 ) ) ) ) ) ) ) ). % 0.57/0.73 % 0.57/0.73 fof(m__3462,hypothesis, % 0.57/0.73 xK != sz00 ). % 0.57/0.73 % 0.57/0.73 fof(m__3520,hypothesis, % 0.57/0.73 ~ ( xK != sz00 ) ). % 0.57/0.73 % 0.57/0.73 fof(m__,conjecture, % 0.57/0.73 ? [W0] : % 0.57/0.73 ( aElementOf0(W0,xT) % 0.57/0.73 & ? [W1] : % 0.57/0.73 ( aSubsetOf0(W1,xS) % 0.57/0.73 & isCountable0(W1) % 0.57/0.73 & ! [W2] : % 0.57/0.73 ( aElementOf0(W2,slbdtsldtrb0(W1,xK)) % 0.57/0.73 => sdtlpdtrp0(xc,W2) = W0 ) ) ) ). % 0.57/0.73 % 0.57/0.73 %------------------------------------------------------------------------------ % 0.57/0.73 %------------------------------------------- % 0.57/0.73 % Proof found % 0.57/0.73 % SZS status Theorem for theBenchmark % 0.57/0.73 % SZS output start Proof % 0.57/0.73 %ClaNum:243(EqnAxiom:90) % 0.57/0.73 %VarNum:1138(SingletonVarNum:330) % 0.57/0.73 %MaxLitNum:9 % 0.57/0.73 %MaxfuncDepth:3 % 0.57/0.73 %SharedTerms:26 % 0.57/0.73 %goalClause: 197 198 % 0.57/0.73 [91]E(a1,a2) % 0.57/0.73 [93]P1(a35) % 0.57/0.73 [94]P1(a41) % 0.57/0.73 [95]P5(a33) % 0.57/0.73 [96]P5(a41) % 0.57/0.73 [97]P6(a35) % 0.57/0.73 [98]P6(a42) % 0.57/0.73 [99]P2(a43) % 0.57/0.73 [100]P3(a2,a35) % 0.57/0.73 [101]P3(a1,a35) % 0.57/0.73 [102]P7(a42,a35) % 0.57/0.73 [105]~E(a1,a2) % 0.57/0.73 [92]E(f3(a2),a33) % 0.57/0.73 [103]E(f34(a42,a1),f36(a43)) % 0.57/0.73 [104]P7(f4(a43,f36(a43)),a41) % 0.57/0.73 [106]P1(x1061)+~E(x1061,a33) % 0.57/0.73 [113]~P1(x1131)+P7(x1131,x1131) % 0.57/0.73 [120]~P3(x1201,a35)+P9(a2,x1201) % 0.57/0.73 [126]P9(x1261,x1261)+~P3(x1261,a35) % 0.57/0.73 [110]~P2(x1101)+P1(f36(x1101)) % 0.57/0.73 [111]~P1(x1111)+P4(f5(x1111)) % 0.57/0.73 [115]~P3(x1151,a35)+~E(f38(x1151),a2) % 0.57/0.73 [116]~P3(x1161,a35)+~E(f38(x1161),x1161) % 0.57/0.73 [118]~P3(x1181,a35)+P5(f3(x1181)) % 0.57/0.73 [127]~P3(x1271,a35)+P3(f38(x1271),a35) % 0.57/0.73 [128]~P3(x1281,a35)+P9(x1281,f38(x1281)) % 0.57/0.73 [129]~P3(x1291,a35)+P8(x1291,f38(x1291)) % 0.57/0.73 [138]~P3(x1381,a35)+~P9(f38(x1381),a2) % 0.57/0.73 [119]~P3(x1191,a35)+E(f5(f3(x1191)),x1191) % 0.57/0.73 [114]~P3(x1142,x1141)+~E(x1141,a33) % 0.57/0.73 [109]~P1(x1091)+~P6(x1091)+~E(x1091,a33) % 0.57/0.73 [112]~P5(x1121)+~P6(x1121)+~P1(x1121) % 0.57/0.73 [107]~P1(x1071)+~E(x1071,a33)+E(f5(x1071),a2) % 0.57/0.73 [108]~P1(x1081)+E(x1081,a33)+~E(f5(x1081),a2) % 0.57/0.73 [117]~P1(x1171)+P3(f6(x1171),x1171)+E(x1171,a33) % 0.57/0.73 [123]~P1(x1231)+~P5(x1231)+P3(f5(x1231),a35) % 0.57/0.73 [130]~P3(x1301,a35)+E(x1301,a2)+P3(f17(x1301),a35) % 0.57/0.73 [131]~P1(x1311)+P5(x1311)+~P3(f5(x1311),a35) % 0.57/0.73 [137]~P5(x1371)+~P7(x1371,a35)+P3(f7(x1371),a35) % 0.57/0.73 [121]~P3(x1211,a35)+E(x1211,a2)+E(f38(f17(x1211)),x1211) % 0.57/0.73 [147]~P5(x1471)+~P7(x1471,a35)+P7(x1471,f3(f7(x1471))) % 0.57/0.73 [124]~P7(x1241,x1242)+P1(x1241)+~P1(x1242) % 0.57/0.73 [125]~P3(x1251,x1252)+P4(x1251)+~P1(x1252) % 0.57/0.73 [122]P1(x1221)+~P3(x1222,a35)+~E(x1221,f3(x1222)) % 0.57/0.73 [148]~P4(x1482)+~P2(x1481)+P7(f28(x1481,x1482),f36(x1481)) % 0.57/0.73 [164]~P2(x1641)+~P3(x1642,f36(x1641))+P4(f32(x1641,x1642)) % 0.57/0.73 [166]~P1(x1661)+~P3(x1662,x1661)+E(f30(f31(x1661,x1662),x1662),x1661) % 0.57/0.73 [204]~P2(x2041)+~P3(x2042,f36(x2041))+P3(f32(x2041,x2042),f4(x2041,f36(x2041))) % 0.57/0.73 [192]~P2(x1921)+~P6(f36(x1921))+P4(f37(x1921))+~P5(f4(x1921,f36(x1921))) % 0.57/0.73 [211]~P2(x2111)+~P6(f36(x2111))+~P5(f4(x2111,f36(x2111)))+P6(f28(x2111,f37(x2111))) % 0.57/0.73 [132]~P5(x1322)+~P7(x1321,x1322)+P5(x1321)+~P1(x1322) % 0.57/0.73 [136]P3(x1362,x1361)+~E(x1362,f39(x1361))+~P7(x1361,a35)+E(x1361,a33) % 0.57/0.73 [140]~P1(x1401)+~P4(x1402)+~P5(x1401)+P5(f30(x1401,x1402)) % 0.57/0.73 [141]~P1(x1411)+~P4(x1412)+~P5(x1411)+P5(f31(x1411,x1412)) % 0.57/0.73 [142]~P1(x1421)+~P4(x1422)+~P6(x1421)+P6(f30(x1421,x1422)) % 0.57/0.73 [143]~P1(x1431)+~P4(x1432)+~P6(x1431)+P6(f31(x1431,x1432)) % 0.57/0.73 [144]~P1(x1441)+P5(x1441)+~P3(x1442,a35)+~E(f34(x1441,x1442),a33) % 0.57/0.73 [146]E(x1461,x1462)+~E(f38(x1461),f38(x1462))+~P3(x1462,a35)+~P3(x1461,a35) % 0.57/0.73 [151]~P1(x1512)+~P5(x1512)+~P7(x1511,x1512)+P9(f5(x1511),f5(x1512)) % 0.57/0.73 [154]~P1(x1541)+~P5(x1541)+~P3(x1542,a35)+P5(f34(x1541,x1542)) % 0.57/0.73 [163]~P1(x1631)+~P1(x1632)+P7(x1631,x1632)+P3(f18(x1632,x1631),x1631) % 0.57/0.73 [170]P9(x1701,x1702)+P9(f38(x1702),x1701)+~P3(x1702,a35)+~P3(x1701,a35) % 0.57/0.73 [182]~P9(x1821,x1822)+~P3(x1822,a35)+~P3(x1821,a35)+P7(f3(x1821),f3(x1822)) % 0.57/0.73 [183]~P9(x1831,x1832)+~P3(x1832,a35)+~P3(x1831,a35)+P9(f38(x1831),f38(x1832)) % 0.57/0.73 [185]~P1(x1851)+~P1(x1852)+P7(x1851,x1852)+~P3(f18(x1852,x1851),x1852) % 0.57/0.73 [187]P9(x1871,x1872)+~P3(x1872,a35)+~P3(x1871,a35)+~P7(f3(x1871),f3(x1872)) % 0.57/0.73 [188]P9(x1881,x1882)+~P3(x1882,a35)+~P3(x1881,a35)+~P9(f38(x1881),f38(x1882)) % 0.57/0.73 [198]~P6(x1982)+~P3(x1981,a41)+~P7(x1982,a42)+P3(f19(x1981,x1982),f34(x1982,a1)) % 0.57/0.73 [165]P3(x1652,x1651)+~P1(x1651)+~P4(x1652)+E(f31(f30(x1651,x1652),x1652),x1651) % 0.57/0.73 [173]~E(x1731,x1732)+~P3(x1732,a35)+~P3(x1731,a35)+P3(x1731,f3(f38(x1732))) % 0.57/0.73 [194]~P3(x1942,a35)+~P3(x1941,a35)+~P3(x1941,f3(x1942))+P3(x1941,f3(f38(x1942))) % 0.57/0.73 [197]~P6(x1972)+~P3(x1971,a41)+~P7(x1972,a42)+~E(f32(a43,f19(x1971,x1972)),x1971) % 0.57/0.73 [193]~P1(x1931)+~P5(x1931)+~P3(x1932,x1931)+E(f38(f5(f31(x1931,x1932))),f5(x1931)) % 0.57/0.73 [158]~P1(x1582)+~P7(x1583,x1582)+P3(x1581,x1582)+~P3(x1581,x1583) % 0.57/0.73 [133]~P1(x1332)+~P4(x1333)+P1(x1331)+~E(x1331,f30(x1332,x1333)) % 0.57/0.73 [134]~P1(x1342)+~P4(x1343)+P1(x1341)+~E(x1341,f31(x1342,x1343)) % 0.57/0.73 [135]~P4(x1353)+~P2(x1352)+P1(x1351)+~E(x1351,f28(x1352,x1353)) % 0.57/0.73 [145]~P1(x1452)+P1(x1451)+~P3(x1453,a35)+~E(x1451,f34(x1452,x1453)) % 0.57/0.73 [152]~P3(x1521,x1522)+~P3(x1523,a35)+P3(x1521,a35)+~E(x1522,f3(x1523)) % 0.57/0.73 [160]~P2(x1602)+P1(x1601)+~P7(x1603,f36(x1602))+~E(x1601,f4(x1602,x1603)) % 0.57/0.73 [161]~P2(x1612)+P2(x1611)+~P7(x1613,f36(x1612))+~E(x1611,f29(x1612,x1613)) % 0.57/0.73 [162]~P2(x1623)+~P7(x1622,f36(x1623))+E(f36(x1621),x1622)+~E(x1621,f29(x1623,x1622)) % 0.57/0.73 [167]~P3(x1671,x1673)+~P3(x1672,a35)+P9(f38(x1671),x1672)+~E(x1673,f3(x1672)) % 0.57/0.73 [149]~P1(x1492)+~P1(x1491)+~P7(x1492,x1491)+~P7(x1491,x1492)+E(x1491,x1492) % 0.57/0.73 [180]~P9(x1802,x1801)+~P9(x1801,x1802)+E(x1801,x1802)+~P3(x1802,a35)+~P3(x1801,a35) % 0.57/0.73 [139]~P5(x1391)+P3(x1392,x1391)+~E(x1392,f40(x1391))+~P7(x1391,a35)+E(x1391,a33) % 0.57/0.73 [157]~P1(x1572)+~P6(x1572)+~P3(x1571,a35)+E(x1571,a2)+P6(f34(x1572,x1571)) % 0.57/0.73 [184]~P3(x1842,x1841)+P3(f24(x1841,x1842),x1841)+~P7(x1841,a35)+E(x1841,a33)+E(x1842,f39(x1841)) % 0.57/0.73 [195]~P1(x1951)+~P5(x1951)+~P3(x1952,a35)+~P9(x1952,f5(x1951))+P7(f25(x1951,x1952),x1951) % 0.57/0.73 [199]~P1(x1991)+P3(f27(x1992,x1991),x1991)+~P3(x1992,a35)+E(x1991,f3(x1992))+P3(f27(x1992,x1991),a35) % 0.57/0.73 [200]~P3(x2002,x2001)+~P7(x2001,a35)+~P9(x2002,f24(x2001,x2002))+E(x2001,a33)+E(x2002,f39(x2001)) % 0.57/0.73 [207]~P6(x2072)+~P2(x2071)+~E(f8(x2071,x2072),f9(x2071,x2072))+~P7(x2072,f36(x2071))+P6(f4(x2071,x2072)) % 0.57/0.73 [208]~P6(x2082)+~P2(x2081)+P3(f9(x2081,x2082),f36(x2081))+~P7(x2082,f36(x2081))+P6(f4(x2081,x2082)) % 0.57/0.73 [209]~P6(x2092)+~P2(x2091)+P3(f8(x2091,x2092),f36(x2091))+~P7(x2092,f36(x2091))+P6(f4(x2091,x2092)) % 0.57/0.73 [172]P3(x1722,x1721)+~P1(x1721)+~P4(x1722)+~P5(x1721)+E(f5(f30(x1721,x1722)),f38(f5(x1721))) % 0.57/0.73 [191]~P1(x1911)+~P5(x1911)+~P3(x1912,a35)+~P9(x1912,f5(x1911))+E(f5(f25(x1911,x1912)),x1912) % 0.57/0.73 [202]E(x2021,x2022)+P3(x2021,f3(x2022))+~P3(x2022,a35)+~P3(x2021,a35)+~P3(x2021,f3(f38(x2022))) % 0.57/0.73 [212]~P1(x2121)+P3(f27(x2122,x2121),x2121)+~P3(x2122,a35)+E(x2121,f3(x2122))+P9(f38(f27(x2122,x2121)),x2122) % 0.57/0.73 [213]~P6(x2132)+~P2(x2131)+~P7(x2132,f36(x2131))+P6(f4(x2131,x2132))+E(f32(x2131,f8(x2131,x2132)),f32(x2131,f9(x2131,x2132))) % 0.57/0.73 [159]~P3(x1593,x1591)+P9(x1592,x1593)+~E(x1592,f39(x1591))+~P7(x1591,a35)+E(x1591,a33) % 0.57/0.73 [186]P3(x1861,x1862)+~P3(x1863,a35)+~P3(x1861,a35)+~P9(f38(x1861),x1863)+~E(x1862,f3(x1863)) % 0.57/0.73 [216]~P1(x2161)+~P5(x2163)+~P3(x2162,a35)+~P7(x2163,f34(x2161,x2162))+P5(f11(x2161,x2162,x2163)) % 0.57/0.73 [217]~P1(x2171)+~P5(x2173)+~P3(x2172,a35)+~P7(x2173,f34(x2171,x2172))+P7(f11(x2171,x2172,x2173),x2171) % 0.57/0.73 [232]~P1(x2322)+~P5(x2321)+~P3(x2323,a35)+~P7(x2321,f34(x2322,x2323))+P7(x2321,f34(f11(x2322,x2323,x2321),x2323)) % 0.57/0.73 [153]~P1(x1534)+~P4(x1532)+~P3(x1531,x1533)+~E(x1531,x1532)+~E(x1533,f31(x1534,x1532)) % 0.57/0.73 [155]~P1(x1553)+~P4(x1554)+~P3(x1551,x1552)+P4(x1551)+~E(x1552,f30(x1553,x1554)) % 0.57/0.73 [156]~P1(x1563)+~P4(x1564)+~P3(x1561,x1562)+P4(x1561)+~E(x1562,f31(x1563,x1564)) % 0.57/0.73 [169]~P1(x1692)+~P4(x1694)+~P3(x1691,x1693)+P3(x1691,x1692)+~E(x1693,f31(x1692,x1694)) % 0.57/0.73 [171]~P4(x1713)+~P2(x1711)+~P3(x1712,x1714)+E(f32(x1711,x1712),x1713)+~E(x1714,f28(x1711,x1713)) % 0.57/0.73 [175]~P1(x1754)+~P3(x1751,x1753)+~P3(x1752,a35)+E(f5(x1751),x1752)+~E(x1753,f34(x1754,x1752)) % 0.57/0.73 [177]~P4(x1774)+~P2(x1772)+~P3(x1771,x1773)+P3(x1771,f36(x1772))+~E(x1773,f28(x1772,x1774)) % 0.57/0.73 [181]~P1(x1812)+~P3(x1811,x1813)+P7(x1811,x1812)+~P3(x1814,a35)+~E(x1813,f34(x1812,x1814)) % 0.57/0.73 [201]~P2(x2013)+~P3(x2012,x2014)+~P7(x2014,f36(x2013))+E(f32(x2011,x2012),f32(x2013,x2012))+~E(x2011,f29(x2013,x2014)) % 0.57/0.73 [238]~P2(x2381)+~P3(x2384,x2383)+~E(x2383,f4(x2381,x2382))+~P7(x2382,f36(x2381))+P3(f15(x2381,x2382,x2383,x2384),x2382) % 0.57/0.73 [239]~P2(x2391)+~P3(x2394,x2393)+~E(x2393,f4(x2391,x2392))+~P7(x2392,f36(x2391))+E(f32(x2391,f15(x2391,x2392,x2393,x2394)),x2394) % 0.57/0.73 [190]~P5(x1901)+~P3(x1902,x1901)+P3(f26(x1901,x1902),x1901)+~P7(x1901,a35)+E(x1901,a33)+E(x1902,f40(x1901)) % 0.57/0.73 [205]~P5(x2051)+~P3(x2052,x2051)+~P7(x2051,a35)+~P9(f26(x2051,x2052),x2052)+E(x2051,a33)+E(x2052,f40(x2051)) % 0.57/0.73 [221]~P1(x2211)+~P3(x2212,a35)+~P3(f27(x2212,x2211),x2211)+E(x2211,f3(x2212))+~P3(f27(x2212,x2211),a35)+~P9(f38(f27(x2212,x2211)),x2212) % 0.57/0.73 [176]~P1(x1762)+~P1(x1761)+~P7(x1763,x1762)+~P7(x1761,x1763)+P7(x1761,x1762)+~P1(x1763) % 0.57/0.73 [206]~P9(x2061,x2063)+P9(x2061,x2062)+~P9(x2063,x2062)+~P3(x2062,a35)+~P3(x2063,a35)+~P3(x2061,a35) % 0.57/0.73 [168]~P5(x1681)+~P3(x1682,x1681)+P9(x1682,x1683)+~E(x1683,f40(x1681))+~P7(x1681,a35)+E(x1681,a33) % 0.57/0.73 [215]~P2(x2151)+~P2(x2152)+P3(f10(x2152,x2153,x2151),x2153)+~E(f36(x2151),x2153)+~P7(x2153,f36(x2152))+E(x2151,f29(x2152,x2153)) % 0.57/0.73 [218]~P1(x2181)+~P1(x2182)+~P4(x2183)+P3(f22(x2182,x2183,x2181),x2181)+~E(f22(x2182,x2183,x2181),x2183)+E(x2181,f31(x2182,x2183)) % 0.57/0.73 [219]~P1(x2191)+~P1(x2192)+~P4(x2193)+P3(f23(x2192,x2193,x2191),x2191)+E(x2191,f30(x2192,x2193))+P4(f23(x2192,x2193,x2191)) % 0.57/0.73 [220]~P1(x2201)+~P1(x2202)+~P4(x2203)+P3(f22(x2202,x2203,x2201),x2201)+E(x2201,f31(x2202,x2203))+P4(f22(x2202,x2203,x2201)) % 0.57/0.73 [222]~P1(x2221)+~P1(x2222)+~P4(x2223)+P3(f22(x2222,x2223,x2221),x2221)+P3(f22(x2222,x2223,x2221),x2222)+E(x2221,f31(x2222,x2223)) % 0.57/0.73 [225]~P1(x2251)+~P4(x2253)+~P2(x2252)+P3(f13(x2252,x2253,x2251),x2251)+P3(f13(x2252,x2253,x2251),f36(x2252))+E(x2251,f28(x2252,x2253)) % 0.57/0.73 [226]~P1(x2261)+~P1(x2262)+P3(f12(x2262,x2263,x2261),x2261)+P7(f12(x2262,x2263,x2261),x2262)+~P3(x2263,a35)+E(x2261,f34(x2262,x2263)) % 0.57/0.73 [229]~P1(x2291)+~P2(x2292)+P3(f14(x2292,x2293,x2291),x2291)+P3(f16(x2292,x2293,x2291),x2293)+~P7(x2293,f36(x2292))+E(x2291,f4(x2292,x2293)) % 0.57/0.73 [223]~P1(x2231)+~P4(x2233)+~P2(x2232)+P3(f13(x2232,x2233,x2231),x2231)+E(x2231,f28(x2232,x2233))+E(f32(x2232,f13(x2232,x2233,x2231)),x2233) % 0.57/0.73 [224]~P1(x2241)+~P1(x2242)+P3(f12(x2242,x2243,x2241),x2241)+~P3(x2243,a35)+E(x2241,f34(x2242,x2243))+E(f5(f12(x2242,x2243,x2241)),x2243) % 0.57/0.73 [233]~P1(x2331)+~P2(x2332)+P3(f14(x2332,x2333,x2331),x2331)+~P7(x2333,f36(x2332))+E(x2331,f4(x2332,x2333))+E(f32(x2332,f16(x2332,x2333,x2331)),f14(x2332,x2333,x2331)) % 0.57/0.73 [235]~P2(x2352)+~P2(x2351)+~E(f36(x2351),x2353)+~P7(x2353,f36(x2352))+E(x2351,f29(x2352,x2353))+~E(f32(x2351,f10(x2352,x2353,x2351)),f32(x2352,f10(x2352,x2353,x2351))) % 0.57/0.73 [150]~P1(x1504)+~P4(x1503)+~P4(x1501)+P3(x1501,x1502)+~E(x1501,x1503)+~E(x1502,f30(x1504,x1503)) % 0.57/0.73 [174]~P1(x1743)+~P4(x1742)+~P3(x1741,x1744)+E(x1741,x1742)+P3(x1741,x1743)+~E(x1744,f30(x1743,x1742)) % 0.57/0.73 [178]~P1(x1783)+~P4(x1784)+~P4(x1781)+~P3(x1781,x1783)+P3(x1781,x1782)+~E(x1782,f30(x1783,x1784)) % 0.57/0.73 [189]~P1(x1894)+~P7(x1891,x1894)+P3(x1891,x1892)+~P3(x1893,a35)+~E(x1892,f34(x1894,x1893))+~E(f5(x1891),x1893) % 0.57/0.73 [196]~P4(x1964)+~P2(x1963)+P3(x1961,x1962)+~E(f32(x1963,x1961),x1964)+~P3(x1961,f36(x1963))+~E(x1962,f28(x1963,x1964)) % 0.57/0.73 [210]~P2(x2103)+~P3(x2105,x2104)+P3(x2101,x2102)+~P7(x2104,f36(x2103))+~E(x2102,f4(x2103,x2104))+~E(f32(x2103,x2105),x2101) % 0.57/0.73 [203]E(f39(x2032),f39(x2031))+~P7(x2031,a35)+~P7(x2032,a35)+~P3(f39(x2031),x2032)+~P3(f39(x2032),x2031)+E(x2031,a33)+E(x2032,a33) % 0.57/0.73 [214]~P1(x2143)+~P1(x2142)+P7(x2142,x2143)+~P3(x2141,a35)+~P7(f34(x2142,x2141),f34(x2143,x2141))+E(x2141,a2)+E(f34(x2142,x2141),a33) % 0.57/0.73 [231]~P1(x2311)+~P1(x2312)+~P4(x2313)+E(f23(x2312,x2313,x2311),x2313)+P3(f23(x2312,x2313,x2311),x2311)+P3(f23(x2312,x2313,x2311),x2312)+E(x2311,f30(x2312,x2313)) % 0.57/0.73 [236]~P1(x2361)+~P1(x2362)+~P4(x2363)+~E(f23(x2362,x2363,x2361),x2363)+~P3(f23(x2362,x2363,x2361),x2361)+E(x2361,f30(x2362,x2363))+~P4(f23(x2362,x2363,x2361)) % 0.57/0.73 [237]~P1(x2371)+~P1(x2372)+~P4(x2373)+~P3(f23(x2372,x2373,x2371),x2371)+~P3(f23(x2372,x2373,x2371),x2372)+E(x2371,f30(x2372,x2373))+~P4(f23(x2372,x2373,x2371)) % 0.57/0.73 [240]~P1(x2401)+~P1(x2402)+~P3(x2403,a35)+~P3(f12(x2402,x2403,x2401),x2401)+~P7(f12(x2402,x2403,x2401),x2402)+E(x2401,f34(x2402,x2403))+~E(f5(f12(x2402,x2403,x2401)),x2403) % 0.57/0.73 [241]~P1(x2411)+~P4(x2413)+~P2(x2412)+~P3(f13(x2412,x2413,x2411),x2411)+~P3(f13(x2412,x2413,x2411),f36(x2412))+E(x2411,f28(x2412,x2413))+~E(f32(x2412,f13(x2412,x2413,x2411)),x2413) % 0.57/0.73 [179]~P1(x1794)+~P4(x1792)+~P4(x1791)+~P3(x1791,x1794)+E(x1791,x1792)+P3(x1791,x1793)+~E(x1793,f31(x1794,x1792)) % 0.57/0.73 [234]~P1(x2341)+~P2(x2342)+~P3(x2344,x2343)+~P7(x2343,f36(x2342))+~P3(f14(x2342,x2343,x2341),x2341)+~E(f32(x2342,x2344),f14(x2342,x2343,x2341))+E(x2341,f4(x2342,x2343)) % 0.57/0.73 [242]~P1(x2421)+~P1(x2422)+~P4(x2423)+E(f22(x2422,x2423,x2421),x2423)+~P3(f22(x2422,x2423,x2421),x2421)+~P3(f22(x2422,x2423,x2421),x2422)+E(x2421,f31(x2422,x2423))+~P4(f22(x2422,x2423,x2421)) % 0.57/0.73 [227]~P6(x2272)+~P2(x2273)+~E(f36(x2273),f34(x2272,x2271))+~P3(x2271,a35)+~P7(x2272,a35)+~P8(x2271,a1)+P6(f20(x2271,x2272,x2273))+~P7(f4(x2273,f36(x2273)),a41) % 0.57/0.73 [228]~P6(x2282)+~P2(x2283)+~E(f36(x2283),f34(x2282,x2281))+~P3(x2281,a35)+~P7(x2282,a35)+~P8(x2281,a1)+P3(f21(x2281,x2282,x2283),a41)+~P7(f4(x2283,f36(x2283)),a41) % 0.57/0.73 [230]~P6(x2302)+~P2(x2303)+~E(f36(x2303),f34(x2302,x2301))+~P3(x2301,a35)+~P7(x2302,a35)+~P8(x2301,a1)+P7(f20(x2301,x2302,x2303),x2302)+~P7(f4(x2303,f36(x2303)),a41) % 0.57/0.73 [243]~P6(x2434)+~P2(x2431)+~E(f36(x2431),f34(x2434,x2433))+~P3(x2433,a35)+~P7(x2434,a35)+~P8(x2433,a1)+E(f32(x2431,x2432),f21(x2433,x2434,x2431))+~P3(x2432,f34(f20(x2433,x2434,x2431),x2433))+~P7(f4(x2431,f36(x2431)),a41) % 0.57/0.73 %EqnAxiom % 0.57/0.73 [1]E(x11,x11) % 0.57/0.73 [2]E(x22,x21)+~E(x21,x22) % 0.57/0.73 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.57/0.73 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 0.57/0.73 [5]~E(x51,x52)+E(f34(x51,x53),f34(x52,x53)) % 0.57/0.73 [6]~E(x61,x62)+E(f34(x63,x61),f34(x63,x62)) % 0.57/0.73 [7]~E(x71,x72)+E(f36(x71),f36(x72)) % 0.57/0.73 [8]~E(x81,x82)+E(f32(x81,x83),f32(x82,x83)) % 0.57/0.73 [9]~E(x91,x92)+E(f32(x93,x91),f32(x93,x92)) % 0.57/0.73 [10]~E(x101,x102)+E(f4(x101,x103),f4(x102,x103)) % 0.57/0.73 [11]~E(x111,x112)+E(f4(x113,x111),f4(x113,x112)) % 0.57/0.73 [12]~E(x121,x122)+E(f5(x121),f5(x122)) % 0.57/0.73 [13]~E(x131,x132)+E(f20(x131,x133,x134),f20(x132,x133,x134)) % 0.57/0.73 [14]~E(x141,x142)+E(f20(x143,x141,x144),f20(x143,x142,x144)) % 0.57/0.73 [15]~E(x151,x152)+E(f20(x153,x154,x151),f20(x153,x154,x152)) % 0.57/0.73 [16]~E(x161,x162)+E(f10(x161,x163,x164),f10(x162,x163,x164)) % 0.57/0.73 [17]~E(x171,x172)+E(f10(x173,x171,x174),f10(x173,x172,x174)) % 0.57/0.73 [18]~E(x181,x182)+E(f10(x183,x184,x181),f10(x183,x184,x182)) % 0.57/0.73 [19]~E(x191,x192)+E(f37(x191),f37(x192)) % 0.57/0.73 [20]~E(x201,x202)+E(f38(x201),f38(x202)) % 0.57/0.73 [21]~E(x211,x212)+E(f11(x211,x213,x214),f11(x212,x213,x214)) % 0.57/0.73 [22]~E(x221,x222)+E(f11(x223,x221,x224),f11(x223,x222,x224)) % 0.57/0.73 [23]~E(x231,x232)+E(f11(x233,x234,x231),f11(x233,x234,x232)) % 0.57/0.73 [24]~E(x241,x242)+E(f6(x241),f6(x242)) % 0.57/0.73 [25]~E(x251,x252)+E(f12(x251,x253,x254),f12(x252,x253,x254)) % 0.57/0.73 [26]~E(x261,x262)+E(f12(x263,x261,x264),f12(x263,x262,x264)) % 0.57/0.73 [27]~E(x271,x272)+E(f12(x273,x274,x271),f12(x273,x274,x272)) % 0.57/0.73 [28]~E(x281,x282)+E(f21(x281,x283,x284),f21(x282,x283,x284)) % 0.57/0.73 [29]~E(x291,x292)+E(f21(x293,x291,x294),f21(x293,x292,x294)) % 0.57/0.73 [30]~E(x301,x302)+E(f21(x303,x304,x301),f21(x303,x304,x302)) % 0.57/0.73 [31]~E(x311,x312)+E(f29(x311,x313),f29(x312,x313)) % 0.57/0.73 [32]~E(x321,x322)+E(f29(x323,x321),f29(x323,x322)) % 0.57/0.73 [33]~E(x331,x332)+E(f17(x331),f17(x332)) % 0.57/0.73 [34]~E(x341,x342)+E(f30(x341,x343),f30(x342,x343)) % 0.57/0.73 [35]~E(x351,x352)+E(f30(x353,x351),f30(x353,x352)) % 0.57/0.73 [36]~E(x361,x362)+E(f27(x361,x363),f27(x362,x363)) % 0.57/0.73 [37]~E(x371,x372)+E(f27(x373,x371),f27(x373,x372)) % 0.57/0.73 [38]~E(x381,x382)+E(f23(x381,x383,x384),f23(x382,x383,x384)) % 0.57/0.73 [39]~E(x391,x392)+E(f23(x393,x391,x394),f23(x393,x392,x394)) % 0.57/0.73 [40]~E(x401,x402)+E(f23(x403,x404,x401),f23(x403,x404,x402)) % 0.57/0.73 [41]~E(x411,x412)+E(f31(x411,x413),f31(x412,x413)) % 0.57/0.73 [42]~E(x421,x422)+E(f31(x423,x421),f31(x423,x422)) % 0.57/0.73 [43]~E(x431,x432)+E(f8(x431,x433),f8(x432,x433)) % 0.57/0.73 [44]~E(x441,x442)+E(f8(x443,x441),f8(x443,x442)) % 0.57/0.73 [45]~E(x451,x452)+E(f22(x451,x453,x454),f22(x452,x453,x454)) % 0.57/0.73 [46]~E(x461,x462)+E(f22(x463,x461,x464),f22(x463,x462,x464)) % 0.57/0.73 [47]~E(x471,x472)+E(f22(x473,x474,x471),f22(x473,x474,x472)) % 0.57/0.73 [48]~E(x481,x482)+E(f28(x481,x483),f28(x482,x483)) % 0.57/0.73 [49]~E(x491,x492)+E(f28(x493,x491),f28(x493,x492)) % 0.57/0.73 [50]~E(x501,x502)+E(f39(x501),f39(x502)) % 0.57/0.73 [51]~E(x511,x512)+E(f19(x511,x513),f19(x512,x513)) % 0.57/0.73 [52]~E(x521,x522)+E(f19(x523,x521),f19(x523,x522)) % 0.57/0.73 [53]~E(x531,x532)+E(f15(x531,x533,x534,x535),f15(x532,x533,x534,x535)) % 0.57/0.73 [54]~E(x541,x542)+E(f15(x543,x541,x544,x545),f15(x543,x542,x544,x545)) % 0.57/0.73 [55]~E(x551,x552)+E(f15(x553,x554,x551,x555),f15(x553,x554,x552,x555)) % 0.57/0.73 [56]~E(x561,x562)+E(f15(x563,x564,x565,x561),f15(x563,x564,x565,x562)) % 0.57/0.73 [57]~E(x571,x572)+E(f13(x571,x573,x574),f13(x572,x573,x574)) % 0.57/0.73 [58]~E(x581,x582)+E(f13(x583,x581,x584),f13(x583,x582,x584)) % 0.57/0.73 [59]~E(x591,x592)+E(f13(x593,x594,x591),f13(x593,x594,x592)) % 0.57/0.73 [60]~E(x601,x602)+E(f9(x601,x603),f9(x602,x603)) % 0.57/0.73 [61]~E(x611,x612)+E(f9(x613,x611),f9(x613,x612)) % 0.57/0.73 [62]~E(x621,x622)+E(f7(x621),f7(x622)) % 0.57/0.73 [63]~E(x631,x632)+E(f14(x631,x633,x634),f14(x632,x633,x634)) % 0.57/0.73 [64]~E(x641,x642)+E(f14(x643,x641,x644),f14(x643,x642,x644)) % 0.57/0.73 [65]~E(x651,x652)+E(f14(x653,x654,x651),f14(x653,x654,x652)) % 0.57/0.73 [66]~E(x661,x662)+E(f40(x661),f40(x662)) % 0.57/0.73 [67]~E(x671,x672)+E(f24(x671,x673),f24(x672,x673)) % 0.57/0.73 [68]~E(x681,x682)+E(f24(x683,x681),f24(x683,x682)) % 0.57/0.73 [69]~E(x691,x692)+E(f16(x691,x693,x694),f16(x692,x693,x694)) % 0.57/0.73 [70]~E(x701,x702)+E(f16(x703,x701,x704),f16(x703,x702,x704)) % 0.57/0.73 [71]~E(x711,x712)+E(f16(x713,x714,x711),f16(x713,x714,x712)) % 0.57/0.73 [72]~E(x721,x722)+E(f25(x721,x723),f25(x722,x723)) % 0.57/0.73 [73]~E(x731,x732)+E(f25(x733,x731),f25(x733,x732)) % 0.57/0.73 [74]~E(x741,x742)+E(f18(x741,x743),f18(x742,x743)) % 0.57/0.73 [75]~E(x751,x752)+E(f18(x753,x751),f18(x753,x752)) % 0.57/0.73 [76]~E(x761,x762)+E(f26(x761,x763),f26(x762,x763)) % 0.57/0.73 [77]~E(x771,x772)+E(f26(x773,x771),f26(x773,x772)) % 0.57/0.73 [78]~P1(x781)+P1(x782)+~E(x781,x782) % 0.57/0.73 [79]P3(x792,x793)+~E(x791,x792)+~P3(x791,x793) % 0.57/0.73 [80]P3(x803,x802)+~E(x801,x802)+~P3(x803,x801) % 0.57/0.73 [81]~P5(x811)+P5(x812)+~E(x811,x812) % 0.57/0.73 [82]~P6(x821)+P6(x822)+~E(x821,x822) % 0.57/0.73 [83]~P2(x831)+P2(x832)+~E(x831,x832) % 0.57/0.73 [84]~P4(x841)+P4(x842)+~E(x841,x842) % 0.57/0.73 [85]P7(x852,x853)+~E(x851,x852)+~P7(x851,x853) % 0.57/0.73 [86]P7(x863,x862)+~E(x861,x862)+~P7(x863,x861) % 0.57/0.73 [87]P9(x872,x873)+~E(x871,x872)+~P9(x871,x873) % 0.57/0.73 [88]P9(x883,x882)+~E(x881,x882)+~P9(x883,x881) % 0.57/0.73 [89]P8(x892,x893)+~E(x891,x892)+~P8(x891,x893) % 0.57/0.73 [90]P8(x903,x902)+~E(x901,x902)+~P8(x903,x901) % 0.57/0.73 % 0.57/0.73 %------------------------------------------- % 0.57/0.73 cnf(279,plain, % 0.57/0.73 ($false), % 0.57/0.73 inference(scs_inference,[],[91,105]), % 0.57/0.73 ['proof']). % 0.57/0.73 % SZS output end Proof % 0.57/0.73 % Total time :0.020000s %------------------------------------------------------------------------------