Erin is blue. Erin is furry. Erin is not green. Erin is quiet. Erin is rough. Erin is round. Erin is young. Harry is not blue. Harry is furry. Harry is green. Harry is quiet. Harry is rough. Harry is round. Harry is young. If Erin is round then Erin is quiet. All quiet things are rough. If something is rough and young then it is furry.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not green.
("Erin" "is" "green" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If Erin is round then Erin is quiet.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "quiet" "+"))
All quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is rough and young then it is furry.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Harry is not blue.
True
1
proof
[(triple8)]
("Harry" "is" "blue" "-")
triple8
Harry is not green.
False
1
inv-proof
[(triple10)]
("Harry" "is" "green" "-")
triple10
@0: Erin is blue.[(triple1)] Erin is furry.[(triple2 OR ((triple5 triple7) -> rule3) OR ((((triple4) -> rule2) triple7) -> rule3) OR ((((((triple6) -> rule1)) -> rule2) triple7) -> rule3))] Erin is not green.[(triple3)] Erin is quiet.[(triple4 OR ((triple6) -> rule1))] Erin is rough.[(triple5 OR ((triple4) -> rule2) OR ((((triple6) -> rule1)) -> rule2))] Erin is round.[(triple6)] Erin is young.[(triple7)] Harry is furry.[(triple9 OR ((triple12 triple14) -> rule3) OR ((((triple11) -> rule2) triple14) -> rule3))] Harry is green.[(triple10)] Harry is not blue.[(triple8)] Harry is quiet.[(triple11)] Harry is rough.[(triple12 OR ((triple11) -> rule2))] Harry is round.[(triple13)] Harry is young.[(triple14)]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
((triple5 triple7) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple4) -> (rule2 % int2)) triple7) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule2 % int2)) triple7) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is not green.
("Erin" "is" "green" "-")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
((triple6) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple5
((triple4) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple9
((triple12 triple14) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple11) -> (rule2 % int2)) triple14) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is not blue.
("Harry" "is" "blue" "-")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
((triple11) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple13
Harry is young.
("Harry" "is" "young" "+")
triple14