The bear is young. The bear likes the cow. The cow likes the bear. The cow sees the bear. The dog is kind. The dog is red. The dog sees the mouse. The dog visits the bear. The mouse is young. The mouse visits the cow. If someone likes the cow then the cow likes the dog. If someone likes the mouse then they see the mouse. If someone likes the dog then they see the cow.
The bear is young.
("bear" "is" "young" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If someone likes the cow then the cow likes the dog.
((("someone" "likes" "cow" "+")) -> ("cow" "likes" "dog" "+"))
If someone likes the mouse then they see the mouse.
((("someone" "likes" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
If someone likes the dog then they see the cow.
((("someone" "likes" "dog" "+")) -> ("someone" "sees" "cow" "+"))
The dog visits the bear.
True
1
proof
[(triple8)]
("dog" "visits" "bear" "+")
triple8
The dog is not kind.
False
1
inv-proof
[(triple5)]
("dog" "is" "kind" "-")
triple5
The cow likes the dog.
True
2
proof
[(((triple2) -> rule1))]
("cow" "likes" "dog" "+")
((triple2) -> (rule1 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The cow does not like the dog.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "likes" "dog" "-")
((triple2) -> (rule1 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The cow sees the cow.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("cow" "sees" "cow" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The cow does not see the cow.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("cow" "sees" "cow" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The dog does not see the cow.
Unknown
inv-rconc
[@1: The dog sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "cow" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse does not see the cow.
Unknown
inv-rconc
[@1: The mouse sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "cow" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
@0: The bear is young.[(triple1)] The bear likes the cow.[(triple2)] The cow likes the bear.[(triple3)] The cow sees the bear.[(triple4)] The dog is kind.[(triple5)] The dog is red.[(triple6)] The dog sees the mouse.[(triple7)] The dog visits the bear.[(triple8)] The mouse is young.[(triple9)] The mouse visits the cow.[(triple10)] @1: The cow likes the dog.[(((triple2) -> rule1))] @2: The cow sees the cow.[(((((triple2) -> rule1)) -> rule3))]
The bear is young.
("bear" "is" "young" "+")
triple1
The bear likes the cow.
("bear" "likes" "cow" "+")
triple2
The cow likes the bear.
("cow" "likes" "bear" "+")
triple3
The cow sees the bear.
("cow" "sees" "bear" "+")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple5
The dog is red.
("dog" "is" "red" "+")
triple6
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple7
The dog visits the bear.
("dog" "visits" "bear" "+")
triple8
The mouse is young.
("mouse" "is" "young" "+")
triple9
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple10
The cow likes the dog.
("cow" "likes" "dog" "+")
((triple2) -> (rule1 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2