%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+82 : 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 : n020.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:49 AM UTC 2026
% Result : Theorem 42.64s 5.62s
% Output : CNFRefutation 42.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 3
% Syntax : Number of formulae : 16 ( 4 unt; 0 def)
% Number of atoms : 147 ( 0 equ)
% Maximal formula atoms : 101 ( 9 avg)
% Number of connectives : 159 ( 28 ~; 20 |; 110 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 11 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 19 ( 18 usr; 1 prp; 0-2 aty)
% Number of functors : 34 ( 34 usr; 33 con; 0-2 aty)
% Number of variables : 53 ( 21 sgn 2 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_007_mira_wp_495,hypothesis,
( gener('einl$u$u344uten$u1$u1',ge)
& fact('einl$u$u344uten$u1$u1',real)
& sort('einl$u$u344uten$u1$u1',dn)
& varia(c373,con)
& refer(c373,det)
& quant(c373,one)
& gener(c373,sp)
& fact(c373,real)
& etype(c373,int0)
& card(c373,int1)
& sort(c373,l)
& gener(c368,sp)
& fact(c368,real)
& sort(c368,dn)
& varia('bereich$u1$u1','varia$uc')
& refer('bereich$u1$u1','refer$uc')
& quant('bereich$u1$u1',one)
& gener('bereich$u1$u1',ge)
& fact('bereich$u1$u1',real)
& etype('bereich$u1$u1',int0)
& card('bereich$u1$u1',int1)
& sort('bereich$u1$u1',d)
& varia(c364,'varia$uc')
& refer(c364,'refer$uc')
& quant(c364,one)
& gener(c364,sp)
& fact(c364,real)
& etype(c364,int0)
& card(c364,int1)
& sort(c364,d)
& varia('mountain$ubike$u1$u1','varia$uc')
& refer('mountain$ubike$u1$u1','refer$uc')
& quant('mountain$ubike$u1$u1',one)
& gener('mountain$ubike$u1$u1',ge)
& fact('mountain$ubike$u1$u1',real)
& etype('mountain$ubike$u1$u1',int0)
& card('mountain$ubike$u1$u1',int1)
& sort('mountain$ubike$u1$u1',d)
& varia(c362,con)
& refer(c362,det)
& quant(c362,one)
& gener(c362,sp)
& fact(c362,real)
& etype(c362,int0)
& card(c362,int1)
& sort(c362,d)
& sort('freeride$u$u$u$u$u344ra$u0',fe)
& varia(c358,'varia$uc')
& refer(c358,'refer$uc')
& quant(c358,one)
& gener(c358,sp)
& fact(c358,hypo)
& etype(c358,int0)
& card(c358,int1)
& sort(c358,o)
& sort('marzocchi$u0',fe)
& varia('familiename$u1$u1','varia$uc')
& refer('familiename$u1$u1','refer$uc')
& quant('familiename$u1$u1',one)
& gener('familiename$u1$u1',ge)
& fact('familiename$u1$u1',real)
& etype('familiename$u1$u1',int0)
& card('familiename$u1$u1',int1)
& sort('familiename$u1$u1',na)
& varia('mensch$u1$u1','varia$uc')
& refer('mensch$u1$u1','refer$uc')
& quant('mensch$u1$u1',one)
& gener('mensch$u1$u1',ge)
& fact('mensch$u1$u1',real)
& etype('mensch$u1$u1',int0)
& card('mensch$u1$u1',int1)
& sort('mensch$u1$u1',d)
& varia(c342,'varia$uc')
& refer(c342,indet)
& quant(c342,one)
& gener(c342,sp)
& fact(c342,real)
& etype(c342,int0)
& card(c342,int1)
& sort(c342,na)
& varia(c341,con)
& refer(c341,det)
& quant(c341,one)
& gener(c341,sp)
& fact(c341,real)
& etype(c341,int0)
& card(c341,int1)
& sort(c341,d)
& in(c373,c362)
& subs(c368,'einl$u$u344uten$u1$u1')
& mcont(c368,c358)
& loc(c368,c373)
& exp(c368,c341)
& benf(c368,c364)
& sub(c364,'bereich$u1$u1')
& sub(c362,'mountain$ubike$u1$u1')
& name(c358,'freeride$u$u$u$u$u344ra$u0')
& val(c342,'marzocchi$u0')
& sub(c342,'familiename$u1$u1')
& sub(c341,'mensch$u1$u1')
& attr(c341,c342) ) ).
fof(name_rel__attr_val_name_1_1,axiom,
! [X0,X1] :
( name(X1,X0)
=> ? [X2] :
( val(X2,X0)
& sub(X2,'name$u1$u1')
& attr(X1,X2) ) ) ).
fof(synth_qa07_007_mira_wp_495,conjecture,
? [X0,X1,X2,X3,X4,X5] :
( sub(X2,'name$u1$u1')
& sub(X1,'name$u1$u1')
& attr(X4,X5)
& attr(X3,X2)
& attr(X0,X1) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5] :
( sub(X2,'name$u1$u1')
& sub(X1,'name$u1$u1')
& attr(X4,X5)
& attr(X3,X2)
& attr(X0,X1) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_007_mira_wp_495]) ).
cnf(c0,plain,
attr(c341,c342),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_495]) ).
cnf(c4,plain,
name(c358,'freeride$u$u$u$u$u344ra$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_495]) ).
cnf(c455,plain,
( attr(X0,sK471(X1,X0))
| ~ name(X0,X1) ),
inference(clausification,[status(esa)],[name_rel__attr_val_name_1_1]) ).
cnf(c456,plain,
( sub(sK471(X1,X0),'name$u1$u1')
| ~ name(X0,X1) ),
inference(clausification,[status(esa)],[name_rel__attr_val_name_1_1]) ).
cnf(c10472,plain,
( ~ attr(X4,X5)
| ~ attr(X3,X0)
| ~ sub(X2,'name$u1$u1')
| ~ attr(X1,X2)
| ~ sub(X0,'name$u1$u1') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ sub(X3,'name$u1$u1')
| ~ attr(X6,sK471(X1,X0))
| ~ attr(X4,X5)
| ~ attr(X2,X3)
| ~ name(X0,X1) ),
inference(resolution,[status(thm)],[c456,c10472]) ).
cnf(d1,plain,
( ~ name(X4,X5)
| ~ name(X4,X5)
| ~ sub(X3,'name$u1$u1')
| ~ attr(X2,X3)
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[d0,c455]) ).
cnf(d2,plain,
( ~ sub(X1,'name$u1$u1')
| ~ attr(X2,X3)
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[d1,c4]) ).
cnf(d3,plain,
( ~ name(X4,X3)
| ~ attr(X2,sK471(X3,X4))
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[d2,c456]) ).
cnf(d4,plain,
( ~ name(X2,X3)
| ~ name(X2,X3)
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[d3,c455]) ).
cnf(d5,plain,
~ attr(X0,X1),
inference(resolution,[status(thm)],[d4,c4]) ).
cnf(d6,plain,
$false,
inference(resolution,[status(thm)],[d5,c0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+82 : 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.10/0.35 % Computer : n020.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 27 01:13:04 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.64/5.62 % SZS status Theorem for theBenchmark.p
% 42.64/5.62 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------