Anne is quiet. Charlie is rough. Gary is rough. Harry is young. If Charlie is rough then Charlie is round. If Anne is quiet and Anne is smart then Anne is young. All green people are rough.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
If Charlie is rough then Charlie is round.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "round" "+"))
If Anne is quiet and Anne is smart then Anne is young.
((("Anne" "is" "quiet" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "young" "+"))
All green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Harry is young.
True
1
proof
[(triple4)]
("Harry" "is" "young" "+")
triple4
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "rough" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Anne is quiet.[(triple1)] Charlie is rough.[(triple2)] Gary is rough.[(triple3)] Harry is young.[(triple4)] @1: Charlie is round.[(((triple2) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
((triple2) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1