%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : MSC014-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:05:46 PM UTC 2026
% Result : Satisfiable 1.48s 0.79s
% Output : Saturation 1.48s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u901,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n0,X0,n1,sK1_exists_f_Z(n1,n0,X0,n1)),true) ).
cnf(u1225,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X2,n0),true) ).
cnf(u338,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X1,n1),true) ).
cnf(u56,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(n1,X1,n0,X0,sK1_exists_f_Z(n1,X1,n0,X0)),true),true) ).
cnf(u1184,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u779,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(X1,n1,X0,n1,sK1_exists_f_Z(X1,n1,X0,n1)),true),true) ).
cnf(u3223,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(n0,X0),true) ).
cnf(u2082,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u2885,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X1,n0),true) ).
cnf(u1178,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X3,n1),true) ).
cnf(u2027,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(n1,X3),true) ).
cnf(u1177,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(n1,X3),true) ).
cnf(u3483,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u3228,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X2,n0),true) ).
cnf(u1324,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u3255,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u3175,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(n1,X3),true) ).
cnf(u1979,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n1,X0,n0,sK1_exists_f_Z(n0,n1,X0,n0)),true) ).
cnf(u2357,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u1220,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(n1,X0),true) ).
cnf(u2893,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u3174,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X2,n0),true) ).
cnf(u1742,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,X0,n1,n0,sK1_exists_f_Z(n1,X0,n1,n0)),true) ).
cnf(u2328,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u1741,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,X0,n1,n1,sK1_exists_f_Z(n1,X0,n1,n1)),true) ).
cnf(u336,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X0,n1),true) ).
cnf(u2389,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u2887,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X2,n1),true) ).
cnf(u2784,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n0,n1,X0,sK1_exists_f_Z(n0,n0,n1,X0)),true) ).
cnf(u2021,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(n0,X0),true) ).
cnf(u2268,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X1,n1),true) ).
cnf(u70,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n1,X0,n0,sK1_exists_f_Z(n1,n1,X0,n0)),true) ).
cnf(u3169,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(n0,X0),true) ).
cnf(u4270,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n0,n1,n0,sK1_exists_f_Z(X0,n0,n1,n0)),true) ).
cnf(u4269,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n0,n1,n1,sK1_exists_f_Z(X0,n0,n1,n1)),true) ).
cnf(u2113,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u415,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u914,axiom,
true = f(n1,n0,n1,n0,sK1_exists_f_Z(n1,n0,n1,n0)) ).
cnf(u2888,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(n0,X3),true) ).
cnf(u2895,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u80,axiom,
true = f(n1,n1,n1,n1,sK1_exists_f_Z(n1,n1,n1,n1)) ).
cnf(u3972,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n1,n1,n0,sK1_exists_f_Z(X0,n1,n1,n0)),true) ).
cnf(u1172,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X0,n1),true) ).
cnf(u2084,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u395,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u43,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(equalish(X2,X2),true,f(X2,X1,X0,n1,sK1_exists_f_Z(X2,X1,X0,n1)),true),true),true) ).
cnf(u1456,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u2078,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X2,n1),true) ).
cnf(u25,axiom,
true = ifeq2(f(X0,n0,X1,X2,X3),true,ifeq2(f(X4,n0,X5,X6,X3),true,true,true),true) ).
cnf(u397,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u3706,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,X0,n1,n0,sK1_exists_f_Z(n0,X0,n1,n0)),true) ).
cnf(u951,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u2140,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u67,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n1,n1,X0,sK1_exists_f_Z(n1,n1,n1,X0)),true) ).
cnf(u391,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u416,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u39,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(equalish(X2,X2),true,f(X2,n1,X1,X0,sK1_exists_f_Z(X2,n1,X1,X0)),true),true),true) ).
cnf(u69,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n1,X0,n1,sK1_exists_f_Z(n1,n1,X0,n1)),true) ).
cnf(u26,axiom,
true = ifeq2(f(X0,n1,X1,X2,X3),true,ifeq2(f(X4,n1,X5,X6,X3),true,true,true),true) ).
cnf(u184,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u2889,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X3,n0),true) ).
cnf(u1651,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u28,axiom,
true = ifeq2(f(n1,X0,X1,X2,X3),true,ifeq2(f(n1,X4,X5,X6,X3),true,true,true),true) ).
cnf(u153,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(n1,X1),true) ).
cnf(u19,axiom,
b = ifeq(equalish(n1,n0),true,a,b) ).
cnf(u22,axiom,
true = ifeq2(f(X0,X1,X2,n1,X3),true,ifeq2(f(X4,X5,X6,n1,X3),true,true,true),true) ).
cnf(u2086,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u21,axiom,
true = ifeq2(f(X0,X1,X2,n0,X3),true,ifeq2(f(X4,X5,X6,n0,X3),true,true,true),true) ).
cnf(u2845,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u829,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u15,axiom,
true = ifeq2(f(X0,X1,X2,X3,X4),true,ifeq2(f(X5,X6,X7,X8,X4),true,equalish(X5,X0),true),true) ).
cnf(u2079,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(n0,X3),true) ).
cnf(ifeq_axiom_001,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u3289,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(ifeq_axiom,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u1257,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u1235,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u913,axiom,
true = f(n1,n0,n1,n1,sK1_exists_f_Z(n1,n0,n1,n1)) ).
cnf(u2917,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u2030,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u1252,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u3229,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(n0,X3),true) ).
cnf(u106,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X0,n1),true) ).
cnf(u1233,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u1993,axiom,
true = f(n0,n1,n1,n0,sK1_exists_f_Z(n0,n1,n1,n0)) ).
cnf(u108,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X1,n1),true) ).
cnf(u2026,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X2,n1),true) ).
cnf(u2840,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u3224,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X0,n0),true) ).
cnf(u1327,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u1826,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,X0,n0,n0,sK1_exists_f_Z(n1,X0,n0,n0)),true) ).
cnf(u3171,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(n0,X1),true) ).
cnf(u2954,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u1186,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u2925,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u2836,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u3173,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(n0,X2),true) ).
cnf(u1978,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n1,X0,n1,sK1_exists_f_Z(n0,n1,X0,n1)),true) ).
cnf(u1332,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u3176,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X3,n1),true) ).
cnf(u2110,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u2272,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X3,n1),true) ).
cnf(u1326,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u2145,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u3170,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X0,n0),true) ).
cnf(u2266,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X0,n0),true) ).
cnf(u596,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(n0,X1,X0,n1,sK1_exists_f_Z(n0,X1,X0,n1)),true),true) ).
cnf(u1303,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(X1,n0,n1,X0,sK1_exists_f_Z(X1,n0,n1,X0)),true),true) ).
cnf(u994,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(n0,X3),true) ).
cnf(u2898,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u2237,axiom,
true = f(n0,n1,n0,n0,sK1_exists_f_Z(n0,n1,n0,n0)) ).
cnf(u386,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(n1,X1),true) ).
cnf(u780,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(X1,n1,X0,n0,sK1_exists_f_Z(X1,n1,X0,n0)),true),true) ).
cnf(u2360,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u154,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X1,n1),true) ).
cnf(u4704,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(X1,X0,n0,n1,sK1_exists_f_Z(X1,X0,n0,n1)),true),true) ).
cnf(u216,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u990,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(n0,X1),true) ).
cnf(u447,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u1019,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u156,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X2,n1),true) ).
cnf(u112,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u3613,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u4374,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n0,n0,n1,sK1_exists_f_Z(X0,n0,n0,n1)),true) ).
cnf(u900,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n0,n0,X0,sK1_exists_f_Z(n1,n0,n0,X0)),true) ).
cnf(u592,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(n0,n1,X1,X0,sK1_exists_f_Z(n0,n1,X1,X0)),true),true) ).
cnf(u340,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X2,n0),true) ).
cnf(u190,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u942,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(n0,X1),true) ).
cnf(u105,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(n1,X0),true) ).
cnf(u2335,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u3705,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,X0,n1,n1,sK1_exists_f_Z(n0,X0,n1,n1)),true) ).
cnf(u2322,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X1,n1),true) ).
cnf(u2321,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(n1,X1),true) ).
cnf(u1825,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,X0,n0,n1,sK1_exists_f_Z(n1,X0,n0,n1)),true) ).
cnf(u2324,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X2,n0),true) ).
cnf(u58,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(n1,X1,X0,n0,sK1_exists_f_Z(n1,X1,X0,n0)),true),true) ).
cnf(u1992,axiom,
true = f(n0,n1,n1,n1,sK1_exists_f_Z(n0,n1,n1,n1)) ).
cnf(u2089,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u57,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(n1,X1,X0,n1,sK1_exists_f_Z(n1,X1,X0,n1)),true),true) ).
cnf(u1223,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X1,n0),true) ).
cnf(u3045,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(X1,X0,n1,n0,sK1_exists_f_Z(X1,X0,n1,n0)),true),true) ).
cnf(u3799,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,X0,n0,n0,sK1_exists_f_Z(n0,X0,n0,n0)),true) ).
cnf(u3227,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(n0,X2),true) ).
cnf(u81,axiom,
true = f(n1,n1,n1,n0,sK1_exists_f_Z(n1,n1,n1,n0)) ).
cnf(u54,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(n1,n0,X1,X0,sK1_exists_f_Z(n1,n0,X1,X0)),true),true) ).
cnf(u2116,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u4375,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n0,n0,n0,sK1_exists_f_Z(X0,n0,n0,n0)),true) ).
cnf(u53,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(n1,n1,X1,X0,sK1_exists_f_Z(n1,n1,X1,X0)),true),true) ).
cnf(u2393,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u40,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(equalish(X2,X2),true,f(X2,n0,X1,X0,sK1_exists_f_Z(X2,n0,X1,X0)),true),true),true) ).
cnf(u946,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(n1,X3),true) ).
cnf(u3232,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u993,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X2,n1),true) ).
cnf(u389,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X2,n0),true) ).
cnf(u1175,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(n0,X2),true) ).
cnf(u3226,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X1,n0),true) ).
cnf(u1306,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(X1,n0,X0,n0,sK1_exists_f_Z(X1,n0,X0,n0)),true),true) ).
cnf(u4075,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n1,n0,n0,sK1_exists_f_Z(X0,n1,n0,n0)),true) ).
cnf(u2884,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(n0,X1),true) ).
cnf(u989,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X0,n1),true) ).
cnf(u1224,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(n0,X2),true) ).
cnf(u945,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X2,n1),true) ).
cnf(u2920,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u3178,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u2799,axiom,
true = f(n0,n0,n1,n1,sK1_exists_f_Z(n0,n0,n1,n1)) ).
cnf(u1304,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(X1,n0,n0,X0,sK1_exists_f_Z(X1,n0,n0,X0)),true),true) ).
cnf(u941,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X0,n1),true) ).
cnf(u166,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u715,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u2833,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(n1,X2),true) ).
cnf(u3225,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(n0,X1),true) ).
cnf(u995,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X3,n0),true) ).
cnf(u339,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(n0,X2),true) ).
cnf(u1180,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u2025,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(n1,X2),true) ).
cnf(u341,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(n1,X3),true) ).
cnf(u3236,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u1977,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n1,n0,X0,sK1_exists_f_Z(n0,n1,n0,X0)),true) ).
cnf(u991,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X1,n0),true) ).
cnf(u947,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u1055,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u2265,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(n0,X0),true) ).
cnf(u399,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u2330,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u943,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X1,n0),true) ).
cnf(u385,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X0,n1),true) ).
cnf(u2332,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u418,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u448,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u2326,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u186,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u27,axiom,
true = ifeq2(f(n0,X0,X1,X2,X3),true,ifeq2(f(n0,X4,X5,X6,X3),true,true,true),true) ).
cnf(u1022,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u223,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u571,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u2023,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(n1,X1),true) ).
cnf(u2831,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(n0,X1),true) ).
cnf(u337,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(n1,X1),true) ).
cnf(u157,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(n0,X3),true) ).
cnf(u2080,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X3,n0),true) ).
cnf(u182,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u23,axiom,
true = ifeq2(f(X0,X1,n0,X2,X3),true,ifeq2(f(X4,X5,n0,X6,X3),true,true,true),true) ).
cnf(u2323,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(n0,X2),true) ).
cnf(u3548,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u2074,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X0,n0),true) ).
cnf(u388,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(n0,X2),true) ).
cnf(u9,axiom,
true = ifeq2(f(X0,X1,X2,X3,X4),true,ifeq2(f(X5,X6,X7,X8,X4),true,equalish(X8,X3),true),true) ).
cnf(u2028,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u2834,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X2,n1),true) ).
cnf(n0_and_n1_reflexive_1,axiom,
equalish(n0,n0) = true ).
cnf(u2076,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X1,n1),true) ).
cnf(u162,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u2354,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u2353,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u2517,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u164,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u5,axiom,
true = equalish(n1,n1) ).
cnf(u2830,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X0,n0),true) ).
cnf(u3971,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n1,n1,n1,sK1_exists_f_Z(X0,n1,n1,n1)),true) ).
cnf(u120,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u594,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(n0,X1,n1,X0,sK1_exists_f_Z(n0,X1,n1,X0)),true),true) ).
cnf(u3287,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u593,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(n0,n0,X1,X0,sK1_exists_f_Z(n0,n0,X1,X0)),true),true) ).
cnf(u2949,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u114,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u116,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u3259,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u3230,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u2886,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(n1,X2),true) ).
cnf(u2024,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X1,n1),true) ).
cnf(u778,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(X1,n1,n0,X0,sK1_exists_f_Z(X1,n1,n0,X0)),true),true) ).
cnf(u2034,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u2842,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u1521,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u1222,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(n0,X1),true) ).
cnf(u3239,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u1221,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X0,n1),true) ).
cnf(u2142,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u3182,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u2838,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u1231,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u3295,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u1171,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(n1,X0),true) ).
cnf(u1174,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X1,n0),true) ).
cnf(u1173,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(n0,X1),true) ).
cnf(u4074,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n1,n0,n1,sK1_exists_f_Z(X0,n1,n0,n1)),true) ).
cnf(u1146,axiom,
true = f(n1,n0,n0,n0,sK1_exists_f_Z(n1,n0,n0,n0)) ).
cnf(u3044,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(X1,X0,n1,n1,sK1_exists_f_Z(X1,X0,n1,n1)),true),true) ).
cnf(u1176,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X2,n0),true) ).
cnf(u1145,axiom,
true = f(n1,n0,n0,n1,sK1_exists_f_Z(n1,n0,n0,n1)) ).
cnf(u988,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(n1,X0),true) ).
cnf(u595,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(n0,X1,n0,X0,sK1_exists_f_Z(n0,X1,n0,X0)),true),true) ).
cnf(u944,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(n1,X2),true) ).
cnf(u992,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(n1,X2),true) ).
cnf(u2267,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(n1,X1),true) ).
cnf(u2269,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(n0,X2),true) ).
cnf(u899,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n0,n1,X0,sK1_exists_f_Z(n1,n0,n1,X0)),true) ).
cnf(u1182,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u940,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(n1,X0),true) ).
cnf(u390,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(n0,X3),true) ).
cnf(u2800,axiom,
true = f(n0,n0,n1,n0,sK1_exists_f_Z(n0,n0,n1,n0)) ).
cnf(u2037,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u155,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(n1,X2),true) ).
cnf(u2832,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X1,n0),true) ).
cnf(u346,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u158,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X3,n0),true) ).
cnf(u1023,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u2952,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u348,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u2883,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X0,n0),true) ).
cnf(u214,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u151,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(n1,X0),true) ).
cnf(u342,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X3,n1),true) ).
cnf(u2882,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(n0,X0),true) ).
cnf(u107,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(n1,X1),true) ).
cnf(u1003,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u110,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X2,n1),true) ).
cnf(u109,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(n1,X2),true) ).
cnf(u2325,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(n0,X3),true) ).
cnf(u2835,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(n1,X3),true) ).
cnf(u455,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u2958,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u955,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u2891,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u38,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(equalish(X2,X2),true,f(n0,X2,X1,X0,sK1_exists_f_Z(n0,X2,X1,X0)),true),true),true) ).
cnf(u2274,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u2785,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n0,n0,X0,sK1_exists_f_Z(n0,n0,n0,X0)),true) ).
cnf(u37,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(equalish(X2,X2),true,f(n1,X2,X1,X0,sK1_exists_f_Z(n1,X2,X1,X0)),true),true),true) ).
cnf(u2276,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u55,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(n1,X1,n1,X0,sK1_exists_f_Z(n1,X1,n1,X0)),true),true) ).
cnf(u42,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(equalish(X2,X2),true,f(X2,X1,n0,X0,sK1_exists_f_Z(X2,X1,n0,X0)),true),true),true) ).
cnf(u393,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u2073,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(n0,X0),true) ).
cnf(u41,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(equalish(X2,X2),true,f(X2,X1,n1,X0,sK1_exists_f_Z(X2,X1,n1,X0)),true),true),true) ).
cnf(u44,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(equalish(X2,X2),true,f(X2,X1,X0,n0,sK1_exists_f_Z(X2,X1,X0,n0)),true),true),true) ).
cnf(u387,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X1,n1),true) ).
cnf(u2108,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u1976,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n1,n1,X0,sK1_exists_f_Z(n0,n1,n1,X0)),true) ).
cnf(u2582,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u902,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n0,X0,n0,sK1_exists_f_Z(n1,n0,X0,n0)),true) ).
cnf(u3418,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u953,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u68,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n1,n0,X0,sK1_exists_f_Z(n1,n1,n0,X0)),true) ).
cnf(u1226,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(n0,X3),true) ).
cnf(u2922,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u24,axiom,
true = ifeq2(f(X0,X1,n1,X2,X3),true,ifeq2(f(X4,X5,n1,X6,X3),true,true,true),true) ).
cnf(u4705,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(X1,X0,n0,n0,sK1_exists_f_Z(X1,X0,n0,n0)),true),true) ).
cnf(u1001,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u3185,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u2712,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u997,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u949,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u3262,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u17,axiom,
b = ifeq(equalish(n0,n1),true,a,b) ).
cnf(u650,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u777,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(X1,n1,n1,X0,sK1_exists_f_Z(X1,n1,n1,X0)),true),true) ).
cnf(u2829,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(n0,X0),true) ).
cnf(u3798,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,X0,n0,n1,sK1_exists_f_Z(n0,X0,n0,n1)),true) ).
cnf(u3180,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u3143,axiom,
true = f(n0,n0,n0,n0,sK1_exists_f_Z(n0,n0,n0,n0)) ).
cnf(u1060,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u1253,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u1051,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u3257,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u1054,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u160,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u999,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u1250,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u3142,axiom,
true = f(n0,n0,n0,n1,sK1_exists_f_Z(n0,n0,n0,n1)) ).
cnf(u1227,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u3234,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u1027,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u2022,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X0,n0),true) ).
cnf(u2270,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X2,n0),true) ).
cnf(u2281,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u450,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u2320,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X0,n0),true) ).
cnf(u422,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u218,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u3172,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X1,n0),true) ).
cnf(u1305,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(X1,n0,X0,n1,sK1_exists_f_Z(X1,n0,X0,n1)),true),true) ).
cnf(u2787,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n0,X0,n0,sK1_exists_f_Z(n0,n0,X0,n0)),true) ).
cnf(u1586,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u2278,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(goal,negated_conjecture,
a != b ).
cnf(u13,axiom,
true = ifeq2(f(X0,X1,X2,X3,X4),true,ifeq2(f(X5,X6,X7,X8,X4),true,equalish(X6,X1),true),true) ).
cnf(u11,axiom,
true = ifeq2(f(X0,X1,X2,X3,X4),true,ifeq2(f(X5,X6,X7,X8,X4),true,equalish(X7,X2),true),true) ).
cnf(u2075,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(n1,X1),true) ).
cnf(u335,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(n1,X0),true) ).
cnf(u7,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(equalish(X2,X2),true,ifeq2(equalish(X3,X3),true,f(X3,X2,X1,X0,sK1_exists_f_Z(X3,X2,X1,X0)),true),true),true),true) ).
cnf(u2319,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(n0,X0),true) ).
cnf(u2271,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(n1,X3),true) ).
cnf(u2236,axiom,
true = f(n0,n1,n0,n1,sK1_exists_f_Z(n0,n1,n0,n1)) ).
cnf(u2647,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u2077,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(n1,X2),true) ).
cnf(u2386,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u2385,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u384,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(n1,X0),true) ).
cnf(u309,axiom,
true = f(n1,n1,n0,n0,sK1_exists_f_Z(n1,n1,n0,n0)) ).
cnf(u2032,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u152,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X0,n1),true) ).
cnf(u2786,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n0,X0,n1,sK1_exists_f_Z(n0,n0,X0,n1)),true) ).
cnf(u350,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u3291,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u597,axiom,
true = ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,f(n0,X1,X0,n0,sK1_exists_f_Z(n0,X1,X0,n0)),true),true) ).
cnf(u118,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u2149,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u1229,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u308,axiom,
true = f(n1,n1,n0,n1,sK1_exists_f_Z(n1,n1,n0,n1)) ).
cnf(u111,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(n1,X3),true) ).
cnf(u344,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MSC014-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n026.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 17:44:57 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.45 Running first-order model finding
% 0.12/0.45 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.48/0.79 % (3095401)Will run a generic schedule for satisfiability detection.
% 1.48/0.79 % (3095406)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=407102242_2999 on theBenchmark for (2999ds/0Mi)
% 1.48/0.79 % TRYING [1]
% 1.48/0.79 % TRYING [2]
% 1.48/0.79 % TRYING [3]
% 1.48/0.79 % (3095407)% WARNING: option uhcvi not known.
% 1.48/0.79 % (3095408)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4246198160:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.48/0.79 % (3095409)dis+10_1_sil=32000:sp=arity:random_seed=4066066026:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.48/0.79 % (3095410)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3919033696:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.48/0.79 % (3095407)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3688517421:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.48/0.79 % (3095412)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1419325903:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.48/0.79 % (3095411)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=217817061:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.48/0.79 % TRYING [4]
% 1.48/0.79 % TRYING [5]
% 1.48/0.79 % (3095409)Instruction limit reached!
% 1.48/0.79 % (3095409)------------------------------
% 1.48/0.79 % (3095409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.79 % (3095409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.79 % (3095409)CaDiCaL version: 2.1.3
% 1.48/0.79 % (3095409)Termination reason: Instruction limit
% 1.48/0.79 % (3095409)Termination phase: Saturation
% 1.48/0.79 % (3095409)Time elapsed: 0.093 s
% 1.48/0.79 % (3095409)Peak memory usage: 11 MB
% 1.48/0.79 % (3095409)Instructions burned: 104 (million)
% 1.48/0.79 % (3095410)Instruction limit reached!
% 1.48/0.79 % (3095410)------------------------------
% 1.48/0.79 % (3095410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.79 % (3095410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.79 % (3095410)CaDiCaL version: 2.1.3
% 1.48/0.79 % (3095410)Termination reason: Instruction limit
% 1.48/0.79 % (3095410)Termination phase: Saturation
% 1.48/0.79 % (3095410)Time elapsed: 0.107 s
% 1.48/0.79 % (3095410)Peak memory usage: 11 MB
% 1.48/0.79 % (3095410)Instructions burned: 117 (million)
% 1.48/0.79 % (3095420)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3233857774:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.48/0.79 % (3095411)Instruction limit reached!
% 1.48/0.79 % (3095411)------------------------------
% 1.48/0.79 % (3095411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.79 % (3095411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.79 % (3095411)CaDiCaL version: 2.1.3
% 1.48/0.79 % (3095411)Termination reason: Instruction limit
% 1.48/0.79 % (3095411)Termination phase: Saturation
% 1.48/0.79 % (3095411)Time elapsed: 0.117 s
% 1.48/0.79 % (3095411)Peak memory usage: 11 MB
% 1.48/0.79 % (3095411)Instructions burned: 131 (million)
% 1.48/0.79 % TRYING [1]
% 1.48/0.79 % TRYING [2]
% 1.48/0.79 % TRYING [3]
% 1.48/0.79 % (3095421)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1323361503:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.48/0.79 % (3095412)Instruction limit reached!
% 1.48/0.79 % (3095412)------------------------------
% 1.48/0.79 % (3095412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.79 % (3095412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.79 % (3095412)CaDiCaL version: 2.1.3
% 1.48/0.79 % (3095412)Termination reason: Instruction limit
% 1.48/0.79 % (3095412)Termination phase: Saturation
% 1.48/0.79 % (3095412)Time elapsed: 0.149 s
% 1.48/0.79 % (3095412)Peak memory usage: 12 MB
% 1.48/0.79 % (3095412)Instructions burned: 160 (million)
% 1.48/0.79 % (3095423)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1255397528:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.48/0.79 % (3095425)ott-21_1_sil=16000:fs=off:random_seed=2083043988:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.48/0.79 % TRYING [4]
% 1.48/0.79 % TRYING [6]
% 1.48/0.79 % (3095421)Instruction limit reached!
% 1.48/0.79 % (3095421)------------------------------
% 1.48/0.79 % (3095421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.79 % (3095421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.79 % (3095421)CaDiCaL version: 2.1.3
% 1.48/0.79 % (3095421)Termination reason: Instruction limit
% 1.48/0.79 % (3095421)Termination phase: Saturation
% 1.48/0.79 % (3095421)Time elapsed: 0.120 s
% 1.48/0.79 % (3095421)Peak memory usage: 12 MB
% 1.48/0.79 % (3095421)Instructions burned: 132 (million)
% 1.48/0.79 % (3095408) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3095401-3095408"...
% 1.48/0.79 % (3095408)...printing done.
% 1.48/0.79 % SZS status Satisfiable for theBenchmark
% 1.48/0.79 % SZS output start Saturation.
% See solution above
% 1.48/0.80 % SZS output start Definitions and Model Updates.
% 1.48/0.80 % SZS output end Definitions and Model Updates.
% 1.48/0.80 % (3095408)------------------------------
% 1.48/0.80 % (3095408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.48/0.80 % (3095408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.48/0.80 % (3095408)CaDiCaL version: 2.1.3
% 1.48/0.80 % (3095408)Termination reason: Satisfiable
% 1.48/0.80 % (3095408)Time elapsed: 0.286 s
% 1.48/0.80 % (3095408)Peak memory usage: 13 MB
% 1.48/0.80 % (3095408)Instructions burned: 317 (million)
% 1.48/0.80 % (3095401)Success in time 0.33 s
% 1.48/0.80 % Vampire exiting
%------------------------------------------------------------------------------