%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM020+4 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : 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 04:52:47 EDT 2024 % Result : Theorem 62.08s 62.12s % Output : CNFRefutation 62.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : COM020+4 : TPTP v8.2.0. Released v4.0.0. % 0.12/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n028.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Jun 20 23:30:54 EDT 2024 % 0.13/0.34 % CPUTime : % 0.22/0.57 start to proof:theBenchmark % 62.05/62.10 %------------------------------------------- % 62.05/62.10 % File :CSE---1.7 % 62.05/62.10 % Problem :theBenchmark % 62.05/62.10 % Transform :cnf % 62.05/62.10 % Format :tptp:raw % 62.05/62.10 % Command :java -jar mcs_scs.jar %d %s % 62.05/62.10 % 62.05/62.10 % Result :Theorem 60.270000s % 62.05/62.10 % Output :CNFRefutation 60.270000s % 62.05/62.10 %------------------------------------------- % 62.08/62.11 %------------------------------------------------------------------------------ % 62.08/62.11 % File : COM020+4 : TPTP v8.2.0. Released v4.0.0. % 62.08/62.11 % Domain : Computing Theory % 62.08/62.11 % Problem : Newman's lemma on rewriting systems 03_01_05_01, 03 expansion % 62.08/62.11 % Version : Especial. % 62.08/62.11 % English : % 62.08/62.11 % 62.08/62.11 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 62.08/62.11 % : [PV+07] Paskevich et al. (2007), Reasoning Inside a Formula an % 62.08/62.11 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 62.08/62.11 % Source : [Pas08] % 62.08/62.11 % Names : newman_03_01_05_01.03 [Pas08] % 62.08/62.11 % 62.08/62.11 % Status : Theorem % 62.08/62.11 % Rating : 0.39 v8.1.0, 0.36 v7.5.0, 0.41 v7.4.0, 0.30 v7.3.0, 0.31 v7.2.0, 0.28 v7.1.0, 0.22 v7.0.0, 0.27 v6.3.0, 0.25 v6.2.0, 0.40 v6.1.0, 0.50 v6.0.0, 0.48 v5.5.0, 0.56 v5.4.0, 0.57 v5.3.0, 0.63 v5.2.0, 0.45 v5.1.0, 0.52 v5.0.0, 0.54 v4.1.0, 0.57 v4.0.1, 0.70 v4.0.0 % 62.08/62.11 % Syntax : Number of formulae : 24 ( 1 unt; 6 def) % 62.08/62.11 % Number of atoms : 216 ( 14 equ) % 62.08/62.11 % Maximal formula atoms : 33 ( 9 avg) % 62.08/62.11 % Number of connectives : 194 ( 2 ~; 40 |; 117 &) % 62.08/62.11 % ( 6 <=>; 29 =>; 0 <=; 0 <~>) % 62.08/62.11 % Maximal formula depth : 17 ( 8 avg) % 62.08/62.11 % Maximal term depth : 1 ( 1 avg) % 62.08/62.11 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 62.08/62.11 % Number of functors : 8 ( 8 usr; 8 con; 0-0 aty) % 62.08/62.11 % Number of variables : 73 ( 48 !; 25 ?) % 62.08/62.11 % SPC : FOF_THM_RFO_SEQ % 62.08/62.11 % 62.08/62.11 % Comments : Problem generated by the SAD system [VLP07] % 62.08/62.11 %------------------------------------------------------------------------------ % 62.08/62.11 fof(mElmSort,axiom, % 62.08/62.11 ! [W0] : % 62.08/62.11 ( aElement0(W0) % 62.08/62.11 => $true ) ). % 62.08/62.11 % 62.08/62.11 fof(mRelSort,axiom, % 62.08/62.11 ! [W0] : % 62.08/62.11 ( aRewritingSystem0(W0) % 62.08/62.11 => $true ) ). % 62.08/62.11 % 62.08/62.11 fof(mReduct,axiom, % 62.08/62.11 ! [W0,W1] : % 62.08/62.11 ( ( aElement0(W0) % 62.08/62.11 & aRewritingSystem0(W1) ) % 62.08/62.11 => ! [W2] : % 62.08/62.11 ( aReductOfIn0(W2,W0,W1) % 62.08/62.11 => aElement0(W2) ) ) ). % 62.08/62.11 % 62.08/62.11 fof(mWFOrd,axiom, % 62.08/62.11 ! [W0,W1] : % 62.08/62.11 ( ( aElement0(W0) % 62.08/62.11 & aElement0(W1) ) % 62.08/62.11 => ( iLess0(W0,W1) % 62.08/62.11 => $true ) ) ). % 62.08/62.11 % 62.08/62.11 fof(mTCbr,axiom, % 62.08/62.11 ! [W0,W1,W2] : % 62.08/62.11 ( ( aElement0(W0) % 62.08/62.11 & aRewritingSystem0(W1) % 62.08/62.11 & aElement0(W2) ) % 62.08/62.11 => ( sdtmndtplgtdt0(W0,W1,W2) % 62.08/62.11 => $true ) ) ). % 62.08/62.11 % 62.08/62.11 fof(mTCDef,definition, % 62.08/62.11 ! [W0,W1,W2] : % 62.08/62.11 ( ( aElement0(W0) % 62.08/62.11 & aRewritingSystem0(W1) % 62.08/62.11 & aElement0(W2) ) % 62.08/62.11 => ( sdtmndtplgtdt0(W0,W1,W2) % 62.08/62.11 <=> ( aReductOfIn0(W2,W0,W1) % 62.08/62.11 | ? [W3] : % 62.08/62.11 ( aElement0(W3) % 62.08/62.11 & aReductOfIn0(W3,W0,W1) % 62.08/62.11 & sdtmndtplgtdt0(W3,W1,W2) ) ) ) ) ). % 62.08/62.11 % 62.08/62.11 fof(mTCTrans,axiom, % 62.08/62.11 ! [W0,W1,W2,W3] : % 62.08/62.11 ( ( aElement0(W0) % 62.08/62.11 & aRewritingSystem0(W1) % 62.08/62.11 & aElement0(W2) % 62.08/62.11 & aElement0(W3) ) % 62.08/62.11 => ( ( sdtmndtplgtdt0(W0,W1,W2) % 62.08/62.11 & sdtmndtplgtdt0(W2,W1,W3) ) % 62.08/62.11 => sdtmndtplgtdt0(W0,W1,W3) ) ) ). % 62.08/62.11 % 62.08/62.11 fof(mTCRDef,definition, % 62.08/62.11 ! [W0,W1,W2] : % 62.08/62.11 ( ( aElement0(W0) % 62.08/62.11 & aRewritingSystem0(W1) % 62.08/62.11 & aElement0(W2) ) % 62.08/62.11 => ( sdtmndtasgtdt0(W0,W1,W2) % 62.08/62.11 <=> ( W0 = W2 % 62.08/62.11 | sdtmndtplgtdt0(W0,W1,W2) ) ) ) ). % 62.08/62.11 % 62.08/62.11 fof(mTCRTrans,axiom, % 62.08/62.11 ! [W0,W1,W2,W3] : % 62.08/62.11 ( ( aElement0(W0) % 62.08/62.11 & aRewritingSystem0(W1) % 62.08/62.11 & aElement0(W2) % 62.08/62.11 & aElement0(W3) ) % 62.08/62.11 => ( ( sdtmndtasgtdt0(W0,W1,W2) % 62.08/62.11 & sdtmndtasgtdt0(W2,W1,W3) ) % 62.08/62.11 => sdtmndtasgtdt0(W0,W1,W3) ) ) ). % 62.08/62.11 % 62.08/62.11 fof(mCRDef,definition, % 62.08/62.11 ! [W0] : % 62.08/62.11 ( aRewritingSystem0(W0) % 62.08/62.11 => ( isConfluent0(W0) % 62.08/62.11 <=> ! [W1,W2,W3] : % 62.08/62.11 ( ( aElement0(W1) % 62.08/62.11 & aElement0(W2) % 62.08/62.11 & aElement0(W3) % 62.08/62.11 & sdtmndtasgtdt0(W1,W0,W2) % 62.08/62.11 & sdtmndtasgtdt0(W1,W0,W3) ) % 62.08/62.11 => ? [W4] : % 62.08/62.11 ( aElement0(W4) % 62.08/62.11 & sdtmndtasgtdt0(W2,W0,W4) % 62.08/62.11 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 62.08/62.11 % 62.08/62.11 fof(mWCRDef,definition, % 62.08/62.12 ! [W0] : % 62.08/62.12 ( aRewritingSystem0(W0) % 62.08/62.12 => ( isLocallyConfluent0(W0) % 62.08/62.12 <=> ! [W1,W2,W3] : % 62.08/62.12 ( ( aElement0(W1) % 62.08/62.12 & aElement0(W2) % 62.08/62.12 & aElement0(W3) % 62.08/62.12 & aReductOfIn0(W2,W1,W0) % 62.08/62.12 & aReductOfIn0(W3,W1,W0) ) % 62.08/62.12 => ? [W4] : % 62.08/62.12 ( aElement0(W4) % 62.08/62.12 & sdtmndtasgtdt0(W2,W0,W4) % 62.08/62.12 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 62.08/62.12 % 62.08/62.12 fof(mTermin,definition, % 62.08/62.12 ! [W0] : % 62.08/62.12 ( aRewritingSystem0(W0) % 62.08/62.12 => ( isTerminating0(W0) % 62.08/62.12 <=> ! [W1,W2] : % 62.08/62.12 ( ( aElement0(W1) % 62.08/62.12 & aElement0(W2) ) % 62.08/62.12 => ( sdtmndtplgtdt0(W1,W0,W2) % 62.08/62.12 => iLess0(W2,W1) ) ) ) ) ). % 62.08/62.12 % 62.08/62.12 fof(mNFRDef,definition, % 62.08/62.12 ! [W0,W1] : % 62.08/62.12 ( ( aElement0(W0) % 62.08/62.12 & aRewritingSystem0(W1) ) % 62.08/62.12 => ! [W2] : % 62.08/62.12 ( aNormalFormOfIn0(W2,W0,W1) % 62.08/62.12 <=> ( aElement0(W2) % 62.08/62.12 & sdtmndtasgtdt0(W0,W1,W2) % 62.08/62.12 & ~ ? [W3] : aReductOfIn0(W3,W2,W1) ) ) ) ). % 62.08/62.12 % 62.08/62.12 fof(mTermNF,axiom, % 62.08/62.12 ! [W0] : % 62.08/62.12 ( ( aRewritingSystem0(W0) % 62.08/62.12 & isTerminating0(W0) ) % 62.08/62.12 => ! [W1] : % 62.08/62.12 ( aElement0(W1) % 62.08/62.12 => ? [W2] : aNormalFormOfIn0(W2,W1,W0) ) ) ). % 62.08/62.12 % 62.08/62.12 fof(m__656,hypothesis, % 62.08/62.12 aRewritingSystem0(xR) ). % 62.08/62.12 % 62.08/62.12 fof(m__656_01,hypothesis, % 62.08/62.12 ( ! [W0,W1,W2] : % 62.08/62.12 ( ( aElement0(W0) % 62.08/62.12 & aElement0(W1) % 62.08/62.12 & aElement0(W2) % 62.08/62.12 & aReductOfIn0(W1,W0,xR) % 62.08/62.12 & aReductOfIn0(W2,W0,xR) ) % 62.08/62.12 => ? [W3] : % 62.08/62.12 ( aElement0(W3) % 62.08/62.12 & ( W1 = W3 % 62.08/62.12 | ( ( aReductOfIn0(W3,W1,xR) % 62.08/62.12 | ? [W4] : % 62.08/62.12 ( aElement0(W4) % 62.08/62.12 & aReductOfIn0(W4,W1,xR) % 62.08/62.12 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 62.08/62.12 & sdtmndtplgtdt0(W1,xR,W3) ) ) % 62.08/62.12 & sdtmndtasgtdt0(W1,xR,W3) % 62.08/62.12 & ( W2 = W3 % 62.08/62.12 | ( ( aReductOfIn0(W3,W2,xR) % 62.08/62.12 | ? [W4] : % 62.08/62.12 ( aElement0(W4) % 62.08/62.12 & aReductOfIn0(W4,W2,xR) % 62.08/62.12 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 62.08/62.12 & sdtmndtplgtdt0(W2,xR,W3) ) ) % 62.08/62.12 & sdtmndtasgtdt0(W2,xR,W3) ) ) % 62.08/62.12 & isLocallyConfluent0(xR) % 62.08/62.12 & ! [W0,W1] : % 62.08/62.12 ( ( aElement0(W0) % 62.08/62.12 & aElement0(W1) ) % 62.08/62.12 => ( ( aReductOfIn0(W1,W0,xR) % 62.08/62.12 | ? [W2] : % 62.08/62.12 ( aElement0(W2) % 62.08/62.12 & aReductOfIn0(W2,W0,xR) % 62.08/62.12 & sdtmndtplgtdt0(W2,xR,W1) ) % 62.08/62.12 | sdtmndtplgtdt0(W0,xR,W1) ) % 62.08/62.12 => iLess0(W1,W0) ) ) % 62.08/62.12 & isTerminating0(xR) ) ). % 62.08/62.12 % 62.08/62.12 fof(m__731,hypothesis, % 62.08/62.12 ( aElement0(xa) % 62.08/62.12 & aElement0(xb) % 62.08/62.12 & aElement0(xc) ) ). % 62.08/62.12 % 62.08/62.12 fof(m__715,hypothesis, % 62.08/62.12 ! [W0,W1,W2] : % 62.08/62.12 ( ( aElement0(W0) % 62.08/62.12 & aElement0(W1) % 62.08/62.12 & aElement0(W2) % 62.08/62.12 & ( W0 = W1 % 62.08/62.12 | aReductOfIn0(W1,W0,xR) % 62.08/62.12 | ? [W3] : % 62.08/62.12 ( aElement0(W3) % 62.08/62.12 & aReductOfIn0(W3,W0,xR) % 62.08/62.12 & sdtmndtplgtdt0(W3,xR,W1) ) % 62.08/62.12 | sdtmndtplgtdt0(W0,xR,W1) % 62.08/62.12 | sdtmndtasgtdt0(W0,xR,W1) ) % 62.08/62.12 & ( W0 = W2 % 62.08/62.12 | aReductOfIn0(W2,W0,xR) % 62.08/62.12 | ? [W3] : % 62.08/62.12 ( aElement0(W3) % 62.08/62.12 & aReductOfIn0(W3,W0,xR) % 62.08/62.12 & sdtmndtplgtdt0(W3,xR,W2) ) % 62.08/62.12 | sdtmndtplgtdt0(W0,xR,W2) % 62.08/62.12 | sdtmndtasgtdt0(W0,xR,W2) ) ) % 62.08/62.12 => ( iLess0(W0,xa) % 62.08/62.12 => ? [W3] : % 62.08/62.12 ( aElement0(W3) % 62.08/62.12 & ( W1 = W3 % 62.08/62.12 | ( ( aReductOfIn0(W3,W1,xR) % 62.08/62.12 | ? [W4] : % 62.08/62.12 ( aElement0(W4) % 62.08/62.12 & aReductOfIn0(W4,W1,xR) % 62.08/62.12 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 62.08/62.12 & sdtmndtplgtdt0(W1,xR,W3) ) ) % 62.08/62.12 & sdtmndtasgtdt0(W1,xR,W3) % 62.08/62.12 & ( W2 = W3 % 62.08/62.12 | ( ( aReductOfIn0(W3,W2,xR) % 62.08/62.12 | ? [W4] : % 62.08/62.12 ( aElement0(W4) % 62.08/62.12 & aReductOfIn0(W4,W2,xR) % 62.08/62.12 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 62.08/62.12 & sdtmndtplgtdt0(W2,xR,W3) ) ) % 62.08/62.12 & sdtmndtasgtdt0(W2,xR,W3) ) ) ) ). % 62.08/62.12 % 62.08/62.12 fof(m__731_02,hypothesis, % 62.08/62.12 ( ( aReductOfIn0(xb,xa,xR) % 62.08/62.12 | ? [W0] : % 62.08/62.12 ( aElement0(W0) % 62.08/62.12 & aReductOfIn0(W0,xa,xR) % 62.08/62.12 & sdtmndtplgtdt0(W0,xR,xb) ) ) % 62.08/62.12 & sdtmndtplgtdt0(xa,xR,xb) % 62.08/62.12 & ( aReductOfIn0(xc,xa,xR) % 62.08/62.12 | ? [W0] : % 62.08/62.12 ( aElement0(W0) % 62.08/62.12 & aReductOfIn0(W0,xa,xR) % 62.08/62.12 & sdtmndtplgtdt0(W0,xR,xc) ) ) % 62.08/62.12 & sdtmndtplgtdt0(xa,xR,xc) ) ). % 62.08/62.12 % 62.08/62.12 fof(m__755,hypothesis, % 62.08/62.12 ( aElement0(xu) % 62.08/62.12 & aReductOfIn0(xu,xa,xR) % 62.08/62.12 & ( xu = xb % 62.08/62.12 | ( ( aReductOfIn0(xb,xu,xR) % 62.08/62.12 | ? [W0] : % 62.08/62.12 ( aElement0(W0) % 62.08/62.12 & aReductOfIn0(W0,xu,xR) % 62.08/62.12 & sdtmndtplgtdt0(W0,xR,xb) ) ) % 62.08/62.12 & sdtmndtplgtdt0(xu,xR,xb) ) ) % 62.08/62.12 & sdtmndtasgtdt0(xu,xR,xb) ) ). % 62.08/62.12 % 62.08/62.12 fof(m__779,hypothesis, % 62.08/62.12 ( aElement0(xv) % 62.08/62.12 & aReductOfIn0(xv,xa,xR) % 62.08/62.12 & ( xv = xc % 62.08/62.12 | ( ( aReductOfIn0(xc,xv,xR) % 62.08/62.12 | ? [W0] : % 62.08/62.12 ( aElement0(W0) % 62.08/62.12 & aReductOfIn0(W0,xv,xR) % 62.08/62.12 & sdtmndtplgtdt0(W0,xR,xc) ) ) % 62.08/62.12 & sdtmndtplgtdt0(xv,xR,xc) ) ) % 62.08/62.12 & sdtmndtasgtdt0(xv,xR,xc) ) ). % 62.08/62.12 % 62.08/62.12 fof(m__799,hypothesis, % 62.08/62.12 ( aElement0(xw) % 62.08/62.12 & ( xu = xw % 62.08/62.12 | ( ( aReductOfIn0(xw,xu,xR) % 62.08/62.12 | ? [W0] : % 62.08/62.12 ( aElement0(W0) % 62.08/62.12 & aReductOfIn0(W0,xu,xR) % 62.08/62.12 & sdtmndtplgtdt0(W0,xR,xw) ) ) % 62.08/62.12 & sdtmndtplgtdt0(xu,xR,xw) ) ) % 62.08/62.12 & sdtmndtasgtdt0(xu,xR,xw) % 62.08/62.12 & ( xv = xw % 62.08/62.12 | ( ( aReductOfIn0(xw,xv,xR) % 62.08/62.12 | ? [W0] : % 62.08/62.12 ( aElement0(W0) % 62.08/62.12 & aReductOfIn0(W0,xv,xR) % 62.08/62.12 & sdtmndtplgtdt0(W0,xR,xw) ) ) % 62.08/62.12 & sdtmndtplgtdt0(xv,xR,xw) ) ) % 62.08/62.12 & sdtmndtasgtdt0(xv,xR,xw) ) ). % 62.08/62.12 % 62.08/62.12 fof(m__818,hypothesis, % 62.08/62.12 ( aElement0(xd) % 62.08/62.12 & ( xw = xd % 62.08/62.12 | ( ( aReductOfIn0(xd,xw,xR) % 62.08/62.12 | ? [W0] : % 62.08/62.12 ( aElement0(W0) % 62.08/62.12 & aReductOfIn0(W0,xw,xR) % 62.08/62.12 & sdtmndtplgtdt0(W0,xR,xd) ) ) % 62.08/62.12 & sdtmndtplgtdt0(xw,xR,xd) ) ) % 62.08/62.12 & sdtmndtasgtdt0(xw,xR,xd) % 62.08/62.12 & ~ ? [W0] : aReductOfIn0(W0,xd,xR) % 62.08/62.12 & aNormalFormOfIn0(xd,xw,xR) ) ). % 62.08/62.12 % 62.08/62.12 fof(m__,conjecture, % 62.08/62.12 ? [W0] : % 62.08/62.12 ( aElement0(W0) % 62.08/62.12 & ( xb = W0 % 62.08/62.12 | aReductOfIn0(W0,xb,xR) % 62.08/62.12 | ? [W1] : % 62.08/62.12 ( aElement0(W1) % 62.08/62.12 & aReductOfIn0(W1,xb,xR) % 62.08/62.12 & sdtmndtplgtdt0(W1,xR,W0) ) % 62.08/62.12 | sdtmndtplgtdt0(xb,xR,W0) % 62.08/62.12 | sdtmndtasgtdt0(xb,xR,W0) ) % 62.08/62.12 & ( xd = W0 % 62.08/62.12 | aReductOfIn0(W0,xd,xR) % 62.08/62.12 | ? [W1] : % 62.08/62.12 ( aElement0(W1) % 62.08/62.12 & aReductOfIn0(W1,xd,xR) % 62.08/62.12 & sdtmndtplgtdt0(W1,xR,W0) ) % 62.08/62.12 | sdtmndtplgtdt0(xd,xR,W0) % 62.08/62.12 | sdtmndtasgtdt0(xd,xR,W0) ) ) ). % 62.08/62.12 % 62.08/62.12 %------------------------------------------------------------------------------ % 62.08/62.12 %------------------------------------------- % 62.08/62.12 % Proof found % 62.08/62.12 % SZS status Theorem for theBenchmark % 62.08/62.12 % SZS output start Proof % 62.08/62.12 %ClaNum:464(EqnAxiom:64) % 62.08/62.12 %VarNum:5652(SingletonVarNum:1090) % 62.08/62.12 %MaxLitNum:13 % 62.08/62.12 %MaxfuncDepth:1 % 62.08/62.12 %SharedTerms:72 % 62.08/62.12 %goalClause: 86 115 116 117 118 119 146 147 150 151 152 153 155 173 174 % 62.08/62.12 [65]P1(a1) % 62.08/62.12 [66]P1(a29) % 62.08/62.12 [67]P1(a30) % 62.08/62.12 [68]P1(a31) % 62.08/62.12 [69]P1(a33) % 62.08/62.12 [70]P1(a34) % 62.08/62.12 [71]P1(a32) % 62.08/62.12 [72]P2(a2) % 62.08/62.12 [73]P5(a2) % 62.08/62.12 [74]P8(a2) % 62.08/62.12 [75]P3(a31,a1,a2) % 62.08/62.12 [76]P3(a33,a1,a2) % 62.08/62.12 [77]P9(a1,a2,a29) % 62.08/62.12 [78]P9(a1,a2,a30) % 62.08/62.12 [79]P10(a31,a2,a29) % 62.08/62.12 [80]P10(a31,a2,a34) % 62.08/62.12 [81]P10(a33,a2,a30) % 62.08/62.12 [82]P10(a33,a2,a34) % 62.08/62.12 [83]P10(a34,a2,a32) % 62.08/62.12 [84]P4(a32,a34,a2) % 62.08/62.12 [85]~P3(x851,a32,a2) % 62.08/62.12 [95]E(a31,a29)+P9(a31,a2,a29) % 62.08/62.12 [96]E(a33,a30)+P9(a33,a2,a30) % 62.08/62.12 [97]E(a34,a31)+P9(a31,a2,a34) % 62.08/62.12 [98]E(a34,a33)+P9(a33,a2,a34) % 62.08/62.12 [99]E(a32,a34)+P9(a34,a2,a32) % 62.08/62.12 [100]P1(a6)+P3(a29,a1,a2) % 62.08/62.12 [101]P1(a16)+P3(a30,a1,a2) % 62.08/62.12 [120]P3(a29,a1,a2)+P3(a6,a1,a2) % 62.08/62.12 [121]P3(a29,a1,a2)+P9(a6,a2,a29) % 62.08/62.12 [122]P3(a30,a1,a2)+P3(a16,a1,a2) % 62.08/62.12 [123]P3(a30,a1,a2)+P9(a16,a2,a30) % 62.08/62.12 [103]E(a31,a29)+P1(a17)+P3(a29,a31,a2) % 62.08/62.12 [104]E(a33,a30)+P1(a18)+P3(a30,a33,a2) % 62.08/62.12 [105]E(a34,a31)+P1(a19)+P3(a34,a31,a2) % 62.08/62.12 [106]E(a34,a33)+P1(a20)+P3(a34,a33,a2) % 62.08/62.12 [107]E(a32,a34)+P1(a21)+P3(a32,a34,a2) % 62.08/62.12 [124]E(a31,a29)+P3(a29,a31,a2)+P3(a17,a31,a2) % 62.08/62.12 [125]P3(a29,a31,a2)+E(a31,a29)+P9(a17,a2,a29) % 62.08/62.12 [126]E(a33,a30)+P3(a30,a33,a2)+P3(a18,a33,a2) % 62.08/62.12 [127]P3(a30,a33,a2)+E(a33,a30)+P9(a18,a2,a30) % 62.08/62.12 [128]E(a34,a31)+P3(a34,a31,a2)+P3(a19,a31,a2) % 62.08/62.12 [129]P3(a34,a31,a2)+E(a34,a31)+P9(a19,a2,a34) % 62.08/62.12 [130]E(a34,a33)+P3(a34,a33,a2)+P3(a20,a33,a2) % 62.08/62.12 [131]P3(a34,a33,a2)+E(a34,a33)+P9(a20,a2,a34) % 62.08/62.12 [132]E(a32,a34)+P3(a32,a34,a2)+P3(a21,a34,a2) % 62.08/62.12 [133]P3(a32,a34,a2)+E(a32,a34)+P9(a21,a2,a32) % 62.08/62.12 [86]~P1(x861)+~E(a32,x861)+~E(a29,x861) % 62.08/62.12 [115]~P1(x1151)+~E(a32,x1151)+~P3(x1151,a29,a2) % 62.08/62.12 [116]~P1(x1161)+~E(a29,x1161)+~P9(a32,a2,x1161) % 62.08/62.12 [117]~P1(x1171)+~E(a29,x1171)+~P10(a32,a2,x1171) % 62.08/62.12 [118]~P1(x1181)+~E(a32,x1181)+~P9(a29,a2,x1181) % 62.08/62.12 [119]~P1(x1191)+~E(a32,x1191)+~P10(a29,a2,x1191) % 62.08/62.12 [146]~P1(x1461)+~P3(x1461,a29,a2)+~P9(a32,a2,x1461) % 62.08/62.12 [147]~P1(x1471)+~P3(x1471,a29,a2)+~P10(a32,a2,x1471) % 62.08/62.12 [150]~P1(x1501)+~P9(a29,a2,x1501)+~P9(a32,a2,x1501) % 62.08/62.12 [151]~P1(x1511)+~P9(a29,a2,x1511)+~P10(a32,a2,x1511) % 62.08/62.12 [152]~P1(x1521)+~P9(a32,a2,x1521)+~P10(a29,a2,x1521) % 62.08/62.12 [153]~P1(x1531)+~P10(a29,a2,x1531)+~P10(a32,a2,x1531) % 62.08/62.12 [87]~P2(x871)+P6(x871)+P1(f3(x871)) % 62.08/62.12 [88]~P2(x881)+P6(x881)+P1(f23(x881)) % 62.08/62.12 [89]~P2(x891)+P6(x891)+P1(f24(x891)) % 62.08/62.12 [90]~P2(x901)+P5(x901)+P1(f25(x901)) % 62.08/62.12 [91]~P2(x911)+P5(x911)+P1(f27(x911)) % 62.08/62.12 [92]~P2(x921)+P5(x921)+P1(f28(x921)) % 62.08/62.12 [93]~P2(x931)+P8(x931)+P1(f4(x931)) % 62.08/62.12 [94]~P2(x941)+P8(x941)+P1(f5(x941)) % 62.08/62.12 [102]~P2(x1021)+P8(x1021)+~P7(f5(x1021),f4(x1021)) % 62.08/62.12 [108]~P2(x1081)+P6(x1081)+P10(f3(x1081),x1081,f23(x1081)) % 62.08/62.12 [109]~P2(x1091)+P6(x1091)+P10(f3(x1091),x1091,f24(x1091)) % 62.08/62.12 [110]~P2(x1101)+P8(x1101)+P9(f4(x1101),x1101,f5(x1101)) % 62.08/62.12 [111]~P2(x1111)+P5(x1111)+P3(f27(x1111),f25(x1111),x1111) % 62.08/62.12 [112]~P2(x1121)+P5(x1121)+P3(f28(x1121),f25(x1121),x1121) % 62.08/62.12 [137]~P1(x1372)+~P1(x1371)+P7(x1371,x1372)+~P3(x1371,x1372,a2) % 62.08/62.12 [138]~P1(x1381)+~P1(x1382)+P7(x1381,x1382)+~P9(x1382,a2,x1381) % 62.08/62.12 [134]~P1(x1342)+~P2(x1341)+~P8(x1341)+P4(f7(x1341,x1342),x1342,x1341) % 62.08/62.12 [135]~P3(x1351,x1352,x1353)+P1(x1351)+~P1(x1352)+~P2(x1353) % 62.08/62.12 [136]~P4(x1361,x1362,x1363)+P1(x1361)+~P1(x1362)+~P2(x1363) % 62.08/62.12 [140]~P1(x1401)+~P2(x1402)+~P4(x1403,x1401,x1402)+P10(x1401,x1402,x1403) % 62.08/62.12 [156]~P4(x1564,x1561,x1562)+~P1(x1561)+~P3(x1563,x1564,x1562)+~P2(x1562) % 62.08/62.12 [155]~P1(x1551)+~P1(x1552)+~P9(x1552,a2,x1551)+~E(a32,x1551)+~P3(x1552,a29,a2) % 62.08/62.12 [173]~P1(x1731)+~P1(x1732)+~P9(x1731,a2,x1732)+~P3(x1731,a29,a2)+~P9(a32,a2,x1732) % 62.08/62.12 [174]~P1(x1741)+~P1(x1742)+~P9(x1741,a2,x1742)+~P3(x1741,a29,a2)+~P10(a32,a2,x1742) % 62.08/62.12 [160]~P2(x1601)+P6(x1601)+~P1(x1602)+~P10(f23(x1601),x1601,x1602)+~P10(f24(x1601),x1601,x1602) % 62.08/62.12 [161]~P2(x1611)+P5(x1611)+~P1(x1612)+~P10(f27(x1611),x1611,x1612)+~P10(f28(x1611),x1611,x1612) % 62.08/62.12 [113]~E(x1131,x1133)+~P1(x1133)+~P1(x1131)+~P2(x1132)+P10(x1131,x1132,x1133) % 62.08/62.12 [142]~P1(x1421)+~P1(x1423)+~P2(x1422)+~P3(x1423,x1421,x1422)+P9(x1421,x1422,x1423) % 62.08/62.12 [143]~P1(x1433)+~P1(x1431)+~P2(x1432)+~P9(x1431,x1432,x1433)+P10(x1431,x1432,x1433) % 62.08/62.12 [139]~P1(x1391)+~P1(x1392)+~P8(x1393)+~P9(x1392,x1393,x1391)+P7(x1391,x1392)+~P2(x1393) % 62.08/62.12 [144]~P1(x1442)+~P1(x1441)+~P2(x1443)+~P10(x1441,x1443,x1442)+E(x1441,x1442)+P9(x1441,x1443,x1442) % 62.08/62.12 [157]~P1(x1571)+~P1(x1572)+P7(x1571,x1572)+~P1(x1573)+~P3(x1573,x1572,a2)+~P9(x1573,a2,x1571) % 62.08/62.12 [179]~P1(x1791)+~P1(x1792)+~P2(x1793)+~P9(x1792,x1793,x1791)+P3(x1791,x1792,x1793)+P1(f13(x1792,x1793,x1791)) % 62.08/62.12 [192]~P1(x1923)+~P1(x1922)+~P1(x1921)+~P3(x1923,x1921,a2)+~P3(x1922,x1921,a2)+P1(f10(x1921,x1922,x1923)) % 62.08/62.12 [202]~P1(x2021)+~P1(x2022)+~P2(x2023)+~P9(x2022,x2023,x2021)+P3(x2021,x2022,x2023)+P3(f13(x2022,x2023,x2021),x2022,x2023) % 62.08/62.12 [203]~P1(x2031)+~P1(x2032)+~P2(x2033)+~P9(x2032,x2033,x2031)+P3(x2031,x2032,x2033)+P9(f13(x2032,x2033,x2031),x2033,x2031) % 62.08/62.12 [204]~P1(x2042)+~P1(x2041)+~P2(x2043)+~P10(x2042,x2043,x2041)+P4(x2041,x2042,x2043)+P3(f8(x2042,x2043,x2041),x2041,x2043) % 62.08/62.12 [219]~P1(x2193)+~P1(x2192)+~P1(x2191)+~P3(x2193,x2192,a2)+~P3(x2191,x2192,a2)+P10(x2191,a2,f10(x2192,x2193,x2191)) % 62.08/62.12 [220]~P1(x2203)+~P1(x2202)+~P1(x2201)+~P3(x2203,x2202,a2)+~P3(x2201,x2202,a2)+P10(x2201,a2,f10(x2202,x2201,x2203)) % 62.08/62.12 [141]~E(x1411,x1413)+~E(x1411,x1412)+~P1(x1413)+~P1(x1412)+~P1(x1411)+~P7(x1411,a1)+P1(f9(x1411,x1412,x1413)) % 62.08/62.12 [158]~E(x1582,x1583)+~E(x1581,x1582)+~P1(x1583)+~P1(x1582)+~P1(x1581)+~P7(x1582,a1)+P10(x1581,a2,f9(x1582,x1583,x1581)) % 62.08/62.12 [159]~E(x1592,x1593)+~E(x1591,x1592)+~P1(x1593)+~P1(x1592)+~P1(x1591)+~P7(x1592,a1)+P10(x1591,a2,f9(x1592,x1591,x1593)) % 62.08/62.12 [162]~E(x1621,x1623)+~P1(x1623)+~P1(x1622)+~P1(x1621)+~P3(x1622,x1621,a2)+~P7(x1621,a1)+P1(f9(x1621,x1622,x1623)) % 62.08/62.13 [163]~E(x1631,x1632)+~P1(x1633)+~P1(x1632)+~P1(x1631)+~P3(x1633,x1631,a2)+~P7(x1631,a1)+P1(f9(x1631,x1632,x1633)) % 62.08/62.13 [164]~E(x1641,x1643)+~P1(x1643)+~P1(x1642)+~P1(x1641)+~P9(x1641,a2,x1642)+~P7(x1641,a1)+P1(f9(x1641,x1642,x1643)) % 62.08/62.13 [165]~E(x1651,x1653)+~P1(x1653)+~P1(x1652)+~P1(x1651)+~P10(x1651,a2,x1652)+~P7(x1651,a1)+P1(f9(x1651,x1652,x1653)) % 62.08/62.13 [166]~E(x1661,x1662)+~P1(x1663)+~P1(x1662)+~P1(x1661)+~P9(x1661,a2,x1663)+~P7(x1661,a1)+P1(f9(x1661,x1662,x1663)) % 62.08/62.13 [167]~E(x1671,x1672)+~P1(x1673)+~P1(x1672)+~P1(x1671)+~P10(x1671,a2,x1673)+~P7(x1671,a1)+P1(f9(x1671,x1672,x1673)) % 62.08/62.13 [180]~E(x1802,x1803)+~P1(x1803)+~P1(x1802)+~P1(x1801)+~P3(x1801,x1802,a2)+~P7(x1802,a1)+P10(x1801,a2,f9(x1802,x1803,x1801)) % 62.08/62.13 [181]~E(x1811,x1812)+~P1(x1813)+~P1(x1812)+~P1(x1811)+~P3(x1813,x1812,a2)+~P7(x1812,a1)+P10(x1811,a2,f9(x1812,x1813,x1811)) % 62.08/62.13 [182]~E(x1822,x1823)+~P1(x1823)+~P1(x1822)+~P1(x1821)+~P3(x1821,x1822,a2)+~P7(x1822,a1)+P10(x1821,a2,f9(x1822,x1821,x1823)) % 62.08/62.13 [183]~E(x1831,x1832)+~P1(x1833)+~P1(x1832)+~P1(x1831)+~P3(x1833,x1832,a2)+~P7(x1832,a1)+P10(x1831,a2,f9(x1832,x1831,x1833)) % 62.08/62.13 [184]~E(x1842,x1843)+~P1(x1843)+~P1(x1842)+~P1(x1841)+~P9(x1842,a2,x1841)+~P7(x1842,a1)+P10(x1841,a2,f9(x1842,x1843,x1841)) % 62.08/62.13 [185]~E(x1852,x1853)+~P1(x1853)+~P1(x1852)+~P1(x1851)+~P10(x1852,a2,x1851)+~P7(x1852,a1)+P10(x1851,a2,f9(x1852,x1853,x1851)) % 62.08/62.13 [186]~E(x1861,x1862)+~P1(x1863)+~P1(x1862)+~P1(x1861)+~P9(x1862,a2,x1863)+~P7(x1862,a1)+P10(x1861,a2,f9(x1862,x1863,x1861)) % 62.08/62.13 [187]~E(x1871,x1872)+~P1(x1873)+~P1(x1872)+~P1(x1871)+~P10(x1872,a2,x1873)+~P7(x1872,a1)+P10(x1871,a2,f9(x1872,x1873,x1871)) % 62.08/62.13 [188]~E(x1882,x1883)+~P1(x1883)+~P1(x1882)+~P1(x1881)+~P9(x1882,a2,x1881)+~P7(x1882,a1)+P10(x1881,a2,f9(x1882,x1881,x1883)) % 62.08/62.13 [189]~E(x1892,x1893)+~P1(x1893)+~P1(x1892)+~P1(x1891)+~P10(x1892,a2,x1891)+~P7(x1892,a1)+P10(x1891,a2,f9(x1892,x1891,x1893)) % 62.08/62.13 [190]~E(x1901,x1902)+~P1(x1903)+~P1(x1902)+~P1(x1901)+~P9(x1902,a2,x1903)+~P7(x1902,a1)+P10(x1901,a2,f9(x1902,x1901,x1903)) % 62.08/62.13 [191]~E(x1911,x1912)+~P1(x1913)+~P1(x1912)+~P1(x1911)+~P10(x1912,a2,x1913)+~P7(x1912,a1)+P10(x1911,a2,f9(x1912,x1911,x1913)) % 62.08/62.13 [193]~P1(x1933)+~P1(x1932)+~P1(x1931)+~P3(x1933,x1931,a2)+~P3(x1932,x1931,a2)+~P7(x1931,a1)+P1(f9(x1931,x1932,x1933)) % 62.08/62.13 [194]~P1(x1943)+~P1(x1942)+~P1(x1941)+~P3(x1943,x1941,a2)+~P9(x1941,a2,x1942)+~P7(x1941,a1)+P1(f9(x1941,x1942,x1943)) % 62.08/62.13 [195]~P1(x1953)+~P1(x1952)+~P1(x1951)+~P3(x1953,x1951,a2)+~P10(x1951,a2,x1952)+~P7(x1951,a1)+P1(f9(x1951,x1952,x1953)) % 62.08/62.13 [196]~P1(x1963)+~P1(x1962)+~P1(x1961)+~P3(x1962,x1961,a2)+~P9(x1961,a2,x1963)+~P7(x1961,a1)+P1(f9(x1961,x1962,x1963)) % 62.08/62.13 [197]~P1(x1973)+~P1(x1972)+~P1(x1971)+~P3(x1972,x1971,a2)+~P10(x1971,a2,x1973)+~P7(x1971,a1)+P1(f9(x1971,x1972,x1973)) % 62.08/62.13 [198]~P1(x1983)+~P1(x1982)+~P1(x1981)+~P9(x1981,a2,x1983)+~P9(x1981,a2,x1982)+~P7(x1981,a1)+P1(f9(x1981,x1982,x1983)) % 62.08/62.13 [199]~P1(x1993)+~P1(x1992)+~P1(x1991)+~P9(x1991,a2,x1993)+~P10(x1991,a2,x1992)+~P7(x1991,a1)+P1(f9(x1991,x1992,x1993)) % 62.08/62.13 [200]~P1(x2003)+~P1(x2002)+~P1(x2001)+~P9(x2001,a2,x2002)+~P10(x2001,a2,x2003)+~P7(x2001,a1)+P1(f9(x2001,x2002,x2003)) % 62.08/62.13 [201]~P1(x2013)+~P1(x2012)+~P1(x2011)+~P10(x2011,a2,x2013)+~P10(x2011,a2,x2012)+~P7(x2011,a1)+P1(f9(x2011,x2012,x2013)) % 62.08/62.13 [222]~P1(x2223)+~P1(x2222)+~P1(x2221)+~P3(x2223,x2222,a2)+~P3(x2221,x2222,a2)+~P7(x2222,a1)+P10(x2221,a2,f9(x2222,x2223,x2221)) % 62.08/62.13 [223]~P1(x2233)+~P1(x2232)+~P1(x2231)+~P3(x2233,x2232,a2)+~P3(x2231,x2232,a2)+~P7(x2232,a1)+P10(x2231,a2,f9(x2232,x2231,x2233)) % 62.08/62.13 [224]~P1(x2243)+~P1(x2242)+~P1(x2241)+~P3(x2243,x2242,a2)+~P9(x2242,a2,x2241)+~P7(x2242,a1)+P10(x2241,a2,f9(x2242,x2243,x2241)) % 62.08/62.13 [225]~P1(x2253)+~P1(x2252)+~P1(x2251)+~P3(x2253,x2252,a2)+~P10(x2252,a2,x2251)+~P7(x2252,a1)+P10(x2251,a2,f9(x2252,x2253,x2251)) % 62.08/62.13 [226]~P1(x2263)+~P1(x2262)+~P1(x2261)+~P3(x2261,x2262,a2)+~P9(x2262,a2,x2263)+~P7(x2262,a1)+P10(x2261,a2,f9(x2262,x2263,x2261)) % 62.08/62.13 [227]~P1(x2273)+~P1(x2272)+~P1(x2271)+~P3(x2271,x2272,a2)+~P10(x2272,a2,x2273)+~P7(x2272,a1)+P10(x2271,a2,f9(x2272,x2273,x2271)) % 62.08/62.13 [228]~P1(x2283)+~P1(x2282)+~P1(x2281)+~P3(x2283,x2282,a2)+~P9(x2282,a2,x2281)+~P7(x2282,a1)+P10(x2281,a2,f9(x2282,x2281,x2283)) % 62.08/62.13 [229]~P1(x2293)+~P1(x2292)+~P1(x2291)+~P3(x2293,x2292,a2)+~P10(x2292,a2,x2291)+~P7(x2292,a1)+P10(x2291,a2,f9(x2292,x2291,x2293)) % 62.08/62.13 [230]~P1(x2303)+~P1(x2302)+~P1(x2301)+~P3(x2301,x2302,a2)+~P9(x2302,a2,x2303)+~P7(x2302,a1)+P10(x2301,a2,f9(x2302,x2301,x2303)) % 62.08/62.13 [231]~P1(x2313)+~P1(x2312)+~P1(x2311)+~P3(x2311,x2312,a2)+~P10(x2312,a2,x2313)+~P7(x2312,a1)+P10(x2311,a2,f9(x2312,x2311,x2313)) % 62.08/62.13 [232]~P1(x2323)+~P1(x2322)+~P1(x2321)+~P9(x2322,a2,x2323)+~P9(x2322,a2,x2321)+~P7(x2322,a1)+P10(x2321,a2,f9(x2322,x2323,x2321)) % 62.08/62.13 [233]~P1(x2333)+~P1(x2332)+~P1(x2331)+~P9(x2332,a2,x2333)+~P10(x2332,a2,x2331)+~P7(x2332,a1)+P10(x2331,a2,f9(x2332,x2333,x2331)) % 62.08/62.13 [234]~P1(x2343)+~P1(x2342)+~P1(x2341)+~P9(x2342,a2,x2341)+~P10(x2342,a2,x2343)+~P7(x2342,a1)+P10(x2341,a2,f9(x2342,x2343,x2341)) % 62.08/62.13 [235]~P1(x2353)+~P1(x2352)+~P1(x2351)+~P10(x2352,a2,x2353)+~P10(x2352,a2,x2351)+~P7(x2352,a1)+P10(x2351,a2,f9(x2352,x2353,x2351)) % 62.08/62.13 [236]~P1(x2363)+~P1(x2362)+~P1(x2361)+~P9(x2362,a2,x2363)+~P9(x2362,a2,x2361)+~P7(x2362,a1)+P10(x2361,a2,f9(x2362,x2361,x2363)) % 62.08/62.13 [237]~P1(x2373)+~P1(x2372)+~P1(x2371)+~P9(x2372,a2,x2373)+~P10(x2372,a2,x2371)+~P7(x2372,a1)+P10(x2371,a2,f9(x2372,x2371,x2373)) % 62.08/62.13 [238]~P1(x2383)+~P1(x2382)+~P1(x2381)+~P9(x2382,a2,x2381)+~P10(x2382,a2,x2383)+~P7(x2382,a1)+P10(x2381,a2,f9(x2382,x2381,x2383)) % 62.08/62.13 [239]~P1(x2393)+~P1(x2392)+~P1(x2391)+~P10(x2392,a2,x2393)+~P10(x2392,a2,x2391)+~P7(x2392,a1)+P10(x2391,a2,f9(x2392,x2391,x2393)) % 62.08/62.13 [246]~P1(x2462)+~P1(x2461)+~P1(x2463)+~P3(x2462,x2461,a2)+~P3(x2463,x2461,a2)+E(f10(x2461,x2462,x2463),x2463)+P9(x2463,a2,f10(x2461,x2462,x2463)) % 62.08/62.13 [247]~P1(x2473)+~P1(x2471)+~P1(x2472)+~P3(x2473,x2471,a2)+~P3(x2472,x2471,a2)+E(f10(x2471,x2472,x2473),x2472)+P9(x2472,a2,f10(x2471,x2472,x2473)) % 62.08/62.13 [168]~P1(x1683)+~P1(x1681)+~P2(x1682)+~P3(x1684,x1681,x1682)+~P9(x1684,x1682,x1683)+P9(x1681,x1682,x1683)+~P1(x1684) % 62.08/62.13 [169]~P1(x1693)+~P1(x1691)+~P2(x1692)+~P9(x1694,x1692,x1693)+~P9(x1691,x1692,x1694)+P9(x1691,x1692,x1693)+~P1(x1694) % 62.08/62.13 [170]~P1(x1703)+~P1(x1701)+~P2(x1702)+~P10(x1704,x1702,x1703)+~P10(x1701,x1702,x1704)+P10(x1701,x1702,x1703)+~P1(x1704) % 62.08/62.13 [177]~E(x1771,x1772)+~E(x1773,x1771)+~P1(x1772)+~P1(x1771)+~P1(x1773)+~P7(x1771,a1)+E(f9(x1771,x1772,x1773),x1773)+P9(x1773,a2,f9(x1771,x1772,x1773)) % 62.08/62.13 [178]~E(x1781,x1783)+~E(x1782,x1781)+~P1(x1783)+~P1(x1781)+~P1(x1782)+~P7(x1781,a1)+E(f9(x1781,x1782,x1783),x1782)+P9(x1782,a2,f9(x1781,x1782,x1783)) % 62.08/62.13 [207]~E(x2071,x2072)+~P1(x2072)+~P1(x2071)+~P1(x2073)+~P3(x2073,x2071,a2)+~P7(x2071,a1)+E(f9(x2071,x2072,x2073),x2073)+P9(x2073,a2,f9(x2071,x2072,x2073)) % 62.08/62.13 [208]~E(x2083,x2081)+~P1(x2082)+~P1(x2081)+~P1(x2083)+~P3(x2082,x2081,a2)+~P7(x2081,a1)+E(f9(x2081,x2082,x2083),x2083)+P9(x2083,a2,f9(x2081,x2082,x2083)) % 62.08/62.13 [209]~E(x2091,x2093)+~P1(x2093)+~P1(x2091)+~P1(x2092)+~P3(x2092,x2091,a2)+~P7(x2091,a1)+E(f9(x2091,x2092,x2093),x2092)+P9(x2092,a2,f9(x2091,x2092,x2093)) % 62.08/62.13 [210]~E(x2102,x2101)+~P1(x2103)+~P1(x2101)+~P1(x2102)+~P3(x2103,x2101,a2)+~P7(x2101,a1)+E(f9(x2101,x2102,x2103),x2102)+P9(x2102,a2,f9(x2101,x2102,x2103)) % 62.08/62.13 [211]~E(x2111,x2112)+~P1(x2112)+~P1(x2111)+~P1(x2113)+~P9(x2111,a2,x2113)+~P7(x2111,a1)+E(f9(x2111,x2112,x2113),x2113)+P9(x2113,a2,f9(x2111,x2112,x2113)) % 62.08/62.13 [212]~E(x2121,x2122)+~P1(x2122)+~P1(x2121)+~P1(x2123)+~P10(x2121,a2,x2123)+~P7(x2121,a1)+E(f9(x2121,x2122,x2123),x2123)+P9(x2123,a2,f9(x2121,x2122,x2123)) % 62.08/62.13 [213]~E(x2133,x2131)+~P1(x2132)+~P1(x2131)+~P1(x2133)+~P9(x2131,a2,x2132)+~P7(x2131,a1)+E(f9(x2131,x2132,x2133),x2133)+P9(x2133,a2,f9(x2131,x2132,x2133)) % 62.08/62.13 [214]~E(x2143,x2141)+~P1(x2142)+~P1(x2141)+~P1(x2143)+~P10(x2141,a2,x2142)+~P7(x2141,a1)+E(f9(x2141,x2142,x2143),x2143)+P9(x2143,a2,f9(x2141,x2142,x2143)) % 62.08/62.13 [215]~E(x2151,x2153)+~P1(x2153)+~P1(x2151)+~P1(x2152)+~P9(x2151,a2,x2152)+~P7(x2151,a1)+E(f9(x2151,x2152,x2153),x2152)+P9(x2152,a2,f9(x2151,x2152,x2153)) % 62.08/62.13 [216]~E(x2161,x2163)+~P1(x2163)+~P1(x2161)+~P1(x2162)+~P10(x2161,a2,x2162)+~P7(x2161,a1)+E(f9(x2161,x2162,x2163),x2162)+P9(x2162,a2,f9(x2161,x2162,x2163)) % 62.08/62.13 [217]~E(x2172,x2171)+~P1(x2173)+~P1(x2171)+~P1(x2172)+~P9(x2171,a2,x2173)+~P7(x2171,a1)+E(f9(x2171,x2172,x2173),x2172)+P9(x2172,a2,f9(x2171,x2172,x2173)) % 62.08/62.13 [218]~E(x2182,x2181)+~P1(x2183)+~P1(x2181)+~P1(x2182)+~P10(x2181,a2,x2183)+~P7(x2181,a1)+E(f9(x2181,x2182,x2183),x2182)+P9(x2182,a2,f9(x2181,x2182,x2183)) % 62.08/62.13 [256]~P1(x2562)+~P1(x2561)+~P1(x2563)+~P3(x2562,x2561,a2)+~P3(x2563,x2561,a2)+~P7(x2561,a1)+E(f9(x2561,x2562,x2563),x2563)+P9(x2563,a2,f9(x2561,x2562,x2563)) % 62.08/62.13 [257]~P1(x2573)+~P1(x2571)+~P1(x2572)+~P3(x2573,x2571,a2)+~P3(x2572,x2571,a2)+~P7(x2571,a1)+E(f9(x2571,x2572,x2573),x2572)+P9(x2572,a2,f9(x2571,x2572,x2573)) % 62.08/62.13 [258]~P1(x2582)+~P1(x2581)+~P1(x2583)+~P3(x2582,x2581,a2)+~P9(x2581,a2,x2583)+~P7(x2581,a1)+E(f9(x2581,x2582,x2583),x2583)+P9(x2583,a2,f9(x2581,x2582,x2583)) % 62.08/62.13 [259]~P1(x2592)+~P1(x2591)+~P1(x2593)+~P3(x2592,x2591,a2)+~P10(x2591,a2,x2593)+~P7(x2591,a1)+E(f9(x2591,x2592,x2593),x2593)+P9(x2593,a2,f9(x2591,x2592,x2593)) % 62.08/62.13 [260]~P1(x2602)+~P1(x2601)+~P1(x2603)+~P3(x2603,x2601,a2)+~P9(x2601,a2,x2602)+~P7(x2601,a1)+E(f9(x2601,x2602,x2603),x2603)+P9(x2603,a2,f9(x2601,x2602,x2603)) % 62.08/62.13 [261]~P1(x2612)+~P1(x2611)+~P1(x2613)+~P3(x2613,x2611,a2)+~P10(x2611,a2,x2612)+~P7(x2611,a1)+E(f9(x2611,x2612,x2613),x2613)+P9(x2613,a2,f9(x2611,x2612,x2613)) % 62.08/62.13 [262]~P1(x2623)+~P1(x2621)+~P1(x2622)+~P3(x2623,x2621,a2)+~P9(x2621,a2,x2622)+~P7(x2621,a1)+E(f9(x2621,x2622,x2623),x2622)+P9(x2622,a2,f9(x2621,x2622,x2623)) % 62.08/62.13 [263]~P1(x2633)+~P1(x2631)+~P1(x2632)+~P3(x2633,x2631,a2)+~P10(x2631,a2,x2632)+~P7(x2631,a1)+E(f9(x2631,x2632,x2633),x2632)+P9(x2632,a2,f9(x2631,x2632,x2633)) % 62.08/62.13 [264]~P1(x2643)+~P1(x2641)+~P1(x2642)+~P3(x2642,x2641,a2)+~P9(x2641,a2,x2643)+~P7(x2641,a1)+E(f9(x2641,x2642,x2643),x2642)+P9(x2642,a2,f9(x2641,x2642,x2643)) % 62.08/62.13 [265]~P1(x2653)+~P1(x2651)+~P1(x2652)+~P3(x2652,x2651,a2)+~P10(x2651,a2,x2653)+~P7(x2651,a1)+E(f9(x2651,x2652,x2653),x2652)+P9(x2652,a2,f9(x2651,x2652,x2653)) % 62.08/62.13 [266]~P1(x2662)+~P1(x2661)+~P1(x2663)+~P9(x2661,a2,x2662)+~P9(x2661,a2,x2663)+~P7(x2661,a1)+E(f9(x2661,x2662,x2663),x2663)+P9(x2663,a2,f9(x2661,x2662,x2663)) % 62.08/62.13 [267]~P1(x2672)+~P1(x2671)+~P1(x2673)+~P9(x2671,a2,x2672)+~P10(x2671,a2,x2673)+~P7(x2671,a1)+E(f9(x2671,x2672,x2673),x2673)+P9(x2673,a2,f9(x2671,x2672,x2673)) % 62.08/62.13 [268]~P1(x2682)+~P1(x2681)+~P1(x2683)+~P9(x2681,a2,x2683)+~P10(x2681,a2,x2682)+~P7(x2681,a1)+E(f9(x2681,x2682,x2683),x2683)+P9(x2683,a2,f9(x2681,x2682,x2683)) % 62.08/62.13 [269]~P1(x2692)+~P1(x2691)+~P1(x2693)+~P10(x2691,a2,x2692)+~P10(x2691,a2,x2693)+~P7(x2691,a1)+E(f9(x2691,x2692,x2693),x2693)+P9(x2693,a2,f9(x2691,x2692,x2693)) % 62.08/62.13 [270]~P1(x2703)+~P1(x2701)+~P1(x2702)+~P9(x2701,a2,x2703)+~P9(x2701,a2,x2702)+~P7(x2701,a1)+E(f9(x2701,x2702,x2703),x2702)+P9(x2702,a2,f9(x2701,x2702,x2703)) % 62.08/62.13 [271]~P1(x2713)+~P1(x2711)+~P1(x2712)+~P9(x2711,a2,x2713)+~P10(x2711,a2,x2712)+~P7(x2711,a1)+E(f9(x2711,x2712,x2713),x2712)+P9(x2712,a2,f9(x2711,x2712,x2713)) % 62.08/62.13 [272]~P1(x2723)+~P1(x2721)+~P1(x2722)+~P9(x2721,a2,x2722)+~P10(x2721,a2,x2723)+~P7(x2721,a1)+E(f9(x2721,x2722,x2723),x2722)+P9(x2722,a2,f9(x2721,x2722,x2723)) % 62.08/62.13 [273]~P1(x2733)+~P1(x2731)+~P1(x2732)+~P10(x2731,a2,x2733)+~P10(x2731,a2,x2732)+~P7(x2731,a1)+E(f9(x2731,x2732,x2733),x2732)+P9(x2732,a2,f9(x2731,x2732,x2733)) % 62.08/62.13 [315]~P1(x3153)+~P1(x3152)+~P1(x3151)+~P3(x3153,x3151,a2)+~P3(x3152,x3151,a2)+E(f10(x3151,x3152,x3153),x3153)+P3(f10(x3151,x3152,x3153),x3153,a2)+P1(f11(x3151,x3152,x3153)) % 62.08/62.13 [316]~P1(x3163)+~P1(x3162)+~P1(x3161)+~P3(x3163,x3161,a2)+~P3(x3162,x3161,a2)+E(f10(x3161,x3162,x3163),x3162)+P3(f10(x3161,x3162,x3163),x3162,a2)+P1(f12(x3161,x3162,x3163)) % 62.08/62.13 [355]~P1(x3553)+~P1(x3552)+~P1(x3551)+~P3(x3553,x3551,a2)+~P3(x3552,x3551,a2)+E(f10(x3551,x3552,x3553),x3553)+P3(f11(x3551,x3552,x3553),x3553,a2)+P3(f10(x3551,x3552,x3553),x3553,a2) % 62.08/62.13 [356]~P1(x3563)+~P1(x3562)+~P1(x3561)+~P3(x3563,x3561,a2)+~P3(x3562,x3561,a2)+E(f10(x3561,x3562,x3563),x3562)+P3(f12(x3561,x3562,x3563),x3562,a2)+P3(f10(x3561,x3562,x3563),x3562,a2) % 62.08/62.13 [405]~P1(x4053)+~P1(x4052)+~P1(x4051)+~P3(x4053,x4051,a2)+~P3(x4052,x4051,a2)+E(f10(x4051,x4052,x4053),x4053)+P9(f11(x4051,x4052,x4053),a2,f10(x4051,x4052,x4053))+P3(f10(x4051,x4052,x4053),x4053,a2) % 62.08/62.13 [406]~P1(x4063)+~P1(x4062)+~P1(x4061)+~P3(x4063,x4061,a2)+~P3(x4062,x4061,a2)+E(f10(x4061,x4062,x4063),x4062)+P9(f12(x4061,x4062,x4063),a2,f10(x4061,x4062,x4063))+P3(f10(x4061,x4062,x4063),x4062,a2) % 62.08/62.13 [441]~P1(x4414)+~P1(x4413)+~P1(x4412)+~P2(x4411)+~P6(x4411)+~P10(x4412,x4411,x4414)+~P10(x4412,x4411,x4413)+P1(f22(x4411,x4412,x4413,x4414)) % 62.08/62.13 [442]~P1(x4424)+~P1(x4423)+~P1(x4422)+~P2(x4421)+~P5(x4421)+~P3(x4424,x4422,x4421)+~P3(x4423,x4422,x4421)+P1(f26(x4421,x4422,x4423,x4424)) % 62.08/62.13 [445]~P1(x4454)+~P1(x4453)+~P1(x4451)+~P2(x4452)+~P6(x4452)+~P10(x4453,x4452,x4454)+~P10(x4453,x4452,x4451)+P10(x4451,x4452,f22(x4452,x4453,x4454,x4451)) % 62.08/62.13 [446]~P1(x4464)+~P1(x4463)+~P1(x4461)+~P2(x4462)+~P6(x4462)+~P10(x4463,x4462,x4464)+~P10(x4463,x4462,x4461)+P10(x4461,x4462,f22(x4462,x4463,x4461,x4464)) % 62.08/62.13 [447]~P1(x4474)+~P1(x4473)+~P1(x4471)+~P2(x4472)+~P5(x4472)+~P3(x4474,x4473,x4472)+~P3(x4471,x4473,x4472)+P10(x4471,x4472,f26(x4472,x4473,x4474,x4471)) % 62.08/62.13 [448]~P1(x4484)+~P1(x4483)+~P1(x4481)+~P2(x4482)+~P5(x4482)+~P3(x4484,x4483,x4482)+~P3(x4481,x4483,x4482)+P10(x4481,x4482,f26(x4482,x4483,x4481,x4484)) % 62.08/62.13 [240]~E(x2401,x2403)+~E(x2401,x2402)+~P1(x2403)+~P1(x2402)+~P1(x2401)+~P7(x2401,a1)+E(f9(x2401,x2402,x2403),x2403)+P3(f9(x2401,x2402,x2403),x2403,a2)+P1(f14(x2401,x2402,x2403)) % 62.08/62.13 [241]~E(x2411,x2413)+~E(x2411,x2412)+~P1(x2413)+~P1(x2412)+~P1(x2411)+~P7(x2411,a1)+E(f9(x2411,x2412,x2413),x2412)+P3(f9(x2411,x2412,x2413),x2412,a2)+P1(f15(x2411,x2412,x2413)) % 62.08/62.13 [254]~E(x2541,x2543)+~E(x2541,x2542)+~P1(x2543)+~P1(x2542)+~P1(x2541)+~P7(x2541,a1)+E(f9(x2541,x2542,x2543),x2543)+P3(f14(x2541,x2542,x2543),x2543,a2)+P3(f9(x2541,x2542,x2543),x2543,a2) % 62.08/62.13 [255]~E(x2551,x2553)+~E(x2551,x2552)+~P1(x2553)+~P1(x2552)+~P1(x2551)+~P7(x2551,a1)+E(f9(x2551,x2552,x2553),x2552)+P3(f15(x2551,x2552,x2553),x2552,a2)+P3(f9(x2551,x2552,x2553),x2552,a2) % 62.08/62.13 [278]~E(x2781,x2783)+~P1(x2783)+~P1(x2782)+~P1(x2781)+~P3(x2782,x2781,a2)+~P7(x2781,a1)+E(f9(x2781,x2782,x2783),x2783)+P3(f9(x2781,x2782,x2783),x2783,a2)+P1(f14(x2781,x2782,x2783)) % 62.08/62.13 [279]~E(x2791,x2792)+~P1(x2793)+~P1(x2792)+~P1(x2791)+~P3(x2793,x2791,a2)+~P7(x2791,a1)+E(f9(x2791,x2792,x2793),x2793)+P3(f9(x2791,x2792,x2793),x2793,a2)+P1(f14(x2791,x2792,x2793)) % 62.08/62.13 [280]~E(x2801,x2803)+~P1(x2803)+~P1(x2802)+~P1(x2801)+~P3(x2802,x2801,a2)+~P7(x2801,a1)+E(f9(x2801,x2802,x2803),x2802)+P3(f9(x2801,x2802,x2803),x2802,a2)+P1(f15(x2801,x2802,x2803)) % 62.08/62.13 [281]~E(x2811,x2812)+~P1(x2813)+~P1(x2812)+~P1(x2811)+~P3(x2813,x2811,a2)+~P7(x2811,a1)+E(f9(x2811,x2812,x2813),x2812)+P3(f9(x2811,x2812,x2813),x2812,a2)+P1(f15(x2811,x2812,x2813)) % 62.08/62.13 [282]~E(x2821,x2823)+~P1(x2823)+~P1(x2822)+~P1(x2821)+~P9(x2821,a2,x2822)+~P7(x2821,a1)+E(f9(x2821,x2822,x2823),x2823)+P3(f9(x2821,x2822,x2823),x2823,a2)+P1(f14(x2821,x2822,x2823)) % 62.08/62.13 [283]~E(x2831,x2833)+~P1(x2833)+~P1(x2832)+~P1(x2831)+~P10(x2831,a2,x2832)+~P7(x2831,a1)+E(f9(x2831,x2832,x2833),x2833)+P3(f9(x2831,x2832,x2833),x2833,a2)+P1(f14(x2831,x2832,x2833)) % 62.08/62.13 [284]~E(x2841,x2842)+~P1(x2843)+~P1(x2842)+~P1(x2841)+~P9(x2841,a2,x2843)+~P7(x2841,a1)+E(f9(x2841,x2842,x2843),x2843)+P3(f9(x2841,x2842,x2843),x2843,a2)+P1(f14(x2841,x2842,x2843)) % 62.08/62.13 [285]~E(x2851,x2852)+~P1(x2853)+~P1(x2852)+~P1(x2851)+~P10(x2851,a2,x2853)+~P7(x2851,a1)+E(f9(x2851,x2852,x2853),x2853)+P3(f9(x2851,x2852,x2853),x2853,a2)+P1(f14(x2851,x2852,x2853)) % 62.08/62.13 [286]~E(x2861,x2863)+~P1(x2863)+~P1(x2862)+~P1(x2861)+~P9(x2861,a2,x2862)+~P7(x2861,a1)+E(f9(x2861,x2862,x2863),x2862)+P3(f9(x2861,x2862,x2863),x2862,a2)+P1(f15(x2861,x2862,x2863)) % 62.08/62.13 [287]~E(x2871,x2873)+~P1(x2873)+~P1(x2872)+~P1(x2871)+~P10(x2871,a2,x2872)+~P7(x2871,a1)+E(f9(x2871,x2872,x2873),x2872)+P3(f9(x2871,x2872,x2873),x2872,a2)+P1(f15(x2871,x2872,x2873)) % 62.08/62.13 [288]~E(x2881,x2882)+~P1(x2883)+~P1(x2882)+~P1(x2881)+~P9(x2881,a2,x2883)+~P7(x2881,a1)+E(f9(x2881,x2882,x2883),x2882)+P3(f9(x2881,x2882,x2883),x2882,a2)+P1(f15(x2881,x2882,x2883)) % 62.08/62.13 [289]~E(x2891,x2892)+~P1(x2893)+~P1(x2892)+~P1(x2891)+~P10(x2891,a2,x2893)+~P7(x2891,a1)+E(f9(x2891,x2892,x2893),x2892)+P3(f9(x2891,x2892,x2893),x2892,a2)+P1(f15(x2891,x2892,x2893)) % 62.08/62.13 [303]~E(x3031,x3033)+~P1(x3033)+~P1(x3032)+~P1(x3031)+~P3(x3032,x3031,a2)+~P7(x3031,a1)+E(f9(x3031,x3032,x3033),x3033)+P3(f14(x3031,x3032,x3033),x3033,a2)+P3(f9(x3031,x3032,x3033),x3033,a2) % 62.08/62.13 [304]~E(x3041,x3042)+~P1(x3043)+~P1(x3042)+~P1(x3041)+~P3(x3043,x3041,a2)+~P7(x3041,a1)+E(f9(x3041,x3042,x3043),x3043)+P3(f14(x3041,x3042,x3043),x3043,a2)+P3(f9(x3041,x3042,x3043),x3043,a2) % 62.08/62.13 [305]~E(x3051,x3053)+~P1(x3053)+~P1(x3052)+~P1(x3051)+~P3(x3052,x3051,a2)+~P7(x3051,a1)+E(f9(x3051,x3052,x3053),x3052)+P3(f15(x3051,x3052,x3053),x3052,a2)+P3(f9(x3051,x3052,x3053),x3052,a2) % 62.08/62.13 [306]~E(x3061,x3062)+~P1(x3063)+~P1(x3062)+~P1(x3061)+~P3(x3063,x3061,a2)+~P7(x3061,a1)+E(f9(x3061,x3062,x3063),x3062)+P3(f15(x3061,x3062,x3063),x3062,a2)+P3(f9(x3061,x3062,x3063),x3062,a2) % 62.08/62.13 [307]~E(x3071,x3073)+~P1(x3073)+~P1(x3072)+~P1(x3071)+~P9(x3071,a2,x3072)+~P7(x3071,a1)+E(f9(x3071,x3072,x3073),x3073)+P3(f14(x3071,x3072,x3073),x3073,a2)+P3(f9(x3071,x3072,x3073),x3073,a2) % 62.08/62.13 [308]~E(x3081,x3083)+~P1(x3083)+~P1(x3082)+~P1(x3081)+~P10(x3081,a2,x3082)+~P7(x3081,a1)+E(f9(x3081,x3082,x3083),x3083)+P3(f14(x3081,x3082,x3083),x3083,a2)+P3(f9(x3081,x3082,x3083),x3083,a2) % 62.08/62.13 [309]~E(x3091,x3092)+~P1(x3093)+~P1(x3092)+~P1(x3091)+~P9(x3091,a2,x3093)+~P7(x3091,a1)+E(f9(x3091,x3092,x3093),x3093)+P3(f14(x3091,x3092,x3093),x3093,a2)+P3(f9(x3091,x3092,x3093),x3093,a2) % 62.08/62.13 [310]~E(x3101,x3102)+~P1(x3103)+~P1(x3102)+~P1(x3101)+~P10(x3101,a2,x3103)+~P7(x3101,a1)+E(f9(x3101,x3102,x3103),x3103)+P3(f14(x3101,x3102,x3103),x3103,a2)+P3(f9(x3101,x3102,x3103),x3103,a2) % 62.08/62.13 [311]~E(x3111,x3113)+~P1(x3113)+~P1(x3112)+~P1(x3111)+~P9(x3111,a2,x3112)+~P7(x3111,a1)+E(f9(x3111,x3112,x3113),x3112)+P3(f15(x3111,x3112,x3113),x3112,a2)+P3(f9(x3111,x3112,x3113),x3112,a2) % 62.08/62.13 [312]~E(x3121,x3123)+~P1(x3123)+~P1(x3122)+~P1(x3121)+~P10(x3121,a2,x3122)+~P7(x3121,a1)+E(f9(x3121,x3122,x3123),x3122)+P3(f15(x3121,x3122,x3123),x3122,a2)+P3(f9(x3121,x3122,x3123),x3122,a2) % 62.08/62.13 [313]~E(x3131,x3132)+~P1(x3133)+~P1(x3132)+~P1(x3131)+~P9(x3131,a2,x3133)+~P7(x3131,a1)+E(f9(x3131,x3132,x3133),x3132)+P3(f15(x3131,x3132,x3133),x3132,a2)+P3(f9(x3131,x3132,x3133),x3132,a2) % 62.08/62.13 [314]~E(x3141,x3142)+~P1(x3143)+~P1(x3142)+~P1(x3141)+~P10(x3141,a2,x3143)+~P7(x3141,a1)+E(f9(x3141,x3142,x3143),x3142)+P3(f15(x3141,x3142,x3143),x3142,a2)+P3(f9(x3141,x3142,x3143),x3142,a2) % 62.08/62.13 [329]~E(x3291,x3293)+~E(x3291,x3292)+~P1(x3293)+~P1(x3292)+~P1(x3291)+~P7(x3291,a1)+E(f9(x3291,x3292,x3293),x3293)+P9(f14(x3291,x3292,x3293),a2,f9(x3291,x3292,x3293))+P3(f9(x3291,x3292,x3293),x3293,a2) % 62.08/62.13 [330]~E(x3301,x3303)+~E(x3301,x3302)+~P1(x3303)+~P1(x3302)+~P1(x3301)+~P7(x3301,a1)+E(f9(x3301,x3302,x3303),x3302)+P9(f15(x3301,x3302,x3303),a2,f9(x3301,x3302,x3303))+P3(f9(x3301,x3302,x3303),x3302,a2) % 62.08/62.13 [331]~P1(x3313)+~P1(x3312)+~P1(x3311)+~P3(x3313,x3311,a2)+~P3(x3312,x3311,a2)+~P7(x3311,a1)+E(f9(x3311,x3312,x3313),x3313)+P3(f9(x3311,x3312,x3313),x3313,a2)+P1(f14(x3311,x3312,x3313)) % 62.08/62.13 [332]~P1(x3323)+~P1(x3322)+~P1(x3321)+~P3(x3323,x3321,a2)+~P3(x3322,x3321,a2)+~P7(x3321,a1)+E(f9(x3321,x3322,x3323),x3322)+P3(f9(x3321,x3322,x3323),x3322,a2)+P1(f15(x3321,x3322,x3323)) % 62.08/62.13 [333]~P1(x3333)+~P1(x3332)+~P1(x3331)+~P3(x3333,x3331,a2)+~P9(x3331,a2,x3332)+~P7(x3331,a1)+E(f9(x3331,x3332,x3333),x3333)+P3(f9(x3331,x3332,x3333),x3333,a2)+P1(f14(x3331,x3332,x3333)) % 62.08/62.13 [334]~P1(x3343)+~P1(x3342)+~P1(x3341)+~P3(x3343,x3341,a2)+~P10(x3341,a2,x3342)+~P7(x3341,a1)+E(f9(x3341,x3342,x3343),x3343)+P3(f9(x3341,x3342,x3343),x3343,a2)+P1(f14(x3341,x3342,x3343)) % 62.08/62.13 [335]~P1(x3353)+~P1(x3352)+~P1(x3351)+~P3(x3352,x3351,a2)+~P9(x3351,a2,x3353)+~P7(x3351,a1)+E(f9(x3351,x3352,x3353),x3353)+P3(f9(x3351,x3352,x3353),x3353,a2)+P1(f14(x3351,x3352,x3353)) % 62.08/62.13 [336]~P1(x3363)+~P1(x3362)+~P1(x3361)+~P3(x3362,x3361,a2)+~P10(x3361,a2,x3363)+~P7(x3361,a1)+E(f9(x3361,x3362,x3363),x3363)+P3(f9(x3361,x3362,x3363),x3363,a2)+P1(f14(x3361,x3362,x3363)) % 62.08/62.13 [337]~P1(x3373)+~P1(x3372)+~P1(x3371)+~P3(x3373,x3371,a2)+~P9(x3371,a2,x3372)+~P7(x3371,a1)+E(f9(x3371,x3372,x3373),x3372)+P3(f9(x3371,x3372,x3373),x3372,a2)+P1(f15(x3371,x3372,x3373)) % 62.08/62.13 [338]~P1(x3383)+~P1(x3382)+~P1(x3381)+~P3(x3383,x3381,a2)+~P10(x3381,a2,x3382)+~P7(x3381,a1)+E(f9(x3381,x3382,x3383),x3382)+P3(f9(x3381,x3382,x3383),x3382,a2)+P1(f15(x3381,x3382,x3383)) % 62.08/62.13 [339]~P1(x3393)+~P1(x3392)+~P1(x3391)+~P3(x3392,x3391,a2)+~P9(x3391,a2,x3393)+~P7(x3391,a1)+E(f9(x3391,x3392,x3393),x3392)+P3(f9(x3391,x3392,x3393),x3392,a2)+P1(f15(x3391,x3392,x3393)) % 62.08/62.13 [340]~P1(x3403)+~P1(x3402)+~P1(x3401)+~P3(x3402,x3401,a2)+~P10(x3401,a2,x3403)+~P7(x3401,a1)+E(f9(x3401,x3402,x3403),x3402)+P3(f9(x3401,x3402,x3403),x3402,a2)+P1(f15(x3401,x3402,x3403)) % 62.08/62.13 [341]~P1(x3413)+~P1(x3412)+~P1(x3411)+~P9(x3411,a2,x3413)+~P9(x3411,a2,x3412)+~P7(x3411,a1)+E(f9(x3411,x3412,x3413),x3413)+P3(f9(x3411,x3412,x3413),x3413,a2)+P1(f14(x3411,x3412,x3413)) % 62.08/62.13 [342]~P1(x3423)+~P1(x3422)+~P1(x3421)+~P9(x3421,a2,x3423)+~P10(x3421,a2,x3422)+~P7(x3421,a1)+E(f9(x3421,x3422,x3423),x3423)+P3(f9(x3421,x3422,x3423),x3423,a2)+P1(f14(x3421,x3422,x3423)) % 62.08/62.13 [343]~P1(x3433)+~P1(x3432)+~P1(x3431)+~P9(x3431,a2,x3432)+~P10(x3431,a2,x3433)+~P7(x3431,a1)+E(f9(x3431,x3432,x3433),x3433)+P3(f9(x3431,x3432,x3433),x3433,a2)+P1(f14(x3431,x3432,x3433)) % 62.08/62.13 [344]~P1(x3443)+~P1(x3442)+~P1(x3441)+~P10(x3441,a2,x3443)+~P10(x3441,a2,x3442)+~P7(x3441,a1)+E(f9(x3441,x3442,x3443),x3443)+P3(f9(x3441,x3442,x3443),x3443,a2)+P1(f14(x3441,x3442,x3443)) % 62.08/62.13 [345]~P1(x3453)+~P1(x3452)+~P1(x3451)+~P9(x3451,a2,x3453)+~P9(x3451,a2,x3452)+~P7(x3451,a1)+E(f9(x3451,x3452,x3453),x3452)+P3(f9(x3451,x3452,x3453),x3452,a2)+P1(f15(x3451,x3452,x3453)) % 62.08/62.13 [346]~P1(x3463)+~P1(x3462)+~P1(x3461)+~P9(x3461,a2,x3463)+~P10(x3461,a2,x3462)+~P7(x3461,a1)+E(f9(x3461,x3462,x3463),x3462)+P3(f9(x3461,x3462,x3463),x3462,a2)+P1(f15(x3461,x3462,x3463)) % 62.08/62.13 [347]~P1(x3473)+~P1(x3472)+~P1(x3471)+~P9(x3471,a2,x3472)+~P10(x3471,a2,x3473)+~P7(x3471,a1)+E(f9(x3471,x3472,x3473),x3472)+P3(f9(x3471,x3472,x3473),x3472,a2)+P1(f15(x3471,x3472,x3473)) % 62.08/62.13 [348]~P1(x3483)+~P1(x3482)+~P1(x3481)+~P10(x3481,a2,x3483)+~P10(x3481,a2,x3482)+~P7(x3481,a1)+E(f9(x3481,x3482,x3483),x3482)+P3(f9(x3481,x3482,x3483),x3482,a2)+P1(f15(x3481,x3482,x3483)) % 62.08/62.13 [357]~P1(x3573)+~P1(x3572)+~P1(x3571)+~P3(x3573,x3571,a2)+~P3(x3572,x3571,a2)+~P7(x3571,a1)+E(f9(x3571,x3572,x3573),x3573)+P3(f14(x3571,x3572,x3573),x3573,a2)+P3(f9(x3571,x3572,x3573),x3573,a2) % 62.08/62.13 [358]~P1(x3583)+~P1(x3582)+~P1(x3581)+~P3(x3583,x3581,a2)+~P3(x3582,x3581,a2)+~P7(x3581,a1)+E(f9(x3581,x3582,x3583),x3582)+P3(f15(x3581,x3582,x3583),x3582,a2)+P3(f9(x3581,x3582,x3583),x3582,a2) % 62.08/62.13 [359]~P1(x3593)+~P1(x3592)+~P1(x3591)+~P3(x3593,x3591,a2)+~P9(x3591,a2,x3592)+~P7(x3591,a1)+E(f9(x3591,x3592,x3593),x3593)+P3(f14(x3591,x3592,x3593),x3593,a2)+P3(f9(x3591,x3592,x3593),x3593,a2) % 62.08/62.13 [360]~P1(x3603)+~P1(x3602)+~P1(x3601)+~P3(x3603,x3601,a2)+~P10(x3601,a2,x3602)+~P7(x3601,a1)+E(f9(x3601,x3602,x3603),x3603)+P3(f14(x3601,x3602,x3603),x3603,a2)+P3(f9(x3601,x3602,x3603),x3603,a2) % 62.08/62.13 [361]~P1(x3613)+~P1(x3612)+~P1(x3611)+~P3(x3612,x3611,a2)+~P9(x3611,a2,x3613)+~P7(x3611,a1)+E(f9(x3611,x3612,x3613),x3613)+P3(f14(x3611,x3612,x3613),x3613,a2)+P3(f9(x3611,x3612,x3613),x3613,a2) % 62.08/62.13 [362]~P1(x3623)+~P1(x3622)+~P1(x3621)+~P3(x3622,x3621,a2)+~P10(x3621,a2,x3623)+~P7(x3621,a1)+E(f9(x3621,x3622,x3623),x3623)+P3(f14(x3621,x3622,x3623),x3623,a2)+P3(f9(x3621,x3622,x3623),x3623,a2) % 62.08/62.13 [363]~P1(x3633)+~P1(x3632)+~P1(x3631)+~P3(x3633,x3631,a2)+~P9(x3631,a2,x3632)+~P7(x3631,a1)+E(f9(x3631,x3632,x3633),x3632)+P3(f15(x3631,x3632,x3633),x3632,a2)+P3(f9(x3631,x3632,x3633),x3632,a2) % 62.08/62.13 [364]~P1(x3643)+~P1(x3642)+~P1(x3641)+~P3(x3643,x3641,a2)+~P10(x3641,a2,x3642)+~P7(x3641,a1)+E(f9(x3641,x3642,x3643),x3642)+P3(f15(x3641,x3642,x3643),x3642,a2)+P3(f9(x3641,x3642,x3643),x3642,a2) % 62.08/62.13 [365]~P1(x3653)+~P1(x3652)+~P1(x3651)+~P3(x3652,x3651,a2)+~P9(x3651,a2,x3653)+~P7(x3651,a1)+E(f9(x3651,x3652,x3653),x3652)+P3(f15(x3651,x3652,x3653),x3652,a2)+P3(f9(x3651,x3652,x3653),x3652,a2) % 62.08/62.13 [366]~P1(x3663)+~P1(x3662)+~P1(x3661)+~P3(x3662,x3661,a2)+~P10(x3661,a2,x3663)+~P7(x3661,a1)+E(f9(x3661,x3662,x3663),x3662)+P3(f15(x3661,x3662,x3663),x3662,a2)+P3(f9(x3661,x3662,x3663),x3662,a2) % 62.08/62.13 [367]~P1(x3673)+~P1(x3672)+~P1(x3671)+~P9(x3671,a2,x3673)+~P9(x3671,a2,x3672)+~P7(x3671,a1)+E(f9(x3671,x3672,x3673),x3673)+P3(f14(x3671,x3672,x3673),x3673,a2)+P3(f9(x3671,x3672,x3673),x3673,a2) % 62.08/62.13 [368]~P1(x3683)+~P1(x3682)+~P1(x3681)+~P9(x3681,a2,x3683)+~P10(x3681,a2,x3682)+~P7(x3681,a1)+E(f9(x3681,x3682,x3683),x3683)+P3(f14(x3681,x3682,x3683),x3683,a2)+P3(f9(x3681,x3682,x3683),x3683,a2) % 62.08/62.13 [369]~P1(x3693)+~P1(x3692)+~P1(x3691)+~P9(x3691,a2,x3692)+~P10(x3691,a2,x3693)+~P7(x3691,a1)+E(f9(x3691,x3692,x3693),x3693)+P3(f14(x3691,x3692,x3693),x3693,a2)+P3(f9(x3691,x3692,x3693),x3693,a2) % 62.08/62.13 [370]~P1(x3703)+~P1(x3702)+~P1(x3701)+~P10(x3701,a2,x3703)+~P10(x3701,a2,x3702)+~P7(x3701,a1)+E(f9(x3701,x3702,x3703),x3703)+P3(f14(x3701,x3702,x3703),x3703,a2)+P3(f9(x3701,x3702,x3703),x3703,a2) % 62.08/62.13 [371]~P1(x3713)+~P1(x3712)+~P1(x3711)+~P9(x3711,a2,x3713)+~P9(x3711,a2,x3712)+~P7(x3711,a1)+E(f9(x3711,x3712,x3713),x3712)+P3(f15(x3711,x3712,x3713),x3712,a2)+P3(f9(x3711,x3712,x3713),x3712,a2) % 62.08/62.13 [372]~P1(x3723)+~P1(x3722)+~P1(x3721)+~P9(x3721,a2,x3723)+~P10(x3721,a2,x3722)+~P7(x3721,a1)+E(f9(x3721,x3722,x3723),x3722)+P3(f15(x3721,x3722,x3723),x3722,a2)+P3(f9(x3721,x3722,x3723),x3722,a2) % 62.08/62.13 [373]~P1(x3733)+~P1(x3732)+~P1(x3731)+~P9(x3731,a2,x3732)+~P10(x3731,a2,x3733)+~P7(x3731,a1)+E(f9(x3731,x3732,x3733),x3732)+P3(f15(x3731,x3732,x3733),x3732,a2)+P3(f9(x3731,x3732,x3733),x3732,a2) % 62.08/62.13 [374]~P1(x3743)+~P1(x3742)+~P1(x3741)+~P10(x3741,a2,x3743)+~P10(x3741,a2,x3742)+~P7(x3741,a1)+E(f9(x3741,x3742,x3743),x3742)+P3(f15(x3741,x3742,x3743),x3742,a2)+P3(f9(x3741,x3742,x3743),x3742,a2) % 62.08/62.13 [381]~E(x3811,x3813)+~P1(x3813)+~P1(x3812)+~P1(x3811)+~P3(x3812,x3811,a2)+~P7(x3811,a1)+E(f9(x3811,x3812,x3813),x3813)+P9(f14(x3811,x3812,x3813),a2,f9(x3811,x3812,x3813))+P3(f9(x3811,x3812,x3813),x3813,a2) % 62.08/62.13 [382]~E(x3821,x3822)+~P1(x3823)+~P1(x3822)+~P1(x3821)+~P3(x3823,x3821,a2)+~P7(x3821,a1)+E(f9(x3821,x3822,x3823),x3823)+P9(f14(x3821,x3822,x3823),a2,f9(x3821,x3822,x3823))+P3(f9(x3821,x3822,x3823),x3823,a2) % 62.08/62.13 [383]~E(x3831,x3833)+~P1(x3833)+~P1(x3832)+~P1(x3831)+~P3(x3832,x3831,a2)+~P7(x3831,a1)+E(f9(x3831,x3832,x3833),x3832)+P9(f15(x3831,x3832,x3833),a2,f9(x3831,x3832,x3833))+P3(f9(x3831,x3832,x3833),x3832,a2) % 62.08/62.13 [384]~E(x3841,x3842)+~P1(x3843)+~P1(x3842)+~P1(x3841)+~P3(x3843,x3841,a2)+~P7(x3841,a1)+E(f9(x3841,x3842,x3843),x3842)+P9(f15(x3841,x3842,x3843),a2,f9(x3841,x3842,x3843))+P3(f9(x3841,x3842,x3843),x3842,a2) % 62.08/62.13 [385]~E(x3851,x3853)+~P1(x3853)+~P1(x3852)+~P1(x3851)+~P9(x3851,a2,x3852)+~P7(x3851,a1)+E(f9(x3851,x3852,x3853),x3853)+P9(f14(x3851,x3852,x3853),a2,f9(x3851,x3852,x3853))+P3(f9(x3851,x3852,x3853),x3853,a2) % 62.08/62.13 [386]~E(x3861,x3863)+~P1(x3863)+~P1(x3862)+~P1(x3861)+~P10(x3861,a2,x3862)+~P7(x3861,a1)+E(f9(x3861,x3862,x3863),x3863)+P9(f14(x3861,x3862,x3863),a2,f9(x3861,x3862,x3863))+P3(f9(x3861,x3862,x3863),x3863,a2) % 62.08/62.13 [387]~E(x3871,x3872)+~P1(x3873)+~P1(x3872)+~P1(x3871)+~P9(x3871,a2,x3873)+~P7(x3871,a1)+E(f9(x3871,x3872,x3873),x3873)+P9(f14(x3871,x3872,x3873),a2,f9(x3871,x3872,x3873))+P3(f9(x3871,x3872,x3873),x3873,a2) % 62.08/62.13 [388]~E(x3881,x3882)+~P1(x3883)+~P1(x3882)+~P1(x3881)+~P10(x3881,a2,x3883)+~P7(x3881,a1)+E(f9(x3881,x3882,x3883),x3883)+P9(f14(x3881,x3882,x3883),a2,f9(x3881,x3882,x3883))+P3(f9(x3881,x3882,x3883),x3883,a2) % 62.08/62.13 [389]~E(x3891,x3893)+~P1(x3893)+~P1(x3892)+~P1(x3891)+~P9(x3891,a2,x3892)+~P7(x3891,a1)+E(f9(x3891,x3892,x3893),x3892)+P9(f15(x3891,x3892,x3893),a2,f9(x3891,x3892,x3893))+P3(f9(x3891,x3892,x3893),x3892,a2) % 62.08/62.13 [390]~E(x3901,x3903)+~P1(x3903)+~P1(x3902)+~P1(x3901)+~P10(x3901,a2,x3902)+~P7(x3901,a1)+E(f9(x3901,x3902,x3903),x3902)+P9(f15(x3901,x3902,x3903),a2,f9(x3901,x3902,x3903))+P3(f9(x3901,x3902,x3903),x3902,a2) % 62.08/62.13 [391]~E(x3911,x3912)+~P1(x3913)+~P1(x3912)+~P1(x3911)+~P9(x3911,a2,x3913)+~P7(x3911,a1)+E(f9(x3911,x3912,x3913),x3912)+P9(f15(x3911,x3912,x3913),a2,f9(x3911,x3912,x3913))+P3(f9(x3911,x3912,x3913),x3912,a2) % 62.08/62.13 [392]~E(x3921,x3922)+~P1(x3923)+~P1(x3922)+~P1(x3921)+~P10(x3921,a2,x3923)+~P7(x3921,a1)+E(f9(x3921,x3922,x3923),x3922)+P9(f15(x3921,x3922,x3923),a2,f9(x3921,x3922,x3923))+P3(f9(x3921,x3922,x3923),x3922,a2) % 62.08/62.13 [419]~P1(x4193)+~P1(x4192)+~P1(x4191)+~P3(x4193,x4191,a2)+~P3(x4192,x4191,a2)+~P7(x4191,a1)+E(f9(x4191,x4192,x4193),x4193)+P9(f14(x4191,x4192,x4193),a2,f9(x4191,x4192,x4193))+P3(f9(x4191,x4192,x4193),x4193,a2) % 62.08/62.13 [420]~P1(x4203)+~P1(x4202)+~P1(x4201)+~P3(x4203,x4201,a2)+~P3(x4202,x4201,a2)+~P7(x4201,a1)+E(f9(x4201,x4202,x4203),x4202)+P9(f15(x4201,x4202,x4203),a2,f9(x4201,x4202,x4203))+P3(f9(x4201,x4202,x4203),x4202,a2) % 62.08/62.13 [421]~P1(x4213)+~P1(x4212)+~P1(x4211)+~P3(x4213,x4211,a2)+~P9(x4211,a2,x4212)+~P7(x4211,a1)+E(f9(x4211,x4212,x4213),x4213)+P9(f14(x4211,x4212,x4213),a2,f9(x4211,x4212,x4213))+P3(f9(x4211,x4212,x4213),x4213,a2) % 62.08/62.13 [422]~P1(x4223)+~P1(x4222)+~P1(x4221)+~P3(x4223,x4221,a2)+~P10(x4221,a2,x4222)+~P7(x4221,a1)+E(f9(x4221,x4222,x4223),x4223)+P9(f14(x4221,x4222,x4223),a2,f9(x4221,x4222,x4223))+P3(f9(x4221,x4222,x4223),x4223,a2) % 62.08/62.13 [423]~P1(x4233)+~P1(x4232)+~P1(x4231)+~P3(x4232,x4231,a2)+~P9(x4231,a2,x4233)+~P7(x4231,a1)+E(f9(x4231,x4232,x4233),x4233)+P9(f14(x4231,x4232,x4233),a2,f9(x4231,x4232,x4233))+P3(f9(x4231,x4232,x4233),x4233,a2) % 62.08/62.13 [424]~P1(x4243)+~P1(x4242)+~P1(x4241)+~P3(x4242,x4241,a2)+~P10(x4241,a2,x4243)+~P7(x4241,a1)+E(f9(x4241,x4242,x4243),x4243)+P9(f14(x4241,x4242,x4243),a2,f9(x4241,x4242,x4243))+P3(f9(x4241,x4242,x4243),x4243,a2) % 62.08/62.13 [425]~P1(x4253)+~P1(x4252)+~P1(x4251)+~P3(x4253,x4251,a2)+~P9(x4251,a2,x4252)+~P7(x4251,a1)+E(f9(x4251,x4252,x4253),x4252)+P9(f15(x4251,x4252,x4253),a2,f9(x4251,x4252,x4253))+P3(f9(x4251,x4252,x4253),x4252,a2) % 62.08/62.13 [426]~P1(x4263)+~P1(x4262)+~P1(x4261)+~P3(x4263,x4261,a2)+~P10(x4261,a2,x4262)+~P7(x4261,a1)+E(f9(x4261,x4262,x4263),x4262)+P9(f15(x4261,x4262,x4263),a2,f9(x4261,x4262,x4263))+P3(f9(x4261,x4262,x4263),x4262,a2) % 62.08/62.13 [427]~P1(x4273)+~P1(x4272)+~P1(x4271)+~P3(x4272,x4271,a2)+~P9(x4271,a2,x4273)+~P7(x4271,a1)+E(f9(x4271,x4272,x4273),x4272)+P9(f15(x4271,x4272,x4273),a2,f9(x4271,x4272,x4273))+P3(f9(x4271,x4272,x4273),x4272,a2) % 62.08/62.13 [428]~P1(x4283)+~P1(x4282)+~P1(x4281)+~P3(x4282,x4281,a2)+~P10(x4281,a2,x4283)+~P7(x4281,a1)+E(f9(x4281,x4282,x4283),x4282)+P9(f15(x4281,x4282,x4283),a2,f9(x4281,x4282,x4283))+P3(f9(x4281,x4282,x4283),x4282,a2) % 62.08/62.13 [429]~P1(x4293)+~P1(x4292)+~P1(x4291)+~P9(x4291,a2,x4293)+~P9(x4291,a2,x4292)+~P7(x4291,a1)+E(f9(x4291,x4292,x4293),x4293)+P9(f14(x4291,x4292,x4293),a2,f9(x4291,x4292,x4293))+P3(f9(x4291,x4292,x4293),x4293,a2) % 62.08/62.13 [430]~P1(x4303)+~P1(x4302)+~P1(x4301)+~P9(x4301,a2,x4303)+~P10(x4301,a2,x4302)+~P7(x4301,a1)+E(f9(x4301,x4302,x4303),x4303)+P9(f14(x4301,x4302,x4303),a2,f9(x4301,x4302,x4303))+P3(f9(x4301,x4302,x4303),x4303,a2) % 62.08/62.13 [431]~P1(x4313)+~P1(x4312)+~P1(x4311)+~P9(x4311,a2,x4312)+~P10(x4311,a2,x4313)+~P7(x4311,a1)+E(f9(x4311,x4312,x4313),x4313)+P9(f14(x4311,x4312,x4313),a2,f9(x4311,x4312,x4313))+P3(f9(x4311,x4312,x4313),x4313,a2) % 62.08/62.13 [432]~P1(x4323)+~P1(x4322)+~P1(x4321)+~P10(x4321,a2,x4323)+~P10(x4321,a2,x4322)+~P7(x4321,a1)+E(f9(x4321,x4322,x4323),x4323)+P9(f14(x4321,x4322,x4323),a2,f9(x4321,x4322,x4323))+P3(f9(x4321,x4322,x4323),x4323,a2) % 62.08/62.13 [433]~P1(x4333)+~P1(x4332)+~P1(x4331)+~P9(x4331,a2,x4333)+~P9(x4331,a2,x4332)+~P7(x4331,a1)+E(f9(x4331,x4332,x4333),x4332)+P9(f15(x4331,x4332,x4333),a2,f9(x4331,x4332,x4333))+P3(f9(x4331,x4332,x4333),x4332,a2) % 62.08/62.13 [434]~P1(x4343)+~P1(x4342)+~P1(x4341)+~P9(x4341,a2,x4343)+~P10(x4341,a2,x4342)+~P7(x4341,a1)+E(f9(x4341,x4342,x4343),x4342)+P9(f15(x4341,x4342,x4343),a2,f9(x4341,x4342,x4343))+P3(f9(x4341,x4342,x4343),x4342,a2) % 62.08/62.13 [435]~P1(x4353)+~P1(x4352)+~P1(x4351)+~P9(x4351,a2,x4352)+~P10(x4351,a2,x4353)+~P7(x4351,a1)+E(f9(x4351,x4352,x4353),x4352)+P9(f15(x4351,x4352,x4353),a2,f9(x4351,x4352,x4353))+P3(f9(x4351,x4352,x4353),x4352,a2) % 62.08/62.13 [436]~P1(x4363)+~P1(x4362)+~P1(x4361)+~P10(x4361,a2,x4363)+~P10(x4361,a2,x4362)+~P7(x4361,a1)+E(f9(x4361,x4362,x4363),x4362)+P9(f15(x4361,x4362,x4363),a2,f9(x4361,x4362,x4363))+P3(f9(x4361,x4362,x4363),x4362,a2) % 62.08/62.13 [205]~E(x2051,x2053)+~P1(x2053)+~P1(x2052)+~P1(x2051)+~P1(x2054)+~P3(x2054,x2051,a2)+~P9(x2054,a2,x2052)+~P7(x2051,a1)+P1(f9(x2051,x2052,x2053)) % 62.08/62.13 [206]~E(x2061,x2062)+~P1(x2063)+~P1(x2062)+~P1(x2061)+~P1(x2064)+~P3(x2064,x2061,a2)+~P9(x2064,a2,x2063)+~P7(x2061,a1)+P1(f9(x2061,x2062,x2063)) % 62.08/62.13 [242]~E(x2422,x2423)+~P1(x2423)+~P1(x2422)+~P1(x2421)+~P1(x2424)+~P3(x2424,x2422,a2)+~P9(x2424,a2,x2421)+~P7(x2422,a1)+P10(x2421,a2,f9(x2422,x2423,x2421)) % 62.08/62.13 [243]~E(x2431,x2432)+~P1(x2433)+~P1(x2432)+~P1(x2431)+~P1(x2434)+~P3(x2434,x2432,a2)+~P9(x2434,a2,x2433)+~P7(x2432,a1)+P10(x2431,a2,f9(x2432,x2433,x2431)) % 62.08/62.13 [244]~E(x2442,x2443)+~P1(x2443)+~P1(x2442)+~P1(x2441)+~P1(x2444)+~P3(x2444,x2442,a2)+~P9(x2444,a2,x2441)+~P7(x2442,a1)+P10(x2441,a2,f9(x2442,x2441,x2443)) % 62.08/62.13 [245]~E(x2451,x2452)+~P1(x2453)+~P1(x2452)+~P1(x2451)+~P1(x2454)+~P3(x2454,x2452,a2)+~P9(x2454,a2,x2453)+~P7(x2452,a1)+P10(x2451,a2,f9(x2452,x2451,x2453)) % 62.08/62.13 [248]~P1(x2483)+~P1(x2482)+~P1(x2481)+~P1(x2484)+~P3(x2484,x2481,a2)+~P3(x2483,x2481,a2)+~P9(x2484,a2,x2482)+~P7(x2481,a1)+P1(f9(x2481,x2482,x2483)) % 62.08/62.13 [249]~P1(x2493)+~P1(x2492)+~P1(x2491)+~P1(x2494)+~P3(x2494,x2491,a2)+~P3(x2492,x2491,a2)+~P9(x2494,a2,x2493)+~P7(x2491,a1)+P1(f9(x2491,x2492,x2493)) % 62.08/62.13 [250]~P1(x2503)+~P1(x2502)+~P1(x2501)+~P1(x2504)+~P3(x2504,x2501,a2)+~P9(x2504,a2,x2503)+~P9(x2501,a2,x2502)+~P7(x2501,a1)+P1(f9(x2501,x2502,x2503)) % 62.08/62.13 [251]~P1(x2513)+~P1(x2512)+~P1(x2511)+~P1(x2514)+~P3(x2514,x2511,a2)+~P9(x2514,a2,x2513)+~P10(x2511,a2,x2512)+~P7(x2511,a1)+P1(f9(x2511,x2512,x2513)) % 62.08/62.13 [252]~P1(x2523)+~P1(x2522)+~P1(x2521)+~P1(x2524)+~P3(x2524,x2521,a2)+~P9(x2524,a2,x2522)+~P9(x2521,a2,x2523)+~P7(x2521,a1)+P1(f9(x2521,x2522,x2523)) % 62.08/62.13 [253]~P1(x2533)+~P1(x2532)+~P1(x2531)+~P1(x2534)+~P3(x2534,x2531,a2)+~P9(x2534,a2,x2532)+~P10(x2531,a2,x2533)+~P7(x2531,a1)+P1(f9(x2531,x2532,x2533)) % 62.08/62.13 [290]~P1(x2903)+~P1(x2902)+~P1(x2901)+~P1(x2904)+~P3(x2904,x2902,a2)+~P3(x2903,x2902,a2)+~P9(x2904,a2,x2901)+~P7(x2902,a1)+P10(x2901,a2,f9(x2902,x2903,x2901)) % 62.08/62.13 [291]~P1(x2913)+~P1(x2912)+~P1(x2911)+~P1(x2914)+~P3(x2914,x2912,a2)+~P3(x2911,x2912,a2)+~P9(x2914,a2,x2913)+~P7(x2912,a1)+P10(x2911,a2,f9(x2912,x2913,x2911)) % 62.08/62.13 [292]~P1(x2923)+~P1(x2922)+~P1(x2921)+~P1(x2924)+~P3(x2924,x2922,a2)+~P3(x2923,x2922,a2)+~P9(x2924,a2,x2921)+~P7(x2922,a1)+P10(x2921,a2,f9(x2922,x2921,x2923)) % 62.08/62.13 [293]~P1(x2933)+~P1(x2932)+~P1(x2931)+~P1(x2934)+~P3(x2934,x2932,a2)+~P3(x2931,x2932,a2)+~P9(x2934,a2,x2933)+~P7(x2932,a1)+P10(x2931,a2,f9(x2932,x2931,x2933)) % 62.08/62.13 [294]~P1(x2943)+~P1(x2942)+~P1(x2941)+~P1(x2944)+~P3(x2944,x2942,a2)+~P9(x2944,a2,x2943)+~P9(x2942,a2,x2941)+~P7(x2942,a1)+P10(x2941,a2,f9(x2942,x2943,x2941)) % 62.08/62.13 [295]~P1(x2953)+~P1(x2952)+~P1(x2951)+~P1(x2954)+~P3(x2954,x2952,a2)+~P9(x2954,a2,x2953)+~P10(x2952,a2,x2951)+~P7(x2952,a1)+P10(x2951,a2,f9(x2952,x2953,x2951)) % 62.08/62.13 [296]~P1(x2963)+~P1(x2962)+~P1(x2961)+~P1(x2964)+~P3(x2964,x2962,a2)+~P9(x2964,a2,x2961)+~P9(x2962,a2,x2963)+~P7(x2962,a1)+P10(x2961,a2,f9(x2962,x2963,x2961)) % 62.08/62.13 [297]~P1(x2973)+~P1(x2972)+~P1(x2971)+~P1(x2974)+~P3(x2974,x2972,a2)+~P9(x2974,a2,x2971)+~P10(x2972,a2,x2973)+~P7(x2972,a1)+P10(x2971,a2,f9(x2972,x2973,x2971)) % 62.08/62.13 [298]~P1(x2983)+~P1(x2982)+~P1(x2981)+~P1(x2984)+~P3(x2984,x2982,a2)+~P9(x2984,a2,x2983)+~P9(x2982,a2,x2981)+~P7(x2982,a1)+P10(x2981,a2,f9(x2982,x2981,x2983)) % 62.08/62.13 [299]~P1(x2993)+~P1(x2992)+~P1(x2991)+~P1(x2994)+~P3(x2994,x2992,a2)+~P9(x2994,a2,x2993)+~P10(x2992,a2,x2991)+~P7(x2992,a1)+P10(x2991,a2,f9(x2992,x2991,x2993)) % 62.08/62.13 [300]~P1(x3003)+~P1(x3002)+~P1(x3001)+~P1(x3004)+~P3(x3004,x3002,a2)+~P9(x3004,a2,x3001)+~P9(x3002,a2,x3003)+~P7(x3002,a1)+P10(x3001,a2,f9(x3002,x3001,x3003)) % 62.08/62.13 [301]~P1(x3013)+~P1(x3012)+~P1(x3011)+~P1(x3014)+~P3(x3014,x3012,a2)+~P9(x3014,a2,x3011)+~P10(x3012,a2,x3013)+~P7(x3012,a1)+P10(x3011,a2,f9(x3012,x3011,x3013)) % 62.08/62.13 [274]~E(x2741,x2742)+~P1(x2742)+~P1(x2741)+~P1(x2743)+~P1(x2744)+~P3(x2744,x2741,a2)+~P9(x2744,a2,x2743)+~P7(x2741,a1)+E(f9(x2741,x2742,x2743),x2743)+P9(x2743,a2,f9(x2741,x2742,x2743)) % 62.08/62.13 [275]~E(x2753,x2751)+~P1(x2752)+~P1(x2751)+~P1(x2753)+~P1(x2754)+~P3(x2754,x2751,a2)+~P9(x2754,a2,x2752)+~P7(x2751,a1)+E(f9(x2751,x2752,x2753),x2753)+P9(x2753,a2,f9(x2751,x2752,x2753)) % 62.08/62.13 [276]~E(x2761,x2763)+~P1(x2763)+~P1(x2761)+~P1(x2762)+~P1(x2764)+~P3(x2764,x2761,a2)+~P9(x2764,a2,x2762)+~P7(x2761,a1)+E(f9(x2761,x2762,x2763),x2762)+P9(x2762,a2,f9(x2761,x2762,x2763)) % 62.08/62.13 [277]~E(x2772,x2771)+~P1(x2773)+~P1(x2771)+~P1(x2772)+~P1(x2774)+~P3(x2774,x2771,a2)+~P9(x2774,a2,x2773)+~P7(x2771,a1)+E(f9(x2771,x2772,x2773),x2772)+P9(x2772,a2,f9(x2771,x2772,x2773)) % 62.08/62.13 [317]~P1(x3172)+~P1(x3171)+~P1(x3173)+~P1(x3174)+~P3(x3174,x3171,a2)+~P3(x3172,x3171,a2)+~P9(x3174,a2,x3173)+~P7(x3171,a1)+E(f9(x3171,x3172,x3173),x3173)+P9(x3173,a2,f9(x3171,x3172,x3173)) % 62.08/62.13 [318]~P1(x3182)+~P1(x3181)+~P1(x3183)+~P1(x3184)+~P3(x3184,x3181,a2)+~P3(x3183,x3181,a2)+~P9(x3184,a2,x3182)+~P7(x3181,a1)+E(f9(x3181,x3182,x3183),x3183)+P9(x3183,a2,f9(x3181,x3182,x3183)) % 62.08/62.13 [319]~P1(x3193)+~P1(x3191)+~P1(x3192)+~P1(x3194)+~P3(x3194,x3191,a2)+~P3(x3193,x3191,a2)+~P9(x3194,a2,x3192)+~P7(x3191,a1)+E(f9(x3191,x3192,x3193),x3192)+P9(x3192,a2,f9(x3191,x3192,x3193)) % 62.08/62.13 [320]~P1(x3203)+~P1(x3201)+~P1(x3202)+~P1(x3204)+~P3(x3204,x3201,a2)+~P3(x3202,x3201,a2)+~P9(x3204,a2,x3203)+~P7(x3201,a1)+E(f9(x3201,x3202,x3203),x3202)+P9(x3202,a2,f9(x3201,x3202,x3203)) % 62.08/62.13 [321]~P1(x3212)+~P1(x3211)+~P1(x3213)+~P1(x3214)+~P3(x3214,x3211,a2)+~P9(x3214,a2,x3212)+~P9(x3211,a2,x3213)+~P7(x3211,a1)+E(f9(x3211,x3212,x3213),x3213)+P9(x3213,a2,f9(x3211,x3212,x3213)) % 62.08/62.13 [322]~P1(x3222)+~P1(x3221)+~P1(x3223)+~P1(x3224)+~P3(x3224,x3221,a2)+~P9(x3224,a2,x3222)+~P10(x3221,a2,x3223)+~P7(x3221,a1)+E(f9(x3221,x3222,x3223),x3223)+P9(x3223,a2,f9(x3221,x3222,x3223)) % 62.08/62.13 [323]~P1(x3232)+~P1(x3231)+~P1(x3233)+~P1(x3234)+~P3(x3234,x3231,a2)+~P9(x3234,a2,x3233)+~P9(x3231,a2,x3232)+~P7(x3231,a1)+E(f9(x3231,x3232,x3233),x3233)+P9(x3233,a2,f9(x3231,x3232,x3233)) % 62.08/62.13 [324]~P1(x3242)+~P1(x3241)+~P1(x3243)+~P1(x3244)+~P3(x3244,x3241,a2)+~P9(x3244,a2,x3243)+~P10(x3241,a2,x3242)+~P7(x3241,a1)+E(f9(x3241,x3242,x3243),x3243)+P9(x3243,a2,f9(x3241,x3242,x3243)) % 62.08/62.13 [325]~P1(x3253)+~P1(x3251)+~P1(x3252)+~P1(x3254)+~P3(x3254,x3251,a2)+~P9(x3254,a2,x3253)+~P9(x3251,a2,x3252)+~P7(x3251,a1)+E(f9(x3251,x3252,x3253),x3252)+P9(x3252,a2,f9(x3251,x3252,x3253)) % 62.08/62.13 [326]~P1(x3263)+~P1(x3261)+~P1(x3262)+~P1(x3264)+~P3(x3264,x3261,a2)+~P9(x3264,a2,x3263)+~P10(x3261,a2,x3262)+~P7(x3261,a1)+E(f9(x3261,x3262,x3263),x3262)+P9(x3262,a2,f9(x3261,x3262,x3263)) % 62.08/62.13 [327]~P1(x3273)+~P1(x3271)+~P1(x3272)+~P1(x3274)+~P3(x3274,x3271,a2)+~P9(x3274,a2,x3272)+~P9(x3271,a2,x3273)+~P7(x3271,a1)+E(f9(x3271,x3272,x3273),x3272)+P9(x3272,a2,f9(x3271,x3272,x3273)) % 62.08/62.13 [328]~P1(x3283)+~P1(x3281)+~P1(x3282)+~P1(x3284)+~P3(x3284,x3281,a2)+~P9(x3284,a2,x3282)+~P10(x3281,a2,x3283)+~P7(x3281,a1)+E(f9(x3281,x3282,x3283),x3282)+P9(x3282,a2,f9(x3281,x3282,x3283)) % 62.08/62.13 [349]~E(x3491,x3493)+~P1(x3493)+~P1(x3492)+~P1(x3491)+~P1(x3494)+~P3(x3494,x3491,a2)+~P9(x3494,a2,x3492)+~P7(x3491,a1)+E(f9(x3491,x3492,x3493),x3493)+P3(f9(x3491,x3492,x3493),x3493,a2)+P1(f14(x3491,x3492,x3493)) % 62.08/62.13 [350]~E(x3501,x3502)+~P1(x3503)+~P1(x3502)+~P1(x3501)+~P1(x3504)+~P3(x3504,x3501,a2)+~P9(x3504,a2,x3503)+~P7(x3501,a1)+E(f9(x3501,x3502,x3503),x3503)+P3(f9(x3501,x3502,x3503),x3503,a2)+P1(f14(x3501,x3502,x3503)) % 62.08/62.13 [351]~E(x3511,x3513)+~P1(x3513)+~P1(x3512)+~P1(x3511)+~P1(x3514)+~P3(x3514,x3511,a2)+~P9(x3514,a2,x3512)+~P7(x3511,a1)+E(f9(x3511,x3512,x3513),x3512)+P3(f9(x3511,x3512,x3513),x3512,a2)+P1(f15(x3511,x3512,x3513)) % 62.08/62.13 [352]~E(x3521,x3522)+~P1(x3523)+~P1(x3522)+~P1(x3521)+~P1(x3524)+~P3(x3524,x3521,a2)+~P9(x3524,a2,x3523)+~P7(x3521,a1)+E(f9(x3521,x3522,x3523),x3522)+P3(f9(x3521,x3522,x3523),x3522,a2)+P1(f15(x3521,x3522,x3523)) % 62.08/62.13 [375]~E(x3751,x3753)+~P1(x3753)+~P1(x3752)+~P1(x3751)+~P1(x3754)+~P3(x3754,x3751,a2)+~P9(x3754,a2,x3752)+~P7(x3751,a1)+E(f9(x3751,x3752,x3753),x3753)+P3(f14(x3751,x3752,x3753),x3753,a2)+P3(f9(x3751,x3752,x3753),x3753,a2) % 62.08/62.13 [376]~E(x3761,x3762)+~P1(x3763)+~P1(x3762)+~P1(x3761)+~P1(x3764)+~P3(x3764,x3761,a2)+~P9(x3764,a2,x3763)+~P7(x3761,a1)+E(f9(x3761,x3762,x3763),x3763)+P3(f14(x3761,x3762,x3763),x3763,a2)+P3(f9(x3761,x3762,x3763),x3763,a2) % 62.08/62.13 [377]~E(x3771,x3773)+~P1(x3773)+~P1(x3772)+~P1(x3771)+~P1(x3774)+~P3(x3774,x3771,a2)+~P9(x3774,a2,x3772)+~P7(x3771,a1)+E(f9(x3771,x3772,x3773),x3772)+P3(f15(x3771,x3772,x3773),x3772,a2)+P3(f9(x3771,x3772,x3773),x3772,a2) % 62.08/62.13 [378]~E(x3781,x3782)+~P1(x3783)+~P1(x3782)+~P1(x3781)+~P1(x3784)+~P3(x3784,x3781,a2)+~P9(x3784,a2,x3783)+~P7(x3781,a1)+E(f9(x3781,x3782,x3783),x3782)+P3(f15(x3781,x3782,x3783),x3782,a2)+P3(f9(x3781,x3782,x3783),x3782,a2) % 62.08/62.13 [393]~P1(x3933)+~P1(x3932)+~P1(x3931)+~P1(x3934)+~P3(x3934,x3931,a2)+~P3(x3933,x3931,a2)+~P9(x3934,a2,x3932)+~P7(x3931,a1)+E(f9(x3931,x3932,x3933),x3933)+P3(f9(x3931,x3932,x3933),x3933,a2)+P1(f14(x3931,x3932,x3933)) % 62.08/62.13 [394]~P1(x3943)+~P1(x3942)+~P1(x3941)+~P1(x3944)+~P3(x3944,x3941,a2)+~P3(x3942,x3941,a2)+~P9(x3944,a2,x3943)+~P7(x3941,a1)+E(f9(x3941,x3942,x3943),x3943)+P3(f9(x3941,x3942,x3943),x3943,a2)+P1(f14(x3941,x3942,x3943)) % 62.08/62.13 [395]~P1(x3953)+~P1(x3952)+~P1(x3951)+~P1(x3954)+~P3(x3954,x3951,a2)+~P3(x3953,x3951,a2)+~P9(x3954,a2,x3952)+~P7(x3951,a1)+E(f9(x3951,x3952,x3953),x3952)+P3(f9(x3951,x3952,x3953),x3952,a2)+P1(f15(x3951,x3952,x3953)) % 62.08/62.13 [396]~P1(x3963)+~P1(x3962)+~P1(x3961)+~P1(x3964)+~P3(x3964,x3961,a2)+~P3(x3962,x3961,a2)+~P9(x3964,a2,x3963)+~P7(x3961,a1)+E(f9(x3961,x3962,x3963),x3962)+P3(f9(x3961,x3962,x3963),x3962,a2)+P1(f15(x3961,x3962,x3963)) % 62.08/62.13 [397]~P1(x3973)+~P1(x3972)+~P1(x3971)+~P1(x3974)+~P3(x3974,x3971,a2)+~P9(x3974,a2,x3973)+~P9(x3971,a2,x3972)+~P7(x3971,a1)+E(f9(x3971,x3972,x3973),x3973)+P3(f9(x3971,x3972,x3973),x3973,a2)+P1(f14(x3971,x3972,x3973)) % 62.08/62.13 [398]~P1(x3983)+~P1(x3982)+~P1(x3981)+~P1(x3984)+~P3(x3984,x3981,a2)+~P9(x3984,a2,x3983)+~P10(x3981,a2,x3982)+~P7(x3981,a1)+E(f9(x3981,x3982,x3983),x3983)+P3(f9(x3981,x3982,x3983),x3983,a2)+P1(f14(x3981,x3982,x3983)) % 62.08/62.13 [399]~P1(x3993)+~P1(x3992)+~P1(x3991)+~P1(x3994)+~P3(x3994,x3991,a2)+~P9(x3994,a2,x3992)+~P9(x3991,a2,x3993)+~P7(x3991,a1)+E(f9(x3991,x3992,x3993),x3993)+P3(f9(x3991,x3992,x3993),x3993,a2)+P1(f14(x3991,x3992,x3993)) % 62.08/62.13 [400]~P1(x4003)+~P1(x4002)+~P1(x4001)+~P1(x4004)+~P3(x4004,x4001,a2)+~P9(x4004,a2,x4002)+~P10(x4001,a2,x4003)+~P7(x4001,a1)+E(f9(x4001,x4002,x4003),x4003)+P3(f9(x4001,x4002,x4003),x4003,a2)+P1(f14(x4001,x4002,x4003)) % 62.08/62.13 [401]~P1(x4013)+~P1(x4012)+~P1(x4011)+~P1(x4014)+~P3(x4014,x4011,a2)+~P9(x4014,a2,x4013)+~P9(x4011,a2,x4012)+~P7(x4011,a1)+E(f9(x4011,x4012,x4013),x4012)+P3(f9(x4011,x4012,x4013),x4012,a2)+P1(f15(x4011,x4012,x4013)) % 62.08/62.13 [402]~P1(x4023)+~P1(x4022)+~P1(x4021)+~P1(x4024)+~P3(x4024,x4021,a2)+~P9(x4024,a2,x4023)+~P10(x4021,a2,x4022)+~P7(x4021,a1)+E(f9(x4021,x4022,x4023),x4022)+P3(f9(x4021,x4022,x4023),x4022,a2)+P1(f15(x4021,x4022,x4023)) % 62.08/62.13 [403]~P1(x4033)+~P1(x4032)+~P1(x4031)+~P1(x4034)+~P3(x4034,x4031,a2)+~P9(x4034,a2,x4032)+~P9(x4031,a2,x4033)+~P7(x4031,a1)+E(f9(x4031,x4032,x4033),x4032)+P3(f9(x4031,x4032,x4033),x4032,a2)+P1(f15(x4031,x4032,x4033)) % 62.08/62.13 [404]~P1(x4043)+~P1(x4042)+~P1(x4041)+~P1(x4044)+~P3(x4044,x4041,a2)+~P9(x4044,a2,x4042)+~P10(x4041,a2,x4043)+~P7(x4041,a1)+E(f9(x4041,x4042,x4043),x4042)+P3(f9(x4041,x4042,x4043),x4042,a2)+P1(f15(x4041,x4042,x4043)) % 62.08/62.13 [407]~P1(x4073)+~P1(x4072)+~P1(x4071)+~P1(x4074)+~P3(x4074,x4071,a2)+~P3(x4073,x4071,a2)+~P9(x4074,a2,x4072)+~P7(x4071,a1)+E(f9(x4071,x4072,x4073),x4073)+P3(f14(x4071,x4072,x4073),x4073,a2)+P3(f9(x4071,x4072,x4073),x4073,a2) % 62.08/62.13 [408]~P1(x4083)+~P1(x4082)+~P1(x4081)+~P1(x4084)+~P3(x4084,x4081,a2)+~P3(x4082,x4081,a2)+~P9(x4084,a2,x4083)+~P7(x4081,a1)+E(f9(x4081,x4082,x4083),x4083)+P3(f14(x4081,x4082,x4083),x4083,a2)+P3(f9(x4081,x4082,x4083),x4083,a2) % 62.08/62.13 [409]~P1(x4093)+~P1(x4092)+~P1(x4091)+~P1(x4094)+~P3(x4094,x4091,a2)+~P3(x4093,x4091,a2)+~P9(x4094,a2,x4092)+~P7(x4091,a1)+E(f9(x4091,x4092,x4093),x4092)+P3(f15(x4091,x4092,x4093),x4092,a2)+P3(f9(x4091,x4092,x4093),x4092,a2) % 62.08/62.13 [410]~P1(x4103)+~P1(x4102)+~P1(x4101)+~P1(x4104)+~P3(x4104,x4101,a2)+~P3(x4102,x4101,a2)+~P9(x4104,a2,x4103)+~P7(x4101,a1)+E(f9(x4101,x4102,x4103),x4102)+P3(f15(x4101,x4102,x4103),x4102,a2)+P3(f9(x4101,x4102,x4103),x4102,a2) % 62.08/62.13 [411]~P1(x4113)+~P1(x4112)+~P1(x4111)+~P1(x4114)+~P3(x4114,x4111,a2)+~P9(x4114,a2,x4113)+~P9(x4111,a2,x4112)+~P7(x4111,a1)+E(f9(x4111,x4112,x4113),x4113)+P3(f14(x4111,x4112,x4113),x4113,a2)+P3(f9(x4111,x4112,x4113),x4113,a2) % 62.08/62.13 [412]~P1(x4123)+~P1(x4122)+~P1(x4121)+~P1(x4124)+~P3(x4124,x4121,a2)+~P9(x4124,a2,x4123)+~P10(x4121,a2,x4122)+~P7(x4121,a1)+E(f9(x4121,x4122,x4123),x4123)+P3(f14(x4121,x4122,x4123),x4123,a2)+P3(f9(x4121,x4122,x4123),x4123,a2) % 62.08/62.13 [413]~P1(x4133)+~P1(x4132)+~P1(x4131)+~P1(x4134)+~P3(x4134,x4131,a2)+~P9(x4134,a2,x4132)+~P9(x4131,a2,x4133)+~P7(x4131,a1)+E(f9(x4131,x4132,x4133),x4133)+P3(f14(x4131,x4132,x4133),x4133,a2)+P3(f9(x4131,x4132,x4133),x4133,a2) % 62.08/62.13 [414]~P1(x4143)+~P1(x4142)+~P1(x4141)+~P1(x4144)+~P3(x4144,x4141,a2)+~P9(x4144,a2,x4142)+~P10(x4141,a2,x4143)+~P7(x4141,a1)+E(f9(x4141,x4142,x4143),x4143)+P3(f14(x4141,x4142,x4143),x4143,a2)+P3(f9(x4141,x4142,x4143),x4143,a2) % 62.08/62.13 [415]~P1(x4153)+~P1(x4152)+~P1(x4151)+~P1(x4154)+~P3(x4154,x4151,a2)+~P9(x4154,a2,x4153)+~P9(x4151,a2,x4152)+~P7(x4151,a1)+E(f9(x4151,x4152,x4153),x4152)+P3(f15(x4151,x4152,x4153),x4152,a2)+P3(f9(x4151,x4152,x4153),x4152,a2) % 62.08/62.13 [416]~P1(x4163)+~P1(x4162)+~P1(x4161)+~P1(x4164)+~P3(x4164,x4161,a2)+~P9(x4164,a2,x4163)+~P10(x4161,a2,x4162)+~P7(x4161,a1)+E(f9(x4161,x4162,x4163),x4162)+P3(f15(x4161,x4162,x4163),x4162,a2)+P3(f9(x4161,x4162,x4163),x4162,a2) % 62.08/62.13 [417]~P1(x4173)+~P1(x4172)+~P1(x4171)+~P1(x4174)+~P3(x4174,x4171,a2)+~P9(x4174,a2,x4172)+~P9(x4171,a2,x4173)+~P7(x4171,a1)+E(f9(x4171,x4172,x4173),x4172)+P3(f15(x4171,x4172,x4173),x4172,a2)+P3(f9(x4171,x4172,x4173),x4172,a2) % 62.08/62.13 [418]~P1(x4183)+~P1(x4182)+~P1(x4181)+~P1(x4184)+~P3(x4184,x4181,a2)+~P9(x4184,a2,x4182)+~P10(x4181,a2,x4183)+~P7(x4181,a1)+E(f9(x4181,x4182,x4183),x4182)+P3(f15(x4181,x4182,x4183),x4182,a2)+P3(f9(x4181,x4182,x4183),x4182,a2) % 62.08/62.13 [437]~E(x4371,x4373)+~P1(x4373)+~P1(x4372)+~P1(x4371)+~P1(x4374)+~P3(x4374,x4371,a2)+~P9(x4374,a2,x4372)+~P7(x4371,a1)+E(f9(x4371,x4372,x4373),x4373)+P9(f14(x4371,x4372,x4373),a2,f9(x4371,x4372,x4373))+P3(f9(x4371,x4372,x4373),x4373,a2) % 62.08/62.13 [438]~E(x4381,x4382)+~P1(x4383)+~P1(x4382)+~P1(x4381)+~P1(x4384)+~P3(x4384,x4381,a2)+~P9(x4384,a2,x4383)+~P7(x4381,a1)+E(f9(x4381,x4382,x4383),x4383)+P9(f14(x4381,x4382,x4383),a2,f9(x4381,x4382,x4383))+P3(f9(x4381,x4382,x4383),x4383,a2) % 62.08/62.13 [439]~E(x4391,x4393)+~P1(x4393)+~P1(x4392)+~P1(x4391)+~P1(x4394)+~P3(x4394,x4391,a2)+~P9(x4394,a2,x4392)+~P7(x4391,a1)+E(f9(x4391,x4392,x4393),x4392)+P9(f15(x4391,x4392,x4393),a2,f9(x4391,x4392,x4393))+P3(f9(x4391,x4392,x4393),x4392,a2) % 62.08/62.13 [440]~E(x4401,x4402)+~P1(x4403)+~P1(x4402)+~P1(x4401)+~P1(x4404)+~P3(x4404,x4401,a2)+~P9(x4404,a2,x4403)+~P7(x4401,a1)+E(f9(x4401,x4402,x4403),x4402)+P9(f15(x4401,x4402,x4403),a2,f9(x4401,x4402,x4403))+P3(f9(x4401,x4402,x4403),x4402,a2) % 62.08/62.13 [451]~P1(x4513)+~P1(x4512)+~P1(x4511)+~P1(x4514)+~P3(x4514,x4511,a2)+~P3(x4513,x4511,a2)+~P9(x4514,a2,x4512)+~P7(x4511,a1)+E(f9(x4511,x4512,x4513),x4513)+P9(f14(x4511,x4512,x4513),a2,f9(x4511,x4512,x4513))+P3(f9(x4511,x4512,x4513),x4513,a2) % 62.08/62.13 [452]~P1(x4523)+~P1(x4522)+~P1(x4521)+~P1(x4524)+~P3(x4524,x4521,a2)+~P3(x4522,x4521,a2)+~P9(x4524,a2,x4523)+~P7(x4521,a1)+E(f9(x4521,x4522,x4523),x4523)+P9(f14(x4521,x4522,x4523),a2,f9(x4521,x4522,x4523))+P3(f9(x4521,x4522,x4523),x4523,a2) % 62.08/62.13 [453]~P1(x4533)+~P1(x4532)+~P1(x4531)+~P1(x4534)+~P3(x4534,x4531,a2)+~P3(x4533,x4531,a2)+~P9(x4534,a2,x4532)+~P7(x4531,a1)+E(f9(x4531,x4532,x4533),x4532)+P9(f15(x4531,x4532,x4533),a2,f9(x4531,x4532,x4533))+P3(f9(x4531,x4532,x4533),x4532,a2) % 62.08/62.13 [454]~P1(x4543)+~P1(x4542)+~P1(x4541)+~P1(x4544)+~P3(x4544,x4541,a2)+~P3(x4542,x4541,a2)+~P9(x4544,a2,x4543)+~P7(x4541,a1)+E(f9(x4541,x4542,x4543),x4542)+P9(f15(x4541,x4542,x4543),a2,f9(x4541,x4542,x4543))+P3(f9(x4541,x4542,x4543),x4542,a2) % 62.08/62.13 [455]~P1(x4553)+~P1(x4552)+~P1(x4551)+~P1(x4554)+~P3(x4554,x4551,a2)+~P9(x4554,a2,x4553)+~P9(x4551,a2,x4552)+~P7(x4551,a1)+E(f9(x4551,x4552,x4553),x4553)+P9(f14(x4551,x4552,x4553),a2,f9(x4551,x4552,x4553))+P3(f9(x4551,x4552,x4553),x4553,a2) % 62.08/62.13 [456]~P1(x4563)+~P1(x4562)+~P1(x4561)+~P1(x4564)+~P3(x4564,x4561,a2)+~P9(x4564,a2,x4563)+~P10(x4561,a2,x4562)+~P7(x4561,a1)+E(f9(x4561,x4562,x4563),x4563)+P9(f14(x4561,x4562,x4563),a2,f9(x4561,x4562,x4563))+P3(f9(x4561,x4562,x4563),x4563,a2) % 62.08/62.13 [457]~P1(x4573)+~P1(x4572)+~P1(x4571)+~P1(x4574)+~P3(x4574,x4571,a2)+~P9(x4574,a2,x4572)+~P9(x4571,a2,x4573)+~P7(x4571,a1)+E(f9(x4571,x4572,x4573),x4573)+P9(f14(x4571,x4572,x4573),a2,f9(x4571,x4572,x4573))+P3(f9(x4571,x4572,x4573),x4573,a2) % 62.08/62.13 [458]~P1(x4583)+~P1(x4582)+~P1(x4581)+~P1(x4584)+~P3(x4584,x4581,a2)+~P9(x4584,a2,x4582)+~P10(x4581,a2,x4583)+~P7(x4581,a1)+E(f9(x4581,x4582,x4583),x4583)+P9(f14(x4581,x4582,x4583),a2,f9(x4581,x4582,x4583))+P3(f9(x4581,x4582,x4583),x4583,a2) % 62.08/62.13 [459]~P1(x4593)+~P1(x4592)+~P1(x4591)+~P1(x4594)+~P3(x4594,x4591,a2)+~P9(x4594,a2,x4593)+~P9(x4591,a2,x4592)+~P7(x4591,a1)+E(f9(x4591,x4592,x4593),x4592)+P9(f15(x4591,x4592,x4593),a2,f9(x4591,x4592,x4593))+P3(f9(x4591,x4592,x4593),x4592,a2) % 62.08/62.13 [460]~P1(x4603)+~P1(x4602)+~P1(x4601)+~P1(x4604)+~P3(x4604,x4601,a2)+~P9(x4604,a2,x4603)+~P10(x4601,a2,x4602)+~P7(x4601,a1)+E(f9(x4601,x4602,x4603),x4602)+P9(f15(x4601,x4602,x4603),a2,f9(x4601,x4602,x4603))+P3(f9(x4601,x4602,x4603),x4602,a2) % 62.08/62.13 [461]~P1(x4613)+~P1(x4612)+~P1(x4611)+~P1(x4614)+~P3(x4614,x4611,a2)+~P9(x4614,a2,x4612)+~P9(x4611,a2,x4613)+~P7(x4611,a1)+E(f9(x4611,x4612,x4613),x4612)+P9(f15(x4611,x4612,x4613),a2,f9(x4611,x4612,x4613))+P3(f9(x4611,x4612,x4613),x4612,a2) % 62.08/62.13 [462]~P1(x4623)+~P1(x4622)+~P1(x4621)+~P1(x4624)+~P3(x4624,x4621,a2)+~P9(x4624,a2,x4622)+~P10(x4621,a2,x4623)+~P7(x4621,a1)+E(f9(x4621,x4622,x4623),x4622)+P9(f15(x4621,x4622,x4623),a2,f9(x4621,x4622,x4623))+P3(f9(x4621,x4622,x4623),x4622,a2) % 62.15/62.13 [302]~P1(x3023)+~P1(x3022)+~P1(x3021)+~P1(x3024)+~P1(x3025)+~P3(x3024,x3021,a2)+~P3(x3025,x3021,a2)+~P9(x3024,a2,x3022)+~P9(x3025,a2,x3023)+~P7(x3021,a1)+P1(f9(x3021,x3022,x3023)) % 62.15/62.13 [353]~P1(x3533)+~P1(x3532)+~P1(x3531)+~P1(x3534)+~P1(x3535)+~P3(x3534,x3532,a2)+~P3(x3535,x3532,a2)+~P9(x3534,a2,x3533)+~P9(x3535,a2,x3531)+~P7(x3532,a1)+P10(x3531,a2,f9(x3532,x3533,x3531)) % 62.15/62.13 [354]~P1(x3543)+~P1(x3542)+~P1(x3541)+~P1(x3544)+~P1(x3545)+~P3(x3544,x3542,a2)+~P3(x3545,x3542,a2)+~P9(x3544,a2,x3541)+~P9(x3545,a2,x3543)+~P7(x3542,a1)+P10(x3541,a2,f9(x3542,x3541,x3543)) % 62.15/62.13 [379]~P1(x3792)+~P1(x3791)+~P1(x3793)+~P1(x3794)+~P1(x3795)+~P3(x3794,x3791,a2)+~P3(x3795,x3791,a2)+~P9(x3794,a2,x3792)+~P9(x3795,a2,x3793)+~P7(x3791,a1)+E(f9(x3791,x3792,x3793),x3793)+P9(x3793,a2,f9(x3791,x3792,x3793)) % 62.15/62.13 [380]~P1(x3803)+~P1(x3801)+~P1(x3802)+~P1(x3804)+~P1(x3805)+~P3(x3804,x3801,a2)+~P3(x3805,x3801,a2)+~P9(x3804,a2,x3802)+~P9(x3805,a2,x3803)+~P7(x3801,a1)+E(f9(x3801,x3802,x3803),x3802)+P9(x3802,a2,f9(x3801,x3802,x3803)) % 62.15/62.13 [443]~P1(x4433)+~P1(x4432)+~P1(x4431)+~P1(x4434)+~P1(x4435)+~P3(x4434,x4431,a2)+~P3(x4435,x4431,a2)+~P9(x4434,a2,x4432)+~P9(x4435,a2,x4433)+~P7(x4431,a1)+E(f9(x4431,x4432,x4433),x4433)+P3(f9(x4431,x4432,x4433),x4433,a2)+P1(f14(x4431,x4432,x4433)) % 62.15/62.13 [444]~P1(x4443)+~P1(x4442)+~P1(x4441)+~P1(x4444)+~P1(x4445)+~P3(x4444,x4441,a2)+~P3(x4445,x4441,a2)+~P9(x4444,a2,x4442)+~P9(x4445,a2,x4443)+~P7(x4441,a1)+E(f9(x4441,x4442,x4443),x4442)+P3(f9(x4441,x4442,x4443),x4442,a2)+P1(f15(x4441,x4442,x4443)) % 62.15/62.13 [449]~P1(x4493)+~P1(x4492)+~P1(x4491)+~P1(x4494)+~P1(x4495)+~P3(x4494,x4491,a2)+~P3(x4495,x4491,a2)+~P9(x4494,a2,x4492)+~P9(x4495,a2,x4493)+~P7(x4491,a1)+E(f9(x4491,x4492,x4493),x4493)+P3(f14(x4491,x4492,x4493),x4493,a2)+P3(f9(x4491,x4492,x4493),x4493,a2) % 62.15/62.13 [450]~P1(x4503)+~P1(x4502)+~P1(x4501)+~P1(x4504)+~P1(x4505)+~P3(x4504,x4501,a2)+~P3(x4505,x4501,a2)+~P9(x4504,a2,x4502)+~P9(x4505,a2,x4503)+~P7(x4501,a1)+E(f9(x4501,x4502,x4503),x4502)+P3(f15(x4501,x4502,x4503),x4502,a2)+P3(f9(x4501,x4502,x4503),x4502,a2) % 62.15/62.13 [463]~P1(x4633)+~P1(x4632)+~P1(x4631)+~P1(x4634)+~P1(x4635)+~P3(x4634,x4631,a2)+~P3(x4635,x4631,a2)+~P9(x4634,a2,x4632)+~P9(x4635,a2,x4633)+~P7(x4631,a1)+E(f9(x4631,x4632,x4633),x4633)+P9(f14(x4631,x4632,x4633),a2,f9(x4631,x4632,x4633))+P3(f9(x4631,x4632,x4633),x4633,a2) % 62.15/62.13 [464]~P1(x4643)+~P1(x4642)+~P1(x4641)+~P1(x4644)+~P1(x4645)+~P3(x4644,x4641,a2)+~P3(x4645,x4641,a2)+~P9(x4644,a2,x4642)+~P9(x4645,a2,x4643)+~P7(x4641,a1)+E(f9(x4641,x4642,x4643),x4642)+P9(f15(x4641,x4642,x4643),a2,f9(x4641,x4642,x4643))+P3(f9(x4641,x4642,x4643),x4642,a2) % 62.15/62.13 %EqnAxiom % 62.15/62.13 [1]E(x11,x11) % 62.15/62.13 [2]E(x22,x21)+~E(x21,x22) % 62.15/62.13 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 62.15/62.13 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 62.15/62.13 [5]~E(x51,x52)+E(f23(x51),f23(x52)) % 62.15/62.13 [6]~E(x61,x62)+E(f24(x61),f24(x62)) % 62.15/62.13 [7]~E(x71,x72)+E(f25(x71),f25(x72)) % 62.15/62.13 [8]~E(x81,x82)+E(f27(x81),f27(x82)) % 62.15/62.13 [9]~E(x91,x92)+E(f28(x91),f28(x92)) % 62.15/62.13 [10]~E(x101,x102)+E(f4(x101),f4(x102)) % 62.15/62.13 [11]~E(x111,x112)+E(f5(x111),f5(x112)) % 62.15/62.13 [12]~E(x121,x122)+E(f9(x121,x123,x124),f9(x122,x123,x124)) % 62.15/62.13 [13]~E(x131,x132)+E(f9(x133,x131,x134),f9(x133,x132,x134)) % 62.15/62.13 [14]~E(x141,x142)+E(f9(x143,x144,x141),f9(x143,x144,x142)) % 62.15/62.13 [15]~E(x151,x152)+E(f15(x151,x153,x154),f15(x152,x153,x154)) % 62.15/62.13 [16]~E(x161,x162)+E(f15(x163,x161,x164),f15(x163,x162,x164)) % 62.15/62.13 [17]~E(x171,x172)+E(f15(x173,x174,x171),f15(x173,x174,x172)) % 62.15/62.13 [18]~E(x181,x182)+E(f14(x181,x183,x184),f14(x182,x183,x184)) % 62.15/62.13 [19]~E(x191,x192)+E(f14(x193,x191,x194),f14(x193,x192,x194)) % 62.15/62.13 [20]~E(x201,x202)+E(f14(x203,x204,x201),f14(x203,x204,x202)) % 62.15/62.13 [21]~E(x211,x212)+E(f10(x211,x213,x214),f10(x212,x213,x214)) % 62.15/62.13 [22]~E(x221,x222)+E(f10(x223,x221,x224),f10(x223,x222,x224)) % 62.15/62.13 [23]~E(x231,x232)+E(f10(x233,x234,x231),f10(x233,x234,x232)) % 62.15/62.13 [24]~E(x241,x242)+E(f12(x241,x243,x244),f12(x242,x243,x244)) % 62.15/62.13 [25]~E(x251,x252)+E(f12(x253,x251,x254),f12(x253,x252,x254)) % 62.15/62.13 [26]~E(x261,x262)+E(f12(x263,x264,x261),f12(x263,x264,x262)) % 62.15/62.13 [27]~E(x271,x272)+E(f13(x271,x273,x274),f13(x272,x273,x274)) % 62.15/62.13 [28]~E(x281,x282)+E(f13(x283,x281,x284),f13(x283,x282,x284)) % 62.15/62.13 [29]~E(x291,x292)+E(f13(x293,x294,x291),f13(x293,x294,x292)) % 62.15/62.13 [30]~E(x301,x302)+E(f11(x301,x303,x304),f11(x302,x303,x304)) % 62.15/62.13 [31]~E(x311,x312)+E(f11(x313,x311,x314),f11(x313,x312,x314)) % 62.15/62.13 [32]~E(x321,x322)+E(f11(x323,x324,x321),f11(x323,x324,x322)) % 62.15/62.13 [33]~E(x331,x332)+E(f22(x331,x333,x334,x335),f22(x332,x333,x334,x335)) % 62.15/62.13 [34]~E(x341,x342)+E(f22(x343,x341,x344,x345),f22(x343,x342,x344,x345)) % 62.15/62.13 [35]~E(x351,x352)+E(f22(x353,x354,x351,x355),f22(x353,x354,x352,x355)) % 62.15/62.13 [36]~E(x361,x362)+E(f22(x363,x364,x365,x361),f22(x363,x364,x365,x362)) % 62.15/62.13 [37]~E(x371,x372)+E(f26(x371,x373,x374,x375),f26(x372,x373,x374,x375)) % 62.15/62.13 [38]~E(x381,x382)+E(f26(x383,x381,x384,x385),f26(x383,x382,x384,x385)) % 62.15/62.13 [39]~E(x391,x392)+E(f26(x393,x394,x391,x395),f26(x393,x394,x392,x395)) % 62.15/62.13 [40]~E(x401,x402)+E(f26(x403,x404,x405,x401),f26(x403,x404,x405,x402)) % 62.15/62.13 [41]~E(x411,x412)+E(f8(x411,x413,x414),f8(x412,x413,x414)) % 62.15/62.13 [42]~E(x421,x422)+E(f8(x423,x421,x424),f8(x423,x422,x424)) % 62.15/62.13 [43]~E(x431,x432)+E(f8(x433,x434,x431),f8(x433,x434,x432)) % 62.15/62.13 [44]~E(x441,x442)+E(f7(x441,x443),f7(x442,x443)) % 62.15/62.13 [45]~E(x451,x452)+E(f7(x453,x451),f7(x453,x452)) % 62.15/62.13 [46]~P1(x461)+P1(x462)+~E(x461,x462) % 62.15/62.13 [47]P9(x472,x473,x474)+~E(x471,x472)+~P9(x471,x473,x474) % 62.15/62.13 [48]P9(x483,x482,x484)+~E(x481,x482)+~P9(x483,x481,x484) % 62.15/62.13 [49]P9(x493,x494,x492)+~E(x491,x492)+~P9(x493,x494,x491) % 62.15/62.13 [50]P3(x502,x503,x504)+~E(x501,x502)+~P3(x501,x503,x504) % 62.15/62.13 [51]P3(x513,x512,x514)+~E(x511,x512)+~P3(x513,x511,x514) % 62.15/62.13 [52]P3(x523,x524,x522)+~E(x521,x522)+~P3(x523,x524,x521) % 62.15/62.13 [53]P10(x532,x533,x534)+~E(x531,x532)+~P10(x531,x533,x534) % 62.15/62.13 [54]P10(x543,x542,x544)+~E(x541,x542)+~P10(x543,x541,x544) % 62.15/62.13 [55]P10(x553,x554,x552)+~E(x551,x552)+~P10(x553,x554,x551) % 62.15/62.13 [56]P7(x562,x563)+~E(x561,x562)+~P7(x561,x563) % 62.15/62.13 [57]P7(x573,x572)+~E(x571,x572)+~P7(x573,x571) % 62.15/62.13 [58]~P2(x581)+P2(x582)+~E(x581,x582) % 62.15/62.13 [59]~P5(x591)+P5(x592)+~E(x591,x592) % 62.15/62.13 [60]~P8(x601)+P8(x602)+~E(x601,x602) % 62.15/62.13 [61]~P6(x611)+P6(x612)+~E(x611,x612) % 62.15/62.13 [62]P4(x622,x623,x624)+~E(x621,x622)+~P4(x621,x623,x624) % 62.15/62.13 [63]P4(x633,x632,x634)+~E(x631,x632)+~P4(x633,x631,x634) % 62.15/62.13 [64]P4(x643,x644,x642)+~E(x641,x642)+~P4(x643,x644,x641) % 62.15/62.13 % 62.15/62.13 %------------------------------------------- % 62.15/62.13 cnf(465,plain, % 62.15/62.13 (~P1(x4651)+~P1(x4651)+P10(x4651,x4652,x4651)+~P2(x4652)), % 62.15/62.13 inference(equality_inference,[],[113])). % 62.15/62.13 cnf(468,plain, % 62.15/62.13 (~P1(a29)+~P10(a32,a2,a29)), % 62.15/62.13 inference(equality_inference,[],[117])). % 62.15/62.13 cnf(469,plain, % 62.15/62.13 (~P1(a32)+~P9(a29,a2,a32)), % 62.15/62.13 inference(equality_inference,[],[118])). % 62.15/62.13 cnf(470,plain, % 62.15/62.13 (~P1(a32)+~P10(a29,a2,a32)), % 62.15/62.13 inference(equality_inference,[],[119])). % 62.15/62.13 cnf(472,plain, % 62.15/62.13 (~P1(x4721)+~P1(x4721)+~P1(x4722)+~P3(x4722,x4721,a2)+~P7(x4721,a1)+P1(f9(x4721,x4722,x4721))), % 62.15/62.13 inference(equality_inference,[],[162])). % 62.15/62.13 cnf(473,plain, % 62.15/62.13 (~P1(x4731)+~P1(x4731)+~P1(x4732)+~P3(x4732,x4731,a2)+~P7(x4731,a1)+P1(f9(x4731,x4731,x4732))), % 62.15/62.13 inference(equality_inference,[],[163])). % 62.15/62.13 cnf(474,plain, % 62.15/62.13 (~P1(x4741)+~P1(x4741)+~P1(x4742)+~P9(x4741,a2,x4742)+~P7(x4741,a1)+P1(f9(x4741,x4742,x4741))), % 62.15/62.13 inference(equality_inference,[],[164])). % 62.15/62.13 cnf(475,plain, % 62.15/62.13 (~P1(x4751)+~P1(x4751)+~P1(x4752)+~P10(x4751,a2,x4752)+~P7(x4751,a1)+P1(f9(x4751,x4752,x4751))), % 62.15/62.13 inference(equality_inference,[],[165])). % 62.15/62.13 cnf(476,plain, % 62.15/62.13 (~P1(x4761)+~P1(x4761)+~P1(x4762)+~P9(x4761,a2,x4762)+~P7(x4761,a1)+P1(f9(x4761,x4761,x4762))), % 62.15/62.13 inference(equality_inference,[],[166])). % 62.15/62.13 cnf(477,plain, % 62.15/62.13 (~P1(x4771)+~P1(x4771)+~P1(x4772)+~P10(x4771,a2,x4772)+~P7(x4771,a1)+P1(f9(x4771,x4771,x4772))), % 62.15/62.13 inference(equality_inference,[],[167])). % 62.15/62.13 cnf(478,plain, % 62.15/62.13 (~P1(x4781)+~P1(x4781)+~P1(x4782)+~P3(x4782,x4781,a2)+~P7(x4781,a1)+P10(x4782,a2,f9(x4781,x4781,x4782))), % 62.15/62.13 inference(equality_inference,[],[180])). % 62.15/62.13 cnf(479,plain, % 62.15/62.14 (~P1(x4791)+~P1(x4791)+~P1(x4792)+~P3(x4792,x4791,a2)+~P7(x4791,a1)+P10(x4791,a2,f9(x4791,x4792,x4791))), % 62.15/62.14 inference(equality_inference,[],[181])). % 62.15/62.14 cnf(480,plain, % 62.15/62.14 (~P1(x4801)+~P1(x4801)+~P1(x4802)+~P3(x4802,x4801,a2)+~P7(x4801,a1)+P10(x4802,a2,f9(x4801,x4802,x4801))), % 62.15/62.14 inference(equality_inference,[],[182])). % 62.15/62.14 cnf(482,plain, % 62.15/62.14 (~P1(x4821)+~P1(x4821)+~P1(x4822)+~P9(x4821,a2,x4822)+~P7(x4821,a1)+P10(x4822,a2,f9(x4821,x4821,x4822))), % 62.15/62.14 inference(equality_inference,[],[184])). % 62.15/62.14 cnf(483,plain, % 62.15/62.14 (~P1(x4831)+~P1(x4831)+~P1(x4832)+~P10(x4831,a2,x4832)+~P7(x4831,a1)+P10(x4832,a2,f9(x4831,x4831,x4832))), % 62.15/62.14 inference(equality_inference,[],[185])). % 62.15/62.14 cnf(485,plain, % 62.15/62.14 (~P1(x4851)+~P1(x4851)+~P1(x4852)+~P10(x4851,a2,x4852)+~P7(x4851,a1)+P10(x4851,a2,f9(x4851,x4852,x4851))), % 62.15/62.14 inference(equality_inference,[],[187])). % 62.15/62.14 cnf(486,plain, % 62.15/62.14 (~P1(x4861)+~P1(x4861)+~P1(x4862)+~P9(x4861,a2,x4862)+~P7(x4861,a1)+P10(x4862,a2,f9(x4861,x4862,x4861))), % 62.15/62.14 inference(equality_inference,[],[188])). % 62.15/62.14 cnf(487,plain, % 62.15/62.14 (~P1(x4871)+~P1(x4871)+~P1(x4872)+~P10(x4871,a2,x4872)+~P7(x4871,a1)+P10(x4872,a2,f9(x4871,x4872,x4871))), % 62.15/62.14 inference(equality_inference,[],[189])). % 62.15/62.14 cnf(488,plain, % 62.15/62.14 (~P1(x4881)+~P1(x4881)+~P1(x4882)+~P9(x4881,a2,x4882)+~P7(x4881,a1)+P10(x4881,a2,f9(x4881,x4881,x4882))), % 62.15/62.14 inference(equality_inference,[],[190])). % 62.15/62.14 cnf(489,plain, % 62.15/62.14 (~P1(x4891)+~P1(x4891)+~P1(x4892)+~P10(x4891,a2,x4892)+~P7(x4891,a1)+P10(x4891,a2,f9(x4891,x4891,x4892))), % 62.15/62.14 inference(equality_inference,[],[191])). % 62.15/62.14 cnf(562,plain, % 62.15/62.14 (~P10(a32,a2,a29)), % 62.15/62.14 inference(scs_inference,[],[66,468])). % 62.15/62.14 cnf(563,plain, % 62.15/62.14 (~P9(a29,a2,a32)), % 62.15/62.14 inference(scs_inference,[],[71,469])). % 62.15/62.14 cnf(564,plain, % 62.15/62.14 (~P10(a29,a2,a32)), % 62.15/62.14 inference(scs_inference,[],[71,470])). % 62.15/62.14 cnf(566,plain, % 62.15/62.14 (~E(a1,a32)), % 62.15/62.14 inference(scs_inference,[],[85,75,51])). % 62.15/62.14 cnf(568,plain, % 62.15/62.14 (P7(a31,a1)), % 62.15/62.14 inference(scs_inference,[],[65,68,85,75,51,137])). % 62.15/62.14 cnf(572,plain, % 62.15/62.14 (P7(a29,a1)), % 62.15/62.14 inference(scs_inference,[],[65,66,68,77,85,72,75,51,137,465,138])). % 62.15/62.14 cnf(576,plain, % 62.15/62.14 (P9(a1,a2,a31)), % 62.15/62.14 inference(scs_inference,[],[65,66,68,77,85,72,75,51,137,465,138,156,142])). % 62.15/62.14 cnf(580,plain, % 62.15/62.14 (P1(f9(a31,a29,a31))), % 62.15/62.14 inference(scs_inference,[],[65,66,68,77,85,72,75,79,51,137,465,138,156,142,143,475])). % 62.15/62.14 cnf(582,plain, % 62.15/62.14 (P1(f9(a31,a31,a29))), % 62.15/62.14 inference(scs_inference,[],[65,66,68,77,85,72,75,79,51,137,465,138,156,142,143,475,477])). % 62.15/62.14 cnf(584,plain, % 62.15/62.14 (P10(a29,a2,f9(a31,a31,a29))), % 62.15/62.14 inference(scs_inference,[],[65,66,68,77,85,72,75,79,51,137,465,138,156,142,143,475,477,483])). % 62.15/62.14 cnf(586,plain, % 62.15/62.14 (P10(a31,a2,f9(a31,a29,a31))), % 62.15/62.14 inference(scs_inference,[],[65,66,68,77,85,72,75,79,51,137,465,138,156,142,143,475,477,483,485])). % 62.15/62.14 cnf(588,plain, % 62.15/62.14 (P10(a29,a2,f9(a31,a29,a31))), % 62.15/62.14 inference(scs_inference,[],[65,66,68,77,85,72,75,79,51,137,465,138,156,142,143,475,477,483,485,487])). % 62.15/62.14 cnf(590,plain, % 62.15/62.14 (P10(a31,a2,f9(a31,a31,a29))), % 62.15/62.14 inference(scs_inference,[],[65,66,68,77,85,72,75,79,51,137,465,138,156,142,143,475,477,483,485,487,489])). % 62.15/62.14 cnf(596,plain, % 62.15/62.14 (~P10(a32,a2,f9(a31,a31,a29))), % 62.15/62.14 inference(scs_inference,[],[65,66,67,68,77,78,85,72,74,75,79,51,137,465,138,156,142,143,475,477,483,485,487,489,139,119,153])). % 62.15/62.14 cnf(613,plain, % 62.15/62.14 (~P10(a32,a2,f9(a31,a29,a31))), % 62.15/62.14 inference(scs_inference,[],[564,580,588,55,119,153])). % 62.15/62.14 cnf(615,plain, % 62.15/62.14 (~E(a31,a32)), % 62.15/62.14 inference(scs_inference,[],[596,564,580,588,590,55,119,153,53])). % 62.15/62.14 cnf(618,plain, % 62.15/62.14 (P7(a33,a1)), % 62.15/62.14 inference(scs_inference,[],[65,596,564,580,588,590,69,76,72,55,119,153,53,156,137])). % 62.15/62.14 cnf(622,plain, % 62.15/62.14 (P9(a1,a2,a33)), % 62.15/62.14 inference(scs_inference,[],[65,562,596,564,580,588,590,69,71,76,72,55,119,153,53,156,137,140,142])). % 62.15/62.14 cnf(624,plain, % 62.15/62.14 (P10(a1,a2,a31)), % 62.15/62.14 inference(scs_inference,[],[65,562,596,564,580,588,590,69,576,71,68,76,72,55,119,153,53,156,137,140,142,143])). % 62.15/62.14 cnf(626,plain, % 62.15/62.14 (P10(a29,a2,f9(a29,a29,f9(a31,a29,a31)))), % 62.15/62.14 inference(scs_inference,[],[65,562,596,564,580,588,590,69,576,71,68,66,572,76,72,55,119,153,53,156,137,140,142,143,489])). % 62.15/62.14 cnf(628,plain, % 62.15/62.14 (P10(a29,a2,f9(a29,f9(a31,a29,a31),a29))), % 62.15/62.14 inference(scs_inference,[],[65,562,596,564,580,588,590,69,576,71,68,66,572,76,72,55,119,153,53,156,137,140,142,143,489,485])). % 62.15/62.14 cnf(630,plain, % 62.15/62.14 (P1(f9(a29,f9(a31,a29,a31),a29))), % 62.15/62.14 inference(scs_inference,[],[65,562,596,564,580,588,590,69,576,71,68,66,572,76,72,55,119,153,53,156,137,140,142,143,489,485,475])). % 62.15/62.14 cnf(632,plain, % 62.15/62.14 (P10(f9(a31,a29,a31),a2,f9(a29,f9(a31,a29,a31),a29))), % 62.15/62.14 inference(scs_inference,[],[65,562,596,564,580,588,590,69,576,71,68,66,572,76,72,55,119,153,53,156,137,140,142,143,489,485,475,487])). % 62.15/62.14 cnf(634,plain, % 62.15/62.14 (P1(f9(a29,a29,f9(a31,a29,a31)))), % 62.15/62.14 inference(scs_inference,[],[65,562,596,564,580,588,590,69,576,71,68,66,572,76,72,55,119,153,53,156,137,140,142,143,489,485,475,487,477])). % 62.15/62.14 cnf(636,plain, % 62.15/62.14 (P10(f9(a31,a29,a31),a2,f9(a29,a29,f9(a31,a29,a31)))), % 62.15/62.14 inference(scs_inference,[],[65,562,596,564,580,588,590,69,576,71,68,66,572,76,72,55,119,153,53,156,137,140,142,143,489,485,475,487,477,483])). % 62.15/62.14 cnf(638,plain, % 62.15/62.14 (~P10(f9(a31,a29,a31),a2,a32)), % 62.15/62.14 inference(scs_inference,[],[65,562,596,564,580,588,590,69,576,71,68,66,572,76,72,55,119,153,53,156,137,140,142,143,489,485,475,487,477,483,170])). % 62.15/62.14 cnf(670,plain, % 62.15/62.14 (~P10(a32,a2,f9(a29,a29,f9(a31,a29,a31)))), % 62.15/62.14 inference(scs_inference,[],[634,632,638,626,55,119,153])). % 62.15/62.14 cnf(672,plain, % 62.15/62.14 (~E(a34,a29)), % 62.15/62.14 inference(scs_inference,[],[564,634,632,638,626,83,55,119,153,53])). % 62.15/62.14 cnf(687,plain, % 62.15/62.14 (P1(f9(a31,f9(a31,a29,a31),a31))), % 62.15/62.14 inference(scs_inference,[],[65,613,564,78,630,634,632,638,586,626,67,71,580,68,568,75,72,83,55,119,153,53,156,140,143,477,485,487,483,475])). % 62.15/62.14 cnf(691,plain, % 62.15/62.14 (~P10(f9(a29,f9(a31,a29,a31),a29),a2,a32)), % 62.15/62.14 inference(scs_inference,[],[65,613,564,78,630,634,632,638,586,626,67,71,580,68,568,75,72,83,55,119,153,53,156,140,143,477,485,487,483,475,489,170])). % 62.15/62.14 cnf(708,plain, % 62.15/62.14 (~P10(a32,a2,f9(a29,f9(a31,a29,a31),a29))), % 62.15/62.14 inference(scs_inference,[],[636,628,630,638,119,55,153])). % 62.15/62.14 cnf(716,plain, % 62.15/62.14 (P1(f9(a33,a33,a30))), % 62.15/62.14 inference(scs_inference,[],[65,670,622,687,636,628,630,638,67,71,69,618,75,72,81,119,55,153,156,140,143,477])). % 62.15/62.14 cnf(720,plain, % 62.15/62.14 (P10(a33,a2,f9(a33,a33,a30))), % 62.15/62.14 inference(scs_inference,[],[65,670,622,687,636,628,630,638,67,71,69,618,75,72,81,119,55,153,156,140,143,477,483,489])). % 62.15/62.14 cnf(724,plain, % 62.15/62.14 (P1(f9(a33,a30,a33))), % 62.15/62.14 inference(scs_inference,[],[65,670,622,687,636,628,630,638,67,71,69,618,75,72,81,119,55,153,156,140,143,477,483,489,485,475])). % 62.15/62.14 cnf(733,plain, % 62.15/62.14 (P4(a32,x7331,a2)+~E(a34,x7331)), % 62.15/62.14 inference(scs_inference,[],[65,670,77,78,622,687,636,628,630,634,638,67,71,69,580,618,75,72,81,84,119,55,153,156,140,143,477,483,489,485,475,487,170,49,56,47,63])). % 62.15/62.14 cnf(747,plain, % 62.15/62.14 (P1(f9(a31,a31,f9(a31,a31,a29)))), % 62.15/62.14 inference(scs_inference,[],[708,564,584,590,724,582,71,68,568,75,72,55,156,140,477])). % 62.15/62.14 cnf(749,plain, % 62.15/62.14 (P10(f9(a31,a31,a29),a2,f9(a31,a31,f9(a31,a31,a29)))), % 62.15/62.14 inference(scs_inference,[],[708,564,584,590,724,582,71,68,568,75,72,55,156,140,477,483])). % 62.15/62.14 cnf(757,plain, % 62.15/62.14 (P10(f9(a31,a31,a29),a2,f9(a31,f9(a31,a31,a29),a31))), % 62.15/62.14 inference(scs_inference,[],[708,564,584,590,724,582,71,68,568,75,72,55,156,140,477,483,489,475,485,487])). % 62.15/62.14 cnf(759,plain, % 62.15/62.14 (~P10(f9(a31,a31,a29),a2,a32)), % 62.15/62.14 inference(scs_inference,[],[708,564,584,590,724,582,71,66,68,568,75,72,55,156,140,477,483,489,475,485,487,170])). % 62.15/62.14 cnf(775,plain, % 62.15/62.14 (P1(f9(a33,a33,f9(a33,a33,a30)))), % 62.15/62.14 inference(scs_inference,[],[564,747,757,716,759,720,69,66,618,75,72,55,156,140,483,489,477])). % 62.15/62.14 cnf(803,plain, % 62.15/62.14 (P1(f9(a29,a29,f9(a31,a31,a29)))), % 62.15/62.14 inference(scs_inference,[],[584,775,691,749,759,630,582,66,572,75,72,55,156,140,489,477])). % 62.15/62.14 cnf(818,plain, % 62.15/62.14 (~P10(a32,a2,f9(a29,a29,f9(a31,a31,a29)))), % 62.15/62.14 inference(scs_inference,[],[584,775,691,749,747,759,630,582,71,66,572,75,72,55,156,140,489,477,483,475,485,487,170,733,119,153])). % 62.15/62.14 cnf(1039,plain, % 62.15/62.14 (~P4(a1,a32,a2)), % 62.15/62.14 inference(scs_inference,[],[71,75,72,156])). % 62.15/62.14 cnf(1457,plain, % 62.15/62.14 (P10(f9(a31,a31,a29),a2,f9(a31,a31,a29))), % 62.15/62.14 inference(scs_inference,[],[582,72,113])). % 62.15/62.14 cnf(1461,plain, % 62.15/62.14 (P10(f9(a31,a29,a31),a2,f9(a31,a29,a31))), % 62.15/62.14 inference(scs_inference,[],[580,1457,72,54,113])). % 62.15/62.14 cnf(1503,plain, % 62.15/62.14 (P10(a33,a2,a33)), % 62.15/62.14 inference(scs_inference,[],[69,72,113])). % 62.15/62.14 cnf(1526,plain, % 62.15/62.14 (P10(a32,a2,a32)), % 62.15/62.14 inference(scs_inference,[],[71,72,113])). % 62.15/62.14 cnf(1530,plain, % 62.15/62.14 (P4(a32,a32,a2)), % 62.15/62.14 inference(scs_inference,[],[564,71,1526,72,85,53,204])). % 62.15/62.14 cnf(1535,plain, % 62.15/62.14 (P10(a29,a2,a29)), % 62.15/62.14 inference(scs_inference,[],[564,71,66,1526,72,85,53,204,64,54,113])). % 62.15/62.14 cnf(1546,plain, % 62.15/62.14 (P10(a31,a2,a31)), % 62.15/62.14 inference(scs_inference,[],[68,1535,72,54,113])). % 62.15/62.14 cnf(1550,plain, % 62.15/62.14 (~P9(a32,a2,a1)+P3(a1,a32,a2)), % 62.15/62.14 inference(scs_inference,[],[65,71,68,1535,568,72,85,54,113,473,202])). % 62.15/62.14 cnf(1566,plain, % 62.15/62.14 (~P9(a32,a2,a1)), % 62.15/62.14 inference(scs_inference,[],[85,1550])). % 62.15/62.14 cnf(2118,plain, % 62.15/62.14 (P10(a29,a2,f9(a29,a29,a29))), % 62.15/62.14 inference(scs_inference,[],[1535,66,572,489])). % 62.15/62.14 cnf(2120,plain, % 62.15/62.14 (P1(f9(a29,a29,a29))), % 62.15/62.14 inference(scs_inference,[],[1535,66,572,489,475])). % 62.15/62.14 cnf(2712,plain, % 62.15/62.14 (P10(a31,a2,f9(a31,a31,a31))), % 62.15/62.14 inference(scs_inference,[],[1546,68,568,483])). % 62.15/62.14 cnf(2714,plain, % 62.15/62.14 (P1(f9(a31,a31,a31))), % 62.15/62.14 inference(scs_inference,[],[1546,68,568,483,475])). % 62.15/62.14 cnf(3051,plain, % 62.15/62.14 (P10(a1,a2,a34)), % 62.15/62.14 inference(scs_inference,[],[70,65,69,68,2712,2714,1503,624,618,568,80,72,483,489,485,487,475,477,170])). % 62.15/62.14 cnf(3549,plain, % 62.15/62.14 (P10(a1,a2,a32)), % 62.15/62.14 inference(scs_inference,[],[71,65,70,3051,83,72,170])). % 62.15/62.14 cnf(3557,plain, % 62.15/62.14 (P10(a32,a2,f9(a32,a32,a32))), % 62.15/62.14 inference(scs_inference,[],[71,564,65,1526,70,3051,566,83,72,74,170,54,53,144,139,485])). % 62.15/62.14 cnf(3559,plain, % 62.15/62.14 (P1(f9(a32,a32,a32))), % 62.15/62.14 inference(scs_inference,[],[71,564,65,1526,70,3051,566,83,72,74,170,54,53,144,139,485,475])). % 62.15/62.14 cnf(3623,plain, % 62.15/62.14 (~P9(a31,a2,a32)+P10(a32,a2,f9(a31,a31,a32))), % 62.15/62.14 inference(scs_inference,[],[71,708,630,68,3557,3559,568,72,55,170,140,479,480,482])). % 62.15/62.14 cnf(3682,plain, % 62.15/62.14 (P1(f9(a31,a32,a31))+~P9(a31,a2,a32)), % 62.15/62.14 inference(scs_inference,[],[71,818,803,69,68,3557,3559,568,618,72,55,170,140,478,472,476,488,473,474])). % 62.15/62.14 cnf(3684,plain, % 62.15/62.14 (P10(a31,a2,a32)), % 62.15/62.14 inference(scs_inference,[],[71,70,68,83,72,80,170])). % 62.15/62.14 cnf(3688,plain, % 62.15/62.14 (P9(a31,a2,a29)), % 62.15/62.14 inference(scs_inference,[],[71,564,70,66,68,83,79,72,80,170,54,53,144])). % 62.15/62.14 cnf(3709,plain, % 62.15/62.14 (P9(a31,a2,a32)), % 62.15/62.14 inference(scs_inference,[],[71,68,3684,615,72,144])). % 62.15/62.14 cnf(3715,plain, % 62.15/62.14 (P10(a33,a2,a32)), % 62.15/62.14 inference(scs_inference,[],[71,563,70,69,66,68,3684,615,83,72,82,74,144,139,168,170])). % 62.15/62.14 cnf(3718,plain, % 62.15/62.14 (~E(a33,a29)), % 62.15/62.14 inference(scs_inference,[],[71,564,563,70,69,66,68,3684,615,83,72,82,74,144,139,168,170,56,53])). % 62.15/62.14 cnf(3730,plain, % 62.15/62.14 (P10(a32,a2,f9(a31,a31,a32))), % 62.15/62.14 inference(scs_inference,[],[3709,3623])). % 62.15/62.14 cnf(3734,plain, % 62.15/62.14 (P1(f9(a31,a32,a31))), % 62.15/62.14 inference(scs_inference,[],[3709,3682])). % 62.15/62.14 cnf(3782,plain, % 62.15/62.14 (P10(a32,a2,f9(a31,a32,a31))), % 62.15/62.14 inference(scs_inference,[],[71,708,68,3709,3730,568,55,486])). % 62.15/62.14 cnf(3861,plain, % 62.15/62.14 (~P10(f9(a31,a32,a31),a2,f9(a31,a29,a31))), % 62.15/62.14 inference(scs_inference,[],[71,613,580,3734,3782,72,55,170])). % 62.15/62.14 cnf(3933,plain, % 62.15/62.14 (P1(f9(a31,a29,a32))), % 62.15/62.14 inference(scs_inference,[],[65,672,1039,1566,3861,3549,3688,3684,1461,3715,2118,2120,3782,3734,76,74,85,580,1530,69,68,71,75,618,72,568,66,2,147,152,153,151,62,53,55,134,140,143,192,219,220,477,204,489,483,485,487,475,144,199,200])). % 62.15/62.14 cnf(3939,plain, % 62.15/62.14 (P10(a32,a2,f9(a31,a29,a32))), % 62.15/62.14 inference(scs_inference,[],[65,672,1039,1566,3861,3549,3688,3684,1461,3715,2118,2120,3782,3734,76,74,85,580,1530,69,68,71,75,618,72,568,66,2,147,152,153,151,62,53,55,134,140,143,192,219,220,477,204,489,483,485,487,475,144,199,200,201,232,233])). % 62.15/62.14 cnf(3947,plain, % 62.15/62.14 (P10(a29,a2,f9(a31,a29,a32))), % 62.15/62.14 inference(scs_inference,[],[65,672,1039,1566,3861,3549,3688,3684,1461,3715,2118,2120,3782,3734,76,74,85,580,1530,69,68,71,75,618,72,568,66,2,147,152,153,151,62,53,55,134,140,143,192,219,220,477,204,489,483,485,487,475,144,199,200,201,232,233,234,235,237,238])). % 62.15/62.14 cnf(4033,plain, % 62.15/62.14 ($false), % 62.15/62.14 inference(scs_inference,[],[3718,3933,3947,3939,2,147,152,151,153]), % 62.15/62.14 ['proof']). % 62.15/62.14 % SZS output end Proof % 62.15/62.14 % Total time :60.270000s %------------------------------------------------------------------------------