Bob is cold. Bob is kind. Bob is nice. Bob is quiet. Bob is not rough. Bob is smart. Bob is young. Erin is not cold. Erin is quiet. Erin is rough. Erin is smart. Erin is young. If someone is rough then they are nice. All kind, young people are not rough. If someone is cold and not rough then they are smart. If someone is nice and not rough then they are quiet. If someone is rough and not young then they are quiet. If someone is kind and not nice then they are quiet. If someone is smart and not cold then they are quiet. If someone is kind then they are quiet.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
If someone is rough then they are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
All kind, young people are not rough.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "-"))
If someone is cold and not rough then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "smart" "+"))
If someone is nice and not rough then they are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "quiet" "+"))
If someone is rough and not young then they are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "quiet" "+"))
If someone is kind and not nice then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "quiet" "+"))
If someone is smart and not cold then they are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "quiet" "+"))
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Bob is not rough.
True
1
proof
[(triple5 OR ((triple2 triple7) -> rule2))]
("Bob" "is" "rough" "-")
triple5
((triple2 triple7) -> (rule2 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is not quiet.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule8) OR ((triple3 triple5) -> rule4) OR ((triple3 ((triple2 triple7) -> rule2)) -> rule4))]
("Bob" "is" "quiet" "-")
triple4
((triple2) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3 triple5) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3 ((triple2 triple7) -> (rule2 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not rough.
("Bob" "is" "rough" "-")
int2
@0: Bob is cold.[(triple1)] Bob is kind.[(triple2)] Bob is nice.[(triple3)] Bob is not rough.[(triple5 OR ((triple2 triple7) -> rule2))] Bob is quiet.[(triple4 OR ((triple2) -> rule8) OR ((triple3 triple5) -> rule4) OR ((triple3 ((triple2 triple7) -> rule2)) -> rule4))] Bob is smart.[(triple6 OR ((triple1 triple5) -> rule3) OR ((triple1 ((triple2 triple7) -> rule2)) -> rule3))] Bob is young.[(triple7)] Erin is not cold.[(triple8)] Erin is quiet.[(triple9 OR ((triple11 triple8) -> rule7))] Erin is rough.[(triple10)] Erin is smart.[(triple11)] Erin is young.[(triple12)] @1: Erin is nice.[(((triple10) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not rough.
("Bob" "is" "rough" "-")
triple5
((triple2 triple7) -> (rule2 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple2) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3 triple5) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3 ((triple2 triple7) -> (rule2 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not rough.
("Bob" "is" "rough" "-")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple1 triple5) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple1 ((triple2 triple7) -> (rule2 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not rough.
("Bob" "is" "rough" "-")
int2
Bob is young.
("Bob" "is" "young" "+")
triple7
Erin is not cold.
("Erin" "is" "cold" "-")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
((triple11 triple8) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
Erin is nice.
("Erin" "is" "nice" "+")
((triple10) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1