Dave is cold. Dave is kind. Dave is nice. Dave is red. Dave is round. Dave is smart. Dave is young. Harry is cold. Harry is kind. Harry is nice. Harry is red. Harry is round. Harry is smart. Harry is young. If Harry is round then Harry is nice. If Dave is cold and Dave is young then Dave is red. All nice things are smart.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is round then Harry is nice.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "nice" "+"))
If Dave is cold and Dave is young then Dave is red.
((("Dave" "is" "cold" "+") ("Dave" "is" "young" "+")) -> ("Dave" "is" "red" "+"))
All nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Dave is red.
True
1
proof
[(triple4 OR ((triple1 triple7) -> rule2))]
("Dave" "is" "red" "+")
triple4
((triple1 triple7) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is not nice.
False
1
inv-proof
[(triple10 OR ((triple12) -> rule1))]
("Harry" "is" "nice" "-")
triple10
((triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
@0: Dave is cold.[(triple1)] Dave is kind.[(triple2)] Dave is nice.[(triple3)] Dave is red.[(triple4 OR ((triple1 triple7) -> rule2))] Dave is round.[(triple5)] Dave is smart.[(triple6 OR ((triple3) -> rule3))] Dave is young.[(triple7)] Harry is cold.[(triple8)] Harry is kind.[(triple9)] Harry is nice.[(triple10 OR ((triple12) -> rule1))] Harry is red.[(triple11)] Harry is round.[(triple12)] Harry is smart.[(triple13 OR ((triple10) -> rule3) OR ((((triple12) -> rule1)) -> rule3))] Harry is young.[(triple14)]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
((triple1 triple7) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
((triple3) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Harry is smart.
("Harry" "is" "smart" "+")
triple13
((triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple14