Harry is big. Harry is blue. Harry is furry. If something is big and rough then it is furry. If something is furry and big then it is round. All big, smart things are blue. All furry things are rough. Rough, smart things are green. If Harry is furry and Harry is rough then Harry is green. Rough things are blue. If Harry is big and Harry is round then Harry is rough.
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If something is big and rough then it is furry.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
If something is furry and big then it is round.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All big, smart things are blue.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
Rough, smart things are green.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If Harry is furry and Harry is rough then Harry is green.
((("Harry" "is" "furry" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "green" "+"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If Harry is big and Harry is round then Harry is rough.
((("Harry" "is" "big" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "rough" "+"))
Harry is big.
True
1
proof
[(triple1)]
("Harry" "is" "big" "+")
triple1
Harry is not furry.
False
1
inv-proof
[(triple3)]
("Harry" "is" "furry" "-")
triple3
Harry is round.
True
3
proof
[(((triple3 triple1) -> rule2))]
("Harry" "is" "round" "+")
((triple3 triple1) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
3
inv-proof
[(((triple3 triple1) -> rule2))]
("Harry" "is" "round" "-")
((triple3 triple1) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
True
4
proof
[(((triple3 ((triple3) -> rule4)) -> rule6) OR ((triple3 ((triple1 ((triple3 triple1) -> rule2)) -> rule8)) -> rule6))]
("Harry" "is" "green" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple3 ((triple1 ((triple3 triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not green.
False
4
inv-proof
[(((triple3 ((triple3) -> rule4)) -> rule6) OR ((triple3 ((triple1 ((triple3 triple1) -> rule2)) -> rule8)) -> rule6))]
("Harry" "is" "green" "-")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple3 ((triple1 ((triple3 triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
@0: Harry is big.[(triple1)] Harry is blue.[(triple2 OR ((((triple3) -> rule4)) -> rule7) OR ((((triple1 ((triple3 triple1) -> rule2)) -> rule8)) -> rule7))] Harry is furry.[(triple3)] @1: Harry is rough.[(((triple3) -> rule4) OR ((triple1 ((triple3 triple1) -> rule2)) -> rule8))] Harry is round.[(((triple3 triple1) -> rule2))] @2: Harry is green.[(((triple3 ((triple3) -> rule4)) -> rule6) OR ((triple3 ((triple1 ((triple3 triple1) -> rule2)) -> rule8)) -> rule6))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
((((triple3) -> (rule4 % int2))) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple1 ((triple3 triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple1 ((triple3 triple1) -> (rule2 % int2))) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple3 triple1) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple3 ((triple1 ((triple3 triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3