%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP052-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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 10:16:32 AM UTC 2026
% Result : Unsatisfiable 16.90s 3.06s
% Output : Refutation 16.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 5
% Syntax : Number of formulae : 84 ( 70 unt; 3 def)
% Number of atoms : 102 ( 75 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 34 ( 16 ~; 15 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 197 ( 0 sgn 197 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : multiply(X0,inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1))) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f3,plain,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| a2 != multiply(multiply(inverse(b2),b2),a2)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
inference(reorient_equations,[],[f2]) ).
fof(f5,definition,
( spl0_1
<=> multiply(multiply(a3,b3),c3) = multiply(a3,multiply(b3,c3)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f7,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| spl0_1 ),
inference(avatar_component_clause,[],[f5]) ).
fof(f9,definition,
( spl0_2
<=> a2 = multiply(multiply(inverse(b2),b2),a2) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f11,plain,
( a2 != multiply(multiply(inverse(b2),b2),a2)
| spl0_2 ),
inference(avatar_component_clause,[],[f9]) ).
fof(f13,definition,
( spl0_3
<=> multiply(inverse(a1),a1) = multiply(inverse(b1),b1) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f15,plain,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| spl0_3 ),
inference(avatar_component_clause,[],[f13]) ).
fof(f16,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f3,f13,f9,f5]) ).
fof(f18,plain,
! [X2,X3,X0,X1] : inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),inverse(X3))),X0))),X3)) = multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X0)),X2))),
inference(superposition,[],[f1,f1]) ).
fof(f36,plain,
! [X2,X3,X0,X1] : inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),inverse(X1))),multiply(inverse(multiply(X2,inverse(X3))),X0)))),X1)) = X0,
inference(superposition,[],[f18,f1]) ).
fof(f38,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X1)))) = X2,
inference(superposition,[],[f1,f18]) ).
fof(f52,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(multiply(inverse(X2),X2),inverse(X3))),X0))),X3) = multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(X0,X2)))),
inference(superposition,[],[f38,f1]) ).
fof(f68,plain,
! [X0,X1,X5] : inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X5)))),X1)) = X5,
inference(superposition,[],[f36,f36]) ).
fof(f101,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X0)) = multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,X0)),
inference(superposition,[],[f38,f68]) ).
fof(f129,plain,
! [X0,X1,X6,X5] : multiply(inverse(multiply(X1,X0)),multiply(X1,X5)) = multiply(inverse(multiply(X6,X0)),multiply(X6,X5)),
inference(superposition,[],[f101,f36]) ).
fof(f181,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X4,X1)),multiply(X4,X3)) = multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X0)))),X3)),
inference(superposition,[],[f129,f68]) ).
fof(f223,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,inverse(multiply(X3,X1)))),multiply(X2,inverse(multiply(multiply(multiply(inverse(multiply(X0,X1)),multiply(X0,X1)),inverse(X4)),multiply(X3,X1))))) = X4,
inference(superposition,[],[f38,f129]) ).
fof(f11114,plain,
! [X2,X0,X1] : multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(multiply(inverse(X2),X2),inverse(X1))),multiply(multiply(inverse(X2),X2),inverse(X0))))),X1) = X0,
inference(superposition,[],[f52,f38]) ).
fof(f11134,plain,
! [X2,X0,X1] : multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,X1)))))) = X2,
inference(superposition,[],[f1,f52]) ).
fof(f11602,plain,
! [X2,X0,X1,X4] : multiply(multiply(inverse(multiply(X4,X2)),multiply(X4,X2)),inverse(X0)) = multiply(multiply(inverse(multiply(X1,X2)),multiply(X1,X2)),inverse(X0)),
inference(superposition,[],[f11134,f223]) ).
fof(f12755,plain,
! [X2,X0,X1,X6] : multiply(multiply(inverse(multiply(X1,X2)),multiply(X1,X2)),X0) = multiply(multiply(inverse(multiply(X6,X2)),multiply(X6,X2)),X0),
inference(superposition,[],[f11602,f36]) ).
fof(f15366,plain,
! [X2,X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,X2)),multiply(X1,X2)),
inference(superposition,[],[f181,f11114]) ).
fof(f15623,plain,
! [X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(X0),X0),
inference(superposition,[],[f15366,f11114]) ).
fof(f16063,plain,
! [X0,X1] : multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X0),X0))),X1) = X1,
inference(superposition,[],[f11114,f15366]) ).
fof(f17009,plain,
! [X2,X0,X1] : multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X2),X2))),X1) = X1,
inference(superposition,[],[f16063,f15623]) ).
fof(f17480,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) = multiply(inverse(X2),X0),
inference(superposition,[],[f181,f17009]) ).
fof(f17510,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X3),X3))),inverse(X1))),inverse(multiply(X0,X1))))) = X0,
inference(superposition,[],[f11134,f17009]) ).
fof(f17782,plain,
! [X0,X1] : multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),inverse(multiply(X0,X1))))) = X0,
inference(forward_demodulation,[],[f17510,f17009]) ).
fof(f17834,plain,
! [X2,X0,X1] : multiply(inverse(X1),X2) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X2)),
inference(superposition,[],[f17480,f15623]) ).
fof(f17909,plain,
! [X2,X0,X1] : multiply(inverse(X2),X1) = multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(X0),X0)),
inference(superposition,[],[f17480,f15623]) ).
fof(f18847,plain,
! [X3,X0] : multiply(inverse(multiply(inverse(X3),X3)),X0) = X0,
inference(superposition,[],[f17834,f1]) ).
fof(f20850,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(inverse(X0),X1)),multiply(inverse(X0),X1)),X4) = multiply(multiply(inverse(multiply(X2,multiply(inverse(X3),X3))),multiply(X2,multiply(inverse(X3),X3))),X4),
inference(superposition,[],[f12755,f17909]) ).
fof(f20855,plain,
! [X3,X0,X1,X4] : multiply(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3)),X4) = multiply(multiply(inverse(multiply(inverse(X0),X1)),multiply(inverse(X0),X1)),X4),
inference(forward_demodulation,[],[f20850,f17480]) ).
fof(f21160,plain,
! [X3,X1,X4] : multiply(multiply(inverse(X1),X1),X4) = multiply(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3)),X4),
inference(forward_demodulation,[],[f20855,f17480]) ).
fof(f21279,plain,
! [X3,X1,X4] : multiply(multiply(inverse(X3),X3),X4) = multiply(multiply(inverse(X1),X1),X4),
inference(forward_demodulation,[],[f21160,f17480]) ).
fof(f33253,plain,
! [X2,X0,X1] : multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1))))) = X2,
inference(superposition,[],[f17782,f15623]) ).
fof(f33328,plain,
! [X0,X1] : inverse(X1) = multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X0),X0))))),
inference(superposition,[],[f17782,f15623]) ).
fof(f47105,plain,
! [X0,X4] : multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(X0),inverse(multiply(inverse(X4),X4))))) = X0,
inference(superposition,[],[f33328,f36]) ).
fof(f47215,plain,
! [X0,X1] : multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X0),X0))) = inverse(multiply(inverse(X1),X1)),
inference(superposition,[],[f33328,f15623]) ).
fof(f47791,plain,
! [X2,X0,X1] : multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2))))) = X1,
inference(superposition,[],[f47105,f21279]) ).
fof(f52605,plain,
! [X2,X0,X1] : inverse(multiply(inverse(X2),X2)) = multiply(X0,inverse(multiply(multiply(X0,inverse(X1)),X1))),
inference(superposition,[],[f1,f47791]) ).
fof(f53664,plain,
! [X2,X3,X0,X1] : inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),inverse(multiply(inverse(X0),X0))))),X1)) = inverse(multiply(multiply(X2,inverse(X3)),X3)),
inference(superposition,[],[f68,f52605]) ).
fof(f53990,plain,
! [X2,X3,X1] : inverse(multiply(multiply(X2,inverse(X3)),X3)) = inverse(multiply(multiply(X2,inverse(X1)),X1)),
inference(forward_demodulation,[],[f53664,f47791]) ).
fof(f56170,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(X0,inverse(X3)),X3) = multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(multiply(X0,inverse(X1)),X1)),inverse(multiply(inverse(X4),X4))))),
inference(superposition,[],[f47791,f53990]) ).
fof(f56178,plain,
! [X3,X0,X1] : multiply(multiply(X0,inverse(X1)),X1) = multiply(multiply(X0,inverse(X3)),X3),
inference(forward_demodulation,[],[f56170,f47791]) ).
fof(f56646,plain,
! [X2,X0,X1] : multiply(inverse(X0),X0) = multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X2),
inference(superposition,[],[f56178,f17009]) ).
fof(f58593,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(X3),X3),inverse(X2)) = multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X2)),inverse(multiply(inverse(X0),X0))))),
inference(superposition,[],[f33253,f56646]) ).
fof(f58677,plain,
! [X2,X3] : inverse(X2) = multiply(multiply(inverse(X3),X3),inverse(X2)),
inference(forward_demodulation,[],[f58593,f47791]) ).
fof(f59628,plain,
! [X0,X4] : multiply(multiply(inverse(X4),X4),X0) = X0,
inference(superposition,[],[f58677,f36]) ).
fof(f59886,plain,
! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(inverse(X0))),inverse(inverse(X0))))),
inference(superposition,[],[f33253,f58677]) ).
fof(f59891,plain,
! [X2,X1] : multiply(inverse(X2),X2) = inverse(multiply(inverse(X1),X1)),
inference(forward_demodulation,[],[f59886,f47215]) ).
fof(f61834,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),multiply(X1,X3)) = multiply(X4,multiply(multiply(multiply(multiply(inverse(X0),X0),multiply(inverse(X2),X2)),inverse(multiply(inverse(multiply(X5,multiply(inverse(X0),X0))),multiply(X5,X4)))),X3)),
inference(superposition,[],[f181,f59891]) ).
fof(f62021,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),multiply(X1,X3)) = multiply(X4,multiply(multiply(multiply(multiply(inverse(X0),X0),multiply(inverse(X2),X2)),inverse(multiply(inverse(multiply(inverse(X0),X0)),X4))),X3)),
inference(forward_demodulation,[],[f61834,f17480]) ).
fof(f62669,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),multiply(X1,X3)) = multiply(X4,multiply(multiply(multiply(multiply(inverse(X0),X0),multiply(inverse(X2),X2)),inverse(X4)),X3)),
inference(forward_demodulation,[],[f62021,f18847]) ).
fof(f62963,plain,
! [X2,X3,X1,X4] : multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),multiply(X1,X3)) = multiply(X4,multiply(multiply(multiply(inverse(X2),X2),inverse(X4)),X3)),
inference(forward_demodulation,[],[f62669,f59628]) ).
fof(f63069,plain,
! [X2,X3,X1,X4] : multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),multiply(X1,X3)) = multiply(X4,multiply(inverse(X4),X3)),
inference(forward_demodulation,[],[f62963,f58677]) ).
fof(f63086,plain,
! [X2,X3,X4] : multiply(inverse(multiply(inverse(X2),X2)),X3) = multiply(X4,multiply(inverse(X4),X3)),
inference(forward_demodulation,[],[f63069,f17480]) ).
fof(f63089,plain,
! [X3,X4] : multiply(X4,multiply(inverse(X4),X3)) = X3,
inference(forward_demodulation,[],[f63086,f18847]) ).
fof(f63116,plain,
! [X0,X1] : multiply(X1,inverse(multiply(inverse(X0),X0))) = X1,
inference(superposition,[],[f63089,f59891]) ).
fof(f63119,plain,
! [X0,X1] : multiply(X1,multiply(inverse(X0),X0)) = X1,
inference(superposition,[],[f63089,f15623]) ).
fof(f64351,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(X1),X1)),X0) = multiply(inverse(inverse(X0)),multiply(inverse(X2),X2)),
inference(superposition,[],[f17909,f63119]) ).
fof(f64521,plain,
! [X0,X1] : inverse(inverse(X0)) = multiply(inverse(multiply(inverse(X1),X1)),X0),
inference(forward_demodulation,[],[f64351,f63119]) ).
fof(f64935,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[],[f64521,f18847]) ).
fof(f70862,plain,
! [X2,X0,X1] : multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,X1))))) = X2,
inference(superposition,[],[f33253,f63116]) ).
fof(f71153,plain,
! [X2,X0,X1] : multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(X1,inverse(multiply(X2,X1))))) = X2,
inference(forward_demodulation,[],[f70862,f64935]) ).
fof(f71552,plain,
! [X2,X0,X1] : multiply(multiply(inverse(X0),X0),inverse(multiply(X1,inverse(multiply(X2,X1))))) = X2,
inference(forward_demodulation,[],[f71153,f64935]) ).
fof(f71848,plain,
! [X2,X1] : inverse(multiply(X1,inverse(multiply(X2,X1)))) = X2,
inference(forward_demodulation,[],[f71552,f58677]) ).
fof(f76969,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(inverse(inverse(multiply(X0,X1))),X2),
inference(superposition,[],[f17480,f71848]) ).
fof(f77260,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X0,X1),X2),
inference(forward_demodulation,[],[f76969,f64935]) ).
fof(f107845,plain,
( multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3))
| spl0_1 ),
inference(superposition,[],[f7,f77260]) ).
fof(f108080,plain,
( $false
| spl0_1 ),
inference(trivial_inequality_removal,[],[f107845]) ).
fof(f108081,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f108080]) ).
fof(f110284,plain,
( $false
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f11,f59628]) ).
fof(f110285,plain,
spl0_2,
inference(avatar_contradiction_clause,[],[f110284]) ).
fof(f110286,plain,
( $false
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f15,f15623]) ).
fof(f110287,plain,
spl0_3,
inference(avatar_contradiction_clause,[],[f110286]) ).
cnf(s4,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f16]) ).
cnf(s33521,plain,
spl0_1,
inference(sat_conversion,[],[f108081]) ).
cnf(s33585,plain,
spl0_2,
inference(sat_conversion,[],[f110285]) ).
cnf(s33586,plain,
spl0_3,
inference(sat_conversion,[],[f110287]) ).
cnf(s33587,plain,
$false,
inference(rat,[],[s4,s33586,s33585,s33521]) ).
fof(f110288,plain,
$false,
inference(avatar_sat_refutation,[],[s33587]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP052-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.38 % Computer : n007.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 09:14:55 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.42 Running first-order model finding
% 0.13/0.42 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.90/3.06 % (1143207)Will run a generic schedule for satisfiability detection.
% 16.90/3.06 % (1143222)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1617964308:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.90/3.06 % (1143221)% WARNING: option uhcvi not known.
% 16.90/3.06 % (1143220)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3344704370_2999 on theBenchmark for (2999ds/0Mi)
% 16.90/3.06 % (1143221)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=840355266:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.90/3.06 % (1143223)dis+10_1_sil=32000:sp=arity:random_seed=3816783697:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.90/3.06 % (1143224)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=422051809:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.90/3.06 % (1143225)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3640172191:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.90/3.06 % TRYING [1]
% 16.90/3.06 % TRYING [2]
% 16.90/3.06 % TRYING [3]
% 16.90/3.06 % (1143226)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3756426730:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.90/3.06 % TRYING [4]
% 16.90/3.06 % (1143223)Instruction limit reached!
% 16.90/3.06 % (1143223)------------------------------
% 16.90/3.06 % (1143223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143223)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143223)Termination reason: Instruction limit
% 16.90/3.06 % (1143223)Termination phase: Saturation
% 16.90/3.06 % (1143223)Time elapsed: 0.055 s
% 16.90/3.06 % (1143223)Peak memory usage: 12 MB
% 16.90/3.06 % (1143223)Instructions burned: 105 (million)
% 16.90/3.06 % (1143224)Instruction limit reached!
% 16.90/3.06 % (1143224)------------------------------
% 16.90/3.06 % (1143224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143224)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143224)Termination reason: Instruction limit
% 16.90/3.06 % (1143224)Termination phase: Saturation
% 16.90/3.06 % (1143224)Time elapsed: 0.069 s
% 16.90/3.06 % (1143224)Peak memory usage: 13 MB
% 16.90/3.06 % (1143224)Instructions burned: 122 (million)
% 16.90/3.06 % (1143225)Instruction limit reached!
% 16.90/3.06 % (1143225)------------------------------
% 16.90/3.06 % (1143225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143225)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143225)Termination reason: Instruction limit
% 16.90/3.06 % (1143225)Termination phase: Saturation
% 16.90/3.06 % (1143225)Time elapsed: 0.073 s
% 16.90/3.06 % (1143225)Peak memory usage: 13 MB
% 16.90/3.06 % (1143225)Instructions burned: 132 (million)
% 16.90/3.06 % (1143234)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4160192008:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.90/3.06 % TRYING [1]
% 16.90/3.06 % TRYING [2]
% 16.90/3.06 % TRYING [3]
% 16.90/3.06 % (1143235)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4021653501:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.90/3.06 % (1143236)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=1003766725:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.90/3.06 % TRYING [4]
% 16.90/3.06 % (1143235)Instruction limit reached!
% 16.90/3.06 % (1143235)------------------------------
% 16.90/3.06 % (1143235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143235)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143235)Termination reason: Instruction limit
% 16.90/3.06 % (1143235)Termination phase: Saturation
% 16.90/3.06 % (1143235)Time elapsed: 0.074 s
% 16.90/3.06 % (1143235)Peak memory usage: 13 MB
% 16.90/3.06 % (1143235)Instructions burned: 132 (million)
% 16.90/3.06 % (1143226)Instruction limit reached!
% 16.90/3.06 % (1143226)------------------------------
% 16.90/3.06 % (1143226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143226)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143226)Termination reason: Instruction limit
% 16.90/3.06 % (1143226)Termination phase: Saturation
% 16.90/3.06 % (1143226)Time elapsed: 0.154 s
% 16.90/3.06 % (1143226)Peak memory usage: 13 MB
% 16.90/3.06 % (1143226)Instructions burned: 160 (million)
% 16.90/3.06 % (1143240)ott-21_1_sil=16000:fs=off:random_seed=501521817:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 16.90/3.06 % (1143241)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3226341406:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 16.90/3.06 % (1143240)Instruction limit reached!
% 16.90/3.06 % (1143240)------------------------------
% 16.90/3.06 % (1143240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143240)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143240)Termination reason: Instruction limit
% 16.90/3.06 % (1143240)Termination phase: Saturation
% 16.90/3.06 % (1143240)Time elapsed: 0.090 s
% 16.90/3.06 % (1143240)Peak memory usage: 12 MB
% 16.90/3.06 % (1143240)Instructions burned: 180 (million)
% 16.90/3.06 % (1143244)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=236647702:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 16.90/3.06 % TRYING [1]
% 16.90/3.06 % TRYING [2]
% 16.90/3.06 % TRYING [3]
% 16.90/3.06 % TRYING [4]
% 16.90/3.06 % (1143241)Instruction limit reached!
% 16.90/3.06 % (1143241)------------------------------
% 16.90/3.06 % (1143241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143241)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143241)Termination reason: Instruction limit
% 16.90/3.06 % (1143241)Termination phase: Saturation
% 16.90/3.06 % (1143241)Time elapsed: 0.240 s
% 16.90/3.06 % (1143241)Peak memory usage: 16 MB
% 16.90/3.06 % (1143241)Instructions burned: 478 (million)
% 16.90/3.06 % (1143236)Instruction limit reached!
% 16.90/3.06 % (1143236)------------------------------
% 16.90/3.06 % (1143236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143236)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143236)Termination reason: Instruction limit
% 16.90/3.06 % (1143236)Termination phase: Saturation
% 16.90/3.06 % (1143236)Time elapsed: 0.341 s
% 16.90/3.06 % (1143236)Peak memory usage: 16 MB
% 16.90/3.06 % (1143236)Instructions burned: 684 (million)
% 16.90/3.06 % (1143246)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1942713799:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 16.90/3.06 % (1143247)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3947834988:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 16.90/3.06 % TRYING [14]
% 16.90/3.06 % (1143234)Instruction limit reached!
% 16.90/3.06 % (1143234)------------------------------
% 16.90/3.06 % (1143234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143234)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143234)Termination reason: Instruction limit
% 16.90/3.06 % (1143234)Termination phase: Finite model building SAT solving
% 16.90/3.06 % (1143234)Time elapsed: 0.418 s
% 16.90/3.06 % (1143234)Peak memory usage: 12 MB
% 16.90/3.06 % (1143234)Instructions burned: 714 (million)
% 16.90/3.06 % (1143250)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=1270916372: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)
% 16.90/3.06 % (1143244)Instruction limit reached!
% 16.90/3.06 % (1143244)------------------------------
% 16.90/3.06 % (1143244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143244)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143244)Termination reason: Instruction limit
% 16.90/3.06 % (1143244)Termination phase: Finite model building SAT solving
% 16.90/3.06 % (1143244)Time elapsed: 0.648 s
% 16.90/3.06 % (1143244)Peak memory usage: 12 MB
% 16.90/3.06 % (1143244)Instructions burned: 866 (million)
% 16.90/3.06 % (1143247)Instruction limit reached!
% 16.90/3.06 % (1143247)------------------------------
% 16.90/3.06 % (1143247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143247)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143247)Termination reason: Instruction limit
% 16.90/3.06 % (1143247)Termination phase: Finite model building constraint generation
% 16.90/3.06 % (1143247)Time elapsed: 0.507 s
% 16.90/3.06 % (1143247)Peak memory usage: 81 MB
% 16.90/3.06 % (1143247)Instructions burned: 889 (million)
% 16.90/3.06 % (1143270)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3681785521:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 16.90/3.06 % (1143272)fmb+10_1_sil=64000:random_seed=2738955167:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 16.90/3.06 % TRYING [1]
% 16.90/3.06 % TRYING [2]
% 16.90/3.06 % TRYING [3]
% 16.90/3.06 % TRYING [4]
% 16.90/3.06 % (1143250)Instruction limit reached!
% 16.90/3.06 % (1143250)------------------------------
% 16.90/3.06 % (1143250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143250)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143250)Termination reason: Instruction limit
% 16.90/3.06 % (1143250)Termination phase: Saturation
% 16.90/3.06 % (1143250)Time elapsed: 0.658 s
% 16.90/3.06 % (1143250)Peak memory usage: 17 MB
% 16.90/3.06 % (1143250)Instructions burned: 692 (million)
% 16.90/3.06 % (1143277)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2711945972:i=9515:nm=5_2987 on theBenchmark for (2987ds/9515Mi)
% 16.90/3.06 % TRYING [20]
% 16.90/3.06 % (1143246)Instruction limit reached!
% 16.90/3.06 % (1143246)------------------------------
% 16.90/3.06 % (1143246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143246)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143246)Termination reason: Instruction limit
% 16.90/3.06 % (1143246)Termination phase: Saturation
% 16.90/3.06 % (1143246)Time elapsed: 0.945 s
% 16.90/3.06 % (1143246)Peak memory usage: 24 MB
% 16.90/3.06 % (1143246)Instructions burned: 1179 (million)
% 16.90/3.06 % (1143280)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3498403981:fmbsr=1.7:i=920_2985 on theBenchmark for (2985ds/920Mi)
% 16.90/3.06 % TRYING [8]
% 16.90/3.06 % (1143270)Instruction limit reached!
% 16.90/3.06 % (1143270)------------------------------
% 16.90/3.06 % (1143270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143270)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143270)Termination reason: Instruction limit
% 16.90/3.06 % (1143270)Termination phase: Saturation
% 16.90/3.06 % (1143270)Time elapsed: 0.689 s
% 16.90/3.06 % (1143270)Peak memory usage: 18 MB
% 16.90/3.06 % (1143270)Instructions burned: 880 (million)
% 16.90/3.06 % (1143287)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2888806682:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 16.90/3.06 % (1143280)Instruction limit reached!
% 16.90/3.06 % (1143280)------------------------------
% 16.90/3.06 % (1143280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.06 % (1143280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.06 % (1143280)CaDiCaL version: 2.1.3
% 16.90/3.06 % (1143280)Termination reason: Instruction limit
% 16.90/3.06 % (1143280)Termination phase: Finite model building SAT solving
% 16.90/3.06 % (1143280)Time elapsed: 0.706 s
% 16.90/3.06 % (1143280)Peak memory usage: 40 MB
% 16.90/3.06 % (1143280)Instructions burned: 921 (million)
% 16.90/3.06 % (1143296)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=134773752:i=1472:ins=7:fdi=8:gsp=on_2978 on theBenchmark for (2978ds/1472Mi)
% 16.90/3.06 % TRYING [5]
% 16.90/3.06 % (1143222) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1143207-1143222"...
% 16.90/3.06 % (1143222)...printing done.
% 16.90/3.06 % (1143222)Refutation found. Thanks to Tanya!
% 16.90/3.06 % SZS status Unsatisfiable for theBenchmark
% 16.90/3.06 % SZS output start Proof for theBenchmark
% See solution above
% 16.90/3.07 % (1143222)------------------------------
% 16.90/3.07 % (1143222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.90/3.07 % (1143222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.90/3.07 % (1143222)CaDiCaL version: 2.1.3
% 16.90/3.07 % (1143222)Termination reason: Refutation
% 16.90/3.07 % (1143222)Time elapsed: 2.566 s
% 16.90/3.07 % (1143222)Peak memory usage: 59 MB
% 16.90/3.07 % (1143222)Instructions burned: 6326 (million)
% 16.90/3.07 % (1143207)Success in time 2.634 s
% 16.90/3.07 % Vampire exiting
%------------------------------------------------------------------------------