Anne is blue. Erin is cold. Fiona is not kind. Harry is young. Blue people are not young. All cold people are furry. If Harry is cold then Harry is furry. Nice, blue people are cold. Nice people are not kind. If someone is cold and nice then they are not kind. If someone is nice and young then they are blue. All cold people are nice.
Anne is blue.
("Anne" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Harry is young.
("Harry" "is" "young" "+")
Blue people are not young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "-"))
All cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If Harry is cold then Harry is furry.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "furry" "+"))
Nice, blue people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Nice people are not kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "-"))
If someone is cold and nice then they are not kind.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "-"))
If someone is nice and young then they are blue.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
All cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Erin is not cold.
False
1
inv-proof
[(triple2)]
("Erin" "is" "cold" "-")
triple2
Erin is furry.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple2) -> rule8))]
("Erin" "is" "nice" "-")
((triple2) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not kind.
True
3
proof
[(((((triple2) -> rule8)) -> rule5) OR ((triple2 ((triple2) -> rule8)) -> rule6))]
("Erin" "is" "kind" "-")
((((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple2 ((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule5) OR ((triple2 ((triple2) -> rule8)) -> rule6))]
("Erin" "is" "kind" "+")
((((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple2 ((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Harry" "is" "cold" "-")
Anne is cold.
Unknown
rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Anne" "is" "cold" "+")
Fiona is not furry.
Unknown
inv-rconc
[@3: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule8 <- FAIL)]]
("Fiona" "is" "furry" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Anne is blue.[(triple1)] Erin is cold.[(triple2)] Fiona is not kind.[(triple3)] Harry is young.[(triple4)] @1: Anne is not young.[(((triple1) -> rule1))] Erin is furry.[(((triple2) -> rule2))] Erin is nice.[(((triple2) -> rule8))] @2: Erin is not kind.[(((((triple2) -> rule8)) -> rule5) OR ((triple2 ((triple2) -> rule8)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Anne is not young.
("Anne" "is" "young" "-")
((triple1) -> (rule1 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple2) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not kind.
("Erin" "is" "kind" "-")
((((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple2 ((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2