%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM630+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : 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:32 EDT 2024 % Result : Theorem 7.32s 7.39s % Output : CNFRefutation 7.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NUM630+1 : TPTP v8.2.0. Released v4.0.0. % 0.04/0.12 % Command : java -jar /export/starexec/sandbox/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 23:02:23 EDT 2024 % 0.12/0.33 % CPUTime : % 0.53/0.56 start to proof:theBenchmark % 7.30/7.36 %------------------------------------------- % 7.30/7.36 % File :CSE---1.7 % 7.30/7.36 % Problem :theBenchmark % 7.30/7.36 % Transform :cnf % 7.30/7.36 % Format :tptp:raw % 7.30/7.36 % Command :java -jar mcs_scs.jar %d %s % 7.30/7.36 % 7.30/7.36 % Result :Theorem 6.700000s % 7.30/7.36 % Output :CNFRefutation 6.700000s % 7.30/7.36 %------------------------------------------- % 7.32/7.36 %------------------------------------------------------------------------------ % 7.32/7.36 % File : NUM630+1 : TPTP v8.2.0. Released v4.0.0. % 7.32/7.36 % Domain : Number Theory % 7.32/7.36 % Problem : Ramsey's Infinite Theorem 15_02_23_12_03, 00 expansion % 7.32/7.36 % Version : Especial. % 7.32/7.36 % English : % 7.32/7.36 % 7.32/7.36 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 7.32/7.36 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 7.32/7.36 % Source : [Pas08] % 7.32/7.36 % Names : ramsey_15_02_23_12_03.00 [Pas08] % 7.32/7.36 % 7.32/7.36 % Status : Theorem % 7.32/7.36 % Rating : 0.33 v8.2.0, 0.39 v7.5.0, 0.41 v7.4.0, 0.33 v7.3.0, 0.45 v7.1.0, 0.39 v7.0.0, 0.43 v6.4.0, 0.46 v6.3.0, 0.42 v6.2.0, 0.40 v6.1.0, 0.47 v6.0.0, 0.48 v5.5.0, 0.59 v5.4.0, 0.61 v5.3.0, 0.70 v5.2.0, 0.65 v5.1.0, 0.71 v5.0.0, 0.75 v4.1.0, 0.78 v4.0.1, 0.87 v4.0.0 % 7.32/7.36 % Syntax : Number of formulae : 116 ( 23 unt; 11 def) % 7.32/7.36 % Number of atoms : 408 ( 76 equ) % 7.32/7.36 % Maximal formula atoms : 12 ( 3 avg) % 7.32/7.36 % Number of connectives : 317 ( 25 ~; 4 |; 131 &) % 7.32/7.36 % ( 22 <=>; 135 =>; 0 <=; 0 <~>) % 7.32/7.36 % Maximal formula depth : 15 ( 5 avg) % 7.32/7.36 % Maximal term depth : 5 ( 1 avg) % 7.32/7.36 % Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty) % 7.32/7.36 % Number of functors : 32 ( 32 usr; 18 con; 0-2 aty) % 7.32/7.36 % Number of variables : 171 ( 159 !; 12 ?) % 7.32/7.36 % SPC : FOF_THM_RFO_SEQ % 7.32/7.36 % 7.32/7.36 % Comments : Problem generated by the SAD system [VLP07] % 7.32/7.36 %------------------------------------------------------------------------------ % 7.32/7.36 fof(mSetSort,axiom, % 7.32/7.36 ! [W0] : % 7.32/7.36 ( aSet0(W0) % 7.32/7.36 => $true ) ). % 7.32/7.36 % 7.32/7.36 fof(mElmSort,axiom, % 7.32/7.36 ! [W0] : % 7.32/7.36 ( aElement0(W0) % 7.32/7.36 => $true ) ). % 7.32/7.36 % 7.32/7.36 fof(mEOfElem,axiom, % 7.32/7.36 ! [W0] : % 7.32/7.36 ( aSet0(W0) % 7.32/7.36 => ! [W1] : % 7.32/7.36 ( aElementOf0(W1,W0) % 7.32/7.36 => aElement0(W1) ) ) ). % 7.32/7.36 % 7.32/7.36 fof(mFinRel,axiom, % 7.32/7.36 ! [W0] : % 7.32/7.36 ( aSet0(W0) % 7.32/7.36 => ( isFinite0(W0) % 7.32/7.36 => $true ) ) ). % 7.32/7.36 % 7.32/7.36 fof(mDefEmp,definition, % 7.32/7.36 ! [W0] : % 7.32/7.36 ( W0 = slcrc0 % 7.32/7.36 <=> ( aSet0(W0) % 7.32/7.36 & ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 7.32/7.36 % 7.32/7.36 fof(mEmpFin,axiom, % 7.32/7.36 isFinite0(slcrc0) ). % 7.32/7.36 % 7.32/7.36 fof(mCntRel,axiom, % 7.32/7.36 ! [W0] : % 7.32/7.36 ( aSet0(W0) % 7.32/7.36 => ( isCountable0(W0) % 7.32/7.36 => $true ) ) ). % 7.32/7.36 % 7.32/7.36 fof(mCountNFin,axiom, % 7.32/7.36 ! [W0] : % 7.32/7.36 ( ( aSet0(W0) % 7.32/7.36 & isCountable0(W0) ) % 7.32/7.36 => ~ isFinite0(W0) ) ). % 7.32/7.36 % 7.32/7.36 fof(mCountNFin_01,axiom, % 7.32/7.36 ! [W0] : % 7.32/7.36 ( ( aSet0(W0) % 7.32/7.36 & isCountable0(W0) ) % 7.32/7.36 => W0 != slcrc0 ) ). % 7.32/7.36 % 7.32/7.36 fof(mDefSub,definition, % 7.32/7.36 ! [W0] : % 7.32/7.36 ( aSet0(W0) % 7.32/7.37 => ! [W1] : % 7.32/7.37 ( aSubsetOf0(W1,W0) % 7.32/7.37 <=> ( aSet0(W1) % 7.32/7.37 & ! [W2] : % 7.32/7.37 ( aElementOf0(W2,W1) % 7.32/7.37 => aElementOf0(W2,W0) ) ) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mSubFSet,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( ( aSet0(W0) % 7.32/7.37 & isFinite0(W0) ) % 7.32/7.37 => ! [W1] : % 7.32/7.37 ( aSubsetOf0(W1,W0) % 7.32/7.37 => isFinite0(W1) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mSubRefl,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aSet0(W0) % 7.32/7.37 => aSubsetOf0(W0,W0) ) ). % 7.32/7.37 % 7.32/7.37 fof(mSubASymm,axiom, % 7.32/7.37 ! [W0,W1] : % 7.32/7.37 ( ( aSet0(W0) % 7.32/7.37 & aSet0(W1) ) % 7.32/7.37 => ( ( aSubsetOf0(W0,W1) % 7.32/7.37 & aSubsetOf0(W1,W0) ) % 7.32/7.37 => W0 = W1 ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mSubTrans,axiom, % 7.32/7.37 ! [W0,W1,W2] : % 7.32/7.37 ( ( aSet0(W0) % 7.32/7.37 & aSet0(W1) % 7.32/7.37 & aSet0(W2) ) % 7.32/7.37 => ( ( aSubsetOf0(W0,W1) % 7.32/7.37 & aSubsetOf0(W1,W2) ) % 7.32/7.37 => aSubsetOf0(W0,W2) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mDefCons,definition, % 7.32/7.37 ! [W0,W1] : % 7.32/7.37 ( ( aSet0(W0) % 7.32/7.37 & aElement0(W1) ) % 7.32/7.37 => ! [W2] : % 7.32/7.37 ( W2 = sdtpldt0(W0,W1) % 7.32/7.37 <=> ( aSet0(W2) % 7.32/7.37 & ! [W3] : % 7.32/7.37 ( aElementOf0(W3,W2) % 7.32/7.37 <=> ( aElement0(W3) % 7.32/7.37 & ( aElementOf0(W3,W0) % 7.32/7.37 | W3 = W1 ) ) ) ) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mDefDiff,definition, % 7.32/7.37 ! [W0,W1] : % 7.32/7.37 ( ( aSet0(W0) % 7.32/7.37 & aElement0(W1) ) % 7.32/7.37 => ! [W2] : % 7.32/7.37 ( W2 = sdtmndt0(W0,W1) % 7.32/7.37 <=> ( aSet0(W2) % 7.32/7.37 & ! [W3] : % 7.32/7.37 ( aElementOf0(W3,W2) % 7.32/7.37 <=> ( aElement0(W3) % 7.32/7.37 & aElementOf0(W3,W0) % 7.32/7.37 & W3 != W1 ) ) ) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mConsDiff,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aSet0(W0) % 7.32/7.37 => ! [W1] : % 7.32/7.37 ( aElementOf0(W1,W0) % 7.32/7.37 => sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mDiffCons,axiom, % 7.32/7.37 ! [W0,W1] : % 7.32/7.37 ( ( aElement0(W0) % 7.32/7.37 & aSet0(W1) ) % 7.32/7.37 => ( ~ aElementOf0(W0,W1) % 7.32/7.37 => sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mCConsSet,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aElement0(W0) % 7.32/7.37 => ! [W1] : % 7.32/7.37 ( ( aSet0(W1) % 7.32/7.37 & isCountable0(W1) ) % 7.32/7.37 => isCountable0(sdtpldt0(W1,W0)) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mCDiffSet,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aElement0(W0) % 7.32/7.37 => ! [W1] : % 7.32/7.37 ( ( aSet0(W1) % 7.32/7.37 & isCountable0(W1) ) % 7.32/7.37 => isCountable0(sdtmndt0(W1,W0)) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mFConsSet,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aElement0(W0) % 7.32/7.37 => ! [W1] : % 7.32/7.37 ( ( aSet0(W1) % 7.32/7.37 & isFinite0(W1) ) % 7.32/7.37 => isFinite0(sdtpldt0(W1,W0)) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mFDiffSet,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aElement0(W0) % 7.32/7.37 => ! [W1] : % 7.32/7.37 ( ( aSet0(W1) % 7.32/7.37 & isFinite0(W1) ) % 7.32/7.37 => isFinite0(sdtmndt0(W1,W0)) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mNATSet,axiom, % 7.32/7.37 ( aSet0(szNzAzT0) % 7.32/7.37 & isCountable0(szNzAzT0) ) ). % 7.32/7.37 % 7.32/7.37 fof(mZeroNum,axiom, % 7.32/7.37 aElementOf0(sz00,szNzAzT0) ). % 7.32/7.37 % 7.32/7.37 fof(mSuccNum,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 => ( aElementOf0(szszuzczcdt0(W0),szNzAzT0) % 7.32/7.37 & szszuzczcdt0(W0) != sz00 ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mSuccEquSucc,axiom, % 7.32/7.37 ! [W0,W1] : % 7.32/7.37 ( ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 & aElementOf0(W1,szNzAzT0) ) % 7.32/7.37 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 7.32/7.37 => W0 = W1 ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mNatExtra,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 => ( W0 = sz00 % 7.32/7.37 | ? [W1] : % 7.32/7.37 ( aElementOf0(W1,szNzAzT0) % 7.32/7.37 & W0 = szszuzczcdt0(W1) ) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mNatNSucc,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 => W0 != szszuzczcdt0(W0) ) ). % 7.32/7.37 % 7.32/7.37 fof(mLessRel,axiom, % 7.32/7.37 ! [W0,W1] : % 7.32/7.37 ( ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 & aElementOf0(W1,szNzAzT0) ) % 7.32/7.37 => ( sdtlseqdt0(W0,W1) % 7.32/7.37 => $true ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mZeroLess,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 => sdtlseqdt0(sz00,W0) ) ). % 7.32/7.37 % 7.32/7.37 fof(mNoScLessZr,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 => ~ sdtlseqdt0(szszuzczcdt0(W0),sz00) ) ). % 7.32/7.37 % 7.32/7.37 fof(mSuccLess,axiom, % 7.32/7.37 ! [W0,W1] : % 7.32/7.37 ( ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 & aElementOf0(W1,szNzAzT0) ) % 7.32/7.37 => ( sdtlseqdt0(W0,W1) % 7.32/7.37 <=> sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(W1)) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mLessSucc,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 => sdtlseqdt0(W0,szszuzczcdt0(W0)) ) ). % 7.32/7.37 % 7.32/7.37 fof(mLessRefl,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 => sdtlseqdt0(W0,W0) ) ). % 7.32/7.37 % 7.32/7.37 fof(mLessASymm,axiom, % 7.32/7.37 ! [W0,W1] : % 7.32/7.37 ( ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 & aElementOf0(W1,szNzAzT0) ) % 7.32/7.37 => ( ( sdtlseqdt0(W0,W1) % 7.32/7.37 & sdtlseqdt0(W1,W0) ) % 7.32/7.37 => W0 = W1 ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mLessTrans,axiom, % 7.32/7.37 ! [W0,W1,W2] : % 7.32/7.37 ( ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 & aElementOf0(W1,szNzAzT0) % 7.32/7.37 & aElementOf0(W2,szNzAzT0) ) % 7.32/7.37 => ( ( sdtlseqdt0(W0,W1) % 7.32/7.37 & sdtlseqdt0(W1,W2) ) % 7.32/7.37 => sdtlseqdt0(W0,W2) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mLessTotal,axiom, % 7.32/7.37 ! [W0,W1] : % 7.32/7.37 ( ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 & aElementOf0(W1,szNzAzT0) ) % 7.32/7.37 => ( sdtlseqdt0(W0,W1) % 7.32/7.37 | sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mIHSort,axiom, % 7.32/7.37 ! [W0,W1] : % 7.32/7.37 ( ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 & aElementOf0(W1,szNzAzT0) ) % 7.32/7.37 => ( iLess0(W0,W1) % 7.32/7.37 => $true ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mIH,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aElementOf0(W0,szNzAzT0) % 7.32/7.37 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 7.32/7.37 % 7.32/7.37 fof(mCardS,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aSet0(W0) % 7.32/7.37 => aElement0(sbrdtbr0(W0)) ) ). % 7.32/7.37 % 7.32/7.37 fof(mCardNum,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aSet0(W0) % 7.32/7.37 => ( aElementOf0(sbrdtbr0(W0),szNzAzT0) % 7.32/7.37 <=> isFinite0(W0) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mCardEmpty,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aSet0(W0) % 7.32/7.37 => ( sbrdtbr0(W0) = sz00 % 7.32/7.37 <=> W0 = slcrc0 ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mCardCons,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( ( aSet0(W0) % 7.32/7.37 & isFinite0(W0) ) % 7.32/7.37 => ! [W1] : % 7.32/7.37 ( aElement0(W1) % 7.32/7.37 => ( ~ aElementOf0(W1,W0) % 7.32/7.37 => sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) ) ). % 7.32/7.37 % 7.32/7.37 fof(mCardDiff,axiom, % 7.32/7.37 ! [W0] : % 7.32/7.37 ( aSet0(W0) % 7.32/7.37 => ! [W1] : % 7.32/7.37 ( ( isFinite0(W0) % 7.32/7.37 & aElementOf0(W1,W0) ) % 7.32/7.38 => szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mCardSub,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aSet0(W0) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( ( isFinite0(W0) % 7.32/7.38 & aSubsetOf0(W1,W0) ) % 7.32/7.38 => sdtlseqdt0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mCardSubEx,axiom, % 7.32/7.38 ! [W0,W1] : % 7.32/7.38 ( ( aSet0(W0) % 7.32/7.38 & aElementOf0(W1,szNzAzT0) ) % 7.32/7.38 => ( ( isFinite0(W0) % 7.32/7.38 & sdtlseqdt0(W1,sbrdtbr0(W0)) ) % 7.32/7.38 => ? [W2] : % 7.32/7.38 ( aSubsetOf0(W2,W0) % 7.32/7.38 & sbrdtbr0(W2) = W1 ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mDefMin,definition, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( ( aSubsetOf0(W0,szNzAzT0) % 7.32/7.38 & W0 != slcrc0 ) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( W1 = szmzizndt0(W0) % 7.32/7.38 <=> ( aElementOf0(W1,W0) % 7.32/7.38 & ! [W2] : % 7.32/7.38 ( aElementOf0(W2,W0) % 7.32/7.38 => sdtlseqdt0(W1,W2) ) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mDefMax,definition, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( ( aSubsetOf0(W0,szNzAzT0) % 7.32/7.38 & isFinite0(W0) % 7.32/7.38 & W0 != slcrc0 ) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( W1 = szmzazxdt0(W0) % 7.32/7.38 <=> ( aElementOf0(W1,W0) % 7.32/7.38 & ! [W2] : % 7.32/7.38 ( aElementOf0(W2,W0) % 7.32/7.38 => sdtlseqdt0(W2,W1) ) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mMinMin,axiom, % 7.32/7.38 ! [W0,W1] : % 7.32/7.38 ( ( aSubsetOf0(W0,szNzAzT0) % 7.32/7.38 & aSubsetOf0(W1,szNzAzT0) % 7.32/7.38 & W0 != slcrc0 % 7.32/7.38 & W1 != slcrc0 ) % 7.32/7.38 => ( ( aElementOf0(szmzizndt0(W0),W1) % 7.32/7.38 & aElementOf0(szmzizndt0(W1),W0) ) % 7.32/7.38 => szmzizndt0(W0) = szmzizndt0(W1) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mDefSeg,definition, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( W1 = slbdtrb0(W0) % 7.32/7.38 <=> ( aSet0(W1) % 7.32/7.38 & ! [W2] : % 7.32/7.38 ( aElementOf0(W2,W1) % 7.32/7.38 <=> ( aElementOf0(W2,szNzAzT0) % 7.32/7.38 & sdtlseqdt0(szszuzczcdt0(W2),W0) ) ) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mSegFin,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 => isFinite0(slbdtrb0(W0)) ) ). % 7.32/7.38 % 7.32/7.38 fof(mSegZero,axiom, % 7.32/7.38 slbdtrb0(sz00) = slcrc0 ). % 7.32/7.38 % 7.32/7.38 fof(mSegSucc,axiom, % 7.32/7.38 ! [W0,W1] : % 7.32/7.38 ( ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 & aElementOf0(W1,szNzAzT0) ) % 7.32/7.38 => ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1))) % 7.32/7.38 <=> ( aElementOf0(W0,slbdtrb0(W1)) % 7.32/7.38 | W0 = W1 ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mSegLess,axiom, % 7.32/7.38 ! [W0,W1] : % 7.32/7.38 ( ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 & aElementOf0(W1,szNzAzT0) ) % 7.32/7.38 => ( sdtlseqdt0(W0,W1) % 7.32/7.38 <=> aSubsetOf0(slbdtrb0(W0),slbdtrb0(W1)) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mFinSubSeg,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( ( aSubsetOf0(W0,szNzAzT0) % 7.32/7.38 & isFinite0(W0) ) % 7.32/7.38 => ? [W1] : % 7.32/7.38 ( aElementOf0(W1,szNzAzT0) % 7.32/7.38 & aSubsetOf0(W0,slbdtrb0(W1)) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mCardSeg,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 => sbrdtbr0(slbdtrb0(W0)) = W0 ) ). % 7.32/7.38 % 7.32/7.38 fof(mDefSel,definition, % 7.32/7.38 ! [W0,W1] : % 7.32/7.38 ( ( aSet0(W0) % 7.32/7.38 & aElementOf0(W1,szNzAzT0) ) % 7.32/7.38 => ! [W2] : % 7.32/7.38 ( W2 = slbdtsldtrb0(W0,W1) % 7.32/7.38 <=> ( aSet0(W2) % 7.32/7.38 & ! [W3] : % 7.32/7.38 ( aElementOf0(W3,W2) % 7.32/7.38 <=> ( aSubsetOf0(W3,W0) % 7.32/7.38 & sbrdtbr0(W3) = W1 ) ) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mSelFSet,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( ( aSet0(W0) % 7.32/7.38 & isFinite0(W0) ) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( aElementOf0(W1,szNzAzT0) % 7.32/7.38 => isFinite0(slbdtsldtrb0(W0,W1)) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mSelNSet,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( ( aSet0(W0) % 7.32/7.38 & ~ isFinite0(W0) ) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( aElementOf0(W1,szNzAzT0) % 7.32/7.38 => slbdtsldtrb0(W0,W1) != slcrc0 ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mSelCSet,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( ( aSet0(W0) % 7.32/7.38 & isCountable0(W0) ) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( ( aElementOf0(W1,szNzAzT0) % 7.32/7.38 & W1 != sz00 ) % 7.32/7.38 => isCountable0(slbdtsldtrb0(W0,W1)) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mSelSub,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 => ! [W1,W2] : % 7.32/7.38 ( ( aSet0(W1) % 7.32/7.38 & aSet0(W2) % 7.32/7.38 & W0 != sz00 ) % 7.32/7.38 => ( ( aSubsetOf0(slbdtsldtrb0(W1,W0),slbdtsldtrb0(W2,W0)) % 7.32/7.38 & slbdtsldtrb0(W1,W0) != slcrc0 ) % 7.32/7.38 => aSubsetOf0(W1,W2) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mSelExtra,axiom, % 7.32/7.38 ! [W0,W1] : % 7.32/7.38 ( ( aSet0(W0) % 7.32/7.38 & aElementOf0(W1,szNzAzT0) ) % 7.32/7.38 => ! [W2] : % 7.32/7.38 ( ( aSubsetOf0(W2,slbdtsldtrb0(W0,W1)) % 7.32/7.38 & isFinite0(W2) ) % 7.32/7.38 => ? [W3] : % 7.32/7.38 ( aSubsetOf0(W3,W0) % 7.32/7.38 & isFinite0(W3) % 7.32/7.38 & aSubsetOf0(W2,slbdtsldtrb0(W3,W1)) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mFunSort,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aFunction0(W0) % 7.32/7.38 => $true ) ). % 7.32/7.38 % 7.32/7.38 fof(mDomSet,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aFunction0(W0) % 7.32/7.38 => aSet0(szDzozmdt0(W0)) ) ). % 7.32/7.38 % 7.32/7.38 fof(mImgElm,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aFunction0(W0) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( aElementOf0(W1,szDzozmdt0(W0)) % 7.32/7.38 => aElement0(sdtlpdtrp0(W0,W1)) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mDefPtt,definition, % 7.32/7.38 ! [W0,W1] : % 7.32/7.38 ( ( aFunction0(W0) % 7.32/7.38 & aElement0(W1) ) % 7.32/7.38 => ! [W2] : % 7.32/7.38 ( W2 = sdtlbdtrb0(W0,W1) % 7.32/7.38 <=> ( aSet0(W2) % 7.32/7.38 & ! [W3] : % 7.32/7.38 ( aElementOf0(W3,W2) % 7.32/7.38 <=> ( aElementOf0(W3,szDzozmdt0(W0)) % 7.32/7.38 & sdtlpdtrp0(W0,W3) = W1 ) ) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mPttSet,axiom, % 7.32/7.38 ! [W0,W1] : % 7.32/7.38 ( ( aFunction0(W0) % 7.32/7.38 & aElement0(W1) ) % 7.32/7.38 => aSubsetOf0(sdtlbdtrb0(W0,W1),szDzozmdt0(W0)) ) ). % 7.32/7.38 % 7.32/7.38 fof(mDefSImg,definition, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aFunction0(W0) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( aSubsetOf0(W1,szDzozmdt0(W0)) % 7.32/7.38 => ! [W2] : % 7.32/7.38 ( W2 = sdtlcdtrc0(W0,W1) % 7.32/7.38 <=> ( aSet0(W2) % 7.32/7.38 & ! [W3] : % 7.32/7.38 ( aElementOf0(W3,W2) % 7.32/7.38 <=> ? [W4] : % 7.32/7.38 ( aElementOf0(W4,W1) % 7.32/7.38 & sdtlpdtrp0(W0,W4) = W3 ) ) ) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mImgRng,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aFunction0(W0) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( aElementOf0(W1,szDzozmdt0(W0)) % 7.32/7.38 => aElementOf0(sdtlpdtrp0(W0,W1),sdtlcdtrc0(W0,szDzozmdt0(W0))) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mDefRst,definition, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aFunction0(W0) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( aSubsetOf0(W1,szDzozmdt0(W0)) % 7.32/7.38 => ! [W2] : % 7.32/7.38 ( W2 = sdtexdt0(W0,W1) % 7.32/7.38 <=> ( aFunction0(W2) % 7.32/7.38 & szDzozmdt0(W2) = W1 % 7.32/7.38 & ! [W3] : % 7.32/7.38 ( aElementOf0(W3,W1) % 7.32/7.38 => sdtlpdtrp0(W2,W3) = sdtlpdtrp0(W0,W3) ) ) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mImgCount,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aFunction0(W0) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( ( aSubsetOf0(W1,szDzozmdt0(W0)) % 7.32/7.38 & isCountable0(W1) ) % 7.32/7.38 => ( ! [W2,W3] : % 7.32/7.38 ( ( aElementOf0(W2,szDzozmdt0(W0)) % 7.32/7.38 & aElementOf0(W3,szDzozmdt0(W0)) % 7.32/7.38 & W2 != W3 ) % 7.32/7.38 => sdtlpdtrp0(W0,W2) != sdtlpdtrp0(W0,W3) ) % 7.32/7.38 => isCountable0(sdtlcdtrc0(W0,W1)) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(mDirichlet,axiom, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aFunction0(W0) % 7.32/7.38 => ( ( isCountable0(szDzozmdt0(W0)) % 7.32/7.38 & isFinite0(sdtlcdtrc0(W0,szDzozmdt0(W0))) ) % 7.32/7.38 => ( aElement0(szDzizrdt0(W0)) % 7.32/7.38 & isCountable0(sdtlbdtrb0(W0,szDzizrdt0(W0))) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__3291,hypothesis, % 7.32/7.38 ( aSet0(xT) % 7.32/7.38 & isFinite0(xT) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__3418,hypothesis, % 7.32/7.38 aElementOf0(xK,szNzAzT0) ). % 7.32/7.38 % 7.32/7.38 fof(m__3435,hypothesis, % 7.32/7.38 ( aSubsetOf0(xS,szNzAzT0) % 7.32/7.38 & isCountable0(xS) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__3453,hypothesis, % 7.32/7.38 ( aFunction0(xc) % 7.32/7.38 & szDzozmdt0(xc) = slbdtsldtrb0(xS,xK) % 7.32/7.38 & aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__3398,hypothesis, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( ( aSubsetOf0(W1,szNzAzT0) % 7.32/7.38 & isCountable0(W1) ) % 7.32/7.38 => ! [W2] : % 7.32/7.38 ( ( aFunction0(W2) % 7.32/7.38 & szDzozmdt0(W2) = slbdtsldtrb0(W1,W0) % 7.32/7.38 & aSubsetOf0(sdtlcdtrc0(W2,szDzozmdt0(W2)),xT) ) % 7.32/7.38 => ( iLess0(W0,xK) % 7.32/7.38 => ? [W3] : % 7.32/7.38 ( aElementOf0(W3,xT) % 7.32/7.38 & ? [W4] : % 7.32/7.38 ( aSubsetOf0(W4,W1) % 7.32/7.38 & isCountable0(W4) % 7.32/7.38 & ! [W5] : % 7.32/7.38 ( aElementOf0(W5,slbdtsldtrb0(W4,W0)) % 7.32/7.38 => sdtlpdtrp0(W2,W5) = W3 ) ) ) ) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__3462,hypothesis, % 7.32/7.38 xK != sz00 ). % 7.32/7.38 % 7.32/7.38 fof(m__3520,hypothesis, % 7.32/7.38 xK != sz00 ). % 7.32/7.38 % 7.32/7.38 fof(m__3533,hypothesis, % 7.32/7.38 ( aElementOf0(xk,szNzAzT0) % 7.32/7.38 & szszuzczcdt0(xk) = xK ) ). % 7.32/7.38 % 7.32/7.38 fof(m__3623,hypothesis, % 7.32/7.38 ( aFunction0(xN) % 7.32/7.38 & szDzozmdt0(xN) = szNzAzT0 % 7.32/7.38 & sdtlpdtrp0(xN,sz00) = xS % 7.32/7.38 & ! [W0] : % 7.32/7.38 ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 => ( ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) % 7.32/7.38 & isCountable0(sdtlpdtrp0(xN,W0)) ) % 7.32/7.38 => ( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) % 7.32/7.38 & isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0))) ) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__3671,hypothesis, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 => ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) % 7.32/7.38 & isCountable0(sdtlpdtrp0(xN,W0)) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__3754,hypothesis, % 7.32/7.38 ! [W0,W1] : % 7.32/7.38 ( ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 & aElementOf0(W1,szNzAzT0) ) % 7.32/7.38 => ( sdtlseqdt0(W1,W0) % 7.32/7.38 => aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1)) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__3821,hypothesis, % 7.32/7.38 ! [W0,W1] : % 7.32/7.38 ( ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 & aElementOf0(W1,szNzAzT0) % 7.32/7.38 & W0 != W1 ) % 7.32/7.38 => szmzizndt0(sdtlpdtrp0(xN,W0)) != szmzizndt0(sdtlpdtrp0(xN,W1)) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__3965,hypothesis, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( ( aSet0(W1) % 7.32/7.38 & aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)) ) % 7.32/7.38 => aElementOf0(sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))),slbdtsldtrb0(xS,xK)) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__4151,hypothesis, % 7.32/7.38 ( aFunction0(xC) % 7.32/7.38 & szDzozmdt0(xC) = szNzAzT0 % 7.32/7.38 & ! [W0] : % 7.32/7.38 ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 => ( aFunction0(sdtlpdtrp0(xC,W0)) % 7.32/7.38 & szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk) % 7.32/7.38 & ! [W1] : % 7.32/7.38 ( ( aSet0(W1) % 7.32/7.38 & aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)) ) % 7.32/7.38 => sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) ) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__4182,hypothesis, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 => aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC,W0),szDzozmdt0(sdtlpdtrp0(xC,W0))),xT) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__4331,hypothesis, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 => ! [W1] : % 7.32/7.38 ( ( aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) % 7.32/7.38 & isCountable0(W1) ) % 7.32/7.38 => ! [W2] : % 7.32/7.38 ( ( aSet0(W2) % 7.32/7.38 & aElementOf0(W2,slbdtsldtrb0(W1,xk)) ) % 7.32/7.38 => aElementOf0(W2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__4411,hypothesis, % 7.32/7.38 ! [W0] : % 7.32/7.38 ( aElementOf0(W0,szNzAzT0) % 7.32/7.38 => ? [W1] : % 7.32/7.38 ( aElementOf0(W1,xT) % 7.32/7.38 & ? [W2] : % 7.32/7.38 ( aSubsetOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) % 7.32/7.38 & isCountable0(W2) % 7.32/7.38 & ! [W3] : % 7.32/7.38 ( ( aSet0(W3) % 7.32/7.38 & aElementOf0(W3,slbdtsldtrb0(W2,xk)) ) % 7.32/7.38 => sdtlpdtrp0(sdtlpdtrp0(xC,W0),W3) = W1 ) ) ) ) ). % 7.32/7.38 % 7.32/7.38 fof(m__4618,hypothesis, % 7.32/7.39 ! [W0] : % 7.32/7.39 ( aElementOf0(W0,szNzAzT0) % 7.32/7.39 => ? [W1] : % 7.32/7.39 ( aElementOf0(W1,xT) % 7.32/7.39 & ! [W2] : % 7.32/7.39 ( ( aSet0(W2) % 7.32/7.39 & aElementOf0(W2,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk)) ) % 7.32/7.39 => sdtlpdtrp0(sdtlpdtrp0(xC,W0),W2) = W1 ) ) ) ). % 7.32/7.39 % 7.32/7.39 fof(m__4660,hypothesis, % 7.32/7.39 ( aFunction0(xe) % 7.32/7.39 & szDzozmdt0(xe) = szNzAzT0 % 7.32/7.39 & ! [W0] : % 7.32/7.39 ( aElementOf0(W0,szNzAzT0) % 7.32/7.39 => sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0)) ) ) ). % 7.32/7.39 % 7.32/7.39 fof(m__4730,hypothesis, % 7.32/7.39 ( aFunction0(xd) % 7.32/7.39 & szDzozmdt0(xd) = szNzAzT0 % 7.32/7.39 & ! [W0] : % 7.32/7.39 ( aElementOf0(W0,szNzAzT0) % 7.32/7.39 => ! [W1] : % 7.32/7.39 ( ( aSet0(W1) % 7.32/7.39 & aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk)) ) % 7.32/7.39 => sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) ) ) ) ). % 7.32/7.39 % 7.32/7.39 fof(m__4758,hypothesis, % 7.32/7.39 aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT) ). % 7.32/7.39 % 7.32/7.39 fof(m__4854,hypothesis, % 7.32/7.39 ( aElementOf0(szDzizrdt0(xd),xT) % 7.32/7.39 & isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ). % 7.32/7.39 % 7.32/7.39 fof(m__4891,hypothesis, % 7.32/7.39 ( aSet0(xO) % 7.32/7.39 & xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ). % 7.32/7.39 % 7.32/7.39 fof(m__4908,hypothesis, % 7.32/7.39 ( aSet0(xO) % 7.32/7.39 & isCountable0(xO) ) ). % 7.32/7.39 % 7.32/7.39 fof(m__4982,hypothesis, % 7.32/7.39 ! [W0] : % 7.32/7.39 ( aElementOf0(W0,xO) % 7.32/7.39 => ? [W1] : % 7.32/7.39 ( aElementOf0(W1,szNzAzT0) % 7.32/7.39 & aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) % 7.32/7.39 & sdtlpdtrp0(xe,W1) = W0 ) ) ). % 7.32/7.39 % 7.32/7.39 fof(m__4998,hypothesis, % 7.32/7.39 aSubsetOf0(xO,xS) ). % 7.32/7.39 % 7.32/7.39 fof(m__5078,hypothesis, % 7.32/7.39 aElementOf0(xQ,slbdtsldtrb0(xO,xK)) ). % 7.32/7.39 % 7.32/7.39 fof(m__5093,hypothesis, % 7.32/7.39 ( aSubsetOf0(xQ,xO) % 7.32/7.39 & xQ != slcrc0 ) ). % 7.32/7.39 % 7.32/7.39 fof(m__5106,hypothesis, % 7.32/7.39 aSubsetOf0(xQ,szNzAzT0) ). % 7.32/7.39 % 7.32/7.39 fof(m__5116,hypothesis, % 7.32/7.39 aElementOf0(xQ,szDzozmdt0(xc)) ). % 7.32/7.39 % 7.32/7.39 fof(m__5147,hypothesis, % 7.32/7.39 xp = szmzizndt0(xQ) ). % 7.32/7.39 % 7.32/7.39 fof(m__5164,hypothesis, % 7.32/7.39 ( aSet0(xP) % 7.32/7.39 & xP = sdtmndt0(xQ,szmzizndt0(xQ)) ) ). % 7.32/7.39 % 7.32/7.39 fof(m__5173,hypothesis, % 7.32/7.39 aElementOf0(xp,xQ) ). % 7.32/7.39 % 7.32/7.39 fof(m__5182,hypothesis, % 7.32/7.39 aElementOf0(xp,xO) ). % 7.32/7.39 % 7.32/7.39 fof(m__5195,hypothesis, % 7.32/7.39 aSubsetOf0(xP,xQ) ). % 7.32/7.39 % 7.32/7.39 fof(m__5208,hypothesis, % 7.32/7.39 aSubsetOf0(xP,xO) ). % 7.32/7.39 % 7.32/7.39 fof(m__5217,hypothesis, % 7.32/7.39 sbrdtbr0(xP) = xk ). % 7.32/7.39 % 7.32/7.39 fof(m__5270,hypothesis, % 7.32/7.39 aElementOf0(xP,slbdtsldtrb0(xO,xk)) ). % 7.32/7.39 % 7.32/7.39 fof(m__5309,hypothesis, % 7.32/7.39 ( aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd))) % 7.32/7.39 & aElementOf0(xn,szNzAzT0) % 7.32/7.39 & sdtlpdtrp0(xe,xn) = xp ) ). % 7.32/7.39 % 7.32/7.39 fof(m__5321,hypothesis, % 7.32/7.39 sdtlpdtrp0(xd,xn) = szDzizrdt0(xd) ). % 7.32/7.39 % 7.32/7.39 fof(m__5334,hypothesis, % 7.32/7.39 aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ). % 7.32/7.39 % 7.32/7.39 fof(m__5585,hypothesis, % 7.32/7.39 xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))) ). % 7.32/7.39 % 7.32/7.39 fof(m__5599,hypothesis, % 7.32/7.39 aElementOf0(xP,slbdtsldtrb0(xD,xk)) ). % 7.32/7.39 % 7.32/7.39 fof(m__,conjecture, % 7.32/7.39 sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) ). % 7.32/7.39 % 7.32/7.39 %------------------------------------------------------------------------------ % 7.32/7.39 %------------------------------------------- % 7.32/7.39 % Proof found % 7.32/7.39 % SZS status Theorem for theBenchmark % 7.32/7.39 % SZS output start Proof % 7.32/7.39 %ClaNum:307(EqnAxiom:92) % 7.32/7.39 %VarNum:1229(SingletonVarNum:358) % 7.32/7.39 %MaxLitNum:9 % 7.32/7.39 %MaxfuncDepth:4 % 7.32/7.39 %SharedTerms:103 % 7.32/7.39 %goalClause: 148 % 7.32/7.39 %singleGoalClaCount:1 % 7.32/7.39 [101]P1(a41) % 7.32/7.39 [102]P1(a54) % 7.32/7.39 [104]P1(a49) % 7.32/7.39 [105]P1(a47) % 7.32/7.39 [106]P5(a37) % 7.32/7.39 [107]P5(a54) % 7.32/7.39 [108]P6(a41) % 7.32/7.39 [109]P6(a55) % 7.32/7.39 [110]P6(a49) % 7.32/7.39 [111]P2(a56) % 7.32/7.39 [112]P2(a48) % 7.32/7.39 [113]P2(a45) % 7.32/7.39 [114]P2(a52) % 7.32/7.39 [115]P2(a53) % 7.32/7.39 [118]P3(a29,a41) % 7.32/7.39 [119]P3(a44,a41) % 7.32/7.39 [120]P3(a51,a41) % 7.32/7.39 [121]P3(a50,a49) % 7.32/7.39 [122]P3(a50,a1) % 7.32/7.39 [123]P3(a57,a41) % 7.32/7.39 [124]P7(a55,a41) % 7.32/7.39 [125]P7(a49,a55) % 7.32/7.39 [126]P7(a1,a41) % 7.32/7.39 [127]P7(a1,a49) % 7.32/7.39 [128]P7(a47,a49) % 7.32/7.39 [129]P7(a47,a1) % 7.32/7.39 [146]~E(a29,a44) % 7.32/7.39 [147]~E(a37,a1) % 7.32/7.39 [93]E(f2(a1),a50) % 7.32/7.39 [94]E(f43(a51),a44) % 7.32/7.39 [95]E(f3(a47),a51) % 7.32/7.39 [96]E(f30(a29),a37) % 7.32/7.39 [97]E(f39(a48),a41) % 7.32/7.39 [98]E(f39(a45),a41) % 7.32/7.39 [99]E(f39(a52),a41) % 7.32/7.39 [100]E(f39(a53),a41) % 7.32/7.39 [116]E(f31(a48,a29),a55) % 7.32/7.39 [117]E(f31(a52,a57),a50) % 7.32/7.39 [130]E(f38(a55,a44),f39(a56)) % 7.32/7.39 [131]E(f31(a53,a57),f40(a53)) % 7.32/7.39 [133]P3(a1,f39(a56)) % 7.32/7.39 [134]P3(f40(a53),a54) % 7.32/7.39 [135]P3(a1,f38(a49,a44)) % 7.32/7.39 [136]P3(a47,f38(a49,a51)) % 7.32/7.39 [137]P3(a47,f38(a46,a51)) % 7.32/7.39 [132]E(f35(a1,f2(a1)),a47) % 7.32/7.39 [138]P6(f32(a53,f40(a53))) % 7.32/7.39 [140]P3(a57,f32(a53,f40(a53))) % 7.32/7.39 [141]P7(a47,f31(a48,f43(a57))) % 7.32/7.39 [142]P7(f34(a56,f39(a56)),a54) % 7.32/7.39 [143]P7(f34(a53,f39(a53)),a54) % 7.32/7.39 [139]E(f34(a52,f32(a53,f40(a53))),a49) % 7.32/7.39 [144]E(f35(f31(a48,a57),f2(f31(a48,a57))),a46) % 7.32/7.39 [148]~E(f31(a56,f36(a47,f2(f31(a48,a57)))),f31(f31(a45,a57),a47)) % 7.32/7.39 [149]P1(x1491)+~E(x1491,a37) % 7.32/7.39 [156]~P1(x1561)+P7(x1561,x1561) % 7.32/7.39 [164]~P3(x1641,a41)+P9(a29,x1641) % 7.32/7.39 [170]P9(x1701,x1701)+~P3(x1701,a41) % 7.32/7.39 [153]~P2(x1531)+P1(f39(x1531)) % 7.32/7.39 [154]~P1(x1541)+P4(f3(x1541)) % 7.32/7.39 [158]~P3(x1581,a41)+~E(f43(x1581),a29) % 7.32/7.39 [159]~P3(x1591,a41)+~E(f43(x1591),x1591) % 7.32/7.39 [161]~P3(x1611,a41)+P5(f30(x1611)) % 7.32/7.39 [162]~P3(x1621,a41)+P6(f15(x1621)) % 7.32/7.39 [171]~P3(x1711,a41)+P3(f43(x1711),a41) % 7.32/7.39 [172]~P3(x1721,a41)+P3(f16(x1721),a54) % 7.32/7.39 [173]~P3(x1731,a41)+P3(f20(x1731),a54) % 7.32/7.39 [174]~P3(x1741,a49)+P3(f21(x1741),a41) % 7.32/7.39 [176]~P3(x1761,a41)+P9(x1761,f43(x1761)) % 7.32/7.39 [177]~P3(x1771,a41)+P8(x1771,f43(x1771)) % 7.32/7.39 [186]~P3(x1861,a41)+P6(f31(a48,x1861)) % 7.32/7.39 [187]~P3(x1871,a41)+P2(f31(a45,x1871)) % 7.32/7.39 [188]~P3(x1881,a41)+~P9(f43(x1881),a29) % 7.32/7.39 [196]~P3(x1961,a41)+P7(f31(a48,x1961),a41) % 7.32/7.39 [163]~P3(x1631,a41)+E(f3(f30(x1631)),x1631) % 7.32/7.39 [175]~P3(x1751,a49)+E(f31(a52,f21(x1751)),x1751) % 7.32/7.39 [198]~P3(x1981,a41)+E(f2(f31(a48,x1981)),f31(a52,x1981)) % 7.32/7.39 [216]~P3(x2161,a49)+P3(f21(x2161),f32(a53,f40(a53))) % 7.32/7.39 [271]~P3(x2711,a41)+P7(f34(f31(a45,x2711),f39(f31(a45,x2711))),a54) % 7.32/7.39 [273]~P3(x2731,a41)+P7(f15(x2731),f35(f31(a48,x2731),f2(f31(a48,x2731)))) % 7.32/7.39 [275]~P3(x2751,a41)+E(f38(f35(f31(a48,x2751),f2(f31(a48,x2751))),a51),f39(f31(a45,x2751))) % 7.32/7.39 [157]~P3(x1572,x1571)+~E(x1571,a37) % 7.32/7.39 [152]~P1(x1521)+~P6(x1521)+~E(x1521,a37) % 7.32/7.39 [155]~P5(x1551)+~P6(x1551)+~P1(x1551) % 7.32/7.39 [150]~P1(x1501)+~E(x1501,a37)+E(f3(x1501),a29) % 7.32/7.39 [151]~P1(x1511)+E(x1511,a37)+~E(f3(x1511),a29) % 7.32/7.39 [160]~P1(x1601)+P3(f4(x1601),x1601)+E(x1601,a37) % 7.32/7.39 [167]~P1(x1671)+~P5(x1671)+P3(f3(x1671),a41) % 7.32/7.39 [178]~P3(x1781,a41)+E(x1781,a29)+P3(f19(x1781),a41) % 7.32/7.39 [179]~P1(x1791)+P5(x1791)+~P3(f3(x1791),a41) % 7.32/7.39 [185]~P5(x1851)+~P7(x1851,a41)+P3(f5(x1851),a41) % 7.32/7.39 [165]~P3(x1651,a41)+E(x1651,a29)+E(f43(f19(x1651)),x1651) % 7.32/7.39 [199]~P5(x1991)+~P7(x1991,a41)+P7(x1991,f30(f5(x1991))) % 7.32/7.39 [168]~P7(x1681,x1682)+P1(x1681)+~P1(x1682) % 7.32/7.39 [169]~P3(x1691,x1692)+P4(x1691)+~P1(x1692) % 7.32/7.39 [166]P1(x1661)+~P3(x1662,a41)+~E(x1661,f30(x1662)) % 7.32/7.39 [200]~P4(x2002)+~P2(x2001)+P7(f32(x2001,x2002),f39(x2001)) % 7.32/7.39 [217]~P2(x2171)+~P3(x2172,f39(x2171))+P4(f31(x2171,x2172)) % 7.32/7.39 [219]~P1(x2191)+~P3(x2192,x2191)+E(f36(f35(x2191,x2192),x2192),x2191) % 7.32/7.39 [255]~P2(x2551)+~P3(x2552,f39(x2551))+P3(f31(x2551,x2552),f34(x2551,f39(x2551))) % 7.32/7.39 [245]~P2(x2451)+~P6(f39(x2451))+P4(f40(x2451))+~P5(f34(x2451,f39(x2451))) % 7.32/7.39 [264]~P2(x2641)+~P6(f39(x2641))+~P5(f34(x2641,f39(x2641)))+P6(f32(x2641,f40(x2641))) % 7.32/7.39 [268]~P3(x2681,a41)+~P7(f31(a48,x2681),a41)+~P6(f31(a48,x2681))+P6(f31(a48,f43(x2681))) % 7.32/7.39 [292]~P3(x2921,a41)+~P7(f31(a48,x2921),a41)+~P6(f31(a48,x2921))+P7(f31(a48,f43(x2921)),f35(f31(a48,x2921),f2(f31(a48,x2921)))) % 7.32/7.39 [180]~P5(x1802)+~P7(x1801,x1802)+P5(x1801)+~P1(x1802) % 7.32/7.39 [184]P3(x1842,x1841)+~E(x1842,f2(x1841))+~P7(x1841,a41)+E(x1841,a37) % 7.32/7.39 [190]~P1(x1901)+~P4(x1902)+~P5(x1901)+P5(f36(x1901,x1902)) % 7.32/7.39 [191]~P1(x1911)+~P4(x1912)+~P5(x1911)+P5(f35(x1911,x1912)) % 7.32/7.39 [192]~P1(x1921)+~P4(x1922)+~P6(x1921)+P6(f36(x1921,x1922)) % 7.32/7.39 [193]~P1(x1931)+~P4(x1932)+~P6(x1931)+P6(f35(x1931,x1932)) % 7.32/7.39 [194]~P1(x1941)+P5(x1941)+~P3(x1942,a41)+~E(f38(x1941,x1942),a37) % 7.32/7.39 [197]E(x1971,x1972)+~E(f43(x1971),f43(x1972))+~P3(x1972,a41)+~P3(x1971,a41) % 7.32/7.39 [203]~P1(x2032)+~P5(x2032)+~P7(x2031,x2032)+P9(f3(x2031),f3(x2032)) % 7.32/7.39 [206]~P1(x2061)+~P5(x2061)+~P3(x2062,a41)+P5(f38(x2061,x2062)) % 7.32/7.39 [215]~P1(x2151)+~P1(x2152)+P7(x2151,x2152)+P3(f22(x2152,x2151),x2151) % 7.32/7.39 [223]P9(x2231,x2232)+P9(f43(x2232),x2231)+~P3(x2232,a41)+~P3(x2231,a41) % 7.32/7.39 [235]~P9(x2351,x2352)+~P3(x2352,a41)+~P3(x2351,a41)+P7(f30(x2351),f30(x2352)) % 7.32/7.39 [236]~P9(x2361,x2362)+~P3(x2362,a41)+~P3(x2361,a41)+P9(f43(x2361),f43(x2362)) % 7.32/7.39 [238]~P1(x2381)+~P1(x2382)+P7(x2381,x2382)+~P3(f22(x2382,x2381),x2382) % 7.32/7.39 [240]P9(x2401,x2402)+~P3(x2402,a41)+~P3(x2401,a41)+~P7(f30(x2401),f30(x2402)) % 7.32/7.39 [241]P9(x2411,x2412)+~P3(x2412,a41)+~P3(x2411,a41)+~P9(f43(x2411),f43(x2412)) % 7.32/7.39 [259]~P9(x2592,x2591)+~P3(x2592,a41)+~P3(x2591,a41)+P7(f31(a48,x2591),f31(a48,x2592)) % 7.32/7.39 [218]P3(x2182,x2181)+~P1(x2181)+~P4(x2182)+E(f35(f36(x2181,x2182),x2182),x2181) % 7.32/7.39 [226]~E(x2261,x2262)+~P3(x2262,a41)+~P3(x2261,a41)+P3(x2261,f30(f43(x2262))) % 7.32/7.39 [247]~P3(x2472,a41)+~P3(x2471,a41)+~P3(x2471,f30(x2472))+P3(x2471,f30(f43(x2472))) % 7.32/7.39 [263]E(x2631,x2632)+~P3(x2632,a41)+~P3(x2631,a41)+~E(f2(f31(a48,x2631)),f2(f31(a48,x2632))) % 7.32/7.39 [266]~P1(x2662)+~P3(x2661,a41)+E(f31(f31(a45,x2661),x2662),f16(x2661))+~P3(x2662,f38(f15(x2661),a51)) % 7.32/7.39 [246]~P1(x2461)+~P5(x2461)+~P3(x2462,x2461)+E(f43(f3(f35(x2461,x2462))),f3(x2461)) % 7.32/7.39 [276]~P1(x2762)+~P3(x2761,a41)+E(f31(f31(a45,x2761),x2762),f20(x2761))+~P3(x2762,f38(f31(a48,f43(x2761)),a51)) % 7.32/7.39 [278]~P1(x2782)+~P3(x2781,a41)+E(f31(f31(a45,x2781),x2782),f31(a53,x2781))+~P3(x2782,f38(f31(a48,f43(x2781)),a51)) % 7.32/7.39 [306]~P1(x3061)+~P3(x3062,a41)+P3(f36(x3061,f2(f31(a48,x3062))),f38(a55,a44))+~P3(x3061,f38(f35(f31(a48,x3062),f2(f31(a48,x3062))),a51)) % 7.32/7.39 [307]~P1(x3071)+~P3(x3072,a41)+~P3(x3071,f38(f35(f31(a48,x3072),f2(f31(a48,x3072))),a51))+E(f31(a56,f36(x3071,f2(f31(a48,x3072)))),f31(f31(a45,x3072),x3071)) % 7.32/7.39 [210]~P1(x2102)+~P7(x2103,x2102)+P3(x2101,x2102)+~P3(x2101,x2103) % 7.32/7.39 [181]~P1(x1812)+~P4(x1813)+P1(x1811)+~E(x1811,f36(x1812,x1813)) % 7.32/7.39 [182]~P1(x1822)+~P4(x1823)+P1(x1821)+~E(x1821,f35(x1822,x1823)) % 7.32/7.39 [183]~P4(x1833)+~P2(x1832)+P1(x1831)+~E(x1831,f32(x1832,x1833)) % 7.32/7.39 [195]~P1(x1952)+P1(x1951)+~P3(x1953,a41)+~E(x1951,f38(x1952,x1953)) % 7.32/7.39 [204]~P3(x2041,x2042)+~P3(x2043,a41)+P3(x2041,a41)+~E(x2042,f30(x2043)) % 7.32/7.39 [212]~P2(x2122)+P1(x2121)+~P7(x2123,f39(x2122))+~E(x2121,f34(x2122,x2123)) % 7.32/7.39 [213]~P2(x2132)+P2(x2131)+~P7(x2133,f39(x2132))+~E(x2131,f33(x2132,x2133)) % 7.32/7.39 [214]~P2(x2143)+~P7(x2142,f39(x2143))+E(f39(x2141),x2142)+~E(x2141,f33(x2143,x2142)) % 7.32/7.39 [220]~P3(x2201,x2203)+~P3(x2202,a41)+P9(f43(x2201),x2202)+~E(x2203,f30(x2202)) % 7.32/7.39 [201]~P1(x2012)+~P1(x2011)+~P7(x2012,x2011)+~P7(x2011,x2012)+E(x2011,x2012) % 7.32/7.39 [233]~P9(x2332,x2331)+~P9(x2331,x2332)+E(x2331,x2332)+~P3(x2332,a41)+~P3(x2331,a41) % 7.32/7.39 [189]~P5(x1891)+P3(x1892,x1891)+~E(x1892,f42(x1891))+~P7(x1891,a41)+E(x1891,a37) % 7.32/7.39 [209]~P1(x2092)+~P6(x2092)+~P3(x2091,a41)+E(x2091,a29)+P6(f38(x2092,x2091)) % 7.32/7.39 [237]~P3(x2372,x2371)+P3(f25(x2371,x2372),x2371)+~P7(x2371,a41)+E(x2371,a37)+E(x2372,f2(x2371)) % 7.32/7.39 [248]~P1(x2481)+~P5(x2481)+~P3(x2482,a41)+~P9(x2482,f3(x2481))+P7(f26(x2481,x2482),x2481) % 7.32/7.39 [250]~P1(x2501)+P3(f28(x2502,x2501),x2501)+~P3(x2502,a41)+E(x2501,f30(x2502))+P3(f28(x2502,x2501),a41) % 7.32/7.39 [251]~P3(x2512,x2511)+~P7(x2511,a41)+~P9(x2512,f25(x2511,x2512))+E(x2511,a37)+E(x2512,f2(x2511)) % 7.32/7.39 [258]~P6(x2582)+~P2(x2581)+~E(f6(x2581,x2582),f7(x2581,x2582))+~P7(x2582,f39(x2581))+P6(f34(x2581,x2582)) % 7.32/7.39 [260]~P6(x2602)+~P2(x2601)+P3(f7(x2601,x2602),f39(x2601))+~P7(x2602,f39(x2601))+P6(f34(x2601,x2602)) % 7.32/7.39 [261]~P6(x2612)+~P2(x2611)+P3(f6(x2611,x2612),f39(x2611))+~P7(x2612,f39(x2611))+P6(f34(x2611,x2612)) % 7.32/7.39 [225]P3(x2252,x2251)+~P1(x2251)+~P4(x2252)+~P5(x2251)+E(f3(f36(x2251,x2252)),f43(f3(x2251))) % 7.32/7.39 [244]~P1(x2441)+~P5(x2441)+~P3(x2442,a41)+~P9(x2442,f3(x2441))+E(f3(f26(x2441,x2442)),x2442) % 7.32/7.39 [253]E(x2531,x2532)+P3(x2531,f30(x2532))+~P3(x2532,a41)+~P3(x2531,a41)+~P3(x2531,f30(f43(x2532))) % 7.32/7.39 [265]~P1(x2651)+P3(f28(x2652,x2651),x2651)+~P3(x2652,a41)+E(x2651,f30(x2652))+P9(f43(f28(x2652,x2651)),x2652) % 7.32/7.39 [267]~P6(x2672)+~P2(x2671)+~P7(x2672,f39(x2671))+P6(f34(x2671,x2672))+E(f31(x2671,f6(x2671,x2672)),f31(x2671,f7(x2671,x2672))) % 7.32/7.39 [211]~P3(x2113,x2111)+P9(x2112,x2113)+~E(x2112,f2(x2111))+~P7(x2111,a41)+E(x2111,a37) % 7.32/7.39 [239]P3(x2391,x2392)+~P3(x2393,a41)+~P3(x2391,a41)+~P9(f43(x2391),x2393)+~E(x2392,f30(x2393)) % 7.32/7.39 [272]~P1(x2721)+~P5(x2723)+~P3(x2722,a41)+~P7(x2723,f38(x2721,x2722))+P5(f9(x2721,x2722,x2723)) % 7.32/7.39 [274]~P1(x2741)+~P5(x2743)+~P3(x2742,a41)+~P7(x2743,f38(x2741,x2742))+P7(f9(x2741,x2742,x2743),x2741) % 7.32/7.39 [293]~P1(x2932)+~P5(x2931)+~P3(x2933,a41)+~P7(x2931,f38(x2932,x2933))+P7(x2931,f38(f9(x2932,x2933,x2931),x2933)) % 7.32/7.39 [205]~P1(x2054)+~P4(x2052)+~P3(x2051,x2053)+~E(x2051,x2052)+~E(x2053,f35(x2054,x2052)) % 7.32/7.39 [207]~P1(x2073)+~P4(x2074)+~P3(x2071,x2072)+P4(x2071)+~E(x2072,f36(x2073,x2074)) % 7.32/7.39 [208]~P1(x2083)+~P4(x2084)+~P3(x2081,x2082)+P4(x2081)+~E(x2082,f35(x2083,x2084)) % 7.32/7.39 [222]~P1(x2222)+~P4(x2224)+~P3(x2221,x2223)+P3(x2221,x2222)+~E(x2223,f35(x2222,x2224)) % 7.32/7.39 [224]~P4(x2243)+~P2(x2241)+~P3(x2242,x2244)+E(f31(x2241,x2242),x2243)+~E(x2244,f32(x2241,x2243)) % 7.32/7.39 [228]~P1(x2284)+~P3(x2281,x2283)+~P3(x2282,a41)+E(f3(x2281),x2282)+~E(x2283,f38(x2284,x2282)) % 7.32/7.39 [230]~P4(x2304)+~P2(x2302)+~P3(x2301,x2303)+P3(x2301,f39(x2302))+~E(x2303,f32(x2302,x2304)) % 7.32/7.39 [234]~P1(x2342)+~P3(x2341,x2343)+P7(x2341,x2342)+~P3(x2344,a41)+~E(x2343,f38(x2342,x2344)) % 7.32/7.39 [252]~P2(x2523)+~P3(x2522,x2524)+~P7(x2524,f39(x2523))+E(f31(x2521,x2522),f31(x2523,x2522))+~E(x2521,f33(x2523,x2524)) % 7.32/7.39 [299]~P2(x2991)+~P3(x2994,x2993)+~E(x2993,f34(x2991,x2992))+~P7(x2992,f39(x2991))+P3(f13(x2991,x2992,x2993,x2994),x2992) % 7.32/7.39 [300]~P2(x3001)+~P3(x3004,x3003)+~E(x3003,f34(x3001,x3002))+~P7(x3002,f39(x3001))+E(f31(x3001,f13(x3001,x3002,x3003,x3004)),x3004) % 7.32/7.39 [243]~P5(x2431)+~P3(x2432,x2431)+P3(f27(x2431,x2432),x2431)+~P7(x2431,a41)+E(x2431,a37)+E(x2432,f42(x2431)) % 7.32/7.39 [256]~P5(x2561)+~P3(x2562,x2561)+~P7(x2561,a41)+~P9(f27(x2561,x2562),x2562)+E(x2561,a37)+E(x2562,f42(x2561)) % 7.32/7.39 [281]~P1(x2811)+~P3(x2812,a41)+~P3(f28(x2812,x2811),x2811)+E(x2811,f30(x2812))+~P3(f28(x2812,x2811),a41)+~P9(f43(f28(x2812,x2811)),x2812) % 7.32/7.39 [229]~P1(x2292)+~P1(x2291)+~P7(x2293,x2292)+~P7(x2291,x2293)+P7(x2291,x2292)+~P1(x2293) % 7.32/7.39 [257]~P9(x2571,x2573)+P9(x2571,x2572)+~P9(x2573,x2572)+~P3(x2572,a41)+~P3(x2573,a41)+~P3(x2571,a41) % 7.32/7.39 [221]~P5(x2211)+~P3(x2212,x2211)+P9(x2212,x2213)+~E(x2213,f42(x2211))+~P7(x2211,a41)+E(x2211,a37) % 7.32/7.39 [270]~P2(x2701)+~P2(x2702)+P3(f8(x2702,x2703,x2701),x2703)+~E(f39(x2701),x2703)+~P7(x2703,f39(x2702))+E(x2701,f33(x2702,x2703)) % 7.32/7.39 [277]~P1(x2771)+~P1(x2772)+~P4(x2773)+P3(f23(x2772,x2773,x2771),x2771)+~E(f23(x2772,x2773,x2771),x2773)+E(x2771,f35(x2772,x2773)) % 7.32/7.39 [279]~P1(x2791)+~P1(x2792)+~P4(x2793)+P3(f24(x2792,x2793,x2791),x2791)+E(x2791,f36(x2792,x2793))+P4(f24(x2792,x2793,x2791)) % 7.32/7.39 [280]~P1(x2801)+~P1(x2802)+~P4(x2803)+P3(f23(x2802,x2803,x2801),x2801)+E(x2801,f35(x2802,x2803))+P4(f23(x2802,x2803,x2801)) % 7.32/7.39 [282]~P1(x2821)+~P1(x2822)+~P4(x2823)+P3(f23(x2822,x2823,x2821),x2821)+P3(f23(x2822,x2823,x2821),x2822)+E(x2821,f35(x2822,x2823)) % 7.32/7.39 [285]~P1(x2851)+~P4(x2853)+~P2(x2852)+P3(f11(x2852,x2853,x2851),x2851)+P3(f11(x2852,x2853,x2851),f39(x2852))+E(x2851,f32(x2852,x2853)) % 7.32/7.39 [286]~P1(x2861)+~P1(x2862)+P3(f10(x2862,x2863,x2861),x2861)+P7(f10(x2862,x2863,x2861),x2862)+~P3(x2863,a41)+E(x2861,f38(x2862,x2863)) % 7.32/7.39 [289]~P1(x2891)+~P2(x2892)+P3(f12(x2892,x2893,x2891),x2891)+P3(f14(x2892,x2893,x2891),x2893)+~P7(x2893,f39(x2892))+E(x2891,f34(x2892,x2893)) % 7.32/7.39 [283]~P1(x2831)+~P4(x2833)+~P2(x2832)+P3(f11(x2832,x2833,x2831),x2831)+E(x2831,f32(x2832,x2833))+E(f31(x2832,f11(x2832,x2833,x2831)),x2833) % 7.32/7.39 [284]~P1(x2841)+~P1(x2842)+P3(f10(x2842,x2843,x2841),x2841)+~P3(x2843,a41)+E(x2841,f38(x2842,x2843))+E(f3(f10(x2842,x2843,x2841)),x2843) % 7.32/7.39 [294]~P1(x2941)+~P2(x2942)+P3(f12(x2942,x2943,x2941),x2941)+~P7(x2943,f39(x2942))+E(x2941,f34(x2942,x2943))+E(f31(x2942,f14(x2942,x2943,x2941)),f12(x2942,x2943,x2941)) % 7.32/7.39 [296]~P2(x2962)+~P2(x2961)+~E(f39(x2961),x2963)+~P7(x2963,f39(x2962))+E(x2961,f33(x2962,x2963))+~E(f31(x2961,f8(x2962,x2963,x2961)),f31(x2962,f8(x2962,x2963,x2961))) % 7.32/7.39 [305]~P1(x3051)+~P6(x3053)+~P3(x3052,a41)+~P3(x3051,f38(x3053,a51))+~P7(x3053,f35(f31(a48,x3052),f2(f31(a48,x3052))))+P3(x3051,f38(f35(f31(a48,x3052),f2(f31(a48,x3052))),a51)) % 7.32/7.39 [202]~P1(x2024)+~P4(x2023)+~P4(x2021)+P3(x2021,x2022)+~E(x2021,x2023)+~E(x2022,f36(x2024,x2023)) % 7.32/7.39 [227]~P1(x2273)+~P4(x2272)+~P3(x2271,x2274)+E(x2271,x2272)+P3(x2271,x2273)+~E(x2274,f36(x2273,x2272)) % 7.32/7.39 [231]~P1(x2313)+~P4(x2314)+~P4(x2311)+~P3(x2311,x2313)+P3(x2311,x2312)+~E(x2312,f36(x2313,x2314)) % 7.32/7.39 [242]~P1(x2424)+~P7(x2421,x2424)+P3(x2421,x2422)+~P3(x2423,a41)+~E(x2422,f38(x2424,x2423))+~E(f3(x2421),x2423) % 7.32/7.39 [249]~P4(x2494)+~P2(x2493)+P3(x2491,x2492)+~E(f31(x2493,x2491),x2494)+~P3(x2491,f39(x2493))+~E(x2492,f32(x2493,x2494)) % 7.32/7.39 [262]~P2(x2623)+~P3(x2625,x2624)+P3(x2621,x2622)+~P7(x2624,f39(x2623))+~E(x2622,f34(x2623,x2624))+~E(f31(x2623,x2625),x2621) % 7.32/7.39 [254]E(f2(x2542),f2(x2541))+~P7(x2541,a41)+~P7(x2542,a41)+~P3(f2(x2541),x2542)+~P3(f2(x2542),x2541)+E(x2541,a37)+E(x2542,a37) % 7.32/7.39 [269]~P1(x2693)+~P1(x2692)+P7(x2692,x2693)+~P3(x2691,a41)+~P7(f38(x2692,x2691),f38(x2693,x2691))+E(x2691,a29)+E(f38(x2692,x2691),a37) % 7.32/7.39 [291]~P1(x2911)+~P1(x2912)+~P4(x2913)+E(f24(x2912,x2913,x2911),x2913)+P3(f24(x2912,x2913,x2911),x2911)+P3(f24(x2912,x2913,x2911),x2912)+E(x2911,f36(x2912,x2913)) % 7.32/7.39 [297]~P1(x2971)+~P1(x2972)+~P4(x2973)+~E(f24(x2972,x2973,x2971),x2973)+~P3(f24(x2972,x2973,x2971),x2971)+E(x2971,f36(x2972,x2973))+~P4(f24(x2972,x2973,x2971)) % 7.32/7.39 [298]~P1(x2981)+~P1(x2982)+~P4(x2983)+~P3(f24(x2982,x2983,x2981),x2981)+~P3(f24(x2982,x2983,x2981),x2982)+E(x2981,f36(x2982,x2983))+~P4(f24(x2982,x2983,x2981)) % 7.32/7.39 [301]~P1(x3011)+~P1(x3012)+~P3(x3013,a41)+~P3(f10(x3012,x3013,x3011),x3011)+~P7(f10(x3012,x3013,x3011),x3012)+E(x3011,f38(x3012,x3013))+~E(f3(f10(x3012,x3013,x3011)),x3013) % 7.32/7.39 [302]~P1(x3021)+~P4(x3023)+~P2(x3022)+~P3(f11(x3022,x3023,x3021),x3021)+~P3(f11(x3022,x3023,x3021),f39(x3022))+E(x3021,f32(x3022,x3023))+~E(f31(x3022,f11(x3022,x3023,x3021)),x3023) % 7.32/7.39 [232]~P1(x2324)+~P4(x2322)+~P4(x2321)+~P3(x2321,x2324)+E(x2321,x2322)+P3(x2321,x2323)+~E(x2323,f35(x2324,x2322)) % 7.32/7.39 [295]~P1(x2951)+~P2(x2952)+~P3(x2954,x2953)+~P7(x2953,f39(x2952))+~P3(f12(x2952,x2953,x2951),x2951)+~E(f31(x2952,x2954),f12(x2952,x2953,x2951))+E(x2951,f34(x2952,x2953)) % 7.32/7.39 [303]~P1(x3031)+~P1(x3032)+~P4(x3033)+E(f23(x3032,x3033,x3031),x3033)+~P3(f23(x3032,x3033,x3031),x3031)+~P3(f23(x3032,x3033,x3031),x3032)+E(x3031,f35(x3032,x3033))+~P4(f23(x3032,x3033,x3031)) % 7.32/7.39 [287]~P6(x2872)+~P2(x2873)+~E(f39(x2873),f38(x2872,x2871))+~P3(x2871,a41)+~P7(x2872,a41)+~P8(x2871,a44)+P6(f17(x2871,x2872,x2873))+~P7(f34(x2873,f39(x2873)),a54) % 7.32/7.39 [288]~P6(x2882)+~P2(x2883)+~E(f39(x2883),f38(x2882,x2881))+~P3(x2881,a41)+~P7(x2882,a41)+~P8(x2881,a44)+P3(f18(x2881,x2882,x2883),a54)+~P7(f34(x2883,f39(x2883)),a54) % 7.32/7.39 [290]~P6(x2902)+~P2(x2903)+~E(f39(x2903),f38(x2902,x2901))+~P3(x2901,a41)+~P7(x2902,a41)+~P8(x2901,a44)+P7(f17(x2901,x2902,x2903),x2902)+~P7(f34(x2903,f39(x2903)),a54) % 7.32/7.39 [304]~P6(x3044)+~P2(x3041)+~E(f39(x3041),f38(x3044,x3043))+~P3(x3043,a41)+~P7(x3044,a41)+~P8(x3043,a44)+E(f31(x3041,x3042),f18(x3043,x3044,x3041))+~P3(x3042,f38(f17(x3043,x3044,x3041),x3043))+~P7(f34(x3041,f39(x3041)),a54) % 7.32/7.39 %EqnAxiom % 7.32/7.39 [1]E(x11,x11) % 7.32/7.39 [2]E(x22,x21)+~E(x21,x22) % 7.32/7.39 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 7.32/7.39 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 7.32/7.39 [5]~E(x51,x52)+E(f43(x51),f43(x52)) % 7.32/7.39 [6]~E(x61,x62)+E(f3(x61),f3(x62)) % 7.32/7.39 [7]~E(x71,x72)+E(f30(x71),f30(x72)) % 7.32/7.39 [8]~E(x81,x82)+E(f39(x81),f39(x82)) % 7.32/7.39 [9]~E(x91,x92)+E(f9(x91,x93,x94),f9(x92,x93,x94)) % 7.32/7.39 [10]~E(x101,x102)+E(f9(x103,x101,x104),f9(x103,x102,x104)) % 7.32/7.39 [11]~E(x111,x112)+E(f9(x113,x114,x111),f9(x113,x114,x112)) % 7.32/7.39 [12]~E(x121,x122)+E(f31(x121,x123),f31(x122,x123)) % 7.32/7.39 [13]~E(x131,x132)+E(f31(x133,x131),f31(x133,x132)) % 7.32/7.39 [14]~E(x141,x142)+E(f28(x141,x143),f28(x142,x143)) % 7.32/7.39 [15]~E(x151,x152)+E(f28(x153,x151),f28(x153,x152)) % 7.32/7.39 [16]~E(x161,x162)+E(f38(x161,x163),f38(x162,x163)) % 7.32/7.39 [17]~E(x171,x172)+E(f38(x173,x171),f38(x173,x172)) % 7.32/7.39 [18]~E(x181,x182)+E(f23(x181,x183,x184),f23(x182,x183,x184)) % 7.32/7.39 [19]~E(x191,x192)+E(f23(x193,x191,x194),f23(x193,x192,x194)) % 7.32/7.39 [20]~E(x201,x202)+E(f23(x203,x204,x201),f23(x203,x204,x202)) % 7.32/7.39 [21]~E(x211,x212)+E(f34(x211,x213),f34(x212,x213)) % 7.32/7.39 [22]~E(x221,x222)+E(f34(x223,x221),f34(x223,x222)) % 7.32/7.39 [23]~E(x231,x232)+E(f35(x231,x233),f35(x232,x233)) % 7.32/7.39 [24]~E(x241,x242)+E(f35(x243,x241),f35(x243,x242)) % 7.32/7.39 [25]~E(x251,x252)+E(f36(x251,x253),f36(x252,x253)) % 7.32/7.39 [26]~E(x261,x262)+E(f36(x263,x261),f36(x263,x262)) % 7.32/7.39 [27]~E(x271,x272)+E(f40(x271),f40(x272)) % 7.32/7.39 [28]~E(x281,x282)+E(f10(x281,x283,x284),f10(x282,x283,x284)) % 7.32/7.39 [29]~E(x291,x292)+E(f10(x293,x291,x294),f10(x293,x292,x294)) % 7.32/7.39 [30]~E(x301,x302)+E(f10(x303,x304,x301),f10(x303,x304,x302)) % 7.32/7.39 [31]~E(x311,x312)+E(f18(x311,x313,x314),f18(x312,x313,x314)) % 7.32/7.39 [32]~E(x321,x322)+E(f18(x323,x321,x324),f18(x323,x322,x324)) % 7.32/7.39 [33]~E(x331,x332)+E(f18(x333,x334,x331),f18(x333,x334,x332)) % 7.32/7.39 [34]~E(x341,x342)+E(f32(x341,x343),f32(x342,x343)) % 7.32/7.39 [35]~E(x351,x352)+E(f32(x353,x351),f32(x353,x352)) % 7.32/7.39 [36]~E(x361,x362)+E(f21(x361),f21(x362)) % 7.32/7.39 [37]~E(x371,x372)+E(f6(x371,x373),f6(x372,x373)) % 7.32/7.39 [38]~E(x381,x382)+E(f6(x383,x381),f6(x383,x382)) % 7.32/7.39 [39]~E(x391,x392)+E(f12(x391,x393,x394),f12(x392,x393,x394)) % 7.32/7.39 [40]~E(x401,x402)+E(f12(x403,x401,x404),f12(x403,x402,x404)) % 7.32/7.39 [41]~E(x411,x412)+E(f12(x413,x414,x411),f12(x413,x414,x412)) % 7.32/7.39 [42]~E(x421,x422)+E(f33(x421,x423),f33(x422,x423)) % 7.32/7.39 [43]~E(x431,x432)+E(f33(x433,x431),f33(x433,x432)) % 7.32/7.39 [44]~E(x441,x442)+E(f22(x441,x443),f22(x442,x443)) % 7.32/7.39 [45]~E(x451,x452)+E(f22(x453,x451),f22(x453,x452)) % 7.32/7.39 [46]~E(x461,x462)+E(f26(x461,x463),f26(x462,x463)) % 7.32/7.39 [47]~E(x471,x472)+E(f26(x473,x471),f26(x473,x472)) % 7.32/7.39 [48]~E(x481,x482)+E(f17(x481,x483,x484),f17(x482,x483,x484)) % 7.32/7.39 [49]~E(x491,x492)+E(f17(x493,x491,x494),f17(x493,x492,x494)) % 7.32/7.39 [50]~E(x501,x502)+E(f17(x503,x504,x501),f17(x503,x504,x502)) % 7.32/7.39 [51]~E(x511,x512)+E(f24(x511,x513,x514),f24(x512,x513,x514)) % 7.32/7.39 [52]~E(x521,x522)+E(f24(x523,x521,x524),f24(x523,x522,x524)) % 7.32/7.39 [53]~E(x531,x532)+E(f24(x533,x534,x531),f24(x533,x534,x532)) % 7.32/7.39 [54]~E(x541,x542)+E(f11(x541,x543,x544),f11(x542,x543,x544)) % 7.32/7.39 [55]~E(x551,x552)+E(f11(x553,x551,x554),f11(x553,x552,x554)) % 7.32/7.39 [56]~E(x561,x562)+E(f11(x563,x564,x561),f11(x563,x564,x562)) % 7.32/7.39 [57]~E(x571,x572)+E(f7(x571,x573),f7(x572,x573)) % 7.32/7.39 [58]~E(x581,x582)+E(f7(x583,x581),f7(x583,x582)) % 7.32/7.39 [59]~E(x591,x592)+E(f27(x591,x593),f27(x592,x593)) % 7.32/7.39 [60]~E(x601,x602)+E(f27(x603,x601),f27(x603,x602)) % 7.32/7.39 [61]~E(x611,x612)+E(f42(x611),f42(x612)) % 7.32/7.39 [62]~E(x621,x622)+E(f15(x621),f15(x622)) % 7.32/7.39 [63]~E(x631,x632)+E(f16(x631),f16(x632)) % 7.32/7.39 [64]~E(x641,x642)+E(f5(x641),f5(x642)) % 7.32/7.39 [65]~E(x651,x652)+E(f13(x651,x653,x654,x655),f13(x652,x653,x654,x655)) % 7.32/7.39 [66]~E(x661,x662)+E(f13(x663,x661,x664,x665),f13(x663,x662,x664,x665)) % 7.32/7.39 [67]~E(x671,x672)+E(f13(x673,x674,x671,x675),f13(x673,x674,x672,x675)) % 7.32/7.39 [68]~E(x681,x682)+E(f13(x683,x684,x685,x681),f13(x683,x684,x685,x682)) % 7.32/7.39 [69]~E(x691,x692)+E(f14(x691,x693,x694),f14(x692,x693,x694)) % 7.32/7.39 [70]~E(x701,x702)+E(f14(x703,x701,x704),f14(x703,x702,x704)) % 7.32/7.39 [71]~E(x711,x712)+E(f14(x713,x714,x711),f14(x713,x714,x712)) % 7.32/7.39 [72]~E(x721,x722)+E(f19(x721),f19(x722)) % 7.32/7.39 [73]~E(x731,x732)+E(f20(x731),f20(x732)) % 7.32/7.39 [74]~E(x741,x742)+E(f25(x741,x743),f25(x742,x743)) % 7.32/7.39 [75]~E(x751,x752)+E(f25(x753,x751),f25(x753,x752)) % 7.32/7.39 [76]~E(x761,x762)+E(f8(x761,x763,x764),f8(x762,x763,x764)) % 7.32/7.39 [77]~E(x771,x772)+E(f8(x773,x771,x774),f8(x773,x772,x774)) % 7.32/7.39 [78]~E(x781,x782)+E(f8(x783,x784,x781),f8(x783,x784,x782)) % 7.32/7.39 [79]~E(x791,x792)+E(f4(x791),f4(x792)) % 7.32/7.39 [80]~P1(x801)+P1(x802)+~E(x801,x802) % 7.32/7.39 [81]P3(x812,x813)+~E(x811,x812)+~P3(x811,x813) % 7.32/7.39 [82]P3(x823,x822)+~E(x821,x822)+~P3(x823,x821) % 7.32/7.39 [83]~P6(x831)+P6(x832)+~E(x831,x832) % 7.32/7.39 [84]P9(x842,x843)+~E(x841,x842)+~P9(x841,x843) % 7.32/7.39 [85]P9(x853,x852)+~E(x851,x852)+~P9(x853,x851) % 7.32/7.39 [86]~P2(x861)+P2(x862)+~E(x861,x862) % 7.32/7.39 [87]~P5(x871)+P5(x872)+~E(x871,x872) % 7.32/7.39 [88]P7(x882,x883)+~E(x881,x882)+~P7(x881,x883) % 7.32/7.39 [89]P7(x893,x892)+~E(x891,x892)+~P7(x893,x891) % 7.32/7.39 [90]~P4(x901)+P4(x902)+~E(x901,x902) % 7.32/7.39 [91]P8(x912,x913)+~E(x911,x912)+~P8(x911,x913) % 7.32/7.39 [92]P8(x923,x922)+~E(x921,x922)+~P8(x923,x921) % 7.32/7.39 % 7.32/7.39 %------------------------------------------- % 7.32/7.39 cnf(308,plain, % 7.32/7.39 (P1(a37)), % 7.32/7.39 inference(equality_inference,[],[149])). % 7.32/7.39 cnf(309,plain, % 7.32/7.39 (~P1(a37)+E(f3(a37),a29)), % 7.32/7.39 inference(equality_inference,[],[150])). % 7.32/7.39 cnf(310,plain, % 7.32/7.39 (~P6(a37)+~P1(a37)), % 7.32/7.39 inference(equality_inference,[],[152])). % 7.32/7.39 cnf(311,plain, % 7.32/7.39 (~P3(x3111,a37)), % 7.32/7.39 inference(equality_inference,[],[157])). % 7.32/7.39 cnf(312,plain, % 7.32/7.39 (P1(f30(x3121))+~P3(x3121,a41)), % 7.32/7.39 inference(equality_inference,[],[166])). % 7.32/7.39 cnf(316,plain, % 7.32/7.39 (P3(f2(x3161),x3161)+~P7(x3161,a41)+E(x3161,a37)), % 7.32/7.39 inference(equality_inference,[],[184])). % 7.32/7.39 cnf(318,plain, % 7.32/7.39 (~P1(x3181)+P1(f38(x3181,x3182))+~P3(x3182,a41)), % 7.32/7.39 inference(equality_inference,[],[195])). % 7.32/7.39 cnf(324,plain, % 7.32/7.39 (~P2(x3241)+P1(f34(x3241,x3242))+~P7(x3242,f39(x3241))), % 7.32/7.39 inference(equality_inference,[],[212])). % 7.32/7.39 cnf(325,plain, % 7.32/7.39 (~P2(x3251)+P2(f33(x3251,x3252))+~P7(x3252,f39(x3251))), % 7.32/7.39 inference(equality_inference,[],[213])). % 7.32/7.39 cnf(326,plain, % 7.32/7.39 (~P2(x3261)+~P7(x3262,f39(x3261))+E(f39(f33(x3261,x3262)),x3262)), % 7.32/7.39 inference(equality_inference,[],[214])). % 7.32/7.39 cnf(331,plain, % 7.32/7.39 (~P3(x3311,a41)+~P3(x3311,a41)+P3(x3311,f30(f43(x3311)))), % 7.32/7.39 inference(equality_inference,[],[226])). % 7.32/7.39 cnf(337,plain, % 7.32/7.39 (P7(x3371,x3372)+~P1(x3372)+~P3(x3371,f38(x3372,x3373))+~P3(x3373,a41)), % 7.32/7.39 inference(equality_inference,[],[234])). % 7.32/7.39 cnf(338,plain, % 7.32/7.39 (P3(x3381,f30(x3382))+~P3(x3381,a41)+~P9(f43(x3381),x3382)+~P3(x3382,a41)), % 7.32/7.39 inference(equality_inference,[],[239])). % 7.32/7.39 cnf(339,plain, % 7.32/7.39 (~P2(x3391)+~P3(x3392,x3393)+~P7(x3393,f39(x3391))+E(f31(f33(x3391,x3393),x3392),f31(x3391,x3392))), % 7.32/7.39 inference(equality_inference,[],[252])). % 7.32/7.39 cnf(344,plain, % 7.32/7.39 (E(f3(a37),a29)), % 7.32/7.39 inference(scs_inference,[],[308,309])). % 7.32/7.39 cnf(345,plain, % 7.32/7.39 (~P6(a37)), % 7.32/7.39 inference(scs_inference,[],[308,310])). % 7.32/7.39 cnf(346,plain, % 7.32/7.39 (E(f39(a56),f38(a55,a44))), % 7.32/7.39 inference(scs_inference,[],[130,2])). % 7.32/7.39 cnf(347,plain, % 7.32/7.39 (P1(f30(a29))), % 7.32/7.39 inference(scs_inference,[],[130,96,2,149])). % 7.32/7.39 cnf(349,plain, % 7.32/7.39 (~P3(x3491,f30(a29))), % 7.32/7.39 inference(scs_inference,[],[130,96,2,149,157])). % 7.32/7.39 cnf(353,plain, % 7.32/7.39 (P9(a29,a29)), % 7.32/7.39 inference(scs_inference,[],[118,119,130,96,2,149,157,312,170])). % 7.32/7.39 cnf(360,plain, % 7.32/7.39 (P3(a29,f30(f43(a29)))), % 7.32/7.39 inference(scs_inference,[],[146,308,118,119,130,94,96,2,149,157,312,170,3,152,318,331])). % 7.32/7.39 cnf(362,plain, % 7.32/7.39 (~P5(a41)), % 7.32/7.39 inference(scs_inference,[],[146,308,101,108,118,119,130,94,96,2,149,157,312,170,3,152,318,331,155])). % 7.32/7.39 cnf(364,plain, % 7.32/7.39 (~E(a41,a37)), % 7.32/7.39 inference(scs_inference,[],[146,311,308,101,108,118,119,130,94,96,2,149,157,312,170,3,152,318,331,155,82])). % 7.32/7.39 cnf(365,plain, % 7.32/7.39 (~P3(x3651,a37)), % 7.32/7.39 inference(rename_variables,[],[311])). % 7.32/7.39 cnf(367,plain, % 7.32/7.39 (~P3(a47,f38(f35(f31(a48,a57),f2(f31(a48,a57))),a51))), % 7.32/7.39 inference(scs_inference,[],[148,146,311,308,101,105,108,118,119,123,130,94,96,97,2,149,157,312,170,3,152,318,331,155,82,87,307])). % 7.32/7.39 cnf(369,plain, % 7.32/7.39 (~P7(a41,a37)), % 7.32/7.39 inference(scs_inference,[],[148,146,311,308,101,105,106,108,118,119,123,130,94,96,97,2,149,157,312,170,3,152,318,331,155,82,87,307,180])). % 7.32/7.39 cnf(371,plain, % 7.32/7.39 (~P7(a49,a37)), % 7.32/7.39 inference(scs_inference,[],[148,146,311,365,308,101,105,106,108,118,119,121,123,130,94,96,97,2,149,157,312,170,3,152,318,331,155,82,87,307,180,210])). % 7.32/7.39 cnf(372,plain, % 7.32/7.39 (~P3(x3721,a37)), % 7.32/7.39 inference(rename_variables,[],[311])). % 7.32/7.39 cnf(374,plain, % 7.32/7.39 (P7(a37,a37)), % 7.32/7.39 inference(scs_inference,[],[148,146,311,365,372,308,101,105,106,108,118,119,121,123,130,94,96,97,2,149,157,312,170,3,152,318,331,155,82,87,307,180,210,215])). % 7.32/7.39 cnf(377,plain, % 7.32/7.39 (P7(f30(a29),f30(a29))), % 7.32/7.39 inference(scs_inference,[],[148,146,311,365,372,308,101,105,106,108,118,119,121,123,130,94,96,97,2,149,157,312,170,3,152,318,331,155,82,87,307,180,210,215,235])). % 7.32/7.39 cnf(383,plain, % 7.32/7.39 (~P9(f43(a29),a29)), % 7.32/7.39 inference(scs_inference,[],[148,146,311,365,372,308,101,105,106,108,118,119,121,123,130,94,96,97,2,149,157,312,170,3,152,318,331,155,82,87,307,180,210,215,235,236,337,338])). % 7.32/7.39 cnf(385,plain, % 7.32/7.39 (~P7(a49,f35(f31(a48,a57),f2(f31(a48,a57))))), % 7.32/7.39 inference(scs_inference,[],[148,146,311,365,372,308,101,105,106,108,110,118,119,121,123,130,94,96,97,136,2,149,157,312,170,3,152,318,331,155,82,87,307,180,210,215,235,236,337,338,305])). % 7.32/7.39 cnf(389,plain, % 7.32/7.39 (P3(f2(a55),a55)+P6(a37)), % 7.32/7.39 inference(scs_inference,[],[148,146,311,365,372,308,101,105,106,108,109,110,118,119,121,123,124,130,94,96,97,136,2,149,157,312,170,3,152,318,331,155,82,87,307,180,210,215,235,236,337,338,305,316,83])). % 7.32/7.39 cnf(396,plain, % 7.32/7.39 (P3(f2(a55),a55)), % 7.32/7.39 inference(scs_inference,[],[345,389])). % 7.32/7.39 cnf(399,plain, % 7.32/7.39 (P9(a51,a51)), % 7.32/7.39 inference(scs_inference,[],[345,120,389,312,170])). % 7.32/7.39 cnf(401,plain, % 7.32/7.39 (E(a29,f3(a37))), % 7.32/7.39 inference(scs_inference,[],[344,345,120,389,312,170,2])). % 7.32/7.39 cnf(402,plain, % 7.32/7.39 (~P5(a49)), % 7.32/7.39 inference(scs_inference,[],[344,345,104,120,110,389,312,170,2,155])). % 7.32/7.39 cnf(406,plain, % 7.32/7.39 (~E(a37,a41)), % 7.32/7.39 inference(scs_inference,[],[344,345,353,369,374,383,104,120,362,98,110,389,312,170,2,155,87,84,88])). % 7.32/7.39 cnf(408,plain, % 7.32/7.39 (P3(a51,f30(f43(a51)))), % 7.32/7.39 inference(scs_inference,[],[344,345,96,353,369,374,383,104,120,362,364,98,110,389,312,170,2,155,87,84,88,3,331])). % 7.32/7.39 cnf(410,plain, % 7.32/7.39 (P1(f38(f30(a29),a29))), % 7.32/7.39 inference(scs_inference,[],[347,344,345,118,96,353,369,374,383,104,120,362,364,98,110,389,312,170,2,155,87,84,88,3,331,318])). % 7.32/7.39 cnf(415,plain, % 7.32/7.39 (~P3(x4151,f30(a29))), % 7.32/7.39 inference(rename_variables,[],[349])). % 7.32/7.39 cnf(416,plain, % 7.32/7.39 (P7(f30(a29),a37)), % 7.32/7.39 inference(scs_inference,[],[349,347,360,344,345,118,96,353,369,374,377,383,104,120,362,364,98,110,389,312,170,2,155,87,84,88,3,331,318,85,81,82,89])). % 7.32/7.39 cnf(419,plain, % 7.32/7.39 (P9(f43(a51),f43(a51))), % 7.32/7.39 inference(scs_inference,[],[349,347,360,344,345,118,96,353,369,374,377,383,104,120,362,364,98,110,389,312,170,2,155,87,84,88,3,331,318,85,81,82,89,235,236])). % 7.32/7.39 cnf(421,plain, % 7.32/7.39 (P7(a37,f30(a29))), % 7.32/7.39 inference(scs_inference,[],[349,347,360,344,345,311,308,118,96,353,369,374,377,383,104,120,362,364,98,110,389,312,170,2,155,87,84,88,3,331,318,85,81,82,89,235,236,215])). % 7.32/7.39 cnf(422,plain, % 7.32/7.39 (~P3(x4221,a37)), % 7.32/7.39 inference(rename_variables,[],[311])). % 7.32/7.39 cnf(424,plain, % 7.32/7.39 (~P7(f30(f43(a29)),f30(a29))), % 7.32/7.39 inference(scs_inference,[],[349,415,347,360,344,345,311,308,118,96,353,369,374,377,383,104,120,362,364,98,110,389,312,170,2,155,87,84,88,3,331,318,85,81,82,89,235,236,215,210])). % 7.32/7.39 cnf(429,plain, % 7.32/7.39 (E(a37,f30(a29))), % 7.32/7.39 inference(scs_inference,[],[349,415,347,360,344,345,311,308,118,96,353,369,374,377,383,104,120,362,364,98,110,389,312,170,2,155,87,84,88,3,331,318,85,81,82,89,235,236,215,210,337,201])). % 7.32/7.39 cnf(431,plain, % 7.32/7.39 (~P9(f43(a44),a29)), % 7.32/7.39 inference(scs_inference,[],[349,415,347,360,344,345,311,422,308,118,96,353,369,374,377,383,104,120,362,364,98,110,119,389,312,170,2,155,87,84,88,3,331,318,85,81,82,89,235,236,215,210,337,201,239])). % 7.32/7.39 cnf(434,plain, % 7.32/7.39 (P7(f26(a37,a29),a37)), % 7.32/7.39 inference(scs_inference,[],[349,415,347,360,344,345,311,422,308,118,96,353,369,374,377,383,104,120,362,364,98,106,110,119,389,312,170,2,155,87,84,88,3,331,318,85,81,82,89,235,236,215,210,337,201,239,248])). % 7.32/7.39 cnf(436,plain, % 7.32/7.39 (~E(f43(a29),a29)), % 7.32/7.39 inference(scs_inference,[],[349,415,347,360,344,345,311,422,308,118,96,353,369,374,377,383,104,120,362,364,98,106,110,119,389,312,170,2,155,87,84,88,3,331,318,85,81,82,89,235,236,215,210,337,201,239,248,7])). % 7.32/7.39 cnf(438,plain, % 7.32/7.39 (P9(a29,a44)), % 7.32/7.39 inference(scs_inference,[],[346,349,415,347,360,344,345,311,422,308,118,96,353,369,374,377,383,104,120,362,364,98,106,110,119,389,312,170,2,155,87,84,88,3,331,318,85,81,82,89,235,236,215,210,337,201,239,248,7,86,223])). % 7.32/7.39 cnf(451,plain, % 7.32/7.39 (E(f40(a53),f31(a53,a57))), % 7.32/7.39 inference(scs_inference,[],[131,123,312,170,2])). % 7.32/7.39 cnf(452,plain, % 7.32/7.39 (P3(a57,f30(f43(a57)))), % 7.32/7.39 inference(scs_inference,[],[131,123,312,170,2,331])). % 7.32/7.39 cnf(454,plain, % 7.32/7.39 (P5(f30(a29))), % 7.32/7.39 inference(scs_inference,[],[429,131,106,123,312,170,2,331,87])). % 7.32/7.39 cnf(455,plain, % 7.32/7.39 (P9(f43(a51),a44)), % 7.32/7.39 inference(scs_inference,[],[429,419,131,94,106,123,312,170,2,331,87,85])). % 7.32/7.39 cnf(456,plain, % 7.32/7.39 (P1(f38(f38(f30(a29),a29),a29))), % 7.32/7.39 inference(scs_inference,[],[429,410,118,419,131,94,106,123,312,170,2,331,87,85,318])). % 7.32/7.39 cnf(458,plain, % 7.32/7.39 (P9(a44,f43(a51))), % 7.32/7.39 inference(scs_inference,[],[429,410,118,419,131,94,106,123,312,170,2,331,87,85,318,84])). % 7.32/7.39 cnf(462,plain, % 7.32/7.39 (~P3(x4621,f30(a29))), % 7.32/7.39 inference(rename_variables,[],[349])). % 7.32/7.39 cnf(463,plain, % 7.32/7.39 (P3(f3(a37),a41)), % 7.32/7.39 inference(scs_inference,[],[401,429,396,410,349,344,118,377,424,436,419,131,94,106,123,312,170,2,331,87,85,318,84,88,3,82,81])). % 7.32/7.39 cnf(464,plain, % 7.32/7.39 (P7(f26(a37,a29),f30(a29))), % 7.32/7.39 inference(scs_inference,[],[401,429,396,410,349,344,118,377,424,436,419,434,131,94,106,123,312,170,2,331,87,85,318,84,88,3,82,81,89])). % 7.32/7.39 cnf(472,plain, % 7.32/7.39 (P7(f9(f30(a29),a29,f30(a29)),f30(a29))), % 7.32/7.39 inference(scs_inference,[],[401,429,396,410,349,462,344,347,118,377,424,436,419,434,131,94,106,123,312,170,2,331,87,85,318,84,88,3,82,81,89,236,235,215,274])). % 7.32/7.39 cnf(474,plain, % 7.32/7.39 (~P9(f43(f3(a37)),a29)), % 7.32/7.39 inference(scs_inference,[],[401,429,396,410,349,462,344,311,347,118,377,424,436,419,434,131,94,106,123,312,170,2,331,87,85,318,84,88,3,82,81,89,236,235,215,274,239])). % 7.32/7.39 cnf(477,plain, % 7.32/7.39 (P7(a37,f38(f30(a29),a29))), % 7.32/7.39 inference(scs_inference,[],[401,429,396,410,349,462,344,311,347,308,118,377,421,424,436,419,434,131,94,106,123,312,170,2,331,87,85,318,84,88,3,82,81,89,236,235,215,274,239,229])). % 7.32/7.39 cnf(488,plain, % 7.32/7.39 (P1(f30(f3(a37)))), % 7.32/7.39 inference(scs_inference,[],[463,312])). % 7.32/7.39 cnf(490,plain, % 7.32/7.39 (P9(f3(a37),f3(a37))), % 7.32/7.39 inference(scs_inference,[],[463,312,170])). % 7.32/7.39 cnf(492,plain, % 7.32/7.39 (E(a50,f2(a1))), % 7.32/7.39 inference(scs_inference,[],[463,93,312,170,2])). % 7.32/7.39 cnf(493,plain, % 7.32/7.39 (P3(f3(a37),f30(f43(f3(a37))))), % 7.32/7.39 inference(scs_inference,[],[463,93,312,170,2,331])). % 7.32/7.39 cnf(495,plain, % 7.32/7.39 (P9(a44,a44)), % 7.32/7.39 inference(scs_inference,[],[458,463,93,94,312,170,2,331,85])). % 7.32/7.39 cnf(497,plain, % 7.32/7.39 (P1(f38(f38(f38(f30(a29),a29),a29),a29))), % 7.32/7.39 inference(scs_inference,[],[456,118,458,463,93,99,362,94,312,170,2,331,85,87,318])). % 7.32/7.39 cnf(500,plain, % 7.32/7.39 (P3(f2(a1),a1)), % 7.32/7.39 inference(scs_inference,[],[456,118,458,463,122,406,93,99,362,94,312,170,2,331,85,87,318,3,81])). % 7.32/7.39 cnf(503,plain, % 7.32/7.39 (P7(f9(f30(a29),a29,f30(a29)),a37)), % 7.32/7.39 inference(scs_inference,[],[401,456,118,96,416,438,472,458,463,122,371,406,93,99,362,94,312,170,2,331,85,87,318,3,81,84,88,89])). % 7.32/7.39 cnf(505,plain, % 7.32/7.39 (~P3(x5051,f30(a29))), % 7.32/7.39 inference(rename_variables,[],[349])). % 7.32/7.39 cnf(506,plain, % 7.32/7.39 (P9(f43(f3(a37)),f43(f3(a37)))), % 7.32/7.39 inference(scs_inference,[],[401,456,408,349,118,96,416,438,472,458,463,122,371,406,93,99,362,94,312,170,2,331,85,87,318,3,81,84,88,89,82,236])). % 7.32/7.40 cnf(508,plain, % 7.32/7.40 (P7(f30(a29),f38(f38(f30(a29),a29),a29))), % 7.32/7.40 inference(scs_inference,[],[401,456,408,349,505,347,118,96,416,438,472,458,463,122,371,406,93,99,362,94,312,170,2,331,85,87,318,3,81,84,88,89,82,236,215])). % 7.32/7.40 cnf(509,plain, % 7.32/7.40 (~P3(x5091,f30(a29))), % 7.32/7.40 inference(rename_variables,[],[349])). % 7.32/7.40 cnf(513,plain, % 7.32/7.40 (P7(f9(f30(a29),a29,a37),f30(a29))), % 7.32/7.40 inference(scs_inference,[],[401,456,408,349,505,347,118,96,416,438,472,477,458,463,122,371,406,93,99,362,106,94,312,170,2,331,85,87,318,3,81,84,88,89,82,236,215,235,274])). % 7.32/7.40 cnf(515,plain, % 7.32/7.40 (P7(f26(a37,f3(a37)),a37)), % 7.32/7.40 inference(scs_inference,[],[401,456,408,349,505,347,308,118,96,416,438,472,477,458,463,122,371,406,93,99,362,106,94,312,170,2,331,85,87,318,3,81,84,88,89,82,236,215,235,274,248])). % 7.32/7.40 cnf(520,plain, % 7.32/7.40 (P7(a37,f38(f38(f30(a29),a29),a29))), % 7.32/7.40 inference(scs_inference,[],[401,456,408,349,505,509,347,308,118,96,120,416,421,438,472,477,455,458,463,122,371,406,93,99,362,106,94,119,312,170,2,331,85,87,318,3,81,84,88,89,82,236,215,235,274,248,239,229])). % 7.32/7.40 cnf(522,plain, % 7.32/7.40 (~E(f43(a51),a29)), % 7.32/7.40 inference(scs_inference,[],[401,456,408,349,505,509,347,308,118,96,120,416,421,438,472,477,455,458,463,122,371,406,93,99,362,106,94,119,312,170,2,331,85,87,318,3,81,84,88,89,82,236,215,235,274,248,239,229,7])). % 7.32/7.40 cnf(529,plain, % 7.32/7.40 (E(a51,f3(a47))), % 7.32/7.40 inference(scs_inference,[],[95,2])). % 7.32/7.40 cnf(530,plain, % 7.32/7.40 (P3(a44,f30(f43(a44)))), % 7.32/7.40 inference(scs_inference,[],[119,95,2,331])). % 7.32/7.40 cnf(533,plain, % 7.32/7.40 (P1(f38(f30(f3(a37)),a29))), % 7.32/7.40 inference(scs_inference,[],[488,118,119,95,100,362,2,331,87,318])). % 7.32/7.40 cnf(535,plain, % 7.32/7.40 (P9(a51,f3(a47))), % 7.32/7.40 inference(scs_inference,[],[488,118,119,399,95,100,362,2,331,87,318,85])). % 7.32/7.40 cnf(537,plain, % 7.32/7.40 (E(f31(a52,a57),f2(a1))), % 7.32/7.40 inference(scs_inference,[],[492,488,118,119,399,95,100,117,362,2,331,87,318,85,84,3])). % 7.32/7.40 cnf(542,plain, % 7.32/7.40 (~P3(x5421,f30(a29))), % 7.32/7.40 inference(rename_variables,[],[349])). % 7.32/7.40 cnf(543,plain, % 7.32/7.40 (P9(f43(a44),f43(a44))), % 7.32/7.40 inference(scs_inference,[],[492,488,452,493,344,349,118,96,416,119,399,495,513,95,100,117,369,362,2,331,87,318,85,84,3,89,81,88,82,236])). % 7.32/7.40 cnf(554,plain, % 7.32/7.40 (~E(f43(a57),a29)), % 7.32/7.40 inference(scs_inference,[],[492,488,452,493,344,349,542,410,347,308,118,96,416,421,119,399,495,508,513,454,95,100,117,369,362,2,331,87,318,85,84,3,89,81,88,82,236,235,215,274,229,7])). % 7.32/7.40 cnf(560,plain, % 7.32/7.40 (E(f2(a1),f31(a52,a57))), % 7.32/7.40 inference(scs_inference,[],[537,2])). % 7.32/7.40 cnf(561,plain, % 7.32/7.40 (P1(f38(f38(f30(f3(a37)),a29),a29))), % 7.32/7.40 inference(scs_inference,[],[537,533,118,2,318])). % 7.32/7.40 cnf(564,plain, % 7.32/7.40 (P9(f3(a47),f3(a47))), % 7.32/7.40 inference(scs_inference,[],[537,529,533,118,535,402,139,2,318,87,84])). % 7.32/7.40 cnf(565,plain, % 7.32/7.40 (P9(f3(a37),a29)), % 7.32/7.40 inference(scs_inference,[],[537,529,533,344,118,490,535,402,139,2,318,87,84,85])). % 7.32/7.40 cnf(568,plain, % 7.32/7.40 (P7(f26(a37,f3(a37)),f30(a29))), % 7.32/7.40 inference(scs_inference,[],[429,537,529,533,344,118,421,490,515,522,535,402,139,424,2,318,87,84,85,3,88,89])). % 7.32/7.40 cnf(571,plain, % 7.32/7.40 (~P3(x5711,a37)), % 7.32/7.40 inference(rename_variables,[],[311])). % 7.32/7.40 cnf(572,plain, % 7.32/7.40 (P7(a37,f38(f30(f3(a37)),a29))), % 7.32/7.40 inference(scs_inference,[],[429,537,529,533,530,408,344,311,571,308,118,421,490,515,522,535,402,139,424,2,318,87,84,85,3,88,89,81,82,215])). % 7.32/7.40 cnf(573,plain, % 7.32/7.40 (~P3(x5731,a37)), % 7.32/7.40 inference(rename_variables,[],[311])). % 7.32/7.40 cnf(580,plain, % 7.32/7.40 (P7(f30(a29),f38(f30(f3(a37)),a29))), % 7.32/7.40 inference(scs_inference,[],[429,537,529,533,530,408,344,311,571,573,410,347,308,118,120,119,416,421,490,515,522,520,535,402,139,424,455,106,2,318,87,84,85,3,88,89,81,82,215,274,239,229])). % 7.32/7.40 cnf(587,plain, % 7.32/7.40 (E(a47,f35(a1,f2(a1)))), % 7.32/7.40 inference(scs_inference,[],[132,2])). % 7.32/7.40 cnf(588,plain, % 7.32/7.40 (P1(f38(f38(f38(f38(f30(a29),a29),a29),a29),f3(a37)))), % 7.32/7.40 inference(scs_inference,[],[497,463,132,2,318])). % 7.32/7.40 cnf(591,plain, % 7.32/7.40 (~E(f43(f3(a37)),a29)), % 7.32/7.40 inference(scs_inference,[],[497,463,383,474,506,565,132,2,318,84,85])). % 7.32/7.40 cnf(592,plain, % 7.32/7.40 (E(a50,f31(a52,a57))), % 7.32/7.40 inference(scs_inference,[],[560,492,497,463,383,474,506,565,132,2,318,84,85,3])). % 7.32/7.40 cnf(596,plain, % 7.32/7.40 (~P3(x5961,f30(a29))), % 7.32/7.40 inference(rename_variables,[],[349])). % 7.32/7.40 cnf(598,plain, % 7.32/7.40 (P3(f3(a47),a41)), % 7.32/7.40 inference(scs_inference,[],[560,492,529,349,497,493,120,463,383,474,374,506,385,565,132,125,371,105,2,318,84,85,3,80,88,82,89,81])). % 7.32/7.40 cnf(603,plain, % 7.32/7.40 (P7(f30(a29),f38(f38(f38(f30(a29),a29),a29),a29))), % 7.32/7.40 inference(scs_inference,[],[560,492,529,349,596,497,493,347,120,463,383,474,374,506,564,385,565,132,125,371,105,2,318,84,85,3,80,88,82,89,81,236,235,215])). % 7.32/7.40 cnf(610,plain, % 7.32/7.40 (P1(f30(f3(a47)))), % 7.32/7.40 inference(scs_inference,[],[560,492,529,349,596,497,493,488,347,308,118,120,463,383,421,474,374,506,580,564,385,565,132,454,125,371,105,2,318,84,85,3,80,88,82,89,81,236,235,215,274,229,312])). % 7.32/7.40 cnf(612,plain, % 7.32/7.40 (P5(a47)), % 7.32/7.40 inference(scs_inference,[],[560,492,529,349,596,497,493,488,347,308,118,120,463,383,421,474,374,506,580,564,385,565,132,454,125,371,105,2,318,84,85,3,80,88,82,89,81,236,235,215,274,229,312,179])). % 7.32/7.40 cnf(614,plain, % 7.32/7.40 (P3(f3(a47),f30(f43(f3(a47))))), % 7.32/7.40 inference(scs_inference,[],[560,492,529,349,596,497,493,488,347,308,118,120,463,383,421,474,374,506,580,564,385,565,132,454,125,371,105,2,318,84,85,3,80,88,82,89,81,236,235,215,274,229,312,179,331])). % 7.32/7.40 cnf(624,plain, % 7.32/7.40 (E(a41,f39(a48))), % 7.32/7.40 inference(scs_inference,[],[97,2])). % 7.32/7.40 cnf(625,plain, % 7.32/7.40 (P1(f38(f38(f38(f38(f38(f30(a29),a29),a29),a29),f3(a37)),f3(a37)))), % 7.32/7.40 inference(scs_inference,[],[588,463,97,2,318])). % 7.32/7.40 cnf(629,plain, % 7.32/7.40 (P1(f39(a48))), % 7.32/7.40 inference(scs_inference,[],[588,344,463,431,97,554,543,101,2,318,85,3,80])). % 7.32/7.40 cnf(630,plain, % 7.32/7.40 (P6(f39(a48))), % 7.32/7.40 inference(scs_inference,[],[588,344,463,431,108,97,554,543,101,2,318,85,3,80,83])). % 7.32/7.40 cnf(634,plain, % 7.32/7.40 (~P3(x6341,f30(a29))), % 7.32/7.40 inference(rename_variables,[],[349])). % 7.32/7.40 cnf(635,plain, % 7.32/7.40 (P7(a55,f39(a48))), % 7.32/7.40 inference(scs_inference,[],[349,588,614,344,463,431,108,97,124,554,543,568,95,101,424,2,318,85,3,80,83,81,88,82,89])). % 7.32/7.40 cnf(643,plain, % 7.32/7.40 (P7(f26(a47,a51),a47)), % 7.32/7.40 inference(scs_inference,[],[349,634,588,614,396,456,344,347,118,120,463,431,108,97,124,554,543,568,603,112,612,535,95,101,424,454,105,2,318,85,3,80,83,81,88,82,89,339,215,274,248])). % 7.32/7.40 cnf(652,plain, % 7.32/7.40 (E(f39(f33(a48,a55)),a55)), % 7.32/7.40 inference(scs_inference,[],[349,634,588,614,396,456,344,347,308,118,120,463,431,421,108,97,124,554,543,568,603,112,612,535,95,101,424,454,105,2,318,85,3,80,83,81,88,82,89,339,215,274,248,229,7,324,325,326])). % 7.32/7.40 cnf(659,plain, % 7.32/7.40 (E(a55,f39(f33(a48,a55)))), % 7.32/7.40 inference(scs_inference,[],[652,2])). % 7.32/7.40 cnf(660,plain, % 7.32/7.40 (P6(f39(f33(a48,a55)))), % 7.32/7.40 inference(scs_inference,[],[652,109,2,83])). % 7.32/7.40 cnf(661,plain, % 7.32/7.40 (E(f39(a45),f39(a48))), % 7.32/7.40 inference(scs_inference,[],[624,652,109,98,2,83,3])). % 7.32/7.40 cnf(663,plain, % 7.32/7.40 (P7(a1,f39(a48))), % 7.32/7.40 inference(scs_inference,[],[624,560,652,109,98,126,500,2,83,3,81,89])). % 7.32/7.40 cnf(664,plain, % 7.32/7.40 (P7(f39(f33(a48,a55)),a41)), % 7.32/7.40 inference(scs_inference,[],[624,560,652,109,98,126,124,500,2,83,3,81,89,88])). % 7.32/7.40 cnf(666,plain, % 7.32/7.40 (~P3(x6661,f30(a29))), % 7.32/7.40 inference(rename_variables,[],[349])). % 7.32/7.40 cnf(682,plain, % 7.32/7.40 (E(f39(f33(a48,a1)),a1)), % 7.32/7.40 inference(scs_inference,[],[624,560,349,666,625,652,530,488,308,347,118,598,421,109,98,126,124,564,500,572,612,112,105,106,2,83,3,81,89,88,82,339,215,248,274,229,324,325,326])). % 7.32/7.40 cnf(692,plain, % 7.32/7.40 (E(f39(a48),f39(a45))), % 7.32/7.40 inference(scs_inference,[],[661,2])). % 7.32/7.40 cnf(693,plain, % 7.32/7.40 (P1(f38(f30(f3(a47)),a29))), % 7.32/7.40 inference(scs_inference,[],[661,610,118,2,318])). % 7.32/7.40 cnf(699,plain, % 7.32/7.40 (P3(f31(a53,a57),a54)), % 7.32/7.40 inference(scs_inference,[],[661,451,610,682,147,118,630,464,629,134,424,2,318,80,83,3,88,81])). % 7.32/7.40 cnf(717,plain, % 7.32/7.40 (E(a1,f39(f33(a48,a1)))), % 7.32/7.40 inference(scs_inference,[],[682,2])). % 7.32/7.40 cnf(722,plain, % 7.32/7.40 (P3(f39(f33(a48,a1)),f39(a56))), % 7.32/7.40 inference(scs_inference,[],[624,692,693,682,118,126,133,2,318,3,88,81])). % 7.32/7.40 cnf(723,plain, % 7.32/7.40 (P7(a55,f39(a45))), % 7.32/7.40 inference(scs_inference,[],[624,692,693,682,118,126,635,133,2,318,3,88,81,89])). % 7.32/7.40 cnf(725,plain, % 7.32/7.40 (~P3(x7251,f30(a29))), % 7.32/7.40 inference(rename_variables,[],[349])). % 7.32/7.40 cnf(733,plain, % 7.32/7.40 (P7(a37,f38(f30(f3(a47)),a29))), % 7.32/7.40 inference(scs_inference,[],[624,692,349,725,693,682,610,308,347,118,421,126,635,663,699,133,122,454,112,2,318,3,88,81,89,82,339,215,274,229])). % 7.32/7.40 cnf(739,plain, % 7.32/7.40 (E(f39(f33(a45,a55)),a55)), % 7.32/7.40 inference(scs_inference,[],[624,692,349,725,693,682,610,308,347,118,421,126,635,663,699,113,133,122,454,112,2,318,3,88,81,89,82,339,215,274,229,325,324,326])). % 7.32/7.40 cnf(749,plain, % 7.32/7.40 (E(a55,f39(f33(a45,a55)))), % 7.32/7.40 inference(scs_inference,[],[739,2])). % 7.32/7.40 cnf(750,plain, % 7.32/7.40 (P1(f38(f38(f38(f30(f3(a37)),a29),a29),f3(a37)))), % 7.32/7.40 inference(scs_inference,[],[561,739,463,2,318])). % 7.32/7.40 cnf(753,plain, % 7.32/7.40 (P7(f39(f33(a48,a55)),f39(a48))), % 7.32/7.40 inference(scs_inference,[],[659,561,739,463,109,635,2,318,83,88])). % 7.32/7.40 cnf(755,plain, % 7.32/7.40 (P7(a1,f39(a45))), % 7.32/7.40 inference(scs_inference,[],[692,659,561,739,344,463,109,635,663,591,2,318,83,88,3,89])). % 7.32/7.40 cnf(758,plain, % 7.32/7.40 (~P3(x7581,f30(a29))), % 7.32/7.40 inference(rename_variables,[],[349])). % 7.32/7.40 cnf(770,plain, % 7.32/7.40 (P1(f34(a48,f39(f33(a48,a55))))), % 7.32/7.40 inference(scs_inference,[],[692,659,717,349,758,561,739,396,610,344,308,347,118,463,421,109,635,663,591,722,733,723,135,113,106,112,2,318,83,88,3,89,81,82,339,215,274,229,325,324])). % 7.32/7.40 cnf(772,plain, % 7.32/7.40 (E(f39(f33(a48,f39(f33(a48,a55)))),f39(f33(a48,a55)))), % 7.32/7.40 inference(scs_inference,[],[692,659,717,349,758,561,739,396,610,344,308,347,118,463,421,109,635,663,591,722,733,723,135,113,106,112,2,318,83,88,3,89,81,82,339,215,274,229,325,324,326])). % 7.32/7.40 cnf(781,plain, % 7.32/7.40 (E(f39(f33(a48,a55)),f39(f33(a48,f39(f33(a48,a55)))))), % 7.32/7.40 inference(scs_inference,[],[772,2])). % 7.32/7.40 cnf(786,plain, % 7.32/7.40 (E(f39(f33(a45,a1)),a1)), % 7.32/7.40 inference(scs_inference,[],[772,755,113,2,325,324,326])). % 7.32/7.40 cnf(790,plain, % 7.32/7.40 (P7(f39(f33(a48,a1)),f39(a48))), % 7.32/7.40 inference(scs_inference,[],[717,772,750,463,663,755,113,2,325,324,326,318,88])). % 7.32/7.40 cnf(793,plain, % 7.32/7.40 (E(f39(f33(a48,a55)),f39(f33(a45,a55)))), % 7.32/7.40 inference(scs_inference,[],[587,749,717,652,772,750,463,663,660,643,755,113,2,325,324,326,318,88,83,89,3])). % 7.32/7.40 cnf(820,plain, % 7.32/7.40 (P1(f34(a48,f39(f33(a48,a1))))), % 7.32/7.40 inference(scs_inference,[],[793,790,112,2,325,326,324])). % 7.32/7.40 cnf(822,plain, % 7.32/7.40 (P7(f39(f33(a48,f39(f33(a48,a55)))),a41)), % 7.32/7.40 inference(scs_inference,[],[781,793,664,790,112,2,325,326,324,88])). % 7.32/7.40 cnf(823,plain, % 7.32/7.40 (P3(f31(a52,a57),a49)), % 7.32/7.40 inference(scs_inference,[],[781,793,592,664,790,121,112,2,325,326,324,88,81])). % 7.32/7.40 cnf(824,plain, % 7.32/7.40 (P7(f39(f33(a48,a55)),f39(a45))), % 7.32/7.40 inference(scs_inference,[],[692,781,793,592,664,753,790,121,112,2,325,326,324,88,81,89])). % 7.32/7.40 cnf(825,plain, % 7.32/7.40 (E(a55,f39(f33(a48,f39(f33(a48,a55)))))), % 7.32/7.40 inference(scs_inference,[],[692,659,781,793,592,664,753,790,121,112,2,325,326,324,88,81,89,3])). % 7.32/7.40 cnf(844,plain, % 7.32/7.40 (E(f39(f33(a48,f39(f33(a48,a55)))),a55)), % 7.32/7.40 inference(scs_inference,[],[825,2])). % 7.32/7.40 cnf(847,plain, % 7.32/7.40 (P1(f34(a45,f39(f33(a48,a55))))), % 7.32/7.40 inference(scs_inference,[],[825,824,113,2,325,324])). % 7.32/7.40 cnf(849,plain, % 7.32/7.40 (E(f39(f33(a45,f39(f33(a48,a55)))),f39(f33(a48,a55)))), % 7.32/7.40 inference(scs_inference,[],[825,824,113,2,325,324,326])). % 7.32/7.40 cnf(853,plain, % 7.32/7.40 (P7(f39(f33(a45,a55)),a41)), % 7.32/7.40 inference(scs_inference,[],[793,825,770,118,664,824,113,2,325,324,326,318,88])). % 7.32/7.40 cnf(855,plain, % 7.32/7.40 (P7(f39(f33(a48,f39(f33(a48,a55)))),f39(a48))), % 7.32/7.40 inference(scs_inference,[],[624,793,825,537,770,118,664,824,822,823,113,2,325,324,326,318,88,81,89])). % 7.32/7.40 cnf(874,plain, % 7.32/7.40 (E(f39(f33(a48,a55)),f39(f33(a45,f39(f33(a48,a55)))))), % 7.32/7.40 inference(scs_inference,[],[849,2])). % 7.32/7.40 cnf(880,plain, % 7.32/7.40 (P7(f39(f33(a48,f39(f33(a48,a55)))),f39(a45))), % 7.32/7.40 inference(scs_inference,[],[587,692,849,820,118,660,855,503,136,369,2,318,83,88,81,89])). % 7.32/7.40 cnf(881,plain, % 7.32/7.40 (E(f39(f33(a48,f39(f33(a48,a55)))),f39(f33(a45,a55)))), % 7.32/7.40 inference(scs_inference,[],[587,692,749,844,849,820,118,660,855,503,136,369,2,318,83,88,81,89,3])). % 7.32/7.40 cnf(898,plain, % 7.32/7.40 (P1(f38(f34(a45,f39(f33(a48,a55))),a29))), % 7.32/7.40 inference(scs_inference,[],[881,847,118,2,318])). % 7.32/7.40 cnf(901,plain, % 7.32/7.40 (P7(f39(f33(a45,a55)),f39(a48))), % 7.32/7.40 inference(scs_inference,[],[624,881,717,847,118,755,853,2,318,88,89])). % 7.32/7.40 cnf(902,plain, % 7.32/7.40 (E(a55,f39(f33(a45,f39(f33(a48,a55)))))), % 7.32/7.40 inference(scs_inference,[],[624,659,874,881,717,847,118,755,853,2,318,88,89,3])). % 7.32/7.40 cnf(944,plain, % 7.32/7.40 (~E(a46,f35(f31(a48,a57),f2(f31(a48,a57))))), % 7.32/7.40 inference(scs_inference,[],[367,881,902,717,349,786,898,147,847,308,347,118,463,421,137,880,901,129,454,112,2,324,326,325,318,88,89,3,82,215,274,229,16])). % 7.32/7.40 cnf(1821,plain, % 7.32/7.40 ($false), % 7.32/7.40 inference(scs_inference,[],[944,144,2]), % 7.32/7.40 ['proof']). % 7.32/7.40 % SZS output end Proof % 7.32/7.40 % Total time :6.700000s %------------------------------------------------------------------------------