Bob is furry. Bob is green. Bob is nice. Bob is smart. Bob is young. Erin is big. Erin is furry. Erin is green. Erin is nice. Erin is red. Erin is smart. Erin is young. Fiona is big. Fiona is green. Fiona is smart. Fiona is young. If someone is green then they are red. If Erin is furry then Erin is big. Green people are red. If someone is smart then they are nice. If someone is furry and red then they are green. All big people are nice. If someone is nice then they are big. Green, furry people are nice.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If Erin is furry then Erin is big.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "big" "+"))
Green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is furry and red then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Green, furry people are nice.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Bob is smart.
True
1
proof
[(triple4)]
("Bob" "is" "smart" "+")
triple4
Fiona is not smart.
False
1
inv-proof
[(triple15)]
("Fiona" "is" "smart" "-")
triple15
@0: Bob is furry.[(triple1)] Bob is green.[(triple2)] Bob is nice.[(triple3 OR ((triple4) -> rule4) OR ((triple2 triple1) -> rule8))] Bob is smart.[(triple4)] Bob is young.[(triple5)] Erin is big.[(triple6 OR ((triple7) -> rule2) OR ((triple9) -> rule7) OR ((((triple11) -> rule4)) -> rule7) OR ((((triple8 triple7) -> rule8)) -> rule7) OR ((((((triple7 triple10) -> rule5) triple7) -> rule8)) -> rule7))] Erin is furry.[(triple7)] Erin is green.[(triple8 OR ((triple7 triple10) -> rule5))] Erin is nice.[(triple9 OR ((triple11) -> rule4) OR ((triple6) -> rule6) OR ((triple8 triple7) -> rule8) OR ((((triple7) -> rule2)) -> rule6) OR ((((triple7 triple10) -> rule5) triple7) -> rule8))] Erin is red.[(triple10 OR ((triple8) -> rule1) OR ((triple8) -> rule3))] Erin is smart.[(triple11)] Erin is young.[(triple12)] Fiona is big.[(triple13 OR ((((triple15) -> rule4)) -> rule7))] Fiona is green.[(triple14)] Fiona is smart.[(triple15)] Fiona is young.[(triple16)] @1: Bob is big.[(((triple3) -> rule7) OR ((((triple4) -> rule4)) -> rule7) OR ((((triple2 triple1) -> rule8)) -> rule7))] Bob is red.[(((triple2) -> rule1) OR ((triple2) -> rule3))] Fiona is nice.[(((triple13) -> rule6) OR ((triple15) -> rule4))] Fiona is red.[(((triple14) -> rule1) OR ((triple14) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple4) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2 triple1) -> (rule8 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
((triple7) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple9) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple11) -> (rule4 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple8 triple7) -> (rule8 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((((triple7 triple10) -> (rule5 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
triple8
((triple7 triple10) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple9
((triple11) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple6) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple8 triple7) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple7 triple10) -> (rule5 % int2)) triple7) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple10
((triple8) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple8) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
Fiona is big.
("Fiona" "is" "big" "+")
triple13
((((triple15) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
triple14
Fiona is smart.
("Fiona" "is" "smart" "+")
triple15
Fiona is young.
("Fiona" "is" "young" "+")
triple16
Bob is big.
("Bob" "is" "big" "+")
((triple3) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2 triple1) -> (rule8 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple2) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple13) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((triple15) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple14) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple14) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1