The mouse is nice. The rabbit is green. If something is nice then it likes the rabbit. If the mouse likes the rabbit then the rabbit likes the mouse. If something likes the mouse then the mouse likes the rabbit. If something likes the mouse then the mouse eats the rabbit. If something eats the mouse then the mouse is round. If something is round then it needs the mouse.
The mouse is nice.
("mouse" "is" "nice" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
If something is nice then it likes the rabbit.
((("something" "is" "nice" "+")) -> ("something" "likes" "rabbit" "+"))
If the mouse likes the rabbit then the rabbit likes the mouse.
((("mouse" "likes" "rabbit" "+")) -> ("rabbit" "likes" "mouse" "+"))
If something likes the mouse then the mouse likes the rabbit.
((("something" "likes" "mouse" "+")) -> ("mouse" "likes" "rabbit" "+"))
If something likes the mouse then the mouse eats the rabbit.
((("something" "likes" "mouse" "+")) -> ("mouse" "eats" "rabbit" "+"))
If something eats the mouse then the mouse is round.
((("something" "eats" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If something is round then it needs the mouse.
((("something" "is" "round" "+")) -> ("something" "needs" "mouse" "+"))
The rabbit is green.
True
1
proof
[(triple2)]
("rabbit" "is" "green" "+")
triple2
The rabbit is not green.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "green" "-")
triple2
The mouse likes the rabbit.
True
2
proof
[(((triple1) -> rule1))]
("mouse" "likes" "rabbit" "+")
((triple1) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse does not like the rabbit.
False
2
inv-proof
[(((triple1) -> rule1))]
("mouse" "likes" "rabbit" "-")
((triple1) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The rabbit likes the mouse.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("rabbit" "likes" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The rabbit does not like the mouse.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("rabbit" "likes" "mouse" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse eats the rabbit.
True
4
proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule4))]
("mouse" "eats" "rabbit" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The mouse does not eat the rabbit.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule4))]
("mouse" "eats" "rabbit" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "round" "-")
The rabbit likes the rabbit.
Unknown
rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "likes" "rabbit" "+")
The mouse does not need the mouse.
Unknown
inv-rconc
[@2: The mouse needs the mouse.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The rabbit needs the mouse.
Unknown
rconc
[@1: The rabbit needs the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "needs" "mouse" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
@0: The mouse is nice.[(triple1)] The rabbit is green.[(triple2)] @1: The mouse likes the rabbit.[(((triple1) -> rule1))] @2: The rabbit likes the mouse.[(((((triple1) -> rule1)) -> rule2))] @3: The mouse eats the rabbit.[(((((((triple1) -> rule1)) -> rule2)) -> rule4))]
The mouse is nice.
("mouse" "is" "nice" "+")
triple1
The rabbit is green.
("rabbit" "is" "green" "+")
triple2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((triple1) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3