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