%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP398-3 : TPTP v9.3.1. Released v2.5.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:13:51 AM UTC 2026
% Result : Satisfiable 20.32s 3.90s
% Output : Saturation 22.09s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u13,axiom,
~ subgroup_member(X0) ).
cnf(u16,axiom,
~ subgroup_member(identity) ).
cnf(u223,axiom,
( ~ subgroup_member(multiply(X1,multiply(X2,X0)))
| ~ subgroup_member(inverse(X0))
| subgroup_member(multiply(X1,X2)) ) ).
cnf(u297,axiom,
( ~ subgroup_member(multiply(X2,multiply(X3,multiply(inverse(X0),inverse(X1)))))
| subgroup_member(multiply(X2,multiply(X3,inverse(X0))))
| ~ subgroup_member(X1) ) ).
cnf(u260,axiom,
( ~ subgroup_member(multiply(X0,multiply(X2,X3)))
| ~ subgroup_member(inverse(X0))
| ~ subgroup_member(X1)
| ~ subgroup_member(X4)
| subgroup_member(multiply(X2,multiply(X3,multiply(X4,X1)))) ) ).
cnf(u562,axiom,
( ~ subgroup_member(inverse(X0))
| subgroup_member(multiply(X0,inverse(X1)))
| ~ subgroup_member(X1) ) ).
cnf(closure_of_inverse,axiom,
( subgroup_member(inverse(X0))
| ~ subgroup_member(X0) ) ).
cnf(u517,axiom,
( ~ subgroup_member(inverse(X1))
| ~ subgroup_member(inverse(X0))
| subgroup_member(multiply(X0,X1)) ) ).
cnf(u519,axiom,
( ~ subgroup_member(multiply(X0,inverse(X1)))
| subgroup_member(multiply(X1,inverse(X0))) ) ).
cnf(u169,axiom,
( ~ subgroup_member(multiply(inverse(X0),X2))
| ~ subgroup_member(multiply(X1,X0))
| subgroup_member(multiply(X1,X2)) ) ).
cnf(u524,axiom,
( ~ subgroup_member(multiply(inverse(X2),multiply(inverse(X0),inverse(X1))))
| subgroup_member(multiply(X1,multiply(X0,X2))) ) ).
cnf(u256,axiom,
( ~ subgroup_member(multiply(X0,X2))
| ~ subgroup_member(inverse(X0))
| ~ subgroup_member(X1)
| ~ subgroup_member(X3)
| subgroup_member(multiply(X2,multiply(X3,X1))) ) ).
cnf(u507,axiom,
( ~ subgroup_member(multiply(X4,multiply(X1,multiply(X2,X0))))
| subgroup_member(multiply(X1,multiply(X2,multiply(X0,X3))))
| ~ subgroup_member(X3)
| ~ subgroup_member(inverse(X4)) ) ).
cnf(u552,axiom,
( ~ subgroup_member(multiply(X1,multiply(X0,X2)))
| ~ subgroup_member(X1)
| ~ subgroup_member(X0)
| subgroup_member(X2) ) ).
cnf(u38,axiom,
multiply(X0,identity) = X0 ).
cnf(u173,axiom,
( ~ subgroup_member(multiply(X1,multiply(X2,inverse(X0))))
| subgroup_member(multiply(X1,multiply(X2,X3)))
| ~ subgroup_member(multiply(X0,X3)) ) ).
cnf(u74,axiom,
identity = multiply(X0,inverse(X0)) ).
cnf(u450,axiom,
( ~ subgroup_member(multiply(X4,multiply(X3,multiply(inverse(X0),inverse(X1)))))
| ~ subgroup_member(multiply(X1,multiply(X0,X2)))
| subgroup_member(multiply(X4,multiply(X3,X2))) ) ).
cnf(u453,axiom,
( subgroup_member(multiply(inverse(X0),inverse(X1)))
| ~ subgroup_member(X0)
| ~ subgroup_member(X1) ) ).
cnf(u24,axiom,
multiply(inverse(X1),multiply(X1,X0)) = X0 ).
cnf(u167,axiom,
( ~ subgroup_member(multiply(X0,X1))
| subgroup_member(multiply(X2,X1))
| ~ subgroup_member(inverse(X0))
| ~ subgroup_member(X2) ) ).
cnf(u76,axiom,
multiply(X1,multiply(inverse(X1),X0)) = X0 ).
cnf(u361,axiom,
( ~ subgroup_member(multiply(X4,multiply(X1,X2)))
| ~ subgroup_member(inverse(X4))
| ~ subgroup_member(X0)
| ~ subgroup_member(X3)
| subgroup_member(multiply(X0,multiply(X1,multiply(X2,X3)))) ) ).
cnf(u570,axiom,
( ~ subgroup_member(multiply(X1,X0))
| subgroup_member(multiply(inverse(X0),multiply(inverse(X1),inverse(X2))))
| ~ subgroup_member(X2) ) ).
cnf(u36,axiom,
( ~ subgroup_member(multiply(X1,X0))
| subgroup_member(X0)
| ~ subgroup_member(inverse(X1)) ) ).
cnf(u530,axiom,
( ~ subgroup_member(multiply(X2,multiply(X3,X1)))
| subgroup_member(multiply(X0,X1))
| ~ subgroup_member(inverse(X2))
| ~ subgroup_member(multiply(X0,inverse(X3))) ) ).
cnf(u327,axiom,
( ~ subgroup_member(multiply(X3,multiply(X1,multiply(X2,inverse(X0)))))
| ~ subgroup_member(X0)
| subgroup_member(multiply(X3,multiply(X1,X2))) ) ).
cnf(u394,axiom,
( ~ subgroup_member(multiply(X2,multiply(inverse(X0),inverse(X1))))
| ~ subgroup_member(multiply(X1,X0))
| subgroup_member(X2) ) ).
cnf(u351,axiom,
( ~ subgroup_member(multiply(inverse(X3),multiply(X0,X1)))
| ~ subgroup_member(X3)
| ~ subgroup_member(X2)
| subgroup_member(multiply(X0,multiply(X1,X2))) ) ).
cnf(u522,axiom,
( ~ subgroup_member(multiply(inverse(X1),X0))
| subgroup_member(multiply(inverse(X0),X1)) ) ).
cnf(u501,axiom,
( ~ subgroup_member(multiply(X2,multiply(X3,multiply(X0,X1))))
| ~ subgroup_member(multiply(inverse(X3),inverse(X2)))
| ~ subgroup_member(X4)
| subgroup_member(multiply(X0,multiply(X1,X4))) ) ).
cnf(u536,axiom,
( ~ subgroup_member(multiply(inverse(X0),multiply(X1,X3)))
| subgroup_member(multiply(X2,X3))
| ~ subgroup_member(multiply(X2,multiply(inverse(X1),X0))) ) ).
cnf(u279,axiom,
( ~ subgroup_member(multiply(X1,X0))
| ~ subgroup_member(inverse(X0))
| ~ subgroup_member(X2)
| subgroup_member(multiply(X1,X2)) ) ).
cnf(u22,axiom,
( subgroup_member(multiply(X1,multiply(X2,X0)))
| ~ subgroup_member(X0)
| ~ subgroup_member(multiply(X1,X2)) ) ).
cnf(u199,axiom,
( subgroup_member(multiply(X3,multiply(X4,multiply(X1,multiply(X2,X0)))))
| ~ subgroup_member(X0)
| ~ subgroup_member(multiply(X3,multiply(X4,multiply(X1,X2)))) ) ).
cnf(u443,axiom,
( ~ subgroup_member(multiply(X2,multiply(X3,multiply(X0,inverse(X1)))))
| subgroup_member(multiply(X2,multiply(X3,multiply(X0,X4))))
| ~ subgroup_member(multiply(X1,X4)) ) ).
cnf(u292,axiom,
( ~ subgroup_member(multiply(inverse(X1),inverse(X0)))
| subgroup_member(X2)
| ~ subgroup_member(X1)
| ~ subgroup_member(multiply(X2,X0)) ) ).
cnf(u294,axiom,
( ~ subgroup_member(multiply(inverse(X2),inverse(X1)))
| ~ subgroup_member(multiply(X1,multiply(X2,X0)))
| ~ subgroup_member(X3)
| subgroup_member(multiply(X0,X3)) ) ).
cnf(u109,axiom,
( ~ subgroup_member(multiply(X1,X0))
| ~ subgroup_member(inverse(X0))
| subgroup_member(X1) ) ).
cnf(u314,axiom,
( ~ subgroup_member(multiply(inverse(X2),multiply(inverse(X1),inverse(X0))))
| subgroup_member(X3)
| ~ subgroup_member(X2)
| ~ subgroup_member(multiply(X3,multiply(X0,X1))) ) ).
cnf(u111,axiom,
( ~ subgroup_member(multiply(X1,multiply(X2,inverse(X0))))
| ~ subgroup_member(X0)
| subgroup_member(multiply(X1,X2)) ) ).
cnf(u51,axiom,
( ~ subgroup_member(multiply(X2,inverse(X1)))
| ~ subgroup_member(multiply(X1,X0))
| subgroup_member(multiply(X2,X0)) ) ).
cnf(u398,axiom,
( ~ subgroup_member(multiply(inverse(X0),inverse(X1)))
| subgroup_member(multiply(X1,X0)) ) ).
cnf(u392,axiom,
( ~ subgroup_member(multiply(X1,X0))
| subgroup_member(multiply(inverse(X0),inverse(X1))) ) ).
cnf(u95,axiom,
( ~ subgroup_member(multiply(X2,X0))
| ~ subgroup_member(inverse(X2))
| ~ subgroup_member(X1)
| subgroup_member(multiply(X0,X1)) ) ).
cnf(u565,axiom,
( ~ subgroup_member(inverse(X0))
| ~ subgroup_member(X1)
| subgroup_member(multiply(inverse(X1),X0)) ) ).
cnf(u467,axiom,
( ~ subgroup_member(multiply(X1,multiply(X2,X0)))
| subgroup_member(multiply(inverse(X0),multiply(inverse(X2),inverse(X1)))) ) ).
cnf(u84,axiom,
inverse(inverse(X0)) = X0 ).
cnf(u257,axiom,
( subgroup_member(multiply(X1,multiply(X0,X2)))
| ~ subgroup_member(X1)
| ~ subgroup_member(X0)
| ~ subgroup_member(X2) ) ).
cnf(u485,axiom,
( ~ subgroup_member(multiply(X3,multiply(X0,X1)))
| ~ subgroup_member(X2)
| subgroup_member(multiply(inverse(X2),multiply(inverse(X1),multiply(inverse(X0),inverse(X3))))) ) ).
cnf(u377,axiom,
( ~ subgroup_member(multiply(X2,multiply(inverse(X0),X1)))
| ~ subgroup_member(multiply(X0,inverse(X2)))
| subgroup_member(X1) ) ).
cnf(u93,axiom,
( ~ subgroup_member(inverse(X0))
| subgroup_member(X0) ) ).
cnf(u379,axiom,
( ~ subgroup_member(multiply(inverse(X0),multiply(X1,X2)))
| ~ subgroup_member(multiply(inverse(X1),X0))
| subgroup_member(X2) ) ).
cnf(u431,axiom,
( ~ subgroup_member(multiply(X3,X2))
| subgroup_member(multiply(X0,multiply(X1,X2)))
| ~ subgroup_member(inverse(X3))
| ~ subgroup_member(multiply(X0,X1)) ) ).
cnf(associativity,axiom,
multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)) ).
cnf(u360,axiom,
( ~ subgroup_member(multiply(X3,X1))
| ~ subgroup_member(inverse(X3))
| ~ subgroup_member(X0)
| ~ subgroup_member(X2)
| subgroup_member(multiply(X0,multiply(X1,X2))) ) ).
cnf(u251,axiom,
( subgroup_member(multiply(inverse(X1),multiply(X0,X2)))
| ~ subgroup_member(X0)
| ~ subgroup_member(inverse(X1))
| ~ subgroup_member(X2) ) ).
cnf(u202,axiom,
( ~ subgroup_member(multiply(X2,multiply(X3,X1)))
| ~ subgroup_member(multiply(inverse(X1),X0))
| subgroup_member(multiply(X2,multiply(X3,X0))) ) ).
cnf(u375,axiom,
( ~ subgroup_member(multiply(X0,multiply(X1,X2)))
| subgroup_member(X2)
| ~ subgroup_member(inverse(X0))
| ~ subgroup_member(inverse(X1)) ) ).
cnf(u288,axiom,
( ~ subgroup_member(multiply(X3,multiply(inverse(X0),inverse(X2))))
| subgroup_member(multiply(X3,X1))
| ~ subgroup_member(multiply(X2,multiply(X0,X1))) ) ).
cnf(u286,axiom,
( ~ subgroup_member(multiply(inverse(X2),inverse(X1)))
| ~ subgroup_member(multiply(X1,multiply(X2,X0)))
| subgroup_member(X0) ) ).
cnf(u543,axiom,
( ~ subgroup_member(multiply(X3,multiply(inverse(X2),multiply(inverse(X0),inverse(X1)))))
| ~ subgroup_member(multiply(X1,multiply(X0,multiply(X2,X4))))
| subgroup_member(multiply(X3,X4)) ) ).
cnf(u322,axiom,
( ~ subgroup_member(multiply(X2,inverse(X0)))
| subgroup_member(multiply(X1,X2))
| ~ subgroup_member(X0)
| ~ subgroup_member(X1) ) ).
cnf(u196,axiom,
( ~ subgroup_member(multiply(X1,multiply(X2,X3)))
| ~ subgroup_member(X0)
| subgroup_member(multiply(X2,multiply(X3,X0)))
| ~ subgroup_member(inverse(X1)) ) ).
cnf(u266,axiom,
inverse(multiply(X1,X0)) = multiply(inverse(X0),inverse(X1)) ).
cnf(u405,axiom,
( ~ subgroup_member(multiply(inverse(X0),multiply(inverse(X1),X2)))
| subgroup_member(X2)
| ~ subgroup_member(multiply(X1,X0)) ) ).
cnf(u404,axiom,
( ~ subgroup_member(multiply(inverse(X2),multiply(inverse(X0),inverse(X1))))
| ~ subgroup_member(multiply(X1,multiply(X0,multiply(X2,X3))))
| subgroup_member(X3) ) ).
cnf(u58,axiom,
( ~ subgroup_member(multiply(X1,inverse(X0)))
| ~ subgroup_member(X0)
| subgroup_member(X1) ) ).
cnf(u399,axiom,
( ~ subgroup_member(multiply(X3,multiply(X2,multiply(inverse(X0),inverse(X1)))))
| ~ subgroup_member(multiply(X1,X0))
| subgroup_member(multiply(X3,X2)) ) ).
cnf(u371,axiom,
( ~ subgroup_member(multiply(inverse(X2),inverse(X1)))
| ~ subgroup_member(multiply(X1,multiply(X2,X0)))
| subgroup_member(multiply(X3,X0))
| ~ subgroup_member(X3) ) ).
cnf(u533,axiom,
( ~ subgroup_member(multiply(X2,multiply(inverse(X0),X3)))
| subgroup_member(multiply(X1,X3))
| ~ subgroup_member(multiply(X1,multiply(X0,inverse(X2)))) ) ).
cnf(u50,axiom,
( subgroup_member(multiply(X3,multiply(X1,multiply(X2,X0))))
| ~ subgroup_member(X0)
| ~ subgroup_member(multiply(X3,multiply(X1,X2))) ) ).
cnf(u185,axiom,
( ~ subgroup_member(multiply(inverse(X1),X0))
| subgroup_member(X0)
| ~ subgroup_member(X1) ) ).
cnf(u479,axiom,
( ~ subgroup_member(multiply(X2,X0))
| ~ subgroup_member(X1)
| subgroup_member(multiply(inverse(X1),multiply(inverse(X0),inverse(X2)))) ) ).
cnf(u60,axiom,
identity = inverse(identity) ).
cnf(u554,axiom,
( ~ subgroup_member(multiply(X1,X2))
| ~ subgroup_member(X1)
| ~ subgroup_member(X0)
| subgroup_member(multiply(inverse(X0),X2)) ) ).
cnf(u432,axiom,
( ~ subgroup_member(multiply(X1,inverse(X3)))
| ~ subgroup_member(multiply(X3,X2))
| subgroup_member(multiply(X0,multiply(X1,X2)))
| ~ subgroup_member(X0) ) ).
cnf(u3,axiom,
identity = multiply(inverse(X0),X0) ).
cnf(u7,axiom,
( subgroup_member(multiply(X0,X1))
| ~ subgroup_member(X1)
| ~ subgroup_member(X0) ) ).
cnf(left_identity,axiom,
multiply(identity,X0) = X0 ).
cnf(u350,axiom,
( ~ subgroup_member(multiply(inverse(X2),X0))
| ~ subgroup_member(X2)
| ~ subgroup_member(X1)
| subgroup_member(multiply(X0,X1)) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP398-3 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.17/0.43 % Computer : n005.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sun Sep 27 10:01:32 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.23/0.48 Running first-order theorem proving
% 0.23/0.48 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
% 12.85/2.87 % (3755331)Input is clausal, will run a generic CNF schedule.
% 12.85/2.87 % (3755339)lrs+10_1_sil=8000:sp=occurrence:random_seed=3244407391:i=107:sd=3:ss=axioms:sgt=8_3000 on theBenchmark for (3000ds/107Mi)
% 12.85/2.87 % (3755339)Refutation not found, incomplete strategy
% 12.85/2.87 % (3755339)------------------------------
% 12.85/2.87 % (3755339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/2.87 % (3755339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/2.87 % (3755339)CaDiCaL version: 2.1.3
% 12.85/2.87 % (3755339)Termination reason: Refutation not found, incomplete strategy
% 12.85/2.87 % (3755339)Time elapsed: 0.001 s
% 12.85/2.87 % (3755339)Peak memory usage: 86 MB
% 12.85/2.87 % (3755338)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1683101761:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_3000 on theBenchmark for (3000ds/137899Mi)
% 12.85/2.87 % (3755337)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4076127895:i=132376:av=off_3000 on theBenchmark for (3000ds/132376Mi)
% 12.85/2.87 % (3755336)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=3071348090:i=140167_3000 on theBenchmark for (3000ds/140167Mi)
% 12.85/2.87 % (3755341)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=784071692:s2a=on:i=180:gtg=position_3000 on theBenchmark for (3000ds/180Mi)
% 12.85/2.87 % (3755342)dis-21_1_sil=8000:lcm=predicate:random_seed=2046540264:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_3000 on theBenchmark for (3000ds/117Mi)
% 12.85/2.87 % (3755340)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3794845864:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_3000 on theBenchmark for (3000ds/114Mi)
% 12.85/2.87 % (3755340)Refutation not found, incomplete strategy
% 12.85/2.87 % (3755340)------------------------------
% 12.85/2.87 % (3755340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/2.87 % (3755342)Refutation not found, incomplete strategy
% 12.85/2.87 % (3755342)------------------------------
% 12.85/2.88 % (3755342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/2.88 % (3755342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/2.88 % (3755340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/2.88 % (3755340)CaDiCaL version: 2.1.3
% 12.85/2.88 % (3755342)CaDiCaL version: 2.1.3
% 12.85/2.88 % (3755340)Termination reason: Refutation not found, incomplete strategy
% 12.85/2.88 % (3755340)Time elapsed: 0.001 s
% 12.85/2.88 % (3755340)Peak memory usage: 86 MB
% 12.85/2.88 % (3755342)Termination reason: Refutation not found, incomplete strategy
% 12.85/2.88 % (3755342)Time elapsed: 0.001 s
% 12.85/2.88 % (3755342)Peak memory usage: 86 MB
% 12.85/2.88 % (3755339)------------------------------
% 12.85/2.88 % (3755339)------------------------------
% 12.85/2.88 % (3755341)Instruction limit reached!
% 12.85/2.88 % (3755341)------------------------------
% 12.85/2.88 % (3755341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/2.88 % (3755341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/2.88 % (3755341)CaDiCaL version: 2.1.3
% 12.85/2.88 % (3755341)Termination reason: Instruction limit
% 12.85/2.88 % (3755341)Termination phase: Saturation
% 12.85/2.88 % (3755341)Time elapsed: 0.172 s
% 12.85/2.88 % (3755341)Peak memory usage: 90 MB
% 12.85/2.88 % (3755341)Instructions burned: 180 (million)
% 12.85/2.88 % (3755350)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=2138847939:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 12.85/2.88 % (3755350)Refutation not found, incomplete strategy
% 12.85/2.88 % (3755350)------------------------------
% 12.85/2.88 % (3755350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/2.88 % (3755350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/2.88 % (3755350)CaDiCaL version: 2.1.3
% 12.85/2.88 % (3755350)Termination reason: Refutation not found, incomplete strategy
% 12.85/2.88 % (3755350)Time elapsed: 0.0000 s
% 12.85/2.88 % (3755350)Peak memory usage: 86 MB
% 12.85/2.88 % (3755342)------------------------------
% 12.85/2.88 % (3755342)------------------------------
% 12.85/2.88 % (3755340)------------------------------
% 20.32/3.90 % (3755340)------------------------------
% 20.32/3.90 % (3755351)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3449884238:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 20.32/3.90 % (3755351)Refutation not found, incomplete strategy
% 20.32/3.90 % (3755351)------------------------------
% 20.32/3.90 % (3755351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.90 % (3755351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.90 % (3755351)CaDiCaL version: 2.1.3
% 20.32/3.90 % (3755351)Termination reason: Refutation not found, incomplete strategy
% 20.32/3.90 % (3755351)Time elapsed: 0.001 s
% 20.32/3.90 % (3755351)Peak memory usage: 86 MB
% 20.32/3.90 % (3755353)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=118660779:st=4:i=219:sd=3:ss=axioms_2993 on theBenchmark for (2993ds/219Mi)
% 20.32/3.90 % (3755354)lrs+10_64_to=lpo:sil=8000:random_seed=4202419463:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 20.32/3.90 % (3755353)Refutation not found, incomplete strategy
% 20.32/3.90 % (3755353)------------------------------
% 20.32/3.90 % (3755353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.90 % (3755353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.90 % (3755353)CaDiCaL version: 2.1.3
% 20.32/3.90 % (3755353)Termination reason: Refutation not found, incomplete strategy
% 20.32/3.90 % (3755353)Time elapsed: 0.001 s
% 20.32/3.90 % (3755353)Peak memory usage: 86 MB
% 20.32/3.90 % (3755350)------------------------------
% 20.32/3.90 % (3755350)------------------------------
% 20.32/3.90 % (3755354)Instruction limit reached!
% 20.32/3.90 % (3755354)------------------------------
% 20.32/3.90 % (3755354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.90 % (3755354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.90 % (3755354)CaDiCaL version: 2.1.3
% 20.32/3.90 % (3755354)Termination reason: Instruction limit
% 20.32/3.90 % (3755354)Termination phase: Saturation
% 20.32/3.90 % (3755354)Time elapsed: 0.126 s
% 20.32/3.90 % (3755354)Peak memory usage: 88 MB
% 20.32/3.90 % (3755354)Instructions burned: 126 (million)
% 20.32/3.90 % (3755351)------------------------------
% 20.32/3.90 % (3755351)------------------------------
% 20.32/3.90 % (3755359)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2781725482:avsq=on:i=194:fgj=on:bd=preordered_2990 on theBenchmark for (2990ds/194Mi)
% 20.32/3.90 % (3755353)------------------------------
% 20.32/3.90 % (3755353)------------------------------
% 20.32/3.90 % (3755360)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1619300066:i=157:gtg=all_2989 on theBenchmark for (2989ds/157Mi)
% 20.32/3.90 % (3755361)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4156836566:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 20.32/3.90 % (3755359)Instruction limit reached!
% 20.32/3.90 % (3755359)------------------------------
% 20.32/3.90 % (3755359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.90 % (3755359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.90 % (3755359)CaDiCaL version: 2.1.3
% 20.32/3.90 % (3755359)Termination reason: Instruction limit
% 20.32/3.90 % (3755359)Termination phase: Saturation
% 20.32/3.90 % (3755359)Time elapsed: 0.201 s
% 20.32/3.90 % (3755359)Peak memory usage: 89 MB
% 20.32/3.90 % (3755359)Instructions burned: 195 (million)
% 20.32/3.90 % (3755360)Instruction limit reached!
% 20.32/3.90 % (3755360)------------------------------
% 20.32/3.90 % (3755360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.90 % (3755360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.90 % (3755360)CaDiCaL version: 2.1.3
% 20.32/3.90 % (3755360)Termination reason: Instruction limit
% 20.32/3.90 % (3755360)Termination phase: Saturation
% 20.32/3.90 % (3755360)Time elapsed: 0.159 s
% 20.32/3.90 % (3755360)Peak memory usage: 89 MB
% 20.32/3.90 % (3755360)Instructions burned: 157 (million)
% 20.32/3.90 % (3755365)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3372704506:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2986 on theBenchmark for (2986ds/106Mi)
% 20.32/3.90 % (3755365)Refutation not found, incomplete strategy
% 20.32/3.90 % (3755365)------------------------------
% 20.32/3.90 % (3755365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.90 % (3755365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.90 % (3755365)CaDiCaL version: 2.1.3
% 20.32/3.90 % (3755365)Termination reason: Refutation not found, incomplete strategy
% 20.32/3.90 % (3755365)Time elapsed: 0.001 s
% 20.32/3.90 % (3755365)Peak memory usage: 86 MB
% 20.32/3.90 % (3755368)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1080561242:i=107_2985 on theBenchmark for (2985ds/107Mi)
% 20.32/3.90 % (3755368)Refutation not found, incomplete strategy
% 20.32/3.90 % (3755368)------------------------------
% 20.32/3.90 % (3755368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.90 % (3755368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.90 % (3755368)CaDiCaL version: 2.1.3
% 20.32/3.90 % (3755368)Termination reason: Refutation not found, incomplete strategy
% 20.32/3.90 % (3755368)Time elapsed: 0.001 s
% 20.32/3.90 % (3755368)Peak memory usage: 87 MB
% 20.32/3.90 % (3755369)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1341833578:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2984 on theBenchmark for (2984ds/242Mi)
% 20.32/3.90 % (3755369)Refutation not found, incomplete strategy
% 20.32/3.90 % (3755369)------------------------------
% 20.32/3.90 % (3755369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.90 % (3755369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.90 % (3755369)CaDiCaL version: 2.1.3
% 20.32/3.90 % (3755369)Termination reason: Refutation not found, incomplete strategy
% 20.32/3.90 % (3755369)Time elapsed: 0.001 s
% 20.32/3.90 % (3755369)Peak memory usage: 86 MB
% 20.32/3.90 [W927 10:01:34.576609565 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.32/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.32/3.90 [W927 10:01:34.576656406 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.32/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.32/3.90 [W927 10:01:34.576717029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.32/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.32/3.90 [W927 10:01:34.576736839 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.32/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.32/3.90 [W927 10:01:34.576781386 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.32/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.32/3.90 [W927 10:01:34.576800476 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.32/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.32/3.90 [W927 10:01:34.576843489 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.32/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.32/3.90 [W927 10:01:34.576861956 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.32/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.32/3.90 [W927 10:01:34.576903146 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.32/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.32/3.90 [W927 10:01:34.576987346 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.32/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.32/3.90 [W927 10:01:34.577054306 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.32/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.32/3.90 [W927 10:01:34.577071529 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.32/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.32/3.90 % (3755365)------------------------------
% 20.32/3.90 % (3755365)------------------------------
% 20.32/3.90 % (3755368)------------------------------
% 20.32/3.90 % (3755368)------------------------------
% 20.32/3.90 % (3755369)------------------------------
% 20.32/3.90 % (3755369)------------------------------
% 20.32/3.90 % (3755361)Refutation not found, incomplete strategy
% 20.32/3.90 % (3755361)------------------------------
% 20.32/3.90 % (3755361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.90 % (3755361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.90 % (3755361)CaDiCaL version: 2.1.3
% 20.32/3.90 % (3755361)Termination reason: Refutation not found, incomplete strategy
% 20.32/3.90 % (3755361)Time elapsed: 0.880 s
% 20.32/3.90 % (3755361)Peak memory usage: 125 MB
% 20.32/3.90 % (3755361)Instructions burned: 825 (million)
% 20.32/3.90 % (3755377)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3037854866:cond=fast:i=5208:av=off_2979 on theBenchmark for (2979ds/5208Mi)
% 20.32/3.90 % (3755379)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4114025002:i=134:sd=2:doe=on:ss=axioms:sgt=14_2978 on theBenchmark for (2978ds/134Mi)
% 20.32/3.90 % (3755379)Refutation not found, incomplete strategy
% 20.32/3.90 % (3755379)------------------------------
% 20.32/3.90 % (3755379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.90 % (3755379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.90 % (3755379)CaDiCaL version: 2.1.3
% 20.32/3.90 % (3755379)Termination reason: Refutation not found, incomplete strategy
% 20.32/3.90 % (3755379)Time elapsed: 0.001 s
% 20.32/3.90 % (3755379)Peak memory usage: 86 MB
% 20.32/3.90 % (3755380)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2748511499:i=499:bd=all_2977 on theBenchmark for (2977ds/499Mi)
% 20.32/3.90 % (3755380)First to succeed.
% 20.32/3.90 % (3755380)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3755331"
% 20.32/3.90 % (3755361)------------------------------
% 20.32/3.90 % (3755361)------------------------------
% 20.32/3.90 % (3755379)------------------------------
% 20.32/3.90 % (3755379)------------------------------
% 20.32/3.90 % (3755384)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3099473652:i=191:fgj=on:bd=all_2973 on theBenchmark for (2973ds/191Mi)
% 20.32/3.90 % (3755384)Instruction limit reached!
% 20.32/3.90 % (3755384)------------------------------
% 20.32/3.90 % (3755384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.90 % (3755384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.90 % (3755384)CaDiCaL version: 2.1.3
% 20.32/3.90 % (3755384)Termination reason: Instruction limit
% 20.32/3.90 % (3755384)Termination phase: Saturation
% 20.32/3.90 % (3755384)Time elapsed: 0.114 s
% 20.32/3.90 % (3755384)Peak memory usage: 89 MB
% 20.32/3.90 % (3755384)Instructions burned: 192 (million)
% 20.32/3.90 % SZS status Satisfiable for theBenchmark
% 22.09/4.12 % SZS output start Saturation.
% See solution above
% 22.09/4.12 % SZS output start Definitions and Model Updates.
% 22.09/4.12 % SZS output end Definitions and Model Updates.
% 22.09/4.12 % (3755380)------------------------------
% 22.09/4.12 % (3755380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.09/4.12 % (3755380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.09/4.12 % (3755380)CaDiCaL version: 2.1.3
% 22.09/4.12 % (3755380)Termination reason: Satisfiable
% 22.09/4.12 % (3755380)Time elapsed: 0.069 s
% 22.09/4.12 % (3755380)Peak memory usage: 90 MB
% 22.09/4.12 % (3755380)Instructions burned: 58 (million)
% 22.09/4.12 % (3755380)------------------------------
% 22.09/4.12 % (3755380)------------------------------
% 22.09/4.12 % (3755331)Success in time 3.049 s
% 22.09/4.12 % Vampire exiting
%------------------------------------------------------------------------------