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