Dave is blue. Dave is furry. Dave is kind. Dave is rough. Dave is round. Dave is smart. Dave is white. Harry is blue. Harry is furry. Harry is kind. Harry is rough. Harry is round. Harry is smart. Harry is white. All rough, kind things are blue. If something is smart then it is furry. Kind things are smart. Furry things are smart. Blue, round things are smart. If Dave is furry then Dave is round.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
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" "+")
Harry is white.
("Harry" "is" "white" "+")
All rough, kind things are blue.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Blue, round things are smart.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If Dave is furry then Dave is round.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "round" "+"))
Dave is rough.
True
1
proof
[(triple4)]
("Dave" "is" "rough" "+")
triple4
Harry is not rough.
False
1
inv-proof
[(triple11)]
("Harry" "is" "rough" "-")
triple11
@0: Dave is blue.[(triple1 OR ((triple4 triple3) -> rule1))] Dave is furry.[(triple2 OR ((triple6) -> rule2) OR ((((triple3) -> rule3)) -> rule2) OR ((((triple1 triple5) -> rule5)) -> rule2) OR ((((((triple4 triple3) -> rule1) triple5) -> rule5)) -> rule2))] Dave is kind.[(triple3)] Dave is rough.[(triple4)] Dave is round.[(triple5 OR ((triple2) -> rule6) OR ((((triple6) -> rule2)) -> rule6) OR ((((((triple3) -> rule3)) -> rule2)) -> rule6))] Dave is smart.[(triple6 OR ((triple2) -> rule4) OR ((triple3) -> rule3) OR ((triple1 triple5) -> rule5) OR ((triple1 ((triple2) -> rule6)) -> rule5) OR ((((triple4 triple3) -> rule1) triple5) -> rule5) OR ((((triple4 triple3) -> rule1) ((triple2) -> rule6)) -> rule5))] Dave is white.[(triple7)] Harry is blue.[(triple8 OR ((triple11 triple10) -> rule1))] Harry is furry.[(triple9 OR ((triple13) -> rule2) OR ((((triple10) -> rule3)) -> rule2) OR ((((triple8 triple12) -> rule5)) -> rule2) OR ((((((triple11 triple10) -> rule1) triple12) -> rule5)) -> rule2))] Harry is kind.[(triple10)] Harry is rough.[(triple11)] Harry is round.[(triple12)] Harry is smart.[(triple13 OR ((triple10) -> rule3) OR ((triple9) -> rule4) OR ((triple8 triple12) -> rule5) OR ((((triple11 triple10) -> rule1) triple12) -> rule5))] Harry is white.[(triple14)]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple4 triple3) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple6) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple1 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((((triple4 triple3) -> (rule1 % int3)) triple5) -> (rule5 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
((triple2) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
triple6
((triple2) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple3) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple1 triple5) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple1 ((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple4 triple3) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple4 triple3) -> (rule1 % int3)) ((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
((triple11 triple10) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple9
((triple13) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple8 triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((((triple11 triple10) -> (rule1 % int3)) triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Harry is smart.
("Harry" "is" "smart" "+")
triple13
((triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple9) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple8 triple12) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple11 triple10) -> (rule1 % int2)) triple12) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
triple14