The cat needs the mouse. The dog needs the rabbit. The mouse does not need the rabbit. The rabbit eats the mouse. If something needs the dog then it likes the mouse. If something eats the mouse then it needs the dog. If something likes the dog then the dog is round. If something likes the cat then the cat eats the dog. If the cat likes the mouse then the mouse does not need the rabbit. If something eats the cat and it is not rough then the cat eats the mouse. Rough things are green. If something eats the rabbit and it is not green then the rabbit needs the mouse.
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The mouse does not need the rabbit.
("mouse" "needs" "rabbit" "-")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
If something needs the dog then it likes the mouse.
((("something" "needs" "dog" "+")) -> ("something" "likes" "mouse" "+"))
If something eats the mouse then it needs the dog.
((("something" "eats" "mouse" "+")) -> ("something" "needs" "dog" "+"))
If something likes the dog then the dog is round.
((("something" "likes" "dog" "+")) -> ("dog" "is" "round" "+"))
If something likes the cat then the cat eats the dog.
((("something" "likes" "cat" "+")) -> ("cat" "eats" "dog" "+"))
If the cat likes the mouse then the mouse does not need the rabbit.
((("cat" "likes" "mouse" "+")) -> ("mouse" "needs" "rabbit" "-"))
If something eats the cat and it is not rough then the cat eats the mouse.
((("something" "eats" "cat" "+") ("something" "is" "rough" "~")) -> ("cat" "eats" "mouse" "+"))
Rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something eats the rabbit and it is not green then the rabbit needs the mouse.
((("something" "eats" "rabbit" "+") ("something" "is" "green" "~")) -> ("rabbit" "needs" "mouse" "+"))
The cat needs the mouse.
True
1
proof
[(triple1)]
("cat" "needs" "mouse" "+")
triple1
The dog does not need the rabbit.
False
1
inv-proof
[(triple2)]
("dog" "needs" "rabbit" "-")
triple2
The rabbit needs the dog.
True
2
proof
[(((triple4) -> rule2))]
("rabbit" "needs" "dog" "+")
((triple4) -> (rule2 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit does not need the dog.
False
2
inv-proof
[(((triple4) -> rule2))]
("rabbit" "needs" "dog" "-")
((triple4) -> (rule2 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit likes the mouse.
True
3
proof
[(((((triple4) -> rule2)) -> rule1))]
("rabbit" "likes" "mouse" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The rabbit does not like the mouse.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule1))]
("rabbit" "likes" "mouse" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "round" "-")
The dog is green.
Unknown
rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "green" "+")
The cat does not eat the dog.
Unknown
inv-rconc
[@1: The cat eats the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "eats" "dog" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat needs the mouse.[(triple1)] The dog needs the rabbit.[(triple2)] The mouse does not need the rabbit.[(triple3)] The rabbit eats the mouse.[(triple4)] @1: The rabbit needs the dog.[(((triple4) -> rule2))] @2: The rabbit likes the mouse.[(((((triple4) -> rule2)) -> rule1))]
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple2
The mouse does not need the rabbit.
("mouse" "needs" "rabbit" "-")
triple3
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple4
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
((triple4) -> (rule2 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2