Dave is big. Dave is cold. Dave is furry. Dave is kind. Dave is nice. Dave is red. Dave is not rough. Harry is big. Harry is cold. Harry is furry. Harry is kind. Harry is nice. Harry is red. Harry is rough. If someone is kind then they are big.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Dave is cold.
True
1
proof
[(triple2)]
("Dave" "is" "cold" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple9)]
("Harry" "is" "cold" "-")
triple9
@0: Dave is big.[(triple1 OR ((triple4) -> rule1))] Dave is cold.[(triple2)] Dave is furry.[(triple3)] Dave is kind.[(triple4)] Dave is nice.[(triple5)] Dave is not rough.[(triple7)] Dave is red.[(triple6)] Harry is big.[(triple8 OR ((triple11) -> rule1))] Harry is cold.[(triple9)] Harry is furry.[(triple10)] Harry is kind.[(triple11)] Harry is nice.[(triple12)] Harry is red.[(triple13)] Harry is rough.[(triple14)]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple4) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is not rough.
("Dave" "is" "rough" "-")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple11) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is nice.
("Harry" "is" "nice" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14