Dave is furry. Dave is red. Dave is not rough. If something is furry then it is not blue. If Dave is rough then Dave is not young. White things are young. Young, kind things are not red. If something is red and not blue then it is white. Red things are white.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
If something is furry then it is not blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "-"))
If Dave is rough then Dave is not young.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "young" "-"))
White things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Young, kind things are not red.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "-"))
If something is red and not blue then it is white.
((("something" "is" "red" "+") ("something" "is" "blue" "~")) -> ("something" "is" "white" "+"))
Red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Dave is red.
True
1
proof
[(triple2)]
("Dave" "is" "red" "+")
triple2
Dave is rough.
False
1
inv-proof
[(triple3)]
("Dave" "is" "rough" "+")
triple3
Dave is white.
True
2
proof
[(((triple2) -> rule6) OR ((triple2 ((triple1) -> rule1)) -> rule5))]
("Dave" "is" "white" "+")
((triple2) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple2 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
int2
Dave is not white.
False
2
inv-proof
[(((triple2) -> rule6) OR ((triple2 ((triple1) -> rule1)) -> rule5))]
("Dave" "is" "white" "-")
((triple2) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple2 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
int2
Dave is young.
True
3
proof
[(((((triple2) -> rule6)) -> rule3) OR ((((triple2 ((triple1) -> rule1)) -> rule5)) -> rule3))]
("Dave" "is" "young" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
int3
Dave is not young.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3) OR ((((triple2 ((triple1) -> rule1)) -> rule5)) -> rule3))]
("Dave" "is" "young" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
int3
@0: Dave is furry.[(triple1)] Dave is not rough.[(triple3)] Dave is red.[(triple2)] @1: Dave is not blue.[(((triple1) -> rule1))] Dave is white.[(((triple2) -> rule6) OR ((triple2 ((triple1) -> rule1)) -> rule5))] @2: Dave is young.[(((((triple2) -> rule6)) -> rule3) OR ((((triple2 ((triple1) -> rule1)) -> rule5)) -> rule3))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is not rough.
("Dave" "is" "rough" "-")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is not blue.
("Dave" "is" "blue" "-")
((triple1) -> (rule1 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple2 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
int3