%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NLP147-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:45 AM UTC 2026
% Result : Unsatisfiable 0.11s 0.42s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 17
% Syntax : Number of formulae : 53 ( 8 unt; 0 def)
% Number of atoms : 98 ( 5 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 94 ( 49 ~; 45 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-4 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 84 ( 11 sgn 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(clause88,axiom,
! [VAR_0] :
( fellow(skc6,VAR_0)
| ~ member(skc6,VAR_0,skc7) ),
file('theBenchmark.p',clause88) ).
cnf(c_1,plain,
( fellow(skc6,A)
| ~ member(skc6,A,skc7) ),
inference(clausify,[status(thm)],[clause88]) ).
fof(clause2,axiom,
! [VAR_0,VAR_1] :
( man(VAR_0,VAR_1)
| ~ fellow(VAR_0,VAR_1) ),
file('theBenchmark.p',clause2) ).
cnf(c_2,plain,
( man(A,B)
| ~ fellow(A,B) ),
inference(clausify,[status(thm)],[clause2]) ).
cnf(c_4,plain,
( man(skc6,A)
| ~ member(skc6,A,skc7) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
fof(clause3,axiom,
! [VAR_0,VAR_1] :
( human_person(VAR_0,VAR_1)
| ~ man(VAR_0,VAR_1) ),
file('theBenchmark.p',clause3) ).
cnf(c_5,plain,
( human_person(A,B)
| ~ man(A,B) ),
inference(clausify,[status(thm)],[clause3]) ).
fof(clause4,axiom,
! [VAR_0,VAR_1] :
( organism(VAR_0,VAR_1)
| ~ human_person(VAR_0,VAR_1) ),
file('theBenchmark.p',clause4) ).
cnf(c_6,plain,
( organism(A,B)
| ~ human_person(A,B) ),
inference(clausify,[status(thm)],[clause4]) ).
cnf(c_7,plain,
( ~ member(skc6,A,skc7)
| human_person(skc6,A) ),
inference(resolve,[status(thm)],[c_5,c_4]) ).
fof(clause11,axiom,
! [VAR_0,VAR_1] :
( living(VAR_0,VAR_1)
| ~ organism(VAR_0,VAR_1) ),
file('theBenchmark.p',clause11) ).
cnf(c_10,plain,
( living(A,B)
| ~ organism(A,B) ),
inference(clausify,[status(thm)],[clause11]) ).
cnf(c_11,plain,
( ~ member(skc6,A,skc7)
| organism(skc6,A) ),
inference(resolve,[status(thm)],[c_6,c_7]) ).
fof(clause55,axiom,
! [VAR_0,VAR_1] :
( ~ nonliving(VAR_0,VAR_1)
| ~ living(VAR_0,VAR_1) ),
file('theBenchmark.p',clause55) ).
cnf(c_37,plain,
( ~ nonliving(A,B)
| ~ living(A,B) ),
inference(clausify,[status(thm)],[clause55]) ).
cnf(c_38,plain,
( ~ member(skc6,A,skc7)
| living(skc6,A) ),
inference(resolve,[status(thm)],[c_10,c_11]) ).
fof(clause60,axiom,
! [VAR_0,VAR_1] :
( member(VAR_0,skf10(VAR_1,VAR_0),VAR_1)
| ~ two(VAR_0,VAR_1) ),
file('theBenchmark.p',clause60) ).
cnf(c_55,plain,
( member(A,skf10(B,A),B)
| ~ two(A,B) ),
inference(clausify,[status(thm)],[clause60]) ).
fof(clause77,axiom,
two(skc6,skc7),
file('theBenchmark.p',clause77) ).
cnf(c_59,plain,
two(skc6,skc7),
inference(clausify,[status(thm)],[clause77]) ).
fof(clause30,axiom,
! [VAR_0,VAR_1] :
( artifact(VAR_0,VAR_1)
| ~ instrumentality(VAR_0,VAR_1) ),
file('theBenchmark.p',clause30) ).
cnf(c_89,plain,
( artifact(A,B)
| ~ instrumentality(A,B) ),
inference(clausify,[status(thm)],[clause30]) ).
fof(clause50,axiom,
! [VAR_0,VAR_1] :
( instrumentality(VAR_0,VAR_1)
| ~ furniture(VAR_0,VAR_1) ),
file('theBenchmark.p',clause50) ).
cnf(c_90,plain,
( instrumentality(A,B)
| ~ furniture(A,B) ),
inference(clausify,[status(thm)],[clause50]) ).
fof(clause31,axiom,
! [VAR_0,VAR_1] :
( object(VAR_0,VAR_1)
| ~ artifact(VAR_0,VAR_1) ),
file('theBenchmark.p',clause31) ).
cnf(c_92,plain,
( object(A,B)
| ~ artifact(A,B) ),
inference(clausify,[status(thm)],[clause31]) ).
cnf(c_93,plain,
( ~ furniture(A,B)
| artifact(A,B) ),
inference(resolve,[status(thm)],[c_89,c_90]) ).
cnf(c_97,plain,
( ~ furniture(A,B)
| object(A,B) ),
inference(resolve,[status(thm)],[c_92,c_93]) ).
fof(clause33,axiom,
! [VAR_0,VAR_1] :
( nonliving(VAR_0,VAR_1)
| ~ object(VAR_0,VAR_1) ),
file('theBenchmark.p',clause33) ).
cnf(c_104,plain,
( nonliving(A,B)
| ~ object(A,B) ),
inference(clausify,[status(thm)],[clause33]) ).
fof(clause89,axiom,
! [VAR_0,VAR_1] :
( frontseat(skc6,skf5(VAR_1))
| ~ member(skc6,VAR_0,skc7) ),
file('theBenchmark.p',clause89) ).
cnf(c_135,plain,
( frontseat(skc6,skf5(B))
| ~ member(skc6,A,skc7) ),
inference(clausify,[status(thm)],[clause89]) ).
fof(clause48,axiom,
! [VAR_0,VAR_1] :
( seat(VAR_0,VAR_1)
| ~ frontseat(VAR_0,VAR_1) ),
file('theBenchmark.p',clause48) ).
cnf(c_136,plain,
( seat(A,B)
| ~ frontseat(A,B) ),
inference(clausify,[status(thm)],[clause48]) ).
fof(clause49,axiom,
! [VAR_0,VAR_1] :
( furniture(VAR_0,VAR_1)
| ~ seat(VAR_0,VAR_1) ),
file('theBenchmark.p',clause49) ).
cnf(c_137,plain,
( furniture(A,B)
| ~ seat(A,B) ),
inference(clausify,[status(thm)],[clause49]) ).
cnf(c_138,plain,
( seat(skc6,skf5(B))
| ~ member(skc6,A,skc7) ),
inference(resolve,[status(thm)],[c_135,c_136]) ).
cnf(c_140,plain,
( ~ member(skc6,B,skc7)
| furniture(skc6,skf5(A)) ),
inference(resolve,[status(thm)],[c_137,c_138]) ).
cnf(c_141,plain,
( ~ furniture(A,B)
| nonliving(A,B) ),
inference(resolve,[status(thm)],[c_104,c_97]) ).
fof(clause92,axiom,
! [VAR_0] :
( be(skc6,skf6(VAR_0),VAR_0,skf5(VAR_0))
| ~ member(skc6,VAR_0,skc7) ),
file('theBenchmark.p',clause92) ).
cnf(c_148,plain,
( be(skc6,skf6(A),A,skf5(A))
| ~ member(skc6,A,skc7) ),
inference(clausify,[status(thm)],[clause92]) ).
fof(clause59,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_2 = VAR_3
| ~ be(VAR_0,VAR_1,VAR_2,VAR_3) ),
file('theBenchmark.p',clause59) ).
cnf(c_149,plain,
( C = D
| ~ be(A,B,C,D) ),
inference(clausify,[status(thm)],[clause59]) ).
cnf(c_150,plain,
( A = skf5(A)
| ~ member(skc6,A,skc7) ),
inference(resolve,[status(thm)],[c_148,c_149]) ).
cnf(c_151,plain,
( skf5(A) = A
| ~ member(skc6,A,skc7) ),
inference(copy,[status(thm)],[c_150]) ).
cnf(c_156,plain,
( ~ member(skc6,B,skc7)
| nonliving(skc6,skf5(A)) ),
inference(resolve,[status(thm)],[c_141,c_140]) ).
cnf(c_171,plain,
member(skc6,skf10(skc7,skc6),skc7),
inference(resolve,[status(thm)],[c_59,c_55]) ).
cnf(c_198,plain,
( ~ member(skc6,A,skc7)
| ~ nonliving(skc6,A) ),
inference(resolve,[status(thm)],[c_37,c_38]) ).
cnf(c_241,plain,
nonliving(skc6,skf5(A)),
inference(resolve,[status(thm)],[c_171,c_156]) ).
cnf(c_245,plain,
skf5(skf10(skc7,skc6)) = skf10(skc7,skc6),
inference(resolve,[status(thm)],[c_171,c_151]) ).
cnf(c_248,plain,
~ nonliving(skc6,skf10(skc7,skc6)),
inference(resolve,[status(thm)],[c_198,c_171]) ).
cnf(c_280,plain,
nonliving(skc6,skf10(skc7,skc6)),
inference(paramod,[status(thm)],[c_245,c_241]) ).
cnf(c_279,plain,
$false,
inference(resolve,[status(thm)],[c_248,c_280]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP147-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n014.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 26 01:04:02 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.38 % Process 1607427 was started by sandbox on n014,
% 0.11/0.38 % Sat Sep 26 01:04:02 2026
% 0.11/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/0.38
% 0.11/0.38 % From the command line: assign(max_seconds, 300).
% 0.11/0.42
% 0.11/0.42 % SZS status Unsatisfiable for theBenchmark
% 0.11/0.42
% 0.11/0.42 % Proof 1 at 0.02 (+ 0.00) seconds.
% 0.11/0.42 % Length of proof is 35.
% 0.11/0.42 % Level of proof is 7.
% 0.11/0.42 % Maximum clause weight is 23.000.
% 0.11/0.42 % Given clauses 102.
% 0.11/0.42
% 0.11/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------