%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NLP007-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.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 : Fri Sep 25 02:14:27 PM UTC 2026
% Result : Unsatisfiable 5.27s 1.16s
% Output : Proof 5.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 86
% Number of leaves : 60
% Syntax : Number of formulae : 326 ( 72 unt; 0 def)
% Number of atoms : 1856 ( 94 equ)
% Maximal formula atoms : 30 ( 5 avg)
% Number of connectives : 2913 (1383 ~;1530 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 39 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 2 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 16 con; 0-0 aty)
% Number of variables : 325 ( 0 sgn 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f58,negated_conjecture,
( X1 = Z
| ssSkC0
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ young(Z)
| ~ man(Z)
| ~ fellow(Z)
| ~ in(Z,Y)
| ~ front(Y)
| ~ furniture(Y)
| ~ seat(Y)
| ~ in(W,X)
| ~ city(X)
| ~ hollywood(X)
| ~ event(W)
| ~ barrel(W,V)
| ~ down(W,U)
| ~ old(V)
| ~ dirty(V)
| ~ white(V)
| ~ car(V)
| ~ chevy(V)
| ~ street(U)
| ~ way(U)
| ~ lonely(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
fof(f58_nnf,plain,
! [U,V,W,X,Y,Z,X1,X2] :
( X1 = Z
| ssSkC0
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ young(Z)
| ~ man(Z)
| ~ fellow(Z)
| ~ in(Z,Y)
| ~ front(Y)
| ~ furniture(Y)
| ~ seat(Y)
| ~ in(W,X)
| ~ city(X)
| ~ hollywood(X)
| ~ event(W)
| ~ barrel(W,V)
| ~ down(W,U)
| ~ old(V)
| ~ dirty(V)
| ~ white(V)
| ~ car(V)
| ~ chevy(V)
| ~ street(U)
| ~ way(U)
| ~ lonely(U) ),
inference(nnf_transformation,[status(thm)],[f58]) ).
fof(f58_sk,plain,
! [U,V,W,X,Y,Z,X1,X2] :
( X1 = Z
| ssSkC0
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ young(Z)
| ~ man(Z)
| ~ fellow(Z)
| ~ in(Z,Y)
| ~ front(Y)
| ~ furniture(Y)
| ~ seat(Y)
| ~ in(W,X)
| ~ city(X)
| ~ hollywood(X)
| ~ event(W)
| ~ barrel(W,V)
| ~ down(W,U)
| ~ old(V)
| ~ dirty(V)
| ~ white(V)
| ~ car(V)
| ~ chevy(V)
| ~ street(U)
| ~ way(U)
| ~ lonely(U) ),
inference(skolemisation,[status(esa)],[f58_nnf]) ).
cnf(c58,plain,
( X6 = X5
| ssSkC0
| ~ fellow(X6)
| ~ man(X6)
| ~ young(X6)
| ~ seat(X7)
| ~ furniture(X7)
| ~ front(X7)
| ~ in(X6,X7)
| ~ young(X5)
| ~ man(X5)
| ~ fellow(X5)
| ~ in(X5,X4)
| ~ front(X4)
| ~ furniture(X4)
| ~ seat(X4)
| ~ in(X2,X3)
| ~ city(X3)
| ~ hollywood(X3)
| ~ event(X2)
| ~ barrel(X2,X1)
| ~ down(X2,X0)
| ~ old(X1)
| ~ dirty(X1)
| ~ white(X1)
| ~ car(X1)
| ~ chevy(X1)
| ~ street(X0)
| ~ way(X0)
| ~ lonely(X0) ),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(f16,negated_conjecture,
( lonely(skc28)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
fof(f16_nnf,plain,
( lonely(skc28)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
( lonely(skc28)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( lonely(skc28)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p65,plain,
( ssSkC0
| X5 = X4
| ssSkC0
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| ~ seat(X6)
| ~ furniture(X6)
| ~ front(X6)
| ~ in(X5,X6)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ in(X4,X3)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X1,X2)
| ~ city(X2)
| ~ hollywood(X2)
| ~ event(X1)
| ~ barrel(X1,X0)
| ~ down(X1,skc28)
| ~ old(X0)
| ~ dirty(X0)
| ~ white(X0)
| ~ car(X0)
| ~ chevy(X0)
| ~ street(skc28)
| ~ way(skc28) ),
inference(resolution,[status(thm)],[c58,c16]) ).
cnf(p96,plain,
( X5 = X4
| ssSkC0
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| ~ seat(X6)
| ~ furniture(X6)
| ~ front(X6)
| ~ in(X5,X6)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ in(X4,X3)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X1,X2)
| ~ city(X2)
| ~ hollywood(X2)
| ~ event(X1)
| ~ barrel(X1,X0)
| ~ down(X1,skc28)
| ~ old(X0)
| ~ dirty(X0)
| ~ white(X0)
| ~ car(X0)
| ~ chevy(X0)
| ~ street(skc28)
| ~ way(skc28) ),
inference(factoring,[status(thm)],[p65]) ).
cnf(f17,negated_conjecture,
( way(skc28)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
fof(f17_nnf,plain,
( way(skc28)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
( way(skc28)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( way(skc28)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p145,plain,
( ssSkC0
| X5 = X4
| ssSkC0
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| ~ seat(X6)
| ~ furniture(X6)
| ~ front(X6)
| ~ in(X5,X6)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ in(X4,X3)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X1,X2)
| ~ city(X2)
| ~ hollywood(X2)
| ~ event(X1)
| ~ barrel(X1,X0)
| ~ down(X1,skc28)
| ~ old(X0)
| ~ dirty(X0)
| ~ white(X0)
| ~ car(X0)
| ~ chevy(X0)
| ~ street(skc28) ),
inference(resolution,[status(thm)],[p96,c17]) ).
cnf(p174,plain,
( X5 = X4
| ssSkC0
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| ~ seat(X6)
| ~ furniture(X6)
| ~ front(X6)
| ~ in(X5,X6)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ in(X4,X3)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X1,X2)
| ~ city(X2)
| ~ hollywood(X2)
| ~ event(X1)
| ~ barrel(X1,X0)
| ~ down(X1,skc28)
| ~ old(X0)
| ~ dirty(X0)
| ~ white(X0)
| ~ car(X0)
| ~ chevy(X0)
| ~ street(skc28) ),
inference(factoring,[status(thm)],[p145]) ).
cnf(f3,negated_conjecture,
street(skc28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
fof(f3_nnf,plain,
street(skc28),
inference(nnf_transformation,[status(thm)],[f3]) ).
cnf(c3,plain,
street(skc28),
inference(cnf_transformation,[status(esa)],[f3_nnf]) ).
cnf(p195,plain,
( X5 = X4
| ssSkC0
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| ~ seat(X6)
| ~ furniture(X6)
| ~ front(X6)
| ~ in(X5,X6)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ in(X4,X3)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X1,X2)
| ~ city(X2)
| ~ hollywood(X2)
| ~ event(X1)
| ~ barrel(X1,X0)
| ~ down(X1,skc28)
| ~ old(X0)
| ~ dirty(X0)
| ~ white(X0)
| ~ car(X0)
| ~ chevy(X0) ),
inference(resolution,[status(thm)],[p174,c3]) ).
cnf(f18,negated_conjecture,
( chevy(skc29)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
fof(f18_nnf,plain,
( chevy(skc29)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
( chevy(skc29)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( chevy(skc29)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p213,plain,
( ssSkC0
| X4 = X3
| ssSkC0
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ in(X3,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc29)
| ~ down(X0,skc28)
| ~ old(skc29)
| ~ dirty(skc29)
| ~ white(skc29)
| ~ car(skc29) ),
inference(resolution,[status(thm)],[p195,c18]) ).
cnf(p227,plain,
( X4 = X3
| ssSkC0
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ in(X3,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc29)
| ~ down(X0,skc28)
| ~ old(skc29)
| ~ dirty(skc29)
| ~ white(skc29)
| ~ car(skc29) ),
inference(factoring,[status(thm)],[p213]) ).
cnf(f19,negated_conjecture,
( car(skc29)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
fof(f19_nnf,plain,
( car(skc29)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
( car(skc29)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( car(skc29)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p237,plain,
( ssSkC0
| X4 = X3
| ssSkC0
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ in(X3,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc29)
| ~ down(X0,skc28)
| ~ old(skc29)
| ~ dirty(skc29)
| ~ white(skc29) ),
inference(resolution,[status(thm)],[p227,c19]) ).
cnf(p246,plain,
( X4 = X3
| ssSkC0
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ in(X3,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc29)
| ~ down(X0,skc28)
| ~ old(skc29)
| ~ dirty(skc29)
| ~ white(skc29) ),
inference(factoring,[status(thm)],[p237]) ).
cnf(f20,negated_conjecture,
( white(skc29)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
fof(f20_nnf,plain,
( white(skc29)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
( white(skc29)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( white(skc29)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p251,plain,
( ssSkC0
| X4 = X3
| ssSkC0
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ in(X3,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc29)
| ~ down(X0,skc28)
| ~ old(skc29)
| ~ dirty(skc29) ),
inference(resolution,[status(thm)],[p246,c20]) ).
cnf(p256,plain,
( X4 = X3
| ssSkC0
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ in(X3,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc29)
| ~ down(X0,skc28)
| ~ old(skc29)
| ~ dirty(skc29) ),
inference(factoring,[status(thm)],[p251]) ).
cnf(f21,negated_conjecture,
( dirty(skc29)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
fof(f21_nnf,plain,
( dirty(skc29)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
( dirty(skc29)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( dirty(skc29)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p261,plain,
( ssSkC0
| X4 = X3
| ssSkC0
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ in(X3,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc29)
| ~ down(X0,skc28)
| ~ old(skc29) ),
inference(resolution,[status(thm)],[p256,c21]) ).
cnf(p268,plain,
( X4 = X3
| ssSkC0
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ in(X3,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc29)
| ~ down(X0,skc28)
| ~ old(skc29) ),
inference(factoring,[status(thm)],[p261]) ).
cnf(f2,negated_conjecture,
old(skc29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
fof(f2_nnf,plain,
old(skc29),
inference(nnf_transformation,[status(thm)],[f2]) ).
cnf(c2,plain,
old(skc29),
inference(cnf_transformation,[status(esa)],[f2_nnf]) ).
cnf(p281,plain,
( X4 = X3
| ssSkC0
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ in(X3,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc29)
| ~ down(X0,skc28) ),
inference(resolution,[status(thm)],[p268,c2]) ).
cnf(f46,negated_conjecture,
( down(skc30,skc28)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
fof(f46_nnf,plain,
( down(skc30,skc28)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
( down(skc30,skc28)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c46,plain,
( down(skc30,skc28)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(p286,plain,
( ssSkC0
| X3 = X2
| ssSkC0
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ in(X2,X1)
| ~ front(X1)
| ~ furniture(X1)
| ~ seat(X1)
| ~ in(skc30,X0)
| ~ city(X0)
| ~ hollywood(X0)
| ~ event(skc30)
| ~ barrel(skc30,skc29) ),
inference(resolution,[status(thm)],[p281,c46]) ).
cnf(p291,plain,
( X3 = X2
| ssSkC0
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ in(X2,X1)
| ~ front(X1)
| ~ furniture(X1)
| ~ seat(X1)
| ~ in(skc30,X0)
| ~ city(X0)
| ~ hollywood(X0)
| ~ event(skc30)
| ~ barrel(skc30,skc29) ),
inference(factoring,[status(thm)],[p286]) ).
cnf(f47,negated_conjecture,
( barrel(skc30,skc29)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
fof(f47_nnf,plain,
( barrel(skc30,skc29)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
( barrel(skc30,skc29)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c47,plain,
( barrel(skc30,skc29)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p294,plain,
( ssSkC0
| X3 = X2
| ssSkC0
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ in(X2,X1)
| ~ front(X1)
| ~ furniture(X1)
| ~ seat(X1)
| ~ in(skc30,X0)
| ~ city(X0)
| ~ hollywood(X0)
| ~ event(skc30) ),
inference(resolution,[status(thm)],[p291,c47]) ).
cnf(p295,plain,
( X3 = X2
| ssSkC0
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ in(X2,X1)
| ~ front(X1)
| ~ furniture(X1)
| ~ seat(X1)
| ~ in(skc30,X0)
| ~ city(X0)
| ~ hollywood(X0)
| ~ event(skc30) ),
inference(factoring,[status(thm)],[p294]) ).
cnf(f1,negated_conjecture,
event(skc30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
fof(f1_nnf,plain,
event(skc30),
inference(nnf_transformation,[status(thm)],[f1]) ).
cnf(c1,plain,
event(skc30),
inference(cnf_transformation,[status(esa)],[f1_nnf]) ).
cnf(p296,plain,
( X3 = X2
| ssSkC0
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ in(X2,X1)
| ~ front(X1)
| ~ furniture(X1)
| ~ seat(X1)
| ~ in(skc30,X0)
| ~ city(X0)
| ~ hollywood(X0) ),
inference(resolution,[status(thm)],[p295,c1]) ).
cnf(f22,negated_conjecture,
( hollywood(skc31)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
fof(f22_nnf,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p297,plain,
( ssSkC0
| X2 = X1
| ssSkC0
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ in(X1,X0)
| ~ front(X0)
| ~ furniture(X0)
| ~ seat(X0)
| ~ in(skc30,skc31)
| ~ city(skc31) ),
inference(resolution,[status(thm)],[p296,c22]) ).
cnf(p298,plain,
( X2 = X1
| ssSkC0
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ in(X1,X0)
| ~ front(X0)
| ~ furniture(X0)
| ~ seat(X0)
| ~ in(skc30,skc31)
| ~ city(skc31) ),
inference(factoring,[status(thm)],[p297]) ).
cnf(f0,negated_conjecture,
city(skc31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
fof(f0_nnf,plain,
city(skc31),
inference(nnf_transformation,[status(thm)],[f0]) ).
cnf(c0,plain,
city(skc31),
inference(cnf_transformation,[status(esa)],[f0_nnf]) ).
cnf(p299,plain,
( X2 = X1
| ssSkC0
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ in(X1,X0)
| ~ front(X0)
| ~ furniture(X0)
| ~ seat(X0)
| ~ in(skc30,skc31) ),
inference(resolution,[status(thm)],[p298,c0]) ).
cnf(f48,negated_conjecture,
( in(skc30,skc31)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
fof(f48_nnf,plain,
( in(skc30,skc31)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
( in(skc30,skc31)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c48,plain,
( in(skc30,skc31)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p300,plain,
( ssSkC0
| X2 = X1
| ssSkC0
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ in(X1,X0)
| ~ front(X0)
| ~ furniture(X0)
| ~ seat(X0) ),
inference(resolution,[status(thm)],[p299,c48]) ).
cnf(p301,plain,
( X2 = X1
| ssSkC0
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ in(X1,X0)
| ~ front(X0)
| ~ furniture(X0)
| ~ seat(X0) ),
inference(factoring,[status(thm)],[p300]) ).
cnf(f4,negated_conjecture,
seat(skc27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
fof(f4_nnf,plain,
seat(skc27),
inference(nnf_transformation,[status(thm)],[f4]) ).
cnf(c4,plain,
seat(skc27),
inference(cnf_transformation,[status(esa)],[f4_nnf]) ).
cnf(p302,plain,
( X1 = X0
| ssSkC0
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ in(X0,skc27)
| ~ front(skc27)
| ~ furniture(skc27) ),
inference(resolution,[status(thm)],[p301,c4]) ).
cnf(f26,negated_conjecture,
( furniture(skc27)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
fof(f26_nnf,plain,
( furniture(skc27)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
( furniture(skc27)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( furniture(skc27)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p305,plain,
( ssSkC0
| X1 = X0
| ssSkC0
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ in(X0,skc27)
| ~ front(skc27) ),
inference(resolution,[status(thm)],[p302,c26]) ).
cnf(p306,plain,
( X1 = X0
| ssSkC0
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ in(X0,skc27)
| ~ front(skc27) ),
inference(factoring,[status(thm)],[p305]) ).
cnf(f25,negated_conjecture,
( front(skc27)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
fof(f25_nnf,plain,
( front(skc27)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
( front(skc27)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
( front(skc27)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p307,plain,
( ssSkC0
| X1 = X0
| ssSkC0
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ in(X0,skc27) ),
inference(resolution,[status(thm)],[p306,c25]) ).
cnf(p308,plain,
( X1 = X0
| ssSkC0
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ in(X0,skc27) ),
inference(factoring,[status(thm)],[p307]) ).
cnf(f49,negated_conjecture,
( in(skc24,skc27)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
fof(f49_nnf,plain,
( in(skc24,skc27)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
( in(skc24,skc27)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c49,plain,
( in(skc24,skc27)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(p309,plain,
( ssSkC0
| X0 = skc24
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24) ),
inference(resolution,[status(thm)],[p308,c49]) ).
cnf(p310,plain,
( X0 = skc24
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24) ),
inference(factoring,[status(thm)],[p309]) ).
cnf(f23,negated_conjecture,
( fellow(skc24)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
fof(f23_nnf,plain,
( fellow(skc24)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
( fellow(skc24)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( fellow(skc24)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p312,plain,
( ssSkC0
| X0 = skc24
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc24)
| ~ man(skc24) ),
inference(resolution,[status(thm)],[p310,c23]) ).
cnf(p313,plain,
( X0 = skc24
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc24)
| ~ man(skc24) ),
inference(factoring,[status(thm)],[p312]) ).
cnf(f24,negated_conjecture,
( man(skc24)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
fof(f24_nnf,plain,
( man(skc24)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
( man(skc24)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( man(skc24)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p314,plain,
( ssSkC0
| X0 = skc24
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc24) ),
inference(resolution,[status(thm)],[p313,c24]) ).
cnf(p315,plain,
( X0 = skc24
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc24) ),
inference(factoring,[status(thm)],[p314]) ).
cnf(f7,negated_conjecture,
young(skc24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
fof(f7_nnf,plain,
young(skc24),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
young(skc24),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(p317,plain,
( X0 = skc24
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[p315,c7]) ).
cnf(f50,negated_conjecture,
( in(skc25,skc26)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
fof(f50_nnf,plain,
( in(skc25,skc26)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
( in(skc25,skc26)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c50,plain,
( in(skc25,skc26)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(p318,plain,
( ssSkC0
| skc25 = skc24
| ssSkC0
| ~ fellow(skc25)
| ~ man(skc25)
| ~ young(skc25)
| ~ seat(skc26)
| ~ furniture(skc26)
| ~ front(skc26) ),
inference(resolution,[status(thm)],[p317,c50]) ).
cnf(p319,plain,
( skc25 = skc24
| ssSkC0
| ~ fellow(skc25)
| ~ man(skc25)
| ~ young(skc25)
| ~ seat(skc26)
| ~ furniture(skc26)
| ~ front(skc26) ),
inference(factoring,[status(thm)],[p318]) ).
cnf(f5,negated_conjecture,
front(skc26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
fof(f5_nnf,plain,
front(skc26),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
front(skc26),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(p320,plain,
( skc25 = skc24
| ssSkC0
| ~ fellow(skc25)
| ~ man(skc25)
| ~ young(skc25)
| ~ seat(skc26)
| ~ furniture(skc26) ),
inference(resolution,[status(thm)],[p319,c5]) ).
cnf(f30,negated_conjecture,
( furniture(skc26)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
fof(f30_nnf,plain,
( furniture(skc26)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
( furniture(skc26)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( furniture(skc26)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p322,plain,
( ssSkC0
| skc25 = skc24
| ssSkC0
| ~ fellow(skc25)
| ~ man(skc25)
| ~ young(skc25)
| ~ seat(skc26) ),
inference(resolution,[status(thm)],[p320,c30]) ).
cnf(p323,plain,
( skc25 = skc24
| ssSkC0
| ~ fellow(skc25)
| ~ man(skc25)
| ~ young(skc25)
| ~ seat(skc26) ),
inference(factoring,[status(thm)],[p322]) ).
cnf(f29,negated_conjecture,
( seat(skc26)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
fof(f29_nnf,plain,
( seat(skc26)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
( seat(skc26)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( seat(skc26)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p324,plain,
( ssSkC0
| skc25 = skc24
| ssSkC0
| ~ fellow(skc25)
| ~ man(skc25)
| ~ young(skc25) ),
inference(resolution,[status(thm)],[p323,c29]) ).
cnf(p325,plain,
( skc25 = skc24
| ssSkC0
| ~ fellow(skc25)
| ~ man(skc25)
| ~ young(skc25) ),
inference(factoring,[status(thm)],[p324]) ).
cnf(f27,negated_conjecture,
( young(skc25)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
fof(f27_nnf,plain,
( young(skc25)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
( young(skc25)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
( young(skc25)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p327,plain,
( ssSkC0
| skc25 = skc24
| ssSkC0
| ~ fellow(skc25)
| ~ man(skc25) ),
inference(resolution,[status(thm)],[p325,c27]) ).
cnf(p328,plain,
( skc25 = skc24
| ssSkC0
| ~ fellow(skc25)
| ~ man(skc25) ),
inference(factoring,[status(thm)],[p327]) ).
cnf(f28,negated_conjecture,
( man(skc25)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
fof(f28_nnf,plain,
( man(skc25)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
( man(skc25)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( man(skc25)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p329,plain,
( ssSkC0
| skc25 = skc24
| ssSkC0
| ~ fellow(skc25) ),
inference(resolution,[status(thm)],[p328,c28]) ).
cnf(p330,plain,
( skc25 = skc24
| ssSkC0
| ~ fellow(skc25) ),
inference(factoring,[status(thm)],[p329]) ).
cnf(f6,negated_conjecture,
fellow(skc25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
fof(f6_nnf,plain,
fellow(skc25),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
fellow(skc25),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(p332,plain,
( skc25 = skc24
| ssSkC0 ),
inference(resolution,[status(thm)],[p330,c6]) ).
cnf(f56,negated_conjecture,
( ssSkC0
| skc25 != skc24 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
fof(f56_nnf,plain,
( ssSkC0
| skc25 != skc24 ),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
( ssSkC0
| skc25 != skc24 ),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c56,plain,
( ssSkC0
| skc25 != skc24 ),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(p334,plain,
( ssSkC0
| ssSkC0 ),
inference(resolution,[status(thm)],[p332,c56]) ).
cnf(p335,plain,
ssSkC0,
inference(factoring,[status(thm)],[p334]) ).
cnf(f31,negated_conjecture,
( lonely(skc20)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
fof(f31_nnf,plain,
( lonely(skc20)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
( lonely(skc20)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( lonely(skc20)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p336,plain,
lonely(skc20),
inference(resolution,[status(thm)],[p335,c31]) ).
cnf(f59,negated_conjecture,
( X1 = Y
| ~ ssSkC0
| ~ in(X1,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(Z)
| ~ furniture(Z)
| ~ front(Z)
| ~ in(Y,Z)
| ~ young(Y)
| ~ man(Y)
| ~ fellow(Y)
| ~ in(W,X)
| ~ city(X)
| ~ hollywood(X)
| ~ event(W)
| ~ barrel(W,V)
| ~ down(W,U)
| ~ old(V)
| ~ dirty(V)
| ~ white(V)
| ~ car(V)
| ~ chevy(V)
| ~ street(U)
| ~ way(U)
| ~ lonely(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause60) ).
fof(f59_nnf,plain,
! [U,V,W,X,Y,Z,X1,X2] :
( X1 = Y
| ~ ssSkC0
| ~ in(X1,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(Z)
| ~ furniture(Z)
| ~ front(Z)
| ~ in(Y,Z)
| ~ young(Y)
| ~ man(Y)
| ~ fellow(Y)
| ~ in(W,X)
| ~ city(X)
| ~ hollywood(X)
| ~ event(W)
| ~ barrel(W,V)
| ~ down(W,U)
| ~ old(V)
| ~ dirty(V)
| ~ white(V)
| ~ car(V)
| ~ chevy(V)
| ~ street(U)
| ~ way(U)
| ~ lonely(U) ),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
! [U,V,W,X,Y,Z,X1,X2] :
( X1 = Y
| ~ ssSkC0
| ~ in(X1,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(Z)
| ~ furniture(Z)
| ~ front(Z)
| ~ in(Y,Z)
| ~ young(Y)
| ~ man(Y)
| ~ fellow(Y)
| ~ in(W,X)
| ~ city(X)
| ~ hollywood(X)
| ~ event(W)
| ~ barrel(W,V)
| ~ down(W,U)
| ~ old(V)
| ~ dirty(V)
| ~ white(V)
| ~ car(V)
| ~ chevy(V)
| ~ street(U)
| ~ way(U)
| ~ lonely(U) ),
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c59,plain,
( X6 = X4
| ~ ssSkC0
| ~ in(X6,X7)
| ~ front(X7)
| ~ furniture(X7)
| ~ seat(X7)
| ~ fellow(X6)
| ~ man(X6)
| ~ young(X6)
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ in(X2,X3)
| ~ city(X3)
| ~ hollywood(X3)
| ~ event(X2)
| ~ barrel(X2,X1)
| ~ down(X2,X0)
| ~ old(X1)
| ~ dirty(X1)
| ~ white(X1)
| ~ car(X1)
| ~ chevy(X1)
| ~ street(X0)
| ~ way(X0)
| ~ lonely(X0) ),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
cnf(p356,plain,
( X5 = X3
| ~ ssSkC0
| ~ in(X5,X6)
| ~ front(X6)
| ~ furniture(X6)
| ~ seat(X6)
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ in(X1,X2)
| ~ city(X2)
| ~ hollywood(X2)
| ~ event(X1)
| ~ barrel(X1,X0)
| ~ down(X1,skc20)
| ~ old(X0)
| ~ dirty(X0)
| ~ white(X0)
| ~ car(X0)
| ~ chevy(X0)
| ~ street(skc20)
| ~ way(skc20) ),
inference(resolution,[status(thm)],[p336,c59]) ).
cnf(f32,negated_conjecture,
( way(skc20)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
fof(f32_nnf,plain,
( way(skc20)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
( way(skc20)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,plain,
( way(skc20)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p337,plain,
way(skc20),
inference(resolution,[status(thm)],[p335,c32]) ).
cnf(p362,plain,
( X5 = X3
| ~ ssSkC0
| ~ in(X5,X6)
| ~ front(X6)
| ~ furniture(X6)
| ~ seat(X6)
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ in(X1,X2)
| ~ city(X2)
| ~ hollywood(X2)
| ~ event(X1)
| ~ barrel(X1,X0)
| ~ down(X1,skc20)
| ~ old(X0)
| ~ dirty(X0)
| ~ white(X0)
| ~ car(X0)
| ~ chevy(X0)
| ~ street(skc20) ),
inference(resolution,[status(thm)],[p356,p337]) ).
cnf(f11,negated_conjecture,
street(skc20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
fof(f11_nnf,plain,
street(skc20),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
street(skc20),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(p386,plain,
( X5 = X3
| ~ ssSkC0
| ~ in(X5,X6)
| ~ front(X6)
| ~ furniture(X6)
| ~ seat(X6)
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ in(X1,X2)
| ~ city(X2)
| ~ hollywood(X2)
| ~ event(X1)
| ~ barrel(X1,X0)
| ~ down(X1,skc20)
| ~ old(X0)
| ~ dirty(X0)
| ~ white(X0)
| ~ car(X0)
| ~ chevy(X0) ),
inference(resolution,[status(thm)],[p362,c11]) ).
cnf(f33,negated_conjecture,
( chevy(skc21)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
fof(f33_nnf,plain,
( chevy(skc21)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
( chevy(skc21)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
( chevy(skc21)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p338,plain,
chevy(skc21),
inference(resolution,[status(thm)],[p335,c33]) ).
cnf(p405,plain,
( X4 = X2
| ~ ssSkC0
| ~ in(X4,X5)
| ~ front(X5)
| ~ furniture(X5)
| ~ seat(X5)
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc21)
| ~ down(X0,skc20)
| ~ old(skc21)
| ~ dirty(skc21)
| ~ white(skc21)
| ~ car(skc21) ),
inference(resolution,[status(thm)],[p386,p338]) ).
cnf(f34,negated_conjecture,
( car(skc21)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
fof(f34_nnf,plain,
( car(skc21)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
( car(skc21)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
( car(skc21)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p339,plain,
car(skc21),
inference(resolution,[status(thm)],[p335,c34]) ).
cnf(p421,plain,
( X4 = X2
| ~ ssSkC0
| ~ in(X4,X5)
| ~ front(X5)
| ~ furniture(X5)
| ~ seat(X5)
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc21)
| ~ down(X0,skc20)
| ~ old(skc21)
| ~ dirty(skc21)
| ~ white(skc21) ),
inference(resolution,[status(thm)],[p405,p339]) ).
cnf(f35,negated_conjecture,
( white(skc21)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
fof(f35_nnf,plain,
( white(skc21)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
( white(skc21)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( white(skc21)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p340,plain,
white(skc21),
inference(resolution,[status(thm)],[p335,c35]) ).
cnf(p435,plain,
( X4 = X2
| ~ ssSkC0
| ~ in(X4,X5)
| ~ front(X5)
| ~ furniture(X5)
| ~ seat(X5)
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc21)
| ~ down(X0,skc20)
| ~ old(skc21)
| ~ dirty(skc21) ),
inference(resolution,[status(thm)],[p421,p340]) ).
cnf(f36,negated_conjecture,
( dirty(skc21)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
fof(f36_nnf,plain,
( dirty(skc21)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
( dirty(skc21)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
( dirty(skc21)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p341,plain,
dirty(skc21),
inference(resolution,[status(thm)],[p335,c36]) ).
cnf(p449,plain,
( X4 = X2
| ~ ssSkC0
| ~ in(X4,X5)
| ~ front(X5)
| ~ furniture(X5)
| ~ seat(X5)
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc21)
| ~ down(X0,skc20)
| ~ old(skc21) ),
inference(resolution,[status(thm)],[p435,p341]) ).
cnf(f10,negated_conjecture,
old(skc21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
fof(f10_nnf,plain,
old(skc21),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
old(skc21),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(p458,plain,
( X4 = X2
| ~ ssSkC0
| ~ in(X4,X5)
| ~ front(X5)
| ~ furniture(X5)
| ~ seat(X5)
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ in(X0,X1)
| ~ city(X1)
| ~ hollywood(X1)
| ~ event(X0)
| ~ barrel(X0,skc21)
| ~ down(X0,skc20) ),
inference(resolution,[status(thm)],[p449,c10]) ).
cnf(f51,negated_conjecture,
( down(skc22,skc20)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
fof(f51_nnf,plain,
( down(skc22,skc20)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
( down(skc22,skc20)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
( down(skc22,skc20)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(p351,plain,
down(skc22,skc20),
inference(resolution,[status(thm)],[p335,c51]) ).
cnf(p463,plain,
( X3 = X1
| ~ ssSkC0
| ~ in(X3,X4)
| ~ front(X4)
| ~ furniture(X4)
| ~ seat(X4)
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ in(skc22,X0)
| ~ city(X0)
| ~ hollywood(X0)
| ~ event(skc22)
| ~ barrel(skc22,skc21) ),
inference(resolution,[status(thm)],[p458,p351]) ).
cnf(f52,negated_conjecture,
( barrel(skc22,skc21)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
fof(f52_nnf,plain,
( barrel(skc22,skc21)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
( barrel(skc22,skc21)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f52_nnf]) ).
cnf(c52,plain,
( barrel(skc22,skc21)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p352,plain,
barrel(skc22,skc21),
inference(resolution,[status(thm)],[p335,c52]) ).
cnf(p469,plain,
( X3 = X1
| ~ ssSkC0
| ~ in(X3,X4)
| ~ front(X4)
| ~ furniture(X4)
| ~ seat(X4)
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ in(skc22,X0)
| ~ city(X0)
| ~ hollywood(X0)
| ~ event(skc22) ),
inference(resolution,[status(thm)],[p463,p352]) ).
cnf(f9,negated_conjecture,
event(skc22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
fof(f9_nnf,plain,
event(skc22),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
event(skc22),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(p478,plain,
( X3 = X1
| ~ ssSkC0
| ~ in(X3,X4)
| ~ front(X4)
| ~ furniture(X4)
| ~ seat(X4)
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ in(skc22,X0)
| ~ city(X0)
| ~ hollywood(X0) ),
inference(resolution,[status(thm)],[p469,c9]) ).
cnf(f37,negated_conjecture,
( hollywood(skc23)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
fof(f37_nnf,plain,
( hollywood(skc23)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
( hollywood(skc23)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
( hollywood(skc23)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p342,plain,
hollywood(skc23),
inference(resolution,[status(thm)],[p335,c37]) ).
cnf(p482,plain,
( X2 = X0
| ~ ssSkC0
| ~ in(X2,X3)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ in(skc22,skc23)
| ~ city(skc23) ),
inference(resolution,[status(thm)],[p478,p342]) ).
cnf(f8,negated_conjecture,
city(skc23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
fof(f8_nnf,plain,
city(skc23),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
city(skc23),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(p483,plain,
( X2 = X0
| ~ ssSkC0
| ~ in(X2,X3)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ in(skc22,skc23) ),
inference(resolution,[status(thm)],[p482,c8]) ).
cnf(f53,negated_conjecture,
( in(skc22,skc23)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
fof(f53_nnf,plain,
( in(skc22,skc23)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f53]) ).
fof(f53_sk,plain,
( in(skc22,skc23)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f53_nnf]) ).
cnf(c53,plain,
( in(skc22,skc23)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(p353,plain,
in(skc22,skc23),
inference(resolution,[status(thm)],[p335,c53]) ).
cnf(p484,plain,
( X2 = X0
| ~ ssSkC0
| ~ in(X2,X3)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0) ),
inference(resolution,[status(thm)],[p483,p353]) ).
cnf(f14,negated_conjecture,
fellow(skc17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
fof(f14_nnf,plain,
fellow(skc17),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c14,plain,
fellow(skc17),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(p486,plain,
( X1 = skc17
| ~ ssSkC0
| ~ in(X1,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ in(skc17,X0)
| ~ young(skc17)
| ~ man(skc17) ),
inference(resolution,[status(thm)],[p484,c14]) ).
cnf(f45,negated_conjecture,
( man(skc17)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
fof(f45_nnf,plain,
( man(skc17)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
( man(skc17)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c45,plain,
( man(skc17)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p350,plain,
man(skc17),
inference(resolution,[status(thm)],[p335,c45]) ).
cnf(p488,plain,
( X1 = skc17
| ~ ssSkC0
| ~ in(X1,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ in(skc17,X0)
| ~ young(skc17) ),
inference(resolution,[status(thm)],[p486,p350]) ).
cnf(f44,negated_conjecture,
( young(skc17)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
fof(f44_nnf,plain,
( young(skc17)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
( young(skc17)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
( young(skc17)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p349,plain,
young(skc17),
inference(resolution,[status(thm)],[p335,c44]) ).
cnf(p489,plain,
( X1 = skc17
| ~ ssSkC0
| ~ in(X1,X2)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ in(skc17,X0) ),
inference(resolution,[status(thm)],[p488,p349]) ).
cnf(f55,negated_conjecture,
( in(skc17,skc18)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
fof(f55_nnf,plain,
( in(skc17,skc18)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f55]) ).
fof(f55_sk,plain,
( in(skc17,skc18)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f55_nnf]) ).
cnf(c55,plain,
( in(skc17,skc18)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f55_sk]) ).
cnf(p355,plain,
in(skc17,skc18),
inference(resolution,[status(thm)],[p335,c55]) ).
cnf(p490,plain,
( X0 = skc17
| ~ ssSkC0
| ~ in(X0,X1)
| ~ front(X1)
| ~ furniture(X1)
| ~ seat(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(skc18)
| ~ furniture(skc18)
| ~ front(skc18) ),
inference(resolution,[status(thm)],[p489,p355]) ).
cnf(f42,negated_conjecture,
( front(skc18)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
fof(f42_nnf,plain,
( front(skc18)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
( front(skc18)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
( front(skc18)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p347,plain,
front(skc18),
inference(resolution,[status(thm)],[p335,c42]) ).
cnf(p491,plain,
( X0 = skc17
| ~ ssSkC0
| ~ in(X0,X1)
| ~ front(X1)
| ~ furniture(X1)
| ~ seat(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(skc18)
| ~ furniture(skc18) ),
inference(resolution,[status(thm)],[p490,p347]) ).
cnf(f43,negated_conjecture,
( furniture(skc18)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
fof(f43_nnf,plain,
( furniture(skc18)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
( furniture(skc18)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
( furniture(skc18)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p348,plain,
furniture(skc18),
inference(resolution,[status(thm)],[p335,c43]) ).
cnf(p492,plain,
( X0 = skc17
| ~ ssSkC0
| ~ in(X0,X1)
| ~ front(X1)
| ~ furniture(X1)
| ~ seat(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(skc18) ),
inference(resolution,[status(thm)],[p491,p348]) ).
cnf(f13,negated_conjecture,
seat(skc18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
fof(f13_nnf,plain,
seat(skc18),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
seat(skc18),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(p494,plain,
( X0 = skc17
| ~ ssSkC0
| ~ in(X0,X1)
| ~ front(X1)
| ~ furniture(X1)
| ~ seat(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0) ),
inference(resolution,[status(thm)],[p492,c13]) ).
cnf(f15,negated_conjecture,
young(skc16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
fof(f15_nnf,plain,
young(skc16),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c15,plain,
young(skc16),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(p496,plain,
( skc16 = skc17
| ~ ssSkC0
| ~ in(skc16,X0)
| ~ front(X0)
| ~ furniture(X0)
| ~ seat(X0)
| ~ fellow(skc16)
| ~ man(skc16) ),
inference(resolution,[status(thm)],[p494,c15]) ).
cnf(f41,negated_conjecture,
( man(skc16)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
fof(f41_nnf,plain,
( man(skc16)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
( man(skc16)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c41,plain,
( man(skc16)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p346,plain,
man(skc16),
inference(resolution,[status(thm)],[p335,c41]) ).
cnf(p497,plain,
( skc16 = skc17
| ~ ssSkC0
| ~ in(skc16,X0)
| ~ front(X0)
| ~ furniture(X0)
| ~ seat(X0)
| ~ fellow(skc16) ),
inference(resolution,[status(thm)],[p496,p346]) ).
cnf(f40,negated_conjecture,
( fellow(skc16)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
fof(f40_nnf,plain,
( fellow(skc16)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
( fellow(skc16)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( fellow(skc16)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p345,plain,
fellow(skc16),
inference(resolution,[status(thm)],[p335,c40]) ).
cnf(p499,plain,
( skc16 = skc17
| ~ ssSkC0
| ~ in(skc16,X0)
| ~ front(X0)
| ~ furniture(X0)
| ~ seat(X0) ),
inference(resolution,[status(thm)],[p497,p345]) ).
cnf(f38,negated_conjecture,
( seat(skc19)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
fof(f38_nnf,plain,
( seat(skc19)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
( seat(skc19)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
( seat(skc19)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p343,plain,
seat(skc19),
inference(resolution,[status(thm)],[p335,c38]) ).
cnf(p501,plain,
( skc16 = skc17
| ~ ssSkC0
| ~ in(skc16,skc19)
| ~ front(skc19)
| ~ furniture(skc19) ),
inference(resolution,[status(thm)],[p499,p343]) ).
cnf(f39,negated_conjecture,
( furniture(skc19)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
fof(f39_nnf,plain,
( furniture(skc19)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
( furniture(skc19)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( furniture(skc19)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p344,plain,
furniture(skc19),
inference(resolution,[status(thm)],[p335,c39]) ).
cnf(p502,plain,
( skc16 = skc17
| ~ ssSkC0
| ~ in(skc16,skc19)
| ~ front(skc19) ),
inference(resolution,[status(thm)],[p501,p344]) ).
cnf(f12,negated_conjecture,
front(skc19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
fof(f12_nnf,plain,
front(skc19),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
front(skc19),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(p504,plain,
( skc16 = skc17
| ~ ssSkC0
| ~ in(skc16,skc19) ),
inference(resolution,[status(thm)],[p502,c12]) ).
cnf(f54,negated_conjecture,
( in(skc16,skc19)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause55) ).
fof(f54_nnf,plain,
( in(skc16,skc19)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
( in(skc16,skc19)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c54,plain,
( in(skc16,skc19)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(p354,plain,
in(skc16,skc19),
inference(resolution,[status(thm)],[p335,c54]) ).
cnf(p505,plain,
( skc16 = skc17
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[p504,p354]) ).
cnf(p506,plain,
skc16 = skc17,
inference(resolution,[status(thm)],[p505,p335]) ).
cnf(f57,negated_conjecture,
( ~ ssSkC0
| skc17 != skc16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause58) ).
fof(f57_nnf,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c57,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(p507,plain,
( ~ ssSkC0
| skc17 != skc17 ),
inference(demodulation,[status(thm)],[p506,c57]) ).
cnf(p511,plain,
~ ssSkC0,
inference(equality_resolution,[status(thm)],[p507]) ).
cnf(p512,plain,
$false,
inference(resolution,[status(thm)],[p511,p335]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP007-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 01:32:46 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 5.27/1.16 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.27/1.16 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------