Erin is cold. Erin is green. Erin is quiet. Erin is not red. Erin is rough. Erin is smart. Erin is young. Fiona is cold. Fiona is not green. Fiona is quiet. Fiona is red. Fiona is rough. Fiona is smart. Fiona is young. All quiet people are young. Rough, cold people are smart. If someone is quiet and smart then they are cold. All smart people are rough. Smart people are rough. If someone is green and not smart then they are not red.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is not red.
("Erin" "is" "red" "-")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not green.
("Fiona" "is" "green" "-")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
All quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
Rough, cold people are smart.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet and smart then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If someone is green and not smart then they are not red.
((("someone" "is" "green" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "red" "-"))
Erin is quiet.
True
1
proof
[(triple3)]
("Erin" "is" "quiet" "+")
triple3
Fiona is not red.
False
1
inv-proof
[(triple11)]
("Fiona" "is" "red" "-")
triple11
@0: Erin is cold.[(triple1 OR ((triple3 triple6) -> rule3))] Erin is green.[(triple2)] Erin is not red.[(triple4)] Erin is quiet.[(triple3)] Erin is rough.[(triple5 OR ((triple6) -> rule4) OR ((triple6) -> rule5))] Erin is smart.[(triple6 OR ((triple5 triple1) -> rule2))] Erin is young.[(triple7 OR ((triple3) -> rule1))] Fiona is cold.[(triple8 OR ((triple10 triple13) -> rule3))] Fiona is not green.[(triple9)] Fiona is quiet.[(triple10)] Fiona is red.[(triple11)] Fiona is rough.[(triple12 OR ((triple13) -> rule4) OR ((triple13) -> rule5))] Fiona is smart.[(triple13 OR ((triple12 triple8) -> rule2))] Fiona is young.[(triple14 OR ((triple10) -> rule1))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
((triple3 triple6) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple2
Erin is not red.
("Erin" "is" "red" "-")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple5
((triple6) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple6) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple6
((triple5 triple1) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple7
((triple3) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
((triple10 triple13) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is not green.
("Fiona" "is" "green" "-")
triple9
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple10
Fiona is red.
("Fiona" "is" "red" "+")
triple11
Fiona is rough.
("Fiona" "is" "rough" "+")
triple12
((triple13) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((triple13) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple13
((triple12 triple8) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple14
((triple10) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1