%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+71 : 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 : n006.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 82.77s 11.54s
% Output : CNFRefutation 82.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+71 : 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.37 % Computer : n006.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 01:11:10 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 82.77/11.54 % SZS status Theorem for theBenchmark.p
% 82.77/11.54 % SZS output start CNFRefutation for theBenchmark.p
% 82.77/11.54 fof(ave07_era5_synth_qa07_007_mira_wp_481, hypothesis, (aff(c1371,c1565) & (init(c1371,c1569) & (prop(c1371,'technisch$u$u1$u1') & (subs(c1371,'entwicklung$u1$u2') & (temp(c1371,c1576) & (attr(c1565,c1566) & (sub(c1565,'firma$u1$u1') & (sub(c1566,'name$u1$u1') & (val(c1566,'bmw$u0') & (sub(c1569,'historie$u1$u1') & (sub(c1576,'gegenwart$u$u1$u1') & (sub(c1585,'vorzeitigkeit$u1$u1') & (modl(c21,'sollen$u0') & (obj(c21,c1371) & (subs(c21,'darlegen$u1$u1') & (temp(c21,c1585) & (sort(c1371,ad) & (card(c1371,int1) & (etype(c1371,int0) & (fact(c1371,real) & (gener(c1371,sp) & (quant(c1371,one) & (refer(c1371,det) & (varia(c1371,con) & (sort(c1565,d) & (sort(c1565,io) & (card(c1565,int1) & (etype(c1565,int0) & (fact(c1565,real) & (gener(c1565,sp) & (quant(c1565,one) & (refer(c1565,det) & (varia(c1565,con) & (sort(c1569,ta) & (card(c1569,int1) & (etype(c1569,int0) & (fact(c1569,real) & (gener(c1569,sp) & (quant(c1569,one) & (refer(c1569,det) & (varia(c1569,con) & (sort('technisch$u$u1$u1',nq) & (sort('entwicklung$u1$u2',ad) & (card('entwicklung$u1$u2',int1) & (etype('entwicklung$u1$u2',int0) & (fact('entwicklung$u1$u2',real) & (gener('entwicklung$u1$u2',ge) & (quant('entwicklung$u1$u2',one) & (refer('entwicklung$u1$u2','refer$uc') & (varia('entwicklung$u1$u2','varia$uc') & (sort(c1576,ta) & (card(c1576,int1) & (etype(c1576,int0) & (fact(c1576,real) & (gener(c1576,sp) & (quant(c1576,one) & (refer(c1576,det) & (varia(c1576,con) & (sort(c1566,na) & (card(c1566,int1) & (etype(c1566,int0) & (fact(c1566,real) & (gener(c1566,sp) & (quant(c1566,one) & (refer(c1566,indet) & (varia(c1566,'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('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('bmw$u0',fe) & (sort('historie$u1$u1',ta) & (card('historie$u1$u1',int1) & (etype('historie$u1$u1',int0) & (fact('historie$u1$u1',real) & (gener('historie$u1$u1',ge) & (quant('historie$u1$u1',one) & (refer('historie$u1$u1','refer$uc') & (varia('historie$u1$u1','varia$uc') & (sort('gegenwart$u$u1$u1',ta) & (card('gegenwart$u$u1$u1',int1) & (etype('gegenwart$u$u1$u1',int0) & (fact('gegenwart$u$u1$u1',real) & (gener('gegenwart$u$u1$u1',ge) & (quant('gegenwart$u$u1$u1',one) & (refer('gegenwart$u$u1$u1','refer$uc') & (varia('gegenwart$u$u1$u1','varia$uc') & (sort(c1585,ta) & (card(c1585,int1) & (etype(c1585,int0) & (fact(c1585,real) & (gener(c1585,sp) & (quant(c1585,one) & (refer(c1585,det) & (varia(c1585,con) & (sort('vorzeitigkeit$u1$u1',ta) & (card('vorzeitigkeit$u1$u1',int1) & (etype('vorzeitigkeit$u1$u1',int0) & (fact('vorzeitigkeit$u1$u1',real) & (gener('vorzeitigkeit$u1$u1',ge) & (quant('vorzeitigkeit$u1$u1',one) & (refer('vorzeitigkeit$u1$u1','refer$uc') & (varia('vorzeitigkeit$u1$u1','varia$uc') & (sort(c21,da) & (fact(c21,real) & (gener(c21,sp) & (sort('sollen$u0',md) & (fact('sollen$u0',real) & (gener('sollen$u0','gener$uc') & (sort('darlegen$u1$u1',da) & (fact('darlegen$u1$u1',real) & gener('darlegen$u1$u1',ge)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 82.77/11.54 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')))))))))))).
% 82.77/11.54 fof(sub__sub_0_expansion, axiom, ! [X0] : ! [X1] : ((sub(X0,X1) => ? [X2] : ((arg1(X2,X0) & (arg2(X2,X1) & subr(X2,'sub$u0'))))))).
% 82.77/11.54 fof(synth_qa07_007_mira_wp_481, 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'))))))))))).
% 82.77/11.54 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_481])).
% 82.77/11.54 cnf(c3, plain, sub(c1565,'firma$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_481])).
% 82.77/11.54 cnf(c4, plain, val(c1566,'bmw$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_481])).
% 82.77/11.54 cnf(c121, plain, sub(c1566,'name$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_481])).
% 82.77/11.54 cnf(c122, plain, attr(c1565,c1566), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_481])).
% 82.77/11.54 cnf(c357, plain, ~arg2(X0,X1) | ~subr(X0,'sub$u0') | ~arg1(X0,X2) | X3(X0,X2,X1), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 82.77/11.54 cnf(c360, plain, ~X0(X1,X2,X3) | obj(sK298(X1,X2,X3),X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 82.77/11.54 cnf(c366, plain, ~sub(X0,X1) | arg1(sK303(X0,X1),X0), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 82.77/11.54 cnf(c367, plain, ~sub(X0,X1) | subr(sK303(X0,X1),'sub$u0'), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 82.77/11.54 cnf(c368, plain, ~sub(X0,X1) | arg2(sK303(X0,X1),X1), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 82.77/11.54 cnf(c448, plain, ~sub(X0,'firma$u1$u1') | ~obj(X1,X0) | ~attr(X2,X3) | ~sub(X4,'name$u1$u1') | ~sub(X5,'name$u1$u1') | ~attr(X0,X5) | ~val(X4,'bmw$u0') | ~attr(X6,X4) | ~val(X5,'bmw$u0'), inference(clausification, [status(esa)], [negated_conjecture])).
% 82.77/11.54 cnf(d0, plain, ~sub(X0,'name$u1$u1') | ~sub(c1565,'firma$u1$u1') | ~sub(c1566,'name$u1$u1') | ~val(X0,'bmw$u0') | ~val(c1566,'bmw$u0') | ~obj(X1,c1565) | ~attr(X2,X3) | ~attr(X4,X0), inference(resolution, [status(thm)], [c122,c448])).
% 82.77/11.54 cnf(d1, plain, ~sub(X0,'name$u1$u1') | ~sub(c1566,'name$u1$u1') | ~val(X0,'bmw$u0') | ~val(c1566,'bmw$u0') | ~obj(X1,c1565) | ~attr(X2,X0) | ~attr(X3,X4), inference(resolution, [status(thm)], [c3,d0])).
% 82.77/11.54 cnf(d2, plain, ~sub(X0,'name$u1$u1') | ~sub(c1566,'name$u1$u1') | ~val(X0,'bmw$u0') | ~obj(X1,c1565) | ~attr(X2,X3) | ~attr(X4,X0), inference(resolution, [status(thm)], [c4,d1])).
% 82.77/11.54 cnf(d3, plain, ~sub(X0,'name$u1$u1') | ~val(X0,'bmw$u0') | ~obj(X1,c1565) | ~attr(X2,X0) | ~attr(X3,X4), inference(resolution, [status(thm)], [c121,d2])).
% 82.77/11.54 cnf(d4, plain, ~sub(c1566,'name$u1$u1') | ~val(c1566,'bmw$u0') | ~obj(X0,c1565) | ~attr(X1,X2), inference(resolution, [status(thm)], [d3,c122])).
% 82.77/11.54 cnf(d5, plain, ~sub(c1566,'name$u1$u1') | ~obj(X0,c1565) | ~attr(X1,X2), inference(resolution, [status(thm)], [c4,d4])).
% 82.77/11.54 cnf(d6, plain, ~obj(X0,c1565) | ~attr(X1,X2), inference(resolution, [status(thm)], [c121,d5])).
% 82.77/11.54 cnf(d7, plain, ~obj(X0,c1565), inference(resolution, [status(thm)], [d6,c122])).
% 82.77/11.54 cnf(d8, plain, ~'Ts294'(X0,c1565,X1), inference(resolution, [status(thm)], [c360,d7])).
% 82.77/11.54 cnf(d9, plain, ~arg2(X0,X1) | ~arg1(X0,c1565) | ~subr(X0,'sub$u0'), inference(resolution, [status(thm)], [d8,c357])).
% 82.77/11.54 cnf(d10, plain, ~sub(X0,X1) | ~arg2(sK303(X0,X1),X2) | ~arg1(sK303(X0,X1),c1565), inference(resolution, [status(thm)], [c367,d9])).
% 82.77/11.54 cnf(d11, plain, ~sub(c1565,X0) | ~arg2(sK303(c1565,X0),X1) | ~sub(c1565,X0), inference(resolution, [status(thm)], [d10,c366])).
% 82.77/11.54 cnf(d12, plain, ~sub(c1565,X0) | ~sub(c1565,X0), inference(resolution, [status(thm)], [c368,d11])).
% 82.77/11.54 cnf(d13, plain, $false, inference(resolution, [status(thm)], [d12,c3])).
% 82.77/11.54 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------