The bear needs the lion. The bear sees the lion. The lion needs the bear. If something sees the bear and it chases the lion then the lion needs the bear. If something sees the bear then the bear does not need the lion. If something chases the bear then the bear is red. If something needs the lion and it is red then it is green. If something sees the lion then the lion chases the bear. If the lion chases the bear and the bear sees the lion then the lion is rough.
The bear needs the lion.
("bear" "needs" "lion" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
If something sees the bear and it chases the lion then the lion needs the bear.
((("something" "sees" "bear" "+") ("something" "chases" "lion" "+")) -> ("lion" "needs" "bear" "+"))
If something sees the bear then the bear does not need the lion.
((("something" "sees" "bear" "+")) -> ("bear" "needs" "lion" "-"))
If something chases the bear then the bear is red.
((("something" "chases" "bear" "+")) -> ("bear" "is" "red" "+"))
If something needs the lion and it is red then it is green.
((("something" "needs" "lion" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something sees the lion then the lion chases the bear.
((("something" "sees" "lion" "+")) -> ("lion" "chases" "bear" "+"))
If the lion chases the bear and the bear sees the lion then the lion is rough.
((("lion" "chases" "bear" "+") ("bear" "sees" "lion" "+")) -> ("lion" "is" "rough" "+"))
The lion needs the bear.
True
1
proof
[(triple3)]
("lion" "needs" "bear" "+")
triple3
The lion does not need the bear.
False
1
inv-proof
[(triple3)]
("lion" "needs" "bear" "-")
triple3
The lion chases the bear.
True
2
proof
[(((triple2) -> rule5))]
("lion" "chases" "bear" "+")
((triple2) -> (rule5 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion does not chase the bear.
False
2
inv-proof
[(((triple2) -> rule5))]
("lion" "chases" "bear" "-")
((triple2) -> (rule5 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The bear is red.
True
3
proof
[(((((triple2) -> rule5)) -> rule3))]
("bear" "is" "red" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The lion is not rough.
False
4
inv-proof
[(((((triple2) -> rule5) triple2) -> rule6))]
("lion" "is" "rough" "-")
((((triple2) -> (rule5 % int2)) triple2) -> (rule6 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The bear is green.
True
5
proof
[(((triple1 ((((triple2) -> rule5)) -> rule3)) -> rule4))]
("bear" "is" "green" "+")
((triple1 ((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The lion chases the bear.
("lion" "chases" "bear" "+")
int3
The bear is not green.
False
5
inv-proof
[(((triple1 ((((triple2) -> rule5)) -> rule3)) -> rule4))]
("bear" "is" "green" "-")
((triple1 ((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The lion chases the bear.
("lion" "chases" "bear" "+")
int3
The lion is not green.
Unknown
inv-rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "green" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
The bear does not chase the lion.
Unknown
inv-random
[@0: The bear chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "lion" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The bear needs the lion.[(triple1)] The bear sees the lion.[(triple2)] The lion needs the bear.[(triple3)] @1: The lion chases the bear.[(((triple2) -> rule5))] @2: The bear is red.[(((((triple2) -> rule5)) -> rule3))] The lion is rough.[(((((triple2) -> rule5) triple2) -> rule6))] @3: The bear is green.[(((triple1 ((((triple2) -> rule5)) -> rule3)) -> rule4))]
The bear needs the lion.
("bear" "needs" "lion" "+")
triple1
The bear sees the lion.
("bear" "sees" "lion" "+")
triple2
The lion needs the bear.
("lion" "needs" "bear" "+")
triple3
The lion chases the bear.
("lion" "chases" "bear" "+")
((triple2) -> (rule5 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule6 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The bear is green.
("bear" "is" "green" "+")
((triple1 ((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The lion chases the bear.
("lion" "chases" "bear" "+")
int3