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