The cow chases the lion. The cow is kind. The cow is nice. The cow is red. The cow is rough. The cow likes the dog. The cow likes the lion. The cow sees the dog. The dog chases the cow. The dog is rough. The lion is kind. The lion is not nice. The lion is red. The lion likes the cow. The lion sees the dog. If something chases the lion and it likes the cow then the lion is not nice. If something likes the dog then it is rough. If the lion does not chase the cow then the cow is kind. If something is big and it likes the dog then the dog is rough. If the dog is big then the dog sees the cow. If the cow sees the dog and the cow does not chase the lion then the lion is rough. If something is kind then it sees the cow. If something sees the cow then the cow likes the lion.
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog is rough.
("dog" "is" "rough" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is not nice.
("lion" "is" "nice" "-")
The lion is red.
("lion" "is" "red" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
If something chases the lion and it likes the cow then the lion is not nice.
((("something" "chases" "lion" "+") ("something" "likes" "cow" "+")) -> ("lion" "is" "nice" "-"))
If something likes the dog then it is rough.
((("something" "likes" "dog" "+")) -> ("something" "is" "rough" "+"))
If the lion does not chase the cow then the cow is kind.
((("lion" "chases" "cow" "~")) -> ("cow" "is" "kind" "+"))
If something is big and it likes the dog then the dog is rough.
((("something" "is" "big" "+") ("something" "likes" "dog" "+")) -> ("dog" "is" "rough" "+"))
If the dog is big then the dog sees the cow.
((("dog" "is" "big" "+")) -> ("dog" "sees" "cow" "+"))
If the cow sees the dog and the cow does not chase the lion then the lion is rough.
((("cow" "sees" "dog" "+") ("cow" "chases" "lion" "~")) -> ("lion" "is" "rough" "+"))
If something is kind then it sees the cow.
((("something" "is" "kind" "+")) -> ("something" "sees" "cow" "+"))
If something sees the cow then the cow likes the lion.
((("something" "sees" "cow" "+")) -> ("cow" "likes" "lion" "+"))
The lion sees the dog.
True
1
proof
[(triple15)]
("lion" "sees" "dog" "+")
triple15
The dog is not rough.
False
1
inv-proof
[(triple10)]
("dog" "is" "rough" "-")
triple10
The lion sees the cow.
True
2
proof
[(((triple11) -> rule7))]
("lion" "sees" "cow" "+")
((triple11) -> (rule7 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The cow does not see the cow.
False
2
inv-proof
[(((triple2) -> rule7))]
("cow" "sees" "cow" "-")
((triple2) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The lion is not rough.
Unknown
inv-rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "rough" "-")
The dog sees the cow.
Unknown
rconc
[@1: The dog sees the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "sees" "cow" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The dog likes the cow.
Unknown
random
[@0: The dog likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cow" "+")
@0: The cow chases the lion.[(triple1)] The cow is kind.[(triple2)] The cow is nice.[(triple3)] The cow is red.[(triple4)] The cow is rough.[(triple5 OR ((triple6) -> rule2))] The cow likes the dog.[(triple6)] The cow likes the lion.[(triple7 OR ((((triple11) -> rule7)) -> rule8) OR ((((triple2) -> rule7)) -> rule8))] The cow sees the dog.[(triple8)] The dog chases the cow.[(triple9)] The dog is rough.[(triple10)] The lion is kind.[(triple11)] The lion is not nice.[(triple12)] The lion is red.[(triple13)] The lion likes the cow.[(triple14)] The lion sees the dog.[(triple15)] @1: The cow sees the cow.[(((triple2) -> rule7))] The lion sees the cow.[(((triple11) -> rule7))]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow is rough.
("cow" "is" "rough" "+")
triple5
((triple6) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
triple6
The cow likes the lion.
("cow" "likes" "lion" "+")
triple7
((((triple11) -> (rule7 % int2))) -> (rule8 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
triple8
The dog chases the cow.
("dog" "chases" "cow" "+")
triple9
The dog is rough.
("dog" "is" "rough" "+")
triple10
The lion is kind.
("lion" "is" "kind" "+")
triple11
The lion is not nice.
("lion" "is" "nice" "-")
triple12
The lion is red.
("lion" "is" "red" "+")
triple13
The lion likes the cow.
("lion" "likes" "cow" "+")
triple14
The lion sees the dog.
("lion" "sees" "dog" "+")
triple15
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple2) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
((triple11) -> (rule7 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1