WATCH: 0.00 CPU 0.01 WC WATCH: 2.87 CPU 3.02 WC # Preprocessing time : 0.300 s # Problem is unsatisfiable (or provable), constructing proof object # SZS status Theorem # SZS output start CNFRefutation. fof(8031, axiom,![X1]:![X2]:![X3]:(?[X4]:?[X5]:?[X6]:(((((((arg1(X5,X2)&hsit(X1,X4))&obj(X4,X2))&sub(X6,X3))&subr(X5,rprs_0))&subs(X4,bezeichnen_1_1))&mcont(X4,X5))&arg2(X5,X6))<=((subr(X1,sub_0)&arg2(X1,X3))&arg1(X1,X2))),file('/CW/home-0/sutcliff/TPTP/Axioms/CSR004+0.ax', sub__bezeichnen_1_1_als)). fof(8465, axiom,![X1]:![X2]:(?[X3]:((arg2(X3,X2)&subr(X3,sub_0))&arg1(X3,X1))<=sub(X1,X2)),file('/CW/home-0/sutcliff/TPTP/Axioms/CSR004+0.ax', sub__sub_0_expansion)). fof(10188, conjecture,?[X1]:?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:((((((((attr(X4,X3)&attr(X6,X7))&sub(X2,name_1_1))&sub(X1,firma_1_1))&sub(X3,name_1_1))&val(X3,bmw_0))&val(X2,bmw_0))&obj(X5,X1))&attr(X1,X2)),file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE084.p', synth_qa07_007_mn3_277)). fof(10189, axiom,((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((attr(c8713,c8714)&sub(c8724,mensch_1_1))&val(c8725,raichle_0))&subs(c8740,absatz_1_2))&pred(c8743,dynafit_1_1))&sub(c8775,name_1_1))&val(c8775,bmw_0))&attr(c8778,c8779))&tupl_p12(c9098,c8713,c8719,c8724,c8733,c8740,c8743,c8740,c8755,c8761,c8774,c8778))&assoc(produktemanagement_1_1,erzeugnis_1_1))&sort(c8713,d))&card(c8713,int1))&fact(c8713,real))&refer(c8713,det))&card(c8714,int1))&gener(c8714,sp))&quant(c8714,one))&varia(c8714,varia_c))&varia(mensch_1_1,varia_c))&gener(familiename_1_1,ge))&quant(familiename_1_1,one))&refer(familiename_1_1,refer_c))&sort(c8719,d))&sort(c8719,io))&etype(c8719,int0))&fact(c8719,real))&gener(c8719,sp))&quant(c8719,one))&refer(c8719,det))&varia(c8719,con))&sort(firma_1_1,d))&etype(firma_1_1,int0))&gener(firma_1_1,ge))&quant(firma_1_1,one))&refer(firma_1_1,refer_c))&varia(firma_1_1,varia_c))&sort(c8724,d))&card(c8724,int1))&etype(c8724,int0))&sort(c8725,na))&card(c8725,int1))&gener(c8725,sp))&quant(c8725,one))&refer(c8725,indet))&sort(raichle_0,fe))&sort(c8733,d))&sort(c8733,io))&card(c8733,int1))&etype(c8733,int0))&gener(c8733,sp))&quant(c8733,one))&varia(c8733,con))&sort(produktemanagement_1_1,io))&fact(produktemanagement_1_1,real))&varia(produktemanagement_1_1,varia_c))&sort(c8740,ad))&card(c8740,int1))&etype(c8740,int0))&fact(c8740,real))&quant(c8740,one))&varia(c8740,con))&sort(absatz_1_2,ad))&card(absatz_1_2,int1))&fact(absatz_1_2,real))&refer(absatz_1_2,refer_c))&varia(absatz_1_2,varia_c))&card(c8743,cons(x_constant,cons(int1,nil))))&gener(c8743,gener_c))&refer(c8743,indet))&varia(c8743,varia_c))&sort(dynafit_1_1,o))&etype(dynafit_1_1,int0))&gener(dynafit_1_1,ge))&quant(dynafit_1_1,one))&refer(dynafit_1_1,refer_c))&sort(c8755,io))&gener(c8755,gener_c))&quant(c8755,one))&refer(c8755,refer_c))&varia(c8755,varia_c))&card(absatzf__366rderung_1_1,int1))&etype(absatzf__366rderung_1_1,int0))&quant(absatzf__366rderung_1_1,one))&refer(absatzf__366rderung_1_1,refer_c))&varia(absatzf__366rderung_1_1,varia_c))&card(c8761,cons(x_constant,cons(int1,nil))))&fact(c8761,real))&refer(c8761,indet))&sort(leiter_1_1,d))&card(leiter_1_1,int1))&gener(leiter_1_1,ge))&refer(leiter_1_1,refer_c))&varia(leiter_1_1,varia_c))&sort(c8774,d))&etype(c8774,int0))&gener(c8774,sp))&quant(c8774,one))&varia(c8774,con))&sort(c8775,na))&fact(c8775,real))&gener(c8775,sp))&quant(c8775,one))&sort(name_1_1,na))&card(name_1_1,int1))&fact(name_1_1,real))&quant(name_1_1,one))&varia(name_1_1,varia_c))&sort(bmw_0,fe))&card(c8778,int1))&gener(c8778,sp))&quant(c8778,one))&etype(c8779,int0))&fact(c8779,real))&refer(c8779,indet))&card(land_1_1,int1))&gener(land_1_1,ge))&quant(land_1_1,one))&sort(c9098,ent))&gener(c9098,gener_c))&quant(c9098,quant_c))&refer(c9098,refer_c))&etype(erzeugnis_1_1,etype_c))&fact(erzeugnis_1_1,real))&refer(erzeugnis_1_1,refer_c))&sort(management__1_1,d))&sort(management__1_1,io))&card(management__1_1,int1))&quant(management__1_1,one))&refer(management__1_1,refer_c))&varia(management__1_1,varia_c))&gener(management__1_1,ge))&fact(management__1_1,real))&etype(management__1_1,int0))&varia(erzeugnis_1_1,varia_c))&quant(erzeugnis_1_1,quant_c))&gener(erzeugnis_1_1,ge))&card(erzeugnis_1_1,card_c))&sort(erzeugnis_1_1,co))&varia(c9098,varia_c))&fact(c9098,real))&etype(c9098,etype_c))&card(c9098,card_c))&sort(schweiz_0,fe))&varia(land_1_1,varia_c))&refer(land_1_1,refer_c))&fact(land_1_1,real))&etype(land_1_1,int0))&sort(land_1_1,io))&sort(land_1_1,d))&varia(c8779,varia_c))&quant(c8779,one))&gener(c8779,sp))&card(c8779,int1))&sort(c8779,na))&varia(c8778,con))&refer(c8778,det))&fact(c8778,real))&etype(c8778,int0))&sort(c8778,io))&sort(c8778,d))&refer(name_1_1,refer_c))&gener(name_1_1,ge))&etype(name_1_1,int0))&varia(c8775,varia_c))&refer(c8775,indet))&etype(c8775,int0))&card(c8775,int1))&refer(c8774,det))&fact(c8774,real))&card(c8774,int1))&sort(c8774,io))&quant(leiter_1_1,one))&fact(leiter_1_1,real))&etype(leiter_1_1,int0))&varia(c8761,varia_c))&quant(c8761,mult))&gener(c8761,gener_c))&etype(c8761,int1))&sort(c8761,d))&gener(absatzf__366rderung_1_1,ge))&fact(absatzf__366rderung_1_1,real))&sort(absatzf__366rderung_1_1,io))&fact(c8755,real))&etype(c8755,int0))&card(c8755,int1))&varia(dynafit_1_1,varia_c))&fact(dynafit_1_1,real))&card(dynafit_1_1,int1))&quant(c8743,mult))&fact(c8743,real))&etype(c8743,int1))&sort(c8743,o))&quant(absatz_1_2,one))&gener(absatz_1_2,ge))&etype(absatz_1_2,int0))&sort(erdweit_1_1,tq))&refer(c8740,det))&gener(c8740,sp))&refer(produktemanagement_1_1,refer_c))&quant(produktemanagement_1_1,one))&gener(produktemanagement_1_1,ge))&etype(produktemanagement_1_1,int0))&card(produktemanagement_1_1,int1))&sort(produktemanagement_1_1,d))&refer(c8733,det))&fact(c8733,real))&varia(c8725,varia_c))&fact(c8725,real))&etype(c8725,int0))&varia(c8724,con))&refer(c8724,det))&quant(c8724,one))&gener(c8724,sp))&fact(c8724,real))&fact(firma_1_1,real))&card(firma_1_1,int1))&sort(firma_1_1,io))&card(c8719,int1))&sort(wellauer_0,fe))&varia(familiename_1_1,varia_c))&fact(familiename_1_1,real))&etype(familiename_1_1,int0))&card(familiename_1_1,int1))&sort(familiename_1_1,na))&refer(mensch_1_1,refer_c))&quant(mensch_1_1,one))&gener(mensch_1_1,ge))&fact(mensch_1_1,real))&etype(mensch_1_1,int0))&card(mensch_1_1,int1))&sort(mensch_1_1,d))&refer(c8714,indet))&fact(c8714,real))&etype(c8714,int0))&sort(c8714,na))&varia(c8713,con))&quant(c8713,one))&gener(c8713,sp))&etype(c8713,int0))&sub(produktemanagement_1_1,management__1_1))&val(c8779,schweiz_0))&sub(c8779,name_1_1))&sub(c8778,land_1_1))&sub(c8774,firma_1_1))&attr(c8774,c8775))&pred(c8761,leiter_1_1))&sub(c8755,absatzf__366rderung_1_1))&prop(c8740,erdweit_1_1))&sub(c8733,produktemanagement_1_1))&sub(c8725,familiename_1_1))&attr(c8724,c8725))&sub(c8719,firma_1_1))&val(c8714,wellauer_0))&sub(c8714,familiename_1_1))&sub(c8713,mensch_1_1)),file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE084.p', ave07_era5_synth_qa07_007_mn3_277)). fof(10190, negated_conjecture,~(?[X1]:?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:((((((((attr(X4,X3)&attr(X6,X7))&sub(X2,name_1_1))&sub(X1,firma_1_1))&sub(X3,name_1_1))&val(X3,bmw_0))&val(X2,bmw_0))&obj(X5,X1))&attr(X1,X2))),inference(assume_negation,[status(cth)],[10188])). fof(10239, plain,![X1]:![X2]:![X3]:(((subr(X1,sub_0)&arg2(X1,X3))&arg1(X1,X2))=>?[X4]:?[X5]:?[X6]:(((((((arg1(X5,X2)&hsit(X1,X4))&obj(X4,X2))&sub(X6,X3))&subr(X5,rprs_0))&subs(X4,bezeichnen_1_1))&mcont(X4,X5))&arg2(X5,X6))),inference(fof_simplification,[status(thm)],[8031,theory(equality)])). fof(10243, plain,![X1]:![X2]:(sub(X1,X2)=>?[X3]:((arg2(X3,X2)&subr(X3,sub_0))&arg1(X3,X1))),inference(fof_simplification,[status(thm)],[8465,theory(equality)])). fof(18707, plain,![X1]:![X2]:![X3]:(((~(subr(X1,sub_0))|~(arg2(X1,X3)))|~(arg1(X1,X2)))|?[X4]:?[X5]:?[X6]:(((((((arg1(X5,X2)&hsit(X1,X4))&obj(X4,X2))&sub(X6,X3))&subr(X5,rprs_0))&subs(X4,bezeichnen_1_1))&mcont(X4,X5))&arg2(X5,X6))),inference(fof_nnf,[status(thm)],[10239])). fof(18708, plain,![X7]:![X8]:![X9]:(((~(subr(X7,sub_0))|~(arg2(X7,X9)))|~(arg1(X7,X8)))|?[X10]:?[X11]:?[X12]:(((((((arg1(X11,X8)&hsit(X7,X10))&obj(X10,X8))&sub(X12,X9))&subr(X11,rprs_0))&subs(X10,bezeichnen_1_1))&mcont(X10,X11))&arg2(X11,X12))),inference(variable_rename,[status(thm)],[18707])). fof(18709, plain,![X7]:![X8]:![X9]:(((~(subr(X7,sub_0))|~(arg2(X7,X9)))|~(arg1(X7,X8)))|(((((((arg1(esk50_3(X7,X8,X9),X8)&hsit(X7,esk49_3(X7,X8,X9)))&obj(esk49_3(X7,X8,X9),X8))&sub(esk51_3(X7,X8,X9),X9))&subr(esk50_3(X7,X8,X9),rprs_0))&subs(esk49_3(X7,X8,X9),bezeichnen_1_1))&mcont(esk49_3(X7,X8,X9),esk50_3(X7,X8,X9)))&arg2(esk50_3(X7,X8,X9),esk51_3(X7,X8,X9)))),inference(skolemize,[status(esa)],[18708])). fof(18710, plain,![X7]:![X8]:![X9]:((((((((arg1(esk50_3(X7,X8,X9),X8)|((~(subr(X7,sub_0))|~(arg2(X7,X9)))|~(arg1(X7,X8))))&(hsit(X7,esk49_3(X7,X8,X9))|((~(subr(X7,sub_0))|~(arg2(X7,X9)))|~(arg1(X7,X8)))))&(obj(esk49_3(X7,X8,X9),X8)|((~(subr(X7,sub_0))|~(arg2(X7,X9)))|~(arg1(X7,X8)))))&(sub(esk51_3(X7,X8,X9),X9)|((~(subr(X7,sub_0))|~(arg2(X7,X9)))|~(arg1(X7,X8)))))&(subr(esk50_3(X7,X8,X9),rprs_0)|((~(subr(X7,sub_0))|~(arg2(X7,X9)))|~(arg1(X7,X8)))))&(subs(esk49_3(X7,X8,X9),bezeichnen_1_1)|((~(subr(X7,sub_0))|~(arg2(X7,X9)))|~(arg1(X7,X8)))))&(mcont(esk49_3(X7,X8,X9),esk50_3(X7,X8,X9))|((~(subr(X7,sub_0))|~(arg2(X7,X9)))|~(arg1(X7,X8)))))&(arg2(esk50_3(X7,X8,X9),esk51_3(X7,X8,X9))|((~(subr(X7,sub_0))|~(arg2(X7,X9)))|~(arg1(X7,X8))))),inference(distribute,[status(thm)],[18709])). cnf(18716,plain,(obj(esk49_3(X1,X2,X3),X2)|~arg1(X1,X2)|~arg2(X1,X3)|~subr(X1,sub_0)),inference(split_conjunct,[status(thm)],[18710])). fof(19168, plain,![X1]:![X2]:(~(sub(X1,X2))|?[X3]:((arg2(X3,X2)&subr(X3,sub_0))&arg1(X3,X1))),inference(fof_nnf,[status(thm)],[10243])). fof(19169, plain,![X4]:![X5]:(~(sub(X4,X5))|?[X6]:((arg2(X6,X5)&subr(X6,sub_0))&arg1(X6,X4))),inference(variable_rename,[status(thm)],[19168])). fof(19170, plain,![X4]:![X5]:(~(sub(X4,X5))|((arg2(esk53_2(X4,X5),X5)&subr(esk53_2(X4,X5),sub_0))&arg1(esk53_2(X4,X5),X4))),inference(skolemize,[status(esa)],[19169])). fof(19171, plain,![X4]:![X5]:(((arg2(esk53_2(X4,X5),X5)|~(sub(X4,X5)))&(subr(esk53_2(X4,X5),sub_0)|~(sub(X4,X5))))&(arg1(esk53_2(X4,X5),X4)|~(sub(X4,X5)))),inference(distribute,[status(thm)],[19170])). cnf(19172,plain,(arg1(esk53_2(X1,X2),X1)|~sub(X1,X2)),inference(split_conjunct,[status(thm)],[19171])). cnf(19173,plain,(subr(esk53_2(X1,X2),sub_0)|~sub(X1,X2)),inference(split_conjunct,[status(thm)],[19171])). cnf(19174,plain,(arg2(esk53_2(X1,X2),X2)|~sub(X1,X2)),inference(split_conjunct,[status(thm)],[19171])). fof(20987, negated_conjecture,![X1]:![X2]:![X3]:![X4]:![X5]:![X6]:![X7]:((((((((~(attr(X4,X3))|~(attr(X6,X7)))|~(sub(X2,name_1_1)))|~(sub(X1,firma_1_1)))|~(sub(X3,name_1_1)))|~(val(X3,bmw_0)))|~(val(X2,bmw_0)))|~(obj(X5,X1)))|~(attr(X1,X2))),inference(fof_nnf,[status(thm)],[10190])). fof(20988, negated_conjecture,![X8]:![X9]:![X10]:![X11]:![X12]:![X13]:![X14]:((((((((~(attr(X11,X10))|~(attr(X13,X14)))|~(sub(X9,name_1_1)))|~(sub(X8,firma_1_1)))|~(sub(X10,name_1_1)))|~(val(X10,bmw_0)))|~(val(X9,bmw_0)))|~(obj(X12,X8)))|~(attr(X8,X9))),inference(variable_rename,[status(thm)],[20987])). cnf(20989,negated_conjecture,(~attr(X1,X2)|~obj(X3,X1)|~val(X2,bmw_0)|~val(X4,bmw_0)|~sub(X4,name_1_1)|~sub(X1,firma_1_1)|~sub(X2,name_1_1)|~attr(X5,X6)|~attr(X7,X4)),inference(split_conjunct,[status(thm)],[20988])). cnf(21000,plain,(attr(c8774,c8775)),inference(split_conjunct,[status(thm)],[10189])). cnf(21001,plain,(sub(c8774,firma_1_1)),inference(split_conjunct,[status(thm)],[10189])). cnf(21238,plain,(val(c8775,bmw_0)),inference(split_conjunct,[status(thm)],[10189])). cnf(21239,plain,(sub(c8775,name_1_1)),inference(split_conjunct,[status(thm)],[10189])). fof(124320, plain,(~(epred1_0)<=>![X7]:![X4]:((~(val(X4,bmw_0))|~(attr(X7,X4)))|~(sub(X4,name_1_1)))),introduced(definition),['split']). cnf(124321,plain,(epred1_0|~sub(X4,name_1_1)|~attr(X7,X4)|~val(X4,bmw_0)),inference(split_equiv,[status(thm)],[124320])). fof(124322, plain,(~(epred2_0)<=>![X1]:![X3]:![X2]:((((~(val(X2,bmw_0))|~(attr(X1,X2)))|~(obj(X3,X1)))|~(sub(X1,firma_1_1)))|~(sub(X2,name_1_1)))),introduced(definition),['split']). cnf(124323,plain,(epred2_0|~sub(X1,firma_1_1)|~sub(X2,name_1_1)|~obj(X3,X1)|~attr(X1,X2)|~val(X2,bmw_0)),inference(split_equiv,[status(thm)],[124322])). fof(124324, plain,(~(epred3_0)<=>![X6]:![X5]:~(attr(X5,X6))),introduced(definition),['split']). cnf(124325,plain,(epred3_0|~attr(X5,X6)),inference(split_equiv,[status(thm)],[124324])). cnf(124326,negated_conjecture,(~epred3_0|~epred2_0|~epred1_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[20989,124320,theory(equality)]),124322,theory(equality)]),124324,theory(equality)]),['split']). cnf(124353,plain,(epred3_0),inference(spm,[status(thm)],[124325,21000,theory(equality)])). cnf(124358,negated_conjecture,($false|~epred2_0|~epred1_0),inference(rw,[status(thm)],[124326,124353,theory(equality)])). cnf(124359,negated_conjecture,(~epred2_0|~epred1_0),inference(cn,[status(thm)],[124358,theory(equality)])). cnf(124366,plain,(epred1_0|~attr(X1,c8775)|~sub(c8775,name_1_1)),inference(spm,[status(thm)],[124321,21238,theory(equality)])). cnf(124367,plain,(epred1_0|~attr(X1,c8775)|$false),inference(rw,[status(thm)],[124366,21239,theory(equality)])). cnf(124368,plain,(epred1_0|~attr(X1,c8775)),inference(cn,[status(thm)],[124367,theory(equality)])). cnf(124370,plain,(epred1_0),inference(spm,[status(thm)],[124368,21000,theory(equality)])). cnf(124371,negated_conjecture,(~epred2_0|$false),inference(rw,[status(thm)],[124359,124370,theory(equality)])). cnf(124372,negated_conjecture,(~epred2_0),inference(cn,[status(thm)],[124371,theory(equality)])). cnf(124375,negated_conjecture,(~sub(X1,firma_1_1)|~sub(X2,name_1_1)|~obj(X3,X1)|~attr(X1,X2)|~val(X2,bmw_0)),inference(sr,[status(thm)],[124323,124372,theory(equality)])). cnf(124381,plain,(~attr(X1,c8775)|~obj(X2,X1)|~sub(X1,firma_1_1)|~sub(c8775,name_1_1)),inference(spm,[status(thm)],[124375,21238,theory(equality)])). cnf(124382,plain,(~attr(X1,c8775)|~obj(X2,X1)|~sub(X1,firma_1_1)|$false),inference(rw,[status(thm)],[124381,21239,theory(equality)])). cnf(124383,plain,(~attr(X1,c8775)|~obj(X2,X1)|~sub(X1,firma_1_1)),inference(cn,[status(thm)],[124382,theory(equality)])). cnf(124384,plain,(~obj(X1,c8774)|~sub(c8774,firma_1_1)),inference(spm,[status(thm)],[124383,21000,theory(equality)])). cnf(124385,plain,(~obj(X1,c8774)|$false),inference(rw,[status(thm)],[124384,21001,theory(equality)])). cnf(124386,plain,(~obj(X1,c8774)),inference(cn,[status(thm)],[124385,theory(equality)])). cnf(124392,plain,(~subr(X1,sub_0)|~arg1(X1,c8774)|~arg2(X1,X2)),inference(spm,[status(thm)],[124386,18716,theory(equality)])). cnf(124443,plain,(~arg1(esk53_2(X1,X2),c8774)|~arg2(esk53_2(X1,X2),X3)|~sub(X1,X2)),inference(spm,[status(thm)],[124392,19173,theory(equality)])). cnf(124447,plain,(~arg1(esk53_2(X1,X2),c8774)|~sub(X1,X2)),inference(spm,[status(thm)],[124443,19174,theory(equality)])). cnf(124448,plain,(~sub(c8774,X1)),inference(spm,[status(thm)],[124447,19172,theory(equality)])). cnf(124450,plain,($false),inference(sr,[status(thm)],[21001,124448,theory(equality)])). cnf(124451,plain,($false),124450,['proof']). # SZS output end CNFRefutation # Initial clauses in saturation : 10626 # Processed clauses : 10665 # ...of these trivial : 0 # ...subsumed : 2 # ...remaining for further processing : 10663 # Other redundant clauses eliminated : 0 # Clauses deleted for lack of memory : 0 # Backward-subsumed : 1 # Backward-rewritten : 5 # Generated clauses : 103179 # ...of the previous two non-trivial : 103179 # Contextual simplify-reflections : 0 # Paramodulations : 103174 # Factorizations : 0 # Equation resolutions : 0 # Current number of processed clauses : 10655 # Positive orientable unit clauses : 10317 # Positive unorientable unit clauses: 0 # Negative unit clauses : 6 # Non-unit-clauses : 332 # Current number of unprocessed clauses: 103126 # ...number of literals in the above : 207582 # Clause-clause subsumption calls (NU) : 109054 # Rec. Clause-clause subsumption calls : 34129 # Unit Clause-clause subsumption calls : 2213 # Rewrite failures with RHS unbound : 0 # Indexed BW rewrite attempts : 2 # Indexed BW rewrite successes : 2 # Unification attempts : 113803 # Unification successes : 113646 # Backwards rewriting index : 27416 leaves, 1.01+/-0.181 terms/leaf # Paramod-from index : 10519 leaves, 1.00+/-0.010 terms/leaf # Paramod-into index : 27306 leaves, 1.00+/-0.041 terms/leaf # ------------------------------------------------- # User time : 2.160 s # System time : 0.230 s # Total time : 2.390 s # Maximum resident set size: 686812 pages WATCH: 3.40 CPU 3.52 WC FINAL WATCH: 3.40 CPU 3.52 WC