The bear eats the rabbit. The bear is rough. The bear needs the lion. The lion does not chase the mouse. The lion eats the mouse. The mouse does not chase the lion. The mouse chases the rabbit. The mouse eats the bear. The mouse needs the bear. The rabbit is round. If someone is round then they eat the mouse. If someone is cold and they eat the mouse then they chase the bear. If someone eats the mouse and the mouse needs the rabbit then the mouse is cold. If someone needs the rabbit and they are not rough then they chase the lion. If someone needs the bear then the bear is young. If someone eats the bear then the bear is young. If someone needs the mouse and they do not chase the mouse then the mouse eats the lion. If someone eats the mouse then they are cold.
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
If someone is round then they eat the mouse.
((("someone" "is" "round" "+")) -> ("someone" "eats" "mouse" "+"))
If someone is cold and they eat the mouse then they chase the bear.
((("someone" "is" "cold" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "chases" "bear" "+"))
If someone eats the mouse and the mouse needs the rabbit then the mouse is cold.
((("someone" "eats" "mouse" "+") ("mouse" "needs" "rabbit" "+")) -> ("mouse" "is" "cold" "+"))
If someone needs the rabbit and they are not rough then they chase the lion.
((("someone" "needs" "rabbit" "+") ("someone" "is" "rough" "~")) -> ("someone" "chases" "lion" "+"))
If someone needs the bear then the bear is young.
((("someone" "needs" "bear" "+")) -> ("bear" "is" "young" "+"))
If someone eats the bear then the bear is young.
((("someone" "eats" "bear" "+")) -> ("bear" "is" "young" "+"))
If someone needs the mouse and they do not chase the mouse then the mouse eats the lion.
((("someone" "needs" "mouse" "+") ("someone" "chases" "mouse" "~")) -> ("mouse" "eats" "lion" "+"))
If someone eats the mouse then they are cold.
((("someone" "eats" "mouse" "+")) -> ("someone" "is" "cold" "+"))
The bear eats the rabbit.
True
1
proof
[(triple1)]
("bear" "eats" "rabbit" "+")
triple1
The bear does not eat the rabbit.
False
1
inv-proof
[(triple1)]
("bear" "eats" "rabbit" "-")
triple1
The bear is young.
True
2
proof
[(((triple8) -> rule6) OR ((triple9) -> rule5))]
("bear" "is" "young" "+")
((triple8) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
((triple9) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The lion is not cold.
False
2
inv-proof
[(((triple5) -> rule8))]
("lion" "is" "cold" "-")
((triple5) -> (rule8 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion chases the bear.
True
4
proof
[(((((triple5) -> rule8) triple5) -> rule2))]
("lion" "chases" "bear" "+")
((((triple5) -> (rule8 % int2)) triple5) -> (rule2 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The rabbit is not cold.
False
3
inv-proof
[(((((triple10) -> rule1)) -> rule8))]
("rabbit" "is" "cold" "-")
((((triple10) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit chases the bear.
True
6
proof
[(((((((triple10) -> rule1)) -> rule8) ((triple10) -> rule1)) -> rule2))]
("rabbit" "chases" "bear" "+")
((((((triple10) -> (rule1 % int3))) -> (rule8 % int2)) ((triple10) -> (rule1 % int3))) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3
The rabbit does not chase the bear.
False
6
inv-proof
[(((((((triple10) -> rule1)) -> rule8) ((triple10) -> rule1)) -> rule2))]
("rabbit" "chases" "bear" "-")
((((((triple10) -> (rule1 % int3))) -> (rule8 % int2)) ((triple10) -> (rule1 % int3))) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3
The mouse is not cold.
Unknown
inv-rconc
[@2: The mouse is cold.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("mouse" "is" "cold" "-")
The bear chases the bear.
Unknown
rconc
[@2: The bear chases the bear.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("bear" "chases" "bear" "+")
The mouse does not chase the bear.
Unknown
inv-rconc
[@2: The mouse chases the bear.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("mouse" "chases" "bear" "-")
The rabbit chases the lion.
Unknown
rconc
[@1: The rabbit chases the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "chases" "lion" "+")
The rabbit does not eat the bear.
Unknown
inv-random
[@0: The rabbit eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "bear" "-")
The rabbit chases the mouse.
Unknown
random
[@0: The rabbit chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "mouse" "+")
The lion does not need the bear.
Unknown
inv-random
[@0: The lion needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "bear" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The bear eats the rabbit.[(triple1)] The bear is rough.[(triple2)] The bear needs the lion.[(triple3)] The lion does not chase the mouse.[(triple4)] The lion eats the mouse.[(triple5)] The mouse chases the rabbit.[(triple7)] The mouse does not chase the lion.[(triple6)] The mouse eats the bear.[(triple8)] The mouse needs the bear.[(triple9)] The rabbit is round.[(triple10)] @1: The bear is young.[(((triple8) -> rule6) OR ((triple9) -> rule5))] The lion is cold.[(((triple5) -> rule8))] The rabbit eats the mouse.[(((triple10) -> rule1))] @2: The lion chases the bear.[(((((triple5) -> rule8) triple5) -> rule2))] The rabbit is cold.[(((((triple10) -> rule1)) -> rule8))] @3: The rabbit chases the bear.[(((((((triple10) -> rule1)) -> rule8) ((triple10) -> rule1)) -> rule2))]
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The bear needs the lion.
("bear" "needs" "lion" "+")
triple3
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
triple4
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple5
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple7
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
triple6
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple8
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple9
The rabbit is round.
("rabbit" "is" "round" "+")
triple10
The bear is young.
("bear" "is" "young" "+")
((triple8) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
((triple9) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((triple5) -> (rule8 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
((triple10) -> (rule1 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
((((triple5) -> (rule8 % int2)) triple5) -> (rule2 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((triple10) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((((((triple10) -> (rule1 % int3))) -> (rule8 % int2)) ((triple10) -> (rule1 % int3))) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3