%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+81 : 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:48 AM UTC 2026
% Result : Theorem 57.82s 15.20s
% Output : CNFRefutation 57.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 2
% Syntax : Number of formulae : 20 ( 8 unt; 0 def)
% Number of atoms : 248 ( 0 equ)
% Maximal formula atoms : 166 ( 12 avg)
% Number of connectives : 284 ( 56 ~; 45 |; 183 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 166 ( 14 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 20 ( 19 usr; 1 prp; 0-4 aty)
% Number of functors : 47 ( 47 usr; 46 con; 0-2 aty)
% Number of variables : 55 ( 16 sgn 0 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_007_mira_wp_491,hypothesis,
( varia('nabe$u1$u1','varia$uc')
& refer('nabe$u1$u1','refer$uc')
& quant('nabe$u1$u1',one)
& gener('nabe$u1$u1',ge)
& fact('nabe$u1$u1',real)
& etype('nabe$u1$u1',int0)
& card('nabe$u1$u1',int1)
& sort('nabe$u1$u1',o)
& varia('rotor$u1$u1','varia$uc')
& refer('rotor$u1$u1','refer$uc')
& quant('rotor$u1$u1',one)
& gener('rotor$u1$u1',ge)
& fact('rotor$u1$u1',real)
& etype('rotor$u1$u1',int0)
& card('rotor$u1$u1',int1)
& sort('rotor$u1$u1',o)
& varia('anlage$u1$u1','varia$uc')
& refer('anlage$u1$u1','refer$uc')
& quant('anlage$u1$u1',one)
& gener('anlage$u1$u1',ge)
& fact('anlage$u1$u1',real)
& etype('anlage$u1$u1',int0)
& card('anlage$u1$u1',int1)
& sort('anlage$u1$u1',as)
& varia('motor$u$u1$u1','varia$uc')
& refer('motor$u$u1$u1','refer$uc')
& quant('motor$u$u1$u1',one)
& gener('motor$u$u1$u1',ge)
& fact('motor$u$u1$u1',real)
& etype('motor$u$u1$u1',int0)
& card('motor$u$u1$u1',int1)
& sort('motor$u$u1$u1',d)
& varia('motoranlage$u1$u1','varia$uc')
& refer('motoranlage$u1$u1','refer$uc')
& quant('motoranlage$u1$u1',one)
& gener('motoranlage$u1$u1',ge)
& fact('motoranlage$u1$u1',real)
& etype('motoranlage$u1$u1',int0)
& card('motoranlage$u1$u1',int1)
& sort('motoranlage$u1$u1',as)
& varia(c9,'varia$uc')
& refer(c9,'refer$uc')
& quant(c9,one)
& gener(c9,'gener$uc')
& fact(c9,real)
& etype(c9,int0)
& card(c9,int1)
& sort(c9,as)
& 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)
& varia(c58,'varia$uc')
& refer(c58,indet)
& quant(c58,one)
& gener(c58,sp)
& fact(c58,real)
& etype(c58,int0)
& card(c58,int1)
& sort(c58,na)
& gener('n374bernehmen$u1$u1',ge)
& fact('n374bernehmen$u1$u1',real)
& sort('n374bernehmen$u1$u1',da)
& varia(c62,con)
& refer(c62,det)
& quant(c62,nfquant)
& gener(c62,sp)
& fact(c62,real)
& etype(c62,int1)
& card(c62,int3)
& sort(c62,o)
& gener('sollen$u0','gener$uc')
& fact('sollen$u0',real)
& sort('sollen$u0',md)
& varia(c57,con)
& refer(c57,det)
& quant(c57,one)
& gener(c57,sp)
& fact(c57,real)
& etype(c57,int0)
& card(c57,int1)
& sort(c57,io)
& sort(c57,d)
& gener(c45,sp)
& fact(c45,real)
& sort(c45,da)
& varia('konstruktion$u1$u1','varia$uc')
& refer('konstruktion$u1$u1','refer$uc')
& quant('konstruktion$u1$u1',one)
& gener('konstruktion$u1$u1',ge)
& fact('konstruktion$u1$u1',real)
& etype('konstruktion$u1$u1',int0)
& card('konstruktion$u1$u1',int1)
& sort('konstruktion$u1$u1',d)
& varia(c4,con)
& refer(c4,det)
& quant(c4,one)
& gener(c4,sp)
& fact(c4,real)
& etype(c4,int0)
& card(c4,int1)
& sort(c4,d)
& varia('rotornabe$u1$u1','varia$uc')
& refer('rotornabe$u1$u1','refer$uc')
& quant('rotornabe$u1$u1',one)
& gener('rotornabe$u1$u1',ge)
& fact('rotornabe$u1$u1',real)
& etype('rotornabe$u1$u1',int0)
& card('rotornabe$u1$u1',int1)
& sort('rotornabe$u1$u1',o)
& varia(c16,'varia$uc')
& refer(c16,indet)
& quant(c16,mult)
& gener(c16,'gener$uc')
& fact(c16,real)
& etype(c16,int1)
& card(c16,cons('x$uconstant',cons(int1,nil)))
& sort(c16,o)
& varia('getriebe$u$u1$u1','varia$uc')
& refer('getriebe$u$u1$u1','refer$uc')
& quant('getriebe$u$u1$u1',one)
& gener('getriebe$u$u1$u1',ge)
& fact('getriebe$u$u1$u1',real)
& etype('getriebe$u$u1$u1',int0)
& card('getriebe$u$u1$u1',int1)
& sort('getriebe$u$u1$u1',d)
& varia(c12,'varia$uc')
& refer(c12,indet)
& quant(c12,mult)
& gener(c12,'gener$uc')
& fact(c12,real)
& etype(c12,int1)
& card(c12,cons('x$uconstant',cons(int1,nil)))
& sort(c12,d)
& sub('rotornabe$u1$u1','nabe$u1$u1')
& assoc('rotornabe$u1$u1','rotor$u1$u1')
& subs('motoranlage$u1$u1','anlage$u1$u1')
& assoc('motoranlage$u1$u1','motor$u$u1$u1')
& subs(c9,'motoranlage$u1$u1')
& attch(c9,c4)
& 'itms$up4'(c62,c4,c12,c16)
& val(c58,'bmw$u0')
& sub(c58,'name$u1$u1')
& sub(c57,'firma$u1$u1')
& attr(c57,c58)
& subs(c45,'n374bernehmen$u1$u1')
& obj(c45,c62)
& modl(c45,'sollen$u0')
& agt(c45,c57)
& sub(c4,'konstruktion$u1$u1')
& pred(c16,'rotornabe$u1$u1')
& pred(c12,'getriebe$u$u1$u1') ) ).
fof(synth_qa07_007_mira_wp_491,conjecture,
? [X0,X1,X2,X3,X4,X5,X6] :
( val(X2,'bmw$u0')
& val(X1,'bmw$u0')
& subs(X4,'n374bernehmen$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')
& subs(X4,'n374bernehmen$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_491]) ).
cnf(c3,plain,
agt(c45,c57),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_491]) ).
cnf(c6,plain,
subs(c45,'n374bernehmen$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_491]) ).
cnf(c7,plain,
attr(c57,c58),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_491]) ).
cnf(c8,plain,
sub(c57,'firma$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_491]) ).
cnf(c9,plain,
sub(c58,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_491]) ).
cnf(c10,plain,
val(c58,'bmw$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_491]) ).
cnf(c344,plain,
( ~ attr(X2,X1)
| ~ subs(X6,'n374bernehmen$u1$u1')
| ~ agt(X6,X3)
| ~ val(X1,'bmw$u0')
| ~ attr(X4,X5)
| ~ attr(X3,X0)
| ~ sub(X2,'firma$u1$u1')
| ~ sub(X0,'name$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ val(X0,'bmw$u0') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ val(X0,'bmw$u0')
| ~ attr(X1,X0)
| ~ attr(X3,c58)
| ~ attr(X4,X5)
| ~ subs(X2,'n374bernehmen$u1$u1')
| ~ agt(X2,X3)
| ~ sub(c58,'name$u1$u1')
| ~ sub(X1,'firma$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[c344,c10]) ).
cnf(d1,plain,
( ~ val(X1,'bmw$u0')
| ~ attr(X0,X1)
| ~ attr(X3,c58)
| ~ attr(X4,X5)
| ~ subs(X2,'n374bernehmen$u1$u1')
| ~ agt(X2,X3)
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[c9,d0]) ).
cnf(d2,plain,
( ~ attr(X0,c58)
| ~ attr(X2,c58)
| ~ attr(X3,X4)
| ~ subs(X1,'n374bernehmen$u1$u1')
| ~ agt(X1,X2)
| ~ sub(X0,'firma$u1$u1')
| ~ sub(c58,'name$u1$u1') ),
inference(resolution,[status(thm)],[d1,c10]) ).
cnf(d3,plain,
( ~ attr(X0,c58)
| ~ attr(X2,c58)
| ~ attr(X3,X4)
| ~ subs(X1,'n374bernehmen$u1$u1')
| ~ agt(X1,X2)
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[c9,d2]) ).
cnf(d4,plain,
( ~ attr(X1,c58)
| ~ attr(X2,X3)
| ~ subs(X0,'n374bernehmen$u1$u1')
| ~ agt(X0,X1)
| ~ sub(c57,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d3,c7]) ).
cnf(d5,plain,
( ~ attr(X1,c58)
| ~ attr(X2,X3)
| ~ subs(X0,'n374bernehmen$u1$u1')
| ~ agt(X0,X1) ),
inference(resolution,[status(thm)],[c8,d4]) ).
cnf(d6,plain,
( ~ attr(X1,X2)
| ~ subs(X0,'n374bernehmen$u1$u1')
| ~ agt(X0,c57) ),
inference(resolution,[status(thm)],[d5,c7]) ).
cnf(d7,plain,
( ~ subs(X0,'n374bernehmen$u1$u1')
| ~ agt(X0,c57) ),
inference(resolution,[status(thm)],[d6,c7]) ).
cnf(d8,plain,
~ agt(c45,c57),
inference(resolution,[status(thm)],[d7,c6]) ).
cnf(d9,plain,
$false,
inference(resolution,[status(thm)],[c3,d8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR115+81 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.46 % Computer : n016.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.46 % CPULimit : 300
% 0.20/0.46 % WCLimit : 300
% 0.20/0.46 % DateTime : Sun Sep 27 01:17:02 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.46 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 57.82/15.20 % SZS status Theorem for theBenchmark.p
% 57.82/15.20 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------