Charlie is big. Charlie is blue. Charlie is furry. Charlie is not kind. Charlie is quiet. Charlie is rough. Charlie is white. Erin is big. Erin is not blue. Erin is furry. Erin is not kind. Erin is quiet. Erin is rough. Erin is not white. If something is furry and not quiet then it is kind. All kind, white things are furry. If something is white then it is furry. If something is quiet and not rough then it is white. Quiet things are big. If Erin is blue and Erin is kind then Erin is furry.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is not white.
("Erin" "is" "white" "-")
If something is furry and not quiet then it is kind.
((("something" "is" "furry" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "kind" "+"))
All kind, white things are furry.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If something is quiet and not rough then it is white.
((("something" "is" "quiet" "+") ("something" "is" "rough" "~")) -> ("something" "is" "white" "+"))
Quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If Erin is blue and Erin is kind then Erin is furry.
((("Erin" "is" "blue" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "furry" "+"))
Charlie is big.
True
1
proof
[(triple1 OR ((triple5) -> rule5))]
("Charlie" "is" "big" "+")
triple1
((triple5) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Erin is not rough.
False
1
inv-proof
[(triple13)]
("Erin" "is" "rough" "-")
triple13
@0: Charlie is big.[(triple1 OR ((triple5) -> rule5))] Charlie is blue.[(triple2)] Charlie is furry.[(triple3 OR ((triple7) -> rule3))] Charlie is not kind.[(triple4)] Charlie is quiet.[(triple5)] Charlie is rough.[(triple6)] Charlie is white.[(triple7)] Erin is big.[(triple8 OR ((triple12) -> rule5))] Erin is furry.[(triple10)] Erin is not blue.[(triple9)] Erin is not kind.[(triple11)] Erin is not white.[(triple14)] Erin is quiet.[(triple12)] Erin is rough.[(triple13)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple5) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
((triple7) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
((triple12) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple10
Erin is not blue.
("Erin" "is" "blue" "-")
triple9
Erin is not kind.
("Erin" "is" "kind" "-")
triple11
Erin is not white.
("Erin" "is" "white" "-")
triple14
Erin is quiet.
("Erin" "is" "quiet" "+")
triple12
Erin is rough.
("Erin" "is" "rough" "+")
triple13