The dog chases the lion. The dog eats the lion. The dog is big. The dog visits the lion. The lion chases the dog. The lion eats the dog. The lion is big. The lion is red. The lion is young. The lion visits the dog. If someone chases the dog then they eat the dog. If someone chases the lion then they are young. If someone is nice and they eat the lion then they are big. If someone visits the dog then they are kind. If someone eats the dog and the dog chases the lion then the lion visits the dog. If someone visits the dog and they are big then the dog is kind. If someone is big and they visit the dog then the dog eats the lion. If someone eats the lion and they chase the lion then the lion chases the dog.
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is big.
("dog" "is" "big" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If someone chases the dog then they eat the dog.
((("someone" "chases" "dog" "+")) -> ("someone" "eats" "dog" "+"))
If someone chases the lion then they are young.
((("someone" "chases" "lion" "+")) -> ("someone" "is" "young" "+"))
If someone is nice and they eat the lion then they are big.
((("someone" "is" "nice" "+") ("someone" "eats" "lion" "+")) -> ("someone" "is" "big" "+"))
If someone visits the dog then they are kind.
((("someone" "visits" "dog" "+")) -> ("someone" "is" "kind" "+"))
If someone eats the dog and the dog chases the lion then the lion visits the dog.
((("someone" "eats" "dog" "+") ("dog" "chases" "lion" "+")) -> ("lion" "visits" "dog" "+"))
If someone visits the dog and they are big then the dog is kind.
((("someone" "visits" "dog" "+") ("someone" "is" "big" "+")) -> ("dog" "is" "kind" "+"))
If someone is big and they visit the dog then the dog eats the lion.
((("someone" "is" "big" "+") ("someone" "visits" "dog" "+")) -> ("dog" "eats" "lion" "+"))
If someone eats the lion and they chase the lion then the lion chases the dog.
((("someone" "eats" "lion" "+") ("someone" "chases" "lion" "+")) -> ("lion" "chases" "dog" "+"))
The dog visits the lion.
True
1
proof
[(triple4)]
("dog" "visits" "lion" "+")
triple4
The lion does not eat the dog.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule1) OR ((((triple2 triple1) -> rule8)) -> rule1) OR ((((((triple7 triple10) -> rule7) triple1) -> rule8)) -> rule1))]
("lion" "eats" "dog" "-")
triple6
((triple5) -> (rule1 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
((((triple2 triple1) -> (rule8 % int2))) -> (rule1 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
((((((triple7 triple10) -> (rule7 % int3)) triple1) -> (rule8 % int2))) -> (rule1 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
The dog eats the lion.
("dog" "eats" "lion" "+")
int3
The dog is kind.
True
3
proof
[(((triple10 triple7) -> rule6) OR ((((triple6 triple1) -> rule5) triple7) -> rule6) OR ((((((triple5) -> rule1) triple1) -> rule5) triple7) -> rule6) OR ((((((((triple2 triple1) -> rule8)) -> rule1) triple1) -> rule5) triple7) -> rule6))]
("dog" "is" "kind" "+")
((triple10 triple7) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
((((triple6 triple1) -> (rule5 % int2)) triple7) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((((triple5) -> (rule1 % int3)) triple1) -> (rule5 % int2)) triple7) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion eats the dog.
("lion" "eats" "dog" "+")
int3
((((((((triple2 triple1) -> (rule8 % int4))) -> (rule1 % int3)) triple1) -> (rule5 % int2)) triple7) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion eats the dog.
("lion" "eats" "dog" "+")
int3
The lion chases the dog.
("lion" "chases" "dog" "+")
int4
The lion is not kind.
False
2
inv-proof
[(((triple10) -> rule4) OR ((((triple6 triple1) -> rule5)) -> rule4) OR ((((((triple5) -> rule1) triple1) -> rule5)) -> rule4) OR ((((((((triple2 triple1) -> rule8)) -> rule1) triple1) -> rule5)) -> rule4))]
("lion" "is" "kind" "-")
((triple10) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple6 triple1) -> (rule5 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((((triple5) -> (rule1 % int3)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion eats the dog.
("lion" "eats" "dog" "+")
int3
((((((((triple2 triple1) -> (rule8 % int4))) -> (rule1 % int3)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion eats the dog.
("lion" "eats" "dog" "+")
int3
The lion chases the dog.
("lion" "chases" "dog" "+")
int4
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "eats" "dog" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The dog chases the lion.[(triple1)] The dog eats the lion.[(triple2 OR ((triple7 triple10) -> rule7) OR ((triple7 ((triple6 triple1) -> rule5)) -> rule7) OR ((triple7 ((((triple5) -> rule1) triple1) -> rule5)) -> rule7))] The dog is big.[(triple3)] The dog visits the lion.[(triple4)] The lion chases the dog.[(triple5 OR ((triple2 triple1) -> rule8) OR ((((triple7 triple10) -> rule7) triple1) -> rule8) OR ((((triple7 ((triple6 triple1) -> rule5)) -> rule7) triple1) -> rule8))] The lion eats the dog.[(triple6 OR ((triple5) -> rule1) OR ((((triple2 triple1) -> rule8)) -> rule1) OR ((((((triple7 triple10) -> rule7) triple1) -> rule8)) -> rule1))] The lion is big.[(triple7)] The lion is red.[(triple8)] The lion is young.[(triple9)] The lion visits the dog.[(triple10 OR ((triple6 triple1) -> rule5) OR ((((triple5) -> rule1) triple1) -> rule5) OR ((((((triple2 triple1) -> rule8)) -> rule1) triple1) -> rule5))] @1: The dog is kind.[(((triple10 triple7) -> rule6) OR ((((triple6 triple1) -> rule5) triple7) -> rule6) OR ((((((triple5) -> rule1) triple1) -> rule5) triple7) -> rule6) OR ((((((((triple2 triple1) -> rule8)) -> rule1) triple1) -> rule5) triple7) -> rule6))] The dog is young.[(((triple1) -> rule2))] The lion is kind.[(((triple10) -> rule4) OR ((((triple6 triple1) -> rule5)) -> rule4) OR ((((((triple5) -> rule1) triple1) -> rule5)) -> rule4) OR ((((((((triple2 triple1) -> rule8)) -> rule1) triple1) -> rule5)) -> rule4))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The dog eats the lion.
("dog" "eats" "lion" "+")
triple2
((triple7 triple10) -> (rule7 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
((triple7 ((triple6 triple1) -> (rule5 % int2))) -> (rule7 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((triple7 ((((triple5) -> (rule1 % int3)) triple1) -> (rule5 % int2))) -> (rule7 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion eats the dog.
("lion" "eats" "dog" "+")
int3
The dog is big.
("dog" "is" "big" "+")
triple3
The dog visits the lion.
("dog" "visits" "lion" "+")
triple4
The lion chases the dog.
("lion" "chases" "dog" "+")
triple5
((triple2 triple1) -> (rule8 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
((((triple7 triple10) -> (rule7 % int2)) triple1) -> (rule8 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The dog eats the lion.
("dog" "eats" "lion" "+")
int2
((((triple7 ((triple6 triple1) -> (rule5 % int3))) -> (rule7 % int2)) triple1) -> (rule8 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The dog eats the lion.
("dog" "eats" "lion" "+")
int2
The lion visits the dog.
("lion" "visits" "dog" "+")
int3
The lion eats the dog.
("lion" "eats" "dog" "+")
triple6
((triple5) -> (rule1 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
((((triple2 triple1) -> (rule8 % int2))) -> (rule1 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
((((((triple7 triple10) -> (rule7 % int3)) triple1) -> (rule8 % int2))) -> (rule1 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
The dog eats the lion.
("dog" "eats" "lion" "+")
int3
The lion is big.
("lion" "is" "big" "+")
triple7
The lion is red.
("lion" "is" "red" "+")
triple8
The lion is young.
("lion" "is" "young" "+")
triple9
The lion visits the dog.
("lion" "visits" "dog" "+")
triple10
((triple6 triple1) -> (rule5 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
((((triple5) -> (rule1 % int2)) triple1) -> (rule5 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion eats the dog.
("lion" "eats" "dog" "+")
int2
((((((triple2 triple1) -> (rule8 % int3))) -> (rule1 % int2)) triple1) -> (rule5 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion eats the dog.
("lion" "eats" "dog" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
((triple10 triple7) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
((((triple6 triple1) -> (rule5 % int2)) triple7) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((((triple5) -> (rule1 % int3)) triple1) -> (rule5 % int2)) triple7) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion eats the dog.
("lion" "eats" "dog" "+")
int3
((((((((triple2 triple1) -> (rule8 % int4))) -> (rule1 % int3)) triple1) -> (rule5 % int2)) triple7) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion eats the dog.
("lion" "eats" "dog" "+")
int3
The lion chases the dog.
("lion" "chases" "dog" "+")
int4
The dog is young.
("dog" "is" "young" "+")
((triple1) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((triple10) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple6 triple1) -> (rule5 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((((triple5) -> (rule1 % int3)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion eats the dog.
("lion" "eats" "dog" "+")
int3
((((((((triple2 triple1) -> (rule8 % int4))) -> (rule1 % int3)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion eats the dog.
("lion" "eats" "dog" "+")
int3
The lion chases the dog.
("lion" "chases" "dog" "+")
int4