Dave is big. Dave is blue. Dave is green. Dave is not nice. Dave is not red. Dave is not rough. Harry is big. Harry is blue. Harry is nice. Harry is red. Harry is rough. Harry is smart. All smart things are red. All big things are green.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is not red.
("Dave" "is" "red" "-")
Dave is not rough.
("Dave" "is" "rough" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
Dave is green.
True
1
proof
[(triple3 OR ((triple1) -> rule2))]
("Dave" "is" "green" "+")
triple3
((triple1) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
False
1
inv-proof
[(triple5)]
("Dave" "is" "red" "+")
triple5
Harry is green.
True
2
proof
[(((triple7) -> rule2))]
("Harry" "is" "green" "+")
((triple7) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple7) -> rule2))]
("Harry" "is" "green" "-")
((triple7) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
@0: Dave is big.[(triple1)] Dave is blue.[(triple2)] Dave is green.[(triple3 OR ((triple1) -> rule2))] Dave is not nice.[(triple4)] Dave is not red.[(triple5)] Dave is not rough.[(triple6)] Harry is big.[(triple7)] Harry is blue.[(triple8)] Harry is nice.[(triple9)] Harry is red.[(triple10 OR ((triple12) -> rule1))] Harry is rough.[(triple11)] Harry is smart.[(triple12)] @1: Harry is green.[(((triple7) -> rule2))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
((triple1) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
triple4
Dave is not red.
("Dave" "is" "red" "-")
triple5
Dave is not rough.
("Dave" "is" "rough" "-")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
((triple12) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
((triple7) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1