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