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