Anne is smart. Harry is round. Harry is young. Round, green things are kind. If Harry is round then Harry is green. If something is young then it is smart. If Anne is kind and Anne is round then Anne is young. If something is big and round then it is young. Kind things are round.
Anne is smart.
("Anne" "is" "smart" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
Round, green things are kind.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If Harry is round then Harry is green.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "green" "+"))
If something is young then it is smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If Anne is kind and Anne is round then Anne is young.
((("Anne" "is" "kind" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "young" "+"))
If something is big and round then it is young.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
Kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Anne is smart.
True
1
proof
[(triple1)]
("Anne" "is" "smart" "+")
triple1
Harry is not young.
False
1
inv-proof
[(triple3)]
("Harry" "is" "young" "-")
triple3
Harry is smart.
True
2
proof
[(((triple3) -> rule3))]
("Harry" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple2) -> rule2))]
("Harry" "is" "green" "-")
((triple2) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Anne is not young.
Unknown
inv-rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Anne is smart.[(triple1)] Harry is round.[(triple2)] Harry is young.[(triple3)] @1: Harry is green.[(((triple2) -> rule2))] Harry is smart.[(((triple3) -> rule3))] @2: Harry is kind.[(((triple2 ((triple2) -> rule2)) -> rule1))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Harry is round.
("Harry" "is" "round" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
((triple2) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2