Dave is furry. Dave is green. Dave is nice. Dave is red. Dave is round. Dave is white. Dave is young. Harry is furry. Harry is green. Harry is nice. Harry is red. Harry is round. Harry is white. Harry is young. All young, round things are nice. If something is furry and white then it is nice. If something is furry then it is young. If Harry is furry and Harry is red then Harry is young. Furry, nice things are round. If something is round then it is furry. If something is green then it is red. White, green things are young.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
All young, round things are nice.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something is furry and white then it is nice.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is furry then it is young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If Harry is furry and Harry is red then Harry is young.
((("Harry" "is" "furry" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "young" "+"))
Furry, nice things are round.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is round then it is furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
White, green things are young.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
Harry is green.
True
1
proof
[(triple9)]
("Harry" "is" "green" "+")
triple9
Dave is not white.
False
1
inv-proof
[(triple6)]
("Dave" "is" "white" "-")
triple6
@0: Dave is furry.[(triple1 OR ((triple5) -> rule6))] Dave is green.[(triple2)] Dave is nice.[(triple3 OR ((triple1 triple6) -> rule2) OR ((triple7 triple5) -> rule1) OR ((((triple1) -> rule3) triple5) -> rule1) OR ((((triple5) -> rule6) triple6) -> rule2) OR ((((triple6 triple2) -> rule8) triple5) -> rule1) OR ((((((triple5) -> rule6)) -> rule3) triple5) -> rule1))] Dave is red.[(triple4 OR ((triple2) -> rule7))] Dave is round.[(triple5 OR ((triple1 triple3) -> rule5) OR ((triple1 ((triple1 triple6) -> rule2)) -> rule5))] Dave is white.[(triple6)] Dave is young.[(triple7 OR ((triple1) -> rule3) OR ((triple6 triple2) -> rule8) OR ((((triple5) -> rule6)) -> rule3))] Harry is furry.[(triple8 OR ((triple12) -> rule6))] Harry is green.[(triple9)] Harry is nice.[(triple10 OR ((triple14 triple12) -> rule1) OR ((triple8 triple13) -> rule2) OR ((((triple12) -> rule6) triple13) -> rule2) OR ((((triple8) -> rule3) triple12) -> rule1) OR ((((triple13 triple9) -> rule8) triple12) -> rule1) OR ((((triple8 triple11) -> rule4) triple12) -> rule1) OR ((((((triple12) -> rule6)) -> rule3) triple12) -> rule1) OR ((((triple8 ((triple9) -> rule7)) -> rule4) triple12) -> rule1) OR ((((((triple12) -> rule6) triple11) -> rule4) triple12) -> rule1) OR ((((((triple12) -> rule6) ((triple9) -> rule7)) -> rule4) triple12) -> rule1))] Harry is red.[(triple11 OR ((triple9) -> rule7))] Harry is round.[(triple12 OR ((triple8 triple10) -> rule5) OR ((triple8 ((triple8 triple13) -> rule2)) -> rule5))] Harry is white.[(triple13)] Harry is young.[(triple14 OR ((triple8) -> rule3) OR ((triple13 triple9) -> rule8) OR ((triple8 triple11) -> rule4) OR ((((triple12) -> rule6)) -> rule3) OR ((triple8 ((triple9) -> rule7)) -> rule4) OR ((((triple12) -> rule6) triple11) -> rule4) OR ((((triple12) -> rule6) ((triple9) -> rule7)) -> rule4))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
((triple5) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple1 triple6) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple7 triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple1) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple5) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((triple6 triple2) -> (rule8 % int2)) triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((((triple5) -> (rule6 % int3))) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
triple4
((triple2) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple5
((triple1 triple3) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple1 ((triple1 triple6) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple1) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple6 triple2) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple8
((triple12) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple14 triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple8 triple13) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple12) -> (rule6 % int2)) triple13) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple8) -> (rule3 % int2)) triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple13 triple9) -> (rule8 % int2)) triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple8 triple11) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((((triple12) -> (rule6 % int3))) -> (rule3 % int2)) triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((triple8 ((triple9) -> (rule7 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((((triple12) -> (rule6 % int3)) triple11) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple12) -> (rule6 % int4)) ((triple9) -> (rule7 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
triple11
((triple9) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple12
((triple8 triple10) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple8 ((triple8 triple13) -> (rule2 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
triple13
Harry is young.
("Harry" "is" "young" "+")
triple14
((triple8) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple13 triple9) -> (rule8 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple8 triple11) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple12) -> (rule6 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple8 ((triple9) -> (rule7 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple12) -> (rule6 % int2)) triple11) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple12) -> (rule6 % int3)) ((triple9) -> (rule7 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3