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