%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP005+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:06:53 PM UTC 2026
% Result : CounterSatisfiable 4.45s 1.39s
% Output : Saturation 4.45s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u87,negated_conjecture,
sP0 ).
cnf(u90,negated_conjecture,
~ sP1 ).
cnf(u98,negated_conjecture,
( ~ in(X18,X10)
| ~ seat(X10)
| X17 = X18
| ~ in(X17,X10)
| ~ young(X18)
| ~ man(X18)
| ~ fellow(X18)
| ~ young(X17)
| ~ man(X17)
| ~ fellow(X17)
| ~ front(X10)
| ~ furniture(X10) ) ).
cnf(u108,axiom,
in(sK20,sK12) ).
cnf(u113,axiom,
sK18 = sK20 ).
cnf(u118,axiom,
in(sK19,sK11) ).
cnf(u123,axiom,
sK17 = sK19 ).
cnf(u128,axiom,
young(sK18) ).
cnf(u133,axiom,
man(sK18) ).
cnf(u138,axiom,
fellow(sK18) ).
cnf(u143,axiom,
young(sK17) ).
cnf(u148,axiom,
man(sK17) ).
cnf(u153,axiom,
fellow(sK17) ).
cnf(u158,axiom,
sK17 != sK18 ).
cnf(u163,axiom,
in(sK14,sK13) ).
cnf(u168,axiom,
down(sK14,sK15) ).
cnf(u173,axiom,
barrel(sK14,sK16) ).
cnf(u178,axiom,
old(sK16) ).
cnf(u183,axiom,
dirty(sK16) ).
cnf(u188,axiom,
white(sK16) ).
cnf(u193,axiom,
car(sK16) ).
cnf(u198,axiom,
chevy(sK16) ).
cnf(u203,axiom,
lonely(sK15) ).
cnf(u208,axiom,
way(sK15) ).
cnf(u213,axiom,
street(sK15) ).
cnf(u218,axiom,
event(sK14) ).
cnf(u223,axiom,
city(sK13) ).
cnf(u228,axiom,
hollywood(sK13) ).
cnf(u233,axiom,
front(sK12) ).
cnf(u238,axiom,
furniture(sK12) ).
cnf(u243,axiom,
seat(sK12) ).
cnf(u248,axiom,
front(sK11) ).
cnf(u253,axiom,
furniture(sK11) ).
cnf(u258,axiom,
seat(sK11) ).
cnf(u262,axiom,
~ in(sK10,sK2) ).
cnf(u268,axiom,
sK8 = sK10 ).
cnf(u273,axiom,
in(sK9,sK2) ).
cnf(u278,axiom,
sK7 = sK9 ).
cnf(u283,axiom,
young(sK8) ).
cnf(u288,axiom,
man(sK8) ).
cnf(u293,axiom,
fellow(sK8) ).
cnf(u298,axiom,
young(sK7) ).
cnf(u303,axiom,
man(sK7) ).
cnf(u308,axiom,
fellow(sK7) ).
cnf(u313,axiom,
sK7 != sK8 ).
cnf(u318,axiom,
in(sK4,sK3) ).
cnf(u323,axiom,
down(sK4,sK6) ).
cnf(u328,axiom,
barrel(sK4,sK5) ).
cnf(u333,axiom,
lonely(sK6) ).
cnf(u338,axiom,
way(sK6) ).
cnf(u343,axiom,
street(sK6) ).
cnf(u348,axiom,
old(sK5) ).
cnf(u353,axiom,
dirty(sK5) ).
cnf(u358,axiom,
white(sK5) ).
cnf(u363,axiom,
car(sK5) ).
cnf(u368,axiom,
chevy(sK5) ).
cnf(u373,axiom,
event(sK4) ).
cnf(u378,axiom,
city(sK3) ).
cnf(u383,axiom,
hollywood(sK3) ).
cnf(u388,axiom,
front(sK2) ).
cnf(u393,axiom,
furniture(sK2) ).
cnf(u398,axiom,
seat(sK2) ).
cnf(u420,negated_conjecture,
~ hollywood(sK2) ).
cnf(u461,negated_conjecture,
~ furniture(sK3) ).
cnf(u645,negated_conjecture,
~ furniture(sK13) ).
cnf(u640,axiom,
in(sK17,sK11) ).
cnf(u591,negated_conjecture,
( ~ in(X0,sK2)
| sK7 = X0
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0) ) ).
cnf(u604,negated_conjecture,
( ~ in(X0,sK12)
| sK18 = X0
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0) ) ).
cnf(u625,axiom,
~ in(sK8,sK2) ).
cnf(u638,negated_conjecture,
( ~ in(X0,sK11)
| sK17 = X0
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0) ) ).
cnf(u401,axiom,
in(sK7,sK2) ).
cnf(u606,axiom,
in(sK18,sK12) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP005+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n026.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 17:49:27 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.45/1.39 % (3102683)Detected formulas, will run a generic FOF schedule.
% 4.45/1.39 % (3102693)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2012534416:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.45/1.39 % (3102693)Refutation not found, incomplete strategy
% 4.45/1.39 % (3102693)------------------------------
% 4.45/1.39 % (3102693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.39 % (3102693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.45/1.39 % (3102693)CaDiCaL version: 2.1.3
% 4.45/1.39 % (3102693)Termination reason: Refutation not found, incomplete strategy
% 4.45/1.39 % (3102693)Time elapsed: 0.005 s
% 4.45/1.39 % (3102693)Peak memory usage: 89 MB
% 4.45/1.39 % (3102693)Instructions burned: 12 (million)
% 4.45/1.39 % (3102694)dis-21_1_sil=8000:lcm=predicate:random_seed=2464183020:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.45/1.39 % (3102691)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=845018656:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.45/1.39 % (3102692)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3218905930:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.45/1.39 % (3102688)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=930251409:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.45/1.39 % (3102689)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=674042595:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.45/1.39 % (3102690)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3097867761:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.45/1.39 % (3102694)Refutation not found, incomplete strategy
% 4.45/1.39 % (3102694)------------------------------
% 4.45/1.39 % (3102694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.39 % (3102694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.45/1.39 % (3102694)CaDiCaL version: 2.1.3
% 4.45/1.39 % (3102694)Termination reason: Refutation not found, incomplete strategy
% 4.45/1.39 % (3102694)Time elapsed: 0.004 s
% 4.45/1.39 % (3102694)Peak memory usage: 88 MB
% 4.45/1.39 % (3102694)Instructions burned: 4 (million)
% 4.45/1.39 % (3102691)Refutation not found, incomplete strategy
% 4.45/1.39 % (3102691)------------------------------
% 4.45/1.39 % (3102691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.39 % (3102691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.45/1.39 % (3102691)CaDiCaL version: 2.1.3
% 4.45/1.39 % (3102691)Termination reason: Refutation not found, incomplete strategy
% 4.45/1.39 % (3102691)Time elapsed: 0.006 s
% 4.45/1.39 % (3102691)Peak memory usage: 88 MB
% 4.45/1.39 % (3102691)Instructions burned: 9 (million)
% 4.45/1.39 % (3102692)Instruction limit reached!
% 4.45/1.39 % (3102692)------------------------------
% 4.45/1.39 % (3102692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.39 % (3102692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.45/1.39 % (3102692)CaDiCaL version: 2.1.3
% 4.45/1.39 % (3102692)Termination reason: Instruction limit
% 4.45/1.39 % (3102692)Termination phase: Saturation
% 4.45/1.39 % (3102692)Time elapsed: 0.044 s
% 4.45/1.39 % (3102692)Peak memory usage: 88 MB
% 4.45/1.39 % (3102692)Instructions burned: 122 (million)
% 4.45/1.39 % (3102693)------------------------------
% 4.45/1.39 % (3102693)------------------------------
% 4.45/1.39 % (3102702)lrs+10_1_sil=8000:sp=occurrence:random_seed=1407840981:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 4.45/1.39 % (3102702)First to succeed.
% 4.45/1.39 % (3102702)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3102683"
% 4.45/1.39 % (3102694)------------------------------
% 4.45/1.39 % (3102694)------------------------------
% 4.45/1.39 % (3102691)------------------------------
% 4.45/1.39 % (3102691)------------------------------
% 4.45/1.39 % (3102703)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2382063810:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.45/1.39 % (3102703)Refutation not found, incomplete strategy
% 4.45/1.39 % (3102703)------------------------------
% 4.45/1.39 % (3102703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.39 % (3102703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.45/1.39 % (3102703)CaDiCaL version: 2.1.3
% 4.45/1.39 % (3102703)Termination reason: Refutation not found, incomplete strategy
% 4.45/1.39 % (3102703)Time elapsed: 0.004 s
% 4.45/1.39 % (3102703)Peak memory usage: 89 MB
% 4.45/1.39 % (3102703)Instructions burned: 12 (million)
% 4.45/1.39 % (3102706)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1527142773:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 4.45/1.39 % (3102707)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2346609526:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 4.45/1.39 % (3102706)Refutation not found, incomplete strategy
% 4.45/1.39 % (3102706)------------------------------
% 4.45/1.39 % (3102706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.39 % (3102706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.45/1.39 % (3102706)CaDiCaL version: 2.1.3
% 4.45/1.39 % (3102706)Termination reason: Refutation not found, incomplete strategy
% 4.45/1.39 % (3102706)Time elapsed: 0.007 s
% 4.45/1.39 % (3102706)Peak memory usage: 89 MB
% 4.45/1.39 % (3102706)Instructions burned: 9 (million)
% 4.45/1.39 % (3102707)Refutation not found, incomplete strategy
% 4.45/1.39 % (3102707)------------------------------
% 4.45/1.39 % (3102707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.39 % (3102707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.45/1.39 % (3102707)CaDiCaL version: 2.1.3
% 4.45/1.39 % (3102707)Termination reason: Refutation not found, incomplete strategy
% 4.45/1.39 % (3102707)Time elapsed: 0.015 s
% 4.45/1.39 % (3102707)Peak memory usage: 89 MB
% 4.45/1.39 % (3102707)Instructions burned: 27 (million)
% 4.45/1.39 % (3102703)------------------------------
% 4.45/1.39 % (3102703)------------------------------
% 4.45/1.39 % SZS status CounterSatisfiable for theBenchmark
% 4.45/1.39 % SZS output start Saturation.
% See solution above
% 4.45/1.39 % SZS output start Definitions and Model Updates.
% 4.45/1.39 % SZS output end Definitions and Model Updates.
% 4.45/1.39 % (3102702)------------------------------
% 4.45/1.39 % (3102702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.45/1.39 % (3102702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.45/1.39 % (3102702)CaDiCaL version: 2.1.3
% 4.45/1.39 % (3102702)Termination reason: Satisfiable
% 4.45/1.39 % (3102702)Time elapsed: 0.008 s
% 4.45/1.39 % (3102702)Peak memory usage: 89 MB
% 4.45/1.39 % (3102702)Instructions burned: 10 (million)
% 4.45/1.39 % (3102702)------------------------------
% 4.45/1.39 % (3102702)------------------------------
% 4.45/1.39 % (3102683)Success in time 0.578 s
% 4.45/1.39 % Vampire exiting
%------------------------------------------------------------------------------