The bear is red. The bear likes the lion. The bear likes the rabbit. The bear sees the mouse. The lion is round. The mouse is blue. The mouse sees the bear. The rabbit is blue. The rabbit is not red. The rabbit likes the bear. The rabbit sees the lion. The rabbit sees the mouse. If the lion sees the rabbit and the lion is red then the lion is cold. If something is cold then it does not like the rabbit. If something sees the lion then it needs the mouse. If something sees the mouse then it sees the lion. If something is round and red then it sees the lion. If something needs the bear then the bear is round. Round things are cold. If something likes the bear and it is big then it does not like the lion.
The bear is red.
("bear" "is" "red" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The lion is round.
("lion" "is" "round" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is not red.
("rabbit" "is" "red" "-")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If the lion sees the rabbit and the lion is red then the lion is cold.
((("lion" "sees" "rabbit" "+") ("lion" "is" "red" "+")) -> ("lion" "is" "cold" "+"))
If something is cold then it does not like the rabbit.
((("something" "is" "cold" "+")) -> ("something" "likes" "rabbit" "-"))
If something sees the lion then it needs the mouse.
((("something" "sees" "lion" "+")) -> ("something" "needs" "mouse" "+"))
If something sees the mouse then it sees the lion.
((("something" "sees" "mouse" "+")) -> ("something" "sees" "lion" "+"))
If something is round and red then it sees the lion.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "sees" "lion" "+"))
If something needs the bear then the bear is round.
((("something" "needs" "bear" "+")) -> ("bear" "is" "round" "+"))
Round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something likes the bear and it is big then it does not like the lion.
((("something" "likes" "bear" "+") ("something" "is" "big" "+")) -> ("something" "likes" "lion" "-"))
The rabbit sees the lion.
True
1
proof
[(triple11 OR ((triple12) -> rule4))]
("rabbit" "sees" "lion" "+")
triple11
((triple12) -> (rule4 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The bear is not red.
False
1
inv-proof
[(triple1)]
("bear" "is" "red" "-")
triple1
The rabbit needs the mouse.
True
2
proof
[(((triple11) -> rule3) OR ((((triple12) -> rule4)) -> rule3))]
("rabbit" "needs" "mouse" "+")
((triple11) -> (rule3 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
((((triple12) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The lion is not cold.
False
2
inv-proof
[(((triple5) -> rule7))]
("lion" "is" "cold" "-")
((triple5) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The bear needs the mouse.
True
3
proof
[(((((triple4) -> rule4)) -> rule3))]
("bear" "needs" "mouse" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The lion likes the rabbit.
False
3
inv-proof
[(((((triple5) -> rule7)) -> rule2))]
("lion" "likes" "rabbit" "+")
((((triple5) -> (rule7 % int2))) -> (rule2 % int1))
The lion does not like the rabbit.
("lion" "likes" "rabbit" "-")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The mouse does not need the mouse.
Unknown
inv-rconc
[@2: The mouse needs the mouse.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse sees the lion.
Unknown
rconc
[@1: The mouse sees the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "lion" "+")
The bear is not cold.
Unknown
inv-rconc
[@2: The bear is cold.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("bear" "is" "cold" "-")
The mouse likes the lion.
Unknown
random
[@0: The mouse likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "lion" "+")
The lion does not see the bear.
Unknown
inv-random
[@0: The lion sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bear" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The bear is red.[(triple1)] The bear likes the lion.[(triple2)] The bear likes the rabbit.[(triple3)] The bear sees the mouse.[(triple4)] The lion is round.[(triple5)] The mouse is blue.[(triple6)] The mouse sees the bear.[(triple7)] The rabbit is blue.[(triple8)] The rabbit is not red.[(triple9)] The rabbit likes the bear.[(triple10)] The rabbit sees the lion.[(triple11 OR ((triple12) -> rule4))] The rabbit sees the mouse.[(triple12)] @1: The bear sees the lion.[(((triple4) -> rule4))] The lion is cold.[(((triple5) -> rule7))] The rabbit needs the mouse.[(((triple11) -> rule3) OR ((((triple12) -> rule4)) -> rule3))] @2: The bear needs the mouse.[(((((triple4) -> rule4)) -> rule3))] The lion does not like the rabbit.[(((((triple5) -> rule7)) -> rule2))]
The bear is red.
("bear" "is" "red" "+")
triple1
The bear likes the lion.
("bear" "likes" "lion" "+")
triple2
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The mouse is blue.
("mouse" "is" "blue" "+")
triple6
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple7
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple8
The rabbit is not red.
("rabbit" "is" "red" "-")
triple9
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple10
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple11
((triple12) -> (rule4 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple12
The bear sees the lion.
("bear" "sees" "lion" "+")
((triple4) -> (rule4 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((triple5) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
((triple11) -> (rule3 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
((((triple12) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The lion does not like the rabbit.
("lion" "likes" "rabbit" "-")
((((triple5) -> (rule7 % int2))) -> (rule2 % int1))
The lion does not like the rabbit.
("lion" "likes" "rabbit" "-")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2