The cat needs the mouse. The mouse is green. If someone is big then they see the cat. If someone sees the cat and they are kind then the cat needs the mouse. If someone is big then they visit the mouse. If someone is green then they visit the cat. If someone visits the cat then they need the mouse. If someone visits the cat and the cat is green then they are rough.
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
If someone is big then they see the cat.
((("someone" "is" "big" "+")) -> ("someone" "sees" "cat" "+"))
If someone sees the cat and they are kind then the cat needs the mouse.
((("someone" "sees" "cat" "+") ("someone" "is" "kind" "+")) -> ("cat" "needs" "mouse" "+"))
If someone is big then they visit the mouse.
((("someone" "is" "big" "+")) -> ("someone" "visits" "mouse" "+"))
If someone is green then they visit the cat.
((("someone" "is" "green" "+")) -> ("someone" "visits" "cat" "+"))
If someone visits the cat then they need the mouse.
((("someone" "visits" "cat" "+")) -> ("someone" "needs" "mouse" "+"))
If someone visits the cat and the cat is green then they are rough.
((("someone" "visits" "cat" "+") ("cat" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
The cat needs the mouse.
True
1
proof
[(triple1)]
("cat" "needs" "mouse" "+")
triple1
The mouse is not green.
False
1
inv-proof
[(triple2)]
("mouse" "is" "green" "-")
triple2
The mouse visits the cat.
True
2
proof
[(((triple2) -> rule4))]
("mouse" "visits" "cat" "+")
((triple2) -> (rule4 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The mouse does not visit the cat.
False
2
inv-proof
[(((triple2) -> rule4))]
("mouse" "visits" "cat" "-")
((triple2) -> (rule4 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The mouse needs the mouse.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("mouse" "needs" "mouse" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The mouse does not need the mouse.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("mouse" "needs" "mouse" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "cat" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "rough" "-")
The cat sees the mouse.
Unknown
random
[@0: The cat sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "mouse" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat needs the mouse.[(triple1)] The mouse is green.[(triple2)] @1: The mouse visits the cat.[(((triple2) -> rule4))] @2: The mouse needs the mouse.[(((((triple2) -> rule4)) -> rule5))]
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple1
The mouse is green.
("mouse" "is" "green" "+")
triple2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
((triple2) -> (rule4 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2