Bob is blue. Bob is green. Bob is quiet. Bob is rough. Bob is round. Bob is smart. Bob is white. If someone is green and round then they are blue. If Bob is smart and Bob is white then Bob is quiet. All rough people are green.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
If someone is green and round then they are blue.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If Bob is smart and Bob is white then Bob is quiet.
((("Bob" "is" "smart" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "quiet" "+"))
All rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
Bob is blue.
True
1
proof
[(triple1 OR ((triple2 triple5) -> rule1) OR ((((triple4) -> rule3) triple5) -> rule1))]
("Bob" "is" "blue" "+")
triple1
((triple2 triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple4) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not rough.
False
1
inv-proof
[(triple4)]
("Bob" "is" "rough" "-")
triple4
@0: Bob is blue.[(triple1 OR ((triple2 triple5) -> rule1) OR ((((triple4) -> rule3) triple5) -> rule1))] Bob is green.[(triple2 OR ((triple4) -> rule3))] Bob is quiet.[(triple3 OR ((triple6 triple7) -> rule2))] Bob is rough.[(triple4)] Bob is round.[(triple5)] Bob is smart.[(triple6)] Bob is white.[(triple7)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple2 triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple4) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple4) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple6 triple7) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7