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