Bob is big. Bob is blue. Bob is cold. Bob is kind. Bob is rough. Bob is smart. Bob is white. Harry is big. Harry is blue. Harry is cold. Harry is kind. Harry is rough. Harry is smart. Harry is white. Big things are kind. Kind, cold things are rough. If something is big then it is rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Kind, cold things are rough.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is big then it is rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Harry is kind.
True
1
proof
[(triple11 OR ((triple8) -> rule1))]
("Harry" "is" "kind" "+")
triple11
((triple8) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Bob is not kind.
False
1
inv-proof
[(triple4 OR ((triple1) -> rule1))]
("Bob" "is" "kind" "-")
triple4
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is cold.[(triple3)] Bob is kind.[(triple4 OR ((triple1) -> rule1))] Bob is rough.[(triple5 OR ((triple1) -> rule3) OR ((triple4 triple3) -> rule2) OR ((((triple1) -> rule1) triple3) -> rule2))] Bob is smart.[(triple6)] Bob is white.[(triple7)] Harry is big.[(triple8)] Harry is blue.[(triple9)] Harry is cold.[(triple10)] Harry is kind.[(triple11 OR ((triple8) -> rule1))] Harry is rough.[(triple12 OR ((triple8) -> rule3) OR ((triple11 triple10) -> rule2) OR ((((triple8) -> rule1) triple10) -> rule2))] Harry is smart.[(triple13)] Harry is white.[(triple14)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple4 triple3) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
((triple8) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple12
((triple8) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple11 triple10) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple8) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14