Bob is quiet. Bob is rough. Bob is not white. If someone is white and red then they are nice. All quiet people are green. Red people are green. If Bob is white then Bob is not rough. If Bob is green then Bob is nice. All nice, green people are kind.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not white.
("Bob" "is" "white" "-")
If someone is white and red then they are nice.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If Bob is white then Bob is not rough.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "rough" "-"))
If Bob is green then Bob is nice.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "nice" "+"))
All nice, green people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Bob is not white.
True
1
proof
[(triple3)]
("Bob" "is" "white" "-")
triple3
Bob is not quiet.
False
1
inv-proof
[(triple1)]
("Bob" "is" "quiet" "-")
triple1
Bob is green.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "green" "+")
((triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "green" "-")
((triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
True
3
proof
[(((((triple1) -> rule2)) -> rule5))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule5))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
True
6
proof
[(((((((triple1) -> rule2)) -> rule5) ((triple1) -> rule2)) -> rule6))]
("Bob" "is" "kind" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule2 % int3))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not kind.
False
6
inv-proof
[(((((((triple1) -> rule2)) -> rule5) ((triple1) -> rule2)) -> rule6))]
("Bob" "is" "kind" "-")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule2 % int3))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
@0: Bob is not white.[(triple3)] Bob is quiet.[(triple1)] Bob is rough.[(triple2)] @1: Bob is green.[(((triple1) -> rule2))] @2: Bob is nice.[(((((triple1) -> rule2)) -> rule5))] @3: Bob is kind.[(((((((triple1) -> rule2)) -> rule5) ((triple1) -> rule2)) -> rule6))]
Bob is not white.
("Bob" "is" "white" "-")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule2 % int3))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3