%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : NLP208+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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 08:05:51 AM UTC 2026
% Result : Theorem 14.35s 2.40s
% Output : CNFRefutation 14.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 9
% Syntax : Number of formulae : 31 ( 13 unt; 0 def)
% Number of atoms : 141 ( 3 equ)
% Maximal formula atoms : 48 ( 4 avg)
% Number of connectives : 125 ( 15 ~; 8 |; 84 &)
% ( 0 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 51 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 44 ( 42 usr; 1 prp; 0-4 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 74 ( 2 sgn 28 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax24,axiom,
! [X0,X1] :
( man(X0,X1)
=> male(X0,X1) ) ).
fof(ax38,axiom,
! [X0,X1] :
( object(X0,X1)
=> unisex(X0,X1) ) ).
fof(ax45,axiom,
! [X0,X1] :
( artifact(X0,X1)
=> object(X0,X1) ) ).
fof(ax46,axiom,
! [X0,X1] :
( instrumentality(X0,X1)
=> artifact(X0,X1) ) ).
fof(ax47,axiom,
! [X0,X1] :
( device(X0,X1)
=> instrumentality(X0,X1) ) ).
fof(ax48,axiom,
! [X0,X1] :
( wheel(X0,X1)
=> device(X0,X1) ) ).
fof(ax63,axiom,
! [X0,X1] :
( unisex(X0,X1)
=> ~ male(X0,X1) ) ).
fof(ax71,axiom,
! [X0,X1,X2,X3] :
( be(X0,X1,X2,X3)
=> X2 = X3 ) ).
fof(co1,conjecture,
~ ? [X0] :
( ? [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( behind(X0,X10,X10)
& be(X0,X9,X1,X10)
& state(X0,X9)
& wheel(X0,X10)
& ! [X18] :
( member(X0,X18,X8)
=> ( cheap(X0,X18)
& black(X0,X18)
& coat(X0,X18) ) )
& group(X0,X8)
& ! [X15] :
( member(X0,X15,X8)
=> ! [X16] :
( member(X0,X16,X7)
=> ? [X17] :
( wear(X0,X17)
& nonreflexive(X0,X17)
& present(X0,X17)
& patient(X0,X17,X15)
& agent(X0,X17,X16)
& event(X0,X17) ) ) )
& ! [X14] :
( member(X0,X14,X7)
=> ( young(X0,X14)
& fellow(X0,X14) ) )
& group(X0,X7)
& two(X0,X7)
& ! [X11] :
( member(X0,X11,X7)
=> ? [X12,X13] :
( in(X0,X13,X5)
& be(X0,X12,X11,X13)
& state(X0,X12) ) )
& in(X0,X6,X5)
& down(X0,X6,X5)
& barrel(X0,X6)
& present(X0,X6)
& agent(X0,X6,X3)
& event(X0,X6)
& lonely(X0,X5)
& street(X0,X5)
& placename(X0,X4)
& 'hollywood$uplacename'(X0,X4)
& city(X0,X5)
& of(X0,X4,X5)
& old(X0,X3)
& dirty(X0,X3)
& white(X0,X3)
& chevy(X0,X3)
& frontseat(X0,X5)
& forename(X0,X2)
& 'jules$uforename'(X0,X2)
& man(X0,X1)
& of(X0,X2,X1) )
& 'actual$uworld'(X0) ) ).
fof(negated_conjecture,negated_conjecture,
~ ~ ? [X0] :
( ? [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( behind(X0,X10,X10)
& be(X0,X9,X1,X10)
& state(X0,X9)
& wheel(X0,X10)
& ! [X18] :
( member(X0,X18,X8)
=> ( cheap(X0,X18)
& black(X0,X18)
& coat(X0,X18) ) )
& group(X0,X8)
& ! [X15] :
( member(X0,X15,X8)
=> ! [X16] :
( member(X0,X16,X7)
=> ? [X17] :
( wear(X0,X17)
& nonreflexive(X0,X17)
& present(X0,X17)
& patient(X0,X17,X15)
& agent(X0,X17,X16)
& event(X0,X17) ) ) )
& ! [X14] :
( member(X0,X14,X7)
=> ( young(X0,X14)
& fellow(X0,X14) ) )
& group(X0,X7)
& two(X0,X7)
& ! [X11] :
( member(X0,X11,X7)
=> ? [X12,X13] :
( in(X0,X13,X5)
& be(X0,X12,X11,X13)
& state(X0,X12) ) )
& in(X0,X6,X5)
& down(X0,X6,X5)
& barrel(X0,X6)
& present(X0,X6)
& agent(X0,X6,X3)
& event(X0,X6)
& lonely(X0,X5)
& street(X0,X5)
& placename(X0,X4)
& 'hollywood$uplacename'(X0,X4)
& city(X0,X5)
& of(X0,X4,X5)
& old(X0,X3)
& dirty(X0,X3)
& white(X0,X3)
& chevy(X0,X3)
& frontseat(X0,X5)
& forename(X0,X2)
& 'jules$uforename'(X0,X2)
& man(X0,X1)
& of(X0,X2,X1) )
& 'actual$uworld'(X0) ),
inference(negate_conjecture,[status(cth)],[co1]) ).
cnf(c23,plain,
( male(X0,X1)
| ~ man(X0,X1) ),
inference(clausification,[status(esa)],[ax24]) ).
cnf(c37,plain,
( unisex(X0,X1)
| ~ object(X0,X1) ),
inference(clausification,[status(esa)],[ax38]) ).
cnf(c44,plain,
( object(X0,X1)
| ~ artifact(X0,X1) ),
inference(clausification,[status(esa)],[ax45]) ).
cnf(c45,plain,
( artifact(X0,X1)
| ~ instrumentality(X0,X1) ),
inference(clausification,[status(esa)],[ax46]) ).
cnf(c46,plain,
( instrumentality(X0,X1)
| ~ device(X0,X1) ),
inference(clausification,[status(esa)],[ax47]) ).
cnf(c47,plain,
( device(X0,X1)
| ~ wheel(X0,X1) ),
inference(clausification,[status(esa)],[ax48]) ).
cnf(c62,plain,
( ~ male(X0,X1)
| ~ unisex(X0,X1) ),
inference(clausification,[status(esa)],[ax63]) ).
cnf(c78,plain,
( X2 = X3
| ~ be(X0,X1,X2,X3) ),
inference(clausification,[status(esa)],[ax71]) ).
cnf(c81,plain,
man(sK158,sK159),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c113,plain,
wheel(sK158,sK168),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c115,plain,
be(sK158,sK167,sK159,sK168),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
device(sK158,sK168),
inference(resolution,[status(thm)],[c47,c113]) ).
cnf(d1,plain,
instrumentality(sK158,sK168),
inference(resolution,[status(thm)],[d0,c46]) ).
cnf(d2,plain,
artifact(sK158,sK168),
inference(resolution,[status(thm)],[d1,c45]) ).
cnf(d3,plain,
object(sK158,sK168),
inference(resolution,[status(thm)],[d2,c44]) ).
cnf(d4,plain,
unisex(sK158,sK168),
inference(resolution,[status(thm)],[d3,c37]) ).
cnf(d5,plain,
sK159 = sK168,
inference(resolution,[status(thm)],[c115,c78]) ).
cnf(d6,plain,
male(sK158,sK159),
inference(resolution,[status(thm)],[c23,c81]) ).
cnf(d7,plain,
~ unisex(sK158,sK159),
inference(resolution,[status(thm)],[c62,d6]) ).
cnf(d8,plain,
~ unisex(sK158,sK168),
inference(demodulation,[status(thm)],[d7,d5]) ).
cnf(d9,plain,
$false,
inference(resolution,[status(thm)],[d8,d4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP208+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n005.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 : Sat Sep 26 01:25:17 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.35/2.40 % SZS status Theorem for theBenchmark.p
% 14.35/2.40 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------