Bob is kind. Gary is quiet. Harry is young. If Gary is young then Gary is smart. If Harry is red then Harry is young. Smart, kind people are round. If Gary is round then Gary is smart. Quiet people are smart. All quiet, kind people are young.
Bob is kind.
("Bob" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
If Gary is young then Gary is smart.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "smart" "+"))
If Harry is red then Harry is young.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "young" "+"))
Smart, kind people are round.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If Gary is round then Gary is smart.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "smart" "+"))
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All quiet, kind people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Gary is quiet.
True
1
proof
[(triple2)]
("Gary" "is" "quiet" "+")
triple2
Bob is not kind.
False
1
inv-proof
[(triple1)]
("Bob" "is" "kind" "-")
triple1
Gary is smart.
True
2
proof
[(((triple2) -> rule5))]
("Gary" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple2) -> rule5))]
("Gary" "is" "smart" "-")
((triple2) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "young" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "smart" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is kind.[(triple1)] Gary is quiet.[(triple2)] Harry is young.[(triple3)] @1: Gary is smart.[(((triple2) -> rule5))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1