%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM539+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n001.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 59.75s 59.82s % Output : CNFRefutation 59.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.01/0.12 % Problem : NUM539+1 : TPTP v8.2.0. Released v4.0.0. % 0.01/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n001.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Sun Jun 23 00:56:54 EDT 2024 % 0.13/0.33 % CPUTime : % 0.51/0.57 start to proof:theBenchmark % 59.75/59.79 %------------------------------------------- % 59.75/59.79 % File :CSE---1.7 % 59.75/59.79 % Problem :theBenchmark % 59.75/59.79 % Transform :cnf % 59.75/59.79 % Format :tptp:raw % 59.75/59.79 % Command :java -jar mcs_scs.jar %d %s % 59.75/59.79 % 59.75/59.79 % Result :Theorem 59.140000s % 59.75/59.79 % Output :CNFRefutation 59.140000s % 59.75/59.79 %------------------------------------------- % 59.75/59.80 %------------------------------------------------------------------------------ % 59.75/59.80 % File : NUM539+1 : TPTP v8.2.0. Released v4.0.0. % 59.75/59.80 % Domain : Number Theory % 59.75/59.80 % Problem : Ramsey's Infinite Theorem 07, 00 expansion % 59.75/59.80 % Version : Especial. % 59.75/59.80 % English : % 59.75/59.80 % 59.75/59.80 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 59.75/59.80 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 59.75/59.80 % Source : [Pas08] % 59.75/59.80 % Names : ramsey_07.00 [Pas08] % 59.75/59.80 % 59.75/59.80 % Status : Theorem % 59.75/59.80 % Rating : 0.25 v8.2.0, 0.22 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.17 v7.3.0, 0.14 v7.1.0, 0.04 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.17 v6.2.0, 0.24 v6.1.0, 0.30 v6.0.0, 0.35 v5.5.0, 0.37 v5.4.0, 0.39 v5.3.0, 0.33 v5.2.0, 0.20 v5.1.0, 0.19 v5.0.0, 0.25 v4.1.0, 0.35 v4.0.1, 0.70 v4.0.0 % 59.75/59.80 % Syntax : Number of formulae : 51 ( 3 unt; 6 def) % 59.75/59.80 % Number of atoms : 184 ( 28 equ) % 59.75/59.80 % Maximal formula atoms : 8 ( 3 avg) % 59.75/59.80 % Number of connectives : 146 ( 13 ~; 3 |; 50 &) % 59.75/59.80 % ( 11 <=>; 69 =>; 0 <=; 0 <~>) % 59.75/59.80 % Maximal formula depth : 12 ( 5 avg) % 59.75/59.80 % Maximal term depth : 4 ( 1 avg) % 59.75/59.80 % Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty) % 59.75/59.80 % Number of functors : 11 ( 11 usr; 5 con; 0-2 aty) % 59.75/59.80 % Number of variables : 83 ( 80 !; 3 ?) % 59.75/59.80 % SPC : FOF_THM_RFO_SEQ % 59.75/59.80 % 59.75/59.80 % Comments : Problem generated by the SAD system [VLP07] % 59.75/59.80 %------------------------------------------------------------------------------ % 59.75/59.80 fof(mSetSort,axiom, % 59.75/59.80 ! [W0] : % 59.75/59.80 ( aSet0(W0) % 59.75/59.80 => $true ) ). % 59.75/59.80 % 59.75/59.80 fof(mElmSort,axiom, % 59.75/59.80 ! [W0] : % 59.75/59.80 ( aElement0(W0) % 59.75/59.80 => $true ) ). % 59.75/59.80 % 59.75/59.80 fof(mEOfElem,axiom, % 59.75/59.80 ! [W0] : % 59.75/59.80 ( aSet0(W0) % 59.75/59.80 => ! [W1] : % 59.75/59.80 ( aElementOf0(W1,W0) % 59.75/59.80 => aElement0(W1) ) ) ). % 59.75/59.80 % 59.75/59.80 fof(mFinRel,axiom, % 59.75/59.80 ! [W0] : % 59.75/59.80 ( aSet0(W0) % 59.75/59.80 => ( isFinite0(W0) % 59.75/59.80 => $true ) ) ). % 59.75/59.80 % 59.75/59.80 fof(mDefEmp,definition, % 59.75/59.80 ! [W0] : % 59.75/59.80 ( W0 = slcrc0 % 59.75/59.80 <=> ( aSet0(W0) % 59.75/59.80 & ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 59.75/59.80 % 59.75/59.80 fof(mEmpFin,axiom, % 59.75/59.80 isFinite0(slcrc0) ). % 59.75/59.80 % 59.75/59.80 fof(mCntRel,axiom, % 59.75/59.80 ! [W0] : % 59.75/59.80 ( aSet0(W0) % 59.75/59.80 => ( isCountable0(W0) % 59.75/59.81 => $true ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mCountNFin,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( ( aSet0(W0) % 59.75/59.81 & isCountable0(W0) ) % 59.75/59.81 => ~ isFinite0(W0) ) ). % 59.75/59.81 % 59.75/59.81 fof(mCountNFin_01,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( ( aSet0(W0) % 59.75/59.81 & isCountable0(W0) ) % 59.75/59.81 => W0 != slcrc0 ) ). % 59.75/59.81 % 59.75/59.81 fof(mDefSub,definition, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aSet0(W0) % 59.75/59.81 => ! [W1] : % 59.75/59.81 ( aSubsetOf0(W1,W0) % 59.75/59.81 <=> ( aSet0(W1) % 59.75/59.81 & ! [W2] : % 59.75/59.81 ( aElementOf0(W2,W1) % 59.75/59.81 => aElementOf0(W2,W0) ) ) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mSubFSet,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( ( aSet0(W0) % 59.75/59.81 & isFinite0(W0) ) % 59.75/59.81 => ! [W1] : % 59.75/59.81 ( aSubsetOf0(W1,W0) % 59.75/59.81 => isFinite0(W1) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mSubRefl,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aSet0(W0) % 59.75/59.81 => aSubsetOf0(W0,W0) ) ). % 59.75/59.81 % 59.75/59.81 fof(mSubASymm,axiom, % 59.75/59.81 ! [W0,W1] : % 59.75/59.81 ( ( aSet0(W0) % 59.75/59.81 & aSet0(W1) ) % 59.75/59.81 => ( ( aSubsetOf0(W0,W1) % 59.75/59.81 & aSubsetOf0(W1,W0) ) % 59.75/59.81 => W0 = W1 ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mSubTrans,axiom, % 59.75/59.81 ! [W0,W1,W2] : % 59.75/59.81 ( ( aSet0(W0) % 59.75/59.81 & aSet0(W1) % 59.75/59.81 & aSet0(W2) ) % 59.75/59.81 => ( ( aSubsetOf0(W0,W1) % 59.75/59.81 & aSubsetOf0(W1,W2) ) % 59.75/59.81 => aSubsetOf0(W0,W2) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mDefCons,definition, % 59.75/59.81 ! [W0,W1] : % 59.75/59.81 ( ( aSet0(W0) % 59.75/59.81 & aElement0(W1) ) % 59.75/59.81 => ! [W2] : % 59.75/59.81 ( W2 = sdtpldt0(W0,W1) % 59.75/59.81 <=> ( aSet0(W2) % 59.75/59.81 & ! [W3] : % 59.75/59.81 ( aElementOf0(W3,W2) % 59.75/59.81 <=> ( aElement0(W3) % 59.75/59.81 & ( aElementOf0(W3,W0) % 59.75/59.81 | W3 = W1 ) ) ) ) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mDefDiff,definition, % 59.75/59.81 ! [W0,W1] : % 59.75/59.81 ( ( aSet0(W0) % 59.75/59.81 & aElement0(W1) ) % 59.75/59.81 => ! [W2] : % 59.75/59.81 ( W2 = sdtmndt0(W0,W1) % 59.75/59.81 <=> ( aSet0(W2) % 59.75/59.81 & ! [W3] : % 59.75/59.81 ( aElementOf0(W3,W2) % 59.75/59.81 <=> ( aElement0(W3) % 59.75/59.81 & aElementOf0(W3,W0) % 59.75/59.81 & W3 != W1 ) ) ) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mConsDiff,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aSet0(W0) % 59.75/59.81 => ! [W1] : % 59.75/59.81 ( aElementOf0(W1,W0) % 59.75/59.81 => sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mDiffCons,axiom, % 59.75/59.81 ! [W0,W1] : % 59.75/59.81 ( ( aElement0(W0) % 59.75/59.81 & aSet0(W1) ) % 59.75/59.81 => ( ~ aElementOf0(W0,W1) % 59.75/59.81 => sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mCConsSet,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aElement0(W0) % 59.75/59.81 => ! [W1] : % 59.75/59.81 ( ( aSet0(W1) % 59.75/59.81 & isCountable0(W1) ) % 59.75/59.81 => isCountable0(sdtpldt0(W1,W0)) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mCDiffSet,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aElement0(W0) % 59.75/59.81 => ! [W1] : % 59.75/59.81 ( ( aSet0(W1) % 59.75/59.81 & isCountable0(W1) ) % 59.75/59.81 => isCountable0(sdtmndt0(W1,W0)) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mFConsSet,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aElement0(W0) % 59.75/59.81 => ! [W1] : % 59.75/59.81 ( ( aSet0(W1) % 59.75/59.81 & isFinite0(W1) ) % 59.75/59.81 => isFinite0(sdtpldt0(W1,W0)) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mFDiffSet,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aElement0(W0) % 59.75/59.81 => ! [W1] : % 59.75/59.81 ( ( aSet0(W1) % 59.75/59.81 & isFinite0(W1) ) % 59.75/59.81 => isFinite0(sdtmndt0(W1,W0)) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mNATSet,axiom, % 59.75/59.81 ( aSet0(szNzAzT0) % 59.75/59.81 & isCountable0(szNzAzT0) ) ). % 59.75/59.81 % 59.75/59.81 fof(mZeroNum,axiom, % 59.75/59.81 aElementOf0(sz00,szNzAzT0) ). % 59.75/59.81 % 59.75/59.81 fof(mSuccNum,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 => ( aElementOf0(szszuzczcdt0(W0),szNzAzT0) % 59.75/59.81 & szszuzczcdt0(W0) != sz00 ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mSuccEquSucc,axiom, % 59.75/59.81 ! [W0,W1] : % 59.75/59.81 ( ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 & aElementOf0(W1,szNzAzT0) ) % 59.75/59.81 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 59.75/59.81 => W0 = W1 ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mNatExtra,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 => ( W0 = sz00 % 59.75/59.81 | ? [W1] : % 59.75/59.81 ( aElementOf0(W1,szNzAzT0) % 59.75/59.81 & W0 = szszuzczcdt0(W1) ) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mNatNSucc,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 => W0 != szszuzczcdt0(W0) ) ). % 59.75/59.81 % 59.75/59.81 fof(mLessRel,axiom, % 59.75/59.81 ! [W0,W1] : % 59.75/59.81 ( ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 & aElementOf0(W1,szNzAzT0) ) % 59.75/59.81 => ( sdtlseqdt0(W0,W1) % 59.75/59.81 => $true ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mZeroLess,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 => sdtlseqdt0(sz00,W0) ) ). % 59.75/59.81 % 59.75/59.81 fof(mNoScLessZr,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 => ~ sdtlseqdt0(szszuzczcdt0(W0),sz00) ) ). % 59.75/59.81 % 59.75/59.81 fof(mSuccLess,axiom, % 59.75/59.81 ! [W0,W1] : % 59.75/59.81 ( ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 & aElementOf0(W1,szNzAzT0) ) % 59.75/59.81 => ( sdtlseqdt0(W0,W1) % 59.75/59.81 <=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mLessSucc,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 => sdtlseqdt0(W0,szszuzczcdt0(W0)) ) ). % 59.75/59.81 % 59.75/59.81 fof(mLessRefl,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 => sdtlseqdt0(W0,W0) ) ). % 59.75/59.81 % 59.75/59.81 fof(mLessASymm,axiom, % 59.75/59.81 ! [W0,W1] : % 59.75/59.81 ( ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 & aElementOf0(W1,szNzAzT0) ) % 59.75/59.81 => ( ( sdtlseqdt0(W0,W1) % 59.75/59.81 & sdtlseqdt0(W1,W0) ) % 59.75/59.81 => W0 = W1 ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mLessTrans,axiom, % 59.75/59.81 ! [W0,W1,W2] : % 59.75/59.81 ( ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 & aElementOf0(W1,szNzAzT0) % 59.75/59.81 & aElementOf0(W2,szNzAzT0) ) % 59.75/59.81 => ( ( sdtlseqdt0(W0,W1) % 59.75/59.81 & sdtlseqdt0(W1,W2) ) % 59.75/59.81 => sdtlseqdt0(W0,W2) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mLessTotal,axiom, % 59.75/59.81 ! [W0,W1] : % 59.75/59.81 ( ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 & aElementOf0(W1,szNzAzT0) ) % 59.75/59.81 => ( sdtlseqdt0(W0,W1) % 59.75/59.81 | sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mIHSort,axiom, % 59.75/59.81 ! [W0,W1] : % 59.75/59.81 ( ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 & aElementOf0(W1,szNzAzT0) ) % 59.75/59.81 => ( iLess0(W0,W1) % 59.75/59.81 => $true ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mIH,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aElementOf0(W0,szNzAzT0) % 59.75/59.81 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 59.75/59.81 % 59.75/59.81 fof(mCardS,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aSet0(W0) % 59.75/59.81 => aElement0(sbrdtbr0(W0)) ) ). % 59.75/59.81 % 59.75/59.81 fof(mCardNum,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aSet0(W0) % 59.75/59.81 => ( aElementOf0(sbrdtbr0(W0),szNzAzT0) % 59.75/59.81 <=> isFinite0(W0) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mCardEmpty,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aSet0(W0) % 59.75/59.81 => ( sbrdtbr0(W0) = sz00 % 59.75/59.81 <=> W0 = slcrc0 ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mCardCons,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( ( aSet0(W0) % 59.75/59.81 & isFinite0(W0) ) % 59.75/59.81 => ! [W1] : % 59.75/59.81 ( aElement0(W1) % 59.75/59.81 => ( ~ aElementOf0(W1,W0) % 59.75/59.81 => sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ) ). % 59.75/59.81 % 59.75/59.81 fof(mCardDiff,axiom, % 59.75/59.81 ! [W0] : % 59.75/59.81 ( aSet0(W0) % 59.75/59.81 => ! [W1] : % 59.75/59.81 ( ( isFinite0(W0) % 59.75/59.81 & aElementOf0(W1,W0) ) % 59.75/59.82 => szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ) ). % 59.75/59.82 % 59.75/59.82 fof(mCardSub,axiom, % 59.75/59.82 ! [W0] : % 59.75/59.82 ( aSet0(W0) % 59.75/59.82 => ! [W1] : % 59.75/59.82 ( ( isFinite0(W0) % 59.75/59.82 & aSubsetOf0(W1,W0) ) % 59.75/59.82 => sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 59.75/59.82 % 59.75/59.82 fof(mCardSubEx,axiom, % 59.75/59.82 ! [W0,W1] : % 59.75/59.82 ( ( aSet0(W0) % 59.75/59.82 & aElementOf0(W1,szNzAzT0) ) % 59.75/59.82 => ( ( isFinite0(W0) % 59.75/59.82 & sdtlseqdt0(W1,sbrdtbr0(W0)) ) % 59.75/59.82 => ? [W2] : % 59.75/59.82 ( aSubsetOf0(W2,W0) % 59.75/59.82 & sbrdtbr0(W2) = W1 ) ) ) ). % 59.75/59.82 % 59.75/59.82 fof(mDefMin,definition, % 59.75/59.82 ! [W0] : % 59.75/59.82 ( ( aSubsetOf0(W0,szNzAzT0) % 59.75/59.82 & W0 != slcrc0 ) % 59.75/59.82 => ! [W1] : % 59.75/59.82 ( W1 = szmzizndt0(W0) % 59.75/59.82 <=> ( aElementOf0(W1,W0) % 59.75/59.82 & ! [W2] : % 59.75/59.82 ( aElementOf0(W2,W0) % 59.75/59.82 => sdtlseqdt0(W1,W2) ) ) ) ) ). % 59.75/59.82 % 59.75/59.82 fof(mDefMax,definition, % 59.75/59.82 ! [W0] : % 59.75/59.82 ( ( aSubsetOf0(W0,szNzAzT0) % 59.75/59.82 & isFinite0(W0) % 59.75/59.82 & W0 != slcrc0 ) % 59.75/59.82 => ! [W1] : % 59.75/59.82 ( W1 = szmzazxdt0(W0) % 59.75/59.82 <=> ( aElementOf0(W1,W0) % 59.75/59.82 & ! [W2] : % 59.75/59.82 ( aElementOf0(W2,W0) % 59.75/59.82 => sdtlseqdt0(W2,W1) ) ) ) ) ). % 59.75/59.82 % 59.75/59.82 fof(m__1779,hypothesis, % 59.75/59.82 ( aSubsetOf0(xS,szNzAzT0) % 59.75/59.82 & aSubsetOf0(xT,szNzAzT0) % 59.75/59.82 & xS != slcrc0 % 59.75/59.82 & xT != slcrc0 ) ). % 59.75/59.82 % 59.75/59.82 fof(m__1802,hypothesis, % 59.75/59.82 ( aElementOf0(szmzizndt0(xS),xT) % 59.75/59.82 & aElementOf0(szmzizndt0(xT),xS) ) ). % 59.75/59.82 % 59.75/59.82 fof(m__,conjecture, % 59.75/59.82 szmzizndt0(xS) = szmzizndt0(xT) ). % 59.75/59.82 % 59.75/59.82 %------------------------------------------------------------------------------ % 59.75/59.82 %------------------------------------------- % 59.75/59.82 % Proof found % 59.75/59.82 % SZS status Theorem for theBenchmark % 59.75/59.82 % SZS output start Proof % 59.75/59.82 %ClaNum:122(EqnAxiom:39) % 59.75/59.82 %VarNum:507(SingletonVarNum:155) % 59.75/59.82 %MaxLitNum:8 % 59.75/59.82 %MaxfuncDepth:3 % 59.75/59.82 %SharedTerms:18 % 59.75/59.82 %goalClause: 50 % 59.75/59.82 %singleGoalClaCount:1 % 59.75/59.82 [40]P1(a1) % 59.75/59.82 [41]P4(a2) % 59.75/59.82 [42]P5(a1) % 59.75/59.82 [43]P2(a14,a1) % 59.75/59.82 [44]P6(a15,a1) % 59.75/59.82 [45]P6(a19,a1) % 59.75/59.82 [48]~E(a15,a2) % 59.75/59.82 [49]~E(a19,a2) % 59.75/59.82 [46]P2(f16(a15),a19) % 59.75/59.82 [47]P2(f16(a19),a15) % 59.75/59.82 [50]~E(f16(a19),f16(a15)) % 59.75/59.82 [51]P1(x511)+~E(x511,a2) % 59.75/59.82 [57]~P1(x571)+P6(x571,x571) % 59.75/59.82 [62]~P2(x621,a1)+P8(a14,x621) % 59.75/59.82 [67]P8(x671,x671)+~P2(x671,a1) % 59.75/59.82 [55]~P1(x551)+P3(f3(x551)) % 59.75/59.82 [59]~P2(x591,a1)+~E(f18(x591),a14) % 59.75/59.82 [60]~P2(x601,a1)+~E(f18(x601),x601) % 59.75/59.82 [68]~P2(x681,a1)+P2(f18(x681),a1) % 59.75/59.82 [69]~P2(x691,a1)+P8(x691,f18(x691)) % 59.75/59.82 [70]~P2(x701,a1)+P7(x701,f18(x701)) % 59.75/59.82 [77]~P2(x771,a1)+~P8(f18(x771),a14) % 59.75/59.82 [58]~P2(x582,x581)+~E(x581,a2) % 59.75/59.82 [54]~P1(x541)+~P5(x541)+~E(x541,a2) % 59.75/59.82 [56]~P4(x561)+~P5(x561)+~P1(x561) % 59.75/59.82 [52]~P1(x521)+~E(x521,a2)+E(f3(x521),a14) % 59.75/59.82 [53]~P1(x531)+E(x531,a2)+~E(f3(x531),a14) % 59.75/59.82 [61]~P1(x611)+P2(f4(x611),x611)+E(x611,a2) % 59.75/59.82 [64]~P1(x641)+~P4(x641)+P2(f3(x641),a1) % 59.75/59.82 [71]~P2(x711,a1)+E(x711,a14)+P2(f5(x711),a1) % 59.75/59.82 [72]~P1(x721)+P4(x721)+~P2(f3(x721),a1) % 59.75/59.82 [63]~P2(x631,a1)+E(x631,a14)+E(f18(f5(x631)),x631) % 59.75/59.82 [65]~P6(x651,x652)+P1(x651)+~P1(x652) % 59.75/59.82 [66]~P2(x661,x662)+P3(x661)+~P1(x662) % 59.75/59.82 [94]~P1(x941)+~P2(x942,x941)+E(f12(f13(x941,x942),x942),x941) % 59.75/59.82 [73]~P4(x732)+~P6(x731,x732)+P4(x731)+~P1(x732) % 59.75/59.82 [76]P2(x762,x761)+~E(x762,f16(x761))+~P6(x761,a1)+E(x761,a2) % 59.75/59.82 [79]~P1(x791)+~P3(x792)+~P4(x791)+P4(f12(x791,x792)) % 59.75/59.82 [80]~P1(x801)+~P3(x802)+~P4(x801)+P4(f13(x801,x802)) % 59.75/59.82 [81]~P1(x811)+~P3(x812)+~P5(x811)+P5(f12(x811,x812)) % 59.75/59.82 [82]~P1(x821)+~P3(x822)+~P5(x821)+P5(f13(x821,x822)) % 59.75/59.82 [83]E(x831,x832)+~E(f18(x831),f18(x832))+~P2(x832,a1)+~P2(x831,a1) % 59.75/59.82 [86]~P1(x862)+~P4(x862)+~P6(x861,x862)+P8(f3(x861),f3(x862)) % 59.75/59.82 [92]~P1(x921)+~P1(x922)+P6(x921,x922)+P2(f6(x922,x921),x921) % 59.75/59.82 [97]P8(x971,x972)+P8(f18(x972),x971)+~P2(x972,a1)+~P2(x971,a1) % 59.75/59.82 [104]~P8(x1041,x1042)+~P2(x1042,a1)+~P2(x1041,a1)+P8(f18(x1041),f18(x1042)) % 59.75/59.82 [106]~P1(x1061)+~P1(x1062)+P6(x1061,x1062)+~P2(f6(x1062,x1061),x1062) % 59.75/59.82 [107]P8(x1071,x1072)+~P2(x1072,a1)+~P2(x1071,a1)+~P8(f18(x1071),f18(x1072)) % 59.75/59.82 [93]P2(x932,x931)+~P1(x931)+~P3(x932)+E(f13(f12(x931,x932),x932),x931) % 59.75/59.82 [110]~P1(x1101)+~P4(x1101)+~P2(x1102,x1101)+E(f18(f3(f13(x1101,x1102))),f3(x1101)) % 59.75/59.82 [90]~P1(x902)+~P6(x903,x902)+P2(x901,x902)+~P2(x901,x903) % 59.75/59.82 [74]~P1(x742)+~P3(x743)+P1(x741)+~E(x741,f12(x742,x743)) % 59.75/59.82 [75]~P1(x752)+~P3(x753)+P1(x751)+~E(x751,f13(x752,x753)) % 59.75/59.82 [84]~P1(x842)+~P1(x841)+~P6(x842,x841)+~P6(x841,x842)+E(x841,x842) % 59.75/59.82 [103]~P8(x1032,x1031)+~P8(x1031,x1032)+E(x1031,x1032)+~P2(x1032,a1)+~P2(x1031,a1) % 59.75/59.82 [78]~P4(x781)+P2(x782,x781)+~E(x782,f17(x781))+~P6(x781,a1)+E(x781,a2) % 59.75/59.82 [105]~P2(x1052,x1051)+P2(f9(x1051,x1052),x1051)+~P6(x1051,a1)+E(x1051,a2)+E(x1052,f16(x1051)) % 59.75/59.82 [111]~P1(x1111)+~P4(x1111)+~P2(x1112,a1)+~P8(x1112,f3(x1111))+P6(f10(x1111,x1112),x1111) % 59.75/59.82 [112]~P2(x1122,x1121)+~P6(x1121,a1)+~P8(x1122,f9(x1121,x1122))+E(x1121,a2)+E(x1122,f16(x1121)) % 59.75/59.82 [98]P2(x982,x981)+~P1(x981)+~P3(x982)+~P4(x981)+E(f3(f12(x981,x982)),f18(f3(x981))) % 59.75/59.82 [109]~P1(x1091)+~P4(x1091)+~P2(x1092,a1)+~P8(x1092,f3(x1091))+E(f3(f10(x1091,x1092)),x1092) % 59.75/59.82 [91]~P2(x913,x911)+P8(x912,x913)+~E(x912,f16(x911))+~P6(x911,a1)+E(x911,a2) % 59.75/59.82 [87]~P1(x874)+~P3(x872)+~P2(x871,x873)+~E(x871,x872)+~E(x873,f13(x874,x872)) % 59.75/59.82 [88]~P1(x883)+~P3(x884)+~P2(x881,x882)+P3(x881)+~E(x882,f12(x883,x884)) % 59.75/59.82 [89]~P1(x893)+~P3(x894)+~P2(x891,x892)+P3(x891)+~E(x892,f13(x893,x894)) % 59.75/59.82 [96]~P1(x962)+~P3(x964)+~P2(x961,x963)+P2(x961,x962)+~E(x963,f13(x962,x964)) % 59.75/59.82 [108]~P4(x1081)+~P2(x1082,x1081)+P2(f11(x1081,x1082),x1081)+~P6(x1081,a1)+E(x1081,a2)+E(x1082,f17(x1081)) % 59.75/59.82 [113]~P4(x1131)+~P2(x1132,x1131)+~P6(x1131,a1)+~P8(f11(x1131,x1132),x1132)+E(x1131,a2)+E(x1132,f17(x1131)) % 59.75/59.82 [100]~P1(x1002)+~P1(x1001)+~P6(x1003,x1002)+~P6(x1001,x1003)+P6(x1001,x1002)+~P1(x1003) % 59.75/59.82 [114]~P8(x1141,x1143)+P8(x1141,x1142)+~P8(x1143,x1142)+~P2(x1142,a1)+~P2(x1143,a1)+~P2(x1141,a1) % 59.75/59.82 [95]~P4(x951)+~P2(x952,x951)+P8(x952,x953)+~E(x953,f17(x951))+~P6(x951,a1)+E(x951,a2) % 59.75/59.82 [115]~P1(x1151)+~P1(x1152)+~P3(x1153)+P2(f7(x1152,x1153,x1151),x1151)+~E(f7(x1152,x1153,x1151),x1153)+E(x1151,f13(x1152,x1153)) % 59.75/59.82 [116]~P1(x1161)+~P1(x1162)+~P3(x1163)+P2(f8(x1162,x1163,x1161),x1161)+E(x1161,f12(x1162,x1163))+P3(f8(x1162,x1163,x1161)) % 59.75/59.82 [117]~P1(x1171)+~P1(x1172)+~P3(x1173)+P2(f7(x1172,x1173,x1171),x1171)+E(x1171,f13(x1172,x1173))+P3(f7(x1172,x1173,x1171)) % 59.75/59.82 [118]~P1(x1181)+~P1(x1182)+~P3(x1183)+P2(f7(x1182,x1183,x1181),x1181)+P2(f7(x1182,x1183,x1181),x1182)+E(x1181,f13(x1182,x1183)) % 59.75/59.82 [85]~P1(x854)+~P3(x853)+~P3(x851)+P2(x851,x852)+~E(x851,x853)+~E(x852,f12(x854,x853)) % 59.75/59.82 [99]~P1(x993)+~P3(x992)+~P2(x991,x994)+E(x991,x992)+P2(x991,x993)+~E(x994,f12(x993,x992)) % 59.75/59.82 [101]~P1(x1013)+~P3(x1014)+~P3(x1011)+~P2(x1011,x1013)+P2(x1011,x1012)+~E(x1012,f12(x1013,x1014)) % 59.75/59.82 [119]~P1(x1191)+~P1(x1192)+~P3(x1193)+E(f8(x1192,x1193,x1191),x1193)+P2(f8(x1192,x1193,x1191),x1191)+P2(f8(x1192,x1193,x1191),x1192)+E(x1191,f12(x1192,x1193)) % 59.75/59.82 [120]~P1(x1201)+~P1(x1202)+~P3(x1203)+~E(f8(x1202,x1203,x1201),x1203)+~P2(f8(x1202,x1203,x1201),x1201)+E(x1201,f12(x1202,x1203))+~P3(f8(x1202,x1203,x1201)) % 59.75/59.82 [121]~P1(x1211)+~P1(x1212)+~P3(x1213)+~P2(f8(x1212,x1213,x1211),x1211)+~P2(f8(x1212,x1213,x1211),x1212)+E(x1211,f12(x1212,x1213))+~P3(f8(x1212,x1213,x1211)) % 59.75/59.82 [102]~P1(x1024)+~P3(x1022)+~P3(x1021)+~P2(x1021,x1024)+E(x1021,x1022)+P2(x1021,x1023)+~E(x1023,f13(x1024,x1022)) % 59.75/59.82 [122]~P1(x1221)+~P1(x1222)+~P3(x1223)+E(f7(x1222,x1223,x1221),x1223)+~P2(f7(x1222,x1223,x1221),x1221)+~P2(f7(x1222,x1223,x1221),x1222)+E(x1221,f13(x1222,x1223))+~P3(f7(x1222,x1223,x1221)) % 59.75/59.82 %EqnAxiom % 59.75/59.82 [1]E(x11,x11) % 59.75/59.82 [2]E(x22,x21)+~E(x21,x22) % 59.75/59.82 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.75/59.82 [4]~E(x41,x42)+E(f16(x41),f16(x42)) % 59.75/59.82 [5]~E(x51,x52)+E(f7(x51,x53,x54),f7(x52,x53,x54)) % 59.75/59.82 [6]~E(x61,x62)+E(f7(x63,x61,x64),f7(x63,x62,x64)) % 59.75/59.82 [7]~E(x71,x72)+E(f7(x73,x74,x71),f7(x73,x74,x72)) % 59.75/59.82 [8]~E(x81,x82)+E(f8(x81,x83,x84),f8(x82,x83,x84)) % 59.75/59.82 [9]~E(x91,x92)+E(f8(x93,x91,x94),f8(x93,x92,x94)) % 59.75/59.82 [10]~E(x101,x102)+E(f8(x103,x104,x101),f8(x103,x104,x102)) % 59.75/59.82 [11]~E(x111,x112)+E(f12(x111,x113),f12(x112,x113)) % 59.75/59.82 [12]~E(x121,x122)+E(f12(x123,x121),f12(x123,x122)) % 59.75/59.82 [13]~E(x131,x132)+E(f3(x131),f3(x132)) % 59.75/59.82 [14]~E(x141,x142)+E(f10(x141,x143),f10(x142,x143)) % 59.75/59.82 [15]~E(x151,x152)+E(f10(x153,x151),f10(x153,x152)) % 59.75/59.82 [16]~E(x161,x162)+E(f11(x161,x163),f11(x162,x163)) % 59.75/59.82 [17]~E(x171,x172)+E(f11(x173,x171),f11(x173,x172)) % 59.75/59.82 [18]~E(x181,x182)+E(f18(x181),f18(x182)) % 59.75/59.82 [19]~E(x191,x192)+E(f13(x191,x193),f13(x192,x193)) % 59.75/59.82 [20]~E(x201,x202)+E(f13(x203,x201),f13(x203,x202)) % 59.75/59.82 [21]~E(x211,x212)+E(f4(x211),f4(x212)) % 59.75/59.82 [22]~E(x221,x222)+E(f5(x221),f5(x222)) % 59.75/59.82 [23]~E(x231,x232)+E(f17(x231),f17(x232)) % 59.75/59.82 [24]~E(x241,x242)+E(f6(x241,x243),f6(x242,x243)) % 59.75/59.82 [25]~E(x251,x252)+E(f6(x253,x251),f6(x253,x252)) % 59.75/59.82 [26]~E(x261,x262)+E(f9(x261,x263),f9(x262,x263)) % 59.75/59.82 [27]~E(x271,x272)+E(f9(x273,x271),f9(x273,x272)) % 59.75/59.82 [28]~P1(x281)+P1(x282)+~E(x281,x282) % 59.75/59.82 [29]~P4(x291)+P4(x292)+~E(x291,x292) % 59.75/59.82 [30]~P5(x301)+P5(x302)+~E(x301,x302) % 59.75/59.82 [31]P2(x312,x313)+~E(x311,x312)+~P2(x311,x313) % 59.75/59.82 [32]P2(x323,x322)+~E(x321,x322)+~P2(x323,x321) % 59.75/59.82 [33]P6(x332,x333)+~E(x331,x332)+~P6(x331,x333) % 59.75/59.82 [34]P6(x343,x342)+~E(x341,x342)+~P6(x343,x341) % 59.75/59.82 [35]~P3(x351)+P3(x352)+~E(x351,x352) % 59.75/59.82 [36]P8(x362,x363)+~E(x361,x362)+~P8(x361,x363) % 59.75/59.82 [37]P8(x373,x372)+~E(x371,x372)+~P8(x373,x371) % 59.75/59.82 [38]P7(x382,x383)+~E(x381,x382)+~P7(x381,x383) % 59.75/59.82 [39]P7(x393,x392)+~E(x391,x392)+~P7(x393,x391) % 59.75/59.82 % 59.75/59.82 %------------------------------------------- % 59.75/59.82 cnf(123,plain, % 59.75/59.82 (P1(a2)), % 59.75/59.82 inference(equality_inference,[],[51])). % 59.75/59.82 cnf(124,plain, % 59.75/59.82 (~P1(a2)+E(f3(a2),a14)), % 59.75/59.82 inference(equality_inference,[],[52])). % 59.75/59.82 cnf(125,plain, % 59.75/59.82 (~P5(a2)+~P1(a2)), % 59.75/59.82 inference(equality_inference,[],[54])). % 59.75/59.82 cnf(126,plain, % 59.75/59.82 (~P2(x1261,a2)), % 59.75/59.82 inference(equality_inference,[],[58])). % 59.75/59.82 cnf(127,plain, % 59.75/59.82 (~P1(x1271)+~P3(x1272)+P1(f12(x1271,x1272))), % 59.75/59.82 inference(equality_inference,[],[74])). % 59.75/59.82 cnf(128,plain, % 59.75/59.82 (~P1(x1281)+~P3(x1282)+P1(f13(x1281,x1282))), % 59.75/59.82 inference(equality_inference,[],[75])). % 59.75/59.82 cnf(129,plain, % 59.75/59.82 (P2(f16(x1291),x1291)+~P6(x1291,a1)+E(x1291,a2)), % 59.75/59.82 inference(equality_inference,[],[76])). % 59.75/59.82 cnf(134,plain, % 59.75/59.82 (~P2(x1341,x1342)+P8(f16(x1342),x1341)+~P6(x1342,a1)+E(x1342,a2)), % 59.75/59.82 inference(equality_inference,[],[91])). % 59.75/59.82 cnf(136,plain, % 59.75/59.82 (P2(x1361,x1362)+~P1(x1362)+~P3(x1363)+~P2(x1361,f13(x1362,x1363))), % 59.75/59.82 inference(equality_inference,[],[96])). % 59.75/59.82 cnf(137,plain, % 59.75/59.82 (E(x1371,x1372)+P2(x1371,x1373)+~P1(x1373)+~P3(x1372)+~P2(x1371,f12(x1373,x1372))), % 59.75/59.82 inference(equality_inference,[],[99])). % 59.75/59.82 cnf(138,plain, % 59.75/59.82 (~P2(x1381,x1382)+~P1(x1382)+~P3(x1383)+P2(x1381,f12(x1382,x1383))+~P3(x1381)), % 59.75/59.82 inference(equality_inference,[],[101])). % 59.75/59.82 cnf(140,plain, % 59.75/59.82 (E(f3(a2),a14)), % 59.75/59.82 inference(scs_inference,[],[123,124])). % 59.75/59.82 cnf(141,plain, % 59.75/59.82 (~P5(a2)), % 59.75/59.82 inference(scs_inference,[],[123,125])). % 59.75/59.82 cnf(142,plain, % 59.75/59.82 (~E(a19,a15)), % 59.75/59.82 inference(scs_inference,[],[50,4])). % 59.75/59.82 cnf(143,plain, % 59.75/59.82 (P8(a14,a14)), % 59.75/59.82 inference(scs_inference,[],[50,43,4,67])). % 59.75/59.82 cnf(145,plain, % 59.75/59.82 (P2(f16(a15),a15)), % 59.75/59.82 inference(scs_inference,[],[50,48,43,44,4,67,129])). % 59.75/59.82 cnf(147,plain, % 59.75/59.82 (~P4(a1)), % 59.75/59.82 inference(scs_inference,[],[50,48,40,42,43,44,4,67,129,56])). % 59.75/59.82 cnf(149,plain, % 59.75/59.82 (~E(a1,a2)), % 59.75/59.82 inference(scs_inference,[],[50,48,126,40,42,43,44,4,67,129,56,32])). % 59.75/59.82 cnf(150,plain, % 59.75/59.82 (~P2(x1501,a2)), % 59.75/59.82 inference(rename_variables,[],[126])). % 59.75/59.82 cnf(151,plain, % 59.75/59.82 (~P6(a1,a2)), % 59.75/59.82 inference(scs_inference,[],[50,48,126,123,40,41,42,43,44,4,67,129,56,32,73])). % 59.75/59.82 cnf(153,plain, % 59.75/59.82 (~P6(a19,a2)), % 59.75/59.82 inference(scs_inference,[],[50,48,126,150,123,40,41,42,43,44,46,4,67,129,56,32,73,90])). % 59.75/59.82 cnf(154,plain, % 59.75/59.82 (~P2(x1541,a2)), % 59.75/59.82 inference(rename_variables,[],[126])). % 59.75/59.82 cnf(156,plain, % 59.75/59.82 (P6(a2,a2)), % 59.75/59.82 inference(scs_inference,[],[50,48,126,150,154,123,40,41,42,43,44,46,4,67,129,56,32,73,90,92])). % 59.75/59.82 cnf(159,plain, % 59.75/59.82 (P8(f18(a14),f18(a14))), % 59.75/59.82 inference(scs_inference,[],[50,48,126,150,154,123,40,41,42,43,44,46,4,67,129,56,32,73,90,92,104])). % 59.75/59.82 cnf(161,plain, % 59.75/59.82 (P8(f16(a15),f16(a19))), % 59.75/59.82 inference(scs_inference,[],[50,48,126,150,154,123,40,41,42,43,44,46,47,4,67,129,56,32,73,90,92,104,134])). % 59.75/59.82 cnf(163,plain, % 59.75/59.82 (~P8(f16(a19),f9(a15,f16(a19)))), % 59.75/59.82 inference(scs_inference,[],[50,48,126,150,154,123,40,41,42,43,44,46,47,4,67,129,56,32,73,90,92,104,134,112])). % 59.75/59.82 cnf(165,plain, % 59.75/59.82 (P2(x1651,a1)+~E(a14,x1651)), % 59.75/59.82 inference(scs_inference,[],[50,48,126,150,154,123,40,41,42,43,44,46,47,4,67,129,56,32,73,90,92,104,134,112,31])). % 59.75/59.82 cnf(166,plain, % 59.75/59.82 (~E(a2,a1)), % 59.75/59.82 inference(scs_inference,[],[50,48,126,150,154,123,40,41,42,43,44,46,47,4,67,129,56,32,73,90,92,104,134,112,31,33])). % 59.75/59.82 cnf(171,plain, % 59.75/59.82 (E(a14,f3(a2))), % 59.75/59.82 inference(scs_inference,[],[140,2])). % 59.75/59.82 cnf(172,plain, % 59.75/59.82 (P2(f3(a2),a1)), % 59.75/59.82 inference(scs_inference,[],[140,2,165])). % 59.75/59.82 cnf(175,plain, % 59.75/59.82 (P2(f16(a19),a19)), % 59.75/59.82 inference(scs_inference,[],[140,49,45,2,165,67,129])). % 59.75/59.82 cnf(177,plain, % 59.75/59.82 (P8(a14,f3(a2))), % 59.75/59.82 inference(scs_inference,[],[140,49,45,143,2,165,67,129,37])). % 59.75/59.82 cnf(178,plain, % 59.75/59.82 (P8(f3(a2),a14)), % 59.75/59.82 inference(scs_inference,[],[140,49,45,143,2,165,67,129,37,36])). % 59.75/59.82 cnf(179,plain, % 59.75/59.82 (~P6(a15,a2)), % 59.75/59.82 inference(scs_inference,[],[140,145,49,126,123,45,143,2,165,67,129,37,36,90])). % 59.75/59.82 cnf(182,plain, % 59.75/59.82 (~P2(f9(a15,f16(a19)),a19)), % 59.75/59.82 inference(scs_inference,[],[163,140,145,49,126,123,45,143,2,165,67,129,37,36,90,134])). % 59.75/59.82 cnf(184,plain, % 59.75/59.82 (P8(f18(f3(a2)),f18(f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[163,140,145,49,126,123,45,143,2,165,67,129,37,36,90,134,104])). % 59.75/59.82 cnf(186,plain, % 59.75/59.82 (P6(f10(a2,f3(a2)),a2)), % 59.75/59.82 inference(scs_inference,[],[163,140,145,49,126,123,45,143,41,2,165,67,129,37,36,90,134,104,111])). % 59.75/59.82 cnf(195,plain, % 59.75/59.82 (~E(a2,a19)), % 59.75/59.82 inference(scs_inference,[],[175,156,182,153,31,33])). % 59.75/59.82 cnf(196,plain, % 59.75/59.82 (P8(f16(a15),f16(a15))), % 59.75/59.82 inference(scs_inference,[],[48,145,175,156,44,182,153,31,33,134])). % 59.75/59.82 cnf(198,plain, % 59.75/59.82 (P6(f10(a2,a14),a2)), % 59.75/59.82 inference(scs_inference,[],[48,145,175,123,43,156,44,182,177,153,41,31,33,134,111])). % 59.75/59.82 cnf(200,plain, % 59.75/59.82 (~P3(a14)+P3(f3(a2))), % 59.75/59.82 inference(scs_inference,[],[171,48,145,175,123,43,156,44,182,177,153,41,31,33,134,111,35])). % 59.75/59.82 cnf(205,plain, % 59.75/59.82 (P6(a2,x2051)+~E(a2,x2051)), % 59.75/59.82 inference(scs_inference,[],[171,48,145,175,123,43,156,44,159,182,177,153,41,31,33,134,111,35,30,29,28,36,34])). % 59.75/59.82 cnf(208,plain, % 59.75/59.82 (~E(a2,a15)), % 59.75/59.82 inference(scs_inference,[],[156,179,33])). % 59.75/59.82 cnf(213,plain, % 59.75/59.82 (~E(f10(a2,a14),a1)), % 59.75/59.82 inference(scs_inference,[],[198,151,33])). % 59.75/59.82 cnf(220,plain, % 59.75/59.82 (~P3(f3(a2))+P3(a14)), % 59.75/59.82 inference(scs_inference,[],[140,186,153,33,35])). % 59.75/59.82 cnf(227,plain, % 59.75/59.82 (P6(f10(a2,f3(a2)),x2271)+~E(a2,x2271)), % 59.75/59.82 inference(scs_inference,[],[145,140,179,186,33,30,31,34])). % 59.75/59.82 cnf(239,plain, % 59.75/59.82 (P6(f10(a2,a14),x2391)+~E(a2,x2391)), % 59.75/59.82 inference(scs_inference,[],[47,196,198,184,31,37,36,34])). % 59.75/59.82 cnf(248,plain, % 59.75/59.82 (P8(x2481,f16(a19))+~E(f16(a15),x2481)), % 59.75/59.82 inference(scs_inference,[],[161,36])). % 59.75/59.82 cnf(257,plain, % 59.75/59.82 (~P2(x2571,f13(a2,x2572))+~P3(x2572)), % 59.75/59.82 inference(scs_inference,[],[126,123,136])). % 59.75/59.82 cnf(263,plain, % 59.75/59.82 (~P3(f16(a15))+~P2(f16(a19),f12(a2,f16(a15)))), % 59.75/59.82 inference(scs_inference,[],[50,126,123,137])). % 59.75/59.82 cnf(268,plain, % 59.75/59.82 (~P3(x2681)+E(a2,f13(a2,x2681))), % 59.75/59.82 inference(scs_inference,[],[126,123,118])). % 59.75/59.82 cnf(272,plain, % 59.75/59.82 (~P3(x2721)+P6(a2,f13(a2,x2721))), % 59.75/59.82 inference(scs_inference,[],[126,123,118,205])). % 59.75/59.82 cnf(273,plain, % 59.75/59.82 (~P3(x2731)+P6(f10(a2,f3(a2)),f13(a2,x2731))), % 59.75/59.82 inference(scs_inference,[],[126,123,118,205,227])). % 59.75/59.82 cnf(274,plain, % 59.75/59.82 (~P3(x2741)+P6(f10(a2,a14),f13(a2,x2741))), % 59.75/59.82 inference(scs_inference,[],[126,123,118,205,227,239])). % 59.75/59.82 cnf(275,plain, % 59.75/59.82 (E(f13(a2,x2751),a2)+~P3(x2751)), % 59.75/59.82 inference(scs_inference,[],[126,123,118,205,227,239,2])). % 59.75/59.82 cnf(277,plain, % 59.75/59.82 (~E(a15,f13(a2,x2771))+~P3(x2771)), % 59.75/59.82 inference(scs_inference,[],[48,126,123,118,205,227,239,2,54,3])). % 59.75/59.82 cnf(282,plain, % 59.75/59.82 (P2(f16(a1),a1)), % 59.75/59.82 inference(scs_inference,[],[40,149,57,129])). % 59.75/59.82 cnf(313,plain, % 59.75/59.82 (P2(f16(a1),f12(a1,x3131))+~P3(f16(a1))+~P3(x3131)), % 59.75/59.82 inference(scs_inference,[],[282,44,40,138])). % 59.75/59.82 cnf(351,plain, % 59.75/59.82 (~E(a2,f12(a1,f3(a2)))+~P3(a14)), % 59.75/59.82 inference(scs_inference,[],[172,40,126,200,101])). % 59.75/59.82 cnf(460,plain, % 59.75/59.82 (P2(f16(a15),a1)), % 59.75/59.82 inference(scs_inference,[],[40,145,44,90])). % 59.75/59.82 cnf(462,plain, % 59.75/59.82 (P6(a2,a1)), % 59.75/59.82 inference(scs_inference,[],[40,123,145,126,44,90,92])). % 59.75/59.82 cnf(465,plain, % 59.75/59.82 (P8(f18(f16(a15)),f18(f16(a15)))), % 59.75/59.82 inference(scs_inference,[],[40,123,145,126,196,44,90,92,104])). % 59.75/59.82 cnf(471,plain, % 59.75/59.82 (P2(f16(a19),a1)), % 59.75/59.82 inference(scs_inference,[],[40,175,45,90])). % 59.75/59.82 cnf(475,plain, % 59.75/59.82 (P8(x4751,f16(a19))+~E(f16(a19),x4751)), % 59.75/59.82 inference(scs_inference,[],[40,175,45,90,67,36])). % 59.75/59.82 cnf(476,plain, % 59.75/59.82 (P8(f18(f16(a19)),f18(f16(a19)))), % 59.75/59.82 inference(scs_inference,[],[40,175,45,90,67,36,104])). % 59.75/59.82 cnf(478,plain, % 59.75/59.82 (P8(f18(f16(a15)),x4781)+~E(f18(f16(a15)),x4781)), % 59.75/59.82 inference(scs_inference,[],[40,175,45,465,90,67,36,104,37])). % 59.75/59.82 cnf(481,plain, % 59.75/59.82 (P6(x4811,a1)+~E(a2,x4811)), % 59.75/59.82 inference(scs_inference,[],[40,175,45,462,465,460,90,67,36,104,37,34,31,33])). % 59.75/59.82 cnf(494,plain, % 59.75/59.82 (P8(f18(f16(a19)),x4941)+~E(f18(f16(a19)),x4941)), % 59.75/59.82 inference(scs_inference,[],[476,37])). % 59.75/59.82 cnf(505,plain, % 59.75/59.82 (P6(f10(a2,f3(a2)),a1)+~P1(f10(a2,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[40,123,186,462,100])). % 59.75/59.82 cnf(542,plain, % 59.75/59.82 (P3(a14)), % 59.75/59.82 inference(scs_inference,[],[123,220,55])). % 59.75/59.82 cnf(543,plain, % 59.75/59.82 (P3(f3(a2))), % 59.75/59.82 inference(scs_inference,[],[542,200])). % 59.75/59.82 cnf(544,plain, % 59.75/59.82 (~E(a2,f12(a1,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[542,351])). % 59.75/59.82 cnf(545,plain, % 59.75/59.82 (~P2(x5451,f13(a2,a14))), % 59.75/59.82 inference(scs_inference,[],[123,126,542,136])). % 59.75/59.82 cnf(547,plain, % 59.75/59.82 (P2(a14,f12(a1,a14))), % 59.75/59.82 inference(scs_inference,[],[40,123,126,43,542,136,138])). % 59.75/59.82 cnf(549,plain, % 59.75/59.82 (E(a2,f13(a2,a14))), % 59.75/59.82 inference(scs_inference,[],[40,123,126,43,542,136,138,118])). % 59.75/59.82 cnf(551,plain, % 59.75/59.82 (~P2(x5511,a2)), % 59.75/59.82 inference(rename_variables,[],[126])). % 59.75/59.82 cnf(553,plain, % 59.75/59.82 (P6(f13(a2,a14),a1)), % 59.75/59.82 inference(scs_inference,[],[40,123,126,43,542,136,138,118,481])). % 59.75/59.82 cnf(556,plain, % 59.75/59.82 (P6(a2,f13(a2,a14))), % 59.75/59.82 inference(scs_inference,[],[40,123,126,43,542,136,138,118,481,227,239,205])). % 59.75/59.82 cnf(557,plain, % 59.75/59.82 (E(f13(a2,a14),a2)), % 59.75/59.82 inference(scs_inference,[],[40,123,126,43,542,136,138,118,481,227,239,205,2])). % 59.75/59.82 cnf(562,plain, % 59.75/59.82 (~E(a15,f13(a2,a14))), % 59.75/59.82 inference(scs_inference,[],[40,48,123,126,551,43,542,136,138,118,481,227,239,205,2,54,32,3])). % 59.75/59.82 cnf(563,plain, % 59.75/59.82 (P6(f13(a2,a14),f13(a2,a14))), % 59.75/59.82 inference(scs_inference,[],[40,48,123,126,551,43,542,136,138,118,481,227,239,205,2,54,32,3,33])). % 59.75/59.82 cnf(564,plain, % 59.75/59.82 (P4(f13(a2,a14))), % 59.75/59.82 inference(scs_inference,[],[40,48,123,126,551,43,542,41,136,138,118,481,227,239,205,2,54,32,3,33,29])). % 59.75/59.82 cnf(565,plain, % 59.75/59.82 (P2(f3(a2),f12(a1,a14))), % 59.75/59.82 inference(scs_inference,[],[40,171,48,123,126,551,43,542,41,136,138,118,481,227,239,205,2,54,32,3,33,29,31])). % 59.75/59.82 cnf(566,plain, % 59.75/59.82 (P1(f13(a2,a14))), % 59.75/59.82 inference(scs_inference,[],[40,171,48,123,126,551,43,542,41,136,138,118,481,227,239,205,2,54,32,3,33,29,31,28])). % 59.75/59.82 cnf(567,plain, % 59.75/59.82 (P6(f13(a2,a14),a2)), % 59.75/59.82 inference(scs_inference,[],[40,171,48,123,126,551,43,542,41,136,138,118,481,227,239,205,2,54,32,3,33,29,31,28,34])). % 59.75/59.82 cnf(573,plain, % 59.75/59.82 (~P2(x5731,f13(a2,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[123,126,543,567,151,33,136])). % 59.75/59.82 cnf(575,plain, % 59.75/59.82 (P2(f3(a2),f12(a1,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[40,123,126,172,543,567,151,33,136,138])). % 59.75/59.82 cnf(577,plain, % 59.75/59.82 (E(a2,f13(a2,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[40,123,126,172,543,567,151,33,136,138,118])). % 59.75/59.82 cnf(579,plain, % 59.75/59.82 (~P2(x5791,a2)), % 59.75/59.82 inference(rename_variables,[],[126])). % 59.75/59.82 cnf(581,plain, % 59.75/59.82 (P6(f13(a2,f3(a2)),a1)), % 59.75/59.82 inference(scs_inference,[],[40,123,126,172,543,567,151,33,136,138,118,481])). % 59.75/59.82 cnf(583,plain, % 59.75/59.82 (P6(a2,f13(a2,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[40,123,126,172,543,567,151,33,136,138,118,481,227,205])). % 59.75/59.82 cnf(585,plain, % 59.75/59.82 (E(f13(a2,f3(a2)),a2)), % 59.75/59.82 inference(scs_inference,[],[40,123,126,172,543,567,151,33,136,138,118,481,227,205,239,2])). % 59.75/59.82 cnf(590,plain, % 59.75/59.82 (E(f13(a2,a14),f13(a2,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[40,557,123,126,579,172,543,567,151,33,136,138,118,481,227,205,239,2,54,32,3])). % 59.75/59.82 cnf(591,plain, % 59.75/59.82 (P1(f13(a2,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[40,557,123,126,579,172,543,567,151,33,136,138,118,481,227,205,239,2,54,32,3,28])). % 59.75/59.82 cnf(592,plain, % 59.75/59.82 (P4(f13(a2,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[40,557,123,126,579,172,543,567,151,41,33,136,138,118,481,227,205,239,2,54,32,3,28,29])). % 59.75/59.82 cnf(593,plain, % 59.75/59.82 (P2(a14,f12(a1,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[40,557,140,123,126,579,172,543,567,151,41,33,136,138,118,481,227,205,239,2,54,32,3,28,29,31])). % 59.75/59.82 cnf(600,plain, % 59.75/59.82 (E(f13(a2,f3(a2)),f13(a2,a14))), % 59.75/59.82 inference(scs_inference,[],[590,2])). % 59.75/59.82 cnf(602,plain, % 59.75/59.82 (~E(f10(a2,a14),a19)), % 59.75/59.82 inference(scs_inference,[],[590,585,48,198,153,2,3,33])). % 59.75/59.82 cnf(603,plain, % 59.75/59.82 (~P2(x6031,f13(f13(a2,a14),f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[590,585,48,198,545,566,153,543,2,3,33,136])). % 59.75/59.82 cnf(611,plain, % 59.75/59.82 (P6(f13(a2,a14),f13(a2,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[549,583,33])). % 59.75/59.82 cnf(612,plain, % 59.75/59.82 (~P2(x6121,f13(f13(a2,f3(a2)),a14))), % 59.75/59.82 inference(scs_inference,[],[549,583,573,591,542,33,136])). % 59.75/59.82 cnf(634,plain, % 59.75/59.82 (~P2(x6341,f13(f13(a2,a14),a14))), % 59.75/59.82 inference(scs_inference,[],[545,566,542,136])). % 59.75/59.82 cnf(638,plain, % 59.75/59.82 (~P1(f13(f13(a2,a14),a14))+~E(a15,f13(f13(a2,a14),a14))), % 59.75/59.82 inference(scs_inference,[],[48,545,566,542,136,61,3])). % 59.75/59.82 cnf(642,plain, % 59.75/59.82 (E(a2,f13(f13(a2,a14),a14))+~P1(f13(f13(a2,a14),a14))), % 59.75/59.82 inference(scs_inference,[],[48,141,545,566,542,136,61,3,30,51,2])). % 59.75/59.82 cnf(650,plain, % 59.75/59.82 (~E(f13(a2,a14),a19)), % 59.75/59.82 inference(scs_inference,[],[567,153,33])). % 59.75/59.82 cnf(659,plain, % 59.75/59.82 (~E(f10(a2,a14),a15)), % 59.75/59.82 inference(scs_inference,[],[198,179,33])). % 59.75/59.82 cnf(710,plain, % 59.75/59.82 (~P2(x7101,f13(a1,f3(a2)))+P2(x7101,a1)), % 59.75/59.82 inference(scs_inference,[],[40,543,136])). % 59.75/59.82 cnf(720,plain, % 59.75/59.82 (~P2(x7201,f12(a2,f3(a2)))+E(x7201,f3(a2))), % 59.75/59.82 inference(scs_inference,[],[40,123,126,553,545,566,543,84,134,105,137])). % 59.75/59.82 cnf(727,plain, % 59.75/59.82 (~P2(x7271,f12(f13(a2,a14),f3(a2)))+E(x7271,f3(a2))), % 59.75/59.82 inference(scs_inference,[],[545,566,543,137])). % 59.75/59.82 cnf(757,plain, % 59.75/59.82 (~P2(x7571,f12(a2,a14))+E(x7571,a14)), % 59.75/59.82 inference(scs_inference,[],[123,126,542,137])). % 59.75/59.82 cnf(825,plain, % 59.75/59.82 (~P2(x8251,f12(f13(a2,a14),a14))+E(x8251,a14)), % 59.75/59.82 inference(scs_inference,[],[545,566,542,137])). % 59.75/59.82 cnf(838,plain, % 59.75/59.82 (~P1(f13(f13(a2,a14),a14))+E(f13(f13(a2,a14),a14),f13(a2,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[123,126,634,543,118])). % 59.75/59.82 cnf(842,plain, % 59.75/59.82 (E(f13(a2,f3(a2)),f13(f13(a2,a14),a14))+~P1(f13(f13(a2,a14),a14))), % 59.75/59.82 inference(scs_inference,[],[123,126,634,543,118,2])). % 59.75/59.82 cnf(845,plain, % 59.75/59.82 (E(f13(a2,a14),f13(f13(a2,a14),a14))+~P1(f13(f13(a2,a14),a14))), % 59.75/59.82 inference(scs_inference,[],[590,123,126,603,634,543,118,2,61,3])). % 59.75/59.82 cnf(877,plain, % 59.75/59.82 (P6(f13(a2,f3(a2)),f13(a2,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[590,611,33])). % 59.75/59.82 cnf(878,plain, % 59.75/59.82 (P6(f13(a2,f3(a2)),f13(a2,a14))), % 59.75/59.82 inference(scs_inference,[],[600,590,611,33,34])). % 59.75/59.82 cnf(942,plain, % 59.75/59.82 (P6(f13(a2,f3(a2)),a2)), % 59.75/59.82 inference(scs_inference,[],[585,877,34])). % 59.75/59.82 cnf(943,plain, % 59.75/59.82 (~P6(f12(a1,a14),a2)), % 59.75/59.82 inference(scs_inference,[],[585,126,123,547,877,34,90])). % 59.75/59.82 cnf(946,plain, % 59.75/59.82 (~E(f13(a2,f3(a2)),a1)), % 59.75/59.82 inference(scs_inference,[],[585,126,123,547,877,151,34,90,33])). % 59.75/59.82 cnf(952,plain, % 59.75/59.82 (~E(a2,f12(a1,a14))), % 59.75/59.82 inference(scs_inference,[],[156,943,33])). % 59.75/59.82 cnf(953,plain, % 59.75/59.82 (~P6(f12(a1,f3(a2)),a2)), % 59.75/59.82 inference(scs_inference,[],[126,123,156,575,943,33,90])). % 59.75/59.82 cnf(964,plain, % 59.75/59.82 (P6(f13(f13(a2,a14),a14),a2)+~P1(f13(f13(a2,a14),a14))), % 59.75/59.82 inference(scs_inference,[],[123,634,567,953,33,92])). % 59.75/59.82 cnf(967,plain, % 59.75/59.82 (P6(f13(f13(a2,a14),a14),f13(a2,a14))+~P1(f13(f13(a2,a14),a14))), % 59.75/59.82 inference(scs_inference,[],[123,634,549,567,953,33,92,34])). % 59.75/59.82 cnf(972,plain, % 59.75/59.82 (~E(f13(a2,a14),f12(a1,a14))), % 59.75/59.82 inference(scs_inference,[],[567,943,33])). % 59.75/59.82 cnf(980,plain, % 59.75/59.82 (~P1(f13(f13(a2,a14),a14))+E(f13(f13(a2,a14),a14),f13(a2,a14))), % 59.75/59.82 inference(scs_inference,[],[126,123,634,186,953,542,33,118])). % 59.75/59.82 cnf(995,plain, % 59.75/59.82 (~E(f10(a2,a14),f12(a1,a14))), % 59.75/59.82 inference(scs_inference,[],[198,943,33])). % 59.75/59.82 cnf(1121,plain, % 59.75/59.82 (~E(f18(f18(f16(a1))),a14)), % 59.75/59.82 inference(scs_inference,[],[282,59,68])). % 59.75/59.82 cnf(1129,plain, % 59.75/59.82 (~P2(f18(f18(f16(a1))),f12(a2,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[140,1121,757,825,3,727,720])). % 59.75/59.82 cnf(1151,plain, % 59.75/59.82 (~P2(f18(f3(a2)),f12(a2,f3(a2)))), % 59.75/59.82 inference(scs_inference,[],[172,60,720])). % 59.75/59.82 cnf(1254,plain, % 59.75/59.82 (P6(a2,f13(a2,f8(a1,f3(a2),a2)))), % 59.75/59.82 inference(scs_inference,[],[126,544,123,40,543,272,116])). % 59.75/59.82 cnf(1286,plain, % 59.75/59.82 (E(f13(a2,f8(a1,a14,a2)),a2)), % 59.75/59.82 inference(scs_inference,[],[126,952,123,40,542,275,116])). % 59.75/59.82 cnf(1287,plain, % 59.75/59.82 (~P2(x12871,f13(a2,f8(a1,a14,a2)))), % 59.75/59.82 inference(scs_inference,[],[1286,58])). % 59.75/59.82 cnf(1289,plain, % 59.75/59.82 (P1(f13(a2,f8(a1,a14,a2)))), % 59.75/59.82 inference(scs_inference,[],[1286,58,51])). % 59.75/59.82 cnf(1291,plain, % 59.75/59.82 (E(a2,f13(a2,f8(a1,a14,a2)))), % 59.75/59.82 inference(scs_inference,[],[1286,58,51,2])). % 59.75/59.82 cnf(1292,plain, % 59.75/59.82 (P6(f10(a2,f3(a2)),f13(a2,f8(a1,a14,a2)))), % 59.75/59.82 inference(scs_inference,[],[1286,58,51,2,227])). % 59.75/59.83 cnf(1294,plain, % 59.75/59.83 (~P5(f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(scs_inference,[],[1286,48,58,51,2,227,3,54])). % 59.75/59.83 cnf(1296,plain, % 59.75/59.83 (P4(f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(scs_inference,[],[1286,48,41,58,51,2,227,3,54,29])). % 59.75/59.83 cnf(1297,plain, % 59.75/59.83 (~P2(x12971,f13(f13(a2,f8(a1,a14,a2)),a14))), % 59.75/59.83 inference(scs_inference,[],[1286,48,41,542,58,51,2,227,3,54,29,136])). % 59.75/59.83 cnf(1299,plain, % 59.75/59.83 (P6(f13(a2,f8(a1,a14,a2)),a2)), % 59.75/59.83 inference(scs_inference,[],[1286,48,123,41,542,58,51,2,227,3,54,29,136,92])). % 59.75/59.83 cnf(1301,plain, % 59.75/59.83 (P6(f13(a2,f8(a1,a14,a2)),a1)), % 59.75/59.83 inference(scs_inference,[],[1286,48,123,41,542,58,51,2,227,3,54,29,136,92,481])). % 59.75/59.83 cnf(1302,plain, % 59.75/59.83 (P6(f10(a2,a14),f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(scs_inference,[],[1286,48,123,41,542,58,51,2,227,3,54,29,136,92,481,239])). % 59.75/59.83 cnf(1310,plain, % 59.75/59.83 (P6(f13(a2,f8(a1,a14,a2)),f13(a2,f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[1291,583,33])). % 59.75/59.83 cnf(1311,plain, % 59.75/59.83 (P6(f13(a2,a14),f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(scs_inference,[],[1291,583,567,33,34])). % 59.75/59.83 cnf(1329,plain, % 59.75/59.83 (P6(f13(a2,f3(a2)),f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(scs_inference,[],[1291,942,1254,33,34])). % 59.75/59.83 cnf(1330,plain, % 59.75/59.83 (~P2(x13301,f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[1291,1289,1287,942,1254,543,33,34,136])). % 59.75/59.83 cnf(1332,plain, % 59.75/59.83 (E(f13(a2,f3(a2)),f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(scs_inference,[],[1291,1289,1287,591,942,1254,1310,543,33,34,136,84])). % 59.75/59.83 cnf(1353,plain, % 59.75/59.83 (~P1(f13(f13(a2,f8(a1,a14,a2)),f3(a2)))+P6(f10(a2,f3(a2)),f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[1291,141,1299,1330,943,33,34,61,30,51,2,205,227])). % 59.75/59.83 cnf(1369,plain, % 59.75/59.83 (P6(f13(f13(a2,f8(a1,a14,a2)),f3(a2)),a2)+~P1(f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[123,942,1301,1330,153,33,34,92])). % 59.75/59.83 cnf(1589,plain, % 59.75/59.83 (~P6(a1,f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(scs_inference,[],[1289,147,1296,73])). % 59.75/59.83 cnf(1591,plain, % 59.75/59.83 (~P6(a19,f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(scs_inference,[],[1287,175,1289,147,1296,73,90])). % 59.75/59.83 cnf(1606,plain, % 59.75/59.83 (~P1(f13(f13(a2,a14),a14))+~E(f13(f13(a2,a14),a14),a1)), % 59.75/59.83 inference(scs_inference,[],[1287,145,1289,45,634,1589,1591,34,90,92,33])). % 59.75/59.83 cnf(1609,plain, % 59.75/59.83 (~P6(f12(a1,a14),f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(scs_inference,[],[1287,1289,547,90])). % 59.75/59.83 cnf(1618,plain, % 59.75/59.83 (~P6(f12(a1,f3(a2)),f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(scs_inference,[],[1287,1289,593,90])). % 59.75/59.83 cnf(1803,plain, % 59.75/59.83 (~P2(x18031,f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(rename_variables,[],[1287])). % 59.75/59.83 cnf(1809,plain, % 59.75/59.83 (P4(f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[1287,1803,1289,175,1296,543,32,118,2,29])). % 59.75/59.83 cnf(1810,plain, % 59.75/59.83 (P1(f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[1287,1803,1289,175,1296,543,32,118,2,29,28])). % 59.75/59.83 cnf(1811,plain, % 59.75/59.83 (E(f13(f13(a2,f8(a1,a14,a2)),f3(a2)),a2)), % 59.75/59.83 inference(scs_inference,[],[1287,1803,1289,175,1330,1296,543,32,118,2,29,28,61])). % 59.75/59.83 cnf(1812,plain, % 59.75/59.83 (~P2(x18121,f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(rename_variables,[],[1330])). % 59.75/59.83 cnf(1815,plain, % 59.75/59.83 (E(a2,f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[1291,1287,1803,1289,175,1330,1296,543,32,118,2,29,28,61,35,3])). % 59.75/59.83 cnf(1816,plain, % 59.75/59.83 (~P5(f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[1291,1294,1287,1803,1289,175,1330,1296,543,32,118,2,29,28,61,35,3,30])). % 59.75/59.83 cnf(1817,plain, % 59.75/59.83 (P6(f13(f13(a2,f8(a1,a14,a2)),f3(a2)),f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(scs_inference,[],[1291,1294,1287,1803,1289,175,1330,1812,1296,543,32,118,2,29,28,61,35,3,30,92])). % 59.75/59.83 cnf(1818,plain, % 59.75/59.83 (~P2(x18181,f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(rename_variables,[],[1330])). % 59.75/59.83 cnf(1820,plain, % 59.75/59.83 (~P2(x18201,f13(f13(f13(a2,f8(a1,a14,a2)),f3(a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[1291,1294,1287,1803,1289,175,1330,1812,1818,1296,543,32,118,2,29,28,61,35,3,30,92,136])). % 59.75/59.83 cnf(1839,plain, % 59.75/59.83 (P6(f10(a2,f3(a2)),f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[1810,1353])). % 59.75/59.83 cnf(1840,plain, % 59.75/59.83 (P6(f13(f13(a2,f8(a1,a14,a2)),f3(a2)),a2)), % 59.75/59.83 inference(scs_inference,[],[1810,1369])). % 59.75/59.83 cnf(1843,plain, % 59.75/59.83 (P6(f13(f13(a2,f8(a1,a14,a2)),f3(a2)),a1)), % 59.75/59.83 inference(scs_inference,[],[1815,481])). % 59.75/59.83 cnf(1844,plain, % 59.75/59.83 (P6(f10(a2,a14),f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[1815,481,239])). % 59.75/59.83 cnf(1845,plain, % 59.75/59.83 (~E(f13(f13(a2,f8(a1,a14,a2)),f3(a2)),a1)), % 59.75/59.83 inference(scs_inference,[],[1815,1589,1817,481,239,33])). % 59.75/59.83 cnf(1847,plain, % 59.75/59.83 (~P2(x18471,f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(rename_variables,[],[1287])). % 59.75/59.83 cnf(1854,plain, % 59.75/59.83 (E(f13(f13(a2,f8(a1,a14,a2)),a14),f13(a2,f8(a1,a14,a2)))), % 59.75/59.83 inference(scs_inference,[],[1815,1287,1847,1289,565,1330,1589,1817,1810,542,481,239,33,32,136,118,2])). % 59.75/59.83 cnf(1855,plain, % 59.75/59.83 (P4(f13(f13(a2,f8(a1,a14,a2)),a14))), % 59.75/59.83 inference(scs_inference,[],[1815,1287,1847,1289,565,1330,1589,1817,1810,1296,542,481,239,33,32,136,118,2,29])). % 59.75/59.83 cnf(1858,plain, % 59.75/59.83 (E(a2,f13(f13(a2,f8(a1,a14,a2)),a14))), % 59.75/59.83 inference(scs_inference,[],[1291,1815,1287,1847,1289,565,1330,1589,1817,1810,1296,542,481,239,33,32,136,118,2,29,61,3])). % 59.75/59.83 cnf(1859,plain, % 59.75/59.83 (P1(f13(f13(a2,f8(a1,a14,a2)),a14))), % 59.75/59.83 inference(scs_inference,[],[1291,1815,1287,1847,1289,565,1330,1589,1817,1810,1296,542,481,239,33,32,136,118,2,29,61,3,28])). % 59.75/59.83 cnf(1860,plain, % 59.75/59.83 (~P5(f13(f13(a2,f8(a1,a14,a2)),a14))), % 59.75/59.83 inference(scs_inference,[],[1291,1815,1294,1287,1847,1289,565,1330,1589,1817,1810,1296,542,481,239,33,32,136,118,2,29,61,3,28,30])). % 59.75/59.83 cnf(1868,plain, % 59.75/59.83 (P6(f10(a2,a14),f13(f13(a2,f8(a1,a14,a2)),a14))), % 59.75/59.83 inference(scs_inference,[],[1858,481,239])). % 59.75/59.83 cnf(1869,plain, % 59.75/59.83 (E(f13(f13(a2,f8(a1,a14,a2)),a14),a2)), % 59.75/59.83 inference(scs_inference,[],[1858,481,239,2])). % 59.75/59.83 cnf(1871,plain, % 59.75/59.83 (E(f13(a2,a14),f13(f13(a2,f8(a1,a14,a2)),a14))), % 59.75/59.83 inference(scs_inference,[],[557,1858,481,239,2,205,3])). % 59.75/59.83 cnf(1874,plain, % 59.75/59.83 (~E(f13(f13(a2,f8(a1,a14,a2)),f3(a2)),f12(a1,f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[557,1858,1287,575,1840,953,481,239,2,205,3,32,33])). % 59.75/59.83 cnf(1883,plain, % 59.75/59.83 (E(f13(f13(a2,f8(a1,a14,a2)),a14),f13(a2,a14))), % 59.75/59.83 inference(scs_inference,[],[1871,2])). % 59.75/59.83 cnf(1903,plain, % 59.75/59.83 (P6(x19031,f13(f13(a2,f8(a1,a14,a2)),f3(a2)))+~E(f10(a2,a14),x19031)), % 59.75/59.83 inference(scs_inference,[],[1854,1844,35,33])). % 59.75/59.83 cnf(1913,plain, % 59.75/59.83 (P6(x19131,f13(f13(a2,f8(a1,a14,a2)),f3(a2)))+~E(f10(a2,f3(a2)),x19131)), % 59.75/59.83 inference(scs_inference,[],[1883,1839,35,33])). % 59.75/59.83 cnf(1945,plain, % 59.75/59.83 (~P1(f13(f13(a2,a14),a14))+E(f13(f13(a2,a14),a14),f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[1287,1289,634,543,118])). % 59.75/59.83 cnf(1949,plain, % 59.75/59.83 (E(f13(f13(a2,f8(a1,a14,a2)),f3(a2)),f13(f13(a2,a14),a14))+~P1(f13(f13(a2,a14),a14))), % 59.75/59.83 inference(scs_inference,[],[1287,1289,634,543,118,2])). % 59.75/59.83 cnf(1953,plain, % 59.75/59.83 (E(f13(a2,f3(a2)),f13(f13(a2,f8(a1,a14,a2)),a14))), % 59.75/59.83 inference(scs_inference,[],[1287,1289,573,591,542,118])). % 59.75/59.83 cnf(2072,plain, % 59.75/59.83 (~P2(f3(a1),f13(a1,f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[147,40,710,72])). % 59.75/59.83 cnf(2272,plain, % 59.75/59.83 (P6(f13(a2,f3(a2)),f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[1815,942,34])). % 59.75/59.83 cnf(2279,plain, % 59.75/59.83 (P6(f13(f13(a2,f8(a1,a14,a2)),f3(a2)),f13(a2,a14))), % 59.75/59.83 inference(scs_inference,[],[1815,1840,556,34,33])). % 59.75/59.83 cnf(3228,plain, % 59.75/59.83 (P8(a14,f16(a15))), % 59.75/59.83 inference(scs_inference,[],[460,1859,57,62])). % 59.75/59.83 cnf(3232,plain, % 59.75/59.83 (P8(f16(a15),f18(f16(a15)))), % 59.75/59.83 inference(scs_inference,[],[460,1859,57,62,60,69])). % 59.75/59.83 cnf(3238,plain, % 59.75/59.83 (P2(f18(f16(a15)),a1)), % 59.75/59.83 inference(scs_inference,[],[460,1859,57,62,60,69,70,59,68])). % 59.75/59.83 cnf(3265,plain, % 59.75/59.83 (~P8(f18(f16(a15)),a14)), % 59.75/59.83 inference(scs_inference,[],[1332,460,1859,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77])). % 59.75/59.83 cnf(3268,plain, % 59.75/59.83 (~E(f16(a15),f16(a19))), % 59.75/59.83 inference(scs_inference,[],[50,1332,460,1859,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2])). % 59.75/59.83 cnf(3279,plain, % 59.75/59.83 (P2(f5(f18(f16(a15))),a1)), % 59.75/59.83 inference(scs_inference,[],[50,1332,460,1869,1859,1296,149,542,1289,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71])). % 59.75/59.83 cnf(3281,plain, % 59.75/59.83 (E(f12(f13(a1,f16(a15)),f16(a15)),a1)), % 59.75/59.83 inference(scs_inference,[],[50,1332,460,1869,1859,1296,149,542,1289,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94])). % 59.75/59.83 cnf(3283,plain, % 59.75/59.83 (~P2(f3(a1),a1)), % 59.75/59.83 inference(scs_inference,[],[50,1332,460,1869,147,1859,1296,149,542,1289,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72])). % 59.75/59.83 cnf(3285,plain, % 59.75/59.83 (P3(f16(a15))), % 59.75/59.83 inference(scs_inference,[],[50,1332,460,1869,147,1859,1296,149,542,1289,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66])). % 59.75/59.83 cnf(3289,plain, % 59.75/59.83 (~P8(f18(f16(a15)),f3(a2))), % 59.75/59.83 inference(scs_inference,[],[50,178,1332,460,1869,147,1859,1296,149,140,1855,542,1289,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37])). % 59.75/59.83 cnf(3293,plain, % 59.75/59.83 (~E(a1,f13(f13(a2,f8(a1,a14,a2)),a14))), % 59.75/59.83 inference(scs_inference,[],[50,208,1860,1618,178,1332,42,460,1869,577,147,1859,1296,149,140,1855,542,1289,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30])). % 59.75/59.83 cnf(3294,plain, % 59.75/59.83 (P2(f4(a1),a1)), % 59.75/59.83 inference(scs_inference,[],[50,208,1860,1618,178,1332,42,460,1869,577,147,1859,1296,149,140,1855,542,1289,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30,61])). % 59.75/59.83 cnf(3297,plain, % 59.75/59.83 (P4(f12(f13(a2,f8(a1,a14,a2)),a14))), % 59.75/59.83 inference(scs_inference,[],[50,208,1860,1618,1329,178,1953,1332,42,460,1869,577,147,1859,1296,149,140,1855,542,1289,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30,61,33,79])). % 59.75/59.83 cnf(3299,plain, % 59.75/59.83 (P4(f13(f13(f13(a2,f8(a1,a14,a2)),f3(a2)),a14))), % 59.75/59.83 inference(scs_inference,[],[50,208,1860,1618,1329,178,1953,1332,42,460,1869,577,147,1859,1296,149,140,1809,1810,1855,542,1289,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30,61,33,79,80])). % 59.75/59.83 cnf(3301,plain, % 59.75/59.83 (P5(f12(a1,a14))), % 59.75/59.83 inference(scs_inference,[],[50,208,1860,1618,1329,178,1953,1332,42,460,1869,577,147,1859,1296,149,140,1809,1810,1855,542,1289,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30,61,33,79,80,81])). % 59.75/59.83 cnf(3303,plain, % 59.75/59.83 (P1(f12(f13(a2,f3(a2)),a14))), % 59.75/59.83 inference(scs_inference,[],[50,208,1860,1618,1329,178,1953,1332,42,460,1869,577,147,1859,1296,149,140,1809,1810,1855,542,1289,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30,61,33,79,80,81,74])). % 59.75/59.83 cnf(3310,plain, % 59.75/59.83 (~P2(x33101,f13(a2,a14))), % 59.75/59.83 inference(rename_variables,[],[545])). % 59.75/59.83 cnf(3312,plain, % 59.75/59.83 (P5(f13(a1,a14))), % 59.75/59.83 inference(scs_inference,[],[50,208,1860,1618,1329,178,1953,1332,42,460,1869,577,182,147,1859,1296,149,140,1809,1810,1855,545,566,542,49,1289,45,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30,61,33,79,80,81,74,86,76,93,82])). % 59.75/59.83 cnf(3318,plain, % 59.75/59.83 (~P8(f16(a19),f16(a15))), % 59.75/59.83 inference(scs_inference,[],[50,208,1860,1618,1329,178,1953,1332,42,460,1869,577,182,471,161,147,1859,1296,149,43,140,1809,1810,1855,545,566,542,49,1289,45,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30,61,33,79,80,81,74,86,76,93,82,104,107,103])). % 59.75/59.83 cnf(3322,plain, % 59.75/59.83 (~P2(x33221,f13(a2,a14))), % 59.75/59.83 inference(rename_variables,[],[545])). % 59.75/59.83 cnf(3324,plain, % 59.75/59.83 (E(f3(f10(a2,a14)),a14)), % 59.75/59.83 inference(scs_inference,[],[50,208,1860,1618,1329,178,1953,1332,177,42,460,1869,577,182,471,161,147,1859,1296,46,149,43,140,1809,1810,1855,41,545,3310,566,542,49,1289,45,564,123,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30,61,33,79,80,81,74,86,76,93,82,104,107,103,91,98,109])). % 59.75/59.83 cnf(3331,plain, % 59.75/59.83 (~P2(x33311,f13(f13(a2,f8(a1,a14,a2)),a14))), % 59.75/59.83 inference(rename_variables,[],[1297])). % 59.75/59.83 cnf(3333,plain, % 59.75/59.83 (~P6(a1,f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[50,208,1845,1860,1618,1329,178,1953,1332,177,42,460,1869,593,577,182,1297,471,161,147,1859,1296,46,149,43,140,1809,1810,1855,47,41,545,3310,566,542,543,49,1289,48,171,1843,44,45,564,123,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30,61,33,79,80,81,74,86,76,93,82,104,107,103,91,98,109,105,87,96,84])). % 59.75/59.83 cnf(3343,plain, % 59.75/59.83 (E(f13(f13(a2,f8(a1,a14,a2)),a14),f13(f13(a2,a14),a14))), % 59.75/59.83 inference(scs_inference,[],[50,208,1845,1874,1820,1860,1618,1329,178,1953,1332,177,42,460,1869,593,577,182,1297,3331,471,1589,161,147,1859,1296,46,149,1330,43,140,1809,1810,1855,47,41,545,3310,3322,566,542,543,49,1289,48,171,1843,44,45,564,123,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30,61,33,79,80,81,74,86,76,93,82,104,107,103,91,98,109,105,87,96,84,101,116,100,118])). % 59.75/59.83 cnf(3349,plain, % 59.75/59.83 (E(a2,f13(a2,f16(a15)))), % 59.75/59.83 inference(scs_inference,[],[50,208,1845,1874,1820,1860,1618,1329,178,1953,1332,177,42,460,1869,593,577,182,1297,3331,471,1589,161,147,1859,1296,46,149,1330,43,140,1809,1810,1855,47,41,545,3310,3322,566,542,543,49,1289,48,171,1843,44,45,564,123,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30,61,33,79,80,81,74,86,76,93,82,104,107,103,91,98,109,105,87,96,84,101,116,100,118,257,268])). % 59.75/59.83 cnf(3351,plain, % 59.75/59.83 (P6(a2,f13(a2,f16(a15)))), % 59.75/59.83 inference(scs_inference,[],[50,208,1845,1874,1820,1860,1618,1329,178,1953,1332,177,42,460,1869,593,577,182,1297,3331,471,1589,161,147,1859,1296,46,149,1330,43,140,1809,1810,1855,47,41,545,3310,3322,566,542,543,49,1289,48,171,1843,44,45,564,123,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30,61,33,79,80,81,74,86,76,93,82,104,107,103,91,98,109,105,87,96,84,101,116,100,118,257,268,272])). % 59.75/59.83 cnf(3353,plain, % 59.75/59.83 (E(f13(a2,f16(a15)),a2)), % 59.75/59.83 inference(scs_inference,[],[50,208,1845,1874,1820,1860,1618,1329,178,1953,1332,177,42,460,1869,593,577,182,1297,3331,471,1589,161,147,1859,1296,46,149,1330,43,140,1809,1810,1855,47,41,545,3310,3322,566,542,543,49,1289,48,171,1843,44,45,564,123,40,57,62,60,69,70,59,68,13,18,21,22,23,11,12,14,15,16,17,19,20,24,25,26,27,5,6,7,8,9,10,55,77,4,2,127,128,64,52,53,71,94,72,66,29,36,37,34,32,3,30,61,33,79,80,81,74,86,76,93,82,104,107,103,91,98,109,105,87,96,84,101,116,100,118,257,268,272,275])). % 59.75/59.83 cnf(3390,plain, % 59.75/59.83 (~P2(f16(a19),f12(a2,f16(a15)))), % 59.75/59.83 inference(scs_inference,[],[3285,263])). % 59.75/59.83 cnf(3399,plain, % 59.75/59.83 (P6(a1,a1)), % 59.75/59.83 inference(scs_inference,[],[3294,40,59,57])). % 59.75/59.83 cnf(3401,plain, % 59.75/59.83 (P8(f4(a1),f18(f4(a1)))), % 59.75/59.83 inference(scs_inference,[],[3294,40,59,57,69])). % 59.75/59.83 cnf(3403,plain, % 59.75/59.83 (P3(f3(f13(f13(a2,f8(a1,a14,a2)),f3(a2))))), % 59.75/59.83 inference(scs_inference,[],[3294,1810,40,59,57,69,55])). % 59.75/59.83 cnf(3405,plain, % 59.75/59.83 (P2(f18(f4(a1)),a1)), % 59.75/59.83 inference(scs_inference,[],[3294,1810,40,59,57,69,55,68])). % 59.75/59.83 cnf(3408,plain, % 59.75/59.83 (E(f12(x34081,f3(f10(a2,a14))),f12(x34081,a14))), % 59.75/59.83 inference(scs_inference,[],[3294,3324,1810,40,59,57,69,55,68,17,12])). % 59.75/59.83 cnf(3409,plain, % 59.75/59.83 (P8(a14,f4(a1))), % 59.75/59.83 inference(scs_inference,[],[3294,3324,1810,40,59,57,69,55,68,17,12,62])). % 59.75/59.83 cnf(3416,plain, % 59.75/59.83 (E(f10(x34161,f3(f10(a2,a14))),f10(x34161,a14))), % 59.75/59.83 inference(scs_inference,[],[3294,3324,1810,40,59,57,69,55,68,17,12,62,9,70,25,22,15])). % 59.75/59.83 cnf(3420,plain, % 59.75/59.83 (~E(f18(f4(a1)),f4(a1))), % 59.75/59.83 inference(scs_inference,[],[3294,3324,1810,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60])). % 59.75/59.83 cnf(3426,plain, % 59.75/59.83 (~P8(f18(f4(a1)),a14)), % 59.75/59.83 inference(scs_inference,[],[3294,3324,1810,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77])). % 59.75/59.83 cnf(3444,plain, % 59.75/59.83 (E(f12(f13(a1,f4(a1)),f4(a1)),a1)), % 59.75/59.83 inference(scs_inference,[],[142,3285,3294,3324,3303,1810,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94])). % 59.75/59.83 cnf(3446,plain, % 59.75/59.83 (P1(f10(a2,f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[142,3285,3294,3324,3303,1292,1810,1289,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65])). % 59.75/59.83 cnf(3450,plain, % 59.75/59.83 (E(f3(f13(f13(a2,f8(a1,a14,a2)),f3(a2))),a14)), % 59.75/59.83 inference(scs_inference,[],[142,3285,3294,3324,3303,1292,1811,1810,1289,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52])). % 59.75/59.83 cnf(3452,plain, % 59.75/59.83 (P2(f3(f13(f13(a2,f8(a1,a14,a2)),f3(a2))),a1)), % 59.75/59.83 inference(scs_inference,[],[142,3285,3294,3324,3303,1292,1811,1809,1810,1289,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64])). % 59.75/59.83 cnf(3454,plain, % 59.75/59.83 (P3(f4(a1))), % 59.75/59.83 inference(scs_inference,[],[142,3285,3294,3324,3303,1292,1811,1809,1810,1289,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66])). % 59.75/59.83 cnf(3458,plain, % 59.75/59.83 (P8(f3(a2),f16(a15))), % 59.75/59.83 inference(scs_inference,[],[142,3285,3228,3283,3294,3324,3303,3297,1292,1811,147,1809,1810,1289,171,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36])). % 59.75/59.83 cnf(3459,plain, % 59.75/59.83 (~P6(f12(a1,a14),f13(a2,f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[142,3285,3228,3283,3294,3324,3303,3297,1609,1292,1811,147,1809,1810,1332,1289,171,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34])). % 59.75/59.83 cnf(3462,plain, % 59.75/59.83 (P1(f13(f13(a2,a14),a14))), % 59.75/59.83 inference(scs_inference,[],[142,3285,3228,3283,3294,3324,3265,3303,3297,612,3343,1609,1292,1811,147,1859,1809,1810,1332,1289,171,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28])). % 59.75/59.83 cnf(3463,plain, % 59.75/59.83 (E(f3(f10(a2,a14)),f3(a2))), % 59.75/59.83 inference(scs_inference,[],[142,3285,3228,3283,3294,3324,3265,3303,3297,612,3343,1609,1292,1811,147,1859,1809,1810,1332,1289,171,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3])). % 59.75/59.83 cnf(3465,plain, % 59.75/59.83 (E(f13(f13(a2,a14),a14),a2)), % 59.75/59.83 inference(scs_inference,[],[142,3301,3285,3228,3283,3294,3324,3265,3303,3297,612,3343,1816,1609,1292,1811,147,1859,1809,1810,634,1332,1289,171,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3,30,61])). % 59.75/59.83 cnf(3466,plain, % 59.75/59.83 (~P2(x34661,f13(f13(a2,a14),a14))), % 59.75/59.83 inference(rename_variables,[],[634])). % 59.75/59.83 cnf(3468,plain, % 59.75/59.83 (~P6(f12(f13(a1,f16(a15)),f16(a15)),f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[142,3301,3285,3228,3283,3294,3324,3265,3333,3281,3303,3297,612,3343,1816,1609,1292,1811,147,1859,1809,1810,634,1332,1289,171,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3,30,61,33])). % 59.75/59.83 cnf(3473,plain, % 59.75/59.83 (P4(f13(f13(f13(a2,f8(a1,a14,a2)),a14),f16(a15)))), % 59.75/59.83 inference(scs_inference,[],[142,3301,3285,3228,3283,3294,3324,3265,3333,3281,3303,3297,612,3343,1816,563,1609,1292,1811,147,149,1859,1809,1810,634,1332,1855,566,1289,171,564,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3,30,61,33,86,76,80])). % 59.75/59.83 cnf(3479,plain, % 59.75/59.83 (P5(f12(a1,f16(a15)))), % 59.75/59.83 inference(scs_inference,[],[142,3301,3285,3318,3228,3283,3294,3324,3265,3333,3281,3303,3297,612,3343,1816,563,1609,1292,1811,42,471,147,149,460,1859,1809,1810,634,1332,1855,566,1289,171,564,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3,30,61,33,86,76,80,97,92,81])). % 59.75/59.83 cnf(3483,plain, % 59.75/59.83 (P4(f12(f13(f13(a2,f8(a1,a14,a2)),a14),f16(a15)))), % 59.75/59.83 inference(scs_inference,[],[50,142,3301,3285,3318,3228,3283,3294,3324,3265,3333,3281,3303,3297,612,3343,1816,563,1609,1292,1811,42,471,147,149,460,1859,1809,1810,634,1332,1855,566,1289,171,564,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3,30,61,33,86,76,80,97,92,81,83,79])). % 59.75/59.83 cnf(3485,plain, % 59.75/59.83 (P5(f13(a1,f16(a15)))), % 59.75/59.83 inference(scs_inference,[],[50,142,3301,3285,3318,3228,3283,3294,3324,3265,3333,3281,3303,3297,612,3343,1816,563,1609,1292,1811,42,471,147,149,460,1859,1809,1810,634,1332,1855,566,1289,171,564,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3,30,61,33,86,76,80,97,92,81,83,79,82])). % 59.75/59.83 cnf(3490,plain, % 59.75/59.83 (P4(f10(a2,f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[50,142,3301,3285,3318,3228,3283,3294,3324,3265,3333,3281,3303,3297,612,3343,1816,563,1609,1292,1811,42,471,147,1296,149,460,1859,1809,1810,634,3466,1332,1855,566,1289,171,564,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3,30,61,33,86,76,80,97,92,81,83,79,82,90,73])). % 59.75/59.83 cnf(3492,plain, % 59.75/59.83 (P8(f16(a1),f4(a1))), % 59.75/59.83 inference(scs_inference,[],[50,142,3301,3285,3318,3228,3283,3294,3324,3265,3333,3281,3303,3297,612,3343,1816,563,1609,1292,1811,42,471,147,1296,149,460,1859,1809,1810,634,3466,1332,1855,566,1289,171,564,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3,30,61,33,86,76,80,97,92,81,83,79,82,90,73,134])). % 59.75/59.83 cnf(3502,plain, % 59.75/59.83 (P3(f8(a1,a14,f13(a2,a14)))), % 59.75/59.83 inference(scs_inference,[],[50,142,3301,972,3268,3285,3318,3228,3283,3294,3324,3265,3333,3281,3303,3297,612,3343,1816,563,1609,1292,1297,1811,42,471,147,1296,46,149,460,1859,1809,1810,634,3466,1332,1855,545,566,542,49,1289,171,45,564,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3,30,61,33,86,76,80,97,92,81,83,79,82,90,73,134,91,105,138,96,116])). % 59.75/59.83 cnf(3512,plain, % 59.75/59.83 (~E(f13(f13(a2,a14),a14),a1)), % 59.75/59.83 inference(scs_inference,[],[50,142,3301,972,3268,3285,3318,3228,3283,3294,3232,3324,3238,3265,3333,3281,3303,3297,612,3293,3343,1816,563,1609,1292,1297,1811,42,471,147,1296,46,149,460,43,1859,1809,1810,634,3466,1332,1855,545,566,542,49,1289,171,45,564,1287,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3,30,61,33,86,76,80,97,92,81,83,79,82,90,73,134,91,105,138,96,116,118,114,638,642,1606])). % 59.75/59.83 cnf(3530,plain, % 59.75/59.83 (~P2(x35301,f13(a2,f4(a1)))), % 59.75/59.83 inference(scs_inference,[],[50,142,3301,972,3268,3285,3318,3228,3283,3294,3232,3324,3238,3265,3333,3281,3303,3297,612,3293,3343,1816,563,1609,1292,1297,1811,42,471,147,1296,46,149,460,43,1859,1809,1810,634,3466,1332,1855,545,566,542,49,1289,171,45,564,1287,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3,30,61,33,86,76,80,97,92,81,83,79,82,90,73,134,91,105,138,96,116,118,114,638,642,1606,1903,1913,275,58,268,273,277,272,274,478,257])). % 59.75/59.83 cnf(3534,plain, % 59.75/59.83 (~P5(f10(a2,f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[50,142,3301,972,3268,3285,3318,3228,3283,3294,3232,3324,3238,3265,3333,3281,3303,3297,612,3293,3343,1816,563,1609,1292,1297,1811,42,471,147,1296,46,149,460,43,1859,1809,1810,634,3466,1332,1855,545,566,542,49,1289,171,45,564,1287,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3,30,61,33,86,76,80,97,92,81,83,79,82,90,73,134,91,105,138,96,116,118,114,638,642,1606,1903,1913,275,58,268,273,277,272,274,478,257,313,56])). % 59.75/59.83 cnf(3536,plain, % 59.75/59.83 (~P5(f13(f13(a2,a14),a14))), % 59.75/59.83 inference(scs_inference,[],[50,142,3301,972,3268,3285,3318,3228,3283,3294,3232,3324,3238,3265,3333,3281,3303,3297,612,3293,3343,1816,563,1609,1292,1297,1811,42,471,147,1296,46,149,460,43,1859,1809,1810,634,3466,1332,1855,545,566,542,49,1289,171,45,564,1287,40,59,57,69,55,68,17,12,62,9,70,25,22,15,5,27,18,60,26,21,20,19,77,13,10,23,7,8,14,6,16,11,24,4,2,128,71,94,65,127,52,64,66,31,29,36,34,37,32,28,3,30,61,33,86,76,80,97,92,81,83,79,82,90,73,134,91,105,138,96,116,118,114,638,642,1606,1903,1913,275,58,268,273,277,272,274,478,257,313,56,54])). % 59.75/59.83 cnf(3558,plain, % 59.75/59.83 (P6(f10(a2,f3(a2)),a1)), % 59.75/59.83 inference(scs_inference,[],[3446,505])). % 59.75/59.83 cnf(3560,plain, % 59.75/59.83 (E(f13(f13(a2,a14),a14),f13(a2,f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[3462,838])). % 59.75/59.83 cnf(3561,plain, % 59.75/59.83 (E(f13(a2,f3(a2)),f13(f13(a2,a14),a14))), % 59.75/59.83 inference(scs_inference,[],[3462,842])). % 59.75/59.83 cnf(3562,plain, % 59.75/59.83 (E(f13(a2,a14),f13(f13(a2,a14),a14))), % 59.75/59.83 inference(scs_inference,[],[3462,845])). % 59.75/59.83 cnf(3563,plain, % 59.75/59.83 (P6(f13(f13(a2,a14),a14),a2)), % 59.75/59.83 inference(scs_inference,[],[3462,964])). % 59.75/59.83 cnf(3564,plain, % 59.75/59.83 (P6(f13(f13(a2,a14),a14),f13(a2,a14))), % 59.75/59.83 inference(scs_inference,[],[3462,967])). % 59.75/59.83 cnf(3565,plain, % 59.75/59.83 (E(f13(f13(a2,a14),a14),f13(a2,a14))), % 59.75/59.83 inference(scs_inference,[],[3462,980])). % 59.75/59.83 cnf(3568,plain, % 59.75/59.83 (E(f13(f13(a2,a14),a14),f13(f13(a2,f8(a1,a14,a2)),f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[3462,1945])). % 59.75/59.83 cnf(3569,plain, % 59.75/59.83 (E(f13(f13(a2,f8(a1,a14,a2)),f3(a2)),f13(f13(a2,a14),a14))), % 59.75/59.83 inference(scs_inference,[],[3462,1949])). % 59.75/59.83 cnf(3590,plain, % 59.75/59.83 (P2(f18(f18(f4(a1))),a1)), % 59.75/59.83 inference(scs_inference,[],[3446,3502,3405,275,59,268,55,277,57,272,273,68])). % 59.75/59.83 cnf(3599,plain, % 59.75/59.83 (~P8(f18(f18(f4(a1))),a14)), % 59.75/59.83 inference(scs_inference,[],[3463,3446,3502,3405,275,59,268,55,277,57,272,273,68,69,70,17,62,77])). % 59.75/59.83 cnf(3608,plain, % 59.75/59.83 (E(f18(f3(f10(a2,a14))),f18(f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[3463,3446,3502,3405,275,59,268,55,277,57,272,273,68,69,70,17,62,77,274,5,25,9,26,12,18])). % 59.75/59.83 cnf(3631,plain, % 59.75/59.83 (P1(f13(f10(a2,f3(a2)),f4(a1)))), % 59.75/59.83 inference(scs_inference,[],[213,3454,3463,3446,3502,3405,275,59,268,55,277,57,272,273,68,69,70,17,62,77,274,5,25,9,26,12,18,60,257,22,10,23,6,20,21,13,11,27,15,24,16,19,8,7,14,4,2,128])). % 59.75/59.83 cnf(3633,plain, % 59.75/59.83 (E(f3(f13(f13(a2,a14),a14)),a14)), % 59.75/59.83 inference(scs_inference,[],[213,3454,3463,3446,3465,3462,3502,3405,275,59,268,55,277,57,272,273,68,69,70,17,62,77,274,5,25,9,26,12,18,60,257,22,10,23,6,20,21,13,11,27,15,24,16,19,8,7,14,4,2,128,52])). % 59.75/59.83 cnf(3635,plain, % 59.75/59.83 (P1(f12(f10(a2,f3(a2)),f4(a1)))), % 59.75/59.83 inference(scs_inference,[],[213,3454,3463,3446,3465,3462,3502,3405,275,59,268,55,277,57,272,273,68,69,70,17,62,77,274,5,25,9,26,12,18,60,257,22,10,23,6,20,21,13,11,27,15,24,16,19,8,7,14,4,2,128,52,127])). % 59.75/59.83 cnf(3639,plain, % 59.75/59.83 (E(f12(f13(a1,f16(a19)),f16(a19)),a1)), % 59.75/59.83 inference(scs_inference,[],[213,3454,3463,3446,3465,3490,3462,3502,3405,471,40,275,59,268,55,277,57,272,273,68,69,70,17,62,77,274,5,25,9,26,12,18,60,257,22,10,23,6,20,21,13,11,27,15,24,16,19,8,7,14,4,2,128,52,127,64,94])). % 59.75/59.83 cnf(3641,plain, % 59.75/59.83 (P3(f18(f4(a1)))), % 59.75/59.83 inference(scs_inference,[],[213,3454,3463,3446,3465,3490,3462,3502,3405,471,40,275,59,268,55,277,57,272,273,68,69,70,17,62,77,274,5,25,9,26,12,18,60,257,22,10,23,6,20,21,13,11,27,15,24,16,19,8,7,14,4,2,128,52,127,64,94,66])). % 59.75/59.83 cnf(3655,plain, % 59.75/59.83 (P4(f13(f10(a2,f3(a2)),f4(a1)))), % 59.75/59.83 inference(scs_inference,[],[166,213,3312,3454,3289,3463,3446,3465,3490,3534,3462,3351,3349,3502,3405,3426,3444,3483,3450,1311,177,3283,153,471,147,1296,543,1289,40,275,59,268,55,277,57,272,273,68,69,70,17,62,77,274,5,25,9,26,12,18,60,257,22,10,23,6,20,21,13,11,27,15,24,16,19,8,7,14,4,2,128,52,127,64,94,66,29,36,37,34,32,3,30,33,74,86,80])). % 59.75/59.83 cnf(3658,plain, % 59.75/59.83 (~P2(x36581,f13(f13(a2,a14),a14))), % 59.75/59.83 inference(rename_variables,[],[634])). % 59.75/59.83 cnf(3662,plain, % 59.75/59.83 (P4(f12(f10(a2,f3(a2)),f4(a1)))), % 59.75/59.83 inference(scs_inference,[],[166,213,3312,3454,3289,3463,3446,3465,3490,3534,3462,3351,3349,3502,3405,3426,3444,3483,3450,1311,177,3283,153,471,147,1296,634,543,1289,40,275,59,268,55,277,57,272,273,68,69,70,17,62,77,274,5,25,9,26,12,18,60,257,22,10,23,6,20,21,13,11,27,15,24,16,19,8,7,14,4,2,128,52,127,64,94,66,29,36,37,34,32,3,30,33,74,86,80,92,75,79])). % 59.75/59.83 cnf(3664,plain, % 59.75/59.83 (~P6(a1,f13(f10(a2,f3(a2)),f4(a1)))), % 59.75/59.83 inference(scs_inference,[],[166,213,3312,3454,3289,3463,3446,3465,3490,3534,3462,3351,3349,3502,3405,3426,3444,3483,3450,1311,177,3283,153,471,147,1296,634,543,1289,40,275,59,268,55,277,57,272,273,68,69,70,17,62,77,274,5,25,9,26,12,18,60,257,22,10,23,6,20,21,13,11,27,15,24,16,19,8,7,14,4,2,128,52,127,64,94,66,29,36,37,34,32,3,30,33,74,86,80,92,75,79,73])). % 59.75/59.83 cnf(3668,plain, % 59.75/59.83 (~P8(f18(f4(a1)),f4(a1))), % 59.75/59.83 inference(scs_inference,[],[166,3399,213,3312,3454,3289,3463,3420,3446,3465,3490,3534,3462,3351,3349,3502,3401,3405,3426,3444,3483,3450,1311,177,3283,153,471,147,3294,1296,149,634,543,1289,40,275,59,268,55,277,57,272,273,68,69,70,17,62,77,274,5,25,9,26,12,18,60,257,22,10,23,6,20,21,13,11,27,15,24,16,19,8,7,14,4,2,128,52,127,64,94,66,29,36,37,34,32,3,30,33,74,86,80,92,75,79,73,134,103])). % 59.75/59.83 cnf(3679,plain, % 59.75/59.83 (~P6(a1,f13(a2,f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[166,3399,213,3312,3454,3289,3463,3420,946,3446,3465,3490,3534,3462,3351,3349,3502,3401,3405,3426,3444,3483,3450,3452,1311,177,3283,153,471,147,3294,1296,149,634,591,41,543,1289,126,581,123,40,275,59,268,55,277,57,272,273,68,69,70,17,62,77,274,5,25,9,26,12,18,60,257,22,10,23,6,20,21,13,11,27,15,24,16,19,8,7,14,4,2,128,52,127,64,94,66,29,36,37,34,32,3,30,33,74,86,80,92,75,79,73,134,103,98,91,138,105,84])). % 59.75/59.83 cnf(3684,plain, % 59.75/59.83 (E(f13(f13(a2,a14),a14),f13(f13(f13(a2,a14),a14),f4(a1)))), % 59.75/59.83 inference(scs_inference,[],[166,3399,213,3312,3454,3289,3463,3420,946,3446,3465,3490,3534,3462,3530,3351,3349,3502,3401,3405,3426,3444,3483,3403,3450,3452,1311,177,3283,153,471,147,3294,1296,149,634,3658,591,41,543,542,1289,126,581,123,40,275,59,268,55,277,57,272,273,68,69,70,17,62,77,274,5,25,9,26,12,18,60,257,22,10,23,6,20,21,13,11,27,15,24,16,19,8,7,14,4,2,128,52,127,64,94,66,29,36,37,34,32,3,30,33,74,86,80,92,75,79,73,134,103,98,91,138,105,84,85,118])). % 59.75/59.83 cnf(3693,plain, % 59.75/59.83 (~P5(f13(f10(a2,f3(a2)),f4(a1)))), % 59.75/59.83 inference(scs_inference,[],[166,3399,213,3312,3458,3454,3289,3463,3420,946,3446,3465,3490,3534,3462,3530,3351,3349,3502,3401,3405,3426,3444,3483,3403,3450,3452,1311,3232,3238,177,3283,153,471,147,3294,1296,149,460,634,3658,591,41,172,543,542,1289,126,581,123,40,275,59,268,55,277,57,272,273,68,69,70,17,62,77,274,5,25,9,26,12,18,60,257,22,10,23,6,20,21,13,11,27,15,24,16,19,8,7,14,4,2,128,52,127,64,94,66,29,36,37,34,32,3,30,33,74,86,80,92,75,79,73,134,103,98,91,138,105,84,85,118,114,58,71,56])). % 59.75/59.83 cnf(3716,plain, % 59.75/59.83 (E(a2,f13(a2,f18(f4(a1))))), % 59.75/59.83 inference(scs_inference,[],[3641,3631,3238,275,55,59,57,268])). % 59.75/59.83 cnf(3724,plain, % 59.75/59.83 (P2(f18(f18(f16(a15))),a1)), % 59.75/59.83 inference(scs_inference,[],[3641,3631,3238,275,55,59,57,268,70,77,272,68])). % 59.75/59.83 cnf(3754,plain, % 59.75/59.83 (E(f3(f13(f13(a2,a14),a14)),f3(f13(a2,a14)))), % 59.75/59.83 inference(scs_inference,[],[3565,3641,3631,3279,3238,275,55,59,57,268,70,77,272,68,273,69,277,60,274,9,62,257,5,17,12,26,21,22,11,10,25,27,15,19,18,13])). % 59.75/59.83 cnf(3765,plain, % 59.75/59.83 (P1(f13(f13(f10(a2,f3(a2)),f4(a1)),f18(f4(a1))))), % 59.75/59.83 inference(scs_inference,[],[602,3565,3641,3631,3279,3238,275,55,59,57,268,70,77,272,68,273,69,277,60,274,9,62,257,5,17,12,26,21,22,11,10,25,27,15,19,18,13,6,23,20,14,16,24,8,7,4,2,128])). % 59.75/59.83 cnf(3767,plain, % 59.75/59.83 (P1(f12(f13(f10(a2,f3(a2)),f4(a1)),f18(f4(a1))))), % 59.75/59.83 inference(scs_inference,[],[602,3565,3641,3631,3279,3238,275,55,59,57,268,70,77,272,68,273,69,277,60,274,9,62,257,5,17,12,26,21,22,11,10,25,27,15,19,18,13,6,23,20,14,16,24,8,7,4,2,128,127])). % 59.75/59.83 cnf(3773,plain, % 59.75/59.83 (~P5(f12(f10(a2,f3(a2)),f4(a1)))), % 59.75/59.83 inference(scs_inference,[],[602,3565,3641,3655,3662,3631,3635,3279,3238,585,591,275,55,59,57,268,70,77,272,68,273,69,277,60,274,9,62,257,5,17,12,26,21,22,11,10,25,27,15,19,18,13,6,23,20,14,16,24,8,7,4,2,128,127,64,52,56])). % 59.75/59.83 cnf(3782,plain, % 59.75/59.83 (~P6(f12(a1,a14),f13(f13(a2,a14),a14))), % 59.75/59.83 inference(scs_inference,[],[602,3409,3565,3390,3459,3641,3560,3655,3662,1151,3631,3635,3279,3599,3608,3238,585,471,147,140,591,171,40,275,55,59,57,268,70,77,272,68,273,69,277,60,274,9,62,257,5,17,12,26,21,22,11,10,25,27,15,19,18,13,6,23,20,14,16,24,8,7,4,2,128,127,64,52,56,66,31,29,36,37,32,34])). % 59.75/59.83 cnf(3787,plain, % 59.75/59.83 (P8(f3(f13(f13(a2,a14),a14)),f3(a2))), % 59.75/59.83 inference(scs_inference,[],[602,650,3409,3565,3390,3459,3563,3479,3562,3536,3641,3560,3655,3662,1151,3631,3635,3279,3599,3608,3408,3238,585,471,147,140,591,41,171,123,40,275,55,59,57,268,70,77,272,68,273,69,277,60,274,9,62,257,5,17,12,26,21,22,11,10,25,27,15,19,18,13,6,23,20,14,16,24,8,7,4,2,128,127,64,52,56,66,31,29,36,37,32,34,30,3,33,86])). % 59.75/59.83 cnf(3789,plain, % 59.75/59.83 (P4(f13(f13(f10(a2,f3(a2)),f4(a1)),f18(f4(a1))))), % 59.75/59.83 inference(scs_inference,[],[602,650,3409,3565,3390,3459,3563,3479,3562,3536,3641,3560,3655,3662,1151,3631,3635,3279,3599,3608,3408,3238,585,471,147,140,591,41,171,123,40,275,55,59,57,268,70,77,272,68,273,69,277,60,274,9,62,257,5,17,12,26,21,22,11,10,25,27,15,19,18,13,6,23,20,14,16,24,8,7,4,2,128,127,64,52,56,66,31,29,36,37,32,34,30,3,33,86,80])). % 59.75/59.83 cnf(3795,plain, % 59.75/59.83 (P4(f12(f13(f10(a2,f3(a2)),f4(a1)),f18(f4(a1))))), % 59.75/59.83 inference(scs_inference,[],[602,650,3409,3565,3390,3459,3563,3479,3562,3536,3641,3560,3655,3662,1151,3631,3635,3664,3279,3590,3599,3608,3408,3238,585,471,147,140,43,591,41,171,123,40,275,55,59,57,268,70,77,272,68,273,69,277,60,274,9,62,257,5,17,12,26,21,22,11,10,25,27,15,19,18,13,6,23,20,14,16,24,8,7,4,2,128,127,64,52,56,66,31,29,36,37,32,34,30,3,33,86,80,97,92,79])). % 59.75/59.83 cnf(3797,plain, % 59.75/59.83 (~P2(f3(a1),f10(a2,f3(a2)))), % 59.75/59.83 inference(scs_inference,[],[602,650,3409,3565,3390,3459,3558,3563,3479,3562,3536,3641,3560,3655,3662,1151,3631,3635,3664,3279,3590,3599,3608,3408,3238,3283,585,471,147,140,43,591,41,171,123,40,275,55,59,57,268,70,77,272,68,273,69,277,60,274,9,62,257,5,17,12,26,21,22,11,10,25,27,15,19,18,13,6,23,20,14,16,24,8,7,4,2,128,127,64,52,56,66,31,29,36,37,32,34,30,3,33,86,80,97,92,79,90])). % 59.75/59.83 cnf(3799,plain, % 59.75/59.83 (~P6(a1,f12(f10(a2,f3(a2)),f4(a1)))), % 59.75/59.83 inference(scs_inference,[],[602,650,3409,3565,3390,3459,3558,3563,3479,3562,3536,3641,3560,3655,3662,1151,3631,3635,3664,3279,3590,3599,3608,3408,3238,3283,585,471,147,140,43,591,41,171,123,40,275,55,59,57,268,70,77,272,68,273,69,277,60,274,9,62,257,5,17,12,26,21,22,11,10,25,27,15,19,18,13,6,23,20,14,16,24,8,7,4,2,128,127,64,52,56,66,31,29,36,37,32,34,30,3,33,86,80,97,92,79,90,73])). % 59.75/59.83 cnf(3821,plain, % 59.75/59.83 (P2(f18(f16(a19)),a1)), % 59.75/59.83 inference(scs_inference,[],[3635,471,57,70,55,68])). % 59.75/59.83 cnf(3823,plain, % 59.75/59.83 (~P8(f18(f16(a19)),a14)), % 59.75/59.83 inference(scs_inference,[],[3635,471,57,70,55,68,77])). % 59.75/59.83 cnf(3825,plain, % 59.75/59.83 (P8(f16(a19),f18(f16(a19)))), % 59.75/59.83 inference(scs_inference,[],[3635,471,57,70,55,68,77,69])). % 59.75/59.83 cnf(3827,plain, % 59.75/59.83 (~E(f18(f16(a19)),a14)), % 59.75/59.83 inference(scs_inference,[],[3635,471,57,70,55,68,77,69,59])). % 59.75/59.83 cnf(3831,plain, % 59.75/59.83 (~E(f18(f16(a19)),f16(a19))), % 59.75/59.83 inference(scs_inference,[],[3724,3635,471,57,70,55,68,77,69,59,62,60])). % 59.75/59.83 cnf(3837,plain, % 59.75/59.83 (E(f12(f12(f13(a1,f16(a19)),f16(a19)),x38371),f12(a1,x38371))), % 59.75/59.83 inference(scs_inference,[],[3639,3724,3635,471,57,70,55,68,77,69,59,62,60,5,21,9,17,11])). % 59.75/59.83 cnf(3842,plain, % 59.75/59.83 (E(f3(f12(f13(a1,f16(a19)),f16(a19))),f3(a1))), % 59.75/59.83 inference(scs_inference,[],[3639,3724,3635,471,57,70,55,68,77,69,59,62,60,5,21,9,17,11,10,12,22,19,13])). % 59.75/59.83 cnf(3866,plain, % 59.75/59.83 (~P5(f13(f13(f10(a2,f3(a2)),f4(a1)),f18(f4(a1))))), % 59.75/59.83 inference(scs_inference,[],[659,3639,3724,3789,3765,3662,3635,471,1286,1289,40,57,70,55,68,77,69,59,62,60,5,21,9,17,11,10,12,22,19,13,23,26,6,25,27,16,18,15,20,14,7,4,24,8,2,71,64,52,66,56])). % 59.75/59.83 cnf(3883,plain, % 59.75/59.83 (~P2(x38831,f10(a2,a14))), % 59.75/59.83 inference(scs_inference,[],[195,659,3492,3564,3668,3679,3485,2072,3561,3693,3639,3568,3724,3716,3473,3789,3765,3468,2272,1868,3662,3635,1297,3283,471,1286,147,3405,3294,1859,591,566,1289,564,40,57,70,55,68,77,69,59,62,60,5,21,9,17,11,10,12,22,19,13,23,26,6,25,27,16,18,15,20,14,7,4,24,8,2,71,64,52,66,56,31,29,32,36,37,34,30,3,33,86,97,92,90])). % 59.75/59.83 cnf(3885,plain, % 59.75/59.83 (P4(f13(f13(a2,a14),a14))), % 59.75/59.83 inference(scs_inference,[],[195,659,3492,3564,3668,3679,3485,2072,3561,3693,3639,3568,3724,3716,3473,3789,3765,3468,2272,1868,3662,3635,1297,3283,471,1286,147,3405,3294,1859,591,566,1289,564,40,57,70,55,68,77,69,59,62,60,5,21,9,17,11,10,12,22,19,13,23,26,6,25,27,16,18,15,20,14,7,4,24,8,2,71,64,52,66,56,31,29,32,36,37,34,30,3,33,86,97,92,90,73])). % 59.75/59.83 cnf(3906,plain, % 59.75/59.83 (P8(f18(f16(a19)),f18(f18(f16(a19))))), % 59.75/59.83 inference(scs_inference,[],[3821,69])). % 59.75/59.83 cnf(3924,plain, % 59.75/59.83 (E(f12(f13(a2,f16(a15)),x39241),f12(a2,x39241))), % 59.75/59.83 inference(scs_inference,[],[3821,3353,3462,69,68,70,59,77,55,62,60,5,21,11])). % 59.75/59.83 cnf(3925,plain, % 59.75/59.83 (E(f13(f13(a2,f16(a15)),x39251),f13(a2,x39251))), % 59.75/59.83 inference(scs_inference,[],[3821,3353,3462,69,68,70,59,77,55,62,60,5,21,11,19])). % 59.75/59.83 cnf(3947,plain, % 59.75/59.83 (P1(f10(a2,a14))), % 59.75/59.83 inference(scs_inference,[],[995,3821,3353,1302,3462,1289,69,68,70,59,77,55,62,60,5,21,11,19,12,9,6,10,17,13,16,27,22,25,23,14,15,18,26,4,20,24,7,8,2,65])). % 59.75/59.83 cnf(3949,plain, % 59.75/59.83 (P2(f3(f13(f13(a2,a14),a14)),a1)), % 59.75/59.83 inference(scs_inference,[],[995,3885,3821,3353,1302,3462,1289,69,68,70,59,77,55,62,60,5,21,11,19,12,9,6,10,17,13,16,27,22,25,23,14,15,18,26,4,20,24,7,8,2,65,64])). % 59.75/59.83 cnf(3953,plain, % 59.75/59.83 (P3(f18(f16(a19)))), % 59.75/59.83 inference(scs_inference,[],[995,3885,3821,3795,3767,3353,1302,3462,1289,40,69,68,70,59,77,55,62,60,5,21,11,19,12,9,6,10,17,13,16,27,22,25,23,14,15,18,26,4,20,24,7,8,2,65,64,56,66])). % 59.75/59.83 cnf(3955,plain, % 59.75/59.83 (E(f3(f13(a2,a14)),a14)), % 59.75/59.83 inference(scs_inference,[],[995,3885,3821,3795,3767,3353,1302,3462,557,566,1289,40,69,68,70,59,77,55,62,60,5,21,11,19,12,9,6,10,17,13,16,27,22,25,23,14,15,18,26,4,20,24,7,8,2,65,64,56,66,52])). % 59.75/59.83 cnf(3960,plain, % 59.75/59.83 (P8(f3(f13(a2,a14)),f3(a2))), % 59.75/59.83 inference(scs_inference,[],[995,3883,3885,3821,3823,3787,3633,3754,3795,3767,3353,3416,1302,3462,557,566,1289,40,69,68,70,59,77,55,62,60,5,21,11,19,12,9,6,10,17,13,16,27,22,25,23,14,15,18,26,4,20,24,7,8,2,65,64,56,66,52,32,37,36])). % 59.75/59.83 cnf(3968,plain, % 59.75/59.83 (P6(f10(a2,a14),f10(a2,a14))), % 59.75/59.83 inference(scs_inference,[],[995,3883,3782,3885,3512,3821,3823,3773,3787,3569,3684,3633,3837,3754,3795,3767,3353,3416,2279,3301,1302,3462,557,566,1289,564,40,69,68,70,59,77,55,62,60,5,21,11,19,12,9,6,10,17,13,16,27,22,25,23,14,15,18,26,4,20,24,7,8,2,65,64,56,66,52,32,37,36,34,30,3,33,86,92])). % 59.75/59.83 cnf(3969,plain, % 59.75/59.83 (~P2(x39691,f10(a2,a14))), % 59.75/59.83 inference(rename_variables,[],[3883])). % 59.75/59.83 cnf(3975,plain, % 59.75/59.83 (~P8(f18(f16(a19)),f16(a19))), % 59.75/59.83 inference(scs_inference,[],[995,3883,3831,3782,3885,3825,3512,3821,3823,3773,3787,3569,3684,3633,3837,3754,3795,3767,3353,3416,2279,3301,1302,3399,3462,147,557,471,149,566,1289,564,40,69,68,70,59,77,55,62,60,5,21,11,19,12,9,6,10,17,13,16,27,22,25,23,14,15,18,26,4,20,24,7,8,2,65,64,56,66,52,32,37,36,34,30,3,33,86,92,73,134,103])). % 59.75/59.83 cnf(3977,plain, % 59.75/59.83 (~P8(f18(f16(a19)),f3(a2))), % 59.75/59.83 inference(scs_inference,[],[995,3883,3831,3782,3885,3825,3512,3821,3823,3773,3787,3569,3684,3633,3837,3754,3795,3767,3353,3416,2279,3301,178,1302,3399,3462,147,557,471,43,149,172,566,1289,564,40,69,68,70,59,77,55,62,60,5,21,11,19,12,9,6,10,17,13,16,27,22,25,23,14,15,18,26,4,20,24,7,8,2,65,64,56,66,52,32,37,36,34,30,3,33,86,92,73,134,103,114])). % 59.75/59.83 cnf(3979,plain, % 59.75/59.83 (~E(f10(a2,a14),f13(a1,a14))), % 59.75/59.83 inference(scs_inference,[],[995,3883,3969,3831,3782,3885,3827,3825,3512,3821,3823,3773,3787,3569,3684,3633,3837,3754,3795,3767,3353,3416,2279,3301,178,1302,3399,3462,147,557,471,43,149,172,566,542,1289,564,40,69,68,70,59,77,55,62,60,5,21,11,19,12,9,6,10,17,13,16,27,22,25,23,14,15,18,26,4,20,24,7,8,2,65,64,56,66,52,32,37,36,34,30,3,33,86,92,73,134,103,114,102])). % 59.75/59.83 cnf(3980,plain, % 59.75/59.83 (~P2(x39801,f10(a2,a14))), % 59.75/59.83 inference(rename_variables,[],[3883])). % 59.75/59.83 cnf(4001,plain, % 59.75/59.83 (E(f10(a2,a14),a2)), % 59.75/59.83 inference(scs_inference,[],[995,3883,3969,3980,3831,3782,3885,3827,3825,3512,3821,3823,3773,3787,3569,3684,3633,3837,3754,3795,3767,3353,3416,2279,3301,178,1302,3399,3462,147,557,3294,471,43,149,172,566,542,1289,564,40,69,68,70,59,77,55,62,60,5,21,11,19,12,9,6,10,17,13,16,27,22,25,23,14,15,18,26,4,20,24,7,8,2,65,64,56,66,52,32,37,36,34,30,3,33,86,92,73,134,103,114,102,248,475,494,275,268,272,273,274,277,257,71,61])). % 59.75/59.83 cnf(4002,plain, % 59.75/59.83 (~P2(x40021,f10(a2,a14))), % 59.75/59.83 inference(rename_variables,[],[3883])). % 59.75/59.83 cnf(4005,plain, % 59.75/59.83 (~P2(x40051,f10(a2,a14))), % 59.75/59.83 inference(rename_variables,[],[3883])). % 59.75/59.83 cnf(4008,plain, % 59.75/59.83 (~P2(x40081,f10(a2,a14))), % 59.75/59.83 inference(rename_variables,[],[3883])). % 59.75/59.83 cnf(4010,plain, % 59.75/59.83 (P3(f7(a1,a14,f10(a2,a14)))), % 59.75/59.83 inference(scs_inference,[],[995,3883,3969,3980,4002,4005,4008,3831,3782,3885,3827,3825,3512,3821,3823,3773,3787,3569,3684,3633,3837,3754,3795,3767,3353,3416,2279,3301,178,3420,1302,3399,3462,3502,3454,147,557,3294,471,43,149,172,566,542,1289,564,40,69,68,70,59,77,55,62,60,5,21,11,19,12,9,6,10,17,13,16,27,22,25,23,14,15,18,26,4,20,24,7,8,2,65,64,56,66,52,32,37,36,34,30,3,33,86,92,73,134,103,114,102,248,475,494,275,268,272,273,274,277,257,71,61,137,96,117])). % 59.75/59.83 cnf(4114,plain, % 59.75/59.83 ($false), % 59.75/59.83 inference(scs_inference,[],[562,3947,3968,3979,4001,3960,3975,3977,3797,3953,4010,3955,3799,3924,3925,3949,1129,3299,3906,3866,3842,878,3312,3789,3765,3883,3662,3318,3635,179,3454,147,46,43,592,591,172,566,49,171,45,564,40,275,494,268,69,272,68,273,277,59,70,274,55,77,62,257,60,5,12,11,9,21,16,22,27,19,13,6,25,17,18,10,23,14,24,15,8,7,4,26,20,2,63,128,71,64,35,127,38,31,29,37,32,36,34,3,30,33,80,93,86,92,79,73,134]), % 59.75/59.83 ['proof']). % 59.75/59.83 % SZS output end Proof % 59.75/59.83 % Total time :59.140000s %------------------------------------------------------------------------------