Erin is furry. Harry is red. If someone is quiet and red then they are kind. If someone is white then they are not cold. If Erin is white then Erin is not furry. If Harry is red then Harry is white. If Harry is kind then Harry is red. All quiet people are white. Furry, cold people are red. Red people are furry.
Erin is furry.
("Erin" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
If someone is quiet and red then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If someone is white then they are not cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "-"))
If Erin is white then Erin is not furry.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "furry" "-"))
If Harry is red then Harry is white.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "white" "+"))
If Harry is kind then Harry is red.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "red" "+"))
All quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Furry, cold people are red.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Harry is red.
True
1
proof
[(triple2)]
("Harry" "is" "red" "+")
triple2
Erin is not furry.
False
1
inv-proof
[(triple1)]
("Erin" "is" "furry" "-")
triple1
Harry is white.
True
2
proof
[(((triple2) -> rule4))]
("Harry" "is" "white" "+")
((triple2) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple2) -> rule8))]
("Harry" "is" "furry" "-")
((triple2) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not cold.
True
3
proof
[(((((triple2) -> rule4)) -> rule2))]
("Harry" "is" "cold" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("Harry" "is" "cold" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "kind" "-")
Erin is red.
Unknown
rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "red" "+")
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "white" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Erin is furry.[(triple1)] Harry is red.[(triple2)] @1: Harry is furry.[(((triple2) -> rule8))] Harry is white.[(((triple2) -> rule4))] @2: Harry is not cold.[(((((triple2) -> rule4)) -> rule2))]
Erin is furry.
("Erin" "is" "furry" "+")
triple1
Harry is red.
("Harry" "is" "red" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
((triple2) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple2) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2