%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV239-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:20:32 PM UTC 2026
% Result : Unsatisfiable 5.59s 1.11s
% Output : Refutation 5.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 12
% Syntax : Number of formulae : 37 ( 22 unt; 6 def)
% Number of atoms : 60 ( 12 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 47 ( 24 ~; 23 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-3 aty)
% Number of variables : 30 ( 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f127,axiom,
! [X2,X0,X1] :
( c_lessequals(X0,X1,tc_set(X2))
| c_in(c_Main_OsubsetI__1(X0,X1,X2),X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-0.ax',cls_Set_OsubsetI_0) ).
fof(f128,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Main_OsubsetI__1(X0,X1,X2),X1,X2)
| c_lessequals(X0,X1,tc_set(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-0.ax',cls_Set_OsubsetI_1) ).
fof(f131,axiom,
! [X0,X1] : c_lessequals(X0,X0,tc_set(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-0.ax',cls_Set_Osubset__refl_0) ).
fof(f1453,axiom,
! [X0,X1] :
( ~ c_in(X0,c_Message_Oanalz(c_Message_Oanalz(X1)),tc_Message_Omsg)
| c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV004-0.ax',cls_Message_Oanalz__analzD__dest_0) ).
fof(f1473,axiom,
! [X2,X3,X0,X1] :
( c_lessequals(c_Message_Oanalz(c_union(X2,X0,tc_Message_Omsg)),c_Message_Oanalz(c_union(X3,X1,tc_Message_Omsg)),tc_set(tc_Message_Omsg))
| ~ c_lessequals(c_Message_Oanalz(X2),c_Message_Oanalz(X3),tc_set(tc_Message_Omsg))
| ~ c_lessequals(c_Message_Oanalz(X0),c_Message_Oanalz(X1),tc_set(tc_Message_Omsg)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Message_Oanalz__subset__cong_0) ).
fof(f1475,negated_conjecture,
~ c_lessequals(c_Message_Oanalz(c_union(c_Message_Oanalz(v_G),v_H,tc_Message_Omsg)),c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_set(tc_Message_Omsg)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1476,definition,
sF0 = c_Message_Oanalz(v_G),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1477,plain,
c_Message_Oanalz(v_G) = sF0,
inference(reorient_equations,[],[f1476]) ).
fof(f1478,definition,
sF1 = c_union(sF0,v_H,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1479,plain,
c_union(sF0,v_H,tc_Message_Omsg) = sF1,
inference(reorient_equations,[],[f1478]) ).
fof(f1480,definition,
sF2 = c_Message_Oanalz(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1481,plain,
c_Message_Oanalz(sF1) = sF2,
inference(reorient_equations,[],[f1480]) ).
fof(f1482,definition,
sF3 = c_union(v_G,v_H,tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1483,plain,
c_union(v_G,v_H,tc_Message_Omsg) = sF3,
inference(reorient_equations,[],[f1482]) ).
fof(f1484,definition,
sF4 = c_Message_Oanalz(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1485,plain,
c_Message_Oanalz(sF3) = sF4,
inference(reorient_equations,[],[f1484]) ).
fof(f1486,definition,
sF5 = tc_set(tc_Message_Omsg),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1487,plain,
tc_set(tc_Message_Omsg) = sF5,
inference(reorient_equations,[],[f1486]) ).
fof(f1488,plain,
~ c_lessequals(sF2,sF4,sF5),
inference(definition_folding,[],[f1475,f1487,f1485,f1483,f1481,f1479,f1477]) ).
fof(f1801,plain,
! [X0] : c_lessequals(X0,X0,sF5),
inference(superposition,[],[f131,f1487]) ).
fof(f1969,plain,
! [X0] :
( ~ c_in(X0,c_Message_Oanalz(sF0),tc_Message_Omsg)
| c_in(X0,sF0,tc_Message_Omsg) ),
inference(superposition,[],[f1453,f1477]) ).
fof(f2005,plain,
! [X0,X1] :
( c_lessequals(X0,X1,sF5)
| c_in(c_Main_OsubsetI__1(X0,X1,tc_Message_Omsg),X0,tc_Message_Omsg) ),
inference(superposition,[],[f127,f1487]) ).
fof(f4023,plain,
! [X0,X1] :
( c_lessequals(c_Message_Oanalz(c_union(X0,X1,tc_Message_Omsg)),c_Message_Oanalz(sF3),tc_set(tc_Message_Omsg))
| ~ c_lessequals(c_Message_Oanalz(X0),c_Message_Oanalz(v_G),tc_set(tc_Message_Omsg))
| ~ c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(v_H),tc_set(tc_Message_Omsg)) ),
inference(superposition,[],[f1473,f1483]) ).
fof(f4025,plain,
! [X0,X1] :
( c_lessequals(c_Message_Oanalz(c_union(X0,X1,tc_Message_Omsg)),c_Message_Oanalz(sF3),sF5)
| ~ c_lessequals(c_Message_Oanalz(X0),c_Message_Oanalz(v_G),tc_set(tc_Message_Omsg))
| ~ c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(v_H),tc_set(tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f4023,f1487]) ).
fof(f4040,plain,
! [X0,X1] :
( c_lessequals(c_Message_Oanalz(c_union(X0,X1,tc_Message_Omsg)),sF4,sF5)
| ~ c_lessequals(c_Message_Oanalz(X0),c_Message_Oanalz(v_G),tc_set(tc_Message_Omsg))
| ~ c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(v_H),tc_set(tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f4025,f1485]) ).
fof(f4055,plain,
! [X0,X1] :
( ~ c_lessequals(c_Message_Oanalz(X0),c_Message_Oanalz(v_G),sF5)
| c_lessequals(c_Message_Oanalz(c_union(X0,X1,tc_Message_Omsg)),sF4,sF5)
| ~ c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(v_H),tc_set(tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f4040,f1487]) ).
fof(f4069,plain,
! [X0,X1] :
( ~ c_lessequals(c_Message_Oanalz(X0),sF0,sF5)
| c_lessequals(c_Message_Oanalz(c_union(X0,X1,tc_Message_Omsg)),sF4,sF5)
| ~ c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(v_H),tc_set(tc_Message_Omsg)) ),
inference(forward_demodulation,[],[f4055,f1477]) ).
fof(f4076,plain,
! [X0,X1] :
( c_lessequals(c_Message_Oanalz(c_union(X0,X1,tc_Message_Omsg)),sF4,sF5)
| ~ c_lessequals(c_Message_Oanalz(X0),sF0,sF5)
| ~ c_lessequals(c_Message_Oanalz(X1),c_Message_Oanalz(v_H),sF5) ),
inference(forward_demodulation,[],[f4069,f1487]) ).
fof(f13409,plain,
( c_lessequals(c_Message_Oanalz(sF1),sF4,sF5)
| ~ c_lessequals(c_Message_Oanalz(sF0),sF0,sF5)
| ~ c_lessequals(c_Message_Oanalz(v_H),c_Message_Oanalz(v_H),sF5) ),
inference(superposition,[],[f4076,f1479]) ).
fof(f13412,plain,
( c_lessequals(c_Message_Oanalz(sF1),sF4,sF5)
| ~ c_lessequals(c_Message_Oanalz(sF0),sF0,sF5) ),
inference(forward_subsumption_resolution,[],[f13409,f1801]) ).
fof(f13422,plain,
( c_lessequals(sF2,sF4,sF5)
| ~ c_lessequals(c_Message_Oanalz(sF0),sF0,sF5) ),
inference(forward_demodulation,[],[f13412,f1481]) ).
fof(f13425,plain,
~ c_lessequals(c_Message_Oanalz(sF0),sF0,sF5),
inference(forward_subsumption_resolution,[],[f13422,f1488]) ).
fof(f13437,plain,
c_in(c_Main_OsubsetI__1(c_Message_Oanalz(sF0),sF0,tc_Message_Omsg),c_Message_Oanalz(sF0),tc_Message_Omsg),
inference(resolution,[],[f13425,f2005]) ).
fof(f13623,plain,
c_in(c_Main_OsubsetI__1(c_Message_Oanalz(sF0),sF0,tc_Message_Omsg),sF0,tc_Message_Omsg),
inference(resolution,[],[f13437,f1969]) ).
fof(f13807,plain,
c_lessequals(c_Message_Oanalz(sF0),sF0,tc_set(tc_Message_Omsg)),
inference(resolution,[],[f13623,f128]) ).
fof(f13813,plain,
c_lessequals(c_Message_Oanalz(sF0),sF0,sF5),
inference(forward_demodulation,[],[f13807,f1487]) ).
fof(f13815,plain,
$false,
inference(forward_subsumption_resolution,[],[f13813,f13425]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV239-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.17 % Computer : n002.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Mon Sep 28 10:17:07 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.21 Running first-order model finding
% 0.10/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.59/1.11 % (253119)Will run a generic schedule for satisfiability detection.
% 5.59/1.11 % (253126)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1236495823:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.59/1.11 % (253125)% WARNING: option uhcvi not known.
% 5.59/1.11 % (253124)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=791163398_2999 on theBenchmark for (2999ds/0Mi)
% 5.59/1.11 % (253125)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1440095801:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.59/1.11 % (253127)dis+10_1_sil=32000:sp=arity:random_seed=3965674955:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.59/1.11 % (253128)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2821422052:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.59/1.11 % (253130)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1792402716:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.59/1.11 % (253129)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2350607263:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.59/1.11 % TRYING [1]
% 5.59/1.11 % TRYING [2]
% 5.59/1.11 % (253127)Instruction limit reached!
% 5.59/1.11 % (253127)------------------------------
% 5.59/1.11 % (253127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.59/1.11 % (253127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.11 % (253127)CaDiCaL version: 2.1.3
% 5.59/1.11 % (253127)Termination reason: Instruction limit
% 5.59/1.11 % (253127)Termination phase: Saturation
% 5.59/1.11 % (253127)Time elapsed: 0.067 s
% 5.59/1.11 % (253127)Peak memory usage: 14 MB
% 5.59/1.11 % (253127)Instructions burned: 103 (million)
% 5.59/1.11 % (253128)Instruction limit reached!
% 5.59/1.11 % (253128)------------------------------
% 5.59/1.11 % (253128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.59/1.11 % (253128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.11 % (253128)CaDiCaL version: 2.1.3
% 5.59/1.11 % (253128)Termination reason: Instruction limit
% 5.59/1.11 % (253128)Termination phase: Saturation
% 5.59/1.11 % (253128)Time elapsed: 0.074 s
% 5.59/1.11 % (253128)Peak memory usage: 14 MB
% 5.59/1.11 % (253128)Instructions burned: 123 (million)
% 5.59/1.11 % (253129)Instruction limit reached!
% 5.59/1.11 % (253129)------------------------------
% 5.59/1.11 % (253129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.59/1.11 % (253129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.11 % (253129)CaDiCaL version: 2.1.3
% 5.59/1.11 % (253129)Termination reason: Instruction limit
% 5.59/1.11 % (253129)Termination phase: Saturation
% 5.59/1.11 % (253129)Time elapsed: 0.074 s
% 5.59/1.11 % (253129)Peak memory usage: 14 MB
% 5.59/1.11 % (253129)Instructions burned: 135 (million)
% 5.59/1.11 % (253138)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3763991798:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 5.59/1.11 % (253130)Instruction limit reached!
% 5.59/1.11 % (253130)------------------------------
% 5.59/1.11 % (253130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.59/1.11 % (253130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.11 % (253130)CaDiCaL version: 2.1.3
% 5.59/1.11 % (253130)Termination reason: Instruction limit
% 5.59/1.11 % (253130)Termination phase: Saturation
% 5.59/1.11 % (253130)Time elapsed: 0.092 s
% 5.59/1.11 % (253130)Peak memory usage: 14 MB
% 5.59/1.11 % (253130)Instructions burned: 159 (million)
% 5.59/1.11 % (253140)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=372773736:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.59/1.11 % (253139)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1632440179:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.59/1.11 % TRYING [3]
% 5.59/1.11 % (253142)ott-21_1_sil=16000:fs=off:random_seed=3657895979:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.59/1.11 % TRYING [1]
% 5.59/1.11 % TRYING [2]
% 5.59/1.11 % (253139)Instruction limit reached!
% 5.59/1.11 % (253139)------------------------------
% 5.59/1.11 % (253139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.59/1.11 % (253139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.11 % (253139)CaDiCaL version: 2.1.3
% 5.59/1.11 % (253139)Termination reason: Instruction limit
% 5.59/1.11 % (253139)Termination phase: Saturation
% 5.59/1.11 % (253139)Time elapsed: 0.080 s
% 5.59/1.11 % (253139)Peak memory usage: 15 MB
% 5.59/1.11 % (253139)Instructions burned: 131 (million)
% 5.59/1.11 % (253146)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3997823742:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 5.59/1.11 % TRYING [3]
% 5.59/1.11 % (253142)Instruction limit reached!
% 5.59/1.11 % (253142)------------------------------
% 5.59/1.11 % (253142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.59/1.11 % (253142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.11 % (253142)CaDiCaL version: 2.1.3
% 5.59/1.11 % (253142)Termination reason: Instruction limit
% 5.59/1.11 % (253142)Termination phase: Saturation
% 5.59/1.11 % (253142)Time elapsed: 0.103 s
% 5.59/1.11 % (253142)Peak memory usage: 14 MB
% 5.59/1.11 % (253142)Instructions burned: 180 (million)
% 5.59/1.11 % (253148)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=274244854:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 5.59/1.11 % TRYING [1]
% 5.59/1.11 % TRYING [2]
% 5.59/1.11 % TRYING [4]
% 5.59/1.11 % (253138)Instruction limit reached!
% 5.59/1.11 % (253138)------------------------------
% 5.59/1.11 % (253138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.59/1.11 % (253138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.11 % (253138)CaDiCaL version: 2.1.3
% 5.59/1.11 % (253138)Termination reason: Instruction limit
% 5.59/1.11 % (253138)Termination phase: Finite model building constraint generation
% 5.59/1.11 % (253138)Time elapsed: 0.288 s
% 5.59/1.11 % (253138)Peak memory usage: 48 MB
% 5.59/1.11 % (253138)Instructions burned: 715 (million)
% 5.59/1.11 % (253150)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1582757961:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 5.59/1.11 % (253140)Instruction limit reached!
% 5.59/1.11 % (253140)------------------------------
% 5.59/1.11 % (253140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.59/1.11 % (253140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.11 % (253140)CaDiCaL version: 2.1.3
% 5.59/1.11 % (253140)Termination reason: Instruction limit
% 5.59/1.11 % (253140)Termination phase: Saturation
% 5.59/1.11 % (253140)Time elapsed: 0.315 s
% 5.59/1.11 % (253140)Peak memory usage: 18 MB
% 5.59/1.11 % (253140)Instructions burned: 685 (million)
% 5.59/1.11 % (253152)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4018534102:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 5.59/1.11 % TRYING [3]
% 5.59/1.11 % (253146)Instruction limit reached!
% 5.59/1.11 % (253146)------------------------------
% 5.59/1.11 % (253146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.59/1.11 % (253146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.11 % (253146)CaDiCaL version: 2.1.3
% 5.59/1.11 % (253146)Termination reason: Instruction limit
% 5.59/1.11 % (253146)Termination phase: Saturation
% 5.59/1.11 % (253146)Time elapsed: 0.299 s
% 5.59/1.11 % (253146)Peak memory usage: 15 MB
% 5.59/1.11 % (253146)Instructions burned: 478 (million)
% 5.59/1.11 % (253154)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=924017442: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)
% 5.59/1.11 % (253148)Instruction limit reached!
% 5.59/1.11 % (253148)------------------------------
% 5.59/1.11 % (253148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.59/1.11 % (253148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.11 % (253148)CaDiCaL version: 2.1.3
% 5.59/1.11 % (253148)Termination reason: Instruction limit
% 5.59/1.11 % (253148)Termination phase: Finite model building constraint generation
% 5.59/1.11 % (253148)Time elapsed: 0.381 s
% 5.59/1.11 % (253148)Peak memory usage: 45 MB
% 5.59/1.11 % (253148)Instructions burned: 866 (million)
% 5.59/1.11 % (253156)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=807614396:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 5.59/1.11 % (253150) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-253119-253150"...
% 5.59/1.11 % (253150)...printing done.
% 5.59/1.11 % (253150)Refutation found. Thanks to Tanya!
% 5.59/1.11 % SZS status Unsatisfiable for theBenchmark
% 5.59/1.11 % SZS output start Proof for theBenchmark
% See solution above
% 5.59/1.12 % (253150)------------------------------
% 5.59/1.12 % (253150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.59/1.12 % (253150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.12 % (253150)CaDiCaL version: 2.1.3
% 5.59/1.12 % (253150)Termination reason: Refutation
% 5.59/1.12 % (253150)Time elapsed: 0.403 s
% 5.59/1.12 % (253150)Peak memory usage: 20 MB
% 5.59/1.12 % (253150)Instructions burned: 637 (million)
% 5.59/1.12 % (253119)Success in time 0.895 s
% 5.59/1.12 % Vampire exiting
%------------------------------------------------------------------------------