The dog is cold. The dog is green. The dog is kind. The dog is red. The dog is young. If the dog is kind then the dog is green. If something is young then it is cold.
The dog is cold.
("dog" "is" "cold" "+")
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" "+")
If the dog is kind then the dog is green.
((("dog" "is" "kind" "+")) -> ("dog" "is" "green" "+"))
If something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
The dog is green.
True
1
proof
[(triple2 OR ((triple3) -> rule1))]
("dog" "is" "green" "+")
triple2
((triple3) -> (rule1 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is not kind.
False
1
inv-proof
[(triple3)]
("dog" "is" "kind" "-")
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 chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The dog is cold.[(triple1 OR ((triple5) -> rule2))] The dog is green.[(triple2 OR ((triple3) -> rule1))] The dog is kind.[(triple3)] The dog is red.[(triple4)] The dog is young.[(triple5)]
The dog is cold.
("dog" "is" "cold" "+")
triple1
((triple5) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is green.
("dog" "is" "green" "+")
triple2
((triple3) -> (rule1 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5