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