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