%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG061+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n008.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 14:00:54 EDT 2024 % Result : Theorem 48.48s 48.59s % Output : CNFRefutation 48.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : RNG061+1 : TPTP v8.2.0. Released v4.0.0. % 0.00/0.06 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.06/0.25 % Computer : n008.cluster.edu % 0.06/0.25 % Model : x86_64 x86_64 % 0.06/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.25 % Memory : 8042.1875MB % 0.06/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.25 % CPULimit : 300 % 0.06/0.25 % WCLimit : 300 % 0.06/0.25 % DateTime : Tue Jun 18 13:48:38 EDT 2024 % 0.06/0.25 % CPUTime : % 0.10/0.40 start to proof:theBenchmark % 48.40/48.57 %------------------------------------------- % 48.40/48.57 % File :CSE---1.7 % 48.40/48.57 % Problem :theBenchmark % 48.40/48.57 % Transform :cnf % 48.40/48.57 % Format :tptp:raw % 48.40/48.57 % Command :java -jar mcs_scs.jar %d %s % 48.40/48.57 % 48.40/48.57 % Result :Theorem 48.050000s % 48.40/48.57 % Output :CNFRefutation 48.050000s % 48.40/48.57 %------------------------------------------- % 48.40/48.57 %------------------------------------------------------------------------------ % 48.40/48.57 % File : RNG061+1 : TPTP v8.2.0. Released v4.0.0. % 48.40/48.57 % Domain : Ring Theory % 48.40/48.57 % Problem : Cauchy-Bouniakowsky-Schwarz inequality 05_16_02_03, 00 expansion % 48.40/48.57 % Version : Especial. % 48.40/48.58 % English : % 48.40/48.58 % 48.40/48.58 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 48.40/48.58 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 48.40/48.58 % Source : [Pas08] % 48.40/48.58 % Names : cauchy_05_16_02_03.00 [Pas08] % 48.40/48.58 % 48.40/48.58 % Status : Theorem % 48.40/48.58 % Rating : 0.33 v8.2.0, 0.36 v8.1.0, 0.42 v7.5.0, 0.38 v7.4.0, 0.30 v7.3.0, 0.34 v7.2.0, 0.31 v7.1.0, 0.39 v7.0.0, 0.33 v6.4.0, 0.38 v6.3.0, 0.29 v6.2.0, 0.32 v6.1.0, 0.40 v6.0.0, 0.43 v5.5.0, 0.56 v5.4.0, 0.57 v5.3.0, 0.59 v5.2.0, 0.40 v5.1.0, 0.48 v5.0.0, 0.62 v4.1.0, 0.65 v4.0.1, 0.83 v4.0.0 % 48.40/48.58 % Syntax : Number of formulae : 60 ( 8 unt; 1 def) % 48.40/48.58 % Number of atoms : 193 ( 62 equ) % 48.40/48.58 % Maximal formula atoms : 9 ( 3 avg) % 48.40/48.58 % Number of connectives : 139 ( 6 ~; 1 |; 78 &) % 48.40/48.58 % ( 1 <=>; 53 =>; 0 <=; 0 <~>) % 48.40/48.58 % Maximal formula depth : 10 ( 4 avg) % 48.40/48.58 % Maximal term depth : 5 ( 1 avg) % 48.40/48.58 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 48.40/48.58 % Number of functors : 26 ( 26 usr; 18 con; 0-2 aty) % 48.40/48.58 % Number of variables : 71 ( 70 !; 1 ?) % 48.40/48.58 % SPC : FOF_THM_RFO_SEQ % 48.40/48.58 % 48.40/48.58 % Comments : Problem generated by the SAD system [VLP07] % 48.40/48.58 %------------------------------------------------------------------------------ % 48.40/48.58 fof(mNatSort,axiom, % 48.40/48.58 ! [W0] : % 48.40/48.58 ( aNaturalNumber0(W0) % 48.40/48.58 => $true ) ). % 48.40/48.58 % 48.40/48.58 fof(mZeroNat,axiom, % 48.40/48.58 aNaturalNumber0(sz00) ). % 48.40/48.58 % 48.40/48.58 fof(mSuccNat,axiom, % 48.40/48.58 ! [W0] : % 48.40/48.58 ( aNaturalNumber0(W0) % 48.40/48.58 => ( aNaturalNumber0(szszuzczcdt0(W0)) % 48.40/48.58 & szszuzczcdt0(W0) != sz00 ) ) ). % 48.40/48.58 % 48.40/48.58 fof(mNatExtr,axiom, % 48.40/48.58 ! [W0] : % 48.40/48.58 ( ( aNaturalNumber0(W0) % 48.40/48.58 & W0 != sz00 ) % 48.40/48.58 => ? [W1] : % 48.40/48.58 ( aNaturalNumber0(W1) % 48.40/48.58 & W0 = szszuzczcdt0(W1) ) ) ). % 48.40/48.58 % 48.40/48.58 fof(mSuccEqu,axiom, % 48.40/48.58 ! [W0,W1] : % 48.40/48.58 ( ( aNaturalNumber0(W0) % 48.40/48.58 & aNaturalNumber0(W1) ) % 48.40/48.58 => ( szszuzczcdt0(W0) = szszuzczcdt0(W1) % 48.40/48.58 => W0 = W1 ) ) ). % 48.40/48.58 % 48.40/48.58 fof(mIHOrd,axiom, % 48.40/48.58 ! [W0,W1] : % 48.40/48.58 ( ( aNaturalNumber0(W0) % 48.40/48.58 & aNaturalNumber0(W1) ) % 48.40/48.58 => ( iLess0(W0,W1) % 48.40/48.58 => $true ) ) ). % 48.40/48.58 % 48.40/48.58 fof(mIH,axiom, % 48.40/48.58 ! [W0] : % 48.40/48.58 ( aNaturalNumber0(W0) % 48.40/48.58 => iLess0(W0,szszuzczcdt0(W0)) ) ). % 48.40/48.58 % 48.40/48.58 fof(mScSort,axiom, % 48.40/48.58 ! [W0] : % 48.40/48.58 ( aScalar0(W0) % 48.40/48.58 => $true ) ). % 48.40/48.58 % 48.40/48.58 fof(mSZeroSc,axiom, % 48.40/48.58 aScalar0(sz0z00) ). % 48.40/48.58 % 48.40/48.58 fof(mSumSc,axiom, % 48.40/48.58 ! [W0,W1] : % 48.40/48.58 ( ( aScalar0(W0) % 48.40/48.58 & aScalar0(W1) ) % 48.40/48.58 => aScalar0(sdtpldt0(W0,W1)) ) ). % 48.40/48.58 % 48.40/48.58 fof(mMulSc,axiom, % 48.40/48.58 ! [W0,W1] : % 48.40/48.58 ( ( aScalar0(W0) % 48.40/48.58 & aScalar0(W1) ) % 48.40/48.58 => aScalar0(sdtasdt0(W0,W1)) ) ). % 48.40/48.58 % 48.40/48.58 fof(mNegSc,axiom, % 48.40/48.58 ! [W0] : % 48.40/48.58 ( aScalar0(W0) % 48.40/48.58 => aScalar0(smndt0(W0)) ) ). % 48.40/48.58 % 48.40/48.58 fof(mScZero,axiom, % 48.40/48.58 ! [W0] : % 48.40/48.58 ( aScalar0(W0) % 48.40/48.58 => ( sdtpldt0(W0,sz0z00) = W0 % 48.40/48.58 & sdtpldt0(sz0z00,W0) = W0 % 48.40/48.58 & sdtasdt0(W0,sz0z00) = sz0z00 % 48.40/48.58 & sdtasdt0(sz0z00,W0) = sz0z00 % 48.40/48.58 & sdtpldt0(W0,smndt0(W0)) = sz0z00 % 48.40/48.58 & sdtpldt0(smndt0(W0),W0) = sz0z00 % 48.40/48.58 & smndt0(smndt0(W0)) = W0 % 48.40/48.58 & smndt0(sz0z00) = sz0z00 ) ) ). % 48.48/48.58 % 48.48/48.58 fof(mArith,axiom, % 48.48/48.58 ! [W0,W1,W2] : % 48.48/48.58 ( ( aScalar0(W0) % 48.48/48.58 & aScalar0(W1) % 48.48/48.58 & aScalar0(W2) ) % 48.48/48.58 => ( sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) % 48.48/48.58 & sdtpldt0(W0,W1) = sdtpldt0(W1,W0) % 48.48/48.58 & sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) % 48.48/48.58 & sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ) ). % 48.48/48.58 % 48.48/48.58 fof(mDistr,axiom, % 48.48/48.58 ! [W0,W1,W2] : % 48.48/48.58 ( ( aScalar0(W0) % 48.48/48.58 & aScalar0(W1) % 48.48/48.58 & aScalar0(W2) ) % 48.48/48.58 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 48.48/48.58 & sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) ). % 48.48/48.58 % 48.48/48.58 fof(mDistr2,axiom, % 48.48/48.58 ! [W0,W1,W2,W3] : % 48.48/48.58 ( ( aScalar0(W0) % 48.48/48.58 & aScalar0(W1) % 48.48/48.58 & aScalar0(W2) % 48.48/48.58 & aScalar0(W3) ) % 48.48/48.58 => sdtasdt0(sdtpldt0(W0,W1),sdtpldt0(W2,W3)) = sdtpldt0(sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W0,W3)),sdtpldt0(sdtasdt0(W1,W2),sdtasdt0(W1,W3))) ) ). % 48.48/48.58 % 48.48/48.58 fof(mMNeg,axiom, % 48.48/48.58 ! [W0,W1] : % 48.48/48.58 ( ( aScalar0(W0) % 48.48/48.58 & aScalar0(W1) ) % 48.48/48.58 => ( sdtasdt0(W0,smndt0(W1)) = smndt0(sdtasdt0(W0,W1)) % 48.48/48.58 & sdtasdt0(smndt0(W0),W1) = smndt0(sdtasdt0(W0,W1)) ) ) ). % 48.48/48.58 % 48.48/48.58 fof(mMDNeg,axiom, % 48.48/48.58 ! [W0,W1] : % 48.48/48.58 ( ( aScalar0(W0) % 48.48/48.58 & aScalar0(W1) ) % 48.48/48.58 => sdtasdt0(smndt0(W0),smndt0(W1)) = sdtasdt0(W0,W1) ) ). % 48.48/48.58 % 48.48/48.58 fof(mLess,axiom, % 48.48/48.58 ! [W0,W1] : % 48.48/48.58 ( ( aScalar0(W0) % 48.48/48.58 & aScalar0(W1) ) % 48.48/48.58 => ( sdtlseqdt0(W0,W1) % 48.48/48.58 => $true ) ) ). % 48.48/48.58 % 48.48/48.58 fof(mLERef,axiom, % 48.48/48.58 ! [W0] : % 48.48/48.58 ( aScalar0(W0) % 48.48/48.58 => sdtlseqdt0(W0,W0) ) ). % 48.48/48.58 % 48.48/48.58 fof(mLEASm,axiom, % 48.48/48.58 ! [W0,W1] : % 48.48/48.58 ( ( aScalar0(W0) % 48.48/48.58 & aScalar0(W1) ) % 48.48/48.58 => ( ( sdtlseqdt0(W0,W1) % 48.48/48.58 & sdtlseqdt0(W1,W0) ) % 48.48/48.58 => W0 = W1 ) ) ). % 48.48/48.58 % 48.48/48.58 fof(mLETrn,axiom, % 48.48/48.58 ! [W0,W1,W2] : % 48.48/48.58 ( ( aScalar0(W0) % 48.48/48.58 & aScalar0(W1) % 48.48/48.58 & aScalar0(W2) ) % 48.48/48.58 => ( ( sdtlseqdt0(W0,W1) % 48.48/48.58 & sdtlseqdt0(W1,W2) ) % 48.48/48.58 => sdtlseqdt0(W0,W2) ) ) ). % 48.48/48.58 % 48.48/48.58 fof(mLEMon,axiom, % 48.48/48.58 ! [W0,W1,W2,W3] : % 48.48/48.58 ( ( aScalar0(W0) % 48.48/48.58 & aScalar0(W1) % 48.48/48.58 & aScalar0(W2) % 48.48/48.58 & aScalar0(W3) ) % 48.48/48.58 => ( ( sdtlseqdt0(W0,W1) % 48.48/48.58 & sdtlseqdt0(W2,W3) ) % 48.48/48.58 => sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W3)) ) ) ). % 48.48/48.58 % 48.48/48.58 fof(mLEMonM,axiom, % 48.48/48.58 ! [W0,W1,W2,W3] : % 48.48/48.58 ( ( aScalar0(W0) % 48.48/48.58 & aScalar0(W1) % 48.48/48.58 & aScalar0(W2) % 48.48/48.58 & aScalar0(W3) ) % 48.48/48.58 => ( ( sdtlseqdt0(W0,W1) % 48.48/48.58 & sdtlseqdt0(sz0z00,W2) % 48.48/48.58 & sdtlseqdt0(W2,W3) ) % 48.48/48.58 => sdtlseqdt0(sdtasdt0(W0,W2),sdtasdt0(W1,W3)) ) ) ). % 48.48/48.58 % 48.48/48.58 fof(mLETot,axiom, % 48.48/48.58 ! [W0,W1] : % 48.48/48.58 ( ( aScalar0(W0) % 48.48/48.58 & aScalar0(W1) ) % 48.48/48.58 => ( sdtlseqdt0(W0,W1) % 48.48/48.58 | sdtlseqdt0(W1,W0) ) ) ). % 48.48/48.58 % 48.48/48.58 fof(mPosMon,axiom, % 48.48/48.58 ! [W0,W1] : % 48.48/48.58 ( ( aScalar0(W0) % 48.48/48.58 & aScalar0(W1) ) % 48.48/48.58 => ( ( sdtlseqdt0(sz0z00,W0) % 48.48/48.58 & sdtlseqdt0(sz0z00,W1) ) % 48.48/48.58 => ( sdtlseqdt0(sz0z00,sdtpldt0(W0,W1)) % 48.48/48.58 & sdtlseqdt0(sz0z00,sdtasdt0(W0,W1)) ) ) ) ). % 48.48/48.58 % 48.48/48.58 fof(mSqPos,axiom, % 48.48/48.58 ! [W0] : % 48.48/48.58 ( aScalar0(W0) % 48.48/48.58 => sdtlseqdt0(sz0z00,sdtasdt0(W0,W0)) ) ). % 48.48/48.58 % 48.48/48.58 fof(mSqrt,axiom, % 48.48/48.58 ! [W0,W1] : % 48.48/48.58 ( ( aScalar0(W0) % 48.48/48.58 & aScalar0(W1) ) % 48.48/48.58 => ( ( sdtlseqdt0(sz0z00,W0) % 48.48/48.58 & sdtlseqdt0(sz0z00,W1) % 48.48/48.58 & sdtasdt0(W0,W0) = sdtasdt0(W1,W1) ) % 48.48/48.58 => W0 = W1 ) ) ). % 48.48/48.58 % 48.48/48.58 fof(mVcSort,axiom, % 48.48/48.58 ! [W0] : % 48.48/48.58 ( aVector0(W0) % 48.48/48.58 => $true ) ). % 48.48/48.58 % 48.48/48.58 fof(mDimNat,axiom, % 48.48/48.58 ! [W0] : % 48.48/48.58 ( aVector0(W0) % 48.48/48.58 => aNaturalNumber0(aDimensionOf0(W0)) ) ). % 48.48/48.58 % 48.48/48.58 fof(mElmSc,axiom, % 48.48/48.59 ! [W0,W1] : % 48.48/48.59 ( ( aVector0(W0) % 48.48/48.59 & aNaturalNumber0(W1) ) % 48.48/48.59 => aScalar0(sdtlbdtrb0(W0,W1)) ) ). % 48.48/48.59 % 48.48/48.59 fof(mDefInit,definition, % 48.48/48.59 ! [W0] : % 48.48/48.59 ( aVector0(W0) % 48.48/48.59 => ( aDimensionOf0(W0) != sz00 % 48.48/48.59 => ! [W1] : % 48.48/48.59 ( W1 = sziznziztdt0(W0) % 48.48/48.59 <=> ( aVector0(W1) % 48.48/48.59 & szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(W0) % 48.48/48.59 & ! [W2] : % 48.48/48.59 ( aNaturalNumber0(W2) % 48.48/48.59 => sdtlbdtrb0(W1,W2) = sdtlbdtrb0(W0,W2) ) ) ) ) ) ). % 48.48/48.59 % 48.48/48.59 fof(mEqInit,axiom, % 48.48/48.59 ! [W0,W1] : % 48.48/48.59 ( ( aVector0(W0) % 48.48/48.59 & aVector0(W1) ) % 48.48/48.59 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 48.48/48.59 & aDimensionOf0(W1) != sz00 ) % 48.48/48.59 => aDimensionOf0(sziznziztdt0(W0)) = aDimensionOf0(sziznziztdt0(W1)) ) ) ). % 48.48/48.59 % 48.48/48.59 fof(mScPr,axiom, % 48.48/48.59 ! [W0,W1] : % 48.48/48.59 ( ( aVector0(W0) % 48.48/48.59 & aVector0(W1) ) % 48.48/48.59 => ( aDimensionOf0(W0) = aDimensionOf0(W1) % 48.48/48.59 => aScalar0(sdtasasdt0(W0,W1)) ) ) ). % 48.48/48.59 % 48.48/48.59 fof(mDefSPZ,axiom, % 48.48/48.59 ! [W0,W1] : % 48.48/48.59 ( ( aVector0(W0) % 48.48/48.59 & aVector0(W1) ) % 48.48/48.59 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 48.48/48.59 & aDimensionOf0(W1) = sz00 ) % 48.48/48.59 => sdtasasdt0(W0,W1) = sz0z00 ) ) ). % 48.48/48.59 % 48.48/48.59 fof(mDefSPN,axiom, % 48.48/48.59 ! [W0,W1] : % 48.48/48.59 ( ( aVector0(W0) % 48.48/48.59 & aVector0(W1) ) % 48.48/48.59 => ( ( aDimensionOf0(W0) = aDimensionOf0(W1) % 48.48/48.59 & aDimensionOf0(W1) != sz00 ) % 48.48/48.59 => sdtasasdt0(W0,W1) = sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1)))) ) ) ). % 48.48/48.59 % 48.48/48.59 fof(mScSqPos,axiom, % 48.48/48.59 ! [W0] : % 48.48/48.59 ( aVector0(W0) % 48.48/48.59 => sdtlseqdt0(sz0z00,sdtasasdt0(W0,W0)) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1678,hypothesis, % 48.48/48.59 ( aVector0(xs) % 48.48/48.59 & aVector0(xt) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1652,hypothesis, % 48.48/48.59 ! [W0,W1] : % 48.48/48.59 ( ( aVector0(W0) % 48.48/48.59 & aVector0(W1) ) % 48.48/48.59 => ( aDimensionOf0(W0) = aDimensionOf0(W1) % 48.48/48.59 => ( iLess0(aDimensionOf0(W0),aDimensionOf0(xs)) % 48.48/48.59 => sdtlseqdt0(sdtasdt0(sdtasasdt0(W0,W1),sdtasasdt0(W0,W1)),sdtasdt0(sdtasasdt0(W0,W0),sdtasasdt0(W1,W1))) ) ) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1678_01,hypothesis, % 48.48/48.59 aDimensionOf0(xs) = aDimensionOf0(xt) ). % 48.48/48.59 % 48.48/48.59 fof(m__1692,hypothesis, % 48.48/48.59 aDimensionOf0(xs) != sz00 ). % 48.48/48.59 % 48.48/48.59 fof(m__1709,hypothesis, % 48.48/48.59 ( aVector0(xp) % 48.48/48.59 & xp = sziznziztdt0(xs) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1726,hypothesis, % 48.48/48.59 ( aVector0(xq) % 48.48/48.59 & xq = sziznziztdt0(xt) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1746,hypothesis, % 48.48/48.59 ( aScalar0(xA) % 48.48/48.59 & xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1766,hypothesis, % 48.48/48.59 ( aScalar0(xB) % 48.48/48.59 & xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1783,hypothesis, % 48.48/48.59 ( aScalar0(xC) % 48.48/48.59 & xC = sdtasasdt0(xp,xp) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1800,hypothesis, % 48.48/48.59 ( aScalar0(xD) % 48.48/48.59 & xD = sdtasasdt0(xq,xq) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1820,hypothesis, % 48.48/48.59 ( aScalar0(xE) % 48.48/48.59 & xE = sdtasasdt0(xp,xq) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1837,hypothesis, % 48.48/48.59 ( aScalar0(xF) % 48.48/48.59 & xF = sdtasdt0(xA,xA) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1854,hypothesis, % 48.48/48.59 ( aScalar0(xG) % 48.48/48.59 & xG = sdtasdt0(xB,xB) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1873,hypothesis, % 48.48/48.59 ( aScalar0(xH) % 48.48/48.59 & xH = sdtasdt0(xA,xB) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1892,hypothesis, % 48.48/48.59 ( aScalar0(xR) % 48.48/48.59 & xR = sdtasdt0(xC,xG) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1911,hypothesis, % 48.48/48.59 ( aScalar0(xP) % 48.48/48.59 & xP = sdtasdt0(xE,xH) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1930,hypothesis, % 48.48/48.59 ( aScalar0(xS) % 48.48/48.59 & xS = sdtasdt0(xF,xD) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1949,hypothesis, % 48.48/48.59 ( aScalar0(xN) % 48.48/48.59 & xN = sdtasdt0(xR,xS) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__1967,hypothesis, % 48.48/48.59 sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)) ). % 48.48/48.59 % 48.48/48.59 fof(m__2004,hypothesis, % 48.48/48.59 sdtlseqdt0(sdtasdt0(xP,xP),xN) ). % 48.48/48.59 % 48.48/48.59 fof(m__2144,hypothesis, % 48.48/48.59 ( sdtasdt0(xR,smndt0(xS)) = smndt0(xN) % 48.48/48.59 & sdtasdt0(smndt0(xS),xR) = smndt0(xN) % 48.48/48.59 & sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS) ) ). % 48.48/48.59 % 48.48/48.59 fof(m__2180,hypothesis, % 48.48/48.59 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(smndt0(xN),sdtasdt0(xS,xS))) ). % 48.48/48.59 % 48.48/48.59 fof(m__,conjecture, % 48.48/48.59 sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),smndt0(xN)),sdtpldt0(sdtasdt0(xS,xS),smndt0(xN))) ). % 48.48/48.59 % 48.48/48.59 %------------------------------------------------------------------------------ % 48.48/48.59 %------------------------------------------- % 48.48/48.59 % Proof found % 48.48/48.59 % SZS status Theorem for theBenchmark % 48.48/48.59 % SZS output start Proof % 48.48/48.59 %ClaNum:116(EqnAxiom:25) % 48.48/48.59 %VarNum:309(SingletonVarNum:96) % 48.48/48.59 %MaxLitNum:8 % 48.48/48.59 %MaxfuncDepth:4 % 48.48/48.59 %SharedTerms:94 % 48.48/48.59 %goalClause: 66 % 48.48/48.59 %singleGoalClaCount:1 % 48.48/48.59 [28]P1(a3) % 48.48/48.59 [29]P2(a12) % 48.48/48.59 [30]P2(a14) % 48.48/48.59 [31]P2(a16) % 48.48/48.59 [32]P2(a17) % 48.48/48.59 [33]P2(a18) % 48.48/48.59 [34]P2(a19) % 48.48/48.59 [35]P2(a20) % 48.48/48.59 [36]P2(a21) % 48.48/48.59 [37]P2(a22) % 48.48/48.59 [38]P2(a23) % 48.48/48.59 [39]P2(a24) % 48.48/48.59 [40]P2(a26) % 48.48/48.59 [41]P2(a25) % 48.48/48.59 [42]P3(a1) % 48.48/48.59 [43]P3(a28) % 48.48/48.59 [44]P3(a13) % 48.48/48.59 [45]P3(a27) % 48.48/48.59 [26]E(f2(a1),a13) % 48.48/48.59 [27]E(f2(a28),a27) % 48.48/48.59 [46]E(f4(a28),f4(a1)) % 48.48/48.59 [47]E(f5(a13,a13),a17) % 48.48/48.59 [48]E(f5(a27,a27),a18) % 48.48/48.59 [49]E(f5(a13,a27),a19) % 48.48/48.59 [50]E(f8(a14,a14),a20) % 48.48/48.59 [51]E(f8(a16,a16),a21) % 48.48/48.59 [52]E(f8(a14,a16),a22) % 48.48/48.59 [53]E(f8(a17,a21),a23) % 48.48/48.59 [54]E(f8(a19,a22),a24) % 48.48/48.59 [55]E(f8(a20,a18),a26) % 48.48/48.59 [56]E(f8(a23,a26),a25) % 48.48/48.59 [62]P4(f8(a24,a24),a25) % 48.48/48.59 [63]P4(f8(a19,a19),f8(a17,a18)) % 48.48/48.59 [65]~E(f4(a1),a3) % 48.48/48.59 [57]E(f9(a1,f4(a1)),a14) % 48.48/48.59 [58]E(f9(a28,f4(a28)),a16) % 48.48/48.59 [59]E(f8(a23,f10(a26)),f10(a25)) % 48.48/48.59 [60]E(f8(f10(a26),a23),f10(a25)) % 48.48/48.59 [61]E(f8(f10(a26),f10(a26)),f8(a26,a26)) % 48.48/48.59 [64]E(f11(f11(f8(a23,a23),f10(a25)),f11(f10(a25),f8(a26,a26))),f8(f11(a23,f10(a26)),f11(a23,f10(a26)))) % 48.48/48.59 [66]~E(f11(f11(f8(a23,a23),f10(a25)),f11(f8(a26,a26),f10(a25))),f8(f11(a23,f10(a26)),f11(a23,f10(a26)))) % 48.48/48.59 [79]~P2(x791)+P4(x791,x791) % 48.48/48.59 [67]~P2(x671)+E(f10(a12),a12) % 48.48/48.59 [68]~P1(x681)+~E(f15(x681),a3) % 48.48/48.59 [69]~P1(x691)+P1(f15(x691)) % 48.48/48.59 [70]~P3(x701)+P1(f4(x701)) % 48.48/48.59 [71]~P2(x711)+P2(f10(x711)) % 48.48/48.59 [74]~P2(x741)+E(f8(x741,a12),a12) % 48.48/48.59 [75]~P2(x751)+E(f8(a12,x751),a12) % 48.48/48.59 [77]~P2(x771)+E(f11(x771,a12),x771) % 48.48/48.59 [78]~P2(x781)+E(f11(a12,x781),x781) % 48.48/48.59 [83]~P1(x831)+P5(x831,f15(x831)) % 48.48/48.59 [90]~P2(x901)+P4(a12,f8(x901,x901)) % 48.48/48.59 [91]~P3(x911)+P4(a12,f5(x911,x911)) % 48.48/48.59 [72]~P2(x721)+E(f10(f10(x721)),x721) % 48.48/48.59 [81]~P2(x811)+E(f11(x811,f10(x811)),a12) % 48.48/48.59 [82]~P2(x821)+E(f11(f10(x821),x821),a12) % 48.48/48.59 [73]~P1(x731)+E(x731,a3)+P1(f6(x731)) % 48.48/48.59 [76]~P1(x761)+E(x761,a3)+E(f15(f6(x761)),x761) % 48.48/48.59 [87]~P2(x872)+~P2(x871)+P2(f11(x871,x872)) % 48.48/48.59 [88]~P2(x882)+~P2(x881)+P2(f8(x881,x882)) % 48.48/48.59 [89]~P1(x892)+~P3(x891)+P2(f9(x891,x892)) % 48.48/48.59 [96]~P2(x962)+~P2(x961)+E(f8(f10(x961),f10(x962)),f8(x961,x962)) % 48.48/48.59 [100]~P2(x1002)+~P2(x1001)+E(f10(f8(x1001,x1002)),f8(x1001,f10(x1002))) % 48.48/48.59 [101]~P2(x1012)+~P2(x1011)+E(f10(f8(x1011,x1012)),f8(f10(x1011),x1012)) % 48.48/48.59 [86]P4(x862,x861)+~P2(x861)+~P2(x862)+P4(x861,x862) % 48.48/48.59 [80]~P3(x801)+P3(x802)+~E(x802,f2(x801))+E(f4(x801),a3) % 48.48/48.59 [84]~P1(x842)+~P1(x841)+E(x841,x842)+~E(f15(x841),f15(x842)) % 48.48/48.59 [98]~P3(x982)+~P3(x981)+~E(f4(x981),f4(x982))+P2(f5(x981,x982)) % 48.48/48.59 [85]~P3(x851)+~E(x852,f2(x851))+E(f4(x851),a3)+E(f15(f4(x852)),f4(x851)) % 48.48/48.59 [93]~P2(x932)+~P2(x931)+~P2(x933)+E(f11(x931,x932),f11(x932,x931)) % 48.48/48.59 [94]~P2(x942)+~P2(x941)+~P2(x943)+E(f8(x941,x942),f8(x942,x941)) % 48.48/48.59 [106]~P2(x1063)+~P2(x1062)+~P2(x1061)+E(f11(f11(x1061,x1062),x1063),f11(x1061,f11(x1062,x1063))) % 48.48/48.59 [107]~P2(x1073)+~P2(x1072)+~P2(x1071)+E(f8(f8(x1071,x1072),x1073),f8(x1071,f8(x1072,x1073))) % 48.48/48.59 [109]~P2(x1093)+~P2(x1092)+~P2(x1091)+E(f11(f8(x1091,x1092),f8(x1091,x1093)),f8(x1091,f11(x1092,x1093))) % 48.48/48.59 [110]~P2(x1102)+~P2(x1103)+~P2(x1101)+E(f11(f8(x1101,x1102),f8(x1103,x1102)),f8(f11(x1101,x1103),x1102)) % 48.48/48.59 [99]~P2(x992)+~P2(x991)+~P4(x992,x991)+~P4(x991,x992)+E(x991,x992) % 48.48/48.59 [92]~P3(x922)+~P3(x921)+~E(f4(x921),f4(x922))+~E(f4(x922),a3)+E(f5(x921,x922),a12) % 48.48/48.59 [104]~P2(x1042)+~P2(x1041)+~P4(a12,x1042)+~P4(a12,x1041)+P4(a12,f11(x1041,x1042)) % 48.48/48.59 [105]~P2(x1052)+~P2(x1051)+~P4(a12,x1052)+~P4(a12,x1051)+P4(a12,f8(x1051,x1052)) % 48.48/48.59 [95]~P3(x951)+~P3(x952)+~E(f4(x952),f4(x951))+E(f4(x951),a3)+E(f4(f2(x952)),f4(f2(x951))) % 48.48/48.59 [115]~P3(x1152)+~P3(x1151)+~E(f4(x1151),f4(x1152))+~P5(f4(x1151),f4(a1))+P4(f8(f5(x1151,x1152),f5(x1151,x1152)),f8(f5(x1151,x1151),f5(x1152,x1152))) % 48.48/48.59 [114]~P3(x1141)+~P3(x1142)+~E(f4(x1142),f4(x1141))+E(f4(x1141),a3)+E(f11(f5(f2(x1142),f2(x1141)),f8(f9(x1142,f4(x1142)),f9(x1141,f4(x1141)))),f5(x1142,x1141)) % 48.48/48.59 [97]~P1(x973)+~P3(x971)+~E(x972,f2(x971))+E(f9(x972,x973),f9(x971,x973))+E(f4(x971),a3) % 48.48/48.59 [116]~P2(x1163)+~P2(x1162)+~P2(x1164)+~P2(x1161)+E(f11(f11(f8(x1161,x1162),f8(x1161,x1163)),f11(f8(x1164,x1162),f8(x1164,x1163))),f8(f11(x1161,x1164),f11(x1162,x1163))) % 48.48/48.59 [108]~P2(x1082)+~P2(x1081)+E(x1081,x1082)+~E(f8(x1081,x1081),f8(x1082,x1082))+~P4(a12,x1082)+~P4(a12,x1081) % 48.48/48.59 [102]~P3(x1021)+~P3(x1022)+E(x1021,f2(x1022))+E(f4(x1022),a3)+P1(f7(x1022,x1021))+~E(f15(f4(x1021)),f4(x1022)) % 48.48/48.59 [113]~P3(x1132)+~P3(x1131)+E(x1131,f2(x1132))+E(f4(x1132),a3)+~E(f15(f4(x1131)),f4(x1132))+~E(f9(x1131,f7(x1132,x1131)),f9(x1132,f7(x1132,x1131))) % 48.48/48.59 [103]~P2(x1032)+~P2(x1031)+~P4(x1033,x1032)+~P4(x1031,x1033)+P4(x1031,x1032)+~P2(x1033) % 48.48/48.59 [111]~P2(x1114)+~P2(x1112)+~P2(x1113)+~P2(x1111)+~P4(x1112,x1114)+~P4(x1111,x1113)+P4(f11(x1111,x1112),f11(x1113,x1114)) % 48.48/48.59 [112]~P2(x1124)+~P2(x1122)+~P2(x1123)+~P2(x1121)+~P4(x1122,x1124)+~P4(x1121,x1123)+~P4(a12,x1122)+P4(f8(x1121,x1122),f8(x1123,x1124)) % 48.48/48.59 %EqnAxiom % 48.48/48.59 [1]E(x11,x11) % 48.48/48.59 [2]E(x22,x21)+~E(x21,x22) % 48.48/48.59 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 48.48/48.59 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 48.48/48.59 [5]~E(x51,x52)+E(f8(x51,x53),f8(x52,x53)) % 48.48/48.59 [6]~E(x61,x62)+E(f8(x63,x61),f8(x63,x62)) % 48.48/48.59 [7]~E(x71,x72)+E(f4(x71),f4(x72)) % 48.48/48.59 [8]~E(x81,x82)+E(f11(x81,x83),f11(x82,x83)) % 48.48/48.59 [9]~E(x91,x92)+E(f11(x93,x91),f11(x93,x92)) % 48.48/48.59 [10]~E(x101,x102)+E(f5(x101,x103),f5(x102,x103)) % 48.48/48.59 [11]~E(x111,x112)+E(f5(x113,x111),f5(x113,x112)) % 48.48/48.59 [12]~E(x121,x122)+E(f9(x121,x123),f9(x122,x123)) % 48.48/48.59 [13]~E(x131,x132)+E(f9(x133,x131),f9(x133,x132)) % 48.48/48.59 [14]~E(x141,x142)+E(f6(x141),f6(x142)) % 48.48/48.59 [15]~E(x151,x152)+E(f10(x151),f10(x152)) % 48.48/48.59 [16]~E(x161,x162)+E(f15(x161),f15(x162)) % 48.48/48.59 [17]~E(x171,x172)+E(f7(x171,x173),f7(x172,x173)) % 48.48/48.59 [18]~E(x181,x182)+E(f7(x183,x181),f7(x183,x182)) % 48.48/48.59 [19]~P1(x191)+P1(x192)+~E(x191,x192) % 48.48/48.59 [20]~P2(x201)+P2(x202)+~E(x201,x202) % 48.48/48.59 [21]P4(x212,x213)+~E(x211,x212)+~P4(x211,x213) % 48.48/48.59 [22]P4(x223,x222)+~E(x221,x222)+~P4(x223,x221) % 48.48/48.59 [23]~P3(x231)+P3(x232)+~E(x231,x232) % 48.48/48.59 [24]P5(x242,x243)+~E(x241,x242)+~P5(x241,x243) % 48.48/48.59 [25]P5(x253,x252)+~E(x251,x252)+~P5(x253,x251) % 48.48/48.59 % 48.48/48.59 %------------------------------------------- % 48.48/48.59 cnf(117,plain, % 48.48/48.59 (~P3(x1171)+P3(f2(x1171))+E(f4(x1171),a3)), % 48.48/48.59 inference(equality_inference,[],[80])). % 48.48/48.59 cnf(119,plain, % 48.48/48.59 (~P3(x1191)+E(f4(x1191),a3)+E(f15(f4(f2(x1191))),f4(x1191))), % 48.48/48.59 inference(equality_inference,[],[85])). % 48.48/48.59 cnf(121,plain, % 48.48/48.59 (~P1(x1211)+~P3(x1212)+E(f9(f2(x1212),x1211),f9(x1212,x1211))+E(f4(x1212),a3)), % 48.48/48.59 inference(equality_inference,[],[97])). % 48.48/48.59 cnf(124,plain, % 48.48/48.59 (~P3(x1241)+~P3(x1241)+E(f4(x1241),a3)+E(f11(f5(f2(x1241),f2(x1241)),f8(f9(x1241,f4(x1241)),f9(x1241,f4(x1241)))),f5(x1241,x1241))), % 48.48/48.59 inference(equality_inference,[],[114])). % 48.48/48.59 cnf(126,plain, % 48.48/48.59 (E(f4(a1),f4(a28))), % 48.48/48.59 inference(scs_inference,[],[46,2])). % 48.48/48.59 cnf(130,plain, % 48.48/48.59 (E(f15(f4(f2(a1))),f4(a1))), % 48.48/48.59 inference(scs_inference,[],[66,42,46,65,64,2,3,117,119])). % 48.48/48.59 cnf(142,plain, % 48.48/48.59 (~E(f11(f8(a26,a26),f10(a25)),f11(f10(a25),f8(a26,a26)))), % 48.48/48.59 inference(scs_inference,[],[66,28,29,42,43,46,65,64,2,3,117,119,86,121,124,95,112,9])). % 48.48/48.59 cnf(148,plain, % 48.48/48.59 (~P2(x1481)+~P2(x1482)+E(f11(x1482,x1481),f11(x1481,x1482))), % 48.48/48.59 inference(scs_inference,[],[30,93])). % 48.48/48.59 cnf(158,plain, % 48.48/48.59 (~P2(f10(a25))+~P2(f8(a26,a26))), % 48.48/48.59 inference(scs_inference,[],[126,28,26,130,142,30,42,65,2,3,86,85,97,148])). % 48.48/48.59 cnf(586,plain, % 48.48/48.59 (~P2(f10(a26))+P2(f10(a25))), % 48.48/48.59 inference(scs_inference,[],[60,38,20,88])). % 48.48/48.59 cnf(2834,plain, % 48.48/48.59 (P2(f10(a25))), % 48.48/48.59 inference(scs_inference,[],[40,586,71])). % 48.48/48.59 cnf(2835,plain, % 48.48/48.59 (~P2(f8(a26,a26))), % 48.48/48.59 inference(scs_inference,[],[2834,158])). % 48.48/48.59 cnf(2851,plain, % 48.48/48.59 ($false), % 48.48/48.59 inference(scs_inference,[],[40,2835,88]), % 48.48/48.59 ['proof']). % 48.48/48.59 % SZS output end Proof % 48.48/48.59 % Total time :48.050000s %------------------------------------------------------------------------------