Bob is furry. Bob is nice. Charlie is big. Dave is kind. Dave is quiet. Gary is big. Gary is kind. If something is nice then it is kind. If Dave is blue and Dave is green then Dave is furry. All nice things are green.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If something is nice then it is kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If Dave is blue and Dave is green then Dave is furry.
((("Dave" "is" "blue" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "furry" "+"))
All nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Dave is quiet.
True
1
proof
[(triple5)]
("Dave" "is" "quiet" "+")
triple5
Gary is not kind.
False
1
inv-proof
[(triple7)]
("Gary" "is" "kind" "-")
triple7
Bob is kind.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "kind" "-")
((triple2) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "green" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Bob is furry.[(triple1)] Bob is nice.[(triple2)] Charlie is big.[(triple3)] Dave is kind.[(triple4)] Dave is quiet.[(triple5)] Gary is big.[(triple6)] Gary is kind.[(triple7)] @1: Bob is green.[(((triple2) -> rule3))] Bob is kind.[(((triple2) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1