The bear is kind. The bear likes the lion. The bear visits the lion. The cow is red. The cow is rough. The cow likes the bear. The cow visits the lion. The lion is cold. The lion is kind. The lion likes the cow. If something is kind and it visits the lion then it chases the lion. If the lion is red then the lion likes the cow.
The bear is kind.
("bear" "is" "kind" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
If something is kind and it visits the lion then it chases the lion.
((("something" "is" "kind" "+") ("something" "visits" "lion" "+")) -> ("something" "chases" "lion" "+"))
If the lion is red then the lion likes the cow.
((("lion" "is" "red" "+")) -> ("lion" "likes" "cow" "+"))
The cow visits the lion.
True
1
proof
[(triple7)]
("cow" "visits" "lion" "+")
triple7
The cow is not rough.
False
1
inv-proof
[(triple5)]
("cow" "is" "rough" "-")
triple5
The bear chases the lion.
True
3
proof
[(((triple1 triple3) -> rule1))]
("bear" "chases" "lion" "+")
((triple1 triple3) -> (rule1 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The bear does not chase the lion.
False
3
inv-proof
[(((triple1 triple3) -> rule1))]
("bear" "chases" "lion" "-")
((triple1 triple3) -> (rule1 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The cow does not chase the lion.
Unknown
inv-rconc
[@1: The cow chases the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "lion" "-")
The lion chases the lion.
Unknown
rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "chases" "lion" "+")
The lion does not visit the cow.
Unknown
inv-random
[@0: The lion visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cow" "-")
The bear visits the cow.
Unknown
random
[@0: The bear visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "cow" "+")
@0: The bear is kind.[(triple1)] The bear likes the lion.[(triple2)] The bear visits the lion.[(triple3)] The cow is red.[(triple4)] The cow is rough.[(triple5)] The cow likes the bear.[(triple6)] The cow visits the lion.[(triple7)] The lion is cold.[(triple8)] The lion is kind.[(triple9)] The lion likes the cow.[(triple10)] @1: The bear chases the lion.[(((triple1 triple3) -> rule1))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The bear likes the lion.
("bear" "likes" "lion" "+")
triple2
The bear visits the lion.
("bear" "visits" "lion" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow is rough.
("cow" "is" "rough" "+")
triple5
The cow likes the bear.
("cow" "likes" "bear" "+")
triple6
The cow visits the lion.
("cow" "visits" "lion" "+")
triple7
The lion is cold.
("lion" "is" "cold" "+")
triple8
The lion is kind.
("lion" "is" "kind" "+")
triple9
The lion likes the cow.
("lion" "likes" "cow" "+")
triple10
The bear chases the lion.
("bear" "chases" "lion" "+")
((triple1 triple3) -> (rule1 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1