Erin is cold. Erin is furry. Erin is kind. Erin is nice. Erin is quiet. Erin is red. Erin is round. Harry is furry. Harry is kind. Harry is nice. Harry is red. Harry is round. If someone is red then they are kind. All furry, quiet people are cold. Red, furry people are quiet. All cold people are furry. If Harry is red and Harry is quiet then Harry is round. All kind people are quiet.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is red then they are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All furry, quiet people are cold.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Red, furry people are quiet.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
All cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If Harry is red and Harry is quiet then Harry is round.
((("Harry" "is" "red" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "round" "+"))
All kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Harry is nice.
True
1
proof
[(triple10)]
("Harry" "is" "nice" "+")
triple10
Erin is not quiet.
False
1
inv-proof
[(triple5 OR ((triple3) -> rule6) OR ((triple6 triple2) -> rule3) OR ((((triple6) -> rule1)) -> rule6) OR ((triple6 ((triple1) -> rule4)) -> rule3))]
("Erin" "is" "quiet" "-")
triple5
((triple3) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple6 triple2) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((triple6 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Harry is quiet.
True
2
proof
[(((triple9) -> rule6) OR ((triple11 triple8) -> rule3) OR ((((triple11) -> rule1)) -> rule6))]
("Harry" "is" "quiet" "+")
((triple9) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple11 triple8) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not quiet.
False
2
inv-proof
[(((triple9) -> rule6) OR ((triple11 triple8) -> rule3) OR ((((triple11) -> rule1)) -> rule6))]
("Harry" "is" "quiet" "-")
((triple9) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple11 triple8) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
@0: Erin is cold.[(triple1 OR ((triple2 triple5) -> rule2) OR ((triple2 ((triple3) -> rule6)) -> rule2) OR ((triple2 ((triple6 triple2) -> rule3)) -> rule2) OR ((triple2 ((((triple6) -> rule1)) -> rule6)) -> rule2))] Erin is furry.[(triple2 OR ((triple1) -> rule4))] Erin is kind.[(triple3 OR ((triple6) -> rule1))] Erin is nice.[(triple4)] Erin is quiet.[(triple5 OR ((triple3) -> rule6) OR ((triple6 triple2) -> rule3) OR ((((triple6) -> rule1)) -> rule6) OR ((triple6 ((triple1) -> rule4)) -> rule3))] Erin is red.[(triple6)] Erin is round.[(triple7)] Harry is furry.[(triple8)] Harry is kind.[(triple9 OR ((triple11) -> rule1))] Harry is nice.[(triple10)] Harry is red.[(triple11)] Harry is round.[(triple12 OR ((triple11 ((triple9) -> rule6)) -> rule5) OR ((triple11 ((triple11 triple8) -> rule3)) -> rule5) OR ((triple11 ((((triple11) -> rule1)) -> rule6)) -> rule5))] @1: Harry is quiet.[(((triple9) -> rule6) OR ((triple11 triple8) -> rule3) OR ((((triple11) -> rule1)) -> rule6))] @2: Harry is cold.[(((triple8 ((triple9) -> rule6)) -> rule2) OR ((triple8 ((triple11 triple8) -> rule3)) -> rule2) OR ((triple8 ((((triple11) -> rule1)) -> rule6)) -> rule2))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
((triple2 triple5) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple2 ((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((triple2 ((triple6 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((triple2 ((((triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple2
((triple1) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple3
((triple6) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
((triple3) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple6 triple2) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((triple6 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
((triple11) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
((triple11 ((triple9) -> (rule6 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple11 ((triple11 triple8) -> (rule3 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple11 ((((triple11) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple9) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple11 triple8) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((triple8 ((triple9) -> (rule6 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple8 ((triple11 triple8) -> (rule3 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple8 ((((triple11) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3