Erin is green. Harry is nice. All blue, kind people are green. If someone is nice then they are kind. If someone is kind and nice then they are green.
Erin is green.
("Erin" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All blue, kind people are green.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is nice then they are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind and nice then they are green.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Harry is nice.
True
1
proof
[(triple2)]
("Harry" "is" "nice" "+")
triple2
Erin is not green.
False
1
inv-proof
[(triple1)]
("Erin" "is" "green" "-")
triple1
Harry is kind.
True
2
proof
[(((triple2) -> rule2))]
("Harry" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple2) -> rule2))]
("Harry" "is" "kind" "-")
((triple2) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
True
4
proof
[(((((triple2) -> rule2) triple2) -> rule3))]
("Harry" "is" "green" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not green.
False
4
inv-proof
[(((((triple2) -> rule2) triple2) -> rule3))]
("Harry" "is" "green" "-")
((((triple2) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "kind" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Erin is green.[(triple1)] Harry is nice.[(triple2)] @1: Harry is kind.[(((triple2) -> rule2))] @2: Harry is green.[(((((triple2) -> rule2) triple2) -> rule3))]
Erin is green.
("Erin" "is" "green" "+")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2