%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR002+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:12:48 PM UTC 2026
% Result : Theorem 0.12s 0.45s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 20
% Syntax : Number of formulae : 98 ( 35 unt; 1 def)
% Number of atoms : 284 ( 83 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 310 ( 124 ~; 122 |; 53 &)
% ( 8 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 9 con; 0-2 aty)
% Number of variables : 148 ( 140 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
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(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(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(f14,axiom,
! [Event,Fluent,Time] :
( terminates(Event,Fluent,Time)
<=> ( ( Fluent = filling
& Event = overflow )
| ( Fluent = filling
& Event = tapOff ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [Event,Fluent,Time] :
( releases(Event,Fluent,Time)
<=> ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOn ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [Event,Time] :
( happens(Event,Time)
<=> ( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| ( Time = n0
& Event = tapOn ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X] : filling != waterLevel(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
plus(n1,n1) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
plus(n1,n2) = n3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
plus(n1,n3) = n4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X,Y] : plus(X,Y) = plus(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [X,Y] :
( less_or_equal(X,Y)
<=> ( X = Y
| less(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
~ ? [X] : less(X,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [X] :
( less(X,n2)
<=> less_or_equal(X,n1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [X] :
( less(X,n3)
<=> less_or_equal(X,n2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,hypothesis,
~ releasedAt(filling,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,lemma,
holdsAt(waterLevel(n3),n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,conjecture,
~ holdsAt(filling,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,negated_conjecture,
~ ~ holdsAt(filling,n4),
inference(negated_conjecture,[status(cth)],[f56]) ).
fof(f84,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(f85,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))],[f84]) ).
fof(f86,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)],[f85]) ).
fof(f92,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(f93,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))],[f92]) ).
fof(f95,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releases(sK7_skl(X1,X0),X0,X1)
| releasedAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f99,plain,
! [Event,Time,Fluent] :
( ~ holdsAt(Fluent,plus(Time,n1))
| ~ terminates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f100,plain,
! [Time,Fluent] :
( ~ holdsAt(Fluent,plus(Time,n1))
| ! [Event] :
( ~ terminates(Event,Fluent,Time)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f99]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ terminates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f119,plain,
! [Event,Fluent,Time] :
( ( ( ( Fluent != filling
| Event != overflow )
& ( Fluent != filling
| Event != tapOff ) )
| terminates(Event,Fluent,Time) )
& ( ( Fluent = filling
& Event = overflow )
| ( Fluent = filling
& Event = tapOff )
| ~ terminates(Event,Fluent,Time) ) ),
inference(NNF_transformation,[status(thm)],[f14]) ).
fof(f120,plain,
( ! [Event,Fluent] :
( ( ( Fluent != filling
| Event != overflow )
& ( Fluent != filling
| Event != tapOff ) )
| ! [Time] : terminates(Event,Fluent,Time) )
& ! [Event,Fluent] :
( ( Fluent = filling
& Event = overflow )
| ( Fluent = filling
& Event = tapOff )
| ! [Time] : ~ terminates(Event,Fluent,Time) ) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f126,plain,
! [X0,X1,X2] :
( X1 != filling
| X0 != overflow
| terminates(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f127,plain,
! [Event,Fluent,Time] :
( ( ! [Height] :
( Fluent != waterLevel(Height)
| Event != tapOn )
| releases(Event,Fluent,Time) )
& ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOn )
| ~ releases(Event,Fluent,Time) ) ),
inference(NNF_transformation,[status(thm)],[f15]) ).
fof(f128,plain,
( ! [Event,Fluent] :
( ! [Height] : Fluent != waterLevel(Height)
| Event != tapOn
| ! [Time] : releases(Event,Fluent,Time) )
& ! [Event,Fluent] :
( ( ? [Height] : Fluent = waterLevel(Height)
& Event = tapOn )
| ! [Time] : ~ releases(Event,Fluent,Time) ) ),
inference(miniscoping,[status(thm)],[f127]) ).
fof(f129,plain,
( ! [Event,Fluent] :
( ! [Height] : Fluent != waterLevel(Height)
| Event != tapOn
| ! [Time] : releases(Event,Fluent,Time) )
& ! [Event,Fluent] :
( ( Fluent = waterLevel(sK9_skl(Fluent,Event))
& Event = tapOn )
| ! [Time] : ~ releases(Event,Fluent,Time) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(Height,sK9_skl(Fluent,Event))],[f128]) ).
fof(f131,plain,
! [X0,X1,X2] :
( X1 = waterLevel(sK9_skl(X1,X0))
| ~ releases(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f133,definition,
! [Event,Time] :
( sP1_prd(Time,Event)
<=> ( Time = n0
& Event = tapOn ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f134,plain,
! [Event,Time] :
( happens(Event,Time)
<=> ( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| sP1_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f16,f133]) ).
fof(f135,plain,
! [Event,Time] :
( ( ( ( Event != overflow
| ~ holdsAt(filling,Time)
| ~ holdsAt(waterLevel(n3),Time) )
& ~ sP1_prd(Time,Event) )
| happens(Event,Time) )
& ( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| sP1_prd(Time,Event)
| ~ happens(Event,Time) ) ),
inference(NNF_transformation,[status(thm)],[f134]) ).
fof(f136,plain,
( ! [Event,Time] :
( ( ( Event != overflow
| ~ holdsAt(filling,Time)
| ~ holdsAt(waterLevel(n3),Time) )
& ~ sP1_prd(Time,Event) )
| happens(Event,Time) )
& ! [Event,Time] :
( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| sP1_prd(Time,Event)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f135]) ).
fof(f138,plain,
! [X0,X1] :
( holdsAt(filling,X1)
| sP1_prd(X1,X0)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f141,plain,
! [X0,X1] :
( X0 != overflow
| ~ holdsAt(filling,X1)
| ~ holdsAt(waterLevel(n3),X1)
| happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f151,plain,
! [X0] : filling != waterLevel(X0),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f159,plain,
plus(n0,n1) = n1,
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f162,plain,
plus(n1,n1) = n2,
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f163,plain,
plus(n1,n2) = n3,
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f164,plain,
plus(n1,n3) = n4,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f168,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f169,plain,
! [X,Y] :
( ( ( X != Y
& ~ less(X,Y) )
| less_or_equal(X,Y) )
& ( X = Y
| less(X,Y)
| ~ less_or_equal(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f37]) ).
fof(f170,plain,
( ! [X,Y] :
( ( X != Y
& ~ less(X,Y) )
| less_or_equal(X,Y) )
& ! [X,Y] :
( X = Y
| less(X,Y)
| ~ less_or_equal(X,Y) ) ),
inference(miniscoping,[status(thm)],[f169]) ).
fof(f172,plain,
! [X0,X1] :
( ~ less(X0,X1)
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f173,plain,
! [X0,X1] :
( X0 != X1
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f174,plain,
! [X] : ~ less(X,n0),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f175,plain,
! [X0] : ~ less(X0,n0),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f180,plain,
! [X] :
( ( ~ less_or_equal(X,n1)
| less(X,n2) )
& ( less_or_equal(X,n1)
| ~ less(X,n2) ) ),
inference(NNF_transformation,[status(thm)],[f40]) ).
fof(f181,plain,
( ! [X] :
( ~ less_or_equal(X,n1)
| less(X,n2) )
& ! [X] :
( less_or_equal(X,n1)
| ~ less(X,n2) ) ),
inference(miniscoping,[status(thm)],[f180]) ).
fof(f183,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f184,plain,
! [X] :
( ( ~ less_or_equal(X,n2)
| less(X,n3) )
& ( less_or_equal(X,n2)
| ~ less(X,n3) ) ),
inference(NNF_transformation,[status(thm)],[f41]) ).
fof(f185,plain,
( ! [X] :
( ~ less_or_equal(X,n2)
| less(X,n3) )
& ! [X] :
( less_or_equal(X,n2)
| ~ less(X,n3) ) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f187,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f221,plain,
~ releasedAt(filling,n0),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f223,plain,
holdsAt(waterLevel(n3),n3),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f224,plain,
holdsAt(filling,n4),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f235,plain,
! [Event,Time] :
( ( Time != n0
| Event != tapOn
| sP1_prd(Time,Event) )
& ( ( Time = n0
& Event = tapOn )
| ~ sP1_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f133]) ).
fof(f236,plain,
( ! [Event,Time] :
( Time != n0
| Event != tapOn
| sP1_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = tapOn )
| ~ sP1_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f235]) ).
fof(f238,plain,
! [X0,X1] :
( X0 = n0
| ~ sP1_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f251,plain,
! [X0] : terminates(overflow,filling,X0),
inference(destructive_equality_resolution,[status(thm)],[f126]) ).
fof(f253,plain,
! [X0] :
( ~ holdsAt(filling,X0)
| ~ holdsAt(waterLevel(n3),X0)
| happens(overflow,X0) ),
inference(destructive_equality_resolution,[status(thm)],[f141]) ).
fof(f255,plain,
! [X0] : less_or_equal(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f173]) ).
fof(f399,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(n1,X1))
| ~ terminates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(paramodulation,[status(thm)],[f168,f101]) ).
fof(f437,plain,
less(n1,n2),
inference(resolution,[status(thm)],[f183,f255]) ).
fof(f441,plain,
! [X0] :
( ~ less(X0,n2)
| less(X0,n3) ),
inference(resolution,[status(thm)],[f187,f172]) ).
fof(f532,plain,
! [X0,X1] : ~ releases(X0,filling,X1),
inference(resolution,[status(thm)],[f131,f151]) ).
fof(f535,plain,
! [X0] :
( ~ releasedAt(filling,plus(X0,n1))
| releasedAt(filling,X0) ),
inference(resolution,[status(thm)],[f532,f95]) ).
fof(f557,plain,
! [X0,X1] :
( X1 = n0
| holdsAt(filling,X1)
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f138,f238]) ).
fof(f568,plain,
! [X0] :
( ~ holdsAt(filling,plus(X0,n1))
| happens(sK5_skl(X0,filling),X0)
| holdsAt(filling,X0)
| releasedAt(filling,X0) ),
inference(resolution,[status(thm)],[f535,f86]) ).
fof(f570,plain,
( ~ releasedAt(filling,n1)
| releasedAt(filling,n0) ),
inference(paramodulation,[status(thm)],[f159,f535]) ).
fof(f571,plain,
( ~ releasedAt(filling,n2)
| releasedAt(filling,n1) ),
inference(paramodulation,[status(thm)],[f162,f535]) ).
fof(f572,plain,
! [X0] :
( ~ releasedAt(filling,plus(n1,X0))
| releasedAt(filling,X0) ),
inference(paramodulation,[status(thm)],[f168,f535]) ).
fof(f574,plain,
~ releasedAt(filling,n1),
inference(forward_subsumption_resolution,[status(thm)],[f570,f221]) ).
fof(f575,plain,
~ releasedAt(filling,n2),
inference(forward_subsumption_resolution,[status(thm)],[f571,f574]) ).
fof(f582,plain,
( ~ releasedAt(filling,n3)
| releasedAt(filling,n2) ),
inference(paramodulation,[status(thm)],[f163,f572]) ).
fof(f591,plain,
~ releasedAt(filling,n3),
inference(forward_subsumption_resolution,[status(thm)],[f582,f575]) ).
fof(f593,plain,
less(n1,n3),
inference(resolution,[status(thm)],[f441,f437]) ).
fof(f616,plain,
( ~ holdsAt(filling,n3)
| happens(overflow,n3) ),
inference(resolution,[status(thm)],[f253,f223]) ).
fof(f1069,plain,
! [X0] :
( ~ holdsAt(filling,plus(X0,n1))
| holdsAt(filling,X0)
| releasedAt(filling,X0)
| X0 = n0
| holdsAt(filling,X0) ),
inference(resolution,[status(thm)],[f557,f568]) ).
fof(f1074,plain,
! [X0] :
( ~ holdsAt(filling,plus(X0,n1))
| releasedAt(filling,X0)
| X0 = n0
| holdsAt(filling,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1069]) ).
fof(f1110,plain,
! [X0] :
( ~ holdsAt(filling,plus(n1,X0))
| releasedAt(filling,X0)
| X0 = n0
| holdsAt(filling,X0) ),
inference(paramodulation,[status(thm)],[f168,f1074]) ).
fof(f1116,plain,
( ~ holdsAt(filling,n4)
| releasedAt(filling,n3)
| n3 = n0
| holdsAt(filling,n3) ),
inference(paramodulation,[status(thm)],[f164,f1110]) ).
fof(f1120,plain,
( ~ holdsAt(filling,n4)
| n3 = n0
| holdsAt(filling,n3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1116,f591]) ).
fof(f1122,plain,
( n3 = n0
| holdsAt(filling,n3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1120,f224]) ).
fof(f2406,plain,
! [X0,X1] :
( ~ holdsAt(X1,n4)
| ~ terminates(X0,X1,n3)
| ~ happens(X0,n3) ),
inference(paramodulation,[status(thm)],[f164,f399]) ).
fof(f2432,plain,
( ~ holdsAt(filling,n4)
| ~ happens(overflow,n3) ),
inference(resolution,[status(thm)],[f2406,f251]) ).
fof(f2435,plain,
~ happens(overflow,n3),
inference(forward_subsumption_resolution,[status(thm)],[f2432,f224]) ).
fof(f2437,plain,
~ holdsAt(filling,n3),
inference(backward_subsumption_resolution,[status(thm)],[f616,f2435]) ).
fof(f2449,plain,
n3 = n0,
inference(backward_subsumption_resolution,[status(thm)],[f1122,f2437]) ).
fof(f2524,plain,
less(n1,n0),
inference(backward_demodulation,[status(thm)],[f2449,f593]) ).
fof(f2650,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2524,f175]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR002+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n005.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 14:23:04 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.12/0.45 % Refutation found
% 0.12/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.47 % Elapsed time: 0.117888 seconds
% 0.12/0.47 % CPU time: 0.628891 seconds
% 0.12/0.47 % Total memory used: 117.007 MB
% 0.12/0.47 % Net memory used: 115.927 MB
%------------------------------------------------------------------------------