Bob is furry. Charlie is big. Dave is kind. Gary is blue. If someone is red and not quiet then they are big. If Bob is furry then Bob is not blue. If Dave is quiet and Dave is red then Dave is big. If someone is kind then they are not red. Kind people are furry. If someone is kind and not big then they are not blue. If someone is furry and not red then they are nice. Kind, quiet people are nice.
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is blue.
("Gary" "is" "blue" "+")
If someone is red and not quiet then they are big.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "big" "+"))
If Bob is furry then Bob is not blue.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "blue" "-"))
If Dave is quiet and Dave is red then Dave is big.
((("Dave" "is" "quiet" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "big" "+"))
If someone is kind then they are not red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "-"))
Kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
If someone is kind and not big then they are not blue.
((("someone" "is" "kind" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "blue" "-"))
If someone is furry and not red then they are nice.
((("someone" "is" "furry" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "nice" "+"))
Kind, quiet people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Charlie is big.
True
1
proof
[(triple2)]
("Charlie" "is" "big" "+")
triple2
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Dave is not red.
True
2
proof
[(((triple3) -> rule4))]
("Dave" "is" "red" "-")
((triple3) -> (rule4 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is red.
False
2
inv-proof
[(((triple3) -> rule4))]
("Dave" "is" "red" "+")
((triple3) -> (rule4 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "big" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "nice" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is furry.[(triple1)] Charlie is big.[(triple2)] Dave is kind.[(triple3)] Gary is blue.[(triple4)] @1: Bob is not blue.[(((triple1) -> rule2))] Dave is furry.[(((triple3) -> rule5))] Dave is not red.[(((triple3) -> rule4))] @2: Dave is nice.[(((((triple3) -> rule5) ((triple3) -> rule4)) -> rule7))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Bob is not blue.
("Bob" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple3) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not red.
("Dave" "is" "red" "-")
((triple3) -> (rule4 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple3) -> (rule5 % int3)) ((triple3) -> (rule4 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not red.
("Dave" "is" "red" "-")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3