Bob is nice. Charlie is kind. Dave is furry. Gary is not green. If something is furry and red then it is not green. If something is kind then it is furry. All furry things are big. If something is furry and nice then it is not cold. All nice things are not cold. If something is kind and not big then it is nice.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Gary is not green.
("Gary" "is" "green" "-")
If something is furry and red then it is not green.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "-"))
If something is kind then it is furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
All furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is furry and nice then it is not cold.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "-"))
All nice things are not cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "-"))
If something is kind and not big then it is nice.
((("something" "is" "kind" "+") ("something" "is" "big" "~")) -> ("something" "is" "nice" "+"))
Dave is furry.
True
1
proof
[(triple3)]
("Dave" "is" "furry" "+")
triple3
Dave is not furry.
False
1
inv-proof
[(triple3)]
("Dave" "is" "furry" "-")
triple3
Charlie is furry.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "furry" "-")
((triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is big.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Charlie" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Charlie" "is" "big" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "furry" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Gary" "is" "big" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Bob is nice.[(triple1)] Charlie is kind.[(triple2)] Dave is furry.[(triple3)] Gary is not green.[(triple4)] @1: Bob is not cold.[(((triple1) -> rule5))] Charlie is furry.[(((triple2) -> rule2))] Dave is big.[(((triple3) -> rule3))] @2: Charlie is big.[(((((triple2) -> rule2)) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Gary is not green.
("Gary" "is" "green" "-")
triple4
Bob is not cold.
("Bob" "is" "cold" "-")
((triple1) -> (rule5 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple3) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2