Anne is blue. Charlie is green. Erin is kind. Harry is rough. Kind people are green. If someone is young and not green then they are not blue. All rough people are not smart. If someone is kind then they are smart. If someone is green and not blue then they are rough. If someone is rough and not smart then they are furry. All smart, young people are not furry. All green, kind people are furry.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is young and not green then they are not blue.
((("someone" "is" "young" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "blue" "-"))
All rough people are not smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "-"))
If someone is kind then they are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is green and not blue then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "rough" "+"))
If someone is rough and not smart then they are furry.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "furry" "+"))
All smart, young people are not furry.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "-"))
All green, kind people are furry.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Harry is rough.
True
1
proof
[(triple4)]
("Harry" "is" "rough" "+")
triple4
Harry is not rough.
False
1
inv-proof
[(triple4)]
("Harry" "is" "rough" "-")
triple4
Harry is not smart.
True
2
proof
[(((triple4) -> rule3))]
("Harry" "is" "smart" "-")
((triple4) -> (rule3 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Erin is not smart.
False
2
inv-proof
[(((triple3) -> rule4))]
("Erin" "is" "smart" "-")
((triple3) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
True
4
proof
[(((((triple3) -> rule1) triple3) -> rule8))]
("Erin" "is" "furry" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not furry.
False
4
inv-proof
[(((((triple3) -> rule1) triple3) -> rule8))]
("Erin" "is" "furry" "-")
((((triple3) -> (rule1 % int2)) triple3) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "smart" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "furry" "+")
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "green" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is blue.[(triple1)] Charlie is green.[(triple2)] Erin is kind.[(triple3)] Harry is rough.[(triple4)] @1: Erin is green.[(((triple3) -> rule1))] Erin is smart.[(((triple3) -> rule4))] Harry is not smart.[(((triple4) -> rule3))] @2: Erin is furry.[(((((triple3) -> rule1) triple3) -> rule8))] Harry is furry.[(((triple4 ((triple4) -> rule3)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
((triple4) -> (rule3 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
int2