Anne is rough. Gary is nice. Harry is green. All red people are young. Rough people are green. If someone is green then they are young. All young, red people are quiet. If someone is rough then they are young. Rough people are young. If Harry is smart then Harry is quiet. If someone is nice then they are quiet.
Anne is rough.
("Anne" "is" "rough" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is green.
("Harry" "is" "green" "+")
All red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
All young, red people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If someone is rough then they are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
Rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If Harry is smart then Harry is quiet.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "quiet" "+"))
If someone is nice then they are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Harry is not green.
False
1
inv-proof
[(triple3)]
("Harry" "is" "green" "-")
triple3
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "quiet" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Anne is rough.[(triple1)] Gary is nice.[(triple2)] Harry is green.[(triple3)] @1: Anne is green.[(((triple1) -> rule2))] Anne is young.[(((triple1) -> rule5) OR ((triple1) -> rule6) OR ((((triple1) -> rule2)) -> rule3))] Gary is quiet.[(((triple2) -> rule8))] Harry is young.[(((triple3) -> rule3))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple1) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple2) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple3) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1