The dog eats the lion. The dog is green. The dog is kind. The dog is rough. The dog is round. The dog is young. The dog needs the lion. The dog visits the lion. The lion eats the dog. The lion is green. The lion is kind. The lion is round. The lion is young. The lion needs the dog. The lion visits the dog. If someone visits the dog then they are green. If someone needs the dog and the dog is young then they need the lion. If someone is young and they visit the lion then the lion visits the dog. If someone is young and they visit the lion then the lion visits the dog. If the lion visits the dog then the dog eats the lion. If someone needs the dog then they are green.
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If someone visits the dog then they are green.
((("someone" "visits" "dog" "+")) -> ("someone" "is" "green" "+"))
If someone needs the dog and the dog is young then they need the lion.
((("someone" "needs" "dog" "+") ("dog" "is" "young" "+")) -> ("someone" "needs" "lion" "+"))
If someone is young and they visit the lion then the lion visits the dog.
((("someone" "is" "young" "+") ("someone" "visits" "lion" "+")) -> ("lion" "visits" "dog" "+"))
If someone is young and they visit the lion then the lion visits the dog.
((("someone" "is" "young" "+") ("someone" "visits" "lion" "+")) -> ("lion" "visits" "dog" "+"))
If the lion visits the dog then the dog eats the lion.
((("lion" "visits" "dog" "+")) -> ("dog" "eats" "lion" "+"))
If someone needs the dog then they are green.
((("someone" "needs" "dog" "+")) -> ("someone" "is" "green" "+"))
The lion visits the dog.
True
1
proof
[(triple15 OR ((triple6 triple8) -> rule3) OR ((triple6 triple8) -> rule4))]
("lion" "visits" "dog" "+")
triple15
((triple6 triple8) -> (rule3 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
((triple6 triple8) -> (rule4 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The dog does not visit the lion.
False
1
inv-proof
[(triple8)]
("dog" "visits" "lion" "-")
triple8
The lion needs the lion.
True
3
proof
[(((triple14 triple6) -> rule2))]
("lion" "needs" "lion" "+")
((triple14 triple6) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion does not need the lion.
False
3
inv-proof
[(((triple14 triple6) -> rule2))]
("lion" "needs" "lion" "-")
((triple14 triple6) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
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 visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
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 eats the lion.[(triple1 OR ((triple15) -> rule5) OR ((((triple6 triple8) -> rule3)) -> rule5) OR ((((triple6 triple8) -> rule4)) -> rule5))] The dog is green.[(triple2)] The dog is kind.[(triple3)] The dog is rough.[(triple4)] The dog is round.[(triple5)] The dog is young.[(triple6)] The dog needs the lion.[(triple7)] The dog visits the lion.[(triple8)] The lion eats the dog.[(triple9)] The lion is green.[(triple10 OR ((triple14) -> rule6) OR ((triple15) -> rule1) OR ((((triple6 triple8) -> rule3)) -> rule1) OR ((((triple6 triple8) -> rule4)) -> rule1))] The lion is kind.[(triple11)] The lion is round.[(triple12)] The lion is young.[(triple13)] The lion needs the dog.[(triple14)] The lion visits the dog.[(triple15 OR ((triple6 triple8) -> rule3) OR ((triple6 triple8) -> rule4))] @1: The lion needs the lion.[(((triple14 triple6) -> rule2))]
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
((triple15) -> (rule5 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
((((triple6 triple8) -> (rule3 % int2))) -> (rule5 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((triple6 triple8) -> (rule4 % int2))) -> (rule5 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The dog is young.
("dog" "is" "young" "+")
triple6
The dog needs the lion.
("dog" "needs" "lion" "+")
triple7
The dog visits the lion.
("dog" "visits" "lion" "+")
triple8
The lion eats the dog.
("lion" "eats" "dog" "+")
triple9
The lion is green.
("lion" "is" "green" "+")
triple10
((triple14) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
((triple15) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
((((triple6 triple8) -> (rule3 % int2))) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
((((triple6 triple8) -> (rule4 % int2))) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
triple11
The lion is round.
("lion" "is" "round" "+")
triple12
The lion is young.
("lion" "is" "young" "+")
triple13
The lion needs the dog.
("lion" "needs" "dog" "+")
triple14
The lion visits the dog.
("lion" "visits" "dog" "+")
triple15
((triple6 triple8) -> (rule3 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
((triple6 triple8) -> (rule4 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple14 triple6) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1