%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM022+4 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : 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:48 EDT 2024 % Result : Theorem 5.24s 5.37s % Output : CNFRefutation 5.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : COM022+4 : TPTP v8.2.0. Released v4.0.0. % 0.00/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.08/0.30 % Computer : n032.cluster.edu % 0.08/0.30 % Model : x86_64 x86_64 % 0.08/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.30 % Memory : 8042.1875MB % 0.08/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.30 % CPULimit : 300 % 0.08/0.30 % WCLimit : 300 % 0.08/0.30 % DateTime : Fri Jun 21 00:14:38 EDT 2024 % 0.08/0.30 % CPUTime : % 0.14/0.52 start to proof:theBenchmark % 5.24/5.35 %------------------------------------------- % 5.24/5.35 % File :CSE---1.7 % 5.24/5.35 % Problem :theBenchmark % 5.24/5.35 % Transform :cnf % 5.24/5.35 % Format :tptp:raw % 5.24/5.35 % Command :java -jar mcs_scs.jar %d %s % 5.24/5.35 % 5.24/5.35 % Result :Theorem 3.440000s % 5.24/5.36 % Output :CNFRefutation 3.440000s % 5.24/5.36 %------------------------------------------- % 5.24/5.36 %------------------------------------------------------------------------------ % 5.24/5.36 % File : COM022+4 : TPTP v8.2.0. Released v4.0.0. % 5.24/5.36 % Domain : Computing Theory % 5.24/5.36 % Problem : Newman's lemma on rewriting systems 03_01_07, 03 expansion % 5.24/5.36 % Version : Especial. % 5.24/5.36 % English : % 5.24/5.36 % 5.24/5.36 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 5.24/5.36 % : [PV+07] Paskevich et al. (2007), Reasoning Inside a Formula an % 5.24/5.36 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 5.24/5.36 % Source : [Pas08] % 5.24/5.36 % Names : newman_03_01_07.03 [Pas08] % 5.24/5.36 % 5.24/5.36 % Status : Theorem % 5.24/5.36 % Rating : 0.25 v8.2.0, 0.22 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.13 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.13 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.16 v6.1.0, 0.23 v6.0.0, 0.22 v5.5.0, 0.37 v5.4.0, 0.39 v5.3.0, 0.44 v5.2.0, 0.30 v5.1.0, 0.38 v5.0.0, 0.46 v4.1.0, 0.48 v4.0.1, 0.65 v4.0.0 % 5.24/5.36 % Syntax : Number of formulae : 19 ( 1 unt; 6 def) % 5.24/5.36 % Number of atoms : 244 ( 18 equ) % 5.24/5.36 % Maximal formula atoms : 96 ( 12 avg) % 5.24/5.36 % Number of connectives : 227 ( 2 ~; 50 |; 137 &) % 5.24/5.36 % ( 6 <=>; 32 =>; 0 <=; 0 <~>) % 5.24/5.36 % Maximal formula depth : 34 ( 9 avg) % 5.24/5.36 % Maximal term depth : 1 ( 1 avg) % 5.24/5.36 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 5.24/5.36 % Number of functors : 4 ( 4 usr; 4 con; 0-0 aty) % 5.24/5.36 % Number of variables : 81 ( 48 !; 33 ?) % 5.24/5.36 % SPC : FOF_THM_RFO_SEQ % 5.24/5.36 % 5.24/5.36 % Comments : Problem generated by the SAD system [VLP07] % 5.24/5.36 %------------------------------------------------------------------------------ % 5.24/5.36 fof(mElmSort,axiom, % 5.24/5.36 ! [W0] : % 5.24/5.36 ( aElement0(W0) % 5.24/5.36 => $true ) ). % 5.24/5.36 % 5.24/5.36 fof(mRelSort,axiom, % 5.24/5.36 ! [W0] : % 5.24/5.36 ( aRewritingSystem0(W0) % 5.24/5.36 => $true ) ). % 5.24/5.36 % 5.24/5.36 fof(mReduct,axiom, % 5.24/5.36 ! [W0,W1] : % 5.24/5.36 ( ( aElement0(W0) % 5.24/5.36 & aRewritingSystem0(W1) ) % 5.24/5.36 => ! [W2] : % 5.24/5.36 ( aReductOfIn0(W2,W0,W1) % 5.24/5.36 => aElement0(W2) ) ) ). % 5.24/5.36 % 5.24/5.36 fof(mWFOrd,axiom, % 5.24/5.36 ! [W0,W1] : % 5.24/5.36 ( ( aElement0(W0) % 5.24/5.36 & aElement0(W1) ) % 5.24/5.36 => ( iLess0(W0,W1) % 5.24/5.36 => $true ) ) ). % 5.24/5.36 % 5.24/5.36 fof(mTCbr,axiom, % 5.24/5.36 ! [W0,W1,W2] : % 5.24/5.36 ( ( aElement0(W0) % 5.24/5.36 & aRewritingSystem0(W1) % 5.24/5.36 & aElement0(W2) ) % 5.24/5.36 => ( sdtmndtplgtdt0(W0,W1,W2) % 5.24/5.36 => $true ) ) ). % 5.24/5.36 % 5.24/5.36 fof(mTCDef,definition, % 5.24/5.36 ! [W0,W1,W2] : % 5.24/5.36 ( ( aElement0(W0) % 5.24/5.36 & aRewritingSystem0(W1) % 5.24/5.36 & aElement0(W2) ) % 5.24/5.36 => ( sdtmndtplgtdt0(W0,W1,W2) % 5.24/5.36 <=> ( aReductOfIn0(W2,W0,W1) % 5.24/5.36 | ? [W3] : % 5.24/5.36 ( aElement0(W3) % 5.24/5.36 & aReductOfIn0(W3,W0,W1) % 5.24/5.36 & sdtmndtplgtdt0(W3,W1,W2) ) ) ) ) ). % 5.24/5.36 % 5.24/5.36 fof(mTCTrans,axiom, % 5.24/5.36 ! [W0,W1,W2,W3] : % 5.24/5.36 ( ( aElement0(W0) % 5.24/5.36 & aRewritingSystem0(W1) % 5.24/5.36 & aElement0(W2) % 5.24/5.36 & aElement0(W3) ) % 5.24/5.36 => ( ( sdtmndtplgtdt0(W0,W1,W2) % 5.24/5.36 & sdtmndtplgtdt0(W2,W1,W3) ) % 5.24/5.36 => sdtmndtplgtdt0(W0,W1,W3) ) ) ). % 5.24/5.36 % 5.24/5.36 fof(mTCRDef,definition, % 5.24/5.36 ! [W0,W1,W2] : % 5.24/5.36 ( ( aElement0(W0) % 5.24/5.36 & aRewritingSystem0(W1) % 5.24/5.36 & aElement0(W2) ) % 5.24/5.36 => ( sdtmndtasgtdt0(W0,W1,W2) % 5.24/5.36 <=> ( W0 = W2 % 5.24/5.36 | sdtmndtplgtdt0(W0,W1,W2) ) ) ) ). % 5.24/5.36 % 5.24/5.36 fof(mTCRTrans,axiom, % 5.24/5.36 ! [W0,W1,W2,W3] : % 5.24/5.36 ( ( aElement0(W0) % 5.24/5.36 & aRewritingSystem0(W1) % 5.24/5.36 & aElement0(W2) % 5.24/5.36 & aElement0(W3) ) % 5.24/5.36 => ( ( sdtmndtasgtdt0(W0,W1,W2) % 5.24/5.36 & sdtmndtasgtdt0(W2,W1,W3) ) % 5.24/5.36 => sdtmndtasgtdt0(W0,W1,W3) ) ) ). % 5.24/5.36 % 5.24/5.36 fof(mCRDef,definition, % 5.24/5.36 ! [W0] : % 5.24/5.36 ( aRewritingSystem0(W0) % 5.24/5.36 => ( isConfluent0(W0) % 5.24/5.36 <=> ! [W1,W2,W3] : % 5.24/5.36 ( ( aElement0(W1) % 5.24/5.36 & aElement0(W2) % 5.24/5.36 & aElement0(W3) % 5.24/5.36 & sdtmndtasgtdt0(W1,W0,W2) % 5.24/5.36 & sdtmndtasgtdt0(W1,W0,W3) ) % 5.24/5.36 => ? [W4] : % 5.24/5.36 ( aElement0(W4) % 5.24/5.36 & sdtmndtasgtdt0(W2,W0,W4) % 5.24/5.36 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 5.24/5.36 % 5.24/5.36 fof(mWCRDef,definition, % 5.24/5.36 ! [W0] : % 5.24/5.36 ( aRewritingSystem0(W0) % 5.24/5.36 => ( isLocallyConfluent0(W0) % 5.24/5.36 <=> ! [W1,W2,W3] : % 5.24/5.36 ( ( aElement0(W1) % 5.24/5.36 & aElement0(W2) % 5.24/5.36 & aElement0(W3) % 5.24/5.36 & aReductOfIn0(W2,W1,W0) % 5.24/5.36 & aReductOfIn0(W3,W1,W0) ) % 5.24/5.36 => ? [W4] : % 5.24/5.36 ( aElement0(W4) % 5.24/5.36 & sdtmndtasgtdt0(W2,W0,W4) % 5.24/5.36 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 5.24/5.36 % 5.24/5.36 fof(mTermin,definition, % 5.24/5.36 ! [W0] : % 5.24/5.36 ( aRewritingSystem0(W0) % 5.24/5.36 => ( isTerminating0(W0) % 5.24/5.36 <=> ! [W1,W2] : % 5.24/5.36 ( ( aElement0(W1) % 5.24/5.36 & aElement0(W2) ) % 5.24/5.36 => ( sdtmndtplgtdt0(W1,W0,W2) % 5.24/5.36 => iLess0(W2,W1) ) ) ) ) ). % 5.24/5.36 % 5.24/5.36 fof(mNFRDef,definition, % 5.24/5.36 ! [W0,W1] : % 5.24/5.36 ( ( aElement0(W0) % 5.24/5.36 & aRewritingSystem0(W1) ) % 5.24/5.36 => ! [W2] : % 5.24/5.36 ( aNormalFormOfIn0(W2,W0,W1) % 5.24/5.36 <=> ( aElement0(W2) % 5.24/5.36 & sdtmndtasgtdt0(W0,W1,W2) % 5.24/5.36 & ~ ? [W3] : aReductOfIn0(W3,W2,W1) ) ) ) ). % 5.24/5.36 % 5.24/5.36 fof(mTermNF,axiom, % 5.24/5.36 ! [W0] : % 5.24/5.36 ( ( aRewritingSystem0(W0) % 5.24/5.36 & isTerminating0(W0) ) % 5.24/5.36 => ! [W1] : % 5.24/5.36 ( aElement0(W1) % 5.24/5.36 => ? [W2] : aNormalFormOfIn0(W2,W1,W0) ) ) ). % 5.24/5.36 % 5.24/5.36 fof(m__656,hypothesis, % 5.24/5.36 aRewritingSystem0(xR) ). % 5.24/5.36 % 5.24/5.36 fof(m__656_01,hypothesis, % 5.24/5.36 ( ! [W0,W1,W2] : % 5.24/5.36 ( ( aElement0(W0) % 5.24/5.36 & aElement0(W1) % 5.24/5.36 & aElement0(W2) % 5.24/5.36 & aReductOfIn0(W1,W0,xR) % 5.24/5.36 & aReductOfIn0(W2,W0,xR) ) % 5.24/5.36 => ? [W3] : % 5.24/5.36 ( aElement0(W3) % 5.24/5.36 & ( W1 = W3 % 5.24/5.36 | ( ( aReductOfIn0(W3,W1,xR) % 5.24/5.36 | ? [W4] : % 5.24/5.36 ( aElement0(W4) % 5.24/5.36 & aReductOfIn0(W4,W1,xR) % 5.24/5.36 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 5.24/5.36 & sdtmndtplgtdt0(W1,xR,W3) ) ) % 5.24/5.36 & sdtmndtasgtdt0(W1,xR,W3) % 5.24/5.36 & ( W2 = W3 % 5.24/5.36 | ( ( aReductOfIn0(W3,W2,xR) % 5.24/5.36 | ? [W4] : % 5.24/5.36 ( aElement0(W4) % 5.24/5.36 & aReductOfIn0(W4,W2,xR) % 5.24/5.36 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 5.24/5.36 & sdtmndtplgtdt0(W2,xR,W3) ) ) % 5.24/5.36 & sdtmndtasgtdt0(W2,xR,W3) ) ) % 5.24/5.36 & isLocallyConfluent0(xR) % 5.24/5.36 & ! [W0,W1] : % 5.24/5.36 ( ( aElement0(W0) % 5.24/5.36 & aElement0(W1) ) % 5.24/5.36 => ( ( aReductOfIn0(W1,W0,xR) % 5.24/5.36 | ? [W2] : % 5.24/5.36 ( aElement0(W2) % 5.24/5.36 & aReductOfIn0(W2,W0,xR) % 5.24/5.36 & sdtmndtplgtdt0(W2,xR,W1) ) % 5.24/5.36 | sdtmndtplgtdt0(W0,xR,W1) ) % 5.24/5.36 => iLess0(W1,W0) ) ) % 5.24/5.36 & isTerminating0(xR) ) ). % 5.24/5.36 % 5.24/5.36 fof(m__731,hypothesis, % 5.24/5.36 ( aElement0(xa) % 5.24/5.36 & aElement0(xb) % 5.24/5.36 & aElement0(xc) ) ). % 5.24/5.36 % 5.24/5.36 fof(m__715,hypothesis, % 5.24/5.36 ! [W0,W1,W2] : % 5.24/5.36 ( ( aElement0(W0) % 5.24/5.36 & aElement0(W1) % 5.24/5.36 & aElement0(W2) % 5.24/5.36 & ( W0 = W1 % 5.24/5.36 | aReductOfIn0(W1,W0,xR) % 5.24/5.36 | ? [W3] : % 5.24/5.36 ( aElement0(W3) % 5.24/5.36 & aReductOfIn0(W3,W0,xR) % 5.24/5.36 & sdtmndtplgtdt0(W3,xR,W1) ) % 5.24/5.36 | sdtmndtplgtdt0(W0,xR,W1) % 5.24/5.36 | sdtmndtasgtdt0(W0,xR,W1) ) % 5.24/5.36 & ( W0 = W2 % 5.24/5.36 | aReductOfIn0(W2,W0,xR) % 5.24/5.36 | ? [W3] : % 5.24/5.36 ( aElement0(W3) % 5.24/5.36 & aReductOfIn0(W3,W0,xR) % 5.24/5.36 & sdtmndtplgtdt0(W3,xR,W2) ) % 5.24/5.36 | sdtmndtplgtdt0(W0,xR,W2) % 5.24/5.36 | sdtmndtasgtdt0(W0,xR,W2) ) ) % 5.24/5.36 => ( iLess0(W0,xa) % 5.24/5.36 => ? [W3] : % 5.24/5.36 ( aElement0(W3) % 5.24/5.36 & ( W1 = W3 % 5.24/5.36 | ( ( aReductOfIn0(W3,W1,xR) % 5.24/5.37 | ? [W4] : % 5.24/5.37 ( aElement0(W4) % 5.24/5.37 & aReductOfIn0(W4,W1,xR) % 5.24/5.37 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 5.24/5.37 & sdtmndtplgtdt0(W1,xR,W3) ) ) % 5.24/5.37 & sdtmndtasgtdt0(W1,xR,W3) % 5.24/5.37 & ( W2 = W3 % 5.24/5.37 | ( ( aReductOfIn0(W3,W2,xR) % 5.24/5.37 | ? [W4] : % 5.24/5.37 ( aElement0(W4) % 5.24/5.37 & aReductOfIn0(W4,W2,xR) % 5.24/5.37 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 5.24/5.37 & sdtmndtplgtdt0(W2,xR,W3) ) ) % 5.24/5.37 & sdtmndtasgtdt0(W2,xR,W3) ) ) ) ). % 5.24/5.37 % 5.24/5.37 fof(m__,conjecture, % 5.24/5.37 ( ( ( ( aReductOfIn0(xb,xa,xR) % 5.24/5.37 | ? [W0] : % 5.24/5.37 ( aElement0(W0) % 5.24/5.37 & aReductOfIn0(W0,xa,xR) % 5.24/5.37 & sdtmndtplgtdt0(W0,xR,xb) ) % 5.24/5.37 | sdtmndtplgtdt0(xa,xR,xb) ) % 5.24/5.37 & ( aReductOfIn0(xc,xa,xR) % 5.24/5.37 | ? [W0] : % 5.24/5.37 ( aElement0(W0) % 5.24/5.37 & aReductOfIn0(W0,xa,xR) % 5.24/5.37 & sdtmndtplgtdt0(W0,xR,xc) ) % 5.24/5.37 | sdtmndtplgtdt0(xa,xR,xc) ) ) % 5.24/5.37 => ? [W0] : % 5.24/5.37 ( aElement0(W0) % 5.24/5.37 & aReductOfIn0(W0,xa,xR) % 5.24/5.37 & ( W0 = xb % 5.24/5.37 | ( ( aReductOfIn0(xb,W0,xR) % 5.24/5.37 | ? [W1] : % 5.24/5.37 ( aElement0(W1) % 5.24/5.37 & aReductOfIn0(W1,W0,xR) % 5.24/5.37 & sdtmndtplgtdt0(W1,xR,xb) ) ) % 5.24/5.37 & sdtmndtplgtdt0(W0,xR,xb) ) ) % 5.24/5.37 & sdtmndtasgtdt0(W0,xR,xb) % 5.24/5.37 & ? [W1] : % 5.24/5.37 ( aElement0(W1) % 5.24/5.37 & aReductOfIn0(W1,xa,xR) % 5.24/5.37 & ( W1 = xc % 5.24/5.37 | ( ( aReductOfIn0(xc,W1,xR) % 5.24/5.37 | ? [W2] : % 5.24/5.37 ( aElement0(W2) % 5.24/5.37 & aReductOfIn0(W2,W1,xR) % 5.24/5.37 & sdtmndtplgtdt0(W2,xR,xc) ) ) % 5.24/5.37 & sdtmndtplgtdt0(W1,xR,xc) ) ) % 5.24/5.37 & sdtmndtasgtdt0(W1,xR,xc) % 5.24/5.37 & ? [W2] : % 5.24/5.37 ( aElement0(W2) % 5.24/5.37 & ( W0 = W2 % 5.24/5.37 | ( ( aReductOfIn0(W2,W0,xR) % 5.24/5.37 | ? [W3] : % 5.24/5.37 ( aElement0(W3) % 5.24/5.37 & aReductOfIn0(W3,W0,xR) % 5.24/5.37 & sdtmndtplgtdt0(W3,xR,W2) ) ) % 5.24/5.37 & sdtmndtplgtdt0(W0,xR,W2) ) ) % 5.24/5.37 & sdtmndtasgtdt0(W0,xR,W2) % 5.24/5.37 & ( W1 = W2 % 5.24/5.37 | ( ( aReductOfIn0(W2,W1,xR) % 5.24/5.37 | ? [W3] : % 5.24/5.37 ( aElement0(W3) % 5.24/5.37 & aReductOfIn0(W3,W1,xR) % 5.24/5.37 & sdtmndtplgtdt0(W3,xR,W2) ) ) % 5.24/5.37 & sdtmndtplgtdt0(W1,xR,W2) ) ) % 5.24/5.37 & sdtmndtasgtdt0(W1,xR,W2) % 5.24/5.37 & ? [W3] : % 5.24/5.37 ( aElement0(W3) % 5.24/5.37 & ( W2 = W3 % 5.24/5.37 | ( ( aReductOfIn0(W3,W2,xR) % 5.24/5.37 | ? [W4] : % 5.24/5.37 ( aElement0(W4) % 5.24/5.37 & aReductOfIn0(W4,W2,xR) % 5.24/5.37 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 5.24/5.37 & sdtmndtplgtdt0(W2,xR,W3) ) ) % 5.24/5.37 & sdtmndtasgtdt0(W2,xR,W3) % 5.24/5.37 & ~ ? [W4] : aReductOfIn0(W4,W3,xR) % 5.24/5.37 & aNormalFormOfIn0(W3,W2,xR) % 5.24/5.37 & ( xb = W3 % 5.24/5.37 | ( ( aReductOfIn0(W3,xb,xR) % 5.24/5.37 | ? [W4] : % 5.24/5.37 ( aElement0(W4) % 5.24/5.37 & aReductOfIn0(W4,xb,xR) % 5.24/5.37 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 5.24/5.37 & sdtmndtplgtdt0(xb,xR,W3) ) ) % 5.24/5.37 & sdtmndtasgtdt0(xb,xR,W3) % 5.24/5.37 & ( xc = W3 % 5.24/5.37 | ( ( aReductOfIn0(W3,xc,xR) % 5.24/5.37 | ? [W4] : % 5.24/5.37 ( aElement0(W4) % 5.24/5.37 & aReductOfIn0(W4,xc,xR) % 5.24/5.37 & sdtmndtplgtdt0(W4,xR,W3) ) ) % 5.24/5.37 & sdtmndtplgtdt0(xc,xR,W3) ) ) % 5.24/5.37 & sdtmndtasgtdt0(xc,xR,W3) ) ) ) ) ) % 5.24/5.37 => ( ( ( xa = xb % 5.24/5.37 | ( ( aReductOfIn0(xb,xa,xR) % 5.24/5.37 | ? [W0] : % 5.24/5.37 ( aElement0(W0) % 5.24/5.37 & aReductOfIn0(W0,xa,xR) % 5.24/5.37 & sdtmndtplgtdt0(W0,xR,xb) ) ) % 5.24/5.37 & sdtmndtplgtdt0(xa,xR,xb) ) ) % 5.24/5.37 & sdtmndtasgtdt0(xa,xR,xb) % 5.24/5.37 & ( xa = xc % 5.24/5.37 | ( ( aReductOfIn0(xc,xa,xR) % 5.24/5.37 | ? [W0] : % 5.24/5.37 ( aElement0(W0) % 5.24/5.37 & aReductOfIn0(W0,xa,xR) % 5.24/5.37 & sdtmndtplgtdt0(W0,xR,xc) ) ) % 5.24/5.37 & sdtmndtplgtdt0(xa,xR,xc) ) ) % 5.24/5.37 & sdtmndtasgtdt0(xa,xR,xc) ) % 5.24/5.37 => ? [W0] : % 5.24/5.37 ( aElement0(W0) % 5.24/5.37 & ( xb = W0 % 5.24/5.37 | aReductOfIn0(W0,xb,xR) % 5.24/5.37 | ? [W1] : % 5.24/5.37 ( aElement0(W1) % 5.24/5.37 & aReductOfIn0(W1,xb,xR) % 5.24/5.37 & sdtmndtplgtdt0(W1,xR,W0) ) % 5.24/5.37 | sdtmndtplgtdt0(xb,xR,W0) % 5.24/5.37 | sdtmndtasgtdt0(xb,xR,W0) ) % 5.24/5.37 & ( xc = W0 % 5.24/5.37 | aReductOfIn0(W0,xc,xR) % 5.24/5.37 | ? [W1] : % 5.24/5.37 ( aElement0(W1) % 5.24/5.37 & aReductOfIn0(W1,xc,xR) % 5.24/5.37 & sdtmndtplgtdt0(W1,xR,W0) ) % 5.24/5.37 | sdtmndtplgtdt0(xc,xR,W0) % 5.24/5.37 | sdtmndtasgtdt0(xc,xR,W0) ) ) ) ) ). % 5.24/5.37 % 5.24/5.37 %------------------------------------------------------------------------------ % 5.24/5.37 %------------------------------------------- % 5.24/5.37 % Proof found % 5.24/5.37 % SZS status Theorem for theBenchmark % 5.24/5.37 % SZS output start Proof % 5.24/5.37 %ClaNum:486(EqnAxiom:65) % 5.24/5.37 %VarNum:5721(SingletonVarNum:1113) % 5.24/5.37 %MaxLitNum:13 % 5.24/5.37 %MaxfuncDepth:1 % 5.24/5.37 %SharedTerms:100 % 5.24/5.37 %goalClause: 72 73 78 87 88 107 108 123 124 125 126 127 128 129 130 131 132 154 155 156 157 162 163 164 165 166 167 168 169 170 171 172 185 186 187 188 192 193 194 195 196 197 228 243 % 5.24/5.37 %singleGoalClaCount:2 % 5.24/5.37 [66]P1(a1) % 5.24/5.37 [67]P1(a35) % 5.24/5.37 [68]P1(a36) % 5.24/5.37 [69]P2(a2) % 5.24/5.37 [70]P5(a2) % 5.24/5.37 [71]P9(a2) % 5.24/5.37 [72]P10(a1,a2,a35) % 5.24/5.37 [73]P10(a1,a2,a36) % 5.24/5.37 [74]P1(a3)+~P6(a5000) % 5.24/5.37 [75]P1(a17)+~P6(a5000) % 5.24/5.37 [76]P1(a19)+~P6(a5000) % 5.24/5.37 [77]P1(a21)+~P6(a5000) % 5.24/5.37 [87]E(a1,a35)+P11(a1,a2,a35) % 5.24/5.37 [88]E(a1,a36)+P11(a1,a2,a36) % 5.24/5.37 [89]P3(a3,a1,a2)+~P6(a5000) % 5.24/5.37 [90]P3(a17,a1,a2)+~P6(a5000) % 5.24/5.37 [91]P10(a35,a2,a21)+~P6(a5000) % 5.24/5.37 [92]P10(a36,a2,a21)+~P6(a5000) % 5.24/5.37 [93]P10(a3,a2,a35)+~P6(a5000) % 5.24/5.37 [94]P10(a3,a2,a19)+~P6(a5000) % 5.24/5.37 [95]P10(a17,a2,a36)+~P6(a5000) % 5.24/5.37 [96]P10(a17,a2,a19)+~P6(a5000) % 5.24/5.37 [97]P10(a19,a2,a21)+~P6(a5000) % 5.24/5.37 [98]P4(a21,a19,a2)+~P6(a5000) % 5.24/5.37 [122]~P3(x1221,a21,a2)+~P6(a5000) % 5.24/5.37 [99]E(a3,a35)+P11(a3,a2,a35)+~P6(a5000) % 5.24/5.37 [100]E(a17,a36)+P11(a17,a2,a36)+~P6(a5000) % 5.24/5.37 [101]E(a19,a3)+P11(a3,a2,a19)+~P6(a5000) % 5.24/5.37 [102]E(a19,a17)+P11(a17,a2,a19)+~P6(a5000) % 5.24/5.37 [103]E(a21,a35)+P11(a35,a2,a21)+~P6(a5000) % 5.24/5.37 [104]E(a21,a36)+P11(a36,a2,a21)+~P6(a5000) % 5.24/5.37 [105]E(a21,a19)+P11(a19,a2,a21)+~P6(a5000) % 5.24/5.37 [107]E(a1,a35)+P1(a6)+P3(a35,a1,a2) % 5.24/5.37 [108]E(a1,a36)+P1(a16)+P3(a36,a1,a2) % 5.24/5.37 [129]E(a1,a35)+P3(a35,a1,a2)+P3(a6,a1,a2) % 5.24/5.37 [130]P3(a35,a1,a2)+E(a1,a35)+P11(a6,a2,a35) % 5.24/5.37 [131]E(a1,a36)+P3(a36,a1,a2)+P3(a16,a1,a2) % 5.24/5.37 [132]P3(a36,a1,a2)+E(a1,a36)+P11(a16,a2,a36) % 5.24/5.37 [154]P6(a5000)+~P3(a35,a1,a2)+~P3(a36,a1,a2) % 5.24/5.37 [155]~P3(a35,a1,a2)+P6(a5000)+~P11(a1,a2,a36) % 5.24/5.37 [156]~P3(a36,a1,a2)+P6(a5000)+~P11(a1,a2,a35) % 5.24/5.37 [157]~P11(a1,a2,a35)+~P11(a1,a2,a36)+P6(a5000) % 5.24/5.37 [78]~P1(x781)+~E(a36,x781)+~E(a35,x781) % 5.24/5.37 [123]~P1(x1231)+~E(a35,x1231)+~P3(x1231,a36,a2) % 5.24/5.37 [124]~P1(x1241)+~E(a36,x1241)+~P3(x1241,a35,a2) % 5.24/5.37 [125]~P1(x1251)+~E(a35,x1251)+~P11(a36,a2,x1251) % 5.24/5.37 [126]~P1(x1261)+~E(a35,x1261)+~P10(a36,a2,x1261) % 5.24/5.37 [127]~P1(x1271)+~E(a36,x1271)+~P11(a35,a2,x1271) % 5.24/5.37 [128]~P1(x1281)+~E(a36,x1281)+~P10(a35,a2,x1281) % 5.24/5.37 [162]~P1(x1621)+~P3(x1621,a35,a2)+~P3(x1621,a36,a2) % 5.24/5.37 [163]~P1(x1631)+~P3(x1631,a35,a2)+~P11(a36,a2,x1631) % 5.24/5.37 [164]~P1(x1641)+~P3(x1641,a35,a2)+~P10(a36,a2,x1641) % 5.24/5.37 [165]~P1(x1651)+~P3(x1651,a36,a2)+~P11(a35,a2,x1651) % 5.24/5.37 [166]~P1(x1661)+~P3(x1661,a36,a2)+~P10(a35,a2,x1661) % 5.24/5.37 [167]~P1(x1671)+~P11(a35,a2,x1671)+~P11(a36,a2,x1671) % 5.24/5.37 [168]~P1(x1681)+~P11(a35,a2,x1681)+~P10(a36,a2,x1681) % 5.24/5.37 [169]~P1(x1691)+~P11(a36,a2,x1691)+~P10(a35,a2,x1691) % 5.24/5.37 [170]~P1(x1701)+~P10(a35,a2,x1701)+~P10(a36,a2,x1701) % 5.24/5.37 [79]~P2(x791)+P7(x791)+P1(f24(x791)) % 5.24/5.37 [80]~P2(x801)+P7(x801)+P1(f29(x801)) % 5.24/5.37 [81]~P2(x811)+P7(x811)+P1(f30(x811)) % 5.24/5.37 [82]~P2(x821)+P5(x821)+P1(f31(x821)) % 5.24/5.37 [83]~P2(x831)+P5(x831)+P1(f33(x831)) % 5.24/5.37 [84]~P2(x841)+P5(x841)+P1(f34(x841)) % 5.24/5.37 [85]~P2(x851)+P9(x851)+P1(f4(x851)) % 5.24/5.37 [86]~P2(x861)+P9(x861)+P1(f5(x861)) % 5.24/5.37 [106]~P2(x1061)+P9(x1061)+~P8(f5(x1061),f4(x1061)) % 5.24/5.37 [116]~P2(x1161)+P7(x1161)+P10(f24(x1161),x1161,f29(x1161)) % 5.24/5.37 [117]~P2(x1171)+P7(x1171)+P10(f24(x1171),x1171,f30(x1171)) % 5.24/5.37 [118]~P2(x1181)+P9(x1181)+P11(f4(x1181),x1181,f5(x1181)) % 5.24/5.37 [119]~P2(x1191)+P5(x1191)+P3(f33(x1191),f31(x1191),x1191) % 5.24/5.37 [120]~P2(x1201)+P5(x1201)+P3(f34(x1201),f31(x1201),x1201) % 5.24/5.37 [109]E(a3,a35)+P1(a18)+P3(a35,a3,a2)+~P6(a5000) % 5.24/5.37 [110]E(a17,a36)+P1(a20)+P3(a36,a17,a2)+~P6(a5000) % 5.24/5.37 [111]E(a19,a3)+P1(a22)+P3(a19,a3,a2)+~P6(a5000) % 5.24/5.37 [112]E(a19,a17)+P1(a23)+P3(a19,a17,a2)+~P6(a5000) % 5.24/5.37 [113]E(a21,a35)+P1(a25)+P3(a21,a35,a2)+~P6(a5000) % 5.24/5.37 [114]E(a21,a36)+P1(a28)+P3(a21,a36,a2)+~P6(a5000) % 5.24/5.37 [115]E(a21,a19)+P1(a26)+P3(a21,a19,a2)+~P6(a5000) % 5.24/5.37 [134]E(a3,a35)+P3(a35,a3,a2)+P3(a18,a3,a2)+~P6(a5000) % 5.24/5.37 [135]P3(a35,a3,a2)+E(a3,a35)+P11(a18,a2,a35)+~P6(a5000) % 5.24/5.37 [136]E(a17,a36)+P3(a36,a17,a2)+P3(a20,a17,a2)+~P6(a5000) % 5.24/5.37 [137]P3(a36,a17,a2)+E(a17,a36)+P11(a20,a2,a36)+~P6(a5000) % 5.24/5.37 [138]E(a19,a3)+P3(a19,a3,a2)+P3(a22,a3,a2)+~P6(a5000) % 5.24/5.37 [139]P3(a19,a3,a2)+E(a19,a3)+P11(a22,a2,a19)+~P6(a5000) % 5.24/5.37 [140]E(a19,a17)+P3(a19,a17,a2)+P3(a23,a17,a2)+~P6(a5000) % 5.24/5.37 [141]P3(a19,a17,a2)+E(a19,a17)+P11(a23,a2,a19)+~P6(a5000) % 5.24/5.37 [142]E(a21,a35)+P3(a21,a35,a2)+P3(a25,a35,a2)+~P6(a5000) % 5.24/5.37 [143]P3(a21,a35,a2)+E(a21,a35)+P11(a25,a2,a21)+~P6(a5000) % 5.24/5.37 [144]E(a21,a36)+P3(a21,a36,a2)+P3(a28,a36,a2)+~P6(a5000) % 5.24/5.37 [145]P3(a21,a36,a2)+E(a21,a36)+P11(a28,a2,a21)+~P6(a5000) % 5.24/5.37 [146]E(a21,a19)+P3(a21,a19,a2)+P3(a26,a19,a2)+~P6(a5000) % 5.24/5.37 [147]P3(a21,a19,a2)+E(a21,a19)+P11(a26,a2,a21)+~P6(a5000) % 5.24/5.37 [150]~P1(x1502)+~P1(x1501)+P8(x1501,x1502)+~P3(x1501,x1502,a2) % 5.24/5.37 [151]~P1(x1511)+~P1(x1512)+P8(x1511,x1512)+~P11(x1512,a2,x1511) % 5.24/5.37 [133]~P1(x1332)+~P2(x1331)+~P9(x1331)+P4(f7(x1331,x1332),x1332,x1331) % 5.24/5.37 [148]~P3(x1481,x1482,x1483)+P1(x1481)+~P1(x1482)+~P2(x1483) % 5.24/5.37 [149]~P4(x1491,x1492,x1493)+P1(x1491)+~P1(x1492)+~P2(x1493) % 5.24/5.37 [153]~P1(x1531)+~P2(x1532)+~P4(x1533,x1531,x1532)+P10(x1531,x1532,x1533) % 5.24/5.37 [173]~P4(x1734,x1731,x1732)+~P1(x1731)+~P3(x1733,x1734,x1732)+~P2(x1732) % 5.24/5.37 [185]~P1(x1851)+~P3(a36,a1,a2)+~P3(x1851,a1,a2)+~P11(x1851,a2,a35)+P6(a5000) % 5.24/5.37 [186]~P1(x1861)+~P11(a1,a2,a36)+~P3(x1861,a1,a2)+~P11(x1861,a2,a35)+P6(a5000) % 5.24/5.37 [187]~P1(x1871)+~P3(a35,a1,a2)+~P3(x1871,a1,a2)+~P11(x1871,a2,a36)+P6(a5000) % 5.24/5.37 [188]~P1(x1881)+~P11(a1,a2,a35)+~P3(x1881,a1,a2)+~P11(x1881,a2,a36)+P6(a5000) % 5.24/5.37 [171]~P1(x1711)+~P1(x1712)+~P11(x1712,a2,x1711)+~E(a35,x1711)+~P3(x1712,a36,a2) % 5.24/5.37 [172]~P1(x1721)+~P1(x1722)+~P11(x1722,a2,x1721)+~E(a36,x1721)+~P3(x1722,a35,a2) % 5.24/5.37 [192]~P1(x1921)+~P1(x1922)+~P11(x1921,a2,x1922)+~P3(x1921,a35,a2)+~P3(x1922,a36,a2) % 5.24/5.37 [193]~P1(x1931)+~P1(x1932)+~P11(x1932,a2,x1931)+~P3(x1931,a35,a2)+~P3(x1932,a36,a2) % 5.24/5.37 [194]~P1(x1941)+~P1(x1942)+~P11(x1941,a2,x1942)+~P3(x1941,a35,a2)+~P11(a36,a2,x1942) % 5.24/5.37 [195]~P1(x1951)+~P1(x1952)+~P11(x1951,a2,x1952)+~P3(x1951,a35,a2)+~P10(a36,a2,x1952) % 5.24/5.37 [196]~P1(x1961)+~P1(x1962)+~P11(x1962,a2,x1961)+~P3(x1962,a36,a2)+~P11(a35,a2,x1961) % 5.24/5.37 [197]~P1(x1971)+~P1(x1972)+~P11(x1972,a2,x1971)+~P3(x1972,a36,a2)+~P10(a35,a2,x1971) % 5.24/5.37 [177]~P2(x1771)+P7(x1771)+~P1(x1772)+~P10(f29(x1771),x1771,x1772)+~P10(f30(x1771),x1771,x1772) % 5.24/5.37 [178]~P2(x1781)+P5(x1781)+~P1(x1782)+~P10(f33(x1781),x1781,x1782)+~P10(f34(x1781),x1781,x1782) % 5.24/5.37 [121]~E(x1211,x1213)+~P1(x1213)+~P1(x1211)+~P2(x1212)+P10(x1211,x1212,x1213) % 5.24/5.37 [159]~P1(x1591)+~P1(x1593)+~P2(x1592)+~P3(x1593,x1591,x1592)+P11(x1591,x1592,x1593) % 5.24/5.37 [160]~P1(x1603)+~P1(x1601)+~P2(x1602)+~P11(x1601,x1602,x1603)+P10(x1601,x1602,x1603) % 5.24/5.37 [152]~P1(x1521)+~P1(x1522)+~P9(x1523)+~P11(x1522,x1523,x1521)+P8(x1521,x1522)+~P2(x1523) % 5.24/5.37 [161]~P1(x1612)+~P1(x1611)+~P2(x1613)+~P10(x1611,x1613,x1612)+E(x1611,x1612)+P11(x1611,x1613,x1612) % 5.24/5.37 [174]~P1(x1741)+~P1(x1742)+P8(x1741,x1742)+~P1(x1743)+~P3(x1743,x1742,a2)+~P11(x1743,a2,x1741) % 5.24/5.37 [200]~P1(x2001)+~P1(x2002)+~P2(x2003)+~P11(x2002,x2003,x2001)+P3(x2001,x2002,x2003)+P1(f13(x2002,x2003,x2001)) % 5.24/5.37 [213]~P1(x2133)+~P1(x2132)+~P1(x2131)+~P3(x2133,x2131,a2)+~P3(x2132,x2131,a2)+P1(f10(x2131,x2132,x2133)) % 5.24/5.37 [223]~P1(x2231)+~P1(x2232)+~P2(x2233)+~P11(x2232,x2233,x2231)+P3(x2231,x2232,x2233)+P3(f13(x2232,x2233,x2231),x2232,x2233) % 5.24/5.37 [224]~P1(x2241)+~P1(x2242)+~P2(x2243)+~P11(x2242,x2243,x2241)+P3(x2241,x2242,x2243)+P11(f13(x2242,x2243,x2241),x2243,x2241) % 5.24/5.37 [225]~P1(x2252)+~P1(x2251)+~P2(x2253)+~P10(x2252,x2253,x2251)+P4(x2251,x2252,x2253)+P3(f8(x2252,x2253,x2251),x2251,x2253) % 5.24/5.37 [241]~P1(x2413)+~P1(x2412)+~P1(x2411)+~P3(x2413,x2412,a2)+~P3(x2411,x2412,a2)+P10(x2411,a2,f10(x2412,x2413,x2411)) % 5.24/5.37 [242]~P1(x2423)+~P1(x2422)+~P1(x2421)+~P3(x2423,x2422,a2)+~P3(x2421,x2422,a2)+P10(x2421,a2,f10(x2422,x2421,x2423)) % 5.24/5.37 [228]~P1(x2281)+~P1(x2282)+~P3(x2281,a1,a2)+~P3(x2282,a1,a2)+~P11(x2281,a2,a35)+~P11(x2282,a2,a36)+P6(a5000) % 5.24/5.37 [243]~P1(x2431)+~P1(x2432)+~P1(x2433)+~P11(x2431,a2,x2432)+~P11(x2433,a2,x2432)+~P3(x2431,a35,a2)+~P3(x2433,a36,a2) % 5.24/5.37 [158]~E(x1581,x1583)+~E(x1581,x1582)+~P1(x1583)+~P1(x1582)+~P1(x1581)+~P8(x1581,a1)+P1(f9(x1581,x1582,x1583)) % 5.24/5.37 [175]~E(x1752,x1753)+~E(x1751,x1752)+~P1(x1753)+~P1(x1752)+~P1(x1751)+~P8(x1752,a1)+P10(x1751,a2,f9(x1752,x1753,x1751)) % 5.24/5.37 [176]~E(x1762,x1763)+~E(x1761,x1762)+~P1(x1763)+~P1(x1762)+~P1(x1761)+~P8(x1762,a1)+P10(x1761,a2,f9(x1762,x1761,x1763)) % 5.24/5.37 [179]~E(x1791,x1793)+~P1(x1793)+~P1(x1792)+~P1(x1791)+~P3(x1792,x1791,a2)+~P8(x1791,a1)+P1(f9(x1791,x1792,x1793)) % 5.24/5.37 [180]~E(x1801,x1802)+~P1(x1803)+~P1(x1802)+~P1(x1801)+~P3(x1803,x1801,a2)+~P8(x1801,a1)+P1(f9(x1801,x1802,x1803)) % 5.24/5.37 [181]~E(x1811,x1813)+~P1(x1813)+~P1(x1812)+~P1(x1811)+~P11(x1811,a2,x1812)+~P8(x1811,a1)+P1(f9(x1811,x1812,x1813)) % 5.24/5.37 [182]~E(x1821,x1823)+~P1(x1823)+~P1(x1822)+~P1(x1821)+~P10(x1821,a2,x1822)+~P8(x1821,a1)+P1(f9(x1821,x1822,x1823)) % 5.24/5.37 [183]~E(x1831,x1832)+~P1(x1833)+~P1(x1832)+~P1(x1831)+~P11(x1831,a2,x1833)+~P8(x1831,a1)+P1(f9(x1831,x1832,x1833)) % 5.24/5.37 [184]~E(x1841,x1842)+~P1(x1843)+~P1(x1842)+~P1(x1841)+~P10(x1841,a2,x1843)+~P8(x1841,a1)+P1(f9(x1841,x1842,x1843)) % 5.24/5.37 [201]~E(x2012,x2013)+~P1(x2013)+~P1(x2012)+~P1(x2011)+~P3(x2011,x2012,a2)+~P8(x2012,a1)+P10(x2011,a2,f9(x2012,x2013,x2011)) % 5.24/5.37 [202]~E(x2021,x2022)+~P1(x2023)+~P1(x2022)+~P1(x2021)+~P3(x2023,x2022,a2)+~P8(x2022,a1)+P10(x2021,a2,f9(x2022,x2023,x2021)) % 5.24/5.37 [203]~E(x2032,x2033)+~P1(x2033)+~P1(x2032)+~P1(x2031)+~P3(x2031,x2032,a2)+~P8(x2032,a1)+P10(x2031,a2,f9(x2032,x2031,x2033)) % 5.24/5.37 [204]~E(x2041,x2042)+~P1(x2043)+~P1(x2042)+~P1(x2041)+~P3(x2043,x2042,a2)+~P8(x2042,a1)+P10(x2041,a2,f9(x2042,x2041,x2043)) % 5.24/5.37 [205]~E(x2052,x2053)+~P1(x2053)+~P1(x2052)+~P1(x2051)+~P11(x2052,a2,x2051)+~P8(x2052,a1)+P10(x2051,a2,f9(x2052,x2053,x2051)) % 5.24/5.37 [206]~E(x2062,x2063)+~P1(x2063)+~P1(x2062)+~P1(x2061)+~P10(x2062,a2,x2061)+~P8(x2062,a1)+P10(x2061,a2,f9(x2062,x2063,x2061)) % 5.24/5.37 [207]~E(x2071,x2072)+~P1(x2073)+~P1(x2072)+~P1(x2071)+~P11(x2072,a2,x2073)+~P8(x2072,a1)+P10(x2071,a2,f9(x2072,x2073,x2071)) % 5.24/5.37 [208]~E(x2081,x2082)+~P1(x2083)+~P1(x2082)+~P1(x2081)+~P10(x2082,a2,x2083)+~P8(x2082,a1)+P10(x2081,a2,f9(x2082,x2083,x2081)) % 5.24/5.37 [209]~E(x2092,x2093)+~P1(x2093)+~P1(x2092)+~P1(x2091)+~P11(x2092,a2,x2091)+~P8(x2092,a1)+P10(x2091,a2,f9(x2092,x2091,x2093)) % 5.24/5.37 [210]~E(x2102,x2103)+~P1(x2103)+~P1(x2102)+~P1(x2101)+~P10(x2102,a2,x2101)+~P8(x2102,a1)+P10(x2101,a2,f9(x2102,x2101,x2103)) % 5.24/5.37 [211]~E(x2111,x2112)+~P1(x2113)+~P1(x2112)+~P1(x2111)+~P11(x2112,a2,x2113)+~P8(x2112,a1)+P10(x2111,a2,f9(x2112,x2111,x2113)) % 5.24/5.37 [212]~E(x2121,x2122)+~P1(x2123)+~P1(x2122)+~P1(x2121)+~P10(x2122,a2,x2123)+~P8(x2122,a1)+P10(x2121,a2,f9(x2122,x2121,x2123)) % 5.24/5.37 [214]~P1(x2143)+~P1(x2142)+~P1(x2141)+~P3(x2143,x2141,a2)+~P3(x2142,x2141,a2)+~P8(x2141,a1)+P1(f9(x2141,x2142,x2143)) % 5.24/5.37 [215]~P1(x2153)+~P1(x2152)+~P1(x2151)+~P3(x2153,x2151,a2)+~P11(x2151,a2,x2152)+~P8(x2151,a1)+P1(f9(x2151,x2152,x2153)) % 5.24/5.37 [216]~P1(x2163)+~P1(x2162)+~P1(x2161)+~P3(x2163,x2161,a2)+~P10(x2161,a2,x2162)+~P8(x2161,a1)+P1(f9(x2161,x2162,x2163)) % 5.24/5.37 [217]~P1(x2173)+~P1(x2172)+~P1(x2171)+~P3(x2172,x2171,a2)+~P11(x2171,a2,x2173)+~P8(x2171,a1)+P1(f9(x2171,x2172,x2173)) % 5.24/5.37 [218]~P1(x2183)+~P1(x2182)+~P1(x2181)+~P3(x2182,x2181,a2)+~P10(x2181,a2,x2183)+~P8(x2181,a1)+P1(f9(x2181,x2182,x2183)) % 5.24/5.37 [219]~P1(x2193)+~P1(x2192)+~P1(x2191)+~P11(x2191,a2,x2193)+~P11(x2191,a2,x2192)+~P8(x2191,a1)+P1(f9(x2191,x2192,x2193)) % 5.24/5.37 [220]~P1(x2203)+~P1(x2202)+~P1(x2201)+~P11(x2201,a2,x2203)+~P10(x2201,a2,x2202)+~P8(x2201,a1)+P1(f9(x2201,x2202,x2203)) % 5.24/5.37 [221]~P1(x2213)+~P1(x2212)+~P1(x2211)+~P11(x2211,a2,x2212)+~P10(x2211,a2,x2213)+~P8(x2211,a1)+P1(f9(x2211,x2212,x2213)) % 5.24/5.37 [222]~P1(x2223)+~P1(x2222)+~P1(x2221)+~P10(x2221,a2,x2223)+~P10(x2221,a2,x2222)+~P8(x2221,a1)+P1(f9(x2221,x2222,x2223)) % 5.24/5.37 [244]~P1(x2443)+~P1(x2442)+~P1(x2441)+~P3(x2443,x2442,a2)+~P3(x2441,x2442,a2)+~P8(x2442,a1)+P10(x2441,a2,f9(x2442,x2443,x2441)) % 5.24/5.37 [245]~P1(x2453)+~P1(x2452)+~P1(x2451)+~P3(x2453,x2452,a2)+~P3(x2451,x2452,a2)+~P8(x2452,a1)+P10(x2451,a2,f9(x2452,x2451,x2453)) % 5.24/5.37 [246]~P1(x2463)+~P1(x2462)+~P1(x2461)+~P3(x2463,x2462,a2)+~P11(x2462,a2,x2461)+~P8(x2462,a1)+P10(x2461,a2,f9(x2462,x2463,x2461)) % 5.24/5.37 [247]~P1(x2473)+~P1(x2472)+~P1(x2471)+~P3(x2473,x2472,a2)+~P10(x2472,a2,x2471)+~P8(x2472,a1)+P10(x2471,a2,f9(x2472,x2473,x2471)) % 5.24/5.37 [248]~P1(x2483)+~P1(x2482)+~P1(x2481)+~P3(x2481,x2482,a2)+~P11(x2482,a2,x2483)+~P8(x2482,a1)+P10(x2481,a2,f9(x2482,x2483,x2481)) % 5.24/5.37 [249]~P1(x2493)+~P1(x2492)+~P1(x2491)+~P3(x2491,x2492,a2)+~P10(x2492,a2,x2493)+~P8(x2492,a1)+P10(x2491,a2,f9(x2492,x2493,x2491)) % 5.24/5.37 [250]~P1(x2503)+~P1(x2502)+~P1(x2501)+~P3(x2503,x2502,a2)+~P11(x2502,a2,x2501)+~P8(x2502,a1)+P10(x2501,a2,f9(x2502,x2501,x2503)) % 5.24/5.37 [251]~P1(x2513)+~P1(x2512)+~P1(x2511)+~P3(x2513,x2512,a2)+~P10(x2512,a2,x2511)+~P8(x2512,a1)+P10(x2511,a2,f9(x2512,x2511,x2513)) % 5.24/5.37 [252]~P1(x2523)+~P1(x2522)+~P1(x2521)+~P3(x2521,x2522,a2)+~P11(x2522,a2,x2523)+~P8(x2522,a1)+P10(x2521,a2,f9(x2522,x2521,x2523)) % 5.24/5.37 [253]~P1(x2533)+~P1(x2532)+~P1(x2531)+~P3(x2531,x2532,a2)+~P10(x2532,a2,x2533)+~P8(x2532,a1)+P10(x2531,a2,f9(x2532,x2531,x2533)) % 5.24/5.37 [254]~P1(x2543)+~P1(x2542)+~P1(x2541)+~P11(x2542,a2,x2543)+~P11(x2542,a2,x2541)+~P8(x2542,a1)+P10(x2541,a2,f9(x2542,x2543,x2541)) % 5.24/5.37 [255]~P1(x2553)+~P1(x2552)+~P1(x2551)+~P11(x2552,a2,x2553)+~P10(x2552,a2,x2551)+~P8(x2552,a1)+P10(x2551,a2,f9(x2552,x2553,x2551)) % 5.24/5.37 [256]~P1(x2563)+~P1(x2562)+~P1(x2561)+~P11(x2562,a2,x2561)+~P10(x2562,a2,x2563)+~P8(x2562,a1)+P10(x2561,a2,f9(x2562,x2563,x2561)) % 5.24/5.37 [257]~P1(x2573)+~P1(x2572)+~P1(x2571)+~P10(x2572,a2,x2573)+~P10(x2572,a2,x2571)+~P8(x2572,a1)+P10(x2571,a2,f9(x2572,x2573,x2571)) % 5.24/5.37 [258]~P1(x2583)+~P1(x2582)+~P1(x2581)+~P11(x2582,a2,x2583)+~P11(x2582,a2,x2581)+~P8(x2582,a1)+P10(x2581,a2,f9(x2582,x2581,x2583)) % 5.24/5.37 [259]~P1(x2593)+~P1(x2592)+~P1(x2591)+~P11(x2592,a2,x2593)+~P10(x2592,a2,x2591)+~P8(x2592,a1)+P10(x2591,a2,f9(x2592,x2591,x2593)) % 5.24/5.37 [260]~P1(x2603)+~P1(x2602)+~P1(x2601)+~P11(x2602,a2,x2601)+~P10(x2602,a2,x2603)+~P8(x2602,a1)+P10(x2601,a2,f9(x2602,x2601,x2603)) % 5.24/5.37 [261]~P1(x2613)+~P1(x2612)+~P1(x2611)+~P10(x2612,a2,x2613)+~P10(x2612,a2,x2611)+~P8(x2612,a1)+P10(x2611,a2,f9(x2612,x2611,x2613)) % 5.24/5.37 [268]~P1(x2682)+~P1(x2681)+~P1(x2683)+~P3(x2682,x2681,a2)+~P3(x2683,x2681,a2)+E(f10(x2681,x2682,x2683),x2683)+P11(x2683,a2,f10(x2681,x2682,x2683)) % 5.24/5.37 [269]~P1(x2693)+~P1(x2691)+~P1(x2692)+~P3(x2693,x2691,a2)+~P3(x2692,x2691,a2)+E(f10(x2691,x2692,x2693),x2692)+P11(x2692,a2,f10(x2691,x2692,x2693)) % 5.24/5.37 [189]~P1(x1893)+~P1(x1891)+~P2(x1892)+~P3(x1894,x1891,x1892)+~P11(x1894,x1892,x1893)+P11(x1891,x1892,x1893)+~P1(x1894) % 5.24/5.37 [190]~P1(x1903)+~P1(x1901)+~P2(x1902)+~P11(x1904,x1902,x1903)+~P11(x1901,x1902,x1904)+P11(x1901,x1902,x1903)+~P1(x1904) % 5.24/5.37 [191]~P1(x1913)+~P1(x1911)+~P2(x1912)+~P10(x1914,x1912,x1913)+~P10(x1911,x1912,x1914)+P10(x1911,x1912,x1913)+~P1(x1914) % 5.24/5.37 [198]~E(x1981,x1982)+~E(x1983,x1981)+~P1(x1982)+~P1(x1981)+~P1(x1983)+~P8(x1981,a1)+E(f9(x1981,x1982,x1983),x1983)+P11(x1983,a2,f9(x1981,x1982,x1983)) % 5.24/5.37 [199]~E(x1991,x1993)+~E(x1992,x1991)+~P1(x1993)+~P1(x1991)+~P1(x1992)+~P8(x1991,a1)+E(f9(x1991,x1992,x1993),x1992)+P11(x1992,a2,f9(x1991,x1992,x1993)) % 5.24/5.37 [229]~E(x2291,x2292)+~P1(x2292)+~P1(x2291)+~P1(x2293)+~P3(x2293,x2291,a2)+~P8(x2291,a1)+E(f9(x2291,x2292,x2293),x2293)+P11(x2293,a2,f9(x2291,x2292,x2293)) % 5.24/5.37 [230]~E(x2303,x2301)+~P1(x2302)+~P1(x2301)+~P1(x2303)+~P3(x2302,x2301,a2)+~P8(x2301,a1)+E(f9(x2301,x2302,x2303),x2303)+P11(x2303,a2,f9(x2301,x2302,x2303)) % 5.24/5.37 [231]~E(x2311,x2313)+~P1(x2313)+~P1(x2311)+~P1(x2312)+~P3(x2312,x2311,a2)+~P8(x2311,a1)+E(f9(x2311,x2312,x2313),x2312)+P11(x2312,a2,f9(x2311,x2312,x2313)) % 5.24/5.37 [232]~E(x2322,x2321)+~P1(x2323)+~P1(x2321)+~P1(x2322)+~P3(x2323,x2321,a2)+~P8(x2321,a1)+E(f9(x2321,x2322,x2323),x2322)+P11(x2322,a2,f9(x2321,x2322,x2323)) % 5.24/5.37 [233]~E(x2331,x2332)+~P1(x2332)+~P1(x2331)+~P1(x2333)+~P11(x2331,a2,x2333)+~P8(x2331,a1)+E(f9(x2331,x2332,x2333),x2333)+P11(x2333,a2,f9(x2331,x2332,x2333)) % 5.24/5.37 [234]~E(x2341,x2342)+~P1(x2342)+~P1(x2341)+~P1(x2343)+~P10(x2341,a2,x2343)+~P8(x2341,a1)+E(f9(x2341,x2342,x2343),x2343)+P11(x2343,a2,f9(x2341,x2342,x2343)) % 5.24/5.37 [235]~E(x2353,x2351)+~P1(x2352)+~P1(x2351)+~P1(x2353)+~P11(x2351,a2,x2352)+~P8(x2351,a1)+E(f9(x2351,x2352,x2353),x2353)+P11(x2353,a2,f9(x2351,x2352,x2353)) % 5.24/5.37 [236]~E(x2363,x2361)+~P1(x2362)+~P1(x2361)+~P1(x2363)+~P10(x2361,a2,x2362)+~P8(x2361,a1)+E(f9(x2361,x2362,x2363),x2363)+P11(x2363,a2,f9(x2361,x2362,x2363)) % 5.24/5.37 [237]~E(x2371,x2373)+~P1(x2373)+~P1(x2371)+~P1(x2372)+~P11(x2371,a2,x2372)+~P8(x2371,a1)+E(f9(x2371,x2372,x2373),x2372)+P11(x2372,a2,f9(x2371,x2372,x2373)) % 5.24/5.37 [238]~E(x2381,x2383)+~P1(x2383)+~P1(x2381)+~P1(x2382)+~P10(x2381,a2,x2382)+~P8(x2381,a1)+E(f9(x2381,x2382,x2383),x2382)+P11(x2382,a2,f9(x2381,x2382,x2383)) % 5.24/5.37 [239]~E(x2392,x2391)+~P1(x2393)+~P1(x2391)+~P1(x2392)+~P11(x2391,a2,x2393)+~P8(x2391,a1)+E(f9(x2391,x2392,x2393),x2392)+P11(x2392,a2,f9(x2391,x2392,x2393)) % 5.24/5.37 [240]~E(x2402,x2401)+~P1(x2403)+~P1(x2401)+~P1(x2402)+~P10(x2401,a2,x2403)+~P8(x2401,a1)+E(f9(x2401,x2402,x2403),x2402)+P11(x2402,a2,f9(x2401,x2402,x2403)) % 5.24/5.37 [278]~P1(x2782)+~P1(x2781)+~P1(x2783)+~P3(x2782,x2781,a2)+~P3(x2783,x2781,a2)+~P8(x2781,a1)+E(f9(x2781,x2782,x2783),x2783)+P11(x2783,a2,f9(x2781,x2782,x2783)) % 5.24/5.37 [279]~P1(x2793)+~P1(x2791)+~P1(x2792)+~P3(x2793,x2791,a2)+~P3(x2792,x2791,a2)+~P8(x2791,a1)+E(f9(x2791,x2792,x2793),x2792)+P11(x2792,a2,f9(x2791,x2792,x2793)) % 5.24/5.37 [280]~P1(x2802)+~P1(x2801)+~P1(x2803)+~P3(x2802,x2801,a2)+~P11(x2801,a2,x2803)+~P8(x2801,a1)+E(f9(x2801,x2802,x2803),x2803)+P11(x2803,a2,f9(x2801,x2802,x2803)) % 5.24/5.37 [281]~P1(x2812)+~P1(x2811)+~P1(x2813)+~P3(x2812,x2811,a2)+~P10(x2811,a2,x2813)+~P8(x2811,a1)+E(f9(x2811,x2812,x2813),x2813)+P11(x2813,a2,f9(x2811,x2812,x2813)) % 5.24/5.37 [282]~P1(x2822)+~P1(x2821)+~P1(x2823)+~P3(x2823,x2821,a2)+~P11(x2821,a2,x2822)+~P8(x2821,a1)+E(f9(x2821,x2822,x2823),x2823)+P11(x2823,a2,f9(x2821,x2822,x2823)) % 5.24/5.37 [283]~P1(x2832)+~P1(x2831)+~P1(x2833)+~P3(x2833,x2831,a2)+~P10(x2831,a2,x2832)+~P8(x2831,a1)+E(f9(x2831,x2832,x2833),x2833)+P11(x2833,a2,f9(x2831,x2832,x2833)) % 5.24/5.37 [284]~P1(x2843)+~P1(x2841)+~P1(x2842)+~P3(x2843,x2841,a2)+~P11(x2841,a2,x2842)+~P8(x2841,a1)+E(f9(x2841,x2842,x2843),x2842)+P11(x2842,a2,f9(x2841,x2842,x2843)) % 5.24/5.37 [285]~P1(x2853)+~P1(x2851)+~P1(x2852)+~P3(x2853,x2851,a2)+~P10(x2851,a2,x2852)+~P8(x2851,a1)+E(f9(x2851,x2852,x2853),x2852)+P11(x2852,a2,f9(x2851,x2852,x2853)) % 5.24/5.37 [286]~P1(x2863)+~P1(x2861)+~P1(x2862)+~P3(x2862,x2861,a2)+~P11(x2861,a2,x2863)+~P8(x2861,a1)+E(f9(x2861,x2862,x2863),x2862)+P11(x2862,a2,f9(x2861,x2862,x2863)) % 5.24/5.37 [287]~P1(x2873)+~P1(x2871)+~P1(x2872)+~P3(x2872,x2871,a2)+~P10(x2871,a2,x2873)+~P8(x2871,a1)+E(f9(x2871,x2872,x2873),x2872)+P11(x2872,a2,f9(x2871,x2872,x2873)) % 5.24/5.37 [288]~P1(x2882)+~P1(x2881)+~P1(x2883)+~P11(x2881,a2,x2882)+~P11(x2881,a2,x2883)+~P8(x2881,a1)+E(f9(x2881,x2882,x2883),x2883)+P11(x2883,a2,f9(x2881,x2882,x2883)) % 5.24/5.37 [289]~P1(x2892)+~P1(x2891)+~P1(x2893)+~P11(x2891,a2,x2892)+~P10(x2891,a2,x2893)+~P8(x2891,a1)+E(f9(x2891,x2892,x2893),x2893)+P11(x2893,a2,f9(x2891,x2892,x2893)) % 5.24/5.37 [290]~P1(x2902)+~P1(x2901)+~P1(x2903)+~P11(x2901,a2,x2903)+~P10(x2901,a2,x2902)+~P8(x2901,a1)+E(f9(x2901,x2902,x2903),x2903)+P11(x2903,a2,f9(x2901,x2902,x2903)) % 5.24/5.37 [291]~P1(x2912)+~P1(x2911)+~P1(x2913)+~P10(x2911,a2,x2912)+~P10(x2911,a2,x2913)+~P8(x2911,a1)+E(f9(x2911,x2912,x2913),x2913)+P11(x2913,a2,f9(x2911,x2912,x2913)) % 5.24/5.37 [292]~P1(x2923)+~P1(x2921)+~P1(x2922)+~P11(x2921,a2,x2923)+~P11(x2921,a2,x2922)+~P8(x2921,a1)+E(f9(x2921,x2922,x2923),x2922)+P11(x2922,a2,f9(x2921,x2922,x2923)) % 5.24/5.37 [293]~P1(x2933)+~P1(x2931)+~P1(x2932)+~P11(x2931,a2,x2933)+~P10(x2931,a2,x2932)+~P8(x2931,a1)+E(f9(x2931,x2932,x2933),x2932)+P11(x2932,a2,f9(x2931,x2932,x2933)) % 5.24/5.37 [294]~P1(x2943)+~P1(x2941)+~P1(x2942)+~P11(x2941,a2,x2942)+~P10(x2941,a2,x2943)+~P8(x2941,a1)+E(f9(x2941,x2942,x2943),x2942)+P11(x2942,a2,f9(x2941,x2942,x2943)) % 5.24/5.37 [295]~P1(x2953)+~P1(x2951)+~P1(x2952)+~P10(x2951,a2,x2953)+~P10(x2951,a2,x2952)+~P8(x2951,a1)+E(f9(x2951,x2952,x2953),x2952)+P11(x2952,a2,f9(x2951,x2952,x2953)) % 5.24/5.37 [337]~P1(x3373)+~P1(x3372)+~P1(x3371)+~P3(x3373,x3371,a2)+~P3(x3372,x3371,a2)+E(f10(x3371,x3372,x3373),x3373)+P3(f10(x3371,x3372,x3373),x3373,a2)+P1(f11(x3371,x3372,x3373)) % 5.24/5.37 [338]~P1(x3383)+~P1(x3382)+~P1(x3381)+~P3(x3383,x3381,a2)+~P3(x3382,x3381,a2)+E(f10(x3381,x3382,x3383),x3382)+P3(f10(x3381,x3382,x3383),x3382,a2)+P1(f12(x3381,x3382,x3383)) % 5.24/5.37 [377]~P1(x3773)+~P1(x3772)+~P1(x3771)+~P3(x3773,x3771,a2)+~P3(x3772,x3771,a2)+E(f10(x3771,x3772,x3773),x3773)+P3(f11(x3771,x3772,x3773),x3773,a2)+P3(f10(x3771,x3772,x3773),x3773,a2) % 5.24/5.37 [378]~P1(x3783)+~P1(x3782)+~P1(x3781)+~P3(x3783,x3781,a2)+~P3(x3782,x3781,a2)+E(f10(x3781,x3782,x3783),x3782)+P3(f12(x3781,x3782,x3783),x3782,a2)+P3(f10(x3781,x3782,x3783),x3782,a2) % 5.24/5.37 [427]~P1(x4273)+~P1(x4272)+~P1(x4271)+~P3(x4273,x4271,a2)+~P3(x4272,x4271,a2)+E(f10(x4271,x4272,x4273),x4273)+P11(f11(x4271,x4272,x4273),a2,f10(x4271,x4272,x4273))+P3(f10(x4271,x4272,x4273),x4273,a2) % 5.24/5.37 [428]~P1(x4283)+~P1(x4282)+~P1(x4281)+~P3(x4283,x4281,a2)+~P3(x4282,x4281,a2)+E(f10(x4281,x4282,x4283),x4282)+P11(f12(x4281,x4282,x4283),a2,f10(x4281,x4282,x4283))+P3(f10(x4281,x4282,x4283),x4282,a2) % 5.24/5.37 [463]~P1(x4634)+~P1(x4633)+~P1(x4632)+~P2(x4631)+~P7(x4631)+~P10(x4632,x4631,x4634)+~P10(x4632,x4631,x4633)+P1(f27(x4631,x4632,x4633,x4634)) % 5.24/5.37 [464]~P1(x4644)+~P1(x4643)+~P1(x4642)+~P2(x4641)+~P5(x4641)+~P3(x4644,x4642,x4641)+~P3(x4643,x4642,x4641)+P1(f32(x4641,x4642,x4643,x4644)) % 5.24/5.37 [467]~P1(x4674)+~P1(x4673)+~P1(x4671)+~P2(x4672)+~P7(x4672)+~P10(x4673,x4672,x4674)+~P10(x4673,x4672,x4671)+P10(x4671,x4672,f27(x4672,x4673,x4674,x4671)) % 5.24/5.37 [468]~P1(x4684)+~P1(x4683)+~P1(x4681)+~P2(x4682)+~P7(x4682)+~P10(x4683,x4682,x4684)+~P10(x4683,x4682,x4681)+P10(x4681,x4682,f27(x4682,x4683,x4681,x4684)) % 5.24/5.37 [469]~P1(x4694)+~P1(x4693)+~P1(x4691)+~P2(x4692)+~P5(x4692)+~P3(x4694,x4693,x4692)+~P3(x4691,x4693,x4692)+P10(x4691,x4692,f32(x4692,x4693,x4694,x4691)) % 5.24/5.37 [470]~P1(x4704)+~P1(x4703)+~P1(x4701)+~P2(x4702)+~P5(x4702)+~P3(x4704,x4703,x4702)+~P3(x4701,x4703,x4702)+P10(x4701,x4702,f32(x4702,x4703,x4701,x4704)) % 5.24/5.37 [262]~E(x2621,x2623)+~E(x2621,x2622)+~P1(x2623)+~P1(x2622)+~P1(x2621)+~P8(x2621,a1)+E(f9(x2621,x2622,x2623),x2623)+P3(f9(x2621,x2622,x2623),x2623,a2)+P1(f14(x2621,x2622,x2623)) % 5.24/5.37 [263]~E(x2631,x2633)+~E(x2631,x2632)+~P1(x2633)+~P1(x2632)+~P1(x2631)+~P8(x2631,a1)+E(f9(x2631,x2632,x2633),x2632)+P3(f9(x2631,x2632,x2633),x2632,a2)+P1(f15(x2631,x2632,x2633)) % 5.24/5.37 [276]~E(x2761,x2763)+~E(x2761,x2762)+~P1(x2763)+~P1(x2762)+~P1(x2761)+~P8(x2761,a1)+E(f9(x2761,x2762,x2763),x2763)+P3(f14(x2761,x2762,x2763),x2763,a2)+P3(f9(x2761,x2762,x2763),x2763,a2) % 5.24/5.37 [277]~E(x2771,x2773)+~E(x2771,x2772)+~P1(x2773)+~P1(x2772)+~P1(x2771)+~P8(x2771,a1)+E(f9(x2771,x2772,x2773),x2772)+P3(f15(x2771,x2772,x2773),x2772,a2)+P3(f9(x2771,x2772,x2773),x2772,a2) % 5.24/5.37 [300]~E(x3001,x3003)+~P1(x3003)+~P1(x3002)+~P1(x3001)+~P3(x3002,x3001,a2)+~P8(x3001,a1)+E(f9(x3001,x3002,x3003),x3003)+P3(f9(x3001,x3002,x3003),x3003,a2)+P1(f14(x3001,x3002,x3003)) % 5.24/5.37 [301]~E(x3011,x3012)+~P1(x3013)+~P1(x3012)+~P1(x3011)+~P3(x3013,x3011,a2)+~P8(x3011,a1)+E(f9(x3011,x3012,x3013),x3013)+P3(f9(x3011,x3012,x3013),x3013,a2)+P1(f14(x3011,x3012,x3013)) % 5.24/5.37 [302]~E(x3021,x3023)+~P1(x3023)+~P1(x3022)+~P1(x3021)+~P3(x3022,x3021,a2)+~P8(x3021,a1)+E(f9(x3021,x3022,x3023),x3022)+P3(f9(x3021,x3022,x3023),x3022,a2)+P1(f15(x3021,x3022,x3023)) % 5.24/5.37 [303]~E(x3031,x3032)+~P1(x3033)+~P1(x3032)+~P1(x3031)+~P3(x3033,x3031,a2)+~P8(x3031,a1)+E(f9(x3031,x3032,x3033),x3032)+P3(f9(x3031,x3032,x3033),x3032,a2)+P1(f15(x3031,x3032,x3033)) % 5.24/5.37 [304]~E(x3041,x3043)+~P1(x3043)+~P1(x3042)+~P1(x3041)+~P11(x3041,a2,x3042)+~P8(x3041,a1)+E(f9(x3041,x3042,x3043),x3043)+P3(f9(x3041,x3042,x3043),x3043,a2)+P1(f14(x3041,x3042,x3043)) % 5.24/5.37 [305]~E(x3051,x3053)+~P1(x3053)+~P1(x3052)+~P1(x3051)+~P10(x3051,a2,x3052)+~P8(x3051,a1)+E(f9(x3051,x3052,x3053),x3053)+P3(f9(x3051,x3052,x3053),x3053,a2)+P1(f14(x3051,x3052,x3053)) % 5.24/5.37 [306]~E(x3061,x3062)+~P1(x3063)+~P1(x3062)+~P1(x3061)+~P11(x3061,a2,x3063)+~P8(x3061,a1)+E(f9(x3061,x3062,x3063),x3063)+P3(f9(x3061,x3062,x3063),x3063,a2)+P1(f14(x3061,x3062,x3063)) % 5.24/5.37 [307]~E(x3071,x3072)+~P1(x3073)+~P1(x3072)+~P1(x3071)+~P10(x3071,a2,x3073)+~P8(x3071,a1)+E(f9(x3071,x3072,x3073),x3073)+P3(f9(x3071,x3072,x3073),x3073,a2)+P1(f14(x3071,x3072,x3073)) % 5.24/5.37 [308]~E(x3081,x3083)+~P1(x3083)+~P1(x3082)+~P1(x3081)+~P11(x3081,a2,x3082)+~P8(x3081,a1)+E(f9(x3081,x3082,x3083),x3082)+P3(f9(x3081,x3082,x3083),x3082,a2)+P1(f15(x3081,x3082,x3083)) % 5.24/5.37 [309]~E(x3091,x3093)+~P1(x3093)+~P1(x3092)+~P1(x3091)+~P10(x3091,a2,x3092)+~P8(x3091,a1)+E(f9(x3091,x3092,x3093),x3092)+P3(f9(x3091,x3092,x3093),x3092,a2)+P1(f15(x3091,x3092,x3093)) % 5.24/5.37 [310]~E(x3101,x3102)+~P1(x3103)+~P1(x3102)+~P1(x3101)+~P11(x3101,a2,x3103)+~P8(x3101,a1)+E(f9(x3101,x3102,x3103),x3102)+P3(f9(x3101,x3102,x3103),x3102,a2)+P1(f15(x3101,x3102,x3103)) % 5.24/5.37 [311]~E(x3111,x3112)+~P1(x3113)+~P1(x3112)+~P1(x3111)+~P10(x3111,a2,x3113)+~P8(x3111,a1)+E(f9(x3111,x3112,x3113),x3112)+P3(f9(x3111,x3112,x3113),x3112,a2)+P1(f15(x3111,x3112,x3113)) % 5.24/5.37 [325]~E(x3251,x3253)+~P1(x3253)+~P1(x3252)+~P1(x3251)+~P3(x3252,x3251,a2)+~P8(x3251,a1)+E(f9(x3251,x3252,x3253),x3253)+P3(f14(x3251,x3252,x3253),x3253,a2)+P3(f9(x3251,x3252,x3253),x3253,a2) % 5.24/5.37 [326]~E(x3261,x3262)+~P1(x3263)+~P1(x3262)+~P1(x3261)+~P3(x3263,x3261,a2)+~P8(x3261,a1)+E(f9(x3261,x3262,x3263),x3263)+P3(f14(x3261,x3262,x3263),x3263,a2)+P3(f9(x3261,x3262,x3263),x3263,a2) % 5.24/5.37 [327]~E(x3271,x3273)+~P1(x3273)+~P1(x3272)+~P1(x3271)+~P3(x3272,x3271,a2)+~P8(x3271,a1)+E(f9(x3271,x3272,x3273),x3272)+P3(f15(x3271,x3272,x3273),x3272,a2)+P3(f9(x3271,x3272,x3273),x3272,a2) % 5.24/5.37 [328]~E(x3281,x3282)+~P1(x3283)+~P1(x3282)+~P1(x3281)+~P3(x3283,x3281,a2)+~P8(x3281,a1)+E(f9(x3281,x3282,x3283),x3282)+P3(f15(x3281,x3282,x3283),x3282,a2)+P3(f9(x3281,x3282,x3283),x3282,a2) % 5.24/5.37 [329]~E(x3291,x3293)+~P1(x3293)+~P1(x3292)+~P1(x3291)+~P11(x3291,a2,x3292)+~P8(x3291,a1)+E(f9(x3291,x3292,x3293),x3293)+P3(f14(x3291,x3292,x3293),x3293,a2)+P3(f9(x3291,x3292,x3293),x3293,a2) % 5.24/5.37 [330]~E(x3301,x3303)+~P1(x3303)+~P1(x3302)+~P1(x3301)+~P10(x3301,a2,x3302)+~P8(x3301,a1)+E(f9(x3301,x3302,x3303),x3303)+P3(f14(x3301,x3302,x3303),x3303,a2)+P3(f9(x3301,x3302,x3303),x3303,a2) % 5.24/5.37 [331]~E(x3311,x3312)+~P1(x3313)+~P1(x3312)+~P1(x3311)+~P11(x3311,a2,x3313)+~P8(x3311,a1)+E(f9(x3311,x3312,x3313),x3313)+P3(f14(x3311,x3312,x3313),x3313,a2)+P3(f9(x3311,x3312,x3313),x3313,a2) % 5.24/5.37 [332]~E(x3321,x3322)+~P1(x3323)+~P1(x3322)+~P1(x3321)+~P10(x3321,a2,x3323)+~P8(x3321,a1)+E(f9(x3321,x3322,x3323),x3323)+P3(f14(x3321,x3322,x3323),x3323,a2)+P3(f9(x3321,x3322,x3323),x3323,a2) % 5.24/5.37 [333]~E(x3331,x3333)+~P1(x3333)+~P1(x3332)+~P1(x3331)+~P11(x3331,a2,x3332)+~P8(x3331,a1)+E(f9(x3331,x3332,x3333),x3332)+P3(f15(x3331,x3332,x3333),x3332,a2)+P3(f9(x3331,x3332,x3333),x3332,a2) % 5.24/5.37 [334]~E(x3341,x3343)+~P1(x3343)+~P1(x3342)+~P1(x3341)+~P10(x3341,a2,x3342)+~P8(x3341,a1)+E(f9(x3341,x3342,x3343),x3342)+P3(f15(x3341,x3342,x3343),x3342,a2)+P3(f9(x3341,x3342,x3343),x3342,a2) % 5.24/5.37 [335]~E(x3351,x3352)+~P1(x3353)+~P1(x3352)+~P1(x3351)+~P11(x3351,a2,x3353)+~P8(x3351,a1)+E(f9(x3351,x3352,x3353),x3352)+P3(f15(x3351,x3352,x3353),x3352,a2)+P3(f9(x3351,x3352,x3353),x3352,a2) % 5.24/5.37 [336]~E(x3361,x3362)+~P1(x3363)+~P1(x3362)+~P1(x3361)+~P10(x3361,a2,x3363)+~P8(x3361,a1)+E(f9(x3361,x3362,x3363),x3362)+P3(f15(x3361,x3362,x3363),x3362,a2)+P3(f9(x3361,x3362,x3363),x3362,a2) % 5.24/5.37 [351]~E(x3511,x3513)+~E(x3511,x3512)+~P1(x3513)+~P1(x3512)+~P1(x3511)+~P8(x3511,a1)+E(f9(x3511,x3512,x3513),x3513)+P11(f14(x3511,x3512,x3513),a2,f9(x3511,x3512,x3513))+P3(f9(x3511,x3512,x3513),x3513,a2) % 5.24/5.37 [352]~E(x3521,x3523)+~E(x3521,x3522)+~P1(x3523)+~P1(x3522)+~P1(x3521)+~P8(x3521,a1)+E(f9(x3521,x3522,x3523),x3522)+P11(f15(x3521,x3522,x3523),a2,f9(x3521,x3522,x3523))+P3(f9(x3521,x3522,x3523),x3522,a2) % 5.24/5.37 [353]~P1(x3533)+~P1(x3532)+~P1(x3531)+~P3(x3533,x3531,a2)+~P3(x3532,x3531,a2)+~P8(x3531,a1)+E(f9(x3531,x3532,x3533),x3533)+P3(f9(x3531,x3532,x3533),x3533,a2)+P1(f14(x3531,x3532,x3533)) % 5.24/5.37 [354]~P1(x3543)+~P1(x3542)+~P1(x3541)+~P3(x3543,x3541,a2)+~P3(x3542,x3541,a2)+~P8(x3541,a1)+E(f9(x3541,x3542,x3543),x3542)+P3(f9(x3541,x3542,x3543),x3542,a2)+P1(f15(x3541,x3542,x3543)) % 5.24/5.37 [355]~P1(x3553)+~P1(x3552)+~P1(x3551)+~P3(x3553,x3551,a2)+~P11(x3551,a2,x3552)+~P8(x3551,a1)+E(f9(x3551,x3552,x3553),x3553)+P3(f9(x3551,x3552,x3553),x3553,a2)+P1(f14(x3551,x3552,x3553)) % 5.24/5.37 [356]~P1(x3563)+~P1(x3562)+~P1(x3561)+~P3(x3563,x3561,a2)+~P10(x3561,a2,x3562)+~P8(x3561,a1)+E(f9(x3561,x3562,x3563),x3563)+P3(f9(x3561,x3562,x3563),x3563,a2)+P1(f14(x3561,x3562,x3563)) % 5.24/5.37 [357]~P1(x3573)+~P1(x3572)+~P1(x3571)+~P3(x3572,x3571,a2)+~P11(x3571,a2,x3573)+~P8(x3571,a1)+E(f9(x3571,x3572,x3573),x3573)+P3(f9(x3571,x3572,x3573),x3573,a2)+P1(f14(x3571,x3572,x3573)) % 5.24/5.37 [358]~P1(x3583)+~P1(x3582)+~P1(x3581)+~P3(x3582,x3581,a2)+~P10(x3581,a2,x3583)+~P8(x3581,a1)+E(f9(x3581,x3582,x3583),x3583)+P3(f9(x3581,x3582,x3583),x3583,a2)+P1(f14(x3581,x3582,x3583)) % 5.24/5.37 [359]~P1(x3593)+~P1(x3592)+~P1(x3591)+~P3(x3593,x3591,a2)+~P11(x3591,a2,x3592)+~P8(x3591,a1)+E(f9(x3591,x3592,x3593),x3592)+P3(f9(x3591,x3592,x3593),x3592,a2)+P1(f15(x3591,x3592,x3593)) % 5.24/5.37 [360]~P1(x3603)+~P1(x3602)+~P1(x3601)+~P3(x3603,x3601,a2)+~P10(x3601,a2,x3602)+~P8(x3601,a1)+E(f9(x3601,x3602,x3603),x3602)+P3(f9(x3601,x3602,x3603),x3602,a2)+P1(f15(x3601,x3602,x3603)) % 5.24/5.37 [361]~P1(x3613)+~P1(x3612)+~P1(x3611)+~P3(x3612,x3611,a2)+~P11(x3611,a2,x3613)+~P8(x3611,a1)+E(f9(x3611,x3612,x3613),x3612)+P3(f9(x3611,x3612,x3613),x3612,a2)+P1(f15(x3611,x3612,x3613)) % 5.24/5.37 [362]~P1(x3623)+~P1(x3622)+~P1(x3621)+~P3(x3622,x3621,a2)+~P10(x3621,a2,x3623)+~P8(x3621,a1)+E(f9(x3621,x3622,x3623),x3622)+P3(f9(x3621,x3622,x3623),x3622,a2)+P1(f15(x3621,x3622,x3623)) % 5.24/5.37 [363]~P1(x3633)+~P1(x3632)+~P1(x3631)+~P11(x3631,a2,x3633)+~P11(x3631,a2,x3632)+~P8(x3631,a1)+E(f9(x3631,x3632,x3633),x3633)+P3(f9(x3631,x3632,x3633),x3633,a2)+P1(f14(x3631,x3632,x3633)) % 5.24/5.37 [364]~P1(x3643)+~P1(x3642)+~P1(x3641)+~P11(x3641,a2,x3643)+~P10(x3641,a2,x3642)+~P8(x3641,a1)+E(f9(x3641,x3642,x3643),x3643)+P3(f9(x3641,x3642,x3643),x3643,a2)+P1(f14(x3641,x3642,x3643)) % 5.24/5.37 [365]~P1(x3653)+~P1(x3652)+~P1(x3651)+~P11(x3651,a2,x3652)+~P10(x3651,a2,x3653)+~P8(x3651,a1)+E(f9(x3651,x3652,x3653),x3653)+P3(f9(x3651,x3652,x3653),x3653,a2)+P1(f14(x3651,x3652,x3653)) % 5.24/5.37 [366]~P1(x3663)+~P1(x3662)+~P1(x3661)+~P10(x3661,a2,x3663)+~P10(x3661,a2,x3662)+~P8(x3661,a1)+E(f9(x3661,x3662,x3663),x3663)+P3(f9(x3661,x3662,x3663),x3663,a2)+P1(f14(x3661,x3662,x3663)) % 5.24/5.37 [367]~P1(x3673)+~P1(x3672)+~P1(x3671)+~P11(x3671,a2,x3673)+~P11(x3671,a2,x3672)+~P8(x3671,a1)+E(f9(x3671,x3672,x3673),x3672)+P3(f9(x3671,x3672,x3673),x3672,a2)+P1(f15(x3671,x3672,x3673)) % 5.24/5.37 [368]~P1(x3683)+~P1(x3682)+~P1(x3681)+~P11(x3681,a2,x3683)+~P10(x3681,a2,x3682)+~P8(x3681,a1)+E(f9(x3681,x3682,x3683),x3682)+P3(f9(x3681,x3682,x3683),x3682,a2)+P1(f15(x3681,x3682,x3683)) % 5.24/5.37 [369]~P1(x3693)+~P1(x3692)+~P1(x3691)+~P11(x3691,a2,x3692)+~P10(x3691,a2,x3693)+~P8(x3691,a1)+E(f9(x3691,x3692,x3693),x3692)+P3(f9(x3691,x3692,x3693),x3692,a2)+P1(f15(x3691,x3692,x3693)) % 5.24/5.37 [370]~P1(x3703)+~P1(x3702)+~P1(x3701)+~P10(x3701,a2,x3703)+~P10(x3701,a2,x3702)+~P8(x3701,a1)+E(f9(x3701,x3702,x3703),x3702)+P3(f9(x3701,x3702,x3703),x3702,a2)+P1(f15(x3701,x3702,x3703)) % 5.24/5.37 [379]~P1(x3793)+~P1(x3792)+~P1(x3791)+~P3(x3793,x3791,a2)+~P3(x3792,x3791,a2)+~P8(x3791,a1)+E(f9(x3791,x3792,x3793),x3793)+P3(f14(x3791,x3792,x3793),x3793,a2)+P3(f9(x3791,x3792,x3793),x3793,a2) % 5.24/5.37 [380]~P1(x3803)+~P1(x3802)+~P1(x3801)+~P3(x3803,x3801,a2)+~P3(x3802,x3801,a2)+~P8(x3801,a1)+E(f9(x3801,x3802,x3803),x3802)+P3(f15(x3801,x3802,x3803),x3802,a2)+P3(f9(x3801,x3802,x3803),x3802,a2) % 5.24/5.37 [381]~P1(x3813)+~P1(x3812)+~P1(x3811)+~P3(x3813,x3811,a2)+~P11(x3811,a2,x3812)+~P8(x3811,a1)+E(f9(x3811,x3812,x3813),x3813)+P3(f14(x3811,x3812,x3813),x3813,a2)+P3(f9(x3811,x3812,x3813),x3813,a2) % 5.24/5.37 [382]~P1(x3823)+~P1(x3822)+~P1(x3821)+~P3(x3823,x3821,a2)+~P10(x3821,a2,x3822)+~P8(x3821,a1)+E(f9(x3821,x3822,x3823),x3823)+P3(f14(x3821,x3822,x3823),x3823,a2)+P3(f9(x3821,x3822,x3823),x3823,a2) % 5.24/5.37 [383]~P1(x3833)+~P1(x3832)+~P1(x3831)+~P3(x3832,x3831,a2)+~P11(x3831,a2,x3833)+~P8(x3831,a1)+E(f9(x3831,x3832,x3833),x3833)+P3(f14(x3831,x3832,x3833),x3833,a2)+P3(f9(x3831,x3832,x3833),x3833,a2) % 5.24/5.37 [384]~P1(x3843)+~P1(x3842)+~P1(x3841)+~P3(x3842,x3841,a2)+~P10(x3841,a2,x3843)+~P8(x3841,a1)+E(f9(x3841,x3842,x3843),x3843)+P3(f14(x3841,x3842,x3843),x3843,a2)+P3(f9(x3841,x3842,x3843),x3843,a2) % 5.24/5.37 [385]~P1(x3853)+~P1(x3852)+~P1(x3851)+~P3(x3853,x3851,a2)+~P11(x3851,a2,x3852)+~P8(x3851,a1)+E(f9(x3851,x3852,x3853),x3852)+P3(f15(x3851,x3852,x3853),x3852,a2)+P3(f9(x3851,x3852,x3853),x3852,a2) % 5.24/5.37 [386]~P1(x3863)+~P1(x3862)+~P1(x3861)+~P3(x3863,x3861,a2)+~P10(x3861,a2,x3862)+~P8(x3861,a1)+E(f9(x3861,x3862,x3863),x3862)+P3(f15(x3861,x3862,x3863),x3862,a2)+P3(f9(x3861,x3862,x3863),x3862,a2) % 5.24/5.37 [387]~P1(x3873)+~P1(x3872)+~P1(x3871)+~P3(x3872,x3871,a2)+~P11(x3871,a2,x3873)+~P8(x3871,a1)+E(f9(x3871,x3872,x3873),x3872)+P3(f15(x3871,x3872,x3873),x3872,a2)+P3(f9(x3871,x3872,x3873),x3872,a2) % 5.24/5.37 [388]~P1(x3883)+~P1(x3882)+~P1(x3881)+~P3(x3882,x3881,a2)+~P10(x3881,a2,x3883)+~P8(x3881,a1)+E(f9(x3881,x3882,x3883),x3882)+P3(f15(x3881,x3882,x3883),x3882,a2)+P3(f9(x3881,x3882,x3883),x3882,a2) % 5.24/5.37 [389]~P1(x3893)+~P1(x3892)+~P1(x3891)+~P11(x3891,a2,x3893)+~P11(x3891,a2,x3892)+~P8(x3891,a1)+E(f9(x3891,x3892,x3893),x3893)+P3(f14(x3891,x3892,x3893),x3893,a2)+P3(f9(x3891,x3892,x3893),x3893,a2) % 5.24/5.37 [390]~P1(x3903)+~P1(x3902)+~P1(x3901)+~P11(x3901,a2,x3903)+~P10(x3901,a2,x3902)+~P8(x3901,a1)+E(f9(x3901,x3902,x3903),x3903)+P3(f14(x3901,x3902,x3903),x3903,a2)+P3(f9(x3901,x3902,x3903),x3903,a2) % 5.24/5.37 [391]~P1(x3913)+~P1(x3912)+~P1(x3911)+~P11(x3911,a2,x3912)+~P10(x3911,a2,x3913)+~P8(x3911,a1)+E(f9(x3911,x3912,x3913),x3913)+P3(f14(x3911,x3912,x3913),x3913,a2)+P3(f9(x3911,x3912,x3913),x3913,a2) % 5.24/5.37 [392]~P1(x3923)+~P1(x3922)+~P1(x3921)+~P10(x3921,a2,x3923)+~P10(x3921,a2,x3922)+~P8(x3921,a1)+E(f9(x3921,x3922,x3923),x3923)+P3(f14(x3921,x3922,x3923),x3923,a2)+P3(f9(x3921,x3922,x3923),x3923,a2) % 5.24/5.38 [393]~P1(x3933)+~P1(x3932)+~P1(x3931)+~P11(x3931,a2,x3933)+~P11(x3931,a2,x3932)+~P8(x3931,a1)+E(f9(x3931,x3932,x3933),x3932)+P3(f15(x3931,x3932,x3933),x3932,a2)+P3(f9(x3931,x3932,x3933),x3932,a2) % 5.24/5.38 [394]~P1(x3943)+~P1(x3942)+~P1(x3941)+~P11(x3941,a2,x3943)+~P10(x3941,a2,x3942)+~P8(x3941,a1)+E(f9(x3941,x3942,x3943),x3942)+P3(f15(x3941,x3942,x3943),x3942,a2)+P3(f9(x3941,x3942,x3943),x3942,a2) % 5.24/5.38 [395]~P1(x3953)+~P1(x3952)+~P1(x3951)+~P11(x3951,a2,x3952)+~P10(x3951,a2,x3953)+~P8(x3951,a1)+E(f9(x3951,x3952,x3953),x3952)+P3(f15(x3951,x3952,x3953),x3952,a2)+P3(f9(x3951,x3952,x3953),x3952,a2) % 5.24/5.38 [396]~P1(x3963)+~P1(x3962)+~P1(x3961)+~P10(x3961,a2,x3963)+~P10(x3961,a2,x3962)+~P8(x3961,a1)+E(f9(x3961,x3962,x3963),x3962)+P3(f15(x3961,x3962,x3963),x3962,a2)+P3(f9(x3961,x3962,x3963),x3962,a2) % 5.24/5.38 [403]~E(x4031,x4033)+~P1(x4033)+~P1(x4032)+~P1(x4031)+~P3(x4032,x4031,a2)+~P8(x4031,a1)+E(f9(x4031,x4032,x4033),x4033)+P11(f14(x4031,x4032,x4033),a2,f9(x4031,x4032,x4033))+P3(f9(x4031,x4032,x4033),x4033,a2) % 5.24/5.38 [404]~E(x4041,x4042)+~P1(x4043)+~P1(x4042)+~P1(x4041)+~P3(x4043,x4041,a2)+~P8(x4041,a1)+E(f9(x4041,x4042,x4043),x4043)+P11(f14(x4041,x4042,x4043),a2,f9(x4041,x4042,x4043))+P3(f9(x4041,x4042,x4043),x4043,a2) % 5.24/5.38 [405]~E(x4051,x4053)+~P1(x4053)+~P1(x4052)+~P1(x4051)+~P3(x4052,x4051,a2)+~P8(x4051,a1)+E(f9(x4051,x4052,x4053),x4052)+P11(f15(x4051,x4052,x4053),a2,f9(x4051,x4052,x4053))+P3(f9(x4051,x4052,x4053),x4052,a2) % 5.24/5.38 [406]~E(x4061,x4062)+~P1(x4063)+~P1(x4062)+~P1(x4061)+~P3(x4063,x4061,a2)+~P8(x4061,a1)+E(f9(x4061,x4062,x4063),x4062)+P11(f15(x4061,x4062,x4063),a2,f9(x4061,x4062,x4063))+P3(f9(x4061,x4062,x4063),x4062,a2) % 5.24/5.38 [407]~E(x4071,x4073)+~P1(x4073)+~P1(x4072)+~P1(x4071)+~P11(x4071,a2,x4072)+~P8(x4071,a1)+E(f9(x4071,x4072,x4073),x4073)+P11(f14(x4071,x4072,x4073),a2,f9(x4071,x4072,x4073))+P3(f9(x4071,x4072,x4073),x4073,a2) % 5.24/5.38 [408]~E(x4081,x4083)+~P1(x4083)+~P1(x4082)+~P1(x4081)+~P10(x4081,a2,x4082)+~P8(x4081,a1)+E(f9(x4081,x4082,x4083),x4083)+P11(f14(x4081,x4082,x4083),a2,f9(x4081,x4082,x4083))+P3(f9(x4081,x4082,x4083),x4083,a2) % 5.24/5.38 [409]~E(x4091,x4092)+~P1(x4093)+~P1(x4092)+~P1(x4091)+~P11(x4091,a2,x4093)+~P8(x4091,a1)+E(f9(x4091,x4092,x4093),x4093)+P11(f14(x4091,x4092,x4093),a2,f9(x4091,x4092,x4093))+P3(f9(x4091,x4092,x4093),x4093,a2) % 5.24/5.38 [410]~E(x4101,x4102)+~P1(x4103)+~P1(x4102)+~P1(x4101)+~P10(x4101,a2,x4103)+~P8(x4101,a1)+E(f9(x4101,x4102,x4103),x4103)+P11(f14(x4101,x4102,x4103),a2,f9(x4101,x4102,x4103))+P3(f9(x4101,x4102,x4103),x4103,a2) % 5.24/5.38 [411]~E(x4111,x4113)+~P1(x4113)+~P1(x4112)+~P1(x4111)+~P11(x4111,a2,x4112)+~P8(x4111,a1)+E(f9(x4111,x4112,x4113),x4112)+P11(f15(x4111,x4112,x4113),a2,f9(x4111,x4112,x4113))+P3(f9(x4111,x4112,x4113),x4112,a2) % 5.24/5.38 [412]~E(x4121,x4123)+~P1(x4123)+~P1(x4122)+~P1(x4121)+~P10(x4121,a2,x4122)+~P8(x4121,a1)+E(f9(x4121,x4122,x4123),x4122)+P11(f15(x4121,x4122,x4123),a2,f9(x4121,x4122,x4123))+P3(f9(x4121,x4122,x4123),x4122,a2) % 5.24/5.38 [413]~E(x4131,x4132)+~P1(x4133)+~P1(x4132)+~P1(x4131)+~P11(x4131,a2,x4133)+~P8(x4131,a1)+E(f9(x4131,x4132,x4133),x4132)+P11(f15(x4131,x4132,x4133),a2,f9(x4131,x4132,x4133))+P3(f9(x4131,x4132,x4133),x4132,a2) % 5.24/5.38 [414]~E(x4141,x4142)+~P1(x4143)+~P1(x4142)+~P1(x4141)+~P10(x4141,a2,x4143)+~P8(x4141,a1)+E(f9(x4141,x4142,x4143),x4142)+P11(f15(x4141,x4142,x4143),a2,f9(x4141,x4142,x4143))+P3(f9(x4141,x4142,x4143),x4142,a2) % 5.24/5.38 [441]~P1(x4413)+~P1(x4412)+~P1(x4411)+~P3(x4413,x4411,a2)+~P3(x4412,x4411,a2)+~P8(x4411,a1)+E(f9(x4411,x4412,x4413),x4413)+P11(f14(x4411,x4412,x4413),a2,f9(x4411,x4412,x4413))+P3(f9(x4411,x4412,x4413),x4413,a2) % 5.24/5.38 [442]~P1(x4423)+~P1(x4422)+~P1(x4421)+~P3(x4423,x4421,a2)+~P3(x4422,x4421,a2)+~P8(x4421,a1)+E(f9(x4421,x4422,x4423),x4422)+P11(f15(x4421,x4422,x4423),a2,f9(x4421,x4422,x4423))+P3(f9(x4421,x4422,x4423),x4422,a2) % 5.24/5.38 [443]~P1(x4433)+~P1(x4432)+~P1(x4431)+~P3(x4433,x4431,a2)+~P11(x4431,a2,x4432)+~P8(x4431,a1)+E(f9(x4431,x4432,x4433),x4433)+P11(f14(x4431,x4432,x4433),a2,f9(x4431,x4432,x4433))+P3(f9(x4431,x4432,x4433),x4433,a2) % 5.24/5.38 [444]~P1(x4443)+~P1(x4442)+~P1(x4441)+~P3(x4443,x4441,a2)+~P10(x4441,a2,x4442)+~P8(x4441,a1)+E(f9(x4441,x4442,x4443),x4443)+P11(f14(x4441,x4442,x4443),a2,f9(x4441,x4442,x4443))+P3(f9(x4441,x4442,x4443),x4443,a2) % 5.24/5.38 [445]~P1(x4453)+~P1(x4452)+~P1(x4451)+~P3(x4452,x4451,a2)+~P11(x4451,a2,x4453)+~P8(x4451,a1)+E(f9(x4451,x4452,x4453),x4453)+P11(f14(x4451,x4452,x4453),a2,f9(x4451,x4452,x4453))+P3(f9(x4451,x4452,x4453),x4453,a2) % 5.24/5.38 [446]~P1(x4463)+~P1(x4462)+~P1(x4461)+~P3(x4462,x4461,a2)+~P10(x4461,a2,x4463)+~P8(x4461,a1)+E(f9(x4461,x4462,x4463),x4463)+P11(f14(x4461,x4462,x4463),a2,f9(x4461,x4462,x4463))+P3(f9(x4461,x4462,x4463),x4463,a2) % 5.24/5.38 [447]~P1(x4473)+~P1(x4472)+~P1(x4471)+~P3(x4473,x4471,a2)+~P11(x4471,a2,x4472)+~P8(x4471,a1)+E(f9(x4471,x4472,x4473),x4472)+P11(f15(x4471,x4472,x4473),a2,f9(x4471,x4472,x4473))+P3(f9(x4471,x4472,x4473),x4472,a2) % 5.24/5.38 [448]~P1(x4483)+~P1(x4482)+~P1(x4481)+~P3(x4483,x4481,a2)+~P10(x4481,a2,x4482)+~P8(x4481,a1)+E(f9(x4481,x4482,x4483),x4482)+P11(f15(x4481,x4482,x4483),a2,f9(x4481,x4482,x4483))+P3(f9(x4481,x4482,x4483),x4482,a2) % 5.24/5.38 [449]~P1(x4493)+~P1(x4492)+~P1(x4491)+~P3(x4492,x4491,a2)+~P11(x4491,a2,x4493)+~P8(x4491,a1)+E(f9(x4491,x4492,x4493),x4492)+P11(f15(x4491,x4492,x4493),a2,f9(x4491,x4492,x4493))+P3(f9(x4491,x4492,x4493),x4492,a2) % 5.24/5.38 [450]~P1(x4503)+~P1(x4502)+~P1(x4501)+~P3(x4502,x4501,a2)+~P10(x4501,a2,x4503)+~P8(x4501,a1)+E(f9(x4501,x4502,x4503),x4502)+P11(f15(x4501,x4502,x4503),a2,f9(x4501,x4502,x4503))+P3(f9(x4501,x4502,x4503),x4502,a2) % 5.24/5.38 [451]~P1(x4513)+~P1(x4512)+~P1(x4511)+~P11(x4511,a2,x4513)+~P11(x4511,a2,x4512)+~P8(x4511,a1)+E(f9(x4511,x4512,x4513),x4513)+P11(f14(x4511,x4512,x4513),a2,f9(x4511,x4512,x4513))+P3(f9(x4511,x4512,x4513),x4513,a2) % 5.24/5.38 [452]~P1(x4523)+~P1(x4522)+~P1(x4521)+~P11(x4521,a2,x4523)+~P10(x4521,a2,x4522)+~P8(x4521,a1)+E(f9(x4521,x4522,x4523),x4523)+P11(f14(x4521,x4522,x4523),a2,f9(x4521,x4522,x4523))+P3(f9(x4521,x4522,x4523),x4523,a2) % 5.24/5.38 [453]~P1(x4533)+~P1(x4532)+~P1(x4531)+~P11(x4531,a2,x4532)+~P10(x4531,a2,x4533)+~P8(x4531,a1)+E(f9(x4531,x4532,x4533),x4533)+P11(f14(x4531,x4532,x4533),a2,f9(x4531,x4532,x4533))+P3(f9(x4531,x4532,x4533),x4533,a2) % 5.24/5.38 [454]~P1(x4543)+~P1(x4542)+~P1(x4541)+~P10(x4541,a2,x4543)+~P10(x4541,a2,x4542)+~P8(x4541,a1)+E(f9(x4541,x4542,x4543),x4543)+P11(f14(x4541,x4542,x4543),a2,f9(x4541,x4542,x4543))+P3(f9(x4541,x4542,x4543),x4543,a2) % 5.24/5.38 [455]~P1(x4553)+~P1(x4552)+~P1(x4551)+~P11(x4551,a2,x4553)+~P11(x4551,a2,x4552)+~P8(x4551,a1)+E(f9(x4551,x4552,x4553),x4552)+P11(f15(x4551,x4552,x4553),a2,f9(x4551,x4552,x4553))+P3(f9(x4551,x4552,x4553),x4552,a2) % 5.24/5.38 [456]~P1(x4563)+~P1(x4562)+~P1(x4561)+~P11(x4561,a2,x4563)+~P10(x4561,a2,x4562)+~P8(x4561,a1)+E(f9(x4561,x4562,x4563),x4562)+P11(f15(x4561,x4562,x4563),a2,f9(x4561,x4562,x4563))+P3(f9(x4561,x4562,x4563),x4562,a2) % 5.24/5.38 [457]~P1(x4573)+~P1(x4572)+~P1(x4571)+~P11(x4571,a2,x4572)+~P10(x4571,a2,x4573)+~P8(x4571,a1)+E(f9(x4571,x4572,x4573),x4572)+P11(f15(x4571,x4572,x4573),a2,f9(x4571,x4572,x4573))+P3(f9(x4571,x4572,x4573),x4572,a2) % 5.24/5.38 [458]~P1(x4583)+~P1(x4582)+~P1(x4581)+~P10(x4581,a2,x4583)+~P10(x4581,a2,x4582)+~P8(x4581,a1)+E(f9(x4581,x4582,x4583),x4582)+P11(f15(x4581,x4582,x4583),a2,f9(x4581,x4582,x4583))+P3(f9(x4581,x4582,x4583),x4582,a2) % 5.24/5.38 [226]~E(x2261,x2263)+~P1(x2263)+~P1(x2262)+~P1(x2261)+~P1(x2264)+~P3(x2264,x2261,a2)+~P11(x2264,a2,x2262)+~P8(x2261,a1)+P1(f9(x2261,x2262,x2263)) % 5.24/5.38 [227]~E(x2271,x2272)+~P1(x2273)+~P1(x2272)+~P1(x2271)+~P1(x2274)+~P3(x2274,x2271,a2)+~P11(x2274,a2,x2273)+~P8(x2271,a1)+P1(f9(x2271,x2272,x2273)) % 5.24/5.38 [264]~E(x2642,x2643)+~P1(x2643)+~P1(x2642)+~P1(x2641)+~P1(x2644)+~P3(x2644,x2642,a2)+~P11(x2644,a2,x2641)+~P8(x2642,a1)+P10(x2641,a2,f9(x2642,x2643,x2641)) % 5.24/5.38 [265]~E(x2651,x2652)+~P1(x2653)+~P1(x2652)+~P1(x2651)+~P1(x2654)+~P3(x2654,x2652,a2)+~P11(x2654,a2,x2653)+~P8(x2652,a1)+P10(x2651,a2,f9(x2652,x2653,x2651)) % 5.24/5.38 [266]~E(x2662,x2663)+~P1(x2663)+~P1(x2662)+~P1(x2661)+~P1(x2664)+~P3(x2664,x2662,a2)+~P11(x2664,a2,x2661)+~P8(x2662,a1)+P10(x2661,a2,f9(x2662,x2661,x2663)) % 5.24/5.38 [267]~E(x2671,x2672)+~P1(x2673)+~P1(x2672)+~P1(x2671)+~P1(x2674)+~P3(x2674,x2672,a2)+~P11(x2674,a2,x2673)+~P8(x2672,a1)+P10(x2671,a2,f9(x2672,x2671,x2673)) % 5.24/5.38 [270]~P1(x2703)+~P1(x2702)+~P1(x2701)+~P1(x2704)+~P3(x2704,x2701,a2)+~P3(x2703,x2701,a2)+~P11(x2704,a2,x2702)+~P8(x2701,a1)+P1(f9(x2701,x2702,x2703)) % 5.24/5.38 [271]~P1(x2713)+~P1(x2712)+~P1(x2711)+~P1(x2714)+~P3(x2714,x2711,a2)+~P3(x2712,x2711,a2)+~P11(x2714,a2,x2713)+~P8(x2711,a1)+P1(f9(x2711,x2712,x2713)) % 5.24/5.38 [272]~P1(x2723)+~P1(x2722)+~P1(x2721)+~P1(x2724)+~P3(x2724,x2721,a2)+~P11(x2724,a2,x2723)+~P11(x2721,a2,x2722)+~P8(x2721,a1)+P1(f9(x2721,x2722,x2723)) % 5.24/5.38 [273]~P1(x2733)+~P1(x2732)+~P1(x2731)+~P1(x2734)+~P3(x2734,x2731,a2)+~P11(x2734,a2,x2733)+~P10(x2731,a2,x2732)+~P8(x2731,a1)+P1(f9(x2731,x2732,x2733)) % 5.24/5.38 [274]~P1(x2743)+~P1(x2742)+~P1(x2741)+~P1(x2744)+~P3(x2744,x2741,a2)+~P11(x2744,a2,x2742)+~P11(x2741,a2,x2743)+~P8(x2741,a1)+P1(f9(x2741,x2742,x2743)) % 5.24/5.38 [275]~P1(x2753)+~P1(x2752)+~P1(x2751)+~P1(x2754)+~P3(x2754,x2751,a2)+~P11(x2754,a2,x2752)+~P10(x2751,a2,x2753)+~P8(x2751,a1)+P1(f9(x2751,x2752,x2753)) % 5.24/5.38 [312]~P1(x3123)+~P1(x3122)+~P1(x3121)+~P1(x3124)+~P3(x3124,x3122,a2)+~P3(x3123,x3122,a2)+~P11(x3124,a2,x3121)+~P8(x3122,a1)+P10(x3121,a2,f9(x3122,x3123,x3121)) % 5.24/5.38 [313]~P1(x3133)+~P1(x3132)+~P1(x3131)+~P1(x3134)+~P3(x3134,x3132,a2)+~P3(x3131,x3132,a2)+~P11(x3134,a2,x3133)+~P8(x3132,a1)+P10(x3131,a2,f9(x3132,x3133,x3131)) % 5.24/5.38 [314]~P1(x3143)+~P1(x3142)+~P1(x3141)+~P1(x3144)+~P3(x3144,x3142,a2)+~P3(x3143,x3142,a2)+~P11(x3144,a2,x3141)+~P8(x3142,a1)+P10(x3141,a2,f9(x3142,x3141,x3143)) % 5.24/5.38 [315]~P1(x3153)+~P1(x3152)+~P1(x3151)+~P1(x3154)+~P3(x3154,x3152,a2)+~P3(x3151,x3152,a2)+~P11(x3154,a2,x3153)+~P8(x3152,a1)+P10(x3151,a2,f9(x3152,x3151,x3153)) % 5.24/5.38 [316]~P1(x3163)+~P1(x3162)+~P1(x3161)+~P1(x3164)+~P3(x3164,x3162,a2)+~P11(x3164,a2,x3163)+~P11(x3162,a2,x3161)+~P8(x3162,a1)+P10(x3161,a2,f9(x3162,x3163,x3161)) % 5.24/5.38 [317]~P1(x3173)+~P1(x3172)+~P1(x3171)+~P1(x3174)+~P3(x3174,x3172,a2)+~P11(x3174,a2,x3173)+~P10(x3172,a2,x3171)+~P8(x3172,a1)+P10(x3171,a2,f9(x3172,x3173,x3171)) % 5.24/5.38 [318]~P1(x3183)+~P1(x3182)+~P1(x3181)+~P1(x3184)+~P3(x3184,x3182,a2)+~P11(x3184,a2,x3181)+~P11(x3182,a2,x3183)+~P8(x3182,a1)+P10(x3181,a2,f9(x3182,x3183,x3181)) % 5.24/5.38 [319]~P1(x3193)+~P1(x3192)+~P1(x3191)+~P1(x3194)+~P3(x3194,x3192,a2)+~P11(x3194,a2,x3191)+~P10(x3192,a2,x3193)+~P8(x3192,a1)+P10(x3191,a2,f9(x3192,x3193,x3191)) % 5.24/5.38 [320]~P1(x3203)+~P1(x3202)+~P1(x3201)+~P1(x3204)+~P3(x3204,x3202,a2)+~P11(x3204,a2,x3203)+~P11(x3202,a2,x3201)+~P8(x3202,a1)+P10(x3201,a2,f9(x3202,x3201,x3203)) % 5.24/5.38 [321]~P1(x3213)+~P1(x3212)+~P1(x3211)+~P1(x3214)+~P3(x3214,x3212,a2)+~P11(x3214,a2,x3213)+~P10(x3212,a2,x3211)+~P8(x3212,a1)+P10(x3211,a2,f9(x3212,x3211,x3213)) % 5.24/5.38 [322]~P1(x3223)+~P1(x3222)+~P1(x3221)+~P1(x3224)+~P3(x3224,x3222,a2)+~P11(x3224,a2,x3221)+~P11(x3222,a2,x3223)+~P8(x3222,a1)+P10(x3221,a2,f9(x3222,x3221,x3223)) % 5.24/5.38 [323]~P1(x3233)+~P1(x3232)+~P1(x3231)+~P1(x3234)+~P3(x3234,x3232,a2)+~P11(x3234,a2,x3231)+~P10(x3232,a2,x3233)+~P8(x3232,a1)+P10(x3231,a2,f9(x3232,x3231,x3233)) % 5.24/5.38 [296]~E(x2961,x2962)+~P1(x2962)+~P1(x2961)+~P1(x2963)+~P1(x2964)+~P3(x2964,x2961,a2)+~P11(x2964,a2,x2963)+~P8(x2961,a1)+E(f9(x2961,x2962,x2963),x2963)+P11(x2963,a2,f9(x2961,x2962,x2963)) % 5.24/5.38 [297]~E(x2973,x2971)+~P1(x2972)+~P1(x2971)+~P1(x2973)+~P1(x2974)+~P3(x2974,x2971,a2)+~P11(x2974,a2,x2972)+~P8(x2971,a1)+E(f9(x2971,x2972,x2973),x2973)+P11(x2973,a2,f9(x2971,x2972,x2973)) % 5.24/5.38 [298]~E(x2981,x2983)+~P1(x2983)+~P1(x2981)+~P1(x2982)+~P1(x2984)+~P3(x2984,x2981,a2)+~P11(x2984,a2,x2982)+~P8(x2981,a1)+E(f9(x2981,x2982,x2983),x2982)+P11(x2982,a2,f9(x2981,x2982,x2983)) % 5.24/5.38 [299]~E(x2992,x2991)+~P1(x2993)+~P1(x2991)+~P1(x2992)+~P1(x2994)+~P3(x2994,x2991,a2)+~P11(x2994,a2,x2993)+~P8(x2991,a1)+E(f9(x2991,x2992,x2993),x2992)+P11(x2992,a2,f9(x2991,x2992,x2993)) % 5.24/5.38 [339]~P1(x3392)+~P1(x3391)+~P1(x3393)+~P1(x3394)+~P3(x3394,x3391,a2)+~P3(x3392,x3391,a2)+~P11(x3394,a2,x3393)+~P8(x3391,a1)+E(f9(x3391,x3392,x3393),x3393)+P11(x3393,a2,f9(x3391,x3392,x3393)) % 5.24/5.38 [340]~P1(x3402)+~P1(x3401)+~P1(x3403)+~P1(x3404)+~P3(x3404,x3401,a2)+~P3(x3403,x3401,a2)+~P11(x3404,a2,x3402)+~P8(x3401,a1)+E(f9(x3401,x3402,x3403),x3403)+P11(x3403,a2,f9(x3401,x3402,x3403)) % 5.24/5.38 [341]~P1(x3413)+~P1(x3411)+~P1(x3412)+~P1(x3414)+~P3(x3414,x3411,a2)+~P3(x3413,x3411,a2)+~P11(x3414,a2,x3412)+~P8(x3411,a1)+E(f9(x3411,x3412,x3413),x3412)+P11(x3412,a2,f9(x3411,x3412,x3413)) % 5.24/5.38 [342]~P1(x3423)+~P1(x3421)+~P1(x3422)+~P1(x3424)+~P3(x3424,x3421,a2)+~P3(x3422,x3421,a2)+~P11(x3424,a2,x3423)+~P8(x3421,a1)+E(f9(x3421,x3422,x3423),x3422)+P11(x3422,a2,f9(x3421,x3422,x3423)) % 5.24/5.38 [343]~P1(x3432)+~P1(x3431)+~P1(x3433)+~P1(x3434)+~P3(x3434,x3431,a2)+~P11(x3434,a2,x3432)+~P11(x3431,a2,x3433)+~P8(x3431,a1)+E(f9(x3431,x3432,x3433),x3433)+P11(x3433,a2,f9(x3431,x3432,x3433)) % 5.24/5.38 [344]~P1(x3442)+~P1(x3441)+~P1(x3443)+~P1(x3444)+~P3(x3444,x3441,a2)+~P11(x3444,a2,x3442)+~P10(x3441,a2,x3443)+~P8(x3441,a1)+E(f9(x3441,x3442,x3443),x3443)+P11(x3443,a2,f9(x3441,x3442,x3443)) % 5.24/5.38 [345]~P1(x3452)+~P1(x3451)+~P1(x3453)+~P1(x3454)+~P3(x3454,x3451,a2)+~P11(x3454,a2,x3453)+~P11(x3451,a2,x3452)+~P8(x3451,a1)+E(f9(x3451,x3452,x3453),x3453)+P11(x3453,a2,f9(x3451,x3452,x3453)) % 5.24/5.38 [346]~P1(x3462)+~P1(x3461)+~P1(x3463)+~P1(x3464)+~P3(x3464,x3461,a2)+~P11(x3464,a2,x3463)+~P10(x3461,a2,x3462)+~P8(x3461,a1)+E(f9(x3461,x3462,x3463),x3463)+P11(x3463,a2,f9(x3461,x3462,x3463)) % 5.24/5.38 [347]~P1(x3473)+~P1(x3471)+~P1(x3472)+~P1(x3474)+~P3(x3474,x3471,a2)+~P11(x3474,a2,x3473)+~P11(x3471,a2,x3472)+~P8(x3471,a1)+E(f9(x3471,x3472,x3473),x3472)+P11(x3472,a2,f9(x3471,x3472,x3473)) % 5.24/5.38 [348]~P1(x3483)+~P1(x3481)+~P1(x3482)+~P1(x3484)+~P3(x3484,x3481,a2)+~P11(x3484,a2,x3483)+~P10(x3481,a2,x3482)+~P8(x3481,a1)+E(f9(x3481,x3482,x3483),x3482)+P11(x3482,a2,f9(x3481,x3482,x3483)) % 5.24/5.38 [349]~P1(x3493)+~P1(x3491)+~P1(x3492)+~P1(x3494)+~P3(x3494,x3491,a2)+~P11(x3494,a2,x3492)+~P11(x3491,a2,x3493)+~P8(x3491,a1)+E(f9(x3491,x3492,x3493),x3492)+P11(x3492,a2,f9(x3491,x3492,x3493)) % 5.24/5.38 [350]~P1(x3503)+~P1(x3501)+~P1(x3502)+~P1(x3504)+~P3(x3504,x3501,a2)+~P11(x3504,a2,x3502)+~P10(x3501,a2,x3503)+~P8(x3501,a1)+E(f9(x3501,x3502,x3503),x3502)+P11(x3502,a2,f9(x3501,x3502,x3503)) % 5.24/5.38 [371]~E(x3711,x3713)+~P1(x3713)+~P1(x3712)+~P1(x3711)+~P1(x3714)+~P3(x3714,x3711,a2)+~P11(x3714,a2,x3712)+~P8(x3711,a1)+E(f9(x3711,x3712,x3713),x3713)+P3(f9(x3711,x3712,x3713),x3713,a2)+P1(f14(x3711,x3712,x3713)) % 5.24/5.38 [372]~E(x3721,x3722)+~P1(x3723)+~P1(x3722)+~P1(x3721)+~P1(x3724)+~P3(x3724,x3721,a2)+~P11(x3724,a2,x3723)+~P8(x3721,a1)+E(f9(x3721,x3722,x3723),x3723)+P3(f9(x3721,x3722,x3723),x3723,a2)+P1(f14(x3721,x3722,x3723)) % 5.24/5.38 [373]~E(x3731,x3733)+~P1(x3733)+~P1(x3732)+~P1(x3731)+~P1(x3734)+~P3(x3734,x3731,a2)+~P11(x3734,a2,x3732)+~P8(x3731,a1)+E(f9(x3731,x3732,x3733),x3732)+P3(f9(x3731,x3732,x3733),x3732,a2)+P1(f15(x3731,x3732,x3733)) % 5.24/5.38 [374]~E(x3741,x3742)+~P1(x3743)+~P1(x3742)+~P1(x3741)+~P1(x3744)+~P3(x3744,x3741,a2)+~P11(x3744,a2,x3743)+~P8(x3741,a1)+E(f9(x3741,x3742,x3743),x3742)+P3(f9(x3741,x3742,x3743),x3742,a2)+P1(f15(x3741,x3742,x3743)) % 5.24/5.38 [397]~E(x3971,x3973)+~P1(x3973)+~P1(x3972)+~P1(x3971)+~P1(x3974)+~P3(x3974,x3971,a2)+~P11(x3974,a2,x3972)+~P8(x3971,a1)+E(f9(x3971,x3972,x3973),x3973)+P3(f14(x3971,x3972,x3973),x3973,a2)+P3(f9(x3971,x3972,x3973),x3973,a2) % 5.24/5.38 [398]~E(x3981,x3982)+~P1(x3983)+~P1(x3982)+~P1(x3981)+~P1(x3984)+~P3(x3984,x3981,a2)+~P11(x3984,a2,x3983)+~P8(x3981,a1)+E(f9(x3981,x3982,x3983),x3983)+P3(f14(x3981,x3982,x3983),x3983,a2)+P3(f9(x3981,x3982,x3983),x3983,a2) % 5.24/5.38 [399]~E(x3991,x3993)+~P1(x3993)+~P1(x3992)+~P1(x3991)+~P1(x3994)+~P3(x3994,x3991,a2)+~P11(x3994,a2,x3992)+~P8(x3991,a1)+E(f9(x3991,x3992,x3993),x3992)+P3(f15(x3991,x3992,x3993),x3992,a2)+P3(f9(x3991,x3992,x3993),x3992,a2) % 5.24/5.38 [400]~E(x4001,x4002)+~P1(x4003)+~P1(x4002)+~P1(x4001)+~P1(x4004)+~P3(x4004,x4001,a2)+~P11(x4004,a2,x4003)+~P8(x4001,a1)+E(f9(x4001,x4002,x4003),x4002)+P3(f15(x4001,x4002,x4003),x4002,a2)+P3(f9(x4001,x4002,x4003),x4002,a2) % 5.24/5.38 [415]~P1(x4153)+~P1(x4152)+~P1(x4151)+~P1(x4154)+~P3(x4154,x4151,a2)+~P3(x4153,x4151,a2)+~P11(x4154,a2,x4152)+~P8(x4151,a1)+E(f9(x4151,x4152,x4153),x4153)+P3(f9(x4151,x4152,x4153),x4153,a2)+P1(f14(x4151,x4152,x4153)) % 5.24/5.38 [416]~P1(x4163)+~P1(x4162)+~P1(x4161)+~P1(x4164)+~P3(x4164,x4161,a2)+~P3(x4162,x4161,a2)+~P11(x4164,a2,x4163)+~P8(x4161,a1)+E(f9(x4161,x4162,x4163),x4163)+P3(f9(x4161,x4162,x4163),x4163,a2)+P1(f14(x4161,x4162,x4163)) % 5.24/5.38 [417]~P1(x4173)+~P1(x4172)+~P1(x4171)+~P1(x4174)+~P3(x4174,x4171,a2)+~P3(x4173,x4171,a2)+~P11(x4174,a2,x4172)+~P8(x4171,a1)+E(f9(x4171,x4172,x4173),x4172)+P3(f9(x4171,x4172,x4173),x4172,a2)+P1(f15(x4171,x4172,x4173)) % 5.24/5.38 [418]~P1(x4183)+~P1(x4182)+~P1(x4181)+~P1(x4184)+~P3(x4184,x4181,a2)+~P3(x4182,x4181,a2)+~P11(x4184,a2,x4183)+~P8(x4181,a1)+E(f9(x4181,x4182,x4183),x4182)+P3(f9(x4181,x4182,x4183),x4182,a2)+P1(f15(x4181,x4182,x4183)) % 5.24/5.38 [419]~P1(x4193)+~P1(x4192)+~P1(x4191)+~P1(x4194)+~P3(x4194,x4191,a2)+~P11(x4194,a2,x4193)+~P11(x4191,a2,x4192)+~P8(x4191,a1)+E(f9(x4191,x4192,x4193),x4193)+P3(f9(x4191,x4192,x4193),x4193,a2)+P1(f14(x4191,x4192,x4193)) % 5.24/5.38 [420]~P1(x4203)+~P1(x4202)+~P1(x4201)+~P1(x4204)+~P3(x4204,x4201,a2)+~P11(x4204,a2,x4203)+~P10(x4201,a2,x4202)+~P8(x4201,a1)+E(f9(x4201,x4202,x4203),x4203)+P3(f9(x4201,x4202,x4203),x4203,a2)+P1(f14(x4201,x4202,x4203)) % 5.24/5.38 [421]~P1(x4213)+~P1(x4212)+~P1(x4211)+~P1(x4214)+~P3(x4214,x4211,a2)+~P11(x4214,a2,x4212)+~P11(x4211,a2,x4213)+~P8(x4211,a1)+E(f9(x4211,x4212,x4213),x4213)+P3(f9(x4211,x4212,x4213),x4213,a2)+P1(f14(x4211,x4212,x4213)) % 5.24/5.38 [422]~P1(x4223)+~P1(x4222)+~P1(x4221)+~P1(x4224)+~P3(x4224,x4221,a2)+~P11(x4224,a2,x4222)+~P10(x4221,a2,x4223)+~P8(x4221,a1)+E(f9(x4221,x4222,x4223),x4223)+P3(f9(x4221,x4222,x4223),x4223,a2)+P1(f14(x4221,x4222,x4223)) % 5.24/5.38 [423]~P1(x4233)+~P1(x4232)+~P1(x4231)+~P1(x4234)+~P3(x4234,x4231,a2)+~P11(x4234,a2,x4233)+~P11(x4231,a2,x4232)+~P8(x4231,a1)+E(f9(x4231,x4232,x4233),x4232)+P3(f9(x4231,x4232,x4233),x4232,a2)+P1(f15(x4231,x4232,x4233)) % 5.24/5.38 [424]~P1(x4243)+~P1(x4242)+~P1(x4241)+~P1(x4244)+~P3(x4244,x4241,a2)+~P11(x4244,a2,x4243)+~P10(x4241,a2,x4242)+~P8(x4241,a1)+E(f9(x4241,x4242,x4243),x4242)+P3(f9(x4241,x4242,x4243),x4242,a2)+P1(f15(x4241,x4242,x4243)) % 5.24/5.38 [425]~P1(x4253)+~P1(x4252)+~P1(x4251)+~P1(x4254)+~P3(x4254,x4251,a2)+~P11(x4254,a2,x4252)+~P11(x4251,a2,x4253)+~P8(x4251,a1)+E(f9(x4251,x4252,x4253),x4252)+P3(f9(x4251,x4252,x4253),x4252,a2)+P1(f15(x4251,x4252,x4253)) % 5.24/5.38 [426]~P1(x4263)+~P1(x4262)+~P1(x4261)+~P1(x4264)+~P3(x4264,x4261,a2)+~P11(x4264,a2,x4262)+~P10(x4261,a2,x4263)+~P8(x4261,a1)+E(f9(x4261,x4262,x4263),x4262)+P3(f9(x4261,x4262,x4263),x4262,a2)+P1(f15(x4261,x4262,x4263)) % 5.24/5.38 [429]~P1(x4293)+~P1(x4292)+~P1(x4291)+~P1(x4294)+~P3(x4294,x4291,a2)+~P3(x4293,x4291,a2)+~P11(x4294,a2,x4292)+~P8(x4291,a1)+E(f9(x4291,x4292,x4293),x4293)+P3(f14(x4291,x4292,x4293),x4293,a2)+P3(f9(x4291,x4292,x4293),x4293,a2) % 5.24/5.38 [430]~P1(x4303)+~P1(x4302)+~P1(x4301)+~P1(x4304)+~P3(x4304,x4301,a2)+~P3(x4302,x4301,a2)+~P11(x4304,a2,x4303)+~P8(x4301,a1)+E(f9(x4301,x4302,x4303),x4303)+P3(f14(x4301,x4302,x4303),x4303,a2)+P3(f9(x4301,x4302,x4303),x4303,a2) % 5.24/5.38 [431]~P1(x4313)+~P1(x4312)+~P1(x4311)+~P1(x4314)+~P3(x4314,x4311,a2)+~P3(x4313,x4311,a2)+~P11(x4314,a2,x4312)+~P8(x4311,a1)+E(f9(x4311,x4312,x4313),x4312)+P3(f15(x4311,x4312,x4313),x4312,a2)+P3(f9(x4311,x4312,x4313),x4312,a2) % 5.24/5.38 [432]~P1(x4323)+~P1(x4322)+~P1(x4321)+~P1(x4324)+~P3(x4324,x4321,a2)+~P3(x4322,x4321,a2)+~P11(x4324,a2,x4323)+~P8(x4321,a1)+E(f9(x4321,x4322,x4323),x4322)+P3(f15(x4321,x4322,x4323),x4322,a2)+P3(f9(x4321,x4322,x4323),x4322,a2) % 5.24/5.38 [433]~P1(x4333)+~P1(x4332)+~P1(x4331)+~P1(x4334)+~P3(x4334,x4331,a2)+~P11(x4334,a2,x4333)+~P11(x4331,a2,x4332)+~P8(x4331,a1)+E(f9(x4331,x4332,x4333),x4333)+P3(f14(x4331,x4332,x4333),x4333,a2)+P3(f9(x4331,x4332,x4333),x4333,a2) % 5.24/5.38 [434]~P1(x4343)+~P1(x4342)+~P1(x4341)+~P1(x4344)+~P3(x4344,x4341,a2)+~P11(x4344,a2,x4343)+~P10(x4341,a2,x4342)+~P8(x4341,a1)+E(f9(x4341,x4342,x4343),x4343)+P3(f14(x4341,x4342,x4343),x4343,a2)+P3(f9(x4341,x4342,x4343),x4343,a2) % 5.24/5.38 [435]~P1(x4353)+~P1(x4352)+~P1(x4351)+~P1(x4354)+~P3(x4354,x4351,a2)+~P11(x4354,a2,x4352)+~P11(x4351,a2,x4353)+~P8(x4351,a1)+E(f9(x4351,x4352,x4353),x4353)+P3(f14(x4351,x4352,x4353),x4353,a2)+P3(f9(x4351,x4352,x4353),x4353,a2) % 5.24/5.38 [436]~P1(x4363)+~P1(x4362)+~P1(x4361)+~P1(x4364)+~P3(x4364,x4361,a2)+~P11(x4364,a2,x4362)+~P10(x4361,a2,x4363)+~P8(x4361,a1)+E(f9(x4361,x4362,x4363),x4363)+P3(f14(x4361,x4362,x4363),x4363,a2)+P3(f9(x4361,x4362,x4363),x4363,a2) % 5.24/5.38 [437]~P1(x4373)+~P1(x4372)+~P1(x4371)+~P1(x4374)+~P3(x4374,x4371,a2)+~P11(x4374,a2,x4373)+~P11(x4371,a2,x4372)+~P8(x4371,a1)+E(f9(x4371,x4372,x4373),x4372)+P3(f15(x4371,x4372,x4373),x4372,a2)+P3(f9(x4371,x4372,x4373),x4372,a2) % 5.24/5.38 [438]~P1(x4383)+~P1(x4382)+~P1(x4381)+~P1(x4384)+~P3(x4384,x4381,a2)+~P11(x4384,a2,x4383)+~P10(x4381,a2,x4382)+~P8(x4381,a1)+E(f9(x4381,x4382,x4383),x4382)+P3(f15(x4381,x4382,x4383),x4382,a2)+P3(f9(x4381,x4382,x4383),x4382,a2) % 5.24/5.38 [439]~P1(x4393)+~P1(x4392)+~P1(x4391)+~P1(x4394)+~P3(x4394,x4391,a2)+~P11(x4394,a2,x4392)+~P11(x4391,a2,x4393)+~P8(x4391,a1)+E(f9(x4391,x4392,x4393),x4392)+P3(f15(x4391,x4392,x4393),x4392,a2)+P3(f9(x4391,x4392,x4393),x4392,a2) % 5.24/5.38 [440]~P1(x4403)+~P1(x4402)+~P1(x4401)+~P1(x4404)+~P3(x4404,x4401,a2)+~P11(x4404,a2,x4402)+~P10(x4401,a2,x4403)+~P8(x4401,a1)+E(f9(x4401,x4402,x4403),x4402)+P3(f15(x4401,x4402,x4403),x4402,a2)+P3(f9(x4401,x4402,x4403),x4402,a2) % 5.24/5.38 [459]~E(x4591,x4593)+~P1(x4593)+~P1(x4592)+~P1(x4591)+~P1(x4594)+~P3(x4594,x4591,a2)+~P11(x4594,a2,x4592)+~P8(x4591,a1)+E(f9(x4591,x4592,x4593),x4593)+P11(f14(x4591,x4592,x4593),a2,f9(x4591,x4592,x4593))+P3(f9(x4591,x4592,x4593),x4593,a2) % 5.24/5.38 [460]~E(x4601,x4602)+~P1(x4603)+~P1(x4602)+~P1(x4601)+~P1(x4604)+~P3(x4604,x4601,a2)+~P11(x4604,a2,x4603)+~P8(x4601,a1)+E(f9(x4601,x4602,x4603),x4603)+P11(f14(x4601,x4602,x4603),a2,f9(x4601,x4602,x4603))+P3(f9(x4601,x4602,x4603),x4603,a2) % 5.24/5.38 [461]~E(x4611,x4613)+~P1(x4613)+~P1(x4612)+~P1(x4611)+~P1(x4614)+~P3(x4614,x4611,a2)+~P11(x4614,a2,x4612)+~P8(x4611,a1)+E(f9(x4611,x4612,x4613),x4612)+P11(f15(x4611,x4612,x4613),a2,f9(x4611,x4612,x4613))+P3(f9(x4611,x4612,x4613),x4612,a2) % 5.24/5.38 [462]~E(x4621,x4622)+~P1(x4623)+~P1(x4622)+~P1(x4621)+~P1(x4624)+~P3(x4624,x4621,a2)+~P11(x4624,a2,x4623)+~P8(x4621,a1)+E(f9(x4621,x4622,x4623),x4622)+P11(f15(x4621,x4622,x4623),a2,f9(x4621,x4622,x4623))+P3(f9(x4621,x4622,x4623),x4622,a2) % 5.24/5.38 [473]~P1(x4733)+~P1(x4732)+~P1(x4731)+~P1(x4734)+~P3(x4734,x4731,a2)+~P3(x4733,x4731,a2)+~P11(x4734,a2,x4732)+~P8(x4731,a1)+E(f9(x4731,x4732,x4733),x4733)+P11(f14(x4731,x4732,x4733),a2,f9(x4731,x4732,x4733))+P3(f9(x4731,x4732,x4733),x4733,a2) % 5.24/5.38 [474]~P1(x4743)+~P1(x4742)+~P1(x4741)+~P1(x4744)+~P3(x4744,x4741,a2)+~P3(x4742,x4741,a2)+~P11(x4744,a2,x4743)+~P8(x4741,a1)+E(f9(x4741,x4742,x4743),x4743)+P11(f14(x4741,x4742,x4743),a2,f9(x4741,x4742,x4743))+P3(f9(x4741,x4742,x4743),x4743,a2) % 5.24/5.38 [475]~P1(x4753)+~P1(x4752)+~P1(x4751)+~P1(x4754)+~P3(x4754,x4751,a2)+~P3(x4753,x4751,a2)+~P11(x4754,a2,x4752)+~P8(x4751,a1)+E(f9(x4751,x4752,x4753),x4752)+P11(f15(x4751,x4752,x4753),a2,f9(x4751,x4752,x4753))+P3(f9(x4751,x4752,x4753),x4752,a2) % 5.24/5.38 [476]~P1(x4763)+~P1(x4762)+~P1(x4761)+~P1(x4764)+~P3(x4764,x4761,a2)+~P3(x4762,x4761,a2)+~P11(x4764,a2,x4763)+~P8(x4761,a1)+E(f9(x4761,x4762,x4763),x4762)+P11(f15(x4761,x4762,x4763),a2,f9(x4761,x4762,x4763))+P3(f9(x4761,x4762,x4763),x4762,a2) % 5.24/5.38 [477]~P1(x4773)+~P1(x4772)+~P1(x4771)+~P1(x4774)+~P3(x4774,x4771,a2)+~P11(x4774,a2,x4773)+~P11(x4771,a2,x4772)+~P8(x4771,a1)+E(f9(x4771,x4772,x4773),x4773)+P11(f14(x4771,x4772,x4773),a2,f9(x4771,x4772,x4773))+P3(f9(x4771,x4772,x4773),x4773,a2) % 5.24/5.38 [478]~P1(x4783)+~P1(x4782)+~P1(x4781)+~P1(x4784)+~P3(x4784,x4781,a2)+~P11(x4784,a2,x4783)+~P10(x4781,a2,x4782)+~P8(x4781,a1)+E(f9(x4781,x4782,x4783),x4783)+P11(f14(x4781,x4782,x4783),a2,f9(x4781,x4782,x4783))+P3(f9(x4781,x4782,x4783),x4783,a2) % 5.24/5.38 [479]~P1(x4793)+~P1(x4792)+~P1(x4791)+~P1(x4794)+~P3(x4794,x4791,a2)+~P11(x4794,a2,x4792)+~P11(x4791,a2,x4793)+~P8(x4791,a1)+E(f9(x4791,x4792,x4793),x4793)+P11(f14(x4791,x4792,x4793),a2,f9(x4791,x4792,x4793))+P3(f9(x4791,x4792,x4793),x4793,a2) % 5.24/5.38 [480]~P1(x4803)+~P1(x4802)+~P1(x4801)+~P1(x4804)+~P3(x4804,x4801,a2)+~P11(x4804,a2,x4802)+~P10(x4801,a2,x4803)+~P8(x4801,a1)+E(f9(x4801,x4802,x4803),x4803)+P11(f14(x4801,x4802,x4803),a2,f9(x4801,x4802,x4803))+P3(f9(x4801,x4802,x4803),x4803,a2) % 5.24/5.38 [481]~P1(x4813)+~P1(x4812)+~P1(x4811)+~P1(x4814)+~P3(x4814,x4811,a2)+~P11(x4814,a2,x4813)+~P11(x4811,a2,x4812)+~P8(x4811,a1)+E(f9(x4811,x4812,x4813),x4812)+P11(f15(x4811,x4812,x4813),a2,f9(x4811,x4812,x4813))+P3(f9(x4811,x4812,x4813),x4812,a2) % 5.24/5.38 [482]~P1(x4823)+~P1(x4822)+~P1(x4821)+~P1(x4824)+~P3(x4824,x4821,a2)+~P11(x4824,a2,x4823)+~P10(x4821,a2,x4822)+~P8(x4821,a1)+E(f9(x4821,x4822,x4823),x4822)+P11(f15(x4821,x4822,x4823),a2,f9(x4821,x4822,x4823))+P3(f9(x4821,x4822,x4823),x4822,a2) % 5.24/5.38 [483]~P1(x4833)+~P1(x4832)+~P1(x4831)+~P1(x4834)+~P3(x4834,x4831,a2)+~P11(x4834,a2,x4832)+~P11(x4831,a2,x4833)+~P8(x4831,a1)+E(f9(x4831,x4832,x4833),x4832)+P11(f15(x4831,x4832,x4833),a2,f9(x4831,x4832,x4833))+P3(f9(x4831,x4832,x4833),x4832,a2) % 5.24/5.38 [484]~P1(x4843)+~P1(x4842)+~P1(x4841)+~P1(x4844)+~P3(x4844,x4841,a2)+~P11(x4844,a2,x4842)+~P10(x4841,a2,x4843)+~P8(x4841,a1)+E(f9(x4841,x4842,x4843),x4842)+P11(f15(x4841,x4842,x4843),a2,f9(x4841,x4842,x4843))+P3(f9(x4841,x4842,x4843),x4842,a2) % 5.24/5.38 [324]~P1(x3243)+~P1(x3242)+~P1(x3241)+~P1(x3244)+~P1(x3245)+~P3(x3244,x3241,a2)+~P3(x3245,x3241,a2)+~P11(x3244,a2,x3242)+~P11(x3245,a2,x3243)+~P8(x3241,a1)+P1(f9(x3241,x3242,x3243)) % 5.24/5.38 [375]~P1(x3753)+~P1(x3752)+~P1(x3751)+~P1(x3754)+~P1(x3755)+~P3(x3754,x3752,a2)+~P3(x3755,x3752,a2)+~P11(x3754,a2,x3753)+~P11(x3755,a2,x3751)+~P8(x3752,a1)+P10(x3751,a2,f9(x3752,x3753,x3751)) % 5.24/5.38 [376]~P1(x3763)+~P1(x3762)+~P1(x3761)+~P1(x3764)+~P1(x3765)+~P3(x3764,x3762,a2)+~P3(x3765,x3762,a2)+~P11(x3764,a2,x3761)+~P11(x3765,a2,x3763)+~P8(x3762,a1)+P10(x3761,a2,f9(x3762,x3761,x3763)) % 5.24/5.38 [401]~P1(x4012)+~P1(x4011)+~P1(x4013)+~P1(x4014)+~P1(x4015)+~P3(x4014,x4011,a2)+~P3(x4015,x4011,a2)+~P11(x4014,a2,x4012)+~P11(x4015,a2,x4013)+~P8(x4011,a1)+E(f9(x4011,x4012,x4013),x4013)+P11(x4013,a2,f9(x4011,x4012,x4013)) % 5.24/5.38 [402]~P1(x4023)+~P1(x4021)+~P1(x4022)+~P1(x4024)+~P1(x4025)+~P3(x4024,x4021,a2)+~P3(x4025,x4021,a2)+~P11(x4024,a2,x4022)+~P11(x4025,a2,x4023)+~P8(x4021,a1)+E(f9(x4021,x4022,x4023),x4022)+P11(x4022,a2,f9(x4021,x4022,x4023)) % 5.24/5.38 [465]~P1(x4653)+~P1(x4652)+~P1(x4651)+~P1(x4654)+~P1(x4655)+~P3(x4654,x4651,a2)+~P3(x4655,x4651,a2)+~P11(x4654,a2,x4652)+~P11(x4655,a2,x4653)+~P8(x4651,a1)+E(f9(x4651,x4652,x4653),x4653)+P3(f9(x4651,x4652,x4653),x4653,a2)+P1(f14(x4651,x4652,x4653)) % 5.24/5.38 [466]~P1(x4663)+~P1(x4662)+~P1(x4661)+~P1(x4664)+~P1(x4665)+~P3(x4664,x4661,a2)+~P3(x4665,x4661,a2)+~P11(x4664,a2,x4662)+~P11(x4665,a2,x4663)+~P8(x4661,a1)+E(f9(x4661,x4662,x4663),x4662)+P3(f9(x4661,x4662,x4663),x4662,a2)+P1(f15(x4661,x4662,x4663)) % 5.24/5.38 [471]~P1(x4713)+~P1(x4712)+~P1(x4711)+~P1(x4714)+~P1(x4715)+~P3(x4714,x4711,a2)+~P3(x4715,x4711,a2)+~P11(x4714,a2,x4712)+~P11(x4715,a2,x4713)+~P8(x4711,a1)+E(f9(x4711,x4712,x4713),x4713)+P3(f14(x4711,x4712,x4713),x4713,a2)+P3(f9(x4711,x4712,x4713),x4713,a2) % 5.24/5.38 [472]~P1(x4723)+~P1(x4722)+~P1(x4721)+~P1(x4724)+~P1(x4725)+~P3(x4724,x4721,a2)+~P3(x4725,x4721,a2)+~P11(x4724,a2,x4722)+~P11(x4725,a2,x4723)+~P8(x4721,a1)+E(f9(x4721,x4722,x4723),x4722)+P3(f15(x4721,x4722,x4723),x4722,a2)+P3(f9(x4721,x4722,x4723),x4722,a2) % 5.24/5.38 [485]~P1(x4853)+~P1(x4852)+~P1(x4851)+~P1(x4854)+~P1(x4855)+~P3(x4854,x4851,a2)+~P3(x4855,x4851,a2)+~P11(x4854,a2,x4852)+~P11(x4855,a2,x4853)+~P8(x4851,a1)+E(f9(x4851,x4852,x4853),x4853)+P11(f14(x4851,x4852,x4853),a2,f9(x4851,x4852,x4853))+P3(f9(x4851,x4852,x4853),x4853,a2) % 5.24/5.38 [486]~P1(x4863)+~P1(x4862)+~P1(x4861)+~P1(x4864)+~P1(x4865)+~P3(x4864,x4861,a2)+~P3(x4865,x4861,a2)+~P11(x4864,a2,x4862)+~P11(x4865,a2,x4863)+~P8(x4861,a1)+E(f9(x4861,x4862,x4863),x4862)+P11(f15(x4861,x4862,x4863),a2,f9(x4861,x4862,x4863))+P3(f9(x4861,x4862,x4863),x4862,a2) % 5.24/5.38 %EqnAxiom % 5.24/5.38 [1]E(x11,x11) % 5.24/5.38 [2]E(x22,x21)+~E(x21,x22) % 5.24/5.38 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 5.24/5.38 [4]~E(x41,x42)+E(f24(x41),f24(x42)) % 5.24/5.38 [5]~E(x51,x52)+E(f29(x51),f29(x52)) % 5.24/5.38 [6]~E(x61,x62)+E(f30(x61),f30(x62)) % 5.24/5.38 [7]~E(x71,x72)+E(f31(x71),f31(x72)) % 5.24/5.38 [8]~E(x81,x82)+E(f33(x81),f33(x82)) % 5.24/5.38 [9]~E(x91,x92)+E(f34(x91),f34(x92)) % 5.24/5.38 [10]~E(x101,x102)+E(f4(x101),f4(x102)) % 5.24/5.38 [11]~E(x111,x112)+E(f5(x111),f5(x112)) % 5.24/5.38 [12]~E(x121,x122)+E(f9(x121,x123,x124),f9(x122,x123,x124)) % 5.24/5.38 [13]~E(x131,x132)+E(f9(x133,x131,x134),f9(x133,x132,x134)) % 5.24/5.38 [14]~E(x141,x142)+E(f9(x143,x144,x141),f9(x143,x144,x142)) % 5.24/5.38 [15]~E(x151,x152)+E(f15(x151,x153,x154),f15(x152,x153,x154)) % 5.24/5.38 [16]~E(x161,x162)+E(f15(x163,x161,x164),f15(x163,x162,x164)) % 5.24/5.38 [17]~E(x171,x172)+E(f15(x173,x174,x171),f15(x173,x174,x172)) % 5.24/5.38 [18]~E(x181,x182)+E(f14(x181,x183,x184),f14(x182,x183,x184)) % 5.24/5.38 [19]~E(x191,x192)+E(f14(x193,x191,x194),f14(x193,x192,x194)) % 5.24/5.38 [20]~E(x201,x202)+E(f14(x203,x204,x201),f14(x203,x204,x202)) % 5.24/5.38 [21]~E(x211,x212)+E(f10(x211,x213,x214),f10(x212,x213,x214)) % 5.24/5.38 [22]~E(x221,x222)+E(f10(x223,x221,x224),f10(x223,x222,x224)) % 5.24/5.38 [23]~E(x231,x232)+E(f10(x233,x234,x231),f10(x233,x234,x232)) % 5.24/5.38 [24]~E(x241,x242)+E(f12(x241,x243,x244),f12(x242,x243,x244)) % 5.24/5.38 [25]~E(x251,x252)+E(f12(x253,x251,x254),f12(x253,x252,x254)) % 5.24/5.38 [26]~E(x261,x262)+E(f12(x263,x264,x261),f12(x263,x264,x262)) % 5.24/5.38 [27]~E(x271,x272)+E(f13(x271,x273,x274),f13(x272,x273,x274)) % 5.24/5.38 [28]~E(x281,x282)+E(f13(x283,x281,x284),f13(x283,x282,x284)) % 5.24/5.38 [29]~E(x291,x292)+E(f13(x293,x294,x291),f13(x293,x294,x292)) % 5.24/5.38 [30]~E(x301,x302)+E(f11(x301,x303,x304),f11(x302,x303,x304)) % 5.24/5.38 [31]~E(x311,x312)+E(f11(x313,x311,x314),f11(x313,x312,x314)) % 5.24/5.38 [32]~E(x321,x322)+E(f11(x323,x324,x321),f11(x323,x324,x322)) % 5.24/5.38 [33]~E(x331,x332)+E(f27(x331,x333,x334,x335),f27(x332,x333,x334,x335)) % 5.24/5.38 [34]~E(x341,x342)+E(f27(x343,x341,x344,x345),f27(x343,x342,x344,x345)) % 5.24/5.38 [35]~E(x351,x352)+E(f27(x353,x354,x351,x355),f27(x353,x354,x352,x355)) % 5.24/5.38 [36]~E(x361,x362)+E(f27(x363,x364,x365,x361),f27(x363,x364,x365,x362)) % 5.24/5.38 [37]~E(x371,x372)+E(f32(x371,x373,x374,x375),f32(x372,x373,x374,x375)) % 5.24/5.38 [38]~E(x381,x382)+E(f32(x383,x381,x384,x385),f32(x383,x382,x384,x385)) % 5.24/5.38 [39]~E(x391,x392)+E(f32(x393,x394,x391,x395),f32(x393,x394,x392,x395)) % 5.24/5.38 [40]~E(x401,x402)+E(f32(x403,x404,x405,x401),f32(x403,x404,x405,x402)) % 5.24/5.38 [41]~E(x411,x412)+E(f8(x411,x413,x414),f8(x412,x413,x414)) % 5.24/5.38 [42]~E(x421,x422)+E(f8(x423,x421,x424),f8(x423,x422,x424)) % 5.24/5.38 [43]~E(x431,x432)+E(f8(x433,x434,x431),f8(x433,x434,x432)) % 5.24/5.38 [44]~E(x441,x442)+E(f7(x441,x443),f7(x442,x443)) % 5.24/5.38 [45]~E(x451,x452)+E(f7(x453,x451),f7(x453,x452)) % 5.24/5.38 [46]~P1(x461)+P1(x462)+~E(x461,x462) % 5.24/5.38 [47]P11(x472,x473,x474)+~E(x471,x472)+~P11(x471,x473,x474) % 5.24/5.38 [48]P11(x483,x482,x484)+~E(x481,x482)+~P11(x483,x481,x484) % 5.24/5.38 [49]P11(x493,x494,x492)+~E(x491,x492)+~P11(x493,x494,x491) % 5.24/5.38 [50]P3(x502,x503,x504)+~E(x501,x502)+~P3(x501,x503,x504) % 5.24/5.38 [51]P3(x513,x512,x514)+~E(x511,x512)+~P3(x513,x511,x514) % 5.24/5.38 [52]P3(x523,x524,x522)+~E(x521,x522)+~P3(x523,x524,x521) % 5.24/5.38 [53]~P2(x531)+P2(x532)+~E(x531,x532) % 5.24/5.38 [54]~P5(x541)+P5(x542)+~E(x541,x542) % 5.24/5.38 [55]~P9(x551)+P9(x552)+~E(x551,x552) % 5.24/5.38 [56]P10(x562,x563,x564)+~E(x561,x562)+~P10(x561,x563,x564) % 5.24/5.38 [57]P10(x573,x572,x574)+~E(x571,x572)+~P10(x573,x571,x574) % 5.24/5.38 [58]P10(x583,x584,x582)+~E(x581,x582)+~P10(x583,x584,x581) % 5.24/5.38 [59]P8(x592,x593)+~E(x591,x592)+~P8(x591,x593) % 5.24/5.38 [60]P8(x603,x602)+~E(x601,x602)+~P8(x603,x601) % 5.24/5.38 [61]~P6(x611)+P6(x612)+~E(x611,x612) % 5.24/5.38 [62]P4(x622,x623,x624)+~E(x621,x622)+~P4(x621,x623,x624) % 5.24/5.38 [63]P4(x633,x632,x634)+~E(x631,x632)+~P4(x633,x631,x634) % 5.24/5.38 [64]P4(x643,x644,x642)+~E(x641,x642)+~P4(x643,x644,x641) % 5.24/5.38 [65]~P7(x651)+P7(x652)+~E(x651,x652) % 5.24/5.38 % 5.24/5.38 %------------------------------------------- % 5.24/5.38 cnf(487,plain, % 5.24/5.38 (~P1(x4871)+~P1(x4871)+P10(x4871,x4872,x4871)+~P2(x4872)), % 5.24/5.38 inference(equality_inference,[],[121])). % 5.24/5.38 cnf(490,plain, % 5.24/5.38 (~P1(a35)+~P11(a36,a2,a35)), % 5.24/5.38 inference(equality_inference,[],[125])). % 5.24/5.38 cnf(491,plain, % 5.24/5.38 (~P1(a35)+~P10(a36,a2,a35)), % 5.24/5.38 inference(equality_inference,[],[126])). % 5.24/5.38 cnf(492,plain, % 5.24/5.38 (~P1(a36)+~P11(a35,a2,a36)), % 5.24/5.38 inference(equality_inference,[],[127])). % 5.24/5.38 cnf(493,plain, % 5.24/5.38 (~P1(a36)+~P10(a35,a2,a36)), % 5.24/5.38 inference(equality_inference,[],[128])). % 5.24/5.38 cnf(495,plain, % 5.24/5.38 (~P1(a36)+~P1(x4951)+~P11(x4951,a2,a36)+~P3(x4951,a35,a2)), % 5.24/5.38 inference(equality_inference,[],[172])). % 5.24/5.38 cnf(499,plain, % 5.24/5.38 (~P1(x4991)+~P1(x4991)+~P1(x4992)+~P10(x4991,a2,x4992)+~P8(x4991,a1)+P1(f9(x4991,x4992,x4991))), % 5.24/5.38 inference(equality_inference,[],[182])). % 5.24/5.38 cnf(501,plain, % 5.24/5.38 (~P1(x5011)+~P1(x5011)+~P1(x5012)+~P10(x5011,a2,x5012)+~P8(x5011,a1)+P1(f9(x5011,x5011,x5012))), % 5.24/5.38 inference(equality_inference,[],[184])). % 5.24/5.38 cnf(507,plain, % 5.24/5.38 (~P1(x5071)+~P1(x5071)+~P1(x5072)+~P10(x5071,a2,x5072)+~P8(x5071,a1)+P10(x5072,a2,f9(x5071,x5071,x5072))), % 5.24/5.38 inference(equality_inference,[],[206])). % 5.24/5.38 cnf(509,plain, % 5.24/5.38 (~P1(x5091)+~P1(x5091)+~P1(x5092)+~P10(x5091,a2,x5092)+~P8(x5091,a1)+P10(x5091,a2,f9(x5091,x5092,x5091))), % 5.24/5.38 inference(equality_inference,[],[208])). % 5.24/5.38 cnf(511,plain, % 5.24/5.38 (~P1(x5111)+~P1(x5111)+~P1(x5112)+~P10(x5111,a2,x5112)+~P8(x5111,a1)+P10(x5112,a2,f9(x5111,x5112,x5111))), % 5.24/5.38 inference(equality_inference,[],[210])). % 5.24/5.38 cnf(513,plain, % 5.24/5.38 (~P1(x5131)+~P1(x5131)+~P1(x5132)+~P10(x5131,a2,x5132)+~P8(x5131,a1)+P10(x5131,a2,f9(x5131,x5131,x5132))), % 5.24/5.38 inference(equality_inference,[],[212])). % 5.24/5.38 cnf(586,plain, % 5.24/5.38 (~P11(a36,a2,a35)), % 5.24/5.38 inference(scs_inference,[],[67,490])). % 5.24/5.38 cnf(587,plain, % 5.24/5.38 (~P10(a36,a2,a35)), % 5.24/5.38 inference(scs_inference,[],[67,491])). % 5.24/5.38 cnf(588,plain, % 5.24/5.38 (~P11(a35,a2,a36)), % 5.24/5.38 inference(scs_inference,[],[68,492])). % 5.24/5.38 cnf(589,plain, % 5.24/5.38 (~P10(a35,a2,a36)), % 5.24/5.38 inference(scs_inference,[],[68,493])). % 5.24/5.38 cnf(591,plain, % 5.24/5.38 (~P1(x5911)+~P11(x5911,a2,a36)+~P3(x5911,a35,a2)), % 5.24/5.38 inference(scs_inference,[],[68,495])). % 5.24/5.38 cnf(595,plain, % 5.24/5.38 (~E(a1,a36)), % 5.24/5.38 inference(scs_inference,[],[72,66,67,69,487,56,126])). % 5.24/5.38 cnf(599,plain, % 5.24/5.38 (P11(a1,a2,a36)), % 5.24/5.38 inference(scs_inference,[],[595,88])). % 5.24/5.38 cnf(606,plain, % 5.24/5.38 (P10(a36,a2,a36)), % 5.24/5.38 inference(scs_inference,[],[73,587,589,68,69,56,153,487])). % 5.24/5.38 cnf(608,plain, % 5.24/5.38 (P11(a1,a2,a35)), % 5.24/5.38 inference(scs_inference,[],[72,73,587,589,68,67,66,69,56,153,487,161])). % 5.24/5.38 cnf(616,plain, % 5.24/5.38 (P8(a35,a1)), % 5.24/5.38 inference(scs_inference,[],[72,73,586,587,589,68,67,66,69,56,153,487,161,189,48,126,58,151])). % 5.24/5.38 cnf(634,plain, % 5.24/5.38 (P6(a5000)), % 5.24/5.38 inference(scs_inference,[],[608,599,157])). % 5.24/5.38 cnf(645,plain, % 5.24/5.38 (P1(f9(a35,a35,a35))), % 5.24/5.38 inference(scs_inference,[],[589,599,67,68,66,616,69,591,151,153,487,499])). % 5.24/5.38 cnf(649,plain, % 5.24/5.38 (P10(a35,a2,f9(a35,a35,a35))), % 5.24/5.38 inference(scs_inference,[],[589,599,606,67,68,66,616,69,591,151,153,487,499,501,507])). % 5.24/5.38 cnf(651,plain, % 5.24/5.38 (P10(a36,a2,f9(a36,a36,a36))), % 5.24/5.38 inference(scs_inference,[],[589,599,606,67,68,66,616,69,591,151,153,487,499,501,507,509])). % 5.24/5.38 cnf(653,plain, % 5.24/5.38 (~P10(f9(a35,a35,a35),a2,a36)), % 5.24/5.38 inference(scs_inference,[],[589,599,606,67,68,66,616,69,591,151,153,487,499,501,507,509,191])). % 5.24/5.38 cnf(657,plain, % 5.24/5.38 (~P10(a36,a2,f9(a35,a35,a35))), % 5.24/5.38 inference(scs_inference,[],[589,599,606,67,68,66,616,69,591,151,153,487,499,501,507,509,191,128,170])). % 5.24/5.38 cnf(674,plain, % 5.24/5.38 (P1(a3)), % 5.24/5.38 inference(scs_inference,[],[634,74])). % 5.24/5.38 cnf(677,plain, % 5.24/5.38 (P1(a21)), % 5.24/5.38 inference(scs_inference,[],[634,77])). % 5.24/5.38 cnf(678,plain, % 5.24/5.38 (P3(a3,a1,a2)), % 5.24/5.38 inference(scs_inference,[],[634,89])). % 5.24/5.38 cnf(680,plain, % 5.24/5.38 (P10(a35,a2,a21)), % 5.24/5.38 inference(scs_inference,[],[634,91])). % 5.24/5.38 cnf(681,plain, % 5.24/5.38 (P10(a36,a2,a21)), % 5.24/5.38 inference(scs_inference,[],[634,92])). % 5.24/5.38 cnf(682,plain, % 5.24/5.38 (P10(a3,a2,a35)), % 5.24/5.38 inference(scs_inference,[],[634,93])). % 5.24/5.38 cnf(702,plain, % 5.24/5.38 (~P3(x7021,a21,a2)), % 5.24/5.38 inference(scs_inference,[],[634,122])). % 5.24/5.38 cnf(724,plain, % 5.24/5.38 (P10(a35,a2,f9(a35,a35,f9(a35,a35,a35)))), % 5.24/5.38 inference(scs_inference,[],[587,657,651,649,645,68,67,616,69,58,153,487,511,513])). % 5.24/5.38 cnf(726,plain, % 5.24/5.38 (P10(f9(a35,a35,a35),a2,f9(a35,a35,f9(a35,a35,a35)))), % 5.24/5.38 inference(scs_inference,[],[587,657,651,649,645,68,67,616,69,58,153,487,511,513,507])). % 5.24/5.38 cnf(728,plain, % 5.24/5.38 (P1(f9(a35,f9(a35,a35,a35),a35))), % 5.24/5.38 inference(scs_inference,[],[587,657,651,649,645,68,67,616,69,58,153,487,511,513,507,499])). % 5.24/5.38 cnf(730,plain, % 5.24/5.38 (P1(f9(a35,a35,f9(a35,a35,a35)))), % 5.24/5.38 inference(scs_inference,[],[587,657,651,649,645,68,67,616,69,58,153,487,511,513,507,499,501])). % 5.24/5.38 cnf(732,plain, % 5.24/5.38 (P10(a35,a2,f9(a35,f9(a35,a35,a35),a35))), % 5.24/5.38 inference(scs_inference,[],[587,657,651,649,645,68,67,616,69,58,153,487,511,513,507,499,501,509])). % 5.24/5.38 cnf(738,plain, % 5.24/5.38 (~P10(a36,a2,f9(a35,a35,f9(a35,a35,a35)))), % 5.24/5.38 inference(scs_inference,[],[72,587,657,651,649,645,66,68,67,616,69,58,153,487,511,513,507,499,501,509,191,128,170])). % 5.24/5.38 cnf(748,plain, % 5.24/5.38 (~P3(x7481,a21,a2)), % 5.24/5.38 inference(rename_variables,[],[702])). % 5.24/5.38 cnf(792,plain, % 5.24/5.38 ($false), % 5.24/5.38 inference(scs_inference,[],[72,587,738,588,730,728,726,653,732,724,674,677,678,680,681,68,66,67,702,748,682,69,51,170,128,126,56,58,150,173,153,159,160,511,513,499,507,225,509,161,501,190,191,127,167,168]), % 5.24/5.38 ['proof']). % 5.24/5.38 % SZS output end Proof % 5.24/5.38 % Total time :3.440000s %------------------------------------------------------------------------------