%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR112+1 : 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 : n004.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 7.44s 1.63s
% Output : Refutation 7.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 14
% Syntax : Number of formulae : 103 ( 34 unt; 9 def)
% Number of atoms : 1130 ( 0 equ)
% Maximal formula atoms : 166 ( 10 avg)
% Number of connectives : 1145 ( 118 ~; 123 |; 893 &)
% ( 9 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 166 ( 13 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 27 ( 26 usr; 10 prp; 0-9 aty)
% Number of functors : 51 ( 51 usr; 49 con; 0-2 aty)
% Number of variables : 126 ( 0 sgn 107 !; 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(f159,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] :
( arg1(X3,X2)
& arg2(X3,X2)
& subs(X3,hei__337en_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',attr_name_hei__337en_1_1) ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7] :
( arg1(X4,X5)
& arg2(X4,X0)
& attr(X7,X6)
& pred(X2,linie_1_1)
& pred(X3,u1_1_1)
& sub(X1,bahn_1_1)
& sub(X6,name_1_1)
& subs(X4,hei__337en_1_1)
& val(X6,u2_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',synth_qa07_001_qapn_4) ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7] :
( arg1(X4,X5)
& arg2(X4,X0)
& attr(X7,X6)
& pred(X2,linie_1_1)
& pred(X3,u1_1_1)
& sub(X1,bahn_1_1)
& sub(X6,name_1_1)
& subs(X4,hei__337en_1_1)
& val(X6,u2_0) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,axiom,
( sub(c5909,bahn_1_1)
& pred(c5910,linie_1_1)
& pred(c5912,u1_1_1)
& attr(c5919,c5920)
& sub(c5919,einrichtung_1_2)
& sub(c5920,name_1_1)
& val(c5920,u2_0)
& pred(c5921,u3_1_1)
& sub(c5932,abstand_1_1)
& pred(c5937,minute_1_1)
& tupl_p9(c6138,c5901,c5909,c5910,c5912,c5919,c5921,c5932,c5937)
& sort(c5909,io)
& card(c5909,int1)
& etype(c5909,int0)
& fact(c5909,real)
& gener(c5909,gener_c)
& quant(c5909,one)
& refer(c5909,refer_c)
& varia(c5909,varia_c)
& sort(bahn_1_1,io)
& card(bahn_1_1,int1)
& etype(bahn_1_1,int0)
& fact(bahn_1_1,real)
& gener(bahn_1_1,ge)
& quant(bahn_1_1,one)
& refer(bahn_1_1,refer_c)
& varia(bahn_1_1,varia_c)
& sort(c5910,d)
& sort(c5910,io)
& card(c5910,cons(x_constant,cons(int1,nil)))
& etype(c5910,int1)
& fact(c5910,real)
& gener(c5910,gener_c)
& quant(c5910,mult)
& refer(c5910,indet)
& varia(c5910,varia_c)
& sort(linie_1_1,d)
& sort(linie_1_1,io)
& card(linie_1_1,int1)
& etype(linie_1_1,int0)
& fact(linie_1_1,real)
& gener(linie_1_1,ge)
& quant(linie_1_1,one)
& refer(linie_1_1,refer_c)
& varia(linie_1_1,varia_c)
& sort(c5912,o)
& card(c5912,cons(x_constant,cons(int1,nil)))
& etype(c5912,int1)
& fact(c5912,real)
& gener(c5912,gener_c)
& quant(c5912,mult)
& refer(c5912,indet)
& varia(c5912,varia_c)
& sort(u1_1_1,o)
& card(u1_1_1,int1)
& etype(u1_1_1,int0)
& fact(u1_1_1,real)
& gener(u1_1_1,ge)
& quant(u1_1_1,one)
& refer(u1_1_1,refer_c)
& varia(u1_1_1,varia_c)
& sort(c5919,d)
& sort(c5919,io)
& card(c5919,int1)
& etype(c5919,int1)
& fact(c5919,real)
& gener(c5919,sp)
& quant(c5919,one)
& refer(c5919,det)
& varia(c5919,con)
& sort(c5920,na)
& card(c5920,int1)
& etype(c5920,int0)
& fact(c5920,real)
& gener(c5920,sp)
& quant(c5920,one)
& refer(c5920,indet)
& varia(c5920,varia_c)
& sort(einrichtung_1_2,d)
& sort(einrichtung_1_2,io)
& card(einrichtung_1_2,card_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& quant(einrichtung_1_2,quant_c)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,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(u2_0,fe)
& sort(c5921,o)
& card(c5921,cons(x_constant,cons(int1,nil)))
& etype(c5921,int1)
& fact(c5921,real)
& gener(c5921,gener_c)
& quant(c5921,mult)
& refer(c5921,indet)
& varia(c5921,varia_c)
& sort(u3_1_1,o)
& card(u3_1_1,int1)
& etype(u3_1_1,int0)
& fact(u3_1_1,real)
& gener(u3_1_1,ge)
& quant(u3_1_1,one)
& refer(u3_1_1,refer_c)
& varia(u3_1_1,varia_c)
& sort(c5932,io)
& sort(c5932,na)
& card(c5932,int1)
& etype(c5932,int0)
& fact(c5932,real)
& gener(c5932,sp)
& quant(c5932,one)
& refer(c5932,det)
& varia(c5932,con)
& sort(abstand_1_1,io)
& sort(abstand_1_1,na)
& card(abstand_1_1,int1)
& etype(abstand_1_1,int0)
& fact(abstand_1_1,real)
& gener(abstand_1_1,ge)
& quant(abstand_1_1,one)
& refer(abstand_1_1,refer_c)
& varia(abstand_1_1,varia_c)
& sort(c5937,me)
& sort(c5937,oa)
& sort(c5937,ta)
& card(c5937,card_c)
& etype(c5937,etype_c)
& fact(c5937,real)
& gener(c5937,gener_c)
& quant(c5937,quant_c)
& refer(c5937,refer_c)
& varia(c5937,varia_c)
& sort(minute_1_1,me)
& sort(minute_1_1,oa)
& sort(minute_1_1,ta)
& card(minute_1_1,card_c)
& etype(minute_1_1,etype_c)
& fact(minute_1_1,real)
& gener(minute_1_1,ge)
& quant(minute_1_1,quant_c)
& refer(minute_1_1,refer_c)
& varia(minute_1_1,varia_c)
& sort(c6138,ent)
& card(c6138,card_c)
& etype(c6138,etype_c)
& fact(c6138,real)
& gener(c6138,gener_c)
& quant(c6138,quant_c)
& refer(c6138,refer_c)
& varia(c6138,varia_c)
& sort(c5901,o)
& card(c5901,int1)
& etype(c5901,int0)
& fact(c5901,real)
& gener(c5901,sp)
& quant(c5901,one)
& refer(c5901,det)
& varia(c5901,varia_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_001_qapn_4) ).
fof(f10191,plain,
( sub(c5909,bahn_1_1)
& pred(c5910,linie_1_1)
& pred(c5912,u1_1_1)
& attr(c5919,c5920)
& sub(c5919,einrichtung_1_2)
& sub(c5920,name_1_1)
& val(c5920,u2_0)
& pred(c5921,u3_1_1)
& sub(c5932,abstand_1_1)
& pred(c5937,minute_1_1)
& sort(c5909,io)
& card(c5909,int1)
& etype(c5909,int0)
& fact(c5909,real)
& gener(c5909,gener_c)
& quant(c5909,one)
& refer(c5909,refer_c)
& varia(c5909,varia_c)
& sort(bahn_1_1,io)
& card(bahn_1_1,int1)
& etype(bahn_1_1,int0)
& fact(bahn_1_1,real)
& gener(bahn_1_1,ge)
& quant(bahn_1_1,one)
& refer(bahn_1_1,refer_c)
& varia(bahn_1_1,varia_c)
& sort(c5910,d)
& sort(c5910,io)
& card(c5910,cons(x_constant,cons(int1,nil)))
& etype(c5910,int1)
& fact(c5910,real)
& gener(c5910,gener_c)
& quant(c5910,mult)
& refer(c5910,indet)
& varia(c5910,varia_c)
& sort(linie_1_1,d)
& sort(linie_1_1,io)
& card(linie_1_1,int1)
& etype(linie_1_1,int0)
& fact(linie_1_1,real)
& gener(linie_1_1,ge)
& quant(linie_1_1,one)
& refer(linie_1_1,refer_c)
& varia(linie_1_1,varia_c)
& sort(c5912,o)
& card(c5912,cons(x_constant,cons(int1,nil)))
& etype(c5912,int1)
& fact(c5912,real)
& gener(c5912,gener_c)
& quant(c5912,mult)
& refer(c5912,indet)
& varia(c5912,varia_c)
& sort(u1_1_1,o)
& card(u1_1_1,int1)
& etype(u1_1_1,int0)
& fact(u1_1_1,real)
& gener(u1_1_1,ge)
& quant(u1_1_1,one)
& refer(u1_1_1,refer_c)
& varia(u1_1_1,varia_c)
& sort(c5919,d)
& sort(c5919,io)
& card(c5919,int1)
& etype(c5919,int1)
& fact(c5919,real)
& gener(c5919,sp)
& quant(c5919,one)
& refer(c5919,det)
& varia(c5919,con)
& sort(c5920,na)
& card(c5920,int1)
& etype(c5920,int0)
& fact(c5920,real)
& gener(c5920,sp)
& quant(c5920,one)
& refer(c5920,indet)
& varia(c5920,varia_c)
& sort(einrichtung_1_2,d)
& sort(einrichtung_1_2,io)
& card(einrichtung_1_2,card_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& quant(einrichtung_1_2,quant_c)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,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(u2_0,fe)
& sort(c5921,o)
& card(c5921,cons(x_constant,cons(int1,nil)))
& etype(c5921,int1)
& fact(c5921,real)
& gener(c5921,gener_c)
& quant(c5921,mult)
& refer(c5921,indet)
& varia(c5921,varia_c)
& sort(u3_1_1,o)
& card(u3_1_1,int1)
& etype(u3_1_1,int0)
& fact(u3_1_1,real)
& gener(u3_1_1,ge)
& quant(u3_1_1,one)
& refer(u3_1_1,refer_c)
& varia(u3_1_1,varia_c)
& sort(c5932,io)
& sort(c5932,na)
& card(c5932,int1)
& etype(c5932,int0)
& fact(c5932,real)
& gener(c5932,sp)
& quant(c5932,one)
& refer(c5932,det)
& varia(c5932,con)
& sort(abstand_1_1,io)
& sort(abstand_1_1,na)
& card(abstand_1_1,int1)
& etype(abstand_1_1,int0)
& fact(abstand_1_1,real)
& gener(abstand_1_1,ge)
& quant(abstand_1_1,one)
& refer(abstand_1_1,refer_c)
& varia(abstand_1_1,varia_c)
& sort(c5937,me)
& sort(c5937,oa)
& sort(c5937,ta)
& card(c5937,card_c)
& etype(c5937,etype_c)
& fact(c5937,real)
& gener(c5937,gener_c)
& quant(c5937,quant_c)
& refer(c5937,refer_c)
& varia(c5937,varia_c)
& sort(minute_1_1,me)
& sort(minute_1_1,oa)
& sort(minute_1_1,ta)
& card(minute_1_1,card_c)
& etype(minute_1_1,etype_c)
& fact(minute_1_1,real)
& gener(minute_1_1,ge)
& quant(minute_1_1,quant_c)
& refer(minute_1_1,refer_c)
& varia(minute_1_1,varia_c)
& sort(c6138,ent)
& card(c6138,card_c)
& etype(c6138,etype_c)
& fact(c6138,real)
& gener(c6138,gener_c)
& quant(c6138,quant_c)
& refer(c6138,refer_c)
& varia(c6138,varia_c)
& sort(c5901,o)
& card(c5901,int1)
& etype(c5901,int0)
& fact(c5901,real)
& gener(c5901,sp)
& quant(c5901,one)
& refer(c5901,det)
& varia(c5901,varia_c) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10327,plain,
( sub(c5909,bahn_1_1)
& pred(c5910,linie_1_1)
& pred(c5912,u1_1_1)
& attr(c5919,c5920)
& sub(c5919,einrichtung_1_2)
& sub(c5920,name_1_1)
& val(c5920,u2_0)
& pred(c5921,u3_1_1)
& sub(c5932,abstand_1_1)
& pred(c5937,minute_1_1)
& card(c5909,int1)
& etype(c5909,int0)
& fact(c5909,real)
& gener(c5909,gener_c)
& quant(c5909,one)
& refer(c5909,refer_c)
& varia(c5909,varia_c)
& card(bahn_1_1,int1)
& etype(bahn_1_1,int0)
& fact(bahn_1_1,real)
& gener(bahn_1_1,ge)
& quant(bahn_1_1,one)
& refer(bahn_1_1,refer_c)
& varia(bahn_1_1,varia_c)
& card(c5910,cons(x_constant,cons(int1,nil)))
& etype(c5910,int1)
& fact(c5910,real)
& gener(c5910,gener_c)
& quant(c5910,mult)
& refer(c5910,indet)
& varia(c5910,varia_c)
& card(linie_1_1,int1)
& etype(linie_1_1,int0)
& fact(linie_1_1,real)
& gener(linie_1_1,ge)
& quant(linie_1_1,one)
& refer(linie_1_1,refer_c)
& varia(linie_1_1,varia_c)
& card(c5912,cons(x_constant,cons(int1,nil)))
& etype(c5912,int1)
& fact(c5912,real)
& gener(c5912,gener_c)
& quant(c5912,mult)
& refer(c5912,indet)
& varia(c5912,varia_c)
& card(u1_1_1,int1)
& etype(u1_1_1,int0)
& fact(u1_1_1,real)
& gener(u1_1_1,ge)
& quant(u1_1_1,one)
& refer(u1_1_1,refer_c)
& varia(u1_1_1,varia_c)
& card(c5919,int1)
& etype(c5919,int1)
& fact(c5919,real)
& gener(c5919,sp)
& quant(c5919,one)
& refer(c5919,det)
& varia(c5919,con)
& card(c5920,int1)
& etype(c5920,int0)
& fact(c5920,real)
& gener(c5920,sp)
& quant(c5920,one)
& refer(c5920,indet)
& varia(c5920,varia_c)
& card(einrichtung_1_2,card_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& quant(einrichtung_1_2,quant_c)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,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(c5921,cons(x_constant,cons(int1,nil)))
& etype(c5921,int1)
& fact(c5921,real)
& gener(c5921,gener_c)
& quant(c5921,mult)
& refer(c5921,indet)
& varia(c5921,varia_c)
& card(u3_1_1,int1)
& etype(u3_1_1,int0)
& fact(u3_1_1,real)
& gener(u3_1_1,ge)
& quant(u3_1_1,one)
& refer(u3_1_1,refer_c)
& varia(u3_1_1,varia_c)
& card(c5932,int1)
& etype(c5932,int0)
& fact(c5932,real)
& gener(c5932,sp)
& quant(c5932,one)
& refer(c5932,det)
& varia(c5932,con)
& card(abstand_1_1,int1)
& etype(abstand_1_1,int0)
& fact(abstand_1_1,real)
& gener(abstand_1_1,ge)
& quant(abstand_1_1,one)
& refer(abstand_1_1,refer_c)
& varia(abstand_1_1,varia_c)
& card(c5937,card_c)
& etype(c5937,etype_c)
& fact(c5937,real)
& gener(c5937,gener_c)
& quant(c5937,quant_c)
& refer(c5937,refer_c)
& varia(c5937,varia_c)
& card(minute_1_1,card_c)
& etype(minute_1_1,etype_c)
& fact(minute_1_1,real)
& gener(minute_1_1,ge)
& quant(minute_1_1,quant_c)
& refer(minute_1_1,refer_c)
& varia(minute_1_1,varia_c)
& card(c6138,card_c)
& etype(c6138,etype_c)
& fact(c6138,real)
& gener(c6138,gener_c)
& quant(c6138,quant_c)
& refer(c6138,refer_c)
& varia(c6138,varia_c)
& card(c5901,int1)
& etype(c5901,int0)
& fact(c5901,real)
& gener(c5901,sp)
& quant(c5901,one)
& refer(c5901,det)
& varia(c5901,varia_c) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10330,plain,
( sub(c5909,bahn_1_1)
& pred(c5910,linie_1_1)
& pred(c5912,u1_1_1)
& attr(c5919,c5920)
& sub(c5919,einrichtung_1_2)
& sub(c5920,name_1_1)
& val(c5920,u2_0)
& pred(c5921,u3_1_1)
& sub(c5932,abstand_1_1)
& pred(c5937,minute_1_1)
& card(c5909,int1)
& etype(c5909,int0)
& fact(c5909,real)
& gener(c5909,gener_c)
& refer(c5909,refer_c)
& varia(c5909,varia_c)
& card(bahn_1_1,int1)
& etype(bahn_1_1,int0)
& fact(bahn_1_1,real)
& gener(bahn_1_1,ge)
& refer(bahn_1_1,refer_c)
& varia(bahn_1_1,varia_c)
& card(c5910,cons(x_constant,cons(int1,nil)))
& etype(c5910,int1)
& fact(c5910,real)
& gener(c5910,gener_c)
& refer(c5910,indet)
& varia(c5910,varia_c)
& card(linie_1_1,int1)
& etype(linie_1_1,int0)
& fact(linie_1_1,real)
& gener(linie_1_1,ge)
& refer(linie_1_1,refer_c)
& varia(linie_1_1,varia_c)
& card(c5912,cons(x_constant,cons(int1,nil)))
& etype(c5912,int1)
& fact(c5912,real)
& gener(c5912,gener_c)
& refer(c5912,indet)
& varia(c5912,varia_c)
& card(u1_1_1,int1)
& etype(u1_1_1,int0)
& fact(u1_1_1,real)
& gener(u1_1_1,ge)
& refer(u1_1_1,refer_c)
& varia(u1_1_1,varia_c)
& card(c5919,int1)
& etype(c5919,int1)
& fact(c5919,real)
& gener(c5919,sp)
& refer(c5919,det)
& varia(c5919,con)
& card(c5920,int1)
& etype(c5920,int0)
& fact(c5920,real)
& gener(c5920,sp)
& refer(c5920,indet)
& varia(c5920,varia_c)
& card(einrichtung_1_2,card_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,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(c5921,cons(x_constant,cons(int1,nil)))
& etype(c5921,int1)
& fact(c5921,real)
& gener(c5921,gener_c)
& refer(c5921,indet)
& varia(c5921,varia_c)
& card(u3_1_1,int1)
& etype(u3_1_1,int0)
& fact(u3_1_1,real)
& gener(u3_1_1,ge)
& refer(u3_1_1,refer_c)
& varia(u3_1_1,varia_c)
& card(c5932,int1)
& etype(c5932,int0)
& fact(c5932,real)
& gener(c5932,sp)
& refer(c5932,det)
& varia(c5932,con)
& card(abstand_1_1,int1)
& etype(abstand_1_1,int0)
& fact(abstand_1_1,real)
& gener(abstand_1_1,ge)
& refer(abstand_1_1,refer_c)
& varia(abstand_1_1,varia_c)
& card(c5937,card_c)
& etype(c5937,etype_c)
& fact(c5937,real)
& gener(c5937,gener_c)
& refer(c5937,refer_c)
& varia(c5937,varia_c)
& card(minute_1_1,card_c)
& etype(minute_1_1,etype_c)
& fact(minute_1_1,real)
& gener(minute_1_1,ge)
& refer(minute_1_1,refer_c)
& varia(minute_1_1,varia_c)
& card(c6138,card_c)
& etype(c6138,etype_c)
& fact(c6138,real)
& gener(c6138,gener_c)
& refer(c6138,refer_c)
& varia(c6138,varia_c)
& card(c5901,int1)
& etype(c5901,int0)
& fact(c5901,real)
& gener(c5901,sp)
& refer(c5901,det)
& varia(c5901,varia_c) ),
inference(pure_predicate_removal,[],[f10327]) ).
fof(f10333,plain,
( sub(c5909,bahn_1_1)
& pred(c5910,linie_1_1)
& pred(c5912,u1_1_1)
& attr(c5919,c5920)
& sub(c5919,einrichtung_1_2)
& sub(c5920,name_1_1)
& val(c5920,u2_0)
& pred(c5921,u3_1_1)
& sub(c5932,abstand_1_1)
& pred(c5937,minute_1_1)
& etype(c5909,int0)
& fact(c5909,real)
& gener(c5909,gener_c)
& refer(c5909,refer_c)
& varia(c5909,varia_c)
& etype(bahn_1_1,int0)
& fact(bahn_1_1,real)
& gener(bahn_1_1,ge)
& refer(bahn_1_1,refer_c)
& varia(bahn_1_1,varia_c)
& etype(c5910,int1)
& fact(c5910,real)
& gener(c5910,gener_c)
& refer(c5910,indet)
& varia(c5910,varia_c)
& etype(linie_1_1,int0)
& fact(linie_1_1,real)
& gener(linie_1_1,ge)
& refer(linie_1_1,refer_c)
& varia(linie_1_1,varia_c)
& etype(c5912,int1)
& fact(c5912,real)
& gener(c5912,gener_c)
& refer(c5912,indet)
& varia(c5912,varia_c)
& etype(u1_1_1,int0)
& fact(u1_1_1,real)
& gener(u1_1_1,ge)
& refer(u1_1_1,refer_c)
& varia(u1_1_1,varia_c)
& etype(c5919,int1)
& fact(c5919,real)
& gener(c5919,sp)
& refer(c5919,det)
& varia(c5919,con)
& etype(c5920,int0)
& fact(c5920,real)
& gener(c5920,sp)
& refer(c5920,indet)
& varia(c5920,varia_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,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(c5921,int1)
& fact(c5921,real)
& gener(c5921,gener_c)
& refer(c5921,indet)
& varia(c5921,varia_c)
& etype(u3_1_1,int0)
& fact(u3_1_1,real)
& gener(u3_1_1,ge)
& refer(u3_1_1,refer_c)
& varia(u3_1_1,varia_c)
& etype(c5932,int0)
& fact(c5932,real)
& gener(c5932,sp)
& refer(c5932,det)
& varia(c5932,con)
& etype(abstand_1_1,int0)
& fact(abstand_1_1,real)
& gener(abstand_1_1,ge)
& refer(abstand_1_1,refer_c)
& varia(abstand_1_1,varia_c)
& etype(c5937,etype_c)
& fact(c5937,real)
& gener(c5937,gener_c)
& refer(c5937,refer_c)
& varia(c5937,varia_c)
& etype(minute_1_1,etype_c)
& fact(minute_1_1,real)
& gener(minute_1_1,ge)
& refer(minute_1_1,refer_c)
& varia(minute_1_1,varia_c)
& etype(c6138,etype_c)
& fact(c6138,real)
& gener(c6138,gener_c)
& refer(c6138,refer_c)
& varia(c6138,varia_c)
& etype(c5901,int0)
& fact(c5901,real)
& gener(c5901,sp)
& refer(c5901,det)
& varia(c5901,varia_c) ),
inference(pure_predicate_removal,[],[f10330]) ).
fof(f10336,plain,
( sub(c5909,bahn_1_1)
& pred(c5910,linie_1_1)
& pred(c5912,u1_1_1)
& attr(c5919,c5920)
& sub(c5919,einrichtung_1_2)
& sub(c5920,name_1_1)
& val(c5920,u2_0)
& pred(c5921,u3_1_1)
& sub(c5932,abstand_1_1)
& pred(c5937,minute_1_1)
& etype(c5909,int0)
& fact(c5909,real)
& gener(c5909,gener_c)
& varia(c5909,varia_c)
& etype(bahn_1_1,int0)
& fact(bahn_1_1,real)
& gener(bahn_1_1,ge)
& varia(bahn_1_1,varia_c)
& etype(c5910,int1)
& fact(c5910,real)
& gener(c5910,gener_c)
& varia(c5910,varia_c)
& etype(linie_1_1,int0)
& fact(linie_1_1,real)
& gener(linie_1_1,ge)
& varia(linie_1_1,varia_c)
& etype(c5912,int1)
& fact(c5912,real)
& gener(c5912,gener_c)
& varia(c5912,varia_c)
& etype(u1_1_1,int0)
& fact(u1_1_1,real)
& gener(u1_1_1,ge)
& varia(u1_1_1,varia_c)
& etype(c5919,int1)
& fact(c5919,real)
& gener(c5919,sp)
& varia(c5919,con)
& etype(c5920,int0)
& fact(c5920,real)
& gener(c5920,sp)
& varia(c5920,varia_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& varia(einrichtung_1_2,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& varia(name_1_1,varia_c)
& etype(c5921,int1)
& fact(c5921,real)
& gener(c5921,gener_c)
& varia(c5921,varia_c)
& etype(u3_1_1,int0)
& fact(u3_1_1,real)
& gener(u3_1_1,ge)
& varia(u3_1_1,varia_c)
& etype(c5932,int0)
& fact(c5932,real)
& gener(c5932,sp)
& varia(c5932,con)
& etype(abstand_1_1,int0)
& fact(abstand_1_1,real)
& gener(abstand_1_1,ge)
& varia(abstand_1_1,varia_c)
& etype(c5937,etype_c)
& fact(c5937,real)
& gener(c5937,gener_c)
& varia(c5937,varia_c)
& etype(minute_1_1,etype_c)
& fact(minute_1_1,real)
& gener(minute_1_1,ge)
& varia(minute_1_1,varia_c)
& etype(c6138,etype_c)
& fact(c6138,real)
& gener(c6138,gener_c)
& varia(c6138,varia_c)
& etype(c5901,int0)
& fact(c5901,real)
& gener(c5901,sp)
& varia(c5901,varia_c) ),
inference(pure_predicate_removal,[],[f10333]) ).
fof(f10341,plain,
( sub(c5909,bahn_1_1)
& pred(c5910,linie_1_1)
& pred(c5912,u1_1_1)
& attr(c5919,c5920)
& sub(c5919,einrichtung_1_2)
& sub(c5920,name_1_1)
& val(c5920,u2_0)
& pred(c5921,u3_1_1)
& sub(c5932,abstand_1_1)
& pred(c5937,minute_1_1)
& etype(c5909,int0)
& fact(c5909,real)
& gener(c5909,gener_c)
& etype(bahn_1_1,int0)
& fact(bahn_1_1,real)
& gener(bahn_1_1,ge)
& etype(c5910,int1)
& fact(c5910,real)
& gener(c5910,gener_c)
& etype(linie_1_1,int0)
& fact(linie_1_1,real)
& gener(linie_1_1,ge)
& etype(c5912,int1)
& fact(c5912,real)
& gener(c5912,gener_c)
& etype(u1_1_1,int0)
& fact(u1_1_1,real)
& gener(u1_1_1,ge)
& etype(c5919,int1)
& fact(c5919,real)
& gener(c5919,sp)
& etype(c5920,int0)
& fact(c5920,real)
& gener(c5920,sp)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& etype(c5921,int1)
& fact(c5921,real)
& gener(c5921,gener_c)
& etype(u3_1_1,int0)
& fact(u3_1_1,real)
& gener(u3_1_1,ge)
& etype(c5932,int0)
& fact(c5932,real)
& gener(c5932,sp)
& etype(abstand_1_1,int0)
& fact(abstand_1_1,real)
& gener(abstand_1_1,ge)
& etype(c5937,etype_c)
& fact(c5937,real)
& gener(c5937,gener_c)
& etype(minute_1_1,etype_c)
& fact(minute_1_1,real)
& gener(minute_1_1,ge)
& etype(c6138,etype_c)
& fact(c6138,real)
& gener(c6138,gener_c)
& etype(c5901,int0)
& fact(c5901,real)
& gener(c5901,sp) ),
inference(pure_predicate_removal,[],[f10336]) ).
fof(f10346,plain,
( sub(c5909,bahn_1_1)
& pred(c5910,linie_1_1)
& pred(c5912,u1_1_1)
& attr(c5919,c5920)
& sub(c5919,einrichtung_1_2)
& sub(c5920,name_1_1)
& val(c5920,u2_0)
& pred(c5921,u3_1_1)
& sub(c5932,abstand_1_1)
& pred(c5937,minute_1_1)
& etype(c5909,int0)
& fact(c5909,real)
& etype(bahn_1_1,int0)
& fact(bahn_1_1,real)
& etype(c5910,int1)
& fact(c5910,real)
& etype(linie_1_1,int0)
& fact(linie_1_1,real)
& etype(c5912,int1)
& fact(c5912,real)
& etype(u1_1_1,int0)
& fact(u1_1_1,real)
& etype(c5919,int1)
& fact(c5919,real)
& etype(c5920,int0)
& fact(c5920,real)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& etype(c5921,int1)
& fact(c5921,real)
& etype(u3_1_1,int0)
& fact(u3_1_1,real)
& etype(c5932,int0)
& fact(c5932,real)
& etype(abstand_1_1,int0)
& fact(abstand_1_1,real)
& etype(c5937,etype_c)
& fact(c5937,real)
& etype(minute_1_1,etype_c)
& fact(minute_1_1,real)
& etype(c6138,etype_c)
& fact(c6138,real)
& etype(c5901,int0)
& fact(c5901,real) ),
inference(pure_predicate_removal,[],[f10341]) ).
fof(f10349,plain,
! [X0,X1,X2] :
( member(X0,cons(X1,X2))
| ~ member(X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f10514,plain,
! [X0,X1,X2] :
( ? [X3] :
( arg1(X3,X2)
& arg2(X3,X2)
& subs(X3,hei__337en_1_1) )
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(ennf_transformation,[],[f159]) ).
fof(f10515,plain,
! [X0,X1,X2] :
( ? [X3] :
( arg1(X3,X2)
& arg2(X3,X2)
& subs(X3,hei__337en_1_1) )
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(flattening,[],[f10514]) ).
fof(f10551,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ arg1(X4,X5)
| ~ arg2(X4,X0)
| ~ attr(X7,X6)
| ~ pred(X2,linie_1_1)
| ~ pred(X3,u1_1_1)
| ~ sub(X1,bahn_1_1)
| ~ sub(X6,name_1_1)
| ~ subs(X4,hei__337en_1_1)
| ~ val(X6,u2_0) ),
inference(ennf_transformation,[],[f10189]) ).
fof(f10552,plain,
! [X0,X1] : member(X0,cons(X0,X1)),
inference(cnf_transformation,[],[f1]) ).
fof(f10553,plain,
! [X2,X0,X1] :
( member(X0,cons(X1,X2))
| ~ member(X0,X2) ),
inference(cnf_transformation,[],[f10349]) ).
fof(f10812,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)
| subs(sK50(X2),hei__337en_1_1) ),
inference(cnf_transformation,[],[f10515]) ).
fof(f10813,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)
| arg2(sK50(X2),X2) ),
inference(cnf_transformation,[],[f10515]) ).
fof(f10814,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)
| arg1(sK50(X2),X2) ),
inference(cnf_transformation,[],[f10515]) ).
fof(f20768,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ val(X6,u2_0)
| ~ subs(X4,hei__337en_1_1)
| ~ sub(X6,name_1_1)
| ~ sub(X1,bahn_1_1)
| ~ pred(X3,u1_1_1)
| ~ pred(X2,linie_1_1)
| ~ attr(X7,X6)
| ~ arg2(X4,X0)
| ~ arg1(X4,X5) ),
inference(cnf_transformation,[],[f10551]) ).
fof(f20808,plain,
val(c5920,u2_0),
inference(cnf_transformation,[],[f10346]) ).
fof(f20809,plain,
sub(c5920,name_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20811,plain,
attr(c5919,c5920),
inference(cnf_transformation,[],[f10346]) ).
fof(f20812,plain,
pred(c5912,u1_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20813,plain,
pred(c5910,linie_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20814,plain,
sub(c5909,bahn_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f21033,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| sub(X0,X1)
| ~ attr(X2,X0)
| arg1(sK50(X2),X2) ),
inference(consistent_polarity_flipping,[],[f10814]) ).
fof(f21034,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| sub(X0,X1)
| ~ attr(X2,X0)
| arg2(sK50(X2),X2) ),
inference(consistent_polarity_flipping,[],[f10813]) ).
fof(f21035,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| sub(X0,X1)
| ~ attr(X2,X0)
| subs(sK50(X2),hei__337en_1_1) ),
inference(consistent_polarity_flipping,[],[f10812]) ).
fof(f22273,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( val(X6,u2_0)
| ~ subs(X4,hei__337en_1_1)
| sub(X6,name_1_1)
| sub(X1,bahn_1_1)
| pred(X3,u1_1_1)
| pred(X2,linie_1_1)
| ~ attr(X7,X6)
| ~ arg2(X4,X0)
| ~ arg1(X4,X5) ),
inference(consistent_polarity_flipping,[],[f20768]) ).
fof(f22274,plain,
~ sub(c5909,bahn_1_1),
inference(consistent_polarity_flipping,[],[f20814]) ).
fof(f22275,plain,
~ pred(c5910,linie_1_1),
inference(consistent_polarity_flipping,[],[f20813]) ).
fof(f22276,plain,
~ pred(c5912,u1_1_1),
inference(consistent_polarity_flipping,[],[f20812]) ).
fof(f22278,plain,
~ sub(c5920,name_1_1),
inference(consistent_polarity_flipping,[],[f20809]) ).
fof(f22279,plain,
~ val(c5920,u2_0),
inference(consistent_polarity_flipping,[],[f20808]) ).
fof(f22284,definition,
( spl63_1
<=> ! [X2] : pred(X2,linie_1_1) ),
introduced(definition,[new_symbols(definition,[spl63_1])],[avatar_definition]) ).
fof(f22285,plain,
( ! [X2] : pred(X2,linie_1_1)
| ~ spl63_1 ),
inference(avatar_component_clause,[],[f22284]) ).
fof(f22287,definition,
( spl63_2
<=> ! [X3] : pred(X3,u1_1_1) ),
introduced(definition,[new_symbols(definition,[spl63_2])],[avatar_definition]) ).
fof(f22288,plain,
( ! [X3] : pred(X3,u1_1_1)
| ~ spl63_2 ),
inference(avatar_component_clause,[],[f22287]) ).
fof(f22290,definition,
( spl63_3
<=> ! [X1] : sub(X1,bahn_1_1) ),
introduced(definition,[new_symbols(definition,[spl63_3])],[avatar_definition]) ).
fof(f22291,plain,
( ! [X1] : sub(X1,bahn_1_1)
| ~ spl63_3 ),
inference(avatar_component_clause,[],[f22290]) ).
fof(f22293,definition,
( spl63_4
<=> ! [X4,X5,X0] :
( ~ subs(X4,hei__337en_1_1)
| ~ arg1(X4,X5)
| ~ arg2(X4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl63_4])],[avatar_definition]) ).
fof(f22294,plain,
( ! [X0,X4,X5] :
( ~ arg2(X4,X0)
| ~ arg1(X4,X5)
| ~ subs(X4,hei__337en_1_1) )
| ~ spl63_4 ),
inference(avatar_component_clause,[],[f22293]) ).
fof(f22296,definition,
( spl63_5
<=> ! [X6,X7] :
( val(X6,u2_0)
| ~ attr(X7,X6)
| sub(X6,name_1_1) ) ),
introduced(definition,[new_symbols(definition,[spl63_5])],[avatar_definition]) ).
fof(f22297,plain,
( ! [X6,X7] :
( ~ attr(X7,X6)
| val(X6,u2_0)
| sub(X6,name_1_1) )
| ~ spl63_5 ),
inference(avatar_component_clause,[],[f22296]) ).
fof(f22298,plain,
( spl63_1
| spl63_2
| spl63_3
| spl63_4
| spl63_5 ),
inference(avatar_split_clause,[],[f22273,f22296,f22293,f22290,f22287,f22284]) ).
fof(f22299,plain,
( $false
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f22276,f22288]) ).
fof(f22300,plain,
~ spl63_2,
inference(avatar_contradiction_clause,[],[f22299]) ).
fof(f22301,plain,
( $false
| ~ spl63_3 ),
inference(backward_subsumption_resolution,[],[f22274,f22291]) ).
fof(f22302,plain,
~ spl63_3,
inference(avatar_contradiction_clause,[],[f22301]) ).
fof(f22668,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(familiename_1_1,cons(name_1_1,nil)))
| ~ attr(X2,X0)
| arg1(sK50(X2),X2)
| sub(X0,X1) ),
inference(resolution,[],[f21033,f10553]) ).
fof(f22670,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(familiename_1_1,cons(name_1_1,nil)))
| ~ attr(X2,X0)
| arg2(sK50(X2),X2)
| sub(X0,X1) ),
inference(resolution,[],[f21034,f10553]) ).
fof(f22674,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(familiename_1_1,cons(name_1_1,nil)))
| ~ attr(X2,X0)
| subs(sK50(X2),hei__337en_1_1)
| sub(X0,X1) ),
inference(resolution,[],[f21035,f10553]) ).
fof(f22679,definition,
( spl63_42
<=> arg1(sK50(c5919),c5919) ),
introduced(definition,[new_symbols(definition,[spl63_42])],[avatar_definition]) ).
fof(f22681,plain,
( arg1(sK50(c5919),c5919)
| ~ spl63_42 ),
inference(avatar_component_clause,[],[f22679]) ).
fof(f22695,definition,
( spl63_44
<=> arg2(sK50(c5919),c5919) ),
introduced(definition,[new_symbols(definition,[spl63_44])],[avatar_definition]) ).
fof(f22697,plain,
( arg2(sK50(c5919),c5919)
| ~ spl63_44 ),
inference(avatar_component_clause,[],[f22695]) ).
fof(f22720,definition,
( spl63_49
<=> subs(sK50(c5919),hei__337en_1_1) ),
introduced(definition,[new_symbols(definition,[spl63_49])],[avatar_definition]) ).
fof(f22724,definition,
( spl63_50
<=> ! [X0] : ~ arg1(sK50(c5919),X0) ),
introduced(definition,[new_symbols(definition,[spl63_50])],[avatar_definition]) ).
fof(f22725,plain,
( ! [X0] : ~ arg1(sK50(c5919),X0)
| ~ spl63_50 ),
inference(avatar_component_clause,[],[f22724]) ).
fof(f22777,plain,
( val(c5920,u2_0)
| sub(c5920,name_1_1)
| ~ spl63_5 ),
inference(resolution,[],[f22297,f20811]) ).
fof(f22782,plain,
( sub(c5920,name_1_1)
| ~ spl63_5 ),
inference(forward_subsumption_resolution,[],[f22777,f22279]) ).
fof(f22783,plain,
( $false
| ~ spl63_5 ),
inference(forward_subsumption_resolution,[],[f22782,f22278]) ).
fof(f22784,plain,
~ spl63_5,
inference(avatar_contradiction_clause,[],[f22783]) ).
fof(f22824,plain,
( $false
| ~ spl63_42
| ~ spl63_50 ),
inference(backward_subsumption_resolution,[],[f22681,f22725]) ).
fof(f22825,plain,
( ~ spl63_42
| ~ spl63_50 ),
inference(avatar_contradiction_clause,[],[f22824]) ).
fof(f22854,plain,
( $false
| ~ spl63_1 ),
inference(backward_subsumption_resolution,[],[f22275,f22285]) ).
fof(f22858,plain,
~ spl63_1,
inference(avatar_contradiction_clause,[],[f22854]) ).
fof(f24462,plain,
! [X2,X0,X1] :
( ~ member(X2,cons(name_1_1,nil))
| arg1(sK50(X0),X0)
| sub(X1,X2)
| ~ attr(X0,X1) ),
inference(resolution,[],[f22668,f10553]) ).
fof(f24464,plain,
! [X2,X0,X1] :
( ~ member(X2,cons(name_1_1,nil))
| arg2(sK50(X0),X0)
| sub(X1,X2)
| ~ attr(X0,X1) ),
inference(resolution,[],[f22670,f10553]) ).
fof(f24466,plain,
! [X2,X0,X1] :
( ~ member(X2,cons(name_1_1,nil))
| subs(sK50(X0),hei__337en_1_1)
| sub(X1,X2)
| ~ attr(X0,X1) ),
inference(resolution,[],[f22674,f10553]) ).
fof(f32668,plain,
! [X0,X1] :
( ~ attr(X0,X1)
| sub(X1,name_1_1)
| arg1(sK50(X0),X0) ),
inference(resolution,[],[f24462,f10552]) ).
fof(f32670,plain,
! [X0,X1] :
( ~ attr(X0,X1)
| sub(X1,name_1_1)
| arg2(sK50(X0),X0) ),
inference(resolution,[],[f24464,f10552]) ).
fof(f33256,plain,
! [X0,X1] :
( ~ attr(X0,X1)
| sub(X1,name_1_1)
| subs(sK50(X0),hei__337en_1_1) ),
inference(resolution,[],[f24466,f10552]) ).
fof(f40769,plain,
( sub(c5920,name_1_1)
| arg1(sK50(c5919),c5919) ),
inference(resolution,[],[f32668,f20811]) ).
fof(f40850,plain,
( sub(c5920,name_1_1)
| arg2(sK50(c5919),c5919) ),
inference(resolution,[],[f32670,f20811]) ).
fof(f40931,plain,
arg2(sK50(c5919),c5919),
inference(forward_subsumption_resolution,[],[f40850,f22278]) ).
fof(f40952,plain,
spl63_44,
inference(avatar_split_clause,[],[f40931,f22695]) ).
fof(f40953,plain,
( ! [X0] :
( ~ arg1(sK50(c5919),X0)
| ~ subs(sK50(c5919),hei__337en_1_1) )
| ~ spl63_4
| ~ spl63_44 ),
inference(resolution,[],[f22697,f22294]) ).
fof(f40960,plain,
( sub(c5920,name_1_1)
| subs(sK50(c5919),hei__337en_1_1) ),
inference(resolution,[],[f33256,f20811]) ).
fof(f41041,plain,
subs(sK50(c5919),hei__337en_1_1),
inference(forward_subsumption_resolution,[],[f40960,f22278]) ).
fof(f41044,plain,
( ~ spl63_49
| spl63_50
| ~ spl63_4
| ~ spl63_44 ),
inference(avatar_split_clause,[],[f40953,f22695,f22293,f22724,f22720]) ).
fof(f41045,plain,
spl63_49,
inference(avatar_split_clause,[],[f41041,f22720]) ).
fof(f41046,plain,
arg1(sK50(c5919),c5919),
inference(forward_subsumption_resolution,[],[f40769,f22278]) ).
fof(f41047,plain,
spl63_42,
inference(avatar_split_clause,[],[f41046,f22679]) ).
cnf(s1,plain,
( spl63_1
| spl63_2
| spl63_3
| spl63_4
| spl63_5 ),
inference(sat_conversion,[],[f22298]) ).
cnf(s2,plain,
~ spl63_2,
inference(sat_conversion,[],[f22300]) ).
cnf(s3,plain,
~ spl63_3,
inference(sat_conversion,[],[f22302]) ).
cnf(s48,plain,
~ spl63_5,
inference(sat_conversion,[],[f22784]) ).
cnf(s60,plain,
( ~ spl63_42
| ~ spl63_50 ),
inference(sat_conversion,[],[f22825]) ).
cnf(s69,plain,
~ spl63_1,
inference(sat_conversion,[],[f22858]) ).
cnf(s2051,plain,
spl63_44,
inference(sat_conversion,[],[f40952]) ).
cnf(s2054,plain,
( ~ spl63_4
| ~ spl63_44
| ~ spl63_49
| spl63_50 ),
inference(sat_conversion,[],[f41044]) ).
cnf(s2055,plain,
spl63_49,
inference(sat_conversion,[],[f41045]) ).
cnf(s2056,plain,
spl63_42,
inference(sat_conversion,[],[f41047]) ).
cnf(s2057,plain,
( ~ spl63_4
| ~ spl63_44
| spl63_50 ),
inference(rat,[],[s2054,s2055]) ).
cnf(s2071,plain,
~ spl63_50,
inference(rat,[],[s60,s2056]) ).
cnf(s2072,plain,
~ spl63_4,
inference(rat,[],[s2057,s2051,s2071]) ).
cnf(s2083,plain,
$false,
inference(rat,[],[s1,s48,s2072,s3,s2,s69]) ).
fof(f41048,plain,
$false,
inference(avatar_sat_refutation,[],[s2083]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR112+1 : 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 : n004.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.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 23:02:07 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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
% 7.44/1.63 % (876191)Will run a generic schedule for satisfiability detection.
% 7.44/1.63 % (876200)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1613476598:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 7.44/1.63 % (876197)% WARNING: option uhcvi not known.
% 7.44/1.63 % (876196)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=824889781_2998 on theBenchmark for (2998ds/0Mi)
% 7.44/1.63 % (876197)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3106625339:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 7.44/1.63 % (876199)dis+10_1_sil=32000:sp=arity:random_seed=1764696562:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 7.44/1.63 % (876198)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1772582218:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 7.44/1.63 % (876201)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3673716874:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 7.44/1.63 % (876202)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3152657455:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 7.44/1.63 % (876200)Instruction limit reached!
% 7.44/1.63 % (876200)------------------------------
% 7.44/1.63 % (876200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876200)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876200)Termination reason: Instruction limit
% 7.44/1.63 % (876200)Termination phase: Blocked clause elimination
% 7.44/1.63 % (876200)Time elapsed: 0.042 s
% 7.44/1.63 % (876200)Peak memory usage: 27 MB
% 7.44/1.63 % (876200)Instructions burned: 116 (million)
% 7.44/1.63 % (876210)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=562354900:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 7.44/1.63 % (876199)Instruction limit reached!
% 7.44/1.63 % (876199)------------------------------
% 7.44/1.63 % (876199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876199)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876199)Termination reason: Instruction limit
% 7.44/1.63 % (876199)Termination phase: Saturation
% 7.44/1.63 % (876199)Time elapsed: 0.057 s
% 7.44/1.63 % (876199)Peak memory usage: 26 MB
% 7.44/1.63 % (876199)Instructions burned: 105 (million)
% 7.44/1.63 % (876201)Instruction limit reached!
% 7.44/1.63 % (876201)------------------------------
% 7.44/1.63 % (876201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876201)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876201)Termination reason: Instruction limit
% 7.44/1.63 % (876201)Termination phase: Saturation
% 7.44/1.63 % (876201)Time elapsed: 0.076 s
% 7.44/1.63 % (876201)Peak memory usage: 28 MB
% 7.44/1.63 % (876201)Instructions burned: 131 (million)
% 7.44/1.63 % (876212)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=551160379:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 7.44/1.63 % (876202)Instruction limit reached!
% 7.44/1.63 % (876202)------------------------------
% 7.44/1.63 % (876202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876202)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876202)Termination reason: Instruction limit
% 7.44/1.63 % (876202)Termination phase: Saturation
% 7.44/1.63 % (876202)Time elapsed: 0.088 s
% 7.44/1.63 % (876202)Peak memory usage: 30 MB
% 7.44/1.63 % (876202)Instructions burned: 160 (million)
% 7.44/1.63 % (876213)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=4037093123:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 7.44/1.63 % (876215)ott-21_1_sil=16000:fs=off:random_seed=2317114412:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 7.44/1.63 % TRYING [1]
% 7.44/1.63 % (876212)Instruction limit reached!
% 7.44/1.63 % (876212)------------------------------
% 7.44/1.63 % (876212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876212)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876212)Termination reason: Instruction limit
% 7.44/1.63 % (876212)Termination phase: Blocked clause elimination
% 7.44/1.63 % (876212)Time elapsed: 0.078 s
% 7.44/1.63 % (876212)Peak memory usage: 28 MB
% 7.44/1.63 % (876212)Instructions burned: 132 (million)
% 7.44/1.63 % TRYING [2]
% 7.44/1.63 % (876218)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3404992365:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 7.44/1.63 % (876215)Instruction limit reached!
% 7.44/1.63 % (876215)------------------------------
% 7.44/1.63 % (876215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876215)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876215)Termination reason: Instruction limit
% 7.44/1.63 % (876215)Termination phase: Saturation
% 7.44/1.63 % (876215)Time elapsed: 0.092 s
% 7.44/1.63 % (876215)Peak memory usage: 28 MB
% 7.44/1.63 % (876215)Instructions burned: 182 (million)
% 7.44/1.63 % (876220)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3281026874:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 7.44/1.63 % (876210)Instruction limit reached!
% 7.44/1.63 % (876210)------------------------------
% 7.44/1.63 % (876210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876210)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876210)Termination reason: Instruction limit
% 7.44/1.63 % (876210)Termination phase: Finite model building constraint generation
% 7.44/1.63 % (876210)Time elapsed: 0.182 s
% 7.44/1.63 % (876210)Peak memory usage: 54 MB
% 7.44/1.63 % (876210)Instructions burned: 715 (million)
% 7.44/1.63 % (876222)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1177650076:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 7.44/1.63 % TRYING [1]
% 7.44/1.63 % TRYING [2]
% 7.44/1.63 % (876218)Instruction limit reached!
% 7.44/1.63 % (876218)------------------------------
% 7.44/1.63 % (876218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876218)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876218)Termination reason: Instruction limit
% 7.44/1.63 % (876218)Termination phase: Saturation
% 7.44/1.63 % (876218)Time elapsed: 0.247 s
% 7.44/1.63 % (876218)Peak memory usage: 37 MB
% 7.44/1.63 % (876218)Instructions burned: 478 (million)
% 7.44/1.63 % TRYING [1]
% 7.44/1.63 % TRYING [3]
% 7.44/1.63 % (876224)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=76602157:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 7.44/1.63 % (876213)Instruction limit reached!
% 7.44/1.63 % (876213)------------------------------
% 7.44/1.63 % (876213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876213)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876213)Termination reason: Instruction limit
% 7.44/1.63 % (876213)Termination phase: Saturation
% 7.44/1.63 % (876213)Time elapsed: 0.372 s
% 7.44/1.63 % (876213)Peak memory usage: 37 MB
% 7.44/1.63 % (876213)Instructions burned: 685 (million)
% 7.44/1.63 % (876226)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=601554:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 7.44/1.63 % (876220)Instruction limit reached!
% 7.44/1.63 % (876220)------------------------------
% 7.44/1.63 % (876220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876220)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876220)Termination reason: Instruction limit
% 7.44/1.63 % (876220)Termination phase: Finite model building SAT solving
% 7.44/1.63 % (876220)Time elapsed: 0.326 s
% 7.44/1.63 % (876220)Peak memory usage: 38 MB
% 7.44/1.63 % (876220)Instructions burned: 866 (million)
% 7.44/1.63 % (876228)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1025527506:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 7.44/1.63 % (876222)Instruction limit reached!
% 7.44/1.63 % (876222)------------------------------
% 7.44/1.63 % (876222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876222)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876222)Termination reason: Instruction limit
% 7.44/1.63 % (876222)Termination phase: Saturation
% 7.44/1.63 % (876222)Time elapsed: 0.343 s
% 7.44/1.63 % (876222)Peak memory usage: 54 MB
% 7.44/1.63 % (876222)Instructions burned: 1183 (million)
% 7.44/1.63 % (876230)fmb+10_1_sil=64000:random_seed=285232131:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 7.44/1.63 % TRYING [1]
% 7.44/1.63 % TRYING [4]
% 7.44/1.63 % TRYING [2]
% 7.44/1.63 % (876226)Instruction limit reached!
% 7.44/1.63 % (876226)------------------------------
% 7.44/1.63 % (876226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876226)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876226)Termination reason: Instruction limit
% 7.44/1.63 % (876226)Termination phase: Saturation
% 7.44/1.63 % (876226)Time elapsed: 0.372 s
% 7.44/1.63 % (876226)Peak memory usage: 42 MB
% 7.44/1.63 % (876226)Instructions burned: 693 (million)
% 7.44/1.63 % (876224)Instruction limit reached!
% 7.44/1.63 % (876224)------------------------------
% 7.44/1.63 % (876224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876224)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876224)Termination reason: Instruction limit
% 7.44/1.63 % (876224)Termination phase: Finite model building constraint generation
% 7.44/1.63 % (876224)Time elapsed: 0.422 s
% 7.44/1.63 % (876224)Peak memory usage: 95 MB
% 7.44/1.63 % (876224)Instructions burned: 892 (million)
% 7.44/1.63 % (876232)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3032195386:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 7.44/1.63 % (876233)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=372026832:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 7.44/1.63 % (876228)Instruction limit reached!
% 7.44/1.63 % (876228)------------------------------
% 7.44/1.63 % (876228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.63 % (876228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.63 % (876228)CaDiCaL version: 2.1.3
% 7.44/1.63 % (876228)Termination reason: Instruction limit
% 7.44/1.63 % (876228)Termination phase: Saturation
% 7.44/1.63 % (876228)Time elapsed: 0.429 s
% 7.44/1.63 % (876228)Peak memory usage: 43 MB
% 7.44/1.63 % (876228)Instructions burned: 881 (million)
% 7.44/1.63 % (876236)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2061594248:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 7.44/1.63 % TRYING [20]
% 7.44/1.63 % TRYING [8]
% 7.44/1.63 % TRYING [3]
% 7.44/1.63 % (876197) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-876191-876197"...
% 7.44/1.63 % (876197)...printing done.
% 7.44/1.63 % (876197)Refutation found. Thanks to Tanya!
% 7.44/1.63 % SZS status Theorem for theBenchmark
% 7.44/1.63 % SZS output start Proof for theBenchmark
% See solution above
% 7.44/1.65 % (876197)------------------------------
% 7.44/1.65 % (876197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.65 % (876197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.65 % (876197)CaDiCaL version: 2.1.3
% 7.44/1.65 % (876197)Termination reason: Refutation
% 7.44/1.65 % (876197)Time elapsed: 1.186 s
% 7.44/1.65 % (876197)Peak memory usage: 45 MB
% 7.44/1.65 % (876197)Instructions burned: 2177 (million)
% 7.44/1.65 % (876191)Success in time 1.406 s
% 7.44/1.65 % Vampire exiting
%------------------------------------------------------------------------------