Bob is furry. Bob is not nice. Bob is rough. Bob is round. Bob is white. Charlie is furry. Harry is not nice. Harry is quiet. Harry is not rough. Harry is not white. If something is quiet then it is smart.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is not white.
("Harry" "is" "white" "-")
If something is quiet then it is smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Harry is not rough.
True
1
proof
[(triple9)]
("Harry" "is" "rough" "-")
triple9
Bob is not white.
False
1
inv-proof
[(triple5)]
("Bob" "is" "white" "-")
triple5
Harry is smart.
True
2
proof
[(((triple8) -> rule1))]
("Harry" "is" "smart" "+")
((triple8) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple8) -> rule1))]
("Harry" "is" "smart" "-")
((triple8) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "smart" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Bob is furry.[(triple1)] Bob is not nice.[(triple2)] Bob is rough.[(triple3)] Bob is round.[(triple4)] Bob is white.[(triple5)] Charlie is furry.[(triple6)] Harry is not nice.[(triple7)] Harry is not rough.[(triple9)] Harry is not white.[(triple10)] Harry is quiet.[(triple8)] @1: Harry is smart.[(((triple8) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is not nice.
("Bob" "is" "nice" "-")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Harry is not nice.
("Harry" "is" "nice" "-")
triple7
Harry is not rough.
("Harry" "is" "rough" "-")
triple9
Harry is not white.
("Harry" "is" "white" "-")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
((triple8) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1