The bear is young. The cat chases the lion. The lion is cold. The rabbit does not chase the cat. If someone is nice and not cold then they need the rabbit. If someone is young then they do not eat the rabbit. If the bear is kind and the rabbit does not need the bear then the bear does not need the lion. If someone is cold then they do not chase the lion. If someone eats the lion and they are not cold then they do not eat the cat. If someone is cold and they do not chase the lion then the lion does not chase the rabbit.
The bear is young.
("bear" "is" "young" "+")
The cat chases the lion.
("cat" "chases" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
If someone is nice and not cold then they need the rabbit.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "~")) -> ("someone" "needs" "rabbit" "+"))
If someone is young then they do not eat the rabbit.
((("someone" "is" "young" "+")) -> ("someone" "eats" "rabbit" "-"))
If the bear is kind and the rabbit does not need the bear then the bear does not need the lion.
((("bear" "is" "kind" "+") ("rabbit" "needs" "bear" "~")) -> ("bear" "needs" "lion" "-"))
If someone is cold then they do not chase the lion.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "lion" "-"))
If someone eats the lion and they are not cold then they do not eat the cat.
((("someone" "eats" "lion" "+") ("someone" "is" "cold" "~")) -> ("someone" "eats" "cat" "-"))
If someone is cold and they do not chase the lion then the lion does not chase the rabbit.
((("someone" "is" "cold" "+") ("someone" "chases" "lion" "~")) -> ("lion" "chases" "rabbit" "-"))
The cat chases the lion.
True
1
proof
[(triple2)]
("cat" "chases" "lion" "+")
triple2
The cat does not chase the lion.
False
1
inv-proof
[(triple2)]
("cat" "chases" "lion" "-")
triple2
The bear does not eat the rabbit.
True
2
proof
[(((triple1) -> rule2))]
("bear" "eats" "rabbit" "-")
((triple1) -> (rule2 % int1))
The bear does not eat the rabbit.
("bear" "eats" "rabbit" "-")
int1
The bear eats the rabbit.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "eats" "rabbit" "+")
((triple1) -> (rule2 % int1))
The bear does not eat the rabbit.
("bear" "eats" "rabbit" "-")
int1
The lion does not chase the rabbit.
True
4
proof
[(((triple3 ((triple3) -> rule4)) -> rule6))]
("lion" "chases" "rabbit" "-")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The lion does not chase the rabbit.
("lion" "chases" "rabbit" "-")
int1
The lion does not chase the lion.
("lion" "chases" "lion" "-")
int2
The lion chases the rabbit.
False
4
inv-proof
[(((triple3 ((triple3) -> rule4)) -> rule6))]
("lion" "chases" "rabbit" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The lion does not chase the rabbit.
("lion" "chases" "rabbit" "-")
int1
The lion does not chase the lion.
("lion" "chases" "lion" "-")
int2
The cat does not need the rabbit.
Unknown
inv-rconc
[@1: The cat needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "rabbit" "-")
The bear needs the rabbit.
Unknown
rconc
[@1: The bear needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "needs" "rabbit" "+")
The lion does not need the rabbit.
Unknown
inv-rconc
[@1: The lion needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "rabbit" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit does not need the lion.
Unknown
inv-random
[@0: The rabbit needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "lion" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
@0: The bear is young.[(triple1)] The cat chases the lion.[(triple2)] The lion is cold.[(triple3)] The rabbit does not chase the cat.[(triple4)] @1: The bear does not eat the rabbit.[(((triple1) -> rule2))] The lion does not chase the lion.[(((triple3) -> rule4))] @2: The lion does not chase the rabbit.[(((triple3 ((triple3) -> rule4)) -> rule6))]
The bear is young.
("bear" "is" "young" "+")
triple1
The cat chases the lion.
("cat" "chases" "lion" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple3
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
triple4
The bear does not eat the rabbit.
("bear" "eats" "rabbit" "-")
((triple1) -> (rule2 % int1))
The bear does not eat the rabbit.
("bear" "eats" "rabbit" "-")
int1
The lion does not chase the lion.
("lion" "chases" "lion" "-")
((triple3) -> (rule4 % int1))
The lion does not chase the lion.
("lion" "chases" "lion" "-")
int1
The lion does not chase the rabbit.
("lion" "chases" "rabbit" "-")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The lion does not chase the rabbit.
("lion" "chases" "rabbit" "-")
int1
The lion does not chase the lion.
("lion" "chases" "lion" "-")
int2