Harry is quiet. Harry is red. Harry is rough. If something is red and smart then it is rough. Smart, quiet things are red. If something is nice then it is big. Nice things are quiet. If Harry is big then Harry is red. All quiet, blue things are nice. If something is blue and smart then it is red. Quiet things are blue.
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If something is red and smart then it is rough.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
Smart, quiet things are red.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If Harry is big then Harry is red.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "red" "+"))
All quiet, blue things are nice.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is blue and smart then it is red.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Harry is red.
True
1
proof
[(triple2 OR ((((((triple1 ((triple1) -> rule8)) -> rule6)) -> rule3)) -> rule5))]
("Harry" "is" "red" "+")
triple2
((((((triple1 ((triple1) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is not rough.
False
1
inv-proof
[(triple3)]
("Harry" "is" "rough" "-")
triple3
Harry is blue.
True
2
proof
[(((triple1) -> rule8))]
("Harry" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple1) -> rule8))]
("Harry" "is" "blue" "-")
((triple1) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
True
4
proof
[(((triple1 ((triple1) -> rule8)) -> rule6))]
("Harry" "is" "nice" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not nice.
False
4
inv-proof
[(((triple1 ((triple1) -> rule8)) -> rule6))]
("Harry" "is" "nice" "-")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is big.
True
5
proof
[(((((triple1 ((triple1) -> rule8)) -> rule6)) -> rule3))]
("Harry" "is" "big" "+")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not big.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule8)) -> rule6)) -> rule3))]
("Harry" "is" "big" "-")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
@0: Harry is quiet.[(triple1)] Harry is red.[(triple2 OR ((((((triple1 ((triple1) -> rule8)) -> rule6)) -> rule3)) -> rule5))] Harry is rough.[(triple3)] @1: Harry is blue.[(((triple1) -> rule8))] @2: Harry is nice.[(((triple1 ((triple1) -> rule8)) -> rule6))] @3: Harry is big.[(((((triple1 ((triple1) -> rule8)) -> rule6)) -> rule3))]
Harry is quiet.
("Harry" "is" "quiet" "+")
triple1
Harry is red.
("Harry" "is" "red" "+")
triple2
((((((triple1 ((triple1) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3