Erin is green. Harry is blue. If Erin is green and Erin is young then Erin is blue. Big things are green. All blue things are green. Quiet things are kind. Young things are green. If Erin is young and Erin is green then Erin is big. All quiet things are green. Kind things are young.
Erin is green.
("Erin" "is" "green" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If Erin is green and Erin is young then Erin is blue.
((("Erin" "is" "green" "+") ("Erin" "is" "young" "+")) -> ("Erin" "is" "blue" "+"))
Big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If Erin is young and Erin is green then Erin is big.
((("Erin" "is" "young" "+") ("Erin" "is" "green" "+")) -> ("Erin" "is" "big" "+"))
All quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Erin is green.
True
1
proof
[(triple1)]
("Erin" "is" "green" "+")
triple1
Erin is not green.
False
1
inv-proof
[(triple1)]
("Erin" "is" "green" "-")
triple1
Harry is green.
True
2
proof
[(((triple2) -> rule3))]
("Harry" "is" "green" "+")
((triple2) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple2) -> rule3))]
("Harry" "is" "green" "-")
((triple2) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "kind" "-")
Harry is young.
Unknown
rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Erin is green.[(triple1)] Harry is blue.[(triple2)] @1: Harry is green.[(((triple2) -> rule3))]
Erin is green.
("Erin" "is" "green" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
((triple2) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1