%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR154+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:15:41 PM UTC 2026
% Result : Satisfiable 0.11s 0.59s
% Output : Saturation 0.11s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [Time1,Fluent,Time2] :
( stoppedIn(Time1,Fluent,Time2)
<=> ? [Event,Time] :
( terminates(Event,Fluent,Time)
& less(Time,Time2)
& less(Time1,Time)
& happens(Event,Time) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [Time1,Time2,Fluent] :
( startedIn(Time1,Fluent,Time2)
<=> ? [Event,Time] :
( initiates(Event,Fluent,Time)
& less(Time,Time2)
& less(Time1,Time)
& happens(Event,Time) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [Event,Time,Fluent,Fluent2,Offset] :
( ( ~ stoppedIn(Time,Fluent,plus(Time,Offset))
& trajectory(Fluent,Time,Fluent2,Offset)
& less(n0,Offset)
& initiates(Event,Fluent,Time)
& happens(Event,Time) )
=> holdsAt(Fluent2,plus(Time,Offset)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [Event,Time1,Fluent1,Time2,Fluent2] :
( ( ~ startedIn(Time1,Fluent1,plus(Time1,Time2))
& antitrajectory(Fluent1,Time1,Fluent2,Time2)
& less(n0,Time2)
& terminates(Event,Fluent1,Time1)
& happens(Event,Time1) )
=> holdsAt(Fluent2,plus(Time1,Time2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [Fluent,Time] :
( ( ~ ? [Event] :
( terminates(Event,Fluent,Time)
& happens(Event,Time) )
& ~ releasedAt(Fluent,plus(Time,n1))
& holdsAt(Fluent,Time) )
=> holdsAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [Fluent,Time] :
( ( ~ ? [Event] :
( initiates(Event,Fluent,Time)
& happens(Event,Time) )
& ~ releasedAt(Fluent,plus(Time,n1))
& ~ holdsAt(Fluent,Time) )
=> ~ holdsAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [Fluent,Time] :
( ( ~ ? [Event] :
( ( terminates(Event,Fluent,Time)
| initiates(Event,Fluent,Time) )
& happens(Event,Time) )
& releasedAt(Fluent,Time) )
=> releasedAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [Fluent,Time] :
( ( ~ ? [Event] :
( releases(Event,Fluent,Time)
& happens(Event,Time) )
& ~ releasedAt(Fluent,Time) )
=> ~ releasedAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [Event,Time,Fluent] :
( ( initiates(Event,Fluent,Time)
& happens(Event,Time) )
=> holdsAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [Event,Time,Fluent] :
( ( terminates(Event,Fluent,Time)
& happens(Event,Time) )
=> ~ holdsAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [Event,Time,Fluent] :
( ( releases(Event,Fluent,Time)
& happens(Event,Time) )
=> releasedAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [Event,Time,Fluent] :
( ( ( terminates(Event,Fluent,Time)
| initiates(Event,Fluent,Time) )
& happens(Event,Time) )
=> ~ releasedAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,plain,
! [Time1,Fluent,Time2] :
( ( ! [Event,Time] :
( ~ terminates(Event,Fluent,Time)
| ~ less(Time,Time2)
| ~ less(Time1,Time)
| ~ happens(Event,Time) )
| stoppedIn(Time1,Fluent,Time2) )
& ( ? [Event,Time] :
( terminates(Event,Fluent,Time)
& less(Time,Time2)
& less(Time1,Time)
& happens(Event,Time) )
| ~ stoppedIn(Time1,Fluent,Time2) ) ),
inference(NNF_transformation,[status(thm)],[f1]) ).
fof(f14,plain,
( ! [Time1,Fluent,Time2] :
( ! [Event,Time] :
( ~ terminates(Event,Fluent,Time)
| ~ less(Time,Time2)
| ~ less(Time1,Time)
| ~ happens(Event,Time) )
| stoppedIn(Time1,Fluent,Time2) )
& ! [Time1,Fluent,Time2] :
( ? [Event,Time] :
( terminates(Event,Fluent,Time)
& less(Time,Time2)
& less(Time1,Time)
& happens(Event,Time) )
| ~ stoppedIn(Time1,Fluent,Time2) ) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f15,plain,
( ! [Time1,Fluent,Time2] :
( ! [Event,Time] :
( ~ terminates(Event,Fluent,Time)
| ~ less(Time,Time2)
| ~ less(Time1,Time)
| ~ happens(Event,Time) )
| stoppedIn(Time1,Fluent,Time2) )
& ! [Time1,Fluent,Time2] :
( ( terminates(sK0_skl(Time2,Fluent,Time1),Fluent,sK1_skl(Time2,Fluent,Time1))
& less(sK1_skl(Time2,Fluent,Time1),Time2)
& less(Time1,sK1_skl(Time2,Fluent,Time1))
& happens(sK0_skl(Time2,Fluent,Time1),sK1_skl(Time2,Fluent,Time1)) )
| ~ stoppedIn(Time1,Fluent,Time2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Event,sK0_skl(Time2,Fluent,Time1)),skolemize(Time,sK1_skl(Time2,Fluent,Time1))],[f14]) ).
fof(f16,plain,
! [X0,X1,X2] :
( happens(sK0_skl(X2,X1,X0),sK1_skl(X2,X1,X0))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f17,plain,
! [X0,X1,X2] :
( less(X0,sK1_skl(X2,X1,X0))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f18,plain,
! [X0,X1,X2] :
( less(sK1_skl(X2,X1,X0),X2)
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f19,plain,
! [X0,X1,X2] :
( terminates(sK0_skl(X2,X1,X0),X1,sK1_skl(X2,X1,X0))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f20,plain,
! [X0,X1,X2,X3,X4] :
( ~ terminates(X3,X1,X4)
| ~ less(X4,X2)
| ~ less(X0,X4)
| ~ happens(X3,X4)
| stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f21,plain,
! [Time1,Time2,Fluent] :
( ( ! [Event,Time] :
( ~ initiates(Event,Fluent,Time)
| ~ less(Time,Time2)
| ~ less(Time1,Time)
| ~ happens(Event,Time) )
| startedIn(Time1,Fluent,Time2) )
& ( ? [Event,Time] :
( initiates(Event,Fluent,Time)
& less(Time,Time2)
& less(Time1,Time)
& happens(Event,Time) )
| ~ startedIn(Time1,Fluent,Time2) ) ),
inference(NNF_transformation,[status(thm)],[f2]) ).
fof(f22,plain,
( ! [Time1,Time2,Fluent] :
( ! [Event,Time] :
( ~ initiates(Event,Fluent,Time)
| ~ less(Time,Time2)
| ~ less(Time1,Time)
| ~ happens(Event,Time) )
| startedIn(Time1,Fluent,Time2) )
& ! [Time1,Time2,Fluent] :
( ? [Event,Time] :
( initiates(Event,Fluent,Time)
& less(Time,Time2)
& less(Time1,Time)
& happens(Event,Time) )
| ~ startedIn(Time1,Fluent,Time2) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f23,plain,
( ! [Time1,Time2,Fluent] :
( ! [Event,Time] :
( ~ initiates(Event,Fluent,Time)
| ~ less(Time,Time2)
| ~ less(Time1,Time)
| ~ happens(Event,Time) )
| startedIn(Time1,Fluent,Time2) )
& ! [Time1,Time2,Fluent] :
( ( initiates(sK2_skl(Fluent,Time2,Time1),Fluent,sK3_skl(Fluent,Time2,Time1))
& less(sK3_skl(Fluent,Time2,Time1),Time2)
& less(Time1,sK3_skl(Fluent,Time2,Time1))
& happens(sK2_skl(Fluent,Time2,Time1),sK3_skl(Fluent,Time2,Time1)) )
| ~ startedIn(Time1,Fluent,Time2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(Event,sK2_skl(Fluent,Time2,Time1)),skolemize(Time,sK3_skl(Fluent,Time2,Time1))],[f22]) ).
fof(f24,plain,
! [X0,X1,X2] :
( happens(sK2_skl(X1,X2,X0),sK3_skl(X1,X2,X0))
| ~ startedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f25,plain,
! [X0,X1,X2] :
( less(X0,sK3_skl(X1,X2,X0))
| ~ startedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f26,plain,
! [X0,X1,X2] :
( less(sK3_skl(X1,X2,X0),X2)
| ~ startedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f27,plain,
! [X0,X1,X2] :
( initiates(sK2_skl(X1,X2,X0),X1,sK3_skl(X1,X2,X0))
| ~ startedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f28,plain,
! [X0,X1,X2,X3,X4] :
( ~ initiates(X3,X1,X4)
| ~ less(X4,X2)
| ~ less(X0,X4)
| ~ happens(X3,X4)
| startedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f29,plain,
! [Event,Time,Fluent,Fluent2,Offset] :
( holdsAt(Fluent2,plus(Time,Offset))
| stoppedIn(Time,Fluent,plus(Time,Offset))
| ~ trajectory(Fluent,Time,Fluent2,Offset)
| ~ less(n0,Offset)
| ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f30,plain,
! [Time,Fluent2,Offset] :
( holdsAt(Fluent2,plus(Time,Offset))
| ! [Fluent] :
( stoppedIn(Time,Fluent,plus(Time,Offset))
| ~ trajectory(Fluent,Time,Fluent2,Offset)
| ~ less(n0,Offset)
| ! [Event] :
( ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ) ) ),
inference(miniscoping,[status(thm)],[f29]) ).
fof(f31,plain,
! [X0,X1,X2,X3,X4] :
( holdsAt(X4,plus(X1,X3))
| stoppedIn(X1,X2,plus(X1,X3))
| ~ trajectory(X2,X1,X4,X3)
| ~ less(n0,X3)
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f32,plain,
! [Event,Time1,Fluent1,Time2,Fluent2] :
( holdsAt(Fluent2,plus(Time1,Time2))
| startedIn(Time1,Fluent1,plus(Time1,Time2))
| ~ antitrajectory(Fluent1,Time1,Fluent2,Time2)
| ~ less(n0,Time2)
| ~ terminates(Event,Fluent1,Time1)
| ~ happens(Event,Time1) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f33,plain,
! [Time1,Time2,Fluent2] :
( holdsAt(Fluent2,plus(Time1,Time2))
| ! [Fluent1] :
( startedIn(Time1,Fluent1,plus(Time1,Time2))
| ~ antitrajectory(Fluent1,Time1,Fluent2,Time2)
| ~ less(n0,Time2)
| ! [Event] :
( ~ terminates(Event,Fluent1,Time1)
| ~ happens(Event,Time1) ) ) ),
inference(miniscoping,[status(thm)],[f32]) ).
fof(f34,plain,
! [X0,X1,X2,X3,X4] :
( holdsAt(X4,plus(X1,X3))
| startedIn(X1,X2,plus(X1,X3))
| ~ antitrajectory(X2,X1,X4,X3)
| ~ less(n0,X3)
| ~ terminates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f35,plain,
! [Fluent,Time] :
( holdsAt(Fluent,plus(Time,n1))
| ? [Event] :
( terminates(Event,Fluent,Time)
& happens(Event,Time) )
| releasedAt(Fluent,plus(Time,n1))
| ~ holdsAt(Fluent,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f36,plain,
! [Fluent,Time] :
( holdsAt(Fluent,plus(Time,n1))
| ( terminates(sK4_skl(Time,Fluent),Fluent,Time)
& happens(sK4_skl(Time,Fluent),Time) )
| releasedAt(Fluent,plus(Time,n1))
| ~ holdsAt(Fluent,Time) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(Event,sK4_skl(Time,Fluent))],[f35]) ).
fof(f37,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| happens(sK4_skl(X1,X0),X1)
| releasedAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f38,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| terminates(sK4_skl(X1,X0),X0,X1)
| releasedAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f39,plain,
! [Fluent,Time] :
( ~ holdsAt(Fluent,plus(Time,n1))
| ? [Event] :
( initiates(Event,Fluent,Time)
& happens(Event,Time) )
| releasedAt(Fluent,plus(Time,n1))
| holdsAt(Fluent,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f40,plain,
! [Fluent,Time] :
( ~ holdsAt(Fluent,plus(Time,n1))
| ( initiates(sK5_skl(Time,Fluent),Fluent,Time)
& happens(sK5_skl(Time,Fluent),Time) )
| releasedAt(Fluent,plus(Time,n1))
| holdsAt(Fluent,Time) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(Event,sK5_skl(Time,Fluent))],[f39]) ).
fof(f41,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| happens(sK5_skl(X1,X0),X1)
| releasedAt(X0,plus(X1,n1))
| holdsAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f42,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| initiates(sK5_skl(X1,X0),X0,X1)
| releasedAt(X0,plus(X1,n1))
| holdsAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f43,plain,
! [Fluent,Time] :
( releasedAt(Fluent,plus(Time,n1))
| ? [Event] :
( ( terminates(Event,Fluent,Time)
| initiates(Event,Fluent,Time) )
& happens(Event,Time) )
| ~ releasedAt(Fluent,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f44,plain,
! [Fluent,Time] :
( releasedAt(Fluent,plus(Time,n1))
| ( ( terminates(sK6_skl(Time,Fluent),Fluent,Time)
| initiates(sK6_skl(Time,Fluent),Fluent,Time) )
& happens(sK6_skl(Time,Fluent),Time) )
| ~ releasedAt(Fluent,Time) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(Event,sK6_skl(Time,Fluent))],[f43]) ).
fof(f45,plain,
! [X0,X1] :
( releasedAt(X0,plus(X1,n1))
| happens(sK6_skl(X1,X0),X1)
| ~ releasedAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f46,plain,
! [X0,X1] :
( releasedAt(X0,plus(X1,n1))
| terminates(sK6_skl(X1,X0),X0,X1)
| initiates(sK6_skl(X1,X0),X0,X1)
| ~ releasedAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f47,plain,
! [Fluent,Time] :
( ~ releasedAt(Fluent,plus(Time,n1))
| ? [Event] :
( releases(Event,Fluent,Time)
& happens(Event,Time) )
| releasedAt(Fluent,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f48,plain,
! [Fluent,Time] :
( ~ releasedAt(Fluent,plus(Time,n1))
| ( releases(sK7_skl(Time,Fluent),Fluent,Time)
& happens(sK7_skl(Time,Fluent),Time) )
| releasedAt(Fluent,Time) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Event,sK7_skl(Time,Fluent))],[f47]) ).
fof(f49,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| happens(sK7_skl(X1,X0),X1)
| releasedAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f50,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releases(sK7_skl(X1,X0),X0,X1)
| releasedAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f51,plain,
! [Event,Time,Fluent] :
( holdsAt(Fluent,plus(Time,n1))
| ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f52,plain,
! [Time,Fluent] :
( holdsAt(Fluent,plus(Time,n1))
| ! [Event] :
( ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f51]) ).
fof(f53,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f54,plain,
! [Event,Time,Fluent] :
( ~ holdsAt(Fluent,plus(Time,n1))
| ~ terminates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f55,plain,
! [Time,Fluent] :
( ~ holdsAt(Fluent,plus(Time,n1))
| ! [Event] :
( ~ terminates(Event,Fluent,Time)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f54]) ).
fof(f56,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ terminates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
! [Event,Time,Fluent] :
( releasedAt(Fluent,plus(Time,n1))
| ~ releases(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f58,plain,
! [Time,Fluent] :
( releasedAt(Fluent,plus(Time,n1))
| ! [Event] :
( ~ releases(Event,Fluent,Time)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f57]) ).
fof(f59,plain,
! [X0,X1,X2] :
( releasedAt(X2,plus(X1,n1))
| ~ releases(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
! [Event,Time,Fluent] :
( ~ releasedAt(Fluent,plus(Time,n1))
| ( ~ terminates(Event,Fluent,Time)
& ~ initiates(Event,Fluent,Time) )
| ~ happens(Event,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f61,plain,
! [Time,Fluent] :
( ~ releasedAt(Fluent,plus(Time,n1))
| ! [Event] :
( ( ~ terminates(Event,Fluent,Time)
& ~ initiates(Event,Fluent,Time) )
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f60]) ).
fof(f62,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ terminates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR154+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.56 % Computer : n020.cluster.edu
% 0.11/0.56 % Model : x86_64 x86_64
% 0.11/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.56 % Memory : 8046.5625MB
% 0.11/0.56 % OS : Linux 6.8.0-71-generic
% 0.11/0.56 % CPULimit : 300
% 0.11/0.56 % WCLimit : 300
% 0.11/0.56 % DateTime : Mon Sep 21 15:14:18 UTC 2026
% 0.11/0.57 % CPUTime :
% 0.11/0.57 % Drodi V4.1.1
% 0.11/0.59 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 0.11/0.59 % SZS output start Saturation for theBenchmark
% See solution above
% 0.11/0.61 % Elapsed time: 0.032685 seconds
% 0.11/0.61 % CPU time: 0.085705 seconds
% 0.11/0.61 % Total memory used: 2.325 MB
% 0.11/0.61 % Net memory used: 2.294 MB
%------------------------------------------------------------------------------