The cow is rough. The cow visits the dog. The cow visits the rabbit. The dog is blue. The dog likes the rabbit. The dog sees the rabbit. The dog visits the cow. The rabbit is round. The rabbit sees the cow. The rabbit sees the dog. If something sees the dog then it likes the rabbit. If something is rough then it sees the cow.
The cow is rough.
("cow" "is" "rough" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If something sees the dog then it likes the rabbit.
((("something" "sees" "dog" "+")) -> ("something" "likes" "rabbit" "+"))
If something is rough then it sees the cow.
((("something" "is" "rough" "+")) -> ("something" "sees" "cow" "+"))
The cow visits the dog.
True
1
proof
[(triple2)]
("cow" "visits" "dog" "+")
triple2
The rabbit does not see the dog.
False
1
inv-proof
[(triple10)]
("rabbit" "sees" "dog" "-")
triple10
The cow sees the cow.
True
2
proof
[(((triple1) -> rule2))]
("cow" "sees" "cow" "+")
((triple1) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The rabbit does not like the rabbit.
False
2
inv-proof
[(((triple10) -> rule1))]
("rabbit" "likes" "rabbit" "-")
((triple10) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The dog does not see the cow.
Unknown
inv-rconc
[@1: The dog sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "cow" "-")
The cow likes the rabbit.
Unknown
rconc
[@1: The cow likes the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "rabbit" "+")
The cow does not see the rabbit.
Unknown
inv-random
[@0: The cow sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "rabbit" "-")
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 rough.[(triple1)] The cow visits the dog.[(triple2)] The cow visits the rabbit.[(triple3)] The dog is blue.[(triple4)] The dog likes the rabbit.[(triple5)] The dog sees the rabbit.[(triple6)] The dog visits the cow.[(triple7)] The rabbit is round.[(triple8)] The rabbit sees the cow.[(triple9)] The rabbit sees the dog.[(triple10)] @1: The cow sees the cow.[(((triple1) -> rule2))] The rabbit likes the rabbit.[(((triple10) -> rule1))]
The cow is rough.
("cow" "is" "rough" "+")
triple1
The cow visits the dog.
("cow" "visits" "dog" "+")
triple2
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple3
The dog is blue.
("dog" "is" "blue" "+")
triple4
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple5
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple6
The dog visits the cow.
("dog" "visits" "cow" "+")
triple7
The rabbit is round.
("rabbit" "is" "round" "+")
triple8
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple9
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple10
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple1) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple10) -> (rule1 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1