%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR004+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:14:34 PM UTC 2026
% Result : Theorem 0.12s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR004+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n009.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 14:23:42 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.12/0.39 % Refutation found
% 0.12/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.39 fof(f16,axiom,(
% 0.12/0.39 (! [Event,Time] :( happens(Event,Time)<=> ( ( Event = tapOn& Time = n0 )| ( holdsAt(waterLevel(n3),Time)& holdsAt(filling,Time)& Event = overflow ) ) ) )),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f55,lemma,(
% 0.12/0.39 holdsAt(waterLevel(n3),n3) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f56,lemma,(
% 0.12/0.39 holdsAt(filling,n3) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f57,conjecture,(
% 0.12/0.39 happens(overflow,n3) ),
% 0.12/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f58,negated_conjecture,(
% 0.12/0.39 ~(happens(overflow,n3) )),
% 0.12/0.39 inference(negated_conjecture,[status(cth)],[f57])).
% 0.12/0.39 fof(f134,definition,(
% 0.12/0.39 ![Event,Time]: (sP1_prd(Time,Event)<=>(Event=tapOn&Time=n0))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.12/0.39 fof(f135,plain,(
% 0.12/0.39 ![Event,Time]: (happens(Event,Time)<=>(sP1_prd(Time,Event)|((holdsAt(waterLevel(n3),Time)&holdsAt(filling,Time))&Event=overflow)))),
% 0.12/0.39 inference(formula_renaming,[status(thm)],[f16,f134])).
% 0.12/0.39 fof(f136,plain,(
% 0.12/0.39 ![Event,Time]: ((~happens(Event,Time)|(sP1_prd(Time,Event)|((holdsAt(waterLevel(n3),Time)&holdsAt(filling,Time))&Event=overflow)))&(happens(Event,Time)|(~sP1_prd(Time,Event)&((~holdsAt(waterLevel(n3),Time)|~holdsAt(filling,Time))|~Event=overflow))))),
% 0.12/0.39 inference(NNF_transformation,[status(thm)],[f135])).
% 0.12/0.39 fof(f137,plain,(
% 0.12/0.39 (![Event,Time]: (~happens(Event,Time)|(sP1_prd(Time,Event)|((holdsAt(waterLevel(n3),Time)&holdsAt(filling,Time))&Event=overflow))))&(![Event,Time]: (happens(Event,Time)|(~sP1_prd(Time,Event)&((~holdsAt(waterLevel(n3),Time)|~holdsAt(filling,Time))|~Event=overflow))))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f136])).
% 0.12/0.39 fof(f142,plain,(
% 0.12/0.39 ![X0,X1]: (happens(X0,X1)|~holdsAt(waterLevel(n3),X1)|~holdsAt(filling,X1)|~X0=overflow)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f137])).
% 0.12/0.39 fof(f224,plain,(
% 0.12/0.39 holdsAt(waterLevel(n3),n3)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f55])).
% 0.12/0.39 fof(f225,plain,(
% 0.12/0.39 holdsAt(filling,n3)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f56])).
% 0.12/0.39 fof(f226,plain,(
% 0.12/0.39 ~happens(overflow,n3)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f58])).
% 0.12/0.39 fof(f255,plain,(
% 0.12/0.39 ![X0]: (happens(overflow,X0)|~holdsAt(waterLevel(n3),X0)|~holdsAt(filling,X0))),
% 0.12/0.39 inference(destructive_equality_resolution,[status(thm)],[f142])).
% 0.12/0.39 fof(f271,plain,(
% 0.12/0.39 happens(overflow,n3)|~holdsAt(filling,n3)),
% 0.12/0.39 inference(resolution,[status(thm)],[f255,f224])).
% 0.12/0.39 fof(f272,definition,(
% 0.12/0.39 sQ2_spl <=> (happens(overflow,n3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f273,plain,(
% 0.12/0.39 happens(overflow,n3)|~sQ2_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f272])).
% 0.12/0.39 fof(f275,definition,(
% 0.12/0.39 sQ3_spl <=> (holdsAt(filling,n3))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f277,plain,(
% 0.12/0.39 ~holdsAt(filling,n3)|sQ3_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f275])).
% 0.12/0.39 fof(f278,plain,(
% 0.12/0.39 sQ2_spl|~sQ3_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f271,f272,f275])).
% 0.12/0.39 fof(f279,plain,(
% 0.12/0.39 $false|~sQ2_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f273,f226])).
% 0.12/0.39 fof(f280,plain,(
% 0.12/0.39 ~sQ2_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f279])).
% 0.12/0.39 fof(f281,plain,(
% 0.12/0.39 $false|sQ3_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f277,f225])).
% 0.12/0.39 fof(f282,plain,(
% 0.12/0.39 sQ3_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f281])).
% 0.12/0.39 fof(f283,plain,(
% 0.12/0.39 $false),
% 0.12/0.39 inference(sat_refutation,[status(thm)],[f278,f280,f282])).
% 0.12/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.43 % Elapsed time: 0.052047 seconds
% 0.12/0.43 % CPU time: 0.153429 seconds
% 0.12/0.43 % Total memory used: 105.543 MB
% 0.12/0.43 % Net memory used: 105.440 MB
%------------------------------------------------------------------------------