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