The cow is rough. The cow likes the dog. The dog likes the cow. If something sees the cow then the cow visits the dog. If something likes the dog then the dog sees the cow.
The cow is rough.
("cow" "is" "rough" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The dog likes the cow.
("dog" "likes" "cow" "+")
If something sees the cow then the cow visits the dog.
((("something" "sees" "cow" "+")) -> ("cow" "visits" "dog" "+"))
If something likes the dog then the dog sees the cow.
((("something" "likes" "dog" "+")) -> ("dog" "sees" "cow" "+"))
The dog likes the cow.
True
1
proof
[(triple3)]
("dog" "likes" "cow" "+")
triple3
The cow is not rough.
False
1
inv-proof
[(triple1)]
("cow" "is" "rough" "-")
triple1
The dog sees the cow.
True
2
proof
[(((triple2) -> rule2))]
("dog" "sees" "cow" "+")
((triple2) -> (rule2 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The dog does not see the cow.
False
2
inv-proof
[(((triple2) -> rule2))]
("dog" "sees" "cow" "-")
((triple2) -> (rule2 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The cow visits the dog.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("cow" "visits" "dog" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The cow does not visit the dog.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("cow" "visits" "dog" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
@0: The cow is rough.[(triple1)] The cow likes the dog.[(triple2)] The dog likes the cow.[(triple3)] @1: The dog sees the cow.[(((triple2) -> rule2))] @2: The cow visits the dog.[(((((triple2) -> rule2)) -> rule1))]
The cow is rough.
("cow" "is" "rough" "+")
triple1
The cow likes the dog.
("cow" "likes" "dog" "+")
triple2
The dog likes the cow.
("dog" "likes" "cow" "+")
triple3
The dog sees the cow.
("dog" "sees" "cow" "+")
((triple2) -> (rule2 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2