%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG124+4 : 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 : n016.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.83s 0.90s % Output : CNFRefutation 0.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : RNG124+4 : TPTP v8.2.0. Released v4.0.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n016.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:35:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.21/0.58 start to proof:theBenchmark % 0.81/0.87 %------------------------------------------- % 0.81/0.87 % File :CSE---1.7 % 0.81/0.87 % Problem :theBenchmark % 0.81/0.87 % Transform :cnf % 0.81/0.87 % Format :tptp:raw % 0.81/0.87 % Command :java -jar mcs_scs.jar %d %s % 0.81/0.87 % 0.81/0.87 % Result :Theorem 0.220000s % 0.81/0.87 % Output :CNFRefutation 0.220000s % 0.81/0.87 %------------------------------------------- % 0.81/0.88 %------------------------------------------------------------------------------ % 0.81/0.88 % File : RNG124+4 : TPTP v8.2.0. Released v4.0.0. % 0.81/0.88 % Domain : Ring Theory % 0.81/0.88 % Problem : Chinese remainder theorem in a ring 07_05_03_07, 03 expansion % 0.81/0.88 % Version : Especial. % 0.81/0.88 % English : % 0.81/0.88 % 0.81/0.88 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 0.81/0.88 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 0.81/0.88 % Source : [Pas08] % 0.81/0.88 % Names : chines_07_05_03_07.03 [Pas08] % 0.81/0.88 % 0.81/0.88 % Status : ContradictoryAxioms % 0.81/0.88 % Rating : 0.22 v8.2.0, 0.19 v8.1.0, 0.22 v7.4.0, 0.43 v7.3.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.17 v6.2.0, 0.20 v6.1.0, 0.27 v6.0.0, 0.26 v5.5.0, 0.30 v5.4.0, 0.36 v5.3.0, 0.37 v5.2.0, 0.25 v5.1.0, 0.38 v5.0.0, 0.42 v4.1.0, 0.57 v4.0.1, 0.78 v4.0.0 % 0.81/0.88 % Syntax : Number of formulae : 56 ( 6 unt; 9 def) % 0.81/0.88 % Number of atoms : 271 ( 67 equ) % 0.81/0.88 % Maximal formula atoms : 23 ( 4 avg) % 0.81/0.88 % Number of connectives : 230 ( 15 ~; 13 |; 132 &) % 0.81/0.88 % ( 17 <=>; 53 =>; 0 <=; 0 <~>) % 0.81/0.88 % Maximal formula depth : 18 ( 6 avg) % 0.81/0.88 % Maximal term depth : 4 ( 1 avg) % 0.81/0.88 % Number of predicates : 14 ( 11 usr; 2 prp; 0-3 aty) % 0.81/0.88 % Number of functors : 16 ( 16 usr; 9 con; 0-2 aty) % 0.81/0.88 % Number of variables : 130 ( 87 !; 43 ?) % 0.81/0.88 % SPC : FOF_CAX_RFO_SEQ % 0.81/0.88 % 0.81/0.88 % Comments : Problem generated by the SAD system [VLP07] % 0.81/0.88 %------------------------------------------------------------------------------ % 0.81/0.88 fof(mElmSort,axiom, % 0.81/0.88 ! [W0] : % 0.81/0.88 ( aElement0(W0) % 0.81/0.88 => $true ) ). % 0.81/0.88 % 0.81/0.88 fof(mSortsC,axiom, % 0.81/0.88 aElement0(sz00) ). % 0.81/0.88 % 0.81/0.88 fof(mSortsC_01,axiom, % 0.81/0.88 aElement0(sz10) ). % 0.81/0.88 % 0.81/0.88 fof(mSortsU,axiom, % 0.81/0.88 ! [W0] : % 0.81/0.88 ( aElement0(W0) % 0.81/0.88 => aElement0(smndt0(W0)) ) ). % 0.81/0.88 % 0.81/0.88 fof(mSortsB,axiom, % 0.81/0.88 ! [W0,W1] : % 0.81/0.88 ( ( aElement0(W0) % 0.81/0.88 & aElement0(W1) ) % 0.81/0.88 => aElement0(sdtpldt0(W0,W1)) ) ). % 0.81/0.88 % 0.81/0.88 fof(mSortsB_02,axiom, % 0.81/0.88 ! [W0,W1] : % 0.81/0.88 ( ( aElement0(W0) % 0.83/0.88 & aElement0(W1) ) % 0.83/0.88 => aElement0(sdtasdt0(W0,W1)) ) ). % 0.83/0.88 % 0.83/0.88 fof(mAddComm,axiom, % 0.83/0.88 ! [W0,W1] : % 0.83/0.88 ( ( aElement0(W0) % 0.83/0.88 & aElement0(W1) ) % 0.83/0.88 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 0.83/0.88 % 0.83/0.88 fof(mAddAsso,axiom, % 0.83/0.88 ! [W0,W1,W2] : % 0.83/0.88 ( ( aElement0(W0) % 0.83/0.88 & aElement0(W1) % 0.83/0.88 & aElement0(W2) ) % 0.83/0.88 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 0.83/0.88 % 0.83/0.88 fof(mAddZero,axiom, % 0.83/0.88 ! [W0] : % 0.83/0.88 ( aElement0(W0) % 0.83/0.88 => ( sdtpldt0(W0,sz00) = W0 % 0.83/0.88 & W0 = sdtpldt0(sz00,W0) ) ) ). % 0.83/0.88 % 0.83/0.88 fof(mAddInvr,axiom, % 0.83/0.88 ! [W0] : % 0.83/0.88 ( aElement0(W0) % 0.83/0.88 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 0.83/0.88 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 0.83/0.88 % 0.83/0.88 fof(mMulComm,axiom, % 0.83/0.88 ! [W0,W1] : % 0.83/0.88 ( ( aElement0(W0) % 0.83/0.88 & aElement0(W1) ) % 0.83/0.88 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 0.83/0.88 % 0.83/0.88 fof(mMulAsso,axiom, % 0.83/0.88 ! [W0,W1,W2] : % 0.83/0.88 ( ( aElement0(W0) % 0.83/0.88 & aElement0(W1) % 0.83/0.88 & aElement0(W2) ) % 0.83/0.88 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 0.83/0.88 % 0.83/0.88 fof(mMulUnit,axiom, % 0.83/0.88 ! [W0] : % 0.83/0.88 ( aElement0(W0) % 0.83/0.88 => ( sdtasdt0(W0,sz10) = W0 % 0.83/0.88 & W0 = sdtasdt0(sz10,W0) ) ) ). % 0.83/0.88 % 0.83/0.88 fof(mAMDistr,axiom, % 0.83/0.88 ! [W0,W1,W2] : % 0.83/0.88 ( ( aElement0(W0) % 0.83/0.88 & aElement0(W1) % 0.83/0.88 & aElement0(W2) ) % 0.83/0.88 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 0.83/0.88 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 0.83/0.88 % 0.83/0.88 fof(mMulMnOne,axiom, % 0.83/0.88 ! [W0] : % 0.83/0.88 ( aElement0(W0) % 0.83/0.88 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 0.83/0.88 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 0.83/0.88 % 0.83/0.88 fof(mMulZero,axiom, % 0.83/0.88 ! [W0] : % 0.83/0.88 ( aElement0(W0) % 0.83/0.88 => ( sdtasdt0(W0,sz00) = sz00 % 0.83/0.88 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 0.83/0.88 % 0.83/0.88 fof(mCancel,axiom, % 0.83/0.88 ! [W0,W1] : % 0.83/0.88 ( ( aElement0(W0) % 0.83/0.88 & aElement0(W1) ) % 0.83/0.88 => ( sdtasdt0(W0,W1) = sz00 % 0.83/0.88 => ( W0 = sz00 % 0.83/0.88 | W1 = sz00 ) ) ) ). % 0.83/0.88 % 0.83/0.88 fof(mUnNeZr,axiom, % 0.83/0.88 sz10 != sz00 ). % 0.83/0.88 % 0.83/0.88 fof(mSetSort,axiom, % 0.83/0.88 ! [W0] : % 0.83/0.88 ( aSet0(W0) % 0.83/0.88 => $true ) ). % 0.83/0.88 % 0.83/0.88 fof(mEOfElem,axiom, % 0.83/0.88 ! [W0] : % 0.83/0.88 ( aSet0(W0) % 0.83/0.88 => ! [W1] : % 0.83/0.88 ( aElementOf0(W1,W0) % 0.83/0.88 => aElement0(W1) ) ) ). % 0.83/0.88 % 0.83/0.88 fof(mSetEq,axiom, % 0.83/0.88 ! [W0,W1] : % 0.83/0.88 ( ( aSet0(W0) % 0.83/0.88 & aSet0(W1) ) % 0.83/0.88 => ( ( ! [W2] : % 0.83/0.88 ( aElementOf0(W2,W0) % 0.83/0.88 => aElementOf0(W2,W1) ) % 0.83/0.88 & ! [W2] : % 0.83/0.88 ( aElementOf0(W2,W1) % 0.83/0.88 => aElementOf0(W2,W0) ) ) % 0.83/0.89 => W0 = W1 ) ) ). % 0.83/0.89 % 0.83/0.89 fof(mDefSSum,definition, % 0.83/0.89 ! [W0,W1] : % 0.83/0.89 ( ( aSet0(W0) % 0.83/0.89 & aSet0(W1) ) % 0.83/0.89 => ! [W2] : % 0.83/0.89 ( W2 = sdtpldt1(W0,W1) % 0.83/0.89 <=> ( aSet0(W2) % 0.83/0.89 & ! [W3] : % 0.83/0.89 ( aElementOf0(W3,W2) % 0.83/0.89 <=> ? [W4,W5] : % 0.83/0.89 ( aElementOf0(W4,W0) % 0.83/0.89 & aElementOf0(W5,W1) % 0.83/0.89 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 0.83/0.89 % 0.83/0.89 fof(mDefSInt,definition, % 0.83/0.89 ! [W0,W1] : % 0.83/0.89 ( ( aSet0(W0) % 0.83/0.89 & aSet0(W1) ) % 0.83/0.89 => ! [W2] : % 0.83/0.89 ( W2 = sdtasasdt0(W0,W1) % 0.83/0.89 <=> ( aSet0(W2) % 0.83/0.89 & ! [W3] : % 0.83/0.89 ( aElementOf0(W3,W2) % 0.83/0.89 <=> ( aElementOf0(W3,W0) % 0.83/0.89 & aElementOf0(W3,W1) ) ) ) ) ) ). % 0.83/0.89 % 0.83/0.89 fof(mDefIdeal,definition, % 0.83/0.89 ! [W0] : % 0.83/0.89 ( aIdeal0(W0) % 0.83/0.89 <=> ( aSet0(W0) % 0.83/0.89 & ! [W1] : % 0.83/0.89 ( aElementOf0(W1,W0) % 0.83/0.89 => ( ! [W2] : % 0.83/0.89 ( aElementOf0(W2,W0) % 0.83/0.89 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 0.83/0.89 & ! [W2] : % 0.83/0.89 ( aElement0(W2) % 0.83/0.89 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 0.83/0.89 % 0.83/0.89 fof(mIdeSum,axiom, % 0.83/0.89 ! [W0,W1] : % 0.83/0.89 ( ( aIdeal0(W0) % 0.83/0.89 & aIdeal0(W1) ) % 0.83/0.89 => aIdeal0(sdtpldt1(W0,W1)) ) ). % 0.83/0.89 % 0.83/0.89 fof(mIdeInt,axiom, % 0.83/0.89 ! [W0,W1] : % 0.83/0.89 ( ( aIdeal0(W0) % 0.83/0.89 & aIdeal0(W1) ) % 0.83/0.89 => aIdeal0(sdtasasdt0(W0,W1)) ) ). % 0.83/0.89 % 0.83/0.89 fof(mDefMod,definition, % 0.83/0.89 ! [W0,W1,W2] : % 0.83/0.89 ( ( aElement0(W0) % 0.83/0.89 & aElement0(W1) % 0.83/0.89 & aIdeal0(W2) ) % 0.83/0.89 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 0.83/0.89 <=> aElementOf0(sdtpldt0(W0,smndt0(W1)),W2) ) ) ). % 0.83/0.89 % 0.83/0.89 fof(mChineseRemainder,axiom, % 0.83/0.89 ! [W0,W1] : % 0.83/0.89 ( ( aIdeal0(W0) % 0.83/0.89 & aIdeal0(W1) ) % 0.83/0.89 => ( ! [W2] : % 0.83/0.89 ( aElement0(W2) % 0.83/0.89 => aElementOf0(W2,sdtpldt1(W0,W1)) ) % 0.83/0.89 => ! [W2,W3] : % 0.83/0.89 ( ( aElement0(W2) % 0.83/0.89 & aElement0(W3) ) % 0.83/0.89 => ? [W4] : % 0.83/0.89 ( aElement0(W4) % 0.83/0.89 & sdteqdtlpzmzozddtrp0(W4,W2,W0) % 0.83/0.89 & sdteqdtlpzmzozddtrp0(W4,W3,W1) ) ) ) ) ). % 0.83/0.89 % 0.83/0.89 fof(mNatSort,axiom, % 0.83/0.89 ! [W0] : % 0.83/0.89 ( aNaturalNumber0(W0) % 0.83/0.89 => $true ) ). % 0.83/0.89 % 0.83/0.89 fof(mEucSort,axiom, % 0.83/0.89 ! [W0] : % 0.83/0.89 ( ( aElement0(W0) % 0.83/0.89 & W0 != sz00 ) % 0.83/0.89 => aNaturalNumber0(sbrdtbr0(W0)) ) ). % 0.83/0.89 % 0.83/0.89 fof(mNatLess,axiom, % 0.83/0.89 ! [W0,W1] : % 0.83/0.89 ( ( aNaturalNumber0(W0) % 0.83/0.89 & aNaturalNumber0(W1) ) % 0.83/0.89 => ( iLess0(W0,W1) % 0.83/0.89 => $true ) ) ). % 0.83/0.89 % 0.83/0.89 fof(mDivision,axiom, % 0.83/0.89 ! [W0,W1] : % 0.83/0.89 ( ( aElement0(W0) % 0.83/0.89 & aElement0(W1) % 0.83/0.89 & W1 != sz00 ) % 0.83/0.89 => ? [W2,W3] : % 0.83/0.89 ( aElement0(W2) % 0.83/0.89 & aElement0(W3) % 0.83/0.89 & W0 = sdtpldt0(sdtasdt0(W2,W1),W3) % 0.83/0.89 & ( W3 != sz00 % 0.83/0.89 => iLess0(sbrdtbr0(W3),sbrdtbr0(W1)) ) ) ) ). % 0.83/0.89 % 0.83/0.89 fof(mDefDiv,definition, % 0.83/0.89 ! [W0,W1] : % 0.83/0.89 ( ( aElement0(W0) % 0.83/0.89 & aElement0(W1) ) % 0.83/0.89 => ( doDivides0(W0,W1) % 0.83/0.89 <=> ? [W2] : % 0.83/0.89 ( aElement0(W2) % 0.83/0.89 & sdtasdt0(W0,W2) = W1 ) ) ) ). % 0.83/0.89 % 0.83/0.89 fof(mDefDvs,definition, % 0.83/0.89 ! [W0] : % 0.83/0.89 ( aElement0(W0) % 0.83/0.89 => ! [W1] : % 0.83/0.89 ( aDivisorOf0(W1,W0) % 0.83/0.89 <=> ( aElement0(W1) % 0.83/0.89 & doDivides0(W1,W0) ) ) ) ). % 0.83/0.89 % 0.83/0.89 fof(mDefGCD,definition, % 0.83/0.89 ! [W0,W1] : % 0.83/0.89 ( ( aElement0(W0) % 0.83/0.89 & aElement0(W1) ) % 0.83/0.89 => ! [W2] : % 0.83/0.89 ( aGcdOfAnd0(W2,W0,W1) % 0.83/0.89 <=> ( aDivisorOf0(W2,W0) % 0.83/0.89 & aDivisorOf0(W2,W1) % 0.83/0.89 & ! [W3] : % 0.83/0.89 ( ( aDivisorOf0(W3,W0) % 0.83/0.89 & aDivisorOf0(W3,W1) ) % 0.83/0.89 => doDivides0(W3,W2) ) ) ) ) ). % 0.83/0.89 % 0.83/0.89 fof(mDefRel,definition, % 0.83/0.89 ! [W0,W1] : % 0.83/0.89 ( ( aElement0(W0) % 0.83/0.89 & aElement0(W1) ) % 0.83/0.89 => ( misRelativelyPrime0(W0,W1) % 0.83/0.89 <=> aGcdOfAnd0(sz10,W0,W1) ) ) ). % 0.83/0.89 % 0.83/0.89 fof(mDefPrIdeal,definition, % 0.83/0.89 ! [W0] : % 0.83/0.89 ( aElement0(W0) % 0.83/0.89 => ! [W1] : % 0.83/0.89 ( W1 = slsdtgt0(W0) % 0.83/0.89 <=> ( aSet0(W1) % 0.83/0.89 & ! [W2] : % 0.83/0.89 ( aElementOf0(W2,W1) % 0.83/0.89 <=> ? [W3] : % 0.83/0.89 ( aElement0(W3) % 0.83/0.89 & sdtasdt0(W0,W3) = W2 ) ) ) ) ) ). % 0.83/0.89 % 0.83/0.89 fof(mPrIdeal,axiom, % 0.83/0.89 ! [W0] : % 0.83/0.89 ( aElement0(W0) % 0.83/0.89 => aIdeal0(slsdtgt0(W0)) ) ). % 0.83/0.89 % 0.83/0.89 fof(m__2091,hypothesis, % 0.83/0.89 ( aElement0(xa) % 0.83/0.89 & aElement0(xb) ) ). % 0.83/0.89 % 0.83/0.89 fof(m__2110,hypothesis, % 0.83/0.89 ( xa != sz00 % 0.83/0.89 | xb != sz00 ) ). % 0.83/0.89 % 0.83/0.89 fof(m__2129,hypothesis, % 0.83/0.89 ( aElement0(xc) % 0.83/0.89 & ? [W0] : % 0.83/0.89 ( aElement0(W0) % 0.83/0.89 & sdtasdt0(xc,W0) = xa ) % 0.83/0.89 & doDivides0(xc,xa) % 0.83/0.89 & aDivisorOf0(xc,xa) % 0.83/0.89 & aElement0(xc) % 0.83/0.89 & ? [W0] : % 0.83/0.89 ( aElement0(W0) % 0.83/0.89 & sdtasdt0(xc,W0) = xb ) % 0.83/0.89 & doDivides0(xc,xb) % 0.83/0.89 & aDivisorOf0(xc,xb) % 0.83/0.89 & ! [W0] : % 0.83/0.89 ( ( ( ( aElement0(W0) % 0.83/0.89 & ( ? [W1] : % 0.83/0.89 ( aElement0(W1) % 0.83/0.89 & sdtasdt0(W0,W1) = xa ) % 0.83/0.89 | doDivides0(W0,xa) ) ) % 0.83/0.89 | aDivisorOf0(W0,xa) ) % 0.83/0.89 & ( ? [W1] : % 0.83/0.89 ( aElement0(W1) % 0.83/0.89 & sdtasdt0(W0,W1) = xb ) % 0.83/0.89 | doDivides0(W0,xb) % 0.83/0.89 | aDivisorOf0(W0,xb) ) ) % 0.83/0.89 => ( ? [W1] : % 0.83/0.89 ( aElement0(W1) % 0.83/0.89 & sdtasdt0(W0,W1) = xc ) % 0.83/0.89 & doDivides0(W0,xc) ) ) % 0.83/0.89 & aGcdOfAnd0(xc,xa,xb) ) ). % 0.83/0.89 % 0.83/0.89 fof(m__2174,hypothesis, % 0.83/0.89 ( aSet0(xI) % 0.83/0.89 & ! [W0] : % 0.83/0.89 ( aElementOf0(W0,xI) % 0.83/0.89 => ( ! [W1] : % 0.83/0.89 ( aElementOf0(W1,xI) % 0.83/0.89 => aElementOf0(sdtpldt0(W0,W1),xI) ) % 0.83/0.89 & ! [W1] : % 0.83/0.89 ( aElement0(W1) % 0.83/0.89 => aElementOf0(sdtasdt0(W1,W0),xI) ) ) ) % 0.83/0.89 & aIdeal0(xI) % 0.83/0.89 & ! [W0] : % 0.83/0.89 ( aElementOf0(W0,slsdtgt0(xa)) % 0.83/0.89 <=> ? [W1] : % 0.83/0.89 ( aElement0(W1) % 0.83/0.89 & sdtasdt0(xa,W1) = W0 ) ) % 0.83/0.89 & ! [W0] : % 0.83/0.89 ( aElementOf0(W0,slsdtgt0(xb)) % 0.83/0.89 <=> ? [W1] : % 0.83/0.89 ( aElement0(W1) % 0.83/0.89 & sdtasdt0(xb,W1) = W0 ) ) % 0.83/0.89 & ! [W0] : % 0.83/0.89 ( aElementOf0(W0,xI) % 0.83/0.89 <=> ? [W1,W2] : % 0.83/0.89 ( aElementOf0(W1,slsdtgt0(xa)) % 0.83/0.89 & aElementOf0(W2,slsdtgt0(xb)) % 0.83/0.89 & sdtpldt0(W1,W2) = W0 ) ) % 0.83/0.89 & xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ) ). % 0.83/0.89 % 0.83/0.89 fof(m__2203,hypothesis, % 0.83/0.89 ( ? [W0] : % 0.83/0.89 ( aElement0(W0) % 0.83/0.89 & sdtasdt0(xa,W0) = sz00 ) % 0.83/0.89 & aElementOf0(sz00,slsdtgt0(xa)) % 0.83/0.89 & ? [W0] : % 0.83/0.89 ( aElement0(W0) % 0.83/0.89 & sdtasdt0(xa,W0) = xa ) % 0.83/0.89 & aElementOf0(xa,slsdtgt0(xa)) % 0.83/0.89 & ? [W0] : % 0.83/0.89 ( aElement0(W0) % 0.83/0.89 & sdtasdt0(xb,W0) = sz00 ) % 0.83/0.89 & aElementOf0(sz00,slsdtgt0(xb)) % 0.83/0.89 & ? [W0] : % 0.83/0.89 ( aElement0(W0) % 0.83/0.89 & sdtasdt0(xb,W0) = xb ) % 0.83/0.89 & aElementOf0(xb,slsdtgt0(xb)) ) ). % 0.83/0.89 % 0.83/0.89 fof(m__2228,hypothesis, % 0.83/0.89 ? [W0] : % 0.83/0.89 ( ! [W1] : % 0.83/0.89 ( aElementOf0(W1,slsdtgt0(xa)) % 0.83/0.89 <=> ? [W2] : % 0.83/0.89 ( aElement0(W2) % 0.83/0.89 & sdtasdt0(xa,W2) = W1 ) ) % 0.83/0.89 & ! [W1] : % 0.83/0.89 ( aElementOf0(W1,slsdtgt0(xb)) % 0.83/0.89 <=> ? [W2] : % 0.83/0.89 ( aElement0(W2) % 0.83/0.89 & sdtasdt0(xb,W2) = W1 ) ) % 0.83/0.89 & ? [W1,W2] : % 0.83/0.89 ( aElementOf0(W1,slsdtgt0(xa)) % 0.83/0.89 & aElementOf0(W2,slsdtgt0(xb)) % 0.83/0.89 & sdtpldt0(W1,W2) = W0 ) % 0.83/0.89 & aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) % 0.83/0.89 & W0 != sz00 ) ). % 0.83/0.89 % 0.83/0.89 fof(m__2273,hypothesis, % 0.83/0.89 ( ? [W0,W1] : % 0.83/0.89 ( aElementOf0(W0,slsdtgt0(xa)) % 0.83/0.89 & aElementOf0(W1,slsdtgt0(xb)) % 0.83/0.89 & sdtpldt0(W0,W1) = xu ) % 0.83/0.89 & aElementOf0(xu,xI) % 0.83/0.89 & xu != sz00 % 0.83/0.89 & ! [W0] : % 0.83/0.89 ( ( ( ? [W1,W2] : % 0.83/0.89 ( aElementOf0(W1,slsdtgt0(xa)) % 0.83/0.89 & aElementOf0(W2,slsdtgt0(xb)) % 0.83/0.89 & sdtpldt0(W1,W2) = W0 ) % 0.83/0.89 | aElementOf0(W0,xI) ) % 0.83/0.89 & W0 != sz00 ) % 0.83/0.89 => ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu)) ) ) ). % 0.83/0.89 % 0.83/0.89 fof(m__2383,hypothesis, % 0.83/0.89 ~ ( ( ? [W0] : % 0.83/0.89 ( aElement0(W0) % 0.83/0.89 & sdtasdt0(xu,W0) = xa ) % 0.83/0.89 | doDivides0(xu,xa) % 0.83/0.89 | aDivisorOf0(xu,xa) ) % 0.83/0.89 & ( ? [W0] : % 0.83/0.90 ( aElement0(W0) % 0.83/0.90 & sdtasdt0(xu,W0) = xb ) % 0.83/0.90 | doDivides0(xu,xb) % 0.83/0.90 | aDivisorOf0(xu,xb) ) ) ). % 0.83/0.90 % 0.83/0.90 fof(m__2416,hypothesis, % 0.83/0.90 ? [W0,W1] : % 0.83/0.90 ( aElement0(W0) % 0.83/0.90 & aElement0(W1) % 0.83/0.90 & xu = sdtpldt0(sdtasdt0(xa,W0),sdtasdt0(xb,W1)) ) ). % 0.83/0.90 % 0.83/0.90 fof(m__2479,hypothesis, % 0.83/0.90 ~ ~ ( ? [W0] : % 0.83/0.90 ( aElement0(W0) % 0.83/0.90 & sdtasdt0(xu,W0) = xa ) % 0.83/0.90 & doDivides0(xu,xa) ) ). % 0.83/0.90 % 0.83/0.90 fof(m__2612,hypothesis, % 0.83/0.90 ~ ( ? [W0] : % 0.83/0.90 ( aElement0(W0) % 0.83/0.90 & sdtasdt0(xu,W0) = xb ) % 0.83/0.90 | doDivides0(xu,xb) ) ). % 0.83/0.90 % 0.83/0.90 fof(m__2666,hypothesis, % 0.83/0.90 ( aElement0(xq) % 0.83/0.90 & aElement0(xr) % 0.83/0.90 & xb = sdtpldt0(sdtasdt0(xq,xu),xr) % 0.83/0.90 & ( xr = sz00 % 0.83/0.90 | iLess0(sbrdtbr0(xr),sbrdtbr0(xu)) ) ) ). % 0.83/0.90 % 0.83/0.90 fof(m__2673,hypothesis, % 0.83/0.90 xr != sz00 ). % 0.83/0.90 % 0.83/0.90 fof(m__2690,hypothesis, % 0.83/0.90 ( ? [W0,W1] : % 0.83/0.90 ( aElementOf0(W0,slsdtgt0(xa)) % 0.83/0.90 & aElementOf0(W1,slsdtgt0(xb)) % 0.83/0.90 & sdtpldt0(W0,W1) = smndt0(sdtasdt0(xq,xu)) ) % 0.83/0.90 & aElementOf0(smndt0(sdtasdt0(xq,xu)),xI) ) ). % 0.83/0.90 % 0.83/0.90 fof(m__2699,hypothesis, % 0.83/0.90 ( ? [W0,W1] : % 0.83/0.90 ( aElementOf0(W0,slsdtgt0(xa)) % 0.83/0.90 & aElementOf0(W1,slsdtgt0(xb)) % 0.83/0.90 & sdtpldt0(W0,W1) = xb ) % 0.83/0.90 & ? [W0,W1] : % 0.83/0.90 ( aElementOf0(W0,slsdtgt0(xa)) % 0.83/0.90 & aElementOf0(W1,slsdtgt0(xb)) % 0.83/0.90 & sdtpldt0(W0,W1) = xb ) % 0.83/0.90 & aElementOf0(xb,xI) ) ). % 0.83/0.90 % 0.83/0.90 fof(m__2718,hypothesis, % 0.83/0.90 xr = sdtpldt0(smndt0(sdtasdt0(xq,xu)),xb) ). % 0.83/0.90 % 0.83/0.90 fof(m__2729,hypothesis, % 0.83/0.90 ( ? [W0,W1] : % 0.83/0.90 ( aElementOf0(W0,slsdtgt0(xa)) % 0.83/0.90 & aElementOf0(W1,slsdtgt0(xb)) % 0.83/0.90 & sdtpldt0(W0,W1) = xr ) % 0.83/0.90 & aElementOf0(xr,xI) ) ). % 0.83/0.90 % 0.83/0.90 fof(m__,conjecture, % 0.83/0.90 $false ). % 0.83/0.90 % 0.83/0.90 %------------------------------------------------------------------------------ % 0.83/0.90 %------------------------------------------- % 0.83/0.90 % Proof found % 0.83/0.90 % SZS status Theorem for theBenchmark % 0.83/0.90 % SZS output start Proof % 0.83/0.90 %ClaNum:300(EqnAxiom:90) % 0.83/0.90 %VarNum:909(SingletonVarNum:286) % 0.83/0.90 %MaxLitNum:8 % 0.83/0.90 %MaxfuncDepth:3 % 0.83/0.90 %SharedTerms:125 % 0.83/0.90 [91]P1(a1) % 0.83/0.90 [92]P1(a56) % 0.83/0.90 [93]P1(a57) % 0.83/0.90 [94]P1(a59) % 0.83/0.90 [96]P1(a60) % 0.83/0.90 [97]P1(a61) % 0.83/0.90 [98]P1(a62) % 0.83/0.90 [99]P1(a2) % 0.83/0.90 [100]P1(a15) % 0.83/0.90 [101]P1(a16) % 0.83/0.90 [102]P1(a22) % 0.83/0.90 [103]P1(a23) % 0.83/0.90 [104]P1(a25) % 0.83/0.90 [105]P1(a26) % 0.83/0.90 [106]P1(a34) % 0.83/0.90 [107]P1(a36) % 0.83/0.90 [108]P3(a58) % 0.83/0.90 [109]P4(a58) % 0.83/0.90 [121]P5(a59,a58) % 0.83/0.90 [122]P5(a63,a58) % 0.83/0.90 [123]P5(a62,a58) % 0.83/0.90 [124]P8(a60,a57) % 0.83/0.90 [125]P8(a60,a59) % 0.83/0.90 [126]P8(a63,a57) % 0.83/0.90 [127]P2(a60,a57) % 0.83/0.90 [128]P2(a60,a59) % 0.83/0.90 [146]P6(a60,a57,a59) % 0.83/0.90 [151]~E(a1,a56) % 0.83/0.90 [152]~E(a1,a63) % 0.83/0.90 [153]~E(a1,a62) % 0.83/0.90 [154]~E(a1,a28) % 0.83/0.90 [155]~P8(a63,a59) % 0.83/0.90 [110]E(f37(a27,a31),a28) % 0.83/0.90 [111]E(f37(a32,a33),a63) % 0.83/0.90 [112]E(f37(a38,a41),a59) % 0.83/0.90 [113]E(f37(a42,a43),a62) % 0.83/0.90 [114]E(f44(a57,a16),a1) % 0.83/0.90 [115]E(f44(a57,a22),a57) % 0.83/0.90 [116]E(f44(a59,a23),a1) % 0.83/0.90 [117]E(f44(a59,a25),a59) % 0.83/0.90 [118]E(f44(a60,a2),a57) % 0.83/0.90 [119]E(f44(a60,a15),a59) % 0.83/0.90 [120]E(f44(a63,a36),a57) % 0.83/0.90 [129]P5(a1,f53(a57)) % 0.83/0.90 [130]P5(a1,f53(a59)) % 0.83/0.90 [131]P5(a57,f53(a57)) % 0.83/0.90 [132]P5(a59,f53(a59)) % 0.83/0.90 [133]P5(a27,f53(a57)) % 0.83/0.90 [134]P5(a31,f53(a59)) % 0.83/0.90 [135]P5(a32,f53(a57)) % 0.83/0.90 [136]P5(a33,f53(a59)) % 0.83/0.90 [137]P5(a39,f53(a57)) % 0.83/0.90 [138]P5(a40,f53(a59)) % 0.83/0.90 [139]P5(a38,f53(a57)) % 0.83/0.90 [140]P5(a41,f53(a59)) % 0.83/0.90 [141]P5(a42,f53(a57)) % 0.83/0.90 [142]P5(a43,f53(a59)) % 0.83/0.90 [143]E(f54(f53(a57),f53(a59)),a58) % 0.83/0.90 [144]E(f37(f44(a61,a63),a62),a59) % 0.83/0.90 [145]E(f55(f44(a61,a63)),f37(a39,a40)) % 0.83/0.90 [147]P5(a28,f54(f53(a57),f53(a59))) % 0.83/0.90 [148]E(f37(f44(a57,a26),f44(a59,a34)),a63) % 0.83/0.90 [150]P5(f55(f44(a61,a63)),a58) % 0.83/0.90 [149]E(f37(f55(f44(a61,a63)),a59),a62) % 0.83/0.90 [156]~E(a1,a57)+~E(a1,a59) % 0.83/0.90 [178]~P8(a63,a57)+~P2(a63,a59) % 0.83/0.90 [180]~P2(a63,a57)+~P2(a63,a59) % 0.83/0.90 [168]E(a1,a62)+P9(f45(a62),f45(a63)) % 0.83/0.90 [157]~P4(x1571)+P3(x1571) % 0.83/0.90 [158]~P1(x1581)+P1(f55(x1581)) % 0.83/0.90 [159]~P1(x1591)+P4(f53(x1591)) % 0.83/0.90 [161]~P1(x1611)+E(f44(a1,x1611),a1) % 0.83/0.90 [162]~P1(x1621)+E(f44(x1621,a1),a1) % 0.83/0.90 [164]~P1(x1641)+E(f37(a1,x1641),x1641) % 0.83/0.90 [165]~P1(x1651)+E(f44(a56,x1651),x1651) % 0.83/0.90 [166]~P1(x1661)+E(f37(x1661,a1),x1661) % 0.83/0.90 [167]~P1(x1671)+E(f44(x1671,a56),x1671) % 0.83/0.90 [169]~P1(x1691)+~E(f44(a63,x1691),a59) % 0.83/0.90 [181]~P5(x1811,f53(a57))+P1(f17(x1811)) % 0.83/0.90 [182]~P5(x1821,f53(a59))+P1(f19(x1821)) % 0.83/0.90 [183]~P5(x1831,f53(a57))+P1(f29(x1831)) % 0.83/0.90 [184]~P5(x1841,f53(a59))+P1(f30(x1841)) % 0.83/0.90 [191]~P5(x1911,a58)+P5(f20(x1911),f53(a57)) % 0.83/0.90 [192]~P5(x1921,a58)+P5(f21(x1921),f53(a59)) % 0.83/0.90 [170]~P1(x1701)+E(f37(f55(x1701),x1701),a1) % 0.83/0.90 [171]~P1(x1711)+E(f37(x1711,f55(x1711)),a1) % 0.83/0.90 [172]~P1(x1721)+E(f44(x1721,f55(a56)),f55(x1721)) % 0.83/0.90 [173]~P1(x1731)+E(f44(f55(a56),x1731),f55(x1731)) % 0.83/0.90 [208]~P5(x2081,f53(a57))+E(f44(a57,f17(x2081)),x2081) % 0.83/0.90 [209]~P5(x2091,f53(a57))+E(f44(a57,f29(x2091)),x2091) % 0.83/0.90 [210]~P5(x2101,f53(a59))+E(f44(a59,f19(x2101)),x2101) % 0.83/0.90 [211]~P5(x2111,f53(a59))+E(f44(a59,f30(x2111)),x2111) % 0.83/0.90 [212]~P5(x2121,a58)+E(f37(f20(x2121),f21(x2121)),x2121) % 0.83/0.90 [216]~P8(x2161,a59)+~P2(x2161,a57)+P8(x2161,a60) % 0.83/0.90 [217]~P2(x2171,a57)+~P2(x2171,a59)+P8(x2171,a60) % 0.83/0.90 [160]~P1(x1601)+E(x1601,a1)+P7(f45(x1601)) % 0.83/0.90 [174]~P3(x1741)+P4(x1741)+P5(f46(x1741),x1741) % 0.83/0.90 [199]~P1(x1991)+~P2(a63,a59)+~E(f44(a63,x1991),a57) % 0.83/0.90 [213]~P8(x2131,a59)+~P2(x2131,a57)+P1(f18(x2131)) % 0.83/0.90 [214]~P2(x2141,a57)+~P2(x2141,a59)+P1(f18(x2141)) % 0.83/0.90 [221]~P5(x2211,a58)+E(x2211,a1)+~P9(f45(x2211),f45(a63)) % 0.83/0.90 [227]~P8(x2271,a59)+~P2(x2271,a57)+E(f44(x2271,f18(x2271)),a60) % 0.83/0.90 [228]~P2(x2281,a57)+~P2(x2281,a59)+E(f44(x2281,f18(x2281)),a60) % 0.83/0.90 [175]~P5(x1751,x1752)+P1(x1751)+~P3(x1752) % 0.83/0.90 [176]~P2(x1761,x1762)+P1(x1761)+~P1(x1762) % 0.83/0.90 [193]~P1(x1932)+~P2(x1931,x1932)+P8(x1931,x1932) % 0.83/0.90 [163]~P1(x1632)+P3(x1631)+~E(x1631,f53(x1632)) % 0.83/0.90 [186]~P1(x1862)+~P1(x1861)+E(f37(x1861,x1862),f37(x1862,x1861)) % 0.83/0.90 [187]~P1(x1872)+~P1(x1871)+E(f44(x1871,x1872),f44(x1872,x1871)) % 0.83/0.90 [194]~P1(x1942)+~P1(x1941)+P1(f37(x1941,x1942)) % 0.83/0.90 [195]~P1(x1952)+~P1(x1951)+P1(f44(x1951,x1952)) % 0.83/0.90 [196]~P4(x1962)+~P4(x1961)+P4(f54(x1961,x1962)) % 0.83/0.90 [197]~P4(x1972)+~P4(x1971)+P4(f52(x1971,x1972)) % 0.83/0.90 [203]~P1(x2032)+~E(f44(a57,x2032),x2031)+P5(x2031,f53(a57)) % 0.83/0.90 [205]~P1(x2052)+~E(f44(a59,x2052),x2051)+P5(x2051,f53(a59)) % 0.83/0.90 [230]~P1(x2301)+~P5(x2302,a58)+P5(f44(x2301,x2302),a58) % 0.83/0.90 [249]~P5(x2491,a58)+~P5(x2492,a58)+P5(f37(x2491,x2492),a58) % 0.83/0.90 [223]~P1(x2231)+~P8(x2231,a57)+~P8(x2231,a59)+P8(x2231,a60) % 0.83/0.90 [224]~P1(x2241)+~P8(x2241,a57)+~P2(x2241,a59)+P8(x2241,a60) % 0.83/0.90 [190]~P3(x1901)+P4(x1901)+P5(f4(x1901),x1901)+P1(f3(x1901)) % 0.83/0.90 [219]~P1(x2191)+~P8(x2191,a57)+~P8(x2191,a59)+P1(f18(x2191)) % 0.83/0.90 [220]~P1(x2201)+~P8(x2201,a57)+~P2(x2201,a59)+P1(f18(x2201)) % 0.83/0.90 [235]~P1(x2351)+~P8(x2351,a57)+~P8(x2351,a59)+E(f44(x2351,f18(x2351)),a60) % 0.83/0.90 [236]~P1(x2361)+~P8(x2361,a57)+~P2(x2361,a59)+E(f44(x2361,f18(x2361)),a60) % 0.83/0.90 [269]~P3(x2691)+P4(x2691)+P1(f3(x2691))+~P5(f37(f46(x2691),f4(x2691)),x2691) % 0.83/0.90 [272]~P3(x2721)+P4(x2721)+P5(f4(x2721),x2721)+~P5(f44(f3(x2721),f46(x2721)),x2721) % 0.83/0.90 [281]~P3(x2811)+P4(x2811)+~P5(f37(f46(x2811),f4(x2811)),x2811)+~P5(f44(f3(x2811),f46(x2811)),x2811) % 0.83/0.90 [215]~P1(x2152)+~P1(x2151)+~P8(x2151,x2152)+P2(x2151,x2152) % 0.83/0.90 [252]~P1(x2522)+~P1(x2521)+~P10(x2521,x2522)+P6(a56,x2521,x2522) % 0.83/0.90 [261]~P1(x2612)+~P1(x2611)+P10(x2611,x2612)+~P6(a56,x2611,x2612) % 0.83/0.90 [206]~P1(x2061)+~P1(x2062)+E(x2061,a1)+P1(f5(x2062,x2061)) % 0.83/0.90 [207]~P1(x2071)+~P1(x2072)+E(x2071,a1)+P1(f8(x2072,x2071)) % 0.83/0.90 [225]~P1(x2252)+~P2(x2251,a57)+P1(f18(x2251))+~E(f44(x2251,x2252),a59) % 0.83/0.90 [229]~P1(x2292)+~P2(x2291,a57)+P8(x2291,a60)+~E(f44(x2291,x2292),a59) % 0.83/0.90 [231]~P1(x2312)+~P1(x2311)+~P8(x2311,x2312)+P1(f9(x2311,x2312)) % 0.83/0.90 [240]~P1(x2402)+~P2(x2401,a57)+~E(f44(x2401,x2402),a59)+E(f44(x2401,f18(x2401)),a60) % 0.83/0.90 [248]~P1(x2482)+~P1(x2481)+~P8(x2481,x2482)+E(f44(x2481,f9(x2481,x2482)),x2482) % 0.83/0.90 [274]~P1(x2741)+~P1(x2742)+E(x2741,a1)+E(f37(f44(f5(x2742,x2741),x2741),f8(x2742,x2741)),x2742) % 0.83/0.90 [263]~P1(x2632)+~P6(x2631,x2633,x2632)+P2(x2631,x2632)+~P1(x2633) % 0.83/0.90 [264]~P1(x2642)+~P6(x2641,x2642,x2643)+P2(x2641,x2642)+~P1(x2643) % 0.83/0.90 [188]~P3(x1883)+~P3(x1882)+P3(x1881)+~E(x1881,f54(x1882,x1883)) % 0.83/0.90 [189]~P3(x1893)+~P3(x1892)+P3(x1891)+~E(x1891,f52(x1892,x1893)) % 0.83/0.90 [243]~P1(x2431)+~P4(x2433)+~P5(x2432,x2433)+P5(f44(x2431,x2432),x2433) % 0.83/0.90 [254]P5(x2541,a58)+~E(f37(x2542,x2543),x2541)+~P5(x2543,f53(a59))+~P5(x2542,f53(a57)) % 0.83/0.90 [255]~P4(x2553)+~P5(x2551,x2553)+~P5(x2552,x2553)+P5(f37(x2551,x2552),x2553) % 0.83/0.90 [276]~P1(x2761)+~P5(x2763,x2762)+~E(x2762,f53(x2761))+P1(f12(x2761,x2762,x2763)) % 0.83/0.90 [258]~P1(x2583)+~P1(x2582)+~P1(x2581)+E(f37(f37(x2581,x2582),x2583),f37(x2581,f37(x2582,x2583))) % 0.83/0.90 [259]~P1(x2593)+~P1(x2592)+~P1(x2591)+E(f44(f44(x2591,x2592),x2593),f44(x2591,f44(x2592,x2593))) % 0.83/0.90 [270]~P1(x2703)+~P1(x2702)+~P1(x2701)+E(f37(f44(x2701,x2702),f44(x2701,x2703)),f44(x2701,f37(x2702,x2703))) % 0.83/0.90 [271]~P1(x2712)+~P1(x2713)+~P1(x2711)+E(f37(f44(x2711,x2712),f44(x2713,x2712)),f44(f37(x2711,x2713),x2712)) % 0.83/0.90 [278]~P1(x2781)+~P5(x2783,x2782)+~E(x2782,f53(x2781))+E(f44(x2781,f12(x2781,x2782,x2783)),x2783) % 0.83/0.90 [185]~P1(x1851)+~P1(x1852)+E(x1851,a1)+E(x1852,a1)+~E(f44(x1852,x1851),a1) % 0.83/0.90 [232]~P1(x2322)+~P1(x2321)+~P8(x2321,a59)+P1(f18(x2321))+~E(f44(x2321,x2322),a57) % 0.83/0.90 [233]~P1(x2332)+~P1(x2331)+~P2(x2331,a59)+P1(f18(x2331))+~E(f44(x2331,x2332),a57) % 0.83/0.90 [234]~P1(x2342)+~P1(x2341)+~P8(x2341,a57)+P1(f18(x2341))+~E(f44(x2341,x2342),a59) % 0.83/0.90 [237]~P1(x2372)+~P1(x2371)+~P8(x2371,a59)+P8(x2371,a60)+~E(f44(x2371,x2372),a57) % 0.83/0.90 [238]~P1(x2382)+~P1(x2381)+~P2(x2381,a59)+P8(x2381,a60)+~E(f44(x2381,x2382),a57) % 0.83/0.90 [239]~P1(x2392)+~P1(x2391)+~P8(x2391,a57)+P8(x2391,a60)+~E(f44(x2391,x2392),a59) % 0.83/0.90 [253]~P1(x2532)+~P3(x2531)+P5(f11(x2532,x2531),x2531)+E(x2531,f53(x2532))+P1(f10(x2532,x2531)) % 0.83/0.90 [256]~P3(x2562)+~P3(x2561)+E(x2561,x2562)+P5(f14(x2561,x2562),x2561)+P5(f24(x2561,x2562),x2562) % 0.83/0.90 [266]~P3(x2662)+~P3(x2661)+E(x2661,x2662)+P5(f14(x2661,x2662),x2661)+~P5(f24(x2661,x2662),x2661) % 0.83/0.90 [267]~P3(x2672)+~P3(x2671)+E(x2671,x2672)+P5(f24(x2671,x2672),x2672)+~P5(f14(x2671,x2672),x2672) % 0.83/0.90 [275]~P3(x2752)+~P3(x2751)+E(x2751,x2752)+~P5(f14(x2751,x2752),x2752)+~P5(f24(x2751,x2752),x2751) % 0.83/0.90 [245]~P1(x2452)+~P1(x2451)+~P8(x2451,a59)+~E(f44(x2451,x2452),a57)+E(f44(x2451,f18(x2451)),a60) % 0.83/0.90 [246]~P1(x2462)+~P1(x2461)+~P2(x2461,a59)+~E(f44(x2461,x2462),a57)+E(f44(x2461,f18(x2461)),a60) % 0.83/0.90 [247]~P1(x2472)+~P1(x2471)+~P8(x2471,a57)+~E(f44(x2471,x2472),a59)+E(f44(x2471,f18(x2471)),a60) % 0.83/0.90 [260]~P1(x2601)+~P1(x2602)+E(x2601,a1)+P9(f45(f8(x2602,x2601)),f45(x2601))+E(f8(x2602,x2601),a1) % 0.83/0.90 [262]~P1(x2622)+~P3(x2621)+P5(f11(x2622,x2621),x2621)+E(x2621,f53(x2622))+E(f44(x2622,f10(x2622,x2621)),f11(x2622,x2621)) % 0.83/0.90 [222]~P1(x2222)+~P1(x2221)+~P1(x2223)+P8(x2221,x2222)+~E(f44(x2221,x2223),x2222) % 0.83/0.90 [265]E(x2651,a1)+~E(f37(x2652,x2653),x2651)+~P5(x2653,f53(a59))+~P5(x2652,f53(a57))+~P9(f45(x2651),f45(a63)) % 0.83/0.90 [277]~P1(x2772)+~P1(x2771)+~P4(x2773)+P11(x2771,x2772,x2773)+~P5(f37(x2771,f55(x2772)),x2773) % 0.83/0.90 [279]~P1(x2792)+~P1(x2791)+~P4(x2793)+~P11(x2791,x2792,x2793)+P5(f37(x2791,f55(x2792)),x2793) % 0.83/0.90 [226]~P1(x2263)+~P1(x2264)+P5(x2261,x2262)+~E(f44(x2263,x2264),x2261)+~E(x2262,f53(x2263)) % 0.83/0.90 [241]~P3(x2414)+~P3(x2412)+~P5(x2411,x2413)+P5(x2411,x2412)+~E(x2413,f52(x2414,x2412)) % 0.83/0.90 [242]~P3(x2424)+~P3(x2422)+~P5(x2421,x2423)+P5(x2421,x2422)+~E(x2423,f52(x2422,x2424)) % 0.83/0.90 [292]~P3(x2922)+~P3(x2921)+~P5(x2924,x2923)+~E(x2923,f54(x2921,x2922))+P5(f35(x2921,x2922,x2923,x2924),x2921) % 0.83/0.90 [293]~P3(x2932)+~P3(x2931)+~P5(x2934,x2933)+~E(x2933,f54(x2931,x2932))+P5(f48(x2931,x2932,x2933,x2934),x2932) % 0.83/0.90 [300]~P3(x3002)+~P3(x3001)+~P5(x3004,x3003)+~E(x3003,f54(x3001,x3002))+E(f37(f35(x3001,x3002,x3003,x3004),f48(x3001,x3002,x3003,x3004)),x3004) % 0.83/0.90 [244]~P1(x2442)+~P1(x2443)+~P1(x2441)+P1(f18(x2441))+~E(f44(x2441,x2442),a57)+~E(f44(x2441,x2443),a59) % 0.83/0.90 [250]~P1(x2502)+~P1(x2503)+~P1(x2501)+P8(x2501,a60)+~E(f44(x2501,x2502),a57)+~E(f44(x2501,x2503),a59) % 0.83/0.90 [273]~P1(x2733)+~P1(x2732)+~P3(x2731)+~P5(f11(x2732,x2731),x2731)+~E(f11(x2732,x2731),f44(x2732,x2733))+E(x2731,f53(x2732)) % 0.83/0.90 [282]~P1(x2823)+~P1(x2822)+~P2(x2821,x2823)+~P2(x2821,x2822)+P6(x2821,x2822,x2823)+P2(f13(x2822,x2823,x2821),x2823) % 0.83/0.90 [283]~P1(x2833)+~P1(x2832)+~P2(x2831,x2833)+~P2(x2831,x2832)+P6(x2831,x2832,x2833)+P2(f13(x2832,x2833,x2831),x2832) % 0.83/0.90 [284]~P3(x2841)+~P3(x2843)+~P3(x2842)+P5(f47(x2842,x2843,x2841),x2841)+P5(f49(x2842,x2843,x2841),x2842)+E(x2841,f54(x2842,x2843)) % 0.83/0.90 [285]~P3(x2851)+~P3(x2853)+~P3(x2852)+P5(f47(x2852,x2853,x2851),x2851)+P5(f50(x2852,x2853,x2851),x2853)+E(x2851,f54(x2852,x2853)) % 0.83/0.90 [286]~P3(x2861)+~P3(x2863)+~P3(x2862)+P5(f51(x2862,x2863,x2861),x2861)+P5(f51(x2862,x2863,x2861),x2863)+E(x2861,f52(x2862,x2863)) % 0.83/0.90 [287]~P3(x2871)+~P3(x2873)+~P3(x2872)+P5(f51(x2872,x2873,x2871),x2871)+P5(f51(x2872,x2873,x2871),x2872)+E(x2871,f52(x2872,x2873)) % 0.83/0.90 [288]~P1(x2883)+~P1(x2882)+~P2(x2881,x2883)+~P2(x2881,x2882)+P6(x2881,x2882,x2883)+~P8(f13(x2882,x2883,x2881),x2881) % 0.83/0.90 [251]~P1(x2512)+~P1(x2513)+~P1(x2511)+~E(f44(x2511,x2512),a57)+~E(f44(x2511,x2513),a59)+E(f44(x2511,f18(x2511)),a60) % 0.83/0.90 [290]~P3(x2901)+~P3(x2903)+~P3(x2902)+P5(f47(x2902,x2903,x2901),x2901)+E(x2901,f54(x2902,x2903))+E(f37(f49(x2902,x2903,x2901),f50(x2902,x2903,x2901)),f47(x2902,x2903,x2901)) % 0.83/0.90 [280]~P2(x2801,x2803)+~P2(x2801,x2804)+~P6(x2802,x2804,x2803)+P8(x2801,x2802)+~P1(x2803)+~P1(x2804) % 0.83/0.90 [257]~P3(x2574)+~P3(x2573)+~P5(x2571,x2574)+~P5(x2571,x2573)+P5(x2571,x2572)+~E(x2572,f52(x2573,x2574)) % 0.83/0.90 [291]~P1(x2914)+~P1(x2913)+~P4(x2912)+~P4(x2911)+P1(f6(x2911,x2912))+P1(f7(x2911,x2912,x2913,x2914)) % 0.83/0.90 [294]~P1(x2944)+~P1(x2943)+~P4(x2942)+~P4(x2941)+P11(f7(x2941,x2942,x2943,x2944),x2944,x2942)+P1(f6(x2941,x2942)) % 0.83/0.90 [295]~P1(x2954)+~P1(x2953)+~P4(x2952)+~P4(x2951)+P11(f7(x2951,x2952,x2953,x2954),x2953,x2951)+P1(f6(x2951,x2952)) % 0.83/0.90 [297]~P1(x2974)+~P1(x2973)+~P4(x2972)+~P4(x2971)+~P5(f6(x2971,x2972),f54(x2971,x2972))+P1(f7(x2971,x2972,x2973,x2974)) % 0.83/0.90 [298]~P1(x2984)+~P1(x2983)+~P4(x2982)+~P4(x2981)+P11(f7(x2981,x2982,x2983,x2984),x2984,x2982)+~P5(f6(x2981,x2982),f54(x2981,x2982)) % 0.83/0.90 [299]~P1(x2994)+~P1(x2993)+~P4(x2992)+~P4(x2991)+P11(f7(x2991,x2992,x2993,x2994),x2993,x2991)+~P5(f6(x2991,x2992),f54(x2991,x2992)) % 0.83/0.90 [296]~P3(x2961)+~P3(x2963)+~P3(x2962)+~P5(f51(x2962,x2963,x2961),x2961)+~P5(f51(x2962,x2963,x2961),x2963)+~P5(f51(x2962,x2963,x2961),x2962)+E(x2961,f52(x2962,x2963)) % 0.83/0.90 [268]~P3(x2684)+~P3(x2683)+~P5(x2686,x2684)+~P5(x2685,x2683)+P5(x2681,x2682)+~E(x2682,f54(x2683,x2684))+~E(f37(x2685,x2686),x2681) % 0.83/0.90 [289]~P3(x2891)+~P3(x2893)+~P3(x2892)+~P5(x2895,x2893)+~P5(x2894,x2892)+~P5(f47(x2892,x2893,x2891),x2891)+E(x2891,f54(x2892,x2893))+~E(f37(x2894,x2895),f47(x2892,x2893,x2891)) % 0.83/0.90 %EqnAxiom % 0.83/0.90 [1]E(x11,x11) % 0.83/0.90 [2]E(x22,x21)+~E(x21,x22) % 0.83/0.90 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.83/0.90 [4]~E(x41,x42)+E(f37(x41,x43),f37(x42,x43)) % 0.83/0.90 [5]~E(x51,x52)+E(f37(x53,x51),f37(x53,x52)) % 0.83/0.90 [6]~E(x61,x62)+E(f54(x61,x63),f54(x62,x63)) % 0.83/0.90 [7]~E(x71,x72)+E(f54(x73,x71),f54(x73,x72)) % 0.83/0.90 [8]~E(x81,x82)+E(f48(x81,x83,x84,x85),f48(x82,x83,x84,x85)) % 0.83/0.90 [9]~E(x91,x92)+E(f48(x93,x91,x94,x95),f48(x93,x92,x94,x95)) % 0.83/0.90 [10]~E(x101,x102)+E(f48(x103,x104,x101,x105),f48(x103,x104,x102,x105)) % 0.83/0.90 [11]~E(x111,x112)+E(f48(x113,x114,x115,x111),f48(x113,x114,x115,x112)) % 0.83/0.90 [12]~E(x121,x122)+E(f35(x121,x123,x124,x125),f35(x122,x123,x124,x125)) % 0.83/0.90 [13]~E(x131,x132)+E(f35(x133,x131,x134,x135),f35(x133,x132,x134,x135)) % 0.83/0.90 [14]~E(x141,x142)+E(f35(x143,x144,x141,x145),f35(x143,x144,x142,x145)) % 0.83/0.90 [15]~E(x151,x152)+E(f35(x153,x154,x155,x151),f35(x153,x154,x155,x152)) % 0.83/0.90 [16]~E(x161,x162)+E(f44(x161,x163),f44(x162,x163)) % 0.83/0.90 [17]~E(x171,x172)+E(f44(x173,x171),f44(x173,x172)) % 0.83/0.90 [18]~E(x181,x182)+E(f46(x181),f46(x182)) % 0.83/0.90 [19]~E(x191,x192)+E(f3(x191),f3(x192)) % 0.83/0.90 [20]~E(x201,x202)+E(f47(x201,x203,x204),f47(x202,x203,x204)) % 0.83/0.90 [21]~E(x211,x212)+E(f47(x213,x211,x214),f47(x213,x212,x214)) % 0.83/0.90 [22]~E(x221,x222)+E(f47(x223,x224,x221),f47(x223,x224,x222)) % 0.83/0.90 [23]~E(x231,x232)+E(f4(x231),f4(x232)) % 0.83/0.90 [24]~E(x241,x242)+E(f18(x241),f18(x242)) % 0.83/0.90 [25]~E(x251,x252)+E(f52(x251,x253),f52(x252,x253)) % 0.83/0.90 [26]~E(x261,x262)+E(f52(x263,x261),f52(x263,x262)) % 0.83/0.90 [27]~E(x271,x272)+E(f53(x271),f53(x272)) % 0.83/0.90 [28]~E(x281,x282)+E(f45(x281),f45(x282)) % 0.83/0.90 [29]~E(x291,x292)+E(f8(x291,x293),f8(x292,x293)) % 0.83/0.90 [30]~E(x301,x302)+E(f8(x303,x301),f8(x303,x302)) % 0.83/0.90 [31]~E(x311,x312)+E(f11(x311,x313),f11(x312,x313)) % 0.83/0.90 [32]~E(x321,x322)+E(f11(x323,x321),f11(x323,x322)) % 0.83/0.90 [33]~E(x331,x332)+E(f50(x331,x333,x334),f50(x332,x333,x334)) % 0.83/0.90 [34]~E(x341,x342)+E(f50(x343,x341,x344),f50(x343,x342,x344)) % 0.83/0.90 [35]~E(x351,x352)+E(f50(x353,x354,x351),f50(x353,x354,x352)) % 0.83/0.90 [36]~E(x361,x362)+E(f21(x361),f21(x362)) % 0.83/0.90 [37]~E(x371,x372)+E(f14(x371,x373),f14(x372,x373)) % 0.83/0.90 [38]~E(x381,x382)+E(f14(x383,x381),f14(x383,x382)) % 0.83/0.90 [39]~E(x391,x392)+E(f7(x391,x393,x394,x395),f7(x392,x393,x394,x395)) % 0.83/0.90 [40]~E(x401,x402)+E(f7(x403,x401,x404,x405),f7(x403,x402,x404,x405)) % 0.83/0.90 [41]~E(x411,x412)+E(f7(x413,x414,x411,x415),f7(x413,x414,x412,x415)) % 0.83/0.90 [42]~E(x421,x422)+E(f7(x423,x424,x425,x421),f7(x423,x424,x425,x422)) % 0.83/0.90 [43]~E(x431,x432)+E(f9(x431,x433),f9(x432,x433)) % 0.83/0.90 [44]~E(x441,x442)+E(f9(x443,x441),f9(x443,x442)) % 0.83/0.90 [45]~E(x451,x452)+E(f13(x451,x453,x454),f13(x452,x453,x454)) % 0.83/0.90 [46]~E(x461,x462)+E(f13(x463,x461,x464),f13(x463,x462,x464)) % 0.83/0.90 [47]~E(x471,x472)+E(f13(x473,x474,x471),f13(x473,x474,x472)) % 0.83/0.90 [48]~E(x481,x482)+E(f24(x481,x483),f24(x482,x483)) % 0.83/0.90 [49]~E(x491,x492)+E(f24(x493,x491),f24(x493,x492)) % 0.83/0.90 [50]~E(x501,x502)+E(f29(x501),f29(x502)) % 0.83/0.90 [51]~E(x511,x512)+E(f55(x511),f55(x512)) % 0.83/0.90 [52]~E(x521,x522)+E(f6(x521,x523),f6(x522,x523)) % 0.83/0.90 [53]~E(x531,x532)+E(f6(x533,x531),f6(x533,x532)) % 0.83/0.90 [54]~E(x541,x542)+E(f20(x541),f20(x542)) % 0.83/0.90 [55]~E(x551,x552)+E(f51(x551,x553,x554),f51(x552,x553,x554)) % 0.83/0.90 [56]~E(x561,x562)+E(f51(x563,x561,x564),f51(x563,x562,x564)) % 0.83/0.90 [57]~E(x571,x572)+E(f51(x573,x574,x571),f51(x573,x574,x572)) % 0.83/0.90 [58]~E(x581,x582)+E(f17(x581),f17(x582)) % 0.83/0.90 [59]~E(x591,x592)+E(f5(x591,x593),f5(x592,x593)) % 0.83/0.90 [60]~E(x601,x602)+E(f5(x603,x601),f5(x603,x602)) % 0.83/0.90 [61]~E(x611,x612)+E(f30(x611),f30(x612)) % 0.83/0.90 [62]~E(x621,x622)+E(f10(x621,x623),f10(x622,x623)) % 0.83/0.90 [63]~E(x631,x632)+E(f10(x633,x631),f10(x633,x632)) % 0.83/0.90 [64]~E(x641,x642)+E(f19(x641),f19(x642)) % 0.83/0.90 [65]~E(x651,x652)+E(f12(x651,x653,x654),f12(x652,x653,x654)) % 0.83/0.90 [66]~E(x661,x662)+E(f12(x663,x661,x664),f12(x663,x662,x664)) % 0.83/0.90 [67]~E(x671,x672)+E(f12(x673,x674,x671),f12(x673,x674,x672)) % 0.83/0.90 [68]~E(x681,x682)+E(f49(x681,x683,x684),f49(x682,x683,x684)) % 0.83/0.90 [69]~E(x691,x692)+E(f49(x693,x691,x694),f49(x693,x692,x694)) % 0.83/0.90 [70]~E(x701,x702)+E(f49(x703,x704,x701),f49(x703,x704,x702)) % 0.83/0.90 [71]~P1(x711)+P1(x712)+~E(x711,x712) % 0.83/0.90 [72]P5(x722,x723)+~E(x721,x722)+~P5(x721,x723) % 0.83/0.90 [73]P5(x733,x732)+~E(x731,x732)+~P5(x733,x731) % 0.83/0.90 [74]~P3(x741)+P3(x742)+~E(x741,x742) % 0.83/0.90 [75]P8(x752,x753)+~E(x751,x752)+~P8(x751,x753) % 0.83/0.90 [76]P8(x763,x762)+~E(x761,x762)+~P8(x763,x761) % 0.83/0.90 [77]P2(x772,x773)+~E(x771,x772)+~P2(x771,x773) % 0.83/0.90 [78]P2(x783,x782)+~E(x781,x782)+~P2(x783,x781) % 0.83/0.90 [79]~P4(x791)+P4(x792)+~E(x791,x792) % 0.83/0.90 [80]P11(x802,x803,x804)+~E(x801,x802)+~P11(x801,x803,x804) % 0.83/0.90 [81]P11(x813,x812,x814)+~E(x811,x812)+~P11(x813,x811,x814) % 0.83/0.90 [82]P11(x823,x824,x822)+~E(x821,x822)+~P11(x823,x824,x821) % 0.83/0.90 [83]P10(x832,x833)+~E(x831,x832)+~P10(x831,x833) % 0.83/0.90 [84]P10(x843,x842)+~E(x841,x842)+~P10(x843,x841) % 0.83/0.90 [85]P6(x852,x853,x854)+~E(x851,x852)+~P6(x851,x853,x854) % 0.83/0.90 [86]P6(x863,x862,x864)+~E(x861,x862)+~P6(x863,x861,x864) % 0.83/0.90 [87]P6(x873,x874,x872)+~E(x871,x872)+~P6(x873,x874,x871) % 0.83/0.90 [88]~P7(x881)+P7(x882)+~E(x881,x882) % 0.83/0.90 [89]P9(x892,x893)+~E(x891,x892)+~P9(x891,x893) % 0.83/0.90 [90]P9(x903,x902)+~E(x901,x902)+~P9(x903,x901) % 0.83/0.90 % 0.83/0.90 %------------------------------------------- % 0.83/0.90 cnf(322,plain, % 0.83/0.90 (E(a62,a1)), % 0.83/0.90 inference(scs_inference,[],[123,125,126,127,153,110,168,178,2,216,221])). % 0.83/0.90 cnf(569,plain, % 0.83/0.90 ($false), % 0.83/0.90 inference(scs_inference,[],[322,153,2]), % 0.83/0.90 ['proof']). % 0.83/0.90 % SZS output end Proof % 0.83/0.90 % Total time :0.220000s %------------------------------------------------------------------------------