Bob is cold. Bob is furry. Bob is kind. Bob is quiet. Bob is red. Bob is round. Bob is smart. Charlie is furry. Charlie is kind. Charlie is red. Harry is cold. Harry is furry. Harry is quiet. Harry is round. Harry is smart. Cold people are kind. If Charlie is smart then Charlie is kind.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is smart then Charlie is kind.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "kind" "+"))
Harry is quiet.
True
1
proof
[(triple13)]
("Harry" "is" "quiet" "+")
triple13
Charlie is not kind.
False
1
inv-proof
[(triple9)]
("Charlie" "is" "kind" "-")
triple9
Harry is kind.
True
2
proof
[(((triple11) -> rule1))]
("Harry" "is" "kind" "+")
((triple11) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple11) -> rule1))]
("Harry" "is" "kind" "-")
((triple11) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2)] Bob is kind.[(triple3 OR ((triple1) -> rule1))] Bob is quiet.[(triple4)] Bob is red.[(triple5)] Bob is round.[(triple6)] Bob is smart.[(triple7)] Charlie is furry.[(triple8)] Charlie is kind.[(triple9)] Charlie is red.[(triple10)] Harry is cold.[(triple11)] Harry is furry.[(triple12)] Harry is quiet.[(triple13)] Harry is round.[(triple14)] Harry is smart.[(triple15)] @1: Harry is kind.[(((triple11) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
Charlie is kind.
("Charlie" "is" "kind" "+")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Harry is kind.
("Harry" "is" "kind" "+")
((triple11) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1