The mouse eats the rabbit. The mouse is blue. The mouse is kind. The rabbit eats the tiger. The rabbit visits the mouse. The tiger eats the mouse. The tiger is cold. The tiger is not green. The tiger likes the rabbit. The tiger visits the rabbit. If someone likes the rabbit and the rabbit visits the tiger then the tiger is nice. If someone is kind and they like the rabbit then they do not eat the tiger. If the rabbit visits the mouse then the rabbit visits the tiger. If the tiger is green and the tiger is not cold then the tiger is blue. If someone likes the mouse and they are not green then the mouse is not kind. If someone is nice then they visit the mouse.
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is not green.
("tiger" "is" "green" "-")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If someone likes the rabbit and the rabbit visits the tiger then the tiger is nice.
((("someone" "likes" "rabbit" "+") ("rabbit" "visits" "tiger" "+")) -> ("tiger" "is" "nice" "+"))
If someone is kind and they like the rabbit then they do not eat the tiger.
((("someone" "is" "kind" "+") ("someone" "likes" "rabbit" "+")) -> ("someone" "eats" "tiger" "-"))
If the rabbit visits the mouse then the rabbit visits the tiger.
((("rabbit" "visits" "mouse" "+")) -> ("rabbit" "visits" "tiger" "+"))
If the tiger is green and the tiger is not cold then the tiger is blue.
((("tiger" "is" "green" "+") ("tiger" "is" "cold" "~")) -> ("tiger" "is" "blue" "+"))
If someone likes the mouse and they are not green then the mouse is not kind.
((("someone" "likes" "mouse" "+") ("someone" "is" "green" "~")) -> ("mouse" "is" "kind" "-"))
If someone is nice then they visit the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "mouse" "+"))
The mouse is blue.
True
1
proof
[(triple2)]
("mouse" "is" "blue" "+")
triple2
The rabbit does not visit the mouse.
False
1
inv-proof
[(triple5)]
("rabbit" "visits" "mouse" "-")
triple5
The rabbit visits the tiger.
True
2
proof
[(((triple5) -> rule3))]
("rabbit" "visits" "tiger" "+")
((triple5) -> (rule3 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit does not visit the tiger.
False
2
inv-proof
[(((triple5) -> rule3))]
("rabbit" "visits" "tiger" "-")
((triple5) -> (rule3 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The tiger is nice.
True
4
proof
[(((triple9 ((triple5) -> rule3)) -> rule1))]
("tiger" "is" "nice" "+")
((triple9 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The tiger is not nice.
False
4
inv-proof
[(((triple9 ((triple5) -> rule3)) -> rule1))]
("tiger" "is" "nice" "-")
((triple9 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The tiger visits the mouse.
True
5
proof
[(((((triple9 ((triple5) -> rule3)) -> rule1)) -> rule6))]
("tiger" "visits" "mouse" "+")
((((triple9 ((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The tiger does not visit the mouse.
False
5
inv-proof
[(((((triple9 ((triple5) -> rule3)) -> rule1)) -> rule6))]
("tiger" "visits" "mouse" "-")
((((triple9 ((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The tiger is not blue.
Unknown
inv-rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "blue" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The rabbit does not like the mouse.
Unknown
inv-random
[@0: The rabbit likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "mouse" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The mouse eats the rabbit.[(triple1)] The mouse is blue.[(triple2)] The mouse is kind.[(triple3)] The rabbit eats the tiger.[(triple4)] The rabbit visits the mouse.[(triple5)] The tiger eats the mouse.[(triple6)] The tiger is cold.[(triple7)] The tiger is not green.[(triple8)] The tiger likes the rabbit.[(triple9)] The tiger visits the rabbit.[(triple10)] @1: The rabbit visits the tiger.[(((triple5) -> rule3))] @2: The tiger is nice.[(((triple9 ((triple5) -> rule3)) -> rule1))] @3: The tiger visits the mouse.[(((((triple9 ((triple5) -> rule3)) -> rule1)) -> rule6))]
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple1
The mouse is blue.
("mouse" "is" "blue" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple4
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple5
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple6
The tiger is cold.
("tiger" "is" "cold" "+")
triple7
The tiger is not green.
("tiger" "is" "green" "-")
triple8
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple9
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple10
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
((triple5) -> (rule3 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple9 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((((triple9 ((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3