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