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