Bob is blue. Dave is rough. Harry is rough. If something is round then it is not rough. All rough things are not quiet. If Bob is round then Bob is not red. If something is quiet and not round then it is kind. If something is blue and not rough then it is kind. Kind, round things are blue. If something is quiet and not kind then it is furry. All quiet things are furry.
Bob is blue.
("Bob" "is" "blue" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If something is round then it is not rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "-"))
All rough things are not quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "-"))
If Bob is round then Bob is not red.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "red" "-"))
If something is quiet and not round then it is kind.
((("something" "is" "quiet" "+") ("something" "is" "round" "~")) -> ("something" "is" "kind" "+"))
If something is blue and not rough then it is kind.
((("something" "is" "blue" "+") ("something" "is" "rough" "~")) -> ("something" "is" "kind" "+"))
Kind, round things are blue.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is quiet and not kind then it is furry.
((("something" "is" "quiet" "+") ("something" "is" "kind" "~")) -> ("something" "is" "furry" "+"))
All quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Harry is not rough.
False
1
inv-proof
[(triple3)]
("Harry" "is" "rough" "-")
triple3
Dave is not quiet.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Harry is quiet.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Bob is blue.[(triple1)] Dave is rough.[(triple2)] Harry is rough.[(triple3)] @1: Dave is not quiet.[(((triple2) -> rule2))] Harry is not quiet.[(((triple3) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Dave is not quiet.
("Dave" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Harry is not quiet.
("Harry" "is" "quiet" "-")
((triple3) -> (rule2 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1