%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MSC014-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Thu Sep 24 01:28:22 PM UTC 2026
% Result : Satisfiable 0.17s 0.65s
% Output : Saturation 0.17s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : ifeq2(A,A,B,C) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B,C] : ifeq(A,A,B,C) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
equalish(n0,n0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
equalish(n1,n1) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X4,X3,X2,X1] : ifeq2(equalish(X4,X4),true,ifeq2(equalish(X3,X3),true,ifeq2(equalish(X2,X2),true,ifeq2(equalish(X1,X1),true,f(X1,X2,X3,X4,sK1_exists_f_Z(X1,X2,X3,X4)),true),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [Y1,Y2,Y3,Y4,Z,X1,X2,X3,X4] : ifeq2(f(Y1,Y2,Y3,Y4,Z),true,ifeq2(f(X1,X2,X3,X4,Z),true,equalish(X4,Y4),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [Y1,Y2,Y3,Y4,Z,X1,X2,X3,X4] : ifeq2(f(Y1,Y2,Y3,Y4,Z),true,ifeq2(f(X1,X2,X3,X4,Z),true,equalish(X3,Y3),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [Y1,Y2,Y3,Y4,Z,X1,X2,X3,X4] : ifeq2(f(Y1,Y2,Y3,Y4,Z),true,ifeq2(f(X1,X2,X3,X4,Z),true,equalish(X2,Y2),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [Y1,Y2,Y3,Y4,Z,X1,X2,X3,X4] : ifeq2(f(Y1,Y2,Y3,Y4,Z),true,ifeq2(f(X1,X2,X3,X4,Z),true,equalish(X1,Y1),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
ifeq(equalish(n0,n1),true,a,b) = b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
ifeq(equalish(n1,n0),true,a,b) = b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,negated_conjecture,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,plain,
! [X0,X1,X2] : ifeq2(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f14,plain,
! [X0,X1,X2] : ifeq(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f15,plain,
equalish(n0,n0) = true,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f16,plain,
equalish(n1,n1) = true,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f17,plain,
! [X0,X1,X2,X3] : 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) = true,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f18,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : ifeq2(f(X0,X1,X2,X3,X4),true,ifeq2(f(X5,X6,X7,X8,X4),true,equalish(X8,X3),true),true) = true,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f19,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : ifeq2(f(X0,X1,X2,X3,X4),true,ifeq2(f(X5,X6,X7,X8,X4),true,equalish(X7,X2),true),true) = true,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f20,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : ifeq2(f(X0,X1,X2,X3,X4),true,ifeq2(f(X5,X6,X7,X8,X4),true,equalish(X6,X1),true),true) = true,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f21,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : ifeq2(f(X0,X1,X2,X3,X4),true,ifeq2(f(X5,X6,X7,X8,X4),true,equalish(X5,X0),true),true) = true,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f22,plain,
ifeq(equalish(n0,n1),true,a,b) = b,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f23,plain,
ifeq(equalish(n1,n0),true,a,b) = b,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f24,plain,
a != b,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f25,plain,
! [X0,X1,X2] : ifeq2(true,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),true) = true,
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f26,plain,
! [X0,X1,X2] : ifeq2(true,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),true) = true,
inference(paramodulation,[status(thm)],[f15,f17]) ).
fof(f27,plain,
! [X0,X1,X2] : ifeq2(equalish(X0,X0),true,ifeq2(true,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),true) = true,
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f28,plain,
! [X0,X1,X2] : ifeq2(equalish(X0,X0),true,ifeq2(true,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),true) = true,
inference(paramodulation,[status(thm)],[f15,f17]) ).
fof(f29,plain,
! [X0,X1,X2] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,ifeq2(equalish(X2,X2),true,f(X2,n1,X1,X0,sK1_exists_f_Z(X2,n1,X1,X0)),true),true),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f30,plain,
! [X0,X1,X2] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,ifeq2(equalish(X2,X2),true,f(X2,n0,X1,X0,sK1_exists_f_Z(X2,n0,X1,X0)),true),true),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f17]) ).
fof(f31,plain,
! [X0,X1,X2] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(equalish(X2,X2),true,ifeq2(true,true,f(n1,X2,X1,X0,sK1_exists_f_Z(n1,X2,X1,X0)),true),true),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f32,plain,
! [X0,X1,X2] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(equalish(X2,X2),true,ifeq2(true,true,f(n0,X2,X1,X0,sK1_exists_f_Z(n0,X2,X1,X0)),true),true),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f17]) ).
fof(f33,plain,
! [X0,X1,X2] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f25]) ).
fof(f34,plain,
! [X0,X1,X2] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f26]) ).
fof(f35,plain,
! [X0,X1,X2] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f27]) ).
fof(f36,plain,
! [X0,X1,X2] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f28]) ).
fof(f37,plain,
! [X0,X1,X2] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f29]) ).
fof(f38,plain,
! [X0,X1,X2] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f30]) ).
fof(f39,plain,
! [X0,X1,X2] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f31]) ).
fof(f40,plain,
! [X0,X1,X2] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f32]) ).
fof(f41,plain,
! [X0,X1,X2,X3,X4,X5,X6] : ifeq2(f(X0,X1,X2,n1,X3),true,ifeq2(f(X4,X5,X6,n1,X3),true,true,true),true) = true,
inference(paramodulation,[status(thm)],[f16,f18]) ).
fof(f42,plain,
! [X0,X1,X2,X3,X4,X5,X6] : ifeq2(f(X0,X1,X2,n0,X3),true,ifeq2(f(X4,X5,X6,n0,X3),true,true,true),true) = true,
inference(paramodulation,[status(thm)],[f15,f18]) ).
fof(f44,plain,
! [X0,X1,X2,X3,X4,X5,X6] : ifeq2(f(X0,X1,n1,X2,X3),true,ifeq2(f(X4,X5,n1,X6,X3),true,true,true),true) = true,
inference(paramodulation,[status(thm)],[f16,f19]) ).
fof(f45,plain,
! [X0,X1,X2,X3,X4,X5,X6] : ifeq2(f(X0,X1,n0,X2,X3),true,ifeq2(f(X4,X5,n0,X6,X3),true,true,true),true) = true,
inference(paramodulation,[status(thm)],[f15,f19]) ).
fof(f49,plain,
! [X0,X1,X2,X3,X4,X5,X6] : ifeq2(f(X0,n1,X1,X2,X3),true,ifeq2(f(X4,n1,X5,X6,X3),true,true,true),true) = true,
inference(paramodulation,[status(thm)],[f16,f20]) ).
fof(f50,plain,
! [X0,X1,X2,X3,X4,X5,X6] : ifeq2(f(X0,n0,X1,X2,X3),true,ifeq2(f(X4,n0,X5,X6,X3),true,true,true),true) = true,
inference(paramodulation,[status(thm)],[f15,f20]) ).
fof(f56,plain,
! [X0,X1,X2,X3,X4,X5,X6] : ifeq2(f(n1,X0,X1,X2,X3),true,ifeq2(f(n1,X4,X5,X6,X3),true,true,true),true) = true,
inference(paramodulation,[status(thm)],[f16,f21]) ).
fof(f57,plain,
! [X0,X1,X2,X3,X4,X5,X6] : ifeq2(f(n0,X0,X1,X2,X3),true,ifeq2(f(n0,X4,X5,X6,X3),true,true,true),true) = true,
inference(paramodulation,[status(thm)],[f15,f21]) ).
fof(f65,plain,
! [X0,X1] : ifeq2(true,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),true) = true,
inference(paramodulation,[status(thm)],[f16,f33]) ).
fof(f66,plain,
! [X0,X1] : ifeq2(true,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),true) = true,
inference(paramodulation,[status(thm)],[f15,f33]) ).
fof(f67,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,ifeq2(equalish(X1,X1),true,f(X1,n1,X0,n1,sK1_exists_f_Z(X1,n1,X0,n1)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f33]) ).
fof(f68,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,ifeq2(equalish(X1,X1),true,f(X1,n0,X0,n1,sK1_exists_f_Z(X1,n0,X0,n1)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f33]) ).
fof(f69,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,f(n1,X1,X0,n1,sK1_exists_f_Z(n1,X1,X0,n1)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f33]) ).
fof(f70,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,f(n0,X1,X0,n1,sK1_exists_f_Z(n0,X1,X0,n1)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f33]) ).
fof(f72,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f65]) ).
fof(f73,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f66]) ).
fof(f74,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f67]) ).
fof(f75,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f68]) ).
fof(f76,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f69]) ).
fof(f77,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f70]) ).
fof(f83,plain,
! [X0,X1] : ifeq2(true,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),true) = true,
inference(paramodulation,[status(thm)],[f16,f34]) ).
fof(f84,plain,
! [X0,X1] : ifeq2(true,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),true) = true,
inference(paramodulation,[status(thm)],[f15,f34]) ).
fof(f85,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,ifeq2(equalish(X1,X1),true,f(X1,n1,X0,n0,sK1_exists_f_Z(X1,n1,X0,n0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f34]) ).
fof(f86,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,ifeq2(equalish(X1,X1),true,f(X1,n0,X0,n0,sK1_exists_f_Z(X1,n0,X0,n0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f34]) ).
fof(f87,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,f(n1,X1,X0,n0,sK1_exists_f_Z(n1,X1,X0,n0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f34]) ).
fof(f88,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,f(n0,X1,X0,n0,sK1_exists_f_Z(n0,X1,X0,n0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f34]) ).
fof(f90,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f83]) ).
fof(f91,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f84]) ).
fof(f92,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f85]) ).
fof(f93,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f86]) ).
fof(f94,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f87]) ).
fof(f95,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f88]) ).
fof(f108,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,ifeq2(equalish(X1,X1),true,f(X1,n1,n1,X0,sK1_exists_f_Z(X1,n1,n1,X0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f35]) ).
fof(f109,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,ifeq2(equalish(X1,X1),true,f(X1,n0,n1,X0,sK1_exists_f_Z(X1,n0,n1,X0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f35]) ).
fof(f110,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,f(n1,X1,n1,X0,sK1_exists_f_Z(n1,X1,n1,X0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f35]) ).
fof(f111,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,f(n0,X1,n1,X0,sK1_exists_f_Z(n0,X1,n1,X0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f35]) ).
fof(f116,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f108]) ).
fof(f117,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f109]) ).
fof(f118,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f110]) ).
fof(f119,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f111]) ).
fof(f132,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,ifeq2(equalish(X1,X1),true,f(X1,n1,n0,X0,sK1_exists_f_Z(X1,n1,n0,X0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f36]) ).
fof(f133,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,ifeq2(equalish(X1,X1),true,f(X1,n0,n0,X0,sK1_exists_f_Z(X1,n0,n0,X0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f36]) ).
fof(f134,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,f(n1,X1,n0,X0,sK1_exists_f_Z(n1,X1,n0,X0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f36]) ).
fof(f135,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,f(n0,X1,n0,X0,sK1_exists_f_Z(n0,X1,n0,X0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f36]) ).
fof(f140,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f132]) ).
fof(f141,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f133]) ).
fof(f142,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f134]) ).
fof(f143,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f135]) ).
fof(f163,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,f(n1,n1,X1,X0,sK1_exists_f_Z(n1,n1,X1,X0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f37]) ).
fof(f164,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,f(n0,n1,X1,X0,sK1_exists_f_Z(n0,n1,X1,X0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f37]) ).
fof(f172,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f163]) ).
fof(f173,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f164]) ).
fof(f193,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,f(n1,n0,X1,X0,sK1_exists_f_Z(n1,n0,X1,X0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f38]) ).
fof(f194,plain,
! [X0,X1] : ifeq2(equalish(X0,X0),true,ifeq2(equalish(X1,X1),true,ifeq2(true,true,f(n0,n0,X1,X0,sK1_exists_f_Z(n0,n0,X1,X0)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f38]) ).
fof(f202,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f193]) ).
fof(f203,plain,
! [X0,X1] : 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) = true,
inference(forward_demodulation,[status(thm)],[f13,f194]) ).
fof(f205,plain,
! [X0] : ifeq2(true,true,ifeq2(equalish(X0,X0),true,f(X0,n1,n1,n1,sK1_exists_f_Z(X0,n1,n1,n1)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f72]) ).
fof(f206,plain,
! [X0] : ifeq2(true,true,ifeq2(equalish(X0,X0),true,f(X0,n0,n1,n1,sK1_exists_f_Z(X0,n0,n1,n1)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f72]) ).
fof(f207,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n1,X0,n1,n1,sK1_exists_f_Z(n1,X0,n1,n1)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f72]) ).
fof(f208,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n0,X0,n1,n1,sK1_exists_f_Z(n0,X0,n1,n1)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f72]) ).
fof(f213,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(X0,n1,n1,n1,sK1_exists_f_Z(X0,n1,n1,n1)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f205]) ).
fof(f214,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(X0,n0,n1,n1,sK1_exists_f_Z(X0,n0,n1,n1)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f206]) ).
fof(f215,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n1,X0,n1,n1,sK1_exists_f_Z(n1,X0,n1,n1)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f207]) ).
fof(f216,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n0,X0,n1,n1,sK1_exists_f_Z(n0,X0,n1,n1)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f208]) ).
fof(f245,plain,
ifeq2(true,true,f(n1,n0,n1,n1,sK1_exists_f_Z(n1,n0,n1,n1)),true) = true,
inference(paramodulation,[status(thm)],[f16,f214]) ).
fof(f246,plain,
ifeq2(true,true,f(n0,n0,n1,n1,sK1_exists_f_Z(n0,n0,n1,n1)),true) = true,
inference(paramodulation,[status(thm)],[f15,f214]) ).
fof(f252,plain,
f(n1,n0,n1,n1,sK1_exists_f_Z(n1,n0,n1,n1)) = true,
inference(forward_demodulation,[status(thm)],[f13,f245]) ).
fof(f253,plain,
f(n0,n0,n1,n1,sK1_exists_f_Z(n0,n0,n1,n1)) = true,
inference(forward_demodulation,[status(thm)],[f13,f246]) ).
fof(f308,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,ifeq2(true,true,equalish(n1,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f252,f21]) ).
fof(f309,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X0,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f252,f21]) ).
fof(f310,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,ifeq2(true,true,equalish(n0,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f252,f20]) ).
fof(f311,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X1,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f252,f20]) ).
fof(f312,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,ifeq2(true,true,equalish(n1,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f252,f19]) ).
fof(f313,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X2,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f252,f19]) ).
fof(f314,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,ifeq2(true,true,equalish(n1,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f252,f18]) ).
fof(f315,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X3,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f252,f18]) ).
fof(f355,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(n1,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f308]) ).
fof(f356,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X0,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f309]) ).
fof(f357,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(n0,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f310]) ).
fof(f358,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X1,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f311]) ).
fof(f359,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(n1,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f312]) ).
fof(f360,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X2,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f313]) ).
fof(f361,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(n1,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f314]) ).
fof(f362,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,equalish(X3,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f315]) ).
fof(f363,plain,
! [X0] : ifeq2(true,true,ifeq2(equalish(X0,X0),true,f(X0,n1,n0,n1,sK1_exists_f_Z(X0,n1,n0,n1)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f73]) ).
fof(f364,plain,
! [X0] : ifeq2(true,true,ifeq2(equalish(X0,X0),true,f(X0,n0,n0,n1,sK1_exists_f_Z(X0,n0,n0,n1)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f73]) ).
fof(f365,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n1,X0,n0,n1,sK1_exists_f_Z(n1,X0,n0,n1)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f73]) ).
fof(f366,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n0,X0,n0,n1,sK1_exists_f_Z(n0,X0,n0,n1)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f73]) ).
fof(f372,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(X0,n1,n0,n1,sK1_exists_f_Z(X0,n1,n0,n1)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f363]) ).
fof(f373,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(X0,n0,n0,n1,sK1_exists_f_Z(X0,n0,n0,n1)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f364]) ).
fof(f374,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n1,X0,n0,n1,sK1_exists_f_Z(n1,X0,n0,n1)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f365]) ).
fof(f375,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n0,X0,n0,n1,sK1_exists_f_Z(n0,X0,n0,n1)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f366]) ).
fof(f398,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,ifeq2(true,true,equalish(n0,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f253,f21]) ).
fof(f399,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X0,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f253,f21]) ).
fof(f400,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,ifeq2(true,true,equalish(n0,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f253,f20]) ).
fof(f401,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X1,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f253,f20]) ).
fof(f402,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,ifeq2(true,true,equalish(n1,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f253,f19]) ).
fof(f403,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X2,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f253,f19]) ).
fof(f404,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,ifeq2(true,true,equalish(n1,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f253,f18]) ).
fof(f405,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X3,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f253,f18]) ).
fof(f445,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(n0,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f398]) ).
fof(f446,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X0,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f399]) ).
fof(f447,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(n0,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f400]) ).
fof(f448,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X1,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f401]) ).
fof(f449,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(n1,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f402]) ).
fof(f450,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X2,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f403]) ).
fof(f451,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(n1,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f404]) ).
fof(f452,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,equalish(X3,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f405]) ).
fof(f456,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n1,n1,X0,n1,sK1_exists_f_Z(n1,n1,X0,n1)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f74]) ).
fof(f457,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n0,n1,X0,n1,sK1_exists_f_Z(n0,n1,X0,n1)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f74]) ).
fof(f466,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n1,n1,X0,n1,sK1_exists_f_Z(n1,n1,X0,n1)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f456]) ).
fof(f467,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n0,n1,X0,n1,sK1_exists_f_Z(n0,n1,X0,n1)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f457]) ).
fof(f487,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n1,n0,X0,n1,sK1_exists_f_Z(n1,n0,X0,n1)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f75]) ).
fof(f488,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n0,n0,X0,n1,sK1_exists_f_Z(n0,n0,X0,n1)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f75]) ).
fof(f500,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n1,n0,X0,n1,sK1_exists_f_Z(n1,n0,X0,n1)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f487]) ).
fof(f501,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n0,n0,X0,n1,sK1_exists_f_Z(n0,n0,X0,n1)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f488]) ).
fof(f583,plain,
! [X0] : ifeq2(true,true,ifeq2(equalish(X0,X0),true,f(X0,n1,n1,n0,sK1_exists_f_Z(X0,n1,n1,n0)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f90]) ).
fof(f584,plain,
! [X0] : ifeq2(true,true,ifeq2(equalish(X0,X0),true,f(X0,n0,n1,n0,sK1_exists_f_Z(X0,n0,n1,n0)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f90]) ).
fof(f585,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n1,X0,n1,n0,sK1_exists_f_Z(n1,X0,n1,n0)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f90]) ).
fof(f586,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n0,X0,n1,n0,sK1_exists_f_Z(n0,X0,n1,n0)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f90]) ).
fof(f592,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(X0,n1,n1,n0,sK1_exists_f_Z(X0,n1,n1,n0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f583]) ).
fof(f593,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(X0,n0,n1,n0,sK1_exists_f_Z(X0,n0,n1,n0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f584]) ).
fof(f594,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n1,X0,n1,n0,sK1_exists_f_Z(n1,X0,n1,n0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f585]) ).
fof(f595,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n0,X0,n1,n0,sK1_exists_f_Z(n0,X0,n1,n0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f586]) ).
fof(f611,plain,
! [X0] : ifeq2(true,true,ifeq2(equalish(X0,X0),true,f(X0,n1,n0,n0,sK1_exists_f_Z(X0,n1,n0,n0)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f91]) ).
fof(f612,plain,
! [X0] : ifeq2(true,true,ifeq2(equalish(X0,X0),true,f(X0,n0,n0,n0,sK1_exists_f_Z(X0,n0,n0,n0)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f91]) ).
fof(f613,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n1,X0,n0,n0,sK1_exists_f_Z(n1,X0,n0,n0)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f91]) ).
fof(f614,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n0,X0,n0,n0,sK1_exists_f_Z(n0,X0,n0,n0)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f91]) ).
fof(f620,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(X0,n1,n0,n0,sK1_exists_f_Z(X0,n1,n0,n0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f611]) ).
fof(f621,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(X0,n0,n0,n0,sK1_exists_f_Z(X0,n0,n0,n0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f612]) ).
fof(f622,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n1,X0,n0,n0,sK1_exists_f_Z(n1,X0,n0,n0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f613]) ).
fof(f623,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n0,X0,n0,n0,sK1_exists_f_Z(n0,X0,n0,n0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f614]) ).
fof(f634,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n1,n1,X0,n0,sK1_exists_f_Z(n1,n1,X0,n0)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f92]) ).
fof(f635,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n0,n1,X0,n0,sK1_exists_f_Z(n0,n1,X0,n0)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f92]) ).
fof(f644,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n1,n1,X0,n0,sK1_exists_f_Z(n1,n1,X0,n0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f634]) ).
fof(f645,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n0,n1,X0,n0,sK1_exists_f_Z(n0,n1,X0,n0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f635]) ).
fof(f666,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n1,n0,X0,n0,sK1_exists_f_Z(n1,n0,X0,n0)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f93]) ).
fof(f667,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n0,n0,X0,n0,sK1_exists_f_Z(n0,n0,X0,n0)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f93]) ).
fof(f676,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n1,n0,X0,n0,sK1_exists_f_Z(n1,n0,X0,n0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f666]) ).
fof(f677,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n0,n0,X0,n0,sK1_exists_f_Z(n0,n0,X0,n0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f667]) ).
fof(f776,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n1,n1,n1,X0,sK1_exists_f_Z(n1,n1,n1,X0)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f116]) ).
fof(f777,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n0,n1,n1,X0,sK1_exists_f_Z(n0,n1,n1,X0)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f116]) ).
fof(f788,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n1,n1,n1,X0,sK1_exists_f_Z(n1,n1,n1,X0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f776]) ).
fof(f789,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n0,n1,n1,X0,sK1_exists_f_Z(n0,n1,n1,X0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f777]) ).
fof(f803,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n1,n0,n1,X0,sK1_exists_f_Z(n1,n0,n1,X0)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f117]) ).
fof(f804,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n0,n0,n1,X0,sK1_exists_f_Z(n0,n0,n1,X0)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f117]) ).
fof(f818,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n1,n0,n1,X0,sK1_exists_f_Z(n1,n0,n1,X0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f803]) ).
fof(f819,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n0,n0,n1,X0,sK1_exists_f_Z(n0,n0,n1,X0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f804]) ).
fof(f963,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n1,n1,n0,X0,sK1_exists_f_Z(n1,n1,n0,X0)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f140]) ).
fof(f964,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n0,n1,n0,X0,sK1_exists_f_Z(n0,n1,n0,X0)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f140]) ).
fof(f975,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n1,n1,n0,X0,sK1_exists_f_Z(n1,n1,n0,X0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f963]) ).
fof(f976,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n0,n1,n0,X0,sK1_exists_f_Z(n0,n1,n0,X0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f964]) ).
fof(f1008,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n1,n0,n0,X0,sK1_exists_f_Z(n1,n0,n0,X0)),true),true) = true,
inference(paramodulation,[status(thm)],[f16,f141]) ).
fof(f1009,plain,
! [X0] : ifeq2(equalish(X0,X0),true,ifeq2(true,true,f(n0,n0,n0,X0,sK1_exists_f_Z(n0,n0,n0,X0)),true),true) = true,
inference(paramodulation,[status(thm)],[f15,f141]) ).
fof(f1020,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n1,n0,n0,X0,sK1_exists_f_Z(n1,n0,n0,X0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1008]) ).
fof(f1021,plain,
! [X0] : ifeq2(equalish(X0,X0),true,f(n0,n0,n0,X0,sK1_exists_f_Z(n0,n0,n0,X0)),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1009]) ).
fof(f1279,plain,
ifeq2(true,true,f(n1,n1,n1,n1,sK1_exists_f_Z(n1,n1,n1,n1)),true) = true,
inference(paramodulation,[status(thm)],[f16,f213]) ).
fof(f1280,plain,
ifeq2(true,true,f(n0,n1,n1,n1,sK1_exists_f_Z(n0,n1,n1,n1)),true) = true,
inference(paramodulation,[status(thm)],[f15,f213]) ).
fof(f1292,plain,
f(n1,n1,n1,n1,sK1_exists_f_Z(n1,n1,n1,n1)) = true,
inference(forward_demodulation,[status(thm)],[f13,f1279]) ).
fof(f1293,plain,
f(n0,n1,n1,n1,sK1_exists_f_Z(n0,n1,n1,n1)) = true,
inference(forward_demodulation,[status(thm)],[f13,f1280]) ).
fof(f1337,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,ifeq2(true,true,equalish(n1,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f1292,f21]) ).
fof(f1338,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X0,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1292,f21]) ).
fof(f1339,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,ifeq2(true,true,equalish(n1,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f1292,f20]) ).
fof(f1340,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X1,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1292,f20]) ).
fof(f1341,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,ifeq2(true,true,equalish(n1,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f1292,f19]) ).
fof(f1342,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X2,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1292,f19]) ).
fof(f1343,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,ifeq2(true,true,equalish(n1,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f1292,f18]) ).
fof(f1344,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X3,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1292,f18]) ).
fof(f1399,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(n1,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1337]) ).
fof(f1400,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X0,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1338]) ).
fof(f1401,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(n1,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1339]) ).
fof(f1402,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X1,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1340]) ).
fof(f1403,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(n1,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1341]) ).
fof(f1404,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X2,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1342]) ).
fof(f1405,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(n1,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1343]) ).
fof(f1406,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,equalish(X3,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1344]) ).
fof(f1471,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,ifeq2(true,true,equalish(n0,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f1293,f21]) ).
fof(f1472,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X0,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f1293,f21]) ).
fof(f1473,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,ifeq2(true,true,equalish(n1,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f1293,f20]) ).
fof(f1474,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X1,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1293,f20]) ).
fof(f1475,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,ifeq2(true,true,equalish(n1,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f1293,f19]) ).
fof(f1476,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X2,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1293,f19]) ).
fof(f1477,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,ifeq2(true,true,equalish(n1,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f1293,f18]) ).
fof(f1478,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X3,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1293,f18]) ).
fof(f1533,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(n0,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1471]) ).
fof(f1534,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X0,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1472]) ).
fof(f1535,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(n1,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1473]) ).
fof(f1536,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X1,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1474]) ).
fof(f1537,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(n1,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1475]) ).
fof(f1538,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X2,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1476]) ).
fof(f1539,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(n1,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1477]) ).
fof(f1540,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,equalish(X3,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1478]) ).
fof(f1585,plain,
ifeq2(true,true,f(n1,n1,n0,n1,sK1_exists_f_Z(n1,n1,n0,n1)),true) = true,
inference(paramodulation,[status(thm)],[f16,f372]) ).
fof(f1586,plain,
ifeq2(true,true,f(n0,n1,n0,n1,sK1_exists_f_Z(n0,n1,n0,n1)),true) = true,
inference(paramodulation,[status(thm)],[f15,f372]) ).
fof(f1598,plain,
f(n1,n1,n0,n1,sK1_exists_f_Z(n1,n1,n0,n1)) = true,
inference(forward_demodulation,[status(thm)],[f13,f1585]) ).
fof(f1599,plain,
f(n0,n1,n0,n1,sK1_exists_f_Z(n0,n1,n0,n1)) = true,
inference(forward_demodulation,[status(thm)],[f13,f1586]) ).
fof(f1643,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,ifeq2(true,true,equalish(n1,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f1598,f21]) ).
fof(f1644,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X0,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1598,f21]) ).
fof(f1645,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,ifeq2(true,true,equalish(n1,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f1598,f20]) ).
fof(f1646,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X1,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1598,f20]) ).
fof(f1647,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,ifeq2(true,true,equalish(n0,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f1598,f19]) ).
fof(f1648,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X2,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f1598,f19]) ).
fof(f1649,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,ifeq2(true,true,equalish(n1,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f1598,f18]) ).
fof(f1650,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X3,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1598,f18]) ).
fof(f1705,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(n1,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1643]) ).
fof(f1706,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X0,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1644]) ).
fof(f1707,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(n1,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1645]) ).
fof(f1708,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X1,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1646]) ).
fof(f1709,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(n0,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1647]) ).
fof(f1710,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X2,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1648]) ).
fof(f1711,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(n1,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1649]) ).
fof(f1712,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,equalish(X3,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1650]) ).
fof(f1713,plain,
ifeq2(true,true,f(n1,n0,n0,n1,sK1_exists_f_Z(n1,n0,n0,n1)),true) = true,
inference(paramodulation,[status(thm)],[f16,f373]) ).
fof(f1714,plain,
ifeq2(true,true,f(n0,n0,n0,n1,sK1_exists_f_Z(n0,n0,n0,n1)),true) = true,
inference(paramodulation,[status(thm)],[f15,f373]) ).
fof(f1726,plain,
f(n1,n0,n0,n1,sK1_exists_f_Z(n1,n0,n0,n1)) = true,
inference(forward_demodulation,[status(thm)],[f13,f1713]) ).
fof(f1727,plain,
f(n0,n0,n0,n1,sK1_exists_f_Z(n0,n0,n0,n1)) = true,
inference(forward_demodulation,[status(thm)],[f13,f1714]) ).
fof(f1771,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,ifeq2(true,true,equalish(n0,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f1599,f21]) ).
fof(f1772,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X0,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f1599,f21]) ).
fof(f1773,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,ifeq2(true,true,equalish(n1,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f1599,f20]) ).
fof(f1774,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X1,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1599,f20]) ).
fof(f1775,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,ifeq2(true,true,equalish(n0,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f1599,f19]) ).
fof(f1776,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X2,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f1599,f19]) ).
fof(f1777,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,ifeq2(true,true,equalish(n1,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f1599,f18]) ).
fof(f1778,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X3,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1599,f18]) ).
fof(f1833,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(n0,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1771]) ).
fof(f1834,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X0,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1772]) ).
fof(f1835,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(n1,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1773]) ).
fof(f1836,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X1,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1774]) ).
fof(f1837,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(n0,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1775]) ).
fof(f1838,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X2,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1776]) ).
fof(f1839,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(n1,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1777]) ).
fof(f1840,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,equalish(X3,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1778]) ).
fof(f1903,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,ifeq2(true,true,equalish(n0,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f1727,f21]) ).
fof(f1904,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X0,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f1727,f21]) ).
fof(f1905,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,ifeq2(true,true,equalish(n0,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f1727,f20]) ).
fof(f1906,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X1,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f1727,f20]) ).
fof(f1907,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,ifeq2(true,true,equalish(n0,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f1727,f19]) ).
fof(f1908,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X2,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f1727,f19]) ).
fof(f1909,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,ifeq2(true,true,equalish(n1,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f1727,f18]) ).
fof(f1910,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X3,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1727,f18]) ).
fof(f1965,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(n0,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1903]) ).
fof(f1966,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X0,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1904]) ).
fof(f1967,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(n0,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1905]) ).
fof(f1968,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X1,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1906]) ).
fof(f1969,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(n0,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1907]) ).
fof(f1970,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X2,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1908]) ).
fof(f1971,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(n1,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1909]) ).
fof(f1972,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,equalish(X3,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f1910]) ).
fof(f2038,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,ifeq2(true,true,equalish(n1,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f1726,f21]) ).
fof(f2039,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X0,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1726,f21]) ).
fof(f2040,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,ifeq2(true,true,equalish(n0,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f1726,f20]) ).
fof(f2041,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X1,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f1726,f20]) ).
fof(f2042,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,ifeq2(true,true,equalish(n0,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f1726,f19]) ).
fof(f2043,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X2,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f1726,f19]) ).
fof(f2044,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,ifeq2(true,true,equalish(n1,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f1726,f18]) ).
fof(f2045,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X3,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f1726,f18]) ).
fof(f2101,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(n1,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2038]) ).
fof(f2102,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X0,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2039]) ).
fof(f2103,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(n0,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2040]) ).
fof(f2104,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X1,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2041]) ).
fof(f2105,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(n0,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2042]) ).
fof(f2106,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X2,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2043]) ).
fof(f2107,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(n1,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2044]) ).
fof(f2108,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,equalish(X3,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2045]) ).
fof(f2301,plain,
ifeq2(true,true,f(n1,n1,n1,n0,sK1_exists_f_Z(n1,n1,n1,n0)),true) = true,
inference(paramodulation,[status(thm)],[f16,f592]) ).
fof(f2302,plain,
ifeq2(true,true,f(n0,n1,n1,n0,sK1_exists_f_Z(n0,n1,n1,n0)),true) = true,
inference(paramodulation,[status(thm)],[f15,f592]) ).
fof(f2314,plain,
f(n1,n1,n1,n0,sK1_exists_f_Z(n1,n1,n1,n0)) = true,
inference(forward_demodulation,[status(thm)],[f13,f2301]) ).
fof(f2315,plain,
f(n0,n1,n1,n0,sK1_exists_f_Z(n0,n1,n1,n0)) = true,
inference(forward_demodulation,[status(thm)],[f13,f2302]) ).
fof(f2359,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,ifeq2(true,true,equalish(n1,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f2314,f21]) ).
fof(f2360,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X0,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f2314,f21]) ).
fof(f2361,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,ifeq2(true,true,equalish(n1,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f2314,f20]) ).
fof(f2362,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X1,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f2314,f20]) ).
fof(f2363,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,ifeq2(true,true,equalish(n1,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f2314,f19]) ).
fof(f2364,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X2,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f2314,f19]) ).
fof(f2365,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,ifeq2(true,true,equalish(n0,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f2314,f18]) ).
fof(f2366,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X3,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2314,f18]) ).
fof(f2421,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(n1,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2359]) ).
fof(f2422,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X0,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2360]) ).
fof(f2423,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(n1,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2361]) ).
fof(f2424,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X1,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2362]) ).
fof(f2425,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(n1,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2363]) ).
fof(f2426,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X2,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2364]) ).
fof(f2427,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(n0,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2365]) ).
fof(f2428,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,equalish(X3,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2366]) ).
fof(f2429,plain,
ifeq2(true,true,f(n1,n0,n1,n0,sK1_exists_f_Z(n1,n0,n1,n0)),true) = true,
inference(paramodulation,[status(thm)],[f16,f593]) ).
fof(f2430,plain,
ifeq2(true,true,f(n0,n0,n1,n0,sK1_exists_f_Z(n0,n0,n1,n0)),true) = true,
inference(paramodulation,[status(thm)],[f15,f593]) ).
fof(f2442,plain,
f(n1,n0,n1,n0,sK1_exists_f_Z(n1,n0,n1,n0)) = true,
inference(forward_demodulation,[status(thm)],[f13,f2429]) ).
fof(f2443,plain,
f(n0,n0,n1,n0,sK1_exists_f_Z(n0,n0,n1,n0)) = true,
inference(forward_demodulation,[status(thm)],[f13,f2430]) ).
fof(f2487,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,ifeq2(true,true,equalish(n0,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f2315,f21]) ).
fof(f2488,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X0,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2315,f21]) ).
fof(f2489,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,ifeq2(true,true,equalish(n1,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f2315,f20]) ).
fof(f2490,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X1,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f2315,f20]) ).
fof(f2491,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,ifeq2(true,true,equalish(n1,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f2315,f19]) ).
fof(f2492,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X2,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f2315,f19]) ).
fof(f2493,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,ifeq2(true,true,equalish(n0,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f2315,f18]) ).
fof(f2494,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X3,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2315,f18]) ).
fof(f2549,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(n0,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2487]) ).
fof(f2550,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X0,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2488]) ).
fof(f2551,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(n1,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2489]) ).
fof(f2552,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X1,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2490]) ).
fof(f2553,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(n1,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2491]) ).
fof(f2554,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X2,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2492]) ).
fof(f2555,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(n0,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2493]) ).
fof(f2556,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,equalish(X3,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2494]) ).
fof(f2619,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,ifeq2(true,true,equalish(n0,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f2443,f21]) ).
fof(f2620,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X0,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2443,f21]) ).
fof(f2621,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,ifeq2(true,true,equalish(n0,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f2443,f20]) ).
fof(f2622,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X1,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2443,f20]) ).
fof(f2623,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,ifeq2(true,true,equalish(n1,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f2443,f19]) ).
fof(f2624,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X2,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f2443,f19]) ).
fof(f2625,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,ifeq2(true,true,equalish(n0,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f2443,f18]) ).
fof(f2626,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X3,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2443,f18]) ).
fof(f2681,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(n0,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2619]) ).
fof(f2682,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X0,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2620]) ).
fof(f2683,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(n0,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2621]) ).
fof(f2684,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X1,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2622]) ).
fof(f2685,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(n1,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2623]) ).
fof(f2686,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X2,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2624]) ).
fof(f2687,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(n0,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2625]) ).
fof(f2688,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,equalish(X3,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2626]) ).
fof(f2754,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,ifeq2(true,true,equalish(n1,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f2442,f21]) ).
fof(f2755,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X0,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f2442,f21]) ).
fof(f2756,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,ifeq2(true,true,equalish(n0,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f2442,f20]) ).
fof(f2757,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X1,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2442,f20]) ).
fof(f2758,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,ifeq2(true,true,equalish(n1,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f2442,f19]) ).
fof(f2759,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X2,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f2442,f19]) ).
fof(f2760,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,ifeq2(true,true,equalish(n0,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f2442,f18]) ).
fof(f2761,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X3,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2442,f18]) ).
fof(f2817,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(n1,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2754]) ).
fof(f2818,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X0,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2755]) ).
fof(f2819,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(n0,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2756]) ).
fof(f2820,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X1,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2757]) ).
fof(f2821,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(n1,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2758]) ).
fof(f2822,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X2,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2759]) ).
fof(f2823,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(n0,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2760]) ).
fof(f2824,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,equalish(X3,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2761]) ).
fof(f2825,plain,
ifeq2(true,true,f(n1,n1,n0,n0,sK1_exists_f_Z(n1,n1,n0,n0)),true) = true,
inference(paramodulation,[status(thm)],[f16,f620]) ).
fof(f2826,plain,
ifeq2(true,true,f(n0,n1,n0,n0,sK1_exists_f_Z(n0,n1,n0,n0)),true) = true,
inference(paramodulation,[status(thm)],[f15,f620]) ).
fof(f2838,plain,
f(n1,n1,n0,n0,sK1_exists_f_Z(n1,n1,n0,n0)) = true,
inference(forward_demodulation,[status(thm)],[f13,f2825]) ).
fof(f2839,plain,
f(n0,n1,n0,n0,sK1_exists_f_Z(n0,n1,n0,n0)) = true,
inference(forward_demodulation,[status(thm)],[f13,f2826]) ).
fof(f2883,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,ifeq2(true,true,equalish(n1,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f2838,f21]) ).
fof(f2884,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X0,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f2838,f21]) ).
fof(f2885,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,ifeq2(true,true,equalish(n1,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f2838,f20]) ).
fof(f2886,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X1,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f2838,f20]) ).
fof(f2887,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,ifeq2(true,true,equalish(n0,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f2838,f19]) ).
fof(f2888,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X2,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2838,f19]) ).
fof(f2889,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,ifeq2(true,true,equalish(n0,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f2838,f18]) ).
fof(f2890,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X3,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2838,f18]) ).
fof(f2945,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(n1,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2883]) ).
fof(f2946,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X0,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2884]) ).
fof(f2947,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(n1,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2885]) ).
fof(f2948,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X1,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2886]) ).
fof(f2949,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(n0,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2887]) ).
fof(f2950,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X2,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2888]) ).
fof(f2951,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(n0,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2889]) ).
fof(f2952,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,equalish(X3,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f2890]) ).
fof(f2953,plain,
ifeq2(true,true,f(n1,n0,n0,n0,sK1_exists_f_Z(n1,n0,n0,n0)),true) = true,
inference(paramodulation,[status(thm)],[f16,f621]) ).
fof(f2954,plain,
ifeq2(true,true,f(n0,n0,n0,n0,sK1_exists_f_Z(n0,n0,n0,n0)),true) = true,
inference(paramodulation,[status(thm)],[f15,f621]) ).
fof(f2966,plain,
f(n1,n0,n0,n0,sK1_exists_f_Z(n1,n0,n0,n0)) = true,
inference(forward_demodulation,[status(thm)],[f13,f2953]) ).
fof(f2967,plain,
f(n0,n0,n0,n0,sK1_exists_f_Z(n0,n0,n0,n0)) = true,
inference(forward_demodulation,[status(thm)],[f13,f2954]) ).
fof(f3011,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,ifeq2(true,true,equalish(n0,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f2839,f21]) ).
fof(f3012,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X0,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2839,f21]) ).
fof(f3013,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,ifeq2(true,true,equalish(n1,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f2839,f20]) ).
fof(f3014,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X1,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f2839,f20]) ).
fof(f3015,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,ifeq2(true,true,equalish(n0,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f2839,f19]) ).
fof(f3016,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X2,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2839,f19]) ).
fof(f3017,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,ifeq2(true,true,equalish(n0,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f2839,f18]) ).
fof(f3018,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X3,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2839,f18]) ).
fof(f3073,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(n0,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3011]) ).
fof(f3074,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X0,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3012]) ).
fof(f3075,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(n1,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3013]) ).
fof(f3076,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X1,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3014]) ).
fof(f3077,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(n0,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3015]) ).
fof(f3078,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X2,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3016]) ).
fof(f3079,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(n0,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3017]) ).
fof(f3080,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,equalish(X3,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3018]) ).
fof(f3143,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,ifeq2(true,true,equalish(n0,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f2967,f21]) ).
fof(f3144,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X0,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2967,f21]) ).
fof(f3145,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,ifeq2(true,true,equalish(n0,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f2967,f20]) ).
fof(f3146,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X1,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2967,f20]) ).
fof(f3147,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,ifeq2(true,true,equalish(n0,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f2967,f19]) ).
fof(f3148,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X2,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2967,f19]) ).
fof(f3149,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,ifeq2(true,true,equalish(n0,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f2967,f18]) ).
fof(f3150,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X3,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2967,f18]) ).
fof(f3205,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(n0,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3143]) ).
fof(f3206,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X0,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3144]) ).
fof(f3207,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(n0,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3145]) ).
fof(f3208,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X1,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3146]) ).
fof(f3209,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(n0,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3147]) ).
fof(f3210,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X2,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3148]) ).
fof(f3211,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(n0,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3149]) ).
fof(f3212,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,equalish(X3,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3150]) ).
fof(f3278,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,ifeq2(true,true,equalish(n1,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f2966,f21]) ).
fof(f3279,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X0,n1),true),true) = true,
inference(paramodulation,[status(thm)],[f2966,f21]) ).
fof(f3280,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,ifeq2(true,true,equalish(n0,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f2966,f20]) ).
fof(f3281,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X1,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2966,f20]) ).
fof(f3282,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,ifeq2(true,true,equalish(n0,X2),true),true) = true,
inference(paramodulation,[status(thm)],[f2966,f19]) ).
fof(f3283,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X2,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2966,f19]) ).
fof(f3284,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,ifeq2(true,true,equalish(n0,X3),true),true) = true,
inference(paramodulation,[status(thm)],[f2966,f18]) ).
fof(f3285,plain,
! [X0,X1,X2,X3] : ifeq2(true,true,ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X3,n0),true),true) = true,
inference(paramodulation,[status(thm)],[f2966,f18]) ).
fof(f3341,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(n1,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3278]) ).
fof(f3342,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X0,n1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3279]) ).
fof(f3343,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(n0,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3280]) ).
fof(f3344,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X1,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3281]) ).
fof(f3345,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(n0,X2),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3282]) ).
fof(f3346,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X2,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3283]) ).
fof(f3347,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(n0,X3),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3284]) ).
fof(f3348,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,equalish(X3,n0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f3285]) ).
fof(f4265,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n1)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f355,f20]) ).
fof(f4400,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n1)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f445,f20]) ).
fof(f4521,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n1)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f1399,f20]) ).
fof(f4683,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n1)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f1533,f20]) ).
fof(f4828,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n1)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f1705,f20]) ).
fof(f4975,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n1)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f1833,f20]) ).
fof(f5120,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n1)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f1965,f20]) ).
fof(f5265,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n1)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f2101,f20]) ).
fof(f5400,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n1,n0)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f2421,f20]) ).
fof(f5543,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n1,n0)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f2549,f20]) ).
fof(f5674,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n1,n0)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f2681,f20]) ).
fof(f5823,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n1,n0)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f2817,f20]) ).
fof(f5932,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n1,n0,n0)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f2945,f20]) ).
fof(f6041,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n1,n0,n0)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f3073,f20]) ).
fof(f6154,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n0,n0,n0,n0)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f3205,f20]) ).
fof(f6279,plain,
! [X0,X1,X2,X3] : ifeq2(f(X0,X1,X2,X3,sK1_exists_f_Z(n1,n0,n0,n0)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f3341,f20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MSC014-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n010.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 01:27:54 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 0.17/0.65 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 0.17/0.65 % SZS output start Saturation for theBenchmark
% See solution above
% 0.17/0.69 % Elapsed time: 0.226960 seconds
% 0.17/0.69 % CPU time: 1.484166 seconds
% 0.17/0.69 % Total memory used: 41.367 MB
% 0.17/0.69 % Net memory used: 40.564 MB
%------------------------------------------------------------------------------