%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP130-4.004 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:01 AM UTC 2026
% Result : Satisfiable 3.94s 1.55s
% Output : Saturation 5.40s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u36,axiom,
~ product(e_4,e_4,e_1) ).
cnf(u41,axiom,
product(e_3,e_4,e_1) ).
cnf(u44,axiom,
~ product(e_2,e_4,e_1) ).
cnf(u48,axiom,
~ product(e_1,e_4,e_1) ).
cnf(u53,axiom,
~ product(e_4,e_3,e_1) ).
cnf(u57,axiom,
~ product(e_3,e_3,e_1) ).
cnf(u62,axiom,
product(e_2,e_3,e_1) ).
cnf(u71,axiom,
product(e_4,e_2,e_1) ).
cnf(u74,axiom,
~ product(e_3,e_2,e_1) ).
cnf(u78,axiom,
~ product(e_2,e_2,e_1) ).
cnf(u82,axiom,
~ product(e_1,e_2,e_1) ).
cnf(u87,axiom,
~ product(e_4,e_1,e_1) ).
cnf(u91,axiom,
~ product(e_3,e_1,e_1) ).
cnf(u95,axiom,
~ product(e_2,e_1,e_1) ).
cnf(u100,axiom,
product(e_1,e_1,e_1) ).
cnf(u386,negated_conjecture,
~ product(e_4,e_4,e_2) ).
cnf(u390,negated_conjecture,
~ product(e_3,e_4,e_2) ).
cnf(u395,negated_conjecture,
product(e_1,e_4,e_2) ).
cnf(u400,negated_conjecture,
product(e_4,e_3,e_2) ).
cnf(u403,negated_conjecture,
~ product(e_3,e_3,e_2) ).
cnf(u407,negated_conjecture,
~ product(e_1,e_3,e_2) ).
cnf(u412,negated_conjecture,
~ product(e_4,e_2,e_2) ).
cnf(u416,negated_conjecture,
~ product(e_3,e_2,e_2) ).
cnf(u420,negated_conjecture,
~ product(e_1,e_2,e_2) ).
cnf(u425,negated_conjecture,
~ product(e_4,e_1,e_2) ).
cnf(u430,negated_conjecture,
product(e_3,e_1,e_2) ).
cnf(u433,negated_conjecture,
~ product(e_1,e_1,e_2) ).
cnf(u449,axiom,
product(e_2,e_2,e_2) ).
cnf(u453,axiom,
~ product(e_2,e_1,e_2) ).
cnf(u599,axiom,
~ product(e_4,e_4,e_3) ).
cnf(u608,axiom,
product(e_2,e_4,e_3) ).
cnf(u621,axiom,
product(e_3,e_3,e_3) ).
cnf(u624,axiom,
~ product(e_2,e_3,e_3) ).
cnf(u634,axiom,
product(e_4,e_1,e_3) ).
cnf(u789,axiom,
product(e_4,e_4,e_4) ).
cnf(u813,axiom,
~ product(e_2,e_3,e_4) ).
cnf(u818,axiom,
product(e_1,e_3,e_4) ).
cnf(u831,axiom,
product(e_2,e_1,e_4) ).
cnf(u834,axiom,
~ product(e_1,e_1,e_4) ).
cnf(u228,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_1)
| product(X0,e_2,e_1)
| product(X0,e_3,e_1)
| product(X0,e_4,e_1) ) ).
cnf(qg3_1,negated_conjecture,
( ~ product(X3,X1,X0)
| product(X0,X1,X2)
| ~ product(X0,X2,X3) ) ).
cnf(u752,negated_conjecture,
( ~ product(e_3,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u928,negated_conjecture,
( ~ product(e_2,e_1,X0)
| product(e_2,X0,e_3) ) ).
cnf(u543,negated_conjecture,
equalish(e_4,e_4) ).
cnf(u578,negated_conjecture,
( ~ product(e_2,e_3,X0)
| product(e_2,X0,e_4) ) ).
cnf(product_total_function2,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u986,axiom,
( ~ product(e_4,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u502,negated_conjecture,
( ~ product(e_1,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u860,axiom,
( ~ product(X0,e_3,e_1)
| equalish(X0,e_2) ) ).
cnf(element_3,axiom,
group_element(e_3) ).
cnf(u976,axiom,
( ~ product(X0,e_1,e_3)
| equalish(X0,e_4) ) ).
cnf(u927,negated_conjecture,
( ~ product(e_3,X0,e_1)
| product(e_2,X0,e_3) ) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(u754,negated_conjecture,
( ~ product(e_4,e_2,X0)
| product(e_4,X0,e_3) ) ).
cnf(u990,negated_conjecture,
( ~ product(e_4,X0,e_4)
| product(e_4,e_4,X0) ) ).
cnf(qg3,negated_conjecture,
( ~ product(X0,X2,X3)
| ~ product(X0,X1,X2)
| product(X3,X1,X0) ) ).
cnf(u977,axiom,
( ~ product(e_4,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u911,negated_conjecture,
( ~ product(e_2,X0,e_2)
| product(e_2,e_2,X0) ) ).
cnf(u950,negated_conjecture,
( ~ product(e_3,e_4,X0)
| product(e_3,X0,e_2) ) ).
cnf(u336,negated_conjecture,
( ~ product(e_1,e_1,X0)
| product(e_1,X0,e_1) ) ).
cnf(u989,negated_conjecture,
( ~ product(e_4,e_4,X0)
| product(e_4,X0,e_4) ) ).
cnf(u1024,axiom,
( ~ product(e_2,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u732,negated_conjecture,
( ~ product(X0,e_2,e_3)
| equalish(X0,e_1) ) ).
cnf(u744,axiom,
( ~ product(e_3,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u980,negated_conjecture,
( ~ product(e_3,e_1,X0)
| product(e_3,X0,e_4) ) ).
cnf(u579,negated_conjecture,
( ~ product(e_2,X0,e_4)
| product(e_2,e_3,X0) ) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(u906,axiom,
( ~ product(X0,e_2,e_2)
| equalish(X0,e_2) ) ).
cnf(u978,axiom,
( ~ product(e_4,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(row_surjectivity,axiom,
( ~ group_element(X1)
| ~ group_element(X0)
| product(e_1,X0,X1)
| product(e_2,X0,X1)
| product(e_3,X0,X1)
| product(e_4,X0,X1) ) ).
cnf(u29,axiom,
( ~ group_element(X0)
| product(e_1,X0,e_4)
| product(e_2,X0,e_4)
| product(e_3,X0,e_4)
| product(e_4,X0,e_4) ) ).
cnf(u981,negated_conjecture,
( ~ product(e_3,X0,e_4)
| product(e_3,e_1,X0) ) ).
cnf(u929,negated_conjecture,
( ~ product(e_2,X0,e_3)
| product(e_2,e_1,X0) ) ).
cnf(u947,axiom,
( ~ product(e_2,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u544,negated_conjecture,
equalish(e_2,e_2) ).
cnf(u500,negated_conjecture,
product(e_1,e_2,e_3) ).
cnf(u231,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_4)
| product(X0,e_2,e_4)
| product(X0,e_3,e_4)
| product(X0,e_4,e_4) ) ).
cnf(u1027,negated_conjecture,
( ~ product(e_4,X0,e_2)
| product(e_4,e_1,X0) ) ).
cnf(u1026,negated_conjecture,
( ~ product(e_4,e_1,X0)
| product(e_4,X0,e_2) ) ).
cnf(u734,negated_conjecture,
( ~ product(e_1,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u755,negated_conjecture,
( ~ product(e_4,X0,e_3)
| product(e_4,e_2,X0) ) ).
cnf(u517,negated_conjecture,
equalish(e_3,e_3) ).
cnf(u745,axiom,
( ~ product(e_3,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(u367,axiom,
equalish(e_1,e_1) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(u900,axiom,
( ~ product(e_4,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u751,negated_conjecture,
( ~ product(e_3,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u1023,axiom,
( ~ product(e_2,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u954,axiom,
( ~ product(X0,e_3,e_3)
| equalish(X0,e_3) ) ).
cnf(u1014,negated_conjecture,
( ~ product(e_4,e_3,X0)
| product(e_4,X0,e_1) ) ).
cnf(u743,axiom,
( ~ product(X0,e_4,e_1)
| equalish(X0,e_3) ) ).
cnf(u737,negated_conjecture,
( ~ product(e_3,X0,e_1)
| product(e_3,e_2,X0) ) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(u908,axiom,
( ~ product(e_2,e_2,X0)
| equalish(X0,e_2) ) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u902,negated_conjecture,
( ~ product(e_1,e_2,X0)
| product(e_1,X0,e_4) ) ).
cnf(u951,negated_conjecture,
( ~ product(e_3,X0,e_2)
| product(e_3,e_4,X0) ) ).
cnf(u735,negated_conjecture,
( ~ product(e_1,X0,e_2)
| product(e_3,X0,e_1) ) ).
cnf(u333,axiom,
( ~ product(e_1,X0,e_1)
| equalish(X0,e_1) ) ).
cnf(u505,negated_conjecture,
( ~ product(e_2,e_4,X0)
| product(e_2,X0,e_1) ) ).
cnf(u956,axiom,
( ~ product(e_3,e_3,X0)
| equalish(X0,e_3) ) ).
cnf(u1011,axiom,
( ~ product(e_1,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(product_right_cancellation,axiom,
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u948,axiom,
( ~ product(e_2,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u910,negated_conjecture,
( ~ product(e_2,e_2,X0)
| product(e_2,X0,e_2) ) ).
cnf(u26,axiom,
( ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_2,X0,e_1)
| product(e_3,X0,e_1)
| product(e_4,X0,e_1) ) ).
cnf(u987,axiom,
( ~ product(e_4,e_4,X0)
| equalish(X0,e_4) ) ).
cnf(u1015,negated_conjecture,
( ~ product(e_4,X0,e_1)
| product(e_4,e_3,X0) ) ).
cnf(u946,axiom,
( ~ product(X0,e_4,e_3)
| equalish(X0,e_2) ) ).
cnf(u506,negated_conjecture,
( ~ product(e_2,X0,e_1)
| product(e_2,e_4,X0) ) ).
cnf(qg3_2,negated_conjecture,
( ~ product(X2,X3,X0)
| product(X0,X1,X2)
| ~ product(X0,X3,X1) ) ).
cnf(u958,negated_conjecture,
( ~ product(e_3,e_3,X0)
| product(e_3,X0,e_3) ) ).
cnf(u352,axiom,
( ~ group_element(X0)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4) ) ).
cnf(u864,negated_conjecture,
( ~ product(e_1,e_3,X0)
| product(e_1,X0,e_2) ) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(u748,negated_conjecture,
( ~ product(e_1,X0,e_3)
| product(e_1,e_4,X0) ) ).
cnf(column_surjectivity,axiom,
( ~ group_element(X1)
| ~ group_element(X0)
| product(X0,e_1,X1)
| product(X0,e_2,X1)
| product(X0,e_3,X1)
| product(X0,e_4,X1) ) ).
cnf(u746,negated_conjecture,
( ~ product(e_3,X0,e_4)
| product(e_1,X0,e_3) ) ).
cnf(u925,negated_conjecture,
( ~ product(e_3,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u898,axiom,
( ~ product(X0,e_2,e_1)
| equalish(X0,e_4) ) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u351,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4) ) ).
cnf(u574,negated_conjecture,
( ~ product(X0,e_3,e_2)
| equalish(X0,e_4) ) ).
cnf(u736,negated_conjecture,
( ~ product(e_3,e_2,X0)
| product(e_3,X0,e_1) ) ).
cnf(u863,negated_conjecture,
( ~ product(e_2,X0,e_3)
| product(e_1,X0,e_2) ) ).
cnf(u949,negated_conjecture,
( ~ product(e_2,X0,e_4)
| product(e_3,X0,e_2) ) ).
cnf(u907,axiom,
( ~ product(e_2,X0,e_2)
| equalish(X0,e_2) ) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(u750,negated_conjecture,
( ~ product(X0,e_2,e_4)
| equalish(X0,e_3) ) ).
cnf(u577,negated_conjecture,
( ~ product(e_4,X0,e_3)
| product(e_2,X0,e_4) ) ).
cnf(product_total_function1,axiom,
( ~ group_element(X1)
| ~ group_element(X0)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4) ) ).
cnf(u985,axiom,
( ~ product(X0,e_4,e_4)
| equalish(X0,e_4) ) ).
cnf(product_left_cancellation,axiom,
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u332,axiom,
( ~ product(X0,e_1,e_1)
| equalish(X0,e_1) ) ).
cnf(u504,negated_conjecture,
( ~ product(e_1,X0,e_4)
| product(e_2,X0,e_1) ) ).
cnf(u979,negated_conjecture,
( ~ product(e_4,X0,e_1)
| product(e_3,X0,e_4) ) ).
cnf(u747,negated_conjecture,
( ~ product(e_1,e_4,X0)
| product(e_1,X0,e_3) ) ).
cnf(u861,axiom,
( ~ product(e_2,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(u753,negated_conjecture,
( ~ product(e_3,X0,e_2)
| product(e_4,X0,e_3) ) ).
cnf(u28,axiom,
( ~ group_element(X0)
| product(e_1,X0,e_3)
| product(e_2,X0,e_3)
| product(e_3,X0,e_3)
| product(e_4,X0,e_3) ) ).
cnf(u575,negated_conjecture,
( ~ product(e_4,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u503,negated_conjecture,
( ~ product(e_1,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(u955,axiom,
( ~ product(e_3,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(u862,axiom,
( ~ product(e_2,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u899,axiom,
( ~ product(e_4,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u742,negated_conjecture,
product(e_3,e_2,e_4) ).
cnf(u334,axiom,
( ~ product(e_1,e_1,X0)
| equalish(X0,e_1) ) ).
cnf(u901,negated_conjecture,
( ~ product(e_4,X0,e_2)
| product(e_1,X0,e_4) ) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(u926,negated_conjecture,
( ~ product(e_3,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(u959,negated_conjecture,
( ~ product(e_3,X0,e_3)
| product(e_3,e_3,X0) ) ).
cnf(u865,negated_conjecture,
( ~ product(e_1,X0,e_2)
| product(e_1,e_3,X0) ) ).
cnf(u903,negated_conjecture,
( ~ product(e_1,X0,e_4)
| product(e_1,e_2,X0) ) ).
cnf(u1022,axiom,
( ~ product(X0,e_1,e_4)
| equalish(X0,e_2) ) ).
cnf(u353,axiom,
( ~ group_element(X0)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4) ) ).
cnf(u337,negated_conjecture,
( ~ product(e_1,X0,e_1)
| product(e_1,e_1,X0) ) ).
cnf(u733,negated_conjecture,
( ~ product(e_1,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u230,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_3)
| product(X0,e_2,e_3)
| product(X0,e_3,e_3)
| product(X0,e_4,e_3) ) ).
cnf(u1025,negated_conjecture,
( ~ product(e_2,X0,e_1)
| product(e_4,X0,e_2) ) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(u924,negated_conjecture,
( ~ product(X0,e_1,e_2)
| equalish(X0,e_3) ) ).
cnf(u576,negated_conjecture,
( ~ product(e_4,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(u27,axiom,
( ~ group_element(X0)
| product(e_1,X0,e_2)
| product(e_2,X0,e_2)
| product(e_3,X0,e_2)
| product(e_4,X0,e_2) ) ).
cnf(u1012,axiom,
( ~ product(e_1,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(u354,axiom,
( ~ group_element(X0)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4) ) ).
cnf(u1010,axiom,
( ~ product(X0,e_3,e_4)
| equalish(X0,e_1) ) ).
cnf(u1013,negated_conjecture,
( ~ product(e_1,X0,e_3)
| product(e_4,X0,e_1) ) ).
cnf(u501,negated_conjecture,
( ~ product(X0,e_4,e_2)
| equalish(X0,e_1) ) ).
cnf(u229,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_2,e_2)
| product(X0,e_3,e_2)
| product(X0,e_4,e_2) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP130-4.004 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n015.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 09:32:01 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 3.94/1.55 % (1398677)Input is clausal, will run a generic CNF schedule.
% 3.94/1.55 % (1398687)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=540453150:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.94/1.55 % (1398688)dis-21_1_sil=8000:lcm=predicate:random_seed=2182851602: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)
% 3.94/1.55 % (1398684)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2281212540:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.94/1.55 % (1398685)lrs+10_1_sil=8000:sp=occurrence:random_seed=462159981:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.94/1.55 % (1398683)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1199722290:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.94/1.55 % (1398682)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=3799642984:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.94/1.55 % (1398686)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=100113364:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.94/1.55 % (1398685)Refutation not found, incomplete strategy
% 3.94/1.55 % (1398685)------------------------------
% 3.94/1.55 % (1398685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.55 % (1398685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.55 % (1398685)CaDiCaL version: 2.1.3
% 3.94/1.55 % (1398685)Termination reason: Refutation not found, incomplete strategy
% 3.94/1.55 % (1398685)Time elapsed: 0.001 s
% 3.94/1.55 % (1398685)Peak memory usage: 87 MB
% 3.94/1.55 % (1398687)Instruction limit reached!
% 3.94/1.55 % (1398687)------------------------------
% 3.94/1.55 % (1398687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.55 % (1398687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.55 % (1398687)CaDiCaL version: 2.1.3
% 3.94/1.55 % (1398687)Termination reason: Instruction limit
% 3.94/1.55 % (1398687)Termination phase: Saturation
% 3.94/1.55 % (1398687)Time elapsed: 0.060 s
% 3.94/1.55 % (1398687)Peak memory usage: 89 MB
% 3.94/1.55 % (1398687)Instructions burned: 180 (million)
% 3.94/1.55 % (1398686)Instruction limit reached!
% 3.94/1.55 % (1398686)------------------------------
% 3.94/1.55 % (1398686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.55 % (1398686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.55 % (1398686)CaDiCaL version: 2.1.3
% 3.94/1.55 % (1398686)Termination reason: Instruction limit
% 3.94/1.55 % (1398686)Termination phase: Saturation
% 3.94/1.55 % (1398686)Time elapsed: 0.058 s
% 3.94/1.55 % (1398686)Peak memory usage: 87 MB
% 3.94/1.55 % (1398686)Instructions burned: 115 (million)
% 3.94/1.55 % (1398688)Instruction limit reached!
% 3.94/1.55 % (1398688)------------------------------
% 3.94/1.55 % (1398688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.55 % (1398688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.55 % (1398688)CaDiCaL version: 2.1.3
% 3.94/1.55 % (1398688)Termination reason: Instruction limit
% 3.94/1.55 % (1398688)Termination phase: Saturation
% 3.94/1.55 % (1398688)Time elapsed: 0.075 s
% 3.94/1.55 % (1398688)Peak memory usage: 88 MB
% 3.94/1.55 % (1398688)Instructions burned: 117 (million)
% 3.94/1.55 % (1398696)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=1970372688:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 3.94/1.55 % (1398696)Instruction limit reached!
% 3.94/1.55 % (1398696)------------------------------
% 3.94/1.55 % (1398696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.55 % (1398696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.55 % (1398696)CaDiCaL version: 2.1.3
% 3.94/1.55 % (1398696)Termination reason: Instruction limit
% 3.94/1.55 % (1398696)Termination phase: Saturation
% 3.94/1.55 % (1398696)Time elapsed: 0.046 s
% 3.94/1.55 % (1398696)Peak memory usage: 89 MB
% 3.94/1.55 % (1398696)Instructions burned: 145 (million)
% 3.94/1.55 % (1398697)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3792352807:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 3.94/1.55 % (1398697)Refutation not found, incomplete strategy
% 3.94/1.55 % (1398697)------------------------------
% 3.94/1.55 % (1398697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.55 % (1398697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.55 % (1398697)CaDiCaL version: 2.1.3
% 3.94/1.55 % (1398697)Termination reason: Refutation not found, incomplete strategy
% 3.94/1.55 % (1398697)Time elapsed: 0.002 s
% 3.94/1.55 % (1398697)Peak memory usage: 87 MB
% 3.94/1.55 % (1398697)Instructions burned: 1 (million)
% 3.94/1.55 % (1398685)------------------------------
% 3.94/1.55 % (1398685)------------------------------
% 3.94/1.55 % (1398698)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2575660145:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 3.94/1.55 % (1398700)lrs+10_64_to=lpo:sil=8000:random_seed=1555955714:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 3.94/1.55 % (1398700)First to succeed.
% 3.94/1.55 % (1398700)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1398677"
% 3.94/1.55 % (1398698)Instruction limit reached!
% 3.94/1.55 % (1398698)------------------------------
% 3.94/1.55 % (1398698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.55 % (1398698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.55 % (1398698)CaDiCaL version: 2.1.3
% 3.94/1.55 % (1398698)Termination reason: Instruction limit
% 3.94/1.55 % (1398698)Termination phase: Saturation
% 3.94/1.55 % (1398698)Time elapsed: 0.112 s
% 3.94/1.55 % (1398698)Peak memory usage: 88 MB
% 3.94/1.55 % (1398698)Instructions burned: 219 (million)
% 3.94/1.55 % (1398703)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2675882600:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 3.94/1.55 % (1398697)------------------------------
% 3.94/1.55 % (1398697)------------------------------
% 3.94/1.55 % (1398703)Instruction limit reached!
% 3.94/1.55 % (1398703)------------------------------
% 3.94/1.55 % (1398703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.94/1.55 % (1398703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/1.55 % (1398703)CaDiCaL version: 2.1.3
% 3.94/1.55 % (1398703)Termination reason: Instruction limit
% 3.94/1.55 % (1398703)Termination phase: Saturation
% 3.94/1.55 % (1398703)Time elapsed: 0.085 s
% 3.94/1.55 % (1398703)Peak memory usage: 88 MB
% 3.94/1.55 % (1398703)Instructions burned: 196 (million)
% 3.94/1.55 % SZS status Satisfiable for theBenchmark
% 3.94/1.55 % SZS output start Saturation.
% See solution above
% 5.40/1.75 % SZS output start Definitions and Model Updates.
% 5.40/1.75 % SZS output end Definitions and Model Updates.
% 5.40/1.75 % (1398700)------------------------------
% 5.40/1.75 % (1398700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.40/1.75 % (1398700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.40/1.75 % (1398700)CaDiCaL version: 2.1.3
% 5.40/1.75 % (1398700)Termination reason: Satisfiable
% 5.40/1.75 % (1398700)Time elapsed: 0.009 s
% 5.40/1.75 % (1398700)Peak memory usage: 88 MB
% 5.40/1.75 % (1398700)Instructions burned: 26 (million)
% 5.40/1.75 % (1398700)------------------------------
% 5.40/1.75 % (1398700)------------------------------
% 5.40/1.75 % (1398677)Success in time 0.676 s
% 5.40/1.75 % Vampire exiting
%------------------------------------------------------------------------------