%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : LAT391-1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sun Jul 17 05:58:39 EDT 2022
% Result : Unsatisfiable 20.33s 5.39s
% Output : CNFRefutation 20.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : LAT391-1 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.11/0.33 % Computer : n028.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Wed Jun 29 00:30:42 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.11/0.33 21597: Facts:
% 0.11/0.33 21597: Id : 2, {_}:
% 0.11/0.33 mult (plus (mult (plus ?2 ?3) (plus ?3 (mult ?2 ?3))) ?4)
% 0.11/0.33 (plus
% 0.11/0.33 (mult (plus ?2 (mult (mult (plus ?5 ?3) (plus ?3 ?6)) ?3))
% 0.11/0.33 (plus
% 0.11/0.33 (mult
% 0.11/0.33 (plus ?3
% 0.11/0.33 (plus (plus (mult ?5 (mult ?3 ?6)) (mult ?7 ?3)) ?3))
% 0.11/0.33 (plus ?8
% 0.11/0.33 (mult ?3 (plus (plus (mult ?3 ?9) (mult ?7 ?3)) ?3))))
% 0.11/0.33 (mult ?2 (mult (mult (plus ?5 ?3) (plus ?3 ?6)) ?3))))
% 0.11/0.33 (mult (mult (plus ?2 ?3) (plus ?3 (mult ?2 ?3))) ?4))
% 0.11/0.33 =>=
% 0.11/0.33 ?3
% 0.11/0.33 [9, 8, 7, 6, 5, 4, 3, 2] by sos ?2 ?3 ?4 ?5 ?6 ?7 ?8 ?9
% 0.11/0.33 21597: Goal:
% 0.11/0.33 21597: Id : 1, {_}: mult (mult (plus a b) (plus b c)) b =>= b [] by goals
% 20.33/5.39 Statistics :
% 20.33/5.39 Max weight : 3542
% 20.33/5.39 Found proof, 5.061175s
% 20.33/5.39 % SZS status Unsatisfiable for theBenchmark.p
% 20.33/5.39 % SZS output start CNFRefutation for theBenchmark.p
% 20.33/5.39 Id : 3, {_}: mult (plus (mult (plus ?11 ?12) (plus ?12 (mult ?11 ?12))) ?13) (plus (mult (plus ?11 (mult (mult (plus ?14 ?12) (plus ?12 ?15)) ?12)) (plus (mult (plus ?12 (plus (plus (mult ?14 (mult ?12 ?15)) (mult ?16 ?12)) ?12)) (plus ?17 (mult ?12 (plus (plus (mult ?12 ?18) (mult ?16 ?12)) ?12)))) (mult ?11 (mult (mult (plus ?14 ?12) (plus ?12 ?15)) ?12)))) (mult (mult (plus ?11 ?12) (plus ?12 (mult ?11 ?12))) ?13)) =>= ?12 [18, 17, 16, 15, 14, 13, 12, 11] by sos ?11 ?12 ?13 ?14 ?15 ?16 ?17 ?18
% 20.33/5.39 Id : 2, {_}: mult (plus (mult (plus ?2 ?3) (plus ?3 (mult ?2 ?3))) ?4) (plus (mult (plus ?2 (mult (mult (plus ?5 ?3) (plus ?3 ?6)) ?3)) (plus (mult (plus ?3 (plus (plus (mult ?5 (mult ?3 ?6)) (mult ?7 ?3)) ?3)) (plus ?8 (mult ?3 (plus (plus (mult ?3 ?9) (mult ?7 ?3)) ?3)))) (mult ?2 (mult (mult (plus ?5 ?3) (plus ?3 ?6)) ?3)))) (mult (mult (plus ?2 ?3) (plus ?3 (mult ?2 ?3))) ?4)) =>= ?3 [9, 8, 7, 6, 5, 4, 3, 2] by sos ?2 ?3 ?4 ?5 ?6 ?7 ?8 ?9
% 20.33/5.39 Id : 11, {_}: mult (plus (mult (plus ?117 (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119)))) (plus (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119))) (mult ?117 (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119)))))) ?120) (plus (mult (plus ?117 (mult (mult (plus (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119))) (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119)))) (plus (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119))) ?121)) (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119))))) (plus ?119 (mult ?117 (mult (mult (plus (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119))) (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119)))) (plus (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119))) ?121)) (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119))))))) (mult (mult (plus ?117 (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119)))) (plus (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119))) (mult ?117 (mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119)))))) ?120)) =>= mult (plus ?118 ?119) (plus ?119 (mult ?118 ?119)) [121, 120, 119, 118, 117] by Super 3 with 2 at 1,2,1,2,2
% 20.33/5.39 Id : 35, {_}: mult (plus (mult (plus ?287 (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289)))) (plus (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289))) (mult ?287 (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289)))))) ?290) (plus (mult (plus ?287 (mult (mult (plus (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289))) (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289)))) (plus (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289))) ?291)) (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289))))) (plus ?289 (mult ?287 (mult (mult (plus (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289))) (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289)))) (plus (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289))) ?291)) (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289))))))) (mult (mult (plus ?287 (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289)))) (plus (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289))) (mult ?287 (mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289)))))) ?290)) =>= mult (plus ?288 ?289) (plus ?289 (mult ?288 ?289)) [291, 290, 289, 288, 287] by Super 3 with 2 at 1,2,1,2,2
% 20.33/5.40 Id : 38, {_}: mult (plus (mult (plus ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))))) ?322) (plus (mult (plus ?314 (mult (mult (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))))) (mult (mult (plus ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 ?316))) ?322)) =>= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [323, 322, 321, 320, 319, 318, 317, 316, 315, 314] by Super 35 with 2 at 2,2,2,1,2,2,2
% 20.33/5.41 Id : 132, {_}: mult (plus (mult (plus ?314 ?316) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))))) ?322) (plus (mult (plus ?314 (mult (mult (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))))) (mult (mult (plus ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 ?316))) ?322)) =>= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [323, 322, 321, 320, 319, 318, 317, 315, 316, 314] by Demod 38 with 2 at 2,1,1,1,2
% 20.33/5.41 Id : 133, {_}: mult (plus (mult (plus ?314 ?316) (plus ?316 (mult ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))))) ?322) (plus (mult (plus ?314 (mult (mult (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))))) (mult (mult (plus ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 ?316))) ?322)) =>= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [323, 322, 321, 320, 319, 318, 317, 315, 316, 314] by Demod 132 with 2 at 1,2,1,1,2
% 20.33/5.42 Id : 134, {_}: mult (plus (mult (plus ?314 ?316) (plus ?316 (mult ?314 ?316))) ?322) (plus (mult (plus ?314 (mult (mult (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))))) (mult (mult (plus ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 ?316))) ?322)) =>= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [323, 321, 320, 319, 318, 317, 315, 322, 316, 314] by Demod 133 with 2 at 2,2,2,1,1,2
% 20.33/5.43 Id : 135, {_}: mult (plus (mult (plus ?314 ?316) (plus ?316 (mult ?314 ?316))) ?322) (plus (mult (plus ?314 (mult (mult (plus ?316 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))))) (mult (mult (plus ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 ?316))) ?322)) =>= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [323, 321, 320, 319, 318, 317, 315, 322, 316, 314] by Demod 134 with 2 at 1,1,1,2,1,1,2,2
% 20.33/5.43 Id : 136, {_}: mult (plus (mult (plus ?314 ?316) (plus ?316 (mult ?314 ?316))) ?322) (plus (mult (plus ?314 (mult (mult (plus ?316 ?316) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))))) (mult (mult (plus ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 ?316))) ?322)) =>= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [323, 321, 320, 319, 318, 317, 315, 322, 316, 314] by Demod 135 with 2 at 2,1,1,2,1,1,2,2
% 20.33/5.44 Id : 137, {_}: mult (plus (mult (plus ?314 ?316) (plus ?316 (mult ?314 ?316))) ?322) (plus (mult (plus ?314 (mult (mult (plus ?316 ?316) (plus ?316 ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))))) (mult (mult (plus ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 ?316))) ?322)) =>= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [321, 320, 319, 318, 317, 315, 323, 322, 316, 314] by Demod 136 with 2 at 1,2,1,2,1,1,2,2
% 20.33/5.44 Id : 138, {_}: mult (plus (mult (plus ?314 ?316) (plus ?316 (mult ?314 ?316))) ?322) (plus (mult (plus ?314 (mult (mult (plus ?316 ?316) (plus ?316 ?323)) ?316)) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))))) (mult (mult (plus ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 ?316))) ?322)) =>= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [321, 320, 319, 318, 317, 315, 323, 322, 316, 314] by Demod 137 with 2 at 2,2,1,1,2,2
% 20.33/5.44 Id : 139, {_}: mult (plus (mult (plus ?314 ?316) (plus ?316 (mult ?314 ?316))) ?322) (plus (mult (plus ?314 (mult (mult (plus ?316 ?316) (plus ?316 ?323)) ?316)) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus ?316 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))))) (mult (mult (plus ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 ?316))) ?322)) =>= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [321, 320, 319, 318, 317, 315, 323, 322, 316, 314] by Demod 138 with 2 at 1,1,1,2,2,2,1,2,2
% 20.33/5.45 Id : 140, {_}: mult (plus (mult (plus ?314 ?316) (plus ?316 (mult ?314 ?316))) ?322) (plus (mult (plus ?314 (mult (mult (plus ?316 ?316) (plus ?316 ?323)) ?316)) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus ?316 ?316) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))))) (mult (mult (plus ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 ?316))) ?322)) =>= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [321, 320, 319, 318, 317, 315, 323, 322, 316, 314] by Demod 139 with 2 at 2,1,1,2,2,2,1,2,2
% 20.33/5.45 Id : 141, {_}: mult (plus (mult (plus ?314 ?316) (plus ?316 (mult ?314 ?316))) ?322) (plus (mult (plus ?314 (mult (mult (plus ?316 ?316) (plus ?316 ?323)) ?316)) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus ?316 ?316) (plus ?316 ?323)) (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))))))) (mult (mult (plus ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 ?316))) ?322)) =>= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [321, 320, 319, 318, 317, 315, 323, 322, 316, 314] by Demod 140 with 2 at 1,2,1,2,2,2,1,2,2
% 20.33/5.45 Id : 142, {_}: mult (plus (mult (plus ?314 ?316) (plus ?316 (mult ?314 ?316))) ?322) (plus (mult (plus ?314 (mult (mult (plus ?316 ?316) (plus ?316 ?323)) ?316)) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus ?316 ?316) (plus ?316 ?323)) ?316)))) (mult (mult (plus ?314 (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))))) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 ?316))) ?322)) =>= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [321, 320, 319, 318, 317, 315, 323, 322, 316, 314] by Demod 141 with 2 at 2,2,2,2,1,2,2
% 20.33/5.45 Id : 143, {_}: mult (plus (mult (plus ?314 ?316) (plus ?316 (mult ?314 ?316))) ?322) (plus (mult (plus ?314 (mult (mult (plus ?316 ?316) (plus ?316 ?323)) ?316)) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus ?316 ?316) (plus ?316 ?323)) ?316)))) (mult (mult (plus ?314 ?316) (plus (mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))))) (mult ?314 ?316))) ?322)) =>= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [321, 320, 319, 318, 317, 315, 323, 322, 316, 314] by Demod 142 with 2 at 2,1,1,2,2,2
% 20.33/5.45 Id : 144, {_}: mult (plus (mult (plus ?314 ?316) (plus ?316 (mult ?314 ?316))) ?322) (plus (mult (plus ?314 (mult (mult (plus ?316 ?316) (plus ?316 ?323)) ?316)) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult ?314 (mult (mult (plus ?316 ?316) (plus ?316 ?323)) ?316)))) (mult (mult (plus ?314 ?316) (plus ?316 (mult ?314 ?316))) ?322)) =?= mult (plus (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316))))) (plus (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))) (mult (mult (plus ?315 ?316) (plus ?316 (mult ?315 ?316))) (mult (plus ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)) (plus (mult (plus ?316 (plus (plus (mult ?317 (mult ?316 ?318)) (mult ?319 ?316)) ?316)) (plus ?320 (mult ?316 (plus (plus (mult ?316 ?321) (mult ?319 ?316)) ?316)))) (mult ?315 (mult (mult (plus ?317 ?316) (plus ?316 ?318)) ?316)))))) [321, 320, 319, 318, 317, 315, 323, 322, 316, 314] by Demod 143 with 2 at 1,2,1,2,2,2
% 20.33/5.45 Id : 928, {_}: mult (plus (mult (plus ?1426 ?1427) (plus ?1427 (mult ?1426 ?1427))) ?1428) (plus (mult (plus ?1426 (mult (mult (plus ?1427 ?1427) (plus ?1427 ?1429)) ?1427)) (plus (mult (plus ?1430 (mult (mult (plus ?1431 ?1427) (plus ?1427 ?1432)) ?1427)) (plus (mult (plus ?1427 (plus (plus (mult ?1431 (mult ?1427 ?1432)) (mult ?1433 ?1427)) ?1427)) (plus ?1434 (mult ?1427 (plus (plus (mult ?1427 ?1435) (mult ?1433 ?1427)) ?1427)))) (mult ?1430 (mult (mult (plus ?1431 ?1427) (plus ?1427 ?1432)) ?1427)))) (mult ?1426 (mult (mult (plus ?1427 ?1427) (plus ?1427 ?1429)) ?1427)))) (mult (mult (plus ?1426 ?1427) (plus ?1427 (mult ?1426 ?1427))) ?1428)) =>= ?1427 [1435, 1434, 1433, 1432, 1431, 1430, 1429, 1428, 1427, 1426] by Demod 144 with 2 at 3
% 20.33/5.45 Id : 956, {_}: mult (plus (mult (plus (mult (plus ?1834 ?1835) (plus ?1835 (mult ?1834 ?1835))) ?1835) (plus ?1835 (mult (mult (plus ?1834 ?1835) (plus ?1835 (mult ?1834 ?1835))) ?1835))) ?1836) (plus ?1835 (mult (mult (plus (mult (plus ?1834 ?1835) (plus ?1835 (mult ?1834 ?1835))) ?1835) (plus ?1835 (mult (mult (plus ?1834 ?1835) (plus ?1835 (mult ?1834 ?1835))) ?1835))) ?1836)) =>= ?1835 [1836, 1835, 1834] by Super 928 with 2 at 1,2,2
% 20.61/5.46 Id : 1390, {_}: mult (plus (mult (plus ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))) (plus ?1946 (mult ?1944 (mult (mult (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))))) (mult (mult (plus ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 ?1946))) ?1947)) =>= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1948, 1947, 1946, 1945, 1944] by Super 11 with 956 at 2,2,2,1,2,2,2
% 20.61/5.46 Id : 1512, {_}: mult (plus (mult (plus ?1944 ?1946) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))) (plus ?1946 (mult ?1944 (mult (mult (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))))) (mult (mult (plus ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 ?1946))) ?1947)) =>= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1948, 1947, 1945, 1946, 1944] by Demod 1390 with 956 at 2,1,1,1,2
% 20.61/5.46 Id : 1513, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))) (plus ?1946 (mult ?1944 (mult (mult (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))))) (mult (mult (plus ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 ?1946))) ?1947)) =>= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1948, 1947, 1945, 1946, 1944] by Demod 1512 with 956 at 1,2,1,1,2
% 20.61/5.46 Id : 1514, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))) (plus ?1946 (mult ?1944 (mult (mult (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))))) (mult (mult (plus ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 ?1946))) ?1947)) =>= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1948, 1945, 1947, 1946, 1944] by Demod 1513 with 956 at 2,2,2,1,1,2
% 20.61/5.47 Id : 1515, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus ?1946 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))) (plus ?1946 (mult ?1944 (mult (mult (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))))) (mult (mult (plus ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 ?1946))) ?1947)) =>= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1948, 1945, 1947, 1946, 1944] by Demod 1514 with 956 at 1,1,1,2,1,1,2,2
% 20.66/5.47 Id : 1516, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus ?1946 ?1946) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))) (plus ?1946 (mult ?1944 (mult (mult (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))))) (mult (mult (plus ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 ?1946))) ?1947)) =>= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1948, 1945, 1947, 1946, 1944] by Demod 1515 with 956 at 2,1,1,2,1,1,2,2
% 20.66/5.47 Id : 1517, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))) (plus ?1946 (mult ?1944 (mult (mult (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))))) (mult (mult (plus ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 ?1946))) ?1947)) =>= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1945, 1948, 1947, 1946, 1944] by Demod 1516 with 956 at 1,2,1,2,1,1,2,2
% 20.66/5.47 Id : 1518, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) ?1946)) (plus ?1946 (mult ?1944 (mult (mult (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))))) (mult (mult (plus ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 ?1946))) ?1947)) =>= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1945, 1948, 1947, 1946, 1944] by Demod 1517 with 956 at 2,2,1,1,2,2
% 20.66/5.47 Id : 1519, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) ?1946)) (plus ?1946 (mult ?1944 (mult (mult (plus ?1946 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))))) (mult (mult (plus ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 ?1946))) ?1947)) =>= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1945, 1948, 1947, 1946, 1944] by Demod 1518 with 956 at 1,1,1,2,2,2,1,2,2
% 20.66/5.47 Id : 1520, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) ?1946)) (plus ?1946 (mult ?1944 (mult (mult (plus ?1946 ?1946) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))))) (mult (mult (plus ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 ?1946))) ?1947)) =>= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1945, 1948, 1947, 1946, 1944] by Demod 1519 with 956 at 2,1,1,2,2,2,1,2,2
% 20.66/5.47 Id : 1521, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) ?1946)) (plus ?1946 (mult ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))))))) (mult (mult (plus ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 ?1946))) ?1947)) =>= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1945, 1948, 1947, 1946, 1944] by Demod 1520 with 956 at 1,2,1,2,2,2,1,2,2
% 20.66/5.47 Id : 1522, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) ?1946)) (plus ?1946 (mult ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) ?1946)))) (mult (mult (plus ?1944 (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)))) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 ?1946))) ?1947)) =>= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1945, 1948, 1947, 1946, 1944] by Demod 1521 with 956 at 2,2,2,2,1,2,2
% 20.66/5.47 Id : 1523, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) ?1946)) (plus ?1946 (mult ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) ?1946)))) (mult (mult (plus ?1944 ?1946) (plus (mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946))) (mult ?1944 ?1946))) ?1947)) =>= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1945, 1948, 1947, 1946, 1944] by Demod 1522 with 956 at 2,1,1,2,2,2
% 20.66/5.48 Id : 1524, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) ?1946)) (plus ?1946 (mult ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) ?1946)))) (mult (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947)) =?= mult (plus (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946) (plus ?1946 (mult (mult (plus (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946) (plus ?1946 (mult (mult (plus ?1945 ?1946) (plus ?1946 (mult ?1945 ?1946))) ?1946))) ?1946)) [1945, 1948, 1947, 1946, 1944] by Demod 1523 with 956 at 1,2,1,2,2,2
% 20.66/5.48 Id : 3131, {_}: mult (plus (mult (plus ?4243 ?4244) (plus ?4244 (mult ?4243 ?4244))) ?4245) (plus (mult (plus ?4243 (mult (mult (plus ?4244 ?4244) (plus ?4244 ?4246)) ?4244)) (plus ?4244 (mult ?4243 (mult (mult (plus ?4244 ?4244) (plus ?4244 ?4246)) ?4244)))) (mult (mult (plus ?4243 ?4244) (plus ?4244 (mult ?4243 ?4244))) ?4245)) =>= ?4244 [4246, 4245, 4244, 4243] by Demod 1524 with 956 at 3
% 20.66/5.48 Id : 1525, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947) (plus (mult (plus ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) ?1946)) (plus ?1946 (mult ?1944 (mult (mult (plus ?1946 ?1946) (plus ?1946 ?1948)) ?1946)))) (mult (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947)) =>= ?1946 [1948, 1947, 1946, 1944] by Demod 1524 with 956 at 3
% 20.66/5.48 Id : 3144, {_}: mult (plus (mult (plus (mult (plus ?4342 ?4343) (plus ?4343 (mult ?4342 ?4343))) (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343))))) (plus (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))) (mult (mult (plus ?4342 ?4343) (plus ?4343 (mult ?4342 ?4343))) (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343))))))) ?4345) (plus (mult (plus (mult (plus ?4342 ?4343) (plus ?4343 (mult ?4342 ?4343))) (mult (mult (plus (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))) (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343))))) (plus (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))) ?4346)) (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))))) (plus (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))) (mult (mult (plus ?4342 ?4343) (plus ?4343 (mult ?4342 ?4343))) (mult (mult (plus (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))) (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343))))) (plus (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))) ?4346)) (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))))))) (mult ?4343 ?4345)) =>= mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343))) [4346, 4345, 4344, 4343, 4342] by Super 3131 with 1525 at 1,2,2,2
% 20.66/5.48 Id : 3626, {_}: mult (plus ?4343 ?4345) (plus (mult (plus (mult (plus ?4342 ?4343) (plus ?4343 (mult ?4342 ?4343))) (mult (mult (plus (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))) (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343))))) (plus (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))) ?4346)) (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))))) (plus (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))) (mult (mult (plus ?4342 ?4343) (plus ?4343 (mult ?4342 ?4343))) (mult (mult (plus (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))) (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343))))) (plus (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))) ?4346)) (mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)))))))) (mult ?4343 ?4345)) =>= mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343))) [4346, 4344, 4342, 4345, 4343] by Demod 3144 with 1525 at 1,1,2
% 20.66/5.48 Id : 3627, {_}: mult (plus ?4343 ?4345) (plus ?4343 (mult ?4343 ?4345)) =?= mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343))) [4344, 4342, 4345, 4343] by Demod 3626 with 1525 at 1,2,2
% 20.66/5.48 Id : 1445, {_}: mult (plus (mult (plus (mult (plus ?2387 ?2388) (plus ?2388 (mult ?2387 ?2388))) ?2388) (plus ?2388 (mult (mult (plus ?2387 ?2388) (plus ?2388 (mult ?2387 ?2388))) ?2388))) ?2389) (plus ?2388 (mult (mult (plus (mult (plus ?2387 ?2388) (plus ?2388 (mult ?2387 ?2388))) ?2388) (plus ?2388 (mult (mult (plus ?2387 ?2388) (plus ?2388 (mult ?2387 ?2388))) ?2388))) ?2389)) =>= ?2388 [2389, 2388, 2387] by Super 928 with 2 at 1,2,2
% 20.66/5.48 Id : 1462, {_}: mult (plus (mult (plus (mult (plus (mult (plus ?2519 ?2520) (plus ?2520 (mult ?2519 ?2520))) ?2520) (plus ?2520 (mult (mult (plus ?2519 ?2520) (plus ?2520 (mult ?2519 ?2520))) ?2520))) ?2520) (plus ?2520 (mult (mult (plus (mult (plus ?2519 ?2520) (plus ?2520 (mult ?2519 ?2520))) ?2520) (plus ?2520 (mult (mult (plus ?2519 ?2520) (plus ?2520 (mult ?2519 ?2520))) ?2520))) ?2520))) ?2521) (plus ?2520 (mult ?2520 ?2521)) =>= ?2520 [2521, 2520, 2519] by Super 1445 with 956 at 1,2,2,2
% 20.66/5.48 Id : 1938, {_}: mult (plus ?2520 ?2521) (plus ?2520 (mult ?2520 ?2521)) =>= ?2520 [2521, 2520] by Demod 1462 with 956 at 1,1,2
% 20.66/5.48 Id : 3628, {_}: ?4343 =<= mult (plus ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343)) (plus ?4343 (mult ?4342 (mult (mult (plus ?4343 ?4343) (plus ?4343 ?4344)) ?4343))) [4344, 4342, 4343] by Demod 3627 with 1938 at 2
% 20.66/5.48 Id : 3703, {_}: mult (plus ?4683 (mult (mult (plus ?4684 ?4685) (plus ?4685 ?4686)) ?4685)) (plus (mult (plus ?4685 (plus (plus (mult ?4684 (mult ?4685 ?4686)) (mult ?4687 ?4685)) ?4685)) (plus ?4688 (mult ?4685 (plus (plus (mult ?4685 ?4689) (mult ?4687 ?4685)) ?4685)))) (mult ?4683 (mult (mult (plus ?4684 ?4685) (plus ?4685 ?4686)) ?4685))) =>= ?4685 [4689, 4688, 4687, 4686, 4685, 4684, 4683] by Super 2 with 3628 at 2
% 20.66/5.48 Id : 3676, {_}: mult (plus (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947) (plus ?1946 (mult (mult (plus ?1944 ?1946) (plus ?1946 (mult ?1944 ?1946))) ?1947)) =>= ?1946 [1947, 1946, 1944] by Demod 1525 with 3628 at 1,2,2
% 20.66/5.48 Id : 4725, {_}: ?5591 =<= mult (plus ?5591 (plus (plus (mult ?5592 (mult ?5591 ?5593)) (mult ?5594 ?5591)) ?5591)) (plus ?5595 (mult ?5591 (plus (plus (mult ?5591 ?5596) (mult ?5594 ?5591)) ?5591))) [5596, 5595, 5594, 5593, 5592, 5591] by Super 3676 with 3703 at 2
% 20.66/5.48 Id : 5027, {_}: mult (plus ?4683 (mult (mult (plus ?4684 ?4685) (plus ?4685 ?4686)) ?4685)) (plus ?4685 (mult ?4683 (mult (mult (plus ?4684 ?4685) (plus ?4685 ?4686)) ?4685))) =>= ?4685 [4686, 4685, 4684, 4683] by Demod 3703 with 4725 at 1,2,2
% 20.66/5.48 Id : 5035, {_}: mult (plus ?6274 ?6275) (plus ?6275 (mult ?6274 ?6275)) =>= ?6275 [6275, 6274] by Super 3676 with 4725 at 2
% 20.66/5.48 Id : 5569, {_}: ?6944 =<= plus (plus (mult ?6944 (mult ?6944 ?6945)) (mult ?6946 ?6944)) ?6944 [6946, 6945, 6944] by Super 4725 with 5035 at 3
% 20.66/5.48 Id : 6808, {_}: ?9146 =<= mult (plus ?9146 ?9146) (plus ?9147 (mult ?9146 (plus (plus (mult ?9146 ?9148) (mult ?9149 ?9146)) ?9146))) [9149, 9148, 9147, 9146] by Super 4725 with 5569 at 2,1,3
% 20.66/5.48 Id : 6837, {_}: ?9301 =<= mult (plus ?9301 ?9301) (plus ?9302 (mult ?9301 ?9301)) [9302, 9301] by Super 6808 with 5569 at 2,2,2,3
% 20.66/5.48 Id : 5563, {_}: mult (plus ?6908 (mult (mult (plus ?6909 ?6910) (plus ?6910 (mult ?6909 ?6910))) ?6910)) (plus ?6910 (mult ?6908 (mult ?6910 ?6910))) =>= ?6910 [6910, 6909, 6908] by Super 5027 with 5035 at 1,2,2,2,2
% 20.66/5.48 Id : 5585, {_}: mult (plus ?6908 (mult ?6910 ?6910)) (plus ?6910 (mult ?6908 (mult ?6910 ?6910))) =>= ?6910 [6910, 6908] by Demod 5563 with 5035 at 1,2,1,2
% 20.66/5.48 Id : 6883, {_}: mult ?9353 ?9353 =>= ?9353 [9353] by Super 5585 with 6837 at 2
% 20.66/5.48 Id : 6952, {_}: ?9301 =<= mult (plus ?9301 ?9301) (plus ?9302 ?9301) [9302, 9301] by Demod 6837 with 6883 at 2,2,3
% 20.66/5.48 Id : 6972, {_}: ?9477 =<= plus ?9477 ?9477 [9477] by Super 6952 with 6883 at 3
% 20.66/5.48 Id : 7092, {_}: mult (mult (mult (plus ?9654 ?9655) (plus ?9655 ?9656)) ?9655) (plus ?9655 (mult (mult (mult (plus ?9654 ?9655) (plus ?9655 ?9656)) ?9655) (mult (mult (plus ?9654 ?9655) (plus ?9655 ?9656)) ?9655))) =>= ?9655 [9656, 9655, 9654] by Super 5027 with 6972 at 1,2
% 20.66/5.48 Id : 7201, {_}: mult (mult (mult (plus ?9654 ?9655) (plus ?9655 ?9656)) ?9655) (plus ?9655 (mult (mult (plus ?9654 ?9655) (plus ?9655 ?9656)) ?9655)) =>= ?9655 [9656, 9655, 9654] by Demod 7092 with 6883 at 2,2,2
% 20.66/5.48 Id : 7058, {_}: ?9301 =<= mult ?9301 (plus ?9302 ?9301) [9302, 9301] by Demod 6952 with 6972 at 1,3
% 20.66/5.48 Id : 7202, {_}: mult (mult (plus ?9654 ?9655) (plus ?9655 ?9656)) ?9655 =>= ?9655 [9656, 9655, 9654] by Demod 7201 with 7058 at 2
% 20.66/5.48 Id : 7607, {_}: b === b [] by Demod 1 with 7202 at 2
% 20.66/5.48 Id : 1, {_}: mult (mult (plus a b) (plus b c)) b =>= b [] by goals
% 20.66/5.48 % SZS output end CNFRefutation for theBenchmark.p
% 20.66/5.48 21600: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 5.150555 using nrkbo
%------------------------------------------------------------------------------