Harry is furry. Harry is quiet. Harry is round. Round things are blue. Round things are green. Furry, red things are green. If something is quiet and round then it is white. Green things are furry. All furry things are red. Green, white things are red. All round things are green.
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Furry, red things are green.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is quiet and round then it is white.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
Green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
All furry things are red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Green, white things are red.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Harry is quiet.
True
1
proof
[(triple2)]
("Harry" "is" "quiet" "+")
triple2
Harry is not quiet.
False
1
inv-proof
[(triple2)]
("Harry" "is" "quiet" "-")
triple2
Harry is white.
True
3
proof
[(((triple2 triple3) -> rule4))]
("Harry" "is" "white" "+")
((triple2 triple3) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple1) -> rule6) OR ((((triple3) -> rule2) ((triple2 triple3) -> rule4)) -> rule7) OR ((((triple3) -> rule8) ((triple2 triple3) -> rule4)) -> rule7) OR ((((((triple3) -> rule2)) -> rule5)) -> rule6) OR ((((((triple3) -> rule8)) -> rule5)) -> rule6))]
("Harry" "is" "red" "-")
((triple1) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple3) -> (rule2 % int3)) ((triple2 triple3) -> (rule4 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((triple3) -> (rule8 % int3)) ((triple2 triple3) -> (rule4 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple3) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
@0: Harry is furry.[(triple1 OR ((((triple3) -> rule2)) -> rule5) OR ((((triple3) -> rule8)) -> rule5))] Harry is quiet.[(triple2)] Harry is round.[(triple3)] @1: Harry is blue.[(((triple3) -> rule1))] Harry is green.[(((triple3) -> rule2) OR ((triple3) -> rule8) OR ((triple1 ((triple1) -> rule6)) -> rule3))] Harry is red.[(((triple1) -> rule6) OR ((((triple3) -> rule2) ((triple2 triple3) -> rule4)) -> rule7) OR ((((triple3) -> rule8) ((triple2 triple3) -> rule4)) -> rule7) OR ((((((triple3) -> rule2)) -> rule5)) -> rule6) OR ((((((triple3) -> rule8)) -> rule5)) -> rule6))] Harry is white.[(((triple2 triple3) -> rule4))]
Harry is furry.
("Harry" "is" "furry" "+")
triple1
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple3) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple3) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple1 ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((triple1) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple3) -> (rule2 % int3)) ((triple2 triple3) -> (rule4 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((triple3) -> (rule8 % int3)) ((triple2 triple3) -> (rule4 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple3) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((triple2 triple3) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1