%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR112+1 : 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 : n018.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:30 AM UTC 2026
% Result : Theorem 70.13s 9.19s
% Output : CNFRefutation 70.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 5
% Syntax : Number of formulae : 42 ( 13 unt; 0 def)
% Number of atoms : 302 ( 0 equ)
% Maximal formula atoms : 166 ( 7 avg)
% Number of connectives : 343 ( 83 ~; 73 |; 185 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 166 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 18 ( 17 usr; 1 prp; 0-9 aty)
% Number of functors : 51 ( 51 usr; 49 con; 0-2 aty)
% Number of variables : 101 ( 35 sgn 8 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_001_qapn_4,hypothesis,
( varia(c5901,'varia$uc')
& refer(c5901,det)
& quant(c5901,one)
& gener(c5901,sp)
& fact(c5901,real)
& etype(c5901,int0)
& card(c5901,int1)
& sort(c5901,o)
& varia(c6138,'varia$uc')
& refer(c6138,'refer$uc')
& quant(c6138,'quant$uc')
& gener(c6138,'gener$uc')
& fact(c6138,real)
& etype(c6138,'etype$uc')
& card(c6138,'card$uc')
& sort(c6138,ent)
& varia('minute$u1$u1','varia$uc')
& refer('minute$u1$u1','refer$uc')
& quant('minute$u1$u1','quant$uc')
& gener('minute$u1$u1',ge)
& fact('minute$u1$u1',real)
& etype('minute$u1$u1','etype$uc')
& card('minute$u1$u1','card$uc')
& sort('minute$u1$u1',ta)
& sort('minute$u1$u1',oa)
& sort('minute$u1$u1',me)
& varia(c5937,'varia$uc')
& refer(c5937,'refer$uc')
& quant(c5937,'quant$uc')
& gener(c5937,'gener$uc')
& fact(c5937,real)
& etype(c5937,'etype$uc')
& card(c5937,'card$uc')
& sort(c5937,ta)
& sort(c5937,oa)
& sort(c5937,me)
& varia('abstand$u1$u1','varia$uc')
& refer('abstand$u1$u1','refer$uc')
& quant('abstand$u1$u1',one)
& gener('abstand$u1$u1',ge)
& fact('abstand$u1$u1',real)
& etype('abstand$u1$u1',int0)
& card('abstand$u1$u1',int1)
& sort('abstand$u1$u1',na)
& sort('abstand$u1$u1',io)
& varia(c5932,con)
& refer(c5932,det)
& quant(c5932,one)
& gener(c5932,sp)
& fact(c5932,real)
& etype(c5932,int0)
& card(c5932,int1)
& sort(c5932,na)
& sort(c5932,io)
& varia('u3$u1$u1','varia$uc')
& refer('u3$u1$u1','refer$uc')
& quant('u3$u1$u1',one)
& gener('u3$u1$u1',ge)
& fact('u3$u1$u1',real)
& etype('u3$u1$u1',int0)
& card('u3$u1$u1',int1)
& sort('u3$u1$u1',o)
& varia(c5921,'varia$uc')
& refer(c5921,indet)
& quant(c5921,mult)
& gener(c5921,'gener$uc')
& fact(c5921,real)
& etype(c5921,int1)
& card(c5921,cons('x$uconstant',cons(int1,nil)))
& sort(c5921,o)
& sort('u2$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('einrichtung$u1$u2','varia$uc')
& refer('einrichtung$u1$u2','refer$uc')
& quant('einrichtung$u1$u2','quant$uc')
& gener('einrichtung$u1$u2',ge)
& fact('einrichtung$u1$u2',real)
& etype('einrichtung$u1$u2',int1)
& card('einrichtung$u1$u2','card$uc')
& sort('einrichtung$u1$u2',io)
& sort('einrichtung$u1$u2',d)
& varia(c5920,'varia$uc')
& refer(c5920,indet)
& quant(c5920,one)
& gener(c5920,sp)
& fact(c5920,real)
& etype(c5920,int0)
& card(c5920,int1)
& sort(c5920,na)
& varia(c5919,con)
& refer(c5919,det)
& quant(c5919,one)
& gener(c5919,sp)
& fact(c5919,real)
& etype(c5919,int1)
& card(c5919,int1)
& sort(c5919,io)
& sort(c5919,d)
& varia('u1$u1$u1','varia$uc')
& refer('u1$u1$u1','refer$uc')
& quant('u1$u1$u1',one)
& gener('u1$u1$u1',ge)
& fact('u1$u1$u1',real)
& etype('u1$u1$u1',int0)
& card('u1$u1$u1',int1)
& sort('u1$u1$u1',o)
& varia(c5912,'varia$uc')
& refer(c5912,indet)
& quant(c5912,mult)
& gener(c5912,'gener$uc')
& fact(c5912,real)
& etype(c5912,int1)
& card(c5912,cons('x$uconstant',cons(int1,nil)))
& sort(c5912,o)
& varia('linie$u1$u1','varia$uc')
& refer('linie$u1$u1','refer$uc')
& quant('linie$u1$u1',one)
& gener('linie$u1$u1',ge)
& fact('linie$u1$u1',real)
& etype('linie$u1$u1',int0)
& card('linie$u1$u1',int1)
& sort('linie$u1$u1',io)
& sort('linie$u1$u1',d)
& varia(c5910,'varia$uc')
& refer(c5910,indet)
& quant(c5910,mult)
& gener(c5910,'gener$uc')
& fact(c5910,real)
& etype(c5910,int1)
& card(c5910,cons('x$uconstant',cons(int1,nil)))
& sort(c5910,io)
& sort(c5910,d)
& varia('bahn$u1$u1','varia$uc')
& refer('bahn$u1$u1','refer$uc')
& quant('bahn$u1$u1',one)
& gener('bahn$u1$u1',ge)
& fact('bahn$u1$u1',real)
& etype('bahn$u1$u1',int0)
& card('bahn$u1$u1',int1)
& sort('bahn$u1$u1',io)
& varia(c5909,'varia$uc')
& refer(c5909,'refer$uc')
& quant(c5909,one)
& gener(c5909,'gener$uc')
& fact(c5909,real)
& etype(c5909,int0)
& card(c5909,int1)
& sort(c5909,io)
& 'tupl$up9'(c6138,c5901,c5909,c5910,c5912,c5919,c5921,c5932,c5937)
& pred(c5937,'minute$u1$u1')
& sub(c5932,'abstand$u1$u1')
& pred(c5921,'u3$u1$u1')
& val(c5920,'u2$u0')
& sub(c5920,'name$u1$u1')
& sub(c5919,'einrichtung$u1$u2')
& attr(c5919,c5920)
& pred(c5912,'u1$u1$u1')
& pred(c5910,'linie$u1$u1')
& sub(c5909,'bahn$u1$u1') ) ).
fof(member_first,axiom,
! [X0,X1] : member(X0,cons(X0,X1)) ).
fof(member_second,axiom,
! [X0,X1,X2] :
( member(X0,X2)
=> member(X0,cons(X1,X2)) ) ).
fof(attr_name_hei__337en_1_1,axiom,
! [X0,X1,X2] :
( ( sub(X0,X1)
& member(X1,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil))))
& attr(X2,X0) )
=> ? [X3] :
( subs(X3,'hei$u$u337en$u1$u1')
& arg2(X3,X2)
& arg1(X3,X2) ) ) ).
fof(synth_qa07_001_qapn_4,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7] :
( val(X6,'u2$u0')
& subs(X4,'hei$u$u337en$u1$u1')
& sub(X6,'name$u1$u1')
& sub(X1,'bahn$u1$u1')
& pred(X3,'u1$u1$u1')
& pred(X2,'linie$u1$u1')
& attr(X7,X6)
& arg2(X4,X0)
& arg1(X4,X5) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7] :
( val(X6,'u2$u0')
& subs(X4,'hei$u$u337en$u1$u1')
& sub(X6,'name$u1$u1')
& sub(X1,'bahn$u1$u1')
& pred(X3,'u1$u1$u1')
& pred(X2,'linie$u1$u1')
& attr(X7,X6)
& arg2(X4,X0)
& arg1(X4,X5) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_001_qapn_4]) ).
cnf(c0,plain,
sub(c5909,'bahn$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_001_qapn_4]) ).
cnf(c1,plain,
pred(c5910,'linie$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_001_qapn_4]) ).
cnf(c2,plain,
pred(c5912,'u1$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_001_qapn_4]) ).
cnf(c3,plain,
attr(c5919,c5920),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_001_qapn_4]) ).
cnf(c5,plain,
sub(c5920,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_001_qapn_4]) ).
cnf(c6,plain,
val(c5920,'u2$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_001_qapn_4]) ).
cnf(c166,plain,
member(X0,cons(X0,X1)),
inference(clausification,[status(esa)],[member_first]) ).
cnf(c167,plain,
( member(X0,cons(X2,X1))
| ~ member(X0,X1) ),
inference(clausification,[status(esa)],[member_second]) ).
cnf(c279,plain,
( arg1(sK172(X0),X0)
| ~ sub(X1,X2)
| ~ member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil))))
| ~ attr(X0,X1) ),
inference(clausification,[status(esa)],[attr_name_hei__337en_1_1]) ).
cnf(c280,plain,
( arg2(sK172(X0),X0)
| ~ sub(X1,X2)
| ~ member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil))))
| ~ attr(X0,X1) ),
inference(clausification,[status(esa)],[attr_name_hei__337en_1_1]) ).
cnf(c281,plain,
( subs(sK172(X0),'hei$u$u337en$u1$u1')
| ~ sub(X1,X2)
| ~ member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil))))
| ~ attr(X0,X1) ),
inference(clausification,[status(esa)],[attr_name_hei__337en_1_1]) ).
cnf(c322,plain,
( ~ val(X5,'u2$u0')
| ~ sub(X5,'name$u1$u1')
| ~ pred(X7,'linie$u1$u1')
| ~ subs(X1,'hei$u$u337en$u1$u1')
| ~ arg1(X1,X6)
| ~ attr(X4,X5)
| ~ sub(X3,'bahn$u1$u1')
| ~ arg2(X1,X2)
| ~ pred(X0,'u1$u1$u1') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ member(X1,cons('familiename$u1$u1',cons('name$u1$u1',nil)))
| arg1(sK172(X2),X2)
| ~ attr(X2,X0)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[c279,c167]) ).
cnf(d1,plain,
( ~ member(X1,cons('name$u1$u1',nil))
| arg1(sK172(X2),X2)
| ~ attr(X2,X0)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[d0,c167]) ).
cnf(d2,plain,
( arg1(sK172(X1),X1)
| ~ attr(X1,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d1,c166]) ).
cnf(d3,plain,
( arg1(sK172(c5919),c5919)
| ~ sub(c5920,'name$u1$u1') ),
inference(resolution,[status(thm)],[d2,c3]) ).
cnf(d4,plain,
arg1(sK172(c5919),c5919),
inference(resolution,[status(thm)],[c5,d3]) ).
cnf(d5,plain,
( ~ member(X1,cons('familiename$u1$u1',cons('name$u1$u1',nil)))
| arg2(sK172(X2),X2)
| ~ attr(X2,X0)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[c280,c167]) ).
cnf(d6,plain,
( ~ member(X1,cons('name$u1$u1',nil))
| arg2(sK172(X2),X2)
| ~ attr(X2,X0)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[d5,c167]) ).
cnf(d7,plain,
( arg2(sK172(X1),X1)
| ~ attr(X1,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d6,c166]) ).
cnf(d8,plain,
( arg2(sK172(c5919),c5919)
| ~ sub(c5920,'name$u1$u1') ),
inference(resolution,[status(thm)],[d7,c3]) ).
cnf(d9,plain,
arg2(sK172(c5919),c5919),
inference(resolution,[status(thm)],[c5,d8]) ).
cnf(d10,plain,
( ~ arg1(sK172(c5919),X5)
| ~ subs(sK172(c5919),'hei$u$u337en$u1$u1')
| ~ val(X0,'u2$u0')
| ~ attr(X4,X0)
| ~ pred(X3,'u1$u1$u1')
| ~ pred(X2,'linie$u1$u1')
| ~ sub(X1,'bahn$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d9,c322]) ).
cnf(d11,plain,
( ~ subs(sK172(c5919),'hei$u$u337en$u1$u1')
| ~ val(X1,'u2$u0')
| ~ attr(X4,X1)
| ~ pred(X3,'linie$u1$u1')
| ~ pred(X2,'u1$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'bahn$u1$u1') ),
inference(resolution,[status(thm)],[d10,d4]) ).
cnf(d12,plain,
( ~ member(X1,cons('familiename$u1$u1',cons('name$u1$u1',nil)))
| subs(sK172(X2),'hei$u$u337en$u1$u1')
| ~ attr(X2,X0)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[c281,c167]) ).
cnf(d13,plain,
( ~ member(X1,cons('name$u1$u1',nil))
| subs(sK172(X2),'hei$u$u337en$u1$u1')
| ~ attr(X2,X0)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[d12,c167]) ).
cnf(d14,plain,
( subs(sK172(X1),'hei$u$u337en$u1$u1')
| ~ attr(X1,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d13,c166]) ).
cnf(d15,plain,
( subs(sK172(c5919),'hei$u$u337en$u1$u1')
| ~ sub(c5920,'name$u1$u1') ),
inference(resolution,[status(thm)],[d14,c3]) ).
cnf(d16,plain,
subs(sK172(c5919),'hei$u$u337en$u1$u1'),
inference(resolution,[status(thm)],[c5,d15]) ).
cnf(d17,plain,
( ~ val(X0,'u2$u0')
| ~ attr(X4,X0)
| ~ pred(X3,'u1$u1$u1')
| ~ pred(X2,'linie$u1$u1')
| ~ sub(X1,'bahn$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d16,d11]) ).
cnf(d18,plain,
( ~ attr(X3,c5920)
| ~ pred(X2,'linie$u1$u1')
| ~ pred(X1,'u1$u1$u1')
| ~ sub(c5920,'name$u1$u1')
| ~ sub(X0,'bahn$u1$u1') ),
inference(resolution,[status(thm)],[d17,c6]) ).
cnf(d19,plain,
( ~ attr(X3,c5920)
| ~ pred(X2,'u1$u1$u1')
| ~ pred(X1,'linie$u1$u1')
| ~ sub(X0,'bahn$u1$u1') ),
inference(resolution,[status(thm)],[c5,d18]) ).
cnf(d20,plain,
( ~ pred(X2,'linie$u1$u1')
| ~ pred(X1,'u1$u1$u1')
| ~ sub(X0,'bahn$u1$u1') ),
inference(resolution,[status(thm)],[d19,c3]) ).
cnf(d21,plain,
( ~ pred(X1,'linie$u1$u1')
| ~ sub(X0,'bahn$u1$u1') ),
inference(resolution,[status(thm)],[d20,c2]) ).
cnf(d22,plain,
~ sub(X0,'bahn$u1$u1'),
inference(resolution,[status(thm)],[d21,c1]) ).
cnf(d23,plain,
$false,
inference(resolution,[status(thm)],[d22,c0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR112+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 01:03:53 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 70.13/9.19 % SZS status Theorem for theBenchmark.p
% 70.13/9.19 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------