%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP124-9.005 : 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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:12:43 AM UTC 2026
% Result : Satisfiable 46.33s 7.46s
% Output : Saturation 46.96s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u60,axiom,
~ product1(e_4,e_5,e_3) ).
cnf(u64,axiom,
~ product1(e_4,e_5,e_2) ).
cnf(u69,axiom,
product1(e_4,e_5,e_1) ).
cnf(u93,axiom,
~ product1(e_5,e_4,e_4) ).
cnf(u98,axiom,
product1(e_5,e_4,e_3) ).
cnf(u101,axiom,
~ product1(e_5,e_4,e_2) ).
cnf(u105,axiom,
~ product1(e_5,e_4,e_1) ).
cnf(u110,axiom,
~ product1(e_5,e_3,e_4) ).
cnf(u114,axiom,
~ product1(e_5,e_3,e_3) ).
cnf(u118,axiom,
~ product1(e_5,e_3,e_2) ).
cnf(u123,axiom,
product1(e_5,e_3,e_1) ).
cnf(u128,axiom,
product1(e_5,e_2,e_4) ).
cnf(u131,axiom,
~ product1(e_5,e_2,e_3) ).
cnf(u135,axiom,
~ product1(e_5,e_2,e_2) ).
cnf(u139,axiom,
~ product1(e_5,e_2,e_1) ).
cnf(u144,axiom,
~ product1(e_5,e_1,e_4) ).
cnf(u148,axiom,
~ product1(e_5,e_1,e_3) ).
cnf(u153,axiom,
product1(e_5,e_1,e_2) ).
cnf(u156,axiom,
~ product1(e_5,e_1,e_1) ).
cnf(u212,negated_conjecture,
~ product1(e_3,e_4,e_4) ).
cnf(u216,negated_conjecture,
~ product1(e_3,e_4,e_3) ).
cnf(u220,negated_conjecture,
~ product1(e_3,e_4,e_2) ).
cnf(u224,negated_conjecture,
~ product1(e_3,e_4,e_1) ).
cnf(u232,negated_conjecture,
~ product1(e_4,e_3,e_4) ).
cnf(u236,negated_conjecture,
~ product1(e_4,e_3,e_3) ).
cnf(u241,negated_conjecture,
product1(e_4,e_3,e_2) ).
cnf(u244,negated_conjecture,
~ product1(e_4,e_3,e_1) ).
cnf(u259,negated_conjecture,
~ product1(e_1,e_4,e_4) ).
cnf(u263,negated_conjecture,
~ product1(e_1,e_4,e_3) ).
cnf(u268,negated_conjecture,
product1(e_1,e_4,e_2) ).
cnf(u271,negated_conjecture,
~ product1(e_1,e_4,e_1) ).
cnf(u336,axiom,
product2(e_4,e_5,e_3) ).
cnf(u339,axiom,
~ product2(e_4,e_5,e_2) ).
cnf(u374,negated_conjecture,
~ product1(e_2,e_5,e_1) ).
cnf(u378,negated_conjecture,
~ product1(e_2,e_5,e_4) ).
cnf(u383,negated_conjecture,
product1(e_2,e_5,e_3) ).
cnf(u386,negated_conjecture,
~ product1(e_2,e_5,e_2) ).
cnf(u396,negated_conjecture,
~ product2(e_5,e_5,e_4) ).
cnf(u401,negated_conjecture,
product1(e_2,e_4,e_1) ).
cnf(u404,negated_conjecture,
~ product1(e_2,e_4,e_4) ).
cnf(u408,negated_conjecture,
~ product1(e_2,e_4,e_3) ).
cnf(u412,negated_conjecture,
~ product1(e_2,e_4,e_2) ).
cnf(u447,negated_conjecture,
~ product1(e_1,e_5,e_1) ).
cnf(u452,negated_conjecture,
product1(e_1,e_5,e_4) ).
cnf(u455,negated_conjecture,
~ product1(e_1,e_5,e_3) ).
cnf(u459,negated_conjecture,
~ product1(e_1,e_5,e_2) ).
cnf(u485,negated_conjecture,
~ product2(e_5,e_4,e_3) ).
cnf(u489,negated_conjecture,
~ product1(e_2,e_3,e_1) ).
cnf(u494,negated_conjecture,
product1(e_2,e_3,e_4) ).
cnf(u497,negated_conjecture,
~ product1(e_2,e_3,e_3) ).
cnf(u501,negated_conjecture,
~ product1(e_2,e_3,e_2) ).
cnf(u522,negated_conjecture,
~ product2(e_5,e_3,e_4) ).
cnf(u533,negated_conjecture,
~ product1(e_1,e_3,e_1) ).
cnf(u537,negated_conjecture,
~ product1(e_1,e_3,e_4) ).
cnf(u570,negated_conjecture,
~ product2(e_5,e_5,e_2) ).
cnf(u574,negated_conjecture,
~ product1(e_1,e_2,e_1) ).
cnf(u578,negated_conjecture,
~ product1(e_1,e_2,e_4) ).
cnf(u583,negated_conjecture,
product1(e_1,e_2,e_3) ).
cnf(u586,negated_conjecture,
~ product1(e_1,e_2,e_2) ).
cnf(u632,negated_conjecture,
~ product1(e_3,e_5,e_1) ).
cnf(u636,negated_conjecture,
~ product1(e_3,e_5,e_4) ).
cnf(u641,negated_conjecture,
product1(e_3,e_5,e_2) ).
cnf(u684,negated_conjecture,
~ product1(e_3,e_5,e_3) ).
cnf(u696,negated_conjecture,
~ product2(e_5,e_4,e_2) ).
cnf(u718,negated_conjecture,
product1(e_3,e_2,e_1) ).
cnf(u721,negated_conjecture,
~ product1(e_3,e_2,e_4) ).
cnf(u725,negated_conjecture,
~ product1(e_3,e_2,e_3) ).
cnf(u729,negated_conjecture,
~ product1(e_3,e_2,e_2) ).
cnf(u777,negated_conjecture,
~ product2(e_5,e_5,e_3) ).
cnf(u878,negated_conjecture,
~ product2(e_5,e_5,e_1) ).
cnf(u882,negated_conjecture,
~ product1(e_3,e_1,e_1) ).
cnf(u887,negated_conjecture,
product1(e_3,e_1,e_4) ).
cnf(u890,negated_conjecture,
~ product1(e_3,e_1,e_3) ).
cnf(u894,negated_conjecture,
~ product1(e_3,e_1,e_2) ).
cnf(u905,negated_conjecture,
~ product1(e_2,e_1,e_1) ).
cnf(u909,negated_conjecture,
~ product1(e_2,e_1,e_4) ).
cnf(u913,negated_conjecture,
~ product1(e_2,e_1,e_3) ).
cnf(u917,negated_conjecture,
~ product1(e_2,e_1,e_2) ).
cnf(u1003,negated_conjecture,
~ product2(e_5,e_2,e_1) ).
cnf(u1159,negated_conjecture,
~ product2(e_5,e_1,e_2) ).
cnf(u1163,negated_conjecture,
~ product1(e_4,e_2,e_1) ).
cnf(u1167,negated_conjecture,
~ product1(e_4,e_2,e_4) ).
cnf(u1171,negated_conjecture,
~ product1(e_4,e_2,e_3) ).
cnf(u1175,negated_conjecture,
~ product1(e_4,e_2,e_2) ).
cnf(u1290,negated_conjecture,
~ product2(e_5,e_2,e_4) ).
cnf(u1303,negated_conjecture,
product2(e_5,e_4,e_1) ).
cnf(u1375,negated_conjecture,
product2(e_5,e_2,e_3) ).
cnf(u1426,negated_conjecture,
product2(e_5,e_3,e_2) ).
cnf(u1455,negated_conjecture,
~ product1(e_4,e_1,e_1) ).
cnf(u1459,negated_conjecture,
~ product1(e_4,e_1,e_4) ).
cnf(u1464,negated_conjecture,
product1(e_4,e_1,e_3) ).
cnf(u1467,negated_conjecture,
~ product1(e_4,e_1,e_2) ).
cnf(u1740,negated_conjecture,
product2(e_5,e_1,e_4) ).
cnf(u2477,negated_conjecture,
~ product2(e_3,e_5,e_3) ).
cnf(u2481,negated_conjecture,
~ product2(e_3,e_5,e_2) ).
cnf(u2486,negated_conjecture,
product2(e_3,e_5,e_1) ).
cnf(u2518,negated_conjecture,
product2(e_2,e_3,e_1) ).
cnf(u2719,negated_conjecture,
( ~ product1(e_1,e_3,X0)
| equalish(X0,e_5) ) ).
cnf(u3066,negated_conjecture,
( ~ group_element(X0)
| equalish(e_1,X0)
| product1(X0,e_3,e_1)
| product1(X0,e_3,e_4)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_2) ) ).
cnf(u3144,axiom,
( ~ group_element(X0)
| product1(X0,e_1,e_2)
| product1(X0,e_1,e_3)
| product1(X0,e_1,e_4)
| product1(X0,e_1,e_1)
| product1(X0,e_2,e_1)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_3)
| product1(X0,e_2,e_4) ) ).
cnf(u2423,negated_conjecture,
( ~ product2(e_4,e_3,X0)
| equalish(X0,e_5) ) ).
cnf(u1410,negated_conjecture,
( ~ product1(e_5,X0,e_3)
| product2(e_2,X0,e_5) ) ).
cnf(u2637,negated_conjecture,
( ~ product2(X0,e_5,e_2)
| equalish(X0,e_1) ) ).
cnf(u314,negated_conjecture,
( ~ product1(X2,X1,X2)
| equalish(X0,X2)
| ~ product2(X0,X1,X2) ) ).
cnf(u50,axiom,
( product1(X0,e_5,e_4)
| product1(X0,e_5,e_1)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| equalish(X0,e_5)
| ~ group_element(X0) ) ).
cnf(u3166,axiom,
( ~ group_element(X0)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_4)
| product1(X0,e_3,e_1)
| product1(X0,e_5,e_1)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| product1(X0,e_5,e_4) ) ).
cnf(u2822,negated_conjecture,
( ~ group_element(X0)
| product2(e_1,X0,e_1)
| product2(e_1,X0,e_2)
| product2(e_1,X0,e_3)
| product2(e_1,X0,e_4)
| equalish(e_2,X0) ) ).
cnf(u3113,axiom,
( ~ group_element(X0)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_3)
| product1(X0,e_4,e_4)
| product1(X0,e_4,e_1)
| product1(X0,e_3,e_1)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_4) ) ).
cnf(u1887,axiom,
( ~ product1(X0,e_3,e_1)
| equalish(X0,e_5) ) ).
cnf(u2355,negated_conjecture,
( ~ product2(X0,e_4,e_1)
| equalish(X0,e_5) ) ).
cnf(u2815,axiom,
( ~ group_element(X1)
| product2(e_2,X0,e_1)
| product2(e_2,X0,e_2)
| product2(e_2,X0,e_3)
| product2(e_2,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| product2(e_2,X1,e_1)
| product2(e_2,X1,e_2)
| product2(e_2,X1,e_3)
| product2(e_2,X1,e_4) ) ).
cnf(u2357,negated_conjecture,
( ~ product2(e_5,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u1706,negated_conjecture,
product2(e_2,e_5,e_4) ).
cnf(u2737,axiom,
( ~ group_element(X2)
| equalish(X0,X1)
| product1(X1,X2,e_1)
| product1(X1,X2,e_2)
| product1(X1,X2,e_3)
| product1(X1,X2,e_4)
| ~ group_element(X1)
| product1(X0,X2,e_1)
| product1(X0,X2,e_2)
| product1(X0,X2,e_3)
| product1(X0,X2,e_4)
| ~ group_element(X0) ) ).
cnf(u2772,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product2(e_4,X1,e_1)
| product2(e_4,X1,e_2)
| product2(e_4,X1,e_3)
| product2(e_4,X1,e_4)
| ~ product2(e_4,X1,X0) ) ).
cnf(u2442,negated_conjecture,
( ~ product2(X0,e_4,e_3)
| equalish(X0,e_1) ) ).
cnf(u2387,negated_conjecture,
product2(e_4,e_1,e_2) ).
cnf(u2444,negated_conjecture,
( ~ product2(e_1,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u2639,negated_conjecture,
( ~ product2(e_1,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(u2389,negated_conjecture,
( ~ product2(X0,e_1,e_2)
| equalish(X0,e_4) ) ).
cnf(u2988,negated_conjecture,
( ~ group_element(X0)
| product1(e_5,X0,e_4)
| product1(e_5,X0,e_3)
| product1(e_5,X0,e_1)
| product2(e_5,e_2,X0)
| product1(e_5,X0,e_2)
| product1(X0,e_2,e_1)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_3)
| product1(X0,e_2,e_4) ) ).
cnf(u1713,negated_conjecture,
~ product1(e_4,e_5,e_4) ).
cnf(u2759,negated_conjecture,
( ~ group_element(X0)
| product1(X0,e_5,e_3)
| equalish(X0,e_5)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_1)
| equalish(e_1,X0) ) ).
cnf(u2816,negated_conjecture,
( ~ group_element(X0)
| product2(e_3,X0,e_1)
| product2(e_3,X0,e_2)
| product2(e_3,X0,e_3)
| product2(e_3,X0,e_4)
| equalish(e_1,X0) ) ).
cnf(u2521,negated_conjecture,
( ~ product2(e_2,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u2520,negated_conjecture,
( ~ product2(X0,e_3,e_1)
| equalish(X0,e_2) ) ).
cnf(u1865,negated_conjecture,
( ~ product1(X0,e_3,e_2)
| equalish(X0,e_4) ) ).
cnf(u2324,negated_conjecture,
( ~ product2(X0,e_3,e_4)
| equalish(X0,e_1) ) ).
cnf(u43,axiom,
equalish(X0,X0) ).
cnf(u1889,negated_conjecture,
( ~ product1(e_3,X0,e_5)
| product2(e_1,X0,e_3) ) ).
cnf(u2396,axiom,
( ~ product2(e_4,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u2192,negated_conjecture,
( ~ product1(X0,e_1,e_3)
| equalish(X0,e_4) ) ).
cnf(u2295,negated_conjecture,
( ~ group_element(X0)
| product2(e_4,X0,e_2)
| product1(e_2,X0,e_1)
| product1(e_2,X0,e_2)
| product1(e_2,X0,e_3)
| product1(e_2,X0,e_4) ) ).
cnf(u2352,negated_conjecture,
( ~ product2(e_2,X0,e_5)
| equalish(X0,e_4) ) ).
cnf(u326,axiom,
( ~ group_element(X0)
| product2(X0,e_5,e_2)
| product2(X0,e_5,e_3)
| equalish(X0,e_5)
| product2(X0,e_5,e_1)
| ~ product2(X0,X1,e_4)
| equalish(X1,e_5) ) ).
cnf(u2390,negated_conjecture,
( ~ product2(e_4,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u2318,negated_conjecture,
~ product1(e_5,e_1,e_5) ).
cnf(u1878,negated_conjecture,
( ~ product1(e_5,X0,e_4)
| product2(e_1,X0,e_5) ) ).
cnf(u2113,negated_conjecture,
( ~ product1(e_2,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(u2346,axiom,
( ~ product1(e_5,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u1911,negated_conjecture,
( ~ product2(e_5,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u2275,negated_conjecture,
( ~ product2(X0,e_2,e_5)
| equalish(X0,e_1) ) ).
cnf(u2348,negated_conjecture,
( ~ product2(X0,e_5,e_4)
| equalish(X0,e_2) ) ).
cnf(u2345,axiom,
( ~ product1(X0,e_4,e_3)
| equalish(X0,e_5) ) ).
cnf(u2119,negated_conjecture,
( ~ product1(X0,e_5,e_4)
| equalish(X0,e_1) ) ).
cnf(u2277,negated_conjecture,
( ~ product2(e_1,e_2,X0)
| equalish(X0,e_5) ) ).
cnf(u52,axiom,
( ~ group_element(X0)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| equalish(X0,e_5)
| product1(X0,e_5,e_1)
| ~ product1(X0,X1,e_4)
| equalish(X1,e_5) ) ).
cnf(u2468,negated_conjecture,
( ~ product2(e_3,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u74,axiom,
( ~ product1(X0,X0,X1)
| equalish(X1,X0) ) ).
cnf(u46,axiom,
( ~ product1(X0,X1,X1)
| equalish(X0,X1) ) ).
cnf(u2339,negated_conjecture,
( ~ product1(X0,e_2,e_3)
| equalish(X0,e_1) ) ).
cnf(u76,axiom,
( ~ group_element(X0)
| equalish(X1,e_4)
| product1(X0,e_5,e_1)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| equalish(X0,e_5)
| ~ product1(X0,e_5,X1) ) ).
cnf(u45,axiom,
( ~ group_element(X0)
| equalish(X0,e_5)
| product1(e_5,X0,e_1)
| product1(e_5,X0,e_2)
| product1(e_5,X0,e_3)
| product1(e_5,X0,e_4) ) ).
cnf(u2807,axiom,
( ~ product2(e_4,X0,e_5)
| ~ group_element(X1)
| product2(e_4,X1,e_1)
| product2(e_4,X1,e_2)
| product2(e_4,X1,e_3)
| product2(e_4,X1,e_4)
| equalish(X0,X1) ) ).
cnf(u353,negated_conjecture,
( ~ product1(X0,X1,e_2)
| product1(e_2,X0,e_2)
| product1(e_2,X0,e_3)
| product1(e_2,X0,e_4)
| ~ group_element(X0)
| product1(e_2,X0,e_1)
| product2(e_5,X1,X0) ) ).
cnf(u2341,negated_conjecture,
( ~ product1(e_2,X0,e_1)
| product2(e_3,X0,e_2) ) ).
cnf(product1_idempotence,axiom,
product1(X0,X0,X0) ).
cnf(u39,negated_conjecture,
( product2(X0,X1,X0)
| ~ product1(X0,X1,X0) ) ).
cnf(u3036,axiom,
( ~ group_element(X0)
| product1(X1,e_4,e_1)
| product1(X1,e_4,e_2)
| product1(X1,e_4,e_3)
| product1(X1,e_4,e_4)
| ~ group_element(X1)
| product1(X0,e_4,e_1)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_3)
| product1(X0,e_4,e_4)
| equalish(X0,X1) ) ).
cnf(u1946,negated_conjecture,
product2(e_1,e_2,e_5) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3) ).
cnf(u184,negated_conjecture,
( ~ product1(X0,X1,X0)
| equalish(X2,X0)
| ~ product2(X0,X1,X2) ) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2) ).
cnf(u2414,negated_conjecture,
( ~ product2(e_3,e_1,X0)
| equalish(X0,e_5) ) ).
cnf(product1_total_function1,axiom,
( product1(X0,X1,e_5)
| ~ group_element(X1)
| product1(X0,X1,e_1)
| product1(X0,X1,e_2)
| product1(X0,X1,e_3)
| product1(X0,X1,e_4)
| ~ group_element(X0) ) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u2363,negated_conjecture,
( ~ group_element(X0)
| product2(e_3,X0,e_4)
| product1(e_4,X0,e_1)
| product1(e_4,X0,e_2)
| product1(e_4,X0,e_3)
| product1(e_4,X0,e_4) ) ).
cnf(u2885,negated_conjecture,
( ~ group_element(X0)
| product2(X0,e_5,e_3)
| equalish(X0,e_5)
| product2(X0,e_5,e_2)
| product2(X0,e_5,e_1)
| equalish(e_2,X0) ) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(u3184,axiom,
( ~ group_element(X0)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_3)
| product1(X0,e_2,e_4)
| product1(X0,e_2,e_1)
| product1(X0,e_5,e_1)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| product1(X0,e_5,e_4) ) ).
cnf(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5) ).
cnf(u1926,negated_conjecture,
( ~ product1(e_1,X0,e_3)
| product2(e_4,X0,e_1) ) ).
cnf(u2164,negated_conjecture,
( ~ product1(X0,e_3,e_4)
| equalish(X0,e_2) ) ).
cnf(u2395,axiom,
( ~ product2(X0,e_5,e_3)
| equalish(X0,e_4) ) ).
cnf(u2638,negated_conjecture,
( ~ product2(e_1,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(u1409,negated_conjecture,
( ~ product1(e_3,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(u2193,negated_conjecture,
( ~ product1(e_4,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u2397,axiom,
( ~ product2(e_4,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(u2813,negated_conjecture,
( ~ group_element(X0)
| product2(e_2,X0,e_1)
| product2(e_2,X0,e_2)
| product2(e_2,X0,e_3)
| product2(e_2,X0,e_4)
| equalish(e_4,X0) ) ).
cnf(u2590,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_3)
| product2(e_4,X0,e_1)
| product2(e_4,X0,e_2)
| product2(e_4,X0,e_3)
| product2(e_4,X0,e_4) ) ).
cnf(u3101,axiom,
( ~ group_element(X0)
| product1(X1,e_1,e_1)
| product1(X1,e_1,e_2)
| product1(X1,e_1,e_3)
| product1(X1,e_1,e_4)
| ~ group_element(X1)
| equalish(X0,e_1)
| product1(X1,X0,e_1)
| product1(X1,X0,e_2)
| product1(X1,X0,e_3)
| product1(X1,X0,e_4) ) ).
cnf(u2522,negated_conjecture,
( ~ product2(e_2,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u3104,axiom,
( ~ group_element(X0)
| product1(X1,e_4,e_1)
| product1(X1,e_4,e_2)
| product1(X1,e_4,e_3)
| product1(X1,e_4,e_4)
| ~ group_element(X1)
| equalish(X0,e_4)
| product1(X1,X0,e_1)
| product1(X1,X0,e_2)
| product1(X1,X0,e_3)
| product1(X1,X0,e_4) ) ).
cnf(u2808,axiom,
( ~ product2(e_5,X0,e_5)
| ~ group_element(X1)
| product2(e_5,X1,e_1)
| product2(e_5,X1,e_2)
| product2(e_5,X1,e_3)
| product2(e_5,X1,e_4)
| equalish(X0,X1) ) ).
cnf(u2684,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product1(e_5,X1,e_1)
| product1(e_5,X1,e_2)
| product1(e_5,X1,e_3)
| product1(e_5,X1,e_4)
| ~ product1(e_5,X1,X0) ) ).
cnf(u2804,axiom,
( ~ product2(e_1,X0,e_5)
| ~ group_element(X1)
| product2(e_1,X1,e_1)
| product2(e_1,X1,e_2)
| product2(e_1,X1,e_3)
| product2(e_1,X1,e_4)
| equalish(X0,X1) ) ).
cnf(u2254,negated_conjecture,
( ~ product1(e_2,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u2356,negated_conjecture,
( ~ product2(e_5,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u2196,axiom,
( ~ product1(e_5,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u2698,negated_conjecture,
( ~ product1(e_2,e_1,X0)
| equalish(X0,e_5) ) ).
cnf(u2595,negated_conjecture,
( ~ product2(e_3,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u2350,negated_conjecture,
( ~ product2(e_2,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u202,negated_conjecture,
~ product1(e_2,e_4,e_5) ).
cnf(u2266,axiom,
( ~ product1(X0,e_2,e_4)
| equalish(X0,e_5) ) ).
cnf(u2738,axiom,
( ~ group_element(X0)
| product1(X0,e_5,e_1)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| product1(X0,e_5,e_4)
| equalish(e_5,X0) ) ).
cnf(u2268,negated_conjecture,
( ~ product1(e_2,X0,e_5)
| product2(e_4,X0,e_2) ) ).
cnf(u1405,negated_conjecture,
( ~ group_element(X0)
| product1(e_4,X0,e_3)
| product1(e_4,X0,e_4)
| product1(e_4,X0,e_2)
| product1(e_4,X0,e_1)
| product1(X0,e_5,e_1)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| equalish(X0,e_5) ) ).
cnf(u2428,negated_conjecture,
( ~ group_element(X0)
| product2(X0,e_3,e_1)
| product2(X0,e_3,e_2)
| product2(X0,e_3,e_3)
| product2(X0,e_3,e_4)
| equalish(X0,e_4) ) ).
cnf(u81,axiom,
( ~ group_element(X0)
| equalish(e_5,X0)
| product1(X0,X0,e_1)
| product1(X0,X0,e_2)
| product1(X0,X0,e_3)
| product1(X0,X0,e_4) ) ).
cnf(u2812,axiom,
( ~ group_element(X1)
| product2(e_5,X0,e_1)
| product2(e_5,X0,e_2)
| product2(e_5,X0,e_3)
| product2(e_5,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| product2(e_5,X1,e_1)
| product2(e_5,X1,e_2)
| product2(e_5,X1,e_3)
| product2(e_5,X1,e_4) ) ).
cnf(u2199,negated_conjecture,
( ~ product1(e_1,X0,e_5)
| product2(e_2,X0,e_1) ) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(u2422,negated_conjecture,
( ~ product2(e_4,X0,e_5)
| equalish(X0,e_3) ) ).
cnf(u1877,axiom,
( ~ product1(e_4,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(u1888,axiom,
( ~ product1(e_5,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u2370,negated_conjecture,
( ~ group_element(X0)
| product2(X0,e_4,e_1)
| product2(X0,e_4,e_2)
| product2(X0,e_4,e_3)
| product2(X0,e_4,e_4)
| equalish(X0,e_2) ) ).
cnf(u1875,axiom,
( ~ product1(e_4,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(u2369,negated_conjecture,
~ product1(e_5,e_4,e_5) ).
cnf(u2241,negated_conjecture,
( ~ product1(e_3,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u2592,negated_conjecture,
product2(e_3,e_4,e_2) ).
cnf(u312,axiom,
( ~ group_element(X0)
| equalish(X0,e_5)
| product2(e_5,X0,e_1)
| product2(e_5,X0,e_2)
| product2(e_5,X0,e_3)
| product2(e_5,X0,e_4) ) ).
cnf(u2631,negated_conjecture,
( ~ product2(e_4,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u2770,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product2(e_2,X1,e_1)
| product2(e_2,X1,e_2)
| product2(e_2,X1,e_3)
| product2(e_2,X1,e_4)
| ~ product2(e_2,X1,X0) ) ).
cnf(u2335,negated_conjecture,
( ~ product1(e_4,X0,e_1)
| product2(e_2,X0,e_4) ) ).
cnf(u2819,negated_conjecture,
( ~ group_element(X0)
| product2(e_4,X0,e_1)
| product2(e_4,X0,e_2)
| product2(e_4,X0,e_3)
| product2(e_4,X0,e_4)
| equalish(e_3,X0) ) ).
cnf(u2166,negated_conjecture,
( ~ product1(e_3,X0,e_2)
| product2(e_4,X0,e_3) ) ).
cnf(u2441,negated_conjecture,
product2(e_1,e_4,e_3) ).
cnf(u3034,axiom,
( ~ group_element(X0)
| product1(X1,e_2,e_1)
| product1(X1,e_2,e_2)
| product1(X1,e_2,e_3)
| product1(X1,e_2,e_4)
| ~ group_element(X1)
| product1(X0,e_2,e_1)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_3)
| product1(X0,e_2,e_4)
| equalish(X0,X1) ) ).
cnf(u2120,negated_conjecture,
( ~ product1(e_1,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u2114,negated_conjecture,
( ~ product1(X0,e_5,e_3)
| equalish(X0,e_2) ) ).
cnf(u2596,negated_conjecture,
( ~ product2(e_3,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(u51,axiom,
( ~ product1(X1,e_5,e_4)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| equalish(X0,e_5)
| ~ group_element(X0)
| product1(X0,e_5,e_1)
| equalish(X1,X0) ) ).
cnf(u2657,negated_conjecture,
( ~ product1(e_5,X0,e_5)
| ~ group_element(X1)
| product1(e_5,X1,e_1)
| product1(e_5,X1,e_2)
| product1(e_5,X1,e_3)
| product1(e_5,X1,e_4)
| equalish(X0,X1) ) ).
cnf(u1912,negated_conjecture,
( ~ product2(e_5,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u2116,negated_conjecture,
( ~ product1(e_5,X0,e_2)
| product2(e_3,X0,e_5) ) ).
cnf(u53,negated_conjecture,
( ~ group_element(X0)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| equalish(X0,e_5)
| product1(X0,e_5,e_1)
| ~ product1(e_5,X1,X0)
| product2(e_4,X1,e_5) ) ).
cnf(u40,negated_conjecture,
( ~ group_element(X1)
| product1(X1,X0,e_1)
| product1(X1,X0,e_2)
| product1(X1,X0,e_3)
| product1(X1,X0,e_4)
| ~ group_element(X0)
| ~ product1(X0,X2,X1)
| product2(e_5,X2,X0) ) ).
cnf(u47,axiom,
( ~ product1(X0,X1,e_5)
| equalish(X0,X2)
| ~ group_element(X1)
| product1(X2,X1,e_1)
| product1(X2,X1,e_2)
| product1(X2,X1,e_3)
| product1(X2,X1,e_4)
| ~ group_element(X2) ) ).
cnf(u355,negated_conjecture,
( ~ product1(X0,X1,e_4)
| product1(e_4,X0,e_2)
| product1(e_4,X0,e_3)
| product1(e_4,X0,e_4)
| ~ group_element(X0)
| product1(e_4,X0,e_1)
| product2(e_5,X1,X0) ) ).
cnf(product2_total_function2,axiom,
( ~ product2(X0,X1,X3)
| ~ product2(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u2418,negated_conjecture,
( ~ group_element(X0)
| product2(X0,e_1,e_1)
| product2(X0,e_1,e_2)
| product2(X0,e_1,e_3)
| product2(X0,e_1,e_4)
| equalish(X0,e_3) ) ).
cnf(u2194,negated_conjecture,
( ~ product1(e_1,X0,e_4)
| product2(e_3,X0,e_1) ) ).
cnf(u2730,negated_conjecture,
( ~ product1(e_4,e_2,X0)
| equalish(X0,e_5) ) ).
cnf(u313,axiom,
( ~ product2(X0,X1,X1)
| equalish(X0,X1) ) ).
cnf(u2769,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product2(e_1,X1,e_1)
| product2(e_1,X1,e_2)
| product2(e_1,X1,e_3)
| product2(e_1,X1,e_4)
| ~ product2(e_1,X1,X0) ) ).
cnf(u2821,axiom,
( ~ group_element(X1)
| product2(e_4,X0,e_1)
| product2(e_4,X0,e_2)
| product2(e_4,X0,e_3)
| product2(e_4,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| product2(e_4,X1,e_1)
| product2(e_4,X1,e_2)
| product2(e_4,X1,e_3)
| product2(e_4,X1,e_4) ) ).
cnf(u3102,axiom,
( ~ group_element(X0)
| product1(X1,e_2,e_1)
| product1(X1,e_2,e_2)
| product1(X1,e_2,e_3)
| product1(X1,e_2,e_4)
| ~ group_element(X1)
| equalish(X0,e_2)
| product1(X1,X0,e_1)
| product1(X1,X0,e_2)
| product1(X1,X0,e_3)
| product1(X1,X0,e_4) ) ).
cnf(u1407,negated_conjecture,
( ~ product1(e_3,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(u2682,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product1(e_3,X1,e_1)
| product1(e_3,X1,e_2)
| product1(e_3,X1,e_3)
| product1(e_3,X1,e_4)
| ~ product1(e_3,X1,X0) ) ).
cnf(u1910,negated_conjecture,
( ~ product2(X0,e_3,e_2)
| equalish(X0,e_5) ) ).
cnf(u2833,axiom,
( ~ group_element(X1)
| equalish(X0,e_4)
| product2(e_4,X1,e_1)
| product2(e_4,X1,e_2)
| product2(e_4,X1,e_3)
| product2(e_4,X1,e_4)
| ~ product2(X0,X1,e_5) ) ).
cnf(u1886,axiom,
( ~ product1(e_5,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u3167,axiom,
( ~ group_element(X0)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_4)
| product1(X0,e_3,e_1)
| product1(X0,e_2,e_1)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_3)
| product1(X0,e_2,e_4) ) ).
cnf(u2118,negated_conjecture,
( ~ product1(e_1,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u2708,negated_conjecture,
( ~ product1(e_3,e_4,X0)
| equalish(X0,e_5) ) ).
cnf(u315,axiom,
( ~ group_element(X2)
| equalish(X0,X2)
| ~ group_element(X1)
| product2(X2,X1,e_1)
| product2(X2,X1,e_2)
| product2(X2,X1,e_3)
| product2(X2,X1,e_4)
| ~ product2(X0,X1,e_5) ) ).
cnf(product1_total_function2,axiom,
( ~ product1(X0,X1,X3)
| ~ product1(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u1864,negated_conjecture,
( ~ product1(e_4,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u75,axiom,
( ~ group_element(X0)
| equalish(X2,e_5)
| ~ group_element(X1)
| product1(X0,X1,e_1)
| product1(X0,X1,e_2)
| product1(X0,X1,e_3)
| product1(X0,X1,e_4)
| ~ product1(X0,X1,X2) ) ).
cnf(u2265,axiom,
( ~ product1(e_5,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u2758,axiom,
( ~ group_element(X1)
| product1(X0,e_5,e_3)
| equalish(X0,e_5)
| ~ group_element(X0)
| product1(X0,e_5,e_1)
| equalish(X1,X0)
| product1(X1,e_5,e_1)
| product1(X1,e_5,e_2)
| product1(X1,e_5,e_3)
| equalish(X1,e_5)
| product1(X0,e_5,e_2) ) ).
cnf(u2683,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product1(e_4,X1,e_1)
| product1(e_4,X1,e_2)
| product1(e_4,X1,e_3)
| product1(e_4,X1,e_4)
| ~ product1(e_4,X1,X0) ) ).
cnf(u2300,negated_conjecture,
( ~ group_element(X0)
| product2(X0,e_2,e_1)
| product2(X0,e_2,e_2)
| product2(X0,e_2,e_3)
| product2(X0,e_2,e_4)
| equalish(X0,e_1) ) ).
cnf(u2332,negated_conjecture,
( ~ product1(e_1,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(product2_total_function1,axiom,
( product2(X0,X1,e_5)
| ~ group_element(X1)
| product2(X0,X1,e_1)
| product2(X0,X1,e_2)
| product2(X0,X1,e_3)
| product2(X0,X1,e_4)
| ~ group_element(X0) ) ).
cnf(u1924,negated_conjecture,
( ~ product1(X0,e_1,e_4)
| equalish(X0,e_3) ) ).
cnf(product2_left_cancellation,axiom,
( ~ product2(X3,X1,X2)
| ~ product2(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u2326,negated_conjecture,
( ~ product2(e_1,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(u2443,negated_conjecture,
( ~ product2(e_1,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4) ).
cnf(u2570,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_4)
| product2(e_2,X0,e_1)
| product2(e_2,X0,e_2)
| product2(e_2,X0,e_3)
| product2(e_2,X0,e_4) ) ).
cnf(u185,axiom,
( ~ group_element(X0)
| equalish(X2,e_5)
| ~ group_element(X1)
| product2(X0,X1,e_1)
| product2(X0,X1,e_2)
| product2(X0,X1,e_3)
| product2(X0,X1,e_4)
| ~ product2(X0,X1,X2) ) ).
cnf(product1_right_cancellation,axiom,
( ~ product1(X0,X3,X2)
| ~ product1(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u2882,negated_conjecture,
( ~ group_element(X1)
| product2(e_5,X0,e_2)
| product2(e_5,X0,e_3)
| product2(e_5,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| product2(e_5,X0,e_1)
| product1(e_5,X1,e_1)
| product1(e_5,X1,e_2)
| product1(e_5,X1,e_3)
| product1(e_5,X1,e_4) ) ).
cnf(u2242,negated_conjecture,
( ~ product1(X0,e_2,e_1)
| equalish(X0,e_3) ) ).
cnf(u2831,axiom,
( ~ group_element(X1)
| equalish(X0,e_2)
| product2(e_2,X1,e_1)
| product2(e_2,X1,e_2)
| product2(e_2,X1,e_3)
| product2(e_2,X1,e_4)
| ~ product2(X0,X1,e_5) ) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(u2244,negated_conjecture,
( ~ product1(e_2,X0,e_3)
| product2(e_1,X0,e_2) ) ).
cnf(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(u2834,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product2(e_5,X1,e_1)
| product2(e_5,X1,e_2)
| product2(e_5,X1,e_3)
| product2(e_5,X1,e_4)
| ~ product2(X0,X1,e_5) ) ).
cnf(u3035,axiom,
( ~ group_element(X0)
| product1(X1,e_3,e_1)
| product1(X1,e_3,e_2)
| product1(X1,e_3,e_3)
| product1(X1,e_3,e_4)
| ~ group_element(X1)
| product1(X0,e_3,e_1)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_4)
| equalish(X0,X1) ) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(u2163,negated_conjecture,
( ~ product1(e_2,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(u2645,negated_conjecture,
( ~ group_element(X1)
| ~ product2(e_5,X1,X0)
| equalish(X0,e_5)
| product1(e_5,X1,e_1)
| product1(e_5,X1,e_2)
| product1(e_5,X1,e_3)
| product1(e_5,X1,e_4) ) ).
cnf(u2353,negated_conjecture,
( ~ product2(e_2,e_4,X0)
| equalish(X0,e_5) ) ).
cnf(u327,axiom,
( ~ group_element(X0)
| product2(X0,e_5,e_2)
| product2(X0,e_5,e_3)
| equalish(X0,e_5)
| product2(X0,e_5,e_1)
| ~ product2(X0,e_5,X1)
| equalish(X1,e_4) ) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(u2165,negated_conjecture,
( ~ product1(e_2,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(element_3,axiom,
group_element(e_3) ).
cnf(u2347,negated_conjecture,
( ~ product1(e_4,X0,e_5)
| product2(e_3,X0,e_4) ) ).
cnf(u2830,axiom,
( ~ group_element(X1)
| equalish(X0,e_1)
| product2(e_1,X1,e_1)
| product2(e_1,X1,e_2)
| product2(e_1,X1,e_3)
| product2(e_1,X1,e_4)
| ~ product2(X0,X1,e_5) ) ).
cnf(u2467,negated_conjecture,
( ~ product2(X0,e_2,e_4)
| equalish(X0,e_3) ) ).
cnf(u2349,negated_conjecture,
( ~ product2(e_2,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u2146,negated_conjecture,
( ~ product2(X0,e_1,e_4)
| equalish(X0,e_5) ) ).
cnf(u2771,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product2(e_3,X1,e_1)
| product2(e_3,X1,e_2)
| product2(e_3,X1,e_3)
| product2(e_3,X1,e_4)
| ~ product2(e_3,X1,X0) ) ).
cnf(u2469,negated_conjecture,
( ~ product2(e_3,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u2148,negated_conjecture,
( ~ product2(e_5,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u2191,negated_conjecture,
( ~ product1(e_4,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u3112,axiom,
( ~ group_element(X0)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_3)
| product1(X0,e_4,e_4)
| product1(X0,e_4,e_1)
| product1(X0,e_5,e_1)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| product1(X0,e_5,e_4) ) ).
cnf(u2987,negated_conjecture,
( ~ group_element(X0)
| product1(e_5,X0,e_4)
| product1(e_5,X0,e_3)
| product1(e_5,X0,e_1)
| product2(e_5,e_1,X0)
| product1(e_5,X0,e_2)
| product1(X0,e_1,e_1)
| product1(X0,e_1,e_2)
| product1(X0,e_1,e_3)
| product1(X0,e_1,e_4) ) ).
cnf(u3105,axiom,
( ~ group_element(X0)
| product1(X1,e_5,e_1)
| product1(X1,e_5,e_2)
| product1(X1,e_5,e_3)
| product1(X1,e_5,e_4)
| ~ group_element(X1)
| equalish(X0,e_5)
| product1(X1,X0,e_1)
| product1(X1,X0,e_2)
| product1(X1,X0,e_3)
| product1(X1,X0,e_4) ) ).
cnf(u2654,negated_conjecture,
( ~ product2(e_5,X0,e_5)
| equalish(X0,X1)
| ~ group_element(X1)
| product1(e_5,X1,e_1)
| product1(e_5,X1,e_2)
| product1(e_5,X1,e_3)
| product1(e_5,X1,e_4) ) ).
cnf(u2609,negated_conjecture,
( ~ product2(e_3,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(u2421,negated_conjecture,
( ~ product2(X0,e_3,e_5)
| equalish(X0,e_4) ) ).
cnf(u1925,negated_conjecture,
( ~ product1(e_3,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u1408,negated_conjecture,
( ~ product1(X0,e_5,e_2)
| equalish(X0,e_3) ) ).
cnf(u2281,negated_conjecture,
( ~ product2(e_2,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u2734,axiom,
( ~ group_element(X1)
| equalish(X0,X1)
| product1(X2,X1,e_1)
| product1(X2,X1,e_2)
| product1(X2,X1,e_3)
| product1(X2,X1,e_4)
| ~ group_element(X2)
| ~ group_element(X0)
| product1(X2,X0,e_1)
| product1(X2,X0,e_2)
| product1(X2,X0,e_3)
| product1(X2,X0,e_4) ) ).
cnf(u2824,axiom,
( ~ group_element(X1)
| product2(e_1,X0,e_1)
| product2(e_1,X0,e_2)
| product2(e_1,X0,e_3)
| product2(e_1,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| product2(e_1,X1,e_1)
| product2(e_1,X1,e_2)
| product2(e_1,X1,e_3)
| product2(e_1,X1,e_4) ) ).
cnf(u1867,negated_conjecture,
( ~ product1(e_3,X0,e_4)
| product2(e_2,X0,e_3) ) ).
cnf(u2147,negated_conjecture,
( ~ product2(e_5,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u2681,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product1(e_2,X1,e_1)
| product1(e_2,X1,e_2)
| product1(e_2,X1,e_3)
| product1(e_2,X1,e_4)
| ~ product1(e_2,X1,X0) ) ).
cnf(u1554,negated_conjecture,
( ~ product2(e_5,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u2267,axiom,
( ~ product1(e_5,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u2811,negated_conjecture,
( ~ product1(e_5,X1,e_5)
| product2(e_5,X0,e_1)
| product2(e_5,X0,e_2)
| product2(e_5,X0,e_3)
| product2(e_5,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0) ) ).
cnf(u2594,negated_conjecture,
( ~ product2(X0,e_4,e_2)
| equalish(X0,e_3) ) ).
cnf(u2256,negated_conjecture,
( ~ product1(e_2,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u352,negated_conjecture,
( ~ product1(X0,X1,e_1)
| product1(e_1,X0,e_2)
| product1(e_1,X0,e_3)
| product1(e_1,X0,e_4)
| ~ group_element(X0)
| product1(e_1,X0,e_1)
| product2(e_5,X1,X0) ) ).
cnf(u199,axiom,
( ~ group_element(X0)
| equalish(e_5,X0)
| product2(X0,X0,e_1)
| product2(X0,X0,e_2)
| product2(X0,X0,e_3)
| product2(X0,X0,e_4) ) ).
cnf(u2340,negated_conjecture,
( ~ product1(e_1,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u42,axiom,
( ~ product1(X0,X1,e_5)
| equalish(X1,X2)
| ~ group_element(X2)
| product1(X0,X2,e_1)
| product1(X0,X2,e_2)
| product1(X0,X2,e_3)
| product1(X0,X2,e_4)
| ~ group_element(X0) ) ).
cnf(u2832,axiom,
( ~ group_element(X1)
| equalish(X0,e_3)
| product2(e_3,X1,e_1)
| product2(e_3,X1,e_2)
| product2(e_3,X1,e_3)
| product2(e_3,X1,e_4)
| ~ product2(X0,X1,e_5) ) ).
cnf(u2632,negated_conjecture,
( ~ product2(e_4,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u2412,negated_conjecture,
( ~ product2(X0,e_1,e_5)
| equalish(X0,e_3) ) ).
cnf(u2208,negated_conjecture,
( ~ group_element(X0)
| product2(e_1,X0,e_3)
| product1(e_3,X0,e_1)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_3)
| product1(e_3,X0,e_4) ) ).
cnf(u2466,negated_conjecture,
product2(e_3,e_2,e_4) ).
cnf(u1876,axiom,
( ~ product1(X0,e_5,e_1)
| equalish(X0,e_4) ) ).
cnf(u1553,negated_conjecture,
( ~ product2(X0,e_2,e_3)
| equalish(X0,e_5) ) ).
cnf(u2587,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_1)
| product2(e_3,X0,e_1)
| product2(e_3,X0,e_2)
| product2(e_3,X0,e_3)
| product2(e_3,X0,e_4) ) ).
cnf(u2204,negated_conjecture,
( ~ group_element(X0)
| product2(e_2,X0,e_1)
| product1(e_1,X0,e_1)
| product1(e_1,X0,e_2)
| product1(e_1,X0,e_3)
| product1(e_1,X0,e_4) ) ).
cnf(u2773,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product2(e_5,X1,e_1)
| product2(e_5,X1,e_2)
| product2(e_5,X1,e_3)
| product2(e_5,X1,e_4)
| ~ product2(e_5,X1,X0) ) ).
cnf(u322,axiom,
( product2(X0,e_5,e_4)
| product2(X0,e_5,e_1)
| product2(X0,e_5,e_2)
| product2(X0,e_5,e_3)
| equalish(X0,e_5)
| ~ group_element(X0) ) ).
cnf(u2198,axiom,
( ~ product1(e_5,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u2280,negated_conjecture,
( ~ product2(X0,e_1,e_3)
| equalish(X0,e_2) ) ).
cnf(u2121,negated_conjecture,
( ~ product1(e_5,X0,e_1)
| product2(e_4,X0,e_5) ) ).
cnf(u2156,negated_conjecture,
( ~ group_element(X0)
| product1(X0,e_5,e_1)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| equalish(X0,e_5)
| equalish(X0,e_1) ) ).
cnf(u2115,negated_conjecture,
( ~ product1(e_2,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u2630,negated_conjecture,
( ~ product2(X0,e_2,e_1)
| equalish(X0,e_4) ) ).
cnf(u3033,axiom,
( ~ group_element(X0)
| product1(X1,e_1,e_1)
| product1(X1,e_1,e_2)
| product1(X1,e_1,e_3)
| product1(X1,e_1,e_4)
| ~ group_element(X1)
| product1(X0,e_1,e_1)
| product1(X0,e_1,e_2)
| product1(X0,e_1,e_3)
| product1(X0,e_1,e_4)
| equalish(X0,X1) ) ).
cnf(u2276,negated_conjecture,
( ~ product2(e_1,X0,e_5)
| equalish(X0,e_2) ) ).
cnf(u3114,axiom,
( ~ group_element(X0)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_3)
| product1(X0,e_4,e_4)
| product1(X0,e_4,e_1)
| product1(X0,e_2,e_1)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_3)
| product1(X0,e_2,e_4) ) ).
cnf(u2427,negated_conjecture,
~ product1(e_5,e_3,e_5) ).
cnf(u41,axiom,
( ~ product1(X0,X1,X0)
| equalish(X1,X0) ) ).
cnf(u3142,axiom,
( ~ group_element(X0)
| product1(X0,e_1,e_2)
| product1(X0,e_1,e_3)
| product1(X0,e_1,e_4)
| product1(X0,e_1,e_1)
| product1(X0,e_5,e_1)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| product1(X0,e_5,e_4) ) ).
cnf(u1879,negated_conjecture,
product2(e_2,e_4,e_5) ).
cnf(product2_right_cancellation,axiom,
( ~ product2(X0,X3,X2)
| ~ product2(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u2391,negated_conjecture,
( ~ product2(e_4,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u359,negated_conjecture,
( ~ group_element(X1)
| product1(e_5,X0,e_3)
| product1(e_5,X0,e_4)
| ~ group_element(X0)
| product1(e_5,X0,e_1)
| product2(e_5,X1,X0)
| product1(e_5,X0,e_2)
| product1(X0,X1,e_1)
| product1(X0,X1,e_2)
| product1(X0,X1,e_3)
| product1(X0,X1,e_4) ) ).
cnf(qg2a,negated_conjecture,
( ~ product1(X2,X0,X3)
| ~ product1(X0,X1,X2)
| product2(X3,X1,X0) ) ).
cnf(u2420,negated_conjecture,
product2(e_4,e_3,e_5) ).
cnf(product2_idempotence,axiom,
product2(X0,X0,X0) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1) ).
cnf(u2658,negated_conjecture,
( ~ group_element(X0)
| ~ group_element(X1)
| product1(e_5,X1,e_1)
| product1(e_5,X1,e_2)
| product1(e_5,X1,e_3)
| product1(e_5,X1,e_4)
| equalish(X0,X1)
| product2(e_5,X0,e_1)
| product2(e_5,X0,e_2)
| product2(e_5,X0,e_3)
| product2(e_5,X0,e_4) ) ).
cnf(u2411,negated_conjecture,
product2(e_3,e_1,e_5) ).
cnf(product1_left_cancellation,axiom,
( ~ product1(X3,X1,X2)
| ~ product1(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u2413,negated_conjecture,
( ~ product2(e_3,X0,e_5)
| equalish(X0,e_1) ) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(u2373,negated_conjecture,
( ~ group_element(X0)
| product2(X0,e_5,e_1)
| product2(X0,e_5,e_2)
| product2(X0,e_5,e_3)
| equalish(X0,e_5)
| equalish(X0,e_2) ) ).
cnf(u2629,negated_conjecture,
product2(e_4,e_2,e_1) ).
cnf(u3037,axiom,
( ~ group_element(X0)
| product1(X1,e_5,e_1)
| product1(X1,e_5,e_2)
| product1(X1,e_5,e_3)
| product1(X1,e_5,e_4)
| ~ group_element(X1)
| product1(X0,e_5,e_1)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| product1(X0,e_5,e_4)
| equalish(X0,X1) ) ).
cnf(u2610,negated_conjecture,
( ~ product2(e_3,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(u3143,axiom,
( ~ group_element(X0)
| product1(X0,e_1,e_2)
| product1(X0,e_1,e_3)
| product1(X0,e_1,e_4)
| product1(X0,e_1,e_1)
| product1(X0,e_3,e_1)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_4) ) ).
cnf(u3081,negated_conjecture,
( ~ group_element(X0)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_3)
| product1(X0,e_4,e_4)
| product1(X0,e_4,e_1)
| equalish(e_3,X0) ) ).
cnf(u2323,negated_conjecture,
product2(e_1,e_3,e_4) ).
cnf(u2567,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_2)
| product2(e_1,X0,e_1)
| product2(e_1,X0,e_2)
| product2(e_1,X0,e_3)
| product2(e_1,X0,e_4) ) ).
cnf(u307,axiom,
( ~ group_element(X0)
| equalish(X1,X2)
| ~ group_element(X2)
| product2(X0,X2,e_1)
| product2(X0,X2,e_2)
| product2(X0,X2,e_3)
| product2(X0,X2,e_4)
| ~ product2(X0,X1,e_5) ) ).
cnf(u3115,axiom,
( ~ group_element(X0)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_3)
| product1(X0,e_4,e_4)
| product1(X0,e_4,e_1)
| product1(X0,e_1,e_1)
| product1(X0,e_1,e_2)
| product1(X0,e_1,e_3)
| product1(X0,e_1,e_4) ) ).
cnf(u2325,negated_conjecture,
( ~ product2(e_1,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u2680,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product1(e_1,X1,e_1)
| product1(e_1,X1,e_2)
| product1(e_1,X1,e_3)
| product1(e_1,X1,e_4)
| ~ product1(e_1,X1,X0) ) ).
cnf(u2989,negated_conjecture,
( ~ group_element(X0)
| product1(e_5,X0,e_4)
| product1(e_5,X0,e_3)
| product1(e_5,X0,e_1)
| product2(e_5,e_3,X0)
| product1(e_5,X0,e_2)
| product1(X0,e_3,e_1)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_4) ) ).
cnf(u2810,axiom,
( ~ group_element(X0)
| product2(e_5,X0,e_1)
| product2(e_5,X0,e_2)
| product2(e_5,X0,e_3)
| product2(e_5,X0,e_4)
| equalish(e_5,X0) ) ).
cnf(u3095,negated_conjecture,
( ~ group_element(X0)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_3)
| product1(X0,e_2,e_4)
| product1(X0,e_2,e_1)
| equalish(e_4,X0) ) ).
cnf(u1555,negated_conjecture,
( ~ product2(e_5,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u2636,negated_conjecture,
product2(e_1,e_5,e_2) ).
cnf(u2299,negated_conjecture,
~ product1(e_5,e_2,e_5) ).
cnf(u305,axiom,
( ~ product2(X0,X1,X0)
| equalish(X1,X0) ) ).
cnf(u2883,axiom,
( ~ group_element(X1)
| product2(X0,e_5,e_3)
| equalish(X0,e_5)
| ~ group_element(X0)
| product2(X0,e_5,e_1)
| equalish(X1,X0)
| product2(X1,e_5,e_1)
| product2(X1,e_5,e_2)
| product2(X1,e_5,e_3)
| equalish(X1,e_5)
| product2(X0,e_5,e_2) ) ).
cnf(u1866,negated_conjecture,
( ~ product1(e_4,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u325,axiom,
( ~ product2(X1,e_5,e_4)
| product2(X0,e_5,e_2)
| product2(X0,e_5,e_3)
| equalish(X0,e_5)
| ~ group_element(X0)
| product2(X0,e_5,e_1)
| equalish(X1,X0) ) ).
cnf(u3103,axiom,
( ~ group_element(X0)
| product1(X1,e_3,e_1)
| product1(X1,e_3,e_2)
| product1(X1,e_3,e_3)
| product1(X1,e_3,e_4)
| ~ group_element(X1)
| equalish(X0,e_3)
| product1(X1,X0,e_1)
| product1(X1,X0,e_2)
| product1(X1,X0,e_3)
| product1(X1,X0,e_4) ) ).
cnf(u2282,negated_conjecture,
( ~ product2(e_2,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u2667,negated_conjecture,
( ~ group_element(X1)
| ~ product2(X0,X1,e_5)
| equalish(X0,e_5)
| product1(e_5,X1,e_1)
| product1(e_5,X1,e_2)
| product1(e_5,X1,e_3)
| product1(e_5,X1,e_4) ) ).
cnf(u2243,negated_conjecture,
( ~ product1(e_3,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u2255,negated_conjecture,
( ~ product1(X0,e_4,e_1)
| equalish(X0,e_2) ) ).
cnf(u183,axiom,
( ~ product2(X0,X0,X1)
| equalish(X1,X0) ) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(u2656,negated_conjecture,
( ~ group_element(X0)
| equalish(e_5,X0)
| product1(e_5,X0,e_1)
| product1(e_5,X0,e_2)
| product1(e_5,X0,e_3)
| product1(e_5,X0,e_4) ) ).
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(u2805,axiom,
( ~ product2(e_2,X0,e_5)
| ~ group_element(X1)
| product2(e_2,X1,e_1)
| product2(e_2,X1,e_2)
| product2(e_2,X1,e_3)
| product2(e_2,X1,e_4)
| equalish(X0,X1) ) ).
cnf(u354,negated_conjecture,
( ~ product1(X0,X1,e_3)
| product1(e_3,X0,e_2)
| product1(e_3,X0,e_3)
| product1(e_3,X0,e_4)
| ~ group_element(X0)
| product1(e_3,X0,e_1)
| product2(e_5,X1,X0) ) ).
cnf(u2257,negated_conjecture,
( ~ product1(e_4,X0,e_2)
| product2(e_1,X0,e_4) ) ).
cnf(element_5,axiom,
group_element(e_5) ).
cnf(u2197,axiom,
( ~ product1(X0,e_1,e_2)
| equalish(X0,e_5) ) ).
cnf(u2608,negated_conjecture,
( ~ product2(X0,e_5,e_1)
| equalish(X0,e_3) ) ).
cnf(u356,negated_conjecture,
( ~ product1(X0,X1,e_5)
| product1(e_5,X0,e_2)
| product1(e_5,X0,e_3)
| product1(e_5,X0,e_4)
| ~ group_element(X0)
| product1(e_5,X0,e_1)
| product2(e_5,X1,X0) ) ).
cnf(u2990,negated_conjecture,
( ~ group_element(X0)
| product1(e_5,X0,e_4)
| product1(e_5,X0,e_3)
| product1(e_5,X0,e_1)
| product2(e_5,e_4,X0)
| product1(e_5,X0,e_2)
| product1(X0,e_4,e_1)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_3)
| product1(X0,e_4,e_4) ) ).
cnf(u2344,axiom,
( ~ product1(e_5,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u2351,negated_conjecture,
( ~ product2(X0,e_4,e_5)
| equalish(X0,e_2) ) ).
cnf(u2818,axiom,
( ~ group_element(X1)
| product2(e_3,X0,e_1)
| product2(e_3,X0,e_2)
| product2(e_3,X0,e_3)
| product2(e_3,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| product2(e_3,X1,e_1)
| product2(e_3,X1,e_2)
| product2(e_3,X1,e_3)
| product2(e_3,X1,e_4) ) ).
cnf(u203,negated_conjecture,
~ product1(e_4,e_3,e_5) ).
cnf(u2338,negated_conjecture,
( ~ product1(e_1,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u2227,negated_conjecture,
product2(e_2,e_1,e_3) ).
cnf(u306,negated_conjecture,
( ~ product1(X0,X2,X0)
| equalish(X1,X2)
| ~ product2(X0,X1,X0) ) ).
cnf(u3046,negated_conjecture,
( ~ group_element(X0)
| product1(X0,e_1,e_2)
| product1(X0,e_1,e_3)
| product1(X0,e_1,e_4)
| product1(X0,e_1,e_1)
| equalish(e_2,X0) ) ).
cnf(u2806,axiom,
( ~ product2(e_3,X0,e_5)
| ~ group_element(X1)
| product2(e_3,X1,e_1)
| product2(e_3,X1,e_2)
| product2(e_3,X1,e_3)
| product2(e_3,X1,e_4)
| equalish(X0,X1) ) ).
cnf(u1923,negated_conjecture,
( ~ product1(e_3,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u2991,negated_conjecture,
( ~ group_element(X0)
| product1(e_5,X0,e_4)
| product1(e_5,X0,e_3)
| product1(e_5,X0,e_1)
| product2(e_5,e_5,X0)
| product1(e_5,X0,e_2)
| product1(X0,e_5,e_1)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| product1(X0,e_5,e_4) ) ).
cnf(u2334,negated_conjecture,
( ~ product1(e_1,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u2333,negated_conjecture,
( ~ product1(X0,e_4,e_2)
| equalish(X0,e_1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP124-9.005 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.39 % Computer : n008.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Sun Sep 27 09:24:09 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.43 Running first-order theorem proving
% 0.14/0.43 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
% 9.75/2.30 % (968577)Input is clausal, will run a generic CNF schedule.
% 9.75/2.30 % (968588)dis-21_1_sil=8000:lcm=predicate:random_seed=3046311938: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)
% 9.75/2.30 % (968586)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2197250433:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.75/2.30 % (968582)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=804687550:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.75/2.30 % (968585)lrs+10_1_sil=8000:sp=occurrence:random_seed=3243957025:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.75/2.30 % (968583)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3091548454:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.75/2.30 % (968584)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2816503467:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.75/2.30 % (968587)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3926643917:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.75/2.30 % (968588)Instruction limit reached!
% 9.75/2.30 % (968588)------------------------------
% 9.75/2.30 % (968588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.75/2.30 % (968588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.75/2.30 % (968588)CaDiCaL version: 2.1.3
% 9.75/2.30 % (968588)Termination reason: Instruction limit
% 9.75/2.30 % (968588)Termination phase: Saturation
% 9.75/2.30 % (968588)Time elapsed: 0.039 s
% 9.75/2.30 % (968588)Peak memory usage: 89 MB
% 9.75/2.30 % (968588)Instructions burned: 119 (million)
% 9.75/2.30 % (968585)Instruction limit reached!
% 9.75/2.30 % (968585)------------------------------
% 9.75/2.30 % (968585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.75/2.30 % (968585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.75/2.30 % (968585)CaDiCaL version: 2.1.3
% 9.75/2.30 % (968585)Termination reason: Instruction limit
% 9.75/2.30 % (968585)Termination phase: Saturation
% 9.75/2.30 % (968585)Time elapsed: 0.059 s
% 9.75/2.30 % (968585)Peak memory usage: 88 MB
% 9.75/2.30 % (968585)Instructions burned: 108 (million)
% 9.75/2.30 % (968586)Instruction limit reached!
% 9.75/2.30 % (968586)------------------------------
% 9.75/2.30 % (968586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.75/2.30 % (968586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.75/2.30 % (968586)CaDiCaL version: 2.1.3
% 9.75/2.30 % (968586)Termination reason: Instruction limit
% 9.75/2.30 % (968586)Termination phase: Saturation
% 9.75/2.30 % (968586)Time elapsed: 0.060 s
% 9.75/2.30 % (968586)Peak memory usage: 88 MB
% 9.75/2.30 % (968586)Instructions burned: 115 (million)
% 9.75/2.30 % (968587)Instruction limit reached!
% 9.75/2.30 % (968587)------------------------------
% 9.75/2.30 % (968587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.75/2.30 % (968587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.75/2.30 % (968587)CaDiCaL version: 2.1.3
% 9.75/2.30 % (968587)Termination reason: Instruction limit
% 9.75/2.30 % (968587)Termination phase: Saturation
% 9.75/2.30 % (968587)Time elapsed: 0.106 s
% 9.75/2.30 % (968587)Peak memory usage: 89 MB
% 9.75/2.30 % (968587)Instructions burned: 181 (million)
% 9.75/2.30 % (968596)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=12779363:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 9.75/2.30 % (968596)Instruction limit reached!
% 9.75/2.30 % (968596)------------------------------
% 9.75/2.30 % (968596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.75/2.30 % (968596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.75/2.30 % (968596)CaDiCaL version: 2.1.3
% 9.75/2.30 % (968596)Termination reason: Instruction limit
% 9.75/2.30 % (968596)Termination phase: Saturation
% 9.75/2.30 % (968596)Time elapsed: 0.046 s
% 9.75/2.30 % (968596)Peak memory usage: 89 MB
% 9.75/2.30 % (968596)Instructions burned: 144 (million)
% 9.75/2.30 % (968598)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=989716741:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 15.64/3.08 % (968597)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2999597109: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)
% 15.64/3.08 % (968597)Refutation not found, incomplete strategy
% 15.64/3.08 % (968597)------------------------------
% 15.64/3.08 % (968597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.08 % (968597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.08 % (968597)CaDiCaL version: 2.1.3
% 15.64/3.08 % (968597)Termination reason: Refutation not found, incomplete strategy
% 15.64/3.08 % (968597)Time elapsed: 0.002 s
% 15.64/3.08 % (968597)Peak memory usage: 87 MB
% 15.64/3.08 % (968597)Instructions burned: 1 (million)
% 15.64/3.08 % (968599)lrs+10_64_to=lpo:sil=8000:random_seed=4134419349:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 15.64/3.08 % (968601)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1296691071:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 15.64/3.08 % (968598)Instruction limit reached!
% 15.64/3.08 % (968598)------------------------------
% 15.64/3.08 % (968598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.08 % (968598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.08 % (968598)CaDiCaL version: 2.1.3
% 15.64/3.08 % (968598)Termination reason: Instruction limit
% 15.64/3.08 % (968598)Termination phase: Saturation
% 15.64/3.08 % (968598)Time elapsed: 0.121 s
% 15.64/3.08 % (968598)Peak memory usage: 88 MB
% 15.64/3.08 % (968598)Instructions burned: 220 (million)
% 15.64/3.08 % (968599)Instruction limit reached!
% 15.64/3.08 % (968599)------------------------------
% 15.64/3.08 % (968599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.08 % (968599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.08 % (968599)CaDiCaL version: 2.1.3
% 15.64/3.08 % (968599)Termination reason: Instruction limit
% 15.64/3.08 % (968599)Termination phase: Saturation
% 15.64/3.08 % (968599)Time elapsed: 0.071 s
% 15.64/3.08 % (968599)Peak memory usage: 88 MB
% 15.64/3.08 % (968599)Instructions burned: 127 (million)
% 15.64/3.08 % (968601)Instruction limit reached!
% 15.64/3.08 % (968601)------------------------------
% 15.64/3.08 % (968601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.08 % (968601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.08 % (968601)CaDiCaL version: 2.1.3
% 15.64/3.08 % (968601)Termination reason: Instruction limit
% 15.64/3.08 % (968601)Termination phase: Saturation
% 15.64/3.08 % (968601)Time elapsed: 0.065 s
% 15.64/3.08 % (968601)Peak memory usage: 89 MB
% 15.64/3.08 % (968601)Instructions burned: 197 (million)
% 15.64/3.08 % (968597)------------------------------
% 15.64/3.08 % (968597)------------------------------
% 15.64/3.08 % (968606)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2628352698:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 15.64/3.08 % (968607)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2579664839:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 15.64/3.08 % (968608)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=3309569620:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 15.64/3.08 % (968608)Refutation not found, incomplete strategy
% 15.64/3.08 % (968608)------------------------------
% 15.64/3.08 % (968608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.08 % (968608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.08 % (968608)CaDiCaL version: 2.1.3
% 15.64/3.08 % (968608)Termination reason: Refutation not found, incomplete strategy
% 15.64/3.08 % (968608)Time elapsed: 0.003 s
% 15.64/3.08 % (968608)Peak memory usage: 87 MB
% 15.64/3.08 % (968608)Instructions burned: 11 (million)
% 15.64/3.08 % (968606)Instruction limit reached!
% 15.64/3.08 % (968606)------------------------------
% 15.64/3.08 % (968606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.08 % (968606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.08 % (968606)CaDiCaL version: 2.1.3
% 15.64/3.08 % (968606)Termination reason: Instruction limit
% 23.45/4.17 % (968606)Termination phase: Saturation
% 23.45/4.17 % (968606)Time elapsed: 0.087 s
% 23.45/4.17 % (968606)Peak memory usage: 89 MB
% 23.45/4.17 % (968606)Instructions burned: 159 (million)
% 23.45/4.17 % (968609)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1732688610:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 23.45/4.17 % (968583)Refutation not found, incomplete strategy
% 23.45/4.17 % (968583)------------------------------
% 23.45/4.17 % (968583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.45/4.17 % (968583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.45/4.17 % (968583)CaDiCaL version: 2.1.3
% 23.45/4.17 % (968583)Termination reason: Refutation not found, incomplete strategy
% 23.45/4.17 % (968583)Time elapsed: 0.645 s
% 23.45/4.17 % (968583)Peak memory usage: 126 MB
% 23.45/4.17 % (968583)Instructions burned: 945 (million)
% 23.45/4.17 % (968608)------------------------------
% 23.45/4.17 % (968608)------------------------------
% 23.45/4.17 % (968609)Instruction limit reached!
% 23.45/4.17 % (968609)------------------------------
% 23.45/4.17 % (968609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.45/4.17 % (968609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.45/4.17 % (968609)CaDiCaL version: 2.1.3
% 23.45/4.17 % (968609)Termination reason: Instruction limit
% 23.45/4.17 % (968609)Termination phase: Saturation
% 23.45/4.17 % (968609)Time elapsed: 0.067 s
% 23.45/4.17 % (968609)Peak memory usage: 88 MB
% 23.45/4.17 % (968609)Instructions burned: 107 (million)
% 23.45/4.17 % (968613)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1610698827:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 23.45/4.17 % (968615)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=872556668:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 23.45/4.17 % (968613)Instruction limit reached!
% 23.45/4.17 % (968613)------------------------------
% 23.45/4.17 % (968613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.45/4.17 % (968613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.45/4.17 % (968613)CaDiCaL version: 2.1.3
% 23.45/4.17 % (968613)Termination reason: Instruction limit
% 23.45/4.17 % (968613)Termination phase: Saturation
% 23.45/4.17 % (968613)Time elapsed: 0.121 s
% 23.45/4.17 % (968613)Peak memory usage: 88 MB
% 23.45/4.17 % (968613)Instructions burned: 243 (million)
% 23.45/4.17 % (968616)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1593319234:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 23.45/4.17 % (968583)------------------------------
% 23.45/4.17 % (968583)------------------------------
% 23.45/4.17 % (968616)Instruction limit reached!
% 23.45/4.17 % (968616)------------------------------
% 23.45/4.17 % (968616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.45/4.17 % (968616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.45/4.17 % (968616)CaDiCaL version: 2.1.3
% 23.45/4.17 % (968616)Termination reason: Instruction limit
% 23.45/4.17 % (968616)Termination phase: Saturation
% 23.45/4.17 % (968616)Time elapsed: 0.088 s
% 23.45/4.17 % (968616)Peak memory usage: 89 MB
% 23.45/4.17 % (968616)Instructions burned: 135 (million)
% 23.45/4.17 % (968620)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=903040146:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 23.45/4.17 % (968621)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=604356528:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 23.45/4.17 % (968622)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3368739012:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 23.45/4.17 % (968621)Instruction limit reached!
% 23.45/4.17 % (968621)------------------------------
% 23.45/4.17 % (968621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.45/4.17 % (968621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.45/4.17 % (968621)CaDiCaL version: 2.1.3
% 23.45/4.17 % (968621)Termination reason: Instruction limit
% 23.45/4.17 % (968621)Termination phase: Saturation
% 23.45/4.17 % (968621)Time elapsed: 0.115 s
% 23.45/4.17 % (968621)Peak memory usage: 89 MB
% 23.45/4.17 % (968621)Instructions burned: 192 (million)
% 23.45/4.17 % (968622)Instruction limit reached!
% 33.32/5.64 % (968622)------------------------------
% 33.32/5.64 % (968622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.32/5.64 % (968622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.32/5.64 % (968622)CaDiCaL version: 2.1.3
% 33.32/5.64 % (968622)Termination reason: Instruction limit
% 33.32/5.64 % (968622)Termination phase: Saturation
% 33.32/5.64 % (968622)Time elapsed: 0.150 s
% 33.32/5.64 % (968622)Peak memory usage: 90 MB
% 33.32/5.64 % (968622)Instructions burned: 265 (million)
% 33.32/5.64 % (968620)Instruction limit reached!
% 33.32/5.64 % (968620)------------------------------
% 33.32/5.64 % (968620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.32/5.64 % (968620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.32/5.64 % (968620)CaDiCaL version: 2.1.3
% 33.32/5.64 % (968620)Termination reason: Instruction limit
% 33.32/5.64 % (968620)Termination phase: Saturation
% 33.32/5.64 % (968620)Time elapsed: 0.259 s
% 33.32/5.64 % (968620)Peak memory usage: 90 MB
% 33.32/5.64 % (968620)Instructions burned: 500 (million)
% 33.32/5.64 % (968626)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2335761520:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 33.32/5.64 % (968627)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=4224406062:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi)
% 33.32/5.64 % (968626)Instruction limit reached!
% 33.32/5.64 % (968626)------------------------------
% 33.32/5.64 % (968626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.32/5.64 % (968626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.32/5.64 % (968626)CaDiCaL version: 2.1.3
% 33.32/5.64 % (968626)Termination reason: Instruction limit
% 33.32/5.64 % (968626)Termination phase: Saturation
% 33.32/5.64 % (968626)Time elapsed: 0.085 s
% 33.32/5.64 % (968626)Peak memory usage: 89 MB
% 33.32/5.64 % (968626)Instructions burned: 156 (million)
% 33.32/5.64 % (968628)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=995003418:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi)
% 33.32/5.64 % (968631)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2610434429:i=180:bd=preordered:av=off_2984 on theBenchmark for (2984ds/180Mi)
% 33.32/5.64 % (968631)Instruction limit reached!
% 33.32/5.64 % (968631)------------------------------
% 33.32/5.64 % (968631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.32/5.64 % (968631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.32/5.64 % (968631)CaDiCaL version: 2.1.3
% 33.32/5.64 % (968631)Termination reason: Instruction limit
% 33.32/5.64 % (968631)Termination phase: Saturation
% 33.32/5.64 % (968631)Time elapsed: 0.088 s
% 33.32/5.64 % (968631)Peak memory usage: 87 MB
% 33.32/5.64 % (968631)Instructions burned: 182 (million)
% 33.32/5.64 % (968628)Instruction limit reached!
% 33.32/5.64 % (968628)------------------------------
% 33.32/5.64 % (968628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.32/5.64 % (968628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.32/5.64 % (968628)CaDiCaL version: 2.1.3
% 33.32/5.64 % (968628)Termination reason: Instruction limit
% 33.32/5.64 % (968628)Termination phase: Saturation
% 33.32/5.64 % (968628)Time elapsed: 0.252 s
% 33.32/5.64 % (968628)Peak memory usage: 88 MB
% 33.32/5.64 % (968628)Instructions burned: 537 (million)
% 33.32/5.64 % (968634)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=126985116:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2981 on theBenchmark for (2981ds/10307Mi)
% 33.32/5.64 % (968635)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=1275559177:i=412:gtgl=4:gtg=exists_all_2981 on theBenchmark for (2981ds/412Mi)
% 33.32/5.64 % (968635)Instruction limit reached!
% 33.32/5.64 % (968635)------------------------------
% 33.32/5.64 % (968635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.32/5.64 % (968635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.32/5.64 % (968635)CaDiCaL version: 2.1.3
% 33.32/5.64 % (968635)Termination reason: Instruction limit
% 33.32/5.64 % (968635)Termination phase: Saturation
% 46.33/7.46 % (968635)Time elapsed: 0.197 s
% 46.33/7.46 % (968635)Peak memory usage: 90 MB
% 46.33/7.46 % (968635)Instructions burned: 414 (million)
% 46.33/7.46 % (968638)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=2246316829:s2pl=no:i=8478:s2at=4:nm=6_2978 on theBenchmark for (2978ds/8478Mi)
% 46.33/7.46 % (968615)Instruction limit reached!
% 46.33/7.46 % (968615)------------------------------
% 46.33/7.46 % (968615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968615)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968615)Termination reason: Instruction limit
% 46.33/7.46 % (968615)Termination phase: Saturation
% 46.33/7.46 % (968615)Time elapsed: 1.482 s
% 46.33/7.46 % (968615)Peak memory usage: 135 MB
% 46.33/7.46 % (968615)Instructions burned: 5210 (million)
% 46.33/7.46 % (968640)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=1433719982: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)
% 46.33/7.46 % (968640)Instruction limit reached!
% 46.33/7.46 % (968640)------------------------------
% 46.33/7.46 % (968640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968640)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968640)Termination reason: Instruction limit
% 46.33/7.46 % (968640)Termination phase: Saturation
% 46.33/7.46 % (968640)Time elapsed: 0.090 s
% 46.33/7.46 % (968640)Peak memory usage: 90 MB
% 46.33/7.46 % (968640)Instructions burned: 304 (million)
% 46.33/7.46 % (968607)Instruction limit reached!
% 46.33/7.46 % (968607)------------------------------
% 46.33/7.46 % (968607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968607)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968607)Termination reason: Instruction limit
% 46.33/7.46 % (968607)Termination phase: Saturation
% 46.33/7.46 % (968607)Time elapsed: 2.120 s
% 46.33/7.46 % (968607)Peak memory usage: 139 MB
% 46.33/7.46 % (968607)Instructions burned: 3395 (million)
% 46.33/7.46 % (968642)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2964599821:st=4:i=720:sd=3:fsr=off:ss=axioms_2973 on theBenchmark for (2973ds/720Mi)
% 46.33/7.46 % (968642)Refutation not found, incomplete strategy
% 46.33/7.46 % (968642)------------------------------
% 46.33/7.46 % (968642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968642)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968642)Termination reason: Refutation not found, incomplete strategy
% 46.33/7.46 % (968642)Time elapsed: 0.001 s
% 46.33/7.46 % (968642)Peak memory usage: 88 MB
% 46.33/7.46 % (968642)Instructions burned: 1 (million)
% 46.33/7.46 % (968642)------------------------------
% 46.33/7.46 % (968642)------------------------------
% 46.33/7.46 % (968643)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=993087851:i=598:bs=on:bd=preordered:av=off:ss=axioms_2972 on theBenchmark for (2972ds/598Mi)
% 46.33/7.46 % (968638)Refutation not found, incomplete strategy
% 46.33/7.46 % (968638)------------------------------
% 46.33/7.46 % (968638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968638)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968638)Termination reason: Refutation not found, incomplete strategy
% 46.33/7.46 % (968638)Time elapsed: 0.622 s
% 46.33/7.46 % (968638)Peak memory usage: 128 MB
% 46.33/7.46 % (968638)Instructions burned: 945 (million)
% 46.33/7.46 % (968645)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=921343120:i=2989:sd=3:ss=axioms:sgt=60_2970 on theBenchmark for (2970ds/2989Mi)
% 46.33/7.46 % (968638)------------------------------
% 46.33/7.46 % (968638)------------------------------
% 46.33/7.46 % (968643)Instruction limit reached!
% 46.33/7.46 % (968643)------------------------------
% 46.33/7.46 % (968643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968643)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968643)Termination reason: Instruction limit
% 46.33/7.46 % (968643)Termination phase: Saturation
% 46.33/7.46 % (968643)Time elapsed: 0.322 s
% 46.33/7.46 % (968643)Peak memory usage: 90 MB
% 46.33/7.46 % (968643)Instructions burned: 599 (million)
% 46.33/7.46 % (968648)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=1350354839:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2967 on theBenchmark for (2967ds/1997Mi)
% 46.33/7.46 % (968649)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=4049090620:i=2088:bd=preordered:av=off_2967 on theBenchmark for (2967ds/2088Mi)
% 46.33/7.46 % (968627)Instruction limit reached!
% 46.33/7.46 % (968627)------------------------------
% 46.33/7.46 % (968627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968627)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968627)Termination reason: Instruction limit
% 46.33/7.46 % (968627)Termination phase: Saturation
% 46.33/7.46 % (968627)Time elapsed: 2.057 s
% 46.33/7.46 % (968627)Peak memory usage: 137 MB
% 46.33/7.46 % (968627)Instructions burned: 3257 (million)
% 46.33/7.46 % (968652)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=743044486:i=1098:nicw=on_2963 on theBenchmark for (2963ds/1098Mi)
% 46.33/7.46 % (968645)Instruction limit reached!
% 46.33/7.46 % (968645)------------------------------
% 46.33/7.46 % (968645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968645)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968645)Termination reason: Instruction limit
% 46.33/7.46 % (968645)Termination phase: Saturation
% 46.33/7.46 % (968645)Time elapsed: 1.050 s
% 46.33/7.46 % (968645)Peak memory usage: 141 MB
% 46.33/7.46 % (968645)Instructions burned: 2992 (million)
% 46.33/7.46 % (968654)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2236596586:i=433:bd=preordered_2958 on theBenchmark for (2958ds/433Mi)
% 46.33/7.46 % (968652)Instruction limit reached!
% 46.33/7.46 % (968652)------------------------------
% 46.33/7.46 % (968652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968652)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968652)Termination reason: Instruction limit
% 46.33/7.46 % (968652)Termination phase: Saturation
% 46.33/7.46 % (968652)Time elapsed: 0.561 s
% 46.33/7.46 % (968652)Peak memory usage: 94 MB
% 46.33/7.46 % (968652)Instructions burned: 1098 (million)
% 46.33/7.46 % (968654)Refutation not found, incomplete strategy
% 46.33/7.46 % (968654)------------------------------
% 46.33/7.46 % (968654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968654)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968654)Termination reason: Refutation not found, incomplete strategy
% 46.33/7.46 % (968654)Time elapsed: 0.108 s
% 46.33/7.46 % (968654)Peak memory usage: 90 MB
% 46.33/7.46 % (968654)Instructions burned: 369 (million)
% 46.33/7.46 % (968656)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1859751693:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2956 on theBenchmark for (2956ds/2942Mi)
% 46.33/7.46 % (968654)------------------------------
% 46.33/7.46 % (968654)------------------------------
% 46.33/7.46 % (968658)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=299276245:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2954 on theBenchmark for (2954ds/6922Mi)
% 46.33/7.46 % (968648)Instruction limit reached!
% 46.33/7.46 % (968648)------------------------------
% 46.33/7.46 % (968648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968648)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968648)Termination reason: Instruction limit
% 46.33/7.46 % (968648)Termination phase: Saturation
% 46.33/7.46 % (968648)Time elapsed: 1.378 s
% 46.33/7.46 % (968648)Peak memory usage: 134 MB
% 46.33/7.46 % (968648)Instructions burned: 1998 (million)
% 46.33/7.46 % (968649)Instruction limit reached!
% 46.33/7.46 % (968649)------------------------------
% 46.33/7.46 % (968649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968649)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968649)Termination reason: Instruction limit
% 46.33/7.46 % (968649)Termination phase: Saturation
% 46.33/7.46 % (968649)Time elapsed: 1.338 s
% 46.33/7.46 % (968649)Peak memory usage: 134 MB
% 46.33/7.46 % (968649)Instructions burned: 2088 (million)
% 46.33/7.46 % (968660)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=3804384388:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2952 on theBenchmark for (2952ds/596Mi)
% 46.33/7.46 % (968660)Refutation not found, incomplete strategy
% 46.33/7.46 % (968660)------------------------------
% 46.33/7.46 % (968660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968660)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968660)Termination reason: Refutation not found, incomplete strategy
% 46.33/7.46 % (968660)Time elapsed: 0.008 s
% 46.33/7.46 % (968660)Peak memory usage: 88 MB
% 46.33/7.46 % (968660)Instructions burned: 15 (million)
% 46.33/7.46 % (968661)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=2303398471:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2952 on theBenchmark for (2952ds/4123Mi)
% 46.33/7.46 % (968658)Refutation not found, incomplete strategy
% 46.33/7.46 % (968658)------------------------------
% 46.33/7.46 % (968658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968658)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968658)Termination reason: Refutation not found, incomplete strategy
% 46.33/7.46 % (968658)Time elapsed: 0.337 s
% 46.33/7.46 % (968658)Peak memory usage: 128 MB
% 46.33/7.46 % (968658)Instructions burned: 946 (million)
% 46.33/7.46 % (968660)------------------------------
% 46.33/7.46 % (968660)------------------------------
% 46.33/7.46 % (968658)------------------------------
% 46.33/7.46 % (968658)------------------------------
% 46.33/7.46 % (968665)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=697545985:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2948 on theBenchmark for (2948ds/1670Mi)
% 46.33/7.46 % (968664)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=405960982:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2948 on theBenchmark for (2948ds/16411Mi)
% 46.33/7.46 % (968665)Instruction limit reached!
% 46.33/7.46 % (968665)------------------------------
% 46.33/7.46 % (968665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968665)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968665)Termination reason: Instruction limit
% 46.33/7.46 % (968665)Termination phase: Saturation
% 46.33/7.46 % (968665)Time elapsed: 0.664 s
% 46.33/7.46 % (968665)Peak memory usage: 133 MB
% 46.33/7.46 % (968665)Instructions burned: 1672 (million)
% 46.33/7.46 % (968668)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=4125475953:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2940 on theBenchmark for (2940ds/1722Mi)
% 46.33/7.46 % (968664)First to succeed.
% 46.33/7.46 % (968664)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-968577"
% 46.33/7.46 % (968656)Instruction limit reached!
% 46.33/7.46 % (968656)------------------------------
% 46.33/7.46 % (968656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.33/7.46 % (968656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.33/7.46 % (968656)CaDiCaL version: 2.1.3
% 46.33/7.46 % (968656)Termination reason: Instruction limit
% 46.33/7.46 % (968656)Termination phase: Saturation
% 46.33/7.46 % (968656)Time elapsed: 1.940 s
% 46.33/7.46 % (968656)Peak memory usage: 138 MB
% 46.33/7.46 % (968656)Instructions burned: 2942 (million)
% 46.33/7.46 % SZS status Satisfiable for theBenchmark
% 46.33/7.46 % SZS output start Saturation.
% See solution above
% 46.96/7.66 % SZS output start Definitions and Model Updates.
% 46.96/7.66 for all inputs,
% 46.96/7.66 define product(X0,X1,X2) := $true
% 46.96/7.66 % SZS output end Definitions and Model Updates.
% 46.96/7.66 % (968664)------------------------------
% 46.96/7.66 % (968664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.96/7.66 % (968664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.96/7.66 % (968664)CaDiCaL version: 2.1.3
% 46.96/7.66 % (968664)Termination reason: Satisfiable
% 46.96/7.66 % (968664)Time elapsed: 0.979 s
% 46.96/7.66 % (968664)Peak memory usage: 131 MB
% 46.96/7.66 % (968664)Instructions burned: 1344 (million)
% 46.96/7.66 % (968664)------------------------------
% 46.96/7.66 % (968664)------------------------------
% 46.96/7.66 % (968577)Success in time 6.58 s
% 46.96/7.66 % Vampire exiting
%------------------------------------------------------------------------------