Bob is smart. Bob is white. Bob is young. If someone is kind then they are rough. All rough, smart people are green. White people are kind.
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
If someone is kind then they are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
All rough, smart people are green.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
White people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Bob is white.
True
1
proof
[(triple2)]
("Bob" "is" "white" "+")
triple2
Bob is not white.
False
1
inv-proof
[(triple2)]
("Bob" "is" "white" "-")
triple2
Bob is kind.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("Bob" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not rough.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("Bob" "is" "rough" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
True
5
proof
[(((((((triple2) -> rule3)) -> rule1) triple1) -> rule2))]
("Bob" "is" "green" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not green.
False
5
inv-proof
[(((((((triple2) -> rule3)) -> rule1) triple1) -> rule2))]
("Bob" "is" "green" "-")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
@0: Bob is smart.[(triple1)] Bob is white.[(triple2)] Bob is young.[(triple3)] @1: Bob is kind.[(((triple2) -> rule3))] @2: Bob is rough.[(((((triple2) -> rule3)) -> rule1))] @3: Bob is green.[(((((((triple2) -> rule3)) -> rule1) triple1) -> rule2))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3