%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM017+4 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n032.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:46 EDT 2024 % Result : Theorem 97.17s 97.28s % Output : CNFRefutation 97.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.08 % Problem : COM017+4 : TPTP v8.2.0. Released v4.0.0. % 0.02/0.08 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.27 % Computer : n032.cluster.edu % 0.07/0.27 % Model : x86_64 x86_64 % 0.07/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.27 % Memory : 8042.1875MB % 0.07/0.27 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.27 % CPULimit : 300 % 0.07/0.27 % WCLimit : 300 % 0.07/0.27 % DateTime : Thu Jun 20 23:54:09 EDT 2024 % 0.07/0.27 % CPUTime : % 0.12/0.45 start to proof:theBenchmark % 97.17/97.25 %------------------------------------------- % 97.17/97.25 % File :CSE---1.7 % 97.17/97.25 % Problem :theBenchmark % 97.17/97.25 % Transform :cnf % 97.17/97.25 % Format :tptp:raw % 97.17/97.25 % Command :java -jar mcs_scs.jar %d %s % 97.17/97.25 % 97.17/97.25 % Result :Theorem 95.760000s % 97.17/97.25 % Output :CNFRefutation 95.760000s % 97.17/97.25 %------------------------------------------- % 97.17/97.26 %------------------------------------------------------------------------------ % 97.17/97.26 % File : COM017+4 : TPTP v8.2.0. Released v4.0.0. % 97.17/97.26 % Domain : Computing Theory % 97.17/97.26 % Problem : Newman's lemma on rewriting systems 03_01_03, 03 expansion % 97.17/97.26 % Version : Especial. % 97.17/97.26 % English : % 97.17/97.26 % 97.17/97.26 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 97.17/97.26 % : [PV+07] Paskevich et al. (2007), Reasoning Inside a Formula an % 97.17/97.26 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 97.17/97.26 % Source : [Pas08] % 97.17/97.26 % Names : newman_03_01_03.03 [Pas08] % 97.17/97.26 % 97.17/97.26 % Status : Theorem % 97.17/97.26 % Rating : 0.22 v8.2.0, 0.19 v8.1.0, 0.25 v7.4.0, 0.13 v7.3.0, 0.14 v7.1.0, 0.13 v6.4.0, 0.15 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.40 v6.0.0, 0.39 v5.5.0, 0.41 v5.4.0, 0.50 v5.3.0, 0.52 v5.2.0, 0.25 v5.1.0, 0.38 v5.0.0, 0.50 v4.1.0, 0.61 v4.0.1, 0.78 v4.0.0 % 97.17/97.26 % Syntax : Number of formulae : 22 ( 1 unt; 6 def) % 97.17/97.26 % Number of atoms : 191 ( 11 equ) % 97.17/97.26 % Maximal formula atoms : 33 ( 8 avg) % 97.17/97.26 % Number of connectives : 170 ( 1 ~; 34 |; 100 &) % 97.17/97.26 % ( 6 <=>; 29 =>; 0 <=; 0 <~>) % 97.17/97.26 % Maximal formula depth : 17 ( 8 avg) % 97.17/97.26 % Maximal term depth : 1 ( 1 avg) % 97.17/97.26 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 97.17/97.26 % Number of functors : 6 ( 6 usr; 6 con; 0-0 aty) % 97.17/97.26 % Number of variables : 69 ( 48 !; 21 ?) % 97.17/97.26 % SPC : FOF_THM_RFO_SEQ % 97.17/97.26 % 97.17/97.26 % Comments : Problem generated by the SAD system [VLP07] % 97.17/97.26 %------------------------------------------------------------------------------ % 97.17/97.26 fof(mElmSort,axiom, % 97.17/97.26 ! [W0] : % 97.17/97.26 ( aElement0(W0) % 97.17/97.26 => $true ) ). % 97.17/97.26 % 97.17/97.26 fof(mRelSort,axiom, % 97.17/97.26 ! [W0] : % 97.17/97.26 ( aRewritingSystem0(W0) % 97.17/97.26 => $true ) ). % 97.17/97.26 % 97.17/97.26 fof(mReduct,axiom, % 97.17/97.26 ! [W0,W1] : % 97.17/97.26 ( ( aElement0(W0) % 97.17/97.26 & aRewritingSystem0(W1) ) % 97.17/97.26 => ! [W2] : % 97.17/97.26 ( aReductOfIn0(W2,W0,W1) % 97.17/97.26 => aElement0(W2) ) ) ). % 97.17/97.26 % 97.17/97.26 fof(mWFOrd,axiom, % 97.17/97.26 ! [W0,W1] : % 97.17/97.26 ( ( aElement0(W0) % 97.17/97.26 & aElement0(W1) ) % 97.17/97.26 => ( iLess0(W0,W1) % 97.17/97.26 => $true ) ) ). % 97.17/97.26 % 97.17/97.26 fof(mTCbr,axiom, % 97.17/97.26 ! [W0,W1,W2] : % 97.17/97.26 ( ( aElement0(W0) % 97.17/97.26 & aRewritingSystem0(W1) % 97.17/97.26 & aElement0(W2) ) % 97.17/97.26 => ( sdtmndtplgtdt0(W0,W1,W2) % 97.17/97.26 => $true ) ) ). % 97.17/97.26 % 97.17/97.26 fof(mTCDef,definition, % 97.17/97.26 ! [W0,W1,W2] : % 97.17/97.26 ( ( aElement0(W0) % 97.17/97.27 & aRewritingSystem0(W1) % 97.17/97.27 & aElement0(W2) ) % 97.17/97.27 => ( sdtmndtplgtdt0(W0,W1,W2) % 97.17/97.27 <=> ( aReductOfIn0(W2,W0,W1) % 97.17/97.27 | ? [W3] : % 97.17/97.27 ( aElement0(W3) % 97.17/97.27 & aReductOfIn0(W3,W0,W1) % 97.17/97.27 & sdtmndtplgtdt0(W3,W1,W2) ) ) ) ) ). % 97.17/97.27 % 97.17/97.27 fof(mTCTrans,axiom, % 97.17/97.27 ! [W0,W1,W2,W3] : % 97.17/97.27 ( ( aElement0(W0) % 97.17/97.27 & aRewritingSystem0(W1) % 97.17/97.27 & aElement0(W2) % 97.17/97.27 & aElement0(W3) ) % 97.17/97.27 => ( ( sdtmndtplgtdt0(W0,W1,W2) % 97.17/97.27 & sdtmndtplgtdt0(W2,W1,W3) ) % 97.17/97.27 => sdtmndtplgtdt0(W0,W1,W3) ) ) ). % 97.17/97.27 % 97.17/97.27 fof(mTCRDef,definition, % 97.17/97.27 ! [W0,W1,W2] : % 97.17/97.27 ( ( aElement0(W0) % 97.17/97.27 & aRewritingSystem0(W1) % 97.17/97.27 & aElement0(W2) ) % 97.17/97.27 => ( sdtmndtasgtdt0(W0,W1,W2) % 97.17/97.27 <=> ( W0 = W2 % 97.17/97.27 | sdtmndtplgtdt0(W0,W1,W2) ) ) ) ). % 97.17/97.27 % 97.17/97.27 fof(mTCRTrans,axiom, % 97.17/97.27 ! [W0,W1,W2,W3] : % 97.17/97.27 ( ( aElement0(W0) % 97.17/97.27 & aRewritingSystem0(W1) % 97.17/97.27 & aElement0(W2) % 97.17/97.27 & aElement0(W3) ) % 97.17/97.27 => ( ( sdtmndtasgtdt0(W0,W1,W2) % 97.17/97.27 & sdtmndtasgtdt0(W2,W1,W3) ) % 97.17/97.27 => sdtmndtasgtdt0(W0,W1,W3) ) ) ). % 97.17/97.27 % 97.17/97.27 fof(mCRDef,definition, % 97.17/97.27 ! [W0] : % 97.17/97.27 ( aRewritingSystem0(W0) % 97.17/97.27 => ( isConfluent0(W0) % 97.17/97.27 <=> ! [W1,W2,W3] : % 97.17/97.27 ( ( aElement0(W1) % 97.17/97.27 & aElement0(W2) % 97.17/97.27 & aElement0(W3) % 97.17/97.27 & sdtmndtasgtdt0(W1,W0,W2) % 97.17/97.27 & sdtmndtasgtdt0(W1,W0,W3) ) % 97.17/97.27 => ? [W4] : % 97.17/97.27 ( aElement0(W4) % 97.17/97.27 & sdtmndtasgtdt0(W2,W0,W4) % 97.17/97.27 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 97.17/97.27 % 97.17/97.27 fof(mWCRDef,definition, % 97.17/97.27 ! [W0] : % 97.17/97.27 ( aRewritingSystem0(W0) % 97.17/97.27 => ( isLocallyConfluent0(W0) % 97.17/97.27 <=> ! [W1,W2,W3] : % 97.17/97.27 ( ( aElement0(W1) % 97.17/97.27 & aElement0(W2) % 97.17/97.27 & aElement0(W3) % 97.17/97.27 & aReductOfIn0(W2,W1,W0) % 97.17/97.27 & aReductOfIn0(W3,W1,W0) ) % 97.17/97.27 => ? [W4] : % 97.17/97.27 ( aElement0(W4) % 97.17/97.27 & sdtmndtasgtdt0(W2,W0,W4) % 97.17/97.27 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 97.17/97.27 % 97.17/97.27 fof(mTermin,definition, % 97.17/97.27 ! [W0] : % 97.17/97.27 ( aRewritingSystem0(W0) % 97.17/97.27 => ( isTerminating0(W0) % 97.17/97.27 <=> ! [W1,W2] : % 97.17/97.27 ( ( aElement0(W1) % 97.17/97.27 & aElement0(W2) ) % 97.17/97.27 => ( sdtmndtplgtdt0(W1,W0,W2) % 97.17/97.27 => iLess0(W2,W1) ) ) ) ) ). % 97.17/97.27 % 97.17/97.27 fof(mNFRDef,definition, % 97.17/97.27 ! [W0,W1] : % 97.17/97.27 ( ( aElement0(W0) % 97.17/97.27 & aRewritingSystem0(W1) ) % 97.17/97.27 => ! [W2] : % 97.17/97.27 ( aNormalFormOfIn0(W2,W0,W1) % 97.17/97.27 <=> ( aElement0(W2) % 97.17/97.27 & sdtmndtasgtdt0(W0,W1,W2) % 97.17/97.27 & ~ ? [W3] : aReductOfIn0(W3,W2,W1) ) ) ) ). % 97.17/97.27 % 97.17/97.27 fof(mTermNF,axiom, % 97.17/97.27 ! [W0] : % 97.17/97.27 ( ( aRewritingSystem0(W0) % 97.17/97.27 & isTerminating0(W0) ) % 97.17/97.27 => ! [W1] : % 97.17/97.27 ( aElement0(W1) % 97.17/97.27 => ? [W2] : aNormalFormOfIn0(W2,W1,W0) ) ) ). % 97.17/97.27 % 97.17/97.27 fof(m__656,hypothesis, % 97.17/97.27 aRewritingSystem0(xR) ). % 97.17/97.27 % 97.17/97.27 fof(m__656_01,hypothesis, % 97.17/97.27 ( ! [W0,W1,W2] : % 97.17/97.27 ( ( aElement0(W0) % 97.17/97.27 & aElement0(W1) % 97.17/97.27 & aElement0(W2) % 97.17/97.27 & aReductOfIn0(W1,W0,xR) % 97.17/97.27 & aReductOfIn0(W2,W0,xR) ) % 97.17/97.27 => ? [W3] : % 97.17/97.27 ( aElement0(W3) % 97.17/97.27 & ( W1 = W3 % 97.17/97.27 | ( ( aReductOfIn0(W3,W1,xR) % 97.17/97.27 | ? [W4] : % 97.17/97.27 ( aElement0(W4) % 97.17/97.27 & aReductOfIn0(W4,W1,xR) % 97.17/97.27 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 97.17/97.27 & sdtmndtplgtdt0(W1,xR,W3) ) ) % 97.17/97.27 & sdtmndtasgtdt0(W1,xR,W3) % 97.17/97.27 & ( W2 = W3 % 97.17/97.27 | ( ( aReductOfIn0(W3,W2,xR) % 97.17/97.27 | ? [W4] : % 97.17/97.27 ( aElement0(W4) % 97.17/97.27 & aReductOfIn0(W4,W2,xR) % 97.17/97.27 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 97.17/97.27 & sdtmndtplgtdt0(W2,xR,W3) ) ) % 97.17/97.27 & sdtmndtasgtdt0(W2,xR,W3) ) ) % 97.17/97.27 & isLocallyConfluent0(xR) % 97.17/97.27 & ! [W0,W1] : % 97.17/97.27 ( ( aElement0(W0) % 97.17/97.27 & aElement0(W1) ) % 97.17/97.27 => ( ( aReductOfIn0(W1,W0,xR) % 97.17/97.27 | ? [W2] : % 97.17/97.27 ( aElement0(W2) % 97.17/97.27 & aReductOfIn0(W2,W0,xR) % 97.17/97.27 & sdtmndtplgtdt0(W2,xR,W1) ) % 97.17/97.27 | sdtmndtplgtdt0(W0,xR,W1) ) % 97.17/97.27 => iLess0(W1,W0) ) ) % 97.17/97.27 & isTerminating0(xR) ) ). % 97.17/97.27 % 97.17/97.27 fof(m__731,hypothesis, % 97.17/97.27 ( aElement0(xa) % 97.17/97.27 & aElement0(xb) % 97.17/97.27 & aElement0(xc) ) ). % 97.17/97.27 % 97.17/97.27 fof(m__715,hypothesis, % 97.17/97.27 ! [W0,W1,W2] : % 97.17/97.27 ( ( aElement0(W0) % 97.17/97.27 & aElement0(W1) % 97.17/97.27 & aElement0(W2) % 97.17/97.27 & ( W0 = W1 % 97.17/97.27 | aReductOfIn0(W1,W0,xR) % 97.17/97.27 | ? [W3] : % 97.17/97.27 ( aElement0(W3) % 97.17/97.27 & aReductOfIn0(W3,W0,xR) % 97.17/97.27 & sdtmndtplgtdt0(W3,xR,W1) ) % 97.17/97.27 | sdtmndtplgtdt0(W0,xR,W1) % 97.17/97.27 | sdtmndtasgtdt0(W0,xR,W1) ) % 97.17/97.27 & ( W0 = W2 % 97.17/97.27 | aReductOfIn0(W2,W0,xR) % 97.17/97.27 | ? [W3] : % 97.17/97.27 ( aElement0(W3) % 97.17/97.27 & aReductOfIn0(W3,W0,xR) % 97.17/97.27 & sdtmndtplgtdt0(W3,xR,W2) ) % 97.17/97.27 | sdtmndtplgtdt0(W0,xR,W2) % 97.17/97.27 | sdtmndtasgtdt0(W0,xR,W2) ) ) % 97.17/97.27 => ( iLess0(W0,xa) % 97.17/97.27 => ? [W3] : % 97.17/97.27 ( aElement0(W3) % 97.17/97.27 & ( W1 = W3 % 97.17/97.27 | ( ( aReductOfIn0(W3,W1,xR) % 97.17/97.27 | ? [W4] : % 97.17/97.27 ( aElement0(W4) % 97.17/97.27 & aReductOfIn0(W4,W1,xR) % 97.17/97.27 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 97.17/97.27 & sdtmndtplgtdt0(W1,xR,W3) ) ) % 97.17/97.27 & sdtmndtasgtdt0(W1,xR,W3) % 97.17/97.27 & ( W2 = W3 % 97.17/97.27 | ( ( aReductOfIn0(W3,W2,xR) % 97.17/97.27 | ? [W4] : % 97.17/97.27 ( aElement0(W4) % 97.17/97.27 & aReductOfIn0(W4,W2,xR) % 97.17/97.27 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 97.17/97.27 & sdtmndtplgtdt0(W2,xR,W3) ) ) % 97.17/97.27 & sdtmndtasgtdt0(W2,xR,W3) ) ) ) ). % 97.17/97.27 % 97.17/97.27 fof(m__731_02,hypothesis, % 97.17/97.27 ( ( aReductOfIn0(xb,xa,xR) % 97.17/97.27 | ? [W0] : % 97.17/97.27 ( aElement0(W0) % 97.17/97.27 & aReductOfIn0(W0,xa,xR) % 97.17/97.27 & sdtmndtplgtdt0(W0,xR,xb) ) ) % 97.17/97.27 & sdtmndtplgtdt0(xa,xR,xb) % 97.17/97.27 & ( aReductOfIn0(xc,xa,xR) % 97.17/97.27 | ? [W0] : % 97.17/97.27 ( aElement0(W0) % 97.17/97.27 & aReductOfIn0(W0,xa,xR) % 97.17/97.27 & sdtmndtplgtdt0(W0,xR,xc) ) ) % 97.17/97.27 & sdtmndtplgtdt0(xa,xR,xc) ) ). % 97.17/97.27 % 97.17/97.28 fof(m__755,hypothesis, % 97.17/97.28 ( aElement0(xu) % 97.17/97.28 & aReductOfIn0(xu,xa,xR) % 97.17/97.28 & ( xu = xb % 97.17/97.28 | ( ( aReductOfIn0(xb,xu,xR) % 97.17/97.28 | ? [W0] : % 97.17/97.28 ( aElement0(W0) % 97.17/97.28 & aReductOfIn0(W0,xu,xR) % 97.17/97.28 & sdtmndtplgtdt0(W0,xR,xb) ) ) % 97.17/97.28 & sdtmndtplgtdt0(xu,xR,xb) ) ) % 97.17/97.28 & sdtmndtasgtdt0(xu,xR,xb) ) ). % 97.17/97.28 % 97.17/97.28 fof(m__779,hypothesis, % 97.17/97.28 ( aElement0(xv) % 97.17/97.28 & aReductOfIn0(xv,xa,xR) % 97.17/97.28 & ( xv = xc % 97.17/97.28 | ( ( aReductOfIn0(xc,xv,xR) % 97.17/97.28 | ? [W0] : % 97.17/97.28 ( aElement0(W0) % 97.17/97.28 & aReductOfIn0(W0,xv,xR) % 97.17/97.28 & sdtmndtplgtdt0(W0,xR,xc) ) ) % 97.17/97.28 & sdtmndtplgtdt0(xv,xR,xc) ) ) % 97.17/97.28 & sdtmndtasgtdt0(xv,xR,xc) ) ). % 97.17/97.28 % 97.17/97.28 fof(m__,conjecture, % 97.17/97.28 ? [W0] : % 97.17/97.28 ( aElement0(W0) % 97.17/97.28 & ( xu = W0 % 97.17/97.28 | aReductOfIn0(W0,xu,xR) % 97.17/97.28 | ? [W1] : % 97.17/97.28 ( aElement0(W1) % 97.17/97.28 & aReductOfIn0(W1,xu,xR) % 97.17/97.28 & sdtmndtplgtdt0(W1,xR,W0) ) % 97.17/97.28 | sdtmndtplgtdt0(xu,xR,W0) % 97.17/97.28 | sdtmndtasgtdt0(xu,xR,W0) ) % 97.17/97.28 & ( xv = W0 % 97.17/97.28 | aReductOfIn0(W0,xv,xR) % 97.17/97.28 | ? [W1] : % 97.17/97.28 ( aElement0(W1) % 97.17/97.28 & aReductOfIn0(W1,xv,xR) % 97.17/97.28 & sdtmndtplgtdt0(W1,xR,W0) ) % 97.17/97.28 | sdtmndtplgtdt0(xv,xR,W0) % 97.17/97.28 | sdtmndtasgtdt0(xv,xR,W0) ) ) ). % 97.17/97.28 % 97.17/97.28 %------------------------------------------------------------------------------ % 97.17/97.28 %------------------------------------------- % 97.17/97.28 % Proof found % 97.17/97.28 % SZS status Theorem for theBenchmark % 97.17/97.28 % SZS output start Proof % 97.17/97.28 %ClaNum:445(EqnAxiom:64) % 97.17/97.28 %VarNum:5702(SingletonVarNum:1106) % 97.17/97.28 %MaxLitNum:13 % 97.17/97.28 %MaxfuncDepth:1 % 97.17/97.28 %SharedTerms:44 % 97.17/97.28 %goalClause: 79 101 102 103 104 105 106 126 127 128 129 130 131 132 133 134 135 136 152 153 154 155 156 157 202 % 97.17/97.28 [65]P1(a1) % 97.17/97.28 [66]P1(a26) % 97.17/97.28 [67]P1(a27) % 97.17/97.28 [68]P1(a28) % 97.17/97.28 [69]P1(a29) % 97.17/97.28 [70]P2(a2) % 97.17/97.28 [71]P5(a2) % 97.17/97.28 [72]P8(a2) % 97.17/97.28 [73]P3(a28,a1,a2) % 97.17/97.28 [74]P3(a29,a1,a2) % 97.17/97.28 [75]P9(a1,a2,a26) % 97.28/97.28 [76]P9(a1,a2,a27) % 97.28/97.28 [77]P10(a28,a2,a26) % 97.28/97.28 [78]P10(a29,a2,a27) % 97.28/97.28 [88]E(a28,a26)+P9(a28,a2,a26) % 97.28/97.28 [89]E(a29,a27)+P9(a29,a2,a27) % 97.28/97.28 [90]P1(a6)+P3(a26,a1,a2) % 97.28/97.28 [91]P1(a16)+P3(a27,a1,a2) % 97.28/97.28 [107]P3(a26,a1,a2)+P3(a6,a1,a2) % 97.28/97.28 [108]P3(a26,a1,a2)+P9(a6,a2,a26) % 97.28/97.28 [109]P3(a27,a1,a2)+P3(a16,a1,a2) % 97.28/97.28 [110]P3(a27,a1,a2)+P9(a16,a2,a27) % 97.28/97.28 [93]E(a28,a26)+P1(a17)+P3(a26,a28,a2) % 97.28/97.28 [94]E(a29,a27)+P1(a18)+P3(a27,a29,a2) % 97.28/97.28 [111]E(a28,a26)+P3(a26,a28,a2)+P3(a17,a28,a2) % 97.28/97.28 [112]P3(a26,a28,a2)+E(a28,a26)+P9(a17,a2,a26) % 97.28/97.28 [113]E(a29,a27)+P3(a27,a29,a2)+P3(a18,a29,a2) % 97.28/97.28 [114]P3(a27,a29,a2)+E(a29,a27)+P9(a18,a2,a27) % 97.28/97.28 [79]~P1(x791)+~E(a29,x791)+~E(a28,x791) % 97.28/97.28 [101]~P1(x1011)+~E(a28,x1011)+~P3(x1011,a29,a2) % 97.28/97.28 [102]~P1(x1021)+~E(a29,x1021)+~P3(x1021,a28,a2) % 97.28/97.28 [103]~P1(x1031)+~E(a28,x1031)+~P9(a29,a2,x1031) % 97.28/97.28 [104]~P1(x1041)+~E(a28,x1041)+~P10(a29,a2,x1041) % 97.28/97.28 [105]~P1(x1051)+~E(a29,x1051)+~P9(a28,a2,x1051) % 97.28/97.28 [106]~P1(x1061)+~E(a29,x1061)+~P10(a28,a2,x1061) % 97.28/97.28 [126]~P1(x1261)+~P3(x1261,a28,a2)+~P3(x1261,a29,a2) % 97.28/97.28 [127]~P1(x1271)+~P3(x1271,a28,a2)+~P9(a29,a2,x1271) % 97.28/97.28 [128]~P1(x1281)+~P3(x1281,a28,a2)+~P10(a29,a2,x1281) % 97.28/97.28 [129]~P1(x1291)+~P3(x1291,a29,a2)+~P9(a28,a2,x1291) % 97.28/97.28 [130]~P1(x1301)+~P3(x1301,a29,a2)+~P10(a28,a2,x1301) % 97.28/97.28 [131]~P1(x1311)+~P9(a28,a2,x1311)+~P9(a29,a2,x1311) % 97.28/97.28 [132]~P1(x1321)+~P9(a28,a2,x1321)+~P10(a29,a2,x1321) % 97.28/97.28 [133]~P1(x1331)+~P9(a29,a2,x1331)+~P10(a28,a2,x1331) % 97.28/97.28 [134]~P1(x1341)+~P10(a28,a2,x1341)+~P10(a29,a2,x1341) % 97.28/97.28 [80]~P2(x801)+P6(x801)+P1(f3(x801)) % 97.28/97.28 [81]~P2(x811)+P6(x811)+P1(f20(x811)) % 97.28/97.28 [82]~P2(x821)+P6(x821)+P1(f21(x821)) % 97.28/97.28 [83]~P2(x831)+P5(x831)+P1(f22(x831)) % 97.28/97.28 [84]~P2(x841)+P5(x841)+P1(f24(x841)) % 97.28/97.28 [85]~P2(x851)+P5(x851)+P1(f25(x851)) % 97.28/97.28 [86]~P2(x861)+P8(x861)+P1(f4(x861)) % 97.28/97.28 [87]~P2(x871)+P8(x871)+P1(f5(x871)) % 97.28/97.28 [92]~P2(x921)+P8(x921)+~P7(f5(x921),f4(x921)) % 97.28/97.28 [95]~P2(x951)+P6(x951)+P10(f3(x951),x951,f20(x951)) % 97.28/97.28 [96]~P2(x961)+P6(x961)+P10(f3(x961),x961,f21(x961)) % 97.28/97.28 [97]~P2(x971)+P8(x971)+P9(f4(x971),x971,f5(x971)) % 97.28/97.28 [98]~P2(x981)+P5(x981)+P3(f24(x981),f22(x981),x981) % 97.28/97.28 [99]~P2(x991)+P5(x991)+P3(f25(x991),f22(x991),x991) % 97.28/97.28 [118]~P1(x1182)+~P1(x1181)+P7(x1181,x1182)+~P3(x1181,x1182,a2) % 97.28/97.28 [119]~P1(x1191)+~P1(x1192)+P7(x1191,x1192)+~P9(x1192,a2,x1191) % 97.28/97.28 [115]~P1(x1152)+~P2(x1151)+~P8(x1151)+P4(f7(x1151,x1152),x1152,x1151) % 97.28/97.28 [116]~P3(x1161,x1162,x1163)+P1(x1161)+~P1(x1162)+~P2(x1163) % 97.28/97.28 [117]~P4(x1171,x1172,x1173)+P1(x1171)+~P1(x1172)+~P2(x1173) % 97.28/97.28 [121]~P1(x1211)+~P2(x1212)+~P4(x1213,x1211,x1212)+P10(x1211,x1212,x1213) % 97.28/97.28 [137]~P4(x1374,x1371,x1372)+~P1(x1371)+~P3(x1373,x1374,x1372)+~P2(x1372) % 97.28/97.28 [135]~P1(x1351)+~P1(x1352)+~P9(x1352,a2,x1351)+~E(a28,x1351)+~P3(x1352,a29,a2) % 97.28/97.28 [136]~P1(x1361)+~P1(x1362)+~P9(x1362,a2,x1361)+~E(a29,x1361)+~P3(x1362,a28,a2) % 97.28/97.28 [152]~P1(x1521)+~P1(x1522)+~P9(x1521,a2,x1522)+~P3(x1521,a28,a2)+~P3(x1522,a29,a2) % 97.28/97.28 [153]~P1(x1531)+~P1(x1532)+~P9(x1532,a2,x1531)+~P3(x1531,a28,a2)+~P3(x1532,a29,a2) % 97.28/97.28 [154]~P1(x1541)+~P1(x1542)+~P9(x1541,a2,x1542)+~P3(x1541,a28,a2)+~P9(a29,a2,x1542) % 97.28/97.28 [155]~P1(x1551)+~P1(x1552)+~P9(x1551,a2,x1552)+~P3(x1551,a28,a2)+~P10(a29,a2,x1552) % 97.28/97.28 [156]~P1(x1561)+~P1(x1562)+~P9(x1562,a2,x1561)+~P3(x1562,a29,a2)+~P9(a28,a2,x1561) % 97.28/97.28 [157]~P1(x1571)+~P1(x1572)+~P9(x1572,a2,x1571)+~P3(x1572,a29,a2)+~P10(a28,a2,x1571) % 97.28/97.28 [141]~P2(x1411)+P6(x1411)+~P1(x1412)+~P10(f20(x1411),x1411,x1412)+~P10(f21(x1411),x1411,x1412) % 97.28/97.28 [142]~P2(x1421)+P5(x1421)+~P1(x1422)+~P10(f24(x1421),x1421,x1422)+~P10(f25(x1421),x1421,x1422) % 97.28/97.28 [100]~E(x1001,x1003)+~P1(x1003)+~P1(x1001)+~P2(x1002)+P10(x1001,x1002,x1003) % 97.28/97.28 [123]~P1(x1231)+~P1(x1233)+~P2(x1232)+~P3(x1233,x1231,x1232)+P9(x1231,x1232,x1233) % 97.28/97.28 [124]~P1(x1243)+~P1(x1241)+~P2(x1242)+~P9(x1241,x1242,x1243)+P10(x1241,x1242,x1243) % 97.28/97.28 [120]~P1(x1201)+~P1(x1202)+~P8(x1203)+~P9(x1202,x1203,x1201)+P7(x1201,x1202)+~P2(x1203) % 97.28/97.28 [125]~P1(x1252)+~P1(x1251)+~P2(x1253)+~P10(x1251,x1253,x1252)+E(x1251,x1252)+P9(x1251,x1253,x1252) % 97.28/97.28 [138]~P1(x1381)+~P1(x1382)+P7(x1381,x1382)+~P1(x1383)+~P3(x1383,x1382,a2)+~P9(x1383,a2,x1381) % 97.28/97.28 [160]~P1(x1601)+~P1(x1602)+~P2(x1603)+~P9(x1602,x1603,x1601)+P3(x1601,x1602,x1603)+P1(f13(x1602,x1603,x1601)) % 97.28/97.28 [173]~P1(x1733)+~P1(x1732)+~P1(x1731)+~P3(x1733,x1731,a2)+~P3(x1732,x1731,a2)+P1(f10(x1731,x1732,x1733)) % 97.28/97.28 [183]~P1(x1831)+~P1(x1832)+~P2(x1833)+~P9(x1832,x1833,x1831)+P3(x1831,x1832,x1833)+P3(f13(x1832,x1833,x1831),x1832,x1833) % 97.28/97.28 [184]~P1(x1841)+~P1(x1842)+~P2(x1843)+~P9(x1842,x1843,x1841)+P3(x1841,x1842,x1843)+P9(f13(x1842,x1843,x1841),x1843,x1841) % 97.28/97.28 [185]~P1(x1852)+~P1(x1851)+~P2(x1853)+~P10(x1852,x1853,x1851)+P4(x1851,x1852,x1853)+P3(f8(x1852,x1853,x1851),x1851,x1853) % 97.28/97.28 [200]~P1(x2003)+~P1(x2002)+~P1(x2001)+~P3(x2003,x2002,a2)+~P3(x2001,x2002,a2)+P10(x2001,a2,f10(x2002,x2003,x2001)) % 97.28/97.28 [201]~P1(x2013)+~P1(x2012)+~P1(x2011)+~P3(x2013,x2012,a2)+~P3(x2011,x2012,a2)+P10(x2011,a2,f10(x2012,x2011,x2013)) % 97.28/97.28 [202]~P1(x2021)+~P1(x2022)+~P1(x2023)+~P9(x2021,a2,x2022)+~P9(x2023,a2,x2022)+~P3(x2021,a28,a2)+~P3(x2023,a29,a2) % 97.28/97.28 [122]~E(x1221,x1223)+~E(x1221,x1222)+~P1(x1223)+~P1(x1222)+~P1(x1221)+~P7(x1221,a1)+P1(f9(x1221,x1222,x1223)) % 97.28/97.28 [139]~E(x1392,x1393)+~E(x1391,x1392)+~P1(x1393)+~P1(x1392)+~P1(x1391)+~P7(x1392,a1)+P10(x1391,a2,f9(x1392,x1393,x1391)) % 97.28/97.28 [140]~E(x1402,x1403)+~E(x1401,x1402)+~P1(x1403)+~P1(x1402)+~P1(x1401)+~P7(x1402,a1)+P10(x1401,a2,f9(x1402,x1401,x1403)) % 97.28/97.28 [143]~E(x1431,x1433)+~P1(x1433)+~P1(x1432)+~P1(x1431)+~P3(x1432,x1431,a2)+~P7(x1431,a1)+P1(f9(x1431,x1432,x1433)) % 97.28/97.28 [144]~E(x1441,x1442)+~P1(x1443)+~P1(x1442)+~P1(x1441)+~P3(x1443,x1441,a2)+~P7(x1441,a1)+P1(f9(x1441,x1442,x1443)) % 97.28/97.28 [145]~E(x1451,x1453)+~P1(x1453)+~P1(x1452)+~P1(x1451)+~P9(x1451,a2,x1452)+~P7(x1451,a1)+P1(f9(x1451,x1452,x1453)) % 97.28/97.28 [146]~E(x1461,x1463)+~P1(x1463)+~P1(x1462)+~P1(x1461)+~P10(x1461,a2,x1462)+~P7(x1461,a1)+P1(f9(x1461,x1462,x1463)) % 97.28/97.28 [147]~E(x1471,x1472)+~P1(x1473)+~P1(x1472)+~P1(x1471)+~P9(x1471,a2,x1473)+~P7(x1471,a1)+P1(f9(x1471,x1472,x1473)) % 97.28/97.28 [148]~E(x1481,x1482)+~P1(x1483)+~P1(x1482)+~P1(x1481)+~P10(x1481,a2,x1483)+~P7(x1481,a1)+P1(f9(x1481,x1482,x1483)) % 97.28/97.28 [161]~E(x1612,x1613)+~P1(x1613)+~P1(x1612)+~P1(x1611)+~P3(x1611,x1612,a2)+~P7(x1612,a1)+P10(x1611,a2,f9(x1612,x1613,x1611)) % 97.28/97.28 [162]~E(x1621,x1622)+~P1(x1623)+~P1(x1622)+~P1(x1621)+~P3(x1623,x1622,a2)+~P7(x1622,a1)+P10(x1621,a2,f9(x1622,x1623,x1621)) % 97.28/97.28 [163]~E(x1632,x1633)+~P1(x1633)+~P1(x1632)+~P1(x1631)+~P3(x1631,x1632,a2)+~P7(x1632,a1)+P10(x1631,a2,f9(x1632,x1631,x1633)) % 97.28/97.28 [164]~E(x1641,x1642)+~P1(x1643)+~P1(x1642)+~P1(x1641)+~P3(x1643,x1642,a2)+~P7(x1642,a1)+P10(x1641,a2,f9(x1642,x1641,x1643)) % 97.28/97.28 [165]~E(x1652,x1653)+~P1(x1653)+~P1(x1652)+~P1(x1651)+~P9(x1652,a2,x1651)+~P7(x1652,a1)+P10(x1651,a2,f9(x1652,x1653,x1651)) % 97.28/97.28 [166]~E(x1662,x1663)+~P1(x1663)+~P1(x1662)+~P1(x1661)+~P10(x1662,a2,x1661)+~P7(x1662,a1)+P10(x1661,a2,f9(x1662,x1663,x1661)) % 97.28/97.28 [167]~E(x1671,x1672)+~P1(x1673)+~P1(x1672)+~P1(x1671)+~P9(x1672,a2,x1673)+~P7(x1672,a1)+P10(x1671,a2,f9(x1672,x1673,x1671)) % 97.28/97.28 [168]~E(x1681,x1682)+~P1(x1683)+~P1(x1682)+~P1(x1681)+~P10(x1682,a2,x1683)+~P7(x1682,a1)+P10(x1681,a2,f9(x1682,x1683,x1681)) % 97.28/97.28 [169]~E(x1692,x1693)+~P1(x1693)+~P1(x1692)+~P1(x1691)+~P9(x1692,a2,x1691)+~P7(x1692,a1)+P10(x1691,a2,f9(x1692,x1691,x1693)) % 97.28/97.28 [170]~E(x1702,x1703)+~P1(x1703)+~P1(x1702)+~P1(x1701)+~P10(x1702,a2,x1701)+~P7(x1702,a1)+P10(x1701,a2,f9(x1702,x1701,x1703)) % 97.28/97.28 [171]~E(x1711,x1712)+~P1(x1713)+~P1(x1712)+~P1(x1711)+~P9(x1712,a2,x1713)+~P7(x1712,a1)+P10(x1711,a2,f9(x1712,x1711,x1713)) % 97.28/97.28 [172]~E(x1721,x1722)+~P1(x1723)+~P1(x1722)+~P1(x1721)+~P10(x1722,a2,x1723)+~P7(x1722,a1)+P10(x1721,a2,f9(x1722,x1721,x1723)) % 97.28/97.28 [174]~P1(x1743)+~P1(x1742)+~P1(x1741)+~P3(x1743,x1741,a2)+~P3(x1742,x1741,a2)+~P7(x1741,a1)+P1(f9(x1741,x1742,x1743)) % 97.28/97.28 [175]~P1(x1753)+~P1(x1752)+~P1(x1751)+~P3(x1753,x1751,a2)+~P9(x1751,a2,x1752)+~P7(x1751,a1)+P1(f9(x1751,x1752,x1753)) % 97.28/97.28 [176]~P1(x1763)+~P1(x1762)+~P1(x1761)+~P3(x1763,x1761,a2)+~P10(x1761,a2,x1762)+~P7(x1761,a1)+P1(f9(x1761,x1762,x1763)) % 97.28/97.28 [177]~P1(x1773)+~P1(x1772)+~P1(x1771)+~P3(x1772,x1771,a2)+~P9(x1771,a2,x1773)+~P7(x1771,a1)+P1(f9(x1771,x1772,x1773)) % 97.28/97.28 [178]~P1(x1783)+~P1(x1782)+~P1(x1781)+~P3(x1782,x1781,a2)+~P10(x1781,a2,x1783)+~P7(x1781,a1)+P1(f9(x1781,x1782,x1783)) % 97.28/97.28 [179]~P1(x1793)+~P1(x1792)+~P1(x1791)+~P9(x1791,a2,x1793)+~P9(x1791,a2,x1792)+~P7(x1791,a1)+P1(f9(x1791,x1792,x1793)) % 97.28/97.28 [180]~P1(x1803)+~P1(x1802)+~P1(x1801)+~P9(x1801,a2,x1803)+~P10(x1801,a2,x1802)+~P7(x1801,a1)+P1(f9(x1801,x1802,x1803)) % 97.28/97.28 [181]~P1(x1813)+~P1(x1812)+~P1(x1811)+~P9(x1811,a2,x1812)+~P10(x1811,a2,x1813)+~P7(x1811,a1)+P1(f9(x1811,x1812,x1813)) % 97.28/97.28 [182]~P1(x1823)+~P1(x1822)+~P1(x1821)+~P10(x1821,a2,x1823)+~P10(x1821,a2,x1822)+~P7(x1821,a1)+P1(f9(x1821,x1822,x1823)) % 97.28/97.28 [203]~P1(x2033)+~P1(x2032)+~P1(x2031)+~P3(x2033,x2032,a2)+~P3(x2031,x2032,a2)+~P7(x2032,a1)+P10(x2031,a2,f9(x2032,x2033,x2031)) % 97.28/97.28 [204]~P1(x2043)+~P1(x2042)+~P1(x2041)+~P3(x2043,x2042,a2)+~P3(x2041,x2042,a2)+~P7(x2042,a1)+P10(x2041,a2,f9(x2042,x2041,x2043)) % 97.28/97.28 [205]~P1(x2053)+~P1(x2052)+~P1(x2051)+~P3(x2053,x2052,a2)+~P9(x2052,a2,x2051)+~P7(x2052,a1)+P10(x2051,a2,f9(x2052,x2053,x2051)) % 97.28/97.28 [206]~P1(x2063)+~P1(x2062)+~P1(x2061)+~P3(x2063,x2062,a2)+~P10(x2062,a2,x2061)+~P7(x2062,a1)+P10(x2061,a2,f9(x2062,x2063,x2061)) % 97.28/97.28 [207]~P1(x2073)+~P1(x2072)+~P1(x2071)+~P3(x2071,x2072,a2)+~P9(x2072,a2,x2073)+~P7(x2072,a1)+P10(x2071,a2,f9(x2072,x2073,x2071)) % 97.28/97.28 [208]~P1(x2083)+~P1(x2082)+~P1(x2081)+~P3(x2081,x2082,a2)+~P10(x2082,a2,x2083)+~P7(x2082,a1)+P10(x2081,a2,f9(x2082,x2083,x2081)) % 97.28/97.28 [209]~P1(x2093)+~P1(x2092)+~P1(x2091)+~P3(x2093,x2092,a2)+~P9(x2092,a2,x2091)+~P7(x2092,a1)+P10(x2091,a2,f9(x2092,x2091,x2093)) % 97.28/97.28 [210]~P1(x2103)+~P1(x2102)+~P1(x2101)+~P3(x2103,x2102,a2)+~P10(x2102,a2,x2101)+~P7(x2102,a1)+P10(x2101,a2,f9(x2102,x2101,x2103)) % 97.28/97.28 [211]~P1(x2113)+~P1(x2112)+~P1(x2111)+~P3(x2111,x2112,a2)+~P9(x2112,a2,x2113)+~P7(x2112,a1)+P10(x2111,a2,f9(x2112,x2111,x2113)) % 97.28/97.28 [212]~P1(x2123)+~P1(x2122)+~P1(x2121)+~P3(x2121,x2122,a2)+~P10(x2122,a2,x2123)+~P7(x2122,a1)+P10(x2121,a2,f9(x2122,x2121,x2123)) % 97.28/97.28 [213]~P1(x2133)+~P1(x2132)+~P1(x2131)+~P9(x2132,a2,x2133)+~P9(x2132,a2,x2131)+~P7(x2132,a1)+P10(x2131,a2,f9(x2132,x2133,x2131)) % 97.28/97.28 [214]~P1(x2143)+~P1(x2142)+~P1(x2141)+~P9(x2142,a2,x2143)+~P10(x2142,a2,x2141)+~P7(x2142,a1)+P10(x2141,a2,f9(x2142,x2143,x2141)) % 97.28/97.28 [215]~P1(x2153)+~P1(x2152)+~P1(x2151)+~P9(x2152,a2,x2151)+~P10(x2152,a2,x2153)+~P7(x2152,a1)+P10(x2151,a2,f9(x2152,x2153,x2151)) % 97.28/97.29 [216]~P1(x2163)+~P1(x2162)+~P1(x2161)+~P10(x2162,a2,x2163)+~P10(x2162,a2,x2161)+~P7(x2162,a1)+P10(x2161,a2,f9(x2162,x2163,x2161)) % 97.28/97.29 [217]~P1(x2173)+~P1(x2172)+~P1(x2171)+~P9(x2172,a2,x2173)+~P9(x2172,a2,x2171)+~P7(x2172,a1)+P10(x2171,a2,f9(x2172,x2171,x2173)) % 97.28/97.29 [218]~P1(x2183)+~P1(x2182)+~P1(x2181)+~P9(x2182,a2,x2183)+~P10(x2182,a2,x2181)+~P7(x2182,a1)+P10(x2181,a2,f9(x2182,x2181,x2183)) % 97.28/97.29 [219]~P1(x2193)+~P1(x2192)+~P1(x2191)+~P9(x2192,a2,x2191)+~P10(x2192,a2,x2193)+~P7(x2192,a1)+P10(x2191,a2,f9(x2192,x2191,x2193)) % 97.28/97.29 [220]~P1(x2203)+~P1(x2202)+~P1(x2201)+~P10(x2202,a2,x2203)+~P10(x2202,a2,x2201)+~P7(x2202,a1)+P10(x2201,a2,f9(x2202,x2201,x2203)) % 97.28/97.29 [227]~P1(x2272)+~P1(x2271)+~P1(x2273)+~P3(x2272,x2271,a2)+~P3(x2273,x2271,a2)+E(f10(x2271,x2272,x2273),x2273)+P9(x2273,a2,f10(x2271,x2272,x2273)) % 97.28/97.29 [228]~P1(x2283)+~P1(x2281)+~P1(x2282)+~P3(x2283,x2281,a2)+~P3(x2282,x2281,a2)+E(f10(x2281,x2282,x2283),x2282)+P9(x2282,a2,f10(x2281,x2282,x2283)) % 97.28/97.29 [149]~P1(x1493)+~P1(x1491)+~P2(x1492)+~P3(x1494,x1491,x1492)+~P9(x1494,x1492,x1493)+P9(x1491,x1492,x1493)+~P1(x1494) % 97.28/97.29 [150]~P1(x1503)+~P1(x1501)+~P2(x1502)+~P9(x1504,x1502,x1503)+~P9(x1501,x1502,x1504)+P9(x1501,x1502,x1503)+~P1(x1504) % 97.28/97.29 [151]~P1(x1513)+~P1(x1511)+~P2(x1512)+~P10(x1514,x1512,x1513)+~P10(x1511,x1512,x1514)+P10(x1511,x1512,x1513)+~P1(x1514) % 97.28/97.29 [158]~E(x1581,x1582)+~E(x1583,x1581)+~P1(x1582)+~P1(x1581)+~P1(x1583)+~P7(x1581,a1)+E(f9(x1581,x1582,x1583),x1583)+P9(x1583,a2,f9(x1581,x1582,x1583)) % 97.28/97.29 [159]~E(x1591,x1593)+~E(x1592,x1591)+~P1(x1593)+~P1(x1591)+~P1(x1592)+~P7(x1591,a1)+E(f9(x1591,x1592,x1593),x1592)+P9(x1592,a2,f9(x1591,x1592,x1593)) % 97.28/97.29 [188]~E(x1881,x1882)+~P1(x1882)+~P1(x1881)+~P1(x1883)+~P3(x1883,x1881,a2)+~P7(x1881,a1)+E(f9(x1881,x1882,x1883),x1883)+P9(x1883,a2,f9(x1881,x1882,x1883)) % 97.28/97.29 [189]~E(x1893,x1891)+~P1(x1892)+~P1(x1891)+~P1(x1893)+~P3(x1892,x1891,a2)+~P7(x1891,a1)+E(f9(x1891,x1892,x1893),x1893)+P9(x1893,a2,f9(x1891,x1892,x1893)) % 97.28/97.29 [190]~E(x1901,x1903)+~P1(x1903)+~P1(x1901)+~P1(x1902)+~P3(x1902,x1901,a2)+~P7(x1901,a1)+E(f9(x1901,x1902,x1903),x1902)+P9(x1902,a2,f9(x1901,x1902,x1903)) % 97.28/97.29 [191]~E(x1912,x1911)+~P1(x1913)+~P1(x1911)+~P1(x1912)+~P3(x1913,x1911,a2)+~P7(x1911,a1)+E(f9(x1911,x1912,x1913),x1912)+P9(x1912,a2,f9(x1911,x1912,x1913)) % 97.28/97.29 [192]~E(x1921,x1922)+~P1(x1922)+~P1(x1921)+~P1(x1923)+~P9(x1921,a2,x1923)+~P7(x1921,a1)+E(f9(x1921,x1922,x1923),x1923)+P9(x1923,a2,f9(x1921,x1922,x1923)) % 97.28/97.29 [193]~E(x1931,x1932)+~P1(x1932)+~P1(x1931)+~P1(x1933)+~P10(x1931,a2,x1933)+~P7(x1931,a1)+E(f9(x1931,x1932,x1933),x1933)+P9(x1933,a2,f9(x1931,x1932,x1933)) % 97.28/97.29 [194]~E(x1943,x1941)+~P1(x1942)+~P1(x1941)+~P1(x1943)+~P9(x1941,a2,x1942)+~P7(x1941,a1)+E(f9(x1941,x1942,x1943),x1943)+P9(x1943,a2,f9(x1941,x1942,x1943)) % 97.28/97.29 [195]~E(x1953,x1951)+~P1(x1952)+~P1(x1951)+~P1(x1953)+~P10(x1951,a2,x1952)+~P7(x1951,a1)+E(f9(x1951,x1952,x1953),x1953)+P9(x1953,a2,f9(x1951,x1952,x1953)) % 97.28/97.29 [196]~E(x1961,x1963)+~P1(x1963)+~P1(x1961)+~P1(x1962)+~P9(x1961,a2,x1962)+~P7(x1961,a1)+E(f9(x1961,x1962,x1963),x1962)+P9(x1962,a2,f9(x1961,x1962,x1963)) % 97.28/97.29 [197]~E(x1971,x1973)+~P1(x1973)+~P1(x1971)+~P1(x1972)+~P10(x1971,a2,x1972)+~P7(x1971,a1)+E(f9(x1971,x1972,x1973),x1972)+P9(x1972,a2,f9(x1971,x1972,x1973)) % 97.28/97.29 [198]~E(x1982,x1981)+~P1(x1983)+~P1(x1981)+~P1(x1982)+~P9(x1981,a2,x1983)+~P7(x1981,a1)+E(f9(x1981,x1982,x1983),x1982)+P9(x1982,a2,f9(x1981,x1982,x1983)) % 97.28/97.29 [199]~E(x1992,x1991)+~P1(x1993)+~P1(x1991)+~P1(x1992)+~P10(x1991,a2,x1993)+~P7(x1991,a1)+E(f9(x1991,x1992,x1993),x1992)+P9(x1992,a2,f9(x1991,x1992,x1993)) % 97.28/97.29 [237]~P1(x2372)+~P1(x2371)+~P1(x2373)+~P3(x2372,x2371,a2)+~P3(x2373,x2371,a2)+~P7(x2371,a1)+E(f9(x2371,x2372,x2373),x2373)+P9(x2373,a2,f9(x2371,x2372,x2373)) % 97.28/97.29 [238]~P1(x2383)+~P1(x2381)+~P1(x2382)+~P3(x2383,x2381,a2)+~P3(x2382,x2381,a2)+~P7(x2381,a1)+E(f9(x2381,x2382,x2383),x2382)+P9(x2382,a2,f9(x2381,x2382,x2383)) % 97.28/97.29 [239]~P1(x2392)+~P1(x2391)+~P1(x2393)+~P3(x2392,x2391,a2)+~P9(x2391,a2,x2393)+~P7(x2391,a1)+E(f9(x2391,x2392,x2393),x2393)+P9(x2393,a2,f9(x2391,x2392,x2393)) % 97.28/97.29 [240]~P1(x2402)+~P1(x2401)+~P1(x2403)+~P3(x2402,x2401,a2)+~P10(x2401,a2,x2403)+~P7(x2401,a1)+E(f9(x2401,x2402,x2403),x2403)+P9(x2403,a2,f9(x2401,x2402,x2403)) % 97.28/97.29 [241]~P1(x2412)+~P1(x2411)+~P1(x2413)+~P3(x2413,x2411,a2)+~P9(x2411,a2,x2412)+~P7(x2411,a1)+E(f9(x2411,x2412,x2413),x2413)+P9(x2413,a2,f9(x2411,x2412,x2413)) % 97.28/97.29 [242]~P1(x2422)+~P1(x2421)+~P1(x2423)+~P3(x2423,x2421,a2)+~P10(x2421,a2,x2422)+~P7(x2421,a1)+E(f9(x2421,x2422,x2423),x2423)+P9(x2423,a2,f9(x2421,x2422,x2423)) % 97.28/97.29 [243]~P1(x2433)+~P1(x2431)+~P1(x2432)+~P3(x2433,x2431,a2)+~P9(x2431,a2,x2432)+~P7(x2431,a1)+E(f9(x2431,x2432,x2433),x2432)+P9(x2432,a2,f9(x2431,x2432,x2433)) % 97.28/97.29 [244]~P1(x2443)+~P1(x2441)+~P1(x2442)+~P3(x2443,x2441,a2)+~P10(x2441,a2,x2442)+~P7(x2441,a1)+E(f9(x2441,x2442,x2443),x2442)+P9(x2442,a2,f9(x2441,x2442,x2443)) % 97.28/97.29 [245]~P1(x2453)+~P1(x2451)+~P1(x2452)+~P3(x2452,x2451,a2)+~P9(x2451,a2,x2453)+~P7(x2451,a1)+E(f9(x2451,x2452,x2453),x2452)+P9(x2452,a2,f9(x2451,x2452,x2453)) % 97.28/97.29 [246]~P1(x2463)+~P1(x2461)+~P1(x2462)+~P3(x2462,x2461,a2)+~P10(x2461,a2,x2463)+~P7(x2461,a1)+E(f9(x2461,x2462,x2463),x2462)+P9(x2462,a2,f9(x2461,x2462,x2463)) % 97.28/97.29 [247]~P1(x2472)+~P1(x2471)+~P1(x2473)+~P9(x2471,a2,x2472)+~P9(x2471,a2,x2473)+~P7(x2471,a1)+E(f9(x2471,x2472,x2473),x2473)+P9(x2473,a2,f9(x2471,x2472,x2473)) % 97.28/97.29 [248]~P1(x2482)+~P1(x2481)+~P1(x2483)+~P9(x2481,a2,x2482)+~P10(x2481,a2,x2483)+~P7(x2481,a1)+E(f9(x2481,x2482,x2483),x2483)+P9(x2483,a2,f9(x2481,x2482,x2483)) % 97.28/97.29 [249]~P1(x2492)+~P1(x2491)+~P1(x2493)+~P9(x2491,a2,x2493)+~P10(x2491,a2,x2492)+~P7(x2491,a1)+E(f9(x2491,x2492,x2493),x2493)+P9(x2493,a2,f9(x2491,x2492,x2493)) % 97.28/97.29 [250]~P1(x2502)+~P1(x2501)+~P1(x2503)+~P10(x2501,a2,x2502)+~P10(x2501,a2,x2503)+~P7(x2501,a1)+E(f9(x2501,x2502,x2503),x2503)+P9(x2503,a2,f9(x2501,x2502,x2503)) % 97.28/97.29 [251]~P1(x2513)+~P1(x2511)+~P1(x2512)+~P9(x2511,a2,x2513)+~P9(x2511,a2,x2512)+~P7(x2511,a1)+E(f9(x2511,x2512,x2513),x2512)+P9(x2512,a2,f9(x2511,x2512,x2513)) % 97.28/97.29 [252]~P1(x2523)+~P1(x2521)+~P1(x2522)+~P9(x2521,a2,x2523)+~P10(x2521,a2,x2522)+~P7(x2521,a1)+E(f9(x2521,x2522,x2523),x2522)+P9(x2522,a2,f9(x2521,x2522,x2523)) % 97.28/97.29 [253]~P1(x2533)+~P1(x2531)+~P1(x2532)+~P9(x2531,a2,x2532)+~P10(x2531,a2,x2533)+~P7(x2531,a1)+E(f9(x2531,x2532,x2533),x2532)+P9(x2532,a2,f9(x2531,x2532,x2533)) % 97.28/97.29 [254]~P1(x2543)+~P1(x2541)+~P1(x2542)+~P10(x2541,a2,x2543)+~P10(x2541,a2,x2542)+~P7(x2541,a1)+E(f9(x2541,x2542,x2543),x2542)+P9(x2542,a2,f9(x2541,x2542,x2543)) % 97.28/97.29 [296]~P1(x2963)+~P1(x2962)+~P1(x2961)+~P3(x2963,x2961,a2)+~P3(x2962,x2961,a2)+E(f10(x2961,x2962,x2963),x2963)+P3(f10(x2961,x2962,x2963),x2963,a2)+P1(f11(x2961,x2962,x2963)) % 97.28/97.29 [297]~P1(x2973)+~P1(x2972)+~P1(x2971)+~P3(x2973,x2971,a2)+~P3(x2972,x2971,a2)+E(f10(x2971,x2972,x2973),x2972)+P3(f10(x2971,x2972,x2973),x2972,a2)+P1(f12(x2971,x2972,x2973)) % 97.28/97.29 [336]~P1(x3363)+~P1(x3362)+~P1(x3361)+~P3(x3363,x3361,a2)+~P3(x3362,x3361,a2)+E(f10(x3361,x3362,x3363),x3363)+P3(f11(x3361,x3362,x3363),x3363,a2)+P3(f10(x3361,x3362,x3363),x3363,a2) % 97.28/97.29 [337]~P1(x3373)+~P1(x3372)+~P1(x3371)+~P3(x3373,x3371,a2)+~P3(x3372,x3371,a2)+E(f10(x3371,x3372,x3373),x3372)+P3(f12(x3371,x3372,x3373),x3372,a2)+P3(f10(x3371,x3372,x3373),x3372,a2) % 97.28/97.29 [386]~P1(x3863)+~P1(x3862)+~P1(x3861)+~P3(x3863,x3861,a2)+~P3(x3862,x3861,a2)+E(f10(x3861,x3862,x3863),x3863)+P9(f11(x3861,x3862,x3863),a2,f10(x3861,x3862,x3863))+P3(f10(x3861,x3862,x3863),x3863,a2) % 97.28/97.29 [387]~P1(x3873)+~P1(x3872)+~P1(x3871)+~P3(x3873,x3871,a2)+~P3(x3872,x3871,a2)+E(f10(x3871,x3872,x3873),x3872)+P9(f12(x3871,x3872,x3873),a2,f10(x3871,x3872,x3873))+P3(f10(x3871,x3872,x3873),x3872,a2) % 97.28/97.29 [422]~P1(x4224)+~P1(x4223)+~P1(x4222)+~P2(x4221)+~P6(x4221)+~P10(x4222,x4221,x4224)+~P10(x4222,x4221,x4223)+P1(f19(x4221,x4222,x4223,x4224)) % 97.28/97.29 [423]~P1(x4234)+~P1(x4233)+~P1(x4232)+~P2(x4231)+~P5(x4231)+~P3(x4234,x4232,x4231)+~P3(x4233,x4232,x4231)+P1(f23(x4231,x4232,x4233,x4234)) % 97.28/97.29 [426]~P1(x4264)+~P1(x4263)+~P1(x4261)+~P2(x4262)+~P6(x4262)+~P10(x4263,x4262,x4264)+~P10(x4263,x4262,x4261)+P10(x4261,x4262,f19(x4262,x4263,x4264,x4261)) % 97.28/97.29 [427]~P1(x4274)+~P1(x4273)+~P1(x4271)+~P2(x4272)+~P6(x4272)+~P10(x4273,x4272,x4274)+~P10(x4273,x4272,x4271)+P10(x4271,x4272,f19(x4272,x4273,x4271,x4274)) % 97.28/97.29 [428]~P1(x4284)+~P1(x4283)+~P1(x4281)+~P2(x4282)+~P5(x4282)+~P3(x4284,x4283,x4282)+~P3(x4281,x4283,x4282)+P10(x4281,x4282,f23(x4282,x4283,x4284,x4281)) % 97.28/97.29 [429]~P1(x4294)+~P1(x4293)+~P1(x4291)+~P2(x4292)+~P5(x4292)+~P3(x4294,x4293,x4292)+~P3(x4291,x4293,x4292)+P10(x4291,x4292,f23(x4292,x4293,x4291,x4294)) % 97.28/97.29 [221]~E(x2211,x2213)+~E(x2211,x2212)+~P1(x2213)+~P1(x2212)+~P1(x2211)+~P7(x2211,a1)+E(f9(x2211,x2212,x2213),x2213)+P3(f9(x2211,x2212,x2213),x2213,a2)+P1(f14(x2211,x2212,x2213)) % 97.28/97.29 [222]~E(x2221,x2223)+~E(x2221,x2222)+~P1(x2223)+~P1(x2222)+~P1(x2221)+~P7(x2221,a1)+E(f9(x2221,x2222,x2223),x2222)+P3(f9(x2221,x2222,x2223),x2222,a2)+P1(f15(x2221,x2222,x2223)) % 97.28/97.29 [235]~E(x2351,x2353)+~E(x2351,x2352)+~P1(x2353)+~P1(x2352)+~P1(x2351)+~P7(x2351,a1)+E(f9(x2351,x2352,x2353),x2353)+P3(f14(x2351,x2352,x2353),x2353,a2)+P3(f9(x2351,x2352,x2353),x2353,a2) % 97.28/97.29 [236]~E(x2361,x2363)+~E(x2361,x2362)+~P1(x2363)+~P1(x2362)+~P1(x2361)+~P7(x2361,a1)+E(f9(x2361,x2362,x2363),x2362)+P3(f15(x2361,x2362,x2363),x2362,a2)+P3(f9(x2361,x2362,x2363),x2362,a2) % 97.28/97.29 [259]~E(x2591,x2593)+~P1(x2593)+~P1(x2592)+~P1(x2591)+~P3(x2592,x2591,a2)+~P7(x2591,a1)+E(f9(x2591,x2592,x2593),x2593)+P3(f9(x2591,x2592,x2593),x2593,a2)+P1(f14(x2591,x2592,x2593)) % 97.28/97.29 [260]~E(x2601,x2602)+~P1(x2603)+~P1(x2602)+~P1(x2601)+~P3(x2603,x2601,a2)+~P7(x2601,a1)+E(f9(x2601,x2602,x2603),x2603)+P3(f9(x2601,x2602,x2603),x2603,a2)+P1(f14(x2601,x2602,x2603)) % 97.28/97.29 [261]~E(x2611,x2613)+~P1(x2613)+~P1(x2612)+~P1(x2611)+~P3(x2612,x2611,a2)+~P7(x2611,a1)+E(f9(x2611,x2612,x2613),x2612)+P3(f9(x2611,x2612,x2613),x2612,a2)+P1(f15(x2611,x2612,x2613)) % 97.28/97.29 [262]~E(x2621,x2622)+~P1(x2623)+~P1(x2622)+~P1(x2621)+~P3(x2623,x2621,a2)+~P7(x2621,a1)+E(f9(x2621,x2622,x2623),x2622)+P3(f9(x2621,x2622,x2623),x2622,a2)+P1(f15(x2621,x2622,x2623)) % 97.28/97.29 [263]~E(x2631,x2633)+~P1(x2633)+~P1(x2632)+~P1(x2631)+~P9(x2631,a2,x2632)+~P7(x2631,a1)+E(f9(x2631,x2632,x2633),x2633)+P3(f9(x2631,x2632,x2633),x2633,a2)+P1(f14(x2631,x2632,x2633)) % 97.28/97.29 [264]~E(x2641,x2643)+~P1(x2643)+~P1(x2642)+~P1(x2641)+~P10(x2641,a2,x2642)+~P7(x2641,a1)+E(f9(x2641,x2642,x2643),x2643)+P3(f9(x2641,x2642,x2643),x2643,a2)+P1(f14(x2641,x2642,x2643)) % 97.28/97.29 [265]~E(x2651,x2652)+~P1(x2653)+~P1(x2652)+~P1(x2651)+~P9(x2651,a2,x2653)+~P7(x2651,a1)+E(f9(x2651,x2652,x2653),x2653)+P3(f9(x2651,x2652,x2653),x2653,a2)+P1(f14(x2651,x2652,x2653)) % 97.28/97.29 [266]~E(x2661,x2662)+~P1(x2663)+~P1(x2662)+~P1(x2661)+~P10(x2661,a2,x2663)+~P7(x2661,a1)+E(f9(x2661,x2662,x2663),x2663)+P3(f9(x2661,x2662,x2663),x2663,a2)+P1(f14(x2661,x2662,x2663)) % 97.28/97.29 [267]~E(x2671,x2673)+~P1(x2673)+~P1(x2672)+~P1(x2671)+~P9(x2671,a2,x2672)+~P7(x2671,a1)+E(f9(x2671,x2672,x2673),x2672)+P3(f9(x2671,x2672,x2673),x2672,a2)+P1(f15(x2671,x2672,x2673)) % 97.28/97.29 [268]~E(x2681,x2683)+~P1(x2683)+~P1(x2682)+~P1(x2681)+~P10(x2681,a2,x2682)+~P7(x2681,a1)+E(f9(x2681,x2682,x2683),x2682)+P3(f9(x2681,x2682,x2683),x2682,a2)+P1(f15(x2681,x2682,x2683)) % 97.28/97.29 [269]~E(x2691,x2692)+~P1(x2693)+~P1(x2692)+~P1(x2691)+~P9(x2691,a2,x2693)+~P7(x2691,a1)+E(f9(x2691,x2692,x2693),x2692)+P3(f9(x2691,x2692,x2693),x2692,a2)+P1(f15(x2691,x2692,x2693)) % 97.28/97.29 [270]~E(x2701,x2702)+~P1(x2703)+~P1(x2702)+~P1(x2701)+~P10(x2701,a2,x2703)+~P7(x2701,a1)+E(f9(x2701,x2702,x2703),x2702)+P3(f9(x2701,x2702,x2703),x2702,a2)+P1(f15(x2701,x2702,x2703)) % 97.28/97.29 [284]~E(x2841,x2843)+~P1(x2843)+~P1(x2842)+~P1(x2841)+~P3(x2842,x2841,a2)+~P7(x2841,a1)+E(f9(x2841,x2842,x2843),x2843)+P3(f14(x2841,x2842,x2843),x2843,a2)+P3(f9(x2841,x2842,x2843),x2843,a2) % 97.28/97.29 [285]~E(x2851,x2852)+~P1(x2853)+~P1(x2852)+~P1(x2851)+~P3(x2853,x2851,a2)+~P7(x2851,a1)+E(f9(x2851,x2852,x2853),x2853)+P3(f14(x2851,x2852,x2853),x2853,a2)+P3(f9(x2851,x2852,x2853),x2853,a2) % 97.28/97.29 [286]~E(x2861,x2863)+~P1(x2863)+~P1(x2862)+~P1(x2861)+~P3(x2862,x2861,a2)+~P7(x2861,a1)+E(f9(x2861,x2862,x2863),x2862)+P3(f15(x2861,x2862,x2863),x2862,a2)+P3(f9(x2861,x2862,x2863),x2862,a2) % 97.28/97.29 [287]~E(x2871,x2872)+~P1(x2873)+~P1(x2872)+~P1(x2871)+~P3(x2873,x2871,a2)+~P7(x2871,a1)+E(f9(x2871,x2872,x2873),x2872)+P3(f15(x2871,x2872,x2873),x2872,a2)+P3(f9(x2871,x2872,x2873),x2872,a2) % 97.28/97.29 [288]~E(x2881,x2883)+~P1(x2883)+~P1(x2882)+~P1(x2881)+~P9(x2881,a2,x2882)+~P7(x2881,a1)+E(f9(x2881,x2882,x2883),x2883)+P3(f14(x2881,x2882,x2883),x2883,a2)+P3(f9(x2881,x2882,x2883),x2883,a2) % 97.28/97.29 [289]~E(x2891,x2893)+~P1(x2893)+~P1(x2892)+~P1(x2891)+~P10(x2891,a2,x2892)+~P7(x2891,a1)+E(f9(x2891,x2892,x2893),x2893)+P3(f14(x2891,x2892,x2893),x2893,a2)+P3(f9(x2891,x2892,x2893),x2893,a2) % 97.28/97.29 [290]~E(x2901,x2902)+~P1(x2903)+~P1(x2902)+~P1(x2901)+~P9(x2901,a2,x2903)+~P7(x2901,a1)+E(f9(x2901,x2902,x2903),x2903)+P3(f14(x2901,x2902,x2903),x2903,a2)+P3(f9(x2901,x2902,x2903),x2903,a2) % 97.28/97.29 [291]~E(x2911,x2912)+~P1(x2913)+~P1(x2912)+~P1(x2911)+~P10(x2911,a2,x2913)+~P7(x2911,a1)+E(f9(x2911,x2912,x2913),x2913)+P3(f14(x2911,x2912,x2913),x2913,a2)+P3(f9(x2911,x2912,x2913),x2913,a2) % 97.28/97.29 [292]~E(x2921,x2923)+~P1(x2923)+~P1(x2922)+~P1(x2921)+~P9(x2921,a2,x2922)+~P7(x2921,a1)+E(f9(x2921,x2922,x2923),x2922)+P3(f15(x2921,x2922,x2923),x2922,a2)+P3(f9(x2921,x2922,x2923),x2922,a2) % 97.28/97.29 [293]~E(x2931,x2933)+~P1(x2933)+~P1(x2932)+~P1(x2931)+~P10(x2931,a2,x2932)+~P7(x2931,a1)+E(f9(x2931,x2932,x2933),x2932)+P3(f15(x2931,x2932,x2933),x2932,a2)+P3(f9(x2931,x2932,x2933),x2932,a2) % 97.28/97.29 [294]~E(x2941,x2942)+~P1(x2943)+~P1(x2942)+~P1(x2941)+~P9(x2941,a2,x2943)+~P7(x2941,a1)+E(f9(x2941,x2942,x2943),x2942)+P3(f15(x2941,x2942,x2943),x2942,a2)+P3(f9(x2941,x2942,x2943),x2942,a2) % 97.28/97.29 [295]~E(x2951,x2952)+~P1(x2953)+~P1(x2952)+~P1(x2951)+~P10(x2951,a2,x2953)+~P7(x2951,a1)+E(f9(x2951,x2952,x2953),x2952)+P3(f15(x2951,x2952,x2953),x2952,a2)+P3(f9(x2951,x2952,x2953),x2952,a2) % 97.28/97.29 [310]~E(x3101,x3103)+~E(x3101,x3102)+~P1(x3103)+~P1(x3102)+~P1(x3101)+~P7(x3101,a1)+E(f9(x3101,x3102,x3103),x3103)+P9(f14(x3101,x3102,x3103),a2,f9(x3101,x3102,x3103))+P3(f9(x3101,x3102,x3103),x3103,a2) % 97.28/97.29 [311]~E(x3111,x3113)+~E(x3111,x3112)+~P1(x3113)+~P1(x3112)+~P1(x3111)+~P7(x3111,a1)+E(f9(x3111,x3112,x3113),x3112)+P9(f15(x3111,x3112,x3113),a2,f9(x3111,x3112,x3113))+P3(f9(x3111,x3112,x3113),x3112,a2) % 97.28/97.29 [312]~P1(x3123)+~P1(x3122)+~P1(x3121)+~P3(x3123,x3121,a2)+~P3(x3122,x3121,a2)+~P7(x3121,a1)+E(f9(x3121,x3122,x3123),x3123)+P3(f9(x3121,x3122,x3123),x3123,a2)+P1(f14(x3121,x3122,x3123)) % 97.28/97.29 [313]~P1(x3133)+~P1(x3132)+~P1(x3131)+~P3(x3133,x3131,a2)+~P3(x3132,x3131,a2)+~P7(x3131,a1)+E(f9(x3131,x3132,x3133),x3132)+P3(f9(x3131,x3132,x3133),x3132,a2)+P1(f15(x3131,x3132,x3133)) % 97.28/97.29 [314]~P1(x3143)+~P1(x3142)+~P1(x3141)+~P3(x3143,x3141,a2)+~P9(x3141,a2,x3142)+~P7(x3141,a1)+E(f9(x3141,x3142,x3143),x3143)+P3(f9(x3141,x3142,x3143),x3143,a2)+P1(f14(x3141,x3142,x3143)) % 97.28/97.29 [315]~P1(x3153)+~P1(x3152)+~P1(x3151)+~P3(x3153,x3151,a2)+~P10(x3151,a2,x3152)+~P7(x3151,a1)+E(f9(x3151,x3152,x3153),x3153)+P3(f9(x3151,x3152,x3153),x3153,a2)+P1(f14(x3151,x3152,x3153)) % 97.28/97.29 [316]~P1(x3163)+~P1(x3162)+~P1(x3161)+~P3(x3162,x3161,a2)+~P9(x3161,a2,x3163)+~P7(x3161,a1)+E(f9(x3161,x3162,x3163),x3163)+P3(f9(x3161,x3162,x3163),x3163,a2)+P1(f14(x3161,x3162,x3163)) % 97.28/97.29 [317]~P1(x3173)+~P1(x3172)+~P1(x3171)+~P3(x3172,x3171,a2)+~P10(x3171,a2,x3173)+~P7(x3171,a1)+E(f9(x3171,x3172,x3173),x3173)+P3(f9(x3171,x3172,x3173),x3173,a2)+P1(f14(x3171,x3172,x3173)) % 97.28/97.29 [318]~P1(x3183)+~P1(x3182)+~P1(x3181)+~P3(x3183,x3181,a2)+~P9(x3181,a2,x3182)+~P7(x3181,a1)+E(f9(x3181,x3182,x3183),x3182)+P3(f9(x3181,x3182,x3183),x3182,a2)+P1(f15(x3181,x3182,x3183)) % 97.28/97.29 [319]~P1(x3193)+~P1(x3192)+~P1(x3191)+~P3(x3193,x3191,a2)+~P10(x3191,a2,x3192)+~P7(x3191,a1)+E(f9(x3191,x3192,x3193),x3192)+P3(f9(x3191,x3192,x3193),x3192,a2)+P1(f15(x3191,x3192,x3193)) % 97.28/97.29 [320]~P1(x3203)+~P1(x3202)+~P1(x3201)+~P3(x3202,x3201,a2)+~P9(x3201,a2,x3203)+~P7(x3201,a1)+E(f9(x3201,x3202,x3203),x3202)+P3(f9(x3201,x3202,x3203),x3202,a2)+P1(f15(x3201,x3202,x3203)) % 97.28/97.29 [321]~P1(x3213)+~P1(x3212)+~P1(x3211)+~P3(x3212,x3211,a2)+~P10(x3211,a2,x3213)+~P7(x3211,a1)+E(f9(x3211,x3212,x3213),x3212)+P3(f9(x3211,x3212,x3213),x3212,a2)+P1(f15(x3211,x3212,x3213)) % 97.28/97.29 [322]~P1(x3223)+~P1(x3222)+~P1(x3221)+~P9(x3221,a2,x3223)+~P9(x3221,a2,x3222)+~P7(x3221,a1)+E(f9(x3221,x3222,x3223),x3223)+P3(f9(x3221,x3222,x3223),x3223,a2)+P1(f14(x3221,x3222,x3223)) % 97.28/97.29 [323]~P1(x3233)+~P1(x3232)+~P1(x3231)+~P9(x3231,a2,x3233)+~P10(x3231,a2,x3232)+~P7(x3231,a1)+E(f9(x3231,x3232,x3233),x3233)+P3(f9(x3231,x3232,x3233),x3233,a2)+P1(f14(x3231,x3232,x3233)) % 97.28/97.29 [324]~P1(x3243)+~P1(x3242)+~P1(x3241)+~P9(x3241,a2,x3242)+~P10(x3241,a2,x3243)+~P7(x3241,a1)+E(f9(x3241,x3242,x3243),x3243)+P3(f9(x3241,x3242,x3243),x3243,a2)+P1(f14(x3241,x3242,x3243)) % 97.28/97.29 [325]~P1(x3253)+~P1(x3252)+~P1(x3251)+~P10(x3251,a2,x3253)+~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)) % 97.28/97.29 [326]~P1(x3263)+~P1(x3262)+~P1(x3261)+~P9(x3261,a2,x3263)+~P9(x3261,a2,x3262)+~P7(x3261,a1)+E(f9(x3261,x3262,x3263),x3262)+P3(f9(x3261,x3262,x3263),x3262,a2)+P1(f15(x3261,x3262,x3263)) % 97.28/97.29 [327]~P1(x3273)+~P1(x3272)+~P1(x3271)+~P9(x3271,a2,x3273)+~P10(x3271,a2,x3272)+~P7(x3271,a1)+E(f9(x3271,x3272,x3273),x3272)+P3(f9(x3271,x3272,x3273),x3272,a2)+P1(f15(x3271,x3272,x3273)) % 97.28/97.29 [328]~P1(x3283)+~P1(x3282)+~P1(x3281)+~P9(x3281,a2,x3282)+~P10(x3281,a2,x3283)+~P7(x3281,a1)+E(f9(x3281,x3282,x3283),x3282)+P3(f9(x3281,x3282,x3283),x3282,a2)+P1(f15(x3281,x3282,x3283)) % 97.28/97.29 [329]~P1(x3293)+~P1(x3292)+~P1(x3291)+~P10(x3291,a2,x3293)+~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)) % 97.28/97.29 [338]~P1(x3383)+~P1(x3382)+~P1(x3381)+~P3(x3383,x3381,a2)+~P3(x3382,x3381,a2)+~P7(x3381,a1)+E(f9(x3381,x3382,x3383),x3383)+P3(f14(x3381,x3382,x3383),x3383,a2)+P3(f9(x3381,x3382,x3383),x3383,a2) % 97.28/97.29 [339]~P1(x3393)+~P1(x3392)+~P1(x3391)+~P3(x3393,x3391,a2)+~P3(x3392,x3391,a2)+~P7(x3391,a1)+E(f9(x3391,x3392,x3393),x3392)+P3(f15(x3391,x3392,x3393),x3392,a2)+P3(f9(x3391,x3392,x3393),x3392,a2) % 97.28/97.29 [340]~P1(x3403)+~P1(x3402)+~P1(x3401)+~P3(x3403,x3401,a2)+~P9(x3401,a2,x3402)+~P7(x3401,a1)+E(f9(x3401,x3402,x3403),x3403)+P3(f14(x3401,x3402,x3403),x3403,a2)+P3(f9(x3401,x3402,x3403),x3403,a2) % 97.28/97.29 [341]~P1(x3413)+~P1(x3412)+~P1(x3411)+~P3(x3413,x3411,a2)+~P10(x3411,a2,x3412)+~P7(x3411,a1)+E(f9(x3411,x3412,x3413),x3413)+P3(f14(x3411,x3412,x3413),x3413,a2)+P3(f9(x3411,x3412,x3413),x3413,a2) % 97.28/97.29 [342]~P1(x3423)+~P1(x3422)+~P1(x3421)+~P3(x3422,x3421,a2)+~P9(x3421,a2,x3423)+~P7(x3421,a1)+E(f9(x3421,x3422,x3423),x3423)+P3(f14(x3421,x3422,x3423),x3423,a2)+P3(f9(x3421,x3422,x3423),x3423,a2) % 97.28/97.29 [343]~P1(x3433)+~P1(x3432)+~P1(x3431)+~P3(x3432,x3431,a2)+~P10(x3431,a2,x3433)+~P7(x3431,a1)+E(f9(x3431,x3432,x3433),x3433)+P3(f14(x3431,x3432,x3433),x3433,a2)+P3(f9(x3431,x3432,x3433),x3433,a2) % 97.28/97.29 [344]~P1(x3443)+~P1(x3442)+~P1(x3441)+~P3(x3443,x3441,a2)+~P9(x3441,a2,x3442)+~P7(x3441,a1)+E(f9(x3441,x3442,x3443),x3442)+P3(f15(x3441,x3442,x3443),x3442,a2)+P3(f9(x3441,x3442,x3443),x3442,a2) % 97.28/97.29 [345]~P1(x3453)+~P1(x3452)+~P1(x3451)+~P3(x3453,x3451,a2)+~P10(x3451,a2,x3452)+~P7(x3451,a1)+E(f9(x3451,x3452,x3453),x3452)+P3(f15(x3451,x3452,x3453),x3452,a2)+P3(f9(x3451,x3452,x3453),x3452,a2) % 97.28/97.29 [346]~P1(x3463)+~P1(x3462)+~P1(x3461)+~P3(x3462,x3461,a2)+~P9(x3461,a2,x3463)+~P7(x3461,a1)+E(f9(x3461,x3462,x3463),x3462)+P3(f15(x3461,x3462,x3463),x3462,a2)+P3(f9(x3461,x3462,x3463),x3462,a2) % 97.28/97.29 [347]~P1(x3473)+~P1(x3472)+~P1(x3471)+~P3(x3472,x3471,a2)+~P10(x3471,a2,x3473)+~P7(x3471,a1)+E(f9(x3471,x3472,x3473),x3472)+P3(f15(x3471,x3472,x3473),x3472,a2)+P3(f9(x3471,x3472,x3473),x3472,a2) % 97.28/97.29 [348]~P1(x3483)+~P1(x3482)+~P1(x3481)+~P9(x3481,a2,x3483)+~P9(x3481,a2,x3482)+~P7(x3481,a1)+E(f9(x3481,x3482,x3483),x3483)+P3(f14(x3481,x3482,x3483),x3483,a2)+P3(f9(x3481,x3482,x3483),x3483,a2) % 97.28/97.29 [349]~P1(x3493)+~P1(x3492)+~P1(x3491)+~P9(x3491,a2,x3493)+~P10(x3491,a2,x3492)+~P7(x3491,a1)+E(f9(x3491,x3492,x3493),x3493)+P3(f14(x3491,x3492,x3493),x3493,a2)+P3(f9(x3491,x3492,x3493),x3493,a2) % 97.28/97.29 [350]~P1(x3503)+~P1(x3502)+~P1(x3501)+~P9(x3501,a2,x3502)+~P10(x3501,a2,x3503)+~P7(x3501,a1)+E(f9(x3501,x3502,x3503),x3503)+P3(f14(x3501,x3502,x3503),x3503,a2)+P3(f9(x3501,x3502,x3503),x3503,a2) % 97.28/97.29 [351]~P1(x3513)+~P1(x3512)+~P1(x3511)+~P10(x3511,a2,x3513)+~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) % 97.28/97.29 [352]~P1(x3523)+~P1(x3522)+~P1(x3521)+~P9(x3521,a2,x3523)+~P9(x3521,a2,x3522)+~P7(x3521,a1)+E(f9(x3521,x3522,x3523),x3522)+P3(f15(x3521,x3522,x3523),x3522,a2)+P3(f9(x3521,x3522,x3523),x3522,a2) % 97.28/97.29 [353]~P1(x3533)+~P1(x3532)+~P1(x3531)+~P9(x3531,a2,x3533)+~P10(x3531,a2,x3532)+~P7(x3531,a1)+E(f9(x3531,x3532,x3533),x3532)+P3(f15(x3531,x3532,x3533),x3532,a2)+P3(f9(x3531,x3532,x3533),x3532,a2) % 97.28/97.29 [354]~P1(x3543)+~P1(x3542)+~P1(x3541)+~P9(x3541,a2,x3542)+~P10(x3541,a2,x3543)+~P7(x3541,a1)+E(f9(x3541,x3542,x3543),x3542)+P3(f15(x3541,x3542,x3543),x3542,a2)+P3(f9(x3541,x3542,x3543),x3542,a2) % 97.28/97.29 [355]~P1(x3553)+~P1(x3552)+~P1(x3551)+~P10(x3551,a2,x3553)+~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) % 97.28/97.29 [362]~E(x3621,x3623)+~P1(x3623)+~P1(x3622)+~P1(x3621)+~P3(x3622,x3621,a2)+~P7(x3621,a1)+E(f9(x3621,x3622,x3623),x3623)+P9(f14(x3621,x3622,x3623),a2,f9(x3621,x3622,x3623))+P3(f9(x3621,x3622,x3623),x3623,a2) % 97.28/97.29 [363]~E(x3631,x3632)+~P1(x3633)+~P1(x3632)+~P1(x3631)+~P3(x3633,x3631,a2)+~P7(x3631,a1)+E(f9(x3631,x3632,x3633),x3633)+P9(f14(x3631,x3632,x3633),a2,f9(x3631,x3632,x3633))+P3(f9(x3631,x3632,x3633),x3633,a2) % 97.28/97.29 [364]~E(x3641,x3643)+~P1(x3643)+~P1(x3642)+~P1(x3641)+~P3(x3642,x3641,a2)+~P7(x3641,a1)+E(f9(x3641,x3642,x3643),x3642)+P9(f15(x3641,x3642,x3643),a2,f9(x3641,x3642,x3643))+P3(f9(x3641,x3642,x3643),x3642,a2) % 97.28/97.29 [365]~E(x3651,x3652)+~P1(x3653)+~P1(x3652)+~P1(x3651)+~P3(x3653,x3651,a2)+~P7(x3651,a1)+E(f9(x3651,x3652,x3653),x3652)+P9(f15(x3651,x3652,x3653),a2,f9(x3651,x3652,x3653))+P3(f9(x3651,x3652,x3653),x3652,a2) % 97.28/97.29 [366]~E(x3661,x3663)+~P1(x3663)+~P1(x3662)+~P1(x3661)+~P9(x3661,a2,x3662)+~P7(x3661,a1)+E(f9(x3661,x3662,x3663),x3663)+P9(f14(x3661,x3662,x3663),a2,f9(x3661,x3662,x3663))+P3(f9(x3661,x3662,x3663),x3663,a2) % 97.28/97.29 [367]~E(x3671,x3673)+~P1(x3673)+~P1(x3672)+~P1(x3671)+~P10(x3671,a2,x3672)+~P7(x3671,a1)+E(f9(x3671,x3672,x3673),x3673)+P9(f14(x3671,x3672,x3673),a2,f9(x3671,x3672,x3673))+P3(f9(x3671,x3672,x3673),x3673,a2) % 97.28/97.29 [368]~E(x3681,x3682)+~P1(x3683)+~P1(x3682)+~P1(x3681)+~P9(x3681,a2,x3683)+~P7(x3681,a1)+E(f9(x3681,x3682,x3683),x3683)+P9(f14(x3681,x3682,x3683),a2,f9(x3681,x3682,x3683))+P3(f9(x3681,x3682,x3683),x3683,a2) % 97.28/97.29 [369]~E(x3691,x3692)+~P1(x3693)+~P1(x3692)+~P1(x3691)+~P10(x3691,a2,x3693)+~P7(x3691,a1)+E(f9(x3691,x3692,x3693),x3693)+P9(f14(x3691,x3692,x3693),a2,f9(x3691,x3692,x3693))+P3(f9(x3691,x3692,x3693),x3693,a2) % 97.28/97.29 [370]~E(x3701,x3703)+~P1(x3703)+~P1(x3702)+~P1(x3701)+~P9(x3701,a2,x3702)+~P7(x3701,a1)+E(f9(x3701,x3702,x3703),x3702)+P9(f15(x3701,x3702,x3703),a2,f9(x3701,x3702,x3703))+P3(f9(x3701,x3702,x3703),x3702,a2) % 97.28/97.29 [371]~E(x3711,x3713)+~P1(x3713)+~P1(x3712)+~P1(x3711)+~P10(x3711,a2,x3712)+~P7(x3711,a1)+E(f9(x3711,x3712,x3713),x3712)+P9(f15(x3711,x3712,x3713),a2,f9(x3711,x3712,x3713))+P3(f9(x3711,x3712,x3713),x3712,a2) % 97.28/97.29 [372]~E(x3721,x3722)+~P1(x3723)+~P1(x3722)+~P1(x3721)+~P9(x3721,a2,x3723)+~P7(x3721,a1)+E(f9(x3721,x3722,x3723),x3722)+P9(f15(x3721,x3722,x3723),a2,f9(x3721,x3722,x3723))+P3(f9(x3721,x3722,x3723),x3722,a2) % 97.28/97.29 [373]~E(x3731,x3732)+~P1(x3733)+~P1(x3732)+~P1(x3731)+~P10(x3731,a2,x3733)+~P7(x3731,a1)+E(f9(x3731,x3732,x3733),x3732)+P9(f15(x3731,x3732,x3733),a2,f9(x3731,x3732,x3733))+P3(f9(x3731,x3732,x3733),x3732,a2) % 97.28/97.29 [400]~P1(x4003)+~P1(x4002)+~P1(x4001)+~P3(x4003,x4001,a2)+~P3(x4002,x4001,a2)+~P7(x4001,a1)+E(f9(x4001,x4002,x4003),x4003)+P9(f14(x4001,x4002,x4003),a2,f9(x4001,x4002,x4003))+P3(f9(x4001,x4002,x4003),x4003,a2) % 97.28/97.29 [401]~P1(x4013)+~P1(x4012)+~P1(x4011)+~P3(x4013,x4011,a2)+~P3(x4012,x4011,a2)+~P7(x4011,a1)+E(f9(x4011,x4012,x4013),x4012)+P9(f15(x4011,x4012,x4013),a2,f9(x4011,x4012,x4013))+P3(f9(x4011,x4012,x4013),x4012,a2) % 97.28/97.29 [402]~P1(x4023)+~P1(x4022)+~P1(x4021)+~P3(x4023,x4021,a2)+~P9(x4021,a2,x4022)+~P7(x4021,a1)+E(f9(x4021,x4022,x4023),x4023)+P9(f14(x4021,x4022,x4023),a2,f9(x4021,x4022,x4023))+P3(f9(x4021,x4022,x4023),x4023,a2) % 97.28/97.29 [403]~P1(x4033)+~P1(x4032)+~P1(x4031)+~P3(x4033,x4031,a2)+~P10(x4031,a2,x4032)+~P7(x4031,a1)+E(f9(x4031,x4032,x4033),x4033)+P9(f14(x4031,x4032,x4033),a2,f9(x4031,x4032,x4033))+P3(f9(x4031,x4032,x4033),x4033,a2) % 97.28/97.29 [404]~P1(x4043)+~P1(x4042)+~P1(x4041)+~P3(x4042,x4041,a2)+~P9(x4041,a2,x4043)+~P7(x4041,a1)+E(f9(x4041,x4042,x4043),x4043)+P9(f14(x4041,x4042,x4043),a2,f9(x4041,x4042,x4043))+P3(f9(x4041,x4042,x4043),x4043,a2) % 97.28/97.29 [405]~P1(x4053)+~P1(x4052)+~P1(x4051)+~P3(x4052,x4051,a2)+~P10(x4051,a2,x4053)+~P7(x4051,a1)+E(f9(x4051,x4052,x4053),x4053)+P9(f14(x4051,x4052,x4053),a2,f9(x4051,x4052,x4053))+P3(f9(x4051,x4052,x4053),x4053,a2) % 97.28/97.29 [406]~P1(x4063)+~P1(x4062)+~P1(x4061)+~P3(x4063,x4061,a2)+~P9(x4061,a2,x4062)+~P7(x4061,a1)+E(f9(x4061,x4062,x4063),x4062)+P9(f15(x4061,x4062,x4063),a2,f9(x4061,x4062,x4063))+P3(f9(x4061,x4062,x4063),x4062,a2) % 97.28/97.29 [407]~P1(x4073)+~P1(x4072)+~P1(x4071)+~P3(x4073,x4071,a2)+~P10(x4071,a2,x4072)+~P7(x4071,a1)+E(f9(x4071,x4072,x4073),x4072)+P9(f15(x4071,x4072,x4073),a2,f9(x4071,x4072,x4073))+P3(f9(x4071,x4072,x4073),x4072,a2) % 97.28/97.29 [408]~P1(x4083)+~P1(x4082)+~P1(x4081)+~P3(x4082,x4081,a2)+~P9(x4081,a2,x4083)+~P7(x4081,a1)+E(f9(x4081,x4082,x4083),x4082)+P9(f15(x4081,x4082,x4083),a2,f9(x4081,x4082,x4083))+P3(f9(x4081,x4082,x4083),x4082,a2) % 97.28/97.29 [409]~P1(x4093)+~P1(x4092)+~P1(x4091)+~P3(x4092,x4091,a2)+~P10(x4091,a2,x4093)+~P7(x4091,a1)+E(f9(x4091,x4092,x4093),x4092)+P9(f15(x4091,x4092,x4093),a2,f9(x4091,x4092,x4093))+P3(f9(x4091,x4092,x4093),x4092,a2) % 97.28/97.29 [410]~P1(x4103)+~P1(x4102)+~P1(x4101)+~P9(x4101,a2,x4103)+~P9(x4101,a2,x4102)+~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) % 97.28/97.29 [411]~P1(x4113)+~P1(x4112)+~P1(x4111)+~P9(x4111,a2,x4113)+~P10(x4111,a2,x4112)+~P7(x4111,a1)+E(f9(x4111,x4112,x4113),x4113)+P9(f14(x4111,x4112,x4113),a2,f9(x4111,x4112,x4113))+P3(f9(x4111,x4112,x4113),x4113,a2) % 97.28/97.29 [412]~P1(x4123)+~P1(x4122)+~P1(x4121)+~P9(x4121,a2,x4122)+~P10(x4121,a2,x4123)+~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) % 97.28/97.29 [413]~P1(x4133)+~P1(x4132)+~P1(x4131)+~P10(x4131,a2,x4133)+~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) % 97.28/97.29 [414]~P1(x4143)+~P1(x4142)+~P1(x4141)+~P9(x4141,a2,x4143)+~P9(x4141,a2,x4142)+~P7(x4141,a1)+E(f9(x4141,x4142,x4143),x4142)+P9(f15(x4141,x4142,x4143),a2,f9(x4141,x4142,x4143))+P3(f9(x4141,x4142,x4143),x4142,a2) % 97.28/97.29 [415]~P1(x4153)+~P1(x4152)+~P1(x4151)+~P9(x4151,a2,x4153)+~P10(x4151,a2,x4152)+~P7(x4151,a1)+E(f9(x4151,x4152,x4153),x4152)+P9(f15(x4151,x4152,x4153),a2,f9(x4151,x4152,x4153))+P3(f9(x4151,x4152,x4153),x4152,a2) % 97.28/97.29 [416]~P1(x4163)+~P1(x4162)+~P1(x4161)+~P9(x4161,a2,x4162)+~P10(x4161,a2,x4163)+~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) % 97.28/97.29 [417]~P1(x4173)+~P1(x4172)+~P1(x4171)+~P10(x4171,a2,x4173)+~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) % 97.28/97.29 [186]~E(x1861,x1863)+~P1(x1863)+~P1(x1862)+~P1(x1861)+~P1(x1864)+~P3(x1864,x1861,a2)+~P9(x1864,a2,x1862)+~P7(x1861,a1)+P1(f9(x1861,x1862,x1863)) % 97.28/97.29 [187]~E(x1871,x1872)+~P1(x1873)+~P1(x1872)+~P1(x1871)+~P1(x1874)+~P3(x1874,x1871,a2)+~P9(x1874,a2,x1873)+~P7(x1871,a1)+P1(f9(x1871,x1872,x1873)) % 97.28/97.29 [223]~E(x2232,x2233)+~P1(x2233)+~P1(x2232)+~P1(x2231)+~P1(x2234)+~P3(x2234,x2232,a2)+~P9(x2234,a2,x2231)+~P7(x2232,a1)+P10(x2231,a2,f9(x2232,x2233,x2231)) % 97.28/97.29 [224]~E(x2241,x2242)+~P1(x2243)+~P1(x2242)+~P1(x2241)+~P1(x2244)+~P3(x2244,x2242,a2)+~P9(x2244,a2,x2243)+~P7(x2242,a1)+P10(x2241,a2,f9(x2242,x2243,x2241)) % 97.28/97.29 [225]~E(x2252,x2253)+~P1(x2253)+~P1(x2252)+~P1(x2251)+~P1(x2254)+~P3(x2254,x2252,a2)+~P9(x2254,a2,x2251)+~P7(x2252,a1)+P10(x2251,a2,f9(x2252,x2251,x2253)) % 97.28/97.29 [226]~E(x2261,x2262)+~P1(x2263)+~P1(x2262)+~P1(x2261)+~P1(x2264)+~P3(x2264,x2262,a2)+~P9(x2264,a2,x2263)+~P7(x2262,a1)+P10(x2261,a2,f9(x2262,x2261,x2263)) % 97.28/97.29 [229]~P1(x2293)+~P1(x2292)+~P1(x2291)+~P1(x2294)+~P3(x2294,x2291,a2)+~P3(x2293,x2291,a2)+~P9(x2294,a2,x2292)+~P7(x2291,a1)+P1(f9(x2291,x2292,x2293)) % 97.28/97.29 [230]~P1(x2303)+~P1(x2302)+~P1(x2301)+~P1(x2304)+~P3(x2304,x2301,a2)+~P3(x2302,x2301,a2)+~P9(x2304,a2,x2303)+~P7(x2301,a1)+P1(f9(x2301,x2302,x2303)) % 97.28/97.29 [231]~P1(x2313)+~P1(x2312)+~P1(x2311)+~P1(x2314)+~P3(x2314,x2311,a2)+~P9(x2314,a2,x2313)+~P9(x2311,a2,x2312)+~P7(x2311,a1)+P1(f9(x2311,x2312,x2313)) % 97.28/97.29 [232]~P1(x2323)+~P1(x2322)+~P1(x2321)+~P1(x2324)+~P3(x2324,x2321,a2)+~P9(x2324,a2,x2323)+~P10(x2321,a2,x2322)+~P7(x2321,a1)+P1(f9(x2321,x2322,x2323)) % 97.28/97.29 [233]~P1(x2333)+~P1(x2332)+~P1(x2331)+~P1(x2334)+~P3(x2334,x2331,a2)+~P9(x2334,a2,x2332)+~P9(x2331,a2,x2333)+~P7(x2331,a1)+P1(f9(x2331,x2332,x2333)) % 97.28/97.29 [234]~P1(x2343)+~P1(x2342)+~P1(x2341)+~P1(x2344)+~P3(x2344,x2341,a2)+~P9(x2344,a2,x2342)+~P10(x2341,a2,x2343)+~P7(x2341,a1)+P1(f9(x2341,x2342,x2343)) % 97.28/97.29 [271]~P1(x2713)+~P1(x2712)+~P1(x2711)+~P1(x2714)+~P3(x2714,x2712,a2)+~P3(x2713,x2712,a2)+~P9(x2714,a2,x2711)+~P7(x2712,a1)+P10(x2711,a2,f9(x2712,x2713,x2711)) % 97.28/97.29 [272]~P1(x2723)+~P1(x2722)+~P1(x2721)+~P1(x2724)+~P3(x2724,x2722,a2)+~P3(x2721,x2722,a2)+~P9(x2724,a2,x2723)+~P7(x2722,a1)+P10(x2721,a2,f9(x2722,x2723,x2721)) % 97.28/97.29 [273]~P1(x2733)+~P1(x2732)+~P1(x2731)+~P1(x2734)+~P3(x2734,x2732,a2)+~P3(x2733,x2732,a2)+~P9(x2734,a2,x2731)+~P7(x2732,a1)+P10(x2731,a2,f9(x2732,x2731,x2733)) % 97.28/97.29 [274]~P1(x2743)+~P1(x2742)+~P1(x2741)+~P1(x2744)+~P3(x2744,x2742,a2)+~P3(x2741,x2742,a2)+~P9(x2744,a2,x2743)+~P7(x2742,a1)+P10(x2741,a2,f9(x2742,x2741,x2743)) % 97.28/97.29 [275]~P1(x2753)+~P1(x2752)+~P1(x2751)+~P1(x2754)+~P3(x2754,x2752,a2)+~P9(x2754,a2,x2753)+~P9(x2752,a2,x2751)+~P7(x2752,a1)+P10(x2751,a2,f9(x2752,x2753,x2751)) % 97.28/97.29 [276]~P1(x2763)+~P1(x2762)+~P1(x2761)+~P1(x2764)+~P3(x2764,x2762,a2)+~P9(x2764,a2,x2763)+~P10(x2762,a2,x2761)+~P7(x2762,a1)+P10(x2761,a2,f9(x2762,x2763,x2761)) % 97.28/97.29 [277]~P1(x2773)+~P1(x2772)+~P1(x2771)+~P1(x2774)+~P3(x2774,x2772,a2)+~P9(x2774,a2,x2771)+~P9(x2772,a2,x2773)+~P7(x2772,a1)+P10(x2771,a2,f9(x2772,x2773,x2771)) % 97.28/97.29 [278]~P1(x2783)+~P1(x2782)+~P1(x2781)+~P1(x2784)+~P3(x2784,x2782,a2)+~P9(x2784,a2,x2781)+~P10(x2782,a2,x2783)+~P7(x2782,a1)+P10(x2781,a2,f9(x2782,x2783,x2781)) % 97.28/97.29 [279]~P1(x2793)+~P1(x2792)+~P1(x2791)+~P1(x2794)+~P3(x2794,x2792,a2)+~P9(x2794,a2,x2793)+~P9(x2792,a2,x2791)+~P7(x2792,a1)+P10(x2791,a2,f9(x2792,x2791,x2793)) % 97.28/97.29 [280]~P1(x2803)+~P1(x2802)+~P1(x2801)+~P1(x2804)+~P3(x2804,x2802,a2)+~P9(x2804,a2,x2803)+~P10(x2802,a2,x2801)+~P7(x2802,a1)+P10(x2801,a2,f9(x2802,x2801,x2803)) % 97.28/97.29 [281]~P1(x2813)+~P1(x2812)+~P1(x2811)+~P1(x2814)+~P3(x2814,x2812,a2)+~P9(x2814,a2,x2811)+~P9(x2812,a2,x2813)+~P7(x2812,a1)+P10(x2811,a2,f9(x2812,x2811,x2813)) % 97.28/97.29 [282]~P1(x2823)+~P1(x2822)+~P1(x2821)+~P1(x2824)+~P3(x2824,x2822,a2)+~P9(x2824,a2,x2821)+~P10(x2822,a2,x2823)+~P7(x2822,a1)+P10(x2821,a2,f9(x2822,x2821,x2823)) % 97.28/97.29 [255]~E(x2551,x2552)+~P1(x2552)+~P1(x2551)+~P1(x2553)+~P1(x2554)+~P3(x2554,x2551,a2)+~P9(x2554,a2,x2553)+~P7(x2551,a1)+E(f9(x2551,x2552,x2553),x2553)+P9(x2553,a2,f9(x2551,x2552,x2553)) % 97.28/97.29 [256]~E(x2563,x2561)+~P1(x2562)+~P1(x2561)+~P1(x2563)+~P1(x2564)+~P3(x2564,x2561,a2)+~P9(x2564,a2,x2562)+~P7(x2561,a1)+E(f9(x2561,x2562,x2563),x2563)+P9(x2563,a2,f9(x2561,x2562,x2563)) % 97.28/97.29 [257]~E(x2571,x2573)+~P1(x2573)+~P1(x2571)+~P1(x2572)+~P1(x2574)+~P3(x2574,x2571,a2)+~P9(x2574,a2,x2572)+~P7(x2571,a1)+E(f9(x2571,x2572,x2573),x2572)+P9(x2572,a2,f9(x2571,x2572,x2573)) % 97.28/97.29 [258]~E(x2582,x2581)+~P1(x2583)+~P1(x2581)+~P1(x2582)+~P1(x2584)+~P3(x2584,x2581,a2)+~P9(x2584,a2,x2583)+~P7(x2581,a1)+E(f9(x2581,x2582,x2583),x2582)+P9(x2582,a2,f9(x2581,x2582,x2583)) % 97.28/97.29 [298]~P1(x2982)+~P1(x2981)+~P1(x2983)+~P1(x2984)+~P3(x2984,x2981,a2)+~P3(x2982,x2981,a2)+~P9(x2984,a2,x2983)+~P7(x2981,a1)+E(f9(x2981,x2982,x2983),x2983)+P9(x2983,a2,f9(x2981,x2982,x2983)) % 97.28/97.29 [299]~P1(x2992)+~P1(x2991)+~P1(x2993)+~P1(x2994)+~P3(x2994,x2991,a2)+~P3(x2993,x2991,a2)+~P9(x2994,a2,x2992)+~P7(x2991,a1)+E(f9(x2991,x2992,x2993),x2993)+P9(x2993,a2,f9(x2991,x2992,x2993)) % 97.28/97.29 [300]~P1(x3003)+~P1(x3001)+~P1(x3002)+~P1(x3004)+~P3(x3004,x3001,a2)+~P3(x3003,x3001,a2)+~P9(x3004,a2,x3002)+~P7(x3001,a1)+E(f9(x3001,x3002,x3003),x3002)+P9(x3002,a2,f9(x3001,x3002,x3003)) % 97.28/97.29 [301]~P1(x3013)+~P1(x3011)+~P1(x3012)+~P1(x3014)+~P3(x3014,x3011,a2)+~P3(x3012,x3011,a2)+~P9(x3014,a2,x3013)+~P7(x3011,a1)+E(f9(x3011,x3012,x3013),x3012)+P9(x3012,a2,f9(x3011,x3012,x3013)) % 97.28/97.29 [302]~P1(x3022)+~P1(x3021)+~P1(x3023)+~P1(x3024)+~P3(x3024,x3021,a2)+~P9(x3024,a2,x3022)+~P9(x3021,a2,x3023)+~P7(x3021,a1)+E(f9(x3021,x3022,x3023),x3023)+P9(x3023,a2,f9(x3021,x3022,x3023)) % 97.28/97.29 [303]~P1(x3032)+~P1(x3031)+~P1(x3033)+~P1(x3034)+~P3(x3034,x3031,a2)+~P9(x3034,a2,x3032)+~P10(x3031,a2,x3033)+~P7(x3031,a1)+E(f9(x3031,x3032,x3033),x3033)+P9(x3033,a2,f9(x3031,x3032,x3033)) % 97.28/97.29 [304]~P1(x3042)+~P1(x3041)+~P1(x3043)+~P1(x3044)+~P3(x3044,x3041,a2)+~P9(x3044,a2,x3043)+~P9(x3041,a2,x3042)+~P7(x3041,a1)+E(f9(x3041,x3042,x3043),x3043)+P9(x3043,a2,f9(x3041,x3042,x3043)) % 97.28/97.29 [305]~P1(x3052)+~P1(x3051)+~P1(x3053)+~P1(x3054)+~P3(x3054,x3051,a2)+~P9(x3054,a2,x3053)+~P10(x3051,a2,x3052)+~P7(x3051,a1)+E(f9(x3051,x3052,x3053),x3053)+P9(x3053,a2,f9(x3051,x3052,x3053)) % 97.28/97.29 [306]~P1(x3063)+~P1(x3061)+~P1(x3062)+~P1(x3064)+~P3(x3064,x3061,a2)+~P9(x3064,a2,x3063)+~P9(x3061,a2,x3062)+~P7(x3061,a1)+E(f9(x3061,x3062,x3063),x3062)+P9(x3062,a2,f9(x3061,x3062,x3063)) % 97.28/97.29 [307]~P1(x3073)+~P1(x3071)+~P1(x3072)+~P1(x3074)+~P3(x3074,x3071,a2)+~P9(x3074,a2,x3073)+~P10(x3071,a2,x3072)+~P7(x3071,a1)+E(f9(x3071,x3072,x3073),x3072)+P9(x3072,a2,f9(x3071,x3072,x3073)) % 97.28/97.29 [308]~P1(x3083)+~P1(x3081)+~P1(x3082)+~P1(x3084)+~P3(x3084,x3081,a2)+~P9(x3084,a2,x3082)+~P9(x3081,a2,x3083)+~P7(x3081,a1)+E(f9(x3081,x3082,x3083),x3082)+P9(x3082,a2,f9(x3081,x3082,x3083)) % 97.28/97.29 [309]~P1(x3093)+~P1(x3091)+~P1(x3092)+~P1(x3094)+~P3(x3094,x3091,a2)+~P9(x3094,a2,x3092)+~P10(x3091,a2,x3093)+~P7(x3091,a1)+E(f9(x3091,x3092,x3093),x3092)+P9(x3092,a2,f9(x3091,x3092,x3093)) % 97.28/97.29 [330]~E(x3301,x3303)+~P1(x3303)+~P1(x3302)+~P1(x3301)+~P1(x3304)+~P3(x3304,x3301,a2)+~P9(x3304,a2,x3302)+~P7(x3301,a1)+E(f9(x3301,x3302,x3303),x3303)+P3(f9(x3301,x3302,x3303),x3303,a2)+P1(f14(x3301,x3302,x3303)) % 97.28/97.29 [331]~E(x3311,x3312)+~P1(x3313)+~P1(x3312)+~P1(x3311)+~P1(x3314)+~P3(x3314,x3311,a2)+~P9(x3314,a2,x3313)+~P7(x3311,a1)+E(f9(x3311,x3312,x3313),x3313)+P3(f9(x3311,x3312,x3313),x3313,a2)+P1(f14(x3311,x3312,x3313)) % 97.28/97.29 [332]~E(x3321,x3323)+~P1(x3323)+~P1(x3322)+~P1(x3321)+~P1(x3324)+~P3(x3324,x3321,a2)+~P9(x3324,a2,x3322)+~P7(x3321,a1)+E(f9(x3321,x3322,x3323),x3322)+P3(f9(x3321,x3322,x3323),x3322,a2)+P1(f15(x3321,x3322,x3323)) % 97.28/97.29 [333]~E(x3331,x3332)+~P1(x3333)+~P1(x3332)+~P1(x3331)+~P1(x3334)+~P3(x3334,x3331,a2)+~P9(x3334,a2,x3333)+~P7(x3331,a1)+E(f9(x3331,x3332,x3333),x3332)+P3(f9(x3331,x3332,x3333),x3332,a2)+P1(f15(x3331,x3332,x3333)) % 97.28/97.29 [356]~E(x3561,x3563)+~P1(x3563)+~P1(x3562)+~P1(x3561)+~P1(x3564)+~P3(x3564,x3561,a2)+~P9(x3564,a2,x3562)+~P7(x3561,a1)+E(f9(x3561,x3562,x3563),x3563)+P3(f14(x3561,x3562,x3563),x3563,a2)+P3(f9(x3561,x3562,x3563),x3563,a2) % 97.28/97.29 [357]~E(x3571,x3572)+~P1(x3573)+~P1(x3572)+~P1(x3571)+~P1(x3574)+~P3(x3574,x3571,a2)+~P9(x3574,a2,x3573)+~P7(x3571,a1)+E(f9(x3571,x3572,x3573),x3573)+P3(f14(x3571,x3572,x3573),x3573,a2)+P3(f9(x3571,x3572,x3573),x3573,a2) % 97.28/97.29 [358]~E(x3581,x3583)+~P1(x3583)+~P1(x3582)+~P1(x3581)+~P1(x3584)+~P3(x3584,x3581,a2)+~P9(x3584,a2,x3582)+~P7(x3581,a1)+E(f9(x3581,x3582,x3583),x3582)+P3(f15(x3581,x3582,x3583),x3582,a2)+P3(f9(x3581,x3582,x3583),x3582,a2) % 97.28/97.29 [359]~E(x3591,x3592)+~P1(x3593)+~P1(x3592)+~P1(x3591)+~P1(x3594)+~P3(x3594,x3591,a2)+~P9(x3594,a2,x3593)+~P7(x3591,a1)+E(f9(x3591,x3592,x3593),x3592)+P3(f15(x3591,x3592,x3593),x3592,a2)+P3(f9(x3591,x3592,x3593),x3592,a2) % 97.28/97.29 [374]~P1(x3743)+~P1(x3742)+~P1(x3741)+~P1(x3744)+~P3(x3744,x3741,a2)+~P3(x3743,x3741,a2)+~P9(x3744,a2,x3742)+~P7(x3741,a1)+E(f9(x3741,x3742,x3743),x3743)+P3(f9(x3741,x3742,x3743),x3743,a2)+P1(f14(x3741,x3742,x3743)) % 97.28/97.29 [375]~P1(x3753)+~P1(x3752)+~P1(x3751)+~P1(x3754)+~P3(x3754,x3751,a2)+~P3(x3752,x3751,a2)+~P9(x3754,a2,x3753)+~P7(x3751,a1)+E(f9(x3751,x3752,x3753),x3753)+P3(f9(x3751,x3752,x3753),x3753,a2)+P1(f14(x3751,x3752,x3753)) % 97.28/97.29 [376]~P1(x3763)+~P1(x3762)+~P1(x3761)+~P1(x3764)+~P3(x3764,x3761,a2)+~P3(x3763,x3761,a2)+~P9(x3764,a2,x3762)+~P7(x3761,a1)+E(f9(x3761,x3762,x3763),x3762)+P3(f9(x3761,x3762,x3763),x3762,a2)+P1(f15(x3761,x3762,x3763)) % 97.28/97.29 [377]~P1(x3773)+~P1(x3772)+~P1(x3771)+~P1(x3774)+~P3(x3774,x3771,a2)+~P3(x3772,x3771,a2)+~P9(x3774,a2,x3773)+~P7(x3771,a1)+E(f9(x3771,x3772,x3773),x3772)+P3(f9(x3771,x3772,x3773),x3772,a2)+P1(f15(x3771,x3772,x3773)) % 97.28/97.29 [378]~P1(x3783)+~P1(x3782)+~P1(x3781)+~P1(x3784)+~P3(x3784,x3781,a2)+~P9(x3784,a2,x3783)+~P9(x3781,a2,x3782)+~P7(x3781,a1)+E(f9(x3781,x3782,x3783),x3783)+P3(f9(x3781,x3782,x3783),x3783,a2)+P1(f14(x3781,x3782,x3783)) % 97.28/97.29 [379]~P1(x3793)+~P1(x3792)+~P1(x3791)+~P1(x3794)+~P3(x3794,x3791,a2)+~P9(x3794,a2,x3793)+~P10(x3791,a2,x3792)+~P7(x3791,a1)+E(f9(x3791,x3792,x3793),x3793)+P3(f9(x3791,x3792,x3793),x3793,a2)+P1(f14(x3791,x3792,x3793)) % 97.28/97.29 [380]~P1(x3803)+~P1(x3802)+~P1(x3801)+~P1(x3804)+~P3(x3804,x3801,a2)+~P9(x3804,a2,x3802)+~P9(x3801,a2,x3803)+~P7(x3801,a1)+E(f9(x3801,x3802,x3803),x3803)+P3(f9(x3801,x3802,x3803),x3803,a2)+P1(f14(x3801,x3802,x3803)) % 97.28/97.29 [381]~P1(x3813)+~P1(x3812)+~P1(x3811)+~P1(x3814)+~P3(x3814,x3811,a2)+~P9(x3814,a2,x3812)+~P10(x3811,a2,x3813)+~P7(x3811,a1)+E(f9(x3811,x3812,x3813),x3813)+P3(f9(x3811,x3812,x3813),x3813,a2)+P1(f14(x3811,x3812,x3813)) % 97.28/97.29 [382]~P1(x3823)+~P1(x3822)+~P1(x3821)+~P1(x3824)+~P3(x3824,x3821,a2)+~P9(x3824,a2,x3823)+~P9(x3821,a2,x3822)+~P7(x3821,a1)+E(f9(x3821,x3822,x3823),x3822)+P3(f9(x3821,x3822,x3823),x3822,a2)+P1(f15(x3821,x3822,x3823)) % 97.28/97.29 [383]~P1(x3833)+~P1(x3832)+~P1(x3831)+~P1(x3834)+~P3(x3834,x3831,a2)+~P9(x3834,a2,x3833)+~P10(x3831,a2,x3832)+~P7(x3831,a1)+E(f9(x3831,x3832,x3833),x3832)+P3(f9(x3831,x3832,x3833),x3832,a2)+P1(f15(x3831,x3832,x3833)) % 97.28/97.29 [384]~P1(x3843)+~P1(x3842)+~P1(x3841)+~P1(x3844)+~P3(x3844,x3841,a2)+~P9(x3844,a2,x3842)+~P9(x3841,a2,x3843)+~P7(x3841,a1)+E(f9(x3841,x3842,x3843),x3842)+P3(f9(x3841,x3842,x3843),x3842,a2)+P1(f15(x3841,x3842,x3843)) % 97.28/97.29 [385]~P1(x3853)+~P1(x3852)+~P1(x3851)+~P1(x3854)+~P3(x3854,x3851,a2)+~P9(x3854,a2,x3852)+~P10(x3851,a2,x3853)+~P7(x3851,a1)+E(f9(x3851,x3852,x3853),x3852)+P3(f9(x3851,x3852,x3853),x3852,a2)+P1(f15(x3851,x3852,x3853)) % 97.28/97.29 [388]~P1(x3883)+~P1(x3882)+~P1(x3881)+~P1(x3884)+~P3(x3884,x3881,a2)+~P3(x3883,x3881,a2)+~P9(x3884,a2,x3882)+~P7(x3881,a1)+E(f9(x3881,x3882,x3883),x3883)+P3(f14(x3881,x3882,x3883),x3883,a2)+P3(f9(x3881,x3882,x3883),x3883,a2) % 97.28/97.29 [389]~P1(x3893)+~P1(x3892)+~P1(x3891)+~P1(x3894)+~P3(x3894,x3891,a2)+~P3(x3892,x3891,a2)+~P9(x3894,a2,x3893)+~P7(x3891,a1)+E(f9(x3891,x3892,x3893),x3893)+P3(f14(x3891,x3892,x3893),x3893,a2)+P3(f9(x3891,x3892,x3893),x3893,a2) % 97.28/97.29 [390]~P1(x3903)+~P1(x3902)+~P1(x3901)+~P1(x3904)+~P3(x3904,x3901,a2)+~P3(x3903,x3901,a2)+~P9(x3904,a2,x3902)+~P7(x3901,a1)+E(f9(x3901,x3902,x3903),x3902)+P3(f15(x3901,x3902,x3903),x3902,a2)+P3(f9(x3901,x3902,x3903),x3902,a2) % 97.28/97.29 [391]~P1(x3913)+~P1(x3912)+~P1(x3911)+~P1(x3914)+~P3(x3914,x3911,a2)+~P3(x3912,x3911,a2)+~P9(x3914,a2,x3913)+~P7(x3911,a1)+E(f9(x3911,x3912,x3913),x3912)+P3(f15(x3911,x3912,x3913),x3912,a2)+P3(f9(x3911,x3912,x3913),x3912,a2) % 97.28/97.29 [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),x3923)+P3(f14(x3921,x3922,x3923),x3923,a2)+P3(f9(x3921,x3922,x3923),x3923,a2) % 97.28/97.29 [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),x3933)+P3(f14(x3931,x3932,x3933),x3933,a2)+P3(f9(x3931,x3932,x3933),x3933,a2) % 97.28/97.29 [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),x3943)+P3(f14(x3941,x3942,x3943),x3943,a2)+P3(f9(x3941,x3942,x3943),x3943,a2) % 97.28/97.29 [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),x3953)+P3(f14(x3951,x3952,x3953),x3953,a2)+P3(f9(x3951,x3952,x3953),x3953,a2) % 97.28/97.29 [396]~P1(x3963)+~P1(x3962)+~P1(x3961)+~P1(x3964)+~P3(x3964,x3961,a2)+~P9(x3964,a2,x3963)+~P9(x3961,a2,x3962)+~P7(x3961,a1)+E(f9(x3961,x3962,x3963),x3962)+P3(f15(x3961,x3962,x3963),x3962,a2)+P3(f9(x3961,x3962,x3963),x3962,a2) % 97.28/97.29 [397]~P1(x3973)+~P1(x3972)+~P1(x3971)+~P1(x3974)+~P3(x3974,x3971,a2)+~P9(x3974,a2,x3973)+~P10(x3971,a2,x3972)+~P7(x3971,a1)+E(f9(x3971,x3972,x3973),x3972)+P3(f15(x3971,x3972,x3973),x3972,a2)+P3(f9(x3971,x3972,x3973),x3972,a2) % 97.28/97.29 [398]~P1(x3983)+~P1(x3982)+~P1(x3981)+~P1(x3984)+~P3(x3984,x3981,a2)+~P9(x3984,a2,x3982)+~P9(x3981,a2,x3983)+~P7(x3981,a1)+E(f9(x3981,x3982,x3983),x3982)+P3(f15(x3981,x3982,x3983),x3982,a2)+P3(f9(x3981,x3982,x3983),x3982,a2) % 97.28/97.29 [399]~P1(x3993)+~P1(x3992)+~P1(x3991)+~P1(x3994)+~P3(x3994,x3991,a2)+~P9(x3994,a2,x3992)+~P10(x3991,a2,x3993)+~P7(x3991,a1)+E(f9(x3991,x3992,x3993),x3992)+P3(f15(x3991,x3992,x3993),x3992,a2)+P3(f9(x3991,x3992,x3993),x3992,a2) % 97.28/97.29 [418]~E(x4181,x4183)+~P1(x4183)+~P1(x4182)+~P1(x4181)+~P1(x4184)+~P3(x4184,x4181,a2)+~P9(x4184,a2,x4182)+~P7(x4181,a1)+E(f9(x4181,x4182,x4183),x4183)+P9(f14(x4181,x4182,x4183),a2,f9(x4181,x4182,x4183))+P3(f9(x4181,x4182,x4183),x4183,a2) % 97.28/97.29 [419]~E(x4191,x4192)+~P1(x4193)+~P1(x4192)+~P1(x4191)+~P1(x4194)+~P3(x4194,x4191,a2)+~P9(x4194,a2,x4193)+~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) % 97.28/97.29 [420]~E(x4201,x4203)+~P1(x4203)+~P1(x4202)+~P1(x4201)+~P1(x4204)+~P3(x4204,x4201,a2)+~P9(x4204,a2,x4202)+~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) % 97.28/97.29 [421]~E(x4211,x4212)+~P1(x4213)+~P1(x4212)+~P1(x4211)+~P1(x4214)+~P3(x4214,x4211,a2)+~P9(x4214,a2,x4213)+~P7(x4211,a1)+E(f9(x4211,x4212,x4213),x4212)+P9(f15(x4211,x4212,x4213),a2,f9(x4211,x4212,x4213))+P3(f9(x4211,x4212,x4213),x4212,a2) % 97.28/97.29 [432]~P1(x4323)+~P1(x4322)+~P1(x4321)+~P1(x4324)+~P3(x4324,x4321,a2)+~P3(x4323,x4321,a2)+~P9(x4324,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) % 97.28/97.29 [433]~P1(x4333)+~P1(x4332)+~P1(x4331)+~P1(x4334)+~P3(x4334,x4331,a2)+~P3(x4332,x4331,a2)+~P9(x4334,a2,x4333)+~P7(x4331,a1)+E(f9(x4331,x4332,x4333),x4333)+P9(f14(x4331,x4332,x4333),a2,f9(x4331,x4332,x4333))+P3(f9(x4331,x4332,x4333),x4333,a2) % 97.28/97.29 [434]~P1(x4343)+~P1(x4342)+~P1(x4341)+~P1(x4344)+~P3(x4344,x4341,a2)+~P3(x4343,x4341,a2)+~P9(x4344,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) % 97.28/97.29 [435]~P1(x4353)+~P1(x4352)+~P1(x4351)+~P1(x4354)+~P3(x4354,x4351,a2)+~P3(x4352,x4351,a2)+~P9(x4354,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) % 97.28/97.29 [436]~P1(x4363)+~P1(x4362)+~P1(x4361)+~P1(x4364)+~P3(x4364,x4361,a2)+~P9(x4364,a2,x4363)+~P9(x4361,a2,x4362)+~P7(x4361,a1)+E(f9(x4361,x4362,x4363),x4363)+P9(f14(x4361,x4362,x4363),a2,f9(x4361,x4362,x4363))+P3(f9(x4361,x4362,x4363),x4363,a2) % 97.28/97.29 [437]~P1(x4373)+~P1(x4372)+~P1(x4371)+~P1(x4374)+~P3(x4374,x4371,a2)+~P9(x4374,a2,x4373)+~P10(x4371,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) % 97.28/97.29 [438]~P1(x4383)+~P1(x4382)+~P1(x4381)+~P1(x4384)+~P3(x4384,x4381,a2)+~P9(x4384,a2,x4382)+~P9(x4381,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) % 97.28/97.29 [439]~P1(x4393)+~P1(x4392)+~P1(x4391)+~P1(x4394)+~P3(x4394,x4391,a2)+~P9(x4394,a2,x4392)+~P10(x4391,a2,x4393)+~P7(x4391,a1)+E(f9(x4391,x4392,x4393),x4393)+P9(f14(x4391,x4392,x4393),a2,f9(x4391,x4392,x4393))+P3(f9(x4391,x4392,x4393),x4393,a2) % 97.28/97.29 [440]~P1(x4403)+~P1(x4402)+~P1(x4401)+~P1(x4404)+~P3(x4404,x4401,a2)+~P9(x4404,a2,x4403)+~P9(x4401,a2,x4402)+~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) % 97.28/97.29 [441]~P1(x4413)+~P1(x4412)+~P1(x4411)+~P1(x4414)+~P3(x4414,x4411,a2)+~P9(x4414,a2,x4413)+~P10(x4411,a2,x4412)+~P7(x4411,a1)+E(f9(x4411,x4412,x4413),x4412)+P9(f15(x4411,x4412,x4413),a2,f9(x4411,x4412,x4413))+P3(f9(x4411,x4412,x4413),x4412,a2) % 97.28/97.29 [442]~P1(x4423)+~P1(x4422)+~P1(x4421)+~P1(x4424)+~P3(x4424,x4421,a2)+~P9(x4424,a2,x4422)+~P9(x4421,a2,x4423)+~P7(x4421,a1)+E(f9(x4421,x4422,x4423),x4422)+P9(f15(x4421,x4422,x4423),a2,f9(x4421,x4422,x4423))+P3(f9(x4421,x4422,x4423),x4422,a2) % 97.28/97.29 [443]~P1(x4433)+~P1(x4432)+~P1(x4431)+~P1(x4434)+~P3(x4434,x4431,a2)+~P9(x4434,a2,x4432)+~P10(x4431,a2,x4433)+~P7(x4431,a1)+E(f9(x4431,x4432,x4433),x4432)+P9(f15(x4431,x4432,x4433),a2,f9(x4431,x4432,x4433))+P3(f9(x4431,x4432,x4433),x4432,a2) % 97.28/97.29 [283]~P1(x2833)+~P1(x2832)+~P1(x2831)+~P1(x2834)+~P1(x2835)+~P3(x2834,x2831,a2)+~P3(x2835,x2831,a2)+~P9(x2834,a2,x2832)+~P9(x2835,a2,x2833)+~P7(x2831,a1)+P1(f9(x2831,x2832,x2833)) % 97.28/97.29 [334]~P1(x3343)+~P1(x3342)+~P1(x3341)+~P1(x3344)+~P1(x3345)+~P3(x3344,x3342,a2)+~P3(x3345,x3342,a2)+~P9(x3344,a2,x3343)+~P9(x3345,a2,x3341)+~P7(x3342,a1)+P10(x3341,a2,f9(x3342,x3343,x3341)) % 97.28/97.29 [335]~P1(x3353)+~P1(x3352)+~P1(x3351)+~P1(x3354)+~P1(x3355)+~P3(x3354,x3352,a2)+~P3(x3355,x3352,a2)+~P9(x3354,a2,x3351)+~P9(x3355,a2,x3353)+~P7(x3352,a1)+P10(x3351,a2,f9(x3352,x3351,x3353)) % 97.28/97.29 [360]~P1(x3602)+~P1(x3601)+~P1(x3603)+~P1(x3604)+~P1(x3605)+~P3(x3604,x3601,a2)+~P3(x3605,x3601,a2)+~P9(x3604,a2,x3602)+~P9(x3605,a2,x3603)+~P7(x3601,a1)+E(f9(x3601,x3602,x3603),x3603)+P9(x3603,a2,f9(x3601,x3602,x3603)) % 97.28/97.29 [361]~P1(x3613)+~P1(x3611)+~P1(x3612)+~P1(x3614)+~P1(x3615)+~P3(x3614,x3611,a2)+~P3(x3615,x3611,a2)+~P9(x3614,a2,x3612)+~P9(x3615,a2,x3613)+~P7(x3611,a1)+E(f9(x3611,x3612,x3613),x3612)+P9(x3612,a2,f9(x3611,x3612,x3613)) % 97.28/97.29 [424]~P1(x4243)+~P1(x4242)+~P1(x4241)+~P1(x4244)+~P1(x4245)+~P3(x4244,x4241,a2)+~P3(x4245,x4241,a2)+~P9(x4244,a2,x4242)+~P9(x4245,a2,x4243)+~P7(x4241,a1)+E(f9(x4241,x4242,x4243),x4243)+P3(f9(x4241,x4242,x4243),x4243,a2)+P1(f14(x4241,x4242,x4243)) % 97.28/97.29 [425]~P1(x4253)+~P1(x4252)+~P1(x4251)+~P1(x4254)+~P1(x4255)+~P3(x4254,x4251,a2)+~P3(x4255,x4251,a2)+~P9(x4254,a2,x4252)+~P9(x4255,a2,x4253)+~P7(x4251,a1)+E(f9(x4251,x4252,x4253),x4252)+P3(f9(x4251,x4252,x4253),x4252,a2)+P1(f15(x4251,x4252,x4253)) % 97.28/97.29 [430]~P1(x4303)+~P1(x4302)+~P1(x4301)+~P1(x4304)+~P1(x4305)+~P3(x4304,x4301,a2)+~P3(x4305,x4301,a2)+~P9(x4304,a2,x4302)+~P9(x4305,a2,x4303)+~P7(x4301,a1)+E(f9(x4301,x4302,x4303),x4303)+P3(f14(x4301,x4302,x4303),x4303,a2)+P3(f9(x4301,x4302,x4303),x4303,a2) % 97.28/97.30 [431]~P1(x4313)+~P1(x4312)+~P1(x4311)+~P1(x4314)+~P1(x4315)+~P3(x4314,x4311,a2)+~P3(x4315,x4311,a2)+~P9(x4314,a2,x4312)+~P9(x4315,a2,x4313)+~P7(x4311,a1)+E(f9(x4311,x4312,x4313),x4312)+P3(f15(x4311,x4312,x4313),x4312,a2)+P3(f9(x4311,x4312,x4313),x4312,a2) % 97.28/97.30 [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),x4443)+P9(f14(x4441,x4442,x4443),a2,f9(x4441,x4442,x4443))+P3(f9(x4441,x4442,x4443),x4443,a2) % 97.28/97.30 [445]~P1(x4453)+~P1(x4452)+~P1(x4451)+~P1(x4454)+~P1(x4455)+~P3(x4454,x4451,a2)+~P3(x4455,x4451,a2)+~P9(x4454,a2,x4452)+~P9(x4455,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) % 97.28/97.30 %EqnAxiom % 97.28/97.30 [1]E(x11,x11) % 97.28/97.30 [2]E(x22,x21)+~E(x21,x22) % 97.28/97.30 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 97.28/97.30 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 97.28/97.30 [5]~E(x51,x52)+E(f20(x51),f20(x52)) % 97.28/97.30 [6]~E(x61,x62)+E(f21(x61),f21(x62)) % 97.28/97.30 [7]~E(x71,x72)+E(f22(x71),f22(x72)) % 97.28/97.30 [8]~E(x81,x82)+E(f24(x81),f24(x82)) % 97.28/97.30 [9]~E(x91,x92)+E(f25(x91),f25(x92)) % 97.28/97.30 [10]~E(x101,x102)+E(f4(x101),f4(x102)) % 97.28/97.30 [11]~E(x111,x112)+E(f5(x111),f5(x112)) % 97.28/97.30 [12]~E(x121,x122)+E(f9(x121,x123,x124),f9(x122,x123,x124)) % 97.28/97.30 [13]~E(x131,x132)+E(f9(x133,x131,x134),f9(x133,x132,x134)) % 97.28/97.30 [14]~E(x141,x142)+E(f9(x143,x144,x141),f9(x143,x144,x142)) % 97.28/97.30 [15]~E(x151,x152)+E(f15(x151,x153,x154),f15(x152,x153,x154)) % 97.28/97.30 [16]~E(x161,x162)+E(f15(x163,x161,x164),f15(x163,x162,x164)) % 97.28/97.30 [17]~E(x171,x172)+E(f15(x173,x174,x171),f15(x173,x174,x172)) % 97.28/97.30 [18]~E(x181,x182)+E(f14(x181,x183,x184),f14(x182,x183,x184)) % 97.28/97.30 [19]~E(x191,x192)+E(f14(x193,x191,x194),f14(x193,x192,x194)) % 97.28/97.30 [20]~E(x201,x202)+E(f14(x203,x204,x201),f14(x203,x204,x202)) % 97.28/97.30 [21]~E(x211,x212)+E(f10(x211,x213,x214),f10(x212,x213,x214)) % 97.28/97.30 [22]~E(x221,x222)+E(f10(x223,x221,x224),f10(x223,x222,x224)) % 97.28/97.30 [23]~E(x231,x232)+E(f10(x233,x234,x231),f10(x233,x234,x232)) % 97.28/97.30 [24]~E(x241,x242)+E(f12(x241,x243,x244),f12(x242,x243,x244)) % 97.28/97.30 [25]~E(x251,x252)+E(f12(x253,x251,x254),f12(x253,x252,x254)) % 97.28/97.30 [26]~E(x261,x262)+E(f12(x263,x264,x261),f12(x263,x264,x262)) % 97.28/97.30 [27]~E(x271,x272)+E(f13(x271,x273,x274),f13(x272,x273,x274)) % 97.28/97.30 [28]~E(x281,x282)+E(f13(x283,x281,x284),f13(x283,x282,x284)) % 97.28/97.30 [29]~E(x291,x292)+E(f13(x293,x294,x291),f13(x293,x294,x292)) % 97.28/97.30 [30]~E(x301,x302)+E(f11(x301,x303,x304),f11(x302,x303,x304)) % 97.28/97.30 [31]~E(x311,x312)+E(f11(x313,x311,x314),f11(x313,x312,x314)) % 97.28/97.30 [32]~E(x321,x322)+E(f11(x323,x324,x321),f11(x323,x324,x322)) % 97.28/97.30 [33]~E(x331,x332)+E(f19(x331,x333,x334,x335),f19(x332,x333,x334,x335)) % 97.28/97.30 [34]~E(x341,x342)+E(f19(x343,x341,x344,x345),f19(x343,x342,x344,x345)) % 97.28/97.30 [35]~E(x351,x352)+E(f19(x353,x354,x351,x355),f19(x353,x354,x352,x355)) % 97.28/97.30 [36]~E(x361,x362)+E(f19(x363,x364,x365,x361),f19(x363,x364,x365,x362)) % 97.28/97.30 [37]~E(x371,x372)+E(f23(x371,x373,x374,x375),f23(x372,x373,x374,x375)) % 97.28/97.30 [38]~E(x381,x382)+E(f23(x383,x381,x384,x385),f23(x383,x382,x384,x385)) % 97.28/97.30 [39]~E(x391,x392)+E(f23(x393,x394,x391,x395),f23(x393,x394,x392,x395)) % 97.28/97.30 [40]~E(x401,x402)+E(f23(x403,x404,x405,x401),f23(x403,x404,x405,x402)) % 97.28/97.30 [41]~E(x411,x412)+E(f8(x411,x413,x414),f8(x412,x413,x414)) % 97.28/97.30 [42]~E(x421,x422)+E(f8(x423,x421,x424),f8(x423,x422,x424)) % 97.28/97.30 [43]~E(x431,x432)+E(f8(x433,x434,x431),f8(x433,x434,x432)) % 97.28/97.30 [44]~E(x441,x442)+E(f7(x441,x443),f7(x442,x443)) % 97.28/97.30 [45]~E(x451,x452)+E(f7(x453,x451),f7(x453,x452)) % 97.28/97.30 [46]~P1(x461)+P1(x462)+~E(x461,x462) % 97.28/97.30 [47]P9(x472,x473,x474)+~E(x471,x472)+~P9(x471,x473,x474) % 97.28/97.30 [48]P9(x483,x482,x484)+~E(x481,x482)+~P9(x483,x481,x484) % 97.28/97.30 [49]P9(x493,x494,x492)+~E(x491,x492)+~P9(x493,x494,x491) % 97.28/97.30 [50]P3(x502,x503,x504)+~E(x501,x502)+~P3(x501,x503,x504) % 97.28/97.30 [51]P3(x513,x512,x514)+~E(x511,x512)+~P3(x513,x511,x514) % 97.28/97.30 [52]P3(x523,x524,x522)+~E(x521,x522)+~P3(x523,x524,x521) % 97.28/97.30 [53]P7(x532,x533)+~E(x531,x532)+~P7(x531,x533) % 97.28/97.30 [54]P7(x543,x542)+~E(x541,x542)+~P7(x543,x541) % 97.28/97.30 [55]P10(x552,x553,x554)+~E(x551,x552)+~P10(x551,x553,x554) % 97.28/97.30 [56]P10(x563,x562,x564)+~E(x561,x562)+~P10(x563,x561,x564) % 97.28/97.30 [57]P10(x573,x574,x572)+~E(x571,x572)+~P10(x573,x574,x571) % 97.28/97.30 [58]~P2(x581)+P2(x582)+~E(x581,x582) % 97.28/97.30 [59]~P5(x591)+P5(x592)+~E(x591,x592) % 97.28/97.30 [60]~P8(x601)+P8(x602)+~E(x601,x602) % 97.28/97.30 [61]P4(x612,x613,x614)+~E(x611,x612)+~P4(x611,x613,x614) % 97.28/97.30 [62]P4(x623,x622,x624)+~E(x621,x622)+~P4(x623,x621,x624) % 97.28/97.30 [63]P4(x633,x634,x632)+~E(x631,x632)+~P4(x633,x634,x631) % 97.28/97.30 [64]~P6(x641)+P6(x642)+~E(x641,x642) % 97.28/97.30 % 97.28/97.30 %------------------------------------------- % 97.28/97.30 cnf(446,plain, % 97.28/97.30 (~P1(x4461)+~P1(x4461)+P10(x4461,x4462,x4461)+~P2(x4462)), % 97.28/97.30 inference(equality_inference,[],[100])). % 97.28/97.30 cnf(448,plain, % 97.28/97.30 (~P1(a29)+~P3(a29,a28,a2)), % 97.28/97.30 inference(equality_inference,[],[102])). % 97.28/97.30 cnf(449,plain, % 97.28/97.30 (~P1(a28)+~P9(a29,a2,a28)), % 97.28/97.30 inference(equality_inference,[],[103])). % 97.28/97.30 cnf(450,plain, % 97.28/97.30 (~P1(a28)+~P10(a29,a2,a28)), % 97.28/97.30 inference(equality_inference,[],[104])). % 97.28/97.30 cnf(451,plain, % 97.28/97.30 (~P1(a29)+~P9(a28,a2,a29)), % 97.28/97.30 inference(equality_inference,[],[105])). % 97.28/97.30 cnf(452,plain, % 97.28/97.30 (~P1(a29)+~P10(a28,a2,a29)), % 97.28/97.30 inference(equality_inference,[],[106])). % 97.28/97.30 cnf(454,plain, % 97.28/97.30 (~P1(a29)+~P1(x4541)+~P9(x4541,a2,a29)+~P3(x4541,a28,a2)), % 97.28/97.30 inference(equality_inference,[],[136])). % 97.28/97.30 cnf(458,plain, % 97.28/97.30 (~P1(x4581)+~P1(x4581)+~P1(x4582)+~P10(x4581,a2,x4582)+~P7(x4581,a1)+P1(f9(x4581,x4582,x4581))), % 97.28/97.30 inference(equality_inference,[],[146])). % 97.28/97.30 cnf(460,plain, % 97.28/97.30 (~P1(x4601)+~P1(x4601)+~P1(x4602)+~P10(x4601,a2,x4602)+~P7(x4601,a1)+P1(f9(x4601,x4601,x4602))), % 97.28/97.30 inference(equality_inference,[],[148])). % 97.28/97.30 cnf(466,plain, % 97.28/97.30 (~P1(x4661)+~P1(x4661)+~P1(x4662)+~P10(x4661,a2,x4662)+~P7(x4661,a1)+P10(x4662,a2,f9(x4661,x4661,x4662))), % 97.28/97.30 inference(equality_inference,[],[166])). % 97.28/97.30 cnf(468,plain, % 97.28/97.30 (~P1(x4681)+~P1(x4681)+~P1(x4682)+~P10(x4681,a2,x4682)+~P7(x4681,a1)+P10(x4681,a2,f9(x4681,x4682,x4681))), % 97.28/97.30 inference(equality_inference,[],[168])). % 97.28/97.30 cnf(470,plain, % 97.28/97.30 (~P1(x4701)+~P1(x4701)+~P1(x4702)+~P10(x4701,a2,x4702)+~P7(x4701,a1)+P10(x4702,a2,f9(x4701,x4702,x4701))), % 97.28/97.30 inference(equality_inference,[],[170])). % 97.28/97.30 cnf(472,plain, % 97.28/97.30 (~P1(x4721)+~P1(x4721)+~P1(x4722)+~P10(x4721,a2,x4722)+~P7(x4721,a1)+P10(x4721,a2,f9(x4721,x4721,x4722))), % 97.28/97.30 inference(equality_inference,[],[172])). % 97.28/97.30 cnf(544,plain, % 97.28/97.30 (~P3(a29,a28,a2)), % 97.28/97.30 inference(scs_inference,[],[69,448])). % 97.28/97.30 cnf(545,plain, % 97.28/97.30 (~P9(a29,a2,a28)), % 97.28/97.30 inference(scs_inference,[],[68,449])). % 97.28/97.30 cnf(546,plain, % 97.28/97.30 (~P10(a29,a2,a28)), % 97.28/97.30 inference(scs_inference,[],[68,450])). % 97.28/97.30 cnf(547,plain, % 97.28/97.30 (~P9(a28,a2,a29)), % 97.28/97.30 inference(scs_inference,[],[69,451])). % 97.28/97.30 cnf(548,plain, % 97.28/97.30 (~P10(a28,a2,a29)), % 97.28/97.30 inference(scs_inference,[],[69,452])). % 97.28/97.30 cnf(550,plain, % 97.28/97.30 (~P1(x5501)+~P9(x5501,a2,a29)+~P3(x5501,a28,a2)), % 97.28/97.30 inference(scs_inference,[],[69,454])). % 97.28/97.30 cnf(551,plain, % 97.28/97.30 (~E(a28,a27)), % 97.28/97.30 inference(scs_inference,[],[67,78,104])). % 97.28/97.30 cnf(555,plain, % 97.28/97.30 (~P10(a29,a2,a26)), % 97.28/97.30 inference(scs_inference,[],[66,67,77,78,104,106,134])). % 97.28/97.30 cnf(558,plain, % 97.28/97.30 (~E(a27,a26)), % 97.28/97.30 inference(scs_inference,[],[66,67,77,78,104,106,134,55,57])). % 97.28/97.30 cnf(559,plain, % 97.28/97.30 (P7(a28,a1)), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,77,78,73,104,106,134,55,57,118])). % 97.28/97.30 cnf(563,plain, % 97.28/97.30 (P10(a1,a2,a1)), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,69,77,78,70,73,104,106,134,55,57,118,121,446])). % 97.28/97.30 cnf(565,plain, % 97.28/97.30 (P7(a26,a1)), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,69,75,77,78,70,73,104,106,134,55,57,118,121,446,119])). % 97.28/97.30 cnf(567,plain, % 97.28/97.30 (~P4(a1,a1,a2)), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,69,75,77,78,70,73,104,106,134,55,57,118,121,446,119,137])). % 97.28/97.30 cnf(569,plain, % 97.28/97.30 (P9(a1,a2,a28)), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,69,75,77,78,70,73,104,106,134,55,57,118,121,446,119,137,123])). % 97.28/97.30 cnf(571,plain, % 97.28/97.30 (P10(a1,a2,a26)), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,69,75,77,78,70,73,104,106,134,55,57,118,121,446,119,137,123,124])). % 97.28/97.30 cnf(573,plain, % 97.28/97.30 (P1(f9(a28,a26,a28))), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,69,75,77,78,70,73,104,106,134,55,57,118,121,446,119,137,123,124,458])). % 97.28/97.30 cnf(575,plain, % 97.28/97.30 (P1(f9(a28,a28,a26))), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,69,75,77,78,70,73,104,106,134,55,57,118,121,446,119,137,123,124,458,460])). % 97.28/97.30 cnf(577,plain, % 97.28/97.30 (P10(a26,a2,f9(a28,a28,a26))), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,69,75,77,78,70,73,104,106,134,55,57,118,121,446,119,137,123,124,458,460,466])). % 97.28/97.30 cnf(579,plain, % 97.28/97.30 (P10(a28,a2,f9(a28,a26,a28))), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,69,75,77,78,70,73,104,106,134,55,57,118,121,446,119,137,123,124,458,460,466,468])). % 97.28/97.30 cnf(581,plain, % 97.28/97.30 (P10(a26,a2,f9(a28,a26,a28))), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,69,75,77,78,70,73,104,106,134,55,57,118,121,446,119,137,123,124,458,460,466,468,470])). % 97.28/97.30 cnf(583,plain, % 97.28/97.30 (P10(a28,a2,f9(a28,a28,a26))), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,69,75,77,78,70,73,104,106,134,55,57,118,121,446,119,137,123,124,458,460,466,468,470,472])). % 97.28/97.30 cnf(585,plain, % 97.28/97.30 (P7(a27,a1)), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,69,75,76,77,78,70,72,73,104,106,134,55,57,118,121,446,119,137,123,124,458,460,466,468,470,472,120])). % 97.28/97.30 cnf(587,plain, % 97.28/97.30 (~P10(a27,a2,a26)), % 97.28/97.30 inference(scs_inference,[],[65,66,67,68,69,75,76,77,78,70,72,73,104,106,134,55,57,118,121,446,119,137,123,124,458,460,466,468,470,472,120,151])). % 97.28/97.30 cnf(600,plain, % 97.28/97.30 (~E(a1,a28)), % 97.28/97.30 inference(scs_inference,[],[544,575,583,74,106,51])). % 97.28/97.30 cnf(602,plain, % 97.28/97.30 (~P10(a29,a2,f9(a28,a28,a26))), % 97.28/97.30 inference(scs_inference,[],[544,548,575,583,74,106,51,57,134])). % 97.28/97.30 cnf(604,plain, % 97.28/97.30 (~E(a1,a29)), % 97.28/97.30 inference(scs_inference,[],[544,545,548,575,583,569,74,106,51,57,134,47])). % 97.28/97.30 cnf(606,plain, % 97.28/97.30 (P7(a29,a1)), % 97.28/97.30 inference(scs_inference,[],[65,544,545,548,575,583,577,569,69,74,106,51,57,134,47,55,118])). % 97.28/97.30 cnf(612,plain, % 97.28/97.30 (P9(a1,a2,a29)), % 97.28/97.30 inference(scs_inference,[],[65,544,545,546,548,573,575,583,577,569,69,74,70,106,51,57,134,47,55,118,121,137,123])). % 97.28/97.30 cnf(616,plain, % 97.28/97.30 (P1(f9(a26,f9(a28,a26,a28),a26))), % 97.28/97.30 inference(scs_inference,[],[65,544,545,546,548,573,575,581,583,577,569,69,68,66,565,74,70,106,51,57,134,47,55,118,121,137,123,124,458])). % 97.28/97.30 cnf(624,plain, % 97.28/97.30 (P1(f9(a26,a26,f9(a28,a26,a28)))), % 97.28/97.30 inference(scs_inference,[],[65,544,545,546,548,573,575,581,583,577,569,69,68,66,565,74,70,106,51,57,134,47,55,118,121,137,123,124,458,466,472,468,460])). % 97.28/97.30 cnf(630,plain, % 97.28/97.30 (~P10(f9(a28,a28,a26),a2,a29)), % 97.28/97.30 inference(scs_inference,[],[65,544,545,546,547,548,573,575,581,583,577,569,69,68,66,565,74,70,106,51,57,134,47,55,118,121,137,123,124,458,466,472,468,460,470,149,151])). % 97.28/97.30 cnf(646,plain, % 97.28/97.30 (~P10(a29,a2,f9(a28,a26,a28))), % 97.28/97.30 inference(scs_inference,[],[579,573,106,134])). % 97.28/97.30 cnf(653,plain, % 97.28/97.30 (P10(a1,a2,a27)), % 97.28/97.30 inference(scs_inference,[],[65,602,76,78,624,579,67,573,69,70,74,106,134,57,121,137,124])). % 97.28/97.30 cnf(655,plain, % 97.28/97.30 (P10(f9(a28,a26,a28),a2,f9(a28,a28,f9(a28,a26,a28)))), % 97.28/97.30 inference(scs_inference,[],[65,602,76,78,624,579,67,573,69,68,559,70,74,106,134,57,121,137,124,466])). % 97.28/97.30 cnf(657,plain, % 97.28/97.30 (P10(a28,a2,f9(a28,f9(a28,a26,a28),a28))), % 97.28/97.30 inference(scs_inference,[],[65,602,76,78,624,579,67,573,69,68,559,70,74,106,134,57,121,137,124,466,468])). % 97.28/97.30 cnf(659,plain, % 97.28/97.30 (P1(f9(a28,f9(a28,a26,a28),a28))), % 97.28/97.30 inference(scs_inference,[],[65,602,76,78,624,579,67,573,69,68,559,70,74,106,134,57,121,137,124,466,468,458])). % 97.28/97.30 cnf(661,plain, % 97.28/97.30 (P10(a28,a2,f9(a28,a28,f9(a28,a26,a28)))), % 97.28/97.30 inference(scs_inference,[],[65,602,76,78,624,579,67,573,69,68,559,70,74,106,134,57,121,137,124,466,468,458,472])). % 97.28/97.30 cnf(663,plain, % 97.28/97.30 (P1(f9(a28,a28,f9(a28,a26,a28)))), % 97.28/97.30 inference(scs_inference,[],[65,602,76,78,624,579,67,573,69,68,559,70,74,106,134,57,121,137,124,466,468,458,472,460])). % 97.28/97.30 cnf(665,plain, % 97.28/97.30 (P10(f9(a28,a26,a28),a2,f9(a28,f9(a28,a26,a28),a28))), % 97.28/97.30 inference(scs_inference,[],[65,602,76,78,624,579,67,573,69,68,559,70,74,106,134,57,121,137,124,466,468,458,472,460,470])). % 97.28/97.30 cnf(667,plain, % 97.28/97.30 (~P10(a27,a2,f9(a28,a28,a26))), % 97.28/97.30 inference(scs_inference,[],[65,602,76,78,624,579,575,67,573,69,68,559,70,74,106,134,57,121,137,124,466,468,458,472,460,470,151])). % 97.28/97.30 cnf(683,plain, % 97.28/97.30 (~P10(a29,a2,f9(a28,a28,f9(a28,a26,a28)))), % 97.28/97.30 inference(scs_inference,[],[663,661,106,134])). % 97.28/97.30 cnf(691,plain, % 97.28/97.30 (P10(a1,a2,a29)), % 97.28/97.30 inference(scs_inference,[],[65,646,612,78,663,655,661,69,73,70,106,134,55,57,137,121,124])). % 97.28/97.30 cnf(693,plain, % 97.28/97.30 (P10(a27,a2,f9(a29,a29,a27))), % 97.28/97.30 inference(scs_inference,[],[65,646,612,78,663,655,661,67,69,606,73,70,106,134,55,57,137,121,124,466])). % 97.28/97.30 cnf(695,plain, % 97.28/97.30 (P10(a29,a2,f9(a29,a27,a29))), % 97.28/97.30 inference(scs_inference,[],[65,646,612,78,663,655,661,67,69,606,73,70,106,134,55,57,137,121,124,466,468])). % 97.28/97.30 cnf(697,plain, % 97.28/97.30 (P10(a29,a2,f9(a29,a29,a27))), % 97.28/97.30 inference(scs_inference,[],[65,646,612,78,663,655,661,67,69,606,73,70,106,134,55,57,137,121,124,466,468,472])). % 97.28/97.30 cnf(699,plain, % 97.28/97.30 (P1(f9(a29,a27,a29))), % 97.28/97.30 inference(scs_inference,[],[65,646,612,78,663,655,661,67,69,606,73,70,106,134,55,57,137,121,124,466,468,472,458])). % 97.28/97.30 cnf(701,plain, % 97.28/97.30 (P1(f9(a29,a29,a27))), % 97.28/97.30 inference(scs_inference,[],[65,646,612,78,663,655,661,67,69,606,73,70,106,134,55,57,137,121,124,466,468,472,458,460])). % 97.28/97.30 cnf(703,plain, % 97.28/97.30 (P10(a27,a2,f9(a29,a27,a29))), % 97.28/97.30 inference(scs_inference,[],[65,646,612,78,663,655,661,67,69,606,73,70,106,134,55,57,137,121,124,466,468,472,458,460,470])). % 97.28/97.30 cnf(705,plain, % 97.28/97.30 (~P10(a27,a2,f9(a28,a26,a28))), % 97.28/97.30 inference(scs_inference,[],[65,646,612,78,663,655,661,67,69,573,606,73,70,106,134,55,57,137,121,124,466,468,472,458,460,470,151])). % 97.28/97.30 cnf(725,plain, % 97.28/97.30 (~P10(a29,a2,f9(a28,f9(a28,a26,a28),a28))), % 97.28/97.30 inference(scs_inference,[],[701,659,697,657,104,106,134])). % 97.28/97.30 cnf(727,plain, % 97.28/97.30 (~E(f9(a29,a27,a29),f9(a28,a26,a28))), % 97.28/97.30 inference(scs_inference,[],[701,659,705,703,697,657,104,106,134,57])). % 97.28/97.30 cnf(730,plain, % 97.28/97.30 (~P4(a1,f9(a29,a29,a27),a2)), % 97.28/97.30 inference(scs_inference,[],[683,701,659,705,703,697,657,69,74,70,104,106,134,57,121,137])). % 97.28/97.30 cnf(734,plain, % 97.28/97.30 (P10(a28,a2,f9(a28,f9(a28,a28,a26),a28))), % 97.28/97.30 inference(scs_inference,[],[683,583,701,659,705,703,697,657,575,68,69,559,74,70,104,106,134,57,121,137,466,468])). % 97.28/97.30 cnf(736,plain, % 97.28/97.30 (P1(f9(a28,f9(a28,a28,a26),a28))), % 97.28/97.30 inference(scs_inference,[],[683,583,701,659,705,703,697,657,575,68,69,559,74,70,104,106,134,57,121,137,466,468,458])). % 97.28/97.30 cnf(738,plain, % 97.28/97.30 (P10(a28,a2,f9(a28,a28,f9(a28,a28,a26)))), % 97.28/97.30 inference(scs_inference,[],[683,583,701,659,705,703,697,657,575,68,69,559,74,70,104,106,134,57,121,137,466,468,458,472])). % 97.28/97.30 cnf(742,plain, % 97.28/97.30 (P1(f9(a28,a28,f9(a28,a28,a26)))), % 97.28/97.30 inference(scs_inference,[],[683,583,701,659,705,703,697,657,575,68,69,559,74,70,104,106,134,57,121,137,466,468,458,472,470,460])). % 97.28/97.30 cnf(744,plain, % 97.28/97.30 (~P10(f9(a28,a26,a28),a2,a29)), % 97.28/97.30 inference(scs_inference,[],[683,548,583,579,701,659,705,703,697,657,575,573,68,69,559,74,70,104,106,134,57,121,137,466,468,458,472,470,460,151])). % 97.28/97.30 cnf(759,plain, % 97.28/97.30 (~P10(a29,a2,f9(a28,a28,f9(a28,a28,a26)))), % 97.28/97.30 inference(scs_inference,[],[742,738,106,134])). % 97.28/97.30 cnf(774,plain, % 97.28/97.30 (P1(f9(a26,f9(a28,a28,a26),a26))), % 97.28/97.30 inference(scs_inference,[],[725,577,665,742,744,738,575,66,69,565,74,70,106,134,57,137,121,466,470,468,472,458])). % 97.28/97.30 cnf(776,plain, % 97.28/97.30 (P1(f9(a26,a26,f9(a28,a28,a26)))), % 97.28/97.30 inference(scs_inference,[],[725,577,665,742,744,738,575,66,69,565,74,70,106,134,57,137,121,466,470,468,472,458,460])). % 97.28/97.30 cnf(778,plain, % 97.28/97.30 (~P10(a26,a2,a29)), % 97.28/97.30 inference(scs_inference,[],[725,548,577,77,665,742,744,738,575,66,69,68,565,74,70,106,134,57,137,121,466,470,468,472,458,460,151])). % 97.28/97.30 cnf(785,plain, % 97.28/97.30 (~P10(a29,a2,f9(a28,f9(a28,a28,a26),a28))), % 97.28/97.30 inference(scs_inference,[],[736,734,106,134])). % 97.28/97.30 cnf(802,plain, % 97.28/97.30 (P1(f9(a27,a27,f9(a29,a29,a27)))), % 97.28/97.30 inference(scs_inference,[],[759,655,774,736,693,734,744,701,67,69,74,70,585,106,134,57,121,137,466,470,468,458,472,460])). % 97.28/97.30 cnf(809,plain, % 97.28/97.30 (~E(f9(a29,a27,a29),a26)), % 97.28/97.30 inference(scs_inference,[],[555,695,57])). % 97.28/97.30 cnf(826,plain, % 97.28/97.30 (~P10(f9(a28,a28,f9(a28,a28,a26)),a2,a29)), % 97.28/97.30 inference(scs_inference,[],[548,738,802,742,68,69,74,70,57,137,121,151])). % 97.28/97.30 cnf(852,plain, % 97.28/97.30 (~P10(f9(a28,f9(a28,a28,a26),a28),a2,a29)), % 97.28/97.30 inference(scs_inference,[],[548,734,630,776,736,575,69,68,74,70,57,137,121,151])). % 97.28/97.30 cnf(876,plain, % 97.28/97.30 (~P4(a26,a27,a2)), % 97.28/97.30 inference(scs_inference,[],[555,697,587,616,67,74,70,57,137,121])). % 97.28/97.30 cnf(932,plain, % 97.28/97.30 (~P10(a27,a2,f9(a28,f9(a28,a28,a26),a28))), % 97.28/97.30 inference(scs_inference,[],[785,78,826,736,742,575,67,69,74,70,57,137,121,151])). % 97.28/97.30 cnf(945,plain, % 97.28/97.30 (~P10(a27,a2,a28)), % 97.28/97.30 inference(scs_inference,[],[546,78,852,736,67,69,68,74,70,57,137,121,151])). % 97.28/97.30 cnf(953,plain, % 97.28/97.30 (~E(f9(a29,a29,a27),f9(a28,a26,a28))), % 97.28/97.30 inference(scs_inference,[],[646,697,57])). % 97.28/97.30 cnf(1049,plain, % 97.28/97.30 (P10(a27,a2,f9(a27,a27,f9(a29,a27,a29)))), % 97.28/97.30 inference(scs_inference,[],[546,697,699,67,932,703,585,70,57,121,466,470,468,460,472])). % 97.28/97.30 cnf(1051,plain, % 97.28/97.30 (P1(f9(a27,f9(a29,a27,a29),a27))), % 97.28/97.30 inference(scs_inference,[],[546,697,699,67,932,703,585,70,57,121,466,470,468,460,472,458])). % 97.28/97.30 cnf(1067,plain, % 97.28/97.30 (~P4(a28,a27,a2)), % 97.28/97.30 inference(scs_inference,[],[67,1051,945,1049,74,70,57,137,121])). % 97.28/97.30 cnf(1296,plain, % 97.28/97.30 (P10(f9(a28,a28,a26),a2,f9(a28,a28,a26))), % 97.28/97.30 inference(scs_inference,[],[575,70,100])). % 97.28/97.30 cnf(1331,plain, % 97.28/97.30 (P10(a27,a2,a27)), % 97.28/97.30 inference(scs_inference,[],[67,70,100])). % 97.28/97.30 cnf(1342,plain, % 97.28/97.30 (P10(a26,a2,a26)), % 97.28/97.30 inference(scs_inference,[],[66,70,100])). % 97.28/97.30 cnf(1346,plain, % 97.28/97.30 (P10(a28,a2,a28)), % 97.28/97.30 inference(scs_inference,[],[68,1342,70,56,100])). % 97.28/97.30 cnf(1360,plain, % 97.28/97.30 (P10(a29,a2,a29)), % 97.28/97.30 inference(scs_inference,[],[68,69,1346,70,106,56,100])). % 97.28/97.30 cnf(1605,plain, % 97.28/97.30 (P10(a28,a2,f9(a28,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[1346,68,559,470])). % 97.28/97.30 cnf(1607,plain, % 97.28/97.30 (P1(f9(a28,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[1346,68,559,470,460])). % 97.28/97.30 cnf(1609,plain, % 97.28/97.30 (~P10(f9(a28,a28,a28),a2,a29)), % 97.28/97.30 inference(scs_inference,[],[548,1346,68,69,559,70,470,460,151])). % 97.28/97.30 cnf(1613,plain, % 97.28/97.30 (~P10(a29,a2,f9(a28,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[548,1346,68,69,559,70,470,460,151,56,57,134])). % 97.28/97.30 cnf(1634,plain, % 97.28/97.30 (~P4(f9(a28,a28,a28),a29,a2)), % 97.28/97.30 inference(scs_inference,[],[1613,69,70,121])). % 97.28/97.30 cnf(1852,plain, % 97.28/97.30 (P10(a29,a2,f9(a29,a29,a29))), % 97.28/97.30 inference(scs_inference,[],[1360,69,606,468])). % 97.28/97.30 cnf(1854,plain, % 97.28/97.30 (P1(f9(a29,a29,a29))), % 97.28/97.30 inference(scs_inference,[],[1360,69,606,468,460])). % 97.28/97.30 cnf(1856,plain, % 97.28/97.30 (~P10(f9(a29,a29,a29),a2,a26)), % 97.28/97.30 inference(scs_inference,[],[555,1360,66,69,606,70,468,460,151])). % 97.28/97.30 cnf(1879,plain, % 97.28/97.30 (~E(f9(a29,a29,a27),f9(a28,a28,a26))), % 97.28/97.30 inference(scs_inference,[],[602,697,57])). % 97.28/97.30 cnf(2343,plain, % 97.28/97.30 (P10(a26,a2,f9(a26,a26,a26))), % 97.28/97.30 inference(scs_inference,[],[1342,66,565,458,470])). % 97.28/97.30 cnf(2347,plain, % 97.28/97.30 (P1(f9(a29,a29,f9(a29,a27,a29)))), % 97.28/97.30 inference(scs_inference,[],[69,695,1342,66,699,565,606,458,470,468,460])). % 97.28/97.30 cnf(2349,plain, % 97.28/97.30 (P10(a29,a2,f9(a29,a29,f9(a29,a27,a29)))), % 97.28/97.30 inference(scs_inference,[],[69,695,1342,66,699,565,606,458,470,468,460,472])). % 97.28/97.30 cnf(2369,plain, % 97.28/97.30 (~E(f9(a26,a26,a26),a29)), % 97.28/97.30 inference(scs_inference,[],[778,2343,2347,2349,104,57])). % 97.28/97.30 cnf(2408,plain, % 97.28/97.30 (~E(f9(a29,a29,a29),f9(a28,a28,a26))), % 97.28/97.30 inference(scs_inference,[],[602,1852,57])). % 97.28/97.30 cnf(2649,plain, % 97.28/97.30 (P1(f9(a29,a29,f9(a29,a29,a29)))), % 97.28/97.30 inference(scs_inference,[],[1852,1854,69,606,466,468,460])). % 97.28/97.30 cnf(2651,plain, % 97.28/97.30 (P1(f9(a29,f9(a29,a29,a29),a29))), % 97.28/97.30 inference(scs_inference,[],[1852,1854,69,606,466,468,460,458])). % 97.28/97.30 cnf(2653,plain, % 97.28/97.30 (P10(a29,a2,f9(a29,a29,f9(a29,a29,a29)))), % 97.28/97.30 inference(scs_inference,[],[1852,1854,69,606,466,468,460,458,472])). % 97.28/97.30 cnf(2655,plain, % 97.28/97.30 (P10(f9(a29,a29,a29),a2,f9(a29,f9(a29,a29,a29),a29))), % 97.28/97.30 inference(scs_inference,[],[1852,1854,69,606,466,468,460,458,472,470])). % 97.28/97.30 cnf(2677,plain, % 97.28/97.30 (P10(a27,a2,f9(a27,a27,a27))), % 97.28/97.30 inference(scs_inference,[],[70,1331,67,1856,2649,2651,2655,2653,74,585,57,104,137,466])). % 97.28/97.30 cnf(2679,plain, % 97.28/97.30 (P1(f9(a27,a27,a27))), % 97.28/97.30 inference(scs_inference,[],[70,1331,67,1856,2649,2651,2655,2653,74,585,57,104,137,466,458])). % 97.28/97.30 cnf(3044,plain, % 97.28/97.30 (~P10(f9(a27,a27,a27),a2,f9(a28,a28,a26))), % 97.28/97.30 inference(scs_inference,[],[2677,575,67,2679,667,70,57,151])). % 97.28/97.30 cnf(3050,plain, % 97.28/97.30 (~P10(f9(a27,a27,a27),a2,a26)), % 97.28/97.30 inference(scs_inference,[],[2677,66,67,2679,587,70,57,151])). % 97.28/97.30 cnf(3055,plain, % 97.28/97.30 (~E(f9(a27,a27,a27),f9(a28,a26,a28))), % 97.28/97.30 inference(scs_inference,[],[2677,705,57])). % 97.28/97.30 cnf(3056,plain, % 97.28/97.30 (~P10(f9(a27,a27,a27),a2,f9(a28,a26,a28))), % 97.28/97.30 inference(scs_inference,[],[2677,573,67,2679,705,70,57,151])). % 97.28/97.30 cnf(3075,plain, % 97.28/97.30 (~P10(a28,a2,f9(a29,a29,a27))), % 97.28/97.30 inference(scs_inference,[],[558,1605,1607,697,701,2,128,130,132,134])). % 97.28/97.30 cnf(3082,plain, % 97.28/97.30 (~P3(x30821,f7(a2,a1),a2)), % 97.28/97.30 inference(scs_inference,[],[65,558,3044,1296,1605,72,1607,697,701,70,2,128,130,132,134,133,55,115,137])). % 97.28/97.30 cnf(3086,plain, % 97.28/97.30 (~P9(f9(a27,a27,a27),a2,f9(a28,a28,a26))), % 97.28/97.30 inference(scs_inference,[],[65,558,3044,1296,1605,72,1607,697,2679,575,701,70,2,128,130,132,134,133,55,115,137,121,124])). % 97.28/97.30 cnf(3088,plain, % 97.28/97.30 (P1(f10(a1,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[65,558,3044,1296,1605,72,1607,73,697,2679,575,701,68,70,2,128,130,132,134,133,55,115,137,121,124,173])). % 97.28/97.30 cnf(3090,plain, % 97.28/97.30 (P3(f8(a1,a2,a1),a1,a2)), % 97.28/97.30 inference(scs_inference,[],[65,558,567,3044,1296,563,1605,72,1607,73,697,2679,575,701,68,70,2,128,130,132,134,133,55,115,137,121,124,173,185])). % 97.28/97.30 cnf(3092,plain, % 97.28/97.30 (P10(a28,a2,f10(a1,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[65,558,567,3044,1296,563,1605,72,1607,73,697,2679,575,701,68,70,2,128,130,132,134,133,55,115,137,121,124,173,185,200])). % 97.28/97.30 cnf(3094,plain, % 97.28/97.30 (P10(a29,a2,f10(a1,a29,a29))), % 97.28/97.30 inference(scs_inference,[],[65,558,567,3044,1296,563,1605,72,1607,73,697,2679,575,701,68,74,69,70,2,128,130,132,134,133,55,115,137,121,124,173,185,200,201])). % 97.28/97.30 cnf(3102,plain, % 97.28/97.30 (P1(f7(a2,a1))), % 97.28/97.30 inference(scs_inference,[],[65,558,567,3044,3050,1296,571,563,1605,72,1607,73,697,2679,575,701,66,68,74,69,70,2,128,130,132,134,133,55,115,137,121,124,173,185,200,201,151,80,106,117])). % 97.28/97.30 cnf(3104,plain, % 97.28/97.30 (P10(f10(a1,a28,a28),a2,f10(a1,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[65,558,567,3044,3050,1296,571,563,1605,72,1607,73,697,2679,575,701,66,68,74,69,70,2,128,130,132,134,133,55,115,137,121,124,173,185,200,201,151,80,106,117,446])). % 97.28/97.30 cnf(3108,plain, % 97.28/97.30 (P1(f9(a28,a26,a26))), % 97.28/97.30 inference(scs_inference,[],[65,558,567,3044,3050,1296,571,563,1605,77,72,1607,73,697,2679,575,701,66,68,74,559,69,70,2,128,130,132,134,133,55,115,137,121,124,173,185,200,201,151,80,106,117,446,100,182])). % 97.28/97.30 cnf(3110,plain, % 97.28/97.30 (P10(a26,a2,f9(a28,a26,a26))), % 97.28/97.30 inference(scs_inference,[],[65,558,567,3044,3050,1296,571,563,1605,77,72,1607,73,697,2679,575,701,66,68,74,559,69,70,2,128,130,132,134,133,55,115,137,121,124,173,185,200,201,151,80,106,117,446,100,182,216])). % 97.28/97.30 cnf(3122,plain, % 97.28/97.30 (~E(a28,a1)), % 97.28/97.30 inference(scs_inference,[],[600,2])). % 97.28/97.30 cnf(3127,plain, % 97.28/97.30 (~P9(a28,a2,a27)), % 97.28/97.30 inference(scs_inference,[],[600,3092,3088,67,78,2,130,128,132])). % 97.28/97.30 cnf(3129,plain, % 97.28/97.30 (~P10(a29,a2,f10(a1,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[600,3092,3088,67,78,2,130,128,132,134])). % 97.28/97.30 cnf(3134,plain, % 97.28/97.30 (P1(f8(a1,a2,a1))), % 97.28/97.30 inference(scs_inference,[],[65,600,3075,3092,3088,3090,67,78,70,2,130,128,132,134,133,57,116])). % 97.28/97.30 cnf(3138,plain, % 97.28/97.30 (~P10(a28,a2,a27)), % 97.28/97.30 inference(scs_inference,[],[65,551,600,3102,3075,3092,3088,3090,67,78,68,70,2,130,128,132,134,133,57,116,446,125])). % 97.28/97.30 cnf(3142,plain, % 97.28/97.30 (~E(a1,f7(a2,a1))), % 97.28/97.30 inference(scs_inference,[],[65,551,600,3102,3075,3092,3082,3088,3090,67,78,68,70,2,130,128,132,134,133,57,116,446,125,95,51])). % 97.28/97.30 cnf(3144,plain, % 97.28/97.30 (P4(f7(a2,a27),a27,a2)), % 97.28/97.30 inference(scs_inference,[],[65,551,600,3102,3075,3092,3082,3088,3090,67,72,78,68,70,2,130,128,132,134,133,57,116,446,125,95,51,115])). % 97.28/97.30 cnf(3146,plain, % 97.28/97.30 (P1(f7(a2,a27))), % 97.28/97.30 inference(scs_inference,[],[65,551,600,3102,3075,3092,3082,3088,3090,67,72,78,68,70,2,130,128,132,134,133,57,116,446,125,95,51,115,117])). % 97.28/97.30 cnf(3162,plain, % 97.28/97.30 (~E(a29,a1)), % 97.28/97.30 inference(scs_inference,[],[604,2])). % 97.28/97.30 cnf(3169,plain, % 97.28/97.30 (~P10(a28,a2,f9(a29,a29,a29))), % 97.28/97.30 inference(scs_inference,[],[604,583,1852,575,1854,2,128,130,132,134])). % 97.28/97.30 cnf(3173,plain, % 97.28/97.30 (~P3(x31731,f7(a2,a27),a2)), % 97.28/97.30 inference(scs_inference,[],[604,3144,583,67,1852,575,1854,70,2,128,130,132,134,133,137])). % 97.28/97.30 cnf(3175,plain, % 97.28/97.30 (P10(a27,a2,f7(a2,a27))), % 97.28/97.30 inference(scs_inference,[],[604,3144,583,67,1852,575,1854,70,2,128,130,132,134,133,137,121])). % 97.28/97.30 cnf(3183,plain, % 97.28/97.30 (P10(a28,a2,f23(a2,a1,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[65,604,3127,3110,3086,3108,3144,571,71,583,67,73,2679,1852,575,1854,66,76,68,70,2,128,130,132,134,133,137,121,123,150,151,428])). % 97.28/97.30 cnf(3185,plain, % 97.28/97.30 (P10(a29,a2,f23(a2,a1,a29,a29))), % 97.28/97.30 inference(scs_inference,[],[65,604,3127,3110,3086,3108,3144,571,71,583,67,73,2679,1852,575,1854,66,76,68,74,69,70,2,128,130,132,134,133,137,121,123,150,151,428,429])). % 97.28/97.30 cnf(3189,plain, % 97.28/97.30 (~P10(a28,a2,a1)), % 97.28/97.30 inference(scs_inference,[],[65,604,3127,3122,3110,3086,3108,3144,571,71,583,67,73,2679,1852,575,1854,66,76,68,74,69,70,2,128,130,132,134,133,137,121,123,150,151,428,429,96,125])). % 97.28/97.30 cnf(3204,plain, % 97.28/97.30 (~P10(a28,a2,f9(a29,a27,a29))), % 97.28/97.30 inference(scs_inference,[],[809,579,695,573,699,2,130,128,132,134])). % 97.28/97.30 cnf(3210,plain, % 97.28/97.30 (~P9(a29,a2,a1)), % 97.28/97.30 inference(scs_inference,[],[65,809,3146,545,579,695,573,699,569,68,69,70,2,130,128,132,134,133,101,150])). % 97.28/97.30 cnf(3233,plain, % 97.28/97.30 (P1(f23(a2,a1,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[65,876,1879,3104,3129,3134,3144,71,73,68,70,2,61,55,126,423])). % 97.28/97.30 cnf(3238,plain, % 97.28/97.30 (~E(a29,f23(a2,a1,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[2369,3183,3233,2,106])). % 97.28/97.30 cnf(3251,plain, % 97.28/97.30 (~P10(a29,a2,f23(a2,a1,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[3138,2369,3183,3233,3173,3090,70,2,106,130,51,133,57,446,550,134])). % 97.28/97.30 cnf(3253,plain, % 97.28/97.30 (~P4(a27,a28,a2)), % 97.28/97.30 inference(scs_inference,[],[3138,2369,3183,3233,3173,3090,68,70,2,106,130,51,133,57,446,550,134,121])). % 97.28/97.30 cnf(3258,plain, % 97.28/97.30 (P4(f7(a2,a26),a26,a2)), % 97.28/97.30 inference(scs_inference,[],[2408,72,66,70,2,115])). % 97.28/97.30 cnf(3260,plain, % 97.28/97.30 (P1(f7(a2,a26))), % 97.28/97.30 inference(scs_inference,[],[2408,72,66,70,2,115,117])). % 97.28/97.30 cnf(3266,plain, % 97.28/97.30 (P10(a26,a2,f7(a2,a26))), % 97.28/97.30 inference(scs_inference,[],[2408,3146,72,66,70,2,115,117,446,104,121])). % 97.28/97.30 cnf(3271,plain, % 97.28/97.30 (~P3(x32711,f7(a2,a26),a2)), % 97.28/97.30 inference(scs_inference,[],[3055,3258,66,70,2,137])). % 97.28/97.30 cnf(3303,plain, % 97.28/97.30 (~E(f10(a1,a28,a28),a1)), % 97.28/97.30 inference(scs_inference,[],[3189,727,3271,3090,3092,2,51,57])). % 97.28/97.30 cnf(3308,plain, % 97.28/97.30 (~P10(a29,a2,a1)), % 97.28/97.30 inference(scs_inference,[],[65,3189,3162,727,3271,3251,3210,3134,3090,3092,69,70,2,51,57,105,121,125])). % 97.28/97.30 cnf(3320,plain, % 97.28/97.30 (~P9(f9(a28,a28,a28),a2,a29)), % 97.28/97.30 inference(scs_inference,[],[953,1609,1607,69,70,2,124])). % 97.28/97.30 cnf(3336,plain, % 97.28/97.30 (~E(a1,f9(a28,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[3238,3320,612,2,47])). % 97.28/97.30 cnf(3356,plain, % 97.28/97.30 (~E(f23(a2,a1,a29,a29),a1)), % 97.28/97.30 inference(scs_inference,[],[3185,3303,3308,2,57])). % 97.28/97.30 cnf(3357,plain, % 97.28/97.30 (P4(f7(a2,a28),a28,a2)), % 97.28/97.30 inference(scs_inference,[],[3185,3303,3308,72,68,70,2,57,115])). % 97.28/97.30 cnf(3359,plain, % 97.28/97.30 (P1(f7(a2,a28))), % 97.28/97.30 inference(scs_inference,[],[3185,3303,3308,72,68,70,2,57,115,117])). % 97.28/97.30 cnf(3363,plain, % 97.28/97.30 (P10(a28,a2,f7(a2,a28))), % 97.28/97.30 inference(scs_inference,[],[3185,3303,3308,3102,72,68,70,2,57,115,117,128,121])). % 97.28/97.30 cnf(3368,plain, % 97.28/97.30 (~E(a29,f7(a2,a28))), % 97.28/97.30 inference(scs_inference,[],[3336,3359,3363,2,106])). % 97.28/97.30 cnf(3372,plain, % 97.28/97.30 (~P10(a29,a2,f7(a2,a28))), % 97.28/97.30 inference(scs_inference,[],[3336,3359,3363,2,106,130,134])). % 97.28/97.30 cnf(3376,plain, % 97.28/97.30 (~P3(x33761,f7(a2,a28),a2)), % 97.28/97.30 inference(scs_inference,[],[3336,3359,3363,3357,68,70,2,106,130,134,133,137])). % 97.28/97.30 cnf(3387,plain, % 97.28/97.30 (~E(a1,f7(a2,a28))), % 97.28/97.30 inference(scs_inference,[],[3368,3376,3090,2,51])). % 97.28/97.30 cnf(3389,plain, % 97.28/97.30 (P1(f10(a1,a29,a29))), % 97.28/97.30 inference(scs_inference,[],[65,3368,3376,3090,74,69,2,51,173])). % 97.28/97.30 cnf(3397,plain, % 97.28/97.30 (~P10(a28,a2,f10(a1,a29,a29))), % 97.28/97.30 inference(scs_inference,[],[65,3368,3376,3094,3090,3102,74,69,2,51,173,104,128,132,134])). % 97.28/97.30 cnf(3408,plain, % 97.28/97.30 (~P10(f10(a1,a28,a28),a2,f10(a1,a29,a29))), % 97.28/97.30 inference(scs_inference,[],[3389,3397,3356,3372,3088,3092,68,69,70,2,121,151])). % 97.28/97.30 cnf(3425,plain, % 97.28/97.30 (~E(a1,f9(a28,a28,a26))), % 97.28/97.30 inference(scs_inference,[],[1067,3387,630,3144,691,2,61,55])). % 97.28/97.30 cnf(3430,plain, % 97.28/97.30 (P10(a1,a2,f7(a2,a27))), % 97.28/97.30 inference(scs_inference,[],[65,1067,3175,3387,3320,630,3144,691,653,612,3260,3146,1607,67,69,70,2,61,55,128,150,151])). % 97.28/97.30 cnf(3435,plain, % 97.28/97.30 (~E(f7(a2,a28),f9(a29,a29,a29))), % 97.28/97.30 inference(scs_inference,[],[3425,3169,3363,2,57])). % 97.28/97.30 cnf(3450,plain, % 97.28/97.30 (P10(f10(a1,a29,a29),a2,f10(a1,a29,a29))), % 97.28/97.30 inference(scs_inference,[],[65,3435,3430,3173,3389,3108,3146,606,67,78,69,70,2,185,182,132,446])). % 97.28/97.30 cnf(3482,plain, % 97.28/97.30 (~E(f10(a1,a29,a29),f10(a1,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[3253,3450,3142,3357,3408,2,61,55])). % 97.28/97.30 cnf(3493,plain, % 97.28/97.30 (P4(f7(a2,a29),a29,a2)), % 97.28/97.30 inference(scs_inference,[],[3482,3204,3363,72,69,70,2,57,115])). % 97.28/97.30 cnf(3757,plain, % 97.28/97.30 (~P9(a27,a2,a26)), % 97.28/97.30 inference(scs_inference,[],[67,587,66,70,119,124])). % 97.28/97.30 cnf(3759,plain, % 97.28/97.30 (~P9(a27,a2,a1)), % 97.28/97.30 inference(scs_inference,[],[67,587,75,66,70,65,119,124,150])). % 97.28/97.30 cnf(3764,plain, % 97.28/97.30 (~E(f7(a2,a29),f9(a28,a28,a28))), % 97.28/97.30 inference(scs_inference,[],[3757,1634,3493,75,47,61])). % 97.28/97.30 cnf(3770,plain, % 97.28/97.30 (~P9(f9(a27,a27,a27),a2,f9(a28,a26,a28))), % 97.28/97.30 inference(scs_inference,[],[67,3757,1634,3056,3493,75,2679,573,66,70,47,61,123,2,116,124])). % 97.28/97.30 cnf(3772,plain, % 97.28/97.30 (~P10(a27,a2,a1)), % 97.28/97.30 inference(scs_inference,[],[67,3757,3759,1634,3056,3493,75,2679,573,66,70,65,47,61,123,2,116,124,125])). % 97.28/97.30 cnf(3780,plain, % 97.28/97.30 (~P10(f7(a2,a27),a2,a1)), % 97.28/97.30 inference(scs_inference,[],[67,3772,3764,3770,3175,3308,3094,3146,2679,573,70,65,2,57,123,151])). % 97.28/97.30 cnf(3818,plain, % 97.28/97.30 (P10(a28,a2,f7(a2,a26))), % 97.28/97.30 inference(scs_inference,[],[68,3266,3260,77,66,70,151])). % 97.28/97.30 cnf(3825,plain, % 97.28/97.30 (P1(f23(a2,a1,a28,a29))), % 97.28/97.30 inference(scs_inference,[],[68,3266,71,3260,77,73,66,70,74,65,69,151,130,46,133,423])). % 97.28/97.30 cnf(3834,plain, % 97.28/97.30 (P10(a29,a2,f10(a1,a28,a29))), % 97.28/97.30 inference(scs_inference,[],[68,3818,3260,73,74,65,69,106,134,200])). % 97.28/97.30 cnf(3836,plain, % 97.28/97.30 (P10(a29,a2,f10(a1,a29,a28))), % 97.28/97.30 inference(scs_inference,[],[68,3818,3260,73,74,65,69,106,134,200,201])). % 97.28/97.30 cnf(3838,plain, % 97.28/97.30 (P10(a29,a2,f23(a2,a1,a29,a28))), % 97.28/97.30 inference(scs_inference,[],[68,3818,71,3260,73,70,74,65,69,106,134,200,201,429])). % 97.28/97.30 cnf(3840,plain, % 97.28/97.30 (P10(a29,a2,f23(a2,a1,a28,a29))), % 97.28/97.30 inference(scs_inference,[],[68,3818,71,3260,73,70,74,65,69,106,134,200,201,429,428])). % 97.28/97.30 cnf(3845,plain, % 97.28/97.30 (~P1(f10(a1,a28,a29))+~P9(a28,a2,f10(a1,a28,a29))), % 97.28/97.30 inference(scs_inference,[],[68,3825,3818,71,3260,73,70,74,65,69,106,134,200,201,429,428,2,128,132])). % 97.28/97.30 cnf(3863,plain, % 97.28/97.30 (P1(f10(a1,a28,a29))), % 97.28/97.30 inference(scs_inference,[],[68,3840,3825,73,74,65,69,132,104,134,173])). % 97.28/97.30 cnf(3871,plain, % 97.28/97.30 (~P9(a28,a2,f10(a1,a28,a29))), % 97.28/97.30 inference(scs_inference,[],[68,730,3840,3834,3780,3825,3146,73,70,74,65,69,132,104,134,173,2,61,128,124,3845])). % 97.28/97.30 cnf(3875,plain, % 97.28/97.30 (~P10(a28,a2,f10(a1,a28,a29))), % 97.28/97.30 inference(scs_inference,[],[3863,3834,134])). % 97.28/97.30 cnf(3877,plain, % 97.28/97.30 (P10(f10(a1,a28,a29),a2,f10(a1,a28,a29))), % 97.28/97.30 inference(scs_inference,[],[3863,3834,70,134,446])). % 97.28/97.30 cnf(3879,plain, % 97.28/97.30 (P1(f23(a2,a1,a29,a28))), % 97.28/97.30 inference(scs_inference,[],[68,3863,3834,71,73,70,74,65,69,134,446,423])). % 97.28/97.30 cnf(3887,plain, % 97.28/97.30 (~P9(f9(a27,a27,a27),a2,a26)), % 97.28/97.30 inference(scs_inference,[],[68,3863,3838,3834,3050,71,2679,73,66,70,74,65,69,134,446,423,128,132,118,124])). % 97.28/97.30 cnf(3889,plain, % 97.28/97.30 (P10(a28,a2,f10(a1,a29,a28))), % 97.28/97.30 inference(scs_inference,[],[68,3863,3838,3834,3050,71,2679,73,66,70,74,65,69,134,446,423,128,132,118,124,200])). % 97.28/97.30 cnf(3903,plain, % 97.28/97.30 ($false), % 97.28/97.30 inference(scs_inference,[],[68,3877,3879,3875,3887,3889,3836,3871,3863,2679,73,66,70,74,65,69,55,57,134,117,123,100,228]), % 97.28/97.30 ['proof']). % 97.28/97.30 % SZS output end Proof % 97.28/97.30 % Total time :95.760000s %------------------------------------------------------------------------------