Bob is cold. Charlie is not red. Dave is not quiet. Harry is kind. If someone is round then they are rough. All kind people are rough.
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Harry is kind.
("Harry" "is" "kind" "+")
If someone is round then they are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Harry is kind.
True
1
proof
[(triple4)]
("Harry" "is" "kind" "+")
triple4
Harry is not kind.
False
1
inv-proof
[(triple4)]
("Harry" "is" "kind" "-")
triple4
Harry is rough.
True
2
proof
[(((triple4) -> rule2))]
("Harry" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "rough" "-")
((triple4) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "rough" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "rough" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Bob is cold.[(triple1)] Charlie is not red.[(triple2)] Dave is not quiet.[(triple3)] Harry is kind.[(triple4)] @1: Harry is rough.[(((triple4) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Charlie is not red.
("Charlie" "is" "red" "-")
triple2
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1