Bob is quiet. Bob is smart. Bob is white. Furry people are young. If someone is big then they are white. Smart people are white. Young people are kind. If Bob is young and Bob is furry then Bob is smart. If Bob is white then Bob is furry.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If Bob is young and Bob is furry then Bob is smart.
((("Bob" "is" "young" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "smart" "+"))
If Bob is white then Bob is furry.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "furry" "+"))
Bob is white.
True
1
proof
[(triple3 OR ((triple2) -> rule3))]
("Bob" "is" "white" "+")
triple3
((triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule3))]
("Bob" "is" "white" "-")
triple3
((triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
True
2
proof
[(((triple3) -> rule6) OR ((((triple2) -> rule3)) -> rule6))]
("Bob" "is" "furry" "+")
((triple3) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not furry.
False
2
inv-proof
[(((triple3) -> rule6) OR ((((triple2) -> rule3)) -> rule6))]
("Bob" "is" "furry" "-")
((triple3) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
True
3
proof
[(((((triple3) -> rule6)) -> rule1) OR ((((((triple2) -> rule3)) -> rule6)) -> rule1))]
("Bob" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not young.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule1) OR ((((((triple2) -> rule3)) -> rule6)) -> rule1))]
("Bob" "is" "young" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is kind.
True
4
proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule4) OR ((((((((triple2) -> rule3)) -> rule6)) -> rule1)) -> rule4))]
("Bob" "is" "kind" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not kind.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule4) OR ((((((((triple2) -> rule3)) -> rule6)) -> rule1)) -> rule4))]
("Bob" "is" "kind" "-")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
@0: Bob is quiet.[(triple1)] Bob is smart.[(triple2 OR ((((((triple3) -> rule6)) -> rule1) ((triple3) -> rule6)) -> rule5))] Bob is white.[(triple3 OR ((triple2) -> rule3))] @1: Bob is furry.[(((triple3) -> rule6) OR ((((triple2) -> rule3)) -> rule6))] @2: Bob is young.[(((((triple3) -> rule6)) -> rule1) OR ((((((triple2) -> rule3)) -> rule6)) -> rule1))] @3: Bob is kind.[(((((((triple3) -> rule6)) -> rule1)) -> rule4) OR ((((((((triple2) -> rule3)) -> rule6)) -> rule1)) -> rule4))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2)) ((triple3) -> (rule6 % int3))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
triple3
((triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple3) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4