%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR114+11 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 : Sun Sep 27 07:04:35 AM UTC 2026
% Result : Theorem 89.93s 17.56s
% Output : CNFRefutation 89.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR114+11 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 01:06:52 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 89.93/17.56 % SZS status Theorem for theBenchmark.p
% 89.93/17.56 % SZS output start CNFRefutation for theBenchmark.p
% 89.93/17.56 fof(ave07_era5_synth_qa07_004_mira_news_631, hypothesis, (tupl(c220,c36,c48) & (attr(c36,c37) & (attr(c36,c405) & (prop(c36,'sizilianisch$u1$u1') & (sub(c36,'stadt$u$u1$u1') & (sub(c37,'name$u1$u1') & (val(c37,'messina$u0') & (subs(c374,'arretierung$u1$u1') & (attr(c381,c382) & (sub(c381,'mensch$u1$u1') & (sub(c382,'eigenname$u1$u1') & (val(c382,'sebastiano$u0') & (attr(c385,c386) & (sub(c385,'stadt$u$u1$u1') & (sub(c386,'name$u1$u1') & (val(c386,'ferrara$u0') & (sub(c387,'nummer$u1$u1') & (subm(c388,c392) & (sub(c392,'gangstersyndikat$u1$u1') & (sub(c405,'name$u1$u1') & (val(c405,'messina$u0') & (prop(c417,'italienisch$u$u1$u1') & (sub(c417,'polizei$u$u1$u1') & (sub(c421,'montag$u$u1$u1') & (prop(c441,'weit$u1$u1') & (subs(c441,'schlag$u1$u1') & (prop(c448,'organisiert$u1$u1') & (sub(c448,'kriminalitaet$u1$u1') & (attr(c48,c49) & (attr(c48,c50) & (sub(c49,'tag$u1$u1') & (val(c49,c46) & (sub(c50,'monat$u1$u1') & (val(c50,c47) & ('tupl$up11'(c580,c374,c381,c385,c387,c388,c36,c417,c421,c441,c448) & (chsp2('organisieren$u1$u1','organisiert$u1$u1') & (sort(c220,ent) & (card(c220,'card$uc') & (etype(c220,'etype$uc') & (fact(c220,real) & (gener(c220,'gener$uc') & (quant(c220,'quant$uc') & (refer(c220,'refer$uc') & (varia(c220,'varia$uc') & (sort(c36,d) & (sort(c36,io) & (card(c36,int1) & (etype(c36,int0) & (fact(c36,real) & (gener(c36,sp) & (quant(c36,one) & (refer(c36,det) & (varia(c36,con) & (sort(c48,t) & (card(c48,int1) & (etype(c48,int0) & (fact(c48,real) & (gener(c48,sp) & (quant(c48,one) & (refer(c48,det) & (varia(c48,con) & (sort(c37,na) & (card(c37,int1) & (etype(c37,int0) & (fact(c37,real) & (gener(c37,sp) & (quant(c37,one) & (refer(c37,indet) & (varia(c37,'varia$uc') & (sort(c405,na) & (card(c405,int1) & (etype(c405,int0) & (fact(c405,real) & (gener(c405,sp) & (quant(c405,one) & (refer(c405,indet) & (varia(c405,'varia$uc') & (sort('sizilianisch$u1$u1',ql) & (sort('stadt$u$u1$u1',d) & (sort('stadt$u$u1$u1',io) & (card('stadt$u$u1$u1',int1) & (etype('stadt$u$u1$u1',int0) & (fact('stadt$u$u1$u1',real) & (gener('stadt$u$u1$u1',ge) & (quant('stadt$u$u1$u1',one) & (refer('stadt$u$u1$u1','refer$uc') & (varia('stadt$u$u1$u1','varia$uc') & (sort('name$u1$u1',na) & (card('name$u1$u1',int1) & (etype('name$u1$u1',int0) & (fact('name$u1$u1',real) & (gener('name$u1$u1',ge) & (quant('name$u1$u1',one) & (refer('name$u1$u1','refer$uc') & (varia('name$u1$u1','varia$uc') & (sort('messina$u0',fe) & (sort(c374,ad) & (card(c374,int1) & (etype(c374,int0) & (fact(c374,real) & (gener(c374,sp) & (quant(c374,one) & (refer(c374,det) & (varia(c374,con) & (sort('arretierung$u1$u1',ad) & (card('arretierung$u1$u1',int1) & (etype('arretierung$u1$u1',int0) & (fact('arretierung$u1$u1',real) & (gener('arretierung$u1$u1',ge) & (quant('arretierung$u1$u1',one) & (refer('arretierung$u1$u1','refer$uc') & (varia('arretierung$u1$u1','varia$uc') & (sort(c381,d) & (card(c381,int1) & (etype(c381,int0) & (fact(c381,real) & (gener(c381,sp) & (quant(c381,one) & (refer(c381,det) & (varia(c381,con) & (sort(c382,na) & (card(c382,int1) & (etype(c382,int0) & (fact(c382,real) & (gener(c382,sp) & (quant(c382,one) & (refer(c382,indet) & (varia(c382,'varia$uc') & (sort('mensch$u1$u1',d) & (card('mensch$u1$u1',int1) & (etype('mensch$u1$u1',int0) & (fact('mensch$u1$u1',real) & (gener('mensch$u1$u1',ge) & (quant('mensch$u1$u1',one) & (refer('mensch$u1$u1','refer$uc') & (varia('mensch$u1$u1','varia$uc') & (sort('eigenname$u1$u1',na) & (card('eigenname$u1$u1',int1) & (etype('eigenname$u1$u1',int0) & (fact('eigenname$u1$u1',real) & (gener('eigenname$u1$u1',ge) & (quant('eigenname$u1$u1',one) & (refer('eigenname$u1$u1','refer$uc') & (varia('eigenname$u1$u1','varia$uc') & (sort('sebastiano$u0',fe) & (sort(c385,d) & (sort(c385,io) & (card(c385,int1) & (etype(c385,int0) & (fact(c385,real) & (gener(c385,sp) & (quant(c385,one) & (refer(c385,det) & (varia(c385,con) & (sort(c386,na) & (card(c386,int1) & (etype(c386,int0) & (fact(c386,real) & (gener(c386,sp) & (quant(c386,one) & (refer(c386,indet) & (varia(c386,'varia$uc') & (sort('ferrara$u0',fe) & (sort(c387,d) & (sort(c387,io) & (card(c387,int1) & (etype(c387,int0) & (fact(c387,real) & (gener(c387,'gener$uc') & (quant(c387,one) & (refer(c387,'refer$uc') & (varia(c387,'varia$uc') & (sort('nummer$u1$u1',d) & (sort('nummer$u1$u1',io) & (card('nummer$u1$u1',int1) & (etype('nummer$u1$u1',int0) & (fact('nummer$u1$u1',real) & (gener('nummer$u1$u1',ge) & (quant('nummer$u1$u1',one) & (refer('nummer$u1$u1','refer$uc') & (varia('nummer$u1$u1','varia$uc') & (sort(c388,d) & (sort(c388,io) & (card(c388,int2) & (etype(c388,int1) & (fact(c388,real) & (gener(c388,sp) & (quant(c388,nfquant) & (refer(c388,det) & (varia(c388,'varia$uc') & (sort(c392,d) & (sort(c392,io) & (card(c392,int1) & (etype(c392,int1) & (fact(c392,real) & (gener(c392,sp) & (quant(c392,one) & (refer(c392,det) & (varia(c392,con) & (sort('gangstersyndikat$u1$u1',d) & (sort('gangstersyndikat$u1$u1',io) & (card('gangstersyndikat$u1$u1','card$uc') & (etype('gangstersyndikat$u1$u1',int1) & (fact('gangstersyndikat$u1$u1',real) & (gener('gangstersyndikat$u1$u1',ge) & (quant('gangstersyndikat$u1$u1','quant$uc') & (refer('gangstersyndikat$u1$u1','refer$uc') & (varia('gangstersyndikat$u1$u1','varia$uc') & (sort(c417,d) & (sort(c417,io) & (card(c417,int1) & (etype(c417,int0) & (fact(c417,real) & (gener(c417,sp) & (quant(c417,one) & (refer(c417,det) & (varia(c417,con) & (sort('italienisch$u$u1$u1',nq) & (sort('polizei$u$u1$u1',d) & (sort('polizei$u$u1$u1',io) & (card('polizei$u$u1$u1',int1) & (etype('polizei$u$u1$u1',int0) & (fact('polizei$u$u1$u1',real) & (gener('polizei$u$u1$u1',ge) & (quant('polizei$u$u1$u1',one) & (refer('polizei$u$u1$u1','refer$uc') & (varia('polizei$u$u1$u1','varia$uc') & (sort(c421,ta) & (card(c421,int1) & (etype(c421,int0) & (fact(c421,real) & (gener(c421,sp) & (quant(c421,one) & (refer(c421,det) & (varia(c421,con) & (sort('montag$u$u1$u1',ta) & (card('montag$u$u1$u1',int1) & (etype('montag$u$u1$u1',int0) & (fact('montag$u$u1$u1',real) & (gener('montag$u$u1$u1',ge) & (quant('montag$u$u1$u1',one) & (refer('montag$u$u1$u1','refer$uc') & (varia('montag$u$u1$u1','varia$uc') & (sort(c441,ad) & (card(c441,int1) & (etype(c441,int0) & (fact(c441,real) & (gener(c441,sp) & (quant(c441,one) & (refer(c441,indet) & (varia(c441,'varia$uc') & (sort('weit$u1$u1',mq) & (sort('schlag$u1$u1',ad) & (card('schlag$u1$u1',int1) & (etype('schlag$u1$u1',int0) & (fact('schlag$u1$u1',real) & (gener('schlag$u1$u1',ge) & (quant('schlag$u1$u1',one) & (refer('schlag$u1$u1','refer$uc') & (varia('schlag$u1$u1','varia$uc') & (sort(c448,io) & (sort(c448,na) & (card(c448,int1) & (etype(c448,int0) & (fact(c448,real) & (gener(c448,sp) & (quant(c448,one) & (refer(c448,det) & (varia(c448,con) & (sort('organisiert$u1$u1',nq) & (sort('kriminalitaet$u1$u1',io) & (sort('kriminalitaet$u1$u1',na) & (card('kriminalitaet$u1$u1',int1) & (etype('kriminalitaet$u1$u1',int0) & (fact('kriminalitaet$u1$u1',real) & (gener('kriminalitaet$u1$u1',ge) & (quant('kriminalitaet$u1$u1',one) & (refer('kriminalitaet$u1$u1','refer$uc') & (varia('kriminalitaet$u1$u1','varia$uc') & (sort(c49,me) & (sort(c49,oa) & (sort(c49,ta) & (card(c49,'card$uc') & (etype(c49,'etype$uc') & (fact(c49,real) & (gener(c49,sp) & (quant(c49,'quant$uc') & (refer(c49,'refer$uc') & (varia(c49,'varia$uc') & (sort(c50,me) & (sort(c50,oa) & (sort(c50,ta) & (card(c50,'card$uc') & (etype(c50,'etype$uc') & (fact(c50,real) & (gener(c50,sp) & (quant(c50,'quant$uc') & (refer(c50,'refer$uc') & (varia(c50,'varia$uc') & (sort('tag$u1$u1',me) & (sort('tag$u1$u1',oa) & (sort('tag$u1$u1',ta) & (card('tag$u1$u1','card$uc') & (etype('tag$u1$u1','etype$uc') & (fact('tag$u1$u1',real) & (gener('tag$u1$u1',ge) & (quant('tag$u1$u1','quant$uc') & (refer('tag$u1$u1','refer$uc') & (varia('tag$u1$u1','varia$uc') & (sort(c46,nu) & (card(c46,int28) & (sort('monat$u1$u1',me) & (sort('monat$u1$u1',oa) & (sort('monat$u1$u1',ta) & (card('monat$u1$u1','card$uc') & (etype('monat$u1$u1','etype$uc') & (fact('monat$u1$u1',real) & (gener('monat$u1$u1',ge) & (quant('monat$u1$u1','quant$uc') & (refer('monat$u1$u1','refer$uc') & (varia('monat$u1$u1','varia$uc') & (sort(c47,nu) & (card(c47,int3) & (sort(c580,ent) & (card(c580,'card$uc') & (etype(c580,'etype$uc') & (fact(c580,real) & (gener(c580,'gener$uc') & (quant(c580,'quant$uc') & (refer(c580,'refer$uc') & (varia(c580,'varia$uc') & (sort('organisieren$u1$u1',da) & (fact('organisieren$u1$u1',real) & gener('organisieren$u1$u1',ge))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 89.93/17.56 fof(state_adjective__in_state, axiom, ! [X0] : ! [X1] : ! [X2] : (((prop(X0,X1) & 'state$uadjective$ustate$ubinding'(X1,X2)) => ? [X3] : ? [X4] : ? [X5] : ((in(X5,X3) & (attr(X3,X4) & (loc(X0,X5) & (sub(X3,'land$u1$u1') & (sub(X4,'name$u1$u1') & val(X4,X2)))))))))).
% 89.93/17.56 fof(loc__stehen_1_1_loc, axiom, ! [X0] : ! [X1] : ((loc(X0,X1) => ? [X2] : ((loc(X2,X1) & (scar(X2,X0) & subs(X2,'stehen$u1$u1'))))))).
% 89.93/17.56 fof(fact_8886, axiom, 'state$uadjective$ustate$ubinding'('italienisch$u$u1$u1','italien$u0')).
% 89.93/17.56 fof(synth_qa07_004_mira_news_631, conjecture, ? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ((in(X2,X0) & (attr(X0,X1) & (loc(X4,X2) & (scar(X4,X3) & (sub(X1,'name$u1$u1') & subs(X4,'stehen$u1$u1')))))))).
% 89.93/17.56 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ((in(X2,X0) & (attr(X0,X1) & (loc(X4,X2) & (scar(X4,X3) & (sub(X1,'name$u1$u1') & subs(X4,'stehen$u1$u1'))))))), inference(negate_conjecture, [status(cth)], [synth_qa07_004_mira_news_631])).
% 89.93/17.56 cnf(c323, plain, prop(c417,'italienisch$u$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_004_mira_news_631])).
% 89.93/17.56 cnf(c557, plain, ~'state$uadjective$ustate$ubinding'(X0,X1) | ~prop(X2,X0) | X3(X2,X1), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 89.93/17.56 cnf(c558, plain, ~X0(X1,X2) | in(sK288(X1,X2),sK286(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 89.93/17.56 cnf(c559, plain, ~X0(X1,X2) | loc(X1,sK288(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 89.93/17.56 cnf(c560, plain, ~X0(X1,X2) | sub(sK287(X1,X2),'name$u1$u1'), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 89.93/17.56 cnf(c563, plain, ~X0(X1,X2) | attr(sK286(X1,X2),sK287(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 89.93/17.56 cnf(c625, plain, ~loc(X0,X1) | loc(sK382(X0,X1),X1), inference(clausification, [status(esa)], [loc__stehen_1_1_loc])).
% 89.93/17.56 cnf(c626, plain, ~loc(X0,X1) | subs(sK382(X0,X1),'stehen$u1$u1'), inference(clausification, [status(esa)], [loc__stehen_1_1_loc])).
% 89.93/17.56 cnf(c627, plain, ~loc(X0,X1) | scar(sK382(X0,X1),X0), inference(clausification, [status(esa)], [loc__stehen_1_1_loc])).
% 89.93/17.56 cnf(c673, plain, 'state$uadjective$ustate$ubinding'('italienisch$u$u1$u1','italien$u0'), inference(clausification, [status(esa)], [fact_8886])).
% 89.93/17.56 cnf(c688, plain, ~attr(X0,X1) | ~loc(X2,X3) | ~subs(X2,'stehen$u1$u1') | ~scar(X2,X4) | ~sub(X1,'name$u1$u1') | ~in(X3,X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 89.93/17.56 cnf(d0, plain, ~loc(X0,X1) | ~attr(X2,X3) | ~sub(X3,'name$u1$u1') | ~subs(sK382(X0,X1),'stehen$u1$u1') | ~loc(sK382(X0,X1),X4) | ~in(X4,X2), inference(resolution, [status(thm)], [c627,c688])).
% 89.93/17.56 cnf(d1, plain, ~attr(X0,X1) | ~sub(X1,'name$u1$u1') | ~subs(sK382(X2,X3),'stehen$u1$u1') | ~loc(X2,X3) | ~in(X3,X0) | ~loc(X2,X3), inference(resolution, [status(thm)], [d0,c625])).
% 89.93/17.56 cnf(d2, plain, ~attr(X0,X1) | ~sub(X1,'name$u1$u1') | ~loc(X2,X3) | ~in(X3,X0) | ~loc(X2,X3), inference(resolution, [status(thm)], [d1,c626])).
% 89.93/17.56 cnf(d3, plain, ~attr(sK286(X0,X1),X2) | ~sub(X2,'name$u1$u1') | ~loc(X3,sK288(X0,X1)) | ~'Ts282'(X0,X1), inference(resolution, [status(thm)], [d2,c558])).
% 89.93/17.56 cnf(d4, plain, ~attr(sK286(X0,X1),X2) | ~sub(X2,'name$u1$u1') | ~'Ts282'(X0,X1) | ~'Ts282'(X0,X1), inference(resolution, [status(thm)], [d3,c559])).
% 89.93/17.56 cnf(d5, plain, ~sub(sK287(X0,X1),'name$u1$u1') | ~'Ts282'(X0,X1) | ~'Ts282'(X0,X1), inference(resolution, [status(thm)], [d4,c563])).
% 89.93/17.56 cnf(d6, plain, ~'Ts282'(X0,X1) | ~'Ts282'(X0,X1), inference(resolution, [status(thm)], [d5,c560])).
% 89.93/17.56 cnf(d7, plain, ~prop(X0,X1) | ~'state$uadjective$ustate$ubinding'(X1,X2), inference(resolution, [status(thm)], [d6,c557])).
% 89.93/17.56 cnf(d8, plain, ~prop(X0,'italienisch$u$u1$u1'), inference(resolution, [status(thm)], [d7,c673])).
% 89.93/17.56 cnf(d9, plain, $false, inference(resolution, [status(thm)], [d8,c323])).
% 89.93/17.56 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------