%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM544+2 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n029.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 12:24:56 EDT 2024 % Result : Theorem 58.77s 58.83s % Output : CNFRefutation 58.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM544+2 : TPTP v8.2.0. Released v4.0.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n029.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Sat Jun 22 19:02:39 EDT 2024 % 0.11/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 58.77/58.80 %------------------------------------------- % 58.77/58.80 % File :CSE---1.7 % 58.77/58.80 % Problem :theBenchmark % 58.77/58.80 % Transform :cnf % 58.77/58.80 % Format :tptp:raw % 58.77/58.80 % Command :java -jar mcs_scs.jar %d %s % 58.77/58.80 % 58.77/58.80 % Result :Theorem 58.180000s % 58.77/58.80 % Output :CNFRefutation 58.180000s % 58.77/58.80 %------------------------------------------- % 58.77/58.81 %------------------------------------------------------------------------------ % 58.77/58.81 % File : NUM544+2 : TPTP v8.2.0. Released v4.0.0. % 58.77/58.81 % Domain : Number Theory % 58.77/58.81 % Problem : Ramsey's Infinite Theorem 11_01, 01 expansion % 58.77/58.81 % Version : Especial. % 58.77/58.81 % English : % 58.77/58.81 % 58.77/58.81 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 58.77/58.81 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 58.77/58.81 % Source : [Pas08] % 58.77/58.81 % Names : ramsey_11_01.01 [Pas08] % 58.77/58.81 % 58.77/58.81 % Status : Theorem % 58.77/58.81 % Rating : 0.22 v8.2.0, 0.25 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.10 v7.3.0, 0.14 v7.1.0, 0.17 v6.4.0, 0.27 v6.3.0, 0.17 v6.2.0, 0.24 v6.1.0, 0.27 v6.0.0, 0.17 v5.5.0, 0.44 v5.4.0, 0.50 v5.3.0, 0.52 v5.2.0, 0.35 v5.1.0, 0.48 v5.0.0, 0.54 v4.1.0, 0.65 v4.0.1, 0.87 v4.0.0 % 58.77/58.81 % Syntax : Number of formulae : 56 ( 3 unt; 7 def) % 58.77/58.81 % Number of atoms : 219 ( 32 equ) % 58.77/58.81 % Maximal formula atoms : 12 ( 3 avg) % 58.77/58.81 % Number of connectives : 178 ( 15 ~; 6 |; 60 &) % 58.77/58.81 % ( 16 <=>; 81 =>; 0 <=; 0 <~>) % 58.77/58.81 % Maximal formula depth : 12 ( 5 avg) % 58.77/58.81 % Maximal term depth : 4 ( 1 avg) % 58.77/58.81 % Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty) % 58.77/58.81 % Number of functors : 11 ( 11 usr; 4 con; 0-2 aty) % 58.77/58.81 % Number of variables : 98 ( 94 !; 4 ?) % 58.77/58.81 % SPC : FOF_THM_RFO_SEQ % 58.77/58.81 % 58.77/58.81 % Comments : Problem generated by the SAD system [VLP07] % 58.77/58.81 %------------------------------------------------------------------------------ % 58.77/58.81 fof(mSetSort,axiom, % 58.77/58.81 ! [W0] : % 58.77/58.81 ( aSet0(W0) % 58.77/58.81 => $true ) ). % 58.77/58.81 % 58.77/58.81 fof(mElmSort,axiom, % 58.77/58.81 ! [W0] : % 58.77/58.81 ( aElement0(W0) % 58.77/58.81 => $true ) ). % 58.77/58.81 % 58.77/58.81 fof(mEOfElem,axiom, % 58.77/58.81 ! [W0] : % 58.77/58.81 ( aSet0(W0) % 58.77/58.81 => ! [W1] : % 58.77/58.81 ( aElementOf0(W1,W0) % 58.77/58.81 => aElement0(W1) ) ) ). % 58.77/58.81 % 58.77/58.81 fof(mFinRel,axiom, % 58.77/58.81 ! [W0] : % 58.77/58.81 ( aSet0(W0) % 58.77/58.81 => ( isFinite0(W0) % 58.77/58.81 => $true ) ) ). % 58.77/58.81 % 58.77/58.81 fof(mDefEmp,definition, % 58.77/58.81 ! [W0] : % 58.77/58.81 ( W0 = slcrc0 % 58.77/58.81 <=> ( aSet0(W0) % 58.77/58.81 & ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 58.77/58.81 % 58.77/58.81 fof(mEmpFin,axiom, % 58.77/58.81 isFinite0(slcrc0) ). % 58.77/58.81 % 58.77/58.81 fof(mCntRel,axiom, % 58.77/58.81 ! [W0] : % 58.77/58.81 ( aSet0(W0) % 58.77/58.81 => ( isCountable0(W0) % 58.77/58.81 => $true ) ) ). % 58.77/58.81 % 58.77/58.81 fof(mCountNFin,axiom, % 58.77/58.81 ! [W0] : % 58.77/58.81 ( ( aSet0(W0) % 58.77/58.81 & isCountable0(W0) ) % 58.77/58.81 => ~ isFinite0(W0) ) ). % 58.77/58.81 % 58.77/58.81 fof(mCountNFin_01,axiom, % 58.77/58.81 ! [W0] : % 58.77/58.81 ( ( aSet0(W0) % 58.77/58.81 & isCountable0(W0) ) % 58.77/58.81 => W0 != slcrc0 ) ). % 58.77/58.81 % 58.77/58.81 fof(mDefSub,definition, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aSet0(W0) % 58.77/58.82 => ! [W1] : % 58.77/58.82 ( aSubsetOf0(W1,W0) % 58.77/58.82 <=> ( aSet0(W1) % 58.77/58.82 & ! [W2] : % 58.77/58.82 ( aElementOf0(W2,W1) % 58.77/58.82 => aElementOf0(W2,W0) ) ) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mSubFSet,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( ( aSet0(W0) % 58.77/58.82 & isFinite0(W0) ) % 58.77/58.82 => ! [W1] : % 58.77/58.82 ( aSubsetOf0(W1,W0) % 58.77/58.82 => isFinite0(W1) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mSubRefl,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aSet0(W0) % 58.77/58.82 => aSubsetOf0(W0,W0) ) ). % 58.77/58.82 % 58.77/58.82 fof(mSubASymm,axiom, % 58.77/58.82 ! [W0,W1] : % 58.77/58.82 ( ( aSet0(W0) % 58.77/58.82 & aSet0(W1) ) % 58.77/58.82 => ( ( aSubsetOf0(W0,W1) % 58.77/58.82 & aSubsetOf0(W1,W0) ) % 58.77/58.82 => W0 = W1 ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mSubTrans,axiom, % 58.77/58.82 ! [W0,W1,W2] : % 58.77/58.82 ( ( aSet0(W0) % 58.77/58.82 & aSet0(W1) % 58.77/58.82 & aSet0(W2) ) % 58.77/58.82 => ( ( aSubsetOf0(W0,W1) % 58.77/58.82 & aSubsetOf0(W1,W2) ) % 58.77/58.82 => aSubsetOf0(W0,W2) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mDefCons,definition, % 58.77/58.82 ! [W0,W1] : % 58.77/58.82 ( ( aSet0(W0) % 58.77/58.82 & aElement0(W1) ) % 58.77/58.82 => ! [W2] : % 58.77/58.82 ( W2 = sdtpldt0(W0,W1) % 58.77/58.82 <=> ( aSet0(W2) % 58.77/58.82 & ! [W3] : % 58.77/58.82 ( aElementOf0(W3,W2) % 58.77/58.82 <=> ( aElement0(W3) % 58.77/58.82 & ( aElementOf0(W3,W0) % 58.77/58.82 | W3 = W1 ) ) ) ) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mDefDiff,definition, % 58.77/58.82 ! [W0,W1] : % 58.77/58.82 ( ( aSet0(W0) % 58.77/58.82 & aElement0(W1) ) % 58.77/58.82 => ! [W2] : % 58.77/58.82 ( W2 = sdtmndt0(W0,W1) % 58.77/58.82 <=> ( aSet0(W2) % 58.77/58.82 & ! [W3] : % 58.77/58.82 ( aElementOf0(W3,W2) % 58.77/58.82 <=> ( aElement0(W3) % 58.77/58.82 & aElementOf0(W3,W0) % 58.77/58.82 & W3 != W1 ) ) ) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mConsDiff,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aSet0(W0) % 58.77/58.82 => ! [W1] : % 58.77/58.82 ( aElementOf0(W1,W0) % 58.77/58.82 => sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mDiffCons,axiom, % 58.77/58.82 ! [W0,W1] : % 58.77/58.82 ( ( aElement0(W0) % 58.77/58.82 & aSet0(W1) ) % 58.77/58.82 => ( ~ aElementOf0(W0,W1) % 58.77/58.82 => sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mCConsSet,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aElement0(W0) % 58.77/58.82 => ! [W1] : % 58.77/58.82 ( ( aSet0(W1) % 58.77/58.82 & isCountable0(W1) ) % 58.77/58.82 => isCountable0(sdtpldt0(W1,W0)) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mCDiffSet,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aElement0(W0) % 58.77/58.82 => ! [W1] : % 58.77/58.82 ( ( aSet0(W1) % 58.77/58.82 & isCountable0(W1) ) % 58.77/58.82 => isCountable0(sdtmndt0(W1,W0)) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mFConsSet,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aElement0(W0) % 58.77/58.82 => ! [W1] : % 58.77/58.82 ( ( aSet0(W1) % 58.77/58.82 & isFinite0(W1) ) % 58.77/58.82 => isFinite0(sdtpldt0(W1,W0)) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mFDiffSet,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aElement0(W0) % 58.77/58.82 => ! [W1] : % 58.77/58.82 ( ( aSet0(W1) % 58.77/58.82 & isFinite0(W1) ) % 58.77/58.82 => isFinite0(sdtmndt0(W1,W0)) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mNATSet,axiom, % 58.77/58.82 ( aSet0(szNzAzT0) % 58.77/58.82 & isCountable0(szNzAzT0) ) ). % 58.77/58.82 % 58.77/58.82 fof(mZeroNum,axiom, % 58.77/58.82 aElementOf0(sz00,szNzAzT0) ). % 58.77/58.82 % 58.77/58.82 fof(mSuccNum,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 => ( aElementOf0(szszuzczcdt0(W0),szNzAzT0) % 58.77/58.82 & szszuzczcdt0(W0) != sz00 ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mSuccEquSucc,axiom, % 58.77/58.82 ! [W0,W1] : % 58.77/58.82 ( ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 & aElementOf0(W1,szNzAzT0) ) % 58.77/58.82 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 58.77/58.82 => W0 = W1 ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mNatExtra,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 => ( W0 = sz00 % 58.77/58.82 | ? [W1] : % 58.77/58.82 ( aElementOf0(W1,szNzAzT0) % 58.77/58.82 & W0 = szszuzczcdt0(W1) ) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mNatNSucc,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 => W0 != szszuzczcdt0(W0) ) ). % 58.77/58.82 % 58.77/58.82 fof(mLessRel,axiom, % 58.77/58.82 ! [W0,W1] : % 58.77/58.82 ( ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 & aElementOf0(W1,szNzAzT0) ) % 58.77/58.82 => ( sdtlseqdt0(W0,W1) % 58.77/58.82 => $true ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mZeroLess,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 => sdtlseqdt0(sz00,W0) ) ). % 58.77/58.82 % 58.77/58.82 fof(mNoScLessZr,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 => ~ sdtlseqdt0(szszuzczcdt0(W0),sz00) ) ). % 58.77/58.82 % 58.77/58.82 fof(mSuccLess,axiom, % 58.77/58.82 ! [W0,W1] : % 58.77/58.82 ( ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 & aElementOf0(W1,szNzAzT0) ) % 58.77/58.82 => ( sdtlseqdt0(W0,W1) % 58.77/58.82 <=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mLessSucc,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 => sdtlseqdt0(W0,szszuzczcdt0(W0)) ) ). % 58.77/58.82 % 58.77/58.82 fof(mLessRefl,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 => sdtlseqdt0(W0,W0) ) ). % 58.77/58.82 % 58.77/58.82 fof(mLessASymm,axiom, % 58.77/58.82 ! [W0,W1] : % 58.77/58.82 ( ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 & aElementOf0(W1,szNzAzT0) ) % 58.77/58.82 => ( ( sdtlseqdt0(W0,W1) % 58.77/58.82 & sdtlseqdt0(W1,W0) ) % 58.77/58.82 => W0 = W1 ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mLessTrans,axiom, % 58.77/58.82 ! [W0,W1,W2] : % 58.77/58.82 ( ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 & aElementOf0(W1,szNzAzT0) % 58.77/58.82 & aElementOf0(W2,szNzAzT0) ) % 58.77/58.82 => ( ( sdtlseqdt0(W0,W1) % 58.77/58.82 & sdtlseqdt0(W1,W2) ) % 58.77/58.82 => sdtlseqdt0(W0,W2) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mLessTotal,axiom, % 58.77/58.82 ! [W0,W1] : % 58.77/58.82 ( ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 & aElementOf0(W1,szNzAzT0) ) % 58.77/58.82 => ( sdtlseqdt0(W0,W1) % 58.77/58.82 | sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mIHSort,axiom, % 58.77/58.82 ! [W0,W1] : % 58.77/58.82 ( ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 & aElementOf0(W1,szNzAzT0) ) % 58.77/58.82 => ( iLess0(W0,W1) % 58.77/58.82 => $true ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mIH,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aElementOf0(W0,szNzAzT0) % 58.77/58.82 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 58.77/58.82 % 58.77/58.82 fof(mCardS,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aSet0(W0) % 58.77/58.82 => aElement0(sbrdtbr0(W0)) ) ). % 58.77/58.82 % 58.77/58.82 fof(mCardNum,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aSet0(W0) % 58.77/58.82 => ( aElementOf0(sbrdtbr0(W0),szNzAzT0) % 58.77/58.82 <=> isFinite0(W0) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mCardEmpty,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aSet0(W0) % 58.77/58.82 => ( sbrdtbr0(W0) = sz00 % 58.77/58.82 <=> W0 = slcrc0 ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mCardCons,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( ( aSet0(W0) % 58.77/58.82 & isFinite0(W0) ) % 58.77/58.82 => ! [W1] : % 58.77/58.82 ( aElement0(W1) % 58.77/58.82 => ( ~ aElementOf0(W1,W0) % 58.77/58.82 => sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ) ). % 58.77/58.82 % 58.77/58.82 fof(mCardDiff,axiom, % 58.77/58.82 ! [W0] : % 58.77/58.82 ( aSet0(W0) % 58.77/58.82 => ! [W1] : % 58.77/58.82 ( ( isFinite0(W0) % 58.77/58.82 & aElementOf0(W1,W0) ) % 58.77/58.83 => szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ) ). % 58.77/58.83 % 58.77/58.83 fof(mCardSub,axiom, % 58.77/58.83 ! [W0] : % 58.77/58.83 ( aSet0(W0) % 58.77/58.83 => ! [W1] : % 58.77/58.83 ( ( isFinite0(W0) % 58.77/58.83 & aSubsetOf0(W1,W0) ) % 58.77/58.83 => sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 58.77/58.83 % 58.77/58.83 fof(mCardSubEx,axiom, % 58.77/58.83 ! [W0,W1] : % 58.77/58.83 ( ( aSet0(W0) % 58.77/58.83 & aElementOf0(W1,szNzAzT0) ) % 58.77/58.83 => ( ( isFinite0(W0) % 58.77/58.83 & sdtlseqdt0(W1,sbrdtbr0(W0)) ) % 58.77/58.83 => ? [W2] : % 58.77/58.83 ( aSubsetOf0(W2,W0) % 58.77/58.83 & sbrdtbr0(W2) = W1 ) ) ) ). % 58.77/58.83 % 58.77/58.83 fof(mDefMin,definition, % 58.77/58.83 ! [W0] : % 58.77/58.83 ( ( aSubsetOf0(W0,szNzAzT0) % 58.77/58.83 & W0 != slcrc0 ) % 58.77/58.83 => ! [W1] : % 58.77/58.83 ( W1 = szmzizndt0(W0) % 58.77/58.83 <=> ( aElementOf0(W1,W0) % 58.77/58.83 & ! [W2] : % 58.77/58.83 ( aElementOf0(W2,W0) % 58.77/58.83 => sdtlseqdt0(W1,W2) ) ) ) ) ). % 58.77/58.83 % 58.77/58.83 fof(mDefMax,definition, % 58.77/58.83 ! [W0] : % 58.77/58.83 ( ( aSubsetOf0(W0,szNzAzT0) % 58.77/58.83 & isFinite0(W0) % 58.77/58.83 & W0 != slcrc0 ) % 58.77/58.83 => ! [W1] : % 58.77/58.83 ( W1 = szmzazxdt0(W0) % 58.77/58.83 <=> ( aElementOf0(W1,W0) % 58.77/58.83 & ! [W2] : % 58.77/58.83 ( aElementOf0(W2,W0) % 58.77/58.83 => sdtlseqdt0(W2,W1) ) ) ) ) ). % 58.77/58.83 % 58.77/58.83 fof(mMinMin,axiom, % 58.77/58.83 ! [W0,W1] : % 58.77/58.83 ( ( aSubsetOf0(W0,szNzAzT0) % 58.77/58.83 & aSubsetOf0(W1,szNzAzT0) % 58.77/58.83 & W0 != slcrc0 % 58.77/58.83 & W1 != slcrc0 ) % 58.77/58.83 => ( ( aElementOf0(szmzizndt0(W0),W1) % 58.77/58.83 & aElementOf0(szmzizndt0(W1),W0) ) % 58.77/58.83 => szmzizndt0(W0) = szmzizndt0(W1) ) ) ). % 58.77/58.83 % 58.77/58.83 fof(mDefSeg,definition, % 58.77/58.83 ! [W0] : % 58.77/58.83 ( aElementOf0(W0,szNzAzT0) % 58.77/58.83 => ! [W1] : % 58.77/58.83 ( W1 = slbdtrb0(W0) % 58.77/58.83 <=> ( aSet0(W1) % 58.77/58.83 & ! [W2] : % 58.77/58.83 ( aElementOf0(W2,W1) % 58.77/58.83 <=> ( aElementOf0(W2,szNzAzT0) % 58.77/58.83 & sdtlseqdt0(szszuzczcdt0(W2),W0) ) ) ) ) ) ). % 58.77/58.83 % 58.77/58.83 fof(mSegFin,axiom, % 58.77/58.83 ! [W0] : % 58.77/58.83 ( aElementOf0(W0,szNzAzT0) % 58.77/58.83 => isFinite0(slbdtrb0(W0)) ) ). % 58.77/58.83 % 58.77/58.83 fof(mSegZero,axiom, % 58.77/58.83 slbdtrb0(sz00) = slcrc0 ). % 58.77/58.83 % 58.77/58.83 fof(mSegSucc,axiom, % 58.77/58.83 ! [W0,W1] : % 58.77/58.83 ( ( aElementOf0(W0,szNzAzT0) % 58.77/58.83 & aElementOf0(W1,szNzAzT0) ) % 58.77/58.83 => ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1))) % 58.77/58.83 <=> ( aElementOf0(W0,slbdtrb0(W1)) % 58.77/58.83 | W0 = W1 ) ) ) ). % 58.77/58.83 % 58.77/58.83 fof(mSegLess,axiom, % 58.77/58.83 ! [W0,W1] : % 58.77/58.83 ( ( aElementOf0(W0,szNzAzT0) % 58.77/58.83 & aElementOf0(W1,szNzAzT0) ) % 58.77/58.83 => ( sdtlseqdt0(W0,W1) % 58.77/58.83 <=> aSubsetOf0(slbdtrb0(W0),slbdtrb0(W1)) ) ) ). % 58.77/58.83 % 58.77/58.83 fof(m__1986,hypothesis, % 58.77/58.83 ( aSet0(xS) % 58.77/58.83 & ! [W0] : % 58.77/58.83 ( aElementOf0(W0,xS) % 58.77/58.83 => aElementOf0(W0,szNzAzT0) ) % 58.77/58.83 & aSubsetOf0(xS,szNzAzT0) % 58.77/58.83 & isFinite0(xS) ) ). % 58.77/58.83 % 58.77/58.83 fof(m__,conjecture, % 58.77/58.83 ( ~ ( ~ ? [W0] : aElementOf0(W0,xS) % 58.77/58.83 | xS = slcrc0 ) % 58.77/58.83 => ( ( aElementOf0(szmzazxdt0(xS),xS) % 58.77/58.83 & ! [W0] : % 58.77/58.83 ( aElementOf0(W0,xS) % 58.77/58.83 => sdtlseqdt0(W0,szmzazxdt0(xS)) ) ) % 58.77/58.83 => ( ( aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) % 58.77/58.83 & ! [W0] : % 58.77/58.83 ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) % 58.77/58.83 <=> ( aElementOf0(W0,szNzAzT0) % 58.77/58.83 & sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))) ) ) ) % 58.77/58.83 => ( ! [W0] : % 58.77/58.83 ( aElementOf0(W0,xS) % 58.77/58.83 => aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ) % 58.77/58.83 | aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ) ) ) ) ). % 58.77/58.83 % 58.77/58.83 %------------------------------------------------------------------------------ % 58.77/58.83 %------------------------------------------- % 58.77/58.83 % Proof found % 58.77/58.83 % SZS status Theorem for theBenchmark % 58.77/58.83 % SZS output start Proof % 58.77/58.83 %ClaNum:148(EqnAxiom:42) % 58.77/58.83 %VarNum:618(SingletonVarNum:190) % 58.77/58.83 %MaxLitNum:8 % 58.77/58.83 %MaxfuncDepth:3 % 58.77/58.83 %SharedTerms:25 % 58.77/58.83 %goalClause: 50 51 53 54 55 56 57 78 116 128 135 % 58.77/58.83 %singleGoalClaCount:7 % 58.77/58.83 [44]P1(a18) % 58.77/58.83 [45]P1(a19) % 58.77/58.83 [46]P4(a17) % 58.77/58.83 [47]P4(a19) % 58.77/58.83 [48]P5(a18) % 58.77/58.83 [49]P2(a1,a18) % 58.77/58.83 [50]P2(a3,a19) % 58.77/58.83 [51]P2(a4,a19) % 58.77/58.83 [52]P6(a19,a18) % 58.77/58.83 [55]~E(a19,a17) % 58.77/58.83 [43]E(f2(a1),a17) % 58.77/58.83 [53]P2(f20(a19),a19) % 58.77/58.83 [54]P1(f2(f21(f20(a19)))) % 58.77/58.83 [56]~P2(a4,f2(f21(f20(a19)))) % 58.77/58.83 [57]~P6(a19,f2(f21(f20(a19)))) % 58.77/58.83 [58]P1(x581)+~E(x581,a17) % 58.77/58.83 [64]~P1(x641)+P6(x641,x641) % 58.77/58.83 [70]~P2(x701,a19)+P2(x701,a18) % 58.77/58.83 [71]~P2(x711,a18)+P8(a1,x711) % 58.77/58.83 [77]P8(x771,x771)+~P2(x771,a18) % 58.77/58.83 [62]~P1(x621)+P3(f5(x621)) % 58.77/58.83 [66]~P2(x661,a18)+~E(f21(x661),a1) % 58.77/58.83 [67]~P2(x671,a18)+~E(f21(x671),x671) % 58.77/58.83 [69]~P2(x691,a18)+P4(f2(x691)) % 58.77/58.83 [78]~P2(x781,a19)+P8(x781,f20(a19)) % 58.77/58.83 [79]~P2(x791,a18)+P2(f21(x791),a18) % 58.77/58.83 [80]~P2(x801,a18)+P8(x801,f21(x801)) % 58.77/58.83 [81]~P2(x811,a18)+P7(x811,f21(x811)) % 58.77/58.83 [88]~P2(x881,a18)+~P8(f21(x881),a1) % 58.77/58.83 [116]P2(x1161,a18)+~P2(x1161,f2(f21(f20(a19)))) % 58.77/58.83 [128]P8(f21(x1281),f21(f20(a19)))+~P2(x1281,f2(f21(f20(a19)))) % 58.77/58.83 [65]~P2(x652,x651)+~E(x651,a17) % 58.77/58.83 [61]~P1(x611)+~P5(x611)+~E(x611,a17) % 58.77/58.83 [63]~P4(x631)+~P5(x631)+~P1(x631) % 58.77/58.83 [59]~P1(x591)+~E(x591,a17)+E(f5(x591),a1) % 58.77/58.83 [60]~P1(x601)+E(x601,a17)+~E(f5(x601),a1) % 58.77/58.83 [68]~P1(x681)+P2(f6(x681),x681)+E(x681,a17) % 58.77/58.83 [74]~P1(x741)+~P4(x741)+P2(f5(x741),a18) % 58.77/58.83 [82]~P2(x821,a18)+E(x821,a1)+P2(f7(x821),a18) % 58.77/58.83 [83]~P1(x831)+P4(x831)+~P2(f5(x831),a18) % 58.77/58.83 [72]~P2(x721,a18)+E(x721,a1)+E(f21(f7(x721)),x721) % 58.77/58.83 [135]~P2(x1351,a18)+~P8(f21(x1351),f21(f20(a19)))+P2(x1351,f2(f21(f20(a19)))) % 58.77/58.83 [75]~P6(x751,x752)+P1(x751)+~P1(x752) % 58.77/58.83 [76]~P2(x761,x762)+P3(x761)+~P1(x762) % 58.77/58.83 [73]P1(x731)+~P2(x732,a18)+~E(x731,f2(x732)) % 58.77/58.83 [106]~P1(x1061)+~P2(x1062,x1061)+E(f15(f16(x1061,x1062),x1062),x1061) % 58.77/58.83 [84]~P4(x842)+~P6(x841,x842)+P4(x841)+~P1(x842) % 58.77/58.83 [87]P2(x872,x871)+~E(x872,f22(x871))+~P6(x871,a18)+E(x871,a17) % 58.77/58.83 [90]~P1(x901)+~P3(x902)+~P4(x901)+P4(f15(x901,x902)) % 58.77/58.83 [91]~P1(x911)+~P3(x912)+~P4(x911)+P4(f16(x911,x912)) % 58.77/58.83 [92]~P1(x921)+~P3(x922)+~P5(x921)+P5(f15(x921,x922)) % 58.77/58.83 [93]~P1(x931)+~P3(x932)+~P5(x931)+P5(f16(x931,x932)) % 58.77/58.83 [94]E(x941,x942)+~E(f21(x941),f21(x942))+~P2(x942,a18)+~P2(x941,a18) % 58.77/58.83 [97]~P1(x972)+~P4(x972)+~P6(x971,x972)+P8(f5(x971),f5(x972)) % 58.77/58.83 [104]~P1(x1041)+~P1(x1042)+P6(x1041,x1042)+P2(f8(x1042,x1041),x1041) % 58.77/58.83 [110]P8(x1101,x1102)+P8(f21(x1102),x1101)+~P2(x1102,a18)+~P2(x1101,a18) % 58.77/58.83 [119]~P8(x1191,x1192)+~P2(x1192,a18)+~P2(x1191,a18)+P6(f2(x1191),f2(x1192)) % 58.77/58.83 [120]~P8(x1201,x1202)+~P2(x1202,a18)+~P2(x1201,a18)+P8(f21(x1201),f21(x1202)) % 58.77/58.83 [122]~P1(x1221)+~P1(x1222)+P6(x1221,x1222)+~P2(f8(x1222,x1221),x1222) % 58.77/58.83 [124]P8(x1241,x1242)+~P2(x1242,a18)+~P2(x1241,a18)+~P6(f2(x1241),f2(x1242)) % 58.77/58.83 [125]P8(x1251,x1252)+~P2(x1252,a18)+~P2(x1251,a18)+~P8(f21(x1251),f21(x1252)) % 58.77/58.83 [105]P2(x1052,x1051)+~P1(x1051)+~P3(x1052)+E(f16(f15(x1051,x1052),x1052),x1051) % 58.77/58.83 [112]~E(x1121,x1122)+~P2(x1122,a18)+~P2(x1121,a18)+P2(x1121,f2(f21(x1122))) % 58.77/58.83 [130]~P2(x1302,a18)+~P2(x1301,a18)+~P2(x1301,f2(x1302))+P2(x1301,f2(f21(x1302))) % 58.77/58.83 [129]~P1(x1291)+~P4(x1291)+~P2(x1292,x1291)+E(f21(f5(f16(x1291,x1292))),f5(x1291)) % 58.77/58.83 [102]~P1(x1022)+~P6(x1023,x1022)+P2(x1021,x1022)+~P2(x1021,x1023) % 58.77/58.83 [85]~P1(x852)+~P3(x853)+P1(x851)+~E(x851,f15(x852,x853)) % 58.77/58.83 [86]~P1(x862)+~P3(x863)+P1(x861)+~E(x861,f16(x862,x863)) % 58.77/58.83 [98]~P2(x981,x982)+~P2(x983,a18)+P2(x981,a18)+~E(x982,f2(x983)) % 58.77/58.83 [107]~P2(x1071,x1073)+~P2(x1072,a18)+P8(f21(x1071),x1072)+~E(x1073,f2(x1072)) % 58.77/58.83 [95]~P1(x952)+~P1(x951)+~P6(x952,x951)+~P6(x951,x952)+E(x951,x952) % 58.77/58.83 [118]~P8(x1182,x1181)+~P8(x1181,x1182)+E(x1181,x1182)+~P2(x1182,a18)+~P2(x1181,a18) % 58.77/58.83 [89]~P4(x891)+P2(x892,x891)+~E(x892,f20(x891))+~P6(x891,a18)+E(x891,a17) % 58.77/58.83 [121]~P2(x1212,x1211)+P2(f11(x1211,x1212),x1211)+~P6(x1211,a18)+E(x1211,a17)+E(x1212,f22(x1211)) % 58.77/58.83 [131]~P1(x1311)+~P4(x1311)+~P2(x1312,a18)+~P8(x1312,f5(x1311))+P6(f12(x1311,x1312),x1311) % 58.77/58.83 [132]~P1(x1321)+P2(f14(x1322,x1321),x1321)+~P2(x1322,a18)+E(x1321,f2(x1322))+P2(f14(x1322,x1321),a18) % 58.77/58.83 [133]~P2(x1332,x1331)+~P6(x1331,a18)+~P8(x1332,f11(x1331,x1332))+E(x1331,a17)+E(x1332,f22(x1331)) % 58.77/58.83 [111]P2(x1112,x1111)+~P1(x1111)+~P3(x1112)+~P4(x1111)+E(f5(f15(x1111,x1112)),f21(f5(x1111))) % 58.77/58.83 [127]~P1(x1271)+~P4(x1271)+~P2(x1272,a18)+~P8(x1272,f5(x1271))+E(f5(f12(x1271,x1272)),x1272) % 58.77/58.83 [134]E(x1341,x1342)+P2(x1341,f2(x1342))+~P2(x1342,a18)+~P2(x1341,a18)+~P2(x1341,f2(f21(x1342))) % 58.77/58.83 [139]~P1(x1391)+P2(f14(x1392,x1391),x1391)+~P2(x1392,a18)+E(x1391,f2(x1392))+P8(f21(f14(x1392,x1391)),x1392) % 58.77/58.83 [103]~P2(x1033,x1031)+P8(x1032,x1033)+~E(x1032,f22(x1031))+~P6(x1031,a18)+E(x1031,a17) % 58.77/58.83 [123]P2(x1231,x1232)+~P2(x1233,a18)+~P2(x1231,a18)+~P8(f21(x1231),x1233)+~E(x1232,f2(x1233)) % 58.77/58.83 [99]~P1(x994)+~P3(x992)+~P2(x991,x993)+~E(x991,x992)+~E(x993,f16(x994,x992)) % 58.77/58.83 [100]~P1(x1003)+~P3(x1004)+~P2(x1001,x1002)+P3(x1001)+~E(x1002,f15(x1003,x1004)) % 58.77/58.83 [101]~P1(x1013)+~P3(x1014)+~P2(x1011,x1012)+P3(x1011)+~E(x1012,f16(x1013,x1014)) % 58.77/58.83 [109]~P1(x1092)+~P3(x1094)+~P2(x1091,x1093)+P2(x1091,x1092)+~E(x1093,f16(x1092,x1094)) % 58.77/58.83 [126]~P4(x1261)+~P2(x1262,x1261)+P2(f13(x1261,x1262),x1261)+~P6(x1261,a18)+E(x1261,a17)+E(x1262,f20(x1261)) % 58.77/58.83 [137]~P4(x1371)+~P2(x1372,x1371)+~P6(x1371,a18)+~P8(f13(x1371,x1372),x1372)+E(x1371,a17)+E(x1372,f20(x1371)) % 58.77/58.83 [143]~P1(x1431)+~P2(x1432,a18)+~P2(f14(x1432,x1431),x1431)+E(x1431,f2(x1432))+~P2(f14(x1432,x1431),a18)+~P8(f21(f14(x1432,x1431)),x1432) % 58.77/58.83 [114]~P1(x1142)+~P1(x1141)+~P6(x1143,x1142)+~P6(x1141,x1143)+P6(x1141,x1142)+~P1(x1143) % 58.77/58.83 [138]~P8(x1381,x1383)+P8(x1381,x1382)+~P8(x1383,x1382)+~P2(x1382,a18)+~P2(x1383,a18)+~P2(x1381,a18) % 58.77/58.83 [108]~P4(x1081)+~P2(x1082,x1081)+P8(x1082,x1083)+~E(x1083,f20(x1081))+~P6(x1081,a18)+E(x1081,a17) % 58.77/58.83 [140]~P1(x1401)+~P1(x1402)+~P3(x1403)+P2(f9(x1402,x1403,x1401),x1401)+~E(f9(x1402,x1403,x1401),x1403)+E(x1401,f16(x1402,x1403)) % 58.77/58.83 [141]~P1(x1411)+~P1(x1412)+~P3(x1413)+P2(f10(x1412,x1413,x1411),x1411)+E(x1411,f15(x1412,x1413))+P3(f10(x1412,x1413,x1411)) % 58.77/58.83 [142]~P1(x1421)+~P1(x1422)+~P3(x1423)+P2(f9(x1422,x1423,x1421),x1421)+E(x1421,f16(x1422,x1423))+P3(f9(x1422,x1423,x1421)) % 58.77/58.83 [144]~P1(x1441)+~P1(x1442)+~P3(x1443)+P2(f9(x1442,x1443,x1441),x1441)+P2(f9(x1442,x1443,x1441),x1442)+E(x1441,f16(x1442,x1443)) % 58.77/58.83 [96]~P1(x964)+~P3(x963)+~P3(x961)+P2(x961,x962)+~E(x961,x963)+~E(x962,f15(x964,x963)) % 58.77/58.83 [113]~P1(x1133)+~P3(x1132)+~P2(x1131,x1134)+E(x1131,x1132)+P2(x1131,x1133)+~E(x1134,f15(x1133,x1132)) % 58.77/58.83 [115]~P1(x1153)+~P3(x1154)+~P3(x1151)+~P2(x1151,x1153)+P2(x1151,x1152)+~E(x1152,f15(x1153,x1154)) % 58.77/58.83 [136]E(f22(x1362),f22(x1361))+~P6(x1361,a18)+~P6(x1362,a18)+~P2(f22(x1361),x1362)+~P2(f22(x1362),x1361)+E(x1361,a17)+E(x1362,a17) % 58.77/58.83 [145]~P1(x1451)+~P1(x1452)+~P3(x1453)+E(f10(x1452,x1453,x1451),x1453)+P2(f10(x1452,x1453,x1451),x1451)+P2(f10(x1452,x1453,x1451),x1452)+E(x1451,f15(x1452,x1453)) % 58.77/58.83 [146]~P1(x1461)+~P1(x1462)+~P3(x1463)+~E(f10(x1462,x1463,x1461),x1463)+~P2(f10(x1462,x1463,x1461),x1461)+E(x1461,f15(x1462,x1463))+~P3(f10(x1462,x1463,x1461)) % 58.77/58.83 [147]~P1(x1471)+~P1(x1472)+~P3(x1473)+~P2(f10(x1472,x1473,x1471),x1471)+~P2(f10(x1472,x1473,x1471),x1472)+E(x1471,f15(x1472,x1473))+~P3(f10(x1472,x1473,x1471)) % 58.77/58.83 [117]~P1(x1174)+~P3(x1172)+~P3(x1171)+~P2(x1171,x1174)+E(x1171,x1172)+P2(x1171,x1173)+~E(x1173,f16(x1174,x1172)) % 58.77/58.83 [148]~P1(x1481)+~P1(x1482)+~P3(x1483)+E(f9(x1482,x1483,x1481),x1483)+~P2(f9(x1482,x1483,x1481),x1481)+~P2(f9(x1482,x1483,x1481),x1482)+E(x1481,f16(x1482,x1483))+~P3(f9(x1482,x1483,x1481)) % 58.77/58.83 %EqnAxiom % 58.77/58.83 [1]E(x11,x11) % 58.77/58.83 [2]E(x22,x21)+~E(x21,x22) % 58.77/58.83 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.77/58.83 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 58.77/58.83 [5]~E(x51,x52)+E(f20(x51),f20(x52)) % 58.77/58.83 [6]~E(x61,x62)+E(f14(x61,x63),f14(x62,x63)) % 58.77/58.83 [7]~E(x71,x72)+E(f14(x73,x71),f14(x73,x72)) % 58.77/58.83 [8]~E(x81,x82)+E(f21(x81),f21(x82)) % 58.77/58.83 [9]~E(x91,x92)+E(f9(x91,x93,x94),f9(x92,x93,x94)) % 58.77/58.83 [10]~E(x101,x102)+E(f9(x103,x101,x104),f9(x103,x102,x104)) % 58.77/58.83 [11]~E(x111,x112)+E(f9(x113,x114,x111),f9(x113,x114,x112)) % 58.77/58.83 [12]~E(x121,x122)+E(f13(x121,x123),f13(x122,x123)) % 58.77/58.83 [13]~E(x131,x132)+E(f13(x133,x131),f13(x133,x132)) % 58.77/58.83 [14]~E(x141,x142)+E(f22(x141),f22(x142)) % 58.77/58.83 [15]~E(x151,x152)+E(f5(x151),f5(x152)) % 58.77/58.83 [16]~E(x161,x162)+E(f12(x161,x163),f12(x162,x163)) % 58.77/58.83 [17]~E(x171,x172)+E(f12(x173,x171),f12(x173,x172)) % 58.77/58.83 [18]~E(x181,x182)+E(f8(x181,x183),f8(x182,x183)) % 58.77/58.83 [19]~E(x191,x192)+E(f8(x193,x191),f8(x193,x192)) % 58.77/58.83 [20]~E(x201,x202)+E(f10(x201,x203,x204),f10(x202,x203,x204)) % 58.77/58.83 [21]~E(x211,x212)+E(f10(x213,x211,x214),f10(x213,x212,x214)) % 58.77/58.83 [22]~E(x221,x222)+E(f10(x223,x224,x221),f10(x223,x224,x222)) % 58.77/58.83 [23]~E(x231,x232)+E(f16(x231,x233),f16(x232,x233)) % 58.77/58.83 [24]~E(x241,x242)+E(f16(x243,x241),f16(x243,x242)) % 58.77/58.83 [25]~E(x251,x252)+E(f15(x251,x253),f15(x252,x253)) % 58.77/58.83 [26]~E(x261,x262)+E(f15(x263,x261),f15(x263,x262)) % 58.77/58.83 [27]~E(x271,x272)+E(f7(x271),f7(x272)) % 58.77/58.83 [28]~E(x281,x282)+E(f11(x281,x283),f11(x282,x283)) % 58.77/58.83 [29]~E(x291,x292)+E(f11(x293,x291),f11(x293,x292)) % 58.77/58.83 [30]~E(x301,x302)+E(f6(x301),f6(x302)) % 58.77/58.83 [31]~P1(x311)+P1(x312)+~E(x311,x312) % 58.77/58.83 [32]P2(x322,x323)+~E(x321,x322)+~P2(x321,x323) % 58.77/58.83 [33]P2(x333,x332)+~E(x331,x332)+~P2(x333,x331) % 58.77/58.83 [34]~P4(x341)+P4(x342)+~E(x341,x342) % 58.77/58.83 [35]P6(x352,x353)+~E(x351,x352)+~P6(x351,x353) % 58.77/58.83 [36]P6(x363,x362)+~E(x361,x362)+~P6(x363,x361) % 58.77/58.83 [37]~P5(x371)+P5(x372)+~E(x371,x372) % 58.77/58.83 [38]P8(x382,x383)+~E(x381,x382)+~P8(x381,x383) % 58.77/58.83 [39]P8(x393,x392)+~E(x391,x392)+~P8(x393,x391) % 58.77/58.83 [40]~P3(x401)+P3(x402)+~E(x401,x402) % 58.77/58.83 [41]P7(x412,x413)+~E(x411,x412)+~P7(x411,x413) % 58.77/58.83 [42]P7(x423,x422)+~E(x421,x422)+~P7(x423,x421) % 58.77/58.83 % 58.77/58.83 %------------------------------------------- % 58.77/58.83 cnf(149,plain, % 58.77/58.83 (P1(a17)), % 58.77/58.83 inference(equality_inference,[],[58])). % 58.77/58.83 cnf(150,plain, % 58.77/58.83 (~P1(a17)+E(f5(a17),a1)), % 58.77/58.83 inference(equality_inference,[],[59])). % 58.77/58.83 cnf(151,plain, % 58.77/58.83 (~P5(a17)+~P1(a17)), % 58.77/58.83 inference(equality_inference,[],[61])). % 58.77/58.83 cnf(152,plain, % 58.77/58.83 (~P2(x1521,a17)), % 58.77/58.83 inference(equality_inference,[],[65])). % 58.77/58.83 cnf(153,plain, % 58.77/58.83 (P1(f2(x1531))+~P2(x1531,a18)), % 58.77/58.83 inference(equality_inference,[],[73])). % 58.77/58.83 cnf(154,plain, % 58.77/58.83 (~P1(x1541)+~P3(x1542)+P1(f15(x1541,x1542))), % 58.77/58.83 inference(equality_inference,[],[85])). % 58.77/58.83 cnf(155,plain, % 58.77/58.83 (~P1(x1551)+~P3(x1552)+P1(f16(x1551,x1552))), % 58.77/58.83 inference(equality_inference,[],[86])). % 58.77/58.83 cnf(156,plain, % 58.77/58.83 (P2(f22(x1561),x1561)+~P6(x1561,a18)+E(x1561,a17)), % 58.77/58.83 inference(equality_inference,[],[87])). % 58.77/58.83 cnf(159,plain, % 58.77/58.83 (~P2(x1591,f2(x1592))+P2(x1591,a18)+~P2(x1592,a18)), % 58.77/58.83 inference(equality_inference,[],[98])). % 58.77/58.83 cnf(162,plain, % 58.77/58.83 (~P2(x1621,x1622)+P8(f22(x1622),x1621)+~P6(x1622,a18)+E(x1622,a17)), % 58.77/58.83 inference(equality_inference,[],[103])). % 58.77/58.83 cnf(163,plain, % 58.77/58.83 (~P2(x1631,f2(x1632))+P8(f21(x1631),x1632)+~P2(x1632,a18)), % 58.77/58.83 inference(equality_inference,[],[107])). % 58.77/58.83 cnf(164,plain, % 58.77/58.83 (~P4(x1641)+~P2(x1642,x1641)+P8(x1642,f20(x1641))+~P6(x1641,a18)+E(x1641,a17)), % 58.77/58.83 inference(equality_inference,[],[108])). % 58.77/58.83 cnf(165,plain, % 58.77/58.83 (P2(x1651,x1652)+~P1(x1652)+~P3(x1653)+~P2(x1651,f16(x1652,x1653))), % 58.77/58.83 inference(equality_inference,[],[109])). % 58.77/58.83 cnf(166,plain, % 58.77/58.83 (~P2(x1661,a18)+~P2(x1661,a18)+P2(x1661,f2(f21(x1661)))), % 58.77/58.83 inference(equality_inference,[],[112])). % 58.77/58.83 cnf(167,plain, % 58.77/58.83 (E(x1671,x1672)+P2(x1671,x1673)+~P1(x1673)+~P3(x1672)+~P2(x1671,f15(x1673,x1672))), % 58.77/58.83 inference(equality_inference,[],[113])). % 58.77/58.83 cnf(168,plain, % 58.77/58.83 (~P2(x1681,x1682)+~P1(x1682)+~P3(x1683)+P2(x1681,f15(x1682,x1683))+~P3(x1681)), % 58.77/58.83 inference(equality_inference,[],[115])). % 58.77/58.83 cnf(170,plain, % 58.77/58.83 (P2(x1701,f2(x1702))+~P2(x1701,a18)+~P8(f21(x1701),x1702)+~P2(x1702,a18)), % 58.77/58.83 inference(equality_inference,[],[123])). % 58.77/58.83 cnf(171,plain, % 58.77/58.83 (E(f5(a17),a1)), % 58.77/58.83 inference(scs_inference,[],[149,150])). % 58.77/58.83 cnf(172,plain, % 58.77/58.83 (~P5(a17)), % 58.77/58.83 inference(scs_inference,[],[149,151])). % 58.77/58.83 cnf(173,plain, % 58.77/58.83 (~P2(x1731,f2(a1))), % 58.77/58.83 inference(scs_inference,[],[43,65])). % 58.77/58.83 cnf(175,plain, % 58.77/58.83 (P1(f2(a1))), % 58.77/58.83 inference(scs_inference,[],[49,43,65,153])). % 58.77/58.83 cnf(177,plain, % 58.77/58.83 (P8(a1,a1)), % 58.77/58.83 inference(scs_inference,[],[49,43,65,153,77])). % 58.77/58.83 cnf(179,plain, % 58.77/58.83 (E(a17,f2(a1))), % 58.77/58.83 inference(scs_inference,[],[49,43,65,153,77,2])). % 58.77/58.83 cnf(182,plain, % 58.77/58.83 (P2(f22(a19),a19)), % 58.77/58.83 inference(scs_inference,[],[55,49,52,43,65,153,77,2,61,156])). % 58.77/58.83 cnf(184,plain, % 58.77/58.83 (P2(a1,f2(f21(a1)))), % 58.77/58.83 inference(scs_inference,[],[55,49,52,43,65,153,77,2,61,156,166])). % 58.77/58.83 cnf(187,plain, % 58.77/58.83 (~P4(a18)), % 58.77/58.83 inference(scs_inference,[],[51,55,56,44,48,49,52,43,65,153,77,2,61,156,166,33,63])). % 58.77/58.83 cnf(194,plain, % 58.77/58.83 (~P8(f21(a1),a1)), % 58.77/58.83 inference(scs_inference,[],[50,51,55,56,57,44,46,48,49,52,43,65,153,77,2,61,156,166,33,63,3,34,36,162,170])). % 58.77/58.83 cnf(196,plain, % 58.77/58.83 (P6(a17,f2(f21(f20(a19))))), % 58.77/58.83 inference(scs_inference,[],[50,51,55,56,57,54,152,44,46,48,49,52,149,43,65,153,77,2,61,156,166,33,63,3,34,36,162,170,104])). % 58.77/58.83 cnf(199,plain, % 58.77/58.83 (P6(f2(a1),f2(a1))), % 58.77/58.83 inference(scs_inference,[],[50,51,55,56,57,54,152,44,46,48,49,52,149,43,65,153,77,2,61,156,166,33,63,3,34,36,162,170,104,119])). % 58.77/58.83 cnf(201,plain, % 58.77/58.83 (P8(f21(a1),f21(a1))), % 58.77/58.83 inference(scs_inference,[],[50,51,55,56,57,54,152,44,46,48,49,52,149,43,65,153,77,2,61,156,166,33,63,3,34,36,162,170,104,119,120])). % 58.77/58.83 cnf(203,plain, % 58.77/58.83 (P8(a3,f20(a19))), % 58.77/58.83 inference(scs_inference,[],[50,51,55,56,57,54,152,44,46,47,48,49,52,149,43,65,153,77,2,61,156,166,33,63,3,34,36,162,170,104,119,120,164])). % 58.77/58.83 cnf(205,plain, % 58.77/58.83 (~P6(a18,f2(f21(f20(a19))))), % 58.77/58.83 inference(scs_inference,[],[50,51,55,56,57,54,152,44,45,46,47,48,49,52,149,43,65,153,77,2,61,156,166,33,63,3,34,36,162,170,104,119,120,164,114])). % 58.77/58.83 cnf(209,plain, % 58.77/58.83 (~E(a17,a19)), % 58.77/58.83 inference(scs_inference,[],[50,51,55,56,57,54,152,44,45,46,47,48,49,52,149,43,65,153,77,2,61,156,166,33,63,3,34,36,162,170,104,119,120,164,114,135,35])). % 58.77/58.83 cnf(211,plain, % 58.77/58.83 (~E(f21(a1),a1)), % 58.77/58.83 inference(scs_inference,[],[50,51,55,56,57,54,152,44,45,46,47,48,49,52,149,43,65,153,77,2,61,156,166,33,63,3,34,36,162,170,104,119,120,164,114,135,35,38,39])). % 58.77/58.83 cnf(212,plain, % 58.77/58.83 (P2(x2121,a19)+~E(a3,x2121)), % 58.77/58.83 inference(scs_inference,[],[50,51,55,56,57,54,152,44,45,46,47,48,49,52,149,43,65,153,77,2,61,156,166,33,63,3,34,36,162,170,104,119,120,164,114,135,35,38,39,32])). % 58.77/58.83 cnf(216,plain, % 58.77/58.83 (~P2(a4,f16(f2(f21(f20(a19))),x2161))+~P3(x2161)+~P2(a4,a18)), % 58.77/58.83 inference(scs_inference,[],[50,51,55,56,57,54,152,44,45,46,47,48,49,52,149,43,65,153,77,2,61,156,166,33,63,3,34,36,162,170,104,119,120,164,114,135,35,38,39,165])). % 58.77/58.83 cnf(218,plain, % 58.77/58.83 (E(a1,f5(a17))), % 58.77/58.83 inference(scs_inference,[],[171,2])). % 58.77/58.83 cnf(220,plain, % 58.77/58.83 (P2(f5(a17),f2(f21(a1)))), % 58.77/58.83 inference(scs_inference,[],[184,177,171,2,39,32])). % 58.77/58.83 cnf(221,plain, % 58.77/58.83 (~E(f21(a1),f5(a17))), % 58.77/58.84 inference(scs_inference,[],[184,177,171,211,2,39,32,3])). % 58.77/58.84 cnf(223,plain, % 58.77/58.84 (~E(f2(f21(a1)),f2(a1))), % 58.77/58.84 inference(scs_inference,[],[173,184,43,177,199,171,211,2,39,32,3,36,33])). % 58.77/58.84 cnf(224,plain, % 58.77/58.84 (~P2(x2241,f2(a1))), % 58.77/58.84 inference(rename_variables,[],[173])). % 58.77/58.84 cnf(225,plain, % 58.77/58.84 (P8(f5(a17),f5(a17))), % 58.77/58.84 inference(scs_inference,[],[173,184,43,177,199,171,211,2,39,32,3,36,33,38])). % 58.77/58.84 cnf(226,plain, % 58.77/58.84 (P6(a17,f2(a1))), % 58.77/58.84 inference(scs_inference,[],[173,184,43,177,199,171,211,2,39,32,3,36,33,38,35])). % 58.77/58.84 cnf(227,plain, % 58.77/58.84 (P6(f2(a1),f2(f21(f20(a19))))), % 58.77/58.84 inference(scs_inference,[],[54,173,224,184,43,177,175,199,171,211,2,39,32,3,36,33,38,35,104])). % 58.77/58.84 cnf(230,plain, % 58.77/58.84 (P6(f12(a17,a1),a17)), % 58.77/58.84 inference(scs_inference,[],[54,173,224,184,49,43,177,175,199,171,211,46,149,2,39,32,3,36,33,38,35,104,131])). % 58.77/58.84 cnf(235,plain, % 58.77/58.84 (~P3(f5(a17))+P3(a1)), % 58.77/58.84 inference(scs_inference,[],[54,173,224,184,49,43,177,175,199,171,211,46,149,2,39,32,3,36,33,38,35,104,131,37,31,34,40])). % 58.77/58.84 cnf(237,plain, % 58.77/58.84 (~P2(a4,f16(f2(f21(f20(a19))),x2371))+P4(a1)+~P3(x2371)), % 58.77/58.84 inference(scs_inference,[],[56,54,173,224,184,49,43,177,175,199,171,211,46,149,2,39,32,3,36,33,38,35,104,131,34,165])). % 58.77/58.84 cnf(238,plain, % 58.77/58.84 (P8(f5(a17),a1)), % 58.77/58.84 inference(scs_inference,[],[225,171,39])). % 58.77/58.84 cnf(239,plain, % 58.77/58.84 (P2(f5(a17),a18)), % 58.77/58.84 inference(scs_inference,[],[49,225,218,171,39,32])). % 58.77/58.84 cnf(242,plain, % 58.77/58.84 (~E(a18,f2(a1))), % 58.77/58.84 inference(scs_inference,[],[223,173,49,43,179,225,218,226,171,39,32,3,36,33])). % 58.77/58.84 cnf(246,plain, % 58.77/58.84 (P8(f21(f5(a17)),f21(f5(a17)))), % 58.77/58.84 inference(scs_inference,[],[57,194,223,173,49,43,179,227,225,218,226,171,39,32,3,36,33,38,35,120])). % 58.77/58.84 cnf(248,plain, % 58.77/58.84 (P6(f2(f5(a17)),f2(f5(a17)))), % 58.77/58.84 inference(scs_inference,[],[57,194,223,173,49,43,179,227,225,218,226,171,39,32,3,36,33,38,35,120,119])). % 58.77/58.84 cnf(250,plain, % 58.77/58.84 (P6(f12(a17,f5(a17)),a17)), % 58.77/58.84 inference(scs_inference,[],[57,194,223,173,49,43,179,227,225,218,226,46,149,171,39,32,3,36,33,38,35,120,119,131])). % 58.77/58.84 cnf(256,plain, % 58.77/58.84 (P2(f5(a17),f2(f21(f5(a17))))), % 58.77/58.84 inference(scs_inference,[],[57,194,223,173,49,43,179,227,225,218,226,46,149,171,39,32,3,36,33,38,35,120,119,131,153,163,166])). % 58.77/58.84 cnf(261,plain, % 58.77/58.84 (P2(a1,f2(f21(f5(a17))))), % 58.77/58.84 inference(scs_inference,[],[256,171,32])). % 58.77/58.84 cnf(262,plain, % 58.77/58.84 (P6(f12(a17,f5(a17)),f2(a1))), % 58.77/58.84 inference(scs_inference,[],[256,179,171,250,32,36])). % 58.77/58.84 cnf(270,plain, % 58.77/58.84 (P6(f12(a17,a1),f2(a1))), % 58.77/58.84 inference(scs_inference,[],[179,230,36])). % 58.77/58.84 cnf(273,plain, % 58.77/58.84 (~E(f21(f5(a17)),a1)), % 58.77/58.84 inference(scs_inference,[],[173,261,179,230,36,33,4])). % 58.77/58.84 cnf(279,plain, % 58.77/58.84 (~E(a18,a17)), % 58.77/58.84 inference(scs_inference,[],[239,152,171,273,3,33])). % 58.77/58.84 cnf(281,plain, % 58.77/58.84 (P2(x2811,a19)+~E(a4,x2811)), % 58.77/58.84 inference(scs_inference,[],[51,239,152,171,273,3,33,32])). % 58.77/58.84 cnf(292,plain, % 58.77/58.84 (~P3(a1)+P3(f5(a17))), % 58.77/58.84 inference(scs_inference,[],[53,218,32,40])). % 58.77/58.84 cnf(294,plain, % 58.77/58.84 (P8(x2941,f20(a19))+~E(a3,x2941)), % 58.77/58.84 inference(scs_inference,[],[53,203,218,196,32,40,36,38])). % 58.77/58.84 cnf(295,plain, % 58.77/58.84 (P6(x2951,f2(a1))+~E(f12(a17,a1),x2951)), % 58.77/58.84 inference(scs_inference,[],[53,203,218,196,270,32,40,36,38,35])). % 58.77/58.84 cnf(304,plain, % 58.77/58.84 (P8(x3041,f21(a1))+~E(f21(a1),x3041)), % 58.77/58.84 inference(scs_inference,[],[182,227,201,36,32,38])). % 58.77/58.84 cnf(305,plain, % 58.77/58.84 (P6(x3051,f2(a1))+~E(f12(a17,f5(a17)),x3051)), % 58.77/58.84 inference(scs_inference,[],[182,227,201,262,36,32,38,35])). % 58.77/58.84 cnf(318,plain, % 58.77/58.84 (~P2(x3181,f16(f2(a1),x3182))+~P3(x3182)), % 58.77/58.84 inference(scs_inference,[],[56,173,250,248,246,175,38,36,35,112,165])). % 58.77/58.84 cnf(323,plain, % 58.77/58.84 (P6(x3231,a17)+~E(f12(a17,a1),x3231)), % 58.77/58.84 inference(scs_inference,[],[230,35])). % 58.77/58.84 cnf(343,plain, % 58.77/58.84 (~P2(x3431,f16(a17,x3432))+~P3(x3432)), % 58.77/58.84 inference(scs_inference,[],[152,149,165])). % 58.77/58.84 cnf(352,plain, % 58.77/58.84 (P3(f5(f2(a1)))), % 58.77/58.84 inference(scs_inference,[],[43,62,58])). % 58.77/58.84 cnf(353,plain, % 58.77/58.84 (~P2(x3531,f16(f2(a1),f5(f2(a1))))), % 58.77/58.84 inference(scs_inference,[],[173,352,175,165])). % 58.77/58.84 cnf(359,plain, % 58.77/58.84 (E(f16(f2(a1),f5(f2(a1))),f2(a1))), % 58.77/58.84 inference(scs_inference,[],[173,352,175,165,144,2])). % 58.77/58.84 cnf(360,plain, % 58.77/58.84 (P1(f16(f2(a1),f5(f2(a1))))), % 58.77/58.84 inference(scs_inference,[],[173,352,49,175,165,144,2,73])). % 58.77/58.84 cnf(362,plain, % 58.77/58.84 (E(a17,f16(f2(a1),f5(f2(a1))))), % 58.77/58.84 inference(scs_inference,[],[173,352,49,179,175,165,144,2,73,3])). % 58.77/58.84 cnf(371,plain, % 58.77/58.84 (~P2(x3711,f16(a17,f5(f2(a1))))), % 58.77/58.84 inference(scs_inference,[],[223,152,352,149,359,362,2,3,165])). % 58.77/58.84 cnf(507,plain, % 58.77/58.84 (P6(f16(f2(a1),f5(f2(a1))),f2(a1))), % 58.77/58.84 inference(scs_inference,[],[362,226,35])). % 58.77/58.84 cnf(570,plain, % 58.77/58.84 (P3(a1)), % 58.77/58.84 inference(scs_inference,[],[149,235,62])). % 58.77/58.84 cnf(571,plain, % 58.77/58.84 (P3(f5(a17))), % 58.77/58.84 inference(scs_inference,[],[570,292])). % 58.77/58.84 cnf(580,plain, % 58.77/58.84 (P8(f22(a19),a4)), % 58.77/58.84 inference(scs_inference,[],[51,55,52,162])). % 58.77/58.84 cnf(582,plain, % 58.77/58.84 (P8(a4,f20(a19))), % 58.77/58.84 inference(scs_inference,[],[51,55,52,47,162,164])). % 58.77/58.84 cnf(584,plain, % 58.77/58.84 (P8(f22(a19),x5841)+~E(a4,x5841)), % 58.77/58.84 inference(scs_inference,[],[51,55,52,47,162,164,39])). % 58.77/58.84 cnf(596,plain, % 58.77/58.84 (E(f20(a19),a4)+~E(f22(a19),f13(a19,a4))), % 58.77/58.84 inference(scs_inference,[],[51,55,580,52,47,38,137,584,2])). % 58.77/58.84 cnf(601,plain, % 58.77/58.84 (P8(x6011,f20(a19))+~E(a4,x6011)), % 58.77/58.84 inference(scs_inference,[],[582,38])). % 58.77/58.84 cnf(610,plain, % 58.77/58.84 (~P8(f13(a19,a4),a4)+E(a4,f20(a19))), % 58.77/58.84 inference(scs_inference,[],[51,55,52,47,137])). % 58.77/58.84 cnf(660,plain, % 58.77/58.84 (P4(f2(a4))), % 58.77/58.84 inference(scs_inference,[],[51,69,70])). % 58.77/58.84 cnf(751,plain, % 58.77/58.84 (P8(f22(a19),f20(a19))), % 58.77/58.84 inference(scs_inference,[],[53,55,52,162])). % 58.77/58.84 cnf(753,plain, % 58.77/58.84 (P8(f20(a19),f20(a19))), % 58.77/58.84 inference(scs_inference,[],[53,55,52,47,162,164])). % 58.77/58.84 cnf(755,plain, % 58.77/58.84 (P8(x7551,f20(a19))+~E(f22(a19),x7551)), % 58.77/58.84 inference(scs_inference,[],[53,55,52,47,162,164,38])). % 58.77/58.84 cnf(760,plain, % 58.77/58.84 (P8(x7601,f20(a19))+~E(f20(a19),x7601)), % 58.77/58.84 inference(scs_inference,[],[753,38])). % 58.77/58.84 cnf(824,plain, % 58.77/58.84 (P8(f6(a19),f20(a19))), % 58.77/58.84 inference(scs_inference,[],[55,45,78,68])). % 58.77/58.84 cnf(825,plain, % 58.77/58.84 (P8(x8251,f20(a19))+~E(f6(a19),x8251)), % 58.77/58.84 inference(scs_inference,[],[824,38])). % 58.77/58.84 cnf(847,plain, % 58.77/58.84 (P2(f21(f20(a19)),a18)), % 58.77/58.84 inference(scs_inference,[],[53,79,70])). % 58.77/58.84 cnf(848,plain, % 58.77/58.84 (P8(f21(f20(a19)),f21(f20(a19)))), % 58.77/58.84 inference(scs_inference,[],[847,77])). % 58.77/58.84 cnf(850,plain, % 58.77/58.84 (~P8(f21(f21(f20(a19))),a1)), % 58.77/58.84 inference(scs_inference,[],[152,847,49,179,77,123])). % 58.77/58.84 cnf(865,plain, % 58.77/58.84 (P8(a1,f21(f20(a19)))), % 58.77/58.84 inference(scs_inference,[],[847,49,850,110])). % 58.77/58.84 cnf(867,plain, % 58.77/58.84 (P8(f5(a17),f21(f20(a19)))), % 58.77/58.84 inference(scs_inference,[],[847,218,49,850,110,38])). % 58.77/58.84 cnf(886,plain, % 58.77/58.84 (~E(a4,f20(a19))+~P2(f20(a19),a18)+~P2(a4,a18)), % 58.77/58.84 inference(scs_inference,[],[56,847,848,112])). % 58.77/58.84 cnf(890,plain, % 58.77/58.84 (~P1(f2(a4))+~E(f21(f20(a19)),f5(f2(a4)))+P6(f12(f2(a4),a1),f2(a4))), % 58.77/58.84 inference(scs_inference,[],[56,49,865,660,39,131])). % 58.77/58.84 cnf(1470,plain, % 58.77/58.84 (~P2(f5(a18),f2(f21(f20(a19))))), % 58.77/58.84 inference(scs_inference,[],[187,44,116,83])). % 58.77/58.84 cnf(1633,plain, % 58.77/58.84 (P6(f2(a1),a18)), % 58.77/58.84 inference(scs_inference,[],[44,173,175,104])). % 58.77/58.84 cnf(1634,plain, % 58.77/58.84 (~P2(x16341,f2(a1))), % 58.77/58.84 inference(rename_variables,[],[173])). % 58.77/58.84 cnf(1636,plain, % 58.77/58.84 (P2(a3,a18)), % 58.77/58.84 inference(scs_inference,[],[44,50,173,175,52,104,102])). % 58.77/58.84 cnf(1638,plain, % 58.77/58.84 (~P6(a18,f2(a1))), % 58.77/58.84 inference(scs_inference,[],[44,50,173,242,175,52,104,102,95])). % 58.77/58.84 cnf(1640,plain, % 58.77/58.84 (~P8(f21(a3),a1)), % 58.77/58.84 inference(scs_inference,[],[44,50,173,242,353,359,175,49,52,104,102,95,123])). % 58.77/58.84 cnf(1643,plain, % 58.77/58.84 (P6(a17,a18)), % 58.77/58.84 inference(scs_inference,[],[44,50,173,242,353,359,175,149,49,226,52,104,102,95,123,114])). % 58.77/58.84 cnf(1645,plain, % 58.77/58.84 (P1(f2(a3))), % 58.77/58.84 inference(scs_inference,[],[44,50,173,242,353,359,175,149,49,226,52,104,102,95,123,114,153])). % 58.77/58.84 cnf(1649,plain, % 58.77/58.84 (~E(f12(a17,a1),a18)), % 58.77/58.84 inference(scs_inference,[],[44,50,173,242,353,359,175,149,49,226,52,104,102,95,123,114,153,77,295])). % 58.77/58.84 cnf(1651,plain, % 58.77/58.84 (P2(a3,f2(f21(a3)))), % 58.77/58.84 inference(scs_inference,[],[44,50,173,242,353,359,175,149,49,226,52,104,102,95,123,114,153,77,295,305,166])). % 58.77/58.84 cnf(1657,plain, % 58.77/58.84 (P8(f21(a3),f21(a3))), % 58.77/58.84 inference(scs_inference,[],[44,50,173,1634,242,353,359,175,149,49,226,52,104,102,95,123,114,153,77,295,305,166,33,36,35,120])). % 58.77/58.84 cnf(1659,plain, % 58.77/58.84 (P6(f2(a3),f2(a3))), % 58.77/58.84 inference(scs_inference,[],[44,50,173,1634,242,353,359,175,149,49,226,52,104,102,95,123,114,153,77,295,305,166,33,36,35,120,119])). % 58.77/58.84 cnf(1661,plain, % 58.77/58.84 (P8(a1,a3)), % 58.77/58.84 inference(scs_inference,[],[44,50,173,1634,242,353,359,175,149,49,226,52,104,102,95,123,114,153,77,295,305,166,33,36,35,120,119,110])). % 58.77/58.84 cnf(1663,plain, % 58.77/58.84 (~E(f21(a3),a1)), % 58.77/58.84 inference(scs_inference,[],[44,50,173,1634,242,353,359,175,149,49,226,52,104,102,95,123,114,153,77,295,305,166,33,36,35,120,119,110,4])). % 58.77/58.84 cnf(1669,plain, % 58.77/58.84 (~E(f21(a3),f5(a17))), % 58.77/58.84 inference(scs_inference,[],[199,171,218,1638,1663,1661,35,38,3])). % 58.77/58.84 cnf(1670,plain, % 58.77/58.84 (P2(f20(a19),a18)), % 58.77/58.84 inference(scs_inference,[],[44,53,199,52,171,218,1638,1663,1661,35,38,3,102])). % 58.77/58.84 cnf(1677,plain, % 58.77/58.84 (P6(f16(f2(a1),f5(f2(a1))),a18)), % 58.77/58.84 inference(scs_inference,[],[44,53,848,847,173,279,175,149,199,52,507,171,218,1633,1638,1663,1643,1661,360,35,38,3,102,95,123,114])). % 58.77/58.84 cnf(1679,plain, % 58.77/58.84 (P1(f2(f20(a19)))), % 58.77/58.84 inference(scs_inference,[],[44,53,848,847,173,279,175,149,199,52,507,171,218,1633,1638,1663,1643,1661,360,35,38,3,102,95,123,114,153])). % 58.77/58.84 cnf(1682,plain, % 58.77/58.84 (~P2(a4,a18)+~E(a4,f20(a19))), % 58.77/58.84 inference(scs_inference,[],[44,53,848,847,173,279,175,149,199,52,507,171,218,1633,1638,1663,1643,1661,360,35,38,3,102,95,123,114,153,4,886])). % 58.77/58.84 cnf(1683,plain, % 58.77/58.84 (P2(f20(a19),f2(f21(f20(a19))))), % 58.77/58.84 inference(scs_inference,[],[44,53,848,847,173,279,175,149,199,52,507,171,218,1633,1638,1663,1643,1661,360,35,38,3,102,95,123,114,153,4,886,166])). % 58.77/58.84 cnf(1685,plain, % 58.77/58.84 (~E(f20(a19),a4)), % 58.77/58.84 inference(scs_inference,[],[44,53,56,848,847,173,279,175,149,199,52,507,171,218,1633,1638,1663,1643,1661,360,35,38,3,102,95,123,114,153,4,886,166,32])). % 58.77/58.84 cnf(1701,plain, % 58.77/58.84 (~E(f22(a19),f13(a19,a4))), % 58.77/58.84 inference(scs_inference,[],[1685,596])). % 58.77/58.84 cnf(1702,plain, % 58.77/58.84 (~E(a4,f20(a19))), % 58.77/58.84 inference(scs_inference,[],[51,1682,70])). % 58.77/58.84 cnf(1704,plain, % 58.77/58.84 (~P8(f13(a19,a4),a4)), % 58.77/58.84 inference(scs_inference,[],[1702,610])). % 58.77/58.84 cnf(1705,plain, % 58.77/58.84 (~E(f16(f2(a1),f5(f2(a1))),a18)), % 58.77/58.84 inference(scs_inference,[],[507,1638,35])). % 58.77/58.84 cnf(1706,plain, % 58.77/58.84 (P2(a4,a18)), % 58.77/58.84 inference(scs_inference,[],[44,51,52,507,1638,35,102])). % 58.77/58.84 cnf(1708,plain, % 58.77/58.84 (~P2(a4,f2(f20(a19)))), % 58.77/58.84 inference(scs_inference,[],[44,51,56,1670,52,507,1638,35,102,130])). % 58.77/58.84 cnf(1710,plain, % 58.77/58.84 (~P8(f21(a4),a1)), % 58.77/58.84 inference(scs_inference,[],[44,51,56,1670,353,359,49,52,507,1638,35,102,130,123])). % 58.77/58.84 cnf(1713,plain, % 58.77/58.84 (P1(f2(a4))), % 58.77/58.84 inference(scs_inference,[],[44,51,56,1670,353,359,49,52,507,1638,35,102,130,123,153])). % 58.77/58.84 cnf(1715,plain, % 58.77/58.84 (P8(a4,a4)), % 58.77/58.84 inference(scs_inference,[],[44,51,56,1670,353,359,49,52,507,1638,35,102,130,123,153,77])). % 58.77/58.84 cnf(1718,plain, % 58.77/58.84 (~P8(f21(a4),f21(f20(a19)))), % 58.77/58.84 inference(scs_inference,[],[44,51,56,1670,353,359,49,52,507,1638,35,102,130,123,153,77,890,135])). % 58.77/58.84 cnf(1720,plain, % 58.77/58.84 (P2(a4,f2(f21(a4)))), % 58.77/58.84 inference(scs_inference,[],[44,51,56,1670,353,359,49,52,507,1638,35,102,130,123,153,77,890,135,166])). % 58.77/58.84 cnf(1726,plain, % 58.77/58.84 (P8(a1,a4)), % 58.77/58.84 inference(scs_inference,[],[44,51,56,848,1670,353,359,49,52,507,1638,35,102,130,123,153,77,890,135,166,33,38,120,110])). % 58.77/58.84 cnf(1728,plain, % 58.77/58.84 (P6(f2(a4),f2(a4))), % 58.77/58.84 inference(scs_inference,[],[44,51,56,848,1670,353,359,49,52,507,1638,35,102,130,123,153,77,890,135,166,33,38,120,110,119])). % 58.77/58.84 cnf(1730,plain, % 58.77/58.84 (~P2(a4,f16(f2(f20(a19)),f5(f2(a1))))), % 58.77/58.84 inference(scs_inference,[],[44,51,56,848,1670,353,352,359,49,52,507,1638,1679,35,102,130,123,153,77,890,135,166,33,38,120,110,119,165])). % 58.77/58.84 cnf(1735,plain, % 58.77/58.84 (P2(x17351,a18)+~E(a3,x17351)), % 58.77/58.84 inference(scs_inference,[],[44,51,56,848,1636,1670,353,352,359,49,52,507,1638,1679,35,102,130,123,153,77,890,135,166,33,38,120,110,119,165,4,163,32])). % 58.77/58.84 cnf(1744,plain, % 58.77/58.84 (~P3(x17441)+~P2(a4,f16(f2(f21(f20(a19))),x17441))), % 58.77/58.84 inference(scs_inference,[],[1706,216])). % 58.77/58.84 cnf(1750,plain, % 58.77/58.84 (P8(f21(f20(a19)),a4)), % 58.77/58.84 inference(scs_inference,[],[847,1718,1706,865,38,110])). % 58.77/58.84 cnf(1752,plain, % 58.77/58.84 (P2(f22(a19),a18)), % 58.77/58.84 inference(scs_inference,[],[44,182,847,1718,1706,865,52,38,110,102])). % 58.77/58.84 cnf(1754,plain, % 58.77/58.84 (~P8(f21(f22(a19)),a1)), % 58.77/58.84 inference(scs_inference,[],[44,182,847,1718,1706,353,359,49,865,52,38,110,102,123])). % 58.77/58.84 cnf(1757,plain, % 58.77/58.84 (P8(f22(a19),f22(a19))), % 58.77/58.84 inference(scs_inference,[],[44,182,847,1718,1706,353,359,49,865,52,38,110,102,123,77])). % 58.77/58.84 cnf(1759,plain, % 58.77/58.84 (P1(f2(f22(a19)))), % 58.77/58.84 inference(scs_inference,[],[44,182,847,1718,1706,353,359,49,865,52,38,110,102,123,77,153])). % 58.77/58.84 cnf(1765,plain, % 58.77/58.84 (~E(f2(f21(f22(a19))),f2(a1))), % 58.77/58.84 inference(scs_inference,[],[44,182,847,173,1670,1718,1706,353,359,49,865,52,38,110,102,123,77,153,166,163,33])). % 58.77/58.84 cnf(1776,plain, % 58.77/58.84 (~E(f21(f22(a19)),a1)), % 58.77/58.84 inference(scs_inference,[],[1765,4])). % 58.77/58.84 cnf(1780,plain, % 58.77/58.84 (P8(a1,f22(a19))), % 58.77/58.84 inference(scs_inference,[],[1718,1765,1752,49,867,1757,1754,4,38,120,110])). % 58.77/58.84 cnf(1792,plain, % 58.77/58.84 (~P6(a19,f2(a1))), % 58.77/58.84 inference(scs_inference,[],[50,173,1704,175,171,1715,1776,3,38,102])). % 58.77/58.84 cnf(1804,plain, % 58.77/58.84 (~P6(f2(f21(a1)),f2(a1))), % 58.77/58.84 inference(scs_inference,[],[220,173,1704,1792,175,507,1750,35,38,102])). % 58.77/58.84 cnf(1815,plain, % 58.77/58.84 (~P6(f2(f21(f5(a17))),f2(a1))), % 58.77/58.84 inference(scs_inference,[],[173,261,1804,175,226,218,1780,35,38,102])). % 58.77/58.84 cnf(1842,plain, % 58.77/58.84 (~P6(f2(f21(a3)),f2(a1))), % 58.77/58.84 inference(scs_inference,[],[173,1651,1704,1815,175,226,1726,35,38,102])). % 58.77/58.84 cnf(1848,plain, % 58.77/58.84 (P2(x18481,a18)+~E(a4,x18481)), % 58.77/58.84 inference(scs_inference,[],[173,1706,1651,1704,1815,175,226,1677,1726,35,38,102,295,305,36,32])). % 58.77/58.84 cnf(1859,plain, % 58.77/58.84 (~E(a17,f2(f21(a3)))), % 58.77/58.84 inference(scs_inference,[],[1842,226,35])). % 58.77/58.84 cnf(1957,plain, % 58.77/58.84 (P8(f21(f20(a19)),x19571)+~E(a4,x19571)), % 58.77/58.84 inference(scs_inference,[],[1750,39])). % 58.77/58.84 cnf(2182,plain, % 58.77/58.84 (~P6(a18,a19)), % 58.77/58.84 inference(scs_inference,[],[45,187,47,84])). % 58.77/58.84 cnf(2373,plain, % 58.77/58.84 (~P2(x23731,a17)), % 58.77/58.84 inference(rename_variables,[],[152])). % 58.77/58.84 cnf(2375,plain, % 58.77/58.84 (~P2(x23751,a17)), % 58.77/58.84 inference(rename_variables,[],[152])). % 58.77/58.84 cnf(2378,plain, % 58.77/58.84 (~P2(x23781,a17)), % 58.77/58.84 inference(rename_variables,[],[152])). % 58.77/58.84 cnf(2380,plain, % 58.77/58.84 (E(a17,f16(a17,f5(f2(a1))))), % 58.77/58.84 inference(scs_inference,[],[152,2373,2375,2378,1651,1670,848,847,352,149,33,102,123,144])). % 58.77/58.84 cnf(2384,plain, % 58.77/58.84 (E(f16(a17,f5(f2(a1))),a17)), % 58.77/58.84 inference(scs_inference,[],[152,2373,2375,2378,1651,1670,848,847,352,149,33,102,123,144,2])). % 58.77/58.84 cnf(2386,plain, % 58.77/58.84 (E(f2(a1),f16(a17,f5(f2(a1))))), % 58.77/58.84 inference(scs_inference,[],[46,152,2373,2375,2378,1651,1670,848,847,352,43,149,33,102,123,144,2,34,3])). % 58.77/58.84 cnf(2387,plain, % 58.77/58.84 (P1(f16(a17,f5(f2(a1))))), % 58.77/58.84 inference(scs_inference,[],[46,152,2373,2375,2378,1651,1670,848,847,352,43,149,33,102,123,144,2,34,3,31])). % 58.77/58.84 cnf(2389,plain, % 58.77/58.84 (~P5(f16(a17,f5(f2(a1))))), % 58.77/58.84 inference(scs_inference,[],[46,152,2373,2375,2378,1651,1670,848,847,172,352,43,149,33,102,123,144,2,34,3,31,40,37])). % 58.77/58.84 cnf(2399,plain, % 58.77/58.84 (E(f16(a17,f5(f2(a1))),f2(a1))), % 58.77/58.84 inference(scs_inference,[],[2386,2])). % 58.77/58.84 cnf(2415,plain, % 58.77/58.84 (~E(f2(f21(f20(a19))),a17)), % 58.77/58.84 inference(scs_inference,[],[152,1683,223,2399,3,33])). % 58.77/58.84 cnf(2430,plain, % 58.77/58.84 (~P6(f2(f21(f5(a17))),a17)), % 58.77/58.84 inference(scs_inference,[],[152,256,149,102])). % 58.77/58.84 cnf(2931,plain, % 58.77/58.84 (~P6(a18,f16(a17,f5(f2(a1))))+E(a18,f16(a17,f5(f2(a1))))), % 58.77/58.84 inference(scs_inference,[],[199,2386,1633,44,2387,36,35,95])). % 58.77/58.84 cnf(3450,plain, % 58.77/58.84 (~P2(x34501,a17)), % 58.77/58.84 inference(rename_variables,[],[152])). % 58.77/58.84 cnf(3451,plain, % 58.77/58.84 (~P6(f2(f21(a4)),a17)), % 58.77/58.84 inference(scs_inference,[],[152,3450,1720,149,33,102])). % 58.77/58.84 cnf(3879,plain, % 58.77/58.84 (P4(f2(a3))), % 58.77/58.84 inference(scs_inference,[],[1759,1636,2387,64,62,69])). % 58.77/58.84 cnf(3881,plain, % 58.77/58.84 (P8(a1,f20(a19))), % 58.77/58.84 inference(scs_inference,[],[1759,1636,1670,2387,64,62,69,71])). % 58.77/58.84 cnf(3889,plain, % 58.77/58.84 (~P2(x38891,f16(a17,f5(a17)))), % 58.77/58.84 inference(scs_inference,[],[571,1759,1636,1670,2387,64,62,69,71,67,80,81,343])). % 58.77/58.84 cnf(3893,plain, % 58.77/58.84 (P2(f21(a3),a18)), % 58.77/58.84 inference(scs_inference,[],[571,1759,1636,1670,1706,2387,64,62,69,71,67,80,81,343,66,79])). % 58.77/58.84 cnf(3943,plain, % 58.77/58.84 (E(f15(f16(a18,a3),a3),a18)), % 58.77/58.84 inference(scs_inference,[],[1701,2415,1663,571,2380,660,2384,1759,1713,1636,1670,1706,2387,44,54,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106])). % 58.77/58.84 cnf(3947,plain, % 58.77/58.84 (~P2(f5(a18),a18)), % 58.77/58.84 inference(scs_inference,[],[1701,2415,1663,571,2380,660,2384,1759,187,1713,1636,1670,1706,2387,44,54,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83])). % 58.77/58.84 cnf(3951,plain, % 58.77/58.84 (P3(a3)), % 58.77/58.84 inference(scs_inference,[],[1701,2415,1663,571,2380,660,2384,1759,187,1713,1636,1670,1706,2387,44,54,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76])). % 58.77/58.84 cnf(3953,plain, % 58.77/58.84 (~P5(f2(a3))), % 58.77/58.84 inference(scs_inference,[],[1701,2415,1663,571,2380,660,2384,1759,187,1645,1713,1636,1670,1706,2387,44,54,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63])). % 58.77/58.84 cnf(3958,plain, % 58.77/58.84 (P2(f21(a3),f2(f21(f21(a3))))), % 58.77/58.84 inference(scs_inference,[],[2182,1701,2415,3451,2389,1663,571,2380,660,2384,1759,187,1645,1713,1636,48,1670,1706,2387,44,54,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166])). % 58.77/58.84 cnf(3960,plain, % 58.77/58.84 (~P8(f21(a4),f5(a17))), % 58.77/58.84 inference(scs_inference,[],[2182,1701,2415,3451,2389,1710,1663,571,2380,660,2384,1759,187,1645,1713,1636,48,1670,1706,2387,171,44,54,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39])). % 58.77/58.84 cnf(3973,plain, % 58.77/58.84 (P5(f15(a18,f5(a17)))), % 58.77/58.84 inference(scs_inference,[],[209,2182,1701,2415,1730,3451,2389,1710,1640,1663,571,2380,660,1720,2384,279,1759,187,1645,1713,1636,48,1670,1706,2387,171,239,44,54,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92])). % 58.77/58.84 cnf(3979,plain, % 58.77/58.84 (E(f16(f15(a17,f5(a17)),f5(a17)),a17)), % 58.77/58.84 inference(scs_inference,[],[209,2182,1701,2415,1730,3451,2389,1710,1640,1663,571,2380,660,1720,2384,279,1759,187,1728,1645,1713,1636,48,1670,1706,2387,152,171,239,44,149,54,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92,85,97,105])). % 58.77/58.84 cnf(3980,plain, % 58.77/58.84 (~P2(x39801,a17)), % 58.77/58.84 inference(rename_variables,[],[152])). % 58.77/58.84 cnf(3984,plain, % 58.77/58.84 (P6(f2(f22(a19)),f2(f20(a19)))), % 58.77/58.84 inference(scs_inference,[],[50,209,2182,1701,2415,1730,3451,2389,1710,1640,1663,571,2380,751,660,1720,2384,279,1759,187,1728,1645,1713,1636,48,1752,1670,1706,47,2387,152,171,239,44,149,54,45,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92,85,97,105,129,119])). % 58.77/58.84 cnf(3988,plain, % 58.77/58.84 (P1(f16(a17,f5(a17)))), % 58.77/58.84 inference(scs_inference,[],[50,209,2182,1701,2415,1730,3451,2389,1710,1640,1663,571,2380,751,660,1720,2384,279,1759,187,1728,1645,1713,1636,48,1752,1670,1706,47,2387,152,171,239,44,149,54,45,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92,85,97,105,129,119,93,86])). % 58.77/58.84 cnf(4003,plain, % 58.77/58.84 (~P6(a19,f16(a17,f5(a17)))), % 58.77/58.84 inference(scs_inference,[],[50,209,2182,1701,2415,1730,3451,2389,1710,1640,1663,571,1708,2380,751,1683,660,1720,2384,279,353,1759,187,1728,1645,1713,1636,48,1752,1670,1706,47,2387,152,847,171,239,49,360,44,149,54,45,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92,85,97,105,129,119,93,86,130,125,104,122,170,120,102])). % 58.77/58.84 cnf(4008,plain, % 58.77/58.84 (~P2(x40081,a17)), % 58.77/58.84 inference(rename_variables,[],[152])). % 58.77/58.84 cnf(4010,plain, % 58.77/58.84 (E(f5(f12(a17,f5(a17))),f5(a17))), % 58.77/58.84 inference(scs_inference,[],[50,209,2182,1701,2415,1730,3451,2389,1710,1640,1663,571,1708,2380,751,1683,660,1720,2384,279,353,1759,187,1728,1645,1713,1636,48,1752,1670,1706,225,46,47,2387,152,3980,847,171,239,49,52,360,44,149,54,55,45,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92,85,97,105,129,119,93,86,130,125,104,122,170,120,102,89,111,127])). % 58.77/58.84 cnf(4013,plain, % 58.77/58.84 (~P2(x40131,f16(a17,f5(f2(a1))))), % 58.77/58.84 inference(rename_variables,[],[371])). % 58.77/58.84 cnf(4018,plain, % 58.77/58.84 (~P2(x40181,f16(a17,f5(f2(a1))))), % 58.77/58.84 inference(rename_variables,[],[371])). % 58.77/58.84 cnf(4022,plain, % 58.77/58.84 (~P2(f21(a4),a19)), % 58.77/58.84 inference(scs_inference,[],[50,209,2182,1701,1705,2415,371,4013,1730,3451,2389,1710,1640,1663,571,1708,2380,751,1657,1683,261,660,1720,2384,279,353,1759,187,1728,1645,1713,1636,48,1752,1670,1706,218,225,46,47,2387,152,3980,847,171,239,49,52,360,44,1677,149,54,55,45,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92,85,97,105,129,119,93,86,130,125,104,122,170,120,102,89,111,127,109,99,123,95,164])). % 58.77/58.84 cnf(4025,plain, % 58.77/58.84 (~P2(x40251,f16(a17,f5(f2(a1))))), % 58.77/58.84 inference(rename_variables,[],[371])). % 58.77/58.84 cnf(4028,plain, % 58.77/58.84 (~P2(x40281,f16(a17,f5(f2(a1))))), % 58.77/58.84 inference(rename_variables,[],[371])). % 58.77/58.84 cnf(4031,plain, % 58.77/58.84 (~P2(x40311,f16(a17,f5(f2(a1))))), % 58.77/58.84 inference(rename_variables,[],[371])). % 58.77/58.84 cnf(4034,plain, % 58.77/58.84 (~P2(x40341,f16(a17,f5(f2(a1))))), % 58.77/58.84 inference(rename_variables,[],[371])). % 58.77/58.84 cnf(4048,plain, % 58.77/58.84 (~E(a4,a1)), % 58.77/58.84 inference(scs_inference,[],[50,209,2182,221,1701,1705,2415,371,4013,4018,4025,4028,4031,1730,3451,2389,1710,1640,1663,571,1708,2380,751,1657,1683,261,660,570,1720,2384,279,353,1759,187,1728,1645,1713,1636,48,1752,1670,1706,218,225,46,47,2387,152,3980,847,171,239,49,52,360,44,1677,149,54,55,45,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92,85,97,105,129,119,93,86,130,125,104,122,170,120,102,89,111,127,109,99,123,95,164,167,96,115,144,212,281,1735,1848,78,294,601,304,755,760,825,1957])). % 58.77/58.84 cnf(4065,plain, % 58.77/58.84 (~P8(f20(a19),a4)), % 58.77/58.84 inference(scs_inference,[],[50,209,2182,221,1701,1702,1669,1705,2415,371,4013,4018,4025,4028,4031,4034,1730,3451,2389,1710,1640,1663,571,1708,2380,751,1657,1683,261,582,660,570,1720,2384,279,353,1759,187,1728,1645,1713,1636,48,1752,1670,1706,218,225,1470,46,47,2387,152,3980,847,171,239,49,52,360,44,1677,149,54,55,45,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92,85,97,105,129,119,93,86,130,125,104,122,170,120,102,89,111,127,109,99,123,95,164,167,96,115,144,212,281,1735,1848,78,294,601,304,755,760,825,1957,2931,70,65,237,135,32,87,94,165,118])). % 58.77/58.84 cnf(4067,plain, % 58.77/58.84 (P2(f14(f21(a3),a17),a18)), % 58.77/58.84 inference(scs_inference,[],[50,209,2182,221,1701,1702,1669,1859,1705,2415,371,4013,4018,4025,4028,4031,4034,1730,3451,2389,1710,1640,1663,571,1708,2380,751,1657,1683,261,582,660,570,1720,2384,279,353,1759,187,1728,1645,1713,1636,48,1752,1670,1706,218,225,1470,46,47,2387,152,3980,4008,847,171,239,49,52,360,44,1677,149,54,55,45,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92,85,97,105,129,119,93,86,130,125,104,122,170,120,102,89,111,127,109,99,123,95,164,167,96,115,144,212,281,1735,1848,78,294,601,304,755,760,825,1957,2931,70,65,237,135,32,87,94,165,118,132])). % 58.77/58.84 cnf(4068,plain, % 58.77/58.84 (~P2(x40681,a17)), % 58.77/58.84 inference(rename_variables,[],[152])). % 58.77/58.84 cnf(4070,plain, % 58.77/58.84 (P8(f21(f14(f21(a3),a17)),f21(a3))), % 58.77/58.84 inference(scs_inference,[],[50,209,2182,221,1701,1702,1669,1859,1705,2415,371,4013,4018,4025,4028,4031,4034,1730,3451,2389,1710,1640,1663,571,1708,2380,751,1657,1683,261,582,660,570,1720,2384,279,353,1759,187,1728,1645,1713,1636,48,1752,1670,1706,218,225,1470,46,47,2387,152,3980,4008,4068,847,171,239,49,52,360,44,1677,149,54,55,45,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92,85,97,105,129,119,93,86,130,125,104,122,170,120,102,89,111,127,109,99,123,95,164,167,96,115,144,212,281,1735,1848,78,294,601,304,755,760,825,1957,2931,70,65,237,135,32,87,94,165,118,132,139])). % 58.77/58.84 cnf(4073,plain, % 58.77/58.84 (P2(a3,f15(a19,a3))), % 58.77/58.84 inference(scs_inference,[],[50,209,2182,221,1701,1702,1669,1859,1705,2415,371,4013,4018,4025,4028,4031,4034,1730,3451,2389,1710,1640,1663,571,1708,2380,751,1657,1683,261,582,660,570,1720,2384,279,353,1759,187,1728,1645,1713,1636,48,1752,1670,1706,218,225,1470,46,47,2387,152,3980,4008,4068,847,171,239,49,52,360,44,1677,149,54,55,45,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92,85,97,105,129,119,93,86,130,125,104,122,170,120,102,89,111,127,109,99,123,95,164,167,96,115,144,212,281,1735,1848,78,294,601,304,755,760,825,1957,2931,70,65,237,135,32,87,94,165,118,132,139,168])). % 58.77/58.84 cnf(4075,plain, % 58.77/58.84 (P6(f12(f2(a4),f5(f2(a4))),f2(a4))), % 58.77/58.84 inference(scs_inference,[],[50,209,2182,221,1701,1702,1669,1859,1705,2415,371,4013,4018,4025,4028,4031,4034,1730,3451,2389,1710,1640,1663,571,1708,2380,751,1657,1683,261,582,660,570,1720,2384,279,353,1759,187,1728,1645,1713,1636,48,1752,1670,1706,218,225,1470,46,47,2387,152,3980,4008,4068,847,171,239,49,52,360,44,1677,149,54,55,45,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92,85,97,105,129,119,93,86,130,125,104,122,170,120,102,89,111,127,109,99,123,95,164,167,96,115,144,212,281,1735,1848,78,294,601,304,755,760,825,1957,2931,70,65,237,135,32,87,94,165,118,132,139,168,131])). % 58.77/58.84 cnf(4080,plain, % 58.77/58.84 (~P8(f21(f20(a19)),f5(a17))), % 58.77/58.84 inference(scs_inference,[],[50,209,2182,221,1701,1702,1669,1859,1705,2415,371,4013,4018,4025,4028,4031,4034,1730,3451,2389,1710,1640,238,1663,571,1708,2380,751,1657,1683,261,582,660,570,1720,2384,279,353,1759,187,1728,1645,1713,1636,48,1752,1670,1706,218,225,1470,46,47,2387,152,3980,4008,4068,847,171,239,49,52,360,44,1677,149,54,55,45,64,62,69,71,67,80,81,343,66,79,5,14,15,27,30,318,6,7,12,13,16,17,18,19,23,24,25,26,28,29,9,10,11,20,21,22,1744,4,88,8,295,2,323,154,155,74,59,60,82,106,72,83,159,76,63,37,35,36,166,39,3,68,163,33,34,38,90,91,92,85,97,105,129,119,93,86,130,125,104,122,170,120,102,89,111,127,109,99,123,95,164,167,96,115,144,212,281,1735,1848,78,294,601,304,755,760,825,1957,2931,70,65,237,135,32,87,94,165,118,132,139,168,131,141,138])). % 58.77/58.84 cnf(4202,plain, % 58.77/58.84 ($false), % 58.77/58.84 inference(scs_inference,[],[50,4048,3951,1649,3947,3879,3953,3960,3881,3893,4022,4065,4073,4080,3889,3988,3973,4003,3943,4067,3984,3979,4010,4070,4075,205,3958,2430,1708,1718,582,279,1659,187,1645,660,1679,1713,48,1636,218,1706,1670,43,49,52,44,55,175,45,343,69,66,318,80,23,81,25,26,29,62,6,67,30,21,79,71,5,16,1957,9,10,64,28,20,13,15,22,19,18,24,14,65,27,11,88,12,17,7,4,8,2,72,106,82,74,59,155,60,75,154,63,76,35,37,36,68,39,3,163,33,32,34,38,92,94,90,87,91,97,93,124,84,125,104,170,102,120]), % 58.77/58.84 ['proof']). % 58.77/58.84 % SZS output end Proof % 58.77/58.84 % Total time :58.180000s %------------------------------------------------------------------------------