%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+76 : 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 : n012.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:48 AM UTC 2026
% Result : Theorem 29.35s 4.80s
% Output : CNFRefutation 29.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 2
% Syntax : Number of formulae : 23 ( 10 unt; 0 def)
% Number of atoms : 294 ( 0 equ)
% Maximal formula atoms : 197 ( 12 avg)
% Number of connectives : 338 ( 67 ~; 55 |; 216 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 197 ( 14 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 25 usr; 1 prp; 0-2 aty)
% Number of functors : 66 ( 66 usr; 65 con; 0-2 aty)
% Number of variables : 45 ( 0 sgn 0 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_007_mira_wp_486,hypothesis,
( varia('fahrer$u$u1$u1','varia$uc')
& refer('fahrer$u$u1$u1','refer$uc')
& quant('fahrer$u$u1$u1',one)
& gener('fahrer$u$u1$u1',ge)
& fact('fahrer$u$u1$u1',real)
& etype('fahrer$u$u1$u1',int0)
& card('fahrer$u$u1$u1',int1)
& sort('fahrer$u$u1$u1',d)
& varia('kunstwerk$u1$u1','varia$uc')
& refer('kunstwerk$u1$u1','refer$uc')
& quant('kunstwerk$u1$u1','quant$uc')
& gener('kunstwerk$u1$u1',ge)
& fact('kunstwerk$u1$u1',real)
& etype('kunstwerk$u1$u1',int1)
& card('kunstwerk$u1$u1','card$uc')
& sort('kunstwerk$u1$u1',io)
& varia('erfolg$u$u1$u1','varia$uc')
& refer('erfolg$u$u1$u1','refer$uc')
& quant('erfolg$u$u1$u1',one)
& gener('erfolg$u$u1$u1',ge)
& fact('erfolg$u$u1$u1',real)
& etype('erfolg$u$u1$u1',int0)
& card('erfolg$u$u1$u1',int1)
& sort('erfolg$u$u1$u1',as)
& gener('rennen$u1$u1',ge)
& fact('rennen$u1$u1',real)
& sort('rennen$u1$u1',da)
& gener('werden$u1$u1',ge)
& fact('werden$u1$u1',real)
& sort('werden$u1$u1',dn)
& sort('weit$u1$u1',mq)
& varia('rennerfolg$u1$u1','varia$uc')
& refer('rennerfolg$u1$u1','refer$uc')
& quant('rennerfolg$u1$u1',one)
& gener('rennerfolg$u1$u1',ge)
& fact('rennerfolg$u1$u1',real)
& etype('rennerfolg$u1$u1',int0)
& card('rennerfolg$u1$u1',int1)
& sort('rennerfolg$u1$u1',as)
& varia(c6,'varia$uc')
& refer(c6,'refer$uc')
& quant(c6,mult)
& gener(c6,'gener$uc')
& fact(c6,real)
& etype(c6,int1)
& card(c6,cons('x$uconstant',cons(int1,nil)))
& sort(c6,as)
& gener('prop$u0','gener$uc')
& fact('prop$u0',real)
& sort('prop$u0',st)
& gener(c500,sp)
& fact(c500,real)
& sort(c500,st)
& gener('fahren$u1$u2',ge)
& fact('fahren$u1$u2',real)
& sort('fahren$u1$u2',da)
& gener(c498,sp)
& fact(c498,real)
& sort(c498,da)
& gener('rprs$u0','gener$uc')
& fact('rprs$u0',real)
& sort('rprs$u0',st)
& varia('werksfahrer$u1$u1','varia$uc')
& refer('werksfahrer$u1$u1','refer$uc')
& quant('werksfahrer$u1$u1',one)
& gener('werksfahrer$u1$u1',ge)
& fact('werksfahrer$u1$u1',real)
& etype('werksfahrer$u1$u1',int0)
& card('werksfahrer$u1$u1',int1)
& sort('werksfahrer$u1$u1',d)
& varia(c493,'varia$uc')
& refer(c493,indet)
& quant(c493,one)
& gener(c493,sp)
& fact(c493,real)
& etype(c493,int0)
& card(c493,int1)
& sort(c493,d)
& card(c486,int1926)
& sort(c486,nu)
& varia('jahr$u$u1$u1','varia$uc')
& refer('jahr$u$u1$u1','refer$uc')
& quant('jahr$u$u1$u1','quant$uc')
& gener('jahr$u$u1$u1',ge)
& fact('jahr$u$u1$u1',real)
& etype('jahr$u$u1$u1','etype$uc')
& card('jahr$u$u1$u1','card$uc')
& sort('jahr$u$u1$u1',ta)
& sort('jahr$u$u1$u1',oa)
& sort('jahr$u$u1$u1',me)
& varia(c491,'varia$uc')
& refer(c491,'refer$uc')
& quant(c491,'quant$uc')
& gener(c491,sp)
& fact(c491,real)
& etype(c491,'etype$uc')
& card(c491,'card$uc')
& sort(c491,ta)
& sort(c491,oa)
& sort(c491,me)
& varia(c490,con)
& refer(c490,det)
& quant(c490,one)
& gener(c490,sp)
& fact(c490,real)
& etype(c490,int0)
& card(c490,int1)
& sort(c490,t)
& gener('verpflichten$u2$u2',ge)
& fact('verpflichten$u2$u2',real)
& sort('verpflichten$u2$u2',da)
& gener(c8,sp)
& fact(c8,real)
& sort(c8,dn)
& gener(c497,sp)
& fact(c497,real)
& sort(c497,st)
& varia(c403,'varia$uc')
& refer(c403,det)
& quant(c403,one)
& gener(c403,sp)
& fact(c403,real)
& etype(c403,int0)
& card(c403,int1)
& sort(c403,o)
& gener(c410,sp)
& fact(c410,real)
& sort(c410,da)
& sort('bmw$u0',fe)
& varia('name$u1$u1','varia$uc')
& refer('name$u1$u1','refer$uc')
& quant('name$u1$u1',one)
& gener('name$u1$u1',ge)
& fact('name$u1$u1',real)
& etype('name$u1$u1',int0)
& card('name$u1$u1',int1)
& sort('name$u1$u1',na)
& varia('firma$u1$u1','varia$uc')
& refer('firma$u1$u1','refer$uc')
& quant('firma$u1$u1',one)
& gener('firma$u1$u1',ge)
& fact('firma$u1$u1',real)
& etype('firma$u1$u1',int0)
& card('firma$u1$u1',int1)
& sort('firma$u1$u1',io)
& sort('firma$u1$u1',d)
& sort('aufmerksam$u1$u1',nq)
& varia(c402,'varia$uc')
& refer(c402,indet)
& quant(c402,one)
& gener(c402,sp)
& fact(c402,real)
& etype(c402,int0)
& card(c402,int1)
& sort(c402,na)
& varia(c401,con)
& refer(c401,det)
& quant(c401,one)
& gener(c401,sp)
& fact(c401,real)
& etype(c401,int0)
& card(c401,int1)
& sort(c401,io)
& sort(c401,d)
& sub('werksfahrer$u1$u1','fahrer$u$u1$u1')
& assoc('werksfahrer$u1$u1','kunstwerk$u1$u1')
& subs('rennerfolg$u1$u1','erfolg$u$u1$u1')
& assoc('rennerfolg$u1$u1','rennen$u1$u1')
& subs(c8,'werden$u1$u1')
& rslt(c8,c500)
& dur(c8,c403)
& prop(c6,'weit$u1$u1')
& preds(c6,'rennerfolg$u1$u1')
& ante(c6,c8)
& subr(c500,'prop$u0')
& arg2(c500,'aufmerksam$u1$u1')
& arg1(c500,c401)
& subs(c498,'fahren$u1$u2')
& agt(c498,c493)
& subr(c497,'rprs$u0')
& arg2(c497,c493)
& arg1(c497,c403)
& sub(c493,'werksfahrer$u1$u1')
& val(c491,c486)
& sub(c491,'jahr$u$u1$u1')
& attr(c490,c491)
& temp(c410,c490)
& subs(c410,'verpflichten$u2$u2')
& semrel(c410,c8)
& rslt(c410,c497)
& obj(c410,c403)
& agt(c410,c401)
& val(c402,'bmw$u0')
& sub(c402,'name$u1$u1')
& sub(c401,'firma$u1$u1')
& prop(c401,'aufmerksam$u1$u1')
& attr(c401,c402) ) ).
fof(synth_qa07_007_mira_wp_486,conjecture,
? [X0,X1,X2,X3,X4,X5,X6] :
( val(X2,'bmw$u0')
& val(X1,'bmw$u0')
& temp(X4,X5)
& sub(X6,'jahr$u$u1$u1')
& sub(X2,'name$u1$u1')
& sub(X0,'firma$u1$u1')
& sub(X1,'name$u1$u1')
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1)
& agt(X4,X3) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6] :
( val(X2,'bmw$u0')
& val(X1,'bmw$u0')
& temp(X4,X5)
& sub(X6,'jahr$u$u1$u1')
& sub(X2,'name$u1$u1')
& sub(X0,'firma$u1$u1')
& sub(X1,'name$u1$u1')
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1)
& agt(X4,X3) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_007_mira_wp_486]) ).
cnf(c0,plain,
attr(c401,c402),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_486]) ).
cnf(c2,plain,
sub(c401,'firma$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_486]) ).
cnf(c3,plain,
sub(c402,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_486]) ).
cnf(c4,plain,
val(c402,'bmw$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_486]) ).
cnf(c5,plain,
agt(c410,c401),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_486]) ).
cnf(c10,plain,
temp(c410,c490),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_486]) ).
cnf(c11,plain,
attr(c490,c491),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_486]) ).
cnf(c12,plain,
sub(c491,'jahr$u$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_486]) ).
cnf(c413,plain,
( ~ sub(X6,'firma$u1$u1')
| ~ attr(X6,X0)
| ~ val(X2,'bmw$u0')
| ~ agt(X5,X1)
| ~ sub(X2,'name$u1$u1')
| ~ temp(X5,X3)
| ~ sub(X4,'jahr$u$u1$u1')
| ~ attr(X3,X4)
| ~ sub(X0,'name$u1$u1')
| ~ attr(X1,X2)
| ~ val(X0,'bmw$u0') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ agt(c410,X3)
| ~ val(X4,'bmw$u0')
| ~ val(X2,'bmw$u0')
| ~ sub(X4,'name$u1$u1')
| ~ sub(X2,'name$u1$u1')
| ~ sub(X0,'jahr$u$u1$u1')
| ~ sub(X1,'firma$u1$u1')
| ~ attr(X3,X4)
| ~ attr(X1,X2)
| ~ attr(c490,X0) ),
inference(resolution,[status(thm)],[c413,c10]) ).
cnf(d1,plain,
( ~ val(X2,'bmw$u0')
| ~ val(X0,'bmw$u0')
| ~ sub(X3,'jahr$u$u1$u1')
| ~ sub(X1,'firma$u1$u1')
| ~ sub(X2,'name$u1$u1')
| ~ sub(X0,'name$u1$u1')
| ~ attr(c490,X3)
| ~ attr(X1,X2)
| ~ attr(c401,X0) ),
inference(resolution,[status(thm)],[d0,c5]) ).
cnf(d2,plain,
( ~ val(X1,'bmw$u0')
| ~ sub(c402,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X2,'jahr$u$u1$u1')
| ~ attr(c490,X2)
| ~ attr(c401,c402)
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[d1,c4]) ).
cnf(d3,plain,
( ~ val(X1,'bmw$u0')
| ~ sub(c402,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X2,'jahr$u$u1$u1')
| ~ attr(c490,X2)
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[c0,d2]) ).
cnf(d4,plain,
( ~ val(X1,'bmw$u0')
| ~ sub(X0,'firma$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X2,'jahr$u$u1$u1')
| ~ attr(c490,X2)
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[c3,d3]) ).
cnf(d5,plain,
( ~ sub(X0,'firma$u1$u1')
| ~ sub(c402,'name$u1$u1')
| ~ sub(X1,'jahr$u$u1$u1')
| ~ attr(c490,X1)
| ~ attr(X0,c402) ),
inference(resolution,[status(thm)],[d4,c4]) ).
cnf(d6,plain,
( ~ sub(X0,'firma$u1$u1')
| ~ sub(X1,'jahr$u$u1$u1')
| ~ attr(c490,X1)
| ~ attr(X0,c402) ),
inference(resolution,[status(thm)],[c3,d5]) ).
cnf(d7,plain,
( ~ sub(X0,'jahr$u$u1$u1')
| ~ attr(c490,X0)
| ~ attr(c401,c402) ),
inference(resolution,[status(thm)],[d6,c2]) ).
cnf(d8,plain,
( ~ sub(X0,'jahr$u$u1$u1')
| ~ attr(c490,X0) ),
inference(resolution,[status(thm)],[c0,d7]) ).
cnf(d9,plain,
~ attr(c490,c491),
inference(resolution,[status(thm)],[d8,c12]) ).
cnf(d10,plain,
$false,
inference(resolution,[status(thm)],[c11,d9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR115+76 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Sun Sep 27 01:11:37 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.35/4.80 % SZS status Theorem for theBenchmark.p
% 29.35/4.80 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------