The cat needs the mouse. The mouse eats the cat. The mouse is rough. If someone is green then they eat the mouse. If someone eats the cat then the cat is green. If someone is big then they chase the mouse. If someone eats the mouse then the mouse eats the cat. If someone needs the mouse and the mouse is nice then they need the cat. If the mouse needs the cat and the mouse chases the cat then the mouse is nice. If the mouse eats the cat then the mouse chases the cat. If someone needs the mouse then they need the cat.
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
If someone is green then they eat the mouse.
((("someone" "is" "green" "+")) -> ("someone" "eats" "mouse" "+"))
If someone eats the cat then the cat is green.
((("someone" "eats" "cat" "+")) -> ("cat" "is" "green" "+"))
If someone is big then they chase the mouse.
((("someone" "is" "big" "+")) -> ("someone" "chases" "mouse" "+"))
If someone eats the mouse then the mouse eats the cat.
((("someone" "eats" "mouse" "+")) -> ("mouse" "eats" "cat" "+"))
If someone needs the mouse and the mouse is nice then they need the cat.
((("someone" "needs" "mouse" "+") ("mouse" "is" "nice" "+")) -> ("someone" "needs" "cat" "+"))
If the mouse needs the cat and the mouse chases the cat then the mouse is nice.
((("mouse" "needs" "cat" "+") ("mouse" "chases" "cat" "+")) -> ("mouse" "is" "nice" "+"))
If the mouse eats the cat then the mouse chases the cat.
((("mouse" "eats" "cat" "+")) -> ("mouse" "chases" "cat" "+"))
If someone needs the mouse then they need the cat.
((("someone" "needs" "mouse" "+")) -> ("someone" "needs" "cat" "+"))
The mouse is rough.
True
1
proof
[(triple3)]
("mouse" "is" "rough" "+")
triple3
The cat does not need the mouse.
False
1
inv-proof
[(triple1)]
("cat" "needs" "mouse" "-")
triple1
The cat needs the cat.
True
2
proof
[(((triple1) -> rule8))]
("cat" "needs" "cat" "+")
((triple1) -> (rule8 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple1) -> rule8))]
("cat" "needs" "cat" "-")
((triple1) -> (rule8 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat eats the mouse.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("cat" "eats" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat does not eat the mouse.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("cat" "eats" "mouse" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse needs the cat.
Unknown
rconc
[@1: The mouse needs the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "needs" "cat" "+")
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat needs the mouse.[(triple1)] The mouse eats the cat.[(triple2)] The mouse is rough.[(triple3)] @1: The cat is green.[(((triple2) -> rule2))] The cat needs the cat.[(((triple1) -> rule8))] The mouse chases the cat.[(((triple2) -> rule7))] @2: The cat eats the mouse.[(((((triple2) -> rule2)) -> rule1))]
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
((triple2) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple1) -> (rule8 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
((triple2) -> (rule7 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2