Bob is furry. Bob is rough. Bob is young. Erin is big. Erin is furry. Erin is green. Erin is red. Erin is rough. Erin is smart. Erin is young. Harry is big. Harry is furry. Harry is green. Harry is red. Harry is rough. Harry is young. If someone is smart then they are green. All smart, furry people are rough. Young, smart people are red. If someone is big then they are green. If someone is rough and young then they are smart. If someone is red then they are young.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
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 red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is smart then they are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
All smart, furry people are rough.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Young, smart people are red.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If someone is big then they are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is rough and young then they are smart.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
If someone is red then they are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Erin is young.
True
1
proof
[(triple10 OR ((triple7) -> rule6))]
("Erin" "is" "young" "+")
triple10
((triple7) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Bob is not rough.
False
1
inv-proof
[(triple2)]
("Bob" "is" "rough" "-")
triple2
Harry is smart.
True
3
proof
[(((triple15 triple16) -> rule5) OR ((triple15 ((triple14) -> rule6)) -> rule5))]
("Harry" "is" "smart" "+")
((triple15 triple16) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple15 ((triple14) -> (rule6 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((triple2 triple3) -> rule5))]
("Bob" "is" "smart" "-")
((triple2 triple3) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
True
5
proof
[(((triple3 ((triple2 triple3) -> rule5)) -> rule3))]
("Bob" "is" "red" "+")
((triple3 ((triple2 triple3) -> (rule5 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not green.
False
4
inv-proof
[(((((triple2 triple3) -> rule5)) -> rule1))]
("Bob" "is" "green" "-")
((((triple2 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
@0: Bob is furry.[(triple1)] Bob is rough.[(triple2)] Bob is young.[(triple3)] Erin is big.[(triple4)] Erin is furry.[(triple5)] Erin is green.[(triple6 OR ((triple4) -> rule4) OR ((triple9) -> rule1) OR ((((triple8 triple10) -> rule5)) -> rule1) OR ((((triple8 ((triple7) -> rule6)) -> rule5)) -> rule1))] Erin is red.[(triple7 OR ((triple10 triple9) -> rule3) OR ((triple10 ((triple8 triple10) -> rule5)) -> rule3))] Erin is rough.[(triple8 OR ((triple9 triple5) -> rule2))] Erin is smart.[(triple9 OR ((triple8 triple10) -> rule5) OR ((triple8 ((triple7) -> rule6)) -> rule5))] Erin is young.[(triple10 OR ((triple7) -> rule6))] Harry is big.[(triple11)] Harry is furry.[(triple12)] Harry is green.[(triple13 OR ((triple11) -> rule4) OR ((((triple15 triple16) -> rule5)) -> rule1) OR ((((triple15 ((triple14) -> rule6)) -> rule5)) -> rule1))] Harry is red.[(triple14 OR ((triple16 ((triple15 triple16) -> rule5)) -> rule3))] Harry is rough.[(triple15)] Harry is young.[(triple16 OR ((triple14) -> rule6))] @1: Bob is smart.[(((triple2 triple3) -> rule5))] Harry is smart.[(((triple15 triple16) -> rule5) OR ((triple15 ((triple14) -> rule6)) -> rule5))] @2: Bob is green.[(((((triple2 triple3) -> rule5)) -> rule1))] Bob is red.[(((triple3 ((triple2 triple3) -> rule5)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
((triple4) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple9) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple8 triple10) -> (rule5 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple8 ((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
triple7
((triple10 triple9) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple10 ((triple8 triple10) -> (rule5 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple8
((triple9 triple5) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple9
((triple8 triple10) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple8 ((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple10
((triple7) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
triple13
((triple11) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple15 triple16) -> (rule5 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple15 ((triple14) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
triple14
((triple16 ((triple15 triple16) -> (rule5 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple14) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple2 triple3) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple15 triple16) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple15 ((triple14) -> (rule6 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((triple2 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple3 ((triple2 triple3) -> (rule5 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2