Anne is blue. Anne is furry. Anne is green. Anne is rough. Anne is white. Charlie is blue. Charlie is furry. Charlie is green. Charlie is kind. Charlie is rough. Charlie is white. Charlie is young. If Charlie is rough and Charlie is furry then Charlie is kind. If someone is young then they are rough. Green people are rough. If someone is blue and rough then they are kind. If Anne is green and Anne is not kind then Anne is white. If Anne is young and Anne is blue then Anne is white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If Charlie is rough and Charlie is furry then Charlie is kind.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "kind" "+"))
If someone is young then they are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue and rough then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If Anne is green and Anne is not kind then Anne is white.
((("Anne" "is" "green" "+") ("Anne" "is" "kind" "~")) -> ("Anne" "is" "white" "+"))
If Anne is young and Anne is blue then Anne is white.
((("Anne" "is" "young" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "white" "+"))
Anne is furry.
True
1
proof
[(triple2)]
("Anne" "is" "furry" "+")
triple2
Charlie is not green.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "green" "-")
triple8
Anne is kind.
True
3
proof
[(((triple1 triple4) -> rule4) OR ((triple1 ((triple3) -> rule3)) -> rule4))]
("Anne" "is" "kind" "+")
((triple1 triple4) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not kind.
False
3
inv-proof
[(((triple1 triple4) -> rule4) OR ((triple1 ((triple3) -> rule3)) -> rule4))]
("Anne" "is" "kind" "-")
((triple1 triple4) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Anne is green.[(triple3)] Anne is rough.[(triple4 OR ((triple3) -> rule3))] Anne is white.[(triple5)] Charlie is blue.[(triple6)] Charlie is furry.[(triple7)] Charlie is green.[(triple8)] Charlie is kind.[(triple9 OR ((triple10 triple7) -> rule1) OR ((triple6 triple10) -> rule4) OR ((triple6 ((triple12) -> rule2)) -> rule4) OR ((triple6 ((triple8) -> rule3)) -> rule4) OR ((((triple12) -> rule2) triple7) -> rule1) OR ((((triple8) -> rule3) triple7) -> rule1))] Charlie is rough.[(triple10 OR ((triple12) -> rule2) OR ((triple8) -> rule3))] Charlie is white.[(triple11)] Charlie is young.[(triple12)] @1: Anne is kind.[(((triple1 triple4) -> rule4) OR ((triple1 ((triple3) -> rule3)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple3) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
Charlie is kind.
("Charlie" "is" "kind" "+")
triple9
((triple10 triple7) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple6 triple10) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple6 ((triple12) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((triple6 ((triple8) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple12) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple8) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple10
((triple12) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple8) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple11
Charlie is young.
("Charlie" "is" "young" "+")
triple12
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 triple4) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2