The cow likes the dog. The cow needs the mouse. The cow needs the rabbit. The cow visits the mouse. The dog is cold. The dog needs the mouse. The dog does not visit the cow. The dog visits the rabbit. The mouse visits the cow. The rabbit is big. The rabbit likes the cow. The rabbit needs the mouse. If something needs the rabbit then it likes the cow. If something needs the dog and it is not red then the dog is big.
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog does not visit the cow.
("dog" "visits" "cow" "-")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If something needs the rabbit then it likes the cow.
((("something" "needs" "rabbit" "+")) -> ("something" "likes" "cow" "+"))
If something needs the dog and it is not red then the dog is big.
((("something" "needs" "dog" "+") ("something" "is" "red" "~")) -> ("dog" "is" "big" "+"))
The rabbit likes the cow.
True
1
proof
[(triple11)]
("rabbit" "likes" "cow" "+")
triple11
The mouse does not visit the cow.
False
1
inv-proof
[(triple9)]
("mouse" "visits" "cow" "-")
triple9
The cow likes the cow.
True
2
proof
[(((triple3) -> rule1))]
("cow" "likes" "cow" "+")
((triple3) -> (rule1 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow does not like the cow.
False
2
inv-proof
[(((triple3) -> rule1))]
("cow" "likes" "cow" "-")
((triple3) -> (rule1 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "big" "-")
The mouse likes the cow.
Unknown
rconc
[@1: The mouse likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "cow" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The cow likes the dog.[(triple1)] The cow needs the mouse.[(triple2)] The cow needs the rabbit.[(triple3)] The cow visits the mouse.[(triple4)] The dog does not visit the cow.[(triple7)] The dog is cold.[(triple5)] The dog needs the mouse.[(triple6)] The dog visits the rabbit.[(triple8)] The mouse visits the cow.[(triple9)] The rabbit is big.[(triple10)] The rabbit likes the cow.[(triple11)] The rabbit needs the mouse.[(triple12)] @1: The cow likes the cow.[(((triple3) -> rule1))]
The cow likes the dog.
("cow" "likes" "dog" "+")
triple1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple3
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple4
The dog does not visit the cow.
("dog" "visits" "cow" "-")
triple7
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple6
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple8
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple9
The rabbit is big.
("rabbit" "is" "big" "+")
triple10
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple11
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple12
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple3) -> (rule1 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1