%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG065+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 : n015.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:33 AM UTC 2026
% Result : Theorem 0.09s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG065+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 : n015.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 12:58:23 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.45 % Refutation found
% 0.09/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.45 fof(f1,axiom,(
% 0.09/0.45 ( ( op(e0,e0) = e0| op(e0,e0) = e1| op(e0,e0) = e2| op(e0,e0) = e3| op(e0,e0) = e4 )& ( op(e0,e1) = e0| op(e0,e1) = e1| op(e0,e1) = e2| op(e0,e1) = e3| op(e0,e1) = e4 )& ( op(e0,e2) = e0| op(e0,e2) = e1| op(e0,e2) = e2| op(e0,e2) = e3| op(e0,e2) = e4 )& ( op(e0,e3) = e0| op(e0,e3) = e1| op(e0,e3) = e2| op(e0,e3) = e3| op(e0,e3) = e4 )& ( op(e0,e4) = e0| op(e0,e4) = e1| op(e0,e4) = e2| op(e0,e4) = e3| op(e0,e4) = e4 )& ( op(e1,e0) = e0| op(e1,e0) = e1| op(e1,e0) = e2| op(e1,e0) = e3| op(e1,e0) = e4 )& ( op(e1,e1) = e0| op(e1,e1) = e1| op(e1,e1) = e2| op(e1,e1) = e3| op(e1,e1) = e4 )& ( op(e1,e2) = e0| op(e1,e2) = e1| op(e1,e2) = e2| op(e1,e2) = e3| op(e1,e2) = e4 )& ( op(e1,e3) = e0| op(e1,e3) = e1| op(e1,e3) = e2| op(e1,e3) = e3| op(e1,e3) = e4 )& ( op(e1,e4) = e0| op(e1,e4) = e1| op(e1,e4) = e2| op(e1,e4) = e3| op(e1,e4) = e4 )& ( op(e2,e0) = e0| op(e2,e0) = e1| op(e2,e0) = e2| op(e2,e0) = e3| op(e2,e0) = e4 )& ( op(e2,e1) = e0| op(e2,e1) = e1| op(e2,e1) = e2| op(e2,e1) = e3| op(e2,e1) = e4 )& ( op(e2,e2) = e0| op(e2,e2) = e1| op(e2,e2) = e2| op(e2,e2) = e3| op(e2,e2) = e4 )& ( op(e2,e3) = e0| op(e2,e3) = e1| op(e2,e3) = e2| op(e2,e3) = e3| op(e2,e3) = e4 )& ( op(e2,e4) = e0| op(e2,e4) = e1| op(e2,e4) = e2| op(e2,e4) = e3| op(e2,e4) = e4 )& ( op(e3,e0) = e0| op(e3,e0) = e1| op(e3,e0) = e2| op(e3,e0) = e3| op(e3,e0) = e4 )& ( op(e3,e1) = e0| op(e3,e1) = e1| op(e3,e1) = e2| op(e3,e1) = e3| op(e3,e1) = e4 )& ( op(e3,e2) = e0| op(e3,e2) = e1| op(e3,e2) = e2| op(e3,e2) = e3| op(e3,e2) = e4 )& ( op(e3,e3) = e0| op(e3,e3) = e1| op(e3,e3) = e2| op(e3,e3) = e3| op(e3,e3) = e4 )& ( op(e3,e4) = e0| op(e3,e4) = e1| op(e3,e4) = e2| op(e3,e4) = e3| op(e3,e4) = e4 )& ( op(e4,e0) = e0| op(e4,e0) = e1| op(e4,e0) = e2| op(e4,e0) = e3| op(e4,e0) = e4 )& ( op(e4,e1) = e0| op(e4,e1) = e1| op(e4,e1) = e2| op(e4,e1) = e3| op(e4,e1) = e4 )& ( op(e4,e2) = e0| op(e4,e2) = e1| op(e4,e2) = e2| op(e4,e2) = e3| op(e4,e2) = e4 )& ( op(e4,e3) = e0| op(e4,e3) = e1| op(e4,e3) = e2| op(e4,e3) = e3| op(e4,e3) = e4 )& ( op(e4,e4) = e0| op(e4,e4) = e1| op(e4,e4) = e2| op(e4,e4) = e3| op(e4,e4) = e4 ) ) ),
% 0.09/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f2,axiom,(
% 0.09/0.45 ( op(unit,e0) = e0& op(e0,unit) = e0& op(unit,e1) = e1& op(e1,unit) = e1& op(unit,e2) = e2& op(e2,unit) = e2& op(unit,e3) = e3& op(e3,unit) = e3& op(unit,e4) = e4& op(e4,unit) = e4& ( unit = e0| unit = e1| unit = e2| unit = e3| unit = e4 ) ) ),
% 0.09/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f3,axiom,(
% 0.09/0.45 ( ( op(e0,e0) = e0| op(e0,e1) = e0| op(e0,e2) = e0| op(e0,e3) = e0| op(e0,e4) = e0 )& ( op(e0,e0) = e0| op(e1,e0) = e0| op(e2,e0) = e0| op(e3,e0) = e0| op(e4,e0) = e0 )& ( op(e0,e0) = e1| op(e0,e1) = e1| op(e0,e2) = e1| op(e0,e3) = e1| op(e0,e4) = e1 )& ( op(e0,e0) = e1| op(e1,e0) = e1| op(e2,e0) = e1| op(e3,e0) = e1| op(e4,e0) = e1 )& ( op(e0,e0) = e2| op(e0,e1) = e2| op(e0,e2) = e2| op(e0,e3) = e2| op(e0,e4) = e2 )& ( op(e0,e0) = e2| op(e1,e0) = e2| op(e2,e0) = e2| op(e3,e0) = e2| op(e4,e0) = e2 )& ( op(e0,e0) = e3| op(e0,e1) = e3| op(e0,e2) = e3| op(e0,e3) = e3| op(e0,e4) = e3 )& ( op(e0,e0) = e3| op(e1,e0) = e3| op(e2,e0) = e3| op(e3,e0) = e3| op(e4,e0) = e3 )& ( op(e0,e0) = e4| op(e0,e1) = e4| op(e0,e2) = e4| op(e0,e3) = e4| op(e0,e4) = e4 )& ( op(e0,e0) = e4| op(e1,e0) = e4| op(e2,e0) = e4| op(e3,e0) = e4| op(e4,e0) = e4 )& ( op(e1,e0) = e0| op(e1,e1) = e0| op(e1,e2) = e0| op(e1,e3) = e0| op(e1,e4) = e0 )& ( op(e0,e1) = e0| op(e1,e1) = e0| op(e2,e1) = e0| op(e3,e1) = e0| op(e4,e1) = e0 )& ( op(e1,e0) = e1| op(e1,e1) = e1| op(e1,e2) = e1| op(e1,e3) = e1| op(e1,e4) = e1 )& ( op(e0,e1) = e1| op(e1,e1) = e1| op(e2,e1) = e1| op(e3,e1) = e1| op(e4,e1) = e1 )& ( op(e1,e0) = e2| op(e1,e1) = e2| op(e1,e2) = e2| op(e1,e3) = e2| op(e1,e4) = e2 )& ( op(e0,e1) = e2| op(e1,e1) = e2| op(e2,e1) = e2| op(e3,e1) = e2| op(e4,e1) = e2 )& ( op(e1,e0) = e3| op(e1,e1) = e3| op(e1,e2) = e3| op(e1,e3) = e3| op(e1,e4) = e3 )& ( op(e0,e1) = e3| op(e1,e1) = e3| op(e2,e1) = e3| op(e3,e1) = e3| op(e4,e1) = e3 )& ( op(e1,e0) = e4| op(e1,e1) = e4| op(e1,e2) = e4| op(e1,e3) = e4| op(e1,e4) = e4 )& ( op(e0,e1) = e4| op(e1,e1) = e4| op(e2,e1) = e4| op(e3,e1) = e4| op(e4,e1) = e4 )& ( op(e2,e0) = e0| op(e2,e1) = e0| op(e2,e2) = e0| op(e2,e3) = e0| op(e2,e4) = e0 )& ( op(e0,e2) = e0| op(e1,e2) = e0| op(e2,e2) = e0| op(e3,e2) = e0| op(e4,e2) = e0 )& ( op(e2,e0) = e1| op(e2,e1) = e1| op(e2,e2) = e1| op(e2,e3) = e1| op(e2,e4) = e1 )& ( op(e0,e2) = e1| op(e1,e2) = e1| op(e2,e2) = e1| op(e3,e2) = e1| op(e4,e2) = e1 )& ( op(e2,e0) = e2| op(e2,e1) = e2| op(e2,e2) = e2| op(e2,e3) = e2| op(e2,e4) = e2 )& ( op(e0,e2) = e2| op(e1,e2) = e2| op(e2,e2) = e2| op(e3,e2) = e2| op(e4,e2) = e2 )& ( op(e2,e0) = e3| op(e2,e1) = e3| op(e2,e2) = e3| op(e2,e3) = e3| op(e2,e4) = e3 )& ( op(e0,e2) = e3| op(e1,e2) = e3| op(e2,e2) = e3| op(e3,e2) = e3| op(e4,e2) = e3 )& ( op(e2,e0) = e4| op(e2,e1) = e4| op(e2,e2) = e4| op(e2,e3) = e4| op(e2,e4) = e4 )& ( op(e0,e2) = e4| op(e1,e2) = e4| op(e2,e2) = e4| op(e3,e2) = e4| op(e4,e2) = e4 )& ( op(e3,e0) = e0| op(e3,e1) = e0| op(e3,e2) = e0| op(e3,e3) = e0| op(e3,e4) = e0 )& ( op(e0,e3) = e0| op(e1,e3) = e0| op(e2,e3) = e0| op(e3,e3) = e0| op(e4,e3) = e0 )& ( op(e3,e0) = e1| op(e3,e1) = e1| op(e3,e2) = e1| op(e3,e3) = e1| op(e3,e4) = e1 )& ( op(e0,e3) = e1| op(e1,e3) = e1| op(e2,e3) = e1| op(e3,e3) = e1| op(e4,e3) = e1 )& ( op(e3,e0) = e2| op(e3,e1) = e2| op(e3,e2) = e2| op(e3,e3) = e2| op(e3,e4) = e2 )& ( op(e0,e3) = e2| op(e1,e3) = e2| op(e2,e3) = e2| op(e3,e3) = e2| op(e4,e3) = e2 )& ( op(e3,e0) = e3| op(e3,e1) = e3| op(e3,e2) = e3| op(e3,e3) = e3| op(e3,e4) = e3 )& ( op(e0,e3) = e3| op(e1,e3) = e3| op(e2,e3) = e3| op(e3,e3) = e3| op(e4,e3) = e3 )& ( op(e3,e0) = e4| op(e3,e1) = e4| op(e3,e2) = e4| op(e3,e3) = e4| op(e3,e4) = e4 )& ( op(e0,e3) = e4| op(e1,e3) = e4| op(e2,e3) = e4| op(e3,e3) = e4| op(e4,e3) = e4 )& ( op(e4,e0) = e0| op(e4,e1) = e0| op(e4,e2) = e0| op(e4,e3) = e0| op(e4,e4) = e0 )& ( op(e0,e4) = e0| op(e1,e4) = e0| op(e2,e4) = e0| op(e3,e4) = e0| op(e4,e4) = e0 )& ( op(e4,e0) = e1| op(e4,e1) = e1| op(e4,e2) = e1| op(e4,e3) = e1| op(e4,e4) = e1 )& ( op(e0,e4) = e1| op(e1,e4) = e1| op(e2,e4) = e1| op(e3,e4) = e1| op(e4,e4) = e1 )& ( op(e4,e0) = e2| op(e4,e1) = e2| op(e4,e2) = e2| op(e4,e3) = e2| op(e4,e4) = e2 )& ( op(e0,e4) = e2| op(e1,e4) = e2| op(e2,e4) = e2| op(e3,e4) = e2| op(e4,e4) = e2 )& ( op(e4,e0) = e3| op(e4,e1) = e3| op(e4,e2) = e3| op(e4,e3) = e3| op(e4,e4) = e3 )& ( op(e0,e4) = e3| op(e1,e4) = e3| op(e2,e4) = e3| op(e3,e4) = e3| op(e4,e4) = e3 )& ( op(e4,e0) = e4| op(e4,e1) = e4| op(e4,e2) = e4| op(e4,e3) = e4| op(e4,e4) = e4 )& ( op(e0,e4) = e4| op(e1,e4) = e4| op(e2,e4) = e4| op(e3,e4) = e4| op(e4,e4) = e4 ) ) ),
% 0.09/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f4,axiom,(
% 0.09/0.45 ( op(e0,e0) != op(e1,e0)& op(e0,e0) != op(e2,e0)& op(e0,e0) != op(e3,e0)& op(e0,e0) != op(e4,e0)& op(e1,e0) != op(e2,e0)& op(e1,e0) != op(e3,e0)& op(e1,e0) != op(e4,e0)& op(e2,e0) != op(e3,e0)& op(e2,e0) != op(e4,e0)& op(e3,e0) != op(e4,e0)& op(e0,e1) != op(e1,e1)& op(e0,e1) != op(e2,e1)& op(e0,e1) != op(e3,e1)& op(e0,e1) != op(e4,e1)& op(e1,e1) != op(e2,e1)& op(e1,e1) != op(e3,e1)& op(e1,e1) != op(e4,e1)& op(e2,e1) != op(e3,e1)& op(e2,e1) != op(e4,e1)& op(e3,e1) != op(e4,e1)& op(e0,e2) != op(e1,e2)& op(e0,e2) != op(e2,e2)& op(e0,e2) != op(e3,e2)& op(e0,e2) != op(e4,e2)& op(e1,e2) != op(e2,e2)& op(e1,e2) != op(e3,e2)& op(e1,e2) != op(e4,e2)& op(e2,e2) != op(e3,e2)& op(e2,e2) != op(e4,e2)& op(e3,e2) != op(e4,e2)& op(e0,e3) != op(e1,e3)& op(e0,e3) != op(e2,e3)& op(e0,e3) != op(e3,e3)& op(e0,e3) != op(e4,e3)& op(e1,e3) != op(e2,e3)& op(e1,e3) != op(e3,e3)& op(e1,e3) != op(e4,e3)& op(e2,e3) != op(e3,e3)& op(e2,e3) != op(e4,e3)& op(e3,e3) != op(e4,e3)& op(e0,e4) != op(e1,e4)& op(e0,e4) != op(e2,e4)& op(e0,e4) != op(e3,e4)& op(e0,e4) != op(e4,e4)& op(e1,e4) != op(e2,e4)& op(e1,e4) != op(e3,e4)& op(e1,e4) != op(e4,e4)& op(e2,e4) != op(e3,e4)& op(e2,e4) != op(e4,e4)& op(e3,e4) != op(e4,e4)& op(e0,e0) != op(e0,e1)& op(e0,e0) != op(e0,e2)& op(e0,e0) != op(e0,e3)& op(e0,e0) != op(e0,e4)& op(e0,e1) != op(e0,e2)& op(e0,e1) != op(e0,e3)& op(e0,e1) != op(e0,e4)& op(e0,e2) != op(e0,e3)& op(e0,e2) != op(e0,e4)& op(e0,e3) != op(e0,e4)& op(e1,e0) != op(e1,e1)& op(e1,e0) != op(e1,e2)& op(e1,e0) != op(e1,e3)& op(e1,e0) != op(e1,e4)& op(e1,e1) != op(e1,e2)& op(e1,e1) != op(e1,e3)& op(e1,e1) != op(e1,e4)& op(e1,e2) != op(e1,e3)& op(e1,e2) != op(e1,e4)& op(e1,e3) != op(e1,e4)& op(e2,e0) != op(e2,e1)& op(e2,e0) != op(e2,e2)& op(e2,e0) != op(e2,e3)& op(e2,e0) != op(e2,e4)& op(e2,e1) != op(e2,e2)& op(e2,e1) != op(e2,e3)& op(e2,e1) != op(e2,e4)& op(e2,e2) != op(e2,e3)& op(e2,e2) != op(e2,e4)& op(e2,e3) != op(e2,e4)& op(e3,e0) != op(e3,e1)& op(e3,e0) != op(e3,e2)& op(e3,e0) != op(e3,e3)& op(e3,e0) != op(e3,e4)& op(e3,e1) != op(e3,e2)& op(e3,e1) != op(e3,e3)& op(e3,e1) != op(e3,e4)& op(e3,e2) != op(e3,e3)& op(e3,e2) != op(e3,e4)& op(e3,e3) != op(e3,e4)& op(e4,e0) != op(e4,e1)& op(e4,e0) != op(e4,e2)& op(e4,e0) != op(e4,e3)& op(e4,e0) != op(e4,e4)& op(e4,e1) != op(e4,e2)& op(e4,e1) != op(e4,e3)& op(e4,e1) != op(e4,e4)& op(e4,e2) != op(e4,e3)& op(e4,e2) != op(e4,e4)& op(e4,e3) != op(e4,e4) ) ),
% 0.09/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f5,axiom,(
% 0.09/0.45 ( e0 != e1& e0 != e2& e0 != e3& e0 != e4& e1 != e2& e1 != e3& e1 != e4& e2 != e3& e2 != e4& e3 != e4 ) ),
% 0.09/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f6,axiom,(
% 0.09/0.45 ( e0 = op(op(e4,e2),op(e4,e2))& e1 = op(e4,e2)& e3 = op(e2,e4) ) ),
% 0.09/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f7,conjecture,(
% 0.09/0.45 ~ ( ( op(e0,e0) != e0| op(e0,e0) = e0 )& ( op(e0,e0) != e1| op(e0,e1) = e0 )& ( op(e0,e0) != e2| op(e0,e2) = e0 )& ( op(e0,e0) != e3| op(e0,e3) = e0 )& ( op(e0,e0) != e4| op(e0,e4) = e0 )& ( op(e1,e1) != e0| op(e1,e0) = e1 )& ( op(e1,e1) != e1| op(e1,e1) = e1 )& ( op(e1,e1) != e2| op(e1,e2) = e1 )& ( op(e1,e1) != e3| op(e1,e3) = e1 )& ( op(e1,e1) != e4| op(e1,e4) = e1 )& ( op(e2,e2) != e0| op(e2,e0) = e2 )& ( op(e2,e2) != e1| op(e2,e1) = e2 )& ( op(e2,e2) != e2| op(e2,e2) = e2 )& ( op(e2,e2) != e3| op(e2,e3) = e2 )& ( op(e2,e2) != e4| op(e2,e4) = e2 )& ( op(e3,e3) != e0| op(e3,e0) = e3 )& ( op(e3,e3) != e1| op(e3,e1) = e3 )& ( op(e3,e3) != e2| op(e3,e2) = e3 )& ( op(e3,e3) != e3| op(e3,e3) = e3 )& ( op(e3,e3) != e4| op(e3,e4) = e3 )& ( op(e4,e4) != e0| op(e4,e0) = e4 )& ( op(e4,e4) != e1| op(e4,e1) = e4 )& ( op(e4,e4) != e2| op(e4,e2) = e4 )& ( op(e4,e4) != e3| op(e4,e3) = e4 )& ( op(e4,e4) != e4| op(e4,e4) = e4 )& ( ( op(e0,op(e0,e0)) != e0& op(e0,op(e0,e0)) = e0 )| ( op(e1,op(e1,e0)) != e0& op(e0,op(e1,e0)) = e1 )| ( op(e2,op(e2,e0)) != e0& op(e0,op(e2,e0)) = e2 )| ( op(e3,op(e3,e0)) != e0& op(e0,op(e3,e0)) = e3 )| ( op(e4,op(e4,e0)) != e0& op(e0,op(e4,e0)) = e4 ) )& ( ( op(e0,op(e0,e1)) != e1& op(e1,op(e0,e1)) = e0 )| ( op(e1,op(e1,e1)) != e1& op(e1,op(e1,e1)) = e1 )| ( op(e2,op(e2,e1)) != e1& op(e1,op(e2,e1)) = e2 )| ( op(e3,op(e3,e1)) != e1& op(e1,op(e3,e1)) = e3 )| ( op(e4,op(e4,e1)) != e1& op(e1,op(e4,e1)) = e4 ) )& ( ( op(e0,op(e0,e2)) != e2& op(e2,op(e0,e2)) = e0 )| ( op(e1,op(e1,e2)) != e2& op(e2,op(e1,e2)) = e1 )| ( op(e2,op(e2,e2)) != e2& op(e2,op(e2,e2)) = e2 )| ( op(e3,op(e3,e2)) != e2& op(e2,op(e3,e2)) = e3 )| ( op(e4,op(e4,e2)) != e2& op(e2,op(e4,e2)) = e4 ) )& ( ( op(e0,op(e0,e3)) != e3& op(e3,op(e0,e3)) = e0 )| ( op(e1,op(e1,e3)) != e3& op(e3,op(e1,e3)) = e1 )| ( op(e2,op(e2,e3)) != e3& op(e3,op(e2,e3)) = e2 )| ( op(e3,op(e3,e3)) != e3& op(e3,op(e3,e3)) = e3 )| ( op(e4,op(e4,e3)) != e3& op(e3,op(e4,e3)) = e4 ) )& ( ( op(e0,op(e0,e4)) != e4& op(e4,op(e0,e4)) = e0 )| ( op(e1,op(e1,e4)) != e4& op(e4,op(e1,e4)) = e1 )| ( op(e2,op(e2,e4)) != e4& op(e4,op(e2,e4)) = e2 )| ( op(e3,op(e3,e4)) != e4& op(e4,op(e3,e4)) = e3 )| ( op(e4,op(e4,e4)) != e4& op(e4,op(e4,e4)) = e4 ) ) ) ),
% 0.09/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f8,negated_conjecture,(
% 0.09/0.45 ~(~ ( ( op(e0,e0) != e0| op(e0,e0) = e0 )& ( op(e0,e0) != e1| op(e0,e1) = e0 )& ( op(e0,e0) != e2| op(e0,e2) = e0 )& ( op(e0,e0) != e3| op(e0,e3) = e0 )& ( op(e0,e0) != e4| op(e0,e4) = e0 )& ( op(e1,e1) != e0| op(e1,e0) = e1 )& ( op(e1,e1) != e1| op(e1,e1) = e1 )& ( op(e1,e1) != e2| op(e1,e2) = e1 )& ( op(e1,e1) != e3| op(e1,e3) = e1 )& ( op(e1,e1) != e4| op(e1,e4) = e1 )& ( op(e2,e2) != e0| op(e2,e0) = e2 )& ( op(e2,e2) != e1| op(e2,e1) = e2 )& ( op(e2,e2) != e2| op(e2,e2) = e2 )& ( op(e2,e2) != e3| op(e2,e3) = e2 )& ( op(e2,e2) != e4| op(e2,e4) = e2 )& ( op(e3,e3) != e0| op(e3,e0) = e3 )& ( op(e3,e3) != e1| op(e3,e1) = e3 )& ( op(e3,e3) != e2| op(e3,e2) = e3 )& ( op(e3,e3) != e3| op(e3,e3) = e3 )& ( op(e3,e3) != e4| op(e3,e4) = e3 )& ( op(e4,e4) != e0| op(e4,e0) = e4 )& ( op(e4,e4) != e1| op(e4,e1) = e4 )& ( op(e4,e4) != e2| op(e4,e2) = e4 )& ( op(e4,e4) != e3| op(e4,e3) = e4 )& ( op(e4,e4) != e4| op(e4,e4) = e4 )& ( ( op(e0,op(e0,e0)) != e0& op(e0,op(e0,e0)) = e0 )| ( op(e1,op(e1,e0)) != e0& op(e0,op(e1,e0)) = e1 )| ( op(e2,op(e2,e0)) != e0& op(e0,op(e2,e0)) = e2 )| ( op(e3,op(e3,e0)) != e0& op(e0,op(e3,e0)) = e3 )| ( op(e4,op(e4,e0)) != e0& op(e0,op(e4,e0)) = e4 ) )& ( ( op(e0,op(e0,e1)) != e1& op(e1,op(e0,e1)) = e0 )| ( op(e1,op(e1,e1)) != e1& op(e1,op(e1,e1)) = e1 )| ( op(e2,op(e2,e1)) != e1& op(e1,op(e2,e1)) = e2 )| ( op(e3,op(e3,e1)) != e1& op(e1,op(e3,e1)) = e3 )| ( op(e4,op(e4,e1)) != e1& op(e1,op(e4,e1)) = e4 ) )& ( ( op(e0,op(e0,e2)) != e2& op(e2,op(e0,e2)) = e0 )| ( op(e1,op(e1,e2)) != e2& op(e2,op(e1,e2)) = e1 )| ( op(e2,op(e2,e2)) != e2& op(e2,op(e2,e2)) = e2 )| ( op(e3,op(e3,e2)) != e2& op(e2,op(e3,e2)) = e3 )| ( op(e4,op(e4,e2)) != e2& op(e2,op(e4,e2)) = e4 ) )& ( ( op(e0,op(e0,e3)) != e3& op(e3,op(e0,e3)) = e0 )| ( op(e1,op(e1,e3)) != e3& op(e3,op(e1,e3)) = e1 )| ( op(e2,op(e2,e3)) != e3& op(e3,op(e2,e3)) = e2 )| ( op(e3,op(e3,e3)) != e3& op(e3,op(e3,e3)) = e3 )| ( op(e4,op(e4,e3)) != e3& op(e3,op(e4,e3)) = e4 ) )& ( ( op(e0,op(e0,e4)) != e4& op(e4,op(e0,e4)) = e0 )| ( op(e1,op(e1,e4)) != e4& op(e4,op(e1,e4)) = e1 )| ( op(e2,op(e2,e4)) != e4& op(e4,op(e2,e4)) = e2 )| ( op(e3,op(e3,e4)) != e4& op(e4,op(e3,e4)) = e3 )| ( op(e4,op(e4,e4)) != e4& op(e4,op(e4,e4)) = e4 ) ) ) )),
% 0.09/0.45 inference(negated_conjecture,[status(cth)],[f7])).
% 0.09/0.45 fof(f21,plain,(
% 0.09/0.45 op(e2,e2)=e0|op(e2,e2)=e1|op(e2,e2)=e2|op(e2,e2)=e3|op(e2,e2)=e4),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f1])).
% 0.09/0.45 fof(f27,plain,(
% 0.09/0.45 op(e3,e3)=e0|op(e3,e3)=e1|op(e3,e3)=e2|op(e3,e3)=e3|op(e3,e3)=e4),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f1])).
% 0.09/0.45 fof(f33,plain,(
% 0.09/0.45 op(e4,e4)=e0|op(e4,e4)=e1|op(e4,e4)=e2|op(e4,e4)=e3|op(e4,e4)=e4),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f1])).
% 0.09/0.45 fof(f37,plain,(
% 0.09/0.45 op(e1,unit)=e1),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.45 fof(f39,plain,(
% 0.09/0.45 op(e2,unit)=e2),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.45 fof(f41,plain,(
% 0.09/0.45 op(e3,unit)=e3),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.45 fof(f42,plain,(
% 0.09/0.45 op(unit,e4)=e4),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.45 fof(f43,plain,(
% 0.09/0.45 op(e4,unit)=e4),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.45 fof(f44,plain,(
% 0.09/0.45 unit=e0|unit=e1|unit=e2|unit=e3|unit=e4),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.45 fof(f88,plain,(
% 0.09/0.45 op(e0,e4)=e1|op(e1,e4)=e1|op(e2,e4)=e1|op(e3,e4)=e1|op(e4,e4)=e1),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f3])).
% 0.09/0.45 fof(f123,plain,(
% 0.09/0.45 ~op(e2,e2)=op(e4,e2)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.45 fof(f142,plain,(
% 0.09/0.45 ~op(e2,e4)=op(e3,e4)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.45 fof(f143,plain,(
% 0.09/0.45 ~op(e2,e4)=op(e4,e4)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.45 fof(f157,plain,(
% 0.09/0.45 ~op(e1,e0)=op(e1,e3)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.45 fof(f158,plain,(
% 0.09/0.45 ~op(e1,e0)=op(e1,e4)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.45 fof(f166,plain,(
% 0.09/0.45 ~op(e2,e0)=op(e2,e2)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.45 fof(f173,plain,(
% 0.09/0.45 ~op(e2,e2)=op(e2,e4)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.45 fof(f176,plain,(
% 0.09/0.45 ~op(e3,e0)=op(e3,e2)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.45 fof(f177,plain,(
% 0.09/0.45 ~op(e3,e0)=op(e3,e3)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.45 fof(f184,plain,(
% 0.09/0.45 ~op(e3,e3)=op(e3,e4)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.45 fof(f188,plain,(
% 0.09/0.45 ~op(e4,e0)=op(e4,e4)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.45 fof(f193,plain,(
% 0.09/0.45 ~op(e4,e2)=op(e4,e4)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.45 fof(f195,plain,(
% 0.09/0.45 ~e0=e1),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.09/0.45 fof(f200,plain,(
% 0.09/0.45 ~e1=e3),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.09/0.45 fof(f201,plain,(
% 0.09/0.45 ~e1=e4),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.09/0.45 fof(f202,plain,(
% 0.09/0.45 ~e2=e3),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.09/0.45 fof(f205,plain,(
% 0.09/0.45 e0=op(op(e4,e2),op(e4,e2))),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f6])).
% 0.09/0.45 fof(f206,plain,(
% 0.09/0.45 e1=op(e4,e2)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f6])).
% 0.09/0.45 fof(f207,plain,(
% 0.09/0.45 e3=op(e2,e4)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f6])).
% 0.09/0.45 fof(f208,definition,(
% 0.09/0.45 sP0_prd<=>((((~op(e0,op(e0,e0))=e0&op(e0,op(e0,e0))=e0)|(~op(e1,op(e1,e0))=e0&op(e0,op(e1,e0))=e1))|(~op(e2,op(e2,e0))=e0&op(e0,op(e2,e0))=e2))|(~op(e3,op(e3,e0))=e0&op(e0,op(e3,e0))=e3))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.09/0.45 fof(f209,definition,(
% 0.09/0.45 sP1_prd<=>((((~op(e0,op(e0,e1))=e1&op(e1,op(e0,e1))=e0)|(~op(e1,op(e1,e1))=e1&op(e1,op(e1,e1))=e1))|(~op(e2,op(e2,e1))=e1&op(e1,op(e2,e1))=e2))|(~op(e3,op(e3,e1))=e1&op(e1,op(e3,e1))=e3))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.09/0.45 fof(f210,definition,(
% 0.09/0.45 sP2_prd<=>((((~op(e0,op(e0,e2))=e2&op(e2,op(e0,e2))=e0)|(~op(e1,op(e1,e2))=e2&op(e2,op(e1,e2))=e1))|(~op(e2,op(e2,e2))=e2&op(e2,op(e2,e2))=e2))|(~op(e3,op(e3,e2))=e2&op(e2,op(e3,e2))=e3))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.09/0.45 fof(f211,definition,(
% 0.09/0.45 sP3_prd<=>((((~op(e0,op(e0,e3))=e3&op(e3,op(e0,e3))=e0)|(~op(e1,op(e1,e3))=e3&op(e3,op(e1,e3))=e1))|(~op(e2,op(e2,e3))=e3&op(e3,op(e2,e3))=e2))|(~op(e3,op(e3,e3))=e3&op(e3,op(e3,e3))=e3))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.09/0.45 fof(f212,definition,(
% 0.09/0.45 sP4_prd<=>((((~op(e0,op(e0,e4))=e4&op(e4,op(e0,e4))=e0)|(~op(e1,op(e1,e4))=e4&op(e4,op(e1,e4))=e1))|(~op(e2,op(e2,e4))=e4&op(e4,op(e2,e4))=e2))|(~op(e3,op(e3,e4))=e4&op(e4,op(e3,e4))=e3))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.09/0.45 fof(f213,plain,(
% 0.09/0.45 (((((((((((((((((((((((((((((~op(e0,e0)=e0|op(e0,e0)=e0)&(~op(e0,e0)=e1|op(e0,e1)=e0))&(~op(e0,e0)=e2|op(e0,e2)=e0))&(~op(e0,e0)=e3|op(e0,e3)=e0))&(~op(e0,e0)=e4|op(e0,e4)=e0))&(~op(e1,e1)=e0|op(e1,e0)=e1))&(~op(e1,e1)=e1|op(e1,e1)=e1))&(~op(e1,e1)=e2|op(e1,e2)=e1))&(~op(e1,e1)=e3|op(e1,e3)=e1))&(~op(e1,e1)=e4|op(e1,e4)=e1))&(~op(e2,e2)=e0|op(e2,e0)=e2))&(~op(e2,e2)=e1|op(e2,e1)=e2))&(~op(e2,e2)=e2|op(e2,e2)=e2))&(~op(e2,e2)=e3|op(e2,e3)=e2))&(~op(e2,e2)=e4|op(e2,e4)=e2))&(~op(e3,e3)=e0|op(e3,e0)=e3))&(~op(e3,e3)=e1|op(e3,e1)=e3))&(~op(e3,e3)=e2|op(e3,e2)=e3))&(~op(e3,e3)=e3|op(e3,e3)=e3))&(~op(e3,e3)=e4|op(e3,e4)=e3))&(~op(e4,e4)=e0|op(e4,e0)=e4))&(~op(e4,e4)=e1|op(e4,e1)=e4))&(~op(e4,e4)=e2|op(e4,e2)=e4))&(~op(e4,e4)=e3|op(e4,e3)=e4))&(~op(e4,e4)=e4|op(e4,e4)=e4))&(sP0_prd|(~op(e4,op(e4,e0))=e0&op(e0,op(e4,e0))=e4)))&(sP1_prd|(~op(e4,op(e4,e1))=e1&op(e1,op(e4,e1))=e4)))&(sP2_prd|(~op(e4,op(e4,e2))=e2&op(e2,op(e4,e2))=e4)))&(sP3_prd|(~op(e4,op(e4,e3))=e3&op(e3,op(e4,e3))=e4)))&(sP4_prd|(~op(e4,op(e4,e4))=e4&op(e4,op(e4,e4))=e4))),
% 0.09/0.45 inference(formula_renaming,[status(thm)],[f8,f212,f211,f210,f209,f208])).
% 0.09/0.45 fof(f219,plain,(
% 0.09/0.45 ~op(e1,e1)=e0|op(e1,e0)=e1),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f213])).
% 0.09/0.45 fof(f228,plain,(
% 0.09/0.45 ~op(e2,e2)=e4|op(e2,e4)=e2),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f213])).
% 0.09/0.45 fof(f231,plain,(
% 0.09/0.45 ~op(e3,e3)=e2|op(e3,e2)=e3),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f213])).
% 0.09/0.45 fof(f233,plain,(
% 0.09/0.45 ~op(e3,e3)=e4|op(e3,e4)=e3),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f213])).
% 0.09/0.45 fof(f236,plain,(
% 0.09/0.45 ~op(e4,e4)=e2|op(e4,e2)=e4),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f213])).
% 0.09/0.45 fof(f239,plain,(
% 0.09/0.45 sP0_prd|~op(e4,op(e4,e0))=e0),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f213])).
% 0.09/0.45 fof(f249,definition,(
% 0.09/0.45 sP5_prd<=>(((~op(e0,op(e0,e0))=e0&op(e0,op(e0,e0))=e0)|(~op(e1,op(e1,e0))=e0&op(e0,op(e1,e0))=e1))|(~op(e2,op(e2,e0))=e0&op(e0,op(e2,e0))=e2))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.09/0.45 fof(f250,plain,(
% 0.09/0.45 sP0_prd<=>(sP5_prd|(~op(e3,op(e3,e0))=e0&op(e0,op(e3,e0))=e3))),
% 0.09/0.45 inference(formula_renaming,[status(thm)],[f208,f249])).
% 0.09/0.45 fof(f251,plain,(
% 0.09/0.45 (~sP0_prd|(sP5_prd|(~op(e3,op(e3,e0))=e0&op(e0,op(e3,e0))=e3)))&(sP0_prd|(~sP5_prd&(op(e3,op(e3,e0))=e0|~op(e0,op(e3,e0))=e3)))),
% 0.09/0.45 inference(NNF_transformation,[status(thm)],[f250])).
% 0.09/0.45 fof(f252,plain,(
% 0.09/0.45 ~sP0_prd|sP5_prd|~op(e3,op(e3,e0))=e0),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f251])).
% 0.09/0.45 fof(f284,definition,(
% 0.09/0.45 sP10_prd<=>((~op(e0,op(e0,e0))=e0&op(e0,op(e0,e0))=e0)|(~op(e1,op(e1,e0))=e0&op(e0,op(e1,e0))=e1))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.09/0.45 fof(f285,plain,(
% 0.09/0.45 sP5_prd<=>(sP10_prd|(~op(e2,op(e2,e0))=e0&op(e0,op(e2,e0))=e2))),
% 0.09/0.45 inference(formula_renaming,[status(thm)],[f249,f284])).
% 0.09/0.45 fof(f286,plain,(
% 0.09/0.45 (~sP5_prd|(sP10_prd|(~op(e2,op(e2,e0))=e0&op(e0,op(e2,e0))=e2)))&(sP5_prd|(~sP10_prd&(op(e2,op(e2,e0))=e0|~op(e0,op(e2,e0))=e2)))),
% 0.09/0.45 inference(NNF_transformation,[status(thm)],[f285])).
% 0.09/0.45 fof(f287,plain,(
% 0.09/0.45 ~sP5_prd|sP10_prd|~op(e2,op(e2,e0))=e0),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f286])).
% 0.09/0.45 fof(f319,plain,(
% 0.09/0.45 (~sP10_prd|((~op(e0,op(e0,e0))=e0&op(e0,op(e0,e0))=e0)|(~op(e1,op(e1,e0))=e0&op(e0,op(e1,e0))=e1)))&(sP10_prd|((op(e0,op(e0,e0))=e0|~op(e0,op(e0,e0))=e0)&(op(e1,op(e1,e0))=e0|~op(e0,op(e1,e0))=e1)))),
% 0.09/0.45 inference(NNF_transformation,[status(thm)],[f284])).
% 0.09/0.45 fof(f320,plain,(
% 0.09/0.45 ~sP10_prd|~op(e0,op(e0,e0))=e0|~op(e1,op(e1,e0))=e0),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f319])).
% 0.09/0.45 fof(f322,plain,(
% 0.09/0.45 ~sP10_prd|op(e0,op(e0,e0))=e0|~op(e1,op(e1,e0))=e0),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f319])).
% 0.09/0.45 fof(f354,plain,(
% 0.09/0.45 e0=op(op(e4,e2),e1)),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f206,f205])).
% 0.09/0.45 fof(f355,plain,(
% 0.09/0.45 ~e1=op(e4,e4)),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f206,f193])).
% 0.09/0.45 fof(f360,plain,(
% 0.09/0.45 ~op(e2,e2)=e1),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f206,f123])).
% 0.09/0.45 fof(f375,plain,(
% 0.09/0.45 ~op(e2,e2)=e3),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f207,f173])).
% 0.09/0.45 fof(f378,plain,(
% 0.09/0.45 ~e3=op(e4,e4)),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f207,f143])).
% 0.09/0.45 fof(f379,plain,(
% 0.09/0.45 ~e3=op(e3,e4)),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f207,f142])).
% 0.09/0.45 fof(f385,plain,(
% 0.09/0.45 op(e0,e4)=e1|op(e1,e4)=e1|e3=e1|op(e3,e4)=e1|op(e4,e4)=e1),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f207,f88])).
% 0.09/0.45 fof(f393,plain,(
% 0.09/0.45 ~op(e2,e2)=e4|e3=e2),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f207,f228])).
% 0.09/0.45 fof(f394,plain,(
% 0.09/0.45 op(e2,e2)=e0|op(e2,e2)=e1|op(e2,e2)=e2|op(e2,e2)=e3),
% 0.09/0.45 inference(backward_subsumption_resolution,[status(thm)],[f21,f395])).
% 0.09/0.45 fof(f395,plain,(
% 0.09/0.45 ~op(e2,e2)=e4),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f393,f202])).
% 0.09/0.45 fof(f396,plain,(
% 0.09/0.45 ~op(e4,e4)=e2|e1=e4),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f206,f236])).
% 0.09/0.45 fof(f397,plain,(
% 0.09/0.45 op(e4,e4)=e0|op(e4,e4)=e1|op(e4,e4)=e3|op(e4,e4)=e4),
% 0.09/0.45 inference(backward_subsumption_resolution,[status(thm)],[f33,f398])).
% 0.09/0.45 fof(f398,plain,(
% 0.09/0.45 ~op(e4,e4)=e2),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f396,f201])).
% 0.09/0.45 fof(f410,plain,(
% 0.09/0.45 ~sP10_prd|~op(e1,op(e1,e0))=e0),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f322,f320])).
% 0.09/0.45 fof(f417,plain,(
% 0.09/0.45 ~e0=e0|op(e1,e0)=e1),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f437,f219])).
% 0.09/0.45 fof(f437,plain,(
% 0.09/0.45 e0=op(e1,e1)),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f206,f354])).
% 0.09/0.45 fof(f464,plain,(
% 0.09/0.45 ~op(e3,e3)=e4),
% 0.09/0.45 inference(backward_subsumption_resolution,[status(thm)],[f233,f379])).
% 0.09/0.45 fof(f472,plain,(
% 0.09/0.45 op(e0,e4)=e1|op(e1,e4)=e1|op(e3,e4)=e1|op(e4,e4)=e1),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f385,f200])).
% 0.09/0.45 fof(f481,plain,(
% 0.09/0.45 op(e2,e2)=e0|op(e2,e2)=e2|op(e2,e2)=e3),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f394,f360])).
% 0.09/0.45 fof(f482,plain,(
% 0.09/0.45 op(e4,e4)=e0|op(e4,e4)=e3|op(e4,e4)=e4),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f397,f355])).
% 0.09/0.45 fof(f485,plain,(
% 0.09/0.45 ~sP10_prd|~op(e1,e1)=e0),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f497,f410])).
% 0.09/0.46 fof(f486,plain,(
% 0.09/0.46 ~e1=op(e1,e4)),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f497,f158])).
% 0.09/0.46 fof(f487,plain,(
% 0.09/0.46 ~e1=op(e1,e3)),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f497,f157])).
% 0.09/0.46 fof(f497,plain,(
% 0.09/0.46 op(e1,e0)=e1),
% 0.09/0.46 inference(trivial_equality_resolution,[status(thm)],[f417])).
% 0.09/0.46 fof(f527,plain,(
% 0.09/0.46 op(e3,e3)=e0|op(e3,e3)=e1|op(e3,e3)=e2|op(e3,e3)=e3),
% 0.09/0.46 inference(backward_subsumption_resolution,[status(thm)],[f27,f464])).
% 0.09/0.46 fof(f530,plain,(
% 0.09/0.46 ~sP10_prd|~e0=e0),
% 0.09/0.46 inference(forward_demodulation,[status(thm)],[f437,f485])).
% 0.09/0.46 fof(f532,plain,(
% 0.09/0.46 ~sP5_prd|~op(e2,op(e2,e0))=e0),
% 0.09/0.46 inference(backward_subsumption_resolution,[status(thm)],[f287,f533])).
% 0.09/0.46 fof(f533,plain,(
% 0.09/0.46 ~sP10_prd),
% 0.09/0.46 inference(trivial_equality_resolution,[status(thm)],[f530])).
% 0.09/0.46 fof(f535,plain,(
% 0.09/0.46 op(e0,e4)=e1|op(e3,e4)=e1|op(e4,e4)=e1),
% 0.09/0.46 inference(backward_subsumption_resolution,[status(thm)],[f472,f486])).
% 0.09/0.46 fof(f548,plain,(
% 0.09/0.46 op(e0,e4)=e1|op(e3,e4)=e1),
% 0.09/0.46 inference(forward_subsumption_resolution,[status(thm)],[f535,f355])).
% 0.09/0.46 fof(f562,plain,(
% 0.09/0.46 op(e3,e4)=e3|unit=e0|unit=e1|unit=e2|unit=e3),
% 0.09/0.46 inference(paramodulation,[status(thm)],[f44,f41])).
% 0.09/0.46 fof(f574,plain,(
% 0.09/0.46 unit=e0|unit=e1|unit=e2|unit=e3),
% 0.09/0.46 inference(forward_subsumption_resolution,[status(thm)],[f562,f379])).
% 0.09/0.46 fof(f612,plain,(
% 0.09/0.46 ~op(e2,op(e2,e0))=e0|~sP0_prd|~op(e3,op(e3,e0))=e0),
% 0.09/0.46 inference(resolution,[status(thm)],[f532,f252])).
% 0.09/0.46 fof(f634,plain,(
% 0.09/0.46 ~op(e3,e3)=e1|op(e0,e4)=e1),
% 0.09/0.46 inference(paramodulation,[status(thm)],[f548,f184])).
% 0.09/0.46 fof(f658,plain,(
% 0.09/0.46 op(e1,e3)=e1|unit=e0|unit=e1|unit=e2),
% 0.09/0.46 inference(paramodulation,[status(thm)],[f574,f37])).
% 0.09/0.46 fof(f665,plain,(
% 0.09/0.46 unit=e0|unit=e1|unit=e2),
% 0.09/0.46 inference(forward_subsumption_resolution,[status(thm)],[f658,f487])).
% 0.09/0.46 fof(f666,plain,(
% 0.09/0.46 op(e4,e2)=e4|unit=e0|unit=e1),
% 0.09/0.46 inference(paramodulation,[status(thm)],[f665,f43])).
% 0.09/0.46 fof(f678,plain,(
% 0.09/0.46 e1=e4|unit=e0|unit=e1),
% 0.09/0.46 inference(forward_demodulation,[status(thm)],[f206,f666])).
% 0.09/0.46 fof(f679,plain,(
% 0.09/0.46 unit=e0|unit=e1),
% 0.09/0.46 inference(forward_subsumption_resolution,[status(thm)],[f678,f201])).
% 0.09/0.46 fof(f687,plain,(
% 0.09/0.46 op(e1,e1)=e1|unit=e0),
% 0.09/0.46 inference(paramodulation,[status(thm)],[f679,f37])).
% 0.09/0.46 fof(f692,plain,(
% 0.09/0.46 e0=e1|unit=e0),
% 0.09/0.46 inference(forward_demodulation,[status(thm)],[f437,f687])).
% 0.09/0.46 fof(f694,plain,(
% 0.09/0.46 op(e4,e0)=e4),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f710,f43])).
% 0.09/0.46 fof(f695,plain,(
% 0.09/0.46 op(e0,e4)=e4),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f710,f42])).
% 0.09/0.46 fof(f696,plain,(
% 0.09/0.46 op(e3,e0)=e3),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f710,f41])).
% 0.09/0.46 fof(f698,plain,(
% 0.09/0.46 op(e2,e0)=e2),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f710,f39])).
% 0.09/0.46 fof(f710,plain,(
% 0.09/0.46 unit=e0),
% 0.09/0.46 inference(forward_subsumption_resolution,[status(thm)],[f692,f195])).
% 0.09/0.46 fof(f713,plain,(
% 0.09/0.46 ~e4=op(e4,e4)),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f694,f188])).
% 0.09/0.46 fof(f718,plain,(
% 0.09/0.46 sP0_prd|~op(e4,e4)=e0),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f694,f239])).
% 0.09/0.46 fof(f746,plain,(
% 0.09/0.46 ~op(e3,e3)=e1|e4=e1),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f695,f634])).
% 0.09/0.46 fof(f765,plain,(
% 0.09/0.46 ~e3=op(e3,e3)),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f696,f177])).
% 0.09/0.46 fof(f766,plain,(
% 0.09/0.46 ~e3=op(e3,e2)),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f696,f176])).
% 0.09/0.46 fof(f773,plain,(
% 0.09/0.46 ~op(e2,op(e2,e0))=e0|~sP0_prd|~op(e3,e3)=e0),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f696,f612])).
% 0.09/0.46 fof(f812,plain,(
% 0.09/0.46 ~e2=op(e2,e2)),
% 0.09/0.46 inference(backward_demodulation,[status(thm)],[f698,f166])).
% 0.09/0.46 fof(f855,plain,(
% 0.09/0.46 op(e4,e4)=e0|op(e4,e4)=e3),
% 0.09/0.46 inference(backward_subsumption_resolution,[status(thm)],[f482,f713])).
% 0.09/0.46 fof(f893,plain,(
% 0.09/0.46 op(e3,e3)=e0|op(e3,e3)=e2|op(e3,e3)=e3),
% 0.09/0.46 inference(backward_subsumption_resolution,[status(thm)],[f527,f894])).
% 0.09/0.46 fof(f894,plain,(
% 0.09/0.46 ~op(e3,e3)=e1),
% 0.09/0.46 inference(forward_subsumption_resolution,[status(thm)],[f746,f201])).
% 0.09/0.46 fof(f925,plain,(
% 0.09/0.46 ~op(e3,e3)=e2),
% 0.09/0.46 inference(backward_subsumption_resolution,[status(thm)],[f231,f766])).
% 0.09/0.46 fof(f930,plain,(
% 0.09/0.46 ~op(e2,e2)=e0|~sP0_prd|~op(e3,e3)=e0),
% 0.09/0.46 inference(forward_demodulation,[status(thm)],[f698,f773])).
% 0.09/0.47 fof(f972,plain,(
% 0.09/0.47 op(e2,e2)=e0|op(e2,e2)=e3),
% 0.09/0.47 inference(backward_subsumption_resolution,[status(thm)],[f481,f812])).
% 0.09/0.47 fof(f1016,plain,(
% 0.09/0.47 sP0_prd|~e0=e0),
% 0.09/0.47 inference(backward_demodulation,[status(thm)],[f1018,f718])).
% 0.09/0.47 fof(f1018,plain,(
% 0.09/0.47 op(e4,e4)=e0),
% 0.09/0.47 inference(forward_subsumption_resolution,[status(thm)],[f855,f378])).
% 0.09/0.47 fof(f1025,plain,(
% 0.09/0.47 op(e3,e3)=e0|op(e3,e3)=e2),
% 0.09/0.47 inference(forward_subsumption_resolution,[status(thm)],[f893,f765])).
% 0.09/0.47 fof(f1031,plain,(
% 0.09/0.47 op(e3,e3)=e0),
% 0.09/0.47 inference(backward_subsumption_resolution,[status(thm)],[f1025,f925])).
% 0.09/0.47 fof(f1081,plain,(
% 0.09/0.47 ~e0=e0|~sP0_prd|~op(e3,e3)=e0),
% 0.09/0.47 inference(backward_demodulation,[status(thm)],[f1082,f930])).
% 0.09/0.47 fof(f1082,plain,(
% 0.09/0.47 op(e2,e2)=e0),
% 0.09/0.47 inference(forward_subsumption_resolution,[status(thm)],[f972,f375])).
% 0.09/0.47 fof(f1122,plain,(
% 0.09/0.47 sP0_prd),
% 0.09/0.47 inference(trivial_equality_resolution,[status(thm)],[f1016])).
% 0.09/0.47 fof(f1153,plain,(
% 0.09/0.47 ~e0=e0|~sP0_prd|~e0=e0),
% 0.09/0.47 inference(forward_demodulation,[status(thm)],[f1031,f1081])).
% 0.09/0.47 fof(f1154,plain,(
% 0.09/0.47 ~e0=e0|~sP0_prd),
% 0.09/0.47 inference(duplicate_literals_removal,[status(thm)],[f1153])).
% 0.09/0.47 fof(f1155,plain,(
% 0.09/0.47 ~sP0_prd),
% 0.09/0.47 inference(trivial_equality_resolution,[status(thm)],[f1154])).
% 0.09/0.47 fof(f1156,plain,(
% 0.09/0.47 $false),
% 0.09/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1155,f1122])).
% 0.09/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.48 % Elapsed time: 0.108610 seconds
% 0.09/0.48 % CPU time: 0.578721 seconds
% 0.09/0.48 % Total memory used: 123.769 MB
% 0.09/0.48 % Net memory used: 123.333 MB
%------------------------------------------------------------------------------