%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+67 : 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 : 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:47 AM UTC 2026
% Result : Theorem 71.58s 19.04s
% Output : CNFRefutation 71.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR115+67 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n016.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sun Sep 27 01:15:15 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 71.58/19.04 % SZS status Theorem for theBenchmark.p
% 71.58/19.04 % SZS output start CNFRefutation for theBenchmark.p
% 71.58/19.04 fof(ave07_era5_synth_qa07_007_mira_wp_477, hypothesis, (assoc('bildsensor$u1$u1','bild$u0') & (sub('bildsensor$u1$u1','sensor$u1$u1') & (sub(c1898,'name$u1$u1') & (pred(c1899,'x3$u1$u1') & (attr(c1998,c1999) & (sub(c1998,'einrichtung$u1$u2') & (sub(c1999,'name$u1$u1') & (val(c1999,'suv$u0') & (attr(c2002,c2003) & (sub(c2002,'firma$u1$u1') & (sub(c2003,'name$u1$u1') & (val(c2003,'bmw$u0') & (attch(c2063,c1899) & (attr(c2063,c2064) & (attr(c2063,c2069) & (sub(c2063,'firma$u1$u1') & (sub(c2064,'name$u1$u1') & (val(c2064,'bmw$u0') & (pred(c2066,'x3$u1$u1') & (sub(c2069,'name$u1$u1') & (val(c2069,'foveon$u0') & (sub(c2070,'direkt$u2$u1') & (sub(c2075,'bildsensor$u1$u1') & (sub(c2082,'digitalphotographie$u2$u1') & ('tupl$up10'(c2101,c1898,c1899,c1998,c2002,c1899,c2066,c2070,c2075,c2082) & (assoc('digitalphotographie$u2$u1','digital$u1$u1') & (sub('digitalphotographie$u2$u1','photographie$u2$u1') & (sort('bildsensor$u1$u1',d) & (card('bildsensor$u1$u1',int1) & (etype('bildsensor$u1$u1',int0) & (fact('bildsensor$u1$u1',real) & (gener('bildsensor$u1$u1',ge) & (quant('bildsensor$u1$u1',one) & (refer('bildsensor$u1$u1','refer$uc') & (varia('bildsensor$u1$u1','varia$uc') & (sort('bild$u0',fe) & (sort('sensor$u1$u1',d) & (card('sensor$u1$u1',int1) & (etype('sensor$u1$u1',int0) & (fact('sensor$u1$u1',real) & (gener('sensor$u1$u1',ge) & (quant('sensor$u1$u1',one) & (refer('sensor$u1$u1','refer$uc') & (varia('sensor$u1$u1','varia$uc') & (sort(c1898,na) & (card(c1898,int1) & (etype(c1898,int0) & (fact(c1898,real) & (gener(c1898,sp) & (quant(c1898,one) & (refer(c1898,det) & (varia(c1898,con) & (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(c1899,o) & (card(c1899,cons('x$uconstant',cons(int1,nil))) & (etype(c1899,int1) & (fact(c1899,real) & (gener(c1899,'gener$uc') & (quant(c1899,mult) & (refer(c1899,indet) & (varia(c1899,'varia$uc') & (sort('x3$u1$u1',o) & (card('x3$u1$u1',int1) & (etype('x3$u1$u1',int0) & (fact('x3$u1$u1',real) & (gener('x3$u1$u1',ge) & (quant('x3$u1$u1',one) & (refer('x3$u1$u1','refer$uc') & (varia('x3$u1$u1','varia$uc') & (sort(c1998,d) & (sort(c1998,io) & (card(c1998,int1) & (etype(c1998,int1) & (fact(c1998,real) & (gener(c1998,sp) & (quant(c1998,one) & (refer(c1998,det) & (varia(c1998,con) & (sort(c1999,na) & (card(c1999,int1) & (etype(c1999,int0) & (fact(c1999,real) & (gener(c1999,sp) & (quant(c1999,one) & (refer(c1999,indet) & (varia(c1999,'varia$uc') & (sort('einrichtung$u1$u2',d) & (sort('einrichtung$u1$u2',io) & (card('einrichtung$u1$u2','card$uc') & (etype('einrichtung$u1$u2',int1) & (fact('einrichtung$u1$u2',real) & (gener('einrichtung$u1$u2',ge) & (quant('einrichtung$u1$u2','quant$uc') & (refer('einrichtung$u1$u2','refer$uc') & (varia('einrichtung$u1$u2','varia$uc') & (sort('suv$u0',fe) & (sort(c2002,d) & (sort(c2002,io) & (card(c2002,int1) & (etype(c2002,int0) & (fact(c2002,real) & (gener(c2002,sp) & (quant(c2002,one) & (refer(c2002,det) & (varia(c2002,con) & (sort(c2003,na) & (card(c2003,int1) & (etype(c2003,int0) & (fact(c2003,real) & (gener(c2003,sp) & (quant(c2003,one) & (refer(c2003,indet) & (varia(c2003,'varia$uc') & (sort('firma$u1$u1',d) & (sort('firma$u1$u1',io) & (card('firma$u1$u1',int1) & (etype('firma$u1$u1',int0) & (fact('firma$u1$u1',real) & (gener('firma$u1$u1',ge) & (quant('firma$u1$u1',one) & (refer('firma$u1$u1','refer$uc') & (varia('firma$u1$u1','varia$uc') & (sort('bmw$u0',fe) & (sort(c2063,d) & (sort(c2063,io) & (card(c2063,int1) & (etype(c2063,int0) & (fact(c2063,real) & (gener(c2063,sp) & (quant(c2063,one) & (refer(c2063,det) & (varia(c2063,con) & (sort(c2064,na) & (card(c2064,int1) & (etype(c2064,int0) & (fact(c2064,real) & (gener(c2064,sp) & (quant(c2064,one) & (refer(c2064,indet) & (varia(c2064,'varia$uc') & (sort(c2069,na) & (card(c2069,int1) & (etype(c2069,int0) & (fact(c2069,real) & (gener(c2069,sp) & (quant(c2069,one) & (refer(c2069,indet) & (varia(c2069,'varia$uc') & (sort(c2066,o) & (card(c2066,cons('x$uconstant',cons(int1,nil))) & (etype(c2066,int1) & (fact(c2066,real) & (gener(c2066,'gener$uc') & (quant(c2066,mult) & (refer(c2066,indet) & (varia(c2066,'varia$uc') & (sort('foveon$u0',fe) & (sort(c2070,o) & (card(c2070,int1) & (etype(c2070,int0) & (fact(c2070,real) & (gener(c2070,'gener$uc') & (quant(c2070,one) & (refer(c2070,'refer$uc') & (varia(c2070,'varia$uc') & (sort('direkt$u2$u1',o) & (card('direkt$u2$u1',int1) & (etype('direkt$u2$u1',int0) & (fact('direkt$u2$u1',real) & (gener('direkt$u2$u1',ge) & (quant('direkt$u2$u1',one) & (refer('direkt$u2$u1','refer$uc') & (varia('direkt$u2$u1','varia$uc') & (sort(c2075,d) & (card(c2075,int1) & (etype(c2075,int0) & (fact(c2075,real) & (gener(c2075,'gener$uc') & (quant(c2075,one) & (refer(c2075,'refer$uc') & (varia(c2075,'varia$uc') & (sort(c2082,io) & (card(c2082,int1) & (etype(c2082,int0) & (fact(c2082,real) & (gener(c2082,sp) & (quant(c2082,one) & (refer(c2082,det) & (varia(c2082,con) & (sort('digitalphotographie$u2$u1',io) & (card('digitalphotographie$u2$u1',int1) & (etype('digitalphotographie$u2$u1',int0) & (fact('digitalphotographie$u2$u1',real) & (gener('digitalphotographie$u2$u1',ge) & (quant('digitalphotographie$u2$u1',one) & (refer('digitalphotographie$u2$u1','refer$uc') & (varia('digitalphotographie$u2$u1','varia$uc') & (sort(c2101,ent) & (card(c2101,'card$uc') & (etype(c2101,'etype$uc') & (fact(c2101,real) & (gener(c2101,'gener$uc') & (quant(c2101,'quant$uc') & (refer(c2101,'refer$uc') & (varia(c2101,'varia$uc') & (sort('digital$u1$u1',tq) & (sort('photographie$u2$u1',io) & (card('photographie$u2$u1',int1) & (etype('photographie$u2$u1',int0) & (fact('photographie$u2$u1',real) & (gener('photographie$u2$u1',ge) & (quant('photographie$u2$u1',one) & (refer('photographie$u2$u1','refer$uc') & varia('photographie$u2$u1','varia$uc')))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 71.58/19.04 fof(sub__bezeichnen_1_1_als, axiom, ! [X0] : ! [X1] : ! [X2] : (((arg1(X0,X1) & (arg2(X0,X2) & subr(X0,'sub$u0'))) => ? [X3] : ? [X4] : ? [X5] : ((arg1(X4,X1) & (arg2(X4,X5) & (hsit(X0,X3) & (mcont(X3,X4) & (obj(X3,X1) & (sub(X5,X2) & (subr(X4,'rprs$u0') & subs(X3,'bezeichnen$u1$u1')))))))))))).
% 71.58/19.04 fof(sub__sub_0_expansion, axiom, ! [X0] : ! [X1] : ((sub(X0,X1) => ? [X2] : ((arg1(X2,X0) & (arg2(X2,X1) & subr(X2,'sub$u0'))))))).
% 71.58/19.04 fof(synth_qa07_007_mira_wp_477, conjecture, ? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ((attr(X0,X1) & (attr(X3,X2) & (attr(X5,X6) & (obj(X4,X0) & (sub(X1,'name$u1$u1') & (sub(X0,'firma$u1$u1') & (sub(X2,'name$u1$u1') & (val(X1,'bmw$u0') & val(X2,'bmw$u0'))))))))))).
% 71.58/19.04 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ((attr(X0,X1) & (attr(X3,X2) & (attr(X5,X6) & (obj(X4,X0) & (sub(X1,'name$u1$u1') & (sub(X0,'firma$u1$u1') & (sub(X2,'name$u1$u1') & (val(X1,'bmw$u0') & val(X2,'bmw$u0')))))))))), inference(negate_conjecture, [status(cth)], [synth_qa07_007_mira_wp_477])).
% 71.58/19.04 cnf(c4, plain, attr(c2002,c2003), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_477])).
% 71.58/19.04 cnf(c5, plain, sub(c2003,'name$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_477])).
% 71.58/19.04 cnf(c7, plain, attr(c2063,c2069), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_477])).
% 71.58/19.04 cnf(c215, plain, val(c2003,'bmw$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_477])).
% 71.58/19.04 cnf(c216, plain, sub(c2002,'firma$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_477])).
% 71.58/19.04 cnf(c476, plain, ~arg2(X0,X1) | ~subr(X0,'sub$u0') | ~arg1(X0,X2) | X3(X0,X2,X1), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 71.58/19.04 cnf(c479, plain, ~X0(X1,X2,X3) | obj(sK333(X1,X2,X3),X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 71.58/19.04 cnf(c485, plain, ~sub(X0,X1) | arg1(sK338(X0,X1),X0), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 71.58/19.04 cnf(c486, plain, ~sub(X0,X1) | subr(sK338(X0,X1),'sub$u0'), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 71.58/19.04 cnf(c487, plain, ~sub(X0,X1) | arg2(sK338(X0,X1),X1), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 71.58/19.04 cnf(c571, plain, ~attr(X0,X1) | ~obj(X2,X3) | ~val(X4,'bmw$u0') | ~sub(X4,'name$u1$u1') | ~val(X1,'bmw$u0') | ~sub(X1,'name$u1$u1') | ~sub(X3,'firma$u1$u1') | ~attr(X5,X6) | ~attr(X3,X4), inference(clausification, [status(esa)], [negated_conjecture])).
% 71.58/19.04 cnf(d0, plain, ~'Ts329'(X0,X1,X2) | ~sub(X3,'name$u1$u1') | ~sub(X1,'firma$u1$u1') | ~sub(X4,'name$u1$u1') | ~attr(X5,X6) | ~attr(X1,X3) | ~attr(X7,X4) | ~val(X3,'bmw$u0') | ~val(X4,'bmw$u0'), inference(resolution, [status(thm)], [c479,c571])).
% 71.58/19.04 cnf(d1, plain, ~sub(X0,'name$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'firma$u1$u1') | ~attr(X3,X0) | ~attr(X4,X5) | ~attr(X2,X1) | ~val(X0,'bmw$u0') | ~val(X1,'bmw$u0') | ~arg2(X6,X7) | ~arg1(X6,X2) | ~subr(X6,'sub$u0'), inference(resolution, [status(thm)], [d0,c476])).
% 71.58/19.04 cnf(d2, plain, ~sub(X0,X1) | ~sub(X2,'firma$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'name$u1$u1') | ~attr(X5,X6) | ~attr(X7,X4) | ~attr(X2,X3) | ~val(X3,'bmw$u0') | ~val(X4,'bmw$u0') | ~arg2(sK338(X0,X1),X8) | ~arg1(sK338(X0,X1),X2), inference(resolution, [status(thm)], [c486,d1])).
% 71.58/19.04 cnf(d3, plain, ~sub(X0,'name$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'firma$u1$u1') | ~sub(X2,X3) | ~attr(X4,X0) | ~attr(X5,X6) | ~attr(X2,X1) | ~val(X0,'bmw$u0') | ~val(X1,'bmw$u0') | ~arg2(sK338(X2,X3),X7) | ~sub(X2,X3), inference(resolution, [status(thm)], [d2,c485])).
% 71.58/19.04 cnf(d4, plain, ~sub(X0,X1) | ~sub(X0,X1) | ~sub(X0,'firma$u1$u1') | ~sub(X2,'name$u1$u1') | ~sub(X3,'name$u1$u1') | ~attr(X4,X5) | ~attr(X6,X3) | ~attr(X0,X2) | ~val(X2,'bmw$u0') | ~val(X3,'bmw$u0'), inference(resolution, [status(thm)], [c487,d3])).
% 71.58/19.04 cnf(d5, plain, ~sub(X0,'name$u1$u1') | ~sub(c2003,'name$u1$u1') | ~sub(X1,X2) | ~sub(X1,'firma$u1$u1') | ~attr(X3,X0) | ~attr(X4,X5) | ~attr(X1,c2003) | ~val(X0,'bmw$u0'), inference(resolution, [status(thm)], [d4,c215])).
% 71.58/19.04 cnf(d6, plain, ~sub(X0,X1) | ~sub(X0,'firma$u1$u1') | ~sub(X2,'name$u1$u1') | ~attr(X3,X4) | ~attr(X5,X2) | ~attr(X0,c2003) | ~val(X2,'bmw$u0'), inference(resolution, [status(thm)], [c5,d5])).
% 71.58/19.04 cnf(d7, plain, ~sub(c2003,'name$u1$u1') | ~sub(X0,X1) | ~sub(X0,'firma$u1$u1') | ~attr(X2,c2003) | ~attr(X3,X4) | ~attr(X0,c2003), inference(resolution, [status(thm)], [d6,c215])).
% 71.58/19.04 cnf(d8, plain, ~sub(X0,X1) | ~sub(X0,'firma$u1$u1') | ~attr(X2,X3) | ~attr(X4,c2003) | ~attr(X0,c2003), inference(resolution, [status(thm)], [c5,d7])).
% 71.58/19.04 cnf(d9, plain, ~sub(c2002,X0) | ~sub(c2002,'firma$u1$u1') | ~attr(X1,c2003) | ~attr(X2,X3), inference(resolution, [status(thm)], [d8,c4])).
% 71.58/19.04 cnf(d10, plain, ~sub(c2002,X0) | ~attr(X1,X2) | ~attr(X3,c2003), inference(resolution, [status(thm)], [c216,d9])).
% 71.58/19.04 cnf(d11, plain, ~sub(c2002,X0) | ~attr(X1,c2003), inference(resolution, [status(thm)], [d10,c7])).
% 71.58/19.04 cnf(d12, plain, ~sub(c2002,X0), inference(resolution, [status(thm)], [d11,c4])).
% 71.58/19.04 cnf(d13, plain, $false, inference(resolution, [status(thm)], [d12,c216])).
% 71.58/19.04 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------