%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG031+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 11:49:29 AM UTC 2026
% Result : Theorem 0.14s 5.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG031+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.37 % Computer : n014.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Mon Sep 21 12:53:55 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.40 % Drodi V4.1.1
% 0.14/5.51 % Refutation found
% 0.14/5.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.51 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.51 fof(f1,axiom,(
% 0.14/5.51 ( e10 != e11& e10 != e12& e10 != e13& e10 != e14& e10 != e15& e11 != e12& e11 != e13& e11 != e14& e11 != e15& e12 != e13& e12 != e14& e12 != e15& e13 != e14& e13 != e15& e14 != e15 ) ),
% 0.14/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.51 fof(f2,axiom,(
% 0.14/5.51 ( e20 != e21& e20 != e22& e20 != e23& e20 != e24& e20 != e25& e21 != e22& e21 != e23& e21 != e24& e21 != e25& e22 != e23& e22 != e24& e22 != e25& e23 != e24& e23 != e25& e24 != e25 ) ),
% 0.14/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.51 fof(f4,axiom,(
% 0.14/5.51 ( op1(e10,e10) = e10& op1(e10,e11) = e11& op1(e10,e12) = e12& op1(e10,e13) = e13& op1(e10,e14) = e14& op1(e10,e15) = e15& op1(e11,e10) = e11& op1(e11,e11) = e10& op1(e11,e12) = e14& op1(e11,e13) = e15& op1(e11,e14) = e12& op1(e11,e15) = e13& op1(e12,e10) = e12& op1(e12,e11) = e14& op1(e12,e12) = e13& op1(e12,e13) = e10& op1(e12,e14) = e15& op1(e12,e15) = e11& op1(e13,e10) = e13& op1(e13,e11) = e15& op1(e13,e12) = e10& op1(e13,e13) = e12& op1(e13,e14) = e11& op1(e13,e15) = e14& op1(e14,e10) = e14& op1(e14,e11) = e12& op1(e14,e12) = e15& op1(e14,e13) = e11& op1(e14,e14) = e13& op1(e14,e15) = e10& op1(e15,e10) = e15& op1(e15,e11) = e13& op1(e15,e12) = e11& op1(e15,e13) = e14& op1(e15,e14) = e10& op1(e15,e15) = e12 ) ),
% 0.14/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.51 fof(f5,axiom,(
% 0.14/5.51 ( op2(e20,e20) = e20& op2(e20,e21) = e21& op2(e20,e22) = e22& op2(e20,e23) = e23& op2(e20,e24) = e24& op2(e20,e25) = e25& op2(e21,e20) = e21& op2(e21,e21) = e20& op2(e21,e22) = e23& op2(e21,e23) = e22& op2(e21,e24) = e25& op2(e21,e25) = e24& op2(e22,e20) = e22& op2(e22,e21) = e24& op2(e22,e22) = e20& op2(e22,e23) = e25& op2(e22,e24) = e21& op2(e22,e25) = e23& op2(e23,e20) = e23& op2(e23,e21) = e25& op2(e23,e22) = e21& op2(e23,e23) = e24& op2(e23,e24) = e20& op2(e23,e25) = e22& op2(e24,e20) = e24& op2(e24,e21) = e22& op2(e24,e22) = e25& op2(e24,e23) = e20& op2(e24,e24) = e23& op2(e24,e25) = e21& op2(e25,e20) = e25& op2(e25,e21) = e23& op2(e25,e22) = e24& op2(e25,e23) = e21& op2(e25,e24) = e22& op2(e25,e25) = e20 ) ),
% 0.14/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.51 fof(f6,conjecture,(
% 0.14/5.51 ( ( ( h(e10) = e20| h(e10) = e21| h(e10) = e22| h(e10) = e23| h(e10) = e24| h(e10) = e25 )& ( h(e11) = e20| h(e11) = e21| h(e11) = e22| h(e11) = e23| h(e11) = e24| h(e11) = e25 )& ( h(e12) = e20| h(e12) = e21| h(e12) = e22| h(e12) = e23| h(e12) = e24| h(e12) = e25 )& ( h(e13) = e20| h(e13) = e21| h(e13) = e22| h(e13) = e23| h(e13) = e24| h(e13) = e25 )& ( h(e14) = e20| h(e14) = e21| h(e14) = e22| h(e14) = e23| h(e14) = e24| h(e14) = e25 )& ( h(e15) = e20| h(e15) = e21| h(e15) = e22| h(e15) = e23| h(e15) = e24| h(e15) = e25 )& ( j(e20) = e10| j(e20) = e11| j(e20) = e12| j(e20) = e13| j(e20) = e14| j(e20) = e15 )& ( j(e21) = e10| j(e21) = e11| j(e21) = e12| j(e21) = e13| j(e21) = e14| j(e21) = e15 )& ( j(e22) = e10| j(e22) = e11| j(e22) = e12| j(e22) = e13| j(e22) = e14| j(e22) = e15 )& ( j(e23) = e10| j(e23) = e11| j(e23) = e12| j(e23) = e13| j(e23) = e14| j(e23) = e15 )& ( j(e24) = e10| j(e24) = e11| j(e24) = e12| j(e24) = e13| j(e24) = e14| j(e24) = e15 )& ( j(e25) = e10| j(e25) = e11| j(e25) = e12| j(e25) = e13| j(e25) = e14| j(e25) = e15 ) )=> ~ ( h(op1(e10,e10)) = op2(h(e10),h(e10))& h(op1(e10,e11)) = op2(h(e10),h(e11))& h(op1(e10,e12)) = op2(h(e10),h(e12))& h(op1(e10,e13)) = op2(h(e10),h(e13))& h(op1(e10,e14)) = op2(h(e10),h(e14))& h(op1(e10,e15)) = op2(h(e10),h(e15))& h(op1(e11,e10)) = op2(h(e11),h(e10))& h(op1(e11,e11)) = op2(h(e11),h(e11))& h(op1(e11,e12)) = op2(h(e11),h(e12))& h(op1(e11,e13)) = op2(h(e11),h(e13))& h(op1(e11,e14)) = op2(h(e11),h(e14))& h(op1(e11,e15)) = op2(h(e11),h(e15))& h(op1(e12,e10)) = op2(h(e12),h(e10))& h(op1(e12,e11)) = op2(h(e12),h(e11))& h(op1(e12,e12)) = op2(h(e12),h(e12))& h(op1(e12,e13)) = op2(h(e12),h(e13))& h(op1(e12,e14)) = op2(h(e12),h(e14))& h(op1(e12,e15)) = op2(h(e12),h(e15))& h(op1(e13,e10)) = op2(h(e13),h(e10))& h(op1(e13,e11)) = op2(h(e13),h(e11))& h(op1(e13,e12)) = op2(h(e13),h(e12))& h(op1(e13,e13)) = op2(h(e13),h(e13))& h(op1(e13,e14)) = op2(h(e13),h(e14))& h(op1(e13,e15)) = op2(h(e13),h(e15))& h(op1(e14,e10)) = op2(h(e14),h(e10))& h(op1(e14,e11)) = op2(h(e14),h(e11))& h(op1(e14,e12)) = op2(h(e14),h(e12))& h(op1(e14,e13)) = op2(h(e14),h(e13))& h(op1(e14,e14)) = op2(h(e14),h(e14))& h(op1(e14,e15)) = op2(h(e14),h(e15))& h(op1(e15,e10)) = op2(h(e15),h(e10))& h(op1(e15,e11)) = op2(h(e15),h(e11))& h(op1(e15,e12)) = op2(h(e15),h(e12))& h(op1(e15,e13)) = op2(h(e15),h(e13))& h(op1(e15,e14)) = op2(h(e15),h(e14))& h(op1(e15,e15)) = op2(h(e15),h(e15))& j(op2(e20,e20)) = op1(j(e20),j(e20))& j(op2(e20,e21)) = op1(j(e20),j(e21))& j(op2(e20,e22)) = op1(j(e20),j(e22))& j(op2(e20,e23)) = op1(j(e20),j(e23))& j(op2(e20,e24)) = op1(j(e20),j(e24))& j(op2(e20,e25)) = op1(j(e20),j(e25))& j(op2(e21,e20)) = op1(j(e21),j(e20))& j(op2(e21,e21)) = op1(j(e21),j(e21))& j(op2(e21,e22)) = op1(j(e21),j(e22))& j(op2(e21,e23)) = op1(j(e21),j(e23))& j(op2(e21,e24)) = op1(j(e21),j(e24))& j(op2(e21,e25)) = op1(j(e21),j(e25))& j(op2(e22,e20)) = op1(j(e22),j(e20))& j(op2(e22,e21)) = op1(j(e22),j(e21))& j(op2(e22,e22)) = op1(j(e22),j(e22))& j(op2(e22,e23)) = op1(j(e22),j(e23))& j(op2(e22,e24)) = op1(j(e22),j(e24))& j(op2(e22,e25)) = op1(j(e22),j(e25))& j(op2(e23,e20)) = op1(j(e23),j(e20))& j(op2(e23,e21)) = op1(j(e23),j(e21))& j(op2(e23,e22)) = op1(j(e23),j(e22))& j(op2(e23,e23)) = op1(j(e23),j(e23))& j(op2(e23,e24)) = op1(j(e23),j(e24))& j(op2(e23,e25)) = op1(j(e23),j(e25))& j(op2(e24,e20)) = op1(j(e24),j(e20))& j(op2(e24,e21)) = op1(j(e24),j(e21))& j(op2(e24,e22)) = op1(j(e24),j(e22))& j(op2(e24,e23)) = op1(j(e24),j(e23))& j(op2(e24,e24)) = op1(j(e24),j(e24))& j(op2(e24,e25)) = op1(j(e24),j(e25))& j(op2(e25,e20)) = op1(j(e25),j(e20))& j(op2(e25,e21)) = op1(j(e25),j(e21))& j(op2(e25,e22)) = op1(j(e25),j(e22))& j(op2(e25,e23)) = op1(j(e25),j(e23))& j(op2(e25,e24)) = op1(j(e25),j(e24))& j(op2(e25,e25)) = op1(j(e25),j(e25))& h(j(e20)) = e20& h(j(e21)) = e21& h(j(e22)) = e22& h(j(e23)) = e23& h(j(e24)) = e24& h(j(e25)) = e25& j(h(e10)) = e10& j(h(e11)) = e11& j(h(e12)) = e12& j(h(e13)) = e13& j(h(e14)) = e14& j(h(e15)) = e15 ) ) ),
% 0.14/5.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.51 fof(f7,negated_conjecture,(
% 0.14/5.51 ~(( ( ( h(e10) = e20| h(e10) = e21| h(e10) = e22| h(e10) = e23| h(e10) = e24| h(e10) = e25 )& ( h(e11) = e20| h(e11) = e21| h(e11) = e22| h(e11) = e23| h(e11) = e24| h(e11) = e25 )& ( h(e12) = e20| h(e12) = e21| h(e12) = e22| h(e12) = e23| h(e12) = e24| h(e12) = e25 )& ( h(e13) = e20| h(e13) = e21| h(e13) = e22| h(e13) = e23| h(e13) = e24| h(e13) = e25 )& ( h(e14) = e20| h(e14) = e21| h(e14) = e22| h(e14) = e23| h(e14) = e24| h(e14) = e25 )& ( h(e15) = e20| h(e15) = e21| h(e15) = e22| h(e15) = e23| h(e15) = e24| h(e15) = e25 )& ( j(e20) = e10| j(e20) = e11| j(e20) = e12| j(e20) = e13| j(e20) = e14| j(e20) = e15 )& ( j(e21) = e10| j(e21) = e11| j(e21) = e12| j(e21) = e13| j(e21) = e14| j(e21) = e15 )& ( j(e22) = e10| j(e22) = e11| j(e22) = e12| j(e22) = e13| j(e22) = e14| j(e22) = e15 )& ( j(e23) = e10| j(e23) = e11| j(e23) = e12| j(e23) = e13| j(e23) = e14| j(e23) = e15 )& ( j(e24) = e10| j(e24) = e11| j(e24) = e12| j(e24) = e13| j(e24) = e14| j(e24) = e15 )& ( j(e25) = e10| j(e25) = e11| j(e25) = e12| j(e25) = e13| j(e25) = e14| j(e25) = e15 ) )=> ~ ( h(op1(e10,e10)) = op2(h(e10),h(e10))& h(op1(e10,e11)) = op2(h(e10),h(e11))& h(op1(e10,e12)) = op2(h(e10),h(e12))& h(op1(e10,e13)) = op2(h(e10),h(e13))& h(op1(e10,e14)) = op2(h(e10),h(e14))& h(op1(e10,e15)) = op2(h(e10),h(e15))& h(op1(e11,e10)) = op2(h(e11),h(e10))& h(op1(e11,e11)) = op2(h(e11),h(e11))& h(op1(e11,e12)) = op2(h(e11),h(e12))& h(op1(e11,e13)) = op2(h(e11),h(e13))& h(op1(e11,e14)) = op2(h(e11),h(e14))& h(op1(e11,e15)) = op2(h(e11),h(e15))& h(op1(e12,e10)) = op2(h(e12),h(e10))& h(op1(e12,e11)) = op2(h(e12),h(e11))& h(op1(e12,e12)) = op2(h(e12),h(e12))& h(op1(e12,e13)) = op2(h(e12),h(e13))& h(op1(e12,e14)) = op2(h(e12),h(e14))& h(op1(e12,e15)) = op2(h(e12),h(e15))& h(op1(e13,e10)) = op2(h(e13),h(e10))& h(op1(e13,e11)) = op2(h(e13),h(e11))& h(op1(e13,e12)) = op2(h(e13),h(e12))& h(op1(e13,e13)) = op2(h(e13),h(e13))& h(op1(e13,e14)) = op2(h(e13),h(e14))& h(op1(e13,e15)) = op2(h(e13),h(e15))& h(op1(e14,e10)) = op2(h(e14),h(e10))& h(op1(e14,e11)) = op2(h(e14),h(e11))& h(op1(e14,e12)) = op2(h(e14),h(e12))& h(op1(e14,e13)) = op2(h(e14),h(e13))& h(op1(e14,e14)) = op2(h(e14),h(e14))& h(op1(e14,e15)) = op2(h(e14),h(e15))& h(op1(e15,e10)) = op2(h(e15),h(e10))& h(op1(e15,e11)) = op2(h(e15),h(e11))& h(op1(e15,e12)) = op2(h(e15),h(e12))& h(op1(e15,e13)) = op2(h(e15),h(e13))& h(op1(e15,e14)) = op2(h(e15),h(e14))& h(op1(e15,e15)) = op2(h(e15),h(e15))& j(op2(e20,e20)) = op1(j(e20),j(e20))& j(op2(e20,e21)) = op1(j(e20),j(e21))& j(op2(e20,e22)) = op1(j(e20),j(e22))& j(op2(e20,e23)) = op1(j(e20),j(e23))& j(op2(e20,e24)) = op1(j(e20),j(e24))& j(op2(e20,e25)) = op1(j(e20),j(e25))& j(op2(e21,e20)) = op1(j(e21),j(e20))& j(op2(e21,e21)) = op1(j(e21),j(e21))& j(op2(e21,e22)) = op1(j(e21),j(e22))& j(op2(e21,e23)) = op1(j(e21),j(e23))& j(op2(e21,e24)) = op1(j(e21),j(e24))& j(op2(e21,e25)) = op1(j(e21),j(e25))& j(op2(e22,e20)) = op1(j(e22),j(e20))& j(op2(e22,e21)) = op1(j(e22),j(e21))& j(op2(e22,e22)) = op1(j(e22),j(e22))& j(op2(e22,e23)) = op1(j(e22),j(e23))& j(op2(e22,e24)) = op1(j(e22),j(e24))& j(op2(e22,e25)) = op1(j(e22),j(e25))& j(op2(e23,e20)) = op1(j(e23),j(e20))& j(op2(e23,e21)) = op1(j(e23),j(e21))& j(op2(e23,e22)) = op1(j(e23),j(e22))& j(op2(e23,e23)) = op1(j(e23),j(e23))& j(op2(e23,e24)) = op1(j(e23),j(e24))& j(op2(e23,e25)) = op1(j(e23),j(e25))& j(op2(e24,e20)) = op1(j(e24),j(e20))& j(op2(e24,e21)) = op1(j(e24),j(e21))& j(op2(e24,e22)) = op1(j(e24),j(e22))& j(op2(e24,e23)) = op1(j(e24),j(e23))& j(op2(e24,e24)) = op1(j(e24),j(e24))& j(op2(e24,e25)) = op1(j(e24),j(e25))& j(op2(e25,e20)) = op1(j(e25),j(e20))& j(op2(e25,e21)) = op1(j(e25),j(e21))& j(op2(e25,e22)) = op1(j(e25),j(e22))& j(op2(e25,e23)) = op1(j(e25),j(e23))& j(op2(e25,e24)) = op1(j(e25),j(e24))& j(op2(e25,e25)) = op1(j(e25),j(e25))& h(j(e20)) = e20& h(j(e21)) = e21& h(j(e22)) = e22& h(j(e23)) = e23& h(j(e24)) = e24& h(j(e25)) = e25& j(h(e10)) = e10& j(h(e11)) = e11& j(h(e12)) = e12& j(h(e13)) = e13& j(h(e14)) = e14& j(h(e15)) = e15 ) ) )),
% 0.14/5.51 inference(negated_conjecture,[status(cth)],[f6])).
% 0.14/5.51 fof(f8,plain,(
% 0.14/5.51 ~e10=e11),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/5.51 fof(f9,plain,(
% 0.14/5.51 ~e10=e12),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/5.51 fof(f10,plain,(
% 0.14/5.51 ~e10=e13),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/5.51 fof(f11,plain,(
% 0.14/5.51 ~e10=e14),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/5.51 fof(f17,plain,(
% 0.14/5.51 ~e12=e13),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/5.51 fof(f21,plain,(
% 0.14/5.51 ~e13=e15),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/5.51 fof(f24,plain,(
% 0.14/5.51 ~e20=e22),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/5.51 fof(f26,plain,(
% 0.14/5.51 ~e20=e24),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/5.51 fof(f27,plain,(
% 0.14/5.51 ~e20=e25),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/5.51 fof(f35,plain,(
% 0.14/5.51 ~e23=e24),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/5.51 fof(f74,plain,(
% 0.14/5.51 op1(e10,e10)=e10),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/5.51 fof(f81,plain,(
% 0.14/5.51 op1(e11,e11)=e10),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/5.51 fof(f88,plain,(
% 0.14/5.51 op1(e12,e12)=e13),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/5.51 fof(f89,plain,(
% 0.14/5.51 op1(e12,e13)=e10),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/5.51 fof(f94,plain,(
% 0.14/5.51 op1(e13,e12)=e10),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/5.51 fof(f95,plain,(
% 0.14/5.51 op1(e13,e13)=e12),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/5.51 fof(f97,plain,(
% 0.14/5.51 op1(e13,e15)=e14),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/5.51 fof(f102,plain,(
% 0.14/5.51 op1(e14,e14)=e13),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/5.51 fof(f109,plain,(
% 0.14/5.51 op1(e15,e15)=e12),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/5.51 fof(f110,plain,(
% 0.14/5.51 op2(e20,e20)=e20),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.51 fof(f114,plain,(
% 0.14/5.51 op2(e20,e24)=e24),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.51 fof(f117,plain,(
% 0.14/5.51 op2(e21,e21)=e20),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.51 fof(f122,plain,(
% 0.14/5.51 op2(e22,e20)=e22),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.51 fof(f124,plain,(
% 0.14/5.51 op2(e22,e22)=e20),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.51 fof(f128,plain,(
% 0.14/5.51 op2(e23,e20)=e23),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.51 fof(f131,plain,(
% 0.14/5.51 op2(e23,e23)=e24),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.51 fof(f132,plain,(
% 0.14/5.51 op2(e23,e24)=e20),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.51 fof(f137,plain,(
% 0.14/5.51 op2(e24,e23)=e20),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.51 fof(f138,plain,(
% 0.14/5.51 op2(e24,e24)=e23),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.51 fof(f145,plain,(
% 0.14/5.51 op2(e25,e25)=e20),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.51 fof(f146,plain,(
% 0.14/5.51 (((((((((((((((((h(e10)=e20|h(e10)=e21)|h(e10)=e22)|h(e10)=e23)|h(e10)=e24)|h(e10)=e25)&(((((h(e11)=e20|h(e11)=e21)|h(e11)=e22)|h(e11)=e23)|h(e11)=e24)|h(e11)=e25))&(((((h(e12)=e20|h(e12)=e21)|h(e12)=e22)|h(e12)=e23)|h(e12)=e24)|h(e12)=e25))&(((((h(e13)=e20|h(e13)=e21)|h(e13)=e22)|h(e13)=e23)|h(e13)=e24)|h(e13)=e25))&(((((h(e14)=e20|h(e14)=e21)|h(e14)=e22)|h(e14)=e23)|h(e14)=e24)|h(e14)=e25))&(((((h(e15)=e20|h(e15)=e21)|h(e15)=e22)|h(e15)=e23)|h(e15)=e24)|h(e15)=e25))&(((((j(e20)=e10|j(e20)=e11)|j(e20)=e12)|j(e20)=e13)|j(e20)=e14)|j(e20)=e15))&(((((j(e21)=e10|j(e21)=e11)|j(e21)=e12)|j(e21)=e13)|j(e21)=e14)|j(e21)=e15))&(((((j(e22)=e10|j(e22)=e11)|j(e22)=e12)|j(e22)=e13)|j(e22)=e14)|j(e22)=e15))&(((((j(e23)=e10|j(e23)=e11)|j(e23)=e12)|j(e23)=e13)|j(e23)=e14)|j(e23)=e15))&(((((j(e24)=e10|j(e24)=e11)|j(e24)=e12)|j(e24)=e13)|j(e24)=e14)|j(e24)=e15))&(((((j(e25)=e10|j(e25)=e11)|j(e25)=e12)|j(e25)=e13)|j(e25)=e14)|j(e25)=e15))&(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((h(op1(e10,e10))=op2(h(e10),h(e10))&h(op1(e10,e11))=op2(h(e10),h(e11)))&h(op1(e10,e12))=op2(h(e10),h(e12)))&h(op1(e10,e13))=op2(h(e10),h(e13)))&h(op1(e10,e14))=op2(h(e10),h(e14)))&h(op1(e10,e15))=op2(h(e10),h(e15)))&h(op1(e11,e10))=op2(h(e11),h(e10)))&h(op1(e11,e11))=op2(h(e11),h(e11)))&h(op1(e11,e12))=op2(h(e11),h(e12)))&h(op1(e11,e13))=op2(h(e11),h(e13)))&h(op1(e11,e14))=op2(h(e11),h(e14)))&h(op1(e11,e15))=op2(h(e11),h(e15)))&h(op1(e12,e10))=op2(h(e12),h(e10)))&h(op1(e12,e11))=op2(h(e12),h(e11)))&h(op1(e12,e12))=op2(h(e12),h(e12)))&h(op1(e12,e13))=op2(h(e12),h(e13)))&h(op1(e12,e14))=op2(h(e12),h(e14)))&h(op1(e12,e15))=op2(h(e12),h(e15)))&h(op1(e13,e10))=op2(h(e13),h(e10)))&h(op1(e13,e11))=op2(h(e13),h(e11)))&h(op1(e13,e12))=op2(h(e13),h(e12)))&h(op1(e13,e13))=op2(h(e13),h(e13)))&h(op1(e13,e14))=op2(h(e13),h(e14)))&h(op1(e13,e15))=op2(h(e13),h(e15)))&h(op1(e14,e10))=op2(h(e14),h(e10)))&h(op1(e14,e11))=op2(h(e14),h(e11)))&h(op1(e14,e12))=op2(h(e14),h(e12)))&h(op1(e14,e13))=op2(h(e14),h(e13)))&h(op1(e14,e14))=op2(h(e14),h(e14)))&h(op1(e14,e15))=op2(h(e14),h(e15)))&h(op1(e15,e10))=op2(h(e15),h(e10)))&h(op1(e15,e11))=op2(h(e15),h(e11)))&h(op1(e15,e12))=op2(h(e15),h(e12)))&h(op1(e15,e13))=op2(h(e15),h(e13)))&h(op1(e15,e14))=op2(h(e15),h(e14)))&h(op1(e15,e15))=op2(h(e15),h(e15)))&j(op2(e20,e20))=op1(j(e20),j(e20)))&j(op2(e20,e21))=op1(j(e20),j(e21)))&j(op2(e20,e22))=op1(j(e20),j(e22)))&j(op2(e20,e23))=op1(j(e20),j(e23)))&j(op2(e20,e24))=op1(j(e20),j(e24)))&j(op2(e20,e25))=op1(j(e20),j(e25)))&j(op2(e21,e20))=op1(j(e21),j(e20)))&j(op2(e21,e21))=op1(j(e21),j(e21)))&j(op2(e21,e22))=op1(j(e21),j(e22)))&j(op2(e21,e23))=op1(j(e21),j(e23)))&j(op2(e21,e24))=op1(j(e21),j(e24)))&j(op2(e21,e25))=op1(j(e21),j(e25)))&j(op2(e22,e20))=op1(j(e22),j(e20)))&j(op2(e22,e21))=op1(j(e22),j(e21)))&j(op2(e22,e22))=op1(j(e22),j(e22)))&j(op2(e22,e23))=op1(j(e22),j(e23)))&j(op2(e22,e24))=op1(j(e22),j(e24)))&j(op2(e22,e25))=op1(j(e22),j(e25)))&j(op2(e23,e20))=op1(j(e23),j(e20)))&j(op2(e23,e21))=op1(j(e23),j(e21)))&j(op2(e23,e22))=op1(j(e23),j(e22)))&j(op2(e23,e23))=op1(j(e23),j(e23)))&j(op2(e23,e24))=op1(j(e23),j(e24)))&j(op2(e23,e25))=op1(j(e23),j(e25)))&j(op2(e24,e20))=op1(j(e24),j(e20)))&j(op2(e24,e21))=op1(j(e24),j(e21)))&j(op2(e24,e22))=op1(j(e24),j(e22)))&j(op2(e24,e23))=op1(j(e24),j(e23)))&j(op2(e24,e24))=op1(j(e24),j(e24)))&j(op2(e24,e25))=op1(j(e24),j(e25)))&j(op2(e25,e20))=op1(j(e25),j(e20)))&j(op2(e25,e21))=op1(j(e25),j(e21)))&j(op2(e25,e22))=op1(j(e25),j(e22)))&j(op2(e25,e23))=op1(j(e25),j(e23)))&j(op2(e25,e24))=op1(j(e25),j(e24)))&j(op2(e25,e25))=op1(j(e25),j(e25)))&h(j(e20))=e20)&h(j(e21))=e21)&h(j(e22))=e22)&h(j(e23))=e23)&h(j(e24))=e24)&h(j(e25))=e25)&j(h(e10))=e10)&j(h(e11))=e11)&j(h(e12))=e12)&j(h(e13))=e13)&j(h(e14))=e14)&j(h(e15))=e15))),
% 0.14/5.51 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.14/5.51 fof(f147,plain,(
% 0.14/5.51 h(e10)=e20|h(e10)=e21|h(e10)=e22|h(e10)=e23|h(e10)=e24|h(e10)=e25),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f149,plain,(
% 0.14/5.51 h(e12)=e20|h(e12)=e21|h(e12)=e22|h(e12)=e23|h(e12)=e24|h(e12)=e25),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f150,plain,(
% 0.14/5.51 h(e13)=e20|h(e13)=e21|h(e13)=e22|h(e13)=e23|h(e13)=e24|h(e13)=e25),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f152,plain,(
% 0.14/5.51 h(e15)=e20|h(e15)=e21|h(e15)=e22|h(e15)=e23|h(e15)=e24|h(e15)=e25),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f157,plain,(
% 0.14/5.51 j(e24)=e10|j(e24)=e11|j(e24)=e12|j(e24)=e13|j(e24)=e14|j(e24)=e15),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f159,plain,(
% 0.14/5.51 h(op1(e10,e10))=op2(h(e10),h(e10))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f173,plain,(
% 0.14/5.51 h(op1(e12,e12))=op2(h(e12),h(e12))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f180,plain,(
% 0.14/5.51 h(op1(e13,e13))=op2(h(e13),h(e13))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f182,plain,(
% 0.14/5.51 h(op1(e13,e15))=op2(h(e13),h(e15))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f187,plain,(
% 0.14/5.51 h(op1(e14,e14))=op2(h(e14),h(e14))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f194,plain,(
% 0.14/5.51 h(op1(e15,e15))=op2(h(e15),h(e15))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f195,plain,(
% 0.14/5.51 j(op2(e20,e20))=op1(j(e20),j(e20))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f199,plain,(
% 0.14/5.51 j(op2(e20,e24))=op1(j(e20),j(e24))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f202,plain,(
% 0.14/5.51 j(op2(e21,e21))=op1(j(e21),j(e21))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f207,plain,(
% 0.14/5.51 j(op2(e22,e20))=op1(j(e22),j(e20))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f209,plain,(
% 0.14/5.51 j(op2(e22,e22))=op1(j(e22),j(e22))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f213,plain,(
% 0.14/5.51 j(op2(e23,e20))=op1(j(e23),j(e20))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f216,plain,(
% 0.14/5.51 j(op2(e23,e23))=op1(j(e23),j(e23))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f222,plain,(
% 0.14/5.51 j(op2(e24,e23))=op1(j(e24),j(e23))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f223,plain,(
% 0.14/5.51 j(op2(e24,e24))=op1(j(e24),j(e24))),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f231,plain,(
% 0.14/5.51 h(j(e20))=e20),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f233,plain,(
% 0.14/5.51 h(j(e22))=e22),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f234,plain,(
% 0.14/5.51 h(j(e23))=e23),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f235,plain,(
% 0.14/5.51 h(j(e24))=e24),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f237,plain,(
% 0.14/5.51 j(h(e10))=e10),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f239,plain,(
% 0.14/5.51 j(h(e12))=e12),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f240,plain,(
% 0.14/5.51 j(h(e13))=e13),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f241,plain,(
% 0.14/5.51 j(h(e14))=e14),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f242,plain,(
% 0.14/5.51 j(h(e15))=e15),
% 0.14/5.51 inference(cnf_transformation,[status(thm)],[f146])).
% 0.14/5.51 fof(f243,definition,(
% 0.14/5.51 sQ0_spl <=> (h(e10)=e20)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f244,plain,(
% 0.14/5.51 h(e10)=e20|~sQ0_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f243])).
% 0.14/5.51 fof(f246,definition,(
% 0.14/5.51 sQ1_spl <=> (h(e10)=e21)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f247,plain,(
% 0.14/5.51 h(e10)=e21|~sQ1_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f246])).
% 0.14/5.51 fof(f249,definition,(
% 0.14/5.51 sQ2_spl <=> (h(e10)=e22)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f250,plain,(
% 0.14/5.51 h(e10)=e22|~sQ2_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f249])).
% 0.14/5.51 fof(f252,definition,(
% 0.14/5.51 sQ3_spl <=> (h(e10)=e23)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f253,plain,(
% 0.14/5.51 h(e10)=e23|~sQ3_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f252])).
% 0.14/5.51 fof(f255,definition,(
% 0.14/5.51 sQ4_spl <=> (h(e10)=e24)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f256,plain,(
% 0.14/5.51 h(e10)=e24|~sQ4_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f255])).
% 0.14/5.51 fof(f258,definition,(
% 0.14/5.51 sQ5_spl <=> (h(e10)=e25)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f259,plain,(
% 0.14/5.51 h(e10)=e25|~sQ5_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f258])).
% 0.14/5.51 fof(f261,plain,(
% 0.14/5.51 sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl|sQ4_spl|sQ5_spl),
% 0.14/5.51 inference(split_clause,[status(thm)],[f147,f243,f246,f249,f252,f255,f258])).
% 0.14/5.51 fof(f281,definition,(
% 0.14/5.51 sQ12_spl <=> (h(e12)=e20)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f282,plain,(
% 0.14/5.51 h(e12)=e20|~sQ12_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f281])).
% 0.14/5.51 fof(f283,plain,(
% 0.14/5.51 ~h(e12)=e20|sQ12_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f281])).
% 0.14/5.51 fof(f284,definition,(
% 0.14/5.51 sQ13_spl <=> (h(e12)=e21)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f285,plain,(
% 0.14/5.51 h(e12)=e21|~sQ13_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f284])).
% 0.14/5.51 fof(f287,definition,(
% 0.14/5.51 sQ14_spl <=> (h(e12)=e22)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f288,plain,(
% 0.14/5.51 h(e12)=e22|~sQ14_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f287])).
% 0.14/5.51 fof(f290,definition,(
% 0.14/5.51 sQ15_spl <=> (h(e12)=e23)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f291,plain,(
% 0.14/5.51 h(e12)=e23|~sQ15_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f290])).
% 0.14/5.51 fof(f293,definition,(
% 0.14/5.51 sQ16_spl <=> (h(e12)=e24)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f294,plain,(
% 0.14/5.51 h(e12)=e24|~sQ16_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f293])).
% 0.14/5.51 fof(f296,definition,(
% 0.14/5.51 sQ17_spl <=> (h(e12)=e25)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f297,plain,(
% 0.14/5.51 h(e12)=e25|~sQ17_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f296])).
% 0.14/5.51 fof(f299,plain,(
% 0.14/5.51 sQ12_spl|sQ13_spl|sQ14_spl|sQ15_spl|sQ16_spl|sQ17_spl),
% 0.14/5.51 inference(split_clause,[status(thm)],[f149,f281,f284,f287,f290,f293,f296])).
% 0.14/5.51 fof(f300,definition,(
% 0.14/5.51 sQ18_spl <=> (h(e13)=e20)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f301,plain,(
% 0.14/5.51 h(e13)=e20|~sQ18_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f300])).
% 0.14/5.51 fof(f302,plain,(
% 0.14/5.51 ~h(e13)=e20|sQ18_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f300])).
% 0.14/5.51 fof(f303,definition,(
% 0.14/5.51 sQ19_spl <=> (h(e13)=e21)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f304,plain,(
% 0.14/5.51 h(e13)=e21|~sQ19_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f303])).
% 0.14/5.51 fof(f306,definition,(
% 0.14/5.51 sQ20_spl <=> (h(e13)=e22)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f307,plain,(
% 0.14/5.51 h(e13)=e22|~sQ20_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f306])).
% 0.14/5.51 fof(f309,definition,(
% 0.14/5.51 sQ21_spl <=> (h(e13)=e23)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f310,plain,(
% 0.14/5.51 h(e13)=e23|~sQ21_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f309])).
% 0.14/5.51 fof(f312,definition,(
% 0.14/5.51 sQ22_spl <=> (h(e13)=e24)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f313,plain,(
% 0.14/5.51 h(e13)=e24|~sQ22_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f312])).
% 0.14/5.51 fof(f314,plain,(
% 0.14/5.51 ~h(e13)=e24|sQ22_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f312])).
% 0.14/5.51 fof(f315,definition,(
% 0.14/5.51 sQ23_spl <=> (h(e13)=e25)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f316,plain,(
% 0.14/5.51 h(e13)=e25|~sQ23_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f315])).
% 0.14/5.51 fof(f318,plain,(
% 0.14/5.51 sQ18_spl|sQ19_spl|sQ20_spl|sQ21_spl|sQ22_spl|sQ23_spl),
% 0.14/5.51 inference(split_clause,[status(thm)],[f150,f300,f303,f306,f309,f312,f315])).
% 0.14/5.51 fof(f319,definition,(
% 0.14/5.51 sQ24_spl <=> (h(e14)=e20)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f320,plain,(
% 0.14/5.51 h(e14)=e20|~sQ24_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f319])).
% 0.14/5.51 fof(f321,plain,(
% 0.14/5.51 ~h(e14)=e20|sQ24_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f319])).
% 0.14/5.51 fof(f328,definition,(
% 0.14/5.51 sQ27_spl <=> (h(e14)=e23)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f329,plain,(
% 0.14/5.51 h(e14)=e23|~sQ27_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f328])).
% 0.14/5.51 fof(f331,definition,(
% 0.14/5.51 sQ28_spl <=> (h(e14)=e24)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f332,plain,(
% 0.14/5.51 h(e14)=e24|~sQ28_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f331])).
% 0.14/5.51 fof(f338,definition,(
% 0.14/5.51 sQ30_spl <=> (h(e15)=e20)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f339,plain,(
% 0.14/5.51 h(e15)=e20|~sQ30_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f338])).
% 0.14/5.51 fof(f341,definition,(
% 0.14/5.51 sQ31_spl <=> (h(e15)=e21)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f342,plain,(
% 0.14/5.51 h(e15)=e21|~sQ31_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f341])).
% 0.14/5.51 fof(f344,definition,(
% 0.14/5.51 sQ32_spl <=> (h(e15)=e22)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f345,plain,(
% 0.14/5.51 h(e15)=e22|~sQ32_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f344])).
% 0.14/5.51 fof(f347,definition,(
% 0.14/5.51 sQ33_spl <=> (h(e15)=e23)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f348,plain,(
% 0.14/5.51 h(e15)=e23|~sQ33_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f347])).
% 0.14/5.51 fof(f350,definition,(
% 0.14/5.51 sQ34_spl <=> (h(e15)=e24)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f351,plain,(
% 0.14/5.51 h(e15)=e24|~sQ34_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f350])).
% 0.14/5.51 fof(f353,definition,(
% 0.14/5.51 sQ35_spl <=> (h(e15)=e25)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f354,plain,(
% 0.14/5.51 h(e15)=e25|~sQ35_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f353])).
% 0.14/5.51 fof(f356,plain,(
% 0.14/5.51 sQ30_spl|sQ31_spl|sQ32_spl|sQ33_spl|sQ34_spl|sQ35_spl),
% 0.14/5.51 inference(split_clause,[status(thm)],[f152,f338,f341,f344,f347,f350,f353])).
% 0.14/5.51 fof(f357,definition,(
% 0.14/5.51 sQ36_spl <=> (j(e20)=e10)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f358,plain,(
% 0.14/5.51 j(e20)=e10|~sQ36_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f357])).
% 0.14/5.51 fof(f360,definition,(
% 0.14/5.51 sQ37_spl <=> (j(e20)=e11)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f361,plain,(
% 0.14/5.51 j(e20)=e11|~sQ37_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f360])).
% 0.14/5.51 fof(f363,definition,(
% 0.14/5.51 sQ38_spl <=> (j(e20)=e12)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f364,plain,(
% 0.14/5.51 j(e20)=e12|~sQ38_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f363])).
% 0.14/5.51 fof(f366,definition,(
% 0.14/5.51 sQ39_spl <=> (j(e20)=e13)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f367,plain,(
% 0.14/5.51 j(e20)=e13|~sQ39_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f366])).
% 0.14/5.51 fof(f369,definition,(
% 0.14/5.51 sQ40_spl <=> (j(e20)=e14)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f370,plain,(
% 0.14/5.51 j(e20)=e14|~sQ40_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f369])).
% 0.14/5.51 fof(f371,plain,(
% 0.14/5.51 ~j(e20)=e14|sQ40_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f369])).
% 0.14/5.51 fof(f372,definition,(
% 0.14/5.51 sQ41_spl <=> (j(e20)=e15)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f373,plain,(
% 0.14/5.51 j(e20)=e15|~sQ41_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f372])).
% 0.14/5.51 fof(f382,definition,(
% 0.14/5.51 sQ44_spl <=> (j(e21)=e12)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f383,plain,(
% 0.14/5.51 j(e21)=e12|~sQ44_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f382])).
% 0.14/5.51 fof(f385,definition,(
% 0.14/5.51 sQ45_spl <=> (j(e21)=e13)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f386,plain,(
% 0.14/5.51 j(e21)=e13|~sQ45_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f385])).
% 0.14/5.51 fof(f391,definition,(
% 0.14/5.51 sQ47_spl <=> (j(e21)=e15)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f392,plain,(
% 0.14/5.51 j(e21)=e15|~sQ47_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f391])).
% 0.14/5.51 fof(f395,definition,(
% 0.14/5.51 sQ48_spl <=> (j(e22)=e10)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f396,plain,(
% 0.14/5.51 j(e22)=e10|~sQ48_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f395])).
% 0.14/5.51 fof(f401,definition,(
% 0.14/5.51 sQ50_spl <=> (j(e22)=e12)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f402,plain,(
% 0.14/5.51 j(e22)=e12|~sQ50_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f401])).
% 0.14/5.51 fof(f404,definition,(
% 0.14/5.51 sQ51_spl <=> (j(e22)=e13)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f405,plain,(
% 0.14/5.51 j(e22)=e13|~sQ51_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f404])).
% 0.14/5.51 fof(f414,definition,(
% 0.14/5.51 sQ54_spl <=> (j(e23)=e10)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f415,plain,(
% 0.14/5.51 j(e23)=e10|~sQ54_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f414])).
% 0.14/5.51 fof(f416,plain,(
% 0.14/5.51 ~j(e23)=e10|sQ54_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f414])).
% 0.14/5.51 fof(f423,definition,(
% 0.14/5.51 sQ57_spl <=> (j(e23)=e13)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f424,plain,(
% 0.14/5.51 j(e23)=e13|~sQ57_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f423])).
% 0.14/5.51 fof(f426,definition,(
% 0.14/5.51 sQ58_spl <=> (j(e23)=e14)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f427,plain,(
% 0.14/5.51 j(e23)=e14|~sQ58_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f426])).
% 0.14/5.51 fof(f433,definition,(
% 0.14/5.51 sQ60_spl <=> (j(e24)=e10)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f434,plain,(
% 0.14/5.51 j(e24)=e10|~sQ60_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f433])).
% 0.14/5.51 fof(f436,definition,(
% 0.14/5.51 sQ61_spl <=> (j(e24)=e11)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f437,plain,(
% 0.14/5.51 j(e24)=e11|~sQ61_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f436])).
% 0.14/5.51 fof(f439,definition,(
% 0.14/5.51 sQ62_spl <=> (j(e24)=e12)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f440,plain,(
% 0.14/5.51 j(e24)=e12|~sQ62_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f439])).
% 0.14/5.51 fof(f441,plain,(
% 0.14/5.51 ~j(e24)=e12|sQ62_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f439])).
% 0.14/5.51 fof(f442,definition,(
% 0.14/5.51 sQ63_spl <=> (j(e24)=e13)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f443,plain,(
% 0.14/5.51 j(e24)=e13|~sQ63_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f442])).
% 0.14/5.51 fof(f445,definition,(
% 0.14/5.51 sQ64_spl <=> (j(e24)=e14)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f446,plain,(
% 0.14/5.51 j(e24)=e14|~sQ64_spl),
% 0.14/5.51 inference(component_clause,[status(thm)],[f445])).
% 0.14/5.51 fof(f448,definition,(
% 0.14/5.51 sQ65_spl <=> (j(e24)=e15)),
% 0.14/5.51 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.14/5.51 fof(f451,plain,(
% 0.14/5.51 sQ60_spl|sQ61_spl|sQ62_spl|sQ63_spl|sQ64_spl|sQ65_spl),
% 0.14/5.51 inference(split_clause,[status(thm)],[f157,f433,f436,f439,f442,f445,f448])).
% 0.14/5.51 fof(f509,plain,(
% 0.14/5.51 j(op2(e21,e21))=op1(e15,j(e21))|~sQ47_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f392,f202])).
% 0.14/5.51 fof(f510,plain,(
% 0.14/5.51 j(op2(e21,e21))=op1(e15,e15)|~sQ47_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f392,f509])).
% 0.14/5.51 fof(f519,plain,(
% 0.14/5.51 e12=e13|~sQ44_spl|~sQ45_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f383,f386])).
% 0.14/5.51 fof(f520,plain,(
% 0.14/5.51 $false|~sQ44_spl|~sQ45_spl),
% 0.14/5.51 inference(forward_subsumption_resolution,[status(thm)],[f519,f17])).
% 0.14/5.51 fof(f521,plain,(
% 0.14/5.51 ~sQ44_spl|~sQ45_spl),
% 0.14/5.51 inference(contradiction_clause,[status(thm)],[f520])).
% 0.14/5.51 fof(f533,plain,(
% 0.14/5.51 j(op2(e20,e20))=op1(j(e20),e15)|~sQ41_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f373,f195])).
% 0.14/5.51 fof(f534,plain,(
% 0.14/5.51 j(op2(e20,e20))=op1(e15,e15)|~sQ41_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f373,f533])).
% 0.14/5.51 fof(f538,plain,(
% 0.14/5.51 e12=e13|~sQ38_spl|~sQ39_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f364,f367])).
% 0.14/5.51 fof(f539,plain,(
% 0.14/5.51 $false|~sQ38_spl|~sQ39_spl),
% 0.14/5.51 inference(forward_subsumption_resolution,[status(thm)],[f538,f17])).
% 0.14/5.51 fof(f540,plain,(
% 0.14/5.51 ~sQ38_spl|~sQ39_spl),
% 0.14/5.51 inference(contradiction_clause,[status(thm)],[f539])).
% 0.14/5.51 fof(f544,plain,(
% 0.14/5.51 h(op1(e15,e15))=op2(h(e15),e25)|~sQ35_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f354,f194])).
% 0.14/5.51 fof(f555,plain,(
% 0.14/5.51 h(op1(e15,e15))=op2(e25,e25)|~sQ35_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f354,f544])).
% 0.14/5.51 fof(f584,plain,(
% 0.14/5.51 h(op1(e13,e13))=op2(h(e13),e25)|~sQ23_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f316,f180])).
% 0.14/5.51 fof(f591,plain,(
% 0.14/5.51 h(op1(e13,e13))=op2(e25,e25)|~sQ23_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f316,f584])).
% 0.14/5.51 fof(f595,plain,(
% 0.14/5.51 j(e23)=e13|~sQ21_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f310,f240])).
% 0.14/5.51 fof(f614,plain,(
% 0.14/5.51 h(op1(e12,e12))=op2(e24,h(e12))|~sQ16_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f294,f173])).
% 0.14/5.51 fof(f615,plain,(
% 0.14/5.51 h(op1(e12,e12))=op2(e24,e24)|~sQ16_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f294,f614])).
% 0.14/5.51 fof(f629,plain,(
% 0.14/5.51 h(op1(e12,e12))=op2(e23,h(e12))|~sQ15_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f291,f173])).
% 0.14/5.51 fof(f630,plain,(
% 0.14/5.51 h(op1(e12,e12))=op2(e23,e23)|~sQ15_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f291,f629])).
% 0.14/5.51 fof(f637,plain,(
% 0.14/5.51 j(e22)=e12|~sQ14_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f288,f239])).
% 0.14/5.51 fof(f657,plain,(
% 0.14/5.51 j(e21)=e12|~sQ13_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f285,f239])).
% 0.14/5.51 fof(f665,plain,(
% 0.14/5.51 j(e20)=e12|~sQ12_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f282,f239])).
% 0.14/5.51 fof(f666,plain,(
% 0.14/5.51 h(op1(e12,e12))=op2(e20,h(e12))|~sQ12_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f282,f173])).
% 0.14/5.51 fof(f667,plain,(
% 0.14/5.51 h(op1(e12,e12))=op2(e20,e20)|~sQ12_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f282,f666])).
% 0.14/5.51 fof(f693,plain,(
% 0.14/5.51 h(op1(e10,e10))=op2(h(e10),e25)|~sQ5_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f259,f159])).
% 0.14/5.51 fof(f695,plain,(
% 0.14/5.51 h(op1(e10,e10))=op2(e25,e25)|~sQ5_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f259,f693])).
% 0.14/5.51 fof(f707,plain,(
% 0.14/5.51 h(op1(e10,e10))=op2(e23,h(e10))|~sQ3_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f253,f159])).
% 0.14/5.51 fof(f708,plain,(
% 0.14/5.51 h(op1(e10,e10))=op2(e23,e23)|~sQ3_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f253,f707])).
% 0.14/5.51 fof(f725,plain,(
% 0.14/5.51 h(op1(e10,e10))=op2(e21,h(e10))|~sQ1_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f247,f159])).
% 0.14/5.51 fof(f726,plain,(
% 0.14/5.51 h(op1(e10,e10))=op2(e21,e21)|~sQ1_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f247,f725])).
% 0.14/5.51 fof(f735,plain,(
% 0.14/5.51 j(e20)=e10|~sQ0_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f244,f237])).
% 0.14/5.51 fof(f749,plain,(
% 0.14/5.51 j(op2(e24,e24))=op1(j(e24),e11)|~sQ61_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f437,f223])).
% 0.14/5.51 fof(f758,plain,(
% 0.14/5.51 j(op2(e24,e24))=op1(e11,e11)|~sQ61_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f437,f749])).
% 0.14/5.51 fof(f835,plain,(
% 0.14/5.51 e10=e12|~sQ0_spl|~sQ12_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f735,f665])).
% 0.14/5.51 fof(f836,plain,(
% 0.14/5.51 $false|~sQ0_spl|~sQ12_spl),
% 0.14/5.51 inference(forward_subsumption_resolution,[status(thm)],[f835,f9])).
% 0.14/5.51 fof(f837,plain,(
% 0.14/5.51 ~sQ0_spl|~sQ12_spl),
% 0.14/5.51 inference(contradiction_clause,[status(thm)],[f836])).
% 0.14/5.51 fof(f848,plain,(
% 0.14/5.51 h(e10)=e24|~sQ60_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f434,f235])).
% 0.14/5.51 fof(f852,plain,(
% 0.14/5.51 sQ4_spl|~sQ60_spl),
% 0.14/5.51 inference(split_clause,[status(thm)],[f848,f255,f433])).
% 0.14/5.51 fof(f875,plain,(
% 0.14/5.51 h(e10)=e22|~sQ48_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f396,f233])).
% 0.14/5.51 fof(f877,plain,(
% 0.14/5.51 sQ2_spl|~sQ48_spl),
% 0.14/5.51 inference(split_clause,[status(thm)],[f875,f249,f395])).
% 0.14/5.51 fof(f917,plain,(
% 0.14/5.51 e10=e14|~sQ36_spl|~sQ40_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f358,f370])).
% 0.14/5.51 fof(f918,plain,(
% 0.14/5.51 $false|~sQ36_spl|~sQ40_spl),
% 0.14/5.51 inference(forward_subsumption_resolution,[status(thm)],[f917,f11])).
% 0.14/5.51 fof(f919,plain,(
% 0.14/5.51 ~sQ36_spl|~sQ40_spl),
% 0.14/5.51 inference(contradiction_clause,[status(thm)],[f918])).
% 0.14/5.51 fof(f934,plain,(
% 0.14/5.51 j(e20)=e14|~sQ24_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f320,f241])).
% 0.14/5.51 fof(f948,plain,(
% 0.14/5.51 j(e22)=e13|~sQ20_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f307,f240])).
% 0.14/5.51 fof(f952,plain,(
% 0.14/5.51 sQ51_spl|~sQ20_spl),
% 0.14/5.51 inference(split_clause,[status(thm)],[f948,f404,f306])).
% 0.14/5.51 fof(f960,plain,(
% 0.14/5.51 h(e10)=e23|~sQ54_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f415,f234])).
% 0.14/5.51 fof(f967,plain,(
% 0.14/5.51 sQ3_spl|~sQ54_spl),
% 0.14/5.51 inference(split_clause,[status(thm)],[f960,f252,f414])).
% 0.14/5.51 fof(f975,plain,(
% 0.14/5.51 sQ50_spl|~sQ14_spl),
% 0.14/5.51 inference(split_clause,[status(thm)],[f637,f401,f287])).
% 0.14/5.51 fof(f976,plain,(
% 0.14/5.51 sQ44_spl|~sQ13_spl),
% 0.14/5.51 inference(split_clause,[status(thm)],[f657,f382,f284])).
% 0.14/5.51 fof(f990,plain,(
% 0.14/5.51 h(e10)=op2(h(e10),h(e10))),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f74,f159])).
% 0.14/5.51 fof(f1007,plain,(
% 0.14/5.51 h(op1(e15,e15))=op2(h(e15),e23)|~sQ33_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f348,f194])).
% 0.14/5.51 fof(f1008,plain,(
% 0.14/5.51 j(e23)=e15|~sQ33_spl),
% 0.14/5.51 inference(backward_demodulation,[status(thm)],[f348,f242])).
% 0.14/5.51 fof(f1011,plain,(
% 0.14/5.51 h(op1(e15,e15))=op2(e23,e23)|~sQ33_spl),
% 0.14/5.51 inference(forward_demodulation,[status(thm)],[f348,f1007])).
% 0.14/5.52 fof(f1015,plain,(
% 0.14/5.52 ~e14=e14|~sQ24_spl|sQ40_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f934,f371])).
% 0.14/5.52 fof(f1016,plain,(
% 0.14/5.52 $false|~sQ24_spl|sQ40_spl),
% 0.14/5.52 inference(trivial_equality_resolution,[status(thm)],[f1015])).
% 0.14/5.52 fof(f1017,plain,(
% 0.14/5.52 ~sQ24_spl|sQ40_spl),
% 0.14/5.52 inference(contradiction_clause,[status(thm)],[f1016])).
% 0.14/5.52 fof(f1026,plain,(
% 0.14/5.52 h(e13)=e24|~sQ63_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f443,f235])).
% 0.14/5.52 fof(f1027,plain,(
% 0.14/5.52 $false|sQ22_spl|~sQ63_spl),
% 0.14/5.52 inference(forward_subsumption_resolution,[status(thm)],[f1026,f314])).
% 0.14/5.52 fof(f1028,plain,(
% 0.14/5.52 sQ22_spl|~sQ63_spl),
% 0.14/5.52 inference(contradiction_clause,[status(thm)],[f1027])).
% 0.14/5.52 fof(f1054,plain,(
% 0.14/5.52 h(e10)=op2(h(e10),e22)|~sQ2_spl),
% 0.14/5.52 inference(backward_demodulation,[status(thm)],[f250,f990])).
% 0.14/5.52 fof(f1059,plain,(
% 0.14/5.52 e22=op2(h(e10),e22)|~sQ2_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f250,f1054])).
% 0.14/5.52 fof(f1060,plain,(
% 0.14/5.52 e22=op2(e22,e22)|~sQ2_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f250,f1059])).
% 0.14/5.52 fof(f1077,plain,(
% 0.14/5.52 h(e10)=e20|~sQ36_spl),
% 0.14/5.52 inference(backward_demodulation,[status(thm)],[f358,f231])).
% 0.14/5.52 fof(f1080,plain,(
% 0.14/5.52 sQ0_spl|~sQ36_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f1077,f243,f357])).
% 0.14/5.52 fof(f1104,plain,(
% 0.14/5.52 j(op2(e23,e23))=op1(e13,j(e23))|~sQ57_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f424,f216])).
% 0.14/5.52 fof(f1105,plain,(
% 0.14/5.52 j(op2(e23,e23))=op1(e13,e13)|~sQ57_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f424,f1104])).
% 0.14/5.52 fof(f1114,plain,(
% 0.14/5.52 h(e13)=e23|~sQ57_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f424,f234])).
% 0.14/5.52 fof(f1159,plain,(
% 0.14/5.52 e13=e15|~sQ57_spl|~sQ33_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f424,f1008])).
% 0.14/5.52 fof(f1160,plain,(
% 0.14/5.52 $false|~sQ57_spl|~sQ33_spl),
% 0.14/5.52 inference(forward_subsumption_resolution,[status(thm)],[f1159,f21])).
% 0.14/5.52 fof(f1161,plain,(
% 0.14/5.52 ~sQ57_spl|~sQ33_spl),
% 0.14/5.52 inference(contradiction_clause,[status(thm)],[f1160])).
% 0.14/5.52 fof(f1167,plain,(
% 0.14/5.52 h(op1(e13,e15))=op2(e23,h(e15))|~sQ57_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f1114,f182])).
% 0.14/5.52 fof(f1195,plain,(
% 0.14/5.52 j(op2(e23,e20))=op1(e13,j(e20))|~sQ57_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f424,f213])).
% 0.14/5.52 fof(f1205,plain,(
% 0.14/5.52 h(op1(e14,e14))=op2(h(e14),e24)|~sQ28_spl),
% 0.14/5.52 inference(backward_demodulation,[status(thm)],[f332,f187])).
% 0.14/5.52 fof(f1220,plain,(
% 0.14/5.52 h(op1(e14,e14))=op2(e24,e24)|~sQ28_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f332,f1205])).
% 0.14/5.52 fof(f1224,plain,(
% 0.14/5.52 j(op2(e24,e23))=op1(j(e24),e13)|~sQ57_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f424,f222])).
% 0.14/5.52 fof(f1232,plain,(
% 0.14/5.52 j(op2(e24,e23))=op1(e12,e13)|~sQ62_spl|~sQ57_spl),
% 0.14/5.52 inference(backward_demodulation,[status(thm)],[f440,f1224])).
% 0.14/5.52 fof(f1236,plain,(
% 0.14/5.52 h(e12)=e24|~sQ62_spl),
% 0.14/5.52 inference(backward_demodulation,[status(thm)],[f440,f235])).
% 0.14/5.52 fof(f1239,plain,(
% 0.14/5.52 j(op2(e24,e23))=e10|~sQ62_spl|~sQ57_spl),
% 0.14/5.52 inference(forward_demodulation,[status(thm)],[f89,f1232])).
% 0.14/5.52 fof(f1244,plain,(
% 0.14/5.52 sQ16_spl|~sQ62_spl),
% 0.14/5.52 inference(split_clause,[status(thm)],[f1236,f293,f439])).
% 0.14/5.52 fof(f1246,plain,(
% 0.14/5.52 j(op2(e23,e23))=e12|~sQ57_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f95,f1105])).
% 0.14/5.53 fof(f1263,plain,(
% 0.14/5.53 h(e12)=op2(h(e13),h(e13))),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f95,f180])).
% 0.14/5.53 fof(f1264,plain,(
% 0.14/5.53 e25=op2(h(e13),h(e13))|~sQ17_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f297,f1263])).
% 0.14/5.53 fof(f1269,plain,(
% 0.14/5.53 sQ57_spl|~sQ21_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f595,f423,f309])).
% 0.14/5.53 fof(f1280,plain,(
% 0.14/5.53 h(e14)=op2(e23,h(e15))|~sQ57_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f97,f1167])).
% 0.14/5.53 fof(f1361,plain,(
% 0.14/5.53 h(op1(e15,e15))=op2(e22,h(e15))|~sQ32_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f345,f194])).
% 0.14/5.53 fof(f1362,plain,(
% 0.14/5.53 h(op1(e15,e15))=op2(e22,e22)|~sQ32_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f345,f1361])).
% 0.14/5.53 fof(f1411,plain,(
% 0.14/5.53 h(e13)=e20|~sQ39_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f367,f231])).
% 0.14/5.53 fof(f1413,plain,(
% 0.14/5.53 j(op2(e20,e20))=op1(e13,j(e20))|~sQ39_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f367,f195])).
% 0.14/5.53 fof(f1414,plain,(
% 0.14/5.53 j(op2(e20,e20))=op1(e13,e13)|~sQ39_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f367,f1413])).
% 0.14/5.53 fof(f1415,plain,(
% 0.14/5.53 j(op2(e20,e20))=e12|~sQ39_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f95,f1414])).
% 0.14/5.53 fof(f1424,plain,(
% 0.14/5.53 h(op1(e14,e14))=op2(h(e14),e23)|~sQ27_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f329,f187])).
% 0.14/5.53 fof(f1430,plain,(
% 0.14/5.53 h(op1(e14,e14))=op2(e23,e23)|~sQ27_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f329,f1424])).
% 0.14/5.53 fof(f1434,plain,(
% 0.14/5.53 ~e20=e20|~sQ39_spl|sQ18_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f1411,f302])).
% 0.14/5.53 fof(f1435,plain,(
% 0.14/5.53 $false|~sQ39_spl|sQ18_spl),
% 0.14/5.53 inference(trivial_equality_resolution,[status(thm)],[f1434])).
% 0.14/5.53 fof(f1436,plain,(
% 0.14/5.53 ~sQ39_spl|sQ18_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f1435])).
% 0.14/5.53 fof(f1465,plain,(
% 0.14/5.53 e25=op2(h(e13),e21)|~sQ19_spl|~sQ17_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f304,f1264])).
% 0.14/5.53 fof(f1466,plain,(
% 0.14/5.53 j(e21)=e13|~sQ19_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f304,f240])).
% 0.14/5.53 fof(f1473,plain,(
% 0.14/5.53 e25=op2(e21,e21)|~sQ19_spl|~sQ17_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f304,f1465])).
% 0.14/5.53 fof(f1474,plain,(
% 0.14/5.53 sQ45_spl|~sQ19_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1466,f385,f303])).
% 0.14/5.53 fof(f1481,plain,(
% 0.14/5.53 h(e14)=e23|~sQ58_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f427,f234])).
% 0.14/5.53 fof(f1495,plain,(
% 0.14/5.53 e24=op2(h(e10),h(e10))|~sQ4_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f256,f990])).
% 0.14/5.53 fof(f1496,plain,(
% 0.14/5.53 e24=op2(e24,h(e10))|~sQ4_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f256,f1495])).
% 0.14/5.53 fof(f1497,plain,(
% 0.14/5.53 e24=op2(e24,e24)|~sQ4_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f256,f1496])).
% 0.14/5.53 fof(f1578,plain,(
% 0.14/5.53 sQ27_spl|~sQ58_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1481,f328,f426])).
% 0.14/5.53 fof(f1600,plain,(
% 0.14/5.53 h(e13)=op2(e23,e23)|~sQ27_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f102,f1430])).
% 0.14/5.53 fof(f1630,plain,(
% 0.14/5.53 j(e20)=op1(j(e20),j(e20))),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f110,f195])).
% 0.14/5.53 fof(f1631,plain,(
% 0.14/5.53 e11=op1(j(e20),j(e20))|~sQ37_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f361,f1630])).
% 0.14/5.53 fof(f1632,plain,(
% 0.14/5.53 e11=op1(e11,j(e20))|~sQ37_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f361,f1631])).
% 0.14/5.53 fof(f1633,plain,(
% 0.14/5.53 e11=op1(e11,e11)|~sQ37_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f361,f1632])).
% 0.14/5.53 fof(f1634,plain,(
% 0.14/5.53 e11=e10|~sQ37_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f81,f1633])).
% 0.14/5.53 fof(f1635,plain,(
% 0.14/5.53 $false|~sQ37_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1634,f8])).
% 0.14/5.53 fof(f1636,plain,(
% 0.14/5.53 ~sQ37_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f1635])).
% 0.14/5.53 fof(f1643,plain,(
% 0.14/5.53 j(e20)=op1(e15,e15)|~sQ41_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f110,f534])).
% 0.14/5.53 fof(f1644,plain,(
% 0.14/5.53 j(e20)=e12|~sQ41_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f109,f1643])).
% 0.14/5.53 fof(f1647,plain,(
% 0.14/5.53 h(e10)=op2(e23,e23)|~sQ3_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f74,f708])).
% 0.14/5.53 fof(f1648,plain,(
% 0.14/5.53 j(e24)=op1(j(e20),j(e24))),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f114,f199])).
% 0.14/5.53 fof(f1660,plain,(
% 0.14/5.53 j(e24)=op1(j(e20),e13)|~sQ22_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f1661,f1648])).
% 0.14/5.53 fof(f1661,plain,(
% 0.14/5.53 j(e24)=e13|~sQ22_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f313,f240])).
% 0.14/5.53 fof(f1662,plain,(
% 0.14/5.53 e13=op1(j(e20),e13)|~sQ22_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f1661,f1660])).
% 0.14/5.53 fof(f1679,plain,(
% 0.14/5.53 h(e10)=op2(e21,e21)|~sQ1_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f74,f726])).
% 0.14/5.53 fof(f1680,plain,(
% 0.14/5.53 h(e10)=e20|~sQ1_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f117,f1679])).
% 0.14/5.53 fof(f1685,plain,(
% 0.14/5.53 j(e22)=op1(j(e22),j(e20))),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f122,f207])).
% 0.14/5.53 fof(f1696,plain,(
% 0.14/5.53 j(op2(e22,e22))=op1(j(e22),e12)|~sQ50_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f402,f209])).
% 0.14/5.53 fof(f1701,plain,(
% 0.14/5.53 j(op2(e22,e22))=op1(e12,e12)|~sQ50_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f402,f1696])).
% 0.14/5.53 fof(f1702,plain,(
% 0.14/5.53 j(op2(e22,e22))=e13|~sQ50_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f88,f1701])).
% 0.14/5.53 fof(f1727,plain,(
% 0.14/5.53 j(e20)=op1(j(e22),j(e22))),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f124,f209])).
% 0.14/5.53 fof(f1737,plain,(
% 0.14/5.53 h(e13)=op2(e20,e20)|~sQ12_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f88,f667])).
% 0.14/5.53 fof(f1738,plain,(
% 0.14/5.53 e24=op2(e20,e20)|~sQ22_spl|~sQ12_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f313,f1737])).
% 0.14/5.53 fof(f1739,plain,(
% 0.14/5.53 e24=e20|~sQ22_spl|~sQ12_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f110,f1738])).
% 0.14/5.53 fof(f1740,plain,(
% 0.14/5.53 $false|~sQ22_spl|~sQ12_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1739,f26])).
% 0.14/5.53 fof(f1741,plain,(
% 0.14/5.53 ~sQ22_spl|~sQ12_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f1740])).
% 0.14/5.53 fof(f1746,plain,(
% 0.14/5.53 h(e13)=op2(e23,e23)|~sQ15_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f88,f630])).
% 0.14/5.53 fof(f1748,plain,(
% 0.14/5.53 h(e10)=op2(e25,e25)|~sQ5_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f74,f695])).
% 0.14/5.53 fof(f1749,plain,(
% 0.14/5.53 j(e20)=op1(e15,e15)|~sQ47_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f117,f510])).
% 0.14/5.53 fof(f1750,plain,(
% 0.14/5.53 j(e20)=e12|~sQ47_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f109,f1749])).
% 0.14/5.53 fof(f1769,plain,(
% 0.14/5.53 h(e12)=e20|~sQ41_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f1644,f231])).
% 0.14/5.53 fof(f1772,plain,(
% 0.14/5.53 sQ12_spl|~sQ41_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1769,f281,f372])).
% 0.14/5.53 fof(f1773,plain,(
% 0.14/5.53 h(e13)=e20|~sQ12_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f110,f1737])).
% 0.14/5.53 fof(f1782,plain,(
% 0.14/5.53 h(e12)=op2(e22,e22)|~sQ32_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f109,f1362])).
% 0.14/5.53 fof(f1783,plain,(
% 0.14/5.53 h(e12)=e20|~sQ32_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f124,f1782])).
% 0.14/5.53 fof(f1794,plain,(
% 0.14/5.53 j(op2(e24,e24))=e10|~sQ61_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f81,f758])).
% 0.14/5.53 fof(f1850,plain,(
% 0.14/5.53 e13=op1(j(e22),j(e20))|~sQ51_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f405,f1685])).
% 0.14/5.53 fof(f1851,plain,(
% 0.14/5.53 e13=op1(e13,j(e20))|~sQ51_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f405,f1850])).
% 0.14/5.53 fof(f1857,plain,(
% 0.14/5.53 ~e20=e20|~sQ12_spl|sQ18_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f1773,f302])).
% 0.14/5.53 fof(f1858,plain,(
% 0.14/5.53 $false|~sQ12_spl|sQ18_spl),
% 0.14/5.53 inference(trivial_equality_resolution,[status(thm)],[f1857])).
% 0.14/5.53 fof(f1859,plain,(
% 0.14/5.53 ~sQ12_spl|sQ18_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f1858])).
% 0.14/5.53 fof(f1868,plain,(
% 0.14/5.53 h(e13)=e24|~sQ15_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f131,f1746])).
% 0.14/5.53 fof(f1888,plain,(
% 0.14/5.53 j(e20)=op1(e13,j(e22))|~sQ51_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f405,f1727])).
% 0.14/5.53 fof(f1889,plain,(
% 0.14/5.53 j(e20)=op1(e13,e13)|~sQ51_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f405,f1888])).
% 0.14/5.53 fof(f1891,plain,(
% 0.14/5.53 e13=op1(e13,e12)|~sQ51_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f1897,f1851])).
% 0.14/5.53 fof(f1897,plain,(
% 0.14/5.53 j(e20)=e12|~sQ51_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f95,f1889])).
% 0.14/5.53 fof(f1898,plain,(
% 0.14/5.53 e13=e10|~sQ51_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f94,f1891])).
% 0.14/5.53 fof(f1899,plain,(
% 0.14/5.53 $false|~sQ51_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1898,f10])).
% 0.14/5.53 fof(f1900,plain,(
% 0.14/5.53 ~sQ51_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f1899])).
% 0.14/5.53 fof(f1917,plain,(
% 0.14/5.53 sQ12_spl|~sQ32_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1783,f281,f344])).
% 0.14/5.53 fof(f1923,plain,(
% 0.14/5.53 j(e23)=op1(e13,j(e20))|~sQ57_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f128,f1195])).
% 0.14/5.53 fof(f1927,plain,(
% 0.14/5.53 j(e24)=e12|~sQ57_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f131,f1246])).
% 0.14/5.53 fof(f1928,plain,(
% 0.14/5.53 $false|sQ62_spl|~sQ57_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1927,f441])).
% 0.14/5.53 fof(f1929,plain,(
% 0.14/5.53 sQ62_spl|~sQ57_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f1928])).
% 0.14/5.53 fof(f1940,plain,(
% 0.14/5.53 j(e20)=e13|~sQ50_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f124,f1702])).
% 0.14/5.53 fof(f1942,plain,(
% 0.14/5.53 h(e13)=op2(e24,e24)|~sQ28_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f102,f1220])).
% 0.14/5.53 fof(f1943,plain,(
% 0.14/5.53 h(e13)=e23|~sQ28_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f138,f1942])).
% 0.14/5.53 fof(f1947,plain,(
% 0.14/5.53 e24=e23|~sQ4_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f138,f1497])).
% 0.14/5.53 fof(f1948,plain,(
% 0.14/5.53 $false|~sQ4_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1947,f35])).
% 0.14/5.53 fof(f1949,plain,(
% 0.14/5.53 ~sQ4_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f1948])).
% 0.14/5.53 fof(f1950,plain,(
% 0.14/5.53 h(e13)=op2(e24,e24)|~sQ16_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f88,f615])).
% 0.14/5.53 fof(f1951,plain,(
% 0.14/5.53 h(e13)=e23|~sQ16_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f138,f1950])).
% 0.14/5.53 fof(f1978,plain,(
% 0.14/5.53 h(e14)=e24|~sQ64_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f446,f235])).
% 0.14/5.53 fof(f2045,plain,(
% 0.14/5.53 j(e23)=e13|~sQ28_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f1943,f240])).
% 0.14/5.53 fof(f2050,plain,(
% 0.14/5.53 sQ57_spl|~sQ28_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f2045,f423,f331])).
% 0.14/5.53 fof(f2059,plain,(
% 0.14/5.53 h(e13)=e24|~sQ27_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f131,f1600])).
% 0.14/5.53 fof(f2097,plain,(
% 0.14/5.53 e25=e20|~sQ19_spl|~sQ17_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f117,f1473])).
% 0.14/5.53 fof(f2098,plain,(
% 0.14/5.53 $false|~sQ19_spl|~sQ17_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2097,f27])).
% 0.14/5.53 fof(f2099,plain,(
% 0.14/5.53 ~sQ19_spl|~sQ17_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f2098])).
% 0.14/5.53 fof(f2117,plain,(
% 0.14/5.53 sQ21_spl|~sQ16_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1951,f309,f293])).
% 0.14/5.53 fof(f2136,plain,(
% 0.14/5.53 sQ28_spl|~sQ64_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1978,f331,f445])).
% 0.14/5.53 fof(f2153,plain,(
% 0.14/5.53 j(e23)=e10|~sQ61_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f138,f1794])).
% 0.14/5.53 fof(f2154,plain,(
% 0.14/5.53 $false|sQ54_spl|~sQ61_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2153,f416])).
% 0.14/5.53 fof(f2155,plain,(
% 0.14/5.53 sQ54_spl|~sQ61_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f2154])).
% 0.14/5.53 fof(f2174,plain,(
% 0.14/5.53 j(e20)=e12|~sQ39_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f110,f1415])).
% 0.14/5.53 fof(f2185,plain,(
% 0.14/5.53 sQ0_spl|~sQ1_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1680,f243,f246])).
% 0.14/5.53 fof(f2187,plain,(
% 0.14/5.53 h(e10)=e24|~sQ3_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f131,f1647])).
% 0.14/5.53 fof(f2202,plain,(
% 0.14/5.53 e22=e20|~sQ2_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f124,f1060])).
% 0.14/5.53 fof(f2203,plain,(
% 0.14/5.53 $false|~sQ2_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2202,f24])).
% 0.14/5.53 fof(f2204,plain,(
% 0.14/5.53 ~sQ2_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f2203])).
% 0.14/5.53 fof(f2206,plain,(
% 0.14/5.53 j(e20)=e10|~sQ62_spl|~sQ57_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f137,f1239])).
% 0.14/5.53 fof(f2213,plain,(
% 0.14/5.53 sQ39_spl|~sQ50_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1940,f366,f401])).
% 0.14/5.53 fof(f2214,plain,(
% 0.14/5.53 sQ4_spl|~sQ3_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f2187,f255,f252])).
% 0.14/5.53 fof(f2224,plain,(
% 0.14/5.53 h(e10)=e20|~sQ5_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f145,f1748])).
% 0.14/5.53 fof(f2225,plain,(
% 0.14/5.53 sQ38_spl|~sQ39_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f2174,f363,f366])).
% 0.14/5.53 fof(f2230,plain,(
% 0.14/5.53 sQ36_spl|~sQ62_spl|~sQ57_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f2206,f357,f439,f423])).
% 0.14/5.53 fof(f2231,plain,(
% 0.14/5.53 sQ22_spl|~sQ27_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f2059,f312,f328])).
% 0.14/5.53 fof(f2254,plain,(
% 0.14/5.53 j(e21)=e15|~sQ31_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f342,f242])).
% 0.14/5.53 fof(f2258,plain,(
% 0.14/5.53 sQ47_spl|~sQ31_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f2254,f391,f341])).
% 0.14/5.53 fof(f2272,plain,(
% 0.14/5.53 sQ22_spl|~sQ15_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1868,f312,f290])).
% 0.14/5.53 fof(f2398,plain,(
% 0.14/5.53 sQ0_spl|~sQ5_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f2224,f243,f258])).
% 0.14/5.53 fof(f2403,plain,(
% 0.14/5.53 sQ38_spl|~sQ47_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f1750,f363,f391])).
% 0.14/5.53 fof(f2500,plain,(
% 0.14/5.53 j(e20)=e13|~sQ18_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f301,f240])).
% 0.14/5.53 fof(f2505,plain,(
% 0.14/5.53 sQ39_spl|~sQ18_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f2500,f366,f300])).
% 0.14/5.53 fof(f2529,plain,(
% 0.14/5.53 h(e12)=op2(e25,e25)|~sQ23_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f95,f591])).
% 0.14/5.53 fof(f2530,plain,(
% 0.14/5.53 h(e12)=e20|~sQ23_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f145,f2529])).
% 0.14/5.53 fof(f2531,plain,(
% 0.14/5.53 $false|sQ12_spl|~sQ23_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2530,f283])).
% 0.14/5.53 fof(f2532,plain,(
% 0.14/5.53 sQ12_spl|~sQ23_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f2531])).
% 0.14/5.53 fof(f2542,plain,(
% 0.14/5.53 j(e20)=e15|~sQ30_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f339,f242])).
% 0.14/5.53 fof(f2549,plain,(
% 0.14/5.53 sQ41_spl|~sQ30_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f2542,f372,f338])).
% 0.14/5.53 fof(f2562,plain,(
% 0.14/5.53 h(e12)=op2(e23,e23)|~sQ33_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f109,f1011])).
% 0.14/5.53 fof(f2563,plain,(
% 0.14/5.53 h(e12)=e24|~sQ33_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f131,f2562])).
% 0.14/5.53 fof(f2592,plain,(
% 0.14/5.53 e13=op1(e12,e13)|~sQ38_spl|~sQ22_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f364,f1662])).
% 0.14/5.53 fof(f2593,plain,(
% 0.14/5.53 e13=e10|~sQ38_spl|~sQ22_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f89,f2592])).
% 0.14/5.53 fof(f2594,plain,(
% 0.14/5.53 $false|~sQ38_spl|~sQ22_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2593,f10])).
% 0.14/5.53 fof(f2595,plain,(
% 0.14/5.53 ~sQ38_spl|~sQ22_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f2594])).
% 0.14/5.53 fof(f2596,plain,(
% 0.14/5.53 j(e23)=op1(e13,e12)|~sQ38_spl|~sQ57_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f364,f1923])).
% 0.14/5.53 fof(f2597,plain,(
% 0.14/5.53 j(e23)=e10|~sQ38_spl|~sQ57_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f94,f2596])).
% 0.14/5.53 fof(f2598,plain,(
% 0.14/5.53 $false|sQ54_spl|~sQ38_spl|~sQ57_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2597,f416])).
% 0.14/5.53 fof(f2599,plain,(
% 0.14/5.53 sQ54_spl|~sQ38_spl|~sQ57_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f2598])).
% 0.14/5.53 fof(f2615,plain,(
% 0.14/5.53 h(e12)=op2(e25,e25)|~sQ35_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f109,f555])).
% 0.14/5.53 fof(f2616,plain,(
% 0.14/5.53 h(e12)=e20|~sQ35_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f145,f2615])).
% 0.14/5.53 fof(f2617,plain,(
% 0.14/5.53 $false|sQ12_spl|~sQ35_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2616,f283])).
% 0.14/5.53 fof(f2618,plain,(
% 0.14/5.53 sQ12_spl|~sQ35_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f2617])).
% 0.14/5.53 fof(f2619,plain,(
% 0.14/5.53 sQ16_spl|~sQ33_spl),
% 0.14/5.53 inference(split_clause,[status(thm)],[f2563,f293,f347])).
% 0.14/5.53 fof(f2810,plain,(
% 0.14/5.53 j(e24)=e15|~sQ34_spl),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f351,f242])).
% 0.14/5.53 fof(f2823,plain,(
% 0.14/5.53 e13=e15|~sQ22_spl|~sQ34_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f1661,f2810])).
% 0.14/5.53 fof(f2824,plain,(
% 0.14/5.53 $false|~sQ22_spl|~sQ34_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2823,f21])).
% 0.14/5.53 fof(f2825,plain,(
% 0.14/5.53 ~sQ22_spl|~sQ34_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f2824])).
% 0.14/5.53 fof(f2841,plain,(
% 0.14/5.53 h(e14)=op2(e23,e24)|~sQ34_spl|~sQ57_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f351,f1280])).
% 0.14/5.53 fof(f2842,plain,(
% 0.14/5.53 h(e14)=e20|~sQ34_spl|~sQ57_spl),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f132,f2841])).
% 0.14/5.53 fof(f2843,plain,(
% 0.14/5.53 $false|sQ24_spl|~sQ34_spl|~sQ57_spl),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2842,f321])).
% 0.14/5.53 fof(f2844,plain,(
% 0.14/5.53 sQ24_spl|~sQ34_spl|~sQ57_spl),
% 0.14/5.53 inference(contradiction_clause,[status(thm)],[f2843])).
% 0.14/5.53 fof(f2845,plain,(
% 0.14/5.53 $false),
% 0.14/5.53 inference(sat_refutation,[status(thm)],[f261,f299,f318,f356,f451,f521,f540,f837,f852,f877,f919,f952,f967,f975,f976,f1017,f1028,f1080,f1161,f1244,f1269,f1436,f1474,f1578,f1636,f1741,f1772,f1859,f1900,f1917,f1929,f1949,f2050,f2099,f2117,f2136,f2155,f2185,f2204,f2213,f2214,f2225,f2230,f2231,f2258,f2272,f2398,f2403,f2505,f2532,f2549,f2595,f2599,f2618,f2619,f2825,f2844])).
% 0.14/5.53 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.54 % Elapsed time: 0.152743 seconds
% 0.14/5.54 % CPU time: 0.966994 seconds
% 0.14/5.54 % Total memory used: 132.652 MB
% 0.14/5.54 % Net memory used: 132.304 MB
%------------------------------------------------------------------------------