%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : CSR005+2 : TPTP v8.1.0. Bugfixed v3.1.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jul 27 12:48:35 EDT 2022 % Result : Timeout 299.85s 300.01s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : CSR005+2 : TPTP v8.1.0. Bugfixed v3.1.0. % 0.07/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n004.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Jul 27 04:05:51 EDT 2022 % 0.12/0.33 % CPUTime : % 1.88/2.09 ----- Otter 3.3f, August 2004 ----- % 1.88/2.09 The process was started by sandbox on n004.cluster.edu, % 1.88/2.09 Wed Jul 27 04:05:51 2022 % 1.88/2.09 The command was "./otter". The process ID is 17423. % 1.88/2.09 % 1.88/2.09 set(prolog_style_variables). % 1.88/2.09 set(auto). % 1.88/2.09 dependent: set(auto1). % 1.88/2.09 dependent: set(process_input). % 1.88/2.09 dependent: clear(print_kept). % 1.88/2.09 dependent: clear(print_new_demod). % 1.88/2.09 dependent: clear(print_back_demod). % 1.88/2.09 dependent: clear(print_back_sub). % 1.88/2.09 dependent: set(control_memory). % 1.88/2.09 dependent: assign(max_mem, 12000). % 1.88/2.09 dependent: assign(pick_given_ratio, 4). % 1.88/2.09 dependent: assign(stats_level, 1). % 1.88/2.09 dependent: assign(max_seconds, 10800). % 1.88/2.09 clear(print_given). % 1.88/2.09 % 1.88/2.09 formula_list(usable). % 1.88/2.09 all A (A=A). % 1.88/2.09 all Time1 Fluent Time2 (stoppedIn(Time1,Fluent,Time2)<-> (exists Event Time (happens(Event,Time)&less(Time1,Time)&less(Time,Time2)&terminates(Event,Fluent,Time)))). % 1.88/2.09 all Time1 Time2 Fluent (startedIn(Time1,Fluent,Time2)<-> (exists Event Time (happens(Event,Time)&less(Time1,Time)&less(Time,Time2)&initiates(Event,Fluent,Time)))). % 1.88/2.09 all Event Time Fluent Fluent2 Offset (happens(Event,Time)&initiates(Event,Fluent,Time)&less(n0,Offset)&trajectory(Fluent,Time,Fluent2,Offset)& -stoppedIn(Time,Fluent,plus(Time,Offset))->holdsAt(Fluent2,plus(Time,Offset))). % 1.88/2.09 all Event Time1 Fluent1 Time2 Fluent2 (happens(Event,Time1)&terminates(Event,Fluent1,Time1)&less(n0,Time2)&antitrajectory(Fluent1,Time1,Fluent2,Time2)& -startedIn(Time1,Fluent1,plus(Time1,Time2))->holdsAt(Fluent2,plus(Time1,Time2))). % 1.88/2.09 all Fluent Time (holdsAt(Fluent,Time)& -releasedAt(Fluent,plus(Time,n1))& -(exists Event (happens(Event,Time)&terminates(Event,Fluent,Time)))->holdsAt(Fluent,plus(Time,n1))). % 1.88/2.09 all Fluent Time (-holdsAt(Fluent,Time)& -releasedAt(Fluent,plus(Time,n1))& -(exists Event (happens(Event,Time)&initiates(Event,Fluent,Time)))-> -holdsAt(Fluent,plus(Time,n1))). % 1.88/2.09 all Fluent Time (releasedAt(Fluent,Time)& -(exists Event (happens(Event,Time)& (initiates(Event,Fluent,Time)|terminates(Event,Fluent,Time))))->releasedAt(Fluent,plus(Time,n1))). % 1.88/2.09 all Fluent Time (-releasedAt(Fluent,Time)& -(exists Event (happens(Event,Time)&releases(Event,Fluent,Time)))-> -releasedAt(Fluent,plus(Time,n1))). % 1.88/2.09 all Event Time Fluent (happens(Event,Time)&initiates(Event,Fluent,Time)->holdsAt(Fluent,plus(Time,n1))). % 1.88/2.09 all Event Time Fluent (happens(Event,Time)&terminates(Event,Fluent,Time)-> -holdsAt(Fluent,plus(Time,n1))). % 1.88/2.09 all Event Time Fluent (happens(Event,Time)&releases(Event,Fluent,Time)->releasedAt(Fluent,plus(Time,n1))). % 1.88/2.09 all Event Time Fluent (happens(Event,Time)& (initiates(Event,Fluent,Time)|terminates(Event,Fluent,Time))-> -releasedAt(Fluent,plus(Time,n1))). % 1.88/2.09 all Event Fluent Time (initiates(Event,Fluent,Time)<->Event=tapOn&Fluent=filling|Event=overflow&Fluent=spilling| (exists Height (holdsAt(waterLevel(Height),Time)&Event=tapOff&Fluent=waterLevel(Height)))| (exists Height (holdsAt(waterLevel(Height),Time)&Event=overflow&Fluent=waterLevel(Height)))). % 1.88/2.09 all Event Fluent Time (terminates(Event,Fluent,Time)<->Event=tapOff&Fluent=filling|Event=overflow&Fluent=filling). % 1.88/2.09 all Event Fluent Time (releases(Event,Fluent,Time)<-> (exists Height (Event=tapOn&Fluent=waterLevel(Height)))). % 1.88/2.09 all Event Time (happens(Event,Time)<->Event=tapOn&Time=n0|holdsAt(waterLevel(n3),Time)&holdsAt(filling,Time)&Event=overflow). % 1.88/2.09 all Height1 Time Height2 Offset (holdsAt(waterLevel(Height1),Time)&Height2=plus(Height1,Offset)->trajectory(filling,Time,waterLevel(Height2),Offset)). % 1.88/2.09 all Time Height1 Height2 (holdsAt(waterLevel(Height1),Time)&holdsAt(waterLevel(Height2),Time)->Height1=Height2). % 1.88/2.09 tapOff!=tapOn. % 1.88/2.09 tapOff!=overflow. % 1.88/2.09 overflow!=tapOn. % 1.88/2.09 all X (filling!=waterLevel(X)). % 1.88/2.09 all X (spilling!=waterLevel(X)). % 1.88/2.09 filling!=spilling. % 1.88/2.09 all X Y (waterLevel(X)=waterLevel(Y)<->X=Y). % 1.88/2.09 plus(n0,n0)=n0. % 1.88/2.09 plus(n0,n1)=n1. % 1.88/2.09 plus(n0,n2)=n2. % 1.88/2.09 plus(n0,n3)=n3. % 1.88/2.09 plus(n1,n1)=n2. % 1.88/2.09 plus(n1,n2)=n3. % 1.88/2.09 plus(n1,n3)=n4. % 1.88/2.09 plus(n2,n2)=n4. % 1.88/2.09 plus(n2,n3)=n5. % 1.88/2.09 plus(n3,n3)=n6. % 1.88/2.09 all X Y (plus(X,Y)=plus(Y,X)). % 1.88/2.09 all X Y (less_or_e_qual(X,Y)<->less(X,Y)|X=Y). % 1.88/2.09 -(exists X less(X,n0)). % 1.88/2.09 all X (less(X,n1)<->less_or_e_qual(X,n0)). % 1.88/2.09 all X (less(X,n2)<->less_or_e_qual(X,n1)). % 1.88/2.09 all X (less(X,n3)<->less_or_e_qual(X,n2)). % 1.88/2.09 all X (less(X,n4)<->less_or_e_qual(X,n3)). % 1.88/2.09 all X (less(X,n5)<->less_or_e_qual(X,n4)). % 1.88/2.09 all X (less(X,n6)<->less_or_e_qual(X,n5)). % 1.88/2.09 all X (less(X,n7)<->less_or_e_qual(X,n6)). % 1.88/2.09 all X (less(X,n8)<->less_or_e_qual(X,n7)). % 1.88/2.09 all X (less(X,n9)<->less_or_e_qual(X,n8)). % 1.88/2.09 all X Y (less(X,Y)<-> -less(Y,X)&Y!=X). % 1.88/2.09 holdsAt(waterLevel(n0),n0). % 1.88/2.09 -holdsAt(filling,n0). % 1.88/2.09 -holdsAt(spilling,n0). % 1.88/2.09 all Height (-releasedAt(waterLevel(Height),n0)). % 1.88/2.09 -releasedAt(filling,n0). % 1.88/2.09 -releasedAt(spilling,n0). % 1.88/2.09 -releasedAt(filling,n3). % 1.88/2.09 -holdsAt(filling,n3). % 1.88/2.09 end_of_list. % 1.88/2.09 % 1.88/2.09 -------> usable clausifies to: % 1.88/2.09 % 1.88/2.09 list(usable). % 1.88/2.09 0 [] A=A. % 1.88/2.09 0 [] -stoppedIn(Time1,Fluent,Time2)|happens($f2(Time1,Fluent,Time2),$f1(Time1,Fluent,Time2)). % 1.88/2.09 0 [] -stoppedIn(Time1,Fluent,Time2)|less(Time1,$f1(Time1,Fluent,Time2)). % 1.88/2.09 0 [] -stoppedIn(Time1,Fluent,Time2)|less($f1(Time1,Fluent,Time2),Time2). % 1.88/2.09 0 [] -stoppedIn(Time1,Fluent,Time2)|terminates($f2(Time1,Fluent,Time2),Fluent,$f1(Time1,Fluent,Time2)). % 1.88/2.09 0 [] stoppedIn(Time1,Fluent,Time2)| -happens(Event,Time)| -less(Time1,Time)| -less(Time,Time2)| -terminates(Event,Fluent,Time). % 1.88/2.09 0 [] -startedIn(Time1,Fluent,Time2)|happens($f4(Time1,Time2,Fluent),$f3(Time1,Time2,Fluent)). % 1.88/2.09 0 [] -startedIn(Time1,Fluent,Time2)|less(Time1,$f3(Time1,Time2,Fluent)). % 1.88/2.09 0 [] -startedIn(Time1,Fluent,Time2)|less($f3(Time1,Time2,Fluent),Time2). % 1.88/2.09 0 [] -startedIn(Time1,Fluent,Time2)|initiates($f4(Time1,Time2,Fluent),Fluent,$f3(Time1,Time2,Fluent)). % 1.88/2.09 0 [] startedIn(Time1,Fluent,Time2)| -happens(Event,Time)| -less(Time1,Time)| -less(Time,Time2)| -initiates(Event,Fluent,Time). % 1.88/2.09 0 [] -happens(Event,Time)| -initiates(Event,Fluent,Time)| -less(n0,Offset)| -trajectory(Fluent,Time,Fluent2,Offset)|stoppedIn(Time,Fluent,plus(Time,Offset))|holdsAt(Fluent2,plus(Time,Offset)). % 1.88/2.09 0 [] -happens(Event,Time1)| -terminates(Event,Fluent1,Time1)| -less(n0,Time2)| -antitrajectory(Fluent1,Time1,Fluent2,Time2)|startedIn(Time1,Fluent1,plus(Time1,Time2))|holdsAt(Fluent2,plus(Time1,Time2)). % 1.88/2.09 0 [] -holdsAt(Fluent,Time)|releasedAt(Fluent,plus(Time,n1))|happens($f5(Fluent,Time),Time)|holdsAt(Fluent,plus(Time,n1)). % 1.88/2.09 0 [] -holdsAt(Fluent,Time)|releasedAt(Fluent,plus(Time,n1))|terminates($f5(Fluent,Time),Fluent,Time)|holdsAt(Fluent,plus(Time,n1)). % 1.88/2.09 0 [] holdsAt(Fluent,Time)|releasedAt(Fluent,plus(Time,n1))|happens($f6(Fluent,Time),Time)| -holdsAt(Fluent,plus(Time,n1)). % 1.88/2.09 0 [] holdsAt(Fluent,Time)|releasedAt(Fluent,plus(Time,n1))|initiates($f6(Fluent,Time),Fluent,Time)| -holdsAt(Fluent,plus(Time,n1)). % 1.88/2.09 0 [] -releasedAt(Fluent,Time)|happens($f7(Fluent,Time),Time)|releasedAt(Fluent,plus(Time,n1)). % 1.88/2.09 0 [] -releasedAt(Fluent,Time)|initiates($f7(Fluent,Time),Fluent,Time)|terminates($f7(Fluent,Time),Fluent,Time)|releasedAt(Fluent,plus(Time,n1)). % 1.88/2.09 0 [] releasedAt(Fluent,Time)|happens($f8(Fluent,Time),Time)| -releasedAt(Fluent,plus(Time,n1)). % 1.88/2.09 0 [] releasedAt(Fluent,Time)|releases($f8(Fluent,Time),Fluent,Time)| -releasedAt(Fluent,plus(Time,n1)). % 1.88/2.09 0 [] -happens(Event,Time)| -initiates(Event,Fluent,Time)|holdsAt(Fluent,plus(Time,n1)). % 1.88/2.09 0 [] -happens(Event,Time)| -terminates(Event,Fluent,Time)| -holdsAt(Fluent,plus(Time,n1)). % 1.88/2.09 0 [] -happens(Event,Time)| -releases(Event,Fluent,Time)|releasedAt(Fluent,plus(Time,n1)). % 1.88/2.09 0 [] -happens(Event,Time)| -initiates(Event,Fluent,Time)| -releasedAt(Fluent,plus(Time,n1)). % 1.88/2.09 0 [] -happens(Event,Time)| -terminates(Event,Fluent,Time)| -releasedAt(Fluent,plus(Time,n1)). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Event=tapOn|Event=overflow|holdsAt(waterLevel($f9(Event,Fluent,Time)),Time). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Event=tapOn|Event=overflow|Event=tapOff. % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Event=tapOn|Event=overflow|Fluent=waterLevel($f9(Event,Fluent,Time)). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Event=tapOn|Fluent=spilling|holdsAt(waterLevel($f9(Event,Fluent,Time)),Time)|holdsAt(waterLevel($f10(Event,Fluent,Time)),Time). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Event=tapOn|Fluent=spilling|holdsAt(waterLevel($f9(Event,Fluent,Time)),Time)|Fluent=waterLevel($f10(Event,Fluent,Time)). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Event=tapOn|Fluent=spilling|Event=tapOff|holdsAt(waterLevel($f10(Event,Fluent,Time)),Time). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Event=tapOn|Fluent=spilling|Event=tapOff|Fluent=waterLevel($f10(Event,Fluent,Time)). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Event=tapOn|Fluent=spilling|Fluent=waterLevel($f9(Event,Fluent,Time))|holdsAt(waterLevel($f10(Event,Fluent,Time)),Time). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Event=tapOn|Fluent=spilling|Fluent=waterLevel($f9(Event,Fluent,Time))|Fluent=waterLevel($f10(Event,Fluent,Time)). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Fluent=filling|Event=overflow|holdsAt(waterLevel($f9(Event,Fluent,Time)),Time). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Fluent=filling|Event=overflow|Event=tapOff. % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Fluent=filling|Event=overflow|Fluent=waterLevel($f9(Event,Fluent,Time)). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Fluent=filling|Fluent=spilling|holdsAt(waterLevel($f9(Event,Fluent,Time)),Time)|holdsAt(waterLevel($f10(Event,Fluent,Time)),Time). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Fluent=filling|Fluent=spilling|holdsAt(waterLevel($f9(Event,Fluent,Time)),Time)|Fluent=waterLevel($f10(Event,Fluent,Time)). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Fluent=filling|Fluent=spilling|Event=tapOff|holdsAt(waterLevel($f10(Event,Fluent,Time)),Time). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Fluent=filling|Fluent=spilling|Event=tapOff|Fluent=waterLevel($f10(Event,Fluent,Time)). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Fluent=filling|Fluent=spilling|Fluent=waterLevel($f9(Event,Fluent,Time))|holdsAt(waterLevel($f10(Event,Fluent,Time)),Time). % 1.88/2.09 0 [] -initiates(Event,Fluent,Time)|Fluent=filling|Fluent=spilling|Fluent=waterLevel($f9(Event,Fluent,Time))|Fluent=waterLevel($f10(Event,Fluent,Time)). % 1.88/2.09 0 [] initiates(Event,Fluent,Time)|Event!=tapOn|Fluent!=filling. % 1.88/2.09 0 [] initiates(Event,Fluent,Time)|Event!=overflow|Fluent!=spilling. % 1.88/2.09 0 [] initiates(Event,Fluent,Time)| -holdsAt(waterLevel(Height),Time)|Event!=tapOff|Fluent!=waterLevel(Height). % 1.88/2.09 0 [] initiates(Event,Fluent,Time)| -holdsAt(waterLevel(X1),Time)|Event!=overflow|Fluent!=waterLevel(X1). % 1.88/2.09 0 [] -terminates(Event,Fluent,Time)|Event=tapOff|Event=overflow. % 1.88/2.09 0 [] -terminates(Event,Fluent,Time)|Fluent=filling. % 1.88/2.09 0 [] terminates(Event,Fluent,Time)|Event!=tapOff|Fluent!=filling. % 1.88/2.09 0 [] terminates(Event,Fluent,Time)|Event!=overflow|Fluent!=filling. % 1.88/2.09 0 [] -releases(Event,Fluent,Time)|Event=tapOn. % 1.88/2.09 0 [] -releases(Event,Fluent,Time)|Fluent=waterLevel($f11(Event,Fluent,Time)). % 1.88/2.09 0 [] releases(Event,Fluent,Time)|Event!=tapOn|Fluent!=waterLevel(Height). % 1.88/2.09 0 [] -happens(Event,Time)|Event=tapOn|holdsAt(waterLevel(n3),Time). % 1.88/2.09 0 [] -happens(Event,Time)|Event=tapOn|holdsAt(filling,Time). % 1.88/2.09 0 [] -happens(Event,Time)|Event=tapOn|Event=overflow. % 1.88/2.09 0 [] -happens(Event,Time)|Time=n0|holdsAt(waterLevel(n3),Time). % 1.88/2.09 0 [] -happens(Event,Time)|Time=n0|holdsAt(filling,Time). % 1.88/2.09 0 [] -happens(Event,Time)|Time=n0|Event=overflow. % 1.88/2.09 0 [] happens(Event,Time)|Event!=tapOn|Time!=n0. % 1.88/2.09 0 [] happens(Event,Time)| -holdsAt(waterLevel(n3),Time)| -holdsAt(filling,Time)|Event!=overflow. % 1.88/2.09 0 [] -holdsAt(waterLevel(Height1),Time)|Height2!=plus(Height1,Offset)|trajectory(filling,Time,waterLevel(Height2),Offset). % 1.88/2.09 0 [] -holdsAt(waterLevel(Height1),Time)| -holdsAt(waterLevel(Height2),Time)|Height1=Height2. % 1.88/2.09 0 [] tapOff!=tapOn. % 1.88/2.09 0 [] tapOff!=overflow. % 1.88/2.09 0 [] overflow!=tapOn. % 1.88/2.09 0 [] filling!=waterLevel(X). % 1.88/2.09 0 [] spilling!=waterLevel(X). % 1.88/2.09 0 [] filling!=spilling. % 1.88/2.09 0 [] waterLevel(X)!=waterLevel(Y)|X=Y. % 1.88/2.09 0 [] waterLevel(X)=waterLevel(Y)|X!=Y. % 1.88/2.09 0 [] plus(n0,n0)=n0. % 1.88/2.09 0 [] plus(n0,n1)=n1. % 1.88/2.09 0 [] plus(n0,n2)=n2. % 1.88/2.09 0 [] plus(n0,n3)=n3. % 1.88/2.09 0 [] plus(n1,n1)=n2. % 1.88/2.09 0 [] plus(n1,n2)=n3. % 1.88/2.09 0 [] plus(n1,n3)=n4. % 1.88/2.09 0 [] plus(n2,n2)=n4. % 1.88/2.09 0 [] plus(n2,n3)=n5. % 1.88/2.09 0 [] plus(n3,n3)=n6. % 1.88/2.09 0 [] plus(X,Y)=plus(Y,X). % 1.88/2.09 0 [] -less_or_e_qual(X,Y)|less(X,Y)|X=Y. % 1.88/2.09 0 [] less_or_e_qual(X,Y)| -less(X,Y). % 1.88/2.09 0 [] less_or_e_qual(X,Y)|X!=Y. % 1.88/2.09 0 [] -less(X,n0). % 1.88/2.09 0 [] -less(X,n1)|less_or_e_qual(X,n0). % 1.88/2.09 0 [] less(X,n1)| -less_or_e_qual(X,n0). % 1.88/2.09 0 [] -less(X,n2)|less_or_e_qual(X,n1). % 1.88/2.09 0 [] less(X,n2)| -less_or_e_qual(X,n1). % 1.88/2.09 0 [] -less(X,n3)|less_or_e_qual(X,n2). % 1.88/2.09 0 [] less(X,n3)| -less_or_e_qual(X,n2). % 1.88/2.09 0 [] -less(X,n4)|less_or_e_qual(X,n3). % 1.88/2.09 0 [] less(X,n4)| -less_or_e_qual(X,n3). % 1.88/2.09 0 [] -less(X,n5)|less_or_e_qual(X,n4). % 1.88/2.09 0 [] less(X,n5)| -less_or_e_qual(X,n4). % 1.88/2.09 0 [] -less(X,n6)|less_or_e_qual(X,n5). % 1.88/2.09 0 [] less(X,n6)| -less_or_e_qual(X,n5). % 1.88/2.09 0 [] -less(X,n7)|less_or_e_qual(X,n6). % 1.88/2.09 0 [] less(X,n7)| -less_or_e_qual(X,n6). % 1.88/2.09 0 [] -less(X,n8)|less_or_e_qual(X,n7). % 1.88/2.09 0 [] less(X,n8)| -less_or_e_qual(X,n7). % 1.88/2.09 0 [] -less(X,n9)|less_or_e_qual(X,n8). % 1.88/2.09 0 [] less(X,n9)| -less_or_e_qual(X,n8). % 1.88/2.09 0 [] -less(X,Y)| -less(Y,X). % 1.88/2.09 0 [] -less(X,Y)|Y!=X. % 1.88/2.09 0 [] less(X,Y)|less(Y,X)|Y=X. % 1.88/2.09 0 [] holdsAt(waterLevel(n0),n0). % 1.88/2.09 0 [] -holdsAt(filling,n0). % 1.88/2.09 0 [] -holdsAt(spilling,n0). % 1.88/2.09 0 [] -releasedAt(waterLevel(Height),n0). % 1.88/2.09 0 [] -releasedAt(filling,n0). % 1.88/2.09 0 [] -releasedAt(spilling,n0). % 1.88/2.09 0 [] -releasedAt(filling,n3). % 1.88/2.09 0 [] -holdsAt(filling,n3). % 1.88/2.09 end_of_list. % 1.88/2.09 % 1.88/2.09 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=6. % 1.88/2.09 % 1.88/2.09 This ia a non-Horn set with equality. The strategy will be % 1.88/2.09 Knuth-Bendix, ordered hyper_res, factoring, and unit % 1.88/2.09 deletion, with positive clauses in sos and nonpositive % 1.88/2.09 clauses in usable. % 1.88/2.09 % 1.88/2.09 dependent: set(knuth_bendix). % 1.88/2.09 dependent: set(anl_eq). % 1.88/2.09 dependent: set(para_from). % 1.88/2.09 dependent: set(para_into). % 1.88/2.09 dependent: clear(para_from_right). % 1.88/2.09 dependent: clear(para_into_right). % 1.88/2.09 dependent: set(para_from_vars). % 1.88/2.09 dependent: set(eq_units_both_ways). % 1.88/2.09 dependent: set(dynamic_demod_all). % 1.88/2.09 dependent: set(dynamic_demod). % 1.88/2.09 dependent: set(order_eq). % 1.88/2.09 dependent: set(back_demod). % 1.88/2.09 dependent: set(lrpo). % 1.88/2.09 dependent: set(hyper_res). % 1.88/2.09 dependent: set(unit_deletion). % 1.88/2.09 dependent: set(factor). % 1.88/2.09 % 1.88/2.09 ------------> process usable: % 1.88/2.09 ** KEPT (pick-wt=13): 1 [] -stoppedIn(A,B,C)|happens($f2(A,B,C),$f1(A,B,C)). % 1.88/2.09 ** KEPT (pick-wt=10): 2 [] -stoppedIn(A,B,C)|less(A,$f1(A,B,C)). % 1.88/2.09 ** KEPT (pick-wt=10): 3 [] -stoppedIn(A,B,C)|less($f1(A,B,C),C). % 1.88/2.09 ** KEPT (pick-wt=14): 4 [] -stoppedIn(A,B,C)|terminates($f2(A,B,C),B,$f1(A,B,C)). % 1.88/2.09 ** KEPT (pick-wt=17): 5 [] stoppedIn(A,B,C)| -happens(D,E)| -less(A,E)| -less(E,C)| -terminates(D,B,E). % 1.88/2.09 ** KEPT (pick-wt=13): 6 [] -startedIn(A,B,C)|happens($f4(A,C,B),$f3(A,C,B)). % 1.88/2.09 ** KEPT (pick-wt=10): 7 [] -startedIn(A,B,C)|less(A,$f3(A,C,B)). % 1.88/2.09 ** KEPT (pick-wt=10): 8 [] -startedIn(A,B,C)|less($f3(A,C,B),C). % 1.88/2.09 ** KEPT (pick-wt=14): 9 [] -startedIn(A,B,C)|initiates($f4(A,C,B),B,$f3(A,C,B)). % 1.88/2.09 ** KEPT (pick-wt=17): 10 [] startedIn(A,B,C)| -happens(D,E)| -less(A,E)| -less(E,C)| -initiates(D,B,E). % 1.88/2.09 ** KEPT (pick-wt=26): 11 [] -happens(A,B)| -initiates(A,C,B)| -less(n0,D)| -trajectory(C,B,E,D)|stoppedIn(B,C,plus(B,D))|holdsAt(E,plus(B,D)). % 1.88/2.09 ** KEPT (pick-wt=26): 12 [] -happens(A,B)| -terminates(A,C,B)| -less(n0,D)| -antitrajectory(C,B,E,D)|startedIn(B,C,plus(B,D))|holdsAt(E,plus(B,D)). % 1.88/2.09 ** KEPT (pick-wt=18): 13 [] -holdsAt(A,B)|releasedAt(A,plus(B,n1))|happens($f5(A,B),B)|holdsAt(A,plus(B,n1)). % 1.88/2.09 ** KEPT (pick-wt=19): 14 [] -holdsAt(A,B)|releasedAt(A,plus(B,n1))|terminates($f5(A,B),A,B)|holdsAt(A,plus(B,n1)). % 1.88/2.09 ** KEPT (pick-wt=18): 15 [] holdsAt(A,B)|releasedAt(A,plus(B,n1))|happens($f6(A,B),B)| -holdsAt(A,plus(B,n1)). % 1.88/2.09 ** KEPT (pick-wt=19): 16 [] holdsAt(A,B)|releasedAt(A,plus(B,n1))|initiates($f6(A,B),A,B)| -holdsAt(A,plus(B,n1)). % 1.88/2.09 ** KEPT (pick-wt=13): 17 [] -releasedAt(A,B)|happens($f7(A,B),B)|releasedAt(A,plus(B,n1)). % 1.88/2.09 ** KEPT (pick-wt=20): 18 [] -releasedAt(A,B)|initiates($f7(A,B),A,B)|terminates($f7(A,B),A,B)|releasedAt(A,plus(B,n1)). % 1.88/2.09 ** KEPT (pick-wt=13): 19 [] releasedAt(A,B)|happens($f8(A,B),B)| -releasedAt(A,plus(B,n1)). % 1.88/2.09 ** KEPT (pick-wt=14): 20 [] releasedAt(A,B)|releases($f8(A,B),A,B)| -releasedAt(A,plus(B,n1)). % 1.88/2.09 ** KEPT (pick-wt=12): 21 [] -happens(A,B)| -initiates(A,C,B)|holdsAt(C,plus(B,n1)). % 1.88/2.09 ** KEPT (pick-wt=12): 22 [] -happens(A,B)| -terminates(A,C,B)| -holdsAt(C,plus(B,n1)). % 1.88/2.09 ** KEPT (pick-wt=12): 23 [] -happens(A,B)| -releases(A,C,B)|releasedAt(C,plus(B,n1)). % 1.88/2.09 ** KEPT (pick-wt=12): 24 [] -happens(A,B)| -initiates(A,C,B)| -releasedAt(C,plus(B,n1)). % 1.88/2.09 ** KEPT (pick-wt=12): 25 [] -happens(A,B)| -terminates(A,C,B)| -releasedAt(C,plus(B,n1)). % 1.88/2.09 ** KEPT (pick-wt=17): 26 [] -initiates(A,B,C)|A=tapOn|A=overflow|holdsAt(waterLevel($f9(A,B,C)),C). % 1.88/2.09 ** KEPT (pick-wt=13): 27 [] -initiates(A,B,C)|A=tapOn|A=overflow|A=tapOff. % 1.88/2.09 ** KEPT (pick-wt=17): 29 [copy,28,flip.4] -initiates(A,B,C)|A=tapOn|A=overflow|waterLevel($f9(A,B,C))=B. % 1.88/2.09 ** KEPT (pick-wt=24): 30 [] -initiates(A,B,C)|A=tapOn|B=spilling|holdsAt(waterLevel($f9(A,B,C)),C)|holdsAt(waterLevel($f10(A,B,C)),C). % 1.88/2.09 ** KEPT (pick-wt=24): 32 [copy,31,flip.5] -initiates(A,B,C)|A=tapOn|B=spilling|holdsAt(waterLevel($f9(A,B,C)),C)|waterLevel($f10(A,B,C))=B. % 1.88/2.09 ** KEPT (pick-wt=20): 33 [] -initiates(A,B,C)|A=tapOn|B=spilling|A=tapOff|holdsAt(waterLevel($f10(A,B,C)),C). % 1.88/2.09 ** KEPT (pick-wt=20): 35 [copy,34,flip.5] -initiates(A,B,C)|A=tapOn|B=spilling|A=tapOff|waterLevel($f10(A,B,C))=B. % 1.88/2.09 ** KEPT (pick-wt=24): 37 [copy,36,flip.4] -initiates(A,B,C)|A=tapOn|B=spilling|waterLevel($f9(A,B,C))=B|holdsAt(waterLevel($f10(A,B,C)),C). % 1.88/2.09 ** KEPT (pick-wt=24): 39 [copy,38,flip.4,flip.5] -initiates(A,B,C)|A=tapOn|B=spilling|waterLevel($f9(A,B,C))=B|waterLevel($f10(A,B,C))=B. % 1.88/2.09 ** KEPT (pick-wt=17): 40 [] -initiates(A,B,C)|B=filling|A=overflow|holdsAt(waterLevel($f9(A,B,C)),C). % 1.88/2.09 ** KEPT (pick-wt=13): 41 [] -initiates(A,B,C)|B=filling|A=overflow|A=tapOff. % 1.88/2.09 ** KEPT (pick-wt=17): 43 [copy,42,flip.4] -initiates(A,B,C)|B=filling|A=overflow|waterLevel($f9(A,B,C))=B. % 1.88/2.09 ** KEPT (pick-wt=24): 44 [] -initiates(A,B,C)|B=filling|B=spilling|holdsAt(waterLevel($f9(A,B,C)),C)|holdsAt(waterLevel($f10(A,B,C)),C). % 1.88/2.09 ** KEPT (pick-wt=24): 46 [copy,45,flip.5] -initiates(A,B,C)|B=filling|B=spilling|holdsAt(waterLevel($f9(A,B,C)),C)|waterLevel($f10(A,B,C))=B. % 1.88/2.09 ** KEPT (pick-wt=20): 47 [] -initiates(A,B,C)|B=filling|B=spilling|A=tapOff|holdsAt(waterLevel($f10(A,B,C)),C). % 1.88/2.09 ** KEPT (pick-wt=20): 49 [copy,48,flip.5] -initiates(A,B,C)|B=filling|B=spilling|A=tapOff|waterLevel($f10(A,B,C))=B. % 1.88/2.09 ** KEPT (pick-wt=24): 51 [copy,50,flip.4] -initiates(A,B,C)|B=filling|B=spilling|waterLevel($f9(A,B,C))=B|holdsAt(waterLevel($f10(A,B,C)),C). % 1.88/2.09 ** KEPT (pick-wt=24): 53 [copy,52,flip.4,flip.5] -initiates(A,B,C)|B=filling|B=spilling|waterLevel($f9(A,B,C))=B|waterLevel($f10(A,B,C))=B. % 1.88/2.09 ** KEPT (pick-wt=10): 54 [] initiates(A,B,C)|A!=tapOn|B!=filling. % 1.88/2.09 ** KEPT (pick-wt=10): 55 [] initiates(A,B,C)|A!=overflow|B!=spilling. % 1.88/2.09 ** KEPT (pick-wt=15): 56 [] initiates(A,B,C)| -holdsAt(waterLevel(D),C)|A!=tapOff|B!=waterLevel(D). % 1.88/2.09 ** KEPT (pick-wt=15): 57 [] initiates(A,B,C)| -holdsAt(waterLevel(D),C)|A!=overflow|B!=waterLevel(D). % 1.88/2.09 ** KEPT (pick-wt=10): 58 [] -terminates(A,B,C)|A=tapOff|A=overflow. % 1.88/2.09 ** KEPT (pick-wt=7): 59 [] -terminates(A,B,C)|B=filling. % 1.88/2.09 ** KEPT (pick-wt=10): 60 [] terminates(A,B,C)|A!=tapOff|B!=filling. % 1.88/2.09 ** KEPT (pick-wt=10): 61 [] terminates(A,B,C)|A!=overflow|B!=filling. % 1.88/2.09 ** KEPT (pick-wt=7): 62 [] -releases(A,B,C)|A=tapOn. % 1.88/2.09 ** KEPT (pick-wt=11): 64 [copy,63,flip.2] -releases(A,B,C)|waterLevel($f11(A,B,C))=B. % 1.88/2.09 ** KEPT (pick-wt=11): 65 [] releases(A,B,C)|A!=tapOn|B!=waterLevel(D). % 1.88/2.09 ** KEPT (pick-wt=10): 66 [] -happens(A,B)|A=tapOn|holdsAt(waterLevel(n3),B). % 1.88/2.09 ** KEPT (pick-wt=9): 67 [] -happens(A,B)|A=tapOn|holdsAt(filling,B). % 1.88/2.09 ** KEPT (pick-wt=9): 68 [] -happens(A,B)|A=tapOn|A=overflow. % 1.88/2.09 ** KEPT (pick-wt=10): 69 [] -happens(A,B)|B=n0|holdsAt(waterLevel(n3),B). % 1.88/2.09 ** KEPT (pick-wt=9): 70 [] -happens(A,B)|B=n0|holdsAt(filling,B). % 1.88/2.09 ** KEPT (pick-wt=9): 71 [] -happens(A,B)|B=n0|A=overflow. % 1.88/2.09 ** KEPT (pick-wt=9): 72 [] happens(A,B)|A!=tapOn|B!=n0. % 1.88/2.09 ** KEPT (pick-wt=13): 73 [] happens(A,B)| -holdsAt(waterLevel(n3),B)| -holdsAt(filling,B)|A!=overflow. % 1.88/2.09 ** KEPT (pick-wt=15): 74 [] -holdsAt(waterLevel(A),B)|C!=plus(A,D)|trajectory(filling,B,waterLevel(C),D). % 1.88/2.09 ** KEPT (pick-wt=11): 75 [] -holdsAt(waterLevel(A),B)| -holdsAt(waterLevel(C),B)|A=C. % 1.88/2.09 ** KEPT (pick-wt=3): 77 [copy,76,flip.1] tapOn!=tapOff. % 1.88/2.09 ** KEPT (pick-wt=3): 78 [] tapOff!=overflow. % 1.88/2.09 ** KEPT (pick-wt=3): 80 [copy,79,flip.1] tapOn!=overflow. % 1.88/2.09 ** KEPT (pick-wt=4): 82 [copy,81,flip.1] waterLevel(A)!=filling. % 1.88/2.09 ** KEPT (pick-wt=4): 84 [copy,83,flip.1] waterLevel(A)!=spilling. % 1.88/2.09 ** KEPT (pick-wt=3): 86 [copy,85,flip.1] spilling!=filling. % 1.88/2.09 ** KEPT (pick-wt=8): 87 [] waterLevel(A)!=waterLevel(B)|A=B. % 1.88/2.09 ** KEPT (pick-wt=8): 88 [] waterLevel(A)=waterLevel(B)|A!=B. % 1.88/2.09 ** KEPT (pick-wt=9): 89 [] -less_or_e_qual(A,B)|less(A,B)|A=B. % 1.88/2.09 ** KEPT (pick-wt=6): 90 [] less_or_e_qual(A,B)| -less(A,B). % 1.88/2.09 ** KEPT (pick-wt=6): 91 [] less_or_e_qual(A,B)|A!=B. % 1.88/2.09 ** KEPT (pick-wt=3): 92 [] -less(A,n0). % 1.88/2.09 ** KEAlarm clock % 299.85/300.01 Otter interrupted % 299.85/300.01 PROOF NOT FOUND %------------------------------------------------------------------------------