Harry is cold. All blue things are red. All blue, cold things are smart. Blue things are rough. If Harry is kind then Harry is rough. If something is rough then it is blue. If something is cold then it is kind.
Harry is cold.
("Harry" "is" "cold" "+")
All blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
All blue, cold things are smart.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If Harry is kind then Harry is rough.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "rough" "+"))
If something is rough then it is blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Harry is cold.
True
1
proof
[(triple1)]
("Harry" "is" "cold" "+")
triple1
Harry is not cold.
False
1
inv-proof
[(triple1)]
("Harry" "is" "cold" "-")
triple1
Harry is kind.
True
2
proof
[(((triple1) -> rule6))]
("Harry" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple1) -> rule6))]
("Harry" "is" "kind" "-")
((triple1) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
True
3
proof
[(((((triple1) -> rule6)) -> rule4))]
("Harry" "is" "rough" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule4))]
("Harry" "is" "rough" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
@0: Harry is cold.[(triple1)] @1: Harry is kind.[(((triple1) -> rule6))] @2: Harry is rough.[(((((triple1) -> rule6)) -> rule4))] @3: Harry is blue.[(((((((triple1) -> rule6)) -> rule4)) -> rule5))] @4: Harry is red.[(((((((((triple1) -> rule6)) -> rule4)) -> rule5)) -> rule1))] Harry is smart.[(((((((((triple1) -> rule6)) -> rule4)) -> rule5) triple1) -> rule2))]
Harry is cold.
("Harry" "is" "cold" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((((((triple1) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
((((((((triple1) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4