The lion is big. The lion is round. The lion sees the mouse. The lion sees the tiger. The lion visits the tiger. The mouse is blue. The mouse likes the lion. The mouse visits the tiger. The rabbit likes the lion. The rabbit sees the lion. The rabbit visits the mouse. The tiger is blue. The tiger is nice. The tiger sees the lion. The tiger sees the rabbit. If the rabbit likes the lion then the rabbit is blue.
The lion is big.
("lion" "is" "big" "+")
The lion is round.
("lion" "is" "round" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If the rabbit likes the lion then the rabbit is blue.
((("rabbit" "likes" "lion" "+")) -> ("rabbit" "is" "blue" "+"))
The lion is round.
True
1
proof
[(triple2)]
("lion" "is" "round" "+")
triple2
The tiger is not blue.
False
1
inv-proof
[(triple12)]
("tiger" "is" "blue" "-")
triple12
The rabbit is blue.
True
2
proof
[(((triple9) -> rule1))]
("rabbit" "is" "blue" "+")
((triple9) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is not blue.
False
2
inv-proof
[(((triple9) -> rule1))]
("rabbit" "is" "blue" "-")
((triple9) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The mouse does not visit the rabbit.
Unknown
inv-random
[@0: The mouse visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "rabbit" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The tiger does not see the mouse.
Unknown
inv-random
[@0: The tiger sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "mouse" "-")
The mouse visits the lion.
Unknown
random
[@0: The mouse visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "lion" "+")
@0: The lion is big.[(triple1)] The lion is round.[(triple2)] The lion sees the mouse.[(triple3)] The lion sees the tiger.[(triple4)] The lion visits the tiger.[(triple5)] The mouse is blue.[(triple6)] The mouse likes the lion.[(triple7)] The mouse visits the tiger.[(triple8)] The rabbit likes the lion.[(triple9)] The rabbit sees the lion.[(triple10)] The rabbit visits the mouse.[(triple11)] The tiger is blue.[(triple12)] The tiger is nice.[(triple13)] The tiger sees the lion.[(triple14)] The tiger sees the rabbit.[(triple15)] @1: The rabbit is blue.[(((triple9) -> rule1))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is round.
("lion" "is" "round" "+")
triple2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple4
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple5
The mouse is blue.
("mouse" "is" "blue" "+")
triple6
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple7
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple8
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple9
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple10
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple11
The tiger is blue.
("tiger" "is" "blue" "+")
triple12
The tiger is nice.
("tiger" "is" "nice" "+")
triple13
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple14
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple15
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple9) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1