The cow visits the lion. The dog is red. The dog likes the lion. The dog needs the cow. The dog needs the tiger. The dog visits the cow. The dog visits the lion. The lion is nice. The lion needs the cow. The lion needs the tiger. The tiger is cold. The tiger is nice. If someone visits the lion then they are rough. If someone visits the lion and the lion needs the dog then the lion likes the cow. If someone is cold then they like the cow. If someone visits the lion then they are round. If someone likes the dog then the dog visits the tiger. If someone likes the dog and they are cold then the dog is round. If someone is red and they visit the cow then they need the dog. If someone is round then they need the cow.
The cow visits the lion.
("cow" "visits" "lion" "+")
The dog is red.
("dog" "is" "red" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If someone visits the lion then they are rough.
((("someone" "visits" "lion" "+")) -> ("someone" "is" "rough" "+"))
If someone visits the lion and the lion needs the dog then the lion likes the cow.
((("someone" "visits" "lion" "+") ("lion" "needs" "dog" "+")) -> ("lion" "likes" "cow" "+"))
If someone is cold then they like the cow.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "cow" "+"))
If someone visits the lion then they are round.
((("someone" "visits" "lion" "+")) -> ("someone" "is" "round" "+"))
If someone likes the dog then the dog visits the tiger.
((("someone" "likes" "dog" "+")) -> ("dog" "visits" "tiger" "+"))
If someone likes the dog and they are cold then the dog is round.
((("someone" "likes" "dog" "+") ("someone" "is" "cold" "+")) -> ("dog" "is" "round" "+"))
If someone is red and they visit the cow then they need the dog.
((("someone" "is" "red" "+") ("someone" "visits" "cow" "+")) -> ("someone" "needs" "dog" "+"))
If someone is round then they need the cow.
((("someone" "is" "round" "+")) -> ("someone" "needs" "cow" "+"))
The cow visits the lion.
True
1
proof
[(triple1)]
("cow" "visits" "lion" "+")
triple1
The dog does not visit the lion.
False
1
inv-proof
[(triple7)]
("dog" "visits" "lion" "-")
triple7
The tiger likes the cow.
True
2
proof
[(((triple11) -> rule3))]
("tiger" "likes" "cow" "+")
((triple11) -> (rule3 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The cow is not round.
False
2
inv-proof
[(((triple1) -> rule4))]
("cow" "is" "round" "-")
((triple1) -> (rule4 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The tiger is not rough.
Unknown
inv-rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "rough" "-")
The lion needs the dog.
Unknown
rconc
[@1: The lion needs the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "needs" "dog" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The cow visits the lion.[(triple1)] The dog is red.[(triple2)] The dog likes the lion.[(triple3)] The dog needs the cow.[(triple4 OR ((((triple7) -> rule4)) -> rule8))] The dog needs the tiger.[(triple5)] The dog visits the cow.[(triple6)] The dog visits the lion.[(triple7)] The lion is nice.[(triple8)] The lion needs the cow.[(triple9)] The lion needs the tiger.[(triple10)] The tiger is cold.[(triple11)] The tiger is nice.[(triple12)] @1: The cow is rough.[(((triple1) -> rule1))] The cow is round.[(((triple1) -> rule4))] The dog is rough.[(((triple7) -> rule1))] The dog is round.[(((triple7) -> rule4))] The dog needs the dog.[(((triple2 triple6) -> rule7))] The tiger likes the cow.[(((triple11) -> rule3))] @2: The cow needs the cow.[(((((triple1) -> rule4)) -> rule8))]
The cow visits the lion.
("cow" "visits" "lion" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The dog likes the lion.
("dog" "likes" "lion" "+")
triple3
The dog needs the cow.
("dog" "needs" "cow" "+")
triple4
((((triple7) -> (rule4 % int2))) -> (rule8 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple5
The dog visits the cow.
("dog" "visits" "cow" "+")
triple6
The dog visits the lion.
("dog" "visits" "lion" "+")
triple7
The lion is nice.
("lion" "is" "nice" "+")
triple8
The lion needs the cow.
("lion" "needs" "cow" "+")
triple9
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The cow is rough.
("cow" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is round.
("cow" "is" "round" "+")
((triple1) -> (rule4 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
((triple7) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is round.
("dog" "is" "round" "+")
((triple7) -> (rule4 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple2 triple6) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
((triple11) -> (rule3 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2