%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG025+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 : n019.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:28 AM UTC 2026
% Result : Theorem 0.15s 5.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG025+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.11/5.38 % Computer : n019.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Mon Sep 21 12:53:42 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.15/5.40 % Drodi V4.1.1
% 0.15/5.42 % Refutation found
% 0.15/5.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/5.42 % SZS output start CNFRefutation for theBenchmark
% 0.15/5.42 fof(f12,conjecture,(
% 0.15/5.42 ( ( op(e0,e0) = op(e0,e0)& op(e0,e1) = op(e1,e0)& op(e0,e2) = op(e2,e0)& op(e0,e3) = op(e3,e0)& op(e0,e4) = op(e4,e0)& op(e0,e5) = op(e5,e0)& op(e1,e0) = op(e0,e1)& op(e1,e1) = op(e1,e1)& op(e1,e2) = op(e2,e1)& op(e1,e3) = op(e3,e1)& op(e1,e4) = op(e4,e1)& op(e1,e5) = op(e5,e1)& op(e2,e0) = op(e0,e2)& op(e2,e1) = op(e1,e2)& op(e2,e2) = op(e2,e2)& op(e2,e3) = op(e3,e2)& op(e2,e4) = op(e4,e2)& op(e2,e5) = op(e5,e2)& op(e3,e0) = op(e0,e3)& op(e3,e1) = op(e1,e3)& op(e3,e2) = op(e2,e3)& op(e3,e3) = op(e3,e3)& op(e3,e4) = op(e4,e3)& op(e3,e5) = op(e5,e3)& op(e4,e0) = op(e0,e4)& op(e4,e1) = op(e1,e4)& op(e4,e2) = op(e2,e4)& op(e4,e3) = op(e3,e4)& op(e4,e4) = op(e4,e4)& op(e4,e5) = op(e5,e4)& op(e5,e0) = op(e0,e5)& op(e5,e1) = op(e1,e5)& op(e5,e2) = op(e2,e5)& op(e5,e3) = op(e3,e5)& op(e5,e4) = op(e4,e5)& op(e5,e5) = op(e5,e5) )| ~ ( op(e0,e0) = op(e0,e0)& op(e0,e1) = op(e1,e0)& op(e0,e2) = op(e2,e0)& op(e0,e3) = op(e3,e0)& op(e0,e4) = op(e4,e0)& op(e0,e5) = op(e5,e0)& op(e1,e0) = op(e0,e1)& op(e1,e1) = op(e1,e1)& op(e1,e2) = op(e2,e1)& op(e1,e3) = op(e3,e1)& op(e1,e4) = op(e4,e1)& op(e1,e5) = op(e5,e1)& op(e2,e0) = op(e0,e2)& op(e2,e1) = op(e1,e2)& op(e2,e2) = op(e2,e2)& op(e2,e3) = op(e3,e2)& op(e2,e4) = op(e4,e2)& op(e2,e5) = op(e5,e2)& op(e3,e0) = op(e0,e3)& op(e3,e1) = op(e1,e3)& op(e3,e2) = op(e2,e3)& op(e3,e3) = op(e3,e3)& op(e3,e4) = op(e4,e3)& op(e3,e5) = op(e5,e3)& op(e4,e0) = op(e0,e4)& op(e4,e1) = op(e1,e4)& op(e4,e2) = op(e2,e4)& op(e4,e3) = op(e3,e4)& op(e4,e4) = op(e4,e4)& op(e4,e5) = op(e5,e4)& op(e5,e0) = op(e0,e5)& op(e5,e1) = op(e1,e5)& op(e5,e2) = op(e2,e5)& op(e5,e3) = op(e3,e5)& op(e5,e4) = op(e4,e5)& op(e5,e5) = op(e5,e5) ) ) ),
% 0.15/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f13,negated_conjecture,(
% 0.15/5.42 ~(( ( op(e0,e0) = op(e0,e0)& op(e0,e1) = op(e1,e0)& op(e0,e2) = op(e2,e0)& op(e0,e3) = op(e3,e0)& op(e0,e4) = op(e4,e0)& op(e0,e5) = op(e5,e0)& op(e1,e0) = op(e0,e1)& op(e1,e1) = op(e1,e1)& op(e1,e2) = op(e2,e1)& op(e1,e3) = op(e3,e1)& op(e1,e4) = op(e4,e1)& op(e1,e5) = op(e5,e1)& op(e2,e0) = op(e0,e2)& op(e2,e1) = op(e1,e2)& op(e2,e2) = op(e2,e2)& op(e2,e3) = op(e3,e2)& op(e2,e4) = op(e4,e2)& op(e2,e5) = op(e5,e2)& op(e3,e0) = op(e0,e3)& op(e3,e1) = op(e1,e3)& op(e3,e2) = op(e2,e3)& op(e3,e3) = op(e3,e3)& op(e3,e4) = op(e4,e3)& op(e3,e5) = op(e5,e3)& op(e4,e0) = op(e0,e4)& op(e4,e1) = op(e1,e4)& op(e4,e2) = op(e2,e4)& op(e4,e3) = op(e3,e4)& op(e4,e4) = op(e4,e4)& op(e4,e5) = op(e5,e4)& op(e5,e0) = op(e0,e5)& op(e5,e1) = op(e1,e5)& op(e5,e2) = op(e2,e5)& op(e5,e3) = op(e3,e5)& op(e5,e4) = op(e4,e5)& op(e5,e5) = op(e5,e5) )| ~ ( op(e0,e0) = op(e0,e0)& op(e0,e1) = op(e1,e0)& op(e0,e2) = op(e2,e0)& op(e0,e3) = op(e3,e0)& op(e0,e4) = op(e4,e0)& op(e0,e5) = op(e5,e0)& op(e1,e0) = op(e0,e1)& op(e1,e1) = op(e1,e1)& op(e1,e2) = op(e2,e1)& op(e1,e3) = op(e3,e1)& op(e1,e4) = op(e4,e1)& op(e1,e5) = op(e5,e1)& op(e2,e0) = op(e0,e2)& op(e2,e1) = op(e1,e2)& op(e2,e2) = op(e2,e2)& op(e2,e3) = op(e3,e2)& op(e2,e4) = op(e4,e2)& op(e2,e5) = op(e5,e2)& op(e3,e0) = op(e0,e3)& op(e3,e1) = op(e1,e3)& op(e3,e2) = op(e2,e3)& op(e3,e3) = op(e3,e3)& op(e3,e4) = op(e4,e3)& op(e3,e5) = op(e5,e3)& op(e4,e0) = op(e0,e4)& op(e4,e1) = op(e1,e4)& op(e4,e2) = op(e2,e4)& op(e4,e3) = op(e3,e4)& op(e4,e4) = op(e4,e4)& op(e4,e5) = op(e5,e4)& op(e5,e0) = op(e0,e5)& op(e5,e1) = op(e1,e5)& op(e5,e2) = op(e2,e5)& op(e5,e3) = op(e3,e5)& op(e5,e4) = op(e4,e5)& op(e5,e5) = op(e5,e5) ) ) )),
% 0.15/5.42 inference(negated_conjecture,[status(cth)],[f12])).
% 0.15/5.42 fof(f552,plain,(
% 0.15/5.42 ((((((((((((((((((((((((((((((((((((~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e1,e0))|~op(e0,e2)=op(e2,e0))|~op(e0,e3)=op(e3,e0))|~op(e0,e4)=op(e4,e0))|~op(e0,e5)=op(e5,e0))|~op(e1,e0)=op(e0,e1))|~op(e1,e1)=op(e1,e1))|~op(e1,e2)=op(e2,e1))|~op(e1,e3)=op(e3,e1))|~op(e1,e4)=op(e4,e1))|~op(e1,e5)=op(e5,e1))|~op(e2,e0)=op(e0,e2))|~op(e2,e1)=op(e1,e2))|~op(e2,e2)=op(e2,e2))|~op(e2,e3)=op(e3,e2))|~op(e2,e4)=op(e4,e2))|~op(e2,e5)=op(e5,e2))|~op(e3,e0)=op(e0,e3))|~op(e3,e1)=op(e1,e3))|~op(e3,e2)=op(e2,e3))|~op(e3,e3)=op(e3,e3))|~op(e3,e4)=op(e4,e3))|~op(e3,e5)=op(e5,e3))|~op(e4,e0)=op(e0,e4))|~op(e4,e1)=op(e1,e4))|~op(e4,e2)=op(e2,e4))|~op(e4,e3)=op(e3,e4))|~op(e4,e4)=op(e4,e4))|~op(e4,e5)=op(e5,e4))|~op(e5,e0)=op(e0,e5))|~op(e5,e1)=op(e1,e5))|~op(e5,e2)=op(e2,e5))|~op(e5,e3)=op(e3,e5))|~op(e5,e4)=op(e4,e5))|~op(e5,e5)=op(e5,e5))&(((((((((((((((((((((((((((((((((((op(e0,e0)=op(e0,e0)&op(e0,e1)=op(e1,e0))&op(e0,e2)=op(e2,e0))&op(e0,e3)=op(e3,e0))&op(e0,e4)=op(e4,e0))&op(e0,e5)=op(e5,e0))&op(e1,e0)=op(e0,e1))&op(e1,e1)=op(e1,e1))&op(e1,e2)=op(e2,e1))&op(e1,e3)=op(e3,e1))&op(e1,e4)=op(e4,e1))&op(e1,e5)=op(e5,e1))&op(e2,e0)=op(e0,e2))&op(e2,e1)=op(e1,e2))&op(e2,e2)=op(e2,e2))&op(e2,e3)=op(e3,e2))&op(e2,e4)=op(e4,e2))&op(e2,e5)=op(e5,e2))&op(e3,e0)=op(e0,e3))&op(e3,e1)=op(e1,e3))&op(e3,e2)=op(e2,e3))&op(e3,e3)=op(e3,e3))&op(e3,e4)=op(e4,e3))&op(e3,e5)=op(e5,e3))&op(e4,e0)=op(e0,e4))&op(e4,e1)=op(e1,e4))&op(e4,e2)=op(e2,e4))&op(e4,e3)=op(e3,e4))&op(e4,e4)=op(e4,e4))&op(e4,e5)=op(e5,e4))&op(e5,e0)=op(e0,e5))&op(e5,e1)=op(e1,e5))&op(e5,e2)=op(e2,e5))&op(e5,e3)=op(e3,e5))&op(e5,e4)=op(e4,e5))&op(e5,e5)=op(e5,e5)))),
% 0.15/5.42 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.15/5.42 fof(f553,plain,(
% 0.15/5.42 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e1,e0)|~op(e0,e2)=op(e2,e0)|~op(e0,e3)=op(e3,e0)|~op(e0,e4)=op(e4,e0)|~op(e0,e5)=op(e5,e0)|~op(e1,e0)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e2,e1)|~op(e1,e3)=op(e3,e1)|~op(e1,e4)=op(e4,e1)|~op(e1,e5)=op(e5,e1)|~op(e2,e0)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f555,plain,(
% 0.15/5.42 op(e0,e1)=op(e1,e0)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f556,plain,(
% 0.15/5.42 op(e0,e2)=op(e2,e0)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f557,plain,(
% 0.15/5.42 op(e0,e3)=op(e3,e0)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f558,plain,(
% 0.15/5.42 op(e0,e4)=op(e4,e0)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f559,plain,(
% 0.15/5.42 op(e0,e5)=op(e5,e0)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f562,plain,(
% 0.15/5.42 op(e1,e2)=op(e2,e1)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f563,plain,(
% 0.15/5.42 op(e1,e3)=op(e3,e1)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f564,plain,(
% 0.15/5.42 op(e1,e4)=op(e4,e1)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f565,plain,(
% 0.15/5.42 op(e1,e5)=op(e5,e1)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f569,plain,(
% 0.15/5.42 op(e2,e3)=op(e3,e2)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f570,plain,(
% 0.15/5.42 op(e2,e4)=op(e4,e2)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f571,plain,(
% 0.15/5.42 op(e2,e5)=op(e5,e2)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f576,plain,(
% 0.15/5.42 op(e3,e4)=op(e4,e3)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f577,plain,(
% 0.15/5.42 op(e3,e5)=op(e5,e3)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f583,plain,(
% 0.15/5.42 op(e4,e5)=op(e5,e4)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f552])).
% 0.15/5.42 fof(f1443,definition,(
% 0.15/5.42 sQ258_spl <=> (op(e0,e0)=op(e0,e0))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1445,plain,(
% 0.15/5.42 ~op(e0,e0)=op(e0,e0)|sQ258_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1443])).
% 0.15/5.42 fof(f1446,definition,(
% 0.15/5.42 sQ259_spl <=> (op(e0,e1)=op(e1,e0))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1448,plain,(
% 0.15/5.42 ~op(e0,e1)=op(e1,e0)|sQ259_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1446])).
% 0.15/5.42 fof(f1449,definition,(
% 0.15/5.42 sQ260_spl <=> (op(e0,e2)=op(e2,e0))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1451,plain,(
% 0.15/5.42 ~op(e0,e2)=op(e2,e0)|sQ260_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1449])).
% 0.15/5.42 fof(f1452,definition,(
% 0.15/5.42 sQ261_spl <=> (op(e0,e3)=op(e3,e0))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1454,plain,(
% 0.15/5.42 ~op(e0,e3)=op(e3,e0)|sQ261_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1452])).
% 0.15/5.42 fof(f1455,definition,(
% 0.15/5.42 sQ262_spl <=> (op(e0,e4)=op(e4,e0))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1457,plain,(
% 0.15/5.42 ~op(e0,e4)=op(e4,e0)|sQ262_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1455])).
% 0.15/5.42 fof(f1458,definition,(
% 0.15/5.42 sQ263_spl <=> (op(e0,e5)=op(e5,e0))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1460,plain,(
% 0.15/5.42 ~op(e0,e5)=op(e5,e0)|sQ263_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1458])).
% 0.15/5.42 fof(f1461,definition,(
% 0.15/5.42 sQ264_spl <=> (op(e1,e1)=op(e1,e1))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1463,plain,(
% 0.15/5.42 ~op(e1,e1)=op(e1,e1)|sQ264_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1461])).
% 0.15/5.42 fof(f1464,definition,(
% 0.15/5.42 sQ265_spl <=> (op(e1,e2)=op(e2,e1))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1466,plain,(
% 0.15/5.42 ~op(e1,e2)=op(e2,e1)|sQ265_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1464])).
% 0.15/5.42 fof(f1467,definition,(
% 0.15/5.42 sQ266_spl <=> (op(e1,e3)=op(e3,e1))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1469,plain,(
% 0.15/5.42 ~op(e1,e3)=op(e3,e1)|sQ266_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1467])).
% 0.15/5.42 fof(f1470,definition,(
% 0.15/5.42 sQ267_spl <=> (op(e1,e4)=op(e4,e1))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1472,plain,(
% 0.15/5.42 ~op(e1,e4)=op(e4,e1)|sQ267_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1470])).
% 0.15/5.42 fof(f1473,definition,(
% 0.15/5.42 sQ268_spl <=> (op(e1,e5)=op(e5,e1))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1475,plain,(
% 0.15/5.42 ~op(e1,e5)=op(e5,e1)|sQ268_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1473])).
% 0.15/5.42 fof(f1476,definition,(
% 0.15/5.42 sQ269_spl <=> (op(e2,e2)=op(e2,e2))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1478,plain,(
% 0.15/5.42 ~op(e2,e2)=op(e2,e2)|sQ269_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1476])).
% 0.15/5.42 fof(f1479,definition,(
% 0.15/5.42 sQ270_spl <=> (op(e2,e3)=op(e3,e2))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1481,plain,(
% 0.15/5.42 ~op(e2,e3)=op(e3,e2)|sQ270_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1479])).
% 0.15/5.42 fof(f1482,definition,(
% 0.15/5.42 sQ271_spl <=> (op(e2,e4)=op(e4,e2))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1484,plain,(
% 0.15/5.42 ~op(e2,e4)=op(e4,e2)|sQ271_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1482])).
% 0.15/5.42 fof(f1485,definition,(
% 0.15/5.42 sQ272_spl <=> (op(e2,e5)=op(e5,e2))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1487,plain,(
% 0.15/5.42 ~op(e2,e5)=op(e5,e2)|sQ272_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1485])).
% 0.15/5.42 fof(f1488,definition,(
% 0.15/5.42 sQ273_spl <=> (op(e3,e3)=op(e3,e3))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1490,plain,(
% 0.15/5.42 ~op(e3,e3)=op(e3,e3)|sQ273_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1488])).
% 0.15/5.42 fof(f1491,definition,(
% 0.15/5.42 sQ274_spl <=> (op(e3,e4)=op(e4,e3))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1493,plain,(
% 0.15/5.42 ~op(e3,e4)=op(e4,e3)|sQ274_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1491])).
% 0.15/5.42 fof(f1494,definition,(
% 0.15/5.42 sQ275_spl <=> (op(e3,e5)=op(e5,e3))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ275_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1496,plain,(
% 0.15/5.42 ~op(e3,e5)=op(e5,e3)|sQ275_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1494])).
% 0.15/5.42 fof(f1497,definition,(
% 0.15/5.42 sQ276_spl <=> (op(e4,e4)=op(e4,e4))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ276_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1499,plain,(
% 0.15/5.42 ~op(e4,e4)=op(e4,e4)|sQ276_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1497])).
% 0.15/5.42 fof(f1500,definition,(
% 0.15/5.42 sQ277_spl <=> (op(e4,e5)=op(e5,e4))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1502,plain,(
% 0.15/5.42 ~op(e4,e5)=op(e5,e4)|sQ277_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1500])).
% 0.15/5.42 fof(f1503,definition,(
% 0.15/5.42 sQ278_spl <=> (op(e5,e5)=op(e5,e5))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f1505,plain,(
% 0.15/5.42 ~op(e5,e5)=op(e5,e5)|sQ278_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f1503])).
% 0.15/5.42 fof(f1506,plain,(
% 0.15/5.42 ~sQ258_spl|~sQ259_spl|~sQ260_spl|~sQ261_spl|~sQ262_spl|~sQ263_spl|~sQ264_spl|~sQ265_spl|~sQ266_spl|~sQ267_spl|~sQ268_spl|~sQ269_spl|~sQ270_spl|~sQ271_spl|~sQ272_spl|~sQ273_spl|~sQ274_spl|~sQ275_spl|~sQ276_spl|~sQ277_spl|~sQ278_spl),
% 0.15/5.42 inference(split_clause,[status(thm)],[f553,f1443,f1446,f1449,f1452,f1455,f1458,f1461,f1464,f1467,f1470,f1473,f1476,f1479,f1482,f1485,f1488,f1491,f1494,f1497,f1500,f1503])).
% 0.15/5.42 fof(f1507,plain,(
% 0.15/5.42 $false|sQ278_spl),
% 0.15/5.42 inference(trivial_equality_resolution,[status(thm)],[f1505])).
% 0.15/5.42 fof(f1508,plain,(
% 0.15/5.42 sQ278_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f1507])).
% 0.15/5.42 fof(f1509,plain,(
% 0.15/5.42 $false|sQ276_spl),
% 0.15/5.42 inference(trivial_equality_resolution,[status(thm)],[f1499])).
% 0.15/5.42 fof(f1510,plain,(
% 0.15/5.42 sQ276_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f1509])).
% 0.15/5.42 fof(f1511,plain,(
% 0.15/5.42 $false|sQ273_spl),
% 0.15/5.42 inference(trivial_equality_resolution,[status(thm)],[f1490])).
% 0.15/5.42 fof(f1512,plain,(
% 0.15/5.42 sQ273_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f1511])).
% 0.15/5.42 fof(f1513,plain,(
% 0.15/5.42 $false|sQ269_spl),
% 0.15/5.42 inference(trivial_equality_resolution,[status(thm)],[f1478])).
% 0.15/5.42 fof(f1514,plain,(
% 0.15/5.42 sQ269_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f1513])).
% 0.15/5.42 fof(f1515,plain,(
% 0.15/5.42 $false|sQ264_spl),
% 0.15/5.42 inference(trivial_equality_resolution,[status(thm)],[f1463])).
% 0.15/5.42 fof(f1516,plain,(
% 0.15/5.42 sQ264_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f1515])).
% 0.15/5.42 fof(f1517,plain,(
% 0.15/5.42 $false|sQ258_spl),
% 0.15/5.42 inference(trivial_equality_resolution,[status(thm)],[f1445])).
% 0.15/5.42 fof(f1518,plain,(
% 0.15/5.42 sQ258_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f1517])).
% 0.15/5.42 fof(f1520,plain,(
% 0.15/5.42 ~op(e4,e5)=op(e4,e5)|sQ277_spl),
% 0.15/5.42 inference(forward_demodulation,[status(thm)],[f583,f1502])).
% 0.15/5.42 fof(f1521,plain,(
% 0.15/5.42 $false|sQ277_spl),
% 0.15/5.42 inference(trivial_equality_resolution,[status(thm)],[f1520])).
% 0.15/5.42 fof(f1522,plain,(
% 0.15/5.42 sQ277_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f1521])).
% 0.15/5.42 fof(f1523,plain,(
% 0.15/5.42 ~op(e3,e5)=op(e3,e5)|sQ275_spl),
% 0.15/5.42 inference(forward_demodulation,[status(thm)],[f577,f1496])).
% 0.15/5.42 fof(f1524,plain,(
% 0.15/5.42 $false|sQ275_spl),
% 0.15/5.42 inference(trivial_equality_resolution,[status(thm)],[f1523])).
% 0.15/5.42 fof(f1525,plain,(
% 0.15/5.42 sQ275_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f1524])).
% 0.15/5.42 fof(f1526,plain,(
% 0.15/5.42 ~op(e3,e4)=op(e3,e4)|sQ274_spl),
% 0.15/5.42 inference(forward_demodulation,[status(thm)],[f576,f1493])).
% 0.15/5.42 fof(f1527,plain,(
% 0.15/5.42 $false|sQ274_spl),
% 0.15/5.42 inference(trivial_equality_resolution,[status(thm)],[f1526])).
% 0.15/5.42 fof(f1528,plain,(
% 0.15/5.42 sQ274_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f1527])).
% 0.15/5.42 fof(f1529,plain,(
% 0.15/5.42 ~op(e2,e5)=op(e2,e5)|sQ272_spl),
% 0.15/5.42 inference(forward_demodulation,[status(thm)],[f571,f1487])).
% 0.15/5.42 fof(f1530,plain,(
% 0.15/5.42 $false|sQ272_spl),
% 0.15/5.42 inference(trivial_equality_resolution,[status(thm)],[f1529])).
% 0.15/5.42 fof(f1531,plain,(
% 0.15/5.42 sQ272_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f1530])).
% 0.15/5.42 fof(f1532,plain,(
% 0.15/5.42 ~op(e2,e4)=op(e2,e4)|sQ271_spl),
% 0.15/5.42 inference(forward_demodulation,[status(thm)],[f570,f1484])).
% 0.15/5.42 fof(f1533,plain,(
% 0.15/5.42 $false|sQ271_spl),
% 0.15/5.42 inference(trivial_equality_resolution,[status(thm)],[f1532])).
% 0.15/5.42 fof(f1534,plain,(
% 0.15/5.42 sQ271_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f1533])).
% 0.15/5.42 fof(f1535,plain,(
% 0.15/5.42 ~op(e2,e3)=op(e2,e3)|sQ270_spl),
% 0.15/5.42 inference(forward_demodulation,[status(thm)],[f569,f1481])).
% 0.15/5.42 fof(f1536,plain,(
% 0.15/5.42 $false|sQ270_spl),
% 0.15/5.43 inference(trivial_equality_resolution,[status(thm)],[f1535])).
% 0.15/5.43 fof(f1537,plain,(
% 0.15/5.43 sQ270_spl),
% 0.15/5.43 inference(contradiction_clause,[status(thm)],[f1536])).
% 0.15/5.43 fof(f1538,plain,(
% 0.15/5.43 ~op(e1,e5)=op(e1,e5)|sQ268_spl),
% 0.15/5.43 inference(forward_demodulation,[status(thm)],[f565,f1475])).
% 0.15/5.43 fof(f1539,plain,(
% 0.15/5.43 $false|sQ268_spl),
% 0.15/5.43 inference(trivial_equality_resolution,[status(thm)],[f1538])).
% 0.15/5.43 fof(f1540,plain,(
% 0.15/5.43 sQ268_spl),
% 0.15/5.43 inference(contradiction_clause,[status(thm)],[f1539])).
% 0.15/5.43 fof(f1541,plain,(
% 0.15/5.43 ~op(e1,e4)=op(e1,e4)|sQ267_spl),
% 0.15/5.43 inference(forward_demodulation,[status(thm)],[f564,f1472])).
% 0.15/5.43 fof(f1542,plain,(
% 0.15/5.43 $false|sQ267_spl),
% 0.15/5.43 inference(trivial_equality_resolution,[status(thm)],[f1541])).
% 0.15/5.43 fof(f1543,plain,(
% 0.15/5.43 sQ267_spl),
% 0.15/5.43 inference(contradiction_clause,[status(thm)],[f1542])).
% 0.15/5.43 fof(f1544,plain,(
% 0.15/5.43 ~op(e1,e3)=op(e1,e3)|sQ266_spl),
% 0.15/5.43 inference(forward_demodulation,[status(thm)],[f563,f1469])).
% 0.15/5.43 fof(f1545,plain,(
% 0.15/5.43 $false|sQ266_spl),
% 0.15/5.43 inference(trivial_equality_resolution,[status(thm)],[f1544])).
% 0.15/5.43 fof(f1546,plain,(
% 0.15/5.43 sQ266_spl),
% 0.15/5.43 inference(contradiction_clause,[status(thm)],[f1545])).
% 0.15/5.43 fof(f1547,plain,(
% 0.15/5.43 ~op(e1,e2)=op(e1,e2)|sQ265_spl),
% 0.15/5.43 inference(forward_demodulation,[status(thm)],[f562,f1466])).
% 0.15/5.43 fof(f1548,plain,(
% 0.15/5.43 $false|sQ265_spl),
% 0.15/5.43 inference(trivial_equality_resolution,[status(thm)],[f1547])).
% 0.15/5.43 fof(f1549,plain,(
% 0.15/5.43 sQ265_spl),
% 0.15/5.43 inference(contradiction_clause,[status(thm)],[f1548])).
% 0.15/5.43 fof(f1550,plain,(
% 0.15/5.43 ~op(e0,e5)=op(e0,e5)|sQ263_spl),
% 0.15/5.43 inference(forward_demodulation,[status(thm)],[f559,f1460])).
% 0.15/5.43 fof(f1551,plain,(
% 0.15/5.43 $false|sQ263_spl),
% 0.15/5.43 inference(trivial_equality_resolution,[status(thm)],[f1550])).
% 0.15/5.43 fof(f1552,plain,(
% 0.15/5.43 sQ263_spl),
% 0.15/5.43 inference(contradiction_clause,[status(thm)],[f1551])).
% 0.15/5.43 fof(f1553,plain,(
% 0.15/5.43 ~op(e0,e4)=op(e0,e4)|sQ262_spl),
% 0.15/5.43 inference(forward_demodulation,[status(thm)],[f558,f1457])).
% 0.15/5.43 fof(f1554,plain,(
% 0.15/5.43 $false|sQ262_spl),
% 0.15/5.43 inference(trivial_equality_resolution,[status(thm)],[f1553])).
% 0.15/5.43 fof(f1555,plain,(
% 0.15/5.43 sQ262_spl),
% 0.15/5.43 inference(contradiction_clause,[status(thm)],[f1554])).
% 0.15/5.43 fof(f1556,plain,(
% 0.15/5.43 ~op(e0,e3)=op(e0,e3)|sQ261_spl),
% 0.15/5.43 inference(forward_demodulation,[status(thm)],[f557,f1454])).
% 0.15/5.43 fof(f1557,plain,(
% 0.15/5.43 $false|sQ261_spl),
% 0.15/5.43 inference(trivial_equality_resolution,[status(thm)],[f1556])).
% 0.15/5.43 fof(f1558,plain,(
% 0.15/5.43 sQ261_spl),
% 0.15/5.43 inference(contradiction_clause,[status(thm)],[f1557])).
% 0.15/5.43 fof(f1559,plain,(
% 0.15/5.43 ~op(e0,e2)=op(e0,e2)|sQ260_spl),
% 0.15/5.43 inference(forward_demodulation,[status(thm)],[f556,f1451])).
% 0.15/5.43 fof(f1560,plain,(
% 0.15/5.43 $false|sQ260_spl),
% 0.15/5.43 inference(trivial_equality_resolution,[status(thm)],[f1559])).
% 0.15/5.43 fof(f1561,plain,(
% 0.15/5.43 sQ260_spl),
% 0.15/5.43 inference(contradiction_clause,[status(thm)],[f1560])).
% 0.15/5.43 fof(f1562,plain,(
% 0.15/5.43 ~op(e0,e1)=op(e0,e1)|sQ259_spl),
% 0.15/5.43 inference(forward_demodulation,[status(thm)],[f555,f1448])).
% 0.15/5.43 fof(f1563,plain,(
% 0.15/5.43 $false|sQ259_spl),
% 0.15/5.43 inference(trivial_equality_resolution,[status(thm)],[f1562])).
% 0.15/5.43 fof(f1564,plain,(
% 0.15/5.43 sQ259_spl),
% 0.15/5.43 inference(contradiction_clause,[status(thm)],[f1563])).
% 0.15/5.43 fof(f1565,plain,(
% 0.15/5.43 $false),
% 0.15/5.43 inference(sat_refutation,[status(thm)],[f1506,f1508,f1510,f1512,f1514,f1516,f1518,f1522,f1525,f1528,f1531,f1534,f1537,f1540,f1543,f1546,f1549,f1552,f1555,f1558,f1561,f1564])).
% 0.15/5.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/5.48 % Elapsed time: 0.092770 seconds
% 0.15/5.48 % CPU time: 0.174210 seconds
% 0.15/5.48 % Total memory used: 58.059 MB
% 0.15/5.48 % Net memory used: 58.027 MB
%------------------------------------------------------------------------------