Anne is kind. Anne is rough. Charlie is blue. Charlie is furry. Charlie is kind. Charlie is nice. Charlie is rough. Erin is nice. Erin is rough. Erin is young. Harry is nice. Harry is young. All young people are white. Nice people are furry. If Erin is kind and Erin is rough then Erin is nice. Rough, nice people are kind. Young people are kind. All blue people are furry.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
All young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If Erin is kind and Erin is rough then Erin is nice.
((("Erin" "is" "kind" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "nice" "+"))
Rough, nice people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
All blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Charlie is furry.
True
1
proof
[(triple4 OR ((triple3) -> rule6) OR ((triple6) -> rule2))]
("Charlie" "is" "furry" "+")
triple4
((triple3) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not rough.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "rough" "-")
triple7
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is kind.[(triple1)] Anne is rough.[(triple2)] Charlie is blue.[(triple3)] Charlie is furry.[(triple4 OR ((triple3) -> rule6) OR ((triple6) -> rule2))] Charlie is kind.[(triple5 OR ((triple7 triple6) -> rule4))] Charlie is nice.[(triple6)] Charlie is rough.[(triple7)] Erin is nice.[(triple8 OR ((((triple10) -> rule5) triple9) -> rule3))] Erin is rough.[(triple9)] Erin is young.[(triple10)] Harry is nice.[(triple11)] Harry is young.[(triple12)] @1: Erin is furry.[(((triple8) -> rule2) OR ((((((triple10) -> rule5) triple9) -> rule3)) -> rule2))] Erin is kind.[(((triple10) -> rule5) OR ((triple9 triple8) -> rule4))] Erin is white.[(((triple10) -> rule1))] Harry is furry.[(((triple11) -> rule2))] Harry is kind.[(((triple12) -> rule5))] Harry is white.[(((triple12) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
((triple3) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
((triple7 triple6) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
((((triple10) -> (rule5 % int2)) triple9) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Erin is furry.
("Erin" "is" "furry" "+")
((triple8) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((((triple10) -> (rule5 % int3)) triple9) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((triple10) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple9 triple8) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple10) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple11) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple12) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple12) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1