Bob is furry. Charlie is cold. Harry is green. Cold people are furry. If someone is furry and not kind then they are rough. If someone is furry then they are green.
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and not kind then they are rough.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "rough" "+"))
If someone is furry then they are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
Charlie is cold.
True
1
proof
[(triple2)]
("Charlie" "is" "cold" "+")
triple2
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Bob is green.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "green" "+")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "green" "-")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is green.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "green" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is furry.
Unknown
rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "furry" "+")
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "rough" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Bob is furry.[(triple1)] Charlie is cold.[(triple2)] Harry is green.[(triple3)] @1: Bob is green.[(((triple1) -> rule3))] Charlie is furry.[(((triple2) -> rule1))] @2: Charlie is green.[(((((triple2) -> rule1)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2