%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW348+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 : n006.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:51 PM UTC 2026
% Result : Theorem 11.93s 2.10s
% Output : Refutation 11.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 10
% Syntax : Number of formulae : 58 ( 16 unt; 3 def)
% Number of atoms : 119 ( 40 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 108 ( 47 ~; 46 |; 2 &)
% ( 4 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 4 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-3 aty)
% Number of variables : 97 ( 0 sgn 93 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(hAPP(c_Natural_Oevalc(X3),X2),X1))
=> ( hBOOL(hAPP(hAPP(c_Natural_Oevalc(X3),X2),X0))
=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_com__det) ).
fof(f2270,axiom,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Code__Numeral_Ocode__numeral) != c_Code__Numeral_OSuc__code__numeral(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_code__numeral_Osimps_I2_J) ).
fof(f3677,axiom,
! [X0,X1,X2,X3,X4] :
( hBOOL(hAPP(hAPP(X4,X3),X2))
=> hBOOL(hAPP(c_Predicate_ODomainP(X1,X0,X4),X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_DomainP_Ointros) ).
fof(f3678,axiom,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(c_Predicate_ODomainP(X3,X2,X1),X0))
<=> ? [X4] : hBOOL(hAPP(hAPP(X1,X0),X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_DomainP_Oequations) ).
fof(f4767,axiom,
! [X0] : hAPP(c_Code__Numeral_Onat__of,hAPP(c_Code__Numeral_Oof__nat,X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_nat__of__of__nat) ).
fof(f4778,axiom,
! [X0] : c_Code__Numeral_OSuc__code__numeral(X0) = hAPP(c_Code__Numeral_Oof__nat,hAPP(c_Nat_OSuc,hAPP(c_Code__Numeral_Onat__of,X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Suc__code__numeral__def) ).
fof(f5227,conjecture,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),X0),X3))
=> X2 = X3 )
=> X2 = X1 )
=> hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
fof(f5228,negated_conjecture,
~ ! [X0,X1] :
( ! [X2] :
( ! [X3] :
( hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),X0),X3))
=> X2 = X3 )
=> X2 = X1 )
=> hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),X0),X1)) ),
inference(negated_conjecture,[status(cth)],[f5227]) ).
fof(f5423,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(X3),X2),X0))
| ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(X3),X2),X1)) ),
inference(ennf_transformation,[],[f2]) ).
fof(f5424,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(X3),X2),X0))
| ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(X3),X2),X1)) ),
inference(flattening,[],[f5423]) ).
fof(f8521,plain,
! [X0,X1,X2,X3,X4] :
( hBOOL(hAPP(c_Predicate_ODomainP(X1,X0,X4),X3))
| ~ hBOOL(hAPP(hAPP(X4,X3),X2)) ),
inference(ennf_transformation,[],[f3677]) ).
fof(f9442,plain,
? [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),X0),X1))
& ! [X2] :
( X2 = X1
| ? [X3] :
( X2 != X3
& hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),X0),X3)) ) ) ),
inference(ennf_transformation,[],[f5228]) ).
fof(f9444,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(X3),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(X3),X2),X0))
| X0 = X1 ),
inference(cnf_transformation,[],[f5424]) ).
fof(f12681,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Code__Numeral_Ocode__numeral) != c_Code__Numeral_OSuc__code__numeral(X0),
inference(cnf_transformation,[],[f2270]) ).
fof(f14383,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(hAPP(X4,X3),X2))
| hBOOL(hAPP(c_Predicate_ODomainP(X1,X0,X4),X3)) ),
inference(cnf_transformation,[],[f8521]) ).
fof(f14385,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(hAPP(X1,X0),sK328(X0,X1)))
| ~ hBOOL(hAPP(c_Predicate_ODomainP(X3,X2,X1),X0)) ),
inference(cnf_transformation,[],[f3678]) ).
fof(f15953,plain,
! [X0] : hAPP(c_Code__Numeral_Onat__of,hAPP(c_Code__Numeral_Oof__nat,X0)) = X0,
inference(cnf_transformation,[],[f4767]) ).
fof(f15968,plain,
! [X0] : c_Code__Numeral_OSuc__code__numeral(X0) = hAPP(c_Code__Numeral_Oof__nat,hAPP(c_Nat_OSuc,hAPP(c_Code__Numeral_Onat__of,X0))),
inference(cnf_transformation,[],[f4778]) ).
fof(f16472,plain,
! [X2] :
( hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),sK517),sK519(X2)))
| sK518 = X2 ),
inference(cnf_transformation,[],[f9442]) ).
fof(f16473,plain,
! [X2] :
( sK519(X2) != X2
| sK518 = X2 ),
inference(cnf_transformation,[],[f9442]) ).
fof(f16474,plain,
~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),sK517),sK518)),
inference(cnf_transformation,[],[f9442]) ).
fof(f16826,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Code__Numeral_Ocode__numeral) != hAPP(c_Code__Numeral_Oof__nat,hAPP(c_Nat_OSuc,hAPP(c_Code__Numeral_Onat__of,X0))),
inference(definition_unfolding,[],[f12681,f15968]) ).
fof(f17951,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(hAPP(c_Natural_Oevalc(X3),X2),X1))
| hBOOL(hAPP(hAPP(c_Natural_Oevalc(X3),X2),X0))
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f9444]) ).
fof(f21437,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(c_Predicate_ODomainP(X1,X0,X4),X3))
| hBOOL(hAPP(hAPP(X4,X3),X2)) ),
inference(consistent_polarity_flipping,[],[f14383]) ).
fof(f21438,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(X1,X0),sK328(X0,X1)))
| hBOOL(hAPP(c_Predicate_ODomainP(X3,X2,X1),X0)) ),
inference(consistent_polarity_flipping,[],[f14385]) ).
fof(f22694,plain,
hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),sK517),sK518)),
inference(consistent_polarity_flipping,[],[f16474]) ).
fof(f22695,plain,
! [X2] :
( ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),sK517),sK519(X2)))
| sK518 = X2 ),
inference(consistent_polarity_flipping,[],[f16472]) ).
fof(f23683,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Code__Numeral_Ocode__numeral) != hAPP(c_Code__Numeral_Oof__nat,hAPP(c_Nat_OSuc,X0)),
inference(superposition,[],[f16826,f15953]) ).
fof(f52724,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),sK517),X1))
| sK519(X0) = X1
| sK518 = X0 ),
inference(resolution,[],[f17951,f22695]) ).
fof(f53207,plain,
! [X2,X0,X1] :
( sK519(X0) = sK328(sK517,c_Natural_Oevalc(v_c))
| sK518 = X0
| hBOOL(hAPP(c_Predicate_ODomainP(X1,X2,c_Natural_Oevalc(v_c)),sK517)) ),
inference(resolution,[],[f52724,f21438]) ).
fof(f53268,definition,
( spl520_1306
<=> ! [X3] : hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),sK517),X3)) ),
introduced(definition,[new_symbols(definition,[spl520_1306])],[avatar_definition]) ).
fof(f53269,plain,
( ! [X3] : hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),sK517),X3))
| ~ spl520_1306 ),
inference(avatar_component_clause,[],[f53268]) ).
fof(f53318,definition,
( spl520_1319
<=> ! [X2,X1] : hBOOL(hAPP(c_Predicate_ODomainP(X1,X2,c_Natural_Oevalc(v_c)),sK517)) ),
introduced(definition,[new_symbols(definition,[spl520_1319])],[avatar_definition]) ).
fof(f53319,plain,
( ! [X2,X1] : hBOOL(hAPP(c_Predicate_ODomainP(X1,X2,c_Natural_Oevalc(v_c)),sK517))
| ~ spl520_1319 ),
inference(avatar_component_clause,[],[f53318]) ).
fof(f53321,definition,
( spl520_1320
<=> ! [X0] :
( sK519(X0) = sK328(sK517,c_Natural_Oevalc(v_c))
| sK518 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl520_1320])],[avatar_definition]) ).
fof(f53322,plain,
( ! [X0] :
( sK519(X0) = sK328(sK517,c_Natural_Oevalc(v_c))
| sK518 = X0 )
| ~ spl520_1320 ),
inference(avatar_component_clause,[],[f53321]) ).
fof(f53323,plain,
( spl520_1319
| spl520_1320 ),
inference(avatar_split_clause,[],[f53207,f53321,f53318]) ).
fof(f53331,plain,
( ! [X2] : sK518 = X2
| ~ spl520_1306 ),
inference(backward_subsumption_resolution,[],[f22695,f53269]) ).
fof(f54080,plain,
( c_Groups_Ozero__class_Ozero(tc_Code__Numeral_Ocode__numeral) != hAPP(c_Code__Numeral_Oof__nat,sK518)
| ~ spl520_1306 ),
inference(superposition,[],[f23683,f53331]) ).
fof(f61693,plain,
( c_Groups_Ozero__class_Ozero(tc_Code__Numeral_Ocode__numeral) != sK518
| ~ spl520_1306 ),
inference(forward_demodulation,[],[f54080,f53331]) ).
fof(f63332,plain,
( $false
| ~ spl520_1306 ),
inference(forward_subsumption_resolution,[],[f61693,f53331]) ).
fof(f63333,plain,
~ spl520_1306,
inference(avatar_contradiction_clause,[],[f63332]) ).
fof(f64067,plain,
( ! [X0] : hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),sK517),X0))
| ~ spl520_1319 ),
inference(resolution,[],[f53319,f21437]) ).
fof(f64074,plain,
( spl520_1306
| ~ spl520_1319 ),
inference(avatar_split_clause,[],[f64067,f53318,f53268]) ).
fof(f65084,plain,
( ! [X0] :
( sK328(sK517,c_Natural_Oevalc(v_c)) != X0
| sK518 = X0
| sK518 = X0 )
| ~ spl520_1320 ),
inference(superposition,[],[f16473,f53322]) ).
fof(f65086,plain,
( ! [X0] :
( sK328(sK517,c_Natural_Oevalc(v_c)) != X0
| sK518 = X0 )
| ~ spl520_1320 ),
inference(duplicate_literal_removal,[],[f65084]) ).
fof(f65097,plain,
( sK518 = sK328(sK517,c_Natural_Oevalc(v_c))
| ~ spl520_1320 ),
inference(equality_resolution,[],[f65086]) ).
fof(f65101,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),sK517),sK518))
| hBOOL(hAPP(c_Predicate_ODomainP(X0,X1,c_Natural_Oevalc(v_c)),sK517)) )
| ~ spl520_1320 ),
inference(superposition,[],[f21438,f65097]) ).
fof(f65102,plain,
( ! [X0,X1] : hBOOL(hAPP(c_Predicate_ODomainP(X0,X1,c_Natural_Oevalc(v_c)),sK517))
| ~ spl520_1320 ),
inference(forward_subsumption_resolution,[],[f65101,f22694]) ).
fof(f65103,plain,
( spl520_1319
| ~ spl520_1320 ),
inference(avatar_split_clause,[],[f65102,f53321,f53318]) ).
cnf(s3413,plain,
( spl520_1319
| spl520_1320 ),
inference(sat_conversion,[],[f53323]) ).
cnf(s5261,plain,
~ spl520_1306,
inference(sat_conversion,[],[f63333]) ).
cnf(s5561,plain,
( spl520_1306
| ~ spl520_1319 ),
inference(sat_conversion,[],[f64074]) ).
cnf(s5569,plain,
( spl520_1319
| ~ spl520_1320 ),
inference(sat_conversion,[],[f65103]) ).
cnf(s5571,plain,
~ spl520_1319,
inference(rat,[],[s5561,s5261]) ).
cnf(s5572,plain,
~ spl520_1320,
inference(rat,[],[s5569,s5571]) ).
cnf(s5573,plain,
$false,
inference(rat,[],[s3413,s5572,s5571]) ).
fof(f65104,plain,
$false,
inference(avatar_sat_refutation,[],[s5573]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW348+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 % Computer : n006.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 13:39:40 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 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
% 11.93/2.10 % (3969623)Will run a generic schedule for satisfiability detection.
% 11.93/2.10 % (3969634)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4242612310:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 11.93/2.10 % (3969629)% WARNING: option uhcvi not known.
% 11.93/2.10 % (3969631)dis+10_1_sil=32000:sp=arity:random_seed=1396459671:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 11.93/2.10 % (3969630)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3947208510:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 11.93/2.10 % (3969628)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2027699765_2998 on theBenchmark for (2998ds/0Mi)
% 11.93/2.10 % (3969629)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1403399079:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 11.93/2.10 % (3969632)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2406670040:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 11.93/2.10 % (3969633)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2182955725:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 11.93/2.10 % (3969634)Instruction limit reached!
% 11.93/2.10 % (3969634)------------------------------
% 11.93/2.10 % (3969634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969634)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969634)Termination reason: Instruction limit
% 11.93/2.10 % (3969634)Termination phase: Clausification
% 11.93/2.10 % (3969634)Time elapsed: 0.053 s
% 11.93/2.10 % (3969634)Peak memory usage: 21 MB
% 11.93/2.10 % (3969634)Instructions burned: 161 (million)
% 11.93/2.10 % (3969651)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3772321045:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 11.93/2.10 % (3969631)Instruction limit reached!
% 11.93/2.10 % (3969631)------------------------------
% 11.93/2.10 % (3969631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969631)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969631)Termination reason: Instruction limit
% 11.93/2.10 % (3969631)Termination phase: Preprocessing 3
% 11.93/2.10 % (3969631)Time elapsed: 0.063 s
% 11.93/2.10 % (3969631)Peak memory usage: 19 MB
% 11.93/2.10 % (3969631)Instructions burned: 103 (million)
% 11.93/2.10 % (3969632)Instruction limit reached!
% 11.93/2.10 % (3969632)------------------------------
% 11.93/2.10 % (3969632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969632)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969632)Termination reason: Instruction limit
% 11.93/2.10 % (3969632)Termination phase: NewCNF
% 11.93/2.10 % (3969632)Time elapsed: 0.075 s
% 11.93/2.10 % (3969632)Peak memory usage: 21 MB
% 11.93/2.10 % (3969632)Instructions burned: 118 (million)
% 11.93/2.10 % (3969633)Instruction limit reached!
% 11.93/2.10 % (3969633)------------------------------
% 11.93/2.10 % (3969633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969633)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969633)Termination reason: Instruction limit
% 11.93/2.10 % (3969633)Termination phase: Preprocessing 3
% 11.93/2.10 % (3969633)Time elapsed: 0.078 s
% 11.93/2.10 % (3969633)Peak memory usage: 20 MB
% 11.93/2.10 % (3969633)Instructions burned: 132 (million)
% 11.93/2.10 % (3969654)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1760290413:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 11.93/2.10 % (3969659)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=2247146546:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 11.93/2.10 % (3969660)ott-21_1_sil=16000:fs=off:random_seed=348048139:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 11.93/2.10 % (3969654)Instruction limit reached!
% 11.93/2.10 % (3969654)------------------------------
% 11.93/2.10 % (3969654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969654)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969654)Termination reason: Instruction limit
% 11.93/2.10 % (3969654)Termination phase: Preprocessing 3
% 11.93/2.10 % (3969654)Time elapsed: 0.079 s
% 11.93/2.10 % (3969654)Peak memory usage: 20 MB
% 11.93/2.10 % (3969654)Instructions burned: 132 (million)
% 11.93/2.10 % (3969688)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2584568270:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 11.93/2.10 % (3969660)Instruction limit reached!
% 11.93/2.10 % (3969660)------------------------------
% 11.93/2.10 % (3969660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969660)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969660)Termination reason: Instruction limit
% 11.93/2.10 % (3969660)Termination phase: Property scanning
% 11.93/2.10 % (3969660)Time elapsed: 0.104 s
% 11.93/2.10 % (3969660)Peak memory usage: 21 MB
% 11.93/2.10 % (3969660)Instructions burned: 181 (million)
% 11.93/2.10 % (3969705)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3983005379:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 11.93/2.10 % (3969651)Instruction limit reached!
% 11.93/2.10 % (3969651)------------------------------
% 11.93/2.10 % (3969651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969651)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969651)Termination reason: Instruction limit
% 11.93/2.10 % (3969651)Termination phase: Finite model building preprocessing
% 11.93/2.10 % (3969651)Time elapsed: 0.180 s
% 11.93/2.10 % (3969651)Peak memory usage: 25 MB
% 11.93/2.10 % (3969651)Instructions burned: 718 (million)
% 11.93/2.10 % (3969718)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3406012269:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 11.93/2.10 % (3969688)Instruction limit reached!
% 11.93/2.10 % (3969688)------------------------------
% 11.93/2.10 % (3969688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969688)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969688)Termination reason: Instruction limit
% 11.93/2.10 % (3969688)Termination phase: Property scanning
% 11.93/2.10 % (3969688)Time elapsed: 0.229 s
% 11.93/2.10 % (3969688)Peak memory usage: 22 MB
% 11.93/2.10 % (3969688)Instructions burned: 478 (million)
% 11.93/2.10 % (3969659)Instruction limit reached!
% 11.93/2.10 % (3969659)------------------------------
% 11.93/2.10 % (3969659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969659)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969659)Termination reason: Instruction limit
% 11.93/2.10 % (3969659)Termination phase: Saturation
% 11.93/2.10 % (3969659)Time elapsed: 0.324 s
% 11.93/2.10 % (3969659)Peak memory usage: 24 MB
% 11.93/2.10 % (3969659)Instructions burned: 685 (million)
% 11.93/2.10 % (3969763)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2056924428:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 11.93/2.10 % (3969764)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=2077858180:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 11.93/2.10 % (3969718)Instruction limit reached!
% 11.93/2.10 % (3969718)------------------------------
% 11.93/2.10 % (3969718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969718)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969718)Termination reason: Instruction limit
% 11.93/2.10 % (3969718)Termination phase: Saturation
% 11.93/2.10 % (3969718)Time elapsed: 0.377 s
% 11.93/2.10 % (3969718)Peak memory usage: 30 MB
% 11.93/2.10 % (3969718)Instructions burned: 1180 (million)
% 11.93/2.10 % (3969705)Instruction limit reached!
% 11.93/2.10 % (3969705)------------------------------
% 11.93/2.10 % (3969705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969705)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969705)Termination reason: Instruction limit
% 11.93/2.10 % (3969705)Termination phase: Finite model building preprocessing
% 11.93/2.10 % (3969705)Time elapsed: 0.423 s
% 11.93/2.10 % (3969705)Peak memory usage: 30 MB
% 11.93/2.10 % (3969705)Instructions burned: 867 (million)
% 11.93/2.10 % (3969790)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1342662893:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 11.93/2.10 % (3969791)fmb+10_1_sil=64000:random_seed=787102953:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 11.93/2.10 % (3969764)Instruction limit reached!
% 11.93/2.10 % (3969764)------------------------------
% 11.93/2.10 % (3969764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969764)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969764)Termination reason: Instruction limit
% 11.93/2.10 % (3969764)Termination phase: Saturation
% 11.93/2.10 % (3969764)Time elapsed: 0.343 s
% 11.93/2.10 % (3969764)Peak memory usage: 27 MB
% 11.93/2.10 % (3969764)Instructions burned: 692 (million)
% 11.93/2.10 % (3969794)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1797296420:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 11.93/2.10 % (3969763)Instruction limit reached!
% 11.93/2.10 % (3969763)------------------------------
% 11.93/2.10 % (3969763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969763)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969763)Termination reason: Instruction limit
% 11.93/2.10 % (3969763)Termination phase: Finite model building preprocessing
% 11.93/2.10 % (3969763)Time elapsed: 0.438 s
% 11.93/2.10 % (3969763)Peak memory usage: 31 MB
% 11.93/2.10 % (3969763)Instructions burned: 889 (million)
% 11.93/2.10 % (3969810)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1817781730:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 11.93/2.10 % (3969790)Instruction limit reached!
% 11.93/2.10 % (3969790)------------------------------
% 11.93/2.10 % (3969790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.10 % (3969790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.10 % (3969790)CaDiCaL version: 2.1.3
% 11.93/2.10 % (3969790)Termination reason: Instruction limit
% 11.93/2.10 % (3969790)Termination phase: Saturation
% 11.93/2.10 % (3969790)Time elapsed: 0.431 s
% 11.93/2.10 % (3969790)Peak memory usage: 30 MB
% 11.93/2.10 % (3969790)Instructions burned: 881 (million)
% 11.93/2.10 % (3969820)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3670345872:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 11.93/2.10 % (3969629) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3969623-3969629"...
% 11.93/2.10 % (3969629)...printing done.
% 11.93/2.10 % (3969629)Refutation found. Thanks to Tanya!
% 11.93/2.10 % SZS status Theorem for theBenchmark
% 11.93/2.10 % SZS output start Proof for theBenchmark
% See solution above
% 11.93/2.11 % (3969629)------------------------------
% 11.93/2.11 % (3969629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.93/2.11 % (3969629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.11 % (3969629)CaDiCaL version: 2.1.3
% 11.93/2.11 % (3969629)Termination reason: Refutation
% 11.93/2.11 % (3969629)Time elapsed: 1.634 s
% 11.93/2.11 % (3969629)Peak memory usage: 44 MB
% 11.93/2.11 % (3969629)Instructions burned: 2404 (million)
% 11.93/2.11 % (3969623)Success in time 1.862 s
% 11.93/2.11 % Vampire exiting
%------------------------------------------------------------------------------