The cow likes the dog. The dog is blue. The dog is kind. The dog sees the cow. The rabbit is nice. The rabbit does not like the cow. The rabbit sees the cow. If something sees the cow then the cow sees the dog. If something likes the cow then the cow is not rough. If something visits the cow and it likes the rabbit then the rabbit is nice. If something is blue and nice then it does not like the dog. If the cow is rough and the cow does not like the dog then the cow visits the dog. If the dog is nice and the dog sees the cow then the cow does not visit the dog.
The cow likes the dog.
("cow" "likes" "dog" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit does not like the cow.
("rabbit" "likes" "cow" "-")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If something sees the cow then the cow sees the dog.
((("something" "sees" "cow" "+")) -> ("cow" "sees" "dog" "+"))
If something likes the cow then the cow is not rough.
((("something" "likes" "cow" "+")) -> ("cow" "is" "rough" "-"))
If something visits the cow and it likes the rabbit then the rabbit is nice.
((("something" "visits" "cow" "+") ("something" "likes" "rabbit" "+")) -> ("rabbit" "is" "nice" "+"))
If something is blue and nice then it does not like the dog.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "likes" "dog" "-"))
If the cow is rough and the cow does not like the dog then the cow visits the dog.
((("cow" "is" "rough" "+") ("cow" "likes" "dog" "~")) -> ("cow" "visits" "dog" "+"))
If the dog is nice and the dog sees the cow then the cow does not visit the dog.
((("dog" "is" "nice" "+") ("dog" "sees" "cow" "+")) -> ("cow" "visits" "dog" "-"))
The cow likes the dog.
True
1
proof
[(triple1)]
("cow" "likes" "dog" "+")
triple1
The rabbit does not see the cow.
False
1
inv-proof
[(triple7)]
("rabbit" "sees" "cow" "-")
triple7
The cow sees the dog.
True
2
proof
[(((triple4) -> rule1) OR ((triple7) -> rule1))]
("cow" "sees" "dog" "+")
((triple4) -> (rule1 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
((triple7) -> (rule1 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow does not see the dog.
False
2
inv-proof
[(((triple4) -> rule1) OR ((triple7) -> rule1))]
("cow" "sees" "dog" "-")
((triple4) -> (rule1 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
((triple7) -> (rule1 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow does not visit the dog.
Unknown
inv-rconc
[@1: The cow visits the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "visits" "dog" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The cow likes the rabbit.
Unknown
random
[@0: The cow likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "rabbit" "+")
@0: The cow likes the dog.[(triple1)] The dog is blue.[(triple2)] The dog is kind.[(triple3)] The dog sees the cow.[(triple4)] The rabbit does not like the cow.[(triple6)] The rabbit is nice.[(triple5)] The rabbit sees the cow.[(triple7)] @1: The cow sees the dog.[(((triple4) -> rule1) OR ((triple7) -> rule1))]
The cow likes the dog.
("cow" "likes" "dog" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog sees the cow.
("dog" "sees" "cow" "+")
triple4
The rabbit does not like the cow.
("rabbit" "likes" "cow" "-")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple5
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple7
The cow sees the dog.
("cow" "sees" "dog" "+")
((triple4) -> (rule1 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
((triple7) -> (rule1 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1