Bob is round. If someone is furry then they are red. If someone is furry then they are round. Round people are furry. Red, furry people are green. If someone is smart and not furry then they are green. All green, furry people are blue. If someone is blue then they are big. If Bob is blue then Bob is not smart.
Bob is round.
("Bob" "is" "round" "+")
If someone is furry then they are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If someone is furry then they are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
Red, furry people are green.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
If someone is smart and not furry then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "green" "+"))
All green, furry people are blue.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If Bob is blue then Bob is not smart.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "smart" "-"))
Bob is round.
True
1
proof
[(triple1)]
("Bob" "is" "round" "+")
triple1
Bob is not round.
False
1
inv-proof
[(triple1)]
("Bob" "is" "round" "-")
triple1
Bob is furry.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "furry" "-")
((triple1) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Bob" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not red.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Bob" "is" "red" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is green.
True
6
proof
[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule4))]
("Bob" "is" "green" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not green.
False
6
inv-proof
[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule4))]
("Bob" "is" "green" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
@0: Bob is round.[(triple1)] @1: Bob is furry.[(((triple1) -> rule3))] @2: Bob is red.[(((((triple1) -> rule3)) -> rule1))] @3: Bob is green.[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule4))] @4: Bob is blue.[(((((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule4) ((triple1) -> rule3)) -> rule6))] @5: Bob is big.[(((((((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule4) ((triple1) -> rule3)) -> rule6)) -> rule7))] Bob is not smart.[(((((((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule4) ((triple1) -> rule3)) -> rule6)) -> rule8))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule1 % int3)) ((triple1) -> (rule3 % int4))) -> (rule4 % int2)) ((triple1) -> (rule3 % int4))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
((((((((((triple1) -> (rule3 % int5))) -> (rule1 % int4)) ((triple1) -> (rule3 % int5))) -> (rule4 % int3)) ((triple1) -> (rule3 % int5))) -> (rule6 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
int5
Bob is not smart.
("Bob" "is" "smart" "-")
((((((((((triple1) -> (rule3 % int5))) -> (rule1 % int4)) ((triple1) -> (rule3 % int5))) -> (rule4 % int3)) ((triple1) -> (rule3 % int5))) -> (rule6 % int2))) -> (rule8 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
int5