%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG194+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 : n017.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:47 AM UTC 2026
% Result : Theorem 0.13s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG194+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 : n017.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:56:28 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 0.13/0.41 % Refutation found
% 0.13/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.41 fof(f6,conjecture,(
% 0.13/0.41 ( ( op(e0,e0) != e0& op(e1,e1) != e1& op(e2,e2) != e2& op(e3,e3) != e3& op(e4,e4) != e4& op(e5,e5) != e5& op(e6,e6) != e6 )| ( op(e0,e0) = e0& op(e1,e1) = e1& op(e2,e2) = e2& op(e3,e3) = e3& op(e4,e4) = e4& op(e5,e5) = e5& op(e6,e6) = e6 )| ( ( op(e0,e0) = e0| op(e1,e1) = e1| op(e2,e2) = e2| op(e3,e3) = e3| op(e4,e4) = e4| op(e5,e5) = e5| op(e6,e6) = e6 )& ( op(e0,e0) != e0| op(e1,e1) != e1| op(e2,e2) != e2| op(e3,e3) != e3| op(e4,e4) != e4| op(e5,e5) != e5| op(e6,e6) != e6 ) ) ) ),
% 0.13/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f7,negated_conjecture,(
% 0.13/0.41 ~(( ( op(e0,e0) != e0& op(e1,e1) != e1& op(e2,e2) != e2& op(e3,e3) != e3& op(e4,e4) != e4& op(e5,e5) != e5& op(e6,e6) != e6 )| ( op(e0,e0) = e0& op(e1,e1) = e1& op(e2,e2) = e2& op(e3,e3) = e3& op(e4,e4) = e4& op(e5,e5) = e5& op(e6,e6) = e6 )| ( ( op(e0,e0) = e0| op(e1,e1) = e1| op(e2,e2) = e2| op(e3,e3) = e3| op(e4,e4) = e4| op(e5,e5) = e5| op(e6,e6) = e6 )& ( op(e0,e0) != e0| op(e1,e1) != e1| op(e2,e2) != e2| op(e3,e3) != e3| op(e4,e4) != e4| op(e5,e5) != e5| op(e6,e6) != e6 ) ) ) )),
% 0.13/0.41 inference(negated_conjecture,[status(cth)],[f6])).
% 0.13/0.41 fof(f519,plain,(
% 0.13/0.41 ((((((((op(e0,e0)=e0|op(e1,e1)=e1)|op(e2,e2)=e2)|op(e3,e3)=e3)|op(e4,e4)=e4)|op(e5,e5)=e5)|op(e6,e6)=e6)&((((((~op(e0,e0)=e0|~op(e1,e1)=e1)|~op(e2,e2)=e2)|~op(e3,e3)=e3)|~op(e4,e4)=e4)|~op(e5,e5)=e5)|~op(e6,e6)=e6))&(((((((~op(e0,e0)=e0&~op(e1,e1)=e1)&~op(e2,e2)=e2)&~op(e3,e3)=e3)&~op(e4,e4)=e4)&~op(e5,e5)=e5)&~op(e6,e6)=e6)|((((((op(e0,e0)=e0&op(e1,e1)=e1)&op(e2,e2)=e2)&op(e3,e3)=e3)&op(e4,e4)=e4)&op(e5,e5)=e5)&op(e6,e6)=e6)))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.13/0.41 fof(f520,definition,(
% 0.13/0.41 sP0_prd<=>((((((~op(e0,e0)=e0&~op(e1,e1)=e1)&~op(e2,e2)=e2)&~op(e3,e3)=e3)&~op(e4,e4)=e4)&~op(e5,e5)=e5)&~op(e6,e6)=e6)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.13/0.41 fof(f521,plain,(
% 0.13/0.41 (((((((op(e0,e0)=e0|op(e1,e1)=e1)|op(e2,e2)=e2)|op(e3,e3)=e3)|op(e4,e4)=e4)|op(e5,e5)=e5)|op(e6,e6)=e6)&((((((~op(e0,e0)=e0|~op(e1,e1)=e1)|~op(e2,e2)=e2)|~op(e3,e3)=e3)|~op(e4,e4)=e4)|~op(e5,e5)=e5)|~op(e6,e6)=e6))&(sP0_prd|((((((op(e0,e0)=e0&op(e1,e1)=e1)&op(e2,e2)=e2)&op(e3,e3)=e3)&op(e4,e4)=e4)&op(e5,e5)=e5)&op(e6,e6)=e6))),
% 0.13/0.41 inference(formula_renaming,[status(thm)],[f519,f520])).
% 0.13/0.41 fof(f522,plain,(
% 0.13/0.41 op(e0,e0)=e0|op(e1,e1)=e1|op(e2,e2)=e2|op(e3,e3)=e3|op(e4,e4)=e4|op(e5,e5)=e5|op(e6,e6)=e6),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f521])).
% 0.13/0.41 fof(f523,plain,(
% 0.13/0.41 ~op(e0,e0)=e0|~op(e1,e1)=e1|~op(e2,e2)=e2|~op(e3,e3)=e3|~op(e4,e4)=e4|~op(e5,e5)=e5|~op(e6,e6)=e6),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f521])).
% 0.13/0.41 fof(f524,plain,(
% 0.13/0.41 sP0_prd|op(e0,e0)=e0),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f521])).
% 0.13/0.41 fof(f525,plain,(
% 0.13/0.41 sP0_prd|op(e1,e1)=e1),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f521])).
% 0.13/0.41 fof(f526,plain,(
% 0.13/0.41 sP0_prd|op(e2,e2)=e2),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f521])).
% 0.13/0.41 fof(f527,plain,(
% 0.13/0.41 sP0_prd|op(e3,e3)=e3),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f521])).
% 0.13/0.41 fof(f528,plain,(
% 0.13/0.41 sP0_prd|op(e4,e4)=e4),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f521])).
% 0.13/0.41 fof(f529,plain,(
% 0.13/0.41 sP0_prd|op(e5,e5)=e5),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f521])).
% 0.13/0.41 fof(f530,plain,(
% 0.13/0.41 sP0_prd|op(e6,e6)=e6),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f521])).
% 0.13/0.41 fof(f531,plain,(
% 0.13/0.41 (~sP0_prd|((((((~op(e0,e0)=e0&~op(e1,e1)=e1)&~op(e2,e2)=e2)&~op(e3,e3)=e3)&~op(e4,e4)=e4)&~op(e5,e5)=e5)&~op(e6,e6)=e6))&(sP0_prd|((((((op(e0,e0)=e0|op(e1,e1)=e1)|op(e2,e2)=e2)|op(e3,e3)=e3)|op(e4,e4)=e4)|op(e5,e5)=e5)|op(e6,e6)=e6))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f520])).
% 0.13/0.41 fof(f532,plain,(
% 0.13/0.41 ~sP0_prd|~op(e0,e0)=e0),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f531])).
% 0.13/0.41 fof(f533,plain,(
% 0.13/0.41 ~sP0_prd|~op(e1,e1)=e1),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f531])).
% 0.13/0.41 fof(f534,plain,(
% 0.13/0.41 ~sP0_prd|~op(e2,e2)=e2),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f531])).
% 0.13/0.41 fof(f535,plain,(
% 0.13/0.41 ~sP0_prd|~op(e3,e3)=e3),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f531])).
% 0.13/0.41 fof(f536,plain,(
% 0.13/0.41 ~sP0_prd|~op(e4,e4)=e4),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f531])).
% 0.13/0.41 fof(f537,plain,(
% 0.13/0.41 ~sP0_prd|~op(e5,e5)=e5),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f531])).
% 0.13/0.41 fof(f538,plain,(
% 0.13/0.41 ~sP0_prd|~op(e6,e6)=e6),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f531])).
% 0.13/0.41 fof(f540,definition,(
% 0.13/0.41 sQ0_spl <=> (op(e0,e0)=e0)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f719,definition,(
% 0.13/0.41 sQ57_spl <=> (op(e1,e1)=e1)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f898,definition,(
% 0.13/0.41 sQ114_spl <=> (op(e2,e2)=e2)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1077,definition,(
% 0.13/0.41 sQ171_spl <=> (op(e3,e3)=e3)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1256,definition,(
% 0.13/0.41 sQ228_spl <=> (op(e4,e4)=e4)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1435,definition,(
% 0.13/0.41 sQ285_spl <=> (op(e5,e5)=e5)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1614,definition,(
% 0.13/0.41 sQ342_spl <=> (op(e6,e6)=e6)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1716,plain,(
% 0.13/0.41 sQ0_spl|sQ57_spl|sQ114_spl|sQ171_spl|sQ228_spl|sQ285_spl|sQ342_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f522,f540,f719,f898,f1077,f1256,f1435,f1614])).
% 0.13/0.41 fof(f1717,plain,(
% 0.13/0.41 ~sQ0_spl|~sQ57_spl|~sQ114_spl|~sQ171_spl|~sQ228_spl|~sQ285_spl|~sQ342_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f523,f540,f719,f898,f1077,f1256,f1435,f1614])).
% 0.13/0.41 fof(f1718,definition,(
% 0.13/0.41 sQ343_spl <=> (sP0_prd)),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ343_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1721,plain,(
% 0.13/0.41 sQ343_spl|sQ0_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f524,f1718,f540])).
% 0.13/0.41 fof(f1722,plain,(
% 0.13/0.41 sQ343_spl|sQ57_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f525,f1718,f719])).
% 0.13/0.41 fof(f1723,plain,(
% 0.13/0.41 sQ343_spl|sQ114_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f526,f1718,f898])).
% 0.13/0.41 fof(f1724,plain,(
% 0.13/0.41 sQ343_spl|sQ171_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f527,f1718,f1077])).
% 0.13/0.41 fof(f1725,plain,(
% 0.13/0.41 sQ343_spl|sQ228_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f528,f1718,f1256])).
% 0.13/0.41 fof(f1726,plain,(
% 0.13/0.41 sQ343_spl|sQ285_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f529,f1718,f1435])).
% 0.13/0.41 fof(f1727,plain,(
% 0.13/0.41 sQ343_spl|sQ342_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f530,f1718,f1614])).
% 0.13/0.41 fof(f1728,plain,(
% 0.13/0.41 ~sQ343_spl|~sQ0_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f532,f1718,f540])).
% 0.13/0.41 fof(f1729,plain,(
% 0.13/0.41 ~sQ343_spl|~sQ57_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f533,f1718,f719])).
% 0.13/0.41 fof(f1730,plain,(
% 0.13/0.41 ~sQ343_spl|~sQ114_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f534,f1718,f898])).
% 0.13/0.41 fof(f1731,plain,(
% 0.13/0.41 ~sQ343_spl|~sQ171_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f535,f1718,f1077])).
% 0.13/0.41 fof(f1732,plain,(
% 0.13/0.41 ~sQ343_spl|~sQ228_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f536,f1718,f1256])).
% 0.13/0.41 fof(f1733,plain,(
% 0.13/0.41 ~sQ343_spl|~sQ285_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f537,f1718,f1435])).
% 0.13/0.41 fof(f1734,plain,(
% 0.13/0.41 ~sQ343_spl|~sQ342_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f538,f1718,f1614])).
% 0.13/0.41 fof(f1736,plain,(
% 0.13/0.41 $false),
% 0.13/0.41 inference(sat_refutation,[status(thm)],[f1716,f1717,f1721,f1722,f1723,f1724,f1725,f1726,f1727,f1728,f1729,f1730,f1731,f1732,f1733,f1734])).
% 0.13/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.46 % Elapsed time: 0.086067 seconds
% 0.13/0.46 % CPU time: 0.234946 seconds
% 0.13/0.46 % Total memory used: 98.452 MB
% 0.13/0.46 % Net memory used: 98.397 MB
%------------------------------------------------------------------------------