%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG061+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : 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:32 AM UTC 2026
% Result : Theorem 0.13s 0.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG061+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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 12:54:48 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 0.13/0.44 % Refutation found
% 0.13/0.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.44 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.44 fof(f1,axiom,(
% 0.13/0.44 ( ( 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.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f2,axiom,(
% 0.13/0.44 ( 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.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f3,axiom,(
% 0.13/0.44 ( ( 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.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f4,axiom,(
% 0.13/0.44 ( 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.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f5,axiom,(
% 0.13/0.44 ( e0 != e1& e0 != e2& e0 != e3& e0 != e4& e1 != e2& e1 != e3& e1 != e4& e2 != e3& e2 != e4& e3 != e4 ) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f6,axiom,(
% 0.13/0.44 ( e0 = op(e1,op(op(e1,e1),op(e1,e1)))& e2 = op(op(e1,e1),op(e1,e1))& e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1)))& e4 = op(e1,e1) ) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f7,conjecture,(
% 0.13/0.44 ~ ( ( op(e0,e0) = e0| op(e1,e1) = e0| op(e2,e2) = e0| op(e3,e3) = e0| op(e4,e4) = e0 )& ( op(e0,e0) = e1| op(e1,e1) = e1| op(e2,e2) = e1| op(e3,e3) = e1| op(e4,e4) = e1 )& ( op(e0,e0) = e2| op(e1,e1) = e2| op(e2,e2) = e2| op(e3,e3) = e2| op(e4,e4) = e2 )& ( op(e0,e0) = e3| op(e1,e1) = e3| op(e2,e2) = e3| op(e3,e3) = e3| op(e4,e4) = e3 )& ( op(e0,e0) = e4| op(e1,e1) = e4| op(e2,e2) = e4| op(e3,e3) = 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.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f8,negated_conjecture,(
% 0.13/0.44 ~(~ ( ( op(e0,e0) = e0| op(e1,e1) = e0| op(e2,e2) = e0| op(e3,e3) = e0| op(e4,e4) = e0 )& ( op(e0,e0) = e1| op(e1,e1) = e1| op(e2,e2) = e1| op(e3,e3) = e1| op(e4,e4) = e1 )& ( op(e0,e0) = e2| op(e1,e1) = e2| op(e2,e2) = e2| op(e3,e3) = e2| op(e4,e4) = e2 )& ( op(e0,e0) = e3| op(e1,e1) = e3| op(e2,e2) = e3| op(e3,e3) = e3| op(e4,e4) = e3 )& ( op(e0,e0) = e4| op(e1,e1) = e4| op(e2,e2) = e4| op(e3,e3) = 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.13/0.44 inference(negated_conjecture,[status(cth)],[f7])).
% 0.13/0.44 fof(f20,plain,(
% 0.13/0.44 op(e2,e1)=e0|op(e2,e1)=e1|op(e2,e1)=e2|op(e2,e1)=e3|op(e2,e1)=e4),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.44 fof(f26,plain,(
% 0.13/0.44 op(e3,e2)=e0|op(e3,e2)=e1|op(e3,e2)=e2|op(e3,e2)=e3|op(e3,e2)=e4),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.44 fof(f35,plain,(
% 0.13/0.44 op(e0,unit)=e0),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.44 fof(f36,plain,(
% 0.13/0.44 op(unit,e1)=e1),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.44 fof(f37,plain,(
% 0.13/0.44 op(e1,unit)=e1),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.44 fof(f38,plain,(
% 0.13/0.44 op(unit,e2)=e2),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.44 fof(f39,plain,(
% 0.13/0.44 op(e2,unit)=e2),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.44 fof(f40,plain,(
% 0.13/0.44 op(unit,e3)=e3),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.44 fof(f41,plain,(
% 0.13/0.44 op(e3,unit)=e3),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.44 fof(f43,plain,(
% 0.13/0.44 op(e4,unit)=e4),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.44 fof(f44,plain,(
% 0.13/0.44 unit=e0|unit=e1|unit=e2|unit=e3|unit=e4),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.44 fof(f59,plain,(
% 0.13/0.44 op(e1,e0)=e2|op(e1,e1)=e2|op(e1,e2)=e2|op(e1,e3)=e2|op(e1,e4)=e2),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.44 fof(f60,plain,(
% 0.13/0.44 op(e0,e1)=e2|op(e1,e1)=e2|op(e2,e1)=e2|op(e3,e1)=e2|op(e4,e1)=e2),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.44 fof(f67,plain,(
% 0.13/0.44 op(e2,e0)=e1|op(e2,e1)=e1|op(e2,e2)=e1|op(e2,e3)=e1|op(e2,e4)=e1),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.44 fof(f77,plain,(
% 0.13/0.44 op(e3,e0)=e1|op(e3,e1)=e1|op(e3,e2)=e1|op(e3,e3)=e1|op(e3,e4)=e1),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.44 fof(f91,plain,(
% 0.13/0.44 op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e2)=e3|op(e4,e3)=e3|op(e4,e4)=e3),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.44 fof(f106,plain,(
% 0.13/0.44 ~op(e0,e1)=op(e2,e1)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f107,plain,(
% 0.13/0.44 ~op(e0,e1)=op(e3,e1)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f109,plain,(
% 0.13/0.44 ~op(e1,e1)=op(e2,e1)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f111,plain,(
% 0.13/0.44 ~op(e1,e1)=op(e4,e1)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f117,plain,(
% 0.13/0.44 ~op(e0,e2)=op(e3,e2)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f120,plain,(
% 0.13/0.44 ~op(e1,e2)=op(e3,e2)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f122,plain,(
% 0.13/0.44 ~op(e2,e2)=op(e3,e2)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f123,plain,(
% 0.13/0.44 ~op(e2,e2)=op(e4,e2)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f127,plain,(
% 0.13/0.44 ~op(e0,e3)=op(e3,e3)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f128,plain,(
% 0.13/0.44 ~op(e0,e3)=op(e4,e3)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f132,plain,(
% 0.13/0.44 ~op(e2,e3)=op(e3,e3)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f141,plain,(
% 0.13/0.44 ~op(e1,e4)=op(e4,e4)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f142,plain,(
% 0.13/0.44 ~op(e2,e4)=op(e3,e4)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f147,plain,(
% 0.13/0.44 ~op(e0,e0)=op(e0,e3)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f165,plain,(
% 0.13/0.44 ~op(e2,e0)=op(e2,e1)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f169,plain,(
% 0.13/0.44 ~op(e2,e1)=op(e2,e2)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f182,plain,(
% 0.13/0.44 ~op(e3,e2)=op(e3,e3)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f191,plain,(
% 0.13/0.44 ~op(e4,e1)=op(e4,e4)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f195,plain,(
% 0.13/0.44 ~e0=e1),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.44 fof(f196,plain,(
% 0.13/0.44 ~e0=e2),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.44 fof(f197,plain,(
% 0.13/0.44 ~e0=e3),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.44 fof(f198,plain,(
% 0.13/0.44 ~e0=e4),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.44 fof(f199,plain,(
% 0.13/0.44 ~e1=e2),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.44 fof(f200,plain,(
% 0.13/0.44 ~e1=e3),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.44 fof(f201,plain,(
% 0.13/0.44 ~e1=e4),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.44 fof(f202,plain,(
% 0.13/0.44 ~e2=e3),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.44 fof(f203,plain,(
% 0.13/0.44 ~e2=e4),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.44 fof(f204,plain,(
% 0.13/0.44 ~e3=e4),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.44 fof(f205,plain,(
% 0.13/0.44 e0=op(e1,op(op(e1,e1),op(e1,e1)))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.44 fof(f206,plain,(
% 0.13/0.44 e2=op(op(e1,e1),op(e1,e1))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.44 fof(f207,plain,(
% 0.13/0.44 e3=op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1)))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.44 fof(f208,plain,(
% 0.13/0.44 e4=op(e1,e1)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.44 fof(f209,definition,(
% 0.13/0.44 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.13/0.44 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.13/0.44 fof(f210,definition,(
% 0.13/0.44 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.13/0.44 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.13/0.44 fof(f211,definition,(
% 0.13/0.44 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.13/0.44 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.13/0.44 fof(f212,definition,(
% 0.13/0.44 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.13/0.44 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.13/0.44 fof(f213,definition,(
% 0.13/0.44 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.13/0.44 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.13/0.44 fof(f214,plain,(
% 0.13/0.44 ((((((((((((op(e0,e0)=e0|op(e1,e1)=e0)|op(e2,e2)=e0)|op(e3,e3)=e0)|op(e4,e4)=e0)&((((op(e0,e0)=e1|op(e1,e1)=e1)|op(e2,e2)=e1)|op(e3,e3)=e1)|op(e4,e4)=e1))&((((op(e0,e0)=e2|op(e1,e1)=e2)|op(e2,e2)=e2)|op(e3,e3)=e2)|op(e4,e4)=e2))&((((op(e0,e0)=e3|op(e1,e1)=e3)|op(e2,e2)=e3)|op(e3,e3)=e3)|op(e4,e4)=e3))&((((op(e0,e0)=e4|op(e1,e1)=e4)|op(e2,e2)=e4)|op(e3,e3)=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.13/0.44 inference(formula_renaming,[status(thm)],[f8,f213,f212,f211,f210,f209])).
% 0.13/0.44 fof(f215,plain,(
% 0.13/0.44 op(e0,e0)=e0|op(e1,e1)=e0|op(e2,e2)=e0|op(e3,e3)=e0|op(e4,e4)=e0),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f214])).
% 0.13/0.44 fof(f216,plain,(
% 0.13/0.44 op(e0,e0)=e1|op(e1,e1)=e1|op(e2,e2)=e1|op(e3,e3)=e1|op(e4,e4)=e1),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f214])).
% 0.13/0.44 fof(f223,plain,(
% 0.13/0.44 sP1_prd|op(e1,op(e4,e1))=e4),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f214])).
% 0.13/0.44 fof(f237,definition,(
% 0.13/0.44 sP6_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))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.13/0.44 fof(f238,plain,(
% 0.13/0.44 sP1_prd<=>(sP6_prd|(~op(e3,op(e3,e1))=e1&op(e1,op(e3,e1))=e3))),
% 0.13/0.44 inference(formula_renaming,[status(thm)],[f210,f237])).
% 0.13/0.44 fof(f239,plain,(
% 0.13/0.44 (~sP1_prd|(sP6_prd|(~op(e3,op(e3,e1))=e1&op(e1,op(e3,e1))=e3)))&(sP1_prd|(~sP6_prd&(op(e3,op(e3,e1))=e1|~op(e1,op(e3,e1))=e3)))),
% 0.13/0.44 inference(NNF_transformation,[status(thm)],[f238])).
% 0.13/0.44 fof(f241,plain,(
% 0.13/0.44 ~sP1_prd|sP6_prd|op(e1,op(e3,e1))=e3),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f239])).
% 0.13/0.44 fof(f272,definition,(
% 0.13/0.44 sP11_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))),
% 0.13/0.44 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.13/0.44 fof(f273,plain,(
% 0.13/0.44 sP6_prd<=>(sP11_prd|(~op(e2,op(e2,e1))=e1&op(e1,op(e2,e1))=e2))),
% 0.13/0.44 inference(formula_renaming,[status(thm)],[f237,f272])).
% 0.13/0.44 fof(f274,plain,(
% 0.13/0.44 (~sP6_prd|(sP11_prd|(~op(e2,op(e2,e1))=e1&op(e1,op(e2,e1))=e2)))&(sP6_prd|(~sP11_prd&(op(e2,op(e2,e1))=e1|~op(e1,op(e2,e1))=e2)))),
% 0.13/0.44 inference(NNF_transformation,[status(thm)],[f273])).
% 0.13/0.44 fof(f276,plain,(
% 0.13/0.44 ~sP6_prd|sP11_prd|op(e1,op(e2,e1))=e2),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f274])).
% 0.13/0.44 fof(f307,plain,(
% 0.13/0.44 (~sP11_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)))&(sP11_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)))),
% 0.13/0.44 inference(NNF_transformation,[status(thm)],[f272])).
% 0.13/0.44 fof(f310,plain,(
% 0.13/0.44 ~sP11_prd|op(e1,op(e0,e1))=e0|~op(e1,op(e1,e1))=e1),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f307])).
% 0.13/0.44 fof(f311,plain,(
% 0.13/0.44 ~sP11_prd|op(e1,op(e0,e1))=e0|op(e1,op(e1,e1))=e1),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f307])).
% 0.13/0.44 fof(f335,plain,(
% 0.13/0.44 e0=op(e1,e2)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f206,f205])).
% 0.13/0.44 fof(f336,plain,(
% 0.13/0.44 e3=op(e2,op(op(e1,e1),op(e1,e1)))),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f206,f207])).
% 0.13/0.44 fof(f339,plain,(
% 0.13/0.44 ~op(e2,e1)=e3),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f356,f169])).
% 0.13/0.44 fof(f341,plain,(
% 0.13/0.44 ~e3=op(e4,e2)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f356,f123])).
% 0.13/0.44 fof(f342,plain,(
% 0.13/0.44 ~e3=op(e3,e2)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f356,f122])).
% 0.13/0.44 fof(f352,plain,(
% 0.13/0.44 op(e2,e0)=e1|op(e2,e1)=e1|e3=e1|op(e2,e3)=e1|op(e2,e4)=e1),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f356,f67])).
% 0.13/0.44 fof(f356,plain,(
% 0.13/0.44 e3=op(e2,e2)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f206,f336])).
% 0.13/0.44 fof(f357,plain,(
% 0.13/0.44 e2=op(op(e1,e1),e4)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f208,f206])).
% 0.13/0.44 fof(f362,plain,(
% 0.13/0.44 ~e4=op(e4,e1)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f208,f111])).
% 0.13/0.44 fof(f364,plain,(
% 0.13/0.44 ~e4=op(e2,e1)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f208,f109])).
% 0.13/0.44 fof(f370,plain,(
% 0.13/0.44 op(e0,e1)=e2|e4=e2|op(e2,e1)=e2|op(e3,e1)=e2|op(e4,e1)=e2),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f208,f60])).
% 0.13/0.44 fof(f371,plain,(
% 0.13/0.44 op(e1,e0)=e2|e4=e2|op(e1,e2)=e2|op(e1,e3)=e2|op(e1,e4)=e2),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f208,f59])).
% 0.13/0.44 fof(f377,plain,(
% 0.13/0.44 op(e0,e0)=e0|e4=e0|op(e2,e2)=e0|op(e3,e3)=e0|op(e4,e4)=e0),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f208,f215])).
% 0.13/0.44 fof(f378,plain,(
% 0.13/0.44 op(e0,e0)=e0|e4=e0|e3=e0|op(e3,e3)=e0|op(e4,e4)=e0),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f356,f377])).
% 0.13/0.44 fof(f379,plain,(
% 0.13/0.44 op(e0,e0)=e0|e3=e0|op(e3,e3)=e0|op(e4,e4)=e0),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f378,f198])).
% 0.13/0.44 fof(f380,plain,(
% 0.13/0.44 op(e0,e0)=e1|e4=e1|op(e2,e2)=e1|op(e3,e3)=e1|op(e4,e4)=e1),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f208,f216])).
% 0.13/0.44 fof(f381,plain,(
% 0.13/0.44 op(e0,e0)=e1|e4=e1|e3=e1|op(e3,e3)=e1|op(e4,e4)=e1),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f356,f380])).
% 0.13/0.44 fof(f382,plain,(
% 0.13/0.44 op(e0,e0)=e1|e3=e1|op(e3,e3)=e1|op(e4,e4)=e1),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f381,f201])).
% 0.13/0.44 fof(f399,plain,(
% 0.13/0.44 ~sP11_prd|op(e1,op(e0,e1))=e0|~op(e1,e4)=e1),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f208,f310])).
% 0.13/0.44 fof(f400,plain,(
% 0.13/0.44 ~sP11_prd|op(e1,op(e0,e1))=e0|op(e1,e4)=e1),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f208,f311])).
% 0.13/0.44 fof(f401,plain,(
% 0.13/0.44 ~sP11_prd|op(e1,op(e0,e1))=e0),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f400,f399])).
% 0.13/0.44 fof(f411,plain,(
% 0.13/0.44 ~e0=op(e3,e2)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f335,f120])).
% 0.13/0.44 fof(f418,plain,(
% 0.13/0.44 op(e2,e1)=e0|op(e2,e1)=e1|op(e2,e1)=e2|op(e2,e1)=e4),
% 0.13/0.44 inference(backward_subsumption_resolution,[status(thm)],[f20,f339])).
% 0.13/0.44 fof(f421,plain,(
% 0.13/0.44 op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e3)=e3|op(e4,e4)=e3),
% 0.13/0.44 inference(backward_subsumption_resolution,[status(thm)],[f91,f341])).
% 0.13/0.44 fof(f424,plain,(
% 0.13/0.44 op(e3,e2)=e0|op(e3,e2)=e1|op(e3,e2)=e2|op(e3,e2)=e4),
% 0.13/0.44 inference(backward_subsumption_resolution,[status(thm)],[f26,f342])).
% 0.13/0.44 fof(f436,plain,(
% 0.13/0.44 op(e2,e0)=e1|op(e2,e1)=e1|op(e2,e3)=e1|op(e2,e4)=e1),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f352,f200])).
% 0.13/0.44 fof(f442,plain,(
% 0.13/0.44 op(e0,e0)=e1|e3=e1|op(e3,e3)=e1|e2=e1),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f461,f382])).
% 0.13/0.44 fof(f443,plain,(
% 0.13/0.44 op(e0,e0)=e0|e3=e0|op(e3,e3)=e0|e2=e0),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f461,f379])).
% 0.13/0.44 fof(f446,plain,(
% 0.13/0.44 ~op(e4,e1)=e2),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f461,f191])).
% 0.13/0.44 fof(f450,plain,(
% 0.13/0.44 ~op(e1,e4)=e2),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f461,f141])).
% 0.13/0.44 fof(f461,plain,(
% 0.13/0.44 e2=op(e4,e4)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f208,f357])).
% 0.13/0.44 fof(f477,plain,(
% 0.13/0.44 op(e0,e1)=e2|op(e2,e1)=e2|op(e3,e1)=e2|op(e4,e1)=e2),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f370,f203])).
% 0.13/0.44 fof(f478,plain,(
% 0.13/0.44 op(e1,e0)=e2|e4=e2|e0=e2|op(e1,e3)=e2|op(e1,e4)=e2),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f335,f371])).
% 0.13/0.44 fof(f479,plain,(
% 0.13/0.44 op(e1,e0)=e2|e0=e2|op(e1,e3)=e2|op(e1,e4)=e2),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f478,f203])).
% 0.13/0.44 fof(f491,plain,(
% 0.13/0.44 op(e2,e1)=e0|op(e2,e1)=e1|op(e2,e1)=e2),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f418,f364])).
% 0.13/0.44 fof(f492,plain,(
% 0.13/0.44 op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e3)=e3|e2=e3),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f461,f421])).
% 0.13/0.44 fof(f493,plain,(
% 0.13/0.44 op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e3)=e3),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f492,f202])).
% 0.13/0.44 fof(f495,plain,(
% 0.13/0.44 op(e3,e2)=e1|op(e3,e2)=e2|op(e3,e2)=e4),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f424,f411])).
% 0.13/0.44 fof(f497,plain,(
% 0.13/0.44 op(e0,e0)=e1|op(e3,e3)=e1|e2=e1),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f442,f200])).
% 0.13/0.44 fof(f498,plain,(
% 0.13/0.44 op(e0,e0)=e0|op(e3,e3)=e0|e2=e0),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f443,f197])).
% 0.13/0.44 fof(f503,plain,(
% 0.13/0.44 op(e0,e1)=e2|op(e2,e1)=e2|op(e3,e1)=e2),
% 0.13/0.44 inference(backward_subsumption_resolution,[status(thm)],[f477,f446])).
% 0.13/0.44 fof(f510,plain,(
% 0.13/0.44 op(e1,e0)=e2|e0=e2|op(e1,e3)=e2),
% 0.13/0.44 inference(backward_subsumption_resolution,[status(thm)],[f479,f450])).
% 0.13/0.44 fof(f526,plain,(
% 0.13/0.44 op(e1,e0)=e2|op(e1,e3)=e2),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f510,f196])).
% 0.13/0.44 fof(f545,plain,(
% 0.13/0.44 op(e4,e4)=e4|unit=e0|unit=e1|unit=e2|unit=e3),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f44,f43])).
% 0.13/0.44 fof(f559,plain,(
% 0.13/0.44 e2=e4|unit=e0|unit=e1|unit=e2|unit=e3),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f461,f545])).
% 0.13/0.44 fof(f560,plain,(
% 0.13/0.44 unit=e0|unit=e1|unit=e2|unit=e3),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f559,f203])).
% 0.13/0.44 fof(f584,plain,(
% 0.13/0.44 ~op(e2,e4)=e1|op(e3,e0)=e1|op(e3,e1)=e1|op(e3,e2)=e1|op(e3,e3)=e1),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f77,f142])).
% 0.13/0.44 fof(f655,plain,(
% 0.13/0.44 op(e0,e3)=e0|unit=e0|unit=e1|unit=e2),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f560,f35])).
% 0.13/0.44 fof(f669,plain,(
% 0.13/0.44 ~op(e3,e2)=e1|op(e0,e0)=e1|e2=e1),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f497,f182])).
% 0.13/0.44 fof(f672,plain,(
% 0.13/0.44 ~op(e2,e3)=e1|op(e0,e0)=e1|e2=e1),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f497,f132])).
% 0.13/0.44 fof(f676,plain,(
% 0.13/0.44 ~op(e3,e2)=e1|op(e0,e0)=e1),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f669,f199])).
% 0.13/0.44 fof(f680,plain,(
% 0.13/0.44 ~op(e2,e3)=e1|op(e0,e0)=e1),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f672,f199])).
% 0.13/0.44 fof(f714,plain,(
% 0.13/0.44 ~op(e0,e3)=e0|op(e0,e0)=e0|e2=e0),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f498,f127])).
% 0.13/0.44 fof(f722,plain,(
% 0.13/0.44 ~op(e0,e3)=e0|op(e0,e0)=e0),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f714,f196])).
% 0.13/0.44 fof(f817,plain,(
% 0.13/0.44 unit=e0|unit=e1|unit=e2|op(e0,e0)=e0),
% 0.13/0.44 inference(resolution,[status(thm)],[f655,f722])).
% 0.13/0.44 fof(f823,plain,(
% 0.13/0.44 ~op(e0,e0)=e0|unit=e0|unit=e1|unit=e2),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f655,f147])).
% 0.13/0.44 fof(f826,plain,(
% 0.13/0.44 unit=e0|unit=e1|unit=e2),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f823,f817])).
% 0.13/0.44 fof(f829,plain,(
% 0.13/0.44 op(e3,e2)=e3|unit=e0|unit=e1),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f826,f41])).
% 0.13/0.44 fof(f839,plain,(
% 0.13/0.44 unit=e0|unit=e1),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f829,f342])).
% 0.13/0.44 fof(f843,plain,(
% 0.13/0.44 op(e4,e1)=e4|unit=e0),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f839,f43])).
% 0.13/0.44 fof(f855,plain,(
% 0.13/0.44 op(e4,e0)=e4),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f865,f43])).
% 0.13/0.44 fof(f857,plain,(
% 0.13/0.44 op(e3,e0)=e3),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f865,f41])).
% 0.13/0.44 fof(f858,plain,(
% 0.13/0.44 op(e0,e3)=e3),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f865,f40])).
% 0.13/0.44 fof(f859,plain,(
% 0.13/0.44 op(e2,e0)=e2),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f865,f39])).
% 0.13/0.44 fof(f860,plain,(
% 0.13/0.44 op(e0,e2)=e2),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f865,f38])).
% 0.13/0.44 fof(f861,plain,(
% 0.13/0.44 op(e1,e0)=e1),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f865,f37])).
% 0.13/0.44 fof(f862,plain,(
% 0.13/0.44 op(e0,e1)=e1),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f865,f36])).
% 0.13/0.44 fof(f863,plain,(
% 0.13/0.44 op(e0,e0)=e0),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f865,f35])).
% 0.13/0.44 fof(f865,plain,(
% 0.13/0.44 unit=e0),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f843,f362])).
% 0.13/0.44 fof(f888,plain,(
% 0.13/0.44 e4=e3|op(e4,e1)=e3|op(e4,e3)=e3),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f855,f493])).
% 0.13/0.44 fof(f942,plain,(
% 0.13/0.44 ~op(e2,e4)=e1|e3=e1|op(e3,e1)=e1|op(e3,e2)=e1|op(e3,e3)=e1),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f857,f584])).
% 0.13/0.44 fof(f962,plain,(
% 0.13/0.44 ~e3=op(e4,e3)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f858,f128])).
% 0.13/0.44 fof(f996,plain,(
% 0.13/0.44 ~e2=op(e2,e1)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f859,f165])).
% 0.13/0.44 fof(f1007,plain,(
% 0.13/0.44 e2=e1|op(e2,e1)=e1|op(e2,e3)=e1|op(e2,e4)=e1),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f859,f436])).
% 0.13/0.44 fof(f1016,plain,(
% 0.13/0.44 ~e2=op(e3,e2)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f860,f117])).
% 0.13/0.44 fof(f1025,plain,(
% 0.13/0.44 e1=e2|op(e1,e3)=e2),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f861,f526])).
% 0.13/0.44 fof(f1040,plain,(
% 0.13/0.44 ~sP11_prd|op(e1,e1)=e0),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f862,f401])).
% 0.13/0.44 fof(f1043,plain,(
% 0.13/0.44 ~e1=op(e3,e1)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f862,f107])).
% 0.13/0.44 fof(f1044,plain,(
% 0.13/0.44 ~e1=op(e2,e1)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f862,f106])).
% 0.13/0.44 fof(f1047,plain,(
% 0.13/0.44 e1=e2|op(e2,e1)=e2|op(e3,e1)=e2),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f862,f503])).
% 0.13/0.44 fof(f1056,plain,(
% 0.13/0.44 ~op(e2,e3)=e1|e0=e1),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f863,f680])).
% 0.13/0.44 fof(f1058,plain,(
% 0.13/0.44 ~op(e3,e2)=e1|e0=e1),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f863,f676])).
% 0.13/0.44 fof(f1083,plain,(
% 0.13/0.44 op(e4,e1)=e3|op(e4,e3)=e3),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f888,f204])).
% 0.13/0.44 fof(f1147,plain,(
% 0.13/0.44 ~op(e2,e4)=e1|op(e3,e1)=e1|op(e3,e2)=e1|op(e3,e3)=e1),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f942,f200])).
% 0.13/0.44 fof(f1164,plain,(
% 0.13/0.44 op(e4,e1)=e3),
% 0.13/0.44 inference(backward_subsumption_resolution,[status(thm)],[f1083,f962])).
% 0.13/0.44 fof(f1199,plain,(
% 0.13/0.44 op(e2,e1)=e0|op(e2,e1)=e1),
% 0.13/0.44 inference(backward_subsumption_resolution,[status(thm)],[f491,f996])).
% 0.13/0.44 fof(f1217,plain,(
% 0.13/0.44 op(e2,e1)=e1|op(e2,e3)=e1|op(e2,e4)=e1),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1007,f199])).
% 0.13/0.46 fof(f1225,plain,(
% 0.13/0.46 op(e3,e2)=e1|op(e3,e2)=e4),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f495,f1016])).
% 0.13/0.46 fof(f1251,plain,(
% 0.13/0.46 op(e1,e3)=e2),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1025,f199])).
% 0.13/0.46 fof(f1270,plain,(
% 0.13/0.46 ~sP11_prd|e4=e0),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f208,f1040])).
% 0.13/0.46 fof(f1271,plain,(
% 0.13/0.46 ~sP6_prd|op(e1,op(e2,e1))=e2),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f276,f1277])).
% 0.13/0.46 fof(f1277,plain,(
% 0.13/0.46 ~sP11_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1270,f198])).
% 0.13/0.46 fof(f1281,plain,(
% 0.13/0.46 ~op(e2,e4)=e1|op(e3,e2)=e1|op(e3,e3)=e1),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1147,f1043])).
% 0.13/0.46 fof(f1283,plain,(
% 0.13/0.46 op(e2,e3)=e1|op(e2,e4)=e1),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1217,f1044])).
% 0.13/0.46 fof(f1285,plain,(
% 0.13/0.46 op(e2,e1)=e2|op(e3,e1)=e2),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1047,f199])).
% 0.13/0.46 fof(f1290,plain,(
% 0.13/0.46 ~op(e2,e3)=e1),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1056,f195])).
% 0.13/0.46 fof(f1291,plain,(
% 0.13/0.46 ~op(e3,e2)=e1),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1058,f195])).
% 0.13/0.46 fof(f1319,plain,(
% 0.13/0.46 sP1_prd|op(e1,e3)=e4),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1164,f223])).
% 0.13/0.46 fof(f1333,plain,(
% 0.13/0.46 e0=e2|op(e3,e1)=e2),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1338,f1285])).
% 0.13/0.46 fof(f1338,plain,(
% 0.13/0.46 op(e2,e1)=e0),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1199,f1044])).
% 0.13/0.46 fof(f1349,plain,(
% 0.13/0.46 op(e3,e2)=e4),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1225,f1291])).
% 0.13/0.46 fof(f1370,plain,(
% 0.13/0.46 ~sP6_prd|op(e1,e0)=e2),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1338,f1271])).
% 0.13/0.46 fof(f1371,plain,(
% 0.13/0.46 ~sP6_prd|e1=e2),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f861,f1370])).
% 0.13/0.46 fof(f1372,plain,(
% 0.13/0.46 ~sP1_prd|op(e1,op(e3,e1))=e3),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f241,f1374])).
% 0.13/0.46 fof(f1374,plain,(
% 0.13/0.46 ~sP6_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1371,f199])).
% 0.13/0.46 fof(f1388,plain,(
% 0.13/0.46 ~op(e2,e4)=e1|e4=e1|op(e3,e3)=e1),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1349,f1281])).
% 0.13/0.46 fof(f1389,plain,(
% 0.13/0.46 ~op(e2,e4)=e1|op(e3,e3)=e1),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1388,f201])).
% 0.13/0.46 fof(f1399,plain,(
% 0.13/0.46 ~e1=e1|op(e3,e3)=e1),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1405,f1389])).
% 0.13/0.46 fof(f1405,plain,(
% 0.13/0.46 op(e2,e4)=e1),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1283,f1290])).
% 0.13/0.46 fof(f1431,plain,(
% 0.13/0.46 sP1_prd|e2=e4),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1251,f1319])).
% 0.13/0.46 fof(f1434,plain,(
% 0.13/0.46 sP1_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1431,f203])).
% 0.13/0.46 fof(f1449,plain,(
% 0.13/0.46 op(e3,e1)=e2),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1333,f196])).
% 0.13/0.46 fof(f1456,plain,(
% 0.13/0.46 ~sP1_prd|op(e1,e2)=e3),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1449,f1372])).
% 0.13/0.46 fof(f1457,plain,(
% 0.13/0.46 ~sP1_prd|e0=e3),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f335,f1456])).
% 0.13/0.46 fof(f1503,plain,(
% 0.13/0.46 e0=e3),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1457,f1434])).
% 0.13/0.46 fof(f1520,plain,(
% 0.13/0.46 ~e1=e1|op(e0,e3)=e1),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1503,f1399])).
% 0.13/0.46 fof(f1521,plain,(
% 0.13/0.46 ~e1=e1|e3=e1),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f858,f1520])).
% 0.13/0.46 fof(f1522,plain,(
% 0.13/0.46 ~e1=e1|e0=e1),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1503,f1521])).
% 0.13/0.46 fof(f1523,plain,(
% 0.13/0.46 e0=e1),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1522])).
% 0.13/0.46 fof(f1524,plain,(
% 0.13/0.46 $false),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1523,f195])).
% 0.13/0.46 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.48 % Elapsed time: 0.114340 seconds
% 0.13/0.48 % CPU time: 0.566587 seconds
% 0.13/0.48 % Total memory used: 80.641 MB
% 0.13/0.48 % Net memory used: 80.492 MB
%------------------------------------------------------------------------------