Anne is big. Anne is blue. Anne is green. Anne is kind. Anne is nice. Anne is quiet. Anne is young. Charlie is big. Charlie is blue. Charlie is green. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is young. All nice people are kind. If someone is quiet then they are young. If someone is kind and big then they are quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and big then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Anne is blue.
True
1
proof
[(triple2)]
("Anne" "is" "blue" "+")
triple2
Anne is not kind.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule1))]
("Anne" "is" "kind" "-")
triple4
((triple5) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is green.[(triple3)] Anne is kind.[(triple4 OR ((triple5) -> rule1))] Anne is nice.[(triple5)] Anne is quiet.[(triple6 OR ((triple4 triple1) -> rule3) OR ((((triple5) -> rule1) triple1) -> rule3))] Anne is young.[(triple7 OR ((triple6) -> rule2) OR ((((triple4 triple1) -> rule3)) -> rule2) OR ((((((triple5) -> rule1) triple1) -> rule3)) -> rule2))] Charlie is big.[(triple8)] Charlie is blue.[(triple9)] Charlie is green.[(triple10)] Charlie is kind.[(triple11 OR ((triple12) -> rule1))] Charlie is nice.[(triple12)] Charlie is quiet.[(triple13 OR ((triple11 triple8) -> rule3) OR ((((triple12) -> rule1) triple8) -> rule3))] Charlie is young.[(triple14 OR ((triple13) -> rule2) OR ((((triple11 triple8) -> rule3)) -> rule2) OR ((((((triple12) -> rule1) triple8) -> rule3)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
((triple5) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple5
Anne is quiet.
("Anne" "is" "quiet" "+")
triple6
((triple4 triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple5) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple6) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple4 triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((((triple5) -> (rule1 % int3)) triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
triple8
Charlie is blue.
("Charlie" "is" "blue" "+")
triple9
Charlie is green.
("Charlie" "is" "green" "+")
triple10
Charlie is kind.
("Charlie" "is" "kind" "+")
triple11
((triple12) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple12
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple13
((triple11 triple8) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple12) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple14
((triple13) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple11 triple8) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((((triple12) -> (rule1 % int3)) triple8) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3