%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NLP094-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:51:13 AM UTC 2026
% Result : Unsatisfiable 3.66s 4.01s
% Output : Proof 3.66s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
actual_world(skc13),
file('theBenchmark.p',clause1) ).
cnf(clause2,negated_conjecture,
actual_world(skc2),
file('theBenchmark.p',clause2) ).
cnf(clause3,negated_conjecture,
( customer(U,skf39(U))
| ssSkC0
| ~ actual_world(U) ),
file('theBenchmark.p',clause3) ).
cnf(clause4,negated_conjecture,
( restaurant(U,skf34(U))
| ssSkC0
| ~ actual_world(U) ),
file('theBenchmark.p',clause4) ).
cnf(clause5,negated_conjecture,
( customer(U,skf25(U))
| ~ ssSkC0
| ~ actual_world(U) ),
file('theBenchmark.p',clause5) ).
cnf(clause6,negated_conjecture,
( restaurant(U,skf20(U))
| ~ ssSkC0
| ~ actual_world(U) ),
file('theBenchmark.p',clause6) ).
cnf(clause7,negated_conjecture,
( in(U,skf39(U),skf34(U))
| ssSkC0
| ~ actual_world(U) ),
file('theBenchmark.p',clause7) ).
cnf(clause8,negated_conjecture,
( in(U,skf25(U),skf20(U))
| ~ ssSkC0
| ~ actual_world(U) ),
file('theBenchmark.p',clause8) ).
cnf(clause9,negated_conjecture,
( event(skc13,skf26(W))
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause9) ).
cnf(clause10,negated_conjecture,
( past(skc13,skf26(W))
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause10) ).
cnf(clause11,negated_conjecture,
( nonreflexive(skc13,skf26(W))
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause11) ).
cnf(clause12,negated_conjecture,
( see(skc13,skf26(W))
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause12) ).
cnf(clause13,negated_conjecture,
( human_person(skc13,skf29(W))
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause13) ).
cnf(clause14,negated_conjecture,
( drink(skc13,skf27(W))
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause14) ).
cnf(clause15,negated_conjecture,
( nonreflexive(skc13,skf27(W))
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause15) ).
cnf(clause16,negated_conjecture,
( past(skc13,skf27(W))
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause16) ).
cnf(clause17,negated_conjecture,
( event(skc13,skf27(W))
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause17) ).
cnf(clause18,negated_conjecture,
( coffee(skc13,skf28(W))
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause18) ).
cnf(clause19,negated_conjecture,
( event(skc2,skf12(W))
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause19) ).
cnf(clause20,negated_conjecture,
( past(skc2,skf12(W))
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause20) ).
cnf(clause21,negated_conjecture,
( nonreflexive(skc2,skf12(W))
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause21) ).
cnf(clause22,negated_conjecture,
( see(skc2,skf12(W))
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause22) ).
cnf(clause23,negated_conjecture,
( coffee(skc2,skf14(W))
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause23) ).
cnf(clause24,negated_conjecture,
( drink(skc2,skf13(W))
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause24) ).
cnf(clause25,negated_conjecture,
( nonreflexive(skc2,skf13(W))
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause25) ).
cnf(clause26,negated_conjecture,
( past(skc2,skf13(W))
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause26) ).
cnf(clause27,negated_conjecture,
( event(skc2,skf13(W))
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause27) ).
cnf(clause28,negated_conjecture,
( human_person(skc2,skf15(W))
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause28) ).
cnf(clause29,negated_conjecture,
( agent(skc13,skf26(V),V)
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause29) ).
cnf(clause30,negated_conjecture,
( agent(skc2,skf12(V),V)
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause30) ).
cnf(clause31,negated_conjecture,
( patient(skc13,skf26(W),skf29(W))
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause31) ).
cnf(clause32,negated_conjecture,
( agent(skc13,skf27(W),skf29(W))
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause32) ).
cnf(clause33,negated_conjecture,
( patient(skc13,skf27(W),skf28(W))
| ssSkC0
| ~ customer(skc13,V)
| ~ in(skc13,V,U)
| ~ restaurant(skc13,U) ),
file('theBenchmark.p',clause33) ).
cnf(clause34,negated_conjecture,
( agent(skc2,skf13(W),skf15(W))
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause34) ).
cnf(clause35,negated_conjecture,
( patient(skc2,skf12(W),skf15(W))
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause35) ).
cnf(clause36,negated_conjecture,
( patient(skc2,skf13(W),skf14(W))
| ~ ssSkC0
| ~ customer(skc2,V)
| ~ in(skc2,V,U)
| ~ restaurant(skc2,U) ),
file('theBenchmark.p',clause36) ).
cnf(clause37,negated_conjecture,
( ssSkC0
| ~ actual_world(U)
| ~ patient(U,V,Y)
| ~ agent(U,W,Y)
| ~ human_person(U,Y)
| ~ event(U,W)
| ~ past(U,W)
| ~ nonreflexive(U,W)
| ~ drink(U,W)
| ~ coffee(U,X)
| ~ patient(U,W,X)
| ~ see(U,V)
| ~ nonreflexive(U,V)
| ~ past(U,V)
| ~ agent(U,V,skf39(U))
| ~ event(U,V) ),
file('theBenchmark.p',clause37) ).
cnf(clause38,negated_conjecture,
( ~ ssSkC0
| ~ actual_world(U)
| ~ patient(U,X,Y)
| ~ coffee(U,Y)
| ~ event(U,X)
| ~ past(U,X)
| ~ nonreflexive(U,X)
| ~ drink(U,X)
| ~ human_person(U,W)
| ~ agent(U,X,W)
| ~ patient(U,V,W)
| ~ see(U,V)
| ~ nonreflexive(U,V)
| ~ past(U,V)
| ~ agent(U,V,skf25(U))
| ~ event(U,V) ),
file('theBenchmark.p',clause38) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP094-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 This is a CNF_UNS_RFO_NEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n006.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 19 16:49:43 UTC 2026
% 0.08/0.35 % CPUTime :
% 3.66/4.01 % SZS status Unsatisfiable for theBenchmark
% 3.66/4.01 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------