Harry is quiet. Harry is not smart. Harry is young. Quiet people are young. Quiet people are green. All quiet people are rough. If someone is big and not green then they are red. If someone is smart and not rough then they are big. If someone is green then they are big.
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Harry is young.
("Harry" "is" "young" "+")
Quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
Quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
All quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If someone is big and not green then they are red.
((("someone" "is" "big" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "red" "+"))
If someone is smart and not rough then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "big" "+"))
If someone is green then they are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Harry is young.
True
1
proof
[(triple3 OR ((triple1) -> rule1))]
("Harry" "is" "young" "+")
triple3
((triple1) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
False
1
inv-proof
[(triple2)]
("Harry" "is" "smart" "+")
triple2
Harry is rough.
True
2
proof
[(((triple1) -> rule3))]
("Harry" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple1) -> rule2))]
("Harry" "is" "green" "-")
((triple1) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("Harry" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not big.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("Harry" "is" "big" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
@0: Harry is not smart.[(triple2)] Harry is quiet.[(triple1)] Harry is young.[(triple3 OR ((triple1) -> rule1))] @1: Harry is green.[(((triple1) -> rule2))] Harry is rough.[(((triple1) -> rule3))] @2: Harry is big.[(((((triple1) -> rule2)) -> rule6))]
Harry is not smart.
("Harry" "is" "smart" "-")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple1
Harry is young.
("Harry" "is" "young" "+")
triple3
((triple1) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple1) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2