%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR085+2 : TPTP v9.3.1. Bugfixed v7.3.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 09:45:04 AM UTC 2026
% Result : Theorem 8.90s 2.06s
% Output : Refutation 8.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 4
% Syntax : Number of formulae : 18 ( 12 unt; 0 def)
% Number of atoms : 29 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 25 ( 14 ~; 9 |; 0 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 5 ( 5 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f37982,axiom,
s__instance(s__Organism12_1,s__Object),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1) ).
fof(f37983,axiom,
s__attribute(s__Organism12_1,s__Living),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_2) ).
fof(f37984,axiom,
! [X0] :
( s__instance(X0,s__Object)
=> ( s__attribute(X0,s__Living)
=> s__instance(X0,s__Organism) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_3) ).
fof(f37985,conjecture,
s__instance(s__Organism12_1,s__Organism),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO_MILO) ).
fof(f37986,negated_conjecture,
~ s__instance(s__Organism12_1,s__Organism),
inference(negated_conjecture,[status(cth)],[f37985]) ).
fof(f37999,plain,
~ s__instance(s__Organism12_1,s__Organism),
inference(flattening,[],[f37986]) ).
fof(f48355,plain,
! [X0] :
( s__instance(X0,s__Organism)
| ~ s__attribute(X0,s__Living)
| ~ s__instance(X0,s__Object) ),
inference(ennf_transformation,[],[f37984]) ).
fof(f48356,plain,
! [X0] :
( s__instance(X0,s__Organism)
| ~ s__attribute(X0,s__Living)
| ~ s__instance(X0,s__Object) ),
inference(flattening,[],[f48355]) ).
fof(f89562,plain,
s__instance(s__Organism12_1,s__Object),
inference(cnf_transformation,[],[f37982]) ).
fof(f89563,plain,
s__attribute(s__Organism12_1,s__Living),
inference(cnf_transformation,[],[f37983]) ).
fof(f89564,plain,
! [X0] :
( ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Living)
| s__instance(X0,s__Organism) ),
inference(cnf_transformation,[],[f48356]) ).
fof(f89565,plain,
~ s__instance(s__Organism12_1,s__Organism),
inference(cnf_transformation,[],[f37999]) ).
fof(f111692,plain,
~ s__instance(s__Organism12_1,s__Object),
inference(consistent_polarity_flipping,[],[f89562]) ).
fof(f111693,plain,
! [X0] :
( ~ s__attribute(X0,s__Living)
| s__instance(X0,s__Object)
| ~ s__instance(X0,s__Organism) ),
inference(consistent_polarity_flipping,[],[f89564]) ).
fof(f111694,plain,
s__instance(s__Organism12_1,s__Organism),
inference(consistent_polarity_flipping,[],[f89565]) ).
fof(f167255,plain,
( s__instance(s__Organism12_1,s__Object)
| ~ s__instance(s__Organism12_1,s__Organism) ),
inference(resolution,[],[f111693,f89563]) ).
fof(f167256,plain,
~ s__instance(s__Organism12_1,s__Organism),
inference(forward_subsumption_resolution,[],[f167255,f111692]) ).
fof(f167257,plain,
$false,
inference(forward_subsumption_resolution,[],[f167256,f111694]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR085+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n005.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 22:34:17 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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
% 7.15/2.01 % (1258940)Will run a generic schedule for satisfiability detection.
% 7.15/2.01 % (1258946)% WARNING: option uhcvi not known.
% 7.15/2.01 % (1258946)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=689961351:i=135531:add=off:rawr=on_2993 on theBenchmark for (2993ds/135531Mi)
% 7.15/2.01 % (1258945)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2422666501_2993 on theBenchmark for (2993ds/0Mi)
% 7.15/2.01 % (1258947)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1170040965:i=88024:add=on:rawr=on_2993 on theBenchmark for (2993ds/88024Mi)
% 7.15/2.01 % (1258948)dis+10_1_sil=32000:sp=arity:random_seed=1519529578:i=103:fgj=on_2993 on theBenchmark for (2993ds/103Mi)
% 7.15/2.01 % (1258949)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3170689505:i=116_2993 on theBenchmark for (2993ds/116Mi)
% 7.15/2.01 % (1258950)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2972206322:i=131_2993 on theBenchmark for (2993ds/131Mi)
% 7.15/2.01 % (1258951)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3608924478:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2993 on theBenchmark for (2993ds/159Mi)
% 7.15/2.01 % (1258948)Instruction limit reached!
% 7.15/2.01 % (1258948)------------------------------
% 7.15/2.01 % (1258948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.15/2.01 % (1258948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.15/2.01 % (1258948)CaDiCaL version: 2.1.3
% 7.15/2.01 % (1258948)Termination reason: Instruction limit
% 7.15/2.01 % (1258948)Termination phase: Preprocessing 2
% 7.15/2.01 % (1258948)Time elapsed: 0.089 s
% 7.15/2.01 % (1258948)Peak memory usage: 51 MB
% 7.15/2.01 % (1258948)Instructions burned: 104 (million)
% 7.15/2.01 % (1258950)Instruction limit reached!
% 7.15/2.01 % (1258950)------------------------------
% 7.15/2.01 % (1258950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.15/2.01 % (1258950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.15/2.01 % (1258950)CaDiCaL version: 2.1.3
% 7.15/2.01 % (1258950)Termination reason: Instruction limit
% 7.15/2.01 % (1258950)Termination phase: Naming
% 7.15/2.01 % (1258950)Time elapsed: 0.097 s
% 7.15/2.01 % (1258950)Peak memory usage: 51 MB
% 7.15/2.01 % (1258950)Instructions burned: 133 (million)
% 7.15/2.01 % (1258949)Instruction limit reached!
% 7.15/2.01 % (1258949)------------------------------
% 7.15/2.01 % (1258949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.15/2.01 % (1258949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.15/2.01 % (1258949)CaDiCaL version: 2.1.3
% 7.15/2.01 % (1258949)Termination reason: Instruction limit
% 7.15/2.01 % (1258949)Termination phase: NewCNF
% 7.15/2.01 % (1258949)Time elapsed: 0.102 s
% 7.15/2.01 % (1258949)Peak memory usage: 53 MB
% 7.15/2.01 % (1258949)Instructions burned: 116 (million)
% 7.15/2.01 % (1258959)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1776539927:i=714:nm=2_2992 on theBenchmark for (2992ds/714Mi)
% 7.15/2.01 % (1258951)Instruction limit reached!
% 7.15/2.01 % (1258951)------------------------------
% 7.15/2.01 % (1258951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.15/2.01 % (1258951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.15/2.01 % (1258951)CaDiCaL version: 2.1.3
% 7.15/2.01 % (1258951)Termination reason: Instruction limit
% 7.15/2.01 % (1258951)Termination phase: Preprocessing 3
% 7.15/2.01 % (1258951)Time elapsed: 0.113 s
% 7.15/2.01 % (1258951)Peak memory usage: 52 MB
% 7.15/2.01 % (1258951)Instructions burned: 160 (million)
% 7.15/2.01 % (1258960)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2588788123:i=131:bd=preordered:fsd=on_2992 on theBenchmark for (2992ds/131Mi)
% 7.15/2.01 % (1258961)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=172173239:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2992 on theBenchmark for (2992ds/684Mi)
% 7.15/2.01 % (1258963)ott-21_1_sil=16000:fs=off:random_seed=3960610928:i=180:av=off:fsr=off_2992 on theBenchmark for (2992ds/180Mi)
% 7.15/2.01 % (1258960)Instruction limit reached!
% 7.15/2.01 % (1258960)------------------------------
% 7.15/2.01 % (1258960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.15/2.01 % (1258960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.15/2.01 % (1258960)CaDiCaL version: 2.1.3
% 8.90/2.06 % (1258960)Termination reason: Instruction limit
% 8.90/2.06 % (1258960)Termination phase: Naming
% 8.90/2.06 % (1258960)Time elapsed: 0.104 s
% 8.90/2.06 % (1258960)Peak memory usage: 52 MB
% 8.90/2.06 % (1258960)Instructions burned: 134 (million)
% 8.90/2.06 % (1258967)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=210581400:i=477:bd=all_2990 on theBenchmark for (2990ds/477Mi)
% 8.90/2.06 % (1258963)Instruction limit reached!
% 8.90/2.06 % (1258963)------------------------------
% 8.90/2.06 % (1258963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.90/2.06 % (1258963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.06 % (1258963)CaDiCaL version: 2.1.3
% 8.90/2.06 % (1258963)Termination reason: Instruction limit
% 8.90/2.06 % (1258963)Termination phase: Preprocessing 3
% 8.90/2.06 % (1258963)Time elapsed: 0.124 s
% 8.90/2.06 % (1258963)Peak memory usage: 52 MB
% 8.90/2.06 % (1258963)Instructions burned: 180 (million)
% 8.90/2.06 % (1258969)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4004660483:fmbsr=1.3:i=865:ins=25_2990 on theBenchmark for (2990ds/865Mi)
% 8.90/2.06 % (1258961)Instruction limit reached!
% 8.90/2.06 % (1258961)------------------------------
% 8.90/2.06 % (1258961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.90/2.06 % (1258961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.06 % (1258961)CaDiCaL version: 2.1.3
% 8.90/2.06 % (1258961)Termination reason: Instruction limit
% 8.90/2.06 % (1258961)Termination phase: NewCNF
% 8.90/2.06 % (1258961)Time elapsed: 0.324 s
% 8.90/2.06 % (1258961)Peak memory usage: 61 MB
% 8.90/2.06 % (1258961)Instructions burned: 687 (million)
% 8.90/2.06 % (1258971)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1192400784:i=1179_2988 on theBenchmark for (2988ds/1179Mi)
% 8.90/2.06 % (1258959)Instruction limit reached!
% 8.90/2.06 % (1258959)------------------------------
% 8.90/2.06 % (1258959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.90/2.06 % (1258959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.06 % (1258959)CaDiCaL version: 2.1.3
% 8.90/2.06 % (1258959)Termination reason: Instruction limit
% 8.90/2.06 % (1258959)Termination phase: Clausification
% 8.90/2.06 % (1258959)Time elapsed: 0.395 s
% 8.90/2.06 % (1258959)Peak memory usage: 85 MB
% 8.90/2.06 % (1258959)Instructions burned: 715 (million)
% 8.90/2.06 % (1258967)Instruction limit reached!
% 8.90/2.06 % (1258967)------------------------------
% 8.90/2.06 % (1258967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.90/2.06 % (1258967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.06 % (1258967)CaDiCaL version: 2.1.3
% 8.90/2.06 % (1258967)Termination reason: Instruction limit
% 8.90/2.06 % (1258967)Termination phase: Equality resolution with deletion
% 8.90/2.06 % (1258967)Time elapsed: 0.274 s
% 8.90/2.06 % (1258967)Peak memory usage: 58 MB
% 8.90/2.06 % (1258967)Instructions burned: 477 (million)
% 8.90/2.06 % (1258973)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2779831421:i=889:ins=1_2988 on theBenchmark for (2988ds/889Mi)
% 8.90/2.06 % (1258974)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=43848004:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2987 on theBenchmark for (2987ds/692Mi)
% 8.90/2.06 % (1258969)Instruction limit reached!
% 8.90/2.06 % (1258969)------------------------------
% 8.90/2.06 % (1258969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.90/2.06 % (1258969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.06 % (1258969)CaDiCaL version: 2.1.3
% 8.90/2.06 % (1258969)Termination reason: Instruction limit
% 8.90/2.06 % (1258969)Termination phase: Property scanning
% 8.90/2.06 % (1258969)Time elapsed: 0.444 s
% 8.90/2.06 % (1258969)Peak memory usage: 89 MB
% 8.90/2.06 % (1258969)Instructions burned: 867 (million)
% 8.90/2.06 % (1258977)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1316467825:i=879:kws=inv_precedence:fsr=off_2985 on theBenchmark for (2985ds/879Mi)
% 8.90/2.06 % (1258974)Instruction limit reached!
% 8.90/2.06 % (1258974)------------------------------
% 8.90/2.06 % (1258974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.90/2.06 % (1258974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.06 % (1258974)CaDiCaL version: 2.1.3
% 8.90/2.06 % (1258974)Termination reason: Instruction limit
% 8.90/2.06 % (1258974)Termination phase: NewCNF
% 8.90/2.06 % (1258974)Time elapsed: 0.324 s
% 8.90/2.06 % (1258974)Peak memory usage: 61 MB
% 8.90/2.06 % (1258974)Instructions burned: 694 (million)
% 8.90/2.06 % (1258979)fmb+10_1_sil=64000:random_seed=1141063391:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi)
% 8.90/2.06 % (1258973)Instruction limit reached!
% 8.90/2.06 % (1258973)------------------------------
% 8.90/2.06 % (1258973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.90/2.06 % (1258973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.06 % (1258973)CaDiCaL version: 2.1.3
% 8.90/2.06 % (1258973)Termination reason: Instruction limit
% 8.90/2.06 % (1258973)Termination phase: Property scanning
% 8.90/2.06 % (1258973)Time elapsed: 0.459 s
% 8.90/2.06 % (1258973)Peak memory usage: 89 MB
% 8.90/2.06 % (1258973)Instructions burned: 891 (million)
% 8.90/2.06 % (1258981)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=432314056:i=9515:nm=5_2983 on theBenchmark for (2983ds/9515Mi)
% 8.90/2.06 % (1258946) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1258940-1258946"...
% 8.90/2.06 % (1258971)Instruction limit reached!
% 8.90/2.06 % (1258971)------------------------------
% 8.90/2.06 % (1258971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.90/2.06 % (1258971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.06 % (1258971)CaDiCaL version: 2.1.3
% 8.90/2.06 % (1258971)Termination reason: Instruction limit
% 8.90/2.06 % (1258971)Termination phase: Saturation
% 8.90/2.06 % (1258971)Time elapsed: 0.601 s
% 8.90/2.06 % (1258971)Peak memory usage: 72 MB
% 8.90/2.06 % (1258971)Instructions burned: 1179 (million)
% 8.90/2.06 % (1258946)...printing done.
% 8.90/2.06 % (1258983)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3467095679:fmbsr=1.7:i=920_2982 on theBenchmark for (2982ds/920Mi)
% 8.90/2.06 % (1258946)Refutation found. Thanks to Tanya!
% 8.90/2.06 % SZS status Theorem for theBenchmark
% 8.90/2.06 % SZS output start Proof for theBenchmark
% See solution above
% 8.90/2.06 % (1258946)------------------------------
% 8.90/2.06 % (1258946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.90/2.06 % (1258946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.06 % (1258946)CaDiCaL version: 2.1.3
% 8.90/2.06 % (1258946)Termination reason: Refutation
% 8.90/2.06 % (1258946)Time elapsed: 1.079 s
% 8.90/2.06 % (1258946)Peak memory usage: 101 MB
% 8.90/2.06 % (1258946)Instructions burned: 3705 (million)
% 8.90/2.06 % (1258940)Success in time 1.794 s
% 8.90/2.06 % Vampire exiting
%------------------------------------------------------------------------------