The dog chases the lion. The dog eats the lion. The dog is green. The dog is rough. The dog is young. The dog needs the lion. The lion chases the dog. The lion eats the dog. The lion is blue. The lion is green. The lion is young. The lion needs the dog. If something is blue and it chases the dog then the dog is rough. If something chases the lion and the lion eats the dog then it eats the dog. If something chases the lion then it is green.
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
If something is blue and it chases the dog then the dog is rough.
((("something" "is" "blue" "+") ("something" "chases" "dog" "+")) -> ("dog" "is" "rough" "+"))
If something chases the lion and the lion eats the dog then it eats the dog.
((("something" "chases" "lion" "+") ("lion" "eats" "dog" "+")) -> ("something" "eats" "dog" "+"))
If something chases the lion then it is green.
((("something" "chases" "lion" "+")) -> ("something" "is" "green" "+"))
The dog needs the lion.
True
1
proof
[(triple6)]
("dog" "needs" "lion" "+")
triple6
The lion does not eat the dog.
False
1
inv-proof
[(triple8)]
("lion" "eats" "dog" "-")
triple8
The dog eats the dog.
True
3
proof
[(((triple1 triple8) -> rule2))]
("dog" "eats" "dog" "+")
((triple1 triple8) -> (rule2 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog does not eat the dog.
False
3
inv-proof
[(((triple1 triple8) -> rule2))]
("dog" "eats" "dog" "-")
((triple1 triple8) -> (rule2 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
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 chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The dog chases the lion.[(triple1)] The dog eats the lion.[(triple2)] The dog is green.[(triple3 OR ((triple1) -> rule3))] The dog is rough.[(triple4 OR ((triple9 triple7) -> rule1))] The dog is young.[(triple5)] The dog needs the lion.[(triple6)] The lion chases the dog.[(triple7)] The lion eats the dog.[(triple8)] The lion is blue.[(triple9)] The lion is green.[(triple10)] The lion is young.[(triple11)] The lion needs the dog.[(triple12)] @1: The dog eats the dog.[(((triple1 triple8) -> rule2))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The dog eats the lion.
("dog" "eats" "lion" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
((triple1) -> (rule3 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
triple4
((triple9 triple7) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is young.
("dog" "is" "young" "+")
triple5
The dog needs the lion.
("dog" "needs" "lion" "+")
triple6
The lion chases the dog.
("lion" "chases" "dog" "+")
triple7
The lion eats the dog.
("lion" "eats" "dog" "+")
triple8
The lion is blue.
("lion" "is" "blue" "+")
triple9
The lion is green.
("lion" "is" "green" "+")
triple10
The lion is young.
("lion" "is" "young" "+")
triple11
The lion needs the dog.
("lion" "needs" "dog" "+")
triple12
The dog eats the dog.
("dog" "eats" "dog" "+")
((triple1 triple8) -> (rule2 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1