%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR114+9 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:39 AM UTC 2026
% Result : Theorem 215.03s 29.05s
% Output : CNFRefutation 215.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR114+9 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.41 % Computer : n008.cluster.edu
% 0.17/0.41 % Model : x86_64 x86_64
% 0.17/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.41 % Memory : 8046.5625MB
% 0.17/0.41 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Sun Sep 27 01:07:10 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.42 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 215.03/29.05 % SZS status Theorem for theBenchmark.p
% 215.03/29.05 % SZS output start CNFRefutation for theBenchmark.p
% 215.03/29.05 fof(ave07_era5_synth_qa07_004_mira_news_552_a281, hypothesis, (attr(c35597,c35598) & (sub(c35597,'mensch$u1$u1') & (sub(c35598,'eigenname$u1$u1') & (val(c35598,'rutelli$u0') & (pred(c35599,'kathpress$u1$u1') & (prop(c35605,'althergebracht$u1$u1') & (sub(c35605,'papstaudienz$u1$u1') & (sub(c35611,'buergermeister$u1$u1') & (sub(c35616,'stadtrat$u1$u1') & (attch(c35631,c35616) & (prop(c35631,'italienisch$u$u1$u1') & (sub(c35631,'hauptsstadt$u1$u1') & (sub(c35676,'kirchenf$u$u374rst$u1$u1') & (prop(c35683,'unbeirrt$u1$u1') & (sub(c35683,'einsatz$u1$u1') & (poss(c35688,c35683) & (sub(c35694,'friede$u1$u1') & (name(c35704,'edelste$uaufgabe$uroms$u0') & ('tupl$up10'(c35765,c35597,c35599,c35605,c35611,c35616,c35676,c35683,c35694,c35704) & (sub('hauptsstadt$u1$u1','stadt$u$u1$u1') & (assoc('papstaudienz$u1$u1','kirchenf$u$u374rst$u1$u1') & (sub('papstaudienz$u1$u1','audienz$u$u1$u1') & (assoc('stadtrat$u1$u1','stadt$u$u1$u1') & (sub('stadtrat$u1$u1','rat$u2$u1') & (sort(c35597,d) & (card(c35597,int1) & (etype(c35597,int0) & (fact(c35597,real) & (gener(c35597,sp) & (quant(c35597,one) & (refer(c35597,det) & (varia(c35597,con) & (sort(c35598,na) & (card(c35598,int1) & (etype(c35598,int0) & (fact(c35598,real) & (gener(c35598,sp) & (quant(c35598,one) & (refer(c35598,indet) & (varia(c35598,'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('rutelli$u0',fe) & (sort(c35599,o) & (card(c35599,cons('x$uconstant',cons(int1,nil))) & (etype(c35599,int1) & (fact(c35599,real) & (gener(c35599,'gener$uc') & (quant(c35599,mult) & (refer(c35599,indet) & (varia(c35599,'varia$uc') & (sort('kathpress$u1$u1',o) & (card('kathpress$u1$u1',int1) & (etype('kathpress$u1$u1',int0) & (fact('kathpress$u1$u1',real) & (gener('kathpress$u1$u1',ge) & (quant('kathpress$u1$u1',one) & (refer('kathpress$u1$u1','refer$uc') & (varia('kathpress$u1$u1','varia$uc') & (sort(c35605,o) & (card(c35605,int1) & (etype(c35605,int0) & (fact(c35605,real) & (gener(c35605,sp) & (quant(c35605,one) & (refer(c35605,det) & (varia(c35605,con) & (sort('althergebracht$u1$u1',nq) & (sort('papstaudienz$u1$u1',o) & (card('papstaudienz$u1$u1',int1) & (etype('papstaudienz$u1$u1',int0) & (fact('papstaudienz$u1$u1',real) & (gener('papstaudienz$u1$u1',ge) & (quant('papstaudienz$u1$u1',one) & (refer('papstaudienz$u1$u1','refer$uc') & (varia('papstaudienz$u1$u1','varia$uc') & (sort(c35611,d) & (card(c35611,int1) & (etype(c35611,int0) & (fact(c35611,real) & (gener(c35611,sp) & (quant(c35611,one) & (refer(c35611,det) & (varia(c35611,con) & (sort('buergermeister$u1$u1',d) & (card('buergermeister$u1$u1',int1) & (etype('buergermeister$u1$u1',int0) & (fact('buergermeister$u1$u1',real) & (gener('buergermeister$u1$u1',ge) & (quant('buergermeister$u1$u1',one) & (refer('buergermeister$u1$u1','refer$uc') & (varia('buergermeister$u1$u1','varia$uc') & (sort(c35616,d) & (sort(c35616,io) & (card(c35616,int1) & (etype(c35616,int1) & (fact(c35616,real) & (gener(c35616,sp) & (quant(c35616,one) & (refer(c35616,det) & (varia(c35616,con) & (sort('stadtrat$u1$u1',d) & (sort('stadtrat$u1$u1',io) & (card('stadtrat$u1$u1','card$uc') & (etype('stadtrat$u1$u1',int1) & (fact('stadtrat$u1$u1',real) & (gener('stadtrat$u1$u1',ge) & (quant('stadtrat$u1$u1','quant$uc') & (refer('stadtrat$u1$u1','refer$uc') & (varia('stadtrat$u1$u1','varia$uc') & (sort(c35631,d) & (sort(c35631,io) & (card(c35631,int1) & (etype(c35631,int0) & (fact(c35631,real) & (gener(c35631,sp) & (quant(c35631,one) & (refer(c35631,det) & (varia(c35631,con) & (sort('italienisch$u$u1$u1',nq) & (sort('hauptsstadt$u1$u1',d) & (sort('hauptsstadt$u1$u1',io) & (card('hauptsstadt$u1$u1',int1) & (etype('hauptsstadt$u1$u1',int0) & (fact('hauptsstadt$u1$u1',real) & (gener('hauptsstadt$u1$u1',ge) & (quant('hauptsstadt$u1$u1',one) & (refer('hauptsstadt$u1$u1','refer$uc') & (varia('hauptsstadt$u1$u1','varia$uc') & (sort(c35676,d) & (card(c35676,int1) & (etype(c35676,int0) & (fact(c35676,real) & (gener(c35676,sp) & (quant(c35676,one) & (refer(c35676,det) & (varia(c35676,con) & (sort('kirchenf$u$u374rst$u1$u1',d) & (card('kirchenf$u$u374rst$u1$u1',int1) & (etype('kirchenf$u$u374rst$u1$u1',int0) & (fact('kirchenf$u$u374rst$u1$u1',real) & (gener('kirchenf$u$u374rst$u1$u1',ge) & (quant('kirchenf$u$u374rst$u1$u1',one) & (refer('kirchenf$u$u374rst$u1$u1','refer$uc') & (varia('kirchenf$u$u374rst$u1$u1','varia$uc') & (sort(c35683,ad) & (sort(c35683,io) & (card(c35683,int1) & (etype(c35683,int0) & (fact(c35683,real) & (gener(c35683,sp) & (quant(c35683,one) & (refer(c35683,det) & (varia(c35683,'varia$uc') & (sort('unbeirrt$u1$u1',nq) & (sort('einsatz$u1$u1',ad) & (sort('einsatz$u1$u1',io) & (card('einsatz$u1$u1',int1) & (etype('einsatz$u1$u1',int0) & (fact('einsatz$u1$u1',real) & (gener('einsatz$u1$u1',ge) & (quant('einsatz$u1$u1',one) & (refer('einsatz$u1$u1','refer$uc') & (varia('einsatz$u1$u1','varia$uc') & (sort(c35688,o) & (card(c35688,int1) & (etype(c35688,int0) & (fact(c35688,real) & (gener(c35688,sp) & (quant(c35688,one) & (refer(c35688,det) & (varia(c35688,'varia$uc') & (sort(c35694,as) & (sort(c35694,io) & (card(c35694,int1) & (etype(c35694,int0) & (fact(c35694,real) & (gener(c35694,sp) & (quant(c35694,one) & (refer(c35694,det) & (varia(c35694,con) & (sort('friede$u1$u1',as) & (sort('friede$u1$u1',io) & (card('friede$u1$u1',int1) & (etype('friede$u1$u1',int0) & (fact('friede$u1$u1',real) & (gener('friede$u1$u1',ge) & (quant('friede$u1$u1',one) & (refer('friede$u1$u1','refer$uc') & (varia('friede$u1$u1','varia$uc') & (sort(c35704,o) & (card(c35704,int1) & (etype(c35704,int0) & (fact(c35704,real) & (gener(c35704,'gener$uc') & (quant(c35704,one) & (refer(c35704,'refer$uc') & (varia(c35704,'varia$uc') & (sort('edelste$uaufgabe$uroms$u0',fe) & (sort(c35765,ent) & (card(c35765,'card$uc') & (etype(c35765,'etype$uc') & (fact(c35765,real) & (gener(c35765,'gener$uc') & (quant(c35765,'quant$uc') & (refer(c35765,'refer$uc') & (varia(c35765,'varia$uc') & (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('audienz$u$u1$u1',o) & (card('audienz$u$u1$u1',int1) & (etype('audienz$u$u1$u1',int0) & (fact('audienz$u$u1$u1',real) & (gener('audienz$u$u1$u1',ge) & (quant('audienz$u$u1$u1',one) & (refer('audienz$u$u1$u1','refer$uc') & (varia('audienz$u$u1$u1','varia$uc') & (sort('rat$u2$u1',d) & (sort('rat$u2$u1',io) & (card('rat$u2$u1','card$uc') & (etype('rat$u2$u1',int1) & (fact('rat$u2$u1',real) & (gener('rat$u2$u1',ge) & (quant('rat$u2$u1','quant$uc') & (refer('rat$u2$u1','refer$uc') & varia('rat$u2$u1','varia$uc')))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 215.03/29.05 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)))))))))).
% 215.03/29.05 fof(loc__stehen_1_1_loc, axiom, ! [X0] : ! [X1] : ((loc(X0,X1) => ? [X2] : ((loc(X2,X1) & (scar(X2,X0) & subs(X2,'stehen$u1$u1'))))))).
% 215.03/29.05 fof(fact_8886, axiom, 'state$uadjective$ustate$ubinding'('italienisch$u$u1$u1','italien$u0')).
% 215.03/29.05 fof(synth_qa07_004_mira_news_552_a281, 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')))))))).
% 215.03/29.05 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_552_a281])).
% 215.03/29.05 cnf(c10, plain, prop(c35631,'italienisch$u$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_004_mira_news_552_a281])).
% 215.03/29.05 cnf(c532, plain, ~prop(X0,X1) | ~'state$uadjective$ustate$ubinding'(X1,X2) | X3(X0,X2), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 215.03/29.05 cnf(c533, plain, ~X0(X1,X2) | in(sK373(X1,X2),sK371(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 215.03/29.05 cnf(c534, plain, ~X0(X1,X2) | attr(sK371(X1,X2),sK372(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 215.03/29.05 cnf(c535, plain, ~X0(X1,X2) | loc(X1,sK373(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 215.03/29.05 cnf(c537, plain, ~X0(X1,X2) | sub(sK372(X1,X2),'name$u1$u1'), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 215.03/29.05 cnf(c608, plain, ~loc(X0,X1) | loc(sK480(X0,X1),X1), inference(clausification, [status(esa)], [loc__stehen_1_1_loc])).
% 215.03/29.05 cnf(c609, plain, ~loc(X0,X1) | scar(sK480(X0,X1),X0), inference(clausification, [status(esa)], [loc__stehen_1_1_loc])).
% 215.03/29.05 cnf(c610, plain, ~loc(X0,X1) | subs(sK480(X0,X1),'stehen$u1$u1'), inference(clausification, [status(esa)], [loc__stehen_1_1_loc])).
% 215.03/29.05 cnf(c9497, plain, 'state$uadjective$ustate$ubinding'('italienisch$u$u1$u1','italien$u0'), inference(clausification, [status(esa)], [fact_8886])).
% 215.03/29.05 cnf(c10618, plain, ~attr(X0,X1) | ~subs(X2,'stehen$u1$u1') | ~sub(X1,'name$u1$u1') | ~scar(X2,X3) | ~loc(X2,X4) | ~in(X4,X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 215.03/29.05 cnf(d0, plain, ~'Ts367'(X0,X1) | ~attr(sK371(X0,X1),X2) | ~sub(X2,'name$u1$u1') | ~subs(X3,'stehen$u1$u1') | ~loc(X3,sK373(X0,X1)) | ~scar(X3,X4), inference(resolution, [status(thm)], [c533,c10618])).
% 215.03/29.05 cnf(d1, plain, ~loc(X0,sK373(X1,X2)) | ~attr(sK371(X1,X2),X3) | ~sub(X3,'name$u1$u1') | ~subs(sK480(X0,sK373(X1,X2)),'stehen$u1$u1') | ~scar(sK480(X0,sK373(X1,X2)),X4) | ~'Ts367'(X1,X2), inference(resolution, [status(thm)], [c608,d0])).
% 215.03/29.05 cnf(d2, plain, ~attr(sK371(X0,X1),X2) | ~sub(X2,'name$u1$u1') | ~subs(sK480(X3,sK373(X0,X1)),'stehen$u1$u1') | ~loc(X3,sK373(X0,X1)) | ~'Ts367'(X0,X1) | ~loc(X3,sK373(X0,X1)), inference(resolution, [status(thm)], [d1,c609])).
% 215.03/29.05 cnf(d3, plain, ~attr(sK371(X0,X1),X2) | ~sub(X2,'name$u1$u1') | ~loc(X3,sK373(X0,X1)) | ~'Ts367'(X0,X1) | ~loc(X3,sK373(X0,X1)), inference(resolution, [status(thm)], [d2,c610])).
% 215.03/29.05 cnf(d4, plain, ~attr(sK371(X0,X1),X2) | ~sub(X2,'name$u1$u1') | ~'Ts367'(X0,X1) | ~'Ts367'(X0,X1), inference(resolution, [status(thm)], [d3,c535])).
% 215.03/29.05 cnf(d5, plain, ~sub(sK372(X0,X1),'name$u1$u1') | ~'Ts367'(X0,X1) | ~'Ts367'(X0,X1), inference(resolution, [status(thm)], [d4,c534])).
% 215.03/29.05 cnf(d6, plain, ~'Ts367'(X0,X1) | ~'Ts367'(X0,X1), inference(resolution, [status(thm)], [d5,c537])).
% 215.03/29.05 cnf(d7, plain, ~prop(X0,X1) | ~'state$uadjective$ustate$ubinding'(X1,X2), inference(resolution, [status(thm)], [d6,c532])).
% 215.03/29.05 cnf(d8, plain, ~prop(X0,'italienisch$u$u1$u1'), inference(resolution, [status(thm)], [d7,c9497])).
% 215.03/29.05 cnf(d9, plain, $false, inference(resolution, [status(thm)], [d8,c10])).
% 215.03/29.05 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------