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