%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP094-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 01:32:29 PM UTC 2026
% Result : Unsatisfiable 0.17s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NLP094-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.45 % Computer : n013.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 01:38:21 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 0.17/0.49 % Refutation found
% 0.17/0.49 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.17/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.49 fof(f1,negated_conjecture,(
% 0.17/0.49 actual_world(skc13) ),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f2,negated_conjecture,(
% 0.17/0.49 actual_world(skc2) ),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f3,negated_conjecture,(
% 0.17/0.49 (![U]: (( ~ actual_world(U)| ssSkC0| customer(U,skf39(U)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f4,negated_conjecture,(
% 0.17/0.49 (![U]: (( ~ actual_world(U)| ssSkC0| restaurant(U,skf34(U)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f5,negated_conjecture,(
% 0.17/0.49 (![U]: (( ~ actual_world(U)| ~ ssSkC0| customer(U,skf25(U)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f6,negated_conjecture,(
% 0.17/0.49 (![U]: (( ~ actual_world(U)| ~ ssSkC0| restaurant(U,skf20(U)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f7,negated_conjecture,(
% 0.17/0.49 (![U]: (( ~ actual_world(U)| ssSkC0| in(U,skf39(U),skf34(U)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f8,negated_conjecture,(
% 0.17/0.49 (![U]: (( ~ actual_world(U)| ~ ssSkC0| in(U,skf25(U),skf20(U)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f9,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| event(skc13,skf26(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f10,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| past(skc13,skf26(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f11,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| nonreflexive(skc13,skf26(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f12,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| see(skc13,skf26(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f13,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| human_person(skc13,skf29(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f14,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| drink(skc13,skf27(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f15,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| nonreflexive(skc13,skf27(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f16,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| past(skc13,skf27(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f17,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| event(skc13,skf27(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f18,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| coffee(skc13,skf28(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f19,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| event(skc2,skf12(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f20,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| past(skc2,skf12(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f21,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| nonreflexive(skc2,skf12(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f22,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| see(skc2,skf12(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f23,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| coffee(skc2,skf14(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f24,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| drink(skc2,skf13(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f25,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| nonreflexive(skc2,skf13(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f26,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| past(skc2,skf13(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f27,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| event(skc2,skf13(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f28,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| human_person(skc2,skf15(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f29,negated_conjecture,(
% 0.17/0.49 (![U,V]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| agent(skc13,skf26(V),V) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f30,negated_conjecture,(
% 0.17/0.49 (![U,V]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| agent(skc2,skf12(V),V) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f31,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| patient(skc13,skf26(W),skf29(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f32,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| agent(skc13,skf27(W),skf29(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f33,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc13,U)| ~ in(skc13,V,U)| ~ customer(skc13,V)| ssSkC0| patient(skc13,skf27(W),skf28(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f34,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| agent(skc2,skf13(W),skf15(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f35,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| patient(skc2,skf12(W),skf15(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f36,negated_conjecture,(
% 0.17/0.49 (![U,V,W]: (( ~ restaurant(skc2,U)| ~ in(skc2,V,U)| ~ customer(skc2,V)| ~ ssSkC0| patient(skc2,skf13(W),skf14(W)) ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f37,negated_conjecture,(
% 0.17/0.49 (![U,V,W,X,Y]: (( ~ event(U,V)| ~ agent(U,V,skf39(U))| ~ past(U,V)| ~ nonreflexive(U,V)| ~ see(U,V)| ~ patient(U,W,X)| ~ coffee(U,X)| ~ drink(U,W)| ~ nonreflexive(U,W)| ~ past(U,W)| ~ event(U,W)| ~ human_person(U,Y)| ~ agent(U,W,Y)| ~ patient(U,V,Y)| ~ actual_world(U)| ssSkC0 ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f38,negated_conjecture,(
% 0.17/0.49 (![U,V,W,X,Y]: (( ~ event(U,V)| ~ agent(U,V,skf25(U))| ~ past(U,V)| ~ nonreflexive(U,V)| ~ see(U,V)| ~ patient(U,V,W)| ~ agent(U,X,W)| ~ human_person(U,W)| ~ drink(U,X)| ~ nonreflexive(U,X)| ~ past(U,X)| ~ event(U,X)| ~ coffee(U,Y)| ~ patient(U,X,Y)| ~ actual_world(U)| ~ ssSkC0 ) ))),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f39,plain,(
% 0.17/0.49 actual_world(skc13)),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f1])).
% 0.17/0.49 fof(f40,plain,(
% 0.17/0.49 actual_world(skc2)),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f2])).
% 0.17/0.49 fof(f41,plain,(
% 0.17/0.49 ![X0]: (~actual_world(X0)|ssSkC0|customer(X0,skf39(X0)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f3])).
% 0.17/0.49 fof(f42,plain,(
% 0.17/0.49 ![X0]: (~actual_world(X0)|ssSkC0|restaurant(X0,skf34(X0)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.17/0.49 fof(f43,plain,(
% 0.17/0.49 ![X0]: (~actual_world(X0)|~ssSkC0|customer(X0,skf25(X0)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.49 fof(f44,plain,(
% 0.17/0.49 ![X0]: (~actual_world(X0)|~ssSkC0|restaurant(X0,skf20(X0)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.49 fof(f45,plain,(
% 0.17/0.49 ![X0]: (~actual_world(X0)|ssSkC0|in(X0,skf39(X0),skf34(X0)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.17/0.49 fof(f46,plain,(
% 0.17/0.49 ![X0]: (~actual_world(X0)|~ssSkC0|in(X0,skf25(X0),skf20(X0)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f8])).
% 0.17/0.49 fof(f47,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V)))|ssSkC0)|(![W]: event(skc13,skf26(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f9])).
% 0.17/0.49 fof(f48,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|event(skc13,skf26(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f47])).
% 0.17/0.49 fof(f49,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V)))|ssSkC0)|(![W]: past(skc13,skf26(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f10])).
% 0.17/0.49 fof(f50,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|past(skc13,skf26(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f49])).
% 0.17/0.49 fof(f51,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V)))|ssSkC0)|(![W]: nonreflexive(skc13,skf26(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f11])).
% 0.17/0.49 fof(f52,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|nonreflexive(skc13,skf26(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f51])).
% 0.17/0.49 fof(f53,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V)))|ssSkC0)|(![W]: see(skc13,skf26(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f12])).
% 0.17/0.49 fof(f54,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|see(skc13,skf26(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f53])).
% 0.17/0.49 fof(f55,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V)))|ssSkC0)|(![W]: human_person(skc13,skf29(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f13])).
% 0.17/0.49 fof(f56,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|human_person(skc13,skf29(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f55])).
% 0.17/0.49 fof(f57,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V)))|ssSkC0)|(![W]: drink(skc13,skf27(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f14])).
% 0.17/0.49 fof(f58,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|drink(skc13,skf27(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f57])).
% 0.17/0.49 fof(f59,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V)))|ssSkC0)|(![W]: nonreflexive(skc13,skf27(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f15])).
% 0.17/0.49 fof(f60,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|nonreflexive(skc13,skf27(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f59])).
% 0.17/0.49 fof(f61,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V)))|ssSkC0)|(![W]: past(skc13,skf27(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f16])).
% 0.17/0.49 fof(f62,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|past(skc13,skf27(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f61])).
% 0.17/0.49 fof(f63,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V)))|ssSkC0)|(![W]: event(skc13,skf27(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f17])).
% 0.17/0.49 fof(f64,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|event(skc13,skf27(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f63])).
% 0.17/0.49 fof(f65,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V)))|ssSkC0)|(![W]: coffee(skc13,skf28(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f18])).
% 0.17/0.49 fof(f66,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|coffee(skc13,skf28(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f65])).
% 0.17/0.49 fof(f67,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V)))|~ssSkC0)|(![W]: event(skc2,skf12(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f19])).
% 0.17/0.49 fof(f68,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|event(skc2,skf12(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f67])).
% 0.17/0.49 fof(f69,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V)))|~ssSkC0)|(![W]: past(skc2,skf12(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f20])).
% 0.17/0.49 fof(f70,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|past(skc2,skf12(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.17/0.49 fof(f71,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V)))|~ssSkC0)|(![W]: nonreflexive(skc2,skf12(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f21])).
% 0.17/0.49 fof(f72,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|nonreflexive(skc2,skf12(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f71])).
% 0.17/0.49 fof(f73,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V)))|~ssSkC0)|(![W]: see(skc2,skf12(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f22])).
% 0.17/0.49 fof(f74,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|see(skc2,skf12(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f73])).
% 0.17/0.49 fof(f75,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V)))|~ssSkC0)|(![W]: coffee(skc2,skf14(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f23])).
% 0.17/0.49 fof(f76,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|coffee(skc2,skf14(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f75])).
% 0.17/0.49 fof(f77,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V)))|~ssSkC0)|(![W]: drink(skc2,skf13(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f24])).
% 0.17/0.49 fof(f78,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|drink(skc2,skf13(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f77])).
% 0.17/0.49 fof(f79,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V)))|~ssSkC0)|(![W]: nonreflexive(skc2,skf13(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f25])).
% 0.17/0.49 fof(f80,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|nonreflexive(skc2,skf13(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f79])).
% 0.17/0.49 fof(f81,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V)))|~ssSkC0)|(![W]: past(skc2,skf13(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f26])).
% 0.17/0.49 fof(f82,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|past(skc2,skf13(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f81])).
% 0.17/0.49 fof(f83,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V)))|~ssSkC0)|(![W]: event(skc2,skf13(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f27])).
% 0.17/0.49 fof(f84,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|event(skc2,skf13(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f83])).
% 0.17/0.49 fof(f85,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V)))|~ssSkC0)|(![W]: human_person(skc2,skf15(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f28])).
% 0.17/0.49 fof(f86,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|human_person(skc2,skf15(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f85])).
% 0.17/0.49 fof(f87,plain,(
% 0.17/0.49 ![V]: ((((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V))|ssSkC0)|agent(skc13,skf26(V),V))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f29])).
% 0.17/0.49 fof(f88,plain,(
% 0.17/0.49 ![X0,X1]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|agent(skc13,skf26(X1),X1))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f87])).
% 0.17/0.49 fof(f89,plain,(
% 0.17/0.49 ![V]: ((((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V))|~ssSkC0)|agent(skc2,skf12(V),V))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f30])).
% 0.17/0.49 fof(f90,plain,(
% 0.17/0.49 ![X0,X1]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|agent(skc2,skf12(X1),X1))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f89])).
% 0.17/0.49 fof(f91,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V)))|ssSkC0)|(![W]: patient(skc13,skf26(W),skf29(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f31])).
% 0.17/0.49 fof(f92,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|patient(skc13,skf26(X2),skf29(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f91])).
% 0.17/0.49 fof(f93,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V)))|ssSkC0)|(![W]: agent(skc13,skf27(W),skf29(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f32])).
% 0.17/0.49 fof(f94,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|agent(skc13,skf27(X2),skf29(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f93])).
% 0.17/0.49 fof(f95,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc13,U)|~in(skc13,V,U)))|~customer(skc13,V)))|ssSkC0)|(![W]: patient(skc13,skf27(W),skf28(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f33])).
% 0.17/0.49 fof(f96,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|ssSkC0|patient(skc13,skf27(X2),skf28(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f95])).
% 0.17/0.49 fof(f97,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V)))|~ssSkC0)|(![W]: agent(skc2,skf13(W),skf15(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f34])).
% 0.17/0.49 fof(f98,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|agent(skc2,skf13(X2),skf15(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f97])).
% 0.17/0.49 fof(f99,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V)))|~ssSkC0)|(![W]: patient(skc2,skf12(W),skf15(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f35])).
% 0.17/0.49 fof(f100,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|patient(skc2,skf12(X2),skf15(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f99])).
% 0.17/0.49 fof(f101,plain,(
% 0.17/0.49 ((![V]: ((![U]: (~restaurant(skc2,U)|~in(skc2,V,U)))|~customer(skc2,V)))|~ssSkC0)|(![W]: patient(skc2,skf13(W),skf14(W)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f36])).
% 0.17/0.49 fof(f102,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~ssSkC0|patient(skc2,skf13(X2),skf14(X2)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f101])).
% 0.17/0.49 fof(f103,plain,(
% 0.17/0.49 (![U]: ((![V,Y]: ((![W]: (((((((![X]: ((((((~event(U,V)|~agent(U,V,skf39(U)))|~past(U,V))|~nonreflexive(U,V))|~see(U,V))|~patient(U,W,X))|~coffee(U,X)))|~drink(U,W))|~nonreflexive(U,W))|~past(U,W))|~event(U,W))|~human_person(U,Y))|~agent(U,W,Y)))|~patient(U,V,Y)))|~actual_world(U)))|ssSkC0),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f37])).
% 0.17/0.49 fof(f104,plain,(
% 0.17/0.49 ![X0,X1,X2,X3,X4]: (~event(X0,X1)|~agent(X0,X1,skf39(X0))|~past(X0,X1)|~nonreflexive(X0,X1)|~see(X0,X1)|~patient(X0,X2,X3)|~coffee(X0,X3)|~drink(X0,X2)|~nonreflexive(X0,X2)|~past(X0,X2)|~event(X0,X2)|~human_person(X0,X4)|~agent(X0,X2,X4)|~patient(X0,X1,X4)|~actual_world(X0)|ssSkC0)),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f103])).
% 0.17/0.49 fof(f105,plain,(
% 0.17/0.49 (![U]: ((![X,Y]: (((((((![W]: (((![V]: (((((~event(U,V)|~agent(U,V,skf25(U)))|~past(U,V))|~nonreflexive(U,V))|~see(U,V))|~patient(U,V,W)))|~agent(U,X,W))|~human_person(U,W)))|~drink(U,X))|~nonreflexive(U,X))|~past(U,X))|~event(U,X))|~coffee(U,Y))|~patient(U,X,Y)))|~actual_world(U)))|~ssSkC0),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f38])).
% 0.17/0.49 fof(f106,plain,(
% 0.17/0.49 ![X0,X1,X2,X3,X4]: (~event(X0,X1)|~agent(X0,X1,skf25(X0))|~past(X0,X1)|~nonreflexive(X0,X1)|~see(X0,X1)|~patient(X0,X1,X2)|~agent(X0,X3,X2)|~human_person(X0,X2)|~drink(X0,X3)|~nonreflexive(X0,X3)|~past(X0,X3)|~event(X0,X3)|~coffee(X0,X4)|~patient(X0,X3,X4)|~actual_world(X0)|~ssSkC0)),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f105])).
% 0.17/0.49 fof(f107,definition,(
% 0.17/0.49 ![X0]: (sQ0_spl <=> (~actual_world(X0)|customer(X0,skf39(X0))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f108,plain,(
% 0.17/0.49 ![X0]: (~actual_world(X0)|customer(X0,skf39(X0))|~sQ0_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f107])).
% 0.17/0.49 fof(f110,definition,(
% 0.17/0.49 sQ1_spl <=> (ssSkC0)),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f113,plain,(
% 0.17/0.49 sQ0_spl|sQ1_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f41,f107,f110])).
% 0.17/0.49 fof(f114,definition,(
% 0.17/0.49 ![X0]: (sQ2_spl <=> (~actual_world(X0)|restaurant(X0,skf34(X0))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f115,plain,(
% 0.17/0.49 ![X0]: (~actual_world(X0)|restaurant(X0,skf34(X0))|~sQ2_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f114])).
% 0.17/0.49 fof(f117,plain,(
% 0.17/0.49 sQ2_spl|sQ1_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f42,f114,f110])).
% 0.17/0.49 fof(f118,definition,(
% 0.17/0.49 ![X0]: (sQ3_spl <=> (~actual_world(X0)|customer(X0,skf25(X0))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f119,plain,(
% 0.17/0.49 ![X0]: (~actual_world(X0)|customer(X0,skf25(X0))|~sQ3_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f118])).
% 0.17/0.49 fof(f121,plain,(
% 0.17/0.49 sQ3_spl|~sQ1_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f43,f118,f110])).
% 0.17/0.49 fof(f122,definition,(
% 0.17/0.49 ![X0]: (sQ4_spl <=> (~actual_world(X0)|restaurant(X0,skf20(X0))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f123,plain,(
% 0.17/0.49 ![X0]: (~actual_world(X0)|restaurant(X0,skf20(X0))|~sQ4_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f122])).
% 0.17/0.49 fof(f125,plain,(
% 0.17/0.49 sQ4_spl|~sQ1_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f44,f122,f110])).
% 0.17/0.49 fof(f126,definition,(
% 0.17/0.49 ![X0]: (sQ5_spl <=> (~actual_world(X0)|in(X0,skf39(X0),skf34(X0))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f127,plain,(
% 0.17/0.49 ![X0]: (~actual_world(X0)|in(X0,skf39(X0),skf34(X0))|~sQ5_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f126])).
% 0.17/0.49 fof(f129,plain,(
% 0.17/0.49 sQ5_spl|sQ1_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f45,f126,f110])).
% 0.17/0.49 fof(f130,definition,(
% 0.17/0.49 ![X0]: (sQ6_spl <=> (~actual_world(X0)|in(X0,skf25(X0),skf20(X0))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f131,plain,(
% 0.17/0.49 ![X0]: (~actual_world(X0)|in(X0,skf25(X0),skf20(X0))|~sQ6_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f130])).
% 0.17/0.49 fof(f133,plain,(
% 0.17/0.49 sQ6_spl|~sQ1_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f46,f130,f110])).
% 0.17/0.49 fof(f134,definition,(
% 0.17/0.49 ![X0,X1]: (sQ7_spl <=> (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f135,plain,(
% 0.17/0.49 ![X0,X1]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|~sQ7_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f134])).
% 0.17/0.49 fof(f137,definition,(
% 0.17/0.49 ![X2]: (sQ8_spl <=> (event(skc13,skf26(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f138,plain,(
% 0.17/0.49 ![X0]: (event(skc13,skf26(X0))|~sQ8_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f137])).
% 0.17/0.49 fof(f140,plain,(
% 0.17/0.49 sQ7_spl|sQ1_spl|sQ8_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f48,f134,f110,f137])).
% 0.17/0.49 fof(f141,definition,(
% 0.17/0.49 ![X2]: (sQ9_spl <=> (past(skc13,skf26(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f142,plain,(
% 0.17/0.49 ![X0]: (past(skc13,skf26(X0))|~sQ9_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f141])).
% 0.17/0.49 fof(f144,plain,(
% 0.17/0.49 sQ7_spl|sQ1_spl|sQ9_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f50,f134,f110,f141])).
% 0.17/0.49 fof(f145,definition,(
% 0.17/0.49 ![X2]: (sQ10_spl <=> (nonreflexive(skc13,skf26(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f146,plain,(
% 0.17/0.49 ![X0]: (nonreflexive(skc13,skf26(X0))|~sQ10_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f145])).
% 0.17/0.49 fof(f148,plain,(
% 0.17/0.49 sQ7_spl|sQ1_spl|sQ10_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f52,f134,f110,f145])).
% 0.17/0.49 fof(f149,definition,(
% 0.17/0.49 ![X2]: (sQ11_spl <=> (see(skc13,skf26(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f150,plain,(
% 0.17/0.49 ![X0]: (see(skc13,skf26(X0))|~sQ11_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f149])).
% 0.17/0.49 fof(f152,plain,(
% 0.17/0.49 sQ7_spl|sQ1_spl|sQ11_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f54,f134,f110,f149])).
% 0.17/0.49 fof(f153,definition,(
% 0.17/0.49 ![X2]: (sQ12_spl <=> (human_person(skc13,skf29(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f154,plain,(
% 0.17/0.49 ![X0]: (human_person(skc13,skf29(X0))|~sQ12_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f153])).
% 0.17/0.49 fof(f156,plain,(
% 0.17/0.49 sQ7_spl|sQ1_spl|sQ12_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f56,f134,f110,f153])).
% 0.17/0.49 fof(f157,definition,(
% 0.17/0.49 ![X2]: (sQ13_spl <=> (drink(skc13,skf27(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f158,plain,(
% 0.17/0.49 ![X0]: (drink(skc13,skf27(X0))|~sQ13_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f157])).
% 0.17/0.49 fof(f160,plain,(
% 0.17/0.49 sQ7_spl|sQ1_spl|sQ13_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f58,f134,f110,f157])).
% 0.17/0.49 fof(f161,definition,(
% 0.17/0.49 ![X2]: (sQ14_spl <=> (nonreflexive(skc13,skf27(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f162,plain,(
% 0.17/0.49 ![X0]: (nonreflexive(skc13,skf27(X0))|~sQ14_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f161])).
% 0.17/0.49 fof(f164,plain,(
% 0.17/0.49 sQ7_spl|sQ1_spl|sQ14_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f60,f134,f110,f161])).
% 0.17/0.49 fof(f165,definition,(
% 0.17/0.49 ![X2]: (sQ15_spl <=> (past(skc13,skf27(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f166,plain,(
% 0.17/0.49 ![X0]: (past(skc13,skf27(X0))|~sQ15_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f165])).
% 0.17/0.49 fof(f168,plain,(
% 0.17/0.49 sQ7_spl|sQ1_spl|sQ15_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f62,f134,f110,f165])).
% 0.17/0.49 fof(f169,definition,(
% 0.17/0.49 ![X2]: (sQ16_spl <=> (event(skc13,skf27(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f170,plain,(
% 0.17/0.49 ![X0]: (event(skc13,skf27(X0))|~sQ16_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f169])).
% 0.17/0.49 fof(f172,plain,(
% 0.17/0.49 sQ7_spl|sQ1_spl|sQ16_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f64,f134,f110,f169])).
% 0.17/0.49 fof(f173,definition,(
% 0.17/0.49 ![X2]: (sQ17_spl <=> (coffee(skc13,skf28(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f174,plain,(
% 0.17/0.49 ![X0]: (coffee(skc13,skf28(X0))|~sQ17_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f173])).
% 0.17/0.49 fof(f176,plain,(
% 0.17/0.49 sQ7_spl|sQ1_spl|sQ17_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f66,f134,f110,f173])).
% 0.17/0.49 fof(f177,definition,(
% 0.17/0.49 ![X0,X1]: (sQ18_spl <=> (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f178,plain,(
% 0.17/0.49 ![X0,X1]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|~sQ18_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f177])).
% 0.17/0.49 fof(f180,definition,(
% 0.17/0.49 ![X2]: (sQ19_spl <=> (event(skc2,skf12(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f181,plain,(
% 0.17/0.49 ![X0]: (event(skc2,skf12(X0))|~sQ19_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f180])).
% 0.17/0.49 fof(f183,plain,(
% 0.17/0.49 sQ18_spl|~sQ1_spl|sQ19_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f68,f177,f110,f180])).
% 0.17/0.49 fof(f184,definition,(
% 0.17/0.49 ![X2]: (sQ20_spl <=> (past(skc2,skf12(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f185,plain,(
% 0.17/0.49 ![X0]: (past(skc2,skf12(X0))|~sQ20_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f184])).
% 0.17/0.49 fof(f187,plain,(
% 0.17/0.49 sQ18_spl|~sQ1_spl|sQ20_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f70,f177,f110,f184])).
% 0.17/0.49 fof(f188,definition,(
% 0.17/0.49 ![X2]: (sQ21_spl <=> (nonreflexive(skc2,skf12(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f189,plain,(
% 0.17/0.49 ![X0]: (nonreflexive(skc2,skf12(X0))|~sQ21_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f188])).
% 0.17/0.49 fof(f191,plain,(
% 0.17/0.49 sQ18_spl|~sQ1_spl|sQ21_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f72,f177,f110,f188])).
% 0.17/0.49 fof(f192,definition,(
% 0.17/0.49 ![X2]: (sQ22_spl <=> (see(skc2,skf12(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f193,plain,(
% 0.17/0.49 ![X0]: (see(skc2,skf12(X0))|~sQ22_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f192])).
% 0.17/0.49 fof(f195,plain,(
% 0.17/0.49 sQ18_spl|~sQ1_spl|sQ22_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f74,f177,f110,f192])).
% 0.17/0.49 fof(f196,definition,(
% 0.17/0.49 ![X2]: (sQ23_spl <=> (coffee(skc2,skf14(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f197,plain,(
% 0.17/0.49 ![X0]: (coffee(skc2,skf14(X0))|~sQ23_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f196])).
% 0.17/0.49 fof(f199,plain,(
% 0.17/0.49 sQ18_spl|~sQ1_spl|sQ23_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f76,f177,f110,f196])).
% 0.17/0.49 fof(f200,definition,(
% 0.17/0.49 ![X2]: (sQ24_spl <=> (drink(skc2,skf13(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f201,plain,(
% 0.17/0.49 ![X0]: (drink(skc2,skf13(X0))|~sQ24_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f200])).
% 0.17/0.49 fof(f203,plain,(
% 0.17/0.49 sQ18_spl|~sQ1_spl|sQ24_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f78,f177,f110,f200])).
% 0.17/0.49 fof(f204,definition,(
% 0.17/0.49 ![X2]: (sQ25_spl <=> (nonreflexive(skc2,skf13(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f205,plain,(
% 0.17/0.49 ![X0]: (nonreflexive(skc2,skf13(X0))|~sQ25_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f204])).
% 0.17/0.49 fof(f207,plain,(
% 0.17/0.49 sQ18_spl|~sQ1_spl|sQ25_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f80,f177,f110,f204])).
% 0.17/0.49 fof(f208,definition,(
% 0.17/0.49 ![X2]: (sQ26_spl <=> (past(skc2,skf13(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f209,plain,(
% 0.17/0.49 ![X0]: (past(skc2,skf13(X0))|~sQ26_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f208])).
% 0.17/0.49 fof(f211,plain,(
% 0.17/0.49 sQ18_spl|~sQ1_spl|sQ26_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f82,f177,f110,f208])).
% 0.17/0.49 fof(f212,definition,(
% 0.17/0.49 ![X2]: (sQ27_spl <=> (event(skc2,skf13(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f213,plain,(
% 0.17/0.49 ![X0]: (event(skc2,skf13(X0))|~sQ27_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f212])).
% 0.17/0.49 fof(f215,plain,(
% 0.17/0.49 sQ18_spl|~sQ1_spl|sQ27_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f84,f177,f110,f212])).
% 0.17/0.49 fof(f216,definition,(
% 0.17/0.49 ![X2]: (sQ28_spl <=> (human_person(skc2,skf15(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f217,plain,(
% 0.17/0.49 ![X0]: (human_person(skc2,skf15(X0))|~sQ28_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f216])).
% 0.17/0.49 fof(f219,plain,(
% 0.17/0.49 sQ18_spl|~sQ1_spl|sQ28_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f86,f177,f110,f216])).
% 0.17/0.49 fof(f220,definition,(
% 0.17/0.49 ![X0,X1]: (sQ29_spl <=> (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|agent(skc13,skf26(X1),X1)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f221,plain,(
% 0.17/0.49 ![X0,X1]: (~restaurant(skc13,X0)|~in(skc13,X1,X0)|~customer(skc13,X1)|agent(skc13,skf26(X1),X1)|~sQ29_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f220])).
% 0.17/0.49 fof(f223,plain,(
% 0.17/0.49 sQ29_spl|sQ1_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f88,f220,f110])).
% 0.17/0.49 fof(f224,definition,(
% 0.17/0.49 ![X0,X1]: (sQ30_spl <=> (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|agent(skc2,skf12(X1),X1)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f225,plain,(
% 0.17/0.49 ![X0,X1]: (~restaurant(skc2,X0)|~in(skc2,X1,X0)|~customer(skc2,X1)|agent(skc2,skf12(X1),X1)|~sQ30_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f224])).
% 0.17/0.49 fof(f227,plain,(
% 0.17/0.49 sQ30_spl|~sQ1_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f90,f224,f110])).
% 0.17/0.49 fof(f228,definition,(
% 0.17/0.49 ![X2]: (sQ31_spl <=> (patient(skc13,skf26(X2),skf29(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f229,plain,(
% 0.17/0.49 ![X0]: (patient(skc13,skf26(X0),skf29(X0))|~sQ31_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f228])).
% 0.17/0.49 fof(f231,plain,(
% 0.17/0.49 sQ7_spl|sQ1_spl|sQ31_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f92,f134,f110,f228])).
% 0.17/0.49 fof(f232,definition,(
% 0.17/0.49 ![X2]: (sQ32_spl <=> (agent(skc13,skf27(X2),skf29(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f233,plain,(
% 0.17/0.49 ![X0]: (agent(skc13,skf27(X0),skf29(X0))|~sQ32_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f232])).
% 0.17/0.49 fof(f235,plain,(
% 0.17/0.49 sQ7_spl|sQ1_spl|sQ32_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f94,f134,f110,f232])).
% 0.17/0.49 fof(f236,definition,(
% 0.17/0.49 ![X2]: (sQ33_spl <=> (patient(skc13,skf27(X2),skf28(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f237,plain,(
% 0.17/0.49 ![X0]: (patient(skc13,skf27(X0),skf28(X0))|~sQ33_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f236])).
% 0.17/0.49 fof(f239,plain,(
% 0.17/0.49 sQ7_spl|sQ1_spl|sQ33_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f96,f134,f110,f236])).
% 0.17/0.49 fof(f240,definition,(
% 0.17/0.49 ![X2]: (sQ34_spl <=> (agent(skc2,skf13(X2),skf15(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f241,plain,(
% 0.17/0.49 ![X0]: (agent(skc2,skf13(X0),skf15(X0))|~sQ34_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f240])).
% 0.17/0.49 fof(f243,plain,(
% 0.17/0.49 sQ18_spl|~sQ1_spl|sQ34_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f98,f177,f110,f240])).
% 0.17/0.49 fof(f244,definition,(
% 0.17/0.49 ![X2]: (sQ35_spl <=> (patient(skc2,skf12(X2),skf15(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f245,plain,(
% 0.17/0.49 ![X0]: (patient(skc2,skf12(X0),skf15(X0))|~sQ35_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f244])).
% 0.17/0.49 fof(f247,plain,(
% 0.17/0.49 sQ18_spl|~sQ1_spl|sQ35_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f100,f177,f110,f244])).
% 0.17/0.49 fof(f248,definition,(
% 0.17/0.49 ![X2]: (sQ36_spl <=> (patient(skc2,skf13(X2),skf14(X2))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f249,plain,(
% 0.17/0.49 ![X0]: (patient(skc2,skf13(X0),skf14(X0))|~sQ36_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f248])).
% 0.17/0.49 fof(f251,plain,(
% 0.17/0.49 sQ18_spl|~sQ1_spl|sQ36_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f102,f177,f110,f248])).
% 0.17/0.49 fof(f252,definition,(
% 0.17/0.49 ![X0,X1,X2,X3,X4]: (sQ37_spl <=> (~event(X0,X1)|~agent(X0,X1,skf39(X0))|~past(X0,X1)|~nonreflexive(X0,X1)|~see(X0,X1)|~patient(X0,X2,X3)|~coffee(X0,X3)|~drink(X0,X2)|~nonreflexive(X0,X2)|~past(X0,X2)|~event(X0,X2)|~human_person(X0,X4)|~agent(X0,X2,X4)|~patient(X0,X1,X4)|~actual_world(X0)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f253,plain,(
% 0.17/0.49 ![X0,X1,X2,X3,X4]: (~event(X0,X1)|~agent(X0,X1,skf39(X0))|~past(X0,X1)|~nonreflexive(X0,X1)|~see(X0,X1)|~patient(X0,X2,X3)|~coffee(X0,X3)|~drink(X0,X2)|~nonreflexive(X0,X2)|~past(X0,X2)|~event(X0,X2)|~human_person(X0,X4)|~agent(X0,X2,X4)|~patient(X0,X1,X4)|~actual_world(X0)|~sQ37_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f252])).
% 0.17/0.49 fof(f255,plain,(
% 0.17/0.49 sQ37_spl|sQ1_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f104,f252,f110])).
% 0.17/0.49 fof(f256,definition,(
% 0.17/0.49 ![X0,X1,X2,X3,X4]: (sQ38_spl <=> (~event(X0,X1)|~agent(X0,X1,skf25(X0))|~past(X0,X1)|~nonreflexive(X0,X1)|~see(X0,X1)|~patient(X0,X1,X2)|~agent(X0,X3,X2)|~human_person(X0,X2)|~drink(X0,X3)|~nonreflexive(X0,X3)|~past(X0,X3)|~event(X0,X3)|~coffee(X0,X4)|~patient(X0,X3,X4)|~actual_world(X0)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f257,plain,(
% 0.17/0.49 ![X0,X1,X2,X3,X4]: (~event(X0,X1)|~agent(X0,X1,skf25(X0))|~past(X0,X1)|~nonreflexive(X0,X1)|~see(X0,X1)|~patient(X0,X1,X2)|~agent(X0,X3,X2)|~human_person(X0,X2)|~drink(X0,X3)|~nonreflexive(X0,X3)|~past(X0,X3)|~event(X0,X3)|~coffee(X0,X4)|~patient(X0,X3,X4)|~actual_world(X0)|~sQ38_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f256])).
% 0.17/0.49 fof(f259,plain,(
% 0.17/0.49 sQ38_spl|~sQ1_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f106,f256,f110])).
% 0.17/0.49 fof(f260,plain,(
% 0.17/0.49 restaurant(skc2,skf20(skc2))|~sQ4_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f123,f40])).
% 0.17/0.49 fof(f261,plain,(
% 0.17/0.49 restaurant(skc13,skf20(skc13))|~sQ4_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f123,f39])).
% 0.17/0.49 fof(f262,plain,(
% 0.17/0.49 customer(skc2,skf25(skc2))|~sQ3_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f119,f40])).
% 0.17/0.49 fof(f263,plain,(
% 0.17/0.49 customer(skc13,skf25(skc13))|~sQ3_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f119,f39])).
% 0.17/0.49 fof(f264,plain,(
% 0.17/0.49 in(skc2,skf25(skc2),skf20(skc2))|~sQ6_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f131,f40])).
% 0.17/0.49 fof(f265,plain,(
% 0.17/0.49 in(skc13,skf25(skc13),skf20(skc13))|~sQ6_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f131,f39])).
% 0.17/0.49 fof(f266,plain,(
% 0.17/0.49 restaurant(skc2,skf34(skc2))|~sQ2_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f115,f40])).
% 0.17/0.49 fof(f267,plain,(
% 0.17/0.49 restaurant(skc13,skf34(skc13))|~sQ2_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f115,f39])).
% 0.17/0.49 fof(f268,plain,(
% 0.17/0.49 in(skc2,skf39(skc2),skf34(skc2))|~sQ5_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f127,f40])).
% 0.17/0.49 fof(f269,plain,(
% 0.17/0.49 in(skc13,skf39(skc13),skf34(skc13))|~sQ5_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f127,f39])).
% 0.17/0.49 fof(f270,plain,(
% 0.17/0.49 customer(skc2,skf39(skc2))|~sQ0_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f108,f40])).
% 0.17/0.49 fof(f271,plain,(
% 0.17/0.49 customer(skc13,skf39(skc13))|~sQ0_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f108,f39])).
% 0.17/0.49 fof(f272,plain,(
% 0.17/0.49 ~restaurant(skc2,skf20(skc2))|~customer(skc2,skf25(skc2))|~sQ6_spl|~sQ18_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f264,f178])).
% 0.17/0.49 fof(f273,definition,(
% 0.17/0.49 sQ39_spl <=> (restaurant(skc2,skf20(skc2)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f275,plain,(
% 0.17/0.49 ~restaurant(skc2,skf20(skc2))|sQ39_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f273])).
% 0.17/0.49 fof(f276,definition,(
% 0.17/0.49 sQ40_spl <=> (customer(skc2,skf25(skc2)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f278,plain,(
% 0.17/0.49 ~customer(skc2,skf25(skc2))|sQ40_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f276])).
% 0.17/0.49 fof(f279,plain,(
% 0.17/0.49 ~sQ39_spl|~sQ40_spl|~sQ6_spl|~sQ18_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f272,f273,f276,f130,f177])).
% 0.17/0.49 fof(f280,plain,(
% 0.17/0.49 $false|~sQ3_spl|sQ40_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f278,f262])).
% 0.17/0.49 fof(f281,plain,(
% 0.17/0.49 ~sQ3_spl|sQ40_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f280])).
% 0.17/0.49 fof(f282,plain,(
% 0.17/0.49 $false|~sQ4_spl|sQ39_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f275,f260])).
% 0.17/0.49 fof(f283,plain,(
% 0.17/0.49 ~sQ4_spl|sQ39_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f282])).
% 0.17/0.49 fof(f284,plain,(
% 0.17/0.49 ~restaurant(skc2,skf34(skc2))|~customer(skc2,skf39(skc2))|~sQ5_spl|~sQ18_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f268,f178])).
% 0.17/0.49 fof(f285,definition,(
% 0.17/0.49 sQ41_spl <=> (restaurant(skc2,skf34(skc2)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f287,plain,(
% 0.17/0.49 ~restaurant(skc2,skf34(skc2))|sQ41_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f285])).
% 0.17/0.49 fof(f288,definition,(
% 0.17/0.49 sQ42_spl <=> (customer(skc2,skf39(skc2)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f290,plain,(
% 0.17/0.49 ~customer(skc2,skf39(skc2))|sQ42_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f288])).
% 0.17/0.49 fof(f291,plain,(
% 0.17/0.49 ~sQ41_spl|~sQ42_spl|~sQ5_spl|~sQ18_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f284,f285,f288,f126,f177])).
% 0.17/0.49 fof(f297,plain,(
% 0.17/0.49 $false|~sQ0_spl|sQ42_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f290,f270])).
% 0.17/0.49 fof(f298,plain,(
% 0.17/0.49 ~sQ0_spl|sQ42_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f297])).
% 0.17/0.49 fof(f299,plain,(
% 0.17/0.49 $false|~sQ2_spl|sQ41_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f287,f266])).
% 0.17/0.49 fof(f300,plain,(
% 0.17/0.49 ~sQ2_spl|sQ41_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f299])).
% 0.17/0.49 fof(f307,plain,(
% 0.17/0.49 ~restaurant(skc13,skf34(skc13))|~customer(skc13,skf39(skc13))|~sQ5_spl|~sQ7_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f269,f135])).
% 0.17/0.49 fof(f308,definition,(
% 0.17/0.49 sQ44_spl <=> (restaurant(skc13,skf34(skc13)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f310,plain,(
% 0.17/0.49 ~restaurant(skc13,skf34(skc13))|sQ44_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f308])).
% 0.17/0.49 fof(f311,definition,(
% 0.17/0.49 sQ45_spl <=> (customer(skc13,skf39(skc13)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f313,plain,(
% 0.17/0.49 ~customer(skc13,skf39(skc13))|sQ45_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f311])).
% 0.17/0.49 fof(f314,plain,(
% 0.17/0.49 ~sQ44_spl|~sQ45_spl|~sQ5_spl|~sQ7_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f307,f308,f311,f126,f134])).
% 0.17/0.49 fof(f315,plain,(
% 0.17/0.49 $false|~sQ0_spl|sQ45_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f313,f271])).
% 0.17/0.49 fof(f316,plain,(
% 0.17/0.49 ~sQ0_spl|sQ45_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f315])).
% 0.17/0.49 fof(f318,definition,(
% 0.17/0.49 sQ46_spl <=> (restaurant(skc13,skf20(skc13)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f320,plain,(
% 0.17/0.49 ~restaurant(skc13,skf20(skc13))|sQ46_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f318])).
% 0.17/0.49 fof(f321,definition,(
% 0.17/0.49 sQ47_spl <=> (customer(skc13,skf25(skc13)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f323,plain,(
% 0.17/0.49 ~customer(skc13,skf25(skc13))|sQ47_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f321])).
% 0.17/0.49 fof(f334,plain,(
% 0.17/0.49 ~restaurant(skc2,skf20(skc2))|~customer(skc2,skf25(skc2))|agent(skc2,skf12(skf25(skc2)),skf25(skc2))|~sQ6_spl|~sQ30_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f264,f225])).
% 0.17/0.49 fof(f335,definition,(
% 0.17/0.49 sQ49_spl <=> (agent(skc2,skf12(skf25(skc2)),skf25(skc2)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f336,plain,(
% 0.17/0.49 agent(skc2,skf12(skf25(skc2)),skf25(skc2))|~sQ49_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f335])).
% 0.17/0.49 fof(f338,plain,(
% 0.17/0.49 ~sQ39_spl|~sQ40_spl|sQ49_spl|~sQ6_spl|~sQ30_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f334,f273,f276,f335,f130,f224])).
% 0.17/0.49 fof(f341,plain,(
% 0.17/0.49 ~restaurant(skc13,skf34(skc13))|~customer(skc13,skf39(skc13))|agent(skc13,skf26(skf39(skc13)),skf39(skc13))|~sQ5_spl|~sQ29_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f269,f221])).
% 0.17/0.49 fof(f342,definition,(
% 0.17/0.49 sQ50_spl <=> (agent(skc13,skf26(skf39(skc13)),skf39(skc13)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f343,plain,(
% 0.17/0.49 agent(skc13,skf26(skf39(skc13)),skf39(skc13))|~sQ50_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f342])).
% 0.17/0.49 fof(f345,plain,(
% 0.17/0.49 ~sQ44_spl|~sQ45_spl|sQ50_spl|~sQ5_spl|~sQ29_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f341,f308,f311,f342,f126,f220])).
% 0.17/0.49 fof(f346,plain,(
% 0.17/0.49 $false|~sQ2_spl|sQ44_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f310,f267])).
% 0.17/0.49 fof(f347,plain,(
% 0.17/0.49 ~sQ2_spl|sQ44_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f346])).
% 0.17/0.49 fof(f348,plain,(
% 0.17/0.49 $false|~sQ3_spl|sQ47_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f323,f263])).
% 0.17/0.49 fof(f349,plain,(
% 0.17/0.49 ~sQ3_spl|sQ47_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f348])).
% 0.17/0.49 fof(f358,plain,(
% 0.17/0.49 $false|sQ46_spl|~sQ4_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f261,f320])).
% 0.17/0.49 fof(f359,plain,(
% 0.17/0.49 sQ46_spl|~sQ4_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f358])).
% 0.17/0.49 fof(f376,definition,(
% 0.17/0.49 sQ56_spl <=> (actual_world(skc2))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f378,plain,(
% 0.17/0.49 ~actual_world(skc2)|sQ56_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f376])).
% 0.17/0.49 fof(f380,plain,(
% 0.17/0.49 $false|sQ56_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f378,f40])).
% 0.17/0.49 fof(f381,plain,(
% 0.17/0.49 sQ56_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f380])).
% 0.17/0.49 fof(f386,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~event(skc13,skf26(skf39(skc13)))|~past(skc13,skf26(skf39(skc13)))|~nonreflexive(skc13,skf26(skf39(skc13)))|~see(skc13,skf26(skf39(skc13)))|~patient(skc13,X0,X1)|~coffee(skc13,X1)|~drink(skc13,X0)|~nonreflexive(skc13,X0)|~past(skc13,X0)|~event(skc13,X0)|~human_person(skc13,X2)|~agent(skc13,X0,X2)|~patient(skc13,skf26(skf39(skc13)),X2)|~actual_world(skc13)|~sQ50_spl|~sQ37_spl)),
% 0.17/0.49 inference(resolution,[status(thm)],[f343,f253])).
% 0.17/0.49 fof(f387,definition,(
% 0.17/0.49 sQ57_spl <=> (event(skc13,skf26(skf39(skc13))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f389,plain,(
% 0.17/0.49 ~event(skc13,skf26(skf39(skc13)))|sQ57_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f387])).
% 0.17/0.49 fof(f390,definition,(
% 0.17/0.49 sQ58_spl <=> (past(skc13,skf26(skf39(skc13))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f392,plain,(
% 0.17/0.49 ~past(skc13,skf26(skf39(skc13)))|sQ58_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f390])).
% 0.17/0.49 fof(f393,definition,(
% 0.17/0.49 sQ59_spl <=> (nonreflexive(skc13,skf26(skf39(skc13))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f395,plain,(
% 0.17/0.49 ~nonreflexive(skc13,skf26(skf39(skc13)))|sQ59_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f393])).
% 0.17/0.49 fof(f396,definition,(
% 0.17/0.49 sQ60_spl <=> (see(skc13,skf26(skf39(skc13))))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f398,plain,(
% 0.17/0.49 ~see(skc13,skf26(skf39(skc13)))|sQ60_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f396])).
% 0.17/0.49 fof(f399,definition,(
% 0.17/0.49 ![X0,X1,X2]: (sQ61_spl <=> (~patient(skc13,X0,X1)|~coffee(skc13,X1)|~drink(skc13,X0)|~nonreflexive(skc13,X0)|~past(skc13,X0)|~event(skc13,X0)|~human_person(skc13,X2)|~agent(skc13,X0,X2)|~patient(skc13,skf26(skf39(skc13)),X2)))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f400,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~patient(skc13,X0,X1)|~coffee(skc13,X1)|~drink(skc13,X0)|~nonreflexive(skc13,X0)|~past(skc13,X0)|~event(skc13,X0)|~human_person(skc13,X2)|~agent(skc13,X0,X2)|~patient(skc13,skf26(skf39(skc13)),X2)|~sQ61_spl)),
% 0.17/0.49 inference(component_clause,[status(thm)],[f399])).
% 0.17/0.49 fof(f402,definition,(
% 0.17/0.49 sQ62_spl <=> (actual_world(skc13))),
% 0.17/0.49 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.17/0.49 fof(f404,plain,(
% 0.17/0.49 ~actual_world(skc13)|sQ62_spl),
% 0.17/0.49 inference(component_clause,[status(thm)],[f402])).
% 0.17/0.49 fof(f405,plain,(
% 0.17/0.49 ~sQ57_spl|~sQ58_spl|~sQ59_spl|~sQ60_spl|sQ61_spl|~sQ62_spl|~sQ50_spl|~sQ37_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f386,f387,f390,f393,f396,f399,f402,f342,f252])).
% 0.17/0.49 fof(f406,plain,(
% 0.17/0.49 $false|sQ62_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f404,f39])).
% 0.17/0.49 fof(f407,plain,(
% 0.17/0.49 sQ62_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f406])).
% 0.17/0.49 fof(f408,plain,(
% 0.17/0.49 $false|~sQ11_spl|sQ60_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f398,f150])).
% 0.17/0.49 fof(f409,plain,(
% 0.17/0.49 ~sQ11_spl|sQ60_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f408])).
% 0.17/0.49 fof(f410,plain,(
% 0.17/0.49 $false|~sQ10_spl|sQ59_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f395,f146])).
% 0.17/0.49 fof(f411,plain,(
% 0.17/0.49 ~sQ10_spl|sQ59_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f410])).
% 0.17/0.49 fof(f412,plain,(
% 0.17/0.49 $false|~sQ9_spl|sQ58_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f392,f142])).
% 0.17/0.49 fof(f413,plain,(
% 0.17/0.49 ~sQ9_spl|sQ58_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f412])).
% 0.17/0.49 fof(f414,plain,(
% 0.17/0.49 $false|~sQ8_spl|sQ57_spl),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f389,f138])).
% 0.17/0.49 fof(f415,plain,(
% 0.17/0.49 ~sQ8_spl|sQ57_spl),
% 0.17/0.49 inference(contradiction_clause,[status(thm)],[f414])).
% 0.17/0.49 fof(f418,plain,(
% 0.17/0.49 ~restaurant(skc13,skf20(skc13))|~customer(skc13,skf25(skc13))|~sQ7_spl|~sQ6_spl),
% 0.17/0.49 inference(resolution,[status(thm)],[f135,f265])).
% 0.17/0.49 fof(f419,plain,(
% 0.17/0.49 ~sQ46_spl|~sQ47_spl|~sQ7_spl|~sQ6_spl),
% 0.17/0.49 inference(split_clause,[status(thm)],[f418,f318,f321,f134,f130])).
% 0.17/0.49 fof(f430,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~event(skc2,skf12(skf25(skc2)))|~past(skc2,skf12(skf25(skc2)))|~nonreflexive(skc2,skf12(skf25(skc2)))|~see(skc2,skf12(skf25(skc2)))|~patient(skc2,skf12(skf25(skc2)),X0)|~agent(skc2,X1,X0)|~human_person(skc2,X0)|~drink(skc2,X1)|~nonreflexive(skc2,X1)|~past(skc2,X1)|~event(skc2,X1)|~coffee(skc2,X2)|~patient(skc2,X1,X2)|~actual_world(skc2)|~sQ49_spl|~sQ38_spl)),
% 0.17/0.49 inference(resolution,[status(thm)],[f336,f257])).
% 0.17/0.49 fof(f431,definition,(
% 0.17/0.49 sQ63_spl <=> (event(skc2,skf12(skf25(skc2))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f433,plain,(
% 0.17/0.50 ~event(skc2,skf12(skf25(skc2)))|sQ63_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f431])).
% 0.17/0.50 fof(f434,definition,(
% 0.17/0.50 sQ64_spl <=> (past(skc2,skf12(skf25(skc2))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f436,plain,(
% 0.17/0.50 ~past(skc2,skf12(skf25(skc2)))|sQ64_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f434])).
% 0.17/0.50 fof(f437,definition,(
% 0.17/0.50 sQ65_spl <=> (nonreflexive(skc2,skf12(skf25(skc2))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f439,plain,(
% 0.17/0.50 ~nonreflexive(skc2,skf12(skf25(skc2)))|sQ65_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f437])).
% 0.17/0.50 fof(f440,definition,(
% 0.17/0.50 sQ66_spl <=> (see(skc2,skf12(skf25(skc2))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f442,plain,(
% 0.17/0.50 ~see(skc2,skf12(skf25(skc2)))|sQ66_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f440])).
% 0.17/0.50 fof(f443,definition,(
% 0.17/0.50 ![X0,X1,X2]: (sQ67_spl <=> (~patient(skc2,skf12(skf25(skc2)),X0)|~agent(skc2,X1,X0)|~human_person(skc2,X0)|~drink(skc2,X1)|~nonreflexive(skc2,X1)|~past(skc2,X1)|~event(skc2,X1)|~coffee(skc2,X2)|~patient(skc2,X1,X2)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f444,plain,(
% 0.17/0.50 ![X0,X1,X2]: (~patient(skc2,skf12(skf25(skc2)),X0)|~agent(skc2,X1,X0)|~human_person(skc2,X0)|~drink(skc2,X1)|~nonreflexive(skc2,X1)|~past(skc2,X1)|~event(skc2,X1)|~coffee(skc2,X2)|~patient(skc2,X1,X2)|~sQ67_spl)),
% 0.17/0.50 inference(component_clause,[status(thm)],[f443])).
% 0.17/0.50 fof(f446,plain,(
% 0.17/0.50 ~sQ63_spl|~sQ64_spl|~sQ65_spl|~sQ66_spl|sQ67_spl|~sQ56_spl|~sQ49_spl|~sQ38_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f430,f431,f434,f437,f440,f443,f376,f335,f256])).
% 0.17/0.50 fof(f447,plain,(
% 0.17/0.50 $false|~sQ21_spl|sQ65_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f439,f189])).
% 0.17/0.50 fof(f448,plain,(
% 0.17/0.50 ~sQ21_spl|sQ65_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f447])).
% 0.17/0.50 fof(f449,plain,(
% 0.17/0.50 $false|~sQ20_spl|sQ64_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f436,f185])).
% 0.17/0.50 fof(f450,plain,(
% 0.17/0.50 ~sQ20_spl|sQ64_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f449])).
% 0.17/0.50 fof(f451,plain,(
% 0.17/0.50 $false|~sQ19_spl|sQ63_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f433,f181])).
% 0.17/0.50 fof(f452,plain,(
% 0.17/0.50 ~sQ19_spl|sQ63_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f451])).
% 0.17/0.50 fof(f465,plain,(
% 0.17/0.50 ![X0,X1]: (~patient(skc13,X0,X1)|~coffee(skc13,X1)|~drink(skc13,X0)|~nonreflexive(skc13,X0)|~past(skc13,X0)|~event(skc13,X0)|~human_person(skc13,skf29(skf39(skc13)))|~agent(skc13,X0,skf29(skf39(skc13)))|~sQ61_spl|~sQ31_spl)),
% 0.17/0.50 inference(resolution,[status(thm)],[f400,f229])).
% 0.17/0.50 fof(f466,definition,(
% 0.17/0.50 ![X0,X1]: (sQ70_spl <=> (~patient(skc13,X0,X1)|~coffee(skc13,X1)|~drink(skc13,X0)|~nonreflexive(skc13,X0)|~past(skc13,X0)|~event(skc13,X0)|~agent(skc13,X0,skf29(skf39(skc13)))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f467,plain,(
% 0.17/0.50 ![X0,X1]: (~patient(skc13,X0,X1)|~coffee(skc13,X1)|~drink(skc13,X0)|~nonreflexive(skc13,X0)|~past(skc13,X0)|~event(skc13,X0)|~agent(skc13,X0,skf29(skf39(skc13)))|~sQ70_spl)),
% 0.17/0.50 inference(component_clause,[status(thm)],[f466])).
% 0.17/0.50 fof(f469,definition,(
% 0.17/0.50 sQ71_spl <=> (human_person(skc13,skf29(skf39(skc13))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f471,plain,(
% 0.17/0.50 ~human_person(skc13,skf29(skf39(skc13)))|sQ71_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f469])).
% 0.17/0.50 fof(f472,plain,(
% 0.17/0.50 sQ70_spl|~sQ71_spl|~sQ61_spl|~sQ31_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f465,f466,f469,f399,f228])).
% 0.17/0.50 fof(f473,plain,(
% 0.17/0.50 $false|~sQ12_spl|sQ71_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f471,f154])).
% 0.17/0.50 fof(f474,plain,(
% 0.17/0.50 ~sQ12_spl|sQ71_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f473])).
% 0.17/0.50 fof(f478,plain,(
% 0.17/0.50 $false|~sQ22_spl|sQ66_spl),
% 0.17/0.50 inference(backward_subsumption_resolution,[status(thm)],[f442,f193])).
% 0.17/0.50 fof(f496,definition,(
% 0.17/0.50 sQ73_spl <=> (drink(skc2,skf13(skf39(skc2))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f498,plain,(
% 0.17/0.50 ~drink(skc2,skf13(skf39(skc2)))|sQ73_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f496])).
% 0.17/0.50 fof(f515,plain,(
% 0.17/0.50 $false|~sQ24_spl|sQ73_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f498,f201])).
% 0.17/0.50 fof(f516,plain,(
% 0.17/0.50 ~sQ24_spl|sQ73_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f515])).
% 0.17/0.50 fof(f520,plain,(
% 0.17/0.50 ![X0]: (~patient(skc13,skf27(skf39(skc13)),X0)|~coffee(skc13,X0)|~drink(skc13,skf27(skf39(skc13)))|~nonreflexive(skc13,skf27(skf39(skc13)))|~past(skc13,skf27(skf39(skc13)))|~event(skc13,skf27(skf39(skc13)))|~sQ70_spl|~sQ32_spl)),
% 0.17/0.50 inference(resolution,[status(thm)],[f467,f233])).
% 0.17/0.50 fof(f521,definition,(
% 0.17/0.50 ![X0]: (sQ77_spl <=> (~patient(skc13,skf27(skf39(skc13)),X0)|~coffee(skc13,X0)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f522,plain,(
% 0.17/0.50 ![X0]: (~patient(skc13,skf27(skf39(skc13)),X0)|~coffee(skc13,X0)|~sQ77_spl)),
% 0.17/0.50 inference(component_clause,[status(thm)],[f521])).
% 0.17/0.50 fof(f524,definition,(
% 0.17/0.50 sQ78_spl <=> (drink(skc13,skf27(skf39(skc13))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f526,plain,(
% 0.17/0.50 ~drink(skc13,skf27(skf39(skc13)))|sQ78_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f524])).
% 0.17/0.50 fof(f527,definition,(
% 0.17/0.50 sQ79_spl <=> (nonreflexive(skc13,skf27(skf39(skc13))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f529,plain,(
% 0.17/0.50 ~nonreflexive(skc13,skf27(skf39(skc13)))|sQ79_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f527])).
% 0.17/0.50 fof(f530,definition,(
% 0.17/0.50 sQ80_spl <=> (past(skc13,skf27(skf39(skc13))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f532,plain,(
% 0.17/0.50 ~past(skc13,skf27(skf39(skc13)))|sQ80_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f530])).
% 0.17/0.50 fof(f533,definition,(
% 0.17/0.50 sQ81_spl <=> (event(skc13,skf27(skf39(skc13))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f535,plain,(
% 0.17/0.50 ~event(skc13,skf27(skf39(skc13)))|sQ81_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f533])).
% 0.17/0.50 fof(f536,plain,(
% 0.17/0.50 sQ77_spl|~sQ78_spl|~sQ79_spl|~sQ80_spl|~sQ81_spl|~sQ70_spl|~sQ32_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f520,f521,f524,f527,f530,f533,f466,f232])).
% 0.17/0.50 fof(f537,plain,(
% 0.17/0.50 $false|~sQ16_spl|sQ81_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f535,f170])).
% 0.17/0.50 fof(f538,plain,(
% 0.17/0.50 ~sQ16_spl|sQ81_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f537])).
% 0.17/0.50 fof(f539,plain,(
% 0.17/0.50 $false|~sQ15_spl|sQ80_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f532,f166])).
% 0.17/0.50 fof(f540,plain,(
% 0.17/0.50 ~sQ15_spl|sQ80_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f539])).
% 0.17/0.50 fof(f541,plain,(
% 0.17/0.50 $false|~sQ14_spl|sQ79_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f529,f162])).
% 0.17/0.50 fof(f542,plain,(
% 0.17/0.50 ~sQ14_spl|sQ79_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f541])).
% 0.17/0.50 fof(f543,plain,(
% 0.17/0.50 $false|~sQ13_spl|sQ78_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f526,f158])).
% 0.17/0.50 fof(f544,plain,(
% 0.17/0.50 ~sQ13_spl|sQ78_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f543])).
% 0.17/0.50 fof(f559,plain,(
% 0.17/0.50 ~coffee(skc13,skf28(skf39(skc13)))|~sQ77_spl|~sQ33_spl),
% 0.17/0.50 inference(resolution,[status(thm)],[f522,f237])).
% 0.17/0.50 fof(f560,plain,(
% 0.17/0.50 $false|~sQ17_spl|~sQ77_spl|~sQ33_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f559,f174])).
% 0.17/0.50 fof(f561,plain,(
% 0.17/0.50 ~sQ17_spl|~sQ77_spl|~sQ33_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f560])).
% 0.17/0.50 fof(f563,plain,(
% 0.17/0.50 ~sQ22_spl|sQ66_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f478])).
% 0.17/0.50 fof(f570,plain,(
% 0.17/0.50 ![X0,X1]: (~agent(skc2,X0,skf15(skf25(skc2)))|~human_person(skc2,skf15(skf25(skc2)))|~drink(skc2,X0)|~nonreflexive(skc2,X0)|~past(skc2,X0)|~event(skc2,X0)|~coffee(skc2,X1)|~patient(skc2,X0,X1)|~sQ35_spl|~sQ67_spl)),
% 0.17/0.50 inference(resolution,[status(thm)],[f245,f444])).
% 0.17/0.50 fof(f571,definition,(
% 0.17/0.50 ![X0,X1]: (sQ82_spl <=> (~agent(skc2,X0,skf15(skf25(skc2)))|~drink(skc2,X0)|~nonreflexive(skc2,X0)|~past(skc2,X0)|~event(skc2,X0)|~coffee(skc2,X1)|~patient(skc2,X0,X1)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f572,plain,(
% 0.17/0.50 ![X0,X1]: (~agent(skc2,X0,skf15(skf25(skc2)))|~drink(skc2,X0)|~nonreflexive(skc2,X0)|~past(skc2,X0)|~event(skc2,X0)|~coffee(skc2,X1)|~patient(skc2,X0,X1)|~sQ82_spl)),
% 0.17/0.50 inference(component_clause,[status(thm)],[f571])).
% 0.17/0.50 fof(f574,definition,(
% 0.17/0.50 sQ83_spl <=> (human_person(skc2,skf15(skf25(skc2))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f576,plain,(
% 0.17/0.50 ~human_person(skc2,skf15(skf25(skc2)))|sQ83_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f574])).
% 0.17/0.50 fof(f577,plain,(
% 0.17/0.50 sQ82_spl|~sQ83_spl|~sQ35_spl|~sQ67_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f570,f571,f574,f244,f443])).
% 0.17/0.50 fof(f578,plain,(
% 0.17/0.50 $false|~sQ28_spl|sQ83_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f576,f217])).
% 0.17/0.50 fof(f579,plain,(
% 0.17/0.50 ~sQ28_spl|sQ83_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f578])).
% 0.17/0.50 fof(f601,plain,(
% 0.17/0.50 ![X0]: (~drink(skc2,skf13(skf25(skc2)))|~nonreflexive(skc2,skf13(skf25(skc2)))|~past(skc2,skf13(skf25(skc2)))|~event(skc2,skf13(skf25(skc2)))|~coffee(skc2,X0)|~patient(skc2,skf13(skf25(skc2)),X0)|~sQ82_spl|~sQ34_spl)),
% 0.17/0.50 inference(resolution,[status(thm)],[f572,f241])).
% 0.17/0.50 fof(f602,definition,(
% 0.17/0.50 sQ89_spl <=> (drink(skc2,skf13(skf25(skc2))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f604,plain,(
% 0.17/0.50 ~drink(skc2,skf13(skf25(skc2)))|sQ89_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f602])).
% 0.17/0.50 fof(f605,definition,(
% 0.17/0.50 sQ90_spl <=> (nonreflexive(skc2,skf13(skf25(skc2))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f607,plain,(
% 0.17/0.50 ~nonreflexive(skc2,skf13(skf25(skc2)))|sQ90_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f605])).
% 0.17/0.50 fof(f608,definition,(
% 0.17/0.50 sQ91_spl <=> (past(skc2,skf13(skf25(skc2))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f610,plain,(
% 0.17/0.50 ~past(skc2,skf13(skf25(skc2)))|sQ91_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f608])).
% 0.17/0.50 fof(f611,definition,(
% 0.17/0.50 sQ92_spl <=> (event(skc2,skf13(skf25(skc2))))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f613,plain,(
% 0.17/0.50 ~event(skc2,skf13(skf25(skc2)))|sQ92_spl),
% 0.17/0.50 inference(component_clause,[status(thm)],[f611])).
% 0.17/0.50 fof(f614,definition,(
% 0.17/0.50 ![X0]: (sQ93_spl <=> (~coffee(skc2,X0)|~patient(skc2,skf13(skf25(skc2)),X0)))),
% 0.17/0.50 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.17/0.50 fof(f615,plain,(
% 0.17/0.50 ![X0]: (~coffee(skc2,X0)|~patient(skc2,skf13(skf25(skc2)),X0)|~sQ93_spl)),
% 0.17/0.50 inference(component_clause,[status(thm)],[f614])).
% 0.17/0.50 fof(f617,plain,(
% 0.17/0.50 ~sQ89_spl|~sQ90_spl|~sQ91_spl|~sQ92_spl|sQ93_spl|~sQ82_spl|~sQ34_spl),
% 0.17/0.50 inference(split_clause,[status(thm)],[f601,f602,f605,f608,f611,f614,f571,f240])).
% 0.17/0.50 fof(f618,plain,(
% 0.17/0.50 $false|~sQ27_spl|sQ92_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f613,f213])).
% 0.17/0.50 fof(f619,plain,(
% 0.17/0.50 ~sQ27_spl|sQ92_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f618])).
% 0.17/0.50 fof(f620,plain,(
% 0.17/0.50 $false|~sQ26_spl|sQ91_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f610,f209])).
% 0.17/0.50 fof(f621,plain,(
% 0.17/0.50 ~sQ26_spl|sQ91_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f620])).
% 0.17/0.50 fof(f622,plain,(
% 0.17/0.50 $false|~sQ25_spl|sQ90_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f607,f205])).
% 0.17/0.50 fof(f623,plain,(
% 0.17/0.50 ~sQ25_spl|sQ90_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f622])).
% 0.17/0.50 fof(f624,plain,(
% 0.17/0.50 $false|~sQ24_spl|sQ89_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f604,f201])).
% 0.17/0.50 fof(f625,plain,(
% 0.17/0.50 ~sQ24_spl|sQ89_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f624])).
% 0.17/0.50 fof(f626,plain,(
% 0.17/0.50 ~coffee(skc2,skf14(skf25(skc2)))|~sQ93_spl|~sQ36_spl),
% 0.17/0.50 inference(resolution,[status(thm)],[f615,f249])).
% 0.17/0.50 fof(f627,plain,(
% 0.17/0.50 $false|~sQ23_spl|~sQ93_spl|~sQ36_spl),
% 0.17/0.50 inference(forward_subsumption_resolution,[status(thm)],[f626,f197])).
% 0.17/0.50 fof(f628,plain,(
% 0.17/0.50 ~sQ23_spl|~sQ93_spl|~sQ36_spl),
% 0.17/0.50 inference(contradiction_clause,[status(thm)],[f627])).
% 0.17/0.50 fof(f629,plain,(
% 0.17/0.50 $false),
% 0.17/0.50 inference(sat_refutation,[status(thm)],[f113,f117,f121,f125,f129,f133,f140,f144,f148,f152,f156,f160,f164,f168,f172,f176,f183,f187,f191,f195,f199,f203,f207,f211,f215,f219,f223,f227,f231,f235,f239,f243,f247,f251,f255,f259,f279,f281,f283,f291,f298,f300,f314,f316,f338,f345,f347,f349,f359,f381,f405,f407,f409,f411,f413,f415,f419,f446,f448,f450,f452,f472,f474,f516,f536,f538,f540,f542,f544,f561,f563,f577,f579,f617,f619,f621,f623,f625,f628])).
% 0.17/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.55 % Elapsed time: 0.083522 seconds
% 0.17/0.55 % CPU time: 0.155771 seconds
% 0.17/0.55 % Total memory used: 7.529 MB
% 0.17/0.55 % Net memory used: 7.457 MB
%------------------------------------------------------------------------------