The mouse is big. The mouse needs the tiger. The rabbit is big. The rabbit is kind. The rabbit is red. The rabbit likes the tiger. The rabbit sees the tiger. The tiger is big. The tiger is kind. The tiger is rough. The tiger needs the mouse. The tiger sees the mouse. If something is kind then it needs the tiger. Kind things are blue. If something needs the tiger then it likes the rabbit.
The mouse is big.
("mouse" "is" "big" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something is kind then it needs the tiger.
((("something" "is" "kind" "+")) -> ("something" "needs" "tiger" "+"))
Kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something needs the tiger then it likes the rabbit.
((("something" "needs" "tiger" "+")) -> ("something" "likes" "rabbit" "+"))
The tiger is kind.
True
1
proof
[(triple9)]
("tiger" "is" "kind" "+")
triple9
The mouse is not big.
False
1
inv-proof
[(triple1)]
("mouse" "is" "big" "-")
triple1
The rabbit is blue.
True
2
proof
[(((triple4) -> rule2))]
("rabbit" "is" "blue" "+")
((triple4) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is not blue.
False
2
inv-proof
[(((triple4) -> rule2))]
("rabbit" "is" "blue" "-")
((triple4) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The tiger likes the rabbit.
True
3
proof
[(((((triple9) -> rule1)) -> rule3))]
("tiger" "likes" "rabbit" "+")
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The rabbit does not like the rabbit.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule3))]
("rabbit" "likes" "rabbit" "-")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int2
The mouse is not blue.
Unknown
inv-rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "blue" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The mouse does not like the tiger.
Unknown
inv-random
[@0: The mouse likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "tiger" "-")
The tiger likes the mouse.
Unknown
random
[@0: The tiger likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "mouse" "+")
The mouse does not see the rabbit.
Unknown
inv-random
[@0: The mouse sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "rabbit" "-")
The mouse sees the tiger.
Unknown
random
[@0: The mouse sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "tiger" "+")
@0: The mouse is big.[(triple1)] The mouse needs the tiger.[(triple2)] The rabbit is big.[(triple3)] The rabbit is kind.[(triple4)] The rabbit is red.[(triple5)] The rabbit likes the tiger.[(triple6)] The rabbit sees the tiger.[(triple7)] The tiger is big.[(triple8)] The tiger is kind.[(triple9)] The tiger is rough.[(triple10)] The tiger needs the mouse.[(triple11)] The tiger sees the mouse.[(triple12)] @1: The mouse likes the rabbit.[(((triple2) -> rule3))] The rabbit is blue.[(((triple4) -> rule2))] The rabbit needs the tiger.[(((triple4) -> rule1))] The tiger is blue.[(((triple9) -> rule2))] The tiger needs the tiger.[(((triple9) -> rule1))] @2: The rabbit likes the rabbit.[(((((triple4) -> rule1)) -> rule3))] The tiger likes the rabbit.[(((((triple9) -> rule1)) -> rule3))]
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple2
The rabbit is big.
("rabbit" "is" "big" "+")
triple3
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple6
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple7
The tiger is big.
("tiger" "is" "big" "+")
triple8
The tiger is kind.
("tiger" "is" "kind" "+")
triple9
The tiger is rough.
("tiger" "is" "rough" "+")
triple10
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple11
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple12
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((triple2) -> (rule3 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple4) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
((triple4) -> (rule1 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple9) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple9) -> (rule1 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int2
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2