%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : MSC013-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.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 13.96s 2.86s
% Output : Saturation 14.55s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u5767,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n0,n1)),true,equalish(n0,X1),true) ).
cnf(u4756,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n1,X0,n1,n0,sK1_relation_exists_F(n0,n1,X0,n1,n0)),true) ).
cnf(u3301,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n1,n1,n1,X0,sK1_relation_exists_F(n0,n1,n1,n1,X0)),true) ).
cnf(u2945,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,X0,X1,n1,n1,sK1_relation_exists_F(n1,X0,X1,n1,n1)),true),true) ).
cnf(u1895,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n0,n0)),true,equalish(n1,X0),true) ).
cnf(u32,axiom,
true = ifeq(f(n1,X3,X0,X1,X7,X8),true,ifeq(f(n1,X6,X4,X5,X2,X8),true,true,true),true) ).
cnf(u4263,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n0,n1)),true,equalish(n1,X3),true) ).
cnf(u232,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n0,n0,X2,X1,X0,sK1_relation_exists_F(n0,n0,X2,X1,X0)),true),true),true) ).
cnf(u1681,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n1,n0)),true,equalish(n1,X2),true) ).
cnf(u1572,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n1,X0,n0,n0,sK1_relation_exists_F(n1,n1,X0,n0,n0)),true) ).
cnf(u4838,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n1,n1)),true,equalish(X0,n1),true) ).
cnf(u5013,axiom,
true = f(n0,n0,n1,n0,n1,sK1_relation_exists_F(n0,n0,n1,n0,n1)) ).
cnf(u3096,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n0,X0,n0,n0,sK1_relation_exists_F(n1,n0,X0,n0,n0)),true) ).
cnf(u5410,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n1,n0,X0,n0,sK1_relation_exists_F(X1,n1,n0,X0,n0)),true),true) ).
cnf(u2587,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n0,n1)),true,equalish(n0,X3),true) ).
cnf(u5534,axiom,
true = f(n0,n0,n0,n1,n0,sK1_relation_exists_F(n0,n0,n0,n1,n0)) ).
cnf(u3373,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n1,n0)),true,equalish(n1,X0),true) ).
cnf(u160,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n1,n0)),true,equalish(X3,n1),true) ).
cnf(u3127,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,X0,n1,n1,n1,sK1_relation_exists_F(n1,X0,n1,n1,n1)),true) ).
cnf(u818,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n1,n0,X0,n0,sK1_relation_exists_F(n1,n1,n0,X0,n0)),true) ).
cnf(u6651,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n0,n0,n0,n1,sK1_relation_exists_F(X0,n0,n0,n0,n1)),true) ).
cnf(u61,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n1,n1,X2,X1,X0,sK1_relation_exists_F(n1,n1,X2,X1,X0)),true),true),true) ).
cnf(u3872,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n1,n1,n0,n1)),true,true,true) ).
cnf(u3377,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n1,n0)),true,equalish(n0,X4),true) ).
cnf(u5043,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n0,n1)),true,equalish(n1,X4),true) ).
cnf(u6484,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n1,n0,n1,n0,sK1_relation_exists_F(X0,n1,n0,n1,n0)),true) ).
cnf(u5077,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n0,n0)),true,equalish(n0,X3),true) ).
cnf(u4269,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n0,n1)),true,equalish(n1,X4),true) ).
cnf(u1058,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n0,n1)),true,equalish(X1,n0),true) ).
cnf(u51,axiom,
true = ifeq(equalish(X3,X3),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,X1,X2,X3,n1,sK1_relation_exists_F(X0,X1,X2,X3,n1)),true),true),true),true) ).
cnf(u330,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n0,n1)),true,equalish(X3,n0),true) ).
cnf(u2780,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n0,n0,n1,n1)),true,true,true) ).
cnf(u1606,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,n0,X0,n0,X1,sK1_relation_exists_F(n1,n0,X0,n0,X1)),true),true) ).
cnf(u822,axiom,
true = f(n1,n1,n0,n1,n0,sK1_relation_exists_F(n1,n1,n0,n1,n0)) ).
cnf(u2750,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,X0,n0,X1,n1,sK1_relation_exists_F(n1,X0,n0,X1,n1)),true),true) ).
cnf(u6312,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,X0,n1,n0,n0,sK1_relation_exists_F(n0,X0,n1,n0,n0)),true) ).
cnf(u2628,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n0,n0)),true,equalish(X4,n0),true) ).
cnf(u1859,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n0,n1)),true,equalish(n1,X4),true) ).
cnf(u78,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,n1,X0,n0,X1,sK1_relation_exists_F(n1,n1,X0,n0,X1)),true),true) ).
cnf(u4801,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n0,n1,n1,X0,sK1_relation_exists_F(n0,n0,n1,n1,X0)),true) ).
cnf(u5041,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n0,n1)),true,equalish(n0,X1),true) ).
cnf(u1094,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n0,n0)),true,equalish(X2,n1),true) ).
cnf(u5557,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n1,n1)),true,equalish(n0,X3),true) ).
cnf(u76,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n1,n1,n0,X1,X0,sK1_relation_exists_F(n1,n1,n0,X1,X0)),true),true) ).
cnf(u6247,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n0,X0,n1,n1,sK1_relation_exists_F(n0,n0,X0,n1,n1)),true) ).
cnf(u847,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n1,n1)),true,equalish(n0,X0),true) ).
cnf(u1098,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n0,n0)),true,equalish(X1,n0),true) ).
cnf(u2385,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n1,n1)),true,equalish(n1,X1),true) ).
cnf(u91,axiom,
true = f(n1,n1,n1,n1,n1,sK1_relation_exists_F(n1,n1,n1,n1,n1)) ).
cnf(u5561,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n1,n1)),true,equalish(n1,X1),true) ).
cnf(u323,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n0,n1)),true,equalish(n1,X2),true) ).
cnf(u1234,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X0,X0),true,f(X0,X2,n0,X1,n1,sK1_relation_exists_F(X0,X2,n0,X1,n1)),true),true),true) ).
cnf(u5210,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n1,n1,X0,n0,sK1_relation_exists_F(X1,n1,n1,X0,n0)),true),true) ).
cnf(u66,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n1,X2,X1,n0,X0,sK1_relation_exists_F(n1,X2,X1,n0,X0)),true),true),true) ).
cnf(u2633,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n0,n0)),true,equalish(n0,X4),true) ).
cnf(u2388,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n1,n1)),true,equalish(X0,n1),true) ).
cnf(u3008,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n0,n0,n0,n0)),true,true,true) ).
cnf(u5207,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n1,n1,n1,X0,sK1_relation_exists_F(X1,n1,n1,n1,X0)),true),true) ).
cnf(u5208,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n1,n1,n0,X0,sK1_relation_exists_F(X1,n1,n1,n0,X0)),true),true) ).
cnf(u116,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n1,n1)),true,equalish(X4,n1),true) ).
cnf(u2634,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n0,n0)),true,equalish(X0,n0),true) ).
cnf(u3921,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,X0,n0,n0,X1,sK1_relation_exists_F(n0,X0,n0,n0,X1)),true),true) ).
cnf(u1235,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(X2,X1,n0,X0,n0,sK1_relation_exists_F(X2,X1,n0,X0,n0)),true),true),true) ).
cnf(u990,axiom,
true = ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,X1,n1,n0,X2,sK1_relation_exists_F(X0,X1,n1,n0,X2)),true),true),true) ).
cnf(u887,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n1,n0)),true,equalish(n0,X0),true) ).
cnf(u3538,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n0,n1)),true,equalish(X4,n1),true) ).
cnf(u5081,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n0,n0)),true,equalish(n0,X1),true) ).
cnf(u363,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n0,n0)),true,equalish(n1,X2),true) ).
cnf(u4871,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n1,n0)),true,equalish(n0,X3),true) ).
cnf(u6848,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,X0,n0,n1,n0,sK1_relation_exists_F(X1,X0,n0,n1,n0)),true),true) ).
cnf(u4303,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n0,n0)),true,equalish(n1,X3),true) ).
cnf(u4218,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n0,X1,X0,n1,n0,sK1_relation_exists_F(n0,X1,X0,n1,n0)),true),true) ).
cnf(u4063,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n1,n1)),true,equalish(n1,X4),true) ).
cnf(u491,axiom,
true = ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n1,X1,n0,X2,sK1_relation_exists_F(X0,n1,X1,n0,X2)),true),true),true) ).
cnf(u6180,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n0,n0,n0,n0)),true,true,true) ).
cnf(u4836,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u6371,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,X0,n0,n0,n1,sK1_relation_exists_F(n0,X0,n0,n0,n1)),true) ).
cnf(u5941,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n1,X1,n0,n1,sK1_relation_exists_F(X0,n1,X1,n0,n1)),true),true) ).
cnf(u1642,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n1,n1)),true,equalish(X2,n1),true) ).
cnf(u489,axiom,
true = ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n1,n0,X1,X2,sK1_relation_exists_F(X0,n1,n0,X1,X2)),true),true),true) ).
cnf(u5083,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n0,n0)),true,equalish(n0,X4),true) ).
cnf(u1648,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u890,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n1,n0)),true,equalish(X3,n1),true) ).
cnf(u3333,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n1,n1)),true,equalish(n1,X0),true) ).
cnf(u4096,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n1,n0)),true,equalish(X2,n0),true) ).
cnf(u16,axiom,
true = ifeq(f(X0,X1,X2,X3,X4,X5),true,ifeq(f(X6,X7,X8,X9,X10,X5),true,equalish(X8,X2),true),true) ).
cnf(u2050,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n0,n1,n1,n1)),true,true,true) ).
cnf(u3337,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n1,n1)),true,equalish(n1,X4),true) ).
cnf(u1556,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n1,X0,n1,n0,sK1_relation_exists_F(n1,n1,X0,n1,n0)),true) ).
cnf(u3922,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,X0,n0,X1,n1,sK1_relation_exists_F(n0,X0,n0,X1,n1)),true),true) ).
cnf(u4102,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n1,n0)),true,equalish(X3,n1),true) ).
cnf(u3080,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n0,X0,n1,n0,sK1_relation_exists_F(n1,n0,X0,n1,n0)),true) ).
cnf(u2852,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n0,n0,n1,n0)),true,true,true) ).
cnf(u1571,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n1,X0,n0,n1,sK1_relation_exists_F(n1,n1,X0,n0,n1)),true) ).
cnf(u5764,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n0,n1)),true,equalish(X4,n0),true) ).
cnf(u22,negated_conjecture,
true != goal ).
cnf(u522,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n1,n1,n1,n1)),true,true,true) ).
cnf(u1684,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n1,n0)),true,equalish(X4,n0),true) ).
cnf(u45,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X3,X3),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X0,X0),true,f(X0,n1,X2,X3,X1,sK1_relation_exists_F(X0,n1,X2,X3,X1)),true),true),true),true) ).
cnf(u5768,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n0,n1)),true,equalish(X3,n0),true) ).
cnf(u1682,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n1,n0)),true,equalish(X2,n1),true) ).
cnf(u6796,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,X0,n1,n0,n0,sK1_relation_exists_F(X1,X0,n1,n0,n0)),true),true) ).
cnf(u1061,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n0,n1)),true,equalish(n1,X4),true) ).
cnf(u1688,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n1,n0)),true,equalish(X3,n1),true) ).
cnf(u1322,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n1,n0,n1,n0)),true,true,true) ).
cnf(u2352,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n0,n0,n0,X0,sK1_relation_exists_F(n1,n0,n0,n0,X0)),true) ).
cnf(u62,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n1,n0,X2,X1,X0,sK1_relation_exists_F(n1,n0,X2,X1,X0)),true),true),true) ).
cnf(u2358,axiom,
true = f(n1,n0,n0,n1,n0,sK1_relation_exists_F(n1,n0,n0,n1,n0)) ).
cnf(u5562,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u817,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n1,n0,X0,n1,sK1_relation_exists_F(n1,n1,n0,X0,n1)),true) ).
cnf(u5556,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n1,n1)),true,equalish(X2,n0),true) ).
cnf(u4030,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n1,n0,X0,n0,sK1_relation_exists_F(n0,n1,n0,X0,n0)),true) ).
cnf(u2629,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n0,n0)),true,equalish(n0,X0),true) ).
cnf(u6566,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n0,n1,n0,X0,sK1_relation_exists_F(X1,n0,n1,n0,X0)),true),true) ).
cnf(u2627,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n0,n0)),true,equalish(n0,X3),true) ).
cnf(u161,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n1,n0)),true,equalish(n0,X4),true) ).
cnf(u1054,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n0,n1)),true,equalish(X2,n1),true) ).
cnf(u5560,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n1,n1)),true,equalish(X1,n0),true) ).
cnf(u5039,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n0,n1)),true,equalish(n1,X0),true) ).
cnf(u50,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X3,X3),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X0,X0),true,f(X0,X2,X3,n0,X1,sK1_relation_exists_F(X0,X2,X3,n0,X1)),true),true),true),true) ).
cnf(u5564,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n1,n1)),true,equalish(X0,n1),true) ).
cnf(u2630,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n0,n0)),true,equalish(X1,n0),true) ).
cnf(u1101,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n0,n0)),true,equalish(n0,X4),true) ).
cnf(u4528,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n1,n0,n1,n0)),true,true,true) ).
cnf(u75,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n1,n1,n1,X1,X0,sK1_relation_exists_F(n1,n1,n1,X1,X0)),true),true) ).
cnf(u329,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n0,n1)),true,equalish(n0,X1),true) ).
cnf(u4802,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n0,n1,n0,X0,sK1_relation_exists_F(n0,n0,n1,n0,X0)),true) ).
cnf(u846,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n1,n1)),true,equalish(X4,n1),true) ).
cnf(u4029,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n1,n0,X0,n1,sK1_relation_exists_F(n0,n1,n0,X0,n1)),true) ).
cnf(u2631,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n0,n0)),true,equalish(n0,X1),true) ).
cnf(u2497,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,X0,n1,n1,X1,sK1_relation_exists_F(n1,X0,n1,n1,X1)),true),true) ).
cnf(u3338,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n1,n1)),true,equalish(X0,n1),true) ).
cnf(u4027,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n1,n0,n1,X0,sK1_relation_exists_F(n0,n1,n0,n1,X0)),true) ).
cnf(u328,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n0,n1)),true,equalish(X1,n1),true) ).
cnf(u3535,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n0,n1)),true,equalish(n0,X2),true) ).
cnf(u2500,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n1,X1,n1,X0,n0,sK1_relation_exists_F(n1,X1,n1,X0,n0)),true),true) ).
cnf(u79,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,n1,X0,X1,n1,sK1_relation_exists_F(n1,n1,X0,X1,n1)),true),true) ).
cnf(u4034,axiom,
true = f(n0,n1,n0,n1,n0,sK1_relation_exists_F(n0,n1,n0,n1,n0)) ).
cnf(u3376,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n1,n0)),true,equalish(X3,n1),true) ).
cnf(u5079,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n0,n0)),true,equalish(n1,X0),true) ).
cnf(u3128,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,X0,n1,n1,n0,sK1_relation_exists_F(n1,X0,n1,n1,n0)),true) ).
cnf(u4033,axiom,
true = f(n0,n1,n0,n1,n1,sK1_relation_exists_F(n0,n1,n0,n1,n1)) ).
cnf(u3542,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n0,n1)),true,equalish(X3,n0),true) ).
cnf(u4829,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n1,n1)),true,equalish(n0,X2),true) ).
cnf(u3800,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n1,n1,n1,n0)),true,true,true) ).
cnf(u1742,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X0,X0),true,f(X0,X2,X1,n0,n1,sK1_relation_exists_F(X0,X2,X1,n0,n1)),true),true),true) ).
cnf(u368,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n0,n0)),true,equalish(X1,n1),true) ).
cnf(u88,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n1,n1,X0,n0,sK1_relation_exists_F(n1,n1,n1,X0,n0)),true) ).
cnf(u6636,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n0,n0,n1,n0,sK1_relation_exists_F(X0,n0,n0,n1,n0)),true) ).
cnf(u1645,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n1,n1)),true,equalish(n1,X0),true) ).
cnf(u119,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n1,n1)),true,equalish(n1,X1),true) ).
cnf(u5740,axiom,
true = f(n0,n0,n0,n0,n0,sK1_relation_exists_F(n0,n0,n0,n0,n0)) ).
cnf(u4835,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n1,n1)),true,equalish(n1,X1),true) ).
cnf(u4103,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n1,n0)),true,equalish(n0,X4),true) ).
cnf(u989,axiom,
true = ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,X1,n1,n1,X2,sK1_relation_exists_F(X0,X1,n1,n1,X2)),true),true),true) ).
cnf(u5080,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n0,n0)),true,equalish(X1,n1),true) ).
cnf(u1649,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n1,n1)),true,equalish(n1,X4),true) ).
cnf(u6499,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n1,n0,n0,n1,sK1_relation_exists_F(X0,n1,n0,n0,n1)),true) ).
cnf(u3302,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n1,n1,n0,X0,sK1_relation_exists_F(n0,n1,n1,n0,X0)),true) ).
cnf(u117,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n1,n1)),true,equalish(n1,X0),true) ).
cnf(u2426,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n1,n0)),true,equalish(X3,n1),true) ).
cnf(u3295,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,n1,X0,X1,n1,sK1_relation_exists_F(n0,n1,X0,X1,n1)),true),true) ).
cnf(u372,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n0,n0)),true,equalish(X0,n0),true) ).
cnf(u2419,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n1,n0)),true,equalish(n1,X2),true) ).
cnf(u4101,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n1,n0)),true,equalish(n1,X1),true) ).
cnf(u1394,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n1,n0,n0,n1)),true,true,true) ).
cnf(u29,axiom,
true = ifeq(f(X0,n0,X1,X2,X3,X4),true,ifeq(f(X5,n0,X6,X7,X8,X4),true,true,true),true) ).
cnf(u3580,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n0,n0)),true,equalish(X1,n1),true) ).
cnf(u5407,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n1,n0,n1,X0,sK1_relation_exists_F(X1,n1,n0,n1,X0)),true),true) ).
cnf(u231,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n0,n1,X2,X1,X0,sK1_relation_exists_F(n0,n1,X2,X1,X0)),true),true),true) ).
cnf(u1555,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n1,X0,n1,n1,sK1_relation_exists_F(n1,n1,X0,n1,n1)),true) ).
cnf(u6,axiom,
true = ifeq(equalish(n0,n1),true,goal,true) ).
cnf(u4872,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n1,n0)),true,equalish(X4,n0),true) ).
cnf(u3095,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n0,X0,n0,n1,sK1_relation_exists_F(n1,n0,X0,n0,n1)),true) ).
cnf(u3577,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n0,n0)),true,equalish(n1,X3),true) ).
cnf(u3203,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,X0,n0,n0,n1,sK1_relation_exists_F(n1,X0,n0,n0,n1)),true) ).
cnf(u1685,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n1,n0)),true,equalish(n1,X0),true) ).
cnf(u4240,axiom,
true = f(n0,n1,n0,n0,n0,sK1_relation_exists_F(n0,n1,n0,n0,n0)) ).
cnf(u1683,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n1,n0)),true,equalish(n0,X3),true) ).
cnf(u4099,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n1,n0)),true,equalish(n0,X0),true) ).
cnf(u6452,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n1,n1,n0,n0,sK1_relation_exists_F(X0,n1,n1,n0,n0)),true) ).
cnf(u6795,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,X1,n1,n0,n1,sK1_relation_exists_F(X0,X1,n1,n0,n1)),true),true) ).
cnf(u2590,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n0,n1)),true,equalish(X1,n0),true) ).
cnf(u157,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n1,n0)),true,equalish(n1,X0),true) ).
cnf(u4870,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n1,n0)),true,equalish(X2,n0),true) ).
cnf(u46,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X3,X3),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X0,X0),true,f(X0,n0,X2,X3,X1,sK1_relation_exists_F(X0,n0,X2,X3,X1)),true),true),true),true) ).
cnf(u3715,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n0,X1,n1,X0,n0,sK1_relation_exists_F(n0,X1,n1,X0,n0)),true),true) ).
cnf(u3475,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n0,n0,n1,X1,X0,sK1_relation_exists_F(n0,n0,n1,X1,X0)),true),true) ).
cnf(u1062,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n0,n1)),true,equalish(X0,n1),true) ).
cnf(u301,axiom,
true = f(n1,n1,n1,n0,n1,sK1_relation_exists_F(n1,n1,n1,n0,n1)) ).
cnf(u1055,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n0,n1)),true,equalish(n1,X3),true) ).
cnf(u44,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X3,X3),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,f(n0,X1,X2,X3,X0,sK1_relation_exists_F(n0,X1,X2,X3,X0)),true),true),true),true) ).
cnf(u3371,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n1,n0)),true,equalish(n1,X3),true) ).
cnf(u3477,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,n0,X0,n1,X1,sK1_relation_exists_F(n0,n0,X0,n1,X1)),true),true) ).
cnf(u815,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n1,n0,n1,X0,sK1_relation_exists_F(n1,n1,n0,n1,X0)),true) ).
cnf(u2353,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n0,n0,X0,n1,sK1_relation_exists_F(n1,n0,n0,X0,n1)),true) ).
cnf(u6436,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n1,n1,n1,n0,sK1_relation_exists_F(X0,n1,n1,n1,n0)),true) ).
cnf(u3374,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n1,n0)),true,equalish(X1,n1),true) ).
cnf(u680,axiom,
true = ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n0,n0,X1,X2,sK1_relation_exists_F(X0,n0,n0,X1,X2)),true),true),true) ).
cnf(u2593,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n0,n1)),true,equalish(n1,X4),true) ).
cnf(u5036,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n0,n1)),true,equalish(X2,n0),true) ).
cnf(u5302,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n0,n1,n1,n0)),true,true,true) ).
cnf(u3378,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n1,n0)),true,equalish(X0,n0),true) ).
cnf(u2748,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,X0,n0,n1,X1,sK1_relation_exists_F(n1,X0,n0,n1,X1)),true),true) ).
cnf(u5529,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n0,n0,X0,n1,sK1_relation_exists_F(n0,n0,n0,X0,n1)),true) ).
cnf(u5038,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n0,n1)),true,equalish(X4,n0),true) ).
cnf(u6688,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n0,X0,n1,n0,sK1_relation_exists_F(X1,n0,X0,n1,n0)),true),true) ).
cnf(u162,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n1,n0)),true,equalish(X0,n0),true) ).
cnf(u1852,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n0,n1)),true,equalish(X2,n1),true) ).
cnf(u6343,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,X0,n0,n1,n1,sK1_relation_exists_F(n0,X0,n0,n1,n1)),true) ).
cnf(u63,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n1,X2,n1,X1,X0,sK1_relation_exists_F(n1,X2,n1,X1,X0)),true),true),true) ).
cnf(u2626,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n0,n0)),true,equalish(X2,n1),true) ).
cnf(u1102,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n0,n0)),true,equalish(X0,n0),true) ).
cnf(u684,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(X2,n0,X1,X0,n0,sK1_relation_exists_F(X2,n0,X1,X0,n0)),true),true),true) ).
cnf(u1095,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n0,n0)),true,equalish(n1,X3),true) ).
cnf(u6588,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n0,n0,X0,n0,sK1_relation_exists_F(X1,n0,n0,X0,n0)),true),true) ).
cnf(u2625,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n0,n0)),true,equalish(n1,X2),true) ).
cnf(u1100,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u331,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n0,n1)),true,equalish(n1,X4),true) ).
cnf(u1856,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n0,n1)),true,equalish(X1,n1),true) ).
cnf(u6296,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,X0,n1,n1,n0,sK1_relation_exists_F(n0,X0,n1,n1,n0)),true) ).
cnf(u4268,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n0,n1)),true,equalish(X3,n0),true) ).
cnf(u1607,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,n0,X0,X1,n1,sK1_relation_exists_F(n1,n0,X0,X1,n1)),true),true) ).
cnf(u5599,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n1,n0)),true,equalish(n0,X0),true) ).
cnf(u5597,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n1,n0)),true,equalish(n0,X3),true) ).
cnf(u845,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n1,n1)),true,equalish(n1,X3),true) ).
cnf(u2386,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u1892,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n0,n0)),true,equalish(X2,n1),true) ).
cnf(u4804,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n0,n1,X0,n0,sK1_relation_exists_F(n0,n0,n1,X0,n0)),true) ).
cnf(u843,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n1,n1)),true,equalish(n1,X2),true) ).
cnf(u1232,axiom,
true = ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,X1,n0,n1,X2,sK1_relation_exists_F(X0,X1,n0,n1,X2)),true),true),true) ).
cnf(u5601,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n1,n0)),true,equalish(n1,X1),true) ).
cnf(u3540,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n0,n1)),true,equalish(X1,n1),true) ).
cnf(u4830,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n1,n1)),true,equalish(X2,n0),true) ).
cnf(u1896,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n0,n0)),true,equalish(X1,n1),true) ).
cnf(u1616,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n0,n1,X0,n0,sK1_relation_exists_F(n1,n0,n1,X0,n0)),true) ).
cnf(u6098,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n0,n0,n0,n1)),true,true,true) ).
cnf(u5739,axiom,
true = f(n0,n0,n0,n0,n1,sK1_relation_exists_F(n0,n0,n0,n0,n1)) ).
cnf(u3544,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n0,n1)),true,equalish(X0,n1),true) ).
cnf(u1647,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n1,n1)),true,equalish(n1,X1),true) ).
cnf(u369,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n0,n0)),true,equalish(n0,X1),true) ).
cnf(u5458,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n0,n1,n0,n0)),true,true,true) ).
cnf(u5595,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n1,n0)),true,equalish(n0,X2),true) ).
cnf(u1646,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n1,n1)),true,equalish(X1,n1),true) ).
cnf(u885,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n1,n0)),true,equalish(n1,X3),true) ).
cnf(u4309,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n0,n0)),true,equalish(n0,X4),true) ).
cnf(u883,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n1,n0)),true,equalish(n1,X2),true) ).
cnf(u4869,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n1,n0)),true,equalish(n0,X2),true) ).
cnf(u1829,axiom,
true = f(n1,n0,n1,n0,n1,sK1_relation_exists_F(n1,n0,n1,n0,n1)) ).
cnf(u992,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(X2,X1,n1,X0,n0,sK1_relation_exists_F(X2,X1,n1,X0,n0)),true),true),true) ).
cnf(u1650,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n1,n1)),true,equalish(X0,n1),true) ).
cnf(u1899,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n0,n0)),true,equalish(n0,X4),true) ).
cnf(u118,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n1,n1)),true,equalish(X1,n1),true) ).
cnf(u2424,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n1,n0)),true,equalish(X1,n0),true) ).
cnf(u3079,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n0,X0,n1,n1,sK1_relation_exists_F(n1,n0,X0,n1,n1)),true) ).
cnf(u4056,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n1,n1)),true,equalish(X2,n0),true) ).
cnf(u2427,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n1,n0)),true,equalish(n0,X4),true) ).
cnf(u4877,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n1,n0)),true,equalish(n0,X4),true) ).
cnf(u3304,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n1,n1,X0,n0,sK1_relation_exists_F(n0,n1,n1,X0,n0)),true) ).
cnf(u30,axiom,
true = ifeq(f(X3,n1,X0,X1,X7,X8),true,ifeq(f(X5,n1,X4,X6,X2,X8),true,true,true),true) ).
cnf(u3329,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n1,n1)),true,equalish(n0,X2),true) ).
cnf(u3581,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n0,n0)),true,equalish(n0,X1),true) ).
cnf(u5762,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n0,n1)),true,equalish(X2,n0),true) ).
cnf(u4832,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n1,n1)),true,equalish(X4,n0),true) ).
cnf(u3331,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n1,n1)),true,equalish(n1,X3),true) ).
cnf(u5766,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n0,n1)),true,equalish(X1,n0),true) ).
cnf(u6248,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n0,X0,n1,n0,sK1_relation_exists_F(n0,n0,X0,n1,n0)),true) ).
cnf(u6635,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n0,n0,n1,n1,sK1_relation_exists_F(X0,n0,n0,n1,n1)),true) ).
cnf(u1686,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n1,n0)),true,equalish(X1,n1),true) ).
cnf(u2563,axiom,
true = f(n1,n0,n0,n0,n1,sK1_relation_exists_F(n1,n0,n0,n0,n1)) ).
cnf(u5374,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n0,n1,n0,n1)),true,true,true) ).
cnf(ifeq_axiom,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u5530,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n0,n0,X0,n0,sK1_relation_exists_F(n0,n0,n0,X0,n0)),true) ).
cnf(u3584,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n0,n0)),true,equalish(X0,n0),true) ).
cnf(u28,axiom,
true = ifeq(f(X2,X3,n1,X0,X7,X8),true,ifeq(f(X4,X6,n1,X5,X1,X8),true,true,true),true) ).
cnf(u158,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n1,n0)),true,equalish(X1,n1),true) ).
cnf(u6295,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,X0,n1,n1,n1,sK1_relation_exists_F(n0,X0,n1,n1,n1)),true) ).
cnf(u658,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n1,n1,n0,n1)),true,true,true) ).
cnf(u43,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X3,X3),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,f(n1,X1,X2,X3,X0,sK1_relation_exists_F(n1,X1,X2,X3,X0)),true),true),true),true) ).
cnf(u5014,axiom,
true = f(n0,n0,n1,n0,n0,sK1_relation_exists_F(n0,n0,n1,n0,n0)) ).
cnf(u1643,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n1,n1)),true,equalish(n0,X3),true) ).
cnf(u5528,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n0,n0,n0,X0,sK1_relation_exists_F(n0,n0,n0,n0,X0)),true) ).
cnf(u3375,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n1,n0)),true,equalish(n1,X1),true) ).
cnf(u5558,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n1,n1)),true,equalish(X4,n0),true) ).
cnf(u3712,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,X0,n1,n1,X1,sK1_relation_exists_F(n0,X0,n1,n1,X1)),true),true) ).
cnf(u5761,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n0,n1)),true,equalish(n0,X2),true) ).
cnf(u18,axiom,
true = ifeq(f(X0,X1,X2,X3,X4,X5),true,ifeq(f(X6,X7,X8,X9,X10,X5),true,equalish(X7,X1),true),true) ).
cnf(u2585,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n0,n1)),true,equalish(n1,X2),true) ).
cnf(u156,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n1,n0)),true,equalish(X4,n1),true) ).
cnf(u1059,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n0,n1)),true,equalish(n0,X1),true) ).
cnf(u5763,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n0,n1)),true,equalish(n0,X3),true) ).
cnf(u4755,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n1,X0,n1,n1,sK1_relation_exists_F(n0,n1,X0,n1,n1)),true) ).
cnf(u1830,axiom,
true = f(n1,n0,n1,n0,n0,sK1_relation_exists_F(n1,n0,n1,n0,n0)) ).
cnf(u2208,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n0,n1,n0,n1)),true,true,true) ).
cnf(u2586,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n0,n1)),true,equalish(X2,n1),true) ).
cnf(u5942,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n1,X0,n0,n0,sK1_relation_exists_F(X1,n1,X0,n0,n0)),true),true) ).
cnf(u2592,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n0,n1)),true,equalish(X3,n0),true) ).
cnf(u47,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X3,X3),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X0,X0),true,f(X0,X2,n1,X3,X1,sK1_relation_exists_F(X0,X2,n1,X3,X1)),true),true),true),true) ).
cnf(u6483,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n1,n0,n1,n1,sK1_relation_exists_F(X0,n1,n0,n1,n1)),true) ).
cnf(u302,axiom,
true = f(n1,n1,n1,n0,n0,sK1_relation_exists_F(n1,n1,n1,n0,n0)) ).
cnf(u2357,axiom,
true = f(n1,n0,n0,n1,n1,sK1_relation_exists_F(n1,n0,n0,n1,n1)) ).
cnf(u683,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X0,X0),true,f(X0,n0,X2,X1,n1,sK1_relation_exists_F(X0,n0,X2,X1,n1)),true),true),true) ).
cnf(u4266,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n0,n1)),true,equalish(X1,n0),true) ).
cnf(u2751,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n1,X1,n0,X0,n0,sK1_relation_exists_F(n1,X1,n0,X0,n0)),true),true) ).
cnf(u3514,axiom,
true = f(n0,n1,n1,n0,n0,sK1_relation_exists_F(n0,n1,n1,n0,n0)) ).
cnf(u1099,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n0,n0)),true,equalish(n0,X1),true) ).
cnf(u2383,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n1,n1)),true,equalish(n0,X0),true) ).
cnf(u5037,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n0,n1)),true,equalish(n0,X3),true) ).
cnf(u4264,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n0,n1)),true,equalish(X4,n1),true) ).
cnf(u5559,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n1,n1)),true,equalish(n0,X0),true) ).
cnf(u5956,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n0,n0,n1,n1)),true,true,true) ).
cnf(u6604,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n0,n1,n0,n0,sK1_relation_exists_F(X0,n0,n1,n0,n0)),true) ).
cnf(u5802,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n0,n0)),true,equalish(X2,n0),true) ).
cnf(u2381,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n1,n1)),true,equalish(n0,X3),true) ).
cnf(u87,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n1,n1,X0,n1,sK1_relation_exists_F(n1,n1,n1,X0,n1)),true) ).
cnf(u4803,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n0,n1,X0,n1,sK1_relation_exists_F(n0,n0,n1,X0,n1)),true) ).
cnf(u5711,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n1,X0,n1,n0,sK1_relation_exists_F(X1,n1,X0,n1,n0)),true),true) ).
cnf(u2498,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,X0,n1,n0,X1,sK1_relation_exists_F(n1,X0,n1,n0,X1)),true),true) ).
cnf(u6567,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n0,n1,X1,n1,sK1_relation_exists_F(X0,n0,n1,X1,n1)),true),true) ).
cnf(u4837,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n1,n1)),true,equalish(n1,X4),true) ).
cnf(u5710,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n1,X1,n1,n1,sK1_relation_exists_F(X0,n1,X1,n1,n1)),true),true) ).
cnf(u85,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n1,n1,n1,X0,sK1_relation_exists_F(n1,n1,n1,n1,X0)),true) ).
cnf(u848,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n1,n1)),true,equalish(X1,n0),true) ).
cnf(u4057,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n1,n1)),true,equalish(n1,X3),true) ).
cnf(u2387,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n1,n1)),true,equalish(n1,X4),true) ).
cnf(u3293,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,n1,X0,n1,X1,sK1_relation_exists_F(n0,n1,X0,n1,X1)),true),true) ).
cnf(u4239,axiom,
true = f(n0,n1,n0,n0,n1,sK1_relation_exists_F(n0,n1,n0,n0,n1)) ).
cnf(u3541,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n0,n1)),true,equalish(n0,X1),true) ).
cnf(u3160,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n1,X1,X0,n0,n0,sK1_relation_exists_F(n1,X1,X0,n0,n0)),true),true) ).
cnf(u5082,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u5598,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n1,n0)),true,equalish(X4,n0),true) ).
cnf(u888,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n1,n0)),true,equalish(X1,n0),true) ).
cnf(u5602,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n1,n0)),true,equalish(X3,n1),true) ).
cnf(u1233,axiom,
true = ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,X1,n0,n0,X2,sK1_relation_exists_F(X0,X1,n0,n0,X2)),true),true),true) ).
cnf(u5765,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n0,n1)),true,equalish(n0,X0),true) ).
cnf(u4058,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n1,n1)),true,equalish(X4,n1),true) ).
cnf(u3308,axiom,
true = f(n0,n1,n1,n1,n0,sK1_relation_exists_F(n0,n1,n1,n1,n0)) ).
cnf(u115,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n1,n1)),true,equalish(n1,X3),true) ).
cnf(u1096,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n0,n0)),true,equalish(X4,n1),true) ).
cnf(u4064,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n1,n1)),true,equalish(X0,n1),true) ).
cnf(u370,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u2425,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n1,n0)),true,equalish(n1,X1),true) ).
cnf(u2564,axiom,
true = f(n1,n0,n0,n0,n0,sK1_relation_exists_F(n1,n0,n0,n0,n0)) ).
cnf(u12,axiom,
true = ifeq(f(X0,X1,X2,X3,X4,X5),true,ifeq(f(X6,X7,X8,X9,X10,X5),true,equalish(X10,X4),true),true) ).
cnf(u14,axiom,
true = ifeq(f(X0,X1,X2,X3,X4,X5),true,ifeq(f(X6,X7,X8,X9,X10,X5),true,equalish(X9,X3),true),true) ).
cnf(u5604,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n1,n0)),true,equalish(X0,n0),true) ).
cnf(u886,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n1,n0)),true,equalish(X4,n1),true) ).
cnf(u3335,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n1,n1)),true,equalish(n1,X1),true) ).
cnf(u113,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n1,n1)),true,equalish(n1,X2),true) ).
cnf(u892,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n1,n0)),true,equalish(X0,n0),true) ).
cnf(u4097,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n1,n0)),true,equalish(n1,X3),true) ).
cnf(u4876,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n1,n0)),true,equalish(X3,n1),true) ).
cnf(u1053,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n0,n1)),true,equalish(n1,X2),true) ).
cnf(u3583,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n0,n0)),true,equalish(n0,X4),true) ).
cnf(u4060,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n1,n1)),true,equalish(X1,n0),true) ).
cnf(u2588,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n0,n1)),true,equalish(X4,n0),true) ).
cnf(u27,axiom,
true = ifeq(f(X0,X1,n0,X2,X3,X4),true,ifeq(f(X5,X6,n0,X7,X8,X4),true,true,true),true) ).
cnf(u4878,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n1,n0)),true,equalish(X0,n0),true) ).
cnf(u3923,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n0,X1,n0,X0,n0,sK1_relation_exists_F(n0,X1,n0,X0,n0)),true),true) ).
cnf(u1057,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n0,n1)),true,equalish(n0,X0),true) ).
cnf(n0_and_n1_reflexive_1,axiom,
equalish(n0,n0) = true ).
cnf(u3713,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,X0,n1,n0,X1,sK1_relation_exists_F(n0,X0,n1,n0,X1)),true),true) ).
cnf(u3204,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,X0,n0,n0,n0,sK1_relation_exists_F(n1,X0,n0,n0,n0)),true) ).
cnf(u6311,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,X0,n1,n0,n1,sK1_relation_exists_F(n0,X0,n1,n0,n1)),true) ).
cnf(u1032,axiom,
true = f(n1,n1,n0,n0,n0,sK1_relation_exists_F(n1,n1,n0,n0,n0)) ).
cnf(u25,axiom,
true = ifeq(f(X0,X1,X2,n0,X3,X4),true,ifeq(f(X5,X6,X7,n0,X8,X4),true,true,true),true) ).
cnf(u155,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n1,n0)),true,equalish(n1,X3),true) ).
cnf(u52,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X3,X3),true,f(X3,X2,X1,X0,n0,sK1_relation_exists_F(X3,X2,X1,X0,n0)),true),true),true),true) ).
cnf(u1440,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X0,X0),true,f(X0,X2,X1,n1,n1,sK1_relation_exists_F(X0,X2,X1,n1,n1)),true),true),true) ).
cnf(u31,axiom,
true = ifeq(f(n0,X0,X1,X2,X3,X4),true,ifeq(f(n0,X5,X6,X7,X8,X4),true,true,true),true) ).
cnf(u153,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n1,n0)),true,equalish(n1,X2),true) ).
cnf(u2594,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n0,n1)),true,equalish(X0,n1),true) ).
cnf(u3370,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n1,n0)),true,equalish(X2,n0),true) ).
cnf(u4265,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n0,n1)),true,equalish(n0,X0),true) ).
cnf(u5044,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n0,n1)),true,equalish(X0,n1),true) ).
cnf(u159,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n1,n0)),true,equalish(n1,X1),true) ).
cnf(u1854,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n0,n1)),true,equalish(X4,n0),true) ).
cnf(u6575,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n0,n1,n1,n1,sK1_relation_exists_F(X0,n0,n1,n1,n1)),true) ).
cnf(u2354,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n0,n0,X0,n0,sK1_relation_exists_F(n1,n0,n0,X0,n0)),true) ).
cnf(u1689,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n1,n0)),true,equalish(n0,X4),true) ).
cnf(u4772,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n1,X0,n0,n0,sK1_relation_exists_F(n0,n1,X0,n0,n0)),true) ).
cnf(u6847,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,X1,n0,n1,n1,sK1_relation_exists_F(X0,X1,n0,n1,n1)),true),true) ).
cnf(u5801,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n0,n0)),true,equalish(n0,X2),true) ).
cnf(u5555,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n1,n1)),true,equalish(n0,X2),true) ).
cnf(u5805,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n0,n0)),true,equalish(n0,X0),true) ).
cnf(u1860,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n0,n1)),true,equalish(X0,n1),true) ).
cnf(u3576,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n0,n0)),true,equalish(X2,n0),true) ).
cnf(u1858,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n0,n1)),true,equalish(X3,n0),true) ).
cnf(u5809,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n0,n0)),true,equalish(n0,X4),true) ).
cnf(u5563,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n1,n1)),true,equalish(n1,X4),true) ).
cnf(u326,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n0,n1)),true,equalish(X4,n1),true) ).
cnf(u2632,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u6576,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n0,n1,n1,n0,sK1_relation_exists_F(X0,n0,n1,n1,n0)),true) ).
cnf(u6715,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n0,X1,n0,n1,sK1_relation_exists_F(X0,n0,X1,n0,n1)),true),true) ).
cnf(u1615,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n0,n1,X0,n1,sK1_relation_exists_F(n1,n0,n1,X0,n1)),true) ).
cnf(u2420,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n1,n0)),true,equalish(X2,n1),true) ).
cnf(u324,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n0,n1)),true,equalish(X2,n1),true) ).
cnf(u1614,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n0,n1,n0,X0,sK1_relation_exists_F(n1,n0,n1,n0,X0)),true) ).
cnf(u80,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n1,n1,X1,X0,n0,sK1_relation_exists_F(n1,n1,X1,X0,n0)),true),true) ).
cnf(u4449,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,X0,X1,n0,n1,sK1_relation_exists_F(n0,X0,X1,n0,n1)),true),true) ).
cnf(u4456,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n1,n0,n1,n1)),true,true,true) ).
cnf(u1620,axiom,
true = f(n1,n0,n1,n1,n0,sK1_relation_exists_F(n1,n0,n1,n1,n0)) ).
cnf(u851,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n1,n1)),true,equalish(n1,X4),true) ).
cnf(u3144,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,X0,n1,n0,n0,sK1_relation_exists_F(n1,X0,n1,n0,n0)),true) ).
cnf(u1743,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(X2,X1,X0,n0,n0,sK1_relation_exists_F(X2,X1,X0,n0,n0)),true),true),true) ).
cnf(u2499,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,X0,n1,X1,n1,sK1_relation_exists_F(n1,X0,n1,X1,n1)),true),true) ).
cnf(u86,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n1,n1,n0,X0,sK1_relation_exists_F(n1,n1,n1,n0,X0)),true) ).
cnf(u6768,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,X0,n1,n1,n0,sK1_relation_exists_F(X1,X0,n1,n1,n0)),true),true) ).
cnf(u3920,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,X0,n0,n1,X1,sK1_relation_exists_F(n0,X0,n0,n1,X1)),true),true) ).
cnf(u364,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n0,n0)),true,equalish(X2,n1),true) ).
cnf(u6860,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,X0,n0,n0,n0,sK1_relation_exists_F(X1,X0,n0,n0,n0)),true),true) ).
cnf(u3303,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n1,n1,X0,n1,sK1_relation_exists_F(n0,n1,n1,X0,n1)),true) ).
cnf(u5209,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n1,n1,X1,n1,sK1_relation_exists_F(X0,n1,n1,X1,n1)),true),true) ).
cnf(u3292,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n0,n1,n0,X1,X0,sK1_relation_exists_F(n0,n1,n0,X1,X0)),true),true) ).
cnf(u237,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n0,X2,X1,X0,n1,sK1_relation_exists_F(n0,X2,X1,X0,n1)),true),true),true) ).
cnf(u492,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X0,X0),true,f(X0,n1,X2,X1,n1,sK1_relation_exists_F(X0,n1,X2,X1,n1)),true),true),true) ).
cnf(u3307,axiom,
true = f(n0,n1,n1,n1,n1,sK1_relation_exists_F(n0,n1,n1,n1,n1)) ).
cnf(u3296,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n0,n1,X1,X0,n0,sK1_relation_exists_F(n0,n1,X1,X0,n0)),true),true) ).
cnf(u6263,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n0,X0,n0,n1,sK1_relation_exists_F(n0,n0,X0,n0,n1)),true) ).
cnf(u2380,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n1,n1)),true,equalish(X2,n1),true) ).
cnf(u2924,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n0,n0,n0,n1)),true,true,true) ).
cnf(u2422,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n1,n0)),true,equalish(X4,n0),true) ).
cnf(u6264,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n0,X0,n0,n0,sK1_relation_exists_F(n0,n0,X0,n0,n0)),true) ).
cnf(u4305,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n0,n0)),true,equalish(n0,X0),true) ).
cnf(u5084,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n0,n0)),true,equalish(X0,n0),true) ).
cnf(u2280,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n0,n1,n0,n0)),true,true,true) ).
cnf(u3575,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n0,n0)),true,equalish(n0,X2),true) ).
cnf(u4098,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n1,n0)),true,equalish(X4,n1),true) ).
cnf(u371,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n0,n0)),true,equalish(n0,X4),true) ).
cnf(u3188,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,X0,n0,n1,n0,sK1_relation_exists_F(n1,X0,n0,n1,n0)),true) ).
cnf(u114,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n1,n1)),true,equalish(X2,n1),true) ).
cnf(u4217,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,X0,X1,n1,n1,sK1_relation_exists_F(n0,X0,X1,n1,n1)),true),true) ).
cnf(u3579,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n0,n0)),true,equalish(n1,X0),true) ).
cnf(u49,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X3,X3),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X0,X0),true,f(X0,X2,X3,n1,X1,sK1_relation_exists_F(X0,X2,X3,n1,X1)),true),true),true),true) ).
cnf(u3330,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n1,n1)),true,equalish(X2,n0),true) ).
cnf(u1613,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n0,n1,n1,X0,sK1_relation_exists_F(n1,n0,n1,n1,X0)),true) ).
cnf(u3582,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u26,axiom,
true = ifeq(f(X2,X3,X0,n1,X7,X8),true,ifeq(f(X5,X6,X4,n1,X1,X8),true,true,true),true) ).
cnf(u2591,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n0,n1)),true,equalish(n0,X1),true) ).
cnf(u3730,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n1,n1,n1,n1)),true,true,true) ).
cnf(u6451,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n1,n1,n0,n1,sK1_relation_exists_F(X0,n1,n1,n0,n1)),true) ).
cnf(u3478,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,n0,X0,n0,X1,sK1_relation_exists_F(n0,n0,X0,n0,X1)),true),true) ).
cnf(u1056,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n0,n1)),true,equalish(X4,n1),true) ).
cnf(u2351,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n0,n0,n1,X0,sK1_relation_exists_F(n1,n0,n0,n1,X0)),true) ).
cnf(u4104,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n1,n0)),true,equalish(X0,n0),true) ).
cnf(u3479,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,n0,X0,X1,n1,sK1_relation_exists_F(n0,n0,X0,X1,n1)),true),true) ).
cnf(u24,axiom,
true = ifeq(f(X2,X3,X0,X1,n1,X8),true,ifeq(f(X5,X7,X4,X6,n1,X8),true,true,true),true) ).
cnf(u154,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n1,n0)),true,equalish(X2,n1),true) ).
cnf(u1441,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(X2,X1,X0,n1,n0,sK1_relation_exists_F(X2,X1,X0,n1,n0)),true),true),true) ).
cnf(u6565,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n0,n1,n1,X0,sK1_relation_exists_F(X1,n0,n1,n1,X0)),true),true) ).
cnf(u5527,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n0,n0,n1,X0,sK1_relation_exists_F(n0,n0,n0,n1,X0)),true) ).
cnf(u4771,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n1,X0,n0,n1,sK1_relation_exists_F(n0,n1,X0,n0,n1)),true) ).
cnf(u2589,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n0,n1)),true,equalish(n0,X0),true) ).
cnf(u5770,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n0,n1)),true,equalish(X0,n1),true) ).
cnf(u6435,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n1,n1,n1,n1,sK1_relation_exists_F(X0,n1,n1,n1,n1)),true) ).
cnf(u816,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,n1,n0,n0,X0,sK1_relation_exists_F(n1,n1,n0,n0,X0)),true) ).
cnf(u1690,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n1,n0)),true,equalish(X0,n0),true) ).
cnf(u5804,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n0,n0)),true,equalish(X4,n0),true) ).
cnf(u5035,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n0,n1)),true,equalish(n0,X2),true) ).
cnf(u5807,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n0,n0)),true,equalish(n0,X1),true) ).
cnf(u5806,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n0,n0)),true,equalish(X1,n0),true) ).
cnf(u1853,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n0,n1)),true,equalish(n0,X3),true) ).
cnf(u5808,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u588,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n1,n1,n1,n0)),true,true,true) ).
cnf(u681,axiom,
true = ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n0,X1,n1,X2,sK1_relation_exists_F(X0,n0,X1,n1,X2)),true),true),true) ).
cnf(u1851,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n0,n1)),true,equalish(n1,X2),true) ).
cnf(u64,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n1,X2,n0,X1,X0,sK1_relation_exists_F(n1,X2,n0,X1,X0)),true),true),true) ).
cnf(u5810,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n0,n0)),true,equalish(X0,n0),true) ).
cnf(u3513,axiom,
true = f(n0,n1,n1,n0,n1,sK1_relation_exists_F(n0,n1,n1,n0,n1)) ).
cnf(u1604,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n1,n0,n0,X1,X0,sK1_relation_exists_F(n1,n0,n0,X1,X0)),true),true) ).
cnf(u2749,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,X0,n0,n0,X1,sK1_relation_exists_F(n1,X0,n0,n0,X1)),true),true) ).
cnf(u327,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n0,n1)),true,equalish(n1,X0),true) ).
cnf(u1619,axiom,
true = f(n1,n0,n1,n1,n1,sK1_relation_exists_F(n1,n0,n1,n1,n1)) ).
cnf(u4028,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,n1,n0,n0,X0,sK1_relation_exists_F(n0,n1,n0,n0,X0)),true) ).
cnf(u6587,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n0,n0,X1,n1,sK1_relation_exists_F(X0,n0,n0,X1,n1)),true),true) ).
cnf(u1608,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n1,n0,X1,X0,n0,sK1_relation_exists_F(n1,n0,X1,X0,n0)),true),true) ).
cnf(u3159,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,X0,X1,n0,n1,sK1_relation_exists_F(n1,X0,X1,n0,n1)),true),true) ).
cnf(u850,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u1857,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n0,n1)),true,equalish(n0,X1),true) ).
cnf(u2379,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n1,n1)),true,equalish(n1,X2),true) ).
cnf(u4304,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n0,n0)),true,equalish(X4,n1),true) ).
cnf(u325,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n0,n1)),true,equalish(n1,X3),true) ).
cnf(u4807,axiom,
true = f(n0,n0,n1,n1,n1,sK1_relation_exists_F(n0,n0,n1,n1,n1)) ).
cnf(u5075,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n0,n0)),true,equalish(n0,X2),true) ).
cnf(u3294,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,n1,X0,n0,X1,sK1_relation_exists_F(n0,n1,X0,n0,X1)),true),true) ).
cnf(u68,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n1,X2,X1,X0,n0,sK1_relation_exists_F(n1,X2,X1,X0,n0)),true),true),true) ).
cnf(u2382,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n1,n1)),true,equalish(X4,n0),true) ).
cnf(u4301,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n0,n0)),true,equalish(n0,X2),true) ).
cnf(u852,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n1,n1)),true,equalish(X0,n1),true) ).
cnf(u1644,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n1,n1)),true,equalish(X4,n0),true) ).
cnf(u6859,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,X1,n0,n0,n1,sK1_relation_exists_F(X0,X1,n0,n0,n1)),true),true) ).
cnf(u4310,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n0,n0)),true,equalish(X0,n0),true) ).
cnf(u1893,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n0,n0)),true,equalish(n0,X3),true) ).
cnf(u367,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n0,n0)),true,equalish(n1,X0),true) ).
cnf(u3537,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n0,n1)),true,equalish(n1,X3),true) ).
cnf(u3291,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n0,n1,n1,X1,X0,sK1_relation_exists_F(n0,n1,n1,X1,X0)),true),true) ).
cnf(u4450,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n0,X1,X0,n0,n0,sK1_relation_exists_F(n0,X1,X0,n0,n0)),true),true) ).
cnf(u4833,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n1,n1)),true,equalish(n1,X0),true) ).
cnf(u3956,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n1,n1,n0,n0)),true,true,true) ).
cnf(u4308,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u3539,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n0,n1)),true,equalish(n1,X0),true) ).
cnf(u365,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n0,n0)),true,equalish(n1,X3),true) ).
cnf(u6344,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,X0,n0,n1,n0,sK1_relation_exists_F(n0,X0,n0,n1,n0)),true) ).
cnf(u238,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n0,X2,X1,X0,n0,sK1_relation_exists_F(n0,X2,X1,X0,n0)),true),true),true) ).
cnf(u6500,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n1,n0,n0,n0,sK1_relation_exists_F(X0,n1,n0,n0,n0)),true) ).
cnf(u493,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(X2,n1,X1,X0,n0,sK1_relation_exists_F(X2,n1,X1,X0,n0)),true),true),true) ).
cnf(u744,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n1,n1,n0,n0)),true,true,true) ).
cnf(u236,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n0,X2,X1,n0,X0,sK1_relation_exists_F(n0,X2,X1,n0,X0)),true),true),true) ).
cnf(u3187,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,X0,n0,n1,n1,sK1_relation_exists_F(n1,X0,n0,n1,n1)),true) ).
cnf(u121,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n1,n1,n1)),true,equalish(n1,X4),true) ).
cnf(u4100,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n1,n0)),true,equalish(X1,n0),true) ).
cnf(u4306,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n0,n0)),true,equalish(X1,n0),true) ).
cnf(u1252,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n1,n0,n1,n1)),true,true,true) ).
cnf(u5408,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n1,n0,n0,X0,sK1_relation_exists_F(X1,n1,n0,n0,X0)),true),true) ).
cnf(u1031,axiom,
true = f(n1,n1,n0,n0,n1,sK1_relation_exists_F(n1,n1,n0,n0,n1)) ).
cnf(u20,axiom,
true = ifeq(f(X0,X1,X2,X3,X4,X5),true,ifeq(f(X6,X7,X8,X9,X10,X5),true,equalish(X6,X0),true),true) ).
cnf(u3334,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n1,n1)),true,equalish(X1,n1),true) ).
cnf(u10,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X3,X3),true,ifeq(equalish(X4,X4),true,f(X4,X3,X2,X1,X0,sK1_relation_exists_F(X4,X3,X2,X1,X0)),true),true),true),true),true) ).
cnf(u3714,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n0,X0,n1,X1,n1,sK1_relation_exists_F(n0,X0,n1,X1,n1)),true),true) ).
cnf(u6652,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n0,n0,n0,n0,sK1_relation_exists_F(X0,n0,n0,n0,n0)),true) ).
cnf(u6687,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n0,X1,n1,n1,sK1_relation_exists_F(X0,n0,X1,n1,n1)),true),true) ).
cnf(u5409,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n1,n0,X1,n1,sK1_relation_exists_F(X0,n1,n0,X1,n1)),true),true) ).
cnf(u4095,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n1,n0)),true,equalish(n0,X2),true) ).
cnf(u6028,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n0,n0,n1,n0)),true,true,true) ).
cnf(u5533,axiom,
true = f(n0,n0,n0,n1,n1,sK1_relation_exists_F(n0,n0,n0,n1,n1)) ).
cnf(u8,axiom,
true = ifeq(equalish(n1,n0),true,goal,true) ).
cnf(u5076,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n0,n0)),true,equalish(X2,n0),true) ).
cnf(u4874,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n1,n0)),true,equalish(X1,n1),true) ).
cnf(u5769,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n0,n1)),true,equalish(n1,X4),true) ).
cnf(u3476,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n0,n0,n0,X1,X0,sK1_relation_exists_F(n0,n0,n0,X1,X0)),true),true) ).
cnf(u3372,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n1,n0)),true,equalish(X4,n1),true) ).
cnf(u1891,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n0,n0)),true,equalish(n1,X2),true) ).
cnf(u1897,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n0,n0)),true,equalish(n0,X1),true) ).
cnf(u3480,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n0,n0,X1,X0,n0,sK1_relation_exists_F(n0,n0,X1,X0,n0)),true),true) ).
cnf(u821,axiom,
true = f(n1,n1,n0,n1,n1,sK1_relation_exists_F(n1,n1,n0,n1,n1)) ).
cnf(u48,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X3,X3),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X0,X0),true,f(X0,X2,n0,X3,X1,sK1_relation_exists_F(X0,X2,n0,X3,X1)),true),true),true),true) ).
cnf(u234,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n0,X2,n0,X1,X0,sK1_relation_exists_F(n0,X2,n0,X1,X0)),true),true),true) ).
cnf(u3369,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n1,n0)),true,equalish(n0,X2),true) ).
cnf(u5803,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n0,n0)),true,equalish(n0,X3),true) ).
cnf(u6716,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n0,X0,n0,n0,sK1_relation_exists_F(X1,n0,X0,n0,n0)),true),true) ).
cnf(u5040,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n0,n1)),true,equalish(X1,n1),true) ).
cnf(u6586,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n0,n0,n0,X0,sK1_relation_exists_F(X1,n0,n0,n0,X0)),true),true) ).
cnf(u679,axiom,
true = ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n0,n1,X1,X2,sK1_relation_exists_F(X0,n0,n1,X1,X2)),true),true),true) ).
cnf(u1605,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,n0,X0,n1,X1,sK1_relation_exists_F(n1,n0,X0,n1,X1)),true),true) ).
cnf(u4262,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n0,n1)),true,equalish(X2,n0),true) ).
cnf(u6568,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n0,n1,X0,n0,sK1_relation_exists_F(X1,n0,n1,X0,n0)),true),true) ).
cnf(u1855,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n0,n1)),true,equalish(n1,X0),true) ).
cnf(u5042,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n0,n1)),true,equalish(X3,n0),true) ).
cnf(u1603,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n1,n0,n1,X1,X0,sK1_relation_exists_F(n1,n0,n1,X1,X0)),true),true) ).
cnf(u4267,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n0,n1)),true,equalish(n0,X1),true) ).
cnf(u3143,axiom,
true = ifeq(equalish(X0,X0),true,f(n1,X0,n1,n0,n1,sK1_relation_exists_F(n1,X0,n1,n0,n1)),true) ).
cnf(u682,axiom,
true = ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n0,X1,n0,X2,sK1_relation_exists_F(X0,n0,X1,n0,X2)),true),true),true) ).
cnf(u77,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(n1,n1,X0,n1,X1,sK1_relation_exists_F(n1,n1,X0,n1,X1)),true),true) ).
cnf(u1687,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n1,n0)),true,equalish(n1,X1),true) ).
cnf(u332,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n0,n1)),true,equalish(X0,n1),true) ).
cnf(u1093,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n0,n0)),true,equalish(n1,X2),true) ).
cnf(u4684,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n1,n0,n0,n0)),true,true,true) ).
cnf(u6585,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(X1,n0,n0,n1,X0,sK1_relation_exists_F(X1,n0,n0,n1,X0)),true),true) ).
cnf(u67,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n1,X2,X1,X0,n1,sK1_relation_exists_F(n1,X2,X1,X0,n1)),true),true),true) ).
cnf(u2384,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n1,n1)),true,equalish(X1,n0),true) ).
cnf(u1097,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n0,n0)),true,equalish(n0,X0),true) ).
cnf(u6603,axiom,
true = ifeq(equalish(X0,X0),true,f(X0,n0,n1,n0,n1,sK1_relation_exists_F(X0,n0,n1,n0,n1)),true) ).
cnf(u4261,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n0,n1)),true,equalish(n0,X2),true) ).
cnf(u2120,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n0,n1,n1,n0)),true,true,true) ).
cnf(u1482,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n1,n1,n0,n0,n0)),true,true,true) ).
cnf(u65,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n1,X2,X1,n1,X0,sK1_relation_exists_F(n1,X2,X1,n1,X0)),true),true),true) ).
cnf(u844,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n1,n1)),true,equalish(X2,n1),true) ).
cnf(u4302,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n0,n0)),true,equalish(X2,n0),true) ).
cnf(u4831,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n1,n1)),true,equalish(n0,X3),true) ).
cnf(u849,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n1,n1)),true,equalish(n1,X1),true) ).
cnf(u92,axiom,
true = f(n1,n1,n1,n1,n0,sK1_relation_exists_F(n1,n1,n1,n1,n0)) ).
cnf(u4307,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n0,n0)),true,equalish(n0,X1),true) ).
cnf(u4062,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u4808,axiom,
true = f(n0,n0,n1,n1,n0,sK1_relation_exists_F(n0,n0,n1,n1,n0)) ).
cnf(u3543,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n1,n0,n1)),true,equalish(n1,X4),true) ).
cnf(u5078,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n0,n0)),true,equalish(X4,n0),true) ).
cnf(u4834,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n1,n1,n1)),true,equalish(X1,n1),true) ).
cnf(u5596,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n1,n0)),true,equalish(X2,n0),true) ).
cnf(u5230,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n0,n1,n1,n1)),true,true,true) ).
cnf(u991,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,ifeq(equalish(X0,X0),true,f(X0,X2,n1,X1,n1,sK1_relation_exists_F(X0,X2,n1,X1,n1)),true),true),true) ).
cnf(u884,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n1,n0)),true,equalish(X2,n1),true) ).
cnf(u235,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n0,X2,X1,n1,X0,sK1_relation_exists_F(n0,X2,X1,n1,X0)),true),true),true) ).
cnf(u4,axiom,
true = equalish(n1,n1) ).
cnf(u1894,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n0,n0)),true,equalish(X4,n0),true) ).
cnf(u5600,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n0,n0,n1,n0)),true,equalish(X1,n0),true) ).
cnf(u2423,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n1,n0)),true,equalish(n0,X0),true) ).
cnf(u490,axiom,
true = ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n1,X1,n1,X2,sK1_relation_exists_F(X0,n1,X1,n1,X2)),true),true),true) ).
cnf(u889,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n1,n0)),true,equalish(n1,X1),true) ).
cnf(u4055,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n1,n1)),true,equalish(n0,X2),true) ).
cnf(u1900,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n0,n0)),true,equalish(X0,n0),true) ).
cnf(u4061,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n1,n1)),true,equalish(n1,X1),true) ).
cnf(u4873,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n1,n0)),true,equalish(n1,X0),true) ).
cnf(u6767,axiom,
true = ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,X1,n1,n1,n1,sK1_relation_exists_F(X0,X1,n1,n1,n1)),true),true) ).
cnf(u1898,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n1,n0,n0)),true,equalish(X3,n0),true) ).
cnf(u233,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X2,X2),true,f(n0,X2,n1,X1,X0,sK1_relation_exists_F(n0,X2,n1,X1,X0)),true),true),true) ).
cnf(u2428,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n0,n0,n1,n0)),true,equalish(X0,n0),true) ).
cnf(u4059,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n1,n0,n1,n1)),true,equalish(n0,X0),true) ).
cnf(u366,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n0,n0)),true,equalish(X4,n1),true) ).
cnf(u2421,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n0,n1,n0)),true,equalish(n0,X3),true) ).
cnf(u488,axiom,
true = ifeq(equalish(X2,X2),true,ifeq(equalish(X1,X1),true,ifeq(equalish(X0,X0),true,f(X0,n1,n1,X1,X2,sK1_relation_exists_F(X0,n1,n1,X1,X2)),true),true),true) ).
cnf(u122,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n1,n1)),true,equalish(X0,n1),true) ).
cnf(u3536,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n0,n1)),true,equalish(X2,n0),true) ).
cnf(u1641,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n0,n1,n1,n1)),true,equalish(n1,X2),true) ).
cnf(u4600,axiom,
true = ifeq(f(X6,X7,X4,X5,X2,sK1_relation_exists_F(n0,n1,n0,n0,n1)),true,true,true) ).
cnf(u2946,axiom,
true = ifeq(equalish(X0,X0),true,ifeq(equalish(X1,X1),true,f(n1,X1,X0,n1,n0,sK1_relation_exists_F(n1,X1,X0,n1,n0)),true),true) ).
cnf(u3332,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n1,n1)),true,equalish(X4,n1),true) ).
cnf(u6372,axiom,
true = ifeq(equalish(X0,X0),true,f(n0,X0,n0,n0,n0,sK1_relation_exists_F(n0,X0,n0,n0,n0)),true) ).
cnf(u5603,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n0,n1,n0)),true,equalish(n0,X4),true) ).
cnf(u120,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n1,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u3578,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n0,n0)),true,equalish(X4,n1),true) ).
cnf(u4270,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n0,n0,n1)),true,equalish(X0,n1),true) ).
cnf(u891,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n1,n1,n0,n1,n0)),true,equalish(n0,X4),true) ).
cnf(u3336,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n0,n1,n1,n1,n1)),true,equalish(X3,n1),true) ).
cnf(u23,axiom,
true = ifeq(f(X0,X1,X2,X3,n0,X4),true,ifeq(f(X5,X6,X7,X8,n0,X4),true,true,true),true) ).
cnf(u1060,axiom,
true = ifeq(f(X2,X4,X1,X3,X0,sK1_relation_exists_F(n1,n1,n0,n0,n1)),true,equalish(X3,n0),true) ).
cnf(u4875,axiom,
true = ifeq(f(X2,X3,X0,X1,X4,sK1_relation_exists_F(n0,n0,n1,n1,n0)),true,equalish(n1,X1),true) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MSC013-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 % Computer : n010.cluster.edu
% 0.11/0.40 % Model : x86_64 x86_64
% 0.11/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.40 % Memory : 8046.5625MB
% 0.11/0.40 % OS : Linux 6.8.0-71-generic
% 0.11/0.40 % CPULimit : 300
% 0.11/0.40 % WCLimit : 300
% 0.11/0.40 % DateTime : Sun Sep 27 17:42:02 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.44 Running first-order theorem proving
% 0.11/0.44 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.96/2.86 % (1192368)Detected a unit-equality problem, will run specialized UEQ schedule.
% 13.96/2.86 % (1192376)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=771191770:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 13.96/2.86 % (1192377)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2524742095:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 13.96/2.86 % (1192379)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1315910889:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 13.96/2.86 % (1192373)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=328150752:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 13.96/2.86 % (1192378)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2714950803:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 13.96/2.86 % (1192375)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=100571499:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 13.96/2.86 % (1192374)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=1350950670:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 13.96/2.86 % (1192376)Instruction limit reached!
% 13.96/2.86 % (1192376)------------------------------
% 13.96/2.86 % (1192376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/2.86 % (1192376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.86 % (1192376)CaDiCaL version: 2.1.3
% 13.96/2.86 % (1192376)Termination reason: Instruction limit
% 13.96/2.86 % (1192376)Termination phase: Saturation
% 13.96/2.86 % (1192376)Time elapsed: 0.040 s
% 13.96/2.86 % (1192376)Peak memory usage: 87 MB
% 13.96/2.86 % (1192376)Instructions burned: 136 (million)
% 13.96/2.86 % (1192377)Instruction limit reached!
% 13.96/2.86 % (1192377)------------------------------
% 13.96/2.86 % (1192377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/2.86 % (1192377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.86 % (1192377)CaDiCaL version: 2.1.3
% 13.96/2.86 % (1192377)Termination reason: Instruction limit
% 13.96/2.86 % (1192377)Termination phase: Saturation
% 13.96/2.86 % (1192377)Time elapsed: 0.087 s
% 13.96/2.86 % (1192377)Peak memory usage: 87 MB
% 13.96/2.86 % (1192377)Instructions burned: 182 (million)
% 13.96/2.86 % (1192387)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3189631123:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 13.96/2.86 % (1192378)Instruction limit reached!
% 13.96/2.86 % (1192378)------------------------------
% 13.96/2.86 % (1192378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/2.86 % (1192378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.86 % (1192378)CaDiCaL version: 2.1.3
% 13.96/2.86 % (1192378)Termination reason: Instruction limit
% 13.96/2.86 % (1192378)Termination phase: Saturation
% 13.96/2.86 % (1192378)Time elapsed: 0.141 s
% 13.96/2.86 % (1192378)Peak memory usage: 89 MB
% 13.96/2.86 % (1192378)Instructions burned: 259 (million)
% 13.96/2.86 % (1192388)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1991392148:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 13.96/2.86 % (1192390)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3038462814:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 13.96/2.86 % (1192390)Instruction limit reached!
% 13.96/2.86 % (1192390)------------------------------
% 13.96/2.86 % (1192390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/2.86 % (1192390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.86 % (1192390)CaDiCaL version: 2.1.3
% 13.96/2.86 % (1192390)Termination reason: Instruction limit
% 13.96/2.86 % (1192390)Termination phase: Saturation
% 13.96/2.86 % (1192390)Time elapsed: 0.099 s
% 13.96/2.86 % (1192390)Peak memory usage: 88 MB
% 13.96/2.86 % (1192390)Instructions burned: 217 (million)
% 13.96/2.86 % (1192393)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=2948954779: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)
% 13.96/2.86 % (1192379)Refutation not found, incomplete strategy
% 13.96/2.86 % (1192379)------------------------------
% 13.96/2.86 % (1192379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/2.86 % (1192379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.86 % (1192379)CaDiCaL version: 2.1.3
% 13.96/2.86 % (1192379)Termination reason: Refutation not found, incomplete strategy
% 13.96/2.86 % (1192379)Time elapsed: 0.576 s
% 13.96/2.86 % (1192379)Peak memory usage: 93 MB
% 13.96/2.86 % (1192379)Instructions burned: 1095 (million)
% 13.96/2.86 % (1192393)Instruction limit reached!
% 13.96/2.86 % (1192393)------------------------------
% 13.96/2.86 % (1192393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/2.86 % (1192393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.86 % (1192393)CaDiCaL version: 2.1.3
% 13.96/2.86 % (1192393)Termination reason: Instruction limit
% 13.96/2.86 % (1192393)Termination phase: Saturation
% 13.96/2.86 % (1192393)Time elapsed: 0.181 s
% 13.96/2.86 % (1192393)Peak memory usage: 91 MB
% 13.96/2.86 % (1192393)Instructions burned: 318 (million)
% 13.96/2.86 % (1192379)------------------------------
% 13.96/2.86 % (1192379)------------------------------
% 13.96/2.86 % (1192387)Instruction limit reached!
% 13.96/2.86 % (1192387)------------------------------
% 13.96/2.86 % (1192387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/2.86 % (1192387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.86 % (1192387)CaDiCaL version: 2.1.3
% 13.96/2.86 % (1192387)Termination reason: Instruction limit
% 13.96/2.86 % (1192387)Termination phase: Saturation
% 13.96/2.86 % (1192387)Time elapsed: 0.725 s
% 13.96/2.86 % (1192387)Peak memory usage: 140 MB
% 13.96/2.86 % (1192387)Instructions burned: 2053 (million)
% 13.96/2.86 % (1192395)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=204283488:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/12125Mi)
% 13.96/2.86 % (1192396)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3869832046:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 13.96/2.86 % (1192397)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2307536261:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 13.96/2.86 % (1192396)First to succeed.
% 13.96/2.86 % (1192396)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1192368"
% 13.96/2.86 % (1192373)Refutation not found, incomplete strategy
% 13.96/2.86 % (1192373)------------------------------
% 13.96/2.86 % (1192373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/2.86 % (1192373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.86 % (1192373)CaDiCaL version: 2.1.3
% 13.96/2.86 % (1192373)Termination reason: Refutation not found, incomplete strategy
% 13.96/2.86 % (1192373)Time elapsed: 1.579 s
% 13.96/2.86 % (1192373)Peak memory usage: 138 MB
% 13.96/2.86 % (1192373)Instructions burned: 2521 (million)
% 13.96/2.86 % (1192374)Also succeeded, but the first one will report.
% 13.96/2.86 % (1192375)Also succeeded, but the first one will report.
% 13.96/2.86 % (1192388)Also succeeded, but the first one will report.
% 13.96/2.86 % SZS status Satisfiable for theBenchmark
% 13.96/2.86 % SZS output start Saturation.
% See solution above
% 14.55/3.06 % SZS output start Definitions and Model Updates.
% 14.55/3.06 % SZS output end Definitions and Model Updates.
% 14.55/3.06 % (1192396)------------------------------
% 14.55/3.06 % (1192396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/3.06 % (1192396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/3.06 % (1192396)CaDiCaL version: 2.1.3
% 14.55/3.06 % (1192396)Termination reason: Satisfiable
% 14.55/3.06 % (1192396)Time elapsed: 0.567 s
% 14.55/3.06 % (1192396)Peak memory usage: 99 MB
% 14.55/3.06 % (1192396)Instructions burned: 924 (million)
% 14.55/3.06 % (1192396)------------------------------
% 14.55/3.06 % (1192396)------------------------------
% 14.55/3.06 % (1192368)Success in time 1.978 s
% 14.55/3.06 % Vampire exiting
%------------------------------------------------------------------------------