%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG205+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 : n009.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.10s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG205+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.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 13:01:27 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.49 % Refutation found
% 0.10/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.49 fof(f1,axiom,(
% 0.10/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.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f4,axiom,(
% 0.10/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.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f5,axiom,(
% 0.10/0.49 ( 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.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f6,conjecture,(
% 0.10/0.49 ( ( ( 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.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f7,negated_conjecture,(
% 0.10/0.49 ~(( ( ( 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.10/0.49 inference(negated_conjecture,[status(cth)],[f6])).
% 0.10/0.49 fof(f13,plain,(
% 0.10/0.49 ~e10=e16),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f1])).
% 0.10/0.49 fof(f17,plain,(
% 0.10/0.49 ~e11=e15),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f1])).
% 0.10/0.49 fof(f20,plain,(
% 0.10/0.49 ~e12=e14),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f1])).
% 0.10/0.49 fof(f99,plain,(
% 0.10/0.49 op1(e10,e10)=e13),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f107,plain,(
% 0.10/0.49 op1(e11,e11)=e16),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f115,plain,(
% 0.10/0.49 op1(e12,e12)=e15),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f123,plain,(
% 0.10/0.49 op1(e13,e13)=e14),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f131,plain,(
% 0.10/0.49 op1(e14,e14)=e12),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f139,plain,(
% 0.10/0.49 op1(e15,e15)=e11),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f147,plain,(
% 0.10/0.49 op1(e16,e16)=e10),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f180,plain,(
% 0.10/0.49 op2(e24,e24)=e24),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.49 fof(f197,plain,(
% 0.10/0.49 ((((((((((((((((((((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.10/0.49 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.10/0.49 fof(f209,plain,(
% 0.10/0.49 j(e24)=e10|j(e24)=e11|j(e24)=e12|j(e24)=e13|j(e24)=e14|j(e24)=e15|j(e24)=e16),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f197])).
% 0.10/0.49 fof(f212,plain,(
% 0.10/0.49 h(op1(e10,e10))=op2(h(e10),h(e10))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f197])).
% 0.10/0.49 fof(f220,plain,(
% 0.10/0.49 h(op1(e11,e11))=op2(h(e11),h(e11))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f197])).
% 0.10/0.49 fof(f228,plain,(
% 0.10/0.49 h(op1(e12,e12))=op2(h(e12),h(e12))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f197])).
% 0.10/0.49 fof(f236,plain,(
% 0.10/0.49 h(op1(e13,e13))=op2(h(e13),h(e13))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f197])).
% 0.10/0.49 fof(f260,plain,(
% 0.10/0.49 h(op1(e16,e16))=op2(h(e16),h(e16))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f197])).
% 0.10/0.49 fof(f293,plain,(
% 0.10/0.49 j(op2(e24,e24))=op1(j(e24),j(e24))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f197])).
% 0.10/0.49 fof(f314,plain,(
% 0.10/0.49 h(j(e24))=e24),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f197])).
% 0.10/0.49 fof(f321,plain,(
% 0.10/0.49 j(h(e14))=e14),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f197])).
% 0.10/0.49 fof(f322,plain,(
% 0.10/0.49 j(h(e15))=e15),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f197])).
% 0.10/0.49 fof(f336,definition,(
% 0.10/0.49 sQ4_spl <=> (h(e10)=e24)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f337,plain,(
% 0.10/0.49 h(e10)=e24|~sQ4_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f336])).
% 0.10/0.49 fof(f338,plain,(
% 0.10/0.49 ~h(e10)=e24|sQ4_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f336])).
% 0.10/0.49 fof(f358,definition,(
% 0.10/0.49 sQ11_spl <=> (h(e11)=e24)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f359,plain,(
% 0.10/0.49 h(e11)=e24|~sQ11_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f358])).
% 0.10/0.49 fof(f380,definition,(
% 0.10/0.49 sQ18_spl <=> (h(e12)=e24)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f381,plain,(
% 0.10/0.49 h(e12)=e24|~sQ18_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f380])).
% 0.10/0.49 fof(f402,definition,(
% 0.10/0.49 sQ25_spl <=> (h(e13)=e24)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f403,plain,(
% 0.10/0.49 h(e13)=e24|~sQ25_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f402])).
% 0.10/0.49 fof(f404,plain,(
% 0.10/0.49 ~h(e13)=e24|sQ25_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f402])).
% 0.10/0.49 fof(f424,definition,(
% 0.10/0.49 sQ32_spl <=> (h(e14)=e24)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f425,plain,(
% 0.10/0.49 h(e14)=e24|~sQ32_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f424])).
% 0.10/0.49 fof(f426,plain,(
% 0.10/0.49 ~h(e14)=e24|sQ32_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f424])).
% 0.10/0.49 fof(f446,definition,(
% 0.10/0.49 sQ39_spl <=> (h(e15)=e24)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f447,plain,(
% 0.10/0.49 h(e15)=e24|~sQ39_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f446])).
% 0.10/0.49 fof(f448,plain,(
% 0.10/0.49 ~h(e15)=e24|sQ39_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f446])).
% 0.10/0.49 fof(f468,definition,(
% 0.10/0.49 sQ46_spl <=> (h(e16)=e24)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f469,plain,(
% 0.10/0.49 h(e16)=e24|~sQ46_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f468])).
% 0.10/0.49 fof(f470,plain,(
% 0.10/0.49 ~h(e16)=e24|sQ46_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f468])).
% 0.10/0.49 fof(f566,definition,(
% 0.10/0.49 sQ77_spl <=> (j(e24)=e10)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f567,plain,(
% 0.10/0.49 j(e24)=e10|~sQ77_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f566])).
% 0.10/0.49 fof(f569,definition,(
% 0.10/0.49 sQ78_spl <=> (j(e24)=e11)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f570,plain,(
% 0.10/0.49 j(e24)=e11|~sQ78_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f569])).
% 0.10/0.49 fof(f572,definition,(
% 0.10/0.49 sQ79_spl <=> (j(e24)=e12)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f573,plain,(
% 0.10/0.49 j(e24)=e12|~sQ79_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f572])).
% 0.10/0.49 fof(f575,definition,(
% 0.10/0.49 sQ80_spl <=> (j(e24)=e13)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f576,plain,(
% 0.10/0.49 j(e24)=e13|~sQ80_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f575])).
% 0.10/0.49 fof(f578,definition,(
% 0.10/0.49 sQ81_spl <=> (j(e24)=e14)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f579,plain,(
% 0.10/0.49 j(e24)=e14|~sQ81_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f578])).
% 0.10/0.49 fof(f581,definition,(
% 0.10/0.49 sQ82_spl <=> (j(e24)=e15)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f582,plain,(
% 0.10/0.49 j(e24)=e15|~sQ82_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f581])).
% 0.10/0.49 fof(f584,definition,(
% 0.10/0.49 sQ83_spl <=> (j(e24)=e16)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f585,plain,(
% 0.10/0.49 j(e24)=e16|~sQ83_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f584])).
% 0.10/0.50 fof(f587,plain,(
% 0.10/0.50 sQ77_spl|sQ78_spl|sQ79_spl|sQ80_spl|sQ81_spl|sQ82_spl|sQ83_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f209,f566,f569,f572,f575,f578,f581,f584])).
% 0.10/0.50 fof(f648,plain,(
% 0.10/0.50 h(e13)=op2(h(e10),h(e10))),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f99,f212])).
% 0.10/0.50 fof(f661,plain,(
% 0.10/0.50 h(e16)=op2(h(e11),h(e11))),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f107,f220])).
% 0.10/0.50 fof(f708,plain,(
% 0.10/0.50 h(e15)=op2(h(e12),h(e12))),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f115,f228])).
% 0.10/0.50 fof(f804,plain,(
% 0.10/0.50 h(e14)=op2(h(e13),h(e13))),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f123,f236])).
% 0.10/0.50 fof(f1021,plain,(
% 0.10/0.50 h(e10)=op2(h(e16),h(e16))),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f147,f260])).
% 0.10/0.50 fof(f1192,plain,(
% 0.10/0.50 j(e24)=op1(j(e24),j(e24))),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f180,f293])).
% 0.10/0.50 fof(f1410,plain,(
% 0.10/0.50 h(e12)=e24|~sQ79_spl),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f573,f314])).
% 0.10/0.50 fof(f1411,plain,(
% 0.10/0.50 sQ18_spl|~sQ79_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f1410,f380,f572])).
% 0.10/0.50 fof(f1668,plain,(
% 0.10/0.50 h(e13)=e24|~sQ80_spl),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f576,f314])).
% 0.10/0.50 fof(f1672,plain,(
% 0.10/0.50 sQ25_spl|~sQ80_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f1668,f402,f575])).
% 0.10/0.50 fof(f1834,plain,(
% 0.10/0.50 h(e14)=op2(h(e13),e24)|~sQ25_spl),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f403,f804])).
% 0.10/0.50 fof(f1836,plain,(
% 0.10/0.50 h(e14)=op2(e24,e24)|~sQ25_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f403,f1834])).
% 0.10/0.50 fof(f1837,plain,(
% 0.10/0.50 h(e14)=e24|~sQ25_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f180,f1836])).
% 0.10/0.50 fof(f1838,plain,(
% 0.10/0.50 $false|sQ32_spl|~sQ25_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1837,f426])).
% 0.10/0.50 fof(f1839,plain,(
% 0.10/0.50 sQ32_spl|~sQ25_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f1838])).
% 0.10/0.50 fof(f1922,plain,(
% 0.10/0.50 h(e10)=e24|~sQ77_spl),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f567,f314])).
% 0.10/0.50 fof(f1933,plain,(
% 0.10/0.50 sQ4_spl|~sQ77_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f1922,f336,f566])).
% 0.10/0.50 fof(f2386,plain,(
% 0.10/0.50 h(e11)=e24|~sQ78_spl),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f570,f314])).
% 0.10/0.50 fof(f2388,plain,(
% 0.10/0.50 sQ11_spl|~sQ78_spl),
% 0.10/0.50 inference(split_clause,[status(thm)],[f2386,f358,f569])).
% 0.10/0.50 fof(f2647,plain,(
% 0.10/0.50 j(e24)=e14|~sQ32_spl),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f425,f321])).
% 0.10/0.50 fof(f2676,plain,(
% 0.10/0.50 j(e24)=op1(j(e24),e14)|~sQ81_spl),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f579,f1192])).
% 0.10/0.50 fof(f2682,plain,(
% 0.10/0.50 e14=op1(j(e24),e14)|~sQ81_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f579,f2676])).
% 0.10/0.50 fof(f2683,plain,(
% 0.10/0.50 e14=op1(e14,e14)|~sQ81_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f579,f2682])).
% 0.10/0.50 fof(f2684,plain,(
% 0.10/0.50 e14=e12|~sQ81_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f131,f2683])).
% 0.10/0.50 fof(f2685,plain,(
% 0.10/0.50 $false|~sQ81_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2684,f20])).
% 0.10/0.50 fof(f2686,plain,(
% 0.10/0.50 ~sQ81_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f2685])).
% 0.10/0.50 fof(f2788,plain,(
% 0.10/0.50 h(e13)=op2(h(e10),e24)|~sQ4_spl),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f337,f648])).
% 0.10/0.50 fof(f2796,plain,(
% 0.10/0.50 h(e13)=op2(e24,e24)|~sQ4_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f337,f2788])).
% 0.10/0.50 fof(f2797,plain,(
% 0.10/0.50 h(e13)=e24|~sQ4_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f180,f2796])).
% 0.10/0.50 fof(f2798,plain,(
% 0.10/0.50 $false|sQ25_spl|~sQ4_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2797,f404])).
% 0.10/0.50 fof(f2799,plain,(
% 0.10/0.50 sQ25_spl|~sQ4_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f2798])).
% 0.10/0.50 fof(f2916,plain,(
% 0.10/0.50 h(e10)=op2(h(e16),e24)|~sQ46_spl),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f469,f1021])).
% 0.10/0.50 fof(f2919,plain,(
% 0.10/0.50 h(e10)=op2(e24,e24)|~sQ46_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f469,f2916])).
% 0.10/0.50 fof(f2920,plain,(
% 0.10/0.50 h(e10)=e24|~sQ46_spl),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f180,f2919])).
% 0.10/0.50 fof(f2921,plain,(
% 0.10/0.50 $false|sQ4_spl|~sQ46_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2920,f338])).
% 0.10/0.50 fof(f2922,plain,(
% 0.10/0.50 sQ4_spl|~sQ46_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f2921])).
% 0.10/0.51 fof(f2976,plain,(
% 0.10/0.51 j(e24)=op1(j(e24),e16)|~sQ83_spl),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f585,f1192])).
% 0.10/0.51 fof(f2981,plain,(
% 0.10/0.51 e16=op1(j(e24),e16)|~sQ83_spl),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f585,f2976])).
% 0.10/0.51 fof(f2982,plain,(
% 0.10/0.51 e16=op1(e16,e16)|~sQ83_spl),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f585,f2981])).
% 0.10/0.51 fof(f2983,plain,(
% 0.10/0.51 e16=e10|~sQ83_spl),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f147,f2982])).
% 0.10/0.51 fof(f2984,plain,(
% 0.10/0.51 $false|~sQ83_spl),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f2983,f13])).
% 0.10/0.51 fof(f2985,plain,(
% 0.10/0.51 ~sQ83_spl),
% 0.10/0.51 inference(contradiction_clause,[status(thm)],[f2984])).
% 0.10/0.51 fof(f3098,plain,(
% 0.10/0.51 j(e24)=e15|~sQ39_spl),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f447,f322])).
% 0.10/0.51 fof(f3105,plain,(
% 0.10/0.51 sQ82_spl|~sQ39_spl),
% 0.10/0.51 inference(split_clause,[status(thm)],[f3098,f581,f446])).
% 0.10/0.51 fof(f3183,plain,(
% 0.10/0.51 h(e16)=op2(e24,h(e11))|~sQ11_spl),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f359,f661])).
% 0.10/0.51 fof(f3184,plain,(
% 0.10/0.51 h(e16)=op2(e24,e24)|~sQ11_spl),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f359,f3183])).
% 0.10/0.51 fof(f3185,plain,(
% 0.10/0.51 h(e16)=e24|~sQ11_spl),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f180,f3184])).
% 0.10/0.51 fof(f3186,plain,(
% 0.10/0.51 $false|sQ46_spl|~sQ11_spl),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f3185,f470])).
% 0.10/0.51 fof(f3187,plain,(
% 0.10/0.51 sQ46_spl|~sQ11_spl),
% 0.10/0.51 inference(contradiction_clause,[status(thm)],[f3186])).
% 0.10/0.51 fof(f3230,plain,(
% 0.10/0.51 j(e24)=op1(j(e24),e15)|~sQ82_spl),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f582,f1192])).
% 0.10/0.51 fof(f3237,plain,(
% 0.10/0.51 e15=op1(j(e24),e15)|~sQ82_spl),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f582,f3230])).
% 0.10/0.51 fof(f3238,plain,(
% 0.10/0.51 e15=op1(e15,e15)|~sQ82_spl),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f582,f3237])).
% 0.10/0.51 fof(f3239,plain,(
% 0.10/0.51 e15=e11|~sQ82_spl),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f139,f3238])).
% 0.10/0.51 fof(f3240,plain,(
% 0.10/0.51 $false|~sQ82_spl),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f3239,f17])).
% 0.10/0.51 fof(f3241,plain,(
% 0.10/0.51 ~sQ82_spl),
% 0.10/0.51 inference(contradiction_clause,[status(thm)],[f3240])).
% 0.10/0.51 fof(f3279,plain,(
% 0.10/0.51 sQ81_spl|~sQ32_spl),
% 0.10/0.51 inference(split_clause,[status(thm)],[f2647,f578,f424])).
% 0.10/0.51 fof(f3303,plain,(
% 0.10/0.51 h(e15)=op2(h(e12),e24)|~sQ18_spl),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f381,f708])).
% 0.10/0.51 fof(f3307,plain,(
% 0.10/0.51 h(e15)=op2(e24,e24)|~sQ18_spl),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f381,f3303])).
% 0.10/0.51 fof(f3308,plain,(
% 0.10/0.51 h(e15)=e24|~sQ18_spl),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f180,f3307])).
% 0.10/0.51 fof(f3309,plain,(
% 0.10/0.51 $false|sQ39_spl|~sQ18_spl),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f3308,f448])).
% 0.10/0.51 fof(f3310,plain,(
% 0.10/0.51 sQ39_spl|~sQ18_spl),
% 0.10/0.51 inference(contradiction_clause,[status(thm)],[f3309])).
% 0.10/0.51 fof(f3311,plain,(
% 0.10/0.51 $false),
% 0.10/0.51 inference(sat_refutation,[status(thm)],[f587,f1411,f1672,f1839,f1933,f2388,f2686,f2799,f2922,f2985,f3105,f3187,f3241,f3279,f3310])).
% 0.10/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.52 % Elapsed time: 0.156198 seconds
% 0.10/0.52 % CPU time: 0.853140 seconds
% 0.10/0.52 % Total memory used: 135.143 MB
% 0.10/0.52 % Net memory used: 134.853 MB
%------------------------------------------------------------------------------