The bear is round. The bear needs the lion. The lion likes the bear. The mouse is blue. The mouse is round. The mouse likes the lion. The mouse needs the bear. If the lion is blue and the lion is kind then the lion likes the bear. If something needs the lion then the lion likes the mouse. If something likes the lion and it chases the bear then it chases the lion. All kind things are rough. If something likes the mouse then the mouse chases the bear. If something is blue then it needs the mouse. If something likes the lion and the lion chases the bear then it needs the lion. If the mouse is kind then the mouse is green.
The bear is round.
("bear" "is" "round" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
If the lion is blue and the lion is kind then the lion likes the bear.
((("lion" "is" "blue" "+") ("lion" "is" "kind" "+")) -> ("lion" "likes" "bear" "+"))
If something needs the lion then the lion likes the mouse.
((("something" "needs" "lion" "+")) -> ("lion" "likes" "mouse" "+"))
If something likes the lion and it chases the bear then it chases the lion.
((("something" "likes" "lion" "+") ("something" "chases" "bear" "+")) -> ("something" "chases" "lion" "+"))
All kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something likes the mouse then the mouse chases the bear.
((("something" "likes" "mouse" "+")) -> ("mouse" "chases" "bear" "+"))
If something is blue then it needs the mouse.
((("something" "is" "blue" "+")) -> ("something" "needs" "mouse" "+"))
If something likes the lion and the lion chases the bear then it needs the lion.
((("something" "likes" "lion" "+") ("lion" "chases" "bear" "+")) -> ("something" "needs" "lion" "+"))
If the mouse is kind then the mouse is green.
((("mouse" "is" "kind" "+")) -> ("mouse" "is" "green" "+"))
The mouse is blue.
True
1
proof
[(triple4)]
("mouse" "is" "blue" "+")
triple4
The lion does not like the bear.
False
1
inv-proof
[(triple3)]
("lion" "likes" "bear" "-")
triple3
The lion likes the mouse.
True
2
proof
[(((triple2) -> rule2))]
("lion" "likes" "mouse" "+")
((triple2) -> (rule2 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The mouse does not need the mouse.
False
2
inv-proof
[(((triple4) -> rule6))]
("mouse" "needs" "mouse" "-")
((triple4) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse chases the bear.
True
3
proof
[(((((triple2) -> rule2)) -> rule5))]
("mouse" "chases" "bear" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The mouse does not chase the bear.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5))]
("mouse" "chases" "bear" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The mouse chases the lion.
True
5
proof
[(((triple6 ((((triple2) -> rule2)) -> rule5)) -> rule3))]
("mouse" "chases" "lion" "+")
((triple6 ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
The mouse does not chase the lion.
False
5
inv-proof
[(((triple6 ((((triple2) -> rule2)) -> rule5)) -> rule3))]
("mouse" "chases" "lion" "-")
((triple6 ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
The bear is not rough.
Unknown
inv-rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "rough" "-")
The bear chases the lion.
Unknown
rconc
[@1: The bear chases the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "lion" "+")
The bear does not need the mouse.
Unknown
inv-rconc
[@1: The bear needs the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "needs" "mouse" "-")
The mouse needs the lion.
Unknown
rconc
[@1: The mouse needs the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "needs" "lion" "+")
The bear does not like the lion.
Unknown
inv-random
[@0: The bear likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "lion" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
@0: The bear is round.[(triple1)] The bear needs the lion.[(triple2)] The lion likes the bear.[(triple3)] The mouse is blue.[(triple4)] The mouse is round.[(triple5)] The mouse likes the lion.[(triple6)] The mouse needs the bear.[(triple7)] @1: The lion likes the mouse.[(((triple2) -> rule2))] The mouse needs the mouse.[(((triple4) -> rule6))] @2: The mouse chases the bear.[(((((triple2) -> rule2)) -> rule5))] @3: The mouse chases the lion.[(((triple6 ((((triple2) -> rule2)) -> rule5)) -> rule3))]
The bear is round.
("bear" "is" "round" "+")
triple1
The bear needs the lion.
("bear" "needs" "lion" "+")
triple2
The lion likes the bear.
("lion" "likes" "bear" "+")
triple3
The mouse is blue.
("mouse" "is" "blue" "+")
triple4
The mouse is round.
("mouse" "is" "round" "+")
triple5
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple6
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple7
The lion likes the mouse.
("lion" "likes" "mouse" "+")
((triple2) -> (rule2 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple4) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
((triple6 ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3