The bear needs the lion. The lion is green. The mouse needs the lion. If the lion eats the bear then the lion is young. If someone eats the lion then they need the mouse. If someone is young then they need the bear. If the mouse visits the bear then the bear does not need the lion. If the bear needs the mouse and the bear eats the mouse then the bear needs the lion. If someone needs the lion then the lion eats the bear.
The bear needs the lion.
("bear" "needs" "lion" "+")
The lion is green.
("lion" "is" "green" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
If the lion eats the bear then the lion is young.
((("lion" "eats" "bear" "+")) -> ("lion" "is" "young" "+"))
If someone eats the lion then they need the mouse.
((("someone" "eats" "lion" "+")) -> ("someone" "needs" "mouse" "+"))
If someone is young then they need the bear.
((("someone" "is" "young" "+")) -> ("someone" "needs" "bear" "+"))
If the mouse visits the bear then the bear does not need the lion.
((("mouse" "visits" "bear" "+")) -> ("bear" "needs" "lion" "-"))
If the bear needs the mouse and the bear eats the mouse then the bear needs the lion.
((("bear" "needs" "mouse" "+") ("bear" "eats" "mouse" "+")) -> ("bear" "needs" "lion" "+"))
If someone needs the lion then the lion eats the bear.
((("someone" "needs" "lion" "+")) -> ("lion" "eats" "bear" "+"))
The lion is green.
True
1
proof
[(triple2)]
("lion" "is" "green" "+")
triple2
The lion is not green.
False
1
inv-proof
[(triple2)]
("lion" "is" "green" "-")
triple2
The lion eats the bear.
True
2
proof
[(((triple1) -> rule6) OR ((triple3) -> rule6))]
("lion" "eats" "bear" "+")
((triple1) -> (rule6 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
((triple3) -> (rule6 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion does not eat the bear.
False
2
inv-proof
[(((triple1) -> rule6) OR ((triple3) -> rule6))]
("lion" "eats" "bear" "-")
((triple1) -> (rule6 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
((triple3) -> (rule6 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion is young.
True
3
proof
[(((((triple1) -> rule6)) -> rule1) OR ((((triple3) -> rule6)) -> rule1))]
("lion" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The lion is not young.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule1) OR ((((triple3) -> rule6)) -> rule1))]
("lion" "is" "young" "-")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The lion needs the bear.
True
4
proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule3) OR ((((((triple3) -> rule6)) -> rule1)) -> rule3))]
("lion" "needs" "bear" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
The lion does not need the bear.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule3) OR ((((((triple3) -> rule6)) -> rule1)) -> rule3))]
("lion" "needs" "bear" "-")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
The mouse does not need the bear.
Unknown
inv-rconc
[@1: The mouse needs the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "needs" "bear" "-")
The mouse needs the mouse.
Unknown
rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "mouse" "+")
The lion does not need the mouse.
Unknown
inv-rconc
[@1: The lion needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "needs" "mouse" "-")
The bear needs the bear.
Unknown
rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "bear" "+")
The mouse does not eat the lion.
Unknown
inv-random
[@0: The mouse eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "lion" "-")
The mouse eats the bear.
Unknown
random
[@0: The mouse eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "bear" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The lion eats the mouse.
Unknown
random
[@0: The lion eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "mouse" "+")
@0: The bear needs the lion.[(triple1)] The lion is green.[(triple2)] The mouse needs the lion.[(triple3)] @1: The lion eats the bear.[(((triple1) -> rule6) OR ((triple3) -> rule6))] @2: The lion is young.[(((((triple1) -> rule6)) -> rule1) OR ((((triple3) -> rule6)) -> rule1))] @3: The lion needs the bear.[(((((((triple1) -> rule6)) -> rule1)) -> rule3) OR ((((((triple3) -> rule6)) -> rule1)) -> rule3))]
The bear needs the lion.
("bear" "needs" "lion" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple3
The lion eats the bear.
("lion" "eats" "bear" "+")
((triple1) -> (rule6 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
((triple3) -> (rule6 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion is young.
("lion" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The lion needs the bear.
("lion" "needs" "bear" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3