Anne is cold. Charlie is smart. Dave is not red. Cold people are red. If Dave is green then Dave is not red. If someone is smart and red then they are not round. If Anne is big and Anne is not smart then Anne is green. If someone is young and not cold then they are green. If someone is big then they are not green.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is not red.
("Dave" "is" "red" "-")
Cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If Dave is green then Dave is not red.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "red" "-"))
If someone is smart and red then they are not round.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "-"))
If Anne is big and Anne is not smart then Anne is green.
((("Anne" "is" "big" "+") ("Anne" "is" "smart" "~")) -> ("Anne" "is" "green" "+"))
If someone is young and not cold then they are green.
((("someone" "is" "young" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "green" "+"))
If someone is big then they are not green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "-"))
Dave is not red.
True
1
proof
[(triple3)]
("Dave" "is" "red" "-")
triple3
Charlie is not smart.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "smart" "-")
triple2
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "green" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is cold.[(triple1)] Charlie is smart.[(triple2)] Dave is not red.[(triple3)] @1: Anne is red.[(((triple1) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Dave is not red.
("Dave" "is" "red" "-")
triple3
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1