%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM021+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 : n024.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 3.72s 3.75s % Output : CNFRefutation 3.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : COM021+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.12/0.34 % Computer : n024.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Jun 20 23:18:24 EDT 2024 % 0.19/0.34 % CPUTime : % 0.57/0.58 start to proof:theBenchmark % 3.71/3.73 %------------------------------------------- % 3.71/3.73 % File :CSE---1.7 % 3.71/3.73 % Problem :theBenchmark % 3.71/3.73 % Transform :cnf % 3.71/3.73 % Format :tptp:raw % 3.71/3.73 % Command :java -jar mcs_scs.jar %d %s % 3.71/3.73 % 3.71/3.73 % Result :Theorem 2.150000s % 3.71/3.73 % Output :CNFRefutation 2.150000s % 3.71/3.73 %------------------------------------------- % 3.71/3.73 %------------------------------------------------------------------------------ % 3.71/3.73 % File : COM021+4 : TPTP v8.2.0. Released v4.0.0. % 3.71/3.73 % Domain : Computing Theory % 3.71/3.73 % Problem : Newman's lemma on rewriting systems 03_01_05_02, 03 expansion % 3.71/3.73 % Version : Especial. % 3.71/3.73 % English : % 3.71/3.73 % 3.71/3.73 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 3.71/3.73 % : [PV+07] Paskevich et al. (2007), Reasoning Inside a Formula an % 3.71/3.73 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 3.71/3.73 % Source : [Pas08] % 3.71/3.73 % Names : newman_03_01_05_02.03 [Pas08] % 3.71/3.73 % 3.71/3.73 % Status : Theorem % 3.71/3.73 % Rating : 0.19 v8.2.0, 0.17 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.13 v7.3.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.13 v7.0.0, 0.07 v6.4.0, 0.08 v6.1.0, 0.10 v6.0.0, 0.04 v5.5.0, 0.15 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.15 v5.1.0, 0.19 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.1, 0.52 v4.0.0 % 3.71/3.73 % Syntax : Number of formulae : 25 ( 1 unt; 6 def) % 3.71/3.73 % Number of atoms : 223 ( 15 equ) % 3.71/3.73 % Maximal formula atoms : 33 ( 8 avg) % 3.71/3.73 % Number of connectives : 200 ( 2 ~; 40 |; 123 &) % 3.71/3.73 % ( 6 <=>; 29 =>; 0 <=; 0 <~>) % 3.71/3.73 % Maximal formula depth : 17 ( 8 avg) % 3.71/3.73 % Maximal term depth : 1 ( 1 avg) % 3.71/3.73 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 3.71/3.73 % Number of functors : 9 ( 9 usr; 9 con; 0-0 aty) % 3.71/3.73 % Number of variables : 73 ( 48 !; 25 ?) % 3.71/3.73 % SPC : FOF_THM_RFO_SEQ % 3.71/3.73 % 3.71/3.73 % Comments : Problem generated by the SAD system [VLP07] % 3.71/3.73 %------------------------------------------------------------------------------ % 3.71/3.73 fof(mElmSort,axiom, % 3.71/3.73 ! [W0] : % 3.71/3.73 ( aElement0(W0) % 3.71/3.73 => $true ) ). % 3.71/3.73 % 3.71/3.73 fof(mRelSort,axiom, % 3.71/3.73 ! [W0] : % 3.71/3.73 ( aRewritingSystem0(W0) % 3.71/3.73 => $true ) ). % 3.71/3.73 % 3.71/3.73 fof(mReduct,axiom, % 3.71/3.73 ! [W0,W1] : % 3.71/3.73 ( ( aElement0(W0) % 3.71/3.73 & aRewritingSystem0(W1) ) % 3.71/3.73 => ! [W2] : % 3.71/3.73 ( aReductOfIn0(W2,W0,W1) % 3.71/3.73 => aElement0(W2) ) ) ). % 3.71/3.73 % 3.71/3.73 fof(mWFOrd,axiom, % 3.71/3.73 ! [W0,W1] : % 3.71/3.73 ( ( aElement0(W0) % 3.71/3.73 & aElement0(W1) ) % 3.71/3.73 => ( iLess0(W0,W1) % 3.71/3.73 => $true ) ) ). % 3.71/3.73 % 3.71/3.73 fof(mTCbr,axiom, % 3.71/3.73 ! [W0,W1,W2] : % 3.71/3.73 ( ( aElement0(W0) % 3.71/3.73 & aRewritingSystem0(W1) % 3.71/3.73 & aElement0(W2) ) % 3.71/3.73 => ( sdtmndtplgtdt0(W0,W1,W2) % 3.71/3.73 => $true ) ) ). % 3.71/3.74 % 3.71/3.74 fof(mTCDef,definition, % 3.71/3.74 ! [W0,W1,W2] : % 3.71/3.74 ( ( aElement0(W0) % 3.71/3.74 & aRewritingSystem0(W1) % 3.71/3.74 & aElement0(W2) ) % 3.71/3.74 => ( sdtmndtplgtdt0(W0,W1,W2) % 3.71/3.74 <=> ( aReductOfIn0(W2,W0,W1) % 3.71/3.74 | ? [W3] : % 3.71/3.74 ( aElement0(W3) % 3.71/3.74 & aReductOfIn0(W3,W0,W1) % 3.71/3.74 & sdtmndtplgtdt0(W3,W1,W2) ) ) ) ) ). % 3.71/3.74 % 3.71/3.74 fof(mTCTrans,axiom, % 3.71/3.74 ! [W0,W1,W2,W3] : % 3.71/3.74 ( ( aElement0(W0) % 3.71/3.74 & aRewritingSystem0(W1) % 3.71/3.74 & aElement0(W2) % 3.71/3.74 & aElement0(W3) ) % 3.71/3.74 => ( ( sdtmndtplgtdt0(W0,W1,W2) % 3.71/3.74 & sdtmndtplgtdt0(W2,W1,W3) ) % 3.71/3.74 => sdtmndtplgtdt0(W0,W1,W3) ) ) ). % 3.71/3.74 % 3.72/3.74 fof(mTCRDef,definition, % 3.72/3.74 ! [W0,W1,W2] : % 3.72/3.74 ( ( aElement0(W0) % 3.72/3.74 & aRewritingSystem0(W1) % 3.72/3.74 & aElement0(W2) ) % 3.72/3.74 => ( sdtmndtasgtdt0(W0,W1,W2) % 3.72/3.74 <=> ( W0 = W2 % 3.72/3.74 | sdtmndtplgtdt0(W0,W1,W2) ) ) ) ). % 3.72/3.74 % 3.72/3.74 fof(mTCRTrans,axiom, % 3.72/3.74 ! [W0,W1,W2,W3] : % 3.72/3.74 ( ( aElement0(W0) % 3.72/3.74 & aRewritingSystem0(W1) % 3.72/3.74 & aElement0(W2) % 3.72/3.74 & aElement0(W3) ) % 3.72/3.74 => ( ( sdtmndtasgtdt0(W0,W1,W2) % 3.72/3.74 & sdtmndtasgtdt0(W2,W1,W3) ) % 3.72/3.74 => sdtmndtasgtdt0(W0,W1,W3) ) ) ). % 3.72/3.74 % 3.72/3.74 fof(mCRDef,definition, % 3.72/3.74 ! [W0] : % 3.72/3.74 ( aRewritingSystem0(W0) % 3.72/3.74 => ( isConfluent0(W0) % 3.72/3.74 <=> ! [W1,W2,W3] : % 3.72/3.74 ( ( aElement0(W1) % 3.72/3.74 & aElement0(W2) % 3.72/3.74 & aElement0(W3) % 3.72/3.74 & sdtmndtasgtdt0(W1,W0,W2) % 3.72/3.74 & sdtmndtasgtdt0(W1,W0,W3) ) % 3.72/3.74 => ? [W4] : % 3.72/3.74 ( aElement0(W4) % 3.72/3.74 & sdtmndtasgtdt0(W2,W0,W4) % 3.72/3.74 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 3.72/3.74 % 3.72/3.74 fof(mWCRDef,definition, % 3.72/3.74 ! [W0] : % 3.72/3.74 ( aRewritingSystem0(W0) % 3.72/3.74 => ( isLocallyConfluent0(W0) % 3.72/3.74 <=> ! [W1,W2,W3] : % 3.72/3.74 ( ( aElement0(W1) % 3.72/3.74 & aElement0(W2) % 3.72/3.74 & aElement0(W3) % 3.72/3.74 & aReductOfIn0(W2,W1,W0) % 3.72/3.74 & aReductOfIn0(W3,W1,W0) ) % 3.72/3.74 => ? [W4] : % 3.72/3.74 ( aElement0(W4) % 3.72/3.74 & sdtmndtasgtdt0(W2,W0,W4) % 3.72/3.74 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 3.72/3.74 % 3.72/3.74 fof(mTermin,definition, % 3.72/3.74 ! [W0] : % 3.72/3.74 ( aRewritingSystem0(W0) % 3.72/3.74 => ( isTerminating0(W0) % 3.72/3.74 <=> ! [W1,W2] : % 3.72/3.74 ( ( aElement0(W1) % 3.72/3.74 & aElement0(W2) ) % 3.72/3.74 => ( sdtmndtplgtdt0(W1,W0,W2) % 3.72/3.74 => iLess0(W2,W1) ) ) ) ) ). % 3.72/3.74 % 3.72/3.74 fof(mNFRDef,definition, % 3.72/3.74 ! [W0,W1] : % 3.72/3.74 ( ( aElement0(W0) % 3.72/3.74 & aRewritingSystem0(W1) ) % 3.72/3.74 => ! [W2] : % 3.72/3.74 ( aNormalFormOfIn0(W2,W0,W1) % 3.72/3.74 <=> ( aElement0(W2) % 3.72/3.74 & sdtmndtasgtdt0(W0,W1,W2) % 3.72/3.74 & ~ ? [W3] : aReductOfIn0(W3,W2,W1) ) ) ) ). % 3.72/3.74 % 3.72/3.74 fof(mTermNF,axiom, % 3.72/3.74 ! [W0] : % 3.72/3.74 ( ( aRewritingSystem0(W0) % 3.72/3.74 & isTerminating0(W0) ) % 3.72/3.74 => ! [W1] : % 3.72/3.74 ( aElement0(W1) % 3.72/3.74 => ? [W2] : aNormalFormOfIn0(W2,W1,W0) ) ) ). % 3.72/3.74 % 3.72/3.74 fof(m__656,hypothesis, % 3.72/3.74 aRewritingSystem0(xR) ). % 3.72/3.74 % 3.72/3.74 fof(m__656_01,hypothesis, % 3.72/3.74 ( ! [W0,W1,W2] : % 3.72/3.74 ( ( aElement0(W0) % 3.72/3.74 & aElement0(W1) % 3.72/3.74 & aElement0(W2) % 3.72/3.74 & aReductOfIn0(W1,W0,xR) % 3.72/3.74 & aReductOfIn0(W2,W0,xR) ) % 3.72/3.74 => ? [W3] : % 3.72/3.74 ( aElement0(W3) % 3.72/3.74 & ( W1 = W3 % 3.72/3.74 | ( ( aReductOfIn0(W3,W1,xR) % 3.72/3.74 | ? [W4] : % 3.72/3.74 ( aElement0(W4) % 3.72/3.74 & aReductOfIn0(W4,W1,xR) % 3.72/3.74 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 3.72/3.74 & sdtmndtplgtdt0(W1,xR,W3) ) ) % 3.72/3.74 & sdtmndtasgtdt0(W1,xR,W3) % 3.72/3.74 & ( W2 = W3 % 3.72/3.74 | ( ( aReductOfIn0(W3,W2,xR) % 3.72/3.74 | ? [W4] : % 3.72/3.74 ( aElement0(W4) % 3.72/3.74 & aReductOfIn0(W4,W2,xR) % 3.72/3.74 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 3.72/3.74 & sdtmndtplgtdt0(W2,xR,W3) ) ) % 3.72/3.74 & sdtmndtasgtdt0(W2,xR,W3) ) ) % 3.72/3.74 & isLocallyConfluent0(xR) % 3.72/3.74 & ! [W0,W1] : % 3.72/3.74 ( ( aElement0(W0) % 3.72/3.74 & aElement0(W1) ) % 3.72/3.74 => ( ( aReductOfIn0(W1,W0,xR) % 3.72/3.74 | ? [W2] : % 3.72/3.74 ( aElement0(W2) % 3.72/3.74 & aReductOfIn0(W2,W0,xR) % 3.72/3.74 & sdtmndtplgtdt0(W2,xR,W1) ) % 3.72/3.74 | sdtmndtplgtdt0(W0,xR,W1) ) % 3.72/3.74 => iLess0(W1,W0) ) ) % 3.72/3.74 & isTerminating0(xR) ) ). % 3.72/3.74 % 3.72/3.74 fof(m__731,hypothesis, % 3.72/3.74 ( aElement0(xa) % 3.72/3.74 & aElement0(xb) % 3.72/3.74 & aElement0(xc) ) ). % 3.72/3.74 % 3.72/3.74 fof(m__715,hypothesis, % 3.72/3.74 ! [W0,W1,W2] : % 3.72/3.74 ( ( aElement0(W0) % 3.72/3.74 & aElement0(W1) % 3.72/3.74 & aElement0(W2) % 3.72/3.74 & ( W0 = W1 % 3.72/3.74 | aReductOfIn0(W1,W0,xR) % 3.72/3.74 | ? [W3] : % 3.72/3.74 ( aElement0(W3) % 3.72/3.74 & aReductOfIn0(W3,W0,xR) % 3.72/3.74 & sdtmndtplgtdt0(W3,xR,W1) ) % 3.72/3.74 | sdtmndtplgtdt0(W0,xR,W1) % 3.72/3.74 | sdtmndtasgtdt0(W0,xR,W1) ) % 3.72/3.74 & ( W0 = W2 % 3.72/3.74 | aReductOfIn0(W2,W0,xR) % 3.72/3.74 | ? [W3] : % 3.72/3.74 ( aElement0(W3) % 3.72/3.74 & aReductOfIn0(W3,W0,xR) % 3.72/3.74 & sdtmndtplgtdt0(W3,xR,W2) ) % 3.72/3.74 | sdtmndtplgtdt0(W0,xR,W2) % 3.72/3.74 | sdtmndtasgtdt0(W0,xR,W2) ) ) % 3.72/3.74 => ( iLess0(W0,xa) % 3.72/3.74 => ? [W3] : % 3.72/3.74 ( aElement0(W3) % 3.72/3.74 & ( W1 = W3 % 3.72/3.74 | ( ( aReductOfIn0(W3,W1,xR) % 3.72/3.74 | ? [W4] : % 3.72/3.74 ( aElement0(W4) % 3.72/3.74 & aReductOfIn0(W4,W1,xR) % 3.72/3.74 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 3.72/3.74 & sdtmndtplgtdt0(W1,xR,W3) ) ) % 3.72/3.74 & sdtmndtasgtdt0(W1,xR,W3) % 3.72/3.74 & ( W2 = W3 % 3.72/3.74 | ( ( aReductOfIn0(W3,W2,xR) % 3.72/3.74 | ? [W4] : % 3.72/3.74 ( aElement0(W4) % 3.72/3.74 & aReductOfIn0(W4,W2,xR) % 3.72/3.74 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 3.72/3.74 & sdtmndtplgtdt0(W2,xR,W3) ) ) % 3.72/3.74 & sdtmndtasgtdt0(W2,xR,W3) ) ) ) ). % 3.72/3.74 % 3.72/3.74 fof(m__731_02,hypothesis, % 3.72/3.74 ( ( aReductOfIn0(xb,xa,xR) % 3.72/3.74 | ? [W0] : % 3.72/3.74 ( aElement0(W0) % 3.72/3.74 & aReductOfIn0(W0,xa,xR) % 3.72/3.74 & sdtmndtplgtdt0(W0,xR,xb) ) ) % 3.72/3.74 & sdtmndtplgtdt0(xa,xR,xb) % 3.72/3.74 & ( aReductOfIn0(xc,xa,xR) % 3.72/3.74 | ? [W0] : % 3.72/3.74 ( aElement0(W0) % 3.72/3.74 & aReductOfIn0(W0,xa,xR) % 3.72/3.74 & sdtmndtplgtdt0(W0,xR,xc) ) ) % 3.72/3.74 & sdtmndtplgtdt0(xa,xR,xc) ) ). % 3.72/3.74 % 3.72/3.74 fof(m__755,hypothesis, % 3.72/3.74 ( aElement0(xu) % 3.72/3.74 & aReductOfIn0(xu,xa,xR) % 3.72/3.74 & ( xu = xb % 3.72/3.74 | ( ( aReductOfIn0(xb,xu,xR) % 3.72/3.74 | ? [W0] : % 3.72/3.74 ( aElement0(W0) % 3.72/3.74 & aReductOfIn0(W0,xu,xR) % 3.72/3.74 & sdtmndtplgtdt0(W0,xR,xb) ) ) % 3.72/3.74 & sdtmndtplgtdt0(xu,xR,xb) ) ) % 3.72/3.74 & sdtmndtasgtdt0(xu,xR,xb) ) ). % 3.72/3.74 % 3.72/3.74 fof(m__779,hypothesis, % 3.72/3.74 ( aElement0(xv) % 3.72/3.74 & aReductOfIn0(xv,xa,xR) % 3.72/3.74 & ( xv = xc % 3.72/3.74 | ( ( aReductOfIn0(xc,xv,xR) % 3.72/3.74 | ? [W0] : % 3.72/3.74 ( aElement0(W0) % 3.72/3.74 & aReductOfIn0(W0,xv,xR) % 3.72/3.74 & sdtmndtplgtdt0(W0,xR,xc) ) ) % 3.72/3.74 & sdtmndtplgtdt0(xv,xR,xc) ) ) % 3.72/3.74 & sdtmndtasgtdt0(xv,xR,xc) ) ). % 3.72/3.74 % 3.72/3.74 fof(m__799,hypothesis, % 3.72/3.74 ( aElement0(xw) % 3.72/3.74 & ( xu = xw % 3.72/3.74 | ( ( aReductOfIn0(xw,xu,xR) % 3.72/3.74 | ? [W0] : % 3.72/3.74 ( aElement0(W0) % 3.72/3.74 & aReductOfIn0(W0,xu,xR) % 3.72/3.74 & sdtmndtplgtdt0(W0,xR,xw) ) ) % 3.72/3.74 & sdtmndtplgtdt0(xu,xR,xw) ) ) % 3.72/3.74 & sdtmndtasgtdt0(xu,xR,xw) % 3.72/3.74 & ( xv = xw % 3.72/3.74 | ( ( aReductOfIn0(xw,xv,xR) % 3.72/3.74 | ? [W0] : % 3.72/3.74 ( aElement0(W0) % 3.72/3.74 & aReductOfIn0(W0,xv,xR) % 3.72/3.74 & sdtmndtplgtdt0(W0,xR,xw) ) ) % 3.72/3.74 & sdtmndtplgtdt0(xv,xR,xw) ) ) % 3.72/3.74 & sdtmndtasgtdt0(xv,xR,xw) ) ). % 3.72/3.74 % 3.72/3.75 fof(m__818,hypothesis, % 3.72/3.75 ( aElement0(xd) % 3.72/3.75 & ( xw = xd % 3.72/3.75 | ( ( aReductOfIn0(xd,xw,xR) % 3.72/3.75 | ? [W0] : % 3.72/3.75 ( aElement0(W0) % 3.72/3.75 & aReductOfIn0(W0,xw,xR) % 3.72/3.75 & sdtmndtplgtdt0(W0,xR,xd) ) ) % 3.72/3.75 & sdtmndtplgtdt0(xw,xR,xd) ) ) % 3.72/3.75 & sdtmndtasgtdt0(xw,xR,xd) % 3.72/3.75 & ~ ? [W0] : aReductOfIn0(W0,xd,xR) % 3.72/3.75 & aNormalFormOfIn0(xd,xw,xR) ) ). % 3.72/3.75 % 3.72/3.75 fof(m__850,hypothesis, % 3.72/3.75 ( aElement0(xx) % 3.72/3.75 & ( xb = xx % 3.72/3.75 | ( ( aReductOfIn0(xx,xb,xR) % 3.72/3.75 | ? [W0] : % 3.72/3.75 ( aElement0(W0) % 3.72/3.75 & aReductOfIn0(W0,xb,xR) % 3.72/3.75 & sdtmndtplgtdt0(W0,xR,xx) ) ) % 3.72/3.75 & sdtmndtplgtdt0(xb,xR,xx) ) ) % 3.72/3.75 & sdtmndtasgtdt0(xb,xR,xx) % 3.72/3.75 & ( xd = xx % 3.72/3.75 | ( ( aReductOfIn0(xx,xd,xR) % 3.72/3.75 | ? [W0] : % 3.72/3.75 ( aElement0(W0) % 3.72/3.75 & aReductOfIn0(W0,xd,xR) % 3.72/3.75 & sdtmndtplgtdt0(W0,xR,xx) ) ) % 3.72/3.75 & sdtmndtplgtdt0(xd,xR,xx) ) ) % 3.72/3.75 & sdtmndtasgtdt0(xd,xR,xx) ) ). % 3.72/3.75 % 3.72/3.75 fof(m__,conjecture, % 3.72/3.75 ( xb = xd % 3.72/3.75 | aReductOfIn0(xd,xb,xR) % 3.72/3.75 | ? [W0] : % 3.72/3.75 ( aElement0(W0) % 3.72/3.75 & aReductOfIn0(W0,xb,xR) % 3.72/3.75 & sdtmndtplgtdt0(W0,xR,xd) ) % 3.72/3.75 | sdtmndtplgtdt0(xb,xR,xd) % 3.72/3.75 | sdtmndtasgtdt0(xb,xR,xd) ) ). % 3.72/3.75 % 3.72/3.75 %------------------------------------------------------------------------------ % 3.72/3.75 %------------------------------------------- % 3.72/3.75 % Proof found % 3.72/3.75 % SZS status Theorem for theBenchmark % 3.72/3.75 % SZS output start Proof % 3.72/3.75 %ClaNum:455(EqnAxiom:64) % 3.72/3.75 %VarNum:5601(SingletonVarNum:1073) % 3.72/3.75 %MaxLitNum:13 % 3.72/3.75 %MaxfuncDepth:1 % 3.72/3.75 %SharedTerms:94 % 3.72/3.75 %goalClause: 88 89 90 91 153 % 3.72/3.75 %singleGoalClaCount:4 % 3.72/3.75 [65]P1(a1) % 3.72/3.75 [66]P1(a31) % 3.72/3.75 [67]P1(a32) % 3.72/3.75 [68]P1(a33) % 3.72/3.75 [69]P1(a35) % 3.72/3.75 [70]P1(a36) % 3.72/3.75 [71]P1(a34) % 3.72/3.75 [72]P1(a37) % 3.72/3.75 [73]P2(a2) % 3.72/3.75 [74]P5(a2) % 3.72/3.75 [75]P8(a2) % 3.72/3.75 [76]P3(a33,a1,a2) % 3.72/3.75 [77]P3(a35,a1,a2) % 3.72/3.75 [78]P9(a1,a2,a31) % 3.72/3.75 [79]P9(a1,a2,a32) % 3.72/3.75 [80]P10(a31,a2,a37) % 3.72/3.75 [81]P10(a33,a2,a31) % 3.72/3.75 [82]P10(a33,a2,a36) % 3.72/3.75 [83]P10(a35,a2,a32) % 3.72/3.75 [84]P10(a35,a2,a36) % 3.72/3.75 [85]P10(a36,a2,a34) % 3.72/3.75 [86]P10(a34,a2,a37) % 3.72/3.75 [87]P4(a34,a36,a2) % 3.72/3.75 [88]~E(a34,a31) % 3.72/3.75 [89]~P3(a34,a31,a2) % 3.72/3.75 [90]~P9(a31,a2,a34) % 3.72/3.75 [91]~P10(a31,a2,a34) % 3.72/3.75 [92]~P3(x921,a34,a2) % 3.72/3.75 [101]E(a33,a31)+P9(a33,a2,a31) % 3.72/3.75 [102]E(a35,a32)+P9(a35,a2,a32) % 3.72/3.75 [103]E(a36,a33)+P9(a33,a2,a36) % 3.72/3.75 [104]E(a36,a35)+P9(a35,a2,a36) % 3.72/3.75 [105]E(a34,a36)+P9(a36,a2,a34) % 3.72/3.75 [106]E(a37,a31)+P9(a31,a2,a37) % 3.72/3.75 [107]E(a37,a34)+P9(a34,a2,a37) % 3.72/3.75 [108]P1(a6)+P3(a31,a1,a2) % 3.72/3.75 [109]P1(a16)+P3(a32,a1,a2) % 3.72/3.75 [124]P3(a31,a1,a2)+P3(a6,a1,a2) % 3.72/3.75 [125]P3(a31,a1,a2)+P9(a6,a2,a31) % 3.72/3.75 [126]P3(a32,a1,a2)+P3(a16,a1,a2) % 3.72/3.75 [127]P3(a32,a1,a2)+P9(a16,a2,a32) % 3.72/3.75 [111]E(a33,a31)+P1(a17)+P3(a31,a33,a2) % 3.72/3.75 [112]E(a35,a32)+P1(a18)+P3(a32,a35,a2) % 3.72/3.75 [113]E(a36,a33)+P1(a19)+P3(a36,a33,a2) % 3.72/3.75 [114]E(a36,a35)+P1(a20)+P3(a36,a35,a2) % 3.72/3.75 [115]E(a34,a36)+P1(a21)+P3(a34,a36,a2) % 3.72/3.75 [116]E(a37,a31)+P1(a22)+P3(a37,a31,a2) % 3.72/3.75 [117]E(a37,a34)+P1(a23)+P3(a37,a34,a2) % 3.72/3.75 [128]E(a33,a31)+P3(a31,a33,a2)+P3(a17,a33,a2) % 3.72/3.75 [129]P3(a31,a33,a2)+E(a33,a31)+P9(a17,a2,a31) % 3.72/3.75 [130]E(a35,a32)+P3(a32,a35,a2)+P3(a18,a35,a2) % 3.72/3.75 [131]P3(a32,a35,a2)+E(a35,a32)+P9(a18,a2,a32) % 3.72/3.75 [132]E(a36,a33)+P3(a36,a33,a2)+P3(a19,a33,a2) % 3.72/3.75 [133]P3(a36,a33,a2)+E(a36,a33)+P9(a19,a2,a36) % 3.72/3.75 [134]E(a36,a35)+P3(a36,a35,a2)+P3(a20,a35,a2) % 3.72/3.75 [135]P3(a36,a35,a2)+E(a36,a35)+P9(a20,a2,a36) % 3.72/3.75 [136]E(a34,a36)+P3(a34,a36,a2)+P3(a21,a36,a2) % 3.72/3.75 [137]P3(a34,a36,a2)+E(a34,a36)+P9(a21,a2,a34) % 3.72/3.75 [138]E(a37,a31)+P3(a37,a31,a2)+P3(a22,a31,a2) % 3.72/3.75 [139]P3(a37,a31,a2)+E(a37,a31)+P9(a22,a2,a37) % 3.72/3.75 [140]E(a37,a34)+P3(a37,a34,a2)+P3(a23,a34,a2) % 3.72/3.75 [141]P3(a37,a34,a2)+E(a37,a34)+P9(a23,a2,a37) % 3.72/3.75 [153]~P1(x1531)+~P3(x1531,a31,a2)+~P9(x1531,a2,a34) % 3.72/3.75 [93]~P2(x931)+P6(x931)+P1(f3(x931)) % 3.72/3.75 [94]~P2(x941)+P6(x941)+P1(f25(x941)) % 3.72/3.75 [95]~P2(x951)+P6(x951)+P1(f26(x951)) % 3.72/3.75 [96]~P2(x961)+P5(x961)+P1(f27(x961)) % 3.72/3.75 [97]~P2(x971)+P5(x971)+P1(f29(x971)) % 3.72/3.75 [98]~P2(x981)+P5(x981)+P1(f30(x981)) % 3.72/3.75 [99]~P2(x991)+P8(x991)+P1(f4(x991)) % 3.72/3.75 [100]~P2(x1001)+P8(x1001)+P1(f5(x1001)) % 3.72/3.75 [110]~P2(x1101)+P8(x1101)+~P7(f5(x1101),f4(x1101)) % 3.72/3.75 [118]~P2(x1181)+P6(x1181)+P10(f3(x1181),x1181,f25(x1181)) % 3.72/3.75 [119]~P2(x1191)+P6(x1191)+P10(f3(x1191),x1191,f26(x1191)) % 3.72/3.75 [120]~P2(x1201)+P8(x1201)+P9(f4(x1201),x1201,f5(x1201)) % 3.72/3.75 [121]~P2(x1211)+P5(x1211)+P3(f29(x1211),f27(x1211),x1211) % 3.72/3.75 [122]~P2(x1221)+P5(x1221)+P3(f30(x1221),f27(x1221),x1221) % 3.72/3.75 [145]~P1(x1452)+~P1(x1451)+P7(x1451,x1452)+~P3(x1451,x1452,a2) % 3.72/3.75 [146]~P1(x1461)+~P1(x1462)+P7(x1461,x1462)+~P9(x1462,a2,x1461) % 3.72/3.75 [142]~P1(x1422)+~P2(x1421)+~P8(x1421)+P4(f7(x1421,x1422),x1422,x1421) % 3.72/3.75 [143]~P3(x1431,x1432,x1433)+P1(x1431)+~P1(x1432)+~P2(x1433) % 3.72/3.75 [144]~P4(x1441,x1442,x1443)+P1(x1441)+~P1(x1442)+~P2(x1443) % 3.72/3.75 [148]~P1(x1481)+~P2(x1482)+~P4(x1483,x1481,x1482)+P10(x1481,x1482,x1483) % 3.72/3.75 [154]~P4(x1544,x1541,x1542)+~P1(x1541)+~P3(x1543,x1544,x1542)+~P2(x1542) % 3.72/3.75 [158]~P2(x1581)+P6(x1581)+~P1(x1582)+~P10(f25(x1581),x1581,x1582)+~P10(f26(x1581),x1581,x1582) % 3.72/3.75 [159]~P2(x1591)+P5(x1591)+~P1(x1592)+~P10(f29(x1591),x1591,x1592)+~P10(f30(x1591),x1591,x1592) % 3.72/3.75 [123]~E(x1231,x1233)+~P1(x1233)+~P1(x1231)+~P2(x1232)+P10(x1231,x1232,x1233) % 3.72/3.75 [150]~P1(x1501)+~P1(x1503)+~P2(x1502)+~P3(x1503,x1501,x1502)+P9(x1501,x1502,x1503) % 3.72/3.75 [151]~P1(x1513)+~P1(x1511)+~P2(x1512)+~P9(x1511,x1512,x1513)+P10(x1511,x1512,x1513) % 3.72/3.75 [147]~P1(x1471)+~P1(x1472)+~P8(x1473)+~P9(x1472,x1473,x1471)+P7(x1471,x1472)+~P2(x1473) % 3.72/3.75 [152]~P1(x1522)+~P1(x1521)+~P2(x1523)+~P10(x1521,x1523,x1522)+E(x1521,x1522)+P9(x1521,x1523,x1522) % 3.72/3.75 [155]~P1(x1551)+~P1(x1552)+P7(x1551,x1552)+~P1(x1553)+~P3(x1553,x1552,a2)+~P9(x1553,a2,x1551) % 3.72/3.75 [171]~P1(x1711)+~P1(x1712)+~P2(x1713)+~P9(x1712,x1713,x1711)+P3(x1711,x1712,x1713)+P1(f13(x1712,x1713,x1711)) % 3.72/3.75 [184]~P1(x1843)+~P1(x1842)+~P1(x1841)+~P3(x1843,x1841,a2)+~P3(x1842,x1841,a2)+P1(f10(x1841,x1842,x1843)) % 3.72/3.75 [194]~P1(x1941)+~P1(x1942)+~P2(x1943)+~P9(x1942,x1943,x1941)+P3(x1941,x1942,x1943)+P3(f13(x1942,x1943,x1941),x1942,x1943) % 3.72/3.75 [195]~P1(x1951)+~P1(x1952)+~P2(x1953)+~P9(x1952,x1953,x1951)+P3(x1951,x1952,x1953)+P9(f13(x1952,x1953,x1951),x1953,x1951) % 3.72/3.75 [196]~P1(x1962)+~P1(x1961)+~P2(x1963)+~P10(x1962,x1963,x1961)+P4(x1961,x1962,x1963)+P3(f8(x1962,x1963,x1961),x1961,x1963) % 3.72/3.75 [211]~P1(x2113)+~P1(x2112)+~P1(x2111)+~P3(x2113,x2112,a2)+~P3(x2111,x2112,a2)+P10(x2111,a2,f10(x2112,x2113,x2111)) % 3.72/3.75 [212]~P1(x2123)+~P1(x2122)+~P1(x2121)+~P3(x2123,x2122,a2)+~P3(x2121,x2122,a2)+P10(x2121,a2,f10(x2122,x2121,x2123)) % 3.72/3.75 [149]~E(x1491,x1493)+~E(x1491,x1492)+~P1(x1493)+~P1(x1492)+~P1(x1491)+~P7(x1491,a1)+P1(f9(x1491,x1492,x1493)) % 3.72/3.75 [156]~E(x1562,x1563)+~E(x1561,x1562)+~P1(x1563)+~P1(x1562)+~P1(x1561)+~P7(x1562,a1)+P10(x1561,a2,f9(x1562,x1563,x1561)) % 3.72/3.75 [157]~E(x1572,x1573)+~E(x1571,x1572)+~P1(x1573)+~P1(x1572)+~P1(x1571)+~P7(x1572,a1)+P10(x1571,a2,f9(x1572,x1571,x1573)) % 3.72/3.75 [160]~E(x1601,x1603)+~P1(x1603)+~P1(x1602)+~P1(x1601)+~P3(x1602,x1601,a2)+~P7(x1601,a1)+P1(f9(x1601,x1602,x1603)) % 3.72/3.75 [161]~E(x1611,x1612)+~P1(x1613)+~P1(x1612)+~P1(x1611)+~P3(x1613,x1611,a2)+~P7(x1611,a1)+P1(f9(x1611,x1612,x1613)) % 3.72/3.75 [162]~E(x1621,x1623)+~P1(x1623)+~P1(x1622)+~P1(x1621)+~P9(x1621,a2,x1622)+~P7(x1621,a1)+P1(f9(x1621,x1622,x1623)) % 3.72/3.75 [163]~E(x1631,x1633)+~P1(x1633)+~P1(x1632)+~P1(x1631)+~P10(x1631,a2,x1632)+~P7(x1631,a1)+P1(f9(x1631,x1632,x1633)) % 3.72/3.75 [164]~E(x1641,x1642)+~P1(x1643)+~P1(x1642)+~P1(x1641)+~P9(x1641,a2,x1643)+~P7(x1641,a1)+P1(f9(x1641,x1642,x1643)) % 3.72/3.75 [165]~E(x1651,x1652)+~P1(x1653)+~P1(x1652)+~P1(x1651)+~P10(x1651,a2,x1653)+~P7(x1651,a1)+P1(f9(x1651,x1652,x1653)) % 3.72/3.75 [172]~E(x1722,x1723)+~P1(x1723)+~P1(x1722)+~P1(x1721)+~P3(x1721,x1722,a2)+~P7(x1722,a1)+P10(x1721,a2,f9(x1722,x1723,x1721)) % 3.72/3.75 [173]~E(x1731,x1732)+~P1(x1733)+~P1(x1732)+~P1(x1731)+~P3(x1733,x1732,a2)+~P7(x1732,a1)+P10(x1731,a2,f9(x1732,x1733,x1731)) % 3.72/3.75 [174]~E(x1742,x1743)+~P1(x1743)+~P1(x1742)+~P1(x1741)+~P3(x1741,x1742,a2)+~P7(x1742,a1)+P10(x1741,a2,f9(x1742,x1741,x1743)) % 3.72/3.75 [175]~E(x1751,x1752)+~P1(x1753)+~P1(x1752)+~P1(x1751)+~P3(x1753,x1752,a2)+~P7(x1752,a1)+P10(x1751,a2,f9(x1752,x1751,x1753)) % 3.72/3.75 [176]~E(x1762,x1763)+~P1(x1763)+~P1(x1762)+~P1(x1761)+~P9(x1762,a2,x1761)+~P7(x1762,a1)+P10(x1761,a2,f9(x1762,x1763,x1761)) % 3.72/3.75 [177]~E(x1772,x1773)+~P1(x1773)+~P1(x1772)+~P1(x1771)+~P10(x1772,a2,x1771)+~P7(x1772,a1)+P10(x1771,a2,f9(x1772,x1773,x1771)) % 3.72/3.75 [178]~E(x1781,x1782)+~P1(x1783)+~P1(x1782)+~P1(x1781)+~P9(x1782,a2,x1783)+~P7(x1782,a1)+P10(x1781,a2,f9(x1782,x1783,x1781)) % 3.72/3.75 [179]~E(x1791,x1792)+~P1(x1793)+~P1(x1792)+~P1(x1791)+~P10(x1792,a2,x1793)+~P7(x1792,a1)+P10(x1791,a2,f9(x1792,x1793,x1791)) % 3.72/3.75 [180]~E(x1802,x1803)+~P1(x1803)+~P1(x1802)+~P1(x1801)+~P9(x1802,a2,x1801)+~P7(x1802,a1)+P10(x1801,a2,f9(x1802,x1801,x1803)) % 3.72/3.75 [181]~E(x1812,x1813)+~P1(x1813)+~P1(x1812)+~P1(x1811)+~P10(x1812,a2,x1811)+~P7(x1812,a1)+P10(x1811,a2,f9(x1812,x1811,x1813)) % 3.72/3.75 [182]~E(x1821,x1822)+~P1(x1823)+~P1(x1822)+~P1(x1821)+~P9(x1822,a2,x1823)+~P7(x1822,a1)+P10(x1821,a2,f9(x1822,x1821,x1823)) % 3.72/3.75 [183]~E(x1831,x1832)+~P1(x1833)+~P1(x1832)+~P1(x1831)+~P10(x1832,a2,x1833)+~P7(x1832,a1)+P10(x1831,a2,f9(x1832,x1831,x1833)) % 3.72/3.75 [185]~P1(x1853)+~P1(x1852)+~P1(x1851)+~P3(x1853,x1851,a2)+~P3(x1852,x1851,a2)+~P7(x1851,a1)+P1(f9(x1851,x1852,x1853)) % 3.72/3.75 [186]~P1(x1863)+~P1(x1862)+~P1(x1861)+~P3(x1863,x1861,a2)+~P9(x1861,a2,x1862)+~P7(x1861,a1)+P1(f9(x1861,x1862,x1863)) % 3.72/3.75 [187]~P1(x1873)+~P1(x1872)+~P1(x1871)+~P3(x1873,x1871,a2)+~P10(x1871,a2,x1872)+~P7(x1871,a1)+P1(f9(x1871,x1872,x1873)) % 3.72/3.75 [188]~P1(x1883)+~P1(x1882)+~P1(x1881)+~P3(x1882,x1881,a2)+~P9(x1881,a2,x1883)+~P7(x1881,a1)+P1(f9(x1881,x1882,x1883)) % 3.72/3.75 [189]~P1(x1893)+~P1(x1892)+~P1(x1891)+~P3(x1892,x1891,a2)+~P10(x1891,a2,x1893)+~P7(x1891,a1)+P1(f9(x1891,x1892,x1893)) % 3.72/3.75 [190]~P1(x1903)+~P1(x1902)+~P1(x1901)+~P9(x1901,a2,x1903)+~P9(x1901,a2,x1902)+~P7(x1901,a1)+P1(f9(x1901,x1902,x1903)) % 3.72/3.75 [191]~P1(x1913)+~P1(x1912)+~P1(x1911)+~P9(x1911,a2,x1913)+~P10(x1911,a2,x1912)+~P7(x1911,a1)+P1(f9(x1911,x1912,x1913)) % 3.72/3.75 [192]~P1(x1923)+~P1(x1922)+~P1(x1921)+~P9(x1921,a2,x1922)+~P10(x1921,a2,x1923)+~P7(x1921,a1)+P1(f9(x1921,x1922,x1923)) % 3.72/3.75 [193]~P1(x1933)+~P1(x1932)+~P1(x1931)+~P10(x1931,a2,x1933)+~P10(x1931,a2,x1932)+~P7(x1931,a1)+P1(f9(x1931,x1932,x1933)) % 3.72/3.75 [213]~P1(x2133)+~P1(x2132)+~P1(x2131)+~P3(x2133,x2132,a2)+~P3(x2131,x2132,a2)+~P7(x2132,a1)+P10(x2131,a2,f9(x2132,x2133,x2131)) % 3.72/3.75 [214]~P1(x2143)+~P1(x2142)+~P1(x2141)+~P3(x2143,x2142,a2)+~P3(x2141,x2142,a2)+~P7(x2142,a1)+P10(x2141,a2,f9(x2142,x2141,x2143)) % 3.72/3.75 [215]~P1(x2153)+~P1(x2152)+~P1(x2151)+~P3(x2153,x2152,a2)+~P9(x2152,a2,x2151)+~P7(x2152,a1)+P10(x2151,a2,f9(x2152,x2153,x2151)) % 3.72/3.75 [216]~P1(x2163)+~P1(x2162)+~P1(x2161)+~P3(x2163,x2162,a2)+~P10(x2162,a2,x2161)+~P7(x2162,a1)+P10(x2161,a2,f9(x2162,x2163,x2161)) % 3.72/3.75 [217]~P1(x2173)+~P1(x2172)+~P1(x2171)+~P3(x2171,x2172,a2)+~P9(x2172,a2,x2173)+~P7(x2172,a1)+P10(x2171,a2,f9(x2172,x2173,x2171)) % 3.72/3.75 [218]~P1(x2183)+~P1(x2182)+~P1(x2181)+~P3(x2181,x2182,a2)+~P10(x2182,a2,x2183)+~P7(x2182,a1)+P10(x2181,a2,f9(x2182,x2183,x2181)) % 3.72/3.75 [219]~P1(x2193)+~P1(x2192)+~P1(x2191)+~P3(x2193,x2192,a2)+~P9(x2192,a2,x2191)+~P7(x2192,a1)+P10(x2191,a2,f9(x2192,x2191,x2193)) % 3.72/3.75 [220]~P1(x2203)+~P1(x2202)+~P1(x2201)+~P3(x2203,x2202,a2)+~P10(x2202,a2,x2201)+~P7(x2202,a1)+P10(x2201,a2,f9(x2202,x2201,x2203)) % 3.72/3.75 [221]~P1(x2213)+~P1(x2212)+~P1(x2211)+~P3(x2211,x2212,a2)+~P9(x2212,a2,x2213)+~P7(x2212,a1)+P10(x2211,a2,f9(x2212,x2211,x2213)) % 3.72/3.75 [222]~P1(x2223)+~P1(x2222)+~P1(x2221)+~P3(x2221,x2222,a2)+~P10(x2222,a2,x2223)+~P7(x2222,a1)+P10(x2221,a2,f9(x2222,x2221,x2223)) % 3.72/3.75 [223]~P1(x2233)+~P1(x2232)+~P1(x2231)+~P9(x2232,a2,x2233)+~P9(x2232,a2,x2231)+~P7(x2232,a1)+P10(x2231,a2,f9(x2232,x2233,x2231)) % 3.72/3.75 [224]~P1(x2243)+~P1(x2242)+~P1(x2241)+~P9(x2242,a2,x2243)+~P10(x2242,a2,x2241)+~P7(x2242,a1)+P10(x2241,a2,f9(x2242,x2243,x2241)) % 3.72/3.75 [225]~P1(x2253)+~P1(x2252)+~P1(x2251)+~P9(x2252,a2,x2251)+~P10(x2252,a2,x2253)+~P7(x2252,a1)+P10(x2251,a2,f9(x2252,x2253,x2251)) % 3.72/3.75 [226]~P1(x2263)+~P1(x2262)+~P1(x2261)+~P10(x2262,a2,x2263)+~P10(x2262,a2,x2261)+~P7(x2262,a1)+P10(x2261,a2,f9(x2262,x2263,x2261)) % 3.72/3.75 [227]~P1(x2273)+~P1(x2272)+~P1(x2271)+~P9(x2272,a2,x2273)+~P9(x2272,a2,x2271)+~P7(x2272,a1)+P10(x2271,a2,f9(x2272,x2271,x2273)) % 3.72/3.75 [228]~P1(x2283)+~P1(x2282)+~P1(x2281)+~P9(x2282,a2,x2283)+~P10(x2282,a2,x2281)+~P7(x2282,a1)+P10(x2281,a2,f9(x2282,x2281,x2283)) % 3.72/3.75 [229]~P1(x2293)+~P1(x2292)+~P1(x2291)+~P9(x2292,a2,x2291)+~P10(x2292,a2,x2293)+~P7(x2292,a1)+P10(x2291,a2,f9(x2292,x2291,x2293)) % 3.72/3.75 [230]~P1(x2303)+~P1(x2302)+~P1(x2301)+~P10(x2302,a2,x2303)+~P10(x2302,a2,x2301)+~P7(x2302,a1)+P10(x2301,a2,f9(x2302,x2301,x2303)) % 3.72/3.75 [237]~P1(x2372)+~P1(x2371)+~P1(x2373)+~P3(x2372,x2371,a2)+~P3(x2373,x2371,a2)+E(f10(x2371,x2372,x2373),x2373)+P9(x2373,a2,f10(x2371,x2372,x2373)) % 3.72/3.75 [238]~P1(x2383)+~P1(x2381)+~P1(x2382)+~P3(x2383,x2381,a2)+~P3(x2382,x2381,a2)+E(f10(x2381,x2382,x2383),x2382)+P9(x2382,a2,f10(x2381,x2382,x2383)) % 3.72/3.75 [166]~P1(x1663)+~P1(x1661)+~P2(x1662)+~P3(x1664,x1661,x1662)+~P9(x1664,x1662,x1663)+P9(x1661,x1662,x1663)+~P1(x1664) % 3.72/3.75 [167]~P1(x1673)+~P1(x1671)+~P2(x1672)+~P9(x1674,x1672,x1673)+~P9(x1671,x1672,x1674)+P9(x1671,x1672,x1673)+~P1(x1674) % 3.72/3.75 [168]~P1(x1683)+~P1(x1681)+~P2(x1682)+~P10(x1684,x1682,x1683)+~P10(x1681,x1682,x1684)+P10(x1681,x1682,x1683)+~P1(x1684) % 3.72/3.75 [169]~E(x1691,x1692)+~E(x1693,x1691)+~P1(x1692)+~P1(x1691)+~P1(x1693)+~P7(x1691,a1)+E(f9(x1691,x1692,x1693),x1693)+P9(x1693,a2,f9(x1691,x1692,x1693)) % 3.72/3.75 [170]~E(x1701,x1703)+~E(x1702,x1701)+~P1(x1703)+~P1(x1701)+~P1(x1702)+~P7(x1701,a1)+E(f9(x1701,x1702,x1703),x1702)+P9(x1702,a2,f9(x1701,x1702,x1703)) % 3.72/3.75 [199]~E(x1991,x1992)+~P1(x1992)+~P1(x1991)+~P1(x1993)+~P3(x1993,x1991,a2)+~P7(x1991,a1)+E(f9(x1991,x1992,x1993),x1993)+P9(x1993,a2,f9(x1991,x1992,x1993)) % 3.72/3.75 [200]~E(x2003,x2001)+~P1(x2002)+~P1(x2001)+~P1(x2003)+~P3(x2002,x2001,a2)+~P7(x2001,a1)+E(f9(x2001,x2002,x2003),x2003)+P9(x2003,a2,f9(x2001,x2002,x2003)) % 3.72/3.75 [201]~E(x2011,x2013)+~P1(x2013)+~P1(x2011)+~P1(x2012)+~P3(x2012,x2011,a2)+~P7(x2011,a1)+E(f9(x2011,x2012,x2013),x2012)+P9(x2012,a2,f9(x2011,x2012,x2013)) % 3.72/3.75 [202]~E(x2022,x2021)+~P1(x2023)+~P1(x2021)+~P1(x2022)+~P3(x2023,x2021,a2)+~P7(x2021,a1)+E(f9(x2021,x2022,x2023),x2022)+P9(x2022,a2,f9(x2021,x2022,x2023)) % 3.72/3.75 [203]~E(x2031,x2032)+~P1(x2032)+~P1(x2031)+~P1(x2033)+~P9(x2031,a2,x2033)+~P7(x2031,a1)+E(f9(x2031,x2032,x2033),x2033)+P9(x2033,a2,f9(x2031,x2032,x2033)) % 3.72/3.75 [204]~E(x2041,x2042)+~P1(x2042)+~P1(x2041)+~P1(x2043)+~P10(x2041,a2,x2043)+~P7(x2041,a1)+E(f9(x2041,x2042,x2043),x2043)+P9(x2043,a2,f9(x2041,x2042,x2043)) % 3.72/3.75 [205]~E(x2053,x2051)+~P1(x2052)+~P1(x2051)+~P1(x2053)+~P9(x2051,a2,x2052)+~P7(x2051,a1)+E(f9(x2051,x2052,x2053),x2053)+P9(x2053,a2,f9(x2051,x2052,x2053)) % 3.72/3.75 [206]~E(x2063,x2061)+~P1(x2062)+~P1(x2061)+~P1(x2063)+~P10(x2061,a2,x2062)+~P7(x2061,a1)+E(f9(x2061,x2062,x2063),x2063)+P9(x2063,a2,f9(x2061,x2062,x2063)) % 3.72/3.75 [207]~E(x2071,x2073)+~P1(x2073)+~P1(x2071)+~P1(x2072)+~P9(x2071,a2,x2072)+~P7(x2071,a1)+E(f9(x2071,x2072,x2073),x2072)+P9(x2072,a2,f9(x2071,x2072,x2073)) % 3.72/3.75 [208]~E(x2081,x2083)+~P1(x2083)+~P1(x2081)+~P1(x2082)+~P10(x2081,a2,x2082)+~P7(x2081,a1)+E(f9(x2081,x2082,x2083),x2082)+P9(x2082,a2,f9(x2081,x2082,x2083)) % 3.72/3.75 [209]~E(x2092,x2091)+~P1(x2093)+~P1(x2091)+~P1(x2092)+~P9(x2091,a2,x2093)+~P7(x2091,a1)+E(f9(x2091,x2092,x2093),x2092)+P9(x2092,a2,f9(x2091,x2092,x2093)) % 3.72/3.75 [210]~E(x2102,x2101)+~P1(x2103)+~P1(x2101)+~P1(x2102)+~P10(x2101,a2,x2103)+~P7(x2101,a1)+E(f9(x2101,x2102,x2103),x2102)+P9(x2102,a2,f9(x2101,x2102,x2103)) % 3.72/3.75 [247]~P1(x2472)+~P1(x2471)+~P1(x2473)+~P3(x2472,x2471,a2)+~P3(x2473,x2471,a2)+~P7(x2471,a1)+E(f9(x2471,x2472,x2473),x2473)+P9(x2473,a2,f9(x2471,x2472,x2473)) % 3.72/3.75 [248]~P1(x2483)+~P1(x2481)+~P1(x2482)+~P3(x2483,x2481,a2)+~P3(x2482,x2481,a2)+~P7(x2481,a1)+E(f9(x2481,x2482,x2483),x2482)+P9(x2482,a2,f9(x2481,x2482,x2483)) % 3.72/3.75 [249]~P1(x2492)+~P1(x2491)+~P1(x2493)+~P3(x2492,x2491,a2)+~P9(x2491,a2,x2493)+~P7(x2491,a1)+E(f9(x2491,x2492,x2493),x2493)+P9(x2493,a2,f9(x2491,x2492,x2493)) % 3.72/3.75 [250]~P1(x2502)+~P1(x2501)+~P1(x2503)+~P3(x2502,x2501,a2)+~P10(x2501,a2,x2503)+~P7(x2501,a1)+E(f9(x2501,x2502,x2503),x2503)+P9(x2503,a2,f9(x2501,x2502,x2503)) % 3.72/3.75 [251]~P1(x2512)+~P1(x2511)+~P1(x2513)+~P3(x2513,x2511,a2)+~P9(x2511,a2,x2512)+~P7(x2511,a1)+E(f9(x2511,x2512,x2513),x2513)+P9(x2513,a2,f9(x2511,x2512,x2513)) % 3.72/3.75 [252]~P1(x2522)+~P1(x2521)+~P1(x2523)+~P3(x2523,x2521,a2)+~P10(x2521,a2,x2522)+~P7(x2521,a1)+E(f9(x2521,x2522,x2523),x2523)+P9(x2523,a2,f9(x2521,x2522,x2523)) % 3.72/3.75 [253]~P1(x2533)+~P1(x2531)+~P1(x2532)+~P3(x2533,x2531,a2)+~P9(x2531,a2,x2532)+~P7(x2531,a1)+E(f9(x2531,x2532,x2533),x2532)+P9(x2532,a2,f9(x2531,x2532,x2533)) % 3.72/3.75 [254]~P1(x2543)+~P1(x2541)+~P1(x2542)+~P3(x2543,x2541,a2)+~P10(x2541,a2,x2542)+~P7(x2541,a1)+E(f9(x2541,x2542,x2543),x2542)+P9(x2542,a2,f9(x2541,x2542,x2543)) % 3.72/3.75 [255]~P1(x2553)+~P1(x2551)+~P1(x2552)+~P3(x2552,x2551,a2)+~P9(x2551,a2,x2553)+~P7(x2551,a1)+E(f9(x2551,x2552,x2553),x2552)+P9(x2552,a2,f9(x2551,x2552,x2553)) % 3.72/3.75 [256]~P1(x2563)+~P1(x2561)+~P1(x2562)+~P3(x2562,x2561,a2)+~P10(x2561,a2,x2563)+~P7(x2561,a1)+E(f9(x2561,x2562,x2563),x2562)+P9(x2562,a2,f9(x2561,x2562,x2563)) % 3.72/3.75 [257]~P1(x2572)+~P1(x2571)+~P1(x2573)+~P9(x2571,a2,x2572)+~P9(x2571,a2,x2573)+~P7(x2571,a1)+E(f9(x2571,x2572,x2573),x2573)+P9(x2573,a2,f9(x2571,x2572,x2573)) % 3.72/3.75 [258]~P1(x2582)+~P1(x2581)+~P1(x2583)+~P9(x2581,a2,x2582)+~P10(x2581,a2,x2583)+~P7(x2581,a1)+E(f9(x2581,x2582,x2583),x2583)+P9(x2583,a2,f9(x2581,x2582,x2583)) % 3.72/3.75 [259]~P1(x2592)+~P1(x2591)+~P1(x2593)+~P9(x2591,a2,x2593)+~P10(x2591,a2,x2592)+~P7(x2591,a1)+E(f9(x2591,x2592,x2593),x2593)+P9(x2593,a2,f9(x2591,x2592,x2593)) % 3.72/3.75 [260]~P1(x2602)+~P1(x2601)+~P1(x2603)+~P10(x2601,a2,x2602)+~P10(x2601,a2,x2603)+~P7(x2601,a1)+E(f9(x2601,x2602,x2603),x2603)+P9(x2603,a2,f9(x2601,x2602,x2603)) % 3.72/3.75 [261]~P1(x2613)+~P1(x2611)+~P1(x2612)+~P9(x2611,a2,x2613)+~P9(x2611,a2,x2612)+~P7(x2611,a1)+E(f9(x2611,x2612,x2613),x2612)+P9(x2612,a2,f9(x2611,x2612,x2613)) % 3.72/3.75 [262]~P1(x2623)+~P1(x2621)+~P1(x2622)+~P9(x2621,a2,x2623)+~P10(x2621,a2,x2622)+~P7(x2621,a1)+E(f9(x2621,x2622,x2623),x2622)+P9(x2622,a2,f9(x2621,x2622,x2623)) % 3.72/3.75 [263]~P1(x2633)+~P1(x2631)+~P1(x2632)+~P9(x2631,a2,x2632)+~P10(x2631,a2,x2633)+~P7(x2631,a1)+E(f9(x2631,x2632,x2633),x2632)+P9(x2632,a2,f9(x2631,x2632,x2633)) % 3.72/3.75 [264]~P1(x2643)+~P1(x2641)+~P1(x2642)+~P10(x2641,a2,x2643)+~P10(x2641,a2,x2642)+~P7(x2641,a1)+E(f9(x2641,x2642,x2643),x2642)+P9(x2642,a2,f9(x2641,x2642,x2643)) % 3.72/3.75 [306]~P1(x3063)+~P1(x3062)+~P1(x3061)+~P3(x3063,x3061,a2)+~P3(x3062,x3061,a2)+E(f10(x3061,x3062,x3063),x3063)+P3(f10(x3061,x3062,x3063),x3063,a2)+P1(f11(x3061,x3062,x3063)) % 3.72/3.75 [307]~P1(x3073)+~P1(x3072)+~P1(x3071)+~P3(x3073,x3071,a2)+~P3(x3072,x3071,a2)+E(f10(x3071,x3072,x3073),x3072)+P3(f10(x3071,x3072,x3073),x3072,a2)+P1(f12(x3071,x3072,x3073)) % 3.72/3.75 [346]~P1(x3463)+~P1(x3462)+~P1(x3461)+~P3(x3463,x3461,a2)+~P3(x3462,x3461,a2)+E(f10(x3461,x3462,x3463),x3463)+P3(f11(x3461,x3462,x3463),x3463,a2)+P3(f10(x3461,x3462,x3463),x3463,a2) % 3.72/3.75 [347]~P1(x3473)+~P1(x3472)+~P1(x3471)+~P3(x3473,x3471,a2)+~P3(x3472,x3471,a2)+E(f10(x3471,x3472,x3473),x3472)+P3(f12(x3471,x3472,x3473),x3472,a2)+P3(f10(x3471,x3472,x3473),x3472,a2) % 3.72/3.75 [396]~P1(x3963)+~P1(x3962)+~P1(x3961)+~P3(x3963,x3961,a2)+~P3(x3962,x3961,a2)+E(f10(x3961,x3962,x3963),x3963)+P9(f11(x3961,x3962,x3963),a2,f10(x3961,x3962,x3963))+P3(f10(x3961,x3962,x3963),x3963,a2) % 3.72/3.75 [397]~P1(x3973)+~P1(x3972)+~P1(x3971)+~P3(x3973,x3971,a2)+~P3(x3972,x3971,a2)+E(f10(x3971,x3972,x3973),x3972)+P9(f12(x3971,x3972,x3973),a2,f10(x3971,x3972,x3973))+P3(f10(x3971,x3972,x3973),x3972,a2) % 3.72/3.75 [432]~P1(x4324)+~P1(x4323)+~P1(x4322)+~P2(x4321)+~P6(x4321)+~P10(x4322,x4321,x4324)+~P10(x4322,x4321,x4323)+P1(f24(x4321,x4322,x4323,x4324)) % 3.72/3.75 [433]~P1(x4334)+~P1(x4333)+~P1(x4332)+~P2(x4331)+~P5(x4331)+~P3(x4334,x4332,x4331)+~P3(x4333,x4332,x4331)+P1(f28(x4331,x4332,x4333,x4334)) % 3.72/3.75 [436]~P1(x4364)+~P1(x4363)+~P1(x4361)+~P2(x4362)+~P6(x4362)+~P10(x4363,x4362,x4364)+~P10(x4363,x4362,x4361)+P10(x4361,x4362,f24(x4362,x4363,x4364,x4361)) % 3.72/3.75 [437]~P1(x4374)+~P1(x4373)+~P1(x4371)+~P2(x4372)+~P6(x4372)+~P10(x4373,x4372,x4374)+~P10(x4373,x4372,x4371)+P10(x4371,x4372,f24(x4372,x4373,x4371,x4374)) % 3.72/3.75 [438]~P1(x4384)+~P1(x4383)+~P1(x4381)+~P2(x4382)+~P5(x4382)+~P3(x4384,x4383,x4382)+~P3(x4381,x4383,x4382)+P10(x4381,x4382,f28(x4382,x4383,x4384,x4381)) % 3.72/3.75 [439]~P1(x4394)+~P1(x4393)+~P1(x4391)+~P2(x4392)+~P5(x4392)+~P3(x4394,x4393,x4392)+~P3(x4391,x4393,x4392)+P10(x4391,x4392,f28(x4392,x4393,x4391,x4394)) % 3.72/3.75 [231]~E(x2311,x2313)+~E(x2311,x2312)+~P1(x2313)+~P1(x2312)+~P1(x2311)+~P7(x2311,a1)+E(f9(x2311,x2312,x2313),x2313)+P3(f9(x2311,x2312,x2313),x2313,a2)+P1(f14(x2311,x2312,x2313)) % 3.72/3.75 [232]~E(x2321,x2323)+~E(x2321,x2322)+~P1(x2323)+~P1(x2322)+~P1(x2321)+~P7(x2321,a1)+E(f9(x2321,x2322,x2323),x2322)+P3(f9(x2321,x2322,x2323),x2322,a2)+P1(f15(x2321,x2322,x2323)) % 3.72/3.75 [245]~E(x2451,x2453)+~E(x2451,x2452)+~P1(x2453)+~P1(x2452)+~P1(x2451)+~P7(x2451,a1)+E(f9(x2451,x2452,x2453),x2453)+P3(f14(x2451,x2452,x2453),x2453,a2)+P3(f9(x2451,x2452,x2453),x2453,a2) % 3.72/3.75 [246]~E(x2461,x2463)+~E(x2461,x2462)+~P1(x2463)+~P1(x2462)+~P1(x2461)+~P7(x2461,a1)+E(f9(x2461,x2462,x2463),x2462)+P3(f15(x2461,x2462,x2463),x2462,a2)+P3(f9(x2461,x2462,x2463),x2462,a2) % 3.72/3.75 [269]~E(x2691,x2693)+~P1(x2693)+~P1(x2692)+~P1(x2691)+~P3(x2692,x2691,a2)+~P7(x2691,a1)+E(f9(x2691,x2692,x2693),x2693)+P3(f9(x2691,x2692,x2693),x2693,a2)+P1(f14(x2691,x2692,x2693)) % 3.72/3.75 [270]~E(x2701,x2702)+~P1(x2703)+~P1(x2702)+~P1(x2701)+~P3(x2703,x2701,a2)+~P7(x2701,a1)+E(f9(x2701,x2702,x2703),x2703)+P3(f9(x2701,x2702,x2703),x2703,a2)+P1(f14(x2701,x2702,x2703)) % 3.72/3.75 [271]~E(x2711,x2713)+~P1(x2713)+~P1(x2712)+~P1(x2711)+~P3(x2712,x2711,a2)+~P7(x2711,a1)+E(f9(x2711,x2712,x2713),x2712)+P3(f9(x2711,x2712,x2713),x2712,a2)+P1(f15(x2711,x2712,x2713)) % 3.72/3.75 [272]~E(x2721,x2722)+~P1(x2723)+~P1(x2722)+~P1(x2721)+~P3(x2723,x2721,a2)+~P7(x2721,a1)+E(f9(x2721,x2722,x2723),x2722)+P3(f9(x2721,x2722,x2723),x2722,a2)+P1(f15(x2721,x2722,x2723)) % 3.72/3.75 [273]~E(x2731,x2733)+~P1(x2733)+~P1(x2732)+~P1(x2731)+~P9(x2731,a2,x2732)+~P7(x2731,a1)+E(f9(x2731,x2732,x2733),x2733)+P3(f9(x2731,x2732,x2733),x2733,a2)+P1(f14(x2731,x2732,x2733)) % 3.72/3.75 [274]~E(x2741,x2743)+~P1(x2743)+~P1(x2742)+~P1(x2741)+~P10(x2741,a2,x2742)+~P7(x2741,a1)+E(f9(x2741,x2742,x2743),x2743)+P3(f9(x2741,x2742,x2743),x2743,a2)+P1(f14(x2741,x2742,x2743)) % 3.72/3.75 [275]~E(x2751,x2752)+~P1(x2753)+~P1(x2752)+~P1(x2751)+~P9(x2751,a2,x2753)+~P7(x2751,a1)+E(f9(x2751,x2752,x2753),x2753)+P3(f9(x2751,x2752,x2753),x2753,a2)+P1(f14(x2751,x2752,x2753)) % 3.72/3.75 [276]~E(x2761,x2762)+~P1(x2763)+~P1(x2762)+~P1(x2761)+~P10(x2761,a2,x2763)+~P7(x2761,a1)+E(f9(x2761,x2762,x2763),x2763)+P3(f9(x2761,x2762,x2763),x2763,a2)+P1(f14(x2761,x2762,x2763)) % 3.72/3.75 [277]~E(x2771,x2773)+~P1(x2773)+~P1(x2772)+~P1(x2771)+~P9(x2771,a2,x2772)+~P7(x2771,a1)+E(f9(x2771,x2772,x2773),x2772)+P3(f9(x2771,x2772,x2773),x2772,a2)+P1(f15(x2771,x2772,x2773)) % 3.72/3.75 [278]~E(x2781,x2783)+~P1(x2783)+~P1(x2782)+~P1(x2781)+~P10(x2781,a2,x2782)+~P7(x2781,a1)+E(f9(x2781,x2782,x2783),x2782)+P3(f9(x2781,x2782,x2783),x2782,a2)+P1(f15(x2781,x2782,x2783)) % 3.72/3.75 [279]~E(x2791,x2792)+~P1(x2793)+~P1(x2792)+~P1(x2791)+~P9(x2791,a2,x2793)+~P7(x2791,a1)+E(f9(x2791,x2792,x2793),x2792)+P3(f9(x2791,x2792,x2793),x2792,a2)+P1(f15(x2791,x2792,x2793)) % 3.72/3.75 [280]~E(x2801,x2802)+~P1(x2803)+~P1(x2802)+~P1(x2801)+~P10(x2801,a2,x2803)+~P7(x2801,a1)+E(f9(x2801,x2802,x2803),x2802)+P3(f9(x2801,x2802,x2803),x2802,a2)+P1(f15(x2801,x2802,x2803)) % 3.72/3.75 [294]~E(x2941,x2943)+~P1(x2943)+~P1(x2942)+~P1(x2941)+~P3(x2942,x2941,a2)+~P7(x2941,a1)+E(f9(x2941,x2942,x2943),x2943)+P3(f14(x2941,x2942,x2943),x2943,a2)+P3(f9(x2941,x2942,x2943),x2943,a2) % 3.72/3.75 [295]~E(x2951,x2952)+~P1(x2953)+~P1(x2952)+~P1(x2951)+~P3(x2953,x2951,a2)+~P7(x2951,a1)+E(f9(x2951,x2952,x2953),x2953)+P3(f14(x2951,x2952,x2953),x2953,a2)+P3(f9(x2951,x2952,x2953),x2953,a2) % 3.72/3.75 [296]~E(x2961,x2963)+~P1(x2963)+~P1(x2962)+~P1(x2961)+~P3(x2962,x2961,a2)+~P7(x2961,a1)+E(f9(x2961,x2962,x2963),x2962)+P3(f15(x2961,x2962,x2963),x2962,a2)+P3(f9(x2961,x2962,x2963),x2962,a2) % 3.72/3.75 [297]~E(x2971,x2972)+~P1(x2973)+~P1(x2972)+~P1(x2971)+~P3(x2973,x2971,a2)+~P7(x2971,a1)+E(f9(x2971,x2972,x2973),x2972)+P3(f15(x2971,x2972,x2973),x2972,a2)+P3(f9(x2971,x2972,x2973),x2972,a2) % 3.72/3.75 [298]~E(x2981,x2983)+~P1(x2983)+~P1(x2982)+~P1(x2981)+~P9(x2981,a2,x2982)+~P7(x2981,a1)+E(f9(x2981,x2982,x2983),x2983)+P3(f14(x2981,x2982,x2983),x2983,a2)+P3(f9(x2981,x2982,x2983),x2983,a2) % 3.72/3.75 [299]~E(x2991,x2993)+~P1(x2993)+~P1(x2992)+~P1(x2991)+~P10(x2991,a2,x2992)+~P7(x2991,a1)+E(f9(x2991,x2992,x2993),x2993)+P3(f14(x2991,x2992,x2993),x2993,a2)+P3(f9(x2991,x2992,x2993),x2993,a2) % 3.72/3.75 [300]~E(x3001,x3002)+~P1(x3003)+~P1(x3002)+~P1(x3001)+~P9(x3001,a2,x3003)+~P7(x3001,a1)+E(f9(x3001,x3002,x3003),x3003)+P3(f14(x3001,x3002,x3003),x3003,a2)+P3(f9(x3001,x3002,x3003),x3003,a2) % 3.72/3.75 [301]~E(x3011,x3012)+~P1(x3013)+~P1(x3012)+~P1(x3011)+~P10(x3011,a2,x3013)+~P7(x3011,a1)+E(f9(x3011,x3012,x3013),x3013)+P3(f14(x3011,x3012,x3013),x3013,a2)+P3(f9(x3011,x3012,x3013),x3013,a2) % 3.72/3.75 [302]~E(x3021,x3023)+~P1(x3023)+~P1(x3022)+~P1(x3021)+~P9(x3021,a2,x3022)+~P7(x3021,a1)+E(f9(x3021,x3022,x3023),x3022)+P3(f15(x3021,x3022,x3023),x3022,a2)+P3(f9(x3021,x3022,x3023),x3022,a2) % 3.72/3.75 [303]~E(x3031,x3033)+~P1(x3033)+~P1(x3032)+~P1(x3031)+~P10(x3031,a2,x3032)+~P7(x3031,a1)+E(f9(x3031,x3032,x3033),x3032)+P3(f15(x3031,x3032,x3033),x3032,a2)+P3(f9(x3031,x3032,x3033),x3032,a2) % 3.72/3.75 [304]~E(x3041,x3042)+~P1(x3043)+~P1(x3042)+~P1(x3041)+~P9(x3041,a2,x3043)+~P7(x3041,a1)+E(f9(x3041,x3042,x3043),x3042)+P3(f15(x3041,x3042,x3043),x3042,a2)+P3(f9(x3041,x3042,x3043),x3042,a2) % 3.72/3.75 [305]~E(x3051,x3052)+~P1(x3053)+~P1(x3052)+~P1(x3051)+~P10(x3051,a2,x3053)+~P7(x3051,a1)+E(f9(x3051,x3052,x3053),x3052)+P3(f15(x3051,x3052,x3053),x3052,a2)+P3(f9(x3051,x3052,x3053),x3052,a2) % 3.72/3.75 [320]~E(x3201,x3203)+~E(x3201,x3202)+~P1(x3203)+~P1(x3202)+~P1(x3201)+~P7(x3201,a1)+E(f9(x3201,x3202,x3203),x3203)+P9(f14(x3201,x3202,x3203),a2,f9(x3201,x3202,x3203))+P3(f9(x3201,x3202,x3203),x3203,a2) % 3.72/3.75 [321]~E(x3211,x3213)+~E(x3211,x3212)+~P1(x3213)+~P1(x3212)+~P1(x3211)+~P7(x3211,a1)+E(f9(x3211,x3212,x3213),x3212)+P9(f15(x3211,x3212,x3213),a2,f9(x3211,x3212,x3213))+P3(f9(x3211,x3212,x3213),x3212,a2) % 3.72/3.75 [322]~P1(x3223)+~P1(x3222)+~P1(x3221)+~P3(x3223,x3221,a2)+~P3(x3222,x3221,a2)+~P7(x3221,a1)+E(f9(x3221,x3222,x3223),x3223)+P3(f9(x3221,x3222,x3223),x3223,a2)+P1(f14(x3221,x3222,x3223)) % 3.72/3.75 [323]~P1(x3233)+~P1(x3232)+~P1(x3231)+~P3(x3233,x3231,a2)+~P3(x3232,x3231,a2)+~P7(x3231,a1)+E(f9(x3231,x3232,x3233),x3232)+P3(f9(x3231,x3232,x3233),x3232,a2)+P1(f15(x3231,x3232,x3233)) % 3.72/3.75 [324]~P1(x3243)+~P1(x3242)+~P1(x3241)+~P3(x3243,x3241,a2)+~P9(x3241,a2,x3242)+~P7(x3241,a1)+E(f9(x3241,x3242,x3243),x3243)+P3(f9(x3241,x3242,x3243),x3243,a2)+P1(f14(x3241,x3242,x3243)) % 3.72/3.75 [325]~P1(x3253)+~P1(x3252)+~P1(x3251)+~P3(x3253,x3251,a2)+~P10(x3251,a2,x3252)+~P7(x3251,a1)+E(f9(x3251,x3252,x3253),x3253)+P3(f9(x3251,x3252,x3253),x3253,a2)+P1(f14(x3251,x3252,x3253)) % 3.72/3.75 [326]~P1(x3263)+~P1(x3262)+~P1(x3261)+~P3(x3262,x3261,a2)+~P9(x3261,a2,x3263)+~P7(x3261,a1)+E(f9(x3261,x3262,x3263),x3263)+P3(f9(x3261,x3262,x3263),x3263,a2)+P1(f14(x3261,x3262,x3263)) % 3.72/3.75 [327]~P1(x3273)+~P1(x3272)+~P1(x3271)+~P3(x3272,x3271,a2)+~P10(x3271,a2,x3273)+~P7(x3271,a1)+E(f9(x3271,x3272,x3273),x3273)+P3(f9(x3271,x3272,x3273),x3273,a2)+P1(f14(x3271,x3272,x3273)) % 3.72/3.75 [328]~P1(x3283)+~P1(x3282)+~P1(x3281)+~P3(x3283,x3281,a2)+~P9(x3281,a2,x3282)+~P7(x3281,a1)+E(f9(x3281,x3282,x3283),x3282)+P3(f9(x3281,x3282,x3283),x3282,a2)+P1(f15(x3281,x3282,x3283)) % 3.72/3.75 [329]~P1(x3293)+~P1(x3292)+~P1(x3291)+~P3(x3293,x3291,a2)+~P10(x3291,a2,x3292)+~P7(x3291,a1)+E(f9(x3291,x3292,x3293),x3292)+P3(f9(x3291,x3292,x3293),x3292,a2)+P1(f15(x3291,x3292,x3293)) % 3.72/3.75 [330]~P1(x3303)+~P1(x3302)+~P1(x3301)+~P3(x3302,x3301,a2)+~P9(x3301,a2,x3303)+~P7(x3301,a1)+E(f9(x3301,x3302,x3303),x3302)+P3(f9(x3301,x3302,x3303),x3302,a2)+P1(f15(x3301,x3302,x3303)) % 3.72/3.75 [331]~P1(x3313)+~P1(x3312)+~P1(x3311)+~P3(x3312,x3311,a2)+~P10(x3311,a2,x3313)+~P7(x3311,a1)+E(f9(x3311,x3312,x3313),x3312)+P3(f9(x3311,x3312,x3313),x3312,a2)+P1(f15(x3311,x3312,x3313)) % 3.72/3.75 [332]~P1(x3323)+~P1(x3322)+~P1(x3321)+~P9(x3321,a2,x3323)+~P9(x3321,a2,x3322)+~P7(x3321,a1)+E(f9(x3321,x3322,x3323),x3323)+P3(f9(x3321,x3322,x3323),x3323,a2)+P1(f14(x3321,x3322,x3323)) % 3.72/3.75 [333]~P1(x3333)+~P1(x3332)+~P1(x3331)+~P9(x3331,a2,x3333)+~P10(x3331,a2,x3332)+~P7(x3331,a1)+E(f9(x3331,x3332,x3333),x3333)+P3(f9(x3331,x3332,x3333),x3333,a2)+P1(f14(x3331,x3332,x3333)) % 3.72/3.75 [334]~P1(x3343)+~P1(x3342)+~P1(x3341)+~P9(x3341,a2,x3342)+~P10(x3341,a2,x3343)+~P7(x3341,a1)+E(f9(x3341,x3342,x3343),x3343)+P3(f9(x3341,x3342,x3343),x3343,a2)+P1(f14(x3341,x3342,x3343)) % 3.72/3.75 [335]~P1(x3353)+~P1(x3352)+~P1(x3351)+~P10(x3351,a2,x3353)+~P10(x3351,a2,x3352)+~P7(x3351,a1)+E(f9(x3351,x3352,x3353),x3353)+P3(f9(x3351,x3352,x3353),x3353,a2)+P1(f14(x3351,x3352,x3353)) % 3.72/3.75 [336]~P1(x3363)+~P1(x3362)+~P1(x3361)+~P9(x3361,a2,x3363)+~P9(x3361,a2,x3362)+~P7(x3361,a1)+E(f9(x3361,x3362,x3363),x3362)+P3(f9(x3361,x3362,x3363),x3362,a2)+P1(f15(x3361,x3362,x3363)) % 3.72/3.75 [337]~P1(x3373)+~P1(x3372)+~P1(x3371)+~P9(x3371,a2,x3373)+~P10(x3371,a2,x3372)+~P7(x3371,a1)+E(f9(x3371,x3372,x3373),x3372)+P3(f9(x3371,x3372,x3373),x3372,a2)+P1(f15(x3371,x3372,x3373)) % 3.72/3.75 [338]~P1(x3383)+~P1(x3382)+~P1(x3381)+~P9(x3381,a2,x3382)+~P10(x3381,a2,x3383)+~P7(x3381,a1)+E(f9(x3381,x3382,x3383),x3382)+P3(f9(x3381,x3382,x3383),x3382,a2)+P1(f15(x3381,x3382,x3383)) % 3.72/3.75 [339]~P1(x3393)+~P1(x3392)+~P1(x3391)+~P10(x3391,a2,x3393)+~P10(x3391,a2,x3392)+~P7(x3391,a1)+E(f9(x3391,x3392,x3393),x3392)+P3(f9(x3391,x3392,x3393),x3392,a2)+P1(f15(x3391,x3392,x3393)) % 3.72/3.75 [348]~P1(x3483)+~P1(x3482)+~P1(x3481)+~P3(x3483,x3481,a2)+~P3(x3482,x3481,a2)+~P7(x3481,a1)+E(f9(x3481,x3482,x3483),x3483)+P3(f14(x3481,x3482,x3483),x3483,a2)+P3(f9(x3481,x3482,x3483),x3483,a2) % 3.72/3.75 [349]~P1(x3493)+~P1(x3492)+~P1(x3491)+~P3(x3493,x3491,a2)+~P3(x3492,x3491,a2)+~P7(x3491,a1)+E(f9(x3491,x3492,x3493),x3492)+P3(f15(x3491,x3492,x3493),x3492,a2)+P3(f9(x3491,x3492,x3493),x3492,a2) % 3.72/3.75 [350]~P1(x3503)+~P1(x3502)+~P1(x3501)+~P3(x3503,x3501,a2)+~P9(x3501,a2,x3502)+~P7(x3501,a1)+E(f9(x3501,x3502,x3503),x3503)+P3(f14(x3501,x3502,x3503),x3503,a2)+P3(f9(x3501,x3502,x3503),x3503,a2) % 3.72/3.75 [351]~P1(x3513)+~P1(x3512)+~P1(x3511)+~P3(x3513,x3511,a2)+~P10(x3511,a2,x3512)+~P7(x3511,a1)+E(f9(x3511,x3512,x3513),x3513)+P3(f14(x3511,x3512,x3513),x3513,a2)+P3(f9(x3511,x3512,x3513),x3513,a2) % 3.72/3.75 [352]~P1(x3523)+~P1(x3522)+~P1(x3521)+~P3(x3522,x3521,a2)+~P9(x3521,a2,x3523)+~P7(x3521,a1)+E(f9(x3521,x3522,x3523),x3523)+P3(f14(x3521,x3522,x3523),x3523,a2)+P3(f9(x3521,x3522,x3523),x3523,a2) % 3.72/3.75 [353]~P1(x3533)+~P1(x3532)+~P1(x3531)+~P3(x3532,x3531,a2)+~P10(x3531,a2,x3533)+~P7(x3531,a1)+E(f9(x3531,x3532,x3533),x3533)+P3(f14(x3531,x3532,x3533),x3533,a2)+P3(f9(x3531,x3532,x3533),x3533,a2) % 3.72/3.75 [354]~P1(x3543)+~P1(x3542)+~P1(x3541)+~P3(x3543,x3541,a2)+~P9(x3541,a2,x3542)+~P7(x3541,a1)+E(f9(x3541,x3542,x3543),x3542)+P3(f15(x3541,x3542,x3543),x3542,a2)+P3(f9(x3541,x3542,x3543),x3542,a2) % 3.72/3.75 [355]~P1(x3553)+~P1(x3552)+~P1(x3551)+~P3(x3553,x3551,a2)+~P10(x3551,a2,x3552)+~P7(x3551,a1)+E(f9(x3551,x3552,x3553),x3552)+P3(f15(x3551,x3552,x3553),x3552,a2)+P3(f9(x3551,x3552,x3553),x3552,a2) % 3.72/3.75 [356]~P1(x3563)+~P1(x3562)+~P1(x3561)+~P3(x3562,x3561,a2)+~P9(x3561,a2,x3563)+~P7(x3561,a1)+E(f9(x3561,x3562,x3563),x3562)+P3(f15(x3561,x3562,x3563),x3562,a2)+P3(f9(x3561,x3562,x3563),x3562,a2) % 3.72/3.75 [357]~P1(x3573)+~P1(x3572)+~P1(x3571)+~P3(x3572,x3571,a2)+~P10(x3571,a2,x3573)+~P7(x3571,a1)+E(f9(x3571,x3572,x3573),x3572)+P3(f15(x3571,x3572,x3573),x3572,a2)+P3(f9(x3571,x3572,x3573),x3572,a2) % 3.72/3.75 [358]~P1(x3583)+~P1(x3582)+~P1(x3581)+~P9(x3581,a2,x3583)+~P9(x3581,a2,x3582)+~P7(x3581,a1)+E(f9(x3581,x3582,x3583),x3583)+P3(f14(x3581,x3582,x3583),x3583,a2)+P3(f9(x3581,x3582,x3583),x3583,a2) % 3.72/3.75 [359]~P1(x3593)+~P1(x3592)+~P1(x3591)+~P9(x3591,a2,x3593)+~P10(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) % 3.72/3.75 [360]~P1(x3603)+~P1(x3602)+~P1(x3601)+~P9(x3601,a2,x3602)+~P10(x3601,a2,x3603)+~P7(x3601,a1)+E(f9(x3601,x3602,x3603),x3603)+P3(f14(x3601,x3602,x3603),x3603,a2)+P3(f9(x3601,x3602,x3603),x3603,a2) % 3.72/3.75 [361]~P1(x3613)+~P1(x3612)+~P1(x3611)+~P10(x3611,a2,x3613)+~P10(x3611,a2,x3612)+~P7(x3611,a1)+E(f9(x3611,x3612,x3613),x3613)+P3(f14(x3611,x3612,x3613),x3613,a2)+P3(f9(x3611,x3612,x3613),x3613,a2) % 3.72/3.75 [362]~P1(x3623)+~P1(x3622)+~P1(x3621)+~P9(x3621,a2,x3623)+~P9(x3621,a2,x3622)+~P7(x3621,a1)+E(f9(x3621,x3622,x3623),x3622)+P3(f15(x3621,x3622,x3623),x3622,a2)+P3(f9(x3621,x3622,x3623),x3622,a2) % 3.72/3.76 [363]~P1(x3633)+~P1(x3632)+~P1(x3631)+~P9(x3631,a2,x3633)+~P10(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) % 3.72/3.76 [364]~P1(x3643)+~P1(x3642)+~P1(x3641)+~P9(x3641,a2,x3642)+~P10(x3641,a2,x3643)+~P7(x3641,a1)+E(f9(x3641,x3642,x3643),x3642)+P3(f15(x3641,x3642,x3643),x3642,a2)+P3(f9(x3641,x3642,x3643),x3642,a2) % 3.72/3.76 [365]~P1(x3653)+~P1(x3652)+~P1(x3651)+~P10(x3651,a2,x3653)+~P10(x3651,a2,x3652)+~P7(x3651,a1)+E(f9(x3651,x3652,x3653),x3652)+P3(f15(x3651,x3652,x3653),x3652,a2)+P3(f9(x3651,x3652,x3653),x3652,a2) % 3.72/3.76 [372]~E(x3721,x3723)+~P1(x3723)+~P1(x3722)+~P1(x3721)+~P3(x3722,x3721,a2)+~P7(x3721,a1)+E(f9(x3721,x3722,x3723),x3723)+P9(f14(x3721,x3722,x3723),a2,f9(x3721,x3722,x3723))+P3(f9(x3721,x3722,x3723),x3723,a2) % 3.72/3.76 [373]~E(x3731,x3732)+~P1(x3733)+~P1(x3732)+~P1(x3731)+~P3(x3733,x3731,a2)+~P7(x3731,a1)+E(f9(x3731,x3732,x3733),x3733)+P9(f14(x3731,x3732,x3733),a2,f9(x3731,x3732,x3733))+P3(f9(x3731,x3732,x3733),x3733,a2) % 3.72/3.76 [374]~E(x3741,x3743)+~P1(x3743)+~P1(x3742)+~P1(x3741)+~P3(x3742,x3741,a2)+~P7(x3741,a1)+E(f9(x3741,x3742,x3743),x3742)+P9(f15(x3741,x3742,x3743),a2,f9(x3741,x3742,x3743))+P3(f9(x3741,x3742,x3743),x3742,a2) % 3.72/3.76 [375]~E(x3751,x3752)+~P1(x3753)+~P1(x3752)+~P1(x3751)+~P3(x3753,x3751,a2)+~P7(x3751,a1)+E(f9(x3751,x3752,x3753),x3752)+P9(f15(x3751,x3752,x3753),a2,f9(x3751,x3752,x3753))+P3(f9(x3751,x3752,x3753),x3752,a2) % 3.72/3.76 [376]~E(x3761,x3763)+~P1(x3763)+~P1(x3762)+~P1(x3761)+~P9(x3761,a2,x3762)+~P7(x3761,a1)+E(f9(x3761,x3762,x3763),x3763)+P9(f14(x3761,x3762,x3763),a2,f9(x3761,x3762,x3763))+P3(f9(x3761,x3762,x3763),x3763,a2) % 3.72/3.76 [377]~E(x3771,x3773)+~P1(x3773)+~P1(x3772)+~P1(x3771)+~P10(x3771,a2,x3772)+~P7(x3771,a1)+E(f9(x3771,x3772,x3773),x3773)+P9(f14(x3771,x3772,x3773),a2,f9(x3771,x3772,x3773))+P3(f9(x3771,x3772,x3773),x3773,a2) % 3.72/3.76 [378]~E(x3781,x3782)+~P1(x3783)+~P1(x3782)+~P1(x3781)+~P9(x3781,a2,x3783)+~P7(x3781,a1)+E(f9(x3781,x3782,x3783),x3783)+P9(f14(x3781,x3782,x3783),a2,f9(x3781,x3782,x3783))+P3(f9(x3781,x3782,x3783),x3783,a2) % 3.72/3.76 [379]~E(x3791,x3792)+~P1(x3793)+~P1(x3792)+~P1(x3791)+~P10(x3791,a2,x3793)+~P7(x3791,a1)+E(f9(x3791,x3792,x3793),x3793)+P9(f14(x3791,x3792,x3793),a2,f9(x3791,x3792,x3793))+P3(f9(x3791,x3792,x3793),x3793,a2) % 3.72/3.76 [380]~E(x3801,x3803)+~P1(x3803)+~P1(x3802)+~P1(x3801)+~P9(x3801,a2,x3802)+~P7(x3801,a1)+E(f9(x3801,x3802,x3803),x3802)+P9(f15(x3801,x3802,x3803),a2,f9(x3801,x3802,x3803))+P3(f9(x3801,x3802,x3803),x3802,a2) % 3.72/3.76 [381]~E(x3811,x3813)+~P1(x3813)+~P1(x3812)+~P1(x3811)+~P10(x3811,a2,x3812)+~P7(x3811,a1)+E(f9(x3811,x3812,x3813),x3812)+P9(f15(x3811,x3812,x3813),a2,f9(x3811,x3812,x3813))+P3(f9(x3811,x3812,x3813),x3812,a2) % 3.72/3.76 [382]~E(x3821,x3822)+~P1(x3823)+~P1(x3822)+~P1(x3821)+~P9(x3821,a2,x3823)+~P7(x3821,a1)+E(f9(x3821,x3822,x3823),x3822)+P9(f15(x3821,x3822,x3823),a2,f9(x3821,x3822,x3823))+P3(f9(x3821,x3822,x3823),x3822,a2) % 3.72/3.76 [383]~E(x3831,x3832)+~P1(x3833)+~P1(x3832)+~P1(x3831)+~P10(x3831,a2,x3833)+~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) % 3.72/3.76 [410]~P1(x4103)+~P1(x4102)+~P1(x4101)+~P3(x4103,x4101,a2)+~P3(x4102,x4101,a2)+~P7(x4101,a1)+E(f9(x4101,x4102,x4103),x4103)+P9(f14(x4101,x4102,x4103),a2,f9(x4101,x4102,x4103))+P3(f9(x4101,x4102,x4103),x4103,a2) % 3.72/3.76 [411]~P1(x4113)+~P1(x4112)+~P1(x4111)+~P3(x4113,x4111,a2)+~P3(x4112,x4111,a2)+~P7(x4111,a1)+E(f9(x4111,x4112,x4113),x4112)+P9(f15(x4111,x4112,x4113),a2,f9(x4111,x4112,x4113))+P3(f9(x4111,x4112,x4113),x4112,a2) % 3.72/3.76 [412]~P1(x4123)+~P1(x4122)+~P1(x4121)+~P3(x4123,x4121,a2)+~P9(x4121,a2,x4122)+~P7(x4121,a1)+E(f9(x4121,x4122,x4123),x4123)+P9(f14(x4121,x4122,x4123),a2,f9(x4121,x4122,x4123))+P3(f9(x4121,x4122,x4123),x4123,a2) % 3.72/3.76 [413]~P1(x4133)+~P1(x4132)+~P1(x4131)+~P3(x4133,x4131,a2)+~P10(x4131,a2,x4132)+~P7(x4131,a1)+E(f9(x4131,x4132,x4133),x4133)+P9(f14(x4131,x4132,x4133),a2,f9(x4131,x4132,x4133))+P3(f9(x4131,x4132,x4133),x4133,a2) % 3.72/3.76 [414]~P1(x4143)+~P1(x4142)+~P1(x4141)+~P3(x4142,x4141,a2)+~P9(x4141,a2,x4143)+~P7(x4141,a1)+E(f9(x4141,x4142,x4143),x4143)+P9(f14(x4141,x4142,x4143),a2,f9(x4141,x4142,x4143))+P3(f9(x4141,x4142,x4143),x4143,a2) % 3.72/3.76 [415]~P1(x4153)+~P1(x4152)+~P1(x4151)+~P3(x4152,x4151,a2)+~P10(x4151,a2,x4153)+~P7(x4151,a1)+E(f9(x4151,x4152,x4153),x4153)+P9(f14(x4151,x4152,x4153),a2,f9(x4151,x4152,x4153))+P3(f9(x4151,x4152,x4153),x4153,a2) % 3.72/3.76 [416]~P1(x4163)+~P1(x4162)+~P1(x4161)+~P3(x4163,x4161,a2)+~P9(x4161,a2,x4162)+~P7(x4161,a1)+E(f9(x4161,x4162,x4163),x4162)+P9(f15(x4161,x4162,x4163),a2,f9(x4161,x4162,x4163))+P3(f9(x4161,x4162,x4163),x4162,a2) % 3.72/3.76 [417]~P1(x4173)+~P1(x4172)+~P1(x4171)+~P3(x4173,x4171,a2)+~P10(x4171,a2,x4172)+~P7(x4171,a1)+E(f9(x4171,x4172,x4173),x4172)+P9(f15(x4171,x4172,x4173),a2,f9(x4171,x4172,x4173))+P3(f9(x4171,x4172,x4173),x4172,a2) % 3.72/3.76 [418]~P1(x4183)+~P1(x4182)+~P1(x4181)+~P3(x4182,x4181,a2)+~P9(x4181,a2,x4183)+~P7(x4181,a1)+E(f9(x4181,x4182,x4183),x4182)+P9(f15(x4181,x4182,x4183),a2,f9(x4181,x4182,x4183))+P3(f9(x4181,x4182,x4183),x4182,a2) % 3.72/3.76 [419]~P1(x4193)+~P1(x4192)+~P1(x4191)+~P3(x4192,x4191,a2)+~P10(x4191,a2,x4193)+~P7(x4191,a1)+E(f9(x4191,x4192,x4193),x4192)+P9(f15(x4191,x4192,x4193),a2,f9(x4191,x4192,x4193))+P3(f9(x4191,x4192,x4193),x4192,a2) % 3.72/3.76 [420]~P1(x4203)+~P1(x4202)+~P1(x4201)+~P9(x4201,a2,x4203)+~P9(x4201,a2,x4202)+~P7(x4201,a1)+E(f9(x4201,x4202,x4203),x4203)+P9(f14(x4201,x4202,x4203),a2,f9(x4201,x4202,x4203))+P3(f9(x4201,x4202,x4203),x4203,a2) % 3.72/3.76 [421]~P1(x4213)+~P1(x4212)+~P1(x4211)+~P9(x4211,a2,x4213)+~P10(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) % 3.72/3.76 [422]~P1(x4223)+~P1(x4222)+~P1(x4221)+~P9(x4221,a2,x4222)+~P10(x4221,a2,x4223)+~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) % 3.72/3.76 [423]~P1(x4233)+~P1(x4232)+~P1(x4231)+~P10(x4231,a2,x4233)+~P10(x4231,a2,x4232)+~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) % 3.72/3.76 [424]~P1(x4243)+~P1(x4242)+~P1(x4241)+~P9(x4241,a2,x4243)+~P9(x4241,a2,x4242)+~P7(x4241,a1)+E(f9(x4241,x4242,x4243),x4242)+P9(f15(x4241,x4242,x4243),a2,f9(x4241,x4242,x4243))+P3(f9(x4241,x4242,x4243),x4242,a2) % 3.72/3.76 [425]~P1(x4253)+~P1(x4252)+~P1(x4251)+~P9(x4251,a2,x4253)+~P10(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) % 3.72/3.76 [426]~P1(x4263)+~P1(x4262)+~P1(x4261)+~P9(x4261,a2,x4262)+~P10(x4261,a2,x4263)+~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) % 3.72/3.76 [427]~P1(x4273)+~P1(x4272)+~P1(x4271)+~P10(x4271,a2,x4273)+~P10(x4271,a2,x4272)+~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) % 3.72/3.76 [197]~E(x1971,x1973)+~P1(x1973)+~P1(x1972)+~P1(x1971)+~P1(x1974)+~P3(x1974,x1971,a2)+~P9(x1974,a2,x1972)+~P7(x1971,a1)+P1(f9(x1971,x1972,x1973)) % 3.72/3.76 [198]~E(x1981,x1982)+~P1(x1983)+~P1(x1982)+~P1(x1981)+~P1(x1984)+~P3(x1984,x1981,a2)+~P9(x1984,a2,x1983)+~P7(x1981,a1)+P1(f9(x1981,x1982,x1983)) % 3.72/3.76 [233]~E(x2332,x2333)+~P1(x2333)+~P1(x2332)+~P1(x2331)+~P1(x2334)+~P3(x2334,x2332,a2)+~P9(x2334,a2,x2331)+~P7(x2332,a1)+P10(x2331,a2,f9(x2332,x2333,x2331)) % 3.72/3.76 [234]~E(x2341,x2342)+~P1(x2343)+~P1(x2342)+~P1(x2341)+~P1(x2344)+~P3(x2344,x2342,a2)+~P9(x2344,a2,x2343)+~P7(x2342,a1)+P10(x2341,a2,f9(x2342,x2343,x2341)) % 3.72/3.76 [235]~E(x2352,x2353)+~P1(x2353)+~P1(x2352)+~P1(x2351)+~P1(x2354)+~P3(x2354,x2352,a2)+~P9(x2354,a2,x2351)+~P7(x2352,a1)+P10(x2351,a2,f9(x2352,x2351,x2353)) % 3.72/3.76 [236]~E(x2361,x2362)+~P1(x2363)+~P1(x2362)+~P1(x2361)+~P1(x2364)+~P3(x2364,x2362,a2)+~P9(x2364,a2,x2363)+~P7(x2362,a1)+P10(x2361,a2,f9(x2362,x2361,x2363)) % 3.72/3.76 [239]~P1(x2393)+~P1(x2392)+~P1(x2391)+~P1(x2394)+~P3(x2394,x2391,a2)+~P3(x2393,x2391,a2)+~P9(x2394,a2,x2392)+~P7(x2391,a1)+P1(f9(x2391,x2392,x2393)) % 3.72/3.76 [240]~P1(x2403)+~P1(x2402)+~P1(x2401)+~P1(x2404)+~P3(x2404,x2401,a2)+~P3(x2402,x2401,a2)+~P9(x2404,a2,x2403)+~P7(x2401,a1)+P1(f9(x2401,x2402,x2403)) % 3.72/3.76 [241]~P1(x2413)+~P1(x2412)+~P1(x2411)+~P1(x2414)+~P3(x2414,x2411,a2)+~P9(x2414,a2,x2413)+~P9(x2411,a2,x2412)+~P7(x2411,a1)+P1(f9(x2411,x2412,x2413)) % 3.72/3.76 [242]~P1(x2423)+~P1(x2422)+~P1(x2421)+~P1(x2424)+~P3(x2424,x2421,a2)+~P9(x2424,a2,x2423)+~P10(x2421,a2,x2422)+~P7(x2421,a1)+P1(f9(x2421,x2422,x2423)) % 3.72/3.76 [243]~P1(x2433)+~P1(x2432)+~P1(x2431)+~P1(x2434)+~P3(x2434,x2431,a2)+~P9(x2434,a2,x2432)+~P9(x2431,a2,x2433)+~P7(x2431,a1)+P1(f9(x2431,x2432,x2433)) % 3.72/3.76 [244]~P1(x2443)+~P1(x2442)+~P1(x2441)+~P1(x2444)+~P3(x2444,x2441,a2)+~P9(x2444,a2,x2442)+~P10(x2441,a2,x2443)+~P7(x2441,a1)+P1(f9(x2441,x2442,x2443)) % 3.72/3.76 [281]~P1(x2813)+~P1(x2812)+~P1(x2811)+~P1(x2814)+~P3(x2814,x2812,a2)+~P3(x2813,x2812,a2)+~P9(x2814,a2,x2811)+~P7(x2812,a1)+P10(x2811,a2,f9(x2812,x2813,x2811)) % 3.72/3.76 [282]~P1(x2823)+~P1(x2822)+~P1(x2821)+~P1(x2824)+~P3(x2824,x2822,a2)+~P3(x2821,x2822,a2)+~P9(x2824,a2,x2823)+~P7(x2822,a1)+P10(x2821,a2,f9(x2822,x2823,x2821)) % 3.72/3.76 [283]~P1(x2833)+~P1(x2832)+~P1(x2831)+~P1(x2834)+~P3(x2834,x2832,a2)+~P3(x2833,x2832,a2)+~P9(x2834,a2,x2831)+~P7(x2832,a1)+P10(x2831,a2,f9(x2832,x2831,x2833)) % 3.72/3.76 [284]~P1(x2843)+~P1(x2842)+~P1(x2841)+~P1(x2844)+~P3(x2844,x2842,a2)+~P3(x2841,x2842,a2)+~P9(x2844,a2,x2843)+~P7(x2842,a1)+P10(x2841,a2,f9(x2842,x2841,x2843)) % 3.72/3.76 [285]~P1(x2853)+~P1(x2852)+~P1(x2851)+~P1(x2854)+~P3(x2854,x2852,a2)+~P9(x2854,a2,x2853)+~P9(x2852,a2,x2851)+~P7(x2852,a1)+P10(x2851,a2,f9(x2852,x2853,x2851)) % 3.72/3.76 [286]~P1(x2863)+~P1(x2862)+~P1(x2861)+~P1(x2864)+~P3(x2864,x2862,a2)+~P9(x2864,a2,x2863)+~P10(x2862,a2,x2861)+~P7(x2862,a1)+P10(x2861,a2,f9(x2862,x2863,x2861)) % 3.72/3.76 [287]~P1(x2873)+~P1(x2872)+~P1(x2871)+~P1(x2874)+~P3(x2874,x2872,a2)+~P9(x2874,a2,x2871)+~P9(x2872,a2,x2873)+~P7(x2872,a1)+P10(x2871,a2,f9(x2872,x2873,x2871)) % 3.72/3.76 [288]~P1(x2883)+~P1(x2882)+~P1(x2881)+~P1(x2884)+~P3(x2884,x2882,a2)+~P9(x2884,a2,x2881)+~P10(x2882,a2,x2883)+~P7(x2882,a1)+P10(x2881,a2,f9(x2882,x2883,x2881)) % 3.72/3.76 [289]~P1(x2893)+~P1(x2892)+~P1(x2891)+~P1(x2894)+~P3(x2894,x2892,a2)+~P9(x2894,a2,x2893)+~P9(x2892,a2,x2891)+~P7(x2892,a1)+P10(x2891,a2,f9(x2892,x2891,x2893)) % 3.72/3.76 [290]~P1(x2903)+~P1(x2902)+~P1(x2901)+~P1(x2904)+~P3(x2904,x2902,a2)+~P9(x2904,a2,x2903)+~P10(x2902,a2,x2901)+~P7(x2902,a1)+P10(x2901,a2,f9(x2902,x2901,x2903)) % 3.72/3.76 [291]~P1(x2913)+~P1(x2912)+~P1(x2911)+~P1(x2914)+~P3(x2914,x2912,a2)+~P9(x2914,a2,x2911)+~P9(x2912,a2,x2913)+~P7(x2912,a1)+P10(x2911,a2,f9(x2912,x2911,x2913)) % 3.72/3.76 [292]~P1(x2923)+~P1(x2922)+~P1(x2921)+~P1(x2924)+~P3(x2924,x2922,a2)+~P9(x2924,a2,x2921)+~P10(x2922,a2,x2923)+~P7(x2922,a1)+P10(x2921,a2,f9(x2922,x2921,x2923)) % 3.72/3.76 [265]~E(x2651,x2652)+~P1(x2652)+~P1(x2651)+~P1(x2653)+~P1(x2654)+~P3(x2654,x2651,a2)+~P9(x2654,a2,x2653)+~P7(x2651,a1)+E(f9(x2651,x2652,x2653),x2653)+P9(x2653,a2,f9(x2651,x2652,x2653)) % 3.72/3.76 [266]~E(x2663,x2661)+~P1(x2662)+~P1(x2661)+~P1(x2663)+~P1(x2664)+~P3(x2664,x2661,a2)+~P9(x2664,a2,x2662)+~P7(x2661,a1)+E(f9(x2661,x2662,x2663),x2663)+P9(x2663,a2,f9(x2661,x2662,x2663)) % 3.72/3.76 [267]~E(x2671,x2673)+~P1(x2673)+~P1(x2671)+~P1(x2672)+~P1(x2674)+~P3(x2674,x2671,a2)+~P9(x2674,a2,x2672)+~P7(x2671,a1)+E(f9(x2671,x2672,x2673),x2672)+P9(x2672,a2,f9(x2671,x2672,x2673)) % 3.72/3.76 [268]~E(x2682,x2681)+~P1(x2683)+~P1(x2681)+~P1(x2682)+~P1(x2684)+~P3(x2684,x2681,a2)+~P9(x2684,a2,x2683)+~P7(x2681,a1)+E(f9(x2681,x2682,x2683),x2682)+P9(x2682,a2,f9(x2681,x2682,x2683)) % 3.72/3.76 [308]~P1(x3082)+~P1(x3081)+~P1(x3083)+~P1(x3084)+~P3(x3084,x3081,a2)+~P3(x3082,x3081,a2)+~P9(x3084,a2,x3083)+~P7(x3081,a1)+E(f9(x3081,x3082,x3083),x3083)+P9(x3083,a2,f9(x3081,x3082,x3083)) % 3.72/3.76 [309]~P1(x3092)+~P1(x3091)+~P1(x3093)+~P1(x3094)+~P3(x3094,x3091,a2)+~P3(x3093,x3091,a2)+~P9(x3094,a2,x3092)+~P7(x3091,a1)+E(f9(x3091,x3092,x3093),x3093)+P9(x3093,a2,f9(x3091,x3092,x3093)) % 3.72/3.76 [310]~P1(x3103)+~P1(x3101)+~P1(x3102)+~P1(x3104)+~P3(x3104,x3101,a2)+~P3(x3103,x3101,a2)+~P9(x3104,a2,x3102)+~P7(x3101,a1)+E(f9(x3101,x3102,x3103),x3102)+P9(x3102,a2,f9(x3101,x3102,x3103)) % 3.72/3.76 [311]~P1(x3113)+~P1(x3111)+~P1(x3112)+~P1(x3114)+~P3(x3114,x3111,a2)+~P3(x3112,x3111,a2)+~P9(x3114,a2,x3113)+~P7(x3111,a1)+E(f9(x3111,x3112,x3113),x3112)+P9(x3112,a2,f9(x3111,x3112,x3113)) % 3.72/3.76 [312]~P1(x3122)+~P1(x3121)+~P1(x3123)+~P1(x3124)+~P3(x3124,x3121,a2)+~P9(x3124,a2,x3122)+~P9(x3121,a2,x3123)+~P7(x3121,a1)+E(f9(x3121,x3122,x3123),x3123)+P9(x3123,a2,f9(x3121,x3122,x3123)) % 3.72/3.76 [313]~P1(x3132)+~P1(x3131)+~P1(x3133)+~P1(x3134)+~P3(x3134,x3131,a2)+~P9(x3134,a2,x3132)+~P10(x3131,a2,x3133)+~P7(x3131,a1)+E(f9(x3131,x3132,x3133),x3133)+P9(x3133,a2,f9(x3131,x3132,x3133)) % 3.72/3.76 [314]~P1(x3142)+~P1(x3141)+~P1(x3143)+~P1(x3144)+~P3(x3144,x3141,a2)+~P9(x3144,a2,x3143)+~P9(x3141,a2,x3142)+~P7(x3141,a1)+E(f9(x3141,x3142,x3143),x3143)+P9(x3143,a2,f9(x3141,x3142,x3143)) % 3.72/3.76 [315]~P1(x3152)+~P1(x3151)+~P1(x3153)+~P1(x3154)+~P3(x3154,x3151,a2)+~P9(x3154,a2,x3153)+~P10(x3151,a2,x3152)+~P7(x3151,a1)+E(f9(x3151,x3152,x3153),x3153)+P9(x3153,a2,f9(x3151,x3152,x3153)) % 3.72/3.76 [316]~P1(x3163)+~P1(x3161)+~P1(x3162)+~P1(x3164)+~P3(x3164,x3161,a2)+~P9(x3164,a2,x3163)+~P9(x3161,a2,x3162)+~P7(x3161,a1)+E(f9(x3161,x3162,x3163),x3162)+P9(x3162,a2,f9(x3161,x3162,x3163)) % 3.72/3.76 [317]~P1(x3173)+~P1(x3171)+~P1(x3172)+~P1(x3174)+~P3(x3174,x3171,a2)+~P9(x3174,a2,x3173)+~P10(x3171,a2,x3172)+~P7(x3171,a1)+E(f9(x3171,x3172,x3173),x3172)+P9(x3172,a2,f9(x3171,x3172,x3173)) % 3.72/3.76 [318]~P1(x3183)+~P1(x3181)+~P1(x3182)+~P1(x3184)+~P3(x3184,x3181,a2)+~P9(x3184,a2,x3182)+~P9(x3181,a2,x3183)+~P7(x3181,a1)+E(f9(x3181,x3182,x3183),x3182)+P9(x3182,a2,f9(x3181,x3182,x3183)) % 3.72/3.76 [319]~P1(x3193)+~P1(x3191)+~P1(x3192)+~P1(x3194)+~P3(x3194,x3191,a2)+~P9(x3194,a2,x3192)+~P10(x3191,a2,x3193)+~P7(x3191,a1)+E(f9(x3191,x3192,x3193),x3192)+P9(x3192,a2,f9(x3191,x3192,x3193)) % 3.72/3.76 [340]~E(x3401,x3403)+~P1(x3403)+~P1(x3402)+~P1(x3401)+~P1(x3404)+~P3(x3404,x3401,a2)+~P9(x3404,a2,x3402)+~P7(x3401,a1)+E(f9(x3401,x3402,x3403),x3403)+P3(f9(x3401,x3402,x3403),x3403,a2)+P1(f14(x3401,x3402,x3403)) % 3.72/3.76 [341]~E(x3411,x3412)+~P1(x3413)+~P1(x3412)+~P1(x3411)+~P1(x3414)+~P3(x3414,x3411,a2)+~P9(x3414,a2,x3413)+~P7(x3411,a1)+E(f9(x3411,x3412,x3413),x3413)+P3(f9(x3411,x3412,x3413),x3413,a2)+P1(f14(x3411,x3412,x3413)) % 3.72/3.76 [342]~E(x3421,x3423)+~P1(x3423)+~P1(x3422)+~P1(x3421)+~P1(x3424)+~P3(x3424,x3421,a2)+~P9(x3424,a2,x3422)+~P7(x3421,a1)+E(f9(x3421,x3422,x3423),x3422)+P3(f9(x3421,x3422,x3423),x3422,a2)+P1(f15(x3421,x3422,x3423)) % 3.72/3.76 [343]~E(x3431,x3432)+~P1(x3433)+~P1(x3432)+~P1(x3431)+~P1(x3434)+~P3(x3434,x3431,a2)+~P9(x3434,a2,x3433)+~P7(x3431,a1)+E(f9(x3431,x3432,x3433),x3432)+P3(f9(x3431,x3432,x3433),x3432,a2)+P1(f15(x3431,x3432,x3433)) % 3.72/3.76 [366]~E(x3661,x3663)+~P1(x3663)+~P1(x3662)+~P1(x3661)+~P1(x3664)+~P3(x3664,x3661,a2)+~P9(x3664,a2,x3662)+~P7(x3661,a1)+E(f9(x3661,x3662,x3663),x3663)+P3(f14(x3661,x3662,x3663),x3663,a2)+P3(f9(x3661,x3662,x3663),x3663,a2) % 3.72/3.76 [367]~E(x3671,x3672)+~P1(x3673)+~P1(x3672)+~P1(x3671)+~P1(x3674)+~P3(x3674,x3671,a2)+~P9(x3674,a2,x3673)+~P7(x3671,a1)+E(f9(x3671,x3672,x3673),x3673)+P3(f14(x3671,x3672,x3673),x3673,a2)+P3(f9(x3671,x3672,x3673),x3673,a2) % 3.72/3.76 [368]~E(x3681,x3683)+~P1(x3683)+~P1(x3682)+~P1(x3681)+~P1(x3684)+~P3(x3684,x3681,a2)+~P9(x3684,a2,x3682)+~P7(x3681,a1)+E(f9(x3681,x3682,x3683),x3682)+P3(f15(x3681,x3682,x3683),x3682,a2)+P3(f9(x3681,x3682,x3683),x3682,a2) % 3.72/3.76 [369]~E(x3691,x3692)+~P1(x3693)+~P1(x3692)+~P1(x3691)+~P1(x3694)+~P3(x3694,x3691,a2)+~P9(x3694,a2,x3693)+~P7(x3691,a1)+E(f9(x3691,x3692,x3693),x3692)+P3(f15(x3691,x3692,x3693),x3692,a2)+P3(f9(x3691,x3692,x3693),x3692,a2) % 3.72/3.76 [384]~P1(x3843)+~P1(x3842)+~P1(x3841)+~P1(x3844)+~P3(x3844,x3841,a2)+~P3(x3843,x3841,a2)+~P9(x3844,a2,x3842)+~P7(x3841,a1)+E(f9(x3841,x3842,x3843),x3843)+P3(f9(x3841,x3842,x3843),x3843,a2)+P1(f14(x3841,x3842,x3843)) % 3.72/3.76 [385]~P1(x3853)+~P1(x3852)+~P1(x3851)+~P1(x3854)+~P3(x3854,x3851,a2)+~P3(x3852,x3851,a2)+~P9(x3854,a2,x3853)+~P7(x3851,a1)+E(f9(x3851,x3852,x3853),x3853)+P3(f9(x3851,x3852,x3853),x3853,a2)+P1(f14(x3851,x3852,x3853)) % 3.72/3.76 [386]~P1(x3863)+~P1(x3862)+~P1(x3861)+~P1(x3864)+~P3(x3864,x3861,a2)+~P3(x3863,x3861,a2)+~P9(x3864,a2,x3862)+~P7(x3861,a1)+E(f9(x3861,x3862,x3863),x3862)+P3(f9(x3861,x3862,x3863),x3862,a2)+P1(f15(x3861,x3862,x3863)) % 3.72/3.76 [387]~P1(x3873)+~P1(x3872)+~P1(x3871)+~P1(x3874)+~P3(x3874,x3871,a2)+~P3(x3872,x3871,a2)+~P9(x3874,a2,x3873)+~P7(x3871,a1)+E(f9(x3871,x3872,x3873),x3872)+P3(f9(x3871,x3872,x3873),x3872,a2)+P1(f15(x3871,x3872,x3873)) % 3.72/3.76 [388]~P1(x3883)+~P1(x3882)+~P1(x3881)+~P1(x3884)+~P3(x3884,x3881,a2)+~P9(x3884,a2,x3883)+~P9(x3881,a2,x3882)+~P7(x3881,a1)+E(f9(x3881,x3882,x3883),x3883)+P3(f9(x3881,x3882,x3883),x3883,a2)+P1(f14(x3881,x3882,x3883)) % 3.72/3.76 [389]~P1(x3893)+~P1(x3892)+~P1(x3891)+~P1(x3894)+~P3(x3894,x3891,a2)+~P9(x3894,a2,x3893)+~P10(x3891,a2,x3892)+~P7(x3891,a1)+E(f9(x3891,x3892,x3893),x3893)+P3(f9(x3891,x3892,x3893),x3893,a2)+P1(f14(x3891,x3892,x3893)) % 3.72/3.76 [390]~P1(x3903)+~P1(x3902)+~P1(x3901)+~P1(x3904)+~P3(x3904,x3901,a2)+~P9(x3904,a2,x3902)+~P9(x3901,a2,x3903)+~P7(x3901,a1)+E(f9(x3901,x3902,x3903),x3903)+P3(f9(x3901,x3902,x3903),x3903,a2)+P1(f14(x3901,x3902,x3903)) % 3.72/3.76 [391]~P1(x3913)+~P1(x3912)+~P1(x3911)+~P1(x3914)+~P3(x3914,x3911,a2)+~P9(x3914,a2,x3912)+~P10(x3911,a2,x3913)+~P7(x3911,a1)+E(f9(x3911,x3912,x3913),x3913)+P3(f9(x3911,x3912,x3913),x3913,a2)+P1(f14(x3911,x3912,x3913)) % 3.72/3.76 [392]~P1(x3923)+~P1(x3922)+~P1(x3921)+~P1(x3924)+~P3(x3924,x3921,a2)+~P9(x3924,a2,x3923)+~P9(x3921,a2,x3922)+~P7(x3921,a1)+E(f9(x3921,x3922,x3923),x3922)+P3(f9(x3921,x3922,x3923),x3922,a2)+P1(f15(x3921,x3922,x3923)) % 3.72/3.76 [393]~P1(x3933)+~P1(x3932)+~P1(x3931)+~P1(x3934)+~P3(x3934,x3931,a2)+~P9(x3934,a2,x3933)+~P10(x3931,a2,x3932)+~P7(x3931,a1)+E(f9(x3931,x3932,x3933),x3932)+P3(f9(x3931,x3932,x3933),x3932,a2)+P1(f15(x3931,x3932,x3933)) % 3.72/3.76 [394]~P1(x3943)+~P1(x3942)+~P1(x3941)+~P1(x3944)+~P3(x3944,x3941,a2)+~P9(x3944,a2,x3942)+~P9(x3941,a2,x3943)+~P7(x3941,a1)+E(f9(x3941,x3942,x3943),x3942)+P3(f9(x3941,x3942,x3943),x3942,a2)+P1(f15(x3941,x3942,x3943)) % 3.72/3.76 [395]~P1(x3953)+~P1(x3952)+~P1(x3951)+~P1(x3954)+~P3(x3954,x3951,a2)+~P9(x3954,a2,x3952)+~P10(x3951,a2,x3953)+~P7(x3951,a1)+E(f9(x3951,x3952,x3953),x3952)+P3(f9(x3951,x3952,x3953),x3952,a2)+P1(f15(x3951,x3952,x3953)) % 3.72/3.76 [398]~P1(x3983)+~P1(x3982)+~P1(x3981)+~P1(x3984)+~P3(x3984,x3981,a2)+~P3(x3983,x3981,a2)+~P9(x3984,a2,x3982)+~P7(x3981,a1)+E(f9(x3981,x3982,x3983),x3983)+P3(f14(x3981,x3982,x3983),x3983,a2)+P3(f9(x3981,x3982,x3983),x3983,a2) % 3.72/3.76 [399]~P1(x3993)+~P1(x3992)+~P1(x3991)+~P1(x3994)+~P3(x3994,x3991,a2)+~P3(x3992,x3991,a2)+~P9(x3994,a2,x3993)+~P7(x3991,a1)+E(f9(x3991,x3992,x3993),x3993)+P3(f14(x3991,x3992,x3993),x3993,a2)+P3(f9(x3991,x3992,x3993),x3993,a2) % 3.72/3.76 [400]~P1(x4003)+~P1(x4002)+~P1(x4001)+~P1(x4004)+~P3(x4004,x4001,a2)+~P3(x4003,x4001,a2)+~P9(x4004,a2,x4002)+~P7(x4001,a1)+E(f9(x4001,x4002,x4003),x4002)+P3(f15(x4001,x4002,x4003),x4002,a2)+P3(f9(x4001,x4002,x4003),x4002,a2) % 3.72/3.76 [401]~P1(x4013)+~P1(x4012)+~P1(x4011)+~P1(x4014)+~P3(x4014,x4011,a2)+~P3(x4012,x4011,a2)+~P9(x4014,a2,x4013)+~P7(x4011,a1)+E(f9(x4011,x4012,x4013),x4012)+P3(f15(x4011,x4012,x4013),x4012,a2)+P3(f9(x4011,x4012,x4013),x4012,a2) % 3.72/3.76 [402]~P1(x4023)+~P1(x4022)+~P1(x4021)+~P1(x4024)+~P3(x4024,x4021,a2)+~P9(x4024,a2,x4023)+~P9(x4021,a2,x4022)+~P7(x4021,a1)+E(f9(x4021,x4022,x4023),x4023)+P3(f14(x4021,x4022,x4023),x4023,a2)+P3(f9(x4021,x4022,x4023),x4023,a2) % 3.72/3.76 [403]~P1(x4033)+~P1(x4032)+~P1(x4031)+~P1(x4034)+~P3(x4034,x4031,a2)+~P9(x4034,a2,x4033)+~P10(x4031,a2,x4032)+~P7(x4031,a1)+E(f9(x4031,x4032,x4033),x4033)+P3(f14(x4031,x4032,x4033),x4033,a2)+P3(f9(x4031,x4032,x4033),x4033,a2) % 3.72/3.76 [404]~P1(x4043)+~P1(x4042)+~P1(x4041)+~P1(x4044)+~P3(x4044,x4041,a2)+~P9(x4044,a2,x4042)+~P9(x4041,a2,x4043)+~P7(x4041,a1)+E(f9(x4041,x4042,x4043),x4043)+P3(f14(x4041,x4042,x4043),x4043,a2)+P3(f9(x4041,x4042,x4043),x4043,a2) % 3.72/3.76 [405]~P1(x4053)+~P1(x4052)+~P1(x4051)+~P1(x4054)+~P3(x4054,x4051,a2)+~P9(x4054,a2,x4052)+~P10(x4051,a2,x4053)+~P7(x4051,a1)+E(f9(x4051,x4052,x4053),x4053)+P3(f14(x4051,x4052,x4053),x4053,a2)+P3(f9(x4051,x4052,x4053),x4053,a2) % 3.72/3.76 [406]~P1(x4063)+~P1(x4062)+~P1(x4061)+~P1(x4064)+~P3(x4064,x4061,a2)+~P9(x4064,a2,x4063)+~P9(x4061,a2,x4062)+~P7(x4061,a1)+E(f9(x4061,x4062,x4063),x4062)+P3(f15(x4061,x4062,x4063),x4062,a2)+P3(f9(x4061,x4062,x4063),x4062,a2) % 3.72/3.76 [407]~P1(x4073)+~P1(x4072)+~P1(x4071)+~P1(x4074)+~P3(x4074,x4071,a2)+~P9(x4074,a2,x4073)+~P10(x4071,a2,x4072)+~P7(x4071,a1)+E(f9(x4071,x4072,x4073),x4072)+P3(f15(x4071,x4072,x4073),x4072,a2)+P3(f9(x4071,x4072,x4073),x4072,a2) % 3.72/3.76 [408]~P1(x4083)+~P1(x4082)+~P1(x4081)+~P1(x4084)+~P3(x4084,x4081,a2)+~P9(x4084,a2,x4082)+~P9(x4081,a2,x4083)+~P7(x4081,a1)+E(f9(x4081,x4082,x4083),x4082)+P3(f15(x4081,x4082,x4083),x4082,a2)+P3(f9(x4081,x4082,x4083),x4082,a2) % 3.72/3.76 [409]~P1(x4093)+~P1(x4092)+~P1(x4091)+~P1(x4094)+~P3(x4094,x4091,a2)+~P9(x4094,a2,x4092)+~P10(x4091,a2,x4093)+~P7(x4091,a1)+E(f9(x4091,x4092,x4093),x4092)+P3(f15(x4091,x4092,x4093),x4092,a2)+P3(f9(x4091,x4092,x4093),x4092,a2) % 3.72/3.76 [428]~E(x4281,x4283)+~P1(x4283)+~P1(x4282)+~P1(x4281)+~P1(x4284)+~P3(x4284,x4281,a2)+~P9(x4284,a2,x4282)+~P7(x4281,a1)+E(f9(x4281,x4282,x4283),x4283)+P9(f14(x4281,x4282,x4283),a2,f9(x4281,x4282,x4283))+P3(f9(x4281,x4282,x4283),x4283,a2) % 3.72/3.76 [429]~E(x4291,x4292)+~P1(x4293)+~P1(x4292)+~P1(x4291)+~P1(x4294)+~P3(x4294,x4291,a2)+~P9(x4294,a2,x4293)+~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) % 3.72/3.76 [430]~E(x4301,x4303)+~P1(x4303)+~P1(x4302)+~P1(x4301)+~P1(x4304)+~P3(x4304,x4301,a2)+~P9(x4304,a2,x4302)+~P7(x4301,a1)+E(f9(x4301,x4302,x4303),x4302)+P9(f15(x4301,x4302,x4303),a2,f9(x4301,x4302,x4303))+P3(f9(x4301,x4302,x4303),x4302,a2) % 3.72/3.76 [431]~E(x4311,x4312)+~P1(x4313)+~P1(x4312)+~P1(x4311)+~P1(x4314)+~P3(x4314,x4311,a2)+~P9(x4314,a2,x4313)+~P7(x4311,a1)+E(f9(x4311,x4312,x4313),x4312)+P9(f15(x4311,x4312,x4313),a2,f9(x4311,x4312,x4313))+P3(f9(x4311,x4312,x4313),x4312,a2) % 3.72/3.76 [442]~P1(x4423)+~P1(x4422)+~P1(x4421)+~P1(x4424)+~P3(x4424,x4421,a2)+~P3(x4423,x4421,a2)+~P9(x4424,a2,x4422)+~P7(x4421,a1)+E(f9(x4421,x4422,x4423),x4423)+P9(f14(x4421,x4422,x4423),a2,f9(x4421,x4422,x4423))+P3(f9(x4421,x4422,x4423),x4423,a2) % 3.72/3.76 [443]~P1(x4433)+~P1(x4432)+~P1(x4431)+~P1(x4434)+~P3(x4434,x4431,a2)+~P3(x4432,x4431,a2)+~P9(x4434,a2,x4433)+~P7(x4431,a1)+E(f9(x4431,x4432,x4433),x4433)+P9(f14(x4431,x4432,x4433),a2,f9(x4431,x4432,x4433))+P3(f9(x4431,x4432,x4433),x4433,a2) % 3.72/3.76 [444]~P1(x4443)+~P1(x4442)+~P1(x4441)+~P1(x4444)+~P3(x4444,x4441,a2)+~P3(x4443,x4441,a2)+~P9(x4444,a2,x4442)+~P7(x4441,a1)+E(f9(x4441,x4442,x4443),x4442)+P9(f15(x4441,x4442,x4443),a2,f9(x4441,x4442,x4443))+P3(f9(x4441,x4442,x4443),x4442,a2) % 3.72/3.76 [445]~P1(x4453)+~P1(x4452)+~P1(x4451)+~P1(x4454)+~P3(x4454,x4451,a2)+~P3(x4452,x4451,a2)+~P9(x4454,a2,x4453)+~P7(x4451,a1)+E(f9(x4451,x4452,x4453),x4452)+P9(f15(x4451,x4452,x4453),a2,f9(x4451,x4452,x4453))+P3(f9(x4451,x4452,x4453),x4452,a2) % 3.72/3.76 [446]~P1(x4463)+~P1(x4462)+~P1(x4461)+~P1(x4464)+~P3(x4464,x4461,a2)+~P9(x4464,a2,x4463)+~P9(x4461,a2,x4462)+~P7(x4461,a1)+E(f9(x4461,x4462,x4463),x4463)+P9(f14(x4461,x4462,x4463),a2,f9(x4461,x4462,x4463))+P3(f9(x4461,x4462,x4463),x4463,a2) % 3.72/3.76 [447]~P1(x4473)+~P1(x4472)+~P1(x4471)+~P1(x4474)+~P3(x4474,x4471,a2)+~P9(x4474,a2,x4473)+~P10(x4471,a2,x4472)+~P7(x4471,a1)+E(f9(x4471,x4472,x4473),x4473)+P9(f14(x4471,x4472,x4473),a2,f9(x4471,x4472,x4473))+P3(f9(x4471,x4472,x4473),x4473,a2) % 3.72/3.76 [448]~P1(x4483)+~P1(x4482)+~P1(x4481)+~P1(x4484)+~P3(x4484,x4481,a2)+~P9(x4484,a2,x4482)+~P9(x4481,a2,x4483)+~P7(x4481,a1)+E(f9(x4481,x4482,x4483),x4483)+P9(f14(x4481,x4482,x4483),a2,f9(x4481,x4482,x4483))+P3(f9(x4481,x4482,x4483),x4483,a2) % 3.72/3.76 [449]~P1(x4493)+~P1(x4492)+~P1(x4491)+~P1(x4494)+~P3(x4494,x4491,a2)+~P9(x4494,a2,x4492)+~P10(x4491,a2,x4493)+~P7(x4491,a1)+E(f9(x4491,x4492,x4493),x4493)+P9(f14(x4491,x4492,x4493),a2,f9(x4491,x4492,x4493))+P3(f9(x4491,x4492,x4493),x4493,a2) % 3.72/3.76 [450]~P1(x4503)+~P1(x4502)+~P1(x4501)+~P1(x4504)+~P3(x4504,x4501,a2)+~P9(x4504,a2,x4503)+~P9(x4501,a2,x4502)+~P7(x4501,a1)+E(f9(x4501,x4502,x4503),x4502)+P9(f15(x4501,x4502,x4503),a2,f9(x4501,x4502,x4503))+P3(f9(x4501,x4502,x4503),x4502,a2) % 3.72/3.76 [451]~P1(x4513)+~P1(x4512)+~P1(x4511)+~P1(x4514)+~P3(x4514,x4511,a2)+~P9(x4514,a2,x4513)+~P10(x4511,a2,x4512)+~P7(x4511,a1)+E(f9(x4511,x4512,x4513),x4512)+P9(f15(x4511,x4512,x4513),a2,f9(x4511,x4512,x4513))+P3(f9(x4511,x4512,x4513),x4512,a2) % 3.72/3.76 [452]~P1(x4523)+~P1(x4522)+~P1(x4521)+~P1(x4524)+~P3(x4524,x4521,a2)+~P9(x4524,a2,x4522)+~P9(x4521,a2,x4523)+~P7(x4521,a1)+E(f9(x4521,x4522,x4523),x4522)+P9(f15(x4521,x4522,x4523),a2,f9(x4521,x4522,x4523))+P3(f9(x4521,x4522,x4523),x4522,a2) % 3.72/3.76 [453]~P1(x4533)+~P1(x4532)+~P1(x4531)+~P1(x4534)+~P3(x4534,x4531,a2)+~P9(x4534,a2,x4532)+~P10(x4531,a2,x4533)+~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) % 3.72/3.76 [293]~P1(x2933)+~P1(x2932)+~P1(x2931)+~P1(x2934)+~P1(x2935)+~P3(x2934,x2931,a2)+~P3(x2935,x2931,a2)+~P9(x2934,a2,x2932)+~P9(x2935,a2,x2933)+~P7(x2931,a1)+P1(f9(x2931,x2932,x2933)) % 3.72/3.76 [344]~P1(x3443)+~P1(x3442)+~P1(x3441)+~P1(x3444)+~P1(x3445)+~P3(x3444,x3442,a2)+~P3(x3445,x3442,a2)+~P9(x3444,a2,x3443)+~P9(x3445,a2,x3441)+~P7(x3442,a1)+P10(x3441,a2,f9(x3442,x3443,x3441)) % 3.72/3.76 [345]~P1(x3453)+~P1(x3452)+~P1(x3451)+~P1(x3454)+~P1(x3455)+~P3(x3454,x3452,a2)+~P3(x3455,x3452,a2)+~P9(x3454,a2,x3451)+~P9(x3455,a2,x3453)+~P7(x3452,a1)+P10(x3451,a2,f9(x3452,x3451,x3453)) % 3.72/3.76 [370]~P1(x3702)+~P1(x3701)+~P1(x3703)+~P1(x3704)+~P1(x3705)+~P3(x3704,x3701,a2)+~P3(x3705,x3701,a2)+~P9(x3704,a2,x3702)+~P9(x3705,a2,x3703)+~P7(x3701,a1)+E(f9(x3701,x3702,x3703),x3703)+P9(x3703,a2,f9(x3701,x3702,x3703)) % 3.72/3.76 [371]~P1(x3713)+~P1(x3711)+~P1(x3712)+~P1(x3714)+~P1(x3715)+~P3(x3714,x3711,a2)+~P3(x3715,x3711,a2)+~P9(x3714,a2,x3712)+~P9(x3715,a2,x3713)+~P7(x3711,a1)+E(f9(x3711,x3712,x3713),x3712)+P9(x3712,a2,f9(x3711,x3712,x3713)) % 3.72/3.76 [434]~P1(x4343)+~P1(x4342)+~P1(x4341)+~P1(x4344)+~P1(x4345)+~P3(x4344,x4341,a2)+~P3(x4345,x4341,a2)+~P9(x4344,a2,x4342)+~P9(x4345,a2,x4343)+~P7(x4341,a1)+E(f9(x4341,x4342,x4343),x4343)+P3(f9(x4341,x4342,x4343),x4343,a2)+P1(f14(x4341,x4342,x4343)) % 3.72/3.76 [435]~P1(x4353)+~P1(x4352)+~P1(x4351)+~P1(x4354)+~P1(x4355)+~P3(x4354,x4351,a2)+~P3(x4355,x4351,a2)+~P9(x4354,a2,x4352)+~P9(x4355,a2,x4353)+~P7(x4351,a1)+E(f9(x4351,x4352,x4353),x4352)+P3(f9(x4351,x4352,x4353),x4352,a2)+P1(f15(x4351,x4352,x4353)) % 3.72/3.76 [440]~P1(x4403)+~P1(x4402)+~P1(x4401)+~P1(x4404)+~P1(x4405)+~P3(x4404,x4401,a2)+~P3(x4405,x4401,a2)+~P9(x4404,a2,x4402)+~P9(x4405,a2,x4403)+~P7(x4401,a1)+E(f9(x4401,x4402,x4403),x4403)+P3(f14(x4401,x4402,x4403),x4403,a2)+P3(f9(x4401,x4402,x4403),x4403,a2) % 3.72/3.76 [441]~P1(x4413)+~P1(x4412)+~P1(x4411)+~P1(x4414)+~P1(x4415)+~P3(x4414,x4411,a2)+~P3(x4415,x4411,a2)+~P9(x4414,a2,x4412)+~P9(x4415,a2,x4413)+~P7(x4411,a1)+E(f9(x4411,x4412,x4413),x4412)+P3(f15(x4411,x4412,x4413),x4412,a2)+P3(f9(x4411,x4412,x4413),x4412,a2) % 3.72/3.76 [454]~P1(x4543)+~P1(x4542)+~P1(x4541)+~P1(x4544)+~P1(x4545)+~P3(x4544,x4541,a2)+~P3(x4545,x4541,a2)+~P9(x4544,a2,x4542)+~P9(x4545,a2,x4543)+~P7(x4541,a1)+E(f9(x4541,x4542,x4543),x4543)+P9(f14(x4541,x4542,x4543),a2,f9(x4541,x4542,x4543))+P3(f9(x4541,x4542,x4543),x4543,a2) % 3.72/3.76 [455]~P1(x4553)+~P1(x4552)+~P1(x4551)+~P1(x4554)+~P1(x4555)+~P3(x4554,x4551,a2)+~P3(x4555,x4551,a2)+~P9(x4554,a2,x4552)+~P9(x4555,a2,x4553)+~P7(x4551,a1)+E(f9(x4551,x4552,x4553),x4552)+P9(f15(x4551,x4552,x4553),a2,f9(x4551,x4552,x4553))+P3(f9(x4551,x4552,x4553),x4552,a2) % 3.72/3.76 %EqnAxiom % 3.72/3.76 [1]E(x11,x11) % 3.72/3.76 [2]E(x22,x21)+~E(x21,x22) % 3.72/3.76 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 3.72/3.76 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 3.72/3.76 [5]~E(x51,x52)+E(f25(x51),f25(x52)) % 3.72/3.76 [6]~E(x61,x62)+E(f26(x61),f26(x62)) % 3.72/3.76 [7]~E(x71,x72)+E(f27(x71),f27(x72)) % 3.72/3.76 [8]~E(x81,x82)+E(f29(x81),f29(x82)) % 3.72/3.76 [9]~E(x91,x92)+E(f30(x91),f30(x92)) % 3.72/3.76 [10]~E(x101,x102)+E(f4(x101),f4(x102)) % 3.72/3.76 [11]~E(x111,x112)+E(f5(x111),f5(x112)) % 3.72/3.76 [12]~E(x121,x122)+E(f9(x121,x123,x124),f9(x122,x123,x124)) % 3.72/3.76 [13]~E(x131,x132)+E(f9(x133,x131,x134),f9(x133,x132,x134)) % 3.72/3.76 [14]~E(x141,x142)+E(f9(x143,x144,x141),f9(x143,x144,x142)) % 3.72/3.76 [15]~E(x151,x152)+E(f15(x151,x153,x154),f15(x152,x153,x154)) % 3.72/3.76 [16]~E(x161,x162)+E(f15(x163,x161,x164),f15(x163,x162,x164)) % 3.72/3.76 [17]~E(x171,x172)+E(f15(x173,x174,x171),f15(x173,x174,x172)) % 3.72/3.76 [18]~E(x181,x182)+E(f14(x181,x183,x184),f14(x182,x183,x184)) % 3.72/3.76 [19]~E(x191,x192)+E(f14(x193,x191,x194),f14(x193,x192,x194)) % 3.72/3.76 [20]~E(x201,x202)+E(f14(x203,x204,x201),f14(x203,x204,x202)) % 3.72/3.76 [21]~E(x211,x212)+E(f10(x211,x213,x214),f10(x212,x213,x214)) % 3.72/3.76 [22]~E(x221,x222)+E(f10(x223,x221,x224),f10(x223,x222,x224)) % 3.72/3.76 [23]~E(x231,x232)+E(f10(x233,x234,x231),f10(x233,x234,x232)) % 3.72/3.76 [24]~E(x241,x242)+E(f12(x241,x243,x244),f12(x242,x243,x244)) % 3.72/3.76 [25]~E(x251,x252)+E(f12(x253,x251,x254),f12(x253,x252,x254)) % 3.72/3.76 [26]~E(x261,x262)+E(f12(x263,x264,x261),f12(x263,x264,x262)) % 3.72/3.76 [27]~E(x271,x272)+E(f13(x271,x273,x274),f13(x272,x273,x274)) % 3.72/3.76 [28]~E(x281,x282)+E(f13(x283,x281,x284),f13(x283,x282,x284)) % 3.72/3.76 [29]~E(x291,x292)+E(f13(x293,x294,x291),f13(x293,x294,x292)) % 3.72/3.76 [30]~E(x301,x302)+E(f11(x301,x303,x304),f11(x302,x303,x304)) % 3.72/3.76 [31]~E(x311,x312)+E(f11(x313,x311,x314),f11(x313,x312,x314)) % 3.72/3.76 [32]~E(x321,x322)+E(f11(x323,x324,x321),f11(x323,x324,x322)) % 3.72/3.76 [33]~E(x331,x332)+E(f24(x331,x333,x334,x335),f24(x332,x333,x334,x335)) % 3.72/3.76 [34]~E(x341,x342)+E(f24(x343,x341,x344,x345),f24(x343,x342,x344,x345)) % 3.72/3.76 [35]~E(x351,x352)+E(f24(x353,x354,x351,x355),f24(x353,x354,x352,x355)) % 3.72/3.76 [36]~E(x361,x362)+E(f24(x363,x364,x365,x361),f24(x363,x364,x365,x362)) % 3.72/3.76 [37]~E(x371,x372)+E(f28(x371,x373,x374,x375),f28(x372,x373,x374,x375)) % 3.72/3.76 [38]~E(x381,x382)+E(f28(x383,x381,x384,x385),f28(x383,x382,x384,x385)) % 3.72/3.76 [39]~E(x391,x392)+E(f28(x393,x394,x391,x395),f28(x393,x394,x392,x395)) % 3.72/3.76 [40]~E(x401,x402)+E(f28(x403,x404,x405,x401),f28(x403,x404,x405,x402)) % 3.72/3.76 [41]~E(x411,x412)+E(f8(x411,x413,x414),f8(x412,x413,x414)) % 3.72/3.76 [42]~E(x421,x422)+E(f8(x423,x421,x424),f8(x423,x422,x424)) % 3.72/3.76 [43]~E(x431,x432)+E(f8(x433,x434,x431),f8(x433,x434,x432)) % 3.72/3.76 [44]~E(x441,x442)+E(f7(x441,x443),f7(x442,x443)) % 3.72/3.76 [45]~E(x451,x452)+E(f7(x453,x451),f7(x453,x452)) % 3.72/3.76 [46]~P1(x461)+P1(x462)+~E(x461,x462) % 3.72/3.76 [47]P9(x472,x473,x474)+~E(x471,x472)+~P9(x471,x473,x474) % 3.72/3.76 [48]P9(x483,x482,x484)+~E(x481,x482)+~P9(x483,x481,x484) % 3.72/3.76 [49]P9(x493,x494,x492)+~E(x491,x492)+~P9(x493,x494,x491) % 3.72/3.76 [50]P3(x502,x503,x504)+~E(x501,x502)+~P3(x501,x503,x504) % 3.72/3.76 [51]P3(x513,x512,x514)+~E(x511,x512)+~P3(x513,x511,x514) % 3.72/3.76 [52]P3(x523,x524,x522)+~E(x521,x522)+~P3(x523,x524,x521) % 3.72/3.76 [53]P10(x532,x533,x534)+~E(x531,x532)+~P10(x531,x533,x534) % 3.72/3.76 [54]P10(x543,x542,x544)+~E(x541,x542)+~P10(x543,x541,x544) % 3.72/3.76 [55]P10(x553,x554,x552)+~E(x551,x552)+~P10(x553,x554,x551) % 3.72/3.76 [56]P7(x562,x563)+~E(x561,x562)+~P7(x561,x563) % 3.72/3.76 [57]P7(x573,x572)+~E(x571,x572)+~P7(x573,x571) % 3.72/3.76 [58]~P6(x581)+P6(x582)+~E(x581,x582) % 3.72/3.76 [59]~P2(x591)+P2(x592)+~E(x591,x592) % 3.72/3.76 [60]~P5(x601)+P5(x602)+~E(x601,x602) % 3.72/3.76 [61]~P8(x611)+P8(x612)+~E(x611,x612) % 3.72/3.76 [62]P4(x622,x623,x624)+~E(x621,x622)+~P4(x621,x623,x624) % 3.72/3.76 [63]P4(x633,x632,x634)+~E(x631,x632)+~P4(x633,x631,x634) % 3.72/3.76 [64]P4(x643,x644,x642)+~E(x641,x642)+~P4(x643,x644,x641) % 3.72/3.76 % 3.72/3.76 %------------------------------------------- % 3.72/3.76 cnf(546,plain, % 3.72/3.76 (~P3(x5461,a34,a2)), % 3.72/3.76 inference(rename_variables,[],[92])). % 3.72/3.76 cnf(549,plain, % 3.72/3.76 (P3(a37,a34,a2)), % 3.72/3.76 inference(scs_inference,[],[91,80,85,92,546,76,51,53,55,140])). % 3.72/3.76 cnf(588,plain, % 3.72/3.76 ($false), % 3.72/3.76 inference(scs_inference,[],[549,92]), % 3.72/3.76 ['proof']). % 3.72/3.76 % SZS output end Proof % 3.72/3.76 % Total time :2.150000s %------------------------------------------------------------------------------