Bob is round. Bob is smart. Bob is white. Charlie is kind. Charlie is red. Harry is kind. Harry is nice. Harry is red. Harry is not rough. Harry is round. Harry is smart. Harry is white. If Bob is smart then Bob is rough. If Harry is smart and Harry is red then Harry is kind. If Charlie is round and Charlie is not nice then Charlie is not kind.
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If Bob is smart then Bob is rough.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "rough" "+"))
If Harry is smart and Harry is red then Harry is kind.
((("Harry" "is" "smart" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "kind" "+"))
If Charlie is round and Charlie is not nice then Charlie is not kind.
((("Charlie" "is" "round" "+") ("Charlie" "is" "nice" "~")) -> ("Charlie" "is" "kind" "-"))
Harry is kind.
True
1
proof
[(triple6 OR ((triple11 triple8) -> rule2))]
("Harry" "is" "kind" "+")
triple6
((triple11 triple8) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Bob is not white.
False
1
inv-proof
[(triple3)]
("Bob" "is" "white" "-")
triple3
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is round.[(triple1)] Bob is smart.[(triple2)] Bob is white.[(triple3)] Charlie is kind.[(triple4)] Charlie is red.[(triple5)] Harry is kind.[(triple6 OR ((triple11 triple8) -> rule2))] Harry is nice.[(triple7)] Harry is not rough.[(triple9)] Harry is red.[(triple8)] Harry is round.[(triple10)] Harry is smart.[(triple11)] Harry is white.[(triple12)] @1: Bob is rough.[(((triple2) -> rule1))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
((triple11 triple8) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Harry is not rough.
("Harry" "is" "rough" "-")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Bob is rough.
("Bob" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1