WATCH: 0.00 CPU 0.01 WC Hi Geoff, go and have some cold beer while I am trying to solve this very hard problem! % remaining time: 2999 next slice time: 17 dis-1002_5:1_bs=unit_only:bsr=unit_only:flr=on:gsp=input_only:lcm=predicate:nwc=1:nicw=on:ptb=off:ssec=off:sswn=on:sos=on:spo=on:swb=on:sp=occurrence_15 on FNE084 Refutation found. Thanks to Tanya! % SZS status Theorem for FNE084 % SZS output start Proof for FNE084 25549. $false (5:0) [subsumption resolution 25536,21263] 21263. ~sP3(c8774) (2:2) [subsumption resolution 21262,10671] 10671. sub(c8774,firma_1_1) (0:3) [cnf transformation 10233] 10233. 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) & assoc(produktemanagement_1_1,erzeugnis_1_1) & fact(c8713,real) & etype(c8719,int0) & fact(c8719,real) & etype(firma_1_1,int0) & etype(c8724,int0) & etype(c8733,int0) & fact(produktemanagement_1_1,real) & etype(c8740,int0) & fact(c8740,real) & fact(absatz_1_2,real) & etype(dynafit_1_1,int0) & etype(absatzf__366rderung_1_1,int0) & fact(c8761,real) & etype(c8774,int0) & fact(c8775,real) & fact(name_1_1,real) & etype(c8779,int0) & fact(c8779,real) & etype(erzeugnis_1_1,etype_c) & fact(erzeugnis_1_1,real) & fact(management__1_1,real) & etype(management__1_1,int0) & fact(c9098,real) & etype(c9098,etype_c) & fact(land_1_1,real) & etype(land_1_1,int0) & fact(c8778,real) & etype(c8778,int0) & etype(name_1_1,int0) & etype(c8775,int0) & fact(c8774,real) & fact(leiter_1_1,real) & etype(leiter_1_1,int0) & etype(c8761,int1) & fact(absatzf__366rderung_1_1,real) & fact(c8755,real) & etype(c8755,int0) & fact(dynafit_1_1,real) & fact(c8743,real) & etype(c8743,int1) & etype(absatz_1_2,int0) & etype(produktemanagement_1_1,int0) & fact(c8733,real) & fact(c8725,real) & etype(c8725,int0) & fact(c8724,real) & fact(firma_1_1,real) & fact(familiename_1_1,real) & etype(familiename_1_1,int0) & fact(mensch_1_1,real) & etype(mensch_1_1,int0) & fact(c8714,real) & etype(c8714,int0) & 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)[pure predicate removal 10225] 10225. 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) & assoc(produktemanagement_1_1,erzeugnis_1_1) & fact(c8713,real) & gener(c8714,sp) & gener(familiename_1_1,ge) & etype(c8719,int0) & fact(c8719,real) & gener(c8719,sp) & etype(firma_1_1,int0) & gener(firma_1_1,ge) & etype(c8724,int0) & gener(c8725,sp) & etype(c8733,int0) & gener(c8733,sp) & fact(produktemanagement_1_1,real) & etype(c8740,int0) & fact(c8740,real) & fact(absatz_1_2,real) & gener(c8743,gener_c) & etype(dynafit_1_1,int0) & gener(dynafit_1_1,ge) & gener(c8755,gener_c) & etype(absatzf__366rderung_1_1,int0) & fact(c8761,real) & gener(leiter_1_1,ge) & etype(c8774,int0) & gener(c8774,sp) & fact(c8775,real) & gener(c8775,sp) & fact(name_1_1,real) & gener(c8778,sp) & etype(c8779,int0) & fact(c8779,real) & gener(land_1_1,ge) & gener(c9098,gener_c) & etype(erzeugnis_1_1,etype_c) & fact(erzeugnis_1_1,real) & gener(management__1_1,ge) & fact(management__1_1,real) & etype(management__1_1,int0) & gener(erzeugnis_1_1,ge) & fact(c9098,real) & etype(c9098,etype_c) & fact(land_1_1,real) & etype(land_1_1,int0) & gener(c8779,sp) & fact(c8778,real) & etype(c8778,int0) & gener(name_1_1,ge) & etype(name_1_1,int0) & etype(c8775,int0) & fact(c8774,real) & fact(leiter_1_1,real) & etype(leiter_1_1,int0) & gener(c8761,gener_c) & etype(c8761,int1) & gener(absatzf__366rderung_1_1,ge) & fact(absatzf__366rderung_1_1,real) & fact(c8755,real) & etype(c8755,int0) & fact(dynafit_1_1,real) & fact(c8743,real) & etype(c8743,int1) & gener(absatz_1_2,ge) & etype(absatz_1_2,int0) & gener(c8740,sp) & gener(produktemanagement_1_1,ge) & etype(produktemanagement_1_1,int0) & fact(c8733,real) & fact(c8725,real) & etype(c8725,int0) & gener(c8724,sp) & fact(c8724,real) & fact(firma_1_1,real) & fact(familiename_1_1,real) & etype(familiename_1_1,int0) & gener(mensch_1_1,ge) & fact(mensch_1_1,real) & etype(mensch_1_1,int0) & fact(c8714,real) & etype(c8714,int0) & 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)[pure predicate removal 10218] 10218. 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) & assoc(produktemanagement_1_1,erzeugnis_1_1) & card(c8713,int1) & fact(c8713,real) & card(c8714,int1) & gener(c8714,sp) & gener(familiename_1_1,ge) & etype(c8719,int0) & fact(c8719,real) & gener(c8719,sp) & etype(firma_1_1,int0) & gener(firma_1_1,ge) & card(c8724,int1) & etype(c8724,int0) & card(c8725,int1) & gener(c8725,sp) & card(c8733,int1) & etype(c8733,int0) & gener(c8733,sp) & fact(produktemanagement_1_1,real) & card(c8740,int1) & etype(c8740,int0) & fact(c8740,real) & card(absatz_1_2,int1) & fact(absatz_1_2,real) & card(c8743,cons(x_constant,cons(int1,nil))) & gener(c8743,gener_c) & etype(dynafit_1_1,int0) & gener(dynafit_1_1,ge) & gener(c8755,gener_c) & card(absatzf__366rderung_1_1,int1) & etype(absatzf__366rderung_1_1,int0) & card(c8761,cons(x_constant,cons(int1,nil))) & fact(c8761,real) & card(leiter_1_1,int1) & gener(leiter_1_1,ge) & etype(c8774,int0) & gener(c8774,sp) & fact(c8775,real) & gener(c8775,sp) & card(name_1_1,int1) & fact(name_1_1,real) & card(c8778,int1) & gener(c8778,sp) & etype(c8779,int0) & fact(c8779,real) & card(land_1_1,int1) & gener(land_1_1,ge) & gener(c9098,gener_c) & etype(erzeugnis_1_1,etype_c) & fact(erzeugnis_1_1,real) & card(management__1_1,int1) & gener(management__1_1,ge) & fact(management__1_1,real) & etype(management__1_1,int0) & gener(erzeugnis_1_1,ge) & card(erzeugnis_1_1,card_c) & fact(c9098,real) & etype(c9098,etype_c) & card(c9098,card_c) & fact(land_1_1,real) & etype(land_1_1,int0) & gener(c8779,sp) & card(c8779,int1) & fact(c8778,real) & etype(c8778,int0) & gener(name_1_1,ge) & etype(name_1_1,int0) & etype(c8775,int0) & card(c8775,int1) & fact(c8774,real) & card(c8774,int1) & fact(leiter_1_1,real) & etype(leiter_1_1,int0) & gener(c8761,gener_c) & etype(c8761,int1) & gener(absatzf__366rderung_1_1,ge) & fact(absatzf__366rderung_1_1,real) & fact(c8755,real) & etype(c8755,int0) & card(c8755,int1) & fact(dynafit_1_1,real) & card(dynafit_1_1,int1) & fact(c8743,real) & etype(c8743,int1) & gener(absatz_1_2,ge) & etype(absatz_1_2,int0) & gener(c8740,sp) & gener(produktemanagement_1_1,ge) & etype(produktemanagement_1_1,int0) & card(produktemanagement_1_1,int1) & fact(c8733,real) & fact(c8725,real) & etype(c8725,int0) & gener(c8724,sp) & fact(c8724,real) & fact(firma_1_1,real) & card(firma_1_1,int1) & card(c8719,int1) & fact(familiename_1_1,real) & etype(familiename_1_1,int0) & card(familiename_1_1,int1) & gener(mensch_1_1,ge) & fact(mensch_1_1,real) & etype(mensch_1_1,int0) & card(mensch_1_1,int1) & fact(c8714,real) & etype(c8714,int0) & 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)[pure predicate removal 10215] 10215. 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) & assoc(produktemanagement_1_1,erzeugnis_1_1) & card(c8713,int1) & fact(c8713,real) & card(c8714,int1) & gener(c8714,sp) & varia(c8714,varia_c) & varia(mensch_1_1,varia_c) & gener(familiename_1_1,ge) & etype(c8719,int0) & fact(c8719,real) & gener(c8719,sp) & varia(c8719,con) & etype(firma_1_1,int0) & gener(firma_1_1,ge) & varia(firma_1_1,varia_c) & card(c8724,int1) & etype(c8724,int0) & card(c8725,int1) & gener(c8725,sp) & card(c8733,int1) & etype(c8733,int0) & gener(c8733,sp) & varia(c8733,con) & fact(produktemanagement_1_1,real) & varia(produktemanagement_1_1,varia_c) & card(c8740,int1) & etype(c8740,int0) & fact(c8740,real) & varia(c8740,con) & card(absatz_1_2,int1) & fact(absatz_1_2,real) & varia(absatz_1_2,varia_c) & card(c8743,cons(x_constant,cons(int1,nil))) & gener(c8743,gener_c) & varia(c8743,varia_c) & etype(dynafit_1_1,int0) & gener(dynafit_1_1,ge) & gener(c8755,gener_c) & varia(c8755,varia_c) & card(absatzf__366rderung_1_1,int1) & etype(absatzf__366rderung_1_1,int0) & varia(absatzf__366rderung_1_1,varia_c) & card(c8761,cons(x_constant,cons(int1,nil))) & fact(c8761,real) & card(leiter_1_1,int1) & gener(leiter_1_1,ge) & varia(leiter_1_1,varia_c) & etype(c8774,int0) & gener(c8774,sp) & varia(c8774,con) & fact(c8775,real) & gener(c8775,sp) & card(name_1_1,int1) & fact(name_1_1,real) & varia(name_1_1,varia_c) & card(c8778,int1) & gener(c8778,sp) & etype(c8779,int0) & fact(c8779,real) & card(land_1_1,int1) & gener(land_1_1,ge) & gener(c9098,gener_c) & etype(erzeugnis_1_1,etype_c) & fact(erzeugnis_1_1,real) & card(management__1_1,int1) & 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) & gener(erzeugnis_1_1,ge) & card(erzeugnis_1_1,card_c) & varia(c9098,varia_c) & fact(c9098,real) & etype(c9098,etype_c) & card(c9098,card_c) & varia(land_1_1,varia_c) & fact(land_1_1,real) & etype(land_1_1,int0) & varia(c8779,varia_c) & gener(c8779,sp) & card(c8779,int1) & varia(c8778,con) & fact(c8778,real) & etype(c8778,int0) & gener(name_1_1,ge) & etype(name_1_1,int0) & varia(c8775,varia_c) & etype(c8775,int0) & card(c8775,int1) & fact(c8774,real) & card(c8774,int1) & fact(leiter_1_1,real) & etype(leiter_1_1,int0) & varia(c8761,varia_c) & gener(c8761,gener_c) & etype(c8761,int1) & gener(absatzf__366rderung_1_1,ge) & fact(absatzf__366rderung_1_1,real) & 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) & fact(c8743,real) & etype(c8743,int1) & gener(absatz_1_2,ge) & etype(absatz_1_2,int0) & gener(c8740,sp) & gener(produktemanagement_1_1,ge) & etype(produktemanagement_1_1,int0) & card(produktemanagement_1_1,int1) & fact(c8733,real) & varia(c8725,varia_c) & fact(c8725,real) & etype(c8725,int0) & varia(c8724,con) & gener(c8724,sp) & fact(c8724,real) & fact(firma_1_1,real) & card(firma_1_1,int1) & card(c8719,int1) & varia(familiename_1_1,varia_c) & fact(familiename_1_1,real) & etype(familiename_1_1,int0) & card(familiename_1_1,int1) & gener(mensch_1_1,ge) & fact(mensch_1_1,real) & etype(mensch_1_1,int0) & card(mensch_1_1,int1) & fact(c8714,real) & etype(c8714,int0) & varia(c8713,con) & 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)[pure predicate removal 10210] 10210. 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) & assoc(produktemanagement_1_1,erzeugnis_1_1) & card(c8713,int1) & fact(c8713,real) & refer(c8713,det) & card(c8714,int1) & gener(c8714,sp) & varia(c8714,varia_c) & varia(mensch_1_1,varia_c) & gener(familiename_1_1,ge) & refer(familiename_1_1,refer_c) & etype(c8719,int0) & fact(c8719,real) & gener(c8719,sp) & refer(c8719,det) & varia(c8719,con) & etype(firma_1_1,int0) & gener(firma_1_1,ge) & refer(firma_1_1,refer_c) & varia(firma_1_1,varia_c) & card(c8724,int1) & etype(c8724,int0) & card(c8725,int1) & gener(c8725,sp) & refer(c8725,indet) & card(c8733,int1) & etype(c8733,int0) & gener(c8733,sp) & varia(c8733,con) & fact(produktemanagement_1_1,real) & varia(produktemanagement_1_1,varia_c) & card(c8740,int1) & etype(c8740,int0) & fact(c8740,real) & varia(c8740,con) & 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) & etype(dynafit_1_1,int0) & gener(dynafit_1_1,ge) & refer(dynafit_1_1,refer_c) & gener(c8755,gener_c) & refer(c8755,refer_c) & varia(c8755,varia_c) & card(absatzf__366rderung_1_1,int1) & etype(absatzf__366rderung_1_1,int0) & 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) & card(leiter_1_1,int1) & gener(leiter_1_1,ge) & refer(leiter_1_1,refer_c) & varia(leiter_1_1,varia_c) & etype(c8774,int0) & gener(c8774,sp) & varia(c8774,con) & fact(c8775,real) & gener(c8775,sp) & card(name_1_1,int1) & fact(name_1_1,real) & varia(name_1_1,varia_c) & card(c8778,int1) & gener(c8778,sp) & etype(c8779,int0) & fact(c8779,real) & refer(c8779,indet) & card(land_1_1,int1) & gener(land_1_1,ge) & gener(c9098,gener_c) & refer(c9098,refer_c) & etype(erzeugnis_1_1,etype_c) & fact(erzeugnis_1_1,real) & refer(erzeugnis_1_1,refer_c) & card(management__1_1,int1) & 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) & gener(erzeugnis_1_1,ge) & card(erzeugnis_1_1,card_c) & varia(c9098,varia_c) & fact(c9098,real) & etype(c9098,etype_c) & card(c9098,card_c) & varia(land_1_1,varia_c) & refer(land_1_1,refer_c) & fact(land_1_1,real) & etype(land_1_1,int0) & varia(c8779,varia_c) & gener(c8779,sp) & card(c8779,int1) & varia(c8778,con) & refer(c8778,det) & fact(c8778,real) & etype(c8778,int0) & 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) & fact(leiter_1_1,real) & etype(leiter_1_1,int0) & varia(c8761,varia_c) & gener(c8761,gener_c) & etype(c8761,int1) & gener(absatzf__366rderung_1_1,ge) & fact(absatzf__366rderung_1_1,real) & 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) & fact(c8743,real) & etype(c8743,int1) & gener(absatz_1_2,ge) & etype(absatz_1_2,int0) & refer(c8740,det) & gener(c8740,sp) & refer(produktemanagement_1_1,refer_c) & gener(produktemanagement_1_1,ge) & etype(produktemanagement_1_1,int0) & card(produktemanagement_1_1,int1) & refer(c8733,det) & fact(c8733,real) & varia(c8725,varia_c) & fact(c8725,real) & etype(c8725,int0) & varia(c8724,con) & refer(c8724,det) & gener(c8724,sp) & fact(c8724,real) & fact(firma_1_1,real) & card(firma_1_1,int1) & card(c8719,int1) & varia(familiename_1_1,varia_c) & fact(familiename_1_1,real) & etype(familiename_1_1,int0) & card(familiename_1_1,int1) & refer(mensch_1_1,refer_c) & gener(mensch_1_1,ge) & fact(mensch_1_1,real) & etype(mensch_1_1,int0) & card(mensch_1_1,int1) & refer(c8714,indet) & fact(c8714,real) & etype(c8714,int0) & varia(c8713,con) & 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)[pure predicate removal 10202] 10202. 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) & assoc(produktemanagement_1_1,erzeugnis_1_1) & 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) & etype(c8719,int0) & fact(c8719,real) & gener(c8719,sp) & quant(c8719,one) & refer(c8719,det) & varia(c8719,con) & 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) & card(c8724,int1) & etype(c8724,int0) & card(c8725,int1) & gener(c8725,sp) & quant(c8725,one) & refer(c8725,indet) & card(c8733,int1) & etype(c8733,int0) & gener(c8733,sp) & quant(c8733,one) & varia(c8733,con) & fact(produktemanagement_1_1,real) & varia(produktemanagement_1_1,varia_c) & card(c8740,int1) & etype(c8740,int0) & fact(c8740,real) & quant(c8740,one) & varia(c8740,con) & 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) & etype(dynafit_1_1,int0) & gener(dynafit_1_1,ge) & quant(dynafit_1_1,one) & refer(dynafit_1_1,refer_c) & 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) & card(leiter_1_1,int1) & gener(leiter_1_1,ge) & refer(leiter_1_1,refer_c) & varia(leiter_1_1,varia_c) & etype(c8774,int0) & gener(c8774,sp) & quant(c8774,one) & varia(c8774,con) & fact(c8775,real) & gener(c8775,sp) & quant(c8775,one) & card(name_1_1,int1) & fact(name_1_1,real) & quant(name_1_1,one) & varia(name_1_1,varia_c) & 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) & 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) & 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) & varia(c9098,varia_c) & fact(c9098,real) & etype(c9098,etype_c) & card(c9098,card_c) & varia(land_1_1,varia_c) & refer(land_1_1,refer_c) & fact(land_1_1,real) & etype(land_1_1,int0) & varia(c8779,varia_c) & quant(c8779,one) & gener(c8779,sp) & card(c8779,int1) & varia(c8778,con) & refer(c8778,det) & fact(c8778,real) & etype(c8778,int0) & 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) & 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) & gener(absatzf__366rderung_1_1,ge) & fact(absatzf__366rderung_1_1,real) & 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) & quant(absatz_1_2,one) & gener(absatz_1_2,ge) & etype(absatz_1_2,int0) & 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) & 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) & card(c8719,int1) & varia(familiename_1_1,varia_c) & fact(familiename_1_1,real) & etype(familiename_1_1,int0) & card(familiename_1_1,int1) & 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) & refer(c8714,indet) & fact(c8714,real) & etype(c8714,int0) & 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)[pure predicate removal 10191] 10191. 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) & 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)[pure predicate removal 10190] 10190. 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)[input] 21262. ~sub(c8774,firma_1_1) | ~sP3(c8774) (2:5) [resolution 21177,10672] 10672. attr(c8774,c8775) (0:3) [cnf transformation 10233] 21177. ~attr(X0,c8775) | ~sub(X0,firma_1_1) | ~sP3(X0) (1:8) [subsumption resolution 21171,10609] 10609. sub(c8775,name_1_1) (0:3) [cnf transformation 10233] 21171. ~attr(X0,c8775) | ~sub(X0,firma_1_1) | ~sub(c8775,name_1_1) | ~sP3(X0) (1:11) [resolution 21170,10610] 10610. val(c8775,bmw_0) (0:3) [cnf transformation 10233] 21170. ~val(X1,bmw_0) | ~attr(X0,X1) | ~sub(X0,firma_1_1) | ~sub(X1,name_1_1) | ~sP3(X0) (0:14) [subsumption resolution 21117,21164] 21164. sP5 (3:1) [resolution 21158,20902] 20902. ~sP4(X3) | sP5 (0:3) [general splitting component introduction] 21158. sP4(c8774) (2:2) [resolution 21095,10672] 21095. ~attr(X0,c8775) | sP4(X0) (1:5) [subsumption resolution 21089,10609] 21089. ~sub(c8775,name_1_1) | ~attr(X0,c8775) | sP4(X0) (1:8) [resolution 20900,10610] 20900. ~val(X2,bmw_0) | ~sub(X2,name_1_1) | ~attr(X3,X2) | sP4(X3) (0:11) [general splitting component introduction] 21117. ~val(X1,bmw_0) | ~attr(X0,X1) | ~sub(X0,firma_1_1) | ~sub(X1,name_1_1) | ~sP3(X0) | ~sP5 (0:15) [subsumption resolution 20903,21101] 21101. sP2 (2:1) [resolution 21069,20896] 20896. ~sP1(X5) | sP2 (0:3) [general splitting component introduction] 21069. sP1(c8713) (1:2) [resolution 20894,10604] 10604. attr(c8713,c8714) (0:3) [cnf transformation 10233] 20894. ~attr(X5,X6) | sP1(X5) (0:5) [general splitting component introduction] 20903. ~val(X1,bmw_0) | ~attr(X0,X1) | ~sub(X0,firma_1_1) | ~sub(X1,name_1_1) | ~sP2 | ~sP3(X0) | ~sP5 (0:16) [general splitting 20901,20902] 20901. ~attr(X0,X1) | ~val(X1,bmw_0) | ~sub(X0,firma_1_1) | ~sub(X1,name_1_1) | ~sP2 | ~sP3(X0) | ~sP4(X3) (0:17) [general splitting 20899,20900] 20899. ~attr(X0,X1) | ~val(X1,bmw_0) | ~val(X2,bmw_0) | ~sub(X2,name_1_1) | ~sub(X0,firma_1_1) | ~sub(X1,name_1_1) | ~attr(X3,X2) | ~sP2 | ~sP3(X0) (0:24) [general splitting 20897,20898] 20898. ~obj(X4,X0) | sP3(X0) (0:5) [general splitting component introduction] 20897. ~attr(X0,X1) | ~obj(X4,X0) | ~val(X1,bmw_0) | ~val(X2,bmw_0) | ~sub(X2,name_1_1) | ~sub(X0,firma_1_1) | ~sub(X1,name_1_1) | ~attr(X3,X2) | ~sP2 (0:25) [general splitting 20895,20896] 20895. ~attr(X0,X1) | ~obj(X4,X0) | ~val(X1,bmw_0) | ~val(X2,bmw_0) | ~sub(X2,name_1_1) | ~sub(X0,firma_1_1) | ~sub(X1,name_1_1) | ~attr(X3,X2) | ~sP1(X5) (0:26) [general splitting 10603,20894] 10603. ~attr(X0,X1) | ~obj(X4,X0) | ~val(X1,bmw_0) | ~val(X2,bmw_0) | ~sub(X2,name_1_1) | ~sub(X0,firma_1_1) | ~sub(X1,name_1_1) | ~attr(X5,X6) | ~attr(X3,X2) (0:27) [cnf transformation 10349] 10349. ! [X0,X1,X2,X3,X4,X5,X6] : (~attr(X3,X2) | ~attr(X5,X6) | ~sub(X1,name_1_1) | ~sub(X0,firma_1_1) | ~sub(X2,name_1_1) | ~val(X2,bmw_0) | ~val(X1,bmw_0) | ~obj(X4,X0) | ~attr(X0,X1))[ennf transformation 10189] 10189. ~? [X0,X1,X2,X3,X4,X5,X6] : (attr(X3,X2) & attr(X5,X6) & sub(X1,name_1_1) & sub(X0,firma_1_1) & sub(X2,name_1_1) & val(X2,bmw_0) & val(X1,bmw_0) & obj(X4,X0) & attr(X0,X1))[negated conjecture 10188] 10188. ? [X0,X1,X2,X3,X4,X5,X6] : (attr(X3,X2) & attr(X5,X6) & sub(X1,name_1_1) & sub(X0,firma_1_1) & sub(X2,name_1_1) & val(X2,bmw_0) & val(X1,bmw_0) & obj(X4,X0) & attr(X0,X1))[input] 25536. sP3(c8774) (5:2) [resolution 22764,10671] 22764. ~sub(X0,X1) | sP3(X0) (4:5) [duplicate literal removal 22763] 22763. sP3(X0) | ~sub(X0,X1) | ~sub(X0,X1) (4:8) [resolution 21673,20636] 20636. arg2(sK4(X1,X0),X1) | ~sub(X0,X1) (0:8) [cnf transformation 10558] 10558. ! [X0,X1] : (~sub(X0,X1) | (arg2(sK4(X1,X0),X1) & subr(sK4(X1,X0),sub_0) & arg1(sK4(X1,X0),X0)))[skolemisation 10358] 10358. ! [X0,X1] : (~sub(X0,X1) | ? [X2] : (arg2(X2,X1) & subr(X2,sub_0) & arg1(X2,X0)))[ennf transformation 8465] 8465. ! [X0,X1] : (sub(X0,X1) => ? [X2] : (arg2(X2,X1) & subr(X2,sub_0) & arg1(X2,X0)))[input] 21673. ~arg2(sK4(X0,X1),X2) | sP3(X1) | ~sub(X1,X0) (3:10) [duplicate literal removal 21672] 21672. ~arg2(sK4(X0,X1),X2) | sP3(X1) | ~sub(X1,X0) | ~sub(X1,X0) (3:13) [resolution 21266,20638] 20638. arg1(sK4(X1,X0),X0) | ~sub(X0,X1) (0:8) [cnf transformation 10558] 21266. ~arg1(sK4(X0,X1),X2) | ~arg2(sK4(X0,X1),X3) | sP3(X2) | ~sub(X1,X0) (2:15) [resolution 21080,20637] 20637. subr(sK4(X1,X0),sub_0) | ~sub(X0,X1) (0:8) [cnf transformation 10558] 21080. ~subr(X9,sub_0) | ~arg1(X9,X8) | ~arg2(X9,X10) | sP3(X8) (1:11) [resolution 20898,20676] 20676. obj(sK13(X2,X1,X0),X1) | ~arg1(X0,X1) | ~arg2(X0,X2) | ~subr(X0,sub_0) (0:15) [cnf transformation 10567] 10567. ! [X0,X1,X2] : (~subr(X0,sub_0) | ~arg2(X0,X2) | ~arg1(X0,X1) | (arg1(sK14(X2,X1,X0),X1) & hsit(X0,sK13(X2,X1,X0)) & obj(sK13(X2,X1,X0),X1) & sub(sK15(X2,X1,X0),X2) & subr(sK14(X2,X1,X0),rprs_0) & subs(sK13(X2,X1,X0),bezeichnen_1_1) & mcont(sK13(X2,X1,X0),sK14(X2,X1,X0)) & arg2(sK14(X2,X1,X0),sK15(X2,X1,X0))))[skolemisation 10387] 10387. ! [X0,X1,X2] : (~subr(X0,sub_0) | ~arg2(X0,X2) | ~arg1(X0,X1) | ? [X3,X4,X5] : (arg1(X4,X1) & hsit(X0,X3) & obj(X3,X1) & sub(X5,X2) & subr(X4,rprs_0) & subs(X3,bezeichnen_1_1) & mcont(X3,X4) & arg2(X4,X5)))[flattening 10386] 10386. ! [X0,X1,X2] : ((~subr(X0,sub_0) | ~arg2(X0,X2) | ~arg1(X0,X1)) | ? [X3,X4,X5] : (arg1(X4,X1) & hsit(X0,X3) & obj(X3,X1) & sub(X5,X2) & subr(X4,rprs_0) & subs(X3,bezeichnen_1_1) & mcont(X3,X4) & arg2(X4,X5)))[ennf transformation 8031] 8031. ! [X0,X1,X2] : ((subr(X0,sub_0) & arg2(X0,X2) & arg1(X0,X1)) => ? [X3,X4,X5] : (arg1(X4,X1) & hsit(X0,X3) & obj(X3,X1) & sub(X5,X2) & subr(X4,rprs_0) & subs(X3,bezeichnen_1_1) & mcont(X3,X4) & arg2(X4,X5)))[input] % SZS output end Proof for FNE084 ------------------------------ Version: Vampire 1.8 (revision 1280) Termination reason: Refutation Active clauses: 10858 Passive clauses: 4314 Generated clauses: 4641 Final active clauses: 10853 Final passive clauses: 3640 Input formulas: 10189 Initial clauses: 10341 Pure predicates: 31 Duplicate literals: 41 Fw subsumption resolutions: 248 Bw subsumption resolutions: 2 Forward subsumptions: 118 Backward subsumptions: 3 Binary resolution: 4280 Factoring: 6 Memory used [KB]: 40041 Time elapsed: 0.362 s ------------------------------ % Success in time 0.41 s WATCH: 0.37 CPU 0.42 WC FINAL WATCH: 0.37 CPU 0.42 WC