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