The cat is red. The cat likes the dog. The cat needs the dog. The dog is cold. The dog likes the cat. The mouse is green. The mouse likes the dog. The mouse needs the cat. The mouse sees the cat. The mouse sees the dog. If something is red then it needs the cat. If something needs the dog then it needs the mouse. If something is red then it likes the cat. If something sees the cat and the cat sees the dog then the cat needs the mouse. If something likes the dog and the dog likes the mouse then it needs the mouse. Green things are rough. If something is green and young then it sees the dog. If something is rough then it needs the dog.
The cat is red.
("cat" "is" "red" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If something is red then it needs the cat.
((("something" "is" "red" "+")) -> ("something" "needs" "cat" "+"))
If something needs the dog then it needs the mouse.
((("something" "needs" "dog" "+")) -> ("something" "needs" "mouse" "+"))
If something is red then it likes the cat.
((("something" "is" "red" "+")) -> ("something" "likes" "cat" "+"))
If something sees the cat and the cat sees the dog then the cat needs the mouse.
((("something" "sees" "cat" "+") ("cat" "sees" "dog" "+")) -> ("cat" "needs" "mouse" "+"))
If something likes the dog and the dog likes the mouse then it needs the mouse.
((("something" "likes" "dog" "+") ("dog" "likes" "mouse" "+")) -> ("something" "needs" "mouse" "+"))
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If something is green and young then it sees the dog.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "sees" "dog" "+"))
If something is rough then it needs the dog.
((("something" "is" "rough" "+")) -> ("something" "needs" "dog" "+"))
The mouse sees the dog.
True
1
proof
[(triple10)]
("mouse" "sees" "dog" "+")
triple10
The mouse does not need the cat.
False
1
inv-proof
[(triple8)]
("mouse" "needs" "cat" "-")
triple8
The mouse is rough.
True
2
proof
[(((triple6) -> rule6))]
("mouse" "is" "rough" "+")
((triple6) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "needs" "cat" "-")
((triple1) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The mouse needs the dog.
True
3
proof
[(((((triple6) -> rule6)) -> rule8))]
("mouse" "needs" "dog" "+")
((((triple6) -> (rule6 % int2))) -> (rule8 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse does not need the dog.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule8))]
("mouse" "needs" "dog" "-")
((((triple6) -> (rule6 % int2))) -> (rule8 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse needs the mouse.
True
4
proof
[(((((((triple6) -> rule6)) -> rule8)) -> rule2))]
("mouse" "needs" "mouse" "+")
((((((triple6) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse does not need the mouse.
False
4
inv-proof
[(((((((triple6) -> rule6)) -> rule8)) -> rule2))]
("mouse" "needs" "mouse" "-")
((((((triple6) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The dog does not need the mouse.
Unknown
inv-rconc
[@3: The dog needs the mouse.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule6 <- FAIL)]]
("dog" "needs" "mouse" "-")
The dog needs the dog.
Unknown
rconc
[@2: The dog needs the dog.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("dog" "needs" "dog" "+")
The mouse does not like the cat.
Unknown
inv-rconc
[@1: The mouse likes the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "likes" "cat" "-")
The dog needs the cat.
Unknown
rconc
[@1: The dog needs the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "needs" "cat" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The dog sees the mouse.
Unknown
random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "+")
@0: The cat is red.[(triple1)] The cat likes the dog.[(triple2)] The cat needs the dog.[(triple3)] The dog is cold.[(triple4)] The dog likes the cat.[(triple5)] The mouse is green.[(triple6)] The mouse likes the dog.[(triple7)] The mouse needs the cat.[(triple8)] The mouse sees the cat.[(triple9)] The mouse sees the dog.[(triple10)] @1: The cat likes the cat.[(((triple1) -> rule3))] The cat needs the cat.[(((triple1) -> rule1))] The cat needs the mouse.[(((triple3) -> rule2))] The mouse is rough.[(((triple6) -> rule6))] @2: The mouse needs the dog.[(((((triple6) -> rule6)) -> rule8))] @3: The mouse needs the mouse.[(((((((triple6) -> rule6)) -> rule8)) -> rule2))]
The cat is red.
("cat" "is" "red" "+")
triple1
The cat likes the dog.
("cat" "likes" "dog" "+")
triple2
The cat needs the dog.
("cat" "needs" "dog" "+")
triple3
The dog is cold.
("dog" "is" "cold" "+")
triple4
The dog likes the cat.
("dog" "likes" "cat" "+")
triple5
The mouse is green.
("mouse" "is" "green" "+")
triple6
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple7
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple8
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple9
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple10
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple1) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple1) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
((triple3) -> (rule2 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((triple6) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
((((triple6) -> (rule6 % int2))) -> (rule8 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((((triple6) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3