The cat is not blue. The cat sees the cow. The cow eats the cat. The cow does not see the rabbit. The cow visits the rabbit. The mouse eats the cat. The mouse is green. The mouse is rough. The mouse sees the rabbit. The rabbit does not eat the cow. The rabbit eats the mouse. The rabbit is not red. The rabbit sees the cat. The rabbit sees the cow. The rabbit sees the mouse. If something is young then it does not see the rabbit. If the rabbit visits the mouse then the rabbit is young. Young things are not rough. If something is rough and it sees the rabbit then the rabbit does not visit the cat. If something eats the rabbit and it does not visit the cow then the cow is young. If something eats the mouse and it does not see the rabbit then it is not blue.
The cat is not blue.
("cat" "is" "blue" "-")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is not red.
("rabbit" "is" "red" "-")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If something is young then it does not see the rabbit.
((("something" "is" "young" "+")) -> ("something" "sees" "rabbit" "-"))
If the rabbit visits the mouse then the rabbit is young.
((("rabbit" "visits" "mouse" "+")) -> ("rabbit" "is" "young" "+"))
Young things are not rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "-"))
If something is rough and it sees the rabbit then the rabbit does not visit the cat.
((("something" "is" "rough" "+") ("something" "sees" "rabbit" "+")) -> ("rabbit" "visits" "cat" "-"))
If something eats the rabbit and it does not visit the cow then the cow is young.
((("something" "eats" "rabbit" "+") ("something" "visits" "cow" "~")) -> ("cow" "is" "young" "+"))
If something eats the mouse and it does not see the rabbit then it is not blue.
((("something" "eats" "mouse" "+") ("something" "sees" "rabbit" "~")) -> ("something" "is" "blue" "-"))
The rabbit sees the mouse.
True
1
proof
[(triple15)]
("rabbit" "sees" "mouse" "+")
triple15
The rabbit does not see the cat.
False
1
inv-proof
[(triple13)]
("rabbit" "sees" "cat" "-")
triple13
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "young" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cat is not blue.[(triple1)] The cat sees the cow.[(triple2)] The cow does not see the rabbit.[(triple4)] The cow eats the cat.[(triple3)] The cow visits the rabbit.[(triple5)] The mouse eats the cat.[(triple6)] The mouse is green.[(triple7)] The mouse is rough.[(triple8)] The mouse sees the rabbit.[(triple9)] The rabbit does not eat the cow.[(triple10)] The rabbit eats the mouse.[(triple11)] The rabbit is not red.[(triple12)] The rabbit sees the cat.[(triple13)] The rabbit sees the cow.[(triple14)] The rabbit sees the mouse.[(triple15)] @1: The rabbit does not visit the cat.[(((triple8 triple9) -> rule4))]
The cat is not blue.
("cat" "is" "blue" "-")
triple1
The cat sees the cow.
("cat" "sees" "cow" "+")
triple2
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
triple4
The cow eats the cat.
("cow" "eats" "cat" "+")
triple3
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple5
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple6
The mouse is green.
("mouse" "is" "green" "+")
triple7
The mouse is rough.
("mouse" "is" "rough" "+")
triple8
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple9
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
triple10
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple11
The rabbit is not red.
("rabbit" "is" "red" "-")
triple12
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple13
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple14
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple15
The rabbit does not visit the cat.
("rabbit" "visits" "cat" "-")
((triple8 triple9) -> (rule4 % int1))
The rabbit does not visit the cat.
("rabbit" "visits" "cat" "-")
int1