%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n016.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:04:58 PM UTC 2026
% Result : Satisfiable 9.70s 2.24s
% Output : Saturation 10.34s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1911,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X0,n0),true) ).
cnf(u1179,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X1,n0),true) ).
cnf(u1808,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X0,n0),true) ).
cnf(u934,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(n1,X2),true) ).
cnf(u3214,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u1182,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(n0,X3),true) ).
cnf(u2018,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(n0,X2),true) ).
cnf(u3245,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u4020,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u1916,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(n0,X3),true) ).
cnf(u63,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(u50,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(u1178,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(n0,X1),true) ).
cnf(u3269,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u2971,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u1177,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X0,n1),true) ).
cnf(u681,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(n1,X2),true) ).
cnf(u1324,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(n0,X2),true) ).
cnf(u3069,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u525,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n1,n0,n1,sK1_exists_f_Z(X0,n1,n0,n1)),true) ).
cnf(u833,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X0,n1),true) ).
cnf(u3317,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u744,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X1,n1),true) ).
cnf(u2936,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u2908,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u3502,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u1320,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(n1,X0),true) ).
cnf(u1470,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u3139,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u2442,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(n0,X3),true) ).
cnf(u3174,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u3414,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u3113,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u3036,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u49,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(u1713,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u2021,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X3,n1),true) ).
cnf(u3606,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u330,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,X0,n1,n0,sK1_exists_f_Z(n0,X0,n1,n0)),true) ).
cnf(u2302,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(n1,X2),true) ).
cnf(u683,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(n1,X3),true) ).
cnf(u3064,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u3226,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u3096,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u835,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X1,n1),true) ).
cnf(u2161,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X2,n0),true) ).
cnf(u2017,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X1,n0),true) ).
cnf(u2940,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u408,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n0,n0,n1,sK1_exists_f_Z(X0,n0,n0,n1)),true) ).
cnf(u250,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n0,X0,n0,sK1_exists_f_Z(n1,n0,X0,n0)),true) ).
cnf(u91,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(u3218,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u1646,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(n1,X3),true) ).
cnf(u2157,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X0,n0),true) ).
cnf(u1645,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X2,n0),true) ).
cnf(u4412,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u171,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n1,n0,X0,sK1_exists_f_Z(n1,n1,n0,X0)),true) ).
cnf(u87,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(u74,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(u3070,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u1912,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(n1,X1),true) ).
cnf(u73,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(u46,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(u2303,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X2,n1),true) ).
cnf(u45,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(u678,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X0,n1),true) ).
cnf(u4013,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u32,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(u677,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(n1,X0),true) ).
cnf(u228,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n0,n0,X0,sK1_exists_f_Z(n1,n0,n0,X0)),true) ).
cnf(u505,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n0,n1,n1,sK1_exists_f_Z(X0,n0,n1,n1)),true) ).
cnf(u1711,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X2,n1),true) ).
cnf(u4153,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u153,axiom,
true = ifeq2(f(n1,X0,X1,X2,X3),true,ifeq2(f(n1,X4,X5,X6,X3),true,true,true),true) ).
cnf(u19,axiom,
b = ifeq(equalish(n1,n0),true,a,b) ).
cnf(u1466,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X1,n0),true) ).
cnf(u4244,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u937,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X3,n0),true) ).
cnf(u2906,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u2015,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X0,n0),true) ).
cnf(u3099,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n0,n1,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(u149,axiom,
true = ifeq2(f(X0,X1,X2,n1,X3),true,ifeq2(f(X4,X5,X6,n1,X3),true,true,true),true) ).
cnf(u2162,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(n0,X3),true) ).
cnf(u1325,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X2,n0),true) ).
cnf(ifeq_axiom_001,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u933,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X1,n1),true) ).
cnf(u3147,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u4517,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(ifeq_axiom,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u1037,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X2,n0),true) ).
cnf(u3156,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u1038,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(n0,X3),true) ).
cnf(u3121,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u1035,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X1,n1),true) ).
cnf(u3146,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u2873,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u585,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n1,n1,n1,sK1_exists_f_Z(X0,n1,n1,n1)),true) ).
cnf(u3101,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u2973,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u3221,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u1467,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(n0,X2),true) ).
cnf(u1034,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(n1,X1),true) ).
cnf(u1982,axiom,
true = f(n0,n0,n0,n1,sK1_exists_f_Z(n0,n0,n0,n1)) ).
cnf(u3098,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u3068,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u1033,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X0,n1),true) ).
cnf(u1469,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(n0,X3),true) ).
cnf(u2300,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(n0,X1),true) ).
cnf(u2967,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u935,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X2,n1),true) ).
cnf(u832,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(n1,X0),true) ).
cnf(u3333,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u2969,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u804,axiom,
true = f(n1,n1,n0,n1,sK1_exists_f_Z(n1,n1,n0,n1)) ).
cnf(u1465,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(n0,X1),true) ).
cnf(u1144,axiom,
true = f(n1,n0,n1,n0,sK1_exists_f_Z(n1,n0,n1,n0)) ).
cnf(u2304,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(n0,X3),true) ).
cnf(u3170,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u2266,axiom,
true = f(n0,n0,n1,n0,sK1_exists_f_Z(n0,n0,n1,n0)) ).
cnf(u174,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n1,X0,n1,sK1_exists_f_Z(n1,n1,X0,n1)),true) ).
cnf(u3125,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u173,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n1,X0,n0,sK1_exists_f_Z(n1,n1,X0,n0)),true) ).
cnf(u936,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(n0,X3),true) ).
cnf(u748,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u2020,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(n1,X3),true) ).
cnf(u4160,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u3985,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u3003,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u154,axiom,
true = ifeq2(f(n0,X0,X1,X2,X3),true,ifeq2(f(n0,X4,X5,X6,X3),true,true,true),true) ).
cnf(u1910,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(n0,X0),true) ).
cnf(u3201,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u2158,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(n1,X1),true) ).
cnf(u156,axiom,
true = ifeq2(f(X0,n0,X1,X2,X3),true,ifeq2(f(X4,n0,X5,X6,X3),true,true,true),true) ).
cnf(u2016,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(n0,X1),true) ).
cnf(u4419,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u150,axiom,
true = ifeq2(f(X0,X1,X2,n0,X3),true,ifeq2(f(X4,X5,X6,n0,X3),true,true,true),true) ).
cnf(u310,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n1,X0,n0,sK1_exists_f_Z(n0,n1,X0,n0)),true) ).
cnf(u4139,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u2974,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u2907,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u682,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X2,n1),true) ).
cnf(u75,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(u4321,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u1609,axiom,
true = f(n0,n1,n0,n1,sK1_exists_f_Z(n0,n1,n0,n1)) ).
cnf(u290,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,X0,n0,n1,sK1_exists_f_Z(n0,X0,n0,n1)),true) ).
cnf(u102,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(u101,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(u2441,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X2,n0),true) ).
cnf(u3034,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u88,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(u1706,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(n0,X0),true) ).
cnf(u1464,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X0,n1),true) ).
cnf(u2124,axiom,
true = f(n0,n1,n0,n0,sK1_exists_f_Z(n0,n1,n0,n0)) ).
cnf(u60,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(u838,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(n1,X3),true) ).
cnf(u3227,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u2437,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X0,n0),true) ).
cnf(u1707,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X0,n0),true) ).
cnf(u4425,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u2938,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u2968,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u328,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n0,n1,X0,sK1_exists_f_Z(n0,n0,n1,X0)),true) ).
cnf(u2877,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u47,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(u1712,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(n1,X3),true) ).
cnf(u34,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(u837,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X2,n0),true) ).
cnf(u3179,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u3150,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u1322,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(n0,X1),true) ).
cnf(u3212,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u3181,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u1811,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(n1,X2),true) ).
cnf(u932,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(n1,X1),true) ).
cnf(u3301,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u3097,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u77,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(u3131,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u3102,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u3486,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u679,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(n0,X1),true) ).
cnf(u3164,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u3133,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u3001,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u3005,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u3158,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u680,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X1,n0),true) ).
cnf(u2872,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u3130,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u1915,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X2,n1),true) ).
cnf(u3238,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u2972,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u2999,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u839,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X3,n1),true) ).
cnf(u3236,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u1323,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X1,n0),true) ).
cnf(u4502,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u3390,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u2871,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u2298,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(n0,X0),true) ).
cnf(u427,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n0,n1,n0,sK1_exists_f_Z(X0,n0,n1,n0)),true) ).
cnf(u3509,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u3035,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u3000,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u1321,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X0,n1),true) ).
cnf(u64,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(u33,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(u230,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,X0,n0,n0,sK1_exists_f_Z(n1,X0,n0,n0)),true) ).
cnf(u2876,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u36,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(u3196,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u2443,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u4608,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u1814,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u1642,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(n1,X1),true) ).
cnf(u2408,axiom,
true = f(n0,n0,n0,n0,sK1_exists_f_Z(n0,n0,n0,n0)) ).
cnf(u30,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(u1641,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X0,n0),true) ).
cnf(u3177,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) ).
cnf(u29,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(u209,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n0,X0,n1,sK1_exists_f_Z(n1,n0,X0,n1)),true) ).
cnf(u309,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n1,n1,X0,sK1_exists_f_Z(n0,n1,n1,X0)),true) ).
cnf(u3066,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u3006,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u1644,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),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(u2939,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(n0_and_n1_reflexive_1,axiom,
equalish(n0,n0) = true ).
cnf(u2163,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u289,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n1,X0,n1,sK1_exists_f_Z(n0,n1,X0,n1)),true) ).
cnf(u5,axiom,
true = equalish(n1,n1) ).
cnf(u1640,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(n0,X0),true) ).
cnf(u1647,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X3,n1),true) ).
cnf(u3153,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u3494,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u3230,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u2905,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u1432,axiom,
true = f(n1,n0,n0,n0,sK1_exists_f_Z(n1,n0,n0,n0)) ).
cnf(u745,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(n1,X2),true) ).
cnf(u2014,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(n0,X0),true) ).
cnf(u1180,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(n1,X2),true) ).
cnf(u3203,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u2156,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(n0,X0),true) ).
cnf(u836,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(n0,X2),true) ).
cnf(u1176,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(n1,X0),true) ).
cnf(u1183,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X3,n0),true) ).
cnf(u1810,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X1,n0),true) ).
cnf(u2909,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u1463,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(n1,X0),true) ).
cnf(u747,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(n1,X3),true) ).
cnf(u4026,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u192,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,X0,n1,n0,sK1_exists_f_Z(n1,X0,n1,n0)),true) ).
cnf(u746,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X2,n1),true) ).
cnf(u3342,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u3004,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u2903,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u1708,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(n1,X1),true) ).
cnf(u155,axiom,
true = ifeq2(f(X0,n1,X1,X2,X3),true,ifeq2(f(X4,n1,X5,X6,X3),true,true,true),true) ).
cnf(u1326,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(n1,X3),true) ).
cnf(u2438,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(n0,X1),true) ).
cnf(u1914,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(n1,X2),true) ).
cnf(u1710,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(n1,X2),true) ).
cnf(u348,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n0,n0,X0,sK1_exists_f_Z(n0,n0,n0,X0)),true) ).
cnf(u465,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n1,n1,n0,sK1_exists_f_Z(X0,n1,n1,n0)),true) ).
cnf(u3234,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) ).
cnf(u1709,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X1,n1),true) ).
cnf(u151,axiom,
true = ifeq2(f(X0,X1,n1,X2,X3),true,ifeq2(f(X4,X5,n1,X6,X3),true,true,true),true) ).
cnf(u48,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(u116,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(u190,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n0,n1,X0,sK1_exists_f_Z(n1,n0,n1,X0)),true) ).
cnf(u3067,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u930,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(n1,X0),true) ).
cnf(u2904,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u742,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X0,n1),true) ).
cnf(u684,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u741,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(n1,X0),true) ).
cnf(u2160,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(n0,X2),true) ).
cnf(u103,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(u3031,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u3117,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u1813,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(n1,X3),true) ).
cnf(u59,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(u89,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(u3193,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u446,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n1,n0,n0,sK1_exists_f_Z(X0,n1,n0,n0)),true) ).
cnf(u61,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(u369,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n0,X0,n0,sK1_exists_f_Z(n0,n0,X0,n0)),true) ).
cnf(u2439,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X1,n0),true) ).
cnf(u2305,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X3,n0),true) ).
cnf(u407,axiom,
true = ifeq2(equalish(X0,X0),true,f(X0,n0,n0,n0,sK1_exists_f_Z(X0,n0,n0,n0)),true) ).
cnf(u3033,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u1809,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(n0,X1),true) ).
cnf(u2970,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u172,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,n1,n1,X0,sK1_exists_f_Z(n1,n1,n1,X0)),true) ).
cnf(u2910,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u2019,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X2,n0),true) ).
cnf(u1879,axiom,
true = f(n0,n1,n1,n0,sK1_exists_f_Z(n0,n1,n1,n0)) ).
cnf(u35,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(u902,axiom,
true = f(n1,n1,n1,n0,sK1_exists_f_Z(n1,n1,n1,n0)) ).
cnf(u3115,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u1468,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X2,n0),true) ).
cnf(u31,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(u17,axiom,
b = ifeq(equalish(n0,n1),true,a,b) ).
cnf(u650,axiom,
true = f(n1,n1,n1,n1,sK1_exists_f_Z(n1,n1,n1,n1)) ).
cnf(u1643,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X1,n1),true) ).
cnf(u649,axiom,
true = f(n1,n0,n1,n1,sK1_exists_f_Z(n1,n0,n1,n1)) ).
cnf(u2874,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u3165,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u288,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n0,X0,n1,sK1_exists_f_Z(n0,n0,X0,n1)),true) ).
cnf(u3095,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) ).
cnf(u3285,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u291,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,X0,n1,n1,sK1_exists_f_Z(n0,X0,n1,n1)),true) ).
cnf(u3162,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
cnf(u1288,axiom,
true = f(n1,n0,n0,n1,sK1_exists_f_Z(n1,n0,n0,n1)) ).
cnf(u1181,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X2,n1),true) ).
cnf(u1807,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(n0,X0),true) ).
cnf(u3037,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u3142,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u1036,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(n0,X2),true) ).
cnf(u3100,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u3187,axiom,
true = ifeq2(f(X0,X1,n0,X2,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u3206,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) ).
cnf(u2941,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u2299,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X0,n0),true) ).
cnf(u3209,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u3220,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) ).
cnf(u3137,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u3189,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u3032,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) ).
cnf(u2301,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X1,n0),true) ).
cnf(u1032,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(n1,X0),true) ).
cnf(u931,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X0,n1),true) ).
cnf(u1039,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u2935,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u3186,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u3197,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u1917,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X3,n0),true) ).
cnf(u2440,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(n0,X2),true) ).
cnf(u3172,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) ).
cnf(u1000,axiom,
true = f(n1,n1,n0,n0,sK1_exists_f_Z(n1,n1,n0,n0)) ).
cnf(u1913,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X1,n1),true) ).
cnf(u211,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,X0,n0,n1,sK1_exists_f_Z(n1,X0,n0,n1)),true) ).
cnf(u3124,axiom,
true = ifeq2(f(X0,X1,n1,X2,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(goal,negated_conjecture,
a != b ).
cnf(u2436,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(n0,X0),true) ).
cnf(u2159,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X1,n1),true) ).
cnf(u3406,axiom,
true = ifeq2(f(n0,X0,X1,X2,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) ).
cnf(u3038,axiom,
true = ifeq2(f(X0,n1,X1,X2,sK1_exists_f_Z(n1,n1,n1,n1)),true,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(u3325,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) ).
cnf(u1610,axiom,
true = f(n0,n1,n1,n1,sK1_exists_f_Z(n0,n1,n1,n1)) ).
cnf(u834,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(n1,X1),true) ).
cnf(u2937,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) ).
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(u193,axiom,
true = ifeq2(equalish(X0,X0),true,f(n1,X0,n1,n1,sK1_exists_f_Z(n1,X0,n1,n1)),true) ).
cnf(u2878,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,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(u3063,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) ).
cnf(u4496,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) ).
cnf(u152,axiom,
true = ifeq2(f(X0,X1,n0,X2,X3),true,ifeq2(f(X4,X5,n0,X6,X3),true,true,true),true) ).
cnf(u1327,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X3,n1),true) ).
cnf(u350,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,X0,n0,n0,sK1_exists_f_Z(n0,X0,n0,n0)),true) ).
cnf(u743,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(n1,X1),true) ).
cnf(u115,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(u3065,axiom,
true = ifeq2(f(X0,X1,X2,n1,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) ).
cnf(u1812,axiom,
true = ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X2,n1),true) ).
cnf(u3002,axiom,
true = ifeq2(f(X0,n0,X1,X2,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) ).
cnf(u308,axiom,
true = ifeq2(equalish(X0,X0),true,f(n0,n1,n0,X0,sK1_exists_f_Z(n0,n1,n0,X0)),true) ).
cnf(u2942,axiom,
true = ifeq2(f(X0,X1,X2,n0,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) ).
cnf(u2875,axiom,
true = ifeq2(f(n1,X0,X1,X2,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) ).
cnf(u1776,axiom,
true = f(n0,n0,n1,n1,sK1_exists_f_Z(n0,n0,n1,n1)) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % 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 THM
% 0.10/0.38 % Computer : n016.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 17:47:03 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.70/2.24 % (2878036)Detected a unit-equality problem, will run specialized UEQ schedule.
% 9.70/2.24 % (2878044)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=360537802:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 9.70/2.24 % (2878044)Instruction limit reached!
% 9.70/2.24 % (2878044)------------------------------
% 9.70/2.24 % (2878044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.70/2.24 % (2878044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/2.24 % (2878044)CaDiCaL version: 2.1.3
% 9.70/2.24 % (2878044)Termination reason: Instruction limit
% 9.70/2.24 % (2878044)Termination phase: Saturation
% 9.70/2.24 % (2878044)Time elapsed: 0.040 s
% 9.70/2.24 % (2878044)Peak memory usage: 87 MB
% 9.70/2.24 % (2878044)Instructions burned: 138 (million)
% 9.70/2.24 % (2878041)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=176785881:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 9.70/2.24 % (2878045)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3686240459:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 9.70/2.24 % (2878043)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=407837958:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 9.70/2.24 % (2878046)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2843397971:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 9.70/2.24 % (2878042)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3792032376:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 9.70/2.24 % (2878047)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2325839154:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 9.70/2.24 % (2878045)Instruction limit reached!
% 9.70/2.24 % (2878045)------------------------------
% 9.70/2.24 % (2878045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.70/2.24 % (2878045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/2.24 % (2878045)CaDiCaL version: 2.1.3
% 9.70/2.24 % (2878045)Termination reason: Instruction limit
% 9.70/2.24 % (2878045)Termination phase: Saturation
% 9.70/2.24 % (2878045)Time elapsed: 0.103 s
% 9.70/2.24 % (2878045)Peak memory usage: 88 MB
% 9.70/2.24 % (2878045)Instructions burned: 182 (million)
% 9.70/2.24 % (2878055)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2751350512:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 9.70/2.24 % (2878046)Instruction limit reached!
% 9.70/2.24 % (2878046)------------------------------
% 9.70/2.24 % (2878046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.70/2.24 % (2878046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/2.24 % (2878046)CaDiCaL version: 2.1.3
% 9.70/2.24 % (2878046)Termination reason: Instruction limit
% 9.70/2.24 % (2878046)Termination phase: Saturation
% 9.70/2.24 % (2878046)Time elapsed: 0.144 s
% 9.70/2.24 % (2878046)Peak memory usage: 89 MB
% 9.70/2.24 % (2878046)Instructions burned: 257 (million)
% 9.70/2.24 % (2878047)Refutation not found, incomplete strategy
% 9.70/2.24 % (2878047)------------------------------
% 9.70/2.24 % (2878047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.70/2.24 % (2878047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/2.24 % (2878047)CaDiCaL version: 2.1.3
% 9.70/2.24 % (2878047)Termination reason: Refutation not found, incomplete strategy
% 9.70/2.24 % (2878047)Time elapsed: 0.154 s
% 9.70/2.24 % (2878047)Peak memory usage: 89 MB
% 9.70/2.24 % (2878047)Instructions burned: 279 (million)
% 9.70/2.24 % (2878056)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3408651302:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 9.70/2.24 % (2878058)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3447704809:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 9.70/2.24 % (2878047)------------------------------
% 9.70/2.24 % (2878047)------------------------------
% 9.70/2.24 % (2878058)Instruction limit reached!
% 9.70/2.24 % (2878058)------------------------------
% 9.70/2.24 % (2878058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.70/2.24 % (2878058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/2.24 % (2878058)CaDiCaL version: 2.1.3
% 9.70/2.24 % (2878058)Termination reason: Instruction limit
% 9.70/2.24 % (2878058)Termination phase: Saturation
% 9.70/2.24 % (2878058)Time elapsed: 0.106 s
% 9.70/2.24 % (2878058)Peak memory usage: 88 MB
% 9.70/2.24 % (2878058)Instructions burned: 215 (million)
% 9.70/2.24 % (2878061)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=2226737770:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 9.70/2.24 % (2878062)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=1697879551:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2994 on theBenchmark for (2994ds/12125Mi)
% 9.70/2.24 % (2878041)Refutation not found, incomplete strategy
% 9.70/2.24 % (2878041)------------------------------
% 9.70/2.24 % (2878041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.70/2.24 % (2878041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/2.24 % (2878041)CaDiCaL version: 2.1.3
% 9.70/2.24 % (2878041)Termination reason: Refutation not found, incomplete strategy
% 9.70/2.24 % (2878041)Time elapsed: 0.727 s
% 9.70/2.24 % (2878041)Peak memory usage: 131 MB
% 9.70/2.24 % (2878041)Instructions burned: 1387 (million)
% 9.70/2.24 % (2878061)Instruction limit reached!
% 9.70/2.24 % (2878061)------------------------------
% 9.70/2.24 % (2878061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.70/2.24 % (2878061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/2.24 % (2878061)CaDiCaL version: 2.1.3
% 9.70/2.24 % (2878061)Termination reason: Instruction limit
% 9.70/2.24 % (2878061)Termination phase: Saturation
% 9.70/2.24 % (2878061)Time elapsed: 0.186 s
% 9.70/2.24 % (2878061)Peak memory usage: 91 MB
% 9.70/2.24 % (2878061)Instructions burned: 317 (million)
% 9.70/2.24 % (2878055)Refutation not found, incomplete strategy
% 9.70/2.24 % (2878055)------------------------------
% 9.70/2.24 % (2878055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.70/2.24 % (2878055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/2.24 % (2878055)CaDiCaL version: 2.1.3
% 9.70/2.24 % (2878055)Termination reason: Refutation not found, incomplete strategy
% 9.70/2.24 % (2878055)Time elapsed: 0.641 s
% 9.70/2.24 % (2878055)Peak memory usage: 132 MB
% 9.70/2.24 % (2878055)Instructions burned: 1324 (million)
% 9.70/2.24 % (2878041)------------------------------
% 9.70/2.24 % (2878041)------------------------------
% 9.70/2.24 % (2878065)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3891719486:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 9.70/2.24 % (2878042)First to succeed.
% 9.70/2.24 % (2878042)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2878036"
% 9.70/2.24 % (2878043)Also succeeded, but the first one will report.
% 9.70/2.24 % (2878055)------------------------------
% 9.70/2.24 % (2878055)------------------------------
% 9.70/2.24 % (2878066)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2758914715:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 9.70/2.24 % (2878065)Also succeeded, but the first one will report.
% 9.70/2.24 % (2878056)Also succeeded, but the first one will report.
% 9.70/2.24 % (2878069)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=2137847349:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2988 on theBenchmark for (2988ds/11832Mi)
% 9.70/2.24 % SZS status Satisfiable for theBenchmark
% 9.70/2.24 % SZS output start Saturation.
% See solution above
% 10.34/2.44 % SZS output start Definitions and Model Updates.
% 10.34/2.44 % SZS output end Definitions and Model Updates.
% 10.34/2.44 % (2878042)------------------------------
% 10.34/2.44 % (2878042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.34/2.44 % (2878042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.34/2.44 % (2878042)CaDiCaL version: 2.1.3
% 10.34/2.44 % (2878042)Termination reason: Satisfiable
% 10.34/2.44 % (2878042)Time elapsed: 0.936 s
% 10.34/2.44 % (2878042)Peak memory usage: 131 MB
% 10.34/2.44 % (2878042)Instructions burned: 1431 (million)
% 10.34/2.44 % (2878042)------------------------------
% 10.34/2.44 % (2878042)------------------------------
% 10.34/2.44 % (2878036)Success in time 1.38 s
% 10.34/2.44 % Vampire exiting
%------------------------------------------------------------------------------