%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG125+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 : n023.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 1.19s 1.26s % Output : CNFRefutation 1.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : RNG125+1 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n023.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Jun 18 13:12:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.52/0.56 start to proof:theBenchmark % 1.19/1.24 %------------------------------------------- % 1.19/1.24 % File :CSE---1.7 % 1.19/1.24 % Problem :theBenchmark % 1.19/1.24 % Transform :cnf % 1.19/1.24 % Format :tptp:raw % 1.19/1.24 % Command :java -jar mcs_scs.jar %d %s % 1.19/1.24 % 1.19/1.24 % Result :Theorem 0.620000s % 1.19/1.24 % Output :CNFRefutation 0.620000s % 1.19/1.24 %------------------------------------------- % 1.19/1.25 %------------------------------------------------------------------------------ % 1.19/1.25 % File : RNG125+1 : TPTP v8.2.0. Released v4.0.0. % 1.19/1.25 % Domain : Ring Theory % 1.19/1.25 % Problem : Chinese remainder theorem in a ring 07_05_04, 00 expansion % 1.19/1.25 % Version : Especial. % 1.19/1.25 % English : % 1.19/1.25 % 1.19/1.25 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 1.19/1.25 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 1.19/1.25 % Source : [Pas08] % 1.19/1.25 % Names : chines_07_05_04.00 [Pas08] % 1.19/1.25 % 1.19/1.25 % Status : ContradictoryAxioms % 1.19/1.25 % Rating : 0.14 v8.1.0, 0.06 v7.5.0, 0.09 v7.4.0, 0.29 v7.3.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.04 v6.2.0, 0.08 v6.1.0, 0.17 v5.5.0, 0.22 v5.4.0, 0.25 v5.3.0, 0.26 v5.2.0, 0.10 v5.1.0, 0.24 v5.0.0, 0.33 v4.1.0, 0.43 v4.0.1, 0.78 v4.0.0 % 1.19/1.25 % Syntax : Number of formulae : 50 ( 7 unt; 9 def) % 1.19/1.25 % Number of atoms : 178 ( 38 equ) % 1.19/1.25 % Maximal formula atoms : 9 ( 3 avg) % 1.19/1.25 % Number of connectives : 143 ( 15 ~; 2 |; 65 &) % 1.19/1.25 % ( 12 <=>; 49 =>; 0 <=; 0 <~>) % 1.19/1.25 % Maximal formula depth : 13 ( 5 avg) % 1.19/1.25 % Maximal term depth : 3 ( 1 avg) % 1.19/1.25 % Number of predicates : 14 ( 11 usr; 2 prp; 0-3 aty) % 1.19/1.25 % Number of functors : 14 ( 14 usr; 7 con; 0-2 aty) % 1.19/1.25 % Number of variables : 88 ( 78 !; 10 ?) % 1.19/1.25 % SPC : FOF_CAX_RFO_SEQ % 1.19/1.25 % 1.19/1.25 % Comments : Problem generated by the SAD system [VLP07] % 1.19/1.25 %------------------------------------------------------------------------------ % 1.19/1.25 fof(mElmSort,axiom, % 1.19/1.25 ! [W0] : % 1.19/1.25 ( aElement0(W0) % 1.19/1.25 => $true ) ). % 1.19/1.25 % 1.19/1.25 fof(mSortsC,axiom, % 1.19/1.25 aElement0(sz00) ). % 1.19/1.25 % 1.19/1.25 fof(mSortsC_01,axiom, % 1.19/1.25 aElement0(sz10) ). % 1.19/1.25 % 1.19/1.25 fof(mSortsU,axiom, % 1.19/1.25 ! [W0] : % 1.19/1.25 ( aElement0(W0) % 1.19/1.25 => aElement0(smndt0(W0)) ) ). % 1.19/1.25 % 1.19/1.25 fof(mSortsB,axiom, % 1.19/1.25 ! [W0,W1] : % 1.19/1.25 ( ( aElement0(W0) % 1.19/1.25 & aElement0(W1) ) % 1.19/1.25 => aElement0(sdtpldt0(W0,W1)) ) ). % 1.19/1.25 % 1.19/1.25 fof(mSortsB_02,axiom, % 1.19/1.25 ! [W0,W1] : % 1.19/1.25 ( ( aElement0(W0) % 1.19/1.25 & aElement0(W1) ) % 1.19/1.25 => aElement0(sdtasdt0(W0,W1)) ) ). % 1.19/1.25 % 1.19/1.25 fof(mAddComm,axiom, % 1.19/1.25 ! [W0,W1] : % 1.19/1.25 ( ( aElement0(W0) % 1.19/1.25 & aElement0(W1) ) % 1.19/1.25 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 1.19/1.25 % 1.19/1.25 fof(mAddAsso,axiom, % 1.19/1.25 ! [W0,W1,W2] : % 1.19/1.25 ( ( aElement0(W0) % 1.19/1.25 & aElement0(W1) % 1.19/1.25 & aElement0(W2) ) % 1.19/1.25 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 1.19/1.25 % 1.19/1.25 fof(mAddZero,axiom, % 1.19/1.25 ! [W0] : % 1.19/1.25 ( aElement0(W0) % 1.19/1.25 => ( sdtpldt0(W0,sz00) = W0 % 1.19/1.25 & W0 = sdtpldt0(sz00,W0) ) ) ). % 1.19/1.25 % 1.19/1.25 fof(mAddInvr,axiom, % 1.19/1.25 ! [W0] : % 1.19/1.25 ( aElement0(W0) % 1.19/1.25 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 1.19/1.25 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 1.19/1.25 % 1.19/1.25 fof(mMulComm,axiom, % 1.19/1.25 ! [W0,W1] : % 1.19/1.25 ( ( aElement0(W0) % 1.19/1.25 & aElement0(W1) ) % 1.19/1.25 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 1.19/1.25 % 1.19/1.25 fof(mMulAsso,axiom, % 1.19/1.25 ! [W0,W1,W2] : % 1.19/1.25 ( ( aElement0(W0) % 1.19/1.25 & aElement0(W1) % 1.19/1.25 & aElement0(W2) ) % 1.19/1.25 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 1.19/1.25 % 1.19/1.25 fof(mMulUnit,axiom, % 1.19/1.25 ! [W0] : % 1.19/1.25 ( aElement0(W0) % 1.19/1.25 => ( sdtasdt0(W0,sz10) = W0 % 1.19/1.25 & W0 = sdtasdt0(sz10,W0) ) ) ). % 1.19/1.25 % 1.19/1.25 fof(mAMDistr,axiom, % 1.19/1.25 ! [W0,W1,W2] : % 1.19/1.25 ( ( aElement0(W0) % 1.19/1.25 & aElement0(W1) % 1.19/1.25 & aElement0(W2) ) % 1.19/1.25 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 1.19/1.25 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 1.19/1.25 % 1.19/1.25 fof(mMulMnOne,axiom, % 1.19/1.25 ! [W0] : % 1.19/1.25 ( aElement0(W0) % 1.19/1.25 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 1.19/1.25 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 1.19/1.25 % 1.19/1.25 fof(mMulZero,axiom, % 1.19/1.25 ! [W0] : % 1.19/1.25 ( aElement0(W0) % 1.19/1.25 => ( sdtasdt0(W0,sz00) = sz00 % 1.19/1.25 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 1.19/1.25 % 1.19/1.25 fof(mCancel,axiom, % 1.19/1.25 ! [W0,W1] : % 1.19/1.25 ( ( aElement0(W0) % 1.19/1.25 & aElement0(W1) ) % 1.19/1.25 => ( sdtasdt0(W0,W1) = sz00 % 1.19/1.25 => ( W0 = sz00 % 1.19/1.25 | W1 = sz00 ) ) ) ). % 1.19/1.25 % 1.19/1.25 fof(mUnNeZr,axiom, % 1.19/1.25 sz10 != sz00 ). % 1.19/1.25 % 1.19/1.25 fof(mSetSort,axiom, % 1.19/1.25 ! [W0] : % 1.19/1.25 ( aSet0(W0) % 1.19/1.25 => $true ) ). % 1.19/1.25 % 1.19/1.25 fof(mEOfElem,axiom, % 1.19/1.25 ! [W0] : % 1.19/1.25 ( aSet0(W0) % 1.19/1.25 => ! [W1] : % 1.19/1.25 ( aElementOf0(W1,W0) % 1.19/1.25 => aElement0(W1) ) ) ). % 1.19/1.25 % 1.19/1.25 fof(mSetEq,axiom, % 1.19/1.25 ! [W0,W1] : % 1.19/1.25 ( ( aSet0(W0) % 1.19/1.25 & aSet0(W1) ) % 1.19/1.25 => ( ( ! [W2] : % 1.19/1.25 ( aElementOf0(W2,W0) % 1.19/1.25 => aElementOf0(W2,W1) ) % 1.19/1.25 & ! [W2] : % 1.19/1.25 ( aElementOf0(W2,W1) % 1.19/1.25 => aElementOf0(W2,W0) ) ) % 1.19/1.25 => W0 = W1 ) ) ). % 1.19/1.25 % 1.19/1.25 fof(mDefSSum,definition, % 1.19/1.25 ! [W0,W1] : % 1.19/1.25 ( ( aSet0(W0) % 1.19/1.25 & aSet0(W1) ) % 1.19/1.25 => ! [W2] : % 1.19/1.25 ( W2 = sdtpldt1(W0,W1) % 1.19/1.25 <=> ( aSet0(W2) % 1.19/1.25 & ! [W3] : % 1.19/1.25 ( aElementOf0(W3,W2) % 1.19/1.25 <=> ? [W4,W5] : % 1.19/1.25 ( aElementOf0(W4,W0) % 1.19/1.25 & aElementOf0(W5,W1) % 1.19/1.25 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 1.19/1.25 % 1.19/1.25 fof(mDefSInt,definition, % 1.19/1.25 ! [W0,W1] : % 1.19/1.25 ( ( aSet0(W0) % 1.19/1.25 & aSet0(W1) ) % 1.19/1.25 => ! [W2] : % 1.19/1.25 ( W2 = sdtasasdt0(W0,W1) % 1.19/1.25 <=> ( aSet0(W2) % 1.19/1.25 & ! [W3] : % 1.19/1.25 ( aElementOf0(W3,W2) % 1.19/1.25 <=> ( aElementOf0(W3,W0) % 1.19/1.25 & aElementOf0(W3,W1) ) ) ) ) ) ). % 1.19/1.25 % 1.19/1.25 fof(mDefIdeal,definition, % 1.19/1.25 ! [W0] : % 1.19/1.25 ( aIdeal0(W0) % 1.19/1.25 <=> ( aSet0(W0) % 1.19/1.25 & ! [W1] : % 1.19/1.25 ( aElementOf0(W1,W0) % 1.19/1.25 => ( ! [W2] : % 1.19/1.25 ( aElementOf0(W2,W0) % 1.19/1.25 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 1.19/1.25 & ! [W2] : % 1.19/1.25 ( aElement0(W2) % 1.19/1.25 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 1.19/1.25 % 1.19/1.25 fof(mIdeSum,axiom, % 1.19/1.25 ! [W0,W1] : % 1.19/1.25 ( ( aIdeal0(W0) % 1.19/1.25 & aIdeal0(W1) ) % 1.19/1.25 => aIdeal0(sdtpldt1(W0,W1)) ) ). % 1.19/1.25 % 1.19/1.25 fof(mIdeInt,axiom, % 1.19/1.25 ! [W0,W1] : % 1.19/1.25 ( ( aIdeal0(W0) % 1.19/1.25 & aIdeal0(W1) ) % 1.19/1.25 => aIdeal0(sdtasasdt0(W0,W1)) ) ). % 1.19/1.25 % 1.19/1.25 fof(mDefMod,definition, % 1.19/1.25 ! [W0,W1,W2] : % 1.19/1.25 ( ( aElement0(W0) % 1.19/1.25 & aElement0(W1) % 1.19/1.25 & aIdeal0(W2) ) % 1.19/1.25 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 1.19/1.25 <=> aElementOf0(sdtpldt0(W0,smndt0(W1)),W2) ) ) ). % 1.19/1.25 % 1.19/1.25 fof(mChineseRemainder,axiom, % 1.19/1.25 ! [W0,W1] : % 1.19/1.25 ( ( aIdeal0(W0) % 1.19/1.25 & aIdeal0(W1) ) % 1.19/1.25 => ( ! [W2] : % 1.19/1.25 ( aElement0(W2) % 1.19/1.25 => aElementOf0(W2,sdtpldt1(W0,W1)) ) % 1.19/1.26 => ! [W2,W3] : % 1.19/1.26 ( ( aElement0(W2) % 1.19/1.26 & aElement0(W3) ) % 1.19/1.26 => ? [W4] : % 1.19/1.26 ( aElement0(W4) % 1.19/1.26 & sdteqdtlpzmzozddtrp0(W4,W2,W0) % 1.19/1.26 & sdteqdtlpzmzozddtrp0(W4,W3,W1) ) ) ) ) ). % 1.19/1.26 % 1.19/1.26 fof(mNatSort,axiom, % 1.19/1.26 ! [W0] : % 1.19/1.26 ( aNaturalNumber0(W0) % 1.19/1.26 => $true ) ). % 1.19/1.26 % 1.19/1.26 fof(mEucSort,axiom, % 1.19/1.26 ! [W0] : % 1.19/1.26 ( ( aElement0(W0) % 1.19/1.26 & W0 != sz00 ) % 1.19/1.26 => aNaturalNumber0(sbrdtbr0(W0)) ) ). % 1.19/1.26 % 1.19/1.26 fof(mNatLess,axiom, % 1.19/1.26 ! [W0,W1] : % 1.19/1.26 ( ( aNaturalNumber0(W0) % 1.19/1.26 & aNaturalNumber0(W1) ) % 1.19/1.26 => ( iLess0(W0,W1) % 1.19/1.26 => $true ) ) ). % 1.19/1.26 % 1.19/1.26 fof(mDivision,axiom, % 1.19/1.26 ! [W0,W1] : % 1.19/1.26 ( ( aElement0(W0) % 1.19/1.26 & aElement0(W1) % 1.19/1.26 & W1 != sz00 ) % 1.19/1.26 => ? [W2,W3] : % 1.19/1.26 ( aElement0(W2) % 1.19/1.26 & aElement0(W3) % 1.19/1.26 & W0 = sdtpldt0(sdtasdt0(W2,W1),W3) % 1.19/1.26 & ( W3 != sz00 % 1.19/1.26 => iLess0(sbrdtbr0(W3),sbrdtbr0(W1)) ) ) ) ). % 1.19/1.26 % 1.19/1.26 fof(mDefDiv,definition, % 1.19/1.26 ! [W0,W1] : % 1.19/1.26 ( ( aElement0(W0) % 1.19/1.26 & aElement0(W1) ) % 1.19/1.26 => ( doDivides0(W0,W1) % 1.19/1.26 <=> ? [W2] : % 1.19/1.26 ( aElement0(W2) % 1.19/1.26 & sdtasdt0(W0,W2) = W1 ) ) ) ). % 1.19/1.26 % 1.19/1.26 fof(mDefDvs,definition, % 1.19/1.26 ! [W0] : % 1.19/1.26 ( aElement0(W0) % 1.19/1.26 => ! [W1] : % 1.19/1.26 ( aDivisorOf0(W1,W0) % 1.19/1.26 <=> ( aElement0(W1) % 1.19/1.26 & doDivides0(W1,W0) ) ) ) ). % 1.19/1.26 % 1.19/1.26 fof(mDefGCD,definition, % 1.19/1.26 ! [W0,W1] : % 1.19/1.26 ( ( aElement0(W0) % 1.19/1.26 & aElement0(W1) ) % 1.19/1.26 => ! [W2] : % 1.19/1.26 ( aGcdOfAnd0(W2,W0,W1) % 1.19/1.26 <=> ( aDivisorOf0(W2,W0) % 1.19/1.26 & aDivisorOf0(W2,W1) % 1.19/1.26 & ! [W3] : % 1.19/1.26 ( ( aDivisorOf0(W3,W0) % 1.19/1.26 & aDivisorOf0(W3,W1) ) % 1.19/1.26 => doDivides0(W3,W2) ) ) ) ) ). % 1.19/1.26 % 1.19/1.26 fof(mDefRel,definition, % 1.19/1.26 ! [W0,W1] : % 1.19/1.26 ( ( aElement0(W0) % 1.19/1.26 & aElement0(W1) ) % 1.19/1.26 => ( misRelativelyPrime0(W0,W1) % 1.19/1.26 <=> aGcdOfAnd0(sz10,W0,W1) ) ) ). % 1.19/1.26 % 1.19/1.26 fof(mDefPrIdeal,definition, % 1.19/1.26 ! [W0] : % 1.19/1.26 ( aElement0(W0) % 1.19/1.26 => ! [W1] : % 1.19/1.26 ( W1 = slsdtgt0(W0) % 1.19/1.26 <=> ( aSet0(W1) % 1.19/1.26 & ! [W2] : % 1.19/1.26 ( aElementOf0(W2,W1) % 1.19/1.26 <=> ? [W3] : % 1.19/1.26 ( aElement0(W3) % 1.19/1.26 & sdtasdt0(W0,W3) = W2 ) ) ) ) ) ). % 1.19/1.26 % 1.19/1.26 fof(mPrIdeal,axiom, % 1.19/1.26 ! [W0] : % 1.19/1.26 ( aElement0(W0) % 1.19/1.26 => aIdeal0(slsdtgt0(W0)) ) ). % 1.19/1.26 % 1.19/1.26 fof(m__2091,hypothesis, % 1.19/1.26 ( aElement0(xa) % 1.19/1.26 & aElement0(xb) ) ). % 1.19/1.26 % 1.19/1.26 fof(m__2110,hypothesis, % 1.19/1.26 ( xa != sz00 % 1.19/1.26 | xb != sz00 ) ). % 1.19/1.26 % 1.19/1.26 fof(m__2129,hypothesis, % 1.19/1.26 aGcdOfAnd0(xc,xa,xb) ). % 1.19/1.26 % 1.19/1.26 fof(m__2174,hypothesis, % 1.19/1.26 ( aIdeal0(xI) % 1.19/1.26 & xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ) ). % 1.19/1.26 % 1.19/1.26 fof(m__2203,hypothesis, % 1.19/1.26 ( aElementOf0(sz00,slsdtgt0(xa)) % 1.19/1.26 & aElementOf0(xa,slsdtgt0(xa)) % 1.19/1.26 & aElementOf0(sz00,slsdtgt0(xb)) % 1.19/1.26 & aElementOf0(xb,slsdtgt0(xb)) ) ). % 1.19/1.26 % 1.19/1.26 fof(m__2228,hypothesis, % 1.19/1.26 ? [W0] : % 1.19/1.26 ( aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) % 1.19/1.26 & W0 != sz00 ) ). % 1.19/1.26 % 1.19/1.26 fof(m__2273,hypothesis, % 1.19/1.26 ( aElementOf0(xu,xI) % 1.19/1.26 & xu != sz00 % 1.19/1.26 & ! [W0] : % 1.19/1.26 ( ( aElementOf0(W0,xI) % 1.19/1.26 & W0 != sz00 ) % 1.19/1.26 => ~ iLess0(sbrdtbr0(W0),sbrdtbr0(xu)) ) ) ). % 1.19/1.26 % 1.19/1.26 fof(m__2383,hypothesis, % 1.19/1.26 ~ ( aDivisorOf0(xu,xa) % 1.19/1.26 & aDivisorOf0(xu,xb) ) ). % 1.19/1.26 % 1.19/1.26 fof(m__2416,hypothesis, % 1.19/1.26 ? [W0,W1] : % 1.19/1.26 ( aElement0(W0) % 1.19/1.26 & aElement0(W1) % 1.19/1.26 & xu = sdtpldt0(sdtasdt0(xa,W0),sdtasdt0(xb,W1)) ) ). % 1.19/1.26 % 1.19/1.26 fof(m__2479,hypothesis, % 1.19/1.26 ~ ~ doDivides0(xu,xa) ). % 1.19/1.26 % 1.19/1.26 fof(m__2612,hypothesis, % 1.19/1.26 ~ ~ doDivides0(xu,xb) ). % 1.19/1.26 % 1.19/1.26 fof(m__,conjecture, % 1.19/1.26 $false ). % 1.19/1.26 % 1.19/1.26 %------------------------------------------------------------------------------ % 1.19/1.26 %------------------------------------------- % 1.19/1.26 % Proof found % 1.19/1.26 % SZS status Theorem for theBenchmark % 1.19/1.26 % SZS output start Proof % 1.19/1.26 %ClaNum:193(EqnAxiom:83) % 1.19/1.26 %VarNum:704(SingletonVarNum:214) % 1.19/1.26 %MaxLitNum:8 % 1.19/1.26 %MaxfuncDepth:2 % 1.19/1.26 %SharedTerms:43 % 1.19/1.26 [84]P1(a1) % 1.19/1.26 [85]P1(a32) % 1.19/1.26 [86]P1(a33) % 1.19/1.26 [87]P1(a35) % 1.19/1.26 [88]P1(a2) % 1.19/1.26 [89]P1(a16) % 1.19/1.26 [90]P3(a34) % 1.19/1.26 [91]P4(a36,a34) % 1.19/1.26 [92]P6(a36,a33) % 1.19/1.26 [93]P6(a36,a35) % 1.19/1.26 [99]P5(a37,a33,a35) % 1.19/1.26 [102]~E(a1,a32) % 1.19/1.26 [103]~E(a1,a36) % 1.19/1.26 [104]~E(a3,a1) % 1.19/1.26 [94]P4(a1,f17(a33)) % 1.19/1.26 [95]P4(a1,f17(a35)) % 1.19/1.26 [96]P4(a33,f17(a33)) % 1.19/1.26 [97]P4(a35,f17(a35)) % 1.19/1.26 [98]E(f18(f17(a33),f17(a35)),a34) % 1.19/1.26 [100]P4(a3,f18(f17(a33),f17(a35))) % 1.19/1.26 [101]E(f30(f19(a33,a2),f19(a35,a16)),a36) % 1.19/1.26 [105]~E(a1,a33)+~E(a1,a35) % 1.19/1.26 [124]~P2(a36,a33)+~P2(a36,a35) % 1.19/1.26 [106]~P3(x1061)+P7(x1061) % 1.19/1.26 [107]~P1(x1071)+P1(f31(x1071)) % 1.19/1.26 [108]~P1(x1081)+P3(f17(x1081)) % 1.19/1.26 [110]~P1(x1101)+E(f19(a1,x1101),a1) % 1.19/1.26 [111]~P1(x1111)+E(f19(x1111,a1),a1) % 1.19/1.26 [113]~P1(x1131)+E(f30(a1,x1131),x1131) % 1.19/1.26 [114]~P1(x1141)+E(f19(a32,x1141),x1141) % 1.19/1.26 [115]~P1(x1151)+E(f30(x1151,a1),x1151) % 1.19/1.26 [116]~P1(x1161)+E(f19(x1161,a32),x1161) % 1.19/1.26 [117]~P1(x1171)+E(f30(f31(x1171),x1171),a1) % 1.19/1.26 [118]~P1(x1181)+E(f30(x1181,f31(x1181)),a1) % 1.19/1.26 [119]~P1(x1191)+E(f19(x1191,f31(a32)),f31(x1191)) % 1.19/1.26 [120]~P1(x1201)+E(f19(f31(a32),x1201),f31(x1201)) % 1.19/1.26 [109]~P1(x1091)+E(x1091,a1)+P8(f20(x1091)) % 1.19/1.26 [121]~P7(x1211)+P3(x1211)+P4(f21(x1211),x1211) % 1.19/1.26 [139]~P4(x1391,a34)+E(x1391,a1)+~P9(f20(x1391),f20(a36)) % 1.19/1.26 [122]~P4(x1221,x1222)+P1(x1221)+~P7(x1222) % 1.19/1.26 [123]~P2(x1231,x1232)+P1(x1231)+~P1(x1232) % 1.19/1.26 [131]~P1(x1312)+~P2(x1311,x1312)+P6(x1311,x1312) % 1.19/1.26 [112]~P1(x1122)+P7(x1121)+~E(x1121,f17(x1122)) % 1.19/1.26 [126]~P1(x1262)+~P1(x1261)+E(f30(x1261,x1262),f30(x1262,x1261)) % 1.19/1.26 [127]~P1(x1272)+~P1(x1271)+E(f19(x1271,x1272),f19(x1272,x1271)) % 1.19/1.26 [132]~P1(x1322)+~P1(x1321)+P1(f30(x1321,x1322)) % 1.19/1.26 [133]~P1(x1332)+~P1(x1331)+P1(f19(x1331,x1332)) % 1.19/1.26 [134]~P3(x1342)+~P3(x1341)+P3(f18(x1341,x1342)) % 1.19/1.26 [135]~P3(x1352)+~P3(x1351)+P3(f29(x1351,x1352)) % 1.19/1.26 [130]~P7(x1301)+P3(x1301)+P4(f5(x1301),x1301)+P1(f4(x1301)) % 1.19/1.26 [162]~P7(x1621)+P3(x1621)+P1(f4(x1621))+~P4(f30(f21(x1621),f5(x1621)),x1621) % 1.19/1.26 [165]~P7(x1651)+P3(x1651)+P4(f5(x1651),x1651)+~P4(f19(f4(x1651),f21(x1651)),x1651) % 1.19/1.26 [174]~P7(x1741)+P3(x1741)+~P4(f30(f21(x1741),f5(x1741)),x1741)+~P4(f19(f4(x1741),f21(x1741)),x1741) % 1.19/1.26 [138]~P1(x1382)+~P1(x1381)+~P6(x1381,x1382)+P2(x1381,x1382) % 1.19/1.26 [147]~P1(x1472)+~P1(x1471)+~P10(x1471,x1472)+P5(a32,x1471,x1472) % 1.19/1.26 [155]~P1(x1552)+~P1(x1551)+P10(x1551,x1552)+~P5(a32,x1551,x1552) % 1.19/1.26 [136]~P1(x1361)+~P1(x1362)+E(x1361,a1)+P1(f6(x1362,x1361)) % 1.19/1.26 [137]~P1(x1371)+~P1(x1372)+E(x1371,a1)+P1(f9(x1372,x1371)) % 1.19/1.26 [142]~P1(x1422)+~P1(x1421)+~P6(x1421,x1422)+P1(f10(x1421,x1422)) % 1.19/1.26 [146]~P1(x1462)+~P1(x1461)+~P6(x1461,x1462)+E(f19(x1461,f10(x1461,x1462)),x1462) % 1.19/1.26 [167]~P1(x1671)+~P1(x1672)+E(x1671,a1)+E(f30(f19(f6(x1672,x1671),x1671),f9(x1672,x1671)),x1672) % 1.19/1.26 [157]~P1(x1572)+~P5(x1571,x1573,x1572)+P2(x1571,x1572)+~P1(x1573) % 1.19/1.26 [158]~P1(x1582)+~P5(x1581,x1582,x1583)+P2(x1581,x1582)+~P1(x1583) % 1.19/1.26 [128]~P7(x1283)+~P7(x1282)+P7(x1281)+~E(x1281,f18(x1282,x1283)) % 1.19/1.26 [129]~P7(x1293)+~P7(x1292)+P7(x1291)+~E(x1291,f29(x1292,x1293)) % 1.19/1.26 [145]~P1(x1451)+~P3(x1453)+~P4(x1452,x1453)+P4(f19(x1451,x1452),x1453) % 1.19/1.26 [149]~P3(x1493)+~P4(x1491,x1493)+~P4(x1492,x1493)+P4(f30(x1491,x1492),x1493) % 1.19/1.26 [169]~P1(x1691)+~P4(x1693,x1692)+~E(x1692,f17(x1691))+P1(f13(x1691,x1692,x1693)) % 1.19/1.26 [152]~P1(x1523)+~P1(x1522)+~P1(x1521)+E(f30(f30(x1521,x1522),x1523),f30(x1521,f30(x1522,x1523))) % 1.19/1.26 [153]~P1(x1533)+~P1(x1532)+~P1(x1531)+E(f19(f19(x1531,x1532),x1533),f19(x1531,f19(x1532,x1533))) % 1.19/1.26 [163]~P1(x1633)+~P1(x1632)+~P1(x1631)+E(f30(f19(x1631,x1632),f19(x1631,x1633)),f19(x1631,f30(x1632,x1633))) % 1.19/1.26 [164]~P1(x1642)+~P1(x1643)+~P1(x1641)+E(f30(f19(x1641,x1642),f19(x1643,x1642)),f19(f30(x1641,x1643),x1642)) % 1.19/1.26 [171]~P1(x1711)+~P4(x1713,x1712)+~E(x1712,f17(x1711))+E(f19(x1711,f13(x1711,x1712,x1713)),x1713) % 1.19/1.26 [125]~P1(x1251)+~P1(x1252)+E(x1251,a1)+E(x1252,a1)+~E(f19(x1252,x1251),a1) % 1.19/1.26 [148]~P1(x1482)+~P7(x1481)+P4(f12(x1482,x1481),x1481)+E(x1481,f17(x1482))+P1(f11(x1482,x1481)) % 1.19/1.26 [150]~P7(x1502)+~P7(x1501)+E(x1501,x1502)+P4(f15(x1501,x1502),x1501)+P4(f22(x1501,x1502),x1502) % 1.19/1.26 [159]~P7(x1592)+~P7(x1591)+E(x1591,x1592)+P4(f15(x1591,x1592),x1591)+~P4(f22(x1591,x1592),x1591) % 1.19/1.26 [160]~P7(x1602)+~P7(x1601)+E(x1601,x1602)+P4(f22(x1601,x1602),x1602)+~P4(f15(x1601,x1602),x1602) % 1.19/1.26 [168]~P7(x1682)+~P7(x1681)+E(x1681,x1682)+~P4(f15(x1681,x1682),x1682)+~P4(f22(x1681,x1682),x1681) % 1.19/1.26 [154]~P1(x1541)+~P1(x1542)+E(x1541,a1)+P9(f20(f9(x1542,x1541)),f20(x1541))+E(f9(x1542,x1541),a1) % 1.19/1.26 [156]~P1(x1562)+~P7(x1561)+P4(f12(x1562,x1561),x1561)+E(x1561,f17(x1562))+E(f19(x1562,f11(x1562,x1561)),f12(x1562,x1561)) % 1.19/1.26 [140]~P1(x1402)+~P1(x1401)+~P1(x1403)+P6(x1401,x1402)+~E(f19(x1401,x1403),x1402) % 1.19/1.26 [170]~P1(x1702)+~P1(x1701)+~P3(x1703)+P11(x1701,x1702,x1703)+~P4(f30(x1701,f31(x1702)),x1703) % 1.19/1.26 [172]~P1(x1722)+~P1(x1721)+~P3(x1723)+~P11(x1721,x1722,x1723)+P4(f30(x1721,f31(x1722)),x1723) % 1.19/1.26 [141]~P1(x1413)+~P1(x1414)+P4(x1411,x1412)+~E(f19(x1413,x1414),x1411)+~E(x1412,f17(x1413)) % 1.19/1.26 [143]~P7(x1434)+~P7(x1432)+~P4(x1431,x1433)+P4(x1431,x1432)+~E(x1433,f29(x1434,x1432)) % 1.19/1.26 [144]~P7(x1444)+~P7(x1442)+~P4(x1441,x1443)+P4(x1441,x1442)+~E(x1443,f29(x1442,x1444)) % 1.19/1.26 [185]~P7(x1852)+~P7(x1851)+~P4(x1854,x1853)+~E(x1853,f18(x1851,x1852))+P4(f24(x1851,x1852,x1853,x1854),x1851) % 1.19/1.26 [186]~P7(x1862)+~P7(x1861)+~P4(x1864,x1863)+~E(x1863,f18(x1861,x1862))+P4(f25(x1861,x1862,x1863,x1864),x1862) % 1.19/1.26 [193]~P7(x1932)+~P7(x1931)+~P4(x1934,x1933)+~E(x1933,f18(x1931,x1932))+E(f30(f24(x1931,x1932,x1933,x1934),f25(x1931,x1932,x1933,x1934)),x1934) % 1.19/1.26 [166]~P1(x1663)+~P1(x1662)+~P7(x1661)+~P4(f12(x1662,x1661),x1661)+~E(f12(x1662,x1661),f19(x1662,x1663))+E(x1661,f17(x1662)) % 1.19/1.26 [175]~P1(x1753)+~P1(x1752)+~P2(x1751,x1753)+~P2(x1751,x1752)+P5(x1751,x1752,x1753)+P2(f14(x1752,x1753,x1751),x1753) % 1.19/1.26 [176]~P1(x1763)+~P1(x1762)+~P2(x1761,x1763)+~P2(x1761,x1762)+P5(x1761,x1762,x1763)+P2(f14(x1762,x1763,x1761),x1762) % 1.19/1.26 [177]~P7(x1771)+~P7(x1773)+~P7(x1772)+P4(f23(x1772,x1773,x1771),x1771)+P4(f26(x1772,x1773,x1771),x1772)+E(x1771,f18(x1772,x1773)) % 1.19/1.26 [178]~P7(x1781)+~P7(x1783)+~P7(x1782)+P4(f23(x1782,x1783,x1781),x1781)+P4(f27(x1782,x1783,x1781),x1783)+E(x1781,f18(x1782,x1783)) % 1.19/1.26 [179]~P7(x1791)+~P7(x1793)+~P7(x1792)+P4(f28(x1792,x1793,x1791),x1791)+P4(f28(x1792,x1793,x1791),x1793)+E(x1791,f29(x1792,x1793)) % 1.19/1.26 [180]~P7(x1801)+~P7(x1803)+~P7(x1802)+P4(f28(x1802,x1803,x1801),x1801)+P4(f28(x1802,x1803,x1801),x1802)+E(x1801,f29(x1802,x1803)) % 1.19/1.26 [181]~P1(x1813)+~P1(x1812)+~P2(x1811,x1813)+~P2(x1811,x1812)+P5(x1811,x1812,x1813)+~P6(f14(x1812,x1813,x1811),x1811) % 1.19/1.26 [183]~P7(x1831)+~P7(x1833)+~P7(x1832)+P4(f23(x1832,x1833,x1831),x1831)+E(x1831,f18(x1832,x1833))+E(f30(f26(x1832,x1833,x1831),f27(x1832,x1833,x1831)),f23(x1832,x1833,x1831)) % 1.19/1.26 [173]~P2(x1731,x1733)+~P2(x1731,x1734)+~P5(x1732,x1734,x1733)+P6(x1731,x1732)+~P1(x1733)+~P1(x1734) % 1.19/1.26 [151]~P7(x1514)+~P7(x1513)+~P4(x1511,x1514)+~P4(x1511,x1513)+P4(x1511,x1512)+~E(x1512,f29(x1513,x1514)) % 1.19/1.26 [184]~P1(x1844)+~P1(x1843)+~P3(x1842)+~P3(x1841)+P1(f7(x1841,x1842))+P1(f8(x1841,x1842,x1843,x1844)) % 1.19/1.26 [187]~P1(x1874)+~P1(x1873)+~P3(x1872)+~P3(x1871)+P11(f8(x1871,x1872,x1873,x1874),x1874,x1872)+P1(f7(x1871,x1872)) % 1.19/1.26 [188]~P1(x1884)+~P1(x1883)+~P3(x1882)+~P3(x1881)+P11(f8(x1881,x1882,x1883,x1884),x1883,x1881)+P1(f7(x1881,x1882)) % 1.19/1.26 [190]~P1(x1904)+~P1(x1903)+~P3(x1902)+~P3(x1901)+~P4(f7(x1901,x1902),f18(x1901,x1902))+P1(f8(x1901,x1902,x1903,x1904)) % 1.19/1.26 [191]~P1(x1914)+~P1(x1913)+~P3(x1912)+~P3(x1911)+P11(f8(x1911,x1912,x1913,x1914),x1914,x1912)+~P4(f7(x1911,x1912),f18(x1911,x1912)) % 1.19/1.26 [192]~P1(x1924)+~P1(x1923)+~P3(x1922)+~P3(x1921)+P11(f8(x1921,x1922,x1923,x1924),x1923,x1921)+~P4(f7(x1921,x1922),f18(x1921,x1922)) % 1.19/1.26 [189]~P7(x1891)+~P7(x1893)+~P7(x1892)+~P4(f28(x1892,x1893,x1891),x1891)+~P4(f28(x1892,x1893,x1891),x1893)+~P4(f28(x1892,x1893,x1891),x1892)+E(x1891,f29(x1892,x1893)) % 1.19/1.26 [161]~P7(x1614)+~P7(x1613)+~P4(x1616,x1614)+~P4(x1615,x1613)+P4(x1611,x1612)+~E(x1612,f18(x1613,x1614))+~E(f30(x1615,x1616),x1611) % 1.19/1.26 [182]~P7(x1821)+~P7(x1823)+~P7(x1822)+~P4(x1825,x1823)+~P4(x1824,x1822)+~P4(f23(x1822,x1823,x1821),x1821)+E(x1821,f18(x1822,x1823))+~E(f30(x1824,x1825),f23(x1822,x1823,x1821)) % 1.19/1.26 %EqnAxiom % 1.19/1.26 [1]E(x11,x11) % 1.19/1.26 [2]E(x22,x21)+~E(x21,x22) % 1.19/1.26 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.19/1.26 [4]~E(x41,x42)+E(f17(x41),f17(x42)) % 1.19/1.26 [5]~E(x51,x52)+E(f18(x51,x53),f18(x52,x53)) % 1.19/1.26 [6]~E(x61,x62)+E(f18(x63,x61),f18(x63,x62)) % 1.19/1.26 [7]~E(x71,x72)+E(f30(x71,x73),f30(x72,x73)) % 1.19/1.26 [8]~E(x81,x82)+E(f30(x83,x81),f30(x83,x82)) % 1.19/1.26 [9]~E(x91,x92)+E(f25(x91,x93,x94,x95),f25(x92,x93,x94,x95)) % 1.19/1.26 [10]~E(x101,x102)+E(f25(x103,x101,x104,x105),f25(x103,x102,x104,x105)) % 1.19/1.26 [11]~E(x111,x112)+E(f25(x113,x114,x111,x115),f25(x113,x114,x112,x115)) % 1.19/1.26 [12]~E(x121,x122)+E(f25(x123,x124,x125,x121),f25(x123,x124,x125,x122)) % 1.19/1.26 [13]~E(x131,x132)+E(f24(x131,x133,x134,x135),f24(x132,x133,x134,x135)) % 1.19/1.26 [14]~E(x141,x142)+E(f24(x143,x141,x144,x145),f24(x143,x142,x144,x145)) % 1.19/1.26 [15]~E(x151,x152)+E(f24(x153,x154,x151,x155),f24(x153,x154,x152,x155)) % 1.19/1.26 [16]~E(x161,x162)+E(f24(x163,x164,x165,x161),f24(x163,x164,x165,x162)) % 1.19/1.26 [17]~E(x171,x172)+E(f28(x171,x173,x174),f28(x172,x173,x174)) % 1.19/1.26 [18]~E(x181,x182)+E(f28(x183,x181,x184),f28(x183,x182,x184)) % 1.19/1.26 [19]~E(x191,x192)+E(f28(x193,x194,x191),f28(x193,x194,x192)) % 1.19/1.26 [20]~E(x201,x202)+E(f29(x201,x203),f29(x202,x203)) % 1.19/1.26 [21]~E(x211,x212)+E(f29(x213,x211),f29(x213,x212)) % 1.19/1.26 [22]~E(x221,x222)+E(f7(x221,x223),f7(x222,x223)) % 1.26/1.26 [23]~E(x231,x232)+E(f7(x233,x231),f7(x233,x232)) % 1.26/1.26 [24]~E(x241,x242)+E(f8(x241,x243,x244,x245),f8(x242,x243,x244,x245)) % 1.26/1.26 [25]~E(x251,x252)+E(f8(x253,x251,x254,x255),f8(x253,x252,x254,x255)) % 1.26/1.26 [26]~E(x261,x262)+E(f8(x263,x264,x261,x265),f8(x263,x264,x262,x265)) % 1.26/1.26 [27]~E(x271,x272)+E(f8(x273,x274,x275,x271),f8(x273,x274,x275,x272)) % 1.26/1.26 [28]~E(x281,x282)+E(f19(x281,x283),f19(x282,x283)) % 1.26/1.26 [29]~E(x291,x292)+E(f19(x293,x291),f19(x293,x292)) % 1.26/1.26 [30]~E(x301,x302)+E(f4(x301),f4(x302)) % 1.26/1.26 [31]~E(x311,x312)+E(f5(x311),f5(x312)) % 1.26/1.26 [32]~E(x321,x322)+E(f27(x321,x323,x324),f27(x322,x323,x324)) % 1.26/1.26 [33]~E(x331,x332)+E(f27(x333,x331,x334),f27(x333,x332,x334)) % 1.26/1.26 [34]~E(x341,x342)+E(f27(x343,x344,x341),f27(x343,x344,x342)) % 1.26/1.26 [35]~E(x351,x352)+E(f31(x351),f31(x352)) % 1.26/1.26 [36]~E(x361,x362)+E(f14(x361,x363,x364),f14(x362,x363,x364)) % 1.26/1.26 [37]~E(x371,x372)+E(f14(x373,x371,x374),f14(x373,x372,x374)) % 1.26/1.26 [38]~E(x381,x382)+E(f14(x383,x384,x381),f14(x383,x384,x382)) % 1.26/1.26 [39]~E(x391,x392)+E(f20(x391),f20(x392)) % 1.26/1.26 [40]~E(x401,x402)+E(f21(x401),f21(x402)) % 1.26/1.26 [41]~E(x411,x412)+E(f23(x411,x413,x414),f23(x412,x413,x414)) % 1.26/1.26 [42]~E(x421,x422)+E(f23(x423,x421,x424),f23(x423,x422,x424)) % 1.26/1.26 [43]~E(x431,x432)+E(f23(x433,x434,x431),f23(x433,x434,x432)) % 1.26/1.26 [44]~E(x441,x442)+E(f9(x441,x443),f9(x442,x443)) % 1.26/1.26 [45]~E(x451,x452)+E(f9(x453,x451),f9(x453,x452)) % 1.26/1.26 [46]~E(x461,x462)+E(f26(x461,x463,x464),f26(x462,x463,x464)) % 1.26/1.26 [47]~E(x471,x472)+E(f26(x473,x471,x474),f26(x473,x472,x474)) % 1.26/1.26 [48]~E(x481,x482)+E(f26(x483,x484,x481),f26(x483,x484,x482)) % 1.26/1.26 [49]~E(x491,x492)+E(f15(x491,x493),f15(x492,x493)) % 1.26/1.26 [50]~E(x501,x502)+E(f15(x503,x501),f15(x503,x502)) % 1.26/1.26 [51]~E(x511,x512)+E(f12(x511,x513),f12(x512,x513)) % 1.26/1.26 [52]~E(x521,x522)+E(f12(x523,x521),f12(x523,x522)) % 1.26/1.26 [53]~E(x531,x532)+E(f11(x531,x533),f11(x532,x533)) % 1.26/1.26 [54]~E(x541,x542)+E(f11(x543,x541),f11(x543,x542)) % 1.26/1.26 [55]~E(x551,x552)+E(f22(x551,x553),f22(x552,x553)) % 1.26/1.26 [56]~E(x561,x562)+E(f22(x563,x561),f22(x563,x562)) % 1.26/1.26 [57]~E(x571,x572)+E(f10(x571,x573),f10(x572,x573)) % 1.26/1.26 [58]~E(x581,x582)+E(f10(x583,x581),f10(x583,x582)) % 1.26/1.26 [59]~E(x591,x592)+E(f13(x591,x593,x594),f13(x592,x593,x594)) % 1.26/1.26 [60]~E(x601,x602)+E(f13(x603,x601,x604),f13(x603,x602,x604)) % 1.26/1.26 [61]~E(x611,x612)+E(f13(x613,x614,x611),f13(x613,x614,x612)) % 1.26/1.27 [62]~E(x621,x622)+E(f6(x621,x623),f6(x622,x623)) % 1.26/1.27 [63]~E(x631,x632)+E(f6(x633,x631),f6(x633,x632)) % 1.26/1.27 [64]~P1(x641)+P1(x642)+~E(x641,x642) % 1.26/1.27 [65]P4(x652,x653)+~E(x651,x652)+~P4(x651,x653) % 1.26/1.27 [66]P4(x663,x662)+~E(x661,x662)+~P4(x663,x661) % 1.26/1.27 [67]~P7(x671)+P7(x672)+~E(x671,x672) % 1.26/1.27 [68]P9(x682,x683)+~E(x681,x682)+~P9(x681,x683) % 1.26/1.27 [69]P9(x693,x692)+~E(x691,x692)+~P9(x693,x691) % 1.26/1.27 [70]~P3(x701)+P3(x702)+~E(x701,x702) % 1.26/1.27 [71]P2(x712,x713)+~E(x711,x712)+~P2(x711,x713) % 1.26/1.27 [72]P2(x723,x722)+~E(x721,x722)+~P2(x723,x721) % 1.26/1.27 [73]P11(x732,x733,x734)+~E(x731,x732)+~P11(x731,x733,x734) % 1.26/1.27 [74]P11(x743,x742,x744)+~E(x741,x742)+~P11(x743,x741,x744) % 1.26/1.27 [75]P11(x753,x754,x752)+~E(x751,x752)+~P11(x753,x754,x751) % 1.26/1.27 [76]P10(x762,x763)+~E(x761,x762)+~P10(x761,x763) % 1.26/1.27 [77]P10(x773,x772)+~E(x771,x772)+~P10(x773,x771) % 1.26/1.27 [78]P6(x782,x783)+~E(x781,x782)+~P6(x781,x783) % 1.26/1.27 [79]P6(x793,x792)+~E(x791,x792)+~P6(x793,x791) % 1.26/1.27 [80]P5(x802,x803,x804)+~E(x801,x802)+~P5(x801,x803,x804) % 1.26/1.27 [81]P5(x813,x812,x814)+~E(x811,x812)+~P5(x813,x811,x814) % 1.26/1.27 [82]P5(x823,x824,x822)+~E(x821,x822)+~P5(x823,x824,x821) % 1.26/1.27 [83]~P8(x831)+P8(x832)+~E(x831,x832) % 1.26/1.27 % 1.26/1.27 %------------------------------------------- % 1.26/1.27 cnf(206,plain, % 1.26/1.27 (E(a34,f18(f17(a33),f17(a35)))), % 1.26/1.27 inference(scs_inference,[],[98,2])). % 1.26/1.27 cnf(208,plain, % 1.26/1.27 (P4(a36,f18(f17(a33),f17(a35)))), % 1.26/1.27 inference(scs_inference,[],[91,103,98,101,2,3,66])). % 1.26/1.27 cnf(216,plain, % 1.26/1.27 (E(a36,f30(f19(a33,a2),f19(a35,a16)))), % 1.26/1.27 inference(scs_inference,[],[101,2])). % 1.26/1.27 cnf(225,plain, % 1.26/1.27 (~P7(a34)+P7(f18(f17(a33),f17(a35)))), % 1.26/1.27 inference(scs_inference,[],[206,208,93,99,100,101,98,2,65,78,66,79,80,81,82,83,67])). % 1.26/1.27 cnf(263,plain, % 1.26/1.27 (~P7(f18(f17(a33),f17(a35)))+P7(a34)), % 1.26/1.27 inference(scs_inference,[],[216,98,96,66,64,67])). % 1.26/1.27 cnf(300,plain, % 1.26/1.27 (P7(f18(f17(a33),f17(a35)))), % 1.26/1.27 inference(scs_inference,[],[90,106,225])). % 1.26/1.27 cnf(301,plain, % 1.26/1.27 (P7(a34)), % 1.26/1.27 inference(scs_inference,[],[300,263])). % 1.26/1.27 cnf(352,plain, % 1.26/1.27 (~P1(a36)+~P2(a36,a35)), % 1.26/1.27 inference(scs_inference,[],[92,86,138,124])). % 1.26/1.27 cnf(356,plain, % 1.26/1.27 (P2(a36,a35)+~P1(a36)), % 1.26/1.27 inference(scs_inference,[],[93,87,138])). % 1.26/1.27 cnf(452,plain, % 1.26/1.27 (~P2(a36,a35)), % 1.26/1.27 inference(scs_inference,[],[301,91,352,122])). % 1.26/1.27 cnf(453,plain, % 1.26/1.27 (~P1(a36)), % 1.26/1.27 inference(scs_inference,[],[452,356])). % 1.26/1.27 cnf(463,plain, % 1.26/1.27 ($false), % 1.26/1.27 inference(scs_inference,[],[84,91,301,453,123,122]), % 1.26/1.27 ['proof']). % 1.26/1.27 % SZS output end Proof % 1.26/1.27 % Total time :0.620000s %------------------------------------------------------------------------------