%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM841+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:43:55 PM UTC 2026
% Result : Theorem 1.21s 0.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM841+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n016.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 03:17:37 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 1.21/0.77 % Refutation found
% 1.21/0.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.21/0.77 % SZS output start CNFRefutation for theBenchmark
% 1.21/0.77 fof(f1,conjecture,(
% 1.21/0.77 greater(vplus(vd344,vd347),vplus(vd345,vd348)) ),
% 1.21/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.21/0.77 fof(f2,negated_conjecture,(
% 1.21/0.77 ~(greater(vplus(vd344,vd347),vplus(vd345,vd348)) )),
% 1.21/0.77 inference(negated_conjecture,[status(cth)],[f1])).
% 1.21/0.77 fof(f4,axiom,(
% 1.21/0.77 greater(vplus(vd347,vd345),vplus(vd348,vd345)) ),
% 1.21/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.21/0.77 fof(f6,axiom,(
% 1.21/0.77 greater(vplus(vd344,vd347),vplus(vd345,vd347)) ),
% 1.21/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.21/0.77 fof(f18,axiom,(
% 1.21/0.77 (! [Vd262,Vd263,Vd265] :( ( less(Vd263,Vd265)& less(Vd262,Vd263) )=> less(Vd262,Vd265) ) )),
% 1.21/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.21/0.77 fof(f24,axiom,(
% 1.21/0.77 (! [Vd208,Vd209] :( greater(Vd208,Vd209)=> less(Vd209,Vd208) ) )),
% 1.21/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.21/0.77 fof(f25,axiom,(
% 1.21/0.77 (! [Vd203,Vd204] :( Vd203 = Vd204| greater(Vd203,Vd204)| less(Vd203,Vd204) ) )),
% 1.21/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.21/0.77 fof(f27,axiom,(
% 1.21/0.77 (! [Vd203,Vd204] :( ~ greater(Vd203,Vd204)| ~ less(Vd203,Vd204) ) )),
% 1.21/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.21/0.77 fof(f37,axiom,(
% 1.21/0.77 (! [Vd78,Vd79] : vplus(Vd79,Vd78) = vplus(Vd78,Vd79) )),
% 1.21/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.21/0.77 fof(f47,plain,(
% 1.21/0.77 ~greater(vplus(vd344,vd347),vplus(vd345,vd348))),
% 1.21/0.77 inference(cnf_transformation,[status(thm)],[f2])).
% 1.21/0.77 fof(f49,plain,(
% 1.21/0.77 greater(vplus(vd347,vd345),vplus(vd348,vd345))),
% 1.21/0.77 inference(cnf_transformation,[status(thm)],[f4])).
% 1.21/0.77 fof(f51,plain,(
% 1.21/0.77 greater(vplus(vd344,vd347),vplus(vd345,vd347))),
% 1.21/0.77 inference(cnf_transformation,[status(thm)],[f6])).
% 1.21/0.77 fof(f80,plain,(
% 1.21/0.77 ![Vd262,Vd263,Vd265]: ((~less(Vd263,Vd265)|~less(Vd262,Vd263))|less(Vd262,Vd265))),
% 1.21/0.77 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 1.21/0.77 fof(f81,plain,(
% 1.21/0.77 ![Vd262,Vd265]: ((![Vd263]: (~less(Vd263,Vd265)|~less(Vd262,Vd263)))|less(Vd262,Vd265))),
% 1.21/0.77 inference(miniscoping,[status(thm)],[f80])).
% 1.21/0.77 fof(f82,plain,(
% 1.21/0.77 ![X0,X1,X2]: (~less(X0,X1)|~less(X2,X0)|less(X2,X1))),
% 1.21/0.77 inference(cnf_transformation,[status(thm)],[f81])).
% 1.21/0.77 fof(f99,plain,(
% 1.21/0.77 ![Vd208,Vd209]: (~greater(Vd208,Vd209)|less(Vd209,Vd208))),
% 1.21/0.77 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 1.21/0.77 fof(f100,plain,(
% 1.21/0.77 ![X0,X1]: (~greater(X0,X1)|less(X1,X0))),
% 1.21/0.77 inference(cnf_transformation,[status(thm)],[f99])).
% 1.21/0.77 fof(f101,plain,(
% 1.21/0.77 ![X0,X1]: (X0=X1|greater(X0,X1)|less(X0,X1))),
% 1.21/0.77 inference(cnf_transformation,[status(thm)],[f25])).
% 1.21/0.77 fof(f103,plain,(
% 1.21/0.77 ![X0,X1]: (~greater(X0,X1)|~less(X0,X1))),
% 1.21/0.77 inference(cnf_transformation,[status(thm)],[f27])).
% 1.21/0.77 fof(f126,plain,(
% 1.21/0.77 ![X0,X1]: (vplus(X0,X1)=vplus(X1,X0))),
% 1.21/0.77 inference(cnf_transformation,[status(thm)],[f37])).
% 1.21/0.77 fof(f162,plain,(
% 1.21/0.77 ~greater(vplus(vd347,vd344),vplus(vd345,vd348))),
% 1.21/0.77 inference(backward_demodulation,[status(thm)],[f126,f47])).
% 1.21/0.77 fof(f177,plain,(
% 1.21/0.77 greater(vplus(vd345,vd347),vplus(vd348,vd345))),
% 1.21/0.77 inference(forward_demodulation,[status(thm)],[f126,f49])).
% 1.21/0.77 fof(f178,plain,(
% 1.21/0.77 greater(vplus(vd345,vd347),vplus(vd345,vd348))),
% 1.21/0.77 inference(forward_demodulation,[status(thm)],[f126,f177])).
% 1.21/0.77 fof(f180,plain,(
% 1.21/0.77 less(vplus(vd345,vd348),vplus(vd345,vd347))),
% 1.21/0.77 inference(resolution,[status(thm)],[f178,f100])).
% 1.21/0.77 fof(f199,plain,(
% 1.21/0.77 greater(vplus(vd347,vd344),vplus(vd345,vd347))),
% 1.21/0.77 inference(forward_demodulation,[status(thm)],[f126,f51])).
% 1.21/0.77 fof(f200,plain,(
% 1.21/0.77 ~less(vplus(vd347,vd344),vplus(vd345,vd347))),
% 1.21/0.77 inference(resolution,[status(thm)],[f199,f103])).
% 1.21/0.77 fof(f242,plain,(
% 1.21/0.77 vplus(vd347,vd344)=vplus(vd345,vd348)|less(vplus(vd347,vd344),vplus(vd345,vd348))),
% 1.21/0.77 inference(resolution,[status(thm)],[f101,f162])).
% 1.21/0.77 fof(f247,definition,(
% 1.21/0.77 sQ0_spl <=> (vplus(vd347,vd344)=vplus(vd345,vd348))),
% 1.21/0.77 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.21/0.77 fof(f248,plain,(
% 1.21/0.77 vplus(vd347,vd344)=vplus(vd345,vd348)|~sQ0_spl),
% 1.21/0.77 inference(component_clause,[status(thm)],[f247])).
% 1.21/0.77 fof(f250,definition,(
% 1.21/0.77 sQ1_spl <=> (less(vplus(vd347,vd344),vplus(vd345,vd348)))),
% 1.21/0.78 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 1.21/0.78 fof(f251,plain,(
% 1.21/0.78 less(vplus(vd347,vd344),vplus(vd345,vd348))|~sQ1_spl),
% 1.21/0.78 inference(component_clause,[status(thm)],[f250])).
% 1.21/0.78 fof(f253,plain,(
% 1.21/0.78 sQ0_spl|sQ1_spl),
% 1.21/0.78 inference(split_clause,[status(thm)],[f242,f247,f250])).
% 1.21/0.78 fof(f378,plain,(
% 1.21/0.78 greater(vplus(vd345,vd348),vplus(vd345,vd347))|~sQ0_spl),
% 1.21/0.78 inference(backward_demodulation,[status(thm)],[f248,f199])).
% 1.21/0.78 fof(f424,plain,(
% 1.21/0.78 ~less(vplus(vd345,vd348),vplus(vd345,vd347))|~sQ0_spl),
% 1.21/0.78 inference(resolution,[status(thm)],[f378,f103])).
% 1.21/0.78 fof(f884,plain,(
% 1.21/0.78 ![X0]: (~less(vplus(vd345,vd348),X0)|less(vplus(vd347,vd344),X0)|~sQ1_spl)),
% 1.21/0.78 inference(resolution,[status(thm)],[f251,f82])).
% 1.21/0.78 fof(f2175,plain,(
% 1.21/0.78 $false|~sQ0_spl),
% 1.21/0.78 inference(forward_subsumption_resolution,[status(thm)],[f424,f180])).
% 1.21/0.78 fof(f2176,plain,(
% 1.21/0.78 ~sQ0_spl),
% 1.21/0.78 inference(contradiction_clause,[status(thm)],[f2175])).
% 1.21/0.78 fof(f2796,plain,(
% 1.21/0.78 less(vplus(vd347,vd344),vplus(vd345,vd347))|~sQ1_spl),
% 1.21/0.78 inference(resolution,[status(thm)],[f884,f180])).
% 1.21/0.78 fof(f2809,plain,(
% 1.21/0.78 $false|~sQ1_spl),
% 1.21/0.78 inference(forward_subsumption_resolution,[status(thm)],[f2796,f200])).
% 1.21/0.78 fof(f2810,plain,(
% 1.21/0.78 ~sQ1_spl),
% 1.21/0.78 inference(contradiction_clause,[status(thm)],[f2809])).
% 1.21/0.78 fof(f2811,plain,(
% 1.21/0.78 $false),
% 1.21/0.78 inference(sat_refutation,[status(thm)],[f253,f2176,f2810])).
% 1.21/0.78 % SZS output end CNFRefutation for theBenchmark.p
% 1.64/0.79 % Elapsed time: 0.403189 seconds
% 1.64/0.79 % CPU time: 2.891559 seconds
% 1.64/0.79 % Total memory used: 139.909 MB
% 1.64/0.79 % Net memory used: 135.035 MB
%------------------------------------------------------------------------------