The bear eats the mouse. The bear eats the tiger. The bear is blue. The bear likes the mouse. The bear likes the tiger. The mouse eats the bear. The mouse eats the tiger. The mouse is blue. The mouse is nice. The mouse likes the bear. The mouse likes the tiger. The tiger eats the bear. The tiger eats the mouse. The tiger is red. The tiger visits the bear. The tiger visits the mouse. If something is nice then it likes the bear. If something likes the bear and it is red then it is blue. If something eats the mouse and it likes the bear then it visits the mouse.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something is nice then it likes the bear.
((("something" "is" "nice" "+")) -> ("something" "likes" "bear" "+"))
If something likes the bear and it is red then it is blue.
((("something" "likes" "bear" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If something eats the mouse and it likes the bear then it visits the mouse.
((("something" "eats" "mouse" "+") ("something" "likes" "bear" "+")) -> ("something" "visits" "mouse" "+"))
The mouse eats the tiger.
True
1
proof
[(triple7)]
("mouse" "eats" "tiger" "+")
triple7
The tiger does not eat the bear.
False
1
inv-proof
[(triple12)]
("tiger" "eats" "bear" "-")
triple12
The bear does not like the bear.
Unknown
inv-rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "bear" "-")
The mouse visits the bear.
Unknown
random
[@0: The mouse visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bear" "+")
@0: The bear eats the mouse.[(triple1)] The bear eats the tiger.[(triple2)] The bear is blue.[(triple3)] The bear likes the mouse.[(triple4)] The bear likes the tiger.[(triple5)] The mouse eats the bear.[(triple6)] The mouse eats the tiger.[(triple7)] The mouse is blue.[(triple8)] The mouse is nice.[(triple9)] The mouse likes the bear.[(triple10 OR ((triple9) -> rule1))] The mouse likes the tiger.[(triple11)] The tiger eats the bear.[(triple12)] The tiger eats the mouse.[(triple13)] The tiger is red.[(triple14)] The tiger visits the bear.[(triple15)] The tiger visits the mouse.[(triple16)]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple2
The bear is blue.
("bear" "is" "blue" "+")
triple3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple4
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple5
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple6
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple7
The mouse is blue.
("mouse" "is" "blue" "+")
triple8
The mouse is nice.
("mouse" "is" "nice" "+")
triple9
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple10
((triple9) -> (rule1 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple11
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple12
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple13
The tiger is red.
("tiger" "is" "red" "+")
triple14
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple15
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple16