%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG025+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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:47:47 AM UTC 2026
% Result : Theorem 0.15s 0.50s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 3
% Syntax : Number of formulae : 46 ( 21 unt; 0 def)
% Number of atoms : 539 ( 538 equ)
% Maximal formula atoms : 72 ( 11 avg)
% Number of connectives : 816 ( 323 ~; 305 |; 188 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 39 ( 10 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 7 con; 0-2 aty)
% Number of variables : 0 ( 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
( ( unit = e5
| unit = e4
| unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& op(e5,unit) = e5
& op(unit,e5) = e5
& op(e4,unit) = e4
& op(unit,e4) = e4
& op(e3,unit) = e3
& op(unit,e3) = e3
& op(e2,unit) = e2
& op(unit,e2) = e2
& op(e1,unit) = e1
& op(unit,e1) = e1
& op(e0,unit) = e0
& op(unit,e0) = e0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
unit = e0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,conjecture,
( ~ ( op(e5,e5) = op(e5,e5)
& op(e5,e4) = op(e4,e5)
& op(e5,e3) = op(e3,e5)
& op(e5,e2) = op(e2,e5)
& op(e5,e1) = op(e1,e5)
& op(e5,e0) = op(e0,e5)
& op(e4,e5) = op(e5,e4)
& op(e4,e4) = op(e4,e4)
& op(e4,e3) = op(e3,e4)
& op(e4,e2) = op(e2,e4)
& op(e4,e1) = op(e1,e4)
& op(e4,e0) = op(e0,e4)
& op(e3,e5) = op(e5,e3)
& op(e3,e4) = op(e4,e3)
& op(e3,e3) = op(e3,e3)
& op(e3,e2) = op(e2,e3)
& op(e3,e1) = op(e1,e3)
& op(e3,e0) = op(e0,e3)
& op(e2,e5) = op(e5,e2)
& op(e2,e4) = op(e4,e2)
& op(e2,e3) = op(e3,e2)
& op(e2,e2) = op(e2,e2)
& op(e2,e1) = op(e1,e2)
& op(e2,e0) = op(e0,e2)
& op(e1,e5) = op(e5,e1)
& op(e1,e4) = op(e4,e1)
& op(e1,e3) = op(e3,e1)
& op(e1,e2) = op(e2,e1)
& op(e1,e1) = op(e1,e1)
& op(e1,e0) = op(e0,e1)
& op(e0,e5) = op(e5,e0)
& op(e0,e4) = op(e4,e0)
& op(e0,e3) = op(e3,e0)
& op(e0,e2) = op(e2,e0)
& op(e0,e1) = op(e1,e0)
& op(e0,e0) = op(e0,e0) )
| ( op(e5,e5) = op(e5,e5)
& op(e5,e4) = op(e4,e5)
& op(e5,e3) = op(e3,e5)
& op(e5,e2) = op(e2,e5)
& op(e5,e1) = op(e1,e5)
& op(e5,e0) = op(e0,e5)
& op(e4,e5) = op(e5,e4)
& op(e4,e4) = op(e4,e4)
& op(e4,e3) = op(e3,e4)
& op(e4,e2) = op(e2,e4)
& op(e4,e1) = op(e1,e4)
& op(e4,e0) = op(e0,e4)
& op(e3,e5) = op(e5,e3)
& op(e3,e4) = op(e4,e3)
& op(e3,e3) = op(e3,e3)
& op(e3,e2) = op(e2,e3)
& op(e3,e1) = op(e1,e3)
& op(e3,e0) = op(e0,e3)
& op(e2,e5) = op(e5,e2)
& op(e2,e4) = op(e4,e2)
& op(e2,e3) = op(e3,e2)
& op(e2,e2) = op(e2,e2)
& op(e2,e1) = op(e1,e2)
& op(e2,e0) = op(e0,e2)
& op(e1,e5) = op(e5,e1)
& op(e1,e4) = op(e4,e1)
& op(e1,e3) = op(e3,e1)
& op(e1,e2) = op(e2,e1)
& op(e1,e1) = op(e1,e1)
& op(e1,e0) = op(e0,e1)
& op(e0,e5) = op(e5,e0)
& op(e0,e4) = op(e4,e0)
& op(e0,e3) = op(e3,e0)
& op(e0,e2) = op(e2,e0)
& op(e0,e1) = op(e1,e0)
& op(e0,e0) = op(e0,e0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
~ ( ~ ( op(e5,e5) = op(e5,e5)
& op(e5,e4) = op(e4,e5)
& op(e5,e3) = op(e3,e5)
& op(e5,e2) = op(e2,e5)
& op(e5,e1) = op(e1,e5)
& op(e5,e0) = op(e0,e5)
& op(e4,e5) = op(e5,e4)
& op(e4,e4) = op(e4,e4)
& op(e4,e3) = op(e3,e4)
& op(e4,e2) = op(e2,e4)
& op(e4,e1) = op(e1,e4)
& op(e4,e0) = op(e0,e4)
& op(e3,e5) = op(e5,e3)
& op(e3,e4) = op(e4,e3)
& op(e3,e3) = op(e3,e3)
& op(e3,e2) = op(e2,e3)
& op(e3,e1) = op(e1,e3)
& op(e3,e0) = op(e0,e3)
& op(e2,e5) = op(e5,e2)
& op(e2,e4) = op(e4,e2)
& op(e2,e3) = op(e3,e2)
& op(e2,e2) = op(e2,e2)
& op(e2,e1) = op(e1,e2)
& op(e2,e0) = op(e0,e2)
& op(e1,e5) = op(e5,e1)
& op(e1,e4) = op(e4,e1)
& op(e1,e3) = op(e3,e1)
& op(e1,e2) = op(e2,e1)
& op(e1,e1) = op(e1,e1)
& op(e1,e0) = op(e0,e1)
& op(e0,e5) = op(e5,e0)
& op(e0,e4) = op(e4,e0)
& op(e0,e3) = op(e3,e0)
& op(e0,e2) = op(e2,e0)
& op(e0,e1) = op(e1,e0)
& op(e0,e0) = op(e0,e0) )
| ( op(e5,e5) = op(e5,e5)
& op(e5,e4) = op(e4,e5)
& op(e5,e3) = op(e3,e5)
& op(e5,e2) = op(e2,e5)
& op(e5,e1) = op(e1,e5)
& op(e5,e0) = op(e0,e5)
& op(e4,e5) = op(e5,e4)
& op(e4,e4) = op(e4,e4)
& op(e4,e3) = op(e3,e4)
& op(e4,e2) = op(e2,e4)
& op(e4,e1) = op(e1,e4)
& op(e4,e0) = op(e0,e4)
& op(e3,e5) = op(e5,e3)
& op(e3,e4) = op(e4,e3)
& op(e3,e3) = op(e3,e3)
& op(e3,e2) = op(e2,e3)
& op(e3,e1) = op(e1,e3)
& op(e3,e0) = op(e0,e3)
& op(e2,e5) = op(e5,e2)
& op(e2,e4) = op(e4,e2)
& op(e2,e3) = op(e3,e2)
& op(e2,e2) = op(e2,e2)
& op(e2,e1) = op(e1,e2)
& op(e2,e0) = op(e0,e2)
& op(e1,e5) = op(e5,e1)
& op(e1,e4) = op(e4,e1)
& op(e1,e3) = op(e3,e1)
& op(e1,e2) = op(e2,e1)
& op(e1,e1) = op(e1,e1)
& op(e1,e0) = op(e0,e1)
& op(e0,e5) = op(e5,e0)
& op(e0,e4) = op(e4,e0)
& op(e0,e3) = op(e3,e0)
& op(e0,e2) = op(e2,e0)
& op(e0,e1) = op(e1,e0)
& op(e0,e0) = op(e0,e0) ) ),
inference(negated_conjecture,[status(cth)],[f12]) ).
fof(f276,plain,
op(unit,e5) = e5,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f277,plain,
op(e5,unit) = e5,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f297,plain,
unit = e0,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f552,plain,
( op(e5,e5) = op(e5,e5)
& op(e5,e4) = op(e4,e5)
& op(e5,e3) = op(e3,e5)
& op(e5,e2) = op(e2,e5)
& op(e5,e1) = op(e1,e5)
& op(e5,e0) = op(e0,e5)
& op(e4,e5) = op(e5,e4)
& op(e4,e4) = op(e4,e4)
& op(e4,e3) = op(e3,e4)
& op(e4,e2) = op(e2,e4)
& op(e4,e1) = op(e1,e4)
& op(e4,e0) = op(e0,e4)
& op(e3,e5) = op(e5,e3)
& op(e3,e4) = op(e4,e3)
& op(e3,e3) = op(e3,e3)
& op(e3,e2) = op(e2,e3)
& op(e3,e1) = op(e1,e3)
& op(e3,e0) = op(e0,e3)
& op(e2,e5) = op(e5,e2)
& op(e2,e4) = op(e4,e2)
& op(e2,e3) = op(e3,e2)
& op(e2,e2) = op(e2,e2)
& op(e2,e1) = op(e1,e2)
& op(e2,e0) = op(e0,e2)
& op(e1,e5) = op(e5,e1)
& op(e1,e4) = op(e4,e1)
& op(e1,e3) = op(e3,e1)
& op(e1,e2) = op(e2,e1)
& op(e1,e1) = op(e1,e1)
& op(e1,e0) = op(e0,e1)
& op(e0,e5) = op(e5,e0)
& op(e0,e4) = op(e4,e0)
& op(e0,e3) = op(e3,e0)
& op(e0,e2) = op(e2,e0)
& op(e0,e1) = op(e1,e0)
& op(e0,e0) = op(e0,e0)
& ( op(e5,e5) != op(e5,e5)
| op(e5,e4) != op(e4,e5)
| op(e5,e3) != op(e3,e5)
| op(e5,e2) != op(e2,e5)
| op(e5,e1) != op(e1,e5)
| op(e5,e0) != op(e0,e5)
| op(e4,e5) != op(e5,e4)
| op(e4,e4) != op(e4,e4)
| op(e4,e3) != op(e3,e4)
| op(e4,e2) != op(e2,e4)
| op(e4,e1) != op(e1,e4)
| op(e4,e0) != op(e0,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e3,e3) != op(e3,e3)
| op(e3,e2) != op(e2,e3)
| op(e3,e1) != op(e1,e3)
| op(e3,e0) != op(e0,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e2,e2) != op(e2,e2)
| op(e2,e1) != op(e1,e2)
| op(e2,e0) != op(e0,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e2) != op(e2,e1)
| op(e1,e1) != op(e1,e1)
| op(e1,e0) != op(e0,e1)
| op(e0,e5) != op(e5,e0)
| op(e0,e4) != op(e4,e0)
| op(e0,e3) != op(e3,e0)
| op(e0,e2) != op(e2,e0)
| op(e0,e1) != op(e1,e0)
| op(e0,e0) != op(e0,e0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f553,plain,
( op(e5,e5) != op(e5,e5)
| op(e5,e4) != op(e4,e5)
| op(e5,e3) != op(e3,e5)
| op(e5,e2) != op(e2,e5)
| op(e5,e1) != op(e1,e5)
| op(e5,e0) != op(e0,e5)
| op(e4,e5) != op(e5,e4)
| op(e4,e4) != op(e4,e4)
| op(e4,e3) != op(e3,e4)
| op(e4,e2) != op(e2,e4)
| op(e4,e1) != op(e1,e4)
| op(e4,e0) != op(e0,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e3,e3) != op(e3,e3)
| op(e3,e2) != op(e2,e3)
| op(e3,e1) != op(e1,e3)
| op(e3,e0) != op(e0,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e2,e2) != op(e2,e2)
| op(e2,e1) != op(e1,e2)
| op(e2,e0) != op(e0,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e2) != op(e2,e1)
| op(e1,e1) != op(e1,e1)
| op(e1,e0) != op(e0,e1)
| op(e0,e5) != op(e5,e0)
| op(e0,e4) != op(e4,e0)
| op(e0,e3) != op(e3,e0)
| op(e0,e2) != op(e2,e0)
| op(e0,e1) != op(e1,e0)
| op(e0,e0) != op(e0,e0) ),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f555,plain,
op(e0,e1) = op(e1,e0),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f556,plain,
op(e0,e2) = op(e2,e0),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f557,plain,
op(e0,e3) = op(e3,e0),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f558,plain,
op(e0,e4) = op(e4,e0),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f562,plain,
op(e1,e2) = op(e2,e1),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f563,plain,
op(e1,e3) = op(e3,e1),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f564,plain,
op(e1,e4) = op(e4,e1),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f565,plain,
op(e1,e5) = op(e5,e1),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f569,plain,
op(e2,e3) = op(e3,e2),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f570,plain,
op(e2,e4) = op(e4,e2),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f571,plain,
op(e2,e5) = op(e5,e2),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f576,plain,
op(e3,e4) = op(e4,e3),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f577,plain,
op(e3,e5) = op(e5,e3),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f583,plain,
op(e4,e5) = op(e5,e4),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f590,plain,
( op(e5,e5) != op(e5,e5)
| op(e4,e5) != op(e5,e4)
| op(e4,e4) != op(e4,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e3,e3) != op(e3,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e2,e2) != op(e2,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e2) != op(e2,e1)
| op(e1,e1) != op(e1,e1)
| op(e0,e5) != op(e5,e0)
| op(e0,e4) != op(e4,e0)
| op(e0,e3) != op(e3,e0)
| op(e0,e2) != op(e2,e0)
| op(e0,e1) != op(e1,e0)
| op(e0,e0) != op(e0,e0) ),
inference(duplicate_literals_removal,[status(thm)],[f553]) ).
fof(f591,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e2) != op(e2,e1)
| op(e0,e5) != op(e5,e0)
| op(e0,e4) != op(e4,e0)
| op(e0,e3) != op(e3,e0)
| op(e0,e2) != op(e2,e0)
| op(e0,e1) != op(e1,e0) ),
inference(trivial_equality_resolution,[status(thm)],[f590]) ).
fof(f592,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e2) != op(e2,e1)
| op(e0,e5) != op(e5,e0)
| op(e0,e4) != op(e4,e0)
| op(e0,e3) != op(e3,e0)
| op(e0,e2) != op(e2,e0)
| op(e0,e1) != op(e0,e1) ),
inference(forward_demodulation,[status(thm)],[f555,f591]) ).
fof(f593,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e2) != op(e2,e1)
| op(e0,e5) != op(e5,e0)
| op(e0,e4) != op(e4,e0)
| op(e0,e3) != op(e3,e0)
| op(e0,e2) != op(e0,e2)
| op(e0,e1) != op(e0,e1) ),
inference(forward_demodulation,[status(thm)],[f556,f592]) ).
fof(f594,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e2) != op(e2,e1)
| op(e0,e5) != op(e5,e0)
| op(e0,e4) != op(e4,e0)
| op(e0,e3) != op(e0,e3)
| op(e0,e2) != op(e0,e2)
| op(e0,e1) != op(e0,e1) ),
inference(forward_demodulation,[status(thm)],[f557,f593]) ).
fof(f595,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e2) != op(e2,e1)
| op(e0,e5) != op(e5,e0)
| op(e0,e4) != op(e4,e0) ),
inference(trivial_equality_resolution,[status(thm)],[f594]) ).
fof(f621,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e2) != op(e2,e1)
| op(e0,e5) != op(e5,e0)
| op(e0,e4) != op(e0,e4) ),
inference(backward_demodulation,[status(thm)],[f558,f595]) ).
fof(f622,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e2) != op(e2,e1)
| op(e0,e5) != op(e5,e0) ),
inference(trivial_equality_resolution,[status(thm)],[f621]) ).
fof(f710,plain,
op(e0,e5) = e5,
inference(forward_demodulation,[status(thm)],[f297,f276]) ).
fof(f711,plain,
op(e5,e0) = e5,
inference(forward_demodulation,[status(thm)],[f297,f277]) ).
fof(f1010,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e2) != op(e2,e1)
| e5 != op(e5,e0) ),
inference(forward_demodulation,[status(thm)],[f710,f622]) ).
fof(f1011,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e2) != op(e2,e1)
| e5 != e5 ),
inference(forward_demodulation,[status(thm)],[f711,f1010]) ).
fof(f1012,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e3,e1)
| op(e1,e2) != op(e1,e2)
| e5 != e5 ),
inference(forward_demodulation,[status(thm)],[f562,f1011]) ).
fof(f1013,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e4,e1)
| op(e1,e3) != op(e1,e3)
| op(e1,e2) != op(e1,e2)
| e5 != e5 ),
inference(forward_demodulation,[status(thm)],[f563,f1012]) ).
fof(f1014,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e1,e5) != op(e5,e1)
| op(e1,e4) != op(e1,e4)
| op(e1,e3) != op(e1,e3)
| op(e1,e2) != op(e1,e2)
| e5 != e5 ),
inference(forward_demodulation,[status(thm)],[f564,f1013]) ).
fof(f1015,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e3,e2)
| op(e1,e5) != op(e1,e5)
| op(e1,e4) != op(e1,e4)
| op(e1,e3) != op(e1,e3)
| op(e1,e2) != op(e1,e2)
| e5 != e5 ),
inference(forward_demodulation,[status(thm)],[f565,f1014]) ).
fof(f1016,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e4,e2)
| op(e2,e3) != op(e2,e3)
| op(e1,e5) != op(e1,e5)
| op(e1,e4) != op(e1,e4)
| op(e1,e3) != op(e1,e3)
| op(e1,e2) != op(e1,e2)
| e5 != e5 ),
inference(forward_demodulation,[status(thm)],[f569,f1015]) ).
fof(f1017,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e5,e2)
| op(e2,e4) != op(e2,e4)
| op(e2,e3) != op(e2,e3)
| op(e1,e5) != op(e1,e5)
| op(e1,e4) != op(e1,e4)
| op(e1,e3) != op(e1,e3)
| op(e1,e2) != op(e1,e2)
| e5 != e5 ),
inference(forward_demodulation,[status(thm)],[f570,f1016]) ).
fof(f1018,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e4,e3)
| op(e2,e5) != op(e2,e5)
| op(e2,e4) != op(e2,e4)
| op(e2,e3) != op(e2,e3)
| op(e1,e5) != op(e1,e5)
| op(e1,e4) != op(e1,e4)
| op(e1,e3) != op(e1,e3)
| op(e1,e2) != op(e1,e2)
| e5 != e5 ),
inference(forward_demodulation,[status(thm)],[f571,f1017]) ).
fof(f1019,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e5,e3)
| op(e3,e4) != op(e3,e4)
| op(e2,e5) != op(e2,e5)
| op(e2,e4) != op(e2,e4)
| op(e2,e3) != op(e2,e3)
| op(e1,e5) != op(e1,e5)
| op(e1,e4) != op(e1,e4)
| op(e1,e3) != op(e1,e3)
| op(e1,e2) != op(e1,e2)
| e5 != e5 ),
inference(forward_demodulation,[status(thm)],[f576,f1018]) ).
fof(f1020,plain,
( op(e4,e5) != op(e5,e4)
| op(e3,e5) != op(e3,e5)
| op(e3,e4) != op(e3,e4)
| op(e2,e5) != op(e2,e5)
| op(e2,e4) != op(e2,e4)
| op(e2,e3) != op(e2,e3)
| op(e1,e5) != op(e1,e5)
| op(e1,e4) != op(e1,e4)
| op(e1,e3) != op(e1,e3)
| op(e1,e2) != op(e1,e2)
| e5 != e5 ),
inference(forward_demodulation,[status(thm)],[f577,f1019]) ).
fof(f1021,plain,
( op(e4,e5) != op(e4,e5)
| op(e3,e5) != op(e3,e5)
| op(e3,e4) != op(e3,e4)
| op(e2,e5) != op(e2,e5)
| op(e2,e4) != op(e2,e4)
| op(e2,e3) != op(e2,e3)
| op(e1,e5) != op(e1,e5)
| op(e1,e4) != op(e1,e4)
| op(e1,e3) != op(e1,e3)
| op(e1,e2) != op(e1,e2)
| e5 != e5 ),
inference(forward_demodulation,[status(thm)],[f583,f1020]) ).
fof(f1022,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f1021]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG025+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n009.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 12:53:28 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.46 % Drodi V4.1.1
% 0.15/0.50 % Refutation found
% 0.15/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.54 % Elapsed time: 0.104575 seconds
% 0.15/0.54 % CPU time: 0.367687 seconds
% 0.15/0.54 % Total memory used: 86.894 MB
% 0.15/0.54 % Net memory used: 86.292 MB
%------------------------------------------------------------------------------