Harry is big. Harry is cold. Harry is young. If something is young then it is not white. If Harry is red and Harry is white then Harry is young. If Harry is kind and Harry is red then Harry is not big. Big, white things are rough. Kind things are not rough. Cold, white things are rough. If something is cold and not young then it is big. All young, big things are kind.
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is young then it is not white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "-"))
If Harry is red and Harry is white then Harry is young.
((("Harry" "is" "red" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "young" "+"))
If Harry is kind and Harry is red then Harry is not big.
((("Harry" "is" "kind" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "big" "-"))
Big, white things are rough.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
Kind things are not rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "-"))
Cold, white things are rough.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is cold and not young then it is big.
((("something" "is" "cold" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "+"))
All young, big things are kind.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Harry is young.
True
1
proof
[(triple3)]
("Harry" "is" "young" "+")
triple3
Harry is not young.
False
1
inv-proof
[(triple3)]
("Harry" "is" "young" "-")
triple3
Harry is kind.
True
3
proof
[(((triple3 triple1) -> rule8))]
("Harry" "is" "kind" "+")
((triple3 triple1) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "white" "+")
((triple3) -> (rule1 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is not rough.
True
4
proof
[(((((triple3 triple1) -> rule8)) -> rule5))]
("Harry" "is" "rough" "-")
((((triple3 triple1) -> (rule8 % int2))) -> (rule5 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
False
4
inv-proof
[(((((triple3 triple1) -> rule8)) -> rule5))]
("Harry" "is" "rough" "+")
((((triple3 triple1) -> (rule8 % int2))) -> (rule5 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
@0: Harry is big.[(triple1)] Harry is cold.[(triple2)] Harry is young.[(triple3)] @1: Harry is kind.[(((triple3 triple1) -> rule8))] Harry is not white.[(((triple3) -> rule1))] @2: Harry is not rough.[(((((triple3 triple1) -> rule8)) -> rule5))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
((triple3 triple1) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
((triple3) -> (rule1 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is not rough.
("Harry" "is" "rough" "-")
((((triple3 triple1) -> (rule8 % int2))) -> (rule5 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2