Dave is big. Dave is blue. Dave is furry. Dave is kind. Dave is red. Dave is white. Dave is young. All white, big things are blue. All furry, kind things are white. Red, kind things are big.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
All white, big things are blue.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
All furry, kind things are white.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Red, kind things are big.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Dave is white.
True
1
proof
[(triple6 OR ((triple3 triple4) -> rule2))]
("Dave" "is" "white" "+")
triple6
((triple3 triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not blue.
False
1
inv-proof
[(triple2 OR ((triple6 triple1) -> rule1) OR ((triple6 ((triple5 triple4) -> rule3)) -> rule1) OR ((((triple3 triple4) -> rule2) triple1) -> rule1) OR ((((triple3 triple4) -> rule2) ((triple5 triple4) -> rule3)) -> rule1))]
("Dave" "is" "blue" "-")
triple2
((triple6 triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple6 ((triple5 triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple3 triple4) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple3 triple4) -> (rule2 % int3)) ((triple5 triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
@0: Dave is big.[(triple1 OR ((triple5 triple4) -> rule3))] Dave is blue.[(triple2 OR ((triple6 triple1) -> rule1) OR ((triple6 ((triple5 triple4) -> rule3)) -> rule1) OR ((((triple3 triple4) -> rule2) triple1) -> rule1) OR ((((triple3 triple4) -> rule2) ((triple5 triple4) -> rule3)) -> rule1))] Dave is furry.[(triple3)] Dave is kind.[(triple4)] Dave is red.[(triple5)] Dave is white.[(triple6 OR ((triple3 triple4) -> rule2))] Dave is young.[(triple7)]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple5 triple4) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((triple6 triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple6 ((triple5 triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple3 triple4) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple3 triple4) -> (rule2 % int3)) ((triple5 triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple3 triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple7