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