%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM615+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 12:25:25 EDT 2024 % Result : Theorem 59.58s 59.59s % Output : CNFRefutation 59.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM615+1 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n019.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sat Jun 22 22:00:38 EDT 2024 % 0.12/0.33 % CPUTime : % 0.52/0.61 start to proof:theBenchmark % 59.55/59.56 %------------------------------------------- % 59.55/59.56 % File :CSE---1.7 % 59.55/59.56 % Problem :theBenchmark % 59.55/59.56 % Transform :cnf % 59.55/59.56 % Format :tptp:raw % 59.55/59.56 % Command :java -jar mcs_scs.jar %d %s % 59.55/59.56 % 59.55/59.56 % Result :Theorem 58.860000s % 59.55/59.56 % Output :CNFRefutation 58.860000s % 59.55/59.56 %------------------------------------------- % 59.55/59.57 %------------------------------------------------------------------------------ % 59.55/59.57 % File : NUM615+1 : TPTP v8.2.0. Released v4.0.0. % 59.55/59.57 % Domain : Number Theory % 59.55/59.57 % Problem : Ramsey's Infinite Theorem 15_02_23_09, 00 expansion % 59.55/59.57 % Version : Especial. % 59.55/59.57 % English : % 59.55/59.57 % 59.55/59.57 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 59.55/59.57 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 59.55/59.57 % Source : [Pas08] % 59.55/59.57 % Names : ramsey_15_02_23_09.00 [Pas08] % 59.55/59.57 % 59.55/59.57 % Status : Theorem % 59.55/59.57 % Rating : 0.25 v8.2.0, 0.28 v8.1.0, 0.25 v7.4.0, 0.20 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.22 v7.0.0, 0.23 v6.4.0, 0.27 v6.3.0, 0.21 v6.2.0, 0.16 v6.1.0, 0.27 v6.0.0, 0.26 v5.5.0, 0.41 v5.4.0, 0.46 v5.3.0, 0.52 v5.2.0, 0.35 v5.1.0, 0.48 v5.0.0, 0.58 v4.1.0, 0.65 v4.0.1, 0.83 v4.0.0 % 59.55/59.57 % Syntax : Number of formulae : 111 ( 18 unt; 11 def) % 59.55/59.57 % Number of atoms : 402 ( 73 equ) % 59.55/59.57 % Maximal formula atoms : 12 ( 3 avg) % 59.55/59.57 % Number of connectives : 316 ( 25 ~; 4 |; 130 &) % 59.55/59.57 % ( 22 <=>; 135 =>; 0 <=; 0 <~>) % 59.55/59.57 % Maximal formula depth : 15 ( 5 avg) % 59.55/59.57 % Maximal term depth : 5 ( 1 avg) % 59.55/59.57 % Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty) % 59.55/59.57 % Number of functors : 30 ( 30 usr; 16 con; 0-2 aty) % 59.55/59.57 % Number of variables : 172 ( 159 !; 13 ?) % 59.55/59.57 % SPC : FOF_THM_RFO_SEQ % 59.55/59.57 % 59.55/59.57 % Comments : Problem generated by the SAD system [VLP07] % 59.55/59.57 %------------------------------------------------------------------------------ % 59.55/59.57 fof(mSetSort,axiom, % 59.55/59.57 ! [W0] : % 59.55/59.57 ( aSet0(W0) % 59.55/59.57 => $true ) ). % 59.55/59.57 % 59.55/59.57 fof(mElmSort,axiom, % 59.55/59.57 ! [W0] : % 59.55/59.57 ( aElement0(W0) % 59.55/59.57 => $true ) ). % 59.55/59.57 % 59.55/59.57 fof(mEOfElem,axiom, % 59.55/59.57 ! [W0] : % 59.55/59.57 ( aSet0(W0) % 59.55/59.57 => ! [W1] : % 59.55/59.57 ( aElementOf0(W1,W0) % 59.55/59.57 => aElement0(W1) ) ) ). % 59.55/59.57 % 59.55/59.57 fof(mFinRel,axiom, % 59.55/59.57 ! [W0] : % 59.55/59.57 ( aSet0(W0) % 59.55/59.57 => ( isFinite0(W0) % 59.55/59.57 => $true ) ) ). % 59.55/59.57 % 59.55/59.57 fof(mDefEmp,definition, % 59.55/59.57 ! [W0] : % 59.55/59.57 ( W0 = slcrc0 % 59.55/59.57 <=> ( aSet0(W0) % 59.55/59.57 & ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 59.55/59.57 % 59.55/59.57 fof(mEmpFin,axiom, % 59.55/59.57 isFinite0(slcrc0) ). % 59.55/59.57 % 59.55/59.57 fof(mCntRel,axiom, % 59.55/59.57 ! [W0] : % 59.55/59.57 ( aSet0(W0) % 59.55/59.57 => ( isCountable0(W0) % 59.55/59.57 => $true ) ) ). % 59.55/59.57 % 59.55/59.57 fof(mCountNFin,axiom, % 59.55/59.57 ! [W0] : % 59.55/59.57 ( ( aSet0(W0) % 59.55/59.57 & isCountable0(W0) ) % 59.55/59.57 => ~ isFinite0(W0) ) ). % 59.55/59.57 % 59.55/59.57 fof(mCountNFin_01,axiom, % 59.55/59.57 ! [W0] : % 59.55/59.57 ( ( aSet0(W0) % 59.55/59.57 & isCountable0(W0) ) % 59.55/59.57 => W0 != slcrc0 ) ). % 59.55/59.57 % 59.55/59.57 fof(mDefSub,definition, % 59.55/59.57 ! [W0] : % 59.55/59.57 ( aSet0(W0) % 59.55/59.57 => ! [W1] : % 59.55/59.57 ( aSubsetOf0(W1,W0) % 59.55/59.57 <=> ( aSet0(W1) % 59.55/59.57 & ! [W2] : % 59.55/59.57 ( aElementOf0(W2,W1) % 59.55/59.57 => aElementOf0(W2,W0) ) ) ) ) ). % 59.55/59.57 % 59.55/59.57 fof(mSubFSet,axiom, % 59.55/59.57 ! [W0] : % 59.55/59.57 ( ( aSet0(W0) % 59.55/59.57 & isFinite0(W0) ) % 59.55/59.57 => ! [W1] : % 59.55/59.57 ( aSubsetOf0(W1,W0) % 59.55/59.57 => isFinite0(W1) ) ) ). % 59.55/59.57 % 59.55/59.57 fof(mSubRefl,axiom, % 59.55/59.57 ! [W0] : % 59.55/59.57 ( aSet0(W0) % 59.55/59.57 => aSubsetOf0(W0,W0) ) ). % 59.55/59.57 % 59.55/59.57 fof(mSubASymm,axiom, % 59.55/59.57 ! [W0,W1] : % 59.55/59.57 ( ( aSet0(W0) % 59.55/59.57 & aSet0(W1) ) % 59.55/59.57 => ( ( aSubsetOf0(W0,W1) % 59.55/59.57 & aSubsetOf0(W1,W0) ) % 59.55/59.57 => W0 = W1 ) ) ). % 59.55/59.57 % 59.55/59.57 fof(mSubTrans,axiom, % 59.55/59.57 ! [W0,W1,W2] : % 59.55/59.57 ( ( aSet0(W0) % 59.55/59.57 & aSet0(W1) % 59.55/59.57 & aSet0(W2) ) % 59.55/59.57 => ( ( aSubsetOf0(W0,W1) % 59.55/59.57 & aSubsetOf0(W1,W2) ) % 59.55/59.57 => aSubsetOf0(W0,W2) ) ) ). % 59.55/59.57 % 59.55/59.57 fof(mDefCons,definition, % 59.55/59.57 ! [W0,W1] : % 59.55/59.57 ( ( aSet0(W0) % 59.55/59.57 & aElement0(W1) ) % 59.55/59.57 => ! [W2] : % 59.55/59.57 ( W2 = sdtpldt0(W0,W1) % 59.55/59.57 <=> ( aSet0(W2) % 59.55/59.57 & ! [W3] : % 59.55/59.57 ( aElementOf0(W3,W2) % 59.55/59.57 <=> ( aElement0(W3) % 59.55/59.57 & ( aElementOf0(W3,W0) % 59.55/59.57 | W3 = W1 ) ) ) ) ) ) ). % 59.55/59.58 % 59.55/59.58 fof(mDefDiff,definition, % 59.55/59.58 ! [W0,W1] : % 59.55/59.58 ( ( aSet0(W0) % 59.55/59.58 & aElement0(W1) ) % 59.55/59.58 => ! [W2] : % 59.55/59.58 ( W2 = sdtmndt0(W0,W1) % 59.55/59.58 <=> ( aSet0(W2) % 59.55/59.58 & ! [W3] : % 59.55/59.58 ( aElementOf0(W3,W2) % 59.55/59.58 <=> ( aElement0(W3) % 59.55/59.58 & aElementOf0(W3,W0) % 59.55/59.58 & W3 != W1 ) ) ) ) ) ). % 59.55/59.58 % 59.55/59.58 fof(mConsDiff,axiom, % 59.55/59.58 ! [W0] : % 59.55/59.58 ( aSet0(W0) % 59.55/59.58 => ! [W1] : % 59.55/59.58 ( aElementOf0(W1,W0) % 59.55/59.58 => sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ) ). % 59.55/59.58 % 59.55/59.58 fof(mDiffCons,axiom, % 59.55/59.58 ! [W0,W1] : % 59.55/59.58 ( ( aElement0(W0) % 59.55/59.58 & aSet0(W1) ) % 59.55/59.58 => ( ~ aElementOf0(W0,W1) % 59.55/59.58 => sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ) ). % 59.55/59.58 % 59.55/59.58 fof(mCConsSet,axiom, % 59.55/59.58 ! [W0] : % 59.55/59.58 ( aElement0(W0) % 59.55/59.58 => ! [W1] : % 59.55/59.58 ( ( aSet0(W1) % 59.55/59.58 & isCountable0(W1) ) % 59.55/59.58 => isCountable0(sdtpldt0(W1,W0)) ) ) ). % 59.55/59.58 % 59.55/59.58 fof(mCDiffSet,axiom, % 59.55/59.58 ! [W0] : % 59.55/59.58 ( aElement0(W0) % 59.55/59.58 => ! [W1] : % 59.55/59.58 ( ( aSet0(W1) % 59.55/59.58 & isCountable0(W1) ) % 59.55/59.58 => isCountable0(sdtmndt0(W1,W0)) ) ) ). % 59.55/59.58 % 59.55/59.58 fof(mFConsSet,axiom, % 59.55/59.58 ! [W0] : % 59.55/59.58 ( aElement0(W0) % 59.55/59.58 => ! [W1] : % 59.55/59.58 ( ( aSet0(W1) % 59.55/59.58 & isFinite0(W1) ) % 59.55/59.58 => isFinite0(sdtpldt0(W1,W0)) ) ) ). % 59.55/59.58 % 59.55/59.58 fof(mFDiffSet,axiom, % 59.55/59.58 ! [W0] : % 59.55/59.58 ( aElement0(W0) % 59.55/59.58 => ! [W1] : % 59.55/59.58 ( ( aSet0(W1) % 59.55/59.58 & isFinite0(W1) ) % 59.55/59.58 => isFinite0(sdtmndt0(W1,W0)) ) ) ). % 59.55/59.58 % 59.55/59.58 fof(mNATSet,axiom, % 59.55/59.58 ( aSet0(szNzAzT0) % 59.55/59.58 & isCountable0(szNzAzT0) ) ). % 59.55/59.58 % 59.55/59.58 fof(mZeroNum,axiom, % 59.55/59.58 aElementOf0(sz00,szNzAzT0) ). % 59.55/59.58 % 59.55/59.58 fof(mSuccNum,axiom, % 59.55/59.58 ! [W0] : % 59.55/59.58 ( aElementOf0(W0,szNzAzT0) % 59.55/59.58 => ( aElementOf0(szszuzczcdt0(W0),szNzAzT0) % 59.55/59.58 & szszuzczcdt0(W0) != sz00 ) ) ). % 59.55/59.58 % 59.55/59.58 fof(mSuccEquSucc,axiom, % 59.55/59.58 ! [W0,W1] : % 59.55/59.58 ( ( aElementOf0(W0,szNzAzT0) % 59.55/59.58 & aElementOf0(W1,szNzAzT0) ) % 59.55/59.58 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 59.55/59.58 => W0 = W1 ) ) ). % 59.55/59.58 % 59.55/59.58 fof(mNatExtra,axiom, % 59.55/59.58 ! [W0] : % 59.55/59.58 ( aElementOf0(W0,szNzAzT0) % 59.55/59.58 => ( W0 = sz00 % 59.55/59.58 | ? [W1] : % 59.55/59.58 ( aElementOf0(W1,szNzAzT0) % 59.55/59.58 & W0 = szszuzczcdt0(W1) ) ) ) ). % 59.55/59.58 % 59.55/59.58 fof(mNatNSucc,axiom, % 59.55/59.58 ! [W0] : % 59.55/59.58 ( aElementOf0(W0,szNzAzT0) % 59.55/59.58 => W0 != szszuzczcdt0(W0) ) ). % 59.55/59.58 % 59.55/59.58 fof(mLessRel,axiom, % 59.55/59.58 ! [W0,W1] : % 59.55/59.58 ( ( aElementOf0(W0,szNzAzT0) % 59.55/59.58 & aElementOf0(W1,szNzAzT0) ) % 59.55/59.58 => ( sdtlseqdt0(W0,W1) % 59.55/59.58 => $true ) ) ). % 59.55/59.58 % 59.55/59.58 fof(mZeroLess,axiom, % 59.55/59.58 ! [W0] : % 59.55/59.58 ( aElementOf0(W0,szNzAzT0) % 59.55/59.58 => sdtlseqdt0(sz00,W0) ) ). % 59.55/59.58 % 59.55/59.58 fof(mNoScLessZr,axiom, % 59.55/59.58 ! [W0] : % 59.55/59.58 ( aElementOf0(W0,szNzAzT0) % 59.55/59.58 => ~ sdtlseqdt0(szszuzczcdt0(W0),sz00) ) ). % 59.55/59.58 % 59.55/59.58 fof(mSuccLess,axiom, % 59.55/59.58 ! [W0,W1] : % 59.55/59.58 ( ( aElementOf0(W0,szNzAzT0) % 59.55/59.58 & aElementOf0(W1,szNzAzT0) ) % 59.55/59.58 => ( sdtlseqdt0(W0,W1) % 59.55/59.58 <=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ) ). % 59.55/59.58 % 59.55/59.58 fof(mLessSucc,axiom, % 59.55/59.58 ! [W0] : % 59.55/59.58 ( aElementOf0(W0,szNzAzT0) % 59.55/59.58 => sdtlseqdt0(W0,szszuzczcdt0(W0)) ) ). % 59.55/59.58 % 59.55/59.58 fof(mLessRefl,axiom, % 59.55/59.58 ! [W0] : % 59.55/59.58 ( aElementOf0(W0,szNzAzT0) % 59.55/59.58 => sdtlseqdt0(W0,W0) ) ). % 59.55/59.58 % 59.58/59.58 fof(mLessASymm,axiom, % 59.58/59.58 ! [W0,W1] : % 59.58/59.58 ( ( aElementOf0(W0,szNzAzT0) % 59.58/59.58 & aElementOf0(W1,szNzAzT0) ) % 59.58/59.58 => ( ( sdtlseqdt0(W0,W1) % 59.58/59.58 & sdtlseqdt0(W1,W0) ) % 59.58/59.58 => W0 = W1 ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mLessTrans,axiom, % 59.58/59.58 ! [W0,W1,W2] : % 59.58/59.58 ( ( aElementOf0(W0,szNzAzT0) % 59.58/59.58 & aElementOf0(W1,szNzAzT0) % 59.58/59.58 & aElementOf0(W2,szNzAzT0) ) % 59.58/59.58 => ( ( sdtlseqdt0(W0,W1) % 59.58/59.58 & sdtlseqdt0(W1,W2) ) % 59.58/59.58 => sdtlseqdt0(W0,W2) ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mLessTotal,axiom, % 59.58/59.58 ! [W0,W1] : % 59.58/59.58 ( ( aElementOf0(W0,szNzAzT0) % 59.58/59.58 & aElementOf0(W1,szNzAzT0) ) % 59.58/59.58 => ( sdtlseqdt0(W0,W1) % 59.58/59.58 | sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mIHSort,axiom, % 59.58/59.58 ! [W0,W1] : % 59.58/59.58 ( ( aElementOf0(W0,szNzAzT0) % 59.58/59.58 & aElementOf0(W1,szNzAzT0) ) % 59.58/59.58 => ( iLess0(W0,W1) % 59.58/59.58 => $true ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mIH,axiom, % 59.58/59.58 ! [W0] : % 59.58/59.58 ( aElementOf0(W0,szNzAzT0) % 59.58/59.58 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 59.58/59.58 % 59.58/59.58 fof(mCardS,axiom, % 59.58/59.58 ! [W0] : % 59.58/59.58 ( aSet0(W0) % 59.58/59.58 => aElement0(sbrdtbr0(W0)) ) ). % 59.58/59.58 % 59.58/59.58 fof(mCardNum,axiom, % 59.58/59.58 ! [W0] : % 59.58/59.58 ( aSet0(W0) % 59.58/59.58 => ( aElementOf0(sbrdtbr0(W0),szNzAzT0) % 59.58/59.58 <=> isFinite0(W0) ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mCardEmpty,axiom, % 59.58/59.58 ! [W0] : % 59.58/59.58 ( aSet0(W0) % 59.58/59.58 => ( sbrdtbr0(W0) = sz00 % 59.58/59.58 <=> W0 = slcrc0 ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mCardCons,axiom, % 59.58/59.58 ! [W0] : % 59.58/59.58 ( ( aSet0(W0) % 59.58/59.58 & isFinite0(W0) ) % 59.58/59.58 => ! [W1] : % 59.58/59.58 ( aElement0(W1) % 59.58/59.58 => ( ~ aElementOf0(W1,W0) % 59.58/59.58 => sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mCardDiff,axiom, % 59.58/59.58 ! [W0] : % 59.58/59.58 ( aSet0(W0) % 59.58/59.58 => ! [W1] : % 59.58/59.58 ( ( isFinite0(W0) % 59.58/59.58 & aElementOf0(W1,W0) ) % 59.58/59.58 => szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mCardSub,axiom, % 59.58/59.58 ! [W0] : % 59.58/59.58 ( aSet0(W0) % 59.58/59.58 => ! [W1] : % 59.58/59.58 ( ( isFinite0(W0) % 59.58/59.58 & aSubsetOf0(W1,W0) ) % 59.58/59.58 => sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mCardSubEx,axiom, % 59.58/59.58 ! [W0,W1] : % 59.58/59.58 ( ( aSet0(W0) % 59.58/59.58 & aElementOf0(W1,szNzAzT0) ) % 59.58/59.58 => ( ( isFinite0(W0) % 59.58/59.58 & sdtlseqdt0(W1,sbrdtbr0(W0)) ) % 59.58/59.58 => ? [W2] : % 59.58/59.58 ( aSubsetOf0(W2,W0) % 59.58/59.58 & sbrdtbr0(W2) = W1 ) ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mDefMin,definition, % 59.58/59.58 ! [W0] : % 59.58/59.58 ( ( aSubsetOf0(W0,szNzAzT0) % 59.58/59.58 & W0 != slcrc0 ) % 59.58/59.58 => ! [W1] : % 59.58/59.58 ( W1 = szmzizndt0(W0) % 59.58/59.58 <=> ( aElementOf0(W1,W0) % 59.58/59.58 & ! [W2] : % 59.58/59.58 ( aElementOf0(W2,W0) % 59.58/59.58 => sdtlseqdt0(W1,W2) ) ) ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mDefMax,definition, % 59.58/59.58 ! [W0] : % 59.58/59.58 ( ( aSubsetOf0(W0,szNzAzT0) % 59.58/59.58 & isFinite0(W0) % 59.58/59.58 & W0 != slcrc0 ) % 59.58/59.58 => ! [W1] : % 59.58/59.58 ( W1 = szmzazxdt0(W0) % 59.58/59.58 <=> ( aElementOf0(W1,W0) % 59.58/59.58 & ! [W2] : % 59.58/59.58 ( aElementOf0(W2,W0) % 59.58/59.58 => sdtlseqdt0(W2,W1) ) ) ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mMinMin,axiom, % 59.58/59.58 ! [W0,W1] : % 59.58/59.58 ( ( aSubsetOf0(W0,szNzAzT0) % 59.58/59.58 & aSubsetOf0(W1,szNzAzT0) % 59.58/59.58 & W0 != slcrc0 % 59.58/59.58 & W1 != slcrc0 ) % 59.58/59.58 => ( ( aElementOf0(szmzizndt0(W0),W1) % 59.58/59.58 & aElementOf0(szmzizndt0(W1),W0) ) % 59.58/59.58 => szmzizndt0(W0) = szmzizndt0(W1) ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mDefSeg,definition, % 59.58/59.58 ! [W0] : % 59.58/59.58 ( aElementOf0(W0,szNzAzT0) % 59.58/59.58 => ! [W1] : % 59.58/59.58 ( W1 = slbdtrb0(W0) % 59.58/59.58 <=> ( aSet0(W1) % 59.58/59.58 & ! [W2] : % 59.58/59.58 ( aElementOf0(W2,W1) % 59.58/59.58 <=> ( aElementOf0(W2,szNzAzT0) % 59.58/59.58 & sdtlseqdt0(szszuzczcdt0(W2),W0) ) ) ) ) ) ). % 59.58/59.58 % 59.58/59.58 fof(mSegFin,axiom, % 59.58/59.58 ! [W0] : % 59.58/59.58 ( aElementOf0(W0,szNzAzT0) % 59.58/59.58 => isFinite0(slbdtrb0(W0)) ) ). % 59.58/59.58 % 59.58/59.58 fof(mSegZero,axiom, % 59.58/59.58 slbdtrb0(sz00) = slcrc0 ). % 59.58/59.58 % 59.58/59.58 fof(mSegSucc,axiom, % 59.58/59.58 ! [W0,W1] : % 59.58/59.58 ( ( aElementOf0(W0,szNzAzT0) % 59.58/59.58 & aElementOf0(W1,szNzAzT0) ) % 59.58/59.59 => ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1))) % 59.58/59.59 <=> ( aElementOf0(W0,slbdtrb0(W1)) % 59.58/59.59 | W0 = W1 ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mSegLess,axiom, % 59.58/59.59 ! [W0,W1] : % 59.58/59.59 ( ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 & aElementOf0(W1,szNzAzT0) ) % 59.58/59.59 => ( sdtlseqdt0(W0,W1) % 59.58/59.59 <=> aSubsetOf0(slbdtrb0(W0),slbdtrb0(W1)) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mFinSubSeg,axiom, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( ( aSubsetOf0(W0,szNzAzT0) % 59.58/59.59 & isFinite0(W0) ) % 59.58/59.59 => ? [W1] : % 59.58/59.59 ( aElementOf0(W1,szNzAzT0) % 59.58/59.59 & aSubsetOf0(W0,slbdtrb0(W1)) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mCardSeg,axiom, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 => sbrdtbr0(slbdtrb0(W0)) = W0 ) ). % 59.58/59.59 % 59.58/59.59 fof(mDefSel,definition, % 59.58/59.59 ! [W0,W1] : % 59.58/59.59 ( ( aSet0(W0) % 59.58/59.59 & aElementOf0(W1,szNzAzT0) ) % 59.58/59.59 => ! [W2] : % 59.58/59.59 ( W2 = slbdtsldtrb0(W0,W1) % 59.58/59.59 <=> ( aSet0(W2) % 59.58/59.59 & ! [W3] : % 59.58/59.59 ( aElementOf0(W3,W2) % 59.58/59.59 <=> ( aSubsetOf0(W3,W0) % 59.58/59.59 & sbrdtbr0(W3) = W1 ) ) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mSelFSet,axiom, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( ( aSet0(W0) % 59.58/59.59 & isFinite0(W0) ) % 59.58/59.59 => ! [W1] : % 59.58/59.59 ( aElementOf0(W1,szNzAzT0) % 59.58/59.59 => isFinite0(slbdtsldtrb0(W0,W1)) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mSelNSet,axiom, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( ( aSet0(W0) % 59.58/59.59 & ~ isFinite0(W0) ) % 59.58/59.59 => ! [W1] : % 59.58/59.59 ( aElementOf0(W1,szNzAzT0) % 59.58/59.59 => slbdtsldtrb0(W0,W1) != slcrc0 ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mSelCSet,axiom, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( ( aSet0(W0) % 59.58/59.59 & isCountable0(W0) ) % 59.58/59.59 => ! [W1] : % 59.58/59.59 ( ( aElementOf0(W1,szNzAzT0) % 59.58/59.59 & W1 != sz00 ) % 59.58/59.59 => isCountable0(slbdtsldtrb0(W0,W1)) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mSelSub,axiom, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 => ! [W1,W2] : % 59.58/59.59 ( ( aSet0(W1) % 59.58/59.59 & aSet0(W2) % 59.58/59.59 & W0 != sz00 ) % 59.58/59.59 => ( ( aSubsetOf0(slbdtsldtrb0(W1,W0),slbdtsldtrb0(W2,W0)) % 59.58/59.59 & slbdtsldtrb0(W1,W0) != slcrc0 ) % 59.58/59.59 => aSubsetOf0(W1,W2) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mSelExtra,axiom, % 59.58/59.59 ! [W0,W1] : % 59.58/59.59 ( ( aSet0(W0) % 59.58/59.59 & aElementOf0(W1,szNzAzT0) ) % 59.58/59.59 => ! [W2] : % 59.58/59.59 ( ( aSubsetOf0(W2,slbdtsldtrb0(W0,W1)) % 59.58/59.59 & isFinite0(W2) ) % 59.58/59.59 => ? [W3] : % 59.58/59.59 ( aSubsetOf0(W3,W0) % 59.58/59.59 & isFinite0(W3) % 59.58/59.59 & aSubsetOf0(W2,slbdtsldtrb0(W3,W1)) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mFunSort,axiom, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aFunction0(W0) % 59.58/59.59 => $true ) ). % 59.58/59.59 % 59.58/59.59 fof(mDomSet,axiom, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aFunction0(W0) % 59.58/59.59 => aSet0(szDzozmdt0(W0)) ) ). % 59.58/59.59 % 59.58/59.59 fof(mImgElm,axiom, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aFunction0(W0) % 59.58/59.59 => ! [W1] : % 59.58/59.59 ( aElementOf0(W1,szDzozmdt0(W0)) % 59.58/59.59 => aElement0(sdtlpdtrp0(W0,W1)) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mDefPtt,definition, % 59.58/59.59 ! [W0,W1] : % 59.58/59.59 ( ( aFunction0(W0) % 59.58/59.59 & aElement0(W1) ) % 59.58/59.59 => ! [W2] : % 59.58/59.59 ( W2 = sdtlbdtrb0(W0,W1) % 59.58/59.59 <=> ( aSet0(W2) % 59.58/59.59 & ! [W3] : % 59.58/59.59 ( aElementOf0(W3,W2) % 59.58/59.59 <=> ( aElementOf0(W3,szDzozmdt0(W0)) % 59.58/59.59 & sdtlpdtrp0(W0,W3) = W1 ) ) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mPttSet,axiom, % 59.58/59.59 ! [W0,W1] : % 59.58/59.59 ( ( aFunction0(W0) % 59.58/59.59 & aElement0(W1) ) % 59.58/59.59 => aSubsetOf0(sdtlbdtrb0(W0,W1),szDzozmdt0(W0)) ) ). % 59.58/59.59 % 59.58/59.59 fof(mDefSImg,definition, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aFunction0(W0) % 59.58/59.59 => ! [W1] : % 59.58/59.59 ( aSubsetOf0(W1,szDzozmdt0(W0)) % 59.58/59.59 => ! [W2] : % 59.58/59.59 ( W2 = sdtlcdtrc0(W0,W1) % 59.58/59.59 <=> ( aSet0(W2) % 59.58/59.59 & ! [W3] : % 59.58/59.59 ( aElementOf0(W3,W2) % 59.58/59.59 <=> ? [W4] : % 59.58/59.59 ( aElementOf0(W4,W1) % 59.58/59.59 & sdtlpdtrp0(W0,W4) = W3 ) ) ) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mImgRng,axiom, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aFunction0(W0) % 59.58/59.59 => ! [W1] : % 59.58/59.59 ( aElementOf0(W1,szDzozmdt0(W0)) % 59.58/59.59 => aElementOf0(sdtlpdtrp0(W0,W1),sdtlcdtrc0(W0,szDzozmdt0(W0))) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mDefRst,definition, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aFunction0(W0) % 59.58/59.59 => ! [W1] : % 59.58/59.59 ( aSubsetOf0(W1,szDzozmdt0(W0)) % 59.58/59.59 => ! [W2] : % 59.58/59.59 ( W2 = sdtexdt0(W0,W1) % 59.58/59.59 <=> ( aFunction0(W2) % 59.58/59.59 & szDzozmdt0(W2) = W1 % 59.58/59.59 & ! [W3] : % 59.58/59.59 ( aElementOf0(W3,W1) % 59.58/59.59 => sdtlpdtrp0(W2,W3) = sdtlpdtrp0(W0,W3) ) ) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mImgCount,axiom, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aFunction0(W0) % 59.58/59.59 => ! [W1] : % 59.58/59.59 ( ( aSubsetOf0(W1,szDzozmdt0(W0)) % 59.58/59.59 & isCountable0(W1) ) % 59.58/59.59 => ( ! [W2,W3] : % 59.58/59.59 ( ( aElementOf0(W2,szDzozmdt0(W0)) % 59.58/59.59 & aElementOf0(W3,szDzozmdt0(W0)) % 59.58/59.59 & W2 != W3 ) % 59.58/59.59 => sdtlpdtrp0(W0,W2) != sdtlpdtrp0(W0,W3) ) % 59.58/59.59 => isCountable0(sdtlcdtrc0(W0,W1)) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(mDirichlet,axiom, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aFunction0(W0) % 59.58/59.59 => ( ( isCountable0(szDzozmdt0(W0)) % 59.58/59.59 & isFinite0(sdtlcdtrc0(W0,szDzozmdt0(W0))) ) % 59.58/59.59 => ( aElement0(szDzizrdt0(W0)) % 59.58/59.59 & isCountable0(sdtlbdtrb0(W0,szDzizrdt0(W0))) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__3291,hypothesis, % 59.58/59.59 ( aSet0(xT) % 59.58/59.59 & isFinite0(xT) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__3418,hypothesis, % 59.58/59.59 aElementOf0(xK,szNzAzT0) ). % 59.58/59.59 % 59.58/59.59 fof(m__3435,hypothesis, % 59.58/59.59 ( aSubsetOf0(xS,szNzAzT0) % 59.58/59.59 & isCountable0(xS) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__3453,hypothesis, % 59.58/59.59 ( aFunction0(xc) % 59.58/59.59 & szDzozmdt0(xc) = slbdtsldtrb0(xS,xK) % 59.58/59.59 & aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__3398,hypothesis, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 => ! [W1] : % 59.58/59.59 ( ( aSubsetOf0(W1,szNzAzT0) % 59.58/59.59 & isCountable0(W1) ) % 59.58/59.59 => ! [W2] : % 59.58/59.59 ( ( aFunction0(W2) % 59.58/59.59 & szDzozmdt0(W2) = slbdtsldtrb0(W1,W0) % 59.58/59.59 & aSubsetOf0(sdtlcdtrc0(W2,szDzozmdt0(W2)),xT) ) % 59.58/59.59 => ( iLess0(W0,xK) % 59.58/59.59 => ? [W3] : % 59.58/59.59 ( aElementOf0(W3,xT) % 59.58/59.59 & ? [W4] : % 59.58/59.59 ( aSubsetOf0(W4,W1) % 59.58/59.59 & isCountable0(W4) % 59.58/59.59 & ! [W5] : % 59.58/59.59 ( aElementOf0(W5,slbdtsldtrb0(W4,W0)) % 59.58/59.59 => sdtlpdtrp0(W2,W5) = W3 ) ) ) ) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__3462,hypothesis, % 59.58/59.59 xK != sz00 ). % 59.58/59.59 % 59.58/59.59 fof(m__3520,hypothesis, % 59.58/59.59 xK != sz00 ). % 59.58/59.59 % 59.58/59.59 fof(m__3533,hypothesis, % 59.58/59.59 ( aElementOf0(xk,szNzAzT0) % 59.58/59.59 & szszuzczcdt0(xk) = xK ) ). % 59.58/59.59 % 59.58/59.59 fof(m__3623,hypothesis, % 59.58/59.59 ( aFunction0(xN) % 59.58/59.59 & szDzozmdt0(xN) = szNzAzT0 % 59.58/59.59 & sdtlpdtrp0(xN,sz00) = xS % 59.58/59.59 & ! [W0] : % 59.58/59.59 ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 => ( ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) % 59.58/59.59 & isCountable0(sdtlpdtrp0(xN,W0)) ) % 59.58/59.59 => ( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) % 59.58/59.59 & isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0))) ) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__3671,hypothesis, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 => ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) % 59.58/59.59 & isCountable0(sdtlpdtrp0(xN,W0)) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__3754,hypothesis, % 59.58/59.59 ! [W0,W1] : % 59.58/59.59 ( ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 & aElementOf0(W1,szNzAzT0) ) % 59.58/59.59 => ( sdtlseqdt0(W1,W0) % 59.58/59.59 => aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1)) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__3821,hypothesis, % 59.58/59.59 ! [W0,W1] : % 59.58/59.59 ( ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 & aElementOf0(W1,szNzAzT0) % 59.58/59.59 & W0 != W1 ) % 59.58/59.59 => szmzizndt0(sdtlpdtrp0(xN,W0)) != szmzizndt0(sdtlpdtrp0(xN,W1)) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__3965,hypothesis, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 => ! [W1] : % 59.58/59.59 ( ( aSet0(W1) % 59.58/59.59 & aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)) ) % 59.58/59.59 => aElementOf0(sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))),slbdtsldtrb0(xS,xK)) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__4151,hypothesis, % 59.58/59.59 ( aFunction0(xC) % 59.58/59.59 & szDzozmdt0(xC) = szNzAzT0 % 59.58/59.59 & ! [W0] : % 59.58/59.59 ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 => ( aFunction0(sdtlpdtrp0(xC,W0)) % 59.58/59.59 & szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk) % 59.58/59.59 & ! [W1] : % 59.58/59.59 ( ( aSet0(W1) % 59.58/59.59 & aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)) ) % 59.58/59.59 => sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) ) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__4182,hypothesis, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 => aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC,W0),szDzozmdt0(sdtlpdtrp0(xC,W0))),xT) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__4331,hypothesis, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 => ! [W1] : % 59.58/59.59 ( ( aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) % 59.58/59.59 & isCountable0(W1) ) % 59.58/59.59 => ! [W2] : % 59.58/59.59 ( ( aSet0(W2) % 59.58/59.59 & aElementOf0(W2,slbdtsldtrb0(W1,xk)) ) % 59.58/59.59 => aElementOf0(W2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__4411,hypothesis, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 => ? [W1] : % 59.58/59.59 ( aElementOf0(W1,xT) % 59.58/59.59 & ? [W2] : % 59.58/59.59 ( aSubsetOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) % 59.58/59.59 & isCountable0(W2) % 59.58/59.59 & ! [W3] : % 59.58/59.59 ( ( aSet0(W3) % 59.58/59.59 & aElementOf0(W3,slbdtsldtrb0(W2,xk)) ) % 59.58/59.59 => sdtlpdtrp0(sdtlpdtrp0(xC,W0),W3) = W1 ) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__4618,hypothesis, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 => ? [W1] : % 59.58/59.59 ( aElementOf0(W1,xT) % 59.58/59.59 & ! [W2] : % 59.58/59.59 ( ( aSet0(W2) % 59.58/59.59 & aElementOf0(W2,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk)) ) % 59.58/59.59 => sdtlpdtrp0(sdtlpdtrp0(xC,W0),W2) = W1 ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__4660,hypothesis, % 59.58/59.59 ( aFunction0(xe) % 59.58/59.59 & szDzozmdt0(xe) = szNzAzT0 % 59.58/59.59 & ! [W0] : % 59.58/59.59 ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 => sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0)) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__4730,hypothesis, % 59.58/59.59 ( aFunction0(xd) % 59.58/59.59 & szDzozmdt0(xd) = szNzAzT0 % 59.58/59.59 & ! [W0] : % 59.58/59.59 ( aElementOf0(W0,szNzAzT0) % 59.58/59.59 => ! [W1] : % 59.58/59.59 ( ( aSet0(W1) % 59.58/59.59 & aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk)) ) % 59.58/59.59 => sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) ) ) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__4758,hypothesis, % 59.58/59.59 aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT) ). % 59.58/59.59 % 59.58/59.59 fof(m__4854,hypothesis, % 59.58/59.59 ( aElementOf0(szDzizrdt0(xd),xT) % 59.58/59.59 & isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__4891,hypothesis, % 59.58/59.59 ( aSet0(xO) % 59.58/59.59 & xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__4908,hypothesis, % 59.58/59.59 ( aSet0(xO) % 59.58/59.59 & isCountable0(xO) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__4982,hypothesis, % 59.58/59.59 ! [W0] : % 59.58/59.59 ( aElementOf0(W0,xO) % 59.58/59.59 => ? [W1] : % 59.58/59.59 ( aElementOf0(W1,szNzAzT0) % 59.58/59.59 & aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) % 59.58/59.59 & sdtlpdtrp0(xe,W1) = W0 ) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__4998,hypothesis, % 59.58/59.59 aSubsetOf0(xO,xS) ). % 59.58/59.59 % 59.58/59.59 fof(m__5078,hypothesis, % 59.58/59.59 aElementOf0(xQ,slbdtsldtrb0(xO,xK)) ). % 59.58/59.59 % 59.58/59.59 fof(m__5093,hypothesis, % 59.58/59.59 ( aSubsetOf0(xQ,xO) % 59.58/59.59 & xQ != slcrc0 ) ). % 59.58/59.59 % 59.58/59.59 fof(m__5106,hypothesis, % 59.58/59.59 aSubsetOf0(xQ,szNzAzT0) ). % 59.58/59.59 % 59.58/59.59 fof(m__5116,hypothesis, % 59.58/59.59 aElementOf0(xQ,szDzozmdt0(xc)) ). % 59.58/59.59 % 59.58/59.59 fof(m__5147,hypothesis, % 59.58/59.59 xp = szmzizndt0(xQ) ). % 59.58/59.59 % 59.58/59.59 fof(m__5164,hypothesis, % 59.58/59.59 ( aSet0(xP) % 59.58/59.59 & xP = sdtmndt0(xQ,szmzizndt0(xQ)) ) ). % 59.58/59.59 % 59.58/59.59 fof(m__5173,hypothesis, % 59.58/59.59 aElementOf0(xp,xQ) ). % 59.58/59.59 % 59.58/59.59 fof(m__5182,hypothesis, % 59.58/59.59 aElementOf0(xp,xO) ). % 59.58/59.59 % 59.58/59.59 fof(m__5195,hypothesis, % 59.58/59.59 aSubsetOf0(xP,xQ) ). % 59.58/59.59 % 59.58/59.59 fof(m__5208,hypothesis, % 59.58/59.59 aSubsetOf0(xP,xO) ). % 59.58/59.59 % 59.58/59.59 fof(m__5217,hypothesis, % 59.58/59.59 sbrdtbr0(xP) = xk ). % 59.58/59.59 % 59.58/59.59 fof(m__5270,hypothesis, % 59.58/59.59 aElementOf0(xP,slbdtsldtrb0(xO,xk)) ). % 59.58/59.59 % 59.58/59.59 fof(m__,conjecture, % 59.58/59.59 ? [W0] : % 59.58/59.59 ( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) % 59.58/59.59 & sdtlpdtrp0(xe,W0) = xp ) ). % 59.58/59.59 % 59.58/59.59 %------------------------------------------------------------------------------ % 59.58/59.59 %------------------------------------------- % 59.58/59.59 % Proof found % 59.58/59.59 % SZS status Theorem for theBenchmark % 59.58/59.59 % SZS output start Proof % 59.58/59.59 %ClaNum:300(EqnAxiom:92) % 59.58/59.59 %VarNum:1231(SingletonVarNum:359) % 59.58/59.59 %MaxLitNum:9 % 59.58/59.59 %MaxfuncDepth:4 % 59.58/59.59 %SharedTerms:81 % 59.58/59.59 %goalClause: 226 % 59.58/59.59 [101]P1(a41) % 59.58/59.59 [102]P1(a53) % 59.58/59.59 [104]P1(a48) % 59.58/59.59 [105]P1(a46) % 59.58/59.59 [106]P5(a37) % 59.58/59.59 [107]P5(a53) % 59.58/59.59 [108]P6(a41) % 59.58/59.59 [109]P6(a54) % 59.58/59.59 [110]P6(a48) % 59.58/59.59 [111]P2(a55) % 59.58/59.59 [112]P2(a47) % 59.58/59.59 [113]P2(a45) % 59.58/59.59 [114]P2(a51) % 59.58/59.59 [115]P2(a52) % 59.58/59.59 [117]P3(a29,a41) % 59.58/59.59 [118]P3(a44,a41) % 59.58/59.59 [119]P3(a50,a41) % 59.58/59.59 [120]P3(a49,a48) % 59.58/59.59 [121]P3(a49,a1) % 59.58/59.59 [122]P7(a54,a41) % 59.58/59.59 [123]P7(a48,a54) % 59.58/59.59 [124]P7(a1,a41) % 59.58/59.59 [125]P7(a1,a48) % 59.58/59.59 [126]P7(a46,a48) % 59.58/59.59 [127]P7(a46,a1) % 59.58/59.59 [139]~E(a29,a44) % 59.58/59.59 [140]~E(a37,a1) % 59.58/59.59 [93]E(f2(a1),a49) % 59.58/59.59 [94]E(f43(a50),a44) % 59.58/59.59 [95]E(f3(a46),a50) % 59.58/59.59 [96]E(f30(a29),a37) % 59.58/59.59 [97]E(f39(a47),a41) % 59.58/59.59 [98]E(f39(a45),a41) % 59.58/59.59 [99]E(f39(a51),a41) % 59.58/59.59 [100]E(f39(a52),a41) % 59.58/59.59 [116]E(f31(a47,a29),a54) % 59.58/59.59 [128]E(f38(a54,a44),f39(a55)) % 59.58/59.59 [130]P3(a1,f39(a55)) % 59.58/59.59 [131]P3(f40(a52),a53) % 59.58/59.59 [132]P3(a1,f38(a48,a44)) % 59.58/59.59 [133]P3(a46,f38(a48,a50)) % 59.58/59.59 [129]E(f35(a1,f2(a1)),a46) % 59.58/59.59 [134]P6(f32(a52,f40(a52))) % 59.58/59.59 [136]P7(f34(a55,f39(a55)),a53) % 59.58/59.59 [137]P7(f34(a52,f39(a52)),a53) % 59.58/59.59 [135]E(f34(a51,f32(a52,f40(a52))),a48) % 59.58/59.59 [141]P1(x1411)+~E(x1411,a37) % 59.58/59.59 [148]~P1(x1481)+P7(x1481,x1481) % 59.58/59.59 [156]~P3(x1561,a41)+P9(a29,x1561) % 59.58/59.59 [162]P9(x1621,x1621)+~P3(x1621,a41) % 59.58/59.59 [145]~P2(x1451)+P1(f39(x1451)) % 59.58/59.59 [146]~P1(x1461)+P4(f3(x1461)) % 59.58/59.59 [150]~P3(x1501,a41)+~E(f43(x1501),a29) % 59.58/59.59 [151]~P3(x1511,a41)+~E(f43(x1511),x1511) % 59.58/59.59 [153]~P3(x1531,a41)+P5(f30(x1531)) % 59.58/59.59 [154]~P3(x1541,a41)+P6(f15(x1541)) % 59.58/59.59 [163]~P3(x1631,a41)+P3(f43(x1631),a41) % 59.58/59.59 [164]~P3(x1641,a41)+P3(f16(x1641),a53) % 59.58/59.59 [165]~P3(x1651,a41)+P3(f20(x1651),a53) % 59.58/59.59 [166]~P3(x1661,a48)+P3(f21(x1661),a41) % 59.58/59.59 [168]~P3(x1681,a41)+P9(x1681,f43(x1681)) % 59.58/59.59 [169]~P3(x1691,a41)+P8(x1691,f43(x1691)) % 59.58/59.60 [178]~P3(x1781,a41)+P6(f31(a47,x1781)) % 59.58/59.60 [179]~P3(x1791,a41)+P2(f31(a45,x1791)) % 59.58/59.60 [180]~P3(x1801,a41)+~P9(f43(x1801),a29) % 59.58/59.60 [188]~P3(x1881,a41)+P7(f31(a47,x1881),a41) % 59.58/59.60 [155]~P3(x1551,a41)+E(f3(f30(x1551)),x1551) % 59.58/59.60 [167]~P3(x1671,a48)+E(f31(a51,f21(x1671)),x1671) % 59.58/59.60 [190]~P3(x1901,a41)+E(f2(f31(a47,x1901)),f31(a51,x1901)) % 59.58/59.60 [208]~P3(x2081,a48)+P3(f21(x2081),f32(a52,f40(a52))) % 59.58/59.60 [226]~P3(x2261,f32(a52,f40(a52)))+~E(f31(a51,x2261),a49) % 59.58/59.60 [264]~P3(x2641,a41)+P7(f34(f31(a45,x2641),f39(f31(a45,x2641))),a53) % 59.58/59.60 [266]~P3(x2661,a41)+P7(f15(x2661),f35(f31(a47,x2661),f2(f31(a47,x2661)))) % 59.58/59.60 [268]~P3(x2681,a41)+E(f38(f35(f31(a47,x2681),f2(f31(a47,x2681))),a50),f39(f31(a45,x2681))) % 59.58/59.60 [149]~P3(x1492,x1491)+~E(x1491,a37) % 59.58/59.60 [144]~P1(x1441)+~P6(x1441)+~E(x1441,a37) % 59.58/59.60 [147]~P5(x1471)+~P6(x1471)+~P1(x1471) % 59.58/59.60 [142]~P1(x1421)+~E(x1421,a37)+E(f3(x1421),a29) % 59.58/59.60 [143]~P1(x1431)+E(x1431,a37)+~E(f3(x1431),a29) % 59.58/59.60 [152]~P1(x1521)+P3(f4(x1521),x1521)+E(x1521,a37) % 59.58/59.60 [159]~P1(x1591)+~P5(x1591)+P3(f3(x1591),a41) % 59.58/59.60 [170]~P3(x1701,a41)+E(x1701,a29)+P3(f19(x1701),a41) % 59.58/59.60 [171]~P1(x1711)+P5(x1711)+~P3(f3(x1711),a41) % 59.58/59.60 [177]~P5(x1771)+~P7(x1771,a41)+P3(f5(x1771),a41) % 59.58/59.60 [157]~P3(x1571,a41)+E(x1571,a29)+E(f43(f19(x1571)),x1571) % 59.58/59.60 [191]~P5(x1911)+~P7(x1911,a41)+P7(x1911,f30(f5(x1911))) % 59.58/59.60 [160]~P7(x1601,x1602)+P1(x1601)+~P1(x1602) % 59.58/59.60 [161]~P3(x1611,x1612)+P4(x1611)+~P1(x1612) % 59.58/59.60 [158]P1(x1581)+~P3(x1582,a41)+~E(x1581,f30(x1582)) % 59.58/59.60 [192]~P4(x1922)+~P2(x1921)+P7(f32(x1921,x1922),f39(x1921)) % 59.58/59.60 [209]~P2(x2091)+~P3(x2092,f39(x2091))+P4(f31(x2091,x2092)) % 59.58/59.60 [211]~P1(x2111)+~P3(x2112,x2111)+E(f36(f35(x2111,x2112),x2112),x2111) % 59.58/59.60 [248]~P2(x2481)+~P3(x2482,f39(x2481))+P3(f31(x2481,x2482),f34(x2481,f39(x2481))) % 59.58/59.60 [238]~P2(x2381)+~P6(f39(x2381))+P4(f40(x2381))+~P5(f34(x2381,f39(x2381))) % 59.58/59.60 [257]~P2(x2571)+~P6(f39(x2571))+~P5(f34(x2571,f39(x2571)))+P6(f32(x2571,f40(x2571))) % 59.58/59.60 [261]~P3(x2611,a41)+~P7(f31(a47,x2611),a41)+~P6(f31(a47,x2611))+P6(f31(a47,f43(x2611))) % 59.58/59.60 [285]~P3(x2851,a41)+~P7(f31(a47,x2851),a41)+~P6(f31(a47,x2851))+P7(f31(a47,f43(x2851)),f35(f31(a47,x2851),f2(f31(a47,x2851)))) % 59.58/59.60 [172]~P5(x1722)+~P7(x1721,x1722)+P5(x1721)+~P1(x1722) % 59.58/59.60 [176]P3(x1762,x1761)+~E(x1762,f2(x1761))+~P7(x1761,a41)+E(x1761,a37) % 59.58/59.60 [182]~P1(x1821)+~P4(x1822)+~P5(x1821)+P5(f36(x1821,x1822)) % 59.58/59.60 [183]~P1(x1831)+~P4(x1832)+~P5(x1831)+P5(f35(x1831,x1832)) % 59.58/59.60 [184]~P1(x1841)+~P4(x1842)+~P6(x1841)+P6(f36(x1841,x1842)) % 59.58/59.60 [185]~P1(x1851)+~P4(x1852)+~P6(x1851)+P6(f35(x1851,x1852)) % 59.58/59.60 [186]~P1(x1861)+P5(x1861)+~P3(x1862,a41)+~E(f38(x1861,x1862),a37) % 59.58/59.60 [189]E(x1891,x1892)+~E(f43(x1891),f43(x1892))+~P3(x1892,a41)+~P3(x1891,a41) % 59.58/59.60 [195]~P1(x1952)+~P5(x1952)+~P7(x1951,x1952)+P9(f3(x1951),f3(x1952)) % 59.58/59.60 [198]~P1(x1981)+~P5(x1981)+~P3(x1982,a41)+P5(f38(x1981,x1982)) % 59.58/59.60 [207]~P1(x2071)+~P1(x2072)+P7(x2071,x2072)+P3(f22(x2072,x2071),x2071) % 59.58/59.60 [215]P9(x2151,x2152)+P9(f43(x2152),x2151)+~P3(x2152,a41)+~P3(x2151,a41) % 59.58/59.60 [228]~P9(x2281,x2282)+~P3(x2282,a41)+~P3(x2281,a41)+P7(f30(x2281),f30(x2282)) % 59.58/59.60 [229]~P9(x2291,x2292)+~P3(x2292,a41)+~P3(x2291,a41)+P9(f43(x2291),f43(x2292)) % 59.58/59.60 [231]~P1(x2311)+~P1(x2312)+P7(x2311,x2312)+~P3(f22(x2312,x2311),x2312) % 59.58/59.60 [233]P9(x2331,x2332)+~P3(x2332,a41)+~P3(x2331,a41)+~P7(f30(x2331),f30(x2332)) % 59.58/59.60 [234]P9(x2341,x2342)+~P3(x2342,a41)+~P3(x2341,a41)+~P9(f43(x2341),f43(x2342)) % 59.58/59.60 [252]~P9(x2522,x2521)+~P3(x2522,a41)+~P3(x2521,a41)+P7(f31(a47,x2521),f31(a47,x2522)) % 59.58/59.60 [210]P3(x2102,x2101)+~P1(x2101)+~P4(x2102)+E(f35(f36(x2101,x2102),x2102),x2101) % 59.58/59.60 [218]~E(x2181,x2182)+~P3(x2182,a41)+~P3(x2181,a41)+P3(x2181,f30(f43(x2182))) % 59.58/59.60 [240]~P3(x2402,a41)+~P3(x2401,a41)+~P3(x2401,f30(x2402))+P3(x2401,f30(f43(x2402))) % 59.58/59.60 [256]E(x2561,x2562)+~P3(x2562,a41)+~P3(x2561,a41)+~E(f2(f31(a47,x2561)),f2(f31(a47,x2562))) % 59.58/59.60 [259]~P1(x2592)+~P3(x2591,a41)+E(f31(f31(a45,x2591),x2592),f16(x2591))+~P3(x2592,f38(f15(x2591),a50)) % 59.58/59.60 [239]~P1(x2391)+~P5(x2391)+~P3(x2392,x2391)+E(f43(f3(f35(x2391,x2392))),f3(x2391)) % 59.58/59.60 [269]~P1(x2692)+~P3(x2691,a41)+E(f31(f31(a45,x2691),x2692),f20(x2691))+~P3(x2692,f38(f31(a47,f43(x2691)),a50)) % 59.58/59.60 [271]~P1(x2712)+~P3(x2711,a41)+E(f31(f31(a45,x2711),x2712),f31(a52,x2711))+~P3(x2712,f38(f31(a47,f43(x2711)),a50)) % 59.58/59.60 [299]~P1(x2991)+~P3(x2992,a41)+P3(f36(x2991,f2(f31(a47,x2992))),f38(a54,a44))+~P3(x2991,f38(f35(f31(a47,x2992),f2(f31(a47,x2992))),a50)) % 59.58/59.60 [300]~P1(x3001)+~P3(x3002,a41)+~P3(x3001,f38(f35(f31(a47,x3002),f2(f31(a47,x3002))),a50))+E(f31(a55,f36(x3001,f2(f31(a47,x3002)))),f31(f31(a45,x3002),x3001)) % 59.58/59.60 [202]~P1(x2022)+~P7(x2023,x2022)+P3(x2021,x2022)+~P3(x2021,x2023) % 59.58/59.60 [173]~P1(x1732)+~P4(x1733)+P1(x1731)+~E(x1731,f36(x1732,x1733)) % 59.58/59.60 [174]~P1(x1742)+~P4(x1743)+P1(x1741)+~E(x1741,f35(x1742,x1743)) % 59.58/59.60 [175]~P4(x1753)+~P2(x1752)+P1(x1751)+~E(x1751,f32(x1752,x1753)) % 59.58/59.60 [187]~P1(x1872)+P1(x1871)+~P3(x1873,a41)+~E(x1871,f38(x1872,x1873)) % 59.58/59.60 [196]~P3(x1961,x1962)+~P3(x1963,a41)+P3(x1961,a41)+~E(x1962,f30(x1963)) % 59.58/59.60 [204]~P2(x2042)+P1(x2041)+~P7(x2043,f39(x2042))+~E(x2041,f34(x2042,x2043)) % 59.58/59.60 [205]~P2(x2052)+P2(x2051)+~P7(x2053,f39(x2052))+~E(x2051,f33(x2052,x2053)) % 59.58/59.60 [206]~P2(x2063)+~P7(x2062,f39(x2063))+E(f39(x2061),x2062)+~E(x2061,f33(x2063,x2062)) % 59.58/59.60 [212]~P3(x2121,x2123)+~P3(x2122,a41)+P9(f43(x2121),x2122)+~E(x2123,f30(x2122)) % 59.58/59.60 [193]~P1(x1932)+~P1(x1931)+~P7(x1932,x1931)+~P7(x1931,x1932)+E(x1931,x1932) % 59.58/59.60 [225]~P9(x2252,x2251)+~P9(x2251,x2252)+E(x2251,x2252)+~P3(x2252,a41)+~P3(x2251,a41) % 59.58/59.60 [181]~P5(x1811)+P3(x1812,x1811)+~E(x1812,f42(x1811))+~P7(x1811,a41)+E(x1811,a37) % 59.58/59.60 [201]~P1(x2012)+~P6(x2012)+~P3(x2011,a41)+E(x2011,a29)+P6(f38(x2012,x2011)) % 59.58/59.60 [230]~P3(x2302,x2301)+P3(f25(x2301,x2302),x2301)+~P7(x2301,a41)+E(x2301,a37)+E(x2302,f2(x2301)) % 59.58/59.60 [241]~P1(x2411)+~P5(x2411)+~P3(x2412,a41)+~P9(x2412,f3(x2411))+P7(f26(x2411,x2412),x2411) % 59.58/59.60 [243]~P1(x2431)+P3(f28(x2432,x2431),x2431)+~P3(x2432,a41)+E(x2431,f30(x2432))+P3(f28(x2432,x2431),a41) % 59.58/59.60 [244]~P3(x2442,x2441)+~P7(x2441,a41)+~P9(x2442,f25(x2441,x2442))+E(x2441,a37)+E(x2442,f2(x2441)) % 59.58/59.60 [251]~P6(x2512)+~P2(x2511)+~E(f6(x2511,x2512),f7(x2511,x2512))+~P7(x2512,f39(x2511))+P6(f34(x2511,x2512)) % 59.58/59.60 [253]~P6(x2532)+~P2(x2531)+P3(f7(x2531,x2532),f39(x2531))+~P7(x2532,f39(x2531))+P6(f34(x2531,x2532)) % 59.58/59.60 [254]~P6(x2542)+~P2(x2541)+P3(f6(x2541,x2542),f39(x2541))+~P7(x2542,f39(x2541))+P6(f34(x2541,x2542)) % 59.58/59.60 [217]P3(x2172,x2171)+~P1(x2171)+~P4(x2172)+~P5(x2171)+E(f3(f36(x2171,x2172)),f43(f3(x2171))) % 59.58/59.60 [237]~P1(x2371)+~P5(x2371)+~P3(x2372,a41)+~P9(x2372,f3(x2371))+E(f3(f26(x2371,x2372)),x2372) % 59.58/59.60 [246]E(x2461,x2462)+P3(x2461,f30(x2462))+~P3(x2462,a41)+~P3(x2461,a41)+~P3(x2461,f30(f43(x2462))) % 59.58/59.60 [258]~P1(x2581)+P3(f28(x2582,x2581),x2581)+~P3(x2582,a41)+E(x2581,f30(x2582))+P9(f43(f28(x2582,x2581)),x2582) % 59.58/59.60 [260]~P6(x2602)+~P2(x2601)+~P7(x2602,f39(x2601))+P6(f34(x2601,x2602))+E(f31(x2601,f6(x2601,x2602)),f31(x2601,f7(x2601,x2602))) % 59.58/59.60 [203]~P3(x2033,x2031)+P9(x2032,x2033)+~E(x2032,f2(x2031))+~P7(x2031,a41)+E(x2031,a37) % 59.58/59.60 [232]P3(x2321,x2322)+~P3(x2323,a41)+~P3(x2321,a41)+~P9(f43(x2321),x2323)+~E(x2322,f30(x2323)) % 59.58/59.60 [265]~P1(x2651)+~P5(x2653)+~P3(x2652,a41)+~P7(x2653,f38(x2651,x2652))+P5(f9(x2651,x2652,x2653)) % 59.58/59.60 [267]~P1(x2671)+~P5(x2673)+~P3(x2672,a41)+~P7(x2673,f38(x2671,x2672))+P7(f9(x2671,x2672,x2673),x2671) % 59.58/59.60 [286]~P1(x2862)+~P5(x2861)+~P3(x2863,a41)+~P7(x2861,f38(x2862,x2863))+P7(x2861,f38(f9(x2862,x2863,x2861),x2863)) % 59.58/59.60 [197]~P1(x1974)+~P4(x1972)+~P3(x1971,x1973)+~E(x1971,x1972)+~E(x1973,f35(x1974,x1972)) % 59.58/59.60 [199]~P1(x1993)+~P4(x1994)+~P3(x1991,x1992)+P4(x1991)+~E(x1992,f36(x1993,x1994)) % 59.58/59.60 [200]~P1(x2003)+~P4(x2004)+~P3(x2001,x2002)+P4(x2001)+~E(x2002,f35(x2003,x2004)) % 59.58/59.60 [214]~P1(x2142)+~P4(x2144)+~P3(x2141,x2143)+P3(x2141,x2142)+~E(x2143,f35(x2142,x2144)) % 59.58/59.60 [216]~P4(x2163)+~P2(x2161)+~P3(x2162,x2164)+E(f31(x2161,x2162),x2163)+~E(x2164,f32(x2161,x2163)) % 59.58/59.60 [220]~P1(x2204)+~P3(x2201,x2203)+~P3(x2202,a41)+E(f3(x2201),x2202)+~E(x2203,f38(x2204,x2202)) % 59.58/59.60 [222]~P4(x2224)+~P2(x2222)+~P3(x2221,x2223)+P3(x2221,f39(x2222))+~E(x2223,f32(x2222,x2224)) % 59.58/59.60 [227]~P1(x2272)+~P3(x2271,x2273)+P7(x2271,x2272)+~P3(x2274,a41)+~E(x2273,f38(x2272,x2274)) % 59.58/59.60 [245]~P2(x2453)+~P3(x2452,x2454)+~P7(x2454,f39(x2453))+E(f31(x2451,x2452),f31(x2453,x2452))+~E(x2451,f33(x2453,x2454)) % 59.58/59.60 [292]~P2(x2921)+~P3(x2924,x2923)+~E(x2923,f34(x2921,x2922))+~P7(x2922,f39(x2921))+P3(f13(x2921,x2922,x2923,x2924),x2922) % 59.58/59.60 [293]~P2(x2931)+~P3(x2934,x2933)+~E(x2933,f34(x2931,x2932))+~P7(x2932,f39(x2931))+E(f31(x2931,f13(x2931,x2932,x2933,x2934)),x2934) % 59.58/59.60 [236]~P5(x2361)+~P3(x2362,x2361)+P3(f27(x2361,x2362),x2361)+~P7(x2361,a41)+E(x2361,a37)+E(x2362,f42(x2361)) % 59.58/59.60 [249]~P5(x2491)+~P3(x2492,x2491)+~P7(x2491,a41)+~P9(f27(x2491,x2492),x2492)+E(x2491,a37)+E(x2492,f42(x2491)) % 59.58/59.60 [274]~P1(x2741)+~P3(x2742,a41)+~P3(f28(x2742,x2741),x2741)+E(x2741,f30(x2742))+~P3(f28(x2742,x2741),a41)+~P9(f43(f28(x2742,x2741)),x2742) % 59.58/59.60 [221]~P1(x2212)+~P1(x2211)+~P7(x2213,x2212)+~P7(x2211,x2213)+P7(x2211,x2212)+~P1(x2213) % 59.58/59.60 [250]~P9(x2501,x2503)+P9(x2501,x2502)+~P9(x2503,x2502)+~P3(x2502,a41)+~P3(x2503,a41)+~P3(x2501,a41) % 59.58/59.60 [213]~P5(x2131)+~P3(x2132,x2131)+P9(x2132,x2133)+~E(x2133,f42(x2131))+~P7(x2131,a41)+E(x2131,a37) % 59.58/59.60 [263]~P2(x2631)+~P2(x2632)+P3(f8(x2632,x2633,x2631),x2633)+~E(f39(x2631),x2633)+~P7(x2633,f39(x2632))+E(x2631,f33(x2632,x2633)) % 59.58/59.60 [270]~P1(x2701)+~P1(x2702)+~P4(x2703)+P3(f23(x2702,x2703,x2701),x2701)+~E(f23(x2702,x2703,x2701),x2703)+E(x2701,f35(x2702,x2703)) % 59.58/59.60 [272]~P1(x2721)+~P1(x2722)+~P4(x2723)+P3(f24(x2722,x2723,x2721),x2721)+E(x2721,f36(x2722,x2723))+P4(f24(x2722,x2723,x2721)) % 59.58/59.60 [273]~P1(x2731)+~P1(x2732)+~P4(x2733)+P3(f23(x2732,x2733,x2731),x2731)+E(x2731,f35(x2732,x2733))+P4(f23(x2732,x2733,x2731)) % 59.58/59.60 [275]~P1(x2751)+~P1(x2752)+~P4(x2753)+P3(f23(x2752,x2753,x2751),x2751)+P3(f23(x2752,x2753,x2751),x2752)+E(x2751,f35(x2752,x2753)) % 59.58/59.60 [278]~P1(x2781)+~P4(x2783)+~P2(x2782)+P3(f11(x2782,x2783,x2781),x2781)+P3(f11(x2782,x2783,x2781),f39(x2782))+E(x2781,f32(x2782,x2783)) % 59.58/59.60 [279]~P1(x2791)+~P1(x2792)+P3(f10(x2792,x2793,x2791),x2791)+P7(f10(x2792,x2793,x2791),x2792)+~P3(x2793,a41)+E(x2791,f38(x2792,x2793)) % 59.58/59.60 [282]~P1(x2821)+~P2(x2822)+P3(f12(x2822,x2823,x2821),x2821)+P3(f14(x2822,x2823,x2821),x2823)+~P7(x2823,f39(x2822))+E(x2821,f34(x2822,x2823)) % 59.58/59.60 [276]~P1(x2761)+~P4(x2763)+~P2(x2762)+P3(f11(x2762,x2763,x2761),x2761)+E(x2761,f32(x2762,x2763))+E(f31(x2762,f11(x2762,x2763,x2761)),x2763) % 59.58/59.60 [277]~P1(x2771)+~P1(x2772)+P3(f10(x2772,x2773,x2771),x2771)+~P3(x2773,a41)+E(x2771,f38(x2772,x2773))+E(f3(f10(x2772,x2773,x2771)),x2773) % 59.58/59.60 [287]~P1(x2871)+~P2(x2872)+P3(f12(x2872,x2873,x2871),x2871)+~P7(x2873,f39(x2872))+E(x2871,f34(x2872,x2873))+E(f31(x2872,f14(x2872,x2873,x2871)),f12(x2872,x2873,x2871)) % 59.58/59.60 [289]~P2(x2892)+~P2(x2891)+~E(f39(x2891),x2893)+~P7(x2893,f39(x2892))+E(x2891,f33(x2892,x2893))+~E(f31(x2891,f8(x2892,x2893,x2891)),f31(x2892,f8(x2892,x2893,x2891))) % 59.58/59.60 [298]~P1(x2981)+~P6(x2983)+~P3(x2982,a41)+~P3(x2981,f38(x2983,a50))+~P7(x2983,f35(f31(a47,x2982),f2(f31(a47,x2982))))+P3(x2981,f38(f35(f31(a47,x2982),f2(f31(a47,x2982))),a50)) % 59.58/59.60 [194]~P1(x1944)+~P4(x1943)+~P4(x1941)+P3(x1941,x1942)+~E(x1941,x1943)+~E(x1942,f36(x1944,x1943)) % 59.58/59.60 [219]~P1(x2193)+~P4(x2192)+~P3(x2191,x2194)+E(x2191,x2192)+P3(x2191,x2193)+~E(x2194,f36(x2193,x2192)) % 59.58/59.60 [223]~P1(x2233)+~P4(x2234)+~P4(x2231)+~P3(x2231,x2233)+P3(x2231,x2232)+~E(x2232,f36(x2233,x2234)) % 59.58/59.60 [235]~P1(x2354)+~P7(x2351,x2354)+P3(x2351,x2352)+~P3(x2353,a41)+~E(x2352,f38(x2354,x2353))+~E(f3(x2351),x2353) % 59.58/59.60 [242]~P4(x2424)+~P2(x2423)+P3(x2421,x2422)+~E(f31(x2423,x2421),x2424)+~P3(x2421,f39(x2423))+~E(x2422,f32(x2423,x2424)) % 59.58/59.60 [255]~P2(x2553)+~P3(x2555,x2554)+P3(x2551,x2552)+~P7(x2554,f39(x2553))+~E(x2552,f34(x2553,x2554))+~E(f31(x2553,x2555),x2551) % 59.58/59.60 [247]E(f2(x2472),f2(x2471))+~P7(x2471,a41)+~P7(x2472,a41)+~P3(f2(x2471),x2472)+~P3(f2(x2472),x2471)+E(x2471,a37)+E(x2472,a37) % 59.58/59.60 [262]~P1(x2623)+~P1(x2622)+P7(x2622,x2623)+~P3(x2621,a41)+~P7(f38(x2622,x2621),f38(x2623,x2621))+E(x2621,a29)+E(f38(x2622,x2621),a37) % 59.58/59.60 [284]~P1(x2841)+~P1(x2842)+~P4(x2843)+E(f24(x2842,x2843,x2841),x2843)+P3(f24(x2842,x2843,x2841),x2841)+P3(f24(x2842,x2843,x2841),x2842)+E(x2841,f36(x2842,x2843)) % 59.58/59.60 [290]~P1(x2901)+~P1(x2902)+~P4(x2903)+~E(f24(x2902,x2903,x2901),x2903)+~P3(f24(x2902,x2903,x2901),x2901)+E(x2901,f36(x2902,x2903))+~P4(f24(x2902,x2903,x2901)) % 59.58/59.60 [291]~P1(x2911)+~P1(x2912)+~P4(x2913)+~P3(f24(x2912,x2913,x2911),x2911)+~P3(f24(x2912,x2913,x2911),x2912)+E(x2911,f36(x2912,x2913))+~P4(f24(x2912,x2913,x2911)) % 59.58/59.60 [294]~P1(x2941)+~P1(x2942)+~P3(x2943,a41)+~P3(f10(x2942,x2943,x2941),x2941)+~P7(f10(x2942,x2943,x2941),x2942)+E(x2941,f38(x2942,x2943))+~E(f3(f10(x2942,x2943,x2941)),x2943) % 59.58/59.60 [295]~P1(x2951)+~P4(x2953)+~P2(x2952)+~P3(f11(x2952,x2953,x2951),x2951)+~P3(f11(x2952,x2953,x2951),f39(x2952))+E(x2951,f32(x2952,x2953))+~E(f31(x2952,f11(x2952,x2953,x2951)),x2953) % 59.58/59.60 [224]~P1(x2244)+~P4(x2242)+~P4(x2241)+~P3(x2241,x2244)+E(x2241,x2242)+P3(x2241,x2243)+~E(x2243,f35(x2244,x2242)) % 59.58/59.60 [288]~P1(x2881)+~P2(x2882)+~P3(x2884,x2883)+~P7(x2883,f39(x2882))+~P3(f12(x2882,x2883,x2881),x2881)+~E(f31(x2882,x2884),f12(x2882,x2883,x2881))+E(x2881,f34(x2882,x2883)) % 59.58/59.60 [296]~P1(x2961)+~P1(x2962)+~P4(x2963)+E(f23(x2962,x2963,x2961),x2963)+~P3(f23(x2962,x2963,x2961),x2961)+~P3(f23(x2962,x2963,x2961),x2962)+E(x2961,f35(x2962,x2963))+~P4(f23(x2962,x2963,x2961)) % 59.58/59.60 [280]~P6(x2802)+~P2(x2803)+~E(f39(x2803),f38(x2802,x2801))+~P3(x2801,a41)+~P7(x2802,a41)+~P8(x2801,a44)+P6(f17(x2801,x2802,x2803))+~P7(f34(x2803,f39(x2803)),a53) % 59.58/59.60 [281]~P6(x2812)+~P2(x2813)+~E(f39(x2813),f38(x2812,x2811))+~P3(x2811,a41)+~P7(x2812,a41)+~P8(x2811,a44)+P3(f18(x2811,x2812,x2813),a53)+~P7(f34(x2813,f39(x2813)),a53) % 59.58/59.60 [283]~P6(x2832)+~P2(x2833)+~E(f39(x2833),f38(x2832,x2831))+~P3(x2831,a41)+~P7(x2832,a41)+~P8(x2831,a44)+P7(f17(x2831,x2832,x2833),x2832)+~P7(f34(x2833,f39(x2833)),a53) % 59.58/59.60 [297]~P6(x2974)+~P2(x2971)+~E(f39(x2971),f38(x2974,x2973))+~P3(x2973,a41)+~P7(x2974,a41)+~P8(x2973,a44)+E(f31(x2971,x2972),f18(x2973,x2974,x2971))+~P3(x2972,f38(f17(x2973,x2974,x2971),x2973))+~P7(f34(x2971,f39(x2971)),a53) % 59.58/59.60 %EqnAxiom % 59.58/59.60 [1]E(x11,x11) % 59.58/59.60 [2]E(x22,x21)+~E(x21,x22) % 59.58/59.60 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.58/59.60 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 59.58/59.60 [5]~E(x51,x52)+E(f43(x51),f43(x52)) % 59.58/59.60 [6]~E(x61,x62)+E(f3(x61),f3(x62)) % 59.58/59.60 [7]~E(x71,x72)+E(f30(x71),f30(x72)) % 59.58/59.60 [8]~E(x81,x82)+E(f39(x81),f39(x82)) % 59.58/59.60 [9]~E(x91,x92)+E(f34(x91,x93),f34(x92,x93)) % 59.58/59.60 [10]~E(x101,x102)+E(f34(x103,x101),f34(x103,x102)) % 59.58/59.60 [11]~E(x111,x112)+E(f38(x111,x113),f38(x112,x113)) % 59.58/59.60 [12]~E(x121,x122)+E(f38(x123,x121),f38(x123,x122)) % 59.58/59.60 [13]~E(x131,x132)+E(f35(x131,x133),f35(x132,x133)) % 59.58/59.60 [14]~E(x141,x142)+E(f35(x143,x141),f35(x143,x142)) % 59.58/59.60 [15]~E(x151,x152)+E(f31(x151,x153),f31(x152,x153)) % 59.58/59.60 [16]~E(x161,x162)+E(f31(x163,x161),f31(x163,x162)) % 59.58/59.60 [17]~E(x171,x172)+E(f10(x171,x173,x174),f10(x172,x173,x174)) % 59.58/59.60 [18]~E(x181,x182)+E(f10(x183,x181,x184),f10(x183,x182,x184)) % 59.58/59.60 [19]~E(x191,x192)+E(f10(x193,x194,x191),f10(x193,x194,x192)) % 59.58/59.60 [20]~E(x201,x202)+E(f9(x201,x203,x204),f9(x202,x203,x204)) % 59.58/59.60 [21]~E(x211,x212)+E(f9(x213,x211,x214),f9(x213,x212,x214)) % 59.58/59.60 [22]~E(x221,x222)+E(f9(x223,x224,x221),f9(x223,x224,x222)) % 59.58/59.60 [23]~E(x231,x232)+E(f11(x231,x233,x234),f11(x232,x233,x234)) % 59.58/59.60 [24]~E(x241,x242)+E(f11(x243,x241,x244),f11(x243,x242,x244)) % 59.58/59.60 [25]~E(x251,x252)+E(f11(x253,x254,x251),f11(x253,x254,x252)) % 59.58/59.60 [26]~E(x261,x262)+E(f33(x261,x263),f33(x262,x263)) % 59.58/59.60 [27]~E(x271,x272)+E(f33(x273,x271),f33(x273,x272)) % 59.58/59.60 [28]~E(x281,x282)+E(f24(x281,x283,x284),f24(x282,x283,x284)) % 59.58/59.60 [29]~E(x291,x292)+E(f24(x293,x291,x294),f24(x293,x292,x294)) % 59.58/59.60 [30]~E(x301,x302)+E(f24(x303,x304,x301),f24(x303,x304,x302)) % 59.58/59.60 [31]~E(x311,x312)+E(f40(x311),f40(x312)) % 59.58/59.60 [32]~E(x321,x322)+E(f20(x321),f20(x322)) % 59.58/59.60 [33]~E(x331,x332)+E(f32(x331,x333),f32(x332,x333)) % 59.58/59.60 [34]~E(x341,x342)+E(f32(x343,x341),f32(x343,x342)) % 59.58/59.60 [35]~E(x351,x352)+E(f36(x351,x353),f36(x352,x353)) % 59.58/59.60 [36]~E(x361,x362)+E(f36(x363,x361),f36(x363,x362)) % 59.58/59.60 [37]~E(x371,x372)+E(f23(x371,x373,x374),f23(x372,x373,x374)) % 59.58/59.60 [38]~E(x381,x382)+E(f23(x383,x381,x384),f23(x383,x382,x384)) % 59.58/59.60 [39]~E(x391,x392)+E(f23(x393,x394,x391),f23(x393,x394,x392)) % 59.58/59.60 [40]~E(x401,x402)+E(f8(x401,x403,x404),f8(x402,x403,x404)) % 59.58/59.60 [41]~E(x411,x412)+E(f8(x413,x411,x414),f8(x413,x412,x414)) % 59.58/59.60 [42]~E(x421,x422)+E(f8(x423,x424,x421),f8(x423,x424,x422)) % 59.58/59.60 [43]~E(x431,x432)+E(f17(x431,x433,x434),f17(x432,x433,x434)) % 59.58/59.60 [44]~E(x441,x442)+E(f17(x443,x441,x444),f17(x443,x442,x444)) % 59.58/59.60 [45]~E(x451,x452)+E(f17(x453,x454,x451),f17(x453,x454,x452)) % 59.58/59.60 [46]~E(x461,x462)+E(f28(x461,x463),f28(x462,x463)) % 59.58/59.60 [47]~E(x471,x472)+E(f28(x473,x471),f28(x473,x472)) % 59.58/59.60 [48]~E(x481,x482)+E(f15(x481),f15(x482)) % 59.58/59.60 [49]~E(x491,x492)+E(f26(x491,x493),f26(x492,x493)) % 59.58/59.60 [50]~E(x501,x502)+E(f26(x503,x501),f26(x503,x502)) % 59.58/59.60 [51]~E(x511,x512)+E(f6(x511,x513),f6(x512,x513)) % 59.58/59.60 [52]~E(x521,x522)+E(f6(x523,x521),f6(x523,x522)) % 59.58/59.60 [53]~E(x531,x532)+E(f12(x531,x533,x534),f12(x532,x533,x534)) % 59.58/59.60 [54]~E(x541,x542)+E(f12(x543,x541,x544),f12(x543,x542,x544)) % 59.58/59.60 [55]~E(x551,x552)+E(f12(x553,x554,x551),f12(x553,x554,x552)) % 59.58/59.60 [56]~E(x561,x562)+E(f42(x561),f42(x562)) % 59.58/59.60 [57]~E(x571,x572)+E(f27(x571,x573),f27(x572,x573)) % 59.58/59.60 [58]~E(x581,x582)+E(f27(x583,x581),f27(x583,x582)) % 59.58/59.60 [59]~E(x591,x592)+E(f25(x591,x593),f25(x592,x593)) % 59.58/59.60 [60]~E(x601,x602)+E(f25(x603,x601),f25(x603,x602)) % 59.58/59.60 [61]~E(x611,x612)+E(f5(x611),f5(x612)) % 59.58/59.60 [62]~E(x621,x622)+E(f16(x621),f16(x622)) % 59.58/59.60 [63]~E(x631,x632)+E(f18(x631,x633,x634),f18(x632,x633,x634)) % 59.58/59.60 [64]~E(x641,x642)+E(f18(x643,x641,x644),f18(x643,x642,x644)) % 59.58/59.60 [65]~E(x651,x652)+E(f18(x653,x654,x651),f18(x653,x654,x652)) % 59.58/59.60 [66]~E(x661,x662)+E(f4(x661),f4(x662)) % 59.58/59.60 [67]~E(x671,x672)+E(f14(x671,x673,x674),f14(x672,x673,x674)) % 59.58/59.60 [68]~E(x681,x682)+E(f14(x683,x681,x684),f14(x683,x682,x684)) % 59.58/59.60 [69]~E(x691,x692)+E(f14(x693,x694,x691),f14(x693,x694,x692)) % 59.58/59.60 [70]~E(x701,x702)+E(f7(x701,x703),f7(x702,x703)) % 59.58/59.60 [71]~E(x711,x712)+E(f7(x713,x711),f7(x713,x712)) % 59.58/59.60 [72]~E(x721,x722)+E(f13(x721,x723,x724,x725),f13(x722,x723,x724,x725)) % 59.58/59.60 [73]~E(x731,x732)+E(f13(x733,x731,x734,x735),f13(x733,x732,x734,x735)) % 59.58/59.60 [74]~E(x741,x742)+E(f13(x743,x744,x741,x745),f13(x743,x744,x742,x745)) % 59.58/59.60 [75]~E(x751,x752)+E(f13(x753,x754,x755,x751),f13(x753,x754,x755,x752)) % 59.58/59.60 [76]~E(x761,x762)+E(f21(x761),f21(x762)) % 59.58/59.60 [77]~E(x771,x772)+E(f19(x771),f19(x772)) % 59.58/59.60 [78]~E(x781,x782)+E(f22(x781,x783),f22(x782,x783)) % 59.58/59.60 [79]~E(x791,x792)+E(f22(x793,x791),f22(x793,x792)) % 59.58/59.60 [80]~P1(x801)+P1(x802)+~E(x801,x802) % 59.58/59.60 [81]P3(x812,x813)+~E(x811,x812)+~P3(x811,x813) % 59.58/59.60 [82]P3(x823,x822)+~E(x821,x822)+~P3(x823,x821) % 59.58/59.60 [83]~P6(x831)+P6(x832)+~E(x831,x832) % 59.58/59.60 [84]P7(x842,x843)+~E(x841,x842)+~P7(x841,x843) % 59.58/59.60 [85]P7(x853,x852)+~E(x851,x852)+~P7(x853,x851) % 59.58/59.60 [86]~P2(x861)+P2(x862)+~E(x861,x862) % 59.58/59.60 [87]~P5(x871)+P5(x872)+~E(x871,x872) % 59.58/59.60 [88]~P4(x881)+P4(x882)+~E(x881,x882) % 59.58/59.60 [89]P9(x892,x893)+~E(x891,x892)+~P9(x891,x893) % 59.58/59.60 [90]P9(x903,x902)+~E(x901,x902)+~P9(x903,x901) % 59.58/59.60 [91]P8(x912,x913)+~E(x911,x912)+~P8(x911,x913) % 59.58/59.60 [92]P8(x923,x922)+~E(x921,x922)+~P8(x923,x921) % 59.58/59.60 % 59.58/59.60 %------------------------------------------- % 59.58/59.60 cnf(301,plain, % 59.58/59.60 (P1(a37)), % 59.58/59.60 inference(equality_inference,[],[141])). % 59.58/59.60 cnf(302,plain, % 59.58/59.60 (~P1(a37)+E(f3(a37),a29)), % 59.58/59.60 inference(equality_inference,[],[142])). % 59.58/59.60 cnf(303,plain, % 59.58/59.60 (~P6(a37)+~P1(a37)), % 59.58/59.60 inference(equality_inference,[],[144])). % 59.58/59.60 cnf(304,plain, % 59.58/59.60 (~P3(x3041,a37)), % 59.58/59.60 inference(equality_inference,[],[149])). % 59.58/59.60 cnf(305,plain, % 59.58/59.60 (P1(f30(x3051))+~P3(x3051,a41)), % 59.58/59.60 inference(equality_inference,[],[158])). % 59.58/59.60 cnf(309,plain, % 59.58/59.60 (P3(f2(x3091),x3091)+~P7(x3091,a41)+E(x3091,a37)), % 59.58/59.60 inference(equality_inference,[],[176])). % 59.58/59.60 cnf(311,plain, % 59.58/59.60 (~P1(x3111)+P1(f38(x3111,x3112))+~P3(x3112,a41)), % 59.58/59.60 inference(equality_inference,[],[187])). % 59.58/59.60 cnf(316,plain, % 59.58/59.60 (~P3(x3161,x3162)+P9(f2(x3162),x3161)+~P7(x3162,a41)+E(x3162,a37)), % 59.58/59.60 inference(equality_inference,[],[203])). % 59.58/59.60 cnf(317,plain, % 59.58/59.60 (~P2(x3171)+P1(f34(x3171,x3172))+~P7(x3172,f39(x3171))), % 59.58/59.60 inference(equality_inference,[],[204])). % 59.58/59.60 cnf(318,plain, % 59.58/59.60 (~P2(x3181)+P2(f33(x3181,x3182))+~P7(x3182,f39(x3181))), % 59.58/59.60 inference(equality_inference,[],[205])). % 59.58/59.60 cnf(319,plain, % 59.58/59.60 (~P2(x3191)+~P7(x3192,f39(x3191))+E(f39(f33(x3191,x3192)),x3192)), % 59.58/59.60 inference(equality_inference,[],[206])). % 59.58/59.60 cnf(320,plain, % 59.58/59.60 (~P3(x3201,f30(x3202))+P9(f43(x3201),x3202)+~P3(x3202,a41)), % 59.58/59.60 inference(equality_inference,[],[212])). % 59.58/59.60 cnf(324,plain, % 59.58/59.60 (~P3(x3241,a41)+~P3(x3241,a41)+P3(x3241,f30(f43(x3241)))), % 59.58/59.60 inference(equality_inference,[],[218])). % 59.58/59.60 cnf(330,plain, % 59.58/59.60 (P7(x3301,x3302)+~P1(x3302)+~P3(x3301,f38(x3302,x3303))+~P3(x3303,a41)), % 59.58/59.60 inference(equality_inference,[],[227])). % 59.58/59.60 cnf(331,plain, % 59.58/59.60 (P3(x3311,f30(x3312))+~P3(x3311,a41)+~P9(f43(x3311),x3312)+~P3(x3312,a41)), % 59.58/59.60 inference(equality_inference,[],[232])). % 59.58/59.60 cnf(332,plain, % 59.58/59.60 (~P2(x3321)+~P3(x3322,x3323)+~P7(x3323,f39(x3321))+E(f31(f33(x3321,x3323),x3322),f31(x3321,x3322))), % 59.58/59.60 inference(equality_inference,[],[245])). % 59.58/59.60 cnf(335,plain, % 59.58/59.60 (~P2(x3351)+~P3(x3352,f34(x3351,x3353))+~P7(x3353,f39(x3351))+P3(f13(x3351,x3353,f34(x3351,x3353),x3352),x3353)), % 59.58/59.60 inference(equality_inference,[],[292])). % 59.58/59.60 cnf(337,plain, % 59.58/59.60 (E(f3(a37),a29)), % 59.58/59.60 inference(scs_inference,[],[301,302])). % 59.58/59.60 cnf(338,plain, % 59.58/59.60 (~P6(a37)), % 59.58/59.60 inference(scs_inference,[],[301,303])). % 59.58/59.60 cnf(339,plain, % 59.58/59.60 (E(a49,f2(a1))), % 59.58/59.60 inference(scs_inference,[],[93,2])). % 59.58/59.60 cnf(340,plain, % 59.58/59.60 (P1(f30(a29))), % 59.58/59.60 inference(scs_inference,[],[93,96,2,141])). % 59.58/59.60 cnf(342,plain, % 59.58/59.60 (~P3(x3421,f30(a29))), % 59.58/59.60 inference(scs_inference,[],[93,96,2,141,149])). % 59.58/59.60 cnf(344,plain, % 59.58/59.60 (P9(a29,a29)), % 59.58/59.60 inference(scs_inference,[],[93,117,96,2,141,149,162])). % 59.58/59.60 cnf(346,plain, % 59.58/59.60 (P1(f30(a44))), % 59.58/59.60 inference(scs_inference,[],[93,117,118,96,2,141,149,162,305])). % 59.58/59.60 cnf(349,plain, % 59.58/59.60 (P3(f2(a1),a48)), % 59.58/59.60 inference(scs_inference,[],[93,120,117,118,139,94,96,2,141,149,162,305,3,81])). % 59.58/59.60 cnf(350,plain, % 59.58/59.60 (~E(a48,a37)), % 59.58/59.60 inference(scs_inference,[],[93,120,304,117,118,139,94,96,2,141,149,162,305,3,81,82])). % 59.58/59.60 cnf(351,plain, % 59.58/59.60 (~P3(x3511,a37)), % 59.58/59.60 inference(rename_variables,[],[304])). % 59.58/59.60 cnf(352,plain, % 59.58/59.60 (P1(f38(a41,a29))), % 59.58/59.60 inference(scs_inference,[],[93,120,304,101,117,118,139,94,96,2,141,149,162,305,3,81,82,311])). % 59.58/59.60 cnf(354,plain, % 59.58/59.60 (P3(a29,f30(f43(a29)))), % 59.58/59.60 inference(scs_inference,[],[93,120,304,101,117,118,139,94,96,2,141,149,162,305,3,81,82,311,324])). % 59.58/59.60 cnf(356,plain, % 59.58/59.60 (~P6(f30(a29))), % 59.58/59.60 inference(scs_inference,[],[93,120,304,101,117,118,139,94,96,2,141,149,162,305,3,81,82,311,324,144])). % 59.58/59.60 cnf(358,plain, % 59.58/59.60 (~P5(a41)), % 59.58/59.60 inference(scs_inference,[],[93,120,304,101,108,117,118,139,94,96,2,141,149,162,305,3,81,82,311,324,144,147])). % 59.58/59.60 cnf(360,plain, % 59.58/59.60 (~P5(f39(a47))), % 59.58/59.60 inference(scs_inference,[],[93,120,304,101,108,117,118,139,94,96,97,2,141,149,162,305,3,81,82,311,324,144,147,87])). % 59.58/59.60 cnf(361,plain, % 59.58/59.60 (P3(a49,a41)), % 59.58/59.60 inference(scs_inference,[],[93,120,304,101,108,117,118,121,124,139,94,96,97,2,141,149,162,305,3,81,82,311,324,144,147,87,202])). % 59.58/59.60 cnf(363,plain, % 59.58/59.60 (P7(a37,a41)), % 59.58/59.60 inference(scs_inference,[],[93,120,304,351,101,301,108,117,118,121,124,139,94,96,97,2,141,149,162,305,3,81,82,311,324,144,147,87,202,207])). % 59.58/59.60 cnf(366,plain, % 59.58/59.60 (~P9(f43(a29),a29)), % 59.58/59.60 inference(scs_inference,[],[93,120,304,351,101,301,108,117,118,121,124,139,94,96,97,2,141,149,162,305,3,81,82,311,324,144,147,87,202,207,331])). % 59.58/59.60 cnf(368,plain, % 59.58/59.60 (~E(a41,f30(a29))), % 59.58/59.60 inference(scs_inference,[],[93,120,304,351,101,301,108,117,118,121,124,139,94,96,97,2,141,149,162,305,3,81,82,311,324,144,147,87,202,207,331,212])). % 59.58/59.60 cnf(370,plain, % 59.58/59.60 (P7(f30(a29),f30(a29))), % 59.58/59.60 inference(scs_inference,[],[93,120,304,351,101,301,108,117,118,121,124,139,94,96,97,2,141,149,162,305,3,81,82,311,324,144,147,87,202,207,331,212,228])). % 59.58/59.60 cnf(372,plain, % 59.58/59.60 (P9(f43(a29),f43(a29))), % 59.58/59.60 inference(scs_inference,[],[93,120,304,351,101,301,108,117,118,121,124,139,94,96,97,2,141,149,162,305,3,81,82,311,324,144,147,87,202,207,331,212,228,229])). % 59.58/59.60 cnf(376,plain, % 59.58/59.60 (P3(f2(a54),a54)+P6(a37)), % 59.58/59.60 inference(scs_inference,[],[93,120,304,351,101,301,108,109,117,118,121,122,124,139,94,96,97,2,141,149,162,305,3,81,82,311,324,144,147,87,202,207,331,212,228,229,309,83])). % 59.58/59.60 cnf(384,plain, % 59.58/59.60 (P3(f2(a54),a54)), % 59.58/59.60 inference(scs_inference,[],[338,376])). % 59.58/59.60 cnf(385,plain, % 59.58/59.60 (P9(a49,a49)), % 59.58/59.60 inference(scs_inference,[],[361,338,376,162])). % 59.58/59.60 cnf(389,plain, % 59.58/59.60 (E(a37,f30(a29))), % 59.58/59.60 inference(scs_inference,[],[361,96,338,376,162,305,2])). % 59.58/59.60 cnf(390,plain, % 59.58/59.60 (P3(a49,f30(f43(a49)))), % 59.58/59.60 inference(scs_inference,[],[361,96,338,376,162,305,2,324])). % 59.58/59.60 cnf(393,plain, % 59.58/59.60 (P1(f38(f30(a29),a49))), % 59.58/59.60 inference(scs_inference,[],[366,361,344,340,96,338,376,162,305,2,324,89,311])). % 59.58/59.60 cnf(395,plain, % 59.58/59.60 (~P5(a48)), % 59.58/59.60 inference(scs_inference,[],[366,361,344,340,104,96,110,338,376,162,305,2,324,89,311,147])). % 59.58/59.60 cnf(398,plain, % 59.58/59.60 (P3(f2(a1),a41)), % 59.58/59.60 inference(scs_inference,[],[339,366,350,361,344,340,104,96,110,338,376,162,305,2,324,89,311,147,3,81])). % 59.58/59.60 cnf(399,plain, % 59.58/59.60 (P7(f30(a29),a37)), % 59.58/59.60 inference(scs_inference,[],[339,366,350,361,344,340,370,104,96,110,338,376,162,305,2,324,89,311,147,3,81,85])). % 59.58/59.60 cnf(400,plain, % 59.58/59.60 (~E(f30(f43(a29)),f30(a29))), % 59.58/59.60 inference(scs_inference,[],[339,366,350,361,344,342,340,370,354,104,96,110,338,376,162,305,2,324,89,311,147,3,81,85,82])). % 59.58/59.60 cnf(401,plain, % 59.58/59.60 (~P3(x4011,f30(a29))), % 59.58/59.60 inference(rename_variables,[],[342])). % 59.58/59.60 cnf(402,plain, % 59.58/59.60 (~E(f43(a29),a29)), % 59.58/59.60 inference(scs_inference,[],[339,366,350,361,344,342,340,370,372,354,104,96,110,338,376,162,305,2,324,89,311,147,3,81,85,82,90])). % 59.58/59.60 cnf(403,plain, % 59.58/59.60 (~P5(f39(a45))), % 59.58/59.60 inference(scs_inference,[],[339,366,350,361,344,342,340,370,372,354,104,96,110,338,358,98,376,162,305,2,324,89,311,147,3,81,85,82,90,87])). % 59.58/59.60 cnf(404,plain, % 59.58/59.60 (P7(f30(a29),a41)), % 59.58/59.60 inference(scs_inference,[],[363,339,366,350,361,344,342,340,370,372,354,104,96,110,338,358,98,376,162,305,2,324,89,311,147,3,81,85,82,90,87,84])). % 59.58/59.60 cnf(407,plain, % 59.58/59.60 (P7(a37,f30(a29))), % 59.58/59.60 inference(scs_inference,[],[363,339,366,350,361,344,342,340,370,372,354,304,104,301,96,110,338,358,98,376,162,305,2,324,89,311,147,3,81,85,82,90,87,84,228,207])). % 59.58/59.60 cnf(408,plain, % 59.58/59.60 (~P3(x4081,a37)), % 59.58/59.60 inference(rename_variables,[],[304])). % 59.58/59.60 cnf(412,plain, % 59.58/59.60 (~P7(a48,f30(a29))), % 59.58/59.60 inference(scs_inference,[],[363,339,349,366,350,361,344,342,401,340,370,372,354,304,104,301,96,110,338,358,98,376,162,305,2,324,89,311,147,3,81,85,82,90,87,84,228,207,229,202])). % 59.58/59.60 cnf(415,plain, % 59.58/59.60 (~P7(a41,f30(a29))), % 59.58/59.60 inference(scs_inference,[],[363,339,349,366,350,361,344,342,401,340,370,372,354,368,304,104,301,101,96,110,338,358,98,376,162,305,2,324,89,311,147,3,81,85,82,90,87,84,228,207,229,202,193])). % 59.58/59.60 cnf(417,plain, % 59.58/59.60 (~P9(f43(a50),a29)), % 59.58/59.60 inference(scs_inference,[],[363,339,349,366,350,361,344,342,401,340,370,372,354,368,304,408,104,301,101,117,96,110,119,338,358,98,376,162,305,2,324,89,311,147,3,81,85,82,90,87,84,228,207,229,202,193,232])). % 59.58/59.60 cnf(424,plain, % 59.58/59.60 (P9(a29,a50)), % 59.58/59.60 inference(scs_inference,[],[363,339,349,366,350,361,344,342,401,340,370,372,354,368,304,408,104,301,101,117,96,110,119,338,358,98,376,162,305,2,324,89,311,147,3,81,85,82,90,87,84,228,207,229,202,193,232,320,330,215])). % 59.58/59.60 cnf(431,plain, % 59.58/59.60 (P1(f30(f2(a1)))), % 59.58/59.60 inference(scs_inference,[],[398,162,305])). % 59.58/59.60 cnf(433,plain, % 59.58/59.60 (E(a29,f3(a37))), % 59.58/59.60 inference(scs_inference,[],[398,337,162,305,2])). % 59.58/59.60 cnf(434,plain, % 59.58/59.60 (P1(f38(f38(f30(a29),a49),a49))), % 59.58/59.60 inference(scs_inference,[],[361,398,393,337,162,305,2,311])). % 59.58/59.60 cnf(436,plain, % 59.58/59.60 (P3(f2(a1),f30(f43(f2(a1))))), % 59.58/59.60 inference(scs_inference,[],[361,398,393,337,162,305,2,311,324])). % 59.58/59.60 cnf(439,plain, % 59.58/59.60 (P3(f2(a1),f30(f43(a49)))), % 59.58/59.60 inference(scs_inference,[],[361,398,339,385,393,390,337,162,305,2,311,324,89,81])). % 59.58/59.60 cnf(442,plain, % 59.58/59.60 (~E(a37,a48)), % 59.58/59.60 inference(scs_inference,[],[361,407,398,412,339,385,393,390,96,402,337,162,305,2,311,324,89,81,85,3,84])). % 59.58/59.60 cnf(444,plain, % 59.58/59.60 (~P3(x4441,f30(a29))), % 59.58/59.60 inference(rename_variables,[],[342])). % 59.58/59.60 cnf(446,plain, % 59.58/59.60 (P5(f30(a29))), % 59.58/59.60 inference(scs_inference,[],[361,384,407,389,398,412,339,385,393,390,342,96,402,337,106,162,305,2,311,324,89,81,85,3,84,82,90,87])). % 59.58/59.60 cnf(447,plain, % 59.58/59.60 (P7(f30(a29),f38(f30(a29),a49))), % 59.58/59.60 inference(scs_inference,[],[361,384,407,389,398,412,339,385,393,390,342,444,340,96,402,337,106,162,305,2,311,324,89,81,85,3,84,82,90,87,207])). % 59.58/59.60 cnf(454,plain, % 59.58/59.60 (P7(f9(f30(a29),a49,f30(a29)),f30(a29))), % 59.58/59.60 inference(scs_inference,[],[361,384,407,389,398,412,339,385,393,390,342,444,340,96,402,337,106,162,305,2,311,324,89,81,85,3,84,82,90,87,207,229,228,267])). % 59.58/59.60 cnf(456,plain, % 59.58/59.60 (~P9(f43(a44),a29)), % 59.58/59.60 inference(scs_inference,[],[361,384,407,389,398,412,339,385,393,390,342,444,304,340,117,96,402,337,106,118,162,305,2,311,324,89,81,85,3,84,82,90,87,207,229,228,267,232])). % 59.58/59.60 cnf(459,plain, % 59.58/59.60 (P7(a37,f38(f30(a29),a49))), % 59.58/59.60 inference(scs_inference,[],[361,384,407,389,398,412,339,385,393,390,342,444,304,301,340,117,96,402,337,106,118,162,305,2,311,324,89,81,85,3,84,82,90,87,207,229,228,267,232,221])). % 59.58/59.60 cnf(463,plain, % 59.58/59.60 (P9(a29,a44)), % 59.58/59.60 inference(scs_inference,[],[361,384,407,389,398,412,339,385,393,390,342,444,304,301,340,117,96,402,337,106,134,118,162,305,2,311,324,89,81,85,3,84,82,90,87,207,229,228,267,232,221,147,215])). % 59.58/59.60 cnf(470,plain, % 59.58/59.60 (P9(a50,a50)), % 59.58/59.60 inference(scs_inference,[],[119,162])). % 59.58/59.60 cnf(475,plain, % 59.58/59.60 (P1(f38(f30(f2(a1)),a49))), % 59.58/59.60 inference(scs_inference,[],[361,431,128,119,162,305,2,311])). % 59.58/59.60 cnf(478,plain, % 59.58/59.60 (P3(a50,f30(f43(a50)))), % 59.58/59.60 inference(scs_inference,[],[361,433,424,431,128,119,162,305,2,311,89,324])). % 59.58/59.60 cnf(480,plain, % 59.58/59.60 (P3(a49,f30(f43(f2(a1))))), % 59.58/59.60 inference(scs_inference,[],[93,361,433,424,431,436,128,119,162,305,2,311,89,324,81])). % 59.58/59.60 cnf(481,plain, % 59.58/59.60 (P7(f9(f30(a29),a49,f30(a29)),a37)), % 59.58/59.60 inference(scs_inference,[],[93,361,433,424,431,436,96,454,128,119,162,305,2,311,89,324,81,85])). % 59.58/59.60 cnf(482,plain, % 59.58/59.60 (~E(a37,a41)), % 59.58/59.60 inference(scs_inference,[],[93,361,407,415,433,424,431,436,96,454,128,119,162,305,2,311,89,324,81,85,84])). % 59.58/59.60 cnf(483,plain, % 59.58/59.60 (~E(f30(f43(a29)),a37)), % 59.58/59.60 inference(scs_inference,[],[93,361,389,400,407,415,433,424,431,436,96,454,128,119,162,305,2,311,89,324,81,85,84,3])). % 59.58/59.60 cnf(485,plain, % 59.58/59.60 (~P3(x4851,f30(a29))), % 59.58/59.60 inference(rename_variables,[],[342])). % 59.58/59.60 cnf(486,plain, % 59.58/59.60 (P9(a29,f3(a37))), % 59.58/59.60 inference(scs_inference,[],[93,361,389,400,407,415,439,433,424,431,436,344,342,96,454,128,119,162,305,2,311,89,324,81,85,84,3,82,90])). % 59.58/59.60 cnf(487,plain, % 59.58/59.60 (~P5(f39(a51))), % 59.58/59.60 inference(scs_inference,[],[93,361,389,400,407,415,439,433,424,431,436,344,342,96,454,128,99,358,119,162,305,2,311,89,324,81,85,84,3,82,90,87])). % 59.58/59.60 cnf(488,plain, % 59.58/59.60 (P9(f43(a50),f43(a50))), % 59.58/59.60 inference(scs_inference,[],[93,361,389,400,407,415,439,433,424,431,436,344,342,96,454,128,99,358,119,162,305,2,311,89,324,81,85,84,3,82,90,87,229])). % 59.58/59.60 cnf(495,plain, % 59.58/59.60 (P7(f26(a37,a29),a37)), % 59.58/59.60 inference(scs_inference,[],[93,361,389,400,407,415,439,433,424,431,436,344,342,485,301,340,117,96,454,128,99,106,358,119,162,305,2,311,89,324,81,85,84,3,82,90,87,229,207,228,241])). % 59.58/59.60 cnf(497,plain, % 59.58/59.60 (P7(f9(f30(a29),a49,a37),f30(a29))), % 59.58/59.60 inference(scs_inference,[],[93,361,389,400,407,415,439,433,424,431,436,344,342,485,301,340,117,96,454,459,128,99,106,358,119,162,305,2,311,89,324,81,85,84,3,82,90,87,229,207,228,241,267])). % 59.58/59.60 cnf(507,plain, % 59.58/59.60 (P9(a44,a44)), % 59.58/59.60 inference(scs_inference,[],[118,162])). % 59.58/59.60 cnf(509,plain, % 59.58/59.60 (E(a50,f3(a46))), % 59.58/59.60 inference(scs_inference,[],[118,95,162,2])). % 59.58/59.60 cnf(510,plain, % 59.58/59.60 (P1(f38(f38(f38(f30(a29),a49),a49),a49))), % 59.58/59.60 inference(scs_inference,[],[361,434,118,95,162,2,311])). % 59.58/59.60 cnf(512,plain, % 59.58/59.60 (P3(a44,f30(f43(a44)))), % 59.58/59.60 inference(scs_inference,[],[361,434,118,95,162,2,311,324])). % 59.58/59.60 cnf(514,plain, % 59.58/59.60 (P3(f3(a46),f30(f43(a50)))), % 59.58/59.60 inference(scs_inference,[],[361,434,478,118,95,162,2,311,324,81])). % 59.58/59.60 cnf(518,plain, % 59.58/59.60 (~P3(x5181,f30(a29))), % 59.58/59.60 inference(rename_variables,[],[342])). % 59.58/59.60 cnf(519,plain, % 59.58/59.60 (P7(f9(f30(a29),a49,a37),a37)), % 59.58/59.60 inference(scs_inference,[],[361,480,470,434,478,342,96,118,497,482,95,100,162,2,311,324,81,89,3,82,85])). % 59.58/59.60 cnf(520,plain, % 59.58/59.60 (~E(f30(a29),a41)), % 59.58/59.60 inference(scs_inference,[],[361,480,415,370,470,434,478,342,96,118,497,482,95,100,162,2,311,324,81,89,3,82,85,84])). % 59.58/59.60 cnf(521,plain, % 59.58/59.60 (P9(a50,f3(a46))), % 59.58/59.60 inference(scs_inference,[],[361,480,415,370,470,434,478,342,96,118,497,482,95,100,162,2,311,324,81,89,3,82,85,84,90])). % 59.58/59.60 cnf(523,plain, % 59.58/59.60 (P7(f30(a29),f38(f38(f30(a29),a49),a49))), % 59.58/59.60 inference(scs_inference,[],[361,480,415,370,470,434,478,342,518,340,96,118,497,482,95,100,358,162,2,311,324,81,89,3,82,85,84,90,87,207])). % 59.58/59.60 cnf(526,plain, % 59.58/59.60 (P9(f43(a44),f43(a44))), % 59.58/59.60 inference(scs_inference,[],[361,480,415,370,470,434,478,342,518,340,96,118,497,482,95,100,358,162,2,311,324,81,89,3,82,85,84,90,87,207,229])). % 59.58/59.60 cnf(532,plain, % 59.58/59.60 (P7(a37,f38(f38(f30(a29),a49),a49))), % 59.58/59.60 inference(scs_inference,[],[361,407,480,415,370,470,434,478,342,518,393,301,340,96,118,497,446,482,95,100,358,162,2,311,324,81,89,3,82,85,84,90,87,207,229,228,267,221])). % 59.58/59.60 cnf(541,plain, % 59.58/59.60 (E(a46,f35(a1,f2(a1)))), % 59.58/59.60 inference(scs_inference,[],[129,2])). % 59.58/59.60 cnf(547,plain, % 59.58/59.60 (P3(f3(a37),f30(f43(a29)))), % 59.58/59.60 inference(scs_inference,[],[361,433,463,475,105,354,442,129,135,2,311,89,80,3,81])). % 59.58/59.60 cnf(549,plain, % 59.58/59.60 (~E(a41,a37)), % 59.58/59.60 inference(scs_inference,[],[361,412,433,370,463,475,105,354,304,442,129,135,2,311,89,80,3,81,84,82])). % 59.58/59.60 cnf(550,plain, % 59.58/59.60 (~P3(x5501,a37)), % 59.58/59.60 inference(rename_variables,[],[304])). % 59.58/59.60 cnf(551,plain, % 59.58/59.60 (P7(f26(a37,a29),f30(a29))), % 59.58/59.60 inference(scs_inference,[],[361,389,412,433,370,463,475,105,354,304,495,442,129,135,2,311,89,80,3,81,84,82,85])). % 59.58/59.60 cnf(553,plain, % 59.58/59.60 (~P5(f34(a51,f32(a52,f40(a52))))), % 59.58/59.60 inference(scs_inference,[],[361,389,417,412,433,370,463,488,475,105,354,304,495,395,442,129,135,2,311,89,80,3,81,84,82,85,90,87])). % 59.58/59.60 cnf(557,plain, % 59.58/59.60 (~P7(a41,a37)), % 59.58/59.60 inference(scs_inference,[],[361,389,417,363,412,433,370,463,488,475,105,354,304,550,101,301,495,395,442,129,135,2,311,89,80,3,81,84,82,85,90,87,207,193])). % 59.58/59.60 cnf(561,plain, % 59.58/59.60 (P7(f30(a29),f38(f30(f2(a1)),a49))), % 59.58/59.60 inference(scs_inference,[],[361,389,417,363,412,433,370,463,488,475,105,354,304,550,393,101,301,340,399,495,532,395,442,129,135,106,2,311,89,80,3,81,84,82,85,90,87,207,193,267,221])). % 59.58/59.60 cnf(569,plain, % 59.58/59.60 (E(a44,f43(a50))), % 59.58/59.60 inference(scs_inference,[],[94,2])). % 59.58/59.60 cnf(570,plain, % 59.58/59.60 (P1(f38(f38(f38(f38(f30(a29),a49),a49),a49),f2(a1)))), % 59.58/59.60 inference(scs_inference,[],[398,510,94,2,311])). % 59.58/59.60 cnf(572,plain, % 59.58/59.60 (P9(f43(a50),a44)), % 59.58/59.60 inference(scs_inference,[],[398,507,510,94,2,311,89])). % 59.58/59.60 cnf(573,plain, % 59.58/59.60 (P3(f43(a50),f30(f43(a44)))), % 59.58/59.60 inference(scs_inference,[],[398,507,512,510,94,2,311,89,81])). % 59.58/59.60 cnf(574,plain, % 59.58/59.60 (~E(f26(a37,a29),a41)), % 59.58/59.60 inference(scs_inference,[],[398,415,507,512,510,551,94,2,311,89,81,84])). % 59.58/59.60 cnf(577,plain, % 59.58/59.60 (~P3(x5771,f30(a29))), % 59.58/59.60 inference(rename_variables,[],[342])). % 59.58/59.60 cnf(579,plain, % 59.58/59.60 (P7(f30(a29),f38(f38(f38(f30(a29),a49),a49),a49))), % 59.58/59.60 inference(scs_inference,[],[398,514,415,342,577,507,512,510,340,551,520,94,97,2,311,89,81,84,3,82,90,207])). % 59.58/59.60 cnf(591,plain, % 59.58/59.60 (E(a41,f39(a45))), % 59.58/59.60 inference(scs_inference,[],[98,2])). % 59.58/59.60 cnf(595,plain, % 59.58/59.60 (P3(f3(a37),a41)), % 59.58/59.60 inference(scs_inference,[],[398,433,570,101,117,98,2,311,80,81])). % 59.58/59.60 cnf(597,plain, % 59.58/59.60 (P9(f3(a37),f3(a37))), % 59.58/59.60 inference(scs_inference,[],[398,433,570,101,117,108,486,98,2,311,80,81,83,89])). % 59.58/59.60 cnf(598,plain, % 59.58/59.60 (P7(a37,f39(a45))), % 59.58/59.60 inference(scs_inference,[],[398,363,433,570,101,117,108,486,98,2,311,80,81,83,89,85])). % 59.58/59.60 cnf(600,plain, % 59.58/59.60 (~E(f9(f30(a29),a49,f30(a29)),a41)), % 59.58/59.60 inference(scs_inference,[],[398,363,557,433,570,101,117,108,486,481,98,574,2,311,80,81,83,89,85,3,84])). % 59.58/59.60 cnf(602,plain, % 59.58/59.60 (~P3(x6021,f30(a29))), % 59.58/59.60 inference(rename_variables,[],[342])). % 59.58/59.60 cnf(604,plain, % 59.58/59.60 (~P3(x6041,f34(a45,a37))), % 59.58/59.60 inference(scs_inference,[],[398,456,363,557,573,433,342,526,570,304,101,117,108,486,481,98,574,113,2,311,80,81,83,89,85,3,84,82,90,335])). % 59.58/59.60 cnf(605,plain, % 59.58/59.60 (~P3(x6051,a37)), % 59.58/59.60 inference(rename_variables,[],[304])). % 59.58/59.60 cnf(614,plain, % 59.58/59.60 (~E(a41,f34(a45,a37))), % 59.58/59.60 inference(scs_inference,[],[361,398,456,363,557,573,433,342,602,526,570,304,605,101,340,117,108,486,481,98,574,113,2,311,80,81,83,89,85,3,84,82,90,335,229,228,207,292])). % 59.58/59.60 cnf(615,plain, % 59.58/59.60 (~P3(x6151,a37)), % 59.58/59.60 inference(rename_variables,[],[304])). % 59.58/59.60 cnf(617,plain, % 59.58/59.60 (P7(f26(a37,f3(a37)),a37)), % 59.58/59.60 inference(scs_inference,[],[361,398,456,363,557,573,433,342,602,526,570,304,605,101,301,340,117,108,486,481,98,574,113,106,2,311,80,81,83,89,85,3,84,82,90,335,229,228,207,292,241])). % 59.58/59.60 cnf(621,plain, % 59.58/59.60 (P3(f12(a45,a37,a41),a41)), % 59.58/59.60 inference(scs_inference,[],[361,398,456,363,557,573,579,433,342,602,526,570,434,304,605,615,101,301,340,117,108,486,481,98,574,113,446,106,2,311,80,81,83,89,85,3,84,82,90,335,229,228,207,292,241,267,282])). % 59.58/59.60 cnf(622,plain, % 59.58/59.60 (~P3(x6221,a37)), % 59.58/59.60 inference(rename_variables,[],[304])). % 59.58/59.60 cnf(628,plain, % 59.58/59.60 (P9(f12(a45,a37,a41),f12(a45,a37,a41))), % 59.58/59.60 inference(scs_inference,[],[361,398,407,456,363,557,573,579,433,342,602,526,570,434,304,605,615,101,301,340,117,108,486,481,98,574,113,446,106,2,311,80,81,83,89,85,3,84,82,90,335,229,228,207,292,241,267,282,221,305,162])). % 59.58/59.60 cnf(630,plain, % 59.58/59.60 (P1(f34(a45,a37))), % 59.58/59.60 inference(scs_inference,[],[361,398,407,456,363,557,573,579,433,342,602,526,570,434,304,605,615,101,301,340,117,108,486,481,98,574,113,446,106,2,311,80,81,83,89,85,3,84,82,90,335,229,228,207,292,241,267,282,221,305,162,317])). % 59.58/59.60 cnf(632,plain, % 59.58/59.60 (P2(f33(a45,a37))), % 59.58/59.60 inference(scs_inference,[],[361,398,407,456,363,557,573,579,433,342,602,526,570,434,304,605,615,101,301,340,117,108,486,481,98,574,113,446,106,2,311,80,81,83,89,85,3,84,82,90,335,229,228,207,292,241,267,282,221,305,162,317,318])). % 59.58/59.60 cnf(634,plain, % 59.58/59.60 (E(f39(f33(a45,a37)),a37)), % 59.58/59.60 inference(scs_inference,[],[361,398,407,456,363,557,573,579,433,342,602,526,570,434,304,605,615,101,301,340,117,108,486,481,98,574,113,446,106,2,311,80,81,83,89,85,3,84,82,90,335,229,228,207,292,241,267,282,221,305,162,317,318,319])). % 59.58/59.60 cnf(636,plain, % 59.58/59.60 (E(f34(a45,a37),a37)), % 59.58/59.60 inference(scs_inference,[],[361,398,407,456,363,557,573,579,433,342,602,526,570,434,304,605,615,101,301,340,117,108,486,481,98,574,113,446,106,2,311,80,81,83,89,85,3,84,82,90,335,229,228,207,292,241,267,282,221,305,162,317,318,319,152])). % 59.58/59.60 cnf(640,plain, % 59.58/59.60 (P3(f3(a37),f30(f43(f3(a37))))), % 59.58/59.60 inference(scs_inference,[],[361,398,407,456,363,557,573,579,433,342,602,526,570,434,304,605,615,101,301,340,117,108,486,481,98,574,113,446,106,2,311,80,81,83,89,85,3,84,82,90,335,229,228,207,292,241,267,282,221,305,162,317,318,319,152,144,324])). % 59.58/59.60 cnf(642,plain, % 59.58/59.60 (~P9(f43(f12(a45,a37,a41)),a29)), % 59.58/59.60 inference(scs_inference,[],[361,398,389,407,456,363,557,573,579,433,342,602,526,570,434,304,605,615,622,101,301,340,117,108,486,481,98,574,113,446,106,2,311,80,81,83,89,85,3,84,82,90,335,229,228,207,292,241,267,282,221,305,162,317,318,319,152,144,324,232])). % 59.58/59.60 cnf(645,plain, % 59.58/59.60 (P1(f39(f33(a45,a37)))), % 59.58/59.60 inference(scs_inference,[],[361,398,389,407,456,363,557,573,579,433,342,602,526,570,434,304,605,615,622,101,301,340,117,108,486,481,98,574,113,446,106,2,311,80,81,83,89,85,3,84,82,90,335,229,228,207,292,241,267,282,221,305,162,317,318,319,152,144,324,232,141])). % 59.58/59.60 cnf(647,plain, % 59.58/59.60 (~P3(x6471,f39(f33(a45,a37)))), % 59.58/59.60 inference(scs_inference,[],[361,398,389,407,456,363,557,573,579,433,342,602,526,570,434,304,605,615,622,101,301,340,117,108,486,481,98,574,113,446,106,2,311,80,81,83,89,85,3,84,82,90,335,229,228,207,292,241,267,282,221,305,162,317,318,319,152,144,324,232,141,149])). % 59.58/59.60 cnf(656,plain, % 59.58/59.60 (P1(f30(f12(a45,a37,a41)))), % 59.58/59.60 inference(scs_inference,[],[621,305])). % 59.58/59.60 cnf(658,plain, % 59.58/59.60 (E(a37,f34(a45,a37))), % 59.58/59.60 inference(scs_inference,[],[636,621,305,2])). % 59.58/59.60 cnf(659,plain, % 59.58/59.60 (~P6(f34(a45,a37))), % 59.58/59.60 inference(scs_inference,[],[636,621,630,305,2,144])). % 59.58/59.60 cnf(663,plain, % 59.58/59.60 (P3(f12(a45,a37,a41),f30(f43(f12(a45,a37,a41))))), % 59.58/59.60 inference(scs_inference,[],[361,636,621,630,305,2,144,311,324])). % 59.58/59.60 cnf(665,plain, % 59.58/59.60 (P3(a29,f30(f43(f3(a37))))), % 59.58/59.60 inference(scs_inference,[],[361,636,621,630,640,337,305,2,144,311,324,81])). % 59.58/59.60 cnf(666,plain, % 59.58/59.60 (P9(f3(a46),f3(a46))), % 59.58/59.60 inference(scs_inference,[],[361,509,636,621,630,640,521,337,305,2,144,311,324,81,89])). % 59.58/59.60 cnf(667,plain, % 59.58/59.60 (P7(f30(a29),f39(a45))), % 59.58/59.60 inference(scs_inference,[],[361,509,636,591,621,630,640,404,521,337,305,2,144,311,324,81,89,85])). % 59.58/59.60 cnf(669,plain, % 59.58/59.60 (~E(f30(f43(a29)),f34(a45,a37))), % 59.58/59.60 inference(scs_inference,[],[361,547,604,509,636,591,621,630,640,404,634,521,337,338,305,2,144,311,324,81,89,85,83,82])). % 59.58/59.60 cnf(670,plain, % 59.58/59.60 (~P3(x6701,f34(a45,a37))), % 59.58/59.60 inference(rename_variables,[],[604])). % 59.58/59.60 cnf(673,plain, % 59.58/59.60 (P9(a29,f3(a46))), % 59.58/59.60 inference(scs_inference,[],[361,547,604,509,636,591,621,557,630,640,424,404,99,519,600,634,521,337,338,305,2,144,311,324,81,89,85,83,82,3,84,90])). % 59.58/59.60 cnf(674,plain, % 59.58/59.60 (P5(f34(a45,a37))), % 59.58/59.60 inference(scs_inference,[],[361,547,604,509,636,591,621,557,630,640,424,404,99,519,600,634,521,337,338,106,305,2,144,311,324,81,89,85,83,82,3,84,90,87])). % 59.58/59.60 cnf(679,plain, % 59.58/59.60 (~P3(x6791,f34(a45,f30(a29)))), % 59.58/59.60 inference(scs_inference,[],[361,547,604,509,636,591,621,557,342,630,640,424,404,99,519,553,600,634,521,337,338,106,113,305,2,144,311,324,81,89,85,83,82,3,84,90,87,172,330,335])). % 59.58/59.60 cnf(680,plain, % 59.58/59.60 (~P3(x6801,f30(a29))), % 59.58/59.60 inference(rename_variables,[],[342])). % 59.58/59.60 cnf(682,plain, % 59.58/59.60 (P9(a29,f12(a45,a37,a41))), % 59.58/59.60 inference(scs_inference,[],[361,547,604,509,642,636,591,621,557,342,630,640,424,117,404,99,519,553,600,634,521,337,338,106,113,305,2,144,311,324,81,89,85,83,82,3,84,90,87,172,330,335,215])). % 59.58/59.60 cnf(684,plain, % 59.58/59.60 (~P7(a41,f34(a45,a37))), % 59.58/59.60 inference(scs_inference,[],[361,547,604,670,509,642,636,591,621,557,342,630,640,424,117,404,99,519,553,600,634,521,337,338,106,113,305,2,144,311,324,81,89,85,83,82,3,84,90,87,172,330,335,215,202])). % 59.58/59.60 cnf(685,plain, % 59.58/59.60 (~P3(x6851,f34(a45,a37))), % 59.58/59.60 inference(rename_variables,[],[604])). % 59.58/59.60 cnf(687,plain, % 59.58/59.60 (P9(f43(f12(a45,a37,a41)),f43(f12(a45,a37,a41)))), % 59.58/59.60 inference(scs_inference,[],[361,547,604,670,509,642,636,591,621,557,342,628,630,640,424,117,404,99,519,553,600,634,521,337,338,106,113,305,2,144,311,324,81,89,85,83,82,3,84,90,87,172,330,335,215,202,229])). % 59.58/59.60 cnf(691,plain, % 59.58/59.60 (P7(f34(a45,a37),f34(a45,a37))), % 59.58/59.60 inference(scs_inference,[],[361,547,604,670,685,509,642,636,591,621,557,342,628,630,640,424,117,404,99,519,553,600,634,521,337,338,106,113,305,2,144,311,324,81,89,85,83,82,3,84,90,87,172,330,335,215,202,229,228,207])). % 59.58/59.60 cnf(694,plain, % 59.58/59.60 (~E(a41,f34(a45,f30(a29)))), % 59.58/59.60 inference(scs_inference,[],[361,547,604,670,685,509,642,636,591,621,557,342,680,628,630,640,424,117,404,99,519,553,600,634,521,337,338,106,113,305,2,144,311,324,81,89,85,83,82,3,84,90,87,172,330,335,215,202,229,228,207,292])). % 59.58/59.60 cnf(695,plain, % 59.58/59.60 (~P3(x6951,f30(a29))), % 59.58/59.60 inference(rename_variables,[],[342])). % 59.58/59.60 cnf(699,plain, % 59.58/59.60 (P3(f12(a45,f30(a29),a41),a41)), % 59.58/59.60 inference(scs_inference,[],[361,547,604,670,685,509,642,636,591,621,557,342,680,695,628,630,640,424,431,101,117,404,99,519,561,553,600,634,521,337,446,338,106,113,305,2,144,311,324,81,89,85,83,82,3,84,90,87,172,330,335,215,202,229,228,207,292,267,282])). % 59.58/59.60 cnf(702,plain, % 59.58/59.60 (P9(f12(a45,f30(a29),a41),f12(a45,f30(a29),a41))), % 59.58/59.60 inference(scs_inference,[],[361,547,604,670,685,509,642,636,591,621,557,342,680,695,628,630,640,424,431,101,117,404,99,519,561,553,600,634,521,337,446,338,106,113,305,2,144,311,324,81,89,85,83,82,3,84,90,87,172,330,335,215,202,229,228,207,292,267,282,162])). % 59.58/59.60 cnf(704,plain, % 59.58/59.60 (P2(f33(a45,f30(a29)))), % 59.58/59.60 inference(scs_inference,[],[361,547,604,670,685,509,642,636,591,621,557,342,680,695,628,630,640,424,431,101,117,404,99,519,561,553,600,634,521,337,446,338,106,113,305,2,144,311,324,81,89,85,83,82,3,84,90,87,172,330,335,215,202,229,228,207,292,267,282,162,318])). % 59.58/59.60 cnf(708,plain, % 59.58/59.60 (P1(f34(a45,f30(a29)))), % 59.58/59.60 inference(scs_inference,[],[361,547,604,670,685,509,642,636,591,621,557,342,680,695,628,630,640,424,431,101,117,404,99,519,561,553,600,634,521,337,446,338,106,113,305,2,144,311,324,81,89,85,83,82,3,84,90,87,172,330,335,215,202,229,228,207,292,267,282,162,318,152,317])). % 59.58/59.60 cnf(710,plain, % 59.58/59.60 (E(f39(f33(a45,f30(a29))),f30(a29))), % 59.58/59.60 inference(scs_inference,[],[361,547,604,670,685,509,642,636,591,621,557,342,680,695,628,630,640,424,431,101,117,404,99,519,561,553,600,634,521,337,446,338,106,113,305,2,144,311,324,81,89,85,83,82,3,84,90,87,172,330,335,215,202,229,228,207,292,267,282,162,318,152,317,319])). % 59.58/59.60 cnf(712,plain, % 59.58/59.60 (~P9(f43(f12(a45,f30(a29),a41)),a29)), % 59.58/59.60 inference(scs_inference,[],[361,389,547,604,670,685,509,642,636,591,621,557,342,680,695,628,630,640,424,431,304,101,117,404,99,519,561,553,600,634,521,337,446,338,106,113,305,2,144,311,324,81,89,85,83,82,3,84,90,87,172,330,335,215,202,229,228,207,292,267,282,162,318,152,317,319,232])). % 59.58/59.60 cnf(715,plain, % 59.58/59.60 (P1(f39(f33(a45,f30(a29))))), % 59.58/59.60 inference(scs_inference,[],[361,389,547,604,670,685,509,642,636,591,621,557,342,680,695,628,630,640,424,431,304,101,117,404,99,519,561,553,600,634,521,337,446,338,106,113,305,2,144,311,324,81,89,85,83,82,3,84,90,87,172,330,335,215,202,229,228,207,292,267,282,162,318,152,317,319,232,158])). % 59.58/59.60 cnf(724,plain, % 59.58/59.60 (P1(f30(f12(a45,f30(a29),a41)))), % 59.58/59.60 inference(scs_inference,[],[699,305])). % 59.58/59.60 cnf(727,plain, % 59.58/59.60 (E(f34(a45,f30(a29)),a37)), % 59.58/59.60 inference(scs_inference,[],[679,699,708,634,305,2,152])). % 59.58/59.60 cnf(728,plain, % 59.58/59.60 (~P3(x7281,f34(a45,f30(a29)))), % 59.58/59.60 inference(rename_variables,[],[679])). % 59.58/59.60 cnf(730,plain, % 59.58/59.60 (~P6(f34(a45,f30(a29)))), % 59.58/59.60 inference(scs_inference,[],[679,699,708,634,305,2,152,144])). % 59.58/59.60 cnf(734,plain, % 59.58/59.60 (P3(f12(a45,f30(a29),a41),f30(f43(f12(a45,f30(a29),a41))))), % 59.58/59.60 inference(scs_inference,[],[361,679,699,656,708,634,305,2,152,144,311,324])). % 59.58/59.60 cnf(736,plain, % 59.58/59.60 (P3(f3(a46),a41)), % 59.58/59.60 inference(scs_inference,[],[361,679,699,509,656,708,119,634,305,2,152,144,311,324,81])). % 59.58/59.60 cnf(740,plain, % 59.58/59.60 (~P3(x7401,f34(a45,f30(a29)))), % 59.58/59.60 inference(rename_variables,[],[679])). % 59.58/59.60 cnf(743,plain, % 59.58/59.60 (~E(f34(a45,a37),a41)), % 59.58/59.60 inference(scs_inference,[],[361,636,547,691,483,679,728,684,699,509,433,656,708,682,119,634,710,356,305,2,152,144,311,324,81,89,85,82,83,3,84])). % 59.58/59.60 cnf(745,plain, % 59.58/59.60 (P5(f39(f33(a45,a37)))), % 59.58/59.60 inference(scs_inference,[],[361,636,547,691,483,679,728,684,699,642,509,433,656,687,708,682,119,634,710,356,106,305,2,152,144,311,324,81,89,85,82,83,3,84,90,87])). % 59.58/59.60 cnf(746,plain, % 59.58/59.60 (P9(a29,f12(a45,f30(a29),a41))), % 59.58/59.60 inference(scs_inference,[],[361,636,547,691,483,679,728,684,712,699,642,509,433,656,687,708,682,117,119,634,710,356,106,305,2,152,144,311,324,81,89,85,82,83,3,84,90,87,215])). % 59.58/59.60 cnf(748,plain, % 59.58/59.60 (P9(f43(f12(a45,f30(a29),a41)),f43(f12(a45,f30(a29),a41)))), % 59.58/59.60 inference(scs_inference,[],[361,636,547,691,483,679,728,684,712,699,642,509,433,656,687,708,702,682,117,119,634,710,356,106,305,2,152,144,311,324,81,89,85,82,83,3,84,90,87,215,229])). % 59.58/59.60 cnf(752,plain, % 59.58/59.60 (P7(f34(a45,f30(a29)),f30(f12(a45,a37,a41)))), % 59.58/59.60 inference(scs_inference,[],[361,636,547,691,483,679,728,740,684,712,699,642,509,433,656,687,708,702,682,117,119,634,710,356,106,305,2,152,144,311,324,81,89,85,82,83,3,84,90,87,215,229,228,207])). % 59.58/59.60 cnf(755,plain, % 59.58/59.60 (~P9(f43(f3(a46)),a29)), % 59.58/59.60 inference(scs_inference,[],[361,389,636,547,691,483,679,728,740,684,712,699,642,509,433,656,687,708,702,682,304,117,119,634,710,356,106,305,2,152,144,311,324,81,89,85,82,83,3,84,90,87,215,229,228,207,232])). % 59.58/59.60 cnf(758,plain, % 59.58/59.60 (P5(a46)), % 59.58/59.60 inference(scs_inference,[],[361,389,636,547,691,483,679,728,740,684,712,699,642,509,433,656,687,708,702,682,105,304,117,119,634,710,356,106,305,2,152,144,311,324,81,89,85,82,83,3,84,90,87,215,229,228,207,232,171])). % 59.58/59.60 cnf(769,plain, % 59.58/59.60 (E(a37,f34(a45,f30(a29)))), % 59.58/59.60 inference(scs_inference,[],[727,736,305,2])). % 59.58/59.60 cnf(772,plain, % 59.58/59.60 (P3(f3(a46),f30(f43(f3(a46))))), % 59.58/59.60 inference(scs_inference,[],[361,727,736,724,305,2,311,324])). % 59.58/59.60 cnf(774,plain, % 59.58/59.60 (P3(f43(a50),a41)), % 59.58/59.60 inference(scs_inference,[],[361,727,569,736,724,118,305,2,311,324,81])). % 59.58/59.60 cnf(777,plain, % 59.58/59.60 (~P3(x7771,f34(a45,f30(a29)))), % 59.58/59.60 inference(rename_variables,[],[679])). % 59.58/59.60 cnf(778,plain, % 59.58/59.60 (P7(a54,f39(a45))), % 59.58/59.60 inference(scs_inference,[],[361,591,727,665,569,736,679,433,724,746,118,122,305,2,311,324,81,89,82,85])). % 59.58/59.60 cnf(783,plain, % 59.58/59.60 (E(f31(f33(a45,a54),f2(a54)),f31(a45,f2(a54)))), % 59.58/59.60 inference(scs_inference,[],[361,541,591,752,727,665,569,736,549,679,712,384,433,724,748,746,118,634,122,758,113,305,2,311,324,81,89,82,85,3,84,87,90,332])). % 59.58/59.60 cnf(785,plain, % 59.58/59.60 (P9(f43(f3(a46)),f43(f3(a46)))), % 59.58/59.61 inference(scs_inference,[],[361,541,591,752,727,665,569,736,549,679,712,384,433,724,748,746,118,634,122,758,666,113,305,2,311,324,81,89,82,85,3,84,87,90,332,229])). % 59.58/59.61 cnf(789,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f30(f12(a45,f30(a29),a41)))), % 59.58/59.61 inference(scs_inference,[],[361,541,591,752,727,665,569,736,549,679,777,712,384,433,724,748,746,708,118,634,122,758,666,113,305,2,311,324,81,89,82,85,3,84,87,90,332,229,228,207])). % 59.58/59.61 cnf(792,plain, % 59.58/59.61 (P7(f26(a46,a29),a46)), % 59.58/59.61 inference(scs_inference,[],[361,541,591,752,727,665,569,736,549,679,777,712,384,433,724,748,746,708,105,117,118,634,122,673,758,666,113,305,2,311,324,81,89,82,85,3,84,87,90,332,229,228,207,241])). % 59.58/59.61 cnf(808,plain, % 59.58/59.61 (P1(f30(f43(a50)))), % 59.58/59.61 inference(scs_inference,[],[774,305])). % 59.58/59.61 cnf(810,plain, % 59.58/59.61 (E(f31(a45,f2(a54)),f31(f33(a45,a54),f2(a54)))), % 59.58/59.61 inference(scs_inference,[],[774,783,305,2])). % 59.58/59.61 cnf(813,plain, % 59.58/59.61 (P3(f43(a50),f30(f43(f43(a50))))), % 59.58/59.61 inference(scs_inference,[],[361,774,715,783,305,2,311,324])). % 59.58/59.61 cnf(815,plain, % 59.58/59.61 (P9(f43(f3(a46)),f43(a50))), % 59.58/59.61 inference(scs_inference,[],[361,774,514,715,783,305,2,311,324,320])). % 59.58/59.61 cnf(817,plain, % 59.58/59.61 (P3(a50,f30(f43(f3(a46))))), % 59.58/59.61 inference(scs_inference,[],[361,774,514,715,783,772,95,305,2,311,324,320,81])). % 59.58/59.61 cnf(818,plain, % 59.58/59.61 (P9(f3(a37),f3(a46))), % 59.58/59.61 inference(scs_inference,[],[361,774,514,433,715,783,772,95,673,305,2,311,324,320,81,89])). % 59.58/59.61 cnf(819,plain, % 59.58/59.61 (~E(a48,f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[361,604,774,349,514,433,715,783,772,95,673,305,2,311,324,320,81,89,82])). % 59.58/59.61 cnf(820,plain, % 59.58/59.61 (~P3(x8201,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(821,plain, % 59.58/59.61 (P7(a1,f39(a45))), % 59.58/59.61 inference(scs_inference,[],[361,591,604,774,349,514,433,715,783,772,124,95,673,305,2,311,324,320,81,89,82,85])). % 59.58/59.61 cnf(824,plain, % 59.58/59.61 (P5(f34(a45,f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[361,727,591,604,789,769,774,349,514,433,715,783,772,98,124,743,95,673,106,305,2,311,324,320,81,89,82,85,3,84,87])). % 59.58/59.61 cnf(826,plain, % 59.58/59.61 (E(f31(f33(a45,a1),a49),f31(a45,a49))), % 59.58/59.61 inference(scs_inference,[],[361,727,591,755,604,789,769,774,349,514,433,715,785,783,772,98,124,743,95,673,121,106,113,305,2,311,324,320,81,89,82,85,3,84,87,90,332])). % 59.58/59.61 cnf(832,plain, % 59.58/59.61 (P7(f34(a45,a37),f39(f33(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,727,591,755,604,820,789,769,774,349,514,433,715,785,783,772,488,630,98,124,743,95,673,121,106,113,305,2,311,324,320,81,89,82,85,3,84,87,90,332,228,229,207])). % 59.58/59.61 cnf(833,plain, % 59.58/59.61 (~P3(x8331,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(835,plain, % 59.58/59.61 (P7(f26(a46,a50),a46)), % 59.58/59.61 inference(scs_inference,[],[361,727,591,755,604,820,789,769,774,349,514,433,715,785,783,772,488,105,630,119,98,124,743,95,673,521,121,758,106,113,305,2,311,324,320,81,89,82,85,3,84,87,90,332,228,229,207,241])). % 59.58/59.61 cnf(838,plain, % 59.58/59.61 (~P3(x8381,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(841,plain, % 59.58/59.61 (~P3(x8411,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(844,plain, % 59.58/59.61 (~P3(x8441,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(846,plain, % 59.58/59.61 (P3(f12(f33(a45,f30(a29)),f34(a45,a37),a41),a41)), % 59.58/59.61 inference(scs_inference,[],[361,727,591,755,604,820,833,838,841,844,789,769,774,349,514,384,433,715,785,783,772,488,105,630,101,119,98,124,704,743,778,95,673,521,121,758,106,113,305,2,311,324,320,81,89,82,85,3,84,87,90,332,228,229,207,241,292,232,255,282])). % 59.58/59.61 cnf(850,plain, % 59.58/59.61 (P9(f12(f33(a45,f30(a29)),f34(a45,a37),a41),f12(f33(a45,f30(a29)),f34(a45,a37),a41))), % 59.58/59.61 inference(scs_inference,[],[361,727,591,755,604,820,833,838,841,844,789,769,774,349,514,384,433,715,785,783,772,488,105,630,101,119,98,124,704,743,778,95,673,521,121,758,106,113,305,2,311,324,320,81,89,82,85,3,84,87,90,332,228,229,207,241,292,232,255,282,10,162])). % 59.58/59.61 cnf(866,plain, % 59.58/59.61 (P1(f30(f12(f33(a45,f30(a29)),f34(a45,a37),a41)))), % 59.58/59.61 inference(scs_inference,[],[846,305])). % 59.58/59.61 cnf(868,plain, % 59.58/59.61 (E(f31(a45,a49),f31(f33(a45,a1),a49))), % 59.58/59.61 inference(scs_inference,[],[846,826,305,2])). % 59.58/59.61 cnf(869,plain, % 59.58/59.61 (P2(f33(f33(a45,f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[832,846,826,704,305,2,318])). % 59.58/59.61 cnf(871,plain, % 59.58/59.61 (P1(f34(f33(a45,f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[832,846,826,704,305,2,318,317])). % 59.58/59.61 cnf(873,plain, % 59.58/59.61 (E(f39(f33(f33(a45,f30(a29)),f34(a45,a37))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[832,846,826,704,305,2,318,317,319])). % 59.58/59.61 cnf(877,plain, % 59.58/59.61 (P3(a44,f30(f43(f43(a50))))), % 59.58/59.61 inference(scs_inference,[],[361,832,846,645,813,826,94,704,305,2,318,317,319,311,81])). % 59.58/59.61 cnf(880,plain, % 59.58/59.61 (~P3(x8801,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(883,plain, % 59.58/59.61 (P7(a37,f39(f33(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,636,400,679,832,817,846,645,813,826,710,659,94,704,305,2,318,317,319,311,81,83,82,85,3,84])). % 59.58/59.61 cnf(885,plain, % 59.58/59.61 (P1(f39(f33(f33(a45,f30(a29)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[361,636,400,679,832,817,846,569,645,813,826,463,598,710,659,94,704,113,305,2,318,317,319,311,81,83,82,85,3,84,90,204])). % 59.58/59.61 cnf(891,plain, % 59.58/59.61 (~P3(x8911,f34(f33(a45,f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,636,400,679,604,832,817,846,569,645,813,826,463,598,710,659,745,360,94,704,113,305,2,318,317,319,311,81,83,82,85,3,84,90,204,172,330,335])). % 59.58/59.61 cnf(892,plain, % 59.58/59.61 (~P3(x8921,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(894,plain, % 59.58/59.61 (~P7(a41,f39(f33(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,636,400,679,604,832,817,846,569,647,645,813,826,463,598,710,659,745,360,94,704,113,305,2,318,317,319,311,81,83,82,85,3,84,90,204,172,330,335,202])). % 59.58/59.61 cnf(899,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f39(f33(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,636,400,679,880,604,832,817,846,569,647,850,645,813,826,463,708,598,710,659,745,360,94,704,113,305,2,318,317,319,311,81,83,82,85,3,84,90,204,172,330,335,202,228,207])). % 59.58/59.61 cnf(900,plain, % 59.58/59.61 (~P3(x9001,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(904,plain, % 59.58/59.61 (P7(f26(a46,f3(a37)),a46)), % 59.58/59.61 inference(scs_inference,[],[361,595,636,400,679,880,604,832,817,846,569,647,850,645,813,826,463,708,105,598,710,659,745,360,818,94,704,758,113,305,2,318,317,319,311,81,83,82,85,3,84,90,204,172,330,335,202,228,207,229,241])). % 59.58/59.61 cnf(910,plain, % 59.58/59.61 (~P3(x9101,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(912,plain, % 59.58/59.61 (E(f34(a45,a37),f34(f33(a45,a37),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,595,636,400,679,880,900,910,604,892,832,810,817,846,569,384,647,850,645,813,826,463,708,105,304,630,598,710,659,745,360,632,818,778,94,704,758,113,305,2,318,317,319,311,81,83,82,85,3,84,90,204,172,330,335,202,228,207,229,241,292,255,282])). % 59.58/59.61 cnf(917,plain, % 59.58/59.61 (E(f34(f33(a45,f30(a29)),f34(a45,a37)),a37)), % 59.58/59.61 inference(scs_inference,[],[361,595,636,400,679,880,900,910,604,892,832,810,817,846,569,384,647,850,645,813,826,463,708,105,304,630,598,710,659,745,360,632,818,778,94,704,758,113,305,2,318,317,319,311,81,83,82,85,3,84,90,204,172,330,335,202,228,207,229,241,292,255,282,10,152])). % 59.58/59.61 cnf(923,plain, % 59.58/59.61 (P1(f34(f33(a45,a37),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,595,636,736,400,679,880,900,910,604,892,832,810,817,846,569,384,647,850,645,813,826,463,708,105,304,630,598,710,659,745,360,632,818,778,94,704,758,113,305,2,318,317,319,311,81,83,82,85,3,84,90,204,172,330,335,202,228,207,229,241,292,255,282,10,152,144,320,80])). % 59.58/59.61 cnf(925,plain, % 59.58/59.61 (P5(f34(f33(a45,a37),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,595,636,736,400,679,880,900,910,604,892,832,810,817,846,569,384,433,647,850,645,813,826,463,708,105,304,630,598,710,659,674,745,360,632,818,778,94,704,758,113,305,2,318,317,319,311,81,83,82,85,3,84,90,204,172,330,335,202,228,207,229,241,292,255,282,10,152,144,320,80,89,87])). % 59.58/59.61 cnf(929,plain, % 59.58/59.61 (E(f34(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[912,2])). % 59.58/59.61 cnf(930,plain, % 59.58/59.61 (P1(f34(f33(a45,f30(a29)),a37))), % 59.58/59.61 inference(scs_inference,[],[912,883,704,2,317])). % 59.58/59.61 cnf(932,plain, % 59.58/59.61 (P2(f33(f33(a45,a37),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[912,899,883,632,704,2,317,318])). % 59.58/59.61 cnf(934,plain, % 59.58/59.61 (E(f39(f33(f33(a45,a37),f34(a45,f30(a29)))),f34(a45,f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[912,899,883,632,704,2,317,318,319])). % 59.58/59.61 cnf(938,plain, % 59.58/59.61 (P3(f35(a1,f2(a1)),f38(a48,a50))), % 59.58/59.61 inference(scs_inference,[],[361,541,912,899,923,883,133,632,704,2,317,318,319,311,81])). % 59.58/59.61 cnf(940,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),a37)), % 59.58/59.61 inference(scs_inference,[],[361,541,912,899,923,634,883,133,659,632,704,2,317,318,319,311,81,83,85])). % 59.58/59.61 cnf(942,plain, % 59.58/59.61 (~P3(x9421,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(943,plain, % 59.58/59.61 (E(a37,f34(f33(a45,a37),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,658,541,679,912,899,877,923,634,883,133,659,632,704,2,317,318,319,311,81,83,85,82,3])). % 59.58/59.61 cnf(948,plain, % 59.58/59.61 (P1(f39(f33(f33(a45,a37),f34(a45,f30(a29)))))), % 59.58/59.61 inference(scs_inference,[],[361,658,541,679,912,899,894,877,923,634,667,597,925,403,883,133,659,632,337,704,113,2,317,318,319,311,81,83,85,82,3,84,90,172,204])). % 59.58/59.61 cnf(950,plain, % 59.58/59.61 (~P3(x9501,f34(f33(a45,a37),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,658,541,679,942,912,899,894,877,923,634,667,597,925,403,883,133,659,632,337,704,113,2,317,318,319,311,81,83,85,82,3,84,90,172,204,335])). % 59.58/59.61 cnf(951,plain, % 59.58/59.61 (~P3(x9511,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(957,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f34(f33(a45,a37),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,658,541,679,942,951,912,899,894,877,923,708,634,667,597,925,403,883,133,659,632,337,704,113,2,317,318,319,311,81,83,85,82,3,84,90,172,204,335,202,330,207])). % 59.58/59.61 cnf(960,plain, % 59.58/59.61 (P7(f26(a46,f3(a46)),a46)), % 59.58/59.61 inference(scs_inference,[],[361,736,658,541,679,942,951,912,899,894,877,923,708,105,634,667,597,666,925,403,883,133,659,632,337,758,704,113,2,317,318,319,311,81,83,85,82,3,84,90,172,204,335,202,330,207,241])). % 59.58/59.61 cnf(979,plain, % 59.58/59.61 (E(f39(f33(f33(a45,f30(a29)),a37)),a37)), % 59.58/59.61 inference(scs_inference,[],[917,950,923,883,704,2,152,318,319])). % 59.58/59.61 cnf(983,plain, % 59.58/59.61 (P3(f2(a1),a1)), % 59.58/59.61 inference(scs_inference,[],[398,917,950,339,948,923,883,121,704,2,152,318,319,311,81])). % 59.58/59.61 cnf(986,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[398,917,950,957,929,483,339,948,923,883,934,730,121,704,2,152,318,319,311,81,83,3,85])). % 59.58/59.61 cnf(987,plain, % 59.58/59.61 (~E(f38(a48,a50),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[398,917,604,950,957,929,938,483,339,948,923,883,934,730,121,704,2,152,318,319,311,81,83,3,85,82])). % 59.58/59.61 cnf(988,plain, % 59.58/59.61 (~P3(x9881,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(992,plain, % 59.58/59.61 (~P3(x9921,f34(f33(a45,f30(a29)),a37))), % 59.58/59.61 inference(scs_inference,[],[398,417,917,604,950,957,929,938,483,412,339,304,948,923,572,454,883,934,730,121,106,704,2,152,318,319,311,81,83,3,85,82,84,87,90,335])). % 59.58/59.61 cnf(993,plain, % 59.58/59.61 (~P3(x9931,a37)), % 59.58/59.61 inference(rename_variables,[],[304])). % 59.58/59.61 cnf(995,plain, % 59.58/59.61 (P7(f34(a45,a37),f39(f33(f33(a45,a37),f34(a45,f30(a29)))))), % 59.58/59.61 inference(scs_inference,[],[398,417,917,604,988,950,957,929,938,483,412,339,304,948,923,630,572,454,883,934,730,121,106,704,2,152,318,319,311,81,83,3,85,82,84,87,90,335,207])). % 59.58/59.61 cnf(996,plain, % 59.58/59.61 (~P3(x9961,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1001,plain, % 59.58/59.61 (E(f33(f33(a45,f30(a29)),a37),f33(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[361,398,417,917,604,988,996,950,957,929,938,483,412,339,304,993,948,923,630,598,572,454,883,934,932,730,121,106,704,113,2,152,318,319,311,81,83,3,85,82,84,87,90,335,207,292,263])). % 59.58/59.61 cnf(1004,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f39(f33(f33(a45,a37),f34(a45,f30(a29)))))), % 59.58/59.61 inference(scs_inference,[],[361,398,417,917,604,988,996,950,957,929,938,483,412,339,304,993,948,923,708,630,598,572,454,883,934,932,730,121,106,704,113,2,152,318,319,311,81,83,3,85,82,84,87,90,335,207,292,263,221])). % 59.58/59.61 cnf(1010,plain, % 59.58/59.61 (P1(f34(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,398,417,917,604,988,996,950,957,929,938,483,412,339,304,993,948,923,708,630,598,572,454,883,934,932,730,121,106,704,113,2,152,318,319,311,81,83,3,85,82,84,87,90,335,207,292,263,221,141,149,317])). % 59.58/59.61 cnf(1021,plain, % 59.58/59.61 (E(f33(a45,a37),f33(f33(a45,f30(a29)),a37))), % 59.58/59.61 inference(scs_inference,[],[1001,2])). % 59.58/59.61 cnf(1022,plain, % 59.58/59.61 (E(f34(f33(a45,f30(a29)),a37),a37)), % 59.58/59.61 inference(scs_inference,[],[992,1001,930,2,152])). % 59.58/59.61 cnf(1025,plain, % 59.58/59.61 (P1(f34(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[992,1001,930,1004,932,2,152,317])). % 59.58/59.61 cnf(1027,plain, % 59.58/59.61 (P2(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[995,992,1001,930,1004,932,2,152,317,318])). % 59.58/59.61 cnf(1031,plain, % 59.58/59.61 (E(f39(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[995,992,1001,930,1004,932,2,152,317,318,144,319])). % 59.58/59.61 cnf(1036,plain, % 59.58/59.61 (~E(a1,f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[361,604,983,995,992,1001,1010,930,1004,932,659,2,152,317,318,144,319,311,83,82])). % 59.58/59.61 cnf(1037,plain, % 59.58/59.61 (~P3(x10371,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1039,plain, % 59.58/59.61 (P7(f34(a45,a37),f34(a45,f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[361,929,604,983,995,614,992,1001,1010,930,934,1004,932,659,2,152,317,318,144,319,311,83,82,3,85])). % 59.58/59.61 cnf(1040,plain, % 59.58/59.61 (P7(a37,f39(f33(f33(a45,a37),f34(a45,f30(a29)))))), % 59.58/59.61 inference(scs_inference,[],[361,636,929,604,983,995,614,992,1001,1010,930,934,1004,932,659,2,152,317,318,144,319,311,83,82,3,85,84])). % 59.58/59.61 cnf(1041,plain, % 59.58/59.61 (E(f31(f33(a45,a1),f2(a1)),f31(a45,f2(a1)))), % 59.58/59.61 inference(scs_inference,[],[361,636,929,604,983,995,614,992,1001,1010,930,821,934,1004,932,659,113,2,152,317,318,144,319,311,83,82,3,85,84,332])). % 59.58/59.61 cnf(1043,plain, % 59.58/59.61 (P1(f39(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[361,636,929,604,983,995,614,992,1001,1010,930,598,821,934,1004,932,659,113,2,152,317,318,144,319,311,83,82,3,85,84,332,204])). % 59.58/59.61 cnf(1045,plain, % 59.58/59.61 (~P3(x10451,f34(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,636,929,604,1037,983,995,614,992,1001,1010,930,598,821,934,1004,932,659,113,2,152,317,318,144,319,311,83,82,3,85,84,332,204,335])). % 59.58/59.61 cnf(1046,plain, % 59.58/59.61 (~P3(x10461,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1051,plain, % 59.58/59.61 (~P3(x10511,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1053,plain, % 59.58/59.61 (E(f34(a45,a37),f34(a45,f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[361,636,929,604,1037,1046,983,995,614,992,1001,1010,930,708,630,598,821,934,1004,986,932,659,113,2,152,317,318,144,319,311,83,82,3,85,84,332,204,335,202,207,193])). % 59.58/59.61 cnf(1056,plain, % 59.58/59.61 (~P3(x10561,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(1058,plain, % 59.58/59.61 (E(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f33(f33(a45,f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,636,929,604,1037,1046,1051,679,832,983,995,614,992,1001,1010,930,708,630,598,821,934,1004,986,932,659,704,113,2,152,317,318,144,319,311,83,82,3,85,84,332,204,335,202,207,193,292,263])). % 59.58/59.61 cnf(1059,plain, % 59.58/59.61 (~P3(x10591,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1066,plain, % 59.58/59.61 (P3(f12(f33(a45,a37),f34(a45,f30(a29)),a41),a41)), % 59.58/59.61 inference(scs_inference,[],[361,636,929,604,1037,1046,1051,1059,679,1056,899,832,983,995,614,992,1001,868,1010,930,708,630,101,598,821,934,1004,986,932,659,632,121,704,113,2,152,317,318,144,319,311,83,82,3,85,84,332,204,335,202,207,193,292,263,255,221,282])). % 59.58/59.61 cnf(1071,plain, % 59.58/59.61 (P1(f30(f12(f33(a45,a37),f34(a45,f30(a29)),a41)))), % 59.58/59.61 inference(scs_inference,[],[361,636,929,604,1037,1046,1051,1059,679,1056,899,832,983,995,614,992,1001,868,1010,930,708,630,101,598,821,934,1004,986,932,659,632,121,704,113,2,152,317,318,144,319,311,83,82,3,85,84,332,204,335,202,207,193,292,263,255,221,282,162,305])). % 59.58/59.61 cnf(1084,plain, % 59.58/59.61 (E(f34(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),a37)), % 59.58/59.61 inference(scs_inference,[],[1045,1053,1010,2,152])). % 59.58/59.61 cnf(1095,plain, % 59.58/59.61 (~E(f30(f43(a49)),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[398,604,439,1045,1053,1043,1010,1040,932,2,152,318,144,317,311,82])). % 59.58/59.61 cnf(1096,plain, % 59.58/59.61 (~P3(x10961,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1097,plain, % 59.58/59.61 (P7(f26(a37,f3(a37)),f30(a29))), % 59.58/59.61 inference(scs_inference,[],[398,389,604,439,1045,1053,1043,1010,617,1040,932,2,152,318,144,317,311,82,85])). % 59.58/59.61 cnf(1099,plain, % 59.58/59.61 (P7(f30(a29),f39(f33(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[398,389,929,604,439,1045,1053,669,1043,1010,883,617,1040,932,2,152,318,144,317,311,82,85,3,84])). % 59.58/59.61 cnf(1101,plain, % 59.58/59.61 (~P3(x11011,a37)), % 59.58/59.61 inference(rename_variables,[],[304])). % 59.58/59.61 cnf(1103,plain, % 59.58/59.61 (P7(f34(a45,a37),f39(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[398,389,929,604,1096,439,1045,1053,669,304,1043,1010,630,883,617,1040,932,2,152,318,144,317,311,82,85,3,84,335,207])). % 59.58/59.61 cnf(1107,plain, % 59.58/59.61 (~P3(x11071,a37)), % 59.58/59.61 inference(rename_variables,[],[304])). % 59.58/59.61 cnf(1112,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f39(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[361,398,389,929,604,1096,439,1045,1053,669,1066,304,1101,1107,1043,1010,708,630,117,883,617,1040,986,932,2,152,318,144,317,311,82,85,3,84,335,207,292,232,221])). % 59.58/59.61 cnf(1114,plain, % 59.58/59.61 (E(f39(f33(f33(a45,f30(a29)),f30(a29))),f30(a29))), % 59.58/59.61 inference(scs_inference,[],[361,398,389,929,604,1096,439,1045,1053,669,1066,304,1101,1107,1043,1010,708,630,117,883,617,1040,986,932,704,2,152,318,144,317,311,82,85,3,84,335,207,292,232,221,319])). % 59.58/59.61 cnf(1118,plain, % 59.58/59.61 (P9(a29,f12(f33(a45,a37),f34(a45,f30(a29)),a41))), % 59.58/59.61 inference(scs_inference,[],[361,398,389,929,1001,604,1096,439,1045,1053,669,1066,304,1101,1107,1043,1010,708,630,117,883,617,1040,356,986,932,704,2,152,318,144,317,311,82,85,3,84,335,207,292,232,221,319,80,83,215])). % 59.58/59.61 cnf(1120,plain, % 59.58/59.61 (P1(f39(f33(f33(a45,f30(a29)),f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,398,389,929,1001,604,1096,439,1045,1053,669,1066,304,1101,1107,1043,1010,708,630,117,883,617,1040,356,986,932,704,2,152,318,144,317,311,82,85,3,84,335,207,292,232,221,319,80,83,215,158])). % 59.58/59.61 cnf(1130,plain, % 59.58/59.61 (P1(f34(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[1058,1103,1027,2,317])). % 59.58/59.61 cnf(1132,plain, % 59.58/59.61 (P2(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[1058,1103,1027,2,317,318])). % 59.58/59.61 cnf(1134,plain, % 59.58/59.61 (E(f39(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[1058,1103,1027,2,317,318,319])). % 59.58/59.61 cnf(1141,plain, % 59.58/59.61 (~P3(x11411,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(1143,plain, % 59.58/59.61 (~E(f30(f43(a49)),a37)), % 59.58/59.61 inference(scs_inference,[],[398,658,541,1058,679,480,1103,1095,433,1025,1118,1027,792,659,2,317,318,319,311,89,83,82,85,3])). % 59.58/59.61 cnf(1144,plain, % 59.58/59.61 (P7(a37,f39(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[398,636,658,541,1058,679,480,1103,1095,433,1025,1118,1027,792,659,2,317,318,319,311,89,83,82,85,3,84])). % 59.58/59.61 cnf(1145,plain, % 59.58/59.61 (P1(f39(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[398,636,658,541,1058,679,480,1103,1095,433,1025,1118,598,1027,792,659,113,2,317,318,319,311,89,83,82,85,3,84,204])). % 59.58/59.61 cnf(1147,plain, % 59.58/59.61 (~P3(x11471,f34(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[398,636,658,541,1058,679,480,1103,1095,433,342,1025,1118,598,1027,792,1099,659,704,113,2,317,318,319,311,89,83,82,85,3,84,204,335])). % 59.58/59.61 cnf(1150,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f34(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[398,636,658,541,1058,679,1141,480,1103,1095,433,342,1025,1118,708,598,1027,792,1099,659,704,113,2,317,318,319,311,89,83,82,85,3,84,204,335,207])). % 59.58/59.61 cnf(1154,plain, % 59.58/59.61 (~P3(x11541,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1156,plain, % 59.58/59.61 (E(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)),f33(f33(a45,f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,398,636,658,541,1058,679,1141,604,1154,480,832,1103,1095,433,342,1025,1118,708,598,1027,792,1099,659,704,113,2,317,318,319,311,89,83,82,85,3,84,204,335,207,292,263])). % 59.58/59.61 cnf(1165,plain, % 59.58/59.61 (~P6(f34(f33(a45,f30(a29)),f30(a29)))+~P1(f34(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[361,398,636,658,541,1058,679,1141,604,1154,480,832,1103,1095,433,342,1025,1118,708,630,598,1039,1027,792,1099,659,704,113,2,317,318,319,311,89,83,82,85,3,84,204,335,207,292,263,221,152,141,144])). % 59.58/59.61 cnf(1169,plain, % 59.58/59.61 (P1(f34(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[1022,1112,1027,2,317])). % 59.58/59.61 cnf(1176,plain, % 59.58/59.61 (~P3(x11761,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(1181,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f39(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[398,727,541,1022,573,679,1176,1150,1143,1145,708,1112,904,1027,106,2,317,318,311,82,87,85,3,84,207])). % 59.58/59.61 cnf(1182,plain, % 59.58/59.61 (~P3(x11821,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(1187,plain, % 59.58/59.61 (P7(f34(a45,a37),f39(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[361,398,727,541,1022,573,679,1176,1182,1150,1143,1145,708,630,1039,1112,904,1027,106,2,317,318,311,82,87,85,3,84,207,292,221])). % 59.58/59.61 cnf(1189,plain, % 59.58/59.61 (E(f39(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)),f34(a45,a37))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[361,398,727,541,1022,573,679,1176,1182,1150,1143,1145,708,630,1039,1112,1132,904,1027,106,2,317,318,311,82,87,85,3,84,207,292,221,319])). % 59.58/59.61 cnf(1211,plain, % 59.58/59.61 (P1(f34(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[1084,1181,1132,2,317])). % 59.58/59.61 cnf(1217,plain, % 59.58/59.61 (~E(f30(f43(f3(a37))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[398,1084,604,665,1181,1169,1132,2,317,318,311,82])). % 59.58/59.61 cnf(1218,plain, % 59.58/59.61 (~P3(x12181,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1221,plain, % 59.58/59.61 (~E(f38(a48,a50),a37)), % 59.58/59.61 inference(scs_inference,[],[398,658,1084,604,665,1181,987,1169,934,1040,1132,106,2,317,318,311,82,85,87,3])). % 59.58/59.61 cnf(1222,plain, % 59.58/59.61 (P7(a37,f39(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[398,727,658,1084,604,665,1181,987,1169,934,1040,1132,106,2,317,318,311,82,85,87,3,84])). % 59.58/59.61 cnf(1223,plain, % 59.58/59.61 (P1(f39(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[398,727,658,1084,604,665,1181,987,1169,598,934,1040,1189,1132,106,113,2,317,318,311,82,85,87,3,84,204])). % 59.58/59.61 cnf(1225,plain, % 59.58/59.61 (P7(f34(a45,a37),f34(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[398,727,658,1084,604,1218,665,1181,987,1169,630,598,934,1040,1189,1132,106,113,2,317,318,311,82,85,87,3,84,204,207])). % 59.58/59.61 cnf(1242,plain, % 59.58/59.61 (P1(f34(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[1156,1099,704,2,317])). % 59.58/59.61 cnf(1244,plain, % 59.58/59.61 (P2(f33(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[1156,1099,704,2,317,318])). % 59.58/59.61 cnf(1246,plain, % 59.58/59.61 (~E(f30(f43(f3(a46))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[1156,604,817,1099,704,2,317,318,82])). % 59.58/59.61 cnf(1247,plain, % 59.58/59.61 (~P3(x12471,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1248,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f30(a29))), % 59.58/59.61 inference(scs_inference,[],[389,1156,604,817,1099,940,704,2,317,318,82,85])). % 59.58/59.61 cnf(1251,plain, % 59.58/59.61 (P7(f34(a45,a37),f34(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[389,636,727,1156,604,1247,817,1225,1221,1211,630,1099,940,704,2,317,318,82,85,3,84,207])). % 59.58/59.61 cnf(1255,plain, % 59.58/59.61 (~P3(x12551,f30(a29))), % 59.58/59.61 inference(rename_variables,[],[342])). % 59.58/59.61 cnf(1257,plain, % 59.58/59.61 (E(f33(f33(a45,f30(a29)),f30(a29)),f33(a45,f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[361,389,636,727,1156,604,1247,817,1225,1221,342,1255,1211,630,667,1114,1099,940,704,113,2,317,318,82,85,3,84,207,292,263])). % 59.58/59.61 cnf(1261,plain, % 59.58/59.61 (E(f34(f33(a45,f30(a29)),f30(a29)),a37)), % 59.58/59.61 inference(scs_inference,[],[361,389,636,727,1156,604,1247,817,1147,1225,1221,342,1255,1211,630,667,1114,1099,940,704,113,2,317,318,82,85,3,84,207,292,263,1165,152])). % 59.58/59.61 cnf(1271,plain, % 59.58/59.61 (P1(f34(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[1257,1187,1132,2,317])). % 59.58/59.61 cnf(1273,plain, % 59.58/59.61 (P2(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[1257,1187,1132,2,317,318])). % 59.58/59.61 cnf(1275,plain, % 59.58/59.61 (~E(f30(f43(f43(a50))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[877,604,1257,1187,1132,2,317,318,82])). % 59.58/59.61 cnf(1276,plain, % 59.58/59.61 (~P3(x12761,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1278,plain, % 59.58/59.61 (~E(f30(f43(f3(a37))),a37)), % 59.58/59.61 inference(scs_inference,[],[658,541,877,604,1257,1217,1187,960,1132,2,317,318,82,85,3])). % 59.58/59.61 cnf(1280,plain, % 59.58/59.61 (P7(f34(a45,a37),f39(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[636,658,541,877,604,1276,1251,1257,1217,1223,630,1187,960,1132,2,317,318,82,85,3,84,207])). % 59.58/59.61 cnf(1281,plain, % 59.58/59.61 (~P3(x12811,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1284,plain, % 59.58/59.61 (~P3(x12841,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1286,plain, % 59.58/59.61 (E(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)),f34(a45,a37)),f33(f33(a45,f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,636,658,541,832,877,604,1276,1281,1284,1251,1257,1217,1223,630,1189,1187,960,1132,704,2,317,318,82,85,3,84,207,292,263])). % 59.58/59.61 cnf(1297,plain, % 59.58/59.61 (P1(f34(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)),f34(a45,a37)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[1261,1280,1273,2,317])). % 59.58/59.61 cnf(1303,plain, % 59.58/59.61 (~E(f30(f43(f2(a1))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[361,480,1261,604,1280,1271,1273,2,317,311,318,82])). % 59.58/59.61 cnf(1304,plain, % 59.58/59.61 (~P3(x13041,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1307,plain, % 59.58/59.61 (P7(a37,f39(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[361,636,541,480,1261,604,1280,1271,1273,835,106,2,317,311,318,82,87,85,84])). % 59.58/59.61 cnf(1309,plain, % 59.58/59.61 (P7(f34(a45,a37),f34(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,636,917,541,480,1261,604,1304,1280,1278,1271,630,1273,835,106,2,317,311,318,82,87,85,84,3,207])). % 59.58/59.61 cnf(1335,plain, % 59.58/59.61 (P7(a37,f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[398,938,891,1286,1297,1031,1144,1027,2,317,311,318,82,85])). % 59.58/59.61 cnf(1337,plain, % 59.58/59.61 (~E(f30(f43(f3(a46))),a37)), % 59.58/59.61 inference(scs_inference,[],[398,636,658,938,891,1286,1309,1246,1297,1031,1144,1027,2,317,311,318,82,85,84,3])). % 59.58/59.61 cnf(1338,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f34(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)),f34(a45,a37)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[398,636,658,938,891,679,1286,1309,1246,1297,708,1031,1144,1027,2,317,311,318,82,85,84,3,207])). % 59.58/59.61 cnf(1357,plain, % 59.58/59.61 (E(f31(a45,f2(a1)),f31(f33(a45,a1),f2(a1)))), % 59.58/59.61 inference(scs_inference,[],[1041,2])). % 59.58/59.61 cnf(1364,plain, % 59.58/59.61 (~E(f30(f43(a50)),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[361,514,604,1130,1041,1222,1132,2,317,311,318,82])). % 59.58/59.61 cnf(1365,plain, % 59.58/59.61 (~P3(x13651,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1369,plain, % 59.58/59.61 (P7(f34(a45,a37),f34(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f34(a45,a37)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,727,917,514,604,1365,1338,1337,1130,1041,630,934,1222,1004,1132,2,317,311,318,82,85,84,3,207])). % 59.58/59.61 cnf(1390,plain, % 59.58/59.61 (~P3(x13901,f34(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[1147])). % 59.58/59.61 cnf(1393,plain, % 59.58/59.61 (P7(f34(f33(a45,f30(a29)),f30(a29)),f39(f33(f33(a45,f30(a29)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[361,636,929,547,1147,1390,1369,819,885,1242,979,1307,1273,106,2,317,311,318,87,82,84,3,207])). % 59.58/59.61 cnf(1394,plain, % 59.58/59.61 (~P3(x13941,f34(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[1147])). % 59.58/59.61 cnf(1397,plain, % 59.58/59.61 (~P3(x13971,f34(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[1147])). % 59.58/59.61 cnf(1403,plain, % 59.58/59.61 (~P3(x14031,f34(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[1147])). % 59.58/59.61 cnf(1405,plain, % 59.58/59.61 (E(f34(a45,f30(a29)),f34(f33(f33(a45,f30(a29)),f34(a45,a37)),f34(f33(a45,f30(a29)),f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,736,774,636,929,547,983,1147,1390,1394,1397,1403,679,1369,1357,819,815,304,885,1242,708,979,821,869,1307,1273,106,113,2,317,311,318,87,82,84,3,207,232,292,255,282])). % 59.58/59.61 cnf(1410,plain, % 59.58/59.61 (P1(f34(f33(f33(a45,f30(a29)),f34(a45,a37)),f34(f33(a45,f30(a29)),f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,736,774,636,929,547,1021,983,1147,1390,1394,1397,1403,679,1369,1357,819,815,304,885,1242,708,979,821,869,1307,1273,106,113,2,317,311,318,87,82,84,3,207,232,292,255,282,83,80])). % 59.58/59.61 cnf(1411,plain, % 59.58/59.61 (P7(f34(f33(a45,f30(a29)),f30(a29)),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[361,736,774,636,929,547,1021,983,1147,1390,1394,1397,1403,679,1369,1357,819,815,304,885,1242,708,979,873,821,869,1307,1273,106,113,2,317,311,318,87,82,84,3,207,232,292,255,282,83,80,85])). % 59.58/59.61 cnf(1420,plain, % 59.58/59.61 (E(f34(f33(f33(a45,f30(a29)),f34(a45,a37)),f34(f33(a45,f30(a29)),f30(a29))),f34(a45,f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[1405,2])). % 59.58/59.61 cnf(1427,plain, % 59.58/59.61 (~E(f30(f43(a44)),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[398,573,604,1405,1393,1410,824,869,730,2,311,318,83,87,82])). % 59.58/59.61 cnf(1428,plain, % 59.58/59.61 (~P3(x14281,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1429,plain, % 59.58/59.61 (P7(f34(f33(a45,f30(a29)),f30(a29)),a37)), % 59.58/59.61 inference(scs_inference,[],[398,636,573,604,1405,1393,1410,1411,824,869,730,2,311,318,83,87,82,85])). % 59.58/59.61 cnf(1430,plain, % 59.58/59.61 (P7(a37,f39(f33(f33(a45,f30(a29)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[398,636,1261,573,604,1405,1393,1410,1411,824,869,730,2,311,318,83,87,82,85,84])). % 59.58/59.61 cnf(1436,plain, % 59.58/59.61 (~P3(x14361,f34(f33(f33(a45,f30(a29)),f34(a45,a37)),a37))), % 59.58/59.61 inference(scs_inference,[],[398,636,658,1261,573,604,1405,1393,1275,304,1410,1411,824,487,869,730,2,311,318,83,87,82,85,84,3,172,330,335])). % 59.58/59.61 cnf(1437,plain, % 59.58/59.61 (~P3(x14371,a37)), % 59.58/59.61 inference(rename_variables,[],[304])). % 59.58/59.61 cnf(1440,plain, % 59.58/59.61 (~P3(x14401,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1445,plain, % 59.58/59.61 (E(f34(a45,a37),f34(f33(f33(a45,f30(a29)),f34(a45,a37)),f34(f33(a45,f30(a29)),f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,398,636,658,1261,573,604,1428,1440,1147,1405,1393,1275,304,1437,1410,630,1411,824,487,869,730,2,311,318,83,87,82,85,84,3,172,330,335,207,292,282])). % 59.58/59.61 cnf(1453,plain, % 59.58/59.61 (E(f39(f33(f33(f33(a45,f30(a29)),f34(a45,a37)),a37)),a37)), % 59.58/59.61 inference(scs_inference,[],[361,398,636,658,1261,573,604,1428,1440,1147,1405,1393,1275,304,1437,1410,708,630,986,1411,824,487,869,730,2,311,318,83,87,82,85,84,3,172,330,335,207,292,282,221,152,319])). % 59.58/59.61 cnf(1455,plain, % 59.58/59.61 (P1(f34(f33(f33(a45,f30(a29)),f34(a45,a37)),a37))), % 59.58/59.61 inference(scs_inference,[],[361,398,636,658,1261,573,604,1428,1440,1147,1405,1393,1275,304,1437,1410,708,630,986,1411,824,487,869,730,2,311,318,83,87,82,85,84,3,172,330,335,207,292,282,221,152,319,317])). % 59.58/59.61 cnf(1459,plain, % 59.58/59.61 (P1(f39(f33(f33(f33(a45,f30(a29)),f34(a45,a37)),a37)))), % 59.58/59.61 inference(scs_inference,[],[361,398,636,658,1261,573,604,1428,1440,1147,1405,1393,1275,304,1437,1410,708,630,986,1411,824,487,869,730,2,311,318,83,87,82,85,84,3,172,330,335,207,292,282,221,152,319,317,149,141])). % 59.58/59.61 cnf(1461,plain, % 59.58/59.61 (~P6(f34(f33(f33(a45,f30(a29)),f34(a45,a37)),a37))+~P1(f34(f33(f33(a45,f30(a29)),f34(a45,a37)),a37))), % 59.58/59.61 inference(scs_inference,[],[361,398,636,658,1261,573,604,1428,1440,1147,1405,1393,1275,304,1437,1410,708,630,986,1411,824,487,869,730,2,311,318,83,87,82,85,84,3,172,330,335,207,292,282,221,152,319,317,149,141,144])). % 59.58/59.61 cnf(1468,plain, % 59.58/59.61 (E(f34(f33(f33(a45,f30(a29)),f34(a45,a37)),a37),a37)), % 59.58/59.61 inference(scs_inference,[],[1445,1436,1455,1459,1453,1461,2,144,152])). % 59.58/59.61 cnf(1475,plain, % 59.58/59.61 (~E(a54,f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[361,604,1445,1436,384,871,1455,1459,1004,1453,932,1461,2,144,152,311,318,82])). % 59.58/59.61 cnf(1477,plain, % 59.58/59.61 (P7(f34(f33(a45,f30(a29)),f30(a29)),f30(a29))), % 59.58/59.61 inference(scs_inference,[],[361,389,604,1445,1436,384,871,1455,1459,1004,1429,1453,932,1461,2,144,152,311,318,82,85])). % 59.58/59.61 cnf(1504,plain, % 59.58/59.61 (~P3(x15041,f34(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[1147])). % 59.58/59.61 cnf(1505,plain, % 59.58/59.61 (P7(f30(a29),f39(f33(f33(a45,a37),f34(a45,f30(a29)))))), % 59.58/59.61 inference(scs_inference,[],[361,389,120,1147,1468,866,1040,1430,869,106,2,311,318,87,82,84])). % 59.58/59.61 cnf(1506,plain, % 59.58/59.61 (~E(f30(f43(f2(a1))),a37)), % 59.58/59.61 inference(scs_inference,[],[361,389,658,120,1147,1303,1468,866,1040,1430,869,106,2,311,318,87,82,84,3])). % 59.58/59.61 cnf(1507,plain, % 59.58/59.61 (~P3(x15071,f34(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[361,389,658,120,1147,1303,1468,342,866,1040,1430,869,932,106,2,311,318,87,82,84,3,335])). % 59.58/59.61 cnf(1508,plain, % 59.58/59.61 (~P3(x15081,f30(a29))), % 59.58/59.61 inference(rename_variables,[],[342])). % 59.58/59.61 cnf(1510,plain, % 59.58/59.61 (P7(f34(f33(a45,f30(a29)),f30(a29)),f30(f12(f33(a45,f30(a29)),f34(a45,a37),a41)))), % 59.58/59.61 inference(scs_inference,[],[361,389,658,120,1147,1504,1303,1468,342,866,1242,1040,1430,869,932,106,2,311,318,87,82,84,3,335,207])). % 59.58/59.61 cnf(1516,plain, % 59.58/59.61 (E(f33(f33(f33(a45,f30(a29)),f34(a45,a37)),a37),f33(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[361,389,658,120,1147,1504,1303,1468,342,1508,304,866,1242,598,1040,1430,1453,869,932,106,113,2,311,318,87,82,84,3,335,207,292,263])). % 59.58/59.61 cnf(1519,plain, % 59.58/59.61 (E(f39(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29))),f30(a29))), % 59.58/59.61 inference(scs_inference,[],[361,389,658,120,1147,1504,1303,1468,342,1508,304,866,1242,598,1040,1430,1453,869,932,106,113,2,311,318,87,82,84,3,335,207,292,263,319])). % 59.58/59.61 cnf(1521,plain, % 59.58/59.61 (P1(f34(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[361,389,658,120,1147,1504,1303,1468,342,1508,304,866,1242,598,1040,1430,1453,869,932,106,113,2,311,318,87,82,84,3,335,207,292,263,319,317])). % 59.58/59.61 cnf(1525,plain, % 59.58/59.61 (P7(f30(a29),f34(a45,f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[361,389,658,1156,120,1147,1504,1303,1468,342,1508,304,866,1242,598,934,1040,1430,1453,356,869,932,106,113,2,311,318,87,82,84,3,335,207,292,263,319,317,80,83,85])). % 59.58/59.61 cnf(1526,plain, % 59.58/59.61 (E(f30(a29),f34(a45,f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[361,389,658,1156,120,1147,1504,1303,1468,342,1508,304,866,1242,340,708,598,934,1040,1430,1453,1248,356,869,932,106,113,2,311,318,87,82,84,3,335,207,292,263,319,317,80,83,85,193])). % 59.58/59.61 cnf(1528,plain, % 59.58/59.61 (P1(f39(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,389,658,1156,120,1147,1504,1303,1468,342,1508,304,866,1242,340,708,117,598,934,1040,1430,1453,1248,356,869,932,106,113,2,311,318,87,82,84,3,335,207,292,263,319,317,80,83,85,193,158])). % 59.58/59.61 cnf(1540,plain, % 59.58/59.61 (E(f34(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),a37)), % 59.58/59.61 inference(scs_inference,[],[1516,1507,1521,2,152])). % 59.58/59.61 cnf(1545,plain, % 59.58/59.61 (P2(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[398,1516,1507,1071,1521,1505,932,2,152,311,318])). % 59.58/59.61 cnf(1549,plain, % 59.58/59.61 (~P3(x15491,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(1553,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f30(f12(f33(a45,a37),f34(a45,f30(a29)),a41)))), % 59.58/59.61 inference(scs_inference,[],[398,917,447,349,679,1549,1516,1507,1526,1506,1071,1521,708,497,1505,338,932,2,152,311,318,83,82,85,84,3,207])). % 59.58/59.61 cnf(1558,plain, % 59.58/59.61 (P7(f9(f30(a29),a49,f34(a45,f30(a29))),f30(a29))), % 59.58/59.61 inference(scs_inference,[],[361,398,917,447,349,679,1549,1516,1507,1526,1506,1071,1521,340,708,497,1248,1525,1505,824,338,932,2,152,311,318,83,82,85,84,3,207,193,267])). % 59.58/59.61 cnf(1560,plain, % 59.58/59.61 (E(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f33(a45,f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[361,398,917,447,349,679,1549,1516,1507,1526,1506,342,1071,1521,340,708,667,497,1248,1525,1505,1519,824,338,932,113,2,152,311,318,83,82,85,84,3,207,193,267,263])). % 59.58/59.61 cnf(1572,plain, % 59.58/59.61 (~E(f30(f43(f12(a45,f30(a29),a41))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[398,604,1560,734,1528,2,311,82])). % 59.58/59.61 cnf(1573,plain, % 59.58/59.61 (~P3(x15731,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1576,plain, % 59.58/59.61 (~E(a1,a37)), % 59.58/59.61 inference(scs_inference,[],[398,658,523,604,1526,1560,1036,734,1528,551,2,311,82,85,84,3])). % 59.58/59.61 cnf(1577,plain, % 59.58/59.61 (P7(f34(a45,a37),f39(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[398,658,523,604,1573,1526,1560,1036,734,1528,630,551,2,311,82,85,84,3,207])). % 59.58/59.61 cnf(1578,plain, % 59.58/59.61 (~P3(x15781,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1585,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f39(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,398,658,523,604,1573,1578,1526,1560,1036,734,1528,393,708,630,986,551,1545,824,2,311,82,85,84,3,207,267,292,221])). % 59.58/59.61 cnf(1587,plain, % 59.58/59.61 (E(f39(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[361,398,658,523,604,1573,1578,1526,1560,1036,734,1528,393,708,630,986,551,1545,824,2,311,82,85,84,3,207,267,292,221,319])). % 59.58/59.61 cnf(1589,plain, % 59.58/59.61 (P1(f34(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,398,658,523,604,1573,1578,1526,1560,1036,734,1528,393,708,630,986,551,1545,824,2,311,82,85,84,3,207,267,292,221,319,317])). % 59.58/59.61 cnf(1591,plain, % 59.58/59.61 (P2(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,398,658,523,604,1573,1578,1526,1560,1036,734,1528,393,708,630,986,551,1545,824,2,311,82,85,84,3,207,267,292,221,319,317,318])). % 59.58/59.61 cnf(1606,plain, % 59.58/59.61 (P1(f34(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[1540,1585,1545,2,317])). % 59.58/59.61 cnf(1615,plain, % 59.58/59.61 (~P3(x16151,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(1619,plain, % 59.58/59.61 (P1(f39(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[361,917,579,983,679,1526,1540,1576,1589,598,454,1587,1585,1545,659,106,113,2,317,311,318,87,83,82,85,84,3,204])). % 59.58/59.61 cnf(1621,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f34(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,917,579,983,679,1615,1526,1540,1576,1589,708,598,454,1587,1585,1545,659,106,113,2,317,311,318,87,83,82,85,84,3,204,207])). % 59.58/59.61 cnf(1622,plain, % 59.58/59.61 (~P3(x16221,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(1627,plain, % 59.58/59.61 (E(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)),f33(f33(a45,f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,917,832,579,983,679,1615,1622,604,1526,1540,1576,1589,708,598,454,1587,1591,1585,1545,659,106,704,113,2,317,311,318,87,83,82,85,84,3,204,207,292,263])). % 59.58/59.61 cnf(1648,plain, % 59.58/59.61 (~E(f30(f43(f12(a45,f30(a29),a41))),a37)), % 59.58/59.61 inference(scs_inference,[],[398,636,658,439,1147,1526,1577,1627,1572,1606,1097,2,311,82,85,84,3])). % 59.58/59.61 cnf(1649,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f34(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[398,636,658,439,1147,679,1526,1577,1627,1572,1606,708,1097,2,311,82,85,84,3,207])). % 59.58/59.61 cnf(1678,plain, % 59.58/59.61 (P7(f34(a45,a37),f39(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[398,727,665,1147,604,1526,1649,1648,1619,630,710,1477,446,2,311,87,82,85,84,3,207])). % 59.58/59.61 cnf(1679,plain, % 59.58/59.61 (~P3(x16791,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1682,plain, % 59.58/59.61 (~P3(x16821,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1687,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f39(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[361,398,727,665,1147,604,1679,1526,1649,1364,1648,304,1619,808,708,630,710,598,986,1477,1591,446,113,2,311,87,82,85,84,3,207,292,282,221])). % 59.58/59.61 cnf(1691,plain, % 59.58/59.61 (P1(f34(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,398,727,665,1147,604,1679,1526,1649,1364,1648,304,1619,808,708,630,710,598,986,1477,1591,446,113,2,311,87,82,85,84,3,207,292,282,221,319,317])). % 59.58/59.61 cnf(1693,plain, % 59.58/59.61 (P2(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,398,727,665,1147,604,1679,1526,1649,1364,1648,304,1619,808,708,630,710,598,986,1477,1591,446,113,2,311,87,82,85,84,3,207,292,282,221,319,317,318])). % 59.58/59.61 cnf(1697,plain, % 59.58/59.61 (P1(f39(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[361,398,727,943,665,1147,604,1679,1526,1649,1364,1648,304,1619,808,708,630,710,598,986,1477,1591,446,659,113,2,311,87,82,85,84,3,207,292,282,221,319,317,318,86,83,204])). % 59.58/59.61 cnf(1699,plain, % 59.58/59.61 (E(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)),f34(a45,a37)),f33(f33(a45,f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[361,398,727,943,832,665,1147,604,1679,1682,1526,1649,1364,1648,304,1619,808,708,630,710,598,986,1477,1591,446,659,704,113,2,311,87,82,85,84,3,207,292,282,221,319,317,318,86,83,204,263])). % 59.58/59.61 cnf(1710,plain, % 59.58/59.61 (P1(f34(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[1699,1687,1591,2,317])). % 59.58/59.61 cnf(1716,plain, % 59.58/59.61 (P7(f9(f30(a29),a49,f34(a45,f30(a29))),f34(a45,f30(a29)))), % 59.58/59.61 inference(scs_inference,[],[817,1526,1147,1699,1687,1558,1591,2,317,318,82,85])). % 59.58/59.61 cnf(1717,plain, % 59.58/59.61 (P7(a37,f39(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[636,817,1526,1147,1699,1678,1687,1558,1591,2,317,318,82,85,84])). % 59.58/59.61 cnf(1718,plain, % 59.58/59.61 (~E(f30(f43(a44)),a37)), % 59.58/59.61 inference(scs_inference,[],[636,658,817,1526,1147,1699,1678,1427,1687,1558,1591,2,317,318,82,85,84,3])). % 59.58/59.61 cnf(1719,plain, % 59.58/59.61 (P7(f34(a45,a37),f39(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[636,658,817,1526,1147,604,1699,1678,1427,1697,630,1687,1558,1591,2,317,318,82,85,84,3,207])). % 59.58/59.61 cnf(1725,plain, % 59.58/59.61 (P7(a37,f39(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[361,636,658,817,1526,1147,679,604,1699,1678,1427,1697,301,630,1335,1687,1558,1591,2,317,318,82,85,84,3,207,292,221])). % 59.58/59.61 cnf(1737,plain, % 59.58/59.61 (P1(f34(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)),f34(a45,a37)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[1719,1031,1693,2,317])). % 59.58/59.61 cnf(1743,plain, % 59.58/59.61 (~P3(x17431,f34(f33(a45,f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(rename_variables,[],[891])). % 59.58/59.61 cnf(1748,plain, % 59.58/59.61 (~P3(x17481,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1754,plain, % 59.58/59.61 (~P3(x17541,f34(f33(a45,f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(rename_variables,[],[891])). % 59.58/59.61 cnf(1756,plain, % 59.58/59.61 (E(f34(f33(a45,f30(a29)),f34(a45,a37)),f34(f33(f33(a45,f30(a29)),f34(a45,a37)),f34(f33(a45,f30(a29)),f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[361,727,917,120,983,891,1743,1754,1147,604,1748,1393,1719,1621,1718,1357,1710,871,630,1031,821,1693,1716,674,869,113,2,317,318,87,82,85,84,3,207,292,255,282])). % 59.58/59.61 cnf(1778,plain, % 59.58/59.61 (~P3(x17781,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(1780,plain, % 59.58/59.61 (~E(a54,a37)), % 59.58/59.61 inference(scs_inference,[],[736,658,1261,514,679,1756,1510,1475,1737,1725,1693,2,317,311,318,82,84,3])). % 59.58/59.61 cnf(1783,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f34(f33(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)),f34(a45,a37)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[736,658,1261,514,679,1778,384,1756,1510,1475,1737,708,122,1725,1693,2,317,311,318,82,84,3,316,207])). % 59.58/59.61 cnf(1807,plain, % 59.58/59.61 (P5(f39(f33(f33(a45,f30(a29)),f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[736,1691,1114,1717,446,1591,2,317,311,318,87])). % 59.58/59.61 cnf(1809,plain, % 59.58/59.61 (~P3(x18091,f34(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[1147])). % 59.58/59.61 cnf(1812,plain, % 59.58/59.61 (P7(f34(f33(a45,f30(a29)),f30(a29)),f34(f33(f33(f33(f33(a45,a37),f34(a45,f30(a29))),f30(a29)),f34(a45,a37)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[736,727,877,1147,1809,1783,1780,1691,1242,1114,1717,446,1591,2,317,311,318,87,82,84,3,207])). % 59.58/59.61 cnf(1828,plain, % 59.58/59.61 (~E(f30(f43(f12(a45,a37,a41))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[736,604,663,1120,1134,674,2,311,87,82])). % 59.58/59.61 cnf(1829,plain, % 59.58/59.61 (~P3(x18291,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1831,plain, % 59.58/59.61 (E(a37,f34(f33(f33(a45,f30(a29)),f34(a45,a37)),f34(f33(a45,f30(a29)),f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[736,769,1261,1405,604,1812,663,1120,1134,674,2,311,87,82,84,3])). % 59.58/59.61 cnf(1832,plain, % 59.58/59.61 (~P7(f34(a51,f32(a52,f40(a52))),f39(f33(f33(a45,f30(a29)),f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[736,769,1261,1405,604,1812,663,1120,1134,1807,553,674,2,311,87,82,84,3,172])). % 59.58/59.61 cnf(1836,plain, % 59.58/59.61 (P7(f34(a45,a37),f39(f33(f33(a45,f30(a29)),f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[736,769,1261,1405,604,1829,1812,663,1120,630,1134,1807,553,674,2,311,87,82,84,3,172,330,207])). % 59.58/59.61 cnf(1837,plain, % 59.58/59.61 (~P3(x18371,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1840,plain, % 59.58/59.61 (~P3(x18401,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1842,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f39(f33(f33(a45,f30(a29)),f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[736,769,1261,1405,604,1829,1837,1812,663,1120,708,630,1134,986,1244,1807,553,674,2,311,87,82,84,3,172,330,207,292,221])). % 59.58/59.61 cnf(1844,plain, % 59.58/59.61 (E(f39(f33(f33(f33(a45,f30(a29)),f30(a29)),f34(a45,a37))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[736,769,1261,1405,604,1829,1837,1812,663,1120,708,630,1134,986,1244,1807,553,674,2,311,87,82,84,3,172,330,207,292,221,319])). % 59.58/59.61 cnf(1846,plain, % 59.58/59.61 (P1(f34(f33(f33(a45,f30(a29)),f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[736,769,1261,1405,604,1829,1837,1812,663,1120,708,630,1134,986,1244,1807,553,674,2,311,87,82,84,3,172,330,207,292,221,319,317])). % 59.58/59.61 cnf(1848,plain, % 59.58/59.61 (P2(f33(f33(f33(a45,f30(a29)),f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[736,769,1261,1405,604,1829,1837,1812,663,1120,708,630,1134,986,1244,1807,553,674,2,311,87,82,84,3,172,330,207,292,221,319,317,318])). % 59.58/59.61 cnf(1852,plain, % 59.58/59.61 (~P3(x18521,f34(a45,a37))), % 59.58/59.61 inference(rename_variables,[],[604])). % 59.58/59.61 cnf(1854,plain, % 59.58/59.61 (P1(f39(f33(f33(f33(a45,f30(a29)),f30(a29)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[736,769,1261,1156,1405,604,1829,1837,1840,1812,663,1120,708,630,1134,598,986,1244,1807,553,674,113,2,311,87,82,84,3,172,330,207,292,221,319,317,318,83,335,204])). % 59.58/59.61 cnf(1856,plain, % 59.58/59.61 (E(f33(f33(f33(a45,f30(a29)),f30(a29)),f34(a45,a37)),f33(f33(a45,f30(a29)),f34(a45,a37)))), % 59.58/59.61 inference(scs_inference,[],[736,769,1261,1156,832,1405,604,1829,1837,1840,1852,1812,663,1120,708,630,1134,598,986,1244,1807,553,674,704,113,2,311,87,82,84,3,172,330,207,292,221,319,317,318,83,335,204,263])). % 59.58/59.61 cnf(1859,plain, % 59.58/59.61 (E(f34(f33(f33(a45,f30(a29)),f30(a29)),f34(a45,a37)),a37)), % 59.58/59.61 inference(scs_inference,[],[736,769,1261,1156,832,1405,604,1829,1837,1840,1852,1812,663,1120,708,630,1134,598,986,1244,1807,553,674,704,113,2,311,87,82,84,3,172,330,207,292,221,319,317,318,83,335,204,263,152])). % 59.58/59.61 cnf(1879,plain, % 59.58/59.61 (~P3(x18791,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(1881,plain, % 59.58/59.61 (~E(f30(f43(f12(a45,a37,a41))),a37)), % 59.58/59.61 inference(scs_inference,[],[736,727,658,679,1856,1553,1828,1859,663,1854,1846,1844,1842,1244,659,2,144,317,311,318,83,82,84,3])). % 59.58/59.61 cnf(1883,plain, % 59.58/59.61 (~P3(x18831,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(1885,plain, % 59.58/59.61 (P7(f34(a45,f30(a29)),f39(f33(f33(f33(a45,f30(a29)),f30(a29)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[736,727,658,679,1879,1883,1856,1553,1828,1859,663,1854,1846,708,1844,1842,1244,659,2,144,317,311,318,83,82,84,3,335,207])). % 59.58/59.61 cnf(1886,plain, % 59.58/59.61 (~P3(x18861,f34(a45,f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[679])). % 59.58/59.61 cnf(1891,plain, % 59.58/59.61 (P7(f34(a45,a37),f39(f33(f33(f33(a45,f30(a29)),f30(a29)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[736,727,658,679,1879,1883,1886,1856,1553,1828,1859,663,1854,1846,708,630,1039,1844,1842,1244,659,2,144,317,311,318,83,82,84,3,335,207,292,221])). % 59.58/59.61 cnf(1893,plain, % 59.58/59.61 (E(f39(f33(f33(f33(f33(a45,f30(a29)),f30(a29)),f34(a45,a37)),f34(a45,a37))),f34(a45,a37))), % 59.58/59.61 inference(scs_inference,[],[736,727,658,679,1879,1883,1886,1856,1553,1828,1859,663,1854,1846,708,630,1039,1844,1848,1842,1244,659,2,144,317,311,318,83,82,84,3,335,207,292,221,319])). % 59.58/59.61 cnf(1896,plain, % 59.58/59.61 (P1(f39(f33(f33(f33(f33(a45,f30(a29)),f30(a29)),f34(a45,a37)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[736,727,658,1156,679,1879,1883,1886,1856,1553,1828,1859,663,1854,1846,708,630,598,1039,1844,1848,1842,1244,659,113,2,144,317,311,318,83,82,84,3,335,207,292,221,319,87,204])). % 59.58/59.61 cnf(1906,plain, % 59.58/59.61 (P1(f34(f33(f33(f33(a45,f30(a29)),f30(a29)),f34(a45,a37)),f34(a45,f30(a29))))), % 59.58/59.61 inference(scs_inference,[],[1859,1885,1848,2,317])). % 59.58/59.61 cnf(1915,plain, % 59.58/59.61 (~P3(x19151,f34(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[1147])). % 59.58/59.61 cnf(1921,plain, % 59.58/59.61 (P7(f34(f33(a45,f30(a29)),f30(a29)),f39(f33(f33(f33(f33(a45,f30(a29)),f30(a29)),f34(a45,a37)),f34(a45,a37))))), % 59.58/59.61 inference(scs_inference,[],[736,917,938,1147,1915,604,1859,1836,1885,1881,1896,1242,1893,1891,1832,1848,659,106,2,317,311,318,87,83,82,84,3,335,207])). % 59.58/59.61 cnf(1944,plain, % 59.58/59.61 (~P3(x19441,f34(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[1147])). % 59.58/59.61 cnf(1951,plain, % 59.58/59.61 (~P3(x19511,f34(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[1147])). % 59.58/59.61 cnf(1954,plain, % 59.58/59.61 (~P3(x19541,f34(f33(a45,f30(a29)),f30(a29)))), % 59.58/59.61 inference(rename_variables,[],[1147])). % 59.58/59.61 cnf(1959,plain, % 59.58/59.61 (P3(f12(f33(f33(a45,f30(a29)),f34(a45,a37)),f34(f33(a45,f30(a29)),f30(a29)),a41),a41)), % 59.58/59.61 inference(scs_inference,[],[736,727,832,1420,480,1147,1944,1951,1954,604,1393,1831,1885,694,1921,304,1906,1242,101,1893,1891,1848,869,704,2,317,311,318,82,84,3,335,207,292,263,282])). % 59.58/59.61 cnf(4132,plain, % 59.58/59.61 ($false), % 59.58/59.61 inference(scs_inference,[],[93,346,352,1959,595,120,148,146,153,154,156,151,168,169,150,163,164,165,166,178,179,4,6,8,31,32,48,56,61,62,66,76,77,155,188,9,11,12,13,14,15,16,26,27,33,34,35,36,46,47,49,50,51,52,57,58,59,60,70,71,78,79,167,17,18,19,20,21,22,23,24,25,28,29,30,37,38,39,40,41,42,43,44,45,53,54,55,63,64,65,67,68,69,208,72,73,74,75,190,226]), % 59.58/59.61 ['proof']). % 59.58/59.61 % SZS output end Proof % 59.58/59.61 % Total time :58.860000s %------------------------------------------------------------------------------