The bear chases the lion. The cow visits the bear. The lion chases the mouse. The mouse needs the cow. If something is young and it needs the cow then it visits the mouse. If the cow chases the mouse and the mouse visits the bear then the cow is not blue. If something chases the bear then the bear needs the lion. If something chases the lion then the lion chases the bear. If something needs the bear and the bear visits the lion then the lion chases the bear. If something is green and not young then it is not nice.
The bear chases the lion.
("bear" "chases" "lion" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
If something is young and it needs the cow then it visits the mouse.
((("something" "is" "young" "+") ("something" "needs" "cow" "+")) -> ("something" "visits" "mouse" "+"))
If the cow chases the mouse and the mouse visits the bear then the cow is not blue.
((("cow" "chases" "mouse" "+") ("mouse" "visits" "bear" "+")) -> ("cow" "is" "blue" "-"))
If something chases the bear then the bear needs the lion.
((("something" "chases" "bear" "+")) -> ("bear" "needs" "lion" "+"))
If something chases the lion then the lion chases the bear.
((("something" "chases" "lion" "+")) -> ("lion" "chases" "bear" "+"))
If something needs the bear and the bear visits the lion then the lion chases the bear.
((("something" "needs" "bear" "+") ("bear" "visits" "lion" "+")) -> ("lion" "chases" "bear" "+"))
If something is green and not young then it is not nice.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "nice" "-"))
The lion chases the mouse.
True
1
proof
[(triple3)]
("lion" "chases" "mouse" "+")
triple3
The lion does not chase the mouse.
False
1
inv-proof
[(triple3)]
("lion" "chases" "mouse" "-")
triple3
The lion chases the bear.
True
2
proof
[(((triple1) -> rule4))]
("lion" "chases" "bear" "+")
((triple1) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion does not chase the bear.
False
2
inv-proof
[(((triple1) -> rule4))]
("lion" "chases" "bear" "-")
((triple1) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The bear needs the lion.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("bear" "needs" "lion" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The bear does not need the lion.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("bear" "needs" "lion" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The lion does not visit the mouse.
Unknown
inv-rconc
[@1: The lion visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "mouse" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The bear does not visit the mouse.
Unknown
inv-rconc
[@1: The bear visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "mouse" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The mouse does not visit the lion.
Unknown
inv-random
[@0: The mouse visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "lion" "-")
The bear needs the mouse.
Unknown
random
[@0: The bear needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "mouse" "+")
@0: The bear chases the lion.[(triple1)] The cow visits the bear.[(triple2)] The lion chases the mouse.[(triple3)] The mouse needs the cow.[(triple4)] @1: The lion chases the bear.[(((triple1) -> rule4))] @2: The bear needs the lion.[(((((triple1) -> rule4)) -> rule3))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The cow visits the bear.
("cow" "visits" "bear" "+")
triple2
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple3
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple4
The lion chases the bear.
("lion" "chases" "bear" "+")
((triple1) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2