Anne is cold. Erin is big. Erin is furry. Erin is red. Harry is furry. Harry is kind. Harry is not red. All kind people are furry. All green people are kind. All cold people are kind. If someone is big then they are green. If someone is big and not green then they are not red. Kind, red people are quiet.
Anne is cold.
("Anne" "is" "cold" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not red.
("Harry" "is" "red" "-")
All kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
All green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is big then they are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is big and not green then they are not red.
((("someone" "is" "big" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "red" "-"))
Kind, red people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Erin is red.
True
1
proof
[(triple4)]
("Erin" "is" "red" "+")
triple4
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is kind.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple2) -> rule4))]
("Erin" "is" "green" "-")
((triple2) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Anne is furry.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Erin is not kind.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("Erin" "is" "kind" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
True
5
proof
[(((((((triple2) -> rule4)) -> rule2) triple4) -> rule6))]
("Erin" "is" "quiet" "+")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not quiet.
False
5
inv-proof
[(((((((triple2) -> rule4)) -> rule2) triple4) -> rule6))]
("Erin" "is" "quiet" "-")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "green" "+")
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "green" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Anne is cold.[(triple1)] Erin is big.[(triple2)] Erin is furry.[(triple3 OR ((((((triple2) -> rule4)) -> rule2)) -> rule1))] Erin is red.[(triple4)] Harry is furry.[(triple5 OR ((triple6) -> rule1))] Harry is kind.[(triple6)] Harry is not red.[(triple7)] @1: Anne is kind.[(((triple1) -> rule3))] Erin is green.[(((triple2) -> rule4))] @2: Anne is furry.[(((((triple1) -> rule3)) -> rule1))] Erin is kind.[(((((triple2) -> rule4)) -> rule2))] @3: Erin is quiet.[(((((((triple2) -> rule4)) -> rule2) triple4) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
triple5
((triple6) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is not red.
("Harry" "is" "red" "-")
triple7
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple2) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3