The cat does not need the mouse. The mouse chases the cat. If the mouse is not red then the mouse does not chase the cat. If something is green and it needs the cat then it needs the mouse. If something is young and it does not need the mouse then the mouse is rough. If something chases the mouse then it visits the cat. If the mouse chases the cat and the mouse is not rough then the cat chases the mouse. If something chases the cat then the cat chases the mouse. If something chases the mouse and it visits the cat then it does not chase the cat. If the cat chases the mouse and the mouse needs the cat then the mouse does not visit the cat.
The cat does not need the mouse.
("cat" "needs" "mouse" "-")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
If the mouse is not red then the mouse does not chase the cat.
((("mouse" "is" "red" "~")) -> ("mouse" "chases" "cat" "-"))
If something is green and it needs the cat then it needs the mouse.
((("something" "is" "green" "+") ("something" "needs" "cat" "+")) -> ("something" "needs" "mouse" "+"))
If something is young and it does not need the mouse then the mouse is rough.
((("something" "is" "young" "+") ("something" "needs" "mouse" "~")) -> ("mouse" "is" "rough" "+"))
If something chases the mouse then it visits the cat.
((("something" "chases" "mouse" "+")) -> ("something" "visits" "cat" "+"))
If the mouse chases the cat and the mouse is not rough then the cat chases the mouse.
((("mouse" "chases" "cat" "+") ("mouse" "is" "rough" "~")) -> ("cat" "chases" "mouse" "+"))
If something chases the cat then the cat chases the mouse.
((("something" "chases" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If something chases the mouse and it visits the cat then it does not chase the cat.
((("something" "chases" "mouse" "+") ("something" "visits" "cat" "+")) -> ("something" "chases" "cat" "-"))
If the cat chases the mouse and the mouse needs the cat then the mouse does not visit the cat.
((("cat" "chases" "mouse" "+") ("mouse" "needs" "cat" "+")) -> ("mouse" "visits" "cat" "-"))
The cat does not need the mouse.
True
1
proof
[(triple1)]
("cat" "needs" "mouse" "-")
triple1
The mouse does not chase the cat.
False
1
inv-proof
[(triple2)]
("mouse" "chases" "cat" "-")
triple2
The cat chases the mouse.
True
2
proof
[(((triple2) -> rule6))]
("cat" "chases" "mouse" "+")
((triple2) -> (rule6 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat does not chase the mouse.
False
2
inv-proof
[(((triple2) -> rule6))]
("cat" "chases" "mouse" "-")
((triple2) -> (rule6 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat visits the cat.
True
3
proof
[(((((triple2) -> rule6)) -> rule4))]
("cat" "visits" "cat" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The cat does not visit the cat.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule4))]
("cat" "visits" "cat" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse is rough.
Unknown
rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "rough" "+")
The mouse does not visit the cat.
Unknown
inv-rconc
[@1: The mouse visits the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "visits" "cat" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The cat does not need the mouse.[(triple1)] The mouse chases the cat.[(triple2)] @1: The cat chases the mouse.[(((triple2) -> rule6))] @2: The cat visits the cat.[(((((triple2) -> rule6)) -> rule4))] @3: The cat does not chase the cat.[(((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule4)) -> rule7))]
The cat does not need the mouse.
("cat" "needs" "mouse" "-")
triple1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((triple2) -> (rule6 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The cat does not chase the cat.
("cat" "chases" "cat" "-")
((((triple2) -> (rule6 % int3)) ((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The cat does not chase the cat.
("cat" "chases" "cat" "-")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3