%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW297+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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 01:39:46 PM UTC 2026
% Result : Theorem 2.72s 0.91s
% Output : Refutation 2.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 2
% Syntax : Number of formulae : 17 ( 7 unt; 0 def)
% Number of atoms : 45 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 44 ( 16 ~; 9 |; 3 &)
% ( 0 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-4 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 43 ( 40 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2,X3] :
( c_Natural_Oevaln(X3,X2,X1,X0)
=> c_Natural_Oevaln(X3,X2,hAPP(c_Nat_OSuc,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_evaln__Suc) ).
fof(f5225,conjecture,
( ! [X0,X1] :
( v_fun1(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(v_com,X1,hAPP(c_Nat_OSuc,v_n),X2)
=> v_fun2(X0,X2) ) )
=> ! [X0,X1] :
( v_fun1(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(v_com,X1,v_n,X2)
=> v_fun2(X0,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f5226,negated_conjecture,
~ ( ! [X0,X1] :
( v_fun1(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(v_com,X1,hAPP(c_Nat_OSuc,v_n),X2)
=> v_fun2(X0,X2) ) )
=> ! [X0,X1] :
( v_fun1(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(v_com,X1,v_n,X2)
=> v_fun2(X0,X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f5225]) ).
fof(f5249,plain,
~ ( ! [X0,X1] :
( v_fun1(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(v_com,X1,hAPP(c_Nat_OSuc,v_n),X2)
=> v_fun2(X0,X2) ) )
=> ! [X3,X4] :
( v_fun1(X3,X4)
=> ! [X5] :
( c_Natural_Oevaln(v_com,X4,v_n,X5)
=> v_fun2(X3,X5) ) ) ),
inference(rectify,[],[f5226]) ).
fof(f5433,plain,
! [X0,X1,X2,X3] :
( c_Natural_Oevaln(X3,X2,hAPP(c_Nat_OSuc,X1),X0)
| ~ c_Natural_Oevaln(X3,X2,X1,X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f9568,plain,
( ? [X3,X4] :
( ? [X5] :
( ~ v_fun2(X3,X5)
& c_Natural_Oevaln(v_com,X4,v_n,X5) )
& v_fun1(X3,X4) )
& ! [X0,X1] :
( ! [X2] :
( v_fun2(X0,X2)
| ~ c_Natural_Oevaln(v_com,X1,hAPP(c_Nat_OSuc,v_n),X2) )
| ~ v_fun1(X0,X1) ) ),
inference(ennf_transformation,[],[f5249]) ).
fof(f9570,plain,
! [X2,X3,X0,X1] :
( ~ c_Natural_Oevaln(X3,X2,X1,X0)
| c_Natural_Oevaln(X3,X2,hAPP(c_Nat_OSuc,X1),X0) ),
inference(cnf_transformation,[],[f5433]) ).
fof(f16684,plain,
c_Natural_Oevaln(v_com,sK548,v_n,sK549),
inference(cnf_transformation,[],[f9568]) ).
fof(f16685,plain,
~ v_fun2(sK547,sK549),
inference(cnf_transformation,[],[f9568]) ).
fof(f16686,plain,
! [X2,X0,X1] :
( ~ v_fun1(X0,X1)
| ~ c_Natural_Oevaln(v_com,X1,hAPP(c_Nat_OSuc,v_n),X2)
| v_fun2(X0,X2) ),
inference(cnf_transformation,[],[f9568]) ).
fof(f16687,plain,
v_fun1(sK547,sK548),
inference(cnf_transformation,[],[f9568]) ).
fof(f23199,plain,
! [X2,X0,X1] :
( ~ c_Natural_Oevaln(v_com,X1,hAPP(c_Nat_OSuc,v_n),X2)
| ~ v_fun1(X0,X1)
| ~ v_fun2(X0,X2) ),
inference(consistent_polarity_flipping,[],[f16686]) ).
fof(f23200,plain,
v_fun2(sK547,sK549),
inference(consistent_polarity_flipping,[],[f16685]) ).
fof(f28567,plain,
c_Natural_Oevaln(v_com,sK548,hAPP(c_Nat_OSuc,v_n),sK549),
inference(resolution,[],[f9570,f16684]) ).
fof(f28570,plain,
! [X0] :
( ~ v_fun2(X0,sK549)
| ~ v_fun1(X0,sK548) ),
inference(resolution,[],[f28567,f23199]) ).
fof(f28572,plain,
~ v_fun1(sK547,sK548),
inference(resolution,[],[f28570,f23200]) ).
fof(f28573,plain,
$false,
inference(forward_subsumption_resolution,[],[f28572,f16687]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW297+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n008.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 13:31:55 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.23 Running first-order model finding
% 0.08/0.23 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
% 2.72/0.91 % (2250269)Will run a generic schedule for satisfiability detection.
% 2.72/0.91 % (2250275)% WARNING: option uhcvi not known.
% 2.72/0.91 % (2250274)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3195361048_2998 on theBenchmark for (2998ds/0Mi)
% 2.72/0.91 % (2250275)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1705040572:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 2.72/0.91 % (2250276)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=438120502:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 2.72/0.91 % (2250277)dis+10_1_sil=32000:sp=arity:random_seed=3472644160:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 2.72/0.91 % (2250278)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=125971115:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 2.72/0.91 % (2250279)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2725048462:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 2.72/0.91 % (2250280)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2593468663:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 2.72/0.91 % (2250277)Instruction limit reached!
% 2.72/0.91 % (2250277)------------------------------
% 2.72/0.91 % (2250277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.91 % (2250277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.91 % (2250277)CaDiCaL version: 2.1.3
% 2.72/0.91 % (2250277)Termination reason: Instruction limit
% 2.72/0.91 % (2250277)Termination phase: Preprocessing 3
% 2.72/0.91 % (2250277)Time elapsed: 0.063 s
% 2.72/0.91 % (2250277)Peak memory usage: 20 MB
% 2.72/0.91 % (2250277)Instructions burned: 103 (million)
% 2.72/0.91 % (2250280)Instruction limit reached!
% 2.72/0.91 % (2250280)------------------------------
% 2.72/0.91 % (2250280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.91 % (2250280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.91 % (2250280)CaDiCaL version: 2.1.3
% 2.72/0.91 % (2250280)Termination reason: Instruction limit
% 2.72/0.91 % (2250280)Termination phase: Clausification
% 2.72/0.91 % (2250280)Time elapsed: 0.064 s
% 2.72/0.91 % (2250280)Peak memory usage: 21 MB
% 2.72/0.91 % (2250280)Instructions burned: 161 (million)
% 2.72/0.91 % (2250278)Instruction limit reached!
% 2.72/0.91 % (2250278)------------------------------
% 2.72/0.91 % (2250278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.91 % (2250278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.91 % (2250278)CaDiCaL version: 2.1.3
% 2.72/0.91 % (2250278)Termination reason: Instruction limit
% 2.72/0.91 % (2250278)Termination phase: NewCNF
% 2.72/0.91 % (2250278)Time elapsed: 0.074 s
% 2.72/0.91 % (2250278)Peak memory usage: 21 MB
% 2.72/0.91 % (2250278)Instructions burned: 116 (million)
% 2.72/0.91 % (2250289)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2788331563:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 2.72/0.91 % (2250279)Instruction limit reached!
% 2.72/0.91 % (2250279)------------------------------
% 2.72/0.91 % (2250279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.91 % (2250279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.91 % (2250279)CaDiCaL version: 2.1.3
% 2.72/0.91 % (2250279)Termination reason: Instruction limit
% 2.72/0.91 % (2250279)Termination phase: Preprocessing 3
% 2.72/0.91 % (2250279)Time elapsed: 0.078 s
% 2.72/0.91 % (2250279)Peak memory usage: 20 MB
% 2.72/0.91 % (2250279)Instructions burned: 132 (million)
% 2.72/0.91 % (2250288)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1066190555:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 2.72/0.91 % (2250290)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=363614553:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 2.72/0.91 % (2250292)ott-21_1_sil=16000:fs=off:random_seed=2579602081:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 2.72/0.91 % (2250289)Instruction limit reached!
% 2.72/0.91 % (2250289)------------------------------
% 2.72/0.91 % (2250289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.91 % (2250289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.91 % (2250289)CaDiCaL version: 2.1.3
% 2.72/0.91 % (2250289)Termination reason: Instruction limit
% 2.72/0.91 % (2250289)Termination phase: Preprocessing 3
% 2.72/0.91 % (2250289)Time elapsed: 0.046 s
% 2.72/0.91 % (2250289)Peak memory usage: 20 MB
% 2.72/0.91 % (2250289)Instructions burned: 141 (million)
% 2.72/0.91 % (2250296)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2424557706:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 2.72/0.91 % (2250292)Instruction limit reached!
% 2.72/0.91 % (2250292)------------------------------
% 2.72/0.91 % (2250292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.91 % (2250292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.91 % (2250292)CaDiCaL version: 2.1.3
% 2.72/0.91 % (2250292)Termination reason: Instruction limit
% 2.72/0.91 % (2250292)Termination phase: Property scanning
% 2.72/0.91 % (2250292)Time elapsed: 0.104 s
% 2.72/0.91 % (2250292)Peak memory usage: 22 MB
% 2.72/0.91 % (2250292)Instructions burned: 181 (million)
% 2.72/0.91 % (2250298)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3425511180:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 2.72/0.91 % (2250296)Instruction limit reached!
% 2.72/0.91 % (2250296)------------------------------
% 2.72/0.91 % (2250296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.91 % (2250296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.91 % (2250296)CaDiCaL version: 2.1.3
% 2.72/0.91 % (2250296)Termination reason: Instruction limit
% 2.72/0.91 % (2250296)Termination phase: Property scanning
% 2.72/0.91 % (2250296)Time elapsed: 0.120 s
% 2.72/0.91 % (2250296)Peak memory usage: 23 MB
% 2.72/0.91 % (2250296)Instructions burned: 479 (million)
% 2.72/0.91 % (2250300)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2099852098:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 2.72/0.91 % (2250288)Instruction limit reached!
% 2.72/0.91 % (2250288)------------------------------
% 2.72/0.91 % (2250288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.91 % (2250288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.91 % (2250288)CaDiCaL version: 2.1.3
% 2.72/0.91 % (2250288)Termination reason: Instruction limit
% 2.72/0.91 % (2250288)Termination phase: Finite model building preprocessing
% 2.72/0.91 % (2250288)Time elapsed: 0.324 s
% 2.72/0.91 % (2250288)Peak memory usage: 25 MB
% 2.72/0.91 % (2250288)Instructions burned: 715 (million)
% 2.72/0.91 % (2250290)Instruction limit reached!
% 2.72/0.91 % (2250290)------------------------------
% 2.72/0.91 % (2250290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.91 % (2250290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.91 % (2250290)CaDiCaL version: 2.1.3
% 2.72/0.91 % (2250290)Termination reason: Instruction limit
% 2.72/0.91 % (2250290)Termination phase: Saturation
% 2.72/0.91 % (2250290)Time elapsed: 0.321 s
% 2.72/0.91 % (2250290)Peak memory usage: 25 MB
% 2.72/0.91 % (2250290)Instructions burned: 686 (million)
% 2.72/0.91 % (2250302)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3004489713:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 2.72/0.91 % (2250303)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=591837720:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 2.72/0.91 % (2250275) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2250269-2250275"...
% 2.72/0.91 % (2250275)...printing done.
% 2.72/0.91 % (2250275)Refutation found. Thanks to Tanya!
% 2.72/0.91 % SZS status Theorem for theBenchmark
% 2.72/0.91 % SZS output start Proof for theBenchmark
% See solution above
% 2.72/0.91 % (2250275)------------------------------
% 2.72/0.91 % (2250275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/0.91 % (2250275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/0.91 % (2250275)CaDiCaL version: 2.1.3
% 2.72/0.91 % (2250275)Termination reason: Refutation
% 2.72/0.91 % (2250275)Time elapsed: 0.479 s
% 2.72/0.91 % (2250275)Peak memory usage: 29 MB
% 2.72/0.91 % (2250275)Instructions burned: 924 (million)
% 2.72/0.91 % (2250269)Success in time 0.673 s
% 2.72/0.91 % Vampire exiting
%------------------------------------------------------------------------------