Harry is big. Harry is blue. Harry is green. Harry is nice. Harry is quiet. Harry is not rough. Harry is round. If someone is green and big then they are blue. If someone is rough and green then they are big. All rough people are nice. If Harry is nice and Harry is not big then Harry is blue. If someone is green and not big then they are round. Blue people are quiet. Nice, blue people are quiet. If someone is rough and not green then they are quiet.
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is round.
("Harry" "is" "round" "+")
If someone is green and big then they are blue.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough and green then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
All rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If Harry is nice and Harry is not big then Harry is blue.
((("Harry" "is" "nice" "+") ("Harry" "is" "big" "~")) -> ("Harry" "is" "blue" "+"))
If someone is green and not big then they are round.
((("someone" "is" "green" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "round" "+"))
Blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
Nice, blue people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is rough and not green then they are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "quiet" "+"))
Harry is not rough.
True
1
proof
[(triple6)]
("Harry" "is" "rough" "-")
triple6
Harry is rough.
False
1
inv-proof
[(triple6)]
("Harry" "is" "rough" "+")
triple6
@0: Harry is big.[(triple1)] Harry is blue.[(triple2 OR ((triple3 triple1) -> rule1))] Harry is green.[(triple3)] Harry is nice.[(triple4)] Harry is not rough.[(triple6)] Harry is quiet.[(triple5 OR ((triple2) -> rule6) OR ((triple4 triple2) -> rule7) OR ((((triple3 triple1) -> rule1)) -> rule6) OR ((triple4 ((triple3 triple1) -> rule1)) -> rule7))] Harry is round.[(triple7)]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
((triple3 triple1) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Harry is not rough.
("Harry" "is" "rough" "-")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
((triple2) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple4 triple2) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple3 triple1) -> (rule1 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((triple4 ((triple3 triple1) -> (rule1 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple7