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