%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NLP004-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 : n006.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:26 PM UTC 2026
% Result : Unsatisfiable 5.15s 6.17s
% Output : Proof 5.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 86
% Number of leaves : 60
% Syntax : Number of formulae : 327 ( 72 unt; 0 def)
% Number of atoms : 1848 ( 96 equ)
% Maximal formula atoms : 30 ( 5 avg)
% Number of connectives : 2895 (1374 ~;1521 |; 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 : 324 ( 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)
| ~ hollywood(X)
| ~ city(X)
| ~ in(W,X)
| ~ down(W,U)
| ~ barrel(W,V)
| ~ event(W)
| ~ chevy(V)
| ~ car(V)
| ~ white(V)
| ~ dirty(V)
| ~ old(V)
| ~ lonely(U)
| ~ way(U)
| ~ street(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)
| ~ hollywood(X)
| ~ city(X)
| ~ in(W,X)
| ~ down(W,U)
| ~ barrel(W,V)
| ~ event(W)
| ~ chevy(V)
| ~ car(V)
| ~ white(V)
| ~ dirty(V)
| ~ old(V)
| ~ lonely(U)
| ~ way(U)
| ~ street(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)
| ~ hollywood(X)
| ~ city(X)
| ~ in(W,X)
| ~ down(W,U)
| ~ barrel(W,V)
| ~ event(W)
| ~ chevy(V)
| ~ car(V)
| ~ white(V)
| ~ dirty(V)
| ~ old(V)
| ~ lonely(U)
| ~ way(U)
| ~ street(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)
| ~ hollywood(X3)
| ~ city(X3)
| ~ in(X2,X3)
| ~ down(X2,X0)
| ~ barrel(X2,X1)
| ~ event(X2)
| ~ chevy(X1)
| ~ car(X1)
| ~ white(X1)
| ~ dirty(X1)
| ~ old(X1)
| ~ lonely(X0)
| ~ way(X0)
| ~ street(X0) ),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(f2,negated_conjecture,
street(skc29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
fof(f2_nnf,plain,
street(skc29),
inference(nnf_transformation,[status(thm)],[f2]) ).
cnf(c2,plain,
street(skc29),
inference(cnf_transformation,[status(esa)],[f2_nnf]) ).
cnf(p65,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)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,skc29)
| ~ barrel(X1,X0)
| ~ event(X1)
| ~ chevy(X0)
| ~ car(X0)
| ~ white(X0)
| ~ dirty(X0)
| ~ old(X0)
| ~ lonely(skc29)
| ~ way(skc29) ),
inference(resolution,[status(thm)],[c58,c2]) ).
cnf(f21,negated_conjecture,
( way(skc29)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
fof(f21_nnf,plain,
( way(skc29)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
( way(skc29)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( way(skc29)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p97,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)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,skc29)
| ~ barrel(X1,X0)
| ~ event(X1)
| ~ chevy(X0)
| ~ car(X0)
| ~ white(X0)
| ~ dirty(X0)
| ~ old(X0)
| ~ lonely(skc29) ),
inference(resolution,[status(thm)],[p65,c21]) ).
cnf(p159,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)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,skc29)
| ~ barrel(X1,X0)
| ~ event(X1)
| ~ chevy(X0)
| ~ car(X0)
| ~ white(X0)
| ~ dirty(X0)
| ~ old(X0)
| ~ lonely(skc29) ),
inference(factoring,[status(thm)],[p97]) ).
cnf(f20,negated_conjecture,
( lonely(skc29)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
fof(f20_nnf,plain,
( lonely(skc29)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
( lonely(skc29)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( lonely(skc29)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p208,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)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,skc29)
| ~ barrel(X1,X0)
| ~ event(X1)
| ~ chevy(X0)
| ~ car(X0)
| ~ white(X0)
| ~ dirty(X0)
| ~ old(X0) ),
inference(resolution,[status(thm)],[p159,c20]) ).
cnf(p248,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)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,skc29)
| ~ barrel(X1,X0)
| ~ event(X1)
| ~ chevy(X0)
| ~ car(X0)
| ~ white(X0)
| ~ dirty(X0)
| ~ old(X0) ),
inference(factoring,[status(thm)],[p208]) ).
cnf(f3,negated_conjecture,
old(skc28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
fof(f3_nnf,plain,
old(skc28),
inference(nnf_transformation,[status(thm)],[f3]) ).
cnf(c3,plain,
old(skc28),
inference(cnf_transformation,[status(esa)],[f3_nnf]) ).
cnf(p267,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)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc29)
| ~ barrel(X0,skc28)
| ~ event(X0)
| ~ chevy(skc28)
| ~ car(skc28)
| ~ white(skc28)
| ~ dirty(skc28) ),
inference(resolution,[status(thm)],[p248,c3]) ).
cnf(f19,negated_conjecture,
( dirty(skc28)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
fof(f19_nnf,plain,
( dirty(skc28)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
( dirty(skc28)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( dirty(skc28)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p272,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)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc29)
| ~ barrel(X0,skc28)
| ~ event(X0)
| ~ chevy(skc28)
| ~ car(skc28)
| ~ white(skc28) ),
inference(resolution,[status(thm)],[p267,c19]) ).
cnf(p277,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)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc29)
| ~ barrel(X0,skc28)
| ~ event(X0)
| ~ chevy(skc28)
| ~ car(skc28)
| ~ white(skc28) ),
inference(factoring,[status(thm)],[p272]) ).
cnf(f18,negated_conjecture,
( white(skc28)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
fof(f18_nnf,plain,
( white(skc28)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
( white(skc28)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( white(skc28)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p283,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)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc29)
| ~ barrel(X0,skc28)
| ~ event(X0)
| ~ chevy(skc28)
| ~ car(skc28) ),
inference(resolution,[status(thm)],[p277,c18]) ).
cnf(p294,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)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc29)
| ~ barrel(X0,skc28)
| ~ event(X0)
| ~ chevy(skc28)
| ~ car(skc28) ),
inference(factoring,[status(thm)],[p283]) ).
cnf(f17,negated_conjecture,
( car(skc28)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
fof(f17_nnf,plain,
( car(skc28)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
( car(skc28)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( car(skc28)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p307,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)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc29)
| ~ barrel(X0,skc28)
| ~ event(X0)
| ~ chevy(skc28) ),
inference(resolution,[status(thm)],[p294,c17]) ).
cnf(p312,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)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc29)
| ~ barrel(X0,skc28)
| ~ event(X0)
| ~ chevy(skc28) ),
inference(factoring,[status(thm)],[p307]) ).
cnf(f16,negated_conjecture,
( chevy(skc28)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
fof(f16_nnf,plain,
( chevy(skc28)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
( chevy(skc28)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( chevy(skc28)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p317,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)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc29)
| ~ barrel(X0,skc28)
| ~ event(X0) ),
inference(resolution,[status(thm)],[p312,c16]) ).
cnf(p320,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)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc29)
| ~ barrel(X0,skc28)
| ~ event(X0) ),
inference(factoring,[status(thm)],[p317]) ).
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(p321,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)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc30,X0)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28) ),
inference(resolution,[status(thm)],[p320,c1]) ).
cnf(f46,negated_conjecture,
( barrel(skc30,skc28)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
fof(f46_nnf,plain,
( barrel(skc30,skc28)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
( barrel(skc30,skc28)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c46,plain,
( barrel(skc30,skc28)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(p323,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)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc30,X0)
| ~ down(skc30,skc29) ),
inference(resolution,[status(thm)],[p321,c46]) ).
cnf(p324,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)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc30,X0)
| ~ down(skc30,skc29) ),
inference(factoring,[status(thm)],[p323]) ).
cnf(f47,negated_conjecture,
( down(skc30,skc29)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
fof(f47_nnf,plain,
( down(skc30,skc29)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
( down(skc30,skc29)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c47,plain,
( down(skc30,skc29)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p325,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)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc30,X0) ),
inference(resolution,[status(thm)],[p324,c47]) ).
cnf(p326,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)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc30,X0) ),
inference(factoring,[status(thm)],[p325]) ).
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(p327,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)
| ~ hollywood(skc31)
| ~ city(skc31) ),
inference(resolution,[status(thm)],[p326,c48]) ).
cnf(p328,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)
| ~ hollywood(skc31)
| ~ city(skc31) ),
inference(factoring,[status(thm)],[p327]) ).
cnf(f22,negated_conjecture,
( city(skc31)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
fof(f22_nnf,plain,
( city(skc31)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
( city(skc31)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( city(skc31)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p329,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)
| ~ hollywood(skc31) ),
inference(resolution,[status(thm)],[p328,c22]) ).
cnf(p330,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)
| ~ hollywood(skc31) ),
inference(factoring,[status(thm)],[p329]) ).
cnf(f0,negated_conjecture,
hollywood(skc31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
fof(f0_nnf,plain,
hollywood(skc31),
inference(nnf_transformation,[status(thm)],[f0]) ).
cnf(c0,plain,
hollywood(skc31),
inference(cnf_transformation,[status(esa)],[f0_nnf]) ).
cnf(p331,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(resolution,[status(thm)],[p330,c0]) ).
cnf(f5,negated_conjecture,
seat(skc26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
fof(f5_nnf,plain,
seat(skc26),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
seat(skc26),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(p332,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,skc26)
| ~ front(skc26)
| ~ furniture(skc26) ),
inference(resolution,[status(thm)],[p331,c5]) ).
cnf(f28,negated_conjecture,
( furniture(skc26)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
fof(f28_nnf,plain,
( furniture(skc26)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
( furniture(skc26)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( furniture(skc26)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p335,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,skc26)
| ~ front(skc26) ),
inference(resolution,[status(thm)],[p332,c28]) ).
cnf(p336,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,skc26)
| ~ front(skc26) ),
inference(factoring,[status(thm)],[p335]) ).
cnf(f27,negated_conjecture,
( front(skc26)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
fof(f27_nnf,plain,
( front(skc26)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
( front(skc26)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
( front(skc26)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p337,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,skc26) ),
inference(resolution,[status(thm)],[p336,c27]) ).
cnf(p338,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,skc26) ),
inference(factoring,[status(thm)],[p337]) ).
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(p339,plain,
( ssSkC0
| X0 = skc25
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc25)
| ~ man(skc25)
| ~ fellow(skc25) ),
inference(resolution,[status(thm)],[p338,c50]) ).
cnf(p340,plain,
( X0 = skc25
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc25)
| ~ man(skc25)
| ~ fellow(skc25) ),
inference(factoring,[status(thm)],[p339]) ).
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(p341,plain,
( X0 = skc25
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc25)
| ~ man(skc25) ),
inference(resolution,[status(thm)],[p340,c6]) ).
cnf(f30,negated_conjecture,
( man(skc25)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
fof(f30_nnf,plain,
( man(skc25)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
( man(skc25)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( man(skc25)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p343,plain,
( ssSkC0
| X0 = skc25
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc25) ),
inference(resolution,[status(thm)],[p341,c30]) ).
cnf(p344,plain,
( X0 = skc25
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc25) ),
inference(factoring,[status(thm)],[p343]) ).
cnf(f29,negated_conjecture,
( young(skc25)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
fof(f29_nnf,plain,
( young(skc25)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
( young(skc25)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( young(skc25)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p345,plain,
( ssSkC0
| X0 = skc25
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[p344,c29]) ).
cnf(p346,plain,
( X0 = skc25
| ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1) ),
inference(factoring,[status(thm)],[p345]) ).
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(p348,plain,
( ssSkC0
| skc24 = skc25
| ssSkC0
| ~ fellow(skc24)
| ~ man(skc24)
| ~ young(skc24)
| ~ seat(skc27)
| ~ furniture(skc27)
| ~ front(skc27) ),
inference(resolution,[status(thm)],[p346,c49]) ).
cnf(p349,plain,
( skc24 = skc25
| ssSkC0
| ~ fellow(skc24)
| ~ man(skc24)
| ~ young(skc24)
| ~ seat(skc27)
| ~ furniture(skc27)
| ~ front(skc27) ),
inference(factoring,[status(thm)],[p348]) ).
cnf(f4,negated_conjecture,
front(skc27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
fof(f4_nnf,plain,
front(skc27),
inference(nnf_transformation,[status(thm)],[f4]) ).
cnf(c4,plain,
front(skc27),
inference(cnf_transformation,[status(esa)],[f4_nnf]) ).
cnf(p350,plain,
( skc24 = skc25
| ssSkC0
| ~ fellow(skc24)
| ~ man(skc24)
| ~ young(skc24)
| ~ seat(skc27)
| ~ furniture(skc27) ),
inference(resolution,[status(thm)],[p349,c4]) ).
cnf(f24,negated_conjecture,
( furniture(skc27)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
fof(f24_nnf,plain,
( furniture(skc27)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
( furniture(skc27)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( furniture(skc27)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p351,plain,
( ssSkC0
| skc24 = skc25
| ssSkC0
| ~ fellow(skc24)
| ~ man(skc24)
| ~ young(skc24)
| ~ seat(skc27) ),
inference(resolution,[status(thm)],[p350,c24]) ).
cnf(p353,plain,
( skc24 = skc25
| ssSkC0
| ~ fellow(skc24)
| ~ man(skc24)
| ~ young(skc24)
| ~ seat(skc27) ),
inference(factoring,[status(thm)],[p351]) ).
cnf(f23,negated_conjecture,
( seat(skc27)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
fof(f23_nnf,plain,
( seat(skc27)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
( seat(skc27)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( seat(skc27)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p354,plain,
( ssSkC0
| skc24 = skc25
| ssSkC0
| ~ fellow(skc24)
| ~ man(skc24)
| ~ young(skc24) ),
inference(resolution,[status(thm)],[p353,c23]) ).
cnf(p355,plain,
( skc24 = skc25
| ssSkC0
| ~ fellow(skc24)
| ~ man(skc24)
| ~ young(skc24) ),
inference(factoring,[status(thm)],[p354]) ).
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(p356,plain,
( skc24 = skc25
| ssSkC0
| ~ fellow(skc24)
| ~ man(skc24) ),
inference(resolution,[status(thm)],[p355,c7]) ).
cnf(f26,negated_conjecture,
( man(skc24)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
fof(f26_nnf,plain,
( man(skc24)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
( man(skc24)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( man(skc24)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p358,plain,
( ssSkC0
| skc24 = skc25
| ssSkC0
| ~ fellow(skc24) ),
inference(resolution,[status(thm)],[p356,c26]) ).
cnf(p359,plain,
( skc24 = skc25
| ssSkC0
| ~ fellow(skc24) ),
inference(factoring,[status(thm)],[p358]) ).
cnf(f25,negated_conjecture,
( fellow(skc24)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
fof(f25_nnf,plain,
( fellow(skc24)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
( fellow(skc24)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
( fellow(skc24)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p360,plain,
( ssSkC0
| skc24 = skc25
| ssSkC0 ),
inference(resolution,[status(thm)],[p359,c25]) ).
cnf(p361,plain,
( skc24 = skc25
| ssSkC0 ),
inference(factoring,[status(thm)],[p360]) ).
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(p364,plain,
( ssSkC0
| skc25 != skc25
| ssSkC0 ),
inference(superposition,[status(thm)],[p361,c56]) ).
cnf(p368,plain,
( skc25 != skc25
| ssSkC0 ),
inference(factoring,[status(thm)],[p364]) ).
cnf(p370,plain,
ssSkC0,
inference(equality_resolution,[status(thm)],[p368]) ).
cnf(f36,negated_conjecture,
( car(skc21)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
fof(f36_nnf,plain,
( car(skc21)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
( car(skc21)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
( car(skc21)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p376,plain,
car(skc21),
inference(resolution,[status(thm)],[p370,c36]) ).
cnf(f59,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)
| ~ hollywood(X)
| ~ city(X)
| ~ in(W,X)
| ~ down(W,V)
| ~ barrel(W,U)
| ~ event(W)
| ~ street(V)
| ~ way(V)
| ~ lonely(V)
| ~ old(U)
| ~ dirty(U)
| ~ white(U)
| ~ car(U)
| ~ chevy(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause60) ).
fof(f59_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)
| ~ hollywood(X)
| ~ city(X)
| ~ in(W,X)
| ~ down(W,V)
| ~ barrel(W,U)
| ~ event(W)
| ~ street(V)
| ~ way(V)
| ~ lonely(V)
| ~ old(U)
| ~ dirty(U)
| ~ white(U)
| ~ car(U)
| ~ chevy(U) ),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_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)
| ~ hollywood(X)
| ~ city(X)
| ~ in(W,X)
| ~ down(W,V)
| ~ barrel(W,U)
| ~ event(W)
| ~ street(V)
| ~ way(V)
| ~ lonely(V)
| ~ old(U)
| ~ dirty(U)
| ~ white(U)
| ~ car(U)
| ~ chevy(U) ),
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c59,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)
| ~ hollywood(X3)
| ~ city(X3)
| ~ in(X2,X3)
| ~ down(X2,X1)
| ~ barrel(X2,X0)
| ~ event(X2)
| ~ street(X1)
| ~ way(X1)
| ~ lonely(X1)
| ~ old(X0)
| ~ dirty(X0)
| ~ white(X0)
| ~ car(X0)
| ~ chevy(X0) ),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
cnf(f10,negated_conjecture,
chevy(skc21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
fof(f10_nnf,plain,
chevy(skc21),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
chevy(skc21),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(p71,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)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,X0)
| ~ barrel(X1,skc21)
| ~ event(X1)
| ~ street(X0)
| ~ way(X0)
| ~ lonely(X0)
| ~ old(skc21)
| ~ dirty(skc21)
| ~ white(skc21)
| ~ car(skc21) ),
inference(resolution,[status(thm)],[c59,c10]) ).
cnf(p391,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)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,X0)
| ~ barrel(X1,skc21)
| ~ event(X1)
| ~ street(X0)
| ~ way(X0)
| ~ lonely(X0)
| ~ old(skc21)
| ~ dirty(skc21)
| ~ white(skc21) ),
inference(resolution,[status(thm)],[p376,p71]) ).
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(p375,plain,
white(skc21),
inference(resolution,[status(thm)],[p370,c35]) ).
cnf(p399,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)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,X0)
| ~ barrel(X1,skc21)
| ~ event(X1)
| ~ street(X0)
| ~ way(X0)
| ~ lonely(X0)
| ~ old(skc21)
| ~ dirty(skc21) ),
inference(resolution,[status(thm)],[p391,p375]) ).
cnf(f34,negated_conjecture,
( dirty(skc21)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
fof(f34_nnf,plain,
( dirty(skc21)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
( dirty(skc21)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
( dirty(skc21)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p374,plain,
dirty(skc21),
inference(resolution,[status(thm)],[p370,c34]) ).
cnf(p418,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)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,X0)
| ~ barrel(X1,skc21)
| ~ event(X1)
| ~ street(X0)
| ~ way(X0)
| ~ lonely(X0)
| ~ old(skc21) ),
inference(resolution,[status(thm)],[p399,p374]) ).
cnf(f33,negated_conjecture,
( old(skc21)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
fof(f33_nnf,plain,
( old(skc21)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
( old(skc21)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
( old(skc21)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p373,plain,
old(skc21),
inference(resolution,[status(thm)],[p370,c33]) ).
cnf(p432,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)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,X0)
| ~ barrel(X1,skc21)
| ~ event(X1)
| ~ street(X0)
| ~ way(X0)
| ~ lonely(X0) ),
inference(resolution,[status(thm)],[p418,p373]) ).
cnf(f11,negated_conjecture,
lonely(skc20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
fof(f11_nnf,plain,
lonely(skc20),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
lonely(skc20),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(p448,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)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc20)
| ~ barrel(X0,skc21)
| ~ event(X0)
| ~ street(skc20)
| ~ way(skc20) ),
inference(resolution,[status(thm)],[p432,c11]) ).
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(p372,plain,
way(skc20),
inference(resolution,[status(thm)],[p370,c32]) ).
cnf(p462,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)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc20)
| ~ barrel(X0,skc21)
| ~ event(X0)
| ~ street(skc20) ),
inference(resolution,[status(thm)],[p448,p372]) ).
cnf(f31,negated_conjecture,
( street(skc20)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
fof(f31_nnf,plain,
( street(skc20)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
( street(skc20)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( street(skc20)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p371,plain,
street(skc20),
inference(resolution,[status(thm)],[p370,c31]) ).
cnf(p471,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)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc20)
| ~ barrel(X0,skc21)
| ~ event(X0) ),
inference(resolution,[status(thm)],[p462,p371]) ).
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(p481,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)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc22,X0)
| ~ down(skc22,skc20)
| ~ barrel(skc22,skc21) ),
inference(resolution,[status(thm)],[p471,c9]) ).
cnf(f51,negated_conjecture,
( barrel(skc22,skc21)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
fof(f51_nnf,plain,
( barrel(skc22,skc21)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
( barrel(skc22,skc21)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
( barrel(skc22,skc21)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(p386,plain,
barrel(skc22,skc21),
inference(resolution,[status(thm)],[p370,c51]) ).
cnf(p491,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)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc22,X0)
| ~ down(skc22,skc20) ),
inference(resolution,[status(thm)],[p481,p386]) ).
cnf(f52,negated_conjecture,
( down(skc22,skc20)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
fof(f52_nnf,plain,
( down(skc22,skc20)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
( down(skc22,skc20)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f52_nnf]) ).
cnf(c52,plain,
( down(skc22,skc20)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p387,plain,
down(skc22,skc20),
inference(resolution,[status(thm)],[p370,c52]) ).
cnf(p500,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)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc22,X0) ),
inference(resolution,[status(thm)],[p491,p387]) ).
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(p388,plain,
in(skc22,skc23),
inference(resolution,[status(thm)],[p370,c53]) ).
cnf(p502,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)
| ~ hollywood(skc23)
| ~ city(skc23) ),
inference(resolution,[status(thm)],[p500,p388]) ).
cnf(f37,negated_conjecture,
( city(skc23)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
fof(f37_nnf,plain,
( city(skc23)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
( city(skc23)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
( city(skc23)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p377,plain,
city(skc23),
inference(resolution,[status(thm)],[p370,c37]) ).
cnf(p503,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)
| ~ hollywood(skc23) ),
inference(resolution,[status(thm)],[p502,p377]) ).
cnf(f8,negated_conjecture,
hollywood(skc23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
fof(f8_nnf,plain,
hollywood(skc23),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
hollywood(skc23),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(p504,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(resolution,[status(thm)],[p503,c8]) ).
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(p506,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,skc18)
| ~ front(skc18)
| ~ furniture(skc18) ),
inference(resolution,[status(thm)],[p504,c13]) ).
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(p383,plain,
furniture(skc18),
inference(resolution,[status(thm)],[p370,c43]) ).
cnf(p508,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,skc18)
| ~ front(skc18) ),
inference(resolution,[status(thm)],[p506,p383]) ).
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(p382,plain,
front(skc18),
inference(resolution,[status(thm)],[p370,c42]) ).
cnf(p509,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,skc18) ),
inference(resolution,[status(thm)],[p508,p382]) ).
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(p390,plain,
in(skc17,skc18),
inference(resolution,[status(thm)],[p370,c55]) ).
cnf(p511,plain,
( X0 = skc17
| ~ ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc17)
| ~ man(skc17)
| ~ fellow(skc17) ),
inference(resolution,[status(thm)],[p509,p390]) ).
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(p512,plain,
( X0 = skc17
| ~ ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc17)
| ~ man(skc17) ),
inference(resolution,[status(thm)],[p511,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(p385,plain,
man(skc17),
inference(resolution,[status(thm)],[p370,c45]) ).
cnf(p513,plain,
( X0 = skc17
| ~ ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ young(skc17) ),
inference(resolution,[status(thm)],[p512,p385]) ).
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(p384,plain,
young(skc17),
inference(resolution,[status(thm)],[p370,c44]) ).
cnf(p514,plain,
( X0 = skc17
| ~ ssSkC0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[p513,p384]) ).
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(p389,plain,
in(skc16,skc19),
inference(resolution,[status(thm)],[p370,c54]) ).
cnf(p516,plain,
( skc16 = skc17
| ~ ssSkC0
| ~ fellow(skc16)
| ~ man(skc16)
| ~ young(skc16)
| ~ seat(skc19)
| ~ furniture(skc19)
| ~ front(skc19) ),
inference(resolution,[status(thm)],[p514,p389]) ).
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(p517,plain,
( skc16 = skc17
| ~ ssSkC0
| ~ fellow(skc16)
| ~ man(skc16)
| ~ young(skc16)
| ~ seat(skc19)
| ~ furniture(skc19) ),
inference(resolution,[status(thm)],[p516,c12]) ).
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(p379,plain,
furniture(skc19),
inference(resolution,[status(thm)],[p370,c39]) ).
cnf(p518,plain,
( skc16 = skc17
| ~ ssSkC0
| ~ fellow(skc16)
| ~ man(skc16)
| ~ young(skc16)
| ~ seat(skc19) ),
inference(resolution,[status(thm)],[p517,p379]) ).
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(p378,plain,
seat(skc19),
inference(resolution,[status(thm)],[p370,c38]) ).
cnf(p519,plain,
( skc16 = skc17
| ~ ssSkC0
| ~ fellow(skc16)
| ~ man(skc16)
| ~ young(skc16) ),
inference(resolution,[status(thm)],[p518,p378]) ).
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(p521,plain,
( skc16 = skc17
| ~ ssSkC0
| ~ fellow(skc16)
| ~ man(skc16) ),
inference(resolution,[status(thm)],[p519,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(p381,plain,
man(skc16),
inference(resolution,[status(thm)],[p370,c41]) ).
cnf(p522,plain,
( skc16 = skc17
| ~ ssSkC0
| ~ fellow(skc16) ),
inference(resolution,[status(thm)],[p521,p381]) ).
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(p380,plain,
fellow(skc16),
inference(resolution,[status(thm)],[p370,c40]) ).
cnf(p523,plain,
( skc16 = skc17
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[p522,p380]) ).
cnf(p524,plain,
skc16 = skc17,
inference(resolution,[status(thm)],[p523,p370]) ).
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(p525,plain,
( ~ ssSkC0
| skc17 != skc17 ),
inference(demodulation,[status(thm)],[p524,c57]) ).
cnf(p528,plain,
~ ssSkC0,
inference(equality_resolution,[status(thm)],[p525]) ).
cnf(p529,plain,
$false,
inference(resolution,[status(thm)],[p528,p370]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP004-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/5.38 % Computer : n006.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Thu Sep 24 01:36:35 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 5.15/6.17 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.15/6.17 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------