Anne is furry. Anne is kind. Anne is nice. Anne is red. Anne is not rough. Anne is smart. Anne is young. Harry is kind. Harry is nice. Harry is rough. Harry is smart. Harry is young. If Harry is nice and Harry is not young then Harry is kind. If someone is kind and nice then they are red. If someone is smart then they are nice. If Harry is smart then Harry is red. All rough people are smart. If Harry is not furry then Harry is smart.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is not rough.
("Anne" "is" "rough" "-")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is nice and Harry is not young then Harry is kind.
((("Harry" "is" "nice" "+") ("Harry" "is" "young" "~")) -> ("Harry" "is" "kind" "+"))
If someone is kind and nice then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If Harry is smart then Harry is red.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "red" "+"))
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If Harry is not furry then Harry is smart.
((("Harry" "is" "furry" "~")) -> ("Harry" "is" "smart" "+"))
Anne is kind.
True
1
proof
[(triple2)]
("Anne" "is" "kind" "+")
triple2
Harry is not young.
False
1
inv-proof
[(triple12)]
("Harry" "is" "young" "-")
triple12
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2)] Anne is nice.[(triple3 OR ((triple6) -> rule3))] Anne is not rough.[(triple5)] Anne is red.[(triple4 OR ((triple2 triple3) -> rule2) OR ((triple2 ((triple6) -> rule3)) -> rule2))] Anne is smart.[(triple6)] Anne is young.[(triple7)] Harry is kind.[(triple8)] Harry is nice.[(triple9 OR ((triple11) -> rule3) OR ((((triple10) -> rule5)) -> rule3))] Harry is rough.[(triple10)] Harry is smart.[(triple11 OR ((triple10) -> rule5))] Harry is young.[(triple12)] @1: Harry is red.[(((triple11) -> rule4) OR ((triple8 triple9) -> rule2) OR ((((triple10) -> rule5)) -> rule4) OR ((triple8 ((triple11) -> rule3)) -> rule2) OR ((triple8 ((((triple10) -> rule5)) -> rule3)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple6) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not rough.
("Anne" "is" "rough" "-")
triple5
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple2 triple3) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
((triple11) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
((triple10) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
((triple11) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple8 triple9) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple8 ((triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple8 ((((triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3