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