Bob is big. Bob is cold. Bob is furry. Bob is green. Bob is kind. Bob is young. Harry is big. Harry is cold. Harry is furry. Harry is not green. Harry is kind. Harry is rough. If Bob is not kind then Bob is cold. If something is green and not kind then it is furry. If Bob is kind then Bob is green. If something is young and furry then it is green. If something is big and not furry then it is rough. If something is young then it is rough. Young, kind things are rough. If something is big and not young then it is rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is young.
("Bob" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Bob is not kind then Bob is cold.
((("Bob" "is" "kind" "~")) -> ("Bob" "is" "cold" "+"))
If something is green and not kind then it is furry.
((("something" "is" "green" "+") ("something" "is" "kind" "~")) -> ("something" "is" "furry" "+"))
If Bob is kind then Bob is green.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "green" "+"))
If something is young and furry then it is green.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is big and not furry then it is rough.
((("something" "is" "big" "+") ("something" "is" "furry" "~")) -> ("something" "is" "rough" "+"))
If something is young then it is rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Young, kind things are rough.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is big and not young then it is rough.
((("something" "is" "big" "+") ("something" "is" "young" "~")) -> ("something" "is" "rough" "+"))
Harry is big.
True
1
proof
[(triple7)]
("Harry" "is" "big" "+")
triple7
Bob is not green.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule3) OR ((triple6 triple3) -> rule4))]
("Bob" "is" "green" "-")
triple4
((triple5) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple6 triple3) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
True
2
proof
[(((triple6) -> rule6) OR ((triple6 triple5) -> rule7))]
("Bob" "is" "rough" "+")
((triple6) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple6 triple5) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple6) -> rule6) OR ((triple6 triple5) -> rule7))]
("Bob" "is" "rough" "-")
((triple6) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple6 triple5) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is furry.[(triple3)] Bob is green.[(triple4 OR ((triple5) -> rule3) OR ((triple6 triple3) -> rule4))] Bob is kind.[(triple5)] Bob is young.[(triple6)] Harry is big.[(triple7)] Harry is cold.[(triple8)] Harry is furry.[(triple9)] Harry is kind.[(triple11)] Harry is not green.[(triple10)] Harry is rough.[(triple12)] @1: Bob is rough.[(((triple6) -> rule6) OR ((triple6 triple5) -> rule7))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
((triple5) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple6 triple3) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is not green.
("Harry" "is" "green" "-")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Bob is rough.
("Bob" "is" "rough" "+")
((triple6) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple6 triple5) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1