The dog does not chase the lion. The dog is cold. The dog is not green. The dog is red. The dog is rough. The dog is not young. The dog likes the lion. The dog does not need the lion. The lion chases the dog. The lion is cold. The lion is green. The lion is red. The lion is rough. The lion is young. The lion does not like the dog. The lion needs the dog. If someone likes the dog then the dog chases the lion. If someone chases the lion then the lion needs the dog. If the dog needs the lion and the lion likes the dog then the lion is red. If the dog is not green and the dog does not chase the lion then the dog is rough. If someone likes the dog and the dog is rough then they need the lion. If someone needs the dog then they need the lion. If someone needs the lion then they do not like the lion. If someone likes the lion and they chase the lion then they are rough.
The dog does not chase the lion.
("dog" "chases" "lion" "-")
The dog is cold.
("dog" "is" "cold" "+")
The dog is not green.
("dog" "is" "green" "-")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is not young.
("dog" "is" "young" "-")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog does not need the lion.
("dog" "needs" "lion" "-")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion does not like the dog.
("lion" "likes" "dog" "-")
The lion needs the dog.
("lion" "needs" "dog" "+")
If someone likes the dog then the dog chases the lion.
((("someone" "likes" "dog" "+")) -> ("dog" "chases" "lion" "+"))
If someone chases the lion then the lion needs the dog.
((("someone" "chases" "lion" "+")) -> ("lion" "needs" "dog" "+"))
If the dog needs the lion and the lion likes the dog then the lion is red.
((("dog" "needs" "lion" "+") ("lion" "likes" "dog" "+")) -> ("lion" "is" "red" "+"))
If the dog is not green and the dog does not chase the lion then the dog is rough.
((("dog" "is" "green" "~") ("dog" "chases" "lion" "~")) -> ("dog" "is" "rough" "+"))
If someone likes the dog and the dog is rough then they need the lion.
((("someone" "likes" "dog" "+") ("dog" "is" "rough" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the dog then they need the lion.
((("someone" "needs" "dog" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the lion then they do not like the lion.
((("someone" "needs" "lion" "+")) -> ("someone" "likes" "lion" "-"))
If someone likes the lion and they chase the lion then they are rough.
((("someone" "likes" "lion" "+") ("someone" "chases" "lion" "+")) -> ("someone" "is" "rough" "+"))
The lion is green.
True
1
proof
[(triple11)]
("lion" "is" "green" "+")
triple11
The dog is green.
False
1
inv-proof
[(triple3)]
("dog" "is" "green" "+")
triple3
The lion needs the lion.
True
2
proof
[(((triple16) -> rule6))]
("lion" "needs" "lion" "+")
((triple16) -> (rule6 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion does not need the lion.
False
2
inv-proof
[(((triple16) -> rule6))]
("lion" "needs" "lion" "-")
((triple16) -> (rule6 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion does not like the lion.
True
3
proof
[(((((triple16) -> rule6)) -> rule7))]
("lion" "likes" "lion" "-")
((((triple16) -> (rule6 % int2))) -> (rule7 % int1))
The lion does not like the lion.
("lion" "likes" "lion" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion likes the lion.
False
3
inv-proof
[(((((triple16) -> rule6)) -> rule7))]
("lion" "likes" "lion" "+")
((((triple16) -> (rule6 % int2))) -> (rule7 % int1))
The lion does not like the lion.
("lion" "likes" "lion" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
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 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 like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The dog does not chase the lion.[(triple1)] The dog does not need the lion.[(triple8)] The dog is cold.[(triple2)] The dog is not green.[(triple3)] The dog is not young.[(triple6)] The dog is red.[(triple4)] The dog is rough.[(triple5 OR ((triple3 triple1) -> rule4))] The dog likes the lion.[(triple7)] The lion chases the dog.[(triple9)] The lion does not like the dog.[(triple15)] The lion is cold.[(triple10)] The lion is green.[(triple11)] The lion is red.[(triple12)] The lion is rough.[(triple13)] The lion is young.[(triple14)] The lion needs the dog.[(triple16)] @1: The lion needs the lion.[(((triple16) -> rule6))] @2: The lion does not like the lion.[(((((triple16) -> rule6)) -> rule7))]
The dog does not chase the lion.
("dog" "chases" "lion" "-")
triple1
The dog does not need the lion.
("dog" "needs" "lion" "-")
triple8
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is not green.
("dog" "is" "green" "-")
triple3
The dog is not young.
("dog" "is" "young" "-")
triple6
The dog is red.
("dog" "is" "red" "+")
triple4
The dog is rough.
("dog" "is" "rough" "+")
triple5
((triple3 triple1) -> (rule4 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
triple7
The lion chases the dog.
("lion" "chases" "dog" "+")
triple9
The lion does not like the dog.
("lion" "likes" "dog" "-")
triple15
The lion is cold.
("lion" "is" "cold" "+")
triple10
The lion is green.
("lion" "is" "green" "+")
triple11
The lion is red.
("lion" "is" "red" "+")
triple12
The lion is rough.
("lion" "is" "rough" "+")
triple13
The lion is young.
("lion" "is" "young" "+")
triple14
The lion needs the dog.
("lion" "needs" "dog" "+")
triple16
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple16) -> (rule6 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion does not like the lion.
("lion" "likes" "lion" "-")
((((triple16) -> (rule6 % int2))) -> (rule7 % int1))
The lion does not like the lion.
("lion" "likes" "lion" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2