Bob is red. Bob is rough. Bob is young. If Bob is cold then Bob is kind. Kind, young things are green. If Bob is young then Bob is cold.
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
If Bob is cold then Bob is kind.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "kind" "+"))
Kind, young things are green.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If Bob is young then Bob is cold.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "cold" "+"))
Bob is red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "+")
triple1
Bob is not young.
False
1
inv-proof
[(triple3)]
("Bob" "is" "young" "-")
triple3
Bob is cold.
True
2
proof
[(((triple3) -> rule3))]
("Bob" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple3) -> rule3))]
("Bob" "is" "cold" "-")
((triple3) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("Bob" "is" "kind" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("Bob" "is" "kind" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
True
5
proof
[(((((((triple3) -> rule3)) -> rule1) triple3) -> rule2))]
("Bob" "is" "green" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not green.
False
5
inv-proof
[(((((((triple3) -> rule3)) -> rule1) triple3) -> rule2))]
("Bob" "is" "green" "-")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
@0: Bob is red.[(triple1)] Bob is rough.[(triple2)] Bob is young.[(triple3)] @1: Bob is cold.[(((triple3) -> rule3))] @2: Bob is kind.[(((((triple3) -> rule3)) -> rule1))] @3: Bob is green.[(((((((triple3) -> rule3)) -> rule1) triple3) -> rule2))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3