The cat visits the mouse. The mouse chases the cat. The mouse sees the cat. If someone chases the cat and the cat visits the mouse then they chase the mouse. If someone chases the mouse and the mouse sees the cat then the cat is kind.
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If someone chases the cat and the cat visits the mouse then they chase the mouse.
((("someone" "chases" "cat" "+") ("cat" "visits" "mouse" "+")) -> ("someone" "chases" "mouse" "+"))
If someone chases the mouse and the mouse sees the cat then the cat is kind.
((("someone" "chases" "mouse" "+") ("mouse" "sees" "cat" "+")) -> ("cat" "is" "kind" "+"))
The mouse chases the cat.
True
1
proof
[(triple2)]
("mouse" "chases" "cat" "+")
triple2
The cat does not visit the mouse.
False
1
inv-proof
[(triple1)]
("cat" "visits" "mouse" "-")
triple1
The mouse chases the mouse.
True
3
proof
[(((triple2 triple1) -> rule1))]
("mouse" "chases" "mouse" "+")
((triple2 triple1) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not chase the mouse.
False
3
inv-proof
[(((triple2 triple1) -> rule1))]
("mouse" "chases" "mouse" "-")
((triple2 triple1) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The cat is kind.
True
5
proof
[(((((triple2 triple1) -> rule1) triple3) -> rule2))]
("cat" "is" "kind" "+")
((((triple2 triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The cat is not kind.
False
5
inv-proof
[(((((triple2 triple1) -> rule1) triple3) -> rule2))]
("cat" "is" "kind" "-")
((((triple2 triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The cat does not chase the mouse.
Unknown
inv-rconc
[@1: The cat chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "mouse" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The cat sees the mouse.
Unknown
random
[@0: The cat sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "mouse" "+")
@0: The cat visits the mouse.[(triple1)] The mouse chases the cat.[(triple2)] The mouse sees the cat.[(triple3)] @1: The mouse chases the mouse.[(((triple2 triple1) -> rule1))] @2: The cat is kind.[(((((triple2 triple1) -> rule1) triple3) -> rule2))]
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple3
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple2 triple1) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
((((triple2 triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2