Harry is quiet. If Harry is nice then Harry is smart. All rough things are kind. If something is rough and smart then it is cold. All nice things are quiet. If something is quiet then it is nice. All quiet things are rough. If something is nice then it is rough. If something is kind then it is cold.
Harry is quiet.
("Harry" "is" "quiet" "+")
If Harry is nice then Harry is smart.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "smart" "+"))
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is rough and smart then it is cold.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
All quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something is kind then it is cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
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 nice.
True
2
proof
[(((triple1) -> rule5))]
("Harry" "is" "nice" "+")
((triple1) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple1) -> rule6) OR ((((triple1) -> rule5)) -> rule7))]
("Harry" "is" "rough" "-")
((triple1) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is kind.
True
3
proof
[(((((triple1) -> rule6)) -> rule2) OR ((((((triple1) -> rule5)) -> rule7)) -> rule2))]
("Harry" "is" "kind" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is not smart.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("Harry" "is" "smart" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
True
4
proof
[(((((((triple1) -> rule6)) -> rule2)) -> rule8) OR ((((triple1) -> rule6) ((((triple1) -> rule5)) -> rule1)) -> rule3) OR ((((((triple1) -> rule5)) -> rule7) ((((triple1) -> rule5)) -> rule1)) -> rule3) OR ((((((((triple1) -> rule5)) -> rule7)) -> rule2)) -> rule8))]
("Harry" "is" "cold" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple1) -> (rule6 % int4)) ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
((((((triple1) -> (rule5 % int4))) -> (rule7 % int3)) ((((triple1) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is not cold.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule2)) -> rule8) OR ((((triple1) -> rule6) ((((triple1) -> rule5)) -> rule1)) -> rule3) OR ((((((triple1) -> rule5)) -> rule7) ((((triple1) -> rule5)) -> rule1)) -> rule3) OR ((((((((triple1) -> rule5)) -> rule7)) -> rule2)) -> rule8))]
("Harry" "is" "cold" "-")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple1) -> (rule6 % int4)) ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
((((((triple1) -> (rule5 % int4))) -> (rule7 % int3)) ((((triple1) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
@0: Harry is quiet.[(triple1)] @1: Harry is nice.[(((triple1) -> rule5))] Harry is rough.[(((triple1) -> rule6) OR ((((triple1) -> rule5)) -> rule7))] @2: Harry is kind.[(((((triple1) -> rule6)) -> rule2) OR ((((((triple1) -> rule5)) -> rule7)) -> rule2))] Harry is smart.[(((((triple1) -> rule5)) -> rule1))] @3: Harry is cold.[(((((((triple1) -> rule6)) -> rule2)) -> rule8) OR ((((triple1) -> rule6) ((((triple1) -> rule5)) -> rule1)) -> rule3) OR ((((((triple1) -> rule5)) -> rule7) ((((triple1) -> rule5)) -> rule1)) -> rule3) OR ((((((((triple1) -> rule5)) -> rule7)) -> rule2)) -> rule8))]
Harry is quiet.
("Harry" "is" "quiet" "+")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
((triple1) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple1) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple1) -> (rule6 % int4)) ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
((((((triple1) -> (rule5 % int4))) -> (rule7 % int3)) ((((triple1) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4