%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NLP094-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n016.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:16:26 PM UTC 2026
% Result : Unsatisfiable 0.58s 1.33s
% Output : CNFRefutation 0.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 44
% Syntax : Number of formulae : 208 ( 25 unt; 6 def)
% Number of atoms : 945 ( 6 equ)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 1310 ( 627 ~; 683 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 36 ( 34 usr; 22 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 2 con; 0-1 aty)
% Number of variables : 359 ( 0 sgn 359 !; 0 ?; 261 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
actual_world(skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f2,negated_conjecture,
actual_world(skc2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
fof(f3,negated_conjecture,
! [X0] :
( customer(X0,skf39(X0))
| ssSkC0
| ~ actual_world(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
fof(f4,negated_conjecture,
! [X0] :
( restaurant(X0,skf34(X0))
| ssSkC0
| ~ actual_world(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
fof(f5,negated_conjecture,
! [X0] :
( customer(X0,skf25(X0))
| ~ ssSkC0
| ~ actual_world(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
fof(f6,negated_conjecture,
! [X0] :
( restaurant(X0,skf20(X0))
| ~ ssSkC0
| ~ actual_world(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
fof(f7,negated_conjecture,
! [X0] :
( in(X0,skf39(X0),skf34(X0))
| ssSkC0
| ~ actual_world(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
fof(f8,negated_conjecture,
! [X0] :
( in(X0,skf25(X0),skf20(X0))
| ~ ssSkC0
| ~ actual_world(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
fof(f9,negated_conjecture,
! [X2,X0,X1] :
( event(skc13,skf26(X2))
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
fof(f10,negated_conjecture,
! [X2,X0,X1] :
( past(skc13,skf26(X2))
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
fof(f11,negated_conjecture,
! [X2,X0,X1] :
( nonreflexive(skc13,skf26(X2))
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
fof(f12,negated_conjecture,
! [X2,X0,X1] :
( see(skc13,skf26(X2))
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
fof(f13,negated_conjecture,
! [X2,X0,X1] :
( human_person(skc13,skf29(X2))
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
fof(f14,negated_conjecture,
! [X2,X0,X1] :
( drink(skc13,skf27(X2))
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
fof(f15,negated_conjecture,
! [X2,X0,X1] :
( nonreflexive(skc13,skf27(X2))
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
fof(f16,negated_conjecture,
! [X2,X0,X1] :
( past(skc13,skf27(X2))
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
fof(f17,negated_conjecture,
! [X2,X0,X1] :
( event(skc13,skf27(X2))
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
fof(f18,negated_conjecture,
! [X2,X0,X1] :
( coffee(skc13,skf28(X2))
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
fof(f19,negated_conjecture,
! [X2,X0,X1] :
( event(skc2,skf12(X2))
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
fof(f20,negated_conjecture,
! [X2,X0,X1] :
( past(skc2,skf12(X2))
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
fof(f21,negated_conjecture,
! [X2,X0,X1] :
( nonreflexive(skc2,skf12(X2))
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
fof(f22,negated_conjecture,
! [X2,X0,X1] :
( see(skc2,skf12(X2))
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
fof(f23,negated_conjecture,
! [X2,X0,X1] :
( coffee(skc2,skf14(X2))
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause23) ).
fof(f24,negated_conjecture,
! [X2,X0,X1] :
( drink(skc2,skf13(X2))
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
fof(f25,negated_conjecture,
! [X2,X0,X1] :
( nonreflexive(skc2,skf13(X2))
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
fof(f26,negated_conjecture,
! [X2,X0,X1] :
( past(skc2,skf13(X2))
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
fof(f27,negated_conjecture,
! [X2,X0,X1] :
( event(skc2,skf13(X2))
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
fof(f28,negated_conjecture,
! [X2,X0,X1] :
( human_person(skc2,skf15(X2))
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
fof(f29,negated_conjecture,
! [X0,X1] :
( agent(skc13,skf26(X1),X1)
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause29) ).
fof(f30,negated_conjecture,
! [X0,X1] :
( agent(skc2,skf12(X1),X1)
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
fof(f31,negated_conjecture,
! [X2,X0,X1] :
( patient(skc13,skf26(X2),skf29(X2))
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
fof(f32,negated_conjecture,
! [X2,X0,X1] :
( agent(skc13,skf27(X2),skf29(X2))
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
fof(f33,negated_conjecture,
! [X2,X0,X1] :
( patient(skc13,skf27(X2),skf28(X2))
| ssSkC0
| ~ customer(skc13,X1)
| ~ in(skc13,X1,X0)
| ~ restaurant(skc13,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
fof(f34,negated_conjecture,
! [X2,X0,X1] :
( agent(skc2,skf13(X2),skf15(X2))
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
fof(f35,negated_conjecture,
! [X2,X0,X1] :
( patient(skc2,skf12(X2),skf15(X2))
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
fof(f36,negated_conjecture,
! [X2,X0,X1] :
( patient(skc2,skf13(X2),skf14(X2))
| ~ ssSkC0
| ~ customer(skc2,X1)
| ~ in(skc2,X1,X0)
| ~ restaurant(skc2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
fof(f37,negated_conjecture,
! [X2,X3,X0,X1,X4] :
( ssSkC0
| ~ actual_world(X0)
| ~ patient(X0,X1,X4)
| ~ agent(X0,X2,X4)
| ~ human_person(X0,X4)
| ~ event(X0,X2)
| ~ past(X0,X2)
| ~ nonreflexive(X0,X2)
| ~ drink(X0,X2)
| ~ coffee(X0,X3)
| ~ patient(X0,X2,X3)
| ~ see(X0,X1)
| ~ nonreflexive(X0,X1)
| ~ past(X0,X1)
| ~ agent(X0,X1,skf39(X0))
| ~ event(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
fof(f38,negated_conjecture,
! [X2,X3,X0,X1,X4] :
( ~ ssSkC0
| ~ actual_world(X0)
| ~ patient(X0,X3,X4)
| ~ coffee(X0,X4)
| ~ event(X0,X3)
| ~ past(X0,X3)
| ~ nonreflexive(X0,X3)
| ~ drink(X0,X3)
| ~ human_person(X0,X2)
| ~ agent(X0,X3,X2)
| ~ patient(X0,X1,X2)
| ~ see(X0,X1)
| ~ nonreflexive(X0,X1)
| ~ past(X0,X1)
| ~ agent(X0,X1,skf25(X0))
| ~ event(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
tcf(c_87,negated_conjecture,
actual_world(skc13),
inference(cnf_transformation,[],[f1]) ).
tcf(c_88,negated_conjecture,
actual_world(skc2),
inference(cnf_transformation,[],[f2]) ).
tcf(c_89,negated_conjecture,
! [X0: $i] :
( ssSkC0
| customer(X0,skf39(X0))
| ~ actual_world(X0) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_90,negated_conjecture,
! [X0: $i] :
( ssSkC0
| restaurant(X0,skf34(X0))
| ~ actual_world(X0) ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_91,negated_conjecture,
! [X0: $i] :
( customer(X0,skf25(X0))
| ~ ssSkC0
| ~ actual_world(X0) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_92,negated_conjecture,
! [X0: $i] :
( restaurant(X0,skf20(X0))
| ~ ssSkC0
| ~ actual_world(X0) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_93,negated_conjecture,
! [X0: $i] :
( ssSkC0
| in(X0,skf39(X0),skf34(X0))
| ~ actual_world(X0) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_94,negated_conjecture,
! [X0: $i] :
( in(X0,skf25(X0),skf20(X0))
| ~ ssSkC0
| ~ actual_world(X0) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_95,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC0
| event(skc13,skf26(X2))
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_96,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC0
| past(skc13,skf26(X2))
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_97,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC0
| nonreflexive(skc13,skf26(X2))
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_98,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC0
| see(skc13,skf26(X2))
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_99,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC0
| human_person(skc13,skf29(X2))
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_100,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC0
| drink(skc13,skf27(X2))
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_101,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC0
| nonreflexive(skc13,skf27(X2))
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_102,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC0
| past(skc13,skf27(X2))
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_103,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC0
| event(skc13,skf27(X2))
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_104,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC0
| coffee(skc13,skf28(X2))
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_105,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( event(skc2,skf12(X2))
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_106,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( past(skc2,skf12(X2))
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_107,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( nonreflexive(skc2,skf12(X2))
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_108,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( see(skc2,skf12(X2))
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_109,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( coffee(skc2,skf14(X2))
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_110,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( drink(skc2,skf13(X2))
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_111,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( nonreflexive(skc2,skf13(X2))
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_112,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( past(skc2,skf13(X2))
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_113,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( event(skc2,skf13(X2))
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_114,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( human_person(skc2,skf15(X2))
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_115,negated_conjecture,
! [X0: $i,X1: $i] :
( ssSkC0
| agent(skc13,skf26(X0),X0)
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_116,negated_conjecture,
! [X0: $i,X1: $i] :
( agent(skc2,skf12(X0),X0)
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_117,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC0
| patient(skc13,skf26(X2),skf29(X2))
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_118,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC0
| agent(skc13,skf27(X2),skf29(X2))
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_119,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC0
| patient(skc13,skf27(X2),skf28(X2))
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_120,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( agent(skc2,skf13(X2),skf15(X2))
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_121,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( patient(skc2,skf12(X2),skf15(X2))
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_122,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( patient(skc2,skf13(X2),skf14(X2))
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_123,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ssSkC0
| ~ actual_world(X0)
| ~ coffee(X0,X4)
| ~ drink(X0,X2)
| ~ human_person(X0,X3)
| ~ see(X0,X1)
| ~ nonreflexive(X0,X2)
| ~ nonreflexive(X0,X1)
| ~ past(X0,X2)
| ~ past(X0,X1)
| ~ event(X0,X2)
| ~ event(X0,X1)
| ~ patient(X0,X2,X4)
| ~ patient(X0,X1,X3)
| ~ agent(X0,X2,X3)
| ~ agent(X0,X1,skf39(X0)) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_124,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ ssSkC0
| ~ actual_world(X0)
| ~ coffee(X0,X4)
| ~ drink(X0,X2)
| ~ human_person(X0,X3)
| ~ see(X0,X1)
| ~ nonreflexive(X0,X2)
| ~ nonreflexive(X0,X1)
| ~ past(X0,X2)
| ~ past(X0,X1)
| ~ event(X0,X2)
| ~ event(X0,X1)
| ~ patient(X0,X2,X4)
| ~ patient(X0,X1,X3)
| ~ agent(X0,X2,X3)
| ~ agent(X0,X1,skf25(X0)) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_546,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ssSkC0
| ~ actual_world(skc13)
| ~ coffee(skc13,X5)
| ~ drink(skc13,X4)
| ~ human_person(skc13,X1)
| ~ nonreflexive(skc13,X4)
| ~ past(skc13,X4)
| ~ event(skc13,X4)
| ~ restaurant(skc13,X3)
| ~ customer(skc13,X2)
| ~ nonreflexive(skc13,skf26(X0))
| ~ past(skc13,skf26(X0))
| ~ event(skc13,skf26(X0))
| ~ patient(skc13,X4,X5)
| ~ agent(skc13,X4,X1)
| ~ in(skc13,X2,X3)
| ~ patient(skc13,skf26(X0),X1)
| ~ agent(skc13,skf26(X0),skf39(skc13)) ),
inference(resolution,[status(thm)],[c_98,c_123]) ).
tcf(c_548,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ssSkC0
| ~ agent(skc13,skf26(X0),skf39(skc13))
| ~ patient(skc13,skf26(X0),X1)
| ~ in(skc13,X2,X3)
| ~ agent(skc13,X4,X1)
| ~ patient(skc13,X4,X5)
| ~ event(skc13,skf26(X0))
| ~ past(skc13,skf26(X0))
| ~ nonreflexive(skc13,skf26(X0))
| ~ customer(skc13,X2)
| ~ restaurant(skc13,X3)
| ~ event(skc13,X4)
| ~ past(skc13,X4)
| ~ nonreflexive(skc13,X4)
| ~ human_person(skc13,X1)
| ~ drink(skc13,X4)
| ~ coffee(skc13,X5) ),
inference(global_subsumption_just,[status(thm)],[c_546,c_87,c_546]) ).
tcf(c_549,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ssSkC0
| ~ coffee(skc13,X5)
| ~ drink(skc13,X4)
| ~ human_person(skc13,X1)
| ~ nonreflexive(skc13,X4)
| ~ past(skc13,X4)
| ~ event(skc13,X4)
| ~ restaurant(skc13,X3)
| ~ customer(skc13,X2)
| ~ nonreflexive(skc13,skf26(X0))
| ~ past(skc13,skf26(X0))
| ~ event(skc13,skf26(X0))
| ~ patient(skc13,X4,X5)
| ~ agent(skc13,X4,X1)
| ~ in(skc13,X2,X3)
| ~ patient(skc13,skf26(X0),X1)
| ~ agent(skc13,skf26(X0),skf39(skc13)) ),
inference(renaming,[status(thm)],[c_548]) ).
tcf(c_585,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ssSkC0
| ~ coffee(skc13,X5)
| ~ drink(skc13,X4)
| ~ human_person(skc13,X1)
| ~ nonreflexive(skc13,X4)
| ~ past(skc13,X4)
| ~ event(skc13,X4)
| ~ restaurant(skc13,X3)
| ~ customer(skc13,X2)
| ~ patient(skc13,X4,X5)
| ~ agent(skc13,X4,X1)
| ~ in(skc13,X2,X3)
| ~ patient(skc13,skf26(X0),X1)
| ~ agent(skc13,skf26(X0),skf39(skc13)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_549,c_97,c_96,c_95]) ).
tcf(c_601,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ~ ssSkC0
| ~ actual_world(skc2)
| ~ coffee(skc2,X5)
| ~ drink(skc2,X4)
| ~ human_person(skc2,X1)
| ~ nonreflexive(skc2,X4)
| ~ past(skc2,X4)
| ~ event(skc2,X4)
| ~ restaurant(skc2,X3)
| ~ customer(skc2,X2)
| ~ nonreflexive(skc2,skf12(X0))
| ~ past(skc2,skf12(X0))
| ~ event(skc2,skf12(X0))
| ~ patient(skc2,X4,X5)
| ~ agent(skc2,X4,X1)
| ~ in(skc2,X2,X3)
| ~ patient(skc2,skf12(X0),X1)
| ~ agent(skc2,skf12(X0),skf25(skc2)) ),
inference(resolution,[status(thm)],[c_108,c_124]) ).
tcf(c_603,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ~ ssSkC0
| ~ agent(skc2,skf12(X0),skf25(skc2))
| ~ patient(skc2,skf12(X0),X1)
| ~ in(skc2,X2,X3)
| ~ agent(skc2,X4,X1)
| ~ patient(skc2,X4,X5)
| ~ event(skc2,skf12(X0))
| ~ past(skc2,skf12(X0))
| ~ nonreflexive(skc2,skf12(X0))
| ~ customer(skc2,X2)
| ~ restaurant(skc2,X3)
| ~ event(skc2,X4)
| ~ past(skc2,X4)
| ~ nonreflexive(skc2,X4)
| ~ human_person(skc2,X1)
| ~ drink(skc2,X4)
| ~ coffee(skc2,X5) ),
inference(global_subsumption_just,[status(thm)],[c_601,c_88,c_601]) ).
tcf(c_604,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ~ ssSkC0
| ~ coffee(skc2,X5)
| ~ drink(skc2,X4)
| ~ human_person(skc2,X1)
| ~ nonreflexive(skc2,X4)
| ~ past(skc2,X4)
| ~ event(skc2,X4)
| ~ restaurant(skc2,X3)
| ~ customer(skc2,X2)
| ~ nonreflexive(skc2,skf12(X0))
| ~ past(skc2,skf12(X0))
| ~ event(skc2,skf12(X0))
| ~ patient(skc2,X4,X5)
| ~ agent(skc2,X4,X1)
| ~ in(skc2,X2,X3)
| ~ patient(skc2,skf12(X0),X1)
| ~ agent(skc2,skf12(X0),skf25(skc2)) ),
inference(renaming,[status(thm)],[c_603]) ).
tcf(c_640,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ~ ssSkC0
| ~ coffee(skc2,X5)
| ~ drink(skc2,X4)
| ~ human_person(skc2,X1)
| ~ nonreflexive(skc2,X4)
| ~ past(skc2,X4)
| ~ event(skc2,X4)
| ~ restaurant(skc2,X3)
| ~ customer(skc2,X2)
| ~ patient(skc2,X4,X5)
| ~ agent(skc2,X4,X1)
| ~ in(skc2,X2,X3)
| ~ patient(skc2,skf12(X0),X1)
| ~ agent(skc2,skf12(X0),skf25(skc2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_604,c_107,c_106,c_105]) ).
tcf(c_664,plain,
( ssSkC0
| in(skc13,skf39(skc13),skf34(skc13)) ),
inference(resolution,[status(thm)],[c_87,c_93]) ).
tcf(c_685,plain,
( ssSkC0
| restaurant(skc13,skf34(skc13)) ),
inference(resolution,[status(thm)],[c_87,c_90]) ).
tcf(c_692,plain,
( ssSkC0
| customer(skc13,skf39(skc13)) ),
inference(resolution,[status(thm)],[c_87,c_89]) ).
tcf(c_699,plain,
( in(skc2,skf25(skc2),skf20(skc2))
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c_88,c_94]) ).
tcf(c_706,plain,
( ssSkC0
| in(skc2,skf39(skc2),skf34(skc2)) ),
inference(resolution,[status(thm)],[c_88,c_93]) ).
tcf(c_713,plain,
( restaurant(skc2,skf20(skc2))
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c_88,c_92]) ).
tcf(c_720,plain,
( customer(skc2,skf25(skc2))
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c_88,c_91]) ).
tcf(c_727,plain,
( ssSkC0
| restaurant(skc2,skf34(skc2)) ),
inference(resolution,[status(thm)],[c_88,c_90]) ).
tcf(c_734,plain,
( ssSkC0
| customer(skc2,skf39(skc2)) ),
inference(resolution,[status(thm)],[c_88,c_89]) ).
tcf(c_865,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( ssSkC0
| ~ coffee(skc13,X3)
| ~ human_person(skc13,X2)
| ~ restaurant(skc13,X7)
| ~ restaurant(skc13,X5)
| ~ customer(skc13,X6)
| ~ customer(skc13,X4)
| ~ nonreflexive(skc13,skf27(X1))
| ~ past(skc13,skf27(X1))
| ~ event(skc13,skf27(X1))
| ~ in(skc13,X6,X7)
| ~ in(skc13,X4,X5)
| ~ patient(skc13,skf27(X1),X3)
| ~ patient(skc13,skf26(X0),X2)
| ~ agent(skc13,skf27(X1),X2)
| ~ agent(skc13,skf26(X0),skf39(skc13)) ),
inference(resolution,[status(thm)],[c_100,c_585]) ).
tcf(c_899,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( ssSkC0
| ~ coffee(skc13,X3)
| ~ human_person(skc13,X2)
| ~ restaurant(skc13,X7)
| ~ restaurant(skc13,X5)
| ~ customer(skc13,X6)
| ~ customer(skc13,X4)
| ~ in(skc13,X6,X7)
| ~ in(skc13,X4,X5)
| ~ patient(skc13,skf27(X1),X3)
| ~ patient(skc13,skf26(X0),X2)
| ~ agent(skc13,skf27(X1),X2)
| ~ agent(skc13,skf26(X0),skf39(skc13)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_865,c_101,c_102,c_103]) ).
tcf(c_914,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( ~ ssSkC0
| ~ coffee(skc2,X3)
| ~ human_person(skc2,X2)
| ~ restaurant(skc2,X7)
| ~ restaurant(skc2,X5)
| ~ customer(skc2,X6)
| ~ customer(skc2,X4)
| ~ nonreflexive(skc2,skf13(X1))
| ~ past(skc2,skf13(X1))
| ~ event(skc2,skf13(X1))
| ~ in(skc2,X6,X7)
| ~ in(skc2,X4,X5)
| ~ patient(skc2,skf13(X1),X3)
| ~ patient(skc2,skf12(X0),X2)
| ~ agent(skc2,skf13(X1),X2)
| ~ agent(skc2,skf12(X0),skf25(skc2)) ),
inference(resolution,[status(thm)],[c_110,c_640]) ).
tcf(c_948,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( ~ ssSkC0
| ~ coffee(skc2,X3)
| ~ human_person(skc2,X2)
| ~ restaurant(skc2,X7)
| ~ restaurant(skc2,X5)
| ~ customer(skc2,X6)
| ~ customer(skc2,X4)
| ~ in(skc2,X6,X7)
| ~ in(skc2,X4,X5)
| ~ patient(skc2,skf13(X1),X3)
| ~ patient(skc2,skf12(X0),X2)
| ~ agent(skc2,skf13(X1),X2)
| ~ agent(skc2,skf12(X0),skf25(skc2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_914,c_111,c_112,c_113]) ).
tcf(c_1555,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_10
| ~ customer(skc2,X0)
| ~ restaurant(skc2,X1)
| ~ in(skc2,X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_948]) ).
tcf(c_1556,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ iPr_def_11
| ~ human_person(skc2,X3)
| ~ coffee(skc2,X1)
| ~ agent(skc2,skf12(X2),skf25(skc2))
| ~ agent(skc2,skf13(X0),X3)
| ~ patient(skc2,skf12(X2),X3)
| ~ patient(skc2,skf13(X0),X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_948]) ).
tcf(c_1557,plain,
( iPr_def_11
| iPr_def_10
| ~ ssSkC0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_948]) ).
tcf(c_1558,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ~ customer(skc13,X0)
| ~ restaurant(skc13,X1)
| ~ in(skc13,X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_899]) ).
tcf(c_1559,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ iPr_def_13
| ~ human_person(skc13,X3)
| ~ coffee(skc13,X1)
| ~ agent(skc13,skf26(X2),skf39(skc13))
| ~ agent(skc13,skf27(X0),X3)
| ~ patient(skc13,skf26(X2),X3)
| ~ patient(skc13,skf27(X0),X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_899]) ).
tcf(c_1560,plain,
( iPr_def_13
| iPr_def_12
| ssSkC0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_899]) ).
tcf(c_1561,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| patient(skc2,skf13(X0),skf14(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_122]) ).
tcf(c_1562,negated_conjecture,
( iPr_def_14
| iPr_def_10
| ~ ssSkC0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_122]) ).
tcf(c_1563,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| patient(skc2,skf12(X0),skf15(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_121]) ).
tcf(c_1564,negated_conjecture,
( iPr_def_15
| iPr_def_10
| ~ ssSkC0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_121]) ).
tcf(c_1565,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_16
| agent(skc2,skf13(X0),skf15(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_120]) ).
tcf(c_1566,negated_conjecture,
( iPr_def_16
| iPr_def_10
| ~ ssSkC0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_120]) ).
tcf(c_1567,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_17
| patient(skc13,skf27(X0),skf28(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_17])],[c_119]) ).
tcf(c_1568,negated_conjecture,
( iPr_def_17
| iPr_def_12
| ssSkC0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_119]) ).
tcf(c_1569,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_18
| agent(skc13,skf27(X0),skf29(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_118]) ).
tcf(c_1570,negated_conjecture,
( iPr_def_18
| iPr_def_12
| ssSkC0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_118]) ).
tcf(c_1571,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_19
| patient(skc13,skf26(X0),skf29(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_19])],[c_117]) ).
tcf(c_1572,negated_conjecture,
( iPr_def_19
| iPr_def_12
| ssSkC0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_117]) ).
tcf(c_1573,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_20
| human_person(skc2,skf15(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_20])],[c_114]) ).
tcf(c_1574,negated_conjecture,
( iPr_def_20
| iPr_def_10
| ~ ssSkC0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_114]) ).
tcf(c_1575,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_21
| coffee(skc2,skf14(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_21])],[c_109]) ).
tcf(c_1576,negated_conjecture,
( iPr_def_21
| iPr_def_10
| ~ ssSkC0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_109]) ).
tcf(c_1577,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_22
| coffee(skc13,skf28(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_22])],[c_104]) ).
tcf(c_1578,negated_conjecture,
( iPr_def_22
| iPr_def_12
| ssSkC0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_104]) ).
tcf(c_1579,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_23
| human_person(skc13,skf29(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_23])],[c_99]) ).
tcf(c_1580,negated_conjecture,
( iPr_def_23
| iPr_def_12
| ssSkC0 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_99]) ).
tcf(c_1581,definition,
iPr_def_24 = skf25(skc2),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_1582,definition,
iPr_def_25 = skf39(skc13),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_1583,definition,
iPr_def_26 = skf39(skc2),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_1584,definition,
iPr_def_27 = skf34(skc2),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_1585,definition,
iPr_def_28 = skf20(skc2),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_1586,definition,
iPr_def_29 = skf34(skc13),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_1589,plain,
( iPr_def_11
| iPr_def_10
| ~ ssSkC0 ),
inference(demodulation,[status(thm)],[c_1557]) ).
tcf(c_1590,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ iPr_def_11
| ~ coffee(skc2,X3)
| ~ human_person(skc2,X1)
| ~ agent(skc2,skf12(X2),iPr_def_24)
| ~ patient(skc2,skf13(X0),X3)
| ~ patient(skc2,skf12(X2),X1)
| ~ agent(skc2,skf13(X0),X1) ),
inference(demodulation,[status(thm)],[c_1556,c_1581]) ).
tcf(c_1593,plain,
( iPr_def_13
| iPr_def_12
| ssSkC0 ),
inference(demodulation,[status(thm)],[c_1560]) ).
tcf(c_1594,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ iPr_def_13
| ~ coffee(skc13,X3)
| ~ human_person(skc13,X1)
| ~ agent(skc13,skf26(X2),iPr_def_25)
| ~ patient(skc13,skf27(X0),X3)
| ~ patient(skc13,skf26(X2),X1)
| ~ agent(skc13,skf27(X0),X1) ),
inference(demodulation,[status(thm)],[c_1559,c_1582]) ).
tcf(c_1597,plain,
( ssSkC0
| customer(skc2,iPr_def_26) ),
inference(demodulation,[status(thm)],[c_734,c_1583]) ).
tcf(c_1598,plain,
( ssSkC0
| restaurant(skc2,iPr_def_27) ),
inference(demodulation,[status(thm)],[c_727,c_1584]) ).
tcf(c_1599,plain,
( customer(skc2,iPr_def_24)
| ~ ssSkC0 ),
inference(demodulation,[status(thm)],[c_720]) ).
tcf(c_1600,plain,
( restaurant(skc2,iPr_def_28)
| ~ ssSkC0 ),
inference(demodulation,[status(thm)],[c_713,c_1585]) ).
tcf(c_1601,plain,
( ssSkC0
| in(skc2,iPr_def_26,iPr_def_27) ),
inference(demodulation,[status(thm)],[c_706]) ).
tcf(c_1602,plain,
( in(skc2,iPr_def_24,iPr_def_28)
| ~ ssSkC0 ),
inference(demodulation,[status(thm)],[c_699]) ).
tcf(c_1603,plain,
( ssSkC0
| customer(skc13,iPr_def_25) ),
inference(demodulation,[status(thm)],[c_692]) ).
tcf(c_1604,plain,
( ssSkC0
| restaurant(skc13,iPr_def_29) ),
inference(demodulation,[status(thm)],[c_685,c_1586]) ).
tcf(c_1607,plain,
( ssSkC0
| in(skc13,iPr_def_25,iPr_def_29) ),
inference(demodulation,[status(thm)],[c_664]) ).
tcf(c_1609,negated_conjecture,
( iPr_def_14
| iPr_def_10
| ~ ssSkC0 ),
inference(demodulation,[status(thm)],[c_1562]) ).
tcf(c_1611,negated_conjecture,
! [X0: $i] :
( patient(skc2,skf13(X0),skf14(X0))
| ~ iPr_def_14 ),
inference(demodulation,[status(thm)],[c_1561]) ).
tcf(c_1612,negated_conjecture,
( iPr_def_15
| iPr_def_10
| ~ ssSkC0 ),
inference(demodulation,[status(thm)],[c_1564]) ).
tcf(c_1614,negated_conjecture,
! [X0: $i] :
( patient(skc2,skf12(X0),skf15(X0))
| ~ iPr_def_15 ),
inference(demodulation,[status(thm)],[c_1563]) ).
tcf(c_1615,negated_conjecture,
( iPr_def_16
| iPr_def_10
| ~ ssSkC0 ),
inference(demodulation,[status(thm)],[c_1566]) ).
tcf(c_1617,negated_conjecture,
! [X0: $i] :
( agent(skc2,skf13(X0),skf15(X0))
| ~ iPr_def_16 ),
inference(demodulation,[status(thm)],[c_1565]) ).
tcf(c_1618,negated_conjecture,
( iPr_def_17
| iPr_def_12
| ssSkC0 ),
inference(demodulation,[status(thm)],[c_1568]) ).
tcf(c_1620,negated_conjecture,
! [X0: $i] :
( patient(skc13,skf27(X0),skf28(X0))
| ~ iPr_def_17 ),
inference(demodulation,[status(thm)],[c_1567]) ).
tcf(c_1621,negated_conjecture,
( iPr_def_18
| iPr_def_12
| ssSkC0 ),
inference(demodulation,[status(thm)],[c_1570]) ).
tcf(c_1623,negated_conjecture,
! [X0: $i] :
( agent(skc13,skf27(X0),skf29(X0))
| ~ iPr_def_18 ),
inference(demodulation,[status(thm)],[c_1569]) ).
tcf(c_1624,negated_conjecture,
( iPr_def_19
| iPr_def_12
| ssSkC0 ),
inference(demodulation,[status(thm)],[c_1572]) ).
tcf(c_1626,negated_conjecture,
! [X0: $i] :
( patient(skc13,skf26(X0),skf29(X0))
| ~ iPr_def_19 ),
inference(demodulation,[status(thm)],[c_1571]) ).
tcf(c_1627,negated_conjecture,
! [X0: $i,X1: $i] :
( agent(skc2,skf12(X0),X0)
| ~ ssSkC0
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_1628,negated_conjecture,
! [X0: $i,X1: $i] :
( ssSkC0
| agent(skc13,skf26(X0),X0)
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(demodulation,[status(thm)],[c_115]) ).
tcf(c_1629,negated_conjecture,
( iPr_def_20
| iPr_def_10
| ~ ssSkC0 ),
inference(demodulation,[status(thm)],[c_1574]) ).
tcf(c_1631,negated_conjecture,
! [X0: $i] :
( human_person(skc2,skf15(X0))
| ~ iPr_def_20 ),
inference(demodulation,[status(thm)],[c_1573]) ).
tcf(c_1632,negated_conjecture,
( iPr_def_21
| iPr_def_10
| ~ ssSkC0 ),
inference(demodulation,[status(thm)],[c_1576]) ).
tcf(c_1633,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_10
| ~ restaurant(skc2,X1)
| ~ customer(skc2,X0)
| ~ in(skc2,X0,X1) ),
inference(demodulation,[status(thm)],[c_1555]) ).
tcf(c_1634,negated_conjecture,
! [X0: $i] :
( coffee(skc2,skf14(X0))
| ~ iPr_def_21 ),
inference(demodulation,[status(thm)],[c_1575]) ).
tcf(c_1635,negated_conjecture,
( iPr_def_22
| iPr_def_12
| ssSkC0 ),
inference(demodulation,[status(thm)],[c_1578]) ).
tcf(c_1637,negated_conjecture,
! [X0: $i] :
( coffee(skc13,skf28(X0))
| ~ iPr_def_22 ),
inference(demodulation,[status(thm)],[c_1577]) ).
tcf(c_1638,negated_conjecture,
( iPr_def_23
| iPr_def_12
| ssSkC0 ),
inference(demodulation,[status(thm)],[c_1580]) ).
tcf(c_1639,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ~ restaurant(skc13,X1)
| ~ customer(skc13,X0)
| ~ in(skc13,X0,X1) ),
inference(demodulation,[status(thm)],[c_1558]) ).
tcf(c_1640,negated_conjecture,
! [X0: $i] :
( human_person(skc13,skf29(X0))
| ~ iPr_def_23 ),
inference(demodulation,[status(thm)],[c_1579]) ).
tcf(c_2719,plain,
( ssSkC0
| agent(skc13,skf26(iPr_def_25),iPr_def_25)
| ~ restaurant(skc13,iPr_def_29)
| ~ customer(skc13,iPr_def_25) ),
inference(superposition,[status(thm)],[c_1607,c_1628]) ).
tcf(c_2824,plain,
( agent(skc2,skf12(iPr_def_24),iPr_def_24)
| ~ ssSkC0
| ~ restaurant(skc2,iPr_def_28)
| ~ customer(skc2,iPr_def_24) ),
inference(superposition,[status(thm)],[c_1602,c_1627]) ).
tcf(c_2834,plain,
( ssSkC0
| agent(skc13,skf26(iPr_def_25),iPr_def_25) ),
inference(global_subsumption_just,[status(thm)],[c_2719,c_1603,c_1604,c_2719]) ).
tcf(c_2840,plain,
( agent(skc2,skf12(iPr_def_24),iPr_def_24)
| ~ ssSkC0 ),
inference(global_subsumption_just,[status(thm)],[c_2824,c_1599,c_1600,c_2824]) ).
tcf(c_2958,plain,
( ssSkC0
| ~ iPr_def_10
| ~ restaurant(skc2,iPr_def_27)
| ~ customer(skc2,iPr_def_26) ),
inference(superposition,[status(thm)],[c_1601,c_1633]) ).
tcf(c_2959,plain,
( ~ iPr_def_10
| ~ ssSkC0
| ~ restaurant(skc2,iPr_def_28)
| ~ customer(skc2,iPr_def_24) ),
inference(superposition,[status(thm)],[c_1602,c_1633]) ).
tcf(c_3016,plain,
( ssSkC0
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_2958,c_1597,c_1598,c_1599,c_1600,c_2958,c_2959]) ).
tcf(c_3018,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_3016,c_1599,c_1600,c_2959,c_3016]) ).
tcf(c_3408,plain,
( ssSkC0
| ~ iPr_def_12
| ~ restaurant(skc13,iPr_def_29)
| ~ customer(skc13,iPr_def_25) ),
inference(superposition,[status(thm)],[c_1607,c_1639]) ).
tcf(c_3432,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iPr_def_14
| ~ iPr_def_11
| ~ human_person(skc2,X1)
| ~ coffee(skc2,skf14(X0))
| ~ agent(skc2,skf12(X2),iPr_def_24)
| ~ patient(skc2,skf12(X2),X1)
| ~ agent(skc2,skf13(X0),X1) ),
inference(superposition,[status(thm)],[c_1611,c_1590]) ).
tcf(c_3455,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_14
| ~ iPr_def_11
| ~ ssSkC0
| ~ human_person(skc2,X1)
| ~ coffee(skc2,skf14(X0))
| ~ patient(skc2,skf12(iPr_def_24),X1)
| ~ agent(skc2,skf13(X0),X1) ),
inference(superposition,[status(thm)],[c_2840,c_3432]) ).
tcf(c_3464,plain,
! [X0: $i,X1: $i] :
( ~ ssSkC0
| ~ human_person(skc2,X1)
| ~ agent(skc2,skf13(X0),X1)
| ~ patient(skc2,skf12(iPr_def_24),X1) ),
inference(global_subsumption_just,[status(thm)],[c_3455,c_1589,c_1609,c_1632,c_1634,c_3018,c_3455]) ).
tcf(c_3465,plain,
! [X0: $i,X1: $i] :
( ~ ssSkC0
| ~ human_person(skc2,X1)
| ~ patient(skc2,skf12(iPr_def_24),X1)
| ~ agent(skc2,skf13(X0),X1) ),
inference(renaming,[status(thm)],[c_3464]) ).
tcf(c_3475,plain,
! [X0: $i] :
( ~ iPr_def_16
| ~ ssSkC0
| ~ human_person(skc2,skf15(X0))
| ~ patient(skc2,skf12(iPr_def_24),skf15(X0)) ),
inference(superposition,[status(thm)],[c_1617,c_3465]) ).
tcf(c_3481,plain,
! [X0: $i] :
( ~ patient(skc2,skf12(iPr_def_24),skf15(X0))
| ~ ssSkC0 ),
inference(global_subsumption_just,[status(thm)],[c_3475,c_1615,c_1629,c_1631,c_3018,c_3475]) ).
tcf(c_3482,plain,
! [X0: $i] :
( ~ ssSkC0
| ~ patient(skc2,skf12(iPr_def_24),skf15(X0)) ),
inference(renaming,[status(thm)],[c_3481]) ).
tcf(c_3488,plain,
( ~ iPr_def_15
| ~ ssSkC0 ),
inference(superposition,[status(thm)],[c_1614,c_3482]) ).
tcf(c_3493,plain,
~ ssSkC0,
inference(global_subsumption_just,[status(thm)],[c_3488,c_1612,c_3018,c_3488]) ).
tcf(c_3495,plain,
agent(skc13,skf26(iPr_def_25),iPr_def_25),
inference(backward_subsumption_resolution,[status(thm)],[c_2834,c_3493]) ).
tcf(c_3502,plain,
( iPr_def_23
| iPr_def_12 ),
inference(backward_subsumption_resolution,[status(thm)],[c_1638,c_3493]) ).
tcf(c_3503,plain,
( iPr_def_22
| iPr_def_12 ),
inference(backward_subsumption_resolution,[status(thm)],[c_1635,c_3493]) ).
tcf(c_3504,plain,
( iPr_def_19
| iPr_def_12 ),
inference(backward_subsumption_resolution,[status(thm)],[c_1624,c_3493]) ).
tcf(c_3505,plain,
( iPr_def_18
| iPr_def_12 ),
inference(backward_subsumption_resolution,[status(thm)],[c_1621,c_3493]) ).
tcf(c_3506,plain,
( iPr_def_17
| iPr_def_12 ),
inference(backward_subsumption_resolution,[status(thm)],[c_1618,c_3493]) ).
tcf(c_3526,plain,
iPr_def_23,
inference(global_subsumption_just,[status(thm)],[c_3502,c_1612,c_1638,c_1597,c_1598,c_1599,c_1600,c_1603,c_1604,c_2958,c_2959,c_3408,c_3488]) ).
tcf(c_3528,plain,
! [X0: $i] : human_person(skc13,skf29(X0)),
inference(backward_subsumption_resolution,[status(thm)],[c_1640,c_3526]) ).
tcf(c_3530,plain,
iPr_def_22,
inference(global_subsumption_just,[status(thm)],[c_3503,c_1612,c_1635,c_1597,c_1598,c_1599,c_1600,c_1603,c_1604,c_2958,c_2959,c_3408,c_3488]) ).
tcf(c_3532,plain,
! [X0: $i] : coffee(skc13,skf28(X0)),
inference(backward_subsumption_resolution,[status(thm)],[c_1637,c_3530]) ).
tcf(c_3534,plain,
iPr_def_19,
inference(global_subsumption_just,[status(thm)],[c_3504,c_1624,c_1603,c_1604,c_3408,c_3493]) ).
tcf(c_3536,plain,
! [X0: $i] : patient(skc13,skf26(X0),skf29(X0)),
inference(backward_subsumption_resolution,[status(thm)],[c_1626,c_3534]) ).
tcf(c_3538,plain,
iPr_def_18,
inference(global_subsumption_just,[status(thm)],[c_3505,c_1612,c_1621,c_1597,c_1598,c_1599,c_1600,c_1603,c_1604,c_2958,c_2959,c_3408,c_3488]) ).
tcf(c_3540,plain,
! [X0: $i] : agent(skc13,skf27(X0),skf29(X0)),
inference(backward_subsumption_resolution,[status(thm)],[c_1623,c_3538]) ).
tcf(c_3542,plain,
iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_3506,c_1612,c_1618,c_1597,c_1598,c_1599,c_1600,c_1603,c_1604,c_2958,c_2959,c_3408,c_3488]) ).
tcf(c_3544,plain,
! [X0: $i] : patient(skc13,skf27(X0),skf28(X0)),
inference(backward_subsumption_resolution,[status(thm)],[c_1620,c_3542]) ).
tcf(c_3563,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ agent(skc13,skf27(X0),X1)
| ~ patient(skc13,skf26(X2),X1)
| ~ patient(skc13,skf27(X0),X3)
| ~ agent(skc13,skf26(X2),iPr_def_25)
| ~ human_person(skc13,X1)
| ~ coffee(skc13,X3) ),
inference(global_subsumption_just,[status(thm)],[c_1594,c_1593,c_1612,c_1594,c_1597,c_1598,c_1599,c_1600,c_1603,c_1604,c_2958,c_2959,c_3408,c_3488]) ).
tcf(c_3564,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ coffee(skc13,X3)
| ~ human_person(skc13,X1)
| ~ agent(skc13,skf26(X2),iPr_def_25)
| ~ patient(skc13,skf27(X0),X3)
| ~ patient(skc13,skf26(X2),X1)
| ~ agent(skc13,skf27(X0),X1) ),
inference(renaming,[status(thm)],[c_3563]) ).
tcf(c_3578,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ human_person(skc13,X1)
| ~ coffee(skc13,skf28(X0))
| ~ agent(skc13,skf26(X2),iPr_def_25)
| ~ patient(skc13,skf26(X2),X1)
| ~ agent(skc13,skf27(X0),X1) ),
inference(superposition,[status(thm)],[c_3544,c_3564]) ).
tcf(c_3579,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ human_person(skc13,X1)
| ~ agent(skc13,skf26(X2),iPr_def_25)
| ~ patient(skc13,skf26(X2),X1)
| ~ agent(skc13,skf27(X0),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3578,c_3532]) ).
tcf(c_3597,plain,
! [X0: $i,X1: $i] :
( ~ human_person(skc13,X1)
| ~ patient(skc13,skf26(iPr_def_25),X1)
| ~ agent(skc13,skf27(X0),X1) ),
inference(superposition,[status(thm)],[c_3495,c_3579]) ).
tcf(c_3608,plain,
! [X0: $i] :
( ~ human_person(skc13,skf29(X0))
| ~ patient(skc13,skf26(iPr_def_25),skf29(X0)) ),
inference(superposition,[status(thm)],[c_3540,c_3597]) ).
tcf(c_3609,plain,
! [X0: $i] : ~ patient(skc13,skf26(iPr_def_25),skf29(X0)),
inference(forward_subsumption_resolution,[status(thm)],[c_3608,c_3528]) ).
tcf(c_3611,plain,
$false,
inference(superposition,[status(thm)],[c_3536,c_3609]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP094-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.35 % Computer : n016.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 : Thu Sep 24 02:04:28 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.41 Running first-order theorem proving
% 0.14/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.43
% 0.14/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.43
% 0.14/0.43 % Detected problem language: tptp
% 0.14/0.44 % Proving...
% 0.58/1.33 % SZS status Started for theBenchmark.p
% 0.58/1.33 % SZS status Unsatisfiable for theBenchmark.p
% 0.58/1.33
% 0.58/1.33 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 0.58/1.33
% 0.58/1.33 % ------ iProver source info
% 0.58/1.33
% 0.58/1.33 % git: date: 2026-07-19 20:42:38 +0200
% 0.58/1.33 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 0.58/1.33 % git: non_committed_changes: false
% 0.58/1.33
% 0.58/1.33 % ------ Parsing...% successful
% 0.58/1.33
% 0.58/1.33
% 0.58/1.33 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 0.58/1.33
% 0.58/1.33 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 0.58/1.33
% 0.58/1.33 % ------ Preprocessing... gs_s sp: 26 0s gs_e snvd_s sp: 0 0s snvd_e %
% 0.58/1.33
% 0.58/1.33 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 0.58/1.33 % ------ Proving...
% 0.58/1.33 % ------ Problem Properties
% 0.58/1.33
% 0.58/1.33 %
% 0.58/1.33 % clauses 48
% 0.58/1.33 % conjectures 22
% 0.58/1.33 % EPR 26
% 0.58/1.33 % Horn 29
% 0.58/1.33 % unary 8
% 0.58/1.33 % binary 22
% 0.58/1.33 % lits 120
% 0.58/1.33 % lits eq 8
% 0.58/1.33 % fd_pure 0
% 0.58/1.33 % fd_pseudo 0
% 0.58/1.33 % fd_cond 0
% 0.58/1.33 % fd_pseudo_cond 0
% 0.58/1.33 % AC symbols 0
% 0.58/1.33
% 0.58/1.33 % ------ Schedule dynamic 5 is on
% 0.58/1.33
% 0.58/1.33 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 0.58/1.33
% 0.58/1.33
% 0.58/1.33 % ------
% 0.58/1.33 % Current options:
% 0.58/1.33 % ------
% 0.58/1.33
% 0.58/1.33
% 0.58/1.33 %
% 0.58/1.33
% 0.58/1.33 % ------ Proving...
% 0.58/1.33 %
% 0.58/1.33
% 0.58/1.33 % SZS status Unsatisfiable for theBenchmark.p
% 0.58/1.33
% 0.58/1.33 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 0.58/1.34
% 0.58/1.34
%------------------------------------------------------------------------------