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