The cat chases the mouse. The cat eats the mouse. The cat eats the squirrel. The cat is not red. The mouse does not chase the cat. The mouse is not kind. The mouse visits the squirrel. The squirrel eats the cat. The squirrel eats the mouse. The squirrel visits the mouse. If someone eats the mouse then they eat the squirrel. If someone eats the squirrel and they eat the mouse then they chase the squirrel.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is not red.
("cat" "is" "red" "-")
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
The mouse is not kind.
("mouse" "is" "kind" "-")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If someone eats the mouse then they eat the squirrel.
((("someone" "eats" "mouse" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone eats the squirrel and they eat the mouse then they chase the squirrel.
((("someone" "eats" "squirrel" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "chases" "squirrel" "+"))
The cat eats the squirrel.
True
1
proof
[(triple3 OR ((triple2) -> rule1))]
("cat" "eats" "squirrel" "+")
triple3
((triple2) -> (rule1 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat does not chase the mouse.
False
1
inv-proof
[(triple1)]
("cat" "chases" "mouse" "-")
triple1
The cat chases the squirrel.
True
3
proof
[(((triple3 triple2) -> rule2) OR ((((triple2) -> rule1) triple2) -> rule2))]
("cat" "chases" "squirrel" "+")
((triple3 triple2) -> (rule2 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat does not chase the squirrel.
False
3
inv-proof
[(((triple3 triple2) -> rule2) OR ((((triple2) -> rule1) triple2) -> rule2))]
("cat" "chases" "squirrel" "-")
((triple3 triple2) -> (rule2 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The squirrel chases the squirrel.
True
4
proof
[(((((triple9) -> rule1) triple9) -> rule2))]
("squirrel" "chases" "squirrel" "+")
((((triple9) -> (rule1 % int2)) triple9) -> (rule2 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel does not chase the squirrel.
False
4
inv-proof
[(((((triple9) -> rule1) triple9) -> rule2))]
("squirrel" "chases" "squirrel" "-")
((((triple9) -> (rule1 % int2)) triple9) -> (rule2 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The mouse does not chase the squirrel.
Unknown
inv-rconc
[@1: The mouse chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "squirrel" "-")
The mouse eats the squirrel.
Unknown
rconc
[@1: The mouse eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "eats" "squirrel" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse visits the cat.
Unknown
random
[@0: The mouse visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cat" "+")
The squirrel does not chase the cat.
Unknown
inv-random
[@0: The squirrel chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "cat" "-")
The squirrel visits the cat.
Unknown
random
[@0: The squirrel visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cat" "+")
@0: The cat chases the mouse.[(triple1)] The cat eats the mouse.[(triple2)] The cat eats the squirrel.[(triple3 OR ((triple2) -> rule1))] The cat is not red.[(triple4)] The mouse does not chase the cat.[(triple5)] The mouse is not kind.[(triple6)] The mouse visits the squirrel.[(triple7)] The squirrel eats the cat.[(triple8)] The squirrel eats the mouse.[(triple9)] The squirrel visits the mouse.[(triple10)] @1: The cat chases the squirrel.[(((triple3 triple2) -> rule2) OR ((((triple2) -> rule1) triple2) -> rule2))] The squirrel eats the squirrel.[(((triple9) -> rule1))] @2: The squirrel chases the squirrel.[(((((triple9) -> rule1) triple9) -> rule2))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple3
((triple2) -> (rule1 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat is not red.
("cat" "is" "red" "-")
triple4
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
triple5
The mouse is not kind.
("mouse" "is" "kind" "-")
triple6
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple7
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple8
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple9
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple10
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
((triple3 triple2) -> (rule2 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple9) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((((triple9) -> (rule1 % int2)) triple9) -> (rule2 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2