The dog needs the mouse. The dog needs the tiger. The lion eats the tiger. The mouse likes the tiger. The tiger eats the mouse. The tiger likes the mouse. The tiger needs the dog. If someone likes the mouse then they are kind. If the tiger likes the lion then the tiger eats the mouse. If someone eats the tiger then they like the mouse.
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If someone likes the mouse then they are kind.
((("someone" "likes" "mouse" "+")) -> ("someone" "is" "kind" "+"))
If the tiger likes the lion then the tiger eats the mouse.
((("tiger" "likes" "lion" "+")) -> ("tiger" "eats" "mouse" "+"))
If someone eats the tiger then they like the mouse.
((("someone" "eats" "tiger" "+")) -> ("someone" "likes" "mouse" "+"))
The tiger likes the mouse.
True
1
proof
[(triple6)]
("tiger" "likes" "mouse" "+")
triple6
The dog does not need the mouse.
False
1
inv-proof
[(triple1)]
("dog" "needs" "mouse" "-")
triple1
The lion likes the mouse.
True
2
proof
[(((triple3) -> rule3))]
("lion" "likes" "mouse" "+")
((triple3) -> (rule3 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The tiger is not kind.
False
2
inv-proof
[(((triple6) -> rule1))]
("tiger" "is" "kind" "-")
((triple6) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The mouse is not kind.
Unknown
inv-rconc
[@2: The mouse is kind.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("mouse" "is" "kind" "-")
The dog is kind.
Unknown
rconc
[@2: The dog is kind.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("dog" "is" "kind" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger eats the lion.
Unknown
random
[@0: The tiger eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "lion" "+")
@0: The dog needs the mouse.[(triple1)] The dog needs the tiger.[(triple2)] The lion eats the tiger.[(triple3)] The mouse likes the tiger.[(triple4)] The tiger eats the mouse.[(triple5)] The tiger likes the mouse.[(triple6)] The tiger needs the dog.[(triple7)] @1: The lion likes the mouse.[(((triple3) -> rule3))] The tiger is kind.[(((triple6) -> rule1))] @2: The lion is kind.[(((((triple3) -> rule3)) -> rule1))]
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple3
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple4
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple5
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple6
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple7
The lion likes the mouse.
("lion" "likes" "mouse" "+")
((triple3) -> (rule3 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple6) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2