The cat chases the mouse. The cat is cold. The mouse chases the cat. If something visits the mouse then the mouse chases the cat. If the cat chases the mouse then the cat visits the mouse. If something visits the mouse then the mouse is rough.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat is cold.
("cat" "is" "cold" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
If something visits the mouse then the mouse chases the cat.
((("something" "visits" "mouse" "+")) -> ("mouse" "chases" "cat" "+"))
If the cat chases the mouse then the cat visits the mouse.
((("cat" "chases" "mouse" "+")) -> ("cat" "visits" "mouse" "+"))
If something visits the mouse then the mouse is rough.
((("something" "visits" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
The cat chases the mouse.
True
1
proof
[(triple1)]
("cat" "chases" "mouse" "+")
triple1
The cat does not chase the mouse.
False
1
inv-proof
[(triple1)]
("cat" "chases" "mouse" "-")
triple1
The cat visits the mouse.
True
2
proof
[(((triple1) -> rule2))]
("cat" "visits" "mouse" "+")
((triple1) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat does not visit the mouse.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "visits" "mouse" "-")
((triple1) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The mouse is rough.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("mouse" "is" "rough" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The mouse is not rough.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("mouse" "is" "rough" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The cat chases the mouse.[(triple1)] The cat is cold.[(triple2)] The mouse chases the cat.[(triple3 OR ((((triple1) -> rule2)) -> rule1))] @1: The cat visits the mouse.[(((triple1) -> rule2))] @2: The mouse is rough.[(((((triple1) -> rule2)) -> rule3))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple3
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
((triple1) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2