Bob is big. All furry people are smart. If someone is big then they are smart. If someone is big then they are white. If Bob is big then Bob is not nice. White, smart people are green. If someone is big and rough then they are green. Green people are rough. Nice, green people are rough.
Bob is big.
("Bob" "is" "big" "+")
All furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If someone is big then they are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If Bob is big then Bob is not nice.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "nice" "-"))
White, smart people are green.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is big and rough then they are green.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Nice, green people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is white.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "white" "+")
((triple1) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "white" "-")
((triple1) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
True
5
proof
[(((((triple1) -> rule3) ((triple1) -> rule2)) -> rule5))]
("Bob" "is" "green" "+")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not green.
False
5
inv-proof
[(((((triple1) -> rule3) ((triple1) -> rule2)) -> rule5))]
("Bob" "is" "green" "-")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is rough.
True
6
proof
[(((((((triple1) -> rule3) ((triple1) -> rule2)) -> rule5)) -> rule7))]
("Bob" "is" "rough" "+")
((((((triple1) -> (rule3 % int4)) ((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not rough.
False
6
inv-proof
[(((((((triple1) -> rule3) ((triple1) -> rule2)) -> rule5)) -> rule7))]
("Bob" "is" "rough" "-")
((((((triple1) -> (rule3 % int4)) ((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
@0: Bob is big.[(triple1)] @1: Bob is not nice.[(((triple1) -> rule4))] Bob is smart.[(((triple1) -> rule2))] Bob is white.[(((triple1) -> rule3))] @2: Bob is green.[(((((triple1) -> rule3) ((triple1) -> rule2)) -> rule5))] @3: Bob is rough.[(((((((triple1) -> rule3) ((triple1) -> rule2)) -> rule5)) -> rule7))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is not nice.
("Bob" "is" "nice" "-")
((triple1) -> (rule4 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple1) -> (rule3 % int4)) ((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4