%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV008-1 : TPTP v9.3.1. Released v1.0.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 02:49:55 PM UTC 2026
% Result : Unsatisfiable 0.10s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV008-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 08:24:21 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.10/0.39 % Refutation found
% 0.10/0.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.39 fof(f5,axiom,(
% 0.10/0.39 (![X]: (less_than(predecessor(X),X) ))),
% 0.10/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f8,axiom,(
% 0.10/0.39 (![X,Y]: (( less_than(X,Y)| less_than(Y,X)| X = Y ) ))),
% 0.10/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f10,axiom,(
% 0.10/0.39 (![X,Y]: (( ~ less_than(X,Y)| ~ less_than(Y,X) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f13,negated_conjecture,(
% 0.10/0.39 ~ less_than(n,l) ),
% 0.10/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f14,negated_conjecture,(
% 0.10/0.39 less_than(one,l) ),
% 0.10/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f15,negated_conjecture,(
% 0.10/0.39 less_than(a(l),a(predecessor(l))) ),
% 0.10/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f16,negated_conjecture,(
% 0.10/0.39 (![X]: (( less_than(X,n)| less_than(n,X)| ~ less_than(one,n)| ~ less_than(a(X),a(predecessor(n))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f17,negated_conjecture,(
% 0.10/0.39 (![X]: (( ~ less_than(one,X)| ~ less_than(X,n)| ~ less_than(a(X),a(predecessor(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f22,plain,(
% 0.10/0.39 ![X0]: (less_than(predecessor(X0),X0))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.39 fof(f26,plain,(
% 0.10/0.39 ![X0,X1]: (less_than(X0,X1)|less_than(X1,X0)|X0=X1)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.39 fof(f28,plain,(
% 0.10/0.39 ![X0,X1]: (~less_than(X0,X1)|~less_than(X1,X0))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f10])).
% 0.10/0.39 fof(f33,plain,(
% 0.10/0.39 ~less_than(n,l)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f13])).
% 0.10/0.39 fof(f34,plain,(
% 0.10/0.39 less_than(one,l)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f14])).
% 0.10/0.39 fof(f35,plain,(
% 0.10/0.39 less_than(a(l),a(predecessor(l)))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.39 fof(f36,plain,(
% 0.10/0.39 ![X0]: (less_than(X0,n)|less_than(n,X0)|~less_than(one,n)|~less_than(a(X0),a(predecessor(n))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f16])).
% 0.10/0.39 fof(f37,plain,(
% 0.10/0.39 ![X0]: (~less_than(one,X0)|~less_than(X0,n)|~less_than(a(X0),a(predecessor(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f17])).
% 0.10/0.39 fof(f38,definition,(
% 0.10/0.39 ![X0]: (sQ0_spl <=> (less_than(X0,n)|less_than(n,X0)|~less_than(a(X0),a(predecessor(n)))))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f39,plain,(
% 0.10/0.39 ![X0]: (less_than(X0,n)|less_than(n,X0)|~less_than(a(X0),a(predecessor(n)))|~sQ0_spl)),
% 0.10/0.39 inference(component_clause,[status(thm)],[f38])).
% 0.10/0.39 fof(f41,definition,(
% 0.10/0.39 sQ1_spl <=> (less_than(one,n))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f43,plain,(
% 0.10/0.39 ~less_than(one,n)|sQ1_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f41])).
% 0.10/0.39 fof(f44,plain,(
% 0.10/0.39 sQ0_spl|~sQ1_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f36,f38,f41])).
% 0.10/0.39 fof(f45,plain,(
% 0.10/0.39 ~less_than(one,l)|~less_than(l,n)),
% 0.10/0.39 inference(resolution,[status(thm)],[f37,f35])).
% 0.10/0.39 fof(f46,definition,(
% 0.10/0.39 sQ2_spl <=> (less_than(one,l))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f48,plain,(
% 0.10/0.39 ~less_than(one,l)|sQ2_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f46])).
% 0.10/0.39 fof(f49,definition,(
% 0.10/0.39 sQ3_spl <=> (less_than(l,n))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f52,plain,(
% 0.10/0.39 ~sQ2_spl|~sQ3_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f45,f46,f49])).
% 0.10/0.39 fof(f53,plain,(
% 0.10/0.39 $false|sQ2_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f48,f34])).
% 0.10/0.39 fof(f54,plain,(
% 0.10/0.39 sQ2_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f53])).
% 0.10/0.39 fof(f56,plain,(
% 0.10/0.39 ![X0]: (~less_than(X0,predecessor(X0)))),
% 0.10/0.39 inference(resolution,[status(thm)],[f28,f22])).
% 0.10/0.39 fof(f64,plain,(
% 0.10/0.39 less_than(l,n)|n=l),
% 0.10/0.39 inference(resolution,[status(thm)],[f26,f33])).
% 0.10/0.39 fof(f82,definition,(
% 0.10/0.39 sQ5_spl <=> (less_than(n,l))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f83,plain,(
% 0.10/0.39 less_than(n,l)|~sQ5_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f82])).
% 0.10/0.39 fof(f85,definition,(
% 0.10/0.39 sQ6_spl <=> (l=n)),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f86,plain,(
% 0.10/0.39 l=n|~sQ6_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f85])).
% 0.10/0.39 fof(f95,definition,(
% 0.10/0.39 sQ9_spl <=> (less_than(n,predecessor(n)))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f96,plain,(
% 0.10/0.39 less_than(n,predecessor(n))|~sQ9_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f95])).
% 0.10/0.39 fof(f99,plain,(
% 0.10/0.39 sQ3_spl|sQ6_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f64,f49,f85])).
% 0.10/0.39 fof(f103,plain,(
% 0.10/0.39 $false|~sQ5_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f83,f33])).
% 0.10/0.39 fof(f104,plain,(
% 0.10/0.39 ~sQ5_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f103])).
% 0.10/0.39 fof(f105,plain,(
% 0.10/0.39 $false|~sQ9_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f96,f56])).
% 0.10/0.39 fof(f106,plain,(
% 0.10/0.39 ~sQ9_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f105])).
% 0.10/0.39 fof(f108,plain,(
% 0.10/0.39 ![X0]: (~less_than(one,X0)|~less_than(X0,l)|~less_than(a(X0),a(predecessor(X0)))|~sQ6_spl)),
% 0.10/0.39 inference(backward_demodulation,[status(thm)],[f86,f37])).
% 0.10/0.39 fof(f110,plain,(
% 0.10/0.39 ~less_than(one,l)|~sQ6_spl|sQ1_spl),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f86,f43])).
% 0.10/0.39 fof(f111,plain,(
% 0.10/0.39 $false|~sQ6_spl|sQ1_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f110,f34])).
% 0.10/0.39 fof(f112,plain,(
% 0.10/0.39 ~sQ6_spl|sQ1_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f111])).
% 0.10/0.39 fof(f114,plain,(
% 0.10/0.39 ![X0]: (less_than(X0,l)|less_than(n,X0)|~less_than(a(X0),a(predecessor(n)))|~sQ6_spl|~sQ0_spl)),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f86,f39])).
% 0.10/0.39 fof(f115,plain,(
% 0.10/0.39 ![X0]: (less_than(X0,l)|less_than(l,X0)|~less_than(a(X0),a(predecessor(n)))|~sQ6_spl|~sQ0_spl)),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f86,f114])).
% 0.10/0.39 fof(f116,plain,(
% 0.10/0.39 ![X0]: (less_than(X0,l)|less_than(l,X0)|~less_than(a(X0),a(predecessor(l)))|~sQ6_spl|~sQ0_spl)),
% 0.10/0.39 inference(forward_demodulation,[status(thm)],[f86,f115])).
% 0.10/0.39 fof(f139,plain,(
% 0.10/0.39 ~less_than(one,l)|~less_than(l,l)|~sQ6_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f108,f35])).
% 0.10/0.39 fof(f142,definition,(
% 0.10/0.39 sQ10_spl <=> (less_than(l,l))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f145,plain,(
% 0.10/0.39 ~sQ2_spl|~sQ10_spl|~sQ6_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f139,f46,f142,f85])).
% 0.10/0.39 fof(f146,plain,(
% 0.10/0.39 less_than(l,l)|less_than(l,l)|~sQ6_spl|~sQ0_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f116,f35])).
% 0.10/0.39 fof(f151,plain,(
% 0.10/0.39 sQ10_spl|~sQ6_spl|~sQ0_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f146,f142,f85,f38])).
% 0.10/0.39 fof(f163,plain,(
% 0.10/0.39 $false),
% 0.10/0.39 inference(sat_refutation,[status(thm)],[f44,f52,f54,f99,f104,f106,f112,f145,f151])).
% 0.10/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.41 % Elapsed time: 0.044992 seconds
% 0.13/0.41 % CPU time: 0.136561 seconds
% 0.13/0.41 % Total memory used: 70.101 MB
% 0.13/0.41 % Net memory used: 69.795 MB
%------------------------------------------------------------------------------