%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : FLD013-2 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 12:22:18 PM UTC 2026
% Result : Unsatisfiable 5.61s 1.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : FLD013-2 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 15:35:20 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 5.61/1.21 % Refutation found
% 5.61/1.21 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 5.61/1.21 % SZS output start CNFRefutation for theBenchmark
% 5.61/1.21 fof(f4,axiom,(
% 5.61/1.21 (![X,Y]: (( equalish(add(X,Y),add(Y,X))| ~ defined(X)| ~ defined(Y) ) ))),
% 5.61/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.61/1.21 fof(f22,axiom,(
% 5.61/1.21 (![X,Y]: (( equalish(X,Y)| ~ equalish(Y,X) ) ))),
% 5.61/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.61/1.21 fof(f23,axiom,(
% 5.61/1.21 (![X,Z,Y]: (( equalish(X,Z)| ~ equalish(X,Y)| ~ equalish(Y,Z) ) ))),
% 5.61/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.61/1.21 fof(f24,axiom,(
% 5.61/1.21 (![X,Z,Y]: (( equalish(add(X,Z),add(Y,Z))| ~ defined(Z)| ~ equalish(X,Y) ) ))),
% 5.61/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.61/1.21 fof(f29,hypothesis,(
% 5.61/1.21 defined(b) ),
% 5.61/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.61/1.21 fof(f30,hypothesis,(
% 5.61/1.21 defined(c) ),
% 5.61/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.61/1.21 fof(f33,negated_conjecture,(
% 5.61/1.21 equalish(a,b) ),
% 5.61/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.61/1.21 fof(f34,negated_conjecture,(
% 5.61/1.21 equalish(c,d) ),
% 5.61/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.61/1.21 fof(f35,negated_conjecture,(
% 5.61/1.21 equalish(add(a,c),u) ),
% 5.61/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.61/1.21 fof(f36,negated_conjecture,(
% 5.61/1.21 ~ equalish(add(d,b),u) ),
% 5.61/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.61/1.21 fof(f41,plain,(
% 5.61/1.21 ![Y]: ((![X]: (equalish(add(X,Y),add(Y,X))|~defined(X)))|~defined(Y))),
% 5.61/1.21 inference(miniscoping,[status(thm)],[f4])).
% 5.61/1.21 fof(f42,plain,(
% 5.61/1.21 ![X0,X1]: (equalish(add(X0,X1),add(X1,X0))|~defined(X0)|~defined(X1))),
% 5.61/1.21 inference(cnf_transformation,[status(thm)],[f41])).
% 5.61/1.21 fof(f69,plain,(
% 5.61/1.21 ![X0,X1]: (equalish(X0,X1)|~equalish(X1,X0))),
% 5.61/1.21 inference(cnf_transformation,[status(thm)],[f22])).
% 5.61/1.21 fof(f70,plain,(
% 5.61/1.21 ![Z,Y]: ((![X]: (equalish(X,Z)|~equalish(X,Y)))|~equalish(Y,Z))),
% 5.61/1.21 inference(miniscoping,[status(thm)],[f23])).
% 5.61/1.21 fof(f71,plain,(
% 5.61/1.21 ![X0,X1,X2]: (equalish(X0,X1)|~equalish(X0,X2)|~equalish(X2,X1))),
% 5.61/1.21 inference(cnf_transformation,[status(thm)],[f70])).
% 5.61/1.21 fof(f72,plain,(
% 5.61/1.21 ![X,Y]: ((![Z]: (equalish(add(X,Z),add(Y,Z))|~defined(Z)))|~equalish(X,Y))),
% 5.61/1.21 inference(miniscoping,[status(thm)],[f24])).
% 5.61/1.21 fof(f73,plain,(
% 5.61/1.21 ![X0,X1,X2]: (equalish(add(X0,X1),add(X2,X1))|~defined(X1)|~equalish(X0,X2))),
% 5.61/1.21 inference(cnf_transformation,[status(thm)],[f72])).
% 5.61/1.21 fof(f80,plain,(
% 5.61/1.21 defined(b)),
% 5.61/1.21 inference(cnf_transformation,[status(thm)],[f29])).
% 5.61/1.21 fof(f81,plain,(
% 5.61/1.21 defined(c)),
% 5.61/1.21 inference(cnf_transformation,[status(thm)],[f30])).
% 5.61/1.21 fof(f84,plain,(
% 5.61/1.21 equalish(a,b)),
% 5.61/1.21 inference(cnf_transformation,[status(thm)],[f33])).
% 5.61/1.21 fof(f85,plain,(
% 5.61/1.21 equalish(c,d)),
% 5.61/1.21 inference(cnf_transformation,[status(thm)],[f34])).
% 5.61/1.21 fof(f86,plain,(
% 5.61/1.21 equalish(add(a,c),u)),
% 5.61/1.21 inference(cnf_transformation,[status(thm)],[f35])).
% 5.61/1.21 fof(f87,plain,(
% 5.61/1.21 ~equalish(add(d,b),u)),
% 5.61/1.21 inference(cnf_transformation,[status(thm)],[f36])).
% 5.61/1.21 fof(f88,plain,(
% 5.61/1.21 ~equalish(u,add(d,b))),
% 5.61/1.21 inference(resolution,[status(thm)],[f69,f87])).
% 5.61/1.21 fof(f90,plain,(
% 5.61/1.21 ![X0]: (~equalish(u,X0)|~equalish(X0,add(d,b)))),
% 5.61/1.21 inference(resolution,[status(thm)],[f71,f88])).
% 5.61/1.21 fof(f93,plain,(
% 5.61/1.21 ![X0]: (~equalish(X0,add(d,b))|~equalish(X0,u))),
% 5.61/1.21 inference(resolution,[status(thm)],[f90,f69])).
% 5.61/1.21 fof(f96,plain,(
% 5.61/1.21 ![X0,X1]: (~equalish(X0,u)|~equalish(X0,X1)|~equalish(X1,add(d,b)))),
% 5.61/1.21 inference(resolution,[status(thm)],[f93,f71])).
% 5.61/1.21 fof(f128,plain,(
% 5.61/1.21 ![X0,X1]: (equalish(add(X0,b),add(X1,b))|~equalish(X0,X1))),
% 5.61/1.21 inference(resolution,[status(thm)],[f80,f73])).
% 5.61/1.21 fof(f134,plain,(
% 5.61/1.21 ![X0,X1]: (equalish(add(X0,c),add(X1,c))|~equalish(X0,X1))),
% 5.61/1.21 inference(resolution,[status(thm)],[f81,f73])).
% 5.61/1.21 fof(f135,plain,(
% 5.61/1.21 ![X0]: (equalish(add(X0,c),add(c,X0))|~defined(X0))),
% 5.61/1.21 inference(resolution,[status(thm)],[f81,f42])).
% 5.61/1.21 fof(f516,definition,(
% 5.61/1.21 sQ35_spl <=> (defined(b))),
% 5.61/1.21 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 5.61/1.21 fof(f518,plain,(
% 5.61/1.21 ~defined(b)|sQ35_spl),
% 5.61/1.21 inference(component_clause,[status(thm)],[f516])).
% 5.61/1.21 fof(f520,plain,(
% 5.61/1.21 $false|sQ35_spl),
% 5.61/1.21 inference(forward_subsumption_resolution,[status(thm)],[f518,f80])).
% 5.61/1.21 fof(f521,plain,(
% 5.61/1.23 sQ35_spl),
% 5.61/1.23 inference(contradiction_clause,[status(thm)],[f520])).
% 5.61/1.23 fof(f1008,plain,(
% 5.61/1.23 equalish(add(c,b),add(d,b))),
% 5.61/1.23 inference(resolution,[status(thm)],[f128,f85])).
% 5.61/1.23 fof(f1460,plain,(
% 5.61/1.23 ![X0]: (~equalish(X0,u)|~equalish(X0,add(c,b)))),
% 5.61/1.23 inference(resolution,[status(thm)],[f1008,f96])).
% 5.61/1.23 fof(f1471,definition,(
% 5.61/1.23 sQ138_spl <=> (equalish(add(b,c),u))),
% 5.61/1.23 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 5.61/1.23 fof(f1473,plain,(
% 5.61/1.23 ~equalish(add(b,c),u)|sQ138_spl),
% 5.61/1.23 inference(component_clause,[status(thm)],[f1471])).
% 5.61/1.23 fof(f1478,plain,(
% 5.61/1.23 ![X0]: (~equalish(add(b,c),X0)|~equalish(X0,u)|sQ138_spl)),
% 5.61/1.23 inference(resolution,[status(thm)],[f1473,f71])).
% 5.61/1.23 fof(f1484,plain,(
% 5.61/1.23 ~equalish(add(b,c),u)|~defined(b)),
% 5.61/1.23 inference(resolution,[status(thm)],[f1460,f135])).
% 5.61/1.23 fof(f1498,plain,(
% 5.61/1.23 ~sQ138_spl|~sQ35_spl),
% 5.61/1.23 inference(split_clause,[status(thm)],[f1484,f1471,f516])).
% 5.61/1.23 fof(f1506,plain,(
% 5.61/1.23 ![X0]: (~equalish(add(X0,c),u)|~equalish(b,X0)|sQ138_spl)),
% 5.61/1.23 inference(resolution,[status(thm)],[f1478,f134])).
% 5.61/1.23 fof(f1584,plain,(
% 5.61/1.23 ~equalish(b,a)|sQ138_spl),
% 5.61/1.23 inference(resolution,[status(thm)],[f1506,f86])).
% 5.61/1.23 fof(f1588,plain,(
% 5.61/1.23 ~equalish(a,b)|sQ138_spl),
% 5.61/1.23 inference(resolution,[status(thm)],[f1584,f69])).
% 5.61/1.23 fof(f1589,plain,(
% 5.61/1.23 $false|sQ138_spl),
% 5.61/1.23 inference(forward_subsumption_resolution,[status(thm)],[f1588,f84])).
% 5.61/1.23 fof(f1590,plain,(
% 5.61/1.23 sQ138_spl),
% 5.61/1.23 inference(contradiction_clause,[status(thm)],[f1589])).
% 5.61/1.23 fof(f1591,plain,(
% 5.61/1.23 $false),
% 5.61/1.23 inference(sat_refutation,[status(thm)],[f521,f1498,f1590])).
% 5.61/1.23 % SZS output end CNFRefutation for theBenchmark.p
% 5.61/1.25 % Elapsed time: 0.883556 seconds
% 5.61/1.25 % CPU time: 6.705918 seconds
% 5.61/1.25 % Total memory used: 126.605 MB
% 5.61/1.25 % Net memory used: 119.250 MB
%------------------------------------------------------------------------------