The cat likes the mouse. The cow does not like the dog. The dog is nice. The mouse needs the cow. If something is nice and not blue then it likes the cat. If something likes the cow and the cow visits the cat then the cat needs the mouse. If something is nice then it needs the cat. If something visits the cat and it needs the dog then it likes the mouse. If something needs the cat then it does not visit the cat. If something needs the dog and it is not red then the dog does not like the mouse. If the dog is round and the dog needs the cow then the dog does not need the cat. If something likes the cat then the cat likes the mouse.
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cow does not like the dog.
("cow" "likes" "dog" "-")
The dog is nice.
("dog" "is" "nice" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
If something is nice and not blue then it likes the cat.
((("something" "is" "nice" "+") ("something" "is" "blue" "~")) -> ("something" "likes" "cat" "+"))
If something likes the cow and the cow visits the cat then the cat needs the mouse.
((("something" "likes" "cow" "+") ("cow" "visits" "cat" "+")) -> ("cat" "needs" "mouse" "+"))
If something is nice then it needs the cat.
((("something" "is" "nice" "+")) -> ("something" "needs" "cat" "+"))
If something visits the cat and it needs the dog then it likes the mouse.
((("something" "visits" "cat" "+") ("something" "needs" "dog" "+")) -> ("something" "likes" "mouse" "+"))
If something needs the cat then it does not visit the cat.
((("something" "needs" "cat" "+")) -> ("something" "visits" "cat" "-"))
If something needs the dog and it is not red then the dog does not like the mouse.
((("something" "needs" "dog" "+") ("something" "is" "red" "~")) -> ("dog" "likes" "mouse" "-"))
If the dog is round and the dog needs the cow then the dog does not need the cat.
((("dog" "is" "round" "+") ("dog" "needs" "cow" "+")) -> ("dog" "needs" "cat" "-"))
If something likes the cat then the cat likes the mouse.
((("something" "likes" "cat" "+")) -> ("cat" "likes" "mouse" "+"))
The dog is nice.
True
1
proof
[(triple3)]
("dog" "is" "nice" "+")
triple3
The cat does not like the mouse.
False
1
inv-proof
[(triple1)]
("cat" "likes" "mouse" "-")
triple1
The dog needs the cat.
True
2
proof
[(((triple3) -> rule3))]
("dog" "needs" "cat" "+")
((triple3) -> (rule3 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The dog does not need the cat.
False
2
inv-proof
[(((triple3) -> rule3))]
("dog" "needs" "cat" "-")
((triple3) -> (rule3 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The dog does not visit the cat.
True
3
proof
[(((((triple3) -> rule3)) -> rule5))]
("dog" "visits" "cat" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The dog does not visit the cat.
("dog" "visits" "cat" "-")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
The dog visits the cat.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule5))]
("dog" "visits" "cat" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The dog does not visit the cat.
("dog" "visits" "cat" "-")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
The cow does not like the cat.
Unknown
inv-rconc
[@1: The cow likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "cat" "-")
The cat needs the cat.
Unknown
rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "needs" "cat" "+")
The dog does not like the cat.
Unknown
inv-rconc
[@1: The dog likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "likes" "cat" "-")
The cow visits the mouse.
Unknown
random
[@0: The cow visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "mouse" "+")
The cat does not visit the mouse.
Unknown
inv-random
[@0: The cat visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "mouse" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The cat likes the mouse.[(triple1)] The cow does not like the dog.[(triple2)] The dog is nice.[(triple3)] The mouse needs the cow.[(triple4)] @1: The dog needs the cat.[(((triple3) -> rule3))] @2: The dog does not visit the cat.[(((((triple3) -> rule3)) -> rule5))]
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple1
The cow does not like the dog.
("cow" "likes" "dog" "-")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple4
The dog needs the cat.
("dog" "needs" "cat" "+")
((triple3) -> (rule3 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The dog does not visit the cat.
("dog" "visits" "cat" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The dog does not visit the cat.
("dog" "visits" "cat" "-")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2