%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NLP009-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 : n002.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 4.21s 6.37s
% Output : Proof 4.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 54
% Syntax : Number of formulae : 295 ( 64 unt; 0 def)
% Number of atoms : 1556 ( 88 equ)
% Maximal formula atoms : 27 ( 5 avg)
% Number of connectives : 2390 (1129 ~;1261 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 2 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 14 con; 0-0 aty)
% Number of variables : 256 ( 0 sgn 28 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f52,negated_conjecture,
( Z = Y
| ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(Z,X1)
| ~ in(Y,X1)
| ~ young(Z)
| ~ man(Z)
| ~ fellow(Z)
| ~ fellow(Y)
| ~ man(Y)
| ~ young(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',clause53) ).
fof(f52_nnf,plain,
! [U,V,W,X,Y,Z,X1] :
( Z = Y
| ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(Z,X1)
| ~ in(Y,X1)
| ~ young(Z)
| ~ man(Z)
| ~ fellow(Z)
| ~ fellow(Y)
| ~ man(Y)
| ~ young(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)],[f52]) ).
fof(f52_sk,plain,
! [U,V,W,X,Y,Z,X1] :
( Z = Y
| ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(Z,X1)
| ~ in(Y,X1)
| ~ young(Z)
| ~ man(Z)
| ~ fellow(Z)
| ~ fellow(Y)
| ~ man(Y)
| ~ young(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)],[f52_nnf]) ).
cnf(c52,plain,
( X5 = X4
| ssSkC0
| ~ seat(X6)
| ~ furniture(X6)
| ~ front(X6)
| ~ in(X5,X6)
| ~ in(X4,X6)
| ~ young(X5)
| ~ man(X5)
| ~ fellow(X5)
| ~ fellow(X4)
| ~ man(X4)
| ~ young(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)],[f52_sk]) ).
cnf(f2,negated_conjecture,
street(skc25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
fof(f2_nnf,plain,
street(skc25),
inference(nnf_transformation,[status(thm)],[f2]) ).
cnf(c2,plain,
street(skc25),
inference(cnf_transformation,[status(esa)],[f2_nnf]) ).
cnf(p56,plain,
( X4 = X3
| ssSkC0
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ in(X3,X5)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,skc25)
| ~ barrel(X1,X0)
| ~ event(X1)
| ~ chevy(X0)
| ~ car(X0)
| ~ white(X0)
| ~ dirty(X0)
| ~ old(X0)
| ~ lonely(skc25)
| ~ way(skc25) ),
inference(resolution,[status(thm)],[c52,c2]) ).
cnf(f19,negated_conjecture,
( way(skc25)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
fof(f19_nnf,plain,
( way(skc25)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
( way(skc25)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( way(skc25)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p70,plain,
( ssSkC0
| X4 = X3
| ssSkC0
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ in(X3,X5)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,skc25)
| ~ barrel(X1,X0)
| ~ event(X1)
| ~ chevy(X0)
| ~ car(X0)
| ~ white(X0)
| ~ dirty(X0)
| ~ old(X0)
| ~ lonely(skc25) ),
inference(resolution,[status(thm)],[p56,c19]) ).
cnf(p93,plain,
( X4 = X3
| ssSkC0
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ in(X3,X5)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,skc25)
| ~ barrel(X1,X0)
| ~ event(X1)
| ~ chevy(X0)
| ~ car(X0)
| ~ white(X0)
| ~ dirty(X0)
| ~ old(X0)
| ~ lonely(skc25) ),
inference(factoring,[status(thm)],[p70]) ).
cnf(f18,negated_conjecture,
( lonely(skc25)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
fof(f18_nnf,plain,
( lonely(skc25)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
( lonely(skc25)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( lonely(skc25)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p107,plain,
( ssSkC0
| X4 = X3
| ssSkC0
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ in(X3,X5)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,skc25)
| ~ barrel(X1,X0)
| ~ event(X1)
| ~ chevy(X0)
| ~ car(X0)
| ~ white(X0)
| ~ dirty(X0)
| ~ old(X0) ),
inference(resolution,[status(thm)],[p93,c18]) ).
cnf(p118,plain,
( X4 = X3
| ssSkC0
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ in(X3,X5)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,skc25)
| ~ barrel(X1,X0)
| ~ event(X1)
| ~ chevy(X0)
| ~ car(X0)
| ~ white(X0)
| ~ dirty(X0)
| ~ old(X0) ),
inference(factoring,[status(thm)],[p107]) ).
cnf(f3,negated_conjecture,
old(skc24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
fof(f3_nnf,plain,
old(skc24),
inference(nnf_transformation,[status(thm)],[f3]) ).
cnf(c3,plain,
old(skc24),
inference(cnf_transformation,[status(esa)],[f3_nnf]) ).
cnf(p126,plain,
( X3 = X2
| ssSkC0
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ in(X2,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc25)
| ~ barrel(X0,skc24)
| ~ event(X0)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24) ),
inference(resolution,[status(thm)],[p118,c3]) ).
cnf(f17,negated_conjecture,
( dirty(skc24)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
fof(f17_nnf,plain,
( dirty(skc24)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
( dirty(skc24)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( dirty(skc24)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p128,plain,
( ssSkC0
| X3 = X2
| ssSkC0
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ in(X2,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc25)
| ~ barrel(X0,skc24)
| ~ event(X0)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24) ),
inference(resolution,[status(thm)],[p126,c17]) ).
cnf(p129,plain,
( X3 = X2
| ssSkC0
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ in(X2,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc25)
| ~ barrel(X0,skc24)
| ~ event(X0)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24) ),
inference(factoring,[status(thm)],[p128]) ).
cnf(f16,negated_conjecture,
( white(skc24)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
fof(f16_nnf,plain,
( white(skc24)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
( white(skc24)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( white(skc24)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p130,plain,
( ssSkC0
| X3 = X2
| ssSkC0
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ in(X2,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc25)
| ~ barrel(X0,skc24)
| ~ event(X0)
| ~ chevy(skc24)
| ~ car(skc24) ),
inference(resolution,[status(thm)],[p129,c16]) ).
cnf(p131,plain,
( X3 = X2
| ssSkC0
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ in(X2,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc25)
| ~ barrel(X0,skc24)
| ~ event(X0)
| ~ chevy(skc24)
| ~ car(skc24) ),
inference(factoring,[status(thm)],[p130]) ).
cnf(f15,negated_conjecture,
( car(skc24)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
fof(f15_nnf,plain,
( car(skc24)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
( car(skc24)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( car(skc24)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p132,plain,
( ssSkC0
| X3 = X2
| ssSkC0
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ in(X2,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc25)
| ~ barrel(X0,skc24)
| ~ event(X0)
| ~ chevy(skc24) ),
inference(resolution,[status(thm)],[p131,c15]) ).
cnf(p133,plain,
( X3 = X2
| ssSkC0
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ in(X2,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc25)
| ~ barrel(X0,skc24)
| ~ event(X0)
| ~ chevy(skc24) ),
inference(factoring,[status(thm)],[p132]) ).
cnf(f14,negated_conjecture,
( chevy(skc24)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
fof(f14_nnf,plain,
( chevy(skc24)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
( chevy(skc24)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( chevy(skc24)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p134,plain,
( ssSkC0
| X3 = X2
| ssSkC0
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ in(X2,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc25)
| ~ barrel(X0,skc24)
| ~ event(X0) ),
inference(resolution,[status(thm)],[p133,c14]) ).
cnf(p135,plain,
( X3 = X2
| ssSkC0
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ in(X2,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc25)
| ~ barrel(X0,skc24)
| ~ event(X0) ),
inference(factoring,[status(thm)],[p134]) ).
cnf(f1,negated_conjecture,
event(skc26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
fof(f1_nnf,plain,
event(skc26),
inference(nnf_transformation,[status(thm)],[f1]) ).
cnf(c1,plain,
event(skc26),
inference(cnf_transformation,[status(esa)],[f1_nnf]) ).
cnf(p136,plain,
( X2 = X1
| ssSkC0
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc26,X0)
| ~ down(skc26,skc25)
| ~ barrel(skc26,skc24) ),
inference(resolution,[status(thm)],[p135,c1]) ).
cnf(f40,negated_conjecture,
( barrel(skc26,skc24)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
fof(f40_nnf,plain,
( barrel(skc26,skc24)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
( barrel(skc26,skc24)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( barrel(skc26,skc24)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p138,plain,
( ssSkC0
| X2 = X1
| ssSkC0
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc26,X0)
| ~ down(skc26,skc25) ),
inference(resolution,[status(thm)],[p136,c40]) ).
cnf(p139,plain,
( X2 = X1
| ssSkC0
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc26,X0)
| ~ down(skc26,skc25) ),
inference(factoring,[status(thm)],[p138]) ).
cnf(f41,negated_conjecture,
( down(skc26,skc25)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
fof(f41_nnf,plain,
( down(skc26,skc25)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
( down(skc26,skc25)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c41,plain,
( down(skc26,skc25)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p140,plain,
( ssSkC0
| X2 = X1
| ssSkC0
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc26,X0) ),
inference(resolution,[status(thm)],[p139,c41]) ).
cnf(p141,plain,
( X2 = X1
| ssSkC0
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc26,X0) ),
inference(factoring,[status(thm)],[p140]) ).
cnf(f42,negated_conjecture,
( in(skc26,skc27)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
fof(f42_nnf,plain,
( in(skc26,skc27)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
( in(skc26,skc27)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
( in(skc26,skc27)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p142,plain,
( ssSkC0
| X1 = X0
| ssSkC0
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ in(X0,X2)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ hollywood(skc27)
| ~ city(skc27) ),
inference(resolution,[status(thm)],[p141,c42]) ).
cnf(p143,plain,
( X1 = X0
| ssSkC0
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ in(X0,X2)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ hollywood(skc27)
| ~ city(skc27) ),
inference(factoring,[status(thm)],[p142]) ).
cnf(f20,negated_conjecture,
( city(skc27)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
fof(f20_nnf,plain,
( city(skc27)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
( city(skc27)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( city(skc27)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p144,plain,
( ssSkC0
| X1 = X0
| ssSkC0
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ in(X0,X2)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ hollywood(skc27) ),
inference(resolution,[status(thm)],[p143,c20]) ).
cnf(p145,plain,
( X1 = X0
| ssSkC0
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ in(X0,X2)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ hollywood(skc27) ),
inference(factoring,[status(thm)],[p144]) ).
cnf(f0,negated_conjecture,
hollywood(skc27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
fof(f0_nnf,plain,
hollywood(skc27),
inference(nnf_transformation,[status(thm)],[f0]) ).
cnf(c0,plain,
hollywood(skc27),
inference(cnf_transformation,[status(esa)],[f0_nnf]) ).
cnf(p146,plain,
( X1 = X0
| ssSkC0
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ in(X0,X2)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0) ),
inference(resolution,[status(thm)],[p145,c0]) ).
cnf(f5,negated_conjecture,
young(skc22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
fof(f5_nnf,plain,
young(skc22),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
young(skc22),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(p147,plain,
( X0 = skc22
| ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ in(skc22,X1)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ fellow(skc22)
| ~ man(skc22) ),
inference(resolution,[status(thm)],[p146,c5]) ).
cnf(f24,negated_conjecture,
( man(skc22)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
fof(f24_nnf,plain,
( man(skc22)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
( man(skc22)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( man(skc22)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p150,plain,
( ssSkC0
| X0 = skc22
| ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ in(skc22,X1)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ fellow(skc22) ),
inference(resolution,[status(thm)],[p147,c24]) ).
cnf(p151,plain,
( X0 = skc22
| ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ in(skc22,X1)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ fellow(skc22) ),
inference(factoring,[status(thm)],[p150]) ).
cnf(f23,negated_conjecture,
( fellow(skc22)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
fof(f23_nnf,plain,
( fellow(skc22)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
( fellow(skc22)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( fellow(skc22)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p152,plain,
( ssSkC0
| X0 = skc22
| ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ in(skc22,X1)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0) ),
inference(resolution,[status(thm)],[p151,c23]) ).
cnf(p153,plain,
( X0 = skc22
| ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ in(skc22,X1)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0) ),
inference(factoring,[status(thm)],[p152]) ).
cnf(f6,negated_conjecture,
fellow(skc21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
fof(f6_nnf,plain,
fellow(skc21),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
fellow(skc21),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(p154,plain,
( skc21 = skc22
| ssSkC0
| ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ in(skc21,X0)
| ~ in(skc22,X0)
| ~ young(skc21)
| ~ man(skc21) ),
inference(resolution,[status(thm)],[p153,c6]) ).
cnf(f22,negated_conjecture,
( man(skc21)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
fof(f22_nnf,plain,
( man(skc21)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
( man(skc21)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( man(skc21)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p156,plain,
( ssSkC0
| skc21 = skc22
| ssSkC0
| ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ in(skc21,X0)
| ~ in(skc22,X0)
| ~ young(skc21) ),
inference(resolution,[status(thm)],[p154,c22]) ).
cnf(p158,plain,
( skc21 = skc22
| ssSkC0
| ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ in(skc21,X0)
| ~ in(skc22,X0)
| ~ young(skc21) ),
inference(factoring,[status(thm)],[p156]) ).
cnf(f21,negated_conjecture,
( young(skc21)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
fof(f21_nnf,plain,
( young(skc21)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
( young(skc21)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( young(skc21)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p159,plain,
( ssSkC0
| skc21 = skc22
| ssSkC0
| ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ in(skc21,X0)
| ~ in(skc22,X0) ),
inference(resolution,[status(thm)],[p158,c21]) ).
cnf(p160,plain,
( skc21 = skc22
| ssSkC0
| ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ in(skc21,X0)
| ~ in(skc22,X0) ),
inference(factoring,[status(thm)],[p159]) ).
cnf(f44,negated_conjecture,
( in(skc22,skc23)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
fof(f44_nnf,plain,
( in(skc22,skc23)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
( in(skc22,skc23)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
( in(skc22,skc23)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p161,plain,
( ssSkC0
| skc21 = skc22
| ssSkC0
| ~ seat(skc23)
| ~ furniture(skc23)
| ~ front(skc23)
| ~ in(skc21,skc23) ),
inference(resolution,[status(thm)],[p160,c44]) ).
cnf(p162,plain,
( skc21 = skc22
| ssSkC0
| ~ seat(skc23)
| ~ furniture(skc23)
| ~ front(skc23)
| ~ in(skc21,skc23) ),
inference(factoring,[status(thm)],[p161]) ).
cnf(f43,negated_conjecture,
( in(skc21,skc23)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
fof(f43_nnf,plain,
( in(skc21,skc23)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
( in(skc21,skc23)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
( in(skc21,skc23)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p163,plain,
( ssSkC0
| skc21 = skc22
| ssSkC0
| ~ seat(skc23)
| ~ furniture(skc23)
| ~ front(skc23) ),
inference(resolution,[status(thm)],[p162,c43]) ).
cnf(p164,plain,
( skc21 = skc22
| ssSkC0
| ~ seat(skc23)
| ~ furniture(skc23)
| ~ front(skc23) ),
inference(factoring,[status(thm)],[p163]) ).
cnf(f25,negated_conjecture,
( front(skc23)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
fof(f25_nnf,plain,
( front(skc23)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
( front(skc23)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
( front(skc23)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p165,plain,
( ssSkC0
| skc21 = skc22
| ssSkC0
| ~ seat(skc23)
| ~ furniture(skc23) ),
inference(resolution,[status(thm)],[p164,c25]) ).
cnf(p167,plain,
( skc21 = skc22
| ssSkC0
| ~ seat(skc23)
| ~ furniture(skc23) ),
inference(factoring,[status(thm)],[p165]) ).
cnf(f26,negated_conjecture,
( furniture(skc23)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
fof(f26_nnf,plain,
( furniture(skc23)
| ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
( furniture(skc23)
| ssSkC0 ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( furniture(skc23)
| ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p168,plain,
( ssSkC0
| skc21 = skc22
| ssSkC0
| ~ seat(skc23) ),
inference(resolution,[status(thm)],[p167,c26]) ).
cnf(p169,plain,
( skc21 = skc22
| ssSkC0
| ~ seat(skc23) ),
inference(factoring,[status(thm)],[p168]) ).
cnf(f4,negated_conjecture,
seat(skc23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
fof(f4_nnf,plain,
seat(skc23),
inference(nnf_transformation,[status(thm)],[f4]) ).
cnf(c4,plain,
seat(skc23),
inference(cnf_transformation,[status(esa)],[f4_nnf]) ).
cnf(p170,plain,
( skc21 = skc22
| ssSkC0 ),
inference(resolution,[status(thm)],[p169,c4]) ).
cnf(f50,negated_conjecture,
( ssSkC0
| skc22 != skc21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
fof(f50_nnf,plain,
( ssSkC0
| skc22 != skc21 ),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
( ssSkC0
| skc22 != skc21 ),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c50,plain,
( ssSkC0
| skc22 != skc21 ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(p172,plain,
( ssSkC0
| skc22 != skc22
| ssSkC0 ),
inference(superposition,[status(thm)],[p170,c50]) ).
cnf(p173,plain,
( skc22 != skc22
| ssSkC0 ),
inference(factoring,[status(thm)],[p172]) ).
cnf(p174,plain,
ssSkC0,
inference(equality_resolution,[status(thm)],[p173]) ).
cnf(f32,negated_conjecture,
( car(skc18)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
fof(f32_nnf,plain,
( car(skc18)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
( car(skc18)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,plain,
( car(skc18)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p180,plain,
car(skc18),
inference(resolution,[status(thm)],[p174,c32]) ).
cnf(f53,negated_conjecture,
( Z = Y
| ~ ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(Z,X1)
| ~ in(Y,X1)
| ~ young(Z)
| ~ man(Z)
| ~ fellow(Z)
| ~ fellow(Y)
| ~ man(Y)
| ~ young(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',clause54) ).
fof(f53_nnf,plain,
! [U,V,W,X,Y,Z,X1] :
( Z = Y
| ~ ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(Z,X1)
| ~ in(Y,X1)
| ~ young(Z)
| ~ man(Z)
| ~ fellow(Z)
| ~ fellow(Y)
| ~ man(Y)
| ~ young(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)],[f53]) ).
fof(f53_sk,plain,
! [U,V,W,X,Y,Z,X1] :
( Z = Y
| ~ ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(Z,X1)
| ~ in(Y,X1)
| ~ young(Z)
| ~ man(Z)
| ~ fellow(Z)
| ~ fellow(Y)
| ~ man(Y)
| ~ young(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)],[f53_nnf]) ).
cnf(c53,plain,
( X5 = X4
| ~ ssSkC0
| ~ seat(X6)
| ~ furniture(X6)
| ~ front(X6)
| ~ in(X5,X6)
| ~ in(X4,X6)
| ~ young(X5)
| ~ man(X5)
| ~ fellow(X5)
| ~ fellow(X4)
| ~ man(X4)
| ~ young(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)],[f53_sk]) ).
cnf(f9,negated_conjecture,
chevy(skc18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
fof(f9_nnf,plain,
chevy(skc18),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
chevy(skc18),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(p60,plain,
( X4 = X3
| ~ ssSkC0
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ in(X3,X5)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,X0)
| ~ barrel(X1,skc18)
| ~ event(X1)
| ~ street(X0)
| ~ way(X0)
| ~ lonely(X0)
| ~ old(skc18)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18) ),
inference(resolution,[status(thm)],[c53,c9]) ).
cnf(p193,plain,
( X4 = X3
| ~ ssSkC0
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ in(X3,X5)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,X0)
| ~ barrel(X1,skc18)
| ~ event(X1)
| ~ street(X0)
| ~ way(X0)
| ~ lonely(X0)
| ~ old(skc18)
| ~ dirty(skc18)
| ~ white(skc18) ),
inference(resolution,[status(thm)],[p180,p60]) ).
cnf(f31,negated_conjecture,
( white(skc18)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
fof(f31_nnf,plain,
( white(skc18)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
( white(skc18)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( white(skc18)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p179,plain,
white(skc18),
inference(resolution,[status(thm)],[p174,c31]) ).
cnf(p198,plain,
( X4 = X3
| ~ ssSkC0
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ in(X3,X5)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,X0)
| ~ barrel(X1,skc18)
| ~ event(X1)
| ~ street(X0)
| ~ way(X0)
| ~ lonely(X0)
| ~ old(skc18)
| ~ dirty(skc18) ),
inference(resolution,[status(thm)],[p193,p179]) ).
cnf(f30,negated_conjecture,
( dirty(skc18)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
fof(f30_nnf,plain,
( dirty(skc18)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
( dirty(skc18)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( dirty(skc18)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p178,plain,
dirty(skc18),
inference(resolution,[status(thm)],[p174,c30]) ).
cnf(p208,plain,
( X4 = X3
| ~ ssSkC0
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ in(X3,X5)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,X0)
| ~ barrel(X1,skc18)
| ~ event(X1)
| ~ street(X0)
| ~ way(X0)
| ~ lonely(X0)
| ~ old(skc18) ),
inference(resolution,[status(thm)],[p198,p178]) ).
cnf(f29,negated_conjecture,
( old(skc18)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
fof(f29_nnf,plain,
( old(skc18)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
( old(skc18)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( old(skc18)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p177,plain,
old(skc18),
inference(resolution,[status(thm)],[p174,c29]) ).
cnf(p217,plain,
( X4 = X3
| ~ ssSkC0
| ~ seat(X5)
| ~ furniture(X5)
| ~ front(X5)
| ~ in(X4,X5)
| ~ in(X3,X5)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| ~ fellow(X3)
| ~ man(X3)
| ~ young(X3)
| ~ hollywood(X2)
| ~ city(X2)
| ~ in(X1,X2)
| ~ down(X1,X0)
| ~ barrel(X1,skc18)
| ~ event(X1)
| ~ street(X0)
| ~ way(X0)
| ~ lonely(X0) ),
inference(resolution,[status(thm)],[p208,p177]) ).
cnf(f10,negated_conjecture,
lonely(skc17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
fof(f10_nnf,plain,
lonely(skc17),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
lonely(skc17),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(p222,plain,
( X3 = X2
| ~ ssSkC0
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ in(X2,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc17)
| ~ barrel(X0,skc18)
| ~ event(X0)
| ~ street(skc17)
| ~ way(skc17) ),
inference(resolution,[status(thm)],[p217,c10]) ).
cnf(f28,negated_conjecture,
( way(skc17)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
fof(f28_nnf,plain,
( way(skc17)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
( way(skc17)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( way(skc17)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p176,plain,
way(skc17),
inference(resolution,[status(thm)],[p174,c28]) ).
cnf(p229,plain,
( X3 = X2
| ~ ssSkC0
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ in(X2,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc17)
| ~ barrel(X0,skc18)
| ~ event(X0)
| ~ street(skc17) ),
inference(resolution,[status(thm)],[p222,p176]) ).
cnf(f27,negated_conjecture,
( street(skc17)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
fof(f27_nnf,plain,
( street(skc17)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
( street(skc17)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
( street(skc17)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p175,plain,
street(skc17),
inference(resolution,[status(thm)],[p174,c27]) ).
cnf(p234,plain,
( X3 = X2
| ~ ssSkC0
| ~ seat(X4)
| ~ furniture(X4)
| ~ front(X4)
| ~ in(X3,X4)
| ~ in(X2,X4)
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| ~ hollywood(X1)
| ~ city(X1)
| ~ in(X0,X1)
| ~ down(X0,skc17)
| ~ barrel(X0,skc18)
| ~ event(X0) ),
inference(resolution,[status(thm)],[p229,p175]) ).
cnf(f8,negated_conjecture,
event(skc19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
fof(f8_nnf,plain,
event(skc19),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
event(skc19),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(p236,plain,
( X2 = X1
| ~ ssSkC0
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc19,X0)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18) ),
inference(resolution,[status(thm)],[p234,c8]) ).
cnf(f45,negated_conjecture,
( barrel(skc19,skc18)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
fof(f45_nnf,plain,
( barrel(skc19,skc18)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
( barrel(skc19,skc18)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c45,plain,
( barrel(skc19,skc18)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p188,plain,
barrel(skc19,skc18),
inference(resolution,[status(thm)],[p174,c45]) ).
cnf(p237,plain,
( X2 = X1
| ~ ssSkC0
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc19,X0)
| ~ down(skc19,skc17) ),
inference(resolution,[status(thm)],[p236,p188]) ).
cnf(f46,negated_conjecture,
( down(skc19,skc17)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
fof(f46_nnf,plain,
( down(skc19,skc17)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
( down(skc19,skc17)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c46,plain,
( down(skc19,skc17)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(p189,plain,
down(skc19,skc17),
inference(resolution,[status(thm)],[p174,c46]) ).
cnf(p238,plain,
( X2 = X1
| ~ ssSkC0
| ~ seat(X3)
| ~ furniture(X3)
| ~ front(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ hollywood(X0)
| ~ city(X0)
| ~ in(skc19,X0) ),
inference(resolution,[status(thm)],[p237,p189]) ).
cnf(f47,negated_conjecture,
( in(skc19,skc20)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
fof(f47_nnf,plain,
( in(skc19,skc20)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
( in(skc19,skc20)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c47,plain,
( in(skc19,skc20)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p190,plain,
in(skc19,skc20),
inference(resolution,[status(thm)],[p174,c47]) ).
cnf(p239,plain,
( X1 = X0
| ~ ssSkC0
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ in(X0,X2)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ hollywood(skc20)
| ~ city(skc20) ),
inference(resolution,[status(thm)],[p238,p190]) ).
cnf(f33,negated_conjecture,
( city(skc20)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
fof(f33_nnf,plain,
( city(skc20)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
( city(skc20)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
( city(skc20)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p181,plain,
city(skc20),
inference(resolution,[status(thm)],[p174,c33]) ).
cnf(p240,plain,
( X1 = X0
| ~ ssSkC0
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ in(X0,X2)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ hollywood(skc20) ),
inference(resolution,[status(thm)],[p239,p181]) ).
cnf(f7,negated_conjecture,
hollywood(skc20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
fof(f7_nnf,plain,
hollywood(skc20),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
hollywood(skc20),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(p241,plain,
( X1 = X0
| ~ ssSkC0
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ in(X0,X2)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0) ),
inference(resolution,[status(thm)],[p240,c7]) ).
cnf(f12,negated_conjecture,
young(skc15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
fof(f12_nnf,plain,
young(skc15),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
young(skc15),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(p243,plain,
( X0 = skc15
| ~ ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ in(skc15,X1)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ fellow(skc15)
| ~ man(skc15) ),
inference(resolution,[status(thm)],[p241,c12]) ).
cnf(f37,negated_conjecture,
( man(skc15)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
fof(f37_nnf,plain,
( man(skc15)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
( man(skc15)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
( man(skc15)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p185,plain,
man(skc15),
inference(resolution,[status(thm)],[p174,c37]) ).
cnf(p245,plain,
( X0 = skc15
| ~ ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ in(skc15,X1)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ fellow(skc15) ),
inference(resolution,[status(thm)],[p243,p185]) ).
cnf(f36,negated_conjecture,
( fellow(skc15)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
fof(f36_nnf,plain,
( fellow(skc15)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
( fellow(skc15)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
( fellow(skc15)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p184,plain,
fellow(skc15),
inference(resolution,[status(thm)],[p174,c36]) ).
cnf(p246,plain,
( X0 = skc15
| ~ ssSkC0
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ in(X0,X1)
| ~ in(skc15,X1)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0) ),
inference(resolution,[status(thm)],[p245,p184]) ).
cnf(f13,negated_conjecture,
fellow(skc14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
fof(f13_nnf,plain,
fellow(skc14),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
fellow(skc14),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(p249,plain,
( skc14 = skc15
| ~ ssSkC0
| ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ in(skc14,X0)
| ~ in(skc15,X0)
| ~ young(skc14)
| ~ man(skc14) ),
inference(resolution,[status(thm)],[p246,c13]) ).
cnf(f35,negated_conjecture,
( man(skc14)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
fof(f35_nnf,plain,
( man(skc14)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
( man(skc14)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( man(skc14)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p183,plain,
man(skc14),
inference(resolution,[status(thm)],[p174,c35]) ).
cnf(p250,plain,
( skc14 = skc15
| ~ ssSkC0
| ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ in(skc14,X0)
| ~ in(skc15,X0)
| ~ young(skc14) ),
inference(resolution,[status(thm)],[p249,p183]) ).
cnf(f34,negated_conjecture,
( young(skc14)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
fof(f34_nnf,plain,
( young(skc14)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
( young(skc14)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
( young(skc14)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p182,plain,
young(skc14),
inference(resolution,[status(thm)],[p174,c34]) ).
cnf(p251,plain,
( skc14 = skc15
| ~ ssSkC0
| ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ in(skc14,X0)
| ~ in(skc15,X0) ),
inference(resolution,[status(thm)],[p250,p182]) ).
cnf(f49,negated_conjecture,
( in(skc15,skc16)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
fof(f49_nnf,plain,
( in(skc15,skc16)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
( in(skc15,skc16)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c49,plain,
( in(skc15,skc16)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(p192,plain,
in(skc15,skc16),
inference(resolution,[status(thm)],[p174,c49]) ).
cnf(p253,plain,
( skc14 = skc15
| ~ ssSkC0
| ~ seat(skc16)
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(skc14,skc16) ),
inference(resolution,[status(thm)],[p251,p192]) ).
cnf(f48,negated_conjecture,
( in(skc14,skc16)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
fof(f48_nnf,plain,
( in(skc14,skc16)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
( in(skc14,skc16)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c48,plain,
( in(skc14,skc16)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p191,plain,
in(skc14,skc16),
inference(resolution,[status(thm)],[p174,c48]) ).
cnf(p254,plain,
( skc14 = skc15
| ~ ssSkC0
| ~ seat(skc16)
| ~ furniture(skc16)
| ~ front(skc16) ),
inference(resolution,[status(thm)],[p253,p191]) ).
cnf(f38,negated_conjecture,
( front(skc16)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
fof(f38_nnf,plain,
( front(skc16)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
( front(skc16)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
( front(skc16)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p186,plain,
front(skc16),
inference(resolution,[status(thm)],[p174,c38]) ).
cnf(p255,plain,
( skc14 = skc15
| ~ ssSkC0
| ~ seat(skc16)
| ~ furniture(skc16) ),
inference(resolution,[status(thm)],[p254,p186]) ).
cnf(f39,negated_conjecture,
( furniture(skc16)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
fof(f39_nnf,plain,
( furniture(skc16)
| ~ ssSkC0 ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
( furniture(skc16)
| ~ ssSkC0 ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( furniture(skc16)
| ~ ssSkC0 ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p187,plain,
furniture(skc16),
inference(resolution,[status(thm)],[p174,c39]) ).
cnf(p256,plain,
( skc14 = skc15
| ~ ssSkC0
| ~ seat(skc16) ),
inference(resolution,[status(thm)],[p255,p187]) ).
cnf(f11,negated_conjecture,
seat(skc16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
fof(f11_nnf,plain,
seat(skc16),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
seat(skc16),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(p259,plain,
( skc14 = skc15
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[p256,c11]) ).
cnf(p260,plain,
skc14 = skc15,
inference(resolution,[status(thm)],[p259,p174]) ).
cnf(f51,negated_conjecture,
( ~ ssSkC0
| skc15 != skc14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
fof(f51_nnf,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(p261,plain,
( ~ ssSkC0
| skc15 != skc15 ),
inference(demodulation,[status(thm)],[p260,c51]) ).
cnf(p262,plain,
~ ssSkC0,
inference(equality_resolution,[status(thm)],[p261]) ).
cnf(p263,plain,
$false,
inference(resolution,[status(thm)],[p262,p174]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP009-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.59 % Computer : n002.cluster.edu
% 0.10/5.59 % Model : x86_64 x86_64
% 0.10/5.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.59 % Memory : 8046.5625MB
% 0.10/5.59 % OS : Linux 6.8.0-71-generic
% 0.10/5.59 % CPULimit : 300
% 0.10/5.59 % WCLimit : 300
% 0.10/5.59 % DateTime : Thu Sep 24 01:40:56 UTC 2026
% 0.10/5.59 % CPUTime :
% 0.10/5.59 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 4.21/6.37 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.21/6.37 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------