The dog chases the lion. The dog eats the lion. The dog is blue. The dog is green. The dog is kind. The dog is red. The dog is young. The dog sees the lion. The lion chases the dog. The lion eats the dog. The lion is blue. The lion sees the dog. If the lion chases the dog then the lion is not red. If someone is kind then they see the dog. If someone chases the dog and they are not red then they do not eat the lion.
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is young.
("dog" "is" "young" "+")
The dog sees the lion.
("dog" "sees" "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 sees the dog.
("lion" "sees" "dog" "+")
If the lion chases the dog then the lion is not red.
((("lion" "chases" "dog" "+")) -> ("lion" "is" "red" "-"))
If someone is kind then they see the dog.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "dog" "+"))
If someone chases the dog and they are not red then they do not eat the lion.
((("someone" "chases" "dog" "+") ("someone" "is" "red" "~")) -> ("someone" "eats" "lion" "-"))
The dog sees the lion.
True
1
proof
[(triple8)]
("dog" "sees" "lion" "+")
triple8
The lion does not eat the dog.
False
1
inv-proof
[(triple10)]
("lion" "eats" "dog" "-")
triple10
The lion is not red.
True
2
proof
[(((triple9) -> rule1))]
("lion" "is" "red" "-")
((triple9) -> (rule1 % int1))
The lion is not red.
("lion" "is" "red" "-")
int1
The lion is red.
False
2
inv-proof
[(((triple9) -> rule1))]
("lion" "is" "red" "+")
((triple9) -> (rule1 % int1))
The lion is not red.
("lion" "is" "red" "-")
int1
The lion does not eat the lion.
True
4
proof
[(((triple9 ((triple9) -> rule1)) -> rule3))]
("lion" "eats" "lion" "-")
((triple9 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion is not red.
("lion" "is" "red" "-")
int2
The lion eats the lion.
False
4
inv-proof
[(((triple9 ((triple9) -> rule1)) -> rule3))]
("lion" "eats" "lion" "+")
((triple9 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion is not red.
("lion" "is" "red" "-")
int2
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
@0: The dog chases the lion.[(triple1)] The dog eats the lion.[(triple2)] The dog is blue.[(triple3)] The dog is green.[(triple4)] The dog is kind.[(triple5)] The dog is red.[(triple6)] The dog is young.[(triple7)] The dog sees the lion.[(triple8)] The lion chases the dog.[(triple9)] The lion eats the dog.[(triple10)] The lion is blue.[(triple11)] The lion sees the dog.[(triple12)] @1: The dog sees the dog.[(((triple5) -> rule2))] The lion is not red.[(((triple9) -> rule1))] @2: The lion does not eat the lion.[(((triple9 ((triple9) -> rule1)) -> rule3))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The dog eats the lion.
("dog" "eats" "lion" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple5
The dog is red.
("dog" "is" "red" "+")
triple6
The dog is young.
("dog" "is" "young" "+")
triple7
The dog sees the lion.
("dog" "sees" "lion" "+")
triple8
The lion chases the dog.
("lion" "chases" "dog" "+")
triple9
The lion eats the dog.
("lion" "eats" "dog" "+")
triple10
The lion is blue.
("lion" "is" "blue" "+")
triple11
The lion sees the dog.
("lion" "sees" "dog" "+")
triple12
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple5) -> (rule2 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The lion is not red.
("lion" "is" "red" "-")
((triple9) -> (rule1 % int1))
The lion is not red.
("lion" "is" "red" "-")
int1
The lion does not eat the lion.
("lion" "eats" "lion" "-")
((triple9 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion is not red.
("lion" "is" "red" "-")
int2