The dog is big. The dog is cold. The dog is green. The dog is kind. The dog is young. If someone is cold and not big then they are green. If someone is big and not green then they are not kind.
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is young.
("dog" "is" "young" "+")
If someone is cold and not big then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "green" "+"))
If someone is big and not green then they are not kind.
((("someone" "is" "big" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "kind" "-"))
The dog is young.
True
1
proof
[(triple5)]
("dog" "is" "young" "+")
triple5
The dog is not big.
False
1
inv-proof
[(triple1)]
("dog" "is" "big" "-")
triple1
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog is big.[(triple1)] The dog is cold.[(triple2)] The dog is green.[(triple3)] The dog is kind.[(triple4)] The dog is young.[(triple5)]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5