The cow chases the rabbit. The cow is blue. The cow likes the rabbit. The rabbit chases the cow. The rabbit is big. The rabbit likes the cow. The rabbit sees the cow. If something likes the rabbit then the rabbit is blue. If something likes the cow and the cow is kind then it is kind. If something is blue and it likes the cow then the cow is kind.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If something likes the rabbit then the rabbit is blue.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "is" "blue" "+"))
If something likes the cow and the cow is kind then it is kind.
((("something" "likes" "cow" "+") ("cow" "is" "kind" "+")) -> ("something" "is" "kind" "+"))
If something is blue and it likes the cow then the cow is kind.
((("something" "is" "blue" "+") ("something" "likes" "cow" "+")) -> ("cow" "is" "kind" "+"))
The rabbit likes the cow.
True
1
proof
[(triple6)]
("rabbit" "likes" "cow" "+")
triple6
The rabbit does not chase the cow.
False
1
inv-proof
[(triple4)]
("rabbit" "chases" "cow" "-")
triple4
The rabbit is blue.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "is" "blue" "+")
((triple3) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is not blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "is" "blue" "-")
((triple3) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cow is kind.
True
4
proof
[(((((triple3) -> rule1) triple6) -> rule3))]
("cow" "is" "kind" "+")
((((triple3) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The cow is not kind.
False
4
inv-proof
[(((((triple3) -> rule1) triple6) -> rule3))]
("cow" "is" "kind" "-")
((((triple3) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is kind.
True
6
proof
[(((triple6 ((((triple3) -> rule1) triple6) -> rule3)) -> rule2))]
("rabbit" "is" "kind" "+")
((triple6 ((((triple3) -> (rule1 % int3)) triple6) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The rabbit is not kind.
False
6
inv-proof
[(((triple6 ((((triple3) -> rule1) triple6) -> rule3)) -> rule2))]
("rabbit" "is" "kind" "-")
((triple6 ((((triple3) -> (rule1 % int3)) triple6) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow sees the rabbit.
Unknown
random
[@0: The cow sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "rabbit" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The cow chases the rabbit.[(triple1)] The cow is blue.[(triple2)] The cow likes the rabbit.[(triple3)] The rabbit chases the cow.[(triple4)] The rabbit is big.[(triple5)] The rabbit likes the cow.[(triple6)] The rabbit sees the cow.[(triple7)] @1: The rabbit is blue.[(((triple3) -> rule1))] @2: The cow is kind.[(((((triple3) -> rule1) triple6) -> rule3))] @3: The rabbit is kind.[(((triple6 ((((triple3) -> rule1) triple6) -> rule3)) -> rule2))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple3
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple4
The rabbit is big.
("rabbit" "is" "big" "+")
triple5
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple6
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple7
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple3) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((((triple3) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple6 ((((triple3) -> (rule1 % int3)) triple6) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3