% Vampire version 0.6 licenced to run at CASC-J5
% Any licence to use Vampire shall only be obtained
% as described on Vampire's home page http://www.vprover.org.

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: 84
dis+10_10_bs=off:gsp=input_only:lcm=reverse:nwc=10.0:nicw=on:sswn=on:sgo=on_62 on FNE084
Refutation found. Thanks to Tanya!
% SZS status Theorem for FNE084
% SZS output start Proof for FNE084
fof(f25690_2,plain,(
  $false),
  inference(merge,[],[f21000_1,f21001_1,f21002_1,f21003_1,f21009_1,f25690_1])).
fof(f25690_1,plain,(
  $false | ( ( $bdd2 => ~$bdd1) & ( ~$bdd2 => $true ) )),
  inference(resolution,[],[f25172,f21011_1])).
fof(f21011_1,plain,(
  ~sP3(c8774) | ( ( $bdd2 => ~$bdd1) & ( ~$bdd2 => $true ) )),
  inference(subsumption_resolution,[],[f21010_1,f10670])).
fof(f10670,plain,(
  sub(c8774,firma_1_1)),
  inference(cnf_transformation,[],[f10230])).
fof(f10230,plain,(
  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)),
  inference(pure_predicate_removal,[],[f10224])).
fof(f10224,plain,(
  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)),
  inference(pure_predicate_removal,[],[f10217])).
fof(f10217,plain,(
  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)),
  inference(pure_predicate_removal,[],[f10214])).
fof(f10214,plain,(
  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)),
  inference(pure_predicate_removal,[],[f10209])).
fof(f10209,plain,(
  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)),
  inference(pure_predicate_removal,[],[f10201])).
fof(f10201,plain,(
  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)),
  inference(pure_predicate_removal,[],[f10190])).
fof(f10190,plain,(
  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)),
  inference(pure_predicate_removal,[],[f10189])).
fof(f10189,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(f21010_1,plain,(
  ~sub(c8774,firma_1_1) | ~sP3(c8774) | ( ( $bdd2 => ~$bdd1) & ( ~$bdd2 => $true ) )),
  inference(resolution,[],[f21008_1,f10671])).
fof(f10671,plain,(
  attr(c8774,c8775)),
  inference(cnf_transformation,[],[f10230])).
fof(f21008_1,plain,(
  ( ! [X0] : (~attr(X0,c8775) | ~sub(X0,firma_1_1) | ~sP3(X0)) ) | ( ( $bdd2 => ~$bdd1) & ( ~$bdd2 => $true ) )),
  inference(subsumption_resolution,[],[f21007_1,f10608])).
fof(f10608,plain,(
  sub(c8775,name_1_1)),
  inference(cnf_transformation,[],[f10230])).
fof(f21007_1,plain,(
  ( ! [X0] : (~attr(X0,c8775) | ~sub(X0,firma_1_1) | ~sub(c8775,name_1_1) | ~sP3(X0)) ) | ( ( $bdd2 => ~$bdd1) & ( ~$bdd2 => $true ) )),
  inference(resolution,[],[f20993_1,f10609])).
fof(f10609,plain,(
  val(c8775,bmw_0)),
  inference(cnf_transformation,[],[f10230])).
fof(fbd2,plain,(
  sP5 <=> $bdd2),
  introduced(bddzation,[])).
fof(fbd1,plain,(
  sP2 <=> $bdd1),
  introduced(bddzation,[])).
fof(f20993_1,plain,(
  ( ! [X0,X1] : (~val(X1,bmw_0) | ~attr(X0,X1) | ~sub(X0,firma_1_1) | ~sub(X1,name_1_1) | ~sP3(X0)) ) | ( ( $bdd2 => ~$bdd1) & ( ~$bdd2 => $true ) )),
  inference(definition_folding,[],[f20902,fbd2,fbd1])).
fof(f20902,plain,(
  ( ! [X0,X1] : (~attr(X0,X1) | ~val(X1,bmw_0) | ~sub(X0,firma_1_1) | ~sub(X1,name_1_1) | ~sP2 | ~sP3(X0) | ~sP5) )),
  inference(general_splitting,[],[f20900,f20901_D])).
fof(f20901,plain,(
  ( ! [X3] : (~sP4(X3) | sP5) )),
  inference(cnf_transformation,[],[f20901_D])).
fof(f20901_D,plain,(
  ( ! [X3] : ~sP4(X3) ) <=> ~sP5),
  introduced(general_splitting_component_introduction,[])).
fof(f20900,plain,(
  ( ! [X0,X3,X1] : (~attr(X0,X1) | ~val(X1,bmw_0) | ~sub(X0,firma_1_1) | ~sub(X1,name_1_1) | ~sP2 | ~sP3(X0) | ~sP4(X3)) )),
  inference(general_splitting,[],[f20898,f20899_D])).
fof(f20899,plain,(
  ( ! [X2,X3] : (~val(X2,bmw_0) | ~sub(X2,name_1_1) | ~attr(X3,X2) | sP4(X3)) )),
  inference(cnf_transformation,[],[f20899_D])).
fof(f20899_D,plain,(
  ( ! [X3] : (( ! [X2] : (~val(X2,bmw_0) | ~sub(X2,name_1_1) | ~attr(X3,X2)) ) <=> ~sP4(X3)) )),
  introduced(general_splitting_component_introduction,[])).
fof(f20898,plain,(
  ( ! [X2,X0,X3,X1] : (~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)) )),
  inference(general_splitting,[],[f20896,f20897_D])).
fof(f20897,plain,(
  ( ! [X4,X0] : (~obj(X4,X0) | sP3(X0)) )),
  inference(cnf_transformation,[],[f20897_D])).
fof(f20897_D,plain,(
  ( ! [X0] : (( ! [X4] : ~obj(X4,X0) ) <=> ~sP3(X0)) )),
  introduced(general_splitting_component_introduction,[])).
fof(f20896,plain,(
  ( ! [X4,X2,X0,X3,X1] : (~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) )),
  inference(general_splitting,[],[f20894,f20895_D])).
fof(f20895,plain,(
  ( ! [X5] : (~sP1(X5) | sP2) )),
  inference(cnf_transformation,[],[f20895_D])).
fof(f20895_D,plain,(
  ( ! [X5] : ~sP1(X5) ) <=> ~sP2),
  introduced(general_splitting_component_introduction,[])).
fof(f20894,plain,(
  ( ! [X4,X2,X0,X5,X3,X1] : (~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)) )),
  inference(general_splitting,[],[f10602,f20893_D])).
fof(f20893,plain,(
  ( ! [X6,X5] : (~attr(X5,X6) | sP1(X5)) )),
  inference(cnf_transformation,[],[f20893_D])).
fof(f20893_D,plain,(
  ( ! [X5] : (( ! [X6] : ~attr(X5,X6) ) <=> ~sP1(X5)) )),
  introduced(general_splitting_component_introduction,[])).
fof(f10602,plain,(
  ( ! [X6,X4,X2,X0,X5,X3,X1] : (~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)) )),
  inference(cnf_transformation,[],[f10348])).
fof(f10348,plain,(
  ! [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))),
  inference(ennf_transformation,[],[f10188])).
fof(f10188,negated_conjecture,(
  ~? [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))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE084.p',synth_qa07_007_mn3_277)).
fof(f25172,plain,(
  sP3(c8774)),
  inference(resolution,[],[f24168,f10670])).
fof(f24168,plain,(
  ( ! [X0,X1] : (~sub(X0,X1) | sP3(X0)) )),
  inference(duplicate_literal_removal,[],[f24167])).
fof(f24167,plain,(
  ( ! [X0,X1] : (~sub(X0,X1) | sP3(X0) | ~sub(X0,X1)) )),
  inference(resolution,[],[f24166,f20635])).
fof(f20635,plain,(
  ( ! [X0,X1] : (arg2(sK4(X1,X0),X1) | ~sub(X0,X1)) )),
  inference(cnf_transformation,[],[f10557])).
fof(f10557,plain,(
  ! [X0,X1] : (~sub(X0,X1) | (arg2(sK4(X1,X0),X1) & subr(sK4(X1,X0),sub_0) & arg1(sK4(X1,X0),X0)))),
  inference(skolemisation,[status(esa)],[f10357])).
fof(f10357,plain,(
  ! [X0,X1] : (~sub(X0,X1) | ? [X2] : (arg2(X2,X1) & subr(X2,sub_0) & arg1(X2,X0)))),
  inference(ennf_transformation,[],[f8465])).
fof(f8465,axiom,(
  ! [X0,X1] : (sub(X0,X1) => ? [X2] : (arg2(X2,X1) & subr(X2,sub_0) & arg1(X2,X0)))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE084.p',sub__sub_0_expansion)).
fof(f24166,plain,(
  ( ! [X2,X0,X1] : (~arg2(sK4(X0,X1),X2) | ~sub(X1,X0) | sP3(X1)) )),
  inference(duplicate_literal_removal,[],[f24165])).
fof(f24165,plain,(
  ( ! [X2,X0,X1] : (~arg2(sK4(X0,X1),X2) | sP3(X1) | ~sub(X1,X0) | ~sub(X1,X0)) )),
  inference(resolution,[],[f24164,f20637])).
fof(f20637,plain,(
  ( ! [X0,X1] : (arg1(sK4(X1,X0),X0) | ~sub(X0,X1)) )),
  inference(cnf_transformation,[],[f10557])).
fof(f24164,plain,(
  ( ! [X2,X0,X3,X1] : (~arg1(sK4(X0,X1),X3) | ~arg2(sK4(X0,X1),X2) | sP3(X3) | ~sub(X1,X0)) )),
  inference(resolution,[],[f24160,f20636])).
fof(f20636,plain,(
  ( ! [X0,X1] : (subr(sK4(X1,X0),sub_0) | ~sub(X0,X1)) )),
  inference(cnf_transformation,[],[f10557])).
fof(f24160,plain,(
  ( ! [X14,X12,X13] : (~subr(X12,sub_0) | ~arg2(X12,X14) | ~arg1(X12,X13) | sP3(X13)) )),
  inference(resolution,[],[f20675,f20897])).
fof(f20675,plain,(
  ( ! [X2,X0,X1] : (obj(sK13(X2,X1,X0),X1) | ~arg1(X0,X1) | ~arg2(X0,X2) | ~subr(X0,sub_0)) )),
  inference(cnf_transformation,[],[f10566])).
fof(f10566,plain,(
  ! [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))))),
  inference(skolemisation,[status(esa)],[f10386])).
fof(f10386,plain,(
  ! [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)))),
  inference(flattening,[],[f10385])).
fof(f10385,plain,(
  ! [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)))),
  inference(ennf_transformation,[],[f8031])).
fof(f8031,axiom,(
  ! [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)))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE084.p',sub__bezeichnen_1_1_als)).
fof(f21009_1,plain,(
  $false | $bdd2),
  inference(resolution,[],[f21006,f20994_1])).
fof(f20994_1,plain,(
  ( ! [X3] : (~sP4(X3)) ) | $bdd2),
  inference(definition_folding,[],[f20901,fbd2])).
fof(f21006,plain,(
  sP4(c8774)),
  inference(resolution,[],[f21005,f10671])).
fof(f21005,plain,(
  ( ! [X0] : (~attr(X0,c8775) | sP4(X0)) )),
  inference(subsumption_resolution,[],[f21004,f10608])).
fof(f21004,plain,(
  ( ! [X0] : (~sub(c8775,name_1_1) | ~attr(X0,c8775) | sP4(X0)) )),
  inference(resolution,[],[f20899,f10609])).
fof(f21003_1,plain,(
  $false | $bdd1),
  inference(resolution,[],[f20999,f20995_1])).
fof(f20995_1,plain,(
  ( ! [X5] : (~sP1(X5)) ) | $bdd1),
  inference(definition_folding,[],[f20895,fbd1])).
fof(f20999,plain,(
  sP1(c8774)),
  inference(resolution,[],[f20893,f10671])).
fof(f21002_1,plain,(
  $false | $bdd1),
  inference(resolution,[],[f20998,f20995_1])).
fof(f20998,plain,(
  sP1(c8778)),
  inference(resolution,[],[f20893,f10610])).
fof(f10610,plain,(
  attr(c8778,c8779)),
  inference(cnf_transformation,[],[f10230])).
fof(f21001_1,plain,(
  $false | $bdd1),
  inference(resolution,[],[f20997,f20995_1])).
fof(f20997,plain,(
  sP1(c8724)),
  inference(resolution,[],[f20893,f10677])).
fof(f10677,plain,(
  attr(c8724,c8725)),
  inference(cnf_transformation,[],[f10230])).
fof(f21000_1,plain,(
  $false | $bdd1),
  inference(resolution,[],[f20996,f20995_1])).
fof(f20996,plain,(
  sP1(c8713)),
  inference(resolution,[],[f20893,f10603])).
fof(f10603,plain,(
  attr(c8713,c8714)),
  inference(cnf_transformation,[],[f10230])).
% SZS output end Proof for FNE084
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Refutation

Active clauses: 13120
Passive clauses: 14973
Generated clauses: 15036
Final active clauses: 13120
Final passive clauses: 1840
Input formulas: 10189
Initial clauses: 10341

Pure predicates: 31

Duplicate literals: 22
Fw subsumption resolutions: 38

Simple tautologies: 1
Forward subsumptions: 17

Binary resolution: 4643

Unique components: 3
BDD propositional clauses: 6
SAT solver clauses: 6

Memory used: 57312KB
Time elapsed: 0.474 s
------------------------------
% Success in time 0.52 s

WATCH: 0.49 CPU 0.53 WC

FINAL WATCH: 0.49 CPU 0.53 WC