%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM578+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 : n029.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 12:25:09 EDT 2024 % Result : Theorem 0.70s 0.79s % Output : CNFRefutation 0.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM578+1 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sat Jun 22 22:53:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.21/0.58 start to proof:theBenchmark % 0.70/0.76 %------------------------------------------- % 0.70/0.76 % File :CSE---1.7 % 0.70/0.76 % Problem :theBenchmark % 0.70/0.76 % Transform :cnf % 0.70/0.76 % Format :tptp:raw % 0.70/0.76 % Command :java -jar mcs_scs.jar %d %s % 0.70/0.76 % 0.70/0.76 % Result :Theorem 0.080000s % 0.70/0.76 % Output :CNFRefutation 0.080000s % 0.70/0.76 %------------------------------------------- % 0.70/0.76 %------------------------------------------------------------------------------ % 0.70/0.76 % File : NUM578+1 : TPTP v8.2.0. Released v4.0.0. % 0.70/0.76 % Domain : Number Theory % 0.70/0.76 % Problem : Ramsey's Infinite Theorem 15_02_05_03, 00 expansion % 0.70/0.76 % Version : Especial. % 0.70/0.76 % English : % 0.70/0.76 % 0.70/0.76 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 0.70/0.76 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 0.70/0.76 % Source : [Pas08] % 0.70/0.76 % Names : ramsey_15_02_05_03.00 [Pas08] % 0.70/0.76 % 0.70/0.76 % Status : Theorem % 0.70/0.76 % Rating : 0.28 v8.2.0, 0.25 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.20 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.26 v7.0.0, 0.20 v6.4.0, 0.23 v6.3.0, 0.25 v6.2.0, 0.24 v6.1.0, 0.33 v6.0.0, 0.26 v5.5.0, 0.37 v5.4.0, 0.39 v5.3.0, 0.44 v5.2.0, 0.35 v5.1.0, 0.48 v5.0.0, 0.54 v4.1.0, 0.61 v4.0.1, 0.83 v4.0.0 % 0.70/0.76 % Syntax : Number of formulae : 86 ( 6 unt; 11 def) % 0.70/0.76 % Number of atoms : 340 ( 59 equ) % 0.70/0.76 % Maximal formula atoms : 12 ( 3 avg) % 0.70/0.76 % Number of connectives : 280 ( 26 ~; 5 |; 104 &) % 0.70/0.77 % ( 22 <=>; 123 =>; 0 <=; 0 <~>) % 0.70/0.77 % Maximal formula depth : 15 ( 5 avg) % 0.70/0.77 % Maximal term depth : 4 ( 1 avg) % 0.70/0.77 % Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty) % 0.70/0.77 % Number of functors : 25 ( 25 usr; 11 con; 0-2 aty) % 0.70/0.77 % Number of variables : 151 ( 143 !; 8 ?) % 0.70/0.77 % SPC : FOF_THM_RFO_SEQ % 0.70/0.77 % 0.70/0.77 % Comments : Problem generated by the SAD system [VLP07] % 0.70/0.77 %------------------------------------------------------------------------------ % 0.70/0.77 fof(mSetSort,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aSet0(W0) % 0.70/0.77 => $true ) ). % 0.70/0.77 % 0.70/0.77 fof(mElmSort,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aElement0(W0) % 0.70/0.77 => $true ) ). % 0.70/0.77 % 0.70/0.77 fof(mEOfElem,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aSet0(W0) % 0.70/0.77 => ! [W1] : % 0.70/0.77 ( aElementOf0(W1,W0) % 0.70/0.77 => aElement0(W1) ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mFinRel,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aSet0(W0) % 0.70/0.77 => ( isFinite0(W0) % 0.70/0.77 => $true ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mDefEmp,definition, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( W0 = slcrc0 % 0.70/0.77 <=> ( aSet0(W0) % 0.70/0.77 & ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mEmpFin,axiom, % 0.70/0.77 isFinite0(slcrc0) ). % 0.70/0.77 % 0.70/0.77 fof(mCntRel,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aSet0(W0) % 0.70/0.77 => ( isCountable0(W0) % 0.70/0.77 => $true ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mCountNFin,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( ( aSet0(W0) % 0.70/0.77 & isCountable0(W0) ) % 0.70/0.77 => ~ isFinite0(W0) ) ). % 0.70/0.77 % 0.70/0.77 fof(mCountNFin_01,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( ( aSet0(W0) % 0.70/0.77 & isCountable0(W0) ) % 0.70/0.77 => W0 != slcrc0 ) ). % 0.70/0.77 % 0.70/0.77 fof(mDefSub,definition, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aSet0(W0) % 0.70/0.77 => ! [W1] : % 0.70/0.77 ( aSubsetOf0(W1,W0) % 0.70/0.77 <=> ( aSet0(W1) % 0.70/0.77 & ! [W2] : % 0.70/0.77 ( aElementOf0(W2,W1) % 0.70/0.77 => aElementOf0(W2,W0) ) ) ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mSubFSet,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( ( aSet0(W0) % 0.70/0.77 & isFinite0(W0) ) % 0.70/0.77 => ! [W1] : % 0.70/0.77 ( aSubsetOf0(W1,W0) % 0.70/0.77 => isFinite0(W1) ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mSubRefl,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aSet0(W0) % 0.70/0.77 => aSubsetOf0(W0,W0) ) ). % 0.70/0.77 % 0.70/0.77 fof(mSubASymm,axiom, % 0.70/0.77 ! [W0,W1] : % 0.70/0.77 ( ( aSet0(W0) % 0.70/0.77 & aSet0(W1) ) % 0.70/0.77 => ( ( aSubsetOf0(W0,W1) % 0.70/0.77 & aSubsetOf0(W1,W0) ) % 0.70/0.77 => W0 = W1 ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mSubTrans,axiom, % 0.70/0.77 ! [W0,W1,W2] : % 0.70/0.77 ( ( aSet0(W0) % 0.70/0.77 & aSet0(W1) % 0.70/0.77 & aSet0(W2) ) % 0.70/0.77 => ( ( aSubsetOf0(W0,W1) % 0.70/0.77 & aSubsetOf0(W1,W2) ) % 0.70/0.77 => aSubsetOf0(W0,W2) ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mDefCons,definition, % 0.70/0.77 ! [W0,W1] : % 0.70/0.77 ( ( aSet0(W0) % 0.70/0.77 & aElement0(W1) ) % 0.70/0.77 => ! [W2] : % 0.70/0.77 ( W2 = sdtpldt0(W0,W1) % 0.70/0.77 <=> ( aSet0(W2) % 0.70/0.77 & ! [W3] : % 0.70/0.77 ( aElementOf0(W3,W2) % 0.70/0.77 <=> ( aElement0(W3) % 0.70/0.77 & ( aElementOf0(W3,W0) % 0.70/0.77 | W3 = W1 ) ) ) ) ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mDefDiff,definition, % 0.70/0.77 ! [W0,W1] : % 0.70/0.77 ( ( aSet0(W0) % 0.70/0.77 & aElement0(W1) ) % 0.70/0.77 => ! [W2] : % 0.70/0.77 ( W2 = sdtmndt0(W0,W1) % 0.70/0.77 <=> ( aSet0(W2) % 0.70/0.77 & ! [W3] : % 0.70/0.77 ( aElementOf0(W3,W2) % 0.70/0.77 <=> ( aElement0(W3) % 0.70/0.77 & aElementOf0(W3,W0) % 0.70/0.77 & W3 != W1 ) ) ) ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mConsDiff,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aSet0(W0) % 0.70/0.77 => ! [W1] : % 0.70/0.77 ( aElementOf0(W1,W0) % 0.70/0.77 => sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mDiffCons,axiom, % 0.70/0.77 ! [W0,W1] : % 0.70/0.77 ( ( aElement0(W0) % 0.70/0.77 & aSet0(W1) ) % 0.70/0.77 => ( ~ aElementOf0(W0,W1) % 0.70/0.77 => sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mCConsSet,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aElement0(W0) % 0.70/0.77 => ! [W1] : % 0.70/0.77 ( ( aSet0(W1) % 0.70/0.77 & isCountable0(W1) ) % 0.70/0.77 => isCountable0(sdtpldt0(W1,W0)) ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mCDiffSet,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aElement0(W0) % 0.70/0.77 => ! [W1] : % 0.70/0.77 ( ( aSet0(W1) % 0.70/0.77 & isCountable0(W1) ) % 0.70/0.77 => isCountable0(sdtmndt0(W1,W0)) ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mFConsSet,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aElement0(W0) % 0.70/0.77 => ! [W1] : % 0.70/0.77 ( ( aSet0(W1) % 0.70/0.77 & isFinite0(W1) ) % 0.70/0.77 => isFinite0(sdtpldt0(W1,W0)) ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mFDiffSet,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aElement0(W0) % 0.70/0.77 => ! [W1] : % 0.70/0.77 ( ( aSet0(W1) % 0.70/0.77 & isFinite0(W1) ) % 0.70/0.77 => isFinite0(sdtmndt0(W1,W0)) ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mNATSet,axiom, % 0.70/0.77 ( aSet0(szNzAzT0) % 0.70/0.77 & isCountable0(szNzAzT0) ) ). % 0.70/0.77 % 0.70/0.77 fof(mZeroNum,axiom, % 0.70/0.77 aElementOf0(sz00,szNzAzT0) ). % 0.70/0.77 % 0.70/0.77 fof(mSuccNum,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aElementOf0(W0,szNzAzT0) % 0.70/0.77 => ( aElementOf0(szszuzczcdt0(W0),szNzAzT0) % 0.70/0.77 & szszuzczcdt0(W0) != sz00 ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mSuccEquSucc,axiom, % 0.70/0.77 ! [W0,W1] : % 0.70/0.77 ( ( aElementOf0(W0,szNzAzT0) % 0.70/0.77 & aElementOf0(W1,szNzAzT0) ) % 0.70/0.77 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 0.70/0.77 => W0 = W1 ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mNatExtra,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aElementOf0(W0,szNzAzT0) % 0.70/0.77 => ( W0 = sz00 % 0.70/0.77 | ? [W1] : % 0.70/0.77 ( aElementOf0(W1,szNzAzT0) % 0.70/0.77 & W0 = szszuzczcdt0(W1) ) ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mNatNSucc,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aElementOf0(W0,szNzAzT0) % 0.70/0.77 => W0 != szszuzczcdt0(W0) ) ). % 0.70/0.77 % 0.70/0.77 fof(mLessRel,axiom, % 0.70/0.77 ! [W0,W1] : % 0.70/0.77 ( ( aElementOf0(W0,szNzAzT0) % 0.70/0.77 & aElementOf0(W1,szNzAzT0) ) % 0.70/0.77 => ( sdtlseqdt0(W0,W1) % 0.70/0.77 => $true ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mZeroLess,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aElementOf0(W0,szNzAzT0) % 0.70/0.77 => sdtlseqdt0(sz00,W0) ) ). % 0.70/0.77 % 0.70/0.77 fof(mNoScLessZr,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aElementOf0(W0,szNzAzT0) % 0.70/0.77 => ~ sdtlseqdt0(szszuzczcdt0(W0),sz00) ) ). % 0.70/0.77 % 0.70/0.77 fof(mSuccLess,axiom, % 0.70/0.77 ! [W0,W1] : % 0.70/0.77 ( ( aElementOf0(W0,szNzAzT0) % 0.70/0.77 & aElementOf0(W1,szNzAzT0) ) % 0.70/0.77 => ( sdtlseqdt0(W0,W1) % 0.70/0.77 <=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ) ). % 0.70/0.77 % 0.70/0.77 fof(mLessSucc,axiom, % 0.70/0.77 ! [W0] : % 0.70/0.77 ( aElementOf0(W0,szNzAzT0) % 0.70/0.77 => sdtlseqdt0(W0,szszuzczcdt0(W0)) ) ). % 0.70/0.78 % 0.70/0.78 fof(mLessRefl,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aElementOf0(W0,szNzAzT0) % 0.70/0.78 => sdtlseqdt0(W0,W0) ) ). % 0.70/0.78 % 0.70/0.78 fof(mLessASymm,axiom, % 0.70/0.78 ! [W0,W1] : % 0.70/0.78 ( ( aElementOf0(W0,szNzAzT0) % 0.70/0.78 & aElementOf0(W1,szNzAzT0) ) % 0.70/0.78 => ( ( sdtlseqdt0(W0,W1) % 0.70/0.78 & sdtlseqdt0(W1,W0) ) % 0.70/0.78 => W0 = W1 ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mLessTrans,axiom, % 0.70/0.78 ! [W0,W1,W2] : % 0.70/0.78 ( ( aElementOf0(W0,szNzAzT0) % 0.70/0.78 & aElementOf0(W1,szNzAzT0) % 0.70/0.78 & aElementOf0(W2,szNzAzT0) ) % 0.70/0.78 => ( ( sdtlseqdt0(W0,W1) % 0.70/0.78 & sdtlseqdt0(W1,W2) ) % 0.70/0.78 => sdtlseqdt0(W0,W2) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mLessTotal,axiom, % 0.70/0.78 ! [W0,W1] : % 0.70/0.78 ( ( aElementOf0(W0,szNzAzT0) % 0.70/0.78 & aElementOf0(W1,szNzAzT0) ) % 0.70/0.78 => ( sdtlseqdt0(W0,W1) % 0.70/0.78 | sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mIHSort,axiom, % 0.70/0.78 ! [W0,W1] : % 0.70/0.78 ( ( aElementOf0(W0,szNzAzT0) % 0.70/0.78 & aElementOf0(W1,szNzAzT0) ) % 0.70/0.78 => ( iLess0(W0,W1) % 0.70/0.78 => $true ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mIH,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aElementOf0(W0,szNzAzT0) % 0.70/0.78 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 0.70/0.78 % 0.70/0.78 fof(mCardS,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aSet0(W0) % 0.70/0.78 => aElement0(sbrdtbr0(W0)) ) ). % 0.70/0.78 % 0.70/0.78 fof(mCardNum,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aSet0(W0) % 0.70/0.78 => ( aElementOf0(sbrdtbr0(W0),szNzAzT0) % 0.70/0.78 <=> isFinite0(W0) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mCardEmpty,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aSet0(W0) % 0.70/0.78 => ( sbrdtbr0(W0) = sz00 % 0.70/0.78 <=> W0 = slcrc0 ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mCardCons,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( ( aSet0(W0) % 0.70/0.78 & isFinite0(W0) ) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( aElement0(W1) % 0.70/0.78 => ( ~ aElementOf0(W1,W0) % 0.70/0.78 => sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mCardDiff,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aSet0(W0) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( ( isFinite0(W0) % 0.70/0.78 & aElementOf0(W1,W0) ) % 0.70/0.78 => szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mCardSub,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aSet0(W0) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( ( isFinite0(W0) % 0.70/0.78 & aSubsetOf0(W1,W0) ) % 0.70/0.78 => sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mCardSubEx,axiom, % 0.70/0.78 ! [W0,W1] : % 0.70/0.78 ( ( aSet0(W0) % 0.70/0.78 & aElementOf0(W1,szNzAzT0) ) % 0.70/0.78 => ( ( isFinite0(W0) % 0.70/0.78 & sdtlseqdt0(W1,sbrdtbr0(W0)) ) % 0.70/0.78 => ? [W2] : % 0.70/0.78 ( aSubsetOf0(W2,W0) % 0.70/0.78 & sbrdtbr0(W2) = W1 ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mDefMin,definition, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( ( aSubsetOf0(W0,szNzAzT0) % 0.70/0.78 & W0 != slcrc0 ) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( W1 = szmzizndt0(W0) % 0.70/0.78 <=> ( aElementOf0(W1,W0) % 0.70/0.78 & ! [W2] : % 0.70/0.78 ( aElementOf0(W2,W0) % 0.70/0.78 => sdtlseqdt0(W1,W2) ) ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mDefMax,definition, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( ( aSubsetOf0(W0,szNzAzT0) % 0.70/0.78 & isFinite0(W0) % 0.70/0.78 & W0 != slcrc0 ) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( W1 = szmzazxdt0(W0) % 0.70/0.78 <=> ( aElementOf0(W1,W0) % 0.70/0.78 & ! [W2] : % 0.70/0.78 ( aElementOf0(W2,W0) % 0.70/0.78 => sdtlseqdt0(W2,W1) ) ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mMinMin,axiom, % 0.70/0.78 ! [W0,W1] : % 0.70/0.78 ( ( aSubsetOf0(W0,szNzAzT0) % 0.70/0.78 & aSubsetOf0(W1,szNzAzT0) % 0.70/0.78 & W0 != slcrc0 % 0.70/0.78 & W1 != slcrc0 ) % 0.70/0.78 => ( ( aElementOf0(szmzizndt0(W0),W1) % 0.70/0.78 & aElementOf0(szmzizndt0(W1),W0) ) % 0.70/0.78 => szmzizndt0(W0) = szmzizndt0(W1) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mDefSeg,definition, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aElementOf0(W0,szNzAzT0) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( W1 = slbdtrb0(W0) % 0.70/0.78 <=> ( aSet0(W1) % 0.70/0.78 & ! [W2] : % 0.70/0.78 ( aElementOf0(W2,W1) % 0.70/0.78 <=> ( aElementOf0(W2,szNzAzT0) % 0.70/0.78 & sdtlseqdt0(szszuzczcdt0(W2),W0) ) ) ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mSegFin,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aElementOf0(W0,szNzAzT0) % 0.70/0.78 => isFinite0(slbdtrb0(W0)) ) ). % 0.70/0.78 % 0.70/0.78 fof(mSegZero,axiom, % 0.70/0.78 slbdtrb0(sz00) = slcrc0 ). % 0.70/0.78 % 0.70/0.78 fof(mSegSucc,axiom, % 0.70/0.78 ! [W0,W1] : % 0.70/0.78 ( ( aElementOf0(W0,szNzAzT0) % 0.70/0.78 & aElementOf0(W1,szNzAzT0) ) % 0.70/0.78 => ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1))) % 0.70/0.78 <=> ( aElementOf0(W0,slbdtrb0(W1)) % 0.70/0.78 | W0 = W1 ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mSegLess,axiom, % 0.70/0.78 ! [W0,W1] : % 0.70/0.78 ( ( aElementOf0(W0,szNzAzT0) % 0.70/0.78 & aElementOf0(W1,szNzAzT0) ) % 0.70/0.78 => ( sdtlseqdt0(W0,W1) % 0.70/0.78 <=> aSubsetOf0(slbdtrb0(W0),slbdtrb0(W1)) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mFinSubSeg,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( ( aSubsetOf0(W0,szNzAzT0) % 0.70/0.78 & isFinite0(W0) ) % 0.70/0.78 => ? [W1] : % 0.70/0.78 ( aElementOf0(W1,szNzAzT0) % 0.70/0.78 & aSubsetOf0(W0,slbdtrb0(W1)) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mCardSeg,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aElementOf0(W0,szNzAzT0) % 0.70/0.78 => sbrdtbr0(slbdtrb0(W0)) = W0 ) ). % 0.70/0.78 % 0.70/0.78 fof(mDefSel,definition, % 0.70/0.78 ! [W0,W1] : % 0.70/0.78 ( ( aSet0(W0) % 0.70/0.78 & aElementOf0(W1,szNzAzT0) ) % 0.70/0.78 => ! [W2] : % 0.70/0.78 ( W2 = slbdtsldtrb0(W0,W1) % 0.70/0.78 <=> ( aSet0(W2) % 0.70/0.78 & ! [W3] : % 0.70/0.78 ( aElementOf0(W3,W2) % 0.70/0.78 <=> ( aSubsetOf0(W3,W0) % 0.70/0.78 & sbrdtbr0(W3) = W1 ) ) ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mSelFSet,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( ( aSet0(W0) % 0.70/0.78 & isFinite0(W0) ) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( aElementOf0(W1,szNzAzT0) % 0.70/0.78 => isFinite0(slbdtsldtrb0(W0,W1)) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mSelNSet,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( ( aSet0(W0) % 0.70/0.78 & ~ isFinite0(W0) ) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( aElementOf0(W1,szNzAzT0) % 0.70/0.78 => slbdtsldtrb0(W0,W1) != slcrc0 ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mSelCSet,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( ( aSet0(W0) % 0.70/0.78 & isCountable0(W0) ) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( ( aElementOf0(W1,szNzAzT0) % 0.70/0.78 & W1 != sz00 ) % 0.70/0.78 => isCountable0(slbdtsldtrb0(W0,W1)) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mSelSub,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aElementOf0(W0,szNzAzT0) % 0.70/0.78 => ! [W1,W2] : % 0.70/0.78 ( ( aSet0(W1) % 0.70/0.78 & aSet0(W2) % 0.70/0.78 & W0 != sz00 ) % 0.70/0.78 => ( ( aSubsetOf0(slbdtsldtrb0(W1,W0),slbdtsldtrb0(W2,W0)) % 0.70/0.78 & slbdtsldtrb0(W1,W0) != slcrc0 ) % 0.70/0.78 => aSubsetOf0(W1,W2) ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mSelExtra,axiom, % 0.70/0.78 ! [W0,W1] : % 0.70/0.78 ( ( aSet0(W0) % 0.70/0.78 & aElementOf0(W1,szNzAzT0) ) % 0.70/0.78 => ! [W2] : % 0.70/0.78 ( ( aSubsetOf0(W2,slbdtsldtrb0(W0,W1)) % 0.70/0.78 & isFinite0(W2) ) % 0.70/0.78 => ? [W3] : % 0.70/0.78 ( aSubsetOf0(W3,W0) % 0.70/0.78 & isFinite0(W3) % 0.70/0.78 & aSubsetOf0(W2,slbdtsldtrb0(W3,W1)) ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mFunSort,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aFunction0(W0) % 0.70/0.78 => $true ) ). % 0.70/0.78 % 0.70/0.78 fof(mDomSet,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aFunction0(W0) % 0.70/0.78 => aSet0(szDzozmdt0(W0)) ) ). % 0.70/0.78 % 0.70/0.78 fof(mImgElm,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aFunction0(W0) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( aElementOf0(W1,szDzozmdt0(W0)) % 0.70/0.78 => aElement0(sdtlpdtrp0(W0,W1)) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mDefPtt,definition, % 0.70/0.78 ! [W0,W1] : % 0.70/0.78 ( ( aFunction0(W0) % 0.70/0.78 & aElement0(W1) ) % 0.70/0.78 => ! [W2] : % 0.70/0.78 ( W2 = sdtlbdtrb0(W0,W1) % 0.70/0.78 <=> ( aSet0(W2) % 0.70/0.78 & ! [W3] : % 0.70/0.78 ( aElementOf0(W3,W2) % 0.70/0.78 <=> ( aElementOf0(W3,szDzozmdt0(W0)) % 0.70/0.78 & sdtlpdtrp0(W0,W3) = W1 ) ) ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mPttSet,axiom, % 0.70/0.78 ! [W0,W1] : % 0.70/0.78 ( ( aFunction0(W0) % 0.70/0.78 & aElement0(W1) ) % 0.70/0.78 => aSubsetOf0(sdtlbdtrb0(W0,W1),szDzozmdt0(W0)) ) ). % 0.70/0.78 % 0.70/0.78 fof(mDefSImg,definition, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aFunction0(W0) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( aSubsetOf0(W1,szDzozmdt0(W0)) % 0.70/0.78 => ! [W2] : % 0.70/0.78 ( W2 = sdtlcdtrc0(W0,W1) % 0.70/0.78 <=> ( aSet0(W2) % 0.70/0.78 & ! [W3] : % 0.70/0.78 ( aElementOf0(W3,W2) % 0.70/0.78 <=> ? [W4] : % 0.70/0.78 ( aElementOf0(W4,W1) % 0.70/0.78 & sdtlpdtrp0(W0,W4) = W3 ) ) ) ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mImgRng,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aFunction0(W0) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( aElementOf0(W1,szDzozmdt0(W0)) % 0.70/0.78 => aElementOf0(sdtlpdtrp0(W0,W1),sdtlcdtrc0(W0,szDzozmdt0(W0))) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mDefRst,definition, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aFunction0(W0) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( aSubsetOf0(W1,szDzozmdt0(W0)) % 0.70/0.78 => ! [W2] : % 0.70/0.78 ( W2 = sdtexdt0(W0,W1) % 0.70/0.78 <=> ( aFunction0(W2) % 0.70/0.78 & szDzozmdt0(W2) = W1 % 0.70/0.78 & ! [W3] : % 0.70/0.78 ( aElementOf0(W3,W1) % 0.70/0.78 => sdtlpdtrp0(W2,W3) = sdtlpdtrp0(W0,W3) ) ) ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mImgCount,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aFunction0(W0) % 0.70/0.78 => ! [W1] : % 0.70/0.78 ( ( aSubsetOf0(W1,szDzozmdt0(W0)) % 0.70/0.78 & isCountable0(W1) ) % 0.70/0.78 => ( ! [W2,W3] : % 0.70/0.78 ( ( aElementOf0(W2,szDzozmdt0(W0)) % 0.70/0.78 & aElementOf0(W3,szDzozmdt0(W0)) % 0.70/0.78 & W2 != W3 ) % 0.70/0.78 => sdtlpdtrp0(W0,W2) != sdtlpdtrp0(W0,W3) ) % 0.70/0.78 => isCountable0(sdtlcdtrc0(W0,W1)) ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(mDirichlet,axiom, % 0.70/0.78 ! [W0] : % 0.70/0.78 ( aFunction0(W0) % 0.70/0.78 => ( ( isCountable0(szDzozmdt0(W0)) % 0.70/0.78 & isFinite0(sdtlcdtrc0(W0,szDzozmdt0(W0))) ) % 0.70/0.78 => ( aElement0(szDzizrdt0(W0)) % 0.70/0.78 & isCountable0(sdtlbdtrb0(W0,szDzizrdt0(W0))) ) ) ) ). % 0.70/0.78 % 0.70/0.78 fof(m__3291,hypothesis, % 0.70/0.78 ( aSet0(xT) % 0.70/0.78 & isFinite0(xT) ) ). % 0.70/0.78 % 0.70/0.78 fof(m__3418,hypothesis, % 0.70/0.78 aElementOf0(xK,szNzAzT0) ). % 0.70/0.78 % 0.70/0.78 fof(m__3435,hypothesis, % 0.70/0.78 ( aSubsetOf0(xS,szNzAzT0) % 0.70/0.78 & isCountable0(xS) ) ). % 0.70/0.78 % 0.70/0.78 fof(m__3453,hypothesis, % 0.70/0.78 ( aFunction0(xc) % 0.70/0.78 & szDzozmdt0(xc) = slbdtsldtrb0(xS,xK) % 0.70/0.78 & aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ). % 0.70/0.78 % 0.70/0.79 fof(m__3398,hypothesis, % 0.70/0.79 ! [W0] : % 0.70/0.79 ( aElementOf0(W0,szNzAzT0) % 0.70/0.79 => ! [W1] : % 0.70/0.79 ( ( aSubsetOf0(W1,szNzAzT0) % 0.70/0.79 & isCountable0(W1) ) % 0.70/0.79 => ! [W2] : % 0.70/0.79 ( ( aFunction0(W2) % 0.70/0.79 & szDzozmdt0(W2) = slbdtsldtrb0(W1,W0) % 0.70/0.79 & aSubsetOf0(sdtlcdtrc0(W2,szDzozmdt0(W2)),xT) ) % 0.70/0.79 => ( iLess0(W0,xK) % 0.70/0.79 => ? [W3] : % 0.70/0.79 ( aElementOf0(W3,xT) % 0.70/0.79 & ? [W4] : % 0.70/0.79 ( aSubsetOf0(W4,W1) % 0.70/0.79 & isCountable0(W4) % 0.70/0.79 & ! [W5] : % 0.70/0.79 ( aElementOf0(W5,slbdtsldtrb0(W4,W0)) % 0.70/0.79 => sdtlpdtrp0(W2,W5) = W3 ) ) ) ) ) ) ) ). % 0.70/0.79 % 0.70/0.79 fof(m__3462,hypothesis, % 0.70/0.79 xK != sz00 ). % 0.70/0.79 % 0.70/0.79 fof(m__3520,hypothesis, % 0.70/0.79 xK != sz00 ). % 0.70/0.79 % 0.70/0.79 fof(m__3533,hypothesis, % 0.70/0.79 ( aElementOf0(xk,szNzAzT0) % 0.70/0.79 & szszuzczcdt0(xk) = xK ) ). % 0.70/0.79 % 0.70/0.79 fof(m__3623,hypothesis, % 0.70/0.79 ( aFunction0(xN) % 0.70/0.79 & szDzozmdt0(xN) = szNzAzT0 % 0.70/0.79 & sdtlpdtrp0(xN,sz00) = xS % 0.70/0.79 & ! [W0] : % 0.70/0.79 ( aElementOf0(W0,szNzAzT0) % 0.70/0.79 => ( ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) % 0.70/0.79 & isCountable0(sdtlpdtrp0(xN,W0)) ) % 0.70/0.79 => ( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) % 0.70/0.79 & isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0))) ) ) ) ) ). % 0.70/0.79 % 0.70/0.79 fof(m__3671,hypothesis, % 0.70/0.79 ! [W0] : % 0.70/0.79 ( aElementOf0(W0,szNzAzT0) % 0.70/0.79 => ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) % 0.70/0.79 & isCountable0(sdtlpdtrp0(xN,W0)) ) ) ). % 0.70/0.79 % 0.70/0.79 fof(m__3754,hypothesis, % 0.70/0.79 ! [W0,W1] : % 0.70/0.79 ( ( aElementOf0(W0,szNzAzT0) % 0.70/0.79 & aElementOf0(W1,szNzAzT0) ) % 0.70/0.79 => ( sdtlseqdt0(W1,W0) % 0.70/0.79 => aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1)) ) ) ). % 0.70/0.79 % 0.70/0.79 fof(m__3856,hypothesis, % 0.70/0.79 ( aElementOf0(xi,szNzAzT0) % 0.70/0.79 & aElementOf0(xj,szNzAzT0) ) ). % 0.70/0.79 % 0.70/0.79 fof(m__3856_02,hypothesis, % 0.70/0.79 ( xi != xj % 0.70/0.79 => ( sdtlseqdt0(szszuzczcdt0(xj),xi) % 0.70/0.79 | sdtlseqdt0(szszuzczcdt0(xi),xj) ) ) ). % 0.70/0.79 % 0.70/0.79 fof(m__,conjecture, % 0.70/0.79 ( ! [W0,W1] : % 0.70/0.79 ( ( aElementOf0(W0,szNzAzT0) % 0.70/0.79 & aElementOf0(W1,szNzAzT0) ) % 0.70/0.79 => ( sdtlseqdt0(szszuzczcdt0(W0),W1) % 0.70/0.79 => ( aSubsetOf0(sdtlpdtrp0(xN,W1),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) % 0.70/0.79 & szmzizndt0(sdtlpdtrp0(xN,W1)) != szmzizndt0(sdtlpdtrp0(xN,W0)) ) ) ) % 0.70/0.79 => ( xi != xj % 0.70/0.79 => szmzizndt0(sdtlpdtrp0(xN,xi)) != szmzizndt0(sdtlpdtrp0(xN,xj)) ) ) ). % 0.70/0.79 % 0.70/0.79 %------------------------------------------------------------------------------ % 0.70/0.79 %------------------------------------------- % 0.70/0.79 % Proof found % 0.70/0.79 % SZS status Theorem for theBenchmark % 0.70/0.79 % SZS output start Proof % 0.70/0.79 %ClaNum:256(EqnAxiom:88) % 0.70/0.79 %VarNum:1159(SingletonVarNum:336) % 0.70/0.79 %MaxLitNum:9 % 0.70/0.79 %MaxfuncDepth:3 % 0.70/0.79 %SharedTerms:50 % 0.70/0.79 %goalClause: 109 112 223 237 % 0.70/0.79 %singleGoalClaCount:2 % 0.70/0.79 [92]P1(a37) % 0.70/0.79 [93]P1(a42) % 0.70/0.79 [94]P5(a33) % 0.70/0.79 [95]P5(a42) % 0.70/0.79 [96]P6(a37) % 0.70/0.79 [97]P6(a43) % 0.70/0.79 [98]P2(a44) % 0.70/0.79 [99]P2(a41) % 0.70/0.79 [101]P3(a3,a37) % 0.70/0.79 [102]P3(a40,a37) % 0.70/0.79 [103]P3(a1,a37) % 0.70/0.79 [104]P3(a45,a37) % 0.70/0.79 [105]P3(a46,a37) % 0.70/0.79 [106]P7(a43,a37) % 0.70/0.79 [111]~E(a3,a40) % 0.70/0.79 [112]~E(a46,a45) % 0.70/0.79 [89]E(f2(a1),a40) % 0.70/0.79 [90]E(f4(a3),a33) % 0.70/0.79 [91]E(f35(a41),a37) % 0.70/0.79 [100]E(f5(a41,a3),a43) % 0.70/0.79 [107]E(f34(a43,a40),f35(a44)) % 0.70/0.79 [108]P7(f6(a44,f35(a44)),a42) % 0.70/0.79 [109]E(f38(f5(a41,a46)),f38(f5(a41,a45))) % 0.70/0.79 [113]P1(x1131)+~E(x1131,a33) % 0.70/0.79 [120]~P1(x1201)+P7(x1201,x1201) % 0.70/0.79 [128]~P3(x1281,a37)+P9(a3,x1281) % 0.70/0.79 [134]P9(x1341,x1341)+~P3(x1341,a37) % 0.70/0.79 [117]~P2(x1171)+P1(f35(x1171)) % 0.70/0.79 [118]~P1(x1181)+P4(f7(x1181)) % 0.70/0.79 [122]~P3(x1221,a37)+~E(f2(x1221),a3) % 0.70/0.79 [123]~P3(x1231,a37)+~E(f2(x1231),x1231) % 0.70/0.79 [125]~P3(x1251,a37)+P5(f4(x1251)) % 0.70/0.79 [135]~P3(x1351,a37)+P3(f2(x1351),a37) % 0.70/0.79 [136]~P3(x1361,a37)+P9(x1361,f2(x1361)) % 0.70/0.79 [137]~P3(x1371,a37)+P8(x1371,f2(x1371)) % 0.70/0.79 [146]~P3(x1461,a37)+P6(f5(a41,x1461)) % 0.70/0.79 [147]~P3(x1471,a37)+~P9(f2(x1471),a3) % 0.70/0.79 [155]~P3(x1551,a37)+P7(f5(a41,x1551),a37) % 0.70/0.79 [126]~P3(x1261,a37)+E(f7(f4(x1261)),x1261) % 0.70/0.79 [121]~P3(x1212,x1211)+~E(x1211,a33) % 0.70/0.79 [127]E(a46,a45)+P9(f2(a45),a46)+P9(f2(a46),a45) % 0.70/0.79 [116]~P1(x1161)+~P6(x1161)+~E(x1161,a33) % 0.70/0.79 [119]~P5(x1191)+~P6(x1191)+~P1(x1191) % 0.70/0.79 [114]~P1(x1141)+~E(x1141,a33)+E(f7(x1141),a3) % 0.70/0.79 [115]~P1(x1151)+E(x1151,a33)+~E(f7(x1151),a3) % 0.70/0.79 [124]~P1(x1241)+P3(f8(x1241),x1241)+E(x1241,a33) % 0.70/0.79 [131]~P1(x1311)+~P5(x1311)+P3(f7(x1311),a37) % 0.70/0.79 [138]~P3(x1381,a37)+E(x1381,a3)+P3(f19(x1381),a37) % 0.70/0.79 [139]~P1(x1391)+P5(x1391)+~P3(f7(x1391),a37) % 0.70/0.79 [145]~P5(x1451)+~P7(x1451,a37)+P3(f9(x1451),a37) % 0.70/0.79 [129]~P3(x1291,a37)+E(x1291,a3)+E(f2(f19(x1291)),x1291) % 0.70/0.79 [157]~P5(x1571)+~P7(x1571,a37)+P7(x1571,f4(f9(x1571))) % 0.70/0.79 [132]~P7(x1321,x1322)+P1(x1321)+~P1(x1322) % 0.70/0.79 [133]~P3(x1331,x1332)+P4(x1331)+~P1(x1332) % 0.70/0.79 [130]P1(x1301)+~P3(x1302,a37)+~E(x1301,f4(x1302)) % 0.70/0.79 [158]~P4(x1582)+~P2(x1581)+P7(f29(x1581,x1582),f35(x1581)) % 0.70/0.79 [174]~P2(x1741)+~P3(x1742,f35(x1741))+P4(f5(x1741,x1742)) % 0.70/0.79 [176]~P1(x1761)+~P3(x1762,x1761)+E(f31(f32(x1761,x1762),x1762),x1761) % 0.70/0.79 [212]~P2(x2121)+~P3(x2122,f35(x2121))+P3(f5(x2121,x2122),f6(x2121,f35(x2121))) % 0.70/0.79 [202]~P2(x2021)+~P6(f35(x2021))+P4(f36(x2021))+~P5(f6(x2021,f35(x2021))) % 0.70/0.79 [220]~P2(x2201)+~P6(f35(x2201))+~P5(f6(x2201,f35(x2201)))+P6(f29(x2201,f36(x2201))) % 0.70/0.79 [224]~P3(x2241,a37)+~P7(f5(a41,x2241),a37)+~P6(f5(a41,x2241))+P6(f5(a41,f2(x2241))) % 0.70/0.79 [244]~P3(x2441,a37)+~P7(f5(a41,x2441),a37)+~P6(f5(a41,x2441))+P7(f5(a41,f2(x2441)),f32(f5(a41,x2441),f38(f5(a41,x2441)))) % 0.70/0.79 [140]~P5(x1402)+~P7(x1401,x1402)+P5(x1401)+~P1(x1402) % 0.70/0.79 [144]P3(x1442,x1441)+~E(x1442,f38(x1441))+~P7(x1441,a37)+E(x1441,a33) % 0.70/0.79 [149]~P1(x1491)+~P4(x1492)+~P5(x1491)+P5(f31(x1491,x1492)) % 0.70/0.79 [150]~P1(x1501)+~P4(x1502)+~P5(x1501)+P5(f32(x1501,x1502)) % 0.70/0.79 [151]~P1(x1511)+~P4(x1512)+~P6(x1511)+P6(f31(x1511,x1512)) % 0.70/0.79 [152]~P1(x1521)+~P4(x1522)+~P6(x1521)+P6(f32(x1521,x1522)) % 0.70/0.79 [153]~P1(x1531)+P5(x1531)+~P3(x1532,a37)+~E(f34(x1531,x1532),a33) % 0.70/0.79 [156]E(x1561,x1562)+~E(f2(x1561),f2(x1562))+~P3(x1562,a37)+~P3(x1561,a37) % 0.70/0.79 [161]~P1(x1612)+~P5(x1612)+~P7(x1611,x1612)+P9(f7(x1611),f7(x1612)) % 0.70/0.79 [164]~P1(x1641)+~P5(x1641)+~P3(x1642,a37)+P5(f34(x1641,x1642)) % 0.70/0.79 [173]~P1(x1731)+~P1(x1732)+P7(x1731,x1732)+P3(f20(x1732,x1731),x1731) % 0.70/0.79 [180]P9(x1801,x1802)+P9(f2(x1802),x1801)+~P3(x1802,a37)+~P3(x1801,a37) % 0.70/0.79 [192]~P9(x1921,x1922)+~P3(x1922,a37)+~P3(x1921,a37)+P7(f4(x1921),f4(x1922)) % 0.70/0.79 [193]~P9(x1931,x1932)+~P3(x1932,a37)+~P3(x1931,a37)+P9(f2(x1931),f2(x1932)) % 0.70/0.79 [195]~P1(x1951)+~P1(x1952)+P7(x1951,x1952)+~P3(f20(x1952,x1951),x1952) % 0.70/0.79 [197]P9(x1971,x1972)+~P3(x1972,a37)+~P3(x1971,a37)+~P7(f4(x1971),f4(x1972)) % 0.70/0.79 [198]P9(x1981,x1982)+~P3(x1982,a37)+~P3(x1981,a37)+~P9(f2(x1981),f2(x1982)) % 0.70/0.79 [216]~P9(x2162,x2161)+~P3(x2162,a37)+~P3(x2161,a37)+P7(f5(a41,x2161),f5(a41,x2162)) % 0.70/0.79 [175]P3(x1752,x1751)+~P1(x1751)+~P4(x1752)+E(f32(f31(x1751,x1752),x1752),x1751) % 0.70/0.79 [183]~E(x1831,x1832)+~P3(x1832,a37)+~P3(x1831,a37)+P3(x1831,f4(f2(x1832))) % 0.70/0.79 [204]~P3(x2042,a37)+~P3(x2041,a37)+~P3(x2041,f4(x2042))+P3(x2041,f4(f2(x2042))) % 0.70/0.79 [223]~P3(x2232,a37)+~P3(x2231,a37)+~P9(f2(x2232),x2231)+~E(f38(f5(a41,x2231)),f38(f5(a41,x2232))) % 0.70/0.79 [203]~P1(x2031)+~P5(x2031)+~P3(x2032,x2031)+E(f2(f7(f32(x2031,x2032))),f7(x2031)) % 0.70/0.79 [237]~P3(x2372,a37)+~P3(x2371,a37)+~P9(f2(x2372),x2371)+P7(f5(a41,x2371),f32(f5(a41,x2372),f38(f5(a41,x2372)))) % 0.70/0.79 [168]~P1(x1682)+~P7(x1683,x1682)+P3(x1681,x1682)+~P3(x1681,x1683) % 0.70/0.79 [141]~P1(x1412)+~P4(x1413)+P1(x1411)+~E(x1411,f31(x1412,x1413)) % 0.70/0.79 [142]~P1(x1422)+~P4(x1423)+P1(x1421)+~E(x1421,f32(x1422,x1423)) % 0.70/0.79 [143]~P4(x1433)+~P2(x1432)+P1(x1431)+~E(x1431,f29(x1432,x1433)) % 0.70/0.79 [154]~P1(x1542)+P1(x1541)+~P3(x1543,a37)+~E(x1541,f34(x1542,x1543)) % 0.70/0.79 [162]~P3(x1621,x1622)+~P3(x1623,a37)+P3(x1621,a37)+~E(x1622,f4(x1623)) % 0.70/0.79 [170]~P2(x1702)+P1(x1701)+~P7(x1703,f35(x1702))+~E(x1701,f6(x1702,x1703)) % 0.70/0.79 [171]~P2(x1712)+P2(x1711)+~P7(x1713,f35(x1712))+~E(x1711,f30(x1712,x1713)) % 0.70/0.79 [172]~P2(x1723)+~P7(x1722,f35(x1723))+E(f35(x1721),x1722)+~E(x1721,f30(x1723,x1722)) % 0.70/0.79 [177]~P3(x1771,x1773)+~P3(x1772,a37)+P9(f2(x1771),x1772)+~E(x1773,f4(x1772)) % 0.70/0.79 [159]~P1(x1592)+~P1(x1591)+~P7(x1592,x1591)+~P7(x1591,x1592)+E(x1591,x1592) % 0.70/0.79 [190]~P9(x1902,x1901)+~P9(x1901,x1902)+E(x1901,x1902)+~P3(x1902,a37)+~P3(x1901,a37) % 0.70/0.79 [148]~P5(x1481)+P3(x1482,x1481)+~E(x1482,f39(x1481))+~P7(x1481,a37)+E(x1481,a33) % 0.70/0.79 [167]~P1(x1672)+~P6(x1672)+~P3(x1671,a37)+E(x1671,a3)+P6(f34(x1672,x1671)) % 0.70/0.79 [194]~P3(x1942,x1941)+P3(f25(x1941,x1942),x1941)+~P7(x1941,a37)+E(x1941,a33)+E(x1942,f38(x1941)) % 0.70/0.79 [205]~P1(x2051)+~P5(x2051)+~P3(x2052,a37)+~P9(x2052,f7(x2051))+P7(f26(x2051,x2052),x2051) % 0.70/0.79 [207]~P1(x2071)+P3(f28(x2072,x2071),x2071)+~P3(x2072,a37)+E(x2071,f4(x2072))+P3(f28(x2072,x2071),a37) % 0.70/0.79 [208]~P3(x2082,x2081)+~P7(x2081,a37)+~P9(x2082,f25(x2081,x2082))+E(x2081,a33)+E(x2082,f38(x2081)) % 0.70/0.79 [215]~P6(x2152)+~P2(x2151)+~E(f10(x2151,x2152),f11(x2151,x2152))+~P7(x2152,f35(x2151))+P6(f6(x2151,x2152)) % 0.70/0.79 [217]~P6(x2172)+~P2(x2171)+P3(f11(x2171,x2172),f35(x2171))+~P7(x2172,f35(x2171))+P6(f6(x2171,x2172)) % 0.70/0.79 [218]~P6(x2182)+~P2(x2181)+P3(f10(x2181,x2182),f35(x2181))+~P7(x2182,f35(x2181))+P6(f6(x2181,x2182)) % 0.70/0.79 [182]P3(x1822,x1821)+~P1(x1821)+~P4(x1822)+~P5(x1821)+E(f7(f31(x1821,x1822)),f2(f7(x1821))) % 0.70/0.79 [201]~P1(x2011)+~P5(x2011)+~P3(x2012,a37)+~P9(x2012,f7(x2011))+E(f7(f26(x2011,x2012)),x2012) % 0.70/0.79 [210]E(x2101,x2102)+P3(x2101,f4(x2102))+~P3(x2102,a37)+~P3(x2101,a37)+~P3(x2101,f4(f2(x2102))) % 0.70/0.79 [221]~P1(x2211)+P3(f28(x2212,x2211),x2211)+~P3(x2212,a37)+E(x2211,f4(x2212))+P9(f2(f28(x2212,x2211)),x2212) % 0.70/0.79 [222]~P6(x2222)+~P2(x2221)+~P7(x2222,f35(x2221))+P6(f6(x2221,x2222))+E(f5(x2221,f10(x2221,x2222)),f5(x2221,f11(x2221,x2222))) % 0.70/0.79 [169]~P3(x1693,x1691)+P9(x1692,x1693)+~E(x1692,f38(x1691))+~P7(x1691,a37)+E(x1691,a33) % 0.70/0.79 [196]P3(x1961,x1962)+~P3(x1963,a37)+~P3(x1961,a37)+~P9(f2(x1961),x1963)+~E(x1962,f4(x1963)) % 0.70/0.79 [227]~P1(x2271)+~P5(x2273)+~P3(x2272,a37)+~P7(x2273,f34(x2271,x2272))+P5(f13(x2271,x2272,x2273)) % 0.70/0.79 [228]~P1(x2281)+~P5(x2283)+~P3(x2282,a37)+~P7(x2283,f34(x2281,x2282))+P7(f13(x2281,x2282,x2283),x2281) % 0.70/0.79 [245]~P1(x2452)+~P5(x2451)+~P3(x2453,a37)+~P7(x2451,f34(x2452,x2453))+P7(x2451,f34(f13(x2452,x2453,x2451),x2453)) % 0.70/0.79 [163]~P1(x1634)+~P4(x1632)+~P3(x1631,x1633)+~E(x1631,x1632)+~E(x1633,f32(x1634,x1632)) % 0.70/0.79 [165]~P1(x1653)+~P4(x1654)+~P3(x1651,x1652)+P4(x1651)+~E(x1652,f31(x1653,x1654)) % 0.70/0.79 [166]~P1(x1663)+~P4(x1664)+~P3(x1661,x1662)+P4(x1661)+~E(x1662,f32(x1663,x1664)) % 0.70/0.79 [179]~P1(x1792)+~P4(x1794)+~P3(x1791,x1793)+P3(x1791,x1792)+~E(x1793,f32(x1792,x1794)) % 0.70/0.79 [181]~P4(x1813)+~P2(x1811)+~P3(x1812,x1814)+E(f5(x1811,x1812),x1813)+~E(x1814,f29(x1811,x1813)) % 0.70/0.79 [185]~P1(x1854)+~P3(x1851,x1853)+~P3(x1852,a37)+E(f7(x1851),x1852)+~E(x1853,f34(x1854,x1852)) % 0.70/0.79 [187]~P4(x1874)+~P2(x1872)+~P3(x1871,x1873)+P3(x1871,f35(x1872))+~E(x1873,f29(x1872,x1874)) % 0.70/0.79 [191]~P1(x1912)+~P3(x1911,x1913)+P7(x1911,x1912)+~P3(x1914,a37)+~E(x1913,f34(x1912,x1914)) % 0.70/0.79 [209]~P2(x2093)+~P3(x2092,x2094)+~P7(x2094,f35(x2093))+E(f5(x2091,x2092),f5(x2093,x2092))+~E(x2091,f30(x2093,x2094)) % 0.70/0.79 [251]~P2(x2511)+~P3(x2514,x2513)+~E(x2513,f6(x2511,x2512))+~P7(x2512,f35(x2511))+P3(f17(x2511,x2512,x2513,x2514),x2512) % 0.70/0.79 [252]~P2(x2521)+~P3(x2524,x2523)+~E(x2523,f6(x2521,x2522))+~P7(x2522,f35(x2521))+E(f5(x2521,f17(x2521,x2522,x2523,x2524)),x2524) % 0.70/0.79 [200]~P5(x2001)+~P3(x2002,x2001)+P3(f27(x2001,x2002),x2001)+~P7(x2001,a37)+E(x2001,a33)+E(x2002,f39(x2001)) % 0.70/0.79 [213]~P5(x2131)+~P3(x2132,x2131)+~P7(x2131,a37)+~P9(f27(x2131,x2132),x2132)+E(x2131,a33)+E(x2132,f39(x2131)) % 0.70/0.79 [232]~P1(x2321)+~P3(x2322,a37)+~P3(f28(x2322,x2321),x2321)+E(x2321,f4(x2322))+~P3(f28(x2322,x2321),a37)+~P9(f2(f28(x2322,x2321)),x2322) % 0.70/0.79 [186]~P1(x1862)+~P1(x1861)+~P7(x1863,x1862)+~P7(x1861,x1863)+P7(x1861,x1862)+~P1(x1863) % 0.70/0.79 [214]~P9(x2141,x2143)+P9(x2141,x2142)+~P9(x2143,x2142)+~P3(x2142,a37)+~P3(x2143,a37)+~P3(x2141,a37) % 0.70/0.79 [178]~P5(x1781)+~P3(x1782,x1781)+P9(x1782,x1783)+~E(x1783,f39(x1781))+~P7(x1781,a37)+E(x1781,a33) % 0.70/0.79 [226]~P2(x2261)+~P2(x2262)+P3(f12(x2262,x2263,x2261),x2263)+~E(f35(x2261),x2263)+~P7(x2263,f35(x2262))+E(x2261,f30(x2262,x2263)) % 0.70/0.79 [229]~P1(x2291)+~P1(x2292)+~P4(x2293)+P3(f23(x2292,x2293,x2291),x2291)+~E(f23(x2292,x2293,x2291),x2293)+E(x2291,f32(x2292,x2293)) % 0.70/0.79 [230]~P1(x2301)+~P1(x2302)+~P4(x2303)+P3(f24(x2302,x2303,x2301),x2301)+E(x2301,f31(x2302,x2303))+P4(f24(x2302,x2303,x2301)) % 0.70/0.79 [231]~P1(x2311)+~P1(x2312)+~P4(x2313)+P3(f23(x2312,x2313,x2311),x2311)+E(x2311,f32(x2312,x2313))+P4(f23(x2312,x2313,x2311)) % 0.70/0.79 [233]~P1(x2331)+~P1(x2332)+~P4(x2333)+P3(f23(x2332,x2333,x2331),x2331)+P3(f23(x2332,x2333,x2331),x2332)+E(x2331,f32(x2332,x2333)) % 0.70/0.79 [236]~P1(x2361)+~P4(x2363)+~P2(x2362)+P3(f15(x2362,x2363,x2361),x2361)+P3(f15(x2362,x2363,x2361),f35(x2362))+E(x2361,f29(x2362,x2363)) % 0.70/0.79 [238]~P1(x2381)+~P1(x2382)+P3(f14(x2382,x2383,x2381),x2381)+P7(f14(x2382,x2383,x2381),x2382)+~P3(x2383,a37)+E(x2381,f34(x2382,x2383)) % 0.70/0.79 [241]~P1(x2411)+~P2(x2412)+P3(f16(x2412,x2413,x2411),x2411)+P3(f18(x2412,x2413,x2411),x2413)+~P7(x2413,f35(x2412))+E(x2411,f6(x2412,x2413)) % 0.70/0.79 [234]~P1(x2341)+~P4(x2343)+~P2(x2342)+P3(f15(x2342,x2343,x2341),x2341)+E(x2341,f29(x2342,x2343))+E(f5(x2342,f15(x2342,x2343,x2341)),x2343) % 0.70/0.79 [235]~P1(x2351)+~P1(x2352)+P3(f14(x2352,x2353,x2351),x2351)+~P3(x2353,a37)+E(x2351,f34(x2352,x2353))+E(f7(f14(x2352,x2353,x2351)),x2353) % 0.70/0.79 [246]~P1(x2461)+~P2(x2462)+P3(f16(x2462,x2463,x2461),x2461)+~P7(x2463,f35(x2462))+E(x2461,f6(x2462,x2463))+E(f5(x2462,f18(x2462,x2463,x2461)),f16(x2462,x2463,x2461)) % 0.70/0.79 [248]~P2(x2482)+~P2(x2481)+~E(f35(x2481),x2483)+~P7(x2483,f35(x2482))+E(x2481,f30(x2482,x2483))+~E(f5(x2481,f12(x2482,x2483,x2481)),f5(x2482,f12(x2482,x2483,x2481))) % 0.70/0.79 [160]~P1(x1604)+~P4(x1603)+~P4(x1601)+P3(x1601,x1602)+~E(x1601,x1603)+~E(x1602,f31(x1604,x1603)) % 0.70/0.79 [184]~P1(x1843)+~P4(x1842)+~P3(x1841,x1844)+E(x1841,x1842)+P3(x1841,x1843)+~E(x1844,f31(x1843,x1842)) % 0.70/0.79 [188]~P1(x1883)+~P4(x1884)+~P4(x1881)+~P3(x1881,x1883)+P3(x1881,x1882)+~E(x1882,f31(x1883,x1884)) % 0.70/0.79 [199]~P1(x1994)+~P7(x1991,x1994)+P3(x1991,x1992)+~P3(x1993,a37)+~E(x1992,f34(x1994,x1993))+~E(f7(x1991),x1993) % 0.70/0.79 [206]~P4(x2064)+~P2(x2063)+P3(x2061,x2062)+~E(f5(x2063,x2061),x2064)+~P3(x2061,f35(x2063))+~E(x2062,f29(x2063,x2064)) % 0.70/0.79 [219]~P2(x2193)+~P3(x2195,x2194)+P3(x2191,x2192)+~P7(x2194,f35(x2193))+~E(x2192,f6(x2193,x2194))+~E(f5(x2193,x2195),x2191) % 0.70/0.79 [211]E(f38(x2112),f38(x2111))+~P7(x2111,a37)+~P7(x2112,a37)+~P3(f38(x2111),x2112)+~P3(f38(x2112),x2111)+E(x2111,a33)+E(x2112,a33) % 0.70/0.79 [225]~P1(x2253)+~P1(x2252)+P7(x2252,x2253)+~P3(x2251,a37)+~P7(f34(x2252,x2251),f34(x2253,x2251))+E(x2251,a3)+E(f34(x2252,x2251),a33) % 0.70/0.79 [243]~P1(x2431)+~P1(x2432)+~P4(x2433)+E(f24(x2432,x2433,x2431),x2433)+P3(f24(x2432,x2433,x2431),x2431)+P3(f24(x2432,x2433,x2431),x2432)+E(x2431,f31(x2432,x2433)) % 0.70/0.79 [249]~P1(x2491)+~P1(x2492)+~P4(x2493)+~E(f24(x2492,x2493,x2491),x2493)+~P3(f24(x2492,x2493,x2491),x2491)+E(x2491,f31(x2492,x2493))+~P4(f24(x2492,x2493,x2491)) % 0.70/0.79 [250]~P1(x2501)+~P1(x2502)+~P4(x2503)+~P3(f24(x2502,x2503,x2501),x2501)+~P3(f24(x2502,x2503,x2501),x2502)+E(x2501,f31(x2502,x2503))+~P4(f24(x2502,x2503,x2501)) % 0.70/0.79 [253]~P1(x2531)+~P1(x2532)+~P3(x2533,a37)+~P3(f14(x2532,x2533,x2531),x2531)+~P7(f14(x2532,x2533,x2531),x2532)+E(x2531,f34(x2532,x2533))+~E(f7(f14(x2532,x2533,x2531)),x2533) % 0.70/0.79 [254]~P1(x2541)+~P4(x2543)+~P2(x2542)+~P3(f15(x2542,x2543,x2541),x2541)+~P3(f15(x2542,x2543,x2541),f35(x2542))+E(x2541,f29(x2542,x2543))+~E(f5(x2542,f15(x2542,x2543,x2541)),x2543) % 0.70/0.79 [189]~P1(x1894)+~P4(x1892)+~P4(x1891)+~P3(x1891,x1894)+E(x1891,x1892)+P3(x1891,x1893)+~E(x1893,f32(x1894,x1892)) % 0.70/0.79 [247]~P1(x2471)+~P2(x2472)+~P3(x2474,x2473)+~P7(x2473,f35(x2472))+~P3(f16(x2472,x2473,x2471),x2471)+~E(f5(x2472,x2474),f16(x2472,x2473,x2471))+E(x2471,f6(x2472,x2473)) % 0.70/0.79 [255]~P1(x2551)+~P1(x2552)+~P4(x2553)+E(f23(x2552,x2553,x2551),x2553)+~P3(f23(x2552,x2553,x2551),x2551)+~P3(f23(x2552,x2553,x2551),x2552)+E(x2551,f32(x2552,x2553))+~P4(f23(x2552,x2553,x2551)) % 0.70/0.79 [239]~P6(x2392)+~P2(x2393)+~E(f35(x2393),f34(x2392,x2391))+~P3(x2391,a37)+~P7(x2392,a37)+~P8(x2391,a40)+P6(f21(x2391,x2392,x2393))+~P7(f6(x2393,f35(x2393)),a42) % 0.70/0.79 [240]~P6(x2402)+~P2(x2403)+~E(f35(x2403),f34(x2402,x2401))+~P3(x2401,a37)+~P7(x2402,a37)+~P8(x2401,a40)+P3(f22(x2401,x2402,x2403),a42)+~P7(f6(x2403,f35(x2403)),a42) % 0.70/0.79 [242]~P6(x2422)+~P2(x2423)+~E(f35(x2423),f34(x2422,x2421))+~P3(x2421,a37)+~P7(x2422,a37)+~P8(x2421,a40)+P7(f21(x2421,x2422,x2423),x2422)+~P7(f6(x2423,f35(x2423)),a42) % 0.70/0.79 [256]~P6(x2564)+~P2(x2561)+~E(f35(x2561),f34(x2564,x2563))+~P3(x2563,a37)+~P7(x2564,a37)+~P8(x2563,a40)+E(f5(x2561,x2562),f22(x2563,x2564,x2561))+~P3(x2562,f34(f21(x2563,x2564,x2561),x2563))+~P7(f6(x2561,f35(x2561)),a42) % 0.70/0.79 %EqnAxiom % 0.70/0.79 [1]E(x11,x11) % 0.70/0.79 [2]E(x22,x21)+~E(x21,x22) % 0.70/0.79 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.70/0.79 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.70/0.79 [5]~E(x51,x52)+E(f4(x51),f4(x52)) % 0.70/0.79 [6]~E(x61,x62)+E(f35(x61),f35(x62)) % 0.70/0.79 [7]~E(x71,x72)+E(f5(x71,x73),f5(x72,x73)) % 0.70/0.79 [8]~E(x81,x82)+E(f5(x83,x81),f5(x83,x82)) % 0.70/0.79 [9]~E(x91,x92)+E(f34(x91,x93),f34(x92,x93)) % 0.70/0.79 [10]~E(x101,x102)+E(f34(x103,x101),f34(x103,x102)) % 0.70/0.79 [11]~E(x111,x112)+E(f16(x111,x113,x114),f16(x112,x113,x114)) % 0.70/0.79 [12]~E(x121,x122)+E(f16(x123,x121,x124),f16(x123,x122,x124)) % 0.70/0.79 [13]~E(x131,x132)+E(f16(x133,x134,x131),f16(x133,x134,x132)) % 0.70/0.79 [14]~E(x141,x142)+E(f14(x141,x143,x144),f14(x142,x143,x144)) % 0.70/0.79 [15]~E(x151,x152)+E(f14(x153,x151,x154),f14(x153,x152,x154)) % 0.70/0.79 [16]~E(x161,x162)+E(f14(x163,x164,x161),f14(x163,x164,x162)) % 0.70/0.79 [17]~E(x171,x172)+E(f6(x171,x173),f6(x172,x173)) % 0.70/0.79 [18]~E(x181,x182)+E(f6(x183,x181),f6(x183,x182)) % 0.70/0.79 [19]~E(x191,x192)+E(f32(x191,x193),f32(x192,x193)) % 0.70/0.79 [20]~E(x201,x202)+E(f32(x203,x201),f32(x203,x202)) % 0.70/0.79 [21]~E(x211,x212)+E(f38(x211),f38(x212)) % 0.70/0.79 [22]~E(x221,x222)+E(f17(x221,x223,x224,x225),f17(x222,x223,x224,x225)) % 0.70/0.79 [23]~E(x231,x232)+E(f17(x233,x231,x234,x235),f17(x233,x232,x234,x235)) % 0.70/0.79 [24]~E(x241,x242)+E(f17(x243,x244,x241,x245),f17(x243,x244,x242,x245)) % 0.70/0.79 [25]~E(x251,x252)+E(f17(x253,x254,x255,x251),f17(x253,x254,x255,x252)) % 0.70/0.79 [26]~E(x261,x262)+E(f24(x261,x263,x264),f24(x262,x263,x264)) % 0.70/0.79 [27]~E(x271,x272)+E(f24(x273,x271,x274),f24(x273,x272,x274)) % 0.70/0.79 [28]~E(x281,x282)+E(f24(x283,x284,x281),f24(x283,x284,x282)) % 0.70/0.79 [29]~E(x291,x292)+E(f7(x291),f7(x292)) % 0.70/0.79 [30]~E(x301,x302)+E(f29(x301,x303),f29(x302,x303)) % 0.70/0.79 [31]~E(x311,x312)+E(f29(x313,x311),f29(x313,x312)) % 0.70/0.79 [32]~E(x321,x322)+E(f28(x321,x323),f28(x322,x323)) % 0.70/0.79 [33]~E(x331,x332)+E(f28(x333,x331),f28(x333,x332)) % 0.70/0.79 [34]~E(x341,x342)+E(f36(x341),f36(x342)) % 0.70/0.79 [35]~E(x351,x352)+E(f13(x351,x353,x354),f13(x352,x353,x354)) % 0.70/0.79 [36]~E(x361,x362)+E(f13(x363,x361,x364),f13(x363,x362,x364)) % 0.70/0.79 [37]~E(x371,x372)+E(f13(x373,x374,x371),f13(x373,x374,x372)) % 0.70/0.79 [38]~E(x381,x382)+E(f21(x381,x383,x384),f21(x382,x383,x384)) % 0.70/0.79 [39]~E(x391,x392)+E(f21(x393,x391,x394),f21(x393,x392,x394)) % 0.70/0.79 [40]~E(x401,x402)+E(f21(x403,x404,x401),f21(x403,x404,x402)) % 0.70/0.79 [41]~E(x411,x412)+E(f8(x411),f8(x412)) % 0.70/0.79 [42]~E(x421,x422)+E(f23(x421,x423,x424),f23(x422,x423,x424)) % 0.70/0.79 [43]~E(x431,x432)+E(f23(x433,x431,x434),f23(x433,x432,x434)) % 0.70/0.79 [44]~E(x441,x442)+E(f23(x443,x444,x441),f23(x443,x444,x442)) % 0.70/0.79 [45]~E(x451,x452)+E(f26(x451,x453),f26(x452,x453)) % 0.70/0.79 [46]~E(x461,x462)+E(f26(x463,x461),f26(x463,x462)) % 0.70/0.79 [47]~E(x471,x472)+E(f27(x471,x473),f27(x472,x473)) % 0.70/0.79 [48]~E(x481,x482)+E(f27(x483,x481),f27(x483,x482)) % 0.70/0.79 [49]~E(x491,x492)+E(f11(x491,x493),f11(x492,x493)) % 0.70/0.79 [50]~E(x501,x502)+E(f11(x503,x501),f11(x503,x502)) % 0.70/0.79 [51]~E(x511,x512)+E(f15(x511,x513,x514),f15(x512,x513,x514)) % 0.70/0.79 [52]~E(x521,x522)+E(f15(x523,x521,x524),f15(x523,x522,x524)) % 0.70/0.79 [53]~E(x531,x532)+E(f15(x533,x534,x531),f15(x533,x534,x532)) % 0.70/0.79 [54]~E(x541,x542)+E(f19(x541),f19(x542)) % 0.70/0.79 [55]~E(x551,x552)+E(f31(x551,x553),f31(x552,x553)) % 0.70/0.79 [56]~E(x561,x562)+E(f31(x563,x561),f31(x563,x562)) % 0.70/0.79 [57]~E(x571,x572)+E(f30(x571,x573),f30(x572,x573)) % 0.70/0.79 [58]~E(x581,x582)+E(f30(x583,x581),f30(x583,x582)) % 0.70/0.79 [59]~E(x591,x592)+E(f39(x591),f39(x592)) % 0.70/0.79 [60]~E(x601,x602)+E(f22(x601,x603,x604),f22(x602,x603,x604)) % 0.70/0.79 [61]~E(x611,x612)+E(f22(x613,x611,x614),f22(x613,x612,x614)) % 0.70/0.79 [62]~E(x621,x622)+E(f22(x623,x624,x621),f22(x623,x624,x622)) % 0.70/0.79 [63]~E(x631,x632)+E(f20(x631,x633),f20(x632,x633)) % 0.70/0.79 [64]~E(x641,x642)+E(f20(x643,x641),f20(x643,x642)) % 0.70/0.79 [65]~E(x651,x652)+E(f10(x651,x653),f10(x652,x653)) % 0.70/0.79 [66]~E(x661,x662)+E(f10(x663,x661),f10(x663,x662)) % 0.70/0.79 [67]~E(x671,x672)+E(f12(x671,x673,x674),f12(x672,x673,x674)) % 0.70/0.79 [68]~E(x681,x682)+E(f12(x683,x681,x684),f12(x683,x682,x684)) % 0.70/0.79 [69]~E(x691,x692)+E(f12(x693,x694,x691),f12(x693,x694,x692)) % 0.70/0.79 [70]~E(x701,x702)+E(f9(x701),f9(x702)) % 0.70/0.79 [71]~E(x711,x712)+E(f25(x711,x713),f25(x712,x713)) % 0.70/0.79 [72]~E(x721,x722)+E(f25(x723,x721),f25(x723,x722)) % 0.70/0.79 [73]~E(x731,x732)+E(f18(x731,x733,x734),f18(x732,x733,x734)) % 0.70/0.79 [74]~E(x741,x742)+E(f18(x743,x741,x744),f18(x743,x742,x744)) % 0.70/0.79 [75]~E(x751,x752)+E(f18(x753,x754,x751),f18(x753,x754,x752)) % 0.70/0.79 [76]~P1(x761)+P1(x762)+~E(x761,x762) % 0.70/0.79 [77]P3(x772,x773)+~E(x771,x772)+~P3(x771,x773) % 0.70/0.79 [78]P3(x783,x782)+~E(x781,x782)+~P3(x783,x781) % 0.70/0.79 [79]~P5(x791)+P5(x792)+~E(x791,x792) % 0.70/0.79 [80]P9(x802,x803)+~E(x801,x802)+~P9(x801,x803) % 0.70/0.79 [81]P9(x813,x812)+~E(x811,x812)+~P9(x813,x811) % 0.70/0.79 [82]~P6(x821)+P6(x822)+~E(x821,x822) % 0.70/0.79 [83]~P2(x831)+P2(x832)+~E(x831,x832) % 0.70/0.79 [84]P7(x842,x843)+~E(x841,x842)+~P7(x841,x843) % 0.70/0.79 [85]P7(x853,x852)+~E(x851,x852)+~P7(x853,x851) % 0.70/0.79 [86]~P4(x861)+P4(x862)+~E(x861,x862) % 0.70/0.79 [87]P8(x872,x873)+~E(x871,x872)+~P8(x871,x873) % 0.70/0.79 [88]P8(x883,x882)+~E(x881,x882)+~P8(x883,x881) % 0.70/0.79 % 0.70/0.79 %------------------------------------------- % 0.70/0.79 cnf(257,plain, % 0.70/0.79 (P1(a33)), % 0.70/0.79 inference(equality_inference,[],[113])). % 0.70/0.79 cnf(258,plain, % 0.70/0.79 (~P1(a33)+E(f7(a33),a3)), % 0.70/0.79 inference(equality_inference,[],[114])). % 0.70/0.79 cnf(259,plain, % 0.70/0.79 (~P6(a33)+~P1(a33)), % 0.70/0.79 inference(equality_inference,[],[116])). % 0.70/0.79 cnf(260,plain, % 0.70/0.79 (~P3(x2601,a33)), % 0.70/0.79 inference(equality_inference,[],[121])). % 0.70/0.79 cnf(261,plain, % 0.70/0.79 (P1(f4(x2611))+~P3(x2611,a37)), % 0.70/0.79 inference(equality_inference,[],[130])). % 0.70/0.79 cnf(265,plain, % 0.70/0.79 (P3(f38(x2651),x2651)+~P7(x2651,a37)+E(x2651,a33)), % 0.70/0.79 inference(equality_inference,[],[144])). % 0.70/0.79 cnf(267,plain, % 0.70/0.79 (~P1(x2671)+P1(f34(x2671,x2672))+~P3(x2672,a37)), % 0.70/0.79 inference(equality_inference,[],[154])). % 0.70/0.79 cnf(276,plain, % 0.70/0.79 (~P3(x2761,f4(x2762))+P9(f2(x2761),x2762)+~P3(x2762,a37)), % 0.70/0.79 inference(equality_inference,[],[177])). % 0.70/0.79 cnf(280,plain, % 0.70/0.79 (~P3(x2801,a37)+~P3(x2801,a37)+P3(x2801,f4(f2(x2801)))), % 0.70/0.79 inference(equality_inference,[],[183])). % 0.70/0.79 cnf(286,plain, % 0.70/0.79 (P7(x2861,x2862)+~P1(x2862)+~P3(x2861,f34(x2862,x2863))+~P3(x2863,a37)), % 0.70/0.79 inference(equality_inference,[],[191])). % 0.70/0.79 cnf(289,plain, % 0.70/0.79 (~P9(f2(x2891),x2891)+~P3(x2891,a37)+~P3(x2891,a37)), % 0.70/0.79 inference(equality_inference,[],[223])). % 0.70/0.79 cnf(293,plain, % 0.70/0.79 (E(f7(a33),a3)), % 0.70/0.79 inference(scs_inference,[],[257,258])). % 0.70/0.79 cnf(294,plain, % 0.70/0.79 (~P6(a33)), % 0.70/0.79 inference(scs_inference,[],[257,259])). % 0.70/0.79 cnf(295,plain, % 0.70/0.79 (E(f38(f5(a41,a45)),f38(f5(a41,a46)))), % 0.70/0.79 inference(scs_inference,[],[109,2])). % 0.70/0.79 cnf(296,plain, % 0.70/0.79 (P1(f4(a3))), % 0.70/0.79 inference(scs_inference,[],[109,90,2,113])). % 0.70/0.79 cnf(298,plain, % 0.70/0.79 (~P3(x2981,f4(a3))), % 0.70/0.79 inference(scs_inference,[],[109,90,2,113,121])). % 0.70/0.79 cnf(306,plain, % 0.70/0.79 (P3(a3,f4(f2(a3)))), % 0.70/0.79 inference(scs_inference,[],[109,101,102,90,2,113,121,134,261,289,280])). % 0.70/0.79 cnf(310,plain, % 0.70/0.79 (~P3(x3101,a33)), % 0.70/0.79 inference(rename_variables,[],[260])). % 0.70/0.79 cnf(318,plain, % 0.70/0.79 (~P9(f2(a45),a46)), % 0.70/0.79 inference(scs_inference,[],[109,260,92,96,101,102,104,105,111,89,90,2,113,121,134,261,289,280,3,78,80,116,119,267,223])). % 0.70/0.79 cnf(320,plain, % 0.70/0.79 (P7(a33,a37)), % 0.70/0.79 inference(scs_inference,[],[109,260,310,92,96,101,102,104,105,111,257,89,90,2,113,121,134,261,289,280,3,78,80,116,119,267,223,173])). % 0.70/0.79 cnf(327,plain, % 0.70/0.79 (P7(f4(a3),f4(a3))), % 0.70/0.79 inference(scs_inference,[],[109,260,310,92,96,101,102,104,105,111,257,89,90,2,113,121,134,261,289,280,3,78,80,116,119,267,223,173,177,180,192])). % 0.70/0.79 cnf(337,plain, % 0.70/0.79 (~P5(f35(a41))), % 0.70/0.79 inference(scs_inference,[],[109,260,310,92,96,101,102,104,105,106,111,257,89,90,91,2,113,121,134,261,289,280,3,78,80,116,119,267,223,173,177,180,192,193,159,265,276,79])). % 0.70/0.79 cnf(338,plain, % 0.70/0.79 (~E(f2(a3),a3)), % 0.70/0.79 inference(scs_inference,[],[109,260,310,92,96,101,102,104,105,106,111,257,89,90,91,2,113,121,134,261,289,280,3,78,80,116,119,267,223,173,177,180,192,193,159,265,276,79,81])). % 0.70/0.79 cnf(339,plain, % 0.70/0.79 (P3(f38(a43),a43)+P6(a33)), % 0.70/0.79 inference(scs_inference,[],[109,260,310,92,96,97,101,102,104,105,106,111,257,89,90,91,2,113,121,134,261,289,280,3,78,80,116,119,267,223,173,177,180,192,193,159,265,276,79,81,82])). % 0.70/0.79 cnf(349,plain, % 0.70/0.79 (P9(f2(a46),a45)), % 0.70/0.79 inference(scs_inference,[],[318,112,127])). % 0.70/0.79 cnf(368,plain, % 0.70/0.79 (~P3(x3681,f4(a3))), % 0.70/0.79 inference(rename_variables,[],[298])). % 0.70/0.79 cnf(382,plain, % 0.70/0.79 (~P9(f2(a46),a45)), % 0.70/0.79 inference(scs_inference,[],[318,295,337,306,338,101,90,298,368,320,296,327,293,94,103,294,104,105,339,134,261,2,267,289,280,85,276,84,80,78,79,3,140,168,286,177,193,223])). % 0.70/0.79 cnf(403,plain, % 0.70/0.79 ($false), % 0.70/0.79 inference(scs_inference,[],[382,349]), % 0.70/0.79 ['proof']). % 0.70/0.79 % SZS output end Proof % 0.70/0.79 % Total time :0.080000s %------------------------------------------------------------------------------