%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR113+10 : 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 : 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:22 AM UTC 2026
% Result : Theorem 2.40s 0.87s
% Output : Refutation 2.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 8
% Syntax : Number of formulae : 65 ( 10 unt; 0 def)
% Number of atoms : 1821 ( 0 equ)
% Maximal formula atoms : 299 ( 28 avg)
% Number of connectives : 1851 ( 95 ~; 83 |;1666 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 299 ( 31 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 25 usr; 1 prp; 0-11 aty)
% Number of functors : 67 ( 67 usr; 62 con; 0-2 aty)
% Number of variables : 130 ( 106 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
! [X0,X1] :
( fact(X0,X1)
=> has_fact_leq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',has_fact_eq) ).
fof(f95,axiom,
! [X0,X1] :
( ( has_fact_leq(X1,real)
& loc(X1,X0) )
=> ? [X2] :
( loc(X2,X0)
& obj(X2,X1)
& subs(X2,geben_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',loc__geben_1_1_loc) ).
fof(f155,axiom,
! [X0,X1,X2] :
( ( prop(X0,X1)
& state_adjective_state_binding(X1,X2) )
=> ? [X3,X4,X5] :
( in(X5,X3)
& attr(X3,X4)
& loc(X0,X5)
& sub(X3,land_1_1)
& sub(X4,name_1_1)
& val(X4,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',state_adjective__in_state) ).
fof(f176,axiom,
! [X0,X1] :
( ( in(X0,X1)
| an(X0,X1)
| bei(X0,X1) )
=> flp(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',local_function___flp) ).
fof(f180,axiom,
! [X0,X1] :
( loc(X0,X1)
=> ? [X2] :
( loc(X2,X1)
& scar(X2,X0)
& subs(X2,stehen_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',loc__stehen_1_1_loc) ).
fof(f9006,axiom,
state_adjective_state_binding(amerikanisch__1_1,usa_0),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',fact_8825) ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4] :
( flp(X0,X2)
& attr(X2,X1)
& loc(X3,X0)
& scar(X3,X4)
& sub(X1,name_1_1)
& subs(X3,stehen_1_1)
& val(X1,usa_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',synth_qa07_003_mira_wp_178_a270) ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4] :
( flp(X0,X2)
& attr(X2,X1)
& loc(X3,X0)
& scar(X3,X4)
& sub(X1,name_1_1)
& subs(X3,stehen_1_1)
& val(X1,usa_0) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,axiom,
( assoc(bundeland_1_1,bund_2_1)
& sub(bundeland_1_1,gebietsinstitution_1_1)
& sub(bundeland_1_1,land_1_1)
& assoc(bunderegierung_1_1,bund_1_1)
& sub(bunderegierung_1_1,regierung_1_1)
& sub(c81293,freiheitsstatue_1_1)
& sub(c81332,insel__1_1)
& attr(c81339,c81340)
& sub(c81339,insel__1_1)
& sub(c81340,name_1_1)
& val(c81340,liberty_island_0)
& prop(c81355,amerikanisch__1_1)
& sub(c81355,bunderegierung_1_1)
& sub(c81366,national_2_1)
& sub(c81368,park__1_1)
& subs(c81373,service_1_1)
& sub(c81378,enklave_1_1)
& sub(c81395,bezirk__1_1)
& attch(c81401,c81395)
& attr(c81401,c81402)
& sub(c81401,land_1_1)
& sub(c81402,name_1_1)
& val(c81402,usa_0)
& attr(c81409,c81410)
& sub(c81409,bundeland_1_1)
& sub(c81410,name_1_1)
& val(c81410,new_jersey_0)
& tupl_p11(c81513,c81293,c81332,c81339,c81355,c81366,c81368,c81373,c81378,c81395,c81409)
& assoc(freiheitsstatue_1_1,freiheit_1_1)
& sub(freiheitsstatue_1_1,statue_1_1)
& sort(bundeland_1_1,d)
& sort(bundeland_1_1,io)
& card(bundeland_1_1,int1)
& etype(bundeland_1_1,int0)
& fact(bundeland_1_1,real)
& gener(bundeland_1_1,ge)
& quant(bundeland_1_1,one)
& refer(bundeland_1_1,refer_c)
& varia(bundeland_1_1,varia_c)
& sort(bund_2_1,d)
& card(bund_2_1,card_c)
& etype(bund_2_1,int1)
& fact(bund_2_1,real)
& gener(bund_2_1,ge)
& quant(bund_2_1,quant_c)
& refer(bund_2_1,refer_c)
& varia(bund_2_1,varia_c)
& sort(gebietsinstitution_1_1,ent)
& card(gebietsinstitution_1_1,card_c)
& etype(gebietsinstitution_1_1,etype_c)
& fact(gebietsinstitution_1_1,real)
& gener(gebietsinstitution_1_1,gener_c)
& quant(gebietsinstitution_1_1,quant_c)
& refer(gebietsinstitution_1_1,refer_c)
& varia(gebietsinstitution_1_1,varia_c)
& sort(land_1_1,d)
& sort(land_1_1,io)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& quant(land_1_1,one)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& sort(bunderegierung_1_1,d)
& sort(bunderegierung_1_1,io)
& card(bunderegierung_1_1,card_c)
& etype(bunderegierung_1_1,int1)
& fact(bunderegierung_1_1,real)
& gener(bunderegierung_1_1,ge)
& quant(bunderegierung_1_1,quant_c)
& refer(bunderegierung_1_1,refer_c)
& varia(bunderegierung_1_1,varia_c)
& sort(bund_1_1,d)
& sort(bund_1_1,io)
& card(bund_1_1,card_c)
& etype(bund_1_1,int1)
& fact(bund_1_1,real)
& gener(bund_1_1,ge)
& quant(bund_1_1,quant_c)
& refer(bund_1_1,refer_c)
& varia(bund_1_1,varia_c)
& sort(regierung_1_1,d)
& sort(regierung_1_1,io)
& card(regierung_1_1,card_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& quant(regierung_1_1,quant_c)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& sort(c81293,d)
& card(c81293,int1)
& etype(c81293,int0)
& fact(c81293,real)
& gener(c81293,sp)
& quant(c81293,one)
& refer(c81293,det)
& varia(c81293,con)
& sort(freiheitsstatue_1_1,d)
& card(freiheitsstatue_1_1,int1)
& etype(freiheitsstatue_1_1,int0)
& fact(freiheitsstatue_1_1,real)
& gener(freiheitsstatue_1_1,ge)
& quant(freiheitsstatue_1_1,one)
& refer(freiheitsstatue_1_1,refer_c)
& varia(freiheitsstatue_1_1,varia_c)
& sort(c81332,d)
& card(c81332,int1)
& etype(c81332,int0)
& fact(c81332,real)
& gener(c81332,sp)
& quant(c81332,one)
& refer(c81332,det)
& varia(c81332,con)
& sort(insel__1_1,d)
& card(insel__1_1,int1)
& etype(insel__1_1,int0)
& fact(insel__1_1,real)
& gener(insel__1_1,ge)
& quant(insel__1_1,one)
& refer(insel__1_1,refer_c)
& varia(insel__1_1,varia_c)
& sort(c81339,d)
& card(c81339,int1)
& etype(c81339,int0)
& fact(c81339,real)
& gener(c81339,sp)
& quant(c81339,one)
& refer(c81339,det)
& varia(c81339,con)
& sort(c81340,na)
& card(c81340,int1)
& etype(c81340,int0)
& fact(c81340,real)
& gener(c81340,sp)
& quant(c81340,one)
& refer(c81340,indet)
& varia(c81340,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(liberty_island_0,fe)
& sort(c81355,d)
& sort(c81355,io)
& card(c81355,int1)
& etype(c81355,int1)
& fact(c81355,real)
& gener(c81355,sp)
& quant(c81355,one)
& refer(c81355,det)
& varia(c81355,con)
& sort(amerikanisch__1_1,nq)
& sort(c81366,o)
& card(c81366,int1)
& etype(c81366,int0)
& fact(c81366,real)
& gener(c81366,sp)
& quant(c81366,one)
& refer(c81366,det)
& varia(c81366,con)
& sort(national_2_1,o)
& card(national_2_1,int1)
& etype(national_2_1,int0)
& fact(national_2_1,real)
& gener(national_2_1,ge)
& quant(national_2_1,one)
& refer(national_2_1,refer_c)
& varia(national_2_1,varia_c)
& sort(c81368,d)
& card(c81368,int1)
& etype(c81368,int0)
& fact(c81368,real)
& gener(c81368,gener_c)
& quant(c81368,one)
& refer(c81368,refer_c)
& varia(c81368,varia_c)
& sort(park__1_1,d)
& card(park__1_1,int1)
& etype(park__1_1,int0)
& fact(park__1_1,real)
& gener(park__1_1,ge)
& quant(park__1_1,one)
& refer(park__1_1,refer_c)
& varia(park__1_1,varia_c)
& sort(c81373,ad)
& card(c81373,int1)
& etype(c81373,int0)
& fact(c81373,real)
& gener(c81373,gener_c)
& quant(c81373,one)
& refer(c81373,refer_c)
& varia(c81373,varia_c)
& sort(service_1_1,ad)
& card(service_1_1,int1)
& etype(service_1_1,int0)
& fact(service_1_1,real)
& gener(service_1_1,ge)
& quant(service_1_1,one)
& refer(service_1_1,refer_c)
& varia(service_1_1,varia_c)
& sort(c81378,d)
& card(c81378,int1)
& etype(c81378,int0)
& fact(c81378,real)
& gener(c81378,gener_c)
& quant(c81378,one)
& refer(c81378,refer_c)
& varia(c81378,varia_c)
& sort(enklave_1_1,d)
& card(enklave_1_1,int1)
& etype(enklave_1_1,int0)
& fact(enklave_1_1,real)
& gener(enklave_1_1,ge)
& quant(enklave_1_1,one)
& refer(enklave_1_1,refer_c)
& varia(enklave_1_1,varia_c)
& sort(c81395,d)
& card(c81395,int1)
& etype(c81395,int0)
& fact(c81395,real)
& gener(c81395,sp)
& quant(c81395,one)
& refer(c81395,det)
& varia(c81395,con)
& sort(bezirk__1_1,d)
& card(bezirk__1_1,int1)
& etype(bezirk__1_1,int0)
& fact(bezirk__1_1,real)
& gener(bezirk__1_1,ge)
& quant(bezirk__1_1,one)
& refer(bezirk__1_1,refer_c)
& varia(bezirk__1_1,varia_c)
& sort(c81401,d)
& sort(c81401,io)
& card(c81401,int1)
& etype(c81401,int0)
& fact(c81401,real)
& gener(c81401,sp)
& quant(c81401,one)
& refer(c81401,det)
& varia(c81401,con)
& sort(c81402,na)
& card(c81402,int1)
& etype(c81402,int0)
& fact(c81402,real)
& gener(c81402,sp)
& quant(c81402,one)
& refer(c81402,indet)
& varia(c81402,varia_c)
& sort(usa_0,fe)
& sort(c81409,d)
& sort(c81409,io)
& card(c81409,int1)
& etype(c81409,int0)
& fact(c81409,real)
& gener(c81409,sp)
& quant(c81409,one)
& refer(c81409,det)
& varia(c81409,con)
& sort(c81410,na)
& card(c81410,int1)
& etype(c81410,int0)
& fact(c81410,real)
& gener(c81410,sp)
& quant(c81410,one)
& refer(c81410,indet)
& varia(c81410,varia_c)
& sort(new_jersey_0,fe)
& sort(c81513,ent)
& card(c81513,card_c)
& etype(c81513,etype_c)
& fact(c81513,real)
& gener(c81513,gener_c)
& quant(c81513,quant_c)
& refer(c81513,refer_c)
& varia(c81513,varia_c)
& sort(freiheit_1_1,as)
& sort(freiheit_1_1,io)
& card(freiheit_1_1,int1)
& etype(freiheit_1_1,int0)
& fact(freiheit_1_1,real)
& gener(freiheit_1_1,ge)
& quant(freiheit_1_1,one)
& refer(freiheit_1_1,refer_c)
& varia(freiheit_1_1,varia_c)
& sort(statue_1_1,d)
& card(statue_1_1,int1)
& etype(statue_1_1,int0)
& fact(statue_1_1,real)
& gener(statue_1_1,ge)
& quant(statue_1_1,one)
& refer(statue_1_1,refer_c)
& varia(statue_1_1,varia_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_003_mira_wp_178_a270) ).
fof(f10191,plain,
( assoc(bundeland_1_1,bund_2_1)
& sub(bundeland_1_1,gebietsinstitution_1_1)
& sub(bundeland_1_1,land_1_1)
& assoc(bunderegierung_1_1,bund_1_1)
& sub(bunderegierung_1_1,regierung_1_1)
& sub(c81293,freiheitsstatue_1_1)
& sub(c81332,insel__1_1)
& attr(c81339,c81340)
& sub(c81339,insel__1_1)
& sub(c81340,name_1_1)
& val(c81340,liberty_island_0)
& prop(c81355,amerikanisch__1_1)
& sub(c81355,bunderegierung_1_1)
& sub(c81366,national_2_1)
& sub(c81368,park__1_1)
& subs(c81373,service_1_1)
& sub(c81378,enklave_1_1)
& sub(c81395,bezirk__1_1)
& attch(c81401,c81395)
& attr(c81401,c81402)
& sub(c81401,land_1_1)
& sub(c81402,name_1_1)
& val(c81402,usa_0)
& attr(c81409,c81410)
& sub(c81409,bundeland_1_1)
& sub(c81410,name_1_1)
& val(c81410,new_jersey_0)
& assoc(freiheitsstatue_1_1,freiheit_1_1)
& sub(freiheitsstatue_1_1,statue_1_1)
& sort(bundeland_1_1,d)
& sort(bundeland_1_1,io)
& card(bundeland_1_1,int1)
& etype(bundeland_1_1,int0)
& fact(bundeland_1_1,real)
& gener(bundeland_1_1,ge)
& quant(bundeland_1_1,one)
& refer(bundeland_1_1,refer_c)
& varia(bundeland_1_1,varia_c)
& sort(bund_2_1,d)
& card(bund_2_1,card_c)
& etype(bund_2_1,int1)
& fact(bund_2_1,real)
& gener(bund_2_1,ge)
& quant(bund_2_1,quant_c)
& refer(bund_2_1,refer_c)
& varia(bund_2_1,varia_c)
& sort(gebietsinstitution_1_1,ent)
& card(gebietsinstitution_1_1,card_c)
& etype(gebietsinstitution_1_1,etype_c)
& fact(gebietsinstitution_1_1,real)
& gener(gebietsinstitution_1_1,gener_c)
& quant(gebietsinstitution_1_1,quant_c)
& refer(gebietsinstitution_1_1,refer_c)
& varia(gebietsinstitution_1_1,varia_c)
& sort(land_1_1,d)
& sort(land_1_1,io)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& quant(land_1_1,one)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& sort(bunderegierung_1_1,d)
& sort(bunderegierung_1_1,io)
& card(bunderegierung_1_1,card_c)
& etype(bunderegierung_1_1,int1)
& fact(bunderegierung_1_1,real)
& gener(bunderegierung_1_1,ge)
& quant(bunderegierung_1_1,quant_c)
& refer(bunderegierung_1_1,refer_c)
& varia(bunderegierung_1_1,varia_c)
& sort(bund_1_1,d)
& sort(bund_1_1,io)
& card(bund_1_1,card_c)
& etype(bund_1_1,int1)
& fact(bund_1_1,real)
& gener(bund_1_1,ge)
& quant(bund_1_1,quant_c)
& refer(bund_1_1,refer_c)
& varia(bund_1_1,varia_c)
& sort(regierung_1_1,d)
& sort(regierung_1_1,io)
& card(regierung_1_1,card_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& quant(regierung_1_1,quant_c)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& sort(c81293,d)
& card(c81293,int1)
& etype(c81293,int0)
& fact(c81293,real)
& gener(c81293,sp)
& quant(c81293,one)
& refer(c81293,det)
& varia(c81293,con)
& sort(freiheitsstatue_1_1,d)
& card(freiheitsstatue_1_1,int1)
& etype(freiheitsstatue_1_1,int0)
& fact(freiheitsstatue_1_1,real)
& gener(freiheitsstatue_1_1,ge)
& quant(freiheitsstatue_1_1,one)
& refer(freiheitsstatue_1_1,refer_c)
& varia(freiheitsstatue_1_1,varia_c)
& sort(c81332,d)
& card(c81332,int1)
& etype(c81332,int0)
& fact(c81332,real)
& gener(c81332,sp)
& quant(c81332,one)
& refer(c81332,det)
& varia(c81332,con)
& sort(insel__1_1,d)
& card(insel__1_1,int1)
& etype(insel__1_1,int0)
& fact(insel__1_1,real)
& gener(insel__1_1,ge)
& quant(insel__1_1,one)
& refer(insel__1_1,refer_c)
& varia(insel__1_1,varia_c)
& sort(c81339,d)
& card(c81339,int1)
& etype(c81339,int0)
& fact(c81339,real)
& gener(c81339,sp)
& quant(c81339,one)
& refer(c81339,det)
& varia(c81339,con)
& sort(c81340,na)
& card(c81340,int1)
& etype(c81340,int0)
& fact(c81340,real)
& gener(c81340,sp)
& quant(c81340,one)
& refer(c81340,indet)
& varia(c81340,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(liberty_island_0,fe)
& sort(c81355,d)
& sort(c81355,io)
& card(c81355,int1)
& etype(c81355,int1)
& fact(c81355,real)
& gener(c81355,sp)
& quant(c81355,one)
& refer(c81355,det)
& varia(c81355,con)
& sort(amerikanisch__1_1,nq)
& sort(c81366,o)
& card(c81366,int1)
& etype(c81366,int0)
& fact(c81366,real)
& gener(c81366,sp)
& quant(c81366,one)
& refer(c81366,det)
& varia(c81366,con)
& sort(national_2_1,o)
& card(national_2_1,int1)
& etype(national_2_1,int0)
& fact(national_2_1,real)
& gener(national_2_1,ge)
& quant(national_2_1,one)
& refer(national_2_1,refer_c)
& varia(national_2_1,varia_c)
& sort(c81368,d)
& card(c81368,int1)
& etype(c81368,int0)
& fact(c81368,real)
& gener(c81368,gener_c)
& quant(c81368,one)
& refer(c81368,refer_c)
& varia(c81368,varia_c)
& sort(park__1_1,d)
& card(park__1_1,int1)
& etype(park__1_1,int0)
& fact(park__1_1,real)
& gener(park__1_1,ge)
& quant(park__1_1,one)
& refer(park__1_1,refer_c)
& varia(park__1_1,varia_c)
& sort(c81373,ad)
& card(c81373,int1)
& etype(c81373,int0)
& fact(c81373,real)
& gener(c81373,gener_c)
& quant(c81373,one)
& refer(c81373,refer_c)
& varia(c81373,varia_c)
& sort(service_1_1,ad)
& card(service_1_1,int1)
& etype(service_1_1,int0)
& fact(service_1_1,real)
& gener(service_1_1,ge)
& quant(service_1_1,one)
& refer(service_1_1,refer_c)
& varia(service_1_1,varia_c)
& sort(c81378,d)
& card(c81378,int1)
& etype(c81378,int0)
& fact(c81378,real)
& gener(c81378,gener_c)
& quant(c81378,one)
& refer(c81378,refer_c)
& varia(c81378,varia_c)
& sort(enklave_1_1,d)
& card(enklave_1_1,int1)
& etype(enklave_1_1,int0)
& fact(enklave_1_1,real)
& gener(enklave_1_1,ge)
& quant(enklave_1_1,one)
& refer(enklave_1_1,refer_c)
& varia(enklave_1_1,varia_c)
& sort(c81395,d)
& card(c81395,int1)
& etype(c81395,int0)
& fact(c81395,real)
& gener(c81395,sp)
& quant(c81395,one)
& refer(c81395,det)
& varia(c81395,con)
& sort(bezirk__1_1,d)
& card(bezirk__1_1,int1)
& etype(bezirk__1_1,int0)
& fact(bezirk__1_1,real)
& gener(bezirk__1_1,ge)
& quant(bezirk__1_1,one)
& refer(bezirk__1_1,refer_c)
& varia(bezirk__1_1,varia_c)
& sort(c81401,d)
& sort(c81401,io)
& card(c81401,int1)
& etype(c81401,int0)
& fact(c81401,real)
& gener(c81401,sp)
& quant(c81401,one)
& refer(c81401,det)
& varia(c81401,con)
& sort(c81402,na)
& card(c81402,int1)
& etype(c81402,int0)
& fact(c81402,real)
& gener(c81402,sp)
& quant(c81402,one)
& refer(c81402,indet)
& varia(c81402,varia_c)
& sort(usa_0,fe)
& sort(c81409,d)
& sort(c81409,io)
& card(c81409,int1)
& etype(c81409,int0)
& fact(c81409,real)
& gener(c81409,sp)
& quant(c81409,one)
& refer(c81409,det)
& varia(c81409,con)
& sort(c81410,na)
& card(c81410,int1)
& etype(c81410,int0)
& fact(c81410,real)
& gener(c81410,sp)
& quant(c81410,one)
& refer(c81410,indet)
& varia(c81410,varia_c)
& sort(new_jersey_0,fe)
& sort(c81513,ent)
& card(c81513,card_c)
& etype(c81513,etype_c)
& fact(c81513,real)
& gener(c81513,gener_c)
& quant(c81513,quant_c)
& refer(c81513,refer_c)
& varia(c81513,varia_c)
& sort(freiheit_1_1,as)
& sort(freiheit_1_1,io)
& card(freiheit_1_1,int1)
& etype(freiheit_1_1,int0)
& fact(freiheit_1_1,real)
& gener(freiheit_1_1,ge)
& quant(freiheit_1_1,one)
& refer(freiheit_1_1,refer_c)
& varia(freiheit_1_1,varia_c)
& sort(statue_1_1,d)
& card(statue_1_1,int1)
& etype(statue_1_1,int0)
& fact(statue_1_1,real)
& gener(statue_1_1,ge)
& quant(statue_1_1,one)
& refer(statue_1_1,refer_c)
& varia(statue_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10317,plain,
! [X0,X1] :
( ( in(X0,X1)
| an(X0,X1) )
=> flp(X0,X1) ),
inference(pure_predicate_removal,[],[f176]) ).
fof(f10319,plain,
! [X0,X1] :
( in(X0,X1)
=> flp(X0,X1) ),
inference(pure_predicate_removal,[],[f10317]) ).
fof(f10327,plain,
( assoc(bundeland_1_1,bund_2_1)
& sub(bundeland_1_1,gebietsinstitution_1_1)
& sub(bundeland_1_1,land_1_1)
& assoc(bunderegierung_1_1,bund_1_1)
& sub(bunderegierung_1_1,regierung_1_1)
& sub(c81293,freiheitsstatue_1_1)
& sub(c81332,insel__1_1)
& attr(c81339,c81340)
& sub(c81339,insel__1_1)
& sub(c81340,name_1_1)
& val(c81340,liberty_island_0)
& prop(c81355,amerikanisch__1_1)
& sub(c81355,bunderegierung_1_1)
& sub(c81366,national_2_1)
& sub(c81368,park__1_1)
& subs(c81373,service_1_1)
& sub(c81378,enklave_1_1)
& sub(c81395,bezirk__1_1)
& attch(c81401,c81395)
& attr(c81401,c81402)
& sub(c81401,land_1_1)
& sub(c81402,name_1_1)
& val(c81402,usa_0)
& attr(c81409,c81410)
& sub(c81409,bundeland_1_1)
& sub(c81410,name_1_1)
& val(c81410,new_jersey_0)
& assoc(freiheitsstatue_1_1,freiheit_1_1)
& sub(freiheitsstatue_1_1,statue_1_1)
& card(bundeland_1_1,int1)
& etype(bundeland_1_1,int0)
& fact(bundeland_1_1,real)
& gener(bundeland_1_1,ge)
& quant(bundeland_1_1,one)
& refer(bundeland_1_1,refer_c)
& varia(bundeland_1_1,varia_c)
& card(bund_2_1,card_c)
& etype(bund_2_1,int1)
& fact(bund_2_1,real)
& gener(bund_2_1,ge)
& quant(bund_2_1,quant_c)
& refer(bund_2_1,refer_c)
& varia(bund_2_1,varia_c)
& card(gebietsinstitution_1_1,card_c)
& etype(gebietsinstitution_1_1,etype_c)
& fact(gebietsinstitution_1_1,real)
& gener(gebietsinstitution_1_1,gener_c)
& quant(gebietsinstitution_1_1,quant_c)
& refer(gebietsinstitution_1_1,refer_c)
& varia(gebietsinstitution_1_1,varia_c)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& quant(land_1_1,one)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& card(bunderegierung_1_1,card_c)
& etype(bunderegierung_1_1,int1)
& fact(bunderegierung_1_1,real)
& gener(bunderegierung_1_1,ge)
& quant(bunderegierung_1_1,quant_c)
& refer(bunderegierung_1_1,refer_c)
& varia(bunderegierung_1_1,varia_c)
& card(bund_1_1,card_c)
& etype(bund_1_1,int1)
& fact(bund_1_1,real)
& gener(bund_1_1,ge)
& quant(bund_1_1,quant_c)
& refer(bund_1_1,refer_c)
& varia(bund_1_1,varia_c)
& card(regierung_1_1,card_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& quant(regierung_1_1,quant_c)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& card(c81293,int1)
& etype(c81293,int0)
& fact(c81293,real)
& gener(c81293,sp)
& quant(c81293,one)
& refer(c81293,det)
& varia(c81293,con)
& card(freiheitsstatue_1_1,int1)
& etype(freiheitsstatue_1_1,int0)
& fact(freiheitsstatue_1_1,real)
& gener(freiheitsstatue_1_1,ge)
& quant(freiheitsstatue_1_1,one)
& refer(freiheitsstatue_1_1,refer_c)
& varia(freiheitsstatue_1_1,varia_c)
& card(c81332,int1)
& etype(c81332,int0)
& fact(c81332,real)
& gener(c81332,sp)
& quant(c81332,one)
& refer(c81332,det)
& varia(c81332,con)
& card(insel__1_1,int1)
& etype(insel__1_1,int0)
& fact(insel__1_1,real)
& gener(insel__1_1,ge)
& quant(insel__1_1,one)
& refer(insel__1_1,refer_c)
& varia(insel__1_1,varia_c)
& card(c81339,int1)
& etype(c81339,int0)
& fact(c81339,real)
& gener(c81339,sp)
& quant(c81339,one)
& refer(c81339,det)
& varia(c81339,con)
& card(c81340,int1)
& etype(c81340,int0)
& fact(c81340,real)
& gener(c81340,sp)
& quant(c81340,one)
& refer(c81340,indet)
& varia(c81340,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(c81355,int1)
& etype(c81355,int1)
& fact(c81355,real)
& gener(c81355,sp)
& quant(c81355,one)
& refer(c81355,det)
& varia(c81355,con)
& card(c81366,int1)
& etype(c81366,int0)
& fact(c81366,real)
& gener(c81366,sp)
& quant(c81366,one)
& refer(c81366,det)
& varia(c81366,con)
& card(national_2_1,int1)
& etype(national_2_1,int0)
& fact(national_2_1,real)
& gener(national_2_1,ge)
& quant(national_2_1,one)
& refer(national_2_1,refer_c)
& varia(national_2_1,varia_c)
& card(c81368,int1)
& etype(c81368,int0)
& fact(c81368,real)
& gener(c81368,gener_c)
& quant(c81368,one)
& refer(c81368,refer_c)
& varia(c81368,varia_c)
& card(park__1_1,int1)
& etype(park__1_1,int0)
& fact(park__1_1,real)
& gener(park__1_1,ge)
& quant(park__1_1,one)
& refer(park__1_1,refer_c)
& varia(park__1_1,varia_c)
& card(c81373,int1)
& etype(c81373,int0)
& fact(c81373,real)
& gener(c81373,gener_c)
& quant(c81373,one)
& refer(c81373,refer_c)
& varia(c81373,varia_c)
& card(service_1_1,int1)
& etype(service_1_1,int0)
& fact(service_1_1,real)
& gener(service_1_1,ge)
& quant(service_1_1,one)
& refer(service_1_1,refer_c)
& varia(service_1_1,varia_c)
& card(c81378,int1)
& etype(c81378,int0)
& fact(c81378,real)
& gener(c81378,gener_c)
& quant(c81378,one)
& refer(c81378,refer_c)
& varia(c81378,varia_c)
& card(enklave_1_1,int1)
& etype(enklave_1_1,int0)
& fact(enklave_1_1,real)
& gener(enklave_1_1,ge)
& quant(enklave_1_1,one)
& refer(enklave_1_1,refer_c)
& varia(enklave_1_1,varia_c)
& card(c81395,int1)
& etype(c81395,int0)
& fact(c81395,real)
& gener(c81395,sp)
& quant(c81395,one)
& refer(c81395,det)
& varia(c81395,con)
& card(bezirk__1_1,int1)
& etype(bezirk__1_1,int0)
& fact(bezirk__1_1,real)
& gener(bezirk__1_1,ge)
& quant(bezirk__1_1,one)
& refer(bezirk__1_1,refer_c)
& varia(bezirk__1_1,varia_c)
& card(c81401,int1)
& etype(c81401,int0)
& fact(c81401,real)
& gener(c81401,sp)
& quant(c81401,one)
& refer(c81401,det)
& varia(c81401,con)
& card(c81402,int1)
& etype(c81402,int0)
& fact(c81402,real)
& gener(c81402,sp)
& quant(c81402,one)
& refer(c81402,indet)
& varia(c81402,varia_c)
& card(c81409,int1)
& etype(c81409,int0)
& fact(c81409,real)
& gener(c81409,sp)
& quant(c81409,one)
& refer(c81409,det)
& varia(c81409,con)
& card(c81410,int1)
& etype(c81410,int0)
& fact(c81410,real)
& gener(c81410,sp)
& quant(c81410,one)
& refer(c81410,indet)
& varia(c81410,varia_c)
& card(c81513,card_c)
& etype(c81513,etype_c)
& fact(c81513,real)
& gener(c81513,gener_c)
& quant(c81513,quant_c)
& refer(c81513,refer_c)
& varia(c81513,varia_c)
& card(freiheit_1_1,int1)
& etype(freiheit_1_1,int0)
& fact(freiheit_1_1,real)
& gener(freiheit_1_1,ge)
& quant(freiheit_1_1,one)
& refer(freiheit_1_1,refer_c)
& varia(freiheit_1_1,varia_c)
& card(statue_1_1,int1)
& etype(statue_1_1,int0)
& fact(statue_1_1,real)
& gener(statue_1_1,ge)
& quant(statue_1_1,one)
& refer(statue_1_1,refer_c)
& varia(statue_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10330,plain,
( assoc(bundeland_1_1,bund_2_1)
& sub(bundeland_1_1,gebietsinstitution_1_1)
& sub(bundeland_1_1,land_1_1)
& assoc(bunderegierung_1_1,bund_1_1)
& sub(bunderegierung_1_1,regierung_1_1)
& sub(c81293,freiheitsstatue_1_1)
& sub(c81332,insel__1_1)
& attr(c81339,c81340)
& sub(c81339,insel__1_1)
& sub(c81340,name_1_1)
& val(c81340,liberty_island_0)
& prop(c81355,amerikanisch__1_1)
& sub(c81355,bunderegierung_1_1)
& sub(c81366,national_2_1)
& sub(c81368,park__1_1)
& subs(c81373,service_1_1)
& sub(c81378,enklave_1_1)
& sub(c81395,bezirk__1_1)
& attch(c81401,c81395)
& attr(c81401,c81402)
& sub(c81401,land_1_1)
& sub(c81402,name_1_1)
& val(c81402,usa_0)
& attr(c81409,c81410)
& sub(c81409,bundeland_1_1)
& sub(c81410,name_1_1)
& val(c81410,new_jersey_0)
& assoc(freiheitsstatue_1_1,freiheit_1_1)
& sub(freiheitsstatue_1_1,statue_1_1)
& card(bundeland_1_1,int1)
& etype(bundeland_1_1,int0)
& fact(bundeland_1_1,real)
& gener(bundeland_1_1,ge)
& refer(bundeland_1_1,refer_c)
& varia(bundeland_1_1,varia_c)
& card(bund_2_1,card_c)
& etype(bund_2_1,int1)
& fact(bund_2_1,real)
& gener(bund_2_1,ge)
& refer(bund_2_1,refer_c)
& varia(bund_2_1,varia_c)
& card(gebietsinstitution_1_1,card_c)
& etype(gebietsinstitution_1_1,etype_c)
& fact(gebietsinstitution_1_1,real)
& gener(gebietsinstitution_1_1,gener_c)
& refer(gebietsinstitution_1_1,refer_c)
& varia(gebietsinstitution_1_1,varia_c)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& card(bunderegierung_1_1,card_c)
& etype(bunderegierung_1_1,int1)
& fact(bunderegierung_1_1,real)
& gener(bunderegierung_1_1,ge)
& refer(bunderegierung_1_1,refer_c)
& varia(bunderegierung_1_1,varia_c)
& card(bund_1_1,card_c)
& etype(bund_1_1,int1)
& fact(bund_1_1,real)
& gener(bund_1_1,ge)
& refer(bund_1_1,refer_c)
& varia(bund_1_1,varia_c)
& card(regierung_1_1,card_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& card(c81293,int1)
& etype(c81293,int0)
& fact(c81293,real)
& gener(c81293,sp)
& refer(c81293,det)
& varia(c81293,con)
& card(freiheitsstatue_1_1,int1)
& etype(freiheitsstatue_1_1,int0)
& fact(freiheitsstatue_1_1,real)
& gener(freiheitsstatue_1_1,ge)
& refer(freiheitsstatue_1_1,refer_c)
& varia(freiheitsstatue_1_1,varia_c)
& card(c81332,int1)
& etype(c81332,int0)
& fact(c81332,real)
& gener(c81332,sp)
& refer(c81332,det)
& varia(c81332,con)
& card(insel__1_1,int1)
& etype(insel__1_1,int0)
& fact(insel__1_1,real)
& gener(insel__1_1,ge)
& refer(insel__1_1,refer_c)
& varia(insel__1_1,varia_c)
& card(c81339,int1)
& etype(c81339,int0)
& fact(c81339,real)
& gener(c81339,sp)
& refer(c81339,det)
& varia(c81339,con)
& card(c81340,int1)
& etype(c81340,int0)
& fact(c81340,real)
& gener(c81340,sp)
& refer(c81340,indet)
& varia(c81340,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(c81355,int1)
& etype(c81355,int1)
& fact(c81355,real)
& gener(c81355,sp)
& refer(c81355,det)
& varia(c81355,con)
& card(c81366,int1)
& etype(c81366,int0)
& fact(c81366,real)
& gener(c81366,sp)
& refer(c81366,det)
& varia(c81366,con)
& card(national_2_1,int1)
& etype(national_2_1,int0)
& fact(national_2_1,real)
& gener(national_2_1,ge)
& refer(national_2_1,refer_c)
& varia(national_2_1,varia_c)
& card(c81368,int1)
& etype(c81368,int0)
& fact(c81368,real)
& gener(c81368,gener_c)
& refer(c81368,refer_c)
& varia(c81368,varia_c)
& card(park__1_1,int1)
& etype(park__1_1,int0)
& fact(park__1_1,real)
& gener(park__1_1,ge)
& refer(park__1_1,refer_c)
& varia(park__1_1,varia_c)
& card(c81373,int1)
& etype(c81373,int0)
& fact(c81373,real)
& gener(c81373,gener_c)
& refer(c81373,refer_c)
& varia(c81373,varia_c)
& card(service_1_1,int1)
& etype(service_1_1,int0)
& fact(service_1_1,real)
& gener(service_1_1,ge)
& refer(service_1_1,refer_c)
& varia(service_1_1,varia_c)
& card(c81378,int1)
& etype(c81378,int0)
& fact(c81378,real)
& gener(c81378,gener_c)
& refer(c81378,refer_c)
& varia(c81378,varia_c)
& card(enklave_1_1,int1)
& etype(enklave_1_1,int0)
& fact(enklave_1_1,real)
& gener(enklave_1_1,ge)
& refer(enklave_1_1,refer_c)
& varia(enklave_1_1,varia_c)
& card(c81395,int1)
& etype(c81395,int0)
& fact(c81395,real)
& gener(c81395,sp)
& refer(c81395,det)
& varia(c81395,con)
& card(bezirk__1_1,int1)
& etype(bezirk__1_1,int0)
& fact(bezirk__1_1,real)
& gener(bezirk__1_1,ge)
& refer(bezirk__1_1,refer_c)
& varia(bezirk__1_1,varia_c)
& card(c81401,int1)
& etype(c81401,int0)
& fact(c81401,real)
& gener(c81401,sp)
& refer(c81401,det)
& varia(c81401,con)
& card(c81402,int1)
& etype(c81402,int0)
& fact(c81402,real)
& gener(c81402,sp)
& refer(c81402,indet)
& varia(c81402,varia_c)
& card(c81409,int1)
& etype(c81409,int0)
& fact(c81409,real)
& gener(c81409,sp)
& refer(c81409,det)
& varia(c81409,con)
& card(c81410,int1)
& etype(c81410,int0)
& fact(c81410,real)
& gener(c81410,sp)
& refer(c81410,indet)
& varia(c81410,varia_c)
& card(c81513,card_c)
& etype(c81513,etype_c)
& fact(c81513,real)
& gener(c81513,gener_c)
& refer(c81513,refer_c)
& varia(c81513,varia_c)
& card(freiheit_1_1,int1)
& etype(freiheit_1_1,int0)
& fact(freiheit_1_1,real)
& gener(freiheit_1_1,ge)
& refer(freiheit_1_1,refer_c)
& varia(freiheit_1_1,varia_c)
& card(statue_1_1,int1)
& etype(statue_1_1,int0)
& fact(statue_1_1,real)
& gener(statue_1_1,ge)
& refer(statue_1_1,refer_c)
& varia(statue_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10327]) ).
fof(f10333,plain,
( assoc(bundeland_1_1,bund_2_1)
& sub(bundeland_1_1,gebietsinstitution_1_1)
& sub(bundeland_1_1,land_1_1)
& assoc(bunderegierung_1_1,bund_1_1)
& sub(bunderegierung_1_1,regierung_1_1)
& sub(c81293,freiheitsstatue_1_1)
& sub(c81332,insel__1_1)
& attr(c81339,c81340)
& sub(c81339,insel__1_1)
& sub(c81340,name_1_1)
& val(c81340,liberty_island_0)
& prop(c81355,amerikanisch__1_1)
& sub(c81355,bunderegierung_1_1)
& sub(c81366,national_2_1)
& sub(c81368,park__1_1)
& subs(c81373,service_1_1)
& sub(c81378,enklave_1_1)
& sub(c81395,bezirk__1_1)
& attch(c81401,c81395)
& attr(c81401,c81402)
& sub(c81401,land_1_1)
& sub(c81402,name_1_1)
& val(c81402,usa_0)
& attr(c81409,c81410)
& sub(c81409,bundeland_1_1)
& sub(c81410,name_1_1)
& val(c81410,new_jersey_0)
& assoc(freiheitsstatue_1_1,freiheit_1_1)
& sub(freiheitsstatue_1_1,statue_1_1)
& etype(bundeland_1_1,int0)
& fact(bundeland_1_1,real)
& gener(bundeland_1_1,ge)
& refer(bundeland_1_1,refer_c)
& varia(bundeland_1_1,varia_c)
& etype(bund_2_1,int1)
& fact(bund_2_1,real)
& gener(bund_2_1,ge)
& refer(bund_2_1,refer_c)
& varia(bund_2_1,varia_c)
& etype(gebietsinstitution_1_1,etype_c)
& fact(gebietsinstitution_1_1,real)
& gener(gebietsinstitution_1_1,gener_c)
& refer(gebietsinstitution_1_1,refer_c)
& varia(gebietsinstitution_1_1,varia_c)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& etype(bunderegierung_1_1,int1)
& fact(bunderegierung_1_1,real)
& gener(bunderegierung_1_1,ge)
& refer(bunderegierung_1_1,refer_c)
& varia(bunderegierung_1_1,varia_c)
& etype(bund_1_1,int1)
& fact(bund_1_1,real)
& gener(bund_1_1,ge)
& refer(bund_1_1,refer_c)
& varia(bund_1_1,varia_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& etype(c81293,int0)
& fact(c81293,real)
& gener(c81293,sp)
& refer(c81293,det)
& varia(c81293,con)
& etype(freiheitsstatue_1_1,int0)
& fact(freiheitsstatue_1_1,real)
& gener(freiheitsstatue_1_1,ge)
& refer(freiheitsstatue_1_1,refer_c)
& varia(freiheitsstatue_1_1,varia_c)
& etype(c81332,int0)
& fact(c81332,real)
& gener(c81332,sp)
& refer(c81332,det)
& varia(c81332,con)
& etype(insel__1_1,int0)
& fact(insel__1_1,real)
& gener(insel__1_1,ge)
& refer(insel__1_1,refer_c)
& varia(insel__1_1,varia_c)
& etype(c81339,int0)
& fact(c81339,real)
& gener(c81339,sp)
& refer(c81339,det)
& varia(c81339,con)
& etype(c81340,int0)
& fact(c81340,real)
& gener(c81340,sp)
& refer(c81340,indet)
& varia(c81340,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(c81355,int1)
& fact(c81355,real)
& gener(c81355,sp)
& refer(c81355,det)
& varia(c81355,con)
& etype(c81366,int0)
& fact(c81366,real)
& gener(c81366,sp)
& refer(c81366,det)
& varia(c81366,con)
& etype(national_2_1,int0)
& fact(national_2_1,real)
& gener(national_2_1,ge)
& refer(national_2_1,refer_c)
& varia(national_2_1,varia_c)
& etype(c81368,int0)
& fact(c81368,real)
& gener(c81368,gener_c)
& refer(c81368,refer_c)
& varia(c81368,varia_c)
& etype(park__1_1,int0)
& fact(park__1_1,real)
& gener(park__1_1,ge)
& refer(park__1_1,refer_c)
& varia(park__1_1,varia_c)
& etype(c81373,int0)
& fact(c81373,real)
& gener(c81373,gener_c)
& refer(c81373,refer_c)
& varia(c81373,varia_c)
& etype(service_1_1,int0)
& fact(service_1_1,real)
& gener(service_1_1,ge)
& refer(service_1_1,refer_c)
& varia(service_1_1,varia_c)
& etype(c81378,int0)
& fact(c81378,real)
& gener(c81378,gener_c)
& refer(c81378,refer_c)
& varia(c81378,varia_c)
& etype(enklave_1_1,int0)
& fact(enklave_1_1,real)
& gener(enklave_1_1,ge)
& refer(enklave_1_1,refer_c)
& varia(enklave_1_1,varia_c)
& etype(c81395,int0)
& fact(c81395,real)
& gener(c81395,sp)
& refer(c81395,det)
& varia(c81395,con)
& etype(bezirk__1_1,int0)
& fact(bezirk__1_1,real)
& gener(bezirk__1_1,ge)
& refer(bezirk__1_1,refer_c)
& varia(bezirk__1_1,varia_c)
& etype(c81401,int0)
& fact(c81401,real)
& gener(c81401,sp)
& refer(c81401,det)
& varia(c81401,con)
& etype(c81402,int0)
& fact(c81402,real)
& gener(c81402,sp)
& refer(c81402,indet)
& varia(c81402,varia_c)
& etype(c81409,int0)
& fact(c81409,real)
& gener(c81409,sp)
& refer(c81409,det)
& varia(c81409,con)
& etype(c81410,int0)
& fact(c81410,real)
& gener(c81410,sp)
& refer(c81410,indet)
& varia(c81410,varia_c)
& etype(c81513,etype_c)
& fact(c81513,real)
& gener(c81513,gener_c)
& refer(c81513,refer_c)
& varia(c81513,varia_c)
& etype(freiheit_1_1,int0)
& fact(freiheit_1_1,real)
& gener(freiheit_1_1,ge)
& refer(freiheit_1_1,refer_c)
& varia(freiheit_1_1,varia_c)
& etype(statue_1_1,int0)
& fact(statue_1_1,real)
& gener(statue_1_1,ge)
& refer(statue_1_1,refer_c)
& varia(statue_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10330]) ).
fof(f10336,plain,
( assoc(bundeland_1_1,bund_2_1)
& sub(bundeland_1_1,gebietsinstitution_1_1)
& sub(bundeland_1_1,land_1_1)
& assoc(bunderegierung_1_1,bund_1_1)
& sub(bunderegierung_1_1,regierung_1_1)
& sub(c81293,freiheitsstatue_1_1)
& sub(c81332,insel__1_1)
& attr(c81339,c81340)
& sub(c81339,insel__1_1)
& sub(c81340,name_1_1)
& val(c81340,liberty_island_0)
& prop(c81355,amerikanisch__1_1)
& sub(c81355,bunderegierung_1_1)
& sub(c81366,national_2_1)
& sub(c81368,park__1_1)
& subs(c81373,service_1_1)
& sub(c81378,enklave_1_1)
& sub(c81395,bezirk__1_1)
& attch(c81401,c81395)
& attr(c81401,c81402)
& sub(c81401,land_1_1)
& sub(c81402,name_1_1)
& val(c81402,usa_0)
& attr(c81409,c81410)
& sub(c81409,bundeland_1_1)
& sub(c81410,name_1_1)
& val(c81410,new_jersey_0)
& assoc(freiheitsstatue_1_1,freiheit_1_1)
& sub(freiheitsstatue_1_1,statue_1_1)
& etype(bundeland_1_1,int0)
& fact(bundeland_1_1,real)
& gener(bundeland_1_1,ge)
& varia(bundeland_1_1,varia_c)
& etype(bund_2_1,int1)
& fact(bund_2_1,real)
& gener(bund_2_1,ge)
& varia(bund_2_1,varia_c)
& etype(gebietsinstitution_1_1,etype_c)
& fact(gebietsinstitution_1_1,real)
& gener(gebietsinstitution_1_1,gener_c)
& varia(gebietsinstitution_1_1,varia_c)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& varia(land_1_1,varia_c)
& etype(bunderegierung_1_1,int1)
& fact(bunderegierung_1_1,real)
& gener(bunderegierung_1_1,ge)
& varia(bunderegierung_1_1,varia_c)
& etype(bund_1_1,int1)
& fact(bund_1_1,real)
& gener(bund_1_1,ge)
& varia(bund_1_1,varia_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& varia(regierung_1_1,varia_c)
& etype(c81293,int0)
& fact(c81293,real)
& gener(c81293,sp)
& varia(c81293,con)
& etype(freiheitsstatue_1_1,int0)
& fact(freiheitsstatue_1_1,real)
& gener(freiheitsstatue_1_1,ge)
& varia(freiheitsstatue_1_1,varia_c)
& etype(c81332,int0)
& fact(c81332,real)
& gener(c81332,sp)
& varia(c81332,con)
& etype(insel__1_1,int0)
& fact(insel__1_1,real)
& gener(insel__1_1,ge)
& varia(insel__1_1,varia_c)
& etype(c81339,int0)
& fact(c81339,real)
& gener(c81339,sp)
& varia(c81339,con)
& etype(c81340,int0)
& fact(c81340,real)
& gener(c81340,sp)
& varia(c81340,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& varia(name_1_1,varia_c)
& etype(c81355,int1)
& fact(c81355,real)
& gener(c81355,sp)
& varia(c81355,con)
& etype(c81366,int0)
& fact(c81366,real)
& gener(c81366,sp)
& varia(c81366,con)
& etype(national_2_1,int0)
& fact(national_2_1,real)
& gener(national_2_1,ge)
& varia(national_2_1,varia_c)
& etype(c81368,int0)
& fact(c81368,real)
& gener(c81368,gener_c)
& varia(c81368,varia_c)
& etype(park__1_1,int0)
& fact(park__1_1,real)
& gener(park__1_1,ge)
& varia(park__1_1,varia_c)
& etype(c81373,int0)
& fact(c81373,real)
& gener(c81373,gener_c)
& varia(c81373,varia_c)
& etype(service_1_1,int0)
& fact(service_1_1,real)
& gener(service_1_1,ge)
& varia(service_1_1,varia_c)
& etype(c81378,int0)
& fact(c81378,real)
& gener(c81378,gener_c)
& varia(c81378,varia_c)
& etype(enklave_1_1,int0)
& fact(enklave_1_1,real)
& gener(enklave_1_1,ge)
& varia(enklave_1_1,varia_c)
& etype(c81395,int0)
& fact(c81395,real)
& gener(c81395,sp)
& varia(c81395,con)
& etype(bezirk__1_1,int0)
& fact(bezirk__1_1,real)
& gener(bezirk__1_1,ge)
& varia(bezirk__1_1,varia_c)
& etype(c81401,int0)
& fact(c81401,real)
& gener(c81401,sp)
& varia(c81401,con)
& etype(c81402,int0)
& fact(c81402,real)
& gener(c81402,sp)
& varia(c81402,varia_c)
& etype(c81409,int0)
& fact(c81409,real)
& gener(c81409,sp)
& varia(c81409,con)
& etype(c81410,int0)
& fact(c81410,real)
& gener(c81410,sp)
& varia(c81410,varia_c)
& etype(c81513,etype_c)
& fact(c81513,real)
& gener(c81513,gener_c)
& varia(c81513,varia_c)
& etype(freiheit_1_1,int0)
& fact(freiheit_1_1,real)
& gener(freiheit_1_1,ge)
& varia(freiheit_1_1,varia_c)
& etype(statue_1_1,int0)
& fact(statue_1_1,real)
& gener(statue_1_1,ge)
& varia(statue_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10333]) ).
fof(f10341,plain,
( assoc(bundeland_1_1,bund_2_1)
& sub(bundeland_1_1,gebietsinstitution_1_1)
& sub(bundeland_1_1,land_1_1)
& assoc(bunderegierung_1_1,bund_1_1)
& sub(bunderegierung_1_1,regierung_1_1)
& sub(c81293,freiheitsstatue_1_1)
& sub(c81332,insel__1_1)
& attr(c81339,c81340)
& sub(c81339,insel__1_1)
& sub(c81340,name_1_1)
& val(c81340,liberty_island_0)
& prop(c81355,amerikanisch__1_1)
& sub(c81355,bunderegierung_1_1)
& sub(c81366,national_2_1)
& sub(c81368,park__1_1)
& subs(c81373,service_1_1)
& sub(c81378,enklave_1_1)
& sub(c81395,bezirk__1_1)
& attch(c81401,c81395)
& attr(c81401,c81402)
& sub(c81401,land_1_1)
& sub(c81402,name_1_1)
& val(c81402,usa_0)
& attr(c81409,c81410)
& sub(c81409,bundeland_1_1)
& sub(c81410,name_1_1)
& val(c81410,new_jersey_0)
& assoc(freiheitsstatue_1_1,freiheit_1_1)
& sub(freiheitsstatue_1_1,statue_1_1)
& etype(bundeland_1_1,int0)
& fact(bundeland_1_1,real)
& gener(bundeland_1_1,ge)
& etype(bund_2_1,int1)
& fact(bund_2_1,real)
& gener(bund_2_1,ge)
& etype(gebietsinstitution_1_1,etype_c)
& fact(gebietsinstitution_1_1,real)
& gener(gebietsinstitution_1_1,gener_c)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& etype(bunderegierung_1_1,int1)
& fact(bunderegierung_1_1,real)
& gener(bunderegierung_1_1,ge)
& etype(bund_1_1,int1)
& fact(bund_1_1,real)
& gener(bund_1_1,ge)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& etype(c81293,int0)
& fact(c81293,real)
& gener(c81293,sp)
& etype(freiheitsstatue_1_1,int0)
& fact(freiheitsstatue_1_1,real)
& gener(freiheitsstatue_1_1,ge)
& etype(c81332,int0)
& fact(c81332,real)
& gener(c81332,sp)
& etype(insel__1_1,int0)
& fact(insel__1_1,real)
& gener(insel__1_1,ge)
& etype(c81339,int0)
& fact(c81339,real)
& gener(c81339,sp)
& etype(c81340,int0)
& fact(c81340,real)
& gener(c81340,sp)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& etype(c81355,int1)
& fact(c81355,real)
& gener(c81355,sp)
& etype(c81366,int0)
& fact(c81366,real)
& gener(c81366,sp)
& etype(national_2_1,int0)
& fact(national_2_1,real)
& gener(national_2_1,ge)
& etype(c81368,int0)
& fact(c81368,real)
& gener(c81368,gener_c)
& etype(park__1_1,int0)
& fact(park__1_1,real)
& gener(park__1_1,ge)
& etype(c81373,int0)
& fact(c81373,real)
& gener(c81373,gener_c)
& etype(service_1_1,int0)
& fact(service_1_1,real)
& gener(service_1_1,ge)
& etype(c81378,int0)
& fact(c81378,real)
& gener(c81378,gener_c)
& etype(enklave_1_1,int0)
& fact(enklave_1_1,real)
& gener(enklave_1_1,ge)
& etype(c81395,int0)
& fact(c81395,real)
& gener(c81395,sp)
& etype(bezirk__1_1,int0)
& fact(bezirk__1_1,real)
& gener(bezirk__1_1,ge)
& etype(c81401,int0)
& fact(c81401,real)
& gener(c81401,sp)
& etype(c81402,int0)
& fact(c81402,real)
& gener(c81402,sp)
& etype(c81409,int0)
& fact(c81409,real)
& gener(c81409,sp)
& etype(c81410,int0)
& fact(c81410,real)
& gener(c81410,sp)
& etype(c81513,etype_c)
& fact(c81513,real)
& gener(c81513,gener_c)
& etype(freiheit_1_1,int0)
& fact(freiheit_1_1,real)
& gener(freiheit_1_1,ge)
& etype(statue_1_1,int0)
& fact(statue_1_1,real)
& gener(statue_1_1,ge) ),
inference(pure_predicate_removal,[],[f10336]) ).
fof(f10346,plain,
( assoc(bundeland_1_1,bund_2_1)
& sub(bundeland_1_1,gebietsinstitution_1_1)
& sub(bundeland_1_1,land_1_1)
& assoc(bunderegierung_1_1,bund_1_1)
& sub(bunderegierung_1_1,regierung_1_1)
& sub(c81293,freiheitsstatue_1_1)
& sub(c81332,insel__1_1)
& attr(c81339,c81340)
& sub(c81339,insel__1_1)
& sub(c81340,name_1_1)
& val(c81340,liberty_island_0)
& prop(c81355,amerikanisch__1_1)
& sub(c81355,bunderegierung_1_1)
& sub(c81366,national_2_1)
& sub(c81368,park__1_1)
& subs(c81373,service_1_1)
& sub(c81378,enklave_1_1)
& sub(c81395,bezirk__1_1)
& attch(c81401,c81395)
& attr(c81401,c81402)
& sub(c81401,land_1_1)
& sub(c81402,name_1_1)
& val(c81402,usa_0)
& attr(c81409,c81410)
& sub(c81409,bundeland_1_1)
& sub(c81410,name_1_1)
& val(c81410,new_jersey_0)
& assoc(freiheitsstatue_1_1,freiheit_1_1)
& sub(freiheitsstatue_1_1,statue_1_1)
& etype(bundeland_1_1,int0)
& fact(bundeland_1_1,real)
& etype(bund_2_1,int1)
& fact(bund_2_1,real)
& etype(gebietsinstitution_1_1,etype_c)
& fact(gebietsinstitution_1_1,real)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& etype(bunderegierung_1_1,int1)
& fact(bunderegierung_1_1,real)
& etype(bund_1_1,int1)
& fact(bund_1_1,real)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& etype(c81293,int0)
& fact(c81293,real)
& etype(freiheitsstatue_1_1,int0)
& fact(freiheitsstatue_1_1,real)
& etype(c81332,int0)
& fact(c81332,real)
& etype(insel__1_1,int0)
& fact(insel__1_1,real)
& etype(c81339,int0)
& fact(c81339,real)
& etype(c81340,int0)
& fact(c81340,real)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& etype(c81355,int1)
& fact(c81355,real)
& etype(c81366,int0)
& fact(c81366,real)
& etype(national_2_1,int0)
& fact(national_2_1,real)
& etype(c81368,int0)
& fact(c81368,real)
& etype(park__1_1,int0)
& fact(park__1_1,real)
& etype(c81373,int0)
& fact(c81373,real)
& etype(service_1_1,int0)
& fact(service_1_1,real)
& etype(c81378,int0)
& fact(c81378,real)
& etype(enklave_1_1,int0)
& fact(enklave_1_1,real)
& etype(c81395,int0)
& fact(c81395,real)
& etype(bezirk__1_1,int0)
& fact(bezirk__1_1,real)
& etype(c81401,int0)
& fact(c81401,real)
& etype(c81402,int0)
& fact(c81402,real)
& etype(c81409,int0)
& fact(c81409,real)
& etype(c81410,int0)
& fact(c81410,real)
& etype(c81513,etype_c)
& fact(c81513,real)
& etype(freiheit_1_1,int0)
& fact(freiheit_1_1,real)
& etype(statue_1_1,int0)
& fact(statue_1_1,real) ),
inference(pure_predicate_removal,[],[f10341]) ).
fof(f10350,plain,
! [X0,X1] :
( has_fact_leq(X0,X1)
| ~ fact(X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f10399,plain,
! [X0,X1] :
( ? [X2] :
( loc(X2,X0)
& obj(X2,X1)
& subs(X2,geben_1_1) )
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(ennf_transformation,[],[f95]) ).
fof(f10400,plain,
! [X0,X1] :
( ? [X2] :
( loc(X2,X0)
& obj(X2,X1)
& subs(X2,geben_1_1) )
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(flattening,[],[f10399]) ).
fof(f10508,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( in(X5,X3)
& attr(X3,X4)
& loc(X0,X5)
& sub(X3,land_1_1)
& sub(X4,name_1_1)
& val(X4,X2) )
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(ennf_transformation,[],[f155]) ).
fof(f10509,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( in(X5,X3)
& attr(X3,X4)
& loc(X0,X5)
& sub(X3,land_1_1)
& sub(X4,name_1_1)
& val(X4,X2) )
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(flattening,[],[f10508]) ).
fof(f10543,plain,
! [X0,X1] :
( flp(X0,X1)
| ~ in(X0,X1) ),
inference(ennf_transformation,[],[f10319]) ).
fof(f10548,plain,
! [X0,X1] :
( ? [X2] :
( loc(X2,X1)
& scar(X2,X0)
& subs(X2,stehen_1_1) )
| ~ loc(X0,X1) ),
inference(ennf_transformation,[],[f180]) ).
fof(f10551,plain,
! [X0,X1,X2,X3,X4] :
( ~ flp(X0,X2)
| ~ attr(X2,X1)
| ~ loc(X3,X0)
| ~ scar(X3,X4)
| ~ sub(X1,name_1_1)
| ~ subs(X3,stehen_1_1)
| ~ val(X1,usa_0) ),
inference(ennf_transformation,[],[f10189]) ).
fof(f10554,plain,
! [X0,X1] :
( ~ fact(X0,X1)
| has_fact_leq(X0,X1) ),
inference(cnf_transformation,[],[f10350]) ).
fof(f10639,plain,
! [X0,X1] :
( ~ loc(X1,X0)
| ~ has_fact_leq(X1,real)
| loc(sK2(X0,X1),X0) ),
inference(cnf_transformation,[],[f10400]) ).
fof(f10804,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| val(sK48(X0,X2),X2) ),
inference(cnf_transformation,[],[f10509]) ).
fof(f10805,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| sub(sK48(X0,X2),name_1_1) ),
inference(cnf_transformation,[],[f10509]) ).
fof(f10807,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| loc(X0,sK49(X0,X2)) ),
inference(cnf_transformation,[],[f10509]) ).
fof(f10808,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| attr(sK47(X0,X2),sK48(X0,X2)) ),
inference(cnf_transformation,[],[f10509]) ).
fof(f10809,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| in(sK49(X0,X2),sK47(X0,X2)) ),
inference(cnf_transformation,[],[f10509]) ).
fof(f10868,plain,
! [X0,X1] :
( ~ in(X0,X1)
| flp(X0,X1) ),
inference(cnf_transformation,[],[f10543]) ).
fof(f10876,plain,
! [X0,X1] :
( subs(sK62(X0,X1),stehen_1_1)
| ~ loc(X0,X1) ),
inference(cnf_transformation,[],[f10548]) ).
fof(f10877,plain,
! [X0,X1] :
( scar(sK62(X0,X1),X0)
| ~ loc(X0,X1) ),
inference(cnf_transformation,[],[f10548]) ).
fof(f10878,plain,
! [X0,X1] :
( loc(sK62(X0,X1),X1)
| ~ loc(X0,X1) ),
inference(cnf_transformation,[],[f10548]) ).
fof(f19586,plain,
state_adjective_state_binding(amerikanisch__1_1,usa_0),
inference(cnf_transformation,[],[f9006]) ).
fof(f20768,plain,
! [X2,X3,X0,X1,X4] :
( ~ val(X1,usa_0)
| ~ subs(X3,stehen_1_1)
| ~ sub(X1,name_1_1)
| ~ scar(X3,X4)
| ~ loc(X3,X0)
| ~ attr(X2,X1)
| ~ flp(X0,X2) ),
inference(cnf_transformation,[],[f10551]) ).
fof(f20803,plain,
fact(c81355,real),
inference(cnf_transformation,[],[f10346]) ).
fof(f20850,plain,
prop(c81355,amerikanisch__1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20890,plain,
has_fact_leq(c81355,real),
inference(resolution,[],[f10554,f20803]) ).
fof(f21260,plain,
! [X0] :
( val(sK48(X0,usa_0),usa_0)
| ~ prop(X0,amerikanisch__1_1) ),
inference(resolution,[],[f10804,f19586]) ).
fof(f21263,plain,
! [X2,X3,X0,X1,X4] :
( ~ sub(sK48(X0,usa_0),name_1_1)
| ~ subs(X1,stehen_1_1)
| ~ prop(X0,amerikanisch__1_1)
| ~ scar(X1,X2)
| ~ loc(X1,X3)
| ~ attr(X4,sK48(X0,usa_0))
| ~ flp(X3,X4) ),
inference(resolution,[],[f21260,f20768]) ).
fof(f21264,plain,
! [X0] :
( ~ prop(X0,amerikanisch__1_1)
| sub(sK48(X0,usa_0),name_1_1) ),
inference(resolution,[],[f10805,f19586]) ).
fof(f21265,plain,
sub(sK48(c81355,usa_0),name_1_1),
inference(resolution,[],[f21264,f20850]) ).
fof(f21266,plain,
! [X2,X3,X0,X1] :
( ~ subs(X0,stehen_1_1)
| ~ prop(c81355,amerikanisch__1_1)
| ~ scar(X0,X1)
| ~ loc(X0,X2)
| ~ attr(X3,sK48(c81355,usa_0))
| ~ flp(X2,X3) ),
inference(resolution,[],[f21265,f21263]) ).
fof(f21268,plain,
! [X2,X3,X0,X1] :
( ~ attr(X3,sK48(c81355,usa_0))
| ~ scar(X0,X1)
| ~ loc(X0,X2)
| ~ subs(X0,stehen_1_1)
| ~ flp(X2,X3) ),
inference(forward_subsumption_resolution,[],[f21266,f20850]) ).
fof(f21273,plain,
! [X0] :
( ~ prop(X0,amerikanisch__1_1)
| loc(X0,sK49(X0,usa_0)) ),
inference(resolution,[],[f10807,f19586]) ).
fof(f21275,plain,
loc(c81355,sK49(c81355,usa_0)),
inference(resolution,[],[f21273,f20850]) ).
fof(f21276,plain,
( ~ has_fact_leq(c81355,real)
| loc(sK2(sK49(c81355,usa_0),c81355),sK49(c81355,usa_0)) ),
inference(resolution,[],[f21275,f10639]) ).
fof(f21281,plain,
loc(sK2(sK49(c81355,usa_0),c81355),sK49(c81355,usa_0)),
inference(forward_subsumption_resolution,[],[f21276,f20890]) ).
fof(f21327,plain,
! [X0] :
( attr(sK47(X0,usa_0),sK48(X0,usa_0))
| ~ prop(X0,amerikanisch__1_1) ),
inference(resolution,[],[f10808,f19586]) ).
fof(f21328,plain,
! [X2,X0,X1] :
( ~ prop(c81355,amerikanisch__1_1)
| ~ scar(X0,X1)
| ~ loc(X0,X2)
| ~ subs(X0,stehen_1_1)
| ~ flp(X2,sK47(c81355,usa_0)) ),
inference(resolution,[],[f21327,f21268]) ).
fof(f21329,plain,
! [X2,X0,X1] :
( ~ flp(X2,sK47(c81355,usa_0))
| ~ loc(X0,X2)
| ~ subs(X0,stehen_1_1)
| ~ scar(X0,X1) ),
inference(forward_subsumption_resolution,[],[f21328,f20850]) ).
fof(f21330,plain,
! [X0] :
( in(sK49(X0,usa_0),sK47(X0,usa_0))
| ~ prop(X0,amerikanisch__1_1) ),
inference(resolution,[],[f10809,f19586]) ).
fof(f21331,plain,
! [X0] :
( flp(sK49(X0,usa_0),sK47(X0,usa_0))
| ~ prop(X0,amerikanisch__1_1) ),
inference(resolution,[],[f21330,f10868]) ).
fof(f21333,plain,
! [X0,X1] :
( ~ prop(c81355,amerikanisch__1_1)
| ~ loc(X0,sK49(c81355,usa_0))
| ~ subs(X0,stehen_1_1)
| ~ scar(X0,X1) ),
inference(resolution,[],[f21331,f21329]) ).
fof(f21334,plain,
! [X0,X1] :
( ~ subs(X0,stehen_1_1)
| ~ loc(X0,sK49(c81355,usa_0))
| ~ scar(X0,X1) ),
inference(forward_subsumption_resolution,[],[f21333,f20850]) ).
fof(f21335,plain,
! [X2,X0,X1] :
( ~ loc(sK62(X0,X1),sK49(c81355,usa_0))
| ~ scar(sK62(X0,X1),X2)
| ~ loc(X0,X1) ),
inference(resolution,[],[f21334,f10876]) ).
fof(f21337,plain,
! [X0,X1] :
( ~ scar(sK62(X0,sK49(c81355,usa_0)),X1)
| ~ loc(X0,sK49(c81355,usa_0))
| ~ loc(X0,sK49(c81355,usa_0)) ),
inference(resolution,[],[f21335,f10878]) ).
fof(f21338,plain,
! [X0,X1] :
( ~ scar(sK62(X0,sK49(c81355,usa_0)),X1)
| ~ loc(X0,sK49(c81355,usa_0)) ),
inference(duplicate_literal_removal,[],[f21337]) ).
fof(f21339,plain,
! [X0] :
( ~ loc(X0,sK49(c81355,usa_0))
| ~ loc(X0,sK49(c81355,usa_0)) ),
inference(resolution,[],[f21338,f10877]) ).
fof(f21340,plain,
! [X0] : ~ loc(X0,sK49(c81355,usa_0)),
inference(duplicate_literal_removal,[],[f21339]) ).
fof(f21343,plain,
$false,
inference(resolution,[],[f21340,f21281]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR113+10 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n002.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 23:05:08 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.24 Running first-order model finding
% 0.08/0.24 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
% 2.40/0.87 % (868490)Will run a generic schedule for satisfiability detection.
% 2.40/0.87 % (868509)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4179341598:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 2.40/0.87 % (868506)% WARNING: option uhcvi not known.
% 2.40/0.87 % (868506)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1256748881:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 2.40/0.87 % (868508)dis+10_1_sil=32000:sp=arity:random_seed=325426377:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 2.40/0.87 % (868507)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1184646677:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 2.40/0.87 % (868505)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2910001503_2997 on theBenchmark for (2997ds/0Mi)
% 2.40/0.87 % (868510)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3831633494:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 2.40/0.87 % (868511)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=812066498:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 2.40/0.87 % (868509)Instruction limit reached!
% 2.40/0.87 % (868509)------------------------------
% 2.40/0.87 % (868509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.87 % (868509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.87 % (868509)CaDiCaL version: 2.1.3
% 2.40/0.87 % (868509)Termination reason: Instruction limit
% 2.40/0.87 % (868509)Termination phase: Blocked clause elimination
% 2.40/0.87 % (868509)Time elapsed: 0.062 s
% 2.40/0.87 % (868509)Peak memory usage: 28 MB
% 2.40/0.87 % (868509)Instructions burned: 117 (million)
% 2.40/0.87 % (868519)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4134780296:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 2.40/0.87 % (868508)Instruction limit reached!
% 2.40/0.87 % (868508)------------------------------
% 2.40/0.87 % (868508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.87 % (868508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.87 % (868508)CaDiCaL version: 2.1.3
% 2.40/0.87 % (868508)Termination reason: Instruction limit
% 2.40/0.87 % (868508)Termination phase: Saturation
% 2.40/0.87 % (868508)Time elapsed: 0.086 s
% 2.40/0.87 % (868508)Peak memory usage: 26 MB
% 2.40/0.87 % (868508)Instructions burned: 104 (million)
% 2.40/0.87 % (868521)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2006527704:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 2.40/0.87 % (868510)Instruction limit reached!
% 2.40/0.87 % (868510)------------------------------
% 2.40/0.87 % (868510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.87 % (868510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.87 % (868510)CaDiCaL version: 2.1.3
% 2.40/0.87 % (868510)Termination reason: Instruction limit
% 2.40/0.87 % (868510)Termination phase: Saturation
% 2.40/0.87 % (868510)Time elapsed: 0.124 s
% 2.40/0.87 % (868510)Peak memory usage: 28 MB
% 2.40/0.87 % (868510)Instructions burned: 131 (million)
% 2.40/0.87 % (868511)Instruction limit reached!
% 2.40/0.87 % (868511)------------------------------
% 2.40/0.87 % (868511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.87 % (868511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.87 % (868511)CaDiCaL version: 2.1.3
% 2.40/0.87 % (868511)Termination reason: Instruction limit
% 2.40/0.87 % (868511)Termination phase: Saturation
% 2.40/0.87 % (868511)Time elapsed: 0.148 s
% 2.40/0.87 % (868511)Peak memory usage: 29 MB
% 2.40/0.87 % (868511)Instructions burned: 162 (million)
% 2.40/0.87 % (868524)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=803221311:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 2.40/0.87 % (868525)ott-21_1_sil=16000:fs=off:random_seed=2926708413:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 2.40/0.87 % TRYING [1]
% 2.40/0.87 % (868521)Instruction limit reached!
% 2.40/0.87 % (868521)------------------------------
% 2.40/0.87 % (868521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.87 % (868521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.87 % (868521)CaDiCaL version: 2.1.3
% 2.40/0.87 % (868521)Termination reason: Instruction limit
% 2.40/0.87 % (868521)Termination phase: Blocked clause elimination
% 2.40/0.87 % (868521)Time elapsed: 0.134 s
% 2.40/0.87 % (868521)Peak memory usage: 29 MB
% 2.40/0.87 % (868521)Instructions burned: 131 (million)
% 2.40/0.87 % TRYING [2]
% 2.40/0.87 % (868531)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2366400459:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi)
% 2.40/0.87 % (868525)Instruction limit reached!
% 2.40/0.87 % (868525)------------------------------
% 2.40/0.87 % (868525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.87 % (868525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.87 % (868525)CaDiCaL version: 2.1.3
% 2.40/0.87 % (868525)Termination reason: Instruction limit
% 2.40/0.87 % (868525)Termination phase: Saturation
% 2.40/0.87 % (868525)Time elapsed: 0.135 s
% 2.40/0.87 % (868525)Peak memory usage: 28 MB
% 2.40/0.87 % (868525)Instructions burned: 180 (million)
% 2.40/0.87 % (868524) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-868490-868524"...
% 2.40/0.87 % (868534)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2830290603:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi)
% 2.40/0.87 % (868524)...printing done.
% 2.40/0.87 % (868524)Refutation found. Thanks to Tanya!
% 2.40/0.87 % SZS status Theorem for theBenchmark
% 2.40/0.87 % SZS output start Proof for theBenchmark
% See solution above
% 2.40/0.90 % (868524)------------------------------
% 2.40/0.90 % (868524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.90 % (868524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.90 % (868524)CaDiCaL version: 2.1.3
% 2.40/0.90 % (868524)Termination reason: Refutation
% 2.40/0.90 % (868524)Time elapsed: 0.191 s
% 2.40/0.90 % (868524)Peak memory usage: 30 MB
% 2.40/0.90 % (868524)Instructions burned: 202 (million)
% 2.40/0.90 % (868490)Success in time 0.622 s
% 2.40/0.90 % Vampire exiting
%------------------------------------------------------------------------------