%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP070-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:12:30 AM UTC 2026
% Result : Unsatisfiable 0.15s 2.03s
% Output : Refutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 6
% Syntax : Number of formulae : 51 ( 31 unt; 3 def)
% Number of atoms : 76 ( 44 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 49 ( 24 ~; 22 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 86 ( 0 sgn 86 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] : divide(divide(X0,X0),divide(X1,divide(divide(X2,divide(X3,X1)),inverse(X3)))) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,axiom,
! [X0,X1] : multiply(X0,X1) = divide(X0,inverse(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiply) ).
fof(f3,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/sandbox/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f4,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,[],[f3]) ).
fof(f5,plain,
( divide(inverse(a1),inverse(a1)) != divide(inverse(b1),inverse(b1))
| a2 != divide(divide(inverse(b2),inverse(b2)),inverse(a2))
| divide(divide(a3,inverse(b3)),inverse(c3)) != divide(a3,inverse(divide(b3,inverse(c3)))) ),
inference(definition_unfolding,[],[f4,f2,f2,f2,f2,f2,f2,f2,f2]) ).
fof(f7,definition,
( spl0_1
<=> divide(divide(a3,inverse(b3)),inverse(c3)) = divide(a3,inverse(divide(b3,inverse(c3)))) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f9,plain,
( divide(divide(a3,inverse(b3)),inverse(c3)) != divide(a3,inverse(divide(b3,inverse(c3))))
| spl0_1 ),
inference(avatar_component_clause,[],[f7]) ).
fof(f11,definition,
( spl0_2
<=> a2 = divide(divide(inverse(b2),inverse(b2)),inverse(a2)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f13,plain,
( a2 != divide(divide(inverse(b2),inverse(b2)),inverse(a2))
| spl0_2 ),
inference(avatar_component_clause,[],[f11]) ).
fof(f15,definition,
( spl0_3
<=> divide(inverse(a1),inverse(a1)) = divide(inverse(b1),inverse(b1)) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f17,plain,
( divide(inverse(a1),inverse(a1)) != divide(inverse(b1),inverse(b1))
| spl0_3 ),
inference(avatar_component_clause,[],[f15]) ).
fof(f18,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f5,f15,f11,f7]) ).
fof(f20,plain,
! [X2,X3,X0,X1,X4] : divide(X4,X4) = divide(divide(X1,X1),divide(divide(divide(X0,divide(X2,X3)),inverse(X2)),divide(X0,inverse(X3)))),
inference(superposition,[],[f1,f1]) ).
fof(f30,plain,
! [X0,X1] : divide(X0,X0) = divide(X1,X1),
inference(superposition,[],[f20,f20]) ).
fof(f54,plain,
! [X2,X3,X0,X1] : divide(divide(X1,X1),divide(X2,divide(divide(X3,divide(X0,X0)),inverse(X2)))) = X3,
inference(superposition,[],[f1,f30]) ).
fof(f56,plain,
! [X2,X3,X0,X1] : divide(X3,X2) = divide(divide(X1,X1),divide(X2,divide(divide(X0,X0),inverse(X3)))),
inference(superposition,[],[f1,f30]) ).
fof(f88,plain,
! [X2,X3,X0,X1,X4,X5] : divide(X1,X4) = divide(divide(X5,X5),divide(X4,divide(divide(X0,X0),divide(inverse(X1),divide(divide(X2,X2),inverse(divide(X3,X3))))))),
inference(superposition,[],[f56,f56]) ).
fof(f103,plain,
! [X2,X3,X0,X1,X4,X5] : divide(divide(X4,X4),divide(X5,divide(divide(divide(X0,X0),divide(divide(X1,X1),divide(divide(X2,X2),inverse(X3)))),inverse(X5)))) = X3,
inference(superposition,[],[f54,f56]) ).
fof(f118,plain,
! [X2,X0,X1] : divide(X2,X2) = divide(X0,divide(divide(X1,X1),inverse(X0))),
inference(superposition,[],[f30,f56]) ).
fof(f156,plain,
! [X2,X3,X0,X1] : divide(divide(X1,X1),divide(inverse(X2),divide(divide(X0,X0),inverse(divide(X3,X3))))) = X2,
inference(superposition,[],[f1,f118]) ).
fof(f159,plain,
! [X1,X4,X5] : divide(X1,X4) = divide(divide(X5,X5),divide(X4,X1)),
inference(backward_demodulation,[],[f88,f156]) ).
fof(f207,plain,
! [X2,X3,X0,X1,X4] : divide(divide(X3,X3),divide(X4,divide(divide(divide(X0,X0),divide(divide(X1,X1),X2)),inverse(X4)))) = X2,
inference(superposition,[],[f54,f159]) ).
fof(f221,plain,
! [X2,X0,X1] : divide(divide(divide(X0,divide(X1,X1)),inverse(X2)),X2) = X0,
inference(superposition,[],[f54,f159]) ).
fof(f229,plain,
! [X2,X3,X0,X1] : divide(X0,divide(X2,X2)) = divide(divide(X3,X3),divide(inverse(X0),divide(X1,X1))),
inference(superposition,[],[f56,f159]) ).
fof(f257,plain,
! [X2,X3] : divide(divide(X2,X2),inverse(X3)) = X3,
inference(backward_demodulation,[],[f103,f207]) ).
fof(f309,plain,
! [X2,X3,X1] : divide(divide(X1,X1),divide(inverse(X2),divide(X3,X3))) = X2,
inference(backward_demodulation,[],[f156,f257]) ).
fof(f326,plain,
! [X2,X0] : divide(X0,divide(X2,X2)) = X0,
inference(backward_demodulation,[],[f229,f309]) ).
fof(f352,plain,
! [X2,X0] : divide(divide(X0,inverse(X2)),X2) = X0,
inference(backward_demodulation,[],[f221,f326]) ).
fof(f400,plain,
! [X2,X0,X1] : divide(inverse(X0),divide(X1,X1)) = divide(divide(X2,X2),X0),
inference(superposition,[],[f159,f257]) ).
fof(f404,plain,
! [X2,X0] : inverse(X0) = divide(divide(X2,X2),X0),
inference(forward_demodulation,[],[f400,f326]) ).
fof(f420,plain,
! [X0,X1] : divide(X1,X0) = inverse(divide(X0,X1)),
inference(superposition,[],[f159,f352]) ).
fof(f421,plain,
! [X2,X3,X0,X1] : divide(X0,inverse(divide(X3,X2))) = divide(divide(X1,X1),divide(X2,divide(X0,inverse(X3)))),
inference(superposition,[],[f1,f352]) ).
fof(f434,plain,
( divide(divide(a3,inverse(b3)),inverse(c3)) != divide(a3,divide(inverse(c3),b3))
| spl0_1 ),
inference(backward_demodulation,[],[f9,f420]) ).
fof(f438,plain,
! [X2,X3,X0,X1] : divide(X0,divide(X2,X3)) = divide(divide(X1,X1),divide(X2,divide(X0,inverse(X3)))),
inference(backward_demodulation,[],[f421,f420]) ).
fof(f452,plain,
( ! [X0] : divide(divide(a3,inverse(b3)),inverse(c3)) != divide(a3,divide(divide(X0,X0),divide(b3,inverse(c3))))
| spl0_1 ),
inference(superposition,[],[f434,f159]) ).
fof(f481,plain,
( ! [X0,X1] : divide(a3,divide(divide(X1,X1),divide(b3,inverse(c3)))) != divide(divide(a3,divide(divide(X0,X0),b3)),inverse(c3))
| spl0_1 ),
inference(superposition,[],[f452,f404]) ).
fof(f524,plain,
( ! [X1] : divide(a3,divide(inverse(c3),b3)) != divide(divide(a3,divide(divide(X1,X1),b3)),inverse(c3))
| spl0_1 ),
inference(superposition,[],[f481,f159]) ).
fof(f549,plain,
( ! [X0,X1] : divide(a3,divide(inverse(c3),b3)) != divide(divide(X0,X0),divide(inverse(c3),divide(a3,divide(divide(X1,X1),b3))))
| spl0_1 ),
inference(superposition,[],[f524,f159]) ).
fof(f560,plain,
( ! [X0] : divide(a3,divide(inverse(c3),b3)) != divide(divide(X0,X0),divide(inverse(c3),divide(a3,inverse(b3))))
| spl0_1 ),
inference(superposition,[],[f549,f404]) ).
fof(f575,plain,
( $false
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f560,f438]) ).
fof(f576,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f575]) ).
fof(f578,plain,
( $false
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f13,f257]) ).
fof(f579,plain,
spl0_2,
inference(avatar_contradiction_clause,[],[f578]) ).
fof(f580,plain,
( $false
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f17,f30]) ).
fof(f581,plain,
spl0_3,
inference(avatar_contradiction_clause,[],[f580]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f18]) ).
cnf(s3,plain,
spl0_1,
inference(sat_conversion,[],[f576]) ).
cnf(s4,plain,
spl0_2,
inference(sat_conversion,[],[f579]) ).
cnf(s5,plain,
spl0_3,
inference(sat_conversion,[],[f581]) ).
cnf(s6,plain,
$false,
inference(rat,[],[s1,s5,s4,s3]) ).
fof(f582,plain,
$false,
inference(avatar_sat_refutation,[],[s6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP070-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n005.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 09:17:47 UTC 2026
% 0.14/0.38 % CPUTime :
% 0.14/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.41 Running first-order theorem proving
% 0.14/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.70/1.93 % (3722872)Input is clausal, will run a generic CNF schedule.
% 6.70/1.93 % (3722895)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=299535201:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.70/1.93 % (3722901)dis-21_1_sil=8000:lcm=predicate:random_seed=2509789394:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 6.70/1.93 % (3722901)Refutation not found, incomplete strategy
% 6.70/1.93 % (3722901)------------------------------
% 6.70/1.93 % (3722901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.70/1.93 % (3722901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.70/1.93 % (3722901)CaDiCaL version: 2.1.3
% 6.70/1.93 % (3722901)Termination reason: Refutation not found, incomplete strategy
% 6.70/1.93 % (3722901)Time elapsed: 0.001 s
% 6.70/1.93 % (3722901)Peak memory usage: 88 MB
% 6.70/1.93 % (3722898)lrs+10_1_sil=8000:sp=occurrence:random_seed=2790946081:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.70/1.93 % (3722900)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4249053531:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.70/1.93 % (3722899)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2552916717:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.70/1.93 % (3722896)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3628871854:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.70/1.93 % (3722897)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=271649823:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.70/1.93 % (3722898)Instruction limit reached!
% 6.70/1.93 % (3722898)------------------------------
% 6.70/1.93 % (3722898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.70/1.93 % (3722898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.70/1.93 % (3722898)CaDiCaL version: 2.1.3
% 6.70/1.93 % (3722898)Termination reason: Instruction limit
% 6.70/1.93 % (3722898)Termination phase: Saturation
% 6.70/1.93 % (3722898)Time elapsed: 0.102 s
% 6.70/1.93 % (3722898)Peak memory usage: 89 MB
% 6.70/1.93 % (3722898)Instructions burned: 107 (million)
% 6.70/1.93 % (3722899)Instruction limit reached!
% 6.70/1.93 % (3722899)------------------------------
% 6.70/1.93 % (3722899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.70/1.93 % (3722899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.70/1.93 % (3722899)CaDiCaL version: 2.1.3
% 6.70/1.93 % (3722899)Termination reason: Instruction limit
% 6.70/1.93 % (3722899)Termination phase: Saturation
% 6.70/1.93 % (3722899)Time elapsed: 0.102 s
% 6.70/1.93 % (3722899)Peak memory usage: 89 MB
% 6.70/1.93 % (3722899)Instructions burned: 115 (million)
% 6.70/1.93 % (3722900)Instruction limit reached!
% 6.70/1.93 % (3722900)------------------------------
% 6.70/1.93 % (3722900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.70/1.93 % (3722900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.70/1.93 % (3722900)CaDiCaL version: 2.1.3
% 6.70/1.93 % (3722900)Termination reason: Instruction limit
% 6.70/1.93 % (3722900)Termination phase: Saturation
% 6.70/1.93 % (3722900)Time elapsed: 0.159 s
% 6.70/1.93 % (3722900)Peak memory usage: 89 MB
% 6.70/1.93 % (3722900)Instructions burned: 180 (million)
% 6.70/1.93 % (3722913)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2343462201:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 6.70/1.93 % (3722913)Refutation not found, incomplete strategy
% 6.70/1.93 % (3722913)------------------------------
% 6.70/1.93 % (3722913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.70/1.93 % (3722913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.70/1.93 % (3722913)CaDiCaL version: 2.1.3
% 6.70/1.93 % (3722913)Termination reason: Refutation not found, incomplete strategy
% 6.70/1.93 % (3722913)Time elapsed: 0.002 s
% 6.70/1.93 % (3722913)Peak memory usage: 88 MB
% 6.70/1.93 % (3722914)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2186334790:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 0.15/2.03 % (3722914)Refutation not found, incomplete strategy
% 0.15/2.03 % (3722914)------------------------------
% 0.15/2.03 % (3722914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.15/2.03 % (3722914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/2.03 % (3722914)CaDiCaL version: 2.1.3
% 0.15/2.03 % (3722914)Termination reason: Refutation not found, incomplete strategy
% 0.15/2.03 % (3722914)Time elapsed: 0.002 s
% 0.15/2.03 % (3722914)Peak memory usage: 88 MB
% 0.15/2.03 % (3722915)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3817575448:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 0.15/2.03 % (3722915)Refutation not found, incomplete strategy
% 0.15/2.03 % (3722915)------------------------------
% 0.15/2.03 % (3722915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.15/2.03 % (3722915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/2.03 % (3722915)CaDiCaL version: 2.1.3
% 0.15/2.03 % (3722915)Termination reason: Refutation not found, incomplete strategy
% 0.15/2.03 % (3722915)Time elapsed: 0.002 s
% 0.15/2.03 % (3722915)Peak memory usage: 88 MB
% 0.15/2.03 % (3722901)------------------------------
% 0.15/2.03 % (3722901)------------------------------
% 0.15/2.03 % (3722920)lrs+10_64_to=lpo:sil=8000:random_seed=636979206:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 0.15/2.03 % (3722920)First to succeed.
% 0.15/2.03 % (3722920)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3722872"
% 0.15/2.03 % (3722913)------------------------------
% 0.15/2.03 % (3722913)------------------------------
% 0.15/2.03 % (3722914)------------------------------
% 0.15/2.03 % (3722914)------------------------------
% 0.15/2.03 % (3722915)------------------------------
% 0.15/2.03 % (3722915)------------------------------
% 0.15/2.03 % (3722895)Also succeeded, but the first one will report.
% 0.15/2.03 % (3722926)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1366476014:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi)
% 0.15/2.03 % (3722927)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3870777566:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 0.15/2.03 % (3722928)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2689298679:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 0.15/2.03 % (3722926)Also succeeded, but the first one will report.
% 0.15/2.03 % (3722927)Instruction limit reached!
% 0.15/2.03 % (3722927)------------------------------
% 0.15/2.03 % (3722927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.15/2.03 % (3722927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/2.03 % (3722927)CaDiCaL version: 2.1.3
% 0.15/2.03 % (3722927)Termination reason: Instruction limit
% 0.15/2.03 % (3722927)Termination phase: Saturation
% 0.15/2.03 % (3722927)Time elapsed: 0.088 s
% 0.15/2.03 % (3722927)Peak memory usage: 91 MB
% 0.15/2.03 % (3722927)Instructions burned: 157 (million)
% 0.15/2.03 % (3722920)Refutation found. Thanks to Tanya!
% 0.15/2.03 % SZS status Unsatisfiable for theBenchmark
% 0.15/2.03 % SZS output start Proof for theBenchmark
% See solution above
% 0.15/2.03 % (3722920)------------------------------
% 0.15/2.03 % (3722920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.15/2.03 % (3722920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/2.03 % (3722920)CaDiCaL version: 2.1.3
% 0.15/2.03 % (3722920)Termination reason: Refutation
% 0.15/2.03 % (3722920)Time elapsed: 0.031 s
% 0.15/2.03 % (3722920)Peak memory usage: 89 MB
% 0.15/2.03 % (3722920)Instructions burned: 51 (million)
% 0.15/2.03 % (3722920)------------------------------
% 0.15/2.03 % (3722920)------------------------------
% 0.15/2.03 % (3722872)Success in time 1.052 s
% 0.15/2.03 % Vampire exiting
%------------------------------------------------------------------------------