Erin is big. Erin is furry. Erin is not quiet. Erin is red. Erin is round. Erin is white. Erin is young. Harry is big. Harry is furry. Harry is quiet. Harry is red. Harry is round. Harry is white. Harry is young. If something is white and not quiet then it is furry. Young, quiet things are furry. If something is furry and round then it is red. If something is young and not round then it is not red. Big, young things are red. If Harry is big and Harry is not white then Harry is not furry. If Erin is round then Erin is big. If something is quiet then it is big.
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is white and not quiet then it is furry.
((("something" "is" "white" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "furry" "+"))
Young, quiet things are furry.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If something is furry and round then it is red.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is young and not round then it is not red.
((("something" "is" "young" "+") ("something" "is" "round" "~")) -> ("something" "is" "red" "-"))
Big, young things are red.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If Harry is big and Harry is not white then Harry is not furry.
((("Harry" "is" "big" "+") ("Harry" "is" "white" "~")) -> ("Harry" "is" "furry" "-"))
If Erin is round then Erin is big.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "big" "+"))
If something is quiet then it is big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Harry is white.
True
1
proof
[(triple13)]
("Harry" "is" "white" "+")
triple13
Erin is not furry.
False
1
inv-proof
[(triple2 OR ((triple6 triple3) -> rule1))]
("Erin" "is" "furry" "-")
triple2
((triple6 triple3) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
@0: Erin is big.[(triple1 OR ((triple5) -> rule7))] Erin is furry.[(triple2 OR ((triple6 triple3) -> rule1))] Erin is not quiet.[(triple3)] Erin is red.[(triple4 OR ((triple1 triple7) -> rule5) OR ((triple2 triple5) -> rule3) OR ((((triple5) -> rule7) triple7) -> rule5) OR ((((triple6 triple3) -> rule1) triple5) -> rule3))] Erin is round.[(triple5)] Erin is white.[(triple6)] Erin is young.[(triple7)] Harry is big.[(triple8 OR ((triple10) -> rule8))] Harry is furry.[(triple9 OR ((triple14 triple10) -> rule2))] Harry is quiet.[(triple10)] Harry is red.[(triple11 OR ((triple8 triple14) -> rule5) OR ((triple9 triple12) -> rule3) OR ((((triple10) -> rule8) triple14) -> rule5) OR ((((triple14 triple10) -> rule2) triple12) -> rule3))] Harry is round.[(triple12)] Harry is white.[(triple13)] Harry is young.[(triple14)]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple5) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
((triple6 triple3) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
((triple1 triple7) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple2 triple5) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple5) -> (rule7 % int2)) triple7) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple6 triple3) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple10) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple9
((triple14 triple10) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
((triple8 triple14) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple9 triple12) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple10) -> (rule8 % int2)) triple14) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple14 triple10) -> (rule2 % int2)) triple12) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple12
Harry is white.
("Harry" "is" "white" "+")
triple13
Harry is young.
("Harry" "is" "young" "+")
triple14