Harry is big. Harry is nice. Harry is smart. If something is cold and not smart then it is blue. All quiet things are blue. If something is big then it is cold. If Harry is kind and Harry is cold then Harry is nice. If Harry is quiet then Harry is nice. If something is blue then it is kind. If Harry is smart and Harry is nice then Harry is quiet. If something is smart then it is quiet.
Harry is big.
("Harry" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is cold and not smart then it is blue.
((("something" "is" "cold" "+") ("something" "is" "smart" "~")) -> ("something" "is" "blue" "+"))
All quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is big then it is cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Harry is kind and Harry is cold then Harry is nice.
((("Harry" "is" "kind" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "nice" "+"))
If Harry is quiet then Harry is nice.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "nice" "+"))
If something is blue then it is kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If Harry is smart and Harry is nice then Harry is quiet.
((("Harry" "is" "smart" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "quiet" "+"))
If something is smart then it is quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Harry is nice.
True
1
proof
[(triple2 OR ((((triple3) -> rule8)) -> rule5) OR ((((((((triple3) -> rule8)) -> rule2)) -> rule6) ((triple1) -> rule3)) -> rule4))]
("Harry" "is" "nice" "+")
triple2
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((((((triple3) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
Harry is not nice.
False
1
inv-proof
[(triple2 OR ((((triple3) -> rule8)) -> rule5) OR ((((((((triple3) -> rule8)) -> rule2)) -> rule6) ((triple1) -> rule3)) -> rule4))]
("Harry" "is" "nice" "-")
triple2
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((((((triple3) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
Harry is quiet.
True
2
proof
[(((triple3) -> rule8) OR ((triple3 triple2) -> rule7))]
("Harry" "is" "quiet" "+")
((triple3) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple3 triple2) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Harry" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
True
3
proof
[(((((triple3) -> rule8)) -> rule2) OR ((((triple3 triple2) -> rule7)) -> rule2))]
("Harry" "is" "blue" "+")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple3 triple2) -> (rule7 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not blue.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule2) OR ((((triple3 triple2) -> rule7)) -> rule2))]
("Harry" "is" "blue" "-")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple3 triple2) -> (rule7 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
True
4
proof
[(((((((triple3) -> rule8)) -> rule2)) -> rule6) OR ((((((triple3 triple2) -> rule7)) -> rule2)) -> rule6))]
("Harry" "is" "kind" "+")
((((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple3 triple2) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not kind.
False
4
inv-proof
[(((((((triple3) -> rule8)) -> rule2)) -> rule6) OR ((((((triple3 triple2) -> rule7)) -> rule2)) -> rule6))]
("Harry" "is" "kind" "-")
((((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple3 triple2) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
@0: Harry is big.[(triple1)] Harry is nice.[(triple2 OR ((((triple3) -> rule8)) -> rule5) OR ((((((((triple3) -> rule8)) -> rule2)) -> rule6) ((triple1) -> rule3)) -> rule4))] Harry is smart.[(triple3)] @1: Harry is cold.[(((triple1) -> rule3))] Harry is quiet.[(((triple3) -> rule8) OR ((triple3 triple2) -> rule7))] @2: Harry is blue.[(((((triple3) -> rule8)) -> rule2) OR ((((triple3 triple2) -> rule7)) -> rule2))] @3: Harry is kind.[(((((((triple3) -> rule8)) -> rule2)) -> rule6) OR ((((((triple3 triple2) -> rule7)) -> rule2)) -> rule6))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
triple2
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((((((triple3) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple3 triple2) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple3 triple2) -> (rule7 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple3 triple2) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3