Anne is furry. Erin is young. All red, cold things are white. All smart things are red. Green, white things are red. All young things are smart. If something is furry then it is green. If something is cold and red then it is young. All furry, young things are smart. If something is green then it is cold.
Anne is furry.
("Anne" "is" "furry" "+")
Erin is young.
("Erin" "is" "young" "+")
All red, cold things are white.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Green, white things are red.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is furry then it is green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is cold and red then it is young.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All furry, young things are smart.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Erin is not young.
False
1
inv-proof
[(triple2)]
("Erin" "is" "young" "-")
triple2
Erin is smart.
True
2
proof
[(((triple2) -> rule4))]
("Erin" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "green" "-")
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Erin is red.
True
3
proof
[(((((triple2) -> rule4)) -> rule2))]
("Erin" "is" "red" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule8))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not red.
Unknown
inv-rconc
[@5: Anne is red.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule6 <- rule3 <- rule1 <- FAIL)]]
("Anne" "is" "red" "-")
Erin is cold.
Unknown
rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Erin" "is" "cold" "+")
Anne is not white.
Unknown
inv-rconc
[@5: Anne is white.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule4 <- rule6 <- rule3 <- FAIL)]]
("Anne" "is" "white" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Erin is young.[(triple2)] @1: Anne is green.[(((triple1) -> rule5))] Erin is smart.[(((triple2) -> rule4))] @2: Anne is cold.[(((((triple1) -> rule5)) -> rule8))] Erin is red.[(((((triple2) -> rule4)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2