%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : CSR013+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 : art05.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:45:09 EST 2010
% Result : Theorem 11.22s
% Output : Solution 11.22s
% 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/SystemOnTPTP16249/CSR013+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP16249/CSR013+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP16249/CSR013+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 16345
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% PrfWatch: 1.92 CPU 2.01 WC
% PrfWatch: 3.91 CPU 4.01 WC
% PrfWatch: 5.90 CPU 6.02 WC
% # Preprocessing time : 0.020 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 7.89 CPU 8.02 WC
% PrfWatch: 9.88 CPU 10.03 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,holdsAt(waterLevel(n0),n0),file('/tmp/SRASS.s.p', waterLevel_0)).
% fof(10, axiom,![X3]:![X4]:![X5]:((holdsAt(waterLevel(X4),X3)&holdsAt(waterLevel(X5),X3))=>X4=X5),file('/tmp/SRASS.s.p', same_waterLevel)).
% fof(14, axiom,plus(n0,n2)=n2,file('/tmp/SRASS.s.p', plus0_2)).
% fof(15, axiom,![X7]:![X3]:(happens(X7,X3)<=>((X7=tapOn&X3=n0)|((holdsAt(waterLevel(n3),X3)&holdsAt(filling,X3))&X7=overflow))),file('/tmp/SRASS.s.p', happens_all_defn)).
% fof(16, axiom,![X4]:![X3]:![X5]:![X9]:((holdsAt(waterLevel(X4),X3)&X5=plus(X4,X9))=>trajectory(filling,X3,waterLevel(X5),X9)),file('/tmp/SRASS.s.p', change_of_waterLevel)).
% fof(17, axiom,~(?[X2]:less(X2,n0)),file('/tmp/SRASS.s.p', less0)).
% fof(22, axiom,~(overflow=tapOn),file('/tmp/SRASS.s.p', overflow_not_tapOn)).
% fof(23, axiom,![X2]:![X8]:plus(X2,X8)=plus(X8,X2),file('/tmp/SRASS.s.p', symmetry_of_plus)).
% fof(24, axiom,![X10]:![X6]:![X12]:(stoppedIn(X10,X6,X12)<=>?[X7]:?[X3]:(((happens(X7,X3)&less(X10,X3))&less(X3,X12))&terminates(X7,X6,X3))),file('/tmp/SRASS.s.p', stoppedin_defn)).
% fof(25, axiom,![X7]:![X6]:![X3]:(initiates(X7,X6,X3)<=>((((X7=tapOn&X6=filling)|(X7=overflow&X6=spilling))|?[X1]:((holdsAt(waterLevel(X1),X3)&X7=tapOff)&X6=waterLevel(X1)))|?[X1]:((holdsAt(waterLevel(X1),X3)&X7=overflow)&X6=waterLevel(X1)))),file('/tmp/SRASS.s.p', initiates_all_defn)).
% fof(27, axiom,![X7]:![X6]:![X3]:(terminates(X7,X6,X3)<=>((X7=tapOff&X6=filling)|(X7=overflow&X6=filling))),file('/tmp/SRASS.s.p', terminates_all_defn)).
% fof(29, axiom,![X7]:![X3]:![X6]:((happens(X7,X3)&initiates(X7,X6,X3))=>holdsAt(X6,plus(X3,n1))),file('/tmp/SRASS.s.p', happens_holds)).
% fof(32, axiom,![X7]:![X3]:![X6]:![X13]:![X9]:(((((happens(X7,X3)&initiates(X7,X6,X3))&less(n0,X9))&trajectory(X6,X3,X13,X9))&~(stoppedIn(X3,X6,plus(X3,X9))))=>holdsAt(X13,plus(X3,X9))),file('/tmp/SRASS.s.p', change_holding)).
% fof(33, axiom,plus(n0,n1)=n1,file('/tmp/SRASS.s.p', plus0_1)).
% fof(34, axiom,plus(n1,n1)=n2,file('/tmp/SRASS.s.p', plus1_1)).
% fof(38, axiom,~(tapOff=tapOn),file('/tmp/SRASS.s.p', tapOff_not_tapOn)).
% fof(39, axiom,~(tapOff=overflow),file('/tmp/SRASS.s.p', tapOff_not_overflow)).
% fof(40, axiom,![X2]:![X8]:(less(X2,X8)<=>(~(less(X8,X2))&~(X8=X2))),file('/tmp/SRASS.s.p', less_property)).
% fof(41, axiom,![X2]:(less(X2,n2)<=>less_or_equal(X2,n1)),file('/tmp/SRASS.s.p', less2)).
% fof(43, axiom,![X2]:(less(X2,n3)<=>less_or_equal(X2,n2)),file('/tmp/SRASS.s.p', less3)).
% fof(45, axiom,![X2]:(less(X2,n1)<=>less_or_equal(X2,n0)),file('/tmp/SRASS.s.p', less1)).
% fof(47, axiom,![X2]:![X8]:(less_or_equal(X2,X8)<=>(less(X2,X8)|X2=X8)),file('/tmp/SRASS.s.p', less_or_equal)).
% fof(55, conjecture,~(?[X7]:(happens(X7,n2)&terminates(X7,filling,n2))),file('/tmp/SRASS.s.p', nothing_terminates_filling_2)).
% fof(56, negated_conjecture,~(~(?[X7]:(happens(X7,n2)&terminates(X7,filling,n2)))),inference(assume_negation,[status(cth)],[55])).
% fof(68, plain,![X7]:![X3]:![X6]:![X13]:![X9]:(((((happens(X7,X3)&initiates(X7,X6,X3))&less(n0,X9))&trajectory(X6,X3,X13,X9))&~(stoppedIn(X3,X6,plus(X3,X9))))=>holdsAt(X13,plus(X3,X9))),inference(fof_simplification,[status(thm)],[32,theory(equality)])).
% fof(69, plain,![X2]:![X8]:(less(X2,X8)<=>(~(less(X8,X2))&~(X8=X2))),inference(fof_simplification,[status(thm)],[40,theory(equality)])).
% fof(70, plain,![X3]:![X7]:![X6]:(epred1_3(X6,X7,X3)<=>((((X7=tapOn&X6=filling)|(X7=overflow&X6=spilling))|?[X1]:((holdsAt(waterLevel(X1),X3)&X7=tapOff)&X6=waterLevel(X1)))|?[X1]:((holdsAt(waterLevel(X1),X3)&X7=overflow)&X6=waterLevel(X1)))),introduced(definition)).
% fof(71, plain,![X7]:![X6]:![X3]:(initiates(X7,X6,X3)<=>epred1_3(X6,X7,X3)),inference(apply_def,[status(esa)],[25,70,theory(equality)])).
% cnf(72,plain,(holdsAt(waterLevel(n0),n0)),inference(split_conjunct,[status(thm)],[1])).
% fof(84, plain,![X3]:![X4]:![X5]:((~(holdsAt(waterLevel(X4),X3))|~(holdsAt(waterLevel(X5),X3)))|X4=X5),inference(fof_nnf,[status(thm)],[10])).
% fof(85, plain,![X6]:![X7]:![X8]:((~(holdsAt(waterLevel(X7),X6))|~(holdsAt(waterLevel(X8),X6)))|X7=X8),inference(variable_rename,[status(thm)],[84])).
% cnf(86,plain,(X1=X2|~holdsAt(waterLevel(X2),X3)|~holdsAt(waterLevel(X1),X3)),inference(split_conjunct,[status(thm)],[85])).
% cnf(100,plain,(plus(n0,n2)=n2),inference(split_conjunct,[status(thm)],[14])).
% fof(101, plain,![X7]:![X3]:((~(happens(X7,X3))|((X7=tapOn&X3=n0)|((holdsAt(waterLevel(n3),X3)&holdsAt(filling,X3))&X7=overflow)))&(((~(X7=tapOn)|~(X3=n0))&((~(holdsAt(waterLevel(n3),X3))|~(holdsAt(filling,X3)))|~(X7=overflow)))|happens(X7,X3))),inference(fof_nnf,[status(thm)],[15])).
% fof(102, plain,![X8]:![X9]:((~(happens(X8,X9))|((X8=tapOn&X9=n0)|((holdsAt(waterLevel(n3),X9)&holdsAt(filling,X9))&X8=overflow)))&(((~(X8=tapOn)|~(X9=n0))&((~(holdsAt(waterLevel(n3),X9))|~(holdsAt(filling,X9)))|~(X8=overflow)))|happens(X8,X9))),inference(variable_rename,[status(thm)],[101])).
% fof(103, plain,![X8]:![X9]:((((((holdsAt(waterLevel(n3),X9)|X8=tapOn)|~(happens(X8,X9)))&((holdsAt(filling,X9)|X8=tapOn)|~(happens(X8,X9))))&((X8=overflow|X8=tapOn)|~(happens(X8,X9))))&((((holdsAt(waterLevel(n3),X9)|X9=n0)|~(happens(X8,X9)))&((holdsAt(filling,X9)|X9=n0)|~(happens(X8,X9))))&((X8=overflow|X9=n0)|~(happens(X8,X9)))))&(((~(X8=tapOn)|~(X9=n0))|happens(X8,X9))&(((~(holdsAt(waterLevel(n3),X9))|~(holdsAt(filling,X9)))|~(X8=overflow))|happens(X8,X9)))),inference(distribute,[status(thm)],[102])).
% cnf(105,plain,(happens(X1,X2)|X2!=n0|X1!=tapOn),inference(split_conjunct,[status(thm)],[103])).
% cnf(109,plain,(X1=tapOn|X1=overflow|~happens(X1,X2)),inference(split_conjunct,[status(thm)],[103])).
% cnf(111,plain,(X1=tapOn|holdsAt(waterLevel(n3),X2)|~happens(X1,X2)),inference(split_conjunct,[status(thm)],[103])).
% fof(112, plain,![X4]:![X3]:![X5]:![X9]:((~(holdsAt(waterLevel(X4),X3))|~(X5=plus(X4,X9)))|trajectory(filling,X3,waterLevel(X5),X9)),inference(fof_nnf,[status(thm)],[16])).
% fof(113, plain,![X10]:![X11]:![X12]:![X13]:((~(holdsAt(waterLevel(X10),X11))|~(X12=plus(X10,X13)))|trajectory(filling,X11,waterLevel(X12),X13)),inference(variable_rename,[status(thm)],[112])).
% cnf(114,plain,(trajectory(filling,X1,waterLevel(X2),X3)|X2!=plus(X4,X3)|~holdsAt(waterLevel(X4),X1)),inference(split_conjunct,[status(thm)],[113])).
% fof(115, plain,![X2]:~(less(X2,n0)),inference(fof_nnf,[status(thm)],[17])).
% fof(116, plain,![X3]:~(less(X3,n0)),inference(variable_rename,[status(thm)],[115])).
% cnf(117,plain,(~less(X1,n0)),inference(split_conjunct,[status(thm)],[116])).
% cnf(138,plain,(overflow!=tapOn),inference(split_conjunct,[status(thm)],[22])).
% fof(139, plain,![X9]:![X10]:plus(X9,X10)=plus(X10,X9),inference(variable_rename,[status(thm)],[23])).
% cnf(140,plain,(plus(X1,X2)=plus(X2,X1)),inference(split_conjunct,[status(thm)],[139])).
% fof(141, plain,![X10]:![X6]:![X12]:((~(stoppedIn(X10,X6,X12))|?[X7]:?[X3]:(((happens(X7,X3)&less(X10,X3))&less(X3,X12))&terminates(X7,X6,X3)))&(![X7]:![X3]:(((~(happens(X7,X3))|~(less(X10,X3)))|~(less(X3,X12)))|~(terminates(X7,X6,X3)))|stoppedIn(X10,X6,X12))),inference(fof_nnf,[status(thm)],[24])).
% fof(142, plain,![X13]:![X14]:![X15]:((~(stoppedIn(X13,X14,X15))|?[X16]:?[X17]:(((happens(X16,X17)&less(X13,X17))&less(X17,X15))&terminates(X16,X14,X17)))&(![X18]:![X19]:(((~(happens(X18,X19))|~(less(X13,X19)))|~(less(X19,X15)))|~(terminates(X18,X14,X19)))|stoppedIn(X13,X14,X15))),inference(variable_rename,[status(thm)],[141])).
% fof(143, plain,![X13]:![X14]:![X15]:((~(stoppedIn(X13,X14,X15))|(((happens(esk4_3(X13,X14,X15),esk5_3(X13,X14,X15))&less(X13,esk5_3(X13,X14,X15)))&less(esk5_3(X13,X14,X15),X15))&terminates(esk4_3(X13,X14,X15),X14,esk5_3(X13,X14,X15))))&(![X18]:![X19]:(((~(happens(X18,X19))|~(less(X13,X19)))|~(less(X19,X15)))|~(terminates(X18,X14,X19)))|stoppedIn(X13,X14,X15))),inference(skolemize,[status(esa)],[142])).
% fof(144, plain,![X13]:![X14]:![X15]:![X18]:![X19]:(((((~(happens(X18,X19))|~(less(X13,X19)))|~(less(X19,X15)))|~(terminates(X18,X14,X19)))|stoppedIn(X13,X14,X15))&(~(stoppedIn(X13,X14,X15))|(((happens(esk4_3(X13,X14,X15),esk5_3(X13,X14,X15))&less(X13,esk5_3(X13,X14,X15)))&less(esk5_3(X13,X14,X15),X15))&terminates(esk4_3(X13,X14,X15),X14,esk5_3(X13,X14,X15))))),inference(shift_quantors,[status(thm)],[143])).
% fof(145, plain,![X13]:![X14]:![X15]:![X18]:![X19]:(((((~(happens(X18,X19))|~(less(X13,X19)))|~(less(X19,X15)))|~(terminates(X18,X14,X19)))|stoppedIn(X13,X14,X15))&((((happens(esk4_3(X13,X14,X15),esk5_3(X13,X14,X15))|~(stoppedIn(X13,X14,X15)))&(less(X13,esk5_3(X13,X14,X15))|~(stoppedIn(X13,X14,X15))))&(less(esk5_3(X13,X14,X15),X15)|~(stoppedIn(X13,X14,X15))))&(terminates(esk4_3(X13,X14,X15),X14,esk5_3(X13,X14,X15))|~(stoppedIn(X13,X14,X15))))),inference(distribute,[status(thm)],[144])).
% cnf(146,plain,(terminates(esk4_3(X1,X2,X3),X2,esk5_3(X1,X2,X3))|~stoppedIn(X1,X2,X3)),inference(split_conjunct,[status(thm)],[145])).
% cnf(147,plain,(less(esk5_3(X1,X2,X3),X3)|~stoppedIn(X1,X2,X3)),inference(split_conjunct,[status(thm)],[145])).
% cnf(148,plain,(less(X1,esk5_3(X1,X2,X3))|~stoppedIn(X1,X2,X3)),inference(split_conjunct,[status(thm)],[145])).
% cnf(149,plain,(happens(esk4_3(X1,X2,X3),esk5_3(X1,X2,X3))|~stoppedIn(X1,X2,X3)),inference(split_conjunct,[status(thm)],[145])).
% fof(151, plain,![X7]:![X6]:![X3]:((~(initiates(X7,X6,X3))|epred1_3(X6,X7,X3))&(~(epred1_3(X6,X7,X3))|initiates(X7,X6,X3))),inference(fof_nnf,[status(thm)],[71])).
% fof(152, plain,![X8]:![X9]:![X10]:((~(initiates(X8,X9,X10))|epred1_3(X9,X8,X10))&(~(epred1_3(X9,X8,X10))|initiates(X8,X9,X10))),inference(variable_rename,[status(thm)],[151])).
% cnf(153,plain,(initiates(X1,X2,X3)|~epred1_3(X2,X1,X3)),inference(split_conjunct,[status(thm)],[152])).
% fof(156, plain,![X7]:![X6]:![X3]:((~(terminates(X7,X6,X3))|((X7=tapOff&X6=filling)|(X7=overflow&X6=filling)))&(((~(X7=tapOff)|~(X6=filling))&(~(X7=overflow)|~(X6=filling)))|terminates(X7,X6,X3))),inference(fof_nnf,[status(thm)],[27])).
% fof(157, plain,![X8]:![X9]:![X10]:((~(terminates(X8,X9,X10))|((X8=tapOff&X9=filling)|(X8=overflow&X9=filling)))&(((~(X8=tapOff)|~(X9=filling))&(~(X8=overflow)|~(X9=filling)))|terminates(X8,X9,X10))),inference(variable_rename,[status(thm)],[156])).
% fof(158, plain,![X8]:![X9]:![X10]:(((((X8=overflow|X8=tapOff)|~(terminates(X8,X9,X10)))&((X9=filling|X8=tapOff)|~(terminates(X8,X9,X10))))&(((X8=overflow|X9=filling)|~(terminates(X8,X9,X10)))&((X9=filling|X9=filling)|~(terminates(X8,X9,X10)))))&(((~(X8=tapOff)|~(X9=filling))|terminates(X8,X9,X10))&((~(X8=overflow)|~(X9=filling))|terminates(X8,X9,X10)))),inference(distribute,[status(thm)],[157])).
% cnf(164,plain,(X1=tapOff|X1=overflow|~terminates(X1,X2,X3)),inference(split_conjunct,[status(thm)],[158])).
% fof(171, plain,![X7]:![X3]:![X6]:((~(happens(X7,X3))|~(initiates(X7,X6,X3)))|holdsAt(X6,plus(X3,n1))),inference(fof_nnf,[status(thm)],[29])).
% fof(172, plain,![X8]:![X9]:![X10]:((~(happens(X8,X9))|~(initiates(X8,X10,X9)))|holdsAt(X10,plus(X9,n1))),inference(variable_rename,[status(thm)],[171])).
% cnf(173,plain,(holdsAt(X1,plus(X2,n1))|~initiates(X3,X1,X2)|~happens(X3,X2)),inference(split_conjunct,[status(thm)],[172])).
% fof(187, plain,![X7]:![X3]:![X6]:![X13]:![X9]:(((((~(happens(X7,X3))|~(initiates(X7,X6,X3)))|~(less(n0,X9)))|~(trajectory(X6,X3,X13,X9)))|stoppedIn(X3,X6,plus(X3,X9)))|holdsAt(X13,plus(X3,X9))),inference(fof_nnf,[status(thm)],[68])).
% fof(188, plain,![X14]:![X15]:![X16]:![X17]:![X18]:(((((~(happens(X14,X15))|~(initiates(X14,X16,X15)))|~(less(n0,X18)))|~(trajectory(X16,X15,X17,X18)))|stoppedIn(X15,X16,plus(X15,X18)))|holdsAt(X17,plus(X15,X18))),inference(variable_rename,[status(thm)],[187])).
% cnf(189,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)],[188])).
% cnf(190,plain,(plus(n0,n1)=n1),inference(split_conjunct,[status(thm)],[33])).
% cnf(191,plain,(plus(n1,n1)=n2),inference(split_conjunct,[status(thm)],[34])).
% cnf(202,plain,(tapOff!=tapOn),inference(split_conjunct,[status(thm)],[38])).
% cnf(203,plain,(tapOff!=overflow),inference(split_conjunct,[status(thm)],[39])).
% fof(204, plain,![X2]:![X8]:((~(less(X2,X8))|(~(less(X8,X2))&~(X8=X2)))&((less(X8,X2)|X8=X2)|less(X2,X8))),inference(fof_nnf,[status(thm)],[69])).
% fof(205, plain,![X9]:![X10]:((~(less(X9,X10))|(~(less(X10,X9))&~(X10=X9)))&((less(X10,X9)|X10=X9)|less(X9,X10))),inference(variable_rename,[status(thm)],[204])).
% fof(206, plain,![X9]:![X10]:(((~(less(X10,X9))|~(less(X9,X10)))&(~(X10=X9)|~(less(X9,X10))))&((less(X10,X9)|X10=X9)|less(X9,X10))),inference(distribute,[status(thm)],[205])).
% cnf(207,plain,(less(X1,X2)|X2=X1|less(X2,X1)),inference(split_conjunct,[status(thm)],[206])).
% cnf(208,plain,(~less(X1,X2)|X2!=X1),inference(split_conjunct,[status(thm)],[206])).
% cnf(209,plain,(~less(X1,X2)|~less(X2,X1)),inference(split_conjunct,[status(thm)],[206])).
% fof(210, plain,![X2]:((~(less(X2,n2))|less_or_equal(X2,n1))&(~(less_or_equal(X2,n1))|less(X2,n2))),inference(fof_nnf,[status(thm)],[41])).
% fof(211, plain,![X3]:((~(less(X3,n2))|less_or_equal(X3,n1))&(~(less_or_equal(X3,n1))|less(X3,n2))),inference(variable_rename,[status(thm)],[210])).
% cnf(212,plain,(less(X1,n2)|~less_or_equal(X1,n1)),inference(split_conjunct,[status(thm)],[211])).
% cnf(213,plain,(less_or_equal(X1,n1)|~less(X1,n2)),inference(split_conjunct,[status(thm)],[211])).
% fof(215, plain,![X2]:((~(less(X2,n3))|less_or_equal(X2,n2))&(~(less_or_equal(X2,n2))|less(X2,n3))),inference(fof_nnf,[status(thm)],[43])).
% fof(216, plain,![X3]:((~(less(X3,n3))|less_or_equal(X3,n2))&(~(less_or_equal(X3,n2))|less(X3,n3))),inference(variable_rename,[status(thm)],[215])).
% cnf(217,plain,(less(X1,n3)|~less_or_equal(X1,n2)),inference(split_conjunct,[status(thm)],[216])).
% fof(220, plain,![X2]:((~(less(X2,n1))|less_or_equal(X2,n0))&(~(less_or_equal(X2,n0))|less(X2,n1))),inference(fof_nnf,[status(thm)],[45])).
% fof(221, plain,![X3]:((~(less(X3,n1))|less_or_equal(X3,n0))&(~(less_or_equal(X3,n0))|less(X3,n1))),inference(variable_rename,[status(thm)],[220])).
% cnf(222,plain,(less(X1,n1)|~less_or_equal(X1,n0)),inference(split_conjunct,[status(thm)],[221])).
% cnf(223,plain,(less_or_equal(X1,n0)|~less(X1,n1)),inference(split_conjunct,[status(thm)],[221])).
% fof(225, plain,![X2]:![X8]:((~(less_or_equal(X2,X8))|(less(X2,X8)|X2=X8))&((~(less(X2,X8))&~(X2=X8))|less_or_equal(X2,X8))),inference(fof_nnf,[status(thm)],[47])).
% fof(226, plain,![X9]:![X10]:((~(less_or_equal(X9,X10))|(less(X9,X10)|X9=X10))&((~(less(X9,X10))&~(X9=X10))|less_or_equal(X9,X10))),inference(variable_rename,[status(thm)],[225])).
% fof(227, plain,![X9]:![X10]:((~(less_or_equal(X9,X10))|(less(X9,X10)|X9=X10))&((~(less(X9,X10))|less_or_equal(X9,X10))&(~(X9=X10)|less_or_equal(X9,X10)))),inference(distribute,[status(thm)],[226])).
% cnf(228,plain,(less_or_equal(X1,X2)|X1!=X2),inference(split_conjunct,[status(thm)],[227])).
% cnf(229,plain,(less_or_equal(X1,X2)|~less(X1,X2)),inference(split_conjunct,[status(thm)],[227])).
% cnf(230,plain,(X1=X2|less(X1,X2)|~less_or_equal(X1,X2)),inference(split_conjunct,[status(thm)],[227])).
% fof(256, negated_conjecture,?[X7]:(happens(X7,n2)&terminates(X7,filling,n2)),inference(fof_nnf,[status(thm)],[56])).
% fof(257, negated_conjecture,?[X8]:(happens(X8,n2)&terminates(X8,filling,n2)),inference(variable_rename,[status(thm)],[256])).
% fof(258, negated_conjecture,(happens(esk10_0,n2)&terminates(esk10_0,filling,n2)),inference(skolemize,[status(esa)],[257])).
% cnf(259,negated_conjecture,(terminates(esk10_0,filling,n2)),inference(split_conjunct,[status(thm)],[258])).
% cnf(260,negated_conjecture,(happens(esk10_0,n2)),inference(split_conjunct,[status(thm)],[258])).
% fof(261, plain,![X3]:![X7]:![X6]:((~(epred1_3(X6,X7,X3))|((((X7=tapOn&X6=filling)|(X7=overflow&X6=spilling))|?[X1]:((holdsAt(waterLevel(X1),X3)&X7=tapOff)&X6=waterLevel(X1)))|?[X1]:((holdsAt(waterLevel(X1),X3)&X7=overflow)&X6=waterLevel(X1))))&(((((~(X7=tapOn)|~(X6=filling))&(~(X7=overflow)|~(X6=spilling)))&![X1]:((~(holdsAt(waterLevel(X1),X3))|~(X7=tapOff))|~(X6=waterLevel(X1))))&![X1]:((~(holdsAt(waterLevel(X1),X3))|~(X7=overflow))|~(X6=waterLevel(X1))))|epred1_3(X6,X7,X3))),inference(fof_nnf,[status(thm)],[70])).
% fof(262, plain,![X8]:![X9]:![X10]:((~(epred1_3(X10,X9,X8))|((((X9=tapOn&X10=filling)|(X9=overflow&X10=spilling))|?[X11]:((holdsAt(waterLevel(X11),X8)&X9=tapOff)&X10=waterLevel(X11)))|?[X12]:((holdsAt(waterLevel(X12),X8)&X9=overflow)&X10=waterLevel(X12))))&(((((~(X9=tapOn)|~(X10=filling))&(~(X9=overflow)|~(X10=spilling)))&![X13]:((~(holdsAt(waterLevel(X13),X8))|~(X9=tapOff))|~(X10=waterLevel(X13))))&![X14]:((~(holdsAt(waterLevel(X14),X8))|~(X9=overflow))|~(X10=waterLevel(X14))))|epred1_3(X10,X9,X8))),inference(variable_rename,[status(thm)],[261])).
% fof(263, plain,![X8]:![X9]:![X10]:((~(epred1_3(X10,X9,X8))|((((X9=tapOn&X10=filling)|(X9=overflow&X10=spilling))|((holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)&X9=tapOff)&X10=waterLevel(esk11_3(X8,X9,X10))))|((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)&X9=overflow)&X10=waterLevel(esk12_3(X8,X9,X10)))))&(((((~(X9=tapOn)|~(X10=filling))&(~(X9=overflow)|~(X10=spilling)))&![X13]:((~(holdsAt(waterLevel(X13),X8))|~(X9=tapOff))|~(X10=waterLevel(X13))))&![X14]:((~(holdsAt(waterLevel(X14),X8))|~(X9=overflow))|~(X10=waterLevel(X14))))|epred1_3(X10,X9,X8))),inference(skolemize,[status(esa)],[262])).
% fof(264, plain,![X8]:![X9]:![X10]:![X13]:![X14]:(((((~(holdsAt(waterLevel(X14),X8))|~(X9=overflow))|~(X10=waterLevel(X14)))&(((~(holdsAt(waterLevel(X13),X8))|~(X9=tapOff))|~(X10=waterLevel(X13)))&((~(X9=tapOn)|~(X10=filling))&(~(X9=overflow)|~(X10=spilling)))))|epred1_3(X10,X9,X8))&(~(epred1_3(X10,X9,X8))|((((X9=tapOn&X10=filling)|(X9=overflow&X10=spilling))|((holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)&X9=tapOff)&X10=waterLevel(esk11_3(X8,X9,X10))))|((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)&X9=overflow)&X10=waterLevel(esk12_3(X8,X9,X10)))))),inference(shift_quantors,[status(thm)],[263])).
% fof(265, plain,![X8]:![X9]:![X10]:![X13]:![X14]:(((((~(holdsAt(waterLevel(X14),X8))|~(X9=overflow))|~(X10=waterLevel(X14)))|epred1_3(X10,X9,X8))&((((~(holdsAt(waterLevel(X13),X8))|~(X9=tapOff))|~(X10=waterLevel(X13)))|epred1_3(X10,X9,X8))&(((~(X9=tapOn)|~(X10=filling))|epred1_3(X10,X9,X8))&((~(X9=overflow)|~(X10=spilling))|epred1_3(X10,X9,X8)))))&((((((((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)|(holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)|(X9=overflow|X9=tapOn)))|~(epred1_3(X10,X9,X8)))&((X9=overflow|(holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)|(X9=overflow|X9=tapOn)))|~(epred1_3(X10,X9,X8))))&((X10=waterLevel(esk12_3(X8,X9,X10))|(holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)|(X9=overflow|X9=tapOn)))|~(epred1_3(X10,X9,X8))))&((((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)|(X9=tapOff|(X9=overflow|X9=tapOn)))|~(epred1_3(X10,X9,X8)))&((X9=overflow|(X9=tapOff|(X9=overflow|X9=tapOn)))|~(epred1_3(X10,X9,X8))))&((X10=waterLevel(esk12_3(X8,X9,X10))|(X9=tapOff|(X9=overflow|X9=tapOn)))|~(epred1_3(X10,X9,X8)))))&((((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)|(X10=waterLevel(esk11_3(X8,X9,X10))|(X9=overflow|X9=tapOn)))|~(epred1_3(X10,X9,X8)))&((X9=overflow|(X10=waterLevel(esk11_3(X8,X9,X10))|(X9=overflow|X9=tapOn)))|~(epred1_3(X10,X9,X8))))&((X10=waterLevel(esk12_3(X8,X9,X10))|(X10=waterLevel(esk11_3(X8,X9,X10))|(X9=overflow|X9=tapOn)))|~(epred1_3(X10,X9,X8)))))&((((((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)|(holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)|(X10=spilling|X9=tapOn)))|~(epred1_3(X10,X9,X8)))&((X9=overflow|(holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)|(X10=spilling|X9=tapOn)))|~(epred1_3(X10,X9,X8))))&((X10=waterLevel(esk12_3(X8,X9,X10))|(holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)|(X10=spilling|X9=tapOn)))|~(epred1_3(X10,X9,X8))))&((((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)|(X9=tapOff|(X10=spilling|X9=tapOn)))|~(epred1_3(X10,X9,X8)))&((X9=overflow|(X9=tapOff|(X10=spilling|X9=tapOn)))|~(epred1_3(X10,X9,X8))))&((X10=waterLevel(esk12_3(X8,X9,X10))|(X9=tapOff|(X10=spilling|X9=tapOn)))|~(epred1_3(X10,X9,X8)))))&((((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)|(X10=waterLevel(esk11_3(X8,X9,X10))|(X10=spilling|X9=tapOn)))|~(epred1_3(X10,X9,X8)))&((X9=overflow|(X10=waterLevel(esk11_3(X8,X9,X10))|(X10=spilling|X9=tapOn)))|~(epred1_3(X10,X9,X8))))&((X10=waterLevel(esk12_3(X8,X9,X10))|(X10=waterLevel(esk11_3(X8,X9,X10))|(X10=spilling|X9=tapOn)))|~(epred1_3(X10,X9,X8))))))&(((((((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)|(holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)|(X9=overflow|X10=filling)))|~(epred1_3(X10,X9,X8)))&((X9=overflow|(holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)|(X9=overflow|X10=filling)))|~(epred1_3(X10,X9,X8))))&((X10=waterLevel(esk12_3(X8,X9,X10))|(holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)|(X9=overflow|X10=filling)))|~(epred1_3(X10,X9,X8))))&((((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)|(X9=tapOff|(X9=overflow|X10=filling)))|~(epred1_3(X10,X9,X8)))&((X9=overflow|(X9=tapOff|(X9=overflow|X10=filling)))|~(epred1_3(X10,X9,X8))))&((X10=waterLevel(esk12_3(X8,X9,X10))|(X9=tapOff|(X9=overflow|X10=filling)))|~(epred1_3(X10,X9,X8)))))&((((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)|(X10=waterLevel(esk11_3(X8,X9,X10))|(X9=overflow|X10=filling)))|~(epred1_3(X10,X9,X8)))&((X9=overflow|(X10=waterLevel(esk11_3(X8,X9,X10))|(X9=overflow|X10=filling)))|~(epred1_3(X10,X9,X8))))&((X10=waterLevel(esk12_3(X8,X9,X10))|(X10=waterLevel(esk11_3(X8,X9,X10))|(X9=overflow|X10=filling)))|~(epred1_3(X10,X9,X8)))))&((((((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)|(holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)|(X10=spilling|X10=filling)))|~(epred1_3(X10,X9,X8)))&((X9=overflow|(holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)|(X10=spilling|X10=filling)))|~(epred1_3(X10,X9,X8))))&((X10=waterLevel(esk12_3(X8,X9,X10))|(holdsAt(waterLevel(esk11_3(X8,X9,X10)),X8)|(X10=spilling|X10=filling)))|~(epred1_3(X10,X9,X8))))&((((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)|(X9=tapOff|(X10=spilling|X10=filling)))|~(epred1_3(X10,X9,X8)))&((X9=overflow|(X9=tapOff|(X10=spilling|X10=filling)))|~(epred1_3(X10,X9,X8))))&((X10=waterLevel(esk12_3(X8,X9,X10))|(X9=tapOff|(X10=spilling|X10=filling)))|~(epred1_3(X10,X9,X8)))))&((((holdsAt(waterLevel(esk12_3(X8,X9,X10)),X8)|(X10=waterLevel(esk11_3(X8,X9,X10))|(X10=spilling|X10=filling)))|~(epred1_3(X10,X9,X8)))&((X9=overflow|(X10=waterLevel(esk11_3(X8,X9,X10))|(X10=spilling|X10=filling)))|~(epred1_3(X10,X9,X8))))&((X10=waterLevel(esk12_3(X8,X9,X10))|(X10=waterLevel(esk11_3(X8,X9,X10))|(X10=spilling|X10=filling)))|~(epred1_3(X10,X9,X8)))))))),inference(distribute,[status(thm)],[264])).
% cnf(303,plain,(epred1_3(X1,X2,X3)|X1!=filling|X2!=tapOn),inference(split_conjunct,[status(thm)],[265])).
% cnf(305,plain,(epred1_3(X1,X2,X3)|X1!=waterLevel(X4)|X2!=overflow|~holdsAt(waterLevel(X4),X3)),inference(split_conjunct,[status(thm)],[265])).
% cnf(306,plain,(less_or_equal(X1,X1)),inference(er,[status(thm)],[228,theory(equality)])).
% cnf(307,plain,(~less(X1,X1)),inference(er,[status(thm)],[208,theory(equality)])).
% cnf(317,plain,(plus(n1,n0)=n1),inference(rw,[status(thm)],[190,140,theory(equality)])).
% cnf(327,plain,(happens(X1,n0)|tapOn!=X1),inference(er,[status(thm)],[105,theory(equality)])).
% cnf(329,negated_conjecture,(overflow=esk10_0|tapOn=esk10_0),inference(spm,[status(thm)],[109,260,theory(equality)])).
% cnf(342,negated_conjecture,(tapOff=esk10_0|overflow=esk10_0),inference(spm,[status(thm)],[164,259,theory(equality)])).
% cnf(349,plain,(epred1_3(filling,X1,X2)|tapOn!=X1),inference(er,[status(thm)],[303,theory(equality)])).
% cnf(350,plain,(less_or_equal(X1,n0)|X1=n1|less(n1,X1)),inference(spm,[status(thm)],[223,207,theory(equality)])).
% cnf(381,plain,(epred1_3(X1,overflow,X2)|waterLevel(X3)!=X1|~holdsAt(waterLevel(X3),X2)),inference(er,[status(thm)],[305,theory(equality)])).
% cnf(395,plain,(trajectory(filling,X1,waterLevel(plus(X2,X3)),X3)|~holdsAt(waterLevel(X2),X1)),inference(er,[status(thm)],[114,theory(equality)])).
% cnf(462,negated_conjecture,(tapOff=tapOn|tapOff=overflow|esk10_0=overflow),inference(spm,[status(thm)],[329,342,theory(equality)])).
% cnf(464,negated_conjecture,(tapOff=overflow|esk10_0=overflow),inference(sr,[status(thm)],[462,202,theory(equality)])).
% cnf(465,negated_conjecture,(esk10_0=overflow),inference(sr,[status(thm)],[464,203,theory(equality)])).
% cnf(472,negated_conjecture,(happens(overflow,n2)),inference(rw,[status(thm)],[260,465,theory(equality)])).
% cnf(474,negated_conjecture,(tapOn=overflow|holdsAt(waterLevel(n3),n2)),inference(spm,[status(thm)],[111,472,theory(equality)])).
% cnf(478,negated_conjecture,(holdsAt(waterLevel(n3),n2)),inference(sr,[status(thm)],[474,138,theory(equality)])).
% cnf(491,plain,(less(n2,n3)),inference(spm,[status(thm)],[217,306,theory(equality)])).
% cnf(492,plain,(less(n1,n2)),inference(spm,[status(thm)],[212,306,theory(equality)])).
% cnf(493,plain,(less(n0,n1)),inference(spm,[status(thm)],[222,306,theory(equality)])).
% cnf(502,plain,(happens(tapOn,n0)),inference(er,[status(thm)],[327,theory(equality)])).
% cnf(505,negated_conjecture,(X1=n3|~holdsAt(waterLevel(X1),n2)),inference(spm,[status(thm)],[86,478,theory(equality)])).
% cnf(515,plain,(less_or_equal(n1,n2)),inference(spm,[status(thm)],[229,492,theory(equality)])).
% cnf(535,plain,(less(n1,n3)),inference(spm,[status(thm)],[217,515,theory(equality)])).
% cnf(657,plain,(less_or_equal(n0,n1)),inference(spm,[status(thm)],[229,493,theory(equality)])).
% cnf(661,plain,(stoppedIn(X1,X2,plus(X1,n1))|holdsAt(X3,plus(X1,n1))|~initiates(X4,X2,X1)|~trajectory(X2,X1,X3,n1)|~happens(X4,X1)),inference(spm,[status(thm)],[189,493,theory(equality)])).
% cnf(728,plain,(less(n0,n2)),inference(spm,[status(thm)],[212,657,theory(equality)])).
% cnf(734,plain,(stoppedIn(X1,X2,plus(X1,n2))|holdsAt(X3,plus(X1,n2))|~initiates(X4,X2,X1)|~trajectory(X2,X1,X3,n2)|~happens(X4,X1)),inference(spm,[status(thm)],[189,728,theory(equality)])).
% cnf(762,plain,(epred1_3(filling,tapOn,X1)),inference(er,[status(thm)],[349,theory(equality)])).
% cnf(789,plain,(X1=n0|less(X1,n0)|X1=n1|less(n1,X1)),inference(spm,[status(thm)],[230,350,theory(equality)])).
% cnf(791,plain,(X1=n0|X1=n1|less(n1,X1)),inference(sr,[status(thm)],[789,117,theory(equality)])).
% cnf(1127,plain,(X1=n1|X1=n0|~less(X1,n1)),inference(spm,[status(thm)],[209,791,theory(equality)])).
% cnf(1151,plain,(initiates(tapOn,filling,X1)),inference(spm,[status(thm)],[153,762,theory(equality)])).
% cnf(1703,plain,(epred1_3(waterLevel(X1),overflow,X2)|~holdsAt(waterLevel(X1),X2)),inference(er,[status(thm)],[381,theory(equality)])).
% cnf(2621,plain,(trajectory(filling,n0,waterLevel(plus(n0,X1)),X1)),inference(spm,[status(thm)],[395,72,theory(equality)])).
% cnf(6321,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)],[661,2621,theory(equality)])).
% cnf(6331,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)],[6321,140,theory(equality)]),317,theory(equality)])).
% cnf(6332,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)],[6331,140,theory(equality)]),317,theory(equality)]),140,theory(equality)]),317,theory(equality)])).
% cnf(6423,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)],[734,2621,theory(equality)])).
% cnf(6438,plain,(stoppedIn(n0,filling,n2)|holdsAt(waterLevel(plus(n0,n2)),plus(n0,n2))|~initiates(X1,filling,n0)|~happens(X1,n0)),inference(rw,[status(thm)],[6423,100,theory(equality)])).
% cnf(6439,plain,(stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2)|~initiates(X1,filling,n0)|~happens(X1,n0)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6438,100,theory(equality)]),100,theory(equality)])).
% cnf(33559,plain,(stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)|~initiates(tapOn,filling,n0)),inference(spm,[status(thm)],[6332,502,theory(equality)])).
% cnf(33560,plain,(stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)|$false),inference(rw,[status(thm)],[33559,1151,theory(equality)])).
% cnf(33561,plain,(stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)),inference(cn,[status(thm)],[33560,theory(equality)])).
% cnf(33586,plain,(less(n0,esk5_3(n0,filling,n1))|holdsAt(waterLevel(n1),n1)),inference(spm,[status(thm)],[148,33561,theory(equality)])).
% cnf(33587,plain,(less(esk5_3(n0,filling,n1),n1)|holdsAt(waterLevel(n1),n1)),inference(spm,[status(thm)],[147,33561,theory(equality)])).
% cnf(33612,plain,(less_or_equal(esk5_3(n0,filling,n1),n0)|holdsAt(waterLevel(n1),n1)),inference(spm,[status(thm)],[223,33587,theory(equality)])).
% cnf(33760,plain,(esk5_3(n0,filling,n1)=n0|less(esk5_3(n0,filling,n1),n0)|holdsAt(waterLevel(n1),n1)),inference(spm,[status(thm)],[230,33612,theory(equality)])).
% cnf(33762,plain,(esk5_3(n0,filling,n1)=n0|holdsAt(waterLevel(n1),n1)),inference(sr,[status(thm)],[33760,117,theory(equality)])).
% cnf(33835,plain,(less(n0,n0)|holdsAt(waterLevel(n1),n1)),inference(spm,[status(thm)],[33586,33762,theory(equality)])).
% cnf(33923,plain,(holdsAt(waterLevel(n1),n1)),inference(sr,[status(thm)],[33835,117,theory(equality)])).
% cnf(33932,plain,(epred1_3(waterLevel(n1),overflow,n1)),inference(spm,[status(thm)],[1703,33923,theory(equality)])).
% cnf(33954,plain,(initiates(overflow,waterLevel(n1),n1)),inference(spm,[status(thm)],[153,33932,theory(equality)])).
% cnf(34047,plain,(holdsAt(waterLevel(n1),plus(n1,n1))|~happens(overflow,n1)),inference(spm,[status(thm)],[173,33954,theory(equality)])).
% cnf(34050,plain,(holdsAt(waterLevel(n1),n2)|~happens(overflow,n1)),inference(rw,[status(thm)],[34047,191,theory(equality)])).
% cnf(34358,plain,(stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2)|~initiates(tapOn,filling,n0)),inference(spm,[status(thm)],[6439,502,theory(equality)])).
% cnf(34359,plain,(stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2)|$false),inference(rw,[status(thm)],[34358,1151,theory(equality)])).
% cnf(34360,plain,(stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2)),inference(cn,[status(thm)],[34359,theory(equality)])).
% cnf(34457,plain,(less(n0,esk5_3(n0,filling,n2))|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[148,34360,theory(equality)])).
% cnf(34458,plain,(less(esk5_3(n0,filling,n2),n2)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[147,34360,theory(equality)])).
% cnf(34459,plain,(happens(esk4_3(n0,filling,n2),esk5_3(n0,filling,n2))|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[149,34360,theory(equality)])).
% cnf(34460,plain,(terminates(esk4_3(n0,filling,n2),filling,esk5_3(n0,filling,n2))|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[146,34360,theory(equality)])).
% cnf(34463,plain,(less_or_equal(esk5_3(n0,filling,n2),n1)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[213,34458,theory(equality)])).
% cnf(34570,plain,(esk5_3(n0,filling,n2)=n1|less(esk5_3(n0,filling,n2),n1)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[230,34463,theory(equality)])).
% cnf(35439,plain,(overflow=esk4_3(n0,filling,n2)|tapOn=esk4_3(n0,filling,n2)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[109,34459,theory(equality)])).
% cnf(35444,plain,(tapOff=esk4_3(n0,filling,n2)|overflow=esk4_3(n0,filling,n2)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[164,34460,theory(equality)])).
% cnf(45150,plain,(tapOff=tapOn|tapOff=overflow|holdsAt(waterLevel(n2),n2)|esk4_3(n0,filling,n2)=overflow),inference(spm,[status(thm)],[35439,35444,theory(equality)])).
% cnf(45153,plain,(tapOff=overflow|holdsAt(waterLevel(n2),n2)|esk4_3(n0,filling,n2)=overflow),inference(sr,[status(thm)],[45150,202,theory(equality)])).
% cnf(45154,plain,(holdsAt(waterLevel(n2),n2)|esk4_3(n0,filling,n2)=overflow),inference(sr,[status(thm)],[45153,203,theory(equality)])).
% cnf(45156,plain,(happens(overflow,esk5_3(n0,filling,n2))|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[34459,45154,theory(equality)])).
% cnf(248972,plain,(esk5_3(n0,filling,n2)=n0|esk5_3(n0,filling,n2)=n1|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[1127,34570,theory(equality)])).
% cnf(249002,plain,(less(n0,n0)|holdsAt(waterLevel(n2),n2)|esk5_3(n0,filling,n2)=n1),inference(spm,[status(thm)],[34457,248972,theory(equality)])).
% cnf(249231,plain,(holdsAt(waterLevel(n2),n2)|esk5_3(n0,filling,n2)=n1),inference(sr,[status(thm)],[249002,117,theory(equality)])).
% cnf(249482,plain,(happens(overflow,n1)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[45156,249231,theory(equality)])).
% cnf(249811,plain,(holdsAt(waterLevel(n1),n2)|holdsAt(waterLevel(n2),n2)),inference(spm,[status(thm)],[34050,249482,theory(equality)])).
% cnf(249857,negated_conjecture,(n2=n3|holdsAt(waterLevel(n1),n2)),inference(spm,[status(thm)],[505,249811,theory(equality)])).
% cnf(249877,negated_conjecture,(n1=n3|n2=n3),inference(spm,[status(thm)],[505,249857,theory(equality)])).
% cnf(249913,negated_conjecture,(less(n3,n3)|n3=n1),inference(spm,[status(thm)],[491,249877,theory(equality)])).
% cnf(250553,negated_conjecture,(n3=n1),inference(sr,[status(thm)],[249913,307,theory(equality)])).
% cnf(255455,plain,(less(n1,n1)),inference(rw,[status(thm)],[535,250553,theory(equality)])).
% cnf(255456,plain,($false),inference(sr,[status(thm)],[255455,307,theory(equality)])).
% cnf(255457,plain,($false),255456,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 11959
% # ...of these trivial : 847
% # ...subsumed : 4535
% # ...remaining for further processing: 6577
% # Other redundant clauses eliminated : 2
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 236
% # Backward-rewritten : 3575
% # Generated clauses : 123102
% # ...of the previous two non-trivial : 57998
% # Contextual simplify-reflections : 2077
% # Paramodulations : 122834
% # Factorizations : 229
% # Equation resolutions : 39
% # Current number of processed clauses: 2764
% # Positive orientable unit clauses: 573
% # Positive unorientable unit clauses: 1
% # Negative unit clauses : 165
% # Non-unit-clauses : 2025
% # Current number of unprocessed clauses: 13179
% # ...number of literals in the above : 51750
% # Clause-clause subsumption calls (NU) : 317607
% # Rec. Clause-clause subsumption calls : 92529
% # Unit Clause-clause subsumption calls : 3040
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 28009
% # Indexed BW rewrite successes : 166
% # Backwards rewriting index: 1004 leaves, 2.09+/-2.994 terms/leaf
% # Paramod-from index: 595 leaves, 1.92+/-2.593 terms/leaf
% # Paramod-into index: 878 leaves, 1.95+/-2.656 terms/leaf
% # -------------------------------------------------
% # User time : 6.523 s
% # System time : 0.219 s
% # Total time : 6.742 s
% # Maximum resident set size: 0 pages
% PrfWatch: 10.30 CPU 10.70 WC
% FINAL PrfWatch: 10.30 CPU 10.70 WC
% SZS output end Solution for /tmp/SystemOnTPTP16249/CSR013+1.tptp
%
%------------------------------------------------------------------------------