%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR106+7 : 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 : n007.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:19 AM UTC 2026
% Result : Theorem 0.20s 3.30s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 3
% Syntax : Number of formulae : 11 ( 8 unt; 0 def)
% Number of atoms : 14 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 12 ( 9 ~; 2 |; 0 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 12 ( 8 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f27726,axiom,
! [X0] :
( s__instance(X0,s__TimePoint)
=> ~ s__before(X0,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+2.ax',kb_SUMO_27908) ).
fof(f33168,axiom,
s__instance(s__PositiveInfinity,s__TimePoint),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+2.ax',kb_SUMO_33361) ).
fof(f55594,conjecture,
? [X0,X1] : ~ s__before(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_ALL) ).
fof(f55595,negated_conjecture,
~ ? [X0,X1] : ~ s__before(X0,X1),
inference(negated_conjecture,[status(cth)],[f55594]) ).
fof(f66236,plain,
! [X0] :
( ~ s__before(X0,X0)
| ~ s__instance(X0,s__TimePoint) ),
inference(ennf_transformation,[],[f27726]) ).
fof(f78994,plain,
! [X0,X1] : s__before(X0,X1),
inference(ennf_transformation,[],[f55595]) ).
fof(f103384,plain,
! [X0] :
( ~ s__instance(X0,s__TimePoint)
| ~ s__before(X0,X0) ),
inference(cnf_transformation,[],[f66236]) ).
fof(f108798,plain,
s__instance(s__PositiveInfinity,s__TimePoint),
inference(cnf_transformation,[],[f33168]) ).
fof(f136050,plain,
! [X0,X1] : s__before(X0,X1),
inference(cnf_transformation,[],[f78994]) ).
fof(f160681,plain,
! [X0] : ~ s__instance(X0,s__TimePoint),
inference(forward_subsumption_resolution,[],[f103384,f136050]) ).
fof(f160682,plain,
$false,
inference(backward_subsumption_resolution,[],[f108798,f160681]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR106+7 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n007.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 22:57:39 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 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.20/3.30 % (2944637)Will run a generic schedule for satisfiability detection.
% 0.20/3.30 % (2944902)% WARNING: option uhcvi not known.
% 0.20/3.30 % (2944902)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3623854713:i=135531:add=off:rawr=on_2984 on theBenchmark for (2984ds/135531Mi)
% 0.20/3.30 % (2944901)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=653592221_2984 on theBenchmark for (2984ds/0Mi)
% 0.20/3.30 % (2944904)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3896292501:i=88024:add=on:rawr=on_2984 on theBenchmark for (2984ds/88024Mi)
% 0.20/3.30 % (2944905)dis+10_1_sil=32000:sp=arity:random_seed=1583302846:i=103:fgj=on_2984 on theBenchmark for (2984ds/103Mi)
% 0.20/3.30 % (2944907)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2787431245:i=116_2984 on theBenchmark for (2984ds/116Mi)
% 0.20/3.30 % (2944910)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3177750659:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2984 on theBenchmark for (2984ds/159Mi)
% 0.20/3.30 % (2944909)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3556518871:i=131_2984 on theBenchmark for (2984ds/131Mi)
% 0.20/3.30 % (2944905)Instruction limit reached!
% 0.20/3.30 % (2944905)------------------------------
% 0.20/3.30 % (2944905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944905)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944905)Termination reason: Instruction limit
% 0.20/3.30 % (2944905)Termination phase: Preprocessing 1
% 0.20/3.30 % (2944905)Time elapsed: 0.065 s
% 0.20/3.30 % (2944905)Peak memory usage: 90 MB
% 0.20/3.30 % (2944905)Instructions burned: 104 (million)
% 0.20/3.30 % (2944907)Instruction limit reached!
% 0.20/3.30 % (2944907)------------------------------
% 0.20/3.30 % (2944907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944907)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944907)Termination reason: Instruction limit
% 0.20/3.30 % (2944907)Termination phase: Preprocessing 1
% 0.20/3.30 % (2944907)Time elapsed: 0.082 s
% 0.20/3.30 % (2944907)Peak memory usage: 90 MB
% 0.20/3.30 % (2944907)Instructions burned: 117 (million)
% 0.20/3.30 % (2944924)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=529046231:i=714:nm=2_2983 on theBenchmark for (2983ds/714Mi)
% 0.20/3.30 % (2944910)Instruction limit reached!
% 0.20/3.30 % (2944910)------------------------------
% 0.20/3.30 % (2944910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944910)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944910)Termination reason: Instruction limit
% 0.20/3.30 % (2944910)Termination phase: Preprocessing 1
% 0.20/3.30 % (2944910)Time elapsed: 0.103 s
% 0.20/3.30 % (2944910)Peak memory usage: 90 MB
% 0.20/3.30 % (2944910)Instructions burned: 159 (million)
% 0.20/3.30 % (2944909)Instruction limit reached!
% 0.20/3.30 % (2944909)------------------------------
% 0.20/3.30 % (2944909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944909)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944909)Termination reason: Instruction limit
% 0.20/3.30 % (2944909)Termination phase: Preprocessing 1
% 0.20/3.30 % (2944909)Time elapsed: 0.097 s
% 0.20/3.30 % (2944909)Peak memory usage: 90 MB
% 0.20/3.30 % (2944909)Instructions burned: 131 (million)
% 0.20/3.30 % (2944926)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4069649358:i=131:bd=preordered:fsd=on_2982 on theBenchmark for (2982ds/131Mi)
% 0.20/3.30 % (2944929)ott-21_1_sil=16000:fs=off:random_seed=4182008713:i=180:av=off:fsr=off_2982 on theBenchmark for (2982ds/180Mi)
% 0.20/3.30 % (2944928)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=3792471288:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2982 on theBenchmark for (2982ds/684Mi)
% 0.20/3.30 % (2944926)Instruction limit reached!
% 0.20/3.30 % (2944926)------------------------------
% 0.20/3.30 % (2944926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944926)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944926)Termination reason: Instruction limit
% 0.20/3.30 % (2944926)Termination phase: Preprocessing 1
% 0.20/3.30 % (2944926)Time elapsed: 0.087 s
% 0.20/3.30 % (2944926)Peak memory usage: 90 MB
% 0.20/3.30 % (2944926)Instructions burned: 132 (million)
% 0.20/3.30 % (2944932)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=205387775:i=477:bd=all_2981 on theBenchmark for (2981ds/477Mi)
% 0.20/3.30 % (2944929)Instruction limit reached!
% 0.20/3.30 % (2944929)------------------------------
% 0.20/3.30 % (2944929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944929)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944929)Termination reason: Instruction limit
% 0.20/3.30 % (2944929)Termination phase: Unused predicate definition removal
% 0.20/3.30 % (2944929)Time elapsed: 0.122 s
% 0.20/3.30 % (2944929)Peak memory usage: 91 MB
% 0.20/3.30 % (2944929)Instructions burned: 181 (million)
% 0.20/3.30 % (2944934)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3199643623:fmbsr=1.3:i=865:ins=25_2981 on theBenchmark for (2981ds/865Mi)
% 0.20/3.30 % (2944924)Instruction limit reached!
% 0.20/3.30 % (2944924)------------------------------
% 0.20/3.30 % (2944924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944924)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944924)Termination reason: Instruction limit
% 0.20/3.30 % (2944924)Termination phase: Unused predicate definition removal
% 0.20/3.30 % (2944924)Time elapsed: 0.403 s
% 0.20/3.30 % (2944924)Peak memory usage: 127 MB
% 0.20/3.30 % (2944924)Instructions burned: 715 (million)
% 0.20/3.30 % (2944936)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2186757307:i=1179_2978 on theBenchmark for (2978ds/1179Mi)
% 0.20/3.30 % (2944932)Instruction limit reached!
% 0.20/3.30 % (2944932)------------------------------
% 0.20/3.30 % (2944932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944932)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944932)Termination reason: Instruction limit
% 0.20/3.30 % (2944932)Termination phase: Preprocessing 3
% 0.20/3.30 % (2944932)Time elapsed: 0.318 s
% 0.20/3.30 % (2944932)Peak memory usage: 102 MB
% 0.20/3.30 % (2944932)Instructions burned: 478 (million)
% 0.20/3.30 % (2944938)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3042545840:i=889:ins=1_2978 on theBenchmark for (2978ds/889Mi)
% 0.20/3.30 % (2944928)Instruction limit reached!
% 0.20/3.30 % (2944928)------------------------------
% 0.20/3.30 % (2944928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944928)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944928)Termination reason: Instruction limit
% 0.20/3.30 % (2944928)Termination phase: NewCNF
% 0.20/3.30 % (2944928)Time elapsed: 0.544 s
% 0.20/3.30 % (2944928)Peak memory usage: 106 MB
% 0.20/3.30 % (2944928)Instructions burned: 684 (million)
% 0.20/3.30 % (2944941)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=1789419145:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2976 on theBenchmark for (2976ds/692Mi)
% 0.20/3.30 % (2944934)Instruction limit reached!
% 0.20/3.30 % (2944934)------------------------------
% 0.20/3.30 % (2944934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944934)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944934)Termination reason: Instruction limit
% 0.20/3.30 % (2944934)Termination phase: Naming
% 0.20/3.30 % (2944934)Time elapsed: 0.514 s
% 0.20/3.30 % (2944934)Peak memory usage: 156 MB
% 0.20/3.30 % (2944934)Instructions burned: 867 (million)
% 0.20/3.30 % (2944943)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=196138288:i=879:kws=inv_precedence:fsr=off_2975 on theBenchmark for (2975ds/879Mi)
% 0.20/3.30 % (2944938)Instruction limit reached!
% 0.20/3.30 % (2944938)------------------------------
% 0.20/3.30 % (2944938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944938)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944938)Termination reason: Instruction limit
% 0.20/3.30 % (2944938)Termination phase: Naming
% 0.20/3.30 % (2944938)Time elapsed: 0.534 s
% 0.20/3.30 % (2944938)Peak memory usage: 149 MB
% 0.20/3.30 % (2944938)Instructions burned: 889 (million)
% 0.20/3.30 % (2944902) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2944637-2944902"...
% 0.20/3.30 % (2944952)fmb+10_1_sil=64000:random_seed=2877785967:i=22061:nm=2:gsp=on_2972 on theBenchmark for (2972ds/22061Mi)
% 0.20/3.30 % (2944936)Instruction limit reached!
% 0.20/3.30 % (2944936)------------------------------
% 0.20/3.30 % (2944936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944936)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944936)Termination reason: Instruction limit
% 0.20/3.30 % (2944936)Termination phase: Property scanning
% 0.20/3.30 % (2944936)Time elapsed: 0.664 s
% 0.20/3.30 % (2944936)Peak memory usage: 111 MB
% 0.20/3.30 % (2944936)Instructions burned: 1180 (million)
% 0.20/3.30 % (2944954)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3784345803:i=9515:nm=5_2971 on theBenchmark for (2971ds/9515Mi)
% 0.20/3.30 % (2944902)...printing done.
% 0.20/3.30 % (2944941)Instruction limit reached!
% 0.20/3.30 % (2944941)------------------------------
% 0.20/3.30 % (2944941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944941)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944941)Termination reason: Instruction limit
% 0.20/3.30 % (2944941)Termination phase: NewCNF
% 0.20/3.30 % (2944941)Time elapsed: 0.520 s
% 0.20/3.30 % (2944941)Peak memory usage: 106 MB
% 0.20/3.30 % (2944941)Instructions burned: 693 (million)
% 0.20/3.30 % (2944902)Refutation found. Thanks to Tanya!
% 0.20/3.30 % SZS status Theorem for theBenchmark
% 0.20/3.30 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/3.30 % (2944902)------------------------------
% 0.20/3.30 % (2944902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/3.30 % (2944902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.30 % (2944902)CaDiCaL version: 2.1.3
% 0.20/3.30 % (2944902)Termination reason: Refutation
% 0.20/3.30 % (2944902)Time elapsed: 1.193 s
% 0.20/3.30 % (2944902)Peak memory usage: 155 MB
% 0.20/3.30 % (2944902)Instructions burned: 3895 (million)
% 0.20/3.30 % (2944637)Success in time 2.932 s
% 0.20/3.30 % Vampire exiting
%------------------------------------------------------------------------------