The dog eats the lion. The dog is big. The dog is cold. The dog is not red. The dog is rough. The dog is round. The dog does not like the lion. The dog visits the lion. The lion eats the dog. The lion is big. The lion is not cold. The lion is not red. The lion is rough. The lion likes the dog. The lion does not visit the dog. If someone visits the lion and the lion is not red then they are round. If the dog likes the lion and the lion likes the dog then the lion eats the dog. If someone eats the lion then they visit the lion. If someone is big then they visit the lion. If someone likes the dog and the dog is round then the dog eats the lion. If someone visits the dog then they like the dog.
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is not red.
("dog" "is" "red" "-")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The dog does not like the lion.
("dog" "likes" "lion" "-")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is not cold.
("lion" "is" "cold" "-")
The lion is not red.
("lion" "is" "red" "-")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion does not visit the dog.
("lion" "visits" "dog" "-")
If someone visits the lion and the lion is not red then they are round.
((("someone" "visits" "lion" "+") ("lion" "is" "red" "~")) -> ("someone" "is" "round" "+"))
If the dog likes the lion and the lion likes the dog then the lion eats the dog.
((("dog" "likes" "lion" "+") ("lion" "likes" "dog" "+")) -> ("lion" "eats" "dog" "+"))
If someone eats the lion then they visit the lion.
((("someone" "eats" "lion" "+")) -> ("someone" "visits" "lion" "+"))
If someone is big then they visit the lion.
((("someone" "is" "big" "+")) -> ("someone" "visits" "lion" "+"))
If someone likes the dog and the dog is round then the dog eats the lion.
((("someone" "likes" "dog" "+") ("dog" "is" "round" "+")) -> ("dog" "eats" "lion" "+"))
If someone visits the dog then they like the dog.
((("someone" "visits" "dog" "+")) -> ("someone" "likes" "dog" "+"))
The dog eats the lion.
True
1
proof
[(triple1 OR ((triple14 triple6) -> rule5) OR ((triple14 ((triple8 triple12) -> rule1)) -> rule5) OR ((triple14 ((((triple2) -> rule4) triple12) -> rule1)) -> rule5))]
("dog" "eats" "lion" "+")
triple1
((triple14 triple6) -> (rule5 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
((triple14 ((triple8 triple12) -> (rule1 % int2))) -> (rule5 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
((triple14 ((((triple2) -> (rule4 % int3)) triple12) -> (rule1 % int2))) -> (rule5 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
int3
The dog is not cold.
False
1
inv-proof
[(triple3)]
("dog" "is" "cold" "-")
triple3
The lion visits the lion.
True
2
proof
[(((triple10) -> rule4))]
("lion" "visits" "lion" "+")
((triple10) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion does not visit the lion.
False
2
inv-proof
[(((triple10) -> rule4))]
("lion" "visits" "lion" "-")
((triple10) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is round.
True
4
proof
[(((((triple10) -> rule4) triple12) -> rule1))]
("lion" "is" "round" "+")
((((triple10) -> (rule4 % int2)) triple12) -> (rule1 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is not round.
False
4
inv-proof
[(((((triple10) -> rule4) triple12) -> rule1))]
("lion" "is" "round" "-")
((((triple10) -> (rule4 % int2)) triple12) -> (rule1 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The dog does not like the dog.
Unknown
inv-rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "likes" "dog" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The dog does not like the lion.[(triple7)] The dog eats the lion.[(triple1 OR ((triple14 triple6) -> rule5) OR ((triple14 ((triple8 triple12) -> rule1)) -> rule5) OR ((triple14 ((((triple2) -> rule4) triple12) -> rule1)) -> rule5))] The dog is big.[(triple2)] The dog is cold.[(triple3)] The dog is not red.[(triple4)] The dog is rough.[(triple5)] The dog is round.[(triple6 OR ((triple8 triple12) -> rule1) OR ((((triple1) -> rule3) triple12) -> rule1) OR ((((triple2) -> rule4) triple12) -> rule1))] The dog visits the lion.[(triple8 OR ((triple1) -> rule3) OR ((triple2) -> rule4) OR ((((triple14 triple6) -> rule5)) -> rule3))] The lion does not visit the dog.[(triple15)] The lion eats the dog.[(triple9)] The lion is big.[(triple10)] The lion is not cold.[(triple11)] The lion is not red.[(triple12)] The lion is rough.[(triple13)] The lion likes the dog.[(triple14)] @1: The lion visits the lion.[(((triple10) -> rule4))] @2: The lion is round.[(((((triple10) -> rule4) triple12) -> rule1))]
The dog does not like the lion.
("dog" "likes" "lion" "-")
triple7
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
((triple14 triple6) -> (rule5 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
((triple14 ((triple8 triple12) -> (rule1 % int2))) -> (rule5 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
((triple14 ((((triple2) -> (rule4 % int3)) triple12) -> (rule1 % int2))) -> (rule5 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
int3
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is not red.
("dog" "is" "red" "-")
triple4
The dog is rough.
("dog" "is" "rough" "+")
triple5
The dog is round.
("dog" "is" "round" "+")
triple6
((triple8 triple12) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((((triple1) -> (rule3 % int2)) triple12) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
((((triple2) -> (rule4 % int2)) triple12) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
triple8
((triple1) -> (rule3 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
((triple2) -> (rule4 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
((((triple14 triple6) -> (rule5 % int2))) -> (rule3 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog eats the lion.
("dog" "eats" "lion" "+")
int2
The lion does not visit the dog.
("lion" "visits" "dog" "-")
triple15
The lion eats the dog.
("lion" "eats" "dog" "+")
triple9
The lion is big.
("lion" "is" "big" "+")
triple10
The lion is not cold.
("lion" "is" "cold" "-")
triple11
The lion is not red.
("lion" "is" "red" "-")
triple12
The lion is rough.
("lion" "is" "rough" "+")
triple13
The lion likes the dog.
("lion" "likes" "dog" "+")
triple14
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple10) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((((triple10) -> (rule4 % int2)) triple12) -> (rule1 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2