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