%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NLP012+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 : n010.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:25 PM UTC 2026
% Result : CounterSatisfiable 0.12s 0.46s
% Output : Saturation 0.12s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u79,negated_conjecture,
sP0 ).
cnf(u82,negated_conjecture,
~ sP1 ).
cnf(u87,negated_conjecture,
( ~ young(X15)
| ~ in(X18,X16)
| X15 != X18
| X14 = X15
| ~ in(X17,X16)
| X14 != X17
| ~ seat(X16)
| ~ man(X15)
| ~ fellow(X15)
| ~ young(X14)
| ~ man(X14)
| ~ fellow(X14)
| ~ front(X16)
| ~ furniture(X16) ) ).
cnf(u100,axiom,
in(sK20,sK11) ).
cnf(u105,axiom,
sK17 = sK20 ).
cnf(u110,axiom,
in(sK19,sK18) ).
cnf(u115,axiom,
sK16 = sK19 ).
cnf(u120,axiom,
young(sK17) ).
cnf(u125,axiom,
man(sK17) ).
cnf(u130,axiom,
fellow(sK17) ).
cnf(u135,axiom,
young(sK16) ).
cnf(u140,axiom,
man(sK16) ).
cnf(u145,axiom,
fellow(sK16) ).
cnf(u150,axiom,
sK16 != sK17 ).
cnf(u155,axiom,
front(sK18) ).
cnf(u160,axiom,
furniture(sK18) ).
cnf(u165,axiom,
seat(sK18) ).
cnf(u170,axiom,
in(sK13,sK12) ).
cnf(u175,axiom,
down(sK13,sK14) ).
cnf(u180,axiom,
barrel(sK13,sK15) ).
cnf(u185,axiom,
old(sK15) ).
cnf(u190,axiom,
dirty(sK15) ).
cnf(u195,axiom,
white(sK15) ).
cnf(u200,axiom,
car(sK15) ).
cnf(u205,axiom,
chevy(sK15) ).
cnf(u210,axiom,
lonely(sK14) ).
cnf(u215,axiom,
way(sK14) ).
cnf(u220,axiom,
street(sK14) ).
cnf(u225,axiom,
event(sK13) ).
cnf(u230,axiom,
city(sK12) ).
cnf(u235,axiom,
hollywood(sK12) ).
cnf(u240,axiom,
front(sK11) ).
cnf(u245,axiom,
furniture(sK11) ).
cnf(u250,axiom,
seat(sK11) ).
cnf(u255,axiom,
in(sK10,sK8) ).
cnf(u260,axiom,
sK7 = sK10 ).
cnf(u265,axiom,
in(sK9,sK8) ).
cnf(u270,axiom,
sK6 = sK9 ).
cnf(u275,axiom,
young(sK7) ).
cnf(u280,axiom,
man(sK7) ).
cnf(u284,axiom,
~ fellow(sK7) ).
cnf(u290,axiom,
young(sK6) ).
cnf(u295,axiom,
man(sK6) ).
cnf(u300,axiom,
fellow(sK6) ).
cnf(u305,axiom,
sK6 != sK7 ).
cnf(u310,axiom,
front(sK8) ).
cnf(u315,axiom,
furniture(sK8) ).
cnf(u320,axiom,
seat(sK8) ).
cnf(u325,axiom,
in(sK3,sK2) ).
cnf(u330,axiom,
down(sK3,sK5) ).
cnf(u335,axiom,
barrel(sK3,sK4) ).
cnf(u340,axiom,
lonely(sK5) ).
cnf(u345,axiom,
way(sK5) ).
cnf(u350,axiom,
street(sK5) ).
cnf(u355,axiom,
old(sK4) ).
cnf(u360,axiom,
dirty(sK4) ).
cnf(u365,axiom,
white(sK4) ).
cnf(u370,axiom,
car(sK4) ).
cnf(u375,axiom,
chevy(sK4) ).
cnf(u380,axiom,
event(sK3) ).
cnf(u385,axiom,
city(sK2) ).
cnf(u390,axiom,
hollywood(sK2) ).
cnf(u471,negated_conjecture,
sK7 != sK17 ).
cnf(u479,negated_conjecture,
sK7 != sK16 ).
cnf(u514,negated_conjecture,
( ~ front(X2)
| ~ furniture(X2)
| sK17 != X0
| ~ in(X0,X2)
| ~ in(X1,X2)
| ~ seat(X2)
| sK7 != X1 ) ).
cnf(u518,negated_conjecture,
sK6 != sK17 ).
cnf(u522,negated_conjecture,
( ~ front(X2)
| ~ furniture(X2)
| sK17 != X0
| ~ in(X0,X2)
| ~ in(X1,X2)
| ~ seat(X2)
| sK6 != X1 ) ).
cnf(u534,negated_conjecture,
( ~ front(X2)
| ~ furniture(X2)
| sK16 != X0
| ~ in(X0,X2)
| ~ in(X1,X2)
| ~ seat(X2)
| sK7 != X1 ) ).
cnf(u538,negated_conjecture,
sK6 != sK16 ).
cnf(u542,negated_conjecture,
( ~ front(X2)
| ~ furniture(X2)
| sK16 != X0
| ~ in(X0,X2)
| ~ in(X1,X2)
| ~ seat(X2)
| sK6 != X1 ) ).
cnf(u595,negated_conjecture,
( ~ in(X0,sK11)
| sK16 != X0 ) ).
cnf(u598,negated_conjecture,
( ~ in(X1,sK11)
| sK7 != X1 ) ).
cnf(u605,negated_conjecture,
( ~ in(X1,sK18)
| sK7 != X1 ) ).
cnf(u609,negated_conjecture,
( ~ in(X0,sK8)
| sK16 != X0 ) ).
cnf(u620,negated_conjecture,
( ~ in(X1,sK18)
| sK17 != X1 ) ).
cnf(u624,negated_conjecture,
( ~ in(X1,sK8)
| sK17 != X1 ) ).
cnf(u648,negated_conjecture,
( ~ in(X1,sK18)
| sK6 != X1 ) ).
cnf(u679,negated_conjecture,
( ~ in(X0,sK11)
| sK6 != X0 ) ).
cnf(u487,axiom,
in(sK17,sK11) ).
cnf(u500,negated_conjecture,
( ~ young(X2)
| sK6 != X0
| sK6 = X2
| ~ in(X3,X1)
| X2 != X3
| ~ seat(X1)
| ~ in(X0,X1)
| ~ man(X2)
| ~ fellow(X2)
| ~ front(X1)
| ~ furniture(X1) ) ).
cnf(u497,negated_conjecture,
( ~ young(X2)
| sK17 != X0
| sK17 = X2
| ~ in(X3,X1)
| X2 != X3
| ~ seat(X1)
| ~ in(X0,X1)
| ~ man(X2)
| ~ fellow(X2)
| ~ front(X1)
| ~ furniture(X1) ) ).
cnf(u392,axiom,
in(sK7,sK8) ).
cnf(u393,axiom,
in(sK6,sK8) ).
cnf(u488,axiom,
in(sK16,sK18) ).
cnf(u498,negated_conjecture,
( ~ young(X2)
| sK16 != X0
| sK16 = X2
| ~ in(X3,X1)
| X2 != X3
| ~ seat(X1)
| ~ in(X0,X1)
| ~ man(X2)
| ~ fellow(X2)
| ~ front(X1)
| ~ furniture(X1) ) ).
cnf(u511,negated_conjecture,
( ~ front(X2)
| ~ in(X1,X2)
| sK16 != X1
| ~ seat(X2)
| ~ in(X0,X2)
| sK17 != X0
| ~ furniture(X2) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP012+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n010.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 17:47:47 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 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.12/0.46 % (1200166)Will run a generic schedule for satisfiability detection.
% 0.12/0.46 % (1200177)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1822031743:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.12/0.46 % (1200173)% WARNING: option uhcvi not known.
% 0.12/0.46 % (1200176)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2018852884:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.12/0.46 % (1200173)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1132030656:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.12/0.46 % (1200177) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1200166-1200177"...
% 0.12/0.46 % (1200177)...printing done.
% 0.12/0.46 % (1200175)dis+10_1_sil=32000:sp=arity:random_seed=1378487315:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.12/0.46 % SZS status CounterSatisfiable for theBenchmark
% 0.12/0.46 % SZS output start Saturation.
% See solution above
% 0.12/0.46 % SZS output start Definitions and Model Updates.
% 0.12/0.46 % SZS output end Definitions and Model Updates.
% 0.12/0.46 % (1200177)------------------------------
% 0.12/0.46 % (1200177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.12/0.46 % (1200177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.12/0.46 % (1200177)CaDiCaL version: 2.1.3
% 0.12/0.46 % (1200177)Termination reason: Satisfiable
% 0.12/0.46 % (1200177)Time elapsed: 0.010 s
% 0.12/0.46 % (1200177)Peak memory usage: 12 MB
% 0.12/0.46 % (1200177)Instructions burned: 20 (million)
% 0.12/0.46 % (1200166)Success in time 0.037 s
% 0.12/0.46 % Vampire exiting
%------------------------------------------------------------------------------