%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR113+10 : 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 : n016.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:31 AM UTC 2026
% Result : Theorem 60.01s 9.31s
% Output : CNFRefutation 60.01s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR113+10 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n016.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:18 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 60.01/9.31 % SZS status Theorem for theBenchmark.p
% 60.01/9.31 % SZS output start CNFRefutation for theBenchmark.p
% 60.01/9.31 fof(ave07_era5_synth_qa07_003_mira_wp_178_a270, hypothesis, (assoc('bundeland$u1$u1','bund$u2$u1') & (sub('bundeland$u1$u1','gebietsinstitution$u1$u1') & (sub('bundeland$u1$u1','land$u1$u1') & (assoc('bunderegierung$u1$u1','bund$u1$u1') & (sub('bunderegierung$u1$u1','regierung$u1$u1') & (sub(c81293,'freiheitsstatue$u1$u1') & (sub(c81332,'insel$u$u1$u1') & (attr(c81339,c81340) & (sub(c81339,'insel$u$u1$u1') & (sub(c81340,'name$u1$u1') & (val(c81340,'liberty$uisland$u0') & (prop(c81355,'amerikanisch$u$u1$u1') & (sub(c81355,'bunderegierung$u1$u1') & (sub(c81366,'national$u2$u1') & (sub(c81368,'park$u$u1$u1') & (subs(c81373,'service$u1$u1') & (sub(c81378,'enklave$u1$u1') & (sub(c81395,'bezirk$u$u1$u1') & (attch(c81401,c81395) & (attr(c81401,c81402) & (sub(c81401,'land$u1$u1') & (sub(c81402,'name$u1$u1') & (val(c81402,'usa$u0') & (attr(c81409,c81410) & (sub(c81409,'bundeland$u1$u1') & (sub(c81410,'name$u1$u1') & (val(c81410,'new$ujersey$u0') & ('tupl$up11'(c81513,c81293,c81332,c81339,c81355,c81366,c81368,c81373,c81378,c81395,c81409) & (assoc('freiheitsstatue$u1$u1','freiheit$u1$u1') & (sub('freiheitsstatue$u1$u1','statue$u1$u1') & (sort('bundeland$u1$u1',d) & (sort('bundeland$u1$u1',io) & (card('bundeland$u1$u1',int1) & (etype('bundeland$u1$u1',int0) & (fact('bundeland$u1$u1',real) & (gener('bundeland$u1$u1',ge) & (quant('bundeland$u1$u1',one) & (refer('bundeland$u1$u1','refer$uc') & (varia('bundeland$u1$u1','varia$uc') & (sort('bund$u2$u1',d) & (card('bund$u2$u1','card$uc') & (etype('bund$u2$u1',int1) & (fact('bund$u2$u1',real) & (gener('bund$u2$u1',ge) & (quant('bund$u2$u1','quant$uc') & (refer('bund$u2$u1','refer$uc') & (varia('bund$u2$u1','varia$uc') & (sort('gebietsinstitution$u1$u1',ent) & (card('gebietsinstitution$u1$u1','card$uc') & (etype('gebietsinstitution$u1$u1','etype$uc') & (fact('gebietsinstitution$u1$u1',real) & (gener('gebietsinstitution$u1$u1','gener$uc') & (quant('gebietsinstitution$u1$u1','quant$uc') & (refer('gebietsinstitution$u1$u1','refer$uc') & (varia('gebietsinstitution$u1$u1','varia$uc') & (sort('land$u1$u1',d) & (sort('land$u1$u1',io) & (card('land$u1$u1',int1) & (etype('land$u1$u1',int0) & (fact('land$u1$u1',real) & (gener('land$u1$u1',ge) & (quant('land$u1$u1',one) & (refer('land$u1$u1','refer$uc') & (varia('land$u1$u1','varia$uc') & (sort('bunderegierung$u1$u1',d) & (sort('bunderegierung$u1$u1',io) & (card('bunderegierung$u1$u1','card$uc') & (etype('bunderegierung$u1$u1',int1) & (fact('bunderegierung$u1$u1',real) & (gener('bunderegierung$u1$u1',ge) & (quant('bunderegierung$u1$u1','quant$uc') & (refer('bunderegierung$u1$u1','refer$uc') & (varia('bunderegierung$u1$u1','varia$uc') & (sort('bund$u1$u1',d) & (sort('bund$u1$u1',io) & (card('bund$u1$u1','card$uc') & (etype('bund$u1$u1',int1) & (fact('bund$u1$u1',real) & (gener('bund$u1$u1',ge) & (quant('bund$u1$u1','quant$uc') & (refer('bund$u1$u1','refer$uc') & (varia('bund$u1$u1','varia$uc') & (sort('regierung$u1$u1',d) & (sort('regierung$u1$u1',io) & (card('regierung$u1$u1','card$uc') & (etype('regierung$u1$u1',int1) & (fact('regierung$u1$u1',real) & (gener('regierung$u1$u1',ge) & (quant('regierung$u1$u1','quant$uc') & (refer('regierung$u1$u1','refer$uc') & (varia('regierung$u1$u1','varia$uc') & (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$u1$u1',d) & (card('freiheitsstatue$u1$u1',int1) & (etype('freiheitsstatue$u1$u1',int0) & (fact('freiheitsstatue$u1$u1',real) & (gener('freiheitsstatue$u1$u1',ge) & (quant('freiheitsstatue$u1$u1',one) & (refer('freiheitsstatue$u1$u1','refer$uc') & (varia('freiheitsstatue$u1$u1','varia$uc') & (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$u$u1$u1',d) & (card('insel$u$u1$u1',int1) & (etype('insel$u$u1$u1',int0) & (fact('insel$u$u1$u1',real) & (gener('insel$u$u1$u1',ge) & (quant('insel$u$u1$u1',one) & (refer('insel$u$u1$u1','refer$uc') & (varia('insel$u$u1$u1','varia$uc') & (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$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('liberty$uisland$u0',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$u$u1$u1',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$u2$u1',o) & (card('national$u2$u1',int1) & (etype('national$u2$u1',int0) & (fact('national$u2$u1',real) & (gener('national$u2$u1',ge) & (quant('national$u2$u1',one) & (refer('national$u2$u1','refer$uc') & (varia('national$u2$u1','varia$uc') & (sort(c81368,d) & (card(c81368,int1) & (etype(c81368,int0) & (fact(c81368,real) & (gener(c81368,'gener$uc') & (quant(c81368,one) & (refer(c81368,'refer$uc') & (varia(c81368,'varia$uc') & (sort('park$u$u1$u1',d) & (card('park$u$u1$u1',int1) & (etype('park$u$u1$u1',int0) & (fact('park$u$u1$u1',real) & (gener('park$u$u1$u1',ge) & (quant('park$u$u1$u1',one) & (refer('park$u$u1$u1','refer$uc') & (varia('park$u$u1$u1','varia$uc') & (sort(c81373,ad) & (card(c81373,int1) & (etype(c81373,int0) & (fact(c81373,real) & (gener(c81373,'gener$uc') & (quant(c81373,one) & (refer(c81373,'refer$uc') & (varia(c81373,'varia$uc') & (sort('service$u1$u1',ad) & (card('service$u1$u1',int1) & (etype('service$u1$u1',int0) & (fact('service$u1$u1',real) & (gener('service$u1$u1',ge) & (quant('service$u1$u1',one) & (refer('service$u1$u1','refer$uc') & (varia('service$u1$u1','varia$uc') & (sort(c81378,d) & (card(c81378,int1) & (etype(c81378,int0) & (fact(c81378,real) & (gener(c81378,'gener$uc') & (quant(c81378,one) & (refer(c81378,'refer$uc') & (varia(c81378,'varia$uc') & (sort('enklave$u1$u1',d) & (card('enklave$u1$u1',int1) & (etype('enklave$u1$u1',int0) & (fact('enklave$u1$u1',real) & (gener('enklave$u1$u1',ge) & (quant('enklave$u1$u1',one) & (refer('enklave$u1$u1','refer$uc') & (varia('enklave$u1$u1','varia$uc') & (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$u$u1$u1',d) & (card('bezirk$u$u1$u1',int1) & (etype('bezirk$u$u1$u1',int0) & (fact('bezirk$u$u1$u1',real) & (gener('bezirk$u$u1$u1',ge) & (quant('bezirk$u$u1$u1',one) & (refer('bezirk$u$u1$u1','refer$uc') & (varia('bezirk$u$u1$u1','varia$uc') & (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$uc') & (sort('usa$u0',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$uc') & (sort('new$ujersey$u0',fe) & (sort(c81513,ent) & (card(c81513,'card$uc') & (etype(c81513,'etype$uc') & (fact(c81513,real) & (gener(c81513,'gener$uc') & (quant(c81513,'quant$uc') & (refer(c81513,'refer$uc') & (varia(c81513,'varia$uc') & (sort('freiheit$u1$u1',as) & (sort('freiheit$u1$u1',io) & (card('freiheit$u1$u1',int1) & (etype('freiheit$u1$u1',int0) & (fact('freiheit$u1$u1',real) & (gener('freiheit$u1$u1',ge) & (quant('freiheit$u1$u1',one) & (refer('freiheit$u1$u1','refer$uc') & (varia('freiheit$u1$u1','varia$uc') & (sort('statue$u1$u1',d) & (card('statue$u1$u1',int1) & (etype('statue$u1$u1',int0) & (fact('statue$u1$u1',real) & (gener('statue$u1$u1',ge) & (quant('statue$u1$u1',one) & (refer('statue$u1$u1','refer$uc') & varia('statue$u1$u1','varia$uc')))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 60.01/9.31 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)))))))))).
% 60.01/9.31 fof(local_function___flp, axiom, ! [X0] : ! [X1] : (((in(X0,X1) | (an(X0,X1) | bei(X0,X1))) => flp(X0,X1)))).
% 60.01/9.31 fof(loc__stehen_1_1_loc, axiom, ! [X0] : ! [X1] : ((loc(X0,X1) => ? [X2] : ((loc(X2,X1) & (scar(X2,X0) & subs(X2,'stehen$u1$u1'))))))).
% 60.01/9.31 fof(fact_8825, axiom, 'state$uadjective$ustate$ubinding'('amerikanisch$u$u1$u1','usa$u0')).
% 60.01/9.31 fof(synth_qa07_003_mira_wp_178_a270, conjecture, ? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ((flp(X0,X2) & (attr(X2,X1) & (loc(X3,X0) & (scar(X3,X4) & (sub(X1,'name$u1$u1') & (subs(X3,'stehen$u1$u1') & val(X1,'usa$u0'))))))))).
% 60.01/9.31 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ((flp(X0,X2) & (attr(X2,X1) & (loc(X3,X0) & (scar(X3,X4) & (sub(X1,'name$u1$u1') & (subs(X3,'stehen$u1$u1') & val(X1,'usa$u0')))))))), inference(negate_conjecture, [status(cth)], [synth_qa07_003_mira_wp_178_a270])).
% 60.01/9.31 cnf(c11, plain, prop(c81355,'amerikanisch$u$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_003_mira_wp_178_a270])).
% 60.01/9.31 cnf(c422, plain, ~prop(X0,X1) | ~'state$uadjective$ustate$ubinding'(X1,X2) | X3(X0,X2), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 60.01/9.31 cnf(c423, plain, ~X0(X1,X2) | in(sK178(X1,X2),sK176(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 60.01/9.31 cnf(c424, plain, ~X0(X1,X2) | attr(sK176(X1,X2),sK177(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 60.01/9.31 cnf(c425, plain, ~X0(X1,X2) | loc(X1,sK178(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 60.01/9.31 cnf(c427, plain, ~X0(X1,X2) | sub(sK177(X1,X2),'name$u1$u1'), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 60.01/9.31 cnf(c428, plain, ~X0(X1,X2) | val(sK177(X1,X2),X2), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 60.01/9.31 cnf(c448, plain, ~in(X0,X1) | flp(X0,X1), inference(clausification, [status(esa)], [local_function___flp])).
% 60.01/9.31 cnf(c451, plain, ~loc(X0,X1) | loc(sK219(X0,X1),X1), inference(clausification, [status(esa)], [loc__stehen_1_1_loc])).
% 60.01/9.31 cnf(c452, plain, ~loc(X0,X1) | scar(sK219(X0,X1),X0), inference(clausification, [status(esa)], [loc__stehen_1_1_loc])).
% 60.01/9.31 cnf(c453, plain, ~loc(X0,X1) | subs(sK219(X0,X1),'stehen$u1$u1'), inference(clausification, [status(esa)], [loc__stehen_1_1_loc])).
% 60.01/9.31 cnf(c467, plain, 'state$uadjective$ustate$ubinding'('amerikanisch$u$u1$u1','usa$u0'), inference(clausification, [status(esa)], [fact_8825])).
% 60.01/9.31 cnf(c475, plain, ~sub(X0,'name$u1$u1') | ~attr(X1,X0) | ~flp(X2,X1) | ~subs(X3,'stehen$u1$u1') | ~loc(X3,X2) | ~val(X0,'usa$u0') | ~scar(X3,X4), inference(clausification, [status(esa)], [negated_conjecture])).
% 60.01/9.31 cnf(d0, plain, ~prop(X0,'amerikanisch$u$u1$u1') | 'Ts172'(X0,'usa$u0'), inference(resolution, [status(thm)], [c422,c467])).
% 60.01/9.31 cnf(d1, plain, 'Ts172'(c81355,'usa$u0'), inference(resolution, [status(thm)], [d0,c11])).
% 60.01/9.31 cnf(d2, plain, flp(sK178(X0,X1),sK176(X0,X1)) | ~'Ts172'(X0,X1), inference(resolution, [status(thm)], [c448,c423])).
% 60.01/9.31 cnf(d3, plain, ~'Ts172'(X0,X1) | ~sub(X2,'name$u1$u1') | ~attr(sK176(X0,X1),X2) | ~val(X2,'usa$u0') | ~subs(X3,'stehen$u1$u1') | ~loc(X3,sK178(X0,X1)) | ~scar(X3,X4), inference(resolution, [status(thm)], [d2,c475])).
% 60.01/9.31 cnf(d4, plain, ~sub(X0,'name$u1$u1') | ~attr(sK176(X1,X2),X0) | ~val(X0,'usa$u0') | ~subs(sK219(X3,sK178(X1,X2)),'stehen$u1$u1') | ~scar(sK219(X3,sK178(X1,X2)),X4) | ~'Ts172'(X1,X2) | ~loc(X3,sK178(X1,X2)), inference(resolution, [status(thm)], [d3,c451])).
% 60.01/9.31 cnf(d5, plain, ~sub(X0,'name$u1$u1') | ~attr(sK176(X1,X2),X0) | ~val(X0,'usa$u0') | ~subs(sK219(X3,sK178(X1,X2)),'stehen$u1$u1') | ~loc(X3,sK178(X1,X2)) | ~'Ts172'(X1,X2) | ~loc(X3,sK178(X1,X2)), inference(resolution, [status(thm)], [d4,c452])).
% 60.01/9.31 cnf(d6, plain, ~sub(X0,'name$u1$u1') | ~attr(sK176(X1,X2),X0) | ~val(X0,'usa$u0') | ~loc(X3,sK178(X1,X2)) | ~'Ts172'(X1,X2) | ~loc(X3,sK178(X1,X2)), inference(resolution, [status(thm)], [d5,c453])).
% 60.01/9.31 cnf(d7, plain, ~sub(X0,'name$u1$u1') | ~attr(sK176(X1,X2),X0) | ~val(X0,'usa$u0') | ~'Ts172'(X1,X2) | ~'Ts172'(X1,X2), inference(resolution, [status(thm)], [d6,c425])).
% 60.01/9.31 cnf(d8, plain, ~sub(sK177(X0,X1),'name$u1$u1') | ~val(sK177(X0,X1),'usa$u0') | ~'Ts172'(X0,X1) | ~'Ts172'(X0,X1), inference(resolution, [status(thm)], [d7,c424])).
% 60.01/9.31 cnf(d9, plain, ~sub(sK177(X0,'usa$u0'),'name$u1$u1') | ~'Ts172'(X0,'usa$u0') | ~'Ts172'(X0,'usa$u0'), inference(resolution, [status(thm)], [d8,c428])).
% 60.01/9.31 cnf(d10, plain, ~'Ts172'(X0,'usa$u0') | ~'Ts172'(X0,'usa$u0'), inference(resolution, [status(thm)], [d9,c427])).
% 60.01/9.31 cnf(d11, plain, $false, inference(resolution, [status(thm)], [d10,d1])).
% 60.01/9.31 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------