The dog is cold. The dog is nice. The dog needs the mouse. The dog does not need the rabbit. The mouse chases the dog. The mouse is not cold. The mouse is nice. The mouse is young. The mouse needs the rabbit. The mouse visits the rabbit. The rabbit chases the mouse. The rabbit is cold. The rabbit is nice. The rabbit needs the mouse. The rabbit visits the dog. If something visits the rabbit then it chases the rabbit. If something chases the rabbit and it is young then the rabbit does not visit the mouse.
The dog is cold.
("dog" "is" "cold" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog does not need the rabbit.
("dog" "needs" "rabbit" "-")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is not cold.
("mouse" "is" "cold" "-")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If something visits the rabbit then it chases the rabbit.
((("something" "visits" "rabbit" "+")) -> ("something" "chases" "rabbit" "+"))
If something chases the rabbit and it is young then the rabbit does not visit the mouse.
((("something" "chases" "rabbit" "+") ("something" "is" "young" "+")) -> ("rabbit" "visits" "mouse" "-"))
The mouse chases the dog.
True
1
proof
[(triple5)]
("mouse" "chases" "dog" "+")
triple5
The mouse is cold.
False
1
inv-proof
[(triple6)]
("mouse" "is" "cold" "+")
triple6
The mouse chases the rabbit.
True
2
proof
[(((triple10) -> rule1))]
("mouse" "chases" "rabbit" "+")
((triple10) -> (rule1 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse does not chase the rabbit.
False
2
inv-proof
[(((triple10) -> rule1))]
("mouse" "chases" "rabbit" "-")
((triple10) -> (rule1 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The rabbit does not visit the mouse.
True
4
proof
[(((((triple10) -> rule1) triple8) -> rule2))]
("rabbit" "visits" "mouse" "-")
((((triple10) -> (rule1 % int2)) triple8) -> (rule2 % int1))
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The rabbit visits the mouse.
False
4
inv-proof
[(((((triple10) -> rule1) triple8) -> rule2))]
("rabbit" "visits" "mouse" "+")
((((triple10) -> (rule1 % int2)) triple8) -> (rule2 % int1))
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The rabbit does not chase the rabbit.
Unknown
inv-rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "chases" "rabbit" "-")
The dog chases the rabbit.
Unknown
rconc
[@1: The dog chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "rabbit" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The rabbit needs the dog.
Unknown
random
[@0: The rabbit needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "dog" "+")
The dog does not chase the mouse.
Unknown
inv-random
[@0: The dog chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "mouse" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The dog does not need the rabbit.[(triple4)] The dog is cold.[(triple1)] The dog is nice.[(triple2)] The dog needs the mouse.[(triple3)] The mouse chases the dog.[(triple5)] The mouse is nice.[(triple7)] The mouse is not cold.[(triple6)] The mouse is young.[(triple8)] The mouse needs the rabbit.[(triple9)] The mouse visits the rabbit.[(triple10)] The rabbit chases the mouse.[(triple11)] The rabbit is cold.[(triple12)] The rabbit is nice.[(triple13)] The rabbit needs the mouse.[(triple14)] The rabbit visits the dog.[(triple15)] @1: The mouse chases the rabbit.[(((triple10) -> rule1))] @2: The rabbit does not visit the mouse.[(((((triple10) -> rule1) triple8) -> rule2))]
The dog does not need the rabbit.
("dog" "needs" "rabbit" "-")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog is nice.
("dog" "is" "nice" "+")
triple2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple3
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple5
The mouse is nice.
("mouse" "is" "nice" "+")
triple7
The mouse is not cold.
("mouse" "is" "cold" "-")
triple6
The mouse is young.
("mouse" "is" "young" "+")
triple8
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple9
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple10
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple11
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple12
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple13
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple14
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple15
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
((triple10) -> (rule1 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
((((triple10) -> (rule1 % int2)) triple8) -> (rule2 % int1))
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2