%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM568+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 : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 12:25:05 EDT 2024 % Result : Theorem 61.23s 61.36s % Output : CNFRefutation 61.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : NUM568+1 : TPTP v8.2.0. Released v4.0.0. % 0.08/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n018.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 : Sat Jun 22 22:47:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.45/0.59 start to proof:theBenchmark % 61.23/61.33 %------------------------------------------- % 61.23/61.33 % File :CSE---1.7 % 61.23/61.33 % Problem :theBenchmark % 61.23/61.33 % Transform :cnf % 61.23/61.33 % Format :tptp:raw % 61.23/61.33 % Command :java -jar mcs_scs.jar %d %s % 61.23/61.33 % 61.23/61.33 % Result :Theorem 60.580000s % 61.23/61.33 % Output :CNFRefutation 60.580000s % 61.23/61.33 %------------------------------------------- % 61.23/61.34 %------------------------------------------------------------------------------ % 61.23/61.34 % File : NUM568+1 : TPTP v8.2.0. Released v4.0.0. % 61.23/61.34 % Domain : Number Theory % 61.23/61.34 % Problem : Ramsey's Infinite Theorem 15_02_01, 00 expansion % 61.23/61.34 % Version : Especial. % 61.23/61.34 % English : % 61.23/61.34 % 61.23/61.34 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 61.23/61.34 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 61.23/61.34 % Source : [Pas08] % 61.23/61.34 % Names : ramsey_15_02_01.00 [Pas08] % 61.23/61.34 % 61.23/61.34 % Status : Theorem % 61.23/61.34 % Rating : 0.19 v8.2.0, 0.22 v8.1.0, 0.14 v7.5.0, 0.12 v7.4.0, 0.13 v7.3.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.13 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.12 v6.1.0, 0.17 v6.0.0, 0.09 v5.5.0, 0.26 v5.4.0, 0.32 v5.3.0, 0.33 v5.2.0, 0.30 v5.1.0, 0.43 v5.0.0, 0.50 v4.1.0, 0.57 v4.0.1, 0.83 v4.0.0 % 61.23/61.34 % Syntax : Number of formulae : 80 ( 6 unt; 11 def) % 61.23/61.34 % Number of atoms : 313 ( 53 equ) % 61.23/61.34 % Maximal formula atoms : 12 ( 3 avg) % 61.23/61.34 % Number of connectives : 255 ( 22 ~; 4 |; 94 &) % 61.23/61.34 % ( 22 <=>; 113 =>; 0 <=; 0 <~>) % 61.23/61.34 % Maximal formula depth : 15 ( 5 avg) % 61.23/61.34 % Maximal term depth : 4 ( 1 avg) % 61.23/61.34 % Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty) % 61.23/61.34 % Number of functors : 21 ( 21 usr; 7 con; 0-2 aty) % 61.23/61.34 % Number of variables : 146 ( 137 !; 9 ?) % 61.23/61.34 % SPC : FOF_THM_RFO_SEQ % 61.23/61.34 % 61.23/61.34 % Comments : Problem generated by the SAD system [VLP07] % 61.23/61.34 %------------------------------------------------------------------------------ % 61.23/61.34 fof(mSetSort,axiom, % 61.23/61.34 ! [W0] : % 61.23/61.34 ( aSet0(W0) % 61.23/61.34 => $true ) ). % 61.23/61.34 % 61.23/61.34 fof(mElmSort,axiom, % 61.23/61.34 ! [W0] : % 61.23/61.34 ( aElement0(W0) % 61.23/61.34 => $true ) ). % 61.23/61.34 % 61.23/61.34 fof(mEOfElem,axiom, % 61.23/61.34 ! [W0] : % 61.23/61.34 ( aSet0(W0) % 61.23/61.34 => ! [W1] : % 61.23/61.34 ( aElementOf0(W1,W0) % 61.23/61.34 => aElement0(W1) ) ) ). % 61.23/61.34 % 61.23/61.34 fof(mFinRel,axiom, % 61.23/61.34 ! [W0] : % 61.23/61.34 ( aSet0(W0) % 61.23/61.34 => ( isFinite0(W0) % 61.23/61.34 => $true ) ) ). % 61.23/61.34 % 61.23/61.34 fof(mDefEmp,definition, % 61.23/61.34 ! [W0] : % 61.23/61.34 ( W0 = slcrc0 % 61.23/61.34 <=> ( aSet0(W0) % 61.23/61.34 & ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 61.23/61.34 % 61.23/61.34 fof(mEmpFin,axiom, % 61.23/61.34 isFinite0(slcrc0) ). % 61.23/61.34 % 61.23/61.34 fof(mCntRel,axiom, % 61.23/61.34 ! [W0] : % 61.23/61.34 ( aSet0(W0) % 61.23/61.34 => ( isCountable0(W0) % 61.23/61.34 => $true ) ) ). % 61.23/61.34 % 61.23/61.34 fof(mCountNFin,axiom, % 61.23/61.34 ! [W0] : % 61.23/61.34 ( ( aSet0(W0) % 61.23/61.34 & isCountable0(W0) ) % 61.23/61.34 => ~ isFinite0(W0) ) ). % 61.23/61.34 % 61.23/61.34 fof(mCountNFin_01,axiom, % 61.23/61.34 ! [W0] : % 61.23/61.34 ( ( aSet0(W0) % 61.23/61.34 & isCountable0(W0) ) % 61.23/61.34 => W0 != slcrc0 ) ). % 61.23/61.34 % 61.23/61.34 fof(mDefSub,definition, % 61.23/61.34 ! [W0] : % 61.23/61.34 ( aSet0(W0) % 61.23/61.34 => ! [W1] : % 61.23/61.34 ( aSubsetOf0(W1,W0) % 61.23/61.34 <=> ( aSet0(W1) % 61.23/61.34 & ! [W2] : % 61.23/61.34 ( aElementOf0(W2,W1) % 61.23/61.34 => aElementOf0(W2,W0) ) ) ) ) ). % 61.23/61.34 % 61.23/61.34 fof(mSubFSet,axiom, % 61.23/61.34 ! [W0] : % 61.23/61.34 ( ( aSet0(W0) % 61.23/61.34 & isFinite0(W0) ) % 61.23/61.34 => ! [W1] : % 61.23/61.34 ( aSubsetOf0(W1,W0) % 61.23/61.34 => isFinite0(W1) ) ) ). % 61.23/61.34 % 61.23/61.34 fof(mSubRefl,axiom, % 61.23/61.34 ! [W0] : % 61.23/61.34 ( aSet0(W0) % 61.23/61.34 => aSubsetOf0(W0,W0) ) ). % 61.23/61.34 % 61.23/61.34 fof(mSubASymm,axiom, % 61.23/61.34 ! [W0,W1] : % 61.23/61.34 ( ( aSet0(W0) % 61.23/61.34 & aSet0(W1) ) % 61.23/61.34 => ( ( aSubsetOf0(W0,W1) % 61.23/61.34 & aSubsetOf0(W1,W0) ) % 61.23/61.34 => W0 = W1 ) ) ). % 61.23/61.34 % 61.23/61.34 fof(mSubTrans,axiom, % 61.23/61.34 ! [W0,W1,W2] : % 61.23/61.34 ( ( aSet0(W0) % 61.23/61.34 & aSet0(W1) % 61.23/61.34 & aSet0(W2) ) % 61.23/61.34 => ( ( aSubsetOf0(W0,W1) % 61.23/61.34 & aSubsetOf0(W1,W2) ) % 61.23/61.34 => aSubsetOf0(W0,W2) ) ) ). % 61.23/61.34 % 61.23/61.34 fof(mDefCons,definition, % 61.23/61.34 ! [W0,W1] : % 61.23/61.34 ( ( aSet0(W0) % 61.23/61.34 & aElement0(W1) ) % 61.23/61.34 => ! [W2] : % 61.23/61.34 ( W2 = sdtpldt0(W0,W1) % 61.23/61.34 <=> ( aSet0(W2) % 61.23/61.34 & ! [W3] : % 61.23/61.34 ( aElementOf0(W3,W2) % 61.23/61.34 <=> ( aElement0(W3) % 61.23/61.34 & ( aElementOf0(W3,W0) % 61.23/61.34 | W3 = W1 ) ) ) ) ) ) ). % 61.23/61.34 % 61.23/61.34 fof(mDefDiff,definition, % 61.23/61.34 ! [W0,W1] : % 61.23/61.34 ( ( aSet0(W0) % 61.23/61.34 & aElement0(W1) ) % 61.23/61.34 => ! [W2] : % 61.23/61.34 ( W2 = sdtmndt0(W0,W1) % 61.23/61.35 <=> ( aSet0(W2) % 61.23/61.35 & ! [W3] : % 61.23/61.35 ( aElementOf0(W3,W2) % 61.23/61.35 <=> ( aElement0(W3) % 61.23/61.35 & aElementOf0(W3,W0) % 61.23/61.35 & W3 != W1 ) ) ) ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mConsDiff,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aSet0(W0) % 61.23/61.35 => ! [W1] : % 61.23/61.35 ( aElementOf0(W1,W0) % 61.23/61.35 => sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mDiffCons,axiom, % 61.23/61.35 ! [W0,W1] : % 61.23/61.35 ( ( aElement0(W0) % 61.23/61.35 & aSet0(W1) ) % 61.23/61.35 => ( ~ aElementOf0(W0,W1) % 61.23/61.35 => sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mCConsSet,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aElement0(W0) % 61.23/61.35 => ! [W1] : % 61.23/61.35 ( ( aSet0(W1) % 61.23/61.35 & isCountable0(W1) ) % 61.23/61.35 => isCountable0(sdtpldt0(W1,W0)) ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mCDiffSet,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aElement0(W0) % 61.23/61.35 => ! [W1] : % 61.23/61.35 ( ( aSet0(W1) % 61.23/61.35 & isCountable0(W1) ) % 61.23/61.35 => isCountable0(sdtmndt0(W1,W0)) ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mFConsSet,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aElement0(W0) % 61.23/61.35 => ! [W1] : % 61.23/61.35 ( ( aSet0(W1) % 61.23/61.35 & isFinite0(W1) ) % 61.23/61.35 => isFinite0(sdtpldt0(W1,W0)) ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mFDiffSet,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aElement0(W0) % 61.23/61.35 => ! [W1] : % 61.23/61.35 ( ( aSet0(W1) % 61.23/61.35 & isFinite0(W1) ) % 61.23/61.35 => isFinite0(sdtmndt0(W1,W0)) ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mNATSet,axiom, % 61.23/61.35 ( aSet0(szNzAzT0) % 61.23/61.35 & isCountable0(szNzAzT0) ) ). % 61.23/61.35 % 61.23/61.35 fof(mZeroNum,axiom, % 61.23/61.35 aElementOf0(sz00,szNzAzT0) ). % 61.23/61.35 % 61.23/61.35 fof(mSuccNum,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 => ( aElementOf0(szszuzczcdt0(W0),szNzAzT0) % 61.23/61.35 & szszuzczcdt0(W0) != sz00 ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mSuccEquSucc,axiom, % 61.23/61.35 ! [W0,W1] : % 61.23/61.35 ( ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 & aElementOf0(W1,szNzAzT0) ) % 61.23/61.35 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 61.23/61.35 => W0 = W1 ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mNatExtra,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 => ( W0 = sz00 % 61.23/61.35 | ? [W1] : % 61.23/61.35 ( aElementOf0(W1,szNzAzT0) % 61.23/61.35 & W0 = szszuzczcdt0(W1) ) ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mNatNSucc,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 => W0 != szszuzczcdt0(W0) ) ). % 61.23/61.35 % 61.23/61.35 fof(mLessRel,axiom, % 61.23/61.35 ! [W0,W1] : % 61.23/61.35 ( ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 & aElementOf0(W1,szNzAzT0) ) % 61.23/61.35 => ( sdtlseqdt0(W0,W1) % 61.23/61.35 => $true ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mZeroLess,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 => sdtlseqdt0(sz00,W0) ) ). % 61.23/61.35 % 61.23/61.35 fof(mNoScLessZr,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 => ~ sdtlseqdt0(szszuzczcdt0(W0),sz00) ) ). % 61.23/61.35 % 61.23/61.35 fof(mSuccLess,axiom, % 61.23/61.35 ! [W0,W1] : % 61.23/61.35 ( ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 & aElementOf0(W1,szNzAzT0) ) % 61.23/61.35 => ( sdtlseqdt0(W0,W1) % 61.23/61.35 <=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mLessSucc,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 => sdtlseqdt0(W0,szszuzczcdt0(W0)) ) ). % 61.23/61.35 % 61.23/61.35 fof(mLessRefl,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 => sdtlseqdt0(W0,W0) ) ). % 61.23/61.35 % 61.23/61.35 fof(mLessASymm,axiom, % 61.23/61.35 ! [W0,W1] : % 61.23/61.35 ( ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 & aElementOf0(W1,szNzAzT0) ) % 61.23/61.35 => ( ( sdtlseqdt0(W0,W1) % 61.23/61.35 & sdtlseqdt0(W1,W0) ) % 61.23/61.35 => W0 = W1 ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mLessTrans,axiom, % 61.23/61.35 ! [W0,W1,W2] : % 61.23/61.35 ( ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 & aElementOf0(W1,szNzAzT0) % 61.23/61.35 & aElementOf0(W2,szNzAzT0) ) % 61.23/61.35 => ( ( sdtlseqdt0(W0,W1) % 61.23/61.35 & sdtlseqdt0(W1,W2) ) % 61.23/61.35 => sdtlseqdt0(W0,W2) ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mLessTotal,axiom, % 61.23/61.35 ! [W0,W1] : % 61.23/61.35 ( ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 & aElementOf0(W1,szNzAzT0) ) % 61.23/61.35 => ( sdtlseqdt0(W0,W1) % 61.23/61.35 | sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mIHSort,axiom, % 61.23/61.35 ! [W0,W1] : % 61.23/61.35 ( ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 & aElementOf0(W1,szNzAzT0) ) % 61.23/61.35 => ( iLess0(W0,W1) % 61.23/61.35 => $true ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mIH,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aElementOf0(W0,szNzAzT0) % 61.23/61.35 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 61.23/61.35 % 61.23/61.35 fof(mCardS,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aSet0(W0) % 61.23/61.35 => aElement0(sbrdtbr0(W0)) ) ). % 61.23/61.35 % 61.23/61.35 fof(mCardNum,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aSet0(W0) % 61.23/61.35 => ( aElementOf0(sbrdtbr0(W0),szNzAzT0) % 61.23/61.35 <=> isFinite0(W0) ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mCardEmpty,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aSet0(W0) % 61.23/61.35 => ( sbrdtbr0(W0) = sz00 % 61.23/61.35 <=> W0 = slcrc0 ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mCardCons,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( ( aSet0(W0) % 61.23/61.35 & isFinite0(W0) ) % 61.23/61.35 => ! [W1] : % 61.23/61.35 ( aElement0(W1) % 61.23/61.35 => ( ~ aElementOf0(W1,W0) % 61.23/61.35 => sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mCardDiff,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aSet0(W0) % 61.23/61.35 => ! [W1] : % 61.23/61.35 ( ( isFinite0(W0) % 61.23/61.35 & aElementOf0(W1,W0) ) % 61.23/61.35 => szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mCardSub,axiom, % 61.23/61.35 ! [W0] : % 61.23/61.35 ( aSet0(W0) % 61.23/61.35 => ! [W1] : % 61.23/61.35 ( ( isFinite0(W0) % 61.23/61.35 & aSubsetOf0(W1,W0) ) % 61.23/61.35 => sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 61.23/61.35 % 61.23/61.35 fof(mCardSubEx,axiom, % 61.23/61.35 ! [W0,W1] : % 61.23/61.35 ( ( aSet0(W0) % 61.23/61.35 & aElementOf0(W1,szNzAzT0) ) % 61.23/61.35 => ( ( isFinite0(W0) % 61.23/61.36 & sdtlseqdt0(W1,sbrdtbr0(W0)) ) % 61.23/61.36 => ? [W2] : % 61.23/61.36 ( aSubsetOf0(W2,W0) % 61.23/61.36 & sbrdtbr0(W2) = W1 ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mDefMin,definition, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( ( aSubsetOf0(W0,szNzAzT0) % 61.23/61.36 & W0 != slcrc0 ) % 61.23/61.36 => ! [W1] : % 61.23/61.36 ( W1 = szmzizndt0(W0) % 61.23/61.36 <=> ( aElementOf0(W1,W0) % 61.23/61.36 & ! [W2] : % 61.23/61.36 ( aElementOf0(W2,W0) % 61.23/61.36 => sdtlseqdt0(W1,W2) ) ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mDefMax,definition, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( ( aSubsetOf0(W0,szNzAzT0) % 61.23/61.36 & isFinite0(W0) % 61.23/61.36 & W0 != slcrc0 ) % 61.23/61.36 => ! [W1] : % 61.23/61.36 ( W1 = szmzazxdt0(W0) % 61.23/61.36 <=> ( aElementOf0(W1,W0) % 61.23/61.36 & ! [W2] : % 61.23/61.36 ( aElementOf0(W2,W0) % 61.23/61.36 => sdtlseqdt0(W2,W1) ) ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mMinMin,axiom, % 61.23/61.36 ! [W0,W1] : % 61.23/61.36 ( ( aSubsetOf0(W0,szNzAzT0) % 61.23/61.36 & aSubsetOf0(W1,szNzAzT0) % 61.23/61.36 & W0 != slcrc0 % 61.23/61.36 & W1 != slcrc0 ) % 61.23/61.36 => ( ( aElementOf0(szmzizndt0(W0),W1) % 61.23/61.36 & aElementOf0(szmzizndt0(W1),W0) ) % 61.23/61.36 => szmzizndt0(W0) = szmzizndt0(W1) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mDefSeg,definition, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( aElementOf0(W0,szNzAzT0) % 61.23/61.36 => ! [W1] : % 61.23/61.36 ( W1 = slbdtrb0(W0) % 61.23/61.36 <=> ( aSet0(W1) % 61.23/61.36 & ! [W2] : % 61.23/61.36 ( aElementOf0(W2,W1) % 61.23/61.36 <=> ( aElementOf0(W2,szNzAzT0) % 61.23/61.36 & sdtlseqdt0(szszuzczcdt0(W2),W0) ) ) ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mSegFin,axiom, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( aElementOf0(W0,szNzAzT0) % 61.23/61.36 => isFinite0(slbdtrb0(W0)) ) ). % 61.23/61.36 % 61.23/61.36 fof(mSegZero,axiom, % 61.23/61.36 slbdtrb0(sz00) = slcrc0 ). % 61.23/61.36 % 61.23/61.36 fof(mSegSucc,axiom, % 61.23/61.36 ! [W0,W1] : % 61.23/61.36 ( ( aElementOf0(W0,szNzAzT0) % 61.23/61.36 & aElementOf0(W1,szNzAzT0) ) % 61.23/61.36 => ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1))) % 61.23/61.36 <=> ( aElementOf0(W0,slbdtrb0(W1)) % 61.23/61.36 | W0 = W1 ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mSegLess,axiom, % 61.23/61.36 ! [W0,W1] : % 61.23/61.36 ( ( aElementOf0(W0,szNzAzT0) % 61.23/61.36 & aElementOf0(W1,szNzAzT0) ) % 61.23/61.36 => ( sdtlseqdt0(W0,W1) % 61.23/61.36 <=> aSubsetOf0(slbdtrb0(W0),slbdtrb0(W1)) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mFinSubSeg,axiom, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( ( aSubsetOf0(W0,szNzAzT0) % 61.23/61.36 & isFinite0(W0) ) % 61.23/61.36 => ? [W1] : % 61.23/61.36 ( aElementOf0(W1,szNzAzT0) % 61.23/61.36 & aSubsetOf0(W0,slbdtrb0(W1)) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mCardSeg,axiom, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( aElementOf0(W0,szNzAzT0) % 61.23/61.36 => sbrdtbr0(slbdtrb0(W0)) = W0 ) ). % 61.23/61.36 % 61.23/61.36 fof(mDefSel,definition, % 61.23/61.36 ! [W0,W1] : % 61.23/61.36 ( ( aSet0(W0) % 61.23/61.36 & aElementOf0(W1,szNzAzT0) ) % 61.23/61.36 => ! [W2] : % 61.23/61.36 ( W2 = slbdtsldtrb0(W0,W1) % 61.23/61.36 <=> ( aSet0(W2) % 61.23/61.36 & ! [W3] : % 61.23/61.36 ( aElementOf0(W3,W2) % 61.23/61.36 <=> ( aSubsetOf0(W3,W0) % 61.23/61.36 & sbrdtbr0(W3) = W1 ) ) ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mSelFSet,axiom, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( ( aSet0(W0) % 61.23/61.36 & isFinite0(W0) ) % 61.23/61.36 => ! [W1] : % 61.23/61.36 ( aElementOf0(W1,szNzAzT0) % 61.23/61.36 => isFinite0(slbdtsldtrb0(W0,W1)) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mSelNSet,axiom, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( ( aSet0(W0) % 61.23/61.36 & ~ isFinite0(W0) ) % 61.23/61.36 => ! [W1] : % 61.23/61.36 ( aElementOf0(W1,szNzAzT0) % 61.23/61.36 => slbdtsldtrb0(W0,W1) != slcrc0 ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mSelCSet,axiom, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( ( aSet0(W0) % 61.23/61.36 & isCountable0(W0) ) % 61.23/61.36 => ! [W1] : % 61.23/61.36 ( ( aElementOf0(W1,szNzAzT0) % 61.23/61.36 & W1 != sz00 ) % 61.23/61.36 => isCountable0(slbdtsldtrb0(W0,W1)) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mSelSub,axiom, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( aElementOf0(W0,szNzAzT0) % 61.23/61.36 => ! [W1,W2] : % 61.23/61.36 ( ( aSet0(W1) % 61.23/61.36 & aSet0(W2) % 61.23/61.36 & W0 != sz00 ) % 61.23/61.36 => ( ( aSubsetOf0(slbdtsldtrb0(W1,W0),slbdtsldtrb0(W2,W0)) % 61.23/61.36 & slbdtsldtrb0(W1,W0) != slcrc0 ) % 61.23/61.36 => aSubsetOf0(W1,W2) ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mSelExtra,axiom, % 61.23/61.36 ! [W0,W1] : % 61.23/61.36 ( ( aSet0(W0) % 61.23/61.36 & aElementOf0(W1,szNzAzT0) ) % 61.23/61.36 => ! [W2] : % 61.23/61.36 ( ( aSubsetOf0(W2,slbdtsldtrb0(W0,W1)) % 61.23/61.36 & isFinite0(W2) ) % 61.23/61.36 => ? [W3] : % 61.23/61.36 ( aSubsetOf0(W3,W0) % 61.23/61.36 & isFinite0(W3) % 61.23/61.36 & aSubsetOf0(W2,slbdtsldtrb0(W3,W1)) ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mFunSort,axiom, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( aFunction0(W0) % 61.23/61.36 => $true ) ). % 61.23/61.36 % 61.23/61.36 fof(mDomSet,axiom, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( aFunction0(W0) % 61.23/61.36 => aSet0(szDzozmdt0(W0)) ) ). % 61.23/61.36 % 61.23/61.36 fof(mImgElm,axiom, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( aFunction0(W0) % 61.23/61.36 => ! [W1] : % 61.23/61.36 ( aElementOf0(W1,szDzozmdt0(W0)) % 61.23/61.36 => aElement0(sdtlpdtrp0(W0,W1)) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mDefPtt,definition, % 61.23/61.36 ! [W0,W1] : % 61.23/61.36 ( ( aFunction0(W0) % 61.23/61.36 & aElement0(W1) ) % 61.23/61.36 => ! [W2] : % 61.23/61.36 ( W2 = sdtlbdtrb0(W0,W1) % 61.23/61.36 <=> ( aSet0(W2) % 61.23/61.36 & ! [W3] : % 61.23/61.36 ( aElementOf0(W3,W2) % 61.23/61.36 <=> ( aElementOf0(W3,szDzozmdt0(W0)) % 61.23/61.36 & sdtlpdtrp0(W0,W3) = W1 ) ) ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mPttSet,axiom, % 61.23/61.36 ! [W0,W1] : % 61.23/61.36 ( ( aFunction0(W0) % 61.23/61.36 & aElement0(W1) ) % 61.23/61.36 => aSubsetOf0(sdtlbdtrb0(W0,W1),szDzozmdt0(W0)) ) ). % 61.23/61.36 % 61.23/61.36 fof(mDefSImg,definition, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( aFunction0(W0) % 61.23/61.36 => ! [W1] : % 61.23/61.36 ( aSubsetOf0(W1,szDzozmdt0(W0)) % 61.23/61.36 => ! [W2] : % 61.23/61.36 ( W2 = sdtlcdtrc0(W0,W1) % 61.23/61.36 <=> ( aSet0(W2) % 61.23/61.36 & ! [W3] : % 61.23/61.36 ( aElementOf0(W3,W2) % 61.23/61.36 <=> ? [W4] : % 61.23/61.36 ( aElementOf0(W4,W1) % 61.23/61.36 & sdtlpdtrp0(W0,W4) = W3 ) ) ) ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mImgRng,axiom, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( aFunction0(W0) % 61.23/61.36 => ! [W1] : % 61.23/61.36 ( aElementOf0(W1,szDzozmdt0(W0)) % 61.23/61.36 => aElementOf0(sdtlpdtrp0(W0,W1),sdtlcdtrc0(W0,szDzozmdt0(W0))) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mDefRst,definition, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( aFunction0(W0) % 61.23/61.36 => ! [W1] : % 61.23/61.36 ( aSubsetOf0(W1,szDzozmdt0(W0)) % 61.23/61.36 => ! [W2] : % 61.23/61.36 ( W2 = sdtexdt0(W0,W1) % 61.23/61.36 <=> ( aFunction0(W2) % 61.23/61.36 & szDzozmdt0(W2) = W1 % 61.23/61.36 & ! [W3] : % 61.23/61.36 ( aElementOf0(W3,W1) % 61.23/61.36 => sdtlpdtrp0(W2,W3) = sdtlpdtrp0(W0,W3) ) ) ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mImgCount,axiom, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( aFunction0(W0) % 61.23/61.36 => ! [W1] : % 61.23/61.36 ( ( aSubsetOf0(W1,szDzozmdt0(W0)) % 61.23/61.36 & isCountable0(W1) ) % 61.23/61.36 => ( ! [W2,W3] : % 61.23/61.36 ( ( aElementOf0(W2,szDzozmdt0(W0)) % 61.23/61.36 & aElementOf0(W3,szDzozmdt0(W0)) % 61.23/61.36 & W2 != W3 ) % 61.23/61.36 => sdtlpdtrp0(W0,W2) != sdtlpdtrp0(W0,W3) ) % 61.23/61.36 => isCountable0(sdtlcdtrc0(W0,W1)) ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(mDirichlet,axiom, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( aFunction0(W0) % 61.23/61.36 => ( ( isCountable0(szDzozmdt0(W0)) % 61.23/61.36 & isFinite0(sdtlcdtrc0(W0,szDzozmdt0(W0))) ) % 61.23/61.36 => ( aElement0(szDzizrdt0(W0)) % 61.23/61.36 & isCountable0(sdtlbdtrb0(W0,szDzizrdt0(W0))) ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(m__3291,hypothesis, % 61.23/61.36 ( aSet0(xT) % 61.23/61.36 & isFinite0(xT) ) ). % 61.23/61.36 % 61.23/61.36 fof(m__3418,hypothesis, % 61.23/61.36 aElementOf0(xK,szNzAzT0) ). % 61.23/61.36 % 61.23/61.36 fof(m__3435,hypothesis, % 61.23/61.36 ( aSubsetOf0(xS,szNzAzT0) % 61.23/61.36 & isCountable0(xS) ) ). % 61.23/61.36 % 61.23/61.36 fof(m__3453,hypothesis, % 61.23/61.36 ( aFunction0(xc) % 61.23/61.36 & szDzozmdt0(xc) = slbdtsldtrb0(xS,xK) % 61.23/61.36 & aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ). % 61.23/61.36 % 61.23/61.36 fof(m__3398,hypothesis, % 61.23/61.36 ! [W0] : % 61.23/61.36 ( aElementOf0(W0,szNzAzT0) % 61.23/61.36 => ! [W1] : % 61.23/61.36 ( ( aSubsetOf0(W1,szNzAzT0) % 61.23/61.36 & isCountable0(W1) ) % 61.23/61.36 => ! [W2] : % 61.23/61.36 ( ( aFunction0(W2) % 61.23/61.36 & szDzozmdt0(W2) = slbdtsldtrb0(W1,W0) % 61.23/61.36 & aSubsetOf0(sdtlcdtrc0(W2,szDzozmdt0(W2)),xT) ) % 61.23/61.36 => ( iLess0(W0,xK) % 61.23/61.36 => ? [W3] : % 61.23/61.36 ( aElementOf0(W3,xT) % 61.23/61.36 & ? [W4] : % 61.23/61.36 ( aSubsetOf0(W4,W1) % 61.23/61.36 & isCountable0(W4) % 61.23/61.36 & ! [W5] : % 61.23/61.36 ( aElementOf0(W5,slbdtsldtrb0(W4,W0)) % 61.23/61.36 => sdtlpdtrp0(W2,W5) = W3 ) ) ) ) ) ) ) ). % 61.23/61.36 % 61.23/61.36 fof(m__3462,hypothesis, % 61.23/61.36 xK != sz00 ). % 61.23/61.36 % 61.23/61.36 fof(m__3520,hypothesis, % 61.23/61.36 xK != sz00 ). % 61.23/61.36 % 61.23/61.36 fof(m__,conjecture, % 61.23/61.36 ? [W0] : % 61.23/61.36 ( aElementOf0(W0,szNzAzT0) % 61.23/61.36 & szszuzczcdt0(W0) = xK ) ). % 61.23/61.36 % 61.23/61.36 %------------------------------------------------------------------------------ % 61.23/61.36 %------------------------------------------- % 61.23/61.36 % Proof found % 61.23/61.36 % SZS status Theorem for theBenchmark % 61.23/61.36 % SZS output start Proof % 61.23/61.36 %ClaNum:240(EqnAxiom:88) % 61.23/61.36 %VarNum:1128(SingletonVarNum:327) % 61.23/61.36 %MaxLitNum:9 % 61.23/61.36 %MaxfuncDepth:3 % 61.23/61.36 %SharedTerms:25 % 61.23/61.36 %goalClause: 114 % 61.23/61.36 [90]P1(a33) % 61.23/61.36 [91]P1(a36) % 61.23/61.36 [92]P5(a31) % 61.23/61.36 [93]P5(a36) % 61.23/61.36 [94]P6(a33) % 61.23/61.36 [95]P6(a37) % 61.23/61.36 [96]P2(a42) % 61.23/61.36 [97]P3(a1,a33) % 61.23/61.36 [98]P3(a38,a33) % 61.23/61.36 [99]P7(a37,a33) % 61.23/61.36 [103]~E(a38,a1) % 61.23/61.36 [89]E(f2(a1),a31) % 61.23/61.36 [100]E(f32(a37,a38),f34(a42)) % 61.23/61.36 [101]P7(f3(a42,f34(a42)),a36) % 61.23/61.36 [104]P1(x1041)+~E(x1041,a31) % 61.23/61.36 [111]~P1(x1111)+P7(x1111,x1111) % 61.23/61.36 [119]~P3(x1191,a33)+P9(a1,x1191) % 61.23/61.36 [125]P9(x1251,x1251)+~P3(x1251,a33) % 61.23/61.36 [108]~P2(x1081)+P1(f34(x1081)) % 61.23/61.36 [109]~P1(x1091)+P4(f4(x1091)) % 61.23/61.36 [113]~P3(x1131,a33)+~E(f39(x1131),a1) % 61.23/61.36 [114]~P3(x1141,a33)+~E(f39(x1141),a38) % 61.23/61.36 [115]~P3(x1151,a33)+~E(f39(x1151),x1151) % 61.23/61.36 [117]~P3(x1171,a33)+P5(f2(x1171)) % 61.23/61.36 [126]~P3(x1261,a33)+P3(f39(x1261),a33) % 61.23/61.36 [127]~P3(x1271,a33)+P9(x1271,f39(x1271)) % 61.23/61.36 [128]~P3(x1281,a33)+P8(x1281,f39(x1281)) % 61.23/61.36 [137]~P3(x1371,a33)+~P9(f39(x1371),a1) % 61.23/61.36 [118]~P3(x1181,a33)+E(f4(f2(x1181)),x1181) % 61.23/61.36 [112]~P3(x1122,x1121)+~E(x1121,a31) % 61.23/61.36 [107]~P1(x1071)+~P6(x1071)+~E(x1071,a31) % 61.23/61.36 [110]~P5(x1101)+~P6(x1101)+~P1(x1101) % 61.23/61.36 [105]~P1(x1051)+~E(x1051,a31)+E(f4(x1051),a1) % 61.23/61.36 [106]~P1(x1061)+E(x1061,a31)+~E(f4(x1061),a1) % 61.23/61.36 [116]~P1(x1161)+P3(f5(x1161),x1161)+E(x1161,a31) % 61.23/61.36 [122]~P1(x1221)+~P5(x1221)+P3(f4(x1221),a33) % 61.23/61.36 [129]~P3(x1291,a33)+E(x1291,a1)+P3(f16(x1291),a33) % 61.23/61.36 [130]~P1(x1301)+P5(x1301)+~P3(f4(x1301),a33) % 61.23/61.36 [136]~P5(x1361)+~P7(x1361,a33)+P3(f6(x1361),a33) % 61.23/61.36 [120]~P3(x1201,a33)+E(x1201,a1)+E(f39(f16(x1201)),x1201) % 61.23/61.36 [146]~P5(x1461)+~P7(x1461,a33)+P7(x1461,f2(f6(x1461))) % 61.23/61.36 [123]~P7(x1231,x1232)+P1(x1231)+~P1(x1232) % 61.23/61.36 [124]~P3(x1241,x1242)+P4(x1241)+~P1(x1242) % 61.23/61.36 [121]P1(x1211)+~P3(x1212,a33)+~E(x1211,f2(x1212)) % 61.23/61.37 [147]~P4(x1472)+~P2(x1471)+P7(f26(x1471,x1472),f34(x1471)) % 61.23/61.37 [163]~P2(x1631)+~P3(x1632,f34(x1631))+P4(f30(x1631,x1632)) % 61.23/61.37 [165]~P1(x1651)+~P3(x1652,x1651)+E(f28(f29(x1651,x1652),x1652),x1651) % 61.23/61.37 [201]~P2(x2011)+~P3(x2012,f34(x2011))+P3(f30(x2011,x2012),f3(x2011,f34(x2011))) % 61.23/61.37 [191]~P2(x1911)+~P6(f34(x1911))+P4(f35(x1911))+~P5(f3(x1911,f34(x1911))) % 61.23/61.37 [208]~P2(x2081)+~P6(f34(x2081))+~P5(f3(x2081,f34(x2081)))+P6(f26(x2081,f35(x2081))) % 61.23/61.37 [131]~P5(x1312)+~P7(x1311,x1312)+P5(x1311)+~P1(x1312) % 61.23/61.37 [135]P3(x1352,x1351)+~E(x1352,f40(x1351))+~P7(x1351,a33)+E(x1351,a31) % 61.23/61.37 [139]~P1(x1391)+~P4(x1392)+~P5(x1391)+P5(f28(x1391,x1392)) % 61.23/61.37 [140]~P1(x1401)+~P4(x1402)+~P5(x1401)+P5(f29(x1401,x1402)) % 61.23/61.37 [141]~P1(x1411)+~P4(x1412)+~P6(x1411)+P6(f28(x1411,x1412)) % 61.23/61.37 [142]~P1(x1421)+~P4(x1422)+~P6(x1421)+P6(f29(x1421,x1422)) % 61.23/61.37 [143]~P1(x1431)+P5(x1431)+~P3(x1432,a33)+~E(f32(x1431,x1432),a31) % 61.23/61.37 [145]E(x1451,x1452)+~E(f39(x1451),f39(x1452))+~P3(x1452,a33)+~P3(x1451,a33) % 61.23/61.37 [150]~P1(x1502)+~P5(x1502)+~P7(x1501,x1502)+P9(f4(x1501),f4(x1502)) % 61.23/61.37 [153]~P1(x1531)+~P5(x1531)+~P3(x1532,a33)+P5(f32(x1531,x1532)) % 61.23/61.37 [162]~P1(x1621)+~P1(x1622)+P7(x1621,x1622)+P3(f17(x1622,x1621),x1621) % 61.23/61.37 [169]P9(x1691,x1692)+P9(f39(x1692),x1691)+~P3(x1692,a33)+~P3(x1691,a33) % 61.23/61.37 [181]~P9(x1811,x1812)+~P3(x1812,a33)+~P3(x1811,a33)+P7(f2(x1811),f2(x1812)) % 61.23/61.37 [182]~P9(x1821,x1822)+~P3(x1822,a33)+~P3(x1821,a33)+P9(f39(x1821),f39(x1822)) % 61.23/61.37 [184]~P1(x1841)+~P1(x1842)+P7(x1841,x1842)+~P3(f17(x1842,x1841),x1842) % 61.23/61.37 [186]P9(x1861,x1862)+~P3(x1862,a33)+~P3(x1861,a33)+~P7(f2(x1861),f2(x1862)) % 61.23/61.37 [187]P9(x1871,x1872)+~P3(x1872,a33)+~P3(x1871,a33)+~P9(f39(x1871),f39(x1872)) % 61.23/61.37 [164]P3(x1642,x1641)+~P1(x1641)+~P4(x1642)+E(f29(f28(x1641,x1642),x1642),x1641) % 61.23/61.37 [172]~E(x1721,x1722)+~P3(x1722,a33)+~P3(x1721,a33)+P3(x1721,f2(f39(x1722))) % 61.23/61.37 [193]~P3(x1932,a33)+~P3(x1931,a33)+~P3(x1931,f2(x1932))+P3(x1931,f2(f39(x1932))) % 61.23/61.37 [192]~P1(x1921)+~P5(x1921)+~P3(x1922,x1921)+E(f39(f4(f29(x1921,x1922))),f4(x1921)) % 61.23/61.37 [157]~P1(x1572)+~P7(x1573,x1572)+P3(x1571,x1572)+~P3(x1571,x1573) % 61.23/61.37 [132]~P1(x1322)+~P4(x1323)+P1(x1321)+~E(x1321,f28(x1322,x1323)) % 61.23/61.37 [133]~P1(x1332)+~P4(x1333)+P1(x1331)+~E(x1331,f29(x1332,x1333)) % 61.23/61.37 [134]~P4(x1343)+~P2(x1342)+P1(x1341)+~E(x1341,f26(x1342,x1343)) % 61.23/61.37 [144]~P1(x1442)+P1(x1441)+~P3(x1443,a33)+~E(x1441,f32(x1442,x1443)) % 61.23/61.37 [151]~P3(x1511,x1512)+~P3(x1513,a33)+P3(x1511,a33)+~E(x1512,f2(x1513)) % 61.23/61.37 [159]~P2(x1592)+P1(x1591)+~P7(x1593,f34(x1592))+~E(x1591,f3(x1592,x1593)) % 61.23/61.37 [160]~P2(x1602)+P2(x1601)+~P7(x1603,f34(x1602))+~E(x1601,f27(x1602,x1603)) % 61.23/61.37 [161]~P2(x1613)+~P7(x1612,f34(x1613))+E(f34(x1611),x1612)+~E(x1611,f27(x1613,x1612)) % 61.23/61.37 [166]~P3(x1661,x1663)+~P3(x1662,a33)+P9(f39(x1661),x1662)+~E(x1663,f2(x1662)) % 61.23/61.37 [148]~P1(x1482)+~P1(x1481)+~P7(x1482,x1481)+~P7(x1481,x1482)+E(x1481,x1482) % 61.23/61.37 [179]~P9(x1792,x1791)+~P9(x1791,x1792)+E(x1791,x1792)+~P3(x1792,a33)+~P3(x1791,a33) % 61.23/61.37 [138]~P5(x1381)+P3(x1382,x1381)+~E(x1382,f41(x1381))+~P7(x1381,a33)+E(x1381,a31) % 61.23/61.37 [156]~P1(x1562)+~P6(x1562)+~P3(x1561,a33)+E(x1561,a1)+P6(f32(x1562,x1561)) % 61.23/61.37 [183]~P3(x1832,x1831)+P3(f22(x1831,x1832),x1831)+~P7(x1831,a33)+E(x1831,a31)+E(x1832,f40(x1831)) % 61.23/61.37 [194]~P1(x1941)+~P5(x1941)+~P3(x1942,a33)+~P9(x1942,f4(x1941))+P7(f23(x1941,x1942),x1941) % 61.23/61.37 [196]~P1(x1961)+P3(f25(x1962,x1961),x1961)+~P3(x1962,a33)+E(x1961,f2(x1962))+P3(f25(x1962,x1961),a33) % 61.23/61.37 [197]~P3(x1972,x1971)+~P7(x1971,a33)+~P9(x1972,f22(x1971,x1972))+E(x1971,a31)+E(x1972,f40(x1971)) % 61.23/61.37 [204]~P6(x2042)+~P2(x2041)+~E(f7(x2041,x2042),f8(x2041,x2042))+~P7(x2042,f34(x2041))+P6(f3(x2041,x2042)) % 61.23/61.37 [205]~P6(x2052)+~P2(x2051)+P3(f8(x2051,x2052),f34(x2051))+~P7(x2052,f34(x2051))+P6(f3(x2051,x2052)) % 61.23/61.37 [206]~P6(x2062)+~P2(x2061)+P3(f7(x2061,x2062),f34(x2061))+~P7(x2062,f34(x2061))+P6(f3(x2061,x2062)) % 61.23/61.37 [171]P3(x1712,x1711)+~P1(x1711)+~P4(x1712)+~P5(x1711)+E(f4(f28(x1711,x1712)),f39(f4(x1711))) % 61.23/61.37 [190]~P1(x1901)+~P5(x1901)+~P3(x1902,a33)+~P9(x1902,f4(x1901))+E(f4(f23(x1901,x1902)),x1902) % 61.23/61.37 [199]E(x1991,x1992)+P3(x1991,f2(x1992))+~P3(x1992,a33)+~P3(x1991,a33)+~P3(x1991,f2(f39(x1992))) % 61.23/61.37 [209]~P1(x2091)+P3(f25(x2092,x2091),x2091)+~P3(x2092,a33)+E(x2091,f2(x2092))+P9(f39(f25(x2092,x2091)),x2092) % 61.23/61.37 [210]~P6(x2102)+~P2(x2101)+~P7(x2102,f34(x2101))+P6(f3(x2101,x2102))+E(f30(x2101,f7(x2101,x2102)),f30(x2101,f8(x2101,x2102))) % 61.23/61.37 [158]~P3(x1583,x1581)+P9(x1582,x1583)+~E(x1582,f40(x1581))+~P7(x1581,a33)+E(x1581,a31) % 61.23/61.37 [185]P3(x1851,x1852)+~P3(x1853,a33)+~P3(x1851,a33)+~P9(f39(x1851),x1853)+~E(x1852,f2(x1853)) % 61.23/61.37 [213]~P1(x2131)+~P5(x2133)+~P3(x2132,a33)+~P7(x2133,f32(x2131,x2132))+P5(f10(x2131,x2132,x2133)) % 61.23/61.37 [214]~P1(x2141)+~P5(x2143)+~P3(x2142,a33)+~P7(x2143,f32(x2141,x2142))+P7(f10(x2141,x2142,x2143),x2141) % 61.23/61.37 [229]~P1(x2292)+~P5(x2291)+~P3(x2293,a33)+~P7(x2291,f32(x2292,x2293))+P7(x2291,f32(f10(x2292,x2293,x2291),x2293)) % 61.23/61.37 [152]~P1(x1524)+~P4(x1522)+~P3(x1521,x1523)+~E(x1521,x1522)+~E(x1523,f29(x1524,x1522)) % 61.23/61.37 [154]~P1(x1543)+~P4(x1544)+~P3(x1541,x1542)+P4(x1541)+~E(x1542,f28(x1543,x1544)) % 61.23/61.37 [155]~P1(x1553)+~P4(x1554)+~P3(x1551,x1552)+P4(x1551)+~E(x1552,f29(x1553,x1554)) % 61.23/61.37 [168]~P1(x1682)+~P4(x1684)+~P3(x1681,x1683)+P3(x1681,x1682)+~E(x1683,f29(x1682,x1684)) % 61.23/61.37 [170]~P4(x1703)+~P2(x1701)+~P3(x1702,x1704)+E(f30(x1701,x1702),x1703)+~E(x1704,f26(x1701,x1703)) % 61.23/61.37 [174]~P1(x1744)+~P3(x1741,x1743)+~P3(x1742,a33)+E(f4(x1741),x1742)+~E(x1743,f32(x1744,x1742)) % 61.23/61.37 [176]~P4(x1764)+~P2(x1762)+~P3(x1761,x1763)+P3(x1761,f34(x1762))+~E(x1763,f26(x1762,x1764)) % 61.23/61.37 [180]~P1(x1802)+~P3(x1801,x1803)+P7(x1801,x1802)+~P3(x1804,a33)+~E(x1803,f32(x1802,x1804)) % 61.23/61.37 [198]~P2(x1983)+~P3(x1982,x1984)+~P7(x1984,f34(x1983))+E(f30(x1981,x1982),f30(x1983,x1982))+~E(x1981,f27(x1983,x1984)) % 61.23/61.37 [235]~P2(x2351)+~P3(x2354,x2353)+~E(x2353,f3(x2351,x2352))+~P7(x2352,f34(x2351))+P3(f14(x2351,x2352,x2353,x2354),x2352) % 61.23/61.37 [236]~P2(x2361)+~P3(x2364,x2363)+~E(x2363,f3(x2361,x2362))+~P7(x2362,f34(x2361))+E(f30(x2361,f14(x2361,x2362,x2363,x2364)),x2364) % 61.23/61.37 [189]~P5(x1891)+~P3(x1892,x1891)+P3(f24(x1891,x1892),x1891)+~P7(x1891,a33)+E(x1891,a31)+E(x1892,f41(x1891)) % 61.23/61.37 [202]~P5(x2021)+~P3(x2022,x2021)+~P7(x2021,a33)+~P9(f24(x2021,x2022),x2022)+E(x2021,a31)+E(x2022,f41(x2021)) % 61.23/61.37 [218]~P1(x2181)+~P3(x2182,a33)+~P3(f25(x2182,x2181),x2181)+E(x2181,f2(x2182))+~P3(f25(x2182,x2181),a33)+~P9(f39(f25(x2182,x2181)),x2182) % 61.23/61.37 [175]~P1(x1752)+~P1(x1751)+~P7(x1753,x1752)+~P7(x1751,x1753)+P7(x1751,x1752)+~P1(x1753) % 61.23/61.37 [203]~P9(x2031,x2033)+P9(x2031,x2032)+~P9(x2033,x2032)+~P3(x2032,a33)+~P3(x2033,a33)+~P3(x2031,a33) % 61.23/61.37 [167]~P5(x1671)+~P3(x1672,x1671)+P9(x1672,x1673)+~E(x1673,f41(x1671))+~P7(x1671,a33)+E(x1671,a31) % 61.23/61.37 [212]~P2(x2121)+~P2(x2122)+P3(f9(x2122,x2123,x2121),x2123)+~E(f34(x2121),x2123)+~P7(x2123,f34(x2122))+E(x2121,f27(x2122,x2123)) % 61.23/61.37 [215]~P1(x2151)+~P1(x2152)+~P4(x2153)+P3(f20(x2152,x2153,x2151),x2151)+~E(f20(x2152,x2153,x2151),x2153)+E(x2151,f29(x2152,x2153)) % 61.23/61.37 [216]~P1(x2161)+~P1(x2162)+~P4(x2163)+P3(f21(x2162,x2163,x2161),x2161)+E(x2161,f28(x2162,x2163))+P4(f21(x2162,x2163,x2161)) % 61.23/61.37 [217]~P1(x2171)+~P1(x2172)+~P4(x2173)+P3(f20(x2172,x2173,x2171),x2171)+E(x2171,f29(x2172,x2173))+P4(f20(x2172,x2173,x2171)) % 61.23/61.37 [219]~P1(x2191)+~P1(x2192)+~P4(x2193)+P3(f20(x2192,x2193,x2191),x2191)+P3(f20(x2192,x2193,x2191),x2192)+E(x2191,f29(x2192,x2193)) % 61.23/61.37 [222]~P1(x2221)+~P4(x2223)+~P2(x2222)+P3(f12(x2222,x2223,x2221),x2221)+P3(f12(x2222,x2223,x2221),f34(x2222))+E(x2221,f26(x2222,x2223)) % 61.23/61.37 [223]~P1(x2231)+~P1(x2232)+P3(f11(x2232,x2233,x2231),x2231)+P7(f11(x2232,x2233,x2231),x2232)+~P3(x2233,a33)+E(x2231,f32(x2232,x2233)) % 61.23/61.37 [226]~P1(x2261)+~P2(x2262)+P3(f13(x2262,x2263,x2261),x2261)+P3(f15(x2262,x2263,x2261),x2263)+~P7(x2263,f34(x2262))+E(x2261,f3(x2262,x2263)) % 61.23/61.37 [220]~P1(x2201)+~P4(x2203)+~P2(x2202)+P3(f12(x2202,x2203,x2201),x2201)+E(x2201,f26(x2202,x2203))+E(f30(x2202,f12(x2202,x2203,x2201)),x2203) % 61.23/61.37 [221]~P1(x2211)+~P1(x2212)+P3(f11(x2212,x2213,x2211),x2211)+~P3(x2213,a33)+E(x2211,f32(x2212,x2213))+E(f4(f11(x2212,x2213,x2211)),x2213) % 61.23/61.37 [230]~P1(x2301)+~P2(x2302)+P3(f13(x2302,x2303,x2301),x2301)+~P7(x2303,f34(x2302))+E(x2301,f3(x2302,x2303))+E(f30(x2302,f15(x2302,x2303,x2301)),f13(x2302,x2303,x2301)) % 61.23/61.37 [232]~P2(x2322)+~P2(x2321)+~E(f34(x2321),x2323)+~P7(x2323,f34(x2322))+E(x2321,f27(x2322,x2323))+~E(f30(x2321,f9(x2322,x2323,x2321)),f30(x2322,f9(x2322,x2323,x2321))) % 61.23/61.37 [149]~P1(x1494)+~P4(x1493)+~P4(x1491)+P3(x1491,x1492)+~E(x1491,x1493)+~E(x1492,f28(x1494,x1493)) % 61.23/61.37 [173]~P1(x1733)+~P4(x1732)+~P3(x1731,x1734)+E(x1731,x1732)+P3(x1731,x1733)+~E(x1734,f28(x1733,x1732)) % 61.23/61.37 [177]~P1(x1773)+~P4(x1774)+~P4(x1771)+~P3(x1771,x1773)+P3(x1771,x1772)+~E(x1772,f28(x1773,x1774)) % 61.23/61.37 [188]~P1(x1884)+~P7(x1881,x1884)+P3(x1881,x1882)+~P3(x1883,a33)+~E(x1882,f32(x1884,x1883))+~E(f4(x1881),x1883) % 61.23/61.37 [195]~P4(x1954)+~P2(x1953)+P3(x1951,x1952)+~E(f30(x1953,x1951),x1954)+~P3(x1951,f34(x1953))+~E(x1952,f26(x1953,x1954)) % 61.23/61.37 [207]~P2(x2073)+~P3(x2075,x2074)+P3(x2071,x2072)+~P7(x2074,f34(x2073))+~E(x2072,f3(x2073,x2074))+~E(f30(x2073,x2075),x2071) % 61.23/61.37 [200]E(f40(x2002),f40(x2001))+~P7(x2001,a33)+~P7(x2002,a33)+~P3(f40(x2001),x2002)+~P3(f40(x2002),x2001)+E(x2001,a31)+E(x2002,a31) % 61.23/61.37 [211]~P1(x2113)+~P1(x2112)+P7(x2112,x2113)+~P3(x2111,a33)+~P7(f32(x2112,x2111),f32(x2113,x2111))+E(x2111,a1)+E(f32(x2112,x2111),a31) % 61.23/61.37 [228]~P1(x2281)+~P1(x2282)+~P4(x2283)+E(f21(x2282,x2283,x2281),x2283)+P3(f21(x2282,x2283,x2281),x2281)+P3(f21(x2282,x2283,x2281),x2282)+E(x2281,f28(x2282,x2283)) % 61.23/61.37 [233]~P1(x2331)+~P1(x2332)+~P4(x2333)+~E(f21(x2332,x2333,x2331),x2333)+~P3(f21(x2332,x2333,x2331),x2331)+E(x2331,f28(x2332,x2333))+~P4(f21(x2332,x2333,x2331)) % 61.23/61.37 [234]~P1(x2341)+~P1(x2342)+~P4(x2343)+~P3(f21(x2342,x2343,x2341),x2341)+~P3(f21(x2342,x2343,x2341),x2342)+E(x2341,f28(x2342,x2343))+~P4(f21(x2342,x2343,x2341)) % 61.23/61.37 [237]~P1(x2371)+~P1(x2372)+~P3(x2373,a33)+~P3(f11(x2372,x2373,x2371),x2371)+~P7(f11(x2372,x2373,x2371),x2372)+E(x2371,f32(x2372,x2373))+~E(f4(f11(x2372,x2373,x2371)),x2373) % 61.23/61.37 [238]~P1(x2381)+~P4(x2383)+~P2(x2382)+~P3(f12(x2382,x2383,x2381),x2381)+~P3(f12(x2382,x2383,x2381),f34(x2382))+E(x2381,f26(x2382,x2383))+~E(f30(x2382,f12(x2382,x2383,x2381)),x2383) % 61.23/61.37 [178]~P1(x1784)+~P4(x1782)+~P4(x1781)+~P3(x1781,x1784)+E(x1781,x1782)+P3(x1781,x1783)+~E(x1783,f29(x1784,x1782)) % 61.23/61.37 [231]~P1(x2311)+~P2(x2312)+~P3(x2314,x2313)+~P7(x2313,f34(x2312))+~P3(f13(x2312,x2313,x2311),x2311)+~E(f30(x2312,x2314),f13(x2312,x2313,x2311))+E(x2311,f3(x2312,x2313)) % 61.23/61.37 [239]~P1(x2391)+~P1(x2392)+~P4(x2393)+E(f20(x2392,x2393,x2391),x2393)+~P3(f20(x2392,x2393,x2391),x2391)+~P3(f20(x2392,x2393,x2391),x2392)+E(x2391,f29(x2392,x2393))+~P4(f20(x2392,x2393,x2391)) % 61.23/61.37 [224]~P6(x2242)+~P2(x2243)+~E(f34(x2243),f32(x2242,x2241))+~P3(x2241,a33)+~P7(x2242,a33)+~P8(x2241,a38)+P6(f18(x2241,x2242,x2243))+~P7(f3(x2243,f34(x2243)),a36) % 61.23/61.37 [225]~P6(x2252)+~P2(x2253)+~E(f34(x2253),f32(x2252,x2251))+~P3(x2251,a33)+~P7(x2252,a33)+~P8(x2251,a38)+P3(f19(x2251,x2252,x2253),a36)+~P7(f3(x2253,f34(x2253)),a36) % 61.23/61.37 [227]~P6(x2272)+~P2(x2273)+~E(f34(x2273),f32(x2272,x2271))+~P3(x2271,a33)+~P7(x2272,a33)+~P8(x2271,a38)+P7(f18(x2271,x2272,x2273),x2272)+~P7(f3(x2273,f34(x2273)),a36) % 61.23/61.37 [240]~P6(x2404)+~P2(x2401)+~E(f34(x2401),f32(x2404,x2403))+~P3(x2403,a33)+~P7(x2404,a33)+~P8(x2403,a38)+E(f30(x2401,x2402),f19(x2403,x2404,x2401))+~P3(x2402,f32(f18(x2403,x2404,x2401),x2403))+~P7(f3(x2401,f34(x2401)),a36) % 61.23/61.37 %EqnAxiom % 61.23/61.37 [1]E(x11,x11) % 61.23/61.37 [2]E(x22,x21)+~E(x21,x22) % 61.23/61.37 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 61.23/61.37 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 61.23/61.37 [5]~E(x51,x52)+E(f32(x51,x53),f32(x52,x53)) % 61.23/61.37 [6]~E(x61,x62)+E(f32(x63,x61),f32(x63,x62)) % 61.23/61.37 [7]~E(x71,x72)+E(f34(x71),f34(x72)) % 61.23/61.37 [8]~E(x81,x82)+E(f9(x81,x83,x84),f9(x82,x83,x84)) % 61.23/61.37 [9]~E(x91,x92)+E(f9(x93,x91,x94),f9(x93,x92,x94)) % 61.23/61.37 [10]~E(x101,x102)+E(f9(x103,x104,x101),f9(x103,x104,x102)) % 61.23/61.37 [11]~E(x111,x112)+E(f3(x111,x113),f3(x112,x113)) % 61.23/61.37 [12]~E(x121,x122)+E(f3(x123,x121),f3(x123,x122)) % 61.23/61.37 [13]~E(x131,x132)+E(f4(x131),f4(x132)) % 61.23/61.37 [14]~E(x141,x142)+E(f25(x141,x143),f25(x142,x143)) % 61.23/61.37 [15]~E(x151,x152)+E(f25(x153,x151),f25(x153,x152)) % 61.23/61.37 [16]~E(x161,x162)+E(f30(x161,x163),f30(x162,x163)) % 61.23/61.37 [17]~E(x171,x172)+E(f30(x173,x171),f30(x173,x172)) % 61.23/61.37 [18]~E(x181,x182)+E(f26(x181,x183),f26(x182,x183)) % 61.23/61.37 [19]~E(x191,x192)+E(f26(x193,x191),f26(x193,x192)) % 61.23/61.37 [20]~E(x201,x202)+E(f39(x201),f39(x202)) % 61.23/61.37 [21]~E(x211,x212)+E(f28(x211,x213),f28(x212,x213)) % 61.23/61.37 [22]~E(x221,x222)+E(f28(x223,x221),f28(x223,x222)) % 61.23/61.37 [23]~E(x231,x232)+E(f8(x231,x233),f8(x232,x233)) % 61.23/61.37 [24]~E(x241,x242)+E(f8(x243,x241),f8(x243,x242)) % 61.23/61.37 [25]~E(x251,x252)+E(f5(x251),f5(x252)) % 61.23/61.37 [26]~E(x261,x262)+E(f11(x261,x263,x264),f11(x262,x263,x264)) % 61.23/61.37 [27]~E(x271,x272)+E(f11(x273,x271,x274),f11(x273,x272,x274)) % 61.23/61.37 [28]~E(x281,x282)+E(f11(x283,x284,x281),f11(x283,x284,x282)) % 61.23/61.37 [29]~E(x291,x292)+E(f18(x291,x293,x294),f18(x292,x293,x294)) % 61.23/61.37 [30]~E(x301,x302)+E(f18(x303,x301,x304),f18(x303,x302,x304)) % 61.23/61.37 [31]~E(x311,x312)+E(f18(x313,x314,x311),f18(x313,x314,x312)) % 61.23/61.37 [32]~E(x321,x322)+E(f20(x321,x323,x324),f20(x322,x323,x324)) % 61.23/61.37 [33]~E(x331,x332)+E(f20(x333,x331,x334),f20(x333,x332,x334)) % 61.23/61.37 [34]~E(x341,x342)+E(f20(x343,x344,x341),f20(x343,x344,x342)) % 61.23/61.37 [35]~E(x351,x352)+E(f16(x351),f16(x352)) % 61.23/61.37 [36]~E(x361,x362)+E(f7(x361,x363),f7(x362,x363)) % 61.23/61.37 [37]~E(x371,x372)+E(f7(x373,x371),f7(x373,x372)) % 61.23/61.37 [38]~E(x381,x382)+E(f10(x381,x383,x384),f10(x382,x383,x384)) % 61.23/61.37 [39]~E(x391,x392)+E(f10(x393,x391,x394),f10(x393,x392,x394)) % 61.23/61.37 [40]~E(x401,x402)+E(f10(x403,x404,x401),f10(x403,x404,x402)) % 61.23/61.37 [41]~E(x411,x412)+E(f41(x411),f41(x412)) % 61.23/61.37 [42]~E(x421,x422)+E(f12(x421,x423,x424),f12(x422,x423,x424)) % 61.23/61.37 [43]~E(x431,x432)+E(f12(x433,x431,x434),f12(x433,x432,x434)) % 61.23/61.37 [44]~E(x441,x442)+E(f12(x443,x444,x441),f12(x443,x444,x442)) % 61.23/61.37 [45]~E(x451,x452)+E(f24(x451,x453),f24(x452,x453)) % 61.23/61.37 [46]~E(x461,x462)+E(f24(x463,x461),f24(x463,x462)) % 61.23/61.37 [47]~E(x471,x472)+E(f27(x471,x473),f27(x472,x473)) % 61.23/61.37 [48]~E(x481,x482)+E(f27(x483,x481),f27(x483,x482)) % 61.23/61.37 [49]~E(x491,x492)+E(f17(x491,x493),f17(x492,x493)) % 61.23/61.37 [50]~E(x501,x502)+E(f17(x503,x501),f17(x503,x502)) % 61.23/61.37 [51]~E(x511,x512)+E(f29(x511,x513),f29(x512,x513)) % 61.23/61.37 [52]~E(x521,x522)+E(f29(x523,x521),f29(x523,x522)) % 61.23/61.37 [53]~E(x531,x532)+E(f21(x531,x533,x534),f21(x532,x533,x534)) % 61.23/61.37 [54]~E(x541,x542)+E(f21(x543,x541,x544),f21(x543,x542,x544)) % 61.23/61.37 [55]~E(x551,x552)+E(f21(x553,x554,x551),f21(x553,x554,x552)) % 61.23/61.37 [56]~E(x561,x562)+E(f40(x561),f40(x562)) % 61.23/61.37 [57]~E(x571,x572)+E(f13(x571,x573,x574),f13(x572,x573,x574)) % 61.23/61.37 [58]~E(x581,x582)+E(f13(x583,x581,x584),f13(x583,x582,x584)) % 61.23/61.37 [59]~E(x591,x592)+E(f13(x593,x594,x591),f13(x593,x594,x592)) % 61.23/61.37 [60]~E(x601,x602)+E(f15(x601,x603,x604),f15(x602,x603,x604)) % 61.23/61.37 [61]~E(x611,x612)+E(f15(x613,x611,x614),f15(x613,x612,x614)) % 61.23/61.37 [62]~E(x621,x622)+E(f15(x623,x624,x621),f15(x623,x624,x622)) % 61.23/61.37 [63]~E(x631,x632)+E(f6(x631),f6(x632)) % 61.23/61.37 [64]~E(x641,x642)+E(f19(x641,x643,x644),f19(x642,x643,x644)) % 61.23/61.37 [65]~E(x651,x652)+E(f19(x653,x651,x654),f19(x653,x652,x654)) % 61.23/61.37 [66]~E(x661,x662)+E(f19(x663,x664,x661),f19(x663,x664,x662)) % 61.23/61.37 [67]~E(x671,x672)+E(f35(x671),f35(x672)) % 61.23/61.37 [68]~E(x681,x682)+E(f22(x681,x683),f22(x682,x683)) % 61.23/61.37 [69]~E(x691,x692)+E(f22(x693,x691),f22(x693,x692)) % 61.23/61.37 [70]~E(x701,x702)+E(f23(x701,x703),f23(x702,x703)) % 61.23/61.37 [71]~E(x711,x712)+E(f23(x713,x711),f23(x713,x712)) % 61.23/61.37 [72]~E(x721,x722)+E(f14(x721,x723,x724,x725),f14(x722,x723,x724,x725)) % 61.23/61.37 [73]~E(x731,x732)+E(f14(x733,x731,x734,x735),f14(x733,x732,x734,x735)) % 61.23/61.37 [74]~E(x741,x742)+E(f14(x743,x744,x741,x745),f14(x743,x744,x742,x745)) % 61.23/61.37 [75]~E(x751,x752)+E(f14(x753,x754,x755,x751),f14(x753,x754,x755,x752)) % 61.23/61.37 [76]~P1(x761)+P1(x762)+~E(x761,x762) % 61.23/61.37 [77]P3(x772,x773)+~E(x771,x772)+~P3(x771,x773) % 61.23/61.37 [78]P3(x783,x782)+~E(x781,x782)+~P3(x783,x781) % 61.23/61.37 [79]~P5(x791)+P5(x792)+~E(x791,x792) % 61.23/61.37 [80]P7(x802,x803)+~E(x801,x802)+~P7(x801,x803) % 61.23/61.37 [81]P7(x813,x812)+~E(x811,x812)+~P7(x813,x811) % 61.23/61.37 [82]~P6(x821)+P6(x822)+~E(x821,x822) % 61.23/61.37 [83]~P4(x831)+P4(x832)+~E(x831,x832) % 61.23/61.37 [84]~P2(x841)+P2(x842)+~E(x841,x842) % 61.23/61.37 [85]P9(x852,x853)+~E(x851,x852)+~P9(x851,x853) % 61.23/61.37 [86]P9(x863,x862)+~E(x861,x862)+~P9(x863,x861) % 61.23/61.37 [87]P8(x872,x873)+~E(x871,x872)+~P8(x871,x873) % 61.23/61.37 [88]P8(x883,x882)+~E(x881,x882)+~P8(x883,x881) % 61.23/61.37 % 61.23/61.37 %------------------------------------------- % 61.23/61.37 cnf(241,plain, % 61.23/61.37 (P1(a31)), % 61.23/61.37 inference(equality_inference,[],[104])). % 61.23/61.37 cnf(242,plain, % 61.23/61.37 (~P1(a31)+E(f4(a31),a1)), % 61.23/61.37 inference(equality_inference,[],[105])). % 61.23/61.37 cnf(243,plain, % 61.23/61.37 (~P6(a31)+~P1(a31)), % 61.23/61.37 inference(equality_inference,[],[107])). % 61.23/61.37 cnf(244,plain, % 61.23/61.37 (~P3(x2441,a31)), % 61.23/61.37 inference(equality_inference,[],[112])). % 61.23/61.37 cnf(245,plain, % 61.23/61.37 (P1(f2(x2451))+~P3(x2451,a33)), % 61.23/61.37 inference(equality_inference,[],[121])). % 61.23/61.37 cnf(246,plain, % 61.23/61.37 (~P1(x2461)+~P4(x2462)+P1(f28(x2461,x2462))), % 61.23/61.37 inference(equality_inference,[],[132])). % 61.23/61.37 cnf(247,plain, % 61.23/61.37 (~P1(x2471)+~P4(x2472)+P1(f29(x2471,x2472))), % 61.23/61.37 inference(equality_inference,[],[133])). % 61.23/61.37 cnf(248,plain, % 61.23/61.37 (~P4(x2481)+~P2(x2482)+P1(f26(x2482,x2481))), % 61.23/61.37 inference(equality_inference,[],[134])). % 61.23/61.37 cnf(249,plain, % 61.23/61.37 (P3(f40(x2491),x2491)+~P7(x2491,a33)+E(x2491,a31)), % 61.23/61.37 inference(equality_inference,[],[135])). % 61.23/61.37 cnf(250,plain, % 61.23/61.37 (~P5(x2501)+P3(f41(x2501),x2501)+~P7(x2501,a33)+E(x2501,a31)), % 61.23/61.37 inference(equality_inference,[],[138])). % 61.23/61.37 cnf(251,plain, % 61.23/61.37 (~P1(x2511)+P1(f32(x2511,x2512))+~P3(x2512,a33)), % 61.23/61.37 inference(equality_inference,[],[144])). % 61.23/61.37 cnf(256,plain, % 61.23/61.37 (~P3(x2561,x2562)+P9(f40(x2562),x2561)+~P7(x2562,a33)+E(x2562,a31)), % 61.23/61.37 inference(equality_inference,[],[158])). % 61.23/61.37 cnf(260,plain, % 61.23/61.37 (~P3(x2601,f2(x2602))+P9(f39(x2601),x2602)+~P3(x2602,a33)), % 61.23/61.37 inference(equality_inference,[],[166])). % 61.23/61.37 cnf(262,plain, % 61.23/61.37 (P3(x2621,x2622)+~P1(x2622)+~P4(x2623)+~P3(x2621,f29(x2622,x2623))), % 61.23/61.37 inference(equality_inference,[],[168])). % 61.23/61.37 cnf(264,plain, % 61.23/61.37 (~P3(x2641,a33)+~P3(x2641,a33)+P3(x2641,f2(f39(x2641)))), % 61.23/61.37 inference(equality_inference,[],[172])). % 61.23/61.37 cnf(265,plain, % 61.23/61.37 (E(x2651,x2652)+P3(x2651,x2653)+~P1(x2653)+~P4(x2652)+~P3(x2651,f28(x2653,x2652))), % 61.23/61.37 inference(equality_inference,[],[173])). % 61.23/61.37 cnf(268,plain, % 61.23/61.37 (~P3(x2681,x2682)+~P1(x2682)+~P4(x2683)+P3(x2681,f28(x2682,x2683))+~P4(x2681)), % 61.23/61.37 inference(equality_inference,[],[177])). % 61.23/61.37 cnf(270,plain, % 61.23/61.37 (P7(x2701,x2702)+~P1(x2702)+~P3(x2701,f32(x2702,x2703))+~P3(x2703,a33)), % 61.23/61.37 inference(equality_inference,[],[180])). % 61.23/61.37 cnf(271,plain, % 61.23/61.37 (P3(x2711,f2(x2712))+~P3(x2711,a33)+~P9(f39(x2711),x2712)+~P3(x2712,a33)), % 61.23/61.37 inference(equality_inference,[],[185])). % 61.23/61.37 cnf(276,plain, % 61.23/61.37 (E(f4(a31),a1)), % 61.23/61.37 inference(scs_inference,[],[241,242])). % 61.23/61.37 cnf(277,plain, % 61.23/61.37 (~P6(a31)), % 61.23/61.37 inference(scs_inference,[],[241,243])). % 61.23/61.37 cnf(278,plain, % 61.23/61.37 (E(a31,f2(a1))), % 61.23/61.37 inference(scs_inference,[],[89,2])). % 61.23/61.37 cnf(279,plain, % 61.23/61.37 (~P3(x2791,f2(a1))), % 61.23/61.37 inference(scs_inference,[],[89,2,112])). % 61.23/61.37 cnf(281,plain, % 61.23/61.37 (P9(a1,a1)), % 61.23/61.37 inference(scs_inference,[],[89,97,2,112,125])). % 61.23/61.37 cnf(283,plain, % 61.23/61.37 (P1(f2(a1))), % 61.23/61.37 inference(scs_inference,[],[89,97,2,112,125,245])). % 61.23/61.37 cnf(285,plain, % 61.23/61.37 (~E(a33,a31)), % 61.23/61.37 inference(scs_inference,[],[89,97,244,2,112,125,245,78])). % 61.23/61.37 cnf(286,plain, % 61.23/61.37 (~P3(x2861,a31)), % 61.23/61.37 inference(rename_variables,[],[244])). % 61.23/61.37 cnf(287,plain, % 61.23/61.37 (P1(f32(a33,a1))), % 61.23/61.37 inference(scs_inference,[],[89,97,244,90,2,112,125,245,78,251])). % 61.23/61.37 cnf(289,plain, % 61.23/61.37 (P3(a1,f2(f39(a1)))), % 61.23/61.37 inference(scs_inference,[],[89,97,244,90,2,112,125,245,78,251,264])). % 61.23/61.37 cnf(291,plain, % 61.23/61.37 (~P6(f2(a1))), % 61.23/61.37 inference(scs_inference,[],[89,97,244,90,2,112,125,245,78,251,264,107])). % 61.23/61.37 cnf(293,plain, % 61.23/61.37 (~P5(a33)), % 61.23/61.37 inference(scs_inference,[],[89,97,244,90,94,2,112,125,245,78,251,264,107,110])). % 61.23/61.37 cnf(295,plain, % 61.23/61.37 (P5(f2(a1))), % 61.23/61.37 inference(scs_inference,[],[89,97,244,90,92,94,2,112,125,245,78,251,264,107,110,79])). % 61.23/61.37 cnf(296,plain, % 61.23/61.37 (P7(a31,a33)), % 61.23/61.37 inference(scs_inference,[],[89,97,244,286,90,92,94,241,2,112,125,245,78,251,264,107,110,79,162])). % 61.23/61.37 cnf(297,plain, % 61.23/61.37 (~P3(x2971,a31)), % 61.23/61.37 inference(rename_variables,[],[244])). % 61.23/61.37 cnf(299,plain, % 61.23/61.37 (~P9(f39(a1),a1)), % 61.23/61.37 inference(scs_inference,[],[89,97,244,286,90,92,94,241,2,112,125,245,78,251,264,107,110,79,162,271])). % 61.23/61.37 cnf(301,plain, % 61.23/61.37 (P7(f2(a1),f2(a1))), % 61.23/61.37 inference(scs_inference,[],[89,97,244,286,90,92,94,241,2,112,125,245,78,251,264,107,110,79,162,271,181])). % 61.23/61.37 cnf(305,plain, % 61.23/61.37 (~P7(a33,a31)), % 61.23/61.37 inference(scs_inference,[],[89,97,244,286,90,92,94,241,2,112,125,245,78,251,264,107,110,79,162,271,181,182,148])). % 61.23/61.37 cnf(307,plain, % 61.23/61.37 (~P9(f39(a38),a1)), % 61.23/61.37 inference(scs_inference,[],[89,97,98,244,286,297,90,92,94,241,2,112,125,245,78,251,264,107,110,79,162,271,181,182,148,185])). % 61.23/61.37 cnf(314,plain, % 61.23/61.37 (P7(f2(a1),a31)), % 61.23/61.37 inference(scs_inference,[],[89,97,98,244,286,297,90,92,94,99,241,2,112,125,245,78,251,264,107,110,79,162,271,181,182,148,185,249,3,80,81])). % 61.23/61.37 cnf(315,plain, % 61.23/61.37 (P3(f40(a37),a37)+P6(a31)), % 61.23/61.37 inference(scs_inference,[],[89,97,98,244,286,297,90,92,94,95,99,241,2,112,125,245,78,251,264,107,110,79,162,271,181,182,148,185,249,3,80,81,82])). % 61.23/61.37 cnf(323,plain, % 61.23/61.37 (P3(f40(a37),a37)), % 61.23/61.37 inference(scs_inference,[],[277,315])). % 61.23/61.37 cnf(326,plain, % 61.23/61.37 (P1(f2(a38))), % 61.23/61.37 inference(scs_inference,[],[98,277,315,125,245])). % 61.23/61.37 cnf(328,plain, % 61.23/61.37 (E(a1,f4(a31))), % 61.23/61.37 inference(scs_inference,[],[98,276,277,315,125,245,2])). % 61.23/61.37 cnf(329,plain, % 61.23/61.37 (P3(a38,f2(f39(a38)))), % 61.23/61.37 inference(scs_inference,[],[98,276,277,315,125,245,2,264])). % 61.23/61.37 cnf(331,plain, % 61.23/61.37 (P1(f32(f2(a1),a1))), % 61.23/61.37 inference(scs_inference,[],[97,98,283,276,277,315,125,245,2,264,251])). % 61.23/61.37 cnf(333,plain, % 61.23/61.37 (P9(a1,f4(a31))), % 61.23/61.37 inference(scs_inference,[],[97,98,281,283,276,277,315,125,245,2,264,251,86])). % 61.23/61.37 cnf(334,plain, % 61.23/61.37 (~E(f2(f39(a1)),f2(a1))), % 61.23/61.37 inference(scs_inference,[],[97,98,281,279,283,289,276,277,315,125,245,2,264,251,86,78])). % 61.23/61.37 cnf(335,plain, % 61.23/61.37 (~P3(x3351,f2(a1))), % 61.23/61.37 inference(rename_variables,[],[279])). % 61.23/61.37 cnf(338,plain, % 61.23/61.37 (P7(a31,f2(a1))), % 61.23/61.37 inference(scs_inference,[],[89,97,299,98,281,279,283,301,289,276,103,277,315,125,245,2,264,251,86,78,3,85,80])). % 61.23/61.37 cnf(339,plain, % 61.23/61.37 (P3(f4(a31),a33)), % 61.23/61.37 inference(scs_inference,[],[89,97,299,98,281,279,283,301,289,276,103,277,315,125,245,2,264,251,86,78,3,85,80,77])). % 61.23/61.37 cnf(342,plain, % 61.23/61.37 (~P3(a33,f32(f2(a1),a1))), % 61.23/61.37 inference(scs_inference,[],[89,97,299,98,281,279,283,301,289,295,276,103,277,293,315,125,245,2,264,251,86,78,3,85,80,77,131,270])). % 61.23/61.37 cnf(344,plain, % 61.23/61.37 (P9(f39(a38),f39(a38))), % 61.23/61.37 inference(scs_inference,[],[89,97,299,98,281,279,283,301,289,295,276,103,277,293,315,125,245,2,264,251,86,78,3,85,80,77,131,270,182])). % 61.23/61.37 cnf(346,plain, % 61.23/61.37 (~P7(f2(f39(a1)),f2(a1))), % 61.23/61.37 inference(scs_inference,[],[89,97,299,98,281,279,335,283,301,289,295,276,103,277,293,315,125,245,2,264,251,86,78,3,85,80,77,131,270,182,157])). % 61.23/61.37 cnf(351,plain, % 61.23/61.37 (P9(a1,a38)), % 61.23/61.37 inference(scs_inference,[],[89,97,299,307,98,281,279,335,283,301,289,295,276,103,277,293,315,125,245,2,264,251,86,78,3,85,80,77,131,270,182,157,181,169])). % 61.23/61.37 cnf(353,plain, % 61.23/61.37 (P7(f23(a31,a1),a31)), % 61.23/61.37 inference(scs_inference,[],[89,97,299,307,98,281,279,335,283,301,289,295,276,103,277,293,92,241,315,125,245,2,264,251,86,78,3,85,80,77,131,270,182,157,181,169,194])). % 61.23/61.37 cnf(355,plain, % 61.23/61.37 (~P9(f39(f4(a31)),a1)), % 61.23/61.37 inference(scs_inference,[],[89,97,278,299,307,98,281,279,335,283,301,289,244,295,276,103,277,293,92,241,315,125,245,2,264,251,86,78,3,85,80,77,131,270,182,157,181,169,194,185])). % 61.23/61.37 cnf(358,plain, % 61.23/61.37 (~E(f39(a1),a1)), % 61.23/61.37 inference(scs_inference,[],[89,97,278,299,307,98,281,279,335,283,301,289,244,295,276,103,277,293,92,241,315,125,245,2,264,251,86,78,3,85,80,77,131,270,182,157,181,169,194,185,4])). % 61.23/61.37 cnf(361,plain, % 61.23/61.37 (P7(a31,a31)), % 61.23/61.37 inference(scs_inference,[],[89,97,278,299,307,98,281,279,335,283,301,289,244,295,276,103,277,293,92,241,315,125,245,2,264,251,86,78,3,85,80,77,131,270,182,157,181,169,194,185,4,260,81])). % 61.23/61.37 cnf(365,plain, % 61.23/61.37 (P1(f2(f4(a31)))), % 61.23/61.37 inference(scs_inference,[],[339,245])). % 61.23/61.37 cnf(367,plain, % 61.23/61.37 (P9(f4(a31),f4(a31))), % 61.23/61.37 inference(scs_inference,[],[339,245,125])). % 61.23/61.37 cnf(369,plain, % 61.23/61.37 (E(f34(a42),f32(a37,a38))), % 61.23/61.37 inference(scs_inference,[],[339,100,245,125,2])). % 61.23/61.37 cnf(370,plain, % 61.23/61.37 (P3(f4(a31),f2(f39(f4(a31))))), % 61.23/61.37 inference(scs_inference,[],[339,100,245,125,2,264])). % 61.23/61.37 cnf(372,plain, % 61.23/61.37 (P1(f32(f32(f2(a1),a1),a1))), % 61.23/61.37 inference(scs_inference,[],[97,339,331,100,245,125,2,264,251])). % 61.23/61.37 cnf(374,plain, % 61.23/61.37 (~E(f39(a38),a1)), % 61.23/61.37 inference(scs_inference,[],[97,339,307,331,344,100,245,125,2,264,251,86])). % 61.23/61.37 cnf(375,plain, % 61.23/61.37 (P7(f23(a31,a1),f2(a1))), % 61.23/61.37 inference(scs_inference,[],[97,278,339,307,331,344,353,100,245,125,2,264,251,86,81])). % 61.23/61.37 cnf(377,plain, % 61.23/61.37 (~P3(x3771,f2(a1))), % 61.23/61.37 inference(rename_variables,[],[279])). % 61.23/61.37 cnf(382,plain, % 61.23/61.37 (P9(f39(f4(a31)),f39(f4(a31)))), % 61.23/61.37 inference(scs_inference,[],[97,278,323,346,328,339,307,301,331,351,344,279,289,358,353,100,276,245,125,2,264,251,86,81,78,3,85,77,80,182])). % 61.23/61.37 cnf(384,plain, % 61.23/61.37 (P7(f2(a1),f32(f2(a1),a1))), % 61.23/61.37 inference(scs_inference,[],[97,278,323,346,328,339,307,301,331,351,344,279,377,289,283,358,353,100,276,245,125,2,264,251,86,81,78,3,85,77,80,182,162])). % 61.23/61.37 cnf(389,plain, % 61.23/61.37 (P7(f10(f2(a1),a1,f2(a1)),f2(a1))), % 61.23/61.37 inference(scs_inference,[],[97,278,323,346,328,339,307,301,331,351,344,279,377,289,283,358,353,100,295,276,245,125,2,264,251,86,81,78,3,85,77,80,182,162,181,214])). % 61.23/61.37 cnf(391,plain, % 61.23/61.37 (P7(f23(a31,f4(a31)),a31)), % 61.23/61.37 inference(scs_inference,[],[97,278,323,346,328,339,307,301,331,351,344,279,377,289,283,358,353,100,295,92,241,276,245,125,2,264,251,86,81,78,3,85,77,80,182,162,181,214,194])). % 61.23/61.37 cnf(393,plain, % 61.23/61.37 (P7(a31,f32(f2(a1),a1))), % 61.23/61.37 inference(scs_inference,[],[97,278,323,346,328,339,307,301,331,351,344,279,377,289,283,338,358,353,100,295,92,241,276,245,125,2,264,251,86,81,78,3,85,77,80,182,162,181,214,194,175])). % 61.23/61.37 cnf(400,plain, % 61.23/61.37 (P1(f32(f2(f4(a31)),a1))), % 61.23/61.37 inference(scs_inference,[],[97,365,251])). % 61.23/61.37 cnf(403,plain, % 61.23/61.37 (P9(f4(a31),a1)), % 61.23/61.37 inference(scs_inference,[],[89,97,367,365,389,276,251,81,86])). % 61.23/61.37 cnf(405,plain, % 61.23/61.37 (~P3(x4051,f2(a1))), % 61.23/61.37 inference(rename_variables,[],[279])). % 61.23/61.37 cnf(409,plain, % 61.23/61.37 (P3(a1,f2(f39(f4(a31))))), % 61.23/61.37 inference(scs_inference,[],[89,97,278,334,355,305,367,365,329,370,281,279,314,389,276,251,81,86,78,85,3,80,77])). % 61.23/61.37 cnf(413,plain, % 61.23/61.37 (P7(f10(f2(a1),a1,a31),f2(a1))), % 61.23/61.37 inference(scs_inference,[],[89,97,278,334,355,305,367,365,329,370,281,279,405,283,314,389,393,92,276,251,81,86,78,85,3,80,77,162,214])). % 61.23/61.37 cnf(424,plain, % 61.23/61.37 (~E(f39(f4(a31)),a1)), % 61.23/61.37 inference(scs_inference,[],[339,355,382,372,251,86])). % 61.23/61.37 cnf(425,plain, % 61.23/61.37 (P7(f23(a31,f4(a31)),f2(a1))), % 61.23/61.37 inference(scs_inference,[],[278,339,355,382,372,391,251,86,81])). % 61.23/61.37 cnf(429,plain, % 61.23/61.37 (~E(f39(a38),f4(a31))), % 61.23/61.37 inference(scs_inference,[],[278,339,299,355,409,382,372,244,276,391,374,403,251,86,81,78,85,3])). % 61.23/61.37 cnf(444,plain, % 61.23/61.37 (P7(f10(f2(a1),a1,a31),a31)), % 61.23/61.37 inference(scs_inference,[],[89,413,81])). % 61.23/61.37 cnf(446,plain, % 61.23/61.37 (~E(f39(f4(a31)),f4(a31))), % 61.23/61.37 inference(scs_inference,[],[89,305,276,361,413,424,81,80,3])). % 61.23/61.37 cnf(461,plain, % 61.23/61.37 (P1(f32(f32(f2(f4(a31)),a1),f4(a31)))), % 61.23/61.37 inference(scs_inference,[],[339,400,251])). % 61.23/61.37 cnf(480,plain, % 61.23/61.37 (P7(f2(a1),f32(f32(f2(f4(a31)),a1),f4(a31)))), % 61.23/61.37 inference(scs_inference,[],[355,346,279,461,283,403,375,85,80,162])). % 61.23/61.37 cnf(495,plain, % 61.23/61.37 (P1(f32(f32(a33,a1),a1))), % 61.23/61.37 inference(scs_inference,[],[97,287,251])). % 61.23/61.37 cnf(499,plain, % 61.23/61.37 (P7(f2(a1),f32(a33,a1))), % 61.23/61.37 inference(scs_inference,[],[97,307,305,281,279,287,283,444,251,85,80,162])). % 61.23/61.37 cnf(502,plain, % 61.23/61.37 (P7(f10(a33,a1,f2(a1)),a33)), % 61.23/61.37 inference(scs_inference,[],[97,307,305,281,279,287,283,444,295,90,251,85,80,162,214])). % 61.23/61.37 cnf(517,plain, % 61.23/61.37 (P1(f32(f32(f32(a33,a1),a1),a1))), % 61.23/61.37 inference(scs_inference,[],[97,495,251])). % 61.23/61.37 cnf(540,plain, % 61.23/61.37 (~E(f23(a31,a1),a33)), % 61.23/61.37 inference(scs_inference,[],[339,305,517,353,251,80])). % 61.23/61.37 cnf(587,plain, % 61.23/61.37 (P1(f32(f2(a38),a1))), % 61.23/61.37 inference(scs_inference,[],[97,326,251])). % 61.23/61.37 cnf(606,plain, % 61.23/61.37 (P1(f32(f32(f2(a38),a1),a1))), % 61.23/61.37 inference(scs_inference,[],[97,587,251])). % 61.23/61.37 cnf(609,plain, % 61.23/61.37 (P7(f2(a1),f32(f2(a38),a1))), % 61.23/61.37 inference(scs_inference,[],[97,346,279,587,283,413,251,80,162])). % 61.23/61.37 cnf(622,plain, % 61.23/61.37 (P1(f32(f32(f32(f2(a38),a1),a1),f4(a31)))), % 61.23/61.37 inference(scs_inference,[],[339,606,251])). % 61.23/61.37 cnf(624,plain, % 61.23/61.37 (P7(f2(a1),f32(f32(f2(a38),a1),a1))), % 61.23/61.37 inference(scs_inference,[],[339,279,606,283,251,162])). % 61.23/61.37 cnf(629,plain, % 61.23/61.37 (P7(a31,f32(f32(f2(a38),a1),a1))), % 61.23/61.37 inference(scs_inference,[],[97,339,609,279,606,326,283,338,295,241,251,162,214,175])). % 61.23/61.37 cnf(635,plain, % 61.23/61.37 (P7(f2(a1),x6351)+~E(f32(f2(a1),a1),x6351)), % 61.23/61.37 inference(scs_inference,[],[97,339,328,369,384,609,344,279,606,326,283,338,276,295,241,251,162,214,175,84,76,85,82,81])). % 61.23/61.37 cnf(652,plain, % 61.23/61.37 (~P4(a1)+P4(f4(a31))), % 61.23/61.37 inference(scs_inference,[],[97,328,369,624,382,279,622,587,283,338,276,100,295,241,162,214,175,84,76,85,79,82,83])). % 61.23/61.37 cnf(669,plain, % 61.23/61.37 (~P4(f4(a31))+P4(a1)), % 61.23/61.37 inference(scs_inference,[],[97,480,587,276,100,629,92,214,84,81,83])). % 61.23/61.37 cnf(815,plain, % 61.23/61.37 (P4(f4(f34(a42)))), % 61.23/61.37 inference(scs_inference,[],[96,109,108])). % 61.23/61.37 cnf(818,plain, % 61.23/61.37 (E(f2(a1),f29(f2(a1),f4(f34(a42))))), % 61.23/61.37 inference(scs_inference,[],[279,331,283,815,342,262,219])). % 61.23/61.37 cnf(822,plain, % 61.23/61.37 (E(f29(f2(a1),f4(f34(a42))),f2(a1))), % 61.23/61.37 inference(scs_inference,[],[279,331,283,815,342,262,219,2])). % 61.23/61.37 cnf(823,plain, % 61.23/61.37 (P1(f29(f2(a1),f4(f34(a42))))), % 61.23/61.37 inference(scs_inference,[],[97,279,331,283,815,342,262,219,2,121])). % 61.23/61.37 cnf(825,plain, % 61.23/61.37 (E(a31,f29(f2(a1),f4(f34(a42))))), % 61.23/61.37 inference(scs_inference,[],[97,278,279,331,283,815,342,262,219,2,121,3])). % 61.23/61.37 cnf(826,plain, % 61.23/61.37 (P5(f29(f2(a1),f4(f34(a42))))), % 61.23/61.37 inference(scs_inference,[],[97,278,279,331,283,815,342,295,262,219,2,121,3,79])). % 61.23/61.37 cnf(839,plain, % 61.23/61.37 (~P3(x8391,f29(f2(a1),f4(f34(a42))))), % 61.23/61.37 inference(scs_inference,[],[339,334,822,825,279,823,283,826,815,293,2,251,3,131,262])). % 61.23/61.37 cnf(859,plain, % 61.23/61.37 (~P3(x8591,f29(a31,f4(f34(a42))))), % 61.23/61.37 inference(scs_inference,[],[97,839,244,815,241,78,262])). % 61.23/61.37 cnf(888,plain, % 61.23/61.37 (P1(f32(f32(f2(a1),a1),a38))), % 61.23/61.37 inference(scs_inference,[],[98,331,251])). % 61.23/61.37 cnf(1016,plain, % 61.23/61.37 (P3(f40(a33),a33)), % 61.23/61.37 inference(scs_inference,[],[90,285,111,249])). % 61.23/61.37 cnf(1021,plain, % 61.23/61.37 (P3(f40(a33),f2(f39(f40(a33))))), % 61.23/61.37 inference(scs_inference,[],[1016,125,245,264])). % 61.23/61.37 cnf(1027,plain, % 61.23/61.37 (P9(f39(f40(a33)),f39(f40(a33)))), % 61.23/61.37 inference(scs_inference,[],[1016,331,125,245,264,251,181,182])). % 61.23/61.37 cnf(1187,plain, % 61.23/61.37 (P7(a31,x11871)+~E(f32(f2(a1),a1),x11871)), % 61.23/61.37 inference(scs_inference,[],[393,81])). % 61.23/61.37 cnf(1895,plain, % 61.23/61.37 (P3(f40(a37),a33)), % 61.23/61.37 inference(scs_inference,[],[90,818,825,339,296,323,99,375,80,81,251,157])). % 61.23/61.37 cnf(1897,plain, % 61.23/61.37 (~P9(f39(f40(a37)),a1)), % 61.23/61.37 inference(scs_inference,[],[90,97,818,825,822,339,296,323,839,99,375,80,81,251,157,185])). % 61.23/61.37 cnf(1905,plain, % 61.23/61.37 (P3(f40(a37),f2(f39(f40(a37))))), % 61.23/61.37 inference(scs_inference,[],[90,97,818,825,822,339,296,323,839,99,375,80,81,251,157,185,125,245,86,264])). % 61.23/61.37 cnf(1920,plain, % 61.23/61.37 (P9(a1,f40(a37))), % 61.23/61.37 inference(scs_inference,[],[90,97,818,1016,499,1897,1895,425,80,251,81,169])). % 61.23/61.37 cnf(2294,plain, % 61.23/61.37 (P1(f32(a36,a1))), % 61.23/61.37 inference(scs_inference,[],[91,97,251])). % 61.23/61.37 cnf(2296,plain, % 61.23/61.37 (~P7(a33,a36)), % 61.23/61.37 inference(scs_inference,[],[91,97,293,93,251,131])). % 61.23/61.37 cnf(2298,plain, % 61.23/61.37 (~P3(a33,f32(a36,a1))), % 61.23/61.37 inference(scs_inference,[],[91,97,293,93,251,131,270])). % 61.23/61.37 cnf(2335,plain, % 61.23/61.37 (P1(f32(a36,a38))), % 61.23/61.37 inference(scs_inference,[],[91,98,251])). % 61.23/61.37 cnf(2339,plain, % 61.23/61.37 (~P3(a33,f32(a36,a38))), % 61.23/61.37 inference(scs_inference,[],[91,98,2294,2298,2296,815,251,262,270])). % 61.23/61.37 cnf(2370,plain, % 61.23/61.37 (P1(f32(a36,f40(a33)))), % 61.23/61.37 inference(scs_inference,[],[91,1016,251])). % 61.23/61.37 cnf(2374,plain, % 61.23/61.37 (~P3(a33,f32(a36,f40(a33)))), % 61.23/61.37 inference(scs_inference,[],[91,1016,2335,2296,2339,815,251,262,270])). % 61.23/61.37 cnf(2381,plain, % 61.23/61.37 (P1(f32(a36,f4(a31)))), % 61.23/61.37 inference(scs_inference,[],[91,339,251])). % 61.23/61.37 cnf(2385,plain, % 61.23/61.37 (~P3(a33,f32(a36,f4(a31)))), % 61.23/61.37 inference(scs_inference,[],[91,339,2370,2296,2374,815,251,262,270])). % 61.23/61.37 cnf(2392,plain, % 61.23/61.37 (P1(f32(a36,f40(a37)))), % 61.23/61.37 inference(scs_inference,[],[91,1895,251])). % 61.23/61.37 cnf(2396,plain, % 61.23/61.37 (~P3(a33,f32(a36,f40(a37)))), % 61.23/61.37 inference(scs_inference,[],[91,1895,2381,2296,2385,815,251,262,270])). % 61.23/61.37 cnf(2505,plain, % 61.23/61.37 (P4(a1)), % 61.23/61.37 inference(scs_inference,[],[241,669,109])). % 61.23/61.37 cnf(2506,plain, % 61.23/61.37 (P4(f4(a31))), % 61.23/61.37 inference(scs_inference,[],[2505,652])). % 61.23/61.37 cnf(2513,plain, % 61.23/61.37 (P3(a1,f28(a33,a1))), % 61.23/61.37 inference(scs_inference,[],[97,279,331,283,90,2505,358,342,262,265,268])). % 61.23/61.37 cnf(2517,plain, % 61.23/61.38 (P3(f4(a31),f28(a33,a1))), % 61.23/61.38 inference(scs_inference,[],[97,328,859,279,331,283,90,2505,358,342,262,265,268,78,77])). % 61.23/61.38 cnf(2522,plain, % 61.23/61.38 (~P3(x25221,f29(f2(a1),f4(f34(a42))))), % 61.23/61.38 inference(rename_variables,[],[839])). % 61.23/61.38 cnf(2526,plain, % 61.23/61.38 (~P3(x25261,f2(a1))), % 61.23/61.38 inference(rename_variables,[],[279])). % 61.23/61.38 cnf(2528,plain, % 61.23/61.38 (P3(f4(a31),f28(a33,f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[339,2517,446,839,279,331,283,90,2506,342,78,262,265,268])). % 61.23/61.38 cnf(2530,plain, % 61.23/61.38 (E(f2(a1),f29(f29(f2(a1),f4(f34(a42))),f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[339,2517,446,839,2522,279,2526,331,283,823,90,2506,342,78,262,265,268,219])). % 61.23/61.38 cnf(2534,plain, % 61.23/61.38 (P3(a1,f28(a33,f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[339,2517,446,839,2522,279,2526,331,283,823,276,90,2506,342,78,262,265,268,219,77])). % 61.23/61.38 cnf(2538,plain, % 61.23/61.38 (E(f29(f29(f2(a1),f4(f34(a42))),f4(a31)),f2(a1))), % 61.23/61.38 inference(scs_inference,[],[2530,2])). % 61.23/61.38 cnf(2541,plain, % 61.23/61.38 (E(a31,f29(f29(f2(a1),f4(f34(a42))),f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[278,2530,2528,859,2,78,3])). % 61.23/61.38 cnf(2542,plain, % 61.23/61.38 (P1(f29(f29(f2(a1),f4(f34(a42))),f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[97,278,2530,2528,859,2,78,3,121])). % 61.23/61.38 cnf(2544,plain, % 61.23/61.38 (P5(f29(f29(f2(a1),f4(f34(a42))),f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[97,278,2530,2528,859,295,2,78,3,121,79])). % 61.23/61.38 cnf(2546,plain, % 61.23/61.38 (~P3(x25461,f29(f2(a1),a1))), % 61.23/61.38 inference(scs_inference,[],[97,278,2530,2528,859,279,283,291,2505,295,2,78,3,121,79,82,262])). % 61.23/61.38 cnf(2558,plain, % 61.23/61.38 (~P3(x25581,f29(f2(a1),f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[97,2546,2541,279,283,2506,2,78,262])). % 61.23/61.38 cnf(2563,plain, % 61.23/61.38 (~P3(x25631,f29(f29(f2(a1),f4(f34(a42))),f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[97,429,2546,2541,279,283,2506,2,78,262,265,112])). % 61.23/61.38 cnf(2687,plain, % 61.23/61.38 (~P3(x26871,f29(f2(a1),a1))), % 61.23/61.38 inference(rename_variables,[],[2546])). % 61.23/61.38 cnf(2693,plain, % 61.23/61.38 (~E(f29(f2(a1),a1),f2(f39(f40(a33))))+~P3(f39(f40(a33)),a33)), % 61.23/61.38 inference(scs_inference,[],[1016,2513,2546,2687,244,1027,2392,241,374,2396,2505,78,262,265,185])). % 61.23/61.38 cnf(2713,plain, % 61.23/61.38 (~P3(x27131,f29(a31,a1))), % 61.23/61.38 inference(scs_inference,[],[2528,2546,244,241,2505,78,262])). % 61.23/61.38 cnf(2725,plain, % 61.23/61.38 (~P3(x27251,f29(a31,f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[2558,1021,244,241,2506,78,262])). % 61.23/61.38 cnf(2851,plain, % 61.23/61.38 (~E(f29(f2(a1),f4(a31)),f2(f39(f40(a33))))+~P3(f39(f40(a33)),a33)), % 61.23/61.38 inference(scs_inference,[],[1016,2558,1027,888,99,502,2506,262,256,250,185])). % 61.23/61.38 cnf(2942,plain, % 61.23/61.38 (E(f4(f23(a31,a1)),a1)), % 61.23/61.38 inference(scs_inference,[],[339,97,92,241,119,190])). % 61.23/61.38 cnf(2943,plain, % 61.23/61.38 (E(a1,f4(f23(a31,a1)))), % 61.23/61.38 inference(scs_inference,[],[2942,2])). % 61.23/61.38 cnf(2945,plain, % 61.23/61.38 (P4(f4(f23(a31,a1)))), % 61.23/61.38 inference(scs_inference,[],[2942,374,2505,2,3,83])). % 61.23/61.38 cnf(3125,plain, % 61.23/61.38 (P3(f4(f23(a31,a1)),a33)), % 61.23/61.38 inference(scs_inference,[],[97,98,2943,287,251,77])). % 61.23/61.38 cnf(3128,plain, % 61.23/61.38 (P3(f4(f23(a31,a1)),f28(a33,f4(f23(a31,a1))))), % 61.23/61.38 inference(scs_inference,[],[97,98,2943,1920,287,281,90,2945,251,77,85,86,268])). % 61.23/61.38 cnf(3133,plain, % 61.23/61.38 (P9(f4(f23(a31,a1)),f4(f23(a31,a1)))), % 61.23/61.38 inference(scs_inference,[],[97,98,2538,2943,1920,287,281,2563,90,2945,251,77,85,86,268,185,125])). % 61.23/61.38 cnf(3135,plain, % 61.23/61.38 (P1(f2(f4(f23(a31,a1))))), % 61.23/61.38 inference(scs_inference,[],[97,98,2538,2943,1920,287,281,2563,90,2945,251,77,85,86,268,185,125,245])). % 61.23/61.38 cnf(3148,plain, % 61.23/61.38 (P3(f4(f23(a31,a1)),f2(f39(f4(a31))))), % 61.23/61.38 inference(scs_inference,[],[1016,409,2943,287,351,251,85,77])). % 61.23/61.38 cnf(3149,plain, % 61.23/61.38 (P9(f4(f23(a31,a1)),a1)), % 61.23/61.38 inference(scs_inference,[],[1016,409,2943,287,351,3133,2942,251,85,77,86])). % 61.23/61.38 cnf(3157,plain, % 61.23/61.38 (P3(f4(f23(a31,a1)),f28(a33,a1))), % 61.23/61.38 inference(scs_inference,[],[339,2513,2943,287,251,77])). % 61.23/61.38 cnf(3160,plain, % 61.23/61.38 (P7(f23(a31,f4(f23(a31,a1))),a31)), % 61.23/61.38 inference(scs_inference,[],[92,339,2513,2943,3125,287,241,403,333,251,77,86,85,194])). % 61.23/61.38 cnf(3182,plain, % 61.23/61.38 (P3(f4(f23(a31,a1)),f28(a33,f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[307,2534,2943,1895,287,3149,251,85,77])). % 61.23/61.38 cnf(3191,plain, % 61.23/61.38 (P3(a1,f28(a33,f4(f23(a31,a1))))), % 61.23/61.38 inference(scs_inference,[],[3125,3128,287,2942,251,77])). % 61.23/61.38 cnf(3199,plain, % 61.23/61.38 (P3(f4(f23(a31,a1)),f2(f39(a1)))), % 61.23/61.38 inference(scs_inference,[],[355,2943,289,3149,85,77])). % 61.23/61.38 cnf(3798,plain, % 61.23/61.38 (~P7(f2(f39(f4(a31))),f2(a1))), % 61.23/61.38 inference(scs_inference,[],[97,2725,1895,3148,278,283,279,3160,251,78,81,157])). % 61.23/61.38 cnf(3801,plain, % 61.23/61.38 (~P3(f2(f39(a1)),f32(f2(a1),a1))), % 61.23/61.38 inference(scs_inference,[],[97,2725,1895,3148,278,346,283,279,3160,251,78,81,157,270])). % 61.23/61.38 cnf(3820,plain, % 61.23/61.38 (~P7(f28(a33,f4(f23(a31,a1))),f2(a1))), % 61.23/61.38 inference(scs_inference,[],[97,2713,3128,98,3798,283,331,301,279,3801,2505,251,78,80,262,157])). % 61.23/61.38 cnf(3835,plain, % 61.23/61.38 (P1(f32(f2(a1),f40(a33)))), % 61.23/61.38 inference(scs_inference,[],[1016,283,251])). % 61.23/61.38 cnf(3840,plain, % 61.23/61.38 (~P7(f28(a33,a1),f2(a1))), % 61.23/61.38 inference(scs_inference,[],[2725,3199,3157,1016,3820,283,301,279,251,78,80,157])). % 61.23/61.38 cnf(3854,plain, % 61.23/61.38 (P1(f32(f2(a1),f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[339,283,251])). % 61.23/61.38 cnf(3859,plain, % 61.23/61.38 (~P7(f28(a33,f4(a31)),f2(a1))), % 61.23/61.38 inference(scs_inference,[],[2713,3199,3182,339,3840,283,301,279,251,78,80,157])). % 61.23/61.38 cnf(3862,plain, % 61.23/61.38 (~P3(f28(a33,a1),f32(f2(a1),a1))), % 61.23/61.38 inference(scs_inference,[],[97,2713,3199,3182,339,3840,283,301,279,251,78,80,157,270])). % 61.23/61.38 cnf(3873,plain, % 61.23/61.38 (P1(f32(f2(a1),f4(f23(a31,a1))))), % 61.23/61.38 inference(scs_inference,[],[3125,283,251])). % 61.23/61.38 cnf(3880,plain, % 61.23/61.38 (~P7(a37,f2(a1))), % 61.23/61.38 inference(scs_inference,[],[2725,3148,323,3125,3859,283,331,301,279,3862,2506,251,78,80,262,157])). % 61.23/61.38 cnf(3883,plain, % 61.23/61.38 (~P3(f28(a33,f4(a31)),f32(f2(a1),a1))), % 61.23/61.38 inference(scs_inference,[],[97,2725,3148,323,3125,3859,283,331,301,279,3862,2506,251,78,80,262,157,270])). % 61.23/61.38 cnf(3903,plain, % 61.23/61.38 (~P7(f2(f39(a38)),f2(a1))), % 61.23/61.38 inference(scs_inference,[],[2713,3148,3880,283,331,301,329,279,3883,2505,78,80,262,157])). % 61.23/61.38 cnf(3915,plain, % 61.23/61.38 (~P7(f2(f39(f40(a33))),f2(a1))), % 61.23/61.38 inference(scs_inference,[],[2725,3128,3903,283,301,279,1021,80,78,157])). % 61.23/61.38 cnf(3932,plain, % 61.23/61.38 (~P7(f2(f39(f40(a37))),f2(a1))), % 61.23/61.38 inference(scs_inference,[],[2713,3128,3915,283,301,279,1905,78,80,157])). % 61.23/61.38 cnf(3961,plain, % 61.23/61.38 (~P3(x39611,f29(f32(f2(a1),f40(a33)),a1))+P3(x39611,f32(f2(a1),f40(a33)))), % 61.23/61.38 inference(scs_inference,[],[2713,1895,3157,3798,283,3835,375,2505,78,80,270,262])). % 61.23/61.38 cnf(3969,plain, % 61.23/61.38 (~P3(x39691,f29(f32(f2(a1),f4(a31)),f4(f23(a31,a1))))+P3(x39691,f32(f2(a1),f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[1895,2725,3182,3840,283,3854,375,2945,80,78,270,262])). % 61.23/61.38 cnf(4015,plain, % 61.23/61.38 (~P3(x40151,f29(f32(f2(a1),f40(a33)),f4(f23(a31,a1))))+P3(x40151,f32(f2(a1),f40(a33)))), % 61.23/61.38 inference(scs_inference,[],[1895,2725,3903,283,329,3835,375,2945,80,78,270,262])). % 61.23/61.38 cnf(4033,plain, % 61.23/61.38 (~P3(x40331,f29(f32(f2(a1),f4(a31)),f4(a31)))+P3(x40331,f32(f2(a1),f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[1895,2725,3932,283,1021,3854,375,2506,78,80,270,262])). % 61.23/61.38 cnf(4041,plain, % 61.23/61.38 (~P3(x40411,f29(f32(f2(a1),f4(a31)),a1))+P3(x40411,f32(f2(a1),f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[2713,98,3798,283,1021,3854,389,2505,78,80,270,262])). % 61.23/61.38 cnf(4114,plain, % 61.23/61.38 (~P3(x41141,f29(f32(f2(a1),f40(a33)),f4(a31)))+P3(x41141,f32(f2(a1),f40(a33)))), % 61.23/61.38 inference(scs_inference,[],[98,3932,283,3835,413,2506,80,270,262])). % 61.23/61.38 cnf(4130,plain, % 61.23/61.38 (~P3(f28(a33,a1),f32(f2(a1),f40(a33)))), % 61.23/61.38 inference(scs_inference,[],[1016,3840,283,389,80,270])). % 61.23/61.38 cnf(4156,plain, % 61.23/61.38 (~P3(f28(a33,f4(f23(a31,a1))),f32(f2(a1),f40(a33)))), % 61.23/61.38 inference(scs_inference,[],[1016,3820,283,425,80,270])). % 61.23/61.38 cnf(4158,plain, % 61.23/61.38 (~E(f29(a31,f4(a31)),f2(f39(f40(a33))))+~P3(f39(f40(a33)),a33)), % 61.23/61.38 inference(scs_inference,[],[2725,1016,3820,283,1027,425,80,270,185])). % 61.23/61.38 cnf(4170,plain, % 61.23/61.38 (~E(f29(a31,a1),f2(f39(f40(a33))))+~P3(f39(f40(a33)),a33)), % 61.23/61.38 inference(scs_inference,[],[2713,1016,3880,283,1027,3835,389,4130,815,80,262,270,4015,185])). % 61.23/61.38 cnf(4178,plain, % 61.23/61.38 (~P3(f2(f39(a38)),f32(f2(a1),f40(a33)))), % 61.23/61.38 inference(scs_inference,[],[1016,3903,283,3835,413,4130,2505,80,262,270])). % 61.23/61.38 cnf(4213,plain, % 61.23/61.38 (~P3(f28(a33,a1),f32(f2(a1),f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[339,3840,283,425,80,270])). % 61.23/61.38 cnf(4217,plain, % 61.23/61.38 (~P3(x42171,f29(f32(f2(a1),f4(f23(a31,a1))),f4(a31)))+P3(x42171,f32(f2(a1),f4(f23(a31,a1))))), % 61.23/61.38 inference(scs_inference,[],[339,3840,283,3873,425,2506,80,270,3969,262])). % 61.23/61.38 cnf(4230,plain, % 61.23/61.38 (~P3(f28(a33,f4(f23(a31,a1))),f32(f2(a1),f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[339,3820,283,3854,413,4213,2505,80,262,270])). % 61.23/61.38 cnf(4254,plain, % 61.23/61.38 (~P3(f2(f39(a38)),f32(f2(a1),f4(a31)))), % 61.23/61.38 inference(scs_inference,[],[339,3903,283,3854,389,4213,2506,80,262,270])). % 61.23/61.38 cnf(4307,plain, % 61.23/61.38 (P9(f4(f23(a31,a1)),f39(a1))), % 61.23/61.38 inference(scs_inference,[],[97,2943,127,85])). % 61.23/61.38 cnf(4308,plain, % 61.23/61.38 (P9(a1,f39(a1))), % 61.23/61.38 inference(scs_inference,[],[2942,4307,85])). % 61.23/61.38 cnf(4329,plain, % 61.23/61.38 (~P3(a37,f32(f2(a1),f4(f23(a31,a1))))), % 61.23/61.38 inference(scs_inference,[],[3125,3880,283,338,80,270])). % 61.23/61.38 cnf(4419,plain, % 61.23/61.38 (P8(f4(f23(a31,a1)),f39(a1))), % 61.23/61.38 inference(scs_inference,[],[97,2943,128,87])). % 61.23/61.38 cnf(4420,plain, % 61.23/61.38 (P8(a1,f39(a1))), % 61.23/61.38 inference(scs_inference,[],[2942,4419,87])). % 61.23/61.38 cnf(4570,plain, % 61.23/61.38 (P3(f4(a31),f28(a33,f4(f23(a31,a1))))), % 61.23/61.38 inference(scs_inference,[],[3191,328,4308,4420,87,85,77])). % 61.23/61.38 cnf(4749,plain, % 61.23/61.38 (P1(f26(a42,a1))), % 61.23/61.38 inference(scs_inference,[],[89,540,4178,4254,4329,2542,4570,3135,1016,2505,96,111,109,117,119,115,127,128,113,114,126,137,7,13,25,35,41,56,63,67,118,5,6,11,12,14,15,16,17,18,19,21,22,23,24,36,37,45,46,47,48,49,50,51,52,68,69,70,71,1187,8,9,10,26,27,28,29,30,31,32,33,34,38,39,40,42,43,44,53,54,55,57,58,59,60,61,62,64,65,66,635,72,73,74,75,4170,2693,4158,2851,3961,4041,4033,4114,4217,20,2,4,112,246,247,248])). % 61.23/61.38 cnf(4761,plain, % 61.23/61.38 (P3(f16(a38),a33)), % 61.23/61.38 inference(scs_inference,[],[89,540,4178,4254,4329,2542,2544,4570,3135,103,92,296,1016,2505,98,96,283,111,109,117,119,115,127,128,113,114,126,137,7,13,25,35,41,56,63,67,118,5,6,11,12,14,15,16,17,18,19,21,22,23,24,36,37,45,46,47,48,49,50,51,52,68,69,70,71,1187,8,9,10,26,27,28,29,30,31,32,33,34,38,39,40,42,43,44,53,54,55,57,58,59,60,61,62,64,65,66,635,72,73,74,75,4170,2693,4158,2851,3961,4041,4033,4114,4217,20,2,4,112,246,247,248,122,105,136,147,146,129])). % 61.23/61.38 cnf(4765,plain, % 61.23/61.38 (E(f39(f16(a38)),a38)), % 61.23/61.38 inference(scs_inference,[],[89,540,4178,4254,4329,2542,2544,4570,3135,103,92,296,1016,2505,90,98,96,283,111,109,117,119,115,127,128,113,114,126,137,7,13,25,35,41,56,63,67,118,5,6,11,12,14,15,16,17,18,19,21,22,23,24,36,37,45,46,47,48,49,50,51,52,68,69,70,71,1187,8,9,10,26,27,28,29,30,31,32,33,34,38,39,40,42,43,44,53,54,55,57,58,59,60,61,62,64,65,66,635,72,73,74,75,4170,2693,4158,2851,3961,4041,4033,4114,4217,20,2,4,112,246,247,248,122,105,136,147,146,129,165,120])). % 61.23/61.38 cnf(5180,plain, % 61.23/61.38 ($false), % 61.23/61.38 inference(scs_inference,[],[4749,4761,4230,4156,4765,115,118,117,119,128,4033,111,4114,114]), % 61.23/61.38 ['proof']). % 61.23/61.38 % SZS output end Proof % 61.23/61.38 % Total time :60.580000s %------------------------------------------------------------------------------