Harry is big. Harry is blue. Harry is cold. Harry is furry. Harry is quiet. Harry is rough. Harry is round. All big things are quiet. If something is quiet and blue then it is rough. Blue things are big. Blue things are furry. If something is quiet then it is rough. All rough, big things are quiet. If something is cold and blue then it is rough. Furry, round things are quiet.
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and blue then it is rough.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All rough, big things are quiet.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is cold and blue then it is rough.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Furry, round things are quiet.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Harry is big.
True
1
proof
[(triple1 OR ((triple2) -> rule3))]
("Harry" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not round.
False
1
inv-proof
[(triple7)]
("Harry" "is" "round" "-")
triple7
@0: Harry is big.[(triple1 OR ((triple2) -> rule3))] Harry is blue.[(triple2)] Harry is cold.[(triple3)] Harry is furry.[(triple4 OR ((triple2) -> rule4))] Harry is quiet.[(triple5 OR ((triple1) -> rule1) OR ((triple4 triple7) -> rule8) OR ((triple6 triple1) -> rule6) OR ((((triple2) -> rule3)) -> rule1) OR ((triple6 ((triple2) -> rule3)) -> rule6) OR ((((triple2) -> rule4) triple7) -> rule8) OR ((((triple3 triple2) -> rule7) triple1) -> rule6) OR ((((triple3 triple2) -> rule7) ((triple2) -> rule3)) -> rule6))] Harry is rough.[(triple6 OR ((triple5) -> rule5) OR ((triple3 triple2) -> rule7) OR ((triple5 triple2) -> rule2) OR ((((triple1) -> rule1)) -> rule5) OR ((((triple4 triple7) -> rule8)) -> rule5) OR ((((triple1) -> rule1) triple2) -> rule2) OR ((((triple4 triple7) -> rule8) triple2) -> rule2) OR ((((((triple2) -> rule3)) -> rule1)) -> rule5) OR ((((((triple2) -> rule4) triple7) -> rule8)) -> rule5) OR ((((((triple2) -> rule3)) -> rule1) triple2) -> rule2) OR ((((((triple2) -> rule4) triple7) -> rule8) triple2) -> rule2))] Harry is round.[(triple7)]
Harry is big.
("Harry" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
((triple2) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
((triple1) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple4 triple7) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple6 triple1) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((triple6 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple2) -> (rule4 % int2)) triple7) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple3 triple2) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple3 triple2) -> (rule7 % int3)) ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
triple6
((triple5) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple3 triple2) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple5 triple2) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple4 triple7) -> (rule8 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple1) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple4 triple7) -> (rule8 % int2)) triple2) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((((triple2) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((((triple2) -> (rule4 % int3)) triple7) -> (rule8 % int2)) triple2) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
triple7