Anne is green. Anne is rough. Bob is furry. Bob is quiet. Charlie is cold. Charlie is quiet. Harry is furry. If someone is red then they are cold. All quiet, furry people are blue. All blue people are cold. Quiet, rough people are green. If someone is rough and quiet then they are blue. All blue, furry people are red.
Anne is green.
("Anne" "is" "green" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
All quiet, furry people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
All blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Quiet, rough people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is rough and quiet then they are blue.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
All blue, furry people are red.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Bob is quiet.
True
1
proof
[(triple4)]
("Bob" "is" "quiet" "+")
triple4
Harry is not furry.
False
1
inv-proof
[(triple7)]
("Harry" "is" "furry" "-")
triple7
Bob is blue.
True
3
proof
[(((triple4 triple3) -> rule2))]
("Bob" "is" "blue" "+")
((triple4 triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
3
inv-proof
[(((triple4 triple3) -> rule2))]
("Bob" "is" "blue" "-")
((triple4 triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "green" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "red" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is green.[(triple1)] Anne is rough.[(triple2)] Bob is furry.[(triple3)] Bob is quiet.[(triple4)] Charlie is cold.[(triple5)] Charlie is quiet.[(triple6)] Harry is furry.[(triple7)] @1: Bob is blue.[(((triple4 triple3) -> rule2))] @2: Bob is cold.[(((((triple4 triple3) -> rule2)) -> rule3) OR ((((((triple4 triple3) -> rule2) triple3) -> rule6)) -> rule1))] Bob is red.[(((((triple4 triple3) -> rule2) triple3) -> rule6))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
((triple4 triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple4 triple3) -> (rule2 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple4 triple3) -> (rule2 % int3)) triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((((triple4 triple3) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2