The dog is cold. All young things are cold. All big things are nice. All green, young things are big. Big, cold things are young. Green things are young. Nice, big things are cold. Big, cold things are nice. If the dog is young then the dog is green.
The dog is cold.
("dog" "is" "cold" "+")
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
All green, young things are big.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Big, cold things are young.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
Nice, big things are cold.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Big, cold things are nice.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If the dog is young then the dog is green.
((("dog" "is" "young" "+")) -> ("dog" "is" "green" "+"))
The dog is cold.
True
1
proof
[(triple1)]
("dog" "is" "cold" "+")
triple1
The dog is not cold.
False
1
inv-proof
[(triple1)]
("dog" "is" "cold" "-")
triple1
The dog is not green.
Unknown
inv-rconc
[@3: The dog is green.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule3 <- FAIL)]]
("dog" "is" "green" "-")
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)]
The dog is cold.
("dog" "is" "cold" "+")
triple1