Anne is big. Anne is blue. Anne is kind. Anne is round. Anne is smart. Anne is white. Anne is young. Harry is big. Harry is blue. Harry is kind. Harry is round. Harry is smart. Harry is white. Harry is young. If someone is white then they are kind.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is white then they are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Harry is kind.
True
1
proof
[(triple10 OR ((triple13) -> rule1))]
("Harry" "is" "kind" "+")
triple10
((triple13) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not smart.
False
1
inv-proof
[(triple12)]
("Harry" "is" "smart" "-")
triple12
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is kind.[(triple3 OR ((triple6) -> rule1))] Anne is round.[(triple4)] Anne is smart.[(triple5)] Anne is white.[(triple6)] Anne is young.[(triple7)] Harry is big.[(triple8)] Harry is blue.[(triple9)] Harry is kind.[(triple10 OR ((triple13) -> rule1))] Harry is round.[(triple11)] Harry is smart.[(triple12)] Harry is white.[(triple13)] Harry is young.[(triple14)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple6) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
((triple13) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Harry is white.
("Harry" "is" "white" "+")
triple13
Harry is young.
("Harry" "is" "young" "+")
triple14