%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG206+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 : n012.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:48 AM UTC 2026
% Result : Theorem 0.07s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG206+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 13:01:23 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.31 % Drodi V4.1.1
% 0.07/0.38 % Refutation found
% 0.07/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.07/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.07/0.38 fof(f2,axiom,(
% 0.07/0.38 ( e20 != e21& e20 != e22& e20 != e23& e20 != e24& e20 != e25& e20 != e26& e21 != e22& e21 != e23& e21 != e24& e21 != e25& e21 != e26& e22 != e23& e22 != e24& e22 != e25& e22 != e26& e23 != e24& e23 != e25& e23 != e26& e24 != e25& e24 != e26& e25 != e26 ) ),
% 0.07/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.38 fof(f4,axiom,(
% 0.07/0.38 ( op1(e10,e10) = e10& op1(e10,e11) = e13& op1(e10,e12) = e11& op1(e10,e13) = e12& op1(e10,e14) = e16& op1(e10,e15) = e14& op1(e10,e16) = e15& op1(e11,e10) = e13& op1(e11,e11) = e11& op1(e11,e12) = e16& op1(e11,e13) = e15& op1(e11,e14) = e12& op1(e11,e15) = e10& op1(e11,e16) = e14& op1(e12,e10) = e11& op1(e12,e11) = e16& op1(e12,e12) = e12& op1(e12,e13) = e14& op1(e12,e14) = e15& op1(e12,e15) = e13& op1(e12,e16) = e10& op1(e13,e10) = e12& op1(e13,e11) = e15& op1(e13,e12) = e14& op1(e13,e13) = e13& op1(e13,e14) = e10& op1(e13,e15) = e16& op1(e13,e16) = e11& op1(e14,e10) = e16& op1(e14,e11) = e12& op1(e14,e12) = e15& op1(e14,e13) = e10& op1(e14,e14) = e14& op1(e14,e15) = e11& op1(e14,e16) = e13& op1(e15,e10) = e14& op1(e15,e11) = e10& op1(e15,e12) = e13& op1(e15,e13) = e16& op1(e15,e14) = e11& op1(e15,e15) = e15& op1(e15,e16) = e12& op1(e16,e10) = e15& op1(e16,e11) = e14& op1(e16,e12) = e10& op1(e16,e13) = e11& op1(e16,e14) = e13& op1(e16,e15) = e12& op1(e16,e16) = e16 ) ),
% 0.07/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.38 fof(f5,axiom,(
% 0.07/0.38 ( op2(e20,e20) = e22& op2(e20,e21) = e20& op2(e20,e22) = e21& op2(e20,e23) = e25& op2(e20,e24) = e23& op2(e20,e25) = e24& op2(e20,e26) = e26& op2(e21,e20) = e20& op2(e21,e21) = e26& op2(e21,e22) = e24& op2(e21,e23) = e21& op2(e21,e24) = e25& op2(e21,e25) = e22& op2(e21,e26) = e23& op2(e22,e20) = e21& op2(e22,e21) = e24& op2(e22,e22) = e23& op2(e22,e23) = e26& op2(e22,e24) = e20& op2(e22,e25) = e25& op2(e22,e26) = e22& op2(e23,e20) = e25& op2(e23,e21) = e21& op2(e23,e22) = e26& op2(e23,e23) = e20& op2(e23,e24) = e22& op2(e23,e25) = e23& op2(e23,e26) = e24& op2(e24,e20) = e23& op2(e24,e21) = e25& op2(e24,e22) = e20& op2(e24,e23) = e22& op2(e24,e24) = e24& op2(e24,e25) = e26& op2(e24,e26) = e21& op2(e25,e20) = e24& op2(e25,e21) = e22& op2(e25,e22) = e25& op2(e25,e23) = e23& op2(e25,e24) = e26& op2(e25,e25) = e21& op2(e25,e26) = e20& op2(e26,e20) = e26& op2(e26,e21) = e23& op2(e26,e22) = e22& op2(e26,e23) = e24& op2(e26,e24) = e21& op2(e26,e25) = e20& op2(e26,e26) = e25 ) ),
% 0.07/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.38 fof(f6,conjecture,(
% 0.07/0.38 ( ( ( h(e10) = e20| h(e10) = e21| h(e10) = e22| h(e10) = e23| h(e10) = e24| h(e10) = e25| h(e10) = e26 )& ( h(e11) = e20| h(e11) = e21| h(e11) = e22| h(e11) = e23| h(e11) = e24| h(e11) = e25| h(e11) = e26 )& ( h(e12) = e20| h(e12) = e21| h(e12) = e22| h(e12) = e23| h(e12) = e24| h(e12) = e25| h(e12) = e26 )& ( h(e13) = e20| h(e13) = e21| h(e13) = e22| h(e13) = e23| h(e13) = e24| h(e13) = e25| h(e13) = e26 )& ( h(e14) = e20| h(e14) = e21| h(e14) = e22| h(e14) = e23| h(e14) = e24| h(e14) = e25| h(e14) = e26 )& ( h(e15) = e20| h(e15) = e21| h(e15) = e22| h(e15) = e23| h(e15) = e24| h(e15) = e25| h(e15) = e26 )& ( h(e16) = e20| h(e16) = e21| h(e16) = e22| h(e16) = e23| h(e16) = e24| h(e16) = e25| h(e16) = e26 )& ( j(e20) = e10| j(e20) = e11| j(e20) = e12| j(e20) = e13| j(e20) = e14| j(e20) = e15| j(e20) = e16 )& ( j(e21) = e10| j(e21) = e11| j(e21) = e12| j(e21) = e13| j(e21) = e14| j(e21) = e15| j(e21) = e16 )& ( j(e22) = e10| j(e22) = e11| j(e22) = e12| j(e22) = e13| j(e22) = e14| j(e22) = e15| j(e22) = e16 )& ( j(e23) = e10| j(e23) = e11| j(e23) = e12| j(e23) = e13| j(e23) = e14| j(e23) = e15| j(e23) = e16 )& ( j(e24) = e10| j(e24) = e11| j(e24) = e12| j(e24) = e13| j(e24) = e14| j(e24) = e15| j(e24) = e16 )& ( j(e25) = e10| j(e25) = e11| j(e25) = e12| j(e25) = e13| j(e25) = e14| j(e25) = e15| j(e25) = e16 )& ( j(e26) = e10| j(e26) = e11| j(e26) = e12| j(e26) = e13| j(e26) = e14| j(e26) = e15| j(e26) = e16 ) )=> ~ ( 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(e10,e16)) = op2(h(e10),h(e16))& 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(e11,e16)) = op2(h(e11),h(e16))& 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(e12,e16)) = op2(h(e12),h(e16))& 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(e13,e16)) = op2(h(e13),h(e16))& 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(e14,e16)) = op2(h(e14),h(e16))& 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))& h(op1(e15,e16)) = op2(h(e15),h(e16))& h(op1(e16,e10)) = op2(h(e16),h(e10))& h(op1(e16,e11)) = op2(h(e16),h(e11))& h(op1(e16,e12)) = op2(h(e16),h(e12))& h(op1(e16,e13)) = op2(h(e16),h(e13))& h(op1(e16,e14)) = op2(h(e16),h(e14))& h(op1(e16,e15)) = op2(h(e16),h(e15))& h(op1(e16,e16)) = op2(h(e16),h(e16))& 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(e20,e26)) = op1(j(e20),j(e26))& 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(e21,e26)) = op1(j(e21),j(e26))& 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(e22,e26)) = op1(j(e22),j(e26))& 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(e23,e26)) = op1(j(e23),j(e26))& 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(e24,e26)) = op1(j(e24),j(e26))& 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))& j(op2(e25,e26)) = op1(j(e25),j(e26))& j(op2(e26,e20)) = op1(j(e26),j(e20))& j(op2(e26,e21)) = op1(j(e26),j(e21))& j(op2(e26,e22)) = op1(j(e26),j(e22))& j(op2(e26,e23)) = op1(j(e26),j(e23))& j(op2(e26,e24)) = op1(j(e26),j(e24))& j(op2(e26,e25)) = op1(j(e26),j(e25))& j(op2(e26,e26)) = op1(j(e26),j(e26))& h(j(e20)) = e20& h(j(e21)) = e21& h(j(e22)) = e22& h(j(e23)) = e23& h(j(e24)) = e24& h(j(e25)) = e25& h(j(e26)) = e26& j(h(e10)) = e10& j(h(e11)) = e11& j(h(e12)) = e12& j(h(e13)) = e13& j(h(e14)) = e14& j(h(e15)) = e15& j(h(e16)) = e16 ) ) ),
% 0.07/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.38 fof(f7,negated_conjecture,(
% 0.07/0.38 ~(( ( ( h(e10) = e20| h(e10) = e21| h(e10) = e22| h(e10) = e23| h(e10) = e24| h(e10) = e25| h(e10) = e26 )& ( h(e11) = e20| h(e11) = e21| h(e11) = e22| h(e11) = e23| h(e11) = e24| h(e11) = e25| h(e11) = e26 )& ( h(e12) = e20| h(e12) = e21| h(e12) = e22| h(e12) = e23| h(e12) = e24| h(e12) = e25| h(e12) = e26 )& ( h(e13) = e20| h(e13) = e21| h(e13) = e22| h(e13) = e23| h(e13) = e24| h(e13) = e25| h(e13) = e26 )& ( h(e14) = e20| h(e14) = e21| h(e14) = e22| h(e14) = e23| h(e14) = e24| h(e14) = e25| h(e14) = e26 )& ( h(e15) = e20| h(e15) = e21| h(e15) = e22| h(e15) = e23| h(e15) = e24| h(e15) = e25| h(e15) = e26 )& ( h(e16) = e20| h(e16) = e21| h(e16) = e22| h(e16) = e23| h(e16) = e24| h(e16) = e25| h(e16) = e26 )& ( j(e20) = e10| j(e20) = e11| j(e20) = e12| j(e20) = e13| j(e20) = e14| j(e20) = e15| j(e20) = e16 )& ( j(e21) = e10| j(e21) = e11| j(e21) = e12| j(e21) = e13| j(e21) = e14| j(e21) = e15| j(e21) = e16 )& ( j(e22) = e10| j(e22) = e11| j(e22) = e12| j(e22) = e13| j(e22) = e14| j(e22) = e15| j(e22) = e16 )& ( j(e23) = e10| j(e23) = e11| j(e23) = e12| j(e23) = e13| j(e23) = e14| j(e23) = e15| j(e23) = e16 )& ( j(e24) = e10| j(e24) = e11| j(e24) = e12| j(e24) = e13| j(e24) = e14| j(e24) = e15| j(e24) = e16 )& ( j(e25) = e10| j(e25) = e11| j(e25) = e12| j(e25) = e13| j(e25) = e14| j(e25) = e15| j(e25) = e16 )& ( j(e26) = e10| j(e26) = e11| j(e26) = e12| j(e26) = e13| j(e26) = e14| j(e26) = e15| j(e26) = e16 ) )=> ~ ( 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(e10,e16)) = op2(h(e10),h(e16))& 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(e11,e16)) = op2(h(e11),h(e16))& 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(e12,e16)) = op2(h(e12),h(e16))& 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(e13,e16)) = op2(h(e13),h(e16))& 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(e14,e16)) = op2(h(e14),h(e16))& 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))& h(op1(e15,e16)) = op2(h(e15),h(e16))& h(op1(e16,e10)) = op2(h(e16),h(e10))& h(op1(e16,e11)) = op2(h(e16),h(e11))& h(op1(e16,e12)) = op2(h(e16),h(e12))& h(op1(e16,e13)) = op2(h(e16),h(e13))& h(op1(e16,e14)) = op2(h(e16),h(e14))& h(op1(e16,e15)) = op2(h(e16),h(e15))& h(op1(e16,e16)) = op2(h(e16),h(e16))& 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(e20,e26)) = op1(j(e20),j(e26))& 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(e21,e26)) = op1(j(e21),j(e26))& 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(e22,e26)) = op1(j(e22),j(e26))& 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(e23,e26)) = op1(j(e23),j(e26))& 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(e24,e26)) = op1(j(e24),j(e26))& 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))& j(op2(e25,e26)) = op1(j(e25),j(e26))& j(op2(e26,e20)) = op1(j(e26),j(e20))& j(op2(e26,e21)) = op1(j(e26),j(e21))& j(op2(e26,e22)) = op1(j(e26),j(e22))& j(op2(e26,e23)) = op1(j(e26),j(e23))& j(op2(e26,e24)) = op1(j(e26),j(e24))& j(op2(e26,e25)) = op1(j(e26),j(e25))& j(op2(e26,e26)) = op1(j(e26),j(e26))& h(j(e20)) = e20& h(j(e21)) = e21& h(j(e22)) = e22& h(j(e23)) = e23& h(j(e24)) = e24& h(j(e25)) = e25& h(j(e26)) = e26& j(h(e10)) = e10& j(h(e11)) = e11& j(h(e12)) = e12& j(h(e13)) = e13& j(h(e14)) = e14& j(h(e15)) = e15& j(h(e16)) = e16 ) ) )),
% 0.07/0.38 inference(negated_conjecture,[status(cth)],[f6])).
% 0.07/0.38 fof(f30,plain,(
% 0.07/0.38 ~e20=e22),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f2])).
% 0.07/0.38 fof(f31,plain,(
% 0.07/0.38 ~e20=e23),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f2])).
% 0.07/0.38 fof(f33,plain,(
% 0.07/0.38 ~e20=e25),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f2])).
% 0.07/0.38 fof(f38,plain,(
% 0.07/0.38 ~e21=e25),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f2])).
% 0.07/0.38 fof(f39,plain,(
% 0.07/0.38 ~e21=e26),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f2])).
% 0.07/0.38 fof(f40,plain,(
% 0.07/0.38 ~e22=e23),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f2])).
% 0.07/0.38 fof(f99,plain,(
% 0.07/0.38 op1(e10,e10)=e10),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f4])).
% 0.07/0.38 fof(f107,plain,(
% 0.07/0.38 op1(e11,e11)=e11),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f4])).
% 0.07/0.38 fof(f115,plain,(
% 0.07/0.38 op1(e12,e12)=e12),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f4])).
% 0.07/0.38 fof(f123,plain,(
% 0.07/0.38 op1(e13,e13)=e13),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f4])).
% 0.07/0.38 fof(f131,plain,(
% 0.07/0.38 op1(e14,e14)=e14),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f4])).
% 0.07/0.38 fof(f139,plain,(
% 0.07/0.38 op1(e15,e15)=e15),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f4])).
% 0.07/0.38 fof(f147,plain,(
% 0.07/0.38 op1(e16,e16)=e16),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f4])).
% 0.07/0.38 fof(f148,plain,(
% 0.07/0.38 op2(e20,e20)=e22),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f5])).
% 0.07/0.38 fof(f151,plain,(
% 0.07/0.38 op2(e20,e23)=e25),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f5])).
% 0.07/0.38 fof(f156,plain,(
% 0.07/0.38 op2(e21,e21)=e26),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f5])).
% 0.07/0.38 fof(f164,plain,(
% 0.07/0.38 op2(e22,e22)=e23),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f5])).
% 0.07/0.38 fof(f172,plain,(
% 0.07/0.38 op2(e23,e23)=e20),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f5])).
% 0.07/0.38 fof(f188,plain,(
% 0.07/0.38 op2(e25,e25)=e21),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f5])).
% 0.07/0.38 fof(f196,plain,(
% 0.07/0.38 op2(e26,e26)=e25),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f5])).
% 0.07/0.38 fof(f197,plain,(
% 0.07/0.38 ((((((((((((((((((((h(e10)=e20|h(e10)=e21)|h(e10)=e22)|h(e10)=e23)|h(e10)=e24)|h(e10)=e25)|h(e10)=e26)&((((((h(e11)=e20|h(e11)=e21)|h(e11)=e22)|h(e11)=e23)|h(e11)=e24)|h(e11)=e25)|h(e11)=e26))&((((((h(e12)=e20|h(e12)=e21)|h(e12)=e22)|h(e12)=e23)|h(e12)=e24)|h(e12)=e25)|h(e12)=e26))&((((((h(e13)=e20|h(e13)=e21)|h(e13)=e22)|h(e13)=e23)|h(e13)=e24)|h(e13)=e25)|h(e13)=e26))&((((((h(e14)=e20|h(e14)=e21)|h(e14)=e22)|h(e14)=e23)|h(e14)=e24)|h(e14)=e25)|h(e14)=e26))&((((((h(e15)=e20|h(e15)=e21)|h(e15)=e22)|h(e15)=e23)|h(e15)=e24)|h(e15)=e25)|h(e15)=e26))&((((((h(e16)=e20|h(e16)=e21)|h(e16)=e22)|h(e16)=e23)|h(e16)=e24)|h(e16)=e25)|h(e16)=e26))&((((((j(e20)=e10|j(e20)=e11)|j(e20)=e12)|j(e20)=e13)|j(e20)=e14)|j(e20)=e15)|j(e20)=e16))&((((((j(e21)=e10|j(e21)=e11)|j(e21)=e12)|j(e21)=e13)|j(e21)=e14)|j(e21)=e15)|j(e21)=e16))&((((((j(e22)=e10|j(e22)=e11)|j(e22)=e12)|j(e22)=e13)|j(e22)=e14)|j(e22)=e15)|j(e22)=e16))&((((((j(e23)=e10|j(e23)=e11)|j(e23)=e12)|j(e23)=e13)|j(e23)=e14)|j(e23)=e15)|j(e23)=e16))&((((((j(e24)=e10|j(e24)=e11)|j(e24)=e12)|j(e24)=e13)|j(e24)=e14)|j(e24)=e15)|j(e24)=e16))&((((((j(e25)=e10|j(e25)=e11)|j(e25)=e12)|j(e25)=e13)|j(e25)=e14)|j(e25)=e15)|j(e25)=e16))&((((((j(e26)=e10|j(e26)=e11)|j(e26)=e12)|j(e26)=e13)|j(e26)=e14)|j(e26)=e15)|j(e26)=e16))&(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((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(e10,e16))=op2(h(e10),h(e16)))&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(e11,e16))=op2(h(e11),h(e16)))&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(e12,e16))=op2(h(e12),h(e16)))&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(e13,e16))=op2(h(e13),h(e16)))&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(e14,e16))=op2(h(e14),h(e16)))&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)))&h(op1(e15,e16))=op2(h(e15),h(e16)))&h(op1(e16,e10))=op2(h(e16),h(e10)))&h(op1(e16,e11))=op2(h(e16),h(e11)))&h(op1(e16,e12))=op2(h(e16),h(e12)))&h(op1(e16,e13))=op2(h(e16),h(e13)))&h(op1(e16,e14))=op2(h(e16),h(e14)))&h(op1(e16,e15))=op2(h(e16),h(e15)))&h(op1(e16,e16))=op2(h(e16),h(e16)))&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(e20,e26))=op1(j(e20),j(e26)))&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(e21,e26))=op1(j(e21),j(e26)))&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(e22,e26))=op1(j(e22),j(e26)))&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(e23,e26))=op1(j(e23),j(e26)))&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(e24,e26))=op1(j(e24),j(e26)))&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)))&j(op2(e25,e26))=op1(j(e25),j(e26)))&j(op2(e26,e20))=op1(j(e26),j(e20)))&j(op2(e26,e21))=op1(j(e26),j(e21)))&j(op2(e26,e22))=op1(j(e26),j(e22)))&j(op2(e26,e23))=op1(j(e26),j(e23)))&j(op2(e26,e24))=op1(j(e26),j(e24)))&j(op2(e26,e25))=op1(j(e26),j(e25)))&j(op2(e26,e26))=op1(j(e26),j(e26)))&h(j(e20))=e20)&h(j(e21))=e21)&h(j(e22))=e22)&h(j(e23))=e23)&h(j(e24))=e24)&h(j(e25))=e25)&h(j(e26))=e26)&j(h(e10))=e10)&j(h(e11))=e11)&j(h(e12))=e12)&j(h(e13))=e13)&j(h(e14))=e14)&j(h(e15))=e15)&j(h(e16))=e16))),
% 0.07/0.38 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.07/0.38 fof(f208,plain,(
% 0.07/0.38 j(e23)=e10|j(e23)=e11|j(e23)=e12|j(e23)=e13|j(e23)=e14|j(e23)=e15|j(e23)=e16),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f212,plain,(
% 0.07/0.38 h(op1(e10,e10))=op2(h(e10),h(e10))),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f220,plain,(
% 0.07/0.38 h(op1(e11,e11))=op2(h(e11),h(e11))),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f228,plain,(
% 0.07/0.38 h(op1(e12,e12))=op2(h(e12),h(e12))),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f236,plain,(
% 0.07/0.38 h(op1(e13,e13))=op2(h(e13),h(e13))),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f244,plain,(
% 0.07/0.38 h(op1(e14,e14))=op2(h(e14),h(e14))),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f252,plain,(
% 0.07/0.38 h(op1(e15,e15))=op2(h(e15),h(e15))),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f261,plain,(
% 0.07/0.38 j(op2(e20,e20))=op1(j(e20),j(e20))),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f264,plain,(
% 0.07/0.38 j(op2(e20,e23))=op1(j(e20),j(e23))),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f269,plain,(
% 0.07/0.38 j(op2(e21,e21))=op1(j(e21),j(e21))),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f285,plain,(
% 0.07/0.38 j(op2(e23,e23))=op1(j(e23),j(e23))),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f309,plain,(
% 0.07/0.38 j(op2(e26,e26))=op1(j(e26),j(e26))),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f310,plain,(
% 0.07/0.38 h(j(e20))=e20),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f311,plain,(
% 0.07/0.38 h(j(e21))=e21),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f312,plain,(
% 0.07/0.38 h(j(e22))=e22),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f313,plain,(
% 0.07/0.38 h(j(e23))=e23),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f315,plain,(
% 0.07/0.38 h(j(e25))=e25),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f316,plain,(
% 0.07/0.38 h(j(e26))=e26),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f318,plain,(
% 0.07/0.38 j(h(e11))=e11),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f321,plain,(
% 0.07/0.38 j(h(e14))=e14),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f322,plain,(
% 0.07/0.38 j(h(e15))=e15),
% 0.07/0.38 inference(cnf_transformation,[status(thm)],[f197])).
% 0.07/0.38 fof(f333,definition,(
% 0.07/0.38 sQ3_spl <=> (h(e10)=e23)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f334,plain,(
% 0.07/0.38 h(e10)=e23|~sQ3_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f333])).
% 0.07/0.38 fof(f349,definition,(
% 0.07/0.38 sQ8_spl <=> (h(e11)=e21)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f350,plain,(
% 0.07/0.38 h(e11)=e21|~sQ8_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f349])).
% 0.07/0.38 fof(f355,definition,(
% 0.07/0.38 sQ10_spl <=> (h(e11)=e23)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f356,plain,(
% 0.07/0.38 h(e11)=e23|~sQ10_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f355])).
% 0.07/0.38 fof(f361,definition,(
% 0.07/0.38 sQ12_spl <=> (h(e11)=e25)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f362,plain,(
% 0.07/0.38 h(e11)=e25|~sQ12_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f361])).
% 0.07/0.38 fof(f363,plain,(
% 0.07/0.38 ~h(e11)=e25|sQ12_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f361])).
% 0.07/0.38 fof(f364,definition,(
% 0.07/0.38 sQ13_spl <=> (h(e11)=e26)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f365,plain,(
% 0.07/0.38 h(e11)=e26|~sQ13_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f364])).
% 0.07/0.38 fof(f377,definition,(
% 0.07/0.38 sQ17_spl <=> (h(e12)=e23)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f378,plain,(
% 0.07/0.38 h(e12)=e23|~sQ17_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f377])).
% 0.07/0.38 fof(f383,definition,(
% 0.07/0.38 sQ19_spl <=> (h(e12)=e25)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f384,plain,(
% 0.07/0.38 h(e12)=e25|~sQ19_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f383])).
% 0.07/0.38 fof(f399,definition,(
% 0.07/0.38 sQ24_spl <=> (h(e13)=e23)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f400,plain,(
% 0.07/0.38 h(e13)=e23|~sQ24_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f399])).
% 0.07/0.38 fof(f412,definition,(
% 0.07/0.38 sQ28_spl <=> (h(e14)=e20)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f413,plain,(
% 0.07/0.38 h(e14)=e20|~sQ28_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f412])).
% 0.07/0.38 fof(f418,definition,(
% 0.07/0.38 sQ30_spl <=> (h(e14)=e22)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f419,plain,(
% 0.07/0.38 h(e14)=e22|~sQ30_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f418])).
% 0.07/0.38 fof(f421,definition,(
% 0.07/0.38 sQ31_spl <=> (h(e14)=e23)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f422,plain,(
% 0.07/0.38 h(e14)=e23|~sQ31_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f421])).
% 0.07/0.38 fof(f434,definition,(
% 0.07/0.38 sQ35_spl <=> (h(e15)=e20)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f435,plain,(
% 0.07/0.38 h(e15)=e20|~sQ35_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f434])).
% 0.07/0.38 fof(f437,definition,(
% 0.07/0.38 sQ36_spl <=> (h(e15)=e21)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f438,plain,(
% 0.07/0.38 h(e15)=e21|~sQ36_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f437])).
% 0.07/0.38 fof(f440,definition,(
% 0.07/0.38 sQ37_spl <=> (h(e15)=e22)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f441,plain,(
% 0.07/0.38 h(e15)=e22|~sQ37_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f440])).
% 0.07/0.38 fof(f443,definition,(
% 0.07/0.38 sQ38_spl <=> (h(e15)=e23)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f444,plain,(
% 0.07/0.38 h(e15)=e23|~sQ38_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f443])).
% 0.07/0.38 fof(f449,definition,(
% 0.07/0.38 sQ40_spl <=> (h(e15)=e25)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f450,plain,(
% 0.07/0.38 h(e15)=e25|~sQ40_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f449])).
% 0.07/0.38 fof(f456,definition,(
% 0.07/0.38 sQ42_spl <=> (h(e16)=e20)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f457,plain,(
% 0.07/0.38 h(e16)=e20|~sQ42_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f456])).
% 0.07/0.38 fof(f493,definition,(
% 0.07/0.38 sQ54_spl <=> (j(e20)=e15)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f494,plain,(
% 0.07/0.38 j(e20)=e15|~sQ54_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f493])).
% 0.07/0.38 fof(f495,plain,(
% 0.07/0.38 ~j(e20)=e15|sQ54_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f493])).
% 0.07/0.38 fof(f496,definition,(
% 0.07/0.38 sQ55_spl <=> (j(e20)=e16)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f497,plain,(
% 0.07/0.38 j(e20)=e16|~sQ55_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f496])).
% 0.07/0.38 fof(f498,plain,(
% 0.07/0.38 ~j(e20)=e16|sQ55_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f496])).
% 0.07/0.38 fof(f503,definition,(
% 0.07/0.38 sQ57_spl <=> (j(e21)=e11)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f504,plain,(
% 0.07/0.38 j(e21)=e11|~sQ57_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f503])).
% 0.07/0.38 fof(f515,definition,(
% 0.07/0.38 sQ61_spl <=> (j(e21)=e15)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f516,plain,(
% 0.07/0.38 j(e21)=e15|~sQ61_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f515])).
% 0.07/0.38 fof(f534,definition,(
% 0.07/0.38 sQ67_spl <=> (j(e22)=e14)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f535,plain,(
% 0.07/0.38 j(e22)=e14|~sQ67_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f534])).
% 0.07/0.38 fof(f536,plain,(
% 0.07/0.38 ~j(e22)=e14|sQ67_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f534])).
% 0.07/0.38 fof(f537,definition,(
% 0.07/0.38 sQ68_spl <=> (j(e22)=e15)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f538,plain,(
% 0.07/0.38 j(e22)=e15|~sQ68_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f537])).
% 0.07/0.38 fof(f539,plain,(
% 0.07/0.38 ~j(e22)=e15|sQ68_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f537])).
% 0.07/0.38 fof(f544,definition,(
% 0.07/0.38 sQ70_spl <=> (j(e23)=e10)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f545,plain,(
% 0.07/0.38 j(e23)=e10|~sQ70_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f544])).
% 0.07/0.38 fof(f547,definition,(
% 0.07/0.38 sQ71_spl <=> (j(e23)=e11)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f548,plain,(
% 0.07/0.38 j(e23)=e11|~sQ71_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f547])).
% 0.07/0.38 fof(f550,definition,(
% 0.07/0.38 sQ72_spl <=> (j(e23)=e12)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f551,plain,(
% 0.07/0.38 j(e23)=e12|~sQ72_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f550])).
% 0.07/0.38 fof(f553,definition,(
% 0.07/0.38 sQ73_spl <=> (j(e23)=e13)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f554,plain,(
% 0.07/0.38 j(e23)=e13|~sQ73_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f553])).
% 0.07/0.38 fof(f556,definition,(
% 0.07/0.38 sQ74_spl <=> (j(e23)=e14)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f557,plain,(
% 0.07/0.38 j(e23)=e14|~sQ74_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f556])).
% 0.07/0.38 fof(f559,definition,(
% 0.07/0.38 sQ75_spl <=> (j(e23)=e15)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f560,plain,(
% 0.07/0.38 j(e23)=e15|~sQ75_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f559])).
% 0.07/0.38 fof(f562,definition,(
% 0.07/0.38 sQ76_spl <=> (j(e23)=e16)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f563,plain,(
% 0.07/0.38 j(e23)=e16|~sQ76_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f562])).
% 0.07/0.38 fof(f565,plain,(
% 0.07/0.38 sQ70_spl|sQ71_spl|sQ72_spl|sQ73_spl|sQ74_spl|sQ75_spl|sQ76_spl),
% 0.07/0.38 inference(split_clause,[status(thm)],[f208,f544,f547,f550,f553,f556,f559,f562])).
% 0.07/0.38 fof(f606,definition,(
% 0.07/0.38 sQ90_spl <=> (j(e25)=e16)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f607,plain,(
% 0.07/0.38 j(e25)=e16|~sQ90_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f606])).
% 0.07/0.38 fof(f608,plain,(
% 0.07/0.38 ~j(e25)=e16|sQ90_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f606])).
% 0.07/0.38 fof(f613,definition,(
% 0.07/0.38 sQ92_spl <=> (j(e26)=e11)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f614,plain,(
% 0.07/0.38 j(e26)=e11|~sQ92_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f613])).
% 0.07/0.38 fof(f622,definition,(
% 0.07/0.38 sQ95_spl <=> (j(e26)=e14)),
% 0.07/0.38 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.07/0.38 fof(f623,plain,(
% 0.07/0.38 j(e26)=e14|~sQ95_spl),
% 0.07/0.38 inference(component_clause,[status(thm)],[f622])).
% 0.07/0.38 fof(f800,plain,(
% 0.07/0.38 h(e11)=e23|~sQ71_spl),
% 0.07/0.38 inference(backward_demodulation,[status(thm)],[f548,f313])).
% 0.07/0.38 fof(f869,plain,(
% 0.07/0.38 h(e16)=e20|~sQ55_spl),
% 0.07/0.38 inference(backward_demodulation,[status(thm)],[f497,f310])).
% 0.07/0.38 fof(f955,plain,(
% 0.07/0.38 h(op1(e11,e11))=op2(h(e11),e26)|~sQ13_spl),
% 0.07/0.38 inference(backward_demodulation,[status(thm)],[f365,f220])).
% 0.07/0.38 fof(f956,plain,(
% 0.07/0.38 h(op1(e11,e11))=op2(e26,e26)|~sQ13_spl),
% 0.07/0.38 inference(forward_demodulation,[status(thm)],[f365,f955])).
% 0.07/0.38 fof(f1002,plain,(
% 0.07/0.39 h(op1(e15,e15))=op2(e20,h(e15))|~sQ35_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f435,f252])).
% 0.07/0.39 fof(f1003,plain,(
% 0.07/0.39 h(op1(e15,e15))=op2(e20,e20)|~sQ35_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f435,f1002])).
% 0.07/0.39 fof(f1100,plain,(
% 0.07/0.39 h(e13)=e23|~sQ73_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f554,f313])).
% 0.07/0.39 fof(f1118,plain,(
% 0.07/0.39 h(op1(e14,e14))=op2(e20,h(e14))|~sQ28_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f413,f244])).
% 0.07/0.39 fof(f1119,plain,(
% 0.07/0.39 h(op1(e14,e14))=op2(e20,e20)|~sQ28_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f413,f1118])).
% 0.07/0.39 fof(f1139,plain,(
% 0.07/0.39 h(e14)=e22|~sQ67_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f535,f312])).
% 0.07/0.39 fof(f1140,plain,(
% 0.07/0.39 e20=e22|~sQ28_spl|~sQ67_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f413,f1139])).
% 0.07/0.39 fof(f1141,plain,(
% 0.07/0.39 $false|~sQ28_spl|~sQ67_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1140,f30])).
% 0.07/0.39 fof(f1142,plain,(
% 0.07/0.39 ~sQ28_spl|~sQ67_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f1141])).
% 0.07/0.39 fof(f1253,plain,(
% 0.07/0.39 sQ42_spl|~sQ55_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f869,f456,f496])).
% 0.07/0.39 fof(f1271,plain,(
% 0.07/0.39 h(e10)=e23|~sQ70_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f545,f313])).
% 0.07/0.39 fof(f1286,plain,(
% 0.07/0.39 h(e16)=e25|~sQ90_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f607,f315])).
% 0.07/0.39 fof(f1324,plain,(
% 0.07/0.39 h(e15)=e21|~sQ61_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f516,f311])).
% 0.07/0.39 fof(f1328,plain,(
% 0.07/0.39 sQ36_spl|~sQ61_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f1324,f437,f515])).
% 0.07/0.39 fof(f1343,plain,(
% 0.07/0.39 j(e22)=e14|~sQ30_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f419,f321])).
% 0.07/0.39 fof(f1395,plain,(
% 0.07/0.39 h(e11)=op2(h(e11),h(e11))),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f107,f220])).
% 0.07/0.39 fof(f1400,plain,(
% 0.07/0.39 h(e12)=op2(h(e12),h(e12))),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f115,f228])).
% 0.07/0.39 fof(f1411,plain,(
% 0.07/0.39 h(e11)=e26|~sQ92_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f614,f316])).
% 0.07/0.39 fof(f1418,plain,(
% 0.07/0.39 sQ13_spl|~sQ92_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f1411,f364,f613])).
% 0.07/0.39 fof(f1419,plain,(
% 0.07/0.39 h(e11)=op2(e26,e26)|~sQ13_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f107,f956])).
% 0.07/0.39 fof(f1442,plain,(
% 0.07/0.39 h(e10)=op2(h(e10),h(e10))),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f99,f212])).
% 0.07/0.39 fof(f1509,plain,(
% 0.07/0.39 ~e14=e14|~sQ30_spl|sQ67_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f1343,f536])).
% 0.07/0.39 fof(f1510,plain,(
% 0.07/0.39 $false|~sQ30_spl|sQ67_spl),
% 0.07/0.39 inference(trivial_equality_resolution,[status(thm)],[f1509])).
% 0.07/0.39 fof(f1511,plain,(
% 0.07/0.39 ~sQ30_spl|sQ67_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f1510])).
% 0.07/0.39 fof(f1523,plain,(
% 0.07/0.39 e20=e25|~sQ42_spl|~sQ90_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f457,f1286])).
% 0.07/0.39 fof(f1524,plain,(
% 0.07/0.39 $false|~sQ42_spl|~sQ90_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1523,f33])).
% 0.07/0.39 fof(f1525,plain,(
% 0.07/0.39 ~sQ42_spl|~sQ90_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f1524])).
% 0.07/0.39 fof(f1535,plain,(
% 0.07/0.39 j(op2(e20,e23))=op1(j(e20),e16)|~sQ76_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f563,f264])).
% 0.07/0.39 fof(f1553,plain,(
% 0.07/0.39 j(op2(e23,e23))=op1(e16,j(e23))|~sQ76_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f563,f285])).
% 0.07/0.39 fof(f1554,plain,(
% 0.07/0.39 j(op2(e23,e23))=op1(e16,e16)|~sQ76_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f563,f1553])).
% 0.07/0.39 fof(f1558,plain,(
% 0.07/0.39 h(e11)=e21|~sQ57_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f504,f311])).
% 0.07/0.39 fof(f1566,plain,(
% 0.07/0.39 sQ8_spl|~sQ57_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f1558,f349,f503])).
% 0.07/0.39 fof(f1573,plain,(
% 0.07/0.39 h(op1(e15,e15))=op2(h(e15),e22)|~sQ37_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f441,f252])).
% 0.07/0.39 fof(f1582,plain,(
% 0.07/0.39 h(op1(e15,e15))=op2(e22,e22)|~sQ37_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f441,f1573])).
% 0.07/0.39 fof(f1604,plain,(
% 0.07/0.39 h(e13)=op2(h(e13),h(e13))),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f123,f236])).
% 0.07/0.39 fof(f1605,plain,(
% 0.07/0.39 e23=op2(h(e13),h(e13))|~sQ24_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f400,f1604])).
% 0.07/0.39 fof(f1606,plain,(
% 0.07/0.39 e23=op2(e23,h(e13))|~sQ24_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f400,f1605])).
% 0.07/0.39 fof(f1608,plain,(
% 0.07/0.39 e23=op2(e23,e23)|~sQ24_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f400,f1606])).
% 0.07/0.39 fof(f1614,plain,(
% 0.07/0.39 sQ24_spl|~sQ73_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f1100,f399,f553])).
% 0.07/0.39 fof(f1615,plain,(
% 0.07/0.39 sQ10_spl|~sQ71_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f800,f355,f547])).
% 0.07/0.39 fof(f1656,plain,(
% 0.07/0.39 e25=op2(h(e11),h(e11))|~sQ12_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f362,f1395])).
% 0.07/0.39 fof(f1657,plain,(
% 0.07/0.39 e25=op2(e25,h(e11))|~sQ12_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f362,f1656])).
% 0.07/0.39 fof(f1658,plain,(
% 0.07/0.39 e25=op2(e25,e25)|~sQ12_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f362,f1657])).
% 0.07/0.39 fof(f1731,plain,(
% 0.07/0.39 h(e14)=op2(h(e14),h(e14))),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f131,f244])).
% 0.07/0.39 fof(f1739,plain,(
% 0.07/0.39 j(e22)=op1(j(e20),j(e20))),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f148,f261])).
% 0.07/0.39 fof(f1781,plain,(
% 0.07/0.39 sQ3_spl|~sQ70_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f1271,f333,f544])).
% 0.07/0.39 fof(f1808,plain,(
% 0.07/0.39 j(op2(e23,e23))=e16|~sQ76_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f147,f1554])).
% 0.07/0.39 fof(f1950,plain,(
% 0.07/0.39 e23=op2(h(e11),h(e11))|~sQ10_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f356,f1395])).
% 0.07/0.39 fof(f1951,plain,(
% 0.07/0.39 e23=op2(e23,h(e11))|~sQ10_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f356,f1950])).
% 0.07/0.39 fof(f1953,plain,(
% 0.07/0.39 e23=op2(e23,e23)|~sQ10_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f356,f1951])).
% 0.07/0.39 fof(f1966,plain,(
% 0.07/0.39 h(e15)=op2(h(e15),h(e15))),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f139,f252])).
% 0.07/0.39 fof(f2001,plain,(
% 0.07/0.39 j(e22)=op1(e15,j(e20))|~sQ54_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f494,f1739])).
% 0.07/0.39 fof(f2002,plain,(
% 0.07/0.39 j(e22)=op1(e15,e15)|~sQ54_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f494,f2001])).
% 0.07/0.39 fof(f2003,plain,(
% 0.07/0.39 j(e22)=e15|~sQ54_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f139,f2002])).
% 0.07/0.39 fof(f2004,plain,(
% 0.07/0.39 $false|sQ68_spl|~sQ54_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f2003,f539])).
% 0.07/0.39 fof(f2005,plain,(
% 0.07/0.39 sQ68_spl|~sQ54_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f2004])).
% 0.07/0.39 fof(f2080,plain,(
% 0.07/0.39 j(e23)=e15|~sQ38_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f444,f322])).
% 0.07/0.39 fof(f2090,plain,(
% 0.07/0.39 sQ75_spl|~sQ38_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f2080,f559,f443])).
% 0.07/0.39 fof(f2091,plain,(
% 0.07/0.39 h(e15)=op2(e22,e22)|~sQ37_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f139,f1582])).
% 0.07/0.39 fof(f2092,plain,(
% 0.07/0.39 h(e15)=e23|~sQ37_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f164,f2091])).
% 0.07/0.39 fof(f2136,plain,(
% 0.07/0.39 j(e26)=op1(j(e21),j(e21))),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f156,f269])).
% 0.07/0.39 fof(f2243,plain,(
% 0.07/0.39 j(e20)=op1(j(e23),j(e23))),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f172,f285])).
% 0.07/0.39 fof(f2244,plain,(
% 0.07/0.39 j(e20)=op1(e14,j(e23))|~sQ74_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f557,f2243])).
% 0.07/0.39 fof(f2245,plain,(
% 0.07/0.39 j(e20)=op1(e14,e14)|~sQ74_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f557,f2244])).
% 0.07/0.39 fof(f2250,plain,(
% 0.07/0.39 h(e14)=e20|~sQ74_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f2258,f310])).
% 0.07/0.39 fof(f2258,plain,(
% 0.07/0.39 j(e20)=e14|~sQ74_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f131,f2245])).
% 0.07/0.39 fof(f2259,plain,(
% 0.07/0.39 sQ28_spl|~sQ74_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f2250,f412,f556])).
% 0.07/0.39 fof(f2262,plain,(
% 0.07/0.39 e23=e20|~sQ24_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f172,f1608])).
% 0.07/0.39 fof(f2263,plain,(
% 0.07/0.39 $false|~sQ24_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f2262,f31])).
% 0.07/0.39 fof(f2264,plain,(
% 0.07/0.39 ~sQ24_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f2263])).
% 0.07/0.39 fof(f2271,plain,(
% 0.07/0.39 h(e14)=op2(e20,e20)|~sQ28_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f131,f1119])).
% 0.07/0.39 fof(f2272,plain,(
% 0.07/0.39 h(e14)=e22|~sQ28_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f148,f2271])).
% 0.07/0.39 fof(f2292,plain,(
% 0.07/0.39 e23=e20|~sQ10_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f172,f1953])).
% 0.07/0.39 fof(f2293,plain,(
% 0.07/0.39 $false|~sQ10_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f2292,f31])).
% 0.07/0.39 fof(f2294,plain,(
% 0.07/0.39 ~sQ10_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f2293])).
% 0.07/0.39 fof(f2317,plain,(
% 0.07/0.39 h(e14)=op2(h(e14),e23)|~sQ31_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f422,f1731])).
% 0.07/0.39 fof(f2319,plain,(
% 0.07/0.39 e23=op2(h(e14),e23)|~sQ31_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f422,f2317])).
% 0.07/0.39 fof(f2320,plain,(
% 0.07/0.39 e23=op2(e23,e23)|~sQ31_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f422,f2319])).
% 0.07/0.39 fof(f2321,plain,(
% 0.07/0.39 e23=e20|~sQ31_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f172,f2320])).
% 0.07/0.39 fof(f2322,plain,(
% 0.07/0.39 $false|~sQ31_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f2321,f31])).
% 0.07/0.39 fof(f2323,plain,(
% 0.07/0.39 ~sQ31_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f2322])).
% 0.07/0.39 fof(f2327,plain,(
% 0.07/0.39 sQ30_spl|~sQ28_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f2272,f418,f412])).
% 0.07/0.39 fof(f2364,plain,(
% 0.07/0.39 e22=e23|~sQ37_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f441,f2092])).
% 0.07/0.39 fof(f2365,plain,(
% 0.07/0.39 $false|~sQ37_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f2364,f40])).
% 0.07/0.39 fof(f2366,plain,(
% 0.07/0.39 ~sQ37_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f2365])).
% 0.07/0.39 fof(f2423,plain,(
% 0.07/0.39 j(e25)=op1(j(e26),j(e26))),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f196,f309])).
% 0.07/0.39 fof(f2477,plain,(
% 0.07/0.39 j(e20)=op1(e15,j(e23))|~sQ75_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f560,f2243])).
% 0.07/0.39 fof(f2478,plain,(
% 0.07/0.39 j(e20)=op1(e15,e15)|~sQ75_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f560,f2477])).
% 0.07/0.39 fof(f2479,plain,(
% 0.07/0.39 j(e20)=e15|~sQ75_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f139,f2478])).
% 0.07/0.39 fof(f2480,plain,(
% 0.07/0.39 $false|sQ54_spl|~sQ75_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f2479,f495])).
% 0.07/0.39 fof(f2481,plain,(
% 0.07/0.39 sQ54_spl|~sQ75_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f2480])).
% 0.07/0.39 fof(f2482,plain,(
% 0.07/0.39 j(e25)=op1(j(e20),e16)|~sQ76_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f151,f1535])).
% 0.07/0.39 fof(f2494,plain,(
% 0.07/0.39 j(e20)=e16|~sQ76_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f172,f1808])).
% 0.07/0.39 fof(f2495,plain,(
% 0.07/0.39 $false|sQ55_spl|~sQ76_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f2494,f498])).
% 0.07/0.39 fof(f2496,plain,(
% 0.07/0.39 sQ55_spl|~sQ76_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f2495])).
% 0.07/0.39 fof(f2636,plain,(
% 0.07/0.39 h(e15)=e22|~sQ68_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f538,f312])).
% 0.07/0.39 fof(f2641,plain,(
% 0.07/0.39 sQ37_spl|~sQ68_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f2636,f440,f537])).
% 0.07/0.39 fof(f2677,plain,(
% 0.07/0.39 e21=op2(h(e15),h(e15))|~sQ36_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f438,f1966])).
% 0.07/0.39 fof(f2678,plain,(
% 0.07/0.39 e21=op2(e21,h(e15))|~sQ36_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f438,f2677])).
% 0.07/0.39 fof(f2679,plain,(
% 0.07/0.39 e21=e26|~sQ36_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f2680,f156])).
% 0.07/0.39 fof(f2680,plain,(
% 0.07/0.39 e21=op2(e21,e21)|~sQ36_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f438,f2678])).
% 0.07/0.39 fof(f2681,plain,(
% 0.07/0.39 $false|~sQ36_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f2679,f39])).
% 0.07/0.39 fof(f2682,plain,(
% 0.07/0.39 ~sQ36_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f2681])).
% 0.07/0.39 fof(f2687,plain,(
% 0.07/0.39 h(e15)=op2(e20,e20)|~sQ35_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f139,f1003])).
% 0.07/0.39 fof(f2688,plain,(
% 0.07/0.39 h(e15)=e22|~sQ35_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f148,f2687])).
% 0.07/0.39 fof(f2757,plain,(
% 0.07/0.39 j(e21)=e11|~sQ8_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f350,f318])).
% 0.07/0.39 fof(f2770,plain,(
% 0.07/0.39 e25=e21|~sQ12_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f188,f1658])).
% 0.07/0.39 fof(f2771,plain,(
% 0.07/0.39 $false|~sQ12_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f2770,f38])).
% 0.07/0.39 fof(f2772,plain,(
% 0.07/0.39 ~sQ12_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f2771])).
% 0.07/0.39 fof(f2799,plain,(
% 0.07/0.39 sQ37_spl|~sQ35_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f2688,f440,f434])).
% 0.07/0.39 fof(f2858,plain,(
% 0.07/0.39 h(e12)=e23|~sQ72_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f551,f313])).
% 0.07/0.39 fof(f2938,plain,(
% 0.07/0.39 e25=op2(h(e12),h(e12))|~sQ19_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f384,f1400])).
% 0.07/0.39 fof(f2939,plain,(
% 0.07/0.39 e25=op2(e25,h(e12))|~sQ19_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f384,f2938])).
% 0.07/0.39 fof(f2940,plain,(
% 0.07/0.39 e25=op2(e25,e25)|~sQ19_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f384,f2939])).
% 0.07/0.39 fof(f2941,plain,(
% 0.07/0.39 e25=e21|~sQ19_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f188,f2940])).
% 0.07/0.39 fof(f2942,plain,(
% 0.07/0.39 $false|~sQ19_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f2941,f38])).
% 0.07/0.39 fof(f2943,plain,(
% 0.07/0.39 ~sQ19_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f2942])).
% 0.07/0.39 fof(f2965,plain,(
% 0.07/0.39 h(e11)=e25|~sQ13_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f196,f1419])).
% 0.07/0.39 fof(f2966,plain,(
% 0.07/0.39 $false|sQ12_spl|~sQ13_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f2965,f363])).
% 0.07/0.39 fof(f2967,plain,(
% 0.07/0.39 sQ12_spl|~sQ13_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f2966])).
% 0.07/0.39 fof(f3066,plain,(
% 0.07/0.39 sQ17_spl|~sQ72_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f2858,f377,f550])).
% 0.07/0.39 fof(f3101,plain,(
% 0.07/0.39 j(e25)=op1(e14,j(e26))|~sQ95_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f623,f2423])).
% 0.07/0.39 fof(f3102,plain,(
% 0.07/0.39 j(e25)=op1(e14,e14)|~sQ95_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f623,f3101])).
% 0.07/0.39 fof(f3124,plain,(
% 0.07/0.39 j(e25)=e14|~sQ95_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f131,f3102])).
% 0.07/0.39 fof(f3142,plain,(
% 0.07/0.39 h(e14)=op2(h(e14),e25)|~sQ95_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f3145,f1731])).
% 0.07/0.39 fof(f3145,plain,(
% 0.07/0.39 h(e14)=e25|~sQ95_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f3124,f315])).
% 0.07/0.39 fof(f3146,plain,(
% 0.07/0.39 e25=op2(h(e14),e25)|~sQ95_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f3145,f3142])).
% 0.07/0.39 fof(f3147,plain,(
% 0.07/0.39 e25=op2(e25,e25)|~sQ95_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f3145,f3146])).
% 0.07/0.39 fof(f3148,plain,(
% 0.07/0.39 e25=e21|~sQ95_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f188,f3147])).
% 0.07/0.39 fof(f3149,plain,(
% 0.07/0.39 $false|~sQ95_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f3148,f38])).
% 0.07/0.39 fof(f3150,plain,(
% 0.07/0.39 ~sQ95_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f3149])).
% 0.07/0.39 fof(f3175,plain,(
% 0.07/0.39 j(e26)=op1(e11,j(e21))|~sQ8_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f2757,f2136])).
% 0.07/0.39 fof(f3176,plain,(
% 0.07/0.39 j(e26)=op1(e11,e11)|~sQ8_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f2757,f3175])).
% 0.07/0.39 fof(f3179,plain,(
% 0.07/0.39 h(e11)=e26|~sQ8_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f3182,f316])).
% 0.07/0.39 fof(f3182,plain,(
% 0.07/0.39 j(e26)=e11|~sQ8_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f107,f3176])).
% 0.07/0.39 fof(f3183,plain,(
% 0.07/0.39 sQ13_spl|~sQ8_spl),
% 0.07/0.39 inference(split_clause,[status(thm)],[f3179,f364,f349])).
% 0.07/0.39 fof(f3210,plain,(
% 0.07/0.39 h(e10)=op2(h(e10),e23)|~sQ3_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f334,f1442])).
% 0.07/0.39 fof(f3215,plain,(
% 0.07/0.39 e23=op2(h(e10),e23)|~sQ3_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f334,f3210])).
% 0.07/0.39 fof(f3216,plain,(
% 0.07/0.39 e23=op2(e23,e23)|~sQ3_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f334,f3215])).
% 0.07/0.39 fof(f3217,plain,(
% 0.07/0.39 e23=e20|~sQ3_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f172,f3216])).
% 0.07/0.39 fof(f3218,plain,(
% 0.07/0.39 $false|~sQ3_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f3217,f31])).
% 0.07/0.39 fof(f3219,plain,(
% 0.07/0.39 ~sQ3_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f3218])).
% 0.07/0.39 fof(f3243,plain,(
% 0.07/0.39 h(e12)=op2(h(e12),e23)|~sQ17_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f378,f1400])).
% 0.07/0.39 fof(f3249,plain,(
% 0.07/0.39 e23=op2(h(e12),e23)|~sQ17_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f378,f3243])).
% 0.07/0.39 fof(f3250,plain,(
% 0.07/0.39 e23=op2(e23,e23)|~sQ17_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f378,f3249])).
% 0.07/0.39 fof(f3251,plain,(
% 0.07/0.39 e23=e20|~sQ17_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f172,f3250])).
% 0.07/0.39 fof(f3252,plain,(
% 0.07/0.39 $false|~sQ17_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f3251,f31])).
% 0.07/0.39 fof(f3253,plain,(
% 0.07/0.39 ~sQ17_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f3252])).
% 0.07/0.39 fof(f3343,plain,(
% 0.07/0.39 h(e15)=op2(h(e15),e25)|~sQ40_spl),
% 0.07/0.39 inference(backward_demodulation,[status(thm)],[f450,f1966])).
% 0.07/0.39 fof(f3352,plain,(
% 0.07/0.39 e25=op2(h(e15),e25)|~sQ40_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f450,f3343])).
% 0.07/0.39 fof(f3353,plain,(
% 0.07/0.39 e25=op2(e25,e25)|~sQ40_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f450,f3352])).
% 0.07/0.39 fof(f3354,plain,(
% 0.07/0.39 e25=e21|~sQ40_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f188,f3353])).
% 0.07/0.39 fof(f3355,plain,(
% 0.07/0.39 $false|~sQ40_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f3354,f38])).
% 0.07/0.39 fof(f3356,plain,(
% 0.07/0.39 ~sQ40_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f3355])).
% 0.07/0.39 fof(f3424,plain,(
% 0.07/0.39 j(e25)=op1(e16,e16)|~sQ76_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f2494,f2482])).
% 0.07/0.39 fof(f3425,plain,(
% 0.07/0.39 j(e25)=e16|~sQ76_spl),
% 0.07/0.39 inference(forward_demodulation,[status(thm)],[f147,f3424])).
% 0.07/0.39 fof(f3426,plain,(
% 0.07/0.39 $false|sQ90_spl|~sQ76_spl),
% 0.07/0.39 inference(forward_subsumption_resolution,[status(thm)],[f3425,f608])).
% 0.07/0.39 fof(f3427,plain,(
% 0.07/0.39 sQ90_spl|~sQ76_spl),
% 0.07/0.39 inference(contradiction_clause,[status(thm)],[f3426])).
% 0.07/0.39 fof(f3428,plain,(
% 0.07/0.39 $false),
% 0.07/0.39 inference(sat_refutation,[status(thm)],[f565,f1142,f1253,f1328,f1418,f1511,f1525,f1566,f1614,f1615,f1781,f2005,f2090,f2259,f2264,f2294,f2323,f2327,f2366,f2481,f2496,f2641,f2682,f2772,f2799,f2943,f2967,f3066,f3150,f3183,f3219,f3253,f3356,f3427])).
% 0.07/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.07/0.39 % Elapsed time: 0.093979 seconds
% 0.07/0.39 % CPU time: 0.535426 seconds
% 0.07/0.39 % Total memory used: 135.516 MB
% 0.07/0.39 % Net memory used: 135.115 MB
%------------------------------------------------------------------------------