Anne is furry. Charlie is furry. Fiona is cold. All cold, furry things are blue. If something is big then it is kind. Kind things are blue. All furry things are kind. If something is round and cold then it is big. All blue, kind things are cold.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
All cold, furry things are blue.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
All furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If something is round and cold then it is big.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All blue, kind things are cold.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Charlie is kind.
True
2
proof
[(((triple2) -> rule4))]
("Charlie" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple2) -> rule4))]
("Charlie" "is" "kind" "-")
((triple2) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Charlie is not blue.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3))]
("Charlie" "is" "blue" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Anne is cold.
True
6
proof
[(((((((triple1) -> rule4)) -> rule3) ((triple1) -> rule4)) -> rule6))]
("Anne" "is" "cold" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2)) ((triple1) -> (rule4 % int3))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Charlie is not cold.
False
6
inv-proof
[(((((((triple2) -> rule4)) -> rule3) ((triple2) -> rule4)) -> rule6))]
("Charlie" "is" "cold" "-")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "big" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "big" "+")
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "big" "-")
Fiona is blue.
Unknown
rconc
[@3: Fiona is blue.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule5 <- FAIL)]]
("Fiona" "is" "blue" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is furry.[(triple1)] Charlie is furry.[(triple2)] Fiona is cold.[(triple3)] @1: Anne is kind.[(((triple1) -> rule4))] Charlie is kind.[(((triple2) -> rule4))] @2: Anne is blue.[(((((triple1) -> rule4)) -> rule3))] Charlie is blue.[(((((triple2) -> rule4)) -> rule3))] @3: Anne is cold.[(((((((triple1) -> rule4)) -> rule3) ((triple1) -> rule4)) -> rule6))] Charlie is cold.[(((((((triple2) -> rule4)) -> rule3) ((triple2) -> rule4)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2)) ((triple1) -> (rule4 % int3))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3