Bob is green. Bob is white. Dave is big. Dave is blue. Dave is furry. Dave is not green. Dave is white. White people are blue. Furry, white people are round. If someone is green and blue then they are furry. Green people are white. If Bob is blue then Bob is red. If someone is green and not white then they are big. If someone is furry then they are red. If someone is green and not big then they are red.
Bob is green.
("Bob" "is" "green" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is white.
("Dave" "is" "white" "+")
White people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
Furry, white people are round.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is green and blue then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If Bob is blue then Bob is red.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "red" "+"))
If someone is green and not white then they are big.
((("someone" "is" "green" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "big" "+"))
If someone is furry then they are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If someone is green and not big then they are red.
((("someone" "is" "green" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "red" "+"))
Dave is furry.
True
1
proof
[(triple5)]
("Dave" "is" "furry" "+")
triple5
Dave is not blue.
False
1
inv-proof
[(triple4 OR ((triple7) -> rule1))]
("Dave" "is" "blue" "-")
triple4
((triple7) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
True
2
proof
[(((triple5) -> rule7))]
("Dave" "is" "red" "+")
((triple5) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple2) -> rule1) OR ((((triple1) -> rule4)) -> rule1))]
("Bob" "is" "blue" "-")
((triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
True
4
proof
[(((triple1 ((triple2) -> rule1)) -> rule3) OR ((triple1 ((((triple1) -> rule4)) -> rule1)) -> rule3))]
("Bob" "is" "furry" "+")
((triple1 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not furry.
False
4
inv-proof
[(((triple1 ((triple2) -> rule1)) -> rule3) OR ((triple1 ((((triple1) -> rule4)) -> rule1)) -> rule3))]
("Bob" "is" "furry" "-")
((triple1 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is round.
True
6
proof
[(((((triple1 ((triple2) -> rule1)) -> rule3) triple2) -> rule2) OR ((((triple1 ((triple2) -> rule1)) -> rule3) ((triple1) -> rule4)) -> rule2) OR ((((triple1 ((((triple1) -> rule4)) -> rule1)) -> rule3) triple2) -> rule2) OR ((((triple1 ((((triple1) -> rule4)) -> rule1)) -> rule3) ((triple1) -> rule4)) -> rule2))]
("Bob" "is" "round" "+")
((((triple1 ((triple2) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((triple1 ((triple2) -> (rule1 % int4))) -> (rule3 % int3)) ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
((((triple1 ((((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((triple1 ((((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) ((triple1) -> (rule4 % int4))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not round.
False
6
inv-proof
[(((((triple1 ((triple2) -> rule1)) -> rule3) triple2) -> rule2) OR ((((triple1 ((triple2) -> rule1)) -> rule3) ((triple1) -> rule4)) -> rule2) OR ((((triple1 ((((triple1) -> rule4)) -> rule1)) -> rule3) triple2) -> rule2) OR ((((triple1 ((((triple1) -> rule4)) -> rule1)) -> rule3) ((triple1) -> rule4)) -> rule2))]
("Bob" "is" "round" "-")
((((triple1 ((triple2) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((triple1 ((triple2) -> (rule1 % int4))) -> (rule3 % int3)) ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
((((triple1 ((((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((triple1 ((((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) ((triple1) -> (rule4 % int4))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
@0: Bob is green.[(triple1)] Bob is white.[(triple2 OR ((triple1) -> rule4))] Dave is big.[(triple3)] Dave is blue.[(triple4 OR ((triple7) -> rule1))] Dave is furry.[(triple5)] Dave is not green.[(triple6)] Dave is white.[(triple7)] @1: Bob is blue.[(((triple2) -> rule1) OR ((((triple1) -> rule4)) -> rule1))] Dave is red.[(((triple5) -> rule7))] Dave is round.[(((triple5 triple7) -> rule2))] @2: Bob is furry.[(((triple1 ((triple2) -> rule1)) -> rule3) OR ((triple1 ((((triple1) -> rule4)) -> rule1)) -> rule3))] Bob is red.[(((((triple2) -> rule1)) -> rule5) OR ((((((triple1) -> rule4)) -> rule1)) -> rule5) OR ((((triple1 ((triple2) -> rule1)) -> rule3)) -> rule7) OR ((((triple1 ((((triple1) -> rule4)) -> rule1)) -> rule3)) -> rule7))] @3: Bob is round.[(((((triple1 ((triple2) -> rule1)) -> rule3) triple2) -> rule2) OR ((((triple1 ((triple2) -> rule1)) -> rule3) ((triple1) -> rule4)) -> rule2) OR ((((triple1 ((((triple1) -> rule4)) -> rule1)) -> rule3) triple2) -> rule2) OR ((((triple1 ((((triple1) -> rule4)) -> rule1)) -> rule3) ((triple1) -> rule4)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
((triple7) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is not green.
("Dave" "is" "green" "-")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((triple5) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple5 triple7) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple1 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((triple1 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((triple1 ((((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
((((triple1 ((triple2) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((triple1 ((triple2) -> (rule1 % int4))) -> (rule3 % int3)) ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
((((triple1 ((((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((triple1 ((((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) ((triple1) -> (rule4 % int4))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4