The bear sees the lion. The lion chases the mouse. The mouse is red. The rabbit chases the bear. If someone is red then they do not need the bear. If the lion sees the rabbit and the lion sees the bear then the bear sees the mouse. If someone is kind and they do not chase the bear then they do not see the bear. If someone chases the lion and the lion chases the mouse then the mouse is red. If someone chases the rabbit then they are blue. If the mouse is red and the mouse does not need the bear then the mouse chases the rabbit.
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The mouse is red.
("mouse" "is" "red" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
If someone is red then they do not need the bear.
((("someone" "is" "red" "+")) -> ("someone" "needs" "bear" "-"))
If the lion sees the rabbit and the lion sees the bear then the bear sees the mouse.
((("lion" "sees" "rabbit" "+") ("lion" "sees" "bear" "+")) -> ("bear" "sees" "mouse" "+"))
If someone is kind and they do not chase the bear then they do not see the bear.
((("someone" "is" "kind" "+") ("someone" "chases" "bear" "~")) -> ("someone" "sees" "bear" "-"))
If someone chases the lion and the lion chases the mouse then the mouse is red.
((("someone" "chases" "lion" "+") ("lion" "chases" "mouse" "+")) -> ("mouse" "is" "red" "+"))
If someone chases the rabbit then they are blue.
((("someone" "chases" "rabbit" "+")) -> ("someone" "is" "blue" "+"))
If the mouse is red and the mouse does not need the bear then the mouse chases the rabbit.
((("mouse" "is" "red" "+") ("mouse" "needs" "bear" "~")) -> ("mouse" "chases" "rabbit" "+"))
The lion chases the mouse.
True
1
proof
[(triple2)]
("lion" "chases" "mouse" "+")
triple2
The rabbit does not chase the bear.
False
1
inv-proof
[(triple4)]
("rabbit" "chases" "bear" "-")
triple4
The mouse does not need the bear.
True
2
proof
[(((triple3) -> rule1))]
("mouse" "needs" "bear" "-")
((triple3) -> (rule1 % int1))
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
int1
The mouse needs the bear.
False
2
inv-proof
[(((triple3) -> rule1))]
("mouse" "needs" "bear" "+")
((triple3) -> (rule1 % int1))
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
int1
The mouse chases the rabbit.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule6))]
("mouse" "chases" "rabbit" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
int2
The mouse does not chase the rabbit.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule6))]
("mouse" "chases" "rabbit" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
int2
The mouse is blue.
True
5
proof
[(((((triple3 ((triple3) -> rule1)) -> rule6)) -> rule5))]
("mouse" "is" "blue" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
int3
The mouse is not blue.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule1)) -> rule6)) -> rule5))]
("mouse" "is" "blue" "-")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
int3
The rabbit is not blue.
Unknown
inv-rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "blue" "-")
The bear sees the mouse.
Unknown
rconc
[@1: The bear sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "mouse" "+")
The lion is not blue.
Unknown
inv-rconc
[@1: The lion is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "blue" "-")
The bear is blue.
Unknown
rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "blue" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The mouse sees the bear.
Unknown
random
[@0: The mouse sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bear" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
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 sees the lion.[(triple1)] The lion chases the mouse.[(triple2)] The mouse is red.[(triple3)] The rabbit chases the bear.[(triple4)] @1: The mouse does not need the bear.[(((triple3) -> rule1))] @2: The mouse chases the rabbit.[(((triple3 ((triple3) -> rule1)) -> rule6))] @3: The mouse is blue.[(((((triple3 ((triple3) -> rule1)) -> rule6)) -> rule5))]
The bear sees the lion.
("bear" "sees" "lion" "+")
triple1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple2
The mouse is red.
("mouse" "is" "red" "+")
triple3
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple4
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
((triple3) -> (rule1 % int1))
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
int3