%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP131-1.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:13:01 AM UTC 2026
% Result : Satisfiable 68.15s 10.88s
% Output : Saturation 69.90s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u53,axiom,
equalish(e_5,e_5) ).
cnf(u73,axiom,
~ product(e_5,e_1,e_4) ).
cnf(u77,axiom,
~ product(e_5,e_1,e_3) ).
cnf(u81,axiom,
~ product(e_5,e_1,e_2) ).
cnf(u86,axiom,
product(e_5,e_1,e_1) ).
cnf(u93,axiom,
~ product(e_4,e_1,e_4) ).
cnf(u97,axiom,
~ product(e_4,e_1,e_3) ).
cnf(u102,axiom,
product(e_4,e_1,e_2) ).
cnf(u105,axiom,
~ product(e_4,e_1,e_1) ).
cnf(u113,axiom,
~ product(e_3,e_1,e_4) ).
cnf(u117,axiom,
~ product(e_3,e_1,e_3) ).
cnf(u121,axiom,
~ product(e_3,e_1,e_2) ).
cnf(u125,axiom,
~ product(e_3,e_1,e_1) ).
cnf(u129,axiom,
( ~ group_element(X0)
| equalish(e_3,X0)
| product(X0,e_1,e_1)
| product(X0,e_1,e_4)
| product(X0,e_1,e_3)
| product(X0,e_1,e_2) ) ).
cnf(u133,axiom,
~ product(e_2,e_1,e_4) ).
cnf(u138,axiom,
product(e_2,e_1,e_3) ).
cnf(u141,axiom,
~ product(e_2,e_1,e_2) ).
cnf(u145,axiom,
~ product(e_2,e_1,e_1) ).
cnf(u154,axiom,
product(e_1,e_1,e_4) ).
cnf(u157,axiom,
~ product(e_1,e_1,e_3) ).
cnf(u161,axiom,
~ product(e_1,e_1,e_2) ).
cnf(u165,axiom,
~ product(e_1,e_1,e_1) ).
cnf(u345,negated_conjecture,
~ product(e_5,e_5,e_4) ).
cnf(u350,negated_conjecture,
product(e_5,e_5,e_3) ).
cnf(u353,negated_conjecture,
~ product(e_5,e_5,e_2) ).
cnf(u357,negated_conjecture,
~ product(e_5,e_5,e_1) ).
cnf(u363,negated_conjecture,
product(e_5,e_4,e_4) ).
cnf(u366,negated_conjecture,
~ product(e_5,e_4,e_3) ).
cnf(u370,negated_conjecture,
~ product(e_5,e_4,e_2) ).
cnf(u374,negated_conjecture,
~ product(e_5,e_4,e_1) ).
cnf(u379,negated_conjecture,
~ product(e_5,e_3,e_4) ).
cnf(u383,negated_conjecture,
~ product(e_5,e_3,e_3) ).
cnf(u388,negated_conjecture,
product(e_5,e_3,e_2) ).
cnf(u391,negated_conjecture,
~ product(e_5,e_3,e_1) ).
cnf(u396,negated_conjecture,
~ product(e_5,e_2,e_4) ).
cnf(u400,negated_conjecture,
~ product(e_5,e_2,e_3) ).
cnf(u404,negated_conjecture,
~ product(e_5,e_2,e_2) ).
cnf(u408,negated_conjecture,
~ product(e_5,e_2,e_1) ).
cnf(u521,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_4)
| product(e_5,X0,e_3)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1)
| product(e_3,X0,e_4)
| product(e_3,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1) ) ).
cnf(u609,negated_conjecture,
product(e_2,e_5,e_4) ).
cnf(u612,negated_conjecture,
~ product(e_2,e_5,e_3) ).
cnf(u616,negated_conjecture,
~ product(e_2,e_5,e_2) ).
cnf(u620,negated_conjecture,
~ product(e_2,e_5,e_1) ).
cnf(u625,negated_conjecture,
~ product(e_2,e_4,e_4) ).
cnf(u629,negated_conjecture,
~ product(e_2,e_4,e_3) ).
cnf(u633,negated_conjecture,
~ product(e_2,e_4,e_2) ).
cnf(u637,negated_conjecture,
~ product(e_2,e_4,e_1) ).
cnf(u642,negated_conjecture,
~ product(e_2,e_3,e_4) ).
cnf(u646,negated_conjecture,
~ product(e_2,e_3,e_3) ).
cnf(u650,negated_conjecture,
~ product(e_2,e_3,e_2) ).
cnf(u655,negated_conjecture,
product(e_2,e_3,e_1) ).
cnf(u659,negated_conjecture,
~ product(e_2,e_2,e_4) ).
cnf(u663,negated_conjecture,
~ product(e_2,e_2,e_3) ).
cnf(u668,negated_conjecture,
product(e_2,e_2,e_2) ).
cnf(u671,negated_conjecture,
~ product(e_2,e_2,e_1) ).
cnf(u791,negated_conjecture,
~ product(e_4,e_4,e_4) ).
cnf(u796,negated_conjecture,
product(e_4,e_4,e_3) ).
cnf(u799,negated_conjecture,
~ product(e_4,e_4,e_2) ).
cnf(u803,negated_conjecture,
~ product(e_4,e_4,e_1) ).
cnf(u851,negated_conjecture,
~ product(e_3,e_4,e_4) ).
cnf(u855,negated_conjecture,
~ product(e_3,e_4,e_3) ).
cnf(u859,negated_conjecture,
~ product(e_3,e_4,e_2) ).
cnf(u864,negated_conjecture,
product(e_3,e_4,e_1) ).
cnf(u939,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_4)
| product(e_5,X0,e_3)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1)
| product(e_4,X0,e_4)
| product(e_4,X0,e_3)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1) ) ).
cnf(u994,negated_conjecture,
~ product(e_1,e_4,e_4) ).
cnf(u998,negated_conjecture,
~ product(e_1,e_4,e_3) ).
cnf(u1003,negated_conjecture,
product(e_1,e_4,e_2) ).
cnf(u1006,negated_conjecture,
~ product(e_1,e_4,e_1) ).
cnf(u1092,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_4)
| product(e_5,X0,e_3)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1)
| product(e_1,X0,e_4)
| product(e_1,X0,e_3)
| product(e_1,X0,e_2)
| product(e_1,X0,e_1) ) ).
cnf(u1161,negated_conjecture,
~ product(e_3,e_5,e_1) ).
cnf(u1166,negated_conjecture,
product(e_3,e_5,e_2) ).
cnf(u1169,negated_conjecture,
~ product(e_3,e_5,e_3) ).
cnf(u1173,negated_conjecture,
~ product(e_3,e_5,e_4) ).
cnf(u1178,negated_conjecture,
~ product(e_3,e_2,e_1) ).
cnf(u1182,negated_conjecture,
~ product(e_3,e_2,e_2) ).
cnf(u1187,negated_conjecture,
product(e_3,e_2,e_3) ).
cnf(u1190,negated_conjecture,
~ product(e_3,e_2,e_4) ).
cnf(u1363,negated_conjecture,
~ product(e_4,e_3,e_4) ).
cnf(u1367,negated_conjecture,
~ product(e_4,e_3,e_3) ).
cnf(u1371,negated_conjecture,
~ product(e_4,e_3,e_2) ).
cnf(u1375,negated_conjecture,
~ product(e_4,e_3,e_1) ).
cnf(u1391,negated_conjecture,
~ product(e_1,e_3,e_4) ).
cnf(u1396,negated_conjecture,
product(e_1,e_3,e_3) ).
cnf(u1399,negated_conjecture,
~ product(e_1,e_3,e_2) ).
cnf(u1403,negated_conjecture,
~ product(e_1,e_3,e_1) ).
cnf(u1470,negated_conjecture,
product(e_3,e_3,e_4) ).
cnf(u1473,negated_conjecture,
~ product(e_3,e_3,e_3) ).
cnf(u1477,negated_conjecture,
~ product(e_3,e_3,e_2) ).
cnf(u1481,negated_conjecture,
~ product(e_3,e_3,e_1) ).
cnf(u1498,negated_conjecture,
~ product(e_1,e_2,e_4) ).
cnf(u1502,negated_conjecture,
~ product(e_1,e_2,e_3) ).
cnf(u1506,negated_conjecture,
~ product(e_1,e_2,e_2) ).
cnf(u1511,negated_conjecture,
product(e_1,e_2,e_1) ).
cnf(u1918,negated_conjecture,
product(e_4,e_5,e_1) ).
cnf(u1921,negated_conjecture,
~ product(e_4,e_5,e_2) ).
cnf(u1925,negated_conjecture,
~ product(e_4,e_5,e_3) ).
cnf(u1929,negated_conjecture,
~ product(e_4,e_5,e_4) ).
cnf(u1934,negated_conjecture,
~ product(e_4,e_2,e_1) ).
cnf(u1938,negated_conjecture,
~ product(e_4,e_2,e_2) ).
cnf(u1942,negated_conjecture,
~ product(e_4,e_2,e_3) ).
cnf(u1947,negated_conjecture,
product(e_4,e_2,e_4) ).
cnf(u2128,negated_conjecture,
( ~ group_element(X0)
| equalish(e_4,X0)
| product(X0,e_3,e_1)
| product(X0,e_3,e_4)
| product(X0,e_3,e_3)
| product(X0,e_3,e_2) ) ).
cnf(u2881,axiom,
~ product(e_1,e_5,e_4) ).
cnf(u2885,axiom,
~ product(e_1,e_5,e_3) ).
cnf(u2889,axiom,
~ product(e_1,e_5,e_2) ).
cnf(u2893,axiom,
~ product(e_1,e_5,e_1) ).
cnf(u2897,axiom,
( ~ group_element(X0)
| equalish(e_1,X0)
| product(X0,e_5,e_1)
| product(X0,e_5,e_4)
| product(X0,e_5,e_3)
| product(X0,e_5,e_2) ) ).
cnf(u7265,negated_conjecture,
( ~ group_element(X0)
| equalish(e_5,X0)
| product(X0,e_2,e_1)
| product(X0,e_2,e_4)
| product(X0,e_2,e_3)
| product(X0,e_2,e_2) ) ).
cnf(u7269,negated_conjecture,
( ~ group_element(X2)
| equalish(X0,e_2)
| product(X2,X0,e_4)
| product(X2,X0,e_3)
| product(X2,X0,e_2)
| product(X2,X0,e_1)
| ~ group_element(X0)
| ~ group_element(X1)
| product(X1,e_2,e_4)
| product(X1,e_2,e_3)
| product(X1,e_2,e_2)
| product(X1,e_2,e_1)
| ~ product(X1,X0,X2) ) ).
cnf(u11223,negated_conjecture,
( ~ product(e_5,X0,e_2)
| product(e_2,X0,e_4)
| equalish(X0,e_2)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3) ) ).
cnf(u18850,negated_conjecture,
( ~ product(e_2,X0,e_4)
| product(e_4,X0,e_4)
| equalish(X0,e_2)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3) ) ).
cnf(u18854,negated_conjecture,
( ~ product(e_2,X0,e_4)
| product(e_4,X0,e_4)
| equalish(X0,e_2)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_3) ) ).
cnf(u57281,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X1,e_3) ) ).
cnf(u57576,negated_conjecture,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_1)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ) ).
cnf(u32,axiom,
( ~ product(X0,X1,X2)
| 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)
| ~ group_element(X0) ) ).
cnf(u52146,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| product(X0,e_4,e_1)
| equalish(e_2,X0) ) ).
cnf(u56100,negated_conjecture,
( ~ product(e_5,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(u57008,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X1,e_1) ) ).
cnf(u63,axiom,
( ~ group_element(X0)
| product(X1,e_3,e_1)
| product(X1,e_3,e_2)
| product(X1,e_3,e_3)
| product(X1,e_3,e_4)
| ~ group_element(X1)
| 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,X1) ) ).
cnf(u44,axiom,
( ~ group_element(X2)
| equalish(X0,X1)
| product(X1,X2,e_1)
| product(X1,X2,e_2)
| product(X1,X2,e_3)
| product(X1,X2,e_4)
| ~ group_element(X1)
| product(X0,X2,e_1)
| product(X0,X2,e_2)
| product(X0,X2,e_3)
| product(X0,X2,e_4)
| ~ group_element(X0) ) ).
cnf(product_left_cancellation,axiom,
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u57295,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X1,e_4) ) ).
cnf(u57219,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4) ).
cnf(u9048,negated_conjecture,
( ~ group_element(X1)
| product(e_4,X0,e_4)
| product(e_4,X0,e_3)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_2)
| product(X1,e_2,e_3)
| product(X1,e_2,e_2)
| product(X1,e_2,e_1)
| ~ product(X1,X0,e_4) ) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(u56103,negated_conjecture,
( ~ product(e_3,e_5,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_3) ) ).
cnf(u57142,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X1,e_4) ) ).
cnf(u53685,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_4)
| equalish(X1,e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u57362,negated_conjecture,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_4)
| ~ group_element(X0)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(u57632,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_4)
| equalish(X0,e_1)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_4) ) ).
cnf(u57667,negated_conjecture,
( ~ product(e_1,X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(u57421,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X1,e_3) ) ).
cnf(u305,axiom,
equalish(e_4,e_4) ).
cnf(u57082,negated_conjecture,
( ~ product(e_4,e_1,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_4) ) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1) ).
cnf(u57035,negated_conjecture,
( ~ product(e_2,e_2,X0)
| equalish(X0,e_2) ) ).
cnf(u57624,negated_conjecture,
( ~ product(e_2,X0,e_5)
| ~ group_element(X0)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(u56773,negated_conjecture,
( ~ product(e_3,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u56829,negated_conjecture,
( ~ product(e_4,e_5,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_5) ) ).
cnf(u9046,negated_conjecture,
( ~ product(X1,X0,e_5)
| product(e_5,X0,e_4)
| product(e_5,X0,e_3)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1)
| ~ group_element(X0)
| ~ group_element(X1)
| product(X1,e_2,e_4)
| product(X1,e_2,e_3)
| product(X1,e_2,e_2)
| product(X1,e_2,e_1)
| equalish(X0,e_2) ) ).
cnf(u14887,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,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(u57592,negated_conjecture,
( ~ product(e_4,X0,e_3)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(u9050,negated_conjecture,
( ~ group_element(X1)
| product(e_2,X0,e_4)
| product(e_2,X0,e_3)
| product(e_2,X0,e_2)
| product(e_2,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_2)
| product(X1,e_2,e_4)
| product(X1,e_2,e_3)
| product(X1,e_2,e_1)
| ~ product(X1,X0,e_2) ) ).
cnf(u56774,negated_conjecture,
( ~ product(e_3,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u57647,negated_conjecture,
( ~ product(e_3,X0,e_1)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(element_3,axiom,
group_element(e_3) ).
cnf(u53677,negated_conjecture,
( ~ product(e_5,e_4,X0)
| equalish(X0,e_4) ) ).
cnf(u57614,negated_conjecture,
( ~ product(e_4,X0,e_2)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u11049,negated_conjecture,
( ~ product(e_5,X0,e_4)
| product(e_4,X0,e_3)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_2)
| product(e_4,X0,e_4) ) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(u1285,axiom,
equalish(e_2,e_2) ).
cnf(u56765,negated_conjecture,
( ~ product(e_4,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u57013,negated_conjecture,
( ~ product(e_3,e_3,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_3) ) ).
cnf(u57601,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_2)
| equalish(X0,e_5)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ) ).
cnf(u57039,negated_conjecture,
( ~ product(e_2,e_2,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_2) ) ).
cnf(u57050,axiom,
( ~ product(e_2,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u56827,negated_conjecture,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_2) ) ).
cnf(u57000,negated_conjecture,
( ~ product(e_3,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u57247,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u57019,negated_conjecture,
( ~ product(e_4,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u57074,negated_conjecture,
( ~ product(e_2,e_1,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_2) ) ).
cnf(u53260,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_1)
| equalish(X1,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)
| ~ product(X0,X1,X2) ) ).
cnf(u57538,negated_conjecture,
( ~ product(e_1,X1,X0)
| equalish(X0,e_5)
| ~ product(X0,X1,e_3) ) ).
cnf(u57002,negated_conjecture,
( ~ product(e_4,e_3,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_4) ) ).
cnf(u56791,negated_conjecture,
( ~ product(e_1,e_2,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_2) ) ).
cnf(u10660,negated_conjecture,
( ~ product(e_5,X0,e_3)
| product(e_3,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_2)
| product(e_3,X0,e_4) ) ).
cnf(u20623,axiom,
equalish(e_1,e_1) ).
cnf(u57014,negated_conjecture,
( ~ product(e_3,e_3,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_3) ) ).
cnf(u57208,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X1,e_4) ) ).
cnf(u57292,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u56799,negated_conjecture,
( ~ product(e_1,e_5,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_5) ) ).
cnf(u57711,negated_conjecture,
( ~ product(e_3,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)
| ~ group_element(X0) ) ).
cnf(u57419,negated_conjecture,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_3)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_4) ) ).
cnf(u57701,negated_conjecture,
( ~ product(e_1,X0,e_3)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u56781,negated_conjecture,
( ~ product(e_1,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u56110,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_3)
| equalish(X2,e_5)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u53253,axiom,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_1) ) ).
cnf(u53678,negated_conjecture,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u57131,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X0,e_2) ) ).
cnf(u64,axiom,
( ~ group_element(X0)
| product(X1,e_4,e_1)
| product(X1,e_4,e_2)
| product(X1,e_4,e_3)
| product(X1,e_4,e_4)
| ~ group_element(X1)
| 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,X1) ) ).
cnf(u57261,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_3,X0,X1)
| equalish(X0,e_3) ) ).
cnf(u14963,axiom,
( ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| product(X0,e_3,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(u57038,negated_conjecture,
( ~ product(e_2,e_2,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_2) ) ).
cnf(u56813,negated_conjecture,
( ~ product(e_2,e_5,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_2) ) ).
cnf(u57053,negated_conjecture,
( ~ product(e_3,e_1,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_3) ) ).
cnf(u15410,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,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(u57330,negated_conjecture,
( ~ group_element(X1)
| equalish(X0,e_1)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_2,X0,X1) ) ).
cnf(u56826,negated_conjecture,
( ~ product(e_2,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u14876,axiom,
( ~ group_element(X0)
| product(X1,e_1,e_1)
| product(X1,e_1,e_2)
| product(X1,e_1,e_3)
| product(X1,e_1,e_4)
| ~ group_element(X1)
| equalish(X0,e_1)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(u57020,negated_conjecture,
( ~ product(X0,e_2,e_4)
| equalish(X0,e_4) ) ).
cnf(u15669,negated_conjecture,
( ~ group_element(X0)
| product(e_1,X0,e_4)
| product(e_1,X0,e_3)
| product(e_1,X0,e_2)
| ~ group_element(X1)
| equalish(X0,e_2)
| product(X1,e_2,e_4)
| product(X1,e_2,e_3)
| product(X1,e_2,e_2)
| ~ product(X1,X0,e_1) ) ).
cnf(u57271,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u53679,negated_conjecture,
( ~ product(X0,e_4,e_4)
| equalish(X0,e_5) ) ).
cnf(u57001,negated_conjecture,
( ~ product(X0,e_3,e_4)
| equalish(X0,e_3) ) ).
cnf(u56124,negated_conjecture,
( ~ product(X0,e_3,e_2)
| equalish(X0,e_5) ) ).
cnf(u57311,negated_conjecture,
( ~ product(e_5,X0,e_1)
| ~ 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) ) ).
cnf(u61,axiom,
( ~ group_element(X0)
| product(X1,e_1,e_1)
| product(X1,e_1,e_2)
| product(X1,e_1,e_3)
| product(X1,e_1,e_4)
| ~ group_element(X1)
| 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,X1) ) ).
cnf(u65,axiom,
( ~ group_element(X0)
| product(X1,e_5,e_1)
| product(X1,e_5,e_2)
| product(X1,e_5,e_3)
| product(X1,e_5,e_4)
| ~ group_element(X1)
| 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,X1) ) ).
cnf(u10661,negated_conjecture,
( ~ product(e_5,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_2)
| product(e_3,X0,e_4) ) ).
cnf(u57373,negated_conjecture,
( ~ group_element(X1)
| equalish(X1,e_3)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_2,X0,X1) ) ).
cnf(u56828,negated_conjecture,
( ~ product(e_4,e_5,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_4) ) ).
cnf(u57,negated_conjecture,
( ~ product(X0,X1,X2)
| equalish(X2,e_5)
| ~ group_element(X3)
| product(X0,X3,e_1)
| product(X0,X3,e_2)
| product(X0,X3,e_3)
| product(X0,X3,e_4)
| ~ group_element(X0)
| product(e_5,X3,e_1)
| product(e_5,X3,e_2)
| product(e_5,X3,e_3)
| product(e_5,X3,e_4)
| ~ group_element(X1)
| product(X2,X1,e_1)
| product(X2,X1,e_2)
| product(X2,X1,e_3)
| product(X2,X1,e_4)
| ~ group_element(X2) ) ).
cnf(u57070,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)
| 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(u9051,negated_conjecture,
( ~ group_element(X1)
| product(e_1,X0,e_4)
| product(e_1,X0,e_3)
| product(e_1,X0,e_2)
| product(e_1,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_2)
| product(X1,e_2,e_4)
| product(X1,e_2,e_3)
| product(X1,e_2,e_2)
| ~ product(X1,X0,e_1) ) ).
cnf(u53680,negated_conjecture,
( ~ product(e_4,e_4,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_4) ) ).
cnf(u57380,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_1,X0,X1)
| equalish(X1,e_2) ) ).
cnf(u57226,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X1,e_3) ) ).
cnf(u54135,negated_conjecture,
( ~ product(e_2,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u42,negated_conjecture,
( ~ product(X2,X1,e_5)
| ~ product(X0,X1,X2)
| equalish(X2,e_5)
| ~ group_element(X3)
| product(X0,X3,e_1)
| product(X0,X3,e_2)
| product(X0,X3,e_3)
| product(X0,X3,e_4)
| ~ group_element(X0)
| product(e_5,X3,e_1)
| product(e_5,X3,e_2)
| product(e_5,X3,e_3)
| product(e_5,X3,e_4) ) ).
cnf(u57591,negated_conjecture,
( ~ product(e_4,X0,e_5)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u54138,negated_conjecture,
( ~ product(e_1,e_3,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_3) ) ).
cnf(u57510,negated_conjecture,
( ~ product(e_4,X1,X0)
| equalish(X0,e_5)
| ~ product(X0,X1,e_2) ) ).
cnf(product_total_function2,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u56797,negated_conjecture,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_4) ) ).
cnf(u57496,negated_conjecture,
( ~ product(e_2,X1,X0)
| equalish(X1,e_4)
| ~ product(X0,X1,e_4) ) ).
cnf(u56777,negated_conjecture,
( ~ product(e_1,e_4,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_4) ) ).
cnf(u53252,axiom,
( ~ product(e_5,e_1,X0)
| equalish(X0,e_1) ) ).
cnf(u57676,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_3)
| equalish(X0,e_4)
| product(e_1,X0,e_1)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(u39,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X2,X3,X4)
| ~ product(X4,X3,X1)
| equalish(X4,e_5)
| ~ group_element(X0)
| product(X2,X0,e_1)
| product(X2,X0,e_2)
| product(X2,X0,e_3)
| product(X2,X0,e_4)
| ~ group_element(X2) ) ).
cnf(u57028,negated_conjecture,
( ~ product(X0,e_2,e_3)
| equalish(X0,e_3) ) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(u35,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X2,X3,X4)
| ~ product(X4,X3,X1)
| equalish(X3,X0)
| ~ group_element(X0)
| product(X2,X0,e_1)
| product(X2,X0,e_2)
| product(X2,X0,e_3)
| product(X2,X0,e_4)
| ~ group_element(X2) ) ).
cnf(u56798,negated_conjecture,
( ~ product(e_1,e_5,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_1) ) ).
cnf(u56790,negated_conjecture,
( ~ product(e_1,e_2,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_1) ) ).
cnf(u57171,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u14888,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,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(u57204,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_4,X0,X1)
| equalish(X1,e_1) ) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u57167,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_4,X0,X1)
| equalish(X0,e_5) ) ).
cnf(u57331,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X1,e_1) ) ).
cnf(u57482,negated_conjecture,
( ~ product(e_3,X1,X0)
| equalish(X0,e_5)
| ~ product(X0,X1,e_1) ) ).
cnf(u57345,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_1,X0,X1)
| equalish(X0,e_4) ) ).
cnf(product_right_cancellation,axiom,
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u10680,negated_conjecture,
( ~ product(e_5,X0,e_1)
| product(e_1,X0,e_3)
| product(e_1,X0,e_2)
| product(e_1,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_2)
| product(e_1,X0,e_4) ) ).
cnf(u56943,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(u57346,negated_conjecture,
( ~ group_element(X1)
| equalish(X0,e_4)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_1,X0,X1) ) ).
cnf(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5) ).
cnf(u57689,negated_conjecture,
( ~ product(e_2,X0,e_1)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u56795,negated_conjecture,
( ~ product(e_4,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3) ).
cnf(u57440,negated_conjecture,
( ~ product(e_3,X1,X0)
| equalish(X1,e_1)
| ~ product(X0,X1,e_1) ) ).
cnf(u57372,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_2,X0,X1)
| equalish(X1,e_3) ) ).
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5) ).
cnf(u57646,negated_conjecture,
( ~ product(e_3,X0,e_2)
| ~ group_element(X0)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u56767,negated_conjecture,
( ~ product(e_3,e_4,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_3) ) ).
cnf(u57169,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u57079,axiom,
( ~ product(e_1,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5) ).
cnf(u56126,negated_conjecture,
( ~ product(e_2,e_3,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_3) ) ).
cnf(u57022,negated_conjecture,
( ~ product(e_4,e_2,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_2) ) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(u57468,negated_conjecture,
( ~ product(e_4,X1,X0)
| equalish(X1,e_3)
| ~ product(X0,X1,e_2) ) ).
cnf(u57303,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X1,e_3) ) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(u56776,negated_conjecture,
( ~ product(e_1,e_4,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_1) ) ).
cnf(u57410,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u57075,negated_conjecture,
( ~ product(e_2,e_1,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_1) ) ).
cnf(u57184,negated_conjecture,
( ~ product(e_5,X0,e_3)
| ~ 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) ) ).
cnf(u57052,axiom,
( ~ product(X0,e_1,e_3)
| equalish(X0,e_2) ) ).
cnf(u57430,negated_conjecture,
( ~ product(e_5,X0,e_4)
| ~ 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) ) ).
cnf(u57159,negated_conjecture,
( ~ product(e_5,X0,e_2)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4) ) ).
cnf(u56825,negated_conjecture,
( ~ product(e_2,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u57205,negated_conjecture,
( ~ group_element(X1)
| equalish(X1,e_1)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_4,X0,X1) ) ).
cnf(u56784,negated_conjecture,
( ~ product(e_2,e_4,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_4) ) ).
cnf(u57081,axiom,
( ~ product(X0,e_1,e_4)
| equalish(X0,e_1) ) ).
cnf(u57026,negated_conjecture,
( ~ product(e_3,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u53255,negated_conjecture,
( ~ product(e_1,e_1,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_1) ) ).
cnf(u56123,negated_conjecture,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u57245,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u15020,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,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(u53261,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_1)
| equalish(X2,e_5)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u56788,negated_conjecture,
( ~ product(e_1,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u57009,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(u57408,negated_conjecture,
( ~ product(e_5,X0,e_1)
| ~ group_element(X0)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(u15422,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,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(u56814,negated_conjecture,
( ~ product(e_2,e_5,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_5) ) ).
cnf(u57206,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X1,e_2) ) ).
cnf(u14890,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,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(u56766,negated_conjecture,
( ~ product(X0,e_4,e_3)
| equalish(X0,e_4) ) ).
cnf(u57382,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X1,e_1) ) ).
cnf(u57029,negated_conjecture,
( ~ product(e_3,e_2,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_3) ) ).
cnf(u56122,negated_conjecture,
( ~ product(e_5,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u14879,axiom,
( ~ group_element(X0)
| product(X1,e_4,e_1)
| product(X1,e_4,e_2)
| product(X1,e_4,e_3)
| product(X1,e_4,e_4)
| ~ group_element(X1)
| equalish(X0,e_4)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(u57320,negated_conjecture,
( ~ group_element(X1)
| equalish(X1,e_4)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_3,X0,X1) ) ).
cnf(u57010,negated_conjecture,
( ~ product(e_1,e_3,X0)
| equalish(X0,e_3) ) ).
cnf(u57243,negated_conjecture,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(u57288,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X1,e_2) ) ).
cnf(u57329,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_2,X0,X1)
| equalish(X0,e_1) ) ).
cnf(u56775,negated_conjecture,
( ~ product(X0,e_4,e_1)
| equalish(X0,e_3) ) ).
cnf(u57593,negated_conjecture,
( ~ product(e_4,X0,e_2)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u33,axiom,
( ~ product(X0,X1,e_5)
| 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)
| ~ group_element(X0) ) ).
cnf(u53254,axiom,
( ~ product(X0,e_1,e_1)
| equalish(X0,e_5) ) ).
cnf(u57364,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X1,e_2) ) ).
cnf(u57655,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_1)
| equalish(X0,e_3)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3) ) ).
cnf(u57399,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X1,e_1) ) ).
cnf(u57027,negated_conjecture,
( ~ product(e_3,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u56999,negated_conjecture,
( ~ product(e_3,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(u14877,axiom,
( ~ group_element(X0)
| product(X1,e_2,e_1)
| product(X1,e_2,e_2)
| product(X1,e_2,e_3)
| product(X1,e_2,e_4)
| ~ group_element(X1)
| equalish(X0,e_2)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(u56780,negated_conjecture,
( ~ product(e_1,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(u57269,negated_conjecture,
( ~ product(e_5,X0,e_4)
| ~ 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) ) ).
cnf(u57550,negated_conjecture,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_1)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3) ) ).
cnf(u56,axiom,
( ~ group_element(X1)
| equalish(X0,X1)
| product(X2,X1,e_1)
| product(X2,X1,e_2)
| product(X2,X1,e_3)
| product(X2,X1,e_4)
| ~ group_element(X2)
| ~ group_element(X0)
| product(X2,X0,e_1)
| product(X2,X0,e_2)
| product(X2,X0,e_3)
| product(X2,X0,e_4) ) ).
cnf(u38374,negated_conjecture,
( ~ product(X0,e_5,e_1)
| product(X0,e_2,e_4)
| product(X0,e_2,e_3)
| product(X0,e_2,e_2)
| ~ group_element(X0) ) ).
cnf(qg1_1,negated_conjecture,
( ~ product(X5,X4,X3)
| ~ product(X3,X4,X2)
| ~ product(X5,X1,X0)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u57012,negated_conjecture,
( ~ product(X0,e_3,e_3)
| equalish(X0,e_1) ) ).
cnf(u56789,negated_conjecture,
( ~ product(X0,e_2,e_1)
| equalish(X0,e_1) ) ).
cnf(u56102,negated_conjecture,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_5) ) ).
cnf(u57073,axiom,
( ~ product(X0,e_1,e_2)
| equalish(X0,e_4) ) ).
cnf(u57080,axiom,
( ~ product(e_1,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u57381,negated_conjecture,
( ~ group_element(X1)
| equalish(X1,e_2)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_1,X0,X1) ) ).
cnf(u57139,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X1,e_2) ) ).
cnf(u57568,negated_conjecture,
( ~ product(e_5,X0,e_2)
| ~ 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) ) ).
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(u57392,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(u57036,negated_conjecture,
( ~ product(e_2,X0,e_2)
| equalish(X0,e_2) ) ).
cnf(u56125,negated_conjecture,
( ~ product(e_2,e_3,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_2) ) ).
cnf(u38,negated_conjecture,
( ~ product(X2,X1,e_5)
| ~ product(X0,X1,X2)
| equalish(X1,X3)
| ~ group_element(X3)
| product(X0,X3,e_1)
| product(X0,X3,e_2)
| product(X0,X3,e_3)
| product(X0,X3,e_4)
| ~ group_element(X0)
| product(e_5,X3,e_1)
| product(e_5,X3,e_2)
| product(e_5,X3,e_3)
| product(e_5,X3,e_4) ) ).
cnf(u57524,negated_conjecture,
( ~ product(e_2,X1,X0)
| equalish(X0,e_5)
| ~ product(X0,X1,e_4) ) ).
cnf(u57279,negated_conjecture,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_4) ) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2) ).
cnf(u57347,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X1,e_4) ) ).
cnf(u34,axiom,
( ~ product(X0,X1,e_5)
| 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)
| ~ group_element(X2) ) ).
cnf(u57030,negated_conjecture,
( ~ product(e_3,e_2,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_2) ) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(u57319,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_3,X0,X1)
| equalish(X1,e_4) ) ).
cnf(u53681,negated_conjecture,
( ~ product(e_4,e_4,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_4) ) ).
cnf(u15668,negated_conjecture,
( ~ group_element(X0)
| product(e_4,X0,e_3)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1)
| ~ group_element(X1)
| equalish(X0,e_2)
| product(X1,e_2,e_3)
| product(X1,e_2,e_2)
| product(X1,e_2,e_1)
| ~ product(X1,X0,e_4) ) ).
cnf(u57699,negated_conjecture,
( ~ product(e_1,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)
| ~ group_element(X0) ) ).
cnf(u57235,negated_conjecture,
( ~ product(e_5,X0,e_3)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_4) ) ).
cnf(u57354,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u56130,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_2)
| equalish(X1,e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u56109,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_3)
| equalish(X1,e_5)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u57051,axiom,
( ~ product(e_2,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u57186,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u56951,negated_conjecture,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3) ) ).
cnf(u56764,negated_conjecture,
( ~ product(e_4,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u56104,negated_conjecture,
( ~ product(e_3,e_5,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_5) ) ).
cnf(u56783,negated_conjecture,
( ~ product(e_2,e_4,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_2) ) ).
cnf(qg1_2,negated_conjecture,
( ~ product(X5,X4,X3)
| ~ product(X3,X4,X2)
| ~ product(X5,X1,X0)
| ~ product(X0,X1,X2)
| equalish(X1,X4) ) ).
cnf(u56101,negated_conjecture,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(u56796,negated_conjecture,
( ~ product(e_4,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(u15661,negated_conjecture,
( ~ product(e_5,X0,e_4)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_2)
| product(e_4,X0,e_3) ) ).
cnf(u56812,negated_conjecture,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_3) ) ).
cnf(u57645,negated_conjecture,
( ~ product(e_3,X0,e_5)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u57321,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(u57071,axiom,
( ~ product(e_4,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u57054,negated_conjecture,
( ~ product(e_3,e_1,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_1) ) ).
cnf(u57612,negated_conjecture,
( ~ product(e_4,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)
| ~ group_element(X0) ) ).
cnf(u14945,axiom,
( ~ group_element(X0)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| product(X0,e_2,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(u57083,negated_conjecture,
( ~ product(e_4,e_1,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_1) ) ).
cnf(u15658,negated_conjecture,
( ~ product(e_5,X0,e_1)
| product(e_1,X0,e_3)
| product(e_1,X0,e_2)
| ~ group_element(X0)
| equalish(X0,e_2)
| product(e_1,X0,e_4) ) ).
cnf(u14889,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,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(u56782,negated_conjecture,
( ~ product(X0,e_4,e_2)
| equalish(X0,e_1) ) ).
cnf(u14878,axiom,
( ~ group_element(X0)
| product(X1,e_3,e_1)
| product(X1,e_3,e_2)
| product(X1,e_3,e_3)
| product(X1,e_3,e_4)
| ~ group_element(X1)
| equalish(X0,e_3)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(element_5,axiom,
group_element(e_5) ).
cnf(u57150,negated_conjecture,
( ~ product(e_5,X0,e_1)
| ~ 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) ) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(u57687,negated_conjecture,
( ~ product(e_2,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)
| ~ group_element(X0) ) ).
cnf(u54136,negated_conjecture,
( ~ product(X0,e_3,e_1)
| equalish(X0,e_2) ) ).
cnf(u16505,axiom,
equalish(e_3,e_3) ).
cnf(u57700,negated_conjecture,
( ~ product(e_1,X0,e_4)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u57666,negated_conjecture,
( ~ product(e_1,X0,e_5)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u57262,negated_conjecture,
( ~ group_element(X1)
| equalish(X0,e_3)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_3,X0,X1) ) ).
cnf(u57011,negated_conjecture,
( ~ product(e_1,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(u56131,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_2)
| equalish(X2,e_5)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u56768,negated_conjecture,
( ~ product(e_3,e_4,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_4) ) ).
cnf(u57712,negated_conjecture,
( ~ product(e_3,X0,e_2)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u57713,negated_conjecture,
( ~ product(e_3,X0,e_1)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u57003,negated_conjecture,
( ~ product(e_4,e_3,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_3) ) ).
cnf(u57626,negated_conjecture,
( ~ product(e_2,X0,e_1)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u57168,negated_conjecture,
( ~ group_element(X1)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_4,X0,X1) ) ).
cnf(u57018,negated_conjecture,
( ~ product(e_4,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u57290,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u53256,negated_conjecture,
( ~ product(e_1,e_1,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_1) ) ).
cnf(u56810,negated_conjecture,
( ~ product(e_3,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(u14880,axiom,
( ~ group_element(X0)
| product(X1,e_5,e_1)
| product(X1,e_5,e_2)
| product(X1,e_5,e_3)
| product(X1,e_5,e_4)
| ~ group_element(X1)
| equalish(X0,e_5)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(u57217,negated_conjecture,
( ~ product(e_5,X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3) ) ).
cnf(u56787,negated_conjecture,
( ~ product(e_1,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u57037,negated_conjecture,
( ~ product(X0,e_2,e_2)
| equalish(X0,e_2) ) ).
cnf(u53686,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_4)
| equalish(X2,e_5)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u9049,negated_conjecture,
( ~ group_element(X1)
| product(e_3,X0,e_4)
| product(e_3,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_2)
| product(X1,e_2,e_4)
| product(X1,e_2,e_2)
| product(X1,e_2,e_1)
| ~ product(X1,X0,e_3) ) ).
cnf(u14946,axiom,
( ~ group_element(X0)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| product(X0,e_2,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(u57625,negated_conjecture,
( ~ product(e_2,X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u18043,negated_conjecture,
( ~ product(X0,e_3,e_4)
| product(X0,e_2,e_3)
| product(X0,e_2,e_2)
| product(X0,e_2,e_1)
| ~ group_element(X0) ) ).
cnf(u57613,negated_conjecture,
( ~ product(e_4,X0,e_3)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u62,axiom,
( ~ group_element(X0)
| product(X1,e_2,e_1)
| product(X1,e_2,e_2)
| product(X1,e_2,e_3)
| product(X1,e_2,e_4)
| ~ group_element(X1)
| 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,X1) ) ).
cnf(u54137,negated_conjecture,
( ~ product(e_1,e_3,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_1) ) ).
cnf(u57021,negated_conjecture,
( ~ product(e_4,e_2,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_4) ) ).
cnf(u54134,negated_conjecture,
( ~ product(e_2,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u58,negated_conjecture,
( ~ group_element(X3)
| equalish(X1,X3)
| ~ product(X0,X1,X2)
| product(X0,X3,e_1)
| product(X0,X3,e_2)
| product(X0,X3,e_3)
| product(X0,X3,e_4)
| ~ group_element(X0)
| product(e_5,X3,e_1)
| product(e_5,X3,e_2)
| product(e_5,X3,e_3)
| product(e_5,X3,e_4)
| ~ group_element(X1)
| product(X2,X1,e_1)
| product(X2,X1,e_2)
| product(X2,X1,e_3)
| product(X2,X1,e_4)
| ~ group_element(X2) ) ).
cnf(u57454,negated_conjecture,
( ~ product(e_1,X1,X0)
| equalish(X1,e_5)
| ~ product(X0,X1,e_3) ) ).
cnf(u57584,negated_conjecture,
( ~ product(e_5,X0,e_3)
| ~ 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) ) ).
cnf(u57668,negated_conjecture,
( ~ product(e_1,X0,e_3)
| ~ group_element(X0)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u56811,negated_conjecture,
( ~ product(e_3,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(u57688,negated_conjecture,
( ~ product(e_2,X0,e_4)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u57072,axiom,
( ~ product(e_4,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u57390,negated_conjecture,
( ~ product(e_5,X0,e_2)
| ~ 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) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP131-1.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n006.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 09:28:11 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/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
% 8.59/2.06 % (2729321)Input is clausal, will run a generic CNF schedule.
% 8.59/2.06 % (2729327)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1323541867:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.59/2.06 % (2729331)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1748177209:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.59/2.06 % (2729329)lrs+10_1_sil=8000:sp=occurrence:random_seed=3461260467:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.59/2.06 % (2729326)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=1529631071:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.59/2.06 % (2729330)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2342924820:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.59/2.06 % (2729328)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2377774176:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.59/2.06 % (2729332)dis-21_1_sil=8000:lcm=predicate:random_seed=362382710: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)
% 8.59/2.06 % (2729329)Instruction limit reached!
% 8.59/2.06 % (2729329)------------------------------
% 8.59/2.06 % (2729329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.06 % (2729329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.06 % (2729329)CaDiCaL version: 2.1.3
% 8.59/2.06 % (2729329)Termination reason: Instruction limit
% 8.59/2.06 % (2729329)Termination phase: Saturation
% 8.59/2.06 % (2729329)Time elapsed: 0.051 s
% 8.59/2.06 % (2729329)Peak memory usage: 87 MB
% 8.59/2.06 % (2729329)Instructions burned: 108 (million)
% 8.59/2.06 % (2729330)Instruction limit reached!
% 8.59/2.06 % (2729330)------------------------------
% 8.59/2.06 % (2729330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.06 % (2729330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.06 % (2729330)CaDiCaL version: 2.1.3
% 8.59/2.06 % (2729330)Termination reason: Instruction limit
% 8.59/2.06 % (2729330)Termination phase: Saturation
% 8.59/2.06 % (2729330)Time elapsed: 0.057 s
% 8.59/2.06 % (2729330)Peak memory usage: 87 MB
% 8.59/2.06 % (2729330)Instructions burned: 115 (million)
% 8.59/2.06 % (2729332)Instruction limit reached!
% 8.59/2.06 % (2729332)------------------------------
% 8.59/2.06 % (2729332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.06 % (2729332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.06 % (2729332)CaDiCaL version: 2.1.3
% 8.59/2.06 % (2729332)Termination reason: Instruction limit
% 8.59/2.06 % (2729332)Termination phase: Saturation
% 8.59/2.06 % (2729332)Time elapsed: 0.068 s
% 8.59/2.06 % (2729332)Peak memory usage: 89 MB
% 8.59/2.06 % (2729332)Instructions burned: 117 (million)
% 8.59/2.06 % (2729331)Instruction limit reached!
% 8.59/2.06 % (2729331)------------------------------
% 8.59/2.06 % (2729331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.06 % (2729331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.06 % (2729331)CaDiCaL version: 2.1.3
% 8.59/2.06 % (2729331)Termination reason: Instruction limit
% 8.59/2.06 % (2729331)Termination phase: Saturation
% 8.59/2.06 % (2729331)Time elapsed: 0.114 s
% 8.59/2.06 % (2729331)Peak memory usage: 89 MB
% 8.59/2.06 % (2729331)Instructions burned: 180 (million)
% 8.59/2.06 % (2729340)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=3520071792:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 8.59/2.06 % (2729341)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2394939997: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)
% 8.59/2.06 % (2729341)Refutation not found, incomplete strategy
% 8.59/2.06 % (2729341)------------------------------
% 8.59/2.06 % (2729341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.59/2.06 % (2729341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.59/2.06 % (2729341)CaDiCaL version: 2.1.3
% 13.16/2.93 % (2729341)Termination reason: Refutation not found, incomplete strategy
% 13.16/2.93 % (2729341)Time elapsed: 0.002 s
% 13.16/2.93 % (2729341)Peak memory usage: 87 MB
% 13.16/2.93 % (2729341)Instructions burned: 2 (million)
% 13.16/2.93 % (2729342)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1540312050:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 13.16/2.93 % (2729343)lrs+10_64_to=lpo:sil=8000:random_seed=4227404528:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 13.16/2.93 % (2729340)Instruction limit reached!
% 13.16/2.93 % (2729340)------------------------------
% 13.16/2.93 % (2729340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.16/2.93 % (2729340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.16/2.93 % (2729340)CaDiCaL version: 2.1.3
% 13.16/2.93 % (2729340)Termination reason: Instruction limit
% 13.16/2.93 % (2729340)Termination phase: Saturation
% 13.16/2.93 % (2729340)Time elapsed: 0.072 s
% 13.16/2.93 % (2729340)Peak memory usage: 88 MB
% 13.16/2.93 % (2729340)Instructions burned: 143 (million)
% 13.16/2.93 % (2729327)Refutation not found, incomplete strategy
% 13.16/2.93 % (2729327)------------------------------
% 13.16/2.93 % (2729327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.16/2.93 % (2729327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.16/2.93 % (2729327)CaDiCaL version: 2.1.3
% 13.16/2.93 % (2729327)Termination reason: Refutation not found, incomplete strategy
% 13.16/2.93 % (2729327)Time elapsed: 0.346 s
% 13.16/2.93 % (2729327)Peak memory usage: 127 MB
% 13.16/2.93 % (2729327)Instructions burned: 863 (million)
% 13.16/2.93 % (2729342)Instruction limit reached!
% 13.16/2.93 % (2729342)------------------------------
% 13.16/2.93 % (2729342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.16/2.93 % (2729342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.16/2.93 % (2729342)CaDiCaL version: 2.1.3
% 13.16/2.93 % (2729342)Termination reason: Instruction limit
% 13.16/2.93 % (2729342)Termination phase: Saturation
% 13.16/2.93 % (2729342)Time elapsed: 0.110 s
% 13.16/2.93 % (2729342)Peak memory usage: 88 MB
% 13.16/2.93 % (2729342)Instructions burned: 219 (million)
% 13.16/2.93 % (2729343)Instruction limit reached!
% 13.16/2.93 % (2729343)------------------------------
% 13.16/2.93 % (2729343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.16/2.93 % (2729343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.16/2.93 % (2729343)CaDiCaL version: 2.1.3
% 13.16/2.93 % (2729343)Termination reason: Instruction limit
% 13.16/2.93 % (2729343)Termination phase: Saturation
% 13.16/2.93 % (2729343)Time elapsed: 0.074 s
% 13.16/2.93 % (2729343)Peak memory usage: 88 MB
% 13.16/2.93 % (2729343)Instructions burned: 128 (million)
% 13.16/2.93 % (2729348)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=792254889:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 13.16/2.93 % (2729341)------------------------------
% 13.16/2.93 % (2729341)------------------------------
% 13.16/2.93 % (2729327)------------------------------
% 13.16/2.93 % (2729327)------------------------------
% 13.16/2.93 % (2729350)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3489537684:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 13.16/2.93 % (2729349)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=212309373:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 13.16/2.93 % (2729348)Instruction limit reached!
% 13.16/2.93 % (2729348)------------------------------
% 13.16/2.93 % (2729348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.16/2.93 % (2729348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.16/2.93 % (2729348)CaDiCaL version: 2.1.3
% 13.16/2.93 % (2729348)Termination reason: Instruction limit
% 13.16/2.93 % (2729348)Termination phase: Saturation
% 13.16/2.93 % (2729348)Time elapsed: 0.120 s
% 13.16/2.93 % (2729348)Peak memory usage: 88 MB
% 13.16/2.93 % (2729348)Instructions burned: 194 (million)
% 13.16/2.93 % (2729349)Instruction limit reached!
% 13.16/2.93 % (2729349)------------------------------
% 13.16/2.93 % (2729349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.16/2.93 % (2729349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.16/2.93 % (2729349)CaDiCaL version: 2.1.3
% 13.16/2.93 % (2729349)Termination reason: Instruction limit
% 13.16/2.93 % (2729349)Termination phase: Saturation
% 23.37/4.17 % (2729349)Time elapsed: 0.076 s
% 23.37/4.17 % (2729349)Peak memory usage: 88 MB
% 23.37/4.17 % (2729349)Instructions burned: 159 (million)
% 23.37/4.17 % (2729353)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3995436862:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 23.37/4.17 % (2729352)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=71584917:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 23.37/4.17 % (2729352)Refutation not found, incomplete strategy
% 23.37/4.17 % (2729352)------------------------------
% 23.37/4.17 % (2729352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.37/4.17 % (2729352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.37/4.17 % (2729352)CaDiCaL version: 2.1.3
% 23.37/4.17 % (2729352)Termination reason: Refutation not found, incomplete strategy
% 23.37/4.17 % (2729352)Time elapsed: 0.002 s
% 23.37/4.17 % (2729352)Peak memory usage: 88 MB
% 23.37/4.17 % (2729352)Instructions burned: 2 (million)
% 23.37/4.17 % (2729353)Instruction limit reached!
% 23.37/4.17 % (2729353)------------------------------
% 23.37/4.17 % (2729353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.37/4.17 % (2729353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.37/4.17 % (2729353)CaDiCaL version: 2.1.3
% 23.37/4.17 % (2729353)Termination reason: Instruction limit
% 23.37/4.17 % (2729353)Termination phase: Saturation
% 23.37/4.17 % (2729353)Time elapsed: 0.027 s
% 23.37/4.17 % (2729353)Peak memory usage: 87 MB
% 23.37/4.17 % (2729353)Instructions burned: 107 (million)
% 23.37/4.17 % (2729356)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2035967063:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 23.37/4.17 % (2729357)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3309684922:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 23.37/4.17 % (2729360)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1240828323:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 23.37/4.17 % (2729360)Instruction limit reached!
% 23.37/4.17 % (2729360)------------------------------
% 23.37/4.17 % (2729360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.37/4.17 % (2729360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.37/4.17 % (2729360)CaDiCaL version: 2.1.3
% 23.37/4.17 % (2729360)Termination reason: Instruction limit
% 23.37/4.17 % (2729360)Termination phase: Saturation
% 23.37/4.17 % (2729360)Time elapsed: 0.044 s
% 23.37/4.17 % (2729360)Peak memory usage: 89 MB
% 23.37/4.17 % (2729360)Instructions burned: 136 (million)
% 23.37/4.17 % (2729356)Instruction limit reached!
% 23.37/4.17 % (2729356)------------------------------
% 23.37/4.17 % (2729356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.37/4.17 % (2729356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.37/4.17 % (2729356)CaDiCaL version: 2.1.3
% 23.37/4.17 % (2729356)Termination reason: Instruction limit
% 23.37/4.17 % (2729356)Termination phase: Saturation
% 23.37/4.17 % (2729356)Time elapsed: 0.116 s
% 23.37/4.17 % (2729356)Peak memory usage: 88 MB
% 23.37/4.17 % (2729356)Instructions burned: 244 (million)
% 23.37/4.17 % (2729352)------------------------------
% 23.37/4.17 % (2729352)------------------------------
% 23.37/4.17 % (2729364)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3506833205:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 23.37/4.17 % (2729365)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=647902982:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 23.37/4.17 % (2729366)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1577507406:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 23.37/4.17 % (2729364)Instruction limit reached!
% 23.37/4.17 % (2729364)------------------------------
% 23.37/4.17 % (2729364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.37/4.17 % (2729364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.37/4.17 % (2729364)CaDiCaL version: 2.1.3
% 23.37/4.17 % (2729364)Termination reason: Instruction limit
% 32.52/5.55 % (2729364)Termination phase: Saturation
% 32.52/5.55 % (2729364)Time elapsed: 0.124 s
% 32.52/5.55 % (2729364)Peak memory usage: 88 MB
% 32.52/5.55 % (2729364)Instructions burned: 500 (million)
% 32.52/5.55 % (2729365)Instruction limit reached!
% 32.52/5.55 % (2729365)------------------------------
% 32.52/5.55 % (2729365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.55 % (2729365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.55 % (2729365)CaDiCaL version: 2.1.3
% 32.52/5.55 % (2729365)Termination reason: Instruction limit
% 32.52/5.55 % (2729365)Termination phase: Saturation
% 32.52/5.55 % (2729365)Time elapsed: 0.107 s
% 32.52/5.55 % (2729365)Peak memory usage: 88 MB
% 32.52/5.55 % (2729365)Instructions burned: 192 (million)
% 32.52/5.55 % (2729370)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=832571408:cond=on:i=156:bs=on:gtg=exists_all:er=known_2988 on theBenchmark for (2988ds/156Mi)
% 32.52/5.55 % (2729366)Instruction limit reached!
% 32.52/5.55 % (2729366)------------------------------
% 32.52/5.55 % (2729366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.55 % (2729366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.55 % (2729366)CaDiCaL version: 2.1.3
% 32.52/5.55 % (2729366)Termination reason: Instruction limit
% 32.52/5.55 % (2729366)Termination phase: Saturation
% 32.52/5.55 % (2729366)Time elapsed: 0.151 s
% 32.52/5.55 % (2729366)Peak memory usage: 89 MB
% 32.52/5.55 % (2729366)Instructions burned: 265 (million)
% 32.52/5.55 % (2729370)Instruction limit reached!
% 32.52/5.55 % (2729370)------------------------------
% 32.52/5.55 % (2729370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.55 % (2729370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.55 % (2729370)CaDiCaL version: 2.1.3
% 32.52/5.55 % (2729370)Termination reason: Instruction limit
% 32.52/5.55 % (2729370)Termination phase: Saturation
% 32.52/5.55 % (2729370)Time elapsed: 0.046 s
% 32.52/5.55 % (2729370)Peak memory usage: 88 MB
% 32.52/5.55 % (2729370)Instructions burned: 159 (million)
% 32.52/5.55 % (2729371)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=3373371852:i=3256:kws=precedence:bd=preordered:av=off_2987 on theBenchmark for (2987ds/3256Mi)
% 32.52/5.55 % (2729374)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=942369581:i=180:bd=preordered:av=off_2986 on theBenchmark for (2986ds/180Mi)
% 32.52/5.55 % (2729373)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=339886243:i=537:av=off:ss=included_2986 on theBenchmark for (2986ds/537Mi)
% 32.52/5.55 % (2729374)Instruction limit reached!
% 32.52/5.55 % (2729374)------------------------------
% 32.52/5.55 % (2729374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.55 % (2729374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.55 % (2729374)CaDiCaL version: 2.1.3
% 32.52/5.55 % (2729374)Termination reason: Instruction limit
% 32.52/5.55 % (2729374)Termination phase: Saturation
% 32.52/5.55 % (2729374)Time elapsed: 0.045 s
% 32.52/5.55 % (2729374)Peak memory usage: 87 MB
% 32.52/5.55 % (2729374)Instructions burned: 183 (million)
% 32.52/5.55 % (2729378)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=31483250:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2984 on theBenchmark for (2984ds/10307Mi)
% 32.52/5.55 % (2729373)Instruction limit reached!
% 32.52/5.55 % (2729373)------------------------------
% 32.52/5.55 % (2729373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.55 % (2729373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.55 % (2729373)CaDiCaL version: 2.1.3
% 32.52/5.55 % (2729373)Termination reason: Instruction limit
% 32.52/5.55 % (2729373)Termination phase: Saturation
% 32.52/5.55 % (2729373)Time elapsed: 0.243 s
% 32.52/5.55 % (2729373)Peak memory usage: 88 MB
% 32.52/5.55 % (2729373)Instructions burned: 539 (million)
% 32.52/5.55 % (2729380)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=1115541307:i=412:gtgl=4:gtg=exists_all_2982 on theBenchmark for (2982ds/412Mi)
% 32.52/5.55 % (2729380)Instruction limit reached!
% 32.52/5.55 % (2729380)------------------------------
% 32.52/5.55 % (2729380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.29/6.28 % (2729380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.29/6.28 % (2729380)CaDiCaL version: 2.1.3
% 37.29/6.28 % (2729380)Termination reason: Instruction limit
% 37.29/6.28 % (2729380)Termination phase: Saturation
% 37.29/6.28 % (2729380)Time elapsed: 0.184 s
% 37.29/6.28 % (2729380)Peak memory usage: 90 MB
% 37.29/6.28 % (2729380)Instructions burned: 413 (million)
% 37.29/6.28 % (2729382)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=915022799:s2pl=no:i=8478:s2at=4:nm=6_2979 on theBenchmark for (2979ds/8478Mi)
% 37.29/6.28 % (2729350)Instruction limit reached!
% 37.29/6.28 % (2729350)------------------------------
% 37.29/6.28 % (2729350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.29/6.28 % (2729350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.29/6.28 % (2729350)CaDiCaL version: 2.1.3
% 37.29/6.28 % (2729350)Termination reason: Instruction limit
% 37.29/6.28 % (2729350)Termination phase: Saturation
% 37.29/6.28 % (2729350)Time elapsed: 1.810 s
% 37.29/6.28 % (2729350)Peak memory usage: 132 MB
% 37.29/6.28 % (2729350)Instructions burned: 3395 (million)
% 37.29/6.28 % (2729384)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=1020365856: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)
% 37.29/6.28 % (2729382)Refutation not found, incomplete strategy
% 37.29/6.28 % (2729382)------------------------------
% 37.29/6.28 % (2729382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.29/6.28 % (2729382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.29/6.28 % (2729382)CaDiCaL version: 2.1.3
% 37.29/6.28 % (2729382)Termination reason: Refutation not found, incomplete strategy
% 37.29/6.28 % (2729382)Time elapsed: 0.566 s
% 37.29/6.28 % (2729382)Peak memory usage: 128 MB
% 37.29/6.28 % (2729382)Instructions burned: 863 (million)
% 37.29/6.28 % (2729384)Instruction limit reached!
% 37.29/6.28 % (2729384)------------------------------
% 37.29/6.28 % (2729384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.29/6.28 % (2729384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.29/6.28 % (2729384)CaDiCaL version: 2.1.3
% 37.29/6.28 % (2729384)Termination reason: Instruction limit
% 37.29/6.28 % (2729384)Termination phase: Saturation
% 37.29/6.28 % (2729384)Time elapsed: 0.168 s
% 37.29/6.28 % (2729384)Peak memory usage: 90 MB
% 37.29/6.28 % (2729384)Instructions burned: 304 (million)
% 37.29/6.28 % (2729386)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3764349554:st=4:i=720:sd=3:fsr=off:ss=axioms_2971 on theBenchmark for (2971ds/720Mi)
% 37.29/6.28 % (2729386)Refutation not found, incomplete strategy
% 37.29/6.28 % (2729386)------------------------------
% 37.29/6.28 % (2729386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.29/6.28 % (2729386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.29/6.28 % (2729386)CaDiCaL version: 2.1.3
% 37.29/6.28 % (2729386)Termination reason: Refutation not found, incomplete strategy
% 37.29/6.28 % (2729386)Time elapsed: 0.001 s
% 37.29/6.28 % (2729386)Peak memory usage: 87 MB
% 37.29/6.28 % (2729386)Instructions burned: 1 (million)
% 37.29/6.29 % (2729382)------------------------------
% 37.29/6.29 % (2729382)------------------------------
% 37.29/6.29 % (2729371)Instruction limit reached!
% 37.29/6.29 % (2729371)------------------------------
% 37.29/6.29 % (2729371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.29/6.29 % (2729371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.29/6.29 % (2729371)CaDiCaL version: 2.1.3
% 37.29/6.29 % (2729371)Termination reason: Instruction limit
% 37.29/6.29 % (2729371)Termination phase: Saturation
% 37.29/6.29 % (2729371)Time elapsed: 1.751 s
% 37.29/6.29 % (2729371)Peak memory usage: 134 MB
% 37.29/6.29 % (2729371)Instructions burned: 3256 (million)
% 37.29/6.29 % (2729388)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=532968132:i=598:bs=on:bd=preordered:av=off:ss=axioms_2969 on theBenchmark for (2969ds/598Mi)
% 37.29/6.29 % (2729386)------------------------------
% 37.29/6.29 % (2729386)------------------------------
% 37.29/6.29 % (2729389)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2247790062:i=2989:sd=3:ss=axioms:sgt=60_2968 on theBenchmark for (2968ds/2989Mi)
% 57.67/9.20 % (2729391)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=1220386785:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2967 on theBenchmark for (2967ds/1997Mi)
% 57.67/9.20 % (2729388)Instruction limit reached!
% 57.67/9.20 % (2729388)------------------------------
% 57.67/9.20 % (2729388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/9.20 % (2729388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/9.20 % (2729388)CaDiCaL version: 2.1.3
% 57.67/9.20 % (2729388)Termination reason: Instruction limit
% 57.67/9.20 % (2729388)Termination phase: Saturation
% 57.67/9.20 % (2729388)Time elapsed: 0.282 s
% 57.67/9.20 % (2729388)Peak memory usage: 89 MB
% 57.67/9.20 % (2729388)Instructions burned: 599 (million)
% 57.67/9.20 % (2729357)Instruction limit reached!
% 57.67/9.20 % (2729357)------------------------------
% 57.67/9.20 % (2729357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/9.20 % (2729357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/9.20 % (2729357)CaDiCaL version: 2.1.3
% 57.67/9.20 % (2729357)Termination reason: Instruction limit
% 57.67/9.20 % (2729357)Termination phase: Saturation
% 57.67/9.20 % (2729357)Time elapsed: 2.757 s
% 57.67/9.20 % (2729357)Peak memory usage: 133 MB
% 57.67/9.20 % (2729357)Instructions burned: 5209 (million)
% 57.67/9.20 % (2729394)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=17272440:i=2088:bd=preordered:av=off_2965 on theBenchmark for (2965ds/2088Mi)
% 57.67/9.20 % (2729396)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=4247636331:i=1098:nicw=on_2963 on theBenchmark for (2963ds/1098Mi)
% 57.67/9.20 % (2729378)Instruction limit reached!
% 57.67/9.20 % (2729378)------------------------------
% 57.67/9.20 % (2729378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/9.20 % (2729378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/9.20 % (2729378)CaDiCaL version: 2.1.3
% 57.67/9.20 % (2729378)Termination reason: Instruction limit
% 57.67/9.20 % (2729378)Termination phase: Saturation
% 57.67/9.20 % (2729378)Time elapsed: 2.406 s
% 57.67/9.20 % (2729378)Peak memory usage: 135 MB
% 57.67/9.20 % (2729378)Instructions burned: 10309 (million)
% 57.67/9.20 % (2729398)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3801768128:i=433:bd=preordered_2959 on theBenchmark for (2959ds/433Mi)
% 57.67/9.20 % (2729398)Instruction limit reached!
% 57.67/9.20 % (2729398)------------------------------
% 57.67/9.20 % (2729398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/9.20 % (2729398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/9.20 % (2729398)CaDiCaL version: 2.1.3
% 57.67/9.20 % (2729398)Termination reason: Instruction limit
% 57.67/9.20 % (2729398)Termination phase: Saturation
% 57.67/9.20 % (2729398)Time elapsed: 0.127 s
% 57.67/9.20 % (2729398)Peak memory usage: 89 MB
% 57.67/9.20 % (2729398)Instructions burned: 435 (million)
% 57.67/9.20 % (2729396)Instruction limit reached!
% 57.67/9.20 % (2729396)------------------------------
% 57.67/9.20 % (2729396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.67/9.20 % (2729396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.67/9.20 % (2729396)CaDiCaL version: 2.1.3
% 57.67/9.20 % (2729396)Termination reason: Instruction limit
% 57.67/9.20 % (2729396)Termination phase: Saturation
% 57.67/9.20 % (2729396)Time elapsed: 0.468 s
% 57.67/9.20 % (2729396)Peak memory usage: 89 MB
% 57.67/9.20 % (2729396)Instructions burned: 1098 (million)
% 57.67/9.20 % (2729400)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1319509836:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2957 on theBenchmark for (2957ds/2942Mi)
% 57.67/9.20 % (2729401)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2223532213:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2957 on theBenchmark for (2957ds/6922Mi)
% 57.67/9.20 % (2729391)Instruction limit reached!
% 57.67/9.20 % (2729391)------------------------------
% 57.67/9.20 % (2729391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729391)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729391)Termination reason: Instruction limit
% 68.15/10.88 % (2729391)Termination phase: Saturation
% 68.15/10.88 % (2729391)Time elapsed: 1.310 s
% 68.15/10.88 % (2729391)Peak memory usage: 134 MB
% 68.15/10.88 % (2729391)Instructions burned: 1998 (million)
% 68.15/10.88 % (2729404)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=536508712:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2953 on theBenchmark for (2953ds/596Mi)
% 68.15/10.88 % (2729404)Refutation not found, incomplete strategy
% 68.15/10.88 % (2729404)------------------------------
% 68.15/10.88 % (2729404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729404)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729404)Termination reason: Refutation not found, incomplete strategy
% 68.15/10.88 % (2729404)Time elapsed: 0.002 s
% 68.15/10.88 % (2729404)Peak memory usage: 88 MB
% 68.15/10.88 % (2729404)Instructions burned: 2 (million)
% 68.15/10.88 % (2729394)Instruction limit reached!
% 68.15/10.88 % (2729394)------------------------------
% 68.15/10.88 % (2729394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729394)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729394)Termination reason: Instruction limit
% 68.15/10.88 % (2729394)Termination phase: Saturation
% 68.15/10.88 % (2729394)Time elapsed: 1.242 s
% 68.15/10.88 % (2729394)Peak memory usage: 134 MB
% 68.15/10.88 % (2729394)Instructions burned: 2088 (million)
% 68.15/10.88 % (2729389)Instruction limit reached!
% 68.15/10.88 % (2729389)------------------------------
% 68.15/10.88 % (2729389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729389)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729389)Termination reason: Instruction limit
% 68.15/10.88 % (2729389)Termination phase: Saturation
% 68.15/10.88 % (2729389)Time elapsed: 1.633 s
% 68.15/10.88 % (2729389)Peak memory usage: 135 MB
% 68.15/10.88 % (2729389)Instructions burned: 2990 (million)
% 68.15/10.88 % (2729401)Refutation not found, incomplete strategy
% 68.15/10.88 % (2729401)------------------------------
% 68.15/10.88 % (2729401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729401)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729401)Termination reason: Refutation not found, incomplete strategy
% 68.15/10.88 % (2729401)Time elapsed: 0.577 s
% 68.15/10.88 % (2729401)Peak memory usage: 127 MB
% 68.15/10.88 % (2729401)Instructions burned: 862 (million)
% 68.15/10.88 % (2729406)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=3790475966:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2950 on theBenchmark for (2950ds/4123Mi)
% 68.15/10.88 % (2729404)------------------------------
% 68.15/10.88 % (2729404)------------------------------
% 68.15/10.88 % (2729407)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=341920614:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2950 on theBenchmark for (2950ds/16411Mi)
% 68.15/10.88 % (2729410)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=394134670:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2948 on theBenchmark for (2948ds/1670Mi)
% 68.15/10.88 % (2729400)Instruction limit reached!
% 68.15/10.88 % (2729400)------------------------------
% 68.15/10.88 % (2729400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729400)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729400)Termination reason: Instruction limit
% 68.15/10.88 % (2729400)Termination phase: Saturation
% 68.15/10.88 % (2729400)Time elapsed: 0.888 s
% 68.15/10.88 % (2729400)Peak memory usage: 132 MB
% 68.15/10.88 % (2729400)Instructions burned: 2944 (million)
% 68.15/10.88 % (2729412)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=3538547128:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2947 on theBenchmark for (2947ds/1722Mi)
% 68.15/10.88 % (2729401)------------------------------
% 68.15/10.88 % (2729401)------------------------------
% 68.15/10.88 % (2729414)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=3806692894:cts=off:cond=on:i=9530:bs=on:fsd=on_2942 on theBenchmark for (2942ds/9530Mi)
% 68.15/10.88 % (2729412)Instruction limit reached!
% 68.15/10.88 % (2729412)------------------------------
% 68.15/10.88 % (2729412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729412)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729412)Termination reason: Instruction limit
% 68.15/10.88 % (2729412)Termination phase: Saturation
% 68.15/10.88 % (2729412)Time elapsed: 0.749 s
% 68.15/10.88 % (2729412)Peak memory usage: 133 MB
% 68.15/10.88 % (2729412)Instructions burned: 1723 (million)
% 68.15/10.88 % (2729416)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3871770340:st=2:i=4495:sd=10:ss=included_2938 on theBenchmark for (2938ds/4495Mi)
% 68.15/10.88 % (2729410)Instruction limit reached!
% 68.15/10.88 % (2729410)------------------------------
% 68.15/10.88 % (2729410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729410)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729410)Termination reason: Instruction limit
% 68.15/10.88 % (2729410)Termination phase: Saturation
% 68.15/10.88 % (2729410)Time elapsed: 1.251 s
% 68.15/10.88 % (2729410)Peak memory usage: 132 MB
% 68.15/10.88 % (2729410)Instructions burned: 1671 (million)
% 68.15/10.88 % (2729418)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=283402824:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2934 on theBenchmark for (2934ds/4920Mi)
% 68.15/10.88 % (2729416)Instruction limit reached!
% 68.15/10.88 % (2729416)------------------------------
% 68.15/10.88 % (2729416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729416)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729416)Termination reason: Instruction limit
% 68.15/10.88 % (2729416)Termination phase: Saturation
% 68.15/10.88 % (2729416)Time elapsed: 1.169 s
% 68.15/10.88 % (2729416)Peak memory usage: 133 MB
% 68.15/10.88 % (2729416)Instructions burned: 4497 (million)
% 68.15/10.88 % (2729420)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=159797597:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2925 on theBenchmark for (2925ds/2083Mi)
% 68.15/10.88 % (2729406)Instruction limit reached!
% 68.15/10.88 % (2729406)------------------------------
% 68.15/10.88 % (2729406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729406)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729406)Termination reason: Instruction limit
% 68.15/10.88 % (2729406)Termination phase: Saturation
% 68.15/10.88 % (2729406)Time elapsed: 2.712 s
% 68.15/10.88 % (2729406)Peak memory usage: 133 MB
% 68.15/10.88 % (2729406)Instructions burned: 4124 (million)
% 68.15/10.88 % (2729422)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=2071115306:i=4629:av=off:gsp=on_2922 on theBenchmark for (2922ds/4629Mi)
% 68.15/10.88 % (2729420)Instruction limit reached!
% 68.15/10.88 % (2729420)------------------------------
% 68.15/10.88 % (2729420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729420)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729420)Termination reason: Instruction limit
% 68.15/10.88 % (2729420)Termination phase: Saturation
% 68.15/10.88 % (2729420)Time elapsed: 0.623 s
% 68.15/10.88 % (2729420)Peak memory usage: 130 MB
% 68.15/10.88 % (2729420)Instructions burned: 2083 (million)
% 68.15/10.88 % (2729424)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=923188355:i=1258:av=off_2917 on theBenchmark for (2917ds/1258Mi)
% 68.15/10.88 % (2729422)Refutation not found, incomplete strategy
% 68.15/10.88 % (2729422)------------------------------
% 68.15/10.88 % (2729422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729422)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729422)Termination reason: Refutation not found, incomplete strategy
% 68.15/10.88 % (2729422)Time elapsed: 0.621 s
% 68.15/10.88 % (2729422)Peak memory usage: 128 MB
% 68.15/10.88 % (2729422)Instructions burned: 936 (million)
% 68.15/10.88 % (2729424)Instruction limit reached!
% 68.15/10.88 % (2729424)------------------------------
% 68.15/10.88 % (2729424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729424)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729424)Termination reason: Instruction limit
% 68.15/10.88 % (2729424)Termination phase: Saturation
% 68.15/10.88 % (2729424)Time elapsed: 0.304 s
% 68.15/10.88 % (2729424)Peak memory usage: 88 MB
% 68.15/10.88 % (2729424)Instructions burned: 1262 (million)
% 68.15/10.88 % (2729426)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=316132224:i=7343:av=off:ss=included_2913 on theBenchmark for (2913ds/7343Mi)
% 68.15/10.88 % (2729422)------------------------------
% 68.15/10.88 % (2729422)------------------------------
% 68.15/10.88 % (2729428)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2044822762:i=1325:sd=2:ss=axioms:sgt=16_2911 on theBenchmark for (2911ds/1325Mi)
% 68.15/10.88 % (2729418)Instruction limit reached!
% 68.15/10.88 % (2729418)------------------------------
% 68.15/10.88 % (2729418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729418)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729418)Termination reason: Instruction limit
% 68.15/10.88 % (2729418)Termination phase: Saturation
% 68.15/10.88 % (2729418)Time elapsed: 2.472 s
% 68.15/10.88 % (2729418)Peak memory usage: 146 MB
% 68.15/10.88 % (2729418)Instructions burned: 4921 (million)
% 68.15/10.88 % (2729430)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=4269946218:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2908 on theBenchmark for (2908ds/2646Mi)
% 68.15/10.88 % (2729428)Instruction limit reached!
% 68.15/10.88 % (2729428)------------------------------
% 68.15/10.88 % (2729428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.15/10.88 % (2729428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.15/10.88 % (2729428)CaDiCaL version: 2.1.3
% 68.15/10.88 % (2729428)Termination reason: Instruction limit
% 68.15/10.88 % (2729428)Termination phase: Saturation
% 68.15/10.88 % (2729428)Time elapsed: 0.675 s
% 68.15/10.88 % (2729428)Peak memory usage: 90 MB
% 68.15/10.88 % (2729428)Instructions burned: 1326 (million)
% 68.15/10.88 % (2729407)First to succeed.
% 68.15/10.88 % (2729407)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2729321"
% 68.15/10.88 % (2729432)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3139582735:i=1489:sd=2:ep=R:ss=axioms_2903 on theBenchmark for (2903ds/1489Mi)
% 68.15/10.88 % SZS status Satisfiable for theBenchmark
% 68.15/10.88 % SZS output start Saturation.
% See solution above
% 69.90/11.07 % SZS output start Definitions and Model Updates.
% 69.90/11.07 % SZS output end Definitions and Model Updates.
% 69.90/11.07 % (2729407)------------------------------
% 69.90/11.07 % (2729407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.90/11.07 % (2729407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.90/11.07 % (2729407)CaDiCaL version: 2.1.3
% 69.90/11.07 % (2729407)Termination reason: Satisfiable
% 69.90/11.07 % (2729407)Time elapsed: 4.644 s
% 69.90/11.07 % (2729407)Peak memory usage: 154 MB
% 69.90/11.07 % (2729407)Instructions burned: 7031 (million)
% 69.90/11.07 % (2729407)------------------------------
% 69.90/11.07 % (2729407)------------------------------
% 69.90/11.07 % (2729321)Success in time 10.01 s
% 69.90/11.07 % Vampire exiting
%------------------------------------------------------------------------------