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