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