%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP135-2.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:04 AM UTC 2026
% Result : Satisfiable 47.89s 7.69s
% Output : Saturation 48.95s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u70,negated_conjecture,
product(e_5,e_3,e_4) ).
cnf(u73,negated_conjecture,
~ product(e_5,e_3,e_3) ).
cnf(u77,negated_conjecture,
~ product(e_5,e_3,e_2) ).
cnf(u81,negated_conjecture,
~ product(e_5,e_3,e_1) ).
cnf(u85,negated_conjecture,
~ product(e_5,e_5,e_1) ).
cnf(u89,negated_conjecture,
~ product(e_5,e_5,e_2) ).
cnf(u93,negated_conjecture,
~ product(e_5,e_5,e_4) ).
cnf(u97,negated_conjecture,
~ product(e_5,e_5,e_3) ).
cnf(u102,negated_conjecture,
~ product(e_4,e_3,e_4) ).
cnf(u106,negated_conjecture,
~ product(e_4,e_3,e_3) ).
cnf(u111,negated_conjecture,
product(e_4,e_3,e_2) ).
cnf(u114,negated_conjecture,
~ product(e_4,e_3,e_1) ).
cnf(u118,negated_conjecture,
~ product(e_5,e_4,e_1) ).
cnf(u122,negated_conjecture,
~ product(e_5,e_4,e_2) ).
cnf(u126,negated_conjecture,
~ product(e_5,e_4,e_4) ).
cnf(u131,negated_conjecture,
product(e_5,e_4,e_3) ).
cnf(u135,negated_conjecture,
~ product(e_3,e_3,e_4) ).
cnf(u140,negated_conjecture,
product(e_3,e_3,e_3) ).
cnf(u143,negated_conjecture,
~ product(e_3,e_3,e_2) ).
cnf(u147,negated_conjecture,
~ product(e_3,e_3,e_1) ).
cnf(u152,negated_conjecture,
~ product(e_2,e_3,e_4) ).
cnf(u156,negated_conjecture,
~ product(e_2,e_3,e_3) ).
cnf(u160,negated_conjecture,
~ product(e_2,e_3,e_2) ).
cnf(u165,negated_conjecture,
product(e_2,e_3,e_1) ).
cnf(u169,negated_conjecture,
product(e_5,e_2,e_1) ).
cnf(u172,negated_conjecture,
~ product(e_5,e_2,e_2) ).
cnf(u176,negated_conjecture,
~ product(e_5,e_2,e_4) ).
cnf(u180,negated_conjecture,
~ product(e_5,e_2,e_3) ).
cnf(u185,negated_conjecture,
~ product(e_1,e_3,e_4) ).
cnf(u189,negated_conjecture,
~ product(e_1,e_3,e_3) ).
cnf(u193,negated_conjecture,
~ product(e_1,e_3,e_2) ).
cnf(u197,negated_conjecture,
~ product(e_1,e_3,e_1) ).
cnf(u201,negated_conjecture,
~ product(e_5,e_1,e_1) ).
cnf(u206,negated_conjecture,
product(e_5,e_1,e_2) ).
cnf(u209,negated_conjecture,
~ product(e_5,e_1,e_4) ).
cnf(u213,negated_conjecture,
~ product(e_5,e_1,e_3) ).
cnf(u225,negated_conjecture,
~ product(e_4,e_2,e_4) ).
cnf(u230,negated_conjecture,
product(e_4,e_2,e_3) ).
cnf(u233,negated_conjecture,
~ product(e_4,e_2,e_2) ).
cnf(u237,negated_conjecture,
~ product(e_4,e_2,e_1) ).
cnf(u249,negated_conjecture,
~ product(e_3,e_2,e_4) ).
cnf(u253,negated_conjecture,
~ product(e_3,e_2,e_3) ).
cnf(u257,negated_conjecture,
~ product(e_3,e_2,e_2) ).
cnf(u261,negated_conjecture,
~ product(e_3,e_2,e_1) ).
cnf(u273,negated_conjecture,
~ product(e_2,e_2,e_4) ).
cnf(u277,negated_conjecture,
~ product(e_2,e_2,e_3) ).
cnf(u282,negated_conjecture,
product(e_2,e_2,e_2) ).
cnf(u285,negated_conjecture,
~ product(e_2,e_2,e_1) ).
cnf(u298,negated_conjecture,
product(e_1,e_2,e_4) ).
cnf(u301,negated_conjecture,
~ product(e_1,e_2,e_3) ).
cnf(u305,negated_conjecture,
~ product(e_1,e_2,e_2) ).
cnf(u309,negated_conjecture,
~ product(e_1,e_2,e_1) ).
cnf(u322,negated_conjecture,
product(e_4,e_4,e_4) ).
cnf(u325,negated_conjecture,
~ product(e_4,e_4,e_3) ).
cnf(u329,negated_conjecture,
~ product(e_4,e_4,e_2) ).
cnf(u333,negated_conjecture,
~ product(e_4,e_4,e_1) ).
cnf(u345,negated_conjecture,
~ product(e_3,e_4,e_4) ).
cnf(u349,negated_conjecture,
~ product(e_3,e_4,e_3) ).
cnf(u353,negated_conjecture,
~ product(e_3,e_4,e_2) ).
cnf(u358,negated_conjecture,
product(e_3,e_4,e_1) ).
cnf(u369,negated_conjecture,
~ product(e_2,e_4,e_4) ).
cnf(u373,negated_conjecture,
~ product(e_2,e_4,e_3) ).
cnf(u377,negated_conjecture,
~ product(e_2,e_4,e_2) ).
cnf(u381,negated_conjecture,
~ product(e_2,e_4,e_1) ).
cnf(u393,negated_conjecture,
~ product(e_1,e_4,e_4) ).
cnf(u397,negated_conjecture,
~ product(e_1,e_4,e_3) ).
cnf(u402,negated_conjecture,
product(e_1,e_4,e_2) ).
cnf(u405,negated_conjecture,
~ product(e_1,e_4,e_1) ).
cnf(u417,negated_conjecture,
~ product(e_1,e_5,e_4) ).
cnf(u422,negated_conjecture,
product(e_1,e_5,e_3) ).
cnf(u425,negated_conjecture,
~ product(e_1,e_5,e_2) ).
cnf(u429,negated_conjecture,
~ product(e_1,e_5,e_1) ).
cnf(u441,negated_conjecture,
~ product(e_3,e_5,e_4) ).
cnf(u445,negated_conjecture,
~ product(e_3,e_5,e_3) ).
cnf(u450,negated_conjecture,
product(e_3,e_5,e_2) ).
cnf(u453,negated_conjecture,
~ product(e_3,e_5,e_1) ).
cnf(u466,negated_conjecture,
product(e_2,e_5,e_4) ).
cnf(u469,negated_conjecture,
~ product(e_2,e_5,e_3) ).
cnf(u473,negated_conjecture,
~ product(e_2,e_5,e_2) ).
cnf(u477,negated_conjecture,
~ product(e_2,e_5,e_1) ).
cnf(u489,negated_conjecture,
~ product(e_4,e_5,e_4) ).
cnf(u493,negated_conjecture,
~ product(e_4,e_5,e_3) ).
cnf(u497,negated_conjecture,
~ product(e_4,e_5,e_2) ).
cnf(u502,negated_conjecture,
product(e_4,e_5,e_1) ).
cnf(u530,negated_conjecture,
product(e_5,e_5,e_5) ).
cnf(u668,negated_conjecture,
~ product(e_4,e_1,e_4) ).
cnf(u672,negated_conjecture,
~ product(e_4,e_1,e_3) ).
cnf(u676,negated_conjecture,
~ product(e_4,e_1,e_2) ).
cnf(u731,negated_conjecture,
~ product(e_2,e_1,e_4) ).
cnf(u736,negated_conjecture,
product(e_2,e_1,e_3) ).
cnf(u739,negated_conjecture,
~ product(e_2,e_1,e_2) ).
cnf(u743,negated_conjecture,
~ product(e_2,e_1,e_1) ).
cnf(u777,negated_conjecture,
product(e_3,e_1,e_4) ).
cnf(u780,negated_conjecture,
~ product(e_3,e_1,e_3) ).
cnf(u784,negated_conjecture,
~ product(e_3,e_1,e_2) ).
cnf(u788,negated_conjecture,
~ product(e_3,e_1,e_1) ).
cnf(u859,negated_conjecture,
~ product(e_1,e_1,e_4) ).
cnf(u863,negated_conjecture,
~ product(e_1,e_1,e_3) ).
cnf(u867,negated_conjecture,
~ product(e_1,e_1,e_2) ).
cnf(u872,negated_conjecture,
product(e_1,e_1,e_1) ).
cnf(u1598,negated_conjecture,
~ product(e_5,e_1,e_5) ).
cnf(u4216,negated_conjecture,
~ product(e_5,e_3,e_5) ).
cnf(u4642,negated_conjecture,
~ product(e_5,e_4,e_5) ).
cnf(u5072,negated_conjecture,
~ product(e_5,e_2,e_5) ).
cnf(u9592,negated_conjecture,
( ~ product(e_3,X0,e_5)
| equalish(X0,e_2) ) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(u9710,axiom,
( ~ group_element(X1)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| product(e_4,X1,e_1)
| product(e_4,X1,e_2)
| product(e_4,X1,e_3)
| product(e_4,X1,e_4) ) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5) ).
cnf(u2959,negated_conjecture,
( ~ product(e_5,X0,e_5)
| equalish(X0,e_5) ) ).
cnf(u9610,negated_conjecture,
( ~ product(X0,e_4,e_5)
| equalish(X0,e_2) ) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2) ).
cnf(u9633,axiom,
( ~ product(e_4,X0,e_5)
| ~ group_element(X1)
| product(e_4,X1,e_1)
| product(e_4,X1,e_2)
| product(e_4,X1,e_3)
| product(e_4,X1,e_4)
| equalish(X0,X1) ) ).
cnf(u61,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1)
| 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(u9622,negated_conjecture,
( ~ product(e_4,X0,e_5)
| equalish(X0,e_1) ) ).
cnf(u9770,negated_conjecture,
~ greater(e_3,e_3) ).
cnf(u9437,negated_conjecture,
( ~ product(e_1,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u9393,negated_conjecture,
( ~ product(e_4,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u9624,negated_conjecture,
( ~ product(e_1,X0,e_4)
| product(e_5,e_1,X0) ) ).
cnf(u5830,negated_conjecture,
product(e_1,e_3,e_5) ).
cnf(u9305,negated_conjecture,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u9644,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product(e_5,X1,e_1)
| product(e_5,X1,e_2)
| product(e_5,X1,e_3)
| product(e_5,X1,e_4)
| ~ product(e_5,X1,X0) ) ).
cnf(u9463,negated_conjecture,
( ~ product(e_1,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u9433,negated_conjecture,
( ~ product(e_3,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u9765,axiom,
( ~ greater(X0,e_4)
| ~ product(e_3,e_1,X0) ) ).
cnf(u9320,negated_conjecture,
( ~ product(X0,e_3,e_5)
| equalish(X0,e_1) ) ).
cnf(u9705,negated_conjecture,
( ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| equalish(e_2,X0) ) ).
cnf(u8696,negated_conjecture,
( ~ product(e_3,X0,e_2)
| product(e_1,e_3,X0) ) ).
cnf(u9613,negated_conjecture,
( ~ product(e_4,X0,e_2)
| product(e_5,e_4,X0) ) ).
cnf(u9295,negated_conjecture,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(e_4_greater_e_1,axiom,
greater(e_4,e_1) ).
cnf(u9628,negated_conjecture,
( ~ 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)
| equalish(X0,e_4) ) ).
cnf(u9304,negated_conjecture,
( ~ product(X0,e_4,e_3)
| equalish(X0,e_5) ) ).
cnf(e_2_greater_e_1,axiom,
greater(e_2,e_1) ).
cnf(u9208,negated_conjecture,
( ~ product(e_5,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(u9738,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_2)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(u8852,negated_conjecture,
( ~ product(e_1,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(u9623,negated_conjecture,
( ~ product(e_4,e_1,X0)
| equalish(X0,e_5) ) ).
cnf(u9502,negated_conjecture,
( ~ product(X0,e_2,e_2)
| equalish(X0,e_2) ) ).
cnf(u8695,negated_conjecture,
( ~ product(e_2,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u9621,negated_conjecture,
( ~ product(X0,e_1,e_5)
| equalish(X0,e_4) ) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(qg3,negated_conjecture,
( ~ product(X2,X0,X3)
| ~ product(X0,X1,X2)
| product(X3,X0,X1) ) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(u9353,negated_conjecture,
( ~ group_element(X0)
| product(e_1,e_2,X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4) ) ).
cnf(u9735,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_4)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4) ) ).
cnf(u8850,negated_conjecture,
( ~ product(X0,e_4,e_2)
| equalish(X0,e_1) ) ).
cnf(u60,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1)
| 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(u9394,negated_conjecture,
( ~ product(e_4,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u9636,axiom,
( ~ group_element(X1)
| equalish(X0,e_2)
| product(e_2,X1,e_1)
| product(e_2,X1,e_2)
| product(e_2,X1,e_3)
| product(e_2,X1,e_4)
| ~ product(X0,X1,e_5) ) ).
cnf(u5816,negated_conjecture,
equalish(e_1,e_1) ).
cnf(u9306,negated_conjecture,
( ~ product(e_5,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u9561,negated_conjecture,
( ~ 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)
| equalish(X0,e_1) ) ).
cnf(u9434,negated_conjecture,
( ~ product(e_1,X0,e_3)
| product(e_4,e_1,X0) ) ).
cnf(u9708,negated_conjecture,
( ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4)
| equalish(e_1,X0) ) ).
cnf(u9443,negated_conjecture,
( ~ product(e_4,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u57,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| product(e_5,X0,e_2)
| product(e_5,X0,e_5)
| product(e_5,X0,e_1)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4) ) ).
cnf(e_3_greater_e_1,axiom,
greater(e_3,e_1) ).
cnf(u9594,negated_conjecture,
( ~ product(e_2,X0,e_3)
| product(e_5,e_2,X0) ) ).
cnf(u2958,negated_conjecture,
( ~ product(X0,e_5,e_5)
| equalish(X0,e_5) ) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(u9639,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product(e_5,X1,e_1)
| product(e_5,X1,e_2)
| product(e_5,X1,e_3)
| product(e_5,X1,e_4)
| ~ product(X0,X1,e_5) ) ).
cnf(u4099,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_5)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4) ) ).
cnf(u9659,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| equalish(e_5,X0) ) ).
cnf(u9772,axiom,
~ product(e_3,e_1,e_5) ).
cnf(u9526,negated_conjecture,
( ~ product(e_3,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(u46,negated_conjecture,
( ~ product(X0,X2,X1)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ group_element(X1)
| ~ group_element(X0)
| product(e_5,X0,X2) ) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(u9249,negated_conjecture,
( ~ product(e_2,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(product_left_cancellation,axiom,
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u9528,negated_conjecture,
( ~ product(e_3,X0,e_3)
| product(e_3,e_3,X0) ) ).
cnf(u9504,negated_conjecture,
( ~ product(e_2,e_2,X0)
| equalish(X0,e_2) ) ).
cnf(u59,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1)
| 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(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u9632,axiom,
( ~ product(e_3,X0,e_5)
| ~ group_element(X1)
| product(e_3,X1,e_1)
| product(e_3,X1,e_2)
| product(e_3,X1,e_3)
| product(e_3,X1,e_4)
| equalish(X0,X1) ) ).
cnf(u9207,negated_conjecture,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u9309,negated_conjecture,
( ~ product(X0,e_1,e_3)
| equalish(X0,e_2) ) ).
cnf(u9392,negated_conjecture,
( ~ product(X0,e_2,e_3)
| equalish(X0,e_4) ) ).
cnf(u3011,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| equalish(X0,e_5) ) ).
cnf(u9294,negated_conjecture,
( ~ product(X0,e_2,e_1)
| equalish(X0,e_5) ) ).
cnf(u9321,negated_conjecture,
( ~ product(e_1,X0,e_5)
| equalish(X0,e_3) ) ).
cnf(u9713,axiom,
( ~ group_element(X1)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| product(e_1,X1,e_1)
| product(e_1,X1,e_2)
| product(e_1,X1,e_3)
| product(e_1,X1,e_4) ) ).
cnf(u9577,negated_conjecture,
( ~ product(e_1,X0,e_1)
| product(e_1,e_1,X0) ) ).
cnf(e_5_greater_e_3,axiom,
greater(e_5,e_3) ).
cnf(u9611,negated_conjecture,
( ~ product(e_2,X0,e_5)
| equalish(X0,e_4) ) ).
cnf(u4877,negated_conjecture,
equalish(e_2,e_2) ).
cnf(u9351,negated_conjecture,
( ~ group_element(X0)
| product(e_3,e_4,X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ) ).
cnf(e_3_then_e_4,axiom,
next(e_3,e_4) ).
cnf(u5762,negated_conjecture,
equalish(e_3,e_3) ).
cnf(u8693,negated_conjecture,
( ~ product(X0,e_3,e_1)
| equalish(X0,e_2) ) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(e_1_then_e_2,axiom,
next(e_1,e_2) ).
cnf(u2961,negated_conjecture,
( ~ product(e_5,X0,e_5)
| product(e_5,e_5,X0) ) ).
cnf(u9638,axiom,
( ~ group_element(X1)
| equalish(X0,e_4)
| product(e_4,X1,e_1)
| product(e_4,X1,e_2)
| product(e_4,X1,e_3)
| product(e_4,X1,e_4)
| ~ product(X0,X1,e_5) ) ).
cnf(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5) ).
cnf(u9593,negated_conjecture,
( ~ product(e_3,e_2,X0)
| equalish(X0,e_5) ) ).
cnf(u9704,axiom,
( ~ group_element(X1)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| product(e_2,X1,e_1)
| product(e_2,X1,e_2)
| product(e_2,X1,e_3)
| product(e_2,X1,e_4) ) ).
cnf(product_right_cancellation,axiom,
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u9612,negated_conjecture,
( ~ product(e_2,e_4,X0)
| equalish(X0,e_5) ) ).
cnf(element_3,axiom,
group_element(e_3) ).
cnf(u9525,negated_conjecture,
( ~ product(X0,e_3,e_3)
| equalish(X0,e_3) ) ).
cnf(u9347,negated_conjecture,
( ~ group_element(X0)
| product(e_2,e_1,X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(u2960,negated_conjecture,
( ~ product(e_5,e_5,X0)
| equalish(X0,e_5) ) ).
cnf(u9250,negated_conjecture,
( ~ product(e_5,X0,e_2)
| product(e_4,e_5,X0) ) ).
cnf(product_total_function1,axiom,
( product(X0,X1,e_5)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ group_element(X0) ) ).
cnf(u9505,negated_conjecture,
( ~ product(e_2,X0,e_2)
| product(e_2,e_2,X0) ) ).
cnf(u9248,negated_conjecture,
( ~ product(e_2,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u47,axiom,
( ~ group_element(X0)
| equalish(X2,e_5)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u58,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1)
| 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(u9741,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_1)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ) ).
cnf(u9431,negated_conjecture,
( ~ product(X0,e_1,e_4)
| equalish(X0,e_3) ) ).
cnf(u9436,negated_conjecture,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_1) ) ).
cnf(u9575,negated_conjecture,
( ~ product(e_1,X0,e_1)
| equalish(X0,e_1) ) ).
cnf(u8694,negated_conjecture,
( ~ product(e_2,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u9307,negated_conjecture,
( ~ product(e_4,X0,e_5)
| product(e_3,e_4,X0) ) ).
cnf(u9301,negated_conjecture,
( ~ product(e_5,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u9310,negated_conjecture,
( ~ product(e_2,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u9429,negated_conjecture,
( ~ product(e_5,X0,e_4)
| product(e_1,e_5,X0) ) ).
cnf(u9598,negated_conjecture,
( ~ 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)
| equalish(X0,e_3) ) ).
cnf(e_5_greater_e_4,axiom,
greater(e_5,e_4) ).
cnf(e_4_greater_e_3,axiom,
greater(e_4,e_3) ).
cnf(u9439,negated_conjecture,
( ~ product(e_5,X0,e_1)
| product(e_3,e_5,X0) ) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(e_2_then_e_3,axiom,
next(e_2,e_3) ).
cnf(u9588,negated_conjecture,
product(e_3,e_2,e_5) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(u52,negated_conjecture,
( ~ group_element(X1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| ~ group_element(X0)
| product(e_5,X0,X1)
| product(e_5,X0,e_1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4) ) ).
cnf(u9243,negated_conjecture,
( ~ product(e_3,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(u9711,negated_conjecture,
( ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4)
| equalish(e_3,X0) ) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(product_total_function2,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u9641,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product(e_2,X1,e_1)
| product(e_2,X1,e_2)
| product(e_2,X1,e_3)
| product(e_2,X1,e_4)
| ~ product(e_2,X1,X0) ) ).
cnf(u9395,negated_conjecture,
( ~ product(e_2,X0,e_4)
| product(e_3,e_2,X0) ) ).
cnf(u9617,negated_conjecture,
( ~ 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)
| equalish(X0,e_2) ) ).
cnf(u9428,negated_conjecture,
( ~ product(e_4,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4) ).
cnf(u9707,axiom,
( ~ group_element(X1)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| product(e_3,X1,e_1)
| product(e_3,X1,e_2)
| product(e_3,X1,e_3)
| product(e_3,X1,e_4) ) ).
cnf(u9549,negated_conjecture,
( ~ product(e_4,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u9296,negated_conjecture,
( ~ product(e_5,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u5818,negated_conjecture,
equalish(e_4,e_4) ).
cnf(u9634,axiom,
( ~ product(e_5,X0,e_5)
| ~ group_element(X1)
| product(e_5,X1,e_1)
| product(e_5,X1,e_2)
| product(e_5,X1,e_3)
| product(e_5,X1,e_4)
| equalish(X0,X1) ) ).
cnf(u9424,negated_conjecture,
( ~ product(e_4,X0,e_3)
| product(e_1,e_4,X0) ) ).
cnf(u9465,negated_conjecture,
( ~ product(e_2,X0,e_1)
| product(e_4,e_2,X0) ) ).
cnf(u9442,negated_conjecture,
( ~ product(e_4,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u9527,negated_conjecture,
( ~ product(e_3,e_3,X0)
| equalish(X0,e_3) ) ).
cnf(u9302,negated_conjecture,
( ~ product(e_1,X0,e_5)
| product(e_2,e_1,X0) ) ).
cnf(u9744,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_3)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(no_redundancy,axiom,
( ~ next(X0,X2)
| ~ product(X0,e_1,X1)
| ~ greater(X1,X2) ) ).
cnf(u9423,negated_conjecture,
( ~ product(e_3,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u9349,negated_conjecture,
( ~ group_element(X0)
| product(e_4,e_3,X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(e_5_greater_e_2,axiom,
greater(e_5,e_2) ).
cnf(e_3_greater_e_2,axiom,
greater(e_3,e_2) ).
cnf(u9242,negated_conjecture,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_3) ) ).
cnf(u9432,negated_conjecture,
( ~ product(e_3,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u9630,axiom,
( ~ product(e_1,X0,e_5)
| ~ group_element(X1)
| product(e_1,X1,e_1)
| product(e_1,X1,e_2)
| product(e_1,X1,e_3)
| product(e_1,X1,e_4)
| equalish(X0,X1) ) ).
cnf(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5) ).
cnf(u9209,negated_conjecture,
( ~ product(e_3,X0,e_5)
| product(e_4,e_3,X0) ) ).
cnf(u9311,negated_conjecture,
( ~ product(e_2,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u9247,negated_conjecture,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_2) ) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(u49,axiom,
( ~ group_element(X2)
| equalish(X0,X2)
| ~ group_element(X1)
| product(X2,X1,e_1)
| product(X2,X1,e_2)
| product(X2,X1,e_3)
| product(X2,X1,e_4)
| ~ product(X0,X1,e_5) ) ).
cnf(u9763,axiom,
( ~ product(e_1,e_1,X0)
| ~ greater(X0,e_2) ) ).
cnf(u8853,negated_conjecture,
( ~ product(e_4,X0,e_1)
| product(e_2,e_4,X0) ) ).
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5) ).
cnf(u9607,negated_conjecture,
product(e_2,e_4,e_5) ).
cnf(u8851,negated_conjecture,
( ~ product(e_1,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u9637,axiom,
( ~ group_element(X1)
| equalish(X0,e_3)
| product(e_3,X1,e_1)
| product(e_3,X1,e_2)
| product(e_3,X1,e_3)
| product(e_3,X1,e_4)
| ~ product(X0,X1,e_5) ) ).
cnf(u9764,axiom,
( ~ product(e_2,e_1,X0)
| ~ greater(X0,e_3) ) ).
cnf(u9766,axiom,
( ~ greater(X0,e_5)
| ~ product(e_4,e_1,X0) ) ).
cnf(u9618,negated_conjecture,
product(e_4,e_1,e_5) ).
cnf(u8279,negated_conjecture,
( ~ group_element(X0)
| product(e_5,e_5,X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4) ) ).
cnf(u9551,negated_conjecture,
( ~ product(e_4,X0,e_4)
| product(e_4,e_4,X0) ) ).
cnf(u9550,negated_conjecture,
( ~ product(e_4,e_4,X0)
| equalish(X0,e_4) ) ).
cnf(u9421,negated_conjecture,
( ~ product(X0,e_4,e_1)
| equalish(X0,e_3) ) ).
cnf(u9426,negated_conjecture,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_4) ) ).
cnf(u9438,negated_conjecture,
( ~ product(e_1,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(u9299,negated_conjecture,
( ~ product(X0,e_1,e_2)
| equalish(X0,e_5) ) ).
cnf(u9441,negated_conjecture,
( ~ product(X0,e_3,e_2)
| equalish(X0,e_4) ) ).
cnf(u9245,negated_conjecture,
( ~ product(e_5,X0,e_3)
| product(e_2,e_5,X0) ) ).
cnf(u9206,negated_conjecture,
( ~ product(X0,e_3,e_4)
| equalish(X0,e_5) ) ).
cnf(u9427,negated_conjecture,
( ~ product(e_4,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(element_5,axiom,
group_element(e_5) ).
cnf(u690,negated_conjecture,
equalish(e_5,e_5) ).
cnf(e_4_greater_e_2,axiom,
greater(e_4,e_2) ).
cnf(u9591,negated_conjecture,
( ~ product(X0,e_2,e_5)
| equalish(X0,e_3) ) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(e_5_greater_e_1,axiom,
greater(e_5,e_1) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3) ).
cnf(u9503,negated_conjecture,
( ~ product(e_2,X0,e_2)
| equalish(X0,e_2) ) ).
cnf(u9635,axiom,
( ~ group_element(X1)
| equalish(X0,e_1)
| product(e_1,X1,e_1)
| product(e_1,X1,e_2)
| product(e_1,X1,e_3)
| product(e_1,X1,e_4)
| ~ product(X0,X1,e_5) ) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1) ).
cnf(u48,axiom,
( ~ group_element(X0)
| equalish(X1,X2)
| ~ group_element(X2)
| product(X0,X2,e_1)
| product(X0,X2,e_2)
| product(X0,X2,e_3)
| product(X0,X2,e_4)
| ~ product(X0,X1,e_5) ) ).
cnf(u9631,axiom,
( ~ product(e_2,X0,e_5)
| ~ group_element(X1)
| product(e_2,X1,e_1)
| product(e_2,X1,e_2)
| product(e_2,X1,e_3)
| product(e_2,X1,e_4)
| equalish(X0,X1) ) ).
cnf(u9643,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product(e_4,X1,e_1)
| product(e_4,X1,e_2)
| product(e_4,X1,e_3)
| product(e_4,X1,e_4)
| ~ product(e_4,X1,X0) ) ).
cnf(u9642,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product(e_3,X1,e_1)
| product(e_3,X1,e_2)
| product(e_3,X1,e_3)
| product(e_3,X1,e_4)
| ~ product(e_3,X1,X0) ) ).
cnf(u9767,negated_conjecture,
~ greater(e_1,e_2) ).
cnf(u9574,negated_conjecture,
( ~ product(X0,e_1,e_1)
| equalish(X0,e_1) ) ).
cnf(u9702,negated_conjecture,
( ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4)
| equalish(e_4,X0) ) ).
cnf(u9548,negated_conjecture,
( ~ product(X0,e_4,e_4)
| equalish(X0,e_4) ) ).
cnf(u9422,negated_conjecture,
( ~ product(e_3,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u9297,negated_conjecture,
( ~ product(e_2,X0,e_5)
| product(e_1,e_2,X0) ) ).
cnf(u9576,negated_conjecture,
( ~ product(e_1,e_1,X0)
| equalish(X0,e_1) ) ).
cnf(u9462,negated_conjecture,
( ~ product(X0,e_2,e_4)
| equalish(X0,e_1) ) ).
cnf(e_4_then_e_5,axiom,
next(e_4,e_5) ).
cnf(u9323,negated_conjecture,
( ~ product(e_3,X0,e_1)
| product(e_5,e_3,X0) ) ).
cnf(u9300,negated_conjecture,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u9312,negated_conjecture,
( ~ product(e_1,X0,e_2)
| product(e_3,e_1,X0) ) ).
cnf(u9464,negated_conjecture,
( ~ product(e_1,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u9244,negated_conjecture,
( ~ product(e_3,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(u9322,negated_conjecture,
( ~ product(e_1,e_3,X0)
| equalish(X0,e_5) ) ).
cnf(u9444,negated_conjecture,
( ~ product(e_3,X0,e_4)
| product(e_2,e_3,X0) ) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(u9640,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product(e_1,X1,e_1)
| product(e_1,X1,e_2)
| product(e_1,X1,e_3)
| product(e_1,X1,e_4)
| ~ product(e_1,X1,X0) ) ).
cnf(u9661,axiom,
( ~ group_element(X1)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| product(e_5,X1,e_1)
| product(e_5,X1,e_2)
| product(e_5,X1,e_3)
| product(e_5,X1,e_4) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP135-2.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 09:34:42 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.12/1.88 % (2573623)Input is clausal, will run a generic CNF schedule.
% 6.12/1.88 % (2573633)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=973231654:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.12/1.88 % (2573628)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=3350307140:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.12/1.88 % (2573634)dis-21_1_sil=8000:lcm=predicate:random_seed=1414016505: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.12/1.88 % (2573630)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3288252090:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.12/1.88 % (2573629)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1463857534:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.12/1.88 % (2573631)lrs+10_1_sil=8000:sp=occurrence:random_seed=1320095601:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.12/1.88 % (2573632)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1502129700:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.12/1.88 % (2573633)Instruction limit reached!
% 6.12/1.88 % (2573633)------------------------------
% 6.12/1.88 % (2573633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.12/1.88 % (2573633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.88 % (2573633)CaDiCaL version: 2.1.3
% 6.12/1.88 % (2573633)Termination reason: Instruction limit
% 6.12/1.88 % (2573633)Termination phase: Saturation
% 6.12/1.88 % (2573633)Time elapsed: 0.060 s
% 6.12/1.88 % (2573633)Peak memory usage: 89 MB
% 6.12/1.88 % (2573633)Instructions burned: 184 (million)
% 6.12/1.88 % (2573631)Instruction limit reached!
% 6.12/1.88 % (2573631)------------------------------
% 6.12/1.88 % (2573631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.12/1.88 % (2573631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.88 % (2573631)CaDiCaL version: 2.1.3
% 6.12/1.88 % (2573631)Termination reason: Instruction limit
% 6.12/1.88 % (2573631)Termination phase: Saturation
% 6.12/1.88 % (2573631)Time elapsed: 0.058 s
% 6.12/1.88 % (2573631)Peak memory usage: 88 MB
% 6.12/1.88 % (2573631)Instructions burned: 107 (million)
% 6.12/1.88 % (2573632)Instruction limit reached!
% 6.12/1.88 % (2573632)------------------------------
% 6.12/1.88 % (2573632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.12/1.88 % (2573632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.88 % (2573632)CaDiCaL version: 2.1.3
% 6.12/1.88 % (2573632)Termination reason: Instruction limit
% 6.12/1.88 % (2573632)Termination phase: Saturation
% 6.12/1.88 % (2573632)Time elapsed: 0.061 s
% 6.12/1.88 % (2573632)Peak memory usage: 88 MB
% 6.12/1.88 % (2573632)Instructions burned: 114 (million)
% 6.12/1.88 % (2573634)Instruction limit reached!
% 6.12/1.88 % (2573634)------------------------------
% 6.12/1.88 % (2573634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.12/1.88 % (2573634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.88 % (2573634)CaDiCaL version: 2.1.3
% 6.12/1.88 % (2573634)Termination reason: Instruction limit
% 6.12/1.88 % (2573634)Termination phase: Saturation
% 6.12/1.88 % (2573634)Time elapsed: 0.077 s
% 6.12/1.88 % (2573634)Peak memory usage: 88 MB
% 6.12/1.88 % (2573634)Instructions burned: 118 (million)
% 6.12/1.88 % (2573642)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=373228375:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.12/1.88 % (2573642)Instruction limit reached!
% 6.12/1.88 % (2573642)------------------------------
% 6.12/1.88 % (2573642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.12/1.88 % (2573642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.12/1.88 % (2573642)CaDiCaL version: 2.1.3
% 6.12/1.88 % (2573642)Termination reason: Instruction limit
% 6.12/1.88 % (2573642)Termination phase: Saturation
% 6.12/1.88 % (2573642)Time elapsed: 0.045 s
% 6.12/1.88 % (2573642)Peak memory usage: 89 MB
% 6.12/1.88 % (2573642)Instructions burned: 147 (million)
% 6.12/1.88 % (2573644)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=728058279:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 12.23/2.77 % (2573643)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3389248183: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)
% 12.23/2.77 % (2573643)Refutation not found, incomplete strategy
% 12.23/2.77 % (2573643)------------------------------
% 12.23/2.77 % (2573643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.77 % (2573643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/2.77 % (2573643)CaDiCaL version: 2.1.3
% 12.23/2.77 % (2573643)Termination reason: Refutation not found, incomplete strategy
% 12.23/2.77 % (2573643)Time elapsed: 0.002 s
% 12.23/2.77 % (2573643)Peak memory usage: 87 MB
% 12.23/2.77 % (2573643)Instructions burned: 1 (million)
% 12.23/2.77 % (2573645)lrs+10_64_to=lpo:sil=8000:random_seed=1344721228:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 12.23/2.77 % (2573647)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2904894147:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 12.23/2.77 % (2573647)Instruction limit reached!
% 12.23/2.77 % (2573647)------------------------------
% 12.23/2.77 % (2573647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.77 % (2573647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/2.77 % (2573647)CaDiCaL version: 2.1.3
% 12.23/2.77 % (2573647)Termination reason: Instruction limit
% 12.23/2.77 % (2573647)Termination phase: Saturation
% 12.23/2.77 % (2573647)Time elapsed: 0.038 s
% 12.23/2.77 % (2573647)Peak memory usage: 87 MB
% 12.23/2.77 % (2573647)Instructions burned: 200 (million)
% 12.23/2.77 % (2573645)Instruction limit reached!
% 12.23/2.77 % (2573645)------------------------------
% 12.23/2.77 % (2573645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.77 % (2573645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/2.77 % (2573645)CaDiCaL version: 2.1.3
% 12.23/2.77 % (2573645)Termination reason: Instruction limit
% 12.23/2.77 % (2573645)Termination phase: Saturation
% 12.23/2.77 % (2573645)Time elapsed: 0.077 s
% 12.23/2.77 % (2573645)Peak memory usage: 88 MB
% 12.23/2.77 % (2573645)Instructions burned: 126 (million)
% 12.23/2.77 % (2573644)Instruction limit reached!
% 12.23/2.77 % (2573644)------------------------------
% 12.23/2.77 % (2573644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.77 % (2573644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/2.77 % (2573644)CaDiCaL version: 2.1.3
% 12.23/2.77 % (2573644)Termination reason: Instruction limit
% 12.23/2.77 % (2573644)Termination phase: Saturation
% 12.23/2.77 % (2573644)Time elapsed: 0.124 s
% 12.23/2.77 % (2573644)Peak memory usage: 88 MB
% 12.23/2.77 % (2573644)Instructions burned: 220 (million)
% 12.23/2.77 % (2573652)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3895564158:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 12.23/2.77 % (2573652)Instruction limit reached!
% 12.23/2.77 % (2573652)------------------------------
% 12.23/2.77 % (2573652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.77 % (2573652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/2.77 % (2573652)CaDiCaL version: 2.1.3
% 12.23/2.77 % (2573652)Termination reason: Instruction limit
% 12.23/2.77 % (2573652)Termination phase: Saturation
% 12.23/2.77 % (2573652)Time elapsed: 0.045 s
% 12.23/2.77 % (2573652)Peak memory usage: 89 MB
% 12.23/2.77 % (2573652)Instructions burned: 161 (million)
% 12.23/2.77 % (2573653)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3723361326:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 12.23/2.77 % (2573643)------------------------------
% 12.23/2.77 % (2573643)------------------------------
% 12.23/2.77 % (2573654)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=2569106341:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 12.23/2.77 % (2573654)Refutation not found, incomplete strategy
% 12.23/2.77 % (2573654)------------------------------
% 12.23/2.77 % (2573654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.77 % (2573654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.10/3.88 % (2573654)CaDiCaL version: 2.1.3
% 21.10/3.88 % (2573654)Termination reason: Refutation not found, incomplete strategy
% 21.10/3.88 % (2573654)Time elapsed: 0.002 s
% 21.10/3.88 % (2573654)Peak memory usage: 87 MB
% 21.10/3.88 % (2573654)Instructions burned: 2 (million)
% 21.10/3.88 % (2573656)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=690422790:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 21.10/3.88 % (2573656)Instruction limit reached!
% 21.10/3.88 % (2573656)------------------------------
% 21.10/3.88 % (2573656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.10/3.88 % (2573656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.10/3.88 % (2573656)CaDiCaL version: 2.1.3
% 21.10/3.88 % (2573656)Termination reason: Instruction limit
% 21.10/3.88 % (2573656)Termination phase: Saturation
% 21.10/3.88 % (2573656)Time elapsed: 0.037 s
% 21.10/3.88 % (2573656)Peak memory usage: 88 MB
% 21.10/3.88 % (2573656)Instructions burned: 109 (million)
% 21.10/3.88 % (2573658)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1184273068:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2994 on theBenchmark for (2994ds/242Mi)
% 21.10/3.88 % (2573629)Refutation not found, incomplete strategy
% 21.10/3.88 % (2573629)------------------------------
% 21.10/3.88 % (2573629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.10/3.88 % (2573629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.10/3.88 % (2573629)CaDiCaL version: 2.1.3
% 21.10/3.88 % (2573629)Termination reason: Refutation not found, incomplete strategy
% 21.10/3.88 % (2573629)Time elapsed: 0.579 s
% 21.10/3.88 % (2573629)Peak memory usage: 127 MB
% 21.10/3.88 % (2573629)Instructions burned: 907 (million)
% 21.10/3.88 % (2573661)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1820912385:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 21.10/3.88 % (2573658)Instruction limit reached!
% 21.10/3.88 % (2573658)------------------------------
% 21.10/3.88 % (2573658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.10/3.88 % (2573658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.10/3.88 % (2573658)CaDiCaL version: 2.1.3
% 21.10/3.88 % (2573658)Termination reason: Instruction limit
% 21.10/3.88 % (2573658)Termination phase: Saturation
% 21.10/3.88 % (2573658)Time elapsed: 0.130 s
% 21.10/3.88 % (2573658)Peak memory usage: 89 MB
% 21.10/3.88 % (2573658)Instructions burned: 244 (million)
% 21.10/3.88 % (2573654)------------------------------
% 21.10/3.88 % (2573654)------------------------------
% 21.10/3.88 % (2573629)------------------------------
% 21.10/3.88 % (2573629)------------------------------
% 21.10/3.88 % (2573666)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3892100466:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi)
% 21.10/3.88 % (2573664)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1628987047:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 21.10/3.88 % (2573665)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2278700890:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 21.10/3.88 % (2573664)Instruction limit reached!
% 21.10/3.88 % (2573664)------------------------------
% 21.10/3.88 % (2573664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.10/3.88 % (2573664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.10/3.88 % (2573664)CaDiCaL version: 2.1.3
% 21.10/3.88 % (2573664)Termination reason: Instruction limit
% 21.10/3.88 % (2573664)Termination phase: Saturation
% 21.10/3.88 % (2573664)Time elapsed: 0.050 s
% 21.10/3.88 % (2573664)Peak memory usage: 88 MB
% 21.10/3.88 % (2573664)Instructions burned: 134 (million)
% 21.10/3.88 % (2573666)Instruction limit reached!
% 21.10/3.88 % (2573666)------------------------------
% 21.10/3.88 % (2573666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.10/3.88 % (2573666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.10/3.88 % (2573666)CaDiCaL version: 2.1.3
% 21.10/3.88 % (2573666)Termination reason: Instruction limit
% 21.10/3.88 % (2573666)Termination phase: Saturation
% 21.10/3.88 % (2573666)Time elapsed: 0.063 s
% 21.10/3.88 % (2573666)Peak memory usage: 88 MB
% 21.10/3.88 % (2573666)Instructions burned: 192 (million)
% 31.62/5.38 % (2573671)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2550507095:cond=on:i=156:bs=on:gtg=exists_all:er=known_2989 on theBenchmark for (2989ds/156Mi)
% 31.62/5.38 % (2573670)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2181057729:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 31.62/5.38 % (2573671)Instruction limit reached!
% 31.62/5.38 % (2573671)------------------------------
% 31.62/5.38 % (2573671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.62/5.38 % (2573671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.62/5.38 % (2573671)CaDiCaL version: 2.1.3
% 31.62/5.38 % (2573671)Termination reason: Instruction limit
% 31.62/5.38 % (2573671)Termination phase: Saturation
% 31.62/5.38 % (2573671)Time elapsed: 0.047 s
% 31.62/5.38 % (2573671)Peak memory usage: 88 MB
% 31.62/5.38 % (2573671)Instructions burned: 157 (million)
% 31.62/5.38 % (2573674)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2284531242:i=3256:kws=precedence:bd=preordered:av=off_2988 on theBenchmark for (2988ds/3256Mi)
% 31.62/5.38 % (2573665)Instruction limit reached!
% 31.62/5.38 % (2573665)------------------------------
% 31.62/5.38 % (2573665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.62/5.38 % (2573665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.62/5.38 % (2573665)CaDiCaL version: 2.1.3
% 31.62/5.38 % (2573665)Termination reason: Instruction limit
% 31.62/5.38 % (2573665)Termination phase: Saturation
% 31.62/5.38 % (2573665)Time elapsed: 0.273 s
% 31.62/5.38 % (2573665)Peak memory usage: 90 MB
% 31.62/5.38 % (2573665)Instructions burned: 499 (million)
% 31.62/5.38 % (2573670)Instruction limit reached!
% 31.62/5.38 % (2573670)------------------------------
% 31.62/5.38 % (2573670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.62/5.38 % (2573670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.62/5.38 % (2573670)CaDiCaL version: 2.1.3
% 31.62/5.38 % (2573670)Termination reason: Instruction limit
% 31.62/5.38 % (2573670)Termination phase: Saturation
% 31.62/5.38 % (2573670)Time elapsed: 0.167 s
% 31.62/5.38 % (2573670)Peak memory usage: 90 MB
% 31.62/5.38 % (2573670)Instructions burned: 264 (million)
% 31.62/5.38 % (2573676)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2406124698:i=537:av=off:ss=included_2987 on theBenchmark for (2987ds/537Mi)
% 31.62/5.38 % (2573677)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=42743748:i=180:bd=preordered:av=off_2986 on theBenchmark for (2986ds/180Mi)
% 31.62/5.38 % (2573677)Instruction limit reached!
% 31.62/5.38 % (2573677)------------------------------
% 31.62/5.38 % (2573677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.62/5.38 % (2573677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.62/5.38 % (2573677)CaDiCaL version: 2.1.3
% 31.62/5.38 % (2573677)Termination reason: Instruction limit
% 31.62/5.38 % (2573677)Termination phase: Saturation
% 31.62/5.38 % (2573677)Time elapsed: 0.096 s
% 31.62/5.38 % (2573677)Peak memory usage: 87 MB
% 31.62/5.38 % (2573677)Instructions burned: 181 (million)
% 31.62/5.38 % (2573676)Instruction limit reached!
% 31.62/5.38 % (2573676)------------------------------
% 31.62/5.38 % (2573676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.62/5.38 % (2573676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.62/5.38 % (2573676)CaDiCaL version: 2.1.3
% 31.62/5.38 % (2573676)Termination reason: Instruction limit
% 31.62/5.38 % (2573676)Termination phase: Saturation
% 31.62/5.38 % (2573676)Time elapsed: 0.198 s
% 31.62/5.38 % (2573676)Peak memory usage: 88 MB
% 31.62/5.38 % (2573676)Instructions burned: 539 (million)
% 31.62/5.38 % (2573680)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2487096827:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2984 on theBenchmark for (2984ds/10307Mi)
% 31.62/5.38 % (2573681)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3139913342:i=412:gtgl=4:gtg=exists_all_2984 on theBenchmark for (2984ds/412Mi)
% 31.62/5.38 % (2573681)Instruction limit reached!
% 31.62/5.38 % (2573681)------------------------------
% 31.62/5.38 % (2573681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.41/6.97 % (2573681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.41/6.97 % (2573681)CaDiCaL version: 2.1.3
% 42.41/6.97 % (2573681)Termination reason: Instruction limit
% 42.41/6.97 % (2573681)Termination phase: Saturation
% 42.41/6.97 % (2573681)Time elapsed: 0.203 s
% 42.41/6.97 % (2573681)Peak memory usage: 91 MB
% 42.41/6.97 % (2573681)Instructions burned: 413 (million)
% 42.41/6.97 % (2573684)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3647592785:s2pl=no:i=8478:s2at=4:nm=6_2980 on theBenchmark for (2980ds/8478Mi)
% 42.41/6.97 % (2573674)Instruction limit reached!
% 42.41/6.97 % (2573674)------------------------------
% 42.41/6.97 % (2573674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.41/6.97 % (2573674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.41/6.97 % (2573674)CaDiCaL version: 2.1.3
% 42.41/6.97 % (2573674)Termination reason: Instruction limit
% 42.41/6.97 % (2573674)Termination phase: Saturation
% 42.41/6.97 % (2573674)Time elapsed: 1.165 s
% 42.41/6.97 % (2573674)Peak memory usage: 135 MB
% 42.41/6.97 % (2573674)Instructions burned: 3260 (million)
% 42.41/6.97 % (2573686)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=549685115:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2975 on theBenchmark for (2975ds/303Mi)
% 42.41/6.97 % (2573686)Instruction limit reached!
% 42.41/6.97 % (2573686)------------------------------
% 42.41/6.97 % (2573686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.41/6.97 % (2573686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.41/6.97 % (2573686)CaDiCaL version: 2.1.3
% 42.41/6.97 % (2573686)Termination reason: Instruction limit
% 42.41/6.97 % (2573686)Termination phase: Saturation
% 42.41/6.97 % (2573686)Time elapsed: 0.100 s
% 42.41/6.97 % (2573686)Peak memory usage: 90 MB
% 42.41/6.97 % (2573686)Instructions burned: 305 (million)
% 42.41/6.97 % (2573684)Refutation not found, incomplete strategy
% 42.41/6.97 % (2573684)------------------------------
% 42.41/6.97 % (2573684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.41/6.97 % (2573684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.41/6.97 % (2573684)CaDiCaL version: 2.1.3
% 42.41/6.97 % (2573684)Termination reason: Refutation not found, incomplete strategy
% 42.41/6.97 % (2573684)Time elapsed: 0.593 s
% 42.41/6.97 % (2573684)Peak memory usage: 128 MB
% 42.41/6.97 % (2573684)Instructions burned: 906 (million)
% 42.41/6.97 % (2573688)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3240289972:st=4:i=720:sd=3:fsr=off:ss=axioms_2973 on theBenchmark for (2973ds/720Mi)
% 42.41/6.97 % (2573688)Refutation not found, incomplete strategy
% 42.41/6.97 % (2573688)------------------------------
% 42.41/6.97 % (2573688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.41/6.97 % (2573688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.41/6.97 % (2573688)CaDiCaL version: 2.1.3
% 42.41/6.97 % (2573688)Termination reason: Refutation not found, incomplete strategy
% 42.41/6.97 % (2573688)Time elapsed: 0.001 s
% 42.41/6.97 % (2573688)Peak memory usage: 87 MB
% 42.41/6.97 % (2573688)Instructions burned: 1 (million)
% 42.41/6.97 % (2573688)------------------------------
% 42.41/6.97 % (2573688)------------------------------
% 42.41/6.97 % (2573684)------------------------------
% 42.41/6.97 % (2573684)------------------------------
% 42.41/6.97 % (2573690)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=375964198:i=598:bs=on:bd=preordered:av=off:ss=axioms_2971 on theBenchmark for (2971ds/598Mi)
% 42.41/6.97 % (2573653)Instruction limit reached!
% 42.41/6.97 % (2573653)------------------------------
% 42.41/6.97 % (2573653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.41/6.97 % (2573653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.41/6.97 % (2573653)CaDiCaL version: 2.1.3
% 42.41/6.97 % (2573653)Termination reason: Instruction limit
% 42.41/6.97 % (2573653)Termination phase: Saturation
% 42.41/6.97 % (2573653)Time elapsed: 2.447 s
% 42.41/6.97 % (2573653)Peak memory usage: 142 MB
% 42.41/6.97 % (2573653)Instructions burned: 3394 (million)
% 42.41/6.97 % (2573691)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=256388298:i=2989:sd=3:ss=axioms:sgt=60_2971 on theBenchmark for (2971ds/2989Mi)
% 47.89/7.69 % (2573690)Instruction limit reached!
% 47.89/7.69 % (2573690)------------------------------
% 47.89/7.69 % (2573690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.89/7.69 % (2573690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.89/7.69 % (2573690)CaDiCaL version: 2.1.3
% 47.89/7.69 % (2573690)Termination reason: Instruction limit
% 47.89/7.69 % (2573690)Termination phase: Saturation
% 47.89/7.69 % (2573690)Time elapsed: 0.151 s
% 47.89/7.69 % (2573690)Peak memory usage: 88 MB
% 47.89/7.69 % (2573690)Instructions burned: 600 (million)
% 47.89/7.69 % (2573693)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3236141872:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2969 on theBenchmark for (2969ds/1997Mi)
% 47.89/7.69 % (2573695)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2034585460:i=2088:bd=preordered:av=off_2969 on theBenchmark for (2969ds/2088Mi)
% 47.89/7.69 % (2573661)Instruction limit reached!
% 47.89/7.69 % (2573661)------------------------------
% 47.89/7.69 % (2573661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.89/7.69 % (2573661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.89/7.69 % (2573661)CaDiCaL version: 2.1.3
% 47.89/7.69 % (2573661)Termination reason: Instruction limit
% 47.89/7.69 % (2573661)Termination phase: Saturation
% 47.89/7.69 % (2573661)Time elapsed: 2.465 s
% 47.89/7.69 % (2573661)Peak memory usage: 131 MB
% 47.89/7.69 % (2573661)Instructions burned: 5210 (million)
% 47.89/7.69 % (2573698)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1092522877:i=1098:nicw=on_2967 on theBenchmark for (2967ds/1098Mi)
% 47.89/7.69 % (2573695)Instruction limit reached!
% 47.89/7.69 % (2573695)------------------------------
% 47.89/7.69 % (2573695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.89/7.69 % (2573695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.89/7.69 % (2573695)CaDiCaL version: 2.1.3
% 47.89/7.69 % (2573695)Termination reason: Instruction limit
% 47.89/7.69 % (2573695)Termination phase: Saturation
% 47.89/7.69 % (2573695)Time elapsed: 0.663 s
% 47.89/7.69 % (2573695)Peak memory usage: 131 MB
% 47.89/7.69 % (2573695)Instructions burned: 2090 (million)
% 47.89/7.69 % (2573700)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2482874135:i=433:bd=preordered_2961 on theBenchmark for (2961ds/433Mi)
% 47.89/7.69 % (2573698)Instruction limit reached!
% 47.89/7.69 % (2573698)------------------------------
% 47.89/7.69 % (2573698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.89/7.69 % (2573698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.89/7.69 % (2573698)CaDiCaL version: 2.1.3
% 47.89/7.69 % (2573698)Termination reason: Instruction limit
% 47.89/7.69 % (2573698)Termination phase: Saturation
% 47.89/7.69 % (2573698)Time elapsed: 0.576 s
% 47.89/7.69 % (2573698)Peak memory usage: 90 MB
% 47.89/7.69 % (2573698)Instructions burned: 1099 (million)
% 47.89/7.69 % (2573700)Refutation not found, incomplete strategy
% 47.89/7.69 % (2573700)------------------------------
% 47.89/7.69 % (2573700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.89/7.69 % (2573700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.89/7.69 % (2573700)CaDiCaL version: 2.1.3
% 47.89/7.69 % (2573700)Termination reason: Refutation not found, incomplete strategy
% 47.89/7.69 % (2573700)Time elapsed: 0.101 s
% 47.89/7.69 % (2573700)Peak memory usage: 89 MB
% 47.89/7.69 % (2573700)Instructions burned: 318 (million)
% 47.89/7.69 % (2573702)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1174652383:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2959 on theBenchmark for (2959ds/2942Mi)
% 47.89/7.69 % (2573700)------------------------------
% 47.89/7.69 % (2573700)------------------------------
% 47.89/7.69 % (2573704)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=91539702:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2958 on theBenchmark for (2958ds/6922Mi)
% 47.89/7.69 % (2573693)Instruction limit reached!
% 47.89/7.69 % (2573693)------------------------------
% 47.89/7.69 % (2573693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.89/7.69 % (2573693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.89/7.69 % (2573693)CaDiCaL version: 2.1.3
% 47.89/7.69 % (2573693)Termination reason: Instruction limit
% 47.89/7.69 % (2573693)Termination phase: Saturation
% 47.89/7.69 % (2573693)Time elapsed: 1.375 s
% 47.89/7.69 % (2573693)Peak memory usage: 133 MB
% 47.89/7.69 % (2573693)Instructions burned: 1998 (million)
% 47.89/7.69 % (2573704)Refutation not found, incomplete strategy
% 47.89/7.69 % (2573704)------------------------------
% 47.89/7.69 % (2573704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.89/7.69 % (2573704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.89/7.69 % (2573704)CaDiCaL version: 2.1.3
% 47.89/7.69 % (2573704)Termination reason: Refutation not found, incomplete strategy
% 47.89/7.69 % (2573704)Time elapsed: 0.334 s
% 47.89/7.69 % (2573704)Peak memory usage: 128 MB
% 47.89/7.69 % (2573704)Instructions burned: 907 (million)
% 47.89/7.69 % (2573706)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1620103459:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2954 on theBenchmark for (2954ds/596Mi)
% 47.89/7.69 % (2573706)Refutation not found, incomplete strategy
% 47.89/7.69 % (2573706)------------------------------
% 47.89/7.69 % (2573706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.89/7.69 % (2573706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.89/7.69 % (2573706)CaDiCaL version: 2.1.3
% 47.89/7.69 % (2573706)Termination reason: Refutation not found, incomplete strategy
% 47.89/7.69 % (2573706)Time elapsed: 0.002 s
% 47.89/7.69 % (2573706)Peak memory usage: 88 MB
% 47.89/7.69 % (2573706)Instructions burned: 2 (million)
% 47.89/7.69 % (2573704)------------------------------
% 47.89/7.69 % (2573704)------------------------------
% 47.89/7.69 % (2573708)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=1291881034:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2952 on theBenchmark for (2952ds/4123Mi)
% 47.89/7.69 % (2573706)------------------------------
% 47.89/7.69 % (2573706)------------------------------
% 47.89/7.69 % (2573710)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3635856800:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2950 on theBenchmark for (2950ds/16411Mi)
% 47.89/7.69 % (2573691)Instruction limit reached!
% 47.89/7.69 % (2573691)------------------------------
% 47.89/7.69 % (2573691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.89/7.69 % (2573691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.89/7.69 % (2573691)CaDiCaL version: 2.1.3
% 47.89/7.69 % (2573691)Termination reason: Instruction limit
% 47.89/7.69 % (2573691)Termination phase: Saturation
% 47.89/7.69 % (2573691)Time elapsed: 2.284 s
% 47.89/7.69 % (2573691)Peak memory usage: 142 MB
% 47.89/7.69 % (2573691)Instructions burned: 2990 (million)
% 47.89/7.69 % (2573712)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3764264825:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2946 on theBenchmark for (2946ds/1670Mi)
% 47.89/7.69 % (2573702)Instruction limit reached!
% 47.89/7.69 % (2573702)------------------------------
% 47.89/7.69 % (2573702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.89/7.69 % (2573702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.89/7.69 % (2573702)CaDiCaL version: 2.1.3
% 47.89/7.69 % (2573702)Termination reason: Instruction limit
% 47.89/7.69 % (2573702)Termination phase: Saturation
% 47.89/7.69 % (2573702)Time elapsed: 1.826 s
% 47.89/7.69 % (2573702)Peak memory usage: 135 MB
% 47.89/7.69 % (2573702)Instructions burned: 2942 (million)
% 47.89/7.69 % (2573714)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3748367264:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2940 on theBenchmark for (2940ds/1722Mi)
% 47.89/7.69 % (2573708)Instruction limit reached!
% 47.89/7.69 % (2573708)------------------------------
% 47.89/7.69 % (2573708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.89/7.69 % (2573708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.89/7.69 % (2573708)CaDiCaL version: 2.1.3
% 47.89/7.69 % (2573708)Termination reason: Instruction limit
% 47.89/7.69 % (2573708)Termination phase: Saturation
% 47.89/7.69 % (2573708)Time elapsed: 1.269 s
% 47.89/7.69 % (2573708)Peak memory usage: 135 MB
% 47.89/7.69 % (2573708)Instructions burned: 4128 (million)
% 47.89/7.69 % (2573716)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1900110474:cts=off:cond=on:i=9530:bs=on:fsd=on_2938 on theBenchmark for (2938ds/9530Mi)
% 47.89/7.69 % (2573712)Instruction limit reached!
% 47.89/7.69 % (2573712)------------------------------
% 47.89/7.69 % (2573712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.89/7.69 % (2573712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.89/7.69 % (2573712)CaDiCaL version: 2.1.3
% 47.89/7.69 % (2573712)Termination reason: Instruction limit
% 47.89/7.69 % (2573712)Termination phase: Saturation
% 47.89/7.69 % (2573712)Time elapsed: 1.019 s
% 47.89/7.69 % (2573712)Peak memory usage: 134 MB
% 47.89/7.69 % (2573712)Instructions burned: 1672 (million)
% 47.89/7.69 % (2573710)First to succeed.
% 47.89/7.69 % (2573710)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2573623"
% 47.89/7.69 % (2573718)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3874080882:st=2:i=4495:sd=10:ss=included_2935 on theBenchmark for (2935ds/4495Mi)
% 47.89/7.69 % SZS status Satisfiable for theBenchmark
% 47.89/7.69 % SZS output start Saturation.
% See solution above
% 48.95/7.88 % SZS output start Definitions and Model Updates.
% 48.95/7.88 % SZS output end Definitions and Model Updates.
% 48.95/7.88 % (2573710)------------------------------
% 48.95/7.88 % (2573710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.95/7.88 % (2573710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.95/7.88 % (2573710)CaDiCaL version: 2.1.3
% 48.95/7.88 % (2573710)Termination reason: Satisfiable
% 48.95/7.88 % (2573710)Time elapsed: 1.539 s
% 48.95/7.88 % (2573710)Peak memory usage: 137 MB
% 48.95/7.88 % (2573710)Instructions burned: 2145 (million)
% 48.95/7.88 % (2573710)------------------------------
% 48.95/7.88 % (2573710)------------------------------
% 48.95/7.88 % (2573623)Success in time 6.842 s
% 48.95/7.88 % Vampire exiting
%------------------------------------------------------------------------------