%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU267+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:52:39 PM UTC 2026
% Result : Theorem 42.04s 6.40s
% Output : Refutation 42.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 7
% Syntax : Number of formulae : 48 ( 13 unt; 2 def)
% Number of atoms : 135 ( 116 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 149 ( 62 ~; 57 |; 14 &)
% ( 8 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 2 con; 0-2 aty)
% Number of variables : 140 ( 0 sgn 122 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0] :
( ? [X1,X2] : X0 = ordered_pair(X1,X2)
=> ! [X1] :
( X1 = pair_first(X0)
<=> ! [X2,X3] :
( X0 = ordered_pair(X2,X3)
=> X1 = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_mcart_1) ).
fof(f36,axiom,
! [X0] :
( ? [X1,X2] : X0 = ordered_pair(X1,X2)
=> ! [X1] :
( X1 = pair_second(X0)
<=> ! [X2,X3] :
( X0 = ordered_pair(X2,X3)
=> X1 = X3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_mcart_1) ).
fof(f60,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f317,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f325,conjecture,
! [X0,X1] :
( pair_first(ordered_pair(X0,X1)) = X0
& pair_second(ordered_pair(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_mcart_1) ).
fof(f326,negated_conjecture,
~ ! [X0,X1] :
( pair_first(ordered_pair(X0,X1)) = X0
& pair_second(ordered_pair(X0,X1)) = X1 ),
inference(negated_conjecture,[status(cth)],[f325]) ).
fof(f344,plain,
! [X0] :
( ? [X1,X2] : X0 = ordered_pair(X1,X2)
=> ! [X3] :
( pair_first(X0) = X3
<=> ! [X4,X5] :
( ordered_pair(X4,X5) = X0
=> X3 = X4 ) ) ),
inference(rectify,[],[f26]) ).
fof(f345,plain,
! [X0] :
( ? [X1,X2] : X0 = ordered_pair(X1,X2)
=> ! [X3] :
( pair_second(X0) = X3
<=> ! [X4,X5] :
( ordered_pair(X4,X5) = X0
=> X3 = X5 ) ) ),
inference(rectify,[],[f36]) ).
fof(f384,plain,
! [X0] :
( ! [X3] :
( pair_first(X0) = X3
<=> ! [X4,X5] :
( X3 = X4
| ordered_pair(X4,X5) != X0 ) )
| ! [X1,X2] : ordered_pair(X1,X2) != X0 ),
inference(ennf_transformation,[],[f344]) ).
fof(f389,plain,
! [X0] :
( ! [X3] :
( pair_second(X0) = X3
<=> ! [X4,X5] :
( X3 = X5
| ordered_pair(X4,X5) != X0 ) )
| ! [X1,X2] : ordered_pair(X1,X2) != X0 ),
inference(ennf_transformation,[],[f345]) ).
fof(f667,plain,
? [X0,X1] :
( pair_first(ordered_pair(X0,X1)) != X0
| pair_second(ordered_pair(X0,X1)) != X1 ),
inference(ennf_transformation,[],[f326]) ).
fof(f724,plain,
! [X0] :
( ! [X3] :
( ( pair_first(X0) = X3
| ? [X4,X5] :
( X3 != X4
& ordered_pair(X4,X5) = X0 ) )
& ( ! [X4,X5] :
( X3 = X4
| ordered_pair(X4,X5) != X0 )
| pair_first(X0) != X3 ) )
| ! [X1,X2] : ordered_pair(X1,X2) != X0 ),
inference(nnf_transformation,[],[f384]) ).
fof(f725,plain,
! [X0] :
( ! [X1] :
( ( pair_first(X0) = X1
| ? [X2,X3] :
( X1 != X2
& ordered_pair(X2,X3) = X0 ) )
& ( ! [X4,X5] :
( X1 = X4
| ordered_pair(X4,X5) != X0 )
| pair_first(X0) != X1 ) )
| ! [X6,X7] : ordered_pair(X6,X7) != X0 ),
inference(rectify,[],[f724]) ).
fof(f726,plain,
! [X0] :
( ! [X1] :
( ( pair_first(X0) = X1
| ( sK20(X0,X1) != X1
& ordered_pair(sK20(X0,X1),sK21(X0,X1)) = X0 ) )
& ( ! [X4,X5] :
( X1 = X4
| ordered_pair(X4,X5) != X0 )
| pair_first(X0) != X1 ) )
| ! [X6,X7] : ordered_pair(X6,X7) != X0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21]),skolemize(X2,sK20(X0,X1)),skolemize(X3,sK21(X0,X1))],[f725]) ).
fof(f750,plain,
! [X0] :
( ! [X3] :
( ( pair_second(X0) = X3
| ? [X4,X5] :
( X3 != X5
& ordered_pair(X4,X5) = X0 ) )
& ( ! [X4,X5] :
( X3 = X5
| ordered_pair(X4,X5) != X0 )
| pair_second(X0) != X3 ) )
| ! [X1,X2] : ordered_pair(X1,X2) != X0 ),
inference(nnf_transformation,[],[f389]) ).
fof(f751,plain,
! [X0] :
( ! [X1] :
( ( pair_second(X0) = X1
| ? [X2,X3] :
( X1 != X3
& ordered_pair(X2,X3) = X0 ) )
& ( ! [X4,X5] :
( X1 = X5
| ordered_pair(X4,X5) != X0 )
| pair_second(X0) != X1 ) )
| ! [X6,X7] : ordered_pair(X6,X7) != X0 ),
inference(rectify,[],[f750]) ).
fof(f752,plain,
! [X0] :
( ! [X1] :
( ( pair_second(X0) = X1
| ( sK34(X0,X1) != X1
& ordered_pair(sK33(X0,X1),sK34(X0,X1)) = X0 ) )
& ( ! [X4,X5] :
( X1 = X5
| ordered_pair(X4,X5) != X0 )
| pair_second(X0) != X1 ) )
| ! [X6,X7] : ordered_pair(X6,X7) != X0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33,sK34]),skolemize(X2,sK33(X0,X1)),skolemize(X3,sK34(X0,X1))],[f751]) ).
fof(f945,plain,
( sK132 != pair_first(ordered_pair(sK132,sK133))
| sK133 != pair_second(ordered_pair(sK132,sK133)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK132,sK133]),skolemize(X0,sK132),skolemize(X1,sK133)],[f667]) ).
fof(f1033,plain,
! [X0,X1,X6,X7,X4,X5] :
( X1 = X4
| ordered_pair(X4,X5) != X0
| pair_first(X0) != X1
| ordered_pair(X6,X7) != X0 ),
inference(cnf_transformation,[],[f726]) ).
fof(f1069,plain,
! [X0,X1,X6,X7,X4,X5] :
( X1 = X5
| ordered_pair(X4,X5) != X0
| pair_second(X0) != X1
| ordered_pair(X6,X7) != X0 ),
inference(cnf_transformation,[],[f752]) ).
fof(f1178,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f60]) ).
fof(f1611,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f317]) ).
fof(f1622,plain,
( sK132 != pair_first(ordered_pair(sK132,sK133))
| sK133 != pair_second(ordered_pair(sK132,sK133)) ),
inference(cnf_transformation,[],[f945]) ).
fof(f1651,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),
inference(definition_unfolding,[],[f1178,f1611]) ).
fof(f1681,plain,
! [X0,X1,X6,X7,X4,X5] :
( X1 = X4
| unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4)) != X0
| pair_first(X0) != X1
| unordered_pair(unordered_pair(X6,X7),unordered_pair(X6,X6)) != X0 ),
inference(definition_unfolding,[],[f1033,f1651,f1651]) ).
fof(f1696,plain,
! [X0,X1,X6,X7,X4,X5] :
( X1 = X5
| unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4)) != X0
| pair_second(X0) != X1
| unordered_pair(unordered_pair(X6,X7),unordered_pair(X6,X6)) != X0 ),
inference(definition_unfolding,[],[f1069,f1651,f1651]) ).
fof(f1839,plain,
( sK132 != pair_first(unordered_pair(unordered_pair(sK132,sK133),unordered_pair(sK132,sK132)))
| sK133 != pair_second(unordered_pair(unordered_pair(sK132,sK133),unordered_pair(sK132,sK132))) ),
inference(definition_unfolding,[],[f1622,f1651,f1651]) ).
fof(f1881,plain,
! [X1,X6,X7,X4,X5] :
( X1 = X4
| pair_first(unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4))) != X1
| unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4)) != unordered_pair(unordered_pair(X6,X7),unordered_pair(X6,X6)) ),
inference(equality_resolution,[],[f1681]) ).
fof(f1882,plain,
! [X6,X7,X4,X5] :
( unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4)) != unordered_pair(unordered_pair(X6,X7),unordered_pair(X6,X6))
| pair_first(unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4))) = X4 ),
inference(equality_resolution,[],[f1881]) ).
fof(f1902,plain,
! [X1,X6,X7,X4,X5] :
( X1 = X5
| pair_second(unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4))) != X1
| unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4)) != unordered_pair(unordered_pair(X6,X7),unordered_pair(X6,X6)) ),
inference(equality_resolution,[],[f1696]) ).
fof(f1903,plain,
! [X6,X7,X4,X5] :
( unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4)) != unordered_pair(unordered_pair(X6,X7),unordered_pair(X6,X6))
| pair_second(unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4))) = X5 ),
inference(equality_resolution,[],[f1902]) ).
fof(f1970,definition,
( spl137_1
<=> sK133 = pair_second(unordered_pair(unordered_pair(sK132,sK133),unordered_pair(sK132,sK132))) ),
introduced(definition,[new_symbols(definition,[spl137_1])],[avatar_definition]) ).
fof(f1971,plain,
( sK133 != pair_second(unordered_pair(unordered_pair(sK132,sK133),unordered_pair(sK132,sK132)))
| spl137_1 ),
inference(avatar_component_clause,[],[f1970]) ).
fof(f1973,definition,
( spl137_2
<=> sK132 = pair_first(unordered_pair(unordered_pair(sK132,sK133),unordered_pair(sK132,sK132))) ),
introduced(definition,[new_symbols(definition,[spl137_2])],[avatar_definition]) ).
fof(f1974,plain,
( sK132 != pair_first(unordered_pair(unordered_pair(sK132,sK133),unordered_pair(sK132,sK132)))
| spl137_2 ),
inference(avatar_component_clause,[],[f1973]) ).
fof(f1975,plain,
( ~ spl137_1
| ~ spl137_2 ),
inference(avatar_split_clause,[],[f1839,f1973,f1970]) ).
fof(f15633,plain,
! [X0,X1] : pair_first(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0))) = X0,
inference(equality_resolution,[],[f1882]) ).
fof(f15682,plain,
! [X0,X1] : pair_second(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0))) = X1,
inference(equality_resolution,[],[f1903]) ).
fof(f45667,plain,
( sK133 != sK133
| spl137_1 ),
inference(superposition,[],[f1971,f15682]) ).
fof(f45668,plain,
( $false
| spl137_1 ),
inference(trivial_inequality_removal,[],[f45667]) ).
fof(f45669,plain,
spl137_1,
inference(avatar_contradiction_clause,[],[f45668]) ).
fof(f45676,plain,
( $false
| spl137_2 ),
inference(forward_subsumption_resolution,[],[f1974,f15633]) ).
fof(f45677,plain,
spl137_2,
inference(avatar_contradiction_clause,[],[f45676]) ).
cnf(s1,plain,
( ~ spl137_1
| ~ spl137_2 ),
inference(sat_conversion,[],[f1975]) ).
cnf(s1196,plain,
spl137_1,
inference(sat_conversion,[],[f45669]) ).
cnf(s1198,plain,
spl137_2,
inference(sat_conversion,[],[f45677]) ).
cnf(s1387,plain,
$false,
inference(rat,[],[s1,s1198,s1196]) ).
fof(f45678,plain,
$false,
inference(avatar_sat_refutation,[],[s1387]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU267+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 % Computer : n017.cluster.edu
% 0.10/0.41 % Model : x86_64 x86_64
% 0.10/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.41 % Memory : 8046.5625MB
% 0.10/0.41 % OS : Linux 6.8.0-71-generic
% 0.10/0.41 % CPULimit : 300
% 0.10/0.41 % WCLimit : 300
% 0.10/0.41 % DateTime : Mon Sep 28 04:19:36 UTC 2026
% 0.10/0.41 % CPUTime :
% 0.10/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.44 Running first-order model finding
% 0.10/0.44 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.51/2.81 % (3196920)Will run a generic schedule for satisfiability detection.
% 16.51/2.81 % (3196929)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=628226771:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.51/2.81 % (3196926)% WARNING: option uhcvi not known.
% 16.51/2.81 % (3196928)dis+10_1_sil=32000:sp=arity:random_seed=625361385:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.51/2.81 % (3196925)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2457164509_2999 on theBenchmark for (2999ds/0Mi)
% 16.51/2.81 % (3196926)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3848458826:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.51/2.81 % (3196927)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=400032805:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.51/2.81 % (3196930)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1239856000:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.51/2.81 % (3196931)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2663742144:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.51/2.81 % (3196929)Instruction limit reached!
% 16.51/2.81 % (3196929)------------------------------
% 16.51/2.81 % (3196929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.51/2.81 % (3196929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.51/2.81 % (3196929)CaDiCaL version: 2.1.3
% 16.51/2.81 % (3196929)Termination reason: Instruction limit
% 16.51/2.81 % (3196929)Termination phase: Saturation
% 16.51/2.81 % (3196929)Time elapsed: 0.039 s
% 16.51/2.81 % (3196929)Peak memory usage: 14 MB
% 16.51/2.81 % (3196929)Instructions burned: 117 (million)
% 16.51/2.81 % (3196939)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1845185779:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.51/2.81 % (3196928)Instruction limit reached!
% 16.51/2.81 % (3196928)------------------------------
% 16.51/2.81 % (3196928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.51/2.81 % (3196928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.51/2.81 % (3196928)CaDiCaL version: 2.1.3
% 16.51/2.81 % (3196928)Termination reason: Instruction limit
% 16.51/2.81 % (3196928)Termination phase: Saturation
% 16.51/2.81 % (3196928)Time elapsed: 0.068 s
% 16.51/2.81 % (3196928)Peak memory usage: 13 MB
% 16.51/2.81 % (3196928)Instructions burned: 104 (million)
% 16.51/2.81 % (3196930)Instruction limit reached!
% 16.51/2.81 % (3196930)------------------------------
% 16.51/2.81 % (3196930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.51/2.81 % (3196930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.51/2.81 % (3196930)CaDiCaL version: 2.1.3
% 16.51/2.81 % (3196930)Termination reason: Instruction limit
% 16.51/2.81 % (3196930)Termination phase: Saturation
% 16.51/2.81 % (3196930)Time elapsed: 0.075 s
% 16.51/2.81 % (3196930)Peak memory usage: 14 MB
% 16.51/2.81 % (3196930)Instructions burned: 132 (million)
% 16.51/2.81 % TRYING [1]
% 16.51/2.81 % TRYING [2]
% 16.51/2.81 % TRYING [1]
% 16.51/2.81 % TRYING [2]
% 16.51/2.81 % (3196941)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1219092659:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.51/2.81 % (3196942)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=539275406:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.51/2.81 % TRYING [3]
% 16.51/2.81 % (3196931)Instruction limit reached!
% 16.51/2.81 % (3196931)------------------------------
% 16.51/2.81 % (3196931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.51/2.81 % (3196931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.51/2.81 % (3196931)CaDiCaL version: 2.1.3
% 16.51/2.81 % (3196931)Termination reason: Instruction limit
% 16.51/2.81 % (3196931)Termination phase: Saturation
% 16.51/2.81 % (3196931)Time elapsed: 0.100 s
% 16.51/2.81 % (3196931)Peak memory usage: 15 MB
% 16.51/2.81 % (3196931)Instructions burned: 160 (million)
% 16.51/2.81 % (3196945)ott-21_1_sil=16000:fs=off:random_seed=258606471:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.51/2.81 % TRYING [3]
% 16.51/2.81 % (3196941)Instruction limit reached!
% 16.51/2.81 % (3196941)------------------------------
% 16.51/2.81 % (3196941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.51/2.81 % (3196941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196941)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196941)Termination reason: Instruction limit
% 42.04/6.40 % (3196941)Termination phase: Saturation
% 42.04/6.40 % (3196941)Time elapsed: 0.075 s
% 42.04/6.40 % (3196941)Peak memory usage: 14 MB
% 42.04/6.40 % (3196941)Instructions burned: 133 (million)
% 42.04/6.40 % (3196947)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=569688840:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 42.04/6.40 % TRYING [4]
% 42.04/6.40 % (3196939)Instruction limit reached!
% 42.04/6.40 % (3196939)------------------------------
% 42.04/6.40 % (3196939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196939)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196939)Termination reason: Instruction limit
% 42.04/6.40 % (3196939)Termination phase: Finite model building constraint generation
% 42.04/6.40 % (3196939)Time elapsed: 0.160 s
% 42.04/6.40 % (3196939)Peak memory usage: 39 MB
% 42.04/6.40 % (3196939)Instructions burned: 719 (million)
% 42.04/6.40 % (3196945)Instruction limit reached!
% 42.04/6.40 % (3196945)------------------------------
% 42.04/6.40 % (3196945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196945)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196945)Termination reason: Instruction limit
% 42.04/6.40 % (3196945)Termination phase: Saturation
% 42.04/6.40 % (3196945)Time elapsed: 0.090 s
% 42.04/6.40 % (3196945)Peak memory usage: 14 MB
% 42.04/6.40 % (3196945)Instructions burned: 181 (million)
% 42.04/6.40 % (3196949)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1271443224:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 42.04/6.40 % (3196950)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2215732350:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 42.04/6.40 % TRYING [1]
% 42.04/6.40 % TRYING [2]
% 42.04/6.40 % TRYING [3]
% 42.04/6.40 % TRYING [4]
% 42.04/6.40 % (3196949)Instruction limit reached!
% 42.04/6.40 % (3196949)------------------------------
% 42.04/6.40 % (3196949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196949)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196949)Termination reason: Instruction limit
% 42.04/6.40 % (3196949)Termination phase: Finite model building SAT solving
% 42.04/6.40 % (3196949)Time elapsed: 0.210 s
% 42.04/6.40 % (3196949)Peak memory usage: 46 MB
% 42.04/6.40 % (3196949)Instructions burned: 869 (million)
% 42.04/6.40 % (3196953)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3975906895:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 42.04/6.40 % (3196942)Instruction limit reached!
% 42.04/6.40 % (3196942)------------------------------
% 42.04/6.40 % (3196942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196942)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196942)Termination reason: Instruction limit
% 42.04/6.40 % (3196942)Termination phase: Saturation
% 42.04/6.40 % (3196942)Time elapsed: 0.360 s
% 42.04/6.40 % (3196942)Peak memory usage: 18 MB
% 42.04/6.40 % (3196942)Instructions burned: 684 (million)
% 42.04/6.40 % (3196955)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=2346325858: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)
% 42.04/6.40 % (3196947)Instruction limit reached!
% 42.04/6.40 % (3196947)------------------------------
% 42.04/6.40 % (3196947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196947)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196947)Termination reason: Instruction limit
% 42.04/6.40 % (3196947)Termination phase: Saturation
% 42.04/6.40 % (3196947)Time elapsed: 0.335 s
% 42.04/6.40 % (3196947)Peak memory usage: 15 MB
% 42.04/6.40 % (3196947)Instructions burned: 478 (million)
% 42.04/6.40 % (3196957)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2894974727:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 42.04/6.40 % (3196953)Instruction limit reached!
% 42.04/6.40 % (3196953)------------------------------
% 42.04/6.40 % (3196953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196953)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196953)Termination reason: Instruction limit
% 42.04/6.40 % (3196953)Termination phase: Finite model building constraint generation
% 42.04/6.40 % (3196953)Time elapsed: 0.245 s
% 42.04/6.40 % (3196953)Peak memory usage: 100 MB
% 42.04/6.40 % (3196953)Instructions burned: 894 (million)
% 42.04/6.40 % (3196959)fmb+10_1_sil=64000:random_seed=4196860992:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 42.04/6.40 % TRYING [1]
% 42.04/6.40 % TRYING [2]
% 42.04/6.40 % TRYING [3]
% 42.04/6.40 % (3196955)Instruction limit reached!
% 42.04/6.40 % (3196955)------------------------------
% 42.04/6.40 % (3196955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196955)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196955)Termination reason: Instruction limit
% 42.04/6.40 % (3196955)Termination phase: Saturation
% 42.04/6.40 % (3196955)Time elapsed: 0.400 s
% 42.04/6.40 % (3196955)Peak memory usage: 23 MB
% 42.04/6.40 % (3196955)Instructions burned: 694 (million)
% 42.04/6.40 % (3196961)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4120823722:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 42.04/6.40 % TRYING [20]
% 42.04/6.40 % (3196950)Instruction limit reached!
% 42.04/6.40 % (3196950)------------------------------
% 42.04/6.40 % (3196950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196950)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196950)Termination reason: Instruction limit
% 42.04/6.40 % (3196950)Termination phase: Saturation
% 42.04/6.40 % (3196950)Time elapsed: 0.750 s
% 42.04/6.40 % (3196950)Peak memory usage: 26 MB
% 42.04/6.40 % (3196950)Instructions burned: 1180 (million)
% 42.04/6.40 % (3196963)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3430237358:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 42.04/6.40 % (3196957)Instruction limit reached!
% 42.04/6.40 % (3196957)------------------------------
% 42.04/6.40 % (3196957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196957)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196957)Termination reason: Instruction limit
% 42.04/6.40 % (3196957)Termination phase: Saturation
% 42.04/6.40 % (3196957)Time elapsed: 0.484 s
% 42.04/6.40 % (3196957)Peak memory usage: 21 MB
% 42.04/6.40 % (3196957)Instructions burned: 880 (million)
% 42.04/6.40 % (3196965)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4044838547:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 42.04/6.40 % TRYING [4]
% 42.04/6.40 % TRYING [8]
% 42.04/6.40 % (3196963)Instruction limit reached!
% 42.04/6.40 % (3196963)------------------------------
% 42.04/6.40 % (3196963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196963)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196963)Termination reason: Instruction limit
% 42.04/6.40 % (3196963)Termination phase: Finite model building constraint generation
% 42.04/6.40 % (3196963)Time elapsed: 0.332 s
% 42.04/6.40 % (3196963)Peak memory usage: 59 MB
% 42.04/6.40 % (3196963)Instructions burned: 921 (million)
% 42.04/6.40 % TRYING [5]
% 42.04/6.40 % (3196967)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1564699590:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 42.04/6.40 % TRYING [5]
% 42.04/6.40 % (3196967)Instruction limit reached!
% 42.04/6.40 % (3196967)------------------------------
% 42.04/6.40 % (3196967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196967)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196967)Termination reason: Instruction limit
% 42.04/6.40 % (3196967)Termination phase: Saturation
% 42.04/6.40 % (3196967)Time elapsed: 0.848 s
% 42.04/6.40 % (3196967)Peak memory usage: 33 MB
% 42.04/6.40 % (3196967)Instructions burned: 1474 (million)
% 42.04/6.40 % (3196969)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3144904642:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 42.04/6.40 % (3196969)Cannot represent all propositional literals internally
% 42.04/6.40 % (3196969)Refutation not found, incomplete strategy
% 42.04/6.40 % (3196969)------------------------------
% 42.04/6.40 % (3196969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196969)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196969)Termination reason: Refutation not found, incomplete strategy
% 42.04/6.40 % (3196969)Time elapsed: 0.082 s
% 42.04/6.40 % (3196969)Peak memory usage: 14 MB
% 42.04/6.40 % (3196969)Instructions burned: 166 (million)
% 42.04/6.40 % (3196969)------------------------------
% 42.04/6.40 % (3196969)------------------------------
% 42.04/6.40 % (3196971)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1604342449:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi)
% 42.04/6.40 % TRYING [16]
% 42.04/6.40 % (3196971)Instruction limit reached!
% 42.04/6.40 % (3196971)------------------------------
% 42.04/6.40 % (3196971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196971)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196971)Termination reason: Instruction limit
% 42.04/6.40 % (3196971)Termination phase: Finite model building constraint generation
% 42.04/6.40 % (3196971)Time elapsed: 0.869 s
% 42.04/6.40 % (3196971)Peak memory usage: 97 MB
% 42.04/6.40 % (3196971)Instructions burned: 2180 (million)
% 42.04/6.40 % (3196973)ott-2_1_sil=16000:newcnf=on:random_seed=748666209:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2967 on theBenchmark for (2967ds/869Mi)
% 42.04/6.40 % (3196973)Instruction limit reached!
% 42.04/6.40 % (3196973)------------------------------
% 42.04/6.40 % (3196973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196973)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196973)Termination reason: Instruction limit
% 42.04/6.40 % (3196973)Termination phase: Saturation
% 42.04/6.40 % (3196973)Time elapsed: 0.515 s
% 42.04/6.40 % (3196973)Peak memory usage: 22 MB
% 42.04/6.40 % (3196973)Instructions burned: 871 (million)
% 42.04/6.40 % (3196975)ott+10_1_sil=32000:tgt=ground:random_seed=546646611:i=5114:av=off_2962 on theBenchmark for (2962ds/5114Mi)
% 42.04/6.40 % (3196965)Instruction limit reached!
% 42.04/6.40 % (3196965)------------------------------
% 42.04/6.40 % (3196965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196965)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196965)Termination reason: Instruction limit
% 42.04/6.40 % (3196965)Termination phase: Saturation
% 42.04/6.40 % (3196965)Time elapsed: 3.106 s
% 42.04/6.40 % (3196965)Peak memory usage: 47 MB
% 42.04/6.40 % (3196965)Instructions burned: 5131 (million)
% 42.04/6.40 % (3196977)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3381858043:i=54282_2958 on theBenchmark for (2958ds/54282Mi)
% 42.04/6.40 % TRYING [1]
% 42.04/6.40 % TRYING [2]
% 42.04/6.40 % (3196961)Instruction limit reached!
% 42.04/6.40 % (3196961)------------------------------
% 42.04/6.40 % (3196961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.40 % (3196961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.40 % (3196961)CaDiCaL version: 2.1.3
% 42.04/6.40 % (3196961)Termination reason: Instruction limit
% 42.04/6.40 % (3196961)Termination phase: Finite model building constraint generation
% 42.04/6.40 % (3196961)Time elapsed: 3.408 s
% 42.04/6.40 % (3196961)Peak memory usage: 614 MB
% 42.04/6.40 % (3196961)Instructions burned: 9516 (million)
% 42.04/6.40 % TRYING [3]
% 42.04/6.40 % (3196979)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3835044698:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi)
% 42.04/6.40 % TRYING [4]
% 42.04/6.40 % TRYING [6]
% 42.04/6.40 % TRYING [6]
% 42.04/6.40 % TRYING [5]
% 42.04/6.40 % (3196979) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3196920-3196979"...
% 42.04/6.40 % (3196979)...printing done.
% 42.04/6.40 % (3196979)Refutation found. Thanks to Tanya!
% 42.04/6.40 % SZS status Theorem for theBenchmark
% 42.04/6.40 % SZS output start Proof for theBenchmark
% See solution above
% 42.04/6.41 % (3196979)------------------------------
% 42.04/6.41 % (3196979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.04/6.41 % (3196979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.04/6.41 % (3196979)CaDiCaL version: 2.1.3
% 42.04/6.41 % (3196979)Termination reason: Refutation
% 42.04/6.41 % (3196979)Time elapsed: 1.440 s
% 42.04/6.41 % (3196979)Peak memory usage: 30 MB
% 42.04/6.41 % (3196979)Instructions burned: 2322 (million)
% 42.04/6.41 % (3196920)Success in time 5.95 s
% 42.04/6.41 % Vampire exiting
%------------------------------------------------------------------------------