%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NLP103-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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 : Tue Sep 29 12:08:52 PM UTC 2026
% Result : Satisfiable 0.10s 0.45s
% Output : Saturation 0.10s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u73,negated_conjecture,
ssSkC0 ).
cnf(u77,negated_conjecture,
( restaurant(X0,X4)
| ~ actual_world(X0)
| event(X0,X5)
| ~ agent(X0,X5,skf12(X0,X4,X3))
| patient(X0,X5,X3)
| ~ past(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ see(X0,X5)
| event(X0,X1)
| human_person(X0,X3)
| ~ agent(X0,X1,X3)
| coffee(X0,X2)
| patient(X0,X1,X2)
| ~ drink(X0,X1)
| ~ nonreflexive(X0,X1)
| ~ past(X0,X1) ) ).
cnf(u85,negated_conjecture,
( restaurant(X0,X4)
| in(X0,skf12(X0,X4,X5),X4)
| ~ actual_world(X0)
| event(X0,X1)
| human_person(X0,X3)
| ~ agent(X0,X1,X3)
| coffee(X0,X2)
| patient(X0,X1,X2)
| ~ drink(X0,X1)
| ~ nonreflexive(X0,X1)
| ~ past(X0,X1) ) ).
cnf(u89,negated_conjecture,
( restaurant(X0,X4)
| ~ customer(X0,skf12(X0,X5,X6))
| ~ actual_world(X0)
| event(X0,X1)
| human_person(X0,X3)
| ~ agent(X0,X1,X3)
| coffee(X0,X2)
| patient(X0,X1,X2)
| ~ drink(X0,X1)
| ~ nonreflexive(X0,X1)
| ~ past(X0,X1) ) ).
cnf(u93,negated_conjecture,
( restaurant(X0,X2)
| in(X0,skf20(X0,X2,X3),X2)
| ~ actual_world(X0)
| coffee(X0,X1) ) ).
cnf(u97,negated_conjecture,
( ~ customer(X0,skf20(X0,X3,X4))
| coffee(X0,X1)
| ~ actual_world(X0)
| restaurant(X0,X2) ) ).
cnf(u101,negated_conjecture,
~ patient(skc8,skf8(X1),skf10(X1)) ).
cnf(u108,negated_conjecture,
agent(skc8,skf9(X1),skf10(X1)) ).
cnf(u112,negated_conjecture,
( customer(skc8,X0)
| agent(skc8,skf8(X0),X0)
| ~ in(skc8,X0,skc10) ) ).
cnf(u116,negated_conjecture,
~ patient(skc8,skf9(X1),skc9) ).
cnf(u120,negated_conjecture,
~ patient(skc20,skf16(X1),skc22) ).
cnf(u123,negated_conjecture,
( customer(skc20,X0)
| ~ in(skc20,X0,skc23) ) ).
cnf(u127,negated_conjecture,
( customer(skc20,X0)
| agent(skc20,skf16(X0),X0)
| ~ in(skc20,X0,skc23) ) ).
cnf(u131,negated_conjecture,
see(skc8,skf8(X1)) ).
cnf(u135,negated_conjecture,
nonreflexive(skc8,skf8(X1)) ).
cnf(u139,negated_conjecture,
past(skc8,skf8(X1)) ).
cnf(u143,negated_conjecture,
~ event(skc8,skf8(X1)) ).
cnf(u147,negated_conjecture,
~ event(skc8,skf9(X1)) ).
cnf(u151,negated_conjecture,
past(skc8,skf9(X1)) ).
cnf(u155,negated_conjecture,
nonreflexive(skc8,skf9(X1)) ).
cnf(u159,negated_conjecture,
drink(skc8,skf9(X1)) ).
cnf(u163,negated_conjecture,
~ human_person(skc8,skf10(X1)) ).
cnf(u167,negated_conjecture,
see(skc20,skf16(X1)) ).
cnf(u171,negated_conjecture,
nonreflexive(skc20,skf16(X1)) ).
cnf(u175,negated_conjecture,
past(skc20,skf16(X1)) ).
cnf(u184,negated_conjecture,
agent(skc20,skc21,skc22) ).
cnf(u189,negated_conjecture,
~ patient(skc20,skc21,skc25) ).
cnf(u194,negated_conjecture,
~ restaurant(skc8,skc10) ).
cnf(u199,negated_conjecture,
~ coffee(skc8,skc9) ).
cnf(u204,negated_conjecture,
~ restaurant(skc20,skc23) ).
cnf(u209,negated_conjecture,
~ human_person(skc20,skc22) ).
cnf(u213,negated_conjecture,
coffee(skc20,skc25) ).
cnf(u219,negated_conjecture,
drink(skc20,skc21) ).
cnf(u224,negated_conjecture,
nonreflexive(skc20,skc21) ).
cnf(u229,negated_conjecture,
past(skc20,skc21) ).
cnf(u234,negated_conjecture,
~ event(skc20,skc21) ).
cnf(u245,negated_conjecture,
actual_world(skc20) ).
cnf(u249,negated_conjecture,
coffee(skc20,X0) ).
cnf(u256,negated_conjecture,
( ~ in(skc20,skf20(skc20,X0,X1),skc23)
| agent(skc20,skf16(skf20(skc20,X0,X1)),skf20(skc20,X0,X1)) ) ).
cnf(u266,negated_conjecture,
in(skc20,skf20(skc20,skc23,X0),skc23) ).
cnf(u273,negated_conjecture,
actual_world(skc8) ).
cnf(u277,negated_conjecture,
in(skc8,skf20(skc8,skc10,X0),skc10) ).
cnf(u285,negated_conjecture,
( human_person(skc20,X1)
| ~ see(skc20,X3)
| ~ nonreflexive(skc20,X3)
| ~ past(skc20,X3)
| ~ agent(skc20,X3,skf20(skc20,skc23,X0))
| event(skc20,X3)
| event(skc20,X2)
| patient(skc20,X3,X1)
| ~ agent(skc20,X2,X1)
| coffee(skc20,X0)
| patient(skc20,X2,X0)
| ~ past(skc20,X2)
| ~ nonreflexive(skc20,X2)
| ~ drink(skc20,X2) ) ).
cnf(u323,negated_conjecture,
( ~ in(skc8,skf20(skc8,X0,X1),skc10)
| agent(skc8,skf8(skf20(skc8,X0,X1)),skf20(skc8,X0,X1)) ) ).
cnf(u334,negated_conjecture,
~ customer(skc8,skf12(skc8,X0,X1)) ).
cnf(u349,negated_conjecture,
in(skc8,skf12(skc8,skc10,X0),skc10) ).
cnf(u361,negated_conjecture,
nonreflexive(skc8,skf8(skf20(skc8,skc10,skc9))) ).
cnf(u365,negated_conjecture,
see(skc8,skf8(skf20(skc8,skc10,skc9))) ).
cnf(u369,negated_conjecture,
~ event(skc8,skf8(skf20(skc8,skc10,skc9))) ).
cnf(u373,negated_conjecture,
past(skc8,skf8(skf20(skc8,skc10,skc9))) ).
cnf(u391,negated_conjecture,
( human_person(skc8,X1)
| ~ past(skc8,X2)
| ~ nonreflexive(skc8,X2)
| ~ drink(skc8,X2)
| patient(skc8,X2,X3)
| coffee(skc8,X3)
| event(skc8,X0)
| event(skc8,X2)
| ~ agent(skc8,X2,X1)
| ~ see(skc8,X0)
| ~ nonreflexive(skc8,X0)
| ~ past(skc8,X0)
| patient(skc8,X0,X1)
| ~ agent(skc8,X0,skf12(skc8,skc10,X1)) ) ).
cnf(u397,negated_conjecture,
drink(skc8,skf9(skf20(skc8,skc10,skc9))) ).
cnf(u401,negated_conjecture,
past(skc8,skf9(skf20(skc8,skc10,skc9))) ).
cnf(u405,negated_conjecture,
nonreflexive(skc8,skf9(skf20(skc8,skc10,skc9))) ).
cnf(u416,negated_conjecture,
( event(skc8,skf9(X0))
| ~ nonreflexive(skc8,skf9(X0))
| ~ past(skc8,skf9(X0))
| event(skc8,X1)
| ~ drink(skc8,skf9(X0))
| ~ agent(skc8,skf9(X0),skf10(X2))
| ~ see(skc8,X1)
| ~ nonreflexive(skc8,X1)
| ~ past(skc8,X1)
| patient(skc8,X1,skf10(X2))
| ~ agent(skc8,X1,skf12(skc8,skc10,skf10(X2))) ) ).
cnf(u281,negated_conjecture,
agent(skc20,skf16(skf20(skc20,skc23,X0)),skf20(skc20,skc23,X0)) ).
cnf(u422,negated_conjecture,
( ~ agent(skc8,skf8(X1),skf12(skc8,skc10,skf10(X0)))
| ~ drink(skc8,skf9(X0))
| ~ nonreflexive(skc8,skf9(X0))
| ~ see(skc8,skf8(X1))
| ~ nonreflexive(skc8,skf8(X1))
| ~ past(skc8,skf8(X1))
| patient(skc8,skf8(X1),skf10(X0))
| ~ past(skc8,skf9(X0)) ) ).
cnf(u414,negated_conjecture,
( coffee(skc8,X1)
| ~ nonreflexive(skc8,X0)
| ~ drink(skc8,X0)
| patient(skc8,X0,X1)
| ~ past(skc8,X0)
| event(skc8,X2)
| event(skc8,X0)
| ~ agent(skc8,X0,skf10(X3))
| ~ see(skc8,X2)
| ~ nonreflexive(skc8,X2)
| ~ past(skc8,X2)
| patient(skc8,X2,skf10(X3))
| ~ agent(skc8,X2,skf12(skc8,skc10,skf10(X3))) ) ).
cnf(u421,negated_conjecture,
( patient(skc8,skf8(skf12(skc8,skc10,skf10(X0))),skf10(X0))
| ~ drink(skc8,skf9(X1))
| ~ nonreflexive(skc8,skf9(X1))
| ~ see(skc8,skf8(skf12(skc8,skc10,skf10(X0))))
| ~ nonreflexive(skc8,skf8(skf12(skc8,skc10,skf10(X0))))
| ~ past(skc8,skf8(skf12(skc8,skc10,skf10(X0))))
| ~ agent(skc8,skf9(X1),skf10(X0))
| ~ past(skc8,skf9(X1)) ) ).
cnf(u419,negated_conjecture,
( ~ agent(skc8,skf9(X2),skf12(skc8,skc10,skf10(X1)))
| ~ agent(skc8,skf9(X0),skf10(X1))
| ~ drink(skc8,skf9(X0))
| ~ nonreflexive(skc8,skf9(X0))
| ~ see(skc8,skf9(X2))
| ~ nonreflexive(skc8,skf9(X2))
| ~ past(skc8,skf9(X2))
| patient(skc8,skf9(X2),skf10(X1))
| ~ past(skc8,skf9(X0)) ) ).
cnf(u417,negated_conjecture,
( event(skc8,X1)
| ~ past(skc8,skf9(X0))
| ~ nonreflexive(skc8,skf9(X0))
| ~ drink(skc8,skf9(X0))
| ~ agent(skc8,skf9(X0),skf10(X2))
| ~ see(skc8,X1)
| ~ nonreflexive(skc8,X1)
| ~ past(skc8,X1)
| patient(skc8,X1,skf10(X2))
| ~ agent(skc8,X1,skf12(skc8,skc10,skf10(X2))) ) ).
cnf(clause2,negated_conjecture,
actual_world(skc8) ).
cnf(u415,negated_conjecture,
( patient(skc8,X0,skc9)
| ~ drink(skc8,X0)
| ~ nonreflexive(skc8,X0)
| ~ past(skc8,X0)
| event(skc8,X1)
| event(skc8,X0)
| ~ agent(skc8,X0,skf10(X2))
| ~ see(skc8,X1)
| ~ nonreflexive(skc8,X1)
| ~ past(skc8,X1)
| patient(skc8,X1,skf10(X2))
| ~ agent(skc8,X1,skf12(skc8,skc10,skf10(X2))) ) ).
cnf(u352,negated_conjecture,
agent(skc8,skf8(skf12(skc8,skc10,X0)),skf12(skc8,skc10,X0)) ).
cnf(u418,negated_conjecture,
( ~ agent(skc8,skf8(X2),skf12(skc8,skc10,skf10(X1)))
| ~ agent(skc8,skf9(X0),skf10(X1))
| ~ drink(skc8,skf9(X0))
| ~ nonreflexive(skc8,skf9(X0))
| ~ see(skc8,skf8(X2))
| ~ nonreflexive(skc8,skf8(X2))
| ~ past(skc8,skf8(X2))
| patient(skc8,skf8(X2),skf10(X1))
| ~ past(skc8,skf9(X0)) ) ).
cnf(u351,negated_conjecture,
( ~ in(skc8,skf12(skc8,X0,X1),skc10)
| agent(skc8,skf8(skf12(skc8,X0,X1)),skf12(skc8,X0,X1)) ) ).
cnf(u326,negated_conjecture,
agent(skc8,skf8(skf20(skc8,skc10,X0)),skf20(skc8,skc10,X0)) ).
cnf(u420,negated_conjecture,
( ~ agent(skc8,skf9(X1),skf12(skc8,skc10,skf10(X0)))
| ~ drink(skc8,skf9(X0))
| ~ nonreflexive(skc8,skf9(X0))
| ~ see(skc8,skf9(X1))
| ~ nonreflexive(skc8,skf9(X1))
| ~ past(skc8,skf9(X1))
| patient(skc8,skf9(X1),skf10(X0))
| ~ past(skc8,skf9(X0)) ) ).
cnf(clause1,negated_conjecture,
actual_world(skc20) ).
cnf(u423,negated_conjecture,
( patient(skc8,skf8(skf12(skc8,skc10,skf10(X0))),skf10(X0))
| ~ nonreflexive(skc8,skf9(X0))
| ~ see(skc8,skf8(skf12(skc8,skc10,skf10(X0))))
| ~ nonreflexive(skc8,skf8(skf12(skc8,skc10,skf10(X0))))
| ~ past(skc8,skf8(skf12(skc8,skc10,skf10(X0))))
| ~ drink(skc8,skf9(X0))
| ~ past(skc8,skf9(X0)) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP103-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.38 % Computer : n005.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 18:04:32 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.45 % (71923)Will run a generic schedule for satisfiability detection.
% 0.10/0.45 % (71934)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1918803999:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.10/0.45 % (71929)% WARNING: option uhcvi not known.
% 0.10/0.45 % (71934) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-71923-71934"...
% 0.10/0.45 % (71934)...printing done.
% 0.10/0.45 % SZS status Satisfiable for theBenchmark
% 0.10/0.45 % SZS output start Saturation.
% See solution above
% 0.10/0.45 % SZS output start Definitions and Model Updates.
% 0.10/0.45 globally flip the polarity of every occurrence of predicate "customer"
% 0.10/0.45 globally flip the polarity of every occurrence of predicate "patient"
% 0.10/0.45 globally flip the polarity of every occurrence of predicate "restaurant"
% 0.10/0.45 globally flip the polarity of every occurrence of predicate "human_person"
% 0.10/0.45 globally flip the polarity of every occurrence of predicate "coffee"
% 0.10/0.45 globally flip the polarity of every occurrence of predicate "event"
% 0.10/0.45 % SZS output end Definitions and Model Updates.
% 0.10/0.45 % (71934)------------------------------
% 0.10/0.45 % (71934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.10/0.45 % (71934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.10/0.45 % (71934)CaDiCaL version: 2.1.3
% 0.10/0.45 % (71934)Termination reason: Satisfiable
% 0.10/0.45 % (71934)Time elapsed: 0.005 s
% 0.10/0.45 % (71934)Peak memory usage: 11 MB
% 0.10/0.45 % (71934)Instructions burned: 10 (million)
% 0.10/0.45 % (71923)Success in time 0.036 s
% 0.10/0.45 % Vampire exiting
%------------------------------------------------------------------------------