Gary is furry. Gary is green. Gary is kind. Gary is red. Gary is rough. Gary is smart. Harry is furry. Harry is green. Harry is kind. Harry is red. Harry is smart. Harry is white. Smart things are green. All furry things are white. Rough, furry things are kind. Red, kind things are furry. Green, red things are furry. If something is green and kind then it is rough. If something is smart then it is green. If Harry is furry and Harry is kind then Harry is green.
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All furry things are white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Rough, furry things are kind.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Red, kind things are furry.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Green, red things are furry.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If something is green and kind then it is rough.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is smart then it is green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If Harry is furry and Harry is kind then Harry is green.
((("Harry" "is" "furry" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "green" "+"))
Gary is smart.
True
1
proof
[(triple6)]
("Gary" "is" "smart" "+")
triple6
Gary is not smart.
False
1
inv-proof
[(triple6)]
("Gary" "is" "smart" "-")
triple6
Harry is rough.
True
3
proof
[(((triple8 triple9) -> rule6) OR ((((triple11) -> rule1) triple9) -> rule6) OR ((((triple11) -> rule7) triple9) -> rule6) OR ((((triple7 triple9) -> rule8) triple9) -> rule6) OR ((((((triple10 triple9) -> rule4) triple9) -> rule8) triple9) -> rule6))]
("Harry" "is" "rough" "+")
((triple8 triple9) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple11) -> (rule1 % int2)) triple9) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple11) -> (rule7 % int2)) triple9) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7 triple9) -> (rule8 % int2)) triple9) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple10 triple9) -> (rule4 % int3)) triple9) -> (rule8 % int2)) triple9) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Gary is not white.
False
2
inv-proof
[(((triple1) -> rule2) OR ((((triple2 triple4) -> rule5)) -> rule2) OR ((((triple4 triple3) -> rule4)) -> rule2) OR ((((((triple6) -> rule1) triple4) -> rule5)) -> rule2) OR ((((((triple6) -> rule7) triple4) -> rule5)) -> rule2))]
("Gary" "is" "white" "-")
((triple1) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple2 triple4) -> (rule5 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple4 triple3) -> (rule4 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple6) -> (rule1 % int3)) triple4) -> (rule5 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((triple6) -> (rule7 % int3)) triple4) -> (rule5 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
@0: Gary is furry.[(triple1 OR ((triple2 triple4) -> rule5) OR ((triple4 triple3) -> rule4) OR ((((triple6) -> rule1) triple4) -> rule5) OR ((((triple6) -> rule7) triple4) -> rule5))] Gary is green.[(triple2 OR ((triple6) -> rule1) OR ((triple6) -> rule7))] Gary is kind.[(triple3 OR ((triple5 triple1) -> rule3) OR ((triple5 ((triple2 triple4) -> rule5)) -> rule3) OR ((triple5 ((((triple6) -> rule1) triple4) -> rule5)) -> rule3) OR ((triple5 ((((triple6) -> rule7) triple4) -> rule5)) -> rule3))] Gary is red.[(triple4)] Gary is rough.[(triple5 OR ((triple2 triple3) -> rule6) OR ((((triple6) -> rule1) triple3) -> rule6) OR ((((triple6) -> rule7) triple3) -> rule6))] Gary is smart.[(triple6)] Harry is furry.[(triple7 OR ((triple10 triple9) -> rule4) OR ((triple8 triple10) -> rule5) OR ((((triple11) -> rule1) triple10) -> rule5) OR ((((triple11) -> rule7) triple10) -> rule5))] Harry is green.[(triple8 OR ((triple11) -> rule1) OR ((triple11) -> rule7) OR ((triple7 triple9) -> rule8) OR ((((triple10 triple9) -> rule4) triple9) -> rule8))] Harry is kind.[(triple9)] Harry is red.[(triple10)] Harry is smart.[(triple11)] Harry is white.[(triple12 OR ((triple7) -> rule2) OR ((((triple10 triple9) -> rule4)) -> rule2) OR ((((triple8 triple10) -> rule5)) -> rule2) OR ((((((triple11) -> rule1) triple10) -> rule5)) -> rule2) OR ((((((triple11) -> rule7) triple10) -> rule5)) -> rule2))] @1: Gary is white.[(((triple1) -> rule2) OR ((((triple2 triple4) -> rule5)) -> rule2) OR ((((triple4 triple3) -> rule4)) -> rule2) OR ((((((triple6) -> rule1) triple4) -> rule5)) -> rule2) OR ((((((triple6) -> rule7) triple4) -> rule5)) -> rule2))] Harry is rough.[(((triple8 triple9) -> rule6) OR ((((triple11) -> rule1) triple9) -> rule6) OR ((((triple11) -> rule7) triple9) -> rule6) OR ((((triple7 triple9) -> rule8) triple9) -> rule6) OR ((((((triple10 triple9) -> rule4) triple9) -> rule8) triple9) -> rule6))]
Gary is furry.
("Gary" "is" "furry" "+")
triple1
((triple2 triple4) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple4 triple3) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple6) -> (rule1 % int2)) triple4) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple6) -> (rule7 % int2)) triple4) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple2
((triple6) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple6) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple3
((triple5 triple1) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple5 ((triple2 triple4) -> (rule5 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((triple5 ((((triple6) -> (rule1 % int3)) triple4) -> (rule5 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((triple5 ((((triple6) -> (rule7 % int3)) triple4) -> (rule5 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
((triple2 triple3) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple6) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple6) -> (rule7 % int2)) triple3) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
((triple10 triple9) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple8 triple10) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple11) -> (rule1 % int2)) triple10) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple11) -> (rule7 % int2)) triple10) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple8
((triple11) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple11) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple7 triple9) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple10 triple9) -> (rule4 % int2)) triple9) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
((triple7) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple10 triple9) -> (rule4 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple8 triple10) -> (rule5 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple11) -> (rule1 % int3)) triple10) -> (rule5 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple11) -> (rule7 % int3)) triple10) -> (rule5 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((triple1) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple2 triple4) -> (rule5 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple4 triple3) -> (rule4 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple6) -> (rule1 % int3)) triple4) -> (rule5 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((triple6) -> (rule7 % int3)) triple4) -> (rule5 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((triple8 triple9) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple11) -> (rule1 % int2)) triple9) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple11) -> (rule7 % int2)) triple9) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7 triple9) -> (rule8 % int2)) triple9) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple10 triple9) -> (rule4 % int3)) triple9) -> (rule8 % int2)) triple9) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3