%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NLP101+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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:51 PM UTC 2026
% Result : CounterSatisfiable 0.04s 0.47s
% Output : Saturation 0.04s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u72,negated_conjecture,
sP3 ).
cnf(u94,axiom,
sP2(sK6) ).
cnf(u99,axiom,
actual_world(sK6) ).
cnf(u103,axiom,
( ~ actual_world(X0)
| in(X0,sK4(X0),sK5(X0)) ) ).
cnf(u107,axiom,
( ~ actual_world(X0)
| restaurant(X0,sK5(X0)) ) ).
cnf(u111,axiom,
( ~ actual_world(X0)
| customer(X0,sK4(X0)) ) ).
cnf(u115,axiom,
( ~ actual_world(X0)
| ~ see(X0,X6)
| ~ nonreflexive(X0,X6)
| ~ past(X0,X6)
| ~ patient(X0,X6,X3)
| ~ agent(X0,X6,sK4(X0))
| ~ event(X0,X6)
| ~ drink(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ past(X0,X5)
| ~ patient(X0,X5,X4)
| ~ agent(X0,X5,X3)
| ~ event(X0,X5)
| ~ coffee(X0,X4)
| ~ human_person(X0,X3) ) ).
cnf(u139,axiom,
~ in(sK6,sK4(sK6),sK8(sK6)) ).
cnf(u142,axiom,
( ~ sP1(sK6,X0,X1)
| ~ in(sK6,sK4(sK6),X1)
| past(sK6,sK11(sK6,X0,sK4(sK6))) ) ).
cnf(u40,axiom,
( ~ sP2(X0)
| coffee(X0,sK7(X0)) ) ).
cnf(u42,axiom,
( ~ customer(X0,X3)
| nonreflexive(X0,sK11(X0,X1,X3))
| ~ in(X0,X3,X2)
| ~ sP1(X0,X1,X2) ) ).
cnf(u128,axiom,
agent(sK6,sK10(sK6),sK9(sK6)) ).
cnf(u52,axiom,
( ~ sP0(X0,X1)
| event(X0,sK15(X0,X1)) ) ).
cnf(u34,axiom,
( ~ sP2(X0)
| past(X0,sK10(X0)) ) ).
cnf(u44,axiom,
( ~ customer(X0,X3)
| patient(X0,sK11(X0,X1,X3),X1)
| ~ in(X0,X3,X2)
| ~ sP1(X0,X1,X2) ) ).
cnf(u127,axiom,
patient(sK6,sK10(sK6),sK7(sK6)) ).
cnf(u46,axiom,
( ~ customer(X0,X3)
| event(X0,sK11(X0,X1,X3))
| ~ in(X0,X3,X2)
| ~ sP1(X0,X1,X2) ) ).
cnf(u121,axiom,
human_person(sK6,sK9(sK6)) ).
cnf(u123,axiom,
coffee(sK6,sK7(sK6)) ).
cnf(u32,axiom,
( ~ sP2(X0)
| drink(X0,sK10(X0)) ) ).
cnf(u125,axiom,
customer(sK6,sK4(sK6)) ).
cnf(u117,axiom,
drink(sK6,sK10(sK6)) ).
cnf(u36,axiom,
( ~ sP2(X0)
| agent(X0,sK10(X0),sK9(X0)) ) ).
cnf(u119,axiom,
past(sK6,sK10(sK6)) ).
cnf(u58,axiom,
( ~ sP0(X0,X1)
| event(X0,sK14(X0,X1)) ) ).
cnf(u59,axiom,
( ~ sP0(X0,X1)
| coffee(X0,sK13(X0,X1)) ) ).
cnf(u141,axiom,
( ~ sP1(sK6,X0,X1)
| ~ in(sK6,sK4(sK6),X1)
| nonreflexive(sK6,sK11(sK6,X0,sK4(sK6))) ) ).
cnf(u51,axiom,
( ~ sP0(X0,X1)
| agent(X0,sK15(X0,X1),X1) ) ).
cnf(u129,axiom,
in(sK6,sK4(sK6),sK5(sK6)) ).
cnf(u148,axiom,
( ~ sP1(sK6,X0,X1)
| ~ in(sK6,sK4(sK6),X1)
| agent(sK6,sK11(sK6,X0,sK4(sK6)),sK4(sK6)) ) ).
cnf(u55,axiom,
( ~ sP0(X0,X1)
| past(X0,sK14(X0,X1)) ) ).
cnf(u49,axiom,
( ~ sP0(X0,X1)
| past(X0,sK15(X0,X1)) ) ).
cnf(u47,axiom,
( ~ sP0(X0,X1)
| see(X0,sK15(X0,X1)) ) ).
cnf(u41,axiom,
( ~ customer(X0,X3)
| see(X0,sK11(X0,X1,X3))
| ~ in(X0,X3,X2)
| ~ sP1(X0,X1,X2) ) ).
cnf(u120,axiom,
event(sK6,sK10(sK6)) ).
cnf(u43,axiom,
( ~ customer(X0,X3)
| past(X0,sK11(X0,X1,X3))
| ~ in(X0,X3,X2)
| ~ sP1(X0,X1,X2) ) ).
cnf(u122,axiom,
restaurant(sK6,sK8(sK6)) ).
cnf(u35,axiom,
( ~ sP2(X0)
| patient(X0,sK10(X0),sK7(X0)) ) ).
cnf(u45,axiom,
( ~ customer(X0,X3)
| agent(X0,sK11(X0,X1,X3),X3)
| ~ in(X0,X3,X2)
| ~ sP1(X0,X1,X2) ) ).
cnf(u53,axiom,
( ~ sP0(X0,X1)
| drink(X0,sK14(X0,X1)) ) ).
cnf(u124,axiom,
restaurant(sK6,sK5(sK6)) ).
cnf(u150,axiom,
( ~ see(sK6,X0)
| ~ nonreflexive(sK6,X0)
| ~ past(sK6,X0)
| ~ patient(sK6,X0,X1)
| ~ agent(sK6,X0,sK4(sK6))
| ~ event(sK6,X0)
| ~ drink(sK6,X2)
| ~ nonreflexive(sK6,X2)
| ~ past(sK6,X2)
| ~ patient(sK6,X2,X3)
| ~ agent(sK6,X2,X1)
| ~ event(sK6,X2)
| ~ coffee(sK6,X3)
| ~ human_person(sK6,X1) ) ).
cnf(u37,axiom,
( ~ sP2(X0)
| event(X0,sK10(X0)) ) ).
cnf(u126,axiom,
sP1(sK6,sK9(sK6),sK8(sK6)) ).
cnf(u39,axiom,
( ~ sP2(X0)
| restaurant(X0,sK8(X0)) ) ).
cnf(u118,axiom,
nonreflexive(sK6,sK10(sK6)) ).
cnf(u33,axiom,
( ~ sP2(X0)
| nonreflexive(X0,sK10(X0)) ) ).
cnf(u31,axiom,
( ~ sP2(X0)
| sP1(X0,sK9(X0),sK8(X0)) ) ).
cnf(u146,axiom,
( ~ sP1(sK6,X0,X1)
| ~ in(sK6,sK4(sK6),X1)
| patient(sK6,sK11(sK6,X0,sK4(sK6)),X0) ) ).
cnf(u56,axiom,
( ~ sP0(X0,X1)
| patient(X0,sK14(X0,X1),sK13(X0,X1)) ) ).
cnf(u38,axiom,
( ~ sP2(X0)
| human_person(X0,sK9(X0)) ) ).
cnf(u144,axiom,
( ~ sP1(sK6,X0,X1)
| ~ in(sK6,sK4(sK6),X1)
| event(sK6,sK11(sK6,X0,sK4(sK6))) ) ).
cnf(u50,axiom,
( ~ sP0(X0,X1)
| patient(X0,sK15(X0,X1),sK12(X0,X1)) ) ).
cnf(u60,axiom,
( ~ sP0(X0,X1)
| human_person(X0,sK12(X0,X1)) ) ).
cnf(u57,axiom,
( ~ sP0(X0,X1)
| agent(X0,sK14(X0,X1),sK12(X0,X1)) ) ).
cnf(u130,axiom,
( ~ sP1(sK6,X0,X1)
| ~ in(sK6,sK4(sK6),X1)
| see(sK6,sK11(sK6,X0,sK4(sK6))) ) ).
cnf(u54,axiom,
( ~ sP0(X0,X1)
| nonreflexive(X0,sK14(X0,X1)) ) ).
cnf(u48,axiom,
( ~ sP0(X0,X1)
| nonreflexive(X0,sK15(X0,X1)) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP101+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n009.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 18:04:30 UTC 2026
% 0.04/0.39 % CPUTime :
% 0.04/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.04/0.42 Running first-order model finding
% 0.04/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.04/0.47 % (2290070)Will run a generic schedule for satisfiability detection.
% 0.04/0.47 % (2290080)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1204899834:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.04/0.47 % (2290080) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2290070-2290080"...
% 0.04/0.47 % (2290080)...printing done.
% 0.04/0.47 % SZS status CounterSatisfiable for theBenchmark
% 0.04/0.47 % SZS output start Saturation.
% See solution above
% 0.04/0.47 % SZS output start Definitions and Model Updates.
% 0.04/0.47 % SZS output end Definitions and Model Updates.
% 0.04/0.47 % (2290080)------------------------------
% 0.04/0.47 % (2290080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.04/0.47 % (2290080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.04/0.47 % (2290080)CaDiCaL version: 2.1.3
% 0.04/0.47 % (2290080)Termination reason: Satisfiable
% 0.04/0.47 % (2290080)Time elapsed: 0.003 s
% 0.04/0.47 % (2290080)Peak memory usage: 11 MB
% 0.04/0.47 % (2290080)Instructions burned: 4 (million)
% 0.04/0.47 % (2290070)Success in time 0.028 s
% 0.04/0.47 % Vampire exiting
%------------------------------------------------------------------------------