%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM539+2 : 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 : n020.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:24:54 EDT 2024 % Result : Theorem 58.99s 59.65s % Output : CNFRefutation 58.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : NUM539+2 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sat Jun 22 23:39:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.48/0.57 start to proof:theBenchmark % 58.89/59.63 %------------------------------------------- % 58.89/59.63 % File :CSE---1.7 % 58.89/59.63 % Problem :theBenchmark % 58.89/59.63 % Transform :cnf % 58.89/59.63 % Format :tptp:raw % 58.89/59.63 % Command :java -jar mcs_scs.jar %d %s % 58.89/59.63 % 58.89/59.63 % Result :Theorem 58.320000s % 58.89/59.63 % Output :CNFRefutation 58.320000s % 58.89/59.63 %------------------------------------------- % 58.89/59.64 %------------------------------------------------------------------------------ % 58.89/59.64 % File : NUM539+2 : TPTP v8.2.0. Released v4.0.0. % 58.89/59.64 % Domain : Number Theory % 58.89/59.64 % Problem : Ramsey's Infinite Theorem 07, 01 expansion % 58.89/59.64 % Version : Especial. % 58.89/59.64 % English : % 58.89/59.64 % 58.89/59.64 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 58.89/59.64 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 58.89/59.64 % Source : [Pas08] % 58.89/59.64 % Names : ramsey_07.01 [Pas08] % 58.89/59.64 % 58.89/59.64 % Status : Theorem % 58.89/59.64 % Rating : 0.17 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.2.0, 0.16 v6.1.0, 0.20 v6.0.0, 0.17 v5.5.0, 0.22 v5.4.0, 0.29 v5.3.0, 0.33 v5.2.0, 0.20 v5.1.0, 0.29 v5.0.0, 0.38 v4.1.0, 0.43 v4.0.1, 0.65 v4.0.0 % 58.89/59.64 % Syntax : Number of formulae : 51 ( 2 unt; 6 def) % 58.89/59.64 % Number of atoms : 203 ( 28 equ) % 58.89/59.64 % Maximal formula atoms : 12 ( 3 avg) % 58.89/59.64 % Number of connectives : 167 ( 15 ~; 6 |; 59 &) % 58.89/59.64 % ( 11 <=>; 76 =>; 0 <=; 0 <~>) % 58.89/59.64 % Maximal formula depth : 12 ( 5 avg) % 58.89/59.64 % Maximal term depth : 4 ( 1 avg) % 58.89/59.64 % Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty) % 58.89/59.64 % Number of functors : 11 ( 11 usr; 5 con; 0-2 aty) % 58.89/59.64 % Number of variables : 91 ( 86 !; 5 ?) % 58.89/59.64 % SPC : FOF_THM_RFO_SEQ % 58.89/59.64 % 58.89/59.64 % Comments : Problem generated by the SAD system [VLP07] % 58.89/59.64 %------------------------------------------------------------------------------ % 58.89/59.64 fof(mSetSort,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aSet0(W0) % 58.89/59.64 => $true ) ). % 58.89/59.64 % 58.89/59.64 fof(mElmSort,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aElement0(W0) % 58.89/59.64 => $true ) ). % 58.89/59.64 % 58.89/59.64 fof(mEOfElem,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aSet0(W0) % 58.89/59.64 => ! [W1] : % 58.89/59.64 ( aElementOf0(W1,W0) % 58.89/59.64 => aElement0(W1) ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mFinRel,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aSet0(W0) % 58.89/59.64 => ( isFinite0(W0) % 58.89/59.64 => $true ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mDefEmp,definition, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( W0 = slcrc0 % 58.89/59.64 <=> ( aSet0(W0) % 58.89/59.64 & ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mEmpFin,axiom, % 58.89/59.64 isFinite0(slcrc0) ). % 58.89/59.64 % 58.89/59.64 fof(mCntRel,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aSet0(W0) % 58.89/59.64 => ( isCountable0(W0) % 58.89/59.64 => $true ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mCountNFin,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( ( aSet0(W0) % 58.89/59.64 & isCountable0(W0) ) % 58.89/59.64 => ~ isFinite0(W0) ) ). % 58.89/59.64 % 58.89/59.64 fof(mCountNFin_01,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( ( aSet0(W0) % 58.89/59.64 & isCountable0(W0) ) % 58.89/59.64 => W0 != slcrc0 ) ). % 58.89/59.64 % 58.89/59.64 fof(mDefSub,definition, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aSet0(W0) % 58.89/59.64 => ! [W1] : % 58.89/59.64 ( aSubsetOf0(W1,W0) % 58.89/59.64 <=> ( aSet0(W1) % 58.89/59.64 & ! [W2] : % 58.89/59.64 ( aElementOf0(W2,W1) % 58.89/59.64 => aElementOf0(W2,W0) ) ) ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mSubFSet,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( ( aSet0(W0) % 58.89/59.64 & isFinite0(W0) ) % 58.89/59.64 => ! [W1] : % 58.89/59.64 ( aSubsetOf0(W1,W0) % 58.89/59.64 => isFinite0(W1) ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mSubRefl,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aSet0(W0) % 58.89/59.64 => aSubsetOf0(W0,W0) ) ). % 58.89/59.64 % 58.89/59.64 fof(mSubASymm,axiom, % 58.89/59.64 ! [W0,W1] : % 58.89/59.64 ( ( aSet0(W0) % 58.89/59.64 & aSet0(W1) ) % 58.89/59.64 => ( ( aSubsetOf0(W0,W1) % 58.89/59.64 & aSubsetOf0(W1,W0) ) % 58.89/59.64 => W0 = W1 ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mSubTrans,axiom, % 58.89/59.64 ! [W0,W1,W2] : % 58.89/59.64 ( ( aSet0(W0) % 58.89/59.64 & aSet0(W1) % 58.89/59.64 & aSet0(W2) ) % 58.89/59.64 => ( ( aSubsetOf0(W0,W1) % 58.89/59.64 & aSubsetOf0(W1,W2) ) % 58.89/59.64 => aSubsetOf0(W0,W2) ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mDefCons,definition, % 58.89/59.64 ! [W0,W1] : % 58.89/59.64 ( ( aSet0(W0) % 58.89/59.64 & aElement0(W1) ) % 58.89/59.64 => ! [W2] : % 58.89/59.64 ( W2 = sdtpldt0(W0,W1) % 58.89/59.64 <=> ( aSet0(W2) % 58.89/59.64 & ! [W3] : % 58.89/59.64 ( aElementOf0(W3,W2) % 58.89/59.64 <=> ( aElement0(W3) % 58.89/59.64 & ( aElementOf0(W3,W0) % 58.89/59.64 | W3 = W1 ) ) ) ) ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mDefDiff,definition, % 58.89/59.64 ! [W0,W1] : % 58.89/59.64 ( ( aSet0(W0) % 58.89/59.64 & aElement0(W1) ) % 58.89/59.64 => ! [W2] : % 58.89/59.64 ( W2 = sdtmndt0(W0,W1) % 58.89/59.64 <=> ( aSet0(W2) % 58.89/59.64 & ! [W3] : % 58.89/59.64 ( aElementOf0(W3,W2) % 58.89/59.64 <=> ( aElement0(W3) % 58.89/59.64 & aElementOf0(W3,W0) % 58.89/59.64 & W3 != W1 ) ) ) ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mConsDiff,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aSet0(W0) % 58.89/59.64 => ! [W1] : % 58.89/59.64 ( aElementOf0(W1,W0) % 58.89/59.64 => sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mDiffCons,axiom, % 58.89/59.64 ! [W0,W1] : % 58.89/59.64 ( ( aElement0(W0) % 58.89/59.64 & aSet0(W1) ) % 58.89/59.64 => ( ~ aElementOf0(W0,W1) % 58.89/59.64 => sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mCConsSet,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aElement0(W0) % 58.89/59.64 => ! [W1] : % 58.89/59.64 ( ( aSet0(W1) % 58.89/59.64 & isCountable0(W1) ) % 58.89/59.64 => isCountable0(sdtpldt0(W1,W0)) ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mCDiffSet,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aElement0(W0) % 58.89/59.64 => ! [W1] : % 58.89/59.64 ( ( aSet0(W1) % 58.89/59.64 & isCountable0(W1) ) % 58.89/59.64 => isCountable0(sdtmndt0(W1,W0)) ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mFConsSet,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aElement0(W0) % 58.89/59.64 => ! [W1] : % 58.89/59.64 ( ( aSet0(W1) % 58.89/59.64 & isFinite0(W1) ) % 58.89/59.64 => isFinite0(sdtpldt0(W1,W0)) ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mFDiffSet,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aElement0(W0) % 58.89/59.64 => ! [W1] : % 58.89/59.64 ( ( aSet0(W1) % 58.89/59.64 & isFinite0(W1) ) % 58.89/59.64 => isFinite0(sdtmndt0(W1,W0)) ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mNATSet,axiom, % 58.89/59.64 ( aSet0(szNzAzT0) % 58.89/59.64 & isCountable0(szNzAzT0) ) ). % 58.89/59.64 % 58.89/59.64 fof(mZeroNum,axiom, % 58.89/59.64 aElementOf0(sz00,szNzAzT0) ). % 58.89/59.64 % 58.89/59.64 fof(mSuccNum,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aElementOf0(W0,szNzAzT0) % 58.89/59.64 => ( aElementOf0(szszuzczcdt0(W0),szNzAzT0) % 58.89/59.64 & szszuzczcdt0(W0) != sz00 ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mSuccEquSucc,axiom, % 58.89/59.64 ! [W0,W1] : % 58.89/59.64 ( ( aElementOf0(W0,szNzAzT0) % 58.89/59.64 & aElementOf0(W1,szNzAzT0) ) % 58.89/59.64 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 58.89/59.64 => W0 = W1 ) ) ). % 58.89/59.64 % 58.89/59.64 fof(mNatExtra,axiom, % 58.89/59.64 ! [W0] : % 58.89/59.64 ( aElementOf0(W0,szNzAzT0) % 58.89/59.65 => ( W0 = sz00 % 58.89/59.65 | ? [W1] : % 58.89/59.65 ( aElementOf0(W1,szNzAzT0) % 58.89/59.65 & W0 = szszuzczcdt0(W1) ) ) ) ). % 58.89/59.65 % 58.89/59.65 fof(mNatNSucc,axiom, % 58.89/59.65 ! [W0] : % 58.89/59.65 ( aElementOf0(W0,szNzAzT0) % 58.89/59.65 => W0 != szszuzczcdt0(W0) ) ). % 58.89/59.65 % 58.89/59.65 fof(mLessRel,axiom, % 58.89/59.65 ! [W0,W1] : % 58.89/59.65 ( ( aElementOf0(W0,szNzAzT0) % 58.89/59.65 & aElementOf0(W1,szNzAzT0) ) % 58.89/59.65 => ( sdtlseqdt0(W0,W1) % 58.89/59.65 => $true ) ) ). % 58.89/59.65 % 58.89/59.65 fof(mZeroLess,axiom, % 58.89/59.65 ! [W0] : % 58.89/59.65 ( aElementOf0(W0,szNzAzT0) % 58.89/59.65 => sdtlseqdt0(sz00,W0) ) ). % 58.89/59.65 % 58.89/59.65 fof(mNoScLessZr,axiom, % 58.89/59.65 ! [W0] : % 58.89/59.65 ( aElementOf0(W0,szNzAzT0) % 58.89/59.65 => ~ sdtlseqdt0(szszuzczcdt0(W0),sz00) ) ). % 58.89/59.65 % 58.89/59.65 fof(mSuccLess,axiom, % 58.89/59.65 ! [W0,W1] : % 58.89/59.65 ( ( aElementOf0(W0,szNzAzT0) % 58.89/59.65 & aElementOf0(W1,szNzAzT0) ) % 58.89/59.65 => ( sdtlseqdt0(W0,W1) % 58.89/59.65 <=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ) ). % 58.89/59.65 % 58.89/59.65 fof(mLessSucc,axiom, % 58.89/59.65 ! [W0] : % 58.89/59.65 ( aElementOf0(W0,szNzAzT0) % 58.99/59.65 => sdtlseqdt0(W0,szszuzczcdt0(W0)) ) ). % 58.99/59.65 % 58.99/59.65 fof(mLessRefl,axiom, % 58.99/59.65 ! [W0] : % 58.99/59.65 ( aElementOf0(W0,szNzAzT0) % 58.99/59.65 => sdtlseqdt0(W0,W0) ) ). % 58.99/59.65 % 58.99/59.65 fof(mLessASymm,axiom, % 58.99/59.65 ! [W0,W1] : % 58.99/59.65 ( ( aElementOf0(W0,szNzAzT0) % 58.99/59.65 & aElementOf0(W1,szNzAzT0) ) % 58.99/59.65 => ( ( sdtlseqdt0(W0,W1) % 58.99/59.65 & sdtlseqdt0(W1,W0) ) % 58.99/59.65 => W0 = W1 ) ) ). % 58.99/59.65 % 58.99/59.65 fof(mLessTrans,axiom, % 58.99/59.65 ! [W0,W1,W2] : % 58.99/59.65 ( ( aElementOf0(W0,szNzAzT0) % 58.99/59.65 & aElementOf0(W1,szNzAzT0) % 58.99/59.65 & aElementOf0(W2,szNzAzT0) ) % 58.99/59.65 => ( ( sdtlseqdt0(W0,W1) % 58.99/59.65 & sdtlseqdt0(W1,W2) ) % 58.99/59.65 => sdtlseqdt0(W0,W2) ) ) ). % 58.99/59.65 % 58.99/59.65 fof(mLessTotal,axiom, % 58.99/59.65 ! [W0,W1] : % 58.99/59.65 ( ( aElementOf0(W0,szNzAzT0) % 58.99/59.65 & aElementOf0(W1,szNzAzT0) ) % 58.99/59.65 => ( sdtlseqdt0(W0,W1) % 58.99/59.65 | sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ). % 58.99/59.65 % 58.99/59.65 fof(mIHSort,axiom, % 58.99/59.65 ! [W0,W1] : % 58.99/59.65 ( ( aElementOf0(W0,szNzAzT0) % 58.99/59.65 & aElementOf0(W1,szNzAzT0) ) % 58.99/59.65 => ( iLess0(W0,W1) % 58.99/59.65 => $true ) ) ). % 58.99/59.65 % 58.99/59.65 fof(mIH,axiom, % 58.99/59.65 ! [W0] : % 58.99/59.65 ( aElementOf0(W0,szNzAzT0) % 58.99/59.65 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 58.99/59.65 % 58.99/59.65 fof(mCardS,axiom, % 58.99/59.65 ! [W0] : % 58.99/59.65 ( aSet0(W0) % 58.99/59.65 => aElement0(sbrdtbr0(W0)) ) ). % 58.99/59.65 % 58.99/59.65 fof(mCardNum,axiom, % 58.99/59.65 ! [W0] : % 58.99/59.65 ( aSet0(W0) % 58.99/59.65 => ( aElementOf0(sbrdtbr0(W0),szNzAzT0) % 58.99/59.65 <=> isFinite0(W0) ) ) ). % 58.99/59.65 % 58.99/59.65 fof(mCardEmpty,axiom, % 58.99/59.65 ! [W0] : % 58.99/59.65 ( aSet0(W0) % 58.99/59.65 => ( sbrdtbr0(W0) = sz00 % 58.99/59.65 <=> W0 = slcrc0 ) ) ). % 58.99/59.65 % 58.99/59.65 fof(mCardCons,axiom, % 58.99/59.65 ! [W0] : % 58.99/59.65 ( ( aSet0(W0) % 58.99/59.65 & isFinite0(W0) ) % 58.99/59.65 => ! [W1] : % 58.99/59.65 ( aElement0(W1) % 58.99/59.65 => ( ~ aElementOf0(W1,W0) % 58.99/59.65 => sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ) ). % 58.99/59.65 % 58.99/59.65 fof(mCardDiff,axiom, % 58.99/59.65 ! [W0] : % 58.99/59.65 ( aSet0(W0) % 58.99/59.65 => ! [W1] : % 58.99/59.65 ( ( isFinite0(W0) % 58.99/59.65 & aElementOf0(W1,W0) ) % 58.99/59.65 => szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ) ). % 58.99/59.65 % 58.99/59.65 fof(mCardSub,axiom, % 58.99/59.65 ! [W0] : % 58.99/59.65 ( aSet0(W0) % 58.99/59.65 => ! [W1] : % 58.99/59.65 ( ( isFinite0(W0) % 58.99/59.65 & aSubsetOf0(W1,W0) ) % 58.99/59.65 => sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 58.99/59.65 % 58.99/59.65 fof(mCardSubEx,axiom, % 58.99/59.65 ! [W0,W1] : % 58.99/59.65 ( ( aSet0(W0) % 58.99/59.65 & aElementOf0(W1,szNzAzT0) ) % 58.99/59.65 => ( ( isFinite0(W0) % 58.99/59.65 & sdtlseqdt0(W1,sbrdtbr0(W0)) ) % 58.99/59.65 => ? [W2] : % 58.99/59.65 ( aSubsetOf0(W2,W0) % 58.99/59.65 & sbrdtbr0(W2) = W1 ) ) ) ). % 58.99/59.65 % 58.99/59.65 fof(mDefMin,definition, % 58.99/59.65 ! [W0] : % 58.99/59.65 ( ( aSubsetOf0(W0,szNzAzT0) % 58.99/59.65 & W0 != slcrc0 ) % 58.99/59.65 => ! [W1] : % 58.99/59.65 ( W1 = szmzizndt0(W0) % 58.99/59.65 <=> ( aElementOf0(W1,W0) % 58.99/59.65 & ! [W2] : % 58.99/59.65 ( aElementOf0(W2,W0) % 58.99/59.65 => sdtlseqdt0(W1,W2) ) ) ) ) ). % 58.99/59.65 % 58.99/59.65 fof(mDefMax,definition, % 58.99/59.65 ! [W0] : % 58.99/59.65 ( ( aSubsetOf0(W0,szNzAzT0) % 58.99/59.65 & isFinite0(W0) % 58.99/59.65 & W0 != slcrc0 ) % 58.99/59.65 => ! [W1] : % 58.99/59.65 ( W1 = szmzazxdt0(W0) % 58.99/59.65 <=> ( aElementOf0(W1,W0) % 58.99/59.65 & ! [W2] : % 58.99/59.65 ( aElementOf0(W2,W0) % 58.99/59.65 => sdtlseqdt0(W2,W1) ) ) ) ) ). % 58.99/59.65 % 58.99/59.65 fof(m__1779,hypothesis, % 58.99/59.65 ( aSet0(xS) % 58.99/59.65 & ! [W0] : % 58.99/59.65 ( aElementOf0(W0,xS) % 58.99/59.65 => aElementOf0(W0,szNzAzT0) ) % 58.99/59.65 & aSubsetOf0(xS,szNzAzT0) % 58.99/59.65 & aSet0(xT) % 58.99/59.65 & ! [W0] : % 58.99/59.65 ( aElementOf0(W0,xT) % 58.99/59.65 => aElementOf0(W0,szNzAzT0) ) % 58.99/59.65 & aSubsetOf0(xT,szNzAzT0) % 58.99/59.65 & ~ ( ~ ? [W0] : aElementOf0(W0,xS) % 58.99/59.65 | xS = slcrc0 ) % 58.99/59.65 & ~ ( ~ ? [W0] : aElementOf0(W0,xT) % 58.99/59.65 | xT = slcrc0 ) ) ). % 58.99/59.65 % 58.99/59.65 fof(m__1802,hypothesis, % 58.99/59.65 ( aElementOf0(szmzizndt0(xS),xS) % 58.99/59.65 & ! [W0] : % 58.99/59.65 ( aElementOf0(W0,xS) % 58.99/59.65 => sdtlseqdt0(szmzizndt0(xS),W0) ) % 58.99/59.65 & aElementOf0(szmzizndt0(xS),xT) % 58.99/59.65 & aElementOf0(szmzizndt0(xT),xT) % 58.99/59.65 & ! [W0] : % 58.99/59.65 ( aElementOf0(W0,xT) % 58.99/59.65 => sdtlseqdt0(szmzizndt0(xT),W0) ) % 58.99/59.65 & aElementOf0(szmzizndt0(xT),xS) ) ). % 58.99/59.65 % 58.99/59.65 fof(m__,conjecture, % 58.99/59.65 ( ( aElementOf0(szmzizndt0(xS),xS) % 58.99/59.65 & ! [W0] : % 58.99/59.65 ( aElementOf0(W0,xS) % 58.99/59.65 => sdtlseqdt0(szmzizndt0(xS),W0) ) ) % 58.99/59.65 => ( ! [W0] : % 58.99/59.65 ( aElementOf0(W0,xT) % 58.99/59.65 => sdtlseqdt0(szmzizndt0(xS),W0) ) % 58.99/59.65 | szmzizndt0(xS) = szmzizndt0(xT) ) ) ). % 58.99/59.65 % 58.99/59.65 %------------------------------------------------------------------------------ % 58.99/59.65 %------------------------------------------- % 58.99/59.65 % Proof found % 58.99/59.65 % SZS status Theorem for theBenchmark % 58.99/59.65 % SZS output start Proof % 58.99/59.65 %ClaNum:136(EqnAxiom:39) % 58.99/59.65 %VarNum:515(SingletonVarNum:159) % 58.99/59.65 %MaxLitNum:8 % 58.99/59.65 %MaxfuncDepth:3 % 58.99/59.65 %SharedTerms:29 % 58.99/59.65 %goalClause: 48 52 58 59 80 % 58.99/59.65 %singleGoalClaCount:4 % 58.99/59.65 [40]P1(a1) % 58.99/59.65 [41]P1(a18) % 58.99/59.65 [42]P1(a22) % 58.99/59.65 [43]P4(a2) % 58.99/59.65 [44]P5(a1) % 58.99/59.65 [45]P2(a17,a1) % 58.99/59.65 [46]P2(a3,a18) % 58.99/59.65 [47]P2(a4,a22) % 58.99/59.65 [48]P2(a5,a22) % 58.99/59.65 [49]P6(a18,a1) % 58.99/59.65 [50]P6(a22,a1) % 58.99/59.65 [56]~E(a2,a18) % 58.99/59.65 [57]~E(a2,a22) % 58.99/59.65 [52]P2(f19(a18),a18) % 58.99/59.65 [53]P2(f19(a18),a22) % 58.99/59.65 [54]P2(f19(a22),a18) % 58.99/59.65 [55]P2(f19(a22),a22) % 58.99/59.65 [58]~E(f19(a22),f19(a18)) % 58.99/59.65 [59]~P8(f19(a18),a5) % 58.99/59.65 [60]P1(x601)+~E(x601,a2) % 58.99/59.65 [66]~P1(x661)+P6(x661,x661) % 58.99/59.65 [71]~P2(x711,a18)+P2(x711,a1) % 58.99/59.65 [72]~P2(x721,a22)+P2(x721,a1) % 58.99/59.65 [73]~P2(x731,a1)+P8(a17,x731) % 58.99/59.65 [78]P8(x781,x781)+~P2(x781,a1) % 58.99/59.65 [64]~P1(x641)+P3(f14(x641)) % 58.99/59.65 [68]~P2(x681,a1)+~E(f21(x681),a17) % 58.99/59.65 [69]~P2(x691,a1)+~E(f21(x691),x691) % 58.99/59.65 [80]~P2(x801,a18)+P8(f19(a18),x801) % 58.99/59.65 [81]~P2(x811,a22)+P8(f19(a22),x811) % 58.99/59.65 [82]~P2(x821,a1)+P2(f21(x821),a1) % 58.99/59.65 [83]~P2(x831,a1)+P8(x831,f21(x831)) % 58.99/59.65 [84]~P2(x841,a1)+P7(x841,f21(x841)) % 58.99/59.65 [91]~P2(x911,a1)+~P8(f21(x911),a17) % 58.99/59.65 [67]~P2(x672,x671)+~E(x671,a2) % 58.99/59.65 [63]~P1(x631)+~P5(x631)+~E(x631,a2) % 58.99/59.65 [65]~P4(x651)+~P5(x651)+~P1(x651) % 58.99/59.65 [61]~P1(x611)+~E(x611,a2)+E(f14(x611),a17) % 58.99/59.65 [62]~P1(x621)+E(x621,a2)+~E(f14(x621),a17) % 58.99/59.65 [70]~P1(x701)+P2(f6(x701),x701)+E(x701,a2) % 58.99/59.65 [75]~P1(x751)+~P4(x751)+P2(f14(x751),a1) % 58.99/59.65 [85]~P2(x851,a1)+E(x851,a17)+P2(f7(x851),a1) % 58.99/59.65 [86]~P1(x861)+P4(x861)+~P2(f14(x861),a1) % 58.99/59.65 [74]~P2(x741,a1)+E(x741,a17)+E(f21(f7(x741)),x741) % 58.99/59.65 [76]~P6(x761,x762)+P1(x761)+~P1(x762) % 58.99/59.65 [77]~P2(x771,x772)+P3(x771)+~P1(x772) % 58.99/59.65 [108]~P1(x1081)+~P2(x1082,x1081)+E(f15(f16(x1081,x1082),x1082),x1081) % 58.99/59.65 [87]~P4(x872)+~P6(x871,x872)+P4(x871)+~P1(x872) % 58.99/59.65 [90]P2(x902,x901)+~E(x902,f19(x901))+~P6(x901,a1)+E(x901,a2) % 58.99/59.65 [93]~P1(x931)+~P3(x932)+~P4(x931)+P4(f15(x931,x932)) % 58.99/59.65 [94]~P1(x941)+~P3(x942)+~P4(x941)+P4(f16(x941,x942)) % 58.99/59.65 [95]~P1(x951)+~P3(x952)+~P5(x951)+P5(f15(x951,x952)) % 58.99/59.65 [96]~P1(x961)+~P3(x962)+~P5(x961)+P5(f16(x961,x962)) % 58.99/59.65 [97]E(x971,x972)+~E(f21(x971),f21(x972))+~P2(x972,a1)+~P2(x971,a1) % 58.99/59.65 [100]~P1(x1002)+~P4(x1002)+~P6(x1001,x1002)+P8(f14(x1001),f14(x1002)) % 58.99/59.65 [106]~P1(x1061)+~P1(x1062)+P6(x1061,x1062)+P2(f8(x1062,x1061),x1061) % 58.99/59.65 [111]P8(x1111,x1112)+P8(f21(x1112),x1111)+~P2(x1112,a1)+~P2(x1111,a1) % 58.99/59.65 [118]~P8(x1181,x1182)+~P2(x1182,a1)+~P2(x1181,a1)+P8(f21(x1181),f21(x1182)) % 58.99/59.65 [120]~P1(x1201)+~P1(x1202)+P6(x1201,x1202)+~P2(f8(x1202,x1201),x1202) % 58.99/59.65 [121]P8(x1211,x1212)+~P2(x1212,a1)+~P2(x1211,a1)+~P8(f21(x1211),f21(x1212)) % 58.99/59.65 [107]P2(x1072,x1071)+~P1(x1071)+~P3(x1072)+E(f16(f15(x1071,x1072),x1072),x1071) % 58.99/59.65 [124]~P1(x1241)+~P4(x1241)+~P2(x1242,x1241)+E(f21(f14(f16(x1241,x1242))),f14(x1241)) % 58.99/59.65 [104]~P1(x1042)+~P6(x1043,x1042)+P2(x1041,x1042)+~P2(x1041,x1043) % 58.99/59.65 [88]~P1(x882)+~P3(x883)+P1(x881)+~E(x881,f15(x882,x883)) % 58.99/59.65 [89]~P1(x892)+~P3(x893)+P1(x891)+~E(x891,f16(x892,x893)) % 58.99/59.65 [98]~P1(x982)+~P1(x981)+~P6(x982,x981)+~P6(x981,x982)+E(x981,x982) % 58.99/59.65 [117]~P8(x1172,x1171)+~P8(x1171,x1172)+E(x1171,x1172)+~P2(x1172,a1)+~P2(x1171,a1) % 58.99/59.65 [92]~P4(x921)+P2(x922,x921)+~E(x922,f20(x921))+~P6(x921,a1)+E(x921,a2) % 58.99/59.65 [119]~P2(x1192,x1191)+P2(f11(x1191,x1192),x1191)+~P6(x1191,a1)+E(x1191,a2)+E(x1192,f19(x1191)) % 58.99/59.65 [125]~P1(x1251)+~P4(x1251)+~P2(x1252,a1)+~P8(x1252,f14(x1251))+P6(f12(x1251,x1252),x1251) % 58.99/59.65 [126]~P2(x1262,x1261)+~P6(x1261,a1)+~P8(x1262,f11(x1261,x1262))+E(x1261,a2)+E(x1262,f19(x1261)) % 58.99/59.65 [112]P2(x1122,x1121)+~P1(x1121)+~P3(x1122)+~P4(x1121)+E(f14(f15(x1121,x1122)),f21(f14(x1121))) % 58.99/59.65 [123]~P1(x1231)+~P4(x1231)+~P2(x1232,a1)+~P8(x1232,f14(x1231))+E(f14(f12(x1231,x1232)),x1232) % 58.99/59.65 [105]~P2(x1053,x1051)+P8(x1052,x1053)+~E(x1052,f19(x1051))+~P6(x1051,a1)+E(x1051,a2) % 58.99/59.65 [101]~P1(x1014)+~P3(x1012)+~P2(x1011,x1013)+~E(x1011,x1012)+~E(x1013,f16(x1014,x1012)) % 58.99/59.65 [102]~P1(x1023)+~P3(x1024)+~P2(x1021,x1022)+P3(x1021)+~E(x1022,f15(x1023,x1024)) % 58.99/59.65 [103]~P1(x1033)+~P3(x1034)+~P2(x1031,x1032)+P3(x1031)+~E(x1032,f16(x1033,x1034)) % 58.99/59.65 [110]~P1(x1102)+~P3(x1104)+~P2(x1101,x1103)+P2(x1101,x1102)+~E(x1103,f16(x1102,x1104)) % 58.99/59.65 [122]~P4(x1221)+~P2(x1222,x1221)+P2(f13(x1221,x1222),x1221)+~P6(x1221,a1)+E(x1221,a2)+E(x1222,f20(x1221)) % 58.99/59.65 [127]~P4(x1271)+~P2(x1272,x1271)+~P6(x1271,a1)+~P8(f13(x1271,x1272),x1272)+E(x1271,a2)+E(x1272,f20(x1271)) % 58.99/59.65 [114]~P1(x1142)+~P1(x1141)+~P6(x1143,x1142)+~P6(x1141,x1143)+P6(x1141,x1142)+~P1(x1143) % 58.99/59.65 [128]~P8(x1281,x1283)+P8(x1281,x1282)+~P8(x1283,x1282)+~P2(x1282,a1)+~P2(x1283,a1)+~P2(x1281,a1) % 58.99/59.65 [109]~P4(x1091)+~P2(x1092,x1091)+P8(x1092,x1093)+~E(x1093,f20(x1091))+~P6(x1091,a1)+E(x1091,a2) % 58.99/59.65 [129]~P1(x1291)+~P1(x1292)+~P3(x1293)+P2(f9(x1292,x1293,x1291),x1291)+~E(f9(x1292,x1293,x1291),x1293)+E(x1291,f16(x1292,x1293)) % 58.99/59.65 [130]~P1(x1301)+~P1(x1302)+~P3(x1303)+P2(f10(x1302,x1303,x1301),x1301)+E(x1301,f15(x1302,x1303))+P3(f10(x1302,x1303,x1301)) % 58.99/59.65 [131]~P1(x1311)+~P1(x1312)+~P3(x1313)+P2(f9(x1312,x1313,x1311),x1311)+E(x1311,f16(x1312,x1313))+P3(f9(x1312,x1313,x1311)) % 58.99/59.65 [132]~P1(x1321)+~P1(x1322)+~P3(x1323)+P2(f9(x1322,x1323,x1321),x1321)+P2(f9(x1322,x1323,x1321),x1322)+E(x1321,f16(x1322,x1323)) % 58.99/59.65 [99]~P1(x994)+~P3(x993)+~P3(x991)+P2(x991,x992)+~E(x991,x993)+~E(x992,f15(x994,x993)) % 58.99/59.65 [113]~P1(x1133)+~P3(x1132)+~P2(x1131,x1134)+E(x1131,x1132)+P2(x1131,x1133)+~E(x1134,f15(x1133,x1132)) % 58.99/59.65 [115]~P1(x1153)+~P3(x1154)+~P3(x1151)+~P2(x1151,x1153)+P2(x1151,x1152)+~E(x1152,f15(x1153,x1154)) % 58.99/59.65 [133]~P1(x1331)+~P1(x1332)+~P3(x1333)+E(f10(x1332,x1333,x1331),x1333)+P2(f10(x1332,x1333,x1331),x1331)+P2(f10(x1332,x1333,x1331),x1332)+E(x1331,f15(x1332,x1333)) % 58.99/59.65 [134]~P1(x1341)+~P1(x1342)+~P3(x1343)+~E(f10(x1342,x1343,x1341),x1343)+~P2(f10(x1342,x1343,x1341),x1341)+E(x1341,f15(x1342,x1343))+~P3(f10(x1342,x1343,x1341)) % 58.99/59.65 [135]~P1(x1351)+~P1(x1352)+~P3(x1353)+~P2(f10(x1352,x1353,x1351),x1351)+~P2(f10(x1352,x1353,x1351),x1352)+E(x1351,f15(x1352,x1353))+~P3(f10(x1352,x1353,x1351)) % 58.99/59.65 [116]~P1(x1164)+~P3(x1162)+~P3(x1161)+~P2(x1161,x1164)+E(x1161,x1162)+P2(x1161,x1163)+~E(x1163,f16(x1164,x1162)) % 58.99/59.65 [136]~P1(x1361)+~P1(x1362)+~P3(x1363)+E(f9(x1362,x1363,x1361),x1363)+~P2(f9(x1362,x1363,x1361),x1361)+~P2(f9(x1362,x1363,x1361),x1362)+E(x1361,f16(x1362,x1363))+~P3(f9(x1362,x1363,x1361)) % 58.99/59.65 %EqnAxiom % 58.99/59.65 [1]E(x11,x11) % 58.99/59.65 [2]E(x22,x21)+~E(x21,x22) % 58.99/59.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.99/59.66 [4]~E(x41,x42)+E(f19(x41),f19(x42)) % 58.99/59.66 [5]~E(x51,x52)+E(f9(x51,x53,x54),f9(x52,x53,x54)) % 58.99/59.66 [6]~E(x61,x62)+E(f9(x63,x61,x64),f9(x63,x62,x64)) % 58.99/59.66 [7]~E(x71,x72)+E(f9(x73,x74,x71),f9(x73,x74,x72)) % 58.99/59.66 [8]~E(x81,x82)+E(f10(x81,x83,x84),f10(x82,x83,x84)) % 58.99/59.66 [9]~E(x91,x92)+E(f10(x93,x91,x94),f10(x93,x92,x94)) % 58.99/59.66 [10]~E(x101,x102)+E(f10(x103,x104,x101),f10(x103,x104,x102)) % 58.99/59.66 [11]~E(x111,x112)+E(f15(x111,x113),f15(x112,x113)) % 58.99/59.66 [12]~E(x121,x122)+E(f15(x123,x121),f15(x123,x122)) % 58.99/59.66 [13]~E(x131,x132)+E(f14(x131),f14(x132)) % 58.99/59.66 [14]~E(x141,x142)+E(f16(x141,x143),f16(x142,x143)) % 58.99/59.66 [15]~E(x151,x152)+E(f16(x153,x151),f16(x153,x152)) % 58.99/59.66 [16]~E(x161,x162)+E(f20(x161),f20(x162)) % 58.99/59.66 [17]~E(x171,x172)+E(f12(x171,x173),f12(x172,x173)) % 58.99/59.66 [18]~E(x181,x182)+E(f12(x183,x181),f12(x183,x182)) % 58.99/59.66 [19]~E(x191,x192)+E(f8(x191,x193),f8(x192,x193)) % 58.99/59.66 [20]~E(x201,x202)+E(f8(x203,x201),f8(x203,x202)) % 58.99/59.66 [21]~E(x211,x212)+E(f11(x211,x213),f11(x212,x213)) % 58.99/59.66 [22]~E(x221,x222)+E(f11(x223,x221),f11(x223,x222)) % 58.99/59.66 [23]~E(x231,x232)+E(f21(x231),f21(x232)) % 58.99/59.66 [24]~E(x241,x242)+E(f13(x241,x243),f13(x242,x243)) % 58.99/59.66 [25]~E(x251,x252)+E(f13(x253,x251),f13(x253,x252)) % 58.99/59.66 [26]~E(x261,x262)+E(f7(x261),f7(x262)) % 58.99/59.66 [27]~E(x271,x272)+E(f6(x271),f6(x272)) % 58.99/59.66 [28]~P1(x281)+P1(x282)+~E(x281,x282) % 58.99/59.66 [29]P2(x292,x293)+~E(x291,x292)+~P2(x291,x293) % 58.99/59.66 [30]P2(x303,x302)+~E(x301,x302)+~P2(x303,x301) % 58.99/59.66 [31]~P4(x311)+P4(x312)+~E(x311,x312) % 58.99/59.66 [32]P8(x322,x323)+~E(x321,x322)+~P8(x321,x323) % 58.99/59.66 [33]P8(x333,x332)+~E(x331,x332)+~P8(x333,x331) % 58.99/59.66 [34]~P5(x341)+P5(x342)+~E(x341,x342) % 58.99/59.66 [35]P6(x352,x353)+~E(x351,x352)+~P6(x351,x353) % 58.99/59.66 [36]P6(x363,x362)+~E(x361,x362)+~P6(x363,x361) % 58.99/59.66 [37]~P3(x371)+P3(x372)+~E(x371,x372) % 58.99/59.66 [38]P7(x382,x383)+~E(x381,x382)+~P7(x381,x383) % 58.99/59.66 [39]P7(x393,x392)+~E(x391,x392)+~P7(x393,x391) % 58.99/59.66 % 58.99/59.66 %------------------------------------------- % 58.99/59.66 cnf(137,plain, % 58.99/59.66 (P1(a2)), % 58.99/59.66 inference(equality_inference,[],[60])). % 58.99/59.66 cnf(138,plain, % 58.99/59.66 (~P1(a2)+E(f14(a2),a17)), % 58.99/59.66 inference(equality_inference,[],[61])). % 58.99/59.66 cnf(139,plain, % 58.99/59.66 (~P5(a2)+~P1(a2)), % 58.99/59.66 inference(equality_inference,[],[63])). % 58.99/59.66 cnf(140,plain, % 58.99/59.66 (~P2(x1401,a2)), % 58.99/59.66 inference(equality_inference,[],[67])). % 58.99/59.66 cnf(141,plain, % 58.99/59.66 (~P1(x1411)+~P3(x1412)+P1(f15(x1411,x1412))), % 58.99/59.66 inference(equality_inference,[],[88])). % 58.99/59.66 cnf(142,plain, % 58.99/59.66 (~P1(x1421)+~P3(x1422)+P1(f16(x1421,x1422))), % 58.99/59.66 inference(equality_inference,[],[89])). % 58.99/59.66 cnf(148,plain, % 58.99/59.66 (~P2(x1481,x1482)+P8(f19(x1482),x1481)+~P6(x1482,a1)+E(x1482,a2)), % 58.99/59.66 inference(equality_inference,[],[105])). % 58.99/59.66 cnf(149,plain, % 58.99/59.66 (~P4(x1491)+~P2(x1492,x1491)+P8(x1492,f20(x1491))+~P6(x1491,a1)+E(x1491,a2)), % 58.99/59.66 inference(equality_inference,[],[109])). % 58.99/59.66 cnf(150,plain, % 58.99/59.66 (P2(x1501,x1502)+~P1(x1502)+~P3(x1503)+~P2(x1501,f16(x1502,x1503))), % 58.99/59.66 inference(equality_inference,[],[110])). % 58.99/59.66 cnf(151,plain, % 58.99/59.66 (E(x1511,x1512)+P2(x1511,x1513)+~P1(x1513)+~P3(x1512)+~P2(x1511,f15(x1513,x1512))), % 58.99/59.66 inference(equality_inference,[],[113])). % 58.99/59.66 cnf(152,plain, % 58.99/59.66 (~P2(x1521,x1522)+~P1(x1522)+~P3(x1523)+P2(x1521,f15(x1522,x1523))+~P3(x1521)), % 58.99/59.66 inference(equality_inference,[],[115])). % 58.99/59.66 cnf(154,plain, % 58.99/59.66 (E(f14(a2),a17)), % 58.99/59.66 inference(scs_inference,[],[137,138])). % 58.99/59.66 cnf(155,plain, % 58.99/59.66 (~P5(a2)), % 58.99/59.66 inference(scs_inference,[],[137,139])). % 58.99/59.66 cnf(156,plain, % 58.99/59.66 (~P2(a5,a18)), % 58.99/59.66 inference(scs_inference,[],[59,80])). % 58.99/59.66 cnf(158,plain, % 58.99/59.66 (~E(a22,a18)), % 58.99/59.66 inference(scs_inference,[],[58,59,80,4])). % 58.99/59.66 cnf(159,plain, % 58.99/59.66 (P8(a17,a17)), % 58.99/59.66 inference(scs_inference,[],[58,59,45,80,4,78])). % 58.99/59.66 cnf(162,plain, % 58.99/59.66 (~E(a22,a2)), % 58.99/59.66 inference(scs_inference,[],[48,58,52,59,140,45,80,4,78,29,30])). % 58.99/59.66 cnf(163,plain, % 58.99/59.66 (~P2(x1631,a2)), % 58.99/59.66 inference(rename_variables,[],[140])). % 58.99/59.66 cnf(164,plain, % 58.99/59.66 (~P4(a1)), % 58.99/59.66 inference(scs_inference,[],[48,58,52,59,140,45,40,44,80,4,78,29,30,65])). % 58.99/59.66 cnf(166,plain, % 58.99/59.66 (P2(a5,a1)), % 58.99/59.66 inference(scs_inference,[],[48,58,52,59,140,45,40,44,50,80,4,78,29,30,65,104])). % 58.99/59.66 cnf(168,plain, % 58.99/59.66 (P6(a2,a1)), % 58.99/59.66 inference(scs_inference,[],[48,58,52,59,140,163,45,40,44,50,137,80,4,78,29,30,65,104,106])). % 58.99/59.66 cnf(173,plain, % 58.99/59.66 (P8(f19(a22),a5)), % 58.99/59.66 inference(scs_inference,[],[48,58,52,59,140,163,45,40,44,50,137,80,4,78,29,30,65,104,106,118,148])). % 58.99/59.66 cnf(180,plain, % 58.99/59.66 (E(a17,f14(a2))), % 58.99/59.66 inference(scs_inference,[],[154,2])). % 58.99/59.66 cnf(181,plain, % 58.99/59.66 (P8(a5,a5)), % 58.99/59.66 inference(scs_inference,[],[166,154,2,78])). % 58.99/59.66 cnf(183,plain, % 58.99/59.66 (~E(a3,a5)), % 58.99/59.66 inference(scs_inference,[],[156,166,46,154,2,78,29])). % 58.99/59.66 cnf(184,plain, % 58.99/59.66 (~E(a18,a2)), % 58.99/59.66 inference(scs_inference,[],[156,52,166,46,140,154,2,78,29,30])). % 58.99/59.66 cnf(185,plain, % 58.99/59.66 (~P2(x1851,a2)), % 58.99/59.66 inference(rename_variables,[],[140])). % 58.99/59.66 cnf(187,plain, % 58.99/59.66 (P8(f14(a2),a17)), % 58.99/59.66 inference(scs_inference,[],[156,52,166,46,140,159,154,2,78,29,30,33,32])). % 58.99/59.66 cnf(188,plain, % 58.99/59.66 (P6(a2,a18)), % 58.99/59.66 inference(scs_inference,[],[156,52,166,46,140,185,159,154,41,137,2,78,29,30,33,32,106])). % 58.99/59.66 cnf(191,plain, % 58.99/59.66 (P8(f21(a5),f21(a5))), % 58.99/59.66 inference(scs_inference,[],[156,52,166,46,140,185,159,154,41,137,2,78,29,30,33,32,106,118])). % 58.99/59.66 cnf(193,plain, % 58.99/59.66 (~P6(a22,a18)), % 58.99/59.66 inference(scs_inference,[],[48,156,52,166,46,140,185,159,154,41,137,2,78,29,30,33,32,106,118,104])). % 58.99/59.66 cnf(197,plain, % 58.99/59.66 (P6(f12(a2,a17),a2)), % 58.99/59.66 inference(scs_inference,[],[48,156,52,166,46,140,185,45,159,154,41,43,137,2,78,29,30,33,32,106,118,104,98,125])). % 58.99/59.66 cnf(203,plain, % 58.99/59.66 (~P2(f11(a18,f19(a22)),a22)), % 58.99/59.66 inference(scs_inference,[],[48,156,52,58,166,46,54,140,185,45,159,49,154,41,43,137,40,2,78,29,30,33,32,106,118,104,98,125,126,114,81])). % 58.99/59.66 cnf(207,plain, % 58.99/59.66 (~E(a1,a2)), % 58.99/59.66 inference(scs_inference,[],[48,156,52,58,166,46,54,140,185,45,159,49,154,41,43,137,40,2,78,29,30,33,32,106,118,104,98,125,126,114,81,28,35,36])). % 58.99/59.66 cnf(214,plain, % 58.99/59.66 (P8(f14(a2),f14(a2))), % 58.99/59.66 inference(scs_inference,[],[48,187,203,180,193,50,29,36,33])). % 58.99/59.66 cnf(216,plain, % 58.99/59.66 (P6(a2,a22)), % 58.99/59.66 inference(scs_inference,[],[48,59,187,203,180,193,140,181,50,42,137,29,36,33,32,106])). % 58.99/59.66 cnf(219,plain, % 58.99/59.66 (~P6(a1,a18)), % 58.99/59.66 inference(scs_inference,[],[48,59,187,203,180,193,140,181,49,50,42,40,137,41,29,36,33,32,106,98])). % 58.99/59.66 cnf(233,plain, % 58.99/59.66 (P6(f12(a2,a17),x2331)+~E(a2,x2331)), % 58.99/59.66 inference(scs_inference,[],[197,47,180,188,162,219,216,203,42,137,29,35,98,34,37,36])). % 58.99/59.66 cnf(240,plain, % 58.99/59.66 (~E(f19(a22),a5)), % 58.99/59.66 inference(scs_inference,[],[156,54,29])). % 58.99/59.66 cnf(242,plain, % 58.99/59.66 (~P3(f14(a2))+P3(a17)), % 58.99/59.66 inference(scs_inference,[],[156,54,154,29,34,37])). % 58.99/59.66 cnf(243,plain, % 58.99/59.66 (P6(x2431,a22)+~E(a2,x2431)), % 58.99/59.66 inference(scs_inference,[],[156,54,216,154,29,34,37,35])). % 58.99/59.66 cnf(250,plain, % 58.99/59.66 (P2(f14(a2),a1)), % 58.99/59.66 inference(scs_inference,[],[180,45,29])). % 58.99/59.66 cnf(253,plain, % 58.99/59.66 (P6(f12(a2,f14(a2)),a2)), % 58.99/59.66 inference(scs_inference,[],[180,214,45,43,137,29,118,125])). % 58.99/59.66 cnf(255,plain, % 58.99/59.66 (P6(x2551,a1)+~E(a2,x2551)), % 58.99/59.66 inference(scs_inference,[],[180,214,168,45,43,137,29,118,125,35])). % 58.99/59.66 cnf(256,plain, % 58.99/59.66 (P8(x2561,f21(a5))+~E(f21(a5),x2561)), % 58.99/59.66 inference(scs_inference,[],[180,214,168,191,45,43,137,29,118,125,35,32])). % 58.99/59.66 cnf(258,plain, % 58.99/59.66 (P8(a5,x2581)+~E(a5,x2581)), % 58.99/59.66 inference(scs_inference,[],[180,214,168,191,45,181,43,137,29,118,125,35,32,36,33])). % 58.99/59.66 cnf(259,plain, % 58.99/59.66 (~P2(f11(a18,f19(a22)),f16(a22,x2591))+~P3(x2591)), % 58.99/59.66 inference(scs_inference,[],[180,214,168,191,203,45,181,43,42,137,29,118,125,35,32,36,33,150])). % 58.99/59.66 cnf(279,plain, % 58.99/59.66 (P2(x2791,a1)+~E(a5,x2791)), % 58.99/59.66 inference(scs_inference,[],[166,29])). % 58.99/59.66 cnf(294,plain, % 58.99/59.66 (P6(f12(a2,f14(a2)),x2941)+~E(a2,x2941)), % 58.99/59.66 inference(scs_inference,[],[253,36])). % 58.99/59.66 cnf(303,plain, % 58.99/59.66 (~P2(a5,f16(a18,x3031))+~P3(x3031)), % 58.99/59.66 inference(scs_inference,[],[156,41,150])). % 58.99/59.66 cnf(309,plain, % 58.99/59.66 (~P8(a5,f11(a22,a5))+E(a5,f19(a22))), % 58.99/59.66 inference(scs_inference,[],[48,52,58,156,250,162,184,49,50,42,41,150,104,149,151,126])). % 58.99/59.66 cnf(311,plain, % 58.99/59.66 (P3(f14(a2))), % 58.99/59.66 inference(scs_inference,[],[42,216,64,76])). % 58.99/59.66 cnf(312,plain, % 58.99/59.66 (P3(a17)), % 58.99/59.66 inference(scs_inference,[],[311,242])). % 58.99/59.66 cnf(315,plain, % 58.99/59.66 (P2(f14(a2),f15(a1,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[250,203,42,311,40,150,152])). % 58.99/59.66 cnf(317,plain, % 58.99/59.66 (E(a2,f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[250,140,203,42,311,40,137,150,152,132])). % 58.99/59.66 cnf(319,plain, % 58.99/59.66 (~P2(x3191,a2)), % 58.99/59.66 inference(rename_variables,[],[140])). % 58.99/59.66 cnf(321,plain, % 58.99/59.66 (P6(f12(a2,a17),f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[250,140,203,42,311,40,137,150,152,132,233])). % 58.99/59.66 cnf(323,plain, % 58.99/59.66 (P6(f16(a2,f14(a2)),a1)), % 58.99/59.66 inference(scs_inference,[],[250,140,203,42,311,40,137,150,152,132,233,243,255])). % 58.99/59.66 cnf(324,plain, % 58.99/59.66 (P6(f12(a2,f14(a2)),f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[250,140,203,42,311,40,137,150,152,132,233,243,255,294])). % 58.99/59.66 cnf(325,plain, % 58.99/59.66 (E(f16(a2,f14(a2)),a2)), % 58.99/59.66 inference(scs_inference,[],[250,140,203,42,311,40,137,150,152,132,233,243,255,294,2])). % 58.99/59.66 cnf(326,plain, % 58.99/59.66 (~E(a22,f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[250,140,162,203,42,311,40,137,150,152,132,233,243,255,294,2,3])). % 58.99/59.66 cnf(329,plain, % 58.99/59.66 (~E(f15(a1,f14(a2)),a2)), % 58.99/59.66 inference(scs_inference,[],[250,140,319,162,203,42,311,40,137,150,152,132,233,243,255,294,2,3,63,30])). % 58.99/59.66 cnf(331,plain, % 58.99/59.66 (P1(f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[250,140,319,162,203,42,311,40,137,150,152,132,233,243,255,294,2,3,63,30,28])). % 58.99/59.66 cnf(332,plain, % 58.99/59.66 (~P5(f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[250,140,319,162,203,42,311,155,40,137,150,152,132,233,243,255,294,2,3,63,30,28,34])). % 58.99/59.66 cnf(333,plain, % 58.99/59.66 (P2(a17,f15(a1,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[250,140,319,162,203,154,42,311,155,40,137,150,152,132,233,243,255,294,2,3,63,30,28,34,29])). % 58.99/59.66 cnf(334,plain, % 58.99/59.66 (P4(f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[250,140,319,162,203,154,42,311,155,43,40,137,150,152,132,233,243,255,294,2,3,63,30,28,34,29,31])). % 58.99/59.66 cnf(335,plain, % 58.99/59.66 (~P6(a22,f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[250,140,319,162,203,154,42,311,155,43,40,137,150,152,132,233,243,255,294,2,3,63,30,28,34,29,31,98])). % 58.99/59.66 cnf(337,plain, % 58.99/59.66 (~P2(x3371,f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[250,140,319,162,203,154,42,311,155,43,40,137,150,152,132,233,243,255,294,2,3,63,30,28,34,29,31,98,67])). % 58.99/59.66 cnf(349,plain, % 58.99/59.66 (P2(a17,f15(a1,a17))), % 58.99/59.66 inference(scs_inference,[],[325,335,329,203,45,50,42,312,40,3,36,150,152])). % 58.99/59.66 cnf(351,plain, % 58.99/59.66 (~P6(a1,f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[325,335,329,203,45,50,42,331,323,312,40,3,36,150,152,98])). % 58.99/59.66 cnf(353,plain, % 58.99/59.66 (E(a2,f16(a2,a17))), % 58.99/59.66 inference(scs_inference,[],[140,325,335,329,203,45,50,42,331,323,312,40,137,3,36,150,152,98,132])). % 58.99/59.66 cnf(355,plain, % 58.99/59.66 (~P2(x3551,a2)), % 58.99/59.66 inference(rename_variables,[],[140])). % 58.99/59.66 cnf(358,plain, % 58.99/59.66 (P6(f16(a2,a17),a22)), % 58.99/59.66 inference(scs_inference,[],[140,325,335,329,203,45,50,42,331,323,312,40,137,3,36,150,152,98,132,233,243])). % 58.99/59.66 cnf(359,plain, % 58.99/59.66 (P6(f12(a2,f14(a2)),f16(a2,a17))), % 58.99/59.66 inference(scs_inference,[],[140,325,335,329,203,45,50,42,331,323,312,40,137,3,36,150,152,98,132,233,243,294])). % 58.99/59.66 cnf(361,plain, % 58.99/59.66 (E(f16(a2,a17),a2)), % 58.99/59.66 inference(scs_inference,[],[140,325,335,329,203,45,50,42,331,323,312,40,137,3,36,150,152,98,132,233,243,294,255,2])). % 58.99/59.66 cnf(364,plain, % 58.99/59.66 (~E(f15(a1,a17),a2)), % 58.99/59.66 inference(scs_inference,[],[140,355,325,335,329,203,45,50,42,331,323,312,40,137,3,36,150,152,98,132,233,243,294,255,2,63,30])). % 58.99/59.66 cnf(366,plain, % 58.99/59.66 (P1(f16(a2,a17))), % 58.99/59.66 inference(scs_inference,[],[140,355,325,335,329,203,45,50,42,331,323,312,40,137,3,36,150,152,98,132,233,243,294,255,2,63,30,28])). % 58.99/59.66 cnf(367,plain, % 58.99/59.66 (P2(f14(a2),f15(a1,a17))), % 58.99/59.66 inference(scs_inference,[],[180,140,355,325,335,329,203,45,50,42,331,323,312,40,137,3,36,150,152,98,132,233,243,294,255,2,63,30,28,29])). % 58.99/59.66 cnf(368,plain, % 58.99/59.66 (~P5(f16(a2,a17))), % 58.99/59.66 inference(scs_inference,[],[180,140,355,325,335,329,203,45,50,42,331,323,312,155,40,137,3,36,150,152,98,132,233,243,294,255,2,63,30,28,29,34])). % 58.99/59.66 cnf(369,plain, % 58.99/59.66 (P4(f16(a2,a17))), % 58.99/59.66 inference(scs_inference,[],[180,140,355,325,335,329,203,45,50,42,331,323,312,155,43,40,137,3,36,150,152,98,132,233,243,294,255,2,63,30,28,29,34,31])). % 58.99/59.66 cnf(370,plain, % 58.99/59.66 (~P2(x3701,f16(a2,a17))), % 58.99/59.66 inference(scs_inference,[],[180,140,355,325,335,329,203,45,50,42,331,323,312,155,43,40,137,3,36,150,152,98,132,233,243,294,255,2,63,30,28,29,34,31,67])). % 58.99/59.66 cnf(377,plain, % 58.99/59.66 (~E(f15(a1,a17),f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[325,364,3])). % 58.99/59.66 cnf(379,plain, % 58.99/59.66 (~P2(x3791,f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[325,370,351,364,324,366,311,3,35,150])). % 58.99/59.66 cnf(381,plain, % 58.99/59.66 (E(f16(a2,a17),f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[140,325,370,351,364,324,366,311,137,3,35,150,132])). % 58.99/59.66 cnf(390,plain, % 58.99/59.66 (~E(f15(a1,f14(a2)),f16(a2,a17))), % 58.99/59.66 inference(scs_inference,[],[361,329,3])). % 58.99/59.66 cnf(392,plain, % 58.99/59.66 (~P2(x3921,f16(f16(a2,f14(a2)),a17))), % 58.99/59.66 inference(scs_inference,[],[361,337,329,351,321,331,312,3,35,150])). % 58.99/59.66 cnf(394,plain, % 58.99/59.66 (~P1(f16(f16(a2,a17),f14(a2)))+E(f16(f16(a2,a17),f14(a2)),a2)), % 58.99/59.66 inference(scs_inference,[],[361,337,379,329,351,321,331,312,3,35,150,70])). % 58.99/59.66 cnf(400,plain, % 58.99/59.66 (E(a2,f16(f16(a2,a17),f14(a2)))+~P1(f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[361,337,379,329,351,321,331,155,312,3,35,150,70,34,60,2])). % 58.99/59.66 cnf(402,plain, % 58.99/59.66 (~E(f15(a1,a17),f16(a2,a17))), % 58.99/59.66 inference(scs_inference,[],[361,364,3])). % 58.99/59.66 cnf(403,plain, % 58.99/59.66 (~P2(x4031,f16(f16(a2,a17),a17))), % 58.99/59.66 inference(scs_inference,[],[361,370,364,366,312,3,150])). % 58.99/59.66 cnf(405,plain, % 58.99/59.66 (~P1(f16(f16(a2,a17),a17))+E(f16(f16(a2,a17),a17),a2)), % 58.99/59.66 inference(scs_inference,[],[361,370,364,366,312,3,150,70])). % 58.99/59.66 cnf(410,plain, % 58.99/59.66 (E(a2,f16(f16(a2,a17),a17))+~P1(f16(f16(a2,a17),a17))), % 58.99/59.66 inference(scs_inference,[],[361,370,364,366,155,312,3,150,70,34,60,2])). % 58.99/59.66 cnf(414,plain, % 58.99/59.66 (P2(f19(a18),a1)), % 58.99/59.66 inference(scs_inference,[],[52,49,40,104])). % 58.99/59.66 cnf(416,plain, % 58.99/59.66 (~P2(a5,f16(a18,a17))), % 58.99/59.66 inference(scs_inference,[],[52,156,49,40,312,41,104,150])). % 58.99/59.66 cnf(423,plain, % 58.99/59.66 (P8(f21(f19(a18)),x4231)+~E(f21(f19(a18)),x4231)), % 58.99/59.66 inference(scs_inference,[],[52,156,49,323,40,312,41,104,150,78,36,118,33])). % 58.99/59.66 cnf(427,plain, % 58.99/59.66 (P6(x4271,f16(a2,a17))+~E(f12(a2,f14(a2)),x4271)), % 58.99/59.66 inference(scs_inference,[],[52,156,353,49,323,359,40,312,41,104,150,78,36,118,33,37,29,32,35])). % 58.99/59.66 cnf(433,plain, % 58.99/59.66 (P2(a3,a1)), % 58.99/59.66 inference(scs_inference,[],[46,49,40,104])). % 58.99/59.66 cnf(435,plain, % 58.99/59.66 (P8(a3,a3)), % 58.99/59.66 inference(scs_inference,[],[46,49,40,104,78])). % 58.99/59.66 cnf(438,plain, % 58.99/59.66 (P8(f21(a3),f21(a3))), % 58.99/59.66 inference(scs_inference,[],[46,49,40,104,78,33,118])). % 58.99/59.66 cnf(447,plain, % 58.99/59.66 (P2(a4,a1)), % 58.99/59.66 inference(scs_inference,[],[47,50,40,104])). % 58.99/59.66 cnf(449,plain, % 58.99/59.66 (P8(a4,a4)), % 58.99/59.66 inference(scs_inference,[],[47,50,40,104,78])). % 58.99/59.66 cnf(451,plain, % 58.99/59.66 (P2(x4511,a1)+~E(a3,x4511)), % 58.99/59.66 inference(scs_inference,[],[47,433,50,40,104,78,29])). % 58.99/59.66 cnf(462,plain, % 58.99/59.66 (~P2(x4621,f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[381,337,326,331,311,3,150])). % 58.99/59.66 cnf(466,plain, % 58.99/59.66 (P2(f19(a22),a1)), % 58.99/59.66 inference(scs_inference,[],[381,54,337,326,447,449,49,40,331,311,3,150,118,104])). % 58.99/59.66 cnf(468,plain, % 58.99/59.66 (~P6(a22,f16(a2,a17))), % 58.99/59.66 inference(scs_inference,[],[381,54,337,326,447,449,49,358,40,42,331,366,311,3,150,118,104,98])). % 58.99/59.66 cnf(470,plain, % 58.99/59.66 (P8(f19(a22),f19(a22))), % 58.99/59.66 inference(scs_inference,[],[381,54,337,326,447,449,49,358,40,42,331,366,311,3,150,118,104,98,78])). % 58.99/59.66 cnf(472,plain, % 58.99/59.66 (~P1(f16(f16(a2,f14(a2)),f14(a2)))+E(f16(f16(a2,f14(a2)),f14(a2)),a2)), % 58.99/59.66 inference(scs_inference,[],[381,54,337,326,447,449,49,358,40,42,331,366,311,3,150,118,104,98,78,70])). % 58.99/59.66 cnf(480,plain, % 58.99/59.66 (~E(a1,f16(a2,a17))), % 58.99/59.66 inference(scs_inference,[],[468,50,36])). % 58.99/59.66 cnf(481,plain, % 58.99/59.66 (P8(f21(f19(a22)),f21(f19(a22)))), % 58.99/59.66 inference(scs_inference,[],[468,466,470,50,36,118])). % 58.99/59.66 cnf(497,plain, % 58.99/59.66 (P8(f21(f19(a22)),x4971)+~E(f21(f19(a22)),x4971)), % 58.99/59.66 inference(scs_inference,[],[481,33])). % 58.99/59.66 cnf(524,plain, % 58.99/59.66 (~E(a18,f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[52,337,30])). % 58.99/59.66 cnf(525,plain, % 58.99/59.66 (~P2(x5251,f16(a2,f14(a2)))), % 58.99/59.66 inference(rename_variables,[],[337])). % 58.99/59.66 cnf(528,plain, % 58.99/59.66 (E(f16(a2,f14(a2)),f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[52,156,337,525,331,41,311,30,150,132])). % 58.99/59.66 cnf(532,plain, % 58.99/59.66 (E(f16(f16(a2,f14(a2)),f14(a2)),f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[52,156,337,525,331,41,311,30,150,132,2])). % 58.99/59.66 cnf(533,plain, % 58.99/59.66 (E(a2,f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[52,156,317,337,525,331,41,311,30,150,132,2,3])). % 58.99/59.66 cnf(534,plain, % 58.99/59.66 (P1(f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[52,156,317,337,525,331,41,311,30,150,132,2,3,28])). % 58.99/59.66 cnf(550,plain, % 58.99/59.66 (E(f16(f16(a2,f14(a2)),f14(a2)),a2)), % 58.99/59.66 inference(scs_inference,[],[534,472])). % 58.99/59.66 cnf(554,plain, % 58.99/59.66 (P6(f16(f16(a2,f14(a2)),f14(a2)),a22)), % 58.99/59.66 inference(scs_inference,[],[533,255,233,243])). % 58.99/59.66 cnf(555,plain, % 58.99/59.66 (P6(f12(a2,f14(a2)),f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[533,255,233,243,294])). % 58.99/59.66 cnf(564,plain, % 58.99/59.66 (E(f16(a2,a17),f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[381,140,462,528,533,524,137,534,334,312,255,233,243,294,3,31,150,132,2])). % 58.99/59.66 cnf(566,plain, % 58.99/59.66 (P2(x5661,a1)+~E(a4,x5661)), % 58.99/59.66 inference(scs_inference,[],[381,140,447,462,438,528,533,524,137,534,334,312,255,233,243,294,3,31,150,132,2,32,29])). % 58.99/59.66 cnf(593,plain, % 58.99/59.66 (E(f16(f16(a2,f14(a2)),a17),f16(a2,f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[337,532,377,331,312,3,132,2])). % 58.99/59.66 cnf(594,plain, % 58.99/59.66 (P1(f16(f16(a2,f14(a2)),a17))), % 58.99/59.66 inference(scs_inference,[],[337,532,377,331,312,3,132,2,28])). % 58.99/59.66 cnf(612,plain, % 58.99/59.66 (~P6(a22,f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[532,392,326,42,554,534,594,311,3,150,98])). % 58.99/59.66 cnf(624,plain, % 58.99/59.66 (~E(a18,f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[532,524,3])). % 58.99/59.66 cnf(629,plain, % 58.99/59.66 (P6(f16(f16(a2,f14(a2)),a17),a1)), % 58.99/59.66 inference(scs_inference,[],[337,140,532,524,331,137,312,3,132,255])). % 58.99/59.66 cnf(632,plain, % 58.99/59.66 (P6(f16(f16(a2,f14(a2)),a17),a22)), % 58.99/59.66 inference(scs_inference,[],[337,140,532,524,331,137,312,3,132,255,233,294,243])). % 58.99/59.66 cnf(660,plain, % 58.99/59.66 (P6(f16(f16(a2,a17),f14(a2)),a1)+~P1(f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[528,379,593,326,435,323,40,42,632,594,3,98,36,32,37,148,106])). % 58.99/59.66 cnf(670,plain, % 58.99/59.66 (P6(f16(f16(a2,a17),a17),a1)+~P1(f16(f16(a2,a17),a17))), % 58.99/59.66 inference(scs_inference,[],[550,593,403,524,449,323,40,629,3,32,36,37,148,106])). % 58.99/59.66 cnf(728,plain, % 58.99/59.66 (~P2(x7281,f15(f16(a2,a17),a17))+E(x7281,a17)), % 58.99/59.66 inference(scs_inference,[],[370,366,312,151])). % 58.99/59.66 cnf(742,plain, % 58.99/59.66 (~P2(x7421,f15(f16(a2,f14(a2)),a17))+E(x7421,a17)), % 58.99/59.66 inference(scs_inference,[],[337,331,312,151])). % 58.99/59.66 cnf(784,plain, % 58.99/59.66 (~P2(x7841,f15(a2,a17))+E(x7841,a17)), % 58.99/59.66 inference(scs_inference,[],[140,137,312,151])). % 58.99/59.66 cnf(827,plain, % 58.99/59.66 (~P1(f16(f16(a2,a17),f14(a2)))+E(f16(f16(a2,a17),f14(a2)),f16(f16(a2,f14(a2)),a17))), % 58.99/59.66 inference(scs_inference,[],[337,379,331,312,132])). % 58.99/59.66 cnf(831,plain, % 58.99/59.66 (E(f16(f16(a2,f14(a2)),a17),f16(f16(a2,a17),f14(a2)))+~P1(f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[337,379,331,312,132,2])). % 58.99/59.66 cnf(858,plain, % 58.99/59.66 (~P1(f16(f16(a2,a17),a17))+E(f16(f16(a2,a17),a17),f16(f16(a2,f14(a2)),a17))), % 58.99/59.66 inference(scs_inference,[],[337,403,331,312,132])). % 58.99/59.66 cnf(862,plain, % 58.99/59.66 (E(f16(f16(a2,f14(a2)),a17),f16(f16(a2,a17),a17))+~P1(f16(f16(a2,a17),a17))), % 58.99/59.66 inference(scs_inference,[],[337,403,331,312,132,2])). % 58.99/59.66 cnf(879,plain, % 58.99/59.66 (~E(a18,f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[52,379,30])). % 58.99/59.66 cnf(880,plain, % 58.99/59.66 (~P2(x8801,f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(rename_variables,[],[379])). % 58.99/59.66 cnf(881,plain, % 58.99/59.66 (~P1(f16(f16(a2,a17),f14(a2)))+E(f16(f16(a2,a17),f14(a2)),f16(f16(f16(a2,a17),f14(a2)),a17))), % 58.99/59.66 inference(scs_inference,[],[52,379,880,312,30,132])). % 58.99/59.66 cnf(885,plain, % 58.99/59.66 (E(f16(f16(f16(a2,a17),f14(a2)),a17),f16(f16(a2,a17),f14(a2)))+~P1(f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[52,379,880,312,30,132,2])). % 58.99/59.66 cnf(890,plain, % 58.99/59.66 (~E(a1,f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[250,379,30])). % 58.99/59.66 cnf(898,plain, % 58.99/59.66 (~E(a18,f16(f16(a2,a17),a17))), % 58.99/59.66 inference(scs_inference,[],[52,403,30])). % 58.99/59.66 cnf(915,plain, % 58.99/59.66 (~E(a1,f16(f16(a2,a17),a17))), % 58.99/59.66 inference(scs_inference,[],[250,403,30])). % 58.99/59.66 cnf(947,plain, % 58.99/59.66 (P6(f16(f16(a2,a17),f14(a2)),a22)+~P1(f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[379,42,106])). % 58.99/59.66 cnf(951,plain, % 58.99/59.66 (P6(f16(f16(a2,a17),a17),a22)+~P1(f16(f16(a2,a17),a17))), % 58.99/59.66 inference(scs_inference,[],[403,42,106])). % 58.99/59.66 cnf(1011,plain, % 58.99/59.66 (~P2(x10111,f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(rename_variables,[],[379])). % 58.99/59.66 cnf(1012,plain, % 58.99/59.66 (~P1(f16(f16(a2,a17),f14(a2)))+E(f16(a2,f14(a2)),f16(f16(f16(a2,a17),f14(a2)),a17))), % 58.99/59.66 inference(scs_inference,[],[349,379,1011,337,331,312,30,132])). % 58.99/59.66 cnf(1016,plain, % 58.99/59.66 (E(f16(f16(f16(a2,a17),f14(a2)),a17),f16(a2,f14(a2)))+~P1(f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[349,379,1011,337,331,312,30,132,2])). % 58.99/59.66 cnf(1019,plain, % 58.99/59.66 (E(a2,f16(f16(f16(a2,a17),f14(a2)),a17))+~P1(f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[317,349,379,1011,403,337,331,312,30,132,2,70,3])). % 58.99/59.66 cnf(1021,plain, % 58.99/59.66 (~E(f15(a1,f14(a2)),f16(f16(a2,a17),a17))), % 58.99/59.66 inference(scs_inference,[],[333,403,30])). % 58.99/59.66 cnf(1033,plain, % 58.99/59.66 (~P2(x10331,f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(rename_variables,[],[379])). % 58.99/59.66 cnf(1034,plain, % 58.99/59.66 (~P1(f16(f16(a2,a17),f14(a2)))+E(f16(a2,a17),f16(f16(f16(a2,a17),f14(a2)),a17))), % 58.99/59.66 inference(scs_inference,[],[379,1033,47,370,366,312,30,132])). % 58.99/59.66 cnf(1038,plain, % 58.99/59.66 (E(f16(f16(f16(a2,a17),f14(a2)),a17),f16(a2,a17))+~P1(f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[379,1033,47,370,366,312,30,132,2])). % 58.99/59.66 cnf(1041,plain, % 58.99/59.66 (~E(f15(a1,f14(a2)),f16(f16(f16(a2,a17),f14(a2)),a17))+~P1(f16(f16(a2,a17),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[379,1033,403,47,370,390,366,312,30,132,2,70,3])). % 58.99/59.66 cnf(1043,plain, % 58.99/59.66 (~E(f15(a1,a17),f16(f16(a2,a17),a17))), % 58.99/59.66 inference(scs_inference,[],[367,403,30])). % 58.99/59.66 cnf(1044,plain, % 58.99/59.66 (~P2(x10441,f16(f16(a2,a17),a17))), % 58.99/59.66 inference(rename_variables,[],[403])). % 58.99/59.66 cnf(1045,plain, % 58.99/59.66 (~P1(f16(f16(a2,a17),a17))+E(f16(f16(a2,a17),a17),f16(f16(f16(a2,a17),a17),a17))), % 58.99/59.66 inference(scs_inference,[],[367,403,1044,312,30,132])). % 58.99/59.66 cnf(1049,plain, % 58.99/59.66 (E(f16(f16(f16(a2,a17),a17),a17),f16(f16(a2,a17),a17))+~P1(f16(f16(a2,a17),a17))), % 58.99/59.66 inference(scs_inference,[],[367,403,1044,312,30,132,2])). % 58.99/59.66 cnf(1052,plain, % 58.99/59.66 (~E(f15(a1,f14(a2)),f16(f16(f16(a2,a17),a17),a17))+~P1(f16(f16(a2,a17),a17))), % 58.99/59.66 inference(scs_inference,[],[367,403,1044,379,1021,312,30,132,2,70,3])). % 58.99/59.66 cnf(1141,plain, % 58.99/59.66 (~E(f21(f19(a18)),a17)), % 58.99/59.66 inference(scs_inference,[],[52,71,68])). % 58.99/59.66 cnf(1148,plain, % 58.99/59.66 (~E(f21(f19(a18)),f14(a2))), % 58.99/59.66 inference(scs_inference,[],[1141,154,728,742,784,3])). % 58.99/59.66 cnf(1159,plain, % 58.99/59.66 (~P1(f16(f16(a2,a17),f14(a2)))+E(f16(f16(a2,a17),f14(a2)),f16(f16(f16(a2,a17),f14(a2)),f14(a2)))), % 58.99/59.66 inference(scs_inference,[],[379,140,1148,137,311,151,132])). % 58.99/59.66 cnf(1163,plain, % 58.99/59.66 (E(f16(f16(f16(a2,a17),f14(a2)),f14(a2)),f16(f16(a2,a17),f14(a2)))+~P1(f16(f16(a2,a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[379,140,1148,137,311,151,132,2])). % 58.99/59.67 cnf(1462,plain, % 58.99/59.67 (P6(f16(f16(a2,f14(a2)),f14(a2)),f16(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[462,366,534,106])). % 58.99/59.67 cnf(1469,plain, % 58.99/59.67 (P6(f16(f16(a2,f14(a2)),f14(a2)),f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[52,564,462,370,468,366,534,106,104,35,36])). % 58.99/59.67 cnf(1478,plain, % 58.99/59.67 (P6(f16(a2,f14(a2)),f16(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[532,337,366,331,1469,36,106])). % 58.99/59.67 cnf(1481,plain, % 58.99/59.67 (~P6(f15(a1,f14(a2)),f16(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[532,337,370,315,366,331,1469,36,106,104])). % 58.99/59.67 cnf(1490,plain, % 58.99/59.67 (P6(f16(a2,a17),f16(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[564,370,1478,366,36,106])). % 58.99/59.67 cnf(1491,plain, % 58.99/59.67 (~P2(x14911,f16(a2,a17))), % 58.99/59.67 inference(rename_variables,[],[370])). % 58.99/59.67 cnf(1493,plain, % 58.99/59.67 (~P6(f15(a1,a17),f16(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[564,370,1491,349,1478,366,36,106,104])). % 58.99/59.67 cnf(1507,plain, % 58.99/59.67 (P6(f16(a2,a17),f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[564,1490,36])). % 58.99/59.67 cnf(1508,plain, % 58.99/59.67 (P6(a2,f16(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[564,140,1490,366,137,36,106])). % 58.99/59.67 cnf(1523,plain, % 58.99/59.67 (P6(a2,f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[564,1508,36])). % 58.99/59.67 cnf(1524,plain, % 58.99/59.67 (P6(f16(f16(a2,a17),f14(a2)),f16(a2,a17))+~P1(f16(f16(a2,a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[564,379,1508,366,36,106])). % 58.99/59.67 cnf(1531,plain, % 58.99/59.67 (P6(f16(f16(a2,a17),a17),f16(a2,a17))+~P1(f16(f16(a2,a17),a17))), % 58.99/59.67 inference(scs_inference,[],[532,403,366,1507,36,106])). % 58.99/59.67 cnf(1550,plain, % 58.99/59.67 (~P1(f16(f16(a2,a17),f14(a2)))+E(f16(f16(a2,f14(a2)),f14(a2)),f16(f16(f16(a2,a17),f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[532,379,462,534,1523,311,36,132])). % 58.99/59.67 cnf(1630,plain, % 58.99/59.67 (P2(f21(f19(a18)),a1)), % 58.99/59.67 inference(scs_inference,[],[52,82,71])). % 58.99/59.67 cnf(1807,plain, % 58.99/59.67 (~E(a22,f16(f16(a2,a17),a17))), % 58.99/59.67 inference(scs_inference,[],[403,47,30])). % 58.99/59.67 cnf(1808,plain, % 58.99/59.67 (~P2(x18081,f16(f16(a2,a17),a17))), % 58.99/59.67 inference(rename_variables,[],[403])). % 58.99/59.67 cnf(1809,plain, % 58.99/59.67 (~P1(f16(f16(a2,a17),a17))+E(f16(a2,f14(a2)),f16(f16(f16(a2,a17),a17),a17))), % 58.99/59.67 inference(scs_inference,[],[403,1808,337,47,331,312,30,132])). % 58.99/59.67 cnf(1813,plain, % 58.99/59.67 (E(f16(f16(f16(a2,a17),a17),a17),f16(a2,f14(a2)))+~P1(f16(f16(a2,a17),a17))), % 58.99/59.67 inference(scs_inference,[],[403,1808,337,47,331,312,30,132,2])). % 58.99/59.67 cnf(1814,plain, % 58.99/59.67 (E(f16(a2,a17),f16(f16(f16(a2,a17),a17),a17))+~P1(f16(f16(a2,a17),a17))), % 58.99/59.67 inference(scs_inference,[],[381,403,1808,337,47,331,312,30,132,2,3])). % 58.99/59.67 cnf(1821,plain, % 58.99/59.67 (~P1(f16(f16(a2,a17),a17))+E(f16(f16(a2,a17),a17),f16(f16(f16(a2,a17),a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[40,403,337,331,323,334,311,129,148,149,132])). % 58.99/59.67 cnf(1825,plain, % 58.99/59.67 (~P1(f16(f16(a2,a17),a17))+E(a2,f16(f16(f16(a2,a17),a17),a17))), % 58.99/59.67 inference(scs_inference,[],[403,140,137,312,132])). % 58.99/59.67 cnf(1831,plain, % 58.99/59.67 (~P1(f16(f16(a2,a17),a17))+P6(f12(a2,a17),f16(f16(f16(a2,a17),a17),a17))), % 58.99/59.67 inference(scs_inference,[],[403,140,137,312,132,243,255,233])). % 58.99/59.67 cnf(1833,plain, % 58.99/59.67 (~P1(f16(f16(a2,a17),a17))+P6(f12(a2,f14(a2)),f16(f16(f16(a2,a17),a17),a17))), % 58.99/59.67 inference(scs_inference,[],[403,140,137,312,132,243,255,233,2,294])). % 58.99/59.67 cnf(1923,plain, % 58.99/59.67 (P6(f16(a2,a17),a18)), % 58.99/59.67 inference(scs_inference,[],[41,370,366,106])). % 58.99/59.67 cnf(1924,plain, % 58.99/59.67 (~P2(x19241,f16(a2,a17))), % 58.99/59.67 inference(rename_variables,[],[370])). % 58.99/59.67 cnf(1933,plain, % 58.99/59.67 (P4(f16(f16(a2,a17),a17))), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,534,366,369,312,106,114,132,2,31])). % 58.99/59.67 cnf(1934,plain, % 58.99/59.67 (~P5(f16(f16(a2,a17),a17))), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,534,366,368,369,312,106,114,132,2,31,34])). % 58.99/59.67 cnf(1935,plain, % 58.99/59.67 (P1(f16(f16(a2,a17),a17))), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,534,366,368,369,312,106,114,132,2,31,34,28])). % 58.99/59.67 cnf(1937,plain, % 58.99/59.67 (~P2(x19371,f16(f16(f16(a2,a17),a17),a17))), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,403,534,366,368,369,312,106,114,132,2,31,34,28,36,150])). % 58.99/59.67 cnf(1945,plain, % 58.99/59.67 (E(a2,f16(f16(a2,a17),a17))), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,403,624,1141,534,366,368,369,312,106,114,132,2,31,34,28,36,150,98,151,405,410])). % 58.99/59.67 cnf(1946,plain, % 58.99/59.67 (P6(f16(f16(a2,a17),a17),a1)), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,403,624,1141,534,366,368,369,312,106,114,132,2,31,34,28,36,150,98,151,405,410,670])). % 58.99/59.67 cnf(1949,plain, % 58.99/59.67 (P6(f16(f16(a2,a17),a17),a22)), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,403,624,1141,534,366,368,369,312,106,114,132,2,31,34,28,36,150,98,151,405,410,670,858,862,951])). % 58.99/59.67 cnf(1951,plain, % 58.99/59.67 (E(f16(f16(f16(a2,a17),a17),a17),f16(f16(a2,a17),a17))), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,403,624,1141,534,366,368,369,312,106,114,132,2,31,34,28,36,150,98,151,405,410,670,858,862,951,1045,1049])). % 58.99/59.67 cnf(1953,plain, % 58.99/59.67 (P6(f16(f16(a2,a17),a17),f16(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,403,624,1141,534,366,368,369,312,106,114,132,2,31,34,28,36,150,98,151,405,410,670,858,862,951,1045,1049,1052,1531])). % 58.99/59.67 cnf(1955,plain, % 58.99/59.67 (E(f16(f16(f16(a2,a17),a17),a17),f16(a2,f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,403,624,1141,534,366,368,369,312,106,114,132,2,31,34,28,36,150,98,151,405,410,670,858,862,951,1045,1049,1052,1531,1809,1813])). % 58.99/59.67 cnf(1956,plain, % 58.99/59.67 (E(f16(a2,a17),f16(f16(f16(a2,a17),a17),a17))), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,403,624,1141,534,366,368,369,312,106,114,132,2,31,34,28,36,150,98,151,405,410,670,858,862,951,1045,1049,1052,1531,1809,1813,1814])). % 58.99/59.67 cnf(1957,plain, % 58.99/59.67 (E(f16(f16(a2,a17),a17),f16(f16(f16(a2,a17),a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,403,624,1141,534,366,368,369,312,106,114,132,2,31,34,28,36,150,98,151,405,410,670,858,862,951,1045,1049,1052,1531,1809,1813,1814,1821])). % 58.99/59.67 cnf(1959,plain, % 58.99/59.67 (P6(f12(a2,a17),f16(f16(f16(a2,a17),a17),a17))), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,403,624,1141,534,366,368,369,312,106,114,132,2,31,34,28,36,150,98,151,405,410,670,858,862,951,1045,1049,1052,1531,1809,1813,1814,1821,1825,1831])). % 58.99/59.67 cnf(1960,plain, % 58.99/59.67 (P6(f12(a2,f14(a2)),f16(f16(f16(a2,a17),a17),a17))), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,403,624,1141,534,366,368,369,312,106,114,132,2,31,34,28,36,150,98,151,405,410,670,858,862,951,1045,1049,1052,1531,1809,1813,1814,1821,1825,1831,1833])). % 58.99/59.67 cnf(1970,plain, % 58.99/59.67 (P1(f16(f16(f16(a2,a17),a17),a17))), % 58.99/59.67 inference(scs_inference,[],[41,370,1924,1462,333,403,468,898,624,1141,629,534,366,368,369,312,106,114,132,2,31,34,28,36,150,98,151,405,410,670,858,862,951,1045,1049,1052,1531,1809,1813,1814,1821,1825,1831,1833,243,294,255,233,3,35,37,104,148,89])). % 58.99/59.67 cnf(1979,plain, % 58.99/59.67 (P4(f16(f16(f16(a2,a17),a17),a17))), % 58.99/59.67 inference(scs_inference,[],[1956,1955,326,369,2,3,31])). % 58.99/59.67 cnf(1981,plain, % 58.99/59.67 (P6(f16(f16(a2,a17),a17),f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[564,1953,1956,1955,326,332,369,2,3,31,34,36])). % 58.99/59.67 cnf(1982,plain, % 58.99/59.67 (P1(f16(f16(f16(a2,a17),a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[564,1953,1956,1955,1957,326,332,1935,369,2,3,31,34,36,28])). % 58.99/59.67 cnf(1983,plain, % 58.99/59.67 (P6(f16(f16(a2,a17),a17),a18)), % 58.99/59.67 inference(scs_inference,[],[41,564,403,1953,1956,1955,1957,326,332,1935,369,2,3,31,34,36,28,106])). % 58.99/59.67 cnf(1984,plain, % 58.99/59.67 (~P2(x19841,f16(f16(a2,a17),a17))), % 58.99/59.67 inference(rename_variables,[],[403])). % 58.99/59.67 cnf(1988,plain, % 58.99/59.67 (~P6(a1,f16(f16(a2,a17),a17))), % 58.99/59.67 inference(scs_inference,[],[41,564,403,1953,915,1946,1937,1956,1955,1957,326,40,332,1970,1935,369,311,2,3,31,34,36,28,106,150,98])). % 58.99/59.67 cnf(1993,plain, % 58.99/59.67 (P6(f16(a2,f14(a2)),a18)), % 58.99/59.67 inference(scs_inference,[],[41,564,1478,403,1984,1148,1953,915,1946,1937,1956,1955,1957,1923,326,40,366,331,332,1970,1935,369,311,2,3,31,34,36,28,106,150,98,151,114])). % 58.99/59.67 cnf(1995,plain, % 58.99/59.67 (E(f16(a2,a17),f16(f16(a2,a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[41,370,564,1478,403,1984,1148,1953,915,1946,1937,1956,1955,1957,1923,326,40,366,331,332,1970,1935,369,311,2,3,31,34,36,28,106,150,98,151,114,132])). % 58.99/59.67 cnf(2007,plain, % 58.99/59.67 (E(f16(f16(f16(a2,a17),a17),f14(a2)),f16(f16(a2,a17),a17))), % 58.99/59.67 inference(scs_inference,[],[1957,2])). % 58.99/59.67 cnf(2010,plain, % 58.99/59.67 (P1(f16(f16(a2,a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[1951,1957,1043,1995,366,1933,2,3,31,28])). % 58.99/59.67 cnf(2011,plain, % 58.99/59.67 (P6(f16(f16(a2,a17),a17),a2)), % 58.99/59.67 inference(scs_inference,[],[550,1951,1957,1043,1995,366,1933,1981,2,3,31,28,36])). % 58.99/59.67 cnf(2013,plain, % 58.99/59.67 (P6(f16(f16(a2,a17),f14(a2)),a18)), % 58.99/59.67 inference(scs_inference,[],[41,550,379,1951,1957,1043,1995,366,1934,1933,1981,2,3,31,28,36,34,106])). % 58.99/59.67 cnf(2014,plain, % 58.99/59.67 (~P2(x20141,f16(f16(a2,a17),f14(a2)))), % 58.99/59.67 inference(rename_variables,[],[379])). % 58.99/59.67 cnf(2016,plain, % 58.99/59.67 (~P2(x20161,f16(f16(f16(a2,a17),f14(a2)),a17))), % 58.99/59.67 inference(scs_inference,[],[41,550,379,2014,1951,1957,1043,1995,366,1934,1933,1981,312,2,3,31,28,36,34,106,150])). % 58.99/59.67 cnf(2020,plain, % 58.99/59.67 (~P2(x20201,f16(f16(f16(a2,a17),a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[41,550,370,379,2014,1951,1957,1043,1995,154,366,1934,1933,1981,312,2,3,31,28,36,34,106,150,101,110])). % 58.99/59.67 cnf(2027,plain, % 58.99/59.67 (E(f16(f16(a2,f14(a2)),f14(a2)),f16(f16(a2,a17),a17))), % 58.99/59.67 inference(scs_inference,[],[41,550,370,462,379,2014,1951,1957,1043,1807,1949,1995,1141,42,154,534,366,1934,1933,1981,1935,312,2,3,31,28,36,34,106,150,101,110,98,151,132])). % 58.99/59.67 cnf(2031,plain, % 58.99/59.67 (E(f16(f16(a2,a17),f14(a2)),a2)), % 58.99/59.67 inference(scs_inference,[],[41,550,370,462,379,2014,1951,1957,1043,1807,1949,1995,1141,42,154,534,366,1934,1933,1981,1935,312,2,3,31,28,36,34,106,150,101,110,98,151,132,394])). % 58.99/59.67 cnf(2032,plain, % 58.99/59.67 (P6(f16(f16(a2,a17),f14(a2)),a1)), % 58.99/59.67 inference(scs_inference,[],[41,550,370,462,379,2014,1951,1957,1043,1807,1949,1995,1141,42,154,534,366,1934,1933,1981,1935,312,2,3,31,28,36,34,106,150,101,110,98,151,132,394,660])). % 58.99/59.67 cnf(2035,plain, % 58.99/59.67 (E(f16(f16(a2,a17),f14(a2)),f16(f16(f16(a2,a17),f14(a2)),a17))), % 58.99/59.67 inference(scs_inference,[],[41,550,370,462,379,2014,1951,1957,1043,1807,1949,1995,1141,42,154,534,366,1934,1933,1981,1935,312,2,3,31,28,36,34,106,150,101,110,98,151,132,394,660,827,831,881])). % 58.99/59.67 cnf(2040,plain, % 58.99/59.67 (E(a2,f16(f16(f16(a2,a17),f14(a2)),a17))), % 58.99/59.67 inference(scs_inference,[],[41,550,370,462,379,2014,1951,1957,1043,1807,1949,1995,1141,42,154,534,366,1934,1933,1981,1935,312,2,3,31,28,36,34,106,150,101,110,98,151,132,394,660,827,831,881,885,947,1012,1016,1019])). % 58.99/59.67 cnf(2042,plain, % 58.99/59.67 (E(f16(f16(f16(a2,a17),f14(a2)),a17),f16(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[41,550,370,462,379,2014,1951,1957,1043,1807,1949,1995,1141,42,154,534,366,1934,1933,1981,1935,312,2,3,31,28,36,34,106,150,101,110,98,151,132,394,660,827,831,881,885,947,1012,1016,1019,1034,1038])). % 58.99/59.67 cnf(2044,plain, % 58.99/59.67 (E(f16(f16(a2,a17),f14(a2)),f16(f16(f16(a2,a17),f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[41,550,370,462,379,2014,1951,1957,1043,1807,1949,1995,1141,42,154,534,366,1934,1933,1981,1935,312,2,3,31,28,36,34,106,150,101,110,98,151,132,394,660,827,831,881,885,947,1012,1016,1019,1034,1038,1041,1159])). % 58.99/59.67 cnf(2045,plain, % 58.99/59.67 (E(f16(f16(f16(a2,a17),f14(a2)),f14(a2)),f16(f16(a2,a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[41,550,370,462,379,2014,1951,1957,1043,1807,1949,1995,1141,42,154,534,366,1934,1933,1981,1935,312,2,3,31,28,36,34,106,150,101,110,98,151,132,394,660,827,831,881,885,947,1012,1016,1019,1034,1038,1041,1159,1163])). % 58.99/59.67 cnf(2046,plain, % 58.99/59.67 (P6(f16(f16(a2,a17),f14(a2)),f16(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[41,550,370,462,379,2014,1951,1957,1043,1807,1949,1995,1141,42,154,534,366,1934,1933,1981,1935,312,2,3,31,28,36,34,106,150,101,110,98,151,132,394,660,827,831,881,885,947,1012,1016,1019,1034,1038,1041,1159,1163,1524])). % 58.99/59.67 cnf(2047,plain, % 58.99/59.67 (E(f16(f16(a2,f14(a2)),f14(a2)),f16(f16(f16(a2,a17),f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[41,550,370,462,379,2014,1951,1957,1043,1807,1949,1995,1141,42,154,534,366,1934,1933,1981,1935,312,2,3,31,28,36,34,106,150,101,110,98,151,132,394,660,827,831,881,885,947,1012,1016,1019,1034,1038,1041,1159,1163,1524,1550])). % 58.99/59.67 cnf(2055,plain, % 58.99/59.67 (P1(f16(f16(f16(a2,a17),f14(a2)),a17))), % 58.99/59.67 inference(scs_inference,[],[41,550,370,462,379,2014,1951,1957,1043,1807,1949,1995,1141,42,154,534,366,1934,1933,1981,1959,1935,312,311,2,3,31,28,36,34,106,150,101,110,98,151,132,394,660,827,831,881,885,947,1012,1016,1019,1034,1038,1041,1159,1163,1524,1550,243,294,255,233,63,35,89])). % 58.99/59.67 cnf(2064,plain, % 58.99/59.67 (E(a2,f16(f16(a2,a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[2010,400])). % 58.99/59.67 cnf(2069,plain, % 58.99/59.67 (E(f16(f16(f16(a2,a17),a17),f14(a2)),a2)), % 58.99/59.67 inference(scs_inference,[],[1995,2020,1982,2,70])). % 58.99/59.67 cnf(2070,plain, % 58.99/59.67 (~P2(x20701,f16(f16(f16(a2,a17),a17),f14(a2)))), % 58.99/59.67 inference(rename_variables,[],[2020])). % 58.99/59.67 cnf(2073,plain, % 58.99/59.67 (P4(f16(f16(a2,a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[1945,1957,1995,2020,1982,369,2,70,3,31])). % 58.99/59.67 cnf(2075,plain, % 58.99/59.67 (P6(f16(f16(a2,a17),f14(a2)),f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[564,1945,1957,1995,2046,2042,2020,368,1982,369,2,70,3,31,34,36])). % 58.99/59.67 cnf(2076,plain, % 58.99/59.67 (P1(f16(f16(f16(a2,a17),f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[564,1945,1957,1995,2046,2042,2047,2020,534,368,1982,369,2,70,3,31,34,36,28])). % 58.99/59.67 cnf(2077,plain, % 58.99/59.67 (P6(f16(f16(f16(a2,a17),a17),f14(a2)),a18)), % 58.99/59.67 inference(scs_inference,[],[41,564,1945,1957,1995,2046,2042,2047,2020,2070,534,368,1982,369,2,70,3,31,34,36,28,106])). % 58.99/59.67 cnf(2084,plain, % 58.99/59.67 (~P2(x20841,f16(f16(f16(a2,a17),f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[41,370,564,180,1945,1957,1995,2016,2046,2042,2047,2020,2070,2045,534,366,368,2055,1982,369,311,2,70,3,31,34,36,28,106,150,101,110])). % 58.99/59.67 cnf(2086,plain, % 58.99/59.67 (~P6(a1,f16(f16(a2,a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[41,370,564,180,1945,1957,1995,890,2032,2016,2046,2042,2047,2020,2070,2045,40,534,366,368,2055,1982,2010,369,311,2,70,3,31,34,36,28,106,150,101,110,98])). % 58.99/59.67 cnf(2110,plain, % 58.99/59.67 (E(f16(f16(f16(a2,a17),f14(a2)),f14(a2)),a2)), % 58.99/59.67 inference(scs_inference,[],[2027,2084,2064,2076,294,233,2,70])). % 58.99/59.67 cnf(2111,plain, % 58.99/59.67 (~P2(x21111,f16(f16(f16(a2,a17),f14(a2)),f14(a2)))), % 58.99/59.67 inference(rename_variables,[],[2084])). % 58.99/59.67 cnf(2113,plain, % 58.99/59.67 (~P5(f16(f16(f16(a2,a17),f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[2027,2084,2064,2076,294,233,2,70,63])). % 58.99/59.67 cnf(2119,plain, % 58.99/59.67 (P6(f16(f16(f16(a2,a17),f14(a2)),f14(a2)),a18)), % 58.99/59.67 inference(scs_inference,[],[41,317,2027,2035,2007,2084,2111,2064,2077,898,193,2011,2073,2076,294,233,2,70,63,31,3,35,36,106])). % 58.99/59.67 cnf(2134,plain, % 58.99/59.67 (E(f16(f16(f16(a2,a17),f14(a2)),a17),a2)), % 58.99/59.67 inference(scs_inference,[],[2040,2])). % 58.99/59.67 cnf(2136,plain, % 58.99/59.67 (P4(f16(f16(f16(a2,a17),f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[2040,2044,1983,219,2073,2,35,31])). % 58.99/59.67 cnf(2138,plain, % 58.99/59.67 (P6(f16(f16(a2,a17),f14(a2)),a2)), % 58.99/59.67 inference(scs_inference,[],[550,1951,2040,2044,1983,915,219,2075,2073,2,35,31,3,36])). % 58.99/59.67 cnf(2141,plain, % 58.99/59.67 (~P6(a18,f16(f16(a2,a17),a17))), % 58.99/59.67 inference(scs_inference,[],[41,550,1951,2040,2044,1983,915,2020,898,219,2075,1935,2073,1982,311,2,35,31,3,36,150,98])). % 58.99/59.67 cnf(2162,plain, % 58.99/59.67 (~P6(a18,f16(f16(a2,a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[41,317,2042,2047,402,879,2013,2119,2020,193,2010,2138,1982,312,2,35,3,36,150,98])). % 58.99/59.67 cnf(2210,plain, % 58.99/59.67 (P6(f16(f16(f16(a2,a17),f14(a2)),f14(a2)),a1)), % 58.99/59.67 inference(scs_inference,[],[41,370,1148,2069,2110,337,2084,524,329,366,331,2076,1993,311,2,3,150,98,151,132,255])). % 58.99/59.67 cnf(2213,plain, % 58.99/59.67 (P6(f12(a2,a17),f16(f16(f16(a2,a17),f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[41,370,1148,2069,2110,337,2084,524,329,366,331,2076,1993,311,2,3,150,98,151,132,255,243,294,233])). % 58.99/59.67 cnf(2642,plain, % 58.99/59.67 (E(f16(a2,a17),f16(f16(f16(a2,a17),a17),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[403,370,366,1935,311,132])). % 58.99/59.67 cnf(2646,plain, % 58.99/59.67 (E(f16(f16(f16(a2,a17),a17),f14(a2)),f16(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[403,370,366,1935,311,132,2])). % 58.99/59.67 cnf(2854,plain, % 58.99/59.67 (E(f16(f16(f16(a2,a17),a17),f14(a2)),f16(f16(a2,f14(a2)),f14(a2)))), % 58.99/59.67 inference(scs_inference,[],[337,2020,1148,392,331,1982,594,311,151,132])). % 58.99/59.67 cnf(2866,plain, % 58.99/59.67 (P8(a17,f19(a22))), % 58.99/59.67 inference(scs_inference,[],[466,1970,66,64,73])). % 58.99/59.67 cnf(2874,plain, % 58.99/59.67 (~E(f21(f19(a22)),a17)), % 58.99/59.67 inference(scs_inference,[],[466,1970,66,64,73,69,83,84,68])). % 58.99/59.67 cnf(2876,plain, % 58.99/59.67 (P2(f21(f19(a22)),a1)), % 58.99/59.67 inference(scs_inference,[],[466,1970,66,64,73,69,83,84,68,82])). % 58.99/59.67 cnf(2883,plain, % 58.99/59.67 (E(f15(f16(f16(f16(a2,a17),a17),f14(a2)),x28831),f15(f16(a2,a17),x28831))), % 58.99/59.67 inference(scs_inference,[],[2646,466,1970,66,64,73,69,83,84,68,82,13,16,23,26,27,11])). % 58.99/59.67 cnf(2885,plain, % 58.99/59.67 (E(f16(f16(f16(f16(a2,a17),a17),f14(a2)),x28851),f16(f16(a2,a17),x28851))), % 58.99/59.67 inference(scs_inference,[],[2646,466,1970,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14])). % 58.99/59.67 cnf(2902,plain, % 58.99/59.67 (P8(f19(a22),f19(a18))), % 58.99/59.67 inference(scs_inference,[],[1493,2646,53,466,1970,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81])). % 58.99/59.67 cnf(2906,plain, % 58.99/59.67 (P8(f19(a18),f19(a22))), % 58.99/59.67 inference(scs_inference,[],[1493,2646,53,466,1970,54,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80])). % 58.99/59.67 cnf(2922,plain, % 58.99/59.67 (E(f15(f16(a18,f19(a22)),f19(a22)),a18)), % 58.99/59.67 inference(scs_inference,[],[158,2136,1493,2646,2134,53,466,1970,2055,54,207,1630,1141,2076,41,40,312,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108])). % 58.99/59.67 cnf(2927,plain, % 58.99/59.67 (P1(f12(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[48,158,416,2136,1493,2646,1959,2134,53,466,1970,2055,54,207,1630,1141,164,2076,41,40,312,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108,86,30,76])). % 58.99/59.67 cnf(2930,plain, % 58.99/59.67 (P3(f19(a22))), % 58.99/59.67 inference(scs_inference,[],[48,158,416,2136,1493,2646,1959,2134,53,466,1970,2055,54,207,1630,1141,164,2076,41,40,312,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108,86,30,76,31,77])). % 58.99/59.67 cnf(2933,plain, % 58.99/59.67 (~P8(f21(f19(a22)),f14(a2))), % 58.99/59.67 inference(scs_inference,[],[48,158,416,2136,1493,2113,2646,44,1959,2134,53,466,1970,2055,54,207,1630,1141,164,2076,154,41,40,312,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108,86,30,76,31,77,34,33])). % 58.99/59.67 cnf(2934,plain, % 58.99/59.67 (P2(f6(a1),a1)), % 58.99/59.67 inference(scs_inference,[],[48,158,416,2136,1493,2113,2646,44,1959,2134,53,466,1970,2055,54,207,1630,1141,164,2076,154,41,40,312,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108,86,30,76,31,77,34,33,70])). % 58.99/59.67 cnf(2945,plain, % 58.99/59.67 (P5(f15(a1,a17))), % 58.99/59.67 inference(scs_inference,[],[48,158,416,2141,612,2136,2854,1493,2113,2646,44,1959,2134,53,466,159,1970,2055,54,207,1630,1141,164,2076,154,41,40,312,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108,86,30,76,31,77,34,33,70,35,29,32,3,36,93,94,95])). % 58.99/59.67 cnf(2947,plain, % 58.99/59.67 (P1(f15(f16(f16(f16(a2,a17),a17),f14(a2)),a17))), % 58.99/59.67 inference(scs_inference,[],[48,158,416,2141,612,2136,2854,1493,2113,2646,44,1959,2134,53,466,159,1970,2055,54,207,1630,1141,164,2076,154,366,41,40,312,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108,86,30,76,31,77,34,33,70,35,29,32,3,36,93,94,95,88])). % 58.99/59.67 cnf(2953,plain, % 58.99/59.67 (E(f16(f15(f16(a2,a17),a17),a17),f16(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[48,158,416,2141,612,2136,2854,1493,2113,2646,44,1959,2134,53,466,159,1970,2055,2213,54,207,1630,1141,162,164,2076,50,203,154,370,366,41,40,312,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108,86,30,76,31,77,34,33,70,35,29,32,3,36,93,94,95,88,100,90,107])). % 58.99/59.67 cnf(2954,plain, % 58.99/59.67 (~P2(x29541,f16(a2,a17))), % 58.99/59.67 inference(rename_variables,[],[370])). % 58.99/59.67 cnf(2956,plain, % 58.99/59.67 (~P2(x29561,f12(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[48,158,416,2141,612,2136,2854,1493,2113,2646,1937,44,1959,2134,53,466,159,1970,2055,2213,54,207,1630,1141,162,164,2076,50,203,154,370,366,41,40,312,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108,86,30,76,31,77,34,33,70,35,29,32,3,36,93,94,95,88,100,90,107,104])). % 58.99/59.67 cnf(2965,plain, % 58.99/59.67 (P4(f12(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[48,158,416,2141,612,2136,1979,2854,1493,2113,173,2646,1937,2016,44,1959,2134,53,466,159,1970,2055,2213,54,207,414,1630,1141,162,164,59,2076,50,203,154,166,370,366,41,40,312,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108,86,30,76,31,77,34,33,70,35,29,32,3,36,93,94,95,88,100,90,107,104,118,121,106,87])). % 58.99/59.67 cnf(2969,plain, % 58.99/59.67 (~P8(a5,f19(a22))), % 58.99/59.67 inference(scs_inference,[],[48,158,240,416,2141,612,2136,1979,2854,1493,2113,173,2646,1937,2016,44,1959,2134,53,466,159,1970,2055,2213,54,207,414,1630,1141,162,164,59,2076,50,203,154,166,370,366,41,40,312,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108,86,30,76,31,77,34,33,70,35,29,32,3,36,93,94,95,88,100,90,107,104,118,121,106,87,96,117])). % 58.99/59.67 cnf(2976,plain, % 58.99/59.67 (E(f14(f12(a2,f14(a2))),f14(a2))), % 58.99/59.67 inference(scs_inference,[],[48,158,240,416,2141,612,2136,1979,2854,1493,2113,173,2646,1937,2016,44,1959,2134,53,466,159,369,1970,2055,2213,54,207,414,1630,1141,214,162,43,164,59,2076,50,250,203,154,166,370,2954,366,41,40,312,137,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108,86,30,76,31,77,34,33,70,35,29,32,3,36,93,94,95,88,100,90,107,104,118,121,106,87,96,117,105,112,123])). % 58.99/59.67 cnf(2997,plain, % 58.99/59.67 (~P8(a5,f11(a22,a5))), % 58.99/59.67 inference(scs_inference,[],[48,158,240,416,480,2141,612,2136,1979,2854,1493,2113,173,2646,1937,2016,44,1959,2134,53,2210,466,159,369,1970,2055,2213,367,54,207,414,1630,1141,214,162,43,164,59,2076,50,250,140,203,154,166,370,2954,366,41,40,312,137,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108,86,30,76,31,77,34,33,70,35,29,32,3,36,93,94,95,88,100,90,107,104,118,121,106,87,96,117,105,112,123,101,110,98,132,258,279,451,566,303,256,259,309])). % 58.99/59.67 cnf(3002,plain, % 58.99/59.67 (~P5(f12(a2,a17))), % 58.99/59.67 inference(scs_inference,[],[48,158,240,416,480,2141,612,2136,1979,2854,1493,2113,173,2646,1937,2016,44,1959,2134,53,2210,466,159,369,1970,2055,2213,367,54,207,414,1630,1141,214,162,43,164,59,2076,50,250,140,203,154,166,370,2954,366,41,40,312,137,66,64,73,69,83,84,68,82,13,16,23,26,27,11,12,14,15,17,18,19,20,21,22,24,25,5,6,7,8,9,10,427,81,91,80,4,2,141,142,75,61,62,85,108,86,30,76,31,77,34,33,70,35,29,32,3,36,93,94,95,88,100,90,107,104,118,121,106,87,96,117,105,112,123,101,110,98,132,258,279,451,566,303,256,259,309,423,497,74,65])). % 58.99/59.67 cnf(3092,plain, % 58.99/59.67 (~P2(x30921,f12(a2,a17))), % 58.99/59.67 inference(rename_variables,[],[2956])). % 58.99/59.67 cnf(3103,plain, % 58.99/59.67 (~P2(x31031,f12(a2,a17))), % 58.99/59.67 inference(rename_variables,[],[2956])). % 58.99/59.67 cnf(3129,plain, % 58.99/59.67 ($false), % 58.99/59.67 inference(scs_inference,[],[48,183,2927,2945,2956,3092,3103,2965,2997,3002,2902,2906,2930,2866,2934,2969,2933,1988,2086,2162,2874,2876,2922,2953,2976,2947,2883,2885,555,1481,2642,1979,1960,2031,58,44,46,47,2010,414,193,1970,466,156,534,184,462,49,166,41,42,40,180,84,69,68,73,5,258,6,82,27,25,66,21,81,64,14,24,83,80,17,427,16,23,22,10,20,91,7,18,11,26,19,12,9,8,13,15,4,2,108,62,85,141,75,142,61,76,30,77,28,35,70,33,34,32,3,36,100,107,94,95,111,93,150,104,120,121,106,96,87,105,117]), % 58.99/59.67 ['proof']). % 58.99/59.67 % SZS output end Proof % 58.99/59.67 % Total time :58.320000s %------------------------------------------------------------------------------