The dog is cold. The dog is green. The dog is nice. If the dog is cold and the dog is big then the dog is green. If the dog is green then the dog is cold. If someone is red and big then they are cold.
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is nice.
("dog" "is" "nice" "+")
If the dog is cold and the dog is big then the dog is green.
((("dog" "is" "cold" "+") ("dog" "is" "big" "+")) -> ("dog" "is" "green" "+"))
If the dog is green then the dog is cold.
((("dog" "is" "green" "+")) -> ("dog" "is" "cold" "+"))
If someone is red and big then they are cold.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
The dog is cold.
True
1
proof
[(triple1 OR ((triple2) -> rule2))]
("dog" "is" "cold" "+")
triple1
((triple2) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is not nice.
False
1
inv-proof
[(triple3)]
("dog" "is" "nice" "-")
triple3
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 dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
@0: The dog is cold.[(triple1 OR ((triple2) -> rule2))] The dog is green.[(triple2)] The dog is nice.[(triple3)]
The dog is cold.
("dog" "is" "cold" "+")
triple1
((triple2) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3