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