Harry is cold. Harry is kind. Harry is young. All kind people are quiet. If someone is quiet then they are rough. If someone is green and not young then they are cold. Young, rough people are not green. If someone is rough and not kind then they are green. If Harry is young and Harry is not kind then Harry is big. If someone is quiet and not green then they are big. If someone is young and not green then they are big.
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
All kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet then they are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If someone is green and not young then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "cold" "+"))
Young, rough people are not green.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "-"))
If someone is rough and not kind then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "green" "+"))
If Harry is young and Harry is not kind then Harry is big.
((("Harry" "is" "young" "+") ("Harry" "is" "kind" "~")) -> ("Harry" "is" "big" "+"))
If someone is quiet and not green then they are big.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "big" "+"))
If someone is young and not green then they are big.
((("someone" "is" "young" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "big" "+"))
Harry is kind.
True
1
proof
[(triple2)]
("Harry" "is" "kind" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple1)]
("Harry" "is" "cold" "-")
triple1
Harry is quiet.
True
2
proof
[(((triple2) -> rule1))]
("Harry" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple2) -> rule1))]
("Harry" "is" "quiet" "-")
((triple2) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("Harry" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("Harry" "is" "rough" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not green.
True
5
proof
[(((triple3 ((((triple2) -> rule1)) -> rule2)) -> rule4))]
("Harry" "is" "green" "-")
((triple3 ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is green.
False
5
inv-proof
[(((triple3 ((((triple2) -> rule1)) -> rule2)) -> rule4))]
("Harry" "is" "green" "+")
((triple3 ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
@0: Harry is cold.[(triple1)] Harry is kind.[(triple2)] Harry is young.[(triple3)] @1: Harry is quiet.[(((triple2) -> rule1))] @2: Harry is rough.[(((((triple2) -> rule1)) -> rule2))] @3: Harry is not green.[(((triple3 ((((triple2) -> rule1)) -> rule2)) -> rule4))] @4: Harry is big.[(((triple3 ((triple3 ((((triple2) -> rule1)) -> rule2)) -> rule4)) -> rule8) OR ((((triple2) -> rule1) ((triple3 ((((triple2) -> rule1)) -> rule2)) -> rule4)) -> rule7))]
Harry is cold.
("Harry" "is" "cold" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not green.
("Harry" "is" "green" "-")
((triple3 ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((triple3 ((triple3 ((((triple2) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not green.
("Harry" "is" "green" "-")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
((((triple2) -> (rule1 % int4)) ((triple3 ((((triple2) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not green.
("Harry" "is" "green" "-")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4