Anne is round. Bob is cold. Gary is furry. All cold, round people are rough. Round, kind people are blue. All kind people are round. Furry, green people are cold. If Anne is round then Anne is kind. If someone is round and blue then they are green. If someone is green and rough then they are cold. Furry, blue people are cold.
Anne is round.
("Anne" "is" "round" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
All cold, round people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Round, kind people are blue.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Furry, green people are cold.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If Anne is round then Anne is kind.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "kind" "+"))
If someone is round and blue then they are green.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If someone is green and rough then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Furry, blue people are cold.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Bob is cold.
True
1
proof
[(triple2)]
("Bob" "is" "cold" "+")
triple2
Bob is not cold.
False
1
inv-proof
[(triple2)]
("Bob" "is" "cold" "-")
triple2
Anne is kind.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "kind" "-")
((triple1) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule2))]
("Anne" "is" "blue" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule2))]
("Anne" "is" "blue" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is green.
True
6
proof
[(((triple1 ((triple1 ((triple1) -> rule5)) -> rule2)) -> rule6))]
("Anne" "is" "green" "+")
((triple1 ((triple1 ((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is not green.
False
6
inv-proof
[(((triple1 ((triple1 ((triple1) -> rule5)) -> rule2)) -> rule6))]
("Anne" "is" "green" "-")
((triple1 ((triple1 ((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Gary is not cold.
Unknown
inv-rconc
[@3: Gary is cold.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule3 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is rough.
Unknown
rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Gary" "is" "rough" "+")
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "round" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is round.[(triple1)] Bob is cold.[(triple2)] Gary is furry.[(triple3)] @1: Anne is kind.[(((triple1) -> rule5))] @2: Anne is blue.[(((triple1 ((triple1) -> rule5)) -> rule2))] @3: Anne is green.[(((triple1 ((triple1 ((triple1) -> rule5)) -> rule2)) -> rule6))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((triple1 ((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3