Anne is young. Charlie is not cold. Dave is not big. Fiona is cold. If Anne is smart and Anne is round then Anne is young. If something is round then it is not smart. All round, cold things are not smart. If something is smart then it is nice. All cold, round things are nice. If Dave is not big and Dave is not round then Dave is cold.
Anne is young.
("Anne" "is" "young" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Dave is not big.
("Dave" "is" "big" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
If Anne is smart and Anne is round then Anne is young.
((("Anne" "is" "smart" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "young" "+"))
If something is round then it is not smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "-"))
All round, cold things are not smart.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "-"))
If something is smart then it is nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
All cold, round things are nice.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If Dave is not big and Dave is not round then Dave is cold.
((("Dave" "is" "big" "~") ("Dave" "is" "round" "~")) -> ("Dave" "is" "cold" "+"))
Anne is young.
True
1
proof
[(triple1)]
("Anne" "is" "young" "+")
triple1
Anne is not young.
False
1
inv-proof
[(triple1)]
("Anne" "is" "young" "-")
triple1
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Anne is young.[(triple1)] Charlie is not cold.[(triple2)] Dave is not big.[(triple3)] Fiona is cold.[(triple4)]
Anne is young.
("Anne" "is" "young" "+")
triple1
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
Dave is not big.
("Dave" "is" "big" "-")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4