%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR115+38 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:45:37 AM UTC 2026
% Result : Theorem 7.76s 1.77s
% Output : Refutation 7.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 12
% Syntax : Number of formulae : 91 ( 20 unt; 8 def)
% Number of atoms : 2318 ( 0 equ)
% Maximal formula atoms : 286 ( 25 avg)
% Number of connectives : 2337 ( 110 ~; 118 |;2099 &)
% ( 8 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 286 ( 27 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 34 ( 33 usr; 9 prp; 0-8 aty)
% Number of functors : 83 ( 83 usr; 80 con; 0-3 aty)
% Number of variables : 119 ( 0 sgn 94 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f162,axiom,
! [X0,X1,X2] :
( ( arg1(X0,X1)
& arg2(X0,X2)
& subr(X0,sub_0) )
=> ? [X3,X4,X5] :
( arg1(X4,X1)
& arg2(X4,X5)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& sub(X5,X2)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax',sub__bezeichnen_1_1_als) ).
fof(f163,axiom,
! [X0,X1] :
( sub(X0,X1)
=> ? [X2] :
( arg1(X2,X0)
& arg2(X2,X1)
& subr(X2,sub_0) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax',sub__sub_0_expansion) ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6] :
( attr(X0,X1)
& attr(X3,X2)
& attr(X5,X6)
& obj(X4,X0)
& sub(X1,name_1_1)
& sub(X0,firma_1_1)
& sub(X2,name_1_1)
& val(X1,bmw_0)
& val(X2,bmw_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',synth_qa07_007_mira_news_1233) ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6] :
( attr(X0,X1)
& attr(X3,X2)
& attr(X5,X6)
& obj(X4,X0)
& sub(X1,name_1_1)
& sub(X0,firma_1_1)
& sub(X2,name_1_1)
& val(X1,bmw_0)
& val(X2,bmw_0) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,axiom,
( attr(c11,c12)
& sub(c11,stadt__1_1)
& sub(c12,name_1_1)
& val(c12,m__374nchen_0)
& attr(c17,c18)
& attr(c17,c19)
& sub(c18,tag_1_1)
& val(c18,c15)
& sub(c19,monat_1_1)
& val(c19,c16)
& prop(c2226,c2204)
& pred(c2230,maschinenfabrikant_1_1)
& prop(c2230,britisch__1_1)
& attr(c2836,c2837)
& sub(c2836,firma_1_1)
& sub(c2837,name_1_1)
& val(c2837,bmw_0)
& attr(c2840,c2841)
& sub(c2840,mensch_1_1)
& sub(c2841,familiename_1_1)
& val(c2841,roll_0)
& sub(c2842,gmbh__1_1)
& attr(c2844,c2845)
& sub(c2844,mensch_1_1)
& sub(c2845,familiename_1_1)
& val(c2845,royce_0)
& comp(c2868,fix_1_2,c2206)
& tupl(c31,c11,c17)
& tupl_p8(c3436,c2226,c2230,c2836,c2840,c2844,c2842,c2868)
& chsp2(gr__374nden_1_2,c2204)
& assoc(maschinenfabrikant_1_1,aggregat_1_1)
& sub(maschinenfabrikant_1_1,fabrikant_1_1)
& chsp2(planen_1_1,c2206)
& sort(c11,d)
& sort(c11,io)
& card(c11,int1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& quant(c11,one)
& refer(c11,det)
& varia(c11,con)
& sort(c12,na)
& card(c12,int1)
& etype(c12,int0)
& fact(c12,real)
& gener(c12,sp)
& quant(c12,one)
& refer(c12,indet)
& varia(c12,varia_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(name_1_1,na)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& sort(m__374nchen_0,fe)
& sort(c17,t)
& card(c17,int1)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& quant(c17,one)
& refer(c17,det)
& varia(c17,con)
& sort(c18,me)
& sort(c18,oa)
& sort(c18,ta)
& card(c18,card_c)
& etype(c18,etype_c)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,quant_c)
& refer(c18,refer_c)
& varia(c18,varia_c)
& sort(c19,me)
& sort(c19,oa)
& sort(c19,ta)
& card(c19,card_c)
& etype(c19,etype_c)
& fact(c19,real)
& gener(c19,sp)
& quant(c19,quant_c)
& refer(c19,refer_c)
& varia(c19,varia_c)
& sort(tag_1_1,me)
& sort(tag_1_1,oa)
& sort(tag_1_1,ta)
& card(tag_1_1,card_c)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& quant(tag_1_1,quant_c)
& refer(tag_1_1,refer_c)
& varia(tag_1_1,varia_c)
& sort(c15,nu)
& card(c15,int3)
& sort(monat_1_1,me)
& sort(monat_1_1,oa)
& sort(monat_1_1,ta)
& card(monat_1_1,card_c)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& quant(monat_1_1,quant_c)
& refer(monat_1_1,refer_c)
& varia(monat_1_1,varia_c)
& sort(c16,nu)
& card(c16,int5)
& sort(c2226,ab)
& card(c2226,int1990)
& etype(c2226,int1)
& fact(c2226,real)
& gener(c2226,gener_c)
& quant(c2226,nfquant)
& refer(c2226,refer_c)
& varia(c2226,varia_c)
& sort(c2204,tq)
& sort(c2230,d)
& sort(c2230,io)
& card(c2230,cons(x_constant,cons(int1,nil)))
& etype(c2230,int1)
& fact(c2230,real)
& gener(c2230,gener_c)
& quant(c2230,mult)
& refer(c2230,refer_c)
& varia(c2230,varia_c)
& sort(maschinenfabrikant_1_1,d)
& sort(maschinenfabrikant_1_1,io)
& card(maschinenfabrikant_1_1,int1)
& etype(maschinenfabrikant_1_1,int0)
& fact(maschinenfabrikant_1_1,real)
& gener(maschinenfabrikant_1_1,ge)
& quant(maschinenfabrikant_1_1,one)
& refer(maschinenfabrikant_1_1,refer_c)
& varia(maschinenfabrikant_1_1,varia_c)
& sort(britisch__1_1,nq)
& sort(c2836,d)
& sort(c2836,io)
& card(c2836,int1)
& etype(c2836,int0)
& fact(c2836,real)
& gener(c2836,sp)
& quant(c2836,one)
& refer(c2836,det)
& varia(c2836,con)
& sort(c2837,na)
& card(c2837,int1)
& etype(c2837,int0)
& fact(c2837,real)
& gener(c2837,sp)
& quant(c2837,one)
& refer(c2837,indet)
& varia(c2837,varia_c)
& sort(firma_1_1,d)
& sort(firma_1_1,io)
& card(firma_1_1,int1)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& quant(firma_1_1,one)
& refer(firma_1_1,refer_c)
& varia(firma_1_1,varia_c)
& sort(bmw_0,fe)
& sort(c2840,d)
& card(c2840,int1)
& etype(c2840,int0)
& fact(c2840,real)
& gener(c2840,sp)
& quant(c2840,one)
& refer(c2840,det)
& varia(c2840,con)
& sort(c2841,na)
& card(c2841,int1)
& etype(c2841,int0)
& fact(c2841,real)
& gener(c2841,sp)
& quant(c2841,one)
& refer(c2841,indet)
& varia(c2841,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& sort(familiename_1_1,na)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& sort(roll_0,fe)
& sort(c2842,d)
& sort(c2842,io)
& card(c2842,int1)
& etype(c2842,int1)
& fact(c2842,real)
& gener(c2842,gener_c)
& quant(c2842,one)
& refer(c2842,refer_c)
& varia(c2842,varia_c)
& sort(gmbh__1_1,d)
& sort(gmbh__1_1,io)
& card(gmbh__1_1,card_c)
& etype(gmbh__1_1,int1)
& fact(gmbh__1_1,real)
& gener(gmbh__1_1,ge)
& quant(gmbh__1_1,quant_c)
& refer(gmbh__1_1,refer_c)
& varia(gmbh__1_1,varia_c)
& sort(c2844,d)
& card(c2844,int1)
& etype(c2844,int0)
& fact(c2844,real)
& gener(c2844,sp)
& quant(c2844,one)
& refer(c2844,det)
& varia(c2844,con)
& sort(c2845,na)
& card(c2845,int1)
& etype(c2845,int0)
& fact(c2845,real)
& gener(c2845,sp)
& quant(c2845,one)
& refer(c2845,indet)
& varia(c2845,varia_c)
& sort(royce_0,fe)
& sort(c2868,tq)
& sort(fix_1_2,mq)
& sort(c2206,tq)
& sort(c31,ent)
& card(c31,card_c)
& etype(c31,etype_c)
& fact(c31,real)
& gener(c31,gener_c)
& quant(c31,quant_c)
& refer(c31,refer_c)
& varia(c31,varia_c)
& sort(c3436,ent)
& card(c3436,card_c)
& etype(c3436,etype_c)
& fact(c3436,real)
& gener(c3436,gener_c)
& quant(c3436,quant_c)
& refer(c3436,refer_c)
& varia(c3436,varia_c)
& sort(gr__374nden_1_2,da)
& fact(gr__374nden_1_2,real)
& gener(gr__374nden_1_2,ge)
& sort(aggregat_1_1,d)
& sort(aggregat_1_1,io)
& card(aggregat_1_1,int1)
& etype(aggregat_1_1,int0)
& fact(aggregat_1_1,real)
& gener(aggregat_1_1,ge)
& quant(aggregat_1_1,one)
& refer(aggregat_1_1,refer_c)
& varia(aggregat_1_1,varia_c)
& sort(fabrikant_1_1,d)
& sort(fabrikant_1_1,io)
& card(fabrikant_1_1,int1)
& etype(fabrikant_1_1,int0)
& fact(fabrikant_1_1,real)
& gener(fabrikant_1_1,ge)
& quant(fabrikant_1_1,one)
& refer(fabrikant_1_1,refer_c)
& varia(fabrikant_1_1,varia_c)
& sort(planen_1_1,da)
& fact(planen_1_1,real)
& gener(planen_1_1,ge) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ave07_era5_synth_qa07_007_mira_news_1233) ).
fof(f10191,plain,
( attr(c11,c12)
& sub(c11,stadt__1_1)
& sub(c12,name_1_1)
& val(c12,m__374nchen_0)
& attr(c17,c18)
& attr(c17,c19)
& sub(c18,tag_1_1)
& val(c18,c15)
& sub(c19,monat_1_1)
& val(c19,c16)
& prop(c2226,c2204)
& pred(c2230,maschinenfabrikant_1_1)
& prop(c2230,britisch__1_1)
& attr(c2836,c2837)
& sub(c2836,firma_1_1)
& sub(c2837,name_1_1)
& val(c2837,bmw_0)
& attr(c2840,c2841)
& sub(c2840,mensch_1_1)
& sub(c2841,familiename_1_1)
& val(c2841,roll_0)
& sub(c2842,gmbh__1_1)
& attr(c2844,c2845)
& sub(c2844,mensch_1_1)
& sub(c2845,familiename_1_1)
& val(c2845,royce_0)
& comp(c2868,fix_1_2,c2206)
& tupl(c31,c11,c17)
& chsp2(gr__374nden_1_2,c2204)
& assoc(maschinenfabrikant_1_1,aggregat_1_1)
& sub(maschinenfabrikant_1_1,fabrikant_1_1)
& chsp2(planen_1_1,c2206)
& sort(c11,d)
& sort(c11,io)
& card(c11,int1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& quant(c11,one)
& refer(c11,det)
& varia(c11,con)
& sort(c12,na)
& card(c12,int1)
& etype(c12,int0)
& fact(c12,real)
& gener(c12,sp)
& quant(c12,one)
& refer(c12,indet)
& varia(c12,varia_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(name_1_1,na)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& sort(m__374nchen_0,fe)
& sort(c17,t)
& card(c17,int1)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& quant(c17,one)
& refer(c17,det)
& varia(c17,con)
& sort(c18,me)
& sort(c18,oa)
& sort(c18,ta)
& card(c18,card_c)
& etype(c18,etype_c)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,quant_c)
& refer(c18,refer_c)
& varia(c18,varia_c)
& sort(c19,me)
& sort(c19,oa)
& sort(c19,ta)
& card(c19,card_c)
& etype(c19,etype_c)
& fact(c19,real)
& gener(c19,sp)
& quant(c19,quant_c)
& refer(c19,refer_c)
& varia(c19,varia_c)
& sort(tag_1_1,me)
& sort(tag_1_1,oa)
& sort(tag_1_1,ta)
& card(tag_1_1,card_c)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& quant(tag_1_1,quant_c)
& refer(tag_1_1,refer_c)
& varia(tag_1_1,varia_c)
& sort(c15,nu)
& card(c15,int3)
& sort(monat_1_1,me)
& sort(monat_1_1,oa)
& sort(monat_1_1,ta)
& card(monat_1_1,card_c)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& quant(monat_1_1,quant_c)
& refer(monat_1_1,refer_c)
& varia(monat_1_1,varia_c)
& sort(c16,nu)
& card(c16,int5)
& sort(c2226,ab)
& card(c2226,int1990)
& etype(c2226,int1)
& fact(c2226,real)
& gener(c2226,gener_c)
& quant(c2226,nfquant)
& refer(c2226,refer_c)
& varia(c2226,varia_c)
& sort(c2204,tq)
& sort(c2230,d)
& sort(c2230,io)
& card(c2230,cons(x_constant,cons(int1,nil)))
& etype(c2230,int1)
& fact(c2230,real)
& gener(c2230,gener_c)
& quant(c2230,mult)
& refer(c2230,refer_c)
& varia(c2230,varia_c)
& sort(maschinenfabrikant_1_1,d)
& sort(maschinenfabrikant_1_1,io)
& card(maschinenfabrikant_1_1,int1)
& etype(maschinenfabrikant_1_1,int0)
& fact(maschinenfabrikant_1_1,real)
& gener(maschinenfabrikant_1_1,ge)
& quant(maschinenfabrikant_1_1,one)
& refer(maschinenfabrikant_1_1,refer_c)
& varia(maschinenfabrikant_1_1,varia_c)
& sort(britisch__1_1,nq)
& sort(c2836,d)
& sort(c2836,io)
& card(c2836,int1)
& etype(c2836,int0)
& fact(c2836,real)
& gener(c2836,sp)
& quant(c2836,one)
& refer(c2836,det)
& varia(c2836,con)
& sort(c2837,na)
& card(c2837,int1)
& etype(c2837,int0)
& fact(c2837,real)
& gener(c2837,sp)
& quant(c2837,one)
& refer(c2837,indet)
& varia(c2837,varia_c)
& sort(firma_1_1,d)
& sort(firma_1_1,io)
& card(firma_1_1,int1)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& quant(firma_1_1,one)
& refer(firma_1_1,refer_c)
& varia(firma_1_1,varia_c)
& sort(bmw_0,fe)
& sort(c2840,d)
& card(c2840,int1)
& etype(c2840,int0)
& fact(c2840,real)
& gener(c2840,sp)
& quant(c2840,one)
& refer(c2840,det)
& varia(c2840,con)
& sort(c2841,na)
& card(c2841,int1)
& etype(c2841,int0)
& fact(c2841,real)
& gener(c2841,sp)
& quant(c2841,one)
& refer(c2841,indet)
& varia(c2841,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& sort(familiename_1_1,na)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& sort(roll_0,fe)
& sort(c2842,d)
& sort(c2842,io)
& card(c2842,int1)
& etype(c2842,int1)
& fact(c2842,real)
& gener(c2842,gener_c)
& quant(c2842,one)
& refer(c2842,refer_c)
& varia(c2842,varia_c)
& sort(gmbh__1_1,d)
& sort(gmbh__1_1,io)
& card(gmbh__1_1,card_c)
& etype(gmbh__1_1,int1)
& fact(gmbh__1_1,real)
& gener(gmbh__1_1,ge)
& quant(gmbh__1_1,quant_c)
& refer(gmbh__1_1,refer_c)
& varia(gmbh__1_1,varia_c)
& sort(c2844,d)
& card(c2844,int1)
& etype(c2844,int0)
& fact(c2844,real)
& gener(c2844,sp)
& quant(c2844,one)
& refer(c2844,det)
& varia(c2844,con)
& sort(c2845,na)
& card(c2845,int1)
& etype(c2845,int0)
& fact(c2845,real)
& gener(c2845,sp)
& quant(c2845,one)
& refer(c2845,indet)
& varia(c2845,varia_c)
& sort(royce_0,fe)
& sort(c2868,tq)
& sort(fix_1_2,mq)
& sort(c2206,tq)
& sort(c31,ent)
& card(c31,card_c)
& etype(c31,etype_c)
& fact(c31,real)
& gener(c31,gener_c)
& quant(c31,quant_c)
& refer(c31,refer_c)
& varia(c31,varia_c)
& sort(c3436,ent)
& card(c3436,card_c)
& etype(c3436,etype_c)
& fact(c3436,real)
& gener(c3436,gener_c)
& quant(c3436,quant_c)
& refer(c3436,refer_c)
& varia(c3436,varia_c)
& sort(gr__374nden_1_2,da)
& fact(gr__374nden_1_2,real)
& gener(gr__374nden_1_2,ge)
& sort(aggregat_1_1,d)
& sort(aggregat_1_1,io)
& card(aggregat_1_1,int1)
& etype(aggregat_1_1,int0)
& fact(aggregat_1_1,real)
& gener(aggregat_1_1,ge)
& quant(aggregat_1_1,one)
& refer(aggregat_1_1,refer_c)
& varia(aggregat_1_1,varia_c)
& sort(fabrikant_1_1,d)
& sort(fabrikant_1_1,io)
& card(fabrikant_1_1,int1)
& etype(fabrikant_1_1,int0)
& fact(fabrikant_1_1,real)
& gener(fabrikant_1_1,ge)
& quant(fabrikant_1_1,one)
& refer(fabrikant_1_1,refer_c)
& varia(fabrikant_1_1,varia_c)
& sort(planen_1_1,da)
& fact(planen_1_1,real)
& gener(planen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10192,plain,
( attr(c11,c12)
& sub(c11,stadt__1_1)
& sub(c12,name_1_1)
& val(c12,m__374nchen_0)
& attr(c17,c18)
& attr(c17,c19)
& sub(c18,tag_1_1)
& val(c18,c15)
& sub(c19,monat_1_1)
& val(c19,c16)
& prop(c2226,c2204)
& pred(c2230,maschinenfabrikant_1_1)
& prop(c2230,britisch__1_1)
& attr(c2836,c2837)
& sub(c2836,firma_1_1)
& sub(c2837,name_1_1)
& val(c2837,bmw_0)
& attr(c2840,c2841)
& sub(c2840,mensch_1_1)
& sub(c2841,familiename_1_1)
& val(c2841,roll_0)
& sub(c2842,gmbh__1_1)
& attr(c2844,c2845)
& sub(c2844,mensch_1_1)
& sub(c2845,familiename_1_1)
& val(c2845,royce_0)
& tupl(c31,c11,c17)
& chsp2(gr__374nden_1_2,c2204)
& assoc(maschinenfabrikant_1_1,aggregat_1_1)
& sub(maschinenfabrikant_1_1,fabrikant_1_1)
& chsp2(planen_1_1,c2206)
& sort(c11,d)
& sort(c11,io)
& card(c11,int1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& quant(c11,one)
& refer(c11,det)
& varia(c11,con)
& sort(c12,na)
& card(c12,int1)
& etype(c12,int0)
& fact(c12,real)
& gener(c12,sp)
& quant(c12,one)
& refer(c12,indet)
& varia(c12,varia_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(name_1_1,na)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& sort(m__374nchen_0,fe)
& sort(c17,t)
& card(c17,int1)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& quant(c17,one)
& refer(c17,det)
& varia(c17,con)
& sort(c18,me)
& sort(c18,oa)
& sort(c18,ta)
& card(c18,card_c)
& etype(c18,etype_c)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,quant_c)
& refer(c18,refer_c)
& varia(c18,varia_c)
& sort(c19,me)
& sort(c19,oa)
& sort(c19,ta)
& card(c19,card_c)
& etype(c19,etype_c)
& fact(c19,real)
& gener(c19,sp)
& quant(c19,quant_c)
& refer(c19,refer_c)
& varia(c19,varia_c)
& sort(tag_1_1,me)
& sort(tag_1_1,oa)
& sort(tag_1_1,ta)
& card(tag_1_1,card_c)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& quant(tag_1_1,quant_c)
& refer(tag_1_1,refer_c)
& varia(tag_1_1,varia_c)
& sort(c15,nu)
& card(c15,int3)
& sort(monat_1_1,me)
& sort(monat_1_1,oa)
& sort(monat_1_1,ta)
& card(monat_1_1,card_c)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& quant(monat_1_1,quant_c)
& refer(monat_1_1,refer_c)
& varia(monat_1_1,varia_c)
& sort(c16,nu)
& card(c16,int5)
& sort(c2226,ab)
& card(c2226,int1990)
& etype(c2226,int1)
& fact(c2226,real)
& gener(c2226,gener_c)
& quant(c2226,nfquant)
& refer(c2226,refer_c)
& varia(c2226,varia_c)
& sort(c2204,tq)
& sort(c2230,d)
& sort(c2230,io)
& card(c2230,cons(x_constant,cons(int1,nil)))
& etype(c2230,int1)
& fact(c2230,real)
& gener(c2230,gener_c)
& quant(c2230,mult)
& refer(c2230,refer_c)
& varia(c2230,varia_c)
& sort(maschinenfabrikant_1_1,d)
& sort(maschinenfabrikant_1_1,io)
& card(maschinenfabrikant_1_1,int1)
& etype(maschinenfabrikant_1_1,int0)
& fact(maschinenfabrikant_1_1,real)
& gener(maschinenfabrikant_1_1,ge)
& quant(maschinenfabrikant_1_1,one)
& refer(maschinenfabrikant_1_1,refer_c)
& varia(maschinenfabrikant_1_1,varia_c)
& sort(britisch__1_1,nq)
& sort(c2836,d)
& sort(c2836,io)
& card(c2836,int1)
& etype(c2836,int0)
& fact(c2836,real)
& gener(c2836,sp)
& quant(c2836,one)
& refer(c2836,det)
& varia(c2836,con)
& sort(c2837,na)
& card(c2837,int1)
& etype(c2837,int0)
& fact(c2837,real)
& gener(c2837,sp)
& quant(c2837,one)
& refer(c2837,indet)
& varia(c2837,varia_c)
& sort(firma_1_1,d)
& sort(firma_1_1,io)
& card(firma_1_1,int1)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& quant(firma_1_1,one)
& refer(firma_1_1,refer_c)
& varia(firma_1_1,varia_c)
& sort(bmw_0,fe)
& sort(c2840,d)
& card(c2840,int1)
& etype(c2840,int0)
& fact(c2840,real)
& gener(c2840,sp)
& quant(c2840,one)
& refer(c2840,det)
& varia(c2840,con)
& sort(c2841,na)
& card(c2841,int1)
& etype(c2841,int0)
& fact(c2841,real)
& gener(c2841,sp)
& quant(c2841,one)
& refer(c2841,indet)
& varia(c2841,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& sort(familiename_1_1,na)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& sort(roll_0,fe)
& sort(c2842,d)
& sort(c2842,io)
& card(c2842,int1)
& etype(c2842,int1)
& fact(c2842,real)
& gener(c2842,gener_c)
& quant(c2842,one)
& refer(c2842,refer_c)
& varia(c2842,varia_c)
& sort(gmbh__1_1,d)
& sort(gmbh__1_1,io)
& card(gmbh__1_1,card_c)
& etype(gmbh__1_1,int1)
& fact(gmbh__1_1,real)
& gener(gmbh__1_1,ge)
& quant(gmbh__1_1,quant_c)
& refer(gmbh__1_1,refer_c)
& varia(gmbh__1_1,varia_c)
& sort(c2844,d)
& card(c2844,int1)
& etype(c2844,int0)
& fact(c2844,real)
& gener(c2844,sp)
& quant(c2844,one)
& refer(c2844,det)
& varia(c2844,con)
& sort(c2845,na)
& card(c2845,int1)
& etype(c2845,int0)
& fact(c2845,real)
& gener(c2845,sp)
& quant(c2845,one)
& refer(c2845,indet)
& varia(c2845,varia_c)
& sort(royce_0,fe)
& sort(c2868,tq)
& sort(fix_1_2,mq)
& sort(c2206,tq)
& sort(c31,ent)
& card(c31,card_c)
& etype(c31,etype_c)
& fact(c31,real)
& gener(c31,gener_c)
& quant(c31,quant_c)
& refer(c31,refer_c)
& varia(c31,varia_c)
& sort(c3436,ent)
& card(c3436,card_c)
& etype(c3436,etype_c)
& fact(c3436,real)
& gener(c3436,gener_c)
& quant(c3436,quant_c)
& refer(c3436,refer_c)
& varia(c3436,varia_c)
& sort(gr__374nden_1_2,da)
& fact(gr__374nden_1_2,real)
& gener(gr__374nden_1_2,ge)
& sort(aggregat_1_1,d)
& sort(aggregat_1_1,io)
& card(aggregat_1_1,int1)
& etype(aggregat_1_1,int0)
& fact(aggregat_1_1,real)
& gener(aggregat_1_1,ge)
& quant(aggregat_1_1,one)
& refer(aggregat_1_1,refer_c)
& varia(aggregat_1_1,varia_c)
& sort(fabrikant_1_1,d)
& sort(fabrikant_1_1,io)
& card(fabrikant_1_1,int1)
& etype(fabrikant_1_1,int0)
& fact(fabrikant_1_1,real)
& gener(fabrikant_1_1,ge)
& quant(fabrikant_1_1,one)
& refer(fabrikant_1_1,refer_c)
& varia(fabrikant_1_1,varia_c)
& sort(planen_1_1,da)
& fact(planen_1_1,real)
& gener(planen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10322,plain,
( attr(c11,c12)
& sub(c11,stadt__1_1)
& sub(c12,name_1_1)
& val(c12,m__374nchen_0)
& attr(c17,c18)
& attr(c17,c19)
& sub(c18,tag_1_1)
& val(c18,c15)
& sub(c19,monat_1_1)
& val(c19,c16)
& prop(c2226,c2204)
& pred(c2230,maschinenfabrikant_1_1)
& prop(c2230,britisch__1_1)
& attr(c2836,c2837)
& sub(c2836,firma_1_1)
& sub(c2837,name_1_1)
& val(c2837,bmw_0)
& attr(c2840,c2841)
& sub(c2840,mensch_1_1)
& sub(c2841,familiename_1_1)
& val(c2841,roll_0)
& sub(c2842,gmbh__1_1)
& attr(c2844,c2845)
& sub(c2844,mensch_1_1)
& sub(c2845,familiename_1_1)
& val(c2845,royce_0)
& tupl(c31,c11,c17)
& assoc(maschinenfabrikant_1_1,aggregat_1_1)
& sub(maschinenfabrikant_1_1,fabrikant_1_1)
& sort(c11,d)
& sort(c11,io)
& card(c11,int1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& quant(c11,one)
& refer(c11,det)
& varia(c11,con)
& sort(c12,na)
& card(c12,int1)
& etype(c12,int0)
& fact(c12,real)
& gener(c12,sp)
& quant(c12,one)
& refer(c12,indet)
& varia(c12,varia_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(name_1_1,na)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& sort(m__374nchen_0,fe)
& sort(c17,t)
& card(c17,int1)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& quant(c17,one)
& refer(c17,det)
& varia(c17,con)
& sort(c18,me)
& sort(c18,oa)
& sort(c18,ta)
& card(c18,card_c)
& etype(c18,etype_c)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,quant_c)
& refer(c18,refer_c)
& varia(c18,varia_c)
& sort(c19,me)
& sort(c19,oa)
& sort(c19,ta)
& card(c19,card_c)
& etype(c19,etype_c)
& fact(c19,real)
& gener(c19,sp)
& quant(c19,quant_c)
& refer(c19,refer_c)
& varia(c19,varia_c)
& sort(tag_1_1,me)
& sort(tag_1_1,oa)
& sort(tag_1_1,ta)
& card(tag_1_1,card_c)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& quant(tag_1_1,quant_c)
& refer(tag_1_1,refer_c)
& varia(tag_1_1,varia_c)
& sort(c15,nu)
& card(c15,int3)
& sort(monat_1_1,me)
& sort(monat_1_1,oa)
& sort(monat_1_1,ta)
& card(monat_1_1,card_c)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& quant(monat_1_1,quant_c)
& refer(monat_1_1,refer_c)
& varia(monat_1_1,varia_c)
& sort(c16,nu)
& card(c16,int5)
& sort(c2226,ab)
& card(c2226,int1990)
& etype(c2226,int1)
& fact(c2226,real)
& gener(c2226,gener_c)
& quant(c2226,nfquant)
& refer(c2226,refer_c)
& varia(c2226,varia_c)
& sort(c2204,tq)
& sort(c2230,d)
& sort(c2230,io)
& card(c2230,cons(x_constant,cons(int1,nil)))
& etype(c2230,int1)
& fact(c2230,real)
& gener(c2230,gener_c)
& quant(c2230,mult)
& refer(c2230,refer_c)
& varia(c2230,varia_c)
& sort(maschinenfabrikant_1_1,d)
& sort(maschinenfabrikant_1_1,io)
& card(maschinenfabrikant_1_1,int1)
& etype(maschinenfabrikant_1_1,int0)
& fact(maschinenfabrikant_1_1,real)
& gener(maschinenfabrikant_1_1,ge)
& quant(maschinenfabrikant_1_1,one)
& refer(maschinenfabrikant_1_1,refer_c)
& varia(maschinenfabrikant_1_1,varia_c)
& sort(britisch__1_1,nq)
& sort(c2836,d)
& sort(c2836,io)
& card(c2836,int1)
& etype(c2836,int0)
& fact(c2836,real)
& gener(c2836,sp)
& quant(c2836,one)
& refer(c2836,det)
& varia(c2836,con)
& sort(c2837,na)
& card(c2837,int1)
& etype(c2837,int0)
& fact(c2837,real)
& gener(c2837,sp)
& quant(c2837,one)
& refer(c2837,indet)
& varia(c2837,varia_c)
& sort(firma_1_1,d)
& sort(firma_1_1,io)
& card(firma_1_1,int1)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& quant(firma_1_1,one)
& refer(firma_1_1,refer_c)
& varia(firma_1_1,varia_c)
& sort(bmw_0,fe)
& sort(c2840,d)
& card(c2840,int1)
& etype(c2840,int0)
& fact(c2840,real)
& gener(c2840,sp)
& quant(c2840,one)
& refer(c2840,det)
& varia(c2840,con)
& sort(c2841,na)
& card(c2841,int1)
& etype(c2841,int0)
& fact(c2841,real)
& gener(c2841,sp)
& quant(c2841,one)
& refer(c2841,indet)
& varia(c2841,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& sort(familiename_1_1,na)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& sort(roll_0,fe)
& sort(c2842,d)
& sort(c2842,io)
& card(c2842,int1)
& etype(c2842,int1)
& fact(c2842,real)
& gener(c2842,gener_c)
& quant(c2842,one)
& refer(c2842,refer_c)
& varia(c2842,varia_c)
& sort(gmbh__1_1,d)
& sort(gmbh__1_1,io)
& card(gmbh__1_1,card_c)
& etype(gmbh__1_1,int1)
& fact(gmbh__1_1,real)
& gener(gmbh__1_1,ge)
& quant(gmbh__1_1,quant_c)
& refer(gmbh__1_1,refer_c)
& varia(gmbh__1_1,varia_c)
& sort(c2844,d)
& card(c2844,int1)
& etype(c2844,int0)
& fact(c2844,real)
& gener(c2844,sp)
& quant(c2844,one)
& refer(c2844,det)
& varia(c2844,con)
& sort(c2845,na)
& card(c2845,int1)
& etype(c2845,int0)
& fact(c2845,real)
& gener(c2845,sp)
& quant(c2845,one)
& refer(c2845,indet)
& varia(c2845,varia_c)
& sort(royce_0,fe)
& sort(c2868,tq)
& sort(fix_1_2,mq)
& sort(c2206,tq)
& sort(c31,ent)
& card(c31,card_c)
& etype(c31,etype_c)
& fact(c31,real)
& gener(c31,gener_c)
& quant(c31,quant_c)
& refer(c31,refer_c)
& varia(c31,varia_c)
& sort(c3436,ent)
& card(c3436,card_c)
& etype(c3436,etype_c)
& fact(c3436,real)
& gener(c3436,gener_c)
& quant(c3436,quant_c)
& refer(c3436,refer_c)
& varia(c3436,varia_c)
& sort(gr__374nden_1_2,da)
& fact(gr__374nden_1_2,real)
& gener(gr__374nden_1_2,ge)
& sort(aggregat_1_1,d)
& sort(aggregat_1_1,io)
& card(aggregat_1_1,int1)
& etype(aggregat_1_1,int0)
& fact(aggregat_1_1,real)
& gener(aggregat_1_1,ge)
& quant(aggregat_1_1,one)
& refer(aggregat_1_1,refer_c)
& varia(aggregat_1_1,varia_c)
& sort(fabrikant_1_1,d)
& sort(fabrikant_1_1,io)
& card(fabrikant_1_1,int1)
& etype(fabrikant_1_1,int0)
& fact(fabrikant_1_1,real)
& gener(fabrikant_1_1,ge)
& quant(fabrikant_1_1,one)
& refer(fabrikant_1_1,refer_c)
& varia(fabrikant_1_1,varia_c)
& sort(planen_1_1,da)
& fact(planen_1_1,real)
& gener(planen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10192]) ).
fof(f10328,plain,
( attr(c11,c12)
& sub(c11,stadt__1_1)
& sub(c12,name_1_1)
& val(c12,m__374nchen_0)
& attr(c17,c18)
& attr(c17,c19)
& sub(c18,tag_1_1)
& val(c18,c15)
& sub(c19,monat_1_1)
& val(c19,c16)
& prop(c2226,c2204)
& pred(c2230,maschinenfabrikant_1_1)
& prop(c2230,britisch__1_1)
& attr(c2836,c2837)
& sub(c2836,firma_1_1)
& sub(c2837,name_1_1)
& val(c2837,bmw_0)
& attr(c2840,c2841)
& sub(c2840,mensch_1_1)
& sub(c2841,familiename_1_1)
& val(c2841,roll_0)
& sub(c2842,gmbh__1_1)
& attr(c2844,c2845)
& sub(c2844,mensch_1_1)
& sub(c2845,familiename_1_1)
& val(c2845,royce_0)
& tupl(c31,c11,c17)
& assoc(maschinenfabrikant_1_1,aggregat_1_1)
& sub(maschinenfabrikant_1_1,fabrikant_1_1)
& card(c11,int1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& quant(c11,one)
& refer(c11,det)
& varia(c11,con)
& card(c12,int1)
& etype(c12,int0)
& fact(c12,real)
& gener(c12,sp)
& quant(c12,one)
& refer(c12,indet)
& varia(c12,varia_c)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& card(c17,int1)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& quant(c17,one)
& refer(c17,det)
& varia(c17,con)
& card(c18,card_c)
& etype(c18,etype_c)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,quant_c)
& refer(c18,refer_c)
& varia(c18,varia_c)
& card(c19,card_c)
& etype(c19,etype_c)
& fact(c19,real)
& gener(c19,sp)
& quant(c19,quant_c)
& refer(c19,refer_c)
& varia(c19,varia_c)
& card(tag_1_1,card_c)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& quant(tag_1_1,quant_c)
& refer(tag_1_1,refer_c)
& varia(tag_1_1,varia_c)
& card(c15,int3)
& card(monat_1_1,card_c)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& quant(monat_1_1,quant_c)
& refer(monat_1_1,refer_c)
& varia(monat_1_1,varia_c)
& card(c16,int5)
& card(c2226,int1990)
& etype(c2226,int1)
& fact(c2226,real)
& gener(c2226,gener_c)
& quant(c2226,nfquant)
& refer(c2226,refer_c)
& varia(c2226,varia_c)
& card(c2230,cons(x_constant,cons(int1,nil)))
& etype(c2230,int1)
& fact(c2230,real)
& gener(c2230,gener_c)
& quant(c2230,mult)
& refer(c2230,refer_c)
& varia(c2230,varia_c)
& card(maschinenfabrikant_1_1,int1)
& etype(maschinenfabrikant_1_1,int0)
& fact(maschinenfabrikant_1_1,real)
& gener(maschinenfabrikant_1_1,ge)
& quant(maschinenfabrikant_1_1,one)
& refer(maschinenfabrikant_1_1,refer_c)
& varia(maschinenfabrikant_1_1,varia_c)
& card(c2836,int1)
& etype(c2836,int0)
& fact(c2836,real)
& gener(c2836,sp)
& quant(c2836,one)
& refer(c2836,det)
& varia(c2836,con)
& card(c2837,int1)
& etype(c2837,int0)
& fact(c2837,real)
& gener(c2837,sp)
& quant(c2837,one)
& refer(c2837,indet)
& varia(c2837,varia_c)
& card(firma_1_1,int1)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& quant(firma_1_1,one)
& refer(firma_1_1,refer_c)
& varia(firma_1_1,varia_c)
& card(c2840,int1)
& etype(c2840,int0)
& fact(c2840,real)
& gener(c2840,sp)
& quant(c2840,one)
& refer(c2840,det)
& varia(c2840,con)
& card(c2841,int1)
& etype(c2841,int0)
& fact(c2841,real)
& gener(c2841,sp)
& quant(c2841,one)
& refer(c2841,indet)
& varia(c2841,varia_c)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& card(c2842,int1)
& etype(c2842,int1)
& fact(c2842,real)
& gener(c2842,gener_c)
& quant(c2842,one)
& refer(c2842,refer_c)
& varia(c2842,varia_c)
& card(gmbh__1_1,card_c)
& etype(gmbh__1_1,int1)
& fact(gmbh__1_1,real)
& gener(gmbh__1_1,ge)
& quant(gmbh__1_1,quant_c)
& refer(gmbh__1_1,refer_c)
& varia(gmbh__1_1,varia_c)
& card(c2844,int1)
& etype(c2844,int0)
& fact(c2844,real)
& gener(c2844,sp)
& quant(c2844,one)
& refer(c2844,det)
& varia(c2844,con)
& card(c2845,int1)
& etype(c2845,int0)
& fact(c2845,real)
& gener(c2845,sp)
& quant(c2845,one)
& refer(c2845,indet)
& varia(c2845,varia_c)
& card(c31,card_c)
& etype(c31,etype_c)
& fact(c31,real)
& gener(c31,gener_c)
& quant(c31,quant_c)
& refer(c31,refer_c)
& varia(c31,varia_c)
& card(c3436,card_c)
& etype(c3436,etype_c)
& fact(c3436,real)
& gener(c3436,gener_c)
& quant(c3436,quant_c)
& refer(c3436,refer_c)
& varia(c3436,varia_c)
& fact(gr__374nden_1_2,real)
& gener(gr__374nden_1_2,ge)
& card(aggregat_1_1,int1)
& etype(aggregat_1_1,int0)
& fact(aggregat_1_1,real)
& gener(aggregat_1_1,ge)
& quant(aggregat_1_1,one)
& refer(aggregat_1_1,refer_c)
& varia(aggregat_1_1,varia_c)
& card(fabrikant_1_1,int1)
& etype(fabrikant_1_1,int0)
& fact(fabrikant_1_1,real)
& gener(fabrikant_1_1,ge)
& quant(fabrikant_1_1,one)
& refer(fabrikant_1_1,refer_c)
& varia(fabrikant_1_1,varia_c)
& fact(planen_1_1,real)
& gener(planen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10322]) ).
fof(f10331,plain,
( attr(c11,c12)
& sub(c11,stadt__1_1)
& sub(c12,name_1_1)
& val(c12,m__374nchen_0)
& attr(c17,c18)
& attr(c17,c19)
& sub(c18,tag_1_1)
& val(c18,c15)
& sub(c19,monat_1_1)
& val(c19,c16)
& prop(c2226,c2204)
& pred(c2230,maschinenfabrikant_1_1)
& prop(c2230,britisch__1_1)
& attr(c2836,c2837)
& sub(c2836,firma_1_1)
& sub(c2837,name_1_1)
& val(c2837,bmw_0)
& attr(c2840,c2841)
& sub(c2840,mensch_1_1)
& sub(c2841,familiename_1_1)
& val(c2841,roll_0)
& sub(c2842,gmbh__1_1)
& attr(c2844,c2845)
& sub(c2844,mensch_1_1)
& sub(c2845,familiename_1_1)
& val(c2845,royce_0)
& tupl(c31,c11,c17)
& assoc(maschinenfabrikant_1_1,aggregat_1_1)
& sub(maschinenfabrikant_1_1,fabrikant_1_1)
& card(c11,int1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& refer(c11,det)
& varia(c11,con)
& card(c12,int1)
& etype(c12,int0)
& fact(c12,real)
& gener(c12,sp)
& refer(c12,indet)
& varia(c12,varia_c)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& card(c17,int1)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& refer(c17,det)
& varia(c17,con)
& card(c18,card_c)
& etype(c18,etype_c)
& fact(c18,real)
& gener(c18,sp)
& refer(c18,refer_c)
& varia(c18,varia_c)
& card(c19,card_c)
& etype(c19,etype_c)
& fact(c19,real)
& gener(c19,sp)
& refer(c19,refer_c)
& varia(c19,varia_c)
& card(tag_1_1,card_c)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& refer(tag_1_1,refer_c)
& varia(tag_1_1,varia_c)
& card(c15,int3)
& card(monat_1_1,card_c)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& refer(monat_1_1,refer_c)
& varia(monat_1_1,varia_c)
& card(c16,int5)
& card(c2226,int1990)
& etype(c2226,int1)
& fact(c2226,real)
& gener(c2226,gener_c)
& refer(c2226,refer_c)
& varia(c2226,varia_c)
& card(c2230,cons(x_constant,cons(int1,nil)))
& etype(c2230,int1)
& fact(c2230,real)
& gener(c2230,gener_c)
& refer(c2230,refer_c)
& varia(c2230,varia_c)
& card(maschinenfabrikant_1_1,int1)
& etype(maschinenfabrikant_1_1,int0)
& fact(maschinenfabrikant_1_1,real)
& gener(maschinenfabrikant_1_1,ge)
& refer(maschinenfabrikant_1_1,refer_c)
& varia(maschinenfabrikant_1_1,varia_c)
& card(c2836,int1)
& etype(c2836,int0)
& fact(c2836,real)
& gener(c2836,sp)
& refer(c2836,det)
& varia(c2836,con)
& card(c2837,int1)
& etype(c2837,int0)
& fact(c2837,real)
& gener(c2837,sp)
& refer(c2837,indet)
& varia(c2837,varia_c)
& card(firma_1_1,int1)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& refer(firma_1_1,refer_c)
& varia(firma_1_1,varia_c)
& card(c2840,int1)
& etype(c2840,int0)
& fact(c2840,real)
& gener(c2840,sp)
& refer(c2840,det)
& varia(c2840,con)
& card(c2841,int1)
& etype(c2841,int0)
& fact(c2841,real)
& gener(c2841,sp)
& refer(c2841,indet)
& varia(c2841,varia_c)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& card(c2842,int1)
& etype(c2842,int1)
& fact(c2842,real)
& gener(c2842,gener_c)
& refer(c2842,refer_c)
& varia(c2842,varia_c)
& card(gmbh__1_1,card_c)
& etype(gmbh__1_1,int1)
& fact(gmbh__1_1,real)
& gener(gmbh__1_1,ge)
& refer(gmbh__1_1,refer_c)
& varia(gmbh__1_1,varia_c)
& card(c2844,int1)
& etype(c2844,int0)
& fact(c2844,real)
& gener(c2844,sp)
& refer(c2844,det)
& varia(c2844,con)
& card(c2845,int1)
& etype(c2845,int0)
& fact(c2845,real)
& gener(c2845,sp)
& refer(c2845,indet)
& varia(c2845,varia_c)
& card(c31,card_c)
& etype(c31,etype_c)
& fact(c31,real)
& gener(c31,gener_c)
& refer(c31,refer_c)
& varia(c31,varia_c)
& card(c3436,card_c)
& etype(c3436,etype_c)
& fact(c3436,real)
& gener(c3436,gener_c)
& refer(c3436,refer_c)
& varia(c3436,varia_c)
& fact(gr__374nden_1_2,real)
& gener(gr__374nden_1_2,ge)
& card(aggregat_1_1,int1)
& etype(aggregat_1_1,int0)
& fact(aggregat_1_1,real)
& gener(aggregat_1_1,ge)
& refer(aggregat_1_1,refer_c)
& varia(aggregat_1_1,varia_c)
& card(fabrikant_1_1,int1)
& etype(fabrikant_1_1,int0)
& fact(fabrikant_1_1,real)
& gener(fabrikant_1_1,ge)
& refer(fabrikant_1_1,refer_c)
& varia(fabrikant_1_1,varia_c)
& fact(planen_1_1,real)
& gener(planen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10328]) ).
fof(f10334,plain,
( attr(c11,c12)
& sub(c11,stadt__1_1)
& sub(c12,name_1_1)
& val(c12,m__374nchen_0)
& attr(c17,c18)
& attr(c17,c19)
& sub(c18,tag_1_1)
& val(c18,c15)
& sub(c19,monat_1_1)
& val(c19,c16)
& prop(c2226,c2204)
& pred(c2230,maschinenfabrikant_1_1)
& prop(c2230,britisch__1_1)
& attr(c2836,c2837)
& sub(c2836,firma_1_1)
& sub(c2837,name_1_1)
& val(c2837,bmw_0)
& attr(c2840,c2841)
& sub(c2840,mensch_1_1)
& sub(c2841,familiename_1_1)
& val(c2841,roll_0)
& sub(c2842,gmbh__1_1)
& attr(c2844,c2845)
& sub(c2844,mensch_1_1)
& sub(c2845,familiename_1_1)
& val(c2845,royce_0)
& tupl(c31,c11,c17)
& assoc(maschinenfabrikant_1_1,aggregat_1_1)
& sub(maschinenfabrikant_1_1,fabrikant_1_1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& refer(c11,det)
& varia(c11,con)
& etype(c12,int0)
& fact(c12,real)
& gener(c12,sp)
& refer(c12,indet)
& varia(c12,varia_c)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& refer(c17,det)
& varia(c17,con)
& etype(c18,etype_c)
& fact(c18,real)
& gener(c18,sp)
& refer(c18,refer_c)
& varia(c18,varia_c)
& etype(c19,etype_c)
& fact(c19,real)
& gener(c19,sp)
& refer(c19,refer_c)
& varia(c19,varia_c)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& refer(tag_1_1,refer_c)
& varia(tag_1_1,varia_c)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& refer(monat_1_1,refer_c)
& varia(monat_1_1,varia_c)
& etype(c2226,int1)
& fact(c2226,real)
& gener(c2226,gener_c)
& refer(c2226,refer_c)
& varia(c2226,varia_c)
& etype(c2230,int1)
& fact(c2230,real)
& gener(c2230,gener_c)
& refer(c2230,refer_c)
& varia(c2230,varia_c)
& etype(maschinenfabrikant_1_1,int0)
& fact(maschinenfabrikant_1_1,real)
& gener(maschinenfabrikant_1_1,ge)
& refer(maschinenfabrikant_1_1,refer_c)
& varia(maschinenfabrikant_1_1,varia_c)
& etype(c2836,int0)
& fact(c2836,real)
& gener(c2836,sp)
& refer(c2836,det)
& varia(c2836,con)
& etype(c2837,int0)
& fact(c2837,real)
& gener(c2837,sp)
& refer(c2837,indet)
& varia(c2837,varia_c)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& refer(firma_1_1,refer_c)
& varia(firma_1_1,varia_c)
& etype(c2840,int0)
& fact(c2840,real)
& gener(c2840,sp)
& refer(c2840,det)
& varia(c2840,con)
& etype(c2841,int0)
& fact(c2841,real)
& gener(c2841,sp)
& refer(c2841,indet)
& varia(c2841,varia_c)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& etype(c2842,int1)
& fact(c2842,real)
& gener(c2842,gener_c)
& refer(c2842,refer_c)
& varia(c2842,varia_c)
& etype(gmbh__1_1,int1)
& fact(gmbh__1_1,real)
& gener(gmbh__1_1,ge)
& refer(gmbh__1_1,refer_c)
& varia(gmbh__1_1,varia_c)
& etype(c2844,int0)
& fact(c2844,real)
& gener(c2844,sp)
& refer(c2844,det)
& varia(c2844,con)
& etype(c2845,int0)
& fact(c2845,real)
& gener(c2845,sp)
& refer(c2845,indet)
& varia(c2845,varia_c)
& etype(c31,etype_c)
& fact(c31,real)
& gener(c31,gener_c)
& refer(c31,refer_c)
& varia(c31,varia_c)
& etype(c3436,etype_c)
& fact(c3436,real)
& gener(c3436,gener_c)
& refer(c3436,refer_c)
& varia(c3436,varia_c)
& fact(gr__374nden_1_2,real)
& gener(gr__374nden_1_2,ge)
& etype(aggregat_1_1,int0)
& fact(aggregat_1_1,real)
& gener(aggregat_1_1,ge)
& refer(aggregat_1_1,refer_c)
& varia(aggregat_1_1,varia_c)
& etype(fabrikant_1_1,int0)
& fact(fabrikant_1_1,real)
& gener(fabrikant_1_1,ge)
& refer(fabrikant_1_1,refer_c)
& varia(fabrikant_1_1,varia_c)
& fact(planen_1_1,real)
& gener(planen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10331]) ).
fof(f10337,plain,
( attr(c11,c12)
& sub(c11,stadt__1_1)
& sub(c12,name_1_1)
& val(c12,m__374nchen_0)
& attr(c17,c18)
& attr(c17,c19)
& sub(c18,tag_1_1)
& val(c18,c15)
& sub(c19,monat_1_1)
& val(c19,c16)
& prop(c2226,c2204)
& pred(c2230,maschinenfabrikant_1_1)
& prop(c2230,britisch__1_1)
& attr(c2836,c2837)
& sub(c2836,firma_1_1)
& sub(c2837,name_1_1)
& val(c2837,bmw_0)
& attr(c2840,c2841)
& sub(c2840,mensch_1_1)
& sub(c2841,familiename_1_1)
& val(c2841,roll_0)
& sub(c2842,gmbh__1_1)
& attr(c2844,c2845)
& sub(c2844,mensch_1_1)
& sub(c2845,familiename_1_1)
& val(c2845,royce_0)
& tupl(c31,c11,c17)
& assoc(maschinenfabrikant_1_1,aggregat_1_1)
& sub(maschinenfabrikant_1_1,fabrikant_1_1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& varia(c11,con)
& etype(c12,int0)
& fact(c12,real)
& gener(c12,sp)
& varia(c12,varia_c)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& varia(stadt__1_1,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& varia(name_1_1,varia_c)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& varia(c17,con)
& etype(c18,etype_c)
& fact(c18,real)
& gener(c18,sp)
& varia(c18,varia_c)
& etype(c19,etype_c)
& fact(c19,real)
& gener(c19,sp)
& varia(c19,varia_c)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& varia(tag_1_1,varia_c)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& varia(monat_1_1,varia_c)
& etype(c2226,int1)
& fact(c2226,real)
& gener(c2226,gener_c)
& varia(c2226,varia_c)
& etype(c2230,int1)
& fact(c2230,real)
& gener(c2230,gener_c)
& varia(c2230,varia_c)
& etype(maschinenfabrikant_1_1,int0)
& fact(maschinenfabrikant_1_1,real)
& gener(maschinenfabrikant_1_1,ge)
& varia(maschinenfabrikant_1_1,varia_c)
& etype(c2836,int0)
& fact(c2836,real)
& gener(c2836,sp)
& varia(c2836,con)
& etype(c2837,int0)
& fact(c2837,real)
& gener(c2837,sp)
& varia(c2837,varia_c)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& varia(firma_1_1,varia_c)
& etype(c2840,int0)
& fact(c2840,real)
& gener(c2840,sp)
& varia(c2840,con)
& etype(c2841,int0)
& fact(c2841,real)
& gener(c2841,sp)
& varia(c2841,varia_c)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& varia(mensch_1_1,varia_c)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& varia(familiename_1_1,varia_c)
& etype(c2842,int1)
& fact(c2842,real)
& gener(c2842,gener_c)
& varia(c2842,varia_c)
& etype(gmbh__1_1,int1)
& fact(gmbh__1_1,real)
& gener(gmbh__1_1,ge)
& varia(gmbh__1_1,varia_c)
& etype(c2844,int0)
& fact(c2844,real)
& gener(c2844,sp)
& varia(c2844,con)
& etype(c2845,int0)
& fact(c2845,real)
& gener(c2845,sp)
& varia(c2845,varia_c)
& etype(c31,etype_c)
& fact(c31,real)
& gener(c31,gener_c)
& varia(c31,varia_c)
& etype(c3436,etype_c)
& fact(c3436,real)
& gener(c3436,gener_c)
& varia(c3436,varia_c)
& fact(gr__374nden_1_2,real)
& gener(gr__374nden_1_2,ge)
& etype(aggregat_1_1,int0)
& fact(aggregat_1_1,real)
& gener(aggregat_1_1,ge)
& varia(aggregat_1_1,varia_c)
& etype(fabrikant_1_1,int0)
& fact(fabrikant_1_1,real)
& gener(fabrikant_1_1,ge)
& varia(fabrikant_1_1,varia_c)
& fact(planen_1_1,real)
& gener(planen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10334]) ).
fof(f10342,plain,
( attr(c11,c12)
& sub(c11,stadt__1_1)
& sub(c12,name_1_1)
& val(c12,m__374nchen_0)
& attr(c17,c18)
& attr(c17,c19)
& sub(c18,tag_1_1)
& val(c18,c15)
& sub(c19,monat_1_1)
& val(c19,c16)
& prop(c2226,c2204)
& pred(c2230,maschinenfabrikant_1_1)
& prop(c2230,britisch__1_1)
& attr(c2836,c2837)
& sub(c2836,firma_1_1)
& sub(c2837,name_1_1)
& val(c2837,bmw_0)
& attr(c2840,c2841)
& sub(c2840,mensch_1_1)
& sub(c2841,familiename_1_1)
& val(c2841,roll_0)
& sub(c2842,gmbh__1_1)
& attr(c2844,c2845)
& sub(c2844,mensch_1_1)
& sub(c2845,familiename_1_1)
& val(c2845,royce_0)
& tupl(c31,c11,c17)
& assoc(maschinenfabrikant_1_1,aggregat_1_1)
& sub(maschinenfabrikant_1_1,fabrikant_1_1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& etype(c12,int0)
& fact(c12,real)
& gener(c12,sp)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& etype(c18,etype_c)
& fact(c18,real)
& gener(c18,sp)
& etype(c19,etype_c)
& fact(c19,real)
& gener(c19,sp)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& etype(c2226,int1)
& fact(c2226,real)
& gener(c2226,gener_c)
& etype(c2230,int1)
& fact(c2230,real)
& gener(c2230,gener_c)
& etype(maschinenfabrikant_1_1,int0)
& fact(maschinenfabrikant_1_1,real)
& gener(maschinenfabrikant_1_1,ge)
& etype(c2836,int0)
& fact(c2836,real)
& gener(c2836,sp)
& etype(c2837,int0)
& fact(c2837,real)
& gener(c2837,sp)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& etype(c2840,int0)
& fact(c2840,real)
& gener(c2840,sp)
& etype(c2841,int0)
& fact(c2841,real)
& gener(c2841,sp)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& etype(c2842,int1)
& fact(c2842,real)
& gener(c2842,gener_c)
& etype(gmbh__1_1,int1)
& fact(gmbh__1_1,real)
& gener(gmbh__1_1,ge)
& etype(c2844,int0)
& fact(c2844,real)
& gener(c2844,sp)
& etype(c2845,int0)
& fact(c2845,real)
& gener(c2845,sp)
& etype(c31,etype_c)
& fact(c31,real)
& gener(c31,gener_c)
& etype(c3436,etype_c)
& fact(c3436,real)
& gener(c3436,gener_c)
& fact(gr__374nden_1_2,real)
& gener(gr__374nden_1_2,ge)
& etype(aggregat_1_1,int0)
& fact(aggregat_1_1,real)
& gener(aggregat_1_1,ge)
& etype(fabrikant_1_1,int0)
& fact(fabrikant_1_1,real)
& gener(fabrikant_1_1,ge)
& fact(planen_1_1,real)
& gener(planen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10337]) ).
fof(f10347,plain,
( attr(c11,c12)
& sub(c11,stadt__1_1)
& sub(c12,name_1_1)
& val(c12,m__374nchen_0)
& attr(c17,c18)
& attr(c17,c19)
& sub(c18,tag_1_1)
& val(c18,c15)
& sub(c19,monat_1_1)
& val(c19,c16)
& prop(c2226,c2204)
& pred(c2230,maschinenfabrikant_1_1)
& prop(c2230,britisch__1_1)
& attr(c2836,c2837)
& sub(c2836,firma_1_1)
& sub(c2837,name_1_1)
& val(c2837,bmw_0)
& attr(c2840,c2841)
& sub(c2840,mensch_1_1)
& sub(c2841,familiename_1_1)
& val(c2841,roll_0)
& sub(c2842,gmbh__1_1)
& attr(c2844,c2845)
& sub(c2844,mensch_1_1)
& sub(c2845,familiename_1_1)
& val(c2845,royce_0)
& tupl(c31,c11,c17)
& assoc(maschinenfabrikant_1_1,aggregat_1_1)
& sub(maschinenfabrikant_1_1,fabrikant_1_1)
& etype(c11,int0)
& fact(c11,real)
& etype(c12,int0)
& fact(c12,real)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& etype(c17,int0)
& fact(c17,real)
& etype(c18,etype_c)
& fact(c18,real)
& etype(c19,etype_c)
& fact(c19,real)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& etype(c2226,int1)
& fact(c2226,real)
& etype(c2230,int1)
& fact(c2230,real)
& etype(maschinenfabrikant_1_1,int0)
& fact(maschinenfabrikant_1_1,real)
& etype(c2836,int0)
& fact(c2836,real)
& etype(c2837,int0)
& fact(c2837,real)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& etype(c2840,int0)
& fact(c2840,real)
& etype(c2841,int0)
& fact(c2841,real)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& etype(c2842,int1)
& fact(c2842,real)
& etype(gmbh__1_1,int1)
& fact(gmbh__1_1,real)
& etype(c2844,int0)
& fact(c2844,real)
& etype(c2845,int0)
& fact(c2845,real)
& etype(c31,etype_c)
& fact(c31,real)
& etype(c3436,etype_c)
& fact(c3436,real)
& fact(gr__374nden_1_2,real)
& etype(aggregat_1_1,int0)
& fact(aggregat_1_1,real)
& etype(fabrikant_1_1,int0)
& fact(fabrikant_1_1,real)
& fact(planen_1_1,real) ),
inference(pure_predicate_removal,[],[f10342]) ).
fof(f10523,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( arg1(X4,X1)
& arg2(X4,X5)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& sub(X5,X2)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(ennf_transformation,[],[f162]) ).
fof(f10524,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( arg1(X4,X1)
& arg2(X4,X5)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& sub(X5,X2)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(flattening,[],[f10523]) ).
fof(f10525,plain,
! [X0,X1] :
( ? [X2] :
( arg1(X2,X0)
& arg2(X2,X1)
& subr(X2,sub_0) )
| ~ sub(X0,X1) ),
inference(ennf_transformation,[],[f163]) ).
fof(f10554,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ attr(X0,X1)
| ~ attr(X3,X2)
| ~ attr(X5,X6)
| ~ obj(X4,X0)
| ~ sub(X1,name_1_1)
| ~ sub(X0,firma_1_1)
| ~ sub(X2,name_1_1)
| ~ val(X1,bmw_0)
| ~ val(X2,bmw_0) ),
inference(ennf_transformation,[],[f10189]) ).
fof(f10833,plain,
! [X2,X0,X1] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| obj(sK54(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f10524]) ).
fof(f10838,plain,
! [X0,X1] :
( ~ sub(X0,X1)
| subr(sK57(X0,X1),sub_0) ),
inference(cnf_transformation,[],[f10525]) ).
fof(f10839,plain,
! [X0,X1] :
( ~ sub(X0,X1)
| arg2(sK57(X0,X1),X1) ),
inference(cnf_transformation,[],[f10525]) ).
fof(f10840,plain,
! [X0,X1] :
( ~ sub(X0,X1)
| arg1(sK57(X0,X1),X0) ),
inference(cnf_transformation,[],[f10525]) ).
fof(f20772,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ val(X2,bmw_0)
| ~ val(X1,bmw_0)
| ~ sub(X2,name_1_1)
| ~ sub(X0,firma_1_1)
| ~ sub(X1,name_1_1)
| ~ obj(X4,X0)
| ~ attr(X5,X6)
| ~ attr(X3,X2)
| ~ attr(X0,X1) ),
inference(cnf_transformation,[],[f10554]) ).
fof(f20835,plain,
attr(c2844,c2845),
inference(cnf_transformation,[],[f10347]) ).
fof(f20841,plain,
val(c2837,bmw_0),
inference(cnf_transformation,[],[f10347]) ).
fof(f20842,plain,
sub(c2837,name_1_1),
inference(cnf_transformation,[],[f10347]) ).
fof(f20843,plain,
sub(c2836,firma_1_1),
inference(cnf_transformation,[],[f10347]) ).
fof(f20844,plain,
attr(c2836,c2837),
inference(cnf_transformation,[],[f10347]) ).
fof(f21133,plain,
! [X2,X0,X1] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| arg1(X0,X1)
| obj(sK54(X0,X1,X2),X1) ),
inference(consistent_polarity_flipping,[],[f10833]) ).
fof(f21137,plain,
! [X0,X1] :
( ~ arg1(sK57(X0,X1),X0)
| sub(X0,X1) ),
inference(consistent_polarity_flipping,[],[f10840]) ).
fof(f21138,plain,
! [X0,X1] :
( arg2(sK57(X0,X1),X1)
| sub(X0,X1) ),
inference(consistent_polarity_flipping,[],[f10839]) ).
fof(f21139,plain,
! [X0,X1] :
( subr(sK57(X0,X1),sub_0)
| sub(X0,X1) ),
inference(consistent_polarity_flipping,[],[f10838]) ).
fof(f31002,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ val(X2,bmw_0)
| ~ val(X1,bmw_0)
| sub(X2,name_1_1)
| sub(X0,firma_1_1)
| sub(X1,name_1_1)
| ~ obj(X4,X0)
| ~ attr(X5,X6)
| ~ attr(X3,X2)
| ~ attr(X0,X1) ),
inference(consistent_polarity_flipping,[],[f20772]) ).
fof(f31009,plain,
~ sub(c2836,firma_1_1),
inference(consistent_polarity_flipping,[],[f20843]) ).
fof(f31010,plain,
~ sub(c2837,name_1_1),
inference(consistent_polarity_flipping,[],[f20842]) ).
fof(f31019,definition,
( spl63_1
<=> ! [X6,X5] : ~ attr(X5,X6) ),
introduced(definition,[new_symbols(definition,[spl63_1])],[avatar_definition]) ).
fof(f31020,plain,
( ! [X6,X5] : ~ attr(X5,X6)
| ~ spl63_1 ),
inference(avatar_component_clause,[],[f31019]) ).
fof(f31022,definition,
( spl63_2
<=> ! [X4,X0,X1] :
( ~ val(X1,bmw_0)
| sub(X1,name_1_1)
| sub(X0,firma_1_1)
| ~ attr(X0,X1)
| ~ obj(X4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl63_2])],[avatar_definition]) ).
fof(f31023,plain,
( ! [X0,X1,X4] :
( ~ val(X1,bmw_0)
| sub(X1,name_1_1)
| sub(X0,firma_1_1)
| ~ attr(X0,X1)
| ~ obj(X4,X0) )
| ~ spl63_2 ),
inference(avatar_component_clause,[],[f31022]) ).
fof(f31025,definition,
( spl63_3
<=> ! [X2,X3] :
( ~ val(X2,bmw_0)
| ~ attr(X3,X2)
| sub(X2,name_1_1) ) ),
introduced(definition,[new_symbols(definition,[spl63_3])],[avatar_definition]) ).
fof(f31026,plain,
( ! [X2,X3] :
( ~ attr(X3,X2)
| ~ val(X2,bmw_0)
| sub(X2,name_1_1) )
| ~ spl63_3 ),
inference(avatar_component_clause,[],[f31025]) ).
fof(f31027,plain,
( spl63_1
| spl63_2
| spl63_3 ),
inference(avatar_split_clause,[],[f31002,f31025,f31022,f31019]) ).
fof(f31028,plain,
( ! [X0,X1] :
( sub(c2837,name_1_1)
| sub(X0,firma_1_1)
| ~ attr(X0,c2837)
| ~ obj(X1,X0) )
| ~ spl63_2 ),
inference(resolution,[],[f20841,f31023]) ).
fof(f31030,definition,
( spl63_4
<=> ! [X0,X1] :
( sub(X0,firma_1_1)
| ~ obj(X1,X0)
| ~ attr(X0,c2837) ) ),
introduced(definition,[new_symbols(definition,[spl63_4])],[avatar_definition]) ).
fof(f31031,plain,
( ! [X0,X1] :
( ~ attr(X0,c2837)
| ~ obj(X1,X0)
| sub(X0,firma_1_1) )
| ~ spl63_4 ),
inference(avatar_component_clause,[],[f31030]) ).
fof(f31033,definition,
( spl63_5
<=> sub(c2837,name_1_1) ),
introduced(definition,[new_symbols(definition,[spl63_5])],[avatar_definition]) ).
fof(f31034,plain,
( ~ sub(c2837,name_1_1)
| spl63_5 ),
inference(avatar_component_clause,[],[f31033]) ).
fof(f31037,plain,
( ! [X0] :
( ~ obj(X0,c2836)
| sub(c2836,firma_1_1) )
| ~ spl63_4 ),
inference(resolution,[],[f31031,f20844]) ).
fof(f31039,definition,
( spl63_6
<=> sub(c2836,firma_1_1) ),
introduced(definition,[new_symbols(definition,[spl63_6])],[avatar_definition]) ).
fof(f31040,plain,
( ~ sub(c2836,firma_1_1)
| spl63_6 ),
inference(avatar_component_clause,[],[f31039]) ).
fof(f31043,definition,
( spl63_7
<=> ! [X0] : ~ obj(X0,c2836) ),
introduced(definition,[new_symbols(definition,[spl63_7])],[avatar_definition]) ).
fof(f31044,plain,
( ! [X0] : ~ obj(X0,c2836)
| ~ spl63_7 ),
inference(avatar_component_clause,[],[f31043]) ).
fof(f31046,plain,
~ spl63_6,
inference(avatar_split_clause,[],[f31009,f31039]) ).
fof(f31047,plain,
~ spl63_5,
inference(avatar_split_clause,[],[f31010,f31033]) ).
fof(f31202,plain,
( $false
| ~ spl63_1 ),
inference(backward_subsumption_resolution,[],[f20835,f31020]) ).
fof(f31208,plain,
~ spl63_1,
inference(avatar_contradiction_clause,[],[f31202]) ).
fof(f31263,plain,
( ~ val(c2837,bmw_0)
| sub(c2837,name_1_1)
| ~ spl63_3 ),
inference(resolution,[],[f20844,f31026]) ).
fof(f31264,plain,
( sub(c2837,name_1_1)
| ~ spl63_3 ),
inference(forward_subsumption_resolution,[],[f31263,f20841]) ).
fof(f31265,plain,
( $false
| ~ spl63_3
| spl63_5 ),
inference(forward_subsumption_resolution,[],[f31264,f31034]) ).
fof(f31266,plain,
( ~ spl63_3
| spl63_5 ),
inference(avatar_contradiction_clause,[],[f31265]) ).
fof(f31267,plain,
( ! [X0,X1] :
( sub(X0,firma_1_1)
| ~ attr(X0,c2837)
| ~ obj(X1,X0) )
| ~ spl63_2
| spl63_5 ),
inference(forward_subsumption_resolution,[],[f31028,f31034]) ).
fof(f31268,plain,
( ! [X0] : ~ obj(X0,c2836)
| ~ spl63_4
| spl63_6 ),
inference(forward_subsumption_resolution,[],[f31037,f31040]) ).
fof(f31272,plain,
( spl63_4
| ~ spl63_2
| spl63_5 ),
inference(avatar_split_clause,[],[f31267,f31033,f31022,f31030]) ).
fof(f31273,plain,
( spl63_7
| ~ spl63_4
| spl63_6 ),
inference(avatar_split_clause,[],[f31268,f31039,f31030,f31043]) ).
fof(f31909,plain,
! [X2,X3,X0,X1] :
( ~ arg2(sK57(X0,X1),X2)
| arg1(sK57(X0,X1),X3)
| obj(sK54(sK57(X0,X1),X3,X2),X3)
| sub(X0,X1) ),
inference(resolution,[],[f21133,f21139]) ).
fof(f31915,definition,
( spl63_128
<=> ! [X2] : sub(c2836,X2) ),
introduced(definition,[new_symbols(definition,[spl63_128])],[avatar_definition]) ).
fof(f31916,plain,
( ! [X2] : sub(c2836,X2)
| ~ spl63_128 ),
inference(avatar_component_clause,[],[f31915]) ).
fof(f34561,plain,
( $false
| spl63_6
| ~ spl63_128 ),
inference(backward_subsumption_resolution,[],[f31040,f31916]) ).
fof(f34573,plain,
( spl63_6
| ~ spl63_128 ),
inference(avatar_contradiction_clause,[],[f34561]) ).
fof(f36046,plain,
! [X2,X0,X1] :
( arg1(sK57(X0,X1),X2)
| obj(sK54(sK57(X0,X1),X2,X1),X2)
| sub(X0,X1)
| sub(X0,X1) ),
inference(resolution,[],[f31909,f21138]) ).
fof(f36047,plain,
! [X2,X0,X1] :
( obj(sK54(sK57(X0,X1),X2,X1),X2)
| arg1(sK57(X0,X1),X2)
| sub(X0,X1) ),
inference(duplicate_literal_removal,[],[f36046]) ).
fof(f46284,plain,
( ! [X0,X1] :
( arg1(sK57(X0,X1),c2836)
| sub(X0,X1) )
| ~ spl63_7 ),
inference(resolution,[],[f36047,f31044]) ).
fof(f46471,plain,
( ! [X0] :
( sub(c2836,X0)
| sub(c2836,X0) )
| ~ spl63_7 ),
inference(resolution,[],[f46284,f21137]) ).
fof(f46472,plain,
( ! [X0] : sub(c2836,X0)
| ~ spl63_7 ),
inference(duplicate_literal_removal,[],[f46471]) ).
fof(f46473,plain,
( spl63_128
| ~ spl63_7 ),
inference(avatar_split_clause,[],[f46472,f31043,f31915]) ).
cnf(s1,plain,
( spl63_1
| spl63_2
| spl63_3 ),
inference(sat_conversion,[],[f31027]) ).
cnf(s4,plain,
~ spl63_6,
inference(sat_conversion,[],[f31046]) ).
cnf(s5,plain,
~ spl63_5,
inference(sat_conversion,[],[f31047]) ).
cnf(s15,plain,
~ spl63_1,
inference(sat_conversion,[],[f31208]) ).
cnf(s23,plain,
( ~ spl63_3
| spl63_5 ),
inference(sat_conversion,[],[f31266]) ).
cnf(s26,plain,
( ~ spl63_2
| spl63_4
| spl63_5 ),
inference(sat_conversion,[],[f31272]) ).
cnf(s27,plain,
( ~ spl63_4
| spl63_6
| spl63_7 ),
inference(sat_conversion,[],[f31273]) ).
cnf(s268,plain,
( spl63_6
| ~ spl63_128 ),
inference(sat_conversion,[],[f34573]) ).
cnf(s1289,plain,
( ~ spl63_7
| spl63_128 ),
inference(sat_conversion,[],[f46473]) ).
cnf(s1327,plain,
~ spl63_3,
inference(rat,[],[s23,s5]) ).
cnf(s1328,plain,
~ spl63_128,
inference(rat,[],[s268,s4]) ).
cnf(s1329,plain,
~ spl63_7,
inference(rat,[],[s1289,s1328]) ).
cnf(s1330,plain,
~ spl63_4,
inference(rat,[],[s27,s4,s1329]) ).
cnf(s1331,plain,
~ spl63_2,
inference(rat,[],[s26,s5,s1330]) ).
cnf(s1332,plain,
$false,
inference(rat,[],[s1,s1327,s1331,s15]) ).
fof(f46474,plain,
$false,
inference(avatar_sat_refutation,[],[s1332]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+38 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n002.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 23:18:50 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.76/1.77 % (879056)Will run a generic schedule for satisfiability detection.
% 7.76/1.77 % (879065)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2943411081:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 7.76/1.77 % (879062)% WARNING: option uhcvi not known.
% 7.76/1.77 % (879061)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2646692431_2998 on theBenchmark for (2998ds/0Mi)
% 7.76/1.77 % (879062)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1034396107:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 7.76/1.77 % (879063)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1724044900:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 7.76/1.77 % (879064)dis+10_1_sil=32000:sp=arity:random_seed=2573293280:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 7.76/1.77 % (879066)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=21514413:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 7.76/1.77 % (879067)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1696083806:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 7.76/1.77 % (879065)Instruction limit reached!
% 7.76/1.77 % (879065)------------------------------
% 7.76/1.77 % (879065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879065)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879065)Termination reason: Instruction limit
% 7.76/1.77 % (879065)Termination phase: Blocked clause elimination
% 7.76/1.77 % (879065)Time elapsed: 0.043 s
% 7.76/1.77 % (879065)Peak memory usage: 28 MB
% 7.76/1.77 % (879065)Instructions burned: 116 (million)
% 7.76/1.77 % (879075)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2808169941:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 7.76/1.77 % (879064)Instruction limit reached!
% 7.76/1.77 % (879064)------------------------------
% 7.76/1.77 % (879064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879064)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879064)Termination reason: Instruction limit
% 7.76/1.77 % (879064)Termination phase: Saturation
% 7.76/1.77 % (879064)Time elapsed: 0.059 s
% 7.76/1.77 % (879064)Peak memory usage: 26 MB
% 7.76/1.77 % (879064)Instructions burned: 104 (million)
% 7.76/1.77 % (879066)Instruction limit reached!
% 7.76/1.77 % (879066)------------------------------
% 7.76/1.77 % (879066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879066)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879066)Termination reason: Instruction limit
% 7.76/1.77 % (879066)Termination phase: Saturation
% 7.76/1.77 % (879066)Time elapsed: 0.074 s
% 7.76/1.77 % (879066)Peak memory usage: 28 MB
% 7.76/1.77 % (879066)Instructions burned: 132 (million)
% 7.76/1.77 % (879077)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=189149059:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 7.76/1.77 % (879067)Instruction limit reached!
% 7.76/1.77 % (879067)------------------------------
% 7.76/1.77 % (879067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879067)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879067)Termination reason: Instruction limit
% 7.76/1.77 % (879067)Termination phase: Saturation
% 7.76/1.77 % (879067)Time elapsed: 0.095 s
% 7.76/1.77 % (879067)Peak memory usage: 30 MB
% 7.76/1.77 % (879067)Instructions burned: 160 (million)
% 7.76/1.77 % (879078)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3675468269:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 7.76/1.77 % (879081)ott-21_1_sil=16000:fs=off:random_seed=3023932211:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 7.76/1.77 % TRYING [1]
% 7.76/1.77 % (879077)Instruction limit reached!
% 7.76/1.77 % (879077)------------------------------
% 7.76/1.77 % (879077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879077)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879077)Termination reason: Instruction limit
% 7.76/1.77 % (879077)Termination phase: Blocked clause elimination
% 7.76/1.77 % (879077)Time elapsed: 0.079 s
% 7.76/1.77 % (879077)Peak memory usage: 28 MB
% 7.76/1.77 % (879077)Instructions burned: 131 (million)
% 7.76/1.77 % TRYING [2]
% 7.76/1.77 % (879083)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3066194225:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 7.76/1.77 % (879081)Instruction limit reached!
% 7.76/1.77 % (879081)------------------------------
% 7.76/1.77 % (879081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879081)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879081)Termination reason: Instruction limit
% 7.76/1.77 % (879081)Termination phase: Saturation
% 7.76/1.77 % (879081)Time elapsed: 0.093 s
% 7.76/1.77 % (879081)Peak memory usage: 28 MB
% 7.76/1.77 % (879081)Instructions burned: 182 (million)
% 7.76/1.77 % (879085)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=960178948:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 7.76/1.77 % (879075)Instruction limit reached!
% 7.76/1.77 % (879075)------------------------------
% 7.76/1.77 % (879075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879075)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879075)Termination reason: Instruction limit
% 7.76/1.77 % (879075)Termination phase: Finite model building constraint generation
% 7.76/1.77 % (879075)Time elapsed: 0.187 s
% 7.76/1.77 % (879075)Peak memory usage: 54 MB
% 7.76/1.77 % (879075)Instructions burned: 716 (million)
% 7.76/1.77 % (879087)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2777961912:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 7.76/1.77 % TRYING [1]
% 7.76/1.77 % TRYING [2]
% 7.76/1.77 % TRYING [3]
% 7.76/1.77 % TRYING [1]
% 7.76/1.77 % (879083)Instruction limit reached!
% 7.76/1.77 % (879083)------------------------------
% 7.76/1.77 % (879083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879083)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879083)Termination reason: Instruction limit
% 7.76/1.77 % (879083)Termination phase: Saturation
% 7.76/1.77 % (879083)Time elapsed: 0.250 s
% 7.76/1.77 % (879083)Peak memory usage: 36 MB
% 7.76/1.77 % (879083)Instructions burned: 479 (million)
% 7.76/1.77 % (879078)Instruction limit reached!
% 7.76/1.77 % (879078)------------------------------
% 7.76/1.77 % (879078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879078)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879078)Termination reason: Instruction limit
% 7.76/1.77 % (879078)Termination phase: Saturation
% 7.76/1.77 % (879078)Time elapsed: 0.341 s
% 7.76/1.77 % (879078)Peak memory usage: 34 MB
% 7.76/1.77 % (879078)Instructions burned: 686 (million)
% 7.76/1.77 % (879089)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=589832489:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 7.76/1.77 % (879090)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2315380551:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 7.76/1.77 % (879085)Instruction limit reached!
% 7.76/1.77 % (879085)------------------------------
% 7.76/1.77 % (879085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879085)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879085)Termination reason: Instruction limit
% 7.76/1.77 % (879085)Termination phase: Finite model building SAT solving
% 7.76/1.77 % (879085)Time elapsed: 0.320 s
% 7.76/1.77 % (879085)Peak memory usage: 38 MB
% 7.76/1.77 % (879085)Instructions burned: 867 (million)
% 7.76/1.77 % (879093)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1862587911:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 7.76/1.77 % (879087)Instruction limit reached!
% 7.76/1.77 % (879087)------------------------------
% 7.76/1.77 % (879087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879087)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879087)Termination reason: Instruction limit
% 7.76/1.77 % (879087)Termination phase: Saturation
% 7.76/1.77 % (879087)Time elapsed: 0.350 s
% 7.76/1.77 % (879087)Peak memory usage: 55 MB
% 7.76/1.77 % (879087)Instructions burned: 1182 (million)
% 7.76/1.77 % (879095)fmb+10_1_sil=64000:random_seed=3450704517:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 7.76/1.77 % TRYING [4]
% 7.76/1.77 % TRYING [1]
% 7.76/1.77 % TRYING [2]
% 7.76/1.77 % (879090)Instruction limit reached!
% 7.76/1.77 % (879090)------------------------------
% 7.76/1.77 % (879090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879090)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879090)Termination reason: Instruction limit
% 7.76/1.77 % (879090)Termination phase: Saturation
% 7.76/1.77 % (879090)Time elapsed: 0.365 s
% 7.76/1.77 % (879090)Peak memory usage: 42 MB
% 7.76/1.77 % (879090)Instructions burned: 692 (million)
% 7.76/1.77 % (879097)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4065868244:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 7.76/1.77 % (879089)Instruction limit reached!
% 7.76/1.77 % (879089)------------------------------
% 7.76/1.77 % (879089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879089)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879089)Termination reason: Instruction limit
% 7.76/1.77 % (879089)Termination phase: Finite model building constraint generation
% 7.76/1.77 % (879089)Time elapsed: 0.430 s
% 7.76/1.77 % (879089)Peak memory usage: 97 MB
% 7.76/1.77 % (879089)Instructions burned: 891 (million)
% 7.76/1.77 % (879099)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4021423865:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 7.76/1.77 % (879093)Instruction limit reached!
% 7.76/1.77 % (879093)------------------------------
% 7.76/1.77 % (879093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879093)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879093)Termination reason: Instruction limit
% 7.76/1.77 % (879093)Termination phase: Saturation
% 7.76/1.77 % (879093)Time elapsed: 0.428 s
% 7.76/1.77 % (879093)Peak memory usage: 42 MB
% 7.76/1.77 % (879093)Instructions burned: 880 (million)
% 7.76/1.77 % (879101)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1912942397:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 7.76/1.77 % TRYING [20]
% 7.76/1.77 % TRYING [8]
% 7.76/1.77 % TRYING [3]
% 7.76/1.77 % (879099)Instruction limit reached!
% 7.76/1.77 % (879099)------------------------------
% 7.76/1.77 % (879099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.77 % (879099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.77 % (879099)CaDiCaL version: 2.1.3
% 7.76/1.77 % (879099)Termination reason: Instruction limit
% 7.76/1.77 % (879099)Termination phase: Finite model building constraint generation
% 7.76/1.77 % (879099)Time elapsed: 0.359 s
% 7.76/1.77 % (879099)Peak memory usage: 64 MB
% 7.76/1.77 % (879099)Instructions burned: 921 (million)
% 7.76/1.77 % (879103)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2814630797:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 7.76/1.77 % (879062) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-879056-879062"...
% 7.76/1.77 % (879062)...printing done.
% 7.76/1.77 % (879062)Refutation found. Thanks to Tanya!
% 7.76/1.77 % SZS status Theorem for theBenchmark
% 7.76/1.77 % SZS output start Proof for theBenchmark
% See solution above
% 7.76/1.79 % (879062)------------------------------
% 7.76/1.79 % (879062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.79 % (879062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.79 % (879062)CaDiCaL version: 2.1.3
% 7.76/1.79 % (879062)Termination reason: Refutation
% 7.76/1.79 % (879062)Time elapsed: 1.319 s
% 7.76/1.79 % (879062)Peak memory usage: 53 MB
% 7.76/1.79 % (879062)Instructions burned: 2265 (million)
% 7.76/1.79 % (879056)Success in time 1.54 s
% 7.76/1.79 % Vampire exiting
%------------------------------------------------------------------------------