Harry is big. Harry is blue. Harry is furry. Harry is kind. Harry is rough. Harry is round. Harry is smart. All rough people are smart. Kind, blue people are rough. If someone is blue then they are kind. If Harry is rough and Harry is kind then Harry is big. If Harry is rough then Harry is big. All smart people are furry. If Harry is rough then Harry is kind. If someone is round and rough then they are furry.
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Kind, blue people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue then they are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If Harry is rough and Harry is kind then Harry is big.
((("Harry" "is" "rough" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "big" "+"))
If Harry is rough then Harry is big.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "big" "+"))
All smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If Harry is rough then Harry is kind.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "kind" "+"))
If someone is round and rough then they are furry.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Harry is round.
True
1
proof
[(triple6)]
("Harry" "is" "round" "+")
triple6
Harry is not blue.
False
1
inv-proof
[(triple2)]
("Harry" "is" "blue" "-")
triple2
@0: Harry is big.[(triple1 OR ((triple5) -> rule5) OR ((triple5 triple4) -> rule4) OR ((((triple4 triple2) -> rule2)) -> rule5) OR ((triple5 ((triple2) -> rule3)) -> rule4) OR ((triple5 ((triple5) -> rule7)) -> rule4) OR ((((triple4 triple2) -> rule2) triple4) -> rule4) OR ((((triple4 triple2) -> rule2) ((triple2) -> rule3)) -> rule4) OR ((((triple4 triple2) -> rule2) ((triple5) -> rule7)) -> rule4) OR ((((((triple2) -> rule3) triple2) -> rule2)) -> rule5) OR ((((((triple2) -> rule3) triple2) -> rule2) triple4) -> rule4) OR ((((((triple2) -> rule3) triple2) -> rule2) ((triple2) -> rule3)) -> rule4) OR ((((((triple2) -> rule3) triple2) -> rule2) ((triple5) -> rule7)) -> rule4))] Harry is blue.[(triple2)] Harry is furry.[(triple3 OR ((triple7) -> rule6) OR ((triple6 triple5) -> rule8) OR ((((triple5) -> rule1)) -> rule6) OR ((triple6 ((triple4 triple2) -> rule2)) -> rule8) OR ((((((triple4 triple2) -> rule2)) -> rule1)) -> rule6) OR ((triple6 ((((triple2) -> rule3) triple2) -> rule2)) -> rule8) OR ((((((((triple2) -> rule3) triple2) -> rule2)) -> rule1)) -> rule6))] Harry is kind.[(triple4 OR ((triple2) -> rule3) OR ((triple5) -> rule7))] Harry is rough.[(triple5 OR ((triple4 triple2) -> rule2) OR ((((triple2) -> rule3) triple2) -> rule2))] Harry is round.[(triple6)] Harry is smart.[(triple7 OR ((triple5) -> rule1) OR ((((triple4 triple2) -> rule2)) -> rule1) OR ((((((triple2) -> rule3) triple2) -> rule2)) -> rule1))]
Harry is big.
("Harry" "is" "big" "+")
triple1
((triple5) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple5 triple4) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple4 triple2) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple5 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((triple5 ((triple5) -> (rule7 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple4 triple2) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple4 triple2) -> (rule2 % int3)) ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple4 triple2) -> (rule2 % int3)) ((triple5) -> (rule7 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2)) ((triple5) -> (rule7 % int3))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
((triple7) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple6 triple5) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple6 ((triple4 triple2) -> (rule2 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple4 triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((triple6 ((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((((triple2) -> (rule3 % int4)) triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
triple4
((triple2) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple5) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple5
((triple4 triple2) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
((triple5) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple4 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3