%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG081+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 : n003.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:34 AM UTC 2026
% Result : Theorem 0.16s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG081+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.41 % Computer : n003.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Mon Sep 21 12:57:16 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.16/0.43 % Drodi V4.1.1
% 0.16/0.57 % Refutation found
% 0.16/0.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.57 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.57 fof(f1,axiom,(
% 0.16/0.57 ( e10 != e11& e10 != e12& e10 != e13& e10 != e14& e11 != e12& e11 != e13& e11 != e14& e12 != e13& e12 != e14& e13 != e14 ) ),
% 0.16/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f2,axiom,(
% 0.16/0.57 ( e20 != e21& e20 != e22& e20 != e23& e20 != e24& e21 != e22& e21 != e23& e21 != e24& e22 != e23& e22 != e24& e23 != e24 ) ),
% 0.16/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f4,axiom,(
% 0.16/0.57 ( op1(e10,e10) = e10& op1(e10,e11) = e11& op1(e10,e12) = e12& op1(e10,e13) = e13& op1(e10,e14) = e14& op1(e11,e10) = e11& op1(e11,e11) = e12& op1(e11,e12) = e13& op1(e11,e13) = e14& op1(e11,e14) = e10& op1(e12,e10) = e12& op1(e12,e11) = e14& op1(e12,e12) = e11& op1(e12,e13) = e10& op1(e12,e14) = e13& op1(e13,e10) = e13& op1(e13,e11) = e10& op1(e13,e12) = e14& op1(e13,e13) = e11& op1(e13,e14) = e12& op1(e14,e10) = e14& op1(e14,e11) = e13& op1(e14,e12) = e10& op1(e14,e13) = e12& op1(e14,e14) = e11 ) ),
% 0.16/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f5,axiom,(
% 0.16/0.57 ( op2(e20,e20) = e20& op2(e20,e21) = e21& op2(e20,e22) = e22& op2(e20,e23) = e23& op2(e20,e24) = e24& op2(e21,e20) = e21& op2(e21,e21) = e22& op2(e21,e22) = e24& op2(e21,e23) = e20& op2(e21,e24) = e23& op2(e22,e20) = e22& op2(e22,e21) = e20& op2(e22,e22) = e23& op2(e22,e23) = e24& op2(e22,e24) = e21& op2(e23,e20) = e23& op2(e23,e21) = e24& op2(e23,e22) = e20& op2(e23,e23) = e21& op2(e23,e24) = e22& op2(e24,e20) = e24& op2(e24,e21) = e23& op2(e24,e22) = e21& op2(e24,e23) = e22& op2(e24,e24) = e20 ) ),
% 0.16/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f6,conjecture,(
% 0.16/0.57 ( ( ( h(e10) = e20| h(e10) = e21| h(e10) = e22| h(e10) = e23| h(e10) = e24 )& ( h(e11) = e20| h(e11) = e21| h(e11) = e22| h(e11) = e23| h(e11) = e24 )& ( h(e12) = e20| h(e12) = e21| h(e12) = e22| h(e12) = e23| h(e12) = e24 )& ( h(e13) = e20| h(e13) = e21| h(e13) = e22| h(e13) = e23| h(e13) = e24 )& ( h(e14) = e20| h(e14) = e21| h(e14) = e22| h(e14) = e23| h(e14) = e24 )& ( j(e20) = e10| j(e20) = e11| j(e20) = e12| j(e20) = e13| j(e20) = e14 )& ( j(e21) = e10| j(e21) = e11| j(e21) = e12| j(e21) = e13| j(e21) = e14 )& ( j(e22) = e10| j(e22) = e11| j(e22) = e12| j(e22) = e13| j(e22) = e14 )& ( j(e23) = e10| j(e23) = e11| j(e23) = e12| j(e23) = e13| j(e23) = e14 )& ( j(e24) = e10| j(e24) = e11| j(e24) = e12| j(e24) = e13| j(e24) = e14 ) )=> ~ ( 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(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(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(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(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))& 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(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(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(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(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))& h(j(e20)) = e20& h(j(e21)) = e21& h(j(e22)) = e22& h(j(e23)) = e23& h(j(e24)) = e24& j(h(e10)) = e10& j(h(e11)) = e11& j(h(e12)) = e12& j(h(e13)) = e13& j(h(e14)) = e14 ) ) ),
% 0.16/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.57 fof(f7,negated_conjecture,(
% 0.16/0.57 ~(( ( ( h(e10) = e20| h(e10) = e21| h(e10) = e22| h(e10) = e23| h(e10) = e24 )& ( h(e11) = e20| h(e11) = e21| h(e11) = e22| h(e11) = e23| h(e11) = e24 )& ( h(e12) = e20| h(e12) = e21| h(e12) = e22| h(e12) = e23| h(e12) = e24 )& ( h(e13) = e20| h(e13) = e21| h(e13) = e22| h(e13) = e23| h(e13) = e24 )& ( h(e14) = e20| h(e14) = e21| h(e14) = e22| h(e14) = e23| h(e14) = e24 )& ( j(e20) = e10| j(e20) = e11| j(e20) = e12| j(e20) = e13| j(e20) = e14 )& ( j(e21) = e10| j(e21) = e11| j(e21) = e12| j(e21) = e13| j(e21) = e14 )& ( j(e22) = e10| j(e22) = e11| j(e22) = e12| j(e22) = e13| j(e22) = e14 )& ( j(e23) = e10| j(e23) = e11| j(e23) = e12| j(e23) = e13| j(e23) = e14 )& ( j(e24) = e10| j(e24) = e11| j(e24) = e12| j(e24) = e13| j(e24) = e14 ) )=> ~ ( 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(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(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(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(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))& 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(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(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(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(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))& h(j(e20)) = e20& h(j(e21)) = e21& h(j(e22)) = e22& h(j(e23)) = e23& h(j(e24)) = e24& j(h(e10)) = e10& j(h(e11)) = e11& j(h(e12)) = e12& j(h(e13)) = e13& j(h(e14)) = e14 ) ) )),
% 0.16/0.57 inference(negated_conjecture,[status(cth)],[f6])).
% 0.16/0.57 fof(f11,plain,(
% 0.16/0.57 ~e10=e14),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f1])).
% 0.16/0.57 fof(f12,plain,(
% 0.16/0.57 ~e11=e12),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f1])).
% 0.16/0.57 fof(f16,plain,(
% 0.16/0.57 ~e12=e14),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f1])).
% 0.16/0.57 fof(f17,plain,(
% 0.16/0.57 ~e13=e14),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f1])).
% 0.16/0.57 fof(f18,plain,(
% 0.16/0.57 ~e20=e21),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f2])).
% 0.16/0.57 fof(f20,plain,(
% 0.16/0.57 ~e20=e23),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f2])).
% 0.16/0.57 fof(f22,plain,(
% 0.16/0.57 ~e21=e22),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f2])).
% 0.16/0.57 fof(f23,plain,(
% 0.16/0.57 ~e21=e23),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f2])).
% 0.16/0.57 fof(f27,plain,(
% 0.16/0.57 ~e23=e24),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f2])).
% 0.16/0.57 fof(f53,plain,(
% 0.16/0.57 op1(e10,e10)=e10),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.57 fof(f59,plain,(
% 0.16/0.57 op1(e11,e11)=e12),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.57 fof(f61,plain,(
% 0.16/0.57 op1(e11,e13)=e14),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.57 fof(f63,plain,(
% 0.16/0.57 op1(e12,e10)=e12),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.57 fof(f64,plain,(
% 0.16/0.57 op1(e12,e11)=e14),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.57 fof(f65,plain,(
% 0.16/0.57 op1(e12,e12)=e11),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.57 fof(f66,plain,(
% 0.16/0.57 op1(e12,e13)=e10),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.57 fof(f67,plain,(
% 0.16/0.57 op1(e12,e14)=e13),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.57 fof(f70,plain,(
% 0.16/0.57 op1(e13,e12)=e14),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.57 fof(f71,plain,(
% 0.16/0.57 op1(e13,e13)=e11),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.57 fof(f72,plain,(
% 0.16/0.57 op1(e13,e14)=e12),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.57 fof(f78,plain,(
% 0.16/0.57 op2(e20,e20)=e20),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/0.57 fof(f81,plain,(
% 0.16/0.57 op2(e20,e23)=e23),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/0.57 fof(f84,plain,(
% 0.16/0.57 op2(e21,e21)=e22),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/0.57 fof(f86,plain,(
% 0.16/0.57 op2(e21,e23)=e20),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/0.57 fof(f90,plain,(
% 0.16/0.57 op2(e22,e22)=e23),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/0.57 fof(f92,plain,(
% 0.16/0.57 op2(e22,e24)=e21),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/0.57 fof(f96,plain,(
% 0.16/0.57 op2(e23,e23)=e21),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/0.57 fof(f98,plain,(
% 0.16/0.57 op2(e24,e20)=e24),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/0.57 fof(f102,plain,(
% 0.16/0.57 op2(e24,e24)=e20),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/0.57 fof(f103,plain,(
% 0.16/0.57 ((((((((((((((h(e10)=e20|h(e10)=e21)|h(e10)=e22)|h(e10)=e23)|h(e10)=e24)&((((h(e11)=e20|h(e11)=e21)|h(e11)=e22)|h(e11)=e23)|h(e11)=e24))&((((h(e12)=e20|h(e12)=e21)|h(e12)=e22)|h(e12)=e23)|h(e12)=e24))&((((h(e13)=e20|h(e13)=e21)|h(e13)=e22)|h(e13)=e23)|h(e13)=e24))&((((h(e14)=e20|h(e14)=e21)|h(e14)=e22)|h(e14)=e23)|h(e14)=e24))&((((j(e20)=e10|j(e20)=e11)|j(e20)=e12)|j(e20)=e13)|j(e20)=e14))&((((j(e21)=e10|j(e21)=e11)|j(e21)=e12)|j(e21)=e13)|j(e21)=e14))&((((j(e22)=e10|j(e22)=e11)|j(e22)=e12)|j(e22)=e13)|j(e22)=e14))&((((j(e23)=e10|j(e23)=e11)|j(e23)=e12)|j(e23)=e13)|j(e23)=e14))&((((j(e24)=e10|j(e24)=e11)|j(e24)=e12)|j(e24)=e13)|j(e24)=e14))&(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((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(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(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(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(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)))&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(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(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(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(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)))&h(j(e20))=e20)&h(j(e21))=e21)&h(j(e22))=e22)&h(j(e23))=e23)&h(j(e24))=e24)&j(h(e10))=e10)&j(h(e11))=e11)&j(h(e12))=e12)&j(h(e13))=e13)&j(h(e14))=e14))),
% 0.16/0.57 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.16/0.57 fof(f104,plain,(
% 0.16/0.57 h(e10)=e20|h(e10)=e21|h(e10)=e22|h(e10)=e23|h(e10)=e24),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f105,plain,(
% 0.16/0.57 h(e11)=e20|h(e11)=e21|h(e11)=e22|h(e11)=e23|h(e11)=e24),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f107,plain,(
% 0.16/0.57 h(e13)=e20|h(e13)=e21|h(e13)=e22|h(e13)=e23|h(e13)=e24),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f109,plain,(
% 0.16/0.57 j(e20)=e10|j(e20)=e11|j(e20)=e12|j(e20)=e13|j(e20)=e14),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f113,plain,(
% 0.16/0.57 j(e24)=e10|j(e24)=e11|j(e24)=e12|j(e24)=e13|j(e24)=e14),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f120,plain,(
% 0.16/0.57 h(op1(e11,e11))=op2(h(e11),h(e11))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f122,plain,(
% 0.16/0.57 h(op1(e11,e13))=op2(h(e11),h(e13))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f124,plain,(
% 0.16/0.57 h(op1(e12,e10))=op2(h(e12),h(e10))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f126,plain,(
% 0.16/0.57 h(op1(e12,e12))=op2(h(e12),h(e12))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f127,plain,(
% 0.16/0.57 h(op1(e12,e13))=op2(h(e12),h(e13))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f128,plain,(
% 0.16/0.57 h(op1(e12,e14))=op2(h(e12),h(e14))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f131,plain,(
% 0.16/0.57 h(op1(e13,e12))=op2(h(e13),h(e12))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f132,plain,(
% 0.16/0.57 h(op1(e13,e13))=op2(h(e13),h(e13))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f133,plain,(
% 0.16/0.57 h(op1(e13,e14))=op2(h(e13),h(e14))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f139,plain,(
% 0.16/0.57 j(op2(e20,e20))=op1(j(e20),j(e20))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f145,plain,(
% 0.16/0.57 j(op2(e21,e21))=op1(j(e21),j(e21))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f157,plain,(
% 0.16/0.57 j(op2(e23,e23))=op1(j(e23),j(e23))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f159,plain,(
% 0.16/0.57 j(op2(e24,e20))=op1(j(e24),j(e20))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f163,plain,(
% 0.16/0.57 j(op2(e24,e24))=op1(j(e24),j(e24))),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f164,plain,(
% 0.16/0.57 h(j(e20))=e20),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f165,plain,(
% 0.16/0.57 h(j(e21))=e21),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f166,plain,(
% 0.16/0.57 h(j(e22))=e22),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f167,plain,(
% 0.16/0.57 h(j(e23))=e23),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f168,plain,(
% 0.16/0.57 h(j(e24))=e24),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f169,plain,(
% 0.16/0.57 j(h(e10))=e10),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f170,plain,(
% 0.16/0.57 j(h(e11))=e11),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f171,plain,(
% 0.16/0.57 j(h(e12))=e12),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f172,plain,(
% 0.16/0.57 j(h(e13))=e13),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f173,plain,(
% 0.16/0.57 j(h(e14))=e14),
% 0.16/0.57 inference(cnf_transformation,[status(thm)],[f103])).
% 0.16/0.57 fof(f174,definition,(
% 0.16/0.57 sQ0_spl <=> (h(e10)=e20)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f175,plain,(
% 0.16/0.57 h(e10)=e20|~sQ0_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f174])).
% 0.16/0.57 fof(f177,definition,(
% 0.16/0.57 sQ1_spl <=> (h(e10)=e21)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f178,plain,(
% 0.16/0.57 h(e10)=e21|~sQ1_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f177])).
% 0.16/0.57 fof(f180,definition,(
% 0.16/0.57 sQ2_spl <=> (h(e10)=e22)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f181,plain,(
% 0.16/0.57 h(e10)=e22|~sQ2_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f180])).
% 0.16/0.57 fof(f183,definition,(
% 0.16/0.57 sQ3_spl <=> (h(e10)=e23)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f184,plain,(
% 0.16/0.57 h(e10)=e23|~sQ3_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f183])).
% 0.16/0.57 fof(f186,definition,(
% 0.16/0.57 sQ4_spl <=> (h(e10)=e24)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f187,plain,(
% 0.16/0.57 h(e10)=e24|~sQ4_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f186])).
% 0.16/0.57 fof(f189,plain,(
% 0.16/0.57 sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl|sQ4_spl),
% 0.16/0.57 inference(split_clause,[status(thm)],[f104,f174,f177,f180,f183,f186])).
% 0.16/0.57 fof(f190,definition,(
% 0.16/0.57 sQ5_spl <=> (h(e11)=e20)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f191,plain,(
% 0.16/0.57 h(e11)=e20|~sQ5_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f190])).
% 0.16/0.57 fof(f193,definition,(
% 0.16/0.57 sQ6_spl <=> (h(e11)=e21)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f194,plain,(
% 0.16/0.57 h(e11)=e21|~sQ6_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f193])).
% 0.16/0.57 fof(f196,definition,(
% 0.16/0.57 sQ7_spl <=> (h(e11)=e22)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f197,plain,(
% 0.16/0.57 h(e11)=e22|~sQ7_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f196])).
% 0.16/0.57 fof(f199,definition,(
% 0.16/0.57 sQ8_spl <=> (h(e11)=e23)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f200,plain,(
% 0.16/0.57 h(e11)=e23|~sQ8_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f199])).
% 0.16/0.57 fof(f202,definition,(
% 0.16/0.57 sQ9_spl <=> (h(e11)=e24)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f203,plain,(
% 0.16/0.57 h(e11)=e24|~sQ9_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f202])).
% 0.16/0.57 fof(f205,plain,(
% 0.16/0.57 sQ5_spl|sQ6_spl|sQ7_spl|sQ8_spl|sQ9_spl),
% 0.16/0.57 inference(split_clause,[status(thm)],[f105,f190,f193,f196,f199,f202])).
% 0.16/0.57 fof(f206,definition,(
% 0.16/0.57 sQ10_spl <=> (h(e12)=e20)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f207,plain,(
% 0.16/0.57 h(e12)=e20|~sQ10_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f206])).
% 0.16/0.57 fof(f208,plain,(
% 0.16/0.57 ~h(e12)=e20|sQ10_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f206])).
% 0.16/0.57 fof(f209,definition,(
% 0.16/0.57 sQ11_spl <=> (h(e12)=e21)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f210,plain,(
% 0.16/0.57 h(e12)=e21|~sQ11_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f209])).
% 0.16/0.57 fof(f212,definition,(
% 0.16/0.57 sQ12_spl <=> (h(e12)=e22)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f213,plain,(
% 0.16/0.57 h(e12)=e22|~sQ12_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f212])).
% 0.16/0.57 fof(f214,plain,(
% 0.16/0.57 ~h(e12)=e22|sQ12_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f212])).
% 0.16/0.57 fof(f215,definition,(
% 0.16/0.57 sQ13_spl <=> (h(e12)=e23)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f216,plain,(
% 0.16/0.57 h(e12)=e23|~sQ13_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f215])).
% 0.16/0.57 fof(f217,plain,(
% 0.16/0.57 ~h(e12)=e23|sQ13_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f215])).
% 0.16/0.57 fof(f222,definition,(
% 0.16/0.57 sQ15_spl <=> (h(e13)=e20)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f223,plain,(
% 0.16/0.57 h(e13)=e20|~sQ15_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f222])).
% 0.16/0.57 fof(f225,definition,(
% 0.16/0.57 sQ16_spl <=> (h(e13)=e21)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f228,definition,(
% 0.16/0.57 sQ17_spl <=> (h(e13)=e22)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f229,plain,(
% 0.16/0.57 h(e13)=e22|~sQ17_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f228])).
% 0.16/0.57 fof(f231,definition,(
% 0.16/0.57 sQ18_spl <=> (h(e13)=e23)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f232,plain,(
% 0.16/0.57 h(e13)=e23|~sQ18_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f231])).
% 0.16/0.57 fof(f234,definition,(
% 0.16/0.57 sQ19_spl <=> (h(e13)=e24)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f235,plain,(
% 0.16/0.57 h(e13)=e24|~sQ19_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f234])).
% 0.16/0.57 fof(f237,plain,(
% 0.16/0.57 sQ15_spl|sQ16_spl|sQ17_spl|sQ18_spl|sQ19_spl),
% 0.16/0.57 inference(split_clause,[status(thm)],[f107,f222,f225,f228,f231,f234])).
% 0.16/0.57 fof(f238,definition,(
% 0.16/0.57 sQ20_spl <=> (h(e14)=e20)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f239,plain,(
% 0.16/0.57 h(e14)=e20|~sQ20_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f238])).
% 0.16/0.57 fof(f240,plain,(
% 0.16/0.57 ~h(e14)=e20|sQ20_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f238])).
% 0.16/0.57 fof(f241,definition,(
% 0.16/0.57 sQ21_spl <=> (h(e14)=e21)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f242,plain,(
% 0.16/0.57 h(e14)=e21|~sQ21_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f241])).
% 0.16/0.57 fof(f244,definition,(
% 0.16/0.57 sQ22_spl <=> (h(e14)=e22)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f245,plain,(
% 0.16/0.57 h(e14)=e22|~sQ22_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f244])).
% 0.16/0.57 fof(f247,definition,(
% 0.16/0.57 sQ23_spl <=> (h(e14)=e23)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f248,plain,(
% 0.16/0.57 h(e14)=e23|~sQ23_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f247])).
% 0.16/0.57 fof(f249,plain,(
% 0.16/0.57 ~h(e14)=e23|sQ23_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f247])).
% 0.16/0.57 fof(f250,definition,(
% 0.16/0.57 sQ24_spl <=> (h(e14)=e24)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f251,plain,(
% 0.16/0.57 h(e14)=e24|~sQ24_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f250])).
% 0.16/0.57 fof(f254,definition,(
% 0.16/0.57 sQ25_spl <=> (j(e20)=e10)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f255,plain,(
% 0.16/0.57 j(e20)=e10|~sQ25_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f254])).
% 0.16/0.57 fof(f257,definition,(
% 0.16/0.57 sQ26_spl <=> (j(e20)=e11)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f258,plain,(
% 0.16/0.57 j(e20)=e11|~sQ26_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f257])).
% 0.16/0.57 fof(f259,plain,(
% 0.16/0.57 ~j(e20)=e11|sQ26_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f257])).
% 0.16/0.57 fof(f260,definition,(
% 0.16/0.57 sQ27_spl <=> (j(e20)=e12)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f261,plain,(
% 0.16/0.57 j(e20)=e12|~sQ27_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f260])).
% 0.16/0.57 fof(f262,plain,(
% 0.16/0.57 ~j(e20)=e12|sQ27_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f260])).
% 0.16/0.57 fof(f263,definition,(
% 0.16/0.57 sQ28_spl <=> (j(e20)=e13)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f264,plain,(
% 0.16/0.57 j(e20)=e13|~sQ28_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f263])).
% 0.16/0.57 fof(f266,definition,(
% 0.16/0.57 sQ29_spl <=> (j(e20)=e14)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f267,plain,(
% 0.16/0.57 j(e20)=e14|~sQ29_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f266])).
% 0.16/0.57 fof(f269,plain,(
% 0.16/0.57 sQ25_spl|sQ26_spl|sQ27_spl|sQ28_spl|sQ29_spl),
% 0.16/0.57 inference(split_clause,[status(thm)],[f109,f254,f257,f260,f263,f266])).
% 0.16/0.57 fof(f270,definition,(
% 0.16/0.57 sQ30_spl <=> (j(e21)=e10)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f271,plain,(
% 0.16/0.57 j(e21)=e10|~sQ30_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f270])).
% 0.16/0.57 fof(f276,definition,(
% 0.16/0.57 sQ32_spl <=> (j(e21)=e12)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f277,plain,(
% 0.16/0.57 j(e21)=e12|~sQ32_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f276])).
% 0.16/0.57 fof(f286,definition,(
% 0.16/0.57 sQ35_spl <=> (j(e22)=e10)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f287,plain,(
% 0.16/0.57 j(e22)=e10|~sQ35_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f286])).
% 0.16/0.57 fof(f289,definition,(
% 0.16/0.57 sQ36_spl <=> (j(e22)=e11)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f290,plain,(
% 0.16/0.57 j(e22)=e11|~sQ36_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f289])).
% 0.16/0.57 fof(f295,definition,(
% 0.16/0.57 sQ38_spl <=> (j(e22)=e13)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f296,plain,(
% 0.16/0.57 j(e22)=e13|~sQ38_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f295])).
% 0.16/0.57 fof(f298,definition,(
% 0.16/0.57 sQ39_spl <=> (j(e22)=e14)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f299,plain,(
% 0.16/0.57 j(e22)=e14|~sQ39_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f298])).
% 0.16/0.57 fof(f302,definition,(
% 0.16/0.57 sQ40_spl <=> (j(e23)=e10)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f303,plain,(
% 0.16/0.57 j(e23)=e10|~sQ40_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f302])).
% 0.16/0.57 fof(f305,definition,(
% 0.16/0.57 sQ41_spl <=> (j(e23)=e11)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f306,plain,(
% 0.16/0.57 j(e23)=e11|~sQ41_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f305])).
% 0.16/0.57 fof(f308,definition,(
% 0.16/0.57 sQ42_spl <=> (j(e23)=e12)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f309,plain,(
% 0.16/0.57 j(e23)=e12|~sQ42_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f308])).
% 0.16/0.57 fof(f311,definition,(
% 0.16/0.57 sQ43_spl <=> (j(e23)=e13)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f312,plain,(
% 0.16/0.57 j(e23)=e13|~sQ43_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f311])).
% 0.16/0.57 fof(f314,definition,(
% 0.16/0.57 sQ44_spl <=> (j(e23)=e14)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f315,plain,(
% 0.16/0.57 j(e23)=e14|~sQ44_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f314])).
% 0.16/0.57 fof(f318,definition,(
% 0.16/0.57 sQ45_spl <=> (j(e24)=e10)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f319,plain,(
% 0.16/0.57 j(e24)=e10|~sQ45_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f318])).
% 0.16/0.57 fof(f321,definition,(
% 0.16/0.57 sQ46_spl <=> (j(e24)=e11)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f322,plain,(
% 0.16/0.57 j(e24)=e11|~sQ46_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f321])).
% 0.16/0.57 fof(f324,definition,(
% 0.16/0.57 sQ47_spl <=> (j(e24)=e12)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f325,plain,(
% 0.16/0.57 j(e24)=e12|~sQ47_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f324])).
% 0.16/0.57 fof(f327,definition,(
% 0.16/0.57 sQ48_spl <=> (j(e24)=e13)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f328,plain,(
% 0.16/0.57 j(e24)=e13|~sQ48_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f327])).
% 0.16/0.57 fof(f330,definition,(
% 0.16/0.57 sQ49_spl <=> (j(e24)=e14)),
% 0.16/0.57 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.16/0.57 fof(f331,plain,(
% 0.16/0.57 j(e24)=e14|~sQ49_spl),
% 0.16/0.57 inference(component_clause,[status(thm)],[f330])).
% 0.16/0.57 fof(f333,plain,(
% 0.16/0.57 sQ45_spl|sQ46_spl|sQ47_spl|sQ48_spl|sQ49_spl),
% 0.16/0.57 inference(split_clause,[status(thm)],[f113,f318,f321,f324,f327,f330])).
% 0.16/0.57 fof(f334,plain,(
% 0.16/0.57 e13=e14|~sQ48_spl|~sQ49_spl),
% 0.16/0.57 inference(backward_demodulation,[status(thm)],[f328,f331])).
% 0.16/0.57 fof(f335,plain,(
% 0.16/0.57 $false|~sQ48_spl|~sQ49_spl),
% 0.16/0.57 inference(forward_subsumption_resolution,[status(thm)],[f334,f17])).
% 0.16/0.57 fof(f336,plain,(
% 0.16/0.57 ~sQ48_spl|~sQ49_spl),
% 0.16/0.57 inference(contradiction_clause,[status(thm)],[f335])).
% 0.16/0.57 fof(f340,plain,(
% 0.16/0.57 e13=e14|~sQ43_spl|~sQ44_spl),
% 0.16/0.57 inference(backward_demodulation,[status(thm)],[f312,f315])).
% 0.16/0.57 fof(f341,plain,(
% 0.16/0.57 $false|~sQ43_spl|~sQ44_spl),
% 0.16/0.57 inference(forward_subsumption_resolution,[status(thm)],[f340,f17])).
% 0.16/0.57 fof(f342,plain,(
% 0.16/0.57 ~sQ43_spl|~sQ44_spl),
% 0.16/0.57 inference(contradiction_clause,[status(thm)],[f341])).
% 0.16/0.57 fof(f346,plain,(
% 0.16/0.57 e11=e12|~sQ41_spl|~sQ42_spl),
% 0.16/0.57 inference(backward_demodulation,[status(thm)],[f306,f309])).
% 0.16/0.57 fof(f347,plain,(
% 0.16/0.57 $false|~sQ41_spl|~sQ42_spl),
% 0.16/0.57 inference(forward_subsumption_resolution,[status(thm)],[f346,f12])).
% 0.16/0.59 fof(f348,plain,(
% 0.16/0.59 ~sQ41_spl|~sQ42_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f347])).
% 0.16/0.59 fof(f351,plain,(
% 0.16/0.59 e13=e14|~sQ38_spl|~sQ39_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f296,f299])).
% 0.16/0.59 fof(f352,plain,(
% 0.16/0.59 $false|~sQ38_spl|~sQ39_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f351,f17])).
% 0.16/0.59 fof(f353,plain,(
% 0.16/0.59 ~sQ38_spl|~sQ39_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f352])).
% 0.16/0.59 fof(f358,plain,(
% 0.16/0.59 h(e12)=op2(h(e11),h(e11))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f59,f120])).
% 0.16/0.59 fof(f366,plain,(
% 0.16/0.59 e13=e14|~sQ28_spl|~sQ29_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f264,f267])).
% 0.16/0.59 fof(f367,plain,(
% 0.16/0.59 $false|~sQ28_spl|~sQ29_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f366,f17])).
% 0.16/0.59 fof(f368,plain,(
% 0.16/0.59 ~sQ28_spl|~sQ29_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f367])).
% 0.16/0.59 fof(f372,plain,(
% 0.16/0.59 h(e14)=op2(h(e11),h(e13))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f61,f122])).
% 0.16/0.59 fof(f374,plain,(
% 0.16/0.59 e23=e24|~sQ23_spl|~sQ24_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f248,f251])).
% 0.16/0.59 fof(f375,plain,(
% 0.16/0.59 $false|~sQ23_spl|~sQ24_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f374,f27])).
% 0.16/0.59 fof(f376,plain,(
% 0.16/0.59 ~sQ23_spl|~sQ24_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f375])).
% 0.16/0.59 fof(f377,plain,(
% 0.16/0.59 e21=e22|~sQ21_spl|~sQ22_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f242,f245])).
% 0.16/0.59 fof(f378,plain,(
% 0.16/0.59 $false|~sQ21_spl|~sQ22_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f377,f22])).
% 0.16/0.59 fof(f379,plain,(
% 0.16/0.59 ~sQ21_spl|~sQ22_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f378])).
% 0.16/0.59 fof(f381,plain,(
% 0.16/0.59 e23=e24|~sQ18_spl|~sQ19_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f232,f235])).
% 0.16/0.59 fof(f382,plain,(
% 0.16/0.59 $false|~sQ18_spl|~sQ19_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f381,f27])).
% 0.16/0.59 fof(f383,plain,(
% 0.16/0.59 ~sQ18_spl|~sQ19_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f382])).
% 0.16/0.59 fof(f393,plain,(
% 0.16/0.59 h(e12)=op2(h(e12),h(e10))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f63,f124])).
% 0.16/0.59 fof(f394,plain,(
% 0.16/0.59 e22=op2(h(e12),h(e10))|~sQ12_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f213,f393])).
% 0.16/0.59 fof(f395,plain,(
% 0.16/0.59 e22=op2(e22,h(e10))|~sQ12_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f213,f394])).
% 0.16/0.59 fof(f396,plain,(
% 0.16/0.59 e21=e22|~sQ11_spl|~sQ12_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f210,f213])).
% 0.16/0.59 fof(f397,plain,(
% 0.16/0.59 $false|~sQ11_spl|~sQ12_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f396,f22])).
% 0.16/0.59 fof(f398,plain,(
% 0.16/0.59 ~sQ11_spl|~sQ12_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f397])).
% 0.16/0.59 fof(f403,plain,(
% 0.16/0.59 e21=e22|~sQ6_spl|~sQ7_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f194,f197])).
% 0.16/0.59 fof(f404,plain,(
% 0.16/0.59 $false|~sQ6_spl|~sQ7_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f403,f22])).
% 0.16/0.59 fof(f405,plain,(
% 0.16/0.59 ~sQ6_spl|~sQ7_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f404])).
% 0.16/0.59 fof(f414,plain,(
% 0.16/0.59 h(e11)=op2(h(e12),h(e12))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f65,f126])).
% 0.16/0.59 fof(f424,plain,(
% 0.16/0.59 h(e10)=op2(h(e12),h(e13))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f66,f127])).
% 0.16/0.59 fof(f435,plain,(
% 0.16/0.59 h(e13)=op2(h(e12),h(e14))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f67,f128])).
% 0.16/0.59 fof(f436,plain,(
% 0.16/0.59 h(e13)=op2(e20,h(e14))|~sQ10_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f207,f435])).
% 0.16/0.59 fof(f437,plain,(
% 0.16/0.59 h(e13)=op2(e20,e20)|~sQ20_spl|~sQ10_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f239,f436])).
% 0.16/0.59 fof(f440,plain,(
% 0.16/0.59 h(e13)=e20|~sQ20_spl|~sQ10_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f78,f437])).
% 0.16/0.59 fof(f446,plain,(
% 0.16/0.59 e23=op2(h(e12),h(e13))|~sQ3_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f184,f424])).
% 0.16/0.59 fof(f447,plain,(
% 0.16/0.59 e23=op2(e20,h(e13))|~sQ10_spl|~sQ3_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f207,f446])).
% 0.16/0.59 fof(f448,plain,(
% 0.16/0.59 e23=op2(e20,e20)|~sQ20_spl|~sQ10_spl|~sQ3_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f440,f447])).
% 0.16/0.59 fof(f449,plain,(
% 0.16/0.59 e23=e20|~sQ20_spl|~sQ10_spl|~sQ3_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f78,f448])).
% 0.16/0.59 fof(f450,plain,(
% 0.16/0.59 $false|~sQ20_spl|~sQ10_spl|~sQ3_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f449,f20])).
% 0.16/0.59 fof(f451,plain,(
% 0.16/0.59 ~sQ20_spl|~sQ10_spl|~sQ3_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f450])).
% 0.16/0.59 fof(f460,plain,(
% 0.16/0.59 h(e14)=op2(h(e13),h(e12))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f70,f131])).
% 0.16/0.59 fof(f464,plain,(
% 0.16/0.59 h(e11)=op2(h(e13),h(e13))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f71,f132])).
% 0.16/0.59 fof(f470,plain,(
% 0.16/0.59 h(e12)=op2(h(e13),h(e14))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f72,f133])).
% 0.16/0.59 fof(f471,plain,(
% 0.16/0.59 h(e12)=op2(e20,h(e14))|~sQ15_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f223,f470])).
% 0.16/0.59 fof(f472,plain,(
% 0.16/0.59 h(e12)=op2(e20,e20)|~sQ20_spl|~sQ15_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f239,f471])).
% 0.16/0.59 fof(f473,plain,(
% 0.16/0.59 h(e12)=e20|~sQ20_spl|~sQ15_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f78,f472])).
% 0.16/0.59 fof(f499,plain,(
% 0.16/0.59 ~e20=e20|~sQ20_spl|~sQ15_spl|sQ10_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f473,f208])).
% 0.16/0.59 fof(f500,plain,(
% 0.16/0.59 $false|~sQ20_spl|~sQ15_spl|sQ10_spl),
% 0.16/0.59 inference(trivial_equality_resolution,[status(thm)],[f499])).
% 0.16/0.59 fof(f501,plain,(
% 0.16/0.59 ~sQ20_spl|~sQ15_spl|sQ10_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f500])).
% 0.16/0.59 fof(f507,plain,(
% 0.16/0.59 j(e20)=op1(j(e20),j(e20))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f78,f139])).
% 0.16/0.59 fof(f532,plain,(
% 0.16/0.59 j(e22)=op1(j(e21),j(e21))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f84,f145])).
% 0.16/0.59 fof(f572,plain,(
% 0.16/0.59 h(e10)=e20|~sQ25_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f255,f164])).
% 0.16/0.59 fof(f573,plain,(
% 0.16/0.59 h(e10)=e21|~sQ30_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f271,f165])).
% 0.16/0.59 fof(f574,plain,(
% 0.16/0.59 e20=e21|~sQ0_spl|~sQ30_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f175,f573])).
% 0.16/0.59 fof(f575,plain,(
% 0.16/0.59 $false|~sQ0_spl|~sQ30_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f574,f18])).
% 0.16/0.59 fof(f576,plain,(
% 0.16/0.59 ~sQ0_spl|~sQ30_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f575])).
% 0.16/0.59 fof(f581,plain,(
% 0.16/0.59 sQ1_spl|~sQ30_spl),
% 0.16/0.59 inference(split_clause,[status(thm)],[f573,f177,f270])).
% 0.16/0.59 fof(f582,plain,(
% 0.16/0.59 sQ0_spl|~sQ25_spl),
% 0.16/0.59 inference(split_clause,[status(thm)],[f572,f174,f254])).
% 0.16/0.59 fof(f616,plain,(
% 0.16/0.59 j(e21)=op1(j(e23),j(e23))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f96,f157])).
% 0.16/0.59 fof(f624,plain,(
% 0.16/0.59 j(e24)=op1(j(e24),j(e20))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f98,f159])).
% 0.16/0.59 fof(f643,plain,(
% 0.16/0.59 j(e20)=op1(j(e24),j(e24))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f102,f163])).
% 0.16/0.59 fof(f690,plain,(
% 0.16/0.59 j(e21)=op1(e10,j(e23))|~sQ40_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f303,f616])).
% 0.16/0.59 fof(f691,plain,(
% 0.16/0.59 j(e21)=op1(e10,e10)|~sQ40_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f303,f690])).
% 0.16/0.59 fof(f692,plain,(
% 0.16/0.59 j(e21)=e10|~sQ40_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f53,f691])).
% 0.16/0.59 fof(f696,plain,(
% 0.16/0.59 h(e10)=e24|~sQ45_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f319,f168])).
% 0.16/0.59 fof(f700,plain,(
% 0.16/0.59 sQ4_spl|~sQ45_spl),
% 0.16/0.59 inference(split_clause,[status(thm)],[f696,f186,f318])).
% 0.16/0.59 fof(f709,plain,(
% 0.16/0.59 sQ30_spl|~sQ40_spl),
% 0.16/0.59 inference(split_clause,[status(thm)],[f692,f270,f302])).
% 0.16/0.59 fof(f711,plain,(
% 0.16/0.59 j(e20)=e11|~sQ5_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f191,f170])).
% 0.16/0.59 fof(f726,plain,(
% 0.16/0.59 ~e11=e11|~sQ5_spl|sQ26_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f711,f259])).
% 0.16/0.59 fof(f727,plain,(
% 0.16/0.59 $false|~sQ5_spl|sQ26_spl),
% 0.16/0.59 inference(trivial_equality_resolution,[status(thm)],[f726])).
% 0.16/0.59 fof(f728,plain,(
% 0.16/0.59 ~sQ5_spl|sQ26_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f727])).
% 0.16/0.59 fof(f733,plain,(
% 0.16/0.59 j(e22)=e10|~sQ2_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f181,f169])).
% 0.16/0.59 fof(f736,plain,(
% 0.16/0.59 sQ35_spl|~sQ2_spl),
% 0.16/0.59 inference(split_clause,[status(thm)],[f733,f286,f180])).
% 0.16/0.59 fof(f761,plain,(
% 0.16/0.59 j(e22)=e13|~sQ17_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f229,f172])).
% 0.16/0.59 fof(f764,plain,(
% 0.16/0.59 sQ38_spl|~sQ17_spl),
% 0.16/0.59 inference(split_clause,[status(thm)],[f761,f295,f228])).
% 0.16/0.59 fof(f772,plain,(
% 0.16/0.59 j(e21)=e12|~sQ11_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f210,f171])).
% 0.16/0.59 fof(f774,plain,(
% 0.16/0.59 sQ32_spl|~sQ11_spl),
% 0.16/0.59 inference(split_clause,[status(thm)],[f772,f276,f209])).
% 0.16/0.59 fof(f777,plain,(
% 0.16/0.59 j(e21)=op1(e12,j(e23))|~sQ42_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f309,f616])).
% 0.16/0.59 fof(f778,plain,(
% 0.16/0.59 j(e21)=op1(e12,e12)|~sQ42_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f309,f777])).
% 0.16/0.59 fof(f785,plain,(
% 0.16/0.59 h(e11)=e21|~sQ42_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f786,f165])).
% 0.16/0.59 fof(f786,plain,(
% 0.16/0.59 j(e21)=e11|~sQ42_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f65,f778])).
% 0.16/0.59 fof(f791,plain,(
% 0.16/0.59 sQ6_spl|~sQ42_spl),
% 0.16/0.59 inference(split_clause,[status(thm)],[f785,f193,f308])).
% 0.16/0.59 fof(f809,plain,(
% 0.16/0.59 j(e20)=op1(j(e20),e12)|~sQ27_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f261,f507])).
% 0.16/0.59 fof(f812,plain,(
% 0.16/0.59 e12=op1(j(e20),e12)|~sQ27_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f261,f809])).
% 0.16/0.59 fof(f813,plain,(
% 0.16/0.59 e12=op1(e12,e12)|~sQ27_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f261,f812])).
% 0.16/0.59 fof(f814,plain,(
% 0.16/0.59 e12=e11|~sQ27_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f65,f813])).
% 0.16/0.59 fof(f815,plain,(
% 0.16/0.59 $false|~sQ27_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f814,f12])).
% 0.16/0.59 fof(f816,plain,(
% 0.16/0.59 ~sQ27_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f815])).
% 0.16/0.59 fof(f843,plain,(
% 0.16/0.59 j(e20)=op1(e12,j(e24))|~sQ47_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f325,f643])).
% 0.16/0.59 fof(f844,plain,(
% 0.16/0.59 j(e20)=op1(e12,e12)|~sQ47_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f325,f843])).
% 0.16/0.59 fof(f845,plain,(
% 0.16/0.59 j(e20)=e11|~sQ47_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f65,f844])).
% 0.16/0.59 fof(f846,plain,(
% 0.16/0.59 e12=op1(j(e24),j(e20))|~sQ47_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f325,f624])).
% 0.16/0.59 fof(f847,plain,(
% 0.16/0.59 e12=op1(e12,j(e20))|~sQ47_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f325,f846])).
% 0.16/0.59 fof(f848,plain,(
% 0.16/0.59 e12=e14|~sQ47_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f849,f64])).
% 0.16/0.59 fof(f849,plain,(
% 0.16/0.59 e12=op1(e12,e11)|~sQ47_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f845,f847])).
% 0.16/0.59 fof(f850,plain,(
% 0.16/0.59 $false|~sQ47_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f848,f16])).
% 0.16/0.59 fof(f851,plain,(
% 0.16/0.59 ~sQ47_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f850])).
% 0.16/0.59 fof(f865,plain,(
% 0.16/0.59 j(e22)=e14|~sQ22_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f245,f173])).
% 0.16/0.59 fof(f866,plain,(
% 0.16/0.59 e10=e14|~sQ35_spl|~sQ22_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f287,f865])).
% 0.16/0.59 fof(f867,plain,(
% 0.16/0.59 $false|~sQ35_spl|~sQ22_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f866,f11])).
% 0.16/0.59 fof(f868,plain,(
% 0.16/0.59 ~sQ35_spl|~sQ22_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f867])).
% 0.16/0.59 fof(f877,plain,(
% 0.16/0.59 sQ15_spl|~sQ20_spl|~sQ10_spl),
% 0.16/0.59 inference(split_clause,[status(thm)],[f440,f222,f238,f206])).
% 0.16/0.59 fof(f910,plain,(
% 0.16/0.59 h(e12)=op2(e22,h(e11))|~sQ7_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f197,f358])).
% 0.16/0.59 fof(f911,plain,(
% 0.16/0.59 h(e12)=op2(e22,e22)|~sQ7_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f197,f910])).
% 0.16/0.59 fof(f912,plain,(
% 0.16/0.59 h(e12)=e23|~sQ7_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f90,f911])).
% 0.16/0.59 fof(f913,plain,(
% 0.16/0.59 $false|sQ13_spl|~sQ7_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f912,f217])).
% 0.16/0.59 fof(f914,plain,(
% 0.16/0.59 sQ13_spl|~sQ7_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f913])).
% 0.16/0.59 fof(f918,plain,(
% 0.16/0.59 j(e22)=op1(e12,j(e21))|~sQ32_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f277,f532])).
% 0.16/0.59 fof(f919,plain,(
% 0.16/0.59 j(e22)=op1(e12,e12)|~sQ32_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f277,f918])).
% 0.16/0.59 fof(f920,plain,(
% 0.16/0.59 j(e22)=e11|~sQ32_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f65,f919])).
% 0.16/0.59 fof(f938,plain,(
% 0.16/0.59 j(e21)=op1(e11,j(e23))|~sQ41_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f306,f616])).
% 0.16/0.59 fof(f939,plain,(
% 0.16/0.59 j(e21)=op1(e11,e11)|~sQ41_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f306,f938])).
% 0.16/0.59 fof(f940,plain,(
% 0.16/0.59 h(e12)=e21|~sQ41_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f943,f165])).
% 0.16/0.59 fof(f943,plain,(
% 0.16/0.59 j(e21)=e12|~sQ41_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f59,f939])).
% 0.16/0.59 fof(f944,plain,(
% 0.16/0.59 sQ11_spl|~sQ41_spl),
% 0.16/0.59 inference(split_clause,[status(thm)],[f940,f209,f305])).
% 0.16/0.59 fof(f955,plain,(
% 0.16/0.59 e11=op1(j(e20),j(e20))|~sQ26_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f258,f507])).
% 0.16/0.59 fof(f956,plain,(
% 0.16/0.59 e11=op1(e11,j(e20))|~sQ26_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f258,f955])).
% 0.16/0.59 fof(f957,plain,(
% 0.16/0.59 e11=e12|~sQ26_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f958,f59])).
% 0.16/0.59 fof(f958,plain,(
% 0.16/0.59 e11=op1(e11,e11)|~sQ26_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f258,f956])).
% 0.16/0.59 fof(f959,plain,(
% 0.16/0.59 $false|~sQ26_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f957,f12])).
% 0.16/0.59 fof(f960,plain,(
% 0.16/0.59 ~sQ26_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f959])).
% 0.16/0.59 fof(f963,plain,(
% 0.16/0.59 e22=op2(e22,e24)|~sQ4_spl|~sQ12_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f187,f395])).
% 0.16/0.59 fof(f964,plain,(
% 0.16/0.59 e22=e21|~sQ4_spl|~sQ12_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f92,f963])).
% 0.16/0.59 fof(f965,plain,(
% 0.16/0.59 $false|~sQ4_spl|~sQ12_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f964,f22])).
% 0.16/0.59 fof(f966,plain,(
% 0.16/0.59 ~sQ4_spl|~sQ12_spl),
% 0.16/0.59 inference(contradiction_clause,[status(thm)],[f965])).
% 0.16/0.59 fof(f983,plain,(
% 0.16/0.59 j(e20)=e13|~sQ15_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f223,f172])).
% 0.16/0.59 fof(f986,plain,(
% 0.16/0.59 h(e14)=op2(e20,h(e12))|~sQ15_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f223,f460])).
% 0.16/0.59 fof(f990,plain,(
% 0.16/0.59 j(e20)=op1(e11,j(e24))|~sQ46_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f322,f643])).
% 0.16/0.59 fof(f991,plain,(
% 0.16/0.59 j(e20)=op1(e11,e11)|~sQ46_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f322,f990])).
% 0.16/0.59 fof(f1020,plain,(
% 0.16/0.59 h(e13)=e23|~sQ43_spl),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f312,f167])).
% 0.16/0.59 fof(f1021,plain,(
% 0.16/0.59 sQ18_spl|~sQ43_spl),
% 0.16/0.59 inference(split_clause,[status(thm)],[f1020,f231,f311])).
% 0.16/0.59 fof(f1022,plain,(
% 0.16/0.59 e20=e23|~sQ15_spl|~sQ18_spl),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f223,f232])).
% 0.16/0.59 fof(f1023,plain,(
% 0.16/0.59 $false|~sQ15_spl|~sQ18_spl),
% 0.16/0.59 inference(forward_subsumption_resolution,[status(thm)],[f1022,f20])).
% 0.16/0.60 fof(f1024,plain,(
% 0.16/0.60 ~sQ15_spl|~sQ18_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f1023])).
% 0.16/0.60 fof(f1042,plain,(
% 0.16/0.60 h(e13)=e20|~sQ28_spl),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f264,f164])).
% 0.16/0.60 fof(f1043,plain,(
% 0.16/0.60 sQ15_spl|~sQ28_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1042,f222,f263])).
% 0.16/0.60 fof(f1045,plain,(
% 0.16/0.60 sQ36_spl|~sQ32_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f920,f289,f276])).
% 0.16/0.60 fof(f1048,plain,(
% 0.16/0.60 h(e12)=op2(e21,h(e11))|~sQ6_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f194,f358])).
% 0.16/0.60 fof(f1049,plain,(
% 0.16/0.60 h(e12)=op2(e21,e21)|~sQ6_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f194,f1048])).
% 0.16/0.60 fof(f1050,plain,(
% 0.16/0.60 h(e12)=e22|~sQ6_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f84,f1049])).
% 0.16/0.60 fof(f1051,plain,(
% 0.16/0.60 $false|sQ12_spl|~sQ6_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1050,f214])).
% 0.16/0.60 fof(f1052,plain,(
% 0.16/0.60 sQ12_spl|~sQ6_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f1051])).
% 0.16/0.60 fof(f1053,plain,(
% 0.16/0.60 h(e14)=op2(e21,h(e13))|~sQ6_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f194,f372])).
% 0.16/0.60 fof(f1147,plain,(
% 0.16/0.60 j(e23)=e12|~sQ13_spl),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f216,f171])).
% 0.16/0.60 fof(f1148,plain,(
% 0.16/0.60 sQ42_spl|~sQ13_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1147,f308,f215])).
% 0.16/0.60 fof(f1170,plain,(
% 0.16/0.60 sQ28_spl|~sQ15_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f983,f263,f222])).
% 0.16/0.60 fof(f1173,plain,(
% 0.16/0.60 h(e14)=op2(e20,e23)|~sQ13_spl|~sQ15_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f216,f986])).
% 0.16/0.60 fof(f1174,plain,(
% 0.16/0.60 h(e14)=e23|~sQ13_spl|~sQ15_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f81,f1173])).
% 0.16/0.60 fof(f1175,plain,(
% 0.16/0.60 $false|sQ23_spl|~sQ13_spl|~sQ15_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1174,f249])).
% 0.16/0.60 fof(f1176,plain,(
% 0.16/0.60 sQ23_spl|~sQ13_spl|~sQ15_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f1175])).
% 0.16/0.60 fof(f1199,plain,(
% 0.16/0.60 h(e13)=e23|~sQ43_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f312,f167])).
% 0.16/0.60 fof(f1249,plain,(
% 0.16/0.60 h(e11)=e22|~sQ36_spl),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f290,f166])).
% 0.16/0.60 fof(f1253,plain,(
% 0.16/0.60 sQ7_spl|~sQ36_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1249,f196,f289])).
% 0.16/0.60 fof(f1260,plain,(
% 0.16/0.60 h(e14)=op2(e21,e23)|~sQ43_spl|~sQ6_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f1199,f1053])).
% 0.16/0.60 fof(f1261,plain,(
% 0.16/0.60 h(e14)=e20|~sQ43_spl|~sQ6_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f86,f1260])).
% 0.16/0.60 fof(f1262,plain,(
% 0.16/0.60 $false|sQ20_spl|~sQ43_spl|~sQ6_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1261,f240])).
% 0.16/0.60 fof(f1263,plain,(
% 0.16/0.60 sQ20_spl|~sQ43_spl|~sQ6_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f1262])).
% 0.16/0.60 fof(f1328,plain,(
% 0.16/0.60 h(e11)=op2(h(e13),e22)|~sQ17_spl),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f229,f464])).
% 0.16/0.60 fof(f1332,plain,(
% 0.16/0.60 h(e11)=op2(e22,e22)|~sQ17_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f229,f1328])).
% 0.16/0.60 fof(f1333,plain,(
% 0.16/0.60 h(e11)=e23|~sQ17_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f90,f1332])).
% 0.16/0.60 fof(f1360,plain,(
% 0.16/0.60 h(e11)=op2(h(e12),e22)|~sQ12_spl),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f213,f414])).
% 0.16/0.60 fof(f1364,plain,(
% 0.16/0.60 h(e11)=op2(e22,e22)|~sQ12_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f213,f1360])).
% 0.16/0.60 fof(f1365,plain,(
% 0.16/0.60 h(e11)=e23|~sQ12_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f90,f1364])).
% 0.16/0.60 fof(f1382,plain,(
% 0.16/0.60 h(e10)=e23|~sQ40_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f303,f167])).
% 0.16/0.60 fof(f1383,plain,(
% 0.16/0.60 e21=e23|~sQ1_spl|~sQ40_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f178,f1382])).
% 0.16/0.60 fof(f1384,plain,(
% 0.16/0.60 $false|~sQ1_spl|~sQ40_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1383,f23])).
% 0.16/0.60 fof(f1385,plain,(
% 0.16/0.60 ~sQ1_spl|~sQ40_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f1384])).
% 0.16/0.60 fof(f1387,plain,(
% 0.16/0.60 j(e23)=e11|~sQ8_spl),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f200,f170])).
% 0.16/0.60 fof(f1388,plain,(
% 0.16/0.60 sQ41_spl|~sQ8_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1387,f305,f199])).
% 0.16/0.60 fof(f1389,plain,(
% 0.16/0.60 sQ8_spl|~sQ12_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1365,f199,f212])).
% 0.16/0.60 fof(f1390,plain,(
% 0.16/0.60 j(e20)=e12|~sQ46_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f59,f991])).
% 0.16/0.60 fof(f1391,plain,(
% 0.16/0.60 $false|sQ27_spl|~sQ46_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1390,f262])).
% 0.16/0.60 fof(f1392,plain,(
% 0.16/0.60 sQ27_spl|~sQ46_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f1391])).
% 0.16/0.60 fof(f1405,plain,(
% 0.16/0.60 sQ8_spl|~sQ17_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1333,f199,f228])).
% 0.16/0.60 fof(f1457,plain,(
% 0.16/0.60 sQ39_spl|~sQ22_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f865,f298,f244])).
% 0.16/0.60 fof(f1473,plain,(
% 0.16/0.60 h(e12)=op2(e24,h(e11))|~sQ9_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f203,f358])).
% 0.16/0.60 fof(f1474,plain,(
% 0.16/0.60 h(e12)=op2(e24,e24)|~sQ9_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f203,f1473])).
% 0.16/0.60 fof(f1475,plain,(
% 0.16/0.60 j(e20)=e12|~sQ9_spl),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f1484,f171])).
% 0.16/0.60 fof(f1484,plain,(
% 0.16/0.60 h(e12)=e20|~sQ9_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f102,f1474])).
% 0.16/0.60 fof(f1485,plain,(
% 0.16/0.60 sQ27_spl|~sQ9_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1475,f260,f202])).
% 0.16/0.60 fof(f1487,plain,(
% 0.16/0.60 $false),
% 0.16/0.60 inference(sat_refutation,[status(thm)],[f189,f205,f237,f269,f333,f336,f342,f348,f353,f368,f376,f379,f383,f398,f405,f451,f501,f576,f581,f582,f700,f709,f728,f736,f764,f774,f791,f816,f851,f868,f877,f914,f944,f960,f966,f1021,f1024,f1043,f1045,f1052,f1148,f1170,f1176,f1253,f1263,f1385,f1388,f1389,f1392,f1405,f1457,f1485])).
% 0.16/0.60 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.61 % Elapsed time: 0.176497 seconds
% 0.16/0.61 % CPU time: 1.043941 seconds
% 0.16/0.61 % Total memory used: 124.333 MB
% 0.16/0.61 % Net memory used: 123.932 MB
%------------------------------------------------------------------------------