%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM514+3 : 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 : n027.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:46 EDT 2024 % Result : Theorem 2.03s 2.16s % Output : CNFRefutation 2.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.07 % Problem : NUM514+3 : TPTP v8.2.0. Released v4.0.0. % 0.02/0.07 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.06/0.25 % Computer : n027.cluster.edu % 0.06/0.25 % Model : x86_64 x86_64 % 0.06/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.25 % Memory : 8042.1875MB % 0.06/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.25 % CPULimit : 300 % 0.06/0.25 % WCLimit : 300 % 0.06/0.25 % DateTime : Sun Jun 23 02:24:38 EDT 2024 % 0.06/0.26 % CPUTime : % 0.11/0.42 start to proof:theBenchmark % 2.03/2.14 %------------------------------------------- % 2.03/2.14 % File :CSE---1.7 % 2.03/2.14 % Problem :theBenchmark % 2.03/2.14 % Transform :cnf % 2.03/2.14 % Format :tptp:raw % 2.03/2.14 % Command :java -jar mcs_scs.jar %d %s % 2.03/2.14 % 2.03/2.14 % Result :Theorem 1.130000s % 2.03/2.14 % Output :CNFRefutation 1.130000s % 2.03/2.14 %------------------------------------------- % 2.03/2.14 %------------------------------------------------------------------------------ % 2.03/2.14 % File : NUM514+3 : TPTP v8.2.0. Released v4.0.0. % 2.03/2.14 % Domain : Number Theory % 2.03/2.14 % Problem : Square root of a prime is irrational 14_03_03_05_02_03, 02 exp % 2.03/2.14 % Version : Especial. % 2.03/2.14 % English : % 2.03/2.14 % 2.03/2.14 % Refs : [LPV06] Lyaletski et al. (2006), SAD as a Mathematical Assista % 2.03/2.14 % : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 2.03/2.14 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 2.03/2.14 % Source : [Pas08] % 2.03/2.14 % Names : primes_14_03_03_05_02_03.02 [Pas08] % 2.03/2.14 % 2.03/2.14 % Status : Theorem % 2.03/2.14 % Rating : 0.11 v8.1.0, 0.06 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.12 v6.3.0, 0.08 v6.1.0, 0.13 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.33 v5.2.0, 0.30 v5.1.0, 0.43 v5.0.0, 0.38 v4.1.0, 0.43 v4.0.1, 0.74 v4.0.0 % 2.03/2.14 % Syntax : Number of formulae : 56 ( 1 unt; 5 def) % 2.03/2.14 % Number of atoms : 296 ( 108 equ) % 2.03/2.14 % Maximal formula atoms : 22 ( 5 avg) % 2.03/2.14 % Number of connectives : 275 ( 35 ~; 20 |; 148 &) % 2.03/2.14 % ( 5 <=>; 67 =>; 0 <=; 0 <~>) % 2.03/2.14 % Maximal formula depth : 16 ( 6 avg) % 2.03/2.14 % Maximal term depth : 4 ( 1 avg) % 2.03/2.14 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 2.03/2.14 % Number of functors : 11 ( 11 usr; 7 con; 0-2 aty) % 2.03/2.14 % Number of variables : 108 ( 85 !; 23 ?) % 2.03/2.14 % SPC : FOF_THM_RFO_SEQ % 2.03/2.14 % 2.03/2.14 % Comments : Problem generated by the SAD system [VLP07] % 2.03/2.14 %------------------------------------------------------------------------------ % 2.03/2.14 fof(mNatSort,axiom, % 2.03/2.14 ! [W0] : % 2.03/2.14 ( aNaturalNumber0(W0) % 2.03/2.14 => $true ) ). % 2.03/2.14 % 2.03/2.14 fof(mSortsC,axiom, % 2.03/2.14 aNaturalNumber0(sz00) ). % 2.03/2.14 % 2.03/2.14 fof(mSortsC_01,axiom, % 2.03/2.14 ( aNaturalNumber0(sz10) % 2.03/2.14 & sz10 != sz00 ) ). % 2.03/2.14 % 2.03/2.14 fof(mSortsB,axiom, % 2.03/2.14 ! [W0,W1] : % 2.03/2.14 ( ( aNaturalNumber0(W0) % 2.03/2.14 & aNaturalNumber0(W1) ) % 2.03/2.14 => aNaturalNumber0(sdtpldt0(W0,W1)) ) ). % 2.03/2.14 % 2.03/2.14 fof(mSortsB_02,axiom, % 2.03/2.14 ! [W0,W1] : % 2.03/2.14 ( ( aNaturalNumber0(W0) % 2.03/2.14 & aNaturalNumber0(W1) ) % 2.03/2.14 => aNaturalNumber0(sdtasdt0(W0,W1)) ) ). % 2.03/2.14 % 2.03/2.14 fof(mAddComm,axiom, % 2.03/2.14 ! [W0,W1] : % 2.03/2.14 ( ( aNaturalNumber0(W0) % 2.03/2.14 & aNaturalNumber0(W1) ) % 2.03/2.14 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 2.03/2.14 % 2.03/2.14 fof(mAddAsso,axiom, % 2.03/2.14 ! [W0,W1,W2] : % 2.03/2.14 ( ( aNaturalNumber0(W0) % 2.03/2.14 & aNaturalNumber0(W1) % 2.03/2.14 & aNaturalNumber0(W2) ) % 2.03/2.14 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 2.03/2.14 % 2.03/2.14 fof(m_AddZero,axiom, % 2.03/2.14 ! [W0] : % 2.03/2.14 ( aNaturalNumber0(W0) % 2.03/2.14 => ( sdtpldt0(W0,sz00) = W0 % 2.03/2.14 & W0 = sdtpldt0(sz00,W0) ) ) ). % 2.03/2.14 % 2.03/2.14 fof(mMulComm,axiom, % 2.03/2.14 ! [W0,W1] : % 2.03/2.14 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 2.03/2.15 % 2.03/2.15 fof(mMulAsso,axiom, % 2.03/2.15 ! [W0,W1,W2] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) % 2.03/2.15 & aNaturalNumber0(W2) ) % 2.03/2.15 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 2.03/2.15 % 2.03/2.15 fof(m_MulUnit,axiom, % 2.03/2.15 ! [W0] : % 2.03/2.15 ( aNaturalNumber0(W0) % 2.03/2.15 => ( sdtasdt0(W0,sz10) = W0 % 2.03/2.15 & W0 = sdtasdt0(sz10,W0) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(m_MulZero,axiom, % 2.03/2.15 ! [W0] : % 2.03/2.15 ( aNaturalNumber0(W0) % 2.03/2.15 => ( sdtasdt0(W0,sz00) = sz00 % 2.03/2.15 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mAMDistr,axiom, % 2.03/2.15 ! [W0,W1,W2] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) % 2.03/2.15 & aNaturalNumber0(W2) ) % 2.03/2.15 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 2.03/2.15 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mAddCanc,axiom, % 2.03/2.15 ! [W0,W1,W2] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) % 2.03/2.15 & aNaturalNumber0(W2) ) % 2.03/2.15 => ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2) % 2.03/2.15 | sdtpldt0(W1,W0) = sdtpldt0(W2,W0) ) % 2.03/2.15 => W1 = W2 ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mMulCanc,axiom, % 2.03/2.15 ! [W0] : % 2.03/2.15 ( aNaturalNumber0(W0) % 2.03/2.15 => ( W0 != sz00 % 2.03/2.15 => ! [W1,W2] : % 2.03/2.15 ( ( aNaturalNumber0(W1) % 2.03/2.15 & aNaturalNumber0(W2) ) % 2.03/2.15 => ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2) % 2.03/2.15 | sdtasdt0(W1,W0) = sdtasdt0(W2,W0) ) % 2.03/2.15 => W1 = W2 ) ) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mZeroAdd,axiom, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( sdtpldt0(W0,W1) = sz00 % 2.03/2.15 => ( W0 = sz00 % 2.03/2.15 & W1 = sz00 ) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mZeroMul,axiom, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( sdtasdt0(W0,W1) = sz00 % 2.03/2.15 => ( W0 = sz00 % 2.03/2.15 | W1 = sz00 ) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mDefLE,definition, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( sdtlseqdt0(W0,W1) % 2.03/2.15 <=> ? [W2] : % 2.03/2.15 ( aNaturalNumber0(W2) % 2.03/2.15 & sdtpldt0(W0,W2) = W1 ) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mDefDiff,definition, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( sdtlseqdt0(W0,W1) % 2.03/2.15 => ! [W2] : % 2.03/2.15 ( W2 = sdtmndt0(W1,W0) % 2.03/2.15 <=> ( aNaturalNumber0(W2) % 2.03/2.15 & sdtpldt0(W0,W2) = W1 ) ) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mLERefl,axiom, % 2.03/2.15 ! [W0] : % 2.03/2.15 ( aNaturalNumber0(W0) % 2.03/2.15 => sdtlseqdt0(W0,W0) ) ). % 2.03/2.15 % 2.03/2.15 fof(mLEAsym,axiom, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( ( sdtlseqdt0(W0,W1) % 2.03/2.15 & sdtlseqdt0(W1,W0) ) % 2.03/2.15 => W0 = W1 ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mLETran,axiom, % 2.03/2.15 ! [W0,W1,W2] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) % 2.03/2.15 & aNaturalNumber0(W2) ) % 2.03/2.15 => ( ( sdtlseqdt0(W0,W1) % 2.03/2.15 & sdtlseqdt0(W1,W2) ) % 2.03/2.15 => sdtlseqdt0(W0,W2) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mLETotal,axiom, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( sdtlseqdt0(W0,W1) % 2.03/2.15 | ( W1 != W0 % 2.03/2.15 & sdtlseqdt0(W1,W0) ) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mMonAdd,axiom, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( ( W0 != W1 % 2.03/2.15 & sdtlseqdt0(W0,W1) ) % 2.03/2.15 => ! [W2] : % 2.03/2.15 ( aNaturalNumber0(W2) % 2.03/2.15 => ( sdtpldt0(W2,W0) != sdtpldt0(W2,W1) % 2.03/2.15 & sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1)) % 2.03/2.15 & sdtpldt0(W0,W2) != sdtpldt0(W1,W2) % 2.03/2.15 & sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2)) ) ) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mMonMul,axiom, % 2.03/2.15 ! [W0,W1,W2] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) % 2.03/2.15 & aNaturalNumber0(W2) ) % 2.03/2.15 => ( ( W0 != sz00 % 2.03/2.15 & W1 != W2 % 2.03/2.15 & sdtlseqdt0(W1,W2) ) % 2.03/2.15 => ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2) % 2.03/2.15 & sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 2.03/2.15 & sdtasdt0(W1,W0) != sdtasdt0(W2,W0) % 2.03/2.15 & sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mLENTr,axiom, % 2.03/2.15 ! [W0] : % 2.03/2.15 ( aNaturalNumber0(W0) % 2.03/2.15 => ( W0 = sz00 % 2.03/2.15 | W0 = sz10 % 2.03/2.15 | ( sz10 != W0 % 2.03/2.15 & sdtlseqdt0(sz10,W0) ) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mMonMul2,axiom, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( W0 != sz00 % 2.03/2.15 => sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mIH,axiom, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( iLess0(W0,W1) % 2.03/2.15 => $true ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mIH_03,axiom, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( ( W0 != W1 % 2.03/2.15 & sdtlseqdt0(W0,W1) ) % 2.03/2.15 => iLess0(W0,W1) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mDefDiv,definition, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( doDivides0(W0,W1) % 2.03/2.15 <=> ? [W2] : % 2.03/2.15 ( aNaturalNumber0(W2) % 2.03/2.15 & W1 = sdtasdt0(W0,W2) ) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mDefQuot,definition, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( ( W0 != sz00 % 2.03/2.15 & doDivides0(W0,W1) ) % 2.03/2.15 => ! [W2] : % 2.03/2.15 ( W2 = sdtsldt0(W1,W0) % 2.03/2.15 <=> ( aNaturalNumber0(W2) % 2.03/2.15 & W1 = sdtasdt0(W0,W2) ) ) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mDivTrans,axiom, % 2.03/2.15 ! [W0,W1,W2] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) % 2.03/2.15 & aNaturalNumber0(W2) ) % 2.03/2.15 => ( ( doDivides0(W0,W1) % 2.03/2.15 & doDivides0(W1,W2) ) % 2.03/2.15 => doDivides0(W0,W2) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mDivSum,axiom, % 2.03/2.15 ! [W0,W1,W2] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) % 2.03/2.15 & aNaturalNumber0(W2) ) % 2.03/2.15 => ( ( doDivides0(W0,W1) % 2.03/2.15 & doDivides0(W0,W2) ) % 2.03/2.15 => doDivides0(W0,sdtpldt0(W1,W2)) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mDivMin,axiom, % 2.03/2.15 ! [W0,W1,W2] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) % 2.03/2.15 & aNaturalNumber0(W2) ) % 2.03/2.15 => ( ( doDivides0(W0,W1) % 2.03/2.15 & doDivides0(W0,sdtpldt0(W1,W2)) ) % 2.03/2.15 => doDivides0(W0,W2) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mDivLE,axiom, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( ( doDivides0(W0,W1) % 2.03/2.15 & W1 != sz00 ) % 2.03/2.15 => sdtlseqdt0(W0,W1) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mDivAsso,axiom, % 2.03/2.15 ! [W0,W1] : % 2.03/2.15 ( ( aNaturalNumber0(W0) % 2.03/2.15 & aNaturalNumber0(W1) ) % 2.03/2.15 => ( ( W0 != sz00 % 2.03/2.15 & doDivides0(W0,W1) ) % 2.03/2.15 => ! [W2] : % 2.03/2.15 ( aNaturalNumber0(W2) % 2.03/2.15 => sdtasdt0(W2,sdtsldt0(W1,W0)) = sdtsldt0(sdtasdt0(W2,W1),W0) ) ) ) ). % 2.03/2.15 % 2.03/2.15 fof(mDefPrime,definition, % 2.03/2.15 ! [W0] : % 2.03/2.15 ( aNaturalNumber0(W0) % 2.03/2.16 => ( isPrime0(W0) % 2.03/2.16 <=> ( W0 != sz00 % 2.03/2.16 & W0 != sz10 % 2.03/2.16 & ! [W1] : % 2.03/2.16 ( ( aNaturalNumber0(W1) % 2.03/2.16 & doDivides0(W1,W0) ) % 2.03/2.16 => ( W1 = sz10 % 2.03/2.16 | W1 = W0 ) ) ) ) ) ). % 2.03/2.16 % 2.03/2.16 fof(mPrimDiv,axiom, % 2.03/2.16 ! [W0] : % 2.03/2.16 ( ( aNaturalNumber0(W0) % 2.03/2.16 & W0 != sz00 % 2.03/2.16 & W0 != sz10 ) % 2.03/2.16 => ? [W1] : % 2.03/2.16 ( aNaturalNumber0(W1) % 2.03/2.16 & doDivides0(W1,W0) % 2.03/2.16 & isPrime0(W1) ) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__1837,hypothesis, % 2.03/2.16 ( aNaturalNumber0(xn) % 2.03/2.16 & aNaturalNumber0(xm) % 2.03/2.16 & aNaturalNumber0(xp) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__1799,hypothesis, % 2.03/2.16 ! [W0,W1,W2] : % 2.03/2.16 ( ( aNaturalNumber0(W0) % 2.03/2.16 & aNaturalNumber0(W1) % 2.03/2.16 & aNaturalNumber0(W2) ) % 2.03/2.16 => ( ( ( ( W2 != sz00 % 2.03/2.16 & W2 != sz10 % 2.03/2.16 & ! [W3] : % 2.03/2.16 ( ( aNaturalNumber0(W3) % 2.03/2.16 & ? [W4] : % 2.03/2.16 ( aNaturalNumber0(W4) % 2.03/2.16 & W2 = sdtasdt0(W3,W4) ) % 2.03/2.16 & doDivides0(W3,W2) ) % 2.03/2.16 => ( W3 = sz10 % 2.03/2.16 | W3 = W2 ) ) ) % 2.03/2.16 | isPrime0(W2) ) % 2.03/2.16 & ( ? [W3] : % 2.03/2.16 ( aNaturalNumber0(W3) % 2.03/2.16 & sdtasdt0(W0,W1) = sdtasdt0(W2,W3) ) % 2.03/2.16 | doDivides0(W2,sdtasdt0(W0,W1)) ) ) % 2.03/2.16 => ( iLess0(sdtpldt0(sdtpldt0(W0,W1),W2),sdtpldt0(sdtpldt0(xn,xm),xp)) % 2.03/2.16 => ( ( ? [W3] : % 2.03/2.16 ( aNaturalNumber0(W3) % 2.03/2.16 & W0 = sdtasdt0(W2,W3) ) % 2.03/2.16 & doDivides0(W2,W0) ) % 2.03/2.16 | ( ? [W3] : % 2.03/2.16 ( aNaturalNumber0(W3) % 2.03/2.16 & W1 = sdtasdt0(W2,W3) ) % 2.03/2.16 & doDivides0(W2,W1) ) ) ) ) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__1860,hypothesis, % 2.03/2.16 ( xp != sz00 % 2.03/2.16 & xp != sz10 % 2.03/2.16 & ! [W0] : % 2.03/2.16 ( ( aNaturalNumber0(W0) % 2.03/2.16 & ( ? [W1] : % 2.03/2.16 ( aNaturalNumber0(W1) % 2.03/2.16 & xp = sdtasdt0(W0,W1) ) % 2.03/2.16 | doDivides0(W0,xp) ) ) % 2.03/2.16 => ( W0 = sz10 % 2.03/2.16 | W0 = xp ) ) % 2.03/2.16 & isPrime0(xp) % 2.03/2.16 & ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & sdtasdt0(xn,xm) = sdtasdt0(xp,W0) ) % 2.03/2.16 & doDivides0(xp,sdtasdt0(xn,xm)) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__1870,hypothesis, % 2.03/2.16 ~ ( ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & sdtpldt0(xp,W0) = xn ) % 2.03/2.16 | sdtlseqdt0(xp,xn) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__2075,hypothesis, % 2.03/2.16 ~ ( ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & sdtpldt0(xp,W0) = xm ) % 2.03/2.16 | sdtlseqdt0(xp,xm) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__2287,hypothesis, % 2.03/2.16 ( xn != xp % 2.03/2.16 & ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & sdtpldt0(xn,W0) = xp ) % 2.03/2.16 & sdtlseqdt0(xn,xp) % 2.03/2.16 & xm != xp % 2.03/2.16 & ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & sdtpldt0(xm,W0) = xp ) % 2.03/2.16 & sdtlseqdt0(xm,xp) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__2306,hypothesis, % 2.03/2.16 ( aNaturalNumber0(xk) % 2.03/2.16 & sdtasdt0(xn,xm) = sdtasdt0(xp,xk) % 2.03/2.16 & xk = sdtsldt0(sdtasdt0(xn,xm),xp) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__2315,hypothesis, % 2.03/2.16 ~ ( xk = sz00 % 2.03/2.16 | xk = sz10 ) ). % 2.03/2.16 % 2.03/2.16 fof(m__2327,hypothesis, % 2.03/2.16 ( xk != sz00 % 2.03/2.16 & xk != sz10 ) ). % 2.03/2.16 % 2.03/2.16 fof(m__2342,hypothesis, % 2.03/2.16 ( aNaturalNumber0(xr) % 2.03/2.16 & ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & xk = sdtasdt0(xr,W0) ) % 2.03/2.16 & doDivides0(xr,xk) % 2.03/2.16 & xr != sz00 % 2.03/2.16 & xr != sz10 % 2.03/2.16 & ! [W0] : % 2.03/2.16 ( ( aNaturalNumber0(W0) % 2.03/2.16 & ( ? [W1] : % 2.03/2.16 ( aNaturalNumber0(W1) % 2.03/2.16 & xr = sdtasdt0(W0,W1) ) % 2.03/2.16 | doDivides0(W0,xr) ) ) % 2.03/2.16 => ( W0 = sz10 % 2.03/2.16 | W0 = xr ) ) % 2.03/2.16 & isPrime0(xr) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__2362,hypothesis, % 2.03/2.16 ( ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & sdtpldt0(xr,W0) = xk ) % 2.03/2.16 & ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & sdtasdt0(xn,xm) = sdtasdt0(xr,W0) ) % 2.03/2.16 & doDivides0(xr,sdtasdt0(xn,xm)) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__2377,hypothesis, % 2.03/2.16 ( xk != xp % 2.03/2.16 & ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & sdtpldt0(xk,W0) = xp ) % 2.03/2.16 & sdtlseqdt0(xk,xp) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__2449,hypothesis, % 2.03/2.16 ( ( ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & xn = sdtasdt0(xr,W0) ) % 2.03/2.16 & doDivides0(xr,xn) ) % 2.03/2.16 | ( ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & xm = sdtasdt0(xr,W0) ) % 2.03/2.16 & doDivides0(xr,xm) ) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__2487,hypothesis, % 2.03/2.16 ( ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & xn = sdtasdt0(xr,W0) ) % 2.03/2.16 & doDivides0(xr,xn) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__2504,hypothesis, % 2.03/2.16 ( ~ ( ( aNaturalNumber0(sdtsldt0(xn,xr)) % 2.03/2.16 & xn = sdtasdt0(xr,sdtsldt0(xn,xr)) ) % 2.03/2.16 => sdtsldt0(xn,xr) = xn ) % 2.03/2.16 & aNaturalNumber0(sdtsldt0(xn,xr)) % 2.03/2.16 & xn = sdtasdt0(xr,sdtsldt0(xn,xr)) % 2.03/2.16 & ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & sdtpldt0(sdtsldt0(xn,xr),W0) = xn ) % 2.03/2.16 & sdtlseqdt0(sdtsldt0(xn,xr),xn) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__2576,hypothesis, % 2.03/2.16 ( aNaturalNumber0(sdtsldt0(xn,xr)) % 2.03/2.16 & xn = sdtasdt0(xr,sdtsldt0(xn,xr)) % 2.03/2.16 & sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr) = sdtasdt0(xn,xm) % 2.03/2.16 & aNaturalNumber0(sdtsldt0(sdtasdt0(xp,xk),xr)) % 2.03/2.16 & sdtasdt0(xp,xk) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr)) % 2.03/2.16 & sdtasdt0(xn,xm) = sdtasdt0(sdtsldt0(sdtasdt0(xp,xk),xr),xr) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__2613,hypothesis, % 2.03/2.16 ( aNaturalNumber0(sdtsldt0(xk,xr)) % 2.03/2.16 & xk = sdtasdt0(xr,sdtsldt0(xk,xr)) % 2.03/2.16 & aNaturalNumber0(sdtsldt0(xn,xr)) % 2.03/2.16 & xn = sdtasdt0(xr,sdtsldt0(xn,xr)) % 2.03/2.16 & sdtasdt0(xp,sdtsldt0(xk,xr)) = sdtasdt0(sdtsldt0(xn,xr),xm) ) ). % 2.03/2.16 % 2.03/2.16 fof(m__,conjecture, % 2.03/2.16 ( ( aNaturalNumber0(sdtsldt0(xn,xr)) % 2.03/2.16 & xn = sdtasdt0(xr,sdtsldt0(xn,xr)) ) % 2.03/2.16 => ( ? [W0] : % 2.03/2.16 ( aNaturalNumber0(W0) % 2.03/2.16 & sdtasdt0(sdtsldt0(xn,xr),xm) = sdtasdt0(xp,W0) ) % 2.03/2.16 | doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)) ) ) ). % 2.03/2.16 % 2.03/2.16 %------------------------------------------------------------------------------ % 2.03/2.16 %------------------------------------------- % 2.03/2.16 % Proof found % 2.03/2.16 % SZS status Theorem for theBenchmark % 2.03/2.16 % SZS output start Proof % 2.03/2.16 %ClaNum:313(EqnAxiom:37) % 2.03/2.16 %VarNum:3218(SingletonVarNum:578) % 2.03/2.16 %MaxLitNum:11 % 2.03/2.16 %MaxfuncDepth:3 % 2.03/2.16 %SharedTerms:109 % 2.03/2.16 %goalClause: 74 80 107 166 % 2.03/2.16 %singleGoalClaCount:3 % 2.03/2.16 [38]P1(a1) % 2.03/2.16 [39]P1(a25) % 2.03/2.16 [40]P1(a26) % 2.03/2.16 [41]P1(a27) % 2.03/2.16 [42]P1(a29) % 2.03/2.16 [43]P1(a28) % 2.03/2.16 [44]P1(a30) % 2.03/2.16 [45]P1(a2) % 2.03/2.16 [46]P1(a3) % 2.03/2.16 [47]P1(a4) % 2.03/2.16 [48]P1(a5) % 2.03/2.16 [49]P1(a6) % 2.03/2.16 [50]P1(a7) % 2.03/2.16 [51]P1(a8) % 2.03/2.16 [52]P1(a9) % 2.03/2.16 [53]P1(a12) % 2.03/2.16 [54]P2(a29) % 2.03/2.16 [55]P2(a30) % 2.03/2.16 [62]P5(a26,a29) % 2.03/2.16 [63]P5(a27,a29) % 2.03/2.16 [64]P5(a28,a29) % 2.03/2.16 [65]P3(a30,a26) % 2.03/2.16 [66]P3(a30,a28) % 2.03/2.16 [92]~E(a1,a25) % 2.03/2.16 [93]~E(a1,a29) % 2.03/2.16 [94]~E(a29,a25) % 2.03/2.16 [95]~E(a29,a26) % 2.03/2.16 [96]~E(a29,a27) % 2.03/2.16 [98]~E(a1,a28) % 2.03/2.16 [100]~E(a28,a25) % 2.03/2.16 [101]~E(a28,a29) % 2.03/2.16 [102]~E(a1,a30) % 2.03/2.16 [103]~E(a30,a25) % 2.03/2.16 [105]~P5(a29,a26) % 2.03/2.16 [106]~P5(a29,a27) % 2.03/2.16 [56]E(f21(a30,a9),a26) % 2.03/2.16 [57]E(f21(a30,a5),a28) % 2.03/2.16 [58]E(f22(a26,a3),a29) % 2.03/2.16 [59]E(f22(a27,a4),a29) % 2.03/2.16 [60]E(f22(a28,a8),a29) % 2.03/2.16 [61]E(f22(a30,a6),a28) % 2.03/2.16 [67]E(f21(a29,a28),f21(a26,a27)) % 2.03/2.16 [68]E(f21(a29,a2),f21(a26,a27)) % 2.03/2.16 [69]E(f21(a30,a7),f21(a26,a27)) % 2.03/2.16 [74]P1(f24(a26,a30)) % 2.03/2.16 [75]P1(f24(a28,a30)) % 2.03/2.16 [84]P3(a29,f21(a26,a27)) % 2.03/2.16 [85]P3(a30,f21(a26,a27)) % 2.03/2.16 [86]P5(f24(a26,a30),a26) % 2.03/2.16 [104]~E(f24(a26,a30),a26) % 2.03/2.16 [80]E(f21(a30,f24(a26,a30)),a26) % 2.03/2.16 [81]E(f21(a30,f24(a28,a30)),a28) % 2.03/2.16 [82]E(f24(f21(a26,a27),a29),a28) % 2.03/2.16 [83]E(f22(f24(a26,a30),a12),a26) % 2.03/2.16 [87]E(f21(f24(a26,a30),a27),f21(a29,f24(a28,a30))) % 2.03/2.16 [88]P1(f24(f21(a29,a28),a30)) % 2.03/2.16 [107]~P3(a29,f21(f24(a26,a30),a27)) % 2.03/2.16 [89]E(f21(a30,f24(f21(a29,a28),a30)),f21(a29,a28)) % 2.03/2.16 [90]E(f21(f24(f21(a29,a28),a30),a30),f21(a26,a27)) % 2.03/2.16 [91]E(f21(f21(f24(a26,a30),a27),a30),f21(a26,a27)) % 2.03/2.16 [108]P1(a10)+P1(a11) % 2.03/2.16 [111]P1(a10)+P3(a30,a27) % 2.03/2.16 [109]P1(a11)+E(f21(a30,a10),a26) % 2.03/2.16 [110]P1(a10)+E(f21(a30,a11),a27) % 2.03/2.16 [125]E(f21(a30,a10),a26)+E(f21(a30,a11),a27) % 2.03/2.16 [126]P3(a30,a27)+E(f21(a30,a10),a26) % 2.03/2.16 [123]~P1(x1231)+P5(x1231,x1231) % 2.03/2.16 [115]~P1(x1151)+E(f21(a1,x1151),a1) % 2.03/2.16 [116]~P1(x1161)+E(f21(x1161,a1),a1) % 2.03/2.16 [117]~P1(x1171)+E(f22(a1,x1171),x1171) % 2.03/2.16 [118]~P1(x1181)+E(f21(a25,x1181),x1181) % 2.03/2.16 [119]~P1(x1191)+E(f22(x1191,a1),x1191) % 2.03/2.16 [120]~P1(x1201)+E(f21(x1201,a25),x1201) % 2.03/2.16 [132]~P1(x1321)+~E(f22(a29,x1321),a26) % 2.03/2.16 [133]~P1(x1331)+~E(f22(a29,x1331),a27) % 2.03/2.16 [166]~P1(x1661)+~E(f21(f24(a26,a30),a27),f21(a29,x1661)) % 2.03/2.16 [113]~P1(x1131)+~P2(x1131)+~E(x1131,a1) % 2.03/2.16 [114]~P1(x1141)+~P2(x1141)+~E(x1141,a25) % 2.03/2.16 [144]~P1(x1442)+~P1(x1441)+E(f22(x1441,x1442),f22(x1442,x1441)) % 2.03/2.16 [145]~P1(x1452)+~P1(x1451)+E(f21(x1451,x1452),f21(x1452,x1451)) % 2.03/2.16 [147]~P1(x1472)+~P1(x1471)+P1(f22(x1471,x1472)) % 2.03/2.16 [148]~P1(x1482)+~P1(x1481)+P1(f21(x1481,x1482)) % 2.03/2.16 [129]~P1(x1291)+E(x1291,a25)+P5(a25,x1291)+E(x1291,a1) % 2.03/2.16 [134]~P1(x1341)+E(x1341,a29)+~P3(x1341,a29)+E(x1341,a25) % 2.03/2.16 [135]~P1(x1351)+E(x1351,a30)+~P3(x1351,a30)+E(x1351,a25) % 2.03/2.16 [121]~P1(x1211)+E(x1211,a25)+E(x1211,a1)+P1(f13(x1211)) % 2.03/2.16 [122]~P1(x1221)+E(x1221,a25)+E(x1221,a1)+P2(f13(x1221)) % 2.03/2.16 [136]~P1(x1361)+E(x1361,a25)+P3(f13(x1361),x1361)+E(x1361,a1) % 2.03/2.16 [137]~E(x1372,x1371)+~P1(x1371)+~P1(x1372)+P5(x1371,x1372) % 2.03/2.16 [146]P5(x1462,x1461)+~P1(x1461)+~P1(x1462)+P5(x1461,x1462) % 2.03/2.16 [139]~P1(x1392)+~P1(x1391)+E(x1391,a1)+~E(f22(x1392,x1391),a1) % 2.03/2.16 [140]~P1(x1402)+~P1(x1401)+E(x1401,a1)+~E(f22(x1401,x1402),a1) % 2.03/2.16 [152]~P1(x1522)+~P1(x1521)+P5(x1522,f21(x1522,x1521))+E(x1521,a1) % 2.03/2.16 [158]~P1(x1582)+~P1(x1581)+~P5(x1581,x1582)+P1(f15(x1581,x1582)) % 2.03/2.16 [159]~P1(x1592)+~P1(x1591)+~P3(x1591,x1592)+P1(f16(x1591,x1592)) % 2.03/2.16 [167]~P1(x1671)+~P1(x1672)+~P3(x1671,x1672)+E(f21(x1671,f16(x1671,x1672)),x1672) % 2.03/2.16 [168]~P1(x1682)+~P1(x1681)+~P5(x1681,x1682)+E(f22(x1681,f15(x1681,x1682)),x1682) % 2.03/2.16 [177]~P1(x1773)+~P1(x1772)+~P1(x1771)+E(f22(f22(x1771,x1772),x1773),f22(x1771,f22(x1772,x1773))) % 2.03/2.16 [178]~P1(x1783)+~P1(x1782)+~P1(x1781)+E(f21(f21(x1781,x1782),x1783),f21(x1781,f21(x1782,x1783))) % 2.03/2.16 [186]~P1(x1863)+~P1(x1862)+~P1(x1861)+E(f22(f21(x1861,x1862),f21(x1861,x1863)),f21(x1861,f22(x1862,x1863))) % 2.03/2.16 [187]~P1(x1872)+~P1(x1873)+~P1(x1871)+E(f22(f21(x1871,x1872),f21(x1873,x1872)),f21(f22(x1871,x1873),x1872)) % 2.03/2.16 [124]P2(x1241)+~P1(x1241)+E(x1241,a25)+E(x1241,a1)+~E(f14(x1241),a25) % 2.03/2.16 [130]P2(x1301)+~P1(x1301)+E(x1301,a25)+~E(f14(x1301),x1301)+E(x1301,a1) % 2.03/2.16 [131]P2(x1311)+~P1(x1311)+E(x1311,a25)+E(x1311,a1)+P1(f14(x1311)) % 2.03/2.16 [138]P2(x1381)+~P1(x1381)+E(x1381,a25)+P3(f14(x1381),x1381)+E(x1381,a1) % 2.03/2.16 [150]~P1(x1501)+~P1(x1502)+~P3(x1502,x1501)+P5(x1502,x1501)+E(x1501,a1) % 2.03/2.16 [151]P4(x1511,x1512)+~P1(x1512)+~P1(x1511)+~P5(x1511,x1512)+E(x1511,x1512) % 2.03/2.16 [155]~P1(x1552)+~P1(x1551)+~P5(x1552,x1551)+~P5(x1551,x1552)+E(x1551,x1552) % 2.03/2.16 [141]~P1(x1411)+~P1(x1412)+E(x1411,a29)+E(x1411,a25)+~E(f21(x1411,x1412),a29) % 2.03/2.16 [142]~P1(x1421)+~P1(x1422)+E(x1421,a30)+E(x1421,a25)+~E(f21(x1421,x1422),a30) % 2.03/2.16 [143]~P1(x1431)+~P1(x1432)+E(x1431,a1)+E(x1432,a1)+~E(f21(x1432,x1431),a1) % 2.03/2.16 [153]~P1(x1531)+~P1(x1532)+~P1(x1533)+P3(x1531,x1532)+~E(x1532,f21(x1531,x1533)) % 2.03/2.16 [154]~P1(x1542)+~P1(x1541)+~P1(x1543)+P5(x1541,x1542)+~E(f22(x1541,x1543),x1542) % 2.03/2.16 [156]~P1(x1563)+~P1(x1562)+~P5(x1563,x1562)+P1(x1561)+~E(x1561,f23(x1562,x1563)) % 2.03/2.16 [160]~P1(x1602)+~P1(x1601)+~P1(x1603)+E(x1601,x1602)+~E(f22(x1603,x1601),f22(x1603,x1602)) % 2.03/2.16 [161]~P1(x1612)+~P1(x1613)+~P1(x1611)+E(x1611,x1612)+~E(f22(x1611,x1613),f22(x1612,x1613)) % 2.03/2.16 [164]~P1(x1643)+~P1(x1641)+~P5(x1641,x1643)+~E(x1642,f23(x1643,x1641))+E(f22(x1641,x1642),x1643) % 2.03/2.16 [149]~P1(x1492)+~P1(x1491)+~P2(x1492)+~P3(x1491,x1492)+E(x1491,x1492)+E(x1491,a25) % 2.03/2.16 [169]~P1(x1692)+~P1(x1691)+~P5(x1693,x1692)+~P5(x1691,x1693)+P5(x1691,x1692)+~P1(x1693) % 2.03/2.16 [170]~P1(x1702)+~P1(x1701)+~P3(x1703,x1702)+~P3(x1701,x1703)+P3(x1701,x1702)+~P1(x1703) % 2.03/2.16 [157]~P1(x1571)+~P1(x1573)+~P3(x1571,x1573)+P1(x1572)+E(x1571,a1)+~E(x1572,f24(x1573,x1571)) % 2.03/2.16 [162]~P1(x1622)+~P1(x1621)+~P1(x1623)+E(x1621,x1622)+~E(f21(x1623,x1621),f21(x1623,x1622))+E(x1623,a1) % 2.03/2.16 [163]~P1(x1632)+~P1(x1633)+~P1(x1631)+E(x1631,x1632)+~E(f21(x1631,x1633),f21(x1632,x1633))+E(x1633,a1) % 2.03/2.16 [165]~P1(x1651)+~P1(x1652)+~P3(x1651,x1652)+~E(x1653,f24(x1652,x1651))+E(x1651,a1)+E(x1652,f21(x1651,x1653)) % 2.03/2.16 [171]~P1(x1712)+~P1(x1713)+~P1(x1711)+~P5(x1713,x1712)+~E(f22(x1713,x1711),x1712)+E(x1711,f23(x1712,x1713)) % 2.03/2.16 [179]~P1(x1793)+~P1(x1792)+~P1(x1791)+~P3(x1791,x1793)+~P3(x1791,x1792)+P3(x1791,f22(x1792,x1793)) % 2.03/2.16 [180]~P1(x1802)+~P1(x1801)+~P1(x1803)+~P5(x1801,x1802)+E(x1801,x1802)+P5(f22(x1803,x1801),f22(x1803,x1802)) % 2.03/2.16 [181]~P1(x1812)+~P1(x1813)+~P1(x1811)+~P5(x1811,x1812)+E(x1811,x1812)+P5(f22(x1811,x1813),f22(x1812,x1813)) % 2.03/2.16 [184]~P1(x1842)+~P1(x1841)+~P3(x1841,x1843)+P3(x1841,x1842)+~P1(x1843)+~P3(x1841,f22(x1843,x1842)) % 2.03/2.16 [185]~P1(x1852)+~P1(x1853)+~P1(x1851)+~P3(x1851,x1853)+E(x1851,a1)+E(f24(f21(x1852,x1853),x1851),f21(x1852,f24(x1853,x1851))) % 2.03/2.16 [172]~P1(x1721)+~P1(x1723)+~P1(x1722)+~P3(x1721,x1723)+~E(x1723,f21(x1721,x1722))+E(x1721,a1)+E(x1722,f24(x1723,x1721)) % 2.03/2.16 [182]~P1(x1822)+~P1(x1821)+~P1(x1823)+~P5(x1821,x1822)+E(x1821,x1822)+P5(f21(x1823,x1821),f21(x1823,x1822))+E(x1823,a1) % 2.03/2.16 [183]~P1(x1832)+~P1(x1833)+~P1(x1831)+~P5(x1831,x1832)+E(x1831,x1832)+P5(f21(x1831,x1833),f21(x1832,x1833))+E(x1833,a1) % 2.03/2.16 [189]~P1(x1892)+~P1(x1893)+~P1(x1891)+~P2(x1891)+P3(x1891,x1892)+P3(x1891,x1893)+~P3(x1891,f21(x1892,x1893))+~P4(f22(f22(x1892,x1893),x1891),f22(f22(a26,a27),a29)) % 2.03/2.16 [200]~P1(x2001)+~P1(x2003)+~P1(x2002)+~P2(x2001)+P3(x2001,x2002)+~P3(x2001,f21(x2002,x2003))+P1(f18(x2002,x2003,x2001))+~P4(f22(f22(x2002,x2003),x2001),f22(f22(a26,a27),a29)) % 2.03/2.16 [201]~P1(x2013)+~P1(x2012)+~P1(x2011)+~P2(x2011)+P3(x2011,x2012)+~P3(x2011,f21(x2013,x2012))+P1(f19(x2013,x2012,x2011))+~P4(f22(f22(x2013,x2012),x2011),f22(f22(a26,a27),a29)) % 2.03/2.16 [205]P3(x2051,x2053)+~P1(x2052)+~P1(x2053)+~P1(x2051)+~P2(x2051)+~P3(x2051,f21(x2052,x2053))+E(f21(x2051,f19(x2052,x2053,x2051)),x2052)+~P4(f22(f22(x2052,x2053),x2051),f22(f22(a26,a27),a29)) % 2.03/2.16 [206]P3(x2061,x2062)+~P1(x2062)+~P1(x2061)+~P1(x2063)+~P2(x2061)+~P3(x2061,f21(x2062,x2063))+E(f21(x2061,f18(x2062,x2063,x2061)),x2063)+~P4(f22(f22(x2062,x2063),x2061),f22(f22(a26,a27),a29)) % 2.03/2.16 [231]~P1(x2313)+~P1(x2312)+~P1(x2311)+~P2(x2313)+~P3(x2313,f21(x2311,x2312))+P1(f18(x2311,x2312,x2313))+~P4(f22(f22(x2311,x2312),x2313),f22(f22(a26,a27),a29))+P1(f19(x2311,x2312,x2313)) % 2.03/2.16 [243]~P1(x2431)+~P1(x2433)+~P1(x2432)+~P2(x2431)+~P3(x2431,f21(x2432,x2433))+P1(f18(x2432,x2433,x2431))+~P4(f22(f22(x2432,x2433),x2431),f22(f22(a26,a27),a29))+E(f21(x2431,f19(x2432,x2433,x2431)),x2432) % 2.03/2.16 [244]~P1(x2442)+~P1(x2441)+~P1(x2443)+~P2(x2441)+~P3(x2441,f21(x2442,x2443))+P1(f19(x2442,x2443,x2441))+~P4(f22(f22(x2442,x2443),x2441),f22(f22(a26,a27),a29))+E(f21(x2441,f18(x2442,x2443,x2441)),x2443) % 2.03/2.16 [254]~P1(x2542)+~P1(x2541)+~P1(x2543)+~P2(x2541)+~P3(x2541,f21(x2542,x2543))+E(f21(x2541,f18(x2542,x2543,x2541)),x2543)+~P4(f22(f22(x2542,x2543),x2541),f22(f22(a26,a27),a29))+E(f21(x2541,f19(x2542,x2543,x2541)),x2542) % 2.03/2.16 [188]~P1(x1884)+~P1(x1882)+~P1(x1883)+~P1(x1881)+~P2(x1881)+P3(x1881,x1882)+P3(x1881,x1883)+~E(f21(x1881,x1884),f21(x1882,x1883))+~P4(f22(f22(x1882,x1883),x1881),f22(f22(a26,a27),a29)) % 2.03/2.16 [194]~P1(x1944)+~P1(x1941)+~P1(x1943)+~P1(x1942)+~P2(x1941)+P3(x1941,x1942)+~E(f21(x1942,x1943),f21(x1941,x1944))+P1(f18(x1942,x1943,x1941))+~P4(f22(f22(x1942,x1943),x1941),f22(f22(a26,a27),a29)) % 2.03/2.16 [195]~P1(x1954)+~P1(x1953)+~P1(x1952)+~P1(x1951)+~P2(x1951)+P3(x1951,x1952)+~E(f21(x1951,x1954),f21(x1953,x1952))+P1(f19(x1953,x1952,x1951))+~P4(f22(f22(x1953,x1952),x1951),f22(f22(a26,a27),a29)) % 2.03/2.16 [198]P3(x1981,x1983)+~P1(x1984)+~P1(x1982)+~P1(x1983)+~P1(x1981)+~P2(x1981)+~E(f21(x1981,x1984),f21(x1982,x1983))+E(f21(x1981,f19(x1982,x1983,x1981)),x1982)+~P4(f22(f22(x1982,x1983),x1981),f22(f22(a26,a27),a29)) % 2.03/2.16 [199]P3(x1991,x1992)+~P1(x1994)+~P1(x1992)+~P1(x1991)+~P1(x1993)+~P2(x1991)+~E(f21(x1991,x1994),f21(x1992,x1993))+E(f21(x1991,f18(x1992,x1993,x1991)),x1993)+~P4(f22(f22(x1992,x1993),x1991),f22(f22(a26,a27),a29)) % 2.03/2.16 [220]~P1(x2204)+~P1(x2203)+~P1(x2202)+~P1(x2201)+~P2(x2203)+~E(f21(x2201,x2202),f21(x2203,x2204))+P1(f18(x2201,x2202,x2203))+~P4(f22(f22(x2201,x2202),x2203),f22(f22(a26,a27),a29))+P1(f19(x2201,x2202,x2203)) % 2.03/2.16 [229]~P1(x2294)+~P1(x2291)+~P1(x2293)+~P1(x2292)+~P2(x2291)+~E(f21(x2292,x2293),f21(x2291,x2294))+P1(f18(x2292,x2293,x2291))+~P4(f22(f22(x2292,x2293),x2291),f22(f22(a26,a27),a29))+E(f21(x2291,f19(x2292,x2293,x2291)),x2292) % 2.03/2.16 [230]~P1(x2304)+~P1(x2302)+~P1(x2301)+~P1(x2303)+~P2(x2301)+~E(f21(x2301,x2304),f21(x2302,x2303))+P1(f19(x2302,x2303,x2301))+~P4(f22(f22(x2302,x2303),x2301),f22(f22(a26,a27),a29))+E(f21(x2301,f18(x2302,x2303,x2301)),x2303) % 2.03/2.16 [238]~P1(x2384)+~P1(x2382)+~P1(x2381)+~P1(x2383)+~P2(x2381)+~E(f21(x2381,x2384),f21(x2382,x2383))+E(f21(x2381,f18(x2382,x2383,x2381)),x2383)+~P4(f22(f22(x2382,x2383),x2381),f22(f22(a26,a27),a29))+E(f21(x2381,f19(x2382,x2383,x2381)),x2382) % 2.03/2.16 [192]~P1(x1922)+~P1(x1923)+~P1(x1921)+P3(x1921,x1922)+P3(x1921,x1923)+E(x1921,a25)+~P3(x1921,f21(x1922,x1923))+E(x1921,a1)+~E(f17(x1922,x1923,x1921),a25)+~P4(f22(f22(x1922,x1923),x1921),f22(f22(a26,a27),a29)) % 2.03/2.16 [193]~P1(x1932)+~P1(x1933)+~P1(x1931)+P3(x1931,x1932)+P3(x1931,x1933)+E(x1931,a25)+~E(f17(x1932,x1933,x1931),x1931)+~P3(x1931,f21(x1932,x1933))+E(x1931,a1)+~P4(f22(f22(x1932,x1933),x1931),f22(f22(a26,a27),a29)) % 2.03/2.16 [203]~P1(x2032)+~P1(x2033)+~P1(x2031)+P3(x2031,x2032)+P3(x2031,x2033)+E(x2031,a25)+~P3(x2031,f21(x2032,x2033))+E(x2031,a1)+P1(f17(x2032,x2033,x2031))+~P4(f22(f22(x2032,x2033),x2031),f22(f22(a26,a27),a29)) % 2.03/2.16 [204]~P1(x2042)+~P1(x2043)+~P1(x2041)+P3(x2041,x2042)+P3(x2041,x2043)+E(x2041,a25)+~P3(x2041,f21(x2042,x2043))+E(x2041,a1)+P1(f20(x2042,x2043,x2041))+~P4(f22(f22(x2042,x2043),x2041),f22(f22(a26,a27),a29)) % 2.03/2.16 [207]~P1(x2072)+~P1(x2073)+~P1(x2071)+P3(x2071,x2072)+P3(x2071,x2073)+E(x2071,a25)+P3(f17(x2072,x2073,x2071),x2071)+~P3(x2071,f21(x2072,x2073))+E(x2071,a1)+~P4(f22(f22(x2072,x2073),x2071),f22(f22(a26,a27),a29)) % 2.03/2.16 [216]~P1(x2161)+~P1(x2163)+~P1(x2162)+P3(x2161,x2162)+E(x2161,a25)+~P3(x2161,f21(x2162,x2163))+E(x2161,a1)+~E(f17(x2162,x2163,x2161),a25)+~P4(f22(f22(x2162,x2163),x2161),f22(f22(a26,a27),a29))+P1(f18(x2162,x2163,x2161)) % 2.03/2.16 [217]~P1(x2173)+~P1(x2172)+~P1(x2171)+P3(x2171,x2172)+E(x2171,a25)+~P3(x2171,f21(x2173,x2172))+E(x2171,a1)+~E(f17(x2173,x2172,x2171),a25)+~P4(f22(f22(x2173,x2172),x2171),f22(f22(a26,a27),a29))+P1(f19(x2173,x2172,x2171)) % 2.03/2.16 [218]~P1(x2181)+~P1(x2183)+~P1(x2182)+P3(x2181,x2182)+E(x2181,a25)+~E(f17(x2182,x2183,x2181),x2181)+~P3(x2181,f21(x2182,x2183))+E(x2181,a1)+~P4(f22(f22(x2182,x2183),x2181),f22(f22(a26,a27),a29))+P1(f18(x2182,x2183,x2181)) % 2.03/2.16 [219]~P1(x2193)+~P1(x2192)+~P1(x2191)+P3(x2191,x2192)+E(x2191,a25)+~E(f17(x2193,x2192,x2191),x2191)+~P3(x2191,f21(x2193,x2192))+E(x2191,a1)+~P4(f22(f22(x2193,x2192),x2191),f22(f22(a26,a27),a29))+P1(f19(x2193,x2192,x2191)) % 2.03/2.16 [221]P3(x2211,x2212)+~P1(x2212)+~P1(x2211)+~P1(x2213)+E(x2211,a25)+~P3(x2211,f21(x2212,x2213))+E(x2211,a1)+~E(f17(x2212,x2213,x2211),a25)+~P4(f22(f22(x2212,x2213),x2211),f22(f22(a26,a27),a29))+E(f21(x2211,f18(x2212,x2213,x2211)),x2213) % 2.03/2.16 [222]P3(x2221,x2223)+~P1(x2222)+~P1(x2223)+~P1(x2221)+E(x2221,a25)+~P3(x2221,f21(x2222,x2223))+E(x2221,a1)+~E(f17(x2222,x2223,x2221),a25)+~P4(f22(f22(x2222,x2223),x2221),f22(f22(a26,a27),a29))+E(f21(x2221,f19(x2222,x2223,x2221)),x2222) % 2.03/2.16 [223]P3(x2231,x2232)+~P1(x2232)+~P1(x2231)+~P1(x2233)+E(x2231,a25)+~E(f17(x2232,x2233,x2231),x2231)+~P3(x2231,f21(x2232,x2233))+E(x2231,a1)+~P4(f22(f22(x2232,x2233),x2231),f22(f22(a26,a27),a29))+E(f21(x2231,f18(x2232,x2233,x2231)),x2233) % 2.03/2.16 [224]P3(x2241,x2243)+~P1(x2242)+~P1(x2243)+~P1(x2241)+E(x2241,a25)+~E(f17(x2242,x2243,x2241),x2241)+~P3(x2241,f21(x2242,x2243))+E(x2241,a1)+~P4(f22(f22(x2242,x2243),x2241),f22(f22(a26,a27),a29))+E(f21(x2241,f19(x2242,x2243,x2241)),x2242) % 2.03/2.17 [239]~P1(x2391)+~P1(x2393)+~P1(x2392)+P3(x2391,x2392)+E(x2391,a25)+~P3(x2391,f21(x2392,x2393))+E(x2391,a1)+P1(f18(x2392,x2393,x2391))+~P4(f22(f22(x2392,x2393),x2391),f22(f22(a26,a27),a29))+P1(f17(x2392,x2393,x2391)) % 2.03/2.17 [240]~P1(x2401)+~P1(x2403)+~P1(x2402)+P3(x2401,x2402)+E(x2401,a25)+~P3(x2401,f21(x2402,x2403))+E(x2401,a1)+P1(f18(x2402,x2403,x2401))+~P4(f22(f22(x2402,x2403),x2401),f22(f22(a26,a27),a29))+P1(f20(x2402,x2403,x2401)) % 2.03/2.17 [241]~P1(x2413)+~P1(x2412)+~P1(x2411)+P3(x2411,x2412)+E(x2411,a25)+~P3(x2411,f21(x2413,x2412))+E(x2411,a1)+P1(f19(x2413,x2412,x2411))+~P4(f22(f22(x2413,x2412),x2411),f22(f22(a26,a27),a29))+P1(f17(x2413,x2412,x2411)) % 2.03/2.17 [242]~P1(x2423)+~P1(x2422)+~P1(x2421)+P3(x2421,x2422)+E(x2421,a25)+~P3(x2421,f21(x2423,x2422))+E(x2421,a1)+P1(f19(x2423,x2422,x2421))+~P4(f22(f22(x2423,x2422),x2421),f22(f22(a26,a27),a29))+P1(f20(x2423,x2422,x2421)) % 2.03/2.17 [248]~P1(x2481)+~P1(x2483)+~P1(x2482)+P3(x2481,x2482)+E(x2481,a25)+P3(f17(x2482,x2483,x2481),x2481)+~P3(x2481,f21(x2482,x2483))+E(x2481,a1)+~P4(f22(f22(x2482,x2483),x2481),f22(f22(a26,a27),a29))+P1(f18(x2482,x2483,x2481)) % 2.03/2.17 [249]~P1(x2493)+~P1(x2492)+~P1(x2491)+P3(x2491,x2492)+E(x2491,a25)+P3(f17(x2493,x2492,x2491),x2491)+~P3(x2491,f21(x2493,x2492))+E(x2491,a1)+~P4(f22(f22(x2493,x2492),x2491),f22(f22(a26,a27),a29))+P1(f19(x2493,x2492,x2491)) % 2.03/2.17 [250]P3(x2501,x2502)+~P1(x2502)+~P1(x2501)+~P1(x2503)+E(x2501,a25)+~P3(x2501,f21(x2502,x2503))+E(x2501,a1)+P1(f17(x2502,x2503,x2501))+~P4(f22(f22(x2502,x2503),x2501),f22(f22(a26,a27),a29))+E(f21(x2501,f18(x2502,x2503,x2501)),x2503) % 2.03/2.17 [251]P3(x2511,x2512)+~P1(x2512)+~P1(x2511)+~P1(x2513)+E(x2511,a25)+~P3(x2511,f21(x2512,x2513))+E(x2511,a1)+P1(f20(x2512,x2513,x2511))+~P4(f22(f22(x2512,x2513),x2511),f22(f22(a26,a27),a29))+E(f21(x2511,f18(x2512,x2513,x2511)),x2513) % 2.03/2.17 [252]P3(x2521,x2523)+~P1(x2522)+~P1(x2523)+~P1(x2521)+E(x2521,a25)+~P3(x2521,f21(x2522,x2523))+E(x2521,a1)+P1(f17(x2522,x2523,x2521))+~P4(f22(f22(x2522,x2523),x2521),f22(f22(a26,a27),a29))+E(f21(x2521,f19(x2522,x2523,x2521)),x2522) % 2.03/2.17 [253]P3(x2531,x2533)+~P1(x2532)+~P1(x2533)+~P1(x2531)+E(x2531,a25)+~P3(x2531,f21(x2532,x2533))+E(x2531,a1)+P1(f20(x2532,x2533,x2531))+~P4(f22(f22(x2532,x2533),x2531),f22(f22(a26,a27),a29))+E(f21(x2531,f19(x2532,x2533,x2531)),x2532) % 2.03/2.17 [255]P3(x2551,x2552)+~P1(x2552)+~P1(x2551)+~P1(x2553)+E(x2551,a25)+P3(f17(x2552,x2553,x2551),x2551)+~P3(x2551,f21(x2552,x2553))+E(x2551,a1)+~P4(f22(f22(x2552,x2553),x2551),f22(f22(a26,a27),a29))+E(f21(x2551,f18(x2552,x2553,x2551)),x2553) % 2.03/2.17 [256]P3(x2561,x2563)+~P1(x2562)+~P1(x2563)+~P1(x2561)+E(x2561,a25)+P3(f17(x2562,x2563,x2561),x2561)+~P3(x2561,f21(x2562,x2563))+E(x2561,a1)+~P4(f22(f22(x2562,x2563),x2561),f22(f22(a26,a27),a29))+E(f21(x2561,f19(x2562,x2563,x2561)),x2562) % 2.03/2.17 [257]P3(x2571,x2572)+P3(x2571,x2573)+~P1(x2572)+~P1(x2573)+~P1(x2571)+E(x2571,a25)+~P3(x2571,f21(x2572,x2573))+E(x2571,a1)+~P4(f22(f22(x2572,x2573),x2571),f22(f22(a26,a27),a29))+E(f21(f17(x2572,x2573,x2571),f20(x2572,x2573,x2571)),x2571) % 2.03/2.17 [264]~P1(x2641)+~P1(x2643)+~P1(x2642)+E(x2641,a25)+~P3(x2641,f21(x2642,x2643))+E(x2641,a1)+P1(f18(x2642,x2643,x2641))+~E(f17(x2642,x2643,x2641),a25)+~P4(f22(f22(x2642,x2643),x2641),f22(f22(a26,a27),a29))+P1(f19(x2642,x2643,x2641)) % 2.03/2.17 [265]~P1(x2651)+~P1(x2653)+~P1(x2652)+E(x2651,a25)+~E(f17(x2652,x2653,x2651),x2651)+~P3(x2651,f21(x2652,x2653))+E(x2651,a1)+P1(f18(x2652,x2653,x2651))+~P4(f22(f22(x2652,x2653),x2651),f22(f22(a26,a27),a29))+P1(f19(x2652,x2653,x2651)) % 2.03/2.17 [268]~P1(x2681)+~P1(x2683)+~P1(x2682)+E(x2681,a25)+~P3(x2681,f21(x2682,x2683))+E(x2681,a1)+P1(f18(x2682,x2683,x2681))+~E(f17(x2682,x2683,x2681),a25)+~P4(f22(f22(x2682,x2683),x2681),f22(f22(a26,a27),a29))+E(f21(x2681,f19(x2682,x2683,x2681)),x2682) % 2.03/2.17 [269]~P1(x2692)+~P1(x2691)+~P1(x2693)+E(x2691,a25)+~P3(x2691,f21(x2692,x2693))+E(x2691,a1)+P1(f19(x2692,x2693,x2691))+~E(f17(x2692,x2693,x2691),a25)+~P4(f22(f22(x2692,x2693),x2691),f22(f22(a26,a27),a29))+E(f21(x2691,f18(x2692,x2693,x2691)),x2693) % 2.03/2.17 [270]~P1(x2701)+~P1(x2703)+~P1(x2702)+E(x2701,a25)+~E(f17(x2702,x2703,x2701),x2701)+~P3(x2701,f21(x2702,x2703))+E(x2701,a1)+P1(f18(x2702,x2703,x2701))+~P4(f22(f22(x2702,x2703),x2701),f22(f22(a26,a27),a29))+E(f21(x2701,f19(x2702,x2703,x2701)),x2702) % 2.03/2.17 [271]~P1(x2712)+~P1(x2711)+~P1(x2713)+E(x2711,a25)+~E(f17(x2712,x2713,x2711),x2711)+~P3(x2711,f21(x2712,x2713))+E(x2711,a1)+P1(f19(x2712,x2713,x2711))+~P4(f22(f22(x2712,x2713),x2711),f22(f22(a26,a27),a29))+E(f21(x2711,f18(x2712,x2713,x2711)),x2713) % 2.03/2.17 [274]~P1(x2742)+~P1(x2741)+~P1(x2743)+E(x2741,a25)+~P3(x2741,f21(x2742,x2743))+E(x2741,a1)+E(f21(x2741,f18(x2742,x2743,x2741)),x2743)+~E(f17(x2742,x2743,x2741),a25)+~P4(f22(f22(x2742,x2743),x2741),f22(f22(a26,a27),a29))+E(f21(x2741,f19(x2742,x2743,x2741)),x2742) % 2.03/2.17 [275]~P1(x2752)+~P1(x2751)+~P1(x2753)+E(x2751,a25)+~E(f17(x2752,x2753,x2751),x2751)+~P3(x2751,f21(x2752,x2753))+E(x2751,a1)+E(f21(x2751,f18(x2752,x2753,x2751)),x2753)+~P4(f22(f22(x2752,x2753),x2751),f22(f22(a26,a27),a29))+E(f21(x2751,f19(x2752,x2753,x2751)),x2752) % 2.03/2.17 [281]~P1(x2811)+~P1(x2813)+~P1(x2812)+E(x2811,a25)+~P3(x2811,f21(x2812,x2813))+E(x2811,a1)+P1(f19(x2812,x2813,x2811))+P1(f18(x2812,x2813,x2811))+~P4(f22(f22(x2812,x2813),x2811),f22(f22(a26,a27),a29))+P1(f17(x2812,x2813,x2811)) % 2.03/2.17 [282]~P1(x2821)+~P1(x2823)+~P1(x2822)+E(x2821,a25)+~P3(x2821,f21(x2822,x2823))+E(x2821,a1)+P1(f19(x2822,x2823,x2821))+P1(f18(x2822,x2823,x2821))+~P4(f22(f22(x2822,x2823),x2821),f22(f22(a26,a27),a29))+P1(f20(x2822,x2823,x2821)) % 2.03/2.17 [289]~P1(x2891)+~P1(x2893)+~P1(x2892)+E(x2891,a25)+P3(f17(x2892,x2893,x2891),x2891)+~P3(x2891,f21(x2892,x2893))+E(x2891,a1)+P1(f18(x2892,x2893,x2891))+~P4(f22(f22(x2892,x2893),x2891),f22(f22(a26,a27),a29))+P1(f19(x2892,x2893,x2891)) % 2.03/2.17 [290]~P1(x2901)+~P1(x2903)+~P1(x2902)+E(x2901,a25)+~P3(x2901,f21(x2902,x2903))+E(x2901,a1)+P1(f17(x2902,x2903,x2901))+P1(f18(x2902,x2903,x2901))+~P4(f22(f22(x2902,x2903),x2901),f22(f22(a26,a27),a29))+E(f21(x2901,f19(x2902,x2903,x2901)),x2902) % 2.03/2.17 [291]~P1(x2911)+~P1(x2913)+~P1(x2912)+E(x2911,a25)+~P3(x2911,f21(x2912,x2913))+E(x2911,a1)+P1(f20(x2912,x2913,x2911))+P1(f18(x2912,x2913,x2911))+~P4(f22(f22(x2912,x2913),x2911),f22(f22(a26,a27),a29))+E(f21(x2911,f19(x2912,x2913,x2911)),x2912) % 2.03/2.17 [292]~P1(x2922)+~P1(x2921)+~P1(x2923)+E(x2921,a25)+~P3(x2921,f21(x2922,x2923))+E(x2921,a1)+P1(f17(x2922,x2923,x2921))+P1(f19(x2922,x2923,x2921))+~P4(f22(f22(x2922,x2923),x2921),f22(f22(a26,a27),a29))+E(f21(x2921,f18(x2922,x2923,x2921)),x2923) % 2.03/2.17 [293]~P1(x2932)+~P1(x2931)+~P1(x2933)+E(x2931,a25)+~P3(x2931,f21(x2932,x2933))+E(x2931,a1)+P1(f20(x2932,x2933,x2931))+P1(f19(x2932,x2933,x2931))+~P4(f22(f22(x2932,x2933),x2931),f22(f22(a26,a27),a29))+E(f21(x2931,f18(x2932,x2933,x2931)),x2933) % 2.03/2.17 [297]~P1(x2971)+~P1(x2973)+~P1(x2972)+E(x2971,a25)+P3(f17(x2972,x2973,x2971),x2971)+~P3(x2971,f21(x2972,x2973))+E(x2971,a1)+P1(f18(x2972,x2973,x2971))+~P4(f22(f22(x2972,x2973),x2971),f22(f22(a26,a27),a29))+E(f21(x2971,f19(x2972,x2973,x2971)),x2972) % 2.03/2.17 [298]~P1(x2982)+~P1(x2981)+~P1(x2983)+E(x2981,a25)+P3(f17(x2982,x2983,x2981),x2981)+~P3(x2981,f21(x2982,x2983))+E(x2981,a1)+P1(f19(x2982,x2983,x2981))+~P4(f22(f22(x2982,x2983),x2981),f22(f22(a26,a27),a29))+E(f21(x2981,f18(x2982,x2983,x2981)),x2983) % 2.03/2.17 [299]P3(x2991,x2992)+~P1(x2991)+~P1(x2993)+~P1(x2992)+E(x2991,a25)+~P3(x2991,f21(x2992,x2993))+E(x2991,a1)+P1(f18(x2992,x2993,x2991))+~P4(f22(f22(x2992,x2993),x2991),f22(f22(a26,a27),a29))+E(f21(f17(x2992,x2993,x2991),f20(x2992,x2993,x2991)),x2991) % 2.03/2.17 [300]P3(x3001,x3003)+~P1(x3002)+~P1(x3003)+~P1(x3001)+E(x3001,a25)+~P3(x3001,f21(x3002,x3003))+E(x3001,a1)+P1(f19(x3002,x3003,x3001))+~P4(f22(f22(x3002,x3003),x3001),f22(f22(a26,a27),a29))+E(f21(f17(x3002,x3003,x3001),f20(x3002,x3003,x3001)),x3001) % 2.03/2.17 [301]~P1(x3012)+~P1(x3011)+~P1(x3013)+E(x3011,a25)+~P3(x3011,f21(x3012,x3013))+E(x3011,a1)+E(f21(x3011,f18(x3012,x3013,x3011)),x3013)+P1(f17(x3012,x3013,x3011))+~P4(f22(f22(x3012,x3013),x3011),f22(f22(a26,a27),a29))+E(f21(x3011,f19(x3012,x3013,x3011)),x3012) % 2.03/2.17 [302]~P1(x3022)+~P1(x3021)+~P1(x3023)+E(x3021,a25)+~P3(x3021,f21(x3022,x3023))+E(x3021,a1)+E(f21(x3021,f18(x3022,x3023,x3021)),x3023)+P1(f20(x3022,x3023,x3021))+~P4(f22(f22(x3022,x3023),x3021),f22(f22(a26,a27),a29))+E(f21(x3021,f19(x3022,x3023,x3021)),x3022) % 2.03/2.17 [303]~P1(x3032)+~P1(x3031)+~P1(x3033)+E(x3031,a25)+P3(f17(x3032,x3033,x3031),x3031)+~P3(x3031,f21(x3032,x3033))+E(x3031,a1)+E(f21(x3031,f18(x3032,x3033,x3031)),x3033)+~P4(f22(f22(x3032,x3033),x3031),f22(f22(a26,a27),a29))+E(f21(x3031,f19(x3032,x3033,x3031)),x3032) % 2.03/2.17 [304]P3(x3041,x3042)+~P1(x3042)+~P1(x3041)+~P1(x3043)+E(x3041,a25)+~P3(x3041,f21(x3042,x3043))+E(x3041,a1)+E(f21(f17(x3042,x3043,x3041),f20(x3042,x3043,x3041)),x3041)+~P4(f22(f22(x3042,x3043),x3041),f22(f22(a26,a27),a29))+E(f21(x3041,f18(x3042,x3043,x3041)),x3043) % 2.03/2.17 [305]P3(x3051,x3053)+~P1(x3052)+~P1(x3053)+~P1(x3051)+E(x3051,a25)+~P3(x3051,f21(x3052,x3053))+E(x3051,a1)+E(f21(f17(x3052,x3053,x3051),f20(x3052,x3053,x3051)),x3051)+~P4(f22(f22(x3052,x3053),x3051),f22(f22(a26,a27),a29))+E(f21(x3051,f19(x3052,x3053,x3051)),x3052) % 2.03/2.17 [309]~P1(x3091)+~P1(x3093)+~P1(x3092)+E(x3091,a25)+~P3(x3091,f21(x3092,x3093))+E(x3091,a1)+P1(f19(x3092,x3093,x3091))+P1(f18(x3092,x3093,x3091))+~P4(f22(f22(x3092,x3093),x3091),f22(f22(a26,a27),a29))+E(f21(f17(x3092,x3093,x3091),f20(x3092,x3093,x3091)),x3091) % 2.03/2.17 [311]~P1(x3111)+~P1(x3113)+~P1(x3112)+E(x3111,a25)+~P3(x3111,f21(x3112,x3113))+E(x3111,a1)+E(f21(f17(x3112,x3113,x3111),f20(x3112,x3113,x3111)),x3111)+P1(f18(x3112,x3113,x3111))+~P4(f22(f22(x3112,x3113),x3111),f22(f22(a26,a27),a29))+E(f21(x3111,f19(x3112,x3113,x3111)),x3112) % 2.03/2.17 [312]~P1(x3122)+~P1(x3121)+~P1(x3123)+E(x3121,a25)+~P3(x3121,f21(x3122,x3123))+E(x3121,a1)+E(f21(f17(x3122,x3123,x3121),f20(x3122,x3123,x3121)),x3121)+P1(f19(x3122,x3123,x3121))+~P4(f22(f22(x3122,x3123),x3121),f22(f22(a26,a27),a29))+E(f21(x3121,f18(x3122,x3123,x3121)),x3123) % 2.03/2.17 [313]~P1(x3132)+~P1(x3131)+~P1(x3133)+E(x3131,a25)+~P3(x3131,f21(x3132,x3133))+E(x3131,a1)+E(f21(x3131,f18(x3132,x3133,x3131)),x3133)+E(f21(f17(x3132,x3133,x3131),f20(x3132,x3133,x3131)),x3131)+~P4(f22(f22(x3132,x3133),x3131),f22(f22(a26,a27),a29))+E(f21(x3131,f19(x3132,x3133,x3131)),x3132) % 2.03/2.17 [190]~P1(x1904)+~P1(x1902)+~P1(x1903)+~P1(x1901)+P3(x1901,x1902)+P3(x1901,x1903)+E(x1901,a25)+E(x1901,a1)+~E(f21(x1901,x1904),f21(x1902,x1903))+~E(f17(x1902,x1903,x1901),a25)+~P4(f22(f22(x1902,x1903),x1901),f22(f22(a26,a27),a29)) % 2.03/2.17 [191]~P1(x1914)+~P1(x1912)+~P1(x1913)+~P1(x1911)+P3(x1911,x1912)+P3(x1911,x1913)+E(x1911,a25)+~E(f17(x1912,x1913,x1911),x1911)+E(x1911,a1)+~E(f21(x1911,x1914),f21(x1912,x1913))+~P4(f22(f22(x1912,x1913),x1911),f22(f22(a26,a27),a29)) % 2.03/2.17 [196]~P1(x1964)+~P1(x1962)+~P1(x1963)+~P1(x1961)+P3(x1961,x1962)+P3(x1961,x1963)+E(x1961,a25)+E(x1961,a1)+~E(f21(x1961,x1964),f21(x1962,x1963))+P1(f17(x1962,x1963,x1961))+~P4(f22(f22(x1962,x1963),x1961),f22(f22(a26,a27),a29)) % 2.03/2.17 [197]~P1(x1974)+~P1(x1972)+~P1(x1973)+~P1(x1971)+P3(x1971,x1972)+P3(x1971,x1973)+E(x1971,a25)+E(x1971,a1)+~E(f21(x1971,x1974),f21(x1972,x1973))+P1(f20(x1972,x1973,x1971))+~P4(f22(f22(x1972,x1973),x1971),f22(f22(a26,a27),a29)) % 2.03/2.17 [202]~P1(x2024)+~P1(x2022)+~P1(x2023)+~P1(x2021)+P3(x2021,x2022)+P3(x2021,x2023)+E(x2021,a25)+P3(f17(x2022,x2023,x2021),x2021)+E(x2021,a1)+~E(f21(x2021,x2024),f21(x2022,x2023))+~P4(f22(f22(x2022,x2023),x2021),f22(f22(a26,a27),a29)) % 2.03/2.17 [208]~P1(x2084)+~P1(x2081)+~P1(x2083)+~P1(x2082)+P3(x2081,x2082)+E(x2081,a25)+E(x2081,a1)+~E(f21(x2082,x2083),f21(x2081,x2084))+~E(f17(x2082,x2083,x2081),a25)+P1(f18(x2082,x2083,x2081))+~P4(f22(f22(x2082,x2083),x2081),f22(f22(a26,a27),a29)) % 2.03/2.17 [209]~P1(x2094)+~P1(x2093)+~P1(x2092)+~P1(x2091)+P3(x2091,x2092)+E(x2091,a25)+E(x2091,a1)+~E(f21(x2091,x2094),f21(x2093,x2092))+~E(f17(x2093,x2092,x2091),a25)+P1(f19(x2093,x2092,x2091))+~P4(f22(f22(x2093,x2092),x2091),f22(f22(a26,a27),a29)) % 2.03/2.17 [210]~P1(x2104)+~P1(x2101)+~P1(x2103)+~P1(x2102)+P3(x2101,x2102)+E(x2101,a25)+~E(f17(x2102,x2103,x2101),x2101)+E(x2101,a1)+~E(f21(x2102,x2103),f21(x2101,x2104))+~P4(f22(f22(x2102,x2103),x2101),f22(f22(a26,a27),a29))+P1(f18(x2102,x2103,x2101)) % 2.03/2.17 [211]~P1(x2114)+~P1(x2113)+~P1(x2112)+~P1(x2111)+P3(x2111,x2112)+E(x2111,a25)+~E(f17(x2113,x2112,x2111),x2111)+E(x2111,a1)+~E(f21(x2111,x2114),f21(x2113,x2112))+~P4(f22(f22(x2113,x2112),x2111),f22(f22(a26,a27),a29))+P1(f19(x2113,x2112,x2111)) % 2.03/2.17 [212]P3(x2121,x2122)+~P1(x2124)+~P1(x2122)+~P1(x2121)+~P1(x2123)+E(x2121,a25)+E(x2121,a1)+~E(f21(x2121,x2124),f21(x2122,x2123))+~E(f17(x2122,x2123,x2121),a25)+~P4(f22(f22(x2122,x2123),x2121),f22(f22(a26,a27),a29))+E(f21(x2121,f18(x2122,x2123,x2121)),x2123) % 2.03/2.17 [213]P3(x2131,x2133)+~P1(x2134)+~P1(x2132)+~P1(x2133)+~P1(x2131)+E(x2131,a25)+E(x2131,a1)+~E(f21(x2131,x2134),f21(x2132,x2133))+~E(f17(x2132,x2133,x2131),a25)+~P4(f22(f22(x2132,x2133),x2131),f22(f22(a26,a27),a29))+E(f21(x2131,f19(x2132,x2133,x2131)),x2132) % 2.03/2.17 [214]P3(x2141,x2142)+~P1(x2144)+~P1(x2142)+~P1(x2141)+~P1(x2143)+E(x2141,a25)+~E(f17(x2142,x2143,x2141),x2141)+E(x2141,a1)+~E(f21(x2141,x2144),f21(x2142,x2143))+~P4(f22(f22(x2142,x2143),x2141),f22(f22(a26,a27),a29))+E(f21(x2141,f18(x2142,x2143,x2141)),x2143) % 2.03/2.17 [215]P3(x2151,x2153)+~P1(x2154)+~P1(x2152)+~P1(x2153)+~P1(x2151)+E(x2151,a25)+~E(f17(x2152,x2153,x2151),x2151)+E(x2151,a1)+~E(f21(x2151,x2154),f21(x2152,x2153))+~P4(f22(f22(x2152,x2153),x2151),f22(f22(a26,a27),a29))+E(f21(x2151,f19(x2152,x2153,x2151)),x2152) % 2.03/2.17 [225]~P1(x2254)+~P1(x2251)+~P1(x2253)+~P1(x2252)+P3(x2251,x2252)+E(x2251,a25)+E(x2251,a1)+~E(f21(x2252,x2253),f21(x2251,x2254))+P1(f18(x2252,x2253,x2251))+~P4(f22(f22(x2252,x2253),x2251),f22(f22(a26,a27),a29))+P1(f17(x2252,x2253,x2251)) % 2.03/2.17 [226]~P1(x2264)+~P1(x2261)+~P1(x2263)+~P1(x2262)+P3(x2261,x2262)+E(x2261,a25)+E(x2261,a1)+~E(f21(x2262,x2263),f21(x2261,x2264))+P1(f18(x2262,x2263,x2261))+~P4(f22(f22(x2262,x2263),x2261),f22(f22(a26,a27),a29))+P1(f20(x2262,x2263,x2261)) % 2.03/2.17 [227]~P1(x2274)+~P1(x2273)+~P1(x2272)+~P1(x2271)+P3(x2271,x2272)+E(x2271,a25)+E(x2271,a1)+~E(f21(x2271,x2274),f21(x2273,x2272))+P1(f19(x2273,x2272,x2271))+~P4(f22(f22(x2273,x2272),x2271),f22(f22(a26,a27),a29))+P1(f17(x2273,x2272,x2271)) % 2.03/2.17 [228]~P1(x2284)+~P1(x2283)+~P1(x2282)+~P1(x2281)+P3(x2281,x2282)+E(x2281,a25)+E(x2281,a1)+~E(f21(x2281,x2284),f21(x2283,x2282))+P1(f19(x2283,x2282,x2281))+~P4(f22(f22(x2283,x2282),x2281),f22(f22(a26,a27),a29))+P1(f20(x2283,x2282,x2281)) % 2.03/2.17 [232]~P1(x2324)+~P1(x2321)+~P1(x2323)+~P1(x2322)+P3(x2321,x2322)+E(x2321,a25)+P3(f17(x2322,x2323,x2321),x2321)+E(x2321,a1)+~E(f21(x2322,x2323),f21(x2321,x2324))+~P4(f22(f22(x2322,x2323),x2321),f22(f22(a26,a27),a29))+P1(f18(x2322,x2323,x2321)) % 2.03/2.17 [233]~P1(x2334)+~P1(x2333)+~P1(x2332)+~P1(x2331)+P3(x2331,x2332)+E(x2331,a25)+P3(f17(x2333,x2332,x2331),x2331)+E(x2331,a1)+~E(f21(x2331,x2334),f21(x2333,x2332))+~P4(f22(f22(x2333,x2332),x2331),f22(f22(a26,a27),a29))+P1(f19(x2333,x2332,x2331)) % 2.03/2.17 [234]P3(x2341,x2342)+~P1(x2344)+~P1(x2342)+~P1(x2341)+~P1(x2343)+E(x2341,a25)+E(x2341,a1)+~E(f21(x2341,x2344),f21(x2342,x2343))+P1(f17(x2342,x2343,x2341))+~P4(f22(f22(x2342,x2343),x2341),f22(f22(a26,a27),a29))+E(f21(x2341,f18(x2342,x2343,x2341)),x2343) % 2.03/2.17 [235]P3(x2351,x2352)+~P1(x2354)+~P1(x2352)+~P1(x2351)+~P1(x2353)+E(x2351,a25)+E(x2351,a1)+~E(f21(x2351,x2354),f21(x2352,x2353))+P1(f20(x2352,x2353,x2351))+~P4(f22(f22(x2352,x2353),x2351),f22(f22(a26,a27),a29))+E(f21(x2351,f18(x2352,x2353,x2351)),x2353) % 2.03/2.17 [236]P3(x2361,x2363)+~P1(x2364)+~P1(x2362)+~P1(x2363)+~P1(x2361)+E(x2361,a25)+E(x2361,a1)+~E(f21(x2361,x2364),f21(x2362,x2363))+P1(f17(x2362,x2363,x2361))+~P4(f22(f22(x2362,x2363),x2361),f22(f22(a26,a27),a29))+E(f21(x2361,f19(x2362,x2363,x2361)),x2362) % 2.03/2.17 [237]P3(x2371,x2373)+~P1(x2374)+~P1(x2372)+~P1(x2373)+~P1(x2371)+E(x2371,a25)+E(x2371,a1)+~E(f21(x2371,x2374),f21(x2372,x2373))+P1(f20(x2372,x2373,x2371))+~P4(f22(f22(x2372,x2373),x2371),f22(f22(a26,a27),a29))+E(f21(x2371,f19(x2372,x2373,x2371)),x2372) % 2.03/2.17 [245]P3(x2451,x2452)+~P1(x2454)+~P1(x2452)+~P1(x2451)+~P1(x2453)+E(x2451,a25)+P3(f17(x2452,x2453,x2451),x2451)+E(x2451,a1)+~E(f21(x2451,x2454),f21(x2452,x2453))+~P4(f22(f22(x2452,x2453),x2451),f22(f22(a26,a27),a29))+E(f21(x2451,f18(x2452,x2453,x2451)),x2453) % 2.03/2.17 [246]P3(x2461,x2463)+~P1(x2464)+~P1(x2462)+~P1(x2463)+~P1(x2461)+E(x2461,a25)+P3(f17(x2462,x2463,x2461),x2461)+E(x2461,a1)+~E(f21(x2461,x2464),f21(x2462,x2463))+~P4(f22(f22(x2462,x2463),x2461),f22(f22(a26,a27),a29))+E(f21(x2461,f19(x2462,x2463,x2461)),x2462) % 2.03/2.17 [247]P3(x2471,x2472)+P3(x2471,x2473)+~P1(x2474)+~P1(x2472)+~P1(x2473)+~P1(x2471)+E(x2471,a25)+E(x2471,a1)+~E(f21(x2471,x2474),f21(x2472,x2473))+~P4(f22(f22(x2472,x2473),x2471),f22(f22(a26,a27),a29))+E(f21(f17(x2472,x2473,x2471),f20(x2472,x2473,x2471)),x2471) % 2.03/2.17 [258]~P1(x2584)+~P1(x2581)+~P1(x2583)+~P1(x2582)+E(x2581,a25)+E(x2581,a1)+~E(f21(x2582,x2583),f21(x2581,x2584))+P1(f18(x2582,x2583,x2581))+~E(f17(x2582,x2583,x2581),a25)+~P4(f22(f22(x2582,x2583),x2581),f22(f22(a26,a27),a29))+P1(f19(x2582,x2583,x2581)) % 2.03/2.17 [259]~P1(x2594)+~P1(x2591)+~P1(x2593)+~P1(x2592)+E(x2591,a25)+~E(f17(x2592,x2593,x2591),x2591)+E(x2591,a1)+~E(f21(x2592,x2593),f21(x2591,x2594))+P1(f18(x2592,x2593,x2591))+~P4(f22(f22(x2592,x2593),x2591),f22(f22(a26,a27),a29))+P1(f19(x2592,x2593,x2591)) % 2.03/2.17 [260]~P1(x2604)+~P1(x2601)+~P1(x2603)+~P1(x2602)+E(x2601,a25)+E(x2601,a1)+~E(f21(x2602,x2603),f21(x2601,x2604))+P1(f18(x2602,x2603,x2601))+~E(f17(x2602,x2603,x2601),a25)+~P4(f22(f22(x2602,x2603),x2601),f22(f22(a26,a27),a29))+E(f21(x2601,f19(x2602,x2603,x2601)),x2602) % 2.03/2.17 [261]~P1(x2614)+~P1(x2612)+~P1(x2611)+~P1(x2613)+E(x2611,a25)+E(x2611,a1)+~E(f21(x2611,x2614),f21(x2612,x2613))+P1(f19(x2612,x2613,x2611))+~E(f17(x2612,x2613,x2611),a25)+~P4(f22(f22(x2612,x2613),x2611),f22(f22(a26,a27),a29))+E(f21(x2611,f18(x2612,x2613,x2611)),x2613) % 2.03/2.17 [262]~P1(x2624)+~P1(x2621)+~P1(x2623)+~P1(x2622)+E(x2621,a25)+~E(f17(x2622,x2623,x2621),x2621)+E(x2621,a1)+~E(f21(x2622,x2623),f21(x2621,x2624))+P1(f18(x2622,x2623,x2621))+~P4(f22(f22(x2622,x2623),x2621),f22(f22(a26,a27),a29))+E(f21(x2621,f19(x2622,x2623,x2621)),x2622) % 2.03/2.17 [263]~P1(x2634)+~P1(x2632)+~P1(x2631)+~P1(x2633)+E(x2631,a25)+~E(f17(x2632,x2633,x2631),x2631)+E(x2631,a1)+~E(f21(x2631,x2634),f21(x2632,x2633))+P1(f19(x2632,x2633,x2631))+~P4(f22(f22(x2632,x2633),x2631),f22(f22(a26,a27),a29))+E(f21(x2631,f18(x2632,x2633,x2631)),x2633) % 2.03/2.17 [266]~P1(x2664)+~P1(x2662)+~P1(x2661)+~P1(x2663)+E(x2661,a25)+E(x2661,a1)+~E(f21(x2661,x2664),f21(x2662,x2663))+E(f21(x2661,f18(x2662,x2663,x2661)),x2663)+~E(f17(x2662,x2663,x2661),a25)+~P4(f22(f22(x2662,x2663),x2661),f22(f22(a26,a27),a29))+E(f21(x2661,f19(x2662,x2663,x2661)),x2662) % 2.03/2.17 [267]~P1(x2674)+~P1(x2672)+~P1(x2671)+~P1(x2673)+E(x2671,a25)+~E(f17(x2672,x2673,x2671),x2671)+E(x2671,a1)+~E(f21(x2671,x2674),f21(x2672,x2673))+E(f21(x2671,f18(x2672,x2673,x2671)),x2673)+~P4(f22(f22(x2672,x2673),x2671),f22(f22(a26,a27),a29))+E(f21(x2671,f19(x2672,x2673,x2671)),x2672) % 2.03/2.17 [272]~P1(x2724)+~P1(x2721)+~P1(x2723)+~P1(x2722)+E(x2721,a25)+E(x2721,a1)+~E(f21(x2722,x2723),f21(x2721,x2724))+P1(f19(x2722,x2723,x2721))+P1(f18(x2722,x2723,x2721))+~P4(f22(f22(x2722,x2723),x2721),f22(f22(a26,a27),a29))+P1(f17(x2722,x2723,x2721)) % 2.03/2.17 [273]~P1(x2734)+~P1(x2731)+~P1(x2733)+~P1(x2732)+E(x2731,a25)+E(x2731,a1)+~E(f21(x2732,x2733),f21(x2731,x2734))+P1(f19(x2732,x2733,x2731))+P1(f18(x2732,x2733,x2731))+~P4(f22(f22(x2732,x2733),x2731),f22(f22(a26,a27),a29))+P1(f20(x2732,x2733,x2731)) % 2.03/2.17 [276]~P1(x2764)+~P1(x2761)+~P1(x2763)+~P1(x2762)+E(x2761,a25)+P3(f17(x2762,x2763,x2761),x2761)+E(x2761,a1)+~E(f21(x2762,x2763),f21(x2761,x2764))+P1(f18(x2762,x2763,x2761))+~P4(f22(f22(x2762,x2763),x2761),f22(f22(a26,a27),a29))+P1(f19(x2762,x2763,x2761)) % 2.03/2.17 [277]~P1(x2774)+~P1(x2771)+~P1(x2773)+~P1(x2772)+E(x2771,a25)+E(x2771,a1)+~E(f21(x2772,x2773),f21(x2771,x2774))+P1(f17(x2772,x2773,x2771))+P1(f18(x2772,x2773,x2771))+~P4(f22(f22(x2772,x2773),x2771),f22(f22(a26,a27),a29))+E(f21(x2771,f19(x2772,x2773,x2771)),x2772) % 2.03/2.17 [278]~P1(x2784)+~P1(x2781)+~P1(x2783)+~P1(x2782)+E(x2781,a25)+E(x2781,a1)+~E(f21(x2782,x2783),f21(x2781,x2784))+P1(f20(x2782,x2783,x2781))+P1(f18(x2782,x2783,x2781))+~P4(f22(f22(x2782,x2783),x2781),f22(f22(a26,a27),a29))+E(f21(x2781,f19(x2782,x2783,x2781)),x2782) % 2.03/2.17 [279]~P1(x2794)+~P1(x2792)+~P1(x2791)+~P1(x2793)+E(x2791,a25)+E(x2791,a1)+~E(f21(x2791,x2794),f21(x2792,x2793))+P1(f17(x2792,x2793,x2791))+P1(f19(x2792,x2793,x2791))+~P4(f22(f22(x2792,x2793),x2791),f22(f22(a26,a27),a29))+E(f21(x2791,f18(x2792,x2793,x2791)),x2793) % 2.03/2.17 [280]~P1(x2804)+~P1(x2802)+~P1(x2801)+~P1(x2803)+E(x2801,a25)+E(x2801,a1)+~E(f21(x2801,x2804),f21(x2802,x2803))+P1(f20(x2802,x2803,x2801))+P1(f19(x2802,x2803,x2801))+~P4(f22(f22(x2802,x2803),x2801),f22(f22(a26,a27),a29))+E(f21(x2801,f18(x2802,x2803,x2801)),x2803) % 2.03/2.17 [283]~P1(x2834)+~P1(x2831)+~P1(x2833)+~P1(x2832)+E(x2831,a25)+P3(f17(x2832,x2833,x2831),x2831)+E(x2831,a1)+~E(f21(x2832,x2833),f21(x2831,x2834))+P1(f18(x2832,x2833,x2831))+~P4(f22(f22(x2832,x2833),x2831),f22(f22(a26,a27),a29))+E(f21(x2831,f19(x2832,x2833,x2831)),x2832) % 2.03/2.17 [284]~P1(x2844)+~P1(x2842)+~P1(x2841)+~P1(x2843)+E(x2841,a25)+P3(f17(x2842,x2843,x2841),x2841)+E(x2841,a1)+~E(f21(x2841,x2844),f21(x2842,x2843))+P1(f19(x2842,x2843,x2841))+~P4(f22(f22(x2842,x2843),x2841),f22(f22(a26,a27),a29))+E(f21(x2841,f18(x2842,x2843,x2841)),x2843) % 2.03/2.17 [285]P3(x2851,x2852)+~P1(x2854)+~P1(x2851)+~P1(x2853)+~P1(x2852)+E(x2851,a25)+E(x2851,a1)+~E(f21(x2852,x2853),f21(x2851,x2854))+P1(f18(x2852,x2853,x2851))+~P4(f22(f22(x2852,x2853),x2851),f22(f22(a26,a27),a29))+E(f21(f17(x2852,x2853,x2851),f20(x2852,x2853,x2851)),x2851) % 2.03/2.17 [286]P3(x2861,x2863)+~P1(x2864)+~P1(x2862)+~P1(x2863)+~P1(x2861)+E(x2861,a25)+E(x2861,a1)+~E(f21(x2861,x2864),f21(x2862,x2863))+P1(f19(x2862,x2863,x2861))+~P4(f22(f22(x2862,x2863),x2861),f22(f22(a26,a27),a29))+E(f21(f17(x2862,x2863,x2861),f20(x2862,x2863,x2861)),x2861) % 2.03/2.17 [287]~P1(x2874)+~P1(x2872)+~P1(x2871)+~P1(x2873)+E(x2871,a25)+E(x2871,a1)+~E(f21(x2871,x2874),f21(x2872,x2873))+E(f21(x2871,f18(x2872,x2873,x2871)),x2873)+P1(f17(x2872,x2873,x2871))+~P4(f22(f22(x2872,x2873),x2871),f22(f22(a26,a27),a29))+E(f21(x2871,f19(x2872,x2873,x2871)),x2872) % 2.03/2.17 [288]~P1(x2884)+~P1(x2882)+~P1(x2881)+~P1(x2883)+E(x2881,a25)+E(x2881,a1)+~E(f21(x2881,x2884),f21(x2882,x2883))+E(f21(x2881,f18(x2882,x2883,x2881)),x2883)+P1(f20(x2882,x2883,x2881))+~P4(f22(f22(x2882,x2883),x2881),f22(f22(a26,a27),a29))+E(f21(x2881,f19(x2882,x2883,x2881)),x2882) % 2.03/2.17 [294]~P1(x2944)+~P1(x2942)+~P1(x2941)+~P1(x2943)+E(x2941,a25)+P3(f17(x2942,x2943,x2941),x2941)+E(x2941,a1)+~E(f21(x2941,x2944),f21(x2942,x2943))+E(f21(x2941,f18(x2942,x2943,x2941)),x2943)+~P4(f22(f22(x2942,x2943),x2941),f22(f22(a26,a27),a29))+E(f21(x2941,f19(x2942,x2943,x2941)),x2942) % 2.03/2.17 [295]P3(x2951,x2952)+~P1(x2954)+~P1(x2952)+~P1(x2951)+~P1(x2953)+E(x2951,a25)+E(x2951,a1)+~E(f21(x2951,x2954),f21(x2952,x2953))+E(f21(f17(x2952,x2953,x2951),f20(x2952,x2953,x2951)),x2951)+~P4(f22(f22(x2952,x2953),x2951),f22(f22(a26,a27),a29))+E(f21(x2951,f18(x2952,x2953,x2951)),x2953) % 2.03/2.17 [296]P3(x2961,x2963)+~P1(x2964)+~P1(x2962)+~P1(x2963)+~P1(x2961)+E(x2961,a25)+E(x2961,a1)+~E(f21(x2961,x2964),f21(x2962,x2963))+E(f21(f17(x2962,x2963,x2961),f20(x2962,x2963,x2961)),x2961)+~P4(f22(f22(x2962,x2963),x2961),f22(f22(a26,a27),a29))+E(f21(x2961,f19(x2962,x2963,x2961)),x2962) % 2.03/2.17 [306]~P1(x3064)+~P1(x3061)+~P1(x3063)+~P1(x3062)+E(x3061,a25)+E(x3061,a1)+~E(f21(x3062,x3063),f21(x3061,x3064))+P1(f19(x3062,x3063,x3061))+P1(f18(x3062,x3063,x3061))+~P4(f22(f22(x3062,x3063),x3061),f22(f22(a26,a27),a29))+E(f21(f17(x3062,x3063,x3061),f20(x3062,x3063,x3061)),x3061) % 2.03/2.17 [307]~P1(x3074)+~P1(x3071)+~P1(x3073)+~P1(x3072)+E(x3071,a25)+E(x3071,a1)+~E(f21(x3072,x3073),f21(x3071,x3074))+E(f21(f17(x3072,x3073,x3071),f20(x3072,x3073,x3071)),x3071)+P1(f18(x3072,x3073,x3071))+~P4(f22(f22(x3072,x3073),x3071),f22(f22(a26,a27),a29))+E(f21(x3071,f19(x3072,x3073,x3071)),x3072) % 2.03/2.17 [308]~P1(x3084)+~P1(x3082)+~P1(x3081)+~P1(x3083)+E(x3081,a25)+E(x3081,a1)+~E(f21(x3081,x3084),f21(x3082,x3083))+E(f21(f17(x3082,x3083,x3081),f20(x3082,x3083,x3081)),x3081)+P1(f19(x3082,x3083,x3081))+~P4(f22(f22(x3082,x3083),x3081),f22(f22(a26,a27),a29))+E(f21(x3081,f18(x3082,x3083,x3081)),x3083) % 2.03/2.17 [310]~P1(x3104)+~P1(x3102)+~P1(x3101)+~P1(x3103)+E(x3101,a25)+E(x3101,a1)+~E(f21(x3101,x3104),f21(x3102,x3103))+E(f21(x3101,f18(x3102,x3103,x3101)),x3103)+E(f21(f17(x3102,x3103,x3101),f20(x3102,x3103,x3101)),x3101)+~P4(f22(f22(x3102,x3103),x3101),f22(f22(a26,a27),a29))+E(f21(x3101,f19(x3102,x3103,x3101)),x3102) % 2.03/2.17 %EqnAxiom % 2.03/2.17 [1]E(x11,x11) % 2.03/2.17 [2]E(x22,x21)+~E(x21,x22) % 2.03/2.17 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 2.03/2.17 [4]~E(x41,x42)+E(f21(x41,x43),f21(x42,x43)) % 2.03/2.17 [5]~E(x51,x52)+E(f21(x53,x51),f21(x53,x52)) % 2.03/2.17 [6]~E(x61,x62)+E(f22(x61,x63),f22(x62,x63)) % 2.03/2.17 [7]~E(x71,x72)+E(f22(x73,x71),f22(x73,x72)) % 2.03/2.17 [8]~E(x81,x82)+E(f18(x81,x83,x84),f18(x82,x83,x84)) % 2.03/2.17 [9]~E(x91,x92)+E(f18(x93,x91,x94),f18(x93,x92,x94)) % 2.03/2.17 [10]~E(x101,x102)+E(f18(x103,x104,x101),f18(x103,x104,x102)) % 2.03/2.17 [11]~E(x111,x112)+E(f17(x111,x113,x114),f17(x112,x113,x114)) % 2.03/2.17 [12]~E(x121,x122)+E(f17(x123,x121,x124),f17(x123,x122,x124)) % 2.03/2.17 [13]~E(x131,x132)+E(f17(x133,x134,x131),f17(x133,x134,x132)) % 2.03/2.17 [14]~E(x141,x142)+E(f19(x141,x143,x144),f19(x142,x143,x144)) % 2.03/2.17 [15]~E(x151,x152)+E(f19(x153,x151,x154),f19(x153,x152,x154)) % 2.03/2.17 [16]~E(x161,x162)+E(f19(x163,x164,x161),f19(x163,x164,x162)) % 2.03/2.17 [17]~E(x171,x172)+E(f20(x171,x173,x174),f20(x172,x173,x174)) % 2.03/2.17 [18]~E(x181,x182)+E(f20(x183,x181,x184),f20(x183,x182,x184)) % 2.03/2.17 [19]~E(x191,x192)+E(f20(x193,x194,x191),f20(x193,x194,x192)) % 2.03/2.17 [20]~E(x201,x202)+E(f23(x201,x203),f23(x202,x203)) % 2.03/2.17 [21]~E(x211,x212)+E(f23(x213,x211),f23(x213,x212)) % 2.03/2.17 [22]~E(x221,x222)+E(f14(x221),f14(x222)) % 2.03/2.17 [23]~E(x231,x232)+E(f13(x231),f13(x232)) % 2.03/2.17 [24]~E(x241,x242)+E(f24(x241,x243),f24(x242,x243)) % 2.03/2.17 [25]~E(x251,x252)+E(f24(x253,x251),f24(x253,x252)) % 2.03/2.17 [26]~E(x261,x262)+E(f16(x261,x263),f16(x262,x263)) % 2.03/2.17 [27]~E(x271,x272)+E(f16(x273,x271),f16(x273,x272)) % 2.03/2.17 [28]~E(x281,x282)+E(f15(x281,x283),f15(x282,x283)) % 2.03/2.17 [29]~E(x291,x292)+E(f15(x293,x291),f15(x293,x292)) % 2.03/2.17 [30]~P1(x301)+P1(x302)+~E(x301,x302) % 2.03/2.17 [31]P4(x312,x313)+~E(x311,x312)+~P4(x311,x313) % 2.03/2.17 [32]P4(x323,x322)+~E(x321,x322)+~P4(x323,x321) % 2.03/2.17 [33]P3(x332,x333)+~E(x331,x332)+~P3(x331,x333) % 2.03/2.17 [34]P3(x343,x342)+~E(x341,x342)+~P3(x343,x341) % 2.03/2.17 [35]~P2(x351)+P2(x352)+~E(x351,x352) % 2.03/2.17 [36]P5(x362,x363)+~E(x361,x362)+~P5(x361,x363) % 2.03/2.17 [37]P5(x373,x372)+~E(x371,x372)+~P5(x373,x371) % 2.03/2.17 % 2.03/2.17 %------------------------------------------- % 2.03/2.17 cnf(376,plain, % 2.03/2.17 ($false), % 2.03/2.17 inference(scs_inference,[],[87,75,166]), % 2.03/2.17 ['proof']). % 2.03/2.17 % SZS output end Proof % 2.03/2.17 % Total time :1.130000s %------------------------------------------------------------------------------