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