%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SET020-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:42:40 PM UTC 2026
% Result : Unsatisfiable 35.64s 6.33s
% Output : Refutation 35.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 13
% Syntax : Number of formulae : 41 ( 29 unt; 6 def)
% Number of atoms : 57 ( 37 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 39 ( 23 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-2 aty)
% Number of variables : 36 ( 36 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',singleton_set) ).
fof(f13,axiom,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',ordered_pair) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',cartesian_product1) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ordered_pair(first(X0),second(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',cartesian_product4) ).
fof(f172,axiom,
! [X2,X3,X0,X1] :
( ordered_pair(X0,X1) != ordered_pair(X2,X3)
| ~ member(X0,universal_class)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair_determines_components1) ).
fof(f179,negated_conjecture,
member(ordered_pair(u,v),cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_unique_1st_and_2nd_in_pair_of_sets1_1) ).
fof(f180,negated_conjecture,
first(ordered_pair(u,v)) != u,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_unique_1st_and_2nd_in_pair_of_sets1_2) ).
fof(f181,plain,
u != first(ordered_pair(u,v)),
inference(reorient_equations,[],[f180]) ).
fof(f186,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),
inference(definition_unfolding,[],[f13,f12,f12]) ).
fof(f193,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X0,X2) ),
inference(definition_unfolding,[],[f14,f186]) ).
fof(f196,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ),
inference(definition_unfolding,[],[f17,f186]) ).
fof(f270,plain,
! [X2,X3,X0,X1] :
( unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))) != unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X3,X3)))
| ~ member(X0,universal_class)
| X0 = X2 ),
inference(definition_unfolding,[],[f172,f186,f186]) ).
fof(f277,plain,
member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v))),cross_product(universal_class,universal_class)),
inference(definition_unfolding,[],[f179,f186]) ).
fof(f278,plain,
u != first(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(v,v)))),
inference(definition_unfolding,[],[f181,f186]) ).
fof(f282,definition,
sF0 = unordered_pair(u,u),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f283,plain,
unordered_pair(u,u) = sF0,
inference(reorient_equations,[],[f282]) ).
fof(f284,definition,
sF1 = unordered_pair(v,v),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f285,plain,
unordered_pair(v,v) = sF1,
inference(reorient_equations,[],[f284]) ).
fof(f286,definition,
sF2 = unordered_pair(u,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f287,plain,
unordered_pair(u,sF1) = sF2,
inference(reorient_equations,[],[f286]) ).
fof(f288,definition,
sF3 = unordered_pair(sF0,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f289,plain,
unordered_pair(sF0,sF2) = sF3,
inference(reorient_equations,[],[f288]) ).
fof(f290,definition,
sF4 = cross_product(universal_class,universal_class),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f291,plain,
cross_product(universal_class,universal_class) = sF4,
inference(reorient_equations,[],[f290]) ).
fof(f292,plain,
member(sF3,sF4),
inference(definition_folding,[],[f277,f291,f289,f287,f285,f283]) ).
fof(f293,definition,
sF5 = first(sF3),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f294,plain,
first(sF3) = sF5,
inference(reorient_equations,[],[f293]) ).
fof(f295,plain,
u != sF5,
inference(definition_folding,[],[f278,f294,f289,f287,f285,f283]) ).
fof(f1014,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF4)
| member(X0,universal_class) ),
inference(superposition,[],[f193,f291]) ).
fof(f1340,plain,
! [X0] :
( ~ member(X0,sF4)
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ),
inference(superposition,[],[f196,f291]) ).
fof(f1637,plain,
! [X2,X0,X1] :
( unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))) != unordered_pair(sF0,unordered_pair(u,unordered_pair(X2,X2)))
| ~ member(X0,universal_class)
| u = X0 ),
inference(superposition,[],[f270,f283]) ).
fof(f19764,plain,
sF3 = unordered_pair(unordered_pair(first(sF3),first(sF3)),unordered_pair(first(sF3),unordered_pair(second(sF3),second(sF3)))),
inference(resolution,[],[f1340,f292]) ).
fof(f19767,plain,
sF3 = unordered_pair(unordered_pair(sF5,sF5),unordered_pair(sF5,unordered_pair(second(sF3),second(sF3)))),
inference(forward_demodulation,[],[f19764,f294]) ).
fof(f28501,plain,
( ~ member(sF3,sF4)
| member(sF5,universal_class) ),
inference(superposition,[],[f1014,f19767]) ).
fof(f28627,plain,
member(sF5,universal_class),
inference(forward_subsumption_resolution,[],[f28501,f292]) ).
fof(f31686,plain,
! [X0] :
( sF3 != unordered_pair(sF0,unordered_pair(u,unordered_pair(X0,X0)))
| ~ member(sF5,universal_class)
| u = sF5 ),
inference(superposition,[],[f1637,f19767]) ).
fof(f31729,plain,
! [X0] :
( sF3 != unordered_pair(sF0,unordered_pair(u,unordered_pair(X0,X0)))
| u = sF5 ),
inference(forward_subsumption_resolution,[],[f31686,f28627]) ).
fof(f31744,plain,
! [X0] : sF3 != unordered_pair(sF0,unordered_pair(u,unordered_pair(X0,X0))),
inference(forward_subsumption_resolution,[],[f31729,f295]) ).
fof(f47309,plain,
sF3 != unordered_pair(sF0,unordered_pair(u,sF1)),
inference(superposition,[],[f31744,f285]) ).
fof(f47319,plain,
unordered_pair(sF0,sF2) != sF3,
inference(forward_demodulation,[],[f47309,f287]) ).
fof(f47322,plain,
$false,
inference(forward_subsumption_resolution,[],[f47319,f289]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET020-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.34 % Computer : n012.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Mon Sep 28 00:09:04 UTC 2026
% 0.10/0.34 % CPUTime :
% 0.10/0.34 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 Running first-order model finding
% 0.10/0.36 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
% 16.23/2.78 % (2893973)Will run a generic schedule for satisfiability detection.
% 16.23/2.78 % (2893982)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1713629865:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.23/2.78 % (2893979)% WARNING: option uhcvi not known.
% 16.23/2.78 % (2893983)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1765939536:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.23/2.78 % (2893984)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2830155073:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.23/2.78 % (2893978)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2893112584_2999 on theBenchmark for (2999ds/0Mi)
% 16.23/2.78 % (2893980)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4183169752:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.23/2.78 % (2893979)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2150188834:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.23/2.78 % (2893981)dis+10_1_sil=32000:sp=arity:random_seed=2721662427:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.23/2.78 % (2893982)Instruction limit reached!
% 16.23/2.78 % (2893982)------------------------------
% 16.23/2.78 % (2893982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.23/2.78 % (2893982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.23/2.78 % (2893982)CaDiCaL version: 2.1.3
% 16.23/2.78 % (2893982)Termination reason: Instruction limit
% 16.23/2.78 % (2893982)Termination phase: Saturation
% 16.23/2.78 % (2893982)Time elapsed: 0.045 s
% 16.23/2.78 % (2893982)Peak memory usage: 13 MB
% 16.23/2.78 % (2893982)Instructions burned: 116 (million)
% 16.23/2.78 % (2893981)Instruction limit reached!
% 16.23/2.78 % (2893981)------------------------------
% 16.23/2.78 % (2893981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.23/2.78 % (2893981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.23/2.78 % (2893981)CaDiCaL version: 2.1.3
% 16.23/2.78 % (2893981)Termination reason: Instruction limit
% 16.23/2.78 % (2893981)Termination phase: Saturation
% 16.23/2.78 % (2893981)Time elapsed: 0.055 s
% 16.23/2.78 % (2893981)Peak memory usage: 12 MB
% 16.23/2.78 % (2893981)Instructions burned: 104 (million)
% 16.23/2.78 % (2893983)Instruction limit reached!
% 16.23/2.78 % (2893983)------------------------------
% 16.23/2.78 % (2893983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.23/2.78 % (2893983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.23/2.78 % (2893983)CaDiCaL version: 2.1.3
% 16.23/2.78 % (2893983)Termination reason: Instruction limit
% 16.23/2.78 % (2893983)Termination phase: Saturation
% 16.23/2.78 % (2893983)Time elapsed: 0.067 s
% 16.23/2.78 % (2893983)Peak memory usage: 13 MB
% 16.23/2.78 % (2893983)Instructions burned: 131 (million)
% 16.23/2.78 % (2893992)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=745040441:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.23/2.78 % (2893993)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2772078:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 16.23/2.78 % (2893995)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=1086954722:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 16.23/2.78 % (2893984)Instruction limit reached!
% 16.23/2.78 % (2893984)------------------------------
% 16.23/2.78 % (2893984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.23/2.78 % (2893984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.23/2.78 % (2893984)CaDiCaL version: 2.1.3
% 16.23/2.78 % (2893984)Termination reason: Instruction limit
% 16.23/2.78 % (2893984)Termination phase: Saturation
% 16.23/2.78 % (2893984)Time elapsed: 0.089 s
% 16.23/2.78 % (2893984)Peak memory usage: 13 MB
% 16.23/2.78 % (2893984)Instructions burned: 159 (million)
% 16.23/2.78 % (2893998)ott-21_1_sil=16000:fs=off:random_seed=3789614341:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.23/2.78 % (2893993)Instruction limit reached!
% 16.23/2.78 % (2893993)------------------------------
% 16.23/2.78 % (2893993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.23/2.78 % (2893993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.23/2.78 % (2893993)CaDiCaL version: 2.1.3
% 38.89/6.00 % (2893993)Termination reason: Instruction limit
% 38.89/6.00 % (2893993)Termination phase: Saturation
% 38.89/6.00 % (2893993)Time elapsed: 0.079 s
% 38.89/6.00 % (2893993)Peak memory usage: 13 MB
% 38.89/6.00 % (2893993)Instructions burned: 132 (million)
% 38.89/6.00 % (2894000)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4167522268:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 38.89/6.00 % TRYING [1]
% 38.89/6.00 % TRYING [2]
% 38.89/6.00 % (2893998)Instruction limit reached!
% 38.89/6.00 % (2893998)------------------------------
% 38.89/6.00 % (2893998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.89/6.00 % (2893998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.89/6.00 % (2893998)CaDiCaL version: 2.1.3
% 38.89/6.00 % (2893998)Termination reason: Instruction limit
% 38.89/6.00 % (2893998)Termination phase: Saturation
% 38.89/6.00 % (2893998)Time elapsed: 0.089 s
% 38.89/6.00 % (2893998)Peak memory usage: 13 MB
% 38.89/6.00 % (2893998)Instructions burned: 181 (million)
% 38.89/6.00 % TRYING [3]
% 38.89/6.00 % (2894002)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2505773912:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 38.89/6.00 % TRYING [1]
% 38.89/6.00 % TRYING [2]
% 38.89/6.00 % TRYING [3]
% 38.89/6.00 % (2894000)Instruction limit reached!
% 38.89/6.00 % (2894000)------------------------------
% 38.89/6.00 % (2894000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.89/6.00 % (2894000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.89/6.00 % (2894000)CaDiCaL version: 2.1.3
% 38.89/6.00 % (2894000)Termination reason: Instruction limit
% 38.89/6.00 % (2894000)Termination phase: Saturation
% 38.89/6.00 % (2894000)Time elapsed: 0.206 s
% 38.89/6.00 % (2894000)Peak memory usage: 13 MB
% 38.89/6.00 % (2894000)Instructions burned: 477 (million)
% 38.89/6.00 % (2893992)Instruction limit reached!
% 38.89/6.00 % (2893992)------------------------------
% 38.89/6.00 % (2893992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.89/6.00 % (2893992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.89/6.00 % (2893992)CaDiCaL version: 2.1.3
% 38.89/6.00 % (2893992)Termination reason: Instruction limit
% 38.89/6.00 % (2893992)Termination phase: Finite model building constraint generation
% 38.89/6.00 % (2893992)Time elapsed: 0.316 s
% 38.89/6.00 % (2893992)Peak memory usage: 34 MB
% 38.89/6.00 % (2893992)Instructions burned: 714 (million)
% 38.89/6.00 % (2894004)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2328869712:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 38.89/6.00 % (2893995)Instruction limit reached!
% 38.89/6.00 % (2893995)------------------------------
% 38.89/6.00 % (2893995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.89/6.00 % (2893995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.89/6.00 % (2893995)CaDiCaL version: 2.1.3
% 38.89/6.00 % (2893995)Termination reason: Instruction limit
% 38.89/6.00 % (2893995)Termination phase: Saturation
% 38.89/6.00 % (2893995)Time elapsed: 0.304 s
% 38.89/6.00 % (2893995)Peak memory usage: 16 MB
% 38.89/6.00 % (2893995)Instructions burned: 685 (million)
% 38.89/6.00 % TRYING [4]
% 38.89/6.00 % TRYING [1]
% 38.89/6.00 % TRYING [2]
% 38.89/6.00 % (2894006)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1289410677:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 38.89/6.00 % (2894007)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=2362247563:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 38.89/6.00 % TRYING [3]
% 38.89/6.00 % (2894002)Instruction limit reached!
% 38.89/6.00 % (2894002)------------------------------
% 38.89/6.00 % (2894002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.89/6.00 % (2894002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.89/6.00 % (2894002)CaDiCaL version: 2.1.3
% 38.89/6.00 % (2894002)Termination reason: Instruction limit
% 38.89/6.00 % (2894002)Termination phase: Finite model building constraint generation
% 38.89/6.00 % (2894002)Time elapsed: 0.378 s
% 38.89/6.00 % (2894002)Peak memory usage: 28 MB
% 38.89/6.00 % (2894002)Instructions burned: 866 (million)
% 38.89/6.00 % (2894010)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4193771486:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 38.89/6.00 % (2894007)Instruction limit reached!
% 38.89/6.00 % (2894007)------------------------------
% 38.89/6.00 % (2894007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.64/6.33 % (2894007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.64/6.33 % (2894007)CaDiCaL version: 2.1.3
% 35.64/6.33 % (2894007)Termination reason: Instruction limit
% 35.64/6.33 % (2894007)Termination phase: Saturation
% 35.64/6.33 % (2894007)Time elapsed: 0.352 s
% 35.64/6.33 % (2894007)Peak memory usage: 18 MB
% 35.64/6.33 % (2894007)Instructions burned: 694 (million)
% 35.64/6.33 % (2894012)fmb+10_1_sil=64000:random_seed=4049049686:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 35.64/6.33 % (2894006)Instruction limit reached!
% 35.64/6.33 % (2894006)------------------------------
% 35.64/6.33 % (2894006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.64/6.33 % (2894006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.64/6.33 % (2894006)CaDiCaL version: 2.1.3
% 35.64/6.33 % (2894006)Termination reason: Instruction limit
% 35.64/6.33 % (2894006)Termination phase: Finite model building constraint generation
% 35.64/6.33 % (2894006)Time elapsed: 0.408 s
% 35.64/6.33 % (2894006)Peak memory usage: 77 MB
% 35.64/6.33 % (2894006)Instructions burned: 889 (million)
% 35.64/6.33 % (2894014)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2177481505:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 35.64/6.33 % (2894004)Instruction limit reached!
% 35.64/6.33 % (2894004)------------------------------
% 35.64/6.33 % (2894004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.64/6.33 % (2894004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.64/6.33 % (2894004)CaDiCaL version: 2.1.3
% 35.64/6.33 % (2894004)Termination reason: Instruction limit
% 35.64/6.33 % (2894004)Termination phase: Saturation
% 35.64/6.33 % (2894004)Time elapsed: 0.546 s
% 35.64/6.33 % (2894004)Peak memory usage: 20 MB
% 35.64/6.33 % (2894004)Instructions burned: 1180 (million)
% 35.64/6.33 % TRYING [20]
% 35.64/6.33 % TRYING [1]
% 35.64/6.33 % TRYING [2]
% 35.64/6.33 % (2894016)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2311703548:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 35.64/6.33 % (2894010)Instruction limit reached!
% 35.64/6.33 % (2894010)------------------------------
% 35.64/6.33 % (2894010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.64/6.33 % (2894010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.64/6.33 % (2894010)CaDiCaL version: 2.1.3
% 35.64/6.33 % (2894010)Termination reason: Instruction limit
% 35.64/6.33 % (2894010)Termination phase: Saturation
% 35.64/6.33 % (2894010)Time elapsed: 0.445 s
% 35.64/6.33 % (2894010)Peak memory usage: 19 MB
% 35.64/6.33 % (2894010)Instructions burned: 879 (million)
% 35.64/6.33 % TRYING [3]
% 35.64/6.33 % (2894018)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=867488619:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 35.64/6.33 % TRYING [8]
% 35.64/6.33 % TRYING [5]
% 35.64/6.33 % (2894016)Instruction limit reached!
% 35.64/6.33 % (2894016)------------------------------
% 35.64/6.33 % (2894016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.64/6.33 % (2894016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.64/6.33 % (2894016)CaDiCaL version: 2.1.3
% 35.64/6.33 % (2894016)Termination reason: Instruction limit
% 35.64/6.33 % (2894016)Termination phase: Finite model building constraint generation
% 35.64/6.33 % (2894016)Time elapsed: 0.372 s
% 35.64/6.33 % (2894016)Peak memory usage: 45 MB
% 35.64/6.33 % (2894016)Instructions burned: 922 (million)
% 35.64/6.33 % (2894020)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2674212648:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 35.64/6.33 % TRYING [4]
% 35.64/6.33 % (2894020)Instruction limit reached!
% 35.64/6.33 % (2894020)------------------------------
% 35.64/6.33 % (2894020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.64/6.33 % (2894020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.64/6.33 % (2894020)CaDiCaL version: 2.1.3
% 35.64/6.33 % (2894020)Termination reason: Instruction limit
% 35.64/6.33 % (2894020)Termination phase: Saturation
% 35.64/6.33 % (2894020)Time elapsed: 0.801 s
% 35.64/6.33 % (2894020)Peak memory usage: 31 MB
% 35.64/6.33 % (2894020)Instructions burned: 1474 (million)
% 35.64/6.33 % (2894024)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2913675790:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 35.64/6.33 % (2894024)Cannot represent all propositional literals internally
% 35.64/6.33 % (2894024)Refutation not found, incomplete strategy
% 35.64/6.33 % (2894024)------------------------------
% 35.64/6.33 % (2894024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.64/6.33 % (2894024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.64/6.33 % (2894024)CaDiCaL version: 2.1.3
% 35.64/6.33 % (2894024)Termination reason: Refutation not found, incomplete strategy
% 35.64/6.33 % (2894024)Time elapsed: 0.180 s
% 35.64/6.33 % (2894024)Peak memory usage: 13 MB
% 35.64/6.33 % (2894024)Instructions burned: 380 (million)
% 35.64/6.33 % (2894024)------------------------------
% 35.64/6.33 % (2894024)------------------------------
% 35.64/6.33 % (2894026)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=553698858:fmbsr=2.30978:i=2174_2975 on theBenchmark for (2975ds/2174Mi)
% 35.64/6.33 % (2894026)Cannot represent all propositional literals internally
% 35.64/6.33 % (2894026)Refutation not found, incomplete strategy
% 35.64/6.33 % (2894026)------------------------------
% 35.64/6.33 % (2894026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.64/6.33 % (2894026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.64/6.33 % (2894026)CaDiCaL version: 2.1.3
% 35.64/6.33 % (2894026)Termination reason: Refutation not found, incomplete strategy
% 35.64/6.33 % (2894026)Time elapsed: 0.843 s
% 35.64/6.33 % (2894026)Peak memory usage: 18 MB
% 35.64/6.33 % (2894026)Instructions burned: 1940 (million)
% 35.64/6.33 % (2894026)------------------------------
% 35.64/6.33 % (2894026)------------------------------
% 35.64/6.33 % (2894030)ott-2_1_sil=16000:newcnf=on:random_seed=2557536331:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2967 on theBenchmark for (2967ds/869Mi)
% 35.64/6.33 % (2894018)Instruction limit reached!
% 35.64/6.33 % (2894018)------------------------------
% 35.64/6.33 % (2894018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.64/6.33 % (2894018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.64/6.33 % (2894018)CaDiCaL version: 2.1.3
% 35.64/6.33 % (2894018)Termination reason: Instruction limit
% 35.64/6.33 % (2894018)Termination phase: Saturation
% 35.64/6.33 % (2894018)Time elapsed: 2.463 s
% 35.64/6.33 % (2894018)Peak memory usage: 32 MB
% 35.64/6.33 % (2894018)Instructions burned: 5133 (million)
% 35.64/6.33 % (2894032)ott+10_1_sil=32000:tgt=ground:random_seed=3611345344:i=5114:av=off_2964 on theBenchmark for (2964ds/5114Mi)
% 35.64/6.33 % (2894030)Instruction limit reached!
% 35.64/6.33 % (2894030)------------------------------
% 35.64/6.33 % (2894030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.64/6.33 % (2894030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.64/6.33 % (2894030)CaDiCaL version: 2.1.3
% 35.64/6.33 % (2894030)Termination reason: Instruction limit
% 35.64/6.33 % (2894030)Termination phase: Saturation
% 35.64/6.33 % (2894030)Time elapsed: 0.405 s
% 35.64/6.33 % (2894030)Peak memory usage: 15 MB
% 35.64/6.33 % (2894030)Instructions burned: 870 (million)
% 35.64/6.33 % (2894034)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2096389099:i=54282_2963 on theBenchmark for (2963ds/54282Mi)
% 35.64/6.33 % TRYING [1]
% 35.64/6.33 % TRYING [2]
% 35.64/6.33 % TRYING [3]
% 35.64/6.33 % (2894014)Instruction limit reached!
% 35.64/6.33 % (2894014)------------------------------
% 35.64/6.33 % (2894014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.64/6.33 % (2894014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.64/6.33 % (2894014)CaDiCaL version: 2.1.3
% 35.64/6.33 % (2894014)Termination reason: Instruction limit
% 35.64/6.33 % (2894014)Termination phase: Finite model building constraint generation
% 35.64/6.33 % (2894014)Time elapsed: 3.109 s
% 35.64/6.33 % (2894014)Peak memory usage: 647 MB
% 35.64/6.33 % (2894014)Instructions burned: 9515 (million)
% 35.64/6.33 % (2894036)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=95627014:i=3512:aac=none_2959 on theBenchmark for (2959ds/3512Mi)
% 35.64/6.33 % TRYING [4]
% 35.64/6.33 % TRYING [5]
% 35.64/6.33 % TRYING [6]
% 35.64/6.33 % TRYING [5]
% 35.64/6.33 % (2894036)Instruction limit reached!
% 35.64/6.33 % (2894036)------------------------------
% 35.64/6.33 % (2894036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.64/6.33 % (2894036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.64/6.33 % (2894036)CaDiCaL version: 2.1.3
% 35.64/6.33 % (2894036)Termination reason: Instruction limit
% 35.64/6.33 % (2894036)Termination phase: Saturation
% 35.64/6.33 % (2894036)Time elapsed: 1.572 s
% 35.64/6.33 % (2894036)Peak memory usage: 32 MB
% 35.64/6.33 % (2894036)Instructions burned: 3517 (million)
% 35.64/6.33 % (2894038)dis+21_1_sil=32000:sas=cadical:random_seed=2584260287:i=3773:amm=off_2943 on theBenchmark for (2943ds/3773Mi)
% 35.64/6.33 % (2894032) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2893973-2894032"...
% 35.64/6.33 % (2894032)...printing done.
% 35.64/6.33 % (2894032)Refutation found. Thanks to Tanya!
% 35.64/6.33 % SZS status Unsatisfiable for theBenchmark
% 35.64/6.33 % SZS output start Proof for theBenchmark
% See solution above
% 35.64/6.33 % (2894032)------------------------------
% 35.64/6.33 % (2894032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.64/6.33 % (2894032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.64/6.33 % (2894032)CaDiCaL version: 2.1.3
% 35.64/6.33 % (2894032)Termination reason: Refutation
% 35.64/6.33 % (2894032)Time elapsed: 2.291 s
% 35.64/6.33 % (2894032)Peak memory usage: 30 MB
% 35.64/6.33 % (2894032)Instructions burned: 4387 (million)
% 35.64/6.33 % (2893973)Success in time 5.962 s
% 35.64/6.33 % Vampire exiting
%------------------------------------------------------------------------------