Erin is big. Erin is blue. Erin is furry. Erin is green. Erin is kind. Erin is smart. Erin is young. Fiona is blue. Fiona is furry. Fiona is green. Fiona is kind. Fiona is young. If something is blue then it is smart. All blue, green things are furry. If something is young then it is smart. All smart, young things are big. Green, young things are smart. If something is green then it is blue. If Fiona is blue then Fiona is furry. If Fiona is blue and Fiona is young then Fiona is smart.
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If something is blue then it is smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
All blue, green things are furry.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If something is young then it is smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
All smart, young things are big.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Green, young things are smart.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is green then it is blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If Fiona is blue then Fiona is furry.
((("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "furry" "+"))
If Fiona is blue and Fiona is young then Fiona is smart.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "young" "+")) -> ("Fiona" "is" "smart" "+"))
Erin is green.
True
1
proof
[(triple4)]
("Erin" "is" "green" "+")
triple4
Erin is not smart.
False
1
inv-proof
[(triple6 OR ((triple2) -> rule1) OR ((triple7) -> rule3) OR ((triple4 triple7) -> rule5) OR ((((triple4) -> rule6)) -> rule1))]
("Erin" "is" "smart" "-")
triple6
((triple2) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple7) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple4 triple7) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Fiona is smart.
True
2
proof
[(((triple12) -> rule3) OR ((triple8) -> rule1) OR ((triple10 triple12) -> rule5) OR ((triple8 triple12) -> rule8) OR ((((triple10) -> rule6)) -> rule1) OR ((((triple10) -> rule6) triple12) -> rule8))]
("Fiona" "is" "smart" "+")
((triple12) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple8) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple10 triple12) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple8 triple12) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple10) -> (rule6 % int2)) triple12) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is not smart.
False
2
inv-proof
[(((triple12) -> rule3) OR ((triple8) -> rule1) OR ((triple10 triple12) -> rule5) OR ((triple8 triple12) -> rule8) OR ((((triple10) -> rule6)) -> rule1) OR ((((triple10) -> rule6) triple12) -> rule8))]
("Fiona" "is" "smart" "-")
((triple12) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple8) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple10 triple12) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple8 triple12) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple10) -> (rule6 % int2)) triple12) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is big.
True
4
proof
[(((((triple12) -> rule3) triple12) -> rule4) OR ((((triple8) -> rule1) triple12) -> rule4) OR ((((triple10 triple12) -> rule5) triple12) -> rule4) OR ((((triple8 triple12) -> rule8) triple12) -> rule4) OR ((((((triple10) -> rule6)) -> rule1) triple12) -> rule4) OR ((((((triple10) -> rule6) triple12) -> rule8) triple12) -> rule4))]
("Fiona" "is" "big" "+")
((((triple12) -> (rule3 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple8) -> (rule1 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple10 triple12) -> (rule5 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple8 triple12) -> (rule8 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((triple10) -> (rule6 % int3))) -> (rule1 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((((triple10) -> (rule6 % int3)) triple12) -> (rule8 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is not big.
False
4
inv-proof
[(((((triple12) -> rule3) triple12) -> rule4) OR ((((triple8) -> rule1) triple12) -> rule4) OR ((((triple10 triple12) -> rule5) triple12) -> rule4) OR ((((triple8 triple12) -> rule8) triple12) -> rule4) OR ((((((triple10) -> rule6)) -> rule1) triple12) -> rule4) OR ((((((triple10) -> rule6) triple12) -> rule8) triple12) -> rule4))]
("Fiona" "is" "big" "-")
((((triple12) -> (rule3 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple8) -> (rule1 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple10 triple12) -> (rule5 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple8 triple12) -> (rule8 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((triple10) -> (rule6 % int3))) -> (rule1 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((((triple10) -> (rule6 % int3)) triple12) -> (rule8 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
@0: Erin is big.[(triple1 OR ((triple6 triple7) -> rule4) OR ((((triple2) -> rule1) triple7) -> rule4) OR ((((triple7) -> rule3) triple7) -> rule4) OR ((((triple4 triple7) -> rule5) triple7) -> rule4) OR ((((((triple4) -> rule6)) -> rule1) triple7) -> rule4))] Erin is blue.[(triple2 OR ((triple4) -> rule6))] Erin is furry.[(triple3 OR ((triple2 triple4) -> rule2) OR ((((triple4) -> rule6) triple4) -> rule2))] Erin is green.[(triple4)] Erin is kind.[(triple5)] Erin is smart.[(triple6 OR ((triple2) -> rule1) OR ((triple7) -> rule3) OR ((triple4 triple7) -> rule5) OR ((((triple4) -> rule6)) -> rule1))] Erin is young.[(triple7)] Fiona is blue.[(triple8 OR ((triple10) -> rule6))] Fiona is furry.[(triple9 OR ((triple8) -> rule7) OR ((triple8 triple10) -> rule2) OR ((((triple10) -> rule6)) -> rule7) OR ((((triple10) -> rule6) triple10) -> rule2))] Fiona is green.[(triple10)] Fiona is kind.[(triple11)] Fiona is young.[(triple12)] @1: Fiona is smart.[(((triple12) -> rule3) OR ((triple8) -> rule1) OR ((triple10 triple12) -> rule5) OR ((triple8 triple12) -> rule8) OR ((((triple10) -> rule6)) -> rule1) OR ((((triple10) -> rule6) triple12) -> rule8))] @2: Fiona is big.[(((((triple12) -> rule3) triple12) -> rule4) OR ((((triple8) -> rule1) triple12) -> rule4) OR ((((triple10 triple12) -> rule5) triple12) -> rule4) OR ((((triple8 triple12) -> rule8) triple12) -> rule4) OR ((((((triple10) -> rule6)) -> rule1) triple12) -> rule4) OR ((((((triple10) -> rule6) triple12) -> rule8) triple12) -> rule4))]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple6 triple7) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple2) -> (rule1 % int2)) triple7) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple7) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple4 triple7) -> (rule5 % int2)) triple7) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple4) -> (rule6 % int3))) -> (rule1 % int2)) triple7) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
triple2
((triple4) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple3
((triple2 triple4) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple4) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
((triple2) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple7) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple4 triple7) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple7
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
((triple10) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple9
((triple8) -> (rule7 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple8 triple10) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule7 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple10) -> (rule6 % int2)) triple10) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
triple10
Fiona is kind.
("Fiona" "is" "kind" "+")
triple11
Fiona is young.
("Fiona" "is" "young" "+")
triple12
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple12) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple8) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple10 triple12) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple8 triple12) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple10) -> (rule6 % int2)) triple12) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((((triple12) -> (rule3 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple8) -> (rule1 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple10 triple12) -> (rule5 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple8 triple12) -> (rule8 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((triple10) -> (rule6 % int3))) -> (rule1 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((((triple10) -> (rule6 % int3)) triple12) -> (rule8 % int2)) triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3