The cat eats the mouse. The cat is red. The mouse is rough. The rabbit is round. The squirrel eats the cat. The squirrel is round. The squirrel needs the cat. If something eats the mouse then it chases the mouse.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is red.
("cat" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
If something eats the mouse then it chases the mouse.
((("something" "eats" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
The cat eats the mouse.
True
1
proof
[(triple1)]
("cat" "eats" "mouse" "+")
triple1
The mouse is not rough.
False
1
inv-proof
[(triple3)]
("mouse" "is" "rough" "-")
triple3
The cat chases the mouse.
True
2
proof
[(((triple1) -> rule1))]
("cat" "chases" "mouse" "+")
((triple1) -> (rule1 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat does not chase the mouse.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "chases" "mouse" "-")
((triple1) -> (rule1 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The squirrel chases the mouse.
Unknown
rconc
[@1: The squirrel chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "mouse" "+")
The rabbit does not need the squirrel.
Unknown
inv-random
[@0: The rabbit needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "squirrel" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat eats the mouse.[(triple1)] The cat is red.[(triple2)] The mouse is rough.[(triple3)] The rabbit is round.[(triple4)] The squirrel eats the cat.[(triple5)] The squirrel is round.[(triple6)] The squirrel needs the cat.[(triple7)] @1: The cat chases the mouse.[(((triple1) -> rule1))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
The rabbit is round.
("rabbit" "is" "round" "+")
triple4
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple5
The squirrel is round.
("squirrel" "is" "round" "+")
triple6
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple7
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((triple1) -> (rule1 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1