Charlie is not blue. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is rough. Charlie is round. Charlie is smart. Erin is blue. Erin is kind. Erin is quiet. Erin is red. Erin is rough. Erin is round. Erin is not smart. All smart people are rough. If Charlie is not rough then Charlie is not red. If Erin is red and Erin is not round then Erin is not kind. If someone is kind then they are red. If someone is smart and not rough then they are not red. If someone is round then they are red.
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If Charlie is not rough then Charlie is not red.
((("Charlie" "is" "rough" "~")) -> ("Charlie" "is" "red" "-"))
If Erin is red and Erin is not round then Erin is not kind.
((("Erin" "is" "red" "+") ("Erin" "is" "round" "~")) -> ("Erin" "is" "kind" "-"))
If someone is kind then they are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone is smart and not rough then they are not red.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "red" "-"))
If someone is round then they are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Charlie is rough.
True
1
proof
[(triple5 OR ((triple7) -> rule1))]
("Charlie" "is" "rough" "+")
triple5
((triple7) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Erin is not red.
False
1
inv-proof
[(triple11 OR ((triple13) -> rule6) OR ((triple9) -> rule4))]
("Erin" "is" "red" "-")
triple11
((triple13) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple9) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
@0: Charlie is kind.[(triple2)] Charlie is not blue.[(triple1)] Charlie is quiet.[(triple3)] Charlie is red.[(triple4 OR ((triple2) -> rule4) OR ((triple6) -> rule6))] Charlie is rough.[(triple5 OR ((triple7) -> rule1))] Charlie is round.[(triple6)] Charlie is smart.[(triple7)] Erin is blue.[(triple8)] Erin is kind.[(triple9)] Erin is not smart.[(triple14)] Erin is quiet.[(triple10)] Erin is red.[(triple11 OR ((triple13) -> rule6) OR ((triple9) -> rule4))] Erin is rough.[(triple12)] Erin is round.[(triple13)]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
((triple2) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple6) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
((triple7) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is not smart.
("Erin" "is" "smart" "-")
triple14
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple11
((triple13) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple9) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple12
Erin is round.
("Erin" "is" "round" "+")
triple13