The cow is big. The cow is green. The cow sees the dog. The cow visits the lion. The dog chases the cow. The dog chases the lion. The dog is kind. The dog visits the cow. The lion chases the dog. The lion is big. The lion is kind. The lion is red. The lion sees the cow. The lion sees the dog. The lion visits the dog. If someone visits the cow then they see the cow. If someone sees the lion then the lion sees the cow. If the dog chases the cow and the cow chases the dog then the dog visits the cow. If someone sees the cow and they are kind then they visit the lion. If the cow is big and the cow chases the lion then the lion is red. If someone chases the lion and they are red then the lion sees the cow.
The cow is big.
("cow" "is" "big" "+")
The cow is green.
("cow" "is" "green" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If someone visits the cow then they see the cow.
((("someone" "visits" "cow" "+")) -> ("someone" "sees" "cow" "+"))
If someone sees the lion then the lion sees the cow.
((("someone" "sees" "lion" "+")) -> ("lion" "sees" "cow" "+"))
If the dog chases the cow and the cow chases the dog then the dog visits the cow.
((("dog" "chases" "cow" "+") ("cow" "chases" "dog" "+")) -> ("dog" "visits" "cow" "+"))
If someone sees the cow and they are kind then they visit the lion.
((("someone" "sees" "cow" "+") ("someone" "is" "kind" "+")) -> ("someone" "visits" "lion" "+"))
If the cow is big and the cow chases the lion then the lion is red.
((("cow" "is" "big" "+") ("cow" "chases" "lion" "+")) -> ("lion" "is" "red" "+"))
If someone chases the lion and they are red then the lion sees the cow.
((("someone" "chases" "lion" "+") ("someone" "is" "red" "+")) -> ("lion" "sees" "cow" "+"))
The dog is kind.
True
1
proof
[(triple7)]
("dog" "is" "kind" "+")
triple7
The cow is not big.
False
1
inv-proof
[(triple1)]
("cow" "is" "big" "-")
triple1
The dog sees the cow.
True
2
proof
[(((triple8) -> rule1))]
("dog" "sees" "cow" "+")
((triple8) -> (rule1 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The lion does not visit the lion.
False
3
inv-proof
[(((triple13 triple11) -> rule4))]
("lion" "visits" "lion" "-")
((triple13 triple11) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "cow" "-")
The cow visits the dog.
Unknown
random
[@0: The cow visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "dog" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The cow is big.[(triple1)] The cow is green.[(triple2)] The cow sees the dog.[(triple3)] The cow visits the lion.[(triple4)] The dog chases the cow.[(triple5)] The dog chases the lion.[(triple6)] The dog is kind.[(triple7)] The dog visits the cow.[(triple8)] The lion chases the dog.[(triple9)] The lion is big.[(triple10)] The lion is kind.[(triple11)] The lion is red.[(triple12)] The lion sees the cow.[(triple13)] The lion sees the dog.[(triple14)] The lion visits the dog.[(triple15)] @1: The dog sees the cow.[(((triple8) -> rule1))] The lion visits the lion.[(((triple13 triple11) -> rule4))] @2: The dog visits the lion.[(((((triple8) -> rule1) triple7) -> rule4))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The cow sees the dog.
("cow" "sees" "dog" "+")
triple3
The cow visits the lion.
("cow" "visits" "lion" "+")
triple4
The dog chases the cow.
("dog" "chases" "cow" "+")
triple5
The dog chases the lion.
("dog" "chases" "lion" "+")
triple6
The dog is kind.
("dog" "is" "kind" "+")
triple7
The dog visits the cow.
("dog" "visits" "cow" "+")
triple8
The lion chases the dog.
("lion" "chases" "dog" "+")
triple9
The lion is big.
("lion" "is" "big" "+")
triple10
The lion is kind.
("lion" "is" "kind" "+")
triple11
The lion is red.
("lion" "is" "red" "+")
triple12
The lion sees the cow.
("lion" "sees" "cow" "+")
triple13
The lion sees the dog.
("lion" "sees" "dog" "+")
triple14
The lion visits the dog.
("lion" "visits" "dog" "+")
triple15
The dog sees the cow.
("dog" "sees" "cow" "+")
((triple8) -> (rule1 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple13 triple11) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
((((triple8) -> (rule1 % int2)) triple7) -> (rule4 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2