%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG124+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 : n011.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:01:11 EDT 2024 % Result : Theorem 0.59s 0.67s % Output : CNFRefutation 0.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : RNG124+1 : TPTP v8.2.0. Released v4.0.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n011.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 14:42:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 0.59/0.66 %------------------------------------------- % 0.59/0.66 % File :CSE---1.7 % 0.59/0.66 % Problem :theBenchmark % 0.59/0.66 % Transform :cnf % 0.59/0.66 % Format :tptp:raw % 0.59/0.66 % Command :java -jar mcs_scs.jar %d %s % 0.59/0.66 % 0.59/0.66 % Result :Theorem 0.020000s % 0.59/0.66 % Output :CNFRefutation 0.020000s % 0.59/0.66 %------------------------------------------- % 0.59/0.66 %------------------------------------------------------------------------------ % 0.59/0.66 % File : RNG124+1 : TPTP v8.2.0. Released v4.0.0. % 0.59/0.66 % Domain : Ring Theory % 0.59/0.66 % Problem : Chinese remainder theorem in a ring 07_05_03_07, 00 expansion % 0.59/0.66 % Version : Especial. % 0.59/0.66 % English : % 0.59/0.66 % 0.59/0.66 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 0.59/0.66 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 0.59/0.66 % Source : [Pas08] % 0.59/0.66 % Names : chines_07_05_03_07.00 [Pas08] % 0.59/0.66 % 0.59/0.66 % Status : ContradictoryAxioms % 0.59/0.66 % Rating : 0.19 v8.2.0, 0.17 v8.1.0, 0.19 v7.4.0, 0.43 v7.3.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.23 v6.0.0, 0.17 v5.5.0, 0.26 v5.4.0, 0.29 v5.3.0, 0.33 v5.2.0, 0.20 v5.1.0, 0.33 v5.0.0, 0.38 v4.1.0, 0.52 v4.0.1, 0.78 v4.0.0 % 0.59/0.66 % Syntax : Number of formulae : 56 ( 12 unt; 9 def) % 0.59/0.66 % Number of atoms : 188 ( 42 equ) % 0.59/0.66 % Maximal formula atoms : 9 ( 3 avg) % 0.59/0.66 % Number of connectives : 147 ( 15 ~; 3 |; 68 &) % 0.59/0.66 % ( 12 <=>; 49 =>; 0 <=; 0 <~>) % 0.59/0.66 % Maximal formula depth : 13 ( 5 avg) % 0.59/0.66 % Maximal term depth : 4 ( 1 avg) % 0.59/0.66 % Number of predicates : 14 ( 11 usr; 2 prp; 0-3 aty) % 0.59/0.66 % Number of functors : 16 ( 16 usr; 9 con; 0-2 aty) % 0.59/0.66 % Number of variables : 88 ( 78 !; 10 ?) % 0.59/0.66 % SPC : FOF_CAX_RFO_SEQ % 0.59/0.66 % 0.59/0.66 % Comments : Problem generated by the SAD system [VLP07] % 0.59/0.66 %------------------------------------------------------------------------------ % 0.59/0.66 fof(mElmSort,axiom, % 0.59/0.66 ! [W0] : % 0.59/0.66 ( aElement0(W0) % 0.59/0.66 => $true ) ). % 0.59/0.66 % 0.59/0.66 fof(mSortsC,axiom, % 0.59/0.66 aElement0(sz00) ). % 0.59/0.66 % 0.59/0.66 fof(mSortsC_01,axiom, % 0.59/0.66 aElement0(sz10) ). % 0.59/0.66 % 0.59/0.66 fof(mSortsU,axiom, % 0.59/0.66 ! [W0] : % 0.59/0.66 ( aElement0(W0) % 0.59/0.66 => aElement0(smndt0(W0)) ) ). % 0.59/0.66 % 0.59/0.66 fof(mSortsB,axiom, % 0.59/0.66 ! [W0,W1] : % 0.59/0.66 ( ( aElement0(W0) % 0.59/0.66 & aElement0(W1) ) % 0.59/0.66 => aElement0(sdtpldt0(W0,W1)) ) ). % 0.59/0.66 % 0.59/0.66 fof(mSortsB_02,axiom, % 0.59/0.66 ! [W0,W1] : % 0.59/0.66 ( ( aElement0(W0) % 0.59/0.66 & aElement0(W1) ) % 0.59/0.66 => aElement0(sdtasdt0(W0,W1)) ) ). % 0.59/0.66 % 0.59/0.66 fof(mAddComm,axiom, % 0.59/0.66 ! [W0,W1] : % 0.59/0.66 ( ( aElement0(W0) % 0.59/0.66 & aElement0(W1) ) % 0.59/0.66 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 0.59/0.66 % 0.59/0.66 fof(mAddAsso,axiom, % 0.59/0.66 ! [W0,W1,W2] : % 0.59/0.66 ( ( aElement0(W0) % 0.59/0.66 & aElement0(W1) % 0.59/0.66 & aElement0(W2) ) % 0.59/0.66 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 0.59/0.66 % 0.59/0.66 fof(mAddZero,axiom, % 0.59/0.66 ! [W0] : % 0.59/0.66 ( aElement0(W0) % 0.59/0.66 => ( sdtpldt0(W0,sz00) = W0 % 0.59/0.66 & W0 = sdtpldt0(sz00,W0) ) ) ). % 0.59/0.66 % 0.59/0.66 fof(mAddInvr,axiom, % 0.59/0.66 ! [W0] : % 0.59/0.66 ( aElement0(W0) % 0.59/0.66 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 0.59/0.66 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 0.59/0.66 % 0.59/0.66 fof(mMulComm,axiom, % 0.59/0.66 ! [W0,W1] : % 0.59/0.66 ( ( aElement0(W0) % 0.59/0.66 & aElement0(W1) ) % 0.59/0.66 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 0.59/0.66 % 0.59/0.66 fof(mMulAsso,axiom, % 0.59/0.66 ! [W0,W1,W2] : % 0.59/0.66 ( ( aElement0(W0) % 0.59/0.66 & aElement0(W1) % 0.59/0.66 & aElement0(W2) ) % 0.59/0.66 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 0.59/0.66 % 0.59/0.66 fof(mMulUnit,axiom, % 0.59/0.66 ! [W0] : % 0.59/0.66 ( aElement0(W0) % 0.59/0.66 => ( sdtasdt0(W0,sz10) = W0 % 0.59/0.66 & W0 = sdtasdt0(sz10,W0) ) ) ). % 0.59/0.66 % 0.59/0.66 fof(mAMDistr,axiom, % 0.59/0.66 ! [W0,W1,W2] : % 0.59/0.66 ( ( aElement0(W0) % 0.59/0.66 & aElement0(W1) % 0.59/0.66 & aElement0(W2) ) % 0.59/0.66 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 0.59/0.66 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 0.59/0.66 % 0.59/0.66 fof(mMulMnOne,axiom, % 0.59/0.66 ! [W0] : % 0.59/0.66 ( aElement0(W0) % 0.59/0.66 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 0.59/0.66 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 0.59/0.66 % 0.59/0.66 fof(mMulZero,axiom, % 0.59/0.66 ! [W0] : % 0.59/0.66 ( aElement0(W0) % 0.59/0.66 => ( sdtasdt0(W0,sz00) = sz00 % 0.59/0.66 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 0.59/0.66 % 0.59/0.66 fof(mCancel,axiom, % 0.59/0.66 ! [W0,W1] : % 0.59/0.66 ( ( aElement0(W0) % 0.59/0.66 & aElement0(W1) ) % 0.59/0.66 => ( sdtasdt0(W0,W1) = sz00 % 0.59/0.66 => ( W0 = sz00 % 0.59/0.66 | W1 = sz00 ) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mUnNeZr,axiom, % 0.59/0.67 sz10 != sz00 ). % 0.59/0.67 % 0.59/0.67 fof(mSetSort,axiom, % 0.59/0.67 ! [W0] : % 0.59/0.67 ( aSet0(W0) % 0.59/0.67 => $true ) ). % 0.59/0.67 % 0.59/0.67 fof(mEOfElem,axiom, % 0.59/0.67 ! [W0] : % 0.59/0.67 ( aSet0(W0) % 0.59/0.67 => ! [W1] : % 0.59/0.67 ( aElementOf0(W1,W0) % 0.59/0.67 => aElement0(W1) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mSetEq,axiom, % 0.59/0.67 ! [W0,W1] : % 0.59/0.67 ( ( aSet0(W0) % 0.59/0.67 & aSet0(W1) ) % 0.59/0.67 => ( ( ! [W2] : % 0.59/0.67 ( aElementOf0(W2,W0) % 0.59/0.67 => aElementOf0(W2,W1) ) % 0.59/0.67 & ! [W2] : % 0.59/0.67 ( aElementOf0(W2,W1) % 0.59/0.67 => aElementOf0(W2,W0) ) ) % 0.59/0.67 => W0 = W1 ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mDefSSum,definition, % 0.59/0.67 ! [W0,W1] : % 0.59/0.67 ( ( aSet0(W0) % 0.59/0.67 & aSet0(W1) ) % 0.59/0.67 => ! [W2] : % 0.59/0.67 ( W2 = sdtpldt1(W0,W1) % 0.59/0.67 <=> ( aSet0(W2) % 0.59/0.67 & ! [W3] : % 0.59/0.67 ( aElementOf0(W3,W2) % 0.59/0.67 <=> ? [W4,W5] : % 0.59/0.67 ( aElementOf0(W4,W0) % 0.59/0.67 & aElementOf0(W5,W1) % 0.59/0.67 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mDefSInt,definition, % 0.59/0.67 ! [W0,W1] : % 0.59/0.67 ( ( aSet0(W0) % 0.59/0.67 & aSet0(W1) ) % 0.59/0.67 => ! [W2] : % 0.59/0.67 ( W2 = sdtasasdt0(W0,W1) % 0.59/0.67 <=> ( aSet0(W2) % 0.59/0.67 & ! [W3] : % 0.59/0.67 ( aElementOf0(W3,W2) % 0.59/0.67 <=> ( aElementOf0(W3,W0) % 0.59/0.67 & aElementOf0(W3,W1) ) ) ) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mDefIdeal,definition, % 0.59/0.67 ! [W0] : % 0.59/0.67 ( aIdeal0(W0) % 0.59/0.67 <=> ( aSet0(W0) % 0.59/0.67 & ! [W1] : % 0.59/0.67 ( aElementOf0(W1,W0) % 0.59/0.67 => ( ! [W2] : % 0.59/0.67 ( aElementOf0(W2,W0) % 0.59/0.67 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 0.59/0.67 & ! [W2] : % 0.59/0.67 ( aElement0(W2) % 0.59/0.67 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mIdeSum,axiom, % 0.59/0.67 ! [W0,W1] : % 0.59/0.67 ( ( aIdeal0(W0) % 0.59/0.67 & aIdeal0(W1) ) % 0.59/0.67 => aIdeal0(sdtpldt1(W0,W1)) ) ). % 0.59/0.67 % 0.59/0.67 fof(mIdeInt,axiom, % 0.59/0.67 ! [W0,W1] : % 0.59/0.67 ( ( aIdeal0(W0) % 0.59/0.67 & aIdeal0(W1) ) % 0.59/0.67 => aIdeal0(sdtasasdt0(W0,W1)) ) ). % 0.59/0.67 % 0.59/0.67 fof(mDefMod,definition, % 0.59/0.67 ! [W0,W1,W2] : % 0.59/0.67 ( ( aElement0(W0) % 0.59/0.67 & aElement0(W1) % 0.59/0.67 & aIdeal0(W2) ) % 0.59/0.67 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 0.59/0.67 <=> aElementOf0(sdtpldt0(W0,smndt0(W1)),W2) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mChineseRemainder,axiom, % 0.59/0.67 ! [W0,W1] : % 0.59/0.67 ( ( aIdeal0(W0) % 0.59/0.67 & aIdeal0(W1) ) % 0.59/0.67 => ( ! [W2] : % 0.59/0.67 ( aElement0(W2) % 0.59/0.67 => aElementOf0(W2,sdtpldt1(W0,W1)) ) % 0.59/0.67 => ! [W2,W3] : % 0.59/0.67 ( ( aElement0(W2) % 0.59/0.67 & aElement0(W3) ) % 0.59/0.67 => ? [W4] : % 0.59/0.67 ( aElement0(W4) % 0.59/0.67 & sdteqdtlpzmzozddtrp0(W4,W2,W0) % 0.59/0.67 & sdteqdtlpzmzozddtrp0(W4,W3,W1) ) ) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mNatSort,axiom, % 0.59/0.67 ! [W0] : % 0.59/0.67 ( aNaturalNumber0(W0) % 0.59/0.67 => $true ) ). % 0.59/0.67 % 0.59/0.67 fof(mEucSort,axiom, % 0.59/0.67 ! [W0] : % 0.59/0.67 ( ( aElement0(W0) % 0.59/0.67 & W0 != sz00 ) % 0.59/0.67 => aNaturalNumber0(sbrdtbr0(W0)) ) ). % 0.59/0.67 % 0.59/0.67 fof(mNatLess,axiom, % 0.59/0.67 ! [W0,W1] : % 0.59/0.67 ( ( aNaturalNumber0(W0) % 0.59/0.67 & aNaturalNumber0(W1) ) % 0.59/0.67 => ( iLess0(W0,W1) % 0.59/0.67 => $true ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mDivision,axiom, % 0.59/0.67 ! [W0,W1] : % 0.59/0.67 ( ( aElement0(W0) % 0.59/0.67 & aElement0(W1) % 0.59/0.67 & W1 != sz00 ) % 0.59/0.67 => ? [W2,W3] : % 0.59/0.67 ( aElement0(W2) % 0.59/0.67 & aElement0(W3) % 0.59/0.67 & W0 = sdtpldt0(sdtasdt0(W2,W1),W3) % 0.59/0.67 & ( W3 != sz00 % 0.59/0.67 => iLess0(sbrdtbr0(W3),sbrdtbr0(W1)) ) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mDefDiv,definition, % 0.59/0.67 ! [W0,W1] : % 0.59/0.67 ( ( aElement0(W0) % 0.59/0.67 & aElement0(W1) ) % 0.59/0.67 => ( doDivides0(W0,W1) % 0.59/0.67 <=> ? [W2] : % 0.59/0.67 ( aElement0(W2) % 0.59/0.67 & sdtasdt0(W0,W2) = W1 ) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mDefDvs,definition, % 0.59/0.67 ! [W0] : % 0.59/0.67 ( aElement0(W0) % 0.59/0.67 => ! [W1] : % 0.59/0.67 ( aDivisorOf0(W1,W0) % 0.59/0.67 <=> ( aElement0(W1) % 0.59/0.67 & doDivides0(W1,W0) ) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mDefGCD,definition, % 0.59/0.67 ! [W0,W1] : % 0.59/0.67 ( ( aElement0(W0) % 0.59/0.67 & aElement0(W1) ) % 0.59/0.67 => ! [W2] : % 0.59/0.67 ( aGcdOfAnd0(W2,W0,W1) % 0.59/0.67 <=> ( aDivisorOf0(W2,W0) % 0.59/0.67 & aDivisorOf0(W2,W1) % 0.59/0.67 & ! [W3] : % 0.59/0.67 ( ( aDivisorOf0(W3,W0) % 0.59/0.67 & aDivisorOf0(W3,W1) ) % 0.59/0.67 => doDivides0(W3,W2) ) ) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mDefRel,definition, % 0.59/0.67 ! [W0,W1] : % 0.59/0.67 ( ( aElement0(W0) % 0.59/0.67 & aElement0(W1) ) % 0.59/0.67 => ( misRelativelyPrime0(W0,W1) % 0.59/0.67 <=> aGcdOfAnd0(sz10,W0,W1) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mDefPrIdeal,definition, % 0.59/0.67 ! [W0] : % 0.59/0.67 ( aElement0(W0) % 0.59/0.67 => ! [W1] : % 0.59/0.67 ( W1 = slsdtgt0(W0) % 0.59/0.67 <=> ( aSet0(W1) % 0.59/0.67 & ! [W2] : % 0.59/0.67 ( aElementOf0(W2,W1) % 0.59/0.67 <=> ? [W3] : % 0.59/0.67 ( aElement0(W3) % 0.59/0.67 & sdtasdt0(W0,W3) = W2 ) ) ) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(mPrIdeal,axiom, % 0.59/0.67 ! [W0] : % 0.59/0.67 ( aElement0(W0) % 0.59/0.67 => aIdeal0(slsdtgt0(W0)) ) ). % 0.59/0.67 % 0.59/0.67 fof(m__2091,hypothesis, % 0.59/0.67 ( aElement0(xa) % 0.59/0.67 & aElement0(xb) ) ). % 0.59/0.67 % 0.59/0.67 fof(m__2110,hypothesis, % 0.59/0.67 ( xa != sz00 % 0.59/0.67 | xb != sz00 ) ). % 0.59/0.67 % 0.59/0.67 fof(m__2129,hypothesis, % 0.59/0.67 aGcdOfAnd0(xc,xa,xb) ). % 0.59/0.67 % 0.59/0.67 fof(m__2174,hypothesis, % 0.59/0.67 ( aIdeal0(xI) % 0.59/0.67 & xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ) ). % 0.59/0.67 % 0.59/0.67 fof(m__2203,hypothesis, % 0.59/0.67 ( aElementOf0(sz00,slsdtgt0(xa)) % 0.59/0.67 & aElementOf0(xa,slsdtgt0(xa)) % 0.59/0.67 & aElementOf0(sz00,slsdtgt0(xb)) % 0.59/0.67 & aElementOf0(xb,slsdtgt0(xb)) ) ). % 0.59/0.67 % 0.59/0.67 fof(m__2228,hypothesis, % 0.59/0.67 ? [W0] : % 0.59/0.67 ( aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) % 0.59/0.67 & W0 != sz00 ) ). % 0.59/0.67 % 0.59/0.67 fof(m__2273,hypothesis, % 0.59/0.67 ( aElementOf0(xu,xI) % 0.59/0.67 & xu != sz00 % 0.59/0.67 & ! [W0] : % 0.59/0.67 ( ( aElementOf0(W0,xI) % 0.59/0.67 & W0 != sz00 ) % 0.59/0.67 => ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu)) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(m__2383,hypothesis, % 0.59/0.67 ~ ( aDivisorOf0(xu,xa) % 0.59/0.67 & aDivisorOf0(xu,xb) ) ). % 0.59/0.67 % 0.59/0.67 fof(m__2416,hypothesis, % 0.59/0.67 ? [W0,W1] : % 0.59/0.67 ( aElement0(W0) % 0.59/0.67 & aElement0(W1) % 0.59/0.67 & xu = sdtpldt0(sdtasdt0(xa,W0),sdtasdt0(xb,W1)) ) ). % 0.59/0.67 % 0.59/0.67 fof(m__2479,hypothesis, % 0.59/0.67 ~ ~ doDivides0(xu,xa) ). % 0.59/0.67 % 0.59/0.67 fof(m__2612,hypothesis, % 0.59/0.67 ~ doDivides0(xu,xb) ). % 0.59/0.67 % 0.59/0.67 fof(m__2666,hypothesis, % 0.59/0.67 ( aElement0(xq) % 0.59/0.67 & aElement0(xr) % 0.59/0.67 & xb = sdtpldt0(sdtasdt0(xq,xu),xr) % 0.59/0.67 & ( xr = sz00 % 0.59/0.67 | iLess0(sbrdtbr0(xr),sbrdtbr0(xu)) ) ) ). % 0.59/0.67 % 0.59/0.67 fof(m__2673,hypothesis, % 0.59/0.67 xr != sz00 ). % 0.59/0.67 % 0.59/0.67 fof(m__2690,hypothesis, % 0.59/0.67 aElementOf0(smndt0(sdtasdt0(xq,xu)),xI) ). % 0.59/0.67 % 0.59/0.67 fof(m__2699,hypothesis, % 0.59/0.67 aElementOf0(xb,xI) ). % 0.59/0.67 % 0.59/0.67 fof(m__2718,hypothesis, % 0.59/0.67 xr = sdtpldt0(smndt0(sdtasdt0(xq,xu)),xb) ). % 0.59/0.67 % 0.59/0.67 fof(m__2729,hypothesis, % 0.59/0.67 aElementOf0(xr,xI) ). % 0.59/0.67 % 0.59/0.67 fof(m__,conjecture, % 0.59/0.67 $false ). % 0.59/0.67 % 0.59/0.67 %------------------------------------------------------------------------------ % 0.59/0.67 %------------------------------------------- % 0.59/0.67 % Proof found % 0.59/0.67 % SZS status Theorem for theBenchmark % 0.59/0.67 % SZS output start Proof % 0.59/0.67 %ClaNum:202(EqnAxiom:83) % 0.59/0.67 %VarNum:704(SingletonVarNum:214) % 0.59/0.67 %MaxLitNum:8 % 0.59/0.67 %MaxfuncDepth:3 % 0.59/0.67 %SharedTerms:60 % 0.59/0.67 [84]P1(a1) % 0.59/0.67 [85]P1(a32) % 0.59/0.67 [86]P1(a33) % 0.59/0.67 [87]P1(a35) % 0.59/0.67 [88]P1(a36) % 0.59/0.67 [89]P1(a38) % 0.59/0.67 [90]P1(a2) % 0.59/0.67 [91]P1(a16) % 0.59/0.67 [92]P3(a34) % 0.59/0.67 [93]P4(a35,a34) % 0.59/0.67 [94]P4(a39,a34) % 0.59/0.67 [95]P4(a38,a34) % 0.59/0.67 [96]P6(a39,a33) % 0.59/0.67 [103]P5(a37,a33,a35) % 0.59/0.67 [108]~E(a1,a32) % 0.59/0.67 [109]~E(a1,a39) % 0.59/0.67 [110]~E(a1,a38) % 0.59/0.67 [111]~E(a3,a1) % 0.59/0.67 [112]~P6(a39,a35) % 0.59/0.67 [97]P4(a1,f17(a33)) % 0.59/0.67 [98]P4(a1,f17(a35)) % 0.59/0.67 [99]P4(a33,f17(a33)) % 0.59/0.67 [100]P4(a35,f17(a35)) % 0.59/0.67 [101]E(f18(f17(a33),f17(a35)),a34) % 0.59/0.67 [102]E(f30(f19(a36,a39),a38),a35) % 0.59/0.67 [104]P4(a3,f18(f17(a33),f17(a35))) % 0.59/0.67 [105]E(f30(f19(a33,a2),f19(a35,a16)),a39) % 0.59/0.67 [107]P4(f31(f19(a36,a39)),a34) % 0.59/0.67 [106]E(f30(f31(f19(a36,a39)),a35),a38) % 0.59/0.67 [113]~E(a1,a33)+~E(a1,a35) % 0.59/0.67 [133]~P2(a39,a33)+~P2(a39,a35) % 0.59/0.67 [125]E(a1,a38)+P9(f20(a38),f20(a39)) % 0.59/0.67 [114]~P3(x1141)+P7(x1141) % 0.59/0.67 [115]~P1(x1151)+P1(f31(x1151)) % 0.59/0.67 [116]~P1(x1161)+P3(f17(x1161)) % 0.59/0.67 [118]~P1(x1181)+E(f19(a1,x1181),a1) % 0.59/0.67 [119]~P1(x1191)+E(f19(x1191,a1),a1) % 0.59/0.67 [121]~P1(x1211)+E(f30(a1,x1211),x1211) % 0.59/0.67 [122]~P1(x1221)+E(f19(a32,x1221),x1221) % 0.59/0.67 [123]~P1(x1231)+E(f30(x1231,a1),x1231) % 0.59/0.67 [124]~P1(x1241)+E(f19(x1241,a32),x1241) % 0.59/0.67 [126]~P1(x1261)+E(f30(f31(x1261),x1261),a1) % 0.59/0.67 [127]~P1(x1271)+E(f30(x1271,f31(x1271)),a1) % 0.59/0.67 [128]~P1(x1281)+E(f19(x1281,f31(a32)),f31(x1281)) % 0.59/0.67 [129]~P1(x1291)+E(f19(f31(a32),x1291),f31(x1291)) % 0.59/0.67 [117]~P1(x1171)+E(x1171,a1)+P8(f20(x1171)) % 0.59/0.67 [130]~P7(x1301)+P3(x1301)+P4(f21(x1301),x1301) % 0.59/0.67 [148]~P4(x1481,a34)+E(x1481,a1)+~P9(f20(x1481),f20(a39)) % 0.59/0.67 [131]~P4(x1311,x1312)+P1(x1311)+~P7(x1312) % 0.59/0.67 [132]~P2(x1321,x1322)+P1(x1321)+~P1(x1322) % 0.59/0.67 [140]~P1(x1402)+~P2(x1401,x1402)+P6(x1401,x1402) % 0.59/0.67 [120]~P1(x1202)+P7(x1201)+~E(x1201,f17(x1202)) % 0.59/0.67 [135]~P1(x1352)+~P1(x1351)+E(f30(x1351,x1352),f30(x1352,x1351)) % 0.59/0.67 [136]~P1(x1362)+~P1(x1361)+E(f19(x1361,x1362),f19(x1362,x1361)) % 0.59/0.67 [141]~P1(x1412)+~P1(x1411)+P1(f30(x1411,x1412)) % 0.59/0.67 [142]~P1(x1422)+~P1(x1421)+P1(f19(x1421,x1422)) % 0.59/0.67 [143]~P3(x1432)+~P3(x1431)+P3(f18(x1431,x1432)) % 0.59/0.67 [144]~P3(x1442)+~P3(x1441)+P3(f29(x1441,x1442)) % 0.59/0.67 [139]~P7(x1391)+P3(x1391)+P4(f5(x1391),x1391)+P1(f4(x1391)) % 0.59/0.67 [171]~P7(x1711)+P3(x1711)+P1(f4(x1711))+~P4(f30(f21(x1711),f5(x1711)),x1711) % 0.59/0.67 [174]~P7(x1741)+P3(x1741)+P4(f5(x1741),x1741)+~P4(f19(f4(x1741),f21(x1741)),x1741) % 0.59/0.67 [183]~P7(x1831)+P3(x1831)+~P4(f30(f21(x1831),f5(x1831)),x1831)+~P4(f19(f4(x1831),f21(x1831)),x1831) % 0.59/0.67 [147]~P1(x1472)+~P1(x1471)+~P6(x1471,x1472)+P2(x1471,x1472) % 0.59/0.67 [156]~P1(x1562)+~P1(x1561)+~P10(x1561,x1562)+P5(a32,x1561,x1562) % 0.59/0.67 [164]~P1(x1642)+~P1(x1641)+P10(x1641,x1642)+~P5(a32,x1641,x1642) % 0.59/0.67 [145]~P1(x1451)+~P1(x1452)+E(x1451,a1)+P1(f6(x1452,x1451)) % 0.59/0.67 [146]~P1(x1461)+~P1(x1462)+E(x1461,a1)+P1(f9(x1462,x1461)) % 0.59/0.67 [151]~P1(x1512)+~P1(x1511)+~P6(x1511,x1512)+P1(f10(x1511,x1512)) % 0.59/0.67 [155]~P1(x1552)+~P1(x1551)+~P6(x1551,x1552)+E(f19(x1551,f10(x1551,x1552)),x1552) % 0.59/0.67 [176]~P1(x1761)+~P1(x1762)+E(x1761,a1)+E(f30(f19(f6(x1762,x1761),x1761),f9(x1762,x1761)),x1762) % 0.59/0.67 [166]~P1(x1662)+~P5(x1661,x1663,x1662)+P2(x1661,x1662)+~P1(x1663) % 0.59/0.67 [167]~P1(x1672)+~P5(x1671,x1672,x1673)+P2(x1671,x1672)+~P1(x1673) % 0.59/0.67 [137]~P7(x1373)+~P7(x1372)+P7(x1371)+~E(x1371,f18(x1372,x1373)) % 0.59/0.67 [138]~P7(x1383)+~P7(x1382)+P7(x1381)+~E(x1381,f29(x1382,x1383)) % 0.59/0.67 [154]~P1(x1541)+~P3(x1543)+~P4(x1542,x1543)+P4(f19(x1541,x1542),x1543) % 0.59/0.67 [158]~P3(x1583)+~P4(x1581,x1583)+~P4(x1582,x1583)+P4(f30(x1581,x1582),x1583) % 0.59/0.67 [178]~P1(x1781)+~P4(x1783,x1782)+~E(x1782,f17(x1781))+P1(f13(x1781,x1782,x1783)) % 0.59/0.67 [161]~P1(x1613)+~P1(x1612)+~P1(x1611)+E(f30(f30(x1611,x1612),x1613),f30(x1611,f30(x1612,x1613))) % 0.59/0.67 [162]~P1(x1623)+~P1(x1622)+~P1(x1621)+E(f19(f19(x1621,x1622),x1623),f19(x1621,f19(x1622,x1623))) % 0.59/0.67 [172]~P1(x1723)+~P1(x1722)+~P1(x1721)+E(f30(f19(x1721,x1722),f19(x1721,x1723)),f19(x1721,f30(x1722,x1723))) % 0.59/0.67 [173]~P1(x1732)+~P1(x1733)+~P1(x1731)+E(f30(f19(x1731,x1732),f19(x1733,x1732)),f19(f30(x1731,x1733),x1732)) % 0.59/0.67 [180]~P1(x1801)+~P4(x1803,x1802)+~E(x1802,f17(x1801))+E(f19(x1801,f13(x1801,x1802,x1803)),x1803) % 0.59/0.67 [134]~P1(x1341)+~P1(x1342)+E(x1341,a1)+E(x1342,a1)+~E(f19(x1342,x1341),a1) % 0.59/0.67 [157]~P1(x1572)+~P7(x1571)+P4(f12(x1572,x1571),x1571)+E(x1571,f17(x1572))+P1(f11(x1572,x1571)) % 0.59/0.67 [159]~P7(x1592)+~P7(x1591)+E(x1591,x1592)+P4(f15(x1591,x1592),x1591)+P4(f22(x1591,x1592),x1592) % 0.59/0.67 [168]~P7(x1682)+~P7(x1681)+E(x1681,x1682)+P4(f15(x1681,x1682),x1681)+~P4(f22(x1681,x1682),x1681) % 0.59/0.67 [169]~P7(x1692)+~P7(x1691)+E(x1691,x1692)+P4(f22(x1691,x1692),x1692)+~P4(f15(x1691,x1692),x1692) % 0.59/0.67 [177]~P7(x1772)+~P7(x1771)+E(x1771,x1772)+~P4(f15(x1771,x1772),x1772)+~P4(f22(x1771,x1772),x1771) % 0.59/0.67 [163]~P1(x1631)+~P1(x1632)+E(x1631,a1)+P9(f20(f9(x1632,x1631)),f20(x1631))+E(f9(x1632,x1631),a1) % 0.59/0.67 [165]~P1(x1652)+~P7(x1651)+P4(f12(x1652,x1651),x1651)+E(x1651,f17(x1652))+E(f19(x1652,f11(x1652,x1651)),f12(x1652,x1651)) % 0.59/0.67 [149]~P1(x1492)+~P1(x1491)+~P1(x1493)+P6(x1491,x1492)+~E(f19(x1491,x1493),x1492) % 0.59/0.67 [179]~P1(x1792)+~P1(x1791)+~P3(x1793)+P11(x1791,x1792,x1793)+~P4(f30(x1791,f31(x1792)),x1793) % 0.59/0.67 [181]~P1(x1812)+~P1(x1811)+~P3(x1813)+~P11(x1811,x1812,x1813)+P4(f30(x1811,f31(x1812)),x1813) % 0.59/0.67 [150]~P1(x1503)+~P1(x1504)+P4(x1501,x1502)+~E(f19(x1503,x1504),x1501)+~E(x1502,f17(x1503)) % 0.59/0.67 [152]~P7(x1524)+~P7(x1522)+~P4(x1521,x1523)+P4(x1521,x1522)+~E(x1523,f29(x1524,x1522)) % 0.59/0.67 [153]~P7(x1534)+~P7(x1532)+~P4(x1531,x1533)+P4(x1531,x1532)+~E(x1533,f29(x1532,x1534)) % 0.59/0.67 [194]~P7(x1942)+~P7(x1941)+~P4(x1944,x1943)+~E(x1943,f18(x1941,x1942))+P4(f24(x1941,x1942,x1943,x1944),x1941) % 0.59/0.67 [195]~P7(x1952)+~P7(x1951)+~P4(x1954,x1953)+~E(x1953,f18(x1951,x1952))+P4(f25(x1951,x1952,x1953,x1954),x1952) % 0.59/0.67 [202]~P7(x2022)+~P7(x2021)+~P4(x2024,x2023)+~E(x2023,f18(x2021,x2022))+E(f30(f24(x2021,x2022,x2023,x2024),f25(x2021,x2022,x2023,x2024)),x2024) % 0.59/0.67 [175]~P1(x1753)+~P1(x1752)+~P7(x1751)+~P4(f12(x1752,x1751),x1751)+~E(f12(x1752,x1751),f19(x1752,x1753))+E(x1751,f17(x1752)) % 0.59/0.67 [184]~P1(x1843)+~P1(x1842)+~P2(x1841,x1843)+~P2(x1841,x1842)+P5(x1841,x1842,x1843)+P2(f14(x1842,x1843,x1841),x1843) % 0.59/0.67 [185]~P1(x1853)+~P1(x1852)+~P2(x1851,x1853)+~P2(x1851,x1852)+P5(x1851,x1852,x1853)+P2(f14(x1852,x1853,x1851),x1852) % 0.59/0.67 [186]~P7(x1861)+~P7(x1863)+~P7(x1862)+P4(f23(x1862,x1863,x1861),x1861)+P4(f26(x1862,x1863,x1861),x1862)+E(x1861,f18(x1862,x1863)) % 0.59/0.67 [187]~P7(x1871)+~P7(x1873)+~P7(x1872)+P4(f23(x1872,x1873,x1871),x1871)+P4(f27(x1872,x1873,x1871),x1873)+E(x1871,f18(x1872,x1873)) % 0.59/0.67 [188]~P7(x1881)+~P7(x1883)+~P7(x1882)+P4(f28(x1882,x1883,x1881),x1881)+P4(f28(x1882,x1883,x1881),x1883)+E(x1881,f29(x1882,x1883)) % 0.59/0.67 [189]~P7(x1891)+~P7(x1893)+~P7(x1892)+P4(f28(x1892,x1893,x1891),x1891)+P4(f28(x1892,x1893,x1891),x1892)+E(x1891,f29(x1892,x1893)) % 0.59/0.67 [190]~P1(x1903)+~P1(x1902)+~P2(x1901,x1903)+~P2(x1901,x1902)+P5(x1901,x1902,x1903)+~P6(f14(x1902,x1903,x1901),x1901) % 0.59/0.67 [192]~P7(x1921)+~P7(x1923)+~P7(x1922)+P4(f23(x1922,x1923,x1921),x1921)+E(x1921,f18(x1922,x1923))+E(f30(f26(x1922,x1923,x1921),f27(x1922,x1923,x1921)),f23(x1922,x1923,x1921)) % 0.59/0.67 [182]~P2(x1821,x1823)+~P2(x1821,x1824)+~P5(x1822,x1824,x1823)+P6(x1821,x1822)+~P1(x1823)+~P1(x1824) % 0.59/0.67 [160]~P7(x1604)+~P7(x1603)+~P4(x1601,x1604)+~P4(x1601,x1603)+P4(x1601,x1602)+~E(x1602,f29(x1603,x1604)) % 0.59/0.67 [193]~P1(x1934)+~P1(x1933)+~P3(x1932)+~P3(x1931)+P1(f7(x1931,x1932))+P1(f8(x1931,x1932,x1933,x1934)) % 0.59/0.67 [196]~P1(x1964)+~P1(x1963)+~P3(x1962)+~P3(x1961)+P11(f8(x1961,x1962,x1963,x1964),x1964,x1962)+P1(f7(x1961,x1962)) % 0.59/0.67 [197]~P1(x1974)+~P1(x1973)+~P3(x1972)+~P3(x1971)+P11(f8(x1971,x1972,x1973,x1974),x1973,x1971)+P1(f7(x1971,x1972)) % 0.59/0.67 [199]~P1(x1994)+~P1(x1993)+~P3(x1992)+~P3(x1991)+~P4(f7(x1991,x1992),f18(x1991,x1992))+P1(f8(x1991,x1992,x1993,x1994)) % 0.59/0.67 [200]~P1(x2004)+~P1(x2003)+~P3(x2002)+~P3(x2001)+P11(f8(x2001,x2002,x2003,x2004),x2004,x2002)+~P4(f7(x2001,x2002),f18(x2001,x2002)) % 0.59/0.67 [201]~P1(x2014)+~P1(x2013)+~P3(x2012)+~P3(x2011)+P11(f8(x2011,x2012,x2013,x2014),x2013,x2011)+~P4(f7(x2011,x2012),f18(x2011,x2012)) % 0.59/0.67 [198]~P7(x1981)+~P7(x1983)+~P7(x1982)+~P4(f28(x1982,x1983,x1981),x1981)+~P4(f28(x1982,x1983,x1981),x1983)+~P4(f28(x1982,x1983,x1981),x1982)+E(x1981,f29(x1982,x1983)) % 0.59/0.67 [170]~P7(x1704)+~P7(x1703)+~P4(x1706,x1704)+~P4(x1705,x1703)+P4(x1701,x1702)+~E(x1702,f18(x1703,x1704))+~E(f30(x1705,x1706),x1701) % 0.59/0.67 [191]~P7(x1911)+~P7(x1913)+~P7(x1912)+~P4(x1915,x1913)+~P4(x1914,x1912)+~P4(f23(x1912,x1913,x1911),x1911)+E(x1911,f18(x1912,x1913))+~E(f30(x1914,x1915),f23(x1912,x1913,x1911)) % 0.59/0.67 %EqnAxiom % 0.59/0.67 [1]E(x11,x11) % 0.59/0.67 [2]E(x22,x21)+~E(x21,x22) % 0.59/0.67 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.59/0.67 [4]~E(x41,x42)+E(f17(x41),f17(x42)) % 0.59/0.67 [5]~E(x51,x52)+E(f18(x51,x53),f18(x52,x53)) % 0.59/0.67 [6]~E(x61,x62)+E(f18(x63,x61),f18(x63,x62)) % 0.59/0.67 [7]~E(x71,x72)+E(f30(x71,x73),f30(x72,x73)) % 0.59/0.67 [8]~E(x81,x82)+E(f30(x83,x81),f30(x83,x82)) % 0.59/0.68 [9]~E(x91,x92)+E(f25(x91,x93,x94,x95),f25(x92,x93,x94,x95)) % 0.59/0.68 [10]~E(x101,x102)+E(f25(x103,x101,x104,x105),f25(x103,x102,x104,x105)) % 0.59/0.68 [11]~E(x111,x112)+E(f25(x113,x114,x111,x115),f25(x113,x114,x112,x115)) % 0.59/0.68 [12]~E(x121,x122)+E(f25(x123,x124,x125,x121),f25(x123,x124,x125,x122)) % 0.59/0.68 [13]~E(x131,x132)+E(f24(x131,x133,x134,x135),f24(x132,x133,x134,x135)) % 0.59/0.68 [14]~E(x141,x142)+E(f24(x143,x141,x144,x145),f24(x143,x142,x144,x145)) % 0.59/0.68 [15]~E(x151,x152)+E(f24(x153,x154,x151,x155),f24(x153,x154,x152,x155)) % 0.59/0.68 [16]~E(x161,x162)+E(f24(x163,x164,x165,x161),f24(x163,x164,x165,x162)) % 0.59/0.68 [17]~E(x171,x172)+E(f28(x171,x173,x174),f28(x172,x173,x174)) % 0.59/0.68 [18]~E(x181,x182)+E(f28(x183,x181,x184),f28(x183,x182,x184)) % 0.59/0.68 [19]~E(x191,x192)+E(f28(x193,x194,x191),f28(x193,x194,x192)) % 0.59/0.68 [20]~E(x201,x202)+E(f29(x201,x203),f29(x202,x203)) % 0.59/0.68 [21]~E(x211,x212)+E(f29(x213,x211),f29(x213,x212)) % 0.59/0.68 [22]~E(x221,x222)+E(f19(x221,x223),f19(x222,x223)) % 0.59/0.68 [23]~E(x231,x232)+E(f19(x233,x231),f19(x233,x232)) % 0.59/0.68 [24]~E(x241,x242)+E(f27(x241,x243,x244),f27(x242,x243,x244)) % 0.59/0.68 [25]~E(x251,x252)+E(f27(x253,x251,x254),f27(x253,x252,x254)) % 0.59/0.68 [26]~E(x261,x262)+E(f27(x263,x264,x261),f27(x263,x264,x262)) % 0.59/0.68 [27]~E(x271,x272)+E(f7(x271,x273),f7(x272,x273)) % 0.59/0.68 [28]~E(x281,x282)+E(f7(x283,x281),f7(x283,x282)) % 0.59/0.68 [29]~E(x291,x292)+E(f8(x291,x293,x294,x295),f8(x292,x293,x294,x295)) % 0.59/0.68 [30]~E(x301,x302)+E(f8(x303,x301,x304,x305),f8(x303,x302,x304,x305)) % 0.59/0.68 [31]~E(x311,x312)+E(f8(x313,x314,x311,x315),f8(x313,x314,x312,x315)) % 0.59/0.68 [32]~E(x321,x322)+E(f8(x323,x324,x325,x321),f8(x323,x324,x325,x322)) % 0.59/0.68 [33]~E(x331,x332)+E(f12(x331,x333),f12(x332,x333)) % 0.59/0.68 [34]~E(x341,x342)+E(f12(x343,x341),f12(x343,x342)) % 0.59/0.68 [35]~E(x351,x352)+E(f6(x351,x353),f6(x352,x353)) % 0.59/0.68 [36]~E(x361,x362)+E(f6(x363,x361),f6(x363,x362)) % 0.59/0.68 [37]~E(x371,x372)+E(f9(x371,x373),f9(x372,x373)) % 0.59/0.68 [38]~E(x381,x382)+E(f9(x383,x381),f9(x383,x382)) % 0.59/0.68 [39]~E(x391,x392)+E(f26(x391,x393,x394),f26(x392,x393,x394)) % 0.59/0.68 [40]~E(x401,x402)+E(f26(x403,x401,x404),f26(x403,x402,x404)) % 0.59/0.68 [41]~E(x411,x412)+E(f26(x413,x414,x411),f26(x413,x414,x412)) % 0.59/0.68 [42]~E(x421,x422)+E(f13(x421,x423,x424),f13(x422,x423,x424)) % 0.59/0.68 [43]~E(x431,x432)+E(f13(x433,x431,x434),f13(x433,x432,x434)) % 0.59/0.68 [44]~E(x441,x442)+E(f13(x443,x444,x441),f13(x443,x444,x442)) % 0.59/0.68 [45]~E(x451,x452)+E(f31(x451),f31(x452)) % 0.59/0.68 [46]~E(x461,x462)+E(f23(x461,x463,x464),f23(x462,x463,x464)) % 0.59/0.68 [47]~E(x471,x472)+E(f23(x473,x471,x474),f23(x473,x472,x474)) % 0.59/0.68 [48]~E(x481,x482)+E(f23(x483,x484,x481),f23(x483,x484,x482)) % 0.59/0.68 [49]~E(x491,x492)+E(f22(x491,x493),f22(x492,x493)) % 0.59/0.68 [50]~E(x501,x502)+E(f22(x503,x501),f22(x503,x502)) % 0.59/0.68 [51]~E(x511,x512)+E(f10(x511,x513),f10(x512,x513)) % 0.59/0.68 [52]~E(x521,x522)+E(f10(x523,x521),f10(x523,x522)) % 0.59/0.68 [53]~E(x531,x532)+E(f21(x531),f21(x532)) % 0.59/0.68 [54]~E(x541,x542)+E(f20(x541),f20(x542)) % 0.59/0.68 [55]~E(x551,x552)+E(f4(x551),f4(x552)) % 0.59/0.68 [56]~E(x561,x562)+E(f5(x561),f5(x562)) % 0.59/0.68 [57]~E(x571,x572)+E(f11(x571,x573),f11(x572,x573)) % 0.59/0.68 [58]~E(x581,x582)+E(f11(x583,x581),f11(x583,x582)) % 0.59/0.68 [59]~E(x591,x592)+E(f14(x591,x593,x594),f14(x592,x593,x594)) % 0.59/0.68 [60]~E(x601,x602)+E(f14(x603,x601,x604),f14(x603,x602,x604)) % 0.59/0.68 [61]~E(x611,x612)+E(f14(x613,x614,x611),f14(x613,x614,x612)) % 0.59/0.68 [62]~E(x621,x622)+E(f15(x621,x623),f15(x622,x623)) % 0.59/0.68 [63]~E(x631,x632)+E(f15(x633,x631),f15(x633,x632)) % 0.59/0.68 [64]~P1(x641)+P1(x642)+~E(x641,x642) % 0.59/0.68 [65]P4(x652,x653)+~E(x651,x652)+~P4(x651,x653) % 0.59/0.68 [66]P4(x663,x662)+~E(x661,x662)+~P4(x663,x661) % 0.59/0.68 [67]~P7(x671)+P7(x672)+~E(x671,x672) % 0.59/0.68 [68]~P3(x681)+P3(x682)+~E(x681,x682) % 0.59/0.68 [69]P2(x692,x693)+~E(x691,x692)+~P2(x691,x693) % 0.59/0.68 [70]P2(x703,x702)+~E(x701,x702)+~P2(x703,x701) % 0.59/0.68 [71]P5(x712,x713,x714)+~E(x711,x712)+~P5(x711,x713,x714) % 0.59/0.68 [72]P5(x723,x722,x724)+~E(x721,x722)+~P5(x723,x721,x724) % 0.59/0.68 [73]P5(x733,x734,x732)+~E(x731,x732)+~P5(x733,x734,x731) % 0.59/0.68 [74]P6(x742,x743)+~E(x741,x742)+~P6(x741,x743) % 0.59/0.68 [75]P6(x753,x752)+~E(x751,x752)+~P6(x753,x751) % 0.59/0.68 [76]P11(x762,x763,x764)+~E(x761,x762)+~P11(x761,x763,x764) % 0.59/0.68 [77]P11(x773,x772,x774)+~E(x771,x772)+~P11(x773,x771,x774) % 0.59/0.68 [78]P11(x783,x784,x782)+~E(x781,x782)+~P11(x783,x784,x781) % 0.59/0.68 [79]P9(x792,x793)+~E(x791,x792)+~P9(x791,x793) % 0.59/0.68 [80]P9(x803,x802)+~E(x801,x802)+~P9(x803,x801) % 0.59/0.68 [81]~P8(x811)+P8(x812)+~E(x811,x812) % 0.59/0.68 [82]P10(x822,x823)+~E(x821,x822)+~P10(x821,x823) % 0.59/0.68 [83]P10(x833,x832)+~E(x831,x832)+~P10(x833,x831) % 0.59/0.68 % 0.59/0.68 %------------------------------------------- % 0.59/0.68 cnf(219,plain, % 0.59/0.68 (E(a38,a1)), % 0.59/0.68 inference(scs_inference,[],[87,95,110,112,101,125,2,140,148])). % 0.59/0.68 cnf(236,plain, % 0.59/0.68 ($false), % 0.59/0.68 inference(scs_inference,[],[219,110,2]), % 0.59/0.68 ['proof']). % 0.59/0.68 % SZS output end Proof % 0.59/0.68 % Total time :0.020000s %------------------------------------------------------------------------------