The bear chases the rabbit. The bear is cold. The bear is green. The mouse chases the rabbit. The mouse eats the rabbit. The mouse is green. The mouse sees the bear. The rabbit chases the mouse. The rabbit is blue. The rabbit sees the mouse. If the mouse is round and the mouse sees the rabbit then the rabbit chases the mouse. If the bear is blue then the bear is round. If something sees the mouse and the mouse chases the rabbit then the rabbit sees the bear. If something eats the rabbit and the rabbit eats the bear then the rabbit is kind. If something chases the mouse and the mouse is green then it eats the mouse. If something eats the mouse then it eats the bear.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If the mouse is round and the mouse sees the rabbit then the rabbit chases the mouse.
((("mouse" "is" "round" "+") ("mouse" "sees" "rabbit" "+")) -> ("rabbit" "chases" "mouse" "+"))
If the bear is blue then the bear is round.
((("bear" "is" "blue" "+")) -> ("bear" "is" "round" "+"))
If something sees the mouse and the mouse chases the rabbit then the rabbit sees the bear.
((("something" "sees" "mouse" "+") ("mouse" "chases" "rabbit" "+")) -> ("rabbit" "sees" "bear" "+"))
If something eats the rabbit and the rabbit eats the bear then the rabbit is kind.
((("something" "eats" "rabbit" "+") ("rabbit" "eats" "bear" "+")) -> ("rabbit" "is" "kind" "+"))
If something chases the mouse and the mouse is green then it eats the mouse.
((("something" "chases" "mouse" "+") ("mouse" "is" "green" "+")) -> ("something" "eats" "mouse" "+"))
If something eats the mouse then it eats the bear.
((("something" "eats" "mouse" "+")) -> ("something" "eats" "bear" "+"))
The rabbit sees the mouse.
True
1
proof
[(triple10)]
("rabbit" "sees" "mouse" "+")
triple10
The bear does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("bear" "chases" "rabbit" "-")
triple1
The rabbit sees the bear.
True
3
proof
[(((triple10 triple4) -> rule3))]
("rabbit" "sees" "bear" "+")
((triple10 triple4) -> (rule3 % int1))
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int1
The rabbit does not see the bear.
False
3
inv-proof
[(((triple10 triple4) -> rule3))]
("rabbit" "sees" "bear" "-")
((triple10 triple4) -> (rule3 % int1))
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int1
The rabbit eats the bear.
True
4
proof
[(((((triple8 triple6) -> rule5)) -> rule6))]
("rabbit" "eats" "bear" "+")
((((triple8 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit does not eat the bear.
False
4
inv-proof
[(((((triple8 triple6) -> rule5)) -> rule6))]
("rabbit" "eats" "bear" "-")
((((triple8 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit is kind.
True
6
proof
[(((triple5 ((((triple8 triple6) -> rule5)) -> rule6)) -> rule4))]
("rabbit" "is" "kind" "+")
((triple5 ((((triple8 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3
The rabbit is not kind.
False
6
inv-proof
[(((triple5 ((((triple8 triple6) -> rule5)) -> rule6)) -> rule4))]
("rabbit" "is" "kind" "-")
((triple5 ((((triple8 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3
The bear does not eat the mouse.
Unknown
inv-rconc
[@1: The bear eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "mouse" "-")
The bear eats the bear.
Unknown
rconc
[@2: The bear eats the bear.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("bear" "eats" "bear" "+")
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse eats the bear.
Unknown
rconc
[@2: The mouse eats the bear.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("mouse" "eats" "bear" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The bear chases the mouse.
Unknown
random
[@0: The bear chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "mouse" "+")
The mouse does not chase the bear.
Unknown
inv-random
[@0: The mouse chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "bear" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The bear chases the rabbit.[(triple1)] The bear is cold.[(triple2)] The bear is green.[(triple3)] The mouse chases the rabbit.[(triple4)] The mouse eats the rabbit.[(triple5)] The mouse is green.[(triple6)] The mouse sees the bear.[(triple7)] The rabbit chases the mouse.[(triple8)] The rabbit is blue.[(triple9)] The rabbit sees the mouse.[(triple10)] @1: The rabbit eats the mouse.[(((triple8 triple6) -> rule5))] The rabbit sees the bear.[(((triple10 triple4) -> rule3))] @2: The rabbit eats the bear.[(((((triple8 triple6) -> rule5)) -> rule6))] @3: The rabbit is kind.[(((triple5 ((((triple8 triple6) -> rule5)) -> rule6)) -> rule4))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple4
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple5
The mouse is green.
("mouse" "is" "green" "+")
triple6
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple7
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple10
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
((triple8 triple6) -> (rule5 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
((triple10 triple4) -> (rule3 % int1))
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
((((triple8 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple5 ((((triple8 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3