Harry is quiet. If someone is quiet then they are rough. If Harry is red then Harry is white. If someone is kind and nice then they are white. Rough people are red. Quiet, rough people are cold. If someone is white and quiet then they are red. If someone is nice and cold then they are quiet. If Harry is quiet then Harry is kind.
Harry is quiet.
("Harry" "is" "quiet" "+")
If someone is quiet then they are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If Harry is red then Harry is white.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "white" "+"))
If someone is kind and nice then they are white.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
Rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
Quiet, rough people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is white and quiet then they are red.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If someone is nice and cold then they are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is quiet then Harry is kind.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "kind" "+"))
Harry is quiet.
True
1
proof
[(triple1)]
("Harry" "is" "quiet" "+")
triple1
Harry is not quiet.
False
1
inv-proof
[(triple1)]
("Harry" "is" "quiet" "-")
triple1
Harry is rough.
True
2
proof
[(((triple1) -> rule1))]
("Harry" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("Harry" "is" "rough" "-")
((triple1) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Harry" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule5))]
("Harry" "is" "cold" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
@0: Harry is quiet.[(triple1)] @1: Harry is kind.[(((triple1) -> rule8))] Harry is rough.[(((triple1) -> rule1))] @2: Harry is cold.[(((triple1 ((triple1) -> rule1)) -> rule5))] Harry is red.[(((((triple1) -> rule1)) -> rule4))] @3: Harry is white.[(((((((triple1) -> rule1)) -> rule4)) -> rule2))]
Harry is quiet.
("Harry" "is" "quiet" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
((triple1) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3