%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR115+90 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:46 AM UTC 2026
% Result : Theorem 5.31s 1.26s
% Output : Refutation 5.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 16
% Syntax : Number of formulae : 106 ( 20 unt; 9 def)
% Number of atoms : 2504 ( 0 equ)
% Maximal formula atoms : 310 ( 23 avg)
% Number of connectives : 2506 ( 108 ~; 121 |;2264 &)
% ( 9 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 310 ( 25 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 35 ( 34 usr; 10 prp; 0-14 aty)
% Number of functors : 84 ( 84 usr; 81 con; 0-2 aty)
% Number of variables : 130 ( 0 sgn 111 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : member(X0,cons(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',member_first) ).
fof(f2,axiom,
! [X0,X1,X2] :
( member(X0,X2)
=> member(X0,cons(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',member_second) ).
fof(f160,axiom,
! [X0,X1,X2] :
( ( attr(X2,X0)
& member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
& sub(X0,X1) )
=> ? [X3] :
( mcont(X3,X2)
& obj(X3,X2)
& scar(X3,X2)
& subs(X3,stehen_1_b) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',attr_name__abk__374rzung_stehen_1_b_f__374r) ).
fof(f177,axiom,
! [X0,X1] :
( name(X1,X0)
=> ? [X2] :
( attr(X1,X2)
& sub(X2,name_1_1)
& val(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',name_rel__attr_val_name_1_1) ).
fof(f178,axiom,
! [X0,X1,X2] :
( ( attr(X2,X0)
& sub(X0,name_1_1)
& val(X0,X1) )
=> name(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',attr_val_name_1_1__name_rel) ).
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(X2,name_1_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',synth_qa07_007_mira_wp_514) ).
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(X2,name_1_1) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,axiom,
( assoc(boxermotor_1_1,boxer_2_1)
& sub(boxermotor_1_1,motor__1_1)
& assoc(bundeswehrausf__374hrung_1_1,bundeswehr_1_1)
& sub(bundeswehrausf__374hrung_1_1,ausf__374hrung_1_1)
& sub(c37238,faun_1_1)
& attr(c37245,c37246)
& sub(c37245,stadt__1_1)
& sub(c37246,name_1_1)
& val(c37246,n__374rnberg_0)
& sub(c37268,c37272)
& pmod(c37272,ackerbautreibend_1_1,einsatz_1_1)
& sub(c37274,fahrzeug__1_1)
& sub(c37284,bundeswehrausf__374hrung_1_1)
& pred(c37291,reifen__1_1)
& attch(c37298,c37291)
& pred(c37298,lypsoid_1_1)
& prop(c37298,n22x12_1_1)
& quant_p3(c37339,c37331,pferdest__344rke_1_1)
& prop(c37341,c37229)
& sub(c37341,bmw_1_1)
& sub(c37345,boxermotor_1_1)
& sub(c37359,last_1_1)
& quant_p3(c37361,c37356,kilo__1_1)
& tupl_p14(c37402,c37233,c37238,c37245,c37268,c37274,c37284,c37291,c37313,c37339,c37341,c37345,c37361,c37359)
& chsp2(drosseln_1_1,c37229)
& sort(boxermotor_1_1,d)
& card(boxermotor_1_1,int1)
& etype(boxermotor_1_1,int0)
& fact(boxermotor_1_1,real)
& gener(boxermotor_1_1,ge)
& quant(boxermotor_1_1,one)
& refer(boxermotor_1_1,refer_c)
& varia(boxermotor_1_1,varia_c)
& sort(boxer_2_1,d)
& card(boxer_2_1,int1)
& etype(boxer_2_1,int0)
& fact(boxer_2_1,real)
& gener(boxer_2_1,ge)
& quant(boxer_2_1,one)
& refer(boxer_2_1,refer_c)
& varia(boxer_2_1,varia_c)
& sort(motor__1_1,d)
& card(motor__1_1,int1)
& etype(motor__1_1,int0)
& fact(motor__1_1,real)
& gener(motor__1_1,ge)
& quant(motor__1_1,one)
& refer(motor__1_1,refer_c)
& varia(motor__1_1,varia_c)
& sort(bundeswehrausf__374hrung_1_1,ad)
& sort(bundeswehrausf__374hrung_1_1,d)
& sort(bundeswehrausf__374hrung_1_1,io)
& card(bundeswehrausf__374hrung_1_1,int1)
& etype(bundeswehrausf__374hrung_1_1,int0)
& fact(bundeswehrausf__374hrung_1_1,real)
& gener(bundeswehrausf__374hrung_1_1,ge)
& quant(bundeswehrausf__374hrung_1_1,one)
& refer(bundeswehrausf__374hrung_1_1,refer_c)
& varia(bundeswehrausf__374hrung_1_1,varia_c)
& sort(bundeswehr_1_1,d)
& sort(bundeswehr_1_1,io)
& card(bundeswehr_1_1,card_c)
& etype(bundeswehr_1_1,int1)
& fact(bundeswehr_1_1,real)
& gener(bundeswehr_1_1,ge)
& quant(bundeswehr_1_1,quant_c)
& refer(bundeswehr_1_1,refer_c)
& varia(bundeswehr_1_1,varia_c)
& sort(ausf__374hrung_1_1,ad)
& sort(ausf__374hrung_1_1,d)
& sort(ausf__374hrung_1_1,io)
& card(ausf__374hrung_1_1,int1)
& etype(ausf__374hrung_1_1,int0)
& fact(ausf__374hrung_1_1,real)
& gener(ausf__374hrung_1_1,ge)
& quant(ausf__374hrung_1_1,one)
& refer(ausf__374hrung_1_1,refer_c)
& varia(ausf__374hrung_1_1,varia_c)
& sort(c37238,o)
& card(c37238,int1)
& etype(c37238,int0)
& fact(c37238,real)
& gener(c37238,gener_c)
& quant(c37238,one)
& refer(c37238,refer_c)
& varia(c37238,varia_c)
& sort(faun_1_1,o)
& card(faun_1_1,int1)
& etype(faun_1_1,int0)
& fact(faun_1_1,real)
& gener(faun_1_1,ge)
& quant(faun_1_1,one)
& refer(faun_1_1,refer_c)
& varia(faun_1_1,varia_c)
& sort(c37245,d)
& sort(c37245,io)
& card(c37245,int1)
& etype(c37245,int0)
& fact(c37245,real)
& gener(c37245,sp)
& quant(c37245,one)
& refer(c37245,det)
& varia(c37245,con)
& sort(c37246,na)
& card(c37246,int1)
& etype(c37246,int0)
& fact(c37246,real)
& gener(c37246,sp)
& quant(c37246,one)
& refer(c37246,indet)
& varia(c37246,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(n__374rnberg_0,fe)
& sort(c37268,ad)
& sort(c37268,io)
& card(c37268,int1)
& etype(c37268,int0)
& fact(c37268,real)
& gener(c37268,sp)
& quant(c37268,one)
& refer(c37268,det)
& varia(c37268,con)
& sort(c37272,ad)
& sort(c37272,io)
& card(c37272,int1)
& etype(c37272,int0)
& fact(c37272,real)
& gener(c37272,ge)
& quant(c37272,one)
& refer(c37272,refer_c)
& varia(c37272,varia_c)
& sort(ackerbautreibend_1_1,aq)
& sort(einsatz_1_1,ad)
& sort(einsatz_1_1,io)
& card(einsatz_1_1,int1)
& etype(einsatz_1_1,int0)
& fact(einsatz_1_1,real)
& gener(einsatz_1_1,ge)
& quant(einsatz_1_1,one)
& refer(einsatz_1_1,refer_c)
& varia(einsatz_1_1,varia_c)
& sort(c37274,d)
& card(c37274,int1)
& etype(c37274,int0)
& fact(c37274,real)
& gener(c37274,gener_c)
& quant(c37274,one)
& refer(c37274,refer_c)
& varia(c37274,varia_c)
& sort(fahrzeug__1_1,d)
& card(fahrzeug__1_1,int1)
& etype(fahrzeug__1_1,int0)
& fact(fahrzeug__1_1,real)
& gener(fahrzeug__1_1,ge)
& quant(fahrzeug__1_1,one)
& refer(fahrzeug__1_1,refer_c)
& varia(fahrzeug__1_1,varia_c)
& sort(c37284,ad)
& sort(c37284,d)
& sort(c37284,io)
& card(c37284,int1)
& etype(c37284,int0)
& fact(c37284,real)
& gener(c37284,sp)
& quant(c37284,one)
& refer(c37284,det)
& varia(c37284,con)
& sort(c37291,d)
& card(c37291,int4)
& etype(c37291,int1)
& fact(c37291,real)
& gener(c37291,sp)
& quant(c37291,nfquant)
& refer(c37291,det)
& varia(c37291,varia_c)
& sort(reifen__1_1,d)
& card(reifen__1_1,int1)
& etype(reifen__1_1,int0)
& fact(reifen__1_1,real)
& gener(reifen__1_1,ge)
& quant(reifen__1_1,one)
& refer(reifen__1_1,refer_c)
& varia(reifen__1_1,varia_c)
& sort(c37298,o)
& card(c37298,cons(x_constant,cons(int1,nil)))
& etype(c37298,int1)
& fact(c37298,real)
& gener(c37298,gener_c)
& quant(c37298,mult)
& refer(c37298,refer_c)
& varia(c37298,varia_c)
& sort(lypsoid_1_1,o)
& card(lypsoid_1_1,int1)
& etype(lypsoid_1_1,int0)
& fact(lypsoid_1_1,real)
& gener(lypsoid_1_1,ge)
& quant(lypsoid_1_1,one)
& refer(lypsoid_1_1,refer_c)
& varia(lypsoid_1_1,varia_c)
& sort(n22x12_1_1,gq)
& sort(c37339,co)
& sort(c37339,m)
& card(c37339,card_c)
& etype(c37339,etype_c)
& fact(c37339,real)
& gener(c37339,gener_c)
& quant(c37339,quant_c)
& refer(c37339,refer_c)
& varia(c37339,con)
& sort(c37331,nu)
& card(c37331,int26)
& sort(pferdest__344rke_1_1,me)
& gener(pferdest__344rke_1_1,ge)
& sort(c37341,d)
& card(c37341,int1)
& etype(c37341,int0)
& fact(c37341,real)
& gener(c37341,gener_c)
& quant(c37341,one)
& refer(c37341,refer_c)
& varia(c37341,varia_c)
& sort(c37229,tq)
& sort(bmw_1_1,d)
& card(bmw_1_1,int1)
& etype(bmw_1_1,int0)
& fact(bmw_1_1,real)
& gener(bmw_1_1,ge)
& quant(bmw_1_1,one)
& refer(bmw_1_1,refer_c)
& varia(bmw_1_1,varia_c)
& sort(c37345,d)
& card(c37345,int1)
& etype(c37345,int0)
& fact(c37345,real)
& gener(c37345,gener_c)
& quant(c37345,one)
& refer(c37345,refer_c)
& varia(c37345,varia_c)
& sort(c37359,io)
& card(c37359,int1)
& etype(c37359,int0)
& fact(c37359,real)
& gener(c37359,gener_c)
& quant(c37359,one)
& refer(c37359,refer_c)
& varia(c37359,varia_c)
& sort(last_1_1,io)
& card(last_1_1,int1)
& etype(last_1_1,int0)
& fact(last_1_1,real)
& gener(last_1_1,ge)
& quant(last_1_1,one)
& refer(last_1_1,refer_c)
& varia(last_1_1,varia_c)
& sort(c37361,co)
& sort(c37361,m)
& card(c37361,card_c)
& etype(c37361,etype_c)
& fact(c37361,real)
& gener(c37361,gener_c)
& quant(c37361,quant_c)
& refer(c37361,refer_c)
& varia(c37361,con)
& sort(c37356,nu)
& card(c37356,int750)
& sort(kilo__1_1,me)
& gener(kilo__1_1,ge)
& sort(c37402,ent)
& card(c37402,card_c)
& etype(c37402,etype_c)
& fact(c37402,real)
& gener(c37402,gener_c)
& quant(c37402,quant_c)
& refer(c37402,refer_c)
& varia(c37402,varia_c)
& sort(c37233,o)
& card(c37233,int1)
& etype(c37233,int0)
& fact(c37233,real)
& gener(c37233,sp)
& quant(c37233,one)
& refer(c37233,det)
& varia(c37233,varia_c)
& sort(c37313,o)
& card(c37313,int1)
& etype(c37313,int0)
& fact(c37313,real)
& gener(c37313,gener_c)
& quant(c37313,one)
& refer(c37313,refer_c)
& varia(c37313,varia_c)
& sort(drosseln_1_1,da)
& fact(drosseln_1_1,real)
& gener(drosseln_1_1,ge) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_007_mira_wp_514) ).
fof(f10191,plain,
( assoc(boxermotor_1_1,boxer_2_1)
& sub(boxermotor_1_1,motor__1_1)
& assoc(bundeswehrausf__374hrung_1_1,bundeswehr_1_1)
& sub(bundeswehrausf__374hrung_1_1,ausf__374hrung_1_1)
& sub(c37238,faun_1_1)
& attr(c37245,c37246)
& sub(c37245,stadt__1_1)
& sub(c37246,name_1_1)
& val(c37246,n__374rnberg_0)
& sub(c37268,c37272)
& pmod(c37272,ackerbautreibend_1_1,einsatz_1_1)
& sub(c37274,fahrzeug__1_1)
& sub(c37284,bundeswehrausf__374hrung_1_1)
& pred(c37291,reifen__1_1)
& attch(c37298,c37291)
& pred(c37298,lypsoid_1_1)
& prop(c37298,n22x12_1_1)
& quant_p3(c37339,c37331,pferdest__344rke_1_1)
& prop(c37341,c37229)
& sub(c37341,bmw_1_1)
& sub(c37345,boxermotor_1_1)
& sub(c37359,last_1_1)
& quant_p3(c37361,c37356,kilo__1_1)
& chsp2(drosseln_1_1,c37229)
& sort(boxermotor_1_1,d)
& card(boxermotor_1_1,int1)
& etype(boxermotor_1_1,int0)
& fact(boxermotor_1_1,real)
& gener(boxermotor_1_1,ge)
& quant(boxermotor_1_1,one)
& refer(boxermotor_1_1,refer_c)
& varia(boxermotor_1_1,varia_c)
& sort(boxer_2_1,d)
& card(boxer_2_1,int1)
& etype(boxer_2_1,int0)
& fact(boxer_2_1,real)
& gener(boxer_2_1,ge)
& quant(boxer_2_1,one)
& refer(boxer_2_1,refer_c)
& varia(boxer_2_1,varia_c)
& sort(motor__1_1,d)
& card(motor__1_1,int1)
& etype(motor__1_1,int0)
& fact(motor__1_1,real)
& gener(motor__1_1,ge)
& quant(motor__1_1,one)
& refer(motor__1_1,refer_c)
& varia(motor__1_1,varia_c)
& sort(bundeswehrausf__374hrung_1_1,ad)
& sort(bundeswehrausf__374hrung_1_1,d)
& sort(bundeswehrausf__374hrung_1_1,io)
& card(bundeswehrausf__374hrung_1_1,int1)
& etype(bundeswehrausf__374hrung_1_1,int0)
& fact(bundeswehrausf__374hrung_1_1,real)
& gener(bundeswehrausf__374hrung_1_1,ge)
& quant(bundeswehrausf__374hrung_1_1,one)
& refer(bundeswehrausf__374hrung_1_1,refer_c)
& varia(bundeswehrausf__374hrung_1_1,varia_c)
& sort(bundeswehr_1_1,d)
& sort(bundeswehr_1_1,io)
& card(bundeswehr_1_1,card_c)
& etype(bundeswehr_1_1,int1)
& fact(bundeswehr_1_1,real)
& gener(bundeswehr_1_1,ge)
& quant(bundeswehr_1_1,quant_c)
& refer(bundeswehr_1_1,refer_c)
& varia(bundeswehr_1_1,varia_c)
& sort(ausf__374hrung_1_1,ad)
& sort(ausf__374hrung_1_1,d)
& sort(ausf__374hrung_1_1,io)
& card(ausf__374hrung_1_1,int1)
& etype(ausf__374hrung_1_1,int0)
& fact(ausf__374hrung_1_1,real)
& gener(ausf__374hrung_1_1,ge)
& quant(ausf__374hrung_1_1,one)
& refer(ausf__374hrung_1_1,refer_c)
& varia(ausf__374hrung_1_1,varia_c)
& sort(c37238,o)
& card(c37238,int1)
& etype(c37238,int0)
& fact(c37238,real)
& gener(c37238,gener_c)
& quant(c37238,one)
& refer(c37238,refer_c)
& varia(c37238,varia_c)
& sort(faun_1_1,o)
& card(faun_1_1,int1)
& etype(faun_1_1,int0)
& fact(faun_1_1,real)
& gener(faun_1_1,ge)
& quant(faun_1_1,one)
& refer(faun_1_1,refer_c)
& varia(faun_1_1,varia_c)
& sort(c37245,d)
& sort(c37245,io)
& card(c37245,int1)
& etype(c37245,int0)
& fact(c37245,real)
& gener(c37245,sp)
& quant(c37245,one)
& refer(c37245,det)
& varia(c37245,con)
& sort(c37246,na)
& card(c37246,int1)
& etype(c37246,int0)
& fact(c37246,real)
& gener(c37246,sp)
& quant(c37246,one)
& refer(c37246,indet)
& varia(c37246,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(n__374rnberg_0,fe)
& sort(c37268,ad)
& sort(c37268,io)
& card(c37268,int1)
& etype(c37268,int0)
& fact(c37268,real)
& gener(c37268,sp)
& quant(c37268,one)
& refer(c37268,det)
& varia(c37268,con)
& sort(c37272,ad)
& sort(c37272,io)
& card(c37272,int1)
& etype(c37272,int0)
& fact(c37272,real)
& gener(c37272,ge)
& quant(c37272,one)
& refer(c37272,refer_c)
& varia(c37272,varia_c)
& sort(ackerbautreibend_1_1,aq)
& sort(einsatz_1_1,ad)
& sort(einsatz_1_1,io)
& card(einsatz_1_1,int1)
& etype(einsatz_1_1,int0)
& fact(einsatz_1_1,real)
& gener(einsatz_1_1,ge)
& quant(einsatz_1_1,one)
& refer(einsatz_1_1,refer_c)
& varia(einsatz_1_1,varia_c)
& sort(c37274,d)
& card(c37274,int1)
& etype(c37274,int0)
& fact(c37274,real)
& gener(c37274,gener_c)
& quant(c37274,one)
& refer(c37274,refer_c)
& varia(c37274,varia_c)
& sort(fahrzeug__1_1,d)
& card(fahrzeug__1_1,int1)
& etype(fahrzeug__1_1,int0)
& fact(fahrzeug__1_1,real)
& gener(fahrzeug__1_1,ge)
& quant(fahrzeug__1_1,one)
& refer(fahrzeug__1_1,refer_c)
& varia(fahrzeug__1_1,varia_c)
& sort(c37284,ad)
& sort(c37284,d)
& sort(c37284,io)
& card(c37284,int1)
& etype(c37284,int0)
& fact(c37284,real)
& gener(c37284,sp)
& quant(c37284,one)
& refer(c37284,det)
& varia(c37284,con)
& sort(c37291,d)
& card(c37291,int4)
& etype(c37291,int1)
& fact(c37291,real)
& gener(c37291,sp)
& quant(c37291,nfquant)
& refer(c37291,det)
& varia(c37291,varia_c)
& sort(reifen__1_1,d)
& card(reifen__1_1,int1)
& etype(reifen__1_1,int0)
& fact(reifen__1_1,real)
& gener(reifen__1_1,ge)
& quant(reifen__1_1,one)
& refer(reifen__1_1,refer_c)
& varia(reifen__1_1,varia_c)
& sort(c37298,o)
& card(c37298,cons(x_constant,cons(int1,nil)))
& etype(c37298,int1)
& fact(c37298,real)
& gener(c37298,gener_c)
& quant(c37298,mult)
& refer(c37298,refer_c)
& varia(c37298,varia_c)
& sort(lypsoid_1_1,o)
& card(lypsoid_1_1,int1)
& etype(lypsoid_1_1,int0)
& fact(lypsoid_1_1,real)
& gener(lypsoid_1_1,ge)
& quant(lypsoid_1_1,one)
& refer(lypsoid_1_1,refer_c)
& varia(lypsoid_1_1,varia_c)
& sort(n22x12_1_1,gq)
& sort(c37339,co)
& sort(c37339,m)
& card(c37339,card_c)
& etype(c37339,etype_c)
& fact(c37339,real)
& gener(c37339,gener_c)
& quant(c37339,quant_c)
& refer(c37339,refer_c)
& varia(c37339,con)
& sort(c37331,nu)
& card(c37331,int26)
& sort(pferdest__344rke_1_1,me)
& gener(pferdest__344rke_1_1,ge)
& sort(c37341,d)
& card(c37341,int1)
& etype(c37341,int0)
& fact(c37341,real)
& gener(c37341,gener_c)
& quant(c37341,one)
& refer(c37341,refer_c)
& varia(c37341,varia_c)
& sort(c37229,tq)
& sort(bmw_1_1,d)
& card(bmw_1_1,int1)
& etype(bmw_1_1,int0)
& fact(bmw_1_1,real)
& gener(bmw_1_1,ge)
& quant(bmw_1_1,one)
& refer(bmw_1_1,refer_c)
& varia(bmw_1_1,varia_c)
& sort(c37345,d)
& card(c37345,int1)
& etype(c37345,int0)
& fact(c37345,real)
& gener(c37345,gener_c)
& quant(c37345,one)
& refer(c37345,refer_c)
& varia(c37345,varia_c)
& sort(c37359,io)
& card(c37359,int1)
& etype(c37359,int0)
& fact(c37359,real)
& gener(c37359,gener_c)
& quant(c37359,one)
& refer(c37359,refer_c)
& varia(c37359,varia_c)
& sort(last_1_1,io)
& card(last_1_1,int1)
& etype(last_1_1,int0)
& fact(last_1_1,real)
& gener(last_1_1,ge)
& quant(last_1_1,one)
& refer(last_1_1,refer_c)
& varia(last_1_1,varia_c)
& sort(c37361,co)
& sort(c37361,m)
& card(c37361,card_c)
& etype(c37361,etype_c)
& fact(c37361,real)
& gener(c37361,gener_c)
& quant(c37361,quant_c)
& refer(c37361,refer_c)
& varia(c37361,con)
& sort(c37356,nu)
& card(c37356,int750)
& sort(kilo__1_1,me)
& gener(kilo__1_1,ge)
& sort(c37402,ent)
& card(c37402,card_c)
& etype(c37402,etype_c)
& fact(c37402,real)
& gener(c37402,gener_c)
& quant(c37402,quant_c)
& refer(c37402,refer_c)
& varia(c37402,varia_c)
& sort(c37233,o)
& card(c37233,int1)
& etype(c37233,int0)
& fact(c37233,real)
& gener(c37233,sp)
& quant(c37233,one)
& refer(c37233,det)
& varia(c37233,varia_c)
& sort(c37313,o)
& card(c37313,int1)
& etype(c37313,int0)
& fact(c37313,real)
& gener(c37313,gener_c)
& quant(c37313,one)
& refer(c37313,refer_c)
& varia(c37313,varia_c)
& sort(drosseln_1_1,da)
& fact(drosseln_1_1,real)
& gener(drosseln_1_1,ge) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10192,plain,
( assoc(boxermotor_1_1,boxer_2_1)
& sub(boxermotor_1_1,motor__1_1)
& assoc(bundeswehrausf__374hrung_1_1,bundeswehr_1_1)
& sub(bundeswehrausf__374hrung_1_1,ausf__374hrung_1_1)
& sub(c37238,faun_1_1)
& attr(c37245,c37246)
& sub(c37245,stadt__1_1)
& sub(c37246,name_1_1)
& val(c37246,n__374rnberg_0)
& sub(c37268,c37272)
& pmod(c37272,ackerbautreibend_1_1,einsatz_1_1)
& sub(c37274,fahrzeug__1_1)
& sub(c37284,bundeswehrausf__374hrung_1_1)
& pred(c37291,reifen__1_1)
& attch(c37298,c37291)
& pred(c37298,lypsoid_1_1)
& prop(c37298,n22x12_1_1)
& prop(c37341,c37229)
& sub(c37341,bmw_1_1)
& sub(c37345,boxermotor_1_1)
& sub(c37359,last_1_1)
& chsp2(drosseln_1_1,c37229)
& sort(boxermotor_1_1,d)
& card(boxermotor_1_1,int1)
& etype(boxermotor_1_1,int0)
& fact(boxermotor_1_1,real)
& gener(boxermotor_1_1,ge)
& quant(boxermotor_1_1,one)
& refer(boxermotor_1_1,refer_c)
& varia(boxermotor_1_1,varia_c)
& sort(boxer_2_1,d)
& card(boxer_2_1,int1)
& etype(boxer_2_1,int0)
& fact(boxer_2_1,real)
& gener(boxer_2_1,ge)
& quant(boxer_2_1,one)
& refer(boxer_2_1,refer_c)
& varia(boxer_2_1,varia_c)
& sort(motor__1_1,d)
& card(motor__1_1,int1)
& etype(motor__1_1,int0)
& fact(motor__1_1,real)
& gener(motor__1_1,ge)
& quant(motor__1_1,one)
& refer(motor__1_1,refer_c)
& varia(motor__1_1,varia_c)
& sort(bundeswehrausf__374hrung_1_1,ad)
& sort(bundeswehrausf__374hrung_1_1,d)
& sort(bundeswehrausf__374hrung_1_1,io)
& card(bundeswehrausf__374hrung_1_1,int1)
& etype(bundeswehrausf__374hrung_1_1,int0)
& fact(bundeswehrausf__374hrung_1_1,real)
& gener(bundeswehrausf__374hrung_1_1,ge)
& quant(bundeswehrausf__374hrung_1_1,one)
& refer(bundeswehrausf__374hrung_1_1,refer_c)
& varia(bundeswehrausf__374hrung_1_1,varia_c)
& sort(bundeswehr_1_1,d)
& sort(bundeswehr_1_1,io)
& card(bundeswehr_1_1,card_c)
& etype(bundeswehr_1_1,int1)
& fact(bundeswehr_1_1,real)
& gener(bundeswehr_1_1,ge)
& quant(bundeswehr_1_1,quant_c)
& refer(bundeswehr_1_1,refer_c)
& varia(bundeswehr_1_1,varia_c)
& sort(ausf__374hrung_1_1,ad)
& sort(ausf__374hrung_1_1,d)
& sort(ausf__374hrung_1_1,io)
& card(ausf__374hrung_1_1,int1)
& etype(ausf__374hrung_1_1,int0)
& fact(ausf__374hrung_1_1,real)
& gener(ausf__374hrung_1_1,ge)
& quant(ausf__374hrung_1_1,one)
& refer(ausf__374hrung_1_1,refer_c)
& varia(ausf__374hrung_1_1,varia_c)
& sort(c37238,o)
& card(c37238,int1)
& etype(c37238,int0)
& fact(c37238,real)
& gener(c37238,gener_c)
& quant(c37238,one)
& refer(c37238,refer_c)
& varia(c37238,varia_c)
& sort(faun_1_1,o)
& card(faun_1_1,int1)
& etype(faun_1_1,int0)
& fact(faun_1_1,real)
& gener(faun_1_1,ge)
& quant(faun_1_1,one)
& refer(faun_1_1,refer_c)
& varia(faun_1_1,varia_c)
& sort(c37245,d)
& sort(c37245,io)
& card(c37245,int1)
& etype(c37245,int0)
& fact(c37245,real)
& gener(c37245,sp)
& quant(c37245,one)
& refer(c37245,det)
& varia(c37245,con)
& sort(c37246,na)
& card(c37246,int1)
& etype(c37246,int0)
& fact(c37246,real)
& gener(c37246,sp)
& quant(c37246,one)
& refer(c37246,indet)
& varia(c37246,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(n__374rnberg_0,fe)
& sort(c37268,ad)
& sort(c37268,io)
& card(c37268,int1)
& etype(c37268,int0)
& fact(c37268,real)
& gener(c37268,sp)
& quant(c37268,one)
& refer(c37268,det)
& varia(c37268,con)
& sort(c37272,ad)
& sort(c37272,io)
& card(c37272,int1)
& etype(c37272,int0)
& fact(c37272,real)
& gener(c37272,ge)
& quant(c37272,one)
& refer(c37272,refer_c)
& varia(c37272,varia_c)
& sort(ackerbautreibend_1_1,aq)
& sort(einsatz_1_1,ad)
& sort(einsatz_1_1,io)
& card(einsatz_1_1,int1)
& etype(einsatz_1_1,int0)
& fact(einsatz_1_1,real)
& gener(einsatz_1_1,ge)
& quant(einsatz_1_1,one)
& refer(einsatz_1_1,refer_c)
& varia(einsatz_1_1,varia_c)
& sort(c37274,d)
& card(c37274,int1)
& etype(c37274,int0)
& fact(c37274,real)
& gener(c37274,gener_c)
& quant(c37274,one)
& refer(c37274,refer_c)
& varia(c37274,varia_c)
& sort(fahrzeug__1_1,d)
& card(fahrzeug__1_1,int1)
& etype(fahrzeug__1_1,int0)
& fact(fahrzeug__1_1,real)
& gener(fahrzeug__1_1,ge)
& quant(fahrzeug__1_1,one)
& refer(fahrzeug__1_1,refer_c)
& varia(fahrzeug__1_1,varia_c)
& sort(c37284,ad)
& sort(c37284,d)
& sort(c37284,io)
& card(c37284,int1)
& etype(c37284,int0)
& fact(c37284,real)
& gener(c37284,sp)
& quant(c37284,one)
& refer(c37284,det)
& varia(c37284,con)
& sort(c37291,d)
& card(c37291,int4)
& etype(c37291,int1)
& fact(c37291,real)
& gener(c37291,sp)
& quant(c37291,nfquant)
& refer(c37291,det)
& varia(c37291,varia_c)
& sort(reifen__1_1,d)
& card(reifen__1_1,int1)
& etype(reifen__1_1,int0)
& fact(reifen__1_1,real)
& gener(reifen__1_1,ge)
& quant(reifen__1_1,one)
& refer(reifen__1_1,refer_c)
& varia(reifen__1_1,varia_c)
& sort(c37298,o)
& card(c37298,cons(x_constant,cons(int1,nil)))
& etype(c37298,int1)
& fact(c37298,real)
& gener(c37298,gener_c)
& quant(c37298,mult)
& refer(c37298,refer_c)
& varia(c37298,varia_c)
& sort(lypsoid_1_1,o)
& card(lypsoid_1_1,int1)
& etype(lypsoid_1_1,int0)
& fact(lypsoid_1_1,real)
& gener(lypsoid_1_1,ge)
& quant(lypsoid_1_1,one)
& refer(lypsoid_1_1,refer_c)
& varia(lypsoid_1_1,varia_c)
& sort(n22x12_1_1,gq)
& sort(c37339,co)
& sort(c37339,m)
& card(c37339,card_c)
& etype(c37339,etype_c)
& fact(c37339,real)
& gener(c37339,gener_c)
& quant(c37339,quant_c)
& refer(c37339,refer_c)
& varia(c37339,con)
& sort(c37331,nu)
& card(c37331,int26)
& sort(pferdest__344rke_1_1,me)
& gener(pferdest__344rke_1_1,ge)
& sort(c37341,d)
& card(c37341,int1)
& etype(c37341,int0)
& fact(c37341,real)
& gener(c37341,gener_c)
& quant(c37341,one)
& refer(c37341,refer_c)
& varia(c37341,varia_c)
& sort(c37229,tq)
& sort(bmw_1_1,d)
& card(bmw_1_1,int1)
& etype(bmw_1_1,int0)
& fact(bmw_1_1,real)
& gener(bmw_1_1,ge)
& quant(bmw_1_1,one)
& refer(bmw_1_1,refer_c)
& varia(bmw_1_1,varia_c)
& sort(c37345,d)
& card(c37345,int1)
& etype(c37345,int0)
& fact(c37345,real)
& gener(c37345,gener_c)
& quant(c37345,one)
& refer(c37345,refer_c)
& varia(c37345,varia_c)
& sort(c37359,io)
& card(c37359,int1)
& etype(c37359,int0)
& fact(c37359,real)
& gener(c37359,gener_c)
& quant(c37359,one)
& refer(c37359,refer_c)
& varia(c37359,varia_c)
& sort(last_1_1,io)
& card(last_1_1,int1)
& etype(last_1_1,int0)
& fact(last_1_1,real)
& gener(last_1_1,ge)
& quant(last_1_1,one)
& refer(last_1_1,refer_c)
& varia(last_1_1,varia_c)
& sort(c37361,co)
& sort(c37361,m)
& card(c37361,card_c)
& etype(c37361,etype_c)
& fact(c37361,real)
& gener(c37361,gener_c)
& quant(c37361,quant_c)
& refer(c37361,refer_c)
& varia(c37361,con)
& sort(c37356,nu)
& card(c37356,int750)
& sort(kilo__1_1,me)
& gener(kilo__1_1,ge)
& sort(c37402,ent)
& card(c37402,card_c)
& etype(c37402,etype_c)
& fact(c37402,real)
& gener(c37402,gener_c)
& quant(c37402,quant_c)
& refer(c37402,refer_c)
& varia(c37402,varia_c)
& sort(c37233,o)
& card(c37233,int1)
& etype(c37233,int0)
& fact(c37233,real)
& gener(c37233,sp)
& quant(c37233,one)
& refer(c37233,det)
& varia(c37233,varia_c)
& sort(c37313,o)
& card(c37313,int1)
& etype(c37313,int0)
& fact(c37313,real)
& gener(c37313,gener_c)
& quant(c37313,one)
& refer(c37313,refer_c)
& varia(c37313,varia_c)
& sort(drosseln_1_1,da)
& fact(drosseln_1_1,real)
& gener(drosseln_1_1,ge) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10323,plain,
( assoc(boxermotor_1_1,boxer_2_1)
& sub(boxermotor_1_1,motor__1_1)
& assoc(bundeswehrausf__374hrung_1_1,bundeswehr_1_1)
& sub(bundeswehrausf__374hrung_1_1,ausf__374hrung_1_1)
& sub(c37238,faun_1_1)
& attr(c37245,c37246)
& sub(c37245,stadt__1_1)
& sub(c37246,name_1_1)
& val(c37246,n__374rnberg_0)
& sub(c37268,c37272)
& pmod(c37272,ackerbautreibend_1_1,einsatz_1_1)
& sub(c37274,fahrzeug__1_1)
& sub(c37284,bundeswehrausf__374hrung_1_1)
& pred(c37291,reifen__1_1)
& attch(c37298,c37291)
& pred(c37298,lypsoid_1_1)
& prop(c37298,n22x12_1_1)
& prop(c37341,c37229)
& sub(c37341,bmw_1_1)
& sub(c37345,boxermotor_1_1)
& sub(c37359,last_1_1)
& sort(boxermotor_1_1,d)
& card(boxermotor_1_1,int1)
& etype(boxermotor_1_1,int0)
& fact(boxermotor_1_1,real)
& gener(boxermotor_1_1,ge)
& quant(boxermotor_1_1,one)
& refer(boxermotor_1_1,refer_c)
& varia(boxermotor_1_1,varia_c)
& sort(boxer_2_1,d)
& card(boxer_2_1,int1)
& etype(boxer_2_1,int0)
& fact(boxer_2_1,real)
& gener(boxer_2_1,ge)
& quant(boxer_2_1,one)
& refer(boxer_2_1,refer_c)
& varia(boxer_2_1,varia_c)
& sort(motor__1_1,d)
& card(motor__1_1,int1)
& etype(motor__1_1,int0)
& fact(motor__1_1,real)
& gener(motor__1_1,ge)
& quant(motor__1_1,one)
& refer(motor__1_1,refer_c)
& varia(motor__1_1,varia_c)
& sort(bundeswehrausf__374hrung_1_1,ad)
& sort(bundeswehrausf__374hrung_1_1,d)
& sort(bundeswehrausf__374hrung_1_1,io)
& card(bundeswehrausf__374hrung_1_1,int1)
& etype(bundeswehrausf__374hrung_1_1,int0)
& fact(bundeswehrausf__374hrung_1_1,real)
& gener(bundeswehrausf__374hrung_1_1,ge)
& quant(bundeswehrausf__374hrung_1_1,one)
& refer(bundeswehrausf__374hrung_1_1,refer_c)
& varia(bundeswehrausf__374hrung_1_1,varia_c)
& sort(bundeswehr_1_1,d)
& sort(bundeswehr_1_1,io)
& card(bundeswehr_1_1,card_c)
& etype(bundeswehr_1_1,int1)
& fact(bundeswehr_1_1,real)
& gener(bundeswehr_1_1,ge)
& quant(bundeswehr_1_1,quant_c)
& refer(bundeswehr_1_1,refer_c)
& varia(bundeswehr_1_1,varia_c)
& sort(ausf__374hrung_1_1,ad)
& sort(ausf__374hrung_1_1,d)
& sort(ausf__374hrung_1_1,io)
& card(ausf__374hrung_1_1,int1)
& etype(ausf__374hrung_1_1,int0)
& fact(ausf__374hrung_1_1,real)
& gener(ausf__374hrung_1_1,ge)
& quant(ausf__374hrung_1_1,one)
& refer(ausf__374hrung_1_1,refer_c)
& varia(ausf__374hrung_1_1,varia_c)
& sort(c37238,o)
& card(c37238,int1)
& etype(c37238,int0)
& fact(c37238,real)
& gener(c37238,gener_c)
& quant(c37238,one)
& refer(c37238,refer_c)
& varia(c37238,varia_c)
& sort(faun_1_1,o)
& card(faun_1_1,int1)
& etype(faun_1_1,int0)
& fact(faun_1_1,real)
& gener(faun_1_1,ge)
& quant(faun_1_1,one)
& refer(faun_1_1,refer_c)
& varia(faun_1_1,varia_c)
& sort(c37245,d)
& sort(c37245,io)
& card(c37245,int1)
& etype(c37245,int0)
& fact(c37245,real)
& gener(c37245,sp)
& quant(c37245,one)
& refer(c37245,det)
& varia(c37245,con)
& sort(c37246,na)
& card(c37246,int1)
& etype(c37246,int0)
& fact(c37246,real)
& gener(c37246,sp)
& quant(c37246,one)
& refer(c37246,indet)
& varia(c37246,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(n__374rnberg_0,fe)
& sort(c37268,ad)
& sort(c37268,io)
& card(c37268,int1)
& etype(c37268,int0)
& fact(c37268,real)
& gener(c37268,sp)
& quant(c37268,one)
& refer(c37268,det)
& varia(c37268,con)
& sort(c37272,ad)
& sort(c37272,io)
& card(c37272,int1)
& etype(c37272,int0)
& fact(c37272,real)
& gener(c37272,ge)
& quant(c37272,one)
& refer(c37272,refer_c)
& varia(c37272,varia_c)
& sort(ackerbautreibend_1_1,aq)
& sort(einsatz_1_1,ad)
& sort(einsatz_1_1,io)
& card(einsatz_1_1,int1)
& etype(einsatz_1_1,int0)
& fact(einsatz_1_1,real)
& gener(einsatz_1_1,ge)
& quant(einsatz_1_1,one)
& refer(einsatz_1_1,refer_c)
& varia(einsatz_1_1,varia_c)
& sort(c37274,d)
& card(c37274,int1)
& etype(c37274,int0)
& fact(c37274,real)
& gener(c37274,gener_c)
& quant(c37274,one)
& refer(c37274,refer_c)
& varia(c37274,varia_c)
& sort(fahrzeug__1_1,d)
& card(fahrzeug__1_1,int1)
& etype(fahrzeug__1_1,int0)
& fact(fahrzeug__1_1,real)
& gener(fahrzeug__1_1,ge)
& quant(fahrzeug__1_1,one)
& refer(fahrzeug__1_1,refer_c)
& varia(fahrzeug__1_1,varia_c)
& sort(c37284,ad)
& sort(c37284,d)
& sort(c37284,io)
& card(c37284,int1)
& etype(c37284,int0)
& fact(c37284,real)
& gener(c37284,sp)
& quant(c37284,one)
& refer(c37284,det)
& varia(c37284,con)
& sort(c37291,d)
& card(c37291,int4)
& etype(c37291,int1)
& fact(c37291,real)
& gener(c37291,sp)
& quant(c37291,nfquant)
& refer(c37291,det)
& varia(c37291,varia_c)
& sort(reifen__1_1,d)
& card(reifen__1_1,int1)
& etype(reifen__1_1,int0)
& fact(reifen__1_1,real)
& gener(reifen__1_1,ge)
& quant(reifen__1_1,one)
& refer(reifen__1_1,refer_c)
& varia(reifen__1_1,varia_c)
& sort(c37298,o)
& card(c37298,cons(x_constant,cons(int1,nil)))
& etype(c37298,int1)
& fact(c37298,real)
& gener(c37298,gener_c)
& quant(c37298,mult)
& refer(c37298,refer_c)
& varia(c37298,varia_c)
& sort(lypsoid_1_1,o)
& card(lypsoid_1_1,int1)
& etype(lypsoid_1_1,int0)
& fact(lypsoid_1_1,real)
& gener(lypsoid_1_1,ge)
& quant(lypsoid_1_1,one)
& refer(lypsoid_1_1,refer_c)
& varia(lypsoid_1_1,varia_c)
& sort(n22x12_1_1,gq)
& sort(c37339,co)
& sort(c37339,m)
& card(c37339,card_c)
& etype(c37339,etype_c)
& fact(c37339,real)
& gener(c37339,gener_c)
& quant(c37339,quant_c)
& refer(c37339,refer_c)
& varia(c37339,con)
& sort(c37331,nu)
& card(c37331,int26)
& sort(pferdest__344rke_1_1,me)
& gener(pferdest__344rke_1_1,ge)
& sort(c37341,d)
& card(c37341,int1)
& etype(c37341,int0)
& fact(c37341,real)
& gener(c37341,gener_c)
& quant(c37341,one)
& refer(c37341,refer_c)
& varia(c37341,varia_c)
& sort(c37229,tq)
& sort(bmw_1_1,d)
& card(bmw_1_1,int1)
& etype(bmw_1_1,int0)
& fact(bmw_1_1,real)
& gener(bmw_1_1,ge)
& quant(bmw_1_1,one)
& refer(bmw_1_1,refer_c)
& varia(bmw_1_1,varia_c)
& sort(c37345,d)
& card(c37345,int1)
& etype(c37345,int0)
& fact(c37345,real)
& gener(c37345,gener_c)
& quant(c37345,one)
& refer(c37345,refer_c)
& varia(c37345,varia_c)
& sort(c37359,io)
& card(c37359,int1)
& etype(c37359,int0)
& fact(c37359,real)
& gener(c37359,gener_c)
& quant(c37359,one)
& refer(c37359,refer_c)
& varia(c37359,varia_c)
& sort(last_1_1,io)
& card(last_1_1,int1)
& etype(last_1_1,int0)
& fact(last_1_1,real)
& gener(last_1_1,ge)
& quant(last_1_1,one)
& refer(last_1_1,refer_c)
& varia(last_1_1,varia_c)
& sort(c37361,co)
& sort(c37361,m)
& card(c37361,card_c)
& etype(c37361,etype_c)
& fact(c37361,real)
& gener(c37361,gener_c)
& quant(c37361,quant_c)
& refer(c37361,refer_c)
& varia(c37361,con)
& sort(c37356,nu)
& card(c37356,int750)
& sort(kilo__1_1,me)
& gener(kilo__1_1,ge)
& sort(c37402,ent)
& card(c37402,card_c)
& etype(c37402,etype_c)
& fact(c37402,real)
& gener(c37402,gener_c)
& quant(c37402,quant_c)
& refer(c37402,refer_c)
& varia(c37402,varia_c)
& sort(c37233,o)
& card(c37233,int1)
& etype(c37233,int0)
& fact(c37233,real)
& gener(c37233,sp)
& quant(c37233,one)
& refer(c37233,det)
& varia(c37233,varia_c)
& sort(c37313,o)
& card(c37313,int1)
& etype(c37313,int0)
& fact(c37313,real)
& gener(c37313,gener_c)
& quant(c37313,one)
& refer(c37313,refer_c)
& varia(c37313,varia_c)
& sort(drosseln_1_1,da)
& fact(drosseln_1_1,real)
& gener(drosseln_1_1,ge) ),
inference(pure_predicate_removal,[],[f10192]) ).
fof(f10329,plain,
( assoc(boxermotor_1_1,boxer_2_1)
& sub(boxermotor_1_1,motor__1_1)
& assoc(bundeswehrausf__374hrung_1_1,bundeswehr_1_1)
& sub(bundeswehrausf__374hrung_1_1,ausf__374hrung_1_1)
& sub(c37238,faun_1_1)
& attr(c37245,c37246)
& sub(c37245,stadt__1_1)
& sub(c37246,name_1_1)
& val(c37246,n__374rnberg_0)
& sub(c37268,c37272)
& pmod(c37272,ackerbautreibend_1_1,einsatz_1_1)
& sub(c37274,fahrzeug__1_1)
& sub(c37284,bundeswehrausf__374hrung_1_1)
& pred(c37291,reifen__1_1)
& attch(c37298,c37291)
& pred(c37298,lypsoid_1_1)
& prop(c37298,n22x12_1_1)
& prop(c37341,c37229)
& sub(c37341,bmw_1_1)
& sub(c37345,boxermotor_1_1)
& sub(c37359,last_1_1)
& card(boxermotor_1_1,int1)
& etype(boxermotor_1_1,int0)
& fact(boxermotor_1_1,real)
& gener(boxermotor_1_1,ge)
& quant(boxermotor_1_1,one)
& refer(boxermotor_1_1,refer_c)
& varia(boxermotor_1_1,varia_c)
& card(boxer_2_1,int1)
& etype(boxer_2_1,int0)
& fact(boxer_2_1,real)
& gener(boxer_2_1,ge)
& quant(boxer_2_1,one)
& refer(boxer_2_1,refer_c)
& varia(boxer_2_1,varia_c)
& card(motor__1_1,int1)
& etype(motor__1_1,int0)
& fact(motor__1_1,real)
& gener(motor__1_1,ge)
& quant(motor__1_1,one)
& refer(motor__1_1,refer_c)
& varia(motor__1_1,varia_c)
& card(bundeswehrausf__374hrung_1_1,int1)
& etype(bundeswehrausf__374hrung_1_1,int0)
& fact(bundeswehrausf__374hrung_1_1,real)
& gener(bundeswehrausf__374hrung_1_1,ge)
& quant(bundeswehrausf__374hrung_1_1,one)
& refer(bundeswehrausf__374hrung_1_1,refer_c)
& varia(bundeswehrausf__374hrung_1_1,varia_c)
& card(bundeswehr_1_1,card_c)
& etype(bundeswehr_1_1,int1)
& fact(bundeswehr_1_1,real)
& gener(bundeswehr_1_1,ge)
& quant(bundeswehr_1_1,quant_c)
& refer(bundeswehr_1_1,refer_c)
& varia(bundeswehr_1_1,varia_c)
& card(ausf__374hrung_1_1,int1)
& etype(ausf__374hrung_1_1,int0)
& fact(ausf__374hrung_1_1,real)
& gener(ausf__374hrung_1_1,ge)
& quant(ausf__374hrung_1_1,one)
& refer(ausf__374hrung_1_1,refer_c)
& varia(ausf__374hrung_1_1,varia_c)
& card(c37238,int1)
& etype(c37238,int0)
& fact(c37238,real)
& gener(c37238,gener_c)
& quant(c37238,one)
& refer(c37238,refer_c)
& varia(c37238,varia_c)
& card(faun_1_1,int1)
& etype(faun_1_1,int0)
& fact(faun_1_1,real)
& gener(faun_1_1,ge)
& quant(faun_1_1,one)
& refer(faun_1_1,refer_c)
& varia(faun_1_1,varia_c)
& card(c37245,int1)
& etype(c37245,int0)
& fact(c37245,real)
& gener(c37245,sp)
& quant(c37245,one)
& refer(c37245,det)
& varia(c37245,con)
& card(c37246,int1)
& etype(c37246,int0)
& fact(c37246,real)
& gener(c37246,sp)
& quant(c37246,one)
& refer(c37246,indet)
& varia(c37246,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(c37268,int1)
& etype(c37268,int0)
& fact(c37268,real)
& gener(c37268,sp)
& quant(c37268,one)
& refer(c37268,det)
& varia(c37268,con)
& card(c37272,int1)
& etype(c37272,int0)
& fact(c37272,real)
& gener(c37272,ge)
& quant(c37272,one)
& refer(c37272,refer_c)
& varia(c37272,varia_c)
& card(einsatz_1_1,int1)
& etype(einsatz_1_1,int0)
& fact(einsatz_1_1,real)
& gener(einsatz_1_1,ge)
& quant(einsatz_1_1,one)
& refer(einsatz_1_1,refer_c)
& varia(einsatz_1_1,varia_c)
& card(c37274,int1)
& etype(c37274,int0)
& fact(c37274,real)
& gener(c37274,gener_c)
& quant(c37274,one)
& refer(c37274,refer_c)
& varia(c37274,varia_c)
& card(fahrzeug__1_1,int1)
& etype(fahrzeug__1_1,int0)
& fact(fahrzeug__1_1,real)
& gener(fahrzeug__1_1,ge)
& quant(fahrzeug__1_1,one)
& refer(fahrzeug__1_1,refer_c)
& varia(fahrzeug__1_1,varia_c)
& card(c37284,int1)
& etype(c37284,int0)
& fact(c37284,real)
& gener(c37284,sp)
& quant(c37284,one)
& refer(c37284,det)
& varia(c37284,con)
& card(c37291,int4)
& etype(c37291,int1)
& fact(c37291,real)
& gener(c37291,sp)
& quant(c37291,nfquant)
& refer(c37291,det)
& varia(c37291,varia_c)
& card(reifen__1_1,int1)
& etype(reifen__1_1,int0)
& fact(reifen__1_1,real)
& gener(reifen__1_1,ge)
& quant(reifen__1_1,one)
& refer(reifen__1_1,refer_c)
& varia(reifen__1_1,varia_c)
& card(c37298,cons(x_constant,cons(int1,nil)))
& etype(c37298,int1)
& fact(c37298,real)
& gener(c37298,gener_c)
& quant(c37298,mult)
& refer(c37298,refer_c)
& varia(c37298,varia_c)
& card(lypsoid_1_1,int1)
& etype(lypsoid_1_1,int0)
& fact(lypsoid_1_1,real)
& gener(lypsoid_1_1,ge)
& quant(lypsoid_1_1,one)
& refer(lypsoid_1_1,refer_c)
& varia(lypsoid_1_1,varia_c)
& card(c37339,card_c)
& etype(c37339,etype_c)
& fact(c37339,real)
& gener(c37339,gener_c)
& quant(c37339,quant_c)
& refer(c37339,refer_c)
& varia(c37339,con)
& card(c37331,int26)
& gener(pferdest__344rke_1_1,ge)
& card(c37341,int1)
& etype(c37341,int0)
& fact(c37341,real)
& gener(c37341,gener_c)
& quant(c37341,one)
& refer(c37341,refer_c)
& varia(c37341,varia_c)
& card(bmw_1_1,int1)
& etype(bmw_1_1,int0)
& fact(bmw_1_1,real)
& gener(bmw_1_1,ge)
& quant(bmw_1_1,one)
& refer(bmw_1_1,refer_c)
& varia(bmw_1_1,varia_c)
& card(c37345,int1)
& etype(c37345,int0)
& fact(c37345,real)
& gener(c37345,gener_c)
& quant(c37345,one)
& refer(c37345,refer_c)
& varia(c37345,varia_c)
& card(c37359,int1)
& etype(c37359,int0)
& fact(c37359,real)
& gener(c37359,gener_c)
& quant(c37359,one)
& refer(c37359,refer_c)
& varia(c37359,varia_c)
& card(last_1_1,int1)
& etype(last_1_1,int0)
& fact(last_1_1,real)
& gener(last_1_1,ge)
& quant(last_1_1,one)
& refer(last_1_1,refer_c)
& varia(last_1_1,varia_c)
& card(c37361,card_c)
& etype(c37361,etype_c)
& fact(c37361,real)
& gener(c37361,gener_c)
& quant(c37361,quant_c)
& refer(c37361,refer_c)
& varia(c37361,con)
& card(c37356,int750)
& gener(kilo__1_1,ge)
& card(c37402,card_c)
& etype(c37402,etype_c)
& fact(c37402,real)
& gener(c37402,gener_c)
& quant(c37402,quant_c)
& refer(c37402,refer_c)
& varia(c37402,varia_c)
& card(c37233,int1)
& etype(c37233,int0)
& fact(c37233,real)
& gener(c37233,sp)
& quant(c37233,one)
& refer(c37233,det)
& varia(c37233,varia_c)
& card(c37313,int1)
& etype(c37313,int0)
& fact(c37313,real)
& gener(c37313,gener_c)
& quant(c37313,one)
& refer(c37313,refer_c)
& varia(c37313,varia_c)
& fact(drosseln_1_1,real)
& gener(drosseln_1_1,ge) ),
inference(pure_predicate_removal,[],[f10323]) ).
fof(f10332,plain,
( assoc(boxermotor_1_1,boxer_2_1)
& sub(boxermotor_1_1,motor__1_1)
& assoc(bundeswehrausf__374hrung_1_1,bundeswehr_1_1)
& sub(bundeswehrausf__374hrung_1_1,ausf__374hrung_1_1)
& sub(c37238,faun_1_1)
& attr(c37245,c37246)
& sub(c37245,stadt__1_1)
& sub(c37246,name_1_1)
& val(c37246,n__374rnberg_0)
& sub(c37268,c37272)
& pmod(c37272,ackerbautreibend_1_1,einsatz_1_1)
& sub(c37274,fahrzeug__1_1)
& sub(c37284,bundeswehrausf__374hrung_1_1)
& pred(c37291,reifen__1_1)
& attch(c37298,c37291)
& pred(c37298,lypsoid_1_1)
& prop(c37298,n22x12_1_1)
& prop(c37341,c37229)
& sub(c37341,bmw_1_1)
& sub(c37345,boxermotor_1_1)
& sub(c37359,last_1_1)
& card(boxermotor_1_1,int1)
& etype(boxermotor_1_1,int0)
& fact(boxermotor_1_1,real)
& gener(boxermotor_1_1,ge)
& refer(boxermotor_1_1,refer_c)
& varia(boxermotor_1_1,varia_c)
& card(boxer_2_1,int1)
& etype(boxer_2_1,int0)
& fact(boxer_2_1,real)
& gener(boxer_2_1,ge)
& refer(boxer_2_1,refer_c)
& varia(boxer_2_1,varia_c)
& card(motor__1_1,int1)
& etype(motor__1_1,int0)
& fact(motor__1_1,real)
& gener(motor__1_1,ge)
& refer(motor__1_1,refer_c)
& varia(motor__1_1,varia_c)
& card(bundeswehrausf__374hrung_1_1,int1)
& etype(bundeswehrausf__374hrung_1_1,int0)
& fact(bundeswehrausf__374hrung_1_1,real)
& gener(bundeswehrausf__374hrung_1_1,ge)
& refer(bundeswehrausf__374hrung_1_1,refer_c)
& varia(bundeswehrausf__374hrung_1_1,varia_c)
& card(bundeswehr_1_1,card_c)
& etype(bundeswehr_1_1,int1)
& fact(bundeswehr_1_1,real)
& gener(bundeswehr_1_1,ge)
& refer(bundeswehr_1_1,refer_c)
& varia(bundeswehr_1_1,varia_c)
& card(ausf__374hrung_1_1,int1)
& etype(ausf__374hrung_1_1,int0)
& fact(ausf__374hrung_1_1,real)
& gener(ausf__374hrung_1_1,ge)
& refer(ausf__374hrung_1_1,refer_c)
& varia(ausf__374hrung_1_1,varia_c)
& card(c37238,int1)
& etype(c37238,int0)
& fact(c37238,real)
& gener(c37238,gener_c)
& refer(c37238,refer_c)
& varia(c37238,varia_c)
& card(faun_1_1,int1)
& etype(faun_1_1,int0)
& fact(faun_1_1,real)
& gener(faun_1_1,ge)
& refer(faun_1_1,refer_c)
& varia(faun_1_1,varia_c)
& card(c37245,int1)
& etype(c37245,int0)
& fact(c37245,real)
& gener(c37245,sp)
& refer(c37245,det)
& varia(c37245,con)
& card(c37246,int1)
& etype(c37246,int0)
& fact(c37246,real)
& gener(c37246,sp)
& refer(c37246,indet)
& varia(c37246,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(c37268,int1)
& etype(c37268,int0)
& fact(c37268,real)
& gener(c37268,sp)
& refer(c37268,det)
& varia(c37268,con)
& card(c37272,int1)
& etype(c37272,int0)
& fact(c37272,real)
& gener(c37272,ge)
& refer(c37272,refer_c)
& varia(c37272,varia_c)
& card(einsatz_1_1,int1)
& etype(einsatz_1_1,int0)
& fact(einsatz_1_1,real)
& gener(einsatz_1_1,ge)
& refer(einsatz_1_1,refer_c)
& varia(einsatz_1_1,varia_c)
& card(c37274,int1)
& etype(c37274,int0)
& fact(c37274,real)
& gener(c37274,gener_c)
& refer(c37274,refer_c)
& varia(c37274,varia_c)
& card(fahrzeug__1_1,int1)
& etype(fahrzeug__1_1,int0)
& fact(fahrzeug__1_1,real)
& gener(fahrzeug__1_1,ge)
& refer(fahrzeug__1_1,refer_c)
& varia(fahrzeug__1_1,varia_c)
& card(c37284,int1)
& etype(c37284,int0)
& fact(c37284,real)
& gener(c37284,sp)
& refer(c37284,det)
& varia(c37284,con)
& card(c37291,int4)
& etype(c37291,int1)
& fact(c37291,real)
& gener(c37291,sp)
& refer(c37291,det)
& varia(c37291,varia_c)
& card(reifen__1_1,int1)
& etype(reifen__1_1,int0)
& fact(reifen__1_1,real)
& gener(reifen__1_1,ge)
& refer(reifen__1_1,refer_c)
& varia(reifen__1_1,varia_c)
& card(c37298,cons(x_constant,cons(int1,nil)))
& etype(c37298,int1)
& fact(c37298,real)
& gener(c37298,gener_c)
& refer(c37298,refer_c)
& varia(c37298,varia_c)
& card(lypsoid_1_1,int1)
& etype(lypsoid_1_1,int0)
& fact(lypsoid_1_1,real)
& gener(lypsoid_1_1,ge)
& refer(lypsoid_1_1,refer_c)
& varia(lypsoid_1_1,varia_c)
& card(c37339,card_c)
& etype(c37339,etype_c)
& fact(c37339,real)
& gener(c37339,gener_c)
& refer(c37339,refer_c)
& varia(c37339,con)
& card(c37331,int26)
& gener(pferdest__344rke_1_1,ge)
& card(c37341,int1)
& etype(c37341,int0)
& fact(c37341,real)
& gener(c37341,gener_c)
& refer(c37341,refer_c)
& varia(c37341,varia_c)
& card(bmw_1_1,int1)
& etype(bmw_1_1,int0)
& fact(bmw_1_1,real)
& gener(bmw_1_1,ge)
& refer(bmw_1_1,refer_c)
& varia(bmw_1_1,varia_c)
& card(c37345,int1)
& etype(c37345,int0)
& fact(c37345,real)
& gener(c37345,gener_c)
& refer(c37345,refer_c)
& varia(c37345,varia_c)
& card(c37359,int1)
& etype(c37359,int0)
& fact(c37359,real)
& gener(c37359,gener_c)
& refer(c37359,refer_c)
& varia(c37359,varia_c)
& card(last_1_1,int1)
& etype(last_1_1,int0)
& fact(last_1_1,real)
& gener(last_1_1,ge)
& refer(last_1_1,refer_c)
& varia(last_1_1,varia_c)
& card(c37361,card_c)
& etype(c37361,etype_c)
& fact(c37361,real)
& gener(c37361,gener_c)
& refer(c37361,refer_c)
& varia(c37361,con)
& card(c37356,int750)
& gener(kilo__1_1,ge)
& card(c37402,card_c)
& etype(c37402,etype_c)
& fact(c37402,real)
& gener(c37402,gener_c)
& refer(c37402,refer_c)
& varia(c37402,varia_c)
& card(c37233,int1)
& etype(c37233,int0)
& fact(c37233,real)
& gener(c37233,sp)
& refer(c37233,det)
& varia(c37233,varia_c)
& card(c37313,int1)
& etype(c37313,int0)
& fact(c37313,real)
& gener(c37313,gener_c)
& refer(c37313,refer_c)
& varia(c37313,varia_c)
& fact(drosseln_1_1,real)
& gener(drosseln_1_1,ge) ),
inference(pure_predicate_removal,[],[f10329]) ).
fof(f10335,plain,
( assoc(boxermotor_1_1,boxer_2_1)
& sub(boxermotor_1_1,motor__1_1)
& assoc(bundeswehrausf__374hrung_1_1,bundeswehr_1_1)
& sub(bundeswehrausf__374hrung_1_1,ausf__374hrung_1_1)
& sub(c37238,faun_1_1)
& attr(c37245,c37246)
& sub(c37245,stadt__1_1)
& sub(c37246,name_1_1)
& val(c37246,n__374rnberg_0)
& sub(c37268,c37272)
& pmod(c37272,ackerbautreibend_1_1,einsatz_1_1)
& sub(c37274,fahrzeug__1_1)
& sub(c37284,bundeswehrausf__374hrung_1_1)
& pred(c37291,reifen__1_1)
& attch(c37298,c37291)
& pred(c37298,lypsoid_1_1)
& prop(c37298,n22x12_1_1)
& prop(c37341,c37229)
& sub(c37341,bmw_1_1)
& sub(c37345,boxermotor_1_1)
& sub(c37359,last_1_1)
& etype(boxermotor_1_1,int0)
& fact(boxermotor_1_1,real)
& gener(boxermotor_1_1,ge)
& refer(boxermotor_1_1,refer_c)
& varia(boxermotor_1_1,varia_c)
& etype(boxer_2_1,int0)
& fact(boxer_2_1,real)
& gener(boxer_2_1,ge)
& refer(boxer_2_1,refer_c)
& varia(boxer_2_1,varia_c)
& etype(motor__1_1,int0)
& fact(motor__1_1,real)
& gener(motor__1_1,ge)
& refer(motor__1_1,refer_c)
& varia(motor__1_1,varia_c)
& etype(bundeswehrausf__374hrung_1_1,int0)
& fact(bundeswehrausf__374hrung_1_1,real)
& gener(bundeswehrausf__374hrung_1_1,ge)
& refer(bundeswehrausf__374hrung_1_1,refer_c)
& varia(bundeswehrausf__374hrung_1_1,varia_c)
& etype(bundeswehr_1_1,int1)
& fact(bundeswehr_1_1,real)
& gener(bundeswehr_1_1,ge)
& refer(bundeswehr_1_1,refer_c)
& varia(bundeswehr_1_1,varia_c)
& etype(ausf__374hrung_1_1,int0)
& fact(ausf__374hrung_1_1,real)
& gener(ausf__374hrung_1_1,ge)
& refer(ausf__374hrung_1_1,refer_c)
& varia(ausf__374hrung_1_1,varia_c)
& etype(c37238,int0)
& fact(c37238,real)
& gener(c37238,gener_c)
& refer(c37238,refer_c)
& varia(c37238,varia_c)
& etype(faun_1_1,int0)
& fact(faun_1_1,real)
& gener(faun_1_1,ge)
& refer(faun_1_1,refer_c)
& varia(faun_1_1,varia_c)
& etype(c37245,int0)
& fact(c37245,real)
& gener(c37245,sp)
& refer(c37245,det)
& varia(c37245,con)
& etype(c37246,int0)
& fact(c37246,real)
& gener(c37246,sp)
& refer(c37246,indet)
& varia(c37246,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(c37268,int0)
& fact(c37268,real)
& gener(c37268,sp)
& refer(c37268,det)
& varia(c37268,con)
& etype(c37272,int0)
& fact(c37272,real)
& gener(c37272,ge)
& refer(c37272,refer_c)
& varia(c37272,varia_c)
& etype(einsatz_1_1,int0)
& fact(einsatz_1_1,real)
& gener(einsatz_1_1,ge)
& refer(einsatz_1_1,refer_c)
& varia(einsatz_1_1,varia_c)
& etype(c37274,int0)
& fact(c37274,real)
& gener(c37274,gener_c)
& refer(c37274,refer_c)
& varia(c37274,varia_c)
& etype(fahrzeug__1_1,int0)
& fact(fahrzeug__1_1,real)
& gener(fahrzeug__1_1,ge)
& refer(fahrzeug__1_1,refer_c)
& varia(fahrzeug__1_1,varia_c)
& etype(c37284,int0)
& fact(c37284,real)
& gener(c37284,sp)
& refer(c37284,det)
& varia(c37284,con)
& etype(c37291,int1)
& fact(c37291,real)
& gener(c37291,sp)
& refer(c37291,det)
& varia(c37291,varia_c)
& etype(reifen__1_1,int0)
& fact(reifen__1_1,real)
& gener(reifen__1_1,ge)
& refer(reifen__1_1,refer_c)
& varia(reifen__1_1,varia_c)
& etype(c37298,int1)
& fact(c37298,real)
& gener(c37298,gener_c)
& refer(c37298,refer_c)
& varia(c37298,varia_c)
& etype(lypsoid_1_1,int0)
& fact(lypsoid_1_1,real)
& gener(lypsoid_1_1,ge)
& refer(lypsoid_1_1,refer_c)
& varia(lypsoid_1_1,varia_c)
& etype(c37339,etype_c)
& fact(c37339,real)
& gener(c37339,gener_c)
& refer(c37339,refer_c)
& varia(c37339,con)
& gener(pferdest__344rke_1_1,ge)
& etype(c37341,int0)
& fact(c37341,real)
& gener(c37341,gener_c)
& refer(c37341,refer_c)
& varia(c37341,varia_c)
& etype(bmw_1_1,int0)
& fact(bmw_1_1,real)
& gener(bmw_1_1,ge)
& refer(bmw_1_1,refer_c)
& varia(bmw_1_1,varia_c)
& etype(c37345,int0)
& fact(c37345,real)
& gener(c37345,gener_c)
& refer(c37345,refer_c)
& varia(c37345,varia_c)
& etype(c37359,int0)
& fact(c37359,real)
& gener(c37359,gener_c)
& refer(c37359,refer_c)
& varia(c37359,varia_c)
& etype(last_1_1,int0)
& fact(last_1_1,real)
& gener(last_1_1,ge)
& refer(last_1_1,refer_c)
& varia(last_1_1,varia_c)
& etype(c37361,etype_c)
& fact(c37361,real)
& gener(c37361,gener_c)
& refer(c37361,refer_c)
& varia(c37361,con)
& gener(kilo__1_1,ge)
& etype(c37402,etype_c)
& fact(c37402,real)
& gener(c37402,gener_c)
& refer(c37402,refer_c)
& varia(c37402,varia_c)
& etype(c37233,int0)
& fact(c37233,real)
& gener(c37233,sp)
& refer(c37233,det)
& varia(c37233,varia_c)
& etype(c37313,int0)
& fact(c37313,real)
& gener(c37313,gener_c)
& refer(c37313,refer_c)
& varia(c37313,varia_c)
& fact(drosseln_1_1,real)
& gener(drosseln_1_1,ge) ),
inference(pure_predicate_removal,[],[f10332]) ).
fof(f10338,plain,
( assoc(boxermotor_1_1,boxer_2_1)
& sub(boxermotor_1_1,motor__1_1)
& assoc(bundeswehrausf__374hrung_1_1,bundeswehr_1_1)
& sub(bundeswehrausf__374hrung_1_1,ausf__374hrung_1_1)
& sub(c37238,faun_1_1)
& attr(c37245,c37246)
& sub(c37245,stadt__1_1)
& sub(c37246,name_1_1)
& val(c37246,n__374rnberg_0)
& sub(c37268,c37272)
& pmod(c37272,ackerbautreibend_1_1,einsatz_1_1)
& sub(c37274,fahrzeug__1_1)
& sub(c37284,bundeswehrausf__374hrung_1_1)
& pred(c37291,reifen__1_1)
& attch(c37298,c37291)
& pred(c37298,lypsoid_1_1)
& prop(c37298,n22x12_1_1)
& prop(c37341,c37229)
& sub(c37341,bmw_1_1)
& sub(c37345,boxermotor_1_1)
& sub(c37359,last_1_1)
& etype(boxermotor_1_1,int0)
& fact(boxermotor_1_1,real)
& gener(boxermotor_1_1,ge)
& varia(boxermotor_1_1,varia_c)
& etype(boxer_2_1,int0)
& fact(boxer_2_1,real)
& gener(boxer_2_1,ge)
& varia(boxer_2_1,varia_c)
& etype(motor__1_1,int0)
& fact(motor__1_1,real)
& gener(motor__1_1,ge)
& varia(motor__1_1,varia_c)
& etype(bundeswehrausf__374hrung_1_1,int0)
& fact(bundeswehrausf__374hrung_1_1,real)
& gener(bundeswehrausf__374hrung_1_1,ge)
& varia(bundeswehrausf__374hrung_1_1,varia_c)
& etype(bundeswehr_1_1,int1)
& fact(bundeswehr_1_1,real)
& gener(bundeswehr_1_1,ge)
& varia(bundeswehr_1_1,varia_c)
& etype(ausf__374hrung_1_1,int0)
& fact(ausf__374hrung_1_1,real)
& gener(ausf__374hrung_1_1,ge)
& varia(ausf__374hrung_1_1,varia_c)
& etype(c37238,int0)
& fact(c37238,real)
& gener(c37238,gener_c)
& varia(c37238,varia_c)
& etype(faun_1_1,int0)
& fact(faun_1_1,real)
& gener(faun_1_1,ge)
& varia(faun_1_1,varia_c)
& etype(c37245,int0)
& fact(c37245,real)
& gener(c37245,sp)
& varia(c37245,con)
& etype(c37246,int0)
& fact(c37246,real)
& gener(c37246,sp)
& varia(c37246,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(c37268,int0)
& fact(c37268,real)
& gener(c37268,sp)
& varia(c37268,con)
& etype(c37272,int0)
& fact(c37272,real)
& gener(c37272,ge)
& varia(c37272,varia_c)
& etype(einsatz_1_1,int0)
& fact(einsatz_1_1,real)
& gener(einsatz_1_1,ge)
& varia(einsatz_1_1,varia_c)
& etype(c37274,int0)
& fact(c37274,real)
& gener(c37274,gener_c)
& varia(c37274,varia_c)
& etype(fahrzeug__1_1,int0)
& fact(fahrzeug__1_1,real)
& gener(fahrzeug__1_1,ge)
& varia(fahrzeug__1_1,varia_c)
& etype(c37284,int0)
& fact(c37284,real)
& gener(c37284,sp)
& varia(c37284,con)
& etype(c37291,int1)
& fact(c37291,real)
& gener(c37291,sp)
& varia(c37291,varia_c)
& etype(reifen__1_1,int0)
& fact(reifen__1_1,real)
& gener(reifen__1_1,ge)
& varia(reifen__1_1,varia_c)
& etype(c37298,int1)
& fact(c37298,real)
& gener(c37298,gener_c)
& varia(c37298,varia_c)
& etype(lypsoid_1_1,int0)
& fact(lypsoid_1_1,real)
& gener(lypsoid_1_1,ge)
& varia(lypsoid_1_1,varia_c)
& etype(c37339,etype_c)
& fact(c37339,real)
& gener(c37339,gener_c)
& varia(c37339,con)
& gener(pferdest__344rke_1_1,ge)
& etype(c37341,int0)
& fact(c37341,real)
& gener(c37341,gener_c)
& varia(c37341,varia_c)
& etype(bmw_1_1,int0)
& fact(bmw_1_1,real)
& gener(bmw_1_1,ge)
& varia(bmw_1_1,varia_c)
& etype(c37345,int0)
& fact(c37345,real)
& gener(c37345,gener_c)
& varia(c37345,varia_c)
& etype(c37359,int0)
& fact(c37359,real)
& gener(c37359,gener_c)
& varia(c37359,varia_c)
& etype(last_1_1,int0)
& fact(last_1_1,real)
& gener(last_1_1,ge)
& varia(last_1_1,varia_c)
& etype(c37361,etype_c)
& fact(c37361,real)
& gener(c37361,gener_c)
& varia(c37361,con)
& gener(kilo__1_1,ge)
& etype(c37402,etype_c)
& fact(c37402,real)
& gener(c37402,gener_c)
& varia(c37402,varia_c)
& etype(c37233,int0)
& fact(c37233,real)
& gener(c37233,sp)
& varia(c37233,varia_c)
& etype(c37313,int0)
& fact(c37313,real)
& gener(c37313,gener_c)
& varia(c37313,varia_c)
& fact(drosseln_1_1,real)
& gener(drosseln_1_1,ge) ),
inference(pure_predicate_removal,[],[f10335]) ).
fof(f10343,plain,
( assoc(boxermotor_1_1,boxer_2_1)
& sub(boxermotor_1_1,motor__1_1)
& assoc(bundeswehrausf__374hrung_1_1,bundeswehr_1_1)
& sub(bundeswehrausf__374hrung_1_1,ausf__374hrung_1_1)
& sub(c37238,faun_1_1)
& attr(c37245,c37246)
& sub(c37245,stadt__1_1)
& sub(c37246,name_1_1)
& val(c37246,n__374rnberg_0)
& sub(c37268,c37272)
& pmod(c37272,ackerbautreibend_1_1,einsatz_1_1)
& sub(c37274,fahrzeug__1_1)
& sub(c37284,bundeswehrausf__374hrung_1_1)
& pred(c37291,reifen__1_1)
& attch(c37298,c37291)
& pred(c37298,lypsoid_1_1)
& prop(c37298,n22x12_1_1)
& prop(c37341,c37229)
& sub(c37341,bmw_1_1)
& sub(c37345,boxermotor_1_1)
& sub(c37359,last_1_1)
& etype(boxermotor_1_1,int0)
& fact(boxermotor_1_1,real)
& gener(boxermotor_1_1,ge)
& etype(boxer_2_1,int0)
& fact(boxer_2_1,real)
& gener(boxer_2_1,ge)
& etype(motor__1_1,int0)
& fact(motor__1_1,real)
& gener(motor__1_1,ge)
& etype(bundeswehrausf__374hrung_1_1,int0)
& fact(bundeswehrausf__374hrung_1_1,real)
& gener(bundeswehrausf__374hrung_1_1,ge)
& etype(bundeswehr_1_1,int1)
& fact(bundeswehr_1_1,real)
& gener(bundeswehr_1_1,ge)
& etype(ausf__374hrung_1_1,int0)
& fact(ausf__374hrung_1_1,real)
& gener(ausf__374hrung_1_1,ge)
& etype(c37238,int0)
& fact(c37238,real)
& gener(c37238,gener_c)
& etype(faun_1_1,int0)
& fact(faun_1_1,real)
& gener(faun_1_1,ge)
& etype(c37245,int0)
& fact(c37245,real)
& gener(c37245,sp)
& etype(c37246,int0)
& fact(c37246,real)
& gener(c37246,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(c37268,int0)
& fact(c37268,real)
& gener(c37268,sp)
& etype(c37272,int0)
& fact(c37272,real)
& gener(c37272,ge)
& etype(einsatz_1_1,int0)
& fact(einsatz_1_1,real)
& gener(einsatz_1_1,ge)
& etype(c37274,int0)
& fact(c37274,real)
& gener(c37274,gener_c)
& etype(fahrzeug__1_1,int0)
& fact(fahrzeug__1_1,real)
& gener(fahrzeug__1_1,ge)
& etype(c37284,int0)
& fact(c37284,real)
& gener(c37284,sp)
& etype(c37291,int1)
& fact(c37291,real)
& gener(c37291,sp)
& etype(reifen__1_1,int0)
& fact(reifen__1_1,real)
& gener(reifen__1_1,ge)
& etype(c37298,int1)
& fact(c37298,real)
& gener(c37298,gener_c)
& etype(lypsoid_1_1,int0)
& fact(lypsoid_1_1,real)
& gener(lypsoid_1_1,ge)
& etype(c37339,etype_c)
& fact(c37339,real)
& gener(c37339,gener_c)
& gener(pferdest__344rke_1_1,ge)
& etype(c37341,int0)
& fact(c37341,real)
& gener(c37341,gener_c)
& etype(bmw_1_1,int0)
& fact(bmw_1_1,real)
& gener(bmw_1_1,ge)
& etype(c37345,int0)
& fact(c37345,real)
& gener(c37345,gener_c)
& etype(c37359,int0)
& fact(c37359,real)
& gener(c37359,gener_c)
& etype(last_1_1,int0)
& fact(last_1_1,real)
& gener(last_1_1,ge)
& etype(c37361,etype_c)
& fact(c37361,real)
& gener(c37361,gener_c)
& gener(kilo__1_1,ge)
& etype(c37402,etype_c)
& fact(c37402,real)
& gener(c37402,gener_c)
& etype(c37233,int0)
& fact(c37233,real)
& gener(c37233,sp)
& etype(c37313,int0)
& fact(c37313,real)
& gener(c37313,gener_c)
& fact(drosseln_1_1,real)
& gener(drosseln_1_1,ge) ),
inference(pure_predicate_removal,[],[f10338]) ).
fof(f10348,plain,
( assoc(boxermotor_1_1,boxer_2_1)
& sub(boxermotor_1_1,motor__1_1)
& assoc(bundeswehrausf__374hrung_1_1,bundeswehr_1_1)
& sub(bundeswehrausf__374hrung_1_1,ausf__374hrung_1_1)
& sub(c37238,faun_1_1)
& attr(c37245,c37246)
& sub(c37245,stadt__1_1)
& sub(c37246,name_1_1)
& val(c37246,n__374rnberg_0)
& sub(c37268,c37272)
& pmod(c37272,ackerbautreibend_1_1,einsatz_1_1)
& sub(c37274,fahrzeug__1_1)
& sub(c37284,bundeswehrausf__374hrung_1_1)
& pred(c37291,reifen__1_1)
& attch(c37298,c37291)
& pred(c37298,lypsoid_1_1)
& prop(c37298,n22x12_1_1)
& prop(c37341,c37229)
& sub(c37341,bmw_1_1)
& sub(c37345,boxermotor_1_1)
& sub(c37359,last_1_1)
& etype(boxermotor_1_1,int0)
& fact(boxermotor_1_1,real)
& etype(boxer_2_1,int0)
& fact(boxer_2_1,real)
& etype(motor__1_1,int0)
& fact(motor__1_1,real)
& etype(bundeswehrausf__374hrung_1_1,int0)
& fact(bundeswehrausf__374hrung_1_1,real)
& etype(bundeswehr_1_1,int1)
& fact(bundeswehr_1_1,real)
& etype(ausf__374hrung_1_1,int0)
& fact(ausf__374hrung_1_1,real)
& etype(c37238,int0)
& fact(c37238,real)
& etype(faun_1_1,int0)
& fact(faun_1_1,real)
& etype(c37245,int0)
& fact(c37245,real)
& etype(c37246,int0)
& fact(c37246,real)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& etype(c37268,int0)
& fact(c37268,real)
& etype(c37272,int0)
& fact(c37272,real)
& etype(einsatz_1_1,int0)
& fact(einsatz_1_1,real)
& etype(c37274,int0)
& fact(c37274,real)
& etype(fahrzeug__1_1,int0)
& fact(fahrzeug__1_1,real)
& etype(c37284,int0)
& fact(c37284,real)
& etype(c37291,int1)
& fact(c37291,real)
& etype(reifen__1_1,int0)
& fact(reifen__1_1,real)
& etype(c37298,int1)
& fact(c37298,real)
& etype(lypsoid_1_1,int0)
& fact(lypsoid_1_1,real)
& etype(c37339,etype_c)
& fact(c37339,real)
& etype(c37341,int0)
& fact(c37341,real)
& etype(bmw_1_1,int0)
& fact(bmw_1_1,real)
& etype(c37345,int0)
& fact(c37345,real)
& etype(c37359,int0)
& fact(c37359,real)
& etype(last_1_1,int0)
& fact(last_1_1,real)
& etype(c37361,etype_c)
& fact(c37361,real)
& etype(c37402,etype_c)
& fact(c37402,real)
& etype(c37233,int0)
& fact(c37233,real)
& etype(c37313,int0)
& fact(c37313,real)
& fact(drosseln_1_1,real) ),
inference(pure_predicate_removal,[],[f10343]) ).
fof(f10351,plain,
! [X0,X1,X2] :
( member(X0,cons(X1,X2))
| ~ member(X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f10518,plain,
! [X0,X1,X2] :
( ? [X3] :
( mcont(X3,X2)
& obj(X3,X2)
& scar(X3,X2)
& subs(X3,stehen_1_b) )
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(ennf_transformation,[],[f160]) ).
fof(f10519,plain,
! [X0,X1,X2] :
( ? [X3] :
( mcont(X3,X2)
& obj(X3,X2)
& scar(X3,X2)
& subs(X3,stehen_1_b) )
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(flattening,[],[f10518]) ).
fof(f10546,plain,
! [X0,X1] :
( ? [X2] :
( attr(X1,X2)
& sub(X2,name_1_1)
& val(X2,X0) )
| ~ name(X1,X0) ),
inference(ennf_transformation,[],[f177]) ).
fof(f10547,plain,
! [X0,X1,X2] :
( name(X2,X1)
| ~ attr(X2,X0)
| ~ sub(X0,name_1_1)
| ~ val(X0,X1) ),
inference(ennf_transformation,[],[f178]) ).
fof(f10548,plain,
! [X0,X1,X2] :
( name(X2,X1)
| ~ attr(X2,X0)
| ~ sub(X0,name_1_1)
| ~ val(X0,X1) ),
inference(flattening,[],[f10547]) ).
fof(f10553,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(X2,name_1_1) ),
inference(ennf_transformation,[],[f10189]) ).
fof(f10554,plain,
! [X0,X1] : member(X0,cons(X0,X1)),
inference(cnf_transformation,[],[f1]) ).
fof(f10555,plain,
! [X2,X0,X1] :
( ~ member(X0,X2)
| member(X0,cons(X1,X2)) ),
inference(cnf_transformation,[],[f10351]) ).
fof(f10819,plain,
! [X2,X0,X1] :
( ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0)
| obj(sK51(X2),X2) ),
inference(cnf_transformation,[],[f10519]) ).
fof(f10872,plain,
! [X0,X1] :
( ~ name(X1,X0)
| sub(sK60(X0,X1),name_1_1) ),
inference(cnf_transformation,[],[f10546]) ).
fof(f10873,plain,
! [X0,X1] :
( ~ name(X1,X0)
| attr(X1,sK60(X0,X1)) ),
inference(cnf_transformation,[],[f10546]) ).
fof(f10874,plain,
! [X2,X0,X1] :
( ~ val(X0,X1)
| ~ sub(X0,name_1_1)
| ~ attr(X2,X0)
| name(X2,X1) ),
inference(cnf_transformation,[],[f10548]) ).
fof(f20770,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sub(X2,name_1_1)
| ~ sub(X1,name_1_1)
| ~ obj(X4,X0)
| ~ attr(X5,X6)
| ~ attr(X3,X2)
| ~ attr(X0,X1) ),
inference(cnf_transformation,[],[f10553]) ).
fof(f20848,plain,
val(c37246,n__374rnberg_0),
inference(cnf_transformation,[],[f10348]) ).
fof(f20849,plain,
sub(c37246,name_1_1),
inference(cnf_transformation,[],[f10348]) ).
fof(f20851,plain,
attr(c37245,c37246),
inference(cnf_transformation,[],[f10348]) ).
fof(f20857,plain,
! [X0,X1] : ~ member(X0,cons(X0,X1)),
inference(consistent_polarity_flipping,[],[f10554]) ).
fof(f20858,plain,
! [X2,X0,X1] :
( ~ member(X0,cons(X1,X2))
| member(X0,X2) ),
inference(consistent_polarity_flipping,[],[f10555]) ).
fof(f21052,plain,
! [X2,X0,X1] :
( ~ obj(sK51(X2),X2)
| member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0)
| sub(X0,X1) ),
inference(consistent_polarity_flipping,[],[f10819]) ).
fof(f21103,plain,
! [X0,X1] :
( ~ sub(sK60(X0,X1),name_1_1)
| ~ name(X1,X0) ),
inference(consistent_polarity_flipping,[],[f10872]) ).
fof(f21104,plain,
! [X2,X0,X1] :
( ~ attr(X2,X0)
| sub(X0,name_1_1)
| ~ val(X0,X1)
| name(X2,X1) ),
inference(consistent_polarity_flipping,[],[f10874]) ).
fof(f22300,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( sub(X2,name_1_1)
| sub(X1,name_1_1)
| obj(X4,X0)
| ~ attr(X5,X6)
| ~ attr(X3,X2)
| ~ attr(X0,X1) ),
inference(consistent_polarity_flipping,[],[f20770]) ).
fof(f22305,plain,
~ sub(c37246,name_1_1),
inference(consistent_polarity_flipping,[],[f20849]) ).
fof(f22382,definition,
( spl63_1
<=> ! [X6,X5] : ~ attr(X5,X6) ),
introduced(definition,[new_symbols(definition,[spl63_1])],[avatar_definition]) ).
fof(f22383,plain,
( ! [X6,X5] : ~ attr(X5,X6)
| ~ spl63_1 ),
inference(avatar_component_clause,[],[f22382]) ).
fof(f22385,definition,
( spl63_2
<=> ! [X4,X0,X1] :
( sub(X1,name_1_1)
| obj(X4,X0)
| ~ attr(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl63_2])],[avatar_definition]) ).
fof(f22386,plain,
( ! [X0,X1,X4] :
( ~ attr(X0,X1)
| obj(X4,X0)
| sub(X1,name_1_1) )
| ~ spl63_2 ),
inference(avatar_component_clause,[],[f22385]) ).
fof(f22388,definition,
( spl63_3
<=> ! [X2,X3] :
( sub(X2,name_1_1)
| ~ attr(X3,X2) ) ),
introduced(definition,[new_symbols(definition,[spl63_3])],[avatar_definition]) ).
fof(f22389,plain,
( ! [X2,X3] :
( ~ attr(X3,X2)
| sub(X2,name_1_1) )
| ~ spl63_3 ),
inference(avatar_component_clause,[],[f22388]) ).
fof(f22390,plain,
( spl63_1
| spl63_2
| spl63_3 ),
inference(avatar_split_clause,[],[f22300,f22388,f22385,f22382]) ).
fof(f22391,plain,
( ! [X0] :
( obj(X0,c37245)
| sub(c37246,name_1_1) )
| ~ spl63_2 ),
inference(resolution,[],[f20851,f22386]) ).
fof(f22393,definition,
( spl63_4
<=> sub(c37246,name_1_1) ),
introduced(definition,[new_symbols(definition,[spl63_4])],[avatar_definition]) ).
fof(f22394,plain,
( ~ sub(c37246,name_1_1)
| spl63_4 ),
inference(avatar_component_clause,[],[f22393]) ).
fof(f22397,definition,
( spl63_5
<=> ! [X0] : obj(X0,c37245) ),
introduced(definition,[new_symbols(definition,[spl63_5])],[avatar_definition]) ).
fof(f22398,plain,
( ! [X0] : obj(X0,c37245)
| ~ spl63_5 ),
inference(avatar_component_clause,[],[f22397]) ).
fof(f22402,plain,
~ spl63_4,
inference(avatar_split_clause,[],[f22305,f22393]) ).
fof(f22403,plain,
( sub(c37246,name_1_1)
| ~ spl63_3 ),
inference(resolution,[],[f22389,f20851]) ).
fof(f22404,plain,
( spl63_4
| ~ spl63_3 ),
inference(avatar_split_clause,[],[f22403,f22388,f22393]) ).
fof(f22622,plain,
( $false
| ~ spl63_1 ),
inference(backward_subsumption_resolution,[],[f20851,f22383]) ).
fof(f22624,plain,
~ spl63_1,
inference(avatar_contradiction_clause,[],[f22622]) ).
fof(f22625,plain,
( ! [X0] : obj(X0,c37245)
| ~ spl63_2
| spl63_4 ),
inference(forward_subsumption_resolution,[],[f22391,f22394]) ).
fof(f22628,plain,
( spl63_5
| ~ spl63_2
| spl63_4 ),
inference(avatar_split_clause,[],[f22625,f22393,f22385,f22397]) ).
fof(f22911,plain,
! [X0] :
( sub(c37246,name_1_1)
| ~ val(c37246,X0)
| name(c37245,X0) ),
inference(resolution,[],[f21104,f20851]) ).
fof(f22912,plain,
( ! [X0] :
( name(c37245,X0)
| ~ val(c37246,X0) )
| spl63_4 ),
inference(forward_subsumption_resolution,[],[f22911,f22394]) ).
fof(f22913,plain,
( ! [X0] :
( ~ val(c37246,X0)
| attr(c37245,sK60(X0,c37245)) )
| spl63_4 ),
inference(resolution,[],[f22912,f10873]) ).
fof(f22945,plain,
( attr(c37245,sK60(n__374rnberg_0,c37245))
| spl63_4 ),
inference(resolution,[],[f22913,f20848]) ).
fof(f23621,definition,
( spl63_186
<=> sub(sK60(n__374rnberg_0,c37245),name_1_1) ),
introduced(definition,[new_symbols(definition,[spl63_186])],[avatar_definition]) ).
fof(f23623,plain,
( sub(sK60(n__374rnberg_0,c37245),name_1_1)
| ~ spl63_186 ),
inference(avatar_component_clause,[],[f23621]) ).
fof(f23909,definition,
( spl63_215
<=> ! [X0] :
( member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| sub(sK60(n__374rnberg_0,c37245),X0) ) ),
introduced(definition,[new_symbols(definition,[spl63_215])],[avatar_definition]) ).
fof(f23910,plain,
( ! [X0] :
( member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| sub(sK60(n__374rnberg_0,c37245),X0) )
| ~ spl63_215 ),
inference(avatar_component_clause,[],[f23909]) ).
fof(f23950,plain,
( ! [X0,X1] :
( member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c37245,X1)
| sub(X1,X0) )
| ~ spl63_5 ),
inference(resolution,[],[f21052,f22398]) ).
fof(f23974,plain,
( ! [X0] :
( member(X0,cons(familiename_1_1,cons(name_1_1,nil)))
| sub(sK60(n__374rnberg_0,c37245),X0) )
| ~ spl63_215 ),
inference(resolution,[],[f23910,f20858]) ).
fof(f24099,definition,
( spl63_239
<=> name(c37245,n__374rnberg_0) ),
introduced(definition,[new_symbols(definition,[spl63_239])],[avatar_definition]) ).
fof(f24100,plain,
( name(c37245,n__374rnberg_0)
| ~ spl63_239 ),
inference(avatar_component_clause,[],[f24099]) ).
fof(f24101,plain,
( ~ name(c37245,n__374rnberg_0)
| spl63_239 ),
inference(avatar_component_clause,[],[f24099]) ).
fof(f24279,definition,
( spl63_263
<=> ! [X0,X1] :
( member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c37245,X1)
| sub(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl63_263])],[avatar_definition]) ).
fof(f24280,plain,
( ! [X0,X1] :
( ~ attr(c37245,X1)
| member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| sub(X1,X0) )
| ~ spl63_263 ),
inference(avatar_component_clause,[],[f24279]) ).
fof(f24575,plain,
( spl63_263
| ~ spl63_5 ),
inference(avatar_split_clause,[],[f23950,f22397,f24279]) ).
fof(f24771,plain,
( ! [X0] :
( member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| sub(sK60(n__374rnberg_0,c37245),X0) )
| spl63_4
| ~ spl63_263 ),
inference(resolution,[],[f24280,f22945]) ).
fof(f24772,plain,
( spl63_215
| spl63_4
| ~ spl63_263 ),
inference(avatar_split_clause,[],[f24771,f24279,f22393,f23909]) ).
fof(f24785,plain,
( ~ val(c37246,n__374rnberg_0)
| spl63_4
| spl63_239 ),
inference(resolution,[],[f24101,f22912]) ).
fof(f24786,plain,
( $false
| spl63_4
| spl63_239 ),
inference(forward_subsumption_resolution,[],[f24785,f20848]) ).
fof(f24787,plain,
( spl63_4
| spl63_239 ),
inference(avatar_contradiction_clause,[],[f24786]) ).
fof(f26207,plain,
( ! [X0] :
( member(X0,cons(name_1_1,nil))
| sub(sK60(n__374rnberg_0,c37245),X0) )
| ~ spl63_215 ),
inference(resolution,[],[f23974,f20858]) ).
fof(f26303,plain,
( sub(sK60(n__374rnberg_0,c37245),name_1_1)
| ~ spl63_215 ),
inference(resolution,[],[f26207,f20857]) ).
fof(f26305,plain,
( spl63_186
| ~ spl63_215 ),
inference(avatar_split_clause,[],[f26303,f23909,f23621]) ).
fof(f26306,plain,
( ~ name(c37245,n__374rnberg_0)
| ~ spl63_186 ),
inference(resolution,[],[f23623,f21103]) ).
fof(f26316,plain,
( $false
| ~ spl63_186
| ~ spl63_239 ),
inference(forward_subsumption_resolution,[],[f26306,f24100]) ).
fof(f26317,plain,
( ~ spl63_186
| ~ spl63_239 ),
inference(avatar_contradiction_clause,[],[f26316]) ).
cnf(s1,plain,
( spl63_1
| spl63_2
| spl63_3 ),
inference(sat_conversion,[],[f22390]) ).
cnf(s4,plain,
~ spl63_4,
inference(sat_conversion,[],[f22402]) ).
cnf(s5,plain,
( ~ spl63_3
| spl63_4 ),
inference(sat_conversion,[],[f22404]) ).
cnf(s21,plain,
~ spl63_1,
inference(sat_conversion,[],[f22624]) ).
cnf(s23,plain,
( ~ spl63_2
| spl63_4
| spl63_5 ),
inference(sat_conversion,[],[f22628]) ).
cnf(s234,plain,
( ~ spl63_5
| spl63_263 ),
inference(sat_conversion,[],[f24575]) ).
cnf(s251,plain,
( spl63_4
| spl63_215
| ~ spl63_263 ),
inference(sat_conversion,[],[f24772]) ).
cnf(s256,plain,
( spl63_4
| spl63_239 ),
inference(sat_conversion,[],[f24787]) ).
cnf(s274,plain,
( spl63_186
| ~ spl63_215 ),
inference(sat_conversion,[],[f26305]) ).
cnf(s276,plain,
( ~ spl63_186
| ~ spl63_239 ),
inference(sat_conversion,[],[f26317]) ).
cnf(s280,plain,
spl63_239,
inference(rat,[],[s256,s4]) ).
cnf(s282,plain,
~ spl63_3,
inference(rat,[],[s5,s4]) ).
cnf(s283,plain,
~ spl63_186,
inference(rat,[],[s276,s280]) ).
cnf(s284,plain,
~ spl63_215,
inference(rat,[],[s274,s283]) ).
cnf(s286,plain,
~ spl63_263,
inference(rat,[],[s251,s4,s284]) ).
cnf(s292,plain,
~ spl63_5,
inference(rat,[],[s234,s286]) ).
cnf(s293,plain,
~ spl63_2,
inference(rat,[],[s23,s4,s292]) ).
cnf(s294,plain,
$false,
inference(rat,[],[s1,s282,s293,s21]) ).
fof(f26318,plain,
$false,
inference(avatar_sat_refutation,[],[s294]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+90 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.26 % Computer : n014.cluster.edu
% 0.11/0.26 % Model : x86_64 x86_64
% 0.11/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.26 % Memory : 8046.5625MB
% 0.11/0.26 % OS : Linux 6.8.0-71-generic
% 0.11/0.27 % CPULimit : 300
% 0.11/0.27 % WCLimit : 300
% 0.11/0.27 % DateTime : Mon Sep 28 23:23:01 UTC 2026
% 0.11/0.27 % CPUTime :
% 0.11/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.27/0.32 Running first-order model finding
% 0.27/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.31/1.26 % (2281360)Will run a generic schedule for satisfiability detection.
% 5.31/1.26 % (2281365)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2719591740_2998 on theBenchmark for (2998ds/0Mi)
% 5.31/1.26 % (2281366)% WARNING: option uhcvi not known.
% 5.31/1.26 % (2281371)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2366053997:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 5.31/1.26 % (2281368)dis+10_1_sil=32000:sp=arity:random_seed=4114664815:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 5.31/1.26 % (2281367)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=71896080:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 5.31/1.26 % (2281366)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1633044842:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 5.31/1.26 % (2281369)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2318900210:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 5.31/1.26 % (2281370)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2419712970:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 5.31/1.26 % (2281368)Instruction limit reached!
% 5.31/1.26 % (2281368)------------------------------
% 5.31/1.26 % (2281368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.31/1.26 % (2281368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.26 % (2281368)CaDiCaL version: 2.1.3
% 5.31/1.26 % (2281368)Termination reason: Instruction limit
% 5.31/1.26 % (2281368)Termination phase: Saturation
% 5.31/1.26 % (2281368)Time elapsed: 0.102 s
% 5.31/1.26 % (2281368)Peak memory usage: 26 MB
% 5.31/1.26 % (2281368)Instructions burned: 103 (million)
% 5.31/1.26 % (2281369)Instruction limit reached!
% 5.31/1.26 % (2281369)------------------------------
% 5.31/1.26 % (2281369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.31/1.26 % (2281369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.26 % (2281369)CaDiCaL version: 2.1.3
% 5.31/1.26 % (2281369)Termination reason: Instruction limit
% 5.31/1.26 % (2281369)Termination phase: Blocked clause elimination
% 5.31/1.26 % (2281369)Time elapsed: 0.122 s
% 5.31/1.26 % (2281369)Peak memory usage: 28 MB
% 5.31/1.26 % (2281369)Instructions burned: 117 (million)
% 5.31/1.26 % (2281370)Instruction limit reached!
% 5.31/1.26 % (2281370)------------------------------
% 5.31/1.26 % (2281370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.31/1.26 % (2281370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.26 % (2281370)CaDiCaL version: 2.1.3
% 5.31/1.26 % (2281370)Termination reason: Instruction limit
% 5.31/1.26 % (2281370)Termination phase: Saturation
% 5.31/1.26 % (2281370)Time elapsed: 0.125 s
% 5.31/1.26 % (2281370)Peak memory usage: 28 MB
% 5.31/1.26 % (2281370)Instructions burned: 131 (million)
% 5.31/1.26 % (2281379)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2822413613:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 5.31/1.26 % (2281380)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4191488725:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 5.31/1.26 % (2281381)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=111668711:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 5.31/1.26 % (2281371)Instruction limit reached!
% 5.31/1.26 % (2281371)------------------------------
% 5.31/1.26 % (2281371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.31/1.26 % (2281371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.26 % (2281371)CaDiCaL version: 2.1.3
% 5.31/1.26 % (2281371)Termination reason: Instruction limit
% 5.31/1.26 % (2281371)Termination phase: Saturation
% 5.31/1.26 % (2281371)Time elapsed: 0.202 s
% 5.31/1.26 % (2281371)Peak memory usage: 29 MB
% 5.31/1.26 % (2281371)Instructions burned: 159 (million)
% 5.31/1.26 % TRYING [1]
% 5.31/1.26 % (2281385)ott-21_1_sil=16000:fs=off:random_seed=2718031524:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 5.31/1.26 % TRYING [2]
% 5.31/1.26 % (2281380)Instruction limit reached!
% 5.31/1.26 % (2281380)------------------------------
% 5.31/1.26 % (2281380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.31/1.26 % (2281380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.26 % (2281380)CaDiCaL version: 2.1.3
% 5.31/1.26 % (2281380)Termination reason: Instruction limit
% 5.31/1.26 % (2281380)Termination phase: Blocked clause elimination
% 5.31/1.26 % (2281380)Time elapsed: 0.134 s
% 5.31/1.26 % (2281380)Peak memory usage: 28 MB
% 5.31/1.26 % (2281380)Instructions burned: 131 (million)
% 5.31/1.26 % (2281387)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=536062977:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi)
% 5.31/1.26 % (2281385)Instruction limit reached!
% 5.31/1.26 % (2281385)------------------------------
% 5.31/1.26 % (2281385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.31/1.26 % (2281385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.26 % (2281385)CaDiCaL version: 2.1.3
% 5.31/1.26 % (2281385)Termination reason: Instruction limit
% 5.31/1.26 % (2281385)Termination phase: Saturation
% 5.31/1.26 % (2281385)Time elapsed: 0.165 s
% 5.31/1.26 % (2281385)Peak memory usage: 28 MB
% 5.31/1.26 % (2281385)Instructions burned: 180 (million)
% 5.31/1.26 % TRYING [3]
% 5.31/1.26 % (2281389)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1159270738:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi)
% 5.31/1.26 % TRYING [1]
% 5.31/1.26 % TRYING [2]
% 5.31/1.26 % (2281366) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2281360-2281366"...
% 5.31/1.26 % (2281366)...printing done.
% 5.31/1.26 % (2281366)Refutation found. Thanks to Tanya!
% 5.31/1.26 % SZS status Theorem for theBenchmark
% 5.31/1.26 % SZS output start Proof for theBenchmark
% See solution above
% 5.31/1.29 % (2281366)------------------------------
% 5.31/1.29 % (2281366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.31/1.29 % (2281366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.29 % (2281366)CaDiCaL version: 2.1.3
% 5.31/1.29 % (2281366)Termination reason: Refutation
% 5.31/1.29 % (2281366)Time elapsed: 0.680 s
% 5.31/1.29 % (2281366)Peak memory usage: 37 MB
% 5.31/1.29 % (2281366)Instructions burned: 729 (million)
% 5.31/1.29 % (2281360)Success in time 0.931 s
% 5.31/1.29 % Vampire exiting
%------------------------------------------------------------------------------