%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM491+3 : 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 : n019.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 12:24:33 EDT 2024 % Result : Theorem 2.20s 2.29s % Output : CNFRefutation 2.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM491+3 : 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.34 % Computer : n019.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 : Sun Jun 23 00:54:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 2.16/2.27 %------------------------------------------- % 2.16/2.27 % File :CSE---1.7 % 2.16/2.27 % Problem :theBenchmark % 2.16/2.27 % Transform :cnf % 2.16/2.27 % Format :tptp:raw % 2.16/2.27 % Command :java -jar mcs_scs.jar %d %s % 2.16/2.27 % 2.16/2.27 % Result :Theorem 1.110000s % 2.16/2.27 % Output :CNFRefutation 1.110000s % 2.16/2.27 %------------------------------------------- % 2.16/2.27 %------------------------------------------------------------------------------ % 2.16/2.27 % File : NUM491+3 : TPTP v8.2.0. Released v4.0.0. % 2.16/2.27 % Domain : Number Theory % 2.16/2.27 % Problem : Square root of a prime is irrational 14_01_03_04, 02 expansion % 2.16/2.27 % Version : Especial. % 2.16/2.27 % English : % 2.16/2.27 % 2.16/2.27 % Refs : [LPV06] Lyaletski et al. (2006), SAD as a Mathematical Assista % 2.16/2.27 % : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 2.16/2.27 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 2.16/2.27 % Source : [Pas08] % 2.16/2.27 % Names : primes_14_01_03_04.02 [Pas08] % 2.16/2.27 % 2.16/2.27 % Status : Theorem % 2.16/2.27 % Rating : 0.11 v8.2.0, 0.08 v8.1.0, 0.06 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.1.0, 0.07 v6.0.0, 0.04 v5.5.0, 0.11 v5.4.0, 0.14 v5.3.0, 0.19 v5.2.0, 0.15 v5.1.0, 0.29 v5.0.0, 0.33 v4.1.0, 0.35 v4.0.1, 0.61 v4.0.0 % 2.16/2.27 % Syntax : Number of formulae : 48 ( 3 unt; 5 def) % 2.16/2.27 % Number of atoms : 237 ( 80 equ) % 2.16/2.27 % Maximal formula atoms : 22 ( 4 avg) % 2.16/2.27 % Number of connectives : 214 ( 25 ~; 14 |; 106 &) % 2.16/2.27 % ( 5 <=>; 64 =>; 0 <=; 0 <~>) % 2.16/2.27 % Maximal formula depth : 16 ( 6 avg) % 2.16/2.27 % Maximal term depth : 3 ( 1 avg) % 2.16/2.27 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 2.16/2.27 % Number of functors : 10 ( 10 usr; 6 con; 0-2 aty) % 2.16/2.27 % Number of variables : 96 ( 84 !; 12 ?) % 2.16/2.27 % SPC : FOF_THM_RFO_SEQ % 2.16/2.27 % 2.16/2.27 % Comments : Problem generated by the SAD system [VLP07] % 2.16/2.27 %------------------------------------------------------------------------------ % 2.16/2.27 fof(mNatSort,axiom, % 2.16/2.27 ! [W0] : % 2.16/2.27 ( aNaturalNumber0(W0) % 2.16/2.27 => $true ) ). % 2.16/2.27 % 2.16/2.27 fof(mSortsC,axiom, % 2.16/2.27 aNaturalNumber0(sz00) ). % 2.16/2.27 % 2.16/2.27 fof(mSortsC_01,axiom, % 2.16/2.27 ( aNaturalNumber0(sz10) % 2.16/2.27 & sz10 != sz00 ) ). % 2.16/2.27 % 2.16/2.27 fof(mSortsB,axiom, % 2.16/2.27 ! [W0,W1] : % 2.16/2.27 ( ( aNaturalNumber0(W0) % 2.16/2.27 & aNaturalNumber0(W1) ) % 2.16/2.27 => aNaturalNumber0(sdtpldt0(W0,W1)) ) ). % 2.16/2.27 % 2.16/2.27 fof(mSortsB_02,axiom, % 2.16/2.27 ! [W0,W1] : % 2.16/2.27 ( ( aNaturalNumber0(W0) % 2.16/2.27 & aNaturalNumber0(W1) ) % 2.16/2.27 => aNaturalNumber0(sdtasdt0(W0,W1)) ) ). % 2.16/2.27 % 2.16/2.27 fof(mAddComm,axiom, % 2.16/2.27 ! [W0,W1] : % 2.16/2.27 ( ( aNaturalNumber0(W0) % 2.16/2.27 & aNaturalNumber0(W1) ) % 2.16/2.27 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 2.16/2.27 % 2.16/2.27 fof(mAddAsso,axiom, % 2.16/2.28 ! [W0,W1,W2] : % 2.16/2.28 ( ( aNaturalNumber0(W0) % 2.16/2.28 & aNaturalNumber0(W1) % 2.16/2.28 & aNaturalNumber0(W2) ) % 2.16/2.28 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 2.16/2.28 % 2.16/2.28 fof(m_AddZero,axiom, % 2.16/2.28 ! [W0] : % 2.16/2.28 ( aNaturalNumber0(W0) % 2.16/2.28 => ( sdtpldt0(W0,sz00) = W0 % 2.16/2.28 & W0 = sdtpldt0(sz00,W0) ) ) ). % 2.16/2.28 % 2.16/2.28 fof(mMulComm,axiom, % 2.16/2.28 ! [W0,W1] : % 2.16/2.28 ( ( aNaturalNumber0(W0) % 2.16/2.28 & aNaturalNumber0(W1) ) % 2.16/2.28 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 2.16/2.28 % 2.16/2.28 fof(mMulAsso,axiom, % 2.16/2.28 ! [W0,W1,W2] : % 2.16/2.28 ( ( aNaturalNumber0(W0) % 2.16/2.28 & aNaturalNumber0(W1) % 2.16/2.28 & aNaturalNumber0(W2) ) % 2.16/2.28 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 2.16/2.28 % 2.16/2.28 fof(m_MulUnit,axiom, % 2.16/2.28 ! [W0] : % 2.16/2.28 ( aNaturalNumber0(W0) % 2.16/2.28 => ( sdtasdt0(W0,sz10) = W0 % 2.16/2.28 & W0 = sdtasdt0(sz10,W0) ) ) ). % 2.16/2.28 % 2.16/2.28 fof(m_MulZero,axiom, % 2.16/2.28 ! [W0] : % 2.16/2.28 ( aNaturalNumber0(W0) % 2.16/2.28 => ( sdtasdt0(W0,sz00) = sz00 % 2.16/2.28 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 2.16/2.28 % 2.16/2.28 fof(mAMDistr,axiom, % 2.16/2.28 ! [W0,W1,W2] : % 2.16/2.28 ( ( aNaturalNumber0(W0) % 2.16/2.28 & aNaturalNumber0(W1) % 2.16/2.28 & aNaturalNumber0(W2) ) % 2.16/2.28 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 2.16/2.28 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 2.16/2.28 % 2.16/2.28 fof(mAddCanc,axiom, % 2.16/2.28 ! [W0,W1,W2] : % 2.16/2.28 ( ( aNaturalNumber0(W0) % 2.16/2.28 & aNaturalNumber0(W1) % 2.16/2.28 & aNaturalNumber0(W2) ) % 2.16/2.28 => ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2) % 2.16/2.28 | sdtpldt0(W1,W0) = sdtpldt0(W2,W0) ) % 2.16/2.28 => W1 = W2 ) ) ). % 2.16/2.28 % 2.16/2.28 fof(mMulCanc,axiom, % 2.16/2.28 ! [W0] : % 2.16/2.28 ( aNaturalNumber0(W0) % 2.16/2.28 => ( W0 != sz00 % 2.16/2.28 => ! [W1,W2] : % 2.16/2.28 ( ( aNaturalNumber0(W1) % 2.16/2.28 & aNaturalNumber0(W2) ) % 2.16/2.28 => ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2) % 2.16/2.28 | sdtasdt0(W1,W0) = sdtasdt0(W2,W0) ) % 2.16/2.28 => W1 = W2 ) ) ) ) ). % 2.16/2.28 % 2.16/2.28 fof(mZeroAdd,axiom, % 2.16/2.28 ! [W0,W1] : % 2.16/2.28 ( ( aNaturalNumber0(W0) % 2.16/2.28 & aNaturalNumber0(W1) ) % 2.16/2.28 => ( sdtpldt0(W0,W1) = sz00 % 2.16/2.28 => ( W0 = sz00 % 2.16/2.28 & W1 = sz00 ) ) ) ). % 2.16/2.28 % 2.16/2.28 fof(mZeroMul,axiom, % 2.16/2.28 ! [W0,W1] : % 2.16/2.28 ( ( aNaturalNumber0(W0) % 2.16/2.28 & aNaturalNumber0(W1) ) % 2.16/2.28 => ( sdtasdt0(W0,W1) = sz00 % 2.16/2.28 => ( W0 = sz00 % 2.16/2.28 | W1 = sz00 ) ) ) ). % 2.16/2.28 % 2.16/2.28 fof(mDefLE,definition, % 2.16/2.28 ! [W0,W1] : % 2.16/2.28 ( ( aNaturalNumber0(W0) % 2.16/2.28 & aNaturalNumber0(W1) ) % 2.16/2.28 => ( sdtlseqdt0(W0,W1) % 2.16/2.28 <=> ? [W2] : % 2.16/2.28 ( aNaturalNumber0(W2) % 2.16/2.28 & sdtpldt0(W0,W2) = W1 ) ) ) ). % 2.16/2.28 % 2.16/2.28 fof(mDefDiff,definition, % 2.16/2.28 ! [W0,W1] : % 2.16/2.28 ( ( aNaturalNumber0(W0) % 2.16/2.28 & aNaturalNumber0(W1) ) % 2.16/2.28 => ( sdtlseqdt0(W0,W1) % 2.16/2.28 => ! [W2] : % 2.16/2.28 ( W2 = sdtmndt0(W1,W0) % 2.16/2.28 <=> ( aNaturalNumber0(W2) % 2.16/2.28 & sdtpldt0(W0,W2) = W1 ) ) ) ) ). % 2.16/2.28 % 2.16/2.28 fof(mLERefl,axiom, % 2.16/2.28 ! [W0] : % 2.16/2.28 ( aNaturalNumber0(W0) % 2.16/2.28 => sdtlseqdt0(W0,W0) ) ). % 2.16/2.28 % 2.16/2.28 fof(mLEAsym,axiom, % 2.16/2.28 ! [W0,W1] : % 2.16/2.28 ( ( aNaturalNumber0(W0) % 2.16/2.28 & aNaturalNumber0(W1) ) % 2.16/2.28 => ( ( sdtlseqdt0(W0,W1) % 2.16/2.28 & sdtlseqdt0(W1,W0) ) % 2.16/2.28 => W0 = W1 ) ) ). % 2.16/2.28 % 2.16/2.28 fof(mLETran,axiom, % 2.16/2.28 ! [W0,W1,W2] : % 2.16/2.28 ( ( aNaturalNumber0(W0) % 2.16/2.28 & aNaturalNumber0(W1) % 2.16/2.28 & aNaturalNumber0(W2) ) % 2.16/2.28 => ( ( sdtlseqdt0(W0,W1) % 2.16/2.28 & sdtlseqdt0(W1,W2) ) % 2.16/2.28 => sdtlseqdt0(W0,W2) ) ) ). % 2.16/2.28 % 2.16/2.28 fof(mLETotal,axiom, % 2.16/2.28 ! [W0,W1] : % 2.16/2.28 ( ( aNaturalNumber0(W0) % 2.16/2.28 & aNaturalNumber0(W1) ) % 2.16/2.28 => ( sdtlseqdt0(W0,W1) % 2.16/2.28 | ( W1 != W0 % 2.16/2.28 & sdtlseqdt0(W1,W0) ) ) ) ). % 2.16/2.28 % 2.16/2.28 fof(mMonAdd,axiom, % 2.16/2.28 ! [W0,W1] : % 2.16/2.28 ( ( aNaturalNumber0(W0) % 2.16/2.28 & aNaturalNumber0(W1) ) % 2.16/2.28 => ( ( W0 != W1 % 2.16/2.28 & sdtlseqdt0(W0,W1) ) % 2.16/2.28 => ! [W2] : % 2.16/2.28 ( aNaturalNumber0(W2) % 2.16/2.28 => ( sdtpldt0(W2,W0) != sdtpldt0(W2,W1) % 2.16/2.28 & sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1)) % 2.16/2.28 & sdtpldt0(W0,W2) != sdtpldt0(W1,W2) % 2.16/2.28 & sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2)) ) ) ) ) ). % 2.16/2.28 % 2.20/2.28 fof(mMonMul,axiom, % 2.20/2.28 ! [W0,W1,W2] : % 2.20/2.28 ( ( aNaturalNumber0(W0) % 2.20/2.28 & aNaturalNumber0(W1) % 2.20/2.28 & aNaturalNumber0(W2) ) % 2.20/2.28 => ( ( W0 != sz00 % 2.20/2.28 & W1 != W2 % 2.20/2.28 & sdtlseqdt0(W1,W2) ) % 2.20/2.28 => ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2) % 2.20/2.28 & sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 2.20/2.28 & sdtasdt0(W1,W0) != sdtasdt0(W2,W0) % 2.20/2.28 & sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ) ). % 2.20/2.28 % 2.20/2.28 fof(mLENTr,axiom, % 2.20/2.28 ! [W0] : % 2.20/2.28 ( aNaturalNumber0(W0) % 2.20/2.28 => ( W0 = sz00 % 2.20/2.28 | W0 = sz10 % 2.20/2.28 | ( sz10 != W0 % 2.20/2.28 & sdtlseqdt0(sz10,W0) ) ) ) ). % 2.20/2.28 % 2.20/2.28 fof(mMonMul2,axiom, % 2.20/2.28 ! [W0,W1] : % 2.20/2.28 ( ( aNaturalNumber0(W0) % 2.20/2.28 & aNaturalNumber0(W1) ) % 2.20/2.28 => ( W0 != sz00 % 2.20/2.28 => sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ) ). % 2.20/2.28 % 2.20/2.28 fof(mIH,axiom, % 2.20/2.28 ! [W0,W1] : % 2.20/2.28 ( ( aNaturalNumber0(W0) % 2.20/2.28 & aNaturalNumber0(W1) ) % 2.20/2.28 => ( iLess0(W0,W1) % 2.20/2.28 => $true ) ) ). % 2.20/2.28 % 2.20/2.28 fof(mIH_03,axiom, % 2.20/2.28 ! [W0,W1] : % 2.20/2.28 ( ( aNaturalNumber0(W0) % 2.20/2.28 & aNaturalNumber0(W1) ) % 2.20/2.28 => ( ( W0 != W1 % 2.20/2.28 & sdtlseqdt0(W0,W1) ) % 2.20/2.28 => iLess0(W0,W1) ) ) ). % 2.20/2.28 % 2.20/2.28 fof(mDefDiv,definition, % 2.20/2.28 ! [W0,W1] : % 2.20/2.28 ( ( aNaturalNumber0(W0) % 2.20/2.28 & aNaturalNumber0(W1) ) % 2.20/2.28 => ( doDivides0(W0,W1) % 2.20/2.28 <=> ? [W2] : % 2.20/2.28 ( aNaturalNumber0(W2) % 2.20/2.28 & W1 = sdtasdt0(W0,W2) ) ) ) ). % 2.20/2.28 % 2.20/2.28 fof(mDefQuot,definition, % 2.20/2.28 ! [W0,W1] : % 2.20/2.28 ( ( aNaturalNumber0(W0) % 2.20/2.28 & aNaturalNumber0(W1) ) % 2.20/2.28 => ( ( W0 != sz00 % 2.20/2.28 & doDivides0(W0,W1) ) % 2.20/2.28 => ! [W2] : % 2.20/2.28 ( W2 = sdtsldt0(W1,W0) % 2.20/2.28 <=> ( aNaturalNumber0(W2) % 2.20/2.28 & W1 = sdtasdt0(W0,W2) ) ) ) ) ). % 2.20/2.28 % 2.20/2.28 fof(mDivTrans,axiom, % 2.20/2.28 ! [W0,W1,W2] : % 2.20/2.28 ( ( aNaturalNumber0(W0) % 2.20/2.28 & aNaturalNumber0(W1) % 2.20/2.28 & aNaturalNumber0(W2) ) % 2.20/2.28 => ( ( doDivides0(W0,W1) % 2.20/2.28 & doDivides0(W1,W2) ) % 2.20/2.28 => doDivides0(W0,W2) ) ) ). % 2.20/2.28 % 2.20/2.28 fof(mDivSum,axiom, % 2.20/2.28 ! [W0,W1,W2] : % 2.20/2.28 ( ( aNaturalNumber0(W0) % 2.20/2.28 & aNaturalNumber0(W1) % 2.20/2.28 & aNaturalNumber0(W2) ) % 2.20/2.28 => ( ( doDivides0(W0,W1) % 2.20/2.28 & doDivides0(W0,W2) ) % 2.20/2.28 => doDivides0(W0,sdtpldt0(W1,W2)) ) ) ). % 2.20/2.28 % 2.20/2.28 fof(mDivMin,axiom, % 2.20/2.28 ! [W0,W1,W2] : % 2.20/2.28 ( ( aNaturalNumber0(W0) % 2.20/2.28 & aNaturalNumber0(W1) % 2.20/2.28 & aNaturalNumber0(W2) ) % 2.20/2.28 => ( ( doDivides0(W0,W1) % 2.20/2.28 & doDivides0(W0,sdtpldt0(W1,W2)) ) % 2.20/2.28 => doDivides0(W0,W2) ) ) ). % 2.20/2.28 % 2.20/2.28 fof(mDivLE,axiom, % 2.20/2.28 ! [W0,W1] : % 2.20/2.28 ( ( aNaturalNumber0(W0) % 2.20/2.28 & aNaturalNumber0(W1) ) % 2.20/2.28 => ( ( doDivides0(W0,W1) % 2.20/2.28 & W1 != sz00 ) % 2.20/2.28 => sdtlseqdt0(W0,W1) ) ) ). % 2.20/2.28 % 2.20/2.28 fof(mDivAsso,axiom, % 2.20/2.29 ! [W0,W1] : % 2.20/2.29 ( ( aNaturalNumber0(W0) % 2.20/2.29 & aNaturalNumber0(W1) ) % 2.20/2.29 => ( ( W0 != sz00 % 2.20/2.29 & doDivides0(W0,W1) ) % 2.20/2.29 => ! [W2] : % 2.20/2.29 ( aNaturalNumber0(W2) % 2.20/2.29 => sdtasdt0(W2,sdtsldt0(W1,W0)) = sdtsldt0(sdtasdt0(W2,W1),W0) ) ) ) ). % 2.20/2.29 % 2.20/2.29 fof(mDefPrime,definition, % 2.20/2.29 ! [W0] : % 2.20/2.29 ( aNaturalNumber0(W0) % 2.20/2.29 => ( isPrime0(W0) % 2.20/2.29 <=> ( W0 != sz00 % 2.20/2.29 & W0 != sz10 % 2.20/2.29 & ! [W1] : % 2.20/2.29 ( ( aNaturalNumber0(W1) % 2.20/2.29 & doDivides0(W1,W0) ) % 2.20/2.29 => ( W1 = sz10 % 2.20/2.29 | W1 = W0 ) ) ) ) ) ). % 2.20/2.29 % 2.20/2.29 fof(mPrimDiv,axiom, % 2.20/2.29 ! [W0] : % 2.20/2.29 ( ( aNaturalNumber0(W0) % 2.20/2.29 & W0 != sz00 % 2.20/2.29 & W0 != sz10 ) % 2.20/2.29 => ? [W1] : % 2.20/2.29 ( aNaturalNumber0(W1) % 2.20/2.29 & doDivides0(W1,W0) % 2.20/2.29 & isPrime0(W1) ) ) ). % 2.20/2.29 % 2.20/2.29 fof(m__1837,hypothesis, % 2.20/2.29 ( aNaturalNumber0(xn) % 2.20/2.29 & aNaturalNumber0(xm) % 2.20/2.29 & aNaturalNumber0(xp) ) ). % 2.20/2.29 % 2.20/2.29 fof(m__1799,hypothesis, % 2.20/2.29 ! [W0,W1,W2] : % 2.20/2.29 ( ( aNaturalNumber0(W0) % 2.20/2.29 & aNaturalNumber0(W1) % 2.20/2.29 & aNaturalNumber0(W2) ) % 2.20/2.29 => ( ( ( ( W2 != sz00 % 2.20/2.29 & W2 != sz10 % 2.20/2.29 & ! [W3] : % 2.20/2.29 ( ( aNaturalNumber0(W3) % 2.20/2.29 & ? [W4] : % 2.20/2.29 ( aNaturalNumber0(W4) % 2.20/2.29 & W2 = sdtasdt0(W3,W4) ) % 2.20/2.29 & doDivides0(W3,W2) ) % 2.20/2.29 => ( W3 = sz10 % 2.20/2.29 | W3 = W2 ) ) ) % 2.20/2.29 | isPrime0(W2) ) % 2.20/2.29 & ( ? [W3] : % 2.20/2.29 ( aNaturalNumber0(W3) % 2.20/2.29 & sdtasdt0(W0,W1) = sdtasdt0(W2,W3) ) % 2.20/2.29 | doDivides0(W2,sdtasdt0(W0,W1)) ) ) % 2.20/2.29 => ( iLess0(sdtpldt0(sdtpldt0(W0,W1),W2),sdtpldt0(sdtpldt0(xn,xm),xp)) % 2.20/2.29 => ( ( ? [W3] : % 2.20/2.29 ( aNaturalNumber0(W3) % 2.20/2.29 & W0 = sdtasdt0(W2,W3) ) % 2.20/2.29 & doDivides0(W2,W0) ) % 2.20/2.29 | ( ? [W3] : % 2.20/2.29 ( aNaturalNumber0(W3) % 2.20/2.29 & W1 = sdtasdt0(W2,W3) ) % 2.20/2.29 & doDivides0(W2,W1) ) ) ) ) ) ). % 2.20/2.29 % 2.20/2.29 fof(m__1860,hypothesis, % 2.20/2.29 ( xp != sz00 % 2.20/2.29 & xp != sz10 % 2.20/2.29 & ! [W0] : % 2.20/2.29 ( ( aNaturalNumber0(W0) % 2.20/2.29 & ( ? [W1] : % 2.20/2.29 ( aNaturalNumber0(W1) % 2.20/2.29 & xp = sdtasdt0(W0,W1) ) % 2.20/2.29 | doDivides0(W0,xp) ) ) % 2.20/2.29 => ( W0 = sz10 % 2.20/2.29 | W0 = xp ) ) % 2.20/2.29 & isPrime0(xp) % 2.20/2.29 & ? [W0] : % 2.20/2.29 ( aNaturalNumber0(W0) % 2.20/2.29 & sdtasdt0(xn,xm) = sdtasdt0(xp,W0) ) % 2.20/2.29 & doDivides0(xp,sdtasdt0(xn,xm)) ) ). % 2.20/2.29 % 2.20/2.29 fof(m__1870,hypothesis, % 2.20/2.29 ( ? [W0] : % 2.20/2.29 ( aNaturalNumber0(W0) % 2.20/2.29 & sdtpldt0(xp,W0) = xn ) % 2.20/2.29 & sdtlseqdt0(xp,xn) ) ). % 2.20/2.29 % 2.20/2.29 fof(m__1883,hypothesis, % 2.20/2.29 ( aNaturalNumber0(xr) % 2.20/2.29 & sdtpldt0(xp,xr) = xn % 2.20/2.29 & xr = sdtmndt0(xn,xp) ) ). % 2.20/2.29 % 2.20/2.29 fof(m__1894,hypothesis, % 2.20/2.29 ( xr != xn % 2.20/2.29 & ? [W0] : % 2.20/2.29 ( aNaturalNumber0(W0) % 2.20/2.29 & sdtpldt0(xr,W0) = xn ) % 2.20/2.29 & sdtlseqdt0(xr,xn) ) ). % 2.20/2.29 % 2.20/2.29 fof(m__1924,hypothesis, % 2.20/2.29 xn = sdtpldt0(xp,xr) ). % 2.20/2.29 % 2.20/2.29 fof(m__1951,hypothesis, % 2.20/2.29 sdtasdt0(xn,xm) = sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm)) ). % 2.20/2.29 % 2.20/2.29 fof(m__1978,hypothesis, % 2.20/2.29 ( sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm)) = sdtasdt0(xn,xm) % 2.20/2.29 & sdtasdt0(xr,xm) = sdtmndt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm)) ) ). % 2.20/2.29 % 2.20/2.29 fof(m__,conjecture, % 2.20/2.29 ( ? [W0] : % 2.20/2.29 ( aNaturalNumber0(W0) % 2.20/2.29 & sdtasdt0(xp,xm) = sdtasdt0(xp,W0) ) % 2.20/2.29 | doDivides0(xp,sdtasdt0(xp,xm)) ) ). % 2.20/2.29 % 2.20/2.29 %------------------------------------------------------------------------------ % 2.20/2.29 %------------------------------------------- % 2.20/2.29 % Proof found % 2.20/2.29 % SZS status Theorem for theBenchmark % 2.20/2.29 % SZS output start Proof % 2.20/2.29 %ClaNum:257(EqnAxiom:37) % 2.20/2.29 %VarNum:3204(SingletonVarNum:573) % 2.20/2.29 %MaxLitNum:11 % 2.20/2.29 %MaxfuncDepth:2 % 2.20/2.29 %SharedTerms:46 % 2.20/2.29 %goalClause: 64 91 % 2.20/2.29 %singleGoalClaCount:1 % 2.20/2.29 [38]P1(a1) % 2.20/2.29 [39]P1(a17) % 2.20/2.29 [40]P1(a18) % 2.20/2.29 [41]P1(a19) % 2.20/2.29 [42]P1(a20) % 2.20/2.29 [43]P1(a21) % 2.20/2.29 [44]P1(a2) % 2.20/2.29 [45]P1(a3) % 2.20/2.29 [46]P1(a4) % 2.20/2.29 [47]P2(a20) % 2.20/2.29 [53]P5(a20,a18) % 2.20/2.29 [54]P5(a21,a18) % 2.20/2.29 [60]~E(a1,a17) % 2.20/2.29 [61]~E(a1,a20) % 2.20/2.29 [62]~E(a20,a17) % 2.20/2.29 [63]~E(a21,a18) % 2.20/2.29 [49]E(f14(a18,a20),a21) % 2.20/2.29 [50]E(f13(a20,a21),a18) % 2.20/2.29 [51]E(f13(a20,a3),a18) % 2.20/2.29 [52]E(f13(a21,a4),a18) % 2.20/2.29 [55]E(f15(a20,a2),f15(a18,a19)) % 2.20/2.29 [56]P3(a20,f15(a18,a19)) % 2.20/2.29 [64]~P3(a20,f15(a20,a19)) % 2.20/2.29 [58]E(f14(f15(a18,a19),f15(a20,a19)),f15(a21,a19)) % 2.20/2.29 [59]E(f13(f15(a20,a19),f15(a21,a19)),f15(a18,a19)) % 2.20/2.29 [75]~P1(x751)+P5(x751,x751) % 2.20/2.29 [67]~P1(x671)+E(f15(a1,x671),a1) % 2.20/2.29 [68]~P1(x681)+E(f15(x681,a1),a1) % 2.20/2.29 [69]~P1(x691)+E(f13(a1,x691),x691) % 2.20/2.29 [70]~P1(x701)+E(f15(a17,x701),x701) % 2.20/2.29 [71]~P1(x711)+E(f13(x711,a1),x711) % 2.20/2.29 [72]~P1(x721)+E(f15(x721,a17),x721) % 2.20/2.29 [91]~P1(x911)+~E(f15(a20,a19),f15(a20,x911)) % 2.20/2.29 [65]~P1(x651)+~P2(x651)+~E(x651,a1) % 2.20/2.29 [66]~P1(x661)+~P2(x661)+~E(x661,a17) % 2.20/2.29 [88]~P1(x882)+~P1(x881)+E(f13(x881,x882),f13(x882,x881)) % 2.20/2.29 [89]~P1(x892)+~P1(x891)+E(f15(x891,x892),f15(x892,x891)) % 2.20/2.29 [92]~P1(x922)+~P1(x921)+P1(f13(x921,x922)) % 2.20/2.29 [93]~P1(x932)+~P1(x931)+P1(f15(x931,x932)) % 2.20/2.29 [77]~P1(x771)+E(x771,a17)+P5(a17,x771)+E(x771,a1) % 2.20/2.29 [80]~P1(x801)+E(x801,a20)+~P3(x801,a20)+E(x801,a17) % 2.20/2.29 [73]~P1(x731)+E(x731,a17)+E(x731,a1)+P1(f5(x731)) % 2.20/2.29 [74]~P1(x741)+E(x741,a17)+E(x741,a1)+P2(f5(x741)) % 2.20/2.29 [81]~P1(x811)+E(x811,a17)+P3(f5(x811),x811)+E(x811,a1) % 2.20/2.29 [82]~E(x822,x821)+~P1(x821)+~P1(x822)+P5(x821,x822) % 2.20/2.29 [90]P5(x902,x901)+~P1(x901)+~P1(x902)+P5(x901,x902) % 2.20/2.29 [84]~P1(x842)+~P1(x841)+E(x841,a1)+~E(f13(x842,x841),a1) % 2.20/2.29 [85]~P1(x852)+~P1(x851)+E(x851,a1)+~E(f13(x851,x852),a1) % 2.20/2.29 [97]~P1(x972)+~P1(x971)+P5(x972,f15(x972,x971))+E(x971,a1) % 2.20/2.29 [103]~P1(x1032)+~P1(x1031)+~P5(x1031,x1032)+P1(f7(x1031,x1032)) % 2.20/2.29 [104]~P1(x1042)+~P1(x1041)+~P3(x1041,x1042)+P1(f8(x1041,x1042)) % 2.20/2.29 [111]~P1(x1111)+~P1(x1112)+~P3(x1111,x1112)+E(f15(x1111,f8(x1111,x1112)),x1112) % 2.20/2.29 [112]~P1(x1122)+~P1(x1121)+~P5(x1121,x1122)+E(f13(x1121,f7(x1121,x1122)),x1122) % 2.20/2.29 [121]~P1(x1213)+~P1(x1212)+~P1(x1211)+E(f13(f13(x1211,x1212),x1213),f13(x1211,f13(x1212,x1213))) % 2.20/2.29 [122]~P1(x1223)+~P1(x1222)+~P1(x1221)+E(f15(f15(x1221,x1222),x1223),f15(x1221,f15(x1222,x1223))) % 2.20/2.29 [130]~P1(x1303)+~P1(x1302)+~P1(x1301)+E(f13(f15(x1301,x1302),f15(x1301,x1303)),f15(x1301,f13(x1302,x1303))) % 2.20/2.29 [131]~P1(x1312)+~P1(x1313)+~P1(x1311)+E(f13(f15(x1311,x1312),f15(x1313,x1312)),f15(f13(x1311,x1313),x1312)) % 2.20/2.29 [76]P2(x761)+~P1(x761)+E(x761,a17)+E(x761,a1)+~E(f6(x761),a17) % 2.20/2.29 [78]P2(x781)+~P1(x781)+E(x781,a17)+~E(f6(x781),x781)+E(x781,a1) % 2.20/2.29 [79]P2(x791)+~P1(x791)+E(x791,a17)+E(x791,a1)+P1(f6(x791)) % 2.20/2.29 [83]P2(x831)+~P1(x831)+E(x831,a17)+P3(f6(x831),x831)+E(x831,a1) % 2.20/2.29 [95]~P1(x951)+~P1(x952)+~P3(x952,x951)+P5(x952,x951)+E(x951,a1) % 2.20/2.29 [96]P4(x961,x962)+~P1(x962)+~P1(x961)+~P5(x961,x962)+E(x961,x962) % 2.20/2.29 [100]~P1(x1002)+~P1(x1001)+~P5(x1002,x1001)+~P5(x1001,x1002)+E(x1001,x1002) % 2.20/2.29 [86]~P1(x861)+~P1(x862)+E(x861,a20)+E(x861,a17)+~E(f15(x861,x862),a20) % 2.20/2.29 [87]~P1(x871)+~P1(x872)+E(x871,a1)+E(x872,a1)+~E(f15(x872,x871),a1) % 2.20/2.29 [98]~P1(x981)+~P1(x982)+~P1(x983)+P3(x981,x982)+~E(x982,f15(x981,x983)) % 2.20/2.29 [99]~P1(x992)+~P1(x991)+~P1(x993)+P5(x991,x992)+~E(f13(x991,x993),x992) % 2.20/2.29 [101]~P1(x1013)+~P1(x1012)+~P5(x1013,x1012)+P1(x1011)+~E(x1011,f14(x1012,x1013)) % 2.20/2.29 [105]~P1(x1052)+~P1(x1051)+~P1(x1053)+E(x1051,x1052)+~E(f13(x1053,x1051),f13(x1053,x1052)) % 2.20/2.29 [106]~P1(x1062)+~P1(x1063)+~P1(x1061)+E(x1061,x1062)+~E(f13(x1061,x1063),f13(x1062,x1063)) % 2.20/2.29 [109]~P1(x1093)+~P1(x1091)+~P5(x1091,x1093)+~E(x1092,f14(x1093,x1091))+E(f13(x1091,x1092),x1093) % 2.20/2.29 [94]~P1(x942)+~P1(x941)+~P2(x942)+~P3(x941,x942)+E(x941,x942)+E(x941,a17) % 2.20/2.29 [113]~P1(x1132)+~P1(x1131)+~P5(x1133,x1132)+~P5(x1131,x1133)+P5(x1131,x1132)+~P1(x1133) % 2.20/2.29 [114]~P1(x1142)+~P1(x1141)+~P3(x1143,x1142)+~P3(x1141,x1143)+P3(x1141,x1142)+~P1(x1143) % 2.20/2.29 [102]~P1(x1021)+~P1(x1023)+~P3(x1021,x1023)+P1(x1022)+E(x1021,a1)+~E(x1022,f16(x1023,x1021)) % 2.20/2.29 [107]~P1(x1072)+~P1(x1071)+~P1(x1073)+E(x1071,x1072)+~E(f15(x1073,x1071),f15(x1073,x1072))+E(x1073,a1) % 2.20/2.29 [108]~P1(x1082)+~P1(x1083)+~P1(x1081)+E(x1081,x1082)+~E(f15(x1081,x1083),f15(x1082,x1083))+E(x1083,a1) % 2.20/2.29 [110]~P1(x1101)+~P1(x1102)+~P3(x1101,x1102)+~E(x1103,f16(x1102,x1101))+E(x1101,a1)+E(x1102,f15(x1101,x1103)) % 2.20/2.29 [115]~P1(x1152)+~P1(x1153)+~P1(x1151)+~P5(x1153,x1152)+~E(f13(x1153,x1151),x1152)+E(x1151,f14(x1152,x1153)) % 2.20/2.29 [123]~P1(x1233)+~P1(x1232)+~P1(x1231)+~P3(x1231,x1233)+~P3(x1231,x1232)+P3(x1231,f13(x1232,x1233)) % 2.20/2.29 [124]~P1(x1242)+~P1(x1241)+~P1(x1243)+~P5(x1241,x1242)+E(x1241,x1242)+P5(f13(x1243,x1241),f13(x1243,x1242)) % 2.20/2.29 [125]~P1(x1252)+~P1(x1253)+~P1(x1251)+~P5(x1251,x1252)+E(x1251,x1252)+P5(f13(x1251,x1253),f13(x1252,x1253)) % 2.20/2.29 [128]~P1(x1282)+~P1(x1281)+~P3(x1281,x1283)+P3(x1281,x1282)+~P1(x1283)+~P3(x1281,f13(x1283,x1282)) % 2.20/2.29 [129]~P1(x1292)+~P1(x1293)+~P1(x1291)+~P3(x1291,x1293)+E(x1291,a1)+E(f16(f15(x1292,x1293),x1291),f15(x1292,f16(x1293,x1291))) % 2.20/2.29 [116]~P1(x1161)+~P1(x1163)+~P1(x1162)+~P3(x1161,x1163)+~E(x1163,f15(x1161,x1162))+E(x1161,a1)+E(x1162,f16(x1163,x1161)) % 2.20/2.29 [126]~P1(x1262)+~P1(x1261)+~P1(x1263)+~P5(x1261,x1262)+E(x1261,x1262)+P5(f15(x1263,x1261),f15(x1263,x1262))+E(x1263,a1) % 2.20/2.29 [127]~P1(x1272)+~P1(x1273)+~P1(x1271)+~P5(x1271,x1272)+E(x1271,x1272)+P5(f15(x1271,x1273),f15(x1272,x1273))+E(x1273,a1) % 2.20/2.29 [133]~P1(x1332)+~P1(x1333)+~P1(x1331)+~P2(x1331)+P3(x1331,x1332)+P3(x1331,x1333)+~P3(x1331,f15(x1332,x1333))+~P4(f13(f13(x1332,x1333),x1331),f13(f13(a18,a19),a20)) % 2.20/2.29 [144]~P1(x1441)+~P1(x1443)+~P1(x1442)+~P2(x1441)+P3(x1441,x1442)+~P3(x1441,f15(x1442,x1443))+P1(f10(x1442,x1443,x1441))+~P4(f13(f13(x1442,x1443),x1441),f13(f13(a18,a19),a20)) % 2.20/2.29 [145]~P1(x1453)+~P1(x1452)+~P1(x1451)+~P2(x1451)+P3(x1451,x1452)+~P3(x1451,f15(x1453,x1452))+P1(f11(x1453,x1452,x1451))+~P4(f13(f13(x1453,x1452),x1451),f13(f13(a18,a19),a20)) % 2.20/2.29 [149]P3(x1491,x1493)+~P1(x1492)+~P1(x1493)+~P1(x1491)+~P2(x1491)+~P3(x1491,f15(x1492,x1493))+E(f15(x1491,f11(x1492,x1493,x1491)),x1492)+~P4(f13(f13(x1492,x1493),x1491),f13(f13(a18,a19),a20)) % 2.20/2.29 [150]P3(x1501,x1502)+~P1(x1502)+~P1(x1501)+~P1(x1503)+~P2(x1501)+~P3(x1501,f15(x1502,x1503))+E(f15(x1501,f10(x1502,x1503,x1501)),x1503)+~P4(f13(f13(x1502,x1503),x1501),f13(f13(a18,a19),a20)) % 2.20/2.29 [175]~P1(x1753)+~P1(x1752)+~P1(x1751)+~P2(x1753)+~P3(x1753,f15(x1751,x1752))+P1(f10(x1751,x1752,x1753))+~P4(f13(f13(x1751,x1752),x1753),f13(f13(a18,a19),a20))+P1(f11(x1751,x1752,x1753)) % 2.20/2.29 [187]~P1(x1871)+~P1(x1873)+~P1(x1872)+~P2(x1871)+~P3(x1871,f15(x1872,x1873))+P1(f10(x1872,x1873,x1871))+~P4(f13(f13(x1872,x1873),x1871),f13(f13(a18,a19),a20))+E(f15(x1871,f11(x1872,x1873,x1871)),x1872) % 2.20/2.29 [188]~P1(x1882)+~P1(x1881)+~P1(x1883)+~P2(x1881)+~P3(x1881,f15(x1882,x1883))+P1(f11(x1882,x1883,x1881))+~P4(f13(f13(x1882,x1883),x1881),f13(f13(a18,a19),a20))+E(f15(x1881,f10(x1882,x1883,x1881)),x1883) % 2.20/2.29 [198]~P1(x1982)+~P1(x1981)+~P1(x1983)+~P2(x1981)+~P3(x1981,f15(x1982,x1983))+E(f15(x1981,f10(x1982,x1983,x1981)),x1983)+~P4(f13(f13(x1982,x1983),x1981),f13(f13(a18,a19),a20))+E(f15(x1981,f11(x1982,x1983,x1981)),x1982) % 2.20/2.29 [132]~P1(x1324)+~P1(x1322)+~P1(x1323)+~P1(x1321)+~P2(x1321)+P3(x1321,x1322)+P3(x1321,x1323)+~E(f15(x1321,x1324),f15(x1322,x1323))+~P4(f13(f13(x1322,x1323),x1321),f13(f13(a18,a19),a20)) % 2.20/2.29 [138]~P1(x1384)+~P1(x1381)+~P1(x1383)+~P1(x1382)+~P2(x1381)+P3(x1381,x1382)+~E(f15(x1382,x1383),f15(x1381,x1384))+P1(f10(x1382,x1383,x1381))+~P4(f13(f13(x1382,x1383),x1381),f13(f13(a18,a19),a20)) % 2.20/2.29 [139]~P1(x1394)+~P1(x1393)+~P1(x1392)+~P1(x1391)+~P2(x1391)+P3(x1391,x1392)+~E(f15(x1391,x1394),f15(x1393,x1392))+P1(f11(x1393,x1392,x1391))+~P4(f13(f13(x1393,x1392),x1391),f13(f13(a18,a19),a20)) % 2.20/2.29 [142]P3(x1421,x1423)+~P1(x1424)+~P1(x1422)+~P1(x1423)+~P1(x1421)+~P2(x1421)+~E(f15(x1421,x1424),f15(x1422,x1423))+E(f15(x1421,f11(x1422,x1423,x1421)),x1422)+~P4(f13(f13(x1422,x1423),x1421),f13(f13(a18,a19),a20)) % 2.20/2.29 [143]P3(x1431,x1432)+~P1(x1434)+~P1(x1432)+~P1(x1431)+~P1(x1433)+~P2(x1431)+~E(f15(x1431,x1434),f15(x1432,x1433))+E(f15(x1431,f10(x1432,x1433,x1431)),x1433)+~P4(f13(f13(x1432,x1433),x1431),f13(f13(a18,a19),a20)) % 2.20/2.29 [164]~P1(x1644)+~P1(x1643)+~P1(x1642)+~P1(x1641)+~P2(x1643)+~E(f15(x1641,x1642),f15(x1643,x1644))+P1(f10(x1641,x1642,x1643))+~P4(f13(f13(x1641,x1642),x1643),f13(f13(a18,a19),a20))+P1(f11(x1641,x1642,x1643)) % 2.20/2.29 [173]~P1(x1734)+~P1(x1731)+~P1(x1733)+~P1(x1732)+~P2(x1731)+~E(f15(x1732,x1733),f15(x1731,x1734))+P1(f10(x1732,x1733,x1731))+~P4(f13(f13(x1732,x1733),x1731),f13(f13(a18,a19),a20))+E(f15(x1731,f11(x1732,x1733,x1731)),x1732) % 2.20/2.29 [174]~P1(x1744)+~P1(x1742)+~P1(x1741)+~P1(x1743)+~P2(x1741)+~E(f15(x1741,x1744),f15(x1742,x1743))+P1(f11(x1742,x1743,x1741))+~P4(f13(f13(x1742,x1743),x1741),f13(f13(a18,a19),a20))+E(f15(x1741,f10(x1742,x1743,x1741)),x1743) % 2.20/2.29 [182]~P1(x1824)+~P1(x1822)+~P1(x1821)+~P1(x1823)+~P2(x1821)+~E(f15(x1821,x1824),f15(x1822,x1823))+E(f15(x1821,f10(x1822,x1823,x1821)),x1823)+~P4(f13(f13(x1822,x1823),x1821),f13(f13(a18,a19),a20))+E(f15(x1821,f11(x1822,x1823,x1821)),x1822) % 2.20/2.29 [136]~P1(x1362)+~P1(x1363)+~P1(x1361)+P3(x1361,x1362)+P3(x1361,x1363)+E(x1361,a17)+~P3(x1361,f15(x1362,x1363))+E(x1361,a1)+~E(f9(x1362,x1363,x1361),a17)+~P4(f13(f13(x1362,x1363),x1361),f13(f13(a18,a19),a20)) % 2.20/2.29 [137]~P1(x1372)+~P1(x1373)+~P1(x1371)+P3(x1371,x1372)+P3(x1371,x1373)+E(x1371,a17)+~E(f9(x1372,x1373,x1371),x1371)+~P3(x1371,f15(x1372,x1373))+E(x1371,a1)+~P4(f13(f13(x1372,x1373),x1371),f13(f13(a18,a19),a20)) % 2.20/2.29 [147]~P1(x1472)+~P1(x1473)+~P1(x1471)+P3(x1471,x1472)+P3(x1471,x1473)+E(x1471,a17)+~P3(x1471,f15(x1472,x1473))+E(x1471,a1)+P1(f9(x1472,x1473,x1471))+~P4(f13(f13(x1472,x1473),x1471),f13(f13(a18,a19),a20)) % 2.20/2.29 [148]~P1(x1482)+~P1(x1483)+~P1(x1481)+P3(x1481,x1482)+P3(x1481,x1483)+E(x1481,a17)+~P3(x1481,f15(x1482,x1483))+E(x1481,a1)+P1(f12(x1482,x1483,x1481))+~P4(f13(f13(x1482,x1483),x1481),f13(f13(a18,a19),a20)) % 2.20/2.29 [151]~P1(x1512)+~P1(x1513)+~P1(x1511)+P3(x1511,x1512)+P3(x1511,x1513)+E(x1511,a17)+P3(f9(x1512,x1513,x1511),x1511)+~P3(x1511,f15(x1512,x1513))+E(x1511,a1)+~P4(f13(f13(x1512,x1513),x1511),f13(f13(a18,a19),a20)) % 2.20/2.29 [160]~P1(x1601)+~P1(x1603)+~P1(x1602)+P3(x1601,x1602)+E(x1601,a17)+~P3(x1601,f15(x1602,x1603))+E(x1601,a1)+~E(f9(x1602,x1603,x1601),a17)+~P4(f13(f13(x1602,x1603),x1601),f13(f13(a18,a19),a20))+P1(f10(x1602,x1603,x1601)) % 2.20/2.29 [161]~P1(x1613)+~P1(x1612)+~P1(x1611)+P3(x1611,x1612)+E(x1611,a17)+~P3(x1611,f15(x1613,x1612))+E(x1611,a1)+~E(f9(x1613,x1612,x1611),a17)+~P4(f13(f13(x1613,x1612),x1611),f13(f13(a18,a19),a20))+P1(f11(x1613,x1612,x1611)) % 2.20/2.29 [162]~P1(x1621)+~P1(x1623)+~P1(x1622)+P3(x1621,x1622)+E(x1621,a17)+~E(f9(x1622,x1623,x1621),x1621)+~P3(x1621,f15(x1622,x1623))+E(x1621,a1)+~P4(f13(f13(x1622,x1623),x1621),f13(f13(a18,a19),a20))+P1(f10(x1622,x1623,x1621)) % 2.20/2.29 [163]~P1(x1633)+~P1(x1632)+~P1(x1631)+P3(x1631,x1632)+E(x1631,a17)+~E(f9(x1633,x1632,x1631),x1631)+~P3(x1631,f15(x1633,x1632))+E(x1631,a1)+~P4(f13(f13(x1633,x1632),x1631),f13(f13(a18,a19),a20))+P1(f11(x1633,x1632,x1631)) % 2.20/2.29 [165]P3(x1651,x1652)+~P1(x1652)+~P1(x1651)+~P1(x1653)+E(x1651,a17)+~P3(x1651,f15(x1652,x1653))+E(x1651,a1)+~E(f9(x1652,x1653,x1651),a17)+~P4(f13(f13(x1652,x1653),x1651),f13(f13(a18,a19),a20))+E(f15(x1651,f10(x1652,x1653,x1651)),x1653) % 2.20/2.29 [166]P3(x1661,x1663)+~P1(x1662)+~P1(x1663)+~P1(x1661)+E(x1661,a17)+~P3(x1661,f15(x1662,x1663))+E(x1661,a1)+~E(f9(x1662,x1663,x1661),a17)+~P4(f13(f13(x1662,x1663),x1661),f13(f13(a18,a19),a20))+E(f15(x1661,f11(x1662,x1663,x1661)),x1662) % 2.20/2.29 [167]P3(x1671,x1672)+~P1(x1672)+~P1(x1671)+~P1(x1673)+E(x1671,a17)+~E(f9(x1672,x1673,x1671),x1671)+~P3(x1671,f15(x1672,x1673))+E(x1671,a1)+~P4(f13(f13(x1672,x1673),x1671),f13(f13(a18,a19),a20))+E(f15(x1671,f10(x1672,x1673,x1671)),x1673) % 2.20/2.29 [168]P3(x1681,x1683)+~P1(x1682)+~P1(x1683)+~P1(x1681)+E(x1681,a17)+~E(f9(x1682,x1683,x1681),x1681)+~P3(x1681,f15(x1682,x1683))+E(x1681,a1)+~P4(f13(f13(x1682,x1683),x1681),f13(f13(a18,a19),a20))+E(f15(x1681,f11(x1682,x1683,x1681)),x1682) % 2.20/2.29 [183]~P1(x1831)+~P1(x1833)+~P1(x1832)+P3(x1831,x1832)+E(x1831,a17)+~P3(x1831,f15(x1832,x1833))+E(x1831,a1)+P1(f10(x1832,x1833,x1831))+~P4(f13(f13(x1832,x1833),x1831),f13(f13(a18,a19),a20))+P1(f9(x1832,x1833,x1831)) % 2.20/2.29 [184]~P1(x1841)+~P1(x1843)+~P1(x1842)+P3(x1841,x1842)+E(x1841,a17)+~P3(x1841,f15(x1842,x1843))+E(x1841,a1)+P1(f10(x1842,x1843,x1841))+~P4(f13(f13(x1842,x1843),x1841),f13(f13(a18,a19),a20))+P1(f12(x1842,x1843,x1841)) % 2.20/2.29 [185]~P1(x1853)+~P1(x1852)+~P1(x1851)+P3(x1851,x1852)+E(x1851,a17)+~P3(x1851,f15(x1853,x1852))+E(x1851,a1)+P1(f11(x1853,x1852,x1851))+~P4(f13(f13(x1853,x1852),x1851),f13(f13(a18,a19),a20))+P1(f9(x1853,x1852,x1851)) % 2.20/2.29 [186]~P1(x1863)+~P1(x1862)+~P1(x1861)+P3(x1861,x1862)+E(x1861,a17)+~P3(x1861,f15(x1863,x1862))+E(x1861,a1)+P1(f11(x1863,x1862,x1861))+~P4(f13(f13(x1863,x1862),x1861),f13(f13(a18,a19),a20))+P1(f12(x1863,x1862,x1861)) % 2.20/2.29 [192]~P1(x1921)+~P1(x1923)+~P1(x1922)+P3(x1921,x1922)+E(x1921,a17)+P3(f9(x1922,x1923,x1921),x1921)+~P3(x1921,f15(x1922,x1923))+E(x1921,a1)+~P4(f13(f13(x1922,x1923),x1921),f13(f13(a18,a19),a20))+P1(f10(x1922,x1923,x1921)) % 2.20/2.29 [193]~P1(x1933)+~P1(x1932)+~P1(x1931)+P3(x1931,x1932)+E(x1931,a17)+P3(f9(x1933,x1932,x1931),x1931)+~P3(x1931,f15(x1933,x1932))+E(x1931,a1)+~P4(f13(f13(x1933,x1932),x1931),f13(f13(a18,a19),a20))+P1(f11(x1933,x1932,x1931)) % 2.20/2.29 [194]P3(x1941,x1942)+~P1(x1942)+~P1(x1941)+~P1(x1943)+E(x1941,a17)+~P3(x1941,f15(x1942,x1943))+E(x1941,a1)+P1(f9(x1942,x1943,x1941))+~P4(f13(f13(x1942,x1943),x1941),f13(f13(a18,a19),a20))+E(f15(x1941,f10(x1942,x1943,x1941)),x1943) % 2.20/2.29 [195]P3(x1951,x1952)+~P1(x1952)+~P1(x1951)+~P1(x1953)+E(x1951,a17)+~P3(x1951,f15(x1952,x1953))+E(x1951,a1)+P1(f12(x1952,x1953,x1951))+~P4(f13(f13(x1952,x1953),x1951),f13(f13(a18,a19),a20))+E(f15(x1951,f10(x1952,x1953,x1951)),x1953) % 2.20/2.29 [196]P3(x1961,x1963)+~P1(x1962)+~P1(x1963)+~P1(x1961)+E(x1961,a17)+~P3(x1961,f15(x1962,x1963))+E(x1961,a1)+P1(f9(x1962,x1963,x1961))+~P4(f13(f13(x1962,x1963),x1961),f13(f13(a18,a19),a20))+E(f15(x1961,f11(x1962,x1963,x1961)),x1962) % 2.20/2.29 [197]P3(x1971,x1973)+~P1(x1972)+~P1(x1973)+~P1(x1971)+E(x1971,a17)+~P3(x1971,f15(x1972,x1973))+E(x1971,a1)+P1(f12(x1972,x1973,x1971))+~P4(f13(f13(x1972,x1973),x1971),f13(f13(a18,a19),a20))+E(f15(x1971,f11(x1972,x1973,x1971)),x1972) % 2.20/2.29 [199]P3(x1991,x1992)+~P1(x1992)+~P1(x1991)+~P1(x1993)+E(x1991,a17)+P3(f9(x1992,x1993,x1991),x1991)+~P3(x1991,f15(x1992,x1993))+E(x1991,a1)+~P4(f13(f13(x1992,x1993),x1991),f13(f13(a18,a19),a20))+E(f15(x1991,f10(x1992,x1993,x1991)),x1993) % 2.20/2.29 [200]P3(x2001,x2003)+~P1(x2002)+~P1(x2003)+~P1(x2001)+E(x2001,a17)+P3(f9(x2002,x2003,x2001),x2001)+~P3(x2001,f15(x2002,x2003))+E(x2001,a1)+~P4(f13(f13(x2002,x2003),x2001),f13(f13(a18,a19),a20))+E(f15(x2001,f11(x2002,x2003,x2001)),x2002) % 2.20/2.29 [201]P3(x2011,x2012)+P3(x2011,x2013)+~P1(x2012)+~P1(x2013)+~P1(x2011)+E(x2011,a17)+~P3(x2011,f15(x2012,x2013))+E(x2011,a1)+~P4(f13(f13(x2012,x2013),x2011),f13(f13(a18,a19),a20))+E(f15(f9(x2012,x2013,x2011),f12(x2012,x2013,x2011)),x2011) % 2.20/2.29 [208]~P1(x2081)+~P1(x2083)+~P1(x2082)+E(x2081,a17)+~P3(x2081,f15(x2082,x2083))+E(x2081,a1)+P1(f10(x2082,x2083,x2081))+~E(f9(x2082,x2083,x2081),a17)+~P4(f13(f13(x2082,x2083),x2081),f13(f13(a18,a19),a20))+P1(f11(x2082,x2083,x2081)) % 2.20/2.29 [209]~P1(x2091)+~P1(x2093)+~P1(x2092)+E(x2091,a17)+~E(f9(x2092,x2093,x2091),x2091)+~P3(x2091,f15(x2092,x2093))+E(x2091,a1)+P1(f10(x2092,x2093,x2091))+~P4(f13(f13(x2092,x2093),x2091),f13(f13(a18,a19),a20))+P1(f11(x2092,x2093,x2091)) % 2.20/2.29 [212]~P1(x2121)+~P1(x2123)+~P1(x2122)+E(x2121,a17)+~P3(x2121,f15(x2122,x2123))+E(x2121,a1)+P1(f10(x2122,x2123,x2121))+~E(f9(x2122,x2123,x2121),a17)+~P4(f13(f13(x2122,x2123),x2121),f13(f13(a18,a19),a20))+E(f15(x2121,f11(x2122,x2123,x2121)),x2122) % 2.20/2.29 [213]~P1(x2132)+~P1(x2131)+~P1(x2133)+E(x2131,a17)+~P3(x2131,f15(x2132,x2133))+E(x2131,a1)+P1(f11(x2132,x2133,x2131))+~E(f9(x2132,x2133,x2131),a17)+~P4(f13(f13(x2132,x2133),x2131),f13(f13(a18,a19),a20))+E(f15(x2131,f10(x2132,x2133,x2131)),x2133) % 2.20/2.29 [214]~P1(x2141)+~P1(x2143)+~P1(x2142)+E(x2141,a17)+~E(f9(x2142,x2143,x2141),x2141)+~P3(x2141,f15(x2142,x2143))+E(x2141,a1)+P1(f10(x2142,x2143,x2141))+~P4(f13(f13(x2142,x2143),x2141),f13(f13(a18,a19),a20))+E(f15(x2141,f11(x2142,x2143,x2141)),x2142) % 2.20/2.29 [215]~P1(x2152)+~P1(x2151)+~P1(x2153)+E(x2151,a17)+~E(f9(x2152,x2153,x2151),x2151)+~P3(x2151,f15(x2152,x2153))+E(x2151,a1)+P1(f11(x2152,x2153,x2151))+~P4(f13(f13(x2152,x2153),x2151),f13(f13(a18,a19),a20))+E(f15(x2151,f10(x2152,x2153,x2151)),x2153) % 2.20/2.29 [218]~P1(x2182)+~P1(x2181)+~P1(x2183)+E(x2181,a17)+~P3(x2181,f15(x2182,x2183))+E(x2181,a1)+E(f15(x2181,f10(x2182,x2183,x2181)),x2183)+~E(f9(x2182,x2183,x2181),a17)+~P4(f13(f13(x2182,x2183),x2181),f13(f13(a18,a19),a20))+E(f15(x2181,f11(x2182,x2183,x2181)),x2182) % 2.20/2.29 [219]~P1(x2192)+~P1(x2191)+~P1(x2193)+E(x2191,a17)+~E(f9(x2192,x2193,x2191),x2191)+~P3(x2191,f15(x2192,x2193))+E(x2191,a1)+E(f15(x2191,f10(x2192,x2193,x2191)),x2193)+~P4(f13(f13(x2192,x2193),x2191),f13(f13(a18,a19),a20))+E(f15(x2191,f11(x2192,x2193,x2191)),x2192) % 2.20/2.29 [225]~P1(x2251)+~P1(x2253)+~P1(x2252)+E(x2251,a17)+~P3(x2251,f15(x2252,x2253))+E(x2251,a1)+P1(f11(x2252,x2253,x2251))+P1(f10(x2252,x2253,x2251))+~P4(f13(f13(x2252,x2253),x2251),f13(f13(a18,a19),a20))+P1(f9(x2252,x2253,x2251)) % 2.20/2.29 [226]~P1(x2261)+~P1(x2263)+~P1(x2262)+E(x2261,a17)+~P3(x2261,f15(x2262,x2263))+E(x2261,a1)+P1(f11(x2262,x2263,x2261))+P1(f10(x2262,x2263,x2261))+~P4(f13(f13(x2262,x2263),x2261),f13(f13(a18,a19),a20))+P1(f12(x2262,x2263,x2261)) % 2.20/2.29 [233]~P1(x2331)+~P1(x2333)+~P1(x2332)+E(x2331,a17)+P3(f9(x2332,x2333,x2331),x2331)+~P3(x2331,f15(x2332,x2333))+E(x2331,a1)+P1(f10(x2332,x2333,x2331))+~P4(f13(f13(x2332,x2333),x2331),f13(f13(a18,a19),a20))+P1(f11(x2332,x2333,x2331)) % 2.20/2.29 [234]~P1(x2341)+~P1(x2343)+~P1(x2342)+E(x2341,a17)+~P3(x2341,f15(x2342,x2343))+E(x2341,a1)+P1(f9(x2342,x2343,x2341))+P1(f10(x2342,x2343,x2341))+~P4(f13(f13(x2342,x2343),x2341),f13(f13(a18,a19),a20))+E(f15(x2341,f11(x2342,x2343,x2341)),x2342) % 2.20/2.29 [235]~P1(x2351)+~P1(x2353)+~P1(x2352)+E(x2351,a17)+~P3(x2351,f15(x2352,x2353))+E(x2351,a1)+P1(f12(x2352,x2353,x2351))+P1(f10(x2352,x2353,x2351))+~P4(f13(f13(x2352,x2353),x2351),f13(f13(a18,a19),a20))+E(f15(x2351,f11(x2352,x2353,x2351)),x2352) % 2.20/2.29 [236]~P1(x2362)+~P1(x2361)+~P1(x2363)+E(x2361,a17)+~P3(x2361,f15(x2362,x2363))+E(x2361,a1)+P1(f9(x2362,x2363,x2361))+P1(f11(x2362,x2363,x2361))+~P4(f13(f13(x2362,x2363),x2361),f13(f13(a18,a19),a20))+E(f15(x2361,f10(x2362,x2363,x2361)),x2363) % 2.20/2.29 [237]~P1(x2372)+~P1(x2371)+~P1(x2373)+E(x2371,a17)+~P3(x2371,f15(x2372,x2373))+E(x2371,a1)+P1(f12(x2372,x2373,x2371))+P1(f11(x2372,x2373,x2371))+~P4(f13(f13(x2372,x2373),x2371),f13(f13(a18,a19),a20))+E(f15(x2371,f10(x2372,x2373,x2371)),x2373) % 2.20/2.29 [241]~P1(x2411)+~P1(x2413)+~P1(x2412)+E(x2411,a17)+P3(f9(x2412,x2413,x2411),x2411)+~P3(x2411,f15(x2412,x2413))+E(x2411,a1)+P1(f10(x2412,x2413,x2411))+~P4(f13(f13(x2412,x2413),x2411),f13(f13(a18,a19),a20))+E(f15(x2411,f11(x2412,x2413,x2411)),x2412) % 2.20/2.29 [242]~P1(x2422)+~P1(x2421)+~P1(x2423)+E(x2421,a17)+P3(f9(x2422,x2423,x2421),x2421)+~P3(x2421,f15(x2422,x2423))+E(x2421,a1)+P1(f11(x2422,x2423,x2421))+~P4(f13(f13(x2422,x2423),x2421),f13(f13(a18,a19),a20))+E(f15(x2421,f10(x2422,x2423,x2421)),x2423) % 2.20/2.29 [243]P3(x2431,x2432)+~P1(x2431)+~P1(x2433)+~P1(x2432)+E(x2431,a17)+~P3(x2431,f15(x2432,x2433))+E(x2431,a1)+P1(f10(x2432,x2433,x2431))+~P4(f13(f13(x2432,x2433),x2431),f13(f13(a18,a19),a20))+E(f15(f9(x2432,x2433,x2431),f12(x2432,x2433,x2431)),x2431) % 2.20/2.29 [244]P3(x2441,x2443)+~P1(x2442)+~P1(x2443)+~P1(x2441)+E(x2441,a17)+~P3(x2441,f15(x2442,x2443))+E(x2441,a1)+P1(f11(x2442,x2443,x2441))+~P4(f13(f13(x2442,x2443),x2441),f13(f13(a18,a19),a20))+E(f15(f9(x2442,x2443,x2441),f12(x2442,x2443,x2441)),x2441) % 2.20/2.29 [245]~P1(x2452)+~P1(x2451)+~P1(x2453)+E(x2451,a17)+~P3(x2451,f15(x2452,x2453))+E(x2451,a1)+E(f15(x2451,f10(x2452,x2453,x2451)),x2453)+P1(f9(x2452,x2453,x2451))+~P4(f13(f13(x2452,x2453),x2451),f13(f13(a18,a19),a20))+E(f15(x2451,f11(x2452,x2453,x2451)),x2452) % 2.20/2.29 [246]~P1(x2462)+~P1(x2461)+~P1(x2463)+E(x2461,a17)+~P3(x2461,f15(x2462,x2463))+E(x2461,a1)+E(f15(x2461,f10(x2462,x2463,x2461)),x2463)+P1(f12(x2462,x2463,x2461))+~P4(f13(f13(x2462,x2463),x2461),f13(f13(a18,a19),a20))+E(f15(x2461,f11(x2462,x2463,x2461)),x2462) % 2.20/2.29 [247]~P1(x2472)+~P1(x2471)+~P1(x2473)+E(x2471,a17)+P3(f9(x2472,x2473,x2471),x2471)+~P3(x2471,f15(x2472,x2473))+E(x2471,a1)+E(f15(x2471,f10(x2472,x2473,x2471)),x2473)+~P4(f13(f13(x2472,x2473),x2471),f13(f13(a18,a19),a20))+E(f15(x2471,f11(x2472,x2473,x2471)),x2472) % 2.20/2.29 [248]P3(x2481,x2482)+~P1(x2482)+~P1(x2481)+~P1(x2483)+E(x2481,a17)+~P3(x2481,f15(x2482,x2483))+E(x2481,a1)+E(f15(f9(x2482,x2483,x2481),f12(x2482,x2483,x2481)),x2481)+~P4(f13(f13(x2482,x2483),x2481),f13(f13(a18,a19),a20))+E(f15(x2481,f10(x2482,x2483,x2481)),x2483) % 2.20/2.29 [249]P3(x2491,x2493)+~P1(x2492)+~P1(x2493)+~P1(x2491)+E(x2491,a17)+~P3(x2491,f15(x2492,x2493))+E(x2491,a1)+E(f15(f9(x2492,x2493,x2491),f12(x2492,x2493,x2491)),x2491)+~P4(f13(f13(x2492,x2493),x2491),f13(f13(a18,a19),a20))+E(f15(x2491,f11(x2492,x2493,x2491)),x2492) % 2.20/2.29 [253]~P1(x2531)+~P1(x2533)+~P1(x2532)+E(x2531,a17)+~P3(x2531,f15(x2532,x2533))+E(x2531,a1)+P1(f11(x2532,x2533,x2531))+P1(f10(x2532,x2533,x2531))+~P4(f13(f13(x2532,x2533),x2531),f13(f13(a18,a19),a20))+E(f15(f9(x2532,x2533,x2531),f12(x2532,x2533,x2531)),x2531) % 2.20/2.29 [255]~P1(x2551)+~P1(x2553)+~P1(x2552)+E(x2551,a17)+~P3(x2551,f15(x2552,x2553))+E(x2551,a1)+E(f15(f9(x2552,x2553,x2551),f12(x2552,x2553,x2551)),x2551)+P1(f10(x2552,x2553,x2551))+~P4(f13(f13(x2552,x2553),x2551),f13(f13(a18,a19),a20))+E(f15(x2551,f11(x2552,x2553,x2551)),x2552) % 2.20/2.29 [256]~P1(x2562)+~P1(x2561)+~P1(x2563)+E(x2561,a17)+~P3(x2561,f15(x2562,x2563))+E(x2561,a1)+E(f15(f9(x2562,x2563,x2561),f12(x2562,x2563,x2561)),x2561)+P1(f11(x2562,x2563,x2561))+~P4(f13(f13(x2562,x2563),x2561),f13(f13(a18,a19),a20))+E(f15(x2561,f10(x2562,x2563,x2561)),x2563) % 2.20/2.29 [257]~P1(x2572)+~P1(x2571)+~P1(x2573)+E(x2571,a17)+~P3(x2571,f15(x2572,x2573))+E(x2571,a1)+E(f15(x2571,f10(x2572,x2573,x2571)),x2573)+E(f15(f9(x2572,x2573,x2571),f12(x2572,x2573,x2571)),x2571)+~P4(f13(f13(x2572,x2573),x2571),f13(f13(a18,a19),a20))+E(f15(x2571,f11(x2572,x2573,x2571)),x2572) % 2.20/2.29 [134]~P1(x1344)+~P1(x1342)+~P1(x1343)+~P1(x1341)+P3(x1341,x1342)+P3(x1341,x1343)+E(x1341,a17)+E(x1341,a1)+~E(f15(x1341,x1344),f15(x1342,x1343))+~E(f9(x1342,x1343,x1341),a17)+~P4(f13(f13(x1342,x1343),x1341),f13(f13(a18,a19),a20)) % 2.20/2.29 [135]~P1(x1354)+~P1(x1352)+~P1(x1353)+~P1(x1351)+P3(x1351,x1352)+P3(x1351,x1353)+E(x1351,a17)+~E(f9(x1352,x1353,x1351),x1351)+E(x1351,a1)+~E(f15(x1351,x1354),f15(x1352,x1353))+~P4(f13(f13(x1352,x1353),x1351),f13(f13(a18,a19),a20)) % 2.20/2.29 [140]~P1(x1404)+~P1(x1402)+~P1(x1403)+~P1(x1401)+P3(x1401,x1402)+P3(x1401,x1403)+E(x1401,a17)+E(x1401,a1)+~E(f15(x1401,x1404),f15(x1402,x1403))+P1(f9(x1402,x1403,x1401))+~P4(f13(f13(x1402,x1403),x1401),f13(f13(a18,a19),a20)) % 2.20/2.29 [141]~P1(x1414)+~P1(x1412)+~P1(x1413)+~P1(x1411)+P3(x1411,x1412)+P3(x1411,x1413)+E(x1411,a17)+E(x1411,a1)+~E(f15(x1411,x1414),f15(x1412,x1413))+P1(f12(x1412,x1413,x1411))+~P4(f13(f13(x1412,x1413),x1411),f13(f13(a18,a19),a20)) % 2.20/2.29 [146]~P1(x1464)+~P1(x1462)+~P1(x1463)+~P1(x1461)+P3(x1461,x1462)+P3(x1461,x1463)+E(x1461,a17)+P3(f9(x1462,x1463,x1461),x1461)+E(x1461,a1)+~E(f15(x1461,x1464),f15(x1462,x1463))+~P4(f13(f13(x1462,x1463),x1461),f13(f13(a18,a19),a20)) % 2.20/2.29 [152]~P1(x1524)+~P1(x1521)+~P1(x1523)+~P1(x1522)+P3(x1521,x1522)+E(x1521,a17)+E(x1521,a1)+~E(f15(x1522,x1523),f15(x1521,x1524))+~E(f9(x1522,x1523,x1521),a17)+P1(f10(x1522,x1523,x1521))+~P4(f13(f13(x1522,x1523),x1521),f13(f13(a18,a19),a20)) % 2.20/2.29 [153]~P1(x1534)+~P1(x1533)+~P1(x1532)+~P1(x1531)+P3(x1531,x1532)+E(x1531,a17)+E(x1531,a1)+~E(f15(x1531,x1534),f15(x1533,x1532))+~E(f9(x1533,x1532,x1531),a17)+P1(f11(x1533,x1532,x1531))+~P4(f13(f13(x1533,x1532),x1531),f13(f13(a18,a19),a20)) % 2.20/2.29 [154]~P1(x1544)+~P1(x1541)+~P1(x1543)+~P1(x1542)+P3(x1541,x1542)+E(x1541,a17)+~E(f9(x1542,x1543,x1541),x1541)+E(x1541,a1)+~E(f15(x1542,x1543),f15(x1541,x1544))+~P4(f13(f13(x1542,x1543),x1541),f13(f13(a18,a19),a20))+P1(f10(x1542,x1543,x1541)) % 2.20/2.29 [155]~P1(x1554)+~P1(x1553)+~P1(x1552)+~P1(x1551)+P3(x1551,x1552)+E(x1551,a17)+~E(f9(x1553,x1552,x1551),x1551)+E(x1551,a1)+~E(f15(x1551,x1554),f15(x1553,x1552))+~P4(f13(f13(x1553,x1552),x1551),f13(f13(a18,a19),a20))+P1(f11(x1553,x1552,x1551)) % 2.20/2.29 [156]P3(x1561,x1562)+~P1(x1564)+~P1(x1562)+~P1(x1561)+~P1(x1563)+E(x1561,a17)+E(x1561,a1)+~E(f15(x1561,x1564),f15(x1562,x1563))+~E(f9(x1562,x1563,x1561),a17)+~P4(f13(f13(x1562,x1563),x1561),f13(f13(a18,a19),a20))+E(f15(x1561,f10(x1562,x1563,x1561)),x1563) % 2.20/2.29 [157]P3(x1571,x1573)+~P1(x1574)+~P1(x1572)+~P1(x1573)+~P1(x1571)+E(x1571,a17)+E(x1571,a1)+~E(f15(x1571,x1574),f15(x1572,x1573))+~E(f9(x1572,x1573,x1571),a17)+~P4(f13(f13(x1572,x1573),x1571),f13(f13(a18,a19),a20))+E(f15(x1571,f11(x1572,x1573,x1571)),x1572) % 2.20/2.29 [158]P3(x1581,x1582)+~P1(x1584)+~P1(x1582)+~P1(x1581)+~P1(x1583)+E(x1581,a17)+~E(f9(x1582,x1583,x1581),x1581)+E(x1581,a1)+~E(f15(x1581,x1584),f15(x1582,x1583))+~P4(f13(f13(x1582,x1583),x1581),f13(f13(a18,a19),a20))+E(f15(x1581,f10(x1582,x1583,x1581)),x1583) % 2.20/2.29 [159]P3(x1591,x1593)+~P1(x1594)+~P1(x1592)+~P1(x1593)+~P1(x1591)+E(x1591,a17)+~E(f9(x1592,x1593,x1591),x1591)+E(x1591,a1)+~E(f15(x1591,x1594),f15(x1592,x1593))+~P4(f13(f13(x1592,x1593),x1591),f13(f13(a18,a19),a20))+E(f15(x1591,f11(x1592,x1593,x1591)),x1592) % 2.20/2.29 [169]~P1(x1694)+~P1(x1691)+~P1(x1693)+~P1(x1692)+P3(x1691,x1692)+E(x1691,a17)+E(x1691,a1)+~E(f15(x1692,x1693),f15(x1691,x1694))+P1(f10(x1692,x1693,x1691))+~P4(f13(f13(x1692,x1693),x1691),f13(f13(a18,a19),a20))+P1(f9(x1692,x1693,x1691)) % 2.20/2.29 [170]~P1(x1704)+~P1(x1701)+~P1(x1703)+~P1(x1702)+P3(x1701,x1702)+E(x1701,a17)+E(x1701,a1)+~E(f15(x1702,x1703),f15(x1701,x1704))+P1(f10(x1702,x1703,x1701))+~P4(f13(f13(x1702,x1703),x1701),f13(f13(a18,a19),a20))+P1(f12(x1702,x1703,x1701)) % 2.20/2.29 [171]~P1(x1714)+~P1(x1713)+~P1(x1712)+~P1(x1711)+P3(x1711,x1712)+E(x1711,a17)+E(x1711,a1)+~E(f15(x1711,x1714),f15(x1713,x1712))+P1(f11(x1713,x1712,x1711))+~P4(f13(f13(x1713,x1712),x1711),f13(f13(a18,a19),a20))+P1(f9(x1713,x1712,x1711)) % 2.20/2.29 [172]~P1(x1724)+~P1(x1723)+~P1(x1722)+~P1(x1721)+P3(x1721,x1722)+E(x1721,a17)+E(x1721,a1)+~E(f15(x1721,x1724),f15(x1723,x1722))+P1(f11(x1723,x1722,x1721))+~P4(f13(f13(x1723,x1722),x1721),f13(f13(a18,a19),a20))+P1(f12(x1723,x1722,x1721)) % 2.20/2.29 [176]~P1(x1764)+~P1(x1761)+~P1(x1763)+~P1(x1762)+P3(x1761,x1762)+E(x1761,a17)+P3(f9(x1762,x1763,x1761),x1761)+E(x1761,a1)+~E(f15(x1762,x1763),f15(x1761,x1764))+~P4(f13(f13(x1762,x1763),x1761),f13(f13(a18,a19),a20))+P1(f10(x1762,x1763,x1761)) % 2.20/2.29 [177]~P1(x1774)+~P1(x1773)+~P1(x1772)+~P1(x1771)+P3(x1771,x1772)+E(x1771,a17)+P3(f9(x1773,x1772,x1771),x1771)+E(x1771,a1)+~E(f15(x1771,x1774),f15(x1773,x1772))+~P4(f13(f13(x1773,x1772),x1771),f13(f13(a18,a19),a20))+P1(f11(x1773,x1772,x1771)) % 2.20/2.29 [178]P3(x1781,x1782)+~P1(x1784)+~P1(x1782)+~P1(x1781)+~P1(x1783)+E(x1781,a17)+E(x1781,a1)+~E(f15(x1781,x1784),f15(x1782,x1783))+P1(f9(x1782,x1783,x1781))+~P4(f13(f13(x1782,x1783),x1781),f13(f13(a18,a19),a20))+E(f15(x1781,f10(x1782,x1783,x1781)),x1783) % 2.20/2.29 [179]P3(x1791,x1792)+~P1(x1794)+~P1(x1792)+~P1(x1791)+~P1(x1793)+E(x1791,a17)+E(x1791,a1)+~E(f15(x1791,x1794),f15(x1792,x1793))+P1(f12(x1792,x1793,x1791))+~P4(f13(f13(x1792,x1793),x1791),f13(f13(a18,a19),a20))+E(f15(x1791,f10(x1792,x1793,x1791)),x1793) % 2.20/2.29 [180]P3(x1801,x1803)+~P1(x1804)+~P1(x1802)+~P1(x1803)+~P1(x1801)+E(x1801,a17)+E(x1801,a1)+~E(f15(x1801,x1804),f15(x1802,x1803))+P1(f9(x1802,x1803,x1801))+~P4(f13(f13(x1802,x1803),x1801),f13(f13(a18,a19),a20))+E(f15(x1801,f11(x1802,x1803,x1801)),x1802) % 2.20/2.29 [181]P3(x1811,x1813)+~P1(x1814)+~P1(x1812)+~P1(x1813)+~P1(x1811)+E(x1811,a17)+E(x1811,a1)+~E(f15(x1811,x1814),f15(x1812,x1813))+P1(f12(x1812,x1813,x1811))+~P4(f13(f13(x1812,x1813),x1811),f13(f13(a18,a19),a20))+E(f15(x1811,f11(x1812,x1813,x1811)),x1812) % 2.20/2.29 [189]P3(x1891,x1892)+~P1(x1894)+~P1(x1892)+~P1(x1891)+~P1(x1893)+E(x1891,a17)+P3(f9(x1892,x1893,x1891),x1891)+E(x1891,a1)+~E(f15(x1891,x1894),f15(x1892,x1893))+~P4(f13(f13(x1892,x1893),x1891),f13(f13(a18,a19),a20))+E(f15(x1891,f10(x1892,x1893,x1891)),x1893) % 2.20/2.29 [190]P3(x1901,x1903)+~P1(x1904)+~P1(x1902)+~P1(x1903)+~P1(x1901)+E(x1901,a17)+P3(f9(x1902,x1903,x1901),x1901)+E(x1901,a1)+~E(f15(x1901,x1904),f15(x1902,x1903))+~P4(f13(f13(x1902,x1903),x1901),f13(f13(a18,a19),a20))+E(f15(x1901,f11(x1902,x1903,x1901)),x1902) % 2.20/2.29 [191]P3(x1911,x1912)+P3(x1911,x1913)+~P1(x1914)+~P1(x1912)+~P1(x1913)+~P1(x1911)+E(x1911,a17)+E(x1911,a1)+~E(f15(x1911,x1914),f15(x1912,x1913))+~P4(f13(f13(x1912,x1913),x1911),f13(f13(a18,a19),a20))+E(f15(f9(x1912,x1913,x1911),f12(x1912,x1913,x1911)),x1911) % 2.20/2.29 [202]~P1(x2024)+~P1(x2021)+~P1(x2023)+~P1(x2022)+E(x2021,a17)+E(x2021,a1)+~E(f15(x2022,x2023),f15(x2021,x2024))+P1(f10(x2022,x2023,x2021))+~E(f9(x2022,x2023,x2021),a17)+~P4(f13(f13(x2022,x2023),x2021),f13(f13(a18,a19),a20))+P1(f11(x2022,x2023,x2021)) % 2.20/2.29 [203]~P1(x2034)+~P1(x2031)+~P1(x2033)+~P1(x2032)+E(x2031,a17)+~E(f9(x2032,x2033,x2031),x2031)+E(x2031,a1)+~E(f15(x2032,x2033),f15(x2031,x2034))+P1(f10(x2032,x2033,x2031))+~P4(f13(f13(x2032,x2033),x2031),f13(f13(a18,a19),a20))+P1(f11(x2032,x2033,x2031)) % 2.20/2.29 [204]~P1(x2044)+~P1(x2041)+~P1(x2043)+~P1(x2042)+E(x2041,a17)+E(x2041,a1)+~E(f15(x2042,x2043),f15(x2041,x2044))+P1(f10(x2042,x2043,x2041))+~E(f9(x2042,x2043,x2041),a17)+~P4(f13(f13(x2042,x2043),x2041),f13(f13(a18,a19),a20))+E(f15(x2041,f11(x2042,x2043,x2041)),x2042) % 2.20/2.29 [205]~P1(x2054)+~P1(x2052)+~P1(x2051)+~P1(x2053)+E(x2051,a17)+E(x2051,a1)+~E(f15(x2051,x2054),f15(x2052,x2053))+P1(f11(x2052,x2053,x2051))+~E(f9(x2052,x2053,x2051),a17)+~P4(f13(f13(x2052,x2053),x2051),f13(f13(a18,a19),a20))+E(f15(x2051,f10(x2052,x2053,x2051)),x2053) % 2.20/2.29 [206]~P1(x2064)+~P1(x2061)+~P1(x2063)+~P1(x2062)+E(x2061,a17)+~E(f9(x2062,x2063,x2061),x2061)+E(x2061,a1)+~E(f15(x2062,x2063),f15(x2061,x2064))+P1(f10(x2062,x2063,x2061))+~P4(f13(f13(x2062,x2063),x2061),f13(f13(a18,a19),a20))+E(f15(x2061,f11(x2062,x2063,x2061)),x2062) % 2.20/2.29 [207]~P1(x2074)+~P1(x2072)+~P1(x2071)+~P1(x2073)+E(x2071,a17)+~E(f9(x2072,x2073,x2071),x2071)+E(x2071,a1)+~E(f15(x2071,x2074),f15(x2072,x2073))+P1(f11(x2072,x2073,x2071))+~P4(f13(f13(x2072,x2073),x2071),f13(f13(a18,a19),a20))+E(f15(x2071,f10(x2072,x2073,x2071)),x2073) % 2.20/2.29 [210]~P1(x2104)+~P1(x2102)+~P1(x2101)+~P1(x2103)+E(x2101,a17)+E(x2101,a1)+~E(f15(x2101,x2104),f15(x2102,x2103))+E(f15(x2101,f10(x2102,x2103,x2101)),x2103)+~E(f9(x2102,x2103,x2101),a17)+~P4(f13(f13(x2102,x2103),x2101),f13(f13(a18,a19),a20))+E(f15(x2101,f11(x2102,x2103,x2101)),x2102) % 2.20/2.29 [211]~P1(x2114)+~P1(x2112)+~P1(x2111)+~P1(x2113)+E(x2111,a17)+~E(f9(x2112,x2113,x2111),x2111)+E(x2111,a1)+~E(f15(x2111,x2114),f15(x2112,x2113))+E(f15(x2111,f10(x2112,x2113,x2111)),x2113)+~P4(f13(f13(x2112,x2113),x2111),f13(f13(a18,a19),a20))+E(f15(x2111,f11(x2112,x2113,x2111)),x2112) % 2.20/2.29 [216]~P1(x2164)+~P1(x2161)+~P1(x2163)+~P1(x2162)+E(x2161,a17)+E(x2161,a1)+~E(f15(x2162,x2163),f15(x2161,x2164))+P1(f11(x2162,x2163,x2161))+P1(f10(x2162,x2163,x2161))+~P4(f13(f13(x2162,x2163),x2161),f13(f13(a18,a19),a20))+P1(f9(x2162,x2163,x2161)) % 2.20/2.29 [217]~P1(x2174)+~P1(x2171)+~P1(x2173)+~P1(x2172)+E(x2171,a17)+E(x2171,a1)+~E(f15(x2172,x2173),f15(x2171,x2174))+P1(f11(x2172,x2173,x2171))+P1(f10(x2172,x2173,x2171))+~P4(f13(f13(x2172,x2173),x2171),f13(f13(a18,a19),a20))+P1(f12(x2172,x2173,x2171)) % 2.20/2.29 [220]~P1(x2204)+~P1(x2201)+~P1(x2203)+~P1(x2202)+E(x2201,a17)+P3(f9(x2202,x2203,x2201),x2201)+E(x2201,a1)+~E(f15(x2202,x2203),f15(x2201,x2204))+P1(f10(x2202,x2203,x2201))+~P4(f13(f13(x2202,x2203),x2201),f13(f13(a18,a19),a20))+P1(f11(x2202,x2203,x2201)) % 2.20/2.29 [221]~P1(x2214)+~P1(x2211)+~P1(x2213)+~P1(x2212)+E(x2211,a17)+E(x2211,a1)+~E(f15(x2212,x2213),f15(x2211,x2214))+P1(f9(x2212,x2213,x2211))+P1(f10(x2212,x2213,x2211))+~P4(f13(f13(x2212,x2213),x2211),f13(f13(a18,a19),a20))+E(f15(x2211,f11(x2212,x2213,x2211)),x2212) % 2.20/2.29 [222]~P1(x2224)+~P1(x2221)+~P1(x2223)+~P1(x2222)+E(x2221,a17)+E(x2221,a1)+~E(f15(x2222,x2223),f15(x2221,x2224))+P1(f12(x2222,x2223,x2221))+P1(f10(x2222,x2223,x2221))+~P4(f13(f13(x2222,x2223),x2221),f13(f13(a18,a19),a20))+E(f15(x2221,f11(x2222,x2223,x2221)),x2222) % 2.20/2.29 [223]~P1(x2234)+~P1(x2232)+~P1(x2231)+~P1(x2233)+E(x2231,a17)+E(x2231,a1)+~E(f15(x2231,x2234),f15(x2232,x2233))+P1(f9(x2232,x2233,x2231))+P1(f11(x2232,x2233,x2231))+~P4(f13(f13(x2232,x2233),x2231),f13(f13(a18,a19),a20))+E(f15(x2231,f10(x2232,x2233,x2231)),x2233) % 2.20/2.29 [224]~P1(x2244)+~P1(x2242)+~P1(x2241)+~P1(x2243)+E(x2241,a17)+E(x2241,a1)+~E(f15(x2241,x2244),f15(x2242,x2243))+P1(f12(x2242,x2243,x2241))+P1(f11(x2242,x2243,x2241))+~P4(f13(f13(x2242,x2243),x2241),f13(f13(a18,a19),a20))+E(f15(x2241,f10(x2242,x2243,x2241)),x2243) % 2.20/2.29 [227]~P1(x2274)+~P1(x2271)+~P1(x2273)+~P1(x2272)+E(x2271,a17)+P3(f9(x2272,x2273,x2271),x2271)+E(x2271,a1)+~E(f15(x2272,x2273),f15(x2271,x2274))+P1(f10(x2272,x2273,x2271))+~P4(f13(f13(x2272,x2273),x2271),f13(f13(a18,a19),a20))+E(f15(x2271,f11(x2272,x2273,x2271)),x2272) % 2.20/2.29 [228]~P1(x2284)+~P1(x2282)+~P1(x2281)+~P1(x2283)+E(x2281,a17)+P3(f9(x2282,x2283,x2281),x2281)+E(x2281,a1)+~E(f15(x2281,x2284),f15(x2282,x2283))+P1(f11(x2282,x2283,x2281))+~P4(f13(f13(x2282,x2283),x2281),f13(f13(a18,a19),a20))+E(f15(x2281,f10(x2282,x2283,x2281)),x2283) % 2.20/2.29 [229]P3(x2291,x2292)+~P1(x2294)+~P1(x2291)+~P1(x2293)+~P1(x2292)+E(x2291,a17)+E(x2291,a1)+~E(f15(x2292,x2293),f15(x2291,x2294))+P1(f10(x2292,x2293,x2291))+~P4(f13(f13(x2292,x2293),x2291),f13(f13(a18,a19),a20))+E(f15(f9(x2292,x2293,x2291),f12(x2292,x2293,x2291)),x2291) % 2.20/2.29 [230]P3(x2301,x2303)+~P1(x2304)+~P1(x2302)+~P1(x2303)+~P1(x2301)+E(x2301,a17)+E(x2301,a1)+~E(f15(x2301,x2304),f15(x2302,x2303))+P1(f11(x2302,x2303,x2301))+~P4(f13(f13(x2302,x2303),x2301),f13(f13(a18,a19),a20))+E(f15(f9(x2302,x2303,x2301),f12(x2302,x2303,x2301)),x2301) % 2.20/2.29 [231]~P1(x2314)+~P1(x2312)+~P1(x2311)+~P1(x2313)+E(x2311,a17)+E(x2311,a1)+~E(f15(x2311,x2314),f15(x2312,x2313))+E(f15(x2311,f10(x2312,x2313,x2311)),x2313)+P1(f9(x2312,x2313,x2311))+~P4(f13(f13(x2312,x2313),x2311),f13(f13(a18,a19),a20))+E(f15(x2311,f11(x2312,x2313,x2311)),x2312) % 2.20/2.29 [232]~P1(x2324)+~P1(x2322)+~P1(x2321)+~P1(x2323)+E(x2321,a17)+E(x2321,a1)+~E(f15(x2321,x2324),f15(x2322,x2323))+E(f15(x2321,f10(x2322,x2323,x2321)),x2323)+P1(f12(x2322,x2323,x2321))+~P4(f13(f13(x2322,x2323),x2321),f13(f13(a18,a19),a20))+E(f15(x2321,f11(x2322,x2323,x2321)),x2322) % 2.20/2.29 [238]~P1(x2384)+~P1(x2382)+~P1(x2381)+~P1(x2383)+E(x2381,a17)+P3(f9(x2382,x2383,x2381),x2381)+E(x2381,a1)+~E(f15(x2381,x2384),f15(x2382,x2383))+E(f15(x2381,f10(x2382,x2383,x2381)),x2383)+~P4(f13(f13(x2382,x2383),x2381),f13(f13(a18,a19),a20))+E(f15(x2381,f11(x2382,x2383,x2381)),x2382) % 2.20/2.29 [239]P3(x2391,x2392)+~P1(x2394)+~P1(x2392)+~P1(x2391)+~P1(x2393)+E(x2391,a17)+E(x2391,a1)+~E(f15(x2391,x2394),f15(x2392,x2393))+E(f15(f9(x2392,x2393,x2391),f12(x2392,x2393,x2391)),x2391)+~P4(f13(f13(x2392,x2393),x2391),f13(f13(a18,a19),a20))+E(f15(x2391,f10(x2392,x2393,x2391)),x2393) % 2.20/2.29 [240]P3(x2401,x2403)+~P1(x2404)+~P1(x2402)+~P1(x2403)+~P1(x2401)+E(x2401,a17)+E(x2401,a1)+~E(f15(x2401,x2404),f15(x2402,x2403))+E(f15(f9(x2402,x2403,x2401),f12(x2402,x2403,x2401)),x2401)+~P4(f13(f13(x2402,x2403),x2401),f13(f13(a18,a19),a20))+E(f15(x2401,f11(x2402,x2403,x2401)),x2402) % 2.20/2.29 [250]~P1(x2504)+~P1(x2501)+~P1(x2503)+~P1(x2502)+E(x2501,a17)+E(x2501,a1)+~E(f15(x2502,x2503),f15(x2501,x2504))+P1(f11(x2502,x2503,x2501))+P1(f10(x2502,x2503,x2501))+~P4(f13(f13(x2502,x2503),x2501),f13(f13(a18,a19),a20))+E(f15(f9(x2502,x2503,x2501),f12(x2502,x2503,x2501)),x2501) % 2.20/2.29 [251]~P1(x2514)+~P1(x2511)+~P1(x2513)+~P1(x2512)+E(x2511,a17)+E(x2511,a1)+~E(f15(x2512,x2513),f15(x2511,x2514))+E(f15(f9(x2512,x2513,x2511),f12(x2512,x2513,x2511)),x2511)+P1(f10(x2512,x2513,x2511))+~P4(f13(f13(x2512,x2513),x2511),f13(f13(a18,a19),a20))+E(f15(x2511,f11(x2512,x2513,x2511)),x2512) % 2.20/2.29 [252]~P1(x2524)+~P1(x2522)+~P1(x2521)+~P1(x2523)+E(x2521,a17)+E(x2521,a1)+~E(f15(x2521,x2524),f15(x2522,x2523))+E(f15(f9(x2522,x2523,x2521),f12(x2522,x2523,x2521)),x2521)+P1(f11(x2522,x2523,x2521))+~P4(f13(f13(x2522,x2523),x2521),f13(f13(a18,a19),a20))+E(f15(x2521,f10(x2522,x2523,x2521)),x2523) % 2.20/2.29 [254]~P1(x2544)+~P1(x2542)+~P1(x2541)+~P1(x2543)+E(x2541,a17)+E(x2541,a1)+~E(f15(x2541,x2544),f15(x2542,x2543))+E(f15(x2541,f10(x2542,x2543,x2541)),x2543)+E(f15(f9(x2542,x2543,x2541),f12(x2542,x2543,x2541)),x2541)+~P4(f13(f13(x2542,x2543),x2541),f13(f13(a18,a19),a20))+E(f15(x2541,f11(x2542,x2543,x2541)),x2542) % 2.20/2.29 %EqnAxiom % 2.20/2.29 [1]E(x11,x11) % 2.20/2.29 [2]E(x22,x21)+~E(x21,x22) % 2.20/2.29 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 2.20/2.29 [4]~E(x41,x42)+E(f13(x41,x43),f13(x42,x43)) % 2.20/2.29 [5]~E(x51,x52)+E(f13(x53,x51),f13(x53,x52)) % 2.20/2.29 [6]~E(x61,x62)+E(f14(x61,x63),f14(x62,x63)) % 2.20/2.29 [7]~E(x71,x72)+E(f14(x73,x71),f14(x73,x72)) % 2.20/2.29 [8]~E(x81,x82)+E(f15(x81,x83),f15(x82,x83)) % 2.20/2.29 [9]~E(x91,x92)+E(f15(x93,x91),f15(x93,x92)) % 2.20/2.29 [10]~E(x101,x102)+E(f9(x101,x103,x104),f9(x102,x103,x104)) % 2.20/2.29 [11]~E(x111,x112)+E(f9(x113,x111,x114),f9(x113,x112,x114)) % 2.20/2.29 [12]~E(x121,x122)+E(f9(x123,x124,x121),f9(x123,x124,x122)) % 2.20/2.29 [13]~E(x131,x132)+E(f12(x131,x133,x134),f12(x132,x133,x134)) % 2.20/2.29 [14]~E(x141,x142)+E(f12(x143,x141,x144),f12(x143,x142,x144)) % 2.20/2.29 [15]~E(x151,x152)+E(f12(x153,x154,x151),f12(x153,x154,x152)) % 2.20/2.29 [16]~E(x161,x162)+E(f10(x161,x163,x164),f10(x162,x163,x164)) % 2.20/2.29 [17]~E(x171,x172)+E(f10(x173,x171,x174),f10(x173,x172,x174)) % 2.20/2.29 [18]~E(x181,x182)+E(f10(x183,x184,x181),f10(x183,x184,x182)) % 2.20/2.29 [19]~E(x191,x192)+E(f11(x191,x193,x194),f11(x192,x193,x194)) % 2.20/2.29 [20]~E(x201,x202)+E(f11(x203,x201,x204),f11(x203,x202,x204)) % 2.20/2.29 [21]~E(x211,x212)+E(f11(x213,x214,x211),f11(x213,x214,x212)) % 2.20/2.29 [22]~E(x221,x222)+E(f16(x221,x223),f16(x222,x223)) % 2.20/2.29 [23]~E(x231,x232)+E(f16(x233,x231),f16(x233,x232)) % 2.20/2.29 [24]~E(x241,x242)+E(f5(x241),f5(x242)) % 2.20/2.29 [25]~E(x251,x252)+E(f6(x251),f6(x252)) % 2.20/2.29 [26]~E(x261,x262)+E(f7(x261,x263),f7(x262,x263)) % 2.20/2.29 [27]~E(x271,x272)+E(f7(x273,x271),f7(x273,x272)) % 2.20/2.29 [28]~E(x281,x282)+E(f8(x281,x283),f8(x282,x283)) % 2.20/2.29 [29]~E(x291,x292)+E(f8(x293,x291),f8(x293,x292)) % 2.20/2.29 [30]~P1(x301)+P1(x302)+~E(x301,x302) % 2.20/2.29 [31]P4(x312,x313)+~E(x311,x312)+~P4(x311,x313) % 2.20/2.29 [32]P4(x323,x322)+~E(x321,x322)+~P4(x323,x321) % 2.20/2.29 [33]P3(x332,x333)+~E(x331,x332)+~P3(x331,x333) % 2.20/2.29 [34]P3(x343,x342)+~E(x341,x342)+~P3(x343,x341) % 2.20/2.29 [35]~P2(x351)+P2(x352)+~E(x351,x352) % 2.20/2.29 [36]P5(x362,x363)+~E(x361,x362)+~P5(x361,x363) % 2.20/2.29 [37]P5(x373,x372)+~E(x371,x372)+~P5(x373,x371) % 2.20/2.29 % 2.20/2.29 %------------------------------------------- % 2.20/2.29 cnf(261,plain, % 2.20/2.29 (~P1(a19)), % 2.20/2.29 inference(equality_inference,[],[91])). % 2.20/2.29 cnf(319,plain, % 2.20/2.29 ($false), % 2.20/2.29 inference(scs_inference,[],[261,41]), % 2.20/2.29 ['proof']). % 2.20/2.29 % SZS output end Proof % 2.20/2.29 % Total time :1.110000s %------------------------------------------------------------------------------