The cat eats the mouse. The mouse chases the cat. The mouse visits the cat. If something chases the cat then it is kind. If something is nice and blue then it chases the cat. If something is round and it eats the mouse then the mouse visits the cat. If the mouse visits the cat and the cat is kind then the cat visits the mouse. If something chases the cat and the cat is kind then the cat is nice. If something visits the cat then the cat is nice. If something eats the cat then it visits the cat. If the cat is nice and the cat eats the mouse then the cat is kind.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If something chases the cat then it is kind.
((("something" "chases" "cat" "+")) -> ("something" "is" "kind" "+"))
If something is nice and blue then it chases the cat.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "chases" "cat" "+"))
If something is round and it eats the mouse then the mouse visits the cat.
((("something" "is" "round" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "visits" "cat" "+"))
If the mouse visits the cat and the cat is kind then the cat visits the mouse.
((("mouse" "visits" "cat" "+") ("cat" "is" "kind" "+")) -> ("cat" "visits" "mouse" "+"))
If something chases the cat and the cat is kind then the cat is nice.
((("something" "chases" "cat" "+") ("cat" "is" "kind" "+")) -> ("cat" "is" "nice" "+"))
If something visits the cat then the cat is nice.
((("something" "visits" "cat" "+")) -> ("cat" "is" "nice" "+"))
If something eats the cat then it visits the cat.
((("something" "eats" "cat" "+")) -> ("something" "visits" "cat" "+"))
If the cat is nice and the cat eats the mouse then the cat is kind.
((("cat" "is" "nice" "+") ("cat" "eats" "mouse" "+")) -> ("cat" "is" "kind" "+"))
The mouse visits the cat.
True
1
proof
[(triple3)]
("mouse" "visits" "cat" "+")
triple3
The mouse does not chase the cat.
False
1
inv-proof
[(triple2)]
("mouse" "chases" "cat" "-")
triple2
The mouse is kind.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "is" "kind" "+")
((triple2) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is not kind.
False
2
inv-proof
[(((triple2) -> rule1))]
("mouse" "is" "kind" "-")
((triple2) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The cat is kind.
True
4
proof
[(((((triple3) -> rule6) triple1) -> rule8))]
("cat" "is" "kind" "+")
((((triple3) -> (rule6 % int2)) triple1) -> (rule8 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is not kind.
False
4
inv-proof
[(((((triple3) -> rule6) triple1) -> rule8))]
("cat" "is" "kind" "-")
((((triple3) -> (rule6 % int2)) triple1) -> (rule8 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat visits the mouse.
True
6
proof
[(((triple3 ((((triple3) -> rule6) triple1) -> rule8)) -> rule4))]
("cat" "visits" "mouse" "+")
((triple3 ((((triple3) -> (rule6 % int3)) triple1) -> (rule8 % int2))) -> (rule4 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat does not visit the mouse.
False
6
inv-proof
[(((triple3 ((((triple3) -> rule6) triple1) -> rule8)) -> rule4))]
("cat" "visits" "mouse" "-")
((triple3 ((((triple3) -> (rule6 % int3)) triple1) -> (rule8 % int2))) -> (rule4 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "visits" "cat" "-")
The cat chases the cat.
Unknown
rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "chases" "cat" "+")
The cat does not chase the mouse.
Unknown
inv-random
[@0: The cat chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "mouse" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The mouse is not nice.
Unknown
inv-random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The cat eats the mouse.[(triple1)] The mouse chases the cat.[(triple2)] The mouse visits the cat.[(triple3)] @1: The cat is nice.[(((triple3) -> rule6))] The mouse is kind.[(((triple2) -> rule1))] @2: The cat is kind.[(((((triple3) -> rule6) triple1) -> rule8))] @3: The cat visits the mouse.[(((triple3 ((((triple3) -> rule6) triple1) -> rule8)) -> rule4))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
((triple3) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((triple2) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
((((triple3) -> (rule6 % int2)) triple1) -> (rule8 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
((triple3 ((((triple3) -> (rule6 % int3)) triple1) -> (rule8 % int2))) -> (rule4 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3