%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM021-1 : TPTP v9.3.1. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 01:42:09 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM021-1 : TPTP v9.3.1. Bugfixed v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.72 % Computer : n010.cluster.edu
% 0.12/0.72 % Model : x86_64 x86_64
% 0.12/0.72 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.72 % Memory : 8046.5625MB
% 0.12/0.72 % OS : Linux 6.8.0-71-generic
% 0.12/0.72 % CPULimit : 300
% 0.12/0.72 % WCLimit : 300
% 0.12/0.72 % DateTime : Mon Sep 21 01:59:10 UTC 2026
% 0.12/0.72 % CPUTime :
% 0.12/0.73 % Drodi V4.1.1
% 0.12/0.78 % Refutation found
% 0.12/0.78 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.78 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.78 fof(f7,axiom,(
% 0.12/0.78 (![A,B,C]: (( ~ less(A,B)| ~ less(C,A)| less(C,B) ) ))),
% 0.12/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.78 fof(f8,axiom,(
% 0.12/0.78 (![A,B,C]: (( ~ equalish(add(successor(A),B),C)| less(B,C) ) ))),
% 0.12/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.78 fof(f9,axiom,(
% 0.12/0.78 (![A,B]: (( ~ less(A,B)| equalish(add(successor(predecessor_of_1st_minus_2nd(B,A)),A),B) ) ))),
% 0.12/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.78 fof(f10,axiom,(
% 0.12/0.78 (![A,B]: (( ~ divides(A,B)| less(A,B)| equalish(A,B) ) ))),
% 0.12/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.78 fof(f15,axiom,(
% 0.12/0.78 (![X,Y,Z]: (( ~ equalish(X,Y)| ~ equalish(Y,Z)| equalish(X,Z) ) ))),
% 0.12/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.78 fof(f16,hypothesis,(
% 0.12/0.78 less(b,c) ),
% 0.12/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.78 fof(f17,hypothesis,(
% 0.12/0.78 ~ less(b,a) ),
% 0.12/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.78 fof(f18,negated_conjecture,(
% 0.12/0.78 divides(c,a) ),
% 0.12/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.78 fof(f26,plain,(
% 0.12/0.78 ![B,C]: ((![A]: (~less(A,B)|~less(C,A)))|less(C,B))),
% 0.12/0.78 inference(miniscoping,[status(thm)],[f7])).
% 0.12/0.78 fof(f27,plain,(
% 0.12/0.78 ![X0,X1,X2]: (~less(X0,X1)|~less(X2,X0)|less(X2,X1))),
% 0.12/0.78 inference(cnf_transformation,[status(thm)],[f26])).
% 0.12/0.78 fof(f28,plain,(
% 0.12/0.78 ![B,C]: ((![A]: ~equalish(add(successor(A),B),C))|less(B,C))),
% 0.12/0.78 inference(miniscoping,[status(thm)],[f8])).
% 0.12/0.78 fof(f29,plain,(
% 0.12/0.78 ![X0,X1,X2]: (~equalish(add(successor(X0),X1),X2)|less(X1,X2))),
% 0.12/0.78 inference(cnf_transformation,[status(thm)],[f28])).
% 0.12/0.78 fof(f30,plain,(
% 0.12/0.78 ![X0,X1]: (~less(X0,X1)|equalish(add(successor(predecessor_of_1st_minus_2nd(X1,X0)),X0),X1))),
% 0.12/0.78 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.78 fof(f31,plain,(
% 0.12/0.78 ![X0,X1]: (~divides(X0,X1)|less(X0,X1)|equalish(X0,X1))),
% 0.12/0.78 inference(cnf_transformation,[status(thm)],[f10])).
% 0.12/0.78 fof(f36,plain,(
% 0.12/0.78 ![X,Z]: ((![Y]: (~equalish(X,Y)|~equalish(Y,Z)))|equalish(X,Z))),
% 0.12/0.78 inference(miniscoping,[status(thm)],[f15])).
% 0.12/0.78 fof(f37,plain,(
% 0.12/0.78 ![X0,X1,X2]: (~equalish(X0,X1)|~equalish(X1,X2)|equalish(X0,X2))),
% 0.12/0.78 inference(cnf_transformation,[status(thm)],[f36])).
% 0.12/0.78 fof(f38,plain,(
% 0.12/0.78 less(b,c)),
% 0.12/0.78 inference(cnf_transformation,[status(thm)],[f16])).
% 0.12/0.78 fof(f39,plain,(
% 0.12/0.78 ~less(b,a)),
% 0.12/0.78 inference(cnf_transformation,[status(thm)],[f17])).
% 0.12/0.78 fof(f40,plain,(
% 0.12/0.78 divides(c,a)),
% 0.12/0.78 inference(cnf_transformation,[status(thm)],[f18])).
% 0.12/0.78 fof(f64,plain,(
% 0.12/0.78 less(c,a)|equalish(c,a)),
% 0.12/0.78 inference(resolution,[status(thm)],[f31,f40])).
% 0.12/0.78 fof(f73,definition,(
% 0.12/0.78 sQ2_spl <=> (less(c,a))),
% 0.12/0.78 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.78 fof(f74,plain,(
% 0.12/0.78 less(c,a)|~sQ2_spl),
% 0.12/0.78 inference(component_clause,[status(thm)],[f73])).
% 0.12/0.78 fof(f76,definition,(
% 0.12/0.78 sQ3_spl <=> (equalish(c,a))),
% 0.12/0.78 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.78 fof(f77,plain,(
% 0.12/0.78 equalish(c,a)|~sQ3_spl),
% 0.12/0.78 inference(component_clause,[status(thm)],[f76])).
% 0.12/0.78 fof(f79,plain,(
% 0.12/0.78 sQ2_spl|sQ3_spl),
% 0.12/0.78 inference(split_clause,[status(thm)],[f64,f73,f76])).
% 0.12/0.78 fof(f377,plain,(
% 0.12/0.78 ![X0]: (~less(c,X0)|less(b,X0))),
% 0.12/0.78 inference(resolution,[status(thm)],[f27,f38])).
% 0.12/0.78 fof(f378,plain,(
% 0.12/0.78 less(b,a)|~sQ2_spl),
% 0.12/0.78 inference(resolution,[status(thm)],[f377,f74])).
% 0.12/0.78 fof(f379,plain,(
% 0.12/0.78 $false|~sQ2_spl),
% 0.12/0.78 inference(forward_subsumption_resolution,[status(thm)],[f378,f39])).
% 0.12/0.78 fof(f380,plain,(
% 0.12/0.78 ~sQ2_spl),
% 0.12/0.78 inference(contradiction_clause,[status(thm)],[f379])).
% 0.12/0.78 fof(f382,plain,(
% 0.12/0.78 ![X0]: (~equalish(X0,c)|equalish(X0,a)|~sQ3_spl)),
% 0.12/0.78 inference(resolution,[status(thm)],[f77,f37])).
% 0.12/0.78 fof(f399,plain,(
% 0.12/0.78 equalish(add(successor(predecessor_of_1st_minus_2nd(c,b)),b),c)),
% 0.12/0.78 inference(resolution,[status(thm)],[f30,f38])).
% 0.12/0.78 fof(f636,definition,(
% 0.12/0.78 sQ24_spl <=> (less(b,a))),
% 0.12/0.78 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.12/0.78 fof(f637,plain,(
% 0.12/0.78 less(b,a)|~sQ24_spl),
% 0.12/0.78 inference(component_clause,[status(thm)],[f636])).
% 0.12/0.78 fof(f643,plain,(
% 0.12/0.78 $false|~sQ24_spl),
% 0.12/0.78 inference(forward_subsumption_resolution,[status(thm)],[f637,f39])).
% 0.12/0.78 fof(f644,plain,(
% 0.12/0.78 ~sQ24_spl),
% 0.12/0.78 inference(contradiction_clause,[status(thm)],[f643])).
% 0.12/0.78 fof(f813,plain,(
% 0.12/0.78 equalish(add(successor(predecessor_of_1st_minus_2nd(c,b)),b),a)|~sQ3_spl),
% 0.12/0.78 inference(resolution,[status(thm)],[f399,f382])).
% 0.12/0.78 fof(f933,plain,(
% 0.12/0.78 less(b,a)|~sQ3_spl),
% 0.12/0.78 inference(resolution,[status(thm)],[f813,f29])).
% 0.12/0.78 fof(f942,plain,(
% 0.12/0.78 sQ24_spl|~sQ3_spl),
% 0.12/0.78 inference(split_clause,[status(thm)],[f933,f636,f76])).
% 0.12/0.78 fof(f943,plain,(
% 0.12/0.78 $false),
% 0.12/0.78 inference(sat_refutation,[status(thm)],[f79,f380,f644,f942])).
% 0.12/0.78 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.80 % Elapsed time: 0.073312 seconds
% 0.16/0.80 % CPU time: 0.172009 seconds
% 0.16/0.80 % Total memory used: 18.650 MB
% 0.16/0.80 % Net memory used: 18.192 MB
%------------------------------------------------------------------------------