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