%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG204+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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.09s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG204+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 13:01:33 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.49 % Refutation found
% 0.09/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.49 fof(f1,axiom,(
% 0.09/0.49 ( e10 != e11& e10 != e12& e10 != e13& e10 != e14& e10 != e15& e10 != e16& e11 != e12& e11 != e13& e11 != e14& e11 != e15& e11 != e16& e12 != e13& e12 != e14& e12 != e15& e12 != e16& e13 != e14& e13 != e15& e13 != e16& e14 != e15& e14 != e16& e15 != e16 ) ),
% 0.09/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.49 fof(f2,axiom,(
% 0.09/0.49 ( 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.09/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.49 fof(f4,axiom,(
% 0.09/0.49 ( op1(e10,e10) = e13& op1(e10,e11) = e10& op1(e10,e12) = e16& op1(e10,e13) = e11& op1(e10,e14) = e14& op1(e10,e15) = e12& op1(e10,e16) = e15& op1(e11,e10) = e10& op1(e11,e11) = e16& op1(e11,e12) = e11& op1(e11,e13) = e15& op1(e11,e14) = e13& op1(e11,e15) = e14& op1(e11,e16) = e12& op1(e12,e10) = e16& op1(e12,e11) = e11& op1(e12,e12) = e15& op1(e12,e13) = e12& op1(e12,e14) = e10& op1(e12,e15) = e13& op1(e12,e16) = e14& op1(e13,e10) = e11& op1(e13,e11) = e15& op1(e13,e12) = e12& op1(e13,e13) = e14& op1(e13,e14) = e16& op1(e13,e15) = e10& op1(e13,e16) = e13& op1(e14,e10) = e14& op1(e14,e11) = e13& op1(e14,e12) = e10& op1(e14,e13) = e16& op1(e14,e14) = e12& op1(e14,e15) = e15& op1(e14,e16) = e11& op1(e15,e10) = e12& op1(e15,e11) = e14& op1(e15,e12) = e13& op1(e15,e13) = e10& op1(e15,e14) = e15& op1(e15,e15) = e11& op1(e15,e16) = e16& op1(e16,e10) = e15& op1(e16,e11) = e12& op1(e16,e12) = e14& op1(e16,e13) = e13& op1(e16,e14) = e11& op1(e16,e15) = e16& op1(e16,e16) = e10 ) ),
% 0.09/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.50 fof(f5,axiom,(
% 0.09/0.50 ( op2(e20,e20) = e20& op2(e20,e21) = e23& op2(e20,e22) = e21& op2(e20,e23) = e22& op2(e20,e24) = e26& op2(e20,e25) = e24& op2(e20,e26) = e25& op2(e21,e20) = e23& op2(e21,e21) = e21& op2(e21,e22) = e26& op2(e21,e23) = e25& op2(e21,e24) = e22& op2(e21,e25) = e20& op2(e21,e26) = e24& op2(e22,e20) = e21& op2(e22,e21) = e26& op2(e22,e22) = e22& op2(e22,e23) = e24& op2(e22,e24) = e25& op2(e22,e25) = e23& op2(e22,e26) = e20& op2(e23,e20) = e22& op2(e23,e21) = e25& op2(e23,e22) = e24& op2(e23,e23) = e23& op2(e23,e24) = e20& op2(e23,e25) = e26& op2(e23,e26) = e21& op2(e24,e20) = e26& op2(e24,e21) = e22& op2(e24,e22) = e25& op2(e24,e23) = e20& op2(e24,e24) = e24& op2(e24,e25) = e21& op2(e24,e26) = e23& op2(e25,e20) = e24& op2(e25,e21) = e20& op2(e25,e22) = e23& op2(e25,e23) = e26& op2(e25,e24) = e21& op2(e25,e25) = e25& op2(e25,e26) = e22& op2(e26,e20) = e25& op2(e26,e21) = e24& op2(e26,e22) = e20& op2(e26,e23) = e21& op2(e26,e24) = e23& op2(e26,e25) = e22& op2(e26,e26) = e26 ) ),
% 0.09/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.50 fof(f6,conjecture,(
% 0.09/0.50 ( ( ( 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.09/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.50 fof(f7,negated_conjecture,(
% 0.09/0.50 ~(( ( ( 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.09/0.50 inference(negated_conjecture,[status(cth)],[f6])).
% 0.09/0.50 fof(f10,plain,(
% 0.09/0.50 ~e10=e13),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f1])).
% 0.09/0.50 fof(f13,plain,(
% 0.09/0.50 ~e10=e16),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f1])).
% 0.09/0.50 fof(f17,plain,(
% 0.09/0.50 ~e11=e15),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f1])).
% 0.09/0.50 fof(f18,plain,(
% 0.09/0.50 ~e11=e16),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f1])).
% 0.09/0.50 fof(f20,plain,(
% 0.09/0.50 ~e12=e14),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f1])).
% 0.09/0.50 fof(f21,plain,(
% 0.09/0.50 ~e12=e15),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f1])).
% 0.09/0.50 fof(f23,plain,(
% 0.09/0.50 ~e13=e14),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f1])).
% 0.09/0.50 fof(f29,plain,(
% 0.09/0.50 ~e20=e21),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.50 fof(f30,plain,(
% 0.09/0.50 ~e20=e22),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.50 fof(f31,plain,(
% 0.09/0.50 ~e20=e23),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.50 fof(f32,plain,(
% 0.09/0.50 ~e20=e24),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.50 fof(f33,plain,(
% 0.09/0.50 ~e20=e25),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.50 fof(f34,plain,(
% 0.09/0.50 ~e20=e26),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.50 fof(f99,plain,(
% 0.09/0.50 op1(e10,e10)=e13),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.50 fof(f107,plain,(
% 0.09/0.50 op1(e11,e11)=e16),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.50 fof(f115,plain,(
% 0.09/0.50 op1(e12,e12)=e15),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.50 fof(f123,plain,(
% 0.09/0.50 op1(e13,e13)=e14),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.50 fof(f131,plain,(
% 0.09/0.50 op1(e14,e14)=e12),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.50 fof(f139,plain,(
% 0.09/0.50 op1(e15,e15)=e11),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.50 fof(f147,plain,(
% 0.09/0.50 op1(e16,e16)=e10),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.50 fof(f148,plain,(
% 0.09/0.50 op2(e20,e20)=e20),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f5])).
% 0.09/0.50 fof(f156,plain,(
% 0.09/0.50 op2(e21,e21)=e21),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f5])).
% 0.09/0.50 fof(f180,plain,(
% 0.09/0.50 op2(e24,e24)=e24),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f5])).
% 0.09/0.50 fof(f188,plain,(
% 0.09/0.50 op2(e25,e25)=e25),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f5])).
% 0.09/0.50 fof(f197,plain,(
% 0.09/0.50 ((((((((((((((((((((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.09/0.50 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.09/0.50 fof(f201,plain,(
% 0.09/0.50 h(e13)=e20|h(e13)=e21|h(e13)=e22|h(e13)=e23|h(e13)=e24|h(e13)=e25|h(e13)=e26),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f197])).
% 0.09/0.50 fof(f205,plain,(
% 0.09/0.50 j(e20)=e10|j(e20)=e11|j(e20)=e12|j(e20)=e13|j(e20)=e14|j(e20)=e15|j(e20)=e16),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f197])).
% 0.09/0.50 fof(f236,plain,(
% 0.09/0.50 h(op1(e13,e13))=op2(h(e13),h(e13))),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f197])).
% 0.09/0.50 fof(f244,plain,(
% 0.09/0.50 h(op1(e14,e14))=op2(h(e14),h(e14))),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f197])).
% 0.09/0.50 fof(f261,plain,(
% 0.09/0.50 j(op2(e20,e20))=op1(j(e20),j(e20))),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f197])).
% 0.09/0.50 fof(f269,plain,(
% 0.09/0.50 j(op2(e21,e21))=op1(j(e21),j(e21))),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f197])).
% 0.09/0.50 fof(f293,plain,(
% 0.09/0.50 j(op2(e24,e24))=op1(j(e24),j(e24))),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f197])).
% 0.09/0.50 fof(f301,plain,(
% 0.09/0.50 j(op2(e25,e25))=op1(j(e25),j(e25))),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f197])).
% 0.09/0.50 fof(f310,plain,(
% 0.09/0.50 h(j(e20))=e20),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f197])).
% 0.09/0.50 fof(f319,plain,(
% 0.09/0.50 j(h(e12))=e12),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f197])).
% 0.09/0.50 fof(f321,plain,(
% 0.09/0.50 j(h(e14))=e14),
% 0.09/0.50 inference(cnf_transformation,[status(thm)],[f197])).
% 0.09/0.50 fof(f368,definition,(
% 0.09/0.50 sQ14_spl <=> (h(e12)=e20)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f369,plain,(
% 0.09/0.50 h(e12)=e20|~sQ14_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f368])).
% 0.09/0.50 fof(f390,definition,(
% 0.09/0.50 sQ21_spl <=> (h(e13)=e20)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f391,plain,(
% 0.09/0.50 h(e13)=e20|~sQ21_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f390])).
% 0.09/0.50 fof(f393,definition,(
% 0.09/0.50 sQ22_spl <=> (h(e13)=e21)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f394,plain,(
% 0.09/0.50 h(e13)=e21|~sQ22_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f393])).
% 0.09/0.50 fof(f396,definition,(
% 0.09/0.50 sQ23_spl <=> (h(e13)=e22)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f397,plain,(
% 0.09/0.50 h(e13)=e22|~sQ23_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f396])).
% 0.09/0.50 fof(f399,definition,(
% 0.09/0.50 sQ24_spl <=> (h(e13)=e23)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f400,plain,(
% 0.09/0.50 h(e13)=e23|~sQ24_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f399])).
% 0.09/0.50 fof(f402,definition,(
% 0.09/0.50 sQ25_spl <=> (h(e13)=e24)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f403,plain,(
% 0.09/0.50 h(e13)=e24|~sQ25_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f402])).
% 0.09/0.50 fof(f405,definition,(
% 0.09/0.50 sQ26_spl <=> (h(e13)=e25)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f406,plain,(
% 0.09/0.50 h(e13)=e25|~sQ26_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f405])).
% 0.09/0.50 fof(f408,definition,(
% 0.09/0.50 sQ27_spl <=> (h(e13)=e26)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f409,plain,(
% 0.09/0.50 h(e13)=e26|~sQ27_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f408])).
% 0.09/0.50 fof(f411,plain,(
% 0.09/0.50 sQ21_spl|sQ22_spl|sQ23_spl|sQ24_spl|sQ25_spl|sQ26_spl|sQ27_spl),
% 0.09/0.50 inference(split_clause,[status(thm)],[f201,f390,f393,f396,f399,f402,f405,f408])).
% 0.09/0.50 fof(f412,definition,(
% 0.09/0.50 sQ28_spl <=> (h(e14)=e20)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f413,plain,(
% 0.09/0.50 h(e14)=e20|~sQ28_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f412])).
% 0.09/0.50 fof(f427,definition,(
% 0.09/0.50 sQ33_spl <=> (h(e14)=e25)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f428,plain,(
% 0.09/0.50 h(e14)=e25|~sQ33_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f427])).
% 0.09/0.50 fof(f478,definition,(
% 0.09/0.50 sQ49_spl <=> (j(e20)=e10)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f479,plain,(
% 0.09/0.50 j(e20)=e10|~sQ49_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f478])).
% 0.09/0.50 fof(f481,definition,(
% 0.09/0.50 sQ50_spl <=> (j(e20)=e11)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f482,plain,(
% 0.09/0.50 j(e20)=e11|~sQ50_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f481])).
% 0.09/0.50 fof(f484,definition,(
% 0.09/0.50 sQ51_spl <=> (j(e20)=e12)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f485,plain,(
% 0.09/0.50 j(e20)=e12|~sQ51_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f484])).
% 0.09/0.50 fof(f487,definition,(
% 0.09/0.50 sQ52_spl <=> (j(e20)=e13)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f488,plain,(
% 0.09/0.50 j(e20)=e13|~sQ52_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f487])).
% 0.09/0.50 fof(f490,definition,(
% 0.09/0.50 sQ53_spl <=> (j(e20)=e14)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f491,plain,(
% 0.09/0.50 j(e20)=e14|~sQ53_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f490])).
% 0.09/0.50 fof(f493,definition,(
% 0.09/0.50 sQ54_spl <=> (j(e20)=e15)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f494,plain,(
% 0.09/0.50 j(e20)=e15|~sQ54_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f493])).
% 0.09/0.50 fof(f496,definition,(
% 0.09/0.50 sQ55_spl <=> (j(e20)=e16)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f497,plain,(
% 0.09/0.50 j(e20)=e16|~sQ55_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f496])).
% 0.09/0.50 fof(f499,plain,(
% 0.09/0.50 sQ49_spl|sQ50_spl|sQ51_spl|sQ52_spl|sQ53_spl|sQ54_spl|sQ55_spl),
% 0.09/0.50 inference(split_clause,[status(thm)],[f205,f478,f481,f484,f487,f490,f493,f496])).
% 0.09/0.50 fof(f509,definition,(
% 0.09/0.50 sQ59_spl <=> (j(e21)=e13)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f510,plain,(
% 0.09/0.50 j(e21)=e13|~sQ59_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f509])).
% 0.09/0.50 fof(f566,definition,(
% 0.09/0.50 sQ77_spl <=> (j(e24)=e10)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f567,plain,(
% 0.09/0.50 j(e24)=e10|~sQ77_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f566])).
% 0.09/0.50 fof(f581,definition,(
% 0.09/0.50 sQ82_spl <=> (j(e24)=e15)),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f582,plain,(
% 0.09/0.50 j(e24)=e15|~sQ82_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f581])).
% 0.09/0.50 fof(f796,plain,(
% 0.09/0.50 h(e14)=op2(h(e13),h(e13))),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f123,f236])).
% 0.09/0.50 fof(f873,plain,(
% 0.09/0.50 h(e12)=op2(h(e14),h(e14))),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f131,f244])).
% 0.09/0.50 fof(f874,plain,(
% 0.09/0.50 h(e12)=op2(e20,h(e14))|~sQ28_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f413,f873])).
% 0.09/0.50 fof(f875,plain,(
% 0.09/0.50 h(e12)=op2(e20,e20)|~sQ28_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f413,f874])).
% 0.09/0.50 fof(f877,plain,(
% 0.09/0.50 h(e12)=e20|~sQ28_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f148,f875])).
% 0.09/0.50 fof(f996,plain,(
% 0.09/0.50 j(e20)=op1(j(e20),j(e20))),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f148,f261])).
% 0.09/0.50 fof(f997,plain,(
% 0.09/0.50 e10=op1(j(e20),j(e20))|~sQ49_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f479,f996])).
% 0.09/0.50 fof(f998,plain,(
% 0.09/0.50 e10=op1(e10,j(e20))|~sQ49_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f479,f997])).
% 0.09/0.50 fof(f999,plain,(
% 0.09/0.50 e10=e13|~sQ49_spl),
% 0.09/0.50 inference(backward_demodulation,[status(thm)],[f1000,f99])).
% 0.09/0.50 fof(f1000,plain,(
% 0.09/0.50 e10=op1(e10,e10)|~sQ49_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f479,f998])).
% 0.09/0.50 fof(f1001,plain,(
% 0.09/0.50 $false|~sQ49_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f999,f10])).
% 0.09/0.50 fof(f1002,plain,(
% 0.09/0.50 ~sQ49_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f1001])).
% 0.09/0.50 fof(f1040,plain,(
% 0.09/0.50 j(e21)=op1(j(e21),j(e21))),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f156,f269])).
% 0.09/0.50 fof(f1190,plain,(
% 0.09/0.50 j(e24)=op1(j(e24),j(e24))),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f180,f293])).
% 0.09/0.50 fof(f1247,plain,(
% 0.09/0.50 j(e25)=op1(j(e25),j(e25))),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f188,f301])).
% 0.09/0.50 fof(f1338,plain,(
% 0.09/0.50 sQ14_spl|~sQ28_spl),
% 0.09/0.50 inference(split_clause,[status(thm)],[f877,f368,f412])).
% 0.09/0.50 fof(f1353,plain,(
% 0.09/0.50 h(e14)=e20|~sQ53_spl),
% 0.09/0.50 inference(backward_demodulation,[status(thm)],[f491,f310])).
% 0.09/0.50 fof(f1354,plain,(
% 0.09/0.50 sQ28_spl|~sQ53_spl),
% 0.09/0.50 inference(split_clause,[status(thm)],[f1353,f412,f490])).
% 0.09/0.50 fof(f1368,plain,(
% 0.09/0.50 e16=op1(j(e20),j(e20))|~sQ55_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f497,f996])).
% 0.09/0.50 fof(f1369,plain,(
% 0.09/0.50 e16=op1(e16,j(e20))|~sQ55_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f497,f1368])).
% 0.09/0.50 fof(f1370,plain,(
% 0.09/0.50 e16=op1(e16,e16)|~sQ55_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f497,f1369])).
% 0.09/0.50 fof(f1371,plain,(
% 0.09/0.50 e16=e10|~sQ55_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f147,f1370])).
% 0.09/0.50 fof(f1372,plain,(
% 0.09/0.50 $false|~sQ55_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1371,f13])).
% 0.09/0.50 fof(f1373,plain,(
% 0.09/0.50 ~sQ55_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f1372])).
% 0.09/0.50 fof(f1645,plain,(
% 0.09/0.50 e15=op1(j(e20),j(e20))|~sQ54_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f494,f996])).
% 0.09/0.50 fof(f1646,plain,(
% 0.09/0.50 e15=op1(e15,j(e20))|~sQ54_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f494,f1645])).
% 0.09/0.50 fof(f1647,plain,(
% 0.09/0.50 e15=op1(e15,e15)|~sQ54_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f494,f1646])).
% 0.09/0.50 fof(f1648,plain,(
% 0.09/0.50 e15=e11|~sQ54_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f139,f1647])).
% 0.09/0.50 fof(f1649,plain,(
% 0.09/0.50 $false|~sQ54_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1648,f17])).
% 0.09/0.50 fof(f1650,plain,(
% 0.09/0.50 ~sQ54_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f1649])).
% 0.09/0.50 fof(f1902,plain,(
% 0.09/0.50 e11=op1(j(e20),j(e20))|~sQ50_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f482,f996])).
% 0.09/0.50 fof(f1903,plain,(
% 0.09/0.50 e11=op1(e11,j(e20))|~sQ50_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f482,f1902])).
% 0.09/0.50 fof(f1904,plain,(
% 0.09/0.50 e11=e16|~sQ50_spl),
% 0.09/0.50 inference(backward_demodulation,[status(thm)],[f1905,f107])).
% 0.09/0.50 fof(f1905,plain,(
% 0.09/0.50 e11=op1(e11,e11)|~sQ50_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f482,f1903])).
% 0.09/0.50 fof(f1906,plain,(
% 0.09/0.50 $false|~sQ50_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1904,f18])).
% 0.09/0.50 fof(f1907,plain,(
% 0.09/0.50 ~sQ50_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f1906])).
% 0.09/0.50 fof(f1957,plain,(
% 0.09/0.50 h(e14)=op2(h(e13),e20)|~sQ21_spl),
% 0.09/0.50 inference(backward_demodulation,[status(thm)],[f391,f796])).
% 0.09/0.50 fof(f1959,plain,(
% 0.09/0.50 h(e14)=op2(e20,e20)|~sQ21_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f391,f1957])).
% 0.09/0.50 fof(f1960,plain,(
% 0.09/0.50 h(e14)=e20|~sQ21_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f148,f1959])).
% 0.09/0.50 fof(f2083,plain,(
% 0.09/0.50 j(e20)=e12|~sQ14_spl),
% 0.09/0.50 inference(backward_demodulation,[status(thm)],[f369,f319])).
% 0.09/0.50 fof(f2086,plain,(
% 0.09/0.50 e12=op1(j(e20),j(e20))|~sQ51_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f485,f996])).
% 0.09/0.50 fof(f2087,plain,(
% 0.09/0.50 e12=op1(e12,j(e20))|~sQ51_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f485,f2086])).
% 0.09/0.50 fof(f2088,plain,(
% 0.09/0.50 e12=e15|~sQ51_spl),
% 0.09/0.50 inference(backward_demodulation,[status(thm)],[f2089,f115])).
% 0.09/0.50 fof(f2089,plain,(
% 0.09/0.50 e12=op1(e12,e12)|~sQ51_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f485,f2087])).
% 0.09/0.50 fof(f2090,plain,(
% 0.09/0.50 $false|~sQ51_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2088,f21])).
% 0.09/0.50 fof(f2091,plain,(
% 0.09/0.50 ~sQ51_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f2090])).
% 0.09/0.50 fof(f2092,plain,(
% 0.09/0.50 sQ51_spl|~sQ14_spl),
% 0.09/0.50 inference(split_clause,[status(thm)],[f2083,f484,f368])).
% 0.09/0.50 fof(f2119,plain,(
% 0.09/0.50 e10=op1(j(e24),j(e24))|~sQ77_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f567,f1190])).
% 0.09/0.50 fof(f2120,plain,(
% 0.09/0.50 e10=op1(e10,j(e24))|~sQ77_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f567,f2119])).
% 0.09/0.50 fof(f2121,plain,(
% 0.09/0.50 e10=e13|~sQ77_spl),
% 0.09/0.50 inference(backward_demodulation,[status(thm)],[f2122,f99])).
% 0.09/0.50 fof(f2122,plain,(
% 0.09/0.50 e10=op1(e10,e10)|~sQ77_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f567,f2120])).
% 0.09/0.50 fof(f2123,plain,(
% 0.09/0.50 $false|~sQ77_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2121,f10])).
% 0.09/0.50 fof(f2124,plain,(
% 0.09/0.50 ~sQ77_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f2123])).
% 0.09/0.50 fof(f2191,plain,(
% 0.09/0.50 sQ28_spl|~sQ21_spl),
% 0.09/0.50 inference(split_clause,[status(thm)],[f1960,f412,f390])).
% 0.09/0.50 fof(f2215,plain,(
% 0.09/0.50 j(e25)=e14|~sQ33_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f428,f321])).
% 0.09/0.50 fof(f2249,plain,(
% 0.09/0.50 e13=op1(j(e21),j(e21))|~sQ59_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f510,f1040])).
% 0.09/0.50 fof(f2250,plain,(
% 0.09/0.50 e13=op1(e13,j(e21))|~sQ59_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f510,f2249])).
% 0.09/0.50 fof(f2251,plain,(
% 0.09/0.50 e13=e14|~sQ59_spl),
% 0.09/0.50 inference(backward_demodulation,[status(thm)],[f2252,f123])).
% 0.09/0.50 fof(f2252,plain,(
% 0.09/0.50 e13=op1(e13,e13)|~sQ59_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f510,f2250])).
% 0.09/0.50 fof(f2253,plain,(
% 0.09/0.50 $false|~sQ59_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2251,f23])).
% 0.09/0.50 fof(f2254,plain,(
% 0.09/0.50 ~sQ59_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f2253])).
% 0.09/0.50 fof(f2279,plain,(
% 0.09/0.50 e14=op1(j(e25),j(e25))|~sQ33_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f2215,f1247])).
% 0.09/0.50 fof(f2280,plain,(
% 0.09/0.50 e14=op1(e14,j(e25))|~sQ33_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f2215,f2279])).
% 0.09/0.50 fof(f2281,plain,(
% 0.09/0.50 e14=op1(e14,e14)|~sQ33_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f2215,f2280])).
% 0.09/0.50 fof(f2282,plain,(
% 0.09/0.50 e14=e12|~sQ33_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f131,f2281])).
% 0.09/0.50 fof(f2283,plain,(
% 0.09/0.50 $false|~sQ33_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2282,f20])).
% 0.09/0.50 fof(f2284,plain,(
% 0.09/0.50 ~sQ33_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f2283])).
% 0.09/0.50 fof(f2300,plain,(
% 0.09/0.50 h(e13)=e20|~sQ52_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f488,f310])).
% 0.09/0.50 fof(f2319,plain,(
% 0.09/0.50 e15=op1(j(e24),j(e24))|~sQ82_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f582,f1190])).
% 0.09/0.50 fof(f2320,plain,(
% 0.09/0.50 e15=op1(e15,j(e24))|~sQ82_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f582,f2319])).
% 0.09/0.50 fof(f2321,plain,(
% 0.09/0.50 e15=op1(e15,e15)|~sQ82_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f582,f2320])).
% 0.09/0.50 fof(f2322,plain,(
% 0.09/0.50 e15=e11|~sQ82_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f139,f2321])).
% 0.09/0.50 fof(f2323,plain,(
% 0.09/0.50 $false|~sQ82_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2322,f17])).
% 0.09/0.50 fof(f2324,plain,(
% 0.09/0.50 ~sQ82_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f2323])).
% 0.09/0.50 fof(f2343,plain,(
% 0.09/0.50 e20=e24|~sQ52_spl|~sQ25_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f2300,f403])).
% 0.09/0.50 fof(f2344,plain,(
% 0.09/0.50 $false|~sQ52_spl|~sQ25_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2343,f32])).
% 0.09/0.50 fof(f2345,plain,(
% 0.09/0.50 ~sQ52_spl|~sQ25_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f2344])).
% 0.09/0.50 fof(f2355,plain,(
% 0.09/0.50 e20=e26|~sQ52_spl|~sQ27_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f2300,f409])).
% 0.09/0.50 fof(f2356,plain,(
% 0.09/0.50 $false|~sQ52_spl|~sQ27_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2355,f34])).
% 0.09/0.50 fof(f2357,plain,(
% 0.09/0.50 ~sQ52_spl|~sQ27_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f2356])).
% 0.09/0.50 fof(f2359,plain,(
% 0.09/0.50 e20=e21|~sQ52_spl|~sQ22_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f2300,f394])).
% 0.09/0.50 fof(f2360,plain,(
% 0.09/0.50 $false|~sQ52_spl|~sQ22_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2359,f29])).
% 0.09/0.50 fof(f2361,plain,(
% 0.09/0.50 ~sQ52_spl|~sQ22_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f2360])).
% 0.09/0.50 fof(f2362,plain,(
% 0.09/0.50 e20=e22|~sQ52_spl|~sQ23_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f2300,f397])).
% 0.09/0.50 fof(f2363,plain,(
% 0.09/0.50 $false|~sQ52_spl|~sQ23_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2362,f30])).
% 0.09/0.50 fof(f2364,plain,(
% 0.09/0.50 ~sQ52_spl|~sQ23_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f2363])).
% 0.09/0.50 fof(f2365,plain,(
% 0.09/0.50 e20=e23|~sQ52_spl|~sQ24_spl),
% 0.09/0.51 inference(forward_demodulation,[status(thm)],[f2300,f400])).
% 0.09/0.51 fof(f2366,plain,(
% 0.09/0.51 $false|~sQ52_spl|~sQ24_spl),
% 0.09/0.51 inference(forward_subsumption_resolution,[status(thm)],[f2365,f31])).
% 0.09/0.51 fof(f2367,plain,(
% 0.09/0.51 ~sQ52_spl|~sQ24_spl),
% 0.09/0.51 inference(contradiction_clause,[status(thm)],[f2366])).
% 0.09/0.51 fof(f2368,plain,(
% 0.09/0.51 e20=e25|~sQ52_spl|~sQ26_spl),
% 0.09/0.51 inference(forward_demodulation,[status(thm)],[f2300,f406])).
% 0.09/0.51 fof(f2369,plain,(
% 0.09/0.51 $false|~sQ52_spl|~sQ26_spl),
% 0.09/0.51 inference(forward_subsumption_resolution,[status(thm)],[f2368,f33])).
% 0.09/0.51 fof(f2370,plain,(
% 0.09/0.51 ~sQ52_spl|~sQ26_spl),
% 0.09/0.51 inference(contradiction_clause,[status(thm)],[f2369])).
% 0.09/0.51 fof(f2371,plain,(
% 0.09/0.51 $false),
% 0.09/0.51 inference(sat_refutation,[status(thm)],[f411,f499,f1002,f1338,f1354,f1373,f1650,f1907,f2091,f2092,f2124,f2191,f2254,f2284,f2324,f2345,f2357,f2361,f2364,f2367,f2370])).
% 0.09/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.51 % Elapsed time: 0.139090 seconds
% 0.09/0.51 % CPU time: 0.769506 seconds
% 0.09/0.51 % Total memory used: 133.567 MB
% 0.09/0.51 % Net memory used: 133.247 MB
%------------------------------------------------------------------------------