%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : CSR004+1 : TPTP v5.0.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art04.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Tue Dec 28 22:44:08 EST 2010
% Result : Theorem 8.84s
% Output : Solution 8.84s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP22163/CSR004+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP22163/CSR004+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP22163/CSR004+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 22259
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.94 CPU 2.02 WC
% PrfWatch: 3.93 CPU 4.03 WC
% PrfWatch: 5.92 CPU 6.03 WC
% # Preprocessing time : 0.019 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,holdsAt(waterLevel(n0),n0),file('/tmp/SRASS.s.p', waterLevel_0)).
% fof(7, axiom,![X2]:![X3]:(happens(X2,X3)<=>((X2=tapOn&X3=n0)|((holdsAt(waterLevel(n3),X3)&holdsAt(filling,X3))&X2=overflow))),file('/tmp/SRASS.s.p', happens_all_defn)).
% fof(9, axiom,![X4]:~(filling=waterLevel(X4)),file('/tmp/SRASS.s.p', filling_not_waterLevel)).
% fof(10, axiom,![X4]:~(spilling=waterLevel(X4)),file('/tmp/SRASS.s.p', spilling_not_waterLevel)).
% fof(11, axiom,![X3]:![X5]:![X6]:((holdsAt(waterLevel(X5),X3)&holdsAt(waterLevel(X6),X3))=>X5=X6),file('/tmp/SRASS.s.p', same_waterLevel)).
% fof(12, axiom,![X4]:![X7]:(waterLevel(X4)=waterLevel(X7)<=>X4=X7),file('/tmp/SRASS.s.p', distinct_waterLevels)).
% fof(13, axiom,plus(n0,n3)=n3,file('/tmp/SRASS.s.p', plus0_3)).
% fof(14, axiom,![X2]:![X8]:![X3]:(initiates(X2,X8,X3)<=>((((X2=tapOn&X8=filling)|(X2=overflow&X8=spilling))|?[X1]:((holdsAt(waterLevel(X1),X3)&X2=tapOff)&X8=waterLevel(X1)))|?[X1]:((holdsAt(waterLevel(X1),X3)&X2=overflow)&X8=waterLevel(X1)))),file('/tmp/SRASS.s.p', initiates_all_defn)).
% fof(15, axiom,![X5]:![X3]:![X6]:![X9]:((holdsAt(waterLevel(X5),X3)&X6=plus(X5,X9))=>trajectory(filling,X3,waterLevel(X6),X9)),file('/tmp/SRASS.s.p', change_of_waterLevel)).
% fof(16, axiom,~(?[X4]:less(X4,n0)),file('/tmp/SRASS.s.p', less0)).
% fof(17, axiom,![X8]:![X3]:(((holdsAt(X8,X3)&~(releasedAt(X8,plus(X3,n1))))&~(?[X2]:(happens(X2,X3)&terminates(X2,X8,X3))))=>holdsAt(X8,plus(X3,n1))),file('/tmp/SRASS.s.p', keep_holding)).
% fof(19, axiom,~(overflow=tapOn),file('/tmp/SRASS.s.p', overflow_not_tapOn)).
% fof(20, axiom,![X4]:![X7]:plus(X4,X7)=plus(X7,X4),file('/tmp/SRASS.s.p', symmetry_of_plus)).
% fof(21, axiom,![X2]:![X8]:![X3]:(terminates(X2,X8,X3)<=>((X2=tapOff&X8=filling)|(X2=overflow&X8=filling))),file('/tmp/SRASS.s.p', terminates_all_defn)).
% fof(22, axiom,![X8]:![X3]:((~(releasedAt(X8,X3))&~(?[X2]:(happens(X2,X3)&releases(X2,X8,X3))))=>~(releasedAt(X8,plus(X3,n1)))),file('/tmp/SRASS.s.p', keep_not_released)).
% fof(23, axiom,![X2]:![X3]:![X8]:((happens(X2,X3)&initiates(X2,X8,X3))=>holdsAt(X8,plus(X3,n1))),file('/tmp/SRASS.s.p', happens_holds)).
% fof(27, axiom,![X2]:![X3]:![X8]:((happens(X2,X3)&(initiates(X2,X8,X3)|terminates(X2,X8,X3)))=>~(releasedAt(X8,plus(X3,n1)))),file('/tmp/SRASS.s.p', happens_not_released)).
% fof(28, axiom,![X2]:![X3]:![X8]:![X10]:![X9]:(((((happens(X2,X3)&initiates(X2,X8,X3))&less(n0,X9))&trajectory(X8,X3,X10,X9))&~(stoppedIn(X3,X8,plus(X3,X9))))=>holdsAt(X10,plus(X3,X9))),file('/tmp/SRASS.s.p', change_holding)).
% fof(30, axiom,plus(n0,n1)=n1,file('/tmp/SRASS.s.p', plus0_1)).
% fof(31, axiom,![X2]:![X8]:![X3]:(releases(X2,X8,X3)<=>?[X1]:(X2=tapOn&X8=waterLevel(X1))),file('/tmp/SRASS.s.p', releases_all_defn)).
% fof(33, axiom,plus(n0,n2)=n2,file('/tmp/SRASS.s.p', plus0_2)).
% fof(35, axiom,~(tapOff=tapOn),file('/tmp/SRASS.s.p', tapOff_not_tapOn)).
% fof(36, axiom,~(tapOff=overflow),file('/tmp/SRASS.s.p', tapOff_not_overflow)).
% fof(37, axiom,![X4]:![X7]:(less(X4,X7)<=>(~(less(X7,X4))&~(X7=X4))),file('/tmp/SRASS.s.p', less_property)).
% fof(38, axiom,plus(n1,n2)=n3,file('/tmp/SRASS.s.p', plus1_2)).
% fof(40, axiom,![X11]:![X8]:![X13]:(stoppedIn(X11,X8,X13)<=>?[X2]:?[X3]:(((happens(X2,X3)&less(X11,X3))&less(X3,X13))&terminates(X2,X8,X3))),file('/tmp/SRASS.s.p', stoppedin_defn)).
% fof(43, axiom,![X4]:(less(X4,n1)<=>less_or_equal(X4,n0)),file('/tmp/SRASS.s.p', less1)).
% fof(44, axiom,plus(n1,n1)=n2,file('/tmp/SRASS.s.p', plus1_1)).
% fof(46, axiom,![X4]:![X7]:(less_or_equal(X4,X7)<=>(less(X4,X7)|X4=X7)),file('/tmp/SRASS.s.p', less_or_equal)).
% fof(47, axiom,![X4]:(less(X4,n3)<=>less_or_equal(X4,n2)),file('/tmp/SRASS.s.p', less3)).
% fof(49, axiom,![X4]:(less(X4,n2)<=>less_or_equal(X4,n1)),file('/tmp/SRASS.s.p', less2)).
% fof(55, conjecture,happens(overflow,n3),file('/tmp/SRASS.s.p', overflow_3)).
% fof(56, negated_conjecture,~(happens(overflow,n3)),inference(assume_negation,[status(cth)],[55])).
% fof(62, plain,![X8]:![X3]:(((holdsAt(X8,X3)&~(releasedAt(X8,plus(X3,n1))))&~(?[X2]:(happens(X2,X3)&terminates(X2,X8,X3))))=>holdsAt(X8,plus(X3,n1))),inference(fof_simplification,[status(thm)],[17,theory(equality)])).
% fof(64, plain,![X8]:![X3]:((~(releasedAt(X8,X3))&~(?[X2]:(happens(X2,X3)&releases(X2,X8,X3))))=>~(releasedAt(X8,plus(X3,n1)))),inference(fof_simplification,[status(thm)],[22,theory(equality)])).
% fof(66, plain,![X2]:![X3]:![X8]:((happens(X2,X3)&(initiates(X2,X8,X3)|terminates(X2,X8,X3)))=>~(releasedAt(X8,plus(X3,n1)))),inference(fof_simplification,[status(thm)],[27,theory(equality)])).
% fof(67, plain,![X2]:![X3]:![X8]:![X10]:![X9]:(((((happens(X2,X3)&initiates(X2,X8,X3))&less(n0,X9))&trajectory(X8,X3,X10,X9))&~(stoppedIn(X3,X8,plus(X3,X9))))=>holdsAt(X10,plus(X3,X9))),inference(fof_simplification,[status(thm)],[28,theory(equality)])).
% fof(69, plain,![X4]:![X7]:(less(X4,X7)<=>(~(less(X7,X4))&~(X7=X4))),inference(fof_simplification,[status(thm)],[37,theory(equality)])).
% fof(70, negated_conjecture,~(happens(overflow,n3)),inference(fof_simplification,[status(thm)],[56,theory(equality)])).
% fof(71, plain,![X2]:![X3]:![X8]:(epred1_3(X8,X3,X2)<=>((((X2=tapOn&X8=filling)|(X2=overflow&X8=spilling))|?[X1]:((holdsAt(waterLevel(X1),X3)&X2=tapOff)&X8=waterLevel(X1)))|?[X1]:((holdsAt(waterLevel(X1),X3)&X2=overflow)&X8=waterLevel(X1)))),introduced(definition)).
% fof(72, plain,![X2]:![X8]:![X3]:(initiates(X2,X8,X3)<=>epred1_3(X8,X3,X2)),inference(apply_def,[status(esa)],[14,71,theory(equality)])).
% cnf(73,plain,(holdsAt(waterLevel(n0),n0)),inference(split_conjunct,[status(thm)],[1])).
% fof(80, plain,![X2]:![X3]:((~(happens(X2,X3))|((X2=tapOn&X3=n0)|((holdsAt(waterLevel(n3),X3)&holdsAt(filling,X3))&X2=overflow)))&(((~(X2=tapOn)|~(X3=n0))&((~(holdsAt(waterLevel(n3),X3))|~(holdsAt(filling,X3)))|~(X2=overflow)))|happens(X2,X3))),inference(fof_nnf,[status(thm)],[7])).
% fof(81, plain,![X4]:![X5]:((~(happens(X4,X5))|((X4=tapOn&X5=n0)|((holdsAt(waterLevel(n3),X5)&holdsAt(filling,X5))&X4=overflow)))&(((~(X4=tapOn)|~(X5=n0))&((~(holdsAt(waterLevel(n3),X5))|~(holdsAt(filling,X5)))|~(X4=overflow)))|happens(X4,X5))),inference(variable_rename,[status(thm)],[80])).
% fof(82, plain,![X4]:![X5]:((((((holdsAt(waterLevel(n3),X5)|X4=tapOn)|~(happens(X4,X5)))&((holdsAt(filling,X5)|X4=tapOn)|~(happens(X4,X5))))&((X4=overflow|X4=tapOn)|~(happens(X4,X5))))&((((holdsAt(waterLevel(n3),X5)|X5=n0)|~(happens(X4,X5)))&((holdsAt(filling,X5)|X5=n0)|~(happens(X4,X5))))&((X4=overflow|X5=n0)|~(happens(X4,X5)))))&(((~(X4=tapOn)|~(X5=n0))|happens(X4,X5))&(((~(holdsAt(waterLevel(n3),X5))|~(holdsAt(filling,X5)))|~(X4=overflow))|happens(X4,X5)))),inference(distribute,[status(thm)],[81])).
% cnf(83,plain,(happens(X1,X2)|X1!=overflow|~holdsAt(filling,X2)|~holdsAt(waterLevel(n3),X2)),inference(split_conjunct,[status(thm)],[82])).
% cnf(84,plain,(happens(X1,X2)|X2!=n0|X1!=tapOn),inference(split_conjunct,[status(thm)],[82])).
% cnf(88,plain,(X1=tapOn|X1=overflow|~happens(X1,X2)),inference(split_conjunct,[status(thm)],[82])).
% cnf(90,plain,(X1=tapOn|holdsAt(waterLevel(n3),X2)|~happens(X1,X2)),inference(split_conjunct,[status(thm)],[82])).
% fof(92, plain,![X5]:~(filling=waterLevel(X5)),inference(variable_rename,[status(thm)],[9])).
% cnf(93,plain,(filling!=waterLevel(X1)),inference(split_conjunct,[status(thm)],[92])).
% fof(94, plain,![X5]:~(spilling=waterLevel(X5)),inference(variable_rename,[status(thm)],[10])).
% cnf(95,plain,(spilling!=waterLevel(X1)),inference(split_conjunct,[status(thm)],[94])).
% fof(96, plain,![X3]:![X5]:![X6]:((~(holdsAt(waterLevel(X5),X3))|~(holdsAt(waterLevel(X6),X3)))|X5=X6),inference(fof_nnf,[status(thm)],[11])).
% fof(97, plain,![X7]:![X8]:![X9]:((~(holdsAt(waterLevel(X8),X7))|~(holdsAt(waterLevel(X9),X7)))|X8=X9),inference(variable_rename,[status(thm)],[96])).
% cnf(98,plain,(X1=X2|~holdsAt(waterLevel(X2),X3)|~holdsAt(waterLevel(X1),X3)),inference(split_conjunct,[status(thm)],[97])).
% fof(99, plain,![X4]:![X7]:((~(waterLevel(X4)=waterLevel(X7))|X4=X7)&(~(X4=X7)|waterLevel(X4)=waterLevel(X7))),inference(fof_nnf,[status(thm)],[12])).
% fof(100, plain,![X8]:![X9]:((~(waterLevel(X8)=waterLevel(X9))|X8=X9)&(~(X8=X9)|waterLevel(X8)=waterLevel(X9))),inference(variable_rename,[status(thm)],[99])).
% cnf(102,plain,(X1=X2|waterLevel(X1)!=waterLevel(X2)),inference(split_conjunct,[status(thm)],[100])).
% cnf(103,plain,(plus(n0,n3)=n3),inference(split_conjunct,[status(thm)],[13])).
% fof(104, plain,![X2]:![X8]:![X3]:((~(initiates(X2,X8,X3))|epred1_3(X8,X3,X2))&(~(epred1_3(X8,X3,X2))|initiates(X2,X8,X3))),inference(fof_nnf,[status(thm)],[72])).
% fof(105, plain,![X9]:![X10]:![X11]:((~(initiates(X9,X10,X11))|epred1_3(X10,X11,X9))&(~(epred1_3(X10,X11,X9))|initiates(X9,X10,X11))),inference(variable_rename,[status(thm)],[104])).
% cnf(106,plain,(initiates(X1,X2,X3)|~epred1_3(X2,X3,X1)),inference(split_conjunct,[status(thm)],[105])).
% cnf(107,plain,(epred1_3(X1,X2,X3)|~initiates(X3,X1,X2)),inference(split_conjunct,[status(thm)],[105])).
% fof(108, plain,![X5]:![X3]:![X6]:![X9]:((~(holdsAt(waterLevel(X5),X3))|~(X6=plus(X5,X9)))|trajectory(filling,X3,waterLevel(X6),X9)),inference(fof_nnf,[status(thm)],[15])).
% fof(109, plain,![X10]:![X11]:![X12]:![X13]:((~(holdsAt(waterLevel(X10),X11))|~(X12=plus(X10,X13)))|trajectory(filling,X11,waterLevel(X12),X13)),inference(variable_rename,[status(thm)],[108])).
% cnf(110,plain,(trajectory(filling,X1,waterLevel(X2),X3)|X2!=plus(X4,X3)|~holdsAt(waterLevel(X4),X1)),inference(split_conjunct,[status(thm)],[109])).
% fof(111, plain,![X4]:~(less(X4,n0)),inference(fof_nnf,[status(thm)],[16])).
% fof(112, plain,![X5]:~(less(X5,n0)),inference(variable_rename,[status(thm)],[111])).
% cnf(113,plain,(~less(X1,n0)),inference(split_conjunct,[status(thm)],[112])).
% fof(114, plain,![X8]:![X3]:(((~(holdsAt(X8,X3))|releasedAt(X8,plus(X3,n1)))|?[X2]:(happens(X2,X3)&terminates(X2,X8,X3)))|holdsAt(X8,plus(X3,n1))),inference(fof_nnf,[status(thm)],[62])).
% fof(115, plain,![X9]:![X10]:(((~(holdsAt(X9,X10))|releasedAt(X9,plus(X10,n1)))|?[X11]:(happens(X11,X10)&terminates(X11,X9,X10)))|holdsAt(X9,plus(X10,n1))),inference(variable_rename,[status(thm)],[114])).
% fof(116, plain,![X9]:![X10]:(((~(holdsAt(X9,X10))|releasedAt(X9,plus(X10,n1)))|(happens(esk1_2(X9,X10),X10)&terminates(esk1_2(X9,X10),X9,X10)))|holdsAt(X9,plus(X10,n1))),inference(skolemize,[status(esa)],[115])).
% fof(117, plain,![X9]:![X10]:(((happens(esk1_2(X9,X10),X10)|(~(holdsAt(X9,X10))|releasedAt(X9,plus(X10,n1))))|holdsAt(X9,plus(X10,n1)))&((terminates(esk1_2(X9,X10),X9,X10)|(~(holdsAt(X9,X10))|releasedAt(X9,plus(X10,n1))))|holdsAt(X9,plus(X10,n1)))),inference(distribute,[status(thm)],[116])).
% cnf(118,plain,(holdsAt(X1,plus(X2,n1))|releasedAt(X1,plus(X2,n1))|terminates(esk1_2(X1,X2),X1,X2)|~holdsAt(X1,X2)),inference(split_conjunct,[status(thm)],[117])).
% cnf(119,plain,(holdsAt(X1,plus(X2,n1))|releasedAt(X1,plus(X2,n1))|happens(esk1_2(X1,X2),X2)|~holdsAt(X1,X2)),inference(split_conjunct,[status(thm)],[117])).
% cnf(126,plain,(overflow!=tapOn),inference(split_conjunct,[status(thm)],[19])).
% fof(127, plain,![X8]:![X9]:plus(X8,X9)=plus(X9,X8),inference(variable_rename,[status(thm)],[20])).
% cnf(128,plain,(plus(X1,X2)=plus(X2,X1)),inference(split_conjunct,[status(thm)],[127])).
% fof(129, plain,![X2]:![X8]:![X3]:((~(terminates(X2,X8,X3))|((X2=tapOff&X8=filling)|(X2=overflow&X8=filling)))&(((~(X2=tapOff)|~(X8=filling))&(~(X2=overflow)|~(X8=filling)))|terminates(X2,X8,X3))),inference(fof_nnf,[status(thm)],[21])).
% fof(130, plain,![X9]:![X10]:![X11]:((~(terminates(X9,X10,X11))|((X9=tapOff&X10=filling)|(X9=overflow&X10=filling)))&(((~(X9=tapOff)|~(X10=filling))&(~(X9=overflow)|~(X10=filling)))|terminates(X9,X10,X11))),inference(variable_rename,[status(thm)],[129])).
% fof(131, plain,![X9]:![X10]:![X11]:(((((X9=overflow|X9=tapOff)|~(terminates(X9,X10,X11)))&((X10=filling|X9=tapOff)|~(terminates(X9,X10,X11))))&(((X9=overflow|X10=filling)|~(terminates(X9,X10,X11)))&((X10=filling|X10=filling)|~(terminates(X9,X10,X11)))))&(((~(X9=tapOff)|~(X10=filling))|terminates(X9,X10,X11))&((~(X9=overflow)|~(X10=filling))|terminates(X9,X10,X11)))),inference(distribute,[status(thm)],[130])).
% cnf(137,plain,(X1=tapOff|X1=overflow|~terminates(X1,X2,X3)),inference(split_conjunct,[status(thm)],[131])).
% fof(138, plain,![X8]:![X3]:((releasedAt(X8,X3)|?[X2]:(happens(X2,X3)&releases(X2,X8,X3)))|~(releasedAt(X8,plus(X3,n1)))),inference(fof_nnf,[status(thm)],[64])).
% fof(139, plain,![X9]:![X10]:((releasedAt(X9,X10)|?[X11]:(happens(X11,X10)&releases(X11,X9,X10)))|~(releasedAt(X9,plus(X10,n1)))),inference(variable_rename,[status(thm)],[138])).
% fof(140, plain,![X9]:![X10]:((releasedAt(X9,X10)|(happens(esk3_2(X9,X10),X10)&releases(esk3_2(X9,X10),X9,X10)))|~(releasedAt(X9,plus(X10,n1)))),inference(skolemize,[status(esa)],[139])).
% fof(141, plain,![X9]:![X10]:(((happens(esk3_2(X9,X10),X10)|releasedAt(X9,X10))|~(releasedAt(X9,plus(X10,n1))))&((releases(esk3_2(X9,X10),X9,X10)|releasedAt(X9,X10))|~(releasedAt(X9,plus(X10,n1))))),inference(distribute,[status(thm)],[140])).
% cnf(142,plain,(releasedAt(X1,X2)|releases(esk3_2(X1,X2),X1,X2)|~releasedAt(X1,plus(X2,n1))),inference(split_conjunct,[status(thm)],[141])).
% fof(144, plain,![X2]:![X3]:![X8]:((~(happens(X2,X3))|~(initiates(X2,X8,X3)))|holdsAt(X8,plus(X3,n1))),inference(fof_nnf,[status(thm)],[23])).
% fof(145, plain,![X9]:![X10]:![X11]:((~(happens(X9,X10))|~(initiates(X9,X11,X10)))|holdsAt(X11,plus(X10,n1))),inference(variable_rename,[status(thm)],[144])).
% cnf(146,plain,(holdsAt(X1,plus(X2,n1))|~initiates(X3,X1,X2)|~happens(X3,X2)),inference(split_conjunct,[status(thm)],[145])).
% fof(159, plain,![X2]:![X3]:![X8]:((~(happens(X2,X3))|(~(initiates(X2,X8,X3))&~(terminates(X2,X8,X3))))|~(releasedAt(X8,plus(X3,n1)))),inference(fof_nnf,[status(thm)],[66])).
% fof(160, plain,![X9]:![X10]:![X11]:((~(happens(X9,X10))|(~(initiates(X9,X11,X10))&~(terminates(X9,X11,X10))))|~(releasedAt(X11,plus(X10,n1)))),inference(variable_rename,[status(thm)],[159])).
% fof(161, plain,![X9]:![X10]:![X11]:(((~(initiates(X9,X11,X10))|~(happens(X9,X10)))|~(releasedAt(X11,plus(X10,n1))))&((~(terminates(X9,X11,X10))|~(happens(X9,X10)))|~(releasedAt(X11,plus(X10,n1))))),inference(distribute,[status(thm)],[160])).
% cnf(163,plain,(~releasedAt(X1,plus(X2,n1))|~happens(X3,X2)|~initiates(X3,X1,X2)),inference(split_conjunct,[status(thm)],[161])).
% fof(164, plain,![X2]:![X3]:![X8]:![X10]:![X9]:(((((~(happens(X2,X3))|~(initiates(X2,X8,X3)))|~(less(n0,X9)))|~(trajectory(X8,X3,X10,X9)))|stoppedIn(X3,X8,plus(X3,X9)))|holdsAt(X10,plus(X3,X9))),inference(fof_nnf,[status(thm)],[67])).
% fof(165, plain,![X11]:![X12]:![X13]:![X14]:![X15]:(((((~(happens(X11,X12))|~(initiates(X11,X13,X12)))|~(less(n0,X15)))|~(trajectory(X13,X12,X14,X15)))|stoppedIn(X12,X13,plus(X12,X15)))|holdsAt(X14,plus(X12,X15))),inference(variable_rename,[status(thm)],[164])).
% cnf(166,plain,(holdsAt(X1,plus(X2,X3))|stoppedIn(X2,X4,plus(X2,X3))|~trajectory(X4,X2,X1,X3)|~less(n0,X3)|~initiates(X5,X4,X2)|~happens(X5,X2)),inference(split_conjunct,[status(thm)],[165])).
% cnf(170,plain,(plus(n0,n1)=n1),inference(split_conjunct,[status(thm)],[30])).
% fof(171, plain,![X2]:![X8]:![X3]:((~(releases(X2,X8,X3))|?[X1]:(X2=tapOn&X8=waterLevel(X1)))&(![X1]:(~(X2=tapOn)|~(X8=waterLevel(X1)))|releases(X2,X8,X3))),inference(fof_nnf,[status(thm)],[31])).
% fof(172, plain,![X9]:![X10]:![X11]:((~(releases(X9,X10,X11))|?[X12]:(X9=tapOn&X10=waterLevel(X12)))&(![X13]:(~(X9=tapOn)|~(X10=waterLevel(X13)))|releases(X9,X10,X11))),inference(variable_rename,[status(thm)],[171])).
% fof(173, plain,![X9]:![X10]:![X11]:((~(releases(X9,X10,X11))|(X9=tapOn&X10=waterLevel(esk5_3(X9,X10,X11))))&(![X13]:(~(X9=tapOn)|~(X10=waterLevel(X13)))|releases(X9,X10,X11))),inference(skolemize,[status(esa)],[172])).
% fof(174, plain,![X9]:![X10]:![X11]:![X13]:(((~(X9=tapOn)|~(X10=waterLevel(X13)))|releases(X9,X10,X11))&(~(releases(X9,X10,X11))|(X9=tapOn&X10=waterLevel(esk5_3(X9,X10,X11))))),inference(shift_quantors,[status(thm)],[173])).
% fof(175, plain,![X9]:![X10]:![X11]:![X13]:(((~(X9=tapOn)|~(X10=waterLevel(X13)))|releases(X9,X10,X11))&((X9=tapOn|~(releases(X9,X10,X11)))&(X10=waterLevel(esk5_3(X9,X10,X11))|~(releases(X9,X10,X11))))),inference(distribute,[status(thm)],[174])).
% cnf(176,plain,(X2=waterLevel(esk5_3(X1,X2,X3))|~releases(X1,X2,X3)),inference(split_conjunct,[status(thm)],[175])).
% cnf(178,plain,(releases(X1,X2,X3)|X2!=waterLevel(X4)|X1!=tapOn),inference(split_conjunct,[status(thm)],[175])).
% cnf(180,plain,(plus(n0,n2)=n2),inference(split_conjunct,[status(thm)],[33])).
% cnf(182,plain,(tapOff!=tapOn),inference(split_conjunct,[status(thm)],[35])).
% cnf(183,plain,(tapOff!=overflow),inference(split_conjunct,[status(thm)],[36])).
% fof(184, plain,![X4]:![X7]:((~(less(X4,X7))|(~(less(X7,X4))&~(X7=X4)))&((less(X7,X4)|X7=X4)|less(X4,X7))),inference(fof_nnf,[status(thm)],[69])).
% fof(185, plain,![X8]:![X9]:((~(less(X8,X9))|(~(less(X9,X8))&~(X9=X8)))&((less(X9,X8)|X9=X8)|less(X8,X9))),inference(variable_rename,[status(thm)],[184])).
% fof(186, plain,![X8]:![X9]:(((~(less(X9,X8))|~(less(X8,X9)))&(~(X9=X8)|~(less(X8,X9))))&((less(X9,X8)|X9=X8)|less(X8,X9))),inference(distribute,[status(thm)],[185])).
% cnf(187,plain,(less(X1,X2)|X2=X1|less(X2,X1)),inference(split_conjunct,[status(thm)],[186])).
% cnf(188,plain,(~less(X1,X2)|X2!=X1),inference(split_conjunct,[status(thm)],[186])).
% cnf(189,plain,(~less(X1,X2)|~less(X2,X1)),inference(split_conjunct,[status(thm)],[186])).
% cnf(190,plain,(plus(n1,n2)=n3),inference(split_conjunct,[status(thm)],[38])).
% fof(192, plain,![X11]:![X8]:![X13]:((~(stoppedIn(X11,X8,X13))|?[X2]:?[X3]:(((happens(X2,X3)&less(X11,X3))&less(X3,X13))&terminates(X2,X8,X3)))&(![X2]:![X3]:(((~(happens(X2,X3))|~(less(X11,X3)))|~(less(X3,X13)))|~(terminates(X2,X8,X3)))|stoppedIn(X11,X8,X13))),inference(fof_nnf,[status(thm)],[40])).
% fof(193, plain,![X14]:![X15]:![X16]:((~(stoppedIn(X14,X15,X16))|?[X17]:?[X18]:(((happens(X17,X18)&less(X14,X18))&less(X18,X16))&terminates(X17,X15,X18)))&(![X19]:![X20]:(((~(happens(X19,X20))|~(less(X14,X20)))|~(less(X20,X16)))|~(terminates(X19,X15,X20)))|stoppedIn(X14,X15,X16))),inference(variable_rename,[status(thm)],[192])).
% fof(194, plain,![X14]:![X15]:![X16]:((~(stoppedIn(X14,X15,X16))|(((happens(esk6_3(X14,X15,X16),esk7_3(X14,X15,X16))&less(X14,esk7_3(X14,X15,X16)))&less(esk7_3(X14,X15,X16),X16))&terminates(esk6_3(X14,X15,X16),X15,esk7_3(X14,X15,X16))))&(![X19]:![X20]:(((~(happens(X19,X20))|~(less(X14,X20)))|~(less(X20,X16)))|~(terminates(X19,X15,X20)))|stoppedIn(X14,X15,X16))),inference(skolemize,[status(esa)],[193])).
% fof(195, plain,![X14]:![X15]:![X16]:![X19]:![X20]:(((((~(happens(X19,X20))|~(less(X14,X20)))|~(less(X20,X16)))|~(terminates(X19,X15,X20)))|stoppedIn(X14,X15,X16))&(~(stoppedIn(X14,X15,X16))|(((happens(esk6_3(X14,X15,X16),esk7_3(X14,X15,X16))&less(X14,esk7_3(X14,X15,X16)))&less(esk7_3(X14,X15,X16),X16))&terminates(esk6_3(X14,X15,X16),X15,esk7_3(X14,X15,X16))))),inference(shift_quantors,[status(thm)],[194])).
% fof(196, plain,![X14]:![X15]:![X16]:![X19]:![X20]:(((((~(happens(X19,X20))|~(less(X14,X20)))|~(less(X20,X16)))|~(terminates(X19,X15,X20)))|stoppedIn(X14,X15,X16))&((((happens(esk6_3(X14,X15,X16),esk7_3(X14,X15,X16))|~(stoppedIn(X14,X15,X16)))&(less(X14,esk7_3(X14,X15,X16))|~(stoppedIn(X14,X15,X16))))&(less(esk7_3(X14,X15,X16),X16)|~(stoppedIn(X14,X15,X16))))&(terminates(esk6_3(X14,X15,X16),X15,esk7_3(X14,X15,X16))|~(stoppedIn(X14,X15,X16))))),inference(distribute,[status(thm)],[195])).
% cnf(197,plain,(terminates(esk6_3(X1,X2,X3),X2,esk7_3(X1,X2,X3))|~stoppedIn(X1,X2,X3)),inference(split_conjunct,[status(thm)],[196])).
% cnf(198,plain,(less(esk7_3(X1,X2,X3),X3)|~stoppedIn(X1,X2,X3)),inference(split_conjunct,[status(thm)],[196])).
% cnf(199,plain,(less(X1,esk7_3(X1,X2,X3))|~stoppedIn(X1,X2,X3)),inference(split_conjunct,[status(thm)],[196])).
% cnf(200,plain,(happens(esk6_3(X1,X2,X3),esk7_3(X1,X2,X3))|~stoppedIn(X1,X2,X3)),inference(split_conjunct,[status(thm)],[196])).
% fof(213, plain,![X4]:((~(less(X4,n1))|less_or_equal(X4,n0))&(~(less_or_equal(X4,n0))|less(X4,n1))),inference(fof_nnf,[status(thm)],[43])).
% fof(214, plain,![X5]:((~(less(X5,n1))|less_or_equal(X5,n0))&(~(less_or_equal(X5,n0))|less(X5,n1))),inference(variable_rename,[status(thm)],[213])).
% cnf(215,plain,(less(X1,n1)|~less_or_equal(X1,n0)),inference(split_conjunct,[status(thm)],[214])).
% cnf(216,plain,(less_or_equal(X1,n0)|~less(X1,n1)),inference(split_conjunct,[status(thm)],[214])).
% cnf(217,plain,(plus(n1,n1)=n2),inference(split_conjunct,[status(thm)],[44])).
% fof(219, plain,![X4]:![X7]:((~(less_or_equal(X4,X7))|(less(X4,X7)|X4=X7))&((~(less(X4,X7))&~(X4=X7))|less_or_equal(X4,X7))),inference(fof_nnf,[status(thm)],[46])).
% fof(220, plain,![X8]:![X9]:((~(less_or_equal(X8,X9))|(less(X8,X9)|X8=X9))&((~(less(X8,X9))&~(X8=X9))|less_or_equal(X8,X9))),inference(variable_rename,[status(thm)],[219])).
% fof(221, plain,![X8]:![X9]:((~(less_or_equal(X8,X9))|(less(X8,X9)|X8=X9))&((~(less(X8,X9))|less_or_equal(X8,X9))&(~(X8=X9)|less_or_equal(X8,X9)))),inference(distribute,[status(thm)],[220])).
% cnf(222,plain,(less_or_equal(X1,X2)|X1!=X2),inference(split_conjunct,[status(thm)],[221])).
% cnf(223,plain,(less_or_equal(X1,X2)|~less(X1,X2)),inference(split_conjunct,[status(thm)],[221])).
% cnf(224,plain,(X1=X2|less(X1,X2)|~less_or_equal(X1,X2)),inference(split_conjunct,[status(thm)],[221])).
% fof(225, plain,![X4]:((~(less(X4,n3))|less_or_equal(X4,n2))&(~(less_or_equal(X4,n2))|less(X4,n3))),inference(fof_nnf,[status(thm)],[47])).
% fof(226, plain,![X5]:((~(less(X5,n3))|less_or_equal(X5,n2))&(~(less_or_equal(X5,n2))|less(X5,n3))),inference(variable_rename,[status(thm)],[225])).
% cnf(227,plain,(less(X1,n3)|~less_or_equal(X1,n2)),inference(split_conjunct,[status(thm)],[226])).
% cnf(228,plain,(less_or_equal(X1,n2)|~less(X1,n3)),inference(split_conjunct,[status(thm)],[226])).
% fof(233, plain,![X4]:((~(less(X4,n2))|less_or_equal(X4,n1))&(~(less_or_equal(X4,n1))|less(X4,n2))),inference(fof_nnf,[status(thm)],[49])).
% fof(234, plain,![X5]:((~(less(X5,n2))|less_or_equal(X5,n1))&(~(less_or_equal(X5,n1))|less(X5,n2))),inference(variable_rename,[status(thm)],[233])).
% cnf(235,plain,(less(X1,n2)|~less_or_equal(X1,n1)),inference(split_conjunct,[status(thm)],[234])).
% cnf(236,plain,(less_or_equal(X1,n1)|~less(X1,n2)),inference(split_conjunct,[status(thm)],[234])).
% cnf(257,negated_conjecture,(~happens(overflow,n3)),inference(split_conjunct,[status(thm)],[70])).
% fof(258, plain,![X2]:![X3]:![X8]:((~(epred1_3(X8,X3,X2))|((((X2=tapOn&X8=filling)|(X2=overflow&X8=spilling))|?[X1]:((holdsAt(waterLevel(X1),X3)&X2=tapOff)&X8=waterLevel(X1)))|?[X1]:((holdsAt(waterLevel(X1),X3)&X2=overflow)&X8=waterLevel(X1))))&(((((~(X2=tapOn)|~(X8=filling))&(~(X2=overflow)|~(X8=spilling)))&![X1]:((~(holdsAt(waterLevel(X1),X3))|~(X2=tapOff))|~(X8=waterLevel(X1))))&![X1]:((~(holdsAt(waterLevel(X1),X3))|~(X2=overflow))|~(X8=waterLevel(X1))))|epred1_3(X8,X3,X2))),inference(fof_nnf,[status(thm)],[71])).
% fof(259, plain,![X9]:![X10]:![X11]:((~(epred1_3(X11,X10,X9))|((((X9=tapOn&X11=filling)|(X9=overflow&X11=spilling))|?[X12]:((holdsAt(waterLevel(X12),X10)&X9=tapOff)&X11=waterLevel(X12)))|?[X13]:((holdsAt(waterLevel(X13),X10)&X9=overflow)&X11=waterLevel(X13))))&(((((~(X9=tapOn)|~(X11=filling))&(~(X9=overflow)|~(X11=spilling)))&![X14]:((~(holdsAt(waterLevel(X14),X10))|~(X9=tapOff))|~(X11=waterLevel(X14))))&![X15]:((~(holdsAt(waterLevel(X15),X10))|~(X9=overflow))|~(X11=waterLevel(X15))))|epred1_3(X11,X10,X9))),inference(variable_rename,[status(thm)],[258])).
% fof(260, plain,![X9]:![X10]:![X11]:((~(epred1_3(X11,X10,X9))|((((X9=tapOn&X11=filling)|(X9=overflow&X11=spilling))|((holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)&X9=tapOff)&X11=waterLevel(esk10_3(X9,X10,X11))))|((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)&X9=overflow)&X11=waterLevel(esk11_3(X9,X10,X11)))))&(((((~(X9=tapOn)|~(X11=filling))&(~(X9=overflow)|~(X11=spilling)))&![X14]:((~(holdsAt(waterLevel(X14),X10))|~(X9=tapOff))|~(X11=waterLevel(X14))))&![X15]:((~(holdsAt(waterLevel(X15),X10))|~(X9=overflow))|~(X11=waterLevel(X15))))|epred1_3(X11,X10,X9))),inference(skolemize,[status(esa)],[259])).
% fof(261, plain,![X9]:![X10]:![X11]:![X14]:![X15]:(((((~(holdsAt(waterLevel(X15),X10))|~(X9=overflow))|~(X11=waterLevel(X15)))&(((~(holdsAt(waterLevel(X14),X10))|~(X9=tapOff))|~(X11=waterLevel(X14)))&((~(X9=tapOn)|~(X11=filling))&(~(X9=overflow)|~(X11=spilling)))))|epred1_3(X11,X10,X9))&(~(epred1_3(X11,X10,X9))|((((X9=tapOn&X11=filling)|(X9=overflow&X11=spilling))|((holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)&X9=tapOff)&X11=waterLevel(esk10_3(X9,X10,X11))))|((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)&X9=overflow)&X11=waterLevel(esk11_3(X9,X10,X11)))))),inference(shift_quantors,[status(thm)],[260])).
% fof(262, plain,![X9]:![X10]:![X11]:![X14]:![X15]:(((((~(holdsAt(waterLevel(X15),X10))|~(X9=overflow))|~(X11=waterLevel(X15)))|epred1_3(X11,X10,X9))&((((~(holdsAt(waterLevel(X14),X10))|~(X9=tapOff))|~(X11=waterLevel(X14)))|epred1_3(X11,X10,X9))&(((~(X9=tapOn)|~(X11=filling))|epred1_3(X11,X10,X9))&((~(X9=overflow)|~(X11=spilling))|epred1_3(X11,X10,X9)))))&((((((((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)|(holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)|(X9=overflow|X9=tapOn)))|~(epred1_3(X11,X10,X9)))&((X9=overflow|(holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)|(X9=overflow|X9=tapOn)))|~(epred1_3(X11,X10,X9))))&((X11=waterLevel(esk11_3(X9,X10,X11))|(holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)|(X9=overflow|X9=tapOn)))|~(epred1_3(X11,X10,X9))))&((((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)|(X9=tapOff|(X9=overflow|X9=tapOn)))|~(epred1_3(X11,X10,X9)))&((X9=overflow|(X9=tapOff|(X9=overflow|X9=tapOn)))|~(epred1_3(X11,X10,X9))))&((X11=waterLevel(esk11_3(X9,X10,X11))|(X9=tapOff|(X9=overflow|X9=tapOn)))|~(epred1_3(X11,X10,X9)))))&((((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)|(X11=waterLevel(esk10_3(X9,X10,X11))|(X9=overflow|X9=tapOn)))|~(epred1_3(X11,X10,X9)))&((X9=overflow|(X11=waterLevel(esk10_3(X9,X10,X11))|(X9=overflow|X9=tapOn)))|~(epred1_3(X11,X10,X9))))&((X11=waterLevel(esk11_3(X9,X10,X11))|(X11=waterLevel(esk10_3(X9,X10,X11))|(X9=overflow|X9=tapOn)))|~(epred1_3(X11,X10,X9)))))&((((((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)|(holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)|(X11=spilling|X9=tapOn)))|~(epred1_3(X11,X10,X9)))&((X9=overflow|(holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)|(X11=spilling|X9=tapOn)))|~(epred1_3(X11,X10,X9))))&((X11=waterLevel(esk11_3(X9,X10,X11))|(holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)|(X11=spilling|X9=tapOn)))|~(epred1_3(X11,X10,X9))))&((((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)|(X9=tapOff|(X11=spilling|X9=tapOn)))|~(epred1_3(X11,X10,X9)))&((X9=overflow|(X9=tapOff|(X11=spilling|X9=tapOn)))|~(epred1_3(X11,X10,X9))))&((X11=waterLevel(esk11_3(X9,X10,X11))|(X9=tapOff|(X11=spilling|X9=tapOn)))|~(epred1_3(X11,X10,X9)))))&((((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)|(X11=waterLevel(esk10_3(X9,X10,X11))|(X11=spilling|X9=tapOn)))|~(epred1_3(X11,X10,X9)))&((X9=overflow|(X11=waterLevel(esk10_3(X9,X10,X11))|(X11=spilling|X9=tapOn)))|~(epred1_3(X11,X10,X9))))&((X11=waterLevel(esk11_3(X9,X10,X11))|(X11=waterLevel(esk10_3(X9,X10,X11))|(X11=spilling|X9=tapOn)))|~(epred1_3(X11,X10,X9))))))&(((((((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)|(holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)|(X9=overflow|X11=filling)))|~(epred1_3(X11,X10,X9)))&((X9=overflow|(holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)|(X9=overflow|X11=filling)))|~(epred1_3(X11,X10,X9))))&((X11=waterLevel(esk11_3(X9,X10,X11))|(holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)|(X9=overflow|X11=filling)))|~(epred1_3(X11,X10,X9))))&((((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)|(X9=tapOff|(X9=overflow|X11=filling)))|~(epred1_3(X11,X10,X9)))&((X9=overflow|(X9=tapOff|(X9=overflow|X11=filling)))|~(epred1_3(X11,X10,X9))))&((X11=waterLevel(esk11_3(X9,X10,X11))|(X9=tapOff|(X9=overflow|X11=filling)))|~(epred1_3(X11,X10,X9)))))&((((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)|(X11=waterLevel(esk10_3(X9,X10,X11))|(X9=overflow|X11=filling)))|~(epred1_3(X11,X10,X9)))&((X9=overflow|(X11=waterLevel(esk10_3(X9,X10,X11))|(X9=overflow|X11=filling)))|~(epred1_3(X11,X10,X9))))&((X11=waterLevel(esk11_3(X9,X10,X11))|(X11=waterLevel(esk10_3(X9,X10,X11))|(X9=overflow|X11=filling)))|~(epred1_3(X11,X10,X9)))))&((((((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)|(holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)|(X11=spilling|X11=filling)))|~(epred1_3(X11,X10,X9)))&((X9=overflow|(holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)|(X11=spilling|X11=filling)))|~(epred1_3(X11,X10,X9))))&((X11=waterLevel(esk11_3(X9,X10,X11))|(holdsAt(waterLevel(esk10_3(X9,X10,X11)),X10)|(X11=spilling|X11=filling)))|~(epred1_3(X11,X10,X9))))&((((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)|(X9=tapOff|(X11=spilling|X11=filling)))|~(epred1_3(X11,X10,X9)))&((X9=overflow|(X9=tapOff|(X11=spilling|X11=filling)))|~(epred1_3(X11,X10,X9))))&((X11=waterLevel(esk11_3(X9,X10,X11))|(X9=tapOff|(X11=spilling|X11=filling)))|~(epred1_3(X11,X10,X9)))))&((((holdsAt(waterLevel(esk11_3(X9,X10,X11)),X10)|(X11=waterLevel(esk10_3(X9,X10,X11))|(X11=spilling|X11=filling)))|~(epred1_3(X11,X10,X9)))&((X9=overflow|(X11=waterLevel(esk10_3(X9,X10,X11))|(X11=spilling|X11=filling)))|~(epred1_3(X11,X10,X9))))&((X11=waterLevel(esk11_3(X9,X10,X11))|(X11=waterLevel(esk10_3(X9,X10,X11))|(X11=spilling|X11=filling)))|~(epred1_3(X11,X10,X9)))))))),inference(distribute,[status(thm)],[261])).
% cnf(266,plain,(X1=filling|X1=spilling|X3=tapOff|X1=waterLevel(esk11_3(X3,X2,X1))|~epred1_3(X1,X2,X3)),inference(split_conjunct,[status(thm)],[262])).
% cnf(268,plain,(X1=filling|X1=spilling|X3=tapOff|holdsAt(waterLevel(esk11_3(X3,X2,X1)),X2)|~epred1_3(X1,X2,X3)),inference(split_conjunct,[status(thm)],[262])).
% cnf(300,plain,(epred1_3(X1,X2,X3)|X1!=filling|X3!=tapOn),inference(split_conjunct,[status(thm)],[262])).
% cnf(302,plain,(epred1_3(X1,X2,X3)|X1!=waterLevel(X4)|X3!=overflow|~holdsAt(waterLevel(X4),X2)),inference(split_conjunct,[status(thm)],[262])).
% cnf(303,plain,(less_or_equal(X1,X1)),inference(er,[status(thm)],[222,theory(equality)])).
% cnf(304,plain,(~less(X1,X1)),inference(er,[status(thm)],[188,theory(equality)])).
% cnf(314,plain,(plus(n1,n0)=n1),inference(rw,[status(thm)],[170,128,theory(equality)])).
% cnf(324,plain,(happens(X1,n0)|tapOn!=X1),inference(er,[status(thm)],[84,theory(equality)])).
% cnf(335,plain,(less_or_equal(X1,n2)|X1=n3|less(n3,X1)),inference(spm,[status(thm)],[228,187,theory(equality)])).
% cnf(340,plain,(less_or_equal(X1,n0)|X1=n1|less(n1,X1)),inference(spm,[status(thm)],[216,187,theory(equality)])).
% cnf(342,plain,(less_or_equal(X1,n1)|X1=n2|less(n2,X1)),inference(spm,[status(thm)],[236,187,theory(equality)])).
% cnf(355,plain,(epred1_3(filling,X1,X2)|tapOn!=X2),inference(er,[status(thm)],[300,theory(equality)])).
% cnf(357,plain,(happens(overflow,X1)|~holdsAt(waterLevel(n3),X1)|~holdsAt(filling,X1)),inference(er,[status(thm)],[83,theory(equality)])).
% cnf(358,plain,(releases(tapOn,X1,X2)|waterLevel(X3)!=X1),inference(er,[status(thm)],[178,theory(equality)])).
% cnf(362,plain,(epred1_3(X1,X2,overflow)|waterLevel(X3)!=X1|~holdsAt(waterLevel(X3),X2)),inference(er,[status(thm)],[302,theory(equality)])).
% cnf(367,plain,(~initiates(X1,X2,X3)|~happens(X1,X3)|~releasedAt(X2,plus(n1,X3))),inference(spm,[status(thm)],[163,128,theory(equality)])).
% cnf(378,plain,(releases(esk3_2(X1,n1),X1,n1)|releasedAt(X1,n1)|~releasedAt(X1,n2)),inference(spm,[status(thm)],[142,217,theory(equality)])).
% cnf(379,plain,(releases(esk3_2(X1,X2),X1,X2)|releasedAt(X1,X2)|~releasedAt(X1,plus(n1,X2))),inference(spm,[status(thm)],[142,128,theory(equality)])).
% cnf(384,plain,(trajectory(filling,X1,waterLevel(plus(X2,X3)),X3)|~holdsAt(waterLevel(X2),X1)),inference(er,[status(thm)],[110,theory(equality)])).
% cnf(453,plain,(less(n2,n3)),inference(spm,[status(thm)],[227,303,theory(equality)])).
% cnf(454,plain,(less(n1,n2)),inference(spm,[status(thm)],[235,303,theory(equality)])).
% cnf(456,plain,(less(n0,n1)),inference(spm,[status(thm)],[215,303,theory(equality)])).
% cnf(487,plain,(happens(tapOn,n0)),inference(er,[status(thm)],[324,theory(equality)])).
% cnf(592,plain,(less_or_equal(n1,n2)),inference(spm,[status(thm)],[223,454,theory(equality)])).
% cnf(596,plain,(less_or_equal(n0,n1)),inference(spm,[status(thm)],[223,456,theory(equality)])).
% cnf(599,plain,(stoppedIn(X1,X2,plus(X1,n1))|holdsAt(X3,plus(X1,n1))|~trajectory(X2,X1,X3,n1)|~initiates(X4,X2,X1)|~happens(X4,X1)),inference(spm,[status(thm)],[166,456,theory(equality)])).
% cnf(646,plain,(X1=n2|less(X1,n2)|X1=n3|less(n3,X1)),inference(spm,[status(thm)],[224,335,theory(equality)])).
% cnf(655,plain,(less(n1,n3)),inference(spm,[status(thm)],[227,592,theory(equality)])).
% cnf(681,plain,(less(n0,n2)),inference(spm,[status(thm)],[235,596,theory(equality)])).
% cnf(738,plain,(less_or_equal(n0,n2)),inference(spm,[status(thm)],[223,681,theory(equality)])).
% cnf(741,plain,(stoppedIn(X1,X2,plus(X1,n2))|holdsAt(X3,plus(X1,n2))|~trajectory(X2,X1,X3,n2)|~initiates(X4,X2,X1)|~happens(X4,X1)),inference(spm,[status(thm)],[166,681,theory(equality)])).
% cnf(753,plain,(X1=n0|less(X1,n0)|X1=n1|less(n1,X1)),inference(spm,[status(thm)],[224,340,theory(equality)])).
% cnf(755,plain,(X1=n0|X1=n1|less(n1,X1)),inference(sr,[status(thm)],[753,113,theory(equality)])).
% cnf(774,plain,(less(n0,n3)),inference(spm,[status(thm)],[227,738,theory(equality)])).
% cnf(791,plain,(stoppedIn(X1,X2,plus(X1,n3))|holdsAt(X3,plus(X1,n3))|~trajectory(X2,X1,X3,n3)|~initiates(X4,X2,X1)|~happens(X4,X1)),inference(spm,[status(thm)],[166,774,theory(equality)])).
% cnf(804,plain,(X1=n1|less(X1,n1)|X1=n2|less(n2,X1)),inference(spm,[status(thm)],[224,342,theory(equality)])).
% cnf(1062,plain,(X1=n1|X1=n0|~less(X1,n1)),inference(spm,[status(thm)],[189,755,theory(equality)])).
% cnf(1103,plain,(epred1_3(filling,X1,tapOn)),inference(er,[status(thm)],[355,theory(equality)])).
% cnf(1111,plain,(initiates(tapOn,filling,X1)),inference(spm,[status(thm)],[106,1103,theory(equality)])).
% cnf(1113,plain,(holdsAt(filling,plus(X1,n1))|~happens(tapOn,X1)),inference(spm,[status(thm)],[146,1111,theory(equality)])).
% cnf(1169,plain,(releases(tapOn,waterLevel(X1),X2)),inference(er,[status(thm)],[358,theory(equality)])).
% cnf(1170,plain,(epred1_3(waterLevel(X1),X2,overflow)|~holdsAt(waterLevel(X1),X2)),inference(er,[status(thm)],[362,theory(equality)])).
% cnf(1200,plain,(waterLevel(esk5_3(tapOn,waterLevel(X1),X2))=waterLevel(X1)),inference(spm,[status(thm)],[176,1169,theory(equality)])).
% cnf(1282,plain,(holdsAt(filling,plus(n0,n1))),inference(spm,[status(thm)],[1113,487,theory(equality)])).
% cnf(1283,plain,(holdsAt(filling,n1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[1282,128,theory(equality)]),314,theory(equality)])).
% cnf(1313,plain,(happens(esk1_2(filling,n1),n1)|releasedAt(filling,plus(n1,n1))|holdsAt(filling,plus(n1,n1))),inference(spm,[status(thm)],[119,1283,theory(equality)])).
% cnf(1314,plain,(terminates(esk1_2(filling,n1),filling,n1)|releasedAt(filling,plus(n1,n1))|holdsAt(filling,plus(n1,n1))),inference(spm,[status(thm)],[118,1283,theory(equality)])).
% cnf(1317,plain,(happens(esk1_2(filling,n1),n1)|releasedAt(filling,n2)|holdsAt(filling,plus(n1,n1))),inference(rw,[status(thm)],[1313,217,theory(equality)])).
% cnf(1318,plain,(happens(esk1_2(filling,n1),n1)|releasedAt(filling,n2)|holdsAt(filling,n2)),inference(rw,[status(thm)],[1317,217,theory(equality)])).
% cnf(1319,plain,(terminates(esk1_2(filling,n1),filling,n1)|releasedAt(filling,n2)|holdsAt(filling,plus(n1,n1))),inference(rw,[status(thm)],[1314,217,theory(equality)])).
% cnf(1320,plain,(terminates(esk1_2(filling,n1),filling,n1)|releasedAt(filling,n2)|holdsAt(filling,n2)),inference(rw,[status(thm)],[1319,217,theory(equality)])).
% cnf(1584,plain,(~initiates(X1,X2,n0)|~happens(X1,n0)|~releasedAt(X2,n1)),inference(spm,[status(thm)],[367,314,theory(equality)])).
% cnf(2342,plain,(releases(esk3_2(X1,n2),X1,n2)|releasedAt(X1,n2)|~releasedAt(X1,n3)),inference(spm,[status(thm)],[379,190,theory(equality)])).
% cnf(2414,plain,(esk5_3(tapOn,waterLevel(X1),X2)=X3|waterLevel(X1)!=waterLevel(X3)),inference(spm,[status(thm)],[102,1200,theory(equality)])).
% cnf(2590,plain,(X1=n3|X1=n2|less(n3,X1)|~less(n2,X1)),inference(spm,[status(thm)],[189,646,theory(equality)])).
% cnf(2627,plain,(trajectory(filling,n0,waterLevel(plus(n0,X1)),X1)),inference(spm,[status(thm)],[384,73,theory(equality)])).
% cnf(2882,plain,(X1=n0|X1=n1|X1=n2|less(n2,X1)),inference(spm,[status(thm)],[1062,804,theory(equality)])).
% cnf(2941,plain,(X1=n2|X1=n1|X1=n0|~less(X1,n2)),inference(spm,[status(thm)],[189,2882,theory(equality)])).
% cnf(4726,plain,(X1=n2|X1=n3|less(n3,X1)|X1=n1|X1=n0),inference(spm,[status(thm)],[2590,2882,theory(equality)])).
% cnf(4758,plain,(X1=n0|X1=n1|X1=n3|X1=n2|~less(X1,n3)),inference(spm,[status(thm)],[189,4726,theory(equality)])).
% cnf(5566,plain,(stoppedIn(n0,filling,plus(n0,n1))|holdsAt(waterLevel(plus(n0,n1)),plus(n0,n1))|~initiates(X1,filling,n0)|~happens(X1,n0)),inference(spm,[status(thm)],[599,2627,theory(equality)])).
% cnf(5569,plain,(stoppedIn(n0,filling,n1)|holdsAt(waterLevel(plus(n0,n1)),plus(n0,n1))|~initiates(X1,filling,n0)|~happens(X1,n0)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[5566,128,theory(equality)]),314,theory(equality)])).
% cnf(5570,plain,(stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)|~initiates(X1,filling,n0)|~happens(X1,n0)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[5569,128,theory(equality)]),314,theory(equality)]),128,theory(equality)]),314,theory(equality)])).
% cnf(5881,plain,(stoppedIn(n0,filling,plus(n0,n2))|holdsAt(waterLevel(plus(n0,n2)),plus(n0,n2))|~initiates(X1,filling,n0)|~happens(X1,n0)),inference(spm,[status(thm)],[741,2627,theory(equality)])).
% cnf(5884,plain,(stoppedIn(n0,filling,n2)|holdsAt(waterLevel(plus(n0,n2)),plus(n0,n2))|~initiates(X1,filling,n0)|~happens(X1,n0)),inference(rw,[status(thm)],[5881,180,theory(equality)])).
% cnf(5885,plain,(stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2)|~initiates(X1,filling,n0)|~happens(X1,n0)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[5884,180,theory(equality)]),180,theory(equality)])).
% cnf(6157,plain,(stoppedIn(n0,filling,plus(n0,n3))|holdsAt(waterLevel(plus(n0,n3)),plus(n0,n3))|~initiates(X1,filling,n0)|~happens(X1,n0)),inference(spm,[status(thm)],[791,2627,theory(equality)])).
% cnf(6160,plain,(stoppedIn(n0,filling,n3)|holdsAt(waterLevel(plus(n0,n3)),plus(n0,n3))|~initiates(X1,filling,n0)|~happens(X1,n0)),inference(rw,[status(thm)],[6157,103,theory(equality)])).
% cnf(6161,plain,(stoppedIn(n0,filling,n3)|holdsAt(waterLevel(n3),n3)|~initiates(X1,filling,n0)|~happens(X1,n0)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6160,103,theory(equality)]),103,theory(equality)])).
% cnf(8163,plain,(~initiates(tapOn,X1,n0)|~releasedAt(X1,n1)),inference(spm,[status(thm)],[1584,487,theory(equality)])).
% cnf(10638,plain,(overflow=esk1_2(filling,n1)|tapOn=esk1_2(filling,n1)|releasedAt(filling,n2)|holdsAt(filling,n2)),inference(spm,[status(thm)],[88,1318,theory(equality)])).
% cnf(10993,plain,(tapOff=esk1_2(filling,n1)|overflow=esk1_2(filling,n1)|releasedAt(filling,n2)|holdsAt(filling,n2)),inference(spm,[status(thm)],[137,1320,theory(equality)])).
% cnf(12850,plain,(esk5_3(tapOn,waterLevel(X1),X2)=X1),inference(er,[status(thm)],[2414,theory(equality)])).
% cnf(13758,plain,(stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)|~initiates(tapOn,filling,n0)),inference(spm,[status(thm)],[5570,487,theory(equality)])).
% cnf(13759,plain,(stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)|$false),inference(rw,[status(thm)],[13758,1111,theory(equality)])).
% cnf(13760,plain,(stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)),inference(cn,[status(thm)],[13759,theory(equality)])).
% cnf(13769,plain,(less(n0,esk7_3(n0,filling,n1))|holdsAt(waterLevel(n1),n1)),inference(spm,[status(thm)],[199,13760,theory(equality)])).
% cnf(13770,plain,(less(esk7_3(n0,filling,n1),n1)|holdsAt(waterLevel(n1),n1)),inference(spm,[status(thm)],[198,13760,theory(equality)])).
% cnf(13779,plain,(less_or_equal(esk7_3(n0,filling,n1),n0)|holdsAt(waterLevel(n1),n1)),inference(spm,[status(thm)],[216,13770,theory(equality)])).
% cnf(13803,plain,(esk7_3(n0,filling,n1)=n0|less(esk7_3(n0,filling,n1),n0)|holdsAt(waterLevel(n1),n1)),inference(spm,[status(thm)],[224,13779,theory(equality)])).
% cnf(13805,plain,(esk7_3(n0,filling,n1)=n0|holdsAt(waterLevel(n1),n1)),inference(sr,[status(thm)],[13803,113,theory(equality)])).
% cnf(13806,plain,(less(n0,n0)|holdsAt(waterLevel(n1),n1)),inference(spm,[status(thm)],[13769,13805,theory(equality)])).
% cnf(13811,plain,(holdsAt(waterLevel(n1),n1)),inference(sr,[status(thm)],[13806,113,theory(equality)])).
% cnf(13822,plain,(X1=n1|~holdsAt(waterLevel(X1),n1)),inference(spm,[status(thm)],[98,13811,theory(equality)])).
% cnf(14642,plain,(stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2)|~initiates(tapOn,filling,n0)),inference(spm,[status(thm)],[5885,487,theory(equality)])).
% cnf(14643,plain,(stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2)|$false),inference(rw,[status(thm)],[14642,1111,theory(equality)])).
% cnf(14644,plain,(stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2)),inference(cn,[status(thm)],[14643,theory(equality)])).
% cnf(14649,plain,(less(n0,esk7_3(n0,filling,n2))|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[199,14644,theory(equality)])).
% cnf(14650,plain,(less(esk7_3(n0,filling,n2),n2)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[198,14644,theory(equality)])).
% cnf(14651,plain,(happens(esk6_3(n0,filling,n2),esk7_3(n0,filling,n2))|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[200,14644,theory(equality)])).
% cnf(14652,plain,(terminates(esk6_3(n0,filling,n2),filling,esk7_3(n0,filling,n2))|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[197,14644,theory(equality)])).
% cnf(14660,plain,(esk7_3(n0,filling,n2)=n0|esk7_3(n0,filling,n2)=n1|esk7_3(n0,filling,n2)=n2|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[2941,14650,theory(equality)])).
% cnf(14852,plain,(stoppedIn(n0,filling,n3)|holdsAt(waterLevel(n3),n3)|~initiates(tapOn,filling,n0)),inference(spm,[status(thm)],[6161,487,theory(equality)])).
% cnf(14853,plain,(stoppedIn(n0,filling,n3)|holdsAt(waterLevel(n3),n3)|$false),inference(rw,[status(thm)],[14852,1111,theory(equality)])).
% cnf(14854,plain,(stoppedIn(n0,filling,n3)|holdsAt(waterLevel(n3),n3)),inference(cn,[status(thm)],[14853,theory(equality)])).
% cnf(14861,plain,(less(n0,esk7_3(n0,filling,n3))|holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[199,14854,theory(equality)])).
% cnf(14862,plain,(less(esk7_3(n0,filling,n3),n3)|holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[198,14854,theory(equality)])).
% cnf(14863,plain,(happens(esk6_3(n0,filling,n3),esk7_3(n0,filling,n3))|holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[200,14854,theory(equality)])).
% cnf(14864,plain,(terminates(esk6_3(n0,filling,n3),filling,esk7_3(n0,filling,n3))|holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[197,14854,theory(equality)])).
% cnf(14875,plain,(esk7_3(n0,filling,n3)=n2|esk7_3(n0,filling,n3)=n3|esk7_3(n0,filling,n3)=n1|esk7_3(n0,filling,n3)=n0|holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[4758,14862,theory(equality)])).
% cnf(15353,plain,(overflow=esk6_3(n0,filling,n3)|tapOn=esk6_3(n0,filling,n3)|holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[88,14863,theory(equality)])).
% cnf(15565,plain,(overflow=esk6_3(n0,filling,n2)|tapOn=esk6_3(n0,filling,n2)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[88,14651,theory(equality)])).
% cnf(15899,plain,(tapOff=esk6_3(n0,filling,n2)|overflow=esk6_3(n0,filling,n2)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[137,14652,theory(equality)])).
% cnf(16416,plain,(tapOff=tapOn|tapOff=overflow|releasedAt(filling,n2)|holdsAt(filling,n2)|esk1_2(filling,n1)=overflow),inference(spm,[status(thm)],[10638,10993,theory(equality)])).
% cnf(16420,plain,(tapOff=overflow|releasedAt(filling,n2)|holdsAt(filling,n2)|esk1_2(filling,n1)=overflow),inference(sr,[status(thm)],[16416,182,theory(equality)])).
% cnf(16421,plain,(releasedAt(filling,n2)|holdsAt(filling,n2)|esk1_2(filling,n1)=overflow),inference(sr,[status(thm)],[16420,183,theory(equality)])).
% cnf(16423,plain,(happens(overflow,n1)|releasedAt(filling,n2)|holdsAt(filling,n2)),inference(spm,[status(thm)],[1318,16421,theory(equality)])).
% cnf(16430,plain,(releases(esk3_2(filling,n1),filling,n1)|releasedAt(filling,n1)|happens(overflow,n1)|holdsAt(filling,n2)),inference(spm,[status(thm)],[378,16423,theory(equality)])).
% cnf(17354,plain,(tapOff=tapOn|tapOff=overflow|holdsAt(waterLevel(n2),n2)|esk6_3(n0,filling,n2)=overflow),inference(spm,[status(thm)],[15565,15899,theory(equality)])).
% cnf(17357,plain,(tapOff=overflow|holdsAt(waterLevel(n2),n2)|esk6_3(n0,filling,n2)=overflow),inference(sr,[status(thm)],[17354,182,theory(equality)])).
% cnf(17358,plain,(holdsAt(waterLevel(n2),n2)|esk6_3(n0,filling,n2)=overflow),inference(sr,[status(thm)],[17357,183,theory(equality)])).
% cnf(17361,plain,(happens(overflow,esk7_3(n0,filling,n2))|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[14651,17358,theory(equality)])).
% cnf(17364,plain,(tapOn=overflow|holdsAt(waterLevel(n3),esk7_3(n0,filling,n2))|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[90,17361,theory(equality)])).
% cnf(17371,plain,(holdsAt(waterLevel(n3),esk7_3(n0,filling,n2))|holdsAt(waterLevel(n2),n2)),inference(sr,[status(thm)],[17364,126,theory(equality)])).
% cnf(17382,plain,(epred1_3(waterLevel(n3),esk7_3(n0,filling,n2),overflow)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[1170,17371,theory(equality)])).
% cnf(17389,plain,(initiates(overflow,waterLevel(n3),esk7_3(n0,filling,n2))|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[106,17382,theory(equality)])).
% cnf(17489,plain,(tapOff=esk6_3(n0,filling,n3)|overflow=esk6_3(n0,filling,n3)|holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[137,14864,theory(equality)])).
% cnf(17495,plain,(tapOff=tapOn|tapOff=overflow|holdsAt(waterLevel(n3),n3)|esk6_3(n0,filling,n3)=overflow),inference(spm,[status(thm)],[15353,17489,theory(equality)])).
% cnf(17499,plain,(tapOff=overflow|holdsAt(waterLevel(n3),n3)|esk6_3(n0,filling,n3)=overflow),inference(sr,[status(thm)],[17495,182,theory(equality)])).
% cnf(17500,plain,(holdsAt(waterLevel(n3),n3)|esk6_3(n0,filling,n3)=overflow),inference(sr,[status(thm)],[17499,183,theory(equality)])).
% cnf(17503,plain,(happens(overflow,esk7_3(n0,filling,n3))|holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[14863,17500,theory(equality)])).
% cnf(17507,plain,(tapOn=overflow|holdsAt(waterLevel(n3),esk7_3(n0,filling,n3))|holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[90,17503,theory(equality)])).
% cnf(17514,plain,(holdsAt(waterLevel(n3),esk7_3(n0,filling,n3))|holdsAt(waterLevel(n3),n3)),inference(sr,[status(thm)],[17507,126,theory(equality)])).
% cnf(17525,plain,(epred1_3(waterLevel(n3),esk7_3(n0,filling,n3),overflow)|holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[1170,17514,theory(equality)])).
% cnf(17532,plain,(initiates(overflow,waterLevel(n3),esk7_3(n0,filling,n3))|holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[106,17525,theory(equality)])).
% cnf(17574,plain,(holdsAt(waterLevel(n3),plus(esk7_3(n0,filling,n3),n1))|holdsAt(waterLevel(n3),n3)|~happens(overflow,esk7_3(n0,filling,n3))),inference(spm,[status(thm)],[146,17532,theory(equality)])).
% cnf(21557,plain,(waterLevel(esk5_3(esk3_2(filling,n1),filling,n1))=filling|happens(overflow,n1)|releasedAt(filling,n1)|holdsAt(filling,n2)),inference(spm,[status(thm)],[176,16430,theory(equality)])).
% cnf(21559,plain,(happens(overflow,n1)|releasedAt(filling,n1)|holdsAt(filling,n2)),inference(sr,[status(thm)],[21557,93,theory(equality)])).
% cnf(21567,plain,(happens(overflow,n1)|holdsAt(filling,n2)|~initiates(tapOn,filling,n0)),inference(spm,[status(thm)],[8163,21559,theory(equality)])).
% cnf(21573,plain,(happens(overflow,n1)|holdsAt(filling,n2)|$false),inference(rw,[status(thm)],[21567,1111,theory(equality)])).
% cnf(21574,plain,(happens(overflow,n1)|holdsAt(filling,n2)),inference(cn,[status(thm)],[21573,theory(equality)])).
% cnf(21576,plain,(tapOn=overflow|holdsAt(waterLevel(n3),n1)|holdsAt(filling,n2)),inference(spm,[status(thm)],[90,21574,theory(equality)])).
% cnf(21599,plain,(holdsAt(waterLevel(n3),n1)|holdsAt(filling,n2)),inference(sr,[status(thm)],[21576,126,theory(equality)])).
% cnf(21624,plain,(n3=n1|holdsAt(filling,n2)),inference(spm,[status(thm)],[13822,21599,theory(equality)])).
% cnf(21632,plain,(happens(esk1_2(filling,n2),n2)|releasedAt(filling,plus(n2,n1))|holdsAt(filling,plus(n2,n1))|n3=n1),inference(spm,[status(thm)],[119,21624,theory(equality)])).
% cnf(21633,plain,(terminates(esk1_2(filling,n2),filling,n2)|releasedAt(filling,plus(n2,n1))|holdsAt(filling,plus(n2,n1))|n3=n1),inference(spm,[status(thm)],[118,21624,theory(equality)])).
% cnf(22052,plain,(less(n2,n2)|holdsAt(waterLevel(n2),n2)|esk7_3(n0,filling,n2)=n1|esk7_3(n0,filling,n2)=n0),inference(spm,[status(thm)],[14650,14660,theory(equality)])).
% cnf(22120,plain,(holdsAt(waterLevel(n2),n2)|esk7_3(n0,filling,n2)=n1|esk7_3(n0,filling,n2)=n0),inference(sr,[status(thm)],[22052,304,theory(equality)])).
% cnf(24120,plain,(happens(overflow,n2)|holdsAt(waterLevel(n3),n3)|esk7_3(n0,filling,n3)=n0|esk7_3(n0,filling,n3)=n1|esk7_3(n0,filling,n3)=n3),inference(spm,[status(thm)],[17503,14875,theory(equality)])).
% cnf(24204,plain,(less(n0,n0)|holdsAt(waterLevel(n2),n2)|esk7_3(n0,filling,n2)=n1),inference(spm,[status(thm)],[14649,22120,theory(equality)])).
% cnf(24273,plain,(holdsAt(waterLevel(n2),n2)|esk7_3(n0,filling,n2)=n1),inference(sr,[status(thm)],[24204,113,theory(equality)])).
% cnf(24345,plain,(initiates(overflow,waterLevel(n3),n1)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[17389,24273,theory(equality)])).
% cnf(24853,plain,(epred1_3(waterLevel(n3),n1,overflow)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[107,24345,theory(equality)])).
% cnf(24860,plain,(tapOff=overflow|spilling=waterLevel(n3)|filling=waterLevel(n3)|holdsAt(waterLevel(esk11_3(overflow,n1,waterLevel(n3))),n1)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[268,24853,theory(equality)])).
% cnf(24863,plain,(waterLevel(esk11_3(overflow,n1,waterLevel(n3)))=waterLevel(n3)|tapOff=overflow|spilling=waterLevel(n3)|filling=waterLevel(n3)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[266,24853,theory(equality)])).
% cnf(24872,plain,(waterLevel(n3)=spilling|waterLevel(n3)=filling|holdsAt(waterLevel(esk11_3(overflow,n1,waterLevel(n3))),n1)|holdsAt(waterLevel(n2),n2)),inference(sr,[status(thm)],[24860,183,theory(equality)])).
% cnf(24873,plain,(waterLevel(n3)=filling|holdsAt(waterLevel(esk11_3(overflow,n1,waterLevel(n3))),n1)|holdsAt(waterLevel(n2),n2)),inference(sr,[status(thm)],[24872,95,theory(equality)])).
% cnf(24874,plain,(holdsAt(waterLevel(esk11_3(overflow,n1,waterLevel(n3))),n1)|holdsAt(waterLevel(n2),n2)),inference(sr,[status(thm)],[24873,93,theory(equality)])).
% cnf(24880,plain,(waterLevel(esk11_3(overflow,n1,waterLevel(n3)))=waterLevel(n3)|waterLevel(n3)=spilling|waterLevel(n3)=filling|holdsAt(waterLevel(n2),n2)),inference(sr,[status(thm)],[24863,183,theory(equality)])).
% cnf(24881,plain,(waterLevel(esk11_3(overflow,n1,waterLevel(n3)))=waterLevel(n3)|waterLevel(n3)=filling|holdsAt(waterLevel(n2),n2)),inference(sr,[status(thm)],[24880,95,theory(equality)])).
% cnf(24882,plain,(waterLevel(esk11_3(overflow,n1,waterLevel(n3)))=waterLevel(n3)|holdsAt(waterLevel(n2),n2)),inference(sr,[status(thm)],[24881,93,theory(equality)])).
% cnf(25184,plain,(esk5_3(tapOn,waterLevel(n3),X1)=esk11_3(overflow,n1,waterLevel(n3))|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[12850,24882,theory(equality)])).
% cnf(25225,plain,(n3=esk11_3(overflow,n1,waterLevel(n3))|holdsAt(waterLevel(n2),n2)),inference(rw,[status(thm)],[25184,12850,theory(equality)])).
% cnf(26207,plain,(esk11_3(overflow,n1,waterLevel(n3))=n1|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[13822,24874,theory(equality)])).
% cnf(26229,plain,(n1=n3|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[25225,26207,theory(equality)])).
% cnf(26243,plain,(X1=n2|n3=n1|~holdsAt(waterLevel(X1),n2)),inference(spm,[status(thm)],[98,26229,theory(equality)])).
% cnf(35865,plain,(holdsAt(waterLevel(n3),plus(n1,esk7_3(n0,filling,n3)))|holdsAt(waterLevel(n3),n3)|~happens(overflow,esk7_3(n0,filling,n3))),inference(rw,[status(thm)],[17574,128,theory(equality)])).
% cnf(35866,plain,(holdsAt(waterLevel(n3),plus(n1,esk7_3(n0,filling,n3)))|holdsAt(waterLevel(n3),n3)),inference(csr,[status(thm)],[35865,17503])).
% cnf(75320,plain,(happens(esk1_2(filling,n2),n2)|releasedAt(filling,n3)|holdsAt(filling,plus(n2,n1))|n3=n1),inference(rw,[status(thm)],[inference(rw,[status(thm)],[21632,128,theory(equality)]),190,theory(equality)])).
% cnf(75321,plain,(happens(esk1_2(filling,n2),n2)|releasedAt(filling,n3)|holdsAt(filling,n3)|n3=n1),inference(rw,[status(thm)],[inference(rw,[status(thm)],[75320,128,theory(equality)]),190,theory(equality)])).
% cnf(75323,plain,(overflow=esk1_2(filling,n2)|tapOn=esk1_2(filling,n2)|n3=n1|releasedAt(filling,n3)|holdsAt(filling,n3)),inference(spm,[status(thm)],[88,75321,theory(equality)])).
% cnf(75346,plain,(terminates(esk1_2(filling,n2),filling,n2)|releasedAt(filling,n3)|holdsAt(filling,plus(n2,n1))|n3=n1),inference(rw,[status(thm)],[inference(rw,[status(thm)],[21633,128,theory(equality)]),190,theory(equality)])).
% cnf(75347,plain,(terminates(esk1_2(filling,n2),filling,n2)|releasedAt(filling,n3)|holdsAt(filling,n3)|n3=n1),inference(rw,[status(thm)],[inference(rw,[status(thm)],[75346,128,theory(equality)]),
% PrfWatch: 7.90 CPU 8.04 WC
% 190,theory(equality)])).
% cnf(75348,plain,(tapOff=esk1_2(filling,n2)|overflow=esk1_2(filling,n2)|n3=n1|releasedAt(filling,n3)|holdsAt(filling,n3)),inference(spm,[status(thm)],[137,75347,theory(equality)])).
% cnf(81227,plain,(tapOff=tapOn|tapOff=overflow|n3=n1|releasedAt(filling,n3)|holdsAt(filling,n3)|esk1_2(filling,n2)=overflow),inference(spm,[status(thm)],[75323,75348,theory(equality)])).
% cnf(81231,plain,(tapOff=overflow|n3=n1|releasedAt(filling,n3)|holdsAt(filling,n3)|esk1_2(filling,n2)=overflow),inference(sr,[status(thm)],[81227,182,theory(equality)])).
% cnf(81232,plain,(n3=n1|releasedAt(filling,n3)|holdsAt(filling,n3)|esk1_2(filling,n2)=overflow),inference(sr,[status(thm)],[81231,183,theory(equality)])).
% cnf(81237,plain,(n3=n1|happens(overflow,n2)|releasedAt(filling,n3)|holdsAt(filling,n3)),inference(spm,[status(thm)],[75321,81232,theory(equality)])).
% cnf(81243,plain,(releases(esk3_2(filling,n2),filling,n2)|releasedAt(filling,n2)|n3=n1|happens(overflow,n2)|holdsAt(filling,n3)),inference(spm,[status(thm)],[2342,81237,theory(equality)])).
% cnf(85547,plain,(waterLevel(esk5_3(esk3_2(filling,n2),filling,n2))=filling|n3=n1|happens(overflow,n2)|releasedAt(filling,n2)|holdsAt(filling,n3)),inference(spm,[status(thm)],[176,81243,theory(equality)])).
% cnf(85549,plain,(n3=n1|happens(overflow,n2)|releasedAt(filling,n2)|holdsAt(filling,n3)),inference(sr,[status(thm)],[85547,93,theory(equality)])).
% cnf(85553,plain,(releases(esk3_2(filling,n1),filling,n1)|releasedAt(filling,n1)|n3=n1|happens(overflow,n2)|holdsAt(filling,n3)),inference(spm,[status(thm)],[378,85549,theory(equality)])).
% cnf(90707,plain,(waterLevel(esk5_3(esk3_2(filling,n1),filling,n1))=filling|n3=n1|happens(overflow,n2)|releasedAt(filling,n1)|holdsAt(filling,n3)),inference(spm,[status(thm)],[176,85553,theory(equality)])).
% cnf(90709,plain,(n3=n1|happens(overflow,n2)|releasedAt(filling,n1)|holdsAt(filling,n3)),inference(sr,[status(thm)],[90707,93,theory(equality)])).
% cnf(90717,plain,(n3=n1|happens(overflow,n2)|holdsAt(filling,n3)|~initiates(tapOn,filling,n0)),inference(spm,[status(thm)],[8163,90709,theory(equality)])).
% cnf(90723,plain,(n3=n1|happens(overflow,n2)|holdsAt(filling,n3)|$false),inference(rw,[status(thm)],[90717,1111,theory(equality)])).
% cnf(90724,plain,(n3=n1|happens(overflow,n2)|holdsAt(filling,n3)),inference(cn,[status(thm)],[90723,theory(equality)])).
% cnf(90726,plain,(tapOn=overflow|holdsAt(waterLevel(n3),n2)|n3=n1|holdsAt(filling,n3)),inference(spm,[status(thm)],[90,90724,theory(equality)])).
% cnf(90749,plain,(holdsAt(waterLevel(n3),n2)|n3=n1|holdsAt(filling,n3)),inference(sr,[status(thm)],[90726,126,theory(equality)])).
% cnf(90805,plain,(n3=n1|n3=n2|holdsAt(filling,n3)),inference(spm,[status(thm)],[26243,90749,theory(equality)])).
% cnf(90823,plain,(happens(overflow,n3)|n2=n3|n3=n1|~holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[357,90805,theory(equality)])).
% cnf(90830,plain,(n2=n3|n3=n1|~holdsAt(waterLevel(n3),n3)),inference(sr,[status(thm)],[90823,257,theory(equality)])).
% cnf(121018,plain,(less(n3,n3)|holdsAt(waterLevel(n3),n3)|esk7_3(n0,filling,n3)=n1|esk7_3(n0,filling,n3)=n0|happens(overflow,n2)),inference(spm,[status(thm)],[14862,24120,theory(equality)])).
% cnf(121302,plain,(holdsAt(waterLevel(n3),n3)|esk7_3(n0,filling,n3)=n1|esk7_3(n0,filling,n3)=n0|happens(overflow,n2)),inference(sr,[status(thm)],[121018,304,theory(equality)])).
% cnf(121517,plain,(less(n0,n0)|holdsAt(waterLevel(n3),n3)|esk7_3(n0,filling,n3)=n1|happens(overflow,n2)),inference(spm,[status(thm)],[14861,121302,theory(equality)])).
% cnf(121799,plain,(holdsAt(waterLevel(n3),n3)|esk7_3(n0,filling,n3)=n1|happens(overflow,n2)),inference(sr,[status(thm)],[121517,113,theory(equality)])).
% cnf(122025,plain,(holdsAt(waterLevel(n3),plus(n1,n1))|holdsAt(waterLevel(n3),n3)|happens(overflow,n2)),inference(spm,[status(thm)],[35866,121799,theory(equality)])).
% cnf(122281,plain,(holdsAt(waterLevel(n3),n2)|holdsAt(waterLevel(n3),n3)|happens(overflow,n2)),inference(rw,[status(thm)],[122025,217,theory(equality)])).
% cnf(124277,plain,(tapOn=overflow|holdsAt(waterLevel(n3),n2)|holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[90,122281,theory(equality)])).
% cnf(124327,plain,(holdsAt(waterLevel(n3),n2)|holdsAt(waterLevel(n3),n3)),inference(sr,[status(thm)],[124277,126,theory(equality)])).
% cnf(124841,plain,(n3=n1|n3=n2|holdsAt(waterLevel(n3),n3)),inference(spm,[status(thm)],[26243,124327,theory(equality)])).
% cnf(124851,plain,(n3=n1|n2=n3),inference(csr,[status(thm)],[124841,90830])).
% cnf(124871,plain,(less(n3,n3)|n3=n1),inference(spm,[status(thm)],[453,124851,theory(equality)])).
% cnf(125979,plain,(n3=n1),inference(sr,[status(thm)],[124871,304,theory(equality)])).
% cnf(130044,plain,(less(n1,n1)),inference(rw,[status(thm)],[655,125979,theory(equality)])).
% cnf(130045,plain,($false),inference(sr,[status(thm)],[130044,304,theory(equality)])).
% cnf(130046,plain,($false),130045,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 15294
% # ...of these trivial : 58
% # ...subsumed : 10338
% # ...remaining for further processing: 4898
% # Other redundant clauses eliminated : 2
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 713
% # Backward-rewritten : 2352
% # Generated clauses : 90385
% # ...of the previous two non-trivial : 76698
% # Contextual simplify-reflections : 8028
% # Paramodulations : 90231
% # Factorizations : 107
% # Equation resolutions : 47
% # Current number of processed clauses: 1831
% # Positive orientable unit clauses: 114
% # Positive unorientable unit clauses: 1
% # Negative unit clauses : 44
% # Non-unit-clauses : 1672
% # Current number of unprocessed clauses: 7114
% # ...number of literals in the above : 27612
% # Clause-clause subsumption calls (NU) : 326665
% # Rec. Clause-clause subsumption calls : 104308
% # Unit Clause-clause subsumption calls : 989
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 90
% # Indexed BW rewrite successes : 45
% # Backwards rewriting index: 850 leaves, 2.03+/-2.003 terms/leaf
% # Paramod-from index: 470 leaves, 2.13+/-1.955 terms/leaf
% # Paramod-into index: 680 leaves, 2.08+/-1.833 terms/leaf
% # -------------------------------------------------
% # User time : 5.876 s
% # System time : 0.143 s
% # Total time : 6.019 s
% # Maximum resident set size: 0 pages
% PrfWatch: 7.96 CPU 8.15 WC
% FINAL PrfWatch: 7.96 CPU 8.15 WC
% SZS output end Solution for /tmp/SystemOnTPTP22163/CSR004+1.tptp
%
%------------------------------------------------------------------------------