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