The lion likes the mouse. The mouse eats the lion. The mouse is kind. The mouse is round. The mouse visits the tiger. The tiger likes the lion. The tiger visits the mouse. If someone is kind and they visit the tiger then the tiger visits the lion. If the tiger eats the mouse and the tiger is nice then the mouse is red. If someone likes the lion then the lion likes the tiger. If someone visits the lion then they are red. If someone is red and they visit the mouse then the mouse likes the tiger. If someone is kind and they like the mouse then the mouse is round.
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone is kind and they visit the tiger then the tiger visits the lion.
((("someone" "is" "kind" "+") ("someone" "visits" "tiger" "+")) -> ("tiger" "visits" "lion" "+"))
If the tiger eats the mouse and the tiger is nice then the mouse is red.
((("tiger" "eats" "mouse" "+") ("tiger" "is" "nice" "+")) -> ("mouse" "is" "red" "+"))
If someone likes the lion then the lion likes the tiger.
((("someone" "likes" "lion" "+")) -> ("lion" "likes" "tiger" "+"))
If someone visits the lion then they are red.
((("someone" "visits" "lion" "+")) -> ("someone" "is" "red" "+"))
If someone is red and they visit the mouse then the mouse likes the tiger.
((("someone" "is" "red" "+") ("someone" "visits" "mouse" "+")) -> ("mouse" "likes" "tiger" "+"))
If someone is kind and they like the mouse then the mouse is round.
((("someone" "is" "kind" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "is" "round" "+"))
The tiger likes the lion.
True
1
proof
[(triple6)]
("tiger" "likes" "lion" "+")
triple6
The lion does not like the mouse.
False
1
inv-proof
[(triple1)]
("lion" "likes" "mouse" "-")
triple1
The lion likes the tiger.
True
2
proof
[(((triple6) -> rule3))]
("lion" "likes" "tiger" "+")
((triple6) -> (rule3 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The tiger does not visit the lion.
False
3
inv-proof
[(((triple3 triple5) -> rule1))]
("tiger" "visits" "lion" "-")
((triple3 triple5) -> (rule1 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The tiger is red.
True
4
proof
[(((((triple3 triple5) -> rule1)) -> rule4))]
("tiger" "is" "red" "+")
((((triple3 triple5) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The tiger is not red.
False
4
inv-proof
[(((((triple3 triple5) -> rule1)) -> rule4))]
("tiger" "is" "red" "-")
((((triple3 triple5) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The mouse likes the tiger.
True
6
proof
[(((((((triple3 triple5) -> rule1)) -> rule4) triple7) -> rule5))]
("mouse" "likes" "tiger" "+")
((((((triple3 triple5) -> (rule1 % int3))) -> (rule4 % int2)) triple7) -> (rule5 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int3
The mouse does not like the tiger.
False
6
inv-proof
[(((((((triple3 triple5) -> rule1)) -> rule4) triple7) -> rule5))]
("mouse" "likes" "tiger" "-")
((((((triple3 triple5) -> (rule1 % int3))) -> (rule4 % int2)) triple7) -> (rule5 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int3
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "red" "-")
The lion is red.
Unknown
rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "red" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The lion eats the mouse.
Unknown
random
[@0: The lion eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "mouse" "+")
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 is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The lion likes the mouse.[(triple1)] The mouse eats the lion.[(triple2)] The mouse is kind.[(triple3)] The mouse is round.[(triple4)] The mouse visits the tiger.[(triple5)] The tiger likes the lion.[(triple6)] The tiger visits the mouse.[(triple7)] @1: The lion likes the tiger.[(((triple6) -> rule3))] The tiger visits the lion.[(((triple3 triple5) -> rule1))] @2: The tiger is red.[(((((triple3 triple5) -> rule1)) -> rule4))] @3: The mouse likes the tiger.[(((((((triple3 triple5) -> rule1)) -> rule4) triple7) -> rule5))]
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The mouse is round.
("mouse" "is" "round" "+")
triple4
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple5
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
The lion likes the tiger.
("lion" "likes" "tiger" "+")
((triple6) -> (rule3 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
((triple3 triple5) -> (rule1 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((((triple3 triple5) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((((((triple3 triple5) -> (rule1 % int3))) -> (rule4 % int2)) triple7) -> (rule5 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int3