%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NLP009-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:07:14 AM UTC 2026
% Result : Unsatisfiable 0.82s 0.47s
% Output : CNFRefutation 0.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 107
% Number of leaves : 54
% Syntax : Number of formulae : 257 ( 50 unt; 0 def)
% Number of atoms : 1751 ( 193 equ)
% Maximal formula atoms : 27 ( 6 avg)
% Number of connectives : 2820 (1326 ~;1494 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 7 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 : 122 ( 0 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(clause53,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( VAR_5 = VAR_4
| ssSkC0
| ~ seat(VAR_6)
| ~ furniture(VAR_6)
| ~ front(VAR_6)
| ~ in(VAR_5,VAR_6)
| ~ in(VAR_4,VAR_6)
| ~ young(VAR_5)
| ~ man(VAR_5)
| ~ fellow(VAR_5)
| ~ fellow(VAR_4)
| ~ man(VAR_4)
| ~ young(VAR_4)
| ~ hollywood(VAR_3)
| ~ city(VAR_3)
| ~ in(VAR_2,VAR_3)
| ~ down(VAR_2,VAR_0)
| ~ barrel(VAR_2,VAR_1)
| ~ event(VAR_2)
| ~ chevy(VAR_1)
| ~ car(VAR_1)
| ~ white(VAR_1)
| ~ dirty(VAR_1)
| ~ old(VAR_1)
| ~ lonely(VAR_0)
| ~ way(VAR_0)
| ~ street(VAR_0) ),
file('theBenchmark.p',clause53) ).
cnf(c_1,plain,
( F = E
| ssSkC0
| ~ seat(V6)
| ~ furniture(V6)
| ~ front(V6)
| ~ in(F,V6)
| ~ in(E,V6)
| ~ young(F)
| ~ man(F)
| ~ fellow(F)
| ~ fellow(E)
| ~ man(E)
| ~ young(E)
| ~ hollywood(D)
| ~ city(D)
| ~ in(C,D)
| ~ down(C,A)
| ~ barrel(C,B)
| ~ event(C)
| ~ chevy(B)
| ~ car(B)
| ~ white(B)
| ~ dirty(B)
| ~ old(B)
| ~ lonely(A)
| ~ way(A)
| ~ street(A) ),
inference(clausify,[status(thm)],[clause53]) ).
fof(clause8,axiom,
hollywood(skc20),
file('theBenchmark.p',clause8) ).
cnf(c_2,plain,
hollywood(skc20),
inference(clausify,[status(thm)],[clause8]) ).
fof(clause1,axiom,
hollywood(skc27),
file('theBenchmark.p',clause1) ).
cnf(c_3,plain,
hollywood(skc27),
inference(clausify,[status(thm)],[clause1]) ).
fof(clause54,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( VAR_5 = VAR_4
| ~ ssSkC0
| ~ seat(VAR_6)
| ~ furniture(VAR_6)
| ~ front(VAR_6)
| ~ in(VAR_5,VAR_6)
| ~ in(VAR_4,VAR_6)
| ~ young(VAR_5)
| ~ man(VAR_5)
| ~ fellow(VAR_5)
| ~ fellow(VAR_4)
| ~ man(VAR_4)
| ~ young(VAR_4)
| ~ hollywood(VAR_3)
| ~ city(VAR_3)
| ~ in(VAR_2,VAR_3)
| ~ down(VAR_2,VAR_1)
| ~ barrel(VAR_2,VAR_0)
| ~ event(VAR_2)
| ~ street(VAR_1)
| ~ way(VAR_1)
| ~ lonely(VAR_1)
| ~ old(VAR_0)
| ~ dirty(VAR_0)
| ~ white(VAR_0)
| ~ car(VAR_0)
| ~ chevy(VAR_0) ),
file('theBenchmark.p',clause54) ).
cnf(c_4,plain,
( F = E
| ~ ssSkC0
| ~ seat(V6)
| ~ furniture(V6)
| ~ front(V6)
| ~ in(F,V6)
| ~ in(E,V6)
| ~ young(F)
| ~ man(F)
| ~ fellow(F)
| ~ fellow(E)
| ~ man(E)
| ~ young(E)
| ~ hollywood(D)
| ~ city(D)
| ~ in(C,D)
| ~ down(C,B)
| ~ barrel(C,A)
| ~ event(C)
| ~ street(B)
| ~ way(B)
| ~ lonely(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A) ),
inference(clausify,[status(thm)],[clause54]) ).
fof(clause9,axiom,
event(skc19),
file('theBenchmark.p',clause9) ).
cnf(c_5,plain,
event(skc19),
inference(clausify,[status(thm)],[clause9]) ).
cnf(c_7,plain,
( E = D
| ssSkC0
| ~ seat(F)
| ~ furniture(F)
| ~ front(F)
| ~ in(E,F)
| ~ in(D,F)
| ~ young(E)
| ~ man(E)
| ~ fellow(E)
| ~ fellow(D)
| ~ man(D)
| ~ young(D)
| ~ city(skc27)
| ~ in(C,skc27)
| ~ down(C,A)
| ~ barrel(C,B)
| ~ event(C)
| ~ chevy(B)
| ~ car(B)
| ~ white(B)
| ~ dirty(B)
| ~ old(B)
| ~ lonely(A)
| ~ way(A)
| ~ street(A) ),
inference(resolve,[status(thm)],[c_1,c_3]) ).
cnf(c_8,plain,
( E = D
| ~ ssSkC0
| ~ seat(F)
| ~ furniture(F)
| ~ front(F)
| ~ in(E,F)
| ~ in(D,F)
| ~ young(E)
| ~ man(E)
| ~ fellow(E)
| ~ fellow(D)
| ~ man(D)
| ~ young(D)
| ~ city(skc20)
| ~ in(C,skc20)
| ~ down(C,B)
| ~ barrel(C,A)
| ~ event(C)
| ~ street(B)
| ~ way(B)
| ~ lonely(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A) ),
inference(resolve,[status(thm)],[c_4,c_2]) ).
fof(clause2,axiom,
event(skc26),
file('theBenchmark.p',clause2) ).
cnf(c_10,plain,
event(skc26),
inference(clausify,[status(thm)],[clause2]) ).
fof(clause3,axiom,
street(skc25),
file('theBenchmark.p',clause3) ).
cnf(c_11,plain,
street(skc25),
inference(clausify,[status(thm)],[clause3]) ).
cnf(c_14,plain,
( D = C
| ~ ssSkC0
| ~ seat(E)
| ~ furniture(E)
| ~ front(E)
| ~ in(D,E)
| ~ in(C,E)
| ~ young(D)
| ~ man(D)
| ~ fellow(D)
| ~ fellow(C)
| ~ man(C)
| ~ young(C)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,B)
| ~ barrel(skc19,A)
| ~ street(B)
| ~ way(B)
| ~ lonely(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A) ),
inference(resolve,[status(thm)],[c_5,c_8]) ).
cnf(c_17,plain,
( D = C
| ssSkC0
| ~ seat(E)
| ~ furniture(E)
| ~ front(E)
| ~ in(D,E)
| ~ in(C,E)
| ~ young(D)
| ~ man(D)
| ~ fellow(D)
| ~ fellow(C)
| ~ man(C)
| ~ young(C)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ down(skc26,A)
| ~ barrel(skc26,B)
| ~ chevy(B)
| ~ car(B)
| ~ white(B)
| ~ dirty(B)
| ~ old(B)
| ~ lonely(A)
| ~ way(A)
| ~ street(A) ),
inference(resolve,[status(thm)],[c_10,c_7]) ).
fof(clause28,axiom,
( street(skc17)
| ~ ssSkC0 ),
file('theBenchmark.p',clause28) ).
cnf(c_20,plain,
( street(skc17)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause28]) ).
fof(clause30,axiom,
( old(skc18)
| ~ ssSkC0 ),
file('theBenchmark.p',clause30) ).
cnf(c_21,plain,
( old(skc18)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause30]) ).
cnf(c_27,plain,
( C = B
| ssSkC0
| ~ seat(D)
| ~ furniture(D)
| ~ front(D)
| ~ in(C,D)
| ~ in(B,D)
| ~ young(C)
| ~ man(C)
| ~ fellow(C)
| ~ fellow(B)
| ~ man(B)
| ~ young(B)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ down(skc26,skc25)
| ~ barrel(skc26,A)
| ~ chevy(A)
| ~ car(A)
| ~ white(A)
| ~ dirty(A)
| ~ old(A)
| ~ lonely(skc25)
| ~ way(skc25) ),
inference(resolve,[status(thm)],[c_11,c_17]) ).
cnf(c_30,plain,
( C = B
| ~ ssSkC0
| ~ seat(D)
| ~ furniture(D)
| ~ front(D)
| ~ in(C,D)
| ~ in(B,D)
| ~ young(C)
| ~ man(C)
| ~ fellow(C)
| ~ fellow(B)
| ~ man(B)
| ~ young(B)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,skc17)
| ~ barrel(skc19,A)
| ~ way(skc17)
| ~ lonely(skc17)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ ssSkC0 ),
inference(resolve,[status(thm)],[c_20,c_14]) ).
fof(clause4,axiom,
old(skc24),
file('theBenchmark.p',clause4) ).
cnf(c_34,plain,
old(skc24),
inference(clausify,[status(thm)],[clause4]) ).
fof(clause5,axiom,
seat(skc23),
file('theBenchmark.p',clause5) ).
cnf(c_35,plain,
seat(skc23),
inference(clausify,[status(thm)],[clause5]) ).
cnf(c_40,plain,
( B = A
| ~ ssSkC0
| ~ seat(C)
| ~ furniture(C)
| ~ front(C)
| ~ in(B,C)
| ~ in(A,C)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| ~ way(skc17)
| ~ lonely(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ chevy(skc18)
| ~ ssSkC0
| ~ ssSkC0 ),
inference(resolve,[status(thm)],[c_21,c_30]) ).
cnf(c_49,plain,
( B = A
| ssSkC0
| ~ seat(C)
| ~ furniture(C)
| ~ front(C)
| ~ in(B,C)
| ~ in(A,C)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ down(skc26,skc25)
| ~ barrel(skc26,skc24)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25) ),
inference(resolve,[status(thm)],[c_34,c_27]) ).
fof(clause12,axiom,
seat(skc16),
file('theBenchmark.p',clause12) ).
cnf(c_56,plain,
seat(skc16),
inference(clausify,[status(thm)],[clause12]) ).
cnf(c_79,plain,
( B = A
| ~ ssSkC0
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| ~ way(skc17)
| ~ lonely(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ chevy(skc18)
| ~ ssSkC0
| ~ ssSkC0 ),
inference(resolve,[status(thm)],[c_56,c_40]) ).
cnf(c_339,plain,
( B = A
| ~ ssSkC0
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| ~ way(skc17)
| ~ lonely(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ chevy(skc18)
| ~ ssSkC0 ),
inference(copy,[status(thm)],[c_79]) ).
cnf(c_80,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| ~ way(skc17)
| ~ lonely(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ chevy(skc18)
| ~ ssSkC0 ),
inference(copy,[status(thm)],[c_339]) ).
cnf(c_99,plain,
( B = A
| ssSkC0
| ~ furniture(skc23)
| ~ front(skc23)
| ~ in(B,skc23)
| ~ in(A,skc23)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ down(skc26,skc25)
| ~ barrel(skc26,skc24)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25) ),
inference(resolve,[status(thm)],[c_35,c_49]) ).
fof(clause52,axiom,
( ~ ssSkC0
| skc15 != skc14 ),
file('theBenchmark.p',clause52) ).
cnf(c_121,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(clausify,[status(thm)],[clause52]) ).
fof(clause51,axiom,
( ssSkC0
| skc22 != skc21 ),
file('theBenchmark.p',clause51) ).
cnf(c_122,plain,
( ssSkC0
| skc22 != skc21 ),
inference(clausify,[status(thm)],[clause51]) ).
fof(clause50,axiom,
( in(skc15,skc16)
| ~ ssSkC0 ),
file('theBenchmark.p',clause50) ).
cnf(c_123,plain,
( in(skc15,skc16)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause50]) ).
fof(clause49,axiom,
( in(skc14,skc16)
| ~ ssSkC0 ),
file('theBenchmark.p',clause49) ).
cnf(c_124,plain,
( in(skc14,skc16)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause49]) ).
fof(clause48,axiom,
( in(skc19,skc20)
| ~ ssSkC0 ),
file('theBenchmark.p',clause48) ).
cnf(c_125,plain,
( in(skc19,skc20)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause48]) ).
fof(clause47,axiom,
( down(skc19,skc17)
| ~ ssSkC0 ),
file('theBenchmark.p',clause47) ).
cnf(c_126,plain,
( down(skc19,skc17)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause47]) ).
fof(clause46,axiom,
( barrel(skc19,skc18)
| ~ ssSkC0 ),
file('theBenchmark.p',clause46) ).
cnf(c_127,plain,
( barrel(skc19,skc18)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause46]) ).
fof(clause45,axiom,
( in(skc22,skc23)
| ssSkC0 ),
file('theBenchmark.p',clause45) ).
cnf(c_128,plain,
( in(skc22,skc23)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause45]) ).
fof(clause44,axiom,
( in(skc21,skc23)
| ssSkC0 ),
file('theBenchmark.p',clause44) ).
cnf(c_129,plain,
( in(skc21,skc23)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause44]) ).
fof(clause43,axiom,
( in(skc26,skc27)
| ssSkC0 ),
file('theBenchmark.p',clause43) ).
cnf(c_130,plain,
( in(skc26,skc27)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause43]) ).
fof(clause42,axiom,
( down(skc26,skc25)
| ssSkC0 ),
file('theBenchmark.p',clause42) ).
cnf(c_131,plain,
( down(skc26,skc25)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause42]) ).
fof(clause41,axiom,
( barrel(skc26,skc24)
| ssSkC0 ),
file('theBenchmark.p',clause41) ).
cnf(c_132,plain,
( barrel(skc26,skc24)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause41]) ).
fof(clause40,axiom,
( furniture(skc16)
| ~ ssSkC0 ),
file('theBenchmark.p',clause40) ).
cnf(c_133,plain,
( furniture(skc16)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause40]) ).
fof(clause39,axiom,
( front(skc16)
| ~ ssSkC0 ),
file('theBenchmark.p',clause39) ).
cnf(c_134,plain,
( front(skc16)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause39]) ).
fof(clause38,axiom,
( man(skc15)
| ~ ssSkC0 ),
file('theBenchmark.p',clause38) ).
cnf(c_135,plain,
( man(skc15)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause38]) ).
fof(clause37,axiom,
( fellow(skc15)
| ~ ssSkC0 ),
file('theBenchmark.p',clause37) ).
cnf(c_136,plain,
( fellow(skc15)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause37]) ).
fof(clause36,axiom,
( man(skc14)
| ~ ssSkC0 ),
file('theBenchmark.p',clause36) ).
cnf(c_137,plain,
( man(skc14)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause36]) ).
fof(clause35,axiom,
( young(skc14)
| ~ ssSkC0 ),
file('theBenchmark.p',clause35) ).
cnf(c_138,plain,
( young(skc14)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause35]) ).
fof(clause34,axiom,
( city(skc20)
| ~ ssSkC0 ),
file('theBenchmark.p',clause34) ).
cnf(c_139,plain,
( city(skc20)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause34]) ).
fof(clause33,axiom,
( car(skc18)
| ~ ssSkC0 ),
file('theBenchmark.p',clause33) ).
cnf(c_140,plain,
( car(skc18)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause33]) ).
fof(clause32,axiom,
( white(skc18)
| ~ ssSkC0 ),
file('theBenchmark.p',clause32) ).
cnf(c_141,plain,
( white(skc18)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause32]) ).
fof(clause31,axiom,
( dirty(skc18)
| ~ ssSkC0 ),
file('theBenchmark.p',clause31) ).
cnf(c_142,plain,
( dirty(skc18)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause31]) ).
fof(clause29,axiom,
( way(skc17)
| ~ ssSkC0 ),
file('theBenchmark.p',clause29) ).
cnf(c_143,plain,
( way(skc17)
| ~ ssSkC0 ),
inference(clausify,[status(thm)],[clause29]) ).
fof(clause27,axiom,
( furniture(skc23)
| ssSkC0 ),
file('theBenchmark.p',clause27) ).
cnf(c_144,plain,
( furniture(skc23)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause27]) ).
fof(clause26,axiom,
( front(skc23)
| ssSkC0 ),
file('theBenchmark.p',clause26) ).
cnf(c_145,plain,
( front(skc23)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause26]) ).
fof(clause25,axiom,
( man(skc22)
| ssSkC0 ),
file('theBenchmark.p',clause25) ).
cnf(c_146,plain,
( man(skc22)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause25]) ).
fof(clause24,axiom,
( fellow(skc22)
| ssSkC0 ),
file('theBenchmark.p',clause24) ).
cnf(c_147,plain,
( fellow(skc22)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause24]) ).
fof(clause23,axiom,
( man(skc21)
| ssSkC0 ),
file('theBenchmark.p',clause23) ).
cnf(c_148,plain,
( man(skc21)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause23]) ).
fof(clause22,axiom,
( young(skc21)
| ssSkC0 ),
file('theBenchmark.p',clause22) ).
cnf(c_149,plain,
( young(skc21)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause22]) ).
fof(clause21,axiom,
( city(skc27)
| ssSkC0 ),
file('theBenchmark.p',clause21) ).
cnf(c_150,plain,
( city(skc27)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause21]) ).
fof(clause20,axiom,
( way(skc25)
| ssSkC0 ),
file('theBenchmark.p',clause20) ).
cnf(c_151,plain,
( way(skc25)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause20]) ).
fof(clause19,axiom,
( lonely(skc25)
| ssSkC0 ),
file('theBenchmark.p',clause19) ).
cnf(c_152,plain,
( lonely(skc25)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause19]) ).
fof(clause18,axiom,
( dirty(skc24)
| ssSkC0 ),
file('theBenchmark.p',clause18) ).
cnf(c_153,plain,
( dirty(skc24)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause18]) ).
fof(clause17,axiom,
( white(skc24)
| ssSkC0 ),
file('theBenchmark.p',clause17) ).
cnf(c_154,plain,
( white(skc24)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause17]) ).
fof(clause16,axiom,
( car(skc24)
| ssSkC0 ),
file('theBenchmark.p',clause16) ).
cnf(c_155,plain,
( car(skc24)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause16]) ).
fof(clause15,axiom,
( chevy(skc24)
| ssSkC0 ),
file('theBenchmark.p',clause15) ).
cnf(c_156,plain,
( chevy(skc24)
| ssSkC0 ),
inference(clausify,[status(thm)],[clause15]) ).
fof(clause14,axiom,
fellow(skc14),
file('theBenchmark.p',clause14) ).
cnf(c_157,plain,
fellow(skc14),
inference(clausify,[status(thm)],[clause14]) ).
fof(clause13,axiom,
young(skc15),
file('theBenchmark.p',clause13) ).
cnf(c_158,plain,
young(skc15),
inference(clausify,[status(thm)],[clause13]) ).
fof(clause11,axiom,
lonely(skc17),
file('theBenchmark.p',clause11) ).
cnf(c_159,plain,
lonely(skc17),
inference(clausify,[status(thm)],[clause11]) ).
fof(clause10,axiom,
chevy(skc18),
file('theBenchmark.p',clause10) ).
cnf(c_160,plain,
chevy(skc18),
inference(clausify,[status(thm)],[clause10]) ).
fof(clause7,axiom,
fellow(skc21),
file('theBenchmark.p',clause7) ).
cnf(c_161,plain,
fellow(skc21),
inference(clausify,[status(thm)],[clause7]) ).
fof(clause6,axiom,
young(skc22),
file('theBenchmark.p',clause6) ).
cnf(c_162,plain,
young(skc22),
inference(clausify,[status(thm)],[clause6]) ).
cnf(c_340,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| ~ way(skc17)
| ~ lonely(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0 ),
inference(resolve,[status(thm)],[c_160,c_80]) ).
cnf(c_171,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0 ),
inference(resolve,[status(thm)],[c_159,c_340]) ).
cnf(c_341,plain,
( B = A
| ssSkC0
| ~ furniture(skc23)
| ~ front(skc23)
| ~ in(B,skc23)
| ~ in(A,skc23)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ barrel(skc26,skc24)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_131,c_99]) ).
cnf(c_188,plain,
( B = A
| ~ furniture(skc23)
| ~ front(skc23)
| ~ in(B,skc23)
| ~ in(A,skc23)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ barrel(skc26,skc24)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(copy,[status(thm)],[c_341]) ).
cnf(c_342,plain,
( ssSkC0
| B = A
| ~ furniture(skc23)
| ~ front(skc23)
| ~ in(B,skc23)
| ~ in(A,skc23)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_188,c_132]) ).
cnf(c_195,plain,
( B = A
| ~ furniture(skc23)
| ~ front(skc23)
| ~ in(B,skc23)
| ~ in(A,skc23)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(copy,[status(thm)],[c_342]) ).
cnf(c_343,plain,
( ssSkC0
| A = skc21
| ~ furniture(skc23)
| ~ front(skc23)
| ~ in(A,skc23)
| ~ young(A)
| ~ man(A)
| ~ fellow(A)
| ~ fellow(skc21)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_195,c_129]) ).
cnf(c_344,plain,
( ssSkC0
| skc21 = A
| ~ furniture(skc23)
| ~ front(skc23)
| ~ in(A,skc23)
| ~ young(A)
| ~ man(A)
| ~ fellow(A)
| ~ fellow(skc21)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(copy,[status(thm)],[c_343]) ).
cnf(c_345,plain,
( skc21 = A
| ~ furniture(skc23)
| ~ front(skc23)
| ~ in(A,skc23)
| ~ young(A)
| ~ man(A)
| ~ fellow(A)
| ~ fellow(skc21)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(copy,[status(thm)],[c_344]) ).
cnf(c_197,plain,
( skc21 = A
| ~ furniture(skc23)
| ~ front(skc23)
| ~ in(A,skc23)
| ~ young(A)
| ~ man(A)
| ~ fellow(A)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_161,c_345]) ).
cnf(c_346,plain,
( ssSkC0
| skc21 = skc22
| ~ furniture(skc23)
| ~ front(skc23)
| ~ young(skc22)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_197,c_128]) ).
cnf(c_347,plain,
( ssSkC0
| skc22 = skc21
| ~ furniture(skc23)
| ~ front(skc23)
| ~ young(skc22)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(copy,[status(thm)],[c_346]) ).
cnf(c_348,plain,
( skc22 = skc21
| ~ furniture(skc23)
| ~ front(skc23)
| ~ young(skc22)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(copy,[status(thm)],[c_347]) ).
cnf(c_200,plain,
( skc22 = skc21
| ~ furniture(skc23)
| ~ front(skc23)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ in(skc26,skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_162,c_348]) ).
cnf(c_349,plain,
( ssSkC0
| skc22 = skc21
| ~ furniture(skc23)
| ~ front(skc23)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_200,c_130]) ).
cnf(c_201,plain,
( skc22 = skc21
| ~ furniture(skc23)
| ~ front(skc23)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ white(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(copy,[status(thm)],[c_349]) ).
cnf(c_350,plain,
( ssSkC0
| skc22 = skc21
| ~ furniture(skc23)
| ~ front(skc23)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_201,c_154]) ).
cnf(c_202,plain,
( skc22 = skc21
| ~ furniture(skc23)
| ~ front(skc23)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ~ way(skc25)
| ssSkC0 ),
inference(copy,[status(thm)],[c_350]) ).
cnf(c_351,plain,
( ssSkC0
| skc22 = skc21
| ~ furniture(skc23)
| ~ front(skc23)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_202,c_151]) ).
cnf(c_204,plain,
( skc22 = skc21
| ~ furniture(skc23)
| ~ front(skc23)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ lonely(skc25)
| ssSkC0 ),
inference(copy,[status(thm)],[c_351]) ).
cnf(c_352,plain,
( ssSkC0
| skc22 = skc21
| ~ furniture(skc23)
| ~ front(skc23)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_204,c_152]) ).
cnf(c_205,plain,
( skc22 = skc21
| ~ furniture(skc23)
| ~ front(skc23)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ssSkC0 ),
inference(copy,[status(thm)],[c_352]) ).
cnf(c_353,plain,
( ssSkC0
| skc22 = skc21
| ~ front(skc23)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_205,c_144]) ).
cnf(c_206,plain,
( skc22 = skc21
| ~ front(skc23)
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ssSkC0 ),
inference(copy,[status(thm)],[c_353]) ).
cnf(c_354,plain,
( ssSkC0
| skc22 = skc21
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_206,c_145]) ).
cnf(c_207,plain,
( skc22 = skc21
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ssSkC0 ),
inference(copy,[status(thm)],[c_354]) ).
cnf(c_355,plain,
( ssSkC0
| skc22 = skc21
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_207,c_153]) ).
cnf(c_209,plain,
( skc22 = skc21
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ city(skc27)
| ~ chevy(skc24)
| ~ car(skc24)
| ssSkC0 ),
inference(copy,[status(thm)],[c_355]) ).
cnf(c_356,plain,
( ssSkC0
| skc22 = skc21
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ chevy(skc24)
| ~ car(skc24)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_209,c_150]) ).
cnf(c_210,plain,
( skc22 = skc21
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ chevy(skc24)
| ~ car(skc24)
| ssSkC0 ),
inference(copy,[status(thm)],[c_356]) ).
cnf(c_357,plain,
( ssSkC0
| skc22 = skc21
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ car(skc24)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_210,c_156]) ).
cnf(c_211,plain,
( skc22 = skc21
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ~ car(skc24)
| ssSkC0 ),
inference(copy,[status(thm)],[c_357]) ).
cnf(c_358,plain,
( ssSkC0
| skc22 = skc21
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_211,c_155]) ).
cnf(c_212,plain,
( skc22 = skc21
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ~ young(skc21)
| ssSkC0 ),
inference(copy,[status(thm)],[c_358]) ).
cnf(c_359,plain,
( ssSkC0
| skc22 = skc21
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_212,c_149]) ).
cnf(c_214,plain,
( skc22 = skc21
| ~ man(skc22)
| ~ fellow(skc22)
| ~ man(skc21)
| ssSkC0 ),
inference(copy,[status(thm)],[c_359]) ).
cnf(c_360,plain,
( ssSkC0
| skc22 = skc21
| ~ fellow(skc22)
| ~ man(skc21)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_214,c_146]) ).
cnf(c_215,plain,
( skc22 = skc21
| ~ fellow(skc22)
| ~ man(skc21)
| ssSkC0 ),
inference(copy,[status(thm)],[c_360]) ).
cnf(c_361,plain,
( ssSkC0
| skc22 = skc21
| ~ fellow(skc22)
| ssSkC0 ),
inference(resolve,[status(thm)],[c_215,c_148]) ).
cnf(c_216,plain,
( skc22 = skc21
| ~ fellow(skc22)
| ssSkC0 ),
inference(copy,[status(thm)],[c_361]) ).
cnf(c_362,plain,
( ssSkC0
| skc22 = skc21
| ssSkC0 ),
inference(resolve,[status(thm)],[c_216,c_147]) ).
cnf(c_217,plain,
( skc22 = skc21
| ssSkC0 ),
inference(copy,[status(thm)],[c_362]) ).
cnf(c_218,plain,
( way(skc17)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_143]) ).
cnf(c_219,plain,
( dirty(skc18)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_142]) ).
cnf(c_220,plain,
( white(skc18)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_141]) ).
cnf(c_221,plain,
( car(skc18)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_140]) ).
cnf(c_222,plain,
( city(skc20)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_139]) ).
cnf(c_223,plain,
( young(skc14)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_138]) ).
cnf(c_224,plain,
( man(skc14)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_137]) ).
cnf(c_225,plain,
( fellow(skc15)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_136]) ).
cnf(c_226,plain,
( man(skc15)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_135]) ).
cnf(c_227,plain,
( front(skc16)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_134]) ).
cnf(c_228,plain,
( furniture(skc16)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_133]) ).
cnf(c_229,plain,
( barrel(skc19,skc18)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_127]) ).
cnf(c_230,plain,
( down(skc19,skc17)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_126]) ).
cnf(c_231,plain,
( in(skc19,skc20)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_125]) ).
cnf(c_232,plain,
( in(skc14,skc16)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_124]) ).
cnf(c_233,plain,
( in(skc15,skc16)
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_123]) ).
cnf(c_234,plain,
( skc15 != skc14
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_217,c_121]) ).
cnf(c_239,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ barrel(skc19,skc18)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_230,c_171]) ).
cnf(c_363,plain,
( skc22 = skc21
| B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_239,c_229]) ).
cnf(c_260,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_363]) ).
cnf(c_364,plain,
( skc22 = skc21
| A = skc15
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(A,skc16)
| ~ young(A)
| ~ man(A)
| ~ fellow(A)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ young(skc15)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_260,c_233]) ).
cnf(c_365,plain,
( skc22 = skc21
| skc15 = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(A,skc16)
| ~ young(A)
| ~ man(A)
| ~ fellow(A)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ young(skc15)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_364]) ).
cnf(c_366,plain,
( skc15 = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(A,skc16)
| ~ young(A)
| ~ man(A)
| ~ fellow(A)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ young(skc15)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_365]) ).
cnf(c_262,plain,
( skc15 = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(A,skc16)
| ~ young(A)
| ~ man(A)
| ~ fellow(A)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_158,c_366]) ).
cnf(c_367,plain,
( skc22 = skc21
| skc15 = skc14
| ~ furniture(skc16)
| ~ front(skc16)
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_262,c_232]) ).
cnf(c_368,plain,
( skc15 = skc14
| ~ furniture(skc16)
| ~ front(skc16)
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_367]) ).
cnf(c_266,plain,
( skc15 = skc14
| ~ furniture(skc16)
| ~ front(skc16)
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_157,c_368]) ).
cnf(c_369,plain,
( skc22 = skc21
| skc15 = skc14
| ~ furniture(skc16)
| ~ front(skc16)
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_266,c_231]) ).
cnf(c_267,plain,
( skc15 = skc14
| ~ furniture(skc16)
| ~ front(skc16)
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_369]) ).
cnf(c_370,plain,
( skc22 = skc21
| skc15 = skc14
| ~ furniture(skc16)
| ~ front(skc16)
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_267,c_220]) ).
cnf(c_268,plain,
( skc15 = skc14
| ~ furniture(skc16)
| ~ front(skc16)
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_370]) ).
cnf(c_371,plain,
( skc22 = skc21
| skc15 = skc14
| ~ furniture(skc16)
| ~ front(skc16)
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ dirty(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_268,c_218]) ).
cnf(c_269,plain,
( skc15 = skc14
| ~ furniture(skc16)
| ~ front(skc16)
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ dirty(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_371]) ).
cnf(c_372,plain,
( skc22 = skc21
| skc15 = skc14
| ~ front(skc16)
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ dirty(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_269,c_228]) ).
cnf(c_270,plain,
( skc15 = skc14
| ~ front(skc16)
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ dirty(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_372]) ).
cnf(c_373,plain,
( skc22 = skc21
| skc15 = skc14
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ dirty(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_270,c_227]) ).
cnf(c_271,plain,
( skc15 = skc14
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ dirty(skc18)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_373]) ).
cnf(c_374,plain,
( skc22 = skc21
| skc15 = skc14
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_271,c_219]) ).
cnf(c_272,plain,
( skc15 = skc14
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ city(skc20)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_374]) ).
cnf(c_375,plain,
( skc22 = skc21
| skc15 = skc14
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_272,c_222]) ).
cnf(c_273,plain,
( skc15 = skc14
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ car(skc18)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_375]) ).
cnf(c_376,plain,
( skc22 = skc21
| skc15 = skc14
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_273,c_221]) ).
cnf(c_275,plain,
( skc15 = skc14
| ~ young(skc14)
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_376]) ).
cnf(c_377,plain,
( skc22 = skc21
| skc15 = skc14
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_275,c_223]) ).
cnf(c_276,plain,
( skc15 = skc14
| ~ man(skc14)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_377]) ).
cnf(c_378,plain,
( skc22 = skc21
| skc15 = skc14
| ~ man(skc14)
| ~ fellow(skc15)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_276,c_226]) ).
cnf(c_277,plain,
( skc15 = skc14
| ~ man(skc14)
| ~ fellow(skc15)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_378]) ).
cnf(c_379,plain,
( skc22 = skc21
| skc15 = skc14
| ~ fellow(skc15)
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_277,c_224]) ).
cnf(c_278,plain,
( skc15 = skc14
| ~ fellow(skc15)
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_379]) ).
cnf(c_380,plain,
( skc22 = skc21
| skc15 = skc14
| ~ ssSkC0
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_278,c_225]) ).
cnf(c_280,plain,
( skc15 = skc14
| ~ ssSkC0
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_380]) ).
cnf(c_381,plain,
( skc22 = skc21
| skc15 = skc14
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_280,c_217]) ).
cnf(c_281,plain,
( skc15 = skc14
| skc22 = skc21 ),
inference(copy,[status(thm)],[c_381]) ).
cnf(c_382,plain,
( skc22 = skc21
| skc22 = skc21 ),
inference(resolve,[status(thm)],[c_281,c_234]) ).
cnf(c_282,plain,
skc22 = skc21,
inference(copy,[status(thm)],[c_382]) ).
cnf(c_383,plain,
( ssSkC0
| skc21 != skc21 ),
inference(paramod,[status(thm)],[c_282,c_122]) ).
cnf(c_286,plain,
ssSkC0,
inference(copy,[status(thm)],[c_383]) ).
cnf(c_302,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18)
| ~ car(skc18) ),
inference(resolve,[status(thm)],[c_286,c_171]) ).
cnf(c_311,plain,
way(skc17),
inference(resolve,[status(thm)],[c_286,c_143]) ).
cnf(c_312,plain,
dirty(skc18),
inference(resolve,[status(thm)],[c_286,c_142]) ).
cnf(c_313,plain,
white(skc18),
inference(resolve,[status(thm)],[c_286,c_141]) ).
cnf(c_314,plain,
car(skc18),
inference(resolve,[status(thm)],[c_286,c_140]) ).
cnf(c_315,plain,
city(skc20),
inference(resolve,[status(thm)],[c_286,c_139]) ).
cnf(c_316,plain,
young(skc14),
inference(resolve,[status(thm)],[c_286,c_138]) ).
cnf(c_317,plain,
man(skc14),
inference(resolve,[status(thm)],[c_286,c_137]) ).
cnf(c_318,plain,
fellow(skc15),
inference(resolve,[status(thm)],[c_286,c_136]) ).
cnf(c_319,plain,
man(skc15),
inference(resolve,[status(thm)],[c_286,c_135]) ).
cnf(c_320,plain,
front(skc16),
inference(resolve,[status(thm)],[c_286,c_134]) ).
cnf(c_321,plain,
furniture(skc16),
inference(resolve,[status(thm)],[c_286,c_133]) ).
cnf(c_322,plain,
barrel(skc19,skc18),
inference(resolve,[status(thm)],[c_286,c_127]) ).
cnf(c_323,plain,
down(skc19,skc17),
inference(resolve,[status(thm)],[c_286,c_126]) ).
cnf(c_324,plain,
in(skc19,skc20),
inference(resolve,[status(thm)],[c_286,c_125]) ).
cnf(c_325,plain,
in(skc14,skc16),
inference(resolve,[status(thm)],[c_286,c_124]) ).
cnf(c_326,plain,
in(skc15,skc16),
inference(resolve,[status(thm)],[c_286,c_123]) ).
cnf(c_327,plain,
skc15 != skc14,
inference(resolve,[status(thm)],[c_286,c_121]) ).
cnf(c_384,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| ~ way(skc17)
| ~ dirty(skc18)
| ~ white(skc18) ),
inference(resolve,[status(thm)],[c_314,c_302]) ).
cnf(c_385,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| ~ way(skc17)
| ~ dirty(skc18) ),
inference(resolve,[status(thm)],[c_313,c_384]) ).
cnf(c_386,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| ~ way(skc17) ),
inference(resolve,[status(thm)],[c_312,c_385]) ).
cnf(c_387,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18) ),
inference(resolve,[status(thm)],[c_311,c_386]) ).
cnf(c_388,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20)
| ~ down(skc19,skc17) ),
inference(resolve,[status(thm)],[c_322,c_387]) ).
cnf(c_389,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20)
| ~ in(skc19,skc20) ),
inference(resolve,[status(thm)],[c_323,c_388]) ).
cnf(c_390,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A)
| ~ city(skc20) ),
inference(resolve,[status(thm)],[c_324,c_389]) ).
cnf(c_391,plain,
( B = A
| ~ furniture(skc16)
| ~ front(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A) ),
inference(resolve,[status(thm)],[c_315,c_390]) ).
cnf(c_392,plain,
( B = A
| ~ furniture(skc16)
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A) ),
inference(resolve,[status(thm)],[c_320,c_391]) ).
cnf(c_335,plain,
( B = A
| ~ in(B,skc16)
| ~ in(A,skc16)
| ~ young(B)
| ~ man(B)
| ~ fellow(B)
| ~ fellow(A)
| ~ man(A)
| ~ young(A) ),
inference(resolve,[status(thm)],[c_321,c_392]) ).
cnf(c_393,plain,
( A = skc15
| ~ in(A,skc16)
| ~ in(skc15,skc16)
| ~ young(A)
| ~ man(A)
| ~ fellow(A)
| ~ fellow(skc15)
| ~ young(skc15) ),
inference(resolve,[status(thm)],[c_335,c_319]) ).
cnf(c_394,plain,
( A = skc15
| ~ in(A,skc16)
| ~ in(skc15,skc16)
| ~ young(A)
| ~ man(A)
| ~ fellow(A)
| ~ young(skc15) ),
inference(resolve,[status(thm)],[c_393,c_318]) ).
cnf(c_395,plain,
( skc14 = skc15
| ~ in(skc14,skc16)
| ~ in(skc15,skc16)
| ~ young(skc14)
| ~ man(skc14)
| ~ young(skc15) ),
inference(resolve,[status(thm)],[c_394,c_157]) ).
cnf(c_396,plain,
( skc14 = skc15
| ~ in(skc14,skc16)
| ~ in(skc15,skc16)
| ~ young(skc14)
| ~ young(skc15) ),
inference(resolve,[status(thm)],[c_395,c_317]) ).
cnf(c_397,plain,
( skc14 = skc15
| ~ in(skc14,skc16)
| ~ in(skc15,skc16)
| ~ young(skc15) ),
inference(resolve,[status(thm)],[c_396,c_316]) ).
cnf(c_398,plain,
( skc14 = skc15
| ~ in(skc14,skc16)
| ~ young(skc15) ),
inference(resolve,[status(thm)],[c_397,c_326]) ).
cnf(c_399,plain,
( skc14 = skc15
| ~ young(skc15) ),
inference(resolve,[status(thm)],[c_398,c_325]) ).
cnf(c_400,plain,
skc14 != skc15,
inference(copy,[status(thm)],[c_327]) ).
cnf(c_401,plain,
~ young(skc15),
inference(resolve,[status(thm)],[c_399,c_400]) ).
cnf(c_338,plain,
$false,
inference(resolve,[status(thm)],[c_158,c_401]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP009-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n020.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 00:24:04 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 4182451 was started by sandbox2 on n020,
% 0.08/0.36 % Sat Sep 26 00:24:04 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.36
% 0.08/0.36 % From the command line: assign(max_seconds, 300).
% 0.82/0.47
% 0.82/0.47 % SZS status Unsatisfiable for theBenchmark
% 0.82/0.47
% 0.82/0.47 % Proof 1 at 0.09 (+ 0.01) seconds.
% 0.82/0.47 % Length of proof is 140.
% 0.82/0.47 % Level of proof is 46.
% 0.82/0.47 % Maximum clause weight is 49.000.
% 0.82/0.47 % Given clauses 192.
% 0.82/0.47
% 0.82/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------