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